MAYBE

Initial complexity problem:
1:	T:
		(Comp: ?, Cost: 1)    f33(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) -> Com_1(f3(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))
		(Comp: ?, Cost: 1)    f3(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) -> Com_1(f25(Fresh_73, Ar_1, Ar_1, 0, 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_0 >= 1 /\ Ar_1 >= 1 /\ Fresh_73 >= 1 ]
		(Comp: ?, Cost: 1)    f3(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) -> Com_1(f25(Fresh_72, Ar_1, Ar_1, 0, 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_0 >= 1 /\ 0 >= Ar_1 + 1 /\ Fresh_72 >= 1 ]
		(Comp: ?, Cost: 1)    f3(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) -> Com_1(f16(Ar_9, Ar_1, Ar_2, Ar_3, Fresh_70, Fresh_71, Fresh_71, Fresh_71, Fresh_71, Ar_9 + 1, Fresh_71, 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))
		(Comp: ?, Cost: 1)    f3(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) -> Com_1(f16(Fresh_68 + 1, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_69, Fresh_69, Fresh_69, Fresh_69, Ar_9 + 1, Fresh_69, 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)) [ Fresh_68 >= 0 /\ Ar_0 >= 0 ]
		(Comp: ?, Cost: 1)    f3(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) -> Com_1(f22(Fresh_67, Ar_11, 0, 0, Ar_4, Ar_5, Ar_6, Ar_7, Ar_11, Ar_9, Ar_10, Ar_11, Ar_11, Ar_11, 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)) [ H1 >= 1 /\ Ar_0 >= 1 /\ Ar_1 = 0 ]
		(Comp: ?, Cost: 1)    f23(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31) -> Com_1(f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_62, 0, Ar_11, 0, Ar_13, Fresh_63, Fresh_64, Fresh_65, Fresh_63, Fresh_66, 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)) [ Fresh_63 >= 1 /\ 0 >= I1 ]
		(Comp: ?, Cost: 1)    f23(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31) -> Com_1(f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_57, 0, Ar_11, 0, Ar_13, Fresh_58, Fresh_59, Fresh_60, Fresh_58, Fresh_61, 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)) [ 0 >= Fresh_58 + 1 /\ 0 >= I1 ]
		(Comp: ?, Cost: 1)    f23(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31) -> Com_1(f21(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Fresh_52, Fresh_53, 0, Ar_11, 0, Ar_13, 0, Fresh_54, Fresh_55, 0, Fresh_56, 0, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31)) [ 0 >= I1 ]
		(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) -> Com_1(f16(Fresh_42 + 1, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_43, Fresh_43, Fresh_43, Fresh_43, Fresh_44 + 1, Fresh_43, Ar_11, Ar_12, Ar_13, Ar_14, Fresh_45, Fresh_46, Ar_17, Ar_18, Ar_19, Fresh_47, Fresh_48, Fresh_49, Fresh_50, Fresh_51, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31)) [ Ar_0 >= 0 /\ M1 >= 0 /\ Ar_16 >= Ar_9 + 1 /\ Fresh_42 >= 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) -> Com_1(f18(Fresh_37, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_38, Ar_10, Ar_11, 0, Ar_13, 0, Fresh_39, Fresh_40, 0, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Fresh_41, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31)) [ Ar_0 >= 0 /\ I1 >= 0 /\ Ar_9 >= Ar_16 /\ Fresh_37 >= 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) -> Com_1(f3(Fresh_23, Fresh_24, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_25, Fresh_26, Fresh_27, 0, Ar_13, Fresh_28, Fresh_29, Fresh_30, Fresh_31, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Fresh_32, Fresh_33, Fresh_34, Fresh_35, Fresh_36, Ar_30, Ar_31)) [ Ar_0 >= 0 /\ R1 >= 0 /\ S1 >= 0 /\ Ar_9 >= Ar_16 /\ Fresh_33 >= 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) -> Com_1(f3(Fresh_9, Fresh_10, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_11, Fresh_12, Fresh_13, 0, Ar_13, Fresh_14, Fresh_15, Fresh_16, Fresh_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Fresh_18, Fresh_19, Fresh_20, Fresh_21, Fresh_22, Ar_30, Ar_31)) [ Ar_0 >= 0 /\ R1 >= 0 /\ S1 >= 0 /\ Ar_9 >= Ar_16 /\ 0 >= Fresh_19 + 1 ]
		(Comp: ?, Cost: 1)    f23(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31) -> Com_1(f16(Fresh_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_1, Fresh_1, Fresh_1, Fresh_1, Fresh_0 + 1, Fresh_1, Ar_11, Ar_12, Ar_13, Ar_14, Fresh_2, Fresh_3, Ar_17, Ar_18, Ar_19, Fresh_4, Fresh_5, Fresh_6, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Fresh_7, Fresh_8)) [ Q1 >= 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, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31) -> Com_1(f33(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)) [ 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_9, Ar_11, Ar_16].
