MAYBE

Initial complexity problem:
1:	T:
		(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) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_3, Fresh_103, Ar_3, Fresh_104, Ar_1, 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_0 >= Ar_1 + 1 /\ 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) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, 0, Fresh_101, Fresh_102, Fresh_102, 0, Fresh_102, Ar_7, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24)) [ B1 >= Ar_7 + 1 /\ Ar_8 >= 0 /\ Fresh_102 >= B1 + 1 /\ Fresh_101 >= 2 /\ Ar_9 = 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) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, 0, Fresh_99, Fresh_100, Fresh_100, 0, Fresh_100, Ar_7, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24)) [ B1 >= Ar_7 + 1 /\ Ar_8 >= 0 /\ B1 >= Fresh_100 + 1 /\ Fresh_99 >= 2 /\ Ar_9 = 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) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, 0, Fresh_97, Fresh_98, Fresh_98, 0, Fresh_98, Ar_7, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24)) [ Ar_7 >= B1 + 1 /\ Ar_8 >= 0 /\ Fresh_98 >= B1 + 1 /\ Fresh_97 >= 2 /\ Ar_9 = 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) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, 0, Fresh_95, Fresh_96, Fresh_96, 0, Fresh_96, Ar_7, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24)) [ Ar_7 >= B1 + 1 /\ Ar_8 >= 0 /\ B1 >= Fresh_96 + 1 /\ Fresh_95 >= 2 /\ Ar_9 = 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) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Fresh_86, Ar_8, Fresh_87, Fresh_88, Fresh_89, Fresh_90, Fresh_91, Fresh_92, Fresh_93, Fresh_94, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24)) [ Ar_8 >= 0 /\ 0 >= Fresh_89 + 1 /\ Fresh_88 >= 2 /\ Ar_9 = Ar_7 ]
		(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) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Fresh_77, Ar_8, Fresh_78, Fresh_79, Fresh_80, Fresh_81, Fresh_82, Fresh_83, Fresh_84, Fresh_85, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24)) [ Ar_8 >= 0 /\ Fresh_80 >= 1 /\ Fresh_79 >= 2 /\ Ar_9 = Ar_7 ]
		(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) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, 0, Fresh_74, Fresh_75, Fresh_75, 0, Fresh_75, Ar_7, Ar_16, Ar_17 - 1, Fresh_76, Ar_17 - 1, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24)) [ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ Fresh_75 >= C1 + 1 /\ Fresh_74 >= 2 /\ Ar_9 = 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) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, 0, Fresh_71, Fresh_72, Fresh_72, 0, Fresh_72, Ar_7, Ar_16, Ar_17 - 1, Fresh_73, Ar_17 - 1, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24)) [ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_72 + 1 /\ Fresh_71 >= 2 /\ Ar_9 = 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) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, 0, Fresh_68, Fresh_69, Fresh_69, 0, Fresh_69, Ar_7, Ar_16, Ar_17 - 1, Fresh_70, Ar_17 - 1, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24)) [ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ Fresh_69 >= C1 + 1 /\ Fresh_68 >= 2 /\ Ar_9 = 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) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, 0, Fresh_65, Fresh_66, Fresh_66, 0, Fresh_66, Ar_7, Ar_16, Ar_17 - 1, Fresh_67, Ar_17 - 1, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24)) [ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_66 + 1 /\ Fresh_65 >= 2 /\ Ar_9 = 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) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Fresh_57, Ar_8, Fresh_58, Fresh_59, Ar_11, Fresh_60, Fresh_61, Fresh_62, Fresh_63, Fresh_64, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24)) [ Fresh_59 >= 2 /\ Ar_17 >= 0 /\ Ar_9 = Ar_7 ]
		(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) -> Com_1(f10(Fresh_41, Fresh_42, Fresh_43, Fresh_44, Fresh_45, Ar_5, Ar_6, Fresh_46, Ar_8, Fresh_47, Fresh_48, 0, Fresh_49, Fresh_50, Fresh_51, Fresh_52, Fresh_53, Ar_17, Ar_18, Ar_19, Fresh_54, Fresh_55, Fresh_56, Ar_23, Ar_24)) [ 0 >= I1 /\ 0 >= Fresh_48 /\ 0 >= J1 ]
		(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) -> Com_1(f1(Fresh_36, 2, Fresh_37, Fresh_38, Fresh_37, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Fresh_36, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Fresh_39, Ar_21, Fresh_37, Fresh_40, Ar_24)) [ Fresh_36 >= 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) -> Com_1(f8(Fresh_27, Fresh_28, Fresh_29, Fresh_30, Fresh_31, Ar_5, Ar_6, Ar_2, Ar_17, 0, Fresh_32, Ar_2, Ar_2, 0, Ar_2, Ar_2, Fresh_33, Ar_17, Ar_18, Ar_19, Ar_20, Fresh_34, Fresh_35, Ar_23, Ar_17 + 1)) [ K1 >= Fresh_32 /\ L1 >= 2 /\ Fresh_28 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_2 >= 1 /\ Fresh_28 >= 0 /\ Fresh_32 >= 2 /\ 0 >= Ar_2 + 1 ]
		(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) -> Com_1(f8(Fresh_18, Fresh_19, Fresh_20, Fresh_21, Fresh_22, Ar_5, Ar_6, Ar_2, Ar_17, 0, Fresh_23, Ar_2, Ar_2, 0, Ar_2, Ar_2, Fresh_24, Ar_17, Ar_18, Ar_19, Ar_20, Fresh_25, Fresh_26, Ar_23, Ar_17 + 1)) [ K1 >= Fresh_23 /\ L1 >= 2 /\ Fresh_19 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_2 >= 1 /\ Fresh_19 >= 0 /\ Fresh_23 >= 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) -> Com_1(f8(Fresh_9, Fresh_10, Fresh_11, Fresh_12, Fresh_13, Ar_5, Ar_6, Ar_2, Ar_17, 0, Fresh_14, Ar_2, Ar_2, 0, Ar_2, Ar_2, Fresh_15, Ar_17, Ar_18, Ar_19, Ar_20, Fresh_16, Fresh_17, Ar_23, Ar_17 + 1)) [ K1 >= Fresh_14 /\ L1 >= 2 /\ Fresh_10 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ 0 >= Ar_2 + 1 /\ Fresh_10 >= 0 /\ Fresh_14 >= 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) -> Com_1(f8(Fresh_0, Fresh_1, Fresh_2, Fresh_3, Fresh_4, Ar_5, Ar_6, Ar_2, Ar_17, 0, Fresh_5, Ar_2, Ar_2, 0, Ar_2, Ar_2, Fresh_6, Ar_17, Ar_18, Ar_19, Ar_20, Fresh_7, Fresh_8, Ar_23, Ar_17 + 1)) [ K1 >= Fresh_5 /\ L1 >= 2 /\ Fresh_1 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ 0 >= Ar_2 + 1 /\ Fresh_1 >= 0 /\ Fresh_5 >= 2 /\ Ar_2 >= 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, Ar_23, Ar_24) -> 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)) [ 0 <= 0 ]
	start location:	koat_start
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17].
We thus obtain the following problem:
2:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17)) [ 0 <= 0 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Fresh_0, Fresh_1, Fresh_2, Fresh_3, Ar_2, Ar_17, 0, Ar_17)) [ K1 >= Fresh_5 /\ L1 >= 2 /\ Fresh_1 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ 0 >= Ar_2 + 1 /\ Fresh_1 >= 0 /\ Fresh_5 >= 2 /\ Ar_2 >= 1 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Fresh_9, Fresh_10, Fresh_11, Fresh_12, Ar_2, Ar_17, 0, Ar_17)) [ K1 >= Fresh_14 /\ L1 >= 2 /\ Fresh_10 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ 0 >= Ar_2 + 1 /\ Fresh_10 >= 0 /\ Fresh_14 >= 2 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Fresh_18, Fresh_19, Fresh_20, Fresh_21, Ar_2, Ar_17, 0, Ar_17)) [ K1 >= Fresh_23 /\ L1 >= 2 /\ Fresh_19 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_2 >= 1 /\ Fresh_19 >= 0 /\ Fresh_23 >= 2 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Fresh_27, Fresh_28, Fresh_29, Fresh_30, Ar_2, Ar_17, 0, Ar_17)) [ K1 >= Fresh_32 /\ L1 >= 2 /\ Fresh_28 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_2 >= 1 /\ Fresh_28 >= 0 /\ Fresh_32 >= 2 /\ 0 >= Ar_2 + 1 ]
		(Comp: ?, Cost: 1)    f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f1(Fresh_36, 2, Fresh_37, Fresh_38, Ar_7, Ar_8, Ar_9, Ar_17)) [ Fresh_36 >= 2 ]
		(Comp: ?, Cost: 1)    f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f10(Fresh_41, Fresh_42, Fresh_43, Fresh_44, Fresh_46, Ar_8, Fresh_47, Ar_17)) [ 0 >= I1 /\ 0 >= Fresh_48 /\ 0 >= J1 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Fresh_57, Ar_8, Fresh_58, Ar_17)) [ Fresh_59 >= 2 /\ Ar_17 >= 0 /\ Ar_9 = Ar_7 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, 0, Ar_17 - 1)) [ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_66 + 1 /\ Fresh_65 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, 0, Ar_17 - 1)) [ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ Fresh_69 >= C1 + 1 /\ Fresh_68 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, 0, Ar_17 - 1)) [ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_72 + 1 /\ Fresh_71 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, 0, Ar_17 - 1)) [ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ Fresh_75 >= C1 + 1 /\ Fresh_74 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Fresh_77, Ar_8, Fresh_78, Ar_17)) [ Ar_8 >= 0 /\ Fresh_80 >= 1 /\ Fresh_79 >= 2 /\ Ar_9 = Ar_7 ]
		(Comp: ?, Cost: 1)    f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Fresh_86, Ar_8, Fresh_87, Ar_17)) [ Ar_8 >= 0 /\ 0 >= Fresh_89 + 1 /\ Fresh_88 >= 2 /\ Ar_9 = Ar_7 ]
		(Comp: ?, Cost: 1)    f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, 0, Ar_17)) [ Ar_7 >= B1 + 1 /\ Ar_8 >= 0 /\ B1 >= Fresh_96 + 1 /\ Fresh_95 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, 0, Ar_17)) [ Ar_7 >= B1 + 1 /\ Ar_8 >= 0 /\ Fresh_98 >= B1 + 1 /\ Fresh_97 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, 0, Ar_17)) [ B1 >= Ar_7 + 1 /\ Ar_8 >= 0 /\ B1 >= Fresh_100 + 1 /\ Fresh_99 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, 0, Ar_17)) [ B1 >= Ar_7 + 1 /\ Ar_8 >= 0 /\ Fresh_102 >= B1 + 1 /\ Fresh_101 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_3, Fresh_103, Ar_7, Ar_8, Ar_9, Ar_17)) [ Ar_0 >= Ar_1 + 1 /\ Ar_1 >= 0 ]
	start location:	koat_start
	leaf cost:	0

