YES(?, 28*d + 7*g + 27)

Initial complexity problem:
1:	T:
		(1, 1)    evalfstart(a, b, c, d, e, f, g) -> evalfentryin(a, b, c, d, e, f, g)
		(?, 1)    evalfentryin(a, b, c, d, e, f, g) -> evalfbb5in(0, 0, 0, d, e, f, g)
		(?, 1)    evalfbb5in(a, b, c, d, e, f, g) -> evalfreturnin(a, b, c, d, e, f, g) [ c >= d ]
		(?, 1)    evalfbb5in(a, b, c, d, e, f, g) -> evalfbbin(a, b, c, d, c + 1, f, g) [ d >= c + 1 ]
		(?, 1)    evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ 0 >= h + 1 ]
		(?, 1)    evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ h >= 1 ]
		(?, 1)    evalfbbin(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, a, g)
		(?, 1)    evalfbb1in(a, b, c, d, e, f, g) -> evalfbb5in(a, f + 1, e, d, e, f, g) [ f >= g ]
		(?, 1)    evalfbb1in(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]
		(?, 1)    evalfbb3in(a, b, c, d, e, f, g) -> evalfbb5in(f + 1, b, e, d, e, f, g) [ f >= g ]
		(?, 1)    evalfbb3in(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]
		(?, 1)    evalfreturnin(a, b, c, d, e, f, g) -> evalfstop(a, b, c, d, e, f, g)
	start location:	evalfstart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalfstart(a, b, c, d, e, f, g) -> evalfentryin(a, b, c, d, e, f, g)
		(?, 1)    evalfentryin(a, b, c, d, e, f, g) -> evalfbb5in(0, 0, 0, d, e, f, g)
		(?, 1)    evalfbb5in(a, b, c, d, e, f, g) -> evalfbbin(a, b, c, d, c + 1, f, g) [ d >= c + 1 ]
		(?, 1)    evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ 0 >= h + 1 ]
		(?, 1)    evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ h >= 1 ]
		(?, 1)    evalfbbin(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, a, g)
		(?, 1)    evalfbb1in(a, b, c, d, e, f, g) -> evalfbb5in(a, f + 1, e, d, e, f, g) [ f >= g ]
		(?, 1)    evalfbb1in(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]
		(?, 1)    evalfbb3in(a, b, c, d, e, f, g) -> evalfbb5in(f + 1, b, e, d, e, f, g) [ f >= g ]
		(?, 1)    evalfbb3in(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]
	start location:	evalfstart
	leaf cost:	2

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

A polynomial rank function with
	Pol(evalfstart) = 3*V_7 - 1
	Pol(evalfentryin) = 3*V_7 - 1
	Pol(evalfbb5in) = -3*V_1 + 3*V_7 - 1
	Pol(evalfbbin) = -3*V_1 + 3*V_7 - 1
	Pol(evalfbb1in) = -3*V_1 + 3*V_7 - 1
	Pol(evalfbb3in) = -3*V_6 + 3*V_7 - 2
orients all transitions weakly and the transition
	evalfbb3in(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]
strictly and produces the following problem:
4:	T:
		(1, 1)          evalfstart(a, b, c, d, e, f, g) -> evalfentryin(a, b, c, d, e, f, g)
		(1, 1)          evalfentryin(a, b, c, d, e, f, g) -> evalfbb5in(0, 0, 0, d, e, f, g)
		(?, 1)          evalfbb5in(a, b, c, d, e, f, g) -> evalfbbin(a, b, c, d, c + 1, f, g) [ d >= c + 1 ]
		(?, 1)          evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ 0 >= h + 1 ]
		(?, 1)          evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ h >= 1 ]
		(?, 1)          evalfbbin(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, a, g)
		(?, 1)          evalfbb1in(a, b, c, d, e, f, g) -> evalfbb5in(a, f + 1, e, d, e, f, g) [ f >= g ]
		(?, 1)          evalfbb1in(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]
		(?, 1)          evalfbb3in(a, b, c, d, e, f, g) -> evalfbb5in(f + 1, b, e, d, e, f, g) [ f >= g ]
		(3*g + 1, 1)    evalfbb3in(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]
	start location:	evalfstart
	leaf cost:	2

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

