YES(?, 11*b + 4*b^2 + 7)

Initial complexity problem:
1:	T:
		(1, 1)    l0(a, b, c, d) -> l1(0, b, c, d)
		(?, 1)    l1(a, b, c, d) -> l2(a, b, 0, 0) [ b >= 1 ]
		(?, 1)    l2(a, b, c, d) -> l2(a, b, c + 1, d + c) [ b >= c + 1 ]
		(?, 1)    l2(a, b, c, d) -> l1(a + d, b - 1, c, d) [ c >= b ]
	start location:	l0
	leaf cost:	0

Separating problem 1 produces the isolated subproblem
10001:	T:
		(1, 0)    inner_10000_start_sep(a, b, c, d) -> l2(a, b, 0, 0)
		(?, 1)    l2(a, b, c, d) -> l2(a, b, c + 1, d + 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, d) -> l2(a, b, 0, 0)
			(?, 1)    l2(a, b, c, d) -> l2(a, b, c + 1, d + c) [ b >= c + 1 ]
		start location:	inner_10000_start_sep
		leaf cost:	0
	
	A polynomial rank function with
		Pol(inner_10000_start_sep) = V_2
		Pol(l2) = V_2 - V_3
	orients all transitions weakly and the transition
		l2(a, b, c, d) -> l2(a, b, c + 1, d + c) [ b >= c + 1 ]
	strictly and produces the following problem:
	10002:	T:
			(1, 0)    inner_10000_start_sep(a, b, c, d) -> l2(a, b, 0, 0)
			(b, 1)    l2(a, b, c, d) -> l2(a, b, c + 1, d + 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 1 produces the following problem:
2:	T:
		(?, 0)    inner_10000_in_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c, d)
		(?, b)    inner_10000_in_sep(a, b, c, d) -> inner_10000_compl_sep(a, b, c, d)
		(?, 0)    inner_10000_compl_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c_sep, d_sep) [ d_sep >= 0 /\ b >= 0 /\ c_sep >= 0 /\ d_sep <= b + b^2 /\ c_sep <= b ]
		(?, 0)    inner_10000_compl_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c_sep, d_sep) [ d_sep >= 0 /\ b >= 0 /\ c_sep < 0 /\ d_sep <= b + b^2 /\ -c_sep <= b ]
		(?, 0)    inner_10000_compl_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c_sep, d_sep) [ d_sep >= 0 /\ b < 0 /\ c_sep >= 0 /\ d_sep <= -b + b^2 /\ c_sep <= -b ]
		(?, 0)    inner_10000_compl_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c_sep, d_sep) [ d_sep >= 0 /\ b < 0 /\ c_sep < 0 /\ d_sep <= -b + b^2 /\ -c_sep <= -b ]
		(?, 0)    inner_10000_compl_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c_sep, d_sep) [ d_sep < 0 /\ b >= 0 /\ c_sep >= 0 /\ -d_sep <= b + b^2 /\ c_sep <= b ]
		(?, 0)    inner_10000_compl_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c_sep, d_sep) [ d_sep < 0 /\ b >= 0 /\ c_sep < 0 /\ -d_sep <= b + b^2 /\ -c_sep <= b ]
		(?, 0)    inner_10000_compl_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c_sep, d_sep) [ d_sep < 0 /\ b < 0 /\ c_sep >= 0 /\ -d_sep <= -b + b^2 /\ c_sep <= -b ]
		(?, 0)    inner_10000_compl_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c_sep, d_sep) [ d_sep < 0 /\ b < 0 /\ c_sep < 0 /\ -d_sep <= -b + b^2 /\ -c_sep <= -b ]
		(?, 1)    inner_10000_out_sep(a, b, c, d) -> l1(a + d, b - 1, c, d) [ c >= b ]
		(?, 1)    l1(a, b, c, d) -> inner_10000_in_sep(a, b, 0, 0) [ b >= 1 ]
		(1, 1)    l0(a, b, c, d) -> l1(0, b, c, d)
	start location:	l0
	leaf cost:	0

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


