MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f11(a, b, c, d, e) -> f11(a - 1, b - 1, c + 1, f, e) [ a >= 1 /\ f >= 1 ]
		(?, 1)    f11(a, b, c, d, e) -> f11(a - 1, b, c, f, e) [ 0 >= f /\ a >= 1 /\ a >= b + 1 ]
		(?, 1)    f21(a, b, c, d, e) -> f21(a, b, c, d, e)
		(?, 1)    f23(a, b, c, d, e) -> f26(a, b, c, d, e)
		(?, 1)    f11(a, b, c, d, e) -> f21(a, b, c, d, e) [ 0 >= a ]
		(1, 1)    f0(a, b, c, d, e) -> f11(8, f, 0, d, 8) [ f >= 1 ]
	start location:	f0
	leaf cost:	0

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

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

A polynomial rank function with
	Pol(f11) = V_1
	Pol(f21) = V_1
	Pol(f0) = 8
orients all transitions weakly and the transitions
	f11(a, b, c, d, e) -> f11(a - 1, b, c, f, e) [ 0 >= f /\ a >= 1 /\ a >= b + 1 ]
	f11(a, b, c, d, e) -> f11(a - 1, b - 1, c + 1, f, e) [ a >= 1 /\ f >= 1 ]
strictly and produces the following problem:
4:	T:
		(8, 1)    f11(a, b, c, d, e) -> f11(a - 1, b - 1, c + 1, f, e) [ a >= 1 /\ f >= 1 ]
		(8, 1)    f11(a, b, c, d, e) -> f11(a - 1, b, c, f, e) [ 0 >= f /\ a >= 1 /\ a >= b + 1 ]
		(?, 1)    f21(a, b, c, d, e) -> f21(a, b, c, d, e)
		(1, 1)    f11(a, b, c, d, e) -> f21(a, b, c, d, e) [ 0 >= a ]
		(1, 1)    f0(a, b, c, d, e) -> f11(8, f, 0, d, 8) [ f >= 1 ]
	start location:	f0
	leaf cost:	1

Applied AI with 'oct' on problem 4 to obtain the following invariants:
  For symbol f11: -X_5 + 8 >= 0 /\ X_3 - X_5 + 8 >= 0 /\ -X_1 - X_5 + 16 >= 0 /\ X_5 - 8 >= 0 /\ X_3 + X_5 - 8 >= 0 /\ -X_1 + X_5 >= 0 /\ -X_1 - X_3 + 8 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ -X_1 + X_3 + 8 >= 0 /\ -X_1 + X_2 + 7 >= 0 /\ -X_1 + 8 >= 0
  For symbol f21: -X_5 + 8 >= 0 /\ X_3 - X_5 + 8 >= 0 /\ -X_1 - X_5 + 8 >= 0 /\ X_5 - 8 >= 0 /\ X_3 + X_5 - 8 >= 0 /\ -X_1 + X_5 - 8 >= 0 /\ -X_1 - X_3 + 8 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ -X_1 + X_3 >= 0 /\ -X_1 + X_2 + 7 >= 0 /\ -X_1 >= 0


This yielded the following problem:
5:	T:
		(1, 1)    f0(a, b, c, d, e) -> f11(8, f, 0, d, 8) [ f >= 1 ]
		(1, 1)    f11(a, b, c, d, e) -> f21(a, b, c, d, e) [ -e + 8 >= 0 /\ c - e + 8 >= 0 /\ -a - e + 16 >= 0 /\ e - 8 >= 0 /\ c + e - 8 >= 0 /\ -a + e >= 0 /\ -a - c + 8 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -a + c + 8 >= 0 /\ -a + b + 7 >= 0 /\ -a + 8 >= 0 /\ 0 >= a ]
		(?, 1)    f21(a, b, c, d, e) -> f21(a, b, c, d, e) [ -e + 8 >= 0 /\ c - e + 8 >= 0 /\ -a - e + 8 >= 0 /\ e - 8 >= 0 /\ c + e - 8 >= 0 /\ -a + e - 8 >= 0 /\ -a - c + 8 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -a + c >= 0 /\ -a + b + 7 >= 0 /\ -a >= 0 ]
		(8, 1)    f11(a, b, c, d, e) -> f11(a - 1, b, c, f, e) [ -e + 8 >= 0 /\ c - e + 8 >= 0 /\ -a - e + 16 >= 0 /\ e - 8 >= 0 /\ c + e - 8 >= 0 /\ -a + e >= 0 /\ -a - c + 8 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -a + c + 8 >= 0 /\ -a + b + 7 >= 0 /\ -a + 8 >= 0 /\ 0 >= f /\ a >= 1 /\ a >= b + 1 ]
		(8, 1)    f11(a, b, c, d, e) -> f11(a - 1, b - 1, c + 1, f, e) [ -e + 8 >= 0 /\ c - e + 8 >= 0 /\ -a - e + 16 >= 0 /\ e - 8 >= 0 /\ c + e - 8 >= 0 /\ -a + e >= 0 /\ -a - c + 8 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -a + c + 8 >= 0 /\ -a + b + 7 >= 0 /\ -a + 8 >= 0 /\ a >= 1 /\ f >= 1 ]
	start location:	f0
	leaf cost:	1

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

Complexity upper bound ?

Time: 0.955 sec (SMT: 0.897 sec)