load ../../rtp fmod P-THIRTEEN is pr PRED-BASE . sort S . op p : -> Atom [metadata "25"] . op q : -> Atom [metadata "26"] . op r : -> Atom [metadata "27"] . endfm fmod TEST is inc RTP . inc P-THIRTEEN . eq USER-MODULE-NAME = 'P-THIRTEEN . endfm red !(( ((empty).AtomMagma -> p,q), ((empty).AtomMagma -> p,r), (p -> (empty).AtomMagma), (q,r -> (empty).AtomMagma) )) . q . --- Input: ((p) \/ ((q) /\ (r))) <=> (((p) \/ (q)) /\ ((p) \/ (r))) --- Generalize: ((p) \/ ((q) /\ (r))) <=> (((p) \/ (q)) /\ ((p) \/ (r))) --- After Negation: ~(((p) \/ ((q) /\ (r))) <=> (((p) \/ (q)) /\ ((p) \/ (r)))) --- After Prenex: (((p) \/ ((q) /\ (r))) /\ (((~(p)) /\ (~(q))) \/ ((~(p)) /\ (~(r))))) \/ (((~(p)) /\ ((~(q)) \/ (~(r)))) /\ (((p) \/ (q)) /\ ((p) \/ (r)))) --- After Skolemization: (((p) \/ ((q) /\ (r))) /\ (((~(p)) /\ (~(q))) \/ ((~(p)) /\ (~(r))))) \/ (((~(p)) /\ ((~(q)) \/ (~(r)))) /\ (((p) \/ (q)) /\ ((p) \/ (r)))) --- After simpcnf: [[p,q], [p,r], [~(p)], [~(q),~(r)]] --- Harrison resolution returned [] taking 6.39999999996e-05 --- Our Harrison resolution solved: true