YES(?, 1030)

Initial complexity problem:
1:	T:
		(1, 1)    f0(a, b, c, d, e) -> f7(f, 0, 0, d, e) [ 0 >= f + 1 ]
		(1, 1)    f0(a, b, c, d, e) -> f7(f, 0, 0, d, e) [ f >= 1 ]
		(1, 1)    f0(a, b, c, d, e) -> f7(0, 1023, 0, d, e)
		(?, 1)    f7(a, b, c, d, e) -> f7(a, b, c + 1, d + 2, e) [ b >= c ]
		(?, 1)    f7(a, b, c, d, e) -> f21(a, b, c, d, e) [ e >= 0 /\ c >= b + 1 /\ 1022 >= e ]
		(?, 1)    f7(a, b, c, d, e) -> f21(a, b, c, d, e) [ c >= b + 1 /\ e >= 1023 ]
		(?, 1)    f7(a, b, c, d, e) -> f21(a, b, c, d, e) [ c >= b + 1 /\ 0 >= e + 1 ]
	start location:	f0
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    f0(a, b, c, d, e) -> f7(f, 0, 0, d, e) [ 0 >= f + 1 ]
		(1, 1)    f0(a, b, c, d, e) -> f7(f, 0, 0, d, e) [ f >= 1 ]
		(1, 1)    f0(a, b, c, d, e) -> f7(0, 1023, 0, d, e)
		(?, 1)    f7(a, b, c, d, e) -> f7(a, b, c + 1, d + 2, e) [ b >= c ]
	start location:	f0
	leaf cost:	3

A polynomial rank function with
	Pol(f0) = 1024
	Pol(f7) = V_2 - V_3 + 1
orients all transitions weakly and the transition
	f7(a, b, c, d, e) -> f7(a, b, c + 1, d + 2, e) [ b >= c ]
strictly and produces the following problem:
3:	T:
		(1, 1)       f0(a, b, c, d, e) -> f7(f, 0, 0, d, e) [ 0 >= f + 1 ]
		(1, 1)       f0(a, b, c, d, e) -> f7(f, 0, 0, d, e) [ f >= 1 ]
		(1, 1)       f0(a, b, c, d, e) -> f7(0, 1023, 0, d, e)
		(1024, 1)    f7(a, b, c, d, e) -> f7(a, b, c + 1, d + 2, e) [ b >= c ]
	start location:	f0
	leaf cost:	3

Complexity upper bound 1030

Time: 0.163 sec (SMT: 0.153 sec)