YES(?, 236*a + 8*c + 352*a*b + 5)

Initial complexity problem:
1:	T:
		(1, 1)    evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)
		(?, 1)    evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\ b >= 0 /\ c >= 0 ]
		(?, 1)    evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopreturnin(a, b, c, d, e, f, g, h) [ d >= a ]
		(?, 1)    evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]
		(?, 1)    evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]
		(?, 1)    evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]
		(?, 1)    evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopreturnin(a, b, c, d, e, f, g, h)
		(?, 1)    evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]
		(?, 1)    evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]
		(?, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(?, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(?, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)
		(?, 1)    evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)
		(?, 1)    evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]
		(?, 1)    evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]
		(?, 1)    evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(?, 1)    evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(?, 1)    evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)
		(?, 1)    evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)
		(?, 1)    evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)
		(?, 1)    evalNestedLoopreturnin(a, b, c, d, e, f, g, h) -> evalNestedLoopstop(a, b, c, d, e, f, g, h)
	start location:	evalNestedLoopstart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)
		(?, 1)    evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\ b >= 0 /\ c >= 0 ]
		(?, 1)    evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]
		(?, 1)    evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]
		(?, 1)    evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]
		(?, 1)    evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]
		(?, 1)    evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]
		(?, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(?, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(?, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)
		(?, 1)    evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)
		(?, 1)    evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]
		(?, 1)    evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]
		(?, 1)    evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(?, 1)    evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(?, 1)    evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)
		(?, 1)    evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)
		(?, 1)    evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)
	start location:	evalNestedLoopstart
	leaf cost:	3

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)
		(1, 1)    evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\ b >= 0 /\ c >= 0 ]
		(?, 1)    evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]
		(?, 1)    evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]
		(?, 1)    evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]
		(?, 1)    evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]
		(?, 1)    evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]
		(?, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(?, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(?, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)
		(?, 1)    evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)
		(?, 1)    evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]
		(?, 1)    evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]
		(?, 1)    evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(?, 1)    evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(?, 1)    evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)
		(?, 1)    evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)
		(?, 1)    evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)
	start location:	evalNestedLoopstart
	leaf cost:	3

A polynomial rank function with
	Pol(evalNestedLoopstart) = 4*V_1
	Pol(evalNestedLoopentryin) = 4*V_1
	Pol(evalNestedLoopbb9in) = 4*V_1 - 4*V_4
	Pol(evalNestedLoopbb10in) = 4*V_1 - 4*V_4 - 1
	Pol(evalNestedLoopbb6in) = 4*V_1 - 4*V_6 - 2
	Pol(evalNestedLoopbb8in) = 4*V_1 - 4*V_6 - 3
	Pol(evalNestedLoopbb7in) = 4*V_1 - 4*V_6 - 2
	Pol(evalNestedLoopbb1in) = 4*V_1 - 4*V_6 - 2
	Pol(evalNestedLoopbb3in) = 4*V_1 - 4*V_8 - 2
	Pol(evalNestedLoopbb4in) = 4*V_1 - 4*V_8 - 2
	Pol(evalNestedLoopbb2in) = 4*V_1 - 4*V_8 - 3
orients all transitions weakly and the transition
	evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]
strictly and produces the following problem:
4:	T:
		(1, 1)      evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)
		(1, 1)      evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\ b >= 0 /\ c >= 0 ]
		(4*a, 1)    evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]
		(?, 1)      evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]
		(?, 1)      evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]
		(?, 1)      evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]
		(?, 1)      evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]
		(?, 1)      evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(?, 1)      evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(?, 1)      evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)
		(?, 1)      evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)
		(?, 1)      evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]
		(?, 1)      evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]
		(?, 1)      evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(?, 1)      evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(?, 1)      evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)
		(?, 1)      evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)
		(?, 1)      evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)
	start location:	evalNestedLoopstart
	leaf cost:	3

Repeatedly propagating knowledge in problem 4 produces the following problem:
5:	T:
		(1, 1)      evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)
		(1, 1)      evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\ b >= 0 /\ c >= 0 ]
		(4*a, 1)    evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]
		(4*a, 1)    evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]
		(4*a, 1)    evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]
		(?, 1)      evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]
		(?, 1)      evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]
		(?, 1)      evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(?, 1)      evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(?, 1)      evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)
		(?, 1)      evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)
		(?, 1)      evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]
		(?, 1)      evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]
		(?, 1)      evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(?, 1)      evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(?, 1)      evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)
		(?, 1)      evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)
		(?, 1)      evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)
	start location:	evalNestedLoopstart
	leaf cost:	3

