YES(?, 132*b + 72*b^2 + 64)

Initial complexity problem:
1:	T:
		(1, 1)    evalrealselectstart(a, b, c) -> evalrealselectentryin(a, b, c)
		(?, 1)    evalrealselectentryin(a, b, c) -> evalrealselectbb6in(0, b, c)
		(?, 1)    evalrealselectbb6in(a, b, c) -> evalrealselectbbin(a, b, c) [ b >= a + 2 ]
		(?, 1)    evalrealselectbb6in(a, b, c) -> evalrealselectreturnin(a, b, c) [ a + 1 >= b ]
		(?, 1)    evalrealselectbbin(a, b, c) -> evalrealselectbb4in(a, b, a + 1)
		(?, 1)    evalrealselectbb4in(a, b, c) -> evalrealselectbb1in(a, b, c) [ b >= c + 1 ]
		(?, 1)    evalrealselectbb4in(a, b, c) -> evalrealselectbb5in(a, b, c) [ c >= b ]
		(?, 1)    evalrealselectbb1in(a, b, c) -> evalrealselectbb4in(a, b, c + 1) [ d >= e + 1 ]
		(?, 1)    evalrealselectbb1in(a, b, c) -> evalrealselectbb4in(a, b, c + 1) [ e >= d ]
		(?, 1)    evalrealselectbb5in(a, b, c) -> evalrealselectbb6in(a + 1, b, c)
		(?, 1)    evalrealselectreturnin(a, b, c) -> evalrealselectstop(a, b, c)
	start location:	evalrealselectstart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalrealselectstart(a, b, c) -> evalrealselectentryin(a, b, c)
		(?, 1)    evalrealselectentryin(a, b, c) -> evalrealselectbb6in(0, b, c)
		(?, 1)    evalrealselectbb6in(a, b, c) -> evalrealselectbbin(a, b, c) [ b >= a + 2 ]
		(?, 1)    evalrealselectbbin(a, b, c) -> evalrealselectbb4in(a, b, a + 1)
		(?, 1)    evalrealselectbb4in(a, b, c) -> evalrealselectbb1in(a, b, c) [ b >= c + 1 ]
		(?, 1)    evalrealselectbb4in(a, b, c) -> evalrealselectbb5in(a, b, c) [ c >= b ]
		(?, 1)    evalrealselectbb1in(a, b, c) -> evalrealselectbb4in(a, b, c + 1) [ d >= e + 1 ]
		(?, 1)    evalrealselectbb1in(a, b, c) -> evalrealselectbb4in(a, b, c + 1) [ e >= d ]
		(?, 1)    evalrealselectbb5in(a, b, c) -> evalrealselectbb6in(a + 1, b, c)
	start location:	evalrealselectstart
	leaf cost:	2

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalrealselectstart(a, b, c) -> evalrealselectentryin(a, b, c)
		(1, 1)    evalrealselectentryin(a, b, c) -> evalrealselectbb6in(0, b, c)
		(?, 1)    evalrealselectbb6in(a, b, c) -> evalrealselectbbin(a, b, c) [ b >= a + 2 ]
		(?, 1)    evalrealselectbbin(a, b, c) -> evalrealselectbb4in(a, b, a + 1)
		(?, 1)    evalrealselectbb4in(a, b, c) -> evalrealselectbb1in(a, b, c) [ b >= c + 1 ]
		(?, 1)    evalrealselectbb4in(a, b, c) -> evalrealselectbb5in(a, b, c) [ c >= b ]
		(?, 1)    evalrealselectbb1in(a, b, c) -> evalrealselectbb4in(a, b, c + 1) [ d >= e + 1 ]
		(?, 1)    evalrealselectbb1in(a, b, c) -> evalrealselectbb4in(a, b, c + 1) [ e >= d ]
		(?, 1)    evalrealselectbb5in(a, b, c) -> evalrealselectbb6in(a + 1, b, c)
	start location:	evalrealselectstart
	leaf cost:	2

