YES(?,O(n^1)) * Step 1: TrivialSCCs WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval_start_start(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb0_in(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 1. eval_start_bb0_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_0(v__0,v__01,v__1,v_1,v_n,v_y) True (?,1) 2. eval_start_0(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_1(v__0,v__01,v__1,v_1,v_n,v_y) True (?,1) 3. eval_start_1(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_2(v__0,v__01,v__1,v_1,v_n,v_y) True (?,1) 4. eval_start_2(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_3(v__0,v__01,v__1,v_1,v_n,v_y) True (?,1) 5. eval_start_3(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_4(v__0,v__01,v__1,v_1,v_n,v_y) True (?,1) 6. eval_start_4(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_5(v__0,v__01,v__1,v_1,v_n,v_y) True (?,1) 7. eval_start_5(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb1_in(v_n,v_y,v__1,v_1,v_n,v_y) True (?,1) 8. eval_start_bb1_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb2_in(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && -1 >= v__0] (?,1) 9. eval_start_bb1_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb5_in(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && v__0 >= 0] (?,1) 10. eval_start_bb2_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb3_in(v__0,v__01,1000 + v__01,1 + v__0,v_n,v_y) [-1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1 + -1*v__0 >= 0] (?,1) 11. eval_start_bb3_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb4_in(v__0,v__01,v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 (?,1) && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -1 + -1*v__0 >= 0 && v__1 >= 100] 12. eval_start_bb3_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb1_in(v_1,v__1,v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 (?,1) && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -1 + -1*v__0 >= 0 && 99 >= v__1] 13. eval_start_bb4_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb3_in(v__0,v__01,-100 + v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 (?,1) && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && -101 + v__1 + -1*v_n >= 0 && 899 + v__01 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && -100 + -1*v_1 + v__1 >= 0 && 900 + -1*v_1 + v__01 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -100 + v__1 >= 0 && 800 + v__01 + v__1 >= 0 && -101 + -1*v__0 + v__1 >= 0 && 900 + v__01 >= 0 && 899 + -1*v__0 + v__01 >= 0 && -1 + -1*v__0 >= 0] 14. eval_start_bb5_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_stop(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && v__0 >= 0] (?,1) Signature: {(eval_start_0,6) ;(eval_start_1,6) ;(eval_start_2,6) ;(eval_start_3,6) ;(eval_start_4,6) ;(eval_start_5,6) ;(eval_start_bb0_in,6) ;(eval_start_bb1_in,6) ;(eval_start_bb2_in,6) ;(eval_start_bb3_in,6) ;(eval_start_bb4_in,6) ;(eval_start_bb5_in,6) ;(eval_start_start,6) ;(eval_start_stop,6)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8,9},8->{10},9->{14},10->{11,12},11->{13},12->{8,9} ,13->{11,12},14->{}] + 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. eval_start_start(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb0_in(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 1. eval_start_bb0_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_0(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 2. eval_start_0(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_1(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 3. eval_start_1(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_2(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 4. eval_start_2(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_3(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 5. eval_start_3(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_4(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 6. eval_start_4(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_5(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 7. eval_start_5(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb1_in(v_n,v_y,v__1,v_1,v_n,v_y) True (1,1) 8. eval_start_bb1_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb2_in(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && -1 >= v__0] (?,1) 9. eval_start_bb1_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb5_in(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && v__0 >= 0] (1,1) 10. eval_start_bb2_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb3_in(v__0,v__01,1000 + v__01,1 + v__0,v_n,v_y) [-1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1 + -1*v__0 >= 0] (?,1) 11. eval_start_bb3_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb4_in(v__0,v__01,v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 (?,1) && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -1 + -1*v__0 >= 0 && v__1 >= 100] 12. eval_start_bb3_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb1_in(v_1,v__1,v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 (?,1) && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -1 + -1*v__0 >= 0 && 99 >= v__1] 13. eval_start_bb4_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb3_in(v__0,v__01,-100 + v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 (?,1) && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && -101 + v__1 + -1*v_n >= 0 && 899 + v__01 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && -100 + -1*v_1 + v__1 >= 0 && 900 + -1*v_1 + v__01 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -100 + v__1 >= 0 && 800 + v__01 + v__1 >= 0 && -101 + -1*v__0 + v__1 >= 0 && 900 + v__01 >= 0 && 899 + -1*v__0 + v__01 >= 0 && -1 + -1*v__0 >= 0] 14. eval_start_bb5_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_stop(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && v__0 >= 0] (1,1) Signature: {(eval_start_0,6) ;(eval_start_1,6) ;(eval_start_2,6) ;(eval_start_3,6) ;(eval_start_4,6) ;(eval_start_5,6) ;(eval_start_bb0_in,6) ;(eval_start_bb1_in,6) ;(eval_start_bb2_in,6) ;(eval_start_bb3_in,6) ;(eval_start_bb4_in,6) ;(eval_start_bb5_in,6) ;(eval_start_start,6) ;(eval_start_stop,6)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8,9},8->{10},9->{14},10->{11,12},11->{13},12->{8,9} ,13->{11,12},14->{}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(eval_start_0) = 900 + -3000*x5 + 3*x6 p(eval_start_1) = 900 + -3000*x5 + 3*x6 p(eval_start_2) = 900 + -3000*x5 + 3*x6 p(eval_start_3) = 900 + -3000*x5 + 3*x6 p(eval_start_4) = 900 + -3000*x5 + 3*x6 p(eval_start_5) = 900 + -3000*x5 + 3*x6 p(eval_start_bb0_in) = 900 + -3000*x5 + 3*x6 p(eval_start_bb1_in) = 900 + -3000*x1 + 3*x2 p(eval_start_bb2_in) = 900 + -3000*x1 + 3*x2 p(eval_start_bb3_in) = -100 + -3000*x1 + 2*x2 + x3 p(eval_start_bb4_in) = -199 + -3000*x1 + 2*x2 + x3 p(eval_start_bb5_in) = 900 + -3000*x1 + 3*x2 p(eval_start_start) = 900 + -3000*x5 + 3*x6 p(eval_start_stop) = 900 + -3000*x1 + 3*x2 Following rules are strictly oriented: [-1 + -1*v_n >= 0 ==> && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && -101 + v__1 + -1*v_n >= 0 && 899 + v__01 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && -100 + -1*v_1 + v__1 >= 0 && 900 + -1*v_1 + v__01 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -100 + v__1 >= 0 && 800 + v__01 + v__1 >= 0 && -101 + -1*v__0 + v__1 >= 0 && 900 + v__01 >= 0 && 899 + -1*v__0 + v__01 >= 0 && -1 + -1*v__0 >= 0] eval_start_bb4_in(v__0,v__01,v__1,v_1,v_n,v_y) = -199 + -3000*v__0 + 2*v__01 + v__1 > -200 + -3000*v__0 + 2*v__01 + v__1 = eval_start_bb3_in(v__0,v__01,-100 + v__1,v_1,v_n,v_y) Following rules are weakly oriented: True ==> eval_start_start(v__0,v__01,v__1,v_1,v_n,v_y) = 900 + -3000*v_n + 3*v_y >= 900 + -3000*v_n + 3*v_y = eval_start_bb0_in(v__0,v__01,v__1,v_1,v_n,v_y) True ==> eval_start_bb0_in(v__0,v__01,v__1,v_1,v_n,v_y) = 900 + -3000*v_n + 3*v_y >= 900 + -3000*v_n + 3*v_y = eval_start_0(v__0,v__01,v__1,v_1,v_n,v_y) True ==> eval_start_0(v__0,v__01,v__1,v_1,v_n,v_y) = 900 + -3000*v_n + 3*v_y >= 900 + -3000*v_n + 3*v_y = eval_start_1(v__0,v__01,v__1,v_1,v_n,v_y) True ==> eval_start_1(v__0,v__01,v__1,v_1,v_n,v_y) = 900 + -3000*v_n + 3*v_y >= 900 + -3000*v_n + 3*v_y = eval_start_2(v__0,v__01,v__1,v_1,v_n,v_y) True ==> eval_start_2(v__0,v__01,v__1,v_1,v_n,v_y) = 900 + -3000*v_n + 3*v_y >= 900 + -3000*v_n + 3*v_y = eval_start_3(v__0,v__01,v__1,v_1,v_n,v_y) True ==> eval_start_3(v__0,v__01,v__1,v_1,v_n,v_y) = 900 + -3000*v_n + 3*v_y >= 900 + -3000*v_n + 3*v_y = eval_start_4(v__0,v__01,v__1,v_1,v_n,v_y) True ==> eval_start_4(v__0,v__01,v__1,v_1,v_n,v_y) = 900 + -3000*v_n + 3*v_y >= 900 + -3000*v_n + 3*v_y = eval_start_5(v__0,v__01,v__1,v_1,v_n,v_y) True ==> eval_start_5(v__0,v__01,v__1,v_1,v_n,v_y) = 900 + -3000*v_n + 3*v_y >= 900 + -3000*v_n + 3*v_y = eval_start_bb1_in(v_n,v_y,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && -1 >= v__0] ==> eval_start_bb1_in(v__0,v__01,v__1,v_1,v_n,v_y) = 900 + -3000*v__0 + 3*v__01 >= 900 + -3000*v__0 + 3*v__01 = eval_start_bb2_in(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && v__0 >= 0] ==> eval_start_bb1_in(v__0,v__01,v__1,v_1,v_n,v_y) = 900 + -3000*v__0 + 3*v__01 >= 900 + -3000*v__0 + 3*v__01 = eval_start_bb5_in(v__0,v__01,v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1 + -1*v__0 >= 0] ==> eval_start_bb2_in(v__0,v__01,v__1,v_1,v_n,v_y) = 900 + -3000*v__0 + 3*v__01 >= 900 + -3000*v__0 + 3*v__01 = eval_start_bb3_in(v__0,v__01,1000 + v__01,1 + v__0,v_n,v_y) [-1 + -1*v_n >= 0 ==> && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -1 + -1*v__0 >= 0 && v__1 >= 100] eval_start_bb3_in(v__0,v__01,v__1,v_1,v_n,v_y) = -100 + -3000*v__0 + 2*v__01 + v__1 >= -199 + -3000*v__0 + 2*v__01 + v__1 = eval_start_bb4_in(v__0,v__01,v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 ==> && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -1 + -1*v__0 >= 0 && 99 >= v__1] eval_start_bb3_in(v__0,v__01,v__1,v_1,v_n,v_y) = -100 + -3000*v__0 + 2*v__01 + v__1 >= 900 + -3000*v_1 + 3*v__1 = eval_start_bb1_in(v_1,v__1,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && v__0 >= 0] ==> eval_start_bb5_in(v__0,v__01,v__1,v_1,v_n,v_y) = 900 + -3000*v__0 + 3*v__01 >= 900 + -3000*v__0 + 3*v__01 = eval_start_stop(v__0,v__01,v__1,v_1,v_n,v_y) * Step 3: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval_start_start(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb0_in(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 1. eval_start_bb0_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_0(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 2. eval_start_0(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_1(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 3. eval_start_1(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_2(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 4. eval_start_2(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_3(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 5. eval_start_3(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_4(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 6. eval_start_4(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_5(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 7. eval_start_5(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb1_in(v_n,v_y,v__1,v_1,v_n,v_y) True (1,1) 8. eval_start_bb1_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb2_in(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && -1 >= v__0] (?,1) 9. eval_start_bb1_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb5_in(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && v__0 >= 0] (1,1) 10. eval_start_bb2_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb3_in(v__0,v__01,1000 + v__01,1 + v__0,v_n,v_y) [-1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1 + -1*v__0 >= 0] (?,1) 11. eval_start_bb3_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb4_in(v__0,v__01,v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 (?,1) && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -1 + -1*v__0 >= 0 && v__1 >= 100] 12. eval_start_bb3_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb1_in(v_1,v__1,v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 (?,1) && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -1 + -1*v__0 >= 0 && 99 >= v__1] 13. eval_start_bb4_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb3_in(v__0,v__01,-100 + v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 (900 + 3000*v_n + 3*v_y,1) && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && -101 + v__1 + -1*v_n >= 0 && 899 + v__01 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && -100 + -1*v_1 + v__1 >= 0 && 900 + -1*v_1 + v__01 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -100 + v__1 >= 0 && 800 + v__01 + v__1 >= 0 && -101 + -1*v__0 + v__1 >= 0 && 900 + v__01 >= 0 && 899 + -1*v__0 + v__01 >= 0 && -1 + -1*v__0 >= 0] 14. eval_start_bb5_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_stop(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && v__0 >= 0] (1,1) Signature: {(eval_start_0,6) ;(eval_start_1,6) ;(eval_start_2,6) ;(eval_start_3,6) ;(eval_start_4,6) ;(eval_start_5,6) ;(eval_start_bb0_in,6) ;(eval_start_bb1_in,6) ;(eval_start_bb2_in,6) ;(eval_start_bb3_in,6) ;(eval_start_bb4_in,6) ;(eval_start_bb5_in,6) ;(eval_start_start,6) ;(eval_start_stop,6)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8,9},8->{10},9->{14},10->{11,12},11->{13},12->{8,9} ,13->{11,12},14->{}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(eval_start_0) = -1*x5 p(eval_start_1) = -1*x5 p(eval_start_2) = -1*x5 p(eval_start_3) = -1*x5 p(eval_start_4) = -1*x5 p(eval_start_5) = -1*x5 p(eval_start_bb0_in) = -1*x5 p(eval_start_bb1_in) = -1*x1 p(eval_start_bb2_in) = -1*x1 p(eval_start_bb3_in) = -1*x1 p(eval_start_bb4_in) = -1*x1 p(eval_start_bb5_in) = -1*x1 p(eval_start_start) = -1*x5 p(eval_start_stop) = -1*x1 Following rules are strictly oriented: [-1 + -1*v_n >= 0 ==> && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -1 + -1*v__0 >= 0 && 99 >= v__1] eval_start_bb3_in(v__0,v__01,v__1,v_1,v_n,v_y) = -1*v__0 > -1*v_1 = eval_start_bb1_in(v_1,v__1,v__1,v_1,v_n,v_y) Following rules are weakly oriented: True ==> eval_start_start(v__0,v__01,v__1,v_1,v_n,v_y) = -1*v_n >= -1*v_n = eval_start_bb0_in(v__0,v__01,v__1,v_1,v_n,v_y) True ==> eval_start_bb0_in(v__0,v__01,v__1,v_1,v_n,v_y) = -1*v_n >= -1*v_n = eval_start_0(v__0,v__01,v__1,v_1,v_n,v_y) True ==> eval_start_0(v__0,v__01,v__1,v_1,v_n,v_y) = -1*v_n >= -1*v_n = eval_start_1(v__0,v__01,v__1,v_1,v_n,v_y) True ==> eval_start_1(v__0,v__01,v__1,v_1,v_n,v_y) = -1*v_n >= -1*v_n = eval_start_2(v__0,v__01,v__1,v_1,v_n,v_y) True ==> eval_start_2(v__0,v__01,v__1,v_1,v_n,v_y) = -1*v_n >= -1*v_n = eval_start_3(v__0,v__01,v__1,v_1,v_n,v_y) True ==> eval_start_3(v__0,v__01,v__1,v_1,v_n,v_y) = -1*v_n >= -1*v_n = eval_start_4(v__0,v__01,v__1,v_1,v_n,v_y) True ==> eval_start_4(v__0,v__01,v__1,v_1,v_n,v_y) = -1*v_n >= -1*v_n = eval_start_5(v__0,v__01,v__1,v_1,v_n,v_y) True ==> eval_start_5(v__0,v__01,v__1,v_1,v_n,v_y) = -1*v_n >= -1*v_n = eval_start_bb1_in(v_n,v_y,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && -1 >= v__0] ==> eval_start_bb1_in(v__0,v__01,v__1,v_1,v_n,v_y) = -1*v__0 >= -1*v__0 = eval_start_bb2_in(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && v__0 >= 0] ==> eval_start_bb1_in(v__0,v__01,v__1,v_1,v_n,v_y) = -1*v__0 >= -1*v__0 = eval_start_bb5_in(v__0,v__01,v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1 + -1*v__0 >= 0] ==> eval_start_bb2_in(v__0,v__01,v__1,v_1,v_n,v_y) = -1*v__0 >= -1*v__0 = eval_start_bb3_in(v__0,v__01,1000 + v__01,1 + v__0,v_n,v_y) [-1 + -1*v_n >= 0 ==> && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -1 + -1*v__0 >= 0 && v__1 >= 100] eval_start_bb3_in(v__0,v__01,v__1,v_1,v_n,v_y) = -1*v__0 >= -1*v__0 = eval_start_bb4_in(v__0,v__01,v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 ==> && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && -101 + v__1 + -1*v_n >= 0 && 899 + v__01 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && -100 + -1*v_1 + v__1 >= 0 && 900 + -1*v_1 + v__01 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -100 + v__1 >= 0 && 800 + v__01 + v__1 >= 0 && -101 + -1*v__0 + v__1 >= 0 && 900 + v__01 >= 0 && 899 + -1*v__0 + v__01 >= 0 && -1 + -1*v__0 >= 0] eval_start_bb4_in(v__0,v__01,v__1,v_1,v_n,v_y) = -1*v__0 >= -1*v__0 = eval_start_bb3_in(v__0,v__01,-100 + v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && v__0 >= 0] ==> eval_start_bb5_in(v__0,v__01,v__1,v_1,v_n,v_y) = -1*v__0 >= -1*v__0 = eval_start_stop(v__0,v__01,v__1,v_1,v_n,v_y) * Step 4: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval_start_start(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb0_in(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 1. eval_start_bb0_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_0(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 2. eval_start_0(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_1(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 3. eval_start_1(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_2(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 4. eval_start_2(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_3(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 5. eval_start_3(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_4(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 6. eval_start_4(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_5(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 7. eval_start_5(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb1_in(v_n,v_y,v__1,v_1,v_n,v_y) True (1,1) 8. eval_start_bb1_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb2_in(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && -1 >= v__0] (?,1) 9. eval_start_bb1_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb5_in(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && v__0 >= 0] (1,1) 10. eval_start_bb2_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb3_in(v__0,v__01,1000 + v__01,1 + v__0,v_n,v_y) [-1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1 + -1*v__0 >= 0] (?,1) 11. eval_start_bb3_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb4_in(v__0,v__01,v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 (?,1) && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -1 + -1*v__0 >= 0 && v__1 >= 100] 12. eval_start_bb3_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb1_in(v_1,v__1,v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 (v_n,1) && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -1 + -1*v__0 >= 0 && 99 >= v__1] 13. eval_start_bb4_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb3_in(v__0,v__01,-100 + v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 (900 + 3000*v_n + 3*v_y,1) && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && -101 + v__1 + -1*v_n >= 0 && 899 + v__01 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && -100 + -1*v_1 + v__1 >= 0 && 900 + -1*v_1 + v__01 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -100 + v__1 >= 0 && 800 + v__01 + v__1 >= 0 && -101 + -1*v__0 + v__1 >= 0 && 900 + v__01 >= 0 && 899 + -1*v__0 + v__01 >= 0 && -1 + -1*v__0 >= 0] 14. eval_start_bb5_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_stop(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && v__0 >= 0] (1,1) Signature: {(eval_start_0,6) ;(eval_start_1,6) ;(eval_start_2,6) ;(eval_start_3,6) ;(eval_start_4,6) ;(eval_start_5,6) ;(eval_start_bb0_in,6) ;(eval_start_bb1_in,6) ;(eval_start_bb2_in,6) ;(eval_start_bb3_in,6) ;(eval_start_bb4_in,6) ;(eval_start_bb5_in,6) ;(eval_start_start,6) ;(eval_start_stop,6)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8,9},8->{10},9->{14},10->{11,12},11->{13},12->{8,9} ,13->{11,12},14->{}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 5: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval_start_start(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb0_in(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 1. eval_start_bb0_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_0(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 2. eval_start_0(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_1(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 3. eval_start_1(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_2(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 4. eval_start_2(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_3(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 5. eval_start_3(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_4(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 6. eval_start_4(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_5(v__0,v__01,v__1,v_1,v_n,v_y) True (1,1) 7. eval_start_5(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb1_in(v_n,v_y,v__1,v_1,v_n,v_y) True (1,1) 8. eval_start_bb1_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb2_in(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && -1 >= v__0] (1 + v_n,1) 9. eval_start_bb1_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb5_in(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && v__0 >= 0] (1,1) 10. eval_start_bb2_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb3_in(v__0,v__01,1000 + v__01,1 + v__0,v_n,v_y) [-1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1 + -1*v__0 >= 0] (1 + v_n,1) 11. eval_start_bb3_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb4_in(v__0,v__01,v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 (901 + 3001*v_n + 3*v_y,1) && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -1 + -1*v__0 >= 0 && v__1 >= 100] 12. eval_start_bb3_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb1_in(v_1,v__1,v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 (v_n,1) && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -1 + -1*v__0 >= 0 && 99 >= v__1] 13. eval_start_bb4_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_bb3_in(v__0,v__01,-100 + v__1,v_1,v_n,v_y) [-1 + -1*v_n >= 0 (900 + 3000*v_n + 3*v_y,1) && -1 + v_1 + -1*v_n >= 0 && -1 + -1*v_1 + -1*v_n >= 0 && -101 + v__1 + -1*v_n >= 0 && 899 + v__01 + -1*v_n >= 0 && v__0 + -1*v_n >= 0 && -2 + -1*v__0 + -1*v_n >= 0 && -1*v_1 >= 0 && -100 + -1*v_1 + v__1 >= 0 && 900 + -1*v_1 + v__01 >= 0 && 1 + -1*v_1 + v__0 >= 0 && -1 + -1*v_1 + -1*v__0 >= 0 && -1 + v_1 + -1*v__0 >= 0 && 1000 + v__01 + -1*v__1 >= 0 && -100 + v__1 >= 0 && 800 + v__01 + v__1 >= 0 && -101 + -1*v__0 + v__1 >= 0 && 900 + v__01 >= 0 && 899 + -1*v__0 + v__01 >= 0 && -1 + -1*v__0 >= 0] 14. eval_start_bb5_in(v__0,v__01,v__1,v_1,v_n,v_y) -> eval_start_stop(v__0,v__01,v__1,v_1,v_n,v_y) [v__0 + -1*v_n >= 0 && v__0 >= 0] (1,1) Signature: {(eval_start_0,6) ;(eval_start_1,6) ;(eval_start_2,6) ;(eval_start_3,6) ;(eval_start_4,6) ;(eval_start_5,6) ;(eval_start_bb0_in,6) ;(eval_start_bb1_in,6) ;(eval_start_bb2_in,6) ;(eval_start_bb3_in,6) ;(eval_start_bb4_in,6) ;(eval_start_bb5_in,6) ;(eval_start_start,6) ;(eval_start_stop,6)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8,9},8->{10},9->{14},10->{11,12},11->{13},12->{8,9} ,13->{11,12},14->{}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: The problem is already solved. YES(?,O(n^1))