YES(?,O(n^1)) * Step 1: UnsatRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [0 >= 1 + A && B = C && D = E && F = A] (?,1) 1. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [A >= 0 && C >= 1 + E && B = C && D = E && F = A] (?,1) 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (?,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (?,1) 4. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 5. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [D >= B && 0 >= 1 + A && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 8. lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 9. lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [D >= B && 0 >= 1 + A && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [0->{},1->{},2->{4,5,6,7},3->{8,9,10,11},4->{},5->{},6->{4,5,6,7},7->{8,9,10,11},8->{},9->{},10->{4,5,6,7} ,11->{8,9,10,11},12->{0,1,2,3}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [5,9] * Step 2: TrivialSCCs WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [0 >= 1 + A && B = C && D = E && F = A] (?,1) 1. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [A >= 0 && C >= 1 + E && B = C && D = E && F = A] (?,1) 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (?,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (?,1) 4. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 8. lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [0->{},1->{},2->{4,6,7},3->{8,10,11},4->{},6->{4,6,7},7->{8,10,11},8->{},10->{4,6,7},11->{8,10,11},12->{0 ,1,2,3}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [0 >= 1 + A && B = C && D = E && F = A] (1,1) 1. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [A >= 0 && C >= 1 + E && B = C && D = E && F = A] (1,1) 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 4. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (1,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 8. lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (1,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [0->{},1->{},2->{4,6,7},3->{8,10,11},4->{},6->{4,6,7},7->{8,10,11},8->{},10->{4,6,7},11->{8,10,11},12->{0 ,1,2,3}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl101) = 1 + x1 + -1*x2 + x5 p(lbl91) = -1*x2 + x5 p(start) = -1*x2 + x4 p(start0) = -1*x3 + x5 p(stop) = -1*x2 + x5 Following rules are strictly oriented: [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = 1 + A + -1*B + E > A + -1*B + E + -1*F = lbl101(A,1 + B + F,C,D,E,F) Following rules are weakly oriented: [0 >= 1 + A && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = -1*B + D >= -1*B + E = stop(A,B,C,D,E,F) [A >= 0 && C >= 1 + E && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = -1*B + D >= -1*B + E = stop(A,B,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = -1*B + D >= -1*B + E = lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = -1*B + D >= A + -1*B + E + -1*F = lbl101(A,1 + B + F,C,D,E,F) [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = -1*B + E >= -1*B + E = stop(A,B,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = -1*B + E >= -1*B + E = lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = -1*B + E >= A + -1*B + E + -1*F = lbl101(A,1 + B + F,C,D,E,F) [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = 1 + A + -1*B + E >= -1*B + E = stop(A,B,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = 1 + A + -1*B + E >= -1*B + E = lbl91(A,B,C,-1 + D + -1*F,E,F) True ==> start0(A,B,C,D,E,F) = -1*C + E >= -1*C + E = start(A,C,C,E,E,A) * Step 4: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [0 >= 1 + A && B = C && D = E && F = A] (1,1) 1. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [A >= 0 && C >= 1 + E && B = C && D = E && F = A] (1,1) 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 4. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (1,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 8. lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (1,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [0->{},1->{},2->{4,6,7},3->{8,10,11},4->{},6->{4,6,7},7->{8,10,11},8->{},10->{4,6,7},11->{8,10,11},12->{0 ,1,2,3}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl101) = 1 + -1*x2 + x5 p(lbl91) = -1*x2 + x5 p(start) = -1*x2 + x4 p(start0) = -1*x3 + x5 p(stop) = -1*x2 + x5 Following rules are strictly oriented: [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = 1 + -1*B + E > -1*B + E = lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = 1 + -1*B + E > -1*B + E + -1*F = lbl101(A,1 + B + F,C,D,E,F) Following rules are weakly oriented: [0 >= 1 + A && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = -1*B + D >= -1*B + E = stop(A,B,C,D,E,F) [A >= 0 && C >= 1 + E && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = -1*B + D >= -1*B + E = stop(A,B,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = -1*B + D >= -1*B + E = lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = -1*B + D >= -1*B + E + -1*F = lbl101(A,1 + B + F,C,D,E,F) [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = -1*B + E >= -1*B + E = stop(A,B,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = -1*B + E >= -1*B + E = lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = -1*B + E >= -1*B + E + -1*F = lbl101(A,1 + B + F,C,D,E,F) [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = 1 + -1*B + E >= -1*B + E = stop(A,B,C,D,E,F) True ==> start0(A,B,C,D,E,F) = -1*C + E >= -1*C + E = start(A,C,C,E,E,A) * Step 5: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [0 >= 1 + A && B = C && D = E && F = A] (1,1) 1. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [A >= 0 && C >= 1 + E && B = C && D = E && F = A] (1,1) 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 4. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (1,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 8. lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (1,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [0->{},1->{},2->{4,6,7},3->{8,10,11},4->{},6->{4,6,7},7->{8,10,11},8->{},10->{4,6,7},11->{8,10,11},12->{0 ,1,2,3}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl101) = 1 + x1 + -2*x2 + x4 + x5 p(lbl91) = -1*x1 + -2*x2 + x4 + x5 + x6 p(start) = 1 + -2*x3 + 2*x4 p(start0) = 1 + -2*x3 + 2*x5 p(stop) = -2*x2 + x4 + x5 Following rules are strictly oriented: [A >= 0 && E >= C && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = 1 + -2*C + 2*D > -1 + -1*A + -2*B + D + E = lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = -1*A + -2*B + D + E + F > -1 + -1*A + -2*B + D + E = lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = 1 + A + -2*B + D + E > -1 + A + -2*B + D + E + -2*F = lbl101(A,1 + B + F,C,D,E,F) Following rules are weakly oriented: [0 >= 1 + A && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = 1 + -2*C + 2*D >= -2*B + D + E = stop(A,B,C,D,E,F) [A >= 0 && C >= 1 + E && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = 1 + -2*C + 2*D >= -2*B + D + E = stop(A,B,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = 1 + -2*C + 2*D >= -1 + A + -2*B + D + E + -2*F = lbl101(A,1 + B + F,C,D,E,F) [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = -1*A + -2*B + D + E + F >= -2*B + D + E = stop(A,B,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = -1*A + -2*B + D + E + F >= -1 + A + -2*B + D + E + -2*F = lbl101(A,1 + B + F,C,D,E,F) [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = 1 + A + -2*B + D + E >= -2*B + D + E = stop(A,B,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = 1 + A + -2*B + D + E >= -1 + -1*A + -2*B + D + E = lbl91(A,B,C,-1 + D + -1*F,E,F) True ==> start0(A,B,C,D,E,F) = 1 + -2*C + 2*E >= 1 + -2*C + 2*E = start(A,C,C,E,E,A) * Step 6: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [0 >= 1 + A && B = C && D = E && F = A] (1,1) 1. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [A >= 0 && C >= 1 + E && B = C && D = E && F = A] (1,1) 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 4. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (1,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (1 + 2*C + 2*E,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 8. lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (1,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [0->{},1->{},2->{4,6,7},3->{8,10,11},4->{},6->{4,6,7},7->{8,10,11},8->{},10->{4,6,7},11->{8,10,11},12->{0 ,1,2,3}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 7: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [0 >= 1 + A && B = C && D = E && F = A] (1,1) 1. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [A >= 0 && C >= 1 + E && B = C && D = E && F = A] (1,1) 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 4. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (1,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (1 + 2*C + 2*E,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (2 + 3*C + 3*E,1) 8. lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (1,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [0->{},1->{},2->{4,6,7},3->{8,10,11},4->{},6->{4,6,7},7->{8,10,11},8->{},10->{4,6,7},11->{8,10,11},12->{0 ,1,2,3}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: The problem is already solved. YES(?,O(n^1))