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) -> Com_1(f12(Ar_0, Ar_1, Fresh_81, Fresh_82, Ar_1, Ar_6, Ar_6, Ar_0, 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_0 >= 0 /\ Fresh_81 >= 2 /\ 0 >= D1 + 1 /\ 0 >= Fresh_82 + 1 /\ 0 >= Ar_1 + 1 ]
		(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) -> Com_1(f12(Ar_0, Ar_1, Fresh_79, Fresh_80, Ar_1, Ar_6, Ar_6, Ar_0, 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_0 >= 0 /\ Fresh_79 >= 2 /\ 0 >= D1 + 1 /\ 0 >= Fresh_80 + 1 /\ Ar_1 >= 1 ]
		(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) -> Com_1(f12(Ar_0, Ar_1, Fresh_77, Fresh_78, Ar_1, Ar_6, Ar_6, Ar_0, 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_0 >= 0 /\ Fresh_77 >= 2 /\ 0 >= D1 + 1 /\ Fresh_78 >= 1 /\ 0 >= Ar_1 + 1 ]
		(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) -> Com_1(f12(Ar_0, Ar_1, Fresh_75, Fresh_76, Ar_1, Ar_6, Ar_6, Ar_0, 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_0 >= 0 /\ Fresh_75 >= 2 /\ 0 >= D1 + 1 /\ Fresh_76 >= 1 /\ Ar_1 >= 1 ]
		(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) -> Com_1(f12(Ar_0, Ar_1, Fresh_73, Fresh_74, Ar_1, Ar_6, Ar_6, Ar_0, 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_0 >= 0 /\ Fresh_73 >= 2 /\ D1 >= 1 /\ 0 >= Fresh_74 + 1 /\ 0 >= Ar_1 + 1 ]
		(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) -> Com_1(f12(Ar_0, Ar_1, Fresh_71, Fresh_72, Ar_1, Ar_6, Ar_6, Ar_0, 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_0 >= 0 /\ Fresh_71 >= 2 /\ D1 >= 1 /\ 0 >= Fresh_72 + 1 /\ Ar_1 >= 1 ]
		(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) -> Com_1(f12(Ar_0, Ar_1, Fresh_69, Fresh_70, Ar_1, Ar_6, Ar_6, Ar_0, 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_0 >= 0 /\ Fresh_69 >= 2 /\ D1 >= 1 /\ Fresh_70 >= 1 /\ 0 >= Ar_1 + 1 ]
		(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) -> Com_1(f12(Ar_0, Ar_1, Fresh_67, Fresh_68, Ar_1, Ar_6, Ar_6, Ar_0, 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_0 >= 0 /\ Fresh_67 >= 2 /\ D1 >= 1 /\ Fresh_68 >= 1 /\ Ar_1 >= 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, Ar_25, Ar_26, Ar_27) -> Com_1(f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9 + 1, Ar_11, Fresh_65, Ar_11, Fresh_66, Ar_9, 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_8 >= Ar_9 + 1 /\ 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, Ar_25, Ar_26, Ar_27) -> Com_1(f1(Ar_0, Ar_1, Fresh_60, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Fresh_60, 2, Fresh_61, Fresh_62, Fresh_61, Ar_13, Ar_14, Fresh_63, Fresh_61, Fresh_64, 2, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27)) [ Fresh_60 >= 2 ]
		(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) -> Com_1(f9(Ar_0, 0, Fresh_44, 0, Ar_4, Ar_5, Ar_6, Ar_7, Fresh_45, Fresh_46, Fresh_47, Fresh_48, Fresh_49, Ar_13, Ar_14, Fresh_50, Fresh_51, Ar_17, Ar_18, Fresh_52, Fresh_53, Fresh_54, Fresh_55, Fresh_56, Fresh_57, Fresh_58, Fresh_59, Ar_27)) [ 0 >= H1 /\ 0 >= I1 /\ 0 >= Fresh_44 /\ 0 >= J1 ]
		(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) -> Com_1(f12(Ar_0, Ar_10, Fresh_33, Fresh_34, Ar_4, Ar_5, Ar_6, Ar_7, Fresh_35, Fresh_36, Fresh_37, Fresh_38, Fresh_39, Ar_13, Ar_14, Ar_15, Fresh_40, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Fresh_41, Fresh_42, Ar_26, Fresh_43)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_36 >= Q1 /\ Fresh_36 >= 0 /\ Fresh_43 >= Fresh_33 /\ Fresh_33 >= 2 /\ 0 >= Ar_10 + 1 /\ 0 >= Fresh_34 + 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, Ar_25, Ar_26, Ar_27) -> Com_1(f12(Ar_0, Ar_10, Fresh_22, Fresh_23, Ar_4, Ar_5, Ar_6, Ar_7, Fresh_24, Fresh_25, Fresh_26, Fresh_27, Fresh_28, Ar_13, Ar_14, Ar_15, Fresh_29, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Fresh_30, Fresh_31, Ar_26, Fresh_32)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_25 >= Q1 /\ Fresh_25 >= 0 /\ Fresh_32 >= Fresh_22 /\ Fresh_22 >= 2 /\ 0 >= Ar_10 + 1 /\ Fresh_23 >= 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, Ar_25, Ar_26, Ar_27) -> Com_1(f12(Ar_0, Ar_10, Fresh_11, Fresh_12, Ar_4, Ar_5, Ar_6, Ar_7, Fresh_13, Fresh_14, Fresh_15, Fresh_16, Fresh_17, Ar_13, Ar_14, Ar_15, Fresh_18, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Fresh_19, Fresh_20, Ar_26, Fresh_21)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_14 >= Q1 /\ Fresh_14 >= 0 /\ Fresh_21 >= Fresh_11 /\ Fresh_11 >= 2 /\ Ar_10 >= 1 /\ 0 >= Fresh_12 + 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, Ar_25, Ar_26, Ar_27) -> Com_1(f12(Ar_0, Ar_10, Fresh_0, Fresh_1, Ar_4, Ar_5, Ar_6, Ar_7, Fresh_2, Fresh_3, Fresh_4, Fresh_5, Fresh_6, Ar_13, Ar_14, Ar_15, Fresh_7, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Fresh_8, Fresh_9, Ar_26, Fresh_10)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_3 >= Q1 /\ Fresh_3 >= 0 /\ Fresh_10 >= Fresh_0 /\ Fresh_0 >= 2 /\ Ar_10 >= 1 /\ Fresh_1 >= 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) -> Com_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)) [ 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_8, Ar_9, Ar_10, Ar_11].
We thus obtain the following problem:
2:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f8(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ 0 <= 0 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_2, Fresh_3, Fresh_4, Fresh_5)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_3 >= Q1 /\ Fresh_3 >= 0 /\ Fresh_10 >= Fresh_0 /\ Fresh_0 >= 2 /\ Ar_10 >= 1 /\ Fresh_1 >= 1 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_13, Fresh_14, Fresh_15, Fresh_16)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_14 >= Q1 /\ Fresh_14 >= 0 /\ Fresh_21 >= Fresh_11 /\ Fresh_11 >= 2 /\ Ar_10 >= 1 /\ 0 >= Fresh_12 + 1 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_24, Fresh_25, Fresh_26, Fresh_27)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_25 >= Q1 /\ Fresh_25 >= 0 /\ Fresh_32 >= Fresh_22 /\ Fresh_22 >= 2 /\ 0 >= Ar_10 + 1 /\ Fresh_23 >= 1 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_35, Fresh_36, Fresh_37, Fresh_38)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_36 >= Q1 /\ Fresh_36 >= 0 /\ Fresh_43 >= Fresh_33 /\ Fresh_33 >= 2 /\ 0 >= Ar_10 + 1 /\ 0 >= Fresh_34 + 1 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f9(Ar_0, 0, Fresh_45, Fresh_46, Fresh_47, Fresh_48)) [ 0 >= H1 /\ 0 >= I1 /\ 0 >= Fresh_44 /\ 0 >= J1 ]
		(Comp: ?, Cost: 1)    f8(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f1(Ar_0, Ar_1, Fresh_60, 2, Fresh_61, Fresh_62)) [ Fresh_60 >= 2 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f1(Ar_0, Ar_1, Ar_8, Ar_9 + 1, Ar_11, Fresh_65)) [ Ar_8 >= Ar_9 + 1 /\ Ar_9 >= 0 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_67 >= 2 /\ D1 >= 1 /\ Fresh_68 >= 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_69 >= 2 /\ D1 >= 1 /\ Fresh_70 >= 1 /\ 0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_71 >= 2 /\ D1 >= 1 /\ 0 >= Fresh_72 + 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_73 >= 2 /\ D1 >= 1 /\ 0 >= Fresh_74 + 1 /\ 0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_75 >= 2 /\ 0 >= D1 + 1 /\ Fresh_76 >= 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_77 >= 2 /\ 0 >= D1 + 1 /\ Fresh_78 >= 1 /\ 0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_79 >= 2 /\ 0 >= D1 + 1 /\ 0 >= Fresh_80 + 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_81 >= 2 /\ 0 >= D1 + 1 /\ 0 >= Fresh_82 + 1 /\ 0 >= Ar_1 + 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_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f8(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ 0 <= 0 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_2, Fresh_3, Fresh_4, Fresh_5)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_3 >= Q1 /\ Fresh_3 >= 0 /\ Fresh_10 >= Fresh_0 /\ Fresh_0 >= 2 /\ Ar_10 >= 1 /\ Fresh_1 >= 1 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_13, Fresh_14, Fresh_15, Fresh_16)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_14 >= Q1 /\ Fresh_14 >= 0 /\ Fresh_21 >= Fresh_11 /\ Fresh_11 >= 2 /\ Ar_10 >= 1 /\ 0 >= Fresh_12 + 1 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_24, Fresh_25, Fresh_26, Fresh_27)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_25 >= Q1 /\ Fresh_25 >= 0 /\ Fresh_32 >= Fresh_22 /\ Fresh_22 >= 2 /\ 0 >= Ar_10 + 1 /\ Fresh_23 >= 1 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_35, Fresh_36, Fresh_37, Fresh_38)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_36 >= Q1 /\ Fresh_36 >= 0 /\ Fresh_43 >= Fresh_33 /\ Fresh_33 >= 2 /\ 0 >= Ar_10 + 1 /\ 0 >= Fresh_34 + 1 ]
		(Comp: 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f9(Ar_0, 0, Fresh_45, Fresh_46, Fresh_47, Fresh_48)) [ 0 >= H1 /\ 0 >= I1 /\ 0 >= Fresh_44 /\ 0 >= J1 ]
		(Comp: 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f1(Ar_0, Ar_1, Fresh_60, 2, Fresh_61, Fresh_62)) [ Fresh_60 >= 2 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f1(Ar_0, Ar_1, Ar_8, Ar_9 + 1, Ar_11, Fresh_65)) [ Ar_8 >= Ar_9 + 1 /\ Ar_9 >= 0 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_67 >= 2 /\ D1 >= 1 /\ Fresh_68 >= 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_69 >= 2 /\ D1 >= 1 /\ Fresh_70 >= 1 /\ 0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_71 >= 2 /\ D1 >= 1 /\ 0 >= Fresh_72 + 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_73 >= 2 /\ D1 >= 1 /\ 0 >= Fresh_74 + 1 /\ 0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_75 >= 2 /\ 0 >= D1 + 1 /\ Fresh_76 >= 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_77 >= 2 /\ 0 >= D1 + 1 /\ Fresh_78 >= 1 /\ 0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_79 >= 2 /\ 0 >= D1 + 1 /\ 0 >= Fresh_80 + 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_81 >= 2 /\ 0 >= D1 + 1 /\ 0 >= Fresh_82 + 1 /\ 0 >= Ar_1 + 1 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(koat_start) = 1
	Pol(f8) = 1
	Pol(f1) = 1
	Pol(f12) = 0
	Pol(f9) = 1
orients all transitions weakly and the transitions
	f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_35, Fresh_36, Fresh_37, Fresh_38)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_36 >= Q1 /\ Fresh_36 >= 0 /\ Fresh_43 >= Fresh_33 /\ Fresh_33 >= 2 /\ 0 >= Ar_10 + 1 /\ 0 >= Fresh_34 + 1 ]
	f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_24, Fresh_25, Fresh_26, Fresh_27)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_25 >= Q1 /\ Fresh_25 >= 0 /\ Fresh_32 >= Fresh_22 /\ Fresh_22 >= 2 /\ 0 >= Ar_10 + 1 /\ Fresh_23 >= 1 ]
	f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_13, Fresh_14, Fresh_15, Fresh_16)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_14 >= Q1 /\ Fresh_14 >= 0 /\ Fresh_21 >= Fresh_11 /\ Fresh_11 >= 2 /\ Ar_10 >= 1 /\ 0 >= Fresh_12 + 1 ]