Separating problem 3 produces the isolated subproblem
10001:	T:
		(1, 0)    inner_10000_start_sep(a, b, c) -> evalrealselectbb4in(a, b, a + 1)
		(?, 1)    evalrealselectbb1in(a, b, c) -> evalrealselectbb4in(a, b, c + 1) [ e >= d ]
		(?, 1)    evalrealselectbb1in(a, b, c) -> evalrealselectbb4in(a, b, c + 1) [ d >= e + 1 ]
		(?, 1)    evalrealselectbb4in(a, b, c) -> evalrealselectbb1in(a, b, c) [ b >= c + 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) -> evalrealselectbb4in(a, b, a + 1)
			(?, 1)    evalrealselectbb1in(a, b, c) -> evalrealselectbb4in(a, b, c + 1) [ e >= d ]
			(?, 1)    evalrealselectbb1in(a, b, c) -> evalrealselectbb4in(a, b, c + 1) [ d >= e + 1 ]
			(?, 1)    evalrealselectbb4in(a, b, c) -> evalrealselectbb1in(a, b, c) [ b >= c + 1 ]
		start location:	inner_10000_start_sep
		leaf cost:	0
	
	A polynomial rank function with
		Pol(inner_10000_start_sep) = -2*V_1 + 2*V_2 - 2
		Pol(evalrealselectbb4in) = 2*V_2 - 2*V_3
		Pol(evalrealselectbb1in) = 2*V_2 - 2*V_3 - 1
	orients all transitions weakly and the transition
		evalrealselectbb4in(a, b, c) -> evalrealselectbb1in(a, b, c) [ b >= c + 1 ]
	strictly and produces the following problem:
	10002:	T:
			(1, 0)                inner_10000_start_sep(a, b, c) -> evalrealselectbb4in(a, b, a + 1)
			(?, 1)                evalrealselectbb1in(a, b, c) -> evalrealselectbb4in(a, b, c + 1) [ e >= d ]
			(?, 1)                evalrealselectbb1in(a, b, c) -> evalrealselectbb4in(a, b, c + 1) [ d >= e + 1 ]
			(2*a + 2*b + 2, 1)    evalrealselectbb4in(a, b, c) -> evalrealselectbb1in(a, b, c) [ b >= c + 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) -> evalrealselectbb4in(a, b, a + 1)
			(2*a + 2*b + 2, 1)    evalrealselectbb1in(a, b, c) -> evalrealselectbb4in(a, b, c + 1) [ e >= d ]
			(2*a + 2*b + 2, 1)    evalrealselectbb1in(a, b, c) -> evalrealselectbb4in(a, b, c + 1) [ d >= e + 1 ]
			(2*a + 2*b + 2, 1)    evalrealselectbb4in(a, b, c) -> evalrealselectbb1in(a, b, c) [ b >= c + 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) -> inner_10000_out_sep(a, b, c)
		(?, 6*a + 6*b + 6)    inner_10000_in_sep(a, b, c) -> inner_10000_compl_sep(a, b, c)
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b >= 0 /\ a >= 0 /\ c_sep >= 0 /\ c_sep <= 5*a + 5*b + 125 ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b >= 0 /\ a >= 0 /\ c_sep < 0 /\ -c_sep <= 5*a + 5*b + 125 ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b >= 0 /\ a < 0 /\ c_sep >= 0 /\ c_sep <= -5*a + 5*b + 125 ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b >= 0 /\ a < 0 /\ c_sep < 0 /\ -c_sep <= -5*a + 5*b + 125 ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b < 0 /\ a >= 0 /\ c_sep >= 0 /\ c_sep <= 5*a - 5*b + 125 ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b < 0 /\ a >= 0 /\ c_sep < 0 /\ -c_sep <= 5*a - 5*b + 125 ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b < 0 /\ a < 0 /\ c_sep >= 0 /\ c_sep <= -5*a - 5*b + 125 ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b < 0 /\ a < 0 /\ c_sep < 0 /\ -c_sep <= -5*a - 5*b + 125 ]
		(?, 1)                inner_10000_out_sep(a, b, c) -> evalrealselectbb5in(a, b, c) [ c >= b ]
		(?, 1)                evalrealselectbbin(a, b, c) -> inner_10000_in_sep(a, b, a + 1)
		(?, 1)                evalrealselectbb5in(a, b, c) -> evalrealselectbb6in(a + 1, b, c)
		(?, 1)                evalrealselectbb6in(a, b, c) -> evalrealselectbbin(a, b, c) [ b >= a + 2 ]
		(1, 1)                evalrealselectentryin(a, b, c) -> evalrealselectbb6in(0, b, c)
		(1, 1)                evalrealselectstart(a, b, c) -> evalrealselectentryin(a, b, c)
	start location:	evalrealselectstart
	leaf cost:	2

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