Testing for reachability in the complexity graph removes the following transitions from problem 2:
	f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Fresh_0, Fresh_1, Fresh_2, Fresh_3, Ar_2, Ar_17, 0, Ar_17)) [ K1 >= Fresh_5 /\ L1 >= 2 /\ Fresh_1 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ 0 >= Ar_2 + 1 /\ Fresh_1 >= 0 /\ Fresh_5 >= 2 /\ Ar_2 >= 1 ]
	f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Fresh_27, Fresh_28, Fresh_29, Fresh_30, Ar_2, Ar_17, 0, Ar_17)) [ K1 >= Fresh_32 /\ L1 >= 2 /\ Fresh_28 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_2 >= 1 /\ Fresh_28 >= 0 /\ Fresh_32 >= 2 /\ 0 >= Ar_2 + 1 ]
	f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Fresh_77, Ar_8, Fresh_78, Ar_17)) [ Ar_8 >= 0 /\ Fresh_80 >= 1 /\ Fresh_79 >= 2 /\ Ar_9 = Ar_7 ]
	f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Fresh_86, Ar_8, Fresh_87, Ar_17)) [ Ar_8 >= 0 /\ 0 >= Fresh_89 + 1 /\ Fresh_88 >= 2 /\ Ar_9 = Ar_7 ]
	f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, 0, Ar_17)) [ Ar_7 >= B1 + 1 /\ Ar_8 >= 0 /\ B1 >= Fresh_96 + 1 /\ Fresh_95 >= 2 /\ Ar_9 = 0 ]
	f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, 0, Ar_17)) [ Ar_7 >= B1 + 1 /\ Ar_8 >= 0 /\ Fresh_98 >= B1 + 1 /\ Fresh_97 >= 2 /\ Ar_9 = 0 ]
	f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, 0, Ar_17)) [ B1 >= Ar_7 + 1 /\ Ar_8 >= 0 /\ B1 >= Fresh_100 + 1 /\ Fresh_99 >= 2 /\ Ar_9 = 0 ]
	f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, 0, Ar_17)) [ B1 >= Ar_7 + 1 /\ Ar_8 >= 0 /\ Fresh_102 >= B1 + 1 /\ Fresh_101 >= 2 /\ Ar_9 = 0 ]