strictly and produces the following problem:
4:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f8(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ 0 <= 0 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_2, Fresh_3, Fresh_4, Fresh_5)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_3 >= Q1 /\ Fresh_3 >= 0 /\ Fresh_10 >= Fresh_0 /\ Fresh_0 >= 2 /\ Ar_10 >= 1 /\ Fresh_1 >= 1 ]
		(Comp: 1, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_13, Fresh_14, Fresh_15, Fresh_16)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_14 >= Q1 /\ Fresh_14 >= 0 /\ Fresh_21 >= Fresh_11 /\ Fresh_11 >= 2 /\ Ar_10 >= 1 /\ 0 >= Fresh_12 + 1 ]
		(Comp: 1, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_24, Fresh_25, Fresh_26, Fresh_27)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_25 >= Q1 /\ Fresh_25 >= 0 /\ Fresh_32 >= Fresh_22 /\ Fresh_22 >= 2 /\ 0 >= Ar_10 + 1 /\ Fresh_23 >= 1 ]
		(Comp: 1, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_35, Fresh_36, Fresh_37, Fresh_38)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_36 >= Q1 /\ Fresh_36 >= 0 /\ Fresh_43 >= Fresh_33 /\ Fresh_33 >= 2 /\ 0 >= Ar_10 + 1 /\ 0 >= Fresh_34 + 1 ]
		(Comp: 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f9(Ar_0, 0, Fresh_45, Fresh_46, Fresh_47, Fresh_48)) [ 0 >= H1 /\ 0 >= I1 /\ 0 >= Fresh_44 /\ 0 >= J1 ]
		(Comp: 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f1(Ar_0, Ar_1, Fresh_60, 2, Fresh_61, Fresh_62)) [ Fresh_60 >= 2 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f1(Ar_0, Ar_1, Ar_8, Ar_9 + 1, Ar_11, Fresh_65)) [ Ar_8 >= Ar_9 + 1 /\ Ar_9 >= 0 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_67 >= 2 /\ D1 >= 1 /\ Fresh_68 >= 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_69 >= 2 /\ D1 >= 1 /\ Fresh_70 >= 1 /\ 0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_71 >= 2 /\ D1 >= 1 /\ 0 >= Fresh_72 + 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_73 >= 2 /\ D1 >= 1 /\ 0 >= Fresh_74 + 1 /\ 0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_75 >= 2 /\ 0 >= D1 + 1 /\ Fresh_76 >= 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_77 >= 2 /\ 0 >= D1 + 1 /\ Fresh_78 >= 1 /\ 0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_79 >= 2 /\ 0 >= D1 + 1 /\ 0 >= Fresh_80 + 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_81 >= 2 /\ 0 >= D1 + 1 /\ 0 >= Fresh_82 + 1 /\ 0 >= Ar_1 + 1 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(koat_start) = 1
	Pol(f8) = 1
	Pol(f1) = 1
	Pol(f12) = 0
	Pol(f9) = 1
orients all transitions weakly and the transition
	f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_2, Fresh_3, Fresh_4, Fresh_5)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_3 >= Q1 /\ Fresh_3 >= 0 /\ Fresh_10 >= Fresh_0 /\ Fresh_0 >= 2 /\ Ar_10 >= 1 /\ Fresh_1 >= 1 ]
