% problem from Manthey/Bry conveyed by Marc Bezem

true => exists(a), exists(b), exists(c), exists(d).

p(a,b) => goal.    
q(c,d) => goal.    

p(X,Y) => p(Y,X).
q(X,Y) => q(Y,X).
p(X,Y),p(Y,Z) => p(X,Z).
q(X,Y),q(Y,Z) => q(X,Z).

exists(X),exists(Y) => p(X,Y);q(X,Y).