We thus obtain the following problem:
3:	T:
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Fresh_57, Ar_8, Fresh_58, Ar_17)) [ Fresh_59 >= 2 /\ Ar_17 >= 0 /\ Ar_9 = Ar_7 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, 0, Ar_17 - 1)) [ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ Fresh_75 >= C1 + 1 /\ Fresh_74 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, 0, Ar_17 - 1)) [ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_72 + 1 /\ Fresh_71 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, 0, Ar_17 - 1)) [ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ Fresh_69 >= C1 + 1 /\ Fresh_68 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, 0, Ar_17 - 1)) [ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_66 + 1 /\ Fresh_65 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_3, Fresh_103, Ar_7, Ar_8, Ar_9, Ar_17)) [ Ar_0 >= Ar_1 + 1 /\ Ar_1 >= 0 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Fresh_18, Fresh_19, Fresh_20, Fresh_21, Ar_2, Ar_17, 0, Ar_17)) [ K1 >= Fresh_23 /\ L1 >= 2 /\ Fresh_19 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_2 >= 1 /\ Fresh_19 >= 0 /\ Fresh_23 >= 2 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f8(Fresh_9, Fresh_10, Fresh_11, Fresh_12, Ar_2, Ar_17, 0, Ar_17)) [ K1 >= Fresh_14 /\ L1 >= 2 /\ Fresh_10 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ 0 >= Ar_2 + 1 /\ Fresh_10 >= 0 /\ Fresh_14 >= 2 ]
		(Comp: ?, Cost: 1)    f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f10(Fresh_41, Fresh_42, Fresh_43, Fresh_44, Fresh_46, Ar_8, Fresh_47, Ar_17)) [ 0 >= I1 /\ 0 >= Fresh_48 /\ 0 >= J1 ]
		(Comp: ?, Cost: 1)    f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f1(Fresh_36, 2, Fresh_37, Fresh_38, Ar_7, Ar_8, Ar_9, Ar_17)) [ Fresh_36 >= 2 ]
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17) -> Com_1(f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_9, Ar_17)) [ 0 <= 0 ]
	start location:	koat_start
	leaf cost:	0

