YES(?, 15*b + 12*b^2 + 4*b^3 + 8)

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 > 0 ]
		(?, 1)    l2(a, b, c, d) -> l2(a, b, c + 1, d + c) [ c < b ]
		(?, 1)    l2(a, b, c, d) -> l1(a + d, b - 1, c, d) [ c >= b ]
		(?, 1)    l1(a, b, c, d) -> l3(a, b, c, d) [ b <= 0 ]
		(?, 1)    l3(a, b, c, d) -> l3(a - 1, b, c, d) [ a > 0 ]
	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) [ c < b ]
	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) [ c < b ]
		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) [ c < b ]
	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) [ c < b ]
		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 > 0 ]
		(?, 1)    l3(a, b, c, d) -> l3(a - 1, b, c, d) [ a > 0 ]
		(?, 1)    l1(a, b, c, d) -> l3(a, b, c, d) [ b <= 0 ]
		(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
  For symbol l3: -X_2 >= 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) -> l3(a, b, c, d) [ b <= 0 ]
		(?, 1)    l3(a, b, c, d) -> l3(a - 1, b, c, d) [ -b >= 0 /\ a > 0 ]
		(?, 1)    l1(a, b, c, d) -> inner_10000_in_sep(a, b, 0, 0) [ b > 0 ]
		(?, 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) -> l3(a, b, c, d) [ b <= 0 ]
		(?, 1)    l3(a, b, c, d) -> l3(a - 1, b, c, d) [ -b >= 0 /\ a > 0 ]
		(?, 1)    l1(a, b, c, d) -> inner_10000_in_sep(a, b, 0, 0) [ b > 0 ]
		(?, 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) = 1
	Pol(l1) = 1
	Pol(l3) = -1
	Pol(inner_10000_in_sep) = 1
	Pol(inner_10000_out_sep) = 1
	Pol(inner_10000_compl_sep) = 1
orients all transitions weakly and the transition
	l1(a, b, c, d) -> l3(a, b, c, d) [ b <= 0 ]
strictly and produces the following problem:
5:	T:
		(1, 1)    l0(a, b, c, d) -> l1(0, b, c, d)
		(1, 1)    l1(a, b, c, d) -> l3(a, b, c, d) [ b <= 0 ]
		(?, 1)    l3(a, b, c, d) -> l3(a - 1, b, c, d) [ -b >= 0 /\ a > 0 ]
		(?, 1)    l1(a, b, c, d) -> inner_10000_in_sep(a, b, 0, 0) [ b > 0 ]
		(?, 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(l3) = 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 > 0 ]
	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:
6:	T:
		(1, 1)          l0(a, b, c, d) -> l1(0, b, c, d)
		(1, 1)          l1(a, b, c, d) -> l3(a, b, c, d) [ b <= 0 ]
		(?, 1)          l3(a, b, c, d) -> l3(a - 1, b, c, d) [ -b >= 0 /\ a > 0 ]
		(4*b + 3, 1)    l1(a, b, c, d) -> inner_10000_in_sep(a, b, 0, 0) [ b > 0 ]
		(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

A polynomial rank function with
	Pol(l3) = V_1
and size complexities
	S("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 ]", 0-0) = 4*b + 8*b^2 + 4*b^3
	S("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 ]", 0-1) = b
	S("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 ]", 0-2) = 0
	S("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 ]", 0-3) = 0
	S("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-0) = 4*b + 8*b^2 + 4*b^3
	S("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-1) = b
	S("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-2) = 0
	S("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-3) = 0
	S("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-0) = 4*b + 8*b^2 + 4*b^3
	S("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-1) = b
	S("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-2) = b
	S("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-3) = b + b^2
	S("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-0) = 4*b + 8*b^2 + 4*b^3
	S("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-1) = b
	S("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-2) = b
	S("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-3) = b + b^2
	S("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-0) = 4*b + 8*b^2 + 4*b^3
	S("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-1) = b
	S("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-2) = b
	S("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-3) = b + b^2
	S("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-0) = 4*b + 8*b^2 + 4*b^3
	S("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-1) = b
	S("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-2) = b
	S("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-3) = b + b^2
	S("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-0) = 4*b + 8*b^2 + 4*b^3
	S("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-1) = b
	S("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-2) = b
	S("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-3) = b + b^2
	S("l1(a, b, c, d) -> inner_10000_in_sep(a, b, 0, 0) [ b > 0 ]", 0-0) = 4*b + 8*b^2 + 4*b^3
	S("l1(a, b, c, d) -> inner_10000_in_sep(a, b, 0, 0) [ b > 0 ]", 0-1) = b
	S("l1(a, b, c, d) -> inner_10000_in_sep(a, b, 0, 0) [ b > 0 ]", 0-2) = 0
	S("l1(a, b, c, d) -> inner_10000_in_sep(a, b, 0, 0) [ b > 0 ]", 0-3) = 0
	S("l3(a, b, c, d) -> l3(a - 1, b, c, d) [ -b >= 0 /\\ a > 0 ]", 0-0) = 4*b + 8*b^2 + 4*b^3
	S("l3(a, b, c, d) -> l3(a - 1, b, c, d) [ -b >= 0 /\\ a > 0 ]", 0-1) = b
	S("l3(a, b, c, d) -> l3(a - 1, b, c, d) [ -b >= 0 /\\ a > 0 ]", 0-2) = b + c
	S("l3(a, b, c, d) -> l3(a - 1, b, c, d) [ -b >= 0 /\\ a > 0 ]", 0-3) = d + b + b^2
	S("l1(a, b, c, d) -> l3(a, b, c, d) [ b <= 0 ]", 0-0) = 4*b + 8*b^2 + 4*b^3
	S("l1(a, b, c, d) -> l3(a, b, c, d) [ b <= 0 ]", 0-1) = b
	S("l1(a, b, c, d) -> l3(a, b, c, d) [ b <= 0 ]", 0-2) = b + c
	S("l1(a, b, c, d) -> l3(a, b, c, d) [ b <= 0 ]", 0-3) = d + b + b^2
	S("l0(a, b, c, d) -> l1(0, b, c, d)", 0-0) = 0
	S("l0(a, b, c, d) -> l1(0, b, c, d)", 0-1) = b
	S("l0(a, b, c, d) -> l1(0, b, c, d)", 0-2) = c
	S("l0(a, b, c, d) -> l1(0, b, c, d)", 0-3) = d
orients the transition
	l3(a, b, c, d) -> l3(a - 1, b, c, d) [ -b >= 0 /\ a > 0 ]
weakly and the transition
	l3(a, b, c, d) -> l3(a - 1, b, c, d) [ -b >= 0 /\ a > 0 ]
strictly and produces the following problem:
7:	T:
		(1, 1)                      l0(a, b, c, d) -> l1(0, b, c, d)
		(1, 1)                      l1(a, b, c, d) -> l3(a, b, c, d) [ b <= 0 ]
		(4*b + 8*b^2 + 4*b^3, 1)    l3(a, b, c, d) -> l3(a - 1, b, c, d) [ -b >= 0 /\ a > 0 ]
		(4*b + 3, 1)                l1(a, b, c, d) -> inner_10000_in_sep(a, b, 0, 0) [ b > 0 ]
		(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 15*b + 12*b^2 + 4*b^3 + 8

Time: 0.912 sec (SMT: 0.845 sec)