A polynomial rank function with
	Pol(evalNestedLoopbb8in) = 1
	Pol(evalNestedLoopbb9in) = 0
	Pol(evalNestedLoopbb7in) = 2
	Pol(evalNestedLoopbb1in) = 2
	Pol(evalNestedLoopbb6in) = 2
	Pol(evalNestedLoopbb4in) = 2
	Pol(evalNestedLoopbb2in) = 2
	Pol(evalNestedLoopbb3in) = 2
and size complexities
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-0) = a
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-1) = b
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-2) = c
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-3) = ?
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-4) = ?
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-5) = ?
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-6) = ?
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-7) = ?
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-0) = a
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-1) = b
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-2) = c
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-3) = ?
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-4) = ?
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-5) = ?
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-6) = ?
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-7) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-0) = a
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-1) = b
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-2) = c
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-3) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-4) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-5) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-6) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-7) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-0) = a
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-1) = b
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-2) = c
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-3) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-4) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-5) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-6) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-7) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-0) = a
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-1) = b
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-2) = c
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-3) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-4) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-5) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-6) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-7) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-0) = a
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-1) = b
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-2) = c
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-3) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-4) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-5) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-6) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-7) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-0) = a
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-1) = b
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-2) = c
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-3) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-4) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-5) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-6) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-7) = ?
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-0) = a
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-1) = b
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-2) = c
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-3) = ?
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-4) = ?
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-5) = ?
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-6) = ?
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-7) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-0) = a
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-1) = b
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-2) = c
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-3) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-4) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-5) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-6) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-7) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-0) = a
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-1) = b
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-2) = c
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-3) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-4) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-5) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-6) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-7) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-0) = a
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-1) = b
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-2) = c
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-3) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-4) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-5) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-6) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-7) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-0) = a
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-1) = b
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-2) = c
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-3) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-4) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-5) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-6) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-7) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-0) = a
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-1) = b
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-2) = c
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-3) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-4) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-5) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-6) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-7) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-0) = a
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-1) = b
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-2) = c
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-3) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-4) = 0
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-5) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-6) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-7) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-0) = a
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-1) = b
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-2) = c
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-3) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-4) = 0
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-5) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-6) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-7) = ?
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-0) = a
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-1) = b
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-2) = c
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-3) = ?
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-4) = ?
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-5) = ?
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-6) = ?
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-7) = ?
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-0) = a
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-1) = b
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-2) = c
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-3) = 0
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-4) = e
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-5) = f
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-6) = g
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-7) = h
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-0) = a
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-1) = b
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-2) = c
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-3) = d
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-4) = e
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-5) = f
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-6) = g
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-7) = h
orients the transitions
	evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)
	evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)
	evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]
	evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
	evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]
	evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]
	evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)
	evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]
	evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
	evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]
	evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]
	evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)
	evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)
weakly and the transitions
	evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)
	evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)
	evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]
strictly and produces the following problem:
6:	T:
		(1, 1)       evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)
		(1, 1)       evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\ b >= 0 /\ c >= 0 ]
		(4*a, 1)     evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]
		(4*a, 1)     evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]
		(4*a, 1)     evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]
		(16*a, 1)    evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]
		(?, 1)       evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]
		(?, 1)       evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(?, 1)       evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(16*a, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)
		(?, 1)       evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)
		(?, 1)       evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]
		(?, 1)       evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]
		(?, 1)       evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(?, 1)       evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(?, 1)       evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)
		(?, 1)       evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)
		(16*a, 1)    evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)
	start location:	evalNestedLoopstart
	leaf cost:	3

A polynomial rank function with
	Pol(evalNestedLoopbb7in) = 4*V_2 - 4*V_5 - 3
	Pol(evalNestedLoopbb1in) = 4*V_2 - 4*V_5 - 4
	Pol(evalNestedLoopbb6in) = 4*V_2 - 4*V_5 - 2
	Pol(evalNestedLoopbb4in) = 4*V_2 - 4*V_7 - 1
	Pol(evalNestedLoopbb2in) = 4*V_2 - 4*V_7 - 1
	Pol(evalNestedLoopbb3in) = 4*V_2 - 4*V_7 - 1
