Defining clauses for setof using p1 and p2.

list(usable).
a(p2,xy) != a(xf,a(p1,xy)) | a(a(setof,xf),xy) = p1.
end_of_list.

Proof of a(p2,xy) != a(xf,a(p1,xy)) | a(a(setof,xf),xy) = p1. | OTTER output file

list(usable).
a(p2,xy) = a(xf,a(p1,xy)) | a(a(setof,xf),xy) = p2.
end_of_list.

Proof of a(p2,xy) = a(xf,a(p1,xy)) | a(a(setof,xf),xy) = p2. | OTTER output file

up | previous | next | detailed contents | brief contents