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) -> Com_1(f13(1, Fresh_65, Fresh_66, Fresh_67, Fresh_68, Fresh_69, Fresh_70, 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_0 = 1 ] (Comp: ?, Cost: 1) f13(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) -> Com_1(f16(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_7 >= Ar_8 ] (Comp: ?, Cost: 1) f16(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) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10 + 1, 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_9 >= Ar_10 ] (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) -> Com_1(f27(Ar_0, Fresh_59, Fresh_60, Fresh_61, Fresh_62, Fresh_63, Fresh_64, 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)) [ 0 >= Ar_0 ] (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) -> Com_1(f27(Ar_0, Fresh_53, Fresh_54, Fresh_55, Fresh_56, Fresh_57, Fresh_58, 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_0 >= 2 ] (Comp: ?, Cost: 1) f27(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) -> Com_1(f35(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_7 - Ar_8 + 2, 1, 0, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ] (Comp: ?, Cost: 1) f27(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) -> Com_1(f35(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_7 - Ar_8 + 2, 1, 0, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ] (Comp: ?, Cost: 1) f27(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) -> Com_1(f35(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, 1, Ar_9, Ar_10, Ar_11, 1, 1, 0, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ Ar_7 >= 1 /\ Ar_8 = 1 ] (Comp: ?, Cost: 1) f35(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) -> Com_1(f38(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_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ] (Comp: ?, Cost: 1) f38(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) -> 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_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f38(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) -> 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_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f38(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) -> Com_1(f38(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Fresh_44 + 3, Ar_12, Ar_13, Ar_14, Ar_15, 1, Ar_1*Fresh_45 + Ar_1*Fresh_46, Ar_1*Fresh_47 - Ar_1*Fresh_48, Ar_2*Fresh_49 - Ar_2*Fresh_50, -Ar_2*Fresh_51 - Ar_2*Fresh_52, Ar_21, Ar_22)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(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) -> Com_1(f38(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Fresh_35 + 3, Ar_12, Ar_13, Ar_14, Ar_15, 1, Ar_1*Fresh_36 + Ar_1*Fresh_37, Ar_1*Fresh_38 - Ar_1*Fresh_39, Ar_2*Fresh_40 - Ar_2*Fresh_41, -Ar_2*Fresh_42 - Ar_2*Fresh_43, Ar_21, Ar_22)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(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) -> Com_1(f38(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, 2, 1, Ar_12, Ar_13, Ar_14, Ar_15, 1, Ar_1*Fresh_27 + Ar_1*Fresh_28, Ar_1*Fresh_29 - Ar_1*Fresh_30, Ar_2*Fresh_31 - Ar_2*Fresh_32, -Ar_2*Fresh_33 - Ar_2*Fresh_34, Ar_21, Ar_22)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ 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) -> Com_1(f38(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_9 - Ar_10 + 2, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_1*Fresh_18 + Ar_1*Fresh_19, Ar_1*Fresh_20 - Ar_1*Fresh_21, Ar_2*Fresh_22 - Ar_2*Fresh_23, -Ar_2*Fresh_24 - Ar_2*Fresh_25, Ar_15 - Fresh_26 + 3, Ar_22)) [ Ar_16 >= 2*Fresh_26 /\ 3*Fresh_26 >= Ar_16 + 1 /\ 0 >= Ar_10 ] (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) -> Com_1(f38(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_9 - Ar_10 + 2, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_1*Fresh_9 + Ar_1*Fresh_10, Ar_1*Fresh_11 - Ar_1*Fresh_12, Ar_2*Fresh_13 - Ar_2*Fresh_14, -Ar_2*Fresh_15 - Ar_2*Fresh_16, Ar_15 - Fresh_17 + 3, Ar_22)) [ Ar_16 >= 2*Fresh_17 /\ 3*Fresh_17 >= Ar_16 + 1 /\ Ar_10 >= 2 ] (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) -> Com_1(f38(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, 2, 1, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_1*Fresh_0 + Ar_1*Fresh_1, Ar_1*Fresh_2 - Ar_1*Fresh_3, Ar_2*Fresh_4 - Ar_2*Fresh_5, -Ar_2*Fresh_6 - Ar_2*Fresh_7, Ar_15 - Fresh_8 + 3, Ar_22)) [ Ar_16 >= 2*Fresh_8 /\ 3*Fresh_8 >= Ar_16 + 1 /\ Ar_10 = 1 ] (Comp: ?, Cost: 1) f38(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) -> Com_1(f35(Ar_0, Ar_1, Ar_2, Ar_3, Ar_13, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13*Ar_5 - Ar_14*Ar_6 + Ar_13, Ar_14*Ar_5 + Ar_13*Ar_6 + Ar_14, Ar_15, Ar_16 + 1, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22 + 2)) [ Ar_10 >= Ar_9 + 1 ] (Comp: ?, Cost: 1) f35(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) -> Com_1(f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8 + 1, 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_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ] (Comp: ?, Cost: 1) f27(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) -> 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)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f27(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) -> 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_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f27(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) -> Com_1(f1(-1, 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_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ] (Comp: ?, Cost: 1) f16(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) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8 + 1, 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_10 >= Ar_9 + 1 ] (Comp: ?, Cost: 1) f13(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) -> Com_1(f27(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_8 >= Ar_7 + 1 ] (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) -> 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)) [ 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_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16]. We thus obtain the following problem: 2: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\ 3*Fresh_8 >= Ar_16 + 1 /\ Ar_10 = 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\ 3*Fresh_17 >= Ar_16 + 1 /\ Ar_10 >= 2 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\ 3*Fresh_26 >= Ar_16 + 1 /\ 0 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ] (Comp: ?, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ] (Comp: ?, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ] (Comp: ?, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ] start location: koat_start leaf cost: 0 Repeatedly propagating knowledge in problem 2 produces the following problem: 3: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\ 3*Fresh_8 >= Ar_16 + 1 /\ Ar_10 = 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\ 3*Fresh_17 >= Ar_16 + 1 /\ Ar_10 >= 2 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\ 3*Fresh_26 >= Ar_16 + 1 /\ 0 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = 1 Pol(f2) = 1 Pol(f13) = 1 Pol(f27) = -1 Pol(f16) = 1 Pol(f1) = -2 Pol(f35) = -1 Pol(f38) = -1 Pol(f53) = -1 orients all transitions weakly and the transition f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ] strictly and produces the following problem: 4: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\ 3*Fresh_8 >= Ar_16 + 1 /\ Ar_10 = 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\ 3*Fresh_17 >= Ar_16 + 1 /\ Ar_10 >= 2 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\ 3*Fresh_26 >= Ar_16 + 1 /\ 0 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = 1 Pol(f2) = 1 Pol(f13) = 1 Pol(f27) = 1 Pol(f16) = 1 Pol(f1) = 0 Pol(f35) = 1 Pol(f38) = 1 Pol(f53) = 1 orients all transitions weakly and the transition f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ] strictly and produces the following problem: 5: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\ 3*Fresh_8 >= Ar_16 + 1 /\ Ar_10 = 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\ 3*Fresh_17 >= Ar_16 + 1 /\ Ar_10 >= 2 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\ 3*Fresh_26 >= Ar_16 + 1 /\ 0 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = 1 Pol(f2) = 1 Pol(f13) = 1 Pol(f27) = 1 Pol(f16) = 1 Pol(f1) = 0 Pol(f35) = 1 Pol(f38) = 1 Pol(f53) = 1 orients all transitions weakly and the transition f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ] strictly and produces the following problem: 6: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\ 3*Fresh_8 >= Ar_16 + 1 /\ Ar_10 = 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\ 3*Fresh_17 >= Ar_16 + 1 /\ Ar_10 >= 2 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\ 3*Fresh_26 >= Ar_16 + 1 /\ 0 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = 1 Pol(f2) = 1 Pol(f13) = 1 Pol(f27) = 1 Pol(f16) = 1 Pol(f1) = 0 Pol(f35) = 1 Pol(f38) = 1 Pol(f53) = 1 orients all transitions weakly and the transition f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ] strictly and produces the following problem: 7: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\ 3*Fresh_8 >= Ar_16 + 1 /\ Ar_10 = 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\ 3*Fresh_17 >= Ar_16 + 1 /\ Ar_10 >= 2 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\ 3*Fresh_26 >= Ar_16 + 1 /\ 0 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = 17*V_2 - 15*V_3 Pol(f2) = 17*V_2 - 15*V_3 Pol(f13) = 17*V_2 - 15*V_3 Pol(f27) = 17*V_2 - 15*V_3 Pol(f16) = 17*V_2 - 15*V_3 - 1 Pol(f1) = 17*V_2 - 15*V_3 Pol(f35) = 17*V_2 - 15*V_3 - 14 Pol(f38) = 17*V_2 - 15*V_3 - 14 Pol(f53) = 17*V_2 - 15*V_3 - 14 orients all transitions weakly and the transition f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ] strictly and produces the following problem: 8: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\ 3*Fresh_8 >= Ar_16 + 1 /\ Ar_10 = 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\ 3*Fresh_17 >= Ar_16 + 1 /\ Ar_10 >= 2 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\ 3*Fresh_26 >= Ar_16 + 1 /\ 0 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ] (Comp: 17*Ar_7 + 15*Ar_8, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = 16*V_2 - 16*V_3 + 1 Pol(f2) = 16*V_2 - 16*V_3 + 1 Pol(f13) = 16*V_2 - 16*V_3 + 1 Pol(f27) = 16*V_2 - 16*V_3 + 1 Pol(f16) = 16*V_2 - 16*V_3 - 1 Pol(f1) = 16*V_2 - 16*V_3 Pol(f35) = 16*V_2 - 16*V_3 - 14 Pol(f38) = 16*V_2 - 16*V_3 - 14 Pol(f53) = 16*V_2 - 16*V_3 - 14 orients all transitions weakly and the transitions f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ] f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ] f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ] strictly and produces the following problem: 9: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\ 3*Fresh_8 >= Ar_16 + 1 /\ Ar_10 = 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\ 3*Fresh_17 >= Ar_16 + 1 /\ Ar_10 >= 2 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\ 3*Fresh_26 >= Ar_16 + 1 /\ 0 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ] (Comp: 17*Ar_7 + 15*Ar_8, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(f53) = 1 Pol(f38) = 1 Pol(f35) = 1 Pol(f27) = 0 Pol(f16) = 1 Pol(f13) = 0 and size complexities S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-0) = 1 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-1) = Ar_7 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-2) = Ar_8 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-3) = Ar_9 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-4) = Ar_10 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-5) = Ar_15 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-6) = Ar_16 S("f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-0) = 1 S("f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-1) = Ar_7 S("f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-2) = ? S("f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-3) = Ar_9 S("f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-4) = ? S("f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-5) = Ar_15 S("f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-6) = Ar_16 S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-0) = 1 S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-1) = Ar_7 S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-2) = ? S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-3) = Ar_9 S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-4) = ? S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-5) = Ar_15 S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-6) = Ar_16 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-0) = Ar_0 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-1) = Ar_7 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-2) = Ar_8 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-3) = Ar_9 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-4) = Ar_10 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-5) = Ar_15 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-6) = Ar_16 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-0) = Ar_0 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-1) = Ar_7 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-2) = Ar_8 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-3) = Ar_9 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-4) = Ar_10 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-5) = Ar_15 S("f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-6) = Ar_16 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-0) = Ar_0 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-1) = Ar_7 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-2) = ? S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-3) = Ar_9 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-4) = ? S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-5) = Ar_15 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-6) = ? S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-0) = Ar_0 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-1) = Ar_7 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-2) = ? S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-3) = Ar_9 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-4) = ? S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-5) = Ar_15 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-6) = ? S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-0) = Ar_0 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-1) = Ar_7 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-2) = 1 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-3) = Ar_9 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-4) = ? S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-5) = Ar_15 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-6) = ? S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-0) = Ar_0 S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-1) = Ar_7 S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-2) = ? S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-3) = Ar_9 S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-4) = ? S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-5) = Ar_15 S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-6) = ? S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-0) = Ar_0 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-1) = Ar_7 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-2) = ? S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-3) = Ar_9 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-4) = ? S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-5) = Ar_15 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-6) = ? S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-0) = Ar_0 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-1) = Ar_7 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-2) = ? S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-3) = Ar_9 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-4) = ? S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-5) = Ar_15 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-6) = ? S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\\ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-0) = Ar_0 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\\ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-1) = Ar_7 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\\ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-2) = ? S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\\ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-3) = Ar_9 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\\ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-4) = ? S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\\ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-5) = Ar_15 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\\ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-6) = 1 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\\ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-0) = Ar_0 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\\ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-1) = Ar_7 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\\ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-2) = ? S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\\ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-3) = Ar_9 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\\ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-4) = Ar_9 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\\ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-5) = Ar_15 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\\ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-6) = 1 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-0) = Ar_0 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-1) = Ar_7 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-2) = ? S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-3) = Ar_9 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-4) = 2 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-5) = Ar_15 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-6) = 1 S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\\ 3*Fresh_26 >= Ar_16 + 1 /\\ 0 >= Ar_10 ]", 0-0) = Ar_0 S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\\ 3*Fresh_26 >= Ar_16 + 1 /\\ 0 >= Ar_10 ]", 0-1) = Ar_7 S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\\ 3*Fresh_26 >= Ar_16 + 1 /\\ 0 >= Ar_10 ]", 0-2) = ? S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\\ 3*Fresh_26 >= Ar_16 + 1 /\\ 0 >= Ar_10 ]", 0-3) = Ar_9 S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\\ 3*Fresh_26 >= Ar_16 + 1 /\\ 0 >= Ar_10 ]", 0-4) = ? S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\\ 3*Fresh_26 >= Ar_16 + 1 /\\ 0 >= Ar_10 ]", 0-5) = Ar_15 S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\\ 3*Fresh_26 >= Ar_16 + 1 /\\ 0 >= Ar_10 ]", 0-6) = ? S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\\ 3*Fresh_17 >= Ar_16 + 1 /\\ Ar_10 >= 2 ]", 0-0) = Ar_0 S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\\ 3*Fresh_17 >= Ar_16 + 1 /\\ Ar_10 >= 2 ]", 0-1) = Ar_7 S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\\ 3*Fresh_17 >= Ar_16 + 1 /\\ Ar_10 >= 2 ]", 0-2) = ? S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\\ 3*Fresh_17 >= Ar_16 + 1 /\\ Ar_10 >= 2 ]", 0-3) = Ar_9 S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\\ 3*Fresh_17 >= Ar_16 + 1 /\\ Ar_10 >= 2 ]", 0-4) = ? S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\\ 3*Fresh_17 >= Ar_16 + 1 /\\ Ar_10 >= 2 ]", 0-5) = Ar_15 S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\\ 3*Fresh_17 >= Ar_16 + 1 /\\ Ar_10 >= 2 ]", 0-6) = ? S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\\ 3*Fresh_8 >= Ar_16 + 1 /\\ Ar_10 = 1 ]", 0-0) = Ar_0 S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\\ 3*Fresh_8 >= Ar_16 + 1 /\\ Ar_10 = 1 ]", 0-1) = Ar_7 S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\\ 3*Fresh_8 >= Ar_16 + 1 /\\ Ar_10 = 1 ]", 0-2) = ? S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\\ 3*Fresh_8 >= Ar_16 + 1 /\\ Ar_10 = 1 ]", 0-3) = Ar_9 S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\\ 3*Fresh_8 >= Ar_16 + 1 /\\ Ar_10 = 1 ]", 0-4) = 2 S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\\ 3*Fresh_8 >= Ar_16 + 1 /\\ Ar_10 = 1 ]", 0-5) = Ar_15 S("f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\\ 3*Fresh_8 >= Ar_16 + 1 /\\ Ar_10 = 1 ]", 0-6) = ? S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-0) = Ar_0 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-1) = Ar_7 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-2) = ? S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-3) = Ar_9 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-4) = ? S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-5) = Ar_15 S("f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-6) = ? S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-0) = Ar_0 S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-1) = Ar_7 S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-2) = ? S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-3) = Ar_9 S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-4) = ? S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-5) = Ar_15 S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-6) = ? S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-0) = Ar_0 + 1 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-1) = Ar_7 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-2) = ? S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-3) = Ar_9 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-4) = ? S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-5) = Ar_15 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-6) = ? S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-0) = Ar_0 + 1 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-1) = Ar_7 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-2) = ? S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-3) = Ar_9 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-4) = ? S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-5) = Ar_15 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-6) = ? S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-0) = 1 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-1) = Ar_7 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-2) = ? S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-3) = Ar_9 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-4) = ? S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-5) = Ar_15 S("f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-6) = ? S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-0) = 1 S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-1) = Ar_7 S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-2) = ? S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-3) = Ar_9 S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-4) = ? S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-5) = Ar_15 S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-6) = Ar_16 S("f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-0) = 1 S("f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-1) = Ar_7 S("f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-2) = ? S("f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-3) = Ar_9 S("f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-4) = ? S("f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-5) = Ar_15 S("f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-6) = Ar_16 S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-0) = Ar_0 S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-1) = Ar_7 S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-2) = Ar_8 S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-3) = Ar_9 S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-4) = Ar_10 S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-5) = Ar_15 S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-6) = Ar_16 orients the transitions f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\ 3*Fresh_8 >= Ar_16 + 1 /\ Ar_10 = 1 ] f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\ 3*Fresh_26 >= Ar_16 + 1 /\ 0 >= Ar_10 ] f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\ 3*Fresh_17 >= Ar_16 + 1 /\ Ar_10 >= 2 ] f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ] f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ] f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ] f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ] f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ] f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ] f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ] f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ] f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ] f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ] weakly and the transitions f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ] f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ] strictly and produces the following problem: 10: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ] (Comp: 65*Ar_7 + 63*Ar_8 + 3, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ] (Comp: 65*Ar_7 + 63*Ar_8 + 3, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\ 3*Fresh_8 >= Ar_16 + 1 /\ Ar_10 = 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\ 3*Fresh_17 >= Ar_16 + 1 /\ Ar_10 >= 2 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\ 3*Fresh_26 >= Ar_16 + 1 /\ 0 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ] (Comp: 17*Ar_7 + 15*Ar_8, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = 5*V_4 - 5*V_5 + 1 Pol(f2) = 5*V_4 - 5*V_5 + 1 Pol(f13) = 5*V_4 - 5*V_5 + 1 Pol(f27) = 5*V_4 - 5*V_5 + 1 Pol(f16) = 5*V_4 - 5*V_5 + 1 Pol(f1) = 5*V_4 - 5*V_5 Pol(f35) = 5*V_4 - 5*V_5 + 1 Pol(f38) = 5*V_4 - 5*V_5 + 1 Pol(f53) = 5*V_4 - 5*V_5 - 3 orients all transitions weakly and the transitions f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ] f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ] f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ] f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ] f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ] f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ] strictly and produces the following problem: 11: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ] (Comp: 65*Ar_7 + 63*Ar_8 + 3, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ] (Comp: 65*Ar_7 + 63*Ar_8 + 3, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\ 3*Fresh_8 >= Ar_16 + 1 /\ Ar_10 = 1 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\ 3*Fresh_17 >= Ar_16 + 1 /\ Ar_10 >= 2 ] (Comp: ?, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\ 3*Fresh_26 >= Ar_16 + 1 /\ 0 >= Ar_10 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ] (Comp: 17*Ar_7 + 15*Ar_8, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ] start location: koat_start leaf cost: 0 Repeatedly propagating knowledge in problem 11 produces the following problem: 12: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ] (Comp: 65*Ar_7 + 63*Ar_8 + 3, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ] (Comp: 65*Ar_7 + 63*Ar_8 + 3, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\ 3*Fresh_8 >= Ar_16 + 1 /\ Ar_10 = 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\ 3*Fresh_17 >= Ar_16 + 1 /\ Ar_10 >= 2 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\ 3*Fresh_26 >= Ar_16 + 1 /\ 0 >= Ar_10 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ] (Comp: ?, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ] (Comp: 17*Ar_7 + 15*Ar_8, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = 3*V_6 - 2*V_7 Pol(f2) = 3*V_6 - 2*V_7 Pol(f13) = 3*V_6 - 2*V_7 Pol(f27) = 3*V_6 - 2*V_7 Pol(f16) = 3*V_6 - 2*V_7 Pol(f1) = 3*V_6 - 2*V_7 Pol(f35) = 3*V_6 - 2*V_7 Pol(f38) = 3*V_6 - 2*V_7 - 1 Pol(f53) = 3*V_6 - 2*V_7 - 1 orients all transitions weakly and the transition f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ] strictly and produces the following problem: 13: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ] (Comp: 65*Ar_7 + 63*Ar_8 + 3, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ] (Comp: 65*Ar_7 + 63*Ar_8 + 3, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ] (Comp: ?, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\ 3*Fresh_8 >= Ar_16 + 1 /\ Ar_10 = 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\ 3*Fresh_17 >= Ar_16 + 1 /\ Ar_10 >= 2 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\ 3*Fresh_26 >= Ar_16 + 1 /\ 0 >= Ar_10 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ] (Comp: 3*Ar_15 + 2*Ar_16, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ] (Comp: 17*Ar_7 + 15*Ar_8, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ] start location: koat_start leaf cost: 0 Repeatedly propagating knowledge in problem 13 produces the following problem: 14: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ] (Comp: 65*Ar_7 + 63*Ar_8 + 3, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ] (Comp: 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f1(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ] (Comp: 65*Ar_7 + 63*Ar_8 + 3, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ] (Comp: 3*Ar_15 + 2*Ar_16 + 20*Ar_9 + 20*Ar_10 + 4, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_8 /\ 3*Fresh_8 >= Ar_16 + 1 /\ Ar_10 = 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_17 /\ 3*Fresh_17 >= Ar_16 + 1 /\ Ar_10 >= 2 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_16 >= 2*Fresh_26 /\ 3*Fresh_26 >= Ar_16 + 1 /\ 0 >= Ar_10 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_35 /\ 5*Fresh_35 + Ar_10 >= Ar_9 + 1 /\ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 + 4*Fresh_44 /\ 5*Fresh_44 + Ar_10 >= Ar_9 + 1 /\ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f53(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ] (Comp: 3*Ar_15 + 2*Ar_16, Cost: 1) f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f38(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ] (Comp: 17*Ar_7 + 15*Ar_8, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f27(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ] (Comp: 5*Ar_9 + 5*Ar_10 + 1, Cost: 1) f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ] (Comp: 16*Ar_7 + 16*Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ] (Comp: 1, Cost: 1) f2(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f13(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ] start location: koat_start leaf cost: 0 Complexity upper bound 195*Ar_7 + 189*Ar_8 + 6*Ar_15 + 4*Ar_16 + 65*Ar_9 + 65*Ar_10 + 29 Time: 4.705 sec (SMT: 4.366 sec)