and size complexities
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-0) = a
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-1) = b
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-2) = c
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-3) = ?
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-4) = ?
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-5) = ?
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-6) = ?
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-7) = ?
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-0) = a
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-1) = b
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-2) = c
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-3) = ?
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-4) = ?
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-5) = ?
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-6) = ?
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-7) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-0) = a
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-1) = b
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-2) = c
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-3) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-4) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-5) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-6) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-7) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-0) = a
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-1) = b
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-2) = c
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-3) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-4) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-5) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-6) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-7) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-0) = a
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-1) = b
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-2) = c
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-3) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-4) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-5) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-6) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-7) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-0) = a
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-1) = b
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-2) = c
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-3) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-4) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-5) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-6) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-7) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-0) = a
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-1) = b
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-2) = c
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-3) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-4) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-5) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-6) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-7) = ?
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-0) = a
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-1) = b
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-2) = c
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-3) = ?
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-4) = ?
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-5) = ?
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-6) = ?
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-7) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-0) = a
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-1) = b
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-2) = c
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-3) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-4) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-5) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-6) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-7) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-0) = a
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-1) = b
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-2) = c
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-3) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-4) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-5) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-6) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-7) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-0) = a
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-1) = b
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-2) = c
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-3) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-4) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-5) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-6) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-7) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-0) = a
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-1) = b
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-2) = c
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-3) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-4) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-5) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-6) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-7) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-0) = a
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-1) = b
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-2) = c
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-3) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-4) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-5) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-6) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-7) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-0) = a
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-1) = b
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-2) = c
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-3) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-4) = 0
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-5) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-6) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-7) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-0) = a
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-1) = b
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-2) = c
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-3) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-4) = 0
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-5) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-6) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-7) = ?
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-0) = a
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-1) = b
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-2) = c
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-3) = ?
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-4) = ?
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-5) = ?
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-6) = ?
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-7) = ?
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-0) = a
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-1) = b
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-2) = c
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-3) = 0
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-4) = e
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-5) = f
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-6) = g
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-7) = h
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-0) = a
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-1) = b
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-2) = c
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-3) = d
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-4) = e
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-5) = f
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-6) = g
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-7) = h
orients the transitions
	evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]
	evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
	evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]
	evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)
	evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]
	evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
	evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]
	evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]
	evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)
	evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)
weakly and the transition
	evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]
strictly and produces the following problem:
7:	T:
		(1, 1)                evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)
		(1, 1)                evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\ b >= 0 /\ c >= 0 ]
		(4*a, 1)              evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]
		(4*a, 1)              evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]
		(4*a, 1)              evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]
		(16*a, 1)             evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]
		(32*a*b + 16*a, 1)    evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]
		(?, 1)                evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(?, 1)                evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(16*a, 1)             evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)
		(?, 1)                evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)
		(?, 1)                evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]
		(?, 1)                evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]
		(?, 1)                evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(?, 1)                evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(?, 1)                evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)
		(?, 1)                evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)
		(16*a, 1)             evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)
	start location:	evalNestedLoopstart
	leaf cost:	3

Repeatedly propagating knowledge in problem 7 produces the following problem:
8:	T:
		(1, 1)                evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)
		(1, 1)                evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\ b >= 0 /\ c >= 0 ]
		(4*a, 1)              evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]
		(4*a, 1)              evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]
		(4*a, 1)              evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]
		(16*a, 1)             evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]
		(32*a*b + 16*a, 1)    evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]
		(32*a*b + 16*a, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(32*a*b + 16*a, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(16*a, 1)             evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)
		(64*a*b + 32*a, 1)    evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)
		(?, 1)                evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]
		(?, 1)                evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]
		(?, 1)                evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(?, 1)                evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(?, 1)                evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)
		(?, 1)                evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)
		(16*a, 1)             evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)
	start location:	evalNestedLoopstart
	leaf cost:	3

A polynomial rank function with
	Pol(evalNestedLoopbb4in) = 1
	Pol(evalNestedLoopbb6in) = 0
	Pol(evalNestedLoopbb2in) = 1
	Pol(evalNestedLoopbb3in) = 1
