YES(?, 25*b + 20*b*e + 4)

Initial complexity problem:
1:	T:
		(1, 1)    evalNestedMultipleDepstart(a, b, c, d, e) -> evalNestedMultipleDepentryin(a, b, c, d, e)
		(?, 1)    evalNestedMultipleDepentryin(a, b, c, d, e) -> evalNestedMultipleDepbb3in(0, b, c, d, e)
		(?, 1)    evalNestedMultipleDepbb3in(a, b, c, d, e) -> evalNestedMultipleDepbbin(a, b, c, d, e) [ b >= a + 1 ]
		(?, 1)    evalNestedMultipleDepbb3in(a, b, c, d, e) -> evalNestedMultipleDepreturnin(a, b, c, d, e) [ a >= b ]
		(?, 1)    evalNestedMultipleDepbbin(a, b, c, d, e) -> evalNestedMultipleDepbb2in(a, b, a + 1, 0, e)
		(?, 1)    evalNestedMultipleDepbb2in(a, b, c, d, e) -> evalNestedMultipleDepbb1in(a, b, c, d, e) [ e >= d + 1 ]
		(?, 1)    evalNestedMultipleDepbb2in(a, b, c, d, e) -> evalNestedMultipleDepbb3in(c, b, c, d, e) [ d >= e ]
		(?, 1)    evalNestedMultipleDepbb1in(a, b, c, d, e) -> evalNestedMultipleDepbb2in(a, b, c, d + 1, e)
		(?, 1)    evalNestedMultipleDepreturnin(a, b, c, d, e) -> evalNestedMultipleDepstop(a, b, c, d, e)
	start location:	evalNestedMultipleDepstart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalNestedMultipleDepstart(a, b, c, d, e) -> evalNestedMultipleDepentryin(a, b, c, d, e)
		(?, 1)    evalNestedMultipleDepentryin(a, b, c, d, e) -> evalNestedMultipleDepbb3in(0, b, c, d, e)
		(?, 1)    evalNestedMultipleDepbb3in(a, b, c, d, e) -> evalNestedMultipleDepbbin(a, b, c, d, e) [ b >= a + 1 ]
		(?, 1)    evalNestedMultipleDepbbin(a, b, c, d, e) -> evalNestedMultipleDepbb2in(a, b, a + 1, 0, e)
		(?, 1)    evalNestedMultipleDepbb2in(a, b, c, d, e) -> evalNestedMultipleDepbb1in(a, b, c, d, e) [ e >= d + 1 ]
		(?, 1)    evalNestedMultipleDepbb2in(a, b, c, d, e) -> evalNestedMultipleDepbb3in(c, b, c, d, e) [ d >= e ]
		(?, 1)    evalNestedMultipleDepbb1in(a, b, c, d, e) -> evalNestedMultipleDepbb2in(a, b, c, d + 1, e)
	start location:	evalNestedMultipleDepstart
	leaf cost:	2

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalNestedMultipleDepstart(a, b, c, d, e) -> evalNestedMultipleDepentryin(a, b, c, d, e)
		(1, 1)    evalNestedMultipleDepentryin(a, b, c, d, e) -> evalNestedMultipleDepbb3in(0, b, c, d, e)
		(?, 1)    evalNestedMultipleDepbb3in(a, b, c, d, e) -> evalNestedMultipleDepbbin(a, b, c, d, e) [ b >= a + 1 ]
		(?, 1)    evalNestedMultipleDepbbin(a, b, c, d, e) -> evalNestedMultipleDepbb2in(a, b, a + 1, 0, e)
		(?, 1)    evalNestedMultipleDepbb2in(a, b, c, d, e) -> evalNestedMultipleDepbb1in(a, b, c, d, e) [ e >= d + 1 ]
		(?, 1)    evalNestedMultipleDepbb2in(a, b, c, d, e) -> evalNestedMultipleDepbb3in(c, b, c, d, e) [ d >= e ]
		(?, 1)    evalNestedMultipleDepbb1in(a, b, c, d, e) -> evalNestedMultipleDepbb2in(a, b, c, d + 1, e)
	start location:	evalNestedMultipleDepstart
	leaf cost:	2

