WORST_CASE(?, O(n^1))

Initial complexity problem:
1:	T:
		(Comp: ?, Cost: 1)    f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f16(1, Fresh_43, Fresh_44, Fresh_45, Fresh_46, Fresh_47, Fresh_48, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ Ar_0 = 1 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ Ar_7 >= Ar_8 ]
		(Comp: ?, Cost: 1)    f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_11 + 2, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f28(Ar_0, Fresh_37, Fresh_38, Fresh_39, Fresh_40, Fresh_41, Fresh_42, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ 0 >= Ar_0 ]
		(Comp: ?, Cost: 1)    f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f28(Ar_0, Fresh_31, Fresh_32, Fresh_33, Fresh_34, Fresh_35, Fresh_36, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ Ar_0 >= 2 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f35(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_7 - Ar_8 + 2, 1, 0, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f35(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_7 - Ar_8 + 2, 1, 0, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f35(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, 1, Ar_9, Ar_10, Ar_11, 1, 1, 0, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ Ar_7 >= 1 /\ Ar_8 = 1 ]
		(Comp: ?, Cost: 1)    f35(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f37(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f52(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f52(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f37(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Fresh_26, Ar_12, Ar_13, Ar_14, Ar_15, 1, Fresh_27, Fresh_28, Fresh_29, Fresh_30, Ar_21, Ar_22)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f37(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Fresh_21, Ar_12, Ar_13, Ar_14, Ar_15, 1, Fresh_22, Fresh_23, Fresh_24, Fresh_25, Ar_21, Ar_22)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f37(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, 2, 1, Ar_12, Ar_13, Ar_14, Ar_15, 1, Fresh_17, Fresh_18, Fresh_19, Fresh_20, Ar_21, Ar_22)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f37(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_9 - Ar_10 + 2, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_12, Fresh_13, Fresh_14, Fresh_15, Fresh_16, Ar_22)) [ 0 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f37(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_9 - Ar_10 + 2, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_7, Fresh_8, Fresh_9, Fresh_10, Fresh_11, Ar_22)) [ Ar_10 >= 2 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f37(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, 2, 1, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_2, Fresh_3, Fresh_4, Fresh_5, Fresh_6, Ar_22)) [ Ar_10 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f35(Ar_0, Ar_1, Ar_2, Ar_3, Ar_13, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Fresh_0, Fresh_1, Ar_15, Ar_16 + 1, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22 + 2)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: ?, Cost: 1)    f35(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f28(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f76(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f76(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f76(-1, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ]
		(Comp: ?, Cost: 1)    f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f28(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ Ar_8 >= Ar_7 + 1 ]
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22)) [ 0 <= 0 ]
	start location:	koat_start
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16].
We thus obtain the following problem:
2:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ]
		(Comp: ?, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]
		(Comp: ?, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]
		(Comp: ?, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]
		(Comp: ?, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]
	start location:	koat_start
	leaf cost:	0

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]
		(Comp: 1, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]
		(Comp: ?, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(koat_start) = 1
	Pol(f0) = 1
	Pol(f16) = 1
	Pol(f28) = -1
	Pol(f18) = 1
	Pol(f76) = -2
	Pol(f35) = -1
	Pol(f37) = -1
	Pol(f52) = -1
orients all transitions weakly and the transition
	f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]
strictly and produces the following problem:
4:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)    f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]
		(Comp: 1, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]
		(Comp: ?, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(koat_start) = 1
	Pol(f0) = 1
	Pol(f16) = 1
	Pol(f28) = 1
	Pol(f18) = 1
	Pol(f76) = 0
	Pol(f35) = 1
	Pol(f37) = 1
	Pol(f52) = 1
orients all transitions weakly and the transition
	f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ]
strictly and produces the following problem:
5:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)    f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: 1, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]
		(Comp: 1, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]
		(Comp: ?, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(koat_start) = 1
	Pol(f0) = 1
	Pol(f16) = 1
	Pol(f28) = 1
	Pol(f18) = 1
	Pol(f76) = 0
	Pol(f35) = 1
	Pol(f37) = 1
	Pol(f52) = 1
orients all transitions weakly and the transition
	f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ]
strictly and produces the following problem:
6:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)    f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: 1, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: 1, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]
		(Comp: 1, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]
		(Comp: ?, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(koat_start) = 1
	Pol(f0) = 1
	Pol(f16) = 1
	Pol(f28) = 1
	Pol(f18) = 1
	Pol(f76) = 0
	Pol(f35) = 1
	Pol(f37) = 1
	Pol(f52) = 1
orients all transitions weakly and the transition
	f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ]
