MAYBE

Initial complexity problem:
1:	T:
		(?, 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, z, a1) -> f8(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) [ a >= b + 1 ]
		(?, 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, z, a1) -> f8(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) [ b >= a + 1 ]
		(?, 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) -> f2(a, b, c, d, e, b1, g - 1, h + 1, h + 1, g - 1, c1, d1, g - 1, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) [ e >= f + 1 /\ g >= 1 /\ h >= 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) -> f2(a, b, c, d, e, b1, g - 1, h + 1, h + 1, g - 1, c1, d1, g - 1, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) [ f >= e + 1 /\ g >= 1 /\ h >= 0 ]
		(1, 1)    f23(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) -> f2(a, b, c, d, e, b1, 2, 1, 1, 2, k, l, m, 2, c1, d1, f1, g1, g1, g1, g1, h1, i1, 2, j1, 0, a1) [ e >= e1 + 1 ]
		(1, 1)    f23(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) -> f2(a, b, c, d, e, b1, 2, 1, 1, 2, k, l, m, 2, c1, d1, f1, g1, g1, g1, g1, h1, i1, 2, j1, 0, a1) [ e1 >= e + 1 ]
		(?, 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) -> f8(a, c1, c1, c1, f, f, g, h, i, j, k, l, m, n, o, p, b1, r, s, t, d1, v, w, x, y, z, f1) [ a >= c1 + 1 /\ g >= 1 /\ h >= 0 /\ f = e ]
		(?, 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) -> f8(a, c1, c1, c1, f, f, g, h, i, j, k, l, m, n, o, p, b1, r, s, t, d1, v, w, x, y, z, f1) [ c1 >= a + 1 /\ g >= 1 /\ h >= 0 /\ f = e ]
	start location:	f23
	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)    f2(a, b, e, f, g, h) -> f8(a, c1, f, f, g, h) [ c1 >= a + 1 /\ g >= 1 /\ h >= 0 /\ f = e ]
		(?, 1)    f2(a, b, e, f, g, h) -> f8(a, c1, f, f, g, h) [ a >= c1 + 1 /\ g >= 1 /\ h >= 0 /\ f = e ]
		(1, 1)    f23(a, b, e, f, g, h) -> f2(a, b, e, b1, 2, 1) [ e1 >= e + 1 ]
		(1, 1)    f23(a, b, e, f, g, h) -> f2(a, b, e, b1, 2, 1) [ e >= e1 + 1 ]
		(?, 1)    f2(a, b, e, f, g, h) -> f2(a, b, e, b1, g - 1, h + 1) [ f >= e + 1 /\ g >= 1 /\ h >= 0 ]
		(?, 1)    f2(a, b, e, f, g, h) -> f2(a, b, e, b1, g - 1, h + 1) [ e >= f + 1 /\ g >= 1 /\ h >= 0 ]
		(?, 1)    f8(a, b, e, f, g, h) -> f8(a, b, e, f, g, h) [ b >= a + 1 ]
		(?, 1)    f8(a, b, e, f, g, h) -> f8(a, b, e, f, g, h) [ a >= b + 1 ]
	start location:	f23
	leaf cost:	0

A polynomial rank function with
	Pol(f2) = 1
	Pol(f8) = -1
	Pol(f23) = 1
orients all transitions weakly and the transition
	f2(a, b, e, f, g, h) -> f8(a, c1, f, f, g, h) [ a >= c1 + 1 /\ g >= 1 /\ h >= 0 /\ f = e ]
