% problem-set/pelletier/p45.clauses
% created : 07/25/86
% revised : 08/17/89

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

% representation:
%
% declare_predicates(2,[H,J]).
% declare_predicates(1,[F,G,K,L]).
% declare_variables([x,y]).


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