YES(?, 18*e + 55)

Initial complexity problem:
1:	T:
		(1, 1)    f0(a, b, c, d, e, f, g, h, i, j) -> f17(0, k, l, 0, e, f, g, h, i, j)
		(?, 1)    f17(a, b, c, d, e, f, g, h, i, j) -> f17(a, b, c, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]
		(?, 1)    f27(a, b, c, d, e, f, g, h, i, j) -> f27(a, b, c, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]
		(?, 1)    f37(a, b, c, d, e, f, g, h, i, j) -> f37(a, b, c, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]
		(?, 1)    f45(a, b, c, d, e, f, g, h, i, j) -> f45(a + 1, b, c, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(?, 1)    f55(a, b, c, d, e, f, g, h, i, j) -> f55(a, b, c, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]
		(?, 1)    f65(a, b, c, d, e, f, g, h, i, j) -> f65(a, b, c, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]
		(?, 1)    f75(a, b, c, d, e, f, g, h, i, j) -> f75(a, b, c, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]
		(?, 1)    f83(a, b, c, d, e, f, g, h, i, j) -> f83(a + 1, b, c, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(?, 1)    f83(a, b, c, d, e, f, g, h, i, j) -> f93(a, b, c, d, e, f, g, h, i, j) [ a >= e ]
		(?, 1)    f75(a, b, c, d, e, f, g, h, i, j) -> f83(0, b, c, d, e, f, g, h, i, j) [ j >= e ]
		(?, 1)    f65(a, b, c, d, e, f, g, h, i, j) -> f75(a, b, c, d, e, f, g, h, i, 0) [ i >= e ]
		(?, 1)    f55(a, b, c, d, e, f, g, h, i, j) -> f65(a, b, c, d, e, f, g, h, 0, j) [ h >= e ]
		(?, 1)    f45(a, b, c, d, e, f, g, h, i, j) -> f55(a, b, c, d, e, f, g, 0, i, j) [ a >= e ]
		(?, 1)    f37(a, b, c, d, e, f, g, h, i, j) -> f45(0, b, c, d, e, f, g, h, i, j) [ g >= e ]
		(?, 1)    f27(a, b, c, d, e, f, g, h, i, j) -> f37(a, b, c, d, e, f, 0, h, i, j) [ f >= e ]
		(?, 1)    f17(a, b, c, d, e, f, g, h, i, j) -> f27(a, b, c, d, e, 0, g, h, i, j) [ d >= e ]
	start location:	f0
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, d, e, f, g, h, i, j].
We thus obtain the following problem:
2:	T:
		(?, 1)    f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]
		(?, 1)    f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]
		(?, 1)    f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]
		(?, 1)    f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]
		(?, 1)    f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]
		(?, 1)    f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]
		(?, 1)    f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]
		(?, 1)    f83(a, d, e, f, g, h, i, j) -> f93(a, d, e, f, g, h, i, j) [ a >= e ]
		(?, 1)    f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(?, 1)    f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]
		(?, 1)    f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]
		(?, 1)    f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]
		(?, 1)    f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(?, 1)    f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]
		(?, 1)    f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]
		(?, 1)    f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]
		(1, 1)    f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)
	start location:	f0
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(?, 1)    f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]
		(?, 1)    f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]
		(?, 1)    f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]
		(?, 1)    f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]
		(?, 1)    f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]
		(?, 1)    f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]
		(?, 1)    f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]
		(?, 1)    f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(?, 1)    f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]
		(?, 1)    f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]
		(?, 1)    f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]
		(?, 1)    f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(?, 1)    f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]
		(?, 1)    f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]
		(?, 1)    f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]
		(1, 1)    f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f17) = 7
	Pol(f27) = 6
	Pol(f37) = 5
	Pol(f45) = 4
	Pol(f55) = 3
	Pol(f65) = 2
	Pol(f75) = 1
	Pol(f83) = -1
	Pol(f0) = 7
orients all transitions weakly and the transitions
	f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]
	f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]
	f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]
	f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]
	f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]
	f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]
	f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]