This yielded the following problem:
5:	T:
		(1, 1)                evalrealselectstart(a, b, c) -> evalrealselectentryin(a, b, c)
		(1, 1)                evalrealselectentryin(a, b, c) -> evalrealselectbb6in(0, b, c)
		(?, 1)                evalrealselectbb6in(a, b, c) -> evalrealselectbbin(a, b, c) [ a >= 0 /\ b >= a + 2 ]
		(?, 1)                evalrealselectbb5in(a, b, c) -> evalrealselectbb6in(a + 1, b, c) [ c - 2 >= 0 /\ b + c - 4 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ -a + c - 2 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 ]
		(?, 1)                evalrealselectbbin(a, b, c) -> inner_10000_in_sep(a, b, a + 1) [ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 ]
		(?, 1)                inner_10000_out_sep(a, b, c) -> evalrealselectbb5in(a, b, c) [ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ c >= b ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b < 0 /\ a < 0 /\ c_sep < 0 /\ -c_sep <= -5*a - 5*b + 125 ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b < 0 /\ a < 0 /\ c_sep >= 0 /\ c_sep <= -5*a - 5*b + 125 ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b < 0 /\ c_sep < 0 /\ -c_sep <= 5*a - 5*b + 125 ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b < 0 /\ c_sep >= 0 /\ c_sep <= 5*a - 5*b + 125 ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b >= 0 /\ a < 0 /\ c_sep < 0 /\ -c_sep <= -5*a + 5*b + 125 ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b >= 0 /\ a < 0 /\ c_sep >= 0 /\ c_sep <= -5*a + 5*b + 125 ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b >= 0 /\ c_sep < 0 /\ -c_sep <= 5*a + 5*b + 125 ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b >= 0 /\ c_sep >= 0 /\ c_sep <= 5*a + 5*b + 125 ]
		(?, 6*a + 6*b + 6)    inner_10000_in_sep(a, b, c) -> inner_10000_compl_sep(a, b, c) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 ]
		(?, 0)                inner_10000_in_sep(a, b, c) -> inner_10000_out_sep(a, b, c) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 ]
	start location:	evalrealselectstart
	leaf cost:	2

Testing for unsatisfiable constraints removes the following transitions from problem 5:
	inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b < 0 /\ a < 0 /\ c_sep < 0 /\ -c_sep <= -5*a - 5*b + 125 ]
	inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b < 0 /\ a < 0 /\ c_sep >= 0 /\ c_sep <= -5*a - 5*b + 125 ]
	inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b < 0 /\ c_sep < 0 /\ -c_sep <= 5*a - 5*b + 125 ]
	inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b < 0 /\ c_sep >= 0 /\ c_sep <= 5*a - 5*b + 125 ]
	inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b >= 0 /\ a < 0 /\ c_sep < 0 /\ -c_sep <= -5*a + 5*b + 125 ]
	inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b >= 0 /\ a < 0 /\ c_sep >= 0 /\ c_sep <= -5*a + 5*b + 125 ]
We thus obtain the following problem:
6:	T:
		(1, 1)                evalrealselectstart(a, b, c) -> evalrealselectentryin(a, b, c)
		(1, 1)                evalrealselectentryin(a, b, c) -> evalrealselectbb6in(0, b, c)
		(?, 1)                evalrealselectbb6in(a, b, c) -> evalrealselectbbin(a, b, c) [ a >= 0 /\ b >= a + 2 ]
		(?, 1)                evalrealselectbb5in(a, b, c) -> evalrealselectbb6in(a + 1, b, c) [ c - 2 >= 0 /\ b + c - 4 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ -a + c - 2 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 ]
		(?, 1)                evalrealselectbbin(a, b, c) -> inner_10000_in_sep(a, b, a + 1) [ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 ]
		(?, 1)                inner_10000_out_sep(a, b, c) -> evalrealselectbb5in(a, b, c) [ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ c >= b ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b >= 0 /\ c_sep < 0 /\ -c_sep <= 5*a + 5*b + 125 ]
		(?, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b >= 0 /\ c_sep >= 0 /\ c_sep <= 5*a + 5*b + 125 ]
		(?, 6*a + 6*b + 6)    inner_10000_in_sep(a, b, c) -> inner_10000_compl_sep(a, b, c) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 ]
		(?, 0)                inner_10000_in_sep(a, b, c) -> inner_10000_out_sep(a, b, c) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 ]
	start location:	evalrealselectstart
	leaf cost:	2

