Proof of a(notp1,a(notp1,x)) = a(isp1,x).

-----> EMPTY CLAUSE at  77.70 sec ----> 5386 [back_demod,2319,demod,4557,4563,unit_del,94,94] $F.

Length of proof is 15.  Level of proof is 5.

Proof

8 [reference] x=x.
16 [reference] x=y|eq pair(x,y) =p2.
17 [reference] x=y|x noteq(x,y) !=y noteq(x,y).
18 [reference] p1!=p2.
19 [reference] x y!=p1|isp1 x y =p1.
20 [reference] x y=p1|isp1 x y =p2.
23 [reference] x y=p1|notp1 x y =p1.
24 [reference] x y!=p1|notp1 x y =p2.
26 [reference] notp1 x y=p1|notp1 x y =p2.
27 [assumption to refute] notp1 (notp1 bad)!=isp1 bad.
28 [ur,27,17] notp1 (notp1 bad) noteq(notp1 (notp1 bad),isp1 bad)!=isp1 bad noteq(notp1 (notp1 bad),isp1 bad).
30,29 [ur,27,16] eq pair(notp1 (notp1 bad),isp1 bad)=p2.
64 [para_into,28.1.1,26.2.1,flip.1] isp1 bad noteq(notp1 (notp1 bad),isp1 bad)!=p2|notp1 (notp1 bad) noteq(notp1 (notp1 bad),isp1 bad) =p1.
65 [para_into,28.1.1,26.1.1,flip.1] isp1 bad noteq(notp1 (notp1 bad),isp1 bad)!=p1|notp1 (notp1 bad) noteq(notp1 (notp1 bad),isp1 bad) =p2.
66 [para_into,28.1.1,24.2.1,flip.1] isp1 bad noteq(notp1 (notp1 bad),isp1 bad)!=p2|notp1 bad noteq(notp1 (notp1 bad),isp1 bad) !=p1.
83 [para_into,28.1.2,19.2.1] notp1 (notp1 bad) noteq(notp1 (notp1 bad),isp1 bad)!=p1|bad noteq(notp1 (notp1 bad),isp1 bad) !=p1.
94 [para_from,29.1.2,18.1.2,demod,30,flip.1] p2!=p1.
628 [para_into,64.1.1,20.2.1,unit_del,8] notp1 (notp1 bad) noteq(notp1 (notp1 bad),isp1 bad)=p1|bad noteq(notp1 (notp1 bad),isp1 bad) =p1.
752 [para_into,65.1.1,19.2.1,unit_del,8] notp1 (notp1 bad) noteq(notp1 (notp1 bad),isp1 bad)=p2|bad noteq(notp1 (notp1 bad),isp1 bad) !=p1.
867 [para_into,83.1.1,23.2.1,unit_del,8] bad noteq(notp1 (notp1 bad),isp1 bad)!=p1|notp1 bad noteq(notp1 (notp1 bad),isp1 bad) =p1.
2319 [para_from,628.2.1,24.1.1,unit_del,8] notp1 bad noteq(notp1 (notp1 bad),isp1 bad)=p2|notp1 (notp1 bad) noteq(notp1 (notp1 bad),isp1 bad) =p1.
4375 [para_into,66.2.1,23.2.1,unit_del,8] isp1 bad noteq(notp1 (notp1 bad),isp1 bad)!=p2|bad noteq(notp1 (notp1 bad),isp1 bad) =p1.
4432,4431 [para_into,4375.1.1,20.2.1,unit_del,8] bad noteq(notp1 (notp1 bad),isp1 bad)=p1.
4557,4556 [back_demod,867,demod,4432,unit_del,8] notp1 bad noteq(notp1 (notp1 bad),isp1 bad)=p1.
4563,4562 [back_demod,752,demod,4432,unit_del,8] notp1 (notp1 bad) noteq(notp1 (notp1 bad),isp1 bad)=p2.
5386 [back_demod,2319,demod,4557,4563,unit_del,94,94] $F.