MAYBE

Initial complexity problem:
1:	T:
		(1, 1)    evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)
		(?, 1)    evalfentryin(a, b, c, d) -> evalfbb7in(0, b, c, d)
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfreturnin(a, b, c, d) [ b^3 >= 0 /\ 0 >= b^3 /\ a >= 0 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfreturnin(a, b, c, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ a >= e ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfreturnin(a, b, c, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ a >= e /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb6in(a, b, c, d) [ c >= b ]
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbb2in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbb4in(a, b, c, d) [ d >= c ]
		(?, 1)    evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1)
		(?, 1)    evalfbb4in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d)
		(?, 1)    evalfbb6in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d)
		(?, 1)    evalfreturnin(a, b, c, d) -> evalfstop(a, b, c, d)
	start location:	evalfstart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)
		(?, 1)    evalfentryin(a, b, c, d) -> evalfbb7in(0, b, c, d)
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb6in(a, b, c, d) [ c >= b ]
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbb2in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbb4in(a, b, c, d) [ d >= c ]
		(?, 1)    evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1)
		(?, 1)    evalfbb4in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d)
		(?, 1)    evalfbb6in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d)
	start location:	evalfstart
	leaf cost:	4

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)
		(1, 1)    evalfentryin(a, b, c, d) -> evalfbb7in(0, b, c, d)
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb6in(a, b, c, d) [ c >= b ]
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbb2in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbb4in(a, b, c, d) [ d >= c ]
		(?, 1)    evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1)
		(?, 1)    evalfbb4in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d)
		(?, 1)    evalfbb6in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d)
	start location:	evalfstart
	leaf cost:	4

A polynomial rank function with
	Pol(evalfstart) = -2
	Pol(evalfentryin) = -2
	Pol(evalfbb7in) = -3*V_1 - 2
	Pol(evalfbb5in) = -3*V_1 - 3
	Pol(evalfbb3in) = -3*V_1 - 3
	Pol(evalfbb6in) = -3*V_1 - 4
	Pol(evalfbb2in) = -3*V_1 - 3
	Pol(evalfbb4in) = -3*V_1 - 3
orients all transitions weakly and the transitions
	evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
	evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
strictly and produces the following problem:
4:	T:
		(1, 1)    evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)
		(1, 1)    evalfentryin(a, b, c, d) -> evalfbb7in(0, b, c, d)
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb6in(a, b, c, d) [ c >= b ]
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbb2in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbb4in(a, b, c, d) [ d >= c ]
		(?, 1)    evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1)
		(?, 1)    evalfbb4in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d)
		(?, 1)    evalfbb6in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d)
	start location:	evalfstart
	leaf cost:	4

By chaining the transition evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d) with all transitions in problem 4, the following new transition is obtained:
	evalfstart(a, b, c, d) -> evalfbb7in(0, b, c, d)
We thus obtain the following problem:
5:	T:
		(1, 2)    evalfstart(a, b, c, d) -> evalfbb7in(0, b, c, d)
		(1, 1)    evalfentryin(a, b, c, d) -> evalfbb7in(0, b, c, d)
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb6in(a, b, c, d) [ c >= b ]
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbb2in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbb4in(a, b, c, d) [ d >= c ]
		(?, 1)    evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1)
		(?, 1)    evalfbb4in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d)
		(?, 1)    evalfbb6in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d)
	start location:	evalfstart
	leaf cost:	4

Testing for reachability in the complexity graph removes the following transition from problem 5:
	evalfentryin(a, b, c, d) -> evalfbb7in(0, b, c, d)
