closedunder ----> UNIT CONFLICT at 46.42 sec ----> 784 [binary,783.1,68.1] $ans(noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2))). Length of proof is 10. Level of proof is 7.
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). 6 [reference] abst x y z=x k(z) (y z). 10 [reference] p1 pair(x,y)=x. 11 [reference] p2 pair(x,y)=y. 15 [reference] x!=y|eq pair(x,y) =p1. 16 [reference] x=y|eq pair(x,y) =p2. 17 [reference] x=y|x noteq(x,y) !=y noteq(x,y). 18 [reference] p1!=p2. 19 [reference] x y!=p1|isp1 x y =p1. 20 [reference] x y=p1|isp1 x y =p2. 39 [reference] closedunder=abst k(eq) pair(k(k(p2)),abst k(abst k(eq)) pair(pair(p1,abst (abst k(abst) (abst k(abst k(isp1)) (abst k(p1)))) p2),k(k(pair(p1,p2))))). 41 [assumption to refute] p. 42 [assumption to refute] bads x!=p1|bads (badf x) =p1|$ans(x). 43 [assumption to refute] -p|closedunder pair(bads,badf) !=p1. 44 [ur,43,41,demod,39,6,1,4,1,6,1,4,4,2,6,6,1,6,1,3,1] eq pair(k(p2),abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))))!=p1. 51,50 [ur,44,20] isp1 eq pair(k(p2),abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))))=p2. 55 [ur,44,15,flip.1] abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2)))!=k(p2). 59 [ur,55,17,demod,6,1,4,4,6,6,1,6,1,1,2,1,1] eq pair(pair(bads noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2)),isp1 bads (badf noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2)))),pair(p1,p2))!=p2. 68 [para_from,50.1.2,18.1.2,demod,51,flip.1] p2!=p1. 141 [ur,59,16] pair(bads noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2)),isp1 bads (badf noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2))))=pair(p1,p2). 698,697 [para_from,141.1.1,11.1.1.2,demod,3,flip.1] isp1 bads (badf noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2)))=p2. 699 [para_from,141.1.1,10.1.1.2,demod,2,flip.1] bads noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2))=p1. 732 [ur,699,42] bads (badf noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2)))=p1|$ans(noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2))). 783 [ur,732,19,demod,698] $ans(noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2)))|p2=p1. 784 [binary,783.1,68.1] $ans(noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2))).
up | previous | next | detailed contents | brief contents | OTTER output file