MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f10(a, b, c, d, e) -> f16(a, 0, f, f, e) [ 0 >= a ]
		(?, 1)    f16(a, b, c, d, e) -> f16(a, b, c, d, e) [ d >= 1 ]
		(?, 1)    f25(a, b, c, d, e) -> f25(a, b, c, d, e)
		(?, 1)    f27(a, b, c, d, e) -> f30(a, b, c, d, e)
		(?, 1)    f16(a, b, c, d, e) -> f10(f, b, f, d, 0) [ 0 >= d ]
		(?, 1)    f10(a, b, c, d, e) -> f25(a, b, c, d, e) [ a >= 1 ]
		(1, 1)    f0(a, b, c, d, e) -> f10(f, 0, f, d, 0)
	start location:	f0
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(?, 1)    f10(a, b, c, d, e) -> f16(a, 0, f, f, e) [ 0 >= a ]
		(?, 1)    f16(a, b, c, d, e) -> f16(a, b, c, d, e) [ d >= 1 ]
		(?, 1)    f25(a, b, c, d, e) -> f25(a, b, c, d, e)
		(?, 1)    f16(a, b, c, d, e) -> f10(f, b, f, d, 0) [ 0 >= d ]
		(?, 1)    f10(a, b, c, d, e) -> f25(a, b, c, d, e) [ a >= 1 ]
		(1, 1)    f0(a, b, c, d, e) -> f10(f, 0, f, d, 0)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f10) = 1
	Pol(f16) = 1
	Pol(f25) = 0
	Pol(f0) = 1
orients all transitions weakly and the transition
	f10(a, b, c, d, e) -> f25(a, b, c, d, e) [ a >= 1 ]
strictly and produces the following problem:
3:	T:
		(?, 1)    f10(a, b, c, d, e) -> f16(a, 0, f, f, e) [ 0 >= a ]
		(?, 1)    f16(a, b, c, d, e) -> f16(a, b, c, d, e) [ d >= 1 ]
		(?, 1)    f25(a, b, c, d, e) -> f25(a, b, c, d, e)
		(?, 1)    f16(a, b, c, d, e) -> f10(f, b, f, d, 0) [ 0 >= d ]
		(1, 1)    f10(a, b, c, d, e) -> f25(a, b, c, d, e) [ a >= 1 ]
		(1, 1)    f0(a, b, c, d, e) -> f10(f, 0, f, d, 0)
	start location:	f0
	leaf cost:	1

Applied AI with 'oct' on problem 3 to obtain the following invariants:
  For symbol f10: -X_5 >= 0 /\ X_2 - X_5 >= 0 /\ -X_2 - X_5 >= 0 /\ X_5 >= 0 /\ X_2 + X_5 >= 0 /\ -X_2 + X_5 >= 0 /\ -X_2 >= 0 /\ X_2 >= 0
  For symbol f16: -X_5 >= 0 /\ X_2 - X_5 >= 0 /\ -X_2 - X_5 >= 0 /\ -X_1 - X_5 >= 0 /\ X_5 >= 0 /\ X_2 + X_5 >= 0 /\ -X_2 + X_5 >= 0 /\ -X_1 + X_5 >= 0 /\ -X_2 >= 0 /\ -X_1 - X_2 >= 0 /\ X_2 >= 0 /\ -X_1 + X_2 >= 0 /\ -X_1 >= 0
  For symbol f25: -X_5 >= 0 /\ X_2 - X_5 >= 0 /\ -X_2 - X_5 >= 0 /\ X_1 - X_5 - 1 >= 0 /\ X_5 >= 0 /\ X_2 + X_5 >= 0 /\ -X_2 + X_5 >= 0 /\ X_1 + X_5 - 1 >= 0 /\ -X_2 >= 0 /\ X_1 - X_2 - 1 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 1 >= 0 /\ X_1 - 1 >= 0


