MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f2(a, b, c) -> f2(a, b - 1, c) [ 29 >= a ]
		(?, 1)    f2(a, b, c) -> f300(a, b - 1, c) [ a >= 30 ]
		(?, 1)    f300(a, b, c) -> f2(a, b, c) [ 19 >= b ]
		(?, 1)    f300(a, b, c) -> f1(a, b, d) [ b >= 20 ]
		(1, 1)    f3(a, b, c) -> f300(a, b, c)
	start location:	f3
	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, b - 1, c) [ 29 >= a ]
		(?, 1)    f2(a, b, c) -> f300(a, b - 1, c) [ a >= 30 ]
		(?, 1)    f300(a, b, c) -> f2(a, b, c) [ 19 >= b ]
		(1, 1)    f3(a, b, c) -> f300(a, b, c)
	start location:	f3
	leaf cost:	1

Applied AI with 'oct' on problem 2 to obtain the following invariants:
  For symbol f2: -X_2 + 19 >= 0


This yielded the following problem:
3:	T:
		(1, 1)    f3(a, b, c) -> f300(a, b, c)
		(?, 1)    f300(a, b, c) -> f2(a, b, c) [ 19 >= b ]
		(?, 1)    f2(a, b, c) -> f300(a, b - 1, c) [ -b + 19 >= 0 /\ a >= 30 ]
		(?, 1)    f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ 29 >= a ]
	start location:	f3
	leaf cost:	1

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

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

Testing for reachability in the complexity graph removes the following transition from problem 5:
	f300(a, b, c) -> f2(a, b, c) [ 19 >= b ]
We thus obtain the following problem:
6:	T:
		(?, 2)    f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 ]
		(?, 1)    f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ 29 >= a ]
		(1, 2)    f3(a, b, c) -> f2(a, b, c) [ 19 >= b ]
	start location:	f3
	leaf cost:	1

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

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

By chaining the transition f3(a, b, c) -> f2(a, b - 2, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 ] with all transitions in problem 8, the following new transition is obtained:
	f3(a, b, c) -> f2(a, b - 3, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 ]
We thus obtain the following problem:
9:	T:
		(1, 8)    f3(a, b, c) -> f2(a, b - 3, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 ]
		(1, 3)    f3(a, b, c) -> f2(a, b - 1, c) [ 19 >= b /\ -b + 19 >= 0 /\ 29 >= a ]
		(?, 2)    f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 ]
		(?, 1)    f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ 29 >= a ]
	start location:	f3
	leaf cost:	1

By chaining the transition f3(a, b, c) -> f2(a, b - 3, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 ] with all transitions in problem 9, the following new transition is obtained:
	f3(a, b, c) -> f2(a, b - 4, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 ]
We thus obtain the following problem:
10:	T:
		(1, 10)    f3(a, b, c) -> f2(a, b - 4, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 ]
		(1, 3)     f3(a, b, c) -> f2(a, b - 1, c) [ 19 >= b /\ -b + 19 >= 0 /\ 29 >= a ]
		(?, 2)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 ]
		(?, 1)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ 29 >= a ]
	start location:	f3
	leaf cost:	1

By chaining the transition f3(a, b, c) -> f2(a, b - 4, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 ] with all transitions in problem 10, the following new transition is obtained:
	f3(a, b, c) -> f2(a, b - 5, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 ]
We thus obtain the following problem:
11:	T:
		(1, 12)    f3(a, b, c) -> f2(a, b - 5, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 ]
		(1, 3)     f3(a, b, c) -> f2(a, b - 1, c) [ 19 >= b /\ -b + 19 >= 0 /\ 29 >= a ]
		(?, 2)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 ]
		(?, 1)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ 29 >= a ]
	start location:	f3
	leaf cost:	1

By chaining the transition f3(a, b, c) -> f2(a, b - 5, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 ] with all transitions in problem 11, the following new transition is obtained:
	f3(a, b, c) -> f2(a, b - 6, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 ]