and size complexities
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-0) = a
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-1) = b
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-2) = c
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-3) = ?
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-4) = 64*a*b + 32*a
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-5) = ?
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-6) = g + 64*a*b + 32*a
	S("evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)", 0-7) = ?
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-0) = a
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-1) = b
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-2) = c
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-3) = ?
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-4) = 64*a*b + 32*a
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-5) = ?
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-6) = 64*a*b + 32*a
	S("evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)", 0-7) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-0) = a
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-1) = b
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-2) = c
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-3) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-4) = 64*a*b + 32*a
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-5) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-6) = 64*a*b + 32*a
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)", 0-7) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-0) = a
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-1) = b
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-2) = c
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-3) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-4) = 64*a*b + 32*a
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-5) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-6) = 64*a*b + 32*a
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-7) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-0) = a
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-1) = b
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-2) = c
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-3) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-4) = 64*a*b + 32*a
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-5) = ?
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-6) = 64*a*b + 32*a
	S("evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-7) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-0) = a
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-1) = b
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-2) = c
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-3) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-4) = 64*a*b + 32*a
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-5) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-6) = 64*a*b + 32*a
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]", 0-7) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-0) = a
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-1) = b
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-2) = c
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-3) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-4) = 64*a*b + 32*a
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-5) = ?
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-6) = 64*a*b + 32*a
	S("evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]", 0-7) = ?
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-0) = a
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-1) = b
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-2) = c
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-3) = ?
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-4) = 64*a*b + 32*a
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-5) = ?
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-6) = 64*a*b + 32*a
	S("evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)", 0-7) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-0) = a
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-1) = b
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-2) = c
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-3) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-4) = 64*a*b + 32*a
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-5) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-6) = g + 64*a*b + 32*a
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)", 0-7) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-0) = a
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-1) = b
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-2) = c
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-3) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-4) = 64*a*b + 32*a
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-5) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-6) = g + 64*a*b + 32*a
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]", 0-7) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-0) = a
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-1) = b
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-2) = c
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-3) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-4) = 64*a*b + 32*a
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-5) = ?
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-6) = g + 64*a*b + 32*a
	S("evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]", 0-7) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-0) = a
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-1) = b
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-2) = c
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-3) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-4) = 64*a*b + 32*a
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-5) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-6) = g + 64*a*b + 32*a
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]", 0-7) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-0) = a
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-1) = b
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-2) = c
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-3) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-4) = 64*a*b + 32*a
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-5) = ?
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-6) = g + 64*a*b + 32*a
	S("evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]", 0-7) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-0) = a
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-1) = b
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-2) = c
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-3) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-4) = 0
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-5) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-6) = g + 64*a*b + 32*a
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]", 0-7) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-0) = a
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-1) = b
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-2) = c
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-3) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-4) = 0
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-5) = ?
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-6) = g + 64*a*b + 32*a
	S("evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]", 0-7) = ?
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-0) = a
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-1) = b
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-2) = c
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-3) = ?
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-4) = e + 64*a*b + 32*a
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-5) = ?
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-6) = g + 64*a*b + 32*a
	S("evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]", 0-7) = ?
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-0) = a
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-1) = b
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-2) = c
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-3) = 0
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-4) = e
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-5) = f
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-6) = g
	S("evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\\ b >= 0 /\\ c >= 0 ]", 0-7) = h
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-0) = a
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-1) = b
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-2) = c
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-3) = d
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-4) = e
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-5) = f
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-6) = g
	S("evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)", 0-7) = h
orients the transitions
	evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)
	evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]
	evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
	evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]
	evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]
	evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)
weakly and the transitions
	evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)
	evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]
strictly and produces the following problem:
9:	T:
		(1, 1)                evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)
		(1, 1)                evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\ b >= 0 /\ c >= 0 ]
		(4*a, 1)              evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ a >= d + 1 ]
		(4*a, 1)              evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ 0 >= i + 1 ]
		(4*a, 1)              evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ i >= 1 ]
		(16*a, 1)             evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ e >= b ]
		(32*a*b + 16*a, 1)    evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ b >= e + 1 ]
		(32*a*b + 16*a, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(32*a*b + 16*a, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(16*a, 1)             evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h)
		(64*a*b + 32*a, 1)    evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f)
		(64*a*b + 32*a, 1)    evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= c ]
		(?, 1)                evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ c >= h + 1 ]
		(?, 1)                evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ 0 >= i + 1 ]
		(?, 1)                evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ i >= 1 ]
		(64*a*b + 32*a, 1)    evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h)
		(?, 1)                evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1)
		(16*a, 1)             evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h)
	start location:	evalNestedLoopstart
	leaf cost:	3

