remove_singleton pair(xset,k(x)) x = p2. ----> UNIT CONFLICT at 1.51 sec ----> 184 [binary,182.1,19.1] $F. Length of proof is 4. 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). 5 [reference] pair(p1 x,p2 x)=x. 6 [reference] abst x y z=x k(z) (y z). 7 [reference] eq pair(x,x)=p1. 19 [reference] p2!=p1. 21 [reference] p1 x=p2 x |eq x =p2. 53 [reference] pair(x1,y1)!=pair(x2,y2)|y1=y2. 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 [reference] xset x=p1|remove_singleton pair(xset,y) x =p2. 82 [assumption to refute] p. 83 [assumption to refute] -p|remove_singleton pair(badset,k(bad)) bad !=p2. 95,94 [hyper,83,82,81] badset bad=p1. 104 [ur,83,82,demod,79,6,1,4,1,4,2,6,1,4,3,1,6,1,4,1,4,95,6,1,4,1,4,5,7] eq pair(pair(p1,p2),pair(p1,p1))!=p2. 175 [hyper,104,21,demod,2,3] pair(p1,p2)=pair(p1,p1). 182 [hyper,175,53] p2=p1. 184 [binary,182.1,19.1] $F.
up | previous | next | detailed contents | brief contents | OTTER output file