T260
(<=> (exists ?X (forall ?Y (<=> (F ?X) (F ?Y)))) (or (not (exists ?X (F ?X))) (forall ?X (F ?X))))
Proof Trace