/*
problem-set/pelletier/p45.out


description:

Full Predicate Logic (without Identities and Functions)..
(Ax)(Fx & (Ay)[Gy & Hxy -> Jxy] -> (Ay)(Gy & Hxy -> Ky)).
-(Ey)(Ly & Ky).
(Ex)[Fx & (Ay)(Hxy -> Ly) &.
---------------------------.
(Ay)(Gy & Hxy -> Jxy)].
----------------------.
(Ex)(Fx & -(Ey)(Gy & Hxy)).


premises
(all x ((F(x) & (all y ((G(y) & H(x,y)) -> J(x,y)))) -> 
	(all y ((G(y) & H(x,y)) -> K(y))))).
-(exists y (L(y) & K(y))).
(exists x (F(x) & 
	((all y (H(x,y) -> L(y))) & (all y ((G(y) & H(x,y)) -> J(x,y)))))).

denial of conclusion
-(exists x (F(x) & -(exists y (G(y) & H(x,y))))).
*/


first_predicate_precedence( [f,g,h,j,k,m] ).
precedence( [f1,f2,c1,c2] ).
predicates( [f,g,h,j,k,m] ).


axiom( [ [f(X),g(Y),h(X,Y)], [g(f1(X)),k(Y)] ] ).
axiom( [ [f(X),g(Y),h(X,Y)],[h(X,f1(X)),k(Y)] ] ).
axiom( [ [f(X),j(X,f1(X)),g(Y),h(X,Y)], [k(Y)] ] ).
axiom( [ [m(Y),k(Y)], [] ] ).
axiom( [ [], [f(c1)] ] ).
axiom( [ [h(c1,Y)], [m(Y)] ] ).
axiom( [ [g(X1),h(c1,X1)], [j(c1,X1)] ] ).
axiom( [ [f(X)], [g(f2(X))] ] ).
axiom( [ [f(X)], [h(X,f2(X))] ] ).