MAYBE

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Complexity upper bound ?

Time: 1.126 sec (SMT: 1.031 sec)