We thus obtain the following problem:
6:	T:
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 1)    evalfbb4in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d)
		(?, 1)    evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1)
		(?, 1)    evalfbb6in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d)
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbb4in(a, b, c, d) [ d >= c ]
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbb2in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb6in(a, b, c, d) [ c >= b ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
		(1, 2)    evalfstart(a, b, c, d) -> evalfbb7in(0, b, c, d)
	start location:	evalfstart
	leaf cost:	4

By chaining the transition evalfbb3in(a, b, c, d) -> evalfbb4in(a, b, c, d) [ d >= c ] with all transitions in problem 6, the following new transition is obtained:
	evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
We thus obtain the following problem:
7:	T:
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 1)    evalfbb4in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d)
		(?, 1)    evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1)
		(?, 1)    evalfbb6in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d)
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbb2in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb6in(a, b, c, d) [ c >= b ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
		(1, 2)    evalfstart(a, b, c, d) -> evalfbb7in(0, b, c, d)
	start location:	evalfstart
	leaf cost:	4

Testing for reachability in the complexity graph removes the following transition from problem 7:
	evalfbb4in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d)
We thus obtain the following problem:
8:	T:
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 1)    evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1)
		(?, 1)    evalfbb6in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d)
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbb2in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb6in(a, b, c, d) [ c >= b ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
		(1, 2)    evalfstart(a, b, c, d) -> evalfbb7in(0, b, c, d)
	start location:	evalfstart
	leaf cost:	4

By chaining the transition evalfbb3in(a, b, c, d) -> evalfbb2in(a, b, c, d) [ c >= d + 1 ] with all transitions in problem 8, the following new transition is obtained:
	evalfbb3in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1) [ c >= d + 1 ]
We thus obtain the following problem:
9:	T:
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1) [ c >= d + 1 ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 1)    evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1)
		(?, 1)    evalfbb6in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d)
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb6in(a, b, c, d) [ c >= b ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
		(1, 2)    evalfstart(a, b, c, d) -> evalfbb7in(0, b, c, d)
	start location:	evalfstart
	leaf cost:	4

Testing for reachability in the complexity graph removes the following transition from problem 9:
	evalfbb2in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1)
We thus obtain the following problem:
10:	T:
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 1)    evalfbb6in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d)
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1) [ c >= d + 1 ]
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb6in(a, b, c, d) [ c >= b ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
		(1, 2)    evalfstart(a, b, c, d) -> evalfbb7in(0, b, c, d)
	start location:	evalfstart
	leaf cost:	4

By chaining the transition evalfbb5in(a, b, c, d) -> evalfbb6in(a, b, c, d) [ c >= b ] with all transitions in problem 10, the following new transition is obtained:
	evalfbb5in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d) [ c >= b ]
We thus obtain the following problem:
11:	T:
		(?, 2)    evalfbb5in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d) [ c >= b ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 1)    evalfbb6in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d)
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1) [ c >= d + 1 ]
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
		(1, 2)    evalfstart(a, b, c, d) -> evalfbb7in(0, b, c, d)
	start location:	evalfstart
	leaf cost:	4

Testing for reachability in the complexity graph removes the following transition from problem 11:
	evalfbb6in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d)
We thus obtain the following problem:
12:	T:
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1) [ c >= d + 1 ]
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(?, 2)    evalfbb5in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d) [ c >= b ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
		(1, 2)    evalfstart(a, b, c, d) -> evalfbb7in(0, b, c, d)
	start location:	evalfstart
	leaf cost:	4

By chaining the transition evalfstart(a, b, c, d) -> evalfbb7in(0, b, c, d) with all transitions in problem 12, the following new transition is obtained:
	evalfstart(a, b, c, d) -> evalfbb5in(0, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 ]
We thus obtain the following problem:
13:	T:
		(1, 3)    evalfstart(a, b, c, d) -> evalfbb5in(0, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1) [ c >= d + 1 ]
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(?, 2)    evalfbb5in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d) [ c >= b ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
	start location:	evalfstart
	leaf cost:	4

By chaining the transition evalfstart(a, b, c, d) -> evalfbb5in(0, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 ] with all transitions in problem 13, the following new transitions are obtained:
	evalfstart(a, b, c, d) -> evalfbb7in(1, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b ]
	evalfstart(a, b, c, d) -> evalfbb3in(0, b, 0, 0) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ b >= 1 ]
