YES(?, 6*c + 602)

Initial complexity problem:
1:	T:
		(1, 1)    evalfstart(a, b, c) -> evalfentryin(a, b, c)
		(?, 1)    evalfentryin(a, b, c) -> evalfbb3in(0, 0, c)
		(?, 1)    evalfbb3in(a, b, c) -> evalfbbin(a, b, c) [ 99 >= b ]
		(?, 1)    evalfbb3in(a, b, c) -> evalfreturnin(a, b, c) [ b >= 100 ]
		(?, 1)    evalfbbin(a, b, c) -> evalfbb1in(a, b, c) [ c >= a + 1 ]
		(?, 1)    evalfbbin(a, b, c) -> evalfbb2in(a, b, c) [ a >= c ]
		(?, 1)    evalfbb1in(a, b, c) -> evalfbb3in(a + 1, b, c)
		(?, 1)    evalfbb2in(a, b, c) -> evalfbb3in(a, b + 1, 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) -> evalfbb3in(0, 0, c)
		(?, 1)    evalfbb3in(a, b, c) -> evalfbbin(a, b, c) [ 99 >= b ]
		(?, 1)    evalfbbin(a, b, c) -> evalfbb1in(a, b, c) [ c >= a + 1 ]
		(?, 1)    evalfbbin(a, b, c) -> evalfbb2in(a, b, c) [ a >= c ]
		(?, 1)    evalfbb1in(a, b, c) -> evalfbb3in(a + 1, b, c)
		(?, 1)    evalfbb2in(a, b, c) -> evalfbb3in(a, b + 1, c)
	start location:	evalfstart
	leaf cost:	2

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) -> evalfbb3in(0, 0, c)
		(?, 1)    evalfbb3in(a, b, c) -> evalfbbin(a, b, c) [ 99 >= b ]
		(?, 1)    evalfbbin(a, b, c) -> evalfbb1in(a, b, c) [ c >= a + 1 ]
		(?, 1)    evalfbbin(a, b, c) -> evalfbb2in(a, b, c) [ a >= c ]
		(?, 1)    evalfbb1in(a, b, c) -> evalfbb3in(a + 1, b, c)
		(?, 1)    evalfbb2in(a, b, c) -> evalfbb3in(a, b + 1, c)
	start location:	evalfstart
	leaf cost:	2

A polynomial rank function with
	Pol(evalfstart) = 2*V_3
	Pol(evalfentryin) = 2*V_3
	Pol(evalfbb3in) = -2*V_1 + 2*V_3
	Pol(evalfbbin) = -2*V_1 + 2*V_3
	Pol(evalfbb1in) = -2*V_1 + 2*V_3 - 1
	Pol(evalfbb2in) = -2*V_1 + 2*V_3
orients all transitions weakly and the transition
	evalfbbin(a, b, c) -> evalfbb1in(a, b, c) [ c >= a + 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) -> evalfbb3in(0, 0, c)
		(?, 1)      evalfbb3in(a, b, c) -> evalfbbin(a, b, c) [ 99 >= b ]
		(2*c, 1)    evalfbbin(a, b, c) -> evalfbb1in(a, b, c) [ c >= a + 1 ]
		(?, 1)      evalfbbin(a, b, c) -> evalfbb2in(a, b, c) [ a >= c ]
		(?, 1)      evalfbb1in(a, b, c) -> evalfbb3in(a + 1, b, c)
		(?, 1)      evalfbb2in(a, b, c) -> evalfbb3in(a, b + 1, c)
	start location:	evalfstart
	leaf cost:	2

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) -> evalfbb3in(0, 0, c)
		(?, 1)      evalfbb3in(a, b, c) -> evalfbbin(a, b, c) [ 99 >= b ]
		(2*c, 1)    evalfbbin(a, b, c) -> evalfbb1in(a, b, c) [ c >= a + 1 ]
		(?, 1)      evalfbbin(a, b, c) -> evalfbb2in(a, b, c) [ a >= c ]
		(2*c, 1)    evalfbb1in(a, b, c) -> evalfbb3in(a + 1, b, c)
		(?, 1)      evalfbb2in(a, b, c) -> evalfbb3in(a, b + 1, c)
	start location:	evalfstart
	leaf cost:	2