Repeatedly propagating knowledge in problem 3 produces the following problem:
4:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)    f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f1(Fresh_36, 2, Fresh_37, Fresh_38, Ar_7, Ar_9, Ar_17)) [ Fresh_36 >= 2 ]
		(Comp: 1, Cost: 1)    f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f10(Fresh_41, Fresh_42, Fresh_43, Fresh_44, Fresh_46, Fresh_47, Ar_17)) [ 0 >= I1 /\ 0 >= Fresh_48 /\ 0 >= J1 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Fresh_9, Fresh_10, Fresh_11, Fresh_12, Ar_2, 0, Ar_17)) [ K1 >= Fresh_14 /\ L1 >= 2 /\ Fresh_10 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ 0 >= Ar_2 + 1 /\ Fresh_10 >= 0 /\ Fresh_14 >= 2 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Fresh_18, Fresh_19, Fresh_20, Fresh_21, Ar_2, 0, Ar_17)) [ K1 >= Fresh_23 /\ L1 >= 2 /\ Fresh_19 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_2 >= 1 /\ Fresh_19 >= 0 /\ Fresh_23 >= 2 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_3, Fresh_103, Ar_7, Ar_9, Ar_17)) [ Ar_0 >= Ar_1 + 1 /\ Ar_1 >= 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_66 + 1 /\ Fresh_65 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ Fresh_69 >= C1 + 1 /\ Fresh_68 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_72 + 1 /\ Fresh_71 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ Fresh_75 >= C1 + 1 /\ Fresh_74 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Fresh_57, Fresh_58, Ar_17)) [ Fresh_59 >= 2 /\ Ar_17 >= 0 /\ Ar_9 = Ar_7 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(koat_start) = 1
	Pol(f9) = 1
	Pol(f1) = 1
	Pol(f10) = -1
	Pol(f8) = 0
orients all transitions weakly and the transitions
	f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Fresh_9, Fresh_10, Fresh_11, Fresh_12, Ar_2, 0, Ar_17)) [ K1 >= Fresh_14 /\ L1 >= 2 /\ Fresh_10 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ 0 >= Ar_2 + 1 /\ Fresh_10 >= 0 /\ Fresh_14 >= 2 ]
	f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Fresh_18, Fresh_19, Fresh_20, Fresh_21, Ar_2, 0, Ar_17)) [ K1 >= Fresh_23 /\ L1 >= 2 /\ Fresh_19 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_2 >= 1 /\ Fresh_19 >= 0 /\ Fresh_23 >= 2 ]
