MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f0(a, b, c, d, e, f, g) -> f2(h, b, i, d, e, f, g) [ a >= b ]
		(?, 1)    f0(a, b, c, d, e, f, g) -> f0(h, b, c, i, 0, f, g) [ b >= a + 1 ]
		(?, 1)    f0(a, b, c, d, e, f, g) -> f0(h, b, c, i, j, k, g) [ 0 >= j + 1 /\ b >= a + 1 ]
		(?, 1)    f0(a, b, c, d, e, f, g) -> f0(h, b, c, i, j, k, g) [ j >= 1 /\ b >= a + 1 ]
		(1, 1)    f1(a, b, c, d, e, f, g) -> f0(a, b, c, d, e, f, h)
	start location:	f1
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(?, 1)    f0(a, b, c, d, e, f, g) -> f0(h, b, c, i, 0, f, g) [ b >= a + 1 ]
		(?, 1)    f0(a, b, c, d, e, f, g) -> f0(h, b, c, i, j, k, g) [ 0 >= j + 1 /\ b >= a + 1 ]
		(?, 1)    f0(a, b, c, d, e, f, g) -> f0(h, b, c, i, j, k, g) [ j >= 1 /\ b >= a + 1 ]
		(1, 1)    f1(a, b, c, d, e, f, g) -> f0(a, b, c, d, e, f, h)
	start location:	f1
	leaf cost:	1

Complexity upper bound ?

Time: 0.255 sec (SMT: 0.235 sec)