T247
(=> (and (exists ?X (F ?X)) (exists ?X (G ?X))) (<=> (and (forall ?X (=> (F ?X) (H ?X))) (forall ?X (=> (G ?X) (J ?X)))) (forall ?X (forall ?Y (=> (and (F ?X) (G ?Y)) (and (H ?X) (J ?Y)))))))
Proof Trace