MAYBE

Initial complexity problem:
1:	T:
		(1, 1)    f33(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) -> f3(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)
		(?, 1)    f3(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) -> f25(g1, b, b, 0, 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) [ a >= 1 /\ b >= 1 /\ g1 >= 1 ]
		(?, 1)    f3(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) -> f25(g1, b, b, 0, 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) [ a >= 1 /\ 0 >= b + 1 /\ g1 >= 1 ]
		(?, 1)    f3(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) -> f16(j, b, c, d, g1, h1, h1, h1, h1, j + 1, h1, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1)
		(?, 1)    f3(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) -> f16(h1 + 1, b, c, d, e, g1, g1, g1, g1, j + 1, g1, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) [ h1 >= 0 /\ a >= 0 ]
		(?, 1)    f3(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) -> f22(g1, l, 0, 0, e, f, g, h, l, j, k, l, l, l, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) [ h1 >= 1 /\ a >= 1 /\ b = 0 ]
		(?, 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, b1, c1, d1, e1, f1) -> f17(a, b, c, d, e, f, g, h, i, k1, 0, l, 0, n, g1, h1, j1, g1, l1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) [ g1 >= 1 /\ 0 >= i1 ]
		(?, 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, b1, c1, d1, e1, f1) -> f17(a, b, c, d, e, f, g, h, i, k1, 0, l, 0, n, g1, h1, j1, g1, l1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) [ 0 >= g1 + 1 /\ 0 >= i1 ]
		(?, 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, b1, c1, d1, e1, f1) -> f21(a, b, c, d, e, f, g, h, g1, k1, 0, l, 0, n, 0, h1, j1, 0, l1, 0, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) [ 0 >= i1 ]
		(?, 1)    f16(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) -> f16(h1 + 1, b, c, d, e, g1, g1, g1, g1, l1 + 1, g1, l, m, n, o, j1, k1, r, s, t, i1, n1, o1, p1, q1, z, a1, b1, c1, d1, e1, f1) [ a >= 0 /\ m1 >= 0 /\ q >= j + 1 /\ h1 >= 0 ]
		(?, 1)    f16(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) -> f18(g1, b, c, d, e, f, g, h, i, k1, k, l, 0, n, 0, h1, j1, 0, s, t, u, v, w, x, y, l1, a1, b1, c1, d1, e1, f1) [ a >= 0 /\ i1 >= 0 /\ j >= q /\ g1 >= 0 ]
		(?, 1)    f16(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) -> f3(g1, n1, c, d, e, f, g, h, i, i1, j1, q1, 0, n, h1, k1, l1, m1, s, t, u, v, w, x, y, v1, o1, p1, t1, u1, e1, f1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 ]
		(?, 1)    f16(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) -> f3(g1, n1, c, d, e, f, g, h, i, i1, j1, q1, 0, n, h1, k1, l1, m1, s, t, u, v, w, x, y, v1, o1, p1, t1, u1, e1, f1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ 0 >= o1 + 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, b1, c1, d1, e1, f1) -> f16(h1, b, c, d, e, g1, g1, g1, g1, h1 + 1, g1, l, m, n, o, j1, k1, r, s, t, l1, i1, n1, x, y, z, a1, b1, c1, d1, o1, p1) [ q1 >= 1 ]
	start location:	f33
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, j, l, q].
We thus obtain the following problem:
2:	T:
		(?, 1)    f23(a, b, j, l, q) -> f16(h1, b, h1 + 1, l, k1) [ q1 >= 1 ]
		(?, 1)    f16(a, b, j, l, q) -> f3(g1, n1, i1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ 0 >= o1 + 1 ]
		(?, 1)    f16(a, b, j, l, q) -> f3(g1, n1, i1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 ]
		(?, 1)    f16(a, b, j, l, q) -> f18(g1, b, k1, l, j1) [ a >= 0 /\ i1 >= 0 /\ j >= q /\ g1 >= 0 ]
		(?, 1)    f16(a, b, j, l, q) -> f16(h1 + 1, b, l1 + 1, l, k1) [ a >= 0 /\ m1 >= 0 /\ q >= j + 1 /\ h1 >= 0 ]
		(?, 1)    f23(a, b, j, l, q) -> f21(a, b, k1, l, j1) [ 0 >= i1 ]
		(?, 1)    f23(a, b, j, l, q) -> f17(a, b, k1, l, j1) [ 0 >= g1 + 1 /\ 0 >= i1 ]
		(?, 1)    f23(a, b, j, l, q) -> f17(a, b, k1, l, j1) [ g1 >= 1 /\ 0 >= i1 ]
		(?, 1)    f3(a, b, j, l, q) -> f22(g1, l, j, l, q) [ h1 >= 1 /\ a >= 1 /\ b = 0 ]
		(?, 1)    f3(a, b, j, l, q) -> f16(h1 + 1, b, j + 1, l, q) [ h1 >= 0 /\ a >= 0 ]
		(?, 1)    f3(a, b, j, l, q) -> f16(j, b, j + 1, l, q)
		(?, 1)    f3(a, b, j, l, q) -> f25(g1, b, j, l, q) [ a >= 1 /\ 0 >= b + 1 /\ g1 >= 1 ]
		(?, 1)    f3(a, b, j, l, q) -> f25(g1, b, j, l, q) [ a >= 1 /\ b >= 1 /\ g1 >= 1 ]
		(1, 1)    f33(a, b, j, l, q) -> f3(a, b, j, l, q)
	start location:	f33
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(?, 1)    f23(a, b, j, l, q) -> f16(h1, b, h1 + 1, l, k1) [ q1 >= 1 ]
		(?, 1)    f16(a, b, j, l, q) -> f3(g1, n1, i1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ 0 >= o1 + 1 ]
		(?, 1)    f16(a, b, j, l, q) -> f3(g1, n1, i1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 ]
		(?, 1)    f16(a, b, j, l, q) -> f16(h1 + 1, b, l1 + 1, l, k1) [ a >= 0 /\ m1 >= 0 /\ q >= j + 1 /\ h1 >= 0 ]
		(?, 1)    f3(a, b, j, l, q) -> f16(h1 + 1, b, j + 1, l, q) [ h1 >= 0 /\ a >= 0 ]
		(?, 1)    f3(a, b, j, l, q) -> f16(j, b, j + 1, l, q)
		(1, 1)    f33(a, b, j, l, q) -> f3(a, b, j, l, q)
	start location:	f33
	leaf cost:	7

