YES(?, 90*b + 5)

Initial complexity problem:
1:	T:
		(1, 1)    evalfstart(a, b, c) -> evalfentryin(a, b, c)
		(?, 1)    evalfentryin(a, b, c) -> evalfbb5in(0, b, c)
		(?, 1)    evalfbb5in(a, b, c) -> evalfreturnin(a, b, c) [ a >= b ]
		(?, 1)    evalfbb5in(a, b, c) -> evalfbb6in(a, b, c) [ b >= a + 1 ]
		(?, 1)    evalfbb6in(a, b, c) -> evalfbb2in(a, b, a) [ 0 >= d + 1 ]
		(?, 1)    evalfbb6in(a, b, c) -> evalfbb2in(a, b, a) [ d >= 1 ]
		(?, 1)    evalfbb6in(a, b, c) -> evalfreturnin(a, b, c)
		(?, 1)    evalfbb2in(a, b, c) -> evalfbb4in(a, b, c) [ c >= b ]
		(?, 1)    evalfbb2in(a, b, c) -> evalfbb3in(a, b, c) [ b >= c + 1 ]
		(?, 1)    evalfbb3in(a, b, c) -> evalfbb1in(a, b, c) [ 0 >= d + 1 ]
		(?, 1)    evalfbb3in(a, b, c) -> evalfbb1in(a, b, c) [ d >= 1 ]
		(?, 1)    evalfbb3in(a, b, c) -> evalfbb4in(a, b, c)
		(?, 1)    evalfbb1in(a, b, c) -> evalfbb2in(a, b, c + 1)
		(?, 1)    evalfbb4in(a, b, c) -> evalfbb5in(c + 1, b, c)
		(?, 1)    evalfreturnin(a, b, c) -> evalfstop(a, b, c)
	start location:	evalfstart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalfstart(a, b, c) -> evalfentryin(a, b, c)
		(?, 1)    evalfentryin(a, b, c) -> evalfbb5in(0, b, c)
		(?, 1)    evalfbb5in(a, b, c) -> evalfbb6in(a, b, c) [ b >= a + 1 ]
		(?, 1)    evalfbb6in(a, b, c) -> evalfbb2in(a, b, a) [ 0 >= d + 1 ]
		(?, 1)    evalfbb6in(a, b, c) -> evalfbb2in(a, b, a) [ d >= 1 ]
		(?, 1)    evalfbb2in(a, b, c) -> evalfbb4in(a, b, c) [ c >= b ]
		(?, 1)    evalfbb2in(a, b, c) -> evalfbb3in(a, b, c) [ b >= c + 1 ]
		(?, 1)    evalfbb3in(a, b, c) -> evalfbb1in(a, b, c) [ 0 >= d + 1 ]
		(?, 1)    evalfbb3in(a, b, c) -> evalfbb1in(a, b, c) [ d >= 1 ]
		(?, 1)    evalfbb3in(a, b, c) -> evalfbb4in(a, b, c)
		(?, 1)    evalfbb1in(a, b, c) -> evalfbb2in(a, b, c + 1)
		(?, 1)    evalfbb4in(a, b, c) -> evalfbb5in(c + 1, b, c)
	start location:	evalfstart
	leaf cost:	3

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalfstart(a, b, c) -> evalfentryin(a, b, c)
		(1, 1)    evalfentryin(a, b, c) -> evalfbb5in(0, b, c)
		(?, 1)    evalfbb5in(a, b, c) -> evalfbb6in(a, b, c) [ b >= a + 1 ]
		(?, 1)    evalfbb6in(a, b, c) -> evalfbb2in(a, b, a) [ 0 >= d + 1 ]
		(?, 1)    evalfbb6in(a, b, c) -> evalfbb2in(a, b, a) [ d >= 1 ]
		(?, 1)    evalfbb2in(a, b, c) -> evalfbb4in(a, b, c) [ c >= b ]
		(?, 1)    evalfbb2in(a, b, c) -> evalfbb3in(a, b, c) [ b >= c + 1 ]
		(?, 1)    evalfbb3in(a, b, c) -> evalfbb1in(a, b, c) [ 0 >= d + 1 ]
		(?, 1)    evalfbb3in(a, b, c) -> evalfbb1in(a, b, c) [ d >= 1 ]
		(?, 1)    evalfbb3in(a, b, c) -> evalfbb4in(a, b, c)
		(?, 1)    evalfbb1in(a, b, c) -> evalfbb2in(a, b, c + 1)
		(?, 1)    evalfbb4in(a, b, c) -> evalfbb5in(c + 1, b, c)
	start location:	evalfstart
	leaf cost:	3

