MAYBE

Initial complexity problem:
1:	T:
		(1, 1)    evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)
		(?, 1)    evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)
		(?, 1)    evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]
		(?, 1)    evalfbb8in(a, b, c, d, e, f) -> evalfreturnin(a, b, c, d, e, f) [ 0 >= b + 1 ]
		(?, 1)    evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]
		(?, 1)    evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]
		(?, 1)    evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]
		(?, 1)    evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]
		(?, 1)    evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)
		(?, 1)    evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)
		(?, 1)    evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)
		(?, 1)    evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]
		(?, 1)    evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]
		(?, 1)    evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]
		(?, 1)    evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)
		(?, 1)    evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)
		(?, 1)    evalfreturnin(a, b, c, d, e, f) -> evalfstop(a, b, c, d, e, f)
	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, e, f) -> evalfentryin(a, b, c, d, e, f)
		(?, 1)    evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)
		(?, 1)    evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]
		(?, 1)    evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]
		(?, 1)    evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]
		(?, 1)    evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]
		(?, 1)    evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]
		(?, 1)    evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)
		(?, 1)    evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)
		(?, 1)    evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)
		(?, 1)    evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]
		(?, 1)    evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]
		(?, 1)    evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]
		(?, 1)    evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]
		(?, 1)    evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)
		(?, 1)    evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)
	start location:	evalfstart
	leaf cost:	2

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

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

A polynomial rank function with
	Pol(evalfbb7in) = 1
	Pol(evalfbb8in) = 0
	Pol(evalfbb5in) = 1
	Pol(evalfbb6in) = 1
	Pol(evalfbb4in) = 2
	Pol(evalfbb3in) = 3
	Pol(evalfbb1in) = 3
	Pol(evalfbb2in) = 3
and size complexities
	S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)", 0-0) = ?
	S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)", 0-1) = ?
	S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)", 0-2) = ?
	S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)", 0-3) = ?
	S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)", 0-4) = ?
	S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)", 0-5) = f
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)", 0-0) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)", 0-1) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)", 0-2) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)", 0-3) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)", 0-4) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)", 0-5) = f
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]", 0-0) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]", 0-1) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]", 0-2) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]", 0-3) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]", 0-4) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]", 0-5) = f
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-0) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-1) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-2) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-3) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-4) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-5) = f
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]", 0-0) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]", 0-1) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]", 0-2) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]", 0-3) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]", 0-4) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]", 0-5) = f
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]", 0-0) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]", 0-1) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]", 0-2) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]", 0-3) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]", 0-4) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]", 0-5) = f
	S("evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)", 0-0) = ?
	S("evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)", 0-1) = ?
	S("evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)", 0-2) = ?
	S("evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)", 0-3) = ?
	S("evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)", 0-4) = ?
	S("evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)", 0-5) = f
	S("evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)", 0-0) = ?
	S("evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)", 0-1) = ?
	S("evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)", 0-2) = ?
	S("evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)", 0-3) = ?
	S("evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)", 0-4) = ?
	S("evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)", 0-5) = f
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)", 0-0) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)", 0-1) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)", 0-2) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)", 0-3) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)", 0-4) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)", 0-5) = f
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]", 0-0) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]", 0-1) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]", 0-2) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]", 0-3) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]", 0-4) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]", 0-5) = f
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-0) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-1) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-2) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-3) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-4) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-5) = f
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]", 0-0) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]", 0-1) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]", 0-2) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]", 0-3) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]", 0-4) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]", 0-5) = f
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]", 0-0) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]", 0-1) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]", 0-2) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]", 0-3) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]", 0-4) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]", 0-5) = f
	S("evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]", 0-0) = ?
	S("evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]", 0-1) = ?
	S("evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]", 0-2) = ?
	S("evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]", 0-3) = ?
	S("evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]", 0-4) = ?
	S("evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]", 0-5) = f
	S("evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)", 0-0) = b
	S("evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)", 0-1) = a
	S("evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)", 0-2) = c
	S("evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)", 0-3) = d
	S("evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)", 0-4) = e
	S("evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)", 0-5) = f
	S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-0) = a
	S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-1) = b
	S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-2) = c
	S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-3) = d
	S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-4) = e
	S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-5) = f
