MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f11(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, z, a1, b1, c1, d1, e1, f1, g1, h1) -> f11(a, b + 1, d, i1, d, j1, b, i, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1) [ a >= b + 1 /\ b >= 0 ]
		(?, 1)    f2(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, z, a1, b1, c1, d1, e1, f1, g1, h1) -> f2(a, b, c, d, e, f, g, h, i, j, i1, j1, j, j1, j, q, q, i, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1) [ 0 >= j + 1 /\ i1 >= 2 ]
		(?, 1)    f2(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, z, a1, b1, c1, d1, e1, f1, g1, h1) -> f2(a, b, c, d, e, f, g, h, i, j, i1, j1, j, j1, j, q, q, i, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1) [ j >= 1 /\ i1 >= 2 ]
		(?, 1)    f5(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, z, a1, b1, c1, d1, e1, f1, g1, h1) -> f5(a, b, c, d, e, f, g, h, i, j, 1, i1, j, i1, j, p, q, r, i, u, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1) [ 0 >= j + 1 ]
		(?, 1)    f5(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, z, a1, b1, c1, d1, e1, f1, g1, h1) -> f5(a, b, c, d, e, f, g, h, i, j, 1, i1, j, i1, j, p, q, r, i, u, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1) [ j >= 1 ]
		(1, 1)    f0(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, z, a1, b1, c1, d1, e1, f1, g1, h1) -> f11(j1, 2, k1, l1, k1, f, g, h, i, j, j1, l, m, n, o, p, q, r, s, t, u, i1, k1, m1, y, z, a1, b1, c1, d1, e1, f1, g1, h1) [ j1 >= 2 ]
		(1, 1)    f0(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, z, a1, b1, c1, d1, e1, f1, g1, h1) -> f1(k1, m1, l1, u1, t1, f, g, h, i, p1, j1, v1, w1, n, x1, p, q, r, s, t, u, i1, s1, x, d2, q1, r1, y1, z1, a2, b2, c2, e2, h1) [ 0 >= n1 /\ 0 >= j1 /\ 0 >= o1 /\ y = 0 ]
		(1, 1)    f0(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, z, a1, b1, c1, d1, e1, f1, g1, h1) -> f5(j1, l1, k1, s1, r1, f, g, h, i, j, 1, t1, j, t1, j, p, q, r, s, t, u, i1, q1, x, y, m1, p1, b1, c1, d1, e1, f1, g1, h1) [ 0 >= j + 1 ]
		(1, 1)    f0(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, z, a1, b1, c1, d1, e1, f1, g1, h1) -> f5(j1, l1, k1, s1, r1, f, g, h, i, j, 1, t1, j, t1, j, p, q, r, s, t, u, i1, q1, x, y, m1, p1, b1, c1, d1, e1, f1, g1, h1) [ j >= 1 ]
		(?, 1)    f11(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, z, a1, b1, c1, d1, e1, f1, g1, h1) -> f2(j1, l1, k1, s1, r1, f, g, h, i, j, i1, t1, j, t1, j, p, q, r, s, t, u, v, q1, x, y, m1, p1, b1, c1, d1, e1, f1, g1, h1) [ u1 >= 2 /\ h1 >= u1 /\ v1 >= 2 /\ h1 >= v1 /\ b >= a /\ b >= 0 /\ i1 >= 2 /\ 0 >= j + 1 /\ h1 >= 0 ]
		(?, 1)    f11(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, z, a1, b1, c1, d1, e1, f1, g1, h1) -> f2(j1, l1, k1, s1, r1, f, g, h, i, j, i1, t1, j, t1, j, p, q, r, s, t, u, v, q1, x, y, m1, p1, b1, c1, d1, e1, f1, g1, h1) [ u1 >= 2 /\ h1 >= u1 /\ v1 >= 2 /\ h1 >= v1 /\ b >= a /\ b >= 0 /\ i1 >= 2 /\ j >= 1 /\ h1 >= 0 ]
	start location:	f0
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, j, y, h1].
We thus obtain the following problem:
2:	T:
		(?, 1)    f11(a, b, j, y, h1) -> f2(j1, l1, j, y, h1) [ u1 >= 2 /\ h1 >= u1 /\ v1 >= 2 /\ h1 >= v1 /\ b >= a /\ b >= 0 /\ i1 >= 2 /\ j >= 1 /\ h1 >= 0 ]
		(?, 1)    f11(a, b, j, y, h1) -> f2(j1, l1, j, y, h1) [ u1 >= 2 /\ h1 >= u1 /\ v1 >= 2 /\ h1 >= v1 /\ b >= a /\ b >= 0 /\ i1 >= 2 /\ 0 >= j + 1 /\ h1 >= 0 ]
		(1, 1)    f0(a, b, j, y, h1) -> f5(j1, l1, j, y, h1) [ j >= 1 ]
		(1, 1)    f0(a, b, j, y, h1) -> f5(j1, l1, j, y, h1) [ 0 >= j + 1 ]
		(1, 1)    f0(a, b, j, y, h1) -> f1(k1, m1, p1, d2, h1) [ 0 >= n1 /\ 0 >= j1 /\ 0 >= o1 /\ y = 0 ]
		(1, 1)    f0(a, b, j, y, h1) -> f11(j1, 2, j, y, h1) [ j1 >= 2 ]
		(?, 1)    f5(a, b, j, y, h1) -> f5(a, b, j, y, h1) [ j >= 1 ]
		(?, 1)    f5(a, b, j, y, h1) -> f5(a, b, j, y, h1) [ 0 >= j + 1 ]
		(?, 1)    f2(a, b, j, y, h1) -> f2(a, b, j, y, h1) [ j >= 1 /\ i1 >= 2 ]
		(?, 1)    f2(a, b, j, y, h1) -> f2(a, b, j, y, h1) [ 0 >= j + 1 /\ i1 >= 2 ]
		(?, 1)    f11(a, b, j, y, h1) -> f11(a, b + 1, j, y, h1) [ a >= b + 1 /\ b >= 0 ]
	start location:	f0
	leaf cost:	0