We thus obtain the following problem:
2:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f33(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16)) [ 0 <= 0 ]
		(Comp: ?, Cost: 1)    f23(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f16(Fresh_0, Ar_1, Fresh_0 + 1, Ar_11, Fresh_3)) [ Q1 >= 1 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f3(Fresh_9, Fresh_10, Fresh_11, Fresh_13, Fresh_16)) [ Ar_0 >= 0 /\ R1 >= 0 /\ S1 >= 0 /\ Ar_9 >= Ar_16 /\ 0 >= Fresh_19 + 1 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f3(Fresh_23, Fresh_24, Fresh_25, Fresh_27, Fresh_30)) [ Ar_0 >= 0 /\ R1 >= 0 /\ S1 >= 0 /\ Ar_9 >= Ar_16 /\ Fresh_33 >= 1 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f18(Fresh_37, Ar_1, Fresh_38, Ar_11, Fresh_40)) [ Ar_0 >= 0 /\ I1 >= 0 /\ Ar_9 >= Ar_16 /\ Fresh_37 >= 0 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f16(Fresh_42 + 1, Ar_1, Fresh_44 + 1, Ar_11, Fresh_46)) [ Ar_0 >= 0 /\ M1 >= 0 /\ Ar_16 >= Ar_9 + 1 /\ Fresh_42 >= 0 ]
		(Comp: ?, Cost: 1)    f23(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f21(Ar_0, Ar_1, Fresh_53, Ar_11, Fresh_55)) [ 0 >= I1 ]
		(Comp: ?, Cost: 1)    f23(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f17(Ar_0, Ar_1, Fresh_57, Ar_11, Fresh_60)) [ 0 >= Fresh_58 + 1 /\ 0 >= I1 ]
		(Comp: ?, Cost: 1)    f23(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f17(Ar_0, Ar_1, Fresh_62, Ar_11, Fresh_65)) [ Fresh_63 >= 1 /\ 0 >= I1 ]
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f22(Fresh_67, Ar_11, Ar_9, Ar_11, Ar_16)) [ H1 >= 1 /\ Ar_0 >= 1 /\ Ar_1 = 0 ]
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f16(Fresh_68 + 1, Ar_1, Ar_9 + 1, Ar_11, Ar_16)) [ Fresh_68 >= 0 /\ Ar_0 >= 0 ]
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f16(Ar_9, Ar_1, Ar_9 + 1, Ar_11, Ar_16))
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f25(Fresh_72, Ar_1, Ar_9, Ar_11, Ar_16)) [ Ar_0 >= 1 /\ 0 >= Ar_1 + 1 /\ Fresh_72 >= 1 ]
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f25(Fresh_73, Ar_1, Ar_9, Ar_11, Ar_16)) [ Ar_0 >= 1 /\ Ar_1 >= 1 /\ Fresh_73 >= 1 ]
		(Comp: ?, Cost: 1)    f33(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16))
	start location:	koat_start
	leaf cost:	0

Testing for reachability in the complexity graph removes the following transitions from problem 2:
	f23(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f16(Fresh_0, Ar_1, Fresh_0 + 1, Ar_11, Fresh_3)) [ Q1 >= 1 ]
	f23(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f21(Ar_0, Ar_1, Fresh_53, Ar_11, Fresh_55)) [ 0 >= I1 ]
	f23(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f17(Ar_0, Ar_1, Fresh_57, Ar_11, Fresh_60)) [ 0 >= Fresh_58 + 1 /\ 0 >= I1 ]
	f23(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f17(Ar_0, Ar_1, Fresh_62, Ar_11, Fresh_65)) [ Fresh_63 >= 1 /\ 0 >= I1 ]
