YES(?, 87)

Initial complexity problem:
1:	T:
		(1, 1)    f0(a, b, c, d, e, f, g) -> f9(0, 0, h, d, e, f, g)
		(?, 1)    f9(a, b, c, d, e, f, g) -> f10(a, b, c, c, e, f, g) [ 0 >= c + 1 ]
		(?, 1)    f9(a, b, c, d, e, f, g) -> f10(a, b, c, c, e, f, g) [ c >= 1 ]
		(?, 1)    f10(a, b, c, d, e, f, g) -> f9(a + 1, a + 1, h, d, e, f, g) [ 9 >= a ]
		(?, 1)    f16(a, b, c, d, e, f, g) -> f28(a, b, c, d, e, f, g) [ a >= 10 ]
		(?, 1)    f16(a, b, c, d, e, f, g) -> f16(a + 1, b, c, d, a, h, h) [ 9 >= a /\ 0 >= h + 1 ]
		(?, 1)    f16(a, b, c, d, e, f, g) -> f16(a + 1, b, c, d, a, h, h) [ 9 >= a /\ h >= 1 ]
		(?, 1)    f16(a, b, c, d, e, f, g) -> f28(a, b, c, d, a, 0, 0) [ 9 >= a ]
		(?, 1)    f10(a, b, c, d, e, f, g) -> f16(0, b, c, d, e, f, g) [ a >= 10 ]
		(?, 1)    f9(a, b, c, d, e, f, g) -> f16(0, b, 0, 0, e, f, g) [ c = 0 ]
	start location:	f0
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, c].
We thus obtain the following problem:
2:	T:
		(?, 1)    f9(a, c) -> f16(0, 0) [ c = 0 ]
		(?, 1)    f10(a, c) -> f16(0, c) [ a >= 10 ]
		(?, 1)    f16(a, c) -> f28(a, c) [ 9 >= a ]
		(?, 1)    f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ h >= 1 ]
		(?, 1)    f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ 0 >= h + 1 ]
		(?, 1)    f16(a, c) -> f28(a, c) [ a >= 10 ]
		(?, 1)    f10(a, c) -> f9(a + 1, h) [ 9 >= a ]
		(?, 1)    f9(a, c) -> f10(a, c) [ c >= 1 ]
		(?, 1)    f9(a, c) -> f10(a, c) [ 0 >= c + 1 ]
		(1, 1)    f0(a, c) -> f9(0, h)
	start location:	f0
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(?, 1)    f9(a, c) -> f16(0, 0) [ c = 0 ]
		(?, 1)    f10(a, c) -> f16(0, c) [ a >= 10 ]
		(?, 1)    f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ h >= 1 ]
		(?, 1)    f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ 0 >= h + 1 ]
		(?, 1)    f10(a, c) -> f9(a + 1, h) [ 9 >= a ]
		(?, 1)    f9(a, c) -> f10(a, c) [ c >= 1 ]
		(?, 1)    f9(a, c) -> f10(a, c) [ 0 >= c + 1 ]
		(1, 1)    f0(a, c) -> f9(0, h)
	start location:	f0
	leaf cost:	2

A polynomial rank function with
	Pol(f9) = 1
	Pol(f16) = 0
	Pol(f10) = 1
	Pol(f0) = 1
orients all transitions weakly and the transition
	f9(a, c) -> f16(0, 0) [ c = 0 ]
strictly and produces the following problem:
4:	T:
		(1, 1)    f9(a, c) -> f16(0, 0) [ c = 0 ]
		(?, 1)    f10(a, c) -> f16(0, c) [ a >= 10 ]
		(?, 1)    f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ h >= 1 ]
		(?, 1)    f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ 0 >= h + 1 ]
		(?, 1)    f10(a, c) -> f9(a + 1, h) [ 9 >= a ]
		(?, 1)    f9(a, c) -> f10(a, c) [ c >= 1 ]
		(?, 1)    f9(a, c) -> f10(a, c) [ 0 >= c + 1 ]
		(1, 1)    f0(a, c) -> f9(0, h)
	start location:	f0
	leaf cost:	2

A polynomial rank function with
	Pol(f9) = 1
	Pol(f16) = 0
	Pol(f10) = 1
	Pol(f0) = 1
orients all transitions weakly and the transition
	f10(a, c) -> f16(0, c) [ a >= 10 ]
strictly and produces the following problem:
5:	T:
		(1, 1)    f9(a, c) -> f16(0, 0) [ c = 0 ]
		(1, 1)    f10(a, c) -> f16(0, c) [ a >= 10 ]
		(?, 1)    f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ h >= 1 ]
		(?, 1)    f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ 0 >= h + 1 ]
		(?, 1)    f10(a, c) -> f9(a + 1, h) [ 9 >= a ]
		(?, 1)    f9(a, c) -> f10(a, c) [ c >= 1 ]
		(?, 1)    f9(a, c) -> f10(a, c) [ 0 >= c + 1 ]
		(1, 1)    f0(a, c) -> f9(0, h)
	start location:	f0
	leaf cost:	2

A polynomial rank function with
	Pol(f9) = 10
	Pol(f16) = -V_1 + 10
	Pol(f10) = 10
	Pol(f0) = 10
orients all transitions weakly and the transition
	f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ 0 >= h + 1 ]
