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) -> f11(a, b, b, b, 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) [ a >= b + 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) -> f11(a, b, b, b, 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) [ b >= a + 1 ]
		(?, 1)    f6(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) -> f6(a, b, c, d, e, h1, g + 1, h - 1, g + 1, h - 1, f1, g1, h - 1, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1) [ e >= f + 1 /\ g >= 0 /\ h >= 1 ]
		(?, 1)    f6(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) -> f6(a, b, c, d, e, h1, g + 1, h - 1, g + 1, h - 1, f1, g1, h - 1, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1) [ f >= e + 1 /\ g >= 0 /\ h >= 1 ]
		(1, 1)    f26(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) -> f6(a, b, c, d, e, l1, 1, 4, 1, 4, k, l, m, f1, 2, 3, g1, h1, 4, j1, 0, k1, m1, m1, m1, m1, n1, o1, p1, 4, e1) [ e >= i1 + 1 ]
		(1, 1)    f26(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) -> f6(a, b, c, d, e, l1, 1, 4, 1, 4, k, l, m, f1, 2, 3, g1, h1, 4, j1, 0, k1, m1, m1, m1, m1, n1, o1, p1, 4, e1) [ i1 >= e + 1 ]
		(?, 1)    f6(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) -> f11(a, j1, j1, j1, f, f, g, h, i, j, k, l, m, f1, o, p, q, r, s, t, u, v, w, x, y, g1, a1, b1, c1, d1, h1) [ a >= j1 + 1 /\ g >= 0 /\ h >= 1 /\ f = e ]
		(?, 1)    f6(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) -> f11(a, j1, j1, j1, f, f, g, h, i, j, k, l, m, f1, o, p, q, r, s, t, u, v, w, x, y, g1, a1, b1, c1, d1, h1) [ j1 >= a + 1 /\ g >= 0 /\ h >= 1 /\ f = e ]
	start location:	f26
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, e, f, g, h].
We thus obtain the following problem:
2:	T:
		(?, 1)    f6(a, b, e, f, g, h) -> f11(a, j1, f, f, g, h) [ j1 >= a + 1 /\ g >= 0 /\ h >= 1 /\ f = e ]
		(?, 1)    f6(a, b, e, f, g, h) -> f11(a, j1, f, f, g, h) [ a >= j1 + 1 /\ g >= 0 /\ h >= 1 /\ f = e ]
		(1, 1)    f26(a, b, e, f, g, h) -> f6(a, b, e, l1, 1, 4) [ i1 >= e + 1 ]
		(1, 1)    f26(a, b, e, f, g, h) -> f6(a, b, e, l1, 1, 4) [ e >= i1 + 1 ]
		(?, 1)    f6(a, b, e, f, g, h) -> f6(a, b, e, h1, g + 1, h - 1) [ f >= e + 1 /\ g >= 0 /\ h >= 1 ]
		(?, 1)    f6(a, b, e, f, g, h) -> f6(a, b, e, h1, g + 1, h - 1) [ e >= f + 1 /\ g >= 0 /\ h >= 1 ]
		(?, 1)    f11(a, b, e, f, g, h) -> f11(a, b, e, f, g, h) [ b >= a + 1 ]
		(?, 1)    f11(a, b, e, f, g, h) -> f11(a, b, e, f, g, h) [ a >= b + 1 ]
	start location:	f26
	leaf cost:	0

A polynomial rank function with
	Pol(f6) = 1
	Pol(f11) = -1
	Pol(f26) = 1
orients all transitions weakly and the transition
	f6(a, b, e, f, g, h) -> f11(a, j1, f, f, g, h) [ a >= j1 + 1 /\ g >= 0 /\ h >= 1 /\ f = e ]
