YES(?,O(n^1)) * Step 1: TrivialSCCs WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (?,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (?,1) 3. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplereturnin(A,B,C,D,E) [B >= A] (?,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0] (?,1) 11. evalNestedMultiplereturnin(A,B,C,D,E) -> evalNestedMultiplestop(A,B,C,D,E) [-1*A + B >= 0] (?,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2,3},11->{}] + 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. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (1,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (?,1) 3. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplereturnin(A,B,C,D,E) [B >= A] (1,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0] (?,1) 11. evalNestedMultiplereturnin(A,B,C,D,E) -> evalNestedMultiplestop(A,B,C,D,E) [-1*A + B >= 0] (1,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2,3},11->{}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalNestedMultiplebb1in) = x1 + -1*x2 p(evalNestedMultiplebb2in) = x1 + -1*x2 p(evalNestedMultiplebb3in) = x1 + -1*x2 p(evalNestedMultiplebb4in) = x1 + -1*x2 p(evalNestedMultiplebb5in) = x1 + -1*x2 p(evalNestedMultipleentryin) = -1*x1 + x2 p(evalNestedMultiplereturnin) = x1 + -1*x2 p(evalNestedMultiplestart) = -1*x1 + x2 p(evalNestedMultiplestop) = x1 + -1*x2 Following rules are strictly oriented: [-1*D + E >= 0 && -1 + A + -1*B >= 0] ==> evalNestedMultiplebb4in(A,B,C,D,E) = A + -1*B > -1 + A + -1*B = evalNestedMultiplebb5in(A,1 + B,C,E,E) Following rules are weakly oriented: True ==> evalNestedMultiplestart(A,B,C,D,E) = -1*A + B >= -1*A + B = evalNestedMultipleentryin(A,B,C,D,E) True ==> evalNestedMultipleentryin(A,B,C,D,E) = -1*A + B >= -1*A + B = evalNestedMultiplebb5in(B,A,D,C,E) [A >= 1 + B] ==> evalNestedMultiplebb5in(A,B,C,D,E) = A + -1*B >= A + -1*B = evalNestedMultiplebb2in(A,B,C,D,D) [B >= A] ==> evalNestedMultiplebb5in(A,B,C,D,E) = A + -1*B >= A + -1*B = evalNestedMultiplereturnin(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && E >= C] ==> evalNestedMultiplebb2in(A,B,C,D,E) = A + -1*B >= A + -1*B = evalNestedMultiplebb4in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && C >= 1 + E] ==> evalNestedMultiplebb2in(A,B,C,D,E) = A + -1*B >= A + -1*B = evalNestedMultiplebb3in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + F] ==> evalNestedMultiplebb3in(A,B,C,D,E) = A + -1*B >= A + -1*B = evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && F >= 1] ==> evalNestedMultiplebb3in(A,B,C,D,E) = A + -1*B >= A + -1*B = evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] ==> evalNestedMultiplebb3in(A,B,C,D,E) = A + -1*B >= A + -1*B = evalNestedMultiplebb4in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] ==> evalNestedMultiplebb1in(A,B,C,D,E) = A + -1*B >= A + -1*B = evalNestedMultiplebb2in(A,B,C,D,1 + E) [-1*A + B >= 0] ==> evalNestedMultiplereturnin(A,B,C,D,E) = A + -1*B >= A + -1*B = evalNestedMultiplestop(A,B,C,D,E) * Step 3: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (1,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (?,1) 3. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplereturnin(A,B,C,D,E) [B >= A] (1,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0] (A + B,1) 11. evalNestedMultiplereturnin(A,B,C,D,E) -> evalNestedMultiplestop(A,B,C,D,E) [-1*A + B >= 0] (1,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2,3},11->{}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 4: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (1,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (1 + A + B,1) 3. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplereturnin(A,B,C,D,E) [B >= A] (1,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0] (A + B,1) 11. evalNestedMultiplereturnin(A,B,C,D,E) -> evalNestedMultiplestop(A,B,C,D,E) [-1*A + B >= 0] (1,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2,3},11->{}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalNestedMultiplebb1in) = x3 + -1*x5 p(evalNestedMultiplebb2in) = x3 + -1*x5 p(evalNestedMultiplebb3in) = x3 + -1*x5 p(evalNestedMultiplebb4in) = x3 + -1*x5 p(evalNestedMultiplebb5in) = x3 + -1*x4 p(evalNestedMultipleentryin) = -1*x3 + x4 p(evalNestedMultiplereturnin) = x3 + -1*x4 p(evalNestedMultiplestart) = -1*x3 + x4 p(evalNestedMultiplestop) = x3 + -1*x4 Following rules are strictly oriented: [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] ==> evalNestedMultiplebb1in(A,B,C,D,E) = C + -1*E > -1 + C + -1*E = evalNestedMultiplebb2in(A,B,C,D,1 + E) Following rules are weakly oriented: True ==> evalNestedMultiplestart(A,B,C,D,E) = -1*C + D >= -1*C + D = evalNestedMultipleentryin(A,B,C,D,E) True ==> evalNestedMultipleentryin(A,B,C,D,E) = -1*C + D >= -1*C + D = evalNestedMultiplebb5in(B,A,D,C,E) [A >= 1 + B] ==> evalNestedMultiplebb5in(A,B,C,D,E) = C + -1*D >= C + -1*D = evalNestedMultiplebb2in(A,B,C,D,D) [B >= A] ==> evalNestedMultiplebb5in(A,B,C,D,E) = C + -1*D >= C + -1*D = evalNestedMultiplereturnin(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && E >= C] ==> evalNestedMultiplebb2in(A,B,C,D,E) = C + -1*E >= C + -1*E = evalNestedMultiplebb4in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && C >= 1 + E] ==> evalNestedMultiplebb2in(A,B,C,D,E) = C + -1*E >= C + -1*E = evalNestedMultiplebb3in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + F] ==> evalNestedMultiplebb3in(A,B,C,D,E) = C + -1*E >= C + -1*E = evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && F >= 1] ==> evalNestedMultiplebb3in(A,B,C,D,E) = C + -1*E >= C + -1*E = evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] ==> evalNestedMultiplebb3in(A,B,C,D,E) = C + -1*E >= C + -1*E = evalNestedMultiplebb4in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0] ==> evalNestedMultiplebb4in(A,B,C,D,E) = C + -1*E >= C + -1*E = evalNestedMultiplebb5in(A,1 + B,C,E,E) [-1*A + B >= 0] ==> evalNestedMultiplereturnin(A,B,C,D,E) = C + -1*D >= C + -1*D = evalNestedMultiplestop(A,B,C,D,E) * Step 5: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (1,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (1 + A + B,1) 3. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplereturnin(A,B,C,D,E) [B >= A] (1,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] (C + D,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0] (A + B,1) 11. evalNestedMultiplereturnin(A,B,C,D,E) -> evalNestedMultiplestop(A,B,C,D,E) [-1*A + B >= 0] (1,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2,3},11->{}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 6: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (1,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (1 + A + B,1) 3. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplereturnin(A,B,C,D,E) [B >= A] (1,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && E >= C] (1 + A + B + C + D,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && C >= 1 + E] (1 + A + B + C + D,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + F] (1 + A + B + C + D,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && F >= 1] (1 + A + B + C + D,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] (1 + A + B + C + D,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] (C + D,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0] (A + B,1) 11. evalNestedMultiplereturnin(A,B,C,D,E) -> evalNestedMultiplestop(A,B,C,D,E) [-1*A + B >= 0] (1,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2,3},11->{}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: The problem is already solved. YES(?,O(n^1))