Mj
Aab
Mabc
Pxyz
Pj
forall x (Hx --> Mx)
exists x (Hx & forall y (Fy -> Axy))
exists x (Hx & Ddxc)
forall z Mz