orients the transitions
	evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)
	evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]
	evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]
	evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]
	evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]
	evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)
	evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)
	evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)
	evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]
	evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]
	evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]
	evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]
	evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)
weakly and the transitions
	evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)
	evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)
	evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)
	evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]
strictly and produces the following problem:
5:	T:
		(1, 1)           evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)
		(1, 1)           evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)
		(5*a + 1, 1)     evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]
		(15*a + 3, 1)    evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]
		(?, 1)           evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]
		(?, 1)           evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]
		(?, 1)           evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]
		(15*a + 3, 1)    evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)
		(?, 1)           evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)
		(15*a + 3, 1)    evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)
		(?, 1)           evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]
		(?, 1)           evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]
		(?, 1)           evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]
		(?, 1)           evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]
		(15*a + 3, 1)    evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)
		(?, 1)           evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)
	start location:	evalfstart
	leaf cost:	2

A polynomial rank function with
	Pol(evalfbb7in) = 1
	Pol(evalfbb5in) = 1
	Pol(evalfbb6in) = 1
	Pol(evalfbb8in) = 0
	Pol(evalfbb3in) = -1
	Pol(evalfbb1in) = -1
	Pol(evalfbb2in) = -1
and size complexities
	S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)", 0-0) = ?
	S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)", 0-1) = 16*a + 196608
	S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)", 0-2) = ?
	S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)", 0-3) = 16*a + 768
	S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)", 0-4) = ?
	S("evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)", 0-5) = f
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)", 0-0) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)", 0-1) = 16*a + 768
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)", 0-2) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)", 0-3) = 16*a + 12288
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)", 0-4) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)", 0-5) = f
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]", 0-0) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]", 0-1) = 16*a + 196608
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]", 0-2) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]", 0-3) = 16*a + 768
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]", 0-4) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]", 0-5) = f
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-0) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-1) = 16*a + 196608
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-2) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-3) = 16*a + 768
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-4) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-5) = f
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]", 0-0) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]", 0-1) = 16*a + 196608
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]", 0-2) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]", 0-3) = 16*a + 768
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]", 0-4) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]", 0-5) = f
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]", 0-0) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]", 0-1) = 16*a + 768
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]", 0-2) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]", 0-3) = 16*a + 12288
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]", 0-4) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]", 0-5) = f
	S("evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)", 0-0) = ?
	S("evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)", 0-1) = 16*a + 12288
	S("evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)", 0-2) = ?
	S("evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)", 0-3) = 16*a + 768
	S("evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)", 0-4) = ?
	S("evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)", 0-5) = f
	S("evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)", 0-0) = ?
	S("evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)", 0-1) = 16*a + 768
	S("evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)", 0-2) = ?
	S("evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)", 0-3) = 16*a + 16*d + 3145728
	S("evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)", 0-4) = ?
	S("evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)", 0-5) = f
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)", 0-0) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)", 0-1) = 16*a + 768
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)", 0-2) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)", 0-3) = 16*a + 16*d + 50331648
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)", 0-4) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)", 0-5) = f
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]", 0-0) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]", 0-1) = 16*a + 768
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]", 0-2) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]", 0-3) = 16*a + 16*d + 3145728
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]", 0-4) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]", 0-5) = f
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-0) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-1) = 16*a + 768
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-2) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-3) = 16*a + 16*d + 3145728
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-4) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]", 0-5) = f
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]", 0-0) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]", 0-1) = 16*a + 768
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]", 0-2) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]", 0-3) = 16*a + 16*d + 3145728
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]", 0-4) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]", 0-5) = f
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]", 0-0) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]", 0-1) = 16*a + 768
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]", 0-2) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]", 0-3) = 16*a + 16*d + 50331648
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]", 0-4) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]", 0-5) = f
	S("evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]", 0-0) = ?
	S("evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]", 0-1) = 16*a + 768
	S("evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]", 0-2) = ?
	S("evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]", 0-3) = 16*a + 16*d + 196608
	S("evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]", 0-4) = ?
	S("evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]", 0-5) = f
	S("evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)", 0-0) = b
	S("evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)", 0-1) = a
	S("evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)", 0-2) = c
	S("evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)", 0-3) = d
	S("evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)", 0-4) = e
	S("evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)", 0-5) = f
	S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-0) = a
	S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-1) = b
	S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-2) = c
	S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-3) = d
	S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-4) = e
	S("evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)", 0-5) = f