strictly and produces the following problem:
3:	T:
		(?, 1)    f6(a, b, e, f, g, h) -> f11(a, j1, f, f, g, h) [ j1 >= a + 1 /\ g >= 0 /\ h >= 1 /\ f = e ]
		(1, 1)    f6(a, b, e, f, g, h) -> f11(a, j1, f, f, g, h) [ a >= j1 + 1 /\ g >= 0 /\ h >= 1 /\ f = e ]
		(1, 1)    f26(a, b, e, f, g, h) -> f6(a, b, e, l1, 1, 4) [ i1 >= e + 1 ]
		(1, 1)    f26(a, b, e, f, g, h) -> f6(a, b, e, l1, 1, 4) [ e >= i1 + 1 ]
		(?, 1)    f6(a, b, e, f, g, h) -> f6(a, b, e, h1, g + 1, h - 1) [ f >= e + 1 /\ g >= 0 /\ h >= 1 ]
		(?, 1)    f6(a, b, e, f, g, h) -> f6(a, b, e, h1, g + 1, h - 1) [ e >= f + 1 /\ g >= 0 /\ h >= 1 ]
		(?, 1)    f11(a, b, e, f, g, h) -> f11(a, b, e, f, g, h) [ b >= a + 1 ]
		(?, 1)    f11(a, b, e, f, g, h) -> f11(a, b, e, f, g, h) [ a >= b + 1 ]
	start location:	f26
	leaf cost:	0

A polynomial rank function with
	Pol(f6) = 1
	Pol(f11) = -1
	Pol(f26) = 1
orients all transitions weakly and the transition
	f6(a, b, e, f, g, h) -> f11(a, j1, f, f, g, h) [ j1 >= a + 1 /\ g >= 0 /\ h >= 1 /\ f = e ]
strictly and produces the following problem:
4:	T:
		(1, 1)    f6(a, b, e, f, g, h) -> f11(a, j1, f, f, g, h) [ j1 >= a + 1 /\ g >= 0 /\ h >= 1 /\ f = e ]
		(1, 1)    f6(a, b, e, f, g, h) -> f11(a, j1, f, f, g, h) [ a >= j1 + 1 /\ g >= 0 /\ h >= 1 /\ f = e ]
		(1, 1)    f26(a, b, e, f, g, h) -> f6(a, b, e, l1, 1, 4) [ i1 >= e + 1 ]
		(1, 1)    f26(a, b, e, f, g, h) -> f6(a, b, e, l1, 1, 4) [ e >= i1 + 1 ]
		(?, 1)    f6(a, b, e, f, g, h) -> f6(a, b, e, h1, g + 1, h - 1) [ f >= e + 1 /\ g >= 0 /\ h >= 1 ]
		(?, 1)    f6(a, b, e, f, g, h) -> f6(a, b, e, h1, g + 1, h - 1) [ e >= f + 1 /\ g >= 0 /\ h >= 1 ]
		(?, 1)    f11(a, b, e, f, g, h) -> f11(a, b, e, f, g, h) [ b >= a + 1 ]
		(?, 1)    f11(a, b, e, f, g, h) -> f11(a, b, e, f, g, h) [ a >= b + 1 ]
	start location:	f26
	leaf cost:	0

A polynomial rank function with
	Pol(f6) = V_5 + 2*V_6 - 1
	Pol(f11) = -V_3 + V_4 + V_5 + 2*V_6 - 1
	Pol(f26) = 8
orients all transitions weakly and the transitions
	f6(a, b, e, f, g, h) -> f6(a, b, e, h1, g + 1, h - 1) [ f >= e + 1 /\ g >= 0 /\ h >= 1 ]
	f6(a, b, e, f, g, h) -> f6(a, b, e, h1, g + 1, h - 1) [ e >= f + 1 /\ g >= 0 /\ h >= 1 ]
strictly and produces the following problem:
5:	T:
		(1, 1)    f6(a, b, e, f, g, h) -> f11(a, j1, f, f, g, h) [ j1 >= a + 1 /\ g >= 0 /\ h >= 1 /\ f = e ]
		(1, 1)    f6(a, b, e, f, g, h) -> f11(a, j1, f, f, g, h) [ a >= j1 + 1 /\ g >= 0 /\ h >= 1 /\ f = e ]
		(1, 1)    f26(a, b, e, f, g, h) -> f6(a, b, e, l1, 1, 4) [ i1 >= e + 1 ]
		(1, 1)    f26(a, b, e, f, g, h) -> f6(a, b, e, l1, 1, 4) [ e >= i1 + 1 ]
		(8, 1)    f6(a, b, e, f, g, h) -> f6(a, b, e, h1, g + 1, h - 1) [ f >= e + 1 /\ g >= 0 /\ h >= 1 ]
		(8, 1)    f6(a, b, e, f, g, h) -> f6(a, b, e, h1, g + 1, h - 1) [ e >= f + 1 /\ g >= 0 /\ h >= 1 ]
		(?, 1)    f11(a, b, e, f, g, h) -> f11(a, b, e, f, g, h) [ b >= a + 1 ]
		(?, 1)    f11(a, b, e, f, g, h) -> f11(a, b, e, f, g, h) [ a >= b + 1 ]
	start location:	f26
	leaf cost:	0

