% problem-set/miscellany/wang/exq2.ver2.clauses
% created : 07/24/86 
% revised : 07/14/88 
   
% description:
%
% THIS PROBLEM IS EXQ2, PROPOSED BY WANG TO TEST THEOREM PROVERS                              
% representation:
%
% declare_constants([b,k,m,j]).
% declare_functions(1,[f,g]).
% declare_predicates(2,[R,P]).
% declare_variables([x,y,z,v,v1,v2,v3]).


 -R(m,b).
  R(b,k) |  R(m,k).
  R(y,j) | -R(y,k) |  P(y,j).
  R(y,j) |  R(y,k) | -P(y,j).
  R(y,m) | -P(y,m) | -R(f(y),m).
  R(y,m) | -P(y,m) | -R(f(y),y).
  R(y,m) | -P(y,m) |  P(y,f(y)).
  R(y,m) | -P(y,m) |  P(f(y),y).
  R(y,m) |  P(y,m) |  R(v1,m) |  R(v1,y) | -P(y,v1) | -P(v1,y).
  R(y,b) | P(y,b) | -R(g(y),b).
  R(y,b) | P(y,b) | -R(g(y),y).
  R(y,b) | P(y,b) |  P(y,g(y)).
  R(y,b) | P(y,b) |  P(g(y),y).
  R(y,b) |  -P(y,b) |  R(v,b) |  R(v,y) | -P(y,v) | -P(v,y).
  R(y,k) | -R(y,m) |  P(y,k).
  R(y,k) | -R(y,b) |  P(y,k).
  R(y,k) |  R(y,m) |  R(y,b) | -P(y,k).

% Equality Axioms 
  R(x,x).
 -R(x,y) |  R(y,x).
 -R(x,y) | -R(y,z) |  R(x,z).

% Equality Substitution Axioms 
 -R(x,y) | -P(x,z) |  P(y,z).
 -R(x,y) | -P(z,x) |  P(z,y).
 -R(x,y) |  R(f(x),f(y)).
-R(x,y) |  R(g(x),g(y)).