YES(?, 94)

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, t) -> f6(0, 0, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t)
		(?, 1)    f6(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) -> f6(u, b + 1, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) [ 63 >= b ]
		(?, 1)    f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) -> f14(a, b, c - 1, u + v, w, x + y, z, a1 + b1, c1, d1 + e1, f1, u + v + d1 + e1, u + v - d1 - e1, x + y + a1 + b1, x + y - a1 - b1, g1, h1, i1 + j1, k1 + j1, j1) [ c >= 0 ]
		(?, 1)    f57(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) -> f57(a, b, c - 1, u + v, w, x + y, z, a1 + b1, c1, d1 + e1, f1, u + v + d1 + e1, u + v - d1 - e1, x + y + a1 + b1, x + y - a1 - b1, g1, h1, i1 + j1, k1 + j1, j1) [ c >= 0 ]
		(?, 1)    f57(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) -> f101(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) [ 0 >= c + 1 ]
		(?, 1)    f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) -> f57(a, b, 7, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) [ 0 >= c + 1 ]
		(?, 1)    f6(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) -> f14(a, b, 7, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) [ b >= 64 ]
	start location:	f0
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [b, c].
We thus obtain the following problem:
2:	T:
		(?, 1)    f6(b, c) -> f14(b, 7) [ b >= 64 ]
		(?, 1)    f14(b, c) -> f57(b, 7) [ 0 >= c + 1 ]
		(?, 1)    f57(b, c) -> f101(b, c) [ 0 >= c + 1 ]
		(?, 1)    f57(b, c) -> f57(b, c - 1) [ c >= 0 ]
		(?, 1)    f14(b, c) -> f14(b, c - 1) [ c >= 0 ]
		(?, 1)    f6(b, c) -> f6(b + 1, c) [ 63 >= b ]
		(1, 1)    f0(b, c) -> f6(0, c)
	start location:	f0
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(?, 1)    f6(b, c) -> f14(b, 7) [ b >= 64 ]
		(?, 1)    f14(b, c) -> f57(b, 7) [ 0 >= c + 1 ]
		(?, 1)    f57(b, c) -> f57(b, c - 1) [ c >= 0 ]
		(?, 1)    f14(b, c) -> f14(b, c - 1) [ c >= 0 ]
		(?, 1)    f6(b, c) -> f6(b + 1, c) [ 63 >= b ]
		(1, 1)    f0(b, c) -> f6(0, c)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f6) = 2
	Pol(f14) = 1
	Pol(f57) = 0
	Pol(f0) = 2
orients all transitions weakly and the transitions
	f6(b, c) -> f14(b, 7) [ b >= 64 ]
	f14(b, c) -> f57(b, 7) [ 0 >= c + 1 ]
strictly and produces the following problem:
4:	T:
		(2, 1)    f6(b, c) -> f14(b, 7) [ b >= 64 ]
		(2, 1)    f14(b, c) -> f57(b, 7) [ 0 >= c + 1 ]
		(?, 1)    f57(b, c) -> f57(b, c - 1) [ c >= 0 ]
		(?, 1)    f14(b, c) -> f14(b, c - 1) [ c >= 0 ]
		(?, 1)    f6(b, c) -> f6(b + 1, c) [ 63 >= b ]
		(1, 1)    f0(b, c) -> f6(0, c)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f6) = -V_1 + 64
	Pol(f14) = -V_1
	Pol(f57) = -V_1 + V_2 - 7
	Pol(f0) = 64
orients all transitions weakly and the transition
	f6(b, c) -> f6(b + 1, c) [ 63 >= b ]
strictly and produces the following problem:
5:	T:
		(2, 1)     f6(b, c) -> f14(b, 7) [ b >= 64 ]
		(2, 1)     f14(b, c) -> f57(b, 7) [ 0 >= c + 1 ]
		(?, 1)     f57(b, c) -> f57(b, c - 1) [ c >= 0 ]
		(?, 1)     f14(b, c) -> f14(b, c - 1) [ c >= 0 ]
		(64, 1)    f6(b, c) -> f6(b + 1, c) [ 63 >= b ]
		(1, 1)     f0(b, c) -> f6(0, c)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f6) = 8
	Pol(f14) = 8
	Pol(f57) = V_2 + 1
	Pol(f0) = 8
orients all transitions weakly and the transition
	f57(b, c) -> f57(b, c - 1) [ c >= 0 ]
strictly and produces the following problem:
6:	T:
		(2, 1)     f6(b, c) -> f14(b, 7) [ b >= 64 ]
		(2, 1)     f14(b, c) -> f57(b, 7) [ 0 >= c + 1 ]
		(8, 1)     f57(b, c) -> f57(b, c - 1) [ c >= 0 ]
		(?, 1)     f14(b, c) -> f14(b, c - 1) [ c >= 0 ]
		(64, 1)    f6(b, c) -> f6(b + 1, c) [ 63 >= b ]
		(1, 1)     f0(b, c) -> f6(0, c)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f14) = V_2 + 1
and size complexities
	S("f0(b, c) -> f6(0, c)", 0-0) = 0
	S("f0(b, c) -> f6(0, c)", 0-1) = c
	S("f6(b, c) -> f6(b + 1, c) [ 63 >= b ]", 0-0) = 64
	S("f6(b, c) -> f6(b + 1, c) [ 63 >= b ]", 0-1) = c
	S("f14(b, c) -> f14(b, c - 1) [ c >= 0 ]", 0-0) = 64
	S("f14(b, c) -> f14(b, c - 1) [ c >= 0 ]", 0-1) = 7
	S("f57(b, c) -> f57(b, c - 1) [ c >= 0 ]", 0-0) = 64
	S("f57(b, c) -> f57(b, c - 1) [ c >= 0 ]", 0-1) = 7
	S("f14(b, c) -> f57(b, 7) [ 0 >= c + 1 ]", 0-0) = 64
	S("f14(b, c) -> f57(b, 7) [ 0 >= c + 1 ]", 0-1) = 7
	S("f6(b, c) -> f14(b, 7) [ b >= 64 ]", 0-0) = 64
	S("f6(b, c) -> f14(b, 7) [ b >= 64 ]", 0-1) = 7
orients the transition
	f14(b, c) -> f14(b, c - 1) [ c >= 0 ]
weakly and the transition
	f14(b, c) -> f14(b, c - 1) [ c >= 0 ]
strictly and produces the following problem:
7:	T:
		(2, 1)     f6(b, c) -> f14(b, 7) [ b >= 64 ]
		(2, 1)     f14(b, c) -> f57(b, 7) [ 0 >= c + 1 ]
		(8, 1)     f57(b, c) -> f57(b, c - 1) [ c >= 0 ]
		(16, 1)    f14(b, c) -> f14(b, c - 1) [ c >= 0 ]
		(64, 1)    f6(b, c) -> f6(b + 1, c) [ 63 >= b ]
		(1, 1)     f0(b, c) -> f6(0, c)
	start location:	f0
	leaf cost:	1

Complexity upper bound 94

Time: 0.264 sec (SMT: 0.252 sec)