load ../../rtp fmod P-THIRTYTHREE is pr PRED-BASE . sort S . op P : S -> Atom [metadata "93"] . op c-c : -> S [metadata "29"] . op c-a : -> S [metadata "30"] . op c-b : -> S [metadata "31"] . op f-x'' : S S -> S [metadata "32"] . endfm fmod TEST is inc RTP . inc P-THIRTYTHREE . eq USER-MODULE-NAME = 'P-THIRTYTHREE . endfm red !(( (P(c-a) -> P(x:S),P(x':S),P(c-c)), ((empty).AtomMagma -> P(c-a)), (P(f-x''(x:S,x':S)) -> P(c-b)), (P(c-a),P(c-b) -> P(c-c)), (P(c-c) -> (empty).AtomMagma) )) . q . --- Input: (ALL x. (((P(a)) /\ ((P(x)) => (P(b)))) => (P(c)))) <=> ((ALL x. ((P(a)) => ((P(x)) \/ (P(c))))) /\ ((P(a)) => ((P(b)) => (P(c))))) --- Generalize: ALL a. (ALL b. (ALL c. ((ALL x. (((P(a)) /\ ((P(x)) => (P(b)))) => (P(c)))) <=> ((ALL x. ((P(a)) => ((P(x)) \/ (P(c))))) /\ ((P(a)) => ((P(b)) => (P(c)))))))) --- After Negation: ~(ALL a. (ALL b. (ALL c. ((ALL x. (((P(a)) /\ ((P(x)) => (P(b)))) => (P(c)))) <=> ((ALL x. ((P(a)) => ((P(x)) \/ (P(c))))) /\ ((P(a)) => ((P(b)) => (P(c))))))))) --- After Prenex: EX a. (EX b. (EX c. (ALL x. (ALL x'. (EX x''. (((((~(P(a))) \/ ((P(x)) /\ (~(P(b))))) \/ (P(c))) /\ (((P(a)) /\ ((~(P(x''))) /\ (~(P(c))))) \/ ((P(a)) /\ ((P(b)) /\ (~(P(c))))))) \/ ((((P(a)) /\ ((~(P(x''))) \/ (P(b)))) /\ (~(P(c)))) /\ (((~(P(a))) \/ ((P(x')) \/ (P(c)))) /\ ((~(P(a))) \/ ((~(P(b))) \/ (P(c)))))))))))) --- After Skolemization: ((((~(P(c_a))) \/ ((P(x)) /\ (~(P(c_b))))) \/ (P(c_c))) /\ (((P(c_a)) /\ ((~(P(f_x''(x,x')))) /\ (~(P(c_c))))) \/ ((P(c_a)) /\ ((P(c_b)) /\ (~(P(c_c))))))) \/ ((((P(c_a)) /\ ((~(P(f_x''(x,x')))) \/ (P(c_b)))) /\ (~(P(c_c)))) /\ (((~(P(c_a))) \/ ((P(x')) \/ (P(c_c)))) /\ ((~(P(c_a))) \/ ((~(P(c_b))) \/ (P(c_c)))))) --- After simpcnf: [[P(x),P(x'),P(c_c),~(P(c_a))], [P(c_a)], [P(c_b),~(P(f_x''(x,x')))], [P(c_c),~(P(c_a)),~(P(c_b))], [~(P(c_c))]] --- Harrison resolution returned [true, true, true] taking 0.001843 --- Our Harrison resolution solved: true