Proof of defining property of closedunder

----> UNIT CONFLICT at 595.27 sec ----> 8418 [binary,8414.1,8383.1] $F.

Length of proof is 16.  Level of proof is 6.

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.
10 [reference] p1 pair(x,y)=x.
14 [reference] abst x y z=x k(z) (y z).
16 [reference] x=y|eq pair(x,y) =p2.
18 [reference] p1!=p2.
20 [reference] x y=p1|isp1 x y =p2.
21 [reference] isp1 (isp1 x)=isp1 x.
23 [reference] x y=p1|notp1 x y =p1.
24 [reference] x y!=p1|notp1 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.
73 [para_into,42.1.2,23.1.2] bads badx=x y |notp1 x y =p1.
91 [para_from,42.1.2,18.1.1] bads badx!=p2.
93,92 [para_from,42.1.2,10.1.1.1] bads badx pair(x,y)=x.
102,101 [ur,43,20] isp1 bads (badf badx)=p2.
133 [para_into,91.1.1,42.1.1,flip.1] p2!=p1.
147 [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).
483 [para_into,101.1.1.1,21.1.2] isp1 (isp1 bads) (badf badx)=p2.
3327 [para_from,147.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.
6927 [para_into,73.2.1,24.2.1,unit_del,133] bads badx=x y |x y !=p1.
7433 [para_into,6927.1.2,92.1.1,demod,93] bads badx=x|x!=p1.
7501 [para_from,7433.1.1,91.1.1] x!=p2|x!=p1.
7778 [para_into,483.1.1.1.2,21.1.2] isp1 (isp1 (isp1 bads)) (badf badx)=p2.
8230,8229 [para_into,3327.1.1.2.1.1,42.1.1,demod,102,7,flip.1] p2=p1.
8383 [back_demod,7778,demod,8230] isp1 (isp1 (isp1 bads)) (badf badx)=p1.
8414 [back_demod,7501,demod,8230] x!=p1.
8418 [binary,8414.1,8383.1] $F.