strictly and produces the following problem:
7:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)    f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: 1, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ]
		(Comp: 1, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: 1, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)    f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]
		(Comp: ?, Cost: 1)    f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ]
		(Comp: ?, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]
		(Comp: 1, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]
		(Comp: ?, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)    f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)    f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(koat_start) = 8*V_2 - 8*V_3 + 1
	Pol(f0) = 8*V_2 - 8*V_3 + 1
	Pol(f16) = 8*V_2 - 8*V_3 + 1
	Pol(f28) = 8*V_2 - 8*V_3 + 1
	Pol(f18) = 8*V_2 - 8*V_3
	Pol(f76) = 8*V_2 - 8*V_3
	Pol(f35) = 8*V_2 - 8*V_3 - 6
	Pol(f37) = 8*V_2 - 8*V_3 - 6
	Pol(f52) = 8*V_2 - 8*V_3 - 6
orients all transitions weakly and the transitions
	f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ]
	f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ]
	f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ]
	f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]
strictly and produces the following problem:
8:	T:
		(Comp: 1, Cost: 0)                      koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)                      f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)                      f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: 1, Cost: 1)                      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ]
		(Comp: 1, Cost: 1)                      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: 1, Cost: 1)                      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)                      f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
		(Comp: ?, Cost: 1)                      f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: ?, Cost: 1)                      f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]
		(Comp: ?, Cost: 1)                      f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]
		(Comp: ?, Cost: 1)                      f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]
		(Comp: ?, Cost: 1)                      f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)                      f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)                      f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)                      f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)                      f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)                      f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)    f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)                      f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]
		(Comp: 1, Cost: 1)                      f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]
		(Comp: ?, Cost: 1)                      f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)    f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)                      f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(f52) = -1
	Pol(f37) = -1
	Pol(f35) = -1
	Pol(f28) = -2
	Pol(f18) = 1
	Pol(f16) = 0