Applied AI with 'oct' on problem 9 to obtain the following invariants:
  For symbol evalNestedLoopbb10in: X_1 - X_4 - 1 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ X_2 + X_4 >= 0 /\ X_1 + X_4 - 1 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 1 >= 0 /\ X_1 - 1 >= 0
  For symbol evalNestedLoopbb1in: X_6 >= 0 /\ X_5 + X_6 >= 0 /\ X_4 + X_6 >= 0 /\ -X_4 + X_6 >= 0 /\ X_3 + X_6 >= 0 /\ X_2 + X_6 - 1 >= 0 /\ X_1 + X_6 - 1 >= 0 /\ X_2 - X_5 - 1 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 >= 0 /\ X_3 + X_5 >= 0 /\ X_2 + X_5 - 1 >= 0 /\ X_1 + X_5 - 1 >= 0 /\ X_1 - X_4 - 1 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ X_2 + X_4 - 1 >= 0 /\ X_1 + X_4 - 1 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 1 >= 0
  For symbol evalNestedLoopbb2in: X_3 - X_8 - 1 >= 0 /\ X_8 >= 0 /\ X_7 + X_8 - 1 >= 0 /\ X_6 + X_8 >= 0 /\ -X_6 + X_8 >= 0 /\ X_5 + X_8 >= 0 /\ X_4 + X_8 >= 0 /\ -X_4 + X_8 >= 0 /\ X_3 + X_8 - 1 >= 0 /\ X_2 + X_8 - 1 >= 0 /\ X_1 + X_8 - 1 >= 0 /\ X_5 - X_7 + 1 >= 0 /\ X_2 - X_7 >= 0 /\ X_7 - 1 >= 0 /\ X_6 + X_7 - 1 >= 0 /\ X_5 + X_7 - 1 >= 0 /\ -X_5 + X_7 - 1 >= 0 /\ X_4 + X_7 - 1 >= 0 /\ X_3 + X_7 - 2 >= 0 /\ X_2 + X_7 - 2 >= 0 /\ X_1 + X_7 - 2 >= 0 /\ X_3 - X_6 - 1 >= 0 /\ X_6 >= 0 /\ X_5 + X_6 >= 0 /\ X_4 + X_6 >= 0 /\ -X_4 + X_6 >= 0 /\ X_3 + X_6 - 1 >= 0 /\ X_2 + X_6 - 1 >= 0 /\ X_1 + X_6 - 1 >= 0 /\ X_2 - X_5 - 1 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 >= 0 /\ X_3 + X_5 - 1 >= 0 /\ X_2 + X_5 - 1 >= 0 /\ X_1 + X_5 - 1 >= 0 /\ X_3 - X_4 - 1 >= 0 /\ X_1 - X_4 - 1 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 - 1 >= 0 /\ X_2 + X_4 - 1 >= 0 /\ X_1 + X_4 - 1 >= 0 /\ X_3 - 1 >= 0 /\ X_2 + X_3 - 2 >= 0 /\ X_1 + X_3 - 2 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 1 >= 0
  For symbol evalNestedLoopbb3in: X_8 >= 0 /\ X_7 + X_8 - 1 >= 0 /\ X_6 + X_8 >= 0 /\ -X_6 + X_8 >= 0 /\ X_5 + X_8 >= 0 /\ X_4 + X_8 >= 0 /\ -X_4 + X_8 >= 0 /\ X_3 + X_8 >= 0 /\ X_2 + X_8 - 1 >= 0 /\ X_1 + X_8 - 1 >= 0 /\ X_5 - X_7 + 1 >= 0 /\ X_2 - X_7 >= 0 /\ X_7 - 1 >= 0 /\ X_6 + X_7 - 1 >= 0 /\ X_5 + X_7 - 1 >= 0 /\ -X_5 + X_7 - 1 >= 0 /\ X_4 + X_7 - 1 >= 0 /\ X_3 + X_7 - 1 >= 0 /\ X_2 + X_7 - 2 >= 0 /\ X_1 + X_7 - 2 >= 0 /\ X_6 >= 0 /\ X_5 + X_6 >= 0 /\ X_4 + X_6 >= 0 /\ -X_4 + X_6 >= 0 /\ X_3 + X_6 >= 0 /\ X_2 + X_6 - 1 >= 0 /\ X_1 + X_6 - 1 >= 0 /\ X_2 - X_5 - 1 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 >= 0 /\ X_3 + X_5 >= 0 /\ X_2 + X_5 - 1 >= 0 /\ X_1 + X_5 - 1 >= 0 /\ X_1 - X_4 - 1 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ X_2 + X_4 - 1 >= 0 /\ X_1 + X_4 - 1 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 1 >= 0
  For symbol evalNestedLoopbb4in: X_3 - X_8 - 1 >= 0 /\ X_8 >= 0 /\ X_7 + X_8 - 1 >= 0 /\ X_6 + X_8 >= 0 /\ -X_6 + X_8 >= 0 /\ X_5 + X_8 >= 0 /\ X_4 + X_8 >= 0 /\ -X_4 + X_8 >= 0 /\ X_3 + X_8 - 1 >= 0 /\ X_2 + X_8 - 1 >= 0 /\ X_1 + X_8 - 1 >= 0 /\ X_5 - X_7 + 1 >= 0 /\ X_2 - X_7 >= 0 /\ X_7 - 1 >= 0 /\ X_6 + X_7 - 1 >= 0 /\ X_5 + X_7 - 1 >= 0 /\ -X_5 + X_7 - 1 >= 0 /\ X_4 + X_7 - 1 >= 0 /\ X_3 + X_7 - 2 >= 0 /\ X_2 + X_7 - 2 >= 0 /\ X_1 + X_7 - 2 >= 0 /\ X_3 - X_6 - 1 >= 0 /\ X_6 >= 0 /\ X_5 + X_6 >= 0 /\ X_4 + X_6 >= 0 /\ -X_4 + X_6 >= 0 /\ X_3 + X_6 - 1 >= 0 /\ X_2 + X_6 - 1 >= 0 /\ X_1 + X_6 - 1 >= 0 /\ X_2 - X_5 - 1 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 >= 0 /\ X_3 + X_5 - 1 >= 0 /\ X_2 + X_5 - 1 >= 0 /\ X_1 + X_5 - 1 >= 0 /\ X_3 - X_4 - 1 >= 0 /\ X_1 - X_4 - 1 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 - 1 >= 0 /\ X_2 + X_4 - 1 >= 0 /\ X_1 + X_4 - 1 >= 0 /\ X_3 - 1 >= 0 /\ X_2 + X_3 - 2 >= 0 /\ X_1 + X_3 - 2 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 1 >= 0
  For symbol evalNestedLoopbb6in: X_6 >= 0 /\ X_5 + X_6 >= 0 /\ X_4 + X_6 >= 0 /\ -X_4 + X_6 >= 0 /\ X_3 + X_6 >= 0 /\ X_2 + X_6 >= 0 /\ X_1 + X_6 - 1 >= 0 /\ X_2 - X_5 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 >= 0 /\ X_3 + X_5 >= 0 /\ X_2 + X_5 >= 0 /\ X_1 + X_5 - 1 >= 0 /\ X_1 - X_4 - 1 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ X_2 + X_4 >= 0 /\ X_1 + X_4 - 1 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 1 >= 0 /\ X_1 - 1 >= 0
  For symbol evalNestedLoopbb7in: X_6 >= 0 /\ X_5 + X_6 >= 0 /\ X_4 + X_6 >= 0 /\ -X_4 + X_6 >= 0 /\ X_3 + X_6 >= 0 /\ X_2 + X_6 - 1 >= 0 /\ X_1 + X_6 - 1 >= 0 /\ X_2 - X_5 - 1 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 >= 0 /\ X_3 + X_5 >= 0 /\ X_2 + X_5 - 1 >= 0 /\ X_1 + X_5 - 1 >= 0 /\ X_1 - X_4 - 1 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ X_2 + X_4 - 1 >= 0 /\ X_1 + X_4 - 1 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 1 >= 0
  For symbol evalNestedLoopbb8in: X_6 >= 0 /\ X_5 + X_6 >= 0 /\ X_4 + X_6 >= 0 /\ -X_4 + X_6 >= 0 /\ X_3 + X_6 >= 0 /\ X_2 + X_6 >= 0 /\ X_1 + X_6 - 1 >= 0 /\ X_2 - X_5 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 >= 0 /\ X_3 + X_5 >= 0 /\ X_2 + X_5 >= 0 /\ X_1 + X_5 - 1 >= 0 /\ X_1 - X_4 - 1 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ X_2 + X_4 >= 0 /\ X_1 + X_4 - 1 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 1 >= 0 /\ X_1 - 1 >= 0
  For symbol evalNestedLoopbb9in: X_4 >= 0 /\ X_3 + X_4 >= 0 /\ X_2 + X_4 >= 0 /\ X_1 + X_4 >= 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