Testing for reachability in the complexity graph removes the following transition from problem 3:
	f23(a, b, j, l, q) -> f16(h1, b, h1 + 1, l, k1) [ q1 >= 1 ]
We thus obtain the following problem:
4:	T:
		(?, 1)    f16(a, b, j, l, q) -> f16(h1 + 1, b, l1 + 1, l, k1) [ a >= 0 /\ m1 >= 0 /\ q >= j + 1 /\ h1 >= 0 ]
		(?, 1)    f16(a, b, j, l, q) -> f3(g1, n1, i1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 ]
		(?, 1)    f16(a, b, j, l, q) -> f3(g1, n1, i1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ 0 >= o1 + 1 ]
		(?, 1)    f3(a, b, j, l, q) -> f16(j, b, j + 1, l, q)
		(?, 1)    f3(a, b, j, l, q) -> f16(h1 + 1, b, j + 1, l, q) [ h1 >= 0 /\ a >= 0 ]
		(1, 1)    f33(a, b, j, l, q) -> f3(a, b, j, l, q)
	start location:	f33
	leaf cost:	7

By chaining the transition f16(a, b, j, l, q) -> f3(g1, n1, i1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 ] with all transitions in problem 4, the following new transitions are obtained:
	f16(a, b, j, l, q) -> f16(i1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 ]
	f16(a, b, j, l, q) -> f16(h1 + 1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 /\ h1 >= 0 /\ g1 >= 0 ]
We thus obtain the following problem:
5:	T:
		(?, 2)    f16(a, b, j, l, q) -> f16(i1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 ]
		(?, 2)    f16(a, b, j, l, q) -> f16(h1 + 1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 /\ h1 >= 0 /\ g1 >= 0 ]
		(?, 1)    f16(a, b, j, l, q) -> f16(h1 + 1, b, l1 + 1, l, k1) [ a >= 0 /\ m1 >= 0 /\ q >= j + 1 /\ h1 >= 0 ]
		(?, 1)    f16(a, b, j, l, q) -> f3(g1, n1, i1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ 0 >= o1 + 1 ]
		(?, 1)    f3(a, b, j, l, q) -> f16(j, b, j + 1, l, q)
		(?, 1)    f3(a, b, j, l, q) -> f16(h1 + 1, b, j + 1, l, q) [ h1 >= 0 /\ a >= 0 ]
		(1, 1)    f33(a, b, j, l, q) -> f3(a, b, j, l, q)
	start location:	f33
	leaf cost:	7

By chaining the transition f16(a, b, j, l, q) -> f3(g1, n1, i1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ 0 >= o1 + 1 ] with all transitions in problem 5, the following new transitions are obtained:
	f16(a, b, j, l, q) -> f16(i1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ 0 >= o1 + 1 ]
	f16(a, b, j, l, q) -> f16(h1 + 1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ 0 >= o1 + 1 /\ h1 >= 0 /\ g1 >= 0 ]
We thus obtain the following problem:
6:	T:
		(?, 2)    f16(a, b, j, l, q) -> f16(i1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ 0 >= o1 + 1 ]
		(?, 2)    f16(a, b, j, l, q) -> f16(h1 + 1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ 0 >= o1 + 1 /\ h1 >= 0 /\ g1 >= 0 ]
		(?, 2)    f16(a, b, j, l, q) -> f16(i1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 ]
		(?, 2)    f16(a, b, j, l, q) -> f16(h1 + 1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 /\ h1 >= 0 /\ g1 >= 0 ]
		(?, 1)    f16(a, b, j, l, q) -> f16(h1 + 1, b, l1 + 1, l, k1) [ a >= 0 /\ m1 >= 0 /\ q >= j + 1 /\ h1 >= 0 ]
		(?, 1)    f3(a, b, j, l, q) -> f16(j, b, j + 1, l, q)
		(?, 1)    f3(a, b, j, l, q) -> f16(h1 + 1, b, j + 1, l, q) [ h1 >= 0 /\ a >= 0 ]
		(1, 1)    f33(a, b, j, l, q) -> f3(a, b, j, l, q)
	start location:	f33
	leaf cost:	7

