YES(?, 1413880)

Initial complexity problem:
1:	T:
		(1, 1)    f0(a, b, c, d, e, f, g) -> f8(-1, -1, 1, d, e, f, g)
		(?, 1)    f8(a, b, c, d, e, f, g) -> f8(a, b, c + 1, d, e, f, g) [ 100 >= c ]
		(?, 1)    f18(a, b, c, d, e, f, g) -> f22(a, b, c, d, 1, 1, g) [ 99 >= d ]
		(?, 1)    f22(a, b, c, d, e, f, g) -> f33(a, b, c, d, e, f, g) [ f >= 100 ]
		(?, 1)    f22(a, b, c, d, e, f, g) -> f33(a, b, c, d, e, f, g) [ 99 >= f /\ f + d >= 101 ]
		(?, 1)    f22(a, b, c, d, e, f, g) -> f22(a, b, c, d, e, f + 1, g) [ 99 >= f /\ 100 >= d + f ]
		(?, 1)    f22(a, b, c, d, e, f, g) -> f22(a, b, c, d, 0, f + 1, h) [ 99 >= f /\ 100 >= d + f ]
		(?, 1)    f33(a, b, c, d, e, f, g) -> f18(a, b, c, d + 1, 0, f, g) [ e = 0 ]
		(?, 1)    f18(a, b, c, d, e, f, g) -> f40(a, b, c, d, e, f, g) [ d >= 100 ]
		(?, 1)    f33(a, b, c, d, e, f, g) -> f40(a, b, c, d, e, f, g) [ 0 >= e + 1 ]
		(?, 1)    f33(a, b, c, d, e, f, g) -> f40(a, b, c, d, e, f, g) [ e >= 1 ]
		(?, 1)    f8(a, b, c, d, e, f, g) -> f18(a, b, c, 1, 0, f, g) [ c >= 101 ]
	start location:	f0
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [c, d, e, f].
We thus obtain the following problem:
2:	T:
		(?, 1)    f8(c, d, e, f) -> f18(c, 1, 0, f) [ c >= 101 ]
		(?, 1)    f33(c, d, e, f) -> f40(c, d, e, f) [ e >= 1 ]
		(?, 1)    f33(c, d, e, f) -> f40(c, d, e, f) [ 0 >= e + 1 ]
		(?, 1)    f18(c, d, e, f) -> f40(c, d, e, f) [ d >= 100 ]
		(?, 1)    f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]
		(?, 1)    f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\ 100 >= d + f ]
		(?, 1)    f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\ 100 >= d + f ]
		(?, 1)    f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\ f + d >= 101 ]
		(?, 1)    f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]
		(?, 1)    f18(c, d, e, f) -> f22(c, d, 1, 1) [ 99 >= d ]
		(?, 1)    f8(c, d, e, f) -> f8(c + 1, d, e, f) [ 100 >= c ]
		(1, 1)    f0(c, d, e, f) -> f8(1, d, e, f)
	start location:	f0
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(?, 1)    f8(c, d, e, f) -> f18(c, 1, 0, f) [ c >= 101 ]
		(?, 1)    f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]
		(?, 1)    f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\ 100 >= d + f ]
		(?, 1)    f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\ 100 >= d + f ]
		(?, 1)    f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\ f + d >= 101 ]
		(?, 1)    f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]
		(?, 1)    f18(c, d, e, f) -> f22(c, d, 1, 1) [ 99 >= d ]
		(?, 1)    f8(c, d, e, f) -> f8(c + 1, d, e, f) [ 100 >= c ]
		(1, 1)    f0(c, d, e, f) -> f8(1, d, e, f)
	start location:	f0
	leaf cost:	3

A polynomial rank function with
	Pol(f8) = 100
	Pol(f18) = -100
	Pol(f33) = -100
	Pol(f22) = -100
	Pol(f0) = 100
orients all transitions weakly and the transition
	f8(c, d, e, f) -> f18(c, 1, 0, f) [ c >= 101 ]
