remove_singleton pair(xset, y) is a subset of xset ----> UNIT CONFLICT at 0.63 sec ----> 138 [binary,136.1,81.1] $F. Length of proof is 3. Level of proof is 3.
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). 5 [reference] pair(p1 x,p2 x)=x. 6 [reference] abst x y z=x k(z) (y z). 21 [reference] p1 x=p2 x |eq x =p2. 52 [reference] pair(x1,y1)!=pair(x2,y2)|x1=x2. 79 [reference] remove_singleton=abst k(abst k(eq)) pair(k(k(pair(p1,p2))),pair(p1,abst k(abst k(eq)) pair(p2,k(pair(p1,p2))))). 81 [assumption to refute] badset bad!=p1. 82 [assumption to refute] p. 83 [assumption to refute] -p|remove_singleton pair(badset,bad1) bad !=p2. 102 [ur,83,82,demod,79,6,1,4,1,4,2,6,1,4,3,1,6,1,4,1,4,6,1,4,4,5] eq pair(pair(p1,p2),pair(badset bad,eq pair(bad1 bad,bad)))!=p 2. 112 [hyper,102,21,demod,2,3,flip.1] pair(badset bad,eq pair(bad1 bad,bad))=pair(p1,p2). 136 [hyper,112,52] badset bad=p1. 138 [binary,136.1,81.1] $F.
up | previous | next | detailed contents | brief contents | OTTER output file