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