YES(?, 16*a + 4*a^2 + 13)

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

Separating problem 1 produces the isolated subproblem
10001:	T:
		(1, 0)    inner_10000_start_sep(a, b) -> eval2(a, 0)
		(?, 1)    eval2(a, b) -> eval2(a, b + 1) [ a >= b + 1 ]
	start location:	inner_10000_start_sep
	leaf cost:	0

=== begin of proof for isolated subproblem 10001 ===
	Initial complexity problem:
	10001:	T:
			(1, 0)    inner_10000_start_sep(a, b) -> eval2(a, 0)
			(?, 1)    eval2(a, b) -> eval2(a, b + 1) [ a >= b + 1 ]
		start location:	inner_10000_start_sep
		leaf cost:	0
	
	A polynomial rank function with
		Pol(inner_10000_start_sep) = V_1
		Pol(eval2) = V_1 - V_2
	orients all transitions weakly and the transition
		eval2(a, b) -> eval2(a, b + 1) [ a >= b + 1 ]
	strictly and produces the following problem:
	10002:	T:
			(1, 0)    inner_10000_start_sep(a, b) -> eval2(a, 0)
			(a, 1)    eval2(a, b) -> eval2(a, b + 1) [ a >= b + 1 ]
		start location:	inner_10000_start_sep
		leaf cost:	0
=== end of proof for isolated subproblem 10001 ===

Applying the information from the isolated subproblem 10001 to problem 1 produces the following problem:
2:	T:
		(?, 0)    inner_10000_in_sep(a, b) -> inner_10000_out_sep(a, b)
		(?, a)    inner_10000_in_sep(a, b) -> inner_10000_compl_sep(a, b)
		(?, 0)    inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ a >= 0 /\ b_sep >= 0 /\ b_sep <= a ]
		(?, 0)    inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ a >= 0 /\ b_sep < 0 /\ -b_sep <= a ]
		(?, 0)    inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ a < 0 /\ b_sep >= 0 /\ b_sep <= -a ]
		(?, 0)    inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ a < 0 /\ b_sep < 0 /\ -b_sep <= -a ]
		(?, 1)    inner_10000_out_sep(a, b) -> eval1(a - 1, b) [ b >= a ]
		(?, 1)    eval1(a, b) -> inner_10000_in_sep(a, 0) [ a >= 0 ]
		(1, 1)    start(a, b) -> eval1(a, b)
	start location:	start
	leaf cost:	0

Applied AI with 'oct' on problem 2 to obtain the following invariants:
  For symbol inner_10000_compl_sep: -X_2 >= 0 /\ X_1 - X_2 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol inner_10000_in_sep: -X_2 >= 0 /\ X_1 - X_2 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol inner_10000_out_sep: X_1 - X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0


This yielded the following problem:
3:	T:
		(1, 1)    start(a, b) -> eval1(a, b)
		(?, 1)    eval1(a, b) -> inner_10000_in_sep(a, 0) [ a >= 0 ]
		(?, 1)    inner_10000_out_sep(a, b) -> eval1(a - 1, b) [ a - b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= a ]
		(?, 0)    inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a < 0 /\ b_sep < 0 /\ -b_sep <= -a ]
		(?, 0)    inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a < 0 /\ b_sep >= 0 /\ b_sep <= -a ]
		(?, 0)    inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b_sep < 0 /\ -b_sep <= a ]
		(?, 0)    inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b_sep >= 0 /\ b_sep <= a ]
		(?, a)    inner_10000_in_sep(a, b) -> inner_10000_compl_sep(a, b) [ -b >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(?, 0)    inner_10000_in_sep(a, b) -> inner_10000_out_sep(a, b) [ -b >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
	start location:	start
	leaf cost:	0

Testing for unsatisfiable constraints removes the following transitions from problem 3:
	inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a < 0 /\ b_sep < 0 /\ -b_sep <= -a ]
	inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a < 0 /\ b_sep >= 0 /\ b_sep <= -a ]
We thus obtain the following problem:
4:	T:
		(1, 1)    start(a, b) -> eval1(a, b)
		(?, 1)    eval1(a, b) -> inner_10000_in_sep(a, 0) [ a >= 0 ]
		(?, 1)    inner_10000_out_sep(a, b) -> eval1(a - 1, b) [ a - b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= a ]
		(?, 0)    inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b_sep < 0 /\ -b_sep <= a ]
		(?, 0)    inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b_sep >= 0 /\ b_sep <= a ]
		(?, a)    inner_10000_in_sep(a, b) -> inner_10000_compl_sep(a, b) [ -b >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(?, 0)    inner_10000_in_sep(a, b) -> inner_10000_out_sep(a, b) [ -b >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
	start location:	start
	leaf cost:	0

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

Complexity upper bound 16*a + 4*a^2 + 13

Time: 0.372 sec (SMT: 0.353 sec)