MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f0(a, b, c, d, e) -> f2(a, f, c, d, e) [ 0 >= a ]
		(?, 1)    f0(a, b, c, d, e) -> f0(3*a + 1, b, f, h, g) [ a >= 1 /\ a >= 2*g + 1 /\ 3*a >= 3*f /\ 3*f >= 3*a /\ f >= 2*g + 1 /\ f >= 1 ]
		(?, 1)    f0(a, b, c, d, e) -> f0(3*a + 1, b, f, h, g) [ a >= 1 /\ a >= 2*g + 1 /\ 3*a >= 3*f /\ 3*f >= 3*a /\ 2*g >= f + 1 /\ f >= 1 ]
		(?, 1)    f0(a, b, c, d, e) -> f0(3*a + 1, b, f, h, g) [ a >= 1 /\ 2*g >= a + 1 /\ 3*a >= 3*f /\ 3*f >= 3*a /\ f >= 2*g + 1 /\ f >= 1 ]
		(?, 1)    f0(a, b, c, d, e) -> f0(3*a + 1, b, f, h, g) [ a >= 1 /\ 2*g >= a + 1 /\ 3*a >= 3*f /\ 3*f >= 3*a /\ 2*g >= f + 1 /\ f >= 1 ]
		(?, 1)    f0(a, b, c, d, e) -> f0(f, b, c, h, f) [ 2*f >= 1 /\ g >= 1 /\ a = 2*f ]
		(1, 1)    f1(a, b, c, d, e) -> f0(a, b, c, d, e)
	start location:	f1
	leaf cost:	0

Testing for unsatisfiable constraints removes the following transitions from problem 1:
	f0(a, b, c, d, e) -> f0(3*a + 1, b, f, h, g) [ a >= 1 /\ a >= 2*g + 1 /\ 3*a >= 3*f /\ 3*f >= 3*a /\ 2*g >= f + 1 /\ f >= 1 ]
	f0(a, b, c, d, e) -> f0(3*a + 1, b, f, h, g) [ a >= 1 /\ 2*g >= a + 1 /\ 3*a >= 3*f /\ 3*f >= 3*a /\ f >= 2*g + 1 /\ f >= 1 ]
We thus obtain the following problem:
2:	T:
		(?, 1)    f0(a, b, c, d, e) -> f2(a, f, c, d, e) [ 0 >= a ]
		(?, 1)    f0(a, b, c, d, e) -> f0(3*a + 1, b, f, h, g) [ a >= 1 /\ a >= 2*g + 1 /\ 3*a >= 3*f /\ 3*f >= 3*a /\ f >= 2*g + 1 /\ f >= 1 ]
		(?, 1)    f0(a, b, c, d, e) -> f0(3*a + 1, b, f, h, g) [ a >= 1 /\ 2*g >= a + 1 /\ 3*a >= 3*f /\ 3*f >= 3*a /\ 2*g >= f + 1 /\ f >= 1 ]
		(?, 1)    f0(a, b, c, d, e) -> f0(f, b, c, h, f) [ 2*f >= 1 /\ g >= 1 /\ a = 2*f ]
		(1, 1)    f1(a, b, c, d, e) -> f0(a, b, c, d, e)
	start location:	f1
	leaf cost:	0

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

Complexity upper bound ?

Time: 0.437 sec (SMT: 0.412 sec)