strictly and produces the following problem:
6:	T:
		(1, 1)     f9(a, c) -> f16(0, 0) [ c = 0 ]
		(1, 1)     f10(a, c) -> f16(0, c) [ a >= 10 ]
		(?, 1)     f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ h >= 1 ]
		(10, 1)    f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ 0 >= h + 1 ]
		(?, 1)     f10(a, c) -> f9(a + 1, h) [ 9 >= a ]
		(?, 1)     f9(a, c) -> f10(a, c) [ c >= 1 ]
		(?, 1)     f9(a, c) -> f10(a, c) [ 0 >= c + 1 ]
		(1, 1)     f0(a, c) -> f9(0, h)
	start location:	f0
	leaf cost:	2

A polynomial rank function with
	Pol(f9) = 10
	Pol(f16) = -V_1 + 10
	Pol(f10) = 10
	Pol(f0) = 10
orients all transitions weakly and the transition
	f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ h >= 1 ]
strictly and produces the following problem:
7:	T:
		(1, 1)     f9(a, c) -> f16(0, 0) [ c = 0 ]
		(1, 1)     f10(a, c) -> f16(0, c) [ a >= 10 ]
		(10, 1)    f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ h >= 1 ]
		(10, 1)    f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ 0 >= h + 1 ]
		(?, 1)     f10(a, c) -> f9(a + 1, h) [ 9 >= a ]
		(?, 1)     f9(a, c) -> f10(a, c) [ c >= 1 ]
		(?, 1)     f9(a, c) -> f10(a, c) [ 0 >= c + 1 ]
		(1, 1)     f0(a, c) -> f9(0, h)
	start location:	f0
	leaf cost:	2

A polynomial rank function with
	Pol(f9) = -2*V_1 + 20
	Pol(f10) = -2*V_1 + 19
and size complexities
	S("f0(a, c) -> f9(0, h)", 0-0) = 0
	S("f0(a, c) -> f9(0, h)", 0-1) = ?
	S("f9(a, c) -> f10(a, c) [ 0 >= c + 1 ]", 0-0) = 10
	S("f9(a, c) -> f10(a, c) [ 0 >= c + 1 ]", 0-1) = ?
	S("f9(a, c) -> f10(a, c) [ c >= 1 ]", 0-0) = 10
	S("f9(a, c) -> f10(a, c) [ c >= 1 ]", 0-1) = ?
	S("f10(a, c) -> f9(a + 1, h) [ 9 >= a ]", 0-0) = 10
	S("f10(a, c) -> f9(a + 1, h) [ 9 >= a ]", 0-1) = ?
	S("f16(a, c) -> f16(a + 1, c) [ 9 >= a /\\ 0 >= h + 1 ]", 0-0) = 10
	S("f16(a, c) -> f16(a + 1, c) [ 9 >= a /\\ 0 >= h + 1 ]", 0-1) = ?
	S("f16(a, c) -> f16(a + 1, c) [ 9 >= a /\\ h >= 1 ]", 0-0) = 10
	S("f16(a, c) -> f16(a + 1, c) [ 9 >= a /\\ h >= 1 ]", 0-1) = ?
	S("f10(a, c) -> f16(0, c) [ a >= 10 ]", 0-0) = 0
	S("f10(a, c) -> f16(0, c) [ a >= 10 ]", 0-1) = ?
	S("f9(a, c) -> f16(0, 0) [ c = 0 ]", 0-0) = 0
	S("f9(a, c) -> f16(0, 0) [ c = 0 ]", 0-1) = 0
orients the transitions
	f9(a, c) -> f10(a, c) [ c >= 1 ]
	f9(a, c) -> f10(a, c) [ 0 >= c + 1 ]
	f10(a, c) -> f9(a + 1, h) [ 9 >= a ]
weakly and the transition
	f10(a, c) -> f9(a + 1, h) [ 9 >= a ]
strictly and produces the following problem:
8:	T:
		(1, 1)     f9(a, c) -> f16(0, 0) [ c = 0 ]
		(1, 1)     f10(a, c) -> f16(0, c) [ a >= 10 ]
		(10, 1)    f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ h >= 1 ]
		(10, 1)    f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ 0 >= h + 1 ]
		(20, 1)    f10(a, c) -> f9(a + 1, h) [ 9 >= a ]
		(?, 1)     f9(a, c) -> f10(a, c) [ c >= 1 ]
		(?, 1)     f9(a, c) -> f10(a, c) [ 0 >= c + 1 ]
		(1, 1)     f0(a, c) -> f9(0, h)
	start location:	f0
	leaf cost:	2

Repeatedly propagating knowledge in problem 8 produces the following problem:
9:	T:
		(1, 1)     f9(a, c) -> f16(0, 0) [ c = 0 ]
		(1, 1)     f10(a, c) -> f16(0, c) [ a >= 10 ]
		(10, 1)    f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ h >= 1 ]
		(10, 1)    f16(a, c) -> f16(a + 1, c) [ 9 >= a /\ 0 >= h + 1 ]
		(20, 1)    f10(a, c) -> f9(a + 1, h) [ 9 >= a ]
		(21, 1)    f9(a, c) -> f10(a, c) [ c >= 1 ]
		(21, 1)    f9(a, c) -> f10(a, c) [ 0 >= c + 1 ]
		(1, 1)     f0(a, c) -> f9(0, h)
	start location:	f0
	leaf cost:	2

Complexity upper bound 87

Time: 0.308 sec (SMT: 0.292 sec)