We thus obtain the following problem:
14:	T:
		(1, 5)    evalfstart(a, b, c, d) -> evalfbb7in(1, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b ]
		(1, 4)    evalfstart(a, b, c, d) -> evalfbb3in(0, b, 0, 0) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ b >= 1 ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1) [ c >= d + 1 ]
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(?, 2)    evalfbb5in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d) [ c >= b ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
	start location:	evalfstart
	leaf cost:	4

By chaining the transition evalfstart(a, b, c, d) -> evalfbb7in(1, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b ] with all transitions in problem 14, the following new transition is obtained:
	evalfstart(a, b, c, d) -> evalfbb5in(1, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 ]
We thus obtain the following problem:
15:	T:
		(1, 6)    evalfstart(a, b, c, d) -> evalfbb5in(1, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 ]
		(1, 4)    evalfstart(a, b, c, d) -> evalfbb3in(0, b, 0, 0) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ b >= 1 ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1) [ c >= d + 1 ]
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(?, 2)    evalfbb5in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d) [ c >= b ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
	start location:	evalfstart
	leaf cost:	4

By chaining the transition evalfstart(a, b, c, d) -> evalfbb5in(1, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 ] with all transitions in problem 15, the following new transition is obtained:
	evalfstart(a, b, c, d) -> evalfbb7in(2, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 ]
We thus obtain the following problem:
16:	T:
		(1, 8)    evalfstart(a, b, c, d) -> evalfbb7in(2, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 ]
		(1, 4)    evalfstart(a, b, c, d) -> evalfbb3in(0, b, 0, 0) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ b >= 1 ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1) [ c >= d + 1 ]
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(?, 2)    evalfbb5in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d) [ c >= b ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
	start location:	evalfstart
	leaf cost:	4

By chaining the transition evalfstart(a, b, c, d) -> evalfbb7in(2, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 ] with all transitions in problem 16, the following new transition is obtained:
	evalfstart(a, b, c, d) -> evalfbb5in(2, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 ]
We thus obtain the following problem:
17:	T:
		(1, 9)    evalfstart(a, b, c, d) -> evalfbb5in(2, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 ]
		(1, 4)    evalfstart(a, b, c, d) -> evalfbb3in(0, b, 0, 0) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ b >= 1 ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1) [ c >= d + 1 ]
		(?, 2)    evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(?, 2)    evalfbb5in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d) [ c >= b ]
		(?, 1)    evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
	start location:	evalfstart
	leaf cost:	4

By chaining the transition evalfstart(a, b, c, d) -> evalfbb5in(2, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 ] with all transitions in problem 17, the following new transition is obtained:
	evalfstart(a, b, c, d) -> evalfbb7in(3, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 ]
We thus obtain the following problem:
18:	T:
		(1, 11)    evalfstart(a, b, c, d) -> evalfbb7in(3, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 ]
		(1, 4)     evalfstart(a, b, c, d) -> evalfbb3in(0, b, 0, 0) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ b >= 1 ]
		(2, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 2)     evalfbb3in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1) [ c >= d + 1 ]
		(?, 2)     evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(?, 2)     evalfbb5in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d) [ c >= b ]
		(?, 1)     evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
	start location:	evalfstart
	leaf cost:	4

By chaining the transition evalfstart(a, b, c, d) -> evalfbb7in(3, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 ] with all transitions in problem 18, the following new transition is obtained:
	evalfstart(a, b, c, d) -> evalfbb5in(3, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 /\ e''' >= 0 /\ b^3 >= 2*e''' /\ 2*e''' + 1 >= b^3 /\ e''' >= 4 ]
