1.	* show  ¬(˛y)(Åx)(P(x,y)ﬂ¬P(x,x))
2.	(˛y)(Åx)(P(x,y)ﬂ¬P(x,x))	ASSUME
3.	(Åx)(P(x,z9)ﬂ¬P(x,x))		2, EI
4.	(P(z9,z9)ﬂ¬P(z9,z9))		3, UI
5.	(P(z9,z9)∞¬P(z9,z9))		4, BC
6.	(¬P(z9,z9)∞P(z9,z9))		4, BC
7.	* show P(z9,z9)
8.	¬P(z9,z9)				ASSUME
9.	P(z9,z9)				8,6, MP
10.	¬P(z9,z9)					5,7, MP

CPU time: 73 msec
Lines deleted: 0

1.	* show ((˛y)(Åx)(F(x,y)ﬂF(x,x))∞¬(Åx)(˛y)(Åz)(F(z,y)ﬂ¬F(z,x)))
2.	(˛y)(Åx)(F(x,y)ﬂF(x,x))		ASSUME
3.	* show ¬(Åx)(˛y)(Åz)(F(z,y)ﬂ¬F(z,x))
4.	(Åx)(˛y)(Åz)(F(z,y)ﬂ¬F(z,x))	ASSUME
5.	(Åx)(F(x,z9)ﬂF(x,x))	2, EI
6.	(˛y)(Åz)(F(z,y)ﬂ¬F(z,z9))	4, UI
7.	(Åz)(F(z,z8)ﬂ¬F(z,z9))	6, EI
8.	(F(z8,z9)ﬂF(z8,z8))		2, EI
9.	(F(z8,z8)ﬂ¬F(z8,z9))	7, UI
10.	(F(z8,z9)∞F(z8,z8))		8, BC
11.	(F(z8,z8)∞F(z8,z9))		8, BC
12.	(F(z8,z8)∞¬F(z8,z9))	9, BC
13.	(¬F(z8,z9)∞F(z8,z8))	9, BC
14.	* show F(z8,z9)
15.	¬F(z8,z9)			ASSUME
16.	F(z8,z8)			13,15, MP
17.	F(z8,z9)			16,11, MP
18.	F(z8,z8)				10,14, MP
19.	¬F(z8,z9)				12,18, MP

CPU time: 467 msec
Lines deleted: 45

1.	* show  ((Åz)(˛y)(Åx)(F(x,y)ﬂ(F(x,z)&¬F(x,x)))∞¬(˛z)(Åx)F(x,z))
2.	(Åz)(˛y)(Åx)(F(x,y)ﬂ(F(x,z)&¬F(x,x)))	ASSUME
3.	* show ¬(˛z)(Åx)F(x,z)
4.	(˛z)(Åx)F(x,z)			ASSUME
5.	(Åx)F(x,z9)			4, EI
6.	(˛y)(Åx)(F(x,y)ﬂ(F(x,z9)&¬F(x,x)))	2, UI
7.	F(z9,z9)				5, UI
8.	(Åx)(F(x,z8)ﬂ(F(x,z9)&¬F(x,x)))	6, EI
9.	(F(z9,z8)ﬂ(F(z9,z9)&¬F(z9,z9)))	8, UI
10.	(F(z9,z8)∞(F(z9,z9)&¬F(z9,z9)))	9, BC
11.	((F(z9,z9)&¬F(z9,z9))∞F(z9,z8))	9, BC
12.	* show F(z9,z8)
13.	¬F(z9,z8)			ASSUME
14.	¬(F(z9,z9)&¬F(z9,z9))	13, 11, MT
15.	F(z9,z9)		7, R
16.	* show ¬F(z9,z9)
17.	F(z8,z9)	5, UI
18.	(F(z8,z8)ﬂ(F(z8,z9)&¬F(z8,z8)))	8, UI
19.	(F(z8,z8)∞(F(z8,z9)&¬F(z8,z8)))	18, BC
20.	((F(z8,z9)&¬F(z8,z8))∞F(z8,z8))	18, BC
21.	* show F(z8,z8)
22.	¬F(z8,z8)	ASSUME
23.	¬(F(z8,z9)&¬F(z8,z8))	22, 20, MT
24.	(F(z8,z9)&¬F(z8,z8))	17, 22, ADJ
25.	(F(z8,z9)&¬F(z8,z8))	19, 21, MP
26.	¬F(z8,z8)		25, S
27.	(F(z9,z9)&¬F(z9,z9))	15, 16, ADJ
28.	(F(z9,z9)&¬F(z9,z9))	10, 12, MP
29.	¬F(z9,z9)				28, S

CPU time: 204 msec
Lines Deleted: 6

1.	* show ¬(˛y)(Åx)(F(x,y)ﬂ¬(˛z)(F(x,z)&F(z,x)))
2.	(˛y)(Åx)(F(x,y)ﬂ¬(˛z)(F(x,z)&F(z,x)))	ASSUME
3.	(Åx)(F(x,z9)ﬂ¬(˛z)(F(x,z)&F(z,x)))	2, EI
4.	(F(z9,z9)ﬂ¬(˛z)(F(z9,z)&F(z,z9)))	3, UI
5.	(F(z9,z9)∞¬(˛z)(F(z9,z)&F(z,z9)))	4, BC
6.	(¬(˛z)(F(z9,z)&F(z,z9))∞F(z9,z9))	4, BC
7.	* show F(z9,z9)
8.	¬F(z9,z9)				ASSUME
9.	¬¬(˛z)(F(z9,z)&F(z,z9))	6, 8, MT
10.	(˛z)(F(z9,z)&F(z,z9))	9, DN
11.	(F(z9,z8)&F(z8,z9))		10, EI
12.	F(z9,z8)				11, S
13.	F(z8,z9)				11, S
14.	* show ¬(˛z)(F(z9,z)&F(z,z9))
15.	(F(z8,z9)ﬂ¬(˛z)(F(z8,z)&F(z,z8)))	3, UI
16.	(F(z8,z9)∞¬(˛z)(F(z8,z)&F(z,z8)))	15, BC
17.	¬(˛z)(F(z8,z)&F(z,z8))	16, 13, MP
18.	(Åz)¬(F(z8,z)&F(z,z8))	17, QN
19.	¬(F(z8,z9)&F(z9,z8))	18, UI
20.	(F(z8,z9)&F(z9,z8))	13, 12, ADJ
21.	¬(˛z)(F(z9,z)&F(z,z9))		5, 7, MP
22.	(Åz)¬(F(z9,z)&F(z,z9))		21, QN
23.	¬(F(z9,z9)&F(z9,z9))		22, UI
24.	(F(z9,z9)&F(z9,z9))			7, 7, ADJ

CPU time: 191 msec
Lines Discarded: 2