strictly and produces the following problem:
3:	T:
		(?, 1)    f2(a, b, e, f, g, h) -> f8(a, c1, f, f, g, h) [ c1 >= a + 1 /\ g >= 1 /\ h >= 0 /\ f = e ]
		(1, 1)    f2(a, b, e, f, g, h) -> f8(a, c1, f, f, g, h) [ a >= c1 + 1 /\ g >= 1 /\ h >= 0 /\ f = e ]
		(1, 1)    f23(a, b, e, f, g, h) -> f2(a, b, e, b1, 2, 1) [ e1 >= e + 1 ]
		(1, 1)    f23(a, b, e, f, g, h) -> f2(a, b, e, b1, 2, 1) [ e >= e1 + 1 ]
		(?, 1)    f2(a, b, e, f, g, h) -> f2(a, b, e, b1, g - 1, h + 1) [ f >= e + 1 /\ g >= 1 /\ h >= 0 ]
		(?, 1)    f2(a, b, e, f, g, h) -> f2(a, b, e, b1, g - 1, h + 1) [ e >= f + 1 /\ g >= 1 /\ h >= 0 ]
		(?, 1)    f8(a, b, e, f, g, h) -> f8(a, b, e, f, g, h) [ b >= a + 1 ]
		(?, 1)    f8(a, b, e, f, g, h) -> f8(a, b, e, f, g, h) [ a >= b + 1 ]
	start location:	f23
	leaf cost:	0

A polynomial rank function with
	Pol(f2) = 1
	Pol(f8) = -1
	Pol(f23) = 1
orients all transitions weakly and the transition
	f2(a, b, e, f, g, h) -> f8(a, c1, f, f, g, h) [ c1 >= a + 1 /\ g >= 1 /\ h >= 0 /\ f = e ]
strictly and produces the following problem:
4:	T:
		(1, 1)    f2(a, b, e, f, g, h) -> f8(a, c1, f, f, g, h) [ c1 >= a + 1 /\ g >= 1 /\ h >= 0 /\ f = e ]
		(1, 1)    f2(a, b, e, f, g, h) -> f8(a, c1, f, f, g, h) [ a >= c1 + 1 /\ g >= 1 /\ h >= 0 /\ f = e ]
		(1, 1)    f23(a, b, e, f, g, h) -> f2(a, b, e, b1, 2, 1) [ e1 >= e + 1 ]
		(1, 1)    f23(a, b, e, f, g, h) -> f2(a, b, e, b1, 2, 1) [ e >= e1 + 1 ]
		(?, 1)    f2(a, b, e, f, g, h) -> f2(a, b, e, b1, g - 1, h + 1) [ f >= e + 1 /\ g >= 1 /\ h >= 0 ]
		(?, 1)    f2(a, b, e, f, g, h) -> f2(a, b, e, b1, g - 1, h + 1) [ e >= f + 1 /\ g >= 1 /\ h >= 0 ]
		(?, 1)    f8(a, b, e, f, g, h) -> f8(a, b, e, f, g, h) [ b >= a + 1 ]
		(?, 1)    f8(a, b, e, f, g, h) -> f8(a, b, e, f, g, h) [ a >= b + 1 ]
	start location:	f23
	leaf cost:	0

A polynomial rank function with
	Pol(f2) = 2*V_5 + V_6 - 1
	Pol(f8) = -V_3 + V_4 + 2*V_5 + V_6 - 1
	Pol(f23) = 4
orients all transitions weakly and the transitions
	f2(a, b, e, f, g, h) -> f2(a, b, e, b1, g - 1, h + 1) [ f >= e + 1 /\ g >= 1 /\ h >= 0 ]
	f2(a, b, e, f, g, h) -> f2(a, b, e, b1, g - 1, h + 1) [ e >= f + 1 /\ g >= 1 /\ h >= 0 ]
