YES(?, a + b + 2)

Initial complexity problem:
1:	T:
		(1, 1)    eval0(a, b, c) -> eval1(a, b, c) [ a >= 1 ]
		(?, 1)    eval1(a, b, c) -> eval1(a, b + a, c) [ a >= b + 1 /\ c >= a + 1 /\ a >= 1 ]
		(?, 1)    eval1(a, b, c) -> eval1(a, b, b - a) [ a >= b + 1 /\ c >= a + 1 /\ a >= 1 ]
	start location:	eval0
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    eval0(a, b, c) -> eval1(a, b, c) [ a >= 1 ]
		(?, 1)    eval1(a, b, c) -> eval1(a, b + a, c) [ a >= b + 1 /\ c >= a + 1 /\ a >= 1 ]
	start location:	eval0
	leaf cost:	1

A polynomial rank function with
	Pol(eval0) = V_1 - V_2
	Pol(eval1) = V_1 - V_2
orients all transitions weakly and the transition
	eval1(a, b, c) -> eval1(a, b + a, c) [ a >= b + 1 /\ c >= a + 1 /\ a >= 1 ]
strictly and produces the following problem:
3:	T:
		(1, 1)        eval0(a, b, c) -> eval1(a, b, c) [ a >= 1 ]
		(a + b, 1)    eval1(a, b, c) -> eval1(a, b + a, c) [ a >= b + 1 /\ c >= a + 1 /\ a >= 1 ]
	start location:	eval0
	leaf cost:	1

Complexity upper bound a + b + 2

Time: 0.122 sec (SMT: 0.117 sec)