Proof of a(charq,xf) = p2 | a(xf,x) = p1 | a(xf,x) = p2.

----> UNIT CONFLICT at   0.12 sec ----> 79 [binary,77.1,34.1] $F.

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

Proof

1 [reference] k(x) y=x.
4 [reference] pair(x,y) z=pair(x z,y z).
5 [reference] pair(p1 x,p2 x)=x.
6 [reference] abst x y z=x k(z) (y z).
16 [reference] x=y|eq pair(x,y) =p2.
20 [reference] x y=p1|isp1 x y =p2.
30 [reference] charq=abst k(eq) pair(pair(p1,p2),isp1).
31 [assumption to refute] -p.
32 [assumption to refute] p|charq badf !=p2.
33 [assumption to refute] badf badx!=p1.
34 [assumption to refute] badf badx!=p2.
35 [ur,32,31,demod,30,6,1,4,4,5] eq pair(badf,isp1 badf)!=p2.
44 [ur,33,20] isp1 badf badx=p2.
73,72 [ur,35,16,flip.1] isp1 badf=badf.
77 [back_demod,44,demod,73] badf badx=p2.
79 [binary,77.1,34.1] $F.