A polynomial rank function with
	Pol(evalfstart) = 5*V_2
	Pol(evalfentryin) = 5*V_2
	Pol(evalfbb5in) = -5*V_1 + 5*V_2
	Pol(evalfbb6in) = -5*V_1 + 5*V_2 - 1
	Pol(evalfbb2in) = 5*V_2 - 5*V_3 - 2
	Pol(evalfbb4in) = 5*V_2 - 5*V_3 - 4
	Pol(evalfbb3in) = 5*V_2 - 5*V_3 - 3
	Pol(evalfbb1in) = 5*V_2 - 5*V_3 - 4
orients all transitions weakly and the transitions
	evalfbb5in(a, b, c) -> evalfbb6in(a, b, c) [ b >= a + 1 ]
	evalfbb2in(a, b, c) -> evalfbb3in(a, b, c) [ b >= c + 1 ]
strictly and produces the following problem:
4:	T:
		(1, 1)      evalfstart(a, b, c) -> evalfentryin(a, b, c)
		(1, 1)      evalfentryin(a, b, c) -> evalfbb5in(0, b, c)
		(5*b, 1)    evalfbb5in(a, b, c) -> evalfbb6in(a, b, c) [ b >= a + 1 ]
		(?, 1)      evalfbb6in(a, b, c) -> evalfbb2in(a, b, a) [ 0 >= d + 1 ]
		(?, 1)      evalfbb6in(a, b, c) -> evalfbb2in(a, b, a) [ d >= 1 ]
		(?, 1)      evalfbb2in(a, b, c) -> evalfbb4in(a, b, c) [ c >= b ]
		(5*b, 1)    evalfbb2in(a, b, c) -> evalfbb3in(a, b, c) [ b >= c + 1 ]
		(?, 1)      evalfbb3in(a, b, c) -> evalfbb1in(a, b, c) [ 0 >= d + 1 ]
		(?, 1)      evalfbb3in(a, b, c) -> evalfbb1in(a, b, c) [ d >= 1 ]
		(?, 1)      evalfbb3in(a, b, c) -> evalfbb4in(a, b, c)
		(?, 1)      evalfbb1in(a, b, c) -> evalfbb2in(a, b, c + 1)
		(?, 1)      evalfbb4in(a, b, c) -> evalfbb5in(c + 1, b, c)
	start location:	evalfstart
	leaf cost:	3

Repeatedly propagating knowledge in problem 4 produces the following problem:
5:	T:
		(1, 1)       evalfstart(a, b, c) -> evalfentryin(a, b, c)
		(1, 1)       evalfentryin(a, b, c) -> evalfbb5in(0, b, c)
		(5*b, 1)     evalfbb5in(a, b, c) -> evalfbb6in(a, b, c) [ b >= a + 1 ]
		(5*b, 1)     evalfbb6in(a, b, c) -> evalfbb2in(a, b, a) [ 0 >= d + 1 ]
		(5*b, 1)     evalfbb6in(a, b, c) -> evalfbb2in(a, b, a) [ d >= 1 ]
		(20*b, 1)    evalfbb2in(a, b, c) -> evalfbb4in(a, b, c) [ c >= b ]
		(5*b, 1)     evalfbb2in(a, b, c) -> evalfbb3in(a, b, c) [ b >= c + 1 ]
		(5*b, 1)     evalfbb3in(a, b, c) -> evalfbb1in(a, b, c) [ 0 >= d + 1 ]
		(5*b, 1)     evalfbb3in(a, b, c) -> evalfbb1in(a, b, c) [ d >= 1 ]
		(5*b, 1)     evalfbb3in(a, b, c) -> evalfbb4in(a, b, c)
		(10*b, 1)    evalfbb1in(a, b, c) -> evalfbb2in(a, b, c + 1)
		(25*b, 1)    evalfbb4in(a, b, c) -> evalfbb5in(c + 1, b, c)
	start location:	evalfstart
	leaf cost:	3

Complexity upper bound 90*b + 5

Time: 3.908 sec (SMT: 3.548 sec)