orients the transitions
	evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]
	evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]
	evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]
	evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]
	evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)
	evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]
	evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]
	evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]
	evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)
weakly and the transition
	evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]
strictly and produces the following problem:
6:	T:
		(1, 1)           evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)
		(1, 1)           evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)
		(5*a + 1, 1)     evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]
		(15*a + 3, 1)    evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ 0 >= c + 1 ]
		(?, 1)           evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ c >= 0 ]
		(?, 1)           evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ 0 >= g + 1 ]
		(?, 1)           evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ g >= 1 ]
		(15*a + 3, 1)    evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f)
		(?, 1)           evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f)
		(15*a + 3, 1)    evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f)
		(20*a + 4, 1)    evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ e >= f + 1 ]
		(?, 1)           evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ f >= e ]
		(?, 1)           evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ 0 >= g + 1 ]
		(?, 1)           evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ g >= 1 ]
		(15*a + 3, 1)    evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f)
		(?, 1)           evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f)
	start location:	evalfstart
	leaf cost:	2

Applied AI with 'oct' on problem 6 to obtain the following invariants:
  For symbol evalfbb1in: X_1 - X_3 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol evalfbb2in: X_1 - X_3 >= 0 /\ X_2 >= 0
  For symbol evalfbb3in: X_1 - X_3 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol evalfbb4in: X_1 - X_3 >= 0 /\ X_2 >= 0
  For symbol evalfbb5in: -X_5 + X_6 >= 0 /\ -X_3 + X_6 >= 0 /\ -X_3 + X_5 >= 0 /\ X_2 - X_4 - 1 >= 0 /\ X_4 + 1 >= 0 /\ X_2 + X_4 + 1 >= 0 /\ -X_2 + X_4 + 1 >= 0 /\ X_1 - X_3 >= 0 /\ X_2 >= 0
  For symbol evalfbb6in: -X_3 + X_5 >= 0 /\ X_2 - X_4 - 1 >= 0 /\ X_4 + 1 >= 0 /\ X_2 + X_4 + 1 >= 0 /\ -X_2 + X_4 + 1 >= 0 /\ X_1 - X_3 >= 0 /\ X_2 >= 0
  For symbol evalfbb7in: -X_5 + X_6 >= 0 /\ -X_3 + X_6 >= 0 /\ -X_3 + X_5 >= 0 /\ X_2 - X_4 - 1 >= 0 /\ X_4 + 1 >= 0 /\ X_2 + X_4 + 1 >= 0 /\ -X_2 + X_4 + 1 >= 0 /\ X_1 - X_3 >= 0 /\ X_2 >= 0