strictly and produces the following problem:
4:	T:
		(7, 1)    f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]
		(7, 1)    f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]
		(7, 1)    f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]
		(7, 1)    f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]
		(7, 1)    f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]
		(7, 1)    f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]
		(7, 1)    f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]
		(?, 1)    f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(?, 1)    f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]
		(?, 1)    f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]
		(?, 1)    f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]
		(?, 1)    f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(?, 1)    f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]
		(?, 1)    f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]
		(?, 1)    f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]
		(1, 1)    f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f17) = -V_2 + V_3
	Pol(f27) = -3*V_2 + 3*V_3 - V_4 - 2
	Pol(f37) = -3*V_2 + 3*V_3 - V_4 - V_5 - 2
	Pol(f45) = -3*V_2 + 3*V_3 - V_4 - V_5 - 2
	Pol(f55) = -3*V_2 + 3*V_3 - V_4 - V_5 - V_6 - 2
	Pol(f65) = -3*V_2 + 3*V_3 - V_4 - V_5 - V_6 - V_7 - 2
	Pol(f75) = -3*V_2 + 3*V_3 - V_4 - V_5 - V_6 - V_7 - V_8 - 2
	Pol(f83) = -V_1 - 3*V_2 + 3*V_3 - V_4 - V_5 - V_6 - V_7 - V_8 - 2
	Pol(f0) = V_3
orients all transitions weakly and the transition
	f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]
strictly and produces the following problem:
5:	T:
		(7, 1)    f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]
		(7, 1)    f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]
		(7, 1)    f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]
		(7, 1)    f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]
		(7, 1)    f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]
		(7, 1)    f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]
		(7, 1)    f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]
		(?, 1)    f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(?, 1)    f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]
		(?, 1)    f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]
		(?, 1)    f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]
		(?, 1)    f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(?, 1)    f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]
		(?, 1)    f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]
		(e, 1)    f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]
		(1, 1)    f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f17) = V_3
	Pol(f27) = V_3 - V_4
	Pol(f37) = V_3 - V_4 - V_5 - 2
	Pol(f45) = 3*V_3 - V_4 - 3*V_5 - 2
	Pol(f55) = 3*V_3 - V_4 - 3*V_5 - V_6 - 2
	Pol(f65) = 3*V_3 - V_4 - 3*V_5 - V_6 - V_7 - 2
	Pol(f75) = 3*V_3 - V_4 - 3*V_5 - V_6 - V_7 - V_8 - 2
	Pol(f83) = -V_1 + 3*V_3 - V_4 - 3*V_5 - V_6 - V_7 - V_8 - 2
	Pol(f0) = V_3
orients all transitions weakly and the transition
	f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]
strictly and produces the following problem:
6:	T:
		(7, 1)    f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]
		(7, 1)    f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]
		(7, 1)    f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]
		(7, 1)    f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]
		(7, 1)    f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]
		(7, 1)    f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]
		(7, 1)    f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]
		(?, 1)    f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(?, 1)    f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]
		(?, 1)    f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]
		(?, 1)    f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]
		(?, 1)    f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(?, 1)    f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]
		(e, 1)    f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]
		(e, 1)    f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]
		(1, 1)    f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f17) = V_3
	Pol(f27) = V_3
	Pol(f37) = V_3 - V_5
	Pol(f45) = 3*V_3 - 3*V_5 - 4
	Pol(f55) = 3*V_3 - 3*V_5 - V_6 - 4
	Pol(f65) = 3*V_3 - 3*V_5 - V_6 - V_7 - 4
	Pol(f75) = 3*V_3 - 3*V_5 - V_6 - V_7 - V_8 - 4
	Pol(f83) = -V_1 + 3*V_3 - 3*V_5 - V_6 - V_7 - V_8 - 4
	Pol(f0) = V_3
orients all transitions weakly and the transition
	f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]