strictly and produces the following problem:
5:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)    f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f1(Fresh_36, 2, Fresh_37, Fresh_38, Ar_7, Ar_9, Ar_17)) [ Fresh_36 >= 2 ]
		(Comp: 1, Cost: 1)    f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f10(Fresh_41, Fresh_42, Fresh_43, Fresh_44, Fresh_46, Fresh_47, Ar_17)) [ 0 >= I1 /\ 0 >= Fresh_48 /\ 0 >= J1 ]
		(Comp: 1, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Fresh_9, Fresh_10, Fresh_11, Fresh_12, Ar_2, 0, Ar_17)) [ K1 >= Fresh_14 /\ L1 >= 2 /\ Fresh_10 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ 0 >= Ar_2 + 1 /\ Fresh_10 >= 0 /\ Fresh_14 >= 2 ]
		(Comp: 1, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Fresh_18, Fresh_19, Fresh_20, Fresh_21, Ar_2, 0, Ar_17)) [ K1 >= Fresh_23 /\ L1 >= 2 /\ Fresh_19 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_2 >= 1 /\ Fresh_19 >= 0 /\ Fresh_23 >= 2 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_3, Fresh_103, Ar_7, Ar_9, Ar_17)) [ Ar_0 >= Ar_1 + 1 /\ Ar_1 >= 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_66 + 1 /\ Fresh_65 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ Fresh_69 >= C1 + 1 /\ Fresh_68 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_72 + 1 /\ Fresh_71 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ Fresh_75 >= C1 + 1 /\ Fresh_74 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Fresh_57, Fresh_58, Ar_17)) [ Fresh_59 >= 2 /\ Ar_17 >= 0 /\ Ar_9 = Ar_7 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(koat_start) = 1
	Pol(f9) = 1
	Pol(f1) = 1
	Pol(f10) = 0
	Pol(f8) = 1
orients all transitions weakly and the transition
	f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Fresh_57, Fresh_58, Ar_17)) [ Fresh_59 >= 2 /\ Ar_17 >= 0 /\ Ar_9 = Ar_7 ]
