MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f1(a, b + 1, d, z, d, a1, b, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) [ a >= b + 1 /\ b >= 0 ]
		(?, 1)    f7(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f8(a, b, c, d, e, f, g, h, i, 0, z, a1, a1, 0, a1, h, q, r, s, t, u, v, w, x, y) [ b1 >= h + 1 /\ i >= 0 /\ a1 >= b1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f7(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f8(a, b, c, d, e, f, g, h, i, 0, z, a1, a1, 0, a1, h, q, r, s, t, u, v, w, x, y) [ b1 >= h + 1 /\ i >= 0 /\ b1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f7(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f8(a, b, c, d, e, f, g, h, i, 0, z, a1, a1, 0, a1, h, q, r, s, t, u, v, w, x, y) [ h >= b1 + 1 /\ i >= 0 /\ a1 >= b1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f7(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f8(a, b, c, d, e, f, g, h, i, 0, z, a1, a1, 0, a1, h, q, r, s, t, u, v, w, x, y) [ h >= b1 + 1 /\ i >= 0 /\ b1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f7(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f10(a, b, c, d, e, f, g, g1, i, f1, z, b1, c1, d1, e1, h1, a1, r, s, t, u, v, w, x, y) [ i >= 0 /\ 0 >= b1 + 1 /\ z >= 2 /\ j = h ]
		(?, 1)    f7(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f10(a, b, c, d, e, f, g, g1, i, f1, z, b1, c1, d1, e1, h1, a1, r, s, t, u, v, w, x, y) [ i >= 0 /\ b1 >= 1 /\ z >= 2 /\ j = h ]
		(?, 1)    f8(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f8(a, b, c, d, e, f, g, h, i, 0, z, a1, a1, 0, a1, h, q, r - 1, b1, r - 1, u, v, w, x, y) [ c1 >= h + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f8(a, b, c, d, e, f, g, h, i, 0, z, a1, a1, 0, a1, h, q, r - 1, b1, r - 1, u, v, w, x, y) [ c1 >= h + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f8(a, b, c, d, e, f, g, h, i, 0, z, a1, a1, 0, a1, h, q, r - 1, b1, r - 1, u, v, w, x, y) [ h >= c1 + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f8(a, b, c, d, e, f, g, h, i, 0, z, a1, a1, 0, a1, h, q, r - 1, b1, r - 1, u, v, w, x, y) [ h >= c1 + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f10(a, b, c, d, e, f, g, f1, i, e1, z, l, b1, c1, d1, g1, a1, r, s, t, u, v, w, x, y) [ z >= 2 /\ r >= 0 /\ j = h ]
		(1, 1)    f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f10(b1, d1, c1, k1, h1, f, g, p1, i, o1, a1, 0, l1, m1, n1, q1, f1, r, s, t, z, e1, g1, x, y) [ 0 >= i1 /\ 0 >= a1 /\ 0 >= j1 ]
		(1, 1)    f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f1(a1, 2, b1, c1, b1, f, g, h, i, j, a1, l, m, n, o, p, q, r, s, t, z, v, b1, d1, y) [ a1 >= 2 ]
		(?, 1)    f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f8(a1, c1, b1, h1, g1, f, g, c, r, 0, z, c, c, 0, c, c, e1, r, s, t, u, d1, f1, x, r + 1) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ c >= 1 /\ c1 >= 0 /\ z >= 2 /\ 0 >= c + 1 ]
		(?, 1)    f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f8(a1, c1, b1, h1, g1, f, g, c, r, 0, z, c, c, 0, c, c, e1, r, s, t, u, d1, f1, x, r + 1) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ c >= 1 /\ c1 >= 0 /\ z >= 2 ]
		(?, 1)    f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f8(a1, c1, b1, h1, g1, f, g, c, r, 0, z, c, c, 0, c, c, e1, r, s, t, u, d1, f1, x, r + 1) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ 0 >= c + 1 /\ c1 >= 0 /\ z >= 2 ]
		(?, 1)    f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -> f8(a1, c1, b1, h1, g1, f, g, c, r, 0, z, c, c, 0, c, c, e1, r, s, t, u, d1, f1, x, r + 1) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ 0 >= c + 1 /\ c1 >= 0 /\ z >= 2 /\ c >= 1 ]
	start location:	f9
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, d, h, i, j, r].
We thus obtain the following problem:
2:	T:
		(?, 1)    f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ 0 >= c + 1 /\ c1 >= 0 /\ z >= 2 /\ c >= 1 ]
		(?, 1)    f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ 0 >= c + 1 /\ c1 >= 0 /\ z >= 2 ]
		(?, 1)    f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ c >= 1 /\ c1 >= 0 /\ z >= 2 ]
		(?, 1)    f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ c >= 1 /\ c1 >= 0 /\ z >= 2 /\ 0 >= c + 1 ]
		(1, 1)    f9(a, b, c, d, h, i, j, r) -> f1(a1, 2, b1, c1, h, i, j, r) [ a1 >= 2 ]
		(1, 1)    f9(a, b, c, d, h, i, j, r) -> f10(b1, d1, c1, k1, p1, i, o1, r) [ 0 >= i1 /\ 0 >= a1 /\ 0 >= j1 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f10(a, b, c, d, f1, i, e1, r) [ z >= 2 /\ r >= 0 /\ j = h ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ h >= c1 + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ h >= c1 + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ c1 >= h + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ c1 >= h + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f7(a, b, c, d, h, i, j, r) -> f10(a, b, c, d, g1, i, f1, r) [ i >= 0 /\ b1 >= 1 /\ z >= 2 /\ j = h ]
		(?, 1)    f7(a, b, c, d, h, i, j, r) -> f10(a, b, c, d, g1, i, f1, r) [ i >= 0 /\ 0 >= b1 + 1 /\ z >= 2 /\ j = h ]
		(?, 1)    f7(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r) [ h >= b1 + 1 /\ i >= 0 /\ b1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f7(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r) [ h >= b1 + 1 /\ i >= 0 /\ a1 >= b1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f7(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r) [ b1 >= h + 1 /\ i >= 0 /\ b1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f7(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r) [ b1 >= h + 1 /\ i >= 0 /\ a1 >= b1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f1(a, b, c, d, h, i, j, r) -> f1(a, b + 1, d, z, h, i, j, r) [ a >= b + 1 /\ b >= 0 ]
	start location:	f9
	leaf cost:	0

Testing for unsatisfiable constraints removes the following transitions from problem 2:
	f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ 0 >= c + 1 /\ c1 >= 0 /\ z >= 2 /\ c >= 1 ]
	f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ c >= 1 /\ c1 >= 0 /\ z >= 2 /\ 0 >= c + 1 ]
We thus obtain the following problem:
3:	T:
		(?, 1)    f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ 0 >= c + 1 /\ c1 >= 0 /\ z >= 2 ]
		(?, 1)    f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ c >= 1 /\ c1 >= 0 /\ z >= 2 ]
		(1, 1)    f9(a, b, c, d, h, i, j, r) -> f1(a1, 2, b1, c1, h, i, j, r) [ a1 >= 2 ]
		(1, 1)    f9(a, b, c, d, h, i, j, r) -> f10(b1, d1, c1, k1, p1, i, o1, r) [ 0 >= i1 /\ 0 >= a1 /\ 0 >= j1 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f10(a, b, c, d, f1, i, e1, r) [ z >= 2 /\ r >= 0 /\ j = h ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ h >= c1 + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ h >= c1 + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ c1 >= h + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ c1 >= h + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f7(a, b, c, d, h, i, j, r) -> f10(a, b, c, d, g1, i, f1, r) [ i >= 0 /\ b1 >= 1 /\ z >= 2 /\ j = h ]
		(?, 1)    f7(a, b, c, d, h, i, j, r) -> f10(a, b, c, d, g1, i, f1, r) [ i >= 0 /\ 0 >= b1 + 1 /\ z >= 2 /\ j = h ]
		(?, 1)    f7(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r) [ h >= b1 + 1 /\ i >= 0 /\ b1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f7(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r) [ h >= b1 + 1 /\ i >= 0 /\ a1 >= b1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f7(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r) [ b1 >= h + 1 /\ i >= 0 /\ b1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f7(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r) [ b1 >= h + 1 /\ i >= 0 /\ a1 >= b1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f1(a, b, c, d, h, i, j, r) -> f1(a, b + 1, d, z, h, i, j, r) [ a >= b + 1 /\ b >= 0 ]
	start location:	f9
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 3 produces the following problem:
4:	T:
		(?, 1)    f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ 0 >= c + 1 /\ c1 >= 0 /\ z >= 2 ]
		(?, 1)    f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ c >= 1 /\ c1 >= 0 /\ z >= 2 ]
		(1, 1)    f9(a, b, c, d, h, i, j, r) -> f1(a1, 2, b1, c1, h, i, j, r) [ a1 >= 2 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ h >= c1 + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ h >= c1 + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ c1 >= h + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ c1 >= h + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f7(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r) [ h >= b1 + 1 /\ i >= 0 /\ b1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f7(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r) [ h >= b1 + 1 /\ i >= 0 /\ a1 >= b1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f7(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r) [ b1 >= h + 1 /\ i >= 0 /\ b1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f7(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r) [ b1 >= h + 1 /\ i >= 0 /\ a1 >= b1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f1(a, b, c, d, h, i, j, r) -> f1(a, b + 1, d, z, h, i, j, r) [ a >= b + 1 /\ b >= 0 ]
	start location:	f9
	leaf cost:	4

Testing for reachability in the complexity graph removes the following transitions from problem 4:
	f7(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r) [ h >= b1 + 1 /\ i >= 0 /\ b1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
	f7(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r) [ h >= b1 + 1 /\ i >= 0 /\ a1 >= b1 + 1 /\ z >= 2 /\ j = 0 ]
	f7(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r) [ b1 >= h + 1 /\ i >= 0 /\ b1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
	f7(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r) [ b1 >= h + 1 /\ i >= 0 /\ a1 >= b1 + 1 /\ z >= 2 /\ j = 0 ]
We thus obtain the following problem:
5:	T:
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ c1 >= h + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ c1 >= h + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ h >= c1 + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ h >= c1 + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f1(a, b, c, d, h, i, j, r) -> f1(a, b + 1, d, z, h, i, j, r) [ a >= b + 1 /\ b >= 0 ]
		(?, 1)    f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ c >= 1 /\ c1 >= 0 /\ z >= 2 ]
		(?, 1)    f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ 0 >= c + 1 /\ c1 >= 0 /\ z >= 2 ]
		(1, 1)    f9(a, b, c, d, h, i, j, r) -> f1(a1, 2, b1, c1, h, i, j, r) [ a1 >= 2 ]
	start location:	f9
	leaf cost:	4

A polynomial rank function with
	Pol(f8) = -5
	Pol(f1) = 2
	Pol(f9) = 2
orients all transitions weakly and the transitions
	f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ c >= 1 /\ c1 >= 0 /\ z >= 2 ]
	f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ 0 >= c + 1 /\ c1 >= 0 /\ z >= 2 ]
strictly and produces the following problem:
6:	T:
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ c1 >= h + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ c1 >= h + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ h >= c1 + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ h >= c1 + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)    f1(a, b, c, d, h, i, j, r) -> f1(a, b + 1, d, z, h, i, j, r) [ a >= b + 1 /\ b >= 0 ]
		(2, 1)    f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ c >= 1 /\ c1 >= 0 /\ z >= 2 ]
		(2, 1)    f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ 0 >= c + 1 /\ c1 >= 0 /\ z >= 2 ]
		(1, 1)    f9(a, b, c, d, h, i, j, r) -> f1(a1, 2, b1, c1, h, i, j, r) [ a1 >= 2 ]
	start location:	f9
	leaf cost:	4

A polynomial rank function with
	Pol(f8) = V_8 + 1
	Pol(f1) = V_8 + 1
	Pol(f9) = V_8 + 1
orients all transitions weakly and the transitions
	f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ h >= c1 + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
	f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ h >= c1 + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
	f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ c1 >= h + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
	f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ c1 >= h + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
strictly and produces the following problem:
7:	T:
		(r + 1, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ c1 >= h + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
		(r + 1, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ c1 >= h + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(r + 1, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ h >= c1 + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
		(r + 1, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ h >= c1 + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(?, 1)        f1(a, b, c, d, h, i, j, r) -> f1(a, b + 1, d, z, h, i, j, r) [ a >= b + 1 /\ b >= 0 ]
		(2, 1)        f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ c >= 1 /\ c1 >= 0 /\ z >= 2 ]
		(2, 1)        f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ 0 >= c + 1 /\ c1 >= 0 /\ z >= 2 ]
		(1, 1)        f9(a, b, c, d, h, i, j, r) -> f1(a1, 2, b1, c1, h, i, j, r) [ a1 >= 2 ]
	start location:	f9
	leaf cost:	4

Applied AI with 'oct' on problem 7 to obtain the following invariants:
  For symbol f1: X_1 - X_2 >= 0 /\ X_2 - 2 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ X_1 - 2 >= 0
  For symbol f8: X_6 - X_8 >= 0 /\ -X_7 >= 0 /\ X_2 - X_7 - 2 >= 0 /\ X_7 >= 0 /\ X_2 + X_7 - 2 >= 0 /\ X_2 - 2 >= 0


This yielded the following problem:
8:	T:
		(1, 1)        f9(a, b, c, d, h, i, j, r) -> f1(a1, 2, b1, c1, h, i, j, r) [ a1 >= 2 ]
		(2, 1)        f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ 0 >= c + 1 /\ c1 >= 0 /\ z >= 2 ]
		(2, 1)        f1(a, b, c, d, h, i, j, r) -> f8(a1, c1, b1, h1, c, r, 0, r) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ k1 >= z /\ l1 >= 2 /\ c1 >= l1 /\ b >= a /\ b >= 0 /\ c >= 1 /\ c1 >= 0 /\ z >= 2 ]
		(?, 1)        f1(a, b, c, d, h, i, j, r) -> f1(a, b + 1, d, z, h, i, j, r) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
		(r + 1, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ i - r >= 0 /\ -j >= 0 /\ b - j - 2 >= 0 /\ j >= 0 /\ b + j - 2 >= 0 /\ b - 2 >= 0 /\ h >= c1 + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(r + 1, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ i - r >= 0 /\ -j >= 0 /\ b - j - 2 >= 0 /\ j >= 0 /\ b + j - 2 >= 0 /\ b - 2 >= 0 /\ h >= c1 + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
		(r + 1, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ i - r >= 0 /\ -j >= 0 /\ b - j - 2 >= 0 /\ j >= 0 /\ b + j - 2 >= 0 /\ b - 2 >= 0 /\ c1 >= h + 1 /\ r >= 0 /\ c1 >= a1 + 1 /\ z >= 2 /\ j = 0 ]
		(r + 1, 1)    f8(a, b, c, d, h, i, j, r) -> f8(a, b, c, d, h, i, 0, r - 1) [ i - r >= 0 /\ -j >= 0 /\ b - j - 2 >= 0 /\ j >= 0 /\ b + j - 2 >= 0 /\ b - 2 >= 0 /\ c1 >= h + 1 /\ r >= 0 /\ a1 >= c1 + 1 /\ z >= 2 /\ j = 0 ]
	start location:	f9
	leaf cost:	4

Complexity upper bound ?

Time: 1.496 sec (SMT: 1.365 sec)