Second proof of a(isp1,a(isp1,x)) = a(isp1,x).

----> UNIT CONFLICT at 178.00 sec ----> 6295 [binary,6294.1,8.1] $F.

Length of proof is 5.  Level of proof is 4.

Proof

8 [reference] x=x.
15 [reference] x=y|x noteq(x,y) !=y noteq(x,y).
17 [reference] x y!=p1|isp1 x y =p1.
18 [reference] x y=p1|isp1 x y =p2.
19 [assumption to refute] isp1 (isp1 bad)!=isp1 bad.
20 [ur,19,15] isp1 (isp1 bad) noteq(isp1 (isp1 bad),isp1 bad)!=isp1 bad noteq(isp1 (isp1 bad),isp1 bad).
74 [para_into,20.1.1,18.2.1,flip.1] isp1 bad noteq(isp1 (isp1 bad),isp1 bad)!=p2|isp1 bad noteq(isp1 (isp1 bad),isp1 bad) =p1.
76 [para_into,20.1.1,17.2.1,flip.1] isp1 bad noteq(isp1 (isp1 bad),isp1 bad)!=p1.
6168,6167 [para_into,74.1.1,18.2.1,unit_del,8,76] bad noteq(isp1 (isp1 bad),isp1 bad)=p1.
6294 [ur,76,17,demod,6168] p1!=p1.
6295 [binary,6294.1,8.1] $F.