/*
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))))).
*/

all(X,f(X) and all(Y,g(Y) and h(X,Y) => j(X,Y)) => all(Y,g(Y) and h(X,Y) => k(Y))).
~exists(Y,l(Y) and k(Y)).
exists(X,f(X) and all(Y,h(X,Y) => l(Y)) and all(Y,g(Y) and h(X,Y) => j(X,Y))).

~exists(X,f(X) and ~exists(Y,g(Y) and h(X,Y))).


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