% problem-set/pelletier/p37.in
% created : 08/17/89
% revised : 08/17/89

% description:
%
% Full Predicate Logic (without Identity and Functions). Problem #37.
% (Az)(Ew)(Ax)(Ey)[(Pxz -> Pyw) & Pyz & (Pyw -> (Eu)Quw)]
% (Ax)(Az)[-Pxz -> (Ey)Qyz]
% (Ex)(Ey)Qxy -> (Ax)Rxx
% ---------------------------------------------
% (Ax)(Ey)Rxy
 
% representation:
%
% declare_predicates(2,[P,Q,R]).
% declare_variables([x,y,z,w,u]).


set(hyper_res).
set(ur_res).
set(factor).
set(simplify_fol).


formula_list(sos).

% premises
(all z exists w all x exists y ( (P(x,z) -> P(y,w)) & (P(y,z) & 
	(P(y,w) -> (exists u Q(u,w)))))).
(all x all z -(P(x,z) -> (exists y Q(y,z)))).
((exists x exists y Q(x,y)) -> (all x R(x,x))).

% denial of the statement
-(all x exists y R(x,y)).

end_of_list.
