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