YES(?, 255*a + 120*a^2 + 139)

Initial complexity problem:
1:	T:
		(1, 1)    evalsipmabubblestart(a, b) -> evalsipmabubbleentryin(a, b)
		(?, 1)    evalsipmabubbleentryin(a, b) -> evalsipmabubblebb6in(a, b)
		(?, 1)    evalsipmabubblebb6in(a, b) -> evalsipmabubblebb4in(a, 0) [ a >= 0 ]
		(?, 1)    evalsipmabubblebb6in(a, b) -> evalsipmabubblereturnin(a, b) [ 0 >= a + 1 ]
		(?, 1)    evalsipmabubblebb4in(a, b) -> evalsipmabubblebb1in(a, b) [ a >= b + 1 ]
		(?, 1)    evalsipmabubblebb4in(a, b) -> evalsipmabubblebb5in(a, b) [ b >= a ]
		(?, 1)    evalsipmabubblebb1in(a, b) -> evalsipmabubblebb2in(a, b) [ c >= d + 1 ]
		(?, 1)    evalsipmabubblebb1in(a, b) -> evalsipmabubblebb3in(a, b) [ d >= c ]
		(?, 1)    evalsipmabubblebb2in(a, b) -> evalsipmabubblebb3in(a, b)
		(?, 1)    evalsipmabubblebb3in(a, b) -> evalsipmabubblebb4in(a, b + 1)
		(?, 1)    evalsipmabubblebb5in(a, b) -> evalsipmabubblebb6in(a - 1, b)
		(?, 1)    evalsipmabubblereturnin(a, b) -> evalsipmabubblestop(a, b)
	start location:	evalsipmabubblestart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalsipmabubblestart(a, b) -> evalsipmabubbleentryin(a, b)
		(?, 1)    evalsipmabubbleentryin(a, b) -> evalsipmabubblebb6in(a, b)
		(?, 1)    evalsipmabubblebb6in(a, b) -> evalsipmabubblebb4in(a, 0) [ a >= 0 ]
		(?, 1)    evalsipmabubblebb4in(a, b) -> evalsipmabubblebb1in(a, b) [ a >= b + 1 ]
		(?, 1)    evalsipmabubblebb4in(a, b) -> evalsipmabubblebb5in(a, b) [ b >= a ]
		(?, 1)    evalsipmabubblebb1in(a, b) -> evalsipmabubblebb2in(a, b) [ c >= d + 1 ]
		(?, 1)    evalsipmabubblebb1in(a, b) -> evalsipmabubblebb3in(a, b) [ d >= c ]
		(?, 1)    evalsipmabubblebb2in(a, b) -> evalsipmabubblebb3in(a, b)
		(?, 1)    evalsipmabubblebb3in(a, b) -> evalsipmabubblebb4in(a, b + 1)
		(?, 1)    evalsipmabubblebb5in(a, b) -> evalsipmabubblebb6in(a - 1, b)
	start location:	evalsipmabubblestart
	leaf cost:	2

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalsipmabubblestart(a, b) -> evalsipmabubbleentryin(a, b)
		(1, 1)    evalsipmabubbleentryin(a, b) -> evalsipmabubblebb6in(a, b)
		(?, 1)    evalsipmabubblebb6in(a, b) -> evalsipmabubblebb4in(a, 0) [ a >= 0 ]
		(?, 1)    evalsipmabubblebb4in(a, b) -> evalsipmabubblebb1in(a, b) [ a >= b + 1 ]
		(?, 1)    evalsipmabubblebb4in(a, b) -> evalsipmabubblebb5in(a, b) [ b >= a ]
		(?, 1)    evalsipmabubblebb1in(a, b) -> evalsipmabubblebb2in(a, b) [ c >= d + 1 ]
		(?, 1)    evalsipmabubblebb1in(a, b) -> evalsipmabubblebb3in(a, b) [ d >= c ]
		(?, 1)    evalsipmabubblebb2in(a, b) -> evalsipmabubblebb3in(a, b)
		(?, 1)    evalsipmabubblebb3in(a, b) -> evalsipmabubblebb4in(a, b + 1)
		(?, 1)    evalsipmabubblebb5in(a, b) -> evalsipmabubblebb6in(a - 1, b)
	start location:	evalsipmabubblestart
	leaf cost:	2

