MAYBE

Initial complexity problem:
1:	T:
		(Comp: ?, Cost: 1)    f17(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) -> Com_1(f17(Ar_0, Fresh_11, Ar_2, Ar_3 + 1, Fresh_12, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14)) [ Ar_0 >= Ar_1 + 1 /\ Ar_2 >= 0 /\ Ar_3 >= 0 ]
		(Comp: ?, Cost: 1)    f17(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) -> Com_1(f17(Ar_0, Fresh_9, Ar_2, Ar_3 + 1, Fresh_10, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14)) [ Ar_1 >= Ar_0 + 1 /\ Ar_2 >= 0 /\ Ar_3 >= 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) -> Com_1(f17(Ar_0, Fresh_7, Ar_2, 1, Fresh_8, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14)) [ Ar_5 >= 0 /\ Ar_0 >= Ar_1 + 1 ]
		(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) -> Com_1(f17(Ar_0, Fresh_5, Ar_2, 1, Fresh_6, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14)) [ Ar_5 >= 0 /\ Ar_1 >= Ar_0 + 1 ]
		(Comp: ?, Cost: 1)    f17(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) -> Com_1(f20(Ar_1, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Fresh_4, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14)) [ Ar_2 >= 0 /\ Ar_3 >= 0 /\ Ar_1 = Ar_0 ]
		(Comp: ?, Cost: 1)    f22(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) -> Com_1(f18(Ar_0, Ar_7, Ar_2, Ar_3, Ar_4, Ar_5, Fresh_2, Ar_7, 2, Fresh_3, Fresh_3, Fresh_3, Fresh_3, 3, 0)) [ Ar_0 >= Ar_7 + 1 /\ Ar_5 >= 0 ]
		(Comp: ?, Cost: 1)    f22(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) -> Com_1(f18(Ar_0, Ar_7, Ar_2, Ar_3, Ar_4, Ar_5, Fresh_0, Ar_7, 2, Fresh_1, Fresh_1, Fresh_1, Fresh_1, 3, 0)) [ Ar_7 >= Ar_0 + 1 /\ Ar_5 >= 0 ]
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14) -> Com_1(f22(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)) [ 0 <= 0 ]
	start location:	koat_start
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7].
We thus obtain the following problem:
2:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f22(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7)) [ 0 <= 0 ]
		(Comp: ?, Cost: 1)    f22(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f18(Ar_0, Ar_7, Ar_2, Ar_3, Ar_5, Ar_7)) [ Ar_7 >= Ar_0 + 1 /\ Ar_5 >= 0 ]
		(Comp: ?, Cost: 1)    f22(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f18(Ar_0, Ar_7, Ar_2, Ar_3, Ar_5, Ar_7)) [ Ar_0 >= Ar_7 + 1 /\ Ar_5 >= 0 ]
		(Comp: ?, Cost: 1)    f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f20(Ar_1, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7)) [ Ar_2 >= 0 /\ Ar_3 >= 0 /\ Ar_1 = Ar_0 ]
		(Comp: ?, Cost: 1)    f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f17(Ar_0, Fresh_5, Ar_2, 1, Ar_5, Ar_7)) [ Ar_5 >= 0 /\ Ar_1 >= Ar_0 + 1 ]
		(Comp: ?, Cost: 1)    f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f17(Ar_0, Fresh_7, Ar_2, 1, Ar_5, Ar_7)) [ Ar_5 >= 0 /\ Ar_0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f17(Ar_0, Fresh_9, Ar_2, Ar_3 + 1, Ar_5, Ar_7)) [ Ar_1 >= Ar_0 + 1 /\ Ar_2 >= 0 /\ Ar_3 >= 0 ]
		(Comp: ?, Cost: 1)    f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f17(Ar_0, Fresh_11, Ar_2, Ar_3 + 1, Ar_5, Ar_7)) [ Ar_0 >= Ar_1 + 1 /\ Ar_2 >= 0 /\ Ar_3 >= 0 ]
	start location:	koat_start
	leaf cost:	0

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f22(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)    f22(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f18(Ar_0, Ar_7, Ar_2, Ar_3, Ar_5, Ar_7)) [ Ar_7 >= Ar_0 + 1 /\ Ar_5 >= 0 ]
		(Comp: 1, Cost: 1)    f22(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f18(Ar_0, Ar_7, Ar_2, Ar_3, Ar_5, Ar_7)) [ Ar_0 >= Ar_7 + 1 /\ Ar_5 >= 0 ]
		(Comp: ?, Cost: 1)    f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f20(Ar_1, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7)) [ Ar_2 >= 0 /\ Ar_3 >= 0 /\ Ar_1 = Ar_0 ]
		(Comp: 1, Cost: 1)    f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f17(Ar_0, Fresh_5, Ar_2, 1, Ar_5, Ar_7)) [ Ar_5 >= 0 /\ Ar_1 >= Ar_0 + 1 ]
		(Comp: 1, Cost: 1)    f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f17(Ar_0, Fresh_7, Ar_2, 1, Ar_5, Ar_7)) [ Ar_5 >= 0 /\ Ar_0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f17(Ar_0, Fresh_9, Ar_2, Ar_3 + 1, Ar_5, Ar_7)) [ Ar_1 >= Ar_0 + 1 /\ Ar_2 >= 0 /\ Ar_3 >= 0 ]
		(Comp: ?, Cost: 1)    f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f17(Ar_0, Fresh_11, Ar_2, Ar_3 + 1, Ar_5, Ar_7)) [ Ar_0 >= Ar_1 + 1 /\ Ar_2 >= 0 /\ Ar_3 >= 0 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(koat_start) = 1
	Pol(f22) = 1
	Pol(f18) = 1
	Pol(f17) = 1
	Pol(f20) = 0
orients all transitions weakly and the transition
	f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f20(Ar_1, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7)) [ Ar_2 >= 0 /\ Ar_3 >= 0 /\ Ar_1 = Ar_0 ]