and size complexities
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-0) = 1
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-1) = Ar_7
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-2) = Ar_8
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-3) = Ar_9
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-4) = Ar_10
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-5) = Ar_15
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-6) = Ar_16
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-0) = 1
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-1) = Ar_7
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-2) = ?
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-3) = Ar_9
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-4) = ?
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-5) = Ar_15
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-6) = Ar_16
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-0) = 1
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-1) = Ar_7
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-2) = ?
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-3) = Ar_9
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-4) = ?
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-5) = Ar_15
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-6) = Ar_16
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-0) = Ar_0
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-1) = Ar_7
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-2) = Ar_8
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-3) = Ar_9
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-4) = Ar_10
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-5) = Ar_15
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-6) = Ar_16
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-0) = Ar_0
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-1) = Ar_7
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-2) = Ar_8
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-3) = Ar_9
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-4) = Ar_10
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-5) = Ar_15
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-6) = Ar_16
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-0) = Ar_0
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-1) = Ar_7
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-2) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-3) = Ar_9
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-4) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-5) = Ar_15
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-6) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-0) = Ar_0
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-1) = Ar_7
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-2) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-3) = Ar_9
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-4) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-5) = Ar_15
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-6) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-0) = Ar_0
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-1) = Ar_7
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-2) = 1
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-3) = Ar_9
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-4) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-5) = Ar_15
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-6) = ?
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-0) = Ar_0
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-1) = Ar_7
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-2) = ?
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-3) = Ar_9
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-4) = ?
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-5) = Ar_15
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-6) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-0) = Ar_0
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-1) = Ar_7
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-2) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-3) = Ar_9
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-4) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-5) = Ar_15
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-6) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-0) = Ar_0
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-1) = Ar_7
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-2) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-3) = Ar_9
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-4) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-5) = Ar_15
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-6) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-0) = Ar_0
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-1) = Ar_7
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-2) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-3) = Ar_9
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-4) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-5) = Ar_15
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-6) = 1
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-0) = Ar_0
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-1) = Ar_7
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-2) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-3) = Ar_9
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-4) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-5) = Ar_15
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-6) = 1
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-0) = Ar_0
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-1) = Ar_7
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-2) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-3) = Ar_9
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-4) = 2
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-5) = Ar_15
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-6) = 1
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]", 0-0) = Ar_0
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]", 0-1) = Ar_7
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]", 0-2) = ?
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]", 0-3) = Ar_9
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]", 0-4) = ?
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]", 0-5) = Ar_15
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]", 0-6) = ?
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]", 0-0) = Ar_0
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]", 0-1) = Ar_7
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]", 0-2) = ?
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]", 0-3) = Ar_9
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]", 0-4) = ?
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]", 0-5) = Ar_15
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]", 0-6) = ?
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]", 0-0) = Ar_0
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]", 0-1) = Ar_7
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]", 0-2) = ?
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]", 0-3) = Ar_9
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]", 0-4) = 2
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]", 0-5) = Ar_15
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]", 0-6) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-0) = Ar_0
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-1) = Ar_7
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-2) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-3) = Ar_9
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-4) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-5) = Ar_15
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-6) = ?
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-0) = Ar_0
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-1) = Ar_7
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-2) = ?
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-3) = Ar_9
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-4) = ?
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-5) = Ar_15
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-6) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-0) = Ar_0 + 1
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-1) = Ar_7
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-2) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-3) = Ar_9
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-4) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-5) = Ar_15
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-6) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-0) = Ar_0 + 1
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-1) = Ar_7
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-2) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-3) = Ar_9
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-4) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-5) = Ar_15
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-6) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-0) = 1
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-1) = Ar_7
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-2) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-3) = Ar_9
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-4) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-5) = Ar_15
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-6) = ?
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-0) = 1
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-1) = Ar_7
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-2) = ?
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-3) = Ar_9
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-4) = ?
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-5) = Ar_15
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-6) = Ar_16
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-0) = 1
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-1) = Ar_7
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-2) = ?
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-3) = Ar_9
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-4) = ?
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-5) = Ar_15
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-6) = Ar_16
	S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-0) = Ar_0
	S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-1) = Ar_7
	S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-2) = Ar_8
	S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-3) = Ar_9
	S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-4) = Ar_10
	S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-5) = Ar_15
	S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-6) = Ar_16
orients the transitions
	f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]
	f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]
	f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]
	f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
	f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
	f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]
	f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]
weakly and the transition
	f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]
strictly and produces the following problem:
9:	T:
		(Comp: 1, Cost: 0)                        koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)                        f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]
		(Comp: 32*Ar_7 + 32*Ar_8 + 4, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: 1, Cost: 1)                        f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ]
		(Comp: 1, Cost: 1)                        f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: 1, Cost: 1)                        f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: ?, Cost: 1)                        f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
		(Comp: ?, Cost: 1)                        f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: ?, Cost: 1)                        f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]
		(Comp: ?, Cost: 1)                        f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]
		(Comp: ?, Cost: 1)                        f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]
		(Comp: ?, Cost: 1)                        f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)                        f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)                        f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)                        f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)                        f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)                        f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)                        f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]
		(Comp: 1, Cost: 1)                        f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]
		(Comp: ?, Cost: 1)                        f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)                        f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(f52) = 1
	Pol(f37) = 1
	Pol(f35) = 1
	Pol(f28) = 0
	Pol(f18) = 0
