MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f11(a, b, c, d, e, f) -> f11(a - 1, b - 1, c + 1, g, e, f) [ a >= 1 /\ g >= 1 ]
		(?, 1)    f11(a, b, c, d, e, f) -> f11(a - 1, b, c, g, e, f) [ 0 >= g /\ a >= 1 /\ a >= b + 1 ]
		(?, 1)    f21(a, b, c, d, e, f) -> f21(a, b, c, d, e, f)
		(?, 1)    f23(a, b, c, d, e, f) -> f26(a, b, c, d, e, f)
		(?, 1)    f11(a, b, c, d, e, f) -> f21(a, b, c, d, e, f) [ 0 >= a ]
		(1, 1)    f0(a, b, c, d, e, f) -> f11(4, g, 0, d, g, 4) [ g >= 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, f) -> f11(a - 1, b - 1, c + 1, g, e, f) [ a >= 1 /\ g >= 1 ]
		(?, 1)    f11(a, b, c, d, e, f) -> f11(a - 1, b, c, g, e, f) [ 0 >= g /\ a >= 1 /\ a >= b + 1 ]
		(?, 1)    f21(a, b, c, d, e, f) -> f21(a, b, c, d, e, f)
		(?, 1)    f11(a, b, c, d, e, f) -> f21(a, b, c, d, e, f) [ 0 >= a ]
		(1, 1)    f0(a, b, c, d, e, f) -> f11(4, g, 0, d, g, 4) [ g >= 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, f) -> f21(a, b, c, d, e, f) [ 0 >= a ]
strictly and produces the following problem:
3:	T:
		(?, 1)    f11(a, b, c, d, e, f) -> f11(a - 1, b - 1, c + 1, g, e, f) [ a >= 1 /\ g >= 1 ]
		(?, 1)    f11(a, b, c, d, e, f) -> f11(a - 1, b, c, g, e, f) [ 0 >= g /\ a >= 1 /\ a >= b + 1 ]
		(?, 1)    f21(a, b, c, d, e, f) -> f21(a, b, c, d, e, f)
		(1, 1)    f11(a, b, c, d, e, f) -> f21(a, b, c, d, e, f) [ 0 >= a ]
		(1, 1)    f0(a, b, c, d, e, f) -> f11(4, g, 0, d, g, 4) [ g >= 1 ]
	start location:	f0
	leaf cost:	1

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

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


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

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

Complexity upper bound ?

Time: 1.008 sec (SMT: 0.946 sec)