YES(?, 149*a + 6*a^2 + 336)

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

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

Complexity upper bound 149*a + 6*a^2 + 336

Time: 0.139 sec (SMT: 0.131 sec)