This yielded the following problem:
7:	T:
		(?, 1)           evalfbb5in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 ]
		(15*a + 3, 1)    evalfbb7in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 ]
		(?, 1)           evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ g >= 1 ]
		(?, 1)           evalfbb7in(a, b, c, d, e, f) -> evalfbb5in(a, b, c, d, e, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 ]
		(?, 1)           evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ f >= e ]
		(20*a + 4, 1)    evalfbb6in(a, b, c, d, e, f) -> evalfbb8in(e, d, c, d, e, f) [ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ e >= f + 1 ]
		(15*a + 3, 1)    evalfbb4in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\ b >= 0 ]
		(?, 1)           evalfbb1in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(15*a + 3, 1)    evalfbb3in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(?, 1)           evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ g >= 1 ]
		(?, 1)           evalfbb3in(a, b, c, d, e, f) -> evalfbb1in(a, b, c, d, e, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= g + 1 ]
		(?, 1)           evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ a - c >= 0 /\ b >= 0 /\ c >= 0 ]
		(15*a + 3, 1)    evalfbb2in(a, b, c, d, e, f) -> evalfbb4in(a, b, c, d, e, f) [ a - c >= 0 /\ b >= 0 /\ 0 >= c + 1 ]
		(5*a + 1, 1)     evalfbb8in(a, b, c, d, e, f) -> evalfbb2in(a, b, a, d, e, f) [ b >= 0 ]
		(1, 1)           evalfentryin(a, b, c, d, e, f) -> evalfbb8in(b, a, c, d, e, f)
		(1, 1)           evalfstart(a, b, c, d, e, f) -> evalfentryin(a, b, c, d, e, f)
	start location:	evalfstart
	leaf cost:	2

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

A polynomial rank function with
	Pol(evalfbb7in) = 1
	Pol(evalfbb6in) = 1
	Pol(evalfbb2in) = -1
	Pol(evalfbb3in) = -1