We thus obtain the following problem:
12:	T:
		(1, 14)    f3(a, b, c) -> f2(a, b - 6, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 ]
		(1, 3)     f3(a, b, c) -> f2(a, b - 1, c) [ 19 >= b /\ -b + 19 >= 0 /\ 29 >= a ]
		(?, 2)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 ]
		(?, 1)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ 29 >= a ]
	start location:	f3
	leaf cost:	1

By chaining the transition f3(a, b, c) -> f2(a, b - 6, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 ] with all transitions in problem 12, the following new transition is obtained:
	f3(a, b, c) -> f2(a, b - 7, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 ]
We thus obtain the following problem:
13:	T:
		(1, 16)    f3(a, b, c) -> f2(a, b - 7, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 ]
		(1, 3)     f3(a, b, c) -> f2(a, b - 1, c) [ 19 >= b /\ -b + 19 >= 0 /\ 29 >= a ]
		(?, 2)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 ]
		(?, 1)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ 29 >= a ]
	start location:	f3
	leaf cost:	1

By chaining the transition f3(a, b, c) -> f2(a, b - 7, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 ] with all transitions in problem 13, the following new transition is obtained:
	f3(a, b, c) -> f2(a, b - 8, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 ]
We thus obtain the following problem:
14:	T:
		(1, 18)    f3(a, b, c) -> f2(a, b - 8, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 ]
		(1, 3)     f3(a, b, c) -> f2(a, b - 1, c) [ 19 >= b /\ -b + 19 >= 0 /\ 29 >= a ]
		(?, 2)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 ]
		(?, 1)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ 29 >= a ]
	start location:	f3
	leaf cost:	1

By chaining the transition f3(a, b, c) -> f2(a, b - 8, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 ] with all transitions in problem 14, the following new transition is obtained:
	f3(a, b, c) -> f2(a, b - 9, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 /\ -b + 27 >= 0 /\ 19 >= b - 9 ]
We thus obtain the following problem:
15:	T:
		(1, 20)    f3(a, b, c) -> f2(a, b - 9, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 /\ -b + 27 >= 0 /\ 19 >= b - 9 ]
		(1, 3)     f3(a, b, c) -> f2(a, b - 1, c) [ 19 >= b /\ -b + 19 >= 0 /\ 29 >= a ]
		(?, 2)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 ]
		(?, 1)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ 29 >= a ]
	start location:	f3
	leaf cost:	1

By chaining the transition f3(a, b, c) -> f2(a, b - 9, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 /\ -b + 27 >= 0 /\ 19 >= b - 9 ] with all transitions in problem 15, the following new transition is obtained:
	f3(a, b, c) -> f2(a, b - 10, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 /\ -b + 27 >= 0 /\ 19 >= b - 9 /\ -b + 28 >= 0 /\ 19 >= b - 10 ]
We thus obtain the following problem:
16:	T:
		(1, 22)    f3(a, b, c) -> f2(a, b - 10, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 /\ -b + 27 >= 0 /\ 19 >= b - 9 /\ -b + 28 >= 0 /\ 19 >= b - 10 ]
		(1, 3)     f3(a, b, c) -> f2(a, b - 1, c) [ 19 >= b /\ -b + 19 >= 0 /\ 29 >= a ]
		(?, 2)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 ]
		(?, 1)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ 29 >= a ]
	start location:	f3
	leaf cost:	1

By chaining the transition f3(a, b, c) -> f2(a, b - 10, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 /\ -b + 27 >= 0 /\ 19 >= b - 9 /\ -b + 28 >= 0 /\ 19 >= b - 10 ] with all transitions in problem 16, the following new transition is obtained:
	f3(a, b, c) -> f2(a, b - 11, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 /\ -b + 27 >= 0 /\ 19 >= b - 9 /\ -b + 28 >= 0 /\ 19 >= b - 10 /\ -b + 29 >= 0 /\ 19 >= b - 11 ]