We thus obtain the following problem:
19:	T:
		(1, 12)    evalfstart(a, b, c, d) -> evalfbb5in(3, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 /\ e''' >= 0 /\ b^3 >= 2*e''' /\ 2*e''' + 1 >= b^3 /\ e''' >= 4 ]
		(1, 4)     evalfstart(a, b, c, d) -> evalfbb3in(0, b, 0, 0) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ b >= 1 ]
		(2, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 2)     evalfbb3in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1) [ c >= d + 1 ]
		(?, 2)     evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(?, 2)     evalfbb5in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d) [ c >= b ]
		(?, 1)     evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
	start location:	evalfstart
	leaf cost:	4

By chaining the transition evalfstart(a, b, c, d) -> evalfbb5in(3, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 /\ e''' >= 0 /\ b^3 >= 2*e''' /\ 2*e''' + 1 >= b^3 /\ e''' >= 4 ] with all transitions in problem 19, the following new transition is obtained:
	evalfstart(a, b, c, d) -> evalfbb7in(4, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 /\ e''' >= 0 /\ b^3 >= 2*e''' /\ 2*e''' + 1 >= b^3 /\ e''' >= 4 ]
We thus obtain the following problem:
20:	T:
		(1, 14)    evalfstart(a, b, c, d) -> evalfbb7in(4, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 /\ e''' >= 0 /\ b^3 >= 2*e''' /\ 2*e''' + 1 >= b^3 /\ e''' >= 4 ]
		(1, 4)     evalfstart(a, b, c, d) -> evalfbb3in(0, b, 0, 0) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ b >= 1 ]
		(2, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 2)     evalfbb3in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1) [ c >= d + 1 ]
		(?, 2)     evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(?, 2)     evalfbb5in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d) [ c >= b ]
		(?, 1)     evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
	start location:	evalfstart
	leaf cost:	4

By chaining the transition evalfstart(a, b, c, d) -> evalfbb7in(4, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 /\ e''' >= 0 /\ b^3 >= 2*e''' /\ 2*e''' + 1 >= b^3 /\ e''' >= 4 ] with all transitions in problem 20, the following new transition is obtained:
	evalfstart(a, b, c, d) -> evalfbb5in(4, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 /\ e''' >= 0 /\ b^3 >= 2*e''' /\ 2*e''' + 1 >= b^3 /\ e''' >= 4 /\ e'''' >= 0 /\ b^3 >= 2*e'''' /\ 2*e'''' + 1 >= b^3 /\ e'''' >= 5 ]
We thus obtain the following problem:
21:	T:
		(1, 15)    evalfstart(a, b, c, d) -> evalfbb5in(4, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 /\ e''' >= 0 /\ b^3 >= 2*e''' /\ 2*e''' + 1 >= b^3 /\ e''' >= 4 /\ e'''' >= 0 /\ b^3 >= 2*e'''' /\ 2*e'''' + 1 >= b^3 /\ e'''' >= 5 ]
		(1, 4)     evalfstart(a, b, c, d) -> evalfbb3in(0, b, 0, 0) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ b >= 1 ]
		(2, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 2)     evalfbb3in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1) [ c >= d + 1 ]
		(?, 2)     evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(?, 2)     evalfbb5in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d) [ c >= b ]
		(?, 1)     evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
	start location:	evalfstart
	leaf cost:	4

By chaining the transition evalfstart(a, b, c, d) -> evalfbb5in(4, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 /\ e''' >= 0 /\ b^3 >= 2*e''' /\ 2*e''' + 1 >= b^3 /\ e''' >= 4 /\ e'''' >= 0 /\ b^3 >= 2*e'''' /\ 2*e'''' + 1 >= b^3 /\ e'''' >= 5 ] with all transitions in problem 21, the following new transition is obtained:
	evalfstart(a, b, c, d) -> evalfbb7in(5, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 /\ e''' >= 0 /\ b^3 >= 2*e''' /\ 2*e''' + 1 >= b^3 /\ e''' >= 4 /\ e'''' >= 0 /\ b^3 >= 2*e'''' /\ 2*e'''' + 1 >= b^3 /\ e'''' >= 5 ]
We thus obtain the following problem:
22:	T:
		(1, 17)    evalfstart(a, b, c, d) -> evalfbb7in(5, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 /\ e''' >= 0 /\ b^3 >= 2*e''' /\ 2*e''' + 1 >= b^3 /\ e''' >= 4 /\ e'''' >= 0 /\ b^3 >= 2*e'''' /\ 2*e'''' + 1 >= b^3 /\ e'''' >= 5 ]
		(1, 4)     evalfstart(a, b, c, d) -> evalfbb3in(0, b, 0, 0) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ b >= 1 ]
		(2, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 2)     evalfbb3in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1) [ c >= d + 1 ]
		(?, 2)     evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(?, 2)     evalfbb5in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d) [ c >= b ]
		(?, 1)     evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
	start location:	evalfstart
	leaf cost:	4

