If the quantifiers are not showing correctly a PDF version is available here.

1. DERIVE: ~x(~Fx v Gx )

1.	x ( ~Fx v ~Gx )	PR
2.	Fa	PR
3.	| x( ~Fx v Gx )	AS
4.	| ~Fa v Ga	3 E
5.	| ~Fa v ~Ga	1 E
6.	| ~~Fa	2DN
7.	| Ga	4, 6 vE
8.	| ~Ga	5, 6 vE
9.	~x(~Fx v Gx )	3-8 ~I

2. DERIVE: xGx

1	x( Fx Gx )	PR
2.	Fm v Fn	PR
3.	| ~xGx	AS
4.	|x~Gx	3 QN
5.	| Fm Gm	1 E
6.	| ~Gm	4 E
7.	| ~Fm	5,6 MT
8.	| Fn	2, 7 vE
9.	| Fn Gn	1 E
10.	| Gn	8,9 E
11.	| ~Gn	4 E
12.	xGx	3-11 ~E

3. DERIVE: x( Fx & ~Gx )

1.	x( Gx y~Kxy )	PR
2.	x( Fx &yKxy )	PR
3.	Fa &yKay	2 E
4.	Ga y~Kay	1E
5.	yKay	3 &E
6.	~~yKay	5 DN
7.	~y~Kay	6 QN
8.	~Ga	4, 7 MT
9.	Fa	3 &E
10.	Fa & ~Ga	8, 9 &I
11.	x( Fx & ~Gx )	10 I

4. DERIVE: x( ~Fx & ~Hx ) xGx

1.	x[( Fx Hx ) Gx ]	PR
2.	| x( ~Fx & ~Hx )	AS
3.	| ~Fx & ~Hx	2 E
4.	| ( Fx & Hx ) v ( ~Fx & ~Hx )	3 vI
5.	| Fx Hx	4 EQUIV
6.	| ( Fx Hx ) G x	1 E
7.	| Gx	5,6 E
8.	|x Gx	7 I
9.	x( ~Fx & ~Hx )xGx	2-8 I

5. DERIVE: Cmn

1.	x( Ax y( By Cxy ))	PR
2.	Am & Bn	PR
3.	Am y( By Cmy )	1 E
4.	Am	2 &E
5.	y( By Cmy )	3, 4 E
6.	Bn Cmn	5 E
7.	Bn	2 &E
8.	Cmn	6, 7 E

6. DERIVE:y( Cy & Ay )

1.	y( My Ay )	PR
2.	y( Cy & My )	PR
3.	Ca & Ma	2 E
4.	Ca	3 &E
5.	Ma	3 &E
6.	Ma Aa	1 E
7.	Aa	5, 6 E
8.	Ca & Aa	4, 7 &I
9.	y( Cy & Ay )	8 I

7. DERIVE:xAx

1.	x( Ax v Bx )	PR
2.	x( Bx Ax )	PR
3.	| ~xAx	AS
4.	|x~Ax	3 QN
5.	| ~Aa	4 E
6.	| Aa v Ba	1 E
7.	| Ba	5, 6 vE
8.	| Ba Aa	2 E
9.	| Aa	7, 8 E
10.	xAx	3-9 ~E

8. DERIVE:xy[( Fx Fy ) ( Fy v ~Fx )]

1.	| Fx Fy	AS
2.	| ~Fx v Fy	1 IMP
3.	| Fy v ~Fx	2 COM
4.	( Fx Fy ) ( Fy v ~Fx )	1-3 I
5.	| Fy v ~Fx	AS
6.	| ~Fx v Fy	5 COM
7.	| Fx Fy	6 IMP
8.	( Fy v ~Fx ) ( Fx Fy )	5-7 I
9.	( Fx Fy ) ( Fy v ~Fx )	5, 8 I
10.	y[( Fx Fy ) ( Fy v ~Fx )]	9 I
11.	xy[( Fx Fy ) ( Fy v ~Fx )]	10 I

9. DERIVE:z ~Jz

1.	y( Jy ( Ky & Ly ))	PR
2.	x~Kx	PR
3.	~Ka	2 E
4.	~Ka v ~La	3 vI
5.	~( Ka & La )	4 DeM
6.	Ja ( Ka & La )	1 E
7.	~Ja	5, 6 MT
8.	z ~Jz	7 I

10. DERIVE: x( Fx Ax )

1.	xFx x( Bx & Cx )	PR
2.	x( Cx v Dx ) xAx	PR
3.	| Fx	AS
4.	|xFx	3 I
5.	|x( Bx & Cx )	1, 4 E
6.	| Ba & Ca	5 E
7.	| Ca	6 &E
8.	| Ca v Da	7 vI
9.	|x( Cx v Dx )	8 I
10.	|xAx	2, 9 E
11.	| Ax	10 E
12.	Fx Ax	4-10 I
13.	x( Fx Ax )	12 I

