Prenex Form

1.    (x)(y)[Dx .Py By]

2.    (x)(y)[~Dx .Py ~By]

3.    (x)(y)[Dx Py ~By. ~Cx]

4.     (x)(y)[Bx Yx. .By Ry]

5.    (x)(y){Bx Rx. Yx : .Yy Ry}

6.    (x)(y)[Sx Wx. :Wy Fy. Fx]

7.    (x)(y)[Ex Lx. :Py ~Fy. ~Sx]

8.     (x)(y)(z)[Ex Lx Py ~Fy. .Ez ~Sz]

9.    (x)(y)[Ex Lx. :Py ~Fy. ~Sx]

10.    (∀x)(y)[Hx ~Sx. :Wy Ay. Ux]

11.    (∀x)(y)[Mx Dx .  . Ty ~Lxy]

12.     (∀x)(y)[Mx Dx .  . Ty ~Lxy]

13.    (x)(y)[~Ax Lx Ay Dy: Mxy]

14.    (x)(w)(z)(u)[[Bx Txw Lw: :Txy ~Buz]  Note, the existentially boutnd 'y' in the antecedent became a 'w' so as not to capture the free 'y' in the consequent when expanding the scope of the exisnteial 'y'.

15.    (x)(y)(z)(u)[Px Dy Hxy Pz Vzx Byz. .Nu Mxu]