MAYBE Initial complexity problem: 1: T: (Comp: ?, Cost: 1) f12(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f16(Ar_0, 1, Fresh_80, Fresh_81, Fresh_82, Ar_6 + 1, Ar_6, Fresh_83, Ar_6, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_0 >= 0 /\ Fresh_80 >= 2 /\ N1 >= Fresh_80 /\ Ar_1 = 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, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f16(Ar_0, Ar_1, Fresh_76, Fresh_77, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_78, Fresh_79, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Fresh_76 >= 2 /\ Ar_8 >= 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, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f16(Ar_0, Ar_1 + 1, Fresh_72, Fresh_73, Fresh_74, Ar_5, Ar_6 - 1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_12, Ar_12, Fresh_75, Ar_1 + 1, Ar_6 - 1, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_1 >= 0 /\ Ar_6 >= 0 /\ Fresh_72 >= 2 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f1(Ar_0 + 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_18, Fresh_70, Ar_18, Fresh_71, Ar_0, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_16 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f16(Ar_6, 0, Fresh_61, Ar_17, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_17, Ar_13, Ar_14, Ar_15, Fresh_62, Fresh_63, Fresh_64, Fresh_65, Ar_20, Ar_21, Fresh_66, Fresh_67, Fresh_68, Fresh_69, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_0 >= Ar_16 /\ Ar_0 >= 0 /\ Fresh_61 >= 2 /\ Fresh_69 >= Fresh_61 /\ Ar_6 >= Fresh_61 /\ Ar_1 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Fresh_59, Fresh_60, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, 0, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, 0, Fresh_60, 0, Fresh_60, Ar_32, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Fresh_59 >= 2 /\ Ar_26 >= 0 /\ Ar_27 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f10(Ar_0, Ar_1, Fresh_50, Fresh_51, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Fresh_52, Ar_25, Ar_26, Fresh_53, Fresh_54, Fresh_55, Fresh_56, Fresh_57, Fresh_58, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Fresh_50 >= 2 /\ Ar_26 >= 0 /\ Ar_27 = Ar_32 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Fresh_47, Fresh_48, Fresh_49, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, 0, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, 0, Fresh_48, 0, Fresh_48, Ar_32, Ar_32, Ar_33 - 1, Ar_33 - 1, Ar_35, Ar_36, Ar_37)) [ Fresh_47 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f10(Ar_0, Ar_1, Fresh_39, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Fresh_40, Ar_25, Ar_26, Fresh_41, Fresh_42, Fresh_43, Fresh_44, Fresh_45, Fresh_46, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Fresh_39 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = Ar_32 ] (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, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_33 + 1, Fresh_38, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, 0, Ar_9, Ar_10, Ar_11, 0, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_33, 0, Ar_3, 0, Ar_3, Ar_3, Ar_3, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ O1 >= 2 /\ Fresh_38 >= 2 /\ Ar_12 = 0 /\ Ar_8 = 0 /\ Ar_1 = 1 ] (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, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_33 + 1, Fresh_37, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, 0, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_33, 0, Ar_3, 0, Ar_3, Ar_3, Ar_3, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ O1 >= 2 /\ Fresh_37 >= 2 /\ Ar_1 >= 0 /\ Ar_6 >= 0 /\ Ar_12 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f1(2, Ar_1, Fresh_32, 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, Fresh_32, Fresh_33, Fresh_34, Fresh_33, Ar_20, Ar_21, Fresh_33, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Fresh_35, Fresh_36, 2)) [ Fresh_32 >= 2 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f10(Fresh_16, Ar_1, Fresh_17, 0, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, 0, Ar_13, Ar_14, Ar_15, Fresh_18, Fresh_19, Fresh_20, Fresh_21, Ar_20, Ar_21, Fresh_22, Fresh_23, Fresh_24, Ar_25, Ar_26, Fresh_25, Fresh_26, Fresh_27, Fresh_28, Fresh_29, Fresh_30, Ar_33, Ar_34, Fresh_31, Ar_36, Ar_37)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_17 /\ 0 >= X1' ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f10(Fresh_0, Ar_1, 1, Fresh_1, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, 0, Ar_13, Ar_14, Ar_15, Fresh_2, Fresh_3, Fresh_4, Fresh_5, Ar_20, Ar_21, Fresh_6, Fresh_7, Fresh_8, Ar_25, Ar_26, Fresh_9, Fresh_10, Fresh_11, Fresh_12, Fresh_13, Fresh_14, Ar_33, Ar_34, Fresh_15, Ar_36, Ar_37)) [ Ar_18 = 0 ] (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33]. We thus obtain the following problem: 2: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33)) [ 0 <= 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Fresh_0, Ar_1, Fresh_1, Ar_6, Ar_8, 0, Fresh_2, Fresh_3, Fresh_4, Ar_26, Fresh_9, Fresh_14, Ar_33)) [ Ar_18 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Fresh_16, Ar_1, 0, Ar_6, Ar_8, 0, Fresh_18, Fresh_19, Fresh_20, Ar_26, Fresh_25, Fresh_30, Ar_33)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_17 /\ 0 >= X1' ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f1(2, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Fresh_32, Fresh_33, Fresh_34, Ar_26, Ar_27, Ar_32, Ar_33)) [ Fresh_32 >= 2 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_33 + 1, Ar_3, Ar_6, Ar_8, 0, Ar_16, Ar_17, Ar_18, Ar_33, 0, Ar_3, Ar_33)) [ O1 >= 2 /\ Fresh_37 >= 2 /\ Ar_1 >= 0 /\ Ar_6 >= 0 /\ Ar_12 = 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_33 + 1, Ar_3, Ar_6, 0, 0, Ar_16, Ar_17, Ar_18, Ar_33, 0, Ar_3, Ar_33)) [ O1 >= 2 /\ Fresh_38 >= 2 /\ Ar_12 = 0 /\ Ar_8 = 0 /\ Ar_1 = 1 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Fresh_41, Fresh_46, Ar_33)) [ Fresh_39 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = Ar_32 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_1, Fresh_48, Ar_6, Ar_8, 0, Ar_16, Ar_17, Ar_18, Ar_26, 0, Ar_32, Ar_33 - 1)) [ Fresh_47 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Ar_0, Ar_1, Fresh_51, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Fresh_53, Fresh_58, Ar_33)) [ Fresh_50 >= 2 /\ Ar_26 >= 0 /\ Ar_27 = Ar_32 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_1, Fresh_60, Ar_6, Ar_8, 0, Ar_16, Ar_17, Ar_18, Ar_26, 0, Ar_32, Ar_33)) [ Fresh_59 >= 2 /\ Ar_26 >= 0 /\ Ar_27 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_6, 0, Ar_17, Ar_6, Ar_8, Ar_17, Fresh_62, Fresh_63, Fresh_64, Ar_26, Ar_27, Ar_32, Ar_33)) [ Ar_0 >= Ar_16 /\ Ar_0 >= 0 /\ Fresh_61 >= 2 /\ Fresh_69 >= Fresh_61 /\ Ar_6 >= Fresh_61 /\ Ar_1 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_18, Fresh_70, Ar_26, Ar_27, Ar_32, Ar_33)) [ Ar_16 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_0, Ar_1 + 1, Fresh_73, Ar_6 - 1, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33)) [ Ar_1 >= 0 /\ Ar_6 >= 0 /\ Fresh_72 >= 2 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_0, Ar_1, Fresh_77, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33)) [ Fresh_76 >= 2 /\ Ar_8 >= 0 ] (Comp: ?, Cost: 1) f12(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_0, 1, Fresh_81, Ar_6, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33)) [ Ar_0 >= 0 /\ Fresh_80 >= 2 /\ N1 >= Fresh_80 /\ Ar_1 = 1 ] start location: koat_start leaf cost: 0 Testing for reachability in the complexity graph removes the following transitions from problem 2: f13(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_33 + 1, Ar_3, Ar_6, 0, 0, Ar_16, Ar_17, Ar_18, Ar_33, 0, Ar_3, Ar_33)) [ O1 >= 2 /\ Fresh_38 >= 2 /\ Ar_12 = 0 /\ Ar_8 = 0 /\ Ar_1 = 1 ] f7(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Ar_0, Ar_1, Fresh_51, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Fresh_53, Fresh_58, Ar_33)) [ Fresh_50 >= 2 /\ Ar_26 >= 0 /\ Ar_27 = Ar_32 ] f7(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_1, Fresh_60, Ar_6, Ar_8, 0, Ar_16, Ar_17, Ar_18, Ar_26, 0, Ar_32, Ar_33)) [ Fresh_59 >= 2 /\ Ar_26 >= 0 /\ Ar_27 = 0 ] f13(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_0, Ar_1, Fresh_77, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33)) [ Fresh_76 >= 2 /\ Ar_8 >= 0 ] f12(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_0, 1, Fresh_81, Ar_6, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33)) [ Ar_0 >= 0 /\ Fresh_80 >= 2 /\ N1 >= Fresh_80 /\ Ar_1 = 1 ] We thus obtain the following problem: 3: T: (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_1, Fresh_48, Ar_6, Ar_8, 0, Ar_16, Ar_17, Ar_18, Ar_26, 0, Ar_32, Ar_33 - 1)) [ Fresh_47 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Fresh_41, Fresh_46, Ar_33)) [ Fresh_39 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = Ar_32 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_0, Ar_1 + 1, Fresh_73, Ar_6 - 1, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33)) [ Ar_1 >= 0 /\ Ar_6 >= 0 /\ Fresh_72 >= 2 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_33 + 1, Ar_3, Ar_6, Ar_8, 0, Ar_16, Ar_17, Ar_18, Ar_33, 0, Ar_3, Ar_33)) [ O1 >= 2 /\ Fresh_37 >= 2 /\ Ar_1 >= 0 /\ Ar_6 >= 0 /\ Ar_12 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_18, Fresh_70, Ar_26, Ar_27, Ar_32, Ar_33)) [ Ar_16 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_6, 0, Ar_17, Ar_6, Ar_8, Ar_17, Fresh_62, Fresh_63, Fresh_64, Ar_26, Ar_27, Ar_32, Ar_33)) [ Ar_0 >= Ar_16 /\ Ar_0 >= 0 /\ Fresh_61 >= 2 /\ Fresh_69 >= Fresh_61 /\ Ar_6 >= Fresh_61 /\ Ar_1 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f1(2, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Fresh_32, Fresh_33, Fresh_34, Ar_26, Ar_27, Ar_32, Ar_33)) [ Fresh_32 >= 2 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Fresh_16, Ar_1, 0, Ar_6, Ar_8, 0, Fresh_18, Fresh_19, Fresh_20, Ar_26, Fresh_25, Fresh_30, Ar_33)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_17 /\ 0 >= X1' ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Fresh_0, Ar_1, Fresh_1, Ar_6, Ar_8, 0, Fresh_2, Fresh_3, Fresh_4, Ar_26, Fresh_9, Fresh_14, Ar_33)) [ Ar_18 = 0 ] (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33) -> Com_1(f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_8, Ar_12, Ar_16, Ar_17, Ar_18, Ar_26, Ar_27, Ar_32, Ar_33)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Repeatedly propagating knowledge in problem 3 produces the following problem: 4: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Fresh_0, Ar_1, Fresh_1, Ar_6, 0, Fresh_2, Fresh_3, Fresh_4, Fresh_9, Fresh_14, Ar_33)) [ Ar_18 = 0 ] (Comp: 1, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Fresh_16, Ar_1, 0, Ar_6, 0, Fresh_18, Fresh_19, Fresh_20, Fresh_25, Fresh_30, Ar_33)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_17 /\ 0 >= X1' ] (Comp: 1, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f1(2, Ar_1, Ar_3, Ar_6, Ar_12, Fresh_32, Fresh_33, Fresh_34, Ar_27, Ar_32, Ar_33)) [ Fresh_32 >= 2 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_6, 0, Ar_17, Ar_6, Ar_17, Fresh_62, Fresh_63, Fresh_64, Ar_27, Ar_32, Ar_33)) [ Ar_0 >= Ar_16 /\ Ar_0 >= 0 /\ Fresh_61 >= 2 /\ Fresh_69 >= Fresh_61 /\ Ar_6 >= Fresh_61 /\ Ar_1 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_18, Fresh_70, Ar_27, Ar_32, Ar_33)) [ Ar_16 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_33 + 1, Ar_3, Ar_6, 0, Ar_16, Ar_17, Ar_18, 0, Ar_3, Ar_33)) [ O1 >= 2 /\ Fresh_37 >= 2 /\ Ar_1 >= 0 /\ Ar_6 >= 0 /\ Ar_12 = 0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_0, Ar_1 + 1, Fresh_73, Ar_6 - 1, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33)) [ Ar_1 >= 0 /\ Ar_6 >= 0 /\ Fresh_72 >= 2 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Fresh_41, Fresh_46, Ar_33)) [ Fresh_39 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = Ar_32 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_1, Fresh_48, Ar_6, 0, Ar_16, Ar_17, Ar_18, 0, Ar_32, Ar_33 - 1)) [ Fresh_47 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = 3 Pol(f9) = 3 Pol(f10) = 0 Pol(f1) = 3 Pol(f16) = 2 Pol(f8) = 1 orients all transitions weakly and the transitions f8(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Fresh_41, Fresh_46, Ar_33)) [ Fresh_39 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = Ar_32 ] f16(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_33 + 1, Ar_3, Ar_6, 0, Ar_16, Ar_17, Ar_18, 0, Ar_3, Ar_33)) [ O1 >= 2 /\ Fresh_37 >= 2 /\ Ar_1 >= 0 /\ Ar_6 >= 0 /\ Ar_12 = 0 ] f1(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_6, 0, Ar_17, Ar_6, Ar_17, Fresh_62, Fresh_63, Fresh_64, Ar_27, Ar_32, Ar_33)) [ Ar_0 >= Ar_16 /\ Ar_0 >= 0 /\ Fresh_61 >= 2 /\ Fresh_69 >= Fresh_61 /\ Ar_6 >= Fresh_61 /\ Ar_1 = 0 ] strictly and produces the following problem: 5: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Fresh_0, Ar_1, Fresh_1, Ar_6, 0, Fresh_2, Fresh_3, Fresh_4, Fresh_9, Fresh_14, Ar_33)) [ Ar_18 = 0 ] (Comp: 1, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Fresh_16, Ar_1, 0, Ar_6, 0, Fresh_18, Fresh_19, Fresh_20, Fresh_25, Fresh_30, Ar_33)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_17 /\ 0 >= X1' ] (Comp: 1, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f1(2, Ar_1, Ar_3, Ar_6, Ar_12, Fresh_32, Fresh_33, Fresh_34, Ar_27, Ar_32, Ar_33)) [ Fresh_32 >= 2 ] (Comp: 3, Cost: 1) f1(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_6, 0, Ar_17, Ar_6, Ar_17, Fresh_62, Fresh_63, Fresh_64, Ar_27, Ar_32, Ar_33)) [ Ar_0 >= Ar_16 /\ Ar_0 >= 0 /\ Fresh_61 >= 2 /\ Fresh_69 >= Fresh_61 /\ Ar_6 >= Fresh_61 /\ Ar_1 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_18, Fresh_70, Ar_27, Ar_32, Ar_33)) [ Ar_16 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: 3, Cost: 1) f16(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_33 + 1, Ar_3, Ar_6, 0, Ar_16, Ar_17, Ar_18, 0, Ar_3, Ar_33)) [ O1 >= 2 /\ Fresh_37 >= 2 /\ Ar_1 >= 0 /\ Ar_6 >= 0 /\ Ar_12 = 0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_0, Ar_1 + 1, Fresh_73, Ar_6 - 1, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33)) [ Ar_1 >= 0 /\ Ar_6 >= 0 /\ Fresh_72 >= 2 ] (Comp: 3, Cost: 1) f8(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Fresh_41, Fresh_46, Ar_33)) [ Fresh_39 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = Ar_32 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_1, Fresh_48, Ar_6, 0, Ar_16, Ar_17, Ar_18, 0, Ar_32, Ar_33 - 1)) [ Fresh_47 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = V_11 + 1 Pol(f9) = V_11 + 1 Pol(f10) = V_11 Pol(f1) = V_11 + 1 Pol(f16) = V_11 + 1 Pol(f8) = V_11 + 1 orients all transitions weakly and the transition f8(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_1, Fresh_48, Ar_6, 0, Ar_16, Ar_17, Ar_18, 0, Ar_32, Ar_33 - 1)) [ Fresh_47 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = 0 ] strictly and produces the following problem: 6: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Fresh_0, Ar_1, Fresh_1, Ar_6, 0, Fresh_2, Fresh_3, Fresh_4, Fresh_9, Fresh_14, Ar_33)) [ Ar_18 = 0 ] (Comp: 1, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Fresh_16, Ar_1, 0, Ar_6, 0, Fresh_18, Fresh_19, Fresh_20, Fresh_25, Fresh_30, Ar_33)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_17 /\ 0 >= X1' ] (Comp: 1, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f1(2, Ar_1, Ar_3, Ar_6, Ar_12, Fresh_32, Fresh_33, Fresh_34, Ar_27, Ar_32, Ar_33)) [ Fresh_32 >= 2 ] (Comp: 3, Cost: 1) f1(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_6, 0, Ar_17, Ar_6, Ar_17, Fresh_62, Fresh_63, Fresh_64, Ar_27, Ar_32, Ar_33)) [ Ar_0 >= Ar_16 /\ Ar_0 >= 0 /\ Fresh_61 >= 2 /\ Fresh_69 >= Fresh_61 /\ Ar_6 >= Fresh_61 /\ Ar_1 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_18, Fresh_70, Ar_27, Ar_32, Ar_33)) [ Ar_16 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: 3, Cost: 1) f16(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_33 + 1, Ar_3, Ar_6, 0, Ar_16, Ar_17, Ar_18, 0, Ar_3, Ar_33)) [ O1 >= 2 /\ Fresh_37 >= 2 /\ Ar_1 >= 0 /\ Ar_6 >= 0 /\ Ar_12 = 0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_0, Ar_1 + 1, Fresh_73, Ar_6 - 1, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33)) [ Ar_1 >= 0 /\ Ar_6 >= 0 /\ Fresh_72 >= 2 ] (Comp: 3, Cost: 1) f8(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Fresh_41, Fresh_46, Ar_33)) [ Fresh_39 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = Ar_32 ] (Comp: Ar_33 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_1, Fresh_48, Ar_6, 0, Ar_16, Ar_17, Ar_18, 0, Ar_32, Ar_33 - 1)) [ Fresh_47 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = -V_2 + V_4 + 1 Pol(f9) = -V_2 + V_4 + 1 Pol(f10) = -V_2 + V_4 Pol(f1) = -V_2 + V_4 + 1 Pol(f16) = V_4 + 1 Pol(f8) = -V_2 + V_4 + V_11 orients all transitions weakly and the transition f16(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_0, Ar_1 + 1, Fresh_73, Ar_6 - 1, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33)) [ Ar_1 >= 0 /\ Ar_6 >= 0 /\ Fresh_72 >= 2 ] strictly and produces the following problem: 7: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Fresh_0, Ar_1, Fresh_1, Ar_6, 0, Fresh_2, Fresh_3, Fresh_4, Fresh_9, Fresh_14, Ar_33)) [ Ar_18 = 0 ] (Comp: 1, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Fresh_16, Ar_1, 0, Ar_6, 0, Fresh_18, Fresh_19, Fresh_20, Fresh_25, Fresh_30, Ar_33)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_17 /\ 0 >= X1' ] (Comp: 1, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f1(2, Ar_1, Ar_3, Ar_6, Ar_12, Fresh_32, Fresh_33, Fresh_34, Ar_27, Ar_32, Ar_33)) [ Fresh_32 >= 2 ] (Comp: 3, Cost: 1) f1(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_6, 0, Ar_17, Ar_6, Ar_17, Fresh_62, Fresh_63, Fresh_64, Ar_27, Ar_32, Ar_33)) [ Ar_0 >= Ar_16 /\ Ar_0 >= 0 /\ Fresh_61 >= 2 /\ Fresh_69 >= Fresh_61 /\ Ar_6 >= Fresh_61 /\ Ar_1 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_18, Fresh_70, Ar_27, Ar_32, Ar_33)) [ Ar_16 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: 3, Cost: 1) f16(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_33 + 1, Ar_3, Ar_6, 0, Ar_16, Ar_17, Ar_18, 0, Ar_3, Ar_33)) [ O1 >= 2 /\ Fresh_37 >= 2 /\ Ar_1 >= 0 /\ Ar_6 >= 0 /\ Ar_12 = 0 ] (Comp: Ar_1 + Ar_6 + 1, Cost: 1) f16(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_0, Ar_1 + 1, Fresh_73, Ar_6 - 1, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33)) [ Ar_1 >= 0 /\ Ar_6 >= 0 /\ Fresh_72 >= 2 ] (Comp: 3, Cost: 1) f8(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Fresh_41, Fresh_46, Ar_33)) [ Fresh_39 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = Ar_32 ] (Comp: Ar_33 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_1, Fresh_48, Ar_6, 0, Ar_16, Ar_17, Ar_18, 0, Ar_32, Ar_33 - 1)) [ Fresh_47 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = 0 ] start location: koat_start leaf cost: 0 Applied AI with 'oct' on problem 7 to obtain the following invariants: For symbol f1: X_6 - 2 >= 0 /\ X_1 + X_6 - 4 >= 0 /\ -X_1 + X_6 >= 0 /\ X_1 - 2 >= 0 For symbol f16: X_1 - X_4 >= 0 /\ X_2 + X_4 - 2 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 2 >= 0 For symbol f8: -X_9 >= 0 /\ X_5 - X_9 >= 0 /\ -X_5 - X_9 >= 0 /\ X_4 - X_9 >= 0 /\ X_1 - X_9 - 2 >= 0 /\ X_9 >= 0 /\ X_5 + X_9 >= 0 /\ -X_5 + X_9 >= 0 /\ X_4 + X_9 >= 0 /\ X_1 + X_9 - 2 >= 0 /\ -X_5 >= 0 /\ X_4 - X_5 >= 0 /\ X_1 - X_5 - 2 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 >= 0 /\ X_1 + X_5 - 2 >= 0 /\ X_1 - X_4 >= 0 /\ X_4 >= 0 /\ X_1 + X_4 - 2 >= 0 /\ -X_11 + X_2 - 1 >= 0 /\ X_1 - 2 >= 0 This yielded the following problem: 8: T: (Comp: Ar_33 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_1, Fresh_48, Ar_6, 0, Ar_16, Ar_17, Ar_18, 0, Ar_32, Ar_33 - 1)) [ -Ar_27 >= 0 /\ Ar_12 - Ar_27 >= 0 /\ -Ar_12 - Ar_27 >= 0 /\ Ar_6 - Ar_27 >= 0 /\ Ar_0 - Ar_27 - 2 >= 0 /\ Ar_27 >= 0 /\ Ar_12 + Ar_27 >= 0 /\ -Ar_12 + Ar_27 >= 0 /\ Ar_6 + Ar_27 >= 0 /\ Ar_0 + Ar_27 - 2 >= 0 /\ -Ar_12 >= 0 /\ Ar_6 - Ar_12 >= 0 /\ Ar_0 - Ar_12 - 2 >= 0 /\ Ar_12 >= 0 /\ Ar_6 + Ar_12 >= 0 /\ Ar_0 + Ar_12 - 2 >= 0 /\ Ar_0 - Ar_6 >= 0 /\ Ar_6 >= 0 /\ Ar_0 + Ar_6 - 2 >= 0 /\ -Ar_33 + Ar_1 - 1 >= 0 /\ Ar_0 - 2 >= 0 /\ Fresh_47 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = 0 ] (Comp: 3, Cost: 1) f8(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Fresh_41, Fresh_46, Ar_33)) [ -Ar_27 >= 0 /\ Ar_12 - Ar_27 >= 0 /\ -Ar_12 - Ar_27 >= 0 /\ Ar_6 - Ar_27 >= 0 /\ Ar_0 - Ar_27 - 2 >= 0 /\ Ar_27 >= 0 /\ Ar_12 + Ar_27 >= 0 /\ -Ar_12 + Ar_27 >= 0 /\ Ar_6 + Ar_27 >= 0 /\ Ar_0 + Ar_27 - 2 >= 0 /\ -Ar_12 >= 0 /\ Ar_6 - Ar_12 >= 0 /\ Ar_0 - Ar_12 - 2 >= 0 /\ Ar_12 >= 0 /\ Ar_6 + Ar_12 >= 0 /\ Ar_0 + Ar_12 - 2 >= 0 /\ Ar_0 - Ar_6 >= 0 /\ Ar_6 >= 0 /\ Ar_0 + Ar_6 - 2 >= 0 /\ -Ar_33 + Ar_1 - 1 >= 0 /\ Ar_0 - 2 >= 0 /\ Fresh_39 >= 2 /\ Ar_33 >= 0 /\ Ar_27 = Ar_32 ] (Comp: Ar_1 + Ar_6 + 1, Cost: 1) f16(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_0, Ar_1 + 1, Fresh_73, Ar_6 - 1, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33)) [ Ar_0 - Ar_6 >= 0 /\ Ar_1 + Ar_6 - 2 >= 0 /\ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 2 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_6 >= 0 /\ Fresh_72 >= 2 ] (Comp: 3, Cost: 1) f16(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f8(Ar_0, Ar_33 + 1, Ar_3, Ar_6, 0, Ar_16, Ar_17, Ar_18, 0, Ar_3, Ar_33)) [ Ar_0 - Ar_6 >= 0 /\ Ar_1 + Ar_6 - 2 >= 0 /\ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 2 >= 0 /\ Ar_0 - 2 >= 0 /\ O1 >= 2 /\ Fresh_37 >= 2 /\ Ar_6 >= 0 /\ Ar_12 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_18, Fresh_70, Ar_27, Ar_32, Ar_33)) [ Ar_16 - 2 >= 0 /\ Ar_0 + Ar_16 - 4 >= 0 /\ -Ar_0 + Ar_16 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_16 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: 3, Cost: 1) f1(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f16(Ar_6, 0, Ar_17, Ar_6, Ar_17, Fresh_62, Fresh_63, Fresh_64, Ar_27, Ar_32, Ar_33)) [ Ar_16 - 2 >= 0 /\ Ar_0 + Ar_16 - 4 >= 0 /\ -Ar_0 + Ar_16 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_0 >= Ar_16 /\ Ar_0 >= 0 /\ Fresh_61 >= 2 /\ Fresh_69 >= Fresh_61 /\ Ar_6 >= Fresh_61 /\ Ar_1 = 0 ] (Comp: 1, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f1(2, Ar_1, Ar_3, Ar_6, Ar_12, Fresh_32, Fresh_33, Fresh_34, Ar_27, Ar_32, Ar_33)) [ Fresh_32 >= 2 ] (Comp: 1, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Fresh_16, Ar_1, 0, Ar_6, 0, Fresh_18, Fresh_19, Fresh_20, Fresh_25, Fresh_30, Ar_33)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_17 /\ 0 >= X1' ] (Comp: 1, Cost: 1) f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f10(Fresh_0, Ar_1, Fresh_1, Ar_6, 0, Fresh_2, Fresh_3, Fresh_4, Fresh_9, Fresh_14, Ar_33)) [ Ar_18 = 0 ] (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33) -> Com_1(f9(Ar_0, Ar_1, Ar_3, Ar_6, Ar_12, Ar_16, Ar_17, Ar_18, Ar_27, Ar_32, Ar_33)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Complexity upper bound ? Time: 5.468 sec (SMT: 5.139 sec)