strictly and produces the following problem:
7:	T:
		(7, 1)    f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]
		(7, 1)    f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]
		(7, 1)    f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]
		(7, 1)    f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]
		(7, 1)    f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]
		(7, 1)    f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]
		(7, 1)    f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]
		(?, 1)    f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(?, 1)    f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]
		(?, 1)    f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]
		(?, 1)    f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]
		(?, 1)    f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(e, 1)    f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]
		(e, 1)    f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]
		(e, 1)    f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]
		(1, 1)    f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f17) = 2*V_3 - 1
	Pol(f27) = 2*V_3 - 1
	Pol(f37) = 2*V_3 - 1
	Pol(f45) = 2*V_3 - 1
	Pol(f55) = 2*V_3 - 2*V_6 - 1
	Pol(f65) = 3*V_3 - 3*V_6 - V_7 - 2
	Pol(f75) = 3*V_3 - 3*V_6 - V_7 - V_8 - 2
	Pol(f83) = -V_1 + 3*V_3 - 3*V_6 - V_7 - V_8 - 2
	Pol(f0) = 2*V_3 - 1
orients all transitions weakly and the transition
	f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]
strictly and produces the following problem:
8:	T:
		(7, 1)          f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]
		(7, 1)          f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]
		(7, 1)          f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]
		(7, 1)          f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]
		(7, 1)          f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]
		(7, 1)          f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]
		(7, 1)          f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]
		(?, 1)          f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(?, 1)          f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]
		(?, 1)          f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]
		(2*e + 1, 1)    f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]
		(?, 1)          f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(e, 1)          f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]
		(e, 1)          f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]
		(e, 1)          f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]
		(1, 1)          f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f17) = 2*V_3 - 1
	Pol(f27) = 2*V_3 - 1
	Pol(f37) = 2*V_3 - 1
	Pol(f45) = 2*V_3 - 1
	Pol(f55) = 2*V_3 - 1
	Pol(f65) = 2*V_3 - 2*V_7 - 1
	Pol(f75) = 2*V_3 - 2*V_7 - V_8 - 3
	Pol(f83) = -V_1 + 3*V_3 - 2*V_7 - 2*V_8 - 3
	Pol(f0) = 2*V_3 - 1
orients all transitions weakly and the transition
	f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]
strictly and produces the following problem:
9:	T:
		(7, 1)          f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]
		(7, 1)          f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]
		(7, 1)          f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]
		(7, 1)          f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]
		(7, 1)          f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]
		(7, 1)          f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]
		(7, 1)          f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]
		(?, 1)          f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(?, 1)          f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]
		(2*e + 1, 1)    f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]
		(2*e + 1, 1)    f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]
		(?, 1)          f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(e, 1)          f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]
		(e, 1)          f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]
		(e, 1)          f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]
		(1, 1)          f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f17) = 2*V_3 - 1
	Pol(f27) = 2*V_3 - 1
	Pol(f37) = 2*V_3 - 1
	Pol(f45) = 2*V_3 - 1
	Pol(f55) = 2*V_3 - 1
	Pol(f65) = 2*V_3 - 1
	Pol(f75) = 2*V_3 - 2*V_8 - 1
	Pol(f83) = -V_1 + 2*V_3 - 2*V_8 - 3
	Pol(f0) = 2*V_3 - 1
orients all transitions weakly and the transition
	f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]
strictly and produces the following problem:
10:	T:
		(7, 1)          f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]
		(7, 1)          f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]
		(7, 1)          f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]
		(7, 1)          f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]
		(7, 1)          f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]
		(7, 1)          f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]
		(7, 1)          f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]
		(?, 1)          f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(2*e + 1, 1)    f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]
		(2*e + 1, 1)    f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]
		(2*e + 1, 1)    f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]
		(?, 1)          f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(e, 1)          f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]
		(e, 1)          f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]
		(e, 1)          f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]
		(1, 1)          f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f17) = 2*V_3 - 1
	Pol(f27) = 2*V_3 - 1
	Pol(f37) = 2*V_3 - 1
	Pol(f45) = 2*V_3 - 1
	Pol(f55) = 2*V_3 - 1
	Pol(f65) = 2*V_3 - 1
	Pol(f75) = 2*V_3 - 1
	Pol(f83) = -2*V_1 + 2*V_3 - 1
	Pol(f0) = 2*V_3 - 1
