WORST_CASE(?, O(n^1)) Initial complexity problem: 1: T: (Comp: ?, Cost: 1) f2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f2(Ar_0, Ar_1 + 1, Ar_2*Fresh_17, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_0 >= Ar_1 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Fresh_12, Fresh_13, Fresh_14, Fresh_15, Fresh_16, 1, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_3 >= 2*C1 /\ 3*C1 >= Ar_3 + 1 /\ C1 >= Fresh_14 /\ Ar_3 >= 2*E1 /\ 3*E1 >= Ar_3 + 1 /\ Fresh_14 >= E1 /\ Ar_3*Fresh_12 >= 2*F1*Fresh_12 /\ 2*F1*Fresh_12 + F1 >= Ar_3*Fresh_12 + 1 /\ F1 >= Fresh_15 /\ Ar_3*Fresh_12 >= 2*Fresh_12*H1 /\ 2*Fresh_12*H1 + H1 >= Ar_3*Fresh_12 + 1 /\ Fresh_15 >= H1 /\ Ar_2 >= Ar_3*Fresh_12*I1 /\ Ar_3*Fresh_12*I1 + I1 >= Ar_2 + 1 /\ Ar_2 >= Ar_3*Fresh_12*J1 /\ Ar_3*Fresh_12*J1 + J1 >= Ar_2 + 1 /\ Ar_3*Fresh_12*I1 >= 2*Fresh_12*J1*K1 /\ 2*Fresh_12*J1*K1 + K1 >= Ar_3*Fresh_12*I1 + 1 /\ K1 >= Fresh_16 /\ Ar_2 >= Ar_3*Fresh_12*M1 /\ Ar_3*Fresh_12*M1 + M1 >= Ar_2 + 1 /\ Ar_2 >= Ar_3*Fresh_12*N1 /\ Ar_3*Fresh_12*N1 + N1 >= Ar_2 + 1 /\ Ar_3*Fresh_12*M1 >= 2*Fresh_12*N1*O1 /\ 2*Fresh_12*N1*O1 + O1 >= Ar_3*Fresh_12*M1 + 1 /\ Fresh_16 >= O1 /\ Ar_1 >= 1 /\ Ar_2 >= Ar_3*Fresh_12*P1 /\ Ar_3*Fresh_12*P1 + P1 >= Ar_2 + 1 /\ P1 >= Fresh_13 /\ Ar_2 >= Ar_3*Fresh_12*R1 /\ Ar_3*Fresh_12*R1 + R1 >= Ar_2 + 1 /\ Fresh_13 >= R1 ] (Comp: ?, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f23(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_7 >= Ar_10 /\ Ar_9 >= Ar_10 + 1 ] (Comp: ?, Cost: 1) f23(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f26(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_10 + Ar_6 >= Ar_11 + 2 ] (Comp: ?, Cost: 1) f26(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f26(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12 + Ar_7, Ar_9 + Ar_12 - Ar_10, Fresh_11, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_8 >= Ar_12 ] (Comp: ?, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Fresh_10, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_10 >= Ar_9 /\ Ar_7 >= 2*Q1 /\ 3*Q1 >= Ar_7 + 1 /\ Q1 >= Fresh_10 /\ Ar_7 >= 2*D1 /\ 3*D1 >= Ar_7 + 1 /\ Fresh_10 >= D1 /\ Ar_7 >= Ar_10 ] (Comp: ?, Cost: 1) f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9 - Ar_15, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Fresh_9, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_9 >= Ar_15 + 1 /\ Ar_15 >= 2*Q1 /\ 3*Q1 >= Ar_15 + 1 /\ Q1 >= Fresh_9 /\ Ar_15 >= 2*D1 /\ 3*D1 >= Ar_15 + 1 /\ Fresh_9 >= D1 /\ Ar_15 >= Ar_6 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f63(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, 2*Ar_16, Fresh_5, Fresh_6, Fresh_7, Fresh_8, 1, 0, Ar_24, Ar_25, Ar_26)) [ Ar_7 >= Ar_16 + 1 ] (Comp: ?, Cost: 1) f63(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f66(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_16 >= Ar_12 ] (Comp: ?, Cost: 1) f66(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f69(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_12 + Ar_6 >= Ar_11 + 2 ] (Comp: ?, Cost: 1) f69(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f69(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10 + Ar_17, Ar_11, Ar_12, Ar_13, Ar_22*Fresh_1 - Ar_23*Fresh_2, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_10, Ar_10 + Ar_16, Ar_22*Fresh_3 + Ar_23*Fresh_4)) [ Ar_8 >= Ar_10 ] (Comp: ?, Cost: 1) f69(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f66(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11 + 2, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_10 >= Ar_8 + 1 ] (Comp: ?, Cost: 1) f66(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f63(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12 + Ar_6, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_22, Ar_20, Ar_21, Ar_20*Ar_22 - Ar_21*Ar_23 + Ar_22, Ar_20*Ar_23 + Ar_21*Ar_22 + Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_11 + 1 >= Ar_12 + Ar_6 ] (Comp: ?, Cost: 1) f63(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f53(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_17, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_12 >= Ar_16 + 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f10(Ar_0, Ar_1 - 1, Ar_2, Ar_3*Ar_4, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_16 >= Ar_7 ] (Comp: ?, Cost: 1) f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9 + Ar_15, Ar_10 + Ar_6, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_15 >= Ar_6 /\ Ar_15 >= Ar_9 ] (Comp: ?, Cost: 1) f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9 + Ar_15, Ar_10 + Ar_6, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_6 >= Ar_15 + 1 ] (Comp: ?, Cost: 1) f26(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f23(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11 + 2, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_12 >= Ar_8 + 1 ] (Comp: ?, Cost: 1) f23(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Fresh_0, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_11 + 1 >= Ar_10 + Ar_6 /\ Ar_7 >= 2*Q1 /\ 3*Q1 >= Ar_7 + 1 /\ Q1 >= Fresh_0 /\ Ar_7 >= 2*D1 /\ 3*D1 >= Ar_7 + 1 /\ Fresh_0 >= D1 ] (Comp: ?, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f53(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_6, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_10 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ 0 >= Ar_1 ] (Comp: ?, Cost: 1) f2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f10(Ar_0, Ar_1, Ar_2, 1, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ Ar_1 >= Ar_0 + 1 ] (Comp: ?, Cost: 1) start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(f2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26) -> Com_1(start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17]. We thus obtain the following problem: 2: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ 0 <= 0 ] (Comp: ?, Cost: 1) start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) (Comp: ?, Cost: 1) f2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f10(Ar_0, Ar_1, Ar_2, 1, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_1 >= Ar_0 + 1 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ 0 >= Ar_1 ] (Comp: ?, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f53(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_6, Ar_17)) [ Ar_10 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f23(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Fresh_0, Ar_16, Ar_17)) [ Ar_11 + 1 >= Ar_10 + Ar_6 /\ Ar_7 >= 2*Q1 /\ 3*Q1 >= Ar_7 + 1 /\ Q1 >= Fresh_0 /\ Ar_7 >= 2*D1 /\ 3*D1 >= Ar_7 + 1 /\ Fresh_0 >= D1 ] (Comp: ?, Cost: 1) f26(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f23(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11 + 2, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_12 >= Ar_8 + 1 ] (Comp: ?, Cost: 1) f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9 + Ar_15, Ar_10 + Ar_6, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_6 >= Ar_15 + 1 ] (Comp: ?, Cost: 1) f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9 + Ar_15, Ar_10 + Ar_6, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_15 >= Ar_6 /\ Ar_15 >= Ar_9 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f10(Ar_0, Ar_1 - 1, Ar_2, Ar_3*Ar_4, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_16 >= Ar_7 ] (Comp: ?, Cost: 1) f63(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f53(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_17, Ar_17)) [ Ar_12 >= Ar_16 + 1 ] (Comp: ?, Cost: 1) f66(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f63(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12 + Ar_6, Ar_15, Ar_16, Ar_17)) [ Ar_11 + 1 >= Ar_12 + Ar_6 ] (Comp: ?, Cost: 1) f69(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f66(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11 + 2, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_10 >= Ar_8 + 1 ] (Comp: ?, Cost: 1) f69(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f69(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10 + Ar_17, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_8 >= Ar_10 ] (Comp: ?, Cost: 1) f66(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f69(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_12 + Ar_6 >= Ar_11 + 2 ] (Comp: ?, Cost: 1) f63(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f66(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_16 >= Ar_12 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f63(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, 2*Ar_16)) [ Ar_7 >= Ar_16 + 1 ] (Comp: ?, Cost: 1) f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9 - Ar_15, Ar_10, Ar_11, Ar_12, Fresh_9, Ar_16, Ar_17)) [ Ar_9 >= Ar_15 + 1 /\ Ar_15 >= 2*Q1 /\ 3*Q1 >= Ar_15 + 1 /\ Q1 >= Fresh_9 /\ Ar_15 >= 2*D1 /\ 3*D1 >= Ar_15 + 1 /\ Fresh_9 >= D1 /\ Ar_15 >= Ar_6 ] (Comp: ?, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Fresh_10, Ar_16, Ar_17)) [ Ar_10 >= Ar_9 /\ Ar_7 >= 2*Q1 /\ 3*Q1 >= Ar_7 + 1 /\ Q1 >= Fresh_10 /\ Ar_7 >= 2*D1 /\ 3*D1 >= Ar_7 + 1 /\ Fresh_10 >= D1 /\ Ar_7 >= Ar_10 ] (Comp: ?, Cost: 1) f26(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f26(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12 + Ar_7, Ar_15, Ar_16, Ar_17)) [ Ar_8 >= Ar_12 ] (Comp: ?, Cost: 1) f23(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f26(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_10 + Ar_6 >= Ar_11 + 2 ] (Comp: ?, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f23(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_7 >= Ar_10 /\ Ar_9 >= Ar_10 + 1 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Fresh_12, Fresh_14, Fresh_15, Fresh_16, 1, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_3 >= 2*C1 /\ 3*C1 >= Ar_3 + 1 /\ C1 >= Fresh_14 /\ Ar_3 >= 2*E1 /\ 3*E1 >= Ar_3 + 1 /\ Fresh_14 >= E1 /\ Ar_3*Fresh_12 >= 2*F1*Fresh_12 /\ 2*F1*Fresh_12 + F1 >= Ar_3*Fresh_12 + 1 /\ F1 >= Fresh_15 /\ Ar_3*Fresh_12 >= 2*Fresh_12*H1 /\ 2*Fresh_12*H1 + H1 >= Ar_3*Fresh_12 + 1 /\ Fresh_15 >= H1 /\ Ar_2 >= Ar_3*Fresh_12*I1 /\ Ar_3*Fresh_12*I1 + I1 >= Ar_2 + 1 /\ Ar_2 >= Ar_3*Fresh_12*J1 /\ Ar_3*Fresh_12*J1 + J1 >= Ar_2 + 1 /\ Ar_3*Fresh_12*I1 >= 2*Fresh_12*J1*K1 /\ 2*Fresh_12*J1*K1 + K1 >= Ar_3*Fresh_12*I1 + 1 /\ K1 >= Fresh_16 /\ Ar_2 >= Ar_3*Fresh_12*M1 /\ Ar_3*Fresh_12*M1 + M1 >= Ar_2 + 1 /\ Ar_2 >= Ar_3*Fresh_12*N1 /\ Ar_3*Fresh_12*N1 + N1 >= Ar_2 + 1 /\ Ar_3*Fresh_12*M1 >= 2*Fresh_12*N1*O1 /\ 2*Fresh_12*N1*O1 + O1 >= Ar_3*Fresh_12*M1 + 1 /\ Fresh_16 >= O1 /\ Ar_1 >= 1 /\ Ar_2 >= Ar_3*Fresh_12*P1 /\ Ar_3*Fresh_12*P1 + P1 >= Ar_2 + 1 /\ P1 >= Fresh_13 /\ Ar_2 >= Ar_3*Fresh_12*R1 /\ Ar_3*Fresh_12*R1 + R1 >= Ar_2 + 1 /\ Fresh_13 >= R1 ] (Comp: ?, Cost: 1) f2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f2(Ar_0, Ar_1 + 1, Ar_2*Fresh_17, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_0 >= Ar_1 ] start location: koat_start leaf cost: 0 Testing for reachability in the complexity graph removes the following transitions from problem 2: f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f53(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_6, Ar_17)) [ Ar_10 >= Ar_7 + 1 ] f23(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Fresh_0, Ar_16, Ar_17)) [ Ar_11 + 1 >= Ar_10 + Ar_6 /\ Ar_7 >= 2*Q1 /\ 3*Q1 >= Ar_7 + 1 /\ Q1 >= Fresh_0 /\ Ar_7 >= 2*D1 /\ 3*D1 >= Ar_7 + 1 /\ Fresh_0 >= D1 ] f26(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f23(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11 + 2, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_12 >= Ar_8 + 1 ] f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9 + Ar_15, Ar_10 + Ar_6, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_6 >= Ar_15 + 1 ] f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9 + Ar_15, Ar_10 + Ar_6, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_15 >= Ar_6 /\ Ar_15 >= Ar_9 ] f53(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f10(Ar_0, Ar_1 - 1, Ar_2, Ar_3*Ar_4, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_16 >= Ar_7 ] f63(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f53(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_17, Ar_17)) [ Ar_12 >= Ar_16 + 1 ] f66(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f63(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12 + Ar_6, Ar_15, Ar_16, Ar_17)) [ Ar_11 + 1 >= Ar_12 + Ar_6 ] f69(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f66(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11 + 2, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_10 >= Ar_8 + 1 ] f69(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f69(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10 + Ar_17, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_8 >= Ar_10 ] f66(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f69(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_12 + Ar_6 >= Ar_11 + 2 ] f63(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f66(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_16 >= Ar_12 ] f53(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f63(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, 2*Ar_16)) [ Ar_7 >= Ar_16 + 1 ] f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9 - Ar_15, Ar_10, Ar_11, Ar_12, Fresh_9, Ar_16, Ar_17)) [ Ar_9 >= Ar_15 + 1 /\ Ar_15 >= 2*Q1 /\ 3*Q1 >= Ar_15 + 1 /\ Q1 >= Fresh_9 /\ Ar_15 >= 2*D1 /\ 3*D1 >= Ar_15 + 1 /\ Fresh_9 >= D1 /\ Ar_15 >= Ar_6 ] f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f41(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Fresh_10, Ar_16, Ar_17)) [ Ar_10 >= Ar_9 /\ Ar_7 >= 2*Q1 /\ 3*Q1 >= Ar_7 + 1 /\ Q1 >= Fresh_10 /\ Ar_7 >= 2*D1 /\ 3*D1 >= Ar_7 + 1 /\ Fresh_10 >= D1 /\ Ar_7 >= Ar_10 ] f26(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f26(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12 + Ar_7, Ar_15, Ar_16, Ar_17)) [ Ar_8 >= Ar_12 ] f23(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f26(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_10 + Ar_6 >= Ar_11 + 2 ] f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f23(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_7 >= Ar_10 /\ Ar_9 >= Ar_10 + 1 ] f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Fresh_12, Fresh_14, Fresh_15, Fresh_16, 1, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_3 >= 2*C1 /\ 3*C1 >= Ar_3 + 1 /\ C1 >= Fresh_14 /\ Ar_3 >= 2*E1 /\ 3*E1 >= Ar_3 + 1 /\ Fresh_14 >= E1 /\ Ar_3*Fresh_12 >= 2*F1*Fresh_12 /\ 2*F1*Fresh_12 + F1 >= Ar_3*Fresh_12 + 1 /\ F1 >= Fresh_15 /\ Ar_3*Fresh_12 >= 2*Fresh_12*H1 /\ 2*Fresh_12*H1 + H1 >= Ar_3*Fresh_12 + 1 /\ Fresh_15 >= H1 /\ Ar_2 >= Ar_3*Fresh_12*I1 /\ Ar_3*Fresh_12*I1 + I1 >= Ar_2 + 1 /\ Ar_2 >= Ar_3*Fresh_12*J1 /\ Ar_3*Fresh_12*J1 + J1 >= Ar_2 + 1 /\ Ar_3*Fresh_12*I1 >= 2*Fresh_12*J1*K1 /\ 2*Fresh_12*J1*K1 + K1 >= Ar_3*Fresh_12*I1 + 1 /\ K1 >= Fresh_16 /\ Ar_2 >= Ar_3*Fresh_12*M1 /\ Ar_3*Fresh_12*M1 + M1 >= Ar_2 + 1 /\ Ar_2 >= Ar_3*Fresh_12*N1 /\ Ar_3*Fresh_12*N1 + N1 >= Ar_2 + 1 /\ Ar_3*Fresh_12*M1 >= 2*Fresh_12*N1*O1 /\ 2*Fresh_12*N1*O1 + O1 >= Ar_3*Fresh_12*M1 + 1 /\ Fresh_16 >= O1 /\ Ar_1 >= 1 /\ Ar_2 >= Ar_3*Fresh_12*P1 /\ Ar_3*Fresh_12*P1 + P1 >= Ar_2 + 1 /\ P1 >= Fresh_13 /\ Ar_2 >= Ar_3*Fresh_12*R1 /\ Ar_3*Fresh_12*R1 + R1 >= Ar_2 + 1 /\ Fresh_13 >= R1 ] We thus obtain the following problem: 3: T: (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ 0 >= Ar_1 ] (Comp: ?, Cost: 1) f2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f2(Ar_0, Ar_1 + 1, Ar_2*Fresh_17, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_0 >= Ar_1 ] (Comp: ?, Cost: 1) f2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f10(Ar_0, Ar_1, Ar_2, 1, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ Ar_1 >= Ar_0 + 1 ] (Comp: ?, Cost: 1) start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(f2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17) -> Com_1(start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_15, Ar_16, Ar_17)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Repeatedly propagating knowledge in problem 3 produces the following problem: 4: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1) -> Com_1(start(Ar_0, Ar_1)) [ 0 <= 0 ] (Comp: 1, Cost: 1) start(Ar_0, Ar_1) -> Com_1(f2(Ar_0, Ar_1)) (Comp: ?, Cost: 1) f2(Ar_0, Ar_1) -> Com_1(f10(Ar_0, Ar_1)) [ Ar_1 >= Ar_0 + 1 ] (Comp: ?, Cost: 1) f2(Ar_0, Ar_1) -> Com_1(f2(Ar_0, Ar_1 + 1)) [ Ar_0 >= Ar_1 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1) -> Com_1(f1(Ar_0, Ar_1)) [ 0 >= Ar_1 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = 2 Pol(start) = 2 Pol(f2) = 2 Pol(f10) = 1 Pol(f1) = 0 orients all transitions weakly and the transitions f2(Ar_0, Ar_1) -> Com_1(f10(Ar_0, Ar_1)) [ Ar_1 >= Ar_0 + 1 ] f10(Ar_0, Ar_1) -> Com_1(f1(Ar_0, Ar_1)) [ 0 >= Ar_1 ] strictly and produces the following problem: 5: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1) -> Com_1(start(Ar_0, Ar_1)) [ 0 <= 0 ] (Comp: 1, Cost: 1) start(Ar_0, Ar_1) -> Com_1(f2(Ar_0, Ar_1)) (Comp: 2, Cost: 1) f2(Ar_0, Ar_1) -> Com_1(f10(Ar_0, Ar_1)) [ Ar_1 >= Ar_0 + 1 ] (Comp: ?, Cost: 1) f2(Ar_0, Ar_1) -> Com_1(f2(Ar_0, Ar_1 + 1)) [ Ar_0 >= Ar_1 ] (Comp: 2, Cost: 1) f10(Ar_0, Ar_1) -> Com_1(f1(Ar_0, Ar_1)) [ 0 >= Ar_1 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = V_1 - V_2 + 1 Pol(start) = V_1 - V_2 + 1 Pol(f2) = V_1 - V_2 + 1 Pol(f10) = V_1 - V_2 + 1 Pol(f1) = V_1 - V_2 + 1 orients all transitions weakly and the transition f2(Ar_0, Ar_1) -> Com_1(f2(Ar_0, Ar_1 + 1)) [ Ar_0 >= Ar_1 ] strictly and produces the following problem: 6: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1) -> Com_1(start(Ar_0, Ar_1)) [ 0 <= 0 ] (Comp: 1, Cost: 1) start(Ar_0, Ar_1) -> Com_1(f2(Ar_0, Ar_1)) (Comp: 2, Cost: 1) f2(Ar_0, Ar_1) -> Com_1(f10(Ar_0, Ar_1)) [ Ar_1 >= Ar_0 + 1 ] (Comp: Ar_0 + Ar_1 + 1, Cost: 1) f2(Ar_0, Ar_1) -> Com_1(f2(Ar_0, Ar_1 + 1)) [ Ar_0 >= Ar_1 ] (Comp: 2, Cost: 1) f10(Ar_0, Ar_1) -> Com_1(f1(Ar_0, Ar_1)) [ 0 >= Ar_1 ] start location: koat_start leaf cost: 0 Complexity upper bound Ar_0 + Ar_1 + 6 Time: 1.006 sec (SMT: 0.909 sec)