MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f9(a, b, c, d) -> f14(a, 0, e, d) [ 0 >= a ]
		(?, 1)    f14(a, b, c, d) -> f14(a, b, c - 1, d) [ c >= 1 ]
		(?, 1)    f22(a, b, c, d) -> f22(a, b, c, d)
		(?, 1)    f24(a, b, c, d) -> f27(a, b, c, d)
		(?, 1)    f14(a, b, c, d) -> f9(e, b, c, 0) [ 0 >= c ]
		(?, 1)    f9(a, b, c, d) -> f22(a, b, c, d) [ a >= 1 ]
		(1, 1)    f0(a, b, c, d) -> f9(e, 0, c, 0)
	start location:	f0
	leaf cost:	0

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

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

Applied AI with 'oct' on problem 3 to obtain the following invariants:
  For symbol f14: -X_4 >= 0 /\ X_2 - X_4 >= 0 /\ -X_2 - X_4 >= 0 /\ -X_1 - X_4 >= 0 /\ X_4 >= 0 /\ X_2 + X_4 >= 0 /\ -X_2 + X_4 >= 0 /\ -X_1 + X_4 >= 0 /\ -X_2 >= 0 /\ -X_1 - X_2 >= 0 /\ X_2 >= 0 /\ -X_1 + X_2 >= 0 /\ -X_1 >= 0
  For symbol f22: -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
  For symbol f9: -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


This yielded the following problem:
4:	T:
		(1, 1)    f0(a, b, c, d) -> f9(e, 0, c, 0)
		(1, 1)    f9(a, b, c, d) -> f22(a, b, c, d) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -b >= 0 /\ b >= 0 /\ a >= 1 ]
		(?, 1)    f14(a, b, c, d) -> f9(e, b, c, 0) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ -a - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -a + d >= 0 /\ -b >= 0 /\ -a - b >= 0 /\ b >= 0 /\ -a + b >= 0 /\ -a >= 0 /\ 0 >= c ]
		(?, 1)    f22(a, b, c, d) -> f22(a, b, c, d) [ -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 ]
		(?, 1)    f14(a, b, c, d) -> f14(a, b, c - 1, d) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ -a - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -a + d >= 0 /\ -b >= 0 /\ -a - b >= 0 /\ b >= 0 /\ -a + b >= 0 /\ -a >= 0 /\ c >= 1 ]
		(?, 1)    f9(a, b, c, d) -> f14(a, 0, e, d) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -b >= 0 /\ b >= 0 /\ 0 >= a ]
	start location:	f0
	leaf cost:	1

By chaining the transition f9(a, b, c, d) -> f22(a, b, c, d) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -b >= 0 /\ b >= 0 /\ a >= 1 ] with all transitions in problem 4, the following new transition is obtained:
	f9(a, b, c, d) -> f22(a, b, c, d) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -b >= 0 /\ b >= 0 /\ a >= 1 /\ a - d - 1 >= 0 /\ a + d - 1 >= 0 /\ a - b - 1 >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 ]
We thus obtain the following problem:
5:	T:
		(1, 2)    f9(a, b, c, d) -> f22(a, b, c, d) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -b >= 0 /\ b >= 0 /\ a >= 1 /\ a - d - 1 >= 0 /\ a + d - 1 >= 0 /\ a - b - 1 >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 ]
		(1, 1)    f0(a, b, c, d) -> f9(e, 0, c, 0)
		(?, 1)    f14(a, b, c, d) -> f9(e, b, c, 0) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ -a - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -a + d >= 0 /\ -b >= 0 /\ -a - b >= 0 /\ b >= 0 /\ -a + b >= 0 /\ -a >= 0 /\ 0 >= c ]
		(?, 1)    f22(a, b, c, d) -> f22(a, b, c, d) [ -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 ]
		(?, 1)    f14(a, b, c, d) -> f14(a, b, c - 1, d) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ -a - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -a + d >= 0 /\ -b >= 0 /\ -a - b >= 0 /\ b >= 0 /\ -a + b >= 0 /\ -a >= 0 /\ c >= 1 ]
		(?, 1)    f9(a, b, c, d) -> f14(a, 0, e, d) [ -d >= 0 /\ b - d >= 0 /\ -b - d >= 0 /\ d >= 0 /\ b + d >= 0 /\ -b + d >= 0 /\ -b >= 0 /\ b >= 0 /\ 0 >= a ]
	start location:	f0
	leaf cost:	1

Complexity upper bound ?

Time: 0.809 sec (SMT: 0.759 sec)