load ../../rtp fmod P-TWENTYNINE is pr PRED-BASE . sort S . op G : S -> Atom [metadata "74"] . op H : S -> Atom [metadata "75"] . op P : S -> Atom [metadata "76"] . op J : S -> Atom [metadata "77"] . op f-x''' : S S S -> S [metadata "22"] . op f-x'''' : S S S -> S [metadata "23"] . op f-y' : S S S -> S [metadata "24"] . op f-x'' : S S S -> S [metadata "25"] . endfm fmod TEST is inc RTP . inc P-TWENTYNINE . eq USER-MODULE-NAME = 'P-TWENTYNINE . endfm red !(( ((empty).AtomMagma -> G(f-x'''(x:S,x':S,y:S))), (H(f-x''''(x:S,x':S,y:S)) -> G(f-x''''(x:S,x':S,y:S)),G(f-y'(x:S,x':S,y:S))), (H(f-x''''(x:S,x':S,y:S)),P(x:S) -> G(f-x''''(x:S,x':S,y:S)),H(x:S)), (G(x:S),H(f-x''''(x:S,x':S,y:S)) -> G(f-x''''(x:S,x':S,y:S)),J(x:S)), ((empty).AtomMagma -> G(f-x''''(x:S,x':S,y:S)),P(f-x''''(x:S,x':S,y:S))), (H(f-x''''(x:S,x':S,y:S)),J(f-y'(x:S,x':S,y:S)) -> G(f-x''''(x:S,x':S,y:S))), (G(y:S),P(x':S) -> G(f-y'(x:S,x':S,y:S)),H(x':S)), (G(y:S),P(x':S) -> G(f-y'(x:S,x':S,y:S)),J(y:S)), (H(f-x''''(x:S,x':S,y:S)),J(f-x''''(x:S,x':S,y:S)) -> G(f-y'(x:S,x':S,y:S))), (G(y:S),P(x:S),P(x':S) -> H(x:S),H(x':S)), (G(y:S),P(x:S),P(x':S) -> H(x:S),J(y:S)), (H(f-x''''(x:S,x':S,y:S)),J(f-x''''(x:S,x':S,y:S)),P(x:S) -> H(x:S)), (G(x:S),G(y:S),P(x':S) -> H(x':S),J(x:S)), (G(y:S),P(x':S) -> H(x':S),P(f-x''''(x:S,x':S,y:S))), (G(y:S),H(f-x''''(x:S,x':S,y:S)),J(f-y'(x:S,x':S,y:S)),P(x':S) -> H(x':S)), (G(x:S),G(y:S),P(x':S) -> J(x:S),J(y:S)), (G(x:S),H(f-x''''(x:S,x':S,y:S)),J(f-x''''(x:S,x':S,y:S)) -> J(x:S)), (G(y:S),P(x':S) -> J(y:S),P(f-x''''(x:S,x':S,y:S))), (G(y:S),H(f-x''''(x:S,x':S,y:S)),J(f-y'(x:S,x':S,y:S)),P(x':S) -> J(y:S)), ((empty).AtomMagma -> P(f-x''(x:S,x':S,y:S))), (J(f-x''''(x:S,x':S,y:S)) -> P(f-x''''(x:S,x':S,y:S))), (H(f-x''''(x:S,x':S,y:S)),J(f-x''''(x:S,x':S,y:S)),J(f-y'(x:S,x':S,y:S)) -> (empty).AtomMagma) )) . q . --- Input: ((EX x. (P(x))) /\ (EX x. (G(x)))) => (((ALL x. ((P(x)) => (H(x)))) /\ (ALL x. ((G(x)) => (J(x))))) <=> (ALL x. (ALL y. (((P(x)) /\ (G(y))) => ((H(x)) /\ (J(y))))))) --- Generalize: ((EX x. (P(x))) /\ (EX x. (G(x)))) => (((ALL x. ((P(x)) => (H(x)))) /\ (ALL x. ((G(x)) => (J(x))))) <=> (ALL x. (ALL y. (((P(x)) /\ (G(y))) => ((H(x)) /\ (J(y))))))) --- After Negation: ~(((EX x. (P(x))) /\ (EX x. (G(x)))) => (((ALL x. ((P(x)) => (H(x)))) /\ (ALL x. ((G(x)) => (J(x))))) <=> (ALL x. (ALL y. (((P(x)) /\ (G(y))) => ((H(x)) /\ (J(y)))))))) --- After Prenex: ALL x. (ALL x'. (ALL y. (EX x''. (EX x'''. (EX x''''. (EX y'. (((P(x'')) /\ (G(x'''))) /\ (((((~(P(x))) \/ (H(x))) /\ ((~(G(x))) \/ (J(x)))) /\ (((P(x'''')) /\ (G(y'))) /\ ((~(H(x''''))) \/ (~(J(y')))))) \/ ((((P(x'''')) /\ (~(H(x'''')))) \/ ((G(x'''')) /\ (~(J(x''''))))) /\ (((~(P(x'))) \/ (~(G(y)))) \/ ((H(x')) /\ (J(y))))))))))))) --- After Skolemization: ((P(f_x''(x,x',y))) /\ (G(f_x'''(x,x',y)))) /\ (((((~(P(x))) \/ (H(x))) /\ ((~(G(x))) \/ (J(x)))) /\ (((P(f_x''''(x,x',y))) /\ (G(f_y'(x,x',y)))) /\ ((~(H(f_x''''(x,x',y)))) \/ (~(J(f_y'(x,x',y))))))) \/ ((((P(f_x''''(x,x',y))) /\ (~(H(f_x''''(x,x',y))))) \/ ((G(f_x''''(x,x',y))) /\ (~(J(f_x''''(x,x',y)))))) /\ (((~(P(x'))) \/ (~(G(y)))) \/ ((H(x')) /\ (J(y)))))) --- After simpcnf: [[G(f_x'''(x,x',y))], [G(f_x''''(x,x',y)),G(f_y'(x,x',y)),~(H(f_x''''(x,x',y)))], [G(f_x''''(x,x',y)),H(x),~(H(f_x''''(x,x',y))),~(P(x))], [G(f_x''''(x,x',y)),J(x),~(G(x)),~(H(f_x''''(x,x',y)))], [G(f_x''''(x,x',y)),P(f_x''''(x,x',y))], [G(f_x''''(x,x',y)),~(H(f_x''''(x,x',y))),~(J(f_y'(x,x',y)))], [G(f_y'(x,x',y)),H(x'),~(G(y)),~(P(x'))], [G(f_y'(x,x',y)),J(y),~(G(y)),~(P(x'))], [G(f_y'(x,x',y)),~(H(f_x''''(x,x',y))),~(J(f_x''''(x,x',y)))], [H(x),H(x'),~(G(y)),~(P(x)),~(P(x'))], [H(x),J(y),~(G(y)),~(P(x)),~(P(x'))], [H(x),~(H(f_x''''(x,x',y))),~(J(f_x''''(x,x',y))),~(P(x))], [H(x'),J(x),~(G(x)),~(G(y)),~(P(x'))], [H(x'),P(f_x''''(x,x',y)),~(G(y)),~(P(x'))], [H(x'),~(G(y)),~(H(f_x''''(x,x',y))),~(J(f_y'(x,x',y))),~(P(x'))], [J(x),J(y),~(G(x)),~(G(y)),~(P(x'))], [J(x),~(G(x)),~(H(f_x''''(x,x',y))),~(J(f_x''''(x,x',y)))], [J(y),P(f_x''''(x,x',y)),~(G(y)),~(P(x'))], [J(y),~(G(y)),~(H(f_x''''(x,x',y))),~(J(f_y'(x,x',y))),~(P(x'))], [P(f_x''(x,x',y))], [P(f_x''''(x,x',y)),~(J(f_x''''(x,x',y)))], [~(H(f_x''''(x,x',y))),~(J(f_x''''(x,x',y))),~(J(f_y'(x,x',y)))]] --- Harrison resolution returned [true, true, true, true] taking 0.003742 --- Our Harrison resolution solved: true