orients all transitions weakly and the transition
	f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
strictly and produces the following problem:
11:	T:
		(7, 1)          f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]
		(7, 1)          f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]
		(7, 1)          f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]
		(7, 1)          f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]
		(7, 1)          f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]
		(7, 1)          f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]
		(7, 1)          f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]
		(2*e + 1, 1)    f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(2*e + 1, 1)    f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]
		(2*e + 1, 1)    f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]
		(2*e + 1, 1)    f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]
		(?, 1)          f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(e, 1)          f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]
		(e, 1)          f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]
		(e, 1)          f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]
		(1, 1)          f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f45) = -V_1 + V_3
and size complexities
	S("f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)", 0-0) = 0
	S("f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)", 0-1) = 0
	S("f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)", 0-2) = e
	S("f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)", 0-3) = f
	S("f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)", 0-4) = g
	S("f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)", 0-5) = h
	S("f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)", 0-6) = i
	S("f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)", 0-7) = j
	S("f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]", 0-0) = 0
	S("f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]", 0-1) = e
	S("f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]", 0-2) = e
	S("f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]", 0-3) = f
	S("f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]", 0-4) = g
	S("f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]", 0-5) = h
	S("f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]", 0-6) = i
	S("f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]", 0-7) = j
	S("f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]", 0-0) = 0
	S("f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]", 0-1) = e
	S("f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]", 0-2) = e
	S("f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]", 0-3) = e
	S("f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]", 0-4) = g
	S("f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]", 0-5) = h
	S("f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]", 0-6) = i
	S("f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]", 0-7) = j
	S("f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]", 0-0) = 0
	S("f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]", 0-1) = e
	S("f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]", 0-2) = e
	S("f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]", 0-3) = e
	S("f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]", 0-4) = e
	S("f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]", 0-5) = h
	S("f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]", 0-6) = i
	S("f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]", 0-7) = j
	S("f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]", 0-0) = ?
	S("f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]", 0-1) = e
	S("f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]", 0-2) = e
	S("f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]", 0-3) = e
	S("f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]", 0-4) = e
	S("f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]", 0-5) = h
	S("f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]", 0-6) = i
	S("f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]", 0-7) = j
	S("f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]", 0-0) = ?
	S("f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]", 0-1) = e
	S("f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]", 0-2) = e
	S("f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]", 0-3) = e
	S("f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]", 0-4) = e
	S("f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]", 0-5) = 2*e + 4
	S("f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]", 0-6) = i
	S("f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]", 0-7) = j
	S("f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]", 0-0) = ?
	S("f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]", 0-1) = e
	S("f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]", 0-2) = e
	S("f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]", 0-3) = e
	S("f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]", 0-4) = e
	S("f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]", 0-5) = 2*e + 16
	S("f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]", 0-6) = 2*e + 4
	S("f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]", 0-7) = j
	S("f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]", 0-0) = ?
	S("f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]", 0-1) = e
	S("f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]", 0-2) = e
	S("f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]", 0-3) = e
	S("f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]", 0-4) = e
	S("f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]", 0-5) = 2*e + 64
	S("f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]", 0-6) = 2*e + 16
	S("f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]", 0-7) = 2*e + 4
	S("f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]", 0-0) = 2*e + 4
	S("f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]", 0-1) = e
	S("f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]", 0-2) = e
	S("f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]", 0-3) = e
	S("f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]", 0-4) = e
	S("f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]", 0-5) = 2*e + 256
	S("f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]", 0-6) = 2*e + 64
	S("f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]", 0-7) = 2*e + 16
	S("f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]", 0-0) = 0
	S("f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]", 0-1) = e
	S("f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]", 0-2) = e
	S("f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]", 0-3) = e
	S("f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]", 0-4) = e
	S("f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]", 0-5) = 2*e + 128
	S("f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]", 0-6) = 2*e + 32
	S("f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]", 0-7) = 2*e + 8
	S("f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]", 0-0) = ?
	S("f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]", 0-1) = e
	S("f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]", 0-2) = e
	S("f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]", 0-3) = e
	S("f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]", 0-4) = e
	S("f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]", 0-5) = 2*e + 32
	S("f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]", 0-6) = 2*e + 8
	S("f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]", 0-7) = 0
	S("f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]", 0-0) = ?
	S("f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]", 0-1) = e
	S("f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]", 0-2) = e
	S("f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]", 0-3) = e
	S("f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]", 0-4) = e
	S("f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]", 0-5) = 2*e + 8
	S("f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]", 0-6) = 0
	S("f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]", 0-7) = j
	S("f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]", 0-0) = ?
	S("f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]", 0-1) = e
	S("f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]", 0-2) = e
	S("f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]", 0-3) = e
	S("f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]", 0-4) = e
	S("f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]", 0-5) = 0
	S("f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]", 0-6) = i
	S("f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]", 0-7) = j
	S("f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]", 0-0) = 0
	S("f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]", 0-1) = e
	S("f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]", 0-2) = e
	S("f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]", 0-3) = e
	S("f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]", 0-4) = e
	S("f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]", 0-5) = h
	S("f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]", 0-6) = i
	S("f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]", 0-7) = j
	S("f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]", 0-0) = 0
	S("f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]", 0-1) = e
	S("f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]", 0-2) = e
	S("f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]", 0-3) = e
	S("f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]", 0-4) = 0
	S("f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]", 0-5) = h
	S("f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]", 0-6) = i
	S("f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]", 0-7) = j
	S("f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]", 0-0) = 0
	S("f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]", 0-1) = e
	S("f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]", 0-2) = e
	S("f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]", 0-3) = 0
	S("f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]", 0-4) = g
	S("f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]", 0-5) = h
	S("f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]", 0-6) = i
	S("f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]", 0-7) = j
