J009
(exists ?X (forall ?Y (P ?X ?Y)))
Proof Trace