11. DERIVE:x ~Fx

1.	xFx xGx	PR
2.	x~Gx	PR
3.	~xGx	2 QN
4.	~xFx	1, 3 MT
5.	x~Fx	4 QN

12. DERIVE: ~xAx

1.	x( Ax & ~Bx ) xCx	PR
2.	~x( Cx v Bx )	PR
3.	x~( Cx v Bx )	2 QN
4.	| xAx	AS
5.	| Ax	4 E
6.	| ~( Cx v Bx )	3 E
7.	| ~Cx & ~Bx	6 DeM
8.	| ~Bx	7 &E
9.	| Ax & ~Bx	5, 8 &I
10.	|x( Ax & ~Bx )	9 I
11.	|xCx	1, 10 E
12.	| ~Cx	7 &E
13.	|x~Cx	12 I
14.	| ~xCx	13 QN
15.	~xAx	4-14 ~I

13. DERIVE:xyRxy

1.	xyRxy	PR
2.	xy( Rxy zRxz )	PR
3.	x( zRxz yRyx )	PR
4.	yRay	1 E
5.	Rab	4 E
6.	y( Ray zRaz )	2 E
7.	Rab zRaz	6 E
8.	zRaz	5, 7 E
9.	zRaz yRya	3 E
10.	yRya	8,9 E
11.	Rxa	10 E
12.	"y( Rxy "zRxz )	2 E
13.	Rxa zRxz	12 E
14.	zRxz	11, 13 E
15.	Rxy	14 E
16.	yRxy	15 I
17.	xyRxy	16 I

14. DERIVE: xAx xCx

1.	xAx x( Bx & Cx )	PR
2.	x( Cx Bx )	PR
3.	| xAx	AS
4.	|x( Bx & Cx )	1, 3 E
5.	| Ba & Ca	4 E
6.	| Ca	5 &E
7.	|xCx	6 I
8.	xAx xCx	3-7 I
9.	| xCx	AS
10.	| Cb	9 E
11.	| Cb Bb	2 E
12.	| Bb	10, 11 E
13.	| Bb & Cb	10, 12 &I
14.	|x( Bx & Cx )	13 I
15.	|xAx	1, 14 E
16.	xCx xAx	9-15 I
17.	xAx xCx	8, 16 I

15. DERIVE: ~xAx

1.	x~Ax vx~Bx	PR
2.	xBx	PR
3.	~~xBx	2 DN
4.	~x~Bx	3 QN
5.	x~Ax	1, 4 vE
6.	~xAx	5 QN

16. DERIVE:x( Ax &y~Bxy ) ~x[ ~Ax vy( Bxy & Bxy )]

1.	| x( Ax & y~Bxy )	AS
2.	|x( ~~Ax &y~Bxy )	1 DN
3.	|x( ~~Ax & ~yBxy )	2 QN
4.	|x~( ~Ax vyBxy )	3 DeM
5.	| ~x( ~Ax vyBxy )	4 QN
6.	| ~vx[ ~Ax vy(Bxy & Bxy )]	5 IDEM
7.	x( Ax &y~Bxy ) ~x[ ~Ax vy( Bxy & Bxy )]	1-5 I
8.	| ~x[ ~Ax v y(Bxy & Bxy )]	AS
9.	| ~x( ~Ax vyBxy )	8 IDEM
10.	|x~( ~Ax vyBxy )	9 QN
11.	|x( ~~Ax & ~yBxy )	10 DeM
12.	|x( ~~Ax &y~Bxy )	11 QN
13.	|x( Ax &y~Bxy )	12 DN
14.	~x[ ~Ax vy( Bxy & Bxy )] x( Ax &y~Bxy )	8-13 I
15.	x( Ax &y~Bxy ) ~x[ ~Ax vy( Bxy & Bxy )]	7, 14 I

17. DERIVE: ~xBx

1.	~x( Ax Cx )	PR
2.	x[( Ax & Bx ) Cx ]	PR
3.	x~( Ax Cx )	1 QN
4.	~( Aa Ca )	3 E
5.	~( ~Aa v Ca )	4 IMP
6.	~~Aa & ~Ca	5 DeM
7.	( Aa & Ba ) Ca	2 E
8.	Aa ( Ba Ca )	7 EXP
9.	~~Aa	6 &E
10.	Aa	9 DN
11.	Ba Ca	8, 10 E
12.	~Ca	6 &E
13.	~Ba	11, 12 MT
14.	x~Bx	13 I
15.	~xBx	14 QN

18. DERIVE:xy~Axy

1.	xyAxy xyBxy	PR
2.	xy~Bxy	PR
3.	x~yBxy	2 QN
4.	~xyBxy	3 QN
5.	~xyAxy	1, 4 MT
6.	x~yAxy	5 QN
7.	xy~Axy	6 QN