orients the transition
	f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
weakly and the transition
	f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
strictly and produces the following problem:
12:	T:
		(7, 1)          f17(a, d, e, f, g, h, i, j) -> f27(a, d, e, 0, g, h, i, j) [ d >= e ]
		(7, 1)          f27(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, 0, h, i, j) [ f >= e ]
		(7, 1)          f37(a, d, e, f, g, h, i, j) -> f45(0, d, e, f, g, h, i, j) [ g >= e ]
		(7, 1)          f45(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, 0, i, j) [ a >= e ]
		(7, 1)          f55(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, 0, j) [ h >= e ]
		(7, 1)          f65(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, 0) [ i >= e ]
		(7, 1)          f75(a, d, e, f, g, h, i, j) -> f83(0, d, e, f, g, h, i, j) [ j >= e ]
		(2*e + 1, 1)    f83(a, d, e, f, g, h, i, j) -> f83(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(2*e + 1, 1)    f75(a, d, e, f, g, h, i, j) -> f75(a, d, e, f, g, h, i, j + 1) [ e >= j + 1 ]
		(2*e + 1, 1)    f65(a, d, e, f, g, h, i, j) -> f65(a, d, e, f, g, h, i + 1, j) [ e >= i + 1 ]
		(2*e + 1, 1)    f55(a, d, e, f, g, h, i, j) -> f55(a, d, e, f, g, h + 1, i, j) [ e >= h + 1 ]
		(7*e, 1)        f45(a, d, e, f, g, h, i, j) -> f45(a + 1, d, e, f, g, h, i, j) [ e >= a + 1 ]
		(e, 1)          f37(a, d, e, f, g, h, i, j) -> f37(a, d, e, f, g + 1, h, i, j) [ e >= g + 1 ]
		(e, 1)          f27(a, d, e, f, g, h, i, j) -> f27(a, d, e, f + 1, g, h, i, j) [ e >= f + 1 ]
		(e, 1)          f17(a, d, e, f, g, h, i, j) -> f17(a, d + 1, e, f, g, h, i, j) [ e >= d + 1 ]
		(1, 1)          f0(a, d, e, f, g, h, i, j) -> f17(0, 0, e, f, g, h, i, j)
	start location:	f0
	leaf cost:	1

Complexity upper bound 18*e + 55

Time: 1.113 sec (SMT: 0.949 sec)