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

% description:
% 
% Full Predicate Logic (without Identity and Functions).
% This is problem #38 from "Seventy-five Problems for Testing
% Automated Theorem Provers", paper by Francis Jeffry Pelletier.
% {(Ax)[Pa & (Px -> (Ey)(Py & Rxy)) -> (Ez)(Ew)(Pz & Rxw & Rwz)] <->
% (Ax)[-Pa | Px | (Ez)(Ew)Pz & Rxw & Rwz)) &
% (-Pa | -(Ey)(Py & Rxy) | (Ez)(Ew)(Pz & Rxw & Rwz))]}
% First half : -> direction

% representation:
% 
% declare_predicate(2,R).
% declare_predicate(1,P).
% declare_variables([x,y,z,w]).

set(hyper_res).
set(factor).
set(process_input).
set(simplify_fol).

formula_list(sos).

% denial of the statement
-((all x ((P(a) & (P(x) -> (exists y (P(y) & R(x,y))))) -> 
	(exists z exists w (P(z) & (R(x,w) & R(w,z)))))) 
->
 (all x ((-P(a) | (P(x) | (exists z exists w (P(z) & (R(x,w) & R(w,z)))))) &
	(-P(a) | (-(exists y (P(y) & R(x,y))) | 
		(exists z exists w (P(z) & (R(x,w) & R(w,z)))))))
)).

end_of_list.
