% problem-set/pelletier/p38b.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))]} % Second half : <- direction % representation: % % declare_predicate(2,R). % declare_predicate(1,P). % declare_constant(a). % declare_variables([x,y,z,w]). set(hyper_res). set(factor). set(process_input). set(simplify_fol). set(delete_identical_nested_skolem). formula_list(sos). % denial of the statement -( (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)))))))) -> (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)))))) ). end_of_list.