A polynomial rank function with
	Pol(evalrealselectstart) = 6*V_2 - 6
	Pol(evalrealselectentryin) = 6*V_2 - 6
	Pol(evalrealselectbb6in) = -6*V_1 + 6*V_2 - 6
	Pol(evalrealselectbbin) = -6*V_1 + 6*V_2 - 7
	Pol(evalrealselectbb5in) = -6*V_1 + 6*V_2 - 11
	Pol(inner_10000_in_sep) = -6*V_1 + 6*V_2 - 8
	Pol(inner_10000_out_sep) = -6*V_1 + 6*V_2 - 10
	Pol(inner_10000_compl_sep) = -6*V_1 + 6*V_2 - 9
orients all transitions weakly and the transitions
	inner_10000_out_sep(a, b, c) -> evalrealselectbb5in(a, b, c) [ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ c >= b ]
	inner_10000_in_sep(a, b, c) -> inner_10000_out_sep(a, b, c) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 ]
	inner_10000_in_sep(a, b, c) -> inner_10000_compl_sep(a, b, c) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 ]
	inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b >= 0 /\ c_sep < 0 /\ -c_sep <= 5*a + 5*b + 125 ]
	inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b >= 0 /\ c_sep >= 0 /\ c_sep <= 5*a + 5*b + 125 ]
	evalrealselectbbin(a, b, c) -> inner_10000_in_sep(a, b, a + 1) [ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 ]
	evalrealselectbb6in(a, b, c) -> evalrealselectbbin(a, b, c) [ a >= 0 /\ b >= a + 2 ]
	evalrealselectbb5in(a, b, c) -> evalrealselectbb6in(a + 1, b, c) [ c - 2 >= 0 /\ b + c - 4 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ -a + c - 2 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 ]
strictly and produces the following problem:
7:	T:
		(1, 1)                      evalrealselectstart(a, b, c) -> evalrealselectentryin(a, b, c)
		(1, 1)                      evalrealselectentryin(a, b, c) -> evalrealselectbb6in(0, b, c)
		(6*b + 6, 1)                evalrealselectbb6in(a, b, c) -> evalrealselectbbin(a, b, c) [ a >= 0 /\ b >= a + 2 ]
		(6*b + 6, 1)                evalrealselectbb5in(a, b, c) -> evalrealselectbb6in(a + 1, b, c) [ c - 2 >= 0 /\ b + c - 4 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ -a + c - 2 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 ]
		(6*b + 6, 1)                evalrealselectbbin(a, b, c) -> inner_10000_in_sep(a, b, a + 1) [ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 ]
		(6*b + 6, 1)                inner_10000_out_sep(a, b, c) -> evalrealselectbb5in(a, b, c) [ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ c >= b ]
		(6*b + 6, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b >= 0 /\ c_sep < 0 /\ -c_sep <= 5*a + 5*b + 125 ]
		(6*b + 6, 0)                inner_10000_compl_sep(a, b, c) -> inner_10000_out_sep(a, b, c_sep) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 /\ b >= 0 /\ c_sep >= 0 /\ c_sep <= 5*a + 5*b + 125 ]
		(6*b + 6, 6*a + 6*b + 6)    inner_10000_in_sep(a, b, c) -> inner_10000_compl_sep(a, b, c) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 ]
		(6*b + 6, 0)                inner_10000_in_sep(a, b, c) -> inner_10000_out_sep(a, b, c) [ b - c - 1 >= 0 /\ a - c + 1 >= 0 /\ c - 1 >= 0 /\ b + c - 3 >= 0 /\ a + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ b - 2 >= 0 /\ a + b - 2 >= 0 /\ -a + b - 2 >= 0 /\ a >= 0 ]
	start location:	evalrealselectstart
	leaf cost:	2

Complexity upper bound 132*b + 72*b^2 + 64

Time: 0.630 sec (SMT: 0.588 sec)