We thus obtain the following problem:
3:	T:
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f16(Fresh_42 + 1, Ar_1, Fresh_44 + 1, Ar_11, Fresh_46)) [ Ar_0 >= 0 /\ M1 >= 0 /\ Ar_16 >= Ar_9 + 1 /\ Fresh_42 >= 0 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f18(Fresh_37, Ar_1, Fresh_38, Ar_11, Fresh_40)) [ Ar_0 >= 0 /\ I1 >= 0 /\ Ar_9 >= Ar_16 /\ Fresh_37 >= 0 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f3(Fresh_23, Fresh_24, Fresh_25, Fresh_27, Fresh_30)) [ Ar_0 >= 0 /\ R1 >= 0 /\ S1 >= 0 /\ Ar_9 >= Ar_16 /\ Fresh_33 >= 1 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f3(Fresh_9, Fresh_10, Fresh_11, Fresh_13, Fresh_16)) [ Ar_0 >= 0 /\ R1 >= 0 /\ S1 >= 0 /\ Ar_9 >= Ar_16 /\ 0 >= Fresh_19 + 1 ]
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f25(Fresh_73, Ar_1, Ar_9, Ar_11, Ar_16)) [ Ar_0 >= 1 /\ Ar_1 >= 1 /\ Fresh_73 >= 1 ]
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f25(Fresh_72, Ar_1, Ar_9, Ar_11, Ar_16)) [ Ar_0 >= 1 /\ 0 >= Ar_1 + 1 /\ Fresh_72 >= 1 ]
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f16(Ar_9, Ar_1, Ar_9 + 1, Ar_11, Ar_16))
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f16(Fresh_68 + 1, Ar_1, Ar_9 + 1, Ar_11, Ar_16)) [ Fresh_68 >= 0 /\ Ar_0 >= 0 ]
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f22(Fresh_67, Ar_11, Ar_9, Ar_11, Ar_16)) [ H1 >= 1 /\ Ar_0 >= 1 /\ Ar_1 = 0 ]
		(Comp: ?, Cost: 1)    f33(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16))
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f33(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16)) [ 0 <= 0 ]
	start location:	koat_start
	leaf cost:	0

Repeatedly propagating knowledge in problem 3 produces the following problem:
4:	T:
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f16(Fresh_42 + 1, Ar_1, Fresh_44 + 1, Ar_11, Fresh_46)) [ Ar_0 >= 0 /\ M1 >= 0 /\ Ar_16 >= Ar_9 + 1 /\ Fresh_42 >= 0 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f18(Fresh_37, Ar_1, Fresh_38, Ar_11, Fresh_40)) [ Ar_0 >= 0 /\ I1 >= 0 /\ Ar_9 >= Ar_16 /\ Fresh_37 >= 0 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f3(Fresh_23, Fresh_24, Fresh_25, Fresh_27, Fresh_30)) [ Ar_0 >= 0 /\ R1 >= 0 /\ S1 >= 0 /\ Ar_9 >= Ar_16 /\ Fresh_33 >= 1 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f3(Fresh_9, Fresh_10, Fresh_11, Fresh_13, Fresh_16)) [ Ar_0 >= 0 /\ R1 >= 0 /\ S1 >= 0 /\ Ar_9 >= Ar_16 /\ 0 >= Fresh_19 + 1 ]
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f25(Fresh_73, Ar_1, Ar_9, Ar_11, Ar_16)) [ Ar_0 >= 1 /\ Ar_1 >= 1 /\ Fresh_73 >= 1 ]
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f25(Fresh_72, Ar_1, Ar_9, Ar_11, Ar_16)) [ Ar_0 >= 1 /\ 0 >= Ar_1 + 1 /\ Fresh_72 >= 1 ]
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f16(Ar_9, Ar_1, Ar_9 + 1, Ar_11, Ar_16))
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f16(Fresh_68 + 1, Ar_1, Ar_9 + 1, Ar_11, Ar_16)) [ Fresh_68 >= 0 /\ Ar_0 >= 0 ]
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f22(Fresh_67, Ar_11, Ar_9, Ar_11, Ar_16)) [ H1 >= 1 /\ Ar_0 >= 1 /\ Ar_1 = 0 ]
		(Comp: 1, Cost: 1)    f33(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16))
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f33(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16)) [ 0 <= 0 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(f16) = 1
	Pol(f18) = 0
	Pol(f3) = 1
	Pol(f25) = 0
	Pol(f22) = 0
	Pol(f33) = 1
	Pol(koat_start) = 1
orients all transitions weakly and the transitions
	f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f25(Fresh_73, Ar_1, Ar_9, Ar_11, Ar_16)) [ Ar_0 >= 1 /\ Ar_1 >= 1 /\ Fresh_73 >= 1 ]
	f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f25(Fresh_72, Ar_1, Ar_9, Ar_11, Ar_16)) [ Ar_0 >= 1 /\ 0 >= Ar_1 + 1 /\ Fresh_72 >= 1 ]
	f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f22(Fresh_67, Ar_11, Ar_9, Ar_11, Ar_16)) [ H1 >= 1 /\ Ar_0 >= 1 /\ Ar_1 = 0 ]
	f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f18(Fresh_37, Ar_1, Fresh_38, Ar_11, Fresh_40)) [ Ar_0 >= 0 /\ I1 >= 0 /\ Ar_9 >= Ar_16 /\ Fresh_37 >= 0 ]
