YES(?, 10*a + 2*a^2 + 9)

Initial complexity problem:
1:	T:
		(?, 1)    eval1(a, b) -> eval2(a, 1) [ a >= 0 ]
		(?, 1)    eval2(a, b) -> eval2(a, 2*b) [ a >= 0 /\ b >= 1 /\ a >= b + 1 ]
		(?, 1)    eval2(a, b) -> eval1(a - 1, b) [ a >= 0 /\ b >= 1 /\ 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 + 2
	Pol(eval2) = 2*V_1 + 1
	Pol(start) = 2*V_1 + 2
orients all transitions weakly and the transitions
	eval2(a, b) -> eval1(a - 1, b) [ a >= 0 /\ b >= 1 /\ b >= a ]
	eval1(a, b) -> eval2(a, 1) [ a >= 0 ]
strictly and produces the following problem:
2:	T:
		(2*a + 2, 1)    eval1(a, b) -> eval2(a, 1) [ a >= 0 ]
		(?, 1)          eval2(a, b) -> eval2(a, 2*b) [ a >= 0 /\ b >= 1 /\ a >= b + 1 ]
		(2*a + 2, 1)    eval2(a, b) -> eval1(a - 1, b) [ a >= 0 /\ b >= 1 /\ 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 >= 0 /\\ b >= 1 /\\ b >= a ]", 0-0) = a + 1
	S("eval2(a, b) -> eval1(a - 1, b) [ a >= 0 /\\ b >= 1 /\\ b >= a ]", 0-1) = ?
	S("eval2(a, b) -> eval2(a, 2*b) [ a >= 0 /\\ b >= 1 /\\ a >= b + 1 ]", 0-0) = a + 1
	S("eval2(a, b) -> eval2(a, 2*b) [ a >= 0 /\\ b >= 1 /\\ a >= b + 1 ]", 0-1) = ?
	S("eval1(a, b) -> eval2(a, 1) [ a >= 0 ]", 0-0) = a + 1
	S("eval1(a, b) -> eval2(a, 1) [ a >= 0 ]", 0-1) = 1
orients the transition
	eval2(a, b) -> eval2(a, 2*b) [ a >= 0 /\ b >= 1 /\ a >= b + 1 ]
weakly and the transition
	eval2(a, b) -> eval2(a, 2*b) [ a >= 0 /\ b >= 1 /\ a >= b + 1 ]
strictly and produces the following problem:
3:	T:
		(2*a + 2, 1)            eval1(a, b) -> eval2(a, 1) [ a >= 0 ]
		(2*a^2 + 6*a + 4, 1)    eval2(a, b) -> eval2(a, 2*b) [ a >= 0 /\ b >= 1 /\ a >= b + 1 ]
		(2*a + 2, 1)            eval2(a, b) -> eval1(a - 1, b) [ a >= 0 /\ b >= 1 /\ b >= a ]
		(1, 1)                  start(a, b) -> eval1(a, b)
	start location:	start
	leaf cost:	0

Complexity upper bound 10*a + 2*a^2 + 9

Time: 0.180 sec (SMT: 0.170 sec)