%
%  A problem from Vladimir Lifschitz
%
%  This problem was suggested as a challenge to resolution programs.
%  It is easily solved by Maslov's inverse method.
%

set(auto).

formula_list(usable).
-(exists x exists x1 all y exists z exists z1 
     (  ( -p(y,y) | p(x,x)   | -s(z,x)  ) &
        ( s(x,y)  | -s(y,z)  | q(z1,z1) ) &
        ( q(x1,y) | -q(y,z1) | s(x1,x1) )  )).
end_of_list.