T270
(<=> (exists ?Y (forall ?X (and (F1 ?X) (G1 ?Y)))) (forall ?X (exists ?Y (and (F1 ?X) (G1 ?Y)))))
Proof Trace