strictly and produces the following problem:
4:	T:
		(100, 1)    f8(c, d, e, f) -> f18(c, 1, 0, f) [ c >= 101 ]
		(?, 1)      f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]
		(?, 1)      f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\ 100 >= d + f ]
		(?, 1)      f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\ 100 >= d + f ]
		(?, 1)      f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\ f + d >= 101 ]
		(?, 1)      f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]
		(?, 1)      f18(c, d, e, f) -> f22(c, d, 1, 1) [ 99 >= d ]
		(?, 1)      f8(c, d, e, f) -> f8(c + 1, d, e, f) [ 100 >= c ]
		(1, 1)      f0(c, d, e, f) -> f8(1, d, e, f)
	start location:	f0
	leaf cost:	3

A polynomial rank function with
	Pol(f8) = -V_1 + 101
	Pol(f18) = -V_1 - 3*V_2 + 2
	Pol(f33) = -V_1 - 3*V_2
	Pol(f22) = -V_1 - 3*V_2 + 1
	Pol(f0) = 100
orients all transitions weakly and the transition
	f8(c, d, e, f) -> f8(c + 1, d, e, f) [ 100 >= c ]
strictly and produces the following problem:
5:	T:
		(100, 1)    f8(c, d, e, f) -> f18(c, 1, 0, f) [ c >= 101 ]
		(?, 1)      f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]
		(?, 1)      f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\ 100 >= d + f ]
		(?, 1)      f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\ 100 >= d + f ]
		(?, 1)      f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\ f + d >= 101 ]
		(?, 1)      f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]
		(?, 1)      f18(c, d, e, f) -> f22(c, d, 1, 1) [ 99 >= d ]
		(100, 1)    f8(c, d, e, f) -> f8(c + 1, d, e, f) [ 100 >= c ]
		(1, 1)      f0(c, d, e, f) -> f8(1, d, e, f)
	start location:	f0
	leaf cost:	3

A polynomial rank function with
	Pol(f8) = 6764
	Pol(f18) = -69*V_2 + 6833
	Pol(f33) = -69*V_2 + 6765
	Pol(f22) = -69*V_2 + 6766
	Pol(f0) = 6764
orients all transitions weakly and the transition
	f18(c, d, e, f) -> f22(c, d, 1, 1) [ 99 >= d ]
strictly and produces the following problem:
6:	T:
		(100, 1)     f8(c, d, e, f) -> f18(c, 1, 0, f) [ c >= 101 ]
		(?, 1)       f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]
		(?, 1)       f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\ 100 >= d + f ]
		(?, 1)       f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\ 100 >= d + f ]
		(?, 1)       f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\ f + d >= 101 ]
		(?, 1)       f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]
		(6764, 1)    f18(c, d, e, f) -> f22(c, d, 1, 1) [ 99 >= d ]
		(100, 1)     f8(c, d, e, f) -> f8(c + 1, d, e, f) [ 100 >= c ]
		(1, 1)       f0(c, d, e, f) -> f8(1, d, e, f)
	start location:	f0
	leaf cost:	3

A polynomial rank function with
	Pol(f33) = 1
	Pol(f18) = 0
	Pol(f22) = 2