We thus obtain the following problem:
17:	T:
		(1, 24)    f3(a, b, c) -> f2(a, b - 11, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 /\ -b + 27 >= 0 /\ 19 >= b - 9 /\ -b + 28 >= 0 /\ 19 >= b - 10 /\ -b + 29 >= 0 /\ 19 >= b - 11 ]
		(1, 3)     f3(a, b, c) -> f2(a, b - 1, c) [ 19 >= b /\ -b + 19 >= 0 /\ 29 >= a ]
		(?, 2)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 ]
		(?, 1)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ 29 >= a ]
	start location:	f3
	leaf cost:	1

By chaining the transition f3(a, b, c) -> f2(a, b - 11, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 /\ -b + 27 >= 0 /\ 19 >= b - 9 /\ -b + 28 >= 0 /\ 19 >= b - 10 /\ -b + 29 >= 0 /\ 19 >= b - 11 ] with all transitions in problem 17, the following new transition is obtained:
	f3(a, b, c) -> f2(a, b - 12, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 /\ -b + 27 >= 0 /\ 19 >= b - 9 /\ -b + 28 >= 0 /\ 19 >= b - 10 /\ -b + 29 >= 0 /\ 19 >= b - 11 /\ -b + 30 >= 0 /\ 19 >= b - 12 ]
We thus obtain the following problem:
18:	T:
		(1, 26)    f3(a, b, c) -> f2(a, b - 12, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 /\ -b + 27 >= 0 /\ 19 >= b - 9 /\ -b + 28 >= 0 /\ 19 >= b - 10 /\ -b + 29 >= 0 /\ 19 >= b - 11 /\ -b + 30 >= 0 /\ 19 >= b - 12 ]
		(1, 3)     f3(a, b, c) -> f2(a, b - 1, c) [ 19 >= b /\ -b + 19 >= 0 /\ 29 >= a ]
		(?, 2)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 ]
		(?, 1)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ 29 >= a ]
	start location:	f3
	leaf cost:	1

By chaining the transition f3(a, b, c) -> f2(a, b - 12, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 /\ -b + 27 >= 0 /\ 19 >= b - 9 /\ -b + 28 >= 0 /\ 19 >= b - 10 /\ -b + 29 >= 0 /\ 19 >= b - 11 /\ -b + 30 >= 0 /\ 19 >= b - 12 ] with all transitions in problem 18, the following new transition is obtained:
	f3(a, b, c) -> f2(a, b - 13, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 /\ -b + 27 >= 0 /\ 19 >= b - 9 /\ -b + 28 >= 0 /\ 19 >= b - 10 /\ -b + 29 >= 0 /\ 19 >= b - 11 /\ -b + 30 >= 0 /\ 19 >= b - 12 /\ -b + 31 >= 0 /\ 19 >= b - 13 ]
We thus obtain the following problem:
19:	T:
		(1, 28)    f3(a, b, c) -> f2(a, b - 13, c) [ 19 >= b /\ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 /\ -b + 20 >= 0 /\ 19 >= b - 2 /\ -b + 21 >= 0 /\ 19 >= b - 3 /\ -b + 22 >= 0 /\ 19 >= b - 4 /\ -b + 23 >= 0 /\ 19 >= b - 5 /\ -b + 24 >= 0 /\ 19 >= b - 6 /\ -b + 25 >= 0 /\ 19 >= b - 7 /\ -b + 26 >= 0 /\ 19 >= b - 8 /\ -b + 27 >= 0 /\ 19 >= b - 9 /\ -b + 28 >= 0 /\ 19 >= b - 10 /\ -b + 29 >= 0 /\ 19 >= b - 11 /\ -b + 30 >= 0 /\ 19 >= b - 12 /\ -b + 31 >= 0 /\ 19 >= b - 13 ]
		(1, 3)     f3(a, b, c) -> f2(a, b - 1, c) [ 19 >= b /\ -b + 19 >= 0 /\ 29 >= a ]
		(?, 2)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ a >= 30 /\ 19 >= b - 1 ]
		(?, 1)     f2(a, b, c) -> f2(a, b - 1, c) [ -b + 19 >= 0 /\ 29 >= a ]
	start location:	f3
	leaf cost:	1

Complexity upper bound ?

Time: 1.426 sec (SMT: 1.323 sec)