YES(?, a + b + c + 102)

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

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

Complexity upper bound a + b + c + 102

Time: 0.087 sec (SMT: 0.083 sec)