MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f2(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(?, 1)    f2(a, b, c) -> f2(a + 1, b, c) [ a >= b + 1 /\ a >= b ]
		(?, 1)    f2(a, b, c) -> f300(a, b, d) [ a = b ]
		(1, 1)    f1(a, b, c) -> f2(a, b, c)
	start location:	f1
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(?, 1)    f2(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(?, 1)    f2(a, b, c) -> f2(a + 1, b, c) [ a >= b + 1 /\ a >= b ]
		(1, 1)    f1(a, b, c) -> f2(a, b, c)
	start location:	f1
	leaf cost:	1

A polynomial rank function with
	Pol(f2) = -3*V_1 + 3*V_2 - 2
	Pol(f1) = -3*V_1 + 3*V_2 - 2
orients all transitions weakly and the transition
	f2(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
strictly and produces the following problem:
3:	T:
		(3*a + 3*b + 2, 1)    f2(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(?, 1)                f2(a, b, c) -> f2(a + 1, b, c) [ a >= b + 1 /\ a >= b ]
		(1, 1)                f1(a, b, c) -> f2(a, b, c)
	start location:	f1
	leaf cost:	1

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

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

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

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

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

By chaining the transition f1(a, b, c) -> f2(a + 5, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b ] with all transitions in problem 8, the following new transition is obtained:
	f1(a, b, c) -> f2(a + 6, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b ]
We thus obtain the following problem:
9:	T:
		(1, 7)                f1(a, b, c) -> f2(a + 6, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b ]
		(1, 2)                f1(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(3*a + 3*b + 2, 1)    f2(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(?, 1)                f2(a, b, c) -> f2(a + 1, b, c) [ a >= b + 1 /\ a >= b ]
	start location:	f1
	leaf cost:	1

By chaining the transition f1(a, b, c) -> f2(a + 6, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b ] with all transitions in problem 9, the following new transition is obtained:
	f1(a, b, c) -> f2(a + 7, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b ]
We thus obtain the following problem:
10:	T:
		(1, 8)                f1(a, b, c) -> f2(a + 7, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b ]
		(1, 2)                f1(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(3*a + 3*b + 2, 1)    f2(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(?, 1)                f2(a, b, c) -> f2(a + 1, b, c) [ a >= b + 1 /\ a >= b ]
	start location:	f1
	leaf cost:	1

By chaining the transition f1(a, b, c) -> f2(a + 7, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b ] with all transitions in problem 10, the following new transition is obtained:
	f1(a, b, c) -> f2(a + 8, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b ]
We thus obtain the following problem:
11:	T:
		(1, 9)                f1(a, b, c) -> f2(a + 8, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b ]
		(1, 2)                f1(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(3*a + 3*b + 2, 1)    f2(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(?, 1)                f2(a, b, c) -> f2(a + 1, b, c) [ a >= b + 1 /\ a >= b ]
	start location:	f1
	leaf cost:	1

By chaining the transition f1(a, b, c) -> f2(a + 8, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b ] with all transitions in problem 11, the following new transition is obtained:
	f1(a, b, c) -> f2(a + 9, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b ]
We thus obtain the following problem:
12:	T:
		(1, 10)               f1(a, b, c) -> f2(a + 9, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b ]
		(1, 2)                f1(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(3*a + 3*b + 2, 1)    f2(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(?, 1)                f2(a, b, c) -> f2(a + 1, b, c) [ a >= b + 1 /\ a >= b ]
	start location:	f1
	leaf cost:	1

By chaining the transition f1(a, b, c) -> f2(a + 9, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b ] with all transitions in problem 12, the following new transition is obtained:
	f1(a, b, c) -> f2(a + 10, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b ]
We thus obtain the following problem:
13:	T:
		(1, 11)               f1(a, b, c) -> f2(a + 10, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b ]
		(1, 2)                f1(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(3*a + 3*b + 2, 1)    f2(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(?, 1)                f2(a, b, c) -> f2(a + 1, b, c) [ a >= b + 1 /\ a >= b ]
	start location:	f1
	leaf cost:	1

By chaining the transition f1(a, b, c) -> f2(a + 10, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b ] with all transitions in problem 13, the following new transition is obtained:
	f1(a, b, c) -> f2(a + 11, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b /\ a + 10 >= b + 1 /\ a + 10 >= b ]
We thus obtain the following problem:
14:	T:
		(1, 12)               f1(a, b, c) -> f2(a + 11, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b /\ a + 10 >= b + 1 /\ a + 10 >= b ]
		(1, 2)                f1(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(3*a + 3*b + 2, 1)    f2(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(?, 1)                f2(a, b, c) -> f2(a + 1, b, c) [ a >= b + 1 /\ a >= b ]
	start location:	f1
	leaf cost:	1

By chaining the transition f1(a, b, c) -> f2(a + 11, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b /\ a + 10 >= b + 1 /\ a + 10 >= b ] with all transitions in problem 14, the following new transition is obtained:
	f1(a, b, c) -> f2(a + 12, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b /\ a + 10 >= b + 1 /\ a + 10 >= b /\ a + 11 >= b + 1 /\ a + 11 >= b ]
We thus obtain the following problem:
15:	T:
		(1, 13)               f1(a, b, c) -> f2(a + 12, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b /\ a + 10 >= b + 1 /\ a + 10 >= b /\ a + 11 >= b + 1 /\ a + 11 >= b ]
		(1, 2)                f1(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(3*a + 3*b + 2, 1)    f2(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(?, 1)                f2(a, b, c) -> f2(a + 1, b, c) [ a >= b + 1 /\ a >= b ]
	start location:	f1
	leaf cost:	1

By chaining the transition f1(a, b, c) -> f2(a + 12, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b /\ a + 10 >= b + 1 /\ a + 10 >= b /\ a + 11 >= b + 1 /\ a + 11 >= b ] with all transitions in problem 15, the following new transition is obtained:
	f1(a, b, c) -> f2(a + 13, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b /\ a + 10 >= b + 1 /\ a + 10 >= b /\ a + 11 >= b + 1 /\ a + 11 >= b /\ a + 12 >= b + 1 /\ a + 12 >= b ]
We thus obtain the following problem:
16:	T:
		(1, 14)               f1(a, b, c) -> f2(a + 13, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b /\ a + 10 >= b + 1 /\ a + 10 >= b /\ a + 11 >= b + 1 /\ a + 11 >= b /\ a + 12 >= b + 1 /\ a + 12 >= b ]
		(1, 2)                f1(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(3*a + 3*b + 2, 1)    f2(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(?, 1)                f2(a, b, c) -> f2(a + 1, b, c) [ a >= b + 1 /\ a >= b ]
	start location:	f1
	leaf cost:	1

By chaining the transition f1(a, b, c) -> f2(a + 13, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b /\ a + 10 >= b + 1 /\ a + 10 >= b /\ a + 11 >= b + 1 /\ a + 11 >= b /\ a + 12 >= b + 1 /\ a + 12 >= b ] with all transitions in problem 16, the following new transition is obtained:
	f1(a, b, c) -> f2(a + 14, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b /\ a + 10 >= b + 1 /\ a + 10 >= b /\ a + 11 >= b + 1 /\ a + 11 >= b /\ a + 12 >= b + 1 /\ a + 12 >= b /\ a + 13 >= b + 1 /\ a + 13 >= b ]
We thus obtain the following problem:
17:	T:
		(1, 15)               f1(a, b, c) -> f2(a + 14, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b /\ a + 10 >= b + 1 /\ a + 10 >= b /\ a + 11 >= b + 1 /\ a + 11 >= b /\ a + 12 >= b + 1 /\ a + 12 >= b /\ a + 13 >= b + 1 /\ a + 13 >= b ]
		(1, 2)                f1(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(3*a + 3*b + 2, 1)    f2(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(?, 1)                f2(a, b, c) -> f2(a + 1, b, c) [ a >= b + 1 /\ a >= b ]
	start location:	f1
	leaf cost:	1

By chaining the transition f1(a, b, c) -> f2(a + 14, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b /\ a + 10 >= b + 1 /\ a + 10 >= b /\ a + 11 >= b + 1 /\ a + 11 >= b /\ a + 12 >= b + 1 /\ a + 12 >= b /\ a + 13 >= b + 1 /\ a + 13 >= b ] with all transitions in problem 17, the following new transition is obtained:
	f1(a, b, c) -> f2(a + 15, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b /\ a + 10 >= b + 1 /\ a + 10 >= b /\ a + 11 >= b + 1 /\ a + 11 >= b /\ a + 12 >= b + 1 /\ a + 12 >= b /\ a + 13 >= b + 1 /\ a + 13 >= b /\ a + 14 >= b + 1 /\ a + 14 >= b ]
We thus obtain the following problem:
18:	T:
		(1, 16)               f1(a, b, c) -> f2(a + 15, b, c) [ a >= b + 1 /\ a >= b /\ a + 1 >= b + 1 /\ a + 1 >= b /\ a + 2 >= b + 1 /\ a + 2 >= b /\ a + 3 >= b + 1 /\ a + 3 >= b /\ a + 4 >= b + 1 /\ a + 4 >= b /\ a + 5 >= b + 1 /\ a + 5 >= b /\ a + 6 >= b + 1 /\ a + 6 >= b /\ a + 7 >= b + 1 /\ a + 7 >= b /\ a + 8 >= b + 1 /\ a + 8 >= b /\ a + 9 >= b + 1 /\ a + 9 >= b /\ a + 10 >= b + 1 /\ a + 10 >= b /\ a + 11 >= b + 1 /\ a + 11 >= b /\ a + 12 >= b + 1 /\ a + 12 >= b /\ a + 13 >= b + 1 /\ a + 13 >= b /\ a + 14 >= b + 1 /\ a + 14 >= b ]
		(1, 2)                f1(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(3*a + 3*b + 2, 1)    f2(a, b, c) -> f2(a + 1, b, c) [ b >= a + 1 ]
		(?, 1)                f2(a, b, c) -> f2(a + 1, b, c) [ a >= b + 1 /\ a >= b ]
	start location:	f1
	leaf cost:	1

Complexity upper bound ?

Time: 1.262 sec (SMT: 1.163 sec)