----> UNIT CONFLICT at 2.77 sec ----> 411 [binary,409.1,149.1] $F. Length of proof is 7. Level of proof is 5.
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.
up | previous | next | detailed contents | brief contents | OTTER output file