Applied AI with 'oct' on problem 5 to obtain the following invariants:
  For symbol f11: -X_6 + 4 >= 0 /\ X_5 - X_6 + 3 >= 0 /\ -X_5 - X_6 + 5 >= 0 /\ X_6 - 1 >= 0 /\ X_5 + X_6 - 5 >= 0 /\ -X_5 + X_6 + 3 >= 0 /\ -X_5 + 4 >= 0 /\ X_5 - 1 >= 0 /\ X_3 - X_4 >= 0 /\ -X_3 + X_4 >= 0
  For symbol f6: -X_6 + 4 >= 0 /\ X_5 - X_6 + 3 >= 0 /\ -X_5 - X_6 + 5 >= 0 /\ X_5 + X_6 - 5 >= 0 /\ X_5 - 1 >= 0


This yielded the following problem:
6:	T:
		(?, 1)    f11(a, b, e, f, g, h) -> f11(a, b, e, f, g, h) [ -h + 4 >= 0 /\ g - h + 3 >= 0 /\ -g - h + 5 >= 0 /\ h - 1 >= 0 /\ g + h - 5 >= 0 /\ -g + h + 3 >= 0 /\ -g + 4 >= 0 /\ g - 1 >= 0 /\ e - f >= 0 /\ -e + f >= 0 /\ a >= b + 1 ]
		(?, 1)    f11(a, b, e, f, g, h) -> f11(a, b, e, f, g, h) [ -h + 4 >= 0 /\ g - h + 3 >= 0 /\ -g - h + 5 >= 0 /\ h - 1 >= 0 /\ g + h - 5 >= 0 /\ -g + h + 3 >= 0 /\ -g + 4 >= 0 /\ g - 1 >= 0 /\ e - f >= 0 /\ -e + f >= 0 /\ b >= a + 1 ]
		(8, 1)    f6(a, b, e, f, g, h) -> f6(a, b, e, h1, g + 1, h - 1) [ -h + 4 >= 0 /\ g - h + 3 >= 0 /\ -g - h + 5 >= 0 /\ g + h - 5 >= 0 /\ g - 1 >= 0 /\ e >= f + 1 /\ g >= 0 /\ h >= 1 ]
		(8, 1)    f6(a, b, e, f, g, h) -> f6(a, b, e, h1, g + 1, h - 1) [ -h + 4 >= 0 /\ g - h + 3 >= 0 /\ -g - h + 5 >= 0 /\ g + h - 5 >= 0 /\ g - 1 >= 0 /\ f >= e + 1 /\ g >= 0 /\ h >= 1 ]
		(1, 1)    f26(a, b, e, f, g, h) -> f6(a, b, e, l1, 1, 4) [ e >= i1 + 1 ]
		(1, 1)    f26(a, b, e, f, g, h) -> f6(a, b, e, l1, 1, 4) [ i1 >= e + 1 ]
		(1, 1)    f6(a, b, e, f, g, h) -> f11(a, j1, f, f, g, h) [ -h + 4 >= 0 /\ g - h + 3 >= 0 /\ -g - h + 5 >= 0 /\ g + h - 5 >= 0 /\ g - 1 >= 0 /\ a >= j1 + 1 /\ g >= 0 /\ h >= 1 /\ f = e ]
		(1, 1)    f6(a, b, e, f, g, h) -> f11(a, j1, f, f, g, h) [ -h + 4 >= 0 /\ g - h + 3 >= 0 /\ -g - h + 5 >= 0 /\ g + h - 5 >= 0 /\ g - 1 >= 0 /\ j1 >= a + 1 /\ g >= 0 /\ h >= 1 /\ f = e ]
	start location:	f26
	leaf cost:	0

