T319
(<=> (and (exists ?X (exists ?Y (and (f ?X) (f ?Y) (not (= ?X ?Y))))) (forall ?X (forall ?Y (forall ?Z (=> (and (f ?X) (f ?Y) (f ?Z)) (or (= ?X ?Y) (= ?X ?Z) (= ?Y ?Z))))))) (exists ?X (exists ?Y (and (f ?X) (f ?Y) (not (= ?X ?Y)) (forall ?Z (=> (f ?Z) (or (= ?X ?Z) (= ?Y ?Z))))))))
Proof Trace