Proof that if x is a member of S then S is not a subset of S - {x}.

----> UNIT CONFLICT at   0.47 sec ----> 153 [binary,151.1,23.1] $F.

Length of proof is 2.  Level of proof is 2.

Proof

23 [reference] p2!=p1.
64 [reference] subset pair(x1,x2)=p2|x1 xc !=p1|x2 xc =p1.
85 [reference] remove_singleton pair(xset,k(x)) x=p2.
99 [assumption to refute] subset pair(bads,remove_singleton pair(bads,k(bad)))!=p2.
100 [assumption to refute] bads bad=p1.
123 [ur,100,64,99] remove_singleton pair(bads,k(bad)) bad=p1.
151 [para_into,123.1.1,85.1.1] p2=p1.
153 [binary,151.1,23.1] $F.

up | previous | next | detailed contents | brief contents | OTTER output file