load ../../rtp fmod P-THIRTYSIX is pr PRED-BASE . sort S . op G : S S -> Atom [metadata "95"] . op H : S S -> Atom [metadata "96"] . op P : S S -> Atom [metadata "97"] . op f-y'' : S S S -> S [metadata "35"] . op f-y' : S S S -> S [metadata "36"] . op f-x' : S S S -> S [metadata "37"] . endfm fmod TEST is inc RTP . inc P-THIRTYSIX . eq USER-MODULE-NAME = 'P-THIRTYSIX . endfm red !(( ((empty).AtomMagma -> G(x:S,f-y''(x:S,y:S,z:S))), (G(x:S,y:S),G(y:S,z:S) -> H(x:S,z:S)), (G(x:S,y:S),P(y:S,z:S) -> H(x:S,z:S)), (G(y:S,z:S),P(x:S,y:S) -> H(x:S,z:S)), (P(x:S,y:S),P(y:S,z:S) -> H(x:S,z:S)), ((empty).AtomMagma -> P(x:S,f-y'(x:S,y:S,z:S))), (H(f-x'(x:S,y:S,z:S),y''':S) -> (empty).AtomMagma) )) . q . --- Input: ((ALL x. (EX y. (P(x,y)))) /\ ((ALL x. (EX y. (G(x,y)))) /\ (ALL x. (ALL y. (((P(x,y)) \/ (G(x,y))) => (ALL z. (((P(y,z)) \/ (G(y,z))) => (H(x,z))))))))) => (ALL x. (EX y. (H(x,y)))) --- Generalize: ((ALL x. (EX y. (P(x,y)))) /\ ((ALL x. (EX y. (G(x,y)))) /\ (ALL x. (ALL y. (((P(x,y)) \/ (G(x,y))) => (ALL z. (((P(y,z)) \/ (G(y,z))) => (H(x,z))))))))) => (ALL x. (EX y. (H(x,y)))) --- After Negation: ~(((ALL x. (EX y. (P(x,y)))) /\ ((ALL x. (EX y. (G(x,y)))) /\ (ALL x. (ALL y. (((P(x,y)) \/ (G(x,y))) => (ALL z. (((P(y,z)) \/ (G(y,z))) => (H(x,z))))))))) => (ALL x. (EX y. (H(x,y))))) --- After Prenex: ALL x. (ALL y. (ALL z. (EX y'. (EX y''. (EX x'. (ALL y'''. (((P(x,y')) /\ ((G(x,y'')) /\ (((~(P(x,y))) /\ (~(G(x,y)))) \/ (((~(P(y,z))) /\ (~(G(y,z)))) \/ (H(x,z)))))) /\ (~(H(x',y''')))))))))) --- After Skolemization: ((P(x,f_y'(x,y,z))) /\ ((G(x,f_y''(x,y,z))) /\ (((~(P(x,y))) /\ (~(G(x,y)))) \/ (((~(P(y,z))) /\ (~(G(y,z)))) \/ (H(x,z)))))) /\ (~(H(f_x'(x,y,z),y'''))) --- After simpcnf: [[G(x,f_y''(x,y,z))], [H(x,z),~(G(x,y)),~(G(y,z))], [H(x,z),~(G(x,y)),~(P(y,z))], [H(x,z),~(G(y,z)),~(P(x,y))], [H(x,z),~(P(x,y)),~(P(y,z))], [P(x,f_y'(x,y,z))], [~(H(f_x'(x,y,z),y'''))]] --- Harrison resolution returned [true] taking 0.005177 --- Our Harrison resolution solved: true