and size complexities
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-0) = 1
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-1) = Ar_7
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-2) = Ar_8
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-3) = Ar_9
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-4) = Ar_10
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-5) = Ar_15
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]", 0-6) = Ar_16
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-0) = 1
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-1) = Ar_7
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-2) = 33*Ar_7 + 33*Ar_8 + 4356
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-3) = Ar_9
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-4) = ?
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-5) = Ar_15
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]", 0-6) = Ar_16
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-0) = 1
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-1) = Ar_7
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-2) = 33*Ar_7 + 33*Ar_8 + 4356
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-3) = Ar_9
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-4) = ?
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-5) = Ar_15
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]", 0-6) = Ar_16
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-0) = Ar_0
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-1) = Ar_7
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-2) = Ar_8
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-3) = Ar_9
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-4) = Ar_10
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-5) = Ar_15
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]", 0-6) = Ar_16
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-0) = Ar_0
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-1) = Ar_7
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-2) = Ar_8
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-3) = Ar_9
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-4) = Ar_10
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-5) = Ar_15
	S("f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]", 0-6) = Ar_16
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-0) = Ar_0
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-1) = Ar_7
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-2) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-3) = Ar_9
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-4) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-5) = Ar_15
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\\ Ar_7 >= Ar_8 ]", 0-6) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-0) = Ar_0
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-1) = Ar_7
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-2) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-3) = Ar_9
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-4) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-5) = Ar_15
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\\ Ar_7 >= Ar_8 ]", 0-6) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-0) = Ar_0
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-1) = Ar_7
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-2) = 1
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-3) = Ar_9
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-4) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-5) = Ar_15
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\\ Ar_8 = 1 ]", 0-6) = ?
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-0) = Ar_0
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-1) = Ar_7
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-2) = ?
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-3) = Ar_9
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-4) = ?
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-5) = Ar_15
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ X' + 1 >= Ar_16 ]", 0-6) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-0) = Ar_0
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-1) = Ar_7
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-2) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-3) = Ar_9
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-4) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-5) = Ar_15
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\\ Ar_9 >= Ar_10 ]", 0-6) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-0) = Ar_0
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-1) = Ar_7
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-2) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-3) = Ar_9
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-4) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-5) = Ar_15
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\\ Ar_9 >= Ar_10 ]", 0-6) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-0) = Ar_0
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-1) = Ar_7
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-2) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-3) = Ar_9
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-4) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-5) = Ar_15
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\\ Ar_9 >= Ar_10 /\\ Ar_16 = 1 ]", 0-6) = 1
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-0) = Ar_0
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-1) = Ar_7
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-2) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-3) = Ar_9
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-4) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-5) = Ar_15
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\\ Ar_10 >= 2 /\\ Ar_16 = 1 ]", 0-6) = 1
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-0) = Ar_0
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-1) = Ar_7
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-2) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-3) = Ar_9
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-4) = 2
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-5) = Ar_15
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\\ Ar_10 = 1 /\\ Ar_16 = 1 ]", 0-6) = 1
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]", 0-0) = Ar_0
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]", 0-1) = Ar_7
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]", 0-2) = ?
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]", 0-3) = Ar_9
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]", 0-4) = ?
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]", 0-5) = Ar_15
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]", 0-6) = ?
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]", 0-0) = Ar_0
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]", 0-1) = Ar_7
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]", 0-2) = ?
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]", 0-3) = Ar_9
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]", 0-4) = ?
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]", 0-5) = Ar_15
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]", 0-6) = ?
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]", 0-0) = Ar_0
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]", 0-1) = Ar_7
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]", 0-2) = ?
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]", 0-3) = Ar_9
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]", 0-4) = 2
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]", 0-5) = Ar_15
	S("f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]", 0-6) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-0) = Ar_0
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-1) = Ar_7
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-2) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-3) = Ar_9
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-4) = ?
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-5) = Ar_15
	S("f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]", 0-6) = ?
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-0) = Ar_0
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-1) = Ar_7
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-2) = ?
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-3) = Ar_9
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-4) = ?
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-5) = Ar_15
	S("f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\\ 3*X' >= Ar_15 + 1 /\\ Ar_16 >= X' + 2 ]", 0-6) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-0) = Ar_0 + 1
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-1) = Ar_7
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-2) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-3) = Ar_9
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-4) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-5) = Ar_15
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\\ Ar_8 >= Ar_7 + 1 ]", 0-6) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-0) = Ar_0 + 1
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-1) = Ar_7
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-2) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-3) = Ar_9
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-4) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-5) = Ar_15
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\\ Ar_8 >= Ar_7 + 1 ]", 0-6) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-0) = 1
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-1) = Ar_7
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-2) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-3) = Ar_9
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-4) = ?
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-5) = Ar_15
	S("f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\\ Ar_0 + 1 = 0 ]", 0-6) = ?
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-0) = 1
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-1) = Ar_7
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-2) = 33*Ar_7 + 33*Ar_8 + 4356
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-3) = Ar_9
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-4) = ?
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-5) = Ar_15
	S("f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]", 0-6) = Ar_16
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-0) = 1
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-1) = Ar_7
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-2) = 33*Ar_7 + 33*Ar_8 + 143748
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-3) = Ar_9
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-4) = ?
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-5) = Ar_15
	S("f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]", 0-6) = Ar_16
	S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-0) = Ar_0
	S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-1) = Ar_7
	S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-2) = Ar_8
	S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-3) = Ar_9
	S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-4) = Ar_10
	S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-5) = Ar_15
	S("koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]", 0-6) = Ar_16
