Purified Form Prenex Form Mixed Form
1 ($x)Dx ($y)(Py By) ("x)($y)[Dx (Py By)] ("x)[Dx ($y)(Py By)]
2 ("x)(Dx Cx) ("x)(Dx Cx)  
3 ("x)~Dx ("y)(Py ~By) ($x)("y)[~Dx (Py ~By)] ~($x)Dx ("y)(Py ~By)
4 ∃x(Dx.Cx) → ∃y(Py.By) ("x)($y)[[Dx (Py ~By)] ~Cx] ("x)[[Dx ("y)(Py ~By)] ~Cx]
5 ("x)[(Bx Yx) Rx] ("x)[(Bx Yx) Rx]  
6 ($x)(Bx Yx) ($y)(By Ry) ("x)("y)[(Bx Yx) (By Ry)]  
7  

("x)($y)[(Bx Yx) [(By Yy) Ry] Rx]

("x)[(Bx Yx) [("y)[(By Yy) Ry] Rx]]
8 ("x)[(Bx Rx) Yx] ($y)(Yy Ry) ($x)($y){[(Bx Rx) Yx] (Yy Ry)}  
9 ("x)[(Ox Px) (Cx v Mx)] [($y)(Cy Py) v ($z)(Mz Pz)]    
10   ("x)("y)[(Ox Px) [(My ~Py) v Mx]] ("x)[(Ox Px) [("y)(My ~Py) v Mx]]
11 ($x)(Ox Px) [("y)((Oy Py) Cy) ($z)(Cz Pz)]    
12     ("x)[(Ox Px) [("y)[(Oy Py) Cy] Cx]]
13 ("x)[(Sx Fx) (Sx Wx)] [($y)(Sy) ($z)(Wz Fz)]    
14     ("x)[(Sx Wx) [("y)(Wy Fy) Fx]]
15     ("x)[[(Sx) ("y)(Sy Wy)] Wx]
16     [("x)(Px Fx) (y")(Ey ~Ly)] ($z)(Ez Sz)
17   ("x)("y)[(Ex Lx) [(Py ~Fy) ~Sx]] ("x)[(Ex Lx) [($y)(Py ~Fy) ~Sx]]
18 [($x)(Ex Lx) ($y)(Py ~Fy)] ($z)(Ez ~Sz)    
19 ($x)(Hx ~Sx) [("y)(Wy Ay) ($z)(Wz Dz)]    
20 ("x)[(Hx ~Sx) [($y)(Wy Ay) Ux]]