Separating problem 3 produces the isolated subproblem
10001:	T:
		(1, 0)    inner_10000_start_sep(a, b) -> evalsipmabubblebb4in(a, 0)
		(?, 1)    evalsipmabubblebb3in(a, b) -> evalsipmabubblebb4in(a, b + 1)
		(?, 1)    evalsipmabubblebb2in(a, b) -> evalsipmabubblebb3in(a, b)
		(?, 1)    evalsipmabubblebb1in(a, b) -> evalsipmabubblebb3in(a, b) [ d >= c ]
		(?, 1)    evalsipmabubblebb1in(a, b) -> evalsipmabubblebb2in(a, b) [ c >= d + 1 ]
		(?, 1)    evalsipmabubblebb4in(a, b) -> evalsipmabubblebb1in(a, b) [ 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) -> evalsipmabubblebb4in(a, 0)
			(?, 1)    evalsipmabubblebb3in(a, b) -> evalsipmabubblebb4in(a, b + 1)
			(?, 1)    evalsipmabubblebb2in(a, b) -> evalsipmabubblebb3in(a, b)
			(?, 1)    evalsipmabubblebb1in(a, b) -> evalsipmabubblebb3in(a, b) [ d >= c ]
			(?, 1)    evalsipmabubblebb1in(a, b) -> evalsipmabubblebb2in(a, b) [ c >= d + 1 ]
			(?, 1)    evalsipmabubblebb4in(a, b) -> evalsipmabubblebb1in(a, b) [ a >= b + 1 ]
		start location:	inner_10000_start_sep
		leaf cost:	0
	
	A polynomial rank function with
		Pol(inner_10000_start_sep) = 4*V_1
		Pol(evalsipmabubblebb4in) = 4*V_1 - 4*V_2
		Pol(evalsipmabubblebb3in) = 4*V_1 - 4*V_2 - 3
		Pol(evalsipmabubblebb2in) = 4*V_1 - 4*V_2 - 2
		Pol(evalsipmabubblebb1in) = 4*V_1 - 4*V_2 - 1
	orients all transitions weakly and the transition
		evalsipmabubblebb4in(a, b) -> evalsipmabubblebb1in(a, b) [ a >= b + 1 ]
	strictly and produces the following problem:
	10002:	T:
			(1, 0)      inner_10000_start_sep(a, b) -> evalsipmabubblebb4in(a, 0)
			(?, 1)      evalsipmabubblebb3in(a, b) -> evalsipmabubblebb4in(a, b + 1)
			(?, 1)      evalsipmabubblebb2in(a, b) -> evalsipmabubblebb3in(a, b)
			(?, 1)      evalsipmabubblebb1in(a, b) -> evalsipmabubblebb3in(a, b) [ d >= c ]
			(?, 1)      evalsipmabubblebb1in(a, b) -> evalsipmabubblebb2in(a, b) [ c >= d + 1 ]
			(4*a, 1)    evalsipmabubblebb4in(a, b) -> evalsipmabubblebb1in(a, b) [ a >= b + 1 ]
		start location:	inner_10000_start_sep
		leaf cost:	0
	
	Repeatedly propagating knowledge in problem 10002 produces the following problem:
	10003:	T:
			(1, 0)      inner_10000_start_sep(a, b) -> evalsipmabubblebb4in(a, 0)
			(8*a, 1)    evalsipmabubblebb3in(a, b) -> evalsipmabubblebb4in(a, b + 1)
			(4*a, 1)    evalsipmabubblebb2in(a, b) -> evalsipmabubblebb3in(a, b)
			(4*a, 1)    evalsipmabubblebb1in(a, b) -> evalsipmabubblebb3in(a, b) [ d >= c ]
			(4*a, 1)    evalsipmabubblebb1in(a, b) -> evalsipmabubblebb2in(a, b) [ c >= d + 1 ]
			(4*a, 1)    evalsipmabubblebb4in(a, b) -> evalsipmabubblebb1in(a, b) [ 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 3 produces the following problem:
4:	T:
		(?, 0)       inner_10000_in_sep(a, b) -> inner_10000_out_sep(a, b)
		(?, 24*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 <= 8*a ]
		(?, 0)       inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ a >= 0 /\ b_sep < 0 /\ -b_sep <= 8*a ]
		(?, 0)       inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ a < 0 /\ b_sep >= 0 /\ b_sep <= -8*a ]
		(?, 0)       inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ a < 0 /\ b_sep < 0 /\ -b_sep <= -8*a ]
		(?, 1)       inner_10000_out_sep(a, b) -> evalsipmabubblebb5in(a, b) [ b >= a ]
		(?, 1)       evalsipmabubblebb6in(a, b) -> inner_10000_in_sep(a, 0) [ a >= 0 ]
		(?, 1)       evalsipmabubblebb5in(a, b) -> evalsipmabubblebb6in(a - 1, b)
		(1, 1)       evalsipmabubbleentryin(a, b) -> evalsipmabubblebb6in(a, b)
		(1, 1)       evalsipmabubblestart(a, b) -> evalsipmabubbleentryin(a, b)
	start location:	evalsipmabubblestart
	leaf cost:	2

