U002a
Premises:
(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)))))
Conclusion:
(exists ?X (forall ?Y (P ?X ?Y)))
Proof Trace