Manual Proof

----> UNIT CONFLICT at   2.77 sec ----> 411 [binary,409.1,149.1] $F.

Length of proof is 7.  Level of proof is 5.

Proof

1 [reference] k(x) y=x.
2 [reference] p1 pair(x,y)=x.
3 [reference] p2 pair(x,y)=y.
4 [reference] pair(x,y) z=pair(x z,y z).
6 [reference] abst x y z=x k(z) (y z).
7 [reference] eq pair(x,x)=p1.
14 [reference] abst x y z=x k(z) (y z).
15 [reference] x!=y|eq pair(x,y) =p1.
16 [reference] x=y|eq pair(x,y) =p2.
20 [reference] x y=p1|isp1 x y =p2.
39 [reference] closedunder=abst k(eq) pair(k(k(p2)),abst k(abst k(eq)) pair(pair(p1,abst (abst k(abst) (abst k(abst k(isp1)) (abst k(p1)))) p2),k(k(pair(p1,p2))))).
40 [assumption to refute] p.
41 [assumption to refute] -p|closedunder pair(bads,badf) !=p2.
42 [assumption to refute] bads badx=p1.
43 [assumption to refute] bads (badf badx)!=p1.
44 [ur,41,40,demod,39,6,1,4,1,6,1,4,4,2,6,6,1,6,1,3,1] eq pair(k(p2),abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(
pair(bads,badf)))) badf),k(pair(p1,p2))))!=p2.
61 [ur,44,16,flip.1] abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2)))=k(p2).
149 [para_into,44.1.1,15.2.1,unit_del,61,flip.1] p2!=p1.
236 [para_from,61.1.1,14.1.1.1,demod,1,1,4,4,6,6,1,6,1,1,2,1,flip.1] eq pair(pair(bads x,isp1 bads (badf x)),pair(p1,p2))=p2.
371 [para_from,42.1.1,236.1.1.2.1.1] eq pair(pair(p1,isp1 bads (badf badx)),pair(p1,p2))=p2.
405,404 [ur,43,20] isp1 bads (badf badx)=p2.
409 [back_demod,371,demod,405,7,flip.1] p2=p1.
411 [binary,409.1,149.1] $F.