Applied AI with 'oct' on problem 4 to obtain the following invariants:
  For symbol evalsipmabubblebb5in: X_2 >= 0 /\ X_1 + X_2 >= 0 /\ -X_1 + X_2 >= 0 /\ X_1 >= 0
  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 >= 0


This yielded the following problem:
5:	T:
		(1, 1)       evalsipmabubblestart(a, b) -> evalsipmabubbleentryin(a, b)
		(1, 1)       evalsipmabubbleentryin(a, b) -> evalsipmabubblebb6in(a, b)
		(?, 1)       evalsipmabubblebb5in(a, b) -> evalsipmabubblebb6in(a - 1, b) [ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 ]
		(?, 1)       evalsipmabubblebb6in(a, b) -> inner_10000_in_sep(a, 0) [ a >= 0 ]
		(?, 1)       inner_10000_out_sep(a, b) -> evalsipmabubblebb5in(a, b) [ 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 <= -8*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 <= -8*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 <= 8*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 <= 8*a ]
		(?, 24*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:	evalsipmabubblestart
	leaf cost:	2

Testing for unsatisfiable constraints removes the following transitions from problem 5:
	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 <= -8*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 <= -8*a ]
We thus obtain the following problem:
6:	T:
		(1, 1)       evalsipmabubblestart(a, b) -> evalsipmabubbleentryin(a, b)
		(1, 1)       evalsipmabubbleentryin(a, b) -> evalsipmabubblebb6in(a, b)
		(?, 1)       evalsipmabubblebb5in(a, b) -> evalsipmabubblebb6in(a - 1, b) [ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 ]
		(?, 1)       evalsipmabubblebb6in(a, b) -> inner_10000_in_sep(a, 0) [ a >= 0 ]
		(?, 1)       inner_10000_out_sep(a, b) -> evalsipmabubblebb5in(a, b) [ 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 <= 8*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 <= 8*a ]
		(?, 24*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:	evalsipmabubblestart
	leaf cost:	2

A polynomial rank function with
	Pol(evalsipmabubblestart) = 5*V_1 + 5
	Pol(evalsipmabubbleentryin) = 5*V_1 + 5
	Pol(evalsipmabubblebb6in) = 5*V_1 + 5
	Pol(evalsipmabubblebb5in) = 5*V_1 + 1
	Pol(inner_10000_in_sep) = 5*V_1 + 4
	Pol(inner_10000_out_sep) = 5*V_1 + 2
	Pol(inner_10000_compl_sep) = 5*V_1 + 3
orients all transitions weakly and the transitions
	inner_10000_out_sep(a, b) -> evalsipmabubblebb5in(a, b) [ 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 <= 8*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 <= 8*a ]
	evalsipmabubblebb6in(a, b) -> inner_10000_in_sep(a, 0) [ a >= 0 ]
	evalsipmabubblebb5in(a, b) -> evalsipmabubblebb6in(a - 1, b) [ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 ]
strictly and produces the following problem:
7:	T:
		(1, 1)             evalsipmabubblestart(a, b) -> evalsipmabubbleentryin(a, b)
		(1, 1)             evalsipmabubbleentryin(a, b) -> evalsipmabubblebb6in(a, b)
		(5*a + 5, 1)       evalsipmabubblebb5in(a, b) -> evalsipmabubblebb6in(a - 1, b) [ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 ]
		(5*a + 5, 1)       evalsipmabubblebb6in(a, b) -> inner_10000_in_sep(a, 0) [ a >= 0 ]
		(5*a + 5, 1)       inner_10000_out_sep(a, b) -> evalsipmabubblebb5in(a, b) [ a >= 0 /\ b >= a ]
		(5*a + 5, 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 <= 8*a ]
		(5*a + 5, 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 <= 8*a ]
		(5*a + 5, 24*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 ]
		(5*a + 5, 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:	evalsipmabubblestart
	leaf cost:	2

Complexity upper bound 255*a + 120*a^2 + 139

Time: 0.529 sec (SMT: 0.504 sec)