Repeatedly propagating knowledge in problem 5 produces the following problem:
6:	T:
		(1, 1)                evalfstart(a, b, c, d, e, f, g) -> evalfentryin(a, b, c, d, e, f, g)
		(1, 1)                evalfentryin(a, b, c, d, e, f, g) -> evalfbb5in(0, 0, 0, d, e, f, g)
		(4*d + 3, 1)          evalfbb5in(a, b, c, d, e, f, g) -> evalfbbin(a, b, c, d, c + 1, f, g) [ d >= c + 1 ]
		(4*d + 3, 1)          evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ 0 >= h + 1 ]
		(4*d + 3, 1)          evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ h >= 1 ]
		(4*d + 3, 1)          evalfbbin(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, a, g)
		(?, 1)                evalfbb1in(a, b, c, d, e, f, g) -> evalfbb5in(a, f + 1, e, d, e, f, g) [ f >= g ]
		(?, 1)                evalfbb1in(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]
		(3*g + 4*d + 4, 1)    evalfbb3in(a, b, c, d, e, f, g) -> evalfbb5in(f + 1, b, e, d, e, f, g) [ f >= g ]
		(3*g + 1, 1)          evalfbb3in(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]
	start location:	evalfstart
	leaf cost:	2

A polynomial rank function with
	Pol(evalfbb1in) = 1
	Pol(evalfbb5in) = 0