orients the transitions
	f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]
	f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]
	f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]
	f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
	f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
	f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]
weakly and the transition
	f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
strictly and produces the following problem:
10:	T:
		(Comp: 1, Cost: 0)                        koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)                        f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]
		(Comp: 32*Ar_7 + 32*Ar_8 + 4, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: 1, Cost: 1)                        f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ]
		(Comp: 1, Cost: 1)                        f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: 1, Cost: 1)                        f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: 24*Ar_7 + 24*Ar_8 + 3, Cost: 1)    f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
		(Comp: ?, Cost: 1)                        f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: ?, Cost: 1)                        f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]
		(Comp: ?, Cost: 1)                        f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]
		(Comp: ?, Cost: 1)                        f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]
		(Comp: ?, Cost: 1)                        f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)                        f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)                        f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
		(Comp: ?, Cost: 1)                        f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)                        f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)                        f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)                        f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]
		(Comp: 1, Cost: 1)                        f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]
		(Comp: ?, Cost: 1)                        f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)                        f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(koat_start) = 2*V_4 - 2*V_5 + 1
	Pol(f0) = 2*V_4 - 2*V_5 + 1
	Pol(f16) = 2*V_4 - 2*V_5 + 1
	Pol(f28) = 2*V_4 - 2*V_5 + 1
	Pol(f18) = 2*V_4 - 2*V_5 + 1
	Pol(f76) = 2*V_4 - 2*V_5
	Pol(f35) = 2*V_4 - 2*V_5 + 1
	Pol(f37) = 2*V_4 - 2*V_5 + 1
	Pol(f52) = 2*V_4 - 2*V_5
orients all transitions weakly and the transitions
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
	f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
	f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]
strictly and produces the following problem:
11:	T:
		(Comp: 1, Cost: 0)                        koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)                        f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]
		(Comp: 32*Ar_7 + 32*Ar_8 + 4, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: 1, Cost: 1)                        f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ]
		(Comp: 1, Cost: 1)                        f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: 1, Cost: 1)                        f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: 24*Ar_7 + 24*Ar_8 + 3, Cost: 1)    f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
		(Comp: ?, Cost: 1)                        f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: ?, Cost: 1)                        f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]
		(Comp: ?, Cost: 1)                        f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]
		(Comp: ?, Cost: 1)                        f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)                        f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)                        f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]
		(Comp: 1, Cost: 1)                        f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)                        f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]
	start location:	koat_start
	leaf cost:	0

Repeatedly propagating knowledge in problem 11 produces the following problem:
12:	T:
		(Comp: 1, Cost: 0)                        koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)                        f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]
		(Comp: 32*Ar_7 + 32*Ar_8 + 4, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: 1, Cost: 1)                        f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ]
		(Comp: 1, Cost: 1)                        f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: 1, Cost: 1)                        f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: 24*Ar_7 + 24*Ar_8 + 3, Cost: 1)    f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
		(Comp: ?, Cost: 1)                        f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: 4*Ar_9 + 4*Ar_10 + 2, Cost: 1)     f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]
		(Comp: 4*Ar_9 + 4*Ar_10 + 2, Cost: 1)     f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]
		(Comp: 4*Ar_9 + 4*Ar_10 + 2, Cost: 1)     f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
		(Comp: ?, Cost: 1)                        f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)                        f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]
		(Comp: 1, Cost: 1)                        f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)                        f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(koat_start) = 3*V_6 - 2*V_7
	Pol(f0) = 3*V_6 - 2*V_7
	Pol(f16) = 3*V_6 - 2*V_7
	Pol(f28) = 3*V_6 - 2*V_7
	Pol(f18) = 3*V_6 - 2*V_7
	Pol(f76) = 3*V_6 - 2*V_7
	Pol(f35) = 3*V_6 - 2*V_7
	Pol(f37) = 3*V_6 - 2*V_7 - 1
	Pol(f52) = 3*V_6 - 2*V_7 - 1
orients all transitions weakly and the transition
	f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