and size complexities
	S("evalfstart(a, b, c, d, e, f) -> evalfbb2in(b, a, b, d, e, f) [ a >= 0 ]", 0-0) = b
	S("evalfstart(a, b, c, d, e, f) -> evalfbb2in(b, a, b, d, e, f) [ a >= 0 ]", 0-1) = a
	S("evalfstart(a, b, c, d, e, f) -> evalfbb2in(b, a, b, d, e, f) [ a >= 0 ]", 0-2) = b
	S("evalfstart(a, b, c, d, e, f) -> evalfbb2in(b, a, b, d, e, f) [ a >= 0 ]", 0-3) = d
	S("evalfstart(a, b, c, d, e, f) -> evalfbb2in(b, a, b, d, e, f) [ a >= 0 ]", 0-4) = e
	S("evalfstart(a, b, c, d, e, f) -> evalfbb2in(b, a, b, d, e, f) [ a >= 0 ]", 0-5) = f
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ a - c >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-0) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ a - c >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-1) = a + 2
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ a - c >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-2) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ a - c >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-3) = a + d + 2
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ a - c >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-4) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ a - c >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-5) = f
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\\ b >= 0 /\\ 0 >= c + 1 ]", 0-0) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\\ b >= 0 /\\ 0 >= c + 1 ]", 0-1) = a + 2
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\\ b >= 0 /\\ 0 >= c + 1 ]", 0-2) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\\ b >= 0 /\\ 0 >= c + 1 ]", 0-3) = a + 2
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\\ b >= 0 /\\ 0 >= c + 1 ]", 0-4) = ?
	S("evalfbb2in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\\ b >= 0 /\\ 0 >= c + 1 ]", 0-5) = f
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ 0 >= g + 1 ]", 0-0) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ 0 >= g + 1 ]", 0-1) = a + 2
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ 0 >= g + 1 ]", 0-2) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ 0 >= g + 1 ]", 0-3) = a + d + 2
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ 0 >= g + 1 ]", 0-4) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ 0 >= g + 1 ]", 0-5) = f
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ g >= 1 ]", 0-0) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ g >= 1 ]", 0-1) = a + 2
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ g >= 1 ]", 0-2) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ g >= 1 ]", 0-3) = a + d + 2
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ g >= 1 ]", 0-4) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ g >= 1 ]", 0-5) = f
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 ]", 0-0) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 ]", 0-1) = a + 2
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 ]", 0-2) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 ]", 0-3) = a + 2
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 ]", 0-4) = ?
	S("evalfbb3in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 ]", 0-5) = f
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ f >= e ]", 0-0) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ f >= e ]", 0-1) = a + 2
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ f >= e ]", 0-2) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ f >= e ]", 0-3) = a + 2
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ f >= e ]", 0-4) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ f >= e ]", 0-5) = f
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ e >= f + 1 /\\ d >= 0 ]", 0-0) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ e >= f + 1 /\\ d >= 0 ]", 0-1) = a + 2
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ e >= f + 1 /\\ d >= 0 ]", 0-2) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ e >= f + 1 /\\ d >= 0 ]", 0-3) = a + 2
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ e >= f + 1 /\\ d >= 0 ]", 0-4) = ?
	S("evalfbb6in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ e >= f + 1 /\\ d >= 0 ]", 0-5) = f
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ d >= 0 ]", 0-0) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ d >= 0 ]", 0-1) = a + 2
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ d >= 0 ]", 0-2) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ d >= 0 ]", 0-3) = a + 2
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ d >= 0 ]", 0-4) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ d >= 0 ]", 0-5) = f
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ g >= 1 ]", 0-0) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ g >= 1 ]", 0-1) = a + 2
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ g >= 1 ]", 0-2) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ g >= 1 ]", 0-3) = a + 2
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ g >= 1 ]", 0-4) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ g >= 1 ]", 0-5) = f
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ 0 >= g + 1 /\\ -c + e + 1 >= 0 /\\ f >= e + 1 ]", 0-0) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ 0 >= g + 1 /\\ -c + e + 1 >= 0 /\\ f >= e + 1 ]", 0-1) = a + 2
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ 0 >= g + 1 /\\ -c + e + 1 >= 0 /\\ f >= e + 1 ]", 0-2) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ 0 >= g + 1 /\\ -c + e + 1 >= 0 /\\ f >= e + 1 ]", 0-3) = a + 2
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ 0 >= g + 1 /\\ -c + e + 1 >= 0 /\\ f >= e + 1 ]", 0-4) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ 0 >= g + 1 /\\ -c + e + 1 >= 0 /\\ f >= e + 1 ]", 0-5) = f
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e + 1, d, e + 1, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ 0 >= g + 1 /\\ -c + e + 1 >= 0 /\\ e + 1 >= f + 1 /\\ d >= 0 ]", 0-0) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e + 1, d, e + 1, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ 0 >= g + 1 /\\ -c + e + 1 >= 0 /\\ e + 1 >= f + 1 /\\ d >= 0 ]", 0-1) = a + 2
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e + 1, d, e + 1, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ 0 >= g + 1 /\\ -c + e + 1 >= 0 /\\ e + 1 >= f + 1 /\\ d >= 0 ]", 0-2) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e + 1, d, e + 1, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ 0 >= g + 1 /\\ -c + e + 1 >= 0 /\\ e + 1 >= f + 1 /\\ d >= 0 ]", 0-3) = a + 2
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e + 1, d, e + 1, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ 0 >= g + 1 /\\ -c + e + 1 >= 0 /\\ e + 1 >= f + 1 /\\ d >= 0 ]", 0-4) = ?
	S("evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e + 1, d, e + 1, d, e + 1, f) [ -e + f >= 0 /\\ -c + f >= 0 /\\ -c + e >= 0 /\\ b - d - 1 >= 0 /\\ d + 1 >= 0 /\\ b + d + 1 >= 0 /\\ -b + d + 1 >= 0 /\\ a - c >= 0 /\\ b >= 0 /\\ 0 >= g + 1 /\\ -c + e + 1 >= 0 /\\ e + 1 >= f + 1 /\\ d >= 0 ]", 0-5) = f
orients the transitions
	evalfbb7in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ f >= e + 1 ]
	evalfbb7in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ g >= 1 ]
	evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e + 1, d, e + 1, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ e + 1 >= f + 1 /\ d >= 0 ]
	evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ f >= e ]
	evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ g >= 1 ]
	evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= g + 1 ]
	evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ a - c >= 0 /\ b >= 0 /\ c >= 0 ]
weakly and the transition
	evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e + 1, d, e + 1, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ e + 1 >= f + 1 /\ d >= 0 ]
