MAYBE

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

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


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

By chaining the transition f1(a) -> f4(3) with all transitions in problem 2, the following new transition is obtained:
	f1(a) -> f4(3) [ 0 >= 0 ]
We thus obtain the following problem:
3:	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.107 sec (SMT: 0.100 sec)