subset ----> UNIT CONFLICT at 39.84 sec ----> 2933 [binary,2931.1,19.1] $F. Length of proof is 5. Level of proof is 4.
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). 19 [reference] p2!=p1. 21 [reference] p1 x=p2 x |eq x =p2. 23 [reference] x y=p1|isp1 x y =p2. 57 [reference] subset=abst k(eq) pair(k(k(p2)),abst k(abst k(eq)) pair(k(k(pair(p1,p2))),pair(p1,abst k(isp1) p2))). 58 [assumption to refute] p. 59 [assumption to refute] -p|subset pair(bad1,bad2) !=p2. 60 [assumption to refute] bad1 badc=p1. 61 [assumption to refute] bad2 badc!=p1. 62 [ur,59,58,demod,57,6,1,4,1,6,1,4,1,4,2,6,1,3] eq pair(k(p2),abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)))!=p2. 149,148 [ur,61,23] isp1 bad2 badc=p2. 185 [ur,62,21,demod,2,3,flip.1] abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2))=k(p2). 896 [para_from,185.1.1,14.1.1.1,demod,1,1,4,1,4,flip.1] eq pair(pair(p1,p2),pair(bad1 x,isp1 bad2 x))=p2. 2931 [para_into,896.1.1.2.2.1,60.1.1,demod,149,7,flip.1] p2=p1. 2933 [binary,2931.1,19.1] $F.
up | previous | next | detailed contents | brief contents | OTTER output file