J024
(=> (forall ?X (exists ?Y (P ?X ?Y))) (exists ?Y (forall ?X (P ?X ?Y))))
Proof Trace