strictly and produces the following problem:
24:	T:
		(65*a + 14, 4)    evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e + 1, d, e + 1, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ e + 1 >= f + 1 /\ d >= 0 ]
		(?, 3)            evalfbb7in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ f >= e + 1 ]
		(?, 2)            evalfbb7in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ g >= 1 ]
		(15*a + 3, 2)     evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ d >= 0 ]
		(20*a + 4, 2)     evalfbb6in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ e >= f + 1 /\ d >= 0 ]
		(?, 1)            evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ f >= e ]
		(15*a + 3, 2)     evalfbb3in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(?, 2)            evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ g >= 1 ]
		(?, 2)            evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= g + 1 ]
		(15*a + 3, 2)     evalfbb2in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\ b >= 0 /\ 0 >= c + 1 ]
		(?, 1)            evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ a - c >= 0 /\ b >= 0 /\ c >= 0 ]
		(1, 3)            evalfstart(a, b, c, d, e, f) -> evalfbb2in(b, a, b, d, e, f) [ a >= 0 ]
	start location:	evalfstart
	leaf cost:	2

By chaining the transition evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e + 1, d, e + 1, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ e + 1 >= f + 1 /\ d >= 0 ] with all transitions in problem 24, the following new transitions are obtained:
	evalfbb7in(a, b, c, d, e, f) -> evalfbb6in(e + 1, d, e + 1, d - 1, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ e + 1 >= f + 1 /\ d >= 0 /\ 0 >= 0 /\ 0 >= e + 2 ]
	evalfbb7in(a, b, c, d, e, f) -> evalfbb3in(e + 1, d, e + 1, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ e + 1 >= f + 1 /\ d >= 0 /\ 0 >= 0 /\ e + 1 >= 0 ]
We thus obtain the following problem:
25:	T:
		(65*a + 14, 6)    evalfbb7in(a, b, c, d, e, f) -> evalfbb6in(e + 1, d, e + 1, d - 1, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ e + 1 >= f + 1 /\ d >= 0 /\ 0 >= 0 /\ 0 >= e + 2 ]
		(65*a + 14, 5)    evalfbb7in(a, b, c, d, e, f) -> evalfbb3in(e + 1, d, e + 1, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ e + 1 >= f + 1 /\ d >= 0 /\ 0 >= 0 /\ e + 1 >= 0 ]
		(?, 3)            evalfbb7in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ f >= e + 1 ]
		(?, 2)            evalfbb7in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ g >= 1 ]
		(15*a + 3, 2)     evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ d >= 0 ]
		(20*a + 4, 2)     evalfbb6in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ e >= f + 1 /\ d >= 0 ]
		(?, 1)            evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ f >= e ]
		(15*a + 3, 2)     evalfbb3in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(?, 2)            evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ g >= 1 ]
		(?, 2)            evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= g + 1 ]
		(15*a + 3, 2)     evalfbb2in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\ b >= 0 /\ 0 >= c + 1 ]
		(?, 1)            evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ a - c >= 0 /\ b >= 0 /\ c >= 0 ]
		(1, 3)            evalfstart(a, b, c, d, e, f) -> evalfbb2in(b, a, b, d, e, f) [ a >= 0 ]
	start location:	evalfstart
	leaf cost:	2

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

By chaining the transition evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e + 1, d - 1, e + 1, d - 1, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ e + 1 >= f + 1 /\ d >= 0 /\ 0 >= 0 /\ 0 >= e + 2 /\ 2*d >= 0 /\ d - 1 >= 0 ] with all transitions in problem 26, the following new transition is obtained:
	evalfbb7in(a, b, c, d, e, f) -> evalfbb6in(e + 1, d - 1, e + 1, d - 2, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ e + 1 >= f + 1 /\ d >= 0 /\ 0 >= 0 /\ 0 >= e + 2 /\ 2*d >= 0 /\ d - 1 >= 0 ]