This yielded the following problem:
10:	T:
		(16*a, 1)             evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f >= 0 /\ a + f - 1 >= 0 /\ b - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 ]
		(?, 1)                evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1) [ c - h - 1 >= 0 /\ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h - 1 >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 2 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ c - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f - 1 >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e - 1 >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ c - d - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(64*a*b + 32*a, 1)    evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ c - h - 1 >= 0 /\ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h - 1 >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 2 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ c - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f - 1 >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e - 1 >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ c - d - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(?, 1)                evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ c - h - 1 >= 0 /\ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h - 1 >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 2 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ c - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f - 1 >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e - 1 >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ c - d - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ i >= 1 ]
		(?, 1)                evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ c - h - 1 >= 0 /\ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h - 1 >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 2 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ c - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f - 1 >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e - 1 >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ c - d - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ 0 >= i + 1 ]
		(?, 1)                evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 1 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= h + 1 ]
		(64*a*b + 32*a, 1)    evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 1 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ h >= c ]
		(64*a*b + 32*a, 1)    evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(16*a, 1)             evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(32*a*b + 16*a, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ i >= 1 ]
		(32*a*b + 16*a, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ 0 >= i + 1 ]
		(32*a*b + 16*a, 1)    evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f >= 0 /\ a + f - 1 >= 0 /\ b - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= e + 1 ]
		(16*a, 1)             evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f >= 0 /\ a + f - 1 >= 0 /\ b - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ e >= b ]
		(4*a, 1)              evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ i >= 1 ]
		(4*a, 1)              evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ 0 >= i + 1 ]
		(4*a, 1)              evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= d + 1 ]
		(1, 1)                evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\ b >= 0 /\ c >= 0 ]
		(1, 1)                evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)
	start location:	evalNestedLoopstart
	leaf cost:	3

