Prover9 Goals List (optional)

  assign(max_proofs, -1).

  clauses(goals).

  f(A,f(A,A)) != f(B,f(B,B))    # answer(constant).

  f(B,A) != f(A,B)              # answer(commute).

  f(B,A) != f(A,B) | f(f(B,A),f(B,f(A,C))) != B # answer(BA) # action(in_proof -> exit).

  end_of_list.

• Goals are back demodulated!
• Goals are back unit deleted.
• Goals are not used for subsumption.
• If a proof is found, the goal can be disabled (the default) or reused.