T323
(exists ?Y (forall ?X (<=> (forall ?Z (<=> (= ?X ?Z) (= ?Z ?Y))) (= ?X ?Y))))
Proof Trace