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

% description:
%
% Full Predicate Logic (without Identities and Functions)..
% (Ax)(Fx & (Ay)[Fy & Hyx -> Gy] -> Gx).
% {(Ex)(Fx & -Gx) ->.
%  (Ex)(Fx & -Gx & (Ay)(Fy & -Gy -> Jxy)}.
% (Ax)(Ay)(Fx & Fy & Hxy -> -Jyx).
% --------------------------------.
% (Ax)(Fx -> Gx).

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

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

% denial of conclusion
-(all x (F(x) -> G(x))).