closure pair(s, f) is the smallest such set ----> UNIT CONFLICT at 1971.40 sec ----> 14492 [binary,14490.1,14414.1] $F. Length of proof is 10. Level of proof is 8.
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). 8 [reference] x=x. 20 [reference] p1 x!=p2 x |eq x =p1. 45 [reference] closedunder pair(xs,xf)=p2|xs x !=p1|xs (xf x) =p1. 46 [reference] closedunder pair(xs,xf)=p1|xs notclosed(xs,xf) =p1. 47 [reference] closedunder pair(xs,xf)=p1|xs (xf notclosed(xs,xf)) !=p1. 51 [reference] abst k(x) k(y)=k(x y). 60 [reference] subset pair(x1,x2)=p2|x1 xc !=p1|x2 xc =p1. 64 [reference] subset x=p1|p1 x notsub(p1 x,p2 x) =p1. 65 [reference] subset x=p1|p2 x notsub(p1 x,p2 x) !=p1. 68 [reference] subset pair(kintersection x y,z)=p1|x z !=p1. 72 [reference] closure=abst (abst k(kintersection) (abst k(abst k(eq)) pair(k(k(pair(p1,p1))),pair(abst k(abst k(subset)) pair(abst k(p1),k(pair(p1,p2))),abst k(abst k(closedunder)) pair(k(pair(p1,p2)),abst k(p2)))))) pair(p1,p2). 75 [assumption to refute] p. 76 [assumption to refute] closedunder pair(bad,badf)!=p2. 77 [assumption to refute] subset pair(bads,bad)!=p2. 78 [assumption to refute] -p|subset pair(closure pair(bads,badf),bad) !=p1. 81 [ur,78,75,demod,72,6,6,1,6,1,4,1,4,6,1,4,51,2,1,6,1,4,1,51,3,4,2,3] subset pair(kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf),bad)!=p1. 82 [neg_hyper,81,68,demod,6,1,4,1,4,6,1,4,1,4,5,6,1,4,4,5,1] eq pair(pair(p1,p1),pair(subset pair(bads,bad),closedunder pair(bad,badf)))!=p1. 116 [neg_hyper,82,20,demod,2,3,flip.1] pair(subset pair(bads,bad),closedunder pair(bad,badf))!=pair(p1,p1). 191 [para_into,116.1.1.1,65.1.1,demod,3,2,3] pair(p1,closedunder pair(bad,badf))!=pair(p1,p1)|bad notsub(bads,bad) !=p1. 192 [para_into,116.1.1.1,64.1.1,demod,2,2,3] pair(p1,closedunder pair(bad,badf))!=pair(p1,p1)|bads notsub(bads,bad) =p1. 1394 [neg_hyper,191,60,77] pair(p1,closedunder pair(bad,badf))!=pair(p1,p1)|bads notsub(bads,bad) !=p1. 14408 [neg_hyper,1394,192] pair(p1,closedunder pair(bad,badf))!=pair(p1,p1). 14414 [para_into,14408.1.1.2,47.1.1,unit_del,8] bad (badf notclosed(bad,badf))!=p1. 14415 [para_into,14408.1.1.2,46.1.1,unit_del,8] bad notclosed(bad,badf)=p1. 14490 [ur,14415,45,76] bad (badf notclosed(bad,badf))=p1. 14492 [binary,14490.1,14414.1] $F.
up | previous | next | detailed contents | brief contents | OTTER output file