A polynomial rank function with
	Pol(f11) = 1
	Pol(f2) = -3
	Pol(f0) = 1
	Pol(f5) = -3
	Pol(f1) = 1
orients all transitions weakly and the transition
	f11(a, b, j, y, h1) -> f2(j1, l1, j, y, h1) [ u1 >= 2 /\ h1 >= u1 /\ v1 >= 2 /\ h1 >= v1 /\ b >= a /\ b >= 0 /\ i1 >= 2 /\ 0 >= j + 1 /\ h1 >= 0 ]
strictly and produces the following problem:
3:	T:
		(?, 1)    f11(a, b, j, y, h1) -> f2(j1, l1, j, y, h1) [ u1 >= 2 /\ h1 >= u1 /\ v1 >= 2 /\ h1 >= v1 /\ b >= a /\ b >= 0 /\ i1 >= 2 /\ j >= 1 /\ h1 >= 0 ]
		(1, 1)    f11(a, b, j, y, h1) -> f2(j1, l1, j, y, h1) [ u1 >= 2 /\ h1 >= u1 /\ v1 >= 2 /\ h1 >= v1 /\ b >= a /\ b >= 0 /\ i1 >= 2 /\ 0 >= j + 1 /\ h1 >= 0 ]
		(1, 1)    f0(a, b, j, y, h1) -> f5(j1, l1, j, y, h1) [ j >= 1 ]
		(1, 1)    f0(a, b, j, y, h1) -> f5(j1, l1, j, y, h1) [ 0 >= j + 1 ]
		(1, 1)    f0(a, b, j, y, h1) -> f1(k1, m1, p1, d2, h1) [ 0 >= n1 /\ 0 >= j1 /\ 0 >= o1 /\ y = 0 ]
		(1, 1)    f0(a, b, j, y, h1) -> f11(j1, 2, j, y, h1) [ j1 >= 2 ]
		(?, 1)    f5(a, b, j, y, h1) -> f5(a, b, j, y, h1) [ j >= 1 ]
		(?, 1)    f5(a, b, j, y, h1) -> f5(a, b, j, y, h1) [ 0 >= j + 1 ]
		(?, 1)    f2(a, b, j, y, h1) -> f2(a, b, j, y, h1) [ j >= 1 /\ i1 >= 2 ]
		(?, 1)    f2(a, b, j, y, h1) -> f2(a, b, j, y, h1) [ 0 >= j + 1 /\ i1 >= 2 ]
		(?, 1)    f11(a, b, j, y, h1) -> f11(a, b + 1, j, y, h1) [ a >= b + 1 /\ b >= 0 ]
	start location:	f0
	leaf cost:	0

A polynomial rank function with
	Pol(f11) = 1
	Pol(f2) = -3
	Pol(f0) = 1
	Pol(f5) = -1
	Pol(f1) = 0
orients all transitions weakly and the transition
	f11(a, b, j, y, h1) -> f2(j1, l1, j, y, h1) [ u1 >= 2 /\ h1 >= u1 /\ v1 >= 2 /\ h1 >= v1 /\ b >= a /\ b >= 0 /\ i1 >= 2 /\ j >= 1 /\ h1 >= 0 ]