strictly and produces the following problem:
5:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f8(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_2, Fresh_3, Fresh_4, Fresh_5)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_3 >= Q1 /\ Fresh_3 >= 0 /\ Fresh_10 >= Fresh_0 /\ Fresh_0 >= 2 /\ Ar_10 >= 1 /\ Fresh_1 >= 1 ]
		(Comp: 1, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_13, Fresh_14, Fresh_15, Fresh_16)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_14 >= Q1 /\ Fresh_14 >= 0 /\ Fresh_21 >= Fresh_11 /\ Fresh_11 >= 2 /\ Ar_10 >= 1 /\ 0 >= Fresh_12 + 1 ]
		(Comp: 1, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_24, Fresh_25, Fresh_26, Fresh_27)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_25 >= Q1 /\ Fresh_25 >= 0 /\ Fresh_32 >= Fresh_22 /\ Fresh_22 >= 2 /\ 0 >= Ar_10 + 1 /\ Fresh_23 >= 1 ]
		(Comp: 1, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_35, Fresh_36, Fresh_37, Fresh_38)) [ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_36 >= Q1 /\ Fresh_36 >= 0 /\ Fresh_43 >= Fresh_33 /\ Fresh_33 >= 2 /\ 0 >= Ar_10 + 1 /\ 0 >= Fresh_34 + 1 ]
		(Comp: 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f9(Ar_0, 0, Fresh_45, Fresh_46, Fresh_47, Fresh_48)) [ 0 >= H1 /\ 0 >= I1 /\ 0 >= Fresh_44 /\ 0 >= J1 ]
		(Comp: 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f1(Ar_0, Ar_1, Fresh_60, 2, Fresh_61, Fresh_62)) [ Fresh_60 >= 2 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f1(Ar_0, Ar_1, Ar_8, Ar_9 + 1, Ar_11, Fresh_65)) [ Ar_8 >= Ar_9 + 1 /\ Ar_9 >= 0 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_67 >= 2 /\ D1 >= 1 /\ Fresh_68 >= 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_69 >= 2 /\ D1 >= 1 /\ Fresh_70 >= 1 /\ 0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_71 >= 2 /\ D1 >= 1 /\ 0 >= Fresh_72 + 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_73 >= 2 /\ D1 >= 1 /\ 0 >= Fresh_74 + 1 /\ 0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_75 >= 2 /\ 0 >= D1 + 1 /\ Fresh_76 >= 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_77 >= 2 /\ 0 >= D1 + 1 /\ Fresh_78 >= 1 /\ 0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_79 >= 2 /\ 0 >= D1 + 1 /\ 0 >= Fresh_80 + 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_0 >= 0 /\ Fresh_81 >= 2 /\ 0 >= D1 + 1 /\ 0 >= Fresh_82 + 1 /\ 0 >= Ar_1 + 1 ]
	start location:	koat_start
	leaf cost:	0

