YES(?, 4*a + 2*a^2 + 1)

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

A polynomial rank function with
	Pol(eval1) = 2*V_1
	Pol(eval2) = 2*V_1 - 1
	Pol(start) = 2*V_1
orients all transitions weakly and the transitions
	eval2(a, b) -> eval1(a - 1, b) [ a >= 1 /\ b >= 0 /\ b >= a ]
	eval1(a, b) -> eval2(a, 0) [ a >= 1 ]
strictly and produces the following problem:
2:	T:
		(2*a, 1)    eval1(a, b) -> eval2(a, 0) [ a >= 1 ]
		(?, 1)      eval2(a, b) -> eval2(a, b + 1) [ a >= 1 /\ b >= 0 /\ a >= b + 1 ]
		(2*a, 1)    eval2(a, b) -> eval1(a - 1, b) [ a >= 1 /\ b >= 0 /\ b >= a ]
		(1, 1)      start(a, b) -> eval1(a, b)
	start location:	start
	leaf cost:	0

A polynomial rank function with
	Pol(eval2) = V_1 - V_2
and size complexities
	S("start(a, b) -> eval1(a, b)", 0-0) = a
	S("start(a, b) -> eval1(a, b)", 0-1) = b
	S("eval2(a, b) -> eval1(a - 1, b) [ a >= 1 /\\ b >= 0 /\\ b >= a ]", 0-0) = a
	S("eval2(a, b) -> eval1(a - 1, b) [ a >= 1 /\\ b >= 0 /\\ b >= a ]", 0-1) = a
	S("eval2(a, b) -> eval2(a, b + 1) [ a >= 1 /\\ b >= 0 /\\ a >= b + 1 ]", 0-0) = a
	S("eval2(a, b) -> eval2(a, b + 1) [ a >= 1 /\\ b >= 0 /\\ a >= b + 1 ]", 0-1) = a
	S("eval1(a, b) -> eval2(a, 0) [ a >= 1 ]", 0-0) = a
	S("eval1(a, b) -> eval2(a, 0) [ a >= 1 ]", 0-1) = 0
orients the transition
	eval2(a, b) -> eval2(a, b + 1) [ a >= 1 /\ b >= 0 /\ a >= b + 1 ]
weakly and the transition
	eval2(a, b) -> eval2(a, b + 1) [ a >= 1 /\ b >= 0 /\ a >= b + 1 ]
strictly and produces the following problem:
3:	T:
		(2*a, 1)      eval1(a, b) -> eval2(a, 0) [ a >= 1 ]
		(2*a^2, 1)    eval2(a, b) -> eval2(a, b + 1) [ a >= 1 /\ b >= 0 /\ a >= b + 1 ]
		(2*a, 1)      eval2(a, b) -> eval1(a - 1, b) [ a >= 1 /\ b >= 0 /\ b >= a ]
		(1, 1)        start(a, b) -> eval1(a, b)
	start location:	start
	leaf cost:	0

Complexity upper bound 4*a + 2*a^2 + 1

Time: 0.158 sec (SMT: 0.148 sec)