J022
(=> (and (forall ?X (exists ?Y (not (P ?X ?Y)))) (forall ?X (P ?X ?X))) (forall ?X (not (P ?X ?X))))
Proof Trace