strictly and produces the following problem:
6:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)    f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f1(Fresh_36, 2, Fresh_37, Fresh_38, Ar_7, Ar_9, Ar_17)) [ Fresh_36 >= 2 ]
		(Comp: 1, Cost: 1)    f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f10(Fresh_41, Fresh_42, Fresh_43, Fresh_44, Fresh_46, Fresh_47, Ar_17)) [ 0 >= I1 /\ 0 >= Fresh_48 /\ 0 >= J1 ]
		(Comp: 1, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Fresh_9, Fresh_10, Fresh_11, Fresh_12, Ar_2, 0, Ar_17)) [ K1 >= Fresh_14 /\ L1 >= 2 /\ Fresh_10 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ 0 >= Ar_2 + 1 /\ Fresh_10 >= 0 /\ Fresh_14 >= 2 ]
		(Comp: 1, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Fresh_18, Fresh_19, Fresh_20, Fresh_21, Ar_2, 0, Ar_17)) [ K1 >= Fresh_23 /\ L1 >= 2 /\ Fresh_19 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_2 >= 1 /\ Fresh_19 >= 0 /\ Fresh_23 >= 2 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_3, Fresh_103, Ar_7, Ar_9, Ar_17)) [ Ar_0 >= Ar_1 + 1 /\ Ar_1 >= 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_66 + 1 /\ Fresh_65 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ Fresh_69 >= C1 + 1 /\ Fresh_68 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_72 + 1 /\ Fresh_71 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ Fresh_75 >= C1 + 1 /\ Fresh_74 >= 2 /\ Ar_9 = 0 ]
		(Comp: 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Fresh_57, Fresh_58, Ar_17)) [ Fresh_59 >= 2 /\ Ar_17 >= 0 /\ Ar_9 = Ar_7 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(koat_start) = V_7 + 1
	Pol(f9) = V_7 + 1
	Pol(f1) = V_7 + 1
	Pol(f10) = V_7
	Pol(f8) = V_7 + 1
orients all transitions weakly and the transitions
	f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ Fresh_75 >= C1 + 1 /\ Fresh_74 >= 2 /\ Ar_9 = 0 ]
	f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_72 + 1 /\ Fresh_71 >= 2 /\ Ar_9 = 0 ]
	f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ Fresh_69 >= C1 + 1 /\ Fresh_68 >= 2 /\ Ar_9 = 0 ]
	f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_66 + 1 /\ Fresh_65 >= 2 /\ Ar_9 = 0 ]
strictly and produces the following problem:
7:	T:
		(Comp: 1, Cost: 0)            koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)            f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f1(Fresh_36, 2, Fresh_37, Fresh_38, Ar_7, Ar_9, Ar_17)) [ Fresh_36 >= 2 ]
		(Comp: 1, Cost: 1)            f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f10(Fresh_41, Fresh_42, Fresh_43, Fresh_44, Fresh_46, Fresh_47, Ar_17)) [ 0 >= I1 /\ 0 >= Fresh_48 /\ 0 >= J1 ]
		(Comp: 1, Cost: 1)            f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Fresh_9, Fresh_10, Fresh_11, Fresh_12, Ar_2, 0, Ar_17)) [ K1 >= Fresh_14 /\ L1 >= 2 /\ Fresh_10 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ 0 >= Ar_2 + 1 /\ Fresh_10 >= 0 /\ Fresh_14 >= 2 ]
		(Comp: 1, Cost: 1)            f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Fresh_18, Fresh_19, Fresh_20, Fresh_21, Ar_2, 0, Ar_17)) [ K1 >= Fresh_23 /\ L1 >= 2 /\ Fresh_19 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_2 >= 1 /\ Fresh_19 >= 0 /\ Fresh_23 >= 2 ]
		(Comp: ?, Cost: 1)            f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_3, Fresh_103, Ar_7, Ar_9, Ar_17)) [ Ar_0 >= Ar_1 + 1 /\ Ar_1 >= 0 ]
		(Comp: Ar_17 + 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_66 + 1 /\ Fresh_65 >= 2 /\ Ar_9 = 0 ]
		(Comp: Ar_17 + 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ Fresh_69 >= C1 + 1 /\ Fresh_68 >= 2 /\ Ar_9 = 0 ]
		(Comp: Ar_17 + 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_72 + 1 /\ Fresh_71 >= 2 /\ Ar_9 = 0 ]
		(Comp: Ar_17 + 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ Fresh_75 >= C1 + 1 /\ Fresh_74 >= 2 /\ Ar_9 = 0 ]
		(Comp: 1, Cost: 1)            f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Fresh_57, Fresh_58, Ar_17)) [ Fresh_59 >= 2 /\ Ar_17 >= 0 /\ Ar_9 = Ar_7 ]
	start location:	koat_start
	leaf cost:	0

Applied AI with 'oct' on problem 7 to obtain the following invariants:
  For symbol f1: X_1 - X_2 >= 0 /\ X_2 - 2 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ X_1 - 2 >= 0
  For symbol f8: -X_6 >= 0 /\ X_2 - X_6 - 2 >= 0 /\ X_6 >= 0 /\ X_2 + X_6 - 2 >= 0 /\ X_2 - 2 >= 0


