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

----> UNIT CONFLICT at   0.06 sec ----> 47 [binary,46.1,8.1] $F.

Length of proof is 4.  Level of proof is 3.

Proof

8 [reference] x=x.
18 [reference] p1!=p2.
23 [reference] x y=p1|notp1 x y =p1.
24 [reference] x y!=p1|notp1 x y =p2.
25 [assumption to refute] notp1 bad=bad.
32 [para_from,25.1.1,24.2.1.1] bad x!=p1|bad x =p2.
34,33 [para_from,25.1.1,23.2.1.1] bad x=p1.
41,40 [back_demod,32,demod,34,34,unit_del,8,flip.1] p2=p1.
46 [back_demod,18,demod,41] p1!=p1.
47 [binary,46.1,8.1] $F.