closure ----> UNIT CONFLICT at 30923.91 sec ----> 19464 [binary,19463.1,23.1] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)). Length of proof is 13. Level of proof is 8.
2 [reference] p1 pair(x,y)=x. 3 [reference] p2 pair(x,y)=y. 12 [reference] x=x. 23 [reference] p2!=p1. 26 [reference] x y!=p1|isp1 x y =p1. 27 [reference] x y=p1|isp1 x y =p2. 64 [reference] subset pair(x1,x2)=p2|x1 xc !=p1|x2 xc =p1. 68 [reference] subset x=p1|p1 x notsub(p1 x,p2 x) =p1. 69 [reference] subset x=p1|p2 x notsub(p1 x,p2 x) !=p1. 76 [reference] subset pair(xs,closure pair(xs,xf))=p1. 79 [reference] closure x y=p1|closure x y =p2. 82 [reference] closedunder pair(x2,p2 x1)=p2|subset pair(p1 x1,x2) =p2|subset pair(closure x1,x2) =p1. 83 [reference] xset x!=p1|x=x1|remove_singleton pair(xset,k(x1)) x =p1. 98 [reference] closedunder pair(remove_singleton pair(closure pair(xs,xf),k(x)),xf)=p1|xs x =p1|xf notclosed(remove_singleton pair(closure pair(xs,xf),k(x)),xf) =x. 99 [reference] subset pair(xs,remove_singleton pair(xs,k(x)))=p2|xs x !=p1. 100 [assumption to refute] badf x!=bad|$ans(x). 101 [assumption to refute] closure pair(bads,badf) bad!=p2. 102 [assumption to refute] bads bad!=p1. 106 [ur,101,79] closure pair(bads,badf) bad=p1. 117 [ur,102,98,100] closedunder pair(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)=p1|$ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)). 131,130 [ur,102,27] isp1 bads bad=p2. 138 [ur,106,99] subset pair(closure pair(bads,badf),remove_singleton pair(closure pair(bads,badf),k(bad)))=p2. 167 [para_from,117.1.2,23.1.2,flip.1] closedunder pair(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)!=p2|$ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)). 182 [para_into,138.1.1,82.3.1,demod,3,2,unit_del,23,167] subset pair(bads,remove_singleton pair(closure pair(bads,badf),k(bad)))=p2|$ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)). 212 [para_into,182.1.1,69.1.1,demod,3,2,3,unit_del,23] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf))|remove_singleton pair(closure pair(bads,badf),k(bad)) notsub(bads,remove_singleton pair(closure pair(bads,badf),k(bad))) !=p1. 213 [para_into,182.1.1,68.1.1,demod,2,2,3,unit_del,23] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf))|bads notsub(bads,remove_singleton pair(closure pair(bads,badf),k(bad))) =p1. 242 [para_into,212.2.1,83.3.1,unit_del,12] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf))|closure pair(bads,badf) notsub(bads,remove_singleton pair(closure pair(bads,badf),k(bad))) !=p1|notsub(bads,remove_singleton pair(closure pair(bads,badf),k(bad)))=bad. 250 [ur,213,26] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf))|isp1 bads notsub(bads,remove_singleton pair(closure pair(bads,badf),k(bad))) =p1. 10198 [para_from,242.2.1,250.2.1.2,demod,131,unit_del,23] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf))|closure pair(bads,badf) notsub(bads,remove_singleton pair(closure pair(bads,badf),k(bad))) !=p1. 19461 [ur,10198,64,213] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf))|subset pair(bads,closure pair(bads,badf)) =p2. 19463 [para_into,19461.2.1,76.1.1,flip.2] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf))|p2=p1. 19464 [binary,19463.1,23.1] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)).
up | previous | next | detailed contents | brief contents | OTTER output file