MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f8(a) -> f8(2)
		(1, 1)    f1(a) -> f4(3)
		(?, 1)    f4(a) -> f4(3)
	start location:	f1
	leaf cost:	0

Testing for reachability in the complexity graph removes the following transition from problem 1:
	f8(a) -> f8(2)
We thus obtain the following problem:
2:	T:
		(?, 1)    f4(a) -> f4(3)
		(1, 1)    f1(a) -> f4(3)
	start location:	f1
	leaf cost:	0

Applied AI with 'oct' on problem 2 to obtain the following invariants:
  For symbol f4: -X_1 + 3 >= 0 /\ X_1 - 3 >= 0


This yielded the following problem:
3:	T:
		(1, 1)    f1(a) -> f4(3)
		(?, 1)    f4(a) -> f4(3) [ -a + 3 >= 0 /\ a - 3 >= 0 ]
	start location:	f1
	leaf cost:	0

By chaining the transition f1(a) -> f4(3) with all transitions in problem 3, the following new transition is obtained:
	f1(a) -> f4(3) [ 0 >= 0 ]
We thus obtain the following problem:
4:	T:
		(1, 2)    f1(a) -> f4(3) [ 0 >= 0 ]
		(?, 1)    f4(a) -> f4(3) [ -a + 3 >= 0 /\ a - 3 >= 0 ]
	start location:	f1
	leaf cost:	0

Complexity upper bound ?

Time: 0.111 sec (SMT: 0.103 sec)