MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f10(a, b, c, d, e) -> f16(a, 0, f, d, e) [ 0 >= a /\ f >= 1 ]
		(?, 1)    f16(a, b, c, d, e) -> f16(a, b, c, d, e) [ c >= 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, c, 0, f) [ 0 >= c ]
		(?, 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, c, 0, f)
	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, d, e) [ 0 >= a /\ f >= 1 ]
		(?, 1)    f16(a, b, c, d, e) -> f16(a, b, c, d, e) [ c >= 1 ]
		(?, 1)    f25(a, b, c, d, e) -> f25(a, b, c, d, e)
		(?, 1)    f16(a, b, c, d, e) -> f10(f, b, c, 0, f) [ 0 >= c ]
		(?, 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, c, 0, f)
	start location:	f0
	leaf cost:	1

Testing for reachability in the complexity graph removes the following transition from problem 2:
	f16(a, b, c, d, e) -> f10(f, b, c, 0, f) [ 0 >= c ]
We thus obtain the following problem:
3:	T:
		(?, 1)    f25(a, b, c, d, e) -> f25(a, b, c, d, e)
		(?, 1)    f16(a, b, c, d, e) -> f16(a, b, c, d, e) [ c >= 1 ]
		(?, 1)    f10(a, b, c, d, e) -> f25(a, b, c, d, e) [ a >= 1 ]
		(?, 1)    f10(a, b, c, d, e) -> f16(a, 0, f, d, e) [ 0 >= a /\ f >= 1 ]
		(1, 1)    f0(a, b, c, d, e) -> f10(f, 0, c, 0, f)
	start location:	f0
	leaf cost:	1

Repeatedly propagating knowledge in problem 3 produces the following problem:
4:	T:
		(?, 1)    f25(a, b, c, d, e) -> f25(a, b, c, d, e)
		(?, 1)    f16(a, b, c, d, e) -> f16(a, b, c, d, e) [ c >= 1 ]
		(1, 1)    f10(a, b, c, d, e) -> f25(a, b, c, d, e) [ a >= 1 ]
		(1, 1)    f10(a, b, c, d, e) -> f16(a, 0, f, d, e) [ 0 >= a /\ f >= 1 ]
		(1, 1)    f0(a, b, c, d, e) -> f10(f, 0, c, 0, f)
	start location:	f0
	leaf cost:	1

Applied AI with 'oct' on problem 4 to obtain the following invariants:
  For symbol f10: -X_4 >= 0 /\ X_2 - X_4 >= 0 /\ -X_2 - X_4 >= 0 /\ X_4 >= 0 /\ X_2 + X_4 >= 0 /\ -X_2 + X_4 >= 0 /\ -X_2 >= 0 /\ X_2 >= 0
  For symbol f16: -X_4 >= 0 /\ X_3 - X_4 - 1 >= 0 /\ X_2 - X_4 >= 0 /\ -X_2 - X_4 >= 0 /\ -X_1 - X_4 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 - 1 >= 0 /\ X_2 + X_4 >= 0 /\ -X_2 + X_4 >= 0 /\ -X_1 + X_4 >= 0 /\ X_3 - 1 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ -X_2 + X_3 - 1 >= 0 /\ -X_1 + X_3 - 1 >= 0 /\ -X_2 >= 0 /\ -X_1 - X_2 >= 0 /\ X_2 >= 0 /\ -X_1 + X_2 >= 0 /\ -X_1 >= 0
  For symbol f25: -X_4 >= 0 /\ X_2 - X_4 >= 0 /\ -X_2 - X_4 >= 0 /\ X_1 - X_4 - 1 >= 0 /\ X_4 >= 0 /\ X_2 + X_4 >= 0 /\ -X_2 + X_4 >= 0 /\ X_1 + X_4 - 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:
5:	T:
		(1, 1)    f0(a, b, c, d, e) -> f10(f, 0, c, 0, f)
		(1, 1)    f10(a, b, c, d, e) -> f16(a, 0, f, d, e) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -b >= 0 /\ b >= 0 /\ 0 >= a /\ f >= 1 ]
		(1, 1)    f10(a, b, c, d, e) -> f25(a, b, c, d, e) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -b >= 0 /\ b >= 0 /\ a >= 1 ]
		(?, 1)    f16(a, b, c, d, e) -> f16(a, b, c, d, e) [ -d >= 0 /\ c - d - 1 >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ -a - d >= 0 /\ d >= 0 /\ c + d - 1 >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -a + d >= 0 /\ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ -a + c - 1 >= 0 /\ -b >= 0 /\ -a - b >= 0 /\ b >= 0 /\ -a + b >= 0 /\ -a >= 0 /\ c >= 1 ]
		(?, 1)    f25(a, b, c, d, e) -> f25(a, b, c, d, e) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ a - d - 1 >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ a + d - 1 >= 0 /\ -b >= 0 /\ a - b - 1 >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 ]
	start location:	f0
	leaf cost:	1

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

Complexity upper bound ?

Time: 0.666 sec (SMT: 0.620 sec)