T261
(<=> (forall ?X (=> (F ?X) (exists ?Y (and (G ?Y) (or (H ?Y) (H ?X)))))) (or (exists ?X (and (G ?X) (H ?X))) (not (exists ?X (F ?X))) (and (exists ?X (G ?X)) (forall ?X (=> (F ?X) (H ?X))))))
Proof Trace