and size complexities
	S("f0(c, d, e, f) -> f8(1, d, e, f)", 0-0) = 1
	S("f0(c, d, e, f) -> f8(1, d, e, f)", 0-1) = d
	S("f0(c, d, e, f) -> f8(1, d, e, f)", 0-2) = e
	S("f0(c, d, e, f) -> f8(1, d, e, f)", 0-3) = f
	S("f8(c, d, e, f) -> f8(c + 1, d, e, f) [ 100 >= c ]", 0-0) = 101
	S("f8(c, d, e, f) -> f8(c + 1, d, e, f) [ 100 >= c ]", 0-1) = d
	S("f8(c, d, e, f) -> f8(c + 1, d, e, f) [ 100 >= c ]", 0-2) = e
	S("f8(c, d, e, f) -> f8(c + 1, d, e, f) [ 100 >= c ]", 0-3) = f
	S("f18(c, d, e, f) -> f22(c, d, 1, 1) [ 99 >= d ]", 0-0) = 101
	S("f18(c, d, e, f) -> f22(c, d, 1, 1) [ 99 >= d ]", 0-1) = ?
	S("f18(c, d, e, f) -> f22(c, d, 1, 1) [ 99 >= d ]", 0-2) = 1
	S("f18(c, d, e, f) -> f22(c, d, 1, 1) [ 99 >= d ]", 0-3) = 1
	S("f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]", 0-0) = 101
	S("f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]", 0-1) = ?
	S("f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]", 0-2) = 1
	S("f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]", 0-3) = 100
	S("f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\\ f + d >= 101 ]", 0-0) = 101
	S("f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\\ f + d >= 101 ]", 0-1) = ?
	S("f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\\ f + d >= 101 ]", 0-2) = 1
	S("f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\\ f + d >= 101 ]", 0-3) = 100
	S("f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\\ 100 >= d + f ]", 0-0) = 101
	S("f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\\ 100 >= d + f ]", 0-1) = ?
	S("f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\\ 100 >= d + f ]", 0-2) = 1
	S("f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\\ 100 >= d + f ]", 0-3) = 100
	S("f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\\ 100 >= d + f ]", 0-0) = 101
	S("f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\\ 100 >= d + f ]", 0-1) = ?
	S("f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\\ 100 >= d + f ]", 0-2) = 0
	S("f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\\ 100 >= d + f ]", 0-3) = 100
	S("f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]", 0-0) = 101
	S("f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]", 0-1) = ?
	S("f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]", 0-2) = 0
	S("f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]", 0-3) = 100
	S("f8(c, d, e, f) -> f18(c, 1, 0, f) [ c >= 101 ]", 0-0) = 101
	S("f8(c, d, e, f) -> f18(c, 1, 0, f) [ c >= 101 ]", 0-1) = 1
	S("f8(c, d, e, f) -> f18(c, 1, 0, f) [ c >= 101 ]", 0-2) = 0
	S("f8(c, d, e, f) -> f18(c, 1, 0, f) [ c >= 101 ]", 0-3) = f
orients the transitions
	f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]
	f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\ f + d >= 101 ]
	f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]
	f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\ 100 >= d + f ]
	f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\ 100 >= d + f ]
weakly and the transitions
	f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]
	f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\ f + d >= 101 ]
	f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]
strictly and produces the following problem:
7:	T:
		(100, 1)      f8(c, d, e, f) -> f18(c, 1, 0, f) [ c >= 101 ]
		(13528, 1)    f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]
		(?, 1)        f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\ 100 >= d + f ]
		(?, 1)        f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\ 100 >= d + f ]
		(13528, 1)    f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\ f + d >= 101 ]
		(13528, 1)    f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]
		(6764, 1)     f18(c, d, e, f) -> f22(c, d, 1, 1) [ 99 >= d ]
		(100, 1)      f8(c, d, e, f) -> f8(c + 1, d, e, f) [ 100 >= c ]
		(1, 1)        f0(c, d, e, f) -> f8(1, d, e, f)
	start location:	f0
	leaf cost:	3

A polynomial rank function with
	Pol(f22) = -V_4 + 100