Separating problem 3 produces the isolated subproblem
10001:	T:
		(1, 0)    inner_10000_start_sep(a, b, c, d, e) -> evalNestedMultipleDepbb2in(a, b, a + 1, 0, e)
		(?, 1)    evalNestedMultipleDepbb1in(a, b, c, d, e) -> evalNestedMultipleDepbb2in(a, b, c, d + 1, e)
		(?, 1)    evalNestedMultipleDepbb2in(a, b, c, d, e) -> evalNestedMultipleDepbb1in(a, b, c, d, e) [ e >= d + 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, c, d, e) -> evalNestedMultipleDepbb2in(a, b, a + 1, 0, e)
			(?, 1)    evalNestedMultipleDepbb1in(a, b, c, d, e) -> evalNestedMultipleDepbb2in(a, b, c, d + 1, e)
			(?, 1)    evalNestedMultipleDepbb2in(a, b, c, d, e) -> evalNestedMultipleDepbb1in(a, b, c, d, e) [ e >= d + 1 ]
		start location:	inner_10000_start_sep
		leaf cost:	0
	
	A polynomial rank function with
		Pol(inner_10000_start_sep) = 2*V_5 + 1
		Pol(evalNestedMultipleDepbb2in) = -2*V_4 + 2*V_5 + 1
		Pol(evalNestedMultipleDepbb1in) = -2*V_4 + 2*V_5
	orients all transitions weakly and the transition
		evalNestedMultipleDepbb2in(a, b, c, d, e) -> evalNestedMultipleDepbb1in(a, b, c, d, e) [ e >= d + 1 ]
	strictly and produces the following problem:
	10002:	T:
			(1, 0)          inner_10000_start_sep(a, b, c, d, e) -> evalNestedMultipleDepbb2in(a, b, a + 1, 0, e)
			(?, 1)          evalNestedMultipleDepbb1in(a, b, c, d, e) -> evalNestedMultipleDepbb2in(a, b, c, d + 1, e)
			(2*e + 1, 1)    evalNestedMultipleDepbb2in(a, b, c, d, e) -> evalNestedMultipleDepbb1in(a, b, c, d, e) [ e >= d + 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, c, d, e) -> evalNestedMultipleDepbb2in(a, b, a + 1, 0, e)
			(2*e + 1, 1)    evalNestedMultipleDepbb1in(a, b, c, d, e) -> evalNestedMultipleDepbb2in(a, b, c, d + 1, e)
			(2*e + 1, 1)    evalNestedMultipleDepbb2in(a, b, c, d, e) -> evalNestedMultipleDepbb1in(a, b, c, d, e) [ e >= d + 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, c, d, e) -> inner_10000_out_sep(a, b, c, d, e)
		(?, 4*e + 2)    inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e)
		(?, 0)          inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d_sep, e) [ e >= 0 /\ d_sep >= 0 /\ d_sep <= 2*e + 4 ]
		(?, 0)          inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d_sep, e) [ e >= 0 /\ d_sep < 0 /\ -d_sep <= 2*e + 4 ]
		(?, 0)          inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d_sep, e) [ e < 0 /\ d_sep >= 0 /\ d_sep <= -2*e + 4 ]
		(?, 0)          inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d_sep, e) [ e < 0 /\ d_sep < 0 /\ -d_sep <= -2*e + 4 ]
		(?, 1)          inner_10000_out_sep(a, b, c, d, e) -> evalNestedMultipleDepbb3in(c, b, c, d, e) [ d >= e ]
		(?, 1)          evalNestedMultipleDepbbin(a, b, c, d, e) -> inner_10000_in_sep(a, b, a + 1, 0, e)
		(?, 1)          evalNestedMultipleDepbb3in(a, b, c, d, e) -> evalNestedMultipleDepbbin(a, b, c, d, e) [ b >= a + 1 ]
		(1, 1)          evalNestedMultipleDepentryin(a, b, c, d, e) -> evalNestedMultipleDepbb3in(0, b, c, d, e)
		(1, 1)          evalNestedMultipleDepstart(a, b, c, d, e) -> evalNestedMultipleDepentryin(a, b, c, d, e)
	start location:	evalNestedMultipleDepstart
	leaf cost:	2

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