strictly and produces the following problem:
5:	T:
		(1, 1)    f2(a, b, e, f, g, h) -> f8(a, c1, f, f, g, h) [ c1 >= a + 1 /\ g >= 1 /\ h >= 0 /\ f = e ]
		(1, 1)    f2(a, b, e, f, g, h) -> f8(a, c1, f, f, g, h) [ a >= c1 + 1 /\ g >= 1 /\ h >= 0 /\ f = e ]
		(1, 1)    f23(a, b, e, f, g, h) -> f2(a, b, e, b1, 2, 1) [ e1 >= e + 1 ]
		(1, 1)    f23(a, b, e, f, g, h) -> f2(a, b, e, b1, 2, 1) [ e >= e1 + 1 ]
		(4, 1)    f2(a, b, e, f, g, h) -> f2(a, b, e, b1, g - 1, h + 1) [ f >= e + 1 /\ g >= 1 /\ h >= 0 ]
		(4, 1)    f2(a, b, e, f, g, h) -> f2(a, b, e, b1, g - 1, h + 1) [ e >= f + 1 /\ g >= 1 /\ h >= 0 ]
		(?, 1)    f8(a, b, e, f, g, h) -> f8(a, b, e, f, g, h) [ b >= a + 1 ]
		(?, 1)    f8(a, b, e, f, g, h) -> f8(a, b, e, f, g, h) [ a >= b + 1 ]
	start location:	f23
	leaf cost:	0

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


This yielded the following problem:
6:	T:
		(?, 1)    f8(a, b, e, f, g, h) -> f8(a, b, e, f, g, h) [ -h + 2 >= 0 /\ g - h + 1 >= 0 /\ -g - h + 3 >= 0 /\ h - 1 >= 0 /\ g + h - 3 >= 0 /\ -g + h + 1 >= 0 /\ -g + 2 >= 0 /\ g - 1 >= 0 /\ e - f >= 0 /\ -e + f >= 0 /\ a >= b + 1 ]
		(?, 1)    f8(a, b, e, f, g, h) -> f8(a, b, e, f, g, h) [ -h + 2 >= 0 /\ g - h + 1 >= 0 /\ -g - h + 3 >= 0 /\ h - 1 >= 0 /\ g + h - 3 >= 0 /\ -g + h + 1 >= 0 /\ -g + 2 >= 0 /\ g - 1 >= 0 /\ e - f >= 0 /\ -e + f >= 0 /\ b >= a + 1 ]
		(4, 1)    f2(a, b, e, f, g, h) -> f2(a, b, e, b1, g - 1, h + 1) [ -g - h + 3 >= 0 /\ h - 1 >= 0 /\ g + h - 3 >= 0 /\ -g + h + 1 >= 0 /\ -g + 2 >= 0 /\ e >= f + 1 /\ g >= 1 /\ h >= 0 ]
		(4, 1)    f2(a, b, e, f, g, h) -> f2(a, b, e, b1, g - 1, h + 1) [ -g - h + 3 >= 0 /\ h - 1 >= 0 /\ g + h - 3 >= 0 /\ -g + h + 1 >= 0 /\ -g + 2 >= 0 /\ f >= e + 1 /\ g >= 1 /\ h >= 0 ]
		(1, 1)    f23(a, b, e, f, g, h) -> f2(a, b, e, b1, 2, 1) [ e >= e1 + 1 ]
		(1, 1)    f23(a, b, e, f, g, h) -> f2(a, b, e, b1, 2, 1) [ e1 >= e + 1 ]
		(1, 1)    f2(a, b, e, f, g, h) -> f8(a, c1, f, f, g, h) [ -g - h + 3 >= 0 /\ h - 1 >= 0 /\ g + h - 3 >= 0 /\ -g + h + 1 >= 0 /\ -g + 2 >= 0 /\ a >= c1 + 1 /\ g >= 1 /\ h >= 0 /\ f = e ]
		(1, 1)    f2(a, b, e, f, g, h) -> f8(a, c1, f, f, g, h) [ -g - h + 3 >= 0 /\ h - 1 >= 0 /\ g + h - 3 >= 0 /\ -g + h + 1 >= 0 /\ -g + 2 >= 0 /\ c1 >= a + 1 /\ g >= 1 /\ h >= 0 /\ f = e ]
	start location:	f23
	leaf cost:	0