strictly and produces the following problem:
4:	T:
		(1, 1)    f11(a, b, j, y, h1) -> f2(j1, l1, j, y, h1) [ u1 >= 2 /\ h1 >= u1 /\ v1 >= 2 /\ h1 >= v1 /\ b >= a /\ b >= 0 /\ i1 >= 2 /\ j >= 1 /\ h1 >= 0 ]
		(1, 1)    f11(a, b, j, y, h1) -> f2(j1, l1, j, y, h1) [ u1 >= 2 /\ h1 >= u1 /\ v1 >= 2 /\ h1 >= v1 /\ b >= a /\ b >= 0 /\ i1 >= 2 /\ 0 >= j + 1 /\ h1 >= 0 ]
		(1, 1)    f0(a, b, j, y, h1) -> f5(j1, l1, j, y, h1) [ j >= 1 ]
		(1, 1)    f0(a, b, j, y, h1) -> f5(j1, l1, j, y, h1) [ 0 >= j + 1 ]
		(1, 1)    f0(a, b, j, y, h1) -> f1(k1, m1, p1, d2, h1) [ 0 >= n1 /\ 0 >= j1 /\ 0 >= o1 /\ y = 0 ]
		(1, 1)    f0(a, b, j, y, h1) -> f11(j1, 2, j, y, h1) [ j1 >= 2 ]
		(?, 1)    f5(a, b, j, y, h1) -> f5(a, b, j, y, h1) [ j >= 1 ]
		(?, 1)    f5(a, b, j, y, h1) -> f5(a, b, j, y, h1) [ 0 >= j + 1 ]
		(?, 1)    f2(a, b, j, y, h1) -> f2(a, b, j, y, h1) [ j >= 1 /\ i1 >= 2 ]
		(?, 1)    f2(a, b, j, y, h1) -> f2(a, b, j, y, h1) [ 0 >= j + 1 /\ i1 >= 2 ]
		(?, 1)    f11(a, b, j, y, h1) -> f11(a, b + 1, j, y, h1) [ a >= b + 1 /\ b >= 0 ]
	start location:	f0
	leaf cost:	0

Applied AI with 'oct' on problem 4 to obtain the following invariants:
  For symbol f11: X_1 - X_2 >= 0 /\ X_2 - 2 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ X_1 - 2 >= 0
  For symbol f2: X_5 - 2 >= 0


This yielded the following problem:
5:	T:
		(?, 1)    f11(a, b, j, y, h1) -> f11(a, b + 1, j, y, h1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ]
		(?, 1)    f2(a, b, j, y, h1) -> f2(a, b, j, y, h1) [ h1 - 2 >= 0 /\ 0 >= j + 1 /\ i1 >= 2 ]
		(?, 1)    f2(a, b, j, y, h1) -> f2(a, b, j, y, h1) [ h1 - 2 >= 0 /\ j >= 1 /\ i1 >= 2 ]
		(?, 1)    f5(a, b, j, y, h1) -> f5(a, b, j, y, h1) [ 0 >= j + 1 ]
		(?, 1)    f5(a, b, j, y, h1) -> f5(a, b, j, y, h1) [ j >= 1 ]
		(1, 1)    f0(a, b, j, y, h1) -> f11(j1, 2, j, y, h1) [ j1 >= 2 ]
		(1, 1)    f0(a, b, j, y, h1) -> f1(k1, m1, p1, d2, h1) [ 0 >= n1 /\ 0 >= j1 /\ 0 >= o1 /\ y = 0 ]
		(1, 1)    f0(a, b, j, y, h1) -> f5(j1, l1, j, y, h1) [ 0 >= j + 1 ]
		(1, 1)    f0(a, b, j, y, h1) -> f5(j1, l1, j, y, h1) [ j >= 1 ]
		(1, 1)    f11(a, b, j, y, h1) -> f2(j1, l1, j, y, h1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ u1 >= 2 /\ h1 >= u1 /\ v1 >= 2 /\ h1 >= v1 /\ b >= a /\ b >= 0 /\ i1 >= 2 /\ 0 >= j + 1 /\ h1 >= 0 ]
		(1, 1)    f11(a, b, j, y, h1) -> f2(j1, l1, j, y, h1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ u1 >= 2 /\ h1 >= u1 /\ v1 >= 2 /\ h1 >= v1 /\ b >= a /\ b >= 0 /\ i1 >= 2 /\ j >= 1 /\ h1 >= 0 ]
	start location:	f0
	leaf cost:	0

Complexity upper bound ?

Time: 0.720 sec (SMT: 0.659 sec)