strictly and produces the following problem:
5:	T:
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f16(Fresh_42 + 1, Ar_1, Fresh_44 + 1, Ar_11, Fresh_46)) [ Ar_0 >= 0 /\ M1 >= 0 /\ Ar_16 >= Ar_9 + 1 /\ Fresh_42 >= 0 ]
		(Comp: 1, Cost: 1)    f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f18(Fresh_37, Ar_1, Fresh_38, Ar_11, Fresh_40)) [ Ar_0 >= 0 /\ I1 >= 0 /\ Ar_9 >= Ar_16 /\ Fresh_37 >= 0 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f3(Fresh_23, Fresh_24, Fresh_25, Fresh_27, Fresh_30)) [ Ar_0 >= 0 /\ R1 >= 0 /\ S1 >= 0 /\ Ar_9 >= Ar_16 /\ Fresh_33 >= 1 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f3(Fresh_9, Fresh_10, Fresh_11, Fresh_13, Fresh_16)) [ Ar_0 >= 0 /\ R1 >= 0 /\ S1 >= 0 /\ Ar_9 >= Ar_16 /\ 0 >= Fresh_19 + 1 ]
		(Comp: 1, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f25(Fresh_73, Ar_1, Ar_9, Ar_11, Ar_16)) [ Ar_0 >= 1 /\ Ar_1 >= 1 /\ Fresh_73 >= 1 ]
		(Comp: 1, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f25(Fresh_72, Ar_1, Ar_9, Ar_11, Ar_16)) [ Ar_0 >= 1 /\ 0 >= Ar_1 + 1 /\ Fresh_72 >= 1 ]
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f16(Ar_9, Ar_1, Ar_9 + 1, Ar_11, Ar_16))
		(Comp: ?, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f16(Fresh_68 + 1, Ar_1, Ar_9 + 1, Ar_11, Ar_16)) [ Fresh_68 >= 0 /\ Ar_0 >= 0 ]
		(Comp: 1, Cost: 1)    f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f22(Fresh_67, Ar_11, Ar_9, Ar_11, Ar_16)) [ H1 >= 1 /\ Ar_0 >= 1 /\ Ar_1 = 0 ]
		(Comp: 1, Cost: 1)    f33(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f3(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16))
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16) -> Com_1(f33(Ar_0, Ar_1, Ar_9, Ar_11, Ar_16)) [ 0 <= 0 ]
	start location:	koat_start
	leaf cost:	0

Complexity upper bound ?

Time: 2.168 sec (SMT: 2.061 sec)