closure pair(s, f) is closed under f ----> UNIT CONFLICT at 7.47 sec ----> 919 [binary,917.1,19.1] $F. Length of proof is 12. Level of proof is 6.
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). 16 [reference] x=y|eq pair(x,y) =p2. 19 [reference] p2!=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. 48 [reference] charq eq=p1. 51 [reference] abst k(x) k(y)=k(x y). 53 [reference] pair(x1,y1)!=pair(x2,y2)|y1=y2. 66 [reference] closedunder pair(kintersection x y,z)=p1|x notinint(x,z notclosed(kintersection x y,z)) =p1. 67 [reference] closedunder pair(kintersection x y,z)=p1|closedunder pair(notinint(x,z notclosed(kintersection x y,z)),z) =p2. 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). 74 [assumption to refute] p. 75 [assumption to refute] -p|closedunder pair(closure pair(bads,badf),badf) !=p1. 76 [ur,75,74,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] closedunder 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),badf)!=p1. 78,77 [ur,76,67] closedunder pair(notinint(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)))),badf notclosed(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),badf)),badf)=p2. 79 [ur,76,66,demod,6,1,4,1,4,6,1,4,1,4,5,6,1,4,4,5,1,78] eq pair(pair(p1,p1),pair(subset pair(bads,notinint(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)))),badf notclosed(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),badf))),p2))=p1. 89 [ur,76,47] 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) (badf notclosed(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),badf))!=p1. 90 [ur,76,46] 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) notclosed(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),badf)=p1. 119 [para_into,76.1.2,48.1.2] closedunder 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),badf)!=charq eq. 202 [ur,119,53] pair(x,closedunder 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),badf))!=pair(y,charq eq). 256 [para_into,79.1.1.2.1.2,48.1.2] eq pair(pair(p1,charq eq),pair(subset pair(bads,notinint(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)))),badf notclosed(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),badf))),p2))=p1. 671,670 [ur,90,45,89] closedunder 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),badf)=p2. 707 [back_demod,202,demod,671,flip.1] pair(x,charq eq)!=pair(y,p2). 916,915 [ur,707,16] eq pair(pair(x,charq eq),pair(y,p2))=p2. 917 [back_demod,256,demod,916] p2=p1. 919 [binary,917.1,19.1] $F.
up | previous | next | detailed contents | brief contents | OTTER output file