and size complexities
	S("f0(c, d, e, f) -> f8(1, d, e, f)", 0-0) = 1
	S("f0(c, d, e, f) -> f8(1, d, e, f)", 0-1) = d
	S("f0(c, d, e, f) -> f8(1, d, e, f)", 0-2) = e
	S("f0(c, d, e, f) -> f8(1, d, e, f)", 0-3) = f
	S("f8(c, d, e, f) -> f8(c + 1, d, e, f) [ 100 >= c ]", 0-0) = 101
	S("f8(c, d, e, f) -> f8(c + 1, d, e, f) [ 100 >= c ]", 0-1) = d
	S("f8(c, d, e, f) -> f8(c + 1, d, e, f) [ 100 >= c ]", 0-2) = e
	S("f8(c, d, e, f) -> f8(c + 1, d, e, f) [ 100 >= c ]", 0-3) = f
	S("f18(c, d, e, f) -> f22(c, d, 1, 1) [ 99 >= d ]", 0-0) = 101
	S("f18(c, d, e, f) -> f22(c, d, 1, 1) [ 99 >= d ]", 0-1) = 13529
	S("f18(c, d, e, f) -> f22(c, d, 1, 1) [ 99 >= d ]", 0-2) = 1
	S("f18(c, d, e, f) -> f22(c, d, 1, 1) [ 99 >= d ]", 0-3) = 1
	S("f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]", 0-0) = 101
	S("f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]", 0-1) = 13529
	S("f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]", 0-2) = 1
	S("f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]", 0-3) = 100
	S("f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\\ f + d >= 101 ]", 0-0) = 101
	S("f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\\ f + d >= 101 ]", 0-1) = 13529
	S("f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\\ f + d >= 101 ]", 0-2) = 1
	S("f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\\ f + d >= 101 ]", 0-3) = 100
	S("f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\\ 100 >= d + f ]", 0-0) = 101
	S("f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\\ 100 >= d + f ]", 0-1) = 13529
	S("f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\\ 100 >= d + f ]", 0-2) = 1
	S("f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\\ 100 >= d + f ]", 0-3) = 100
	S("f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\\ 100 >= d + f ]", 0-0) = 101
	S("f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\\ 100 >= d + f ]", 0-1) = 13529
	S("f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\\ 100 >= d + f ]", 0-2) = 0
	S("f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\\ 100 >= d + f ]", 0-3) = 100
	S("f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]", 0-0) = 101
	S("f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]", 0-1) = 13529
	S("f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]", 0-2) = 0
	S("f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]", 0-3) = 100
	S("f8(c, d, e, f) -> f18(c, 1, 0, f) [ c >= 101 ]", 0-0) = 101
	S("f8(c, d, e, f) -> f18(c, 1, 0, f) [ c >= 101 ]", 0-1) = 1
	S("f8(c, d, e, f) -> f18(c, 1, 0, f) [ c >= 101 ]", 0-2) = 0
	S("f8(c, d, e, f) -> f18(c, 1, 0, f) [ c >= 101 ]", 0-3) = f
orients the transitions
	f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\ 100 >= d + f ]
	f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\ 100 >= d + f ]
weakly and the transitions
	f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\ 100 >= d + f ]
	f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\ 100 >= d + f ]
strictly and produces the following problem:
8:	T:
		(100, 1)       f8(c, d, e, f) -> f18(c, 1, 0, f) [ c >= 101 ]
		(13528, 1)     f33(c, d, e, f) -> f18(c, d + 1, 0, f) [ e = 0 ]
		(683164, 1)    f22(c, d, e, f) -> f22(c, d, 0, f + 1) [ 99 >= f /\ 100 >= d + f ]
		(683164, 1)    f22(c, d, e, f) -> f22(c, d, e, f + 1) [ 99 >= f /\ 100 >= d + f ]
		(13528, 1)     f22(c, d, e, f) -> f33(c, d, e, f) [ 99 >= f /\ f + d >= 101 ]
		(13528, 1)     f22(c, d, e, f) -> f33(c, d, e, f) [ f >= 100 ]
		(6764, 1)      f18(c, d, e, f) -> f22(c, d, 1, 1) [ 99 >= d ]
		(100, 1)       f8(c, d, e, f) -> f8(c + 1, d, e, f) [ 100 >= c ]
		(1, 1)         f0(c, d, e, f) -> f8(1, d, e, f)
	start location:	f0
	leaf cost:	3

Complexity upper bound 1413880

Time: 0.398 sec (SMT: 0.372 sec)