Basic defining clauses

list(usable).
a(x,y) = p1 | a(a(notp1,x),y) = p1.
end_of_list.

Proof of a(x,y) = p1 | a(a(notp1,x),y) = p1. | OTTER output file

list(usable).
a(x,y) != p1 | a(a(notp1,x),y) = p2.
end_of_list.

Proof of a(x,y) != p1 | a(a(notp1,x),y) = p2. | OTTER output file

up show outline