charq push x = p1 ----> UNIT CONFLICT at 46.51 sec ----> 6280 [binary,6278.1,1559.1] $F. Length of proof is 12. Level of proof is 6.
2 [reference] p1 pair(x,y)=x. 3 [reference] p2 pair(x,y)=y. 23 [reference] p2!=p1. 30 [reference] x y=p1|notp1 x y =p1. 40 [reference] charq xf=p2|xf x =p1|xf x =p2. 41 [reference] charq xf=p1|xf noteq(isp1 xf,xf) !=p1. 42 [reference] charq xf=p1|xf noteq(isp1 xf,xf) !=p2. 44 [reference] setof xf pair(x,y)=p2|xf x =y. 45 [reference] p2 xy!=xf (p1 xy) |setof xf xy =p1. 47 [reference] charq (setof x)=p1. 64 [reference] subset pair(x1,x2)=p2|x1 xc !=p1|x2 xc =p1. 76 [reference] subset pair(xs,closure pair(xs,xf))=p1. 83 [reference] closure pair(notp1 charq,setof) x=p1|push x =x. 84 [reference] closure pair(notp1 charq,setof) x=p2|push x =setof x. 85 [assumption to refute] charq (push bad)!=p1. 108,107 [para_into,85.1.1.2,84.2.1,unit_del,47] closure pair(notp1 charq,setof) bad=p2. 109 [para_into,85.1.1.2,83.2.1,demod,108,unit_del,23] charq bad!=p1. 177 [hyper,109,30] notp1 charq bad=p1. 186 [neg_hyper,109,42] bad noteq(isp1 bad,bad)!=p2. 187 [neg_hyper,109,41] bad noteq(isp1 bad,bad)!=p1. 197 [para_into,109.1.1,44.2.1] x!=p1|setof charq pair(bad,x) =p2. 205 [para_into,109.1.2,76.1.2,flip.1] subset pair(x,closure pair(x,y))!=charq bad. 252 [hyper,177,64] subset pair(notp1 charq,x)=p2|x bad =p1. 1285,1284 [hyper,186,40,unit_del,187] charq bad=p2. 1559 [back_demod,205,demod,1285] subset pair(x,closure pair(x,y))!=p2. 5667 [para_into,197.2.1,45.2.1,demod,3,2,1285,unit_del,23] x!=p1|x!=p2. 6278 [hyper,252,5667,107] subset pair(notp1 charq,closure pair(notp1 charq,setof))=p2. 6280 [binary,6278.1,1559.1] $F.
up | previous | next | detailed contents | brief contents | OTTER output file