This yielded the following problem:
8:	T:
		(Comp: 1, Cost: 1)            f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Fresh_57, Fresh_58, Ar_17)) [ -Ar_9 >= 0 /\ Ar_1 - Ar_9 - 2 >= 0 /\ Ar_9 >= 0 /\ Ar_1 + Ar_9 - 2 >= 0 /\ Ar_1 - 2 >= 0 /\ Fresh_59 >= 2 /\ Ar_17 >= 0 /\ Ar_9 = Ar_7 ]
		(Comp: Ar_17 + 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ -Ar_9 >= 0 /\ Ar_1 - Ar_9 - 2 >= 0 /\ Ar_9 >= 0 /\ Ar_1 + Ar_9 - 2 >= 0 /\ Ar_1 - 2 >= 0 /\ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ Fresh_75 >= C1 + 1 /\ Fresh_74 >= 2 /\ Ar_9 = 0 ]
		(Comp: Ar_17 + 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ -Ar_9 >= 0 /\ Ar_1 - Ar_9 - 2 >= 0 /\ Ar_9 >= 0 /\ Ar_1 + Ar_9 - 2 >= 0 /\ Ar_1 - 2 >= 0 /\ C1 >= Ar_7 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_72 + 1 /\ Fresh_71 >= 2 /\ Ar_9 = 0 ]
		(Comp: Ar_17 + 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ -Ar_9 >= 0 /\ Ar_1 - Ar_9 - 2 >= 0 /\ Ar_9 >= 0 /\ Ar_1 + Ar_9 - 2 >= 0 /\ Ar_1 - 2 >= 0 /\ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ Fresh_69 >= C1 + 1 /\ Fresh_68 >= 2 /\ Ar_9 = 0 ]
		(Comp: Ar_17 + 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, 0, Ar_17 - 1)) [ -Ar_9 >= 0 /\ Ar_1 - Ar_9 - 2 >= 0 /\ Ar_9 >= 0 /\ Ar_1 + Ar_9 - 2 >= 0 /\ Ar_1 - 2 >= 0 /\ Ar_7 >= C1 + 1 /\ Ar_17 >= 0 /\ C1 >= Fresh_66 + 1 /\ Fresh_65 >= 2 /\ Ar_9 = 0 ]
		(Comp: ?, Cost: 1)            f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_3, Fresh_103, Ar_7, Ar_9, Ar_17)) [ Ar_0 - Ar_1 >= 0 /\ Ar_1 - 2 >= 0 /\ Ar_0 + Ar_1 - 4 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_0 >= Ar_1 + 1 /\ Ar_1 >= 0 ]
		(Comp: 1, Cost: 1)            f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Fresh_18, Fresh_19, Fresh_20, Fresh_21, Ar_2, 0, Ar_17)) [ Ar_0 - Ar_1 >= 0 /\ Ar_1 - 2 >= 0 /\ Ar_0 + Ar_1 - 4 >= 0 /\ Ar_0 - 2 >= 0 /\ K1 >= Fresh_23 /\ L1 >= 2 /\ Fresh_19 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_2 >= 1 /\ Fresh_19 >= 0 /\ Fresh_23 >= 2 ]
		(Comp: 1, Cost: 1)            f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f8(Fresh_9, Fresh_10, Fresh_11, Fresh_12, Ar_2, 0, Ar_17)) [ Ar_0 - Ar_1 >= 0 /\ Ar_1 - 2 >= 0 /\ Ar_0 + Ar_1 - 4 >= 0 /\ Ar_0 - 2 >= 0 /\ K1 >= Fresh_14 /\ L1 >= 2 /\ Fresh_10 >= L1 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ 0 >= Ar_2 + 1 /\ Fresh_10 >= 0 /\ Fresh_14 >= 2 ]
		(Comp: 1, Cost: 1)            f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f10(Fresh_41, Fresh_42, Fresh_43, Fresh_44, Fresh_46, Fresh_47, Ar_17)) [ 0 >= I1 /\ 0 >= Fresh_48 /\ 0 >= J1 ]
		(Comp: 1, Cost: 1)            f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f1(Fresh_36, 2, Fresh_37, Fresh_38, Ar_7, Ar_9, Ar_17)) [ Fresh_36 >= 2 ]
		(Comp: 1, Cost: 0)            koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17) -> Com_1(f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_9, Ar_17)) [ 0 <= 0 ]
	start location:	koat_start
	leaf cost:	0

Complexity upper bound ?

Time: 6.253 sec (SMT: 5.952 sec)