WORST_CASE(?, O(n^2)) Initial complexity problem: 1: T: (Comp: ?, Cost: 1) eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, 1, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1)) (Comp: ?, Cost: 1) eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Repeatedly propagating knowledge in problem 1 produces the following problem: 2: T: (Comp: 1, Cost: 1) eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, 1, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1)) (Comp: ?, Cost: 1) eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(eval_ex2_start) = 2 Pol(eval_ex2_bb0_in) = 2 Pol(eval_ex2_0) = 2 Pol(eval_ex2_1) = 2 Pol(eval_ex2_2) = 2 Pol(eval_ex2_3) = 2 Pol(eval_ex2_4) = 2 Pol(eval_ex2_bb1_in) = 2 Pol(eval_ex2_bb2_in) = 2 Pol(eval_ex2_bb5_in) = 1 Pol(eval_ex2_bb3_in) = 2 Pol(eval_ex2_bb4_in) = 2 Pol(eval_ex2_5) = 2 Pol(eval_ex2_6) = 2 Pol(eval_ex2_9) = 2 Pol(eval_ex2_10) = 2 Pol(eval_ex2_stop) = 0 Pol(koat_start) = 2 orients all transitions weakly and the transition eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3)) strictly and produces the following problem: 3: T: (Comp: 1, Cost: 1) eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, 1, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1)) (Comp: ?, Cost: 1) eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3)) (Comp: 2, Cost: 1) eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(eval_ex2_start) = 1 Pol(eval_ex2_bb0_in) = 1 Pol(eval_ex2_0) = 1 Pol(eval_ex2_1) = 1 Pol(eval_ex2_2) = 1 Pol(eval_ex2_3) = 1 Pol(eval_ex2_4) = 1 Pol(eval_ex2_bb1_in) = 1 Pol(eval_ex2_bb2_in) = 1 Pol(eval_ex2_bb5_in) = 0 Pol(eval_ex2_bb3_in) = 1 Pol(eval_ex2_bb4_in) = 1 Pol(eval_ex2_5) = 1 Pol(eval_ex2_6) = 1 Pol(eval_ex2_9) = 1 Pol(eval_ex2_10) = 1 Pol(eval_ex2_stop) = 0 Pol(koat_start) = 1 orients all transitions weakly and the transition eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ] strictly and produces the following problem: 4: T: (Comp: 1, Cost: 1) eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, 1, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ] (Comp: 1, Cost: 1) eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1)) (Comp: ?, Cost: 1) eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3)) (Comp: 2, Cost: 1) eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(eval_ex2_start) = 6*V_2 Pol(eval_ex2_bb0_in) = 6*V_2 Pol(eval_ex2_0) = 6*V_2 Pol(eval_ex2_1) = 6*V_2 Pol(eval_ex2_2) = 6*V_2 Pol(eval_ex2_3) = 6*V_2 Pol(eval_ex2_4) = 6*V_2 Pol(eval_ex2_bb1_in) = 6*V_2 - 6*V_3 + 1 Pol(eval_ex2_bb2_in) = 6*V_2 - 6*V_3 - 1 Pol(eval_ex2_bb5_in) = 6*V_2 - 6*V_3 + 1 Pol(eval_ex2_bb3_in) = 6*V_2 - 6*V_3 - 1 Pol(eval_ex2_bb4_in) = 6*V_2 - 6*V_3 - 2 Pol(eval_ex2_5) = 6*V_2 - 6*V_3 - 1 Pol(eval_ex2_6) = 6*V_2 - 6*V_3 - 1 Pol(eval_ex2_9) = -6*V_1 + 6*V_2 + 3 Pol(eval_ex2_10) = -6*V_1 + 6*V_2 + 2 Pol(eval_ex2_stop) = 6*V_2 - 6*V_3 + 1 Pol(koat_start) = 6*V_2 orients all transitions weakly and the transition eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ] strictly and produces the following problem: 5: T: (Comp: 1, Cost: 1) eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, 1, Ar_3)) (Comp: 6*Ar_1, Cost: 1) eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ] (Comp: 1, Cost: 1) eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1)) (Comp: ?, Cost: 1) eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3)) (Comp: 2, Cost: 1) eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(eval_ex2_bb4_in) = 3 Pol(eval_ex2_9) = 2 Pol(eval_ex2_bb3_in) = 4 Pol(eval_ex2_5) = 4 Pol(eval_ex2_bb2_in) = 4 Pol(eval_ex2_10) = 1 Pol(eval_ex2_6) = 4 Pol(eval_ex2_bb1_in) = 0 and size complexities S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3)) [ 0 <= 0 ]", 0-0) = Ar_0 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3)) [ 0 <= 0 ]", 0-1) = Ar_1 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3)) [ 0 <= 0 ]", 0-2) = Ar_2 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3)) [ 0 <= 0 ]", 0-3) = Ar_3 S("eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = ? S("eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = ? S("eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = ? S("eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3))", 0-0) = ? S("eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3))", 0-1) = Ar_1 S("eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3))", 0-2) = ? S("eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3))", 0-3) = ? S("eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = ? S("eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = ? S("eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = ? S("eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3))", 0-0) = ? S("eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3))", 0-2) = ? S("eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3))", 0-3) = ? S("eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1))", 0-0) = ? S("eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1))", 0-1) = Ar_1 S("eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1))", 0-2) = ? S("eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1))", 0-3) = ? S("eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = ? S("eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = ? S("eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = ? S("eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = ? S("eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = ? S("eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = ? S("eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ]", 0-0) = ? S("eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ]", 0-1) = Ar_1 S("eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ]", 0-2) = ? S("eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ]", 0-3) = ? S("eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ]", 0-0) = ? S("eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ]", 0-1) = Ar_1 S("eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ]", 0-2) = ? S("eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ]", 0-3) = ? S("eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ]", 0-0) = ? S("eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ]", 0-1) = Ar_1 S("eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ]", 0-2) = ? S("eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ]", 0-3) = ? S("eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ]", 0-0) = ? S("eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ]", 0-1) = Ar_1 S("eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ]", 0-2) = ? S("eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ]", 0-3) = ? S("eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, 1, Ar_3))", 0-0) = Ar_0 S("eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, 1, Ar_3))", 0-1) = Ar_1 S("eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, 1, Ar_3))", 0-2) = 1 S("eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, 1, Ar_3))", 0-3) = Ar_3 S("eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = Ar_0 S("eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = Ar_2 S("eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = Ar_3 S("eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = Ar_0 S("eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = Ar_2 S("eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = Ar_3 S("eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = Ar_0 S("eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = Ar_2 S("eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = Ar_3 S("eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = Ar_0 S("eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = Ar_2 S("eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = Ar_3 S("eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = Ar_0 S("eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = Ar_2 S("eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = Ar_3 S("eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = Ar_0 S("eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = Ar_2 S("eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = Ar_3 orients the transitions eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3)) eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3)) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ] eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ] eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3)) eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1)) eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3)) eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3)) weakly and the transitions eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3)) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ] eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3)) eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3)) strictly and produces the following problem: 6: T: (Comp: 1, Cost: 1) eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, 1, Ar_3)) (Comp: 6*Ar_1, Cost: 1) eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ] (Comp: 1, Cost: 1) eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ] (Comp: 24*Ar_1, Cost: 1) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1)) (Comp: 24*Ar_1, Cost: 1) eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3)) (Comp: 24*Ar_1, Cost: 1) eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 24*Ar_1, Cost: 1) eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3)) (Comp: 2, Cost: 1) eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(eval_ex2_bb3_in) = 4*V_2 - 4*V_4 Pol(eval_ex2_5) = 4*V_2 - 4*V_4 - 1 Pol(eval_ex2_bb2_in) = 4*V_2 - 4*V_4 + 1 Pol(eval_ex2_6) = 4*V_2 - 4*V_4 - 2 and size complexities S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3)) [ 0 <= 0 ]", 0-0) = Ar_0 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3)) [ 0 <= 0 ]", 0-1) = Ar_1 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3)) [ 0 <= 0 ]", 0-2) = Ar_2 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3)) [ 0 <= 0 ]", 0-3) = Ar_3 S("eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = 24*Ar_0 + 24*Ar_1 + 7962624 S("eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = 24*Ar_1 + 332352 S("eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = ? S("eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3))", 0-0) = 24*Ar_1 + 13824 S("eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3))", 0-1) = Ar_1 S("eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3))", 0-2) = 24*Ar_1 + 576 S("eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3))", 0-3) = ? S("eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = 24*Ar_1 + 576 S("eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = 24*Ar_1 + 331776 S("eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = ? S("eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3))", 0-0) = 24*Ar_1 + 576 S("eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3))", 0-2) = 24*Ar_1 + 13824 S("eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3))", 0-3) = ? S("eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1))", 0-0) = 24*Ar_0 + 24*Ar_1 + 7962624 S("eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1))", 0-1) = Ar_1 S("eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1))", 0-2) = 24*Ar_1 + 576 S("eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1))", 0-3) = ? S("eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = 24*Ar_0 + 24*Ar_1 + 7962624 S("eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = 24*Ar_1 + 576 S("eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = ? S("eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = 24*Ar_0 + 24*Ar_1 + 7962624 S("eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = 24*Ar_1 + 576 S("eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = ? S("eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ]", 0-0) = 24*Ar_0 + 24*Ar_1 + 191102976 S("eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ]", 0-1) = Ar_1 S("eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ]", 0-2) = 24*Ar_1 + 576 S("eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ]", 0-3) = ? S("eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ]", 0-0) = 24*Ar_0 + 24*Ar_1 + 7962624 S("eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ]", 0-1) = Ar_1 S("eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ]", 0-2) = 24*Ar_1 + 576 S("eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ]", 0-3) = ? S("eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ]", 0-0) = 24*Ar_0 + 24*Ar_1 + 331776 S("eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ]", 0-1) = Ar_1 S("eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ]", 0-2) = 24*Ar_1 + 13848 S("eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ]", 0-3) = ? S("eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ]", 0-0) = 24*Ar_0 + 24*Ar_1 + 331776 S("eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ]", 0-1) = Ar_1 S("eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ]", 0-2) = 24*Ar_1 + 576 S("eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ]", 0-3) = 24*Ar_1 + 13848 S("eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, 1, Ar_3))", 0-0) = Ar_0 S("eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, 1, Ar_3))", 0-1) = Ar_1 S("eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, 1, Ar_3))", 0-2) = 1 S("eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, 1, Ar_3))", 0-3) = Ar_3 S("eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = Ar_0 S("eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = Ar_2 S("eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = Ar_3 S("eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = Ar_0 S("eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = Ar_2 S("eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = Ar_3 S("eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = Ar_0 S("eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = Ar_2 S("eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = Ar_3 S("eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = Ar_0 S("eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = Ar_2 S("eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = Ar_3 S("eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = Ar_0 S("eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = Ar_2 S("eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = Ar_3 S("eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3))", 0-0) = Ar_0 S("eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3))", 0-1) = Ar_1 S("eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3))", 0-2) = Ar_2 S("eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3))", 0-3) = Ar_3 orients the transitions eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3)) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ] eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1)) eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3)) weakly and the transition eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ] strictly and produces the following problem: 7: T: (Comp: 1, Cost: 1) eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, 1, Ar_3)) (Comp: 6*Ar_1, Cost: 1) eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ] (Comp: 1, Cost: 1) eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ] (Comp: 600*Ar_1^2 + 332358*Ar_1, Cost: 1) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ] (Comp: 24*Ar_1, Cost: 1) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ] (Comp: ?, Cost: 1) eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: ?, Cost: 1) eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1)) (Comp: 24*Ar_1, Cost: 1) eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3)) (Comp: 24*Ar_1, Cost: 1) eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 24*Ar_1, Cost: 1) eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3)) (Comp: 2, Cost: 1) eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Repeatedly propagating knowledge in problem 7 produces the following problem: 8: T: (Comp: 1, Cost: 1) eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_0(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_1(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_2(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_3(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 1) eval_ex2_4(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, 1, Ar_3)) (Comp: 6*Ar_1, Cost: 1) eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_2)) [ Ar_2 <= Ar_1 ] (Comp: 1, Cost: 1) eval_ex2_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_2 > Ar_1 ] (Comp: 600*Ar_1^2 + 332358*Ar_1, Cost: 1) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 <= Ar_1 ] (Comp: 24*Ar_1, Cost: 1) eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3)) [ Ar_3 > Ar_1 ] (Comp: 600*Ar_1^2 + 332358*Ar_1, Cost: 1) eval_ex2_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 600*Ar_1^2 + 332358*Ar_1, Cost: 1) eval_ex2_5(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 600*Ar_1^2 + 332358*Ar_1, Cost: 1) eval_ex2_6(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3 + 1)) (Comp: 24*Ar_1, Cost: 1) eval_ex2_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_9(Ar_2 + 1, Ar_1, Ar_2, Ar_3)) (Comp: 24*Ar_1, Cost: 1) eval_ex2_9(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 24*Ar_1, Cost: 1) eval_ex2_10(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_bb1_in(Ar_0, Ar_1, Ar_0, Ar_3)) (Comp: 2, Cost: 1) eval_ex2_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_stop(Ar_0, Ar_1, Ar_2, Ar_3)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3) -> Com_1(eval_ex2_start(Ar_0, Ar_1, Ar_2, Ar_3)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Complexity upper bound 1329534*Ar_1 + 2400*Ar_1^2 + 10 Time: 1.438 sec (SMT: 1.365 sec)