Applied AI with 'oct' on problem 5 to obtain the following invariants:
  For symbol f1: X_3 - X_4 >= 0 /\ X_4 - 2 >= 0 /\ X_3 + X_4 - 4 >= 0 /\ X_3 - 2 >= 0
  For symbol f12: X_4 - 2 >= 0


This yielded the following problem:
6:	T:
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_9 - 2 >= 0 /\ Ar_0 >= 0 /\ Fresh_81 >= 2 /\ 0 >= D1 + 1 /\ 0 >= Fresh_82 + 1 /\ 0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_9 - 2 >= 0 /\ Ar_0 >= 0 /\ Fresh_79 >= 2 /\ 0 >= D1 + 1 /\ 0 >= Fresh_80 + 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_9 - 2 >= 0 /\ Ar_0 >= 0 /\ Fresh_77 >= 2 /\ 0 >= D1 + 1 /\ Fresh_78 >= 1 /\ 0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_9 - 2 >= 0 /\ Ar_0 >= 0 /\ Fresh_75 >= 2 /\ 0 >= D1 + 1 /\ Fresh_76 >= 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_9 - 2 >= 0 /\ Ar_0 >= 0 /\ Fresh_73 >= 2 /\ D1 >= 1 /\ 0 >= Fresh_74 + 1 /\ 0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_9 - 2 >= 0 /\ Ar_0 >= 0 /\ Fresh_71 >= 2 /\ D1 >= 1 /\ 0 >= Fresh_72 + 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_9 - 2 >= 0 /\ Ar_0 >= 0 /\ Fresh_69 >= 2 /\ D1 >= 1 /\ Fresh_70 >= 1 /\ 0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ Ar_9 - 2 >= 0 /\ Ar_0 >= 0 /\ Fresh_67 >= 2 /\ D1 >= 1 /\ Fresh_68 >= 1 /\ Ar_1 >= 1 ]
		(Comp: ?, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f1(Ar_0, Ar_1, Ar_8, Ar_9 + 1, Ar_11, Fresh_65)) [ Ar_8 - Ar_9 >= 0 /\ Ar_9 - 2 >= 0 /\ Ar_8 + Ar_9 - 4 >= 0 /\ Ar_8 - 2 >= 0 /\ Ar_8 >= Ar_9 + 1 /\ Ar_9 >= 0 ]
		(Comp: 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f1(Ar_0, Ar_1, Fresh_60, 2, Fresh_61, Fresh_62)) [ Fresh_60 >= 2 ]
		(Comp: 1, Cost: 1)    f8(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f9(Ar_0, 0, Fresh_45, Fresh_46, Fresh_47, Fresh_48)) [ 0 >= H1 /\ 0 >= I1 /\ 0 >= Fresh_44 /\ 0 >= J1 ]
		(Comp: 1, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_35, Fresh_36, Fresh_37, Fresh_38)) [ Ar_8 - Ar_9 >= 0 /\ Ar_9 - 2 >= 0 /\ Ar_8 + Ar_9 - 4 >= 0 /\ Ar_8 - 2 >= 0 /\ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_36 >= Q1 /\ Fresh_36 >= 0 /\ Fresh_43 >= Fresh_33 /\ Fresh_33 >= 2 /\ 0 >= Ar_10 + 1 /\ 0 >= Fresh_34 + 1 ]
		(Comp: 1, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_24, Fresh_25, Fresh_26, Fresh_27)) [ Ar_8 - Ar_9 >= 0 /\ Ar_9 - 2 >= 0 /\ Ar_8 + Ar_9 - 4 >= 0 /\ Ar_8 - 2 >= 0 /\ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_25 >= Q1 /\ Fresh_25 >= 0 /\ Fresh_32 >= Fresh_22 /\ Fresh_22 >= 2 /\ 0 >= Ar_10 + 1 /\ Fresh_23 >= 1 ]
		(Comp: 1, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_13, Fresh_14, Fresh_15, Fresh_16)) [ Ar_8 - Ar_9 >= 0 /\ Ar_9 - 2 >= 0 /\ Ar_8 + Ar_9 - 4 >= 0 /\ Ar_8 - 2 >= 0 /\ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_14 >= Q1 /\ Fresh_14 >= 0 /\ Fresh_21 >= Fresh_11 /\ Fresh_11 >= 2 /\ Ar_10 >= 1 /\ 0 >= Fresh_12 + 1 ]
		(Comp: 1, Cost: 1)    f1(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f12(Ar_0, Ar_10, Fresh_2, Fresh_3, Fresh_4, Fresh_5)) [ Ar_8 - Ar_9 >= 0 /\ Ar_9 - 2 >= 0 /\ Ar_8 + Ar_9 - 4 >= 0 /\ Ar_8 - 2 >= 0 /\ Ar_9 >= Ar_8 /\ Ar_9 >= 0 /\ Q1 >= 2 /\ Fresh_3 >= Q1 /\ Fresh_3 >= 0 /\ Fresh_10 >= Fresh_0 /\ Fresh_0 >= 2 /\ Ar_10 >= 1 /\ Fresh_1 >= 1 ]
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11) -> Com_1(f8(Ar_0, Ar_1, Ar_8, Ar_9, Ar_10, Ar_11)) [ 0 <= 0 ]
	start location:	koat_start
	leaf cost:	0

Complexity upper bound ?

Time: 7.107 sec (SMT: 6.709 sec)