strictly and produces the following problem:
13:	T:
		(Comp: 1, Cost: 0)                        koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)                        f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]
		(Comp: 32*Ar_7 + 32*Ar_8 + 4, Cost: 1)    f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: 1, Cost: 1)                        f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ]
		(Comp: 1, Cost: 1)                        f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: 1, Cost: 1)                        f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: 24*Ar_7 + 24*Ar_8 + 3, Cost: 1)    f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
		(Comp: ?, Cost: 1)                        f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: 4*Ar_9 + 4*Ar_10 + 2, Cost: 1)     f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]
		(Comp: 4*Ar_9 + 4*Ar_10 + 2, Cost: 1)     f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]
		(Comp: 4*Ar_9 + 4*Ar_10 + 2, Cost: 1)     f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
		(Comp: 3*Ar_15 + 2*Ar_16, Cost: 1)        f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)                        f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]
		(Comp: 1, Cost: 1)                        f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)     f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)      f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)                        f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]
	start location:	koat_start
	leaf cost:	0

Repeatedly propagating knowledge in problem 13 produces the following problem:
14:	T:
		(Comp: 1, Cost: 0)                                             koat_start(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)                                             f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 ]
		(Comp: 32*Ar_7 + 32*Ar_8 + 4, Cost: 1)                         f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: 1, Cost: 1)                                             f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(-1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= Ar_7 + 1 /\ Ar_0 + 1 = 0 ]
		(Comp: 1, Cost: 1)                                             f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 0 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: 1, Cost: 1)                                             f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f76(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 + 2 /\ Ar_8 >= Ar_7 + 1 ]
		(Comp: 24*Ar_7 + 24*Ar_8 + 3, Cost: 1)                         f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8 + 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ Ar_16 >= X' + 2 ]
		(Comp: 3*Ar_15 + 2*Ar_16 + 18*Ar_9 + 18*Ar_10 + 9, Cost: 1)    f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16 + 1)) [ Ar_10 >= Ar_9 + 1 ]
		(Comp: 4*Ar_9 + 4*Ar_10 + 2, Cost: 1)                          f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, Ar_16)) [ Ar_10 = 1 ]
		(Comp: 4*Ar_9 + 4*Ar_10 + 2, Cost: 1)                          f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_10 >= 2 ]
		(Comp: 4*Ar_9 + 4*Ar_10 + 2, Cost: 1)                          f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ 0 >= Ar_10 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)                          f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, 2, Ar_15, 1)) [ Ar_9 >= 1 /\ Ar_10 = 1 /\ Ar_16 = 1 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)                          f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ Ar_9 >= Ar_10 /\ Ar_10 >= 2 /\ Ar_16 = 1 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)                          f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, 1)) [ 0 >= Ar_10 /\ Ar_9 >= Ar_10 /\ Ar_16 = 1 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)                          f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_16 >= 2 /\ Ar_9 >= Ar_10 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)                          f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f52(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_16 /\ Ar_9 >= Ar_10 ]
		(Comp: 3*Ar_15 + 2*Ar_16, Cost: 1)                             f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f37(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_15 >= 2*X' /\ 3*X' >= Ar_15 + 1 /\ X' + 1 >= Ar_16 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)                           f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, 1, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= 1 /\ Ar_8 = 1 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)                           f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_8 >= 2 /\ Ar_7 >= Ar_8 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)                           f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f35(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_8 /\ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)                                             f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 >= 2 ]
		(Comp: 1, Cost: 1)                                             f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f28(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ 0 >= Ar_0 ]
		(Comp: 2*Ar_9 + 2*Ar_10 + 1, Cost: 1)                          f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10 + 1, Ar_15, Ar_16)) [ Ar_9 >= Ar_10 ]
		(Comp: 8*Ar_7 + 8*Ar_8 + 1, Cost: 1)                           f16(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f18(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_7 >= Ar_8 ]
		(Comp: 1, Cost: 1)                                             f0(Ar_0, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16) -> Com_1(f16(1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_15, Ar_16)) [ Ar_0 = 1 ]
	start location:	koat_start
	leaf cost:	0

Complexity upper bound 88*Ar_7 + 88*Ar_8 + 6*Ar_15 + 4*Ar_16 + 42*Ar_9 + 42*Ar_10 + 39

Time: 4.370 sec (SMT: 4.044 sec)