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