% 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)).