% This is a simple example due to Loveland, JACM 74, 
% in which he demonstrates the power of a certain
% model generation technique. 
% The consistency proof is no problem for ordered resolution 
% provided the ordering is the right one.
% As usual for flat formulas, predicates should have a lower
% precedence that function symbols.

predicates([p,q]).

q(X,Y),q(f(X,Y),f(X,Y)) -> [].
p(X,Y),p(f(X,Y),f(X,Y)).
q(X,Y),q(f(X,Y),f(X,Y)).
p(X,Y),p(f(X,Y),f(X,Y)) -> q(f(X,Y),f(X,Y)).
q(f(X,Y),f(X,Y)) -> p(X,Y).
p(X,Y),q(Y,f(X,Y)) -> p(X,f(X,Y)).
p(X,Y),p(Y,f(X,Y)) -> q(X,f(X,Y)).

precedence([f,p,q]).