We thus obtain the following problem:
27:	T:
		(65*a + 14, 10)    evalfbb7in(a, b, c, d, e, f) -> evalfbb6in(e + 1, d - 1, e + 1, d - 2, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ e + 1 >= f + 1 /\ d >= 0 /\ 0 >= 0 /\ 0 >= e + 2 /\ 2*d >= 0 /\ d - 1 >= 0 ]
		(65*a + 14, 5)     evalfbb7in(a, b, c, d, e, f) -> evalfbb3in(e + 1, d, e + 1, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ e + 1 >= f + 1 /\ d >= 0 /\ 0 >= 0 /\ e + 1 >= 0 ]
		(?, 3)             evalfbb7in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ f >= e + 1 ]
		(?, 2)             evalfbb7in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ g >= 1 ]
		(15*a + 3, 2)      evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ d >= 0 ]
		(20*a + 4, 2)      evalfbb6in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ e >= f + 1 /\ d >= 0 ]
		(?, 1)             evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ f >= e ]
		(15*a + 3, 2)      evalfbb3in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(?, 2)             evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ g >= 1 ]
		(?, 2)             evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= g + 1 ]
		(15*a + 3, 2)      evalfbb2in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\ b >= 0 /\ 0 >= c + 1 ]
		(?, 1)             evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ a - c >= 0 /\ b >= 0 /\ c >= 0 ]
		(1, 3)             evalfstart(a, b, c, d, e, f) -> evalfbb2in(b, a, b, d, e, f) [ a >= 0 ]
	start location:	evalfstart
	leaf cost:	2

By chaining the transition evalfbb7in(a, b, c, d, e, f) -> evalfbb6in(e + 1, d - 1, e + 1, d - 2, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ e + 1 >= f + 1 /\ d >= 0 /\ 0 >= 0 /\ 0 >= e + 2 /\ 2*d >= 0 /\ d - 1 >= 0 ] with all transitions in problem 27, the following new transition is obtained:
	evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e + 1, d - 2, e + 1, d - 2, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ e + 1 >= f + 1 /\ d >= 0 /\ 0 >= 0 /\ 0 >= e + 2 /\ 2*d >= 0 /\ d - 1 >= 0 /\ 2*d - 2 >= 0 /\ d - 2 >= 0 ]
We thus obtain the following problem:
28:	T:
		(65*a + 14, 12)    evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e + 1, d - 2, e + 1, d - 2, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ e + 1 >= f + 1 /\ d >= 0 /\ 0 >= 0 /\ 0 >= e + 2 /\ 2*d >= 0 /\ d - 1 >= 0 /\ 2*d - 2 >= 0 /\ d - 2 >= 0 ]
		(65*a + 14, 5)     evalfbb7in(a, b, c, d, e, f) -> evalfbb3in(e + 1, d, e + 1, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ e + 1 >= f + 1 /\ d >= 0 /\ 0 >= 0 /\ e + 1 >= 0 ]
		(?, 3)             evalfbb7in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ 0 >= g + 1 /\ -c + e + 1 >= 0 /\ f >= e + 1 ]
		(?, 2)             evalfbb7in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, d, e + 1, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ g >= 1 ]
		(15*a + 3, 2)      evalfbb7in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -e + f >= 0 /\ -c + f >= 0 /\ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ d >= 0 ]
		(20*a + 4, 2)      evalfbb6in(a, b, c, d, e, f) -> evalfbb2in(e, d, e, d, e, f) [ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ e >= f + 1 /\ d >= 0 ]
		(?, 1)             evalfbb6in(a, b, c, d, e, f) -> evalfbb7in(a, b, c, d, e, f) [ -c + e >= 0 /\ b - d - 1 >= 0 /\ d + 1 >= 0 /\ b + d + 1 >= 0 /\ -b + d + 1 >= 0 /\ a - c >= 0 /\ b >= 0 /\ f >= e ]
		(15*a + 3, 2)      evalfbb3in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(?, 2)             evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ g >= 1 ]
		(?, 2)             evalfbb3in(a, b, c, d, e, f) -> evalfbb2in(a, b, c - 1, d, e, f) [ a - c >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ 0 >= g + 1 ]
		(15*a + 3, 2)      evalfbb2in(a, b, c, d, e, f) -> evalfbb6in(a, b, c, b - 1, c, f) [ a - c >= 0 /\ b >= 0 /\ 0 >= c + 1 ]
		(?, 1)             evalfbb2in(a, b, c, d, e, f) -> evalfbb3in(a, b, c, d, e, f) [ a - c >= 0 /\ b >= 0 /\ c >= 0 ]
		(1, 3)             evalfstart(a, b, c, d, e, f) -> evalfbb2in(b, a, b, d, e, f) [ a >= 0 ]
	start location:	evalfstart
	leaf cost:	2

Complexity upper bound ?

Time: 5.157 sec (SMT: 4.607 sec)