YES(?, 17)

Initial complexity problem:
1:	T:
		(1, 1)    f0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s) -> f12(3, t, 3, 1, 0, f, g, h, i, j, k, l, m, n, o, p, q, r, s)
		(?, 1)    f12(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s) -> f12(a, b, c, t, e + 1, f, g, h, i, j, k, l, m, n, o, p, q, r, s) [ c >= e + 1 ]
		(?, 1)    f24(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s) -> f24(a, b, c, d, e, f, g + 1, t, i, j, k, l, m, n, o, p, q, r, s) [ f >= g + 1 ]
		(?, 1)    f36(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s) -> f36(a, b, c, d, e, f, g, h, i, j + 1, t, l, m, n, o, p, q, r, s) [ i >= j + 1 ]
		(?, 1)    f36(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s) -> f46(a, b, c, d, e, f, g, h, i, j, k, k, k, n, o, p, q, r, s) [ j >= i ]
		(?, 1)    f24(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s) -> f36(a, b, c, d, e, f, g, h, a, 0, 1, l, m, h, h, t, q, r, s) [ g >= f ]
		(?, 1)    f12(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s) -> f24(a, b, c, d, e, a, 0, 1, i, j, k, l, m, n, o, p, d, d, t) [ e >= c ]
	start location:	f0
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, c, e, f, g, i, j].
We thus obtain the following problem:
2:	T:
		(?, 1)    f12(a, c, e, f, g, i, j) -> f24(a, c, e, a, 0, i, j) [ e >= c ]
		(?, 1)    f24(a, c, e, f, g, i, j) -> f36(a, c, e, f, g, a, 0) [ g >= f ]
		(?, 1)    f36(a, c, e, f, g, i, j) -> f46(a, c, e, f, g, i, j) [ j >= i ]
		(?, 1)    f36(a, c, e, f, g, i, j) -> f36(a, c, e, f, g, i, j + 1) [ i >= j + 1 ]
		(?, 1)    f24(a, c, e, f, g, i, j) -> f24(a, c, e, f, g + 1, i, j) [ f >= g + 1 ]
		(?, 1)    f12(a, c, e, f, g, i, j) -> f12(a, c, e + 1, f, g, i, j) [ c >= e + 1 ]
		(1, 1)    f0(a, c, e, f, g, i, j) -> f12(3, 3, 0, f, g, i, j)
	start location:	f0
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(?, 1)    f12(a, c, e, f, g, i, j) -> f24(a, c, e, a, 0, i, j) [ e >= c ]
		(?, 1)    f24(a, c, e, f, g, i, j) -> f36(a, c, e, f, g, a, 0) [ g >= f ]
		(?, 1)    f36(a, c, e, f, g, i, j) -> f36(a, c, e, f, g, i, j + 1) [ i >= j + 1 ]
		(?, 1)    f24(a, c, e, f, g, i, j) -> f24(a, c, e, f, g + 1, i, j) [ f >= g + 1 ]
		(?, 1)    f12(a, c, e, f, g, i, j) -> f12(a, c, e + 1, f, g, i, j) [ c >= e + 1 ]
		(1, 1)    f0(a, c, e, f, g, i, j) -> f12(3, 3, 0, f, g, i, j)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f12) = 2
	Pol(f24) = 1
	Pol(f36) = -1
	Pol(f0) = 2
orients all transitions weakly and the transitions
	f24(a, c, e, f, g, i, j) -> f36(a, c, e, f, g, a, 0) [ g >= f ]
	f12(a, c, e, f, g, i, j) -> f24(a, c, e, a, 0, i, j) [ e >= c ]
strictly and produces the following problem:
4:	T:
		(2, 1)    f12(a, c, e, f, g, i, j) -> f24(a, c, e, a, 0, i, j) [ e >= c ]
		(2, 1)    f24(a, c, e, f, g, i, j) -> f36(a, c, e, f, g, a, 0) [ g >= f ]
		(?, 1)    f36(a, c, e, f, g, i, j) -> f36(a, c, e, f, g, i, j + 1) [ i >= j + 1 ]
		(?, 1)    f24(a, c, e, f, g, i, j) -> f24(a, c, e, f, g + 1, i, j) [ f >= g + 1 ]
		(?, 1)    f12(a, c, e, f, g, i, j) -> f12(a, c, e + 1, f, g, i, j) [ c >= e + 1 ]
		(1, 1)    f0(a, c, e, f, g, i, j) -> f12(3, 3, 0, f, g, i, j)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f12) = V_2 - V_3
	Pol(f24) = 4*V_1 + V_2 - V_3 - 4*V_4 - V_5 - 2
	Pol(f36) = V_1 + V_2 - V_3 + V_4 - 6*V_5 + 3*V_6 - V_7 - 2
	Pol(f0) = 3
