load ../../rtp fmod P-TWENTYTWO is pr PRED-BASE . sort S . op P : -> Atom [metadata "47"] . op Q : S -> Atom [metadata "48"] . op f-x' : S -> S [metadata "10"] . endfm fmod TEST is inc RTP . inc P-TWENTYTWO . eq USER-MODULE-NAME = 'P-TWENTYTWO . endfm red !(( ((empty).AtomMagma -> P,Q(x:S)), (Q(x:S) -> P), (P -> Q(x:S)), (Q(f-x'(x:S)) -> Q(x:S)), (P,Q(f-x'(x:S)) -> (empty).AtomMagma) )) . q . --- Input: (ALL x. ((P) <=> (Q(x)))) => ((P) <=> (ALL x. (Q(x)))) --- Generalize: (ALL x. ((P) <=> (Q(x)))) => ((P) <=> (ALL x. (Q(x)))) --- After Negation: ~((ALL x. ((P) <=> (Q(x)))) => ((P) <=> (ALL x. (Q(x))))) --- After Prenex: ALL x. (EX x'. ((((P) /\ (Q(x))) \/ ((~(P)) /\ (~(Q(x))))) /\ (((P) /\ (~(Q(x')))) \/ ((~(P)) /\ (Q(x)))))) --- After Skolemization: (((P) /\ (Q(x))) \/ ((~(P)) /\ (~(Q(x))))) /\ (((P) /\ (~(Q(f_x'(x))))) \/ ((~(P)) /\ (Q(x)))) --- After simpcnf: [[P,Q(x)], [P,~(Q(x))], [Q(x),~(P)], [Q(x),~(Q(f_x'(x)))], [~(P),~(Q(f_x'(x)))]] --- Harrison resolution returned [true, true] taking 0.000444 --- Our Harrison resolution solved: true