File "stdin", line 2, characters 7-11:
Error: Tactic failure: Cannot solve this goal.