YES(?, 12*a + 13)

Initial complexity problem:
1:	T:
		(1, 1)    evalrandom1dstart(a, b) -> evalrandom1dentryin(a, b)
		(?, 1)    evalrandom1dentryin(a, b) -> evalrandom1dbb5in(a, 1) [ a >= 1 ]
		(?, 1)    evalrandom1dentryin(a, b) -> evalrandom1dreturnin(a, b) [ 0 >= a ]
		(?, 1)    evalrandom1dbb5in(a, b) -> evalrandom1dbb1in(a, b) [ a >= b ]
		(?, 1)    evalrandom1dbb5in(a, b) -> evalrandom1dreturnin(a, b) [ b >= a + 1 ]
		(?, 1)    evalrandom1dbb1in(a, b) -> evalrandom1dbb5in(a, b + 1) [ 0 >= c + 1 ]
		(?, 1)    evalrandom1dbb1in(a, b) -> evalrandom1dbb5in(a, b + 1) [ c >= 1 ]
		(?, 1)    evalrandom1dbb1in(a, b) -> evalrandom1dbb5in(a, b + 1)
		(?, 1)    evalrandom1dreturnin(a, b) -> evalrandom1dstop(a, b)
	start location:	evalrandom1dstart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalrandom1dstart(a, b) -> evalrandom1dentryin(a, b)
		(?, 1)    evalrandom1dentryin(a, b) -> evalrandom1dbb5in(a, 1) [ a >= 1 ]
		(?, 1)    evalrandom1dbb5in(a, b) -> evalrandom1dbb1in(a, b) [ a >= b ]
		(?, 1)    evalrandom1dbb1in(a, b) -> evalrandom1dbb5in(a, b + 1) [ 0 >= c + 1 ]
		(?, 1)    evalrandom1dbb1in(a, b) -> evalrandom1dbb5in(a, b + 1) [ c >= 1 ]
		(?, 1)    evalrandom1dbb1in(a, b) -> evalrandom1dbb5in(a, b + 1)
	start location:	evalrandom1dstart
	leaf cost:	3

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalrandom1dstart(a, b) -> evalrandom1dentryin(a, b)
		(1, 1)    evalrandom1dentryin(a, b) -> evalrandom1dbb5in(a, 1) [ a >= 1 ]
		(?, 1)    evalrandom1dbb5in(a, b) -> evalrandom1dbb1in(a, b) [ a >= b ]
		(?, 1)    evalrandom1dbb1in(a, b) -> evalrandom1dbb5in(a, b + 1) [ 0 >= c + 1 ]
		(?, 1)    evalrandom1dbb1in(a, b) -> evalrandom1dbb5in(a, b + 1) [ c >= 1 ]
		(?, 1)    evalrandom1dbb1in(a, b) -> evalrandom1dbb5in(a, b + 1)
	start location:	evalrandom1dstart
	leaf cost:	3

A polynomial rank function with
	Pol(evalrandom1dstart) = 3*V_1 - 2
	Pol(evalrandom1dentryin) = 3*V_1 - 2
	Pol(evalrandom1dbb5in) = 3*V_1 - 3*V_2 + 1
	Pol(evalrandom1dbb1in) = 3*V_1 - 3*V_2 - 1
orients all transitions weakly and the transition
	evalrandom1dbb5in(a, b) -> evalrandom1dbb1in(a, b) [ a >= b ]
strictly and produces the following problem:
4:	T:
		(1, 1)          evalrandom1dstart(a, b) -> evalrandom1dentryin(a, b)
		(1, 1)          evalrandom1dentryin(a, b) -> evalrandom1dbb5in(a, 1) [ a >= 1 ]
		(3*a + 2, 1)    evalrandom1dbb5in(a, b) -> evalrandom1dbb1in(a, b) [ a >= b ]
		(?, 1)          evalrandom1dbb1in(a, b) -> evalrandom1dbb5in(a, b + 1) [ 0 >= c + 1 ]
		(?, 1)          evalrandom1dbb1in(a, b) -> evalrandom1dbb5in(a, b + 1) [ c >= 1 ]
		(?, 1)          evalrandom1dbb1in(a, b) -> evalrandom1dbb5in(a, b + 1)
	start location:	evalrandom1dstart
	leaf cost:	3

Repeatedly propagating knowledge in problem 4 produces the following problem:
5:	T:
		(1, 1)          evalrandom1dstart(a, b) -> evalrandom1dentryin(a, b)
		(1, 1)          evalrandom1dentryin(a, b) -> evalrandom1dbb5in(a, 1) [ a >= 1 ]
		(3*a + 2, 1)    evalrandom1dbb5in(a, b) -> evalrandom1dbb1in(a, b) [ a >= b ]
		(3*a + 2, 1)    evalrandom1dbb1in(a, b) -> evalrandom1dbb5in(a, b + 1) [ 0 >= c + 1 ]
		(3*a + 2, 1)    evalrandom1dbb1in(a, b) -> evalrandom1dbb5in(a, b + 1) [ c >= 1 ]
		(3*a + 2, 1)    evalrandom1dbb1in(a, b) -> evalrandom1dbb5in(a, b + 1)
	start location:	evalrandom1dstart
	leaf cost:	3

Complexity upper bound 12*a + 13

Time: 0.144 sec (SMT: 0.136 sec)