% problem-set/pelletier/p36.clauses
% created : 08/17/89
% revised : 08/17/89

% description:
%
% Full Predicate Logic (without Identity and Functions). Problem #35.
% (Ax)(Ey)Fxy
% (Ax)(Ey)Gxy
% (Ax)(Ay)((Fxy | Gxy) -> (Az)((Fyz | Gyz) -> Hxz)) 
% -------------------------------------------------
% (Ax)(Ey)Hxy

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


% premises
(all x exists y F(x,y)).
(all x exists y G(x,y)).
(all x all y ((F(x,y) | G(x,y)) -> (all z ((F(y,z) | G(y,z)) -> H(x,z))))).

% denial of the conclusion
-(all x exists y H(x,y)).