WORST_CASE(?, O(n^2)) Initial complexity problem: 1: T: (Comp: ?, Cost: 1) eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3)) (Comp: ?, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ] (Comp: ?, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ] (Comp: ?, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ] (Comp: ?, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 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_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3)) (Comp: ?, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ] (Comp: ?, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ] (Comp: ?, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ] (Comp: ?, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(eval_foo_start) = 1 Pol(eval_foo_bb0_in) = 1 Pol(eval_foo_0) = 1 Pol(eval_foo_1) = 1 Pol(eval_foo_2) = 1 Pol(eval_foo_3) = 1 Pol(eval_foo_4) = 1 Pol(eval_foo_5) = 1 Pol(eval_foo_6) = 1 Pol(eval_foo_7) = 1 Pol(eval_foo_bb1_in) = 1 Pol(eval_foo_bb2_in) = 1 Pol(eval_foo_bb5_in) = 0 Pol(eval_foo_10) = 1 Pol(eval_foo_11) = 1 Pol(eval_foo_bb3_in) = 1 Pol(eval_foo_bb4_in) = 1 Pol(eval_foo_stop) = -1 Pol(koat_start) = 1 orients all transitions weakly and the transition eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ] strictly and produces the following problem: 3: T: (Comp: 1, Cost: 1) eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3)) (Comp: ?, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ] (Comp: 1, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ] (Comp: ?, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ] (Comp: ?, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Repeatedly propagating knowledge in problem 3 produces the following problem: 4: T: (Comp: 1, Cost: 1) eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3)) (Comp: ?, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ] (Comp: 1, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ] (Comp: ?, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ] (Comp: ?, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(eval_foo_start) = 5*V_4 Pol(eval_foo_bb0_in) = 5*V_4 Pol(eval_foo_0) = 5*V_4 Pol(eval_foo_1) = 5*V_4 Pol(eval_foo_2) = 5*V_4 Pol(eval_foo_3) = 5*V_4 Pol(eval_foo_4) = 5*V_4 Pol(eval_foo_5) = 5*V_4 Pol(eval_foo_6) = 5*V_4 Pol(eval_foo_7) = 5*V_4 Pol(eval_foo_bb1_in) = 5*V_7 - 3 Pol(eval_foo_bb2_in) = 5*V_7 - 4 Pol(eval_foo_bb5_in) = 5*V_7 - 3 Pol(eval_foo_10) = 5*V_1 Pol(eval_foo_11) = 5*V_1 - 1 Pol(eval_foo_bb3_in) = 5*V_1 - 2 Pol(eval_foo_bb4_in) = 5*V_1 - 2 Pol(eval_foo_stop) = 5*V_7 - 3 Pol(koat_start) = 5*V_4 orients all transitions weakly and the transition eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ] strictly and produces the following problem: 5: T: (Comp: 1, Cost: 1) eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3)) (Comp: 5*Ar_3, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ] (Comp: 1, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: ?, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ] (Comp: ?, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ] (Comp: ?, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Repeatedly propagating knowledge in problem 5 produces the following problem: 6: T: (Comp: 1, Cost: 1) eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3)) (Comp: 5*Ar_3, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ] (Comp: 1, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ] (Comp: 5*Ar_3, Cost: 1) eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 5*Ar_3, Cost: 1) eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 5*Ar_3, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ] (Comp: 5*Ar_3, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ] (Comp: ?, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(eval_foo_bb4_in) = 1 Pol(eval_foo_bb3_in) = 1 Pol(eval_foo_bb1_in) = 0 and size complexities S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ]", 0-0) = Ar_0 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ]", 0-1) = Ar_1 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ]", 0-2) = Ar_2 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ]", 0-3) = Ar_3 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ]", 0-4) = Ar_4 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ]", 0-5) = Ar_5 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ]", 0-6) = Ar_6 S("eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = 6*Ar_0 + 6*Ar_3 S("eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = 5*Ar_1 + 5*Ar_3 S("eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = ? S("eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = ? S("eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = 5*Ar_3 S("eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = 6*Ar_3 S("eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6))", 0-0) = 6*Ar_3 S("eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6))", 0-1) = 5*Ar_3 S("eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6))", 0-2) = ? S("eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6))", 0-4) = ? S("eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6))", 0-5) = 5*Ar_3 S("eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6))", 0-6) = 6*Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ]", 0-0) = 6*Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ]", 0-1) = 5*Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ]", 0-2) = ? S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ]", 0-3) = Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ]", 0-4) = ? S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ]", 0-5) = 0 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ]", 0-6) = 6*Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ]", 0-0) = 6*Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ]", 0-1) = 5*Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ]", 0-2) = ? S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ]", 0-3) = Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ]", 0-4) = ? S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ]", 0-5) = 5*Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ]", 0-6) = 6*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ]", 0-0) = 6*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ]", 0-1) = 5*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ]", 0-2) = ? S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ]", 0-3) = Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ]", 0-4) = ? S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ]", 0-5) = 5*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ]", 0-6) = 6*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ]", 0-0) = 6*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ]", 0-1) = 5*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ]", 0-2) = ? S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ]", 0-3) = Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ]", 0-4) = 5*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ]", 0-5) = 5*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ]", 0-6) = 6*Ar_3 S("eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = 6*Ar_3 S("eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = 5*Ar_3 S("eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = ? S("eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = ? S("eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = 5*Ar_3 S("eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = 6*Ar_3 S("eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = 6*Ar_3 S("eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = 5*Ar_3 S("eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = ? S("eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = ? S("eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = 5*Ar_3 S("eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = 6*Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ]", 0-0) = 6*Ar_0 + 6*Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ]", 0-1) = 5*Ar_1 + 5*Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ]", 0-2) = ? S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ]", 0-3) = Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ]", 0-4) = ? S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ]", 0-5) = 5*Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ]", 0-6) = 6*Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ]", 0-0) = 6*Ar_0 + 6*Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ]", 0-1) = 5*Ar_1 + 5*Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ]", 0-2) = ? S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ]", 0-3) = Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ]", 0-4) = ? S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ]", 0-5) = 5*Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ]", 0-6) = 6*Ar_3 S("eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3))", 0-0) = Ar_0 S("eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3))", 0-1) = Ar_1 S("eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3))", 0-2) = Ar_2 S("eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3))", 0-3) = Ar_3 S("eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3))", 0-4) = Ar_4 S("eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3))", 0-5) = 0 S("eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3))", 0-6) = Ar_3 S("eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 S("eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 S("eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 S("eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 S("eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 S("eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 S("eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 S("eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 S("eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 orients the transitions eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6)) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ] eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ] weakly and the transition eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ] strictly and produces the following problem: 7: T: (Comp: 1, Cost: 1) eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3)) (Comp: 5*Ar_3, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ] (Comp: 1, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ] (Comp: 5*Ar_3, Cost: 1) eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 5*Ar_3, Cost: 1) eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 5*Ar_3, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ] (Comp: 5*Ar_3, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ] (Comp: 5*Ar_3, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(eval_foo_bb4_in) = 2*V_5 - 1 Pol(eval_foo_bb3_in) = 2*V_5 and size complexities S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ]", 0-0) = Ar_0 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ]", 0-1) = Ar_1 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ]", 0-2) = Ar_2 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ]", 0-3) = Ar_3 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ]", 0-4) = Ar_4 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ]", 0-5) = Ar_5 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ]", 0-6) = Ar_6 S("eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = 6*Ar_0 + 6*Ar_3 S("eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = 5*Ar_1 + 5*Ar_3 S("eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = ? S("eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = ? S("eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = 5*Ar_3 S("eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = 6*Ar_3 S("eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6))", 0-0) = 6*Ar_3 S("eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6))", 0-1) = 5*Ar_3 S("eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6))", 0-2) = ? S("eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6))", 0-4) = ? S("eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6))", 0-5) = 5*Ar_3 S("eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6))", 0-6) = 6*Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ]", 0-0) = 6*Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ]", 0-1) = 5*Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ]", 0-2) = ? S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ]", 0-3) = Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ]", 0-4) = ? S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ]", 0-5) = 0 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ]", 0-6) = 6*Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ]", 0-0) = 6*Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ]", 0-1) = 5*Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ]", 0-2) = ? S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ]", 0-3) = Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ]", 0-4) = ? S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ]", 0-5) = 5*Ar_3 S("eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ]", 0-6) = 6*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ]", 0-0) = 6*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ]", 0-1) = 5*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ]", 0-2) = ? S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ]", 0-3) = Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ]", 0-4) = ? S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ]", 0-5) = 5*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ]", 0-6) = 6*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ]", 0-0) = 6*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ]", 0-1) = 5*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ]", 0-2) = ? S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ]", 0-3) = Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ]", 0-4) = 5*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ]", 0-5) = 5*Ar_3 S("eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ]", 0-6) = 6*Ar_3 S("eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = 6*Ar_3 S("eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = 5*Ar_3 S("eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = ? S("eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = ? S("eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = 5*Ar_3 S("eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = 6*Ar_3 S("eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = 6*Ar_3 S("eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = 5*Ar_3 S("eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = ? S("eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = ? S("eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = 5*Ar_3 S("eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = 6*Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ]", 0-0) = 6*Ar_0 + 6*Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ]", 0-1) = 5*Ar_1 + 5*Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ]", 0-2) = ? S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ]", 0-3) = Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ]", 0-4) = ? S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ]", 0-5) = 5*Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ]", 0-6) = 6*Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ]", 0-0) = 6*Ar_0 + 6*Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ]", 0-1) = 5*Ar_1 + 5*Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ]", 0-2) = ? S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ]", 0-3) = Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ]", 0-4) = ? S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ]", 0-5) = 5*Ar_3 S("eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ]", 0-6) = 6*Ar_3 S("eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3))", 0-0) = Ar_0 S("eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3))", 0-1) = Ar_1 S("eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3))", 0-2) = Ar_2 S("eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3))", 0-3) = Ar_3 S("eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3))", 0-4) = Ar_4 S("eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3))", 0-5) = 0 S("eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3))", 0-6) = Ar_3 S("eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 S("eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 S("eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 S("eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 S("eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 S("eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 S("eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 S("eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 S("eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-0) = Ar_0 S("eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-1) = Ar_1 S("eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-2) = Ar_2 S("eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-3) = Ar_3 S("eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-4) = Ar_4 S("eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-5) = Ar_5 S("eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6))", 0-6) = Ar_6 orients the transitions eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6)) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ] weakly and the transition eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ] strictly and produces the following problem: 8: T: (Comp: 1, Cost: 1) eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3)) (Comp: 5*Ar_3, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ] (Comp: 1, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ] (Comp: 5*Ar_3, Cost: 1) eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 5*Ar_3, Cost: 1) eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 5*Ar_3, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ] (Comp: 5*Ar_3, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ] (Comp: 50*Ar_3^2, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ] (Comp: 5*Ar_3, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ] (Comp: ?, Cost: 1) eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Repeatedly propagating knowledge in problem 8 produces the following problem: 9: T: (Comp: 1, Cost: 1) eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_bb0_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_4(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_5(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_3)) (Comp: 5*Ar_3, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 > 0 ] (Comp: 1, Cost: 1) eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_6 <= 0 ] (Comp: 5*Ar_3, Cost: 1) eval_foo_bb2_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_10(Ar_6 - 1, Ar_5 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 5*Ar_3, Cost: 1) eval_foo_10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_11(Ar_0, Ar_1, Fresh_0, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 5*Ar_3, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_1, Ar_5, Ar_6)) [ Ar_2 > 0 ] (Comp: 5*Ar_3, Cost: 1) eval_foo_11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_1, Ar_0)) [ Ar_2 <= 0 ] (Comp: 50*Ar_3^2, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ Ar_4 > 0 ] (Comp: 5*Ar_3, Cost: 1) eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb1_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_0)) [ Ar_4 <= 0 ] (Comp: 50*Ar_3^2, Cost: 1) eval_foo_bb4_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_bb3_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4 - 1, Ar_5, Ar_6)) (Comp: 1, Cost: 1) eval_foo_bb5_in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_stop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6) -> Com_1(eval_foo_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Complexity upper bound 30*Ar_3 + 100*Ar_3^2 + 12 Time: 2.541 sec (SMT: 2.375 sec)