A polynomial rank function with
	Pol(evalNestedLoopbb8in) = 2*V_3 - 2*V_6
	Pol(evalNestedLoopbb9in) = 2*V_3 - 2*V_4
	Pol(evalNestedLoopbb2in) = 2*V_3 - 2*V_8 - 1
	Pol(evalNestedLoopbb3in) = 2*V_3 - 2*V_8
	Pol(evalNestedLoopbb4in) = 2*V_3 - 2*V_8
	Pol(evalNestedLoopbb6in) = 2*V_3 - 2*V_6
	Pol(evalNestedLoopbb1in) = 2*V_3 - 2*V_6
	Pol(evalNestedLoopbb7in) = 2*V_3 - 2*V_6
	Pol(evalNestedLoopbb10in) = 2*V_3 - 2*V_4
	Pol(evalNestedLoopentryin) = 2*V_3
	Pol(evalNestedLoopstart) = 2*V_3
orients all transitions weakly and the transitions
	evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ c - h - 1 >= 0 /\ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h - 1 >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 2 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ c - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f - 1 >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e - 1 >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ c - d - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ i >= 1 ]
	evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ c - h - 1 >= 0 /\ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h - 1 >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 2 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ c - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f - 1 >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e - 1 >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ c - d - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ 0 >= i + 1 ]
	evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1) [ c - h - 1 >= 0 /\ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h - 1 >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 2 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ c - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f - 1 >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e - 1 >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ c - d - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
strictly and produces the following problem:
11:	T:
		(16*a, 1)             evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f >= 0 /\ a + f - 1 >= 0 /\ b - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 ]
		(2*c, 1)              evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1) [ c - h - 1 >= 0 /\ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h - 1 >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 2 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ c - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f - 1 >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e - 1 >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ c - d - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(64*a*b + 32*a, 1)    evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ c - h - 1 >= 0 /\ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h - 1 >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 2 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ c - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f - 1 >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e - 1 >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ c - d - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(2*c, 1)              evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ c - h - 1 >= 0 /\ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h - 1 >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 2 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ c - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f - 1 >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e - 1 >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ c - d - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ i >= 1 ]
		(2*c, 1)              evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ c - h - 1 >= 0 /\ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h - 1 >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 2 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ c - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f - 1 >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e - 1 >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ c - d - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ 0 >= i + 1 ]
		(?, 1)                evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 1 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= h + 1 ]
		(64*a*b + 32*a, 1)    evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 1 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ h >= c ]
		(64*a*b + 32*a, 1)    evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(16*a, 1)             evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(32*a*b + 16*a, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ i >= 1 ]
		(32*a*b + 16*a, 1)    evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ 0 >= i + 1 ]
		(32*a*b + 16*a, 1)    evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f >= 0 /\ a + f - 1 >= 0 /\ b - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= e + 1 ]
		(16*a, 1)             evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f >= 0 /\ a + f - 1 >= 0 /\ b - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ e >= b ]
		(4*a, 1)              evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ i >= 1 ]
		(4*a, 1)              evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ 0 >= i + 1 ]
		(4*a, 1)              evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= d + 1 ]
		(1, 1)                evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\ b >= 0 /\ c >= 0 ]
		(1, 1)                evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)
	start location:	evalNestedLoopstart
	leaf cost:	3