and size complexities
	S("evalfbb3in(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]", 0-0) = 6*d + 6*g + 6480
	S("evalfbb3in(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]", 0-1) = ?
	S("evalfbb3in(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]", 0-2) = 4*d + 3072
	S("evalfbb3in(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]", 0-3) = d
	S("evalfbb3in(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]", 0-4) = 4*d + 48
	S("evalfbb3in(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]", 0-5) = 6*d + 6*g + 180
	S("evalfbb3in(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]", 0-6) = g
	S("evalfbb3in(a, b, c, d, e, f, g) -> evalfbb5in(f + 1, b, e, d, e, f, g) [ f >= g ]", 0-0) = 6*d + 6*g + 180
	S("evalfbb3in(a, b, c, d, e, f, g) -> evalfbb5in(f + 1, b, e, d, e, f, g) [ f >= g ]", 0-1) = ?
	S("evalfbb3in(a, b, c, d, e, f, g) -> evalfbb5in(f + 1, b, e, d, e, f, g) [ f >= g ]", 0-2) = 4*d + 48
	S("evalfbb3in(a, b, c, d, e, f, g) -> evalfbb5in(f + 1, b, e, d, e, f, g) [ f >= g ]", 0-3) = d
	S("evalfbb3in(a, b, c, d, e, f, g) -> evalfbb5in(f + 1, b, e, d, e, f, g) [ f >= g ]", 0-4) = 4*d + 192
	S("evalfbb3in(a, b, c, d, e, f, g) -> evalfbb5in(f + 1, b, e, d, e, f, g) [ f >= g ]", 0-5) = 6*d + 6*g + 1080
	S("evalfbb3in(a, b, c, d, e, f, g) -> evalfbb5in(f + 1, b, e, d, e, f, g) [ f >= g ]", 0-6) = g
	S("evalfbb1in(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]", 0-0) = 6*d + 6*g + 180
	S("evalfbb1in(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]", 0-1) = ?
	S("evalfbb1in(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]", 0-2) = 4*d + 3072
	S("evalfbb1in(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]", 0-3) = d
	S("evalfbb1in(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]", 0-4) = 4*d + 48
	S("evalfbb1in(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]", 0-5) = ?
	S("evalfbb1in(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]", 0-6) = g
	S("evalfbb1in(a, b, c, d, e, f, g) -> evalfbb5in(a, f + 1, e, d, e, f, g) [ f >= g ]", 0-0) = 6*d + 6*g + 180
	S("evalfbb1in(a, b, c, d, e, f, g) -> evalfbb5in(a, f + 1, e, d, e, f, g) [ f >= g ]", 0-1) = ?
	S("evalfbb1in(a, b, c, d, e, f, g) -> evalfbb5in(a, f + 1, e, d, e, f, g) [ f >= g ]", 0-2) = 4*d + 48
	S("evalfbb1in(a, b, c, d, e, f, g) -> evalfbb5in(a, f + 1, e, d, e, f, g) [ f >= g ]", 0-3) = d
	S("evalfbb1in(a, b, c, d, e, f, g) -> evalfbb5in(a, f + 1, e, d, e, f, g) [ f >= g ]", 0-4) = 4*d + 192
	S("evalfbb1in(a, b, c, d, e, f, g) -> evalfbb5in(a, f + 1, e, d, e, f, g) [ f >= g ]", 0-5) = ?
	S("evalfbb1in(a, b, c, d, e, f, g) -> evalfbb5in(a, f + 1, e, d, e, f, g) [ f >= g ]", 0-6) = g
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, a, g)", 0-0) = 6*d + 6*g + 1080
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, a, g)", 0-1) = ?
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, a, g)", 0-2) = 4*d + 768
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, a, g)", 0-3) = d
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, a, g)", 0-4) = 4*d + 48
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, a, g)", 0-5) = 6*d + 6*g + 180
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, a, g)", 0-6) = g
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ h >= 1 ]", 0-0) = 6*d + 6*g + 180
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ h >= 1 ]", 0-1) = ?
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ h >= 1 ]", 0-2) = 4*d + 768
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ h >= 1 ]", 0-3) = d
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ h >= 1 ]", 0-4) = 4*d + 48
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ h >= 1 ]", 0-5) = ?
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ h >= 1 ]", 0-6) = g
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ 0 >= h + 1 ]", 0-0) = 6*d + 6*g + 180
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ 0 >= h + 1 ]", 0-1) = ?
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ 0 >= h + 1 ]", 0-2) = 4*d + 768
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ 0 >= h + 1 ]", 0-3) = d
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ 0 >= h + 1 ]", 0-4) = 4*d + 48
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ 0 >= h + 1 ]", 0-5) = ?
	S("evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ 0 >= h + 1 ]", 0-6) = g
	S("evalfbb5in(a, b, c, d, e, f, g) -> evalfbbin(a, b, c, d, c + 1, f, g) [ d >= c + 1 ]", 0-0) = 6*d + 6*g + 180
	S("evalfbb5in(a, b, c, d, e, f, g) -> evalfbbin(a, b, c, d, c + 1, f, g) [ d >= c + 1 ]", 0-1) = ?
	S("evalfbb5in(a, b, c, d, e, f, g) -> evalfbbin(a, b, c, d, c + 1, f, g) [ d >= c + 1 ]", 0-2) = 4*d + 192
	S("evalfbb5in(a, b, c, d, e, f, g) -> evalfbbin(a, b, c, d, c + 1, f, g) [ d >= c + 1 ]", 0-3) = d
	S("evalfbb5in(a, b, c, d, e, f, g) -> evalfbbin(a, b, c, d, c + 1, f, g) [ d >= c + 1 ]", 0-4) = 4*d + 48
	S("evalfbb5in(a, b, c, d, e, f, g) -> evalfbbin(a, b, c, d, c + 1, f, g) [ d >= c + 1 ]", 0-5) = ?
	S("evalfbb5in(a, b, c, d, e, f, g) -> evalfbbin(a, b, c, d, c + 1, f, g) [ d >= c + 1 ]", 0-6) = g
	S("evalfentryin(a, b, c, d, e, f, g) -> evalfbb5in(0, 0, 0, d, e, f, g)", 0-0) = 0
	S("evalfentryin(a, b, c, d, e, f, g) -> evalfbb5in(0, 0, 0, d, e, f, g)", 0-1) = 0
	S("evalfentryin(a, b, c, d, e, f, g) -> evalfbb5in(0, 0, 0, d, e, f, g)", 0-2) = 0
	S("evalfentryin(a, b, c, d, e, f, g) -> evalfbb5in(0, 0, 0, d, e, f, g)", 0-3) = d
	S("evalfentryin(a, b, c, d, e, f, g) -> evalfbb5in(0, 0, 0, d, e, f, g)", 0-4) = e
	S("evalfentryin(a, b, c, d, e, f, g) -> evalfbb5in(0, 0, 0, d, e, f, g)", 0-5) = f
	S("evalfentryin(a, b, c, d, e, f, g) -> evalfbb5in(0, 0, 0, d, e, f, g)", 0-6) = g
	S("evalfstart(a, b, c, d, e, f, g) -> evalfentryin(a, b, c, d, e, f, g)", 0-0) = a
	S("evalfstart(a, b, c, d, e, f, g) -> evalfentryin(a, b, c, d, e, f, g)", 0-1) = b
	S("evalfstart(a, b, c, d, e, f, g) -> evalfentryin(a, b, c, d, e, f, g)", 0-2) = c
	S("evalfstart(a, b, c, d, e, f, g) -> evalfentryin(a, b, c, d, e, f, g)", 0-3) = d
	S("evalfstart(a, b, c, d, e, f, g) -> evalfentryin(a, b, c, d, e, f, g)", 0-4) = e
	S("evalfstart(a, b, c, d, e, f, g) -> evalfentryin(a, b, c, d, e, f, g)", 0-5) = f
	S("evalfstart(a, b, c, d, e, f, g) -> evalfentryin(a, b, c, d, e, f, g)", 0-6) = g
