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