This yielded the following problem:
5:	T:
		(1, 1)          evalNestedMultipleDepstart(a, b, c, d, e) -> evalNestedMultipleDepentryin(a, b, c, d, e)
		(1, 1)          evalNestedMultipleDepentryin(a, b, c, d, e) -> evalNestedMultipleDepbb3in(0, b, c, d, e)
		(?, 1)          evalNestedMultipleDepbb3in(a, b, c, d, e) -> evalNestedMultipleDepbbin(a, b, c, d, e) [ a >= 0 /\ b >= a + 1 ]
		(?, 1)          evalNestedMultipleDepbbin(a, b, c, d, e) -> inner_10000_in_sep(a, b, a + 1, 0, e) [ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 ]
		(?, 1)          inner_10000_out_sep(a, b, c, d, e) -> evalNestedMultipleDepbb3in(c, b, c, d, e) [ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ d >= e ]
		(?, 0)          inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d_sep, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ e < 0 /\ d_sep < 0 /\ -d_sep <= -2*e + 4 ]
		(?, 0)          inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d_sep, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ e < 0 /\ d_sep >= 0 /\ d_sep <= -2*e + 4 ]
		(?, 0)          inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d_sep, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ e >= 0 /\ d_sep < 0 /\ -d_sep <= 2*e + 4 ]
		(?, 0)          inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d_sep, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ e >= 0 /\ d_sep >= 0 /\ d_sep <= 2*e + 4 ]
		(?, 4*e + 2)    inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 ]
		(?, 0)          inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 ]
	start location:	evalNestedMultipleDepstart
	leaf cost:	2

A polynomial rank function with
	Pol(evalNestedMultipleDepstart) = 5*V_2
	Pol(evalNestedMultipleDepentryin) = 5*V_2
	Pol(evalNestedMultipleDepbb3in) = -5*V_1 + 5*V_2
	Pol(evalNestedMultipleDepbbin) = -5*V_1 + 5*V_2 - 1
	Pol(inner_10000_in_sep) = 5*V_2 - 5*V_3 + 3
	Pol(inner_10000_out_sep) = 5*V_2 - 5*V_3 + 1
	Pol(inner_10000_compl_sep) = 5*V_2 - 5*V_3 + 2
orients all transitions weakly and the transitions
	inner_10000_out_sep(a, b, c, d, e) -> evalNestedMultipleDepbb3in(c, b, c, d, e) [ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ d >= e ]
	inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 ]
	inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 ]
	inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d_sep, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ e < 0 /\ d_sep < 0 /\ -d_sep <= -2*e + 4 ]
	inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d_sep, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ e < 0 /\ d_sep >= 0 /\ d_sep <= -2*e + 4 ]
	inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d_sep, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ e >= 0 /\ d_sep < 0 /\ -d_sep <= 2*e + 4 ]
	inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d_sep, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ e >= 0 /\ d_sep >= 0 /\ d_sep <= 2*e + 4 ]
	evalNestedMultipleDepbbin(a, b, c, d, e) -> inner_10000_in_sep(a, b, a + 1, 0, e) [ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 ]
	evalNestedMultipleDepbb3in(a, b, c, d, e) -> evalNestedMultipleDepbbin(a, b, c, d, e) [ a >= 0 /\ b >= a + 1 ]
strictly and produces the following problem:
6:	T:
		(1, 1)            evalNestedMultipleDepstart(a, b, c, d, e) -> evalNestedMultipleDepentryin(a, b, c, d, e)
		(1, 1)            evalNestedMultipleDepentryin(a, b, c, d, e) -> evalNestedMultipleDepbb3in(0, b, c, d, e)
		(5*b, 1)          evalNestedMultipleDepbb3in(a, b, c, d, e) -> evalNestedMultipleDepbbin(a, b, c, d, e) [ a >= 0 /\ b >= a + 1 ]
		(5*b, 1)          evalNestedMultipleDepbbin(a, b, c, d, e) -> inner_10000_in_sep(a, b, a + 1, 0, e) [ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 ]
		(5*b, 1)          inner_10000_out_sep(a, b, c, d, e) -> evalNestedMultipleDepbb3in(c, b, c, d, e) [ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ d >= e ]
		(5*b, 0)          inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d_sep, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ e < 0 /\ d_sep < 0 /\ -d_sep <= -2*e + 4 ]
		(5*b, 0)          inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d_sep, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ e < 0 /\ d_sep >= 0 /\ d_sep <= -2*e + 4 ]
		(5*b, 0)          inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d_sep, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ e >= 0 /\ d_sep < 0 /\ -d_sep <= 2*e + 4 ]
		(5*b, 0)          inner_10000_compl_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d_sep, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ e >= 0 /\ d_sep >= 0 /\ d_sep <= 2*e + 4 ]
		(5*b, 4*e + 2)    inner_10000_in_sep(a, b, c, d, e) -> inner_10000_compl_sep(a, b, c, d, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 ]
		(5*b, 0)          inner_10000_in_sep(a, b, c, d, e) -> inner_10000_out_sep(a, b, c, d, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d - 1 >= 0 /\ a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 ]
	start location:	evalNestedMultipleDepstart
	leaf cost:	2

Complexity upper bound 25*b + 20*b*e + 4

Time: 0.649 sec (SMT: 0.587 sec)