This yielded the following problem:
4:	T:
		(1, 1)    f0(a, b, c, d, e) -> f10(f, 0, f, d, 0)
		(1, 1)    f10(a, b, c, d, e) -> f25(a, b, c, d, e) [ -e >= 0 /\ b - e >= 0 /\ -b - e >= 0 /\ e >= 0 /\ b + e >= 0 /\ -b + e >= 0 /\ -b >= 0 /\ b >= 0 /\ a >= 1 ]
		(?, 1)    f16(a, b, c, d, e) -> f10(f, b, f, d, 0) [ -e >= 0 /\ b - e >= 0 /\ -b - e >= 0 /\ -a - e >= 0 /\ e >= 0 /\ b + e >= 0 /\ -b + e >= 0 /\ -a + e >= 0 /\ -b >= 0 /\ -a - b >= 0 /\ b >= 0 /\ -a + b >= 0 /\ -a >= 0 /\ 0 >= d ]
		(?, 1)    f25(a, b, c, d, e) -> f25(a, b, c, d, e) [ -e >= 0 /\ b - e >= 0 /\ -b - e >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ b + e >= 0 /\ -b + e >= 0 /\ a + e - 1 >= 0 /\ -b >= 0 /\ a - b - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 ]
		(?, 1)    f16(a, b, c, d, e) -> f16(a, b, c, d, e) [ -e >= 0 /\ b - e >= 0 /\ -b - e >= 0 /\ -a - e >= 0 /\ e >= 0 /\ b + e >= 0 /\ -b + e >= 0 /\ -a + e >= 0 /\ -b >= 0 /\ -a - b >= 0 /\ b >= 0 /\ -a + b >= 0 /\ -a >= 0 /\ d >= 1 ]
		(?, 1)    f10(a, b, c, d, e) -> f16(a, 0, f, f, e) [ -e >= 0 /\ b - e >= 0 /\ -b - e >= 0 /\ e >= 0 /\ b + e >= 0 /\ -b + e >= 0 /\ -b >= 0 /\ b >= 0 /\ 0 >= a ]
	start location:	f0
	leaf cost:	1

By chaining the transition f10(a, b, c, d, e) -> f25(a, b, c, d, e) [ -e >= 0 /\ b - e >= 0 /\ -b - e >= 0 /\ e >= 0 /\ b + e >= 0 /\ -b + e >= 0 /\ -b >= 0 /\ b >= 0 /\ a >= 1 ] with all transitions in problem 4, the following new transition is obtained:
	f10(a, b, c, d, e) -> f25(a, b, c, d, e) [ -e >= 0 /\ b - e >= 0 /\ -b - e >= 0 /\ e >= 0 /\ b + e >= 0 /\ -b + e >= 0 /\ -b >= 0 /\ b >= 0 /\ a >= 1 /\ a - e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 ]
We thus obtain the following problem:
5:	T:
		(1, 2)    f10(a, b, c, d, e) -> f25(a, b, c, d, e) [ -e >= 0 /\ b - e >= 0 /\ -b - e >= 0 /\ e >= 0 /\ b + e >= 0 /\ -b + e >= 0 /\ -b >= 0 /\ b >= 0 /\ a >= 1 /\ a - e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 ]
		(1, 1)    f0(a, b, c, d, e) -> f10(f, 0, f, d, 0)
		(?, 1)    f16(a, b, c, d, e) -> f10(f, b, f, d, 0) [ -e >= 0 /\ b - e >= 0 /\ -b - e >= 0 /\ -a - e >= 0 /\ e >= 0 /\ b + e >= 0 /\ -b + e >= 0 /\ -a + e >= 0 /\ -b >= 0 /\ -a - b >= 0 /\ b >= 0 /\ -a + b >= 0 /\ -a >= 0 /\ 0 >= d ]
		(?, 1)    f25(a, b, c, d, e) -> f25(a, b, c, d, e) [ -e >= 0 /\ b - e >= 0 /\ -b - e >= 0 /\ a - e - 1 >= 0 /\ e >= 0 /\ b + e >= 0 /\ -b + e >= 0 /\ a + e - 1 >= 0 /\ -b >= 0 /\ a - b - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 ]
		(?, 1)    f16(a, b, c, d, e) -> f16(a, b, c, d, e) [ -e >= 0 /\ b - e >= 0 /\ -b - e >= 0 /\ -a - e >= 0 /\ e >= 0 /\ b + e >= 0 /\ -b + e >= 0 /\ -a + e >= 0 /\ -b >= 0 /\ -a - b >= 0 /\ b >= 0 /\ -a + b >= 0 /\ -a >= 0 /\ d >= 1 ]
		(?, 1)    f10(a, b, c, d, e) -> f16(a, 0, f, f, e) [ -e >= 0 /\ b - e >= 0 /\ -b - e >= 0 /\ e >= 0 /\ b + e >= 0 /\ -b + e >= 0 /\ -b >= 0 /\ b >= 0 /\ 0 >= a ]
	start location:	f0
	leaf cost:	1

Complexity upper bound ?

Time: 0.788 sec (SMT: 0.736 sec)