19. DERIVE:x( Bx y( Ay & Cyx ))

1.	x( Ax &y( By Cxy ))	PR
2.	Aa &y( By Cay )	1E
3.	Aa	2 &E
4.	y( By Cay )	2 &E
5.	| Bx	AS
6.	| Bx Cax	4 E
7.	| Cax	5, 6 E
8.	| Aa & Cax	3, 7 &I
9.	|y( Ay & Cyx )	8 I
10.	Bx y( Ay & Cyx )	5-10 I
11.	x( Bx y( Ay & Cyx ))	10 I

20. DERIVE:xCxj

1.	x[ Ax &y( By Cxy ))	PR
2.	xAx Bj	PR
3.	Aa &y( By Cay )	1 E
4.	Aa	3 &E
5.	y( By Cay )	3 &E
6.	Bj Caj	5 E
7.	xAx	4 I
8.	Bj	2, 7 E
9.	Caj	6, 8 E
10.	xCxj	9 I

21. DERIVE: z( ~Wz & Hz )

1.	x(xRxy z ~Wz )	PR
2.	yz( Ryz & Hz )	PR
3.	x( ~Hx Wx )	PR
4.	z( Raz & Hz )	2 E
5.	Rab & Hb	4 E
6.	Rab	5 &E
7.	yRay	6 I
8.	yRay z~Wz	1E
9.	z~Wz	7, 8 E
10.	~Wc	9 E
11.	~Hc Wc	3E
12.	~~Hc	10, 11 MT
13.	Hc	11 DN
14.	~Wc & Hc	10, 13 &I
15.	z( ~Wz & Hz )	14 I

22. DERIVE: [xAx (yBy zCz )] xyz[( Ax & By ) Cz ]

1.	|xAx ( yBy zCz )]	AS
2.	| | Ax & By	AS
3.	| | Ax	2 &E
4.	| |xAx	3 I
5.	| |yBy zCz	1, 4 E
6.	| | By	2 &E
7.	| |yBy	6 I
8.	| |zCz	5, 7 E
9.	| | Cz	8 E
10.	|( Ax & By ) Cz	2-9 I
11.	z[( Ax & By ) Cz ]	10 I
12.	|yz[( Ax & By ) Cz ]	11 I
13.	|xyz[( Ax & By ) Cz ]	12 I
14.	[xAx (yBy "zCz )] "x"y"z[( Ax & By ) Cz ]	1-13 I

23. DERIVE:w( Qw & Bw ) y( Lyy ~Ay )

1.	zQz w( Lww ~Hw )	PR
2.	xBx y( Ay Hy )	PR
3.	| w( Qw & Bw )	AS
4.	| Qa & Ba	3 E
5.	| Qa	4 &E
6.	|zQz	5 I
7.	|w( Lww ~Hw )	1, 6 E
8.	| Ba	4 &E
9.	|xBx	8 I
10.	|y( Ay Hy )	2, 9 E
11.	| Lyy ~Hy	7 E
12.	| Ay Hy	10 E
13.	| ~Hy ~Ay	12 TRANS
14.	| Lyy ~Ay	11, 13 HS
15.	|y( Lyy ~Ay )	14 I
16.	w( Qw & Bw ) y( Lyy ~Ay )	3-15 I

24. DERIVE:zw[( Az & Hw ) Czw ]

1.	xy[( Ax & By ) Cxy ]	PR
2.	y[ Ey &w( Hw Cyw )]	PR
3.	xyz[( Cxy & Cyz ) Cxz ]	PR
4.	w( Ew Bw )	PR
5.	| Ax & Hw	AS
6.	| Ax	5 &E
7.	| Hw	5 &E
8.	| Ea &w( Hw Caw )	2 E
9.	|w( Hw Caw )	8 &E
10.	| Hw Caw	9 E
11.	| Ea	8 &E
12.	| Ea Ba	4 E
13.	| Ba	11, 12 E
14.	|y[( Ax & By ) Cxy ]	1 E
15.	| ( Ax & Ba ) Cxa	14 "E
16.	| Ax & Ba	6, 13 &I
17.	| Cxa	15, 16 E
18.	| Caw	7, 10 E
19.	| Cxa & Caw	17, 18 &I
20.	|yz[( Cxy & Cyz ) Cxz ]	3 E
21.	|z[( Cxa & Caz ) Cxz ]	20 E
22.	| ( Cxy & Cyw ) Cxw	21 E
23.	| Cxw	19, 22 E
24.	( Ax & Hw ) Cxw	5-23 I
25.	w[( Ax & Hw ) Cxw ]	24 I
26..	zw[( Az & Hw ) Czw ]	25 I