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