By chaining the transition evalfstart(a, b, c, d) -> evalfbb7in(5, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 /\ e''' >= 0 /\ b^3 >= 2*e''' /\ 2*e''' + 1 >= b^3 /\ e''' >= 4 /\ e'''' >= 0 /\ b^3 >= 2*e'''' /\ 2*e'''' + 1 >= b^3 /\ e'''' >= 5 ] with all transitions in problem 22, the following new transition is obtained:
	evalfstart(a, b, c, d) -> evalfbb5in(5, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 /\ e''' >= 0 /\ b^3 >= 2*e''' /\ 2*e''' + 1 >= b^3 /\ e''' >= 4 /\ e'''' >= 0 /\ b^3 >= 2*e'''' /\ 2*e'''' + 1 >= b^3 /\ e'''' >= 5 /\ e''''' >= 0 /\ b^3 >= 2*e''''' /\ 2*e''''' + 1 >= b^3 /\ e''''' >= 6 ]
We thus obtain the following problem:
23:	T:
		(1, 18)    evalfstart(a, b, c, d) -> evalfbb5in(5, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ 0 >= b /\ e' >= 0 /\ b^3 >= 2*e' /\ 2*e' + 1 >= b^3 /\ e' >= 2 /\ e'' >= 0 /\ b^3 >= 2*e'' /\ 2*e'' + 1 >= b^3 /\ e'' >= 3 /\ e''' >= 0 /\ b^3 >= 2*e''' /\ 2*e''' + 1 >= b^3 /\ e''' >= 4 /\ e'''' >= 0 /\ b^3 >= 2*e'''' /\ 2*e'''' + 1 >= b^3 /\ e'''' >= 5 /\ e''''' >= 0 /\ b^3 >= 2*e''''' /\ 2*e''''' + 1 >= b^3 /\ e''''' >= 6 ]
		(1, 4)     evalfstart(a, b, c, d) -> evalfbb3in(0, b, 0, 0) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= 1 /\ b >= 1 ]
		(2, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ 0 >= b^3 + 1 /\ 0 >= e /\ e >= a + 1 /\ 2*e >= b^3 /\ b^3 + 1 >= 2*e ]
		(2, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 0 /\ 0 >= b^3 /\ 0 >= a + 1 ]
		(?, 2)     evalfbb3in(a, b, c, d) -> evalfbb3in(a, b, c, d + 1) [ c >= d + 1 ]
		(?, 2)     evalfbb3in(a, b, c, d) -> evalfbb5in(a, b, c + 1, d) [ d >= c ]
		(?, 2)     evalfbb5in(a, b, c, d) -> evalfbb7in(a + 1, b, c, d) [ c >= b ]
		(?, 1)     evalfbb5in(a, b, c, d) -> evalfbb3in(a, b, c, 0) [ b >= c + 1 ]
		(?, 1)     evalfbb7in(a, b, c, d) -> evalfbb5in(a, b, 0, d) [ b^3 >= 1 /\ e >= 0 /\ b^3 >= 2*e /\ 2*e + 1 >= b^3 /\ e >= a + 1 ]
	start location:	evalfstart
	leaf cost:	4

Complexity upper bound ?

Time: 6.173 sec (SMT: 5.266 sec)