T2-325
(<=> (exists ?X (exists ?Y (forall ?Z (or (= ?Z ?X) (= ?Z ?Y))))) (or (exists ?X (forall ?Y (= ?Y ?X))) (exists ?X (exists ?Y (and (not (= ?X ?Y)) (forall ?Z (or (= ?Z ?X) (= ?Z ?Y))))))))
Proof Trace