By chaining the transition f6(a, b, e, f, g, h) -> f11(a, j1, f, f, g, h) [ -h + 4 >= 0 /\ g - h + 3 >= 0 /\ -g - h + 5 >= 0 /\ g + h - 5 >= 0 /\ g - 1 >= 0 /\ a >= j1 + 1 /\ g >= 0 /\ h >= 1 /\ f = e ] with all transitions in problem 6, the following new transition is obtained:
	f6(a, b, e, f, g, h) -> f11(a, j1, f, f, g, h) [ -h + 4 >= 0 /\ g - h + 3 >= 0 /\ -g - h + 5 >= 0 /\ g + h - 5 >= 0 /\ g - 1 >= 0 /\ a >= j1 + 1 /\ g >= 0 /\ h >= 1 /\ f = e /\ h - 1 >= 0 /\ -g + h + 3 >= 0 /\ -g + 4 >= 0 /\ 0 >= 0 ]
We thus obtain the following problem:
7:	T:
		(1, 2)    f6(a, b, e, f, g, h) -> f11(a, j1, f, f, g, h) [ -h + 4 >= 0 /\ g - h + 3 >= 0 /\ -g - h + 5 >= 0 /\ g + h - 5 >= 0 /\ g - 1 >= 0 /\ a >= j1 + 1 /\ g >= 0 /\ h >= 1 /\ f = e /\ h - 1 >= 0 /\ -g + h + 3 >= 0 /\ -g + 4 >= 0 /\ 0 >= 0 ]
		(?, 1)    f11(a, b, e, f, g, h) -> f11(a, b, e, f, g, h) [ -h + 4 >= 0 /\ g - h + 3 >= 0 /\ -g - h + 5 >= 0 /\ h - 1 >= 0 /\ g + h - 5 >= 0 /\ -g + h + 3 >= 0 /\ -g + 4 >= 0 /\ g - 1 >= 0 /\ e - f >= 0 /\ -e + f >= 0 /\ a >= b + 1 ]
		(?, 1)    f11(a, b, e, f, g, h) -> f11(a, b, e, f, g, h) [ -h + 4 >= 0 /\ g - h + 3 >= 0 /\ -g - h + 5 >= 0 /\ h - 1 >= 0 /\ g + h - 5 >= 0 /\ -g + h + 3 >= 0 /\ -g + 4 >= 0 /\ g - 1 >= 0 /\ e - f >= 0 /\ -e + f >= 0 /\ b >= a + 1 ]
		(8, 1)    f6(a, b, e, f, g, h) -> f6(a, b, e, h1, g + 1, h - 1) [ -h + 4 >= 0 /\ g - h + 3 >= 0 /\ -g - h + 5 >= 0 /\ g + h - 5 >= 0 /\ g - 1 >= 0 /\ e >= f + 1 /\ g >= 0 /\ h >= 1 ]
		(8, 1)    f6(a, b, e, f, g, h) -> f6(a, b, e, h1, g + 1, h - 1) [ -h + 4 >= 0 /\ g - h + 3 >= 0 /\ -g - h + 5 >= 0 /\ g + h - 5 >= 0 /\ g - 1 >= 0 /\ f >= e + 1 /\ g >= 0 /\ h >= 1 ]
		(1, 1)    f26(a, b, e, f, g, h) -> f6(a, b, e, l1, 1, 4) [ e >= i1 + 1 ]
		(1, 1)    f26(a, b, e, f, g, h) -> f6(a, b, e, l1, 1, 4) [ i1 >= e + 1 ]
		(1, 1)    f6(a, b, e, f, g, h) -> f11(a, j1, f, f, g, h) [ -h + 4 >= 0 /\ g - h + 3 >= 0 /\ -g - h + 5 >= 0 /\ g + h - 5 >= 0 /\ g - 1 >= 0 /\ j1 >= a + 1 /\ g >= 0 /\ h >= 1 /\ f = e ]
	start location:	f26
	leaf cost:	0

Complexity upper bound ?

Time: 1.293 sec (SMT: 1.202 sec)