U002
(=> (and (forall ?X (forall ?Y (or (P ?X ?Y) (P ?Y ?X)))) (forall ?X (forall ?Y (forall ?Z (=> (and (P ?X ?Y) (P ?Y ?Z)) (P ?X ?Z)))))) (exists ?X (forall ?Y (P ?X ?Y))))
Proof Trace