This yielded the following problem:
3:	T:
		(1, 1)    l0(a, b, c, d) -> l1(0, b, c, d)
		(?, 1)    l1(a, b, c, d) -> inner_10000_in_sep(a, b, 0, 0) [ b >= 1 ]
		(?, 1)    inner_10000_out_sep(a, b, c, d) -> l1(a + d, b - 1, c, d) [ b - c >= 0 /\ b + c >= 0 /\ b - 1 >= 0 /\ c >= b ]
		(?, 0)    inner_10000_compl_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c_sep, d_sep) [ -d >= 0 /\ c - d >= 0 /\ -c - d >= 0 /\ b - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 1 >= 0 /\ -c >= 0 /\ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ b - 1 >= 0 /\ d_sep < 0 /\ b < 0 /\ c_sep < 0 /\ -d_sep <= -b + b^2 /\ -c_sep <= -b ]
		(?, 0)    inner_10000_compl_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c_sep, d_sep) [ -d >= 0 /\ c - d >= 0 /\ -c - d >= 0 /\ b - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 1 >= 0 /\ -c >= 0 /\ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ b - 1 >= 0 /\ d_sep < 0 /\ b < 0 /\ c_sep >= 0 /\ -d_sep <= -b + b^2 /\ c_sep <= -b ]
		(?, 0)    inner_10000_compl_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c_sep, d_sep) [ -d >= 0 /\ c - d >= 0 /\ -c - d >= 0 /\ b - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 1 >= 0 /\ -c >= 0 /\ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ b - 1 >= 0 /\ d_sep < 0 /\ b >= 0 /\ c_sep < 0 /\ -d_sep <= b + b^2 /\ -c_sep <= b ]
		(?, 0)    inner_10000_compl_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c_sep, d_sep) [ -d >= 0 /\ c - d >= 0 /\ -c - d >= 0 /\ b - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 1 >= 0 /\ -c >= 0 /\ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ b - 1 >= 0 /\ d_sep < 0 /\ b >= 0 /\ c_sep >= 0 /\ -d_sep <= b + b^2 /\ c_sep <= b ]
		(?, 0)    inner_10000_compl_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c_sep, d_sep) [ -d >= 0 /\ c - d >= 0 /\ -c - d >= 0 /\ b - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 1 >= 0 /\ -c >= 0 /\ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ b - 1 >= 0 /\ d_sep >= 0 /\ b < 0 /\ c_sep < 0 /\ d_sep <= -b + b^2 /\ -c_sep <= -b ]
		(?, 0)    inner_10000_compl_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c_sep, d_sep) [ -d >= 0 /\ c - d >= 0 /\ -c - d >= 0 /\ b - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 1 >= 0 /\ -c >= 0 /\ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ b - 1 >= 0 /\ d_sep >= 0 /\ b < 0 /\ c_sep >= 0 /\ d_sep <= -b + b^2 /\ c_sep <= -b ]
		(?, 0)    inner_10000_compl_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c_sep, d_sep) [ -d >= 0 /\ c - d >= 0 /\ -c - d >= 0 /\ b - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 1 >= 0 /\ -c >= 0 /\ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ b - 1 >= 0 /\ d_sep >= 0 /\ b >= 0 /\ c_sep < 0 /\ d_sep <= b + b^2 /\ -c_sep <= b ]
		(?, 0)    inner_10000_compl_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c_sep, d_sep) [ -d >= 0 /\ c - d >= 0 /\ -c - d >= 0 /\ b - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 1 >= 0 /\ -c >= 0 /\ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ b - 1 >= 0 /\ d_sep >= 0 /\ b >= 0 /\ c_sep >= 0 /\ d_sep <= b + b^2 /\ c_sep <= b ]
		(?, b)    inner_10000_in_sep(a, b, c, d) -> inner_10000_compl_sep(a, b, c, d) [ -d >= 0 /\ c - d >= 0 /\ -c - d >= 0 /\ b - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 1 >= 0 /\ -c >= 0 /\ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ b - 1 >= 0 ]
		(?, 0)    inner_10000_in_sep(a, b, c, d) -> inner_10000_out_sep(a, b, c, d) [ -d >= 0 /\ c - d >= 0 /\ -c - d >= 0 /\ b - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ b + d - 1 >= 0 /\ -c >= 0 /\ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ b - 1 >= 0 ]
	start location:	l0
	leaf cost:	0

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

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

Complexity upper bound 11*b + 4*b^2 + 7

Time: 0.812 sec (SMT: 0.760 sec)