orients all transitions weakly and the transition
	f12(a, c, e, f, g, i, j) -> f12(a, c, e + 1, f, g, i, j) [ c >= e + 1 ]
strictly and produces the following problem:
5:	T:
		(2, 1)    f12(a, c, e, f, g, i, j) -> f24(a, c, e, a, 0, i, j) [ e >= c ]
		(2, 1)    f24(a, c, e, f, g, i, j) -> f36(a, c, e, f, g, a, 0) [ g >= f ]
		(?, 1)    f36(a, c, e, f, g, i, j) -> f36(a, c, e, f, g, i, j + 1) [ i >= j + 1 ]
		(?, 1)    f24(a, c, e, f, g, i, j) -> f24(a, c, e, f, g + 1, i, j) [ f >= g + 1 ]
		(3, 1)    f12(a, c, e, f, g, i, j) -> f12(a, c, e + 1, f, g, i, j) [ c >= e + 1 ]
		(1, 1)    f0(a, c, e, f, g, i, j) -> f12(3, 3, 0, f, g, i, j)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f12) = V_1 + 2
	Pol(f24) = V_4 - V_5 + 2
	Pol(f36) = V_1 + V_4 - V_5 - V_6 - V_7 + 2
	Pol(f0) = 5
orients all transitions weakly and the transition
	f24(a, c, e, f, g, i, j) -> f24(a, c, e, f, g + 1, i, j) [ f >= g + 1 ]
strictly and produces the following problem:
6:	T:
		(2, 1)    f12(a, c, e, f, g, i, j) -> f24(a, c, e, a, 0, i, j) [ e >= c ]
		(2, 1)    f24(a, c, e, f, g, i, j) -> f36(a, c, e, f, g, a, 0) [ g >= f ]
		(?, 1)    f36(a, c, e, f, g, i, j) -> f36(a, c, e, f, g, i, j + 1) [ i >= j + 1 ]
		(5, 1)    f24(a, c, e, f, g, i, j) -> f24(a, c, e, f, g + 1, i, j) [ f >= g + 1 ]
		(3, 1)    f12(a, c, e, f, g, i, j) -> f12(a, c, e + 1, f, g, i, j) [ c >= e + 1 ]
		(1, 1)    f0(a, c, e, f, g, i, j) -> f12(3, 3, 0, f, g, i, j)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f12) = V_1
	Pol(f24) = V_1
	Pol(f36) = V_6 - V_7
	Pol(f0) = 3
orients all transitions weakly and the transition
	f36(a, c, e, f, g, i, j) -> f36(a, c, e, f, g, i, j + 1) [ i >= j + 1 ]
strictly and produces the following problem:
7:	T:
		(2, 1)    f12(a, c, e, f, g, i, j) -> f24(a, c, e, a, 0, i, j) [ e >= c ]
		(2, 1)    f24(a, c, e, f, g, i, j) -> f36(a, c, e, f, g, a, 0) [ g >= f ]
		(3, 1)    f36(a, c, e, f, g, i, j) -> f36(a, c, e, f, g, i, j + 1) [ i >= j + 1 ]
		(5, 1)    f24(a, c, e, f, g, i, j) -> f24(a, c, e, f, g + 1, i, j) [ f >= g + 1 ]
		(3, 1)    f12(a, c, e, f, g, i, j) -> f12(a, c, e + 1, f, g, i, j) [ c >= e + 1 ]
		(1, 1)    f0(a, c, e, f, g, i, j) -> f12(3, 3, 0, f, g, i, j)
	start location:	f0
	leaf cost:	1

Complexity upper bound 17

Time: 0.282 sec (SMT: 0.262 sec)