strictly and produces the following problem:
4:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f22(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)    f22(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f18(Ar_0, Ar_7, Ar_2, Ar_3, Ar_5, Ar_7)) [ Ar_7 >= Ar_0 + 1 /\ Ar_5 >= 0 ]
		(Comp: 1, Cost: 1)    f22(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f18(Ar_0, Ar_7, Ar_2, Ar_3, Ar_5, Ar_7)) [ Ar_0 >= Ar_7 + 1 /\ Ar_5 >= 0 ]
		(Comp: 1, Cost: 1)    f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f20(Ar_1, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7)) [ Ar_2 >= 0 /\ Ar_3 >= 0 /\ Ar_1 = Ar_0 ]
		(Comp: 1, Cost: 1)    f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f17(Ar_0, Fresh_5, Ar_2, 1, Ar_5, Ar_7)) [ Ar_5 >= 0 /\ Ar_1 >= Ar_0 + 1 ]
		(Comp: 1, Cost: 1)    f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f17(Ar_0, Fresh_7, Ar_2, 1, Ar_5, Ar_7)) [ Ar_5 >= 0 /\ Ar_0 >= Ar_1 + 1 ]
		(Comp: ?, Cost: 1)    f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f17(Ar_0, Fresh_9, Ar_2, Ar_3 + 1, Ar_5, Ar_7)) [ Ar_1 >= Ar_0 + 1 /\ Ar_2 >= 0 /\ Ar_3 >= 0 ]
		(Comp: ?, Cost: 1)    f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f17(Ar_0, Fresh_11, Ar_2, Ar_3 + 1, Ar_5, Ar_7)) [ Ar_0 >= Ar_1 + 1 /\ Ar_2 >= 0 /\ Ar_3 >= 0 ]
	start location:	koat_start
	leaf cost:	0

Applied AI with 'oct' on problem 4 to obtain the following invariants:
  For symbol f17: X_5 >= 0 /\ X_4 + X_5 - 1 >= 0 /\ X_4 - 1 >= 0
  For symbol f18: X_2 - X_6 >= 0 /\ -X_2 + X_6 >= 0 /\ X_5 >= 0


This yielded the following problem:
5:	T:
		(Comp: ?, Cost: 1)    f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f17(Ar_0, Fresh_11, Ar_2, Ar_3 + 1, Ar_5, Ar_7)) [ Ar_5 >= 0 /\ Ar_3 + Ar_5 - 1 >= 0 /\ Ar_3 - 1 >= 0 /\ Ar_0 >= Ar_1 + 1 /\ Ar_2 >= 0 /\ Ar_3 >= 0 ]
		(Comp: ?, Cost: 1)    f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f17(Ar_0, Fresh_9, Ar_2, Ar_3 + 1, Ar_5, Ar_7)) [ Ar_5 >= 0 /\ Ar_3 + Ar_5 - 1 >= 0 /\ Ar_3 - 1 >= 0 /\ Ar_1 >= Ar_0 + 1 /\ Ar_2 >= 0 /\ Ar_3 >= 0 ]
		(Comp: 1, Cost: 1)    f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f17(Ar_0, Fresh_7, Ar_2, 1, Ar_5, Ar_7)) [ Ar_1 - Ar_7 >= 0 /\ -Ar_1 + Ar_7 >= 0 /\ Ar_5 >= 0 /\ Ar_0 >= Ar_1 + 1 ]
		(Comp: 1, Cost: 1)    f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f17(Ar_0, Fresh_5, Ar_2, 1, Ar_5, Ar_7)) [ Ar_1 - Ar_7 >= 0 /\ -Ar_1 + Ar_7 >= 0 /\ Ar_5 >= 0 /\ Ar_1 >= Ar_0 + 1 ]
		(Comp: 1, Cost: 1)    f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f20(Ar_1, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7)) [ Ar_5 >= 0 /\ Ar_3 + Ar_5 - 1 >= 0 /\ Ar_3 - 1 >= 0 /\ Ar_2 >= 0 /\ Ar_3 >= 0 /\ Ar_1 = Ar_0 ]
		(Comp: 1, Cost: 1)    f22(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f18(Ar_0, Ar_7, Ar_2, Ar_3, Ar_5, Ar_7)) [ Ar_0 >= Ar_7 + 1 /\ Ar_5 >= 0 ]
		(Comp: 1, Cost: 1)    f22(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f18(Ar_0, Ar_7, Ar_2, Ar_3, Ar_5, Ar_7)) [ Ar_7 >= Ar_0 + 1 /\ Ar_5 >= 0 ]
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7) -> Com_1(f22(Ar_0, Ar_1, Ar_2, Ar_3, Ar_5, Ar_7)) [ 0 <= 0 ]
	start location:	koat_start
	leaf cost:	0

Complexity upper bound ?

Time: 2.317 sec (SMT: 2.234 sec)