orients the transitions
	evalfbb1in(a, b, c, d, e, f, g) -> evalfbb5in(a, f + 1, e, d, e, f, g) [ f >= g ]
	evalfbb1in(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]
weakly and the transition
	evalfbb1in(a, b, c, d, e, f, g) -> evalfbb5in(a, f + 1, e, d, e, f, g) [ f >= g ]
strictly and produces the following problem:
7:	T:
		(1, 1)                evalfstart(a, b, c, d, e, f, g) -> evalfentryin(a, b, c, d, e, f, g)
		(1, 1)                evalfentryin(a, b, c, d, e, f, g) -> evalfbb5in(0, 0, 0, d, e, f, g)
		(4*d + 3, 1)          evalfbb5in(a, b, c, d, e, f, g) -> evalfbbin(a, b, c, d, c + 1, f, g) [ d >= c + 1 ]
		(4*d + 3, 1)          evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ 0 >= h + 1 ]
		(4*d + 3, 1)          evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ h >= 1 ]
		(4*d + 3, 1)          evalfbbin(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, a, g)
		(8*d + 6, 1)          evalfbb1in(a, b, c, d, e, f, g) -> evalfbb5in(a, f + 1, e, d, e, f, g) [ f >= g ]
		(?, 1)                evalfbb1in(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]
		(3*g + 4*d + 4, 1)    evalfbb3in(a, b, c, d, e, f, g) -> evalfbb5in(f + 1, b, e, d, e, f, g) [ f >= g ]
		(3*g + 1, 1)          evalfbb3in(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]
	start location:	evalfstart
	leaf cost:	2

A polynomial rank function with
	Pol(evalfstart) = V_7
	Pol(evalfentryin) = V_7
	Pol(evalfbb5in) = -V_2 + V_7
	Pol(evalfbbin) = -V_2 + V_7
	Pol(evalfbb1in) = -V_6 + V_7
	Pol(evalfbb3in) = -V_2 + V_7
orients all transitions weakly and the transition
	evalfbb1in(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]
strictly and produces the following problem:
8:	T:
		(1, 1)                evalfstart(a, b, c, d, e, f, g) -> evalfentryin(a, b, c, d, e, f, g)
		(1, 1)                evalfentryin(a, b, c, d, e, f, g) -> evalfbb5in(0, 0, 0, d, e, f, g)
		(4*d + 3, 1)          evalfbb5in(a, b, c, d, e, f, g) -> evalfbbin(a, b, c, d, c + 1, f, g) [ d >= c + 1 ]
		(4*d + 3, 1)          evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ 0 >= h + 1 ]
		(4*d + 3, 1)          evalfbbin(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, b, g) [ h >= 1 ]
		(4*d + 3, 1)          evalfbbin(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, a, g)
		(8*d + 6, 1)          evalfbb1in(a, b, c, d, e, f, g) -> evalfbb5in(a, f + 1, e, d, e, f, g) [ f >= g ]
		(g, 1)                evalfbb1in(a, b, c, d, e, f, g) -> evalfbb1in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]
		(3*g + 4*d + 4, 1)    evalfbb3in(a, b, c, d, e, f, g) -> evalfbb5in(f + 1, b, e, d, e, f, g) [ f >= g ]
		(3*g + 1, 1)          evalfbb3in(a, b, c, d, e, f, g) -> evalfbb3in(a, b, c, d, e, f + 1, g) [ g >= f + 1 ]
	start location:	evalfstart
	leaf cost:	2

Complexity upper bound 28*d + 7*g + 27

Time: 2.421 sec (SMT: 1.869 sec)