YES(?,O(n^1)) * Step 1: TrivialSCCs WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (?,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (?,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (?,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (?,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (?,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (?,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (?,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (?,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (?,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (?,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (1,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (1,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (1,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (1,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (?,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (1,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (?,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (?,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (?,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl121) = -4 + 5*x1 + -1*x8 p(lbl141) = -4 + 5*x1 + -1*x8 p(lbl171) = -3 + 5*x1 + -1*x8 p(lbl191) = -4 + 5*x1 + -1*x8 p(lbl21) = -4 + 5*x1 + -1*x8 p(lbl81) = -3 + 5*x1 + -1*x8 p(start) = 5*x1 p(start0) = 5*x1 p(stop) = -4 + 5*x1 + -1*x8 Following rules are strictly oriented: [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -3 + 5*A + -1*H > -4 + 5*A + -1*H = lbl191(A,-1 + B,C,D,E,F,G,H,I,J) Following rules are weakly oriented: [0 >= A && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = 5*A >= -4 + 5*A = stop(A,0,C,0,E,F,G,0,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = 5*A >= -4 + 5*A = lbl81(A,0,C,0,E,K,G,1,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = -4 + 5*A + -1*H >= -4 + 5*A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = -4 + 5*A + -1*H >= -4 + 5*A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = -4 + 5*A + -1*H >= -4 + 5*A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = -4 + 5*A + -1*H >= -4 + 5*A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = -4 + 5*A + -1*H >= -4 + 5*A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = -4 + 5*A + -1*H >= -4 + 5*A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = -3 + 5*A + -1*H >= -4 + 5*A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = -3 + 5*A + -1*H >= -4 + 5*A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = -4 + 5*A + -1*H >= -4 + 5*A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = -4 + 5*A + -1*H >= -4 + 5*A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -3 + 5*A + -1*H >= -4 + 5*A + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -3 + 5*A + -1*H >= -4 + 5*A + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -3 + 5*A + -1*H >= -4 + 5*A + -1*H = lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -3 + 5*A + -1*H >= -4 + 5*A + -1*H = lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -3 + 5*A + -1*H >= -3 + 5*A + -1*H = lbl171(A,1 + B,C,D,E,F,G,H,I,J) True ==> start0(A,B,C,D,E,F,G,H,I,J) = 5*A >= 5*A = start(A,C,C,E,E,G,G,I,I,A) * Step 3: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (1,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (1,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (1,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (1,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (?,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (1,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (?,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (?,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (5*A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 4: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (1,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (1,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (1,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (1,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (?,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (1,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (5*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (?,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (5*A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl121) = -3 + 4*x1 + -1*x2 + x4 + -1*x8 p(lbl141) = -1 + 4*x1 + -1*x2 + x4 + -1*x8 p(lbl171) = -2 + 4*x1 + -1*x2 + x4 + -1*x8 p(lbl191) = -3 + 4*x1 + -1*x2 + x4 + -1*x8 p(lbl21) = -3 + 4*x1 + -1*x2 + x4 + -1*x8 p(lbl81) = -2 + 4*x1 + -1*x2 + x4 + -1*x8 p(start) = 4*x1 p(start0) = 4*x1 p(stop) = -3 + 4*x1 + -1*x2 + x4 + -1*x8 Following rules are strictly oriented: [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 4*A + -1*B + D + -1*H > -3 + 4*A + -1*B + D + -1*H = lbl171(A,1 + B,C,D,E,F,G,H,I,J) Following rules are weakly oriented: [0 >= A && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = 4*A >= -3 + 4*A = stop(A,0,C,0,E,F,G,0,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = 4*A >= -3 + 4*A = lbl81(A,0,C,0,E,K,G,1,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = -3 + 4*A + -1*B + D + -1*H >= -3 + 4*A + -1*B + D + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = -3 + 4*A + -1*B + D + -1*H >= -3 + 4*A + -1*B + D + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = -3 + 4*A + -1*B + D + -1*H >= -3 + 4*A + -1*B + D + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = -3 + 4*A + -1*B + D + -1*H >= -3 + 4*A + -1*B + D + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = -1 + 4*A + -1*B + D + -1*H >= -3 + 4*A + -1*B + D + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = -1 + 4*A + -1*B + D + -1*H >= -3 + 4*A + -1*B + D + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = -2 + 4*A + -1*B + D + -1*H >= -3 + 4*A + -1*B + D + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = -2 + 4*A + -1*B + D + -1*H >= -3 + 4*A + -1*B + D + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = -3 + 4*A + -1*B + D + -1*H >= -3 + 4*A + -1*B + D + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = -3 + 4*A + -1*B + D + -1*H >= -3 + 4*A + -1*B + D + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 4*A + -1*B + D + -1*H >= -3 + 4*A + -1*B + D + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 4*A + -1*B + D + -1*H >= -3 + 4*A + -1*B + D + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 4*A + -1*B + D + -1*H >= -2 + 4*A + -1*B + D + -1*H = lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 4*A + -1*B + D + -1*H >= -2 + 4*A + -1*B + D + -1*H = lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 4*A + -1*B + D + -1*H >= -2 + 4*A + -1*B + D + -1*H = lbl191(A,-1 + B,C,D,E,F,G,H,I,J) True ==> start0(A,B,C,D,E,F,G,H,I,J) = 4*A >= 4*A = start(A,C,C,E,E,G,G,I,I,A) * Step 5: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (1,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (1,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (1,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (1,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (?,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (1,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (5*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (4*A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (5*A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 6: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (1,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (1,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (1,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (1,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (4*A,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (1,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (5*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (4*A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (5*A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl121) = -3 + 5*x1 + -1*x8 p(lbl141) = -3 + 5*x1 + -1*x8 p(lbl171) = -2 + 5*x1 + -1*x8 p(lbl191) = -2 + 5*x1 + -1*x8 p(lbl21) = -2 + 5*x1 + -1*x8 p(lbl81) = -2 + 5*x1 + -1*x8 p(start) = -3 + 5*x1 p(start0) = -3 + 5*x1 p(stop) = -3 + 5*x1 + -1*x8 Following rules are strictly oriented: [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = -2 + 5*A + -1*H > -3 + 5*A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = -2 + 5*A + -1*H > -3 + 5*A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 5*A + -1*H > -3 + 5*A + -1*H = lbl141(A,B,C,-1 + D,E,F,G,H,I,J) Following rules are weakly oriented: [0 >= A && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = -3 + 5*A >= -3 + 5*A = stop(A,0,C,0,E,F,G,0,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = -3 + 5*A >= -3 + 5*A = lbl81(A,0,C,0,E,K,G,1,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = -2 + 5*A + -1*H >= -3 + 5*A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = -2 + 5*A + -1*H >= -3 + 5*A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = -3 + 5*A + -1*H >= -3 + 5*A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = -3 + 5*A + -1*H >= -3 + 5*A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = -3 + 5*A + -1*H >= -3 + 5*A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = -3 + 5*A + -1*H >= -3 + 5*A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = -2 + 5*A + -1*H >= -3 + 5*A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = -2 + 5*A + -1*H >= -3 + 5*A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 5*A + -1*H >= -2 + 5*A + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 5*A + -1*H >= -2 + 5*A + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 5*A + -1*H >= -3 + 5*A + -1*H = lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 5*A + -1*H >= -2 + 5*A + -1*H = lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 5*A + -1*H >= -2 + 5*A + -1*H = lbl191(A,-1 + B,C,D,E,F,G,H,I,J) True ==> start0(A,B,C,D,E,F,G,H,I,J) = -3 + 5*A >= -3 + 5*A = start(A,C,C,E,E,G,G,I,I,A) * Step 7: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (1,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (1,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (1,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (1,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (4*A,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (1,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (5*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (3 + 5*A,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (4*A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (5*A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 8: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (1,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (1,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (1,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (3 + 5*A,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (1,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (4*A,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (1,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (5*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (3 + 5*A,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (4*A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (5*A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl121) = -4 + 6*x1 + -1*x2 + -1*x4 + -1*x8 p(lbl141) = -4 + 6*x1 + -1*x2 + -1*x4 + -1*x8 p(lbl171) = -2 + 6*x1 + -1*x2 + -1*x4 + -1*x8 p(lbl191) = -4 + 6*x1 + -1*x2 + -1*x4 + -1*x8 p(lbl21) = -4 + 6*x1 + -1*x2 + -1*x4 + -1*x8 p(lbl81) = -3 + 6*x1 + -1*x2 + -1*x4 + -1*x8 p(start) = 6*x1 p(start0) = 6*x1 p(stop) = -4 + 6*x1 + -1*x2 + -1*x4 + -1*x8 Following rules are strictly oriented: [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -3 + 6*A + -1*B + -1*D + -1*H > -5 + 6*A + -1*B + -1*D + -1*H = lbl121(A,B,C,1 + D,E,F,G,H,I,J) Following rules are weakly oriented: [0 >= A && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = 6*A >= -4 + 6*A = stop(A,0,C,0,E,F,G,0,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = 6*A >= -4 + 6*A = lbl81(A,0,C,0,E,K,G,1,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = -4 + 6*A + -1*B + -1*D + -1*H >= -4 + 6*A + -1*B + -1*D + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = -4 + 6*A + -1*B + -1*D + -1*H >= -4 + 6*A + -1*B + -1*D + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = -4 + 6*A + -1*B + -1*D + -1*H >= -4 + 6*A + -1*B + -1*D + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = -4 + 6*A + -1*B + -1*D + -1*H >= -4 + 6*A + -1*B + -1*D + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = -4 + 6*A + -1*B + -1*D + -1*H >= -4 + 6*A + -1*B + -1*D + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = -4 + 6*A + -1*B + -1*D + -1*H >= -4 + 6*A + -1*B + -1*D + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = -2 + 6*A + -1*B + -1*D + -1*H >= -4 + 6*A + -1*B + -1*D + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = -2 + 6*A + -1*B + -1*D + -1*H >= -4 + 6*A + -1*B + -1*D + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = -4 + 6*A + -1*B + -1*D + -1*H >= -4 + 6*A + -1*B + -1*D + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = -4 + 6*A + -1*B + -1*D + -1*H >= -4 + 6*A + -1*B + -1*D + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -3 + 6*A + -1*B + -1*D + -1*H >= -4 + 6*A + -1*B + -1*D + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -3 + 6*A + -1*B + -1*D + -1*H >= -4 + 6*A + -1*B + -1*D + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -3 + 6*A + -1*B + -1*D + -1*H >= -3 + 6*A + -1*B + -1*D + -1*H = lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -3 + 6*A + -1*B + -1*D + -1*H >= -3 + 6*A + -1*B + -1*D + -1*H = lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -3 + 6*A + -1*B + -1*D + -1*H >= -3 + 6*A + -1*B + -1*D + -1*H = lbl191(A,-1 + B,C,D,E,F,G,H,I,J) True ==> start0(A,B,C,D,E,F,G,H,I,J) = 6*A >= 6*A = start(A,C,C,E,E,G,G,I,I,A) * Step 9: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (1,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (1,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (1,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (3 + 5*A,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (1,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (4*A,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (1,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (5*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (6*A,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (3 + 5*A,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (4*A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (5*A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 10: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (1,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (1,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (6*A,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (1,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (3 + 5*A,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (1,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (4*A,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (1,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (5*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (6*A,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (3 + 5*A,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (4*A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (5*A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl121) = x1 + -1*x8 p(lbl141) = x1 + -1*x8 p(lbl171) = x1 + -1*x8 p(lbl191) = x1 + -1*x8 p(lbl21) = x1 + -1*x8 p(lbl81) = 1 + x1 + -1*x8 p(start) = x1 p(start0) = x1 p(stop) = x1 + -1*x8 Following rules are strictly oriented: [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl191(A,-1 + B,C,D,E,F,G,H,I,J) Following rules are weakly oriented: [0 >= A && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = A >= A = stop(A,0,C,0,E,F,G,0,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = A >= A = lbl81(A,0,C,0,E,K,G,1,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H >= A + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) True ==> start0(A,B,C,D,E,F,G,H,I,J) = A >= A = start(A,C,C,E,E,G,G,I,I,A) * Step 11: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (1,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (1,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (6*A,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (1,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (3 + 5*A,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (1,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (4*A,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (1,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (5*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (A,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (6*A,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (3 + 5*A,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (4*A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (5*A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl121) = x1 + -1*x8 p(lbl141) = x1 + -1*x8 p(lbl171) = x1 + -1*x8 p(lbl191) = x1 + -1*x8 p(lbl21) = x1 + -1*x8 p(lbl81) = 1 + x1 + -1*x8 p(start) = x1 p(start0) = x1 p(stop) = x1 + -1*x8 Following rules are strictly oriented: [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl191(A,-1 + B,C,D,E,F,G,H,I,J) Following rules are weakly oriented: [0 >= A && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = A >= A = stop(A,0,C,0,E,F,G,0,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = A >= A = lbl81(A,0,C,0,E,K,G,1,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = stop(A,B,C,D,E,F,G,H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) True ==> start0(A,B,C,D,E,F,G,H,I,J) = A >= A = start(A,C,C,E,E,G,G,I,I,A) * Step 12: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (1,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (1,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (6*A,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (1,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (3 + 5*A,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (1,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (4*A,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (1,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (5*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (A,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (A,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (6*A,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (3 + 5*A,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (4*A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (5*A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 13: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (1,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (2*A,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (1,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (6*A,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (1,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (3 + 5*A,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (1,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (4*A,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (1,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (5*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (A,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (A,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (6*A,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (3 + 5*A,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (4*A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (5*A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: The problem is already solved. YES(?,O(n^1))