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