Applied AI with 'oct' on problem 5 to obtain the following invariants:
  For symbol evalfbb1in: X_3 - 1 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ -X_2 + X_3 + 98 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ -X_1 + X_3 - 1 >= 0 /\ -X_2 + 99 >= 0 /\ X_1 - X_2 + 99 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol evalfbb2in: X_1 - X_3 >= 0 /\ -X_2 + 99 >= 0 /\ X_1 - X_2 + 99 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol evalfbb3in: X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol evalfbbin: -X_2 + 99 >= 0 /\ X_1 - X_2 + 99 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0


This yielded the following problem:
6:	T:
		(?, 1)      evalfbb2in(a, b, c) -> evalfbb3in(a, b + 1, c) [ a - c >= 0 /\ -b + 99 >= 0 /\ a - b + 99 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(2*c, 1)    evalfbb1in(a, b, c) -> evalfbb3in(a + 1, b, c) [ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c + 98 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ -b + 99 >= 0 /\ a - b + 99 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(?, 1)      evalfbbin(a, b, c) -> evalfbb2in(a, b, c) [ -b + 99 >= 0 /\ a - b + 99 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= c ]
		(2*c, 1)    evalfbbin(a, b, c) -> evalfbb1in(a, b, c) [ -b + 99 >= 0 /\ a - b + 99 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= a + 1 ]
		(?, 1)      evalfbb3in(a, b, c) -> evalfbbin(a, b, c) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 99 >= b ]
		(1, 1)      evalfentryin(a, b, c) -> evalfbb3in(0, 0, c)
		(1, 1)      evalfstart(a, b, c) -> evalfentryin(a, b, c)
	start location:	evalfstart
	leaf cost:	2

A polynomial rank function with
	Pol(evalfbb2in) = -2*V_2 + 198
	Pol(evalfbb3in) = -2*V_2 + 199
	Pol(evalfbb1in) = -2*V_2 + 199
	Pol(evalfbbin) = -2*V_2 + 199
	Pol(evalfentryin) = 199
	Pol(evalfstart) = 199
orients all transitions weakly and the transition
	evalfbbin(a, b, c) -> evalfbb2in(a, b, c) [ -b + 99 >= 0 /\ a - b + 99 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= c ]
strictly and produces the following problem:
7:	T:
		(?, 1)      evalfbb2in(a, b, c) -> evalfbb3in(a, b + 1, c) [ a - c >= 0 /\ -b + 99 >= 0 /\ a - b + 99 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(2*c, 1)    evalfbb1in(a, b, c) -> evalfbb3in(a + 1, b, c) [ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c + 98 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ -b + 99 >= 0 /\ a - b + 99 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(199, 1)    evalfbbin(a, b, c) -> evalfbb2in(a, b, c) [ -b + 99 >= 0 /\ a - b + 99 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= c ]
		(2*c, 1)    evalfbbin(a, b, c) -> evalfbb1in(a, b, c) [ -b + 99 >= 0 /\ a - b + 99 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= a + 1 ]
		(?, 1)      evalfbb3in(a, b, c) -> evalfbbin(a, b, c) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 99 >= b ]
		(1, 1)      evalfentryin(a, b, c) -> evalfbb3in(0, 0, c)
		(1, 1)      evalfstart(a, b, c) -> evalfentryin(a, b, c)
	start location:	evalfstart
	leaf cost:	2

Repeatedly propagating knowledge in problem 7 produces the following problem:
8:	T:
		(199, 1)          evalfbb2in(a, b, c) -> evalfbb3in(a, b + 1, c) [ a - c >= 0 /\ -b + 99 >= 0 /\ a - b + 99 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(2*c, 1)          evalfbb1in(a, b, c) -> evalfbb3in(a + 1, b, c) [ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c + 98 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ -b + 99 >= 0 /\ a - b + 99 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(199, 1)          evalfbbin(a, b, c) -> evalfbb2in(a, b, c) [ -b + 99 >= 0 /\ a - b + 99 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= c ]
		(2*c, 1)          evalfbbin(a, b, c) -> evalfbb1in(a, b, c) [ -b + 99 >= 0 /\ a - b + 99 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= a + 1 ]
		(2*c + 200, 1)    evalfbb3in(a, b, c) -> evalfbbin(a, b, c) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 99 >= b ]
		(1, 1)            evalfentryin(a, b, c) -> evalfbb3in(0, 0, c)
		(1, 1)            evalfstart(a, b, c) -> evalfentryin(a, b, c)
	start location:	evalfstart
	leaf cost:	2

Complexity upper bound 6*c + 602

Time: 0.500 sec (SMT: 0.474 sec)