Repeatedly propagating knowledge in problem 11 produces the following problem:
12:	T:
		(16*a, 1)                   evalNestedLoopbb8in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, f + 1, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f >= 0 /\ a + f - 1 >= 0 /\ b - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 ]
		(2*c, 1)                    evalNestedLoopbb2in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, g, h + 1) [ c - h - 1 >= 0 /\ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h - 1 >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 2 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ c - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f - 1 >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e - 1 >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ c - d - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(64*a*b + 32*a, 1)          evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ c - h - 1 >= 0 /\ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h - 1 >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 2 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ c - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f - 1 >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e - 1 >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ c - d - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(2*c, 1)                    evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ c - h - 1 >= 0 /\ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h - 1 >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 2 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ c - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f - 1 >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e - 1 >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ c - d - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ i >= 1 ]
		(2*c, 1)                    evalNestedLoopbb4in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb2in(a, b, c, d, e, f, g, h) [ c - h - 1 >= 0 /\ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h - 1 >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 2 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ c - f - 1 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f - 1 >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e - 1 >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ c - d - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ a + c - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ 0 >= i + 1 ]
		(64*a*b + 32*a + 2*c, 1)    evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb4in(a, b, c, d, e, f, g, h) [ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 1 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= h + 1 ]
		(64*a*b + 32*a, 1)          evalNestedLoopbb3in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, g, h, g, h) [ h >= 0 /\ g + h - 1 >= 0 /\ f + h >= 0 /\ -f + h >= 0 /\ e + h >= 0 /\ d + h >= 0 /\ -d + h >= 0 /\ c + h >= 0 /\ b + h - 1 >= 0 /\ a + h - 1 >= 0 /\ e - g + 1 >= 0 /\ b - g >= 0 /\ g - 1 >= 0 /\ f + g - 1 >= 0 /\ e + g - 1 >= 0 /\ -e + g - 1 >= 0 /\ d + g - 1 >= 0 /\ c + g - 1 >= 0 /\ b + g - 2 >= 0 /\ a + g - 2 >= 0 /\ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ h >= c ]
		(64*a*b + 32*a, 1)          evalNestedLoopbb1in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb3in(a, b, c, d, e, f, e + 1, f) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(16*a, 1)                   evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(32*a*b + 16*a, 1)          evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ i >= 1 ]
		(32*a*b + 16*a, 1)          evalNestedLoopbb7in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb1in(a, b, c, d, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f - 1 >= 0 /\ a + f - 1 >= 0 /\ b - e - 1 >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ 0 >= i + 1 ]
		(32*a*b + 16*a, 1)          evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb7in(a, b, c, d, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f >= 0 /\ a + f - 1 >= 0 /\ b - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= e + 1 ]
		(16*a, 1)                   evalNestedLoopbb6in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb8in(a, b, c, d, e, f, g, h) [ f >= 0 /\ e + f >= 0 /\ d + f >= 0 /\ -d + f >= 0 /\ c + f >= 0 /\ b + f >= 0 /\ a + f - 1 >= 0 /\ b - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e - 1 >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ e >= b ]
		(4*a, 1)                    evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ i >= 1 ]
		(4*a, 1)                    evalNestedLoopbb10in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb6in(a, b, c, d, 0, d, g, h) [ a - d - 1 >= 0 /\ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d - 1 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ 0 >= i + 1 ]
		(4*a, 1)                    evalNestedLoopbb9in(a, b, c, d, e, f, g, h) -> evalNestedLoopbb10in(a, b, c, d, e, f, g, h) [ d >= 0 /\ c + d >= 0 /\ b + d >= 0 /\ a + d >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= d + 1 ]
		(1, 1)                      evalNestedLoopentryin(a, b, c, d, e, f, g, h) -> evalNestedLoopbb9in(a, b, c, 0, e, f, g, h) [ a >= 0 /\ b >= 0 /\ c >= 0 ]
		(1, 1)                      evalNestedLoopstart(a, b, c, d, e, f, g, h) -> evalNestedLoopentryin(a, b, c, d, e, f, g, h)
	start location:	evalNestedLoopstart
	leaf cost:	3

Complexity upper bound 236*a + 8*c + 352*a*b + 5

Time: 1.743 sec (SMT: 1.406 sec)