By chaining the transition f2(a, b, e, f, g, h) -> f8(a, c1, f, f, g, h) [ -g - h + 3 >= 0 /\ h - 1 >= 0 /\ g + h - 3 >= 0 /\ -g + h + 1 >= 0 /\ -g + 2 >= 0 /\ a >= c1 + 1 /\ g >= 1 /\ h >= 0 /\ f = e ] with all transitions in problem 6, the following new transition is obtained:
	f2(a, b, e, f, g, h) -> f8(a, c1, f, f, g, h) [ -g - h + 3 >= 0 /\ h - 1 >= 0 /\ g + h - 3 >= 0 /\ -g + h + 1 >= 0 /\ -g + 2 >= 0 /\ a >= c1 + 1 /\ g >= 1 /\ h >= 0 /\ f = e /\ -h + 2 >= 0 /\ g - h + 1 >= 0 /\ g - 1 >= 0 /\ 0 >= 0 ]
We thus obtain the following problem:
7:	T:
		(1, 2)    f2(a, b, e, f, g, h) -> f8(a, c1, f, f, g, h) [ -g - h + 3 >= 0 /\ h - 1 >= 0 /\ g + h - 3 >= 0 /\ -g + h + 1 >= 0 /\ -g + 2 >= 0 /\ a >= c1 + 1 /\ g >= 1 /\ h >= 0 /\ f = e /\ -h + 2 >= 0 /\ g - h + 1 >= 0 /\ g - 1 >= 0 /\ 0 >= 0 ]
		(?, 1)    f8(a, b, e, f, g, h) -> f8(a, b, e, f, g, h) [ -h + 2 >= 0 /\ g - h + 1 >= 0 /\ -g - h + 3 >= 0 /\ h - 1 >= 0 /\ g + h - 3 >= 0 /\ -g + h + 1 >= 0 /\ -g + 2 >= 0 /\ g - 1 >= 0 /\ e - f >= 0 /\ -e + f >= 0 /\ a >= b + 1 ]
		(?, 1)    f8(a, b, e, f, g, h) -> f8(a, b, e, f, g, h) [ -h + 2 >= 0 /\ g - h + 1 >= 0 /\ -g - h + 3 >= 0 /\ h - 1 >= 0 /\ g + h - 3 >= 0 /\ -g + h + 1 >= 0 /\ -g + 2 >= 0 /\ g - 1 >= 0 /\ e - f >= 0 /\ -e + f >= 0 /\ b >= a + 1 ]
		(4, 1)    f2(a, b, e, f, g, h) -> f2(a, b, e, b1, g - 1, h + 1) [ -g - h + 3 >= 0 /\ h - 1 >= 0 /\ g + h - 3 >= 0 /\ -g + h + 1 >= 0 /\ -g + 2 >= 0 /\ e >= f + 1 /\ g >= 1 /\ h >= 0 ]
		(4, 1)    f2(a, b, e, f, g, h) -> f2(a, b, e, b1, g - 1, h + 1) [ -g - h + 3 >= 0 /\ h - 1 >= 0 /\ g + h - 3 >= 0 /\ -g + h + 1 >= 0 /\ -g + 2 >= 0 /\ f >= e + 1 /\ g >= 1 /\ h >= 0 ]
		(1, 1)    f23(a, b, e, f, g, h) -> f2(a, b, e, b1, 2, 1) [ e >= e1 + 1 ]
		(1, 1)    f23(a, b, e, f, g, h) -> f2(a, b, e, b1, 2, 1) [ e1 >= e + 1 ]
		(1, 1)    f2(a, b, e, f, g, h) -> f8(a, c1, f, f, g, h) [ -g - h + 3 >= 0 /\ h - 1 >= 0 /\ g + h - 3 >= 0 /\ -g + h + 1 >= 0 /\ -g + 2 >= 0 /\ c1 >= a + 1 /\ g >= 1 /\ h >= 0 /\ f = e ]
	start location:	f23
	leaf cost:	0

Complexity upper bound ?

Time: 1.270 sec (SMT: 1.179 sec)