Repeatedly propagating knowledge in problem 6 produces the following problem:
7:	T:
		(?, 2)    f16(a, b, j, l, q) -> f16(i1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ 0 >= o1 + 1 ]
		(?, 2)    f16(a, b, j, l, q) -> f16(h1 + 1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ 0 >= o1 + 1 /\ h1 >= 0 /\ g1 >= 0 ]
		(?, 2)    f16(a, b, j, l, q) -> f16(i1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 ]
		(?, 2)    f16(a, b, j, l, q) -> f16(h1 + 1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 /\ h1 >= 0 /\ g1 >= 0 ]
		(?, 1)    f16(a, b, j, l, q) -> f16(h1 + 1, b, l1 + 1, l, k1) [ a >= 0 /\ m1 >= 0 /\ q >= j + 1 /\ h1 >= 0 ]
		(1, 1)    f3(a, b, j, l, q) -> f16(j, b, j + 1, l, q)
		(1, 1)    f3(a, b, j, l, q) -> f16(h1 + 1, b, j + 1, l, q) [ h1 >= 0 /\ a >= 0 ]
		(1, 1)    f33(a, b, j, l, q) -> f3(a, b, j, l, q)
	start location:	f33
	leaf cost:	7

By chaining the transition f33(a, b, j, l, q) -> f3(a, b, j, l, q) with all transitions in problem 7, the following new transitions are obtained:
	f33(a, b, j, l, q) -> f16(j, b, j + 1, l, q)
	f33(a, b, j, l, q) -> f16(h1 + 1, b, j + 1, l, q) [ h1 >= 0 /\ a >= 0 ]
We thus obtain the following problem:
8:	T:
		(1, 2)    f33(a, b, j, l, q) -> f16(j, b, j + 1, l, q)
		(1, 2)    f33(a, b, j, l, q) -> f16(h1 + 1, b, j + 1, l, q) [ h1 >= 0 /\ a >= 0 ]
		(?, 2)    f16(a, b, j, l, q) -> f16(i1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ 0 >= o1 + 1 ]
		(?, 2)    f16(a, b, j, l, q) -> f16(h1 + 1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ 0 >= o1 + 1 /\ h1 >= 0 /\ g1 >= 0 ]
		(?, 2)    f16(a, b, j, l, q) -> f16(i1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 ]
		(?, 2)    f16(a, b, j, l, q) -> f16(h1 + 1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 /\ h1 >= 0 /\ g1 >= 0 ]
		(?, 1)    f16(a, b, j, l, q) -> f16(h1 + 1, b, l1 + 1, l, k1) [ a >= 0 /\ m1 >= 0 /\ q >= j + 1 /\ h1 >= 0 ]
		(1, 1)    f3(a, b, j, l, q) -> f16(j, b, j + 1, l, q)
		(1, 1)    f3(a, b, j, l, q) -> f16(h1 + 1, b, j + 1, l, q) [ h1 >= 0 /\ a >= 0 ]
	start location:	f33
	leaf cost:	7

Testing for reachability in the complexity graph removes the following transitions from problem 8:
	f3(a, b, j, l, q) -> f16(j, b, j + 1, l, q)
	f3(a, b, j, l, q) -> f16(h1 + 1, b, j + 1, l, q) [ h1 >= 0 /\ a >= 0 ]
We thus obtain the following problem:
9:	T:
		(?, 2)    f16(a, b, j, l, q) -> f16(h1 + 1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ 0 >= o1 + 1 /\ h1 >= 0 /\ g1 >= 0 ]
		(?, 2)    f16(a, b, j, l, q) -> f16(i1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ 0 >= o1 + 1 ]
		(?, 2)    f16(a, b, j, l, q) -> f16(h1 + 1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 /\ h1 >= 0 /\ g1 >= 0 ]
		(?, 2)    f16(a, b, j, l, q) -> f16(i1, n1, i1 + 1, q1, l1) [ a >= 0 /\ r1 >= 0 /\ s1 >= 0 /\ j >= q /\ o1 >= 1 ]
		(?, 1)    f16(a, b, j, l, q) -> f16(h1 + 1, b, l1 + 1, l, k1) [ a >= 0 /\ m1 >= 0 /\ q >= j + 1 /\ h1 >= 0 ]
		(1, 2)    f33(a, b, j, l, q) -> f16(h1 + 1, b, j + 1, l, q) [ h1 >= 0 /\ a >= 0 ]
		(1, 2)    f33(a, b, j, l, q) -> f16(j, b, j + 1, l, q)
	start location:	f33
	leaf cost:	7

Complexity upper bound ?

Time: 0.743 sec (SMT: 0.675 sec)