T2-320d
(=> (and (not (exists ?Y (forall ?X (<=> (F ?X) (= ?X ?Y))))) (not (exists ?X (exists ?Y (and (not (= ?X ?Y)) (F ?X) (F ?Y)))))) (exists ?X (F ?X)))
Proof Trace