MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f2(a, b) -> f2(c - 2, b) [ 0 >= a + 1 ]
		(?, 1)    f2(a, b) -> f2(c + 2, b) [ a >= 1 ]
		(1, 1)    f3(a, b) -> f2(a, b)
		(?, 1)    f2(a, b) -> f300(a, c) [ a = 0 ]
	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) -> f2(c - 2, b) [ 0 >= a + 1 ]
		(?, 1)    f2(a, b) -> f2(c + 2, b) [ a >= 1 ]
		(1, 1)    f3(a, b) -> f2(a, b)
	start location:	f3
	leaf cost:	1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Complexity upper bound ?

Time: 1.124 sec (SMT: 1.002 sec)