YES(?,O(n^1)) * Step 1: TrivialSCCs WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalcomplexstart(A,B,C,D,E) -> evalcomplexentryin(A,B,C,D,E) True (1,1) 1. evalcomplexentryin(A,B,C,D,E) -> evalcomplexbb10in(B,A,C,D,E) True (?,1) 2. evalcomplexbb10in(A,B,C,D,E) -> evalcomplexreturnin(A,B,C,D,E) [B >= 30] (?,1) 3. evalcomplexbb10in(A,B,C,D,E) -> evalcomplexbb8in(A,B,A,B,E) [29 >= B] (?,1) 4. evalcomplexreturnin(A,B,C,D,E) -> evalcomplexstop(A,B,C,D,E) [-30 + B >= 0] (?,1) 5. evalcomplexbb8in(A,B,C,D,E) -> evalcomplexbb9in(A,B,C,D,E) [-1*B + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && C >= D] (?,1) 6. evalcomplexbb8in(A,B,C,D,E) -> evalcomplexbb1in(A,B,C,D,E) [-1*B + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && D >= 1 + C] (?,1) 7. evalcomplexbb9in(A,B,C,D,E) -> evalcomplexbb10in(-10 + C,2 + D,C,D,E) [C + -1*D >= 0 && -1*B + D >= 0 && -1*B + C >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0] (?,1) 8. evalcomplexbb1in(A,B,C,D,E) -> evalcomplexbb7in(A,B,C,D,2 + C) [-1 + -1*C + D >= 0 (?,1) && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && 5 >= C && 7 >= C] 9. evalcomplexbb1in(A,B,C,D,E) -> evalcomplexbb7in(A,B,C,D,7 + C) [-1 + -1*C + D >= 0 && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && C >= 6] (?,1) 10. evalcomplexbb7in(A,B,C,D,E) -> evalcomplexbb8in(A,B,E,1 + D,E) [6 + D + -1*E >= 0 (?,1) && 7 + C + -1*E >= 0 && -2 + -1*C + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*C + D >= 0 && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0] Signature: {(evalcomplexbb10in,5) ;(evalcomplexbb1in,5) ;(evalcomplexbb7in,5) ;(evalcomplexbb8in,5) ;(evalcomplexbb9in,5) ;(evalcomplexentryin,5) ;(evalcomplexreturnin,5) ;(evalcomplexstart,5) ;(evalcomplexstop,5)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{5,6},4->{},5->{7},6->{8,9},7->{2,3},8->{10},9->{10},10->{5,6}] + 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. evalcomplexstart(A,B,C,D,E) -> evalcomplexentryin(A,B,C,D,E) True (1,1) 1. evalcomplexentryin(A,B,C,D,E) -> evalcomplexbb10in(B,A,C,D,E) True (1,1) 2. evalcomplexbb10in(A,B,C,D,E) -> evalcomplexreturnin(A,B,C,D,E) [B >= 30] (1,1) 3. evalcomplexbb10in(A,B,C,D,E) -> evalcomplexbb8in(A,B,A,B,E) [29 >= B] (?,1) 4. evalcomplexreturnin(A,B,C,D,E) -> evalcomplexstop(A,B,C,D,E) [-30 + B >= 0] (1,1) 5. evalcomplexbb8in(A,B,C,D,E) -> evalcomplexbb9in(A,B,C,D,E) [-1*B + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && C >= D] (?,1) 6. evalcomplexbb8in(A,B,C,D,E) -> evalcomplexbb1in(A,B,C,D,E) [-1*B + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && D >= 1 + C] (?,1) 7. evalcomplexbb9in(A,B,C,D,E) -> evalcomplexbb10in(-10 + C,2 + D,C,D,E) [C + -1*D >= 0 && -1*B + D >= 0 && -1*B + C >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0] (?,1) 8. evalcomplexbb1in(A,B,C,D,E) -> evalcomplexbb7in(A,B,C,D,2 + C) [-1 + -1*C + D >= 0 (?,1) && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && 5 >= C && 7 >= C] 9. evalcomplexbb1in(A,B,C,D,E) -> evalcomplexbb7in(A,B,C,D,7 + C) [-1 + -1*C + D >= 0 && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && C >= 6] (?,1) 10. evalcomplexbb7in(A,B,C,D,E) -> evalcomplexbb8in(A,B,E,1 + D,E) [6 + D + -1*E >= 0 (?,1) && 7 + C + -1*E >= 0 && -2 + -1*C + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*C + D >= 0 && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0] Signature: {(evalcomplexbb10in,5) ;(evalcomplexbb1in,5) ;(evalcomplexbb7in,5) ;(evalcomplexbb8in,5) ;(evalcomplexbb9in,5) ;(evalcomplexentryin,5) ;(evalcomplexreturnin,5) ;(evalcomplexstart,5) ;(evalcomplexstop,5)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{5,6},4->{},5->{7},6->{8,9},7->{2,3},8->{10},9->{10},10->{5,6}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalcomplexbb10in) = 179 + -1*x1 + -5*x2 p(evalcomplexbb1in) = 179 + -6*x2 + -1*x3 + x4 p(evalcomplexbb7in) = 181 + -6*x2 + x4 + -1*x5 p(evalcomplexbb8in) = 179 + -6*x2 + -1*x3 + x4 p(evalcomplexbb9in) = 179 + -6*x2 + -1*x3 + x4 p(evalcomplexentryin) = 179 + -5*x1 + -1*x2 p(evalcomplexreturnin) = 179 + -1*x1 + -5*x2 p(evalcomplexstart) = 179 + -5*x1 + -1*x2 p(evalcomplexstop) = 179 + -1*x1 + -5*x2 Following rules are strictly oriented: [6 + D + -1*E >= 0 ==> && 7 + C + -1*E >= 0 && -2 + -1*C + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*C + D >= 0 && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0] evalcomplexbb7in(A,B,C,D,E) = 181 + -6*B + D + -1*E > 180 + -6*B + D + -1*E = evalcomplexbb8in(A,B,E,1 + D,E) Following rules are weakly oriented: True ==> evalcomplexstart(A,B,C,D,E) = 179 + -5*A + -1*B >= 179 + -5*A + -1*B = evalcomplexentryin(A,B,C,D,E) True ==> evalcomplexentryin(A,B,C,D,E) = 179 + -5*A + -1*B >= 179 + -5*A + -1*B = evalcomplexbb10in(B,A,C,D,E) [B >= 30] ==> evalcomplexbb10in(A,B,C,D,E) = 179 + -1*A + -5*B >= 179 + -1*A + -5*B = evalcomplexreturnin(A,B,C,D,E) [29 >= B] ==> evalcomplexbb10in(A,B,C,D,E) = 179 + -1*A + -5*B >= 179 + -1*A + -5*B = evalcomplexbb8in(A,B,A,B,E) [-30 + B >= 0] ==> evalcomplexreturnin(A,B,C,D,E) = 179 + -1*A + -5*B >= 179 + -1*A + -5*B = evalcomplexstop(A,B,C,D,E) [-1*B + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && C >= D] ==> evalcomplexbb8in(A,B,C,D,E) = 179 + -6*B + -1*C + D >= 179 + -6*B + -1*C + D = evalcomplexbb9in(A,B,C,D,E) [-1*B + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && D >= 1 + C] ==> evalcomplexbb8in(A,B,C,D,E) = 179 + -6*B + -1*C + D >= 179 + -6*B + -1*C + D = evalcomplexbb1in(A,B,C,D,E) [C + -1*D >= 0 && -1*B + D >= 0 && -1*B + C >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0] ==> evalcomplexbb9in(A,B,C,D,E) = 179 + -6*B + -1*C + D >= 179 + -1*C + -5*D = evalcomplexbb10in(-10 + C,2 + D,C,D,E) [-1 + -1*C + D >= 0 ==> && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && 5 >= C && 7 >= C] evalcomplexbb1in(A,B,C,D,E) = 179 + -6*B + -1*C + D >= 179 + -6*B + -1*C + D = evalcomplexbb7in(A,B,C,D,2 + C) [-1 + -1*C + D >= 0 && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && C >= 6] ==> evalcomplexbb1in(A,B,C,D,E) = 179 + -6*B + -1*C + D >= 174 + -6*B + -1*C + D = evalcomplexbb7in(A,B,C,D,7 + C) * Step 3: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalcomplexstart(A,B,C,D,E) -> evalcomplexentryin(A,B,C,D,E) True (1,1) 1. evalcomplexentryin(A,B,C,D,E) -> evalcomplexbb10in(B,A,C,D,E) True (1,1) 2. evalcomplexbb10in(A,B,C,D,E) -> evalcomplexreturnin(A,B,C,D,E) [B >= 30] (1,1) 3. evalcomplexbb10in(A,B,C,D,E) -> evalcomplexbb8in(A,B,A,B,E) [29 >= B] (?,1) 4. evalcomplexreturnin(A,B,C,D,E) -> evalcomplexstop(A,B,C,D,E) [-30 + B >= 0] (1,1) 5. evalcomplexbb8in(A,B,C,D,E) -> evalcomplexbb9in(A,B,C,D,E) [-1*B + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && C >= D] (?,1) 6. evalcomplexbb8in(A,B,C,D,E) -> evalcomplexbb1in(A,B,C,D,E) [-1*B + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && D >= 1 + C] (?,1) 7. evalcomplexbb9in(A,B,C,D,E) -> evalcomplexbb10in(-10 + C,2 + D,C,D,E) [C + -1*D >= 0 && -1*B + D >= 0 && -1*B + C >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0] (?,1) 8. evalcomplexbb1in(A,B,C,D,E) -> evalcomplexbb7in(A,B,C,D,2 + C) [-1 + -1*C + D >= 0 (?,1) && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && 5 >= C && 7 >= C] 9. evalcomplexbb1in(A,B,C,D,E) -> evalcomplexbb7in(A,B,C,D,7 + C) [-1 + -1*C + D >= 0 && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && C >= 6] (?,1) 10. evalcomplexbb7in(A,B,C,D,E) -> evalcomplexbb8in(A,B,E,1 + D,E) [6 + D + -1*E >= 0 (179 + 5*A + B,1) && 7 + C + -1*E >= 0 && -2 + -1*C + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*C + D >= 0 && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0] Signature: {(evalcomplexbb10in,5) ;(evalcomplexbb1in,5) ;(evalcomplexbb7in,5) ;(evalcomplexbb8in,5) ;(evalcomplexbb9in,5) ;(evalcomplexentryin,5) ;(evalcomplexreturnin,5) ;(evalcomplexstart,5) ;(evalcomplexstop,5)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{5,6},4->{},5->{7},6->{8,9},7->{2,3},8->{10},9->{10},10->{5,6}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalcomplexbb10in) = 31 + -1*x2 p(evalcomplexbb1in) = 31 + -1*x2 p(evalcomplexbb7in) = 31 + -1*x2 p(evalcomplexbb8in) = 31 + -1*x2 p(evalcomplexbb9in) = 30 + -1*x2 p(evalcomplexentryin) = 31 + -1*x1 p(evalcomplexreturnin) = 31 + -1*x2 p(evalcomplexstart) = 31 + -1*x1 p(evalcomplexstop) = 31 + -1*x2 Following rules are strictly oriented: [-1*B + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && C >= D] ==> evalcomplexbb8in(A,B,C,D,E) = 31 + -1*B > 30 + -1*B = evalcomplexbb9in(A,B,C,D,E) [C + -1*D >= 0 && -1*B + D >= 0 && -1*B + C >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0] ==> evalcomplexbb9in(A,B,C,D,E) = 30 + -1*B > 29 + -1*D = evalcomplexbb10in(-10 + C,2 + D,C,D,E) Following rules are weakly oriented: True ==> evalcomplexstart(A,B,C,D,E) = 31 + -1*A >= 31 + -1*A = evalcomplexentryin(A,B,C,D,E) True ==> evalcomplexentryin(A,B,C,D,E) = 31 + -1*A >= 31 + -1*A = evalcomplexbb10in(B,A,C,D,E) [B >= 30] ==> evalcomplexbb10in(A,B,C,D,E) = 31 + -1*B >= 31 + -1*B = evalcomplexreturnin(A,B,C,D,E) [29 >= B] ==> evalcomplexbb10in(A,B,C,D,E) = 31 + -1*B >= 31 + -1*B = evalcomplexbb8in(A,B,A,B,E) [-30 + B >= 0] ==> evalcomplexreturnin(A,B,C,D,E) = 31 + -1*B >= 31 + -1*B = evalcomplexstop(A,B,C,D,E) [-1*B + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && D >= 1 + C] ==> evalcomplexbb8in(A,B,C,D,E) = 31 + -1*B >= 31 + -1*B = evalcomplexbb1in(A,B,C,D,E) [-1 + -1*C + D >= 0 ==> && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && 5 >= C && 7 >= C] evalcomplexbb1in(A,B,C,D,E) = 31 + -1*B >= 31 + -1*B = evalcomplexbb7in(A,B,C,D,2 + C) [-1 + -1*C + D >= 0 && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && C >= 6] ==> evalcomplexbb1in(A,B,C,D,E) = 31 + -1*B >= 31 + -1*B = evalcomplexbb7in(A,B,C,D,7 + C) [6 + D + -1*E >= 0 ==> && 7 + C + -1*E >= 0 && -2 + -1*C + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*C + D >= 0 && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0] evalcomplexbb7in(A,B,C,D,E) = 31 + -1*B >= 31 + -1*B = evalcomplexbb8in(A,B,E,1 + D,E) * Step 4: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalcomplexstart(A,B,C,D,E) -> evalcomplexentryin(A,B,C,D,E) True (1,1) 1. evalcomplexentryin(A,B,C,D,E) -> evalcomplexbb10in(B,A,C,D,E) True (1,1) 2. evalcomplexbb10in(A,B,C,D,E) -> evalcomplexreturnin(A,B,C,D,E) [B >= 30] (1,1) 3. evalcomplexbb10in(A,B,C,D,E) -> evalcomplexbb8in(A,B,A,B,E) [29 >= B] (?,1) 4. evalcomplexreturnin(A,B,C,D,E) -> evalcomplexstop(A,B,C,D,E) [-30 + B >= 0] (1,1) 5. evalcomplexbb8in(A,B,C,D,E) -> evalcomplexbb9in(A,B,C,D,E) [-1*B + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && C >= D] (31 + A,1) 6. evalcomplexbb8in(A,B,C,D,E) -> evalcomplexbb1in(A,B,C,D,E) [-1*B + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && D >= 1 + C] (?,1) 7. evalcomplexbb9in(A,B,C,D,E) -> evalcomplexbb10in(-10 + C,2 + D,C,D,E) [C + -1*D >= 0 && -1*B + D >= 0 && -1*B + C >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0] (31 + A,1) 8. evalcomplexbb1in(A,B,C,D,E) -> evalcomplexbb7in(A,B,C,D,2 + C) [-1 + -1*C + D >= 0 (?,1) && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && 5 >= C && 7 >= C] 9. evalcomplexbb1in(A,B,C,D,E) -> evalcomplexbb7in(A,B,C,D,7 + C) [-1 + -1*C + D >= 0 && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && C >= 6] (?,1) 10. evalcomplexbb7in(A,B,C,D,E) -> evalcomplexbb8in(A,B,E,1 + D,E) [6 + D + -1*E >= 0 (179 + 5*A + B,1) && 7 + C + -1*E >= 0 && -2 + -1*C + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*C + D >= 0 && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0] Signature: {(evalcomplexbb10in,5) ;(evalcomplexbb1in,5) ;(evalcomplexbb7in,5) ;(evalcomplexbb8in,5) ;(evalcomplexbb9in,5) ;(evalcomplexentryin,5) ;(evalcomplexreturnin,5) ;(evalcomplexstart,5) ;(evalcomplexstop,5)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{5,6},4->{},5->{7},6->{8,9},7->{2,3},8->{10},9->{10},10->{5,6}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 5: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalcomplexstart(A,B,C,D,E) -> evalcomplexentryin(A,B,C,D,E) True (1,1) 1. evalcomplexentryin(A,B,C,D,E) -> evalcomplexbb10in(B,A,C,D,E) True (1,1) 2. evalcomplexbb10in(A,B,C,D,E) -> evalcomplexreturnin(A,B,C,D,E) [B >= 30] (1,1) 3. evalcomplexbb10in(A,B,C,D,E) -> evalcomplexbb8in(A,B,A,B,E) [29 >= B] (32 + A,1) 4. evalcomplexreturnin(A,B,C,D,E) -> evalcomplexstop(A,B,C,D,E) [-30 + B >= 0] (1,1) 5. evalcomplexbb8in(A,B,C,D,E) -> evalcomplexbb9in(A,B,C,D,E) [-1*B + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && C >= D] (31 + A,1) 6. evalcomplexbb8in(A,B,C,D,E) -> evalcomplexbb1in(A,B,C,D,E) [-1*B + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && D >= 1 + C] (211 + 6*A + B,1) 7. evalcomplexbb9in(A,B,C,D,E) -> evalcomplexbb10in(-10 + C,2 + D,C,D,E) [C + -1*D >= 0 && -1*B + D >= 0 && -1*B + C >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0] (31 + A,1) 8. evalcomplexbb1in(A,B,C,D,E) -> evalcomplexbb7in(A,B,C,D,2 + C) [-1 + -1*C + D >= 0 (211 + 6*A + B,1) && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && 5 >= C && 7 >= C] 9. evalcomplexbb1in(A,B,C,D,E) -> evalcomplexbb7in(A,B,C,D,7 + C) [-1 + -1*C + D >= 0 && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0 && C >= 6] (211 + 6*A + B,1) 10. evalcomplexbb7in(A,B,C,D,E) -> evalcomplexbb8in(A,B,E,1 + D,E) [6 + D + -1*E >= 0 (179 + 5*A + B,1) && 7 + C + -1*E >= 0 && -2 + -1*C + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*C + D >= 0 && -1*B + D >= 0 && -1 + -1*A + D >= 0 && -1*A + C >= 0 && 29 + -1*B >= 0] Signature: {(evalcomplexbb10in,5) ;(evalcomplexbb1in,5) ;(evalcomplexbb7in,5) ;(evalcomplexbb8in,5) ;(evalcomplexbb9in,5) ;(evalcomplexentryin,5) ;(evalcomplexreturnin,5) ;(evalcomplexstart,5) ;(evalcomplexstop,5)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{5,6},4->{},5->{7},6->{8,9},7->{2,3},8->{10},9->{10},10->{5,6}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: The problem is already solved. YES(?,O(n^1))