MAYBE

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

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, e, f, g].
We thus obtain the following problem:
2:	T:
		(?, 1)    f10(a, b, c, e, f, g) -> f32(a, b, c, e, f, g) [ f >= e + 1 ]
		(?, 1)    f10(a, b, c, e, f, g) -> f32(a, b, c, e, f, g) [ 0 >= f /\ e >= f ]
		(?, 1)    f21(a, b, c, e, f, g) -> f10(a, b, c, e, f + 1, g) [ e + 1 >= a /\ g >= 1 ]
		(?, 1)    f21(a, b, c, e, f, g) -> f10(a, b, c, e, f - 1, g) [ e + 1 >= a /\ 0 >= g ]
		(?, 1)    f10(a, b, c, e, f, g) -> f21(a, b, c - 1, e, f, h) [ h >= 0 /\ 1 >= h /\ f >= 1 /\ c >= 1 /\ e >= f ]
		(?, 1)    f10(a, b, c, e, f, g) -> f21(a + 1, a + 1, h, e, f, i) [ i >= 0 /\ 1 >= i /\ h >= 0 /\ f >= 1 /\ e >= f /\ 0 >= b /\ 0 >= c ]
		(?, 1)    f10(a, b, c, e, f, g) -> f21(a, b - 1, c, e, f, 0) [ f >= 1 /\ e >= f /\ b >= 1 /\ 0 >= c ]
		(1, 1)    f0(a, b, c, e, f, g) -> f10(1, 1, h, 2, 1, g) [ h >= 0 ]
	start location:	f0
	leaf cost:	0

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

Applied AI with 'oct' on problem 3 to obtain the following invariants:
  For symbol f10: -X_4 + 2 >= 0 /\ X_3 - X_4 + 2 >= 0 /\ X_1 - X_4 + 1 >= 0 /\ X_4 - 2 >= 0 /\ X_3 + X_4 - 2 >= 0 /\ X_1 + X_4 - 3 >= 0 /\ X_3 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_1 - X_2 >= 0 /\ X_1 - 1 >= 0
  For symbol f21: -X_6 + 1 >= 0 /\ X_5 - X_6 >= 0 /\ -X_5 - X_6 + 3 >= 0 /\ X_4 - X_6 - 1 >= 0 /\ -X_4 - X_6 + 3 >= 0 /\ X_3 - X_6 + 1 >= 0 /\ X_1 - X_6 >= 0 /\ X_6 >= 0 /\ X_5 + X_6 - 1 >= 0 /\ -X_5 + X_6 + 2 >= 0 /\ X_4 + X_6 - 2 >= 0 /\ -X_4 + X_6 + 2 >= 0 /\ X_3 + X_6 >= 0 /\ X_1 + X_6 - 1 >= 0 /\ -X_5 + 2 >= 0 /\ X_4 - X_5 >= 0 /\ -X_4 - X_5 + 4 >= 0 /\ X_3 - X_5 + 2 >= 0 /\ X_1 - X_5 + 1 >= 0 /\ X_5 - 1 >= 0 /\ X_4 + X_5 - 3 >= 0 /\ -X_4 + X_5 + 1 >= 0 /\ X_3 + X_5 - 1 >= 0 /\ X_1 + X_5 - 2 >= 0 /\ -X_4 + 2 >= 0 /\ X_3 - X_4 + 2 >= 0 /\ X_1 - X_4 + 1 >= 0 /\ X_4 - 2 >= 0 /\ X_3 + X_4 - 2 >= 0 /\ X_1 + X_4 - 3 >= 0 /\ X_3 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_1 - X_2 >= 0 /\ X_1 - 1 >= 0


This yielded the following problem:
4:	T:
		(1, 1)    f0(a, b, c, e, f, g) -> f10(1, 1, h, 2, 1, g) [ h >= 0 ]
		(?, 1)    f10(a, b, c, e, f, g) -> f21(a, b - 1, c, e, f, 0) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ f >= 1 /\ e >= f /\ b >= 1 /\ 0 >= c ]
		(?, 1)    f10(a, b, c, e, f, g) -> f21(a + 1, a + 1, h, e, f, i) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ i >= 0 /\ 1 >= i /\ h >= 0 /\ f >= 1 /\ e >= f /\ 0 >= b /\ 0 >= c ]
		(?, 1)    f10(a, b, c, e, f, g) -> f21(a, b, c - 1, e, f, h) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ h >= 0 /\ 1 >= h /\ f >= 1 /\ c >= 1 /\ e >= f ]
		(?, 1)    f21(a, b, c, e, f, g) -> f10(a, b, c, e, f - 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ 0 >= g ]
		(?, 1)    f21(a, b, c, e, f, g) -> f10(a, b, c, e, f + 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ g >= 1 ]
	start location:	f0
	leaf cost:	2

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

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

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

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

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

By chaining the transition f0(a, b, c, e, f, g) -> f21(2, 2, h'', 2, 1, i) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 ] with all transitions in problem 9, the following new transitions are obtained:
	f0(a, b, c, e, f, g) -> f10(2, 2, h'', 2, 2, i) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 ]
	f0(a, b, c, e, f, g) -> f10(2, 2, h'', 2, 0, i) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ 0 >= i ]
We thus obtain the following problem:
10:	T:
		(1, 7)    f0(a, b, c, e, f, g) -> f10(2, 2, h'', 2, 2, i) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 ]
		(1, 7)    f0(a, b, c, e, f, g) -> f10(2, 2, h'', 2, 0, i) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ 0 >= i ]
		(1, 4)    f0(a, b, c, e, f, g) -> f21(1, 1, h - 2, 2, 2, h'') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ h'' >= 0 /\ 1 >= h'' /\ h - 1 >= 1 /\ 2 >= 2 ]
		(1, 3)    f0(a, b, c, e, f, g) -> f10(1, 1, h - 1, 2, 0, h') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ 0 >= h' ]
		(1, 3)    f0(a, b, c, e, f, g) -> f10(1, 0, h, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ 1 >= 1 /\ 2 >= 1 /\ 0 >= h /\ 1 >= 0 /\ 2 >= 0 /\ h + 1 >= 0 /\ 3 >= 1 ]
		(?, 2)    f10(a, b, c, e, f, g) -> f10(a, b - 1, c, e, f - 1, 0) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ f >= 1 /\ e >= f /\ b >= 1 /\ 0 >= c /\ 1 >= 0 /\ f >= 0 /\ -f + 3 >= 0 /\ e - 1 >= 0 /\ -e + 3 >= 0 /\ c + 1 >= 0 /\ a >= 0 /\ 0 >= 0 /\ f - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ a - b + 1 >= 0 /\ e + 1 >= a ]
		(?, 1)    f10(a, b, c, e, f, g) -> f21(a + 1, a + 1, h, e, f, i) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ i >= 0 /\ 1 >= i /\ h >= 0 /\ f >= 1 /\ e >= f /\ 0 >= b /\ 0 >= c ]
		(?, 1)    f10(a, b, c, e, f, g) -> f21(a, b, c - 1, e, f, h) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ h >= 0 /\ 1 >= h /\ f >= 1 /\ c >= 1 /\ e >= f ]
		(?, 1)    f21(a, b, c, e, f, g) -> f10(a, b, c, e, f - 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ 0 >= g ]
		(?, 1)    f21(a, b, c, e, f, g) -> f10(a, b, c, e, f + 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ g >= 1 ]
	start location:	f0
	leaf cost:	2

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

By chaining the transition f0(a, b, c, e, f, g) -> f10(2, 1, h'', 2, 1, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ 0 >= h'' ] with all transitions in problem 11, the following new transition is obtained:
	f0(a, b, c, e, f, g) -> f10(2, 0, h'', 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ 0 >= h'' ]
We thus obtain the following problem:
12:	T:
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 0, h'', 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ 0 >= h'' ]
		(1, 8)     f0(a, b, c, e, f, g) -> f21(2, 2, h'' - 1, 2, 2, h''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 ]
		(1, 7)     f0(a, b, c, e, f, g) -> f10(2, 2, h'', 2, 0, i) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ 0 >= i ]
		(1, 4)     f0(a, b, c, e, f, g) -> f21(1, 1, h - 2, 2, 2, h'') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ h'' >= 0 /\ 1 >= h'' /\ h - 1 >= 1 /\ 2 >= 2 ]
		(1, 3)     f0(a, b, c, e, f, g) -> f10(1, 1, h - 1, 2, 0, h') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ 0 >= h' ]
		(1, 3)     f0(a, b, c, e, f, g) -> f10(1, 0, h, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ 1 >= 1 /\ 2 >= 1 /\ 0 >= h /\ 1 >= 0 /\ 2 >= 0 /\ h + 1 >= 0 /\ 3 >= 1 ]
		(?, 2)     f10(a, b, c, e, f, g) -> f10(a, b - 1, c, e, f - 1, 0) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ f >= 1 /\ e >= f /\ b >= 1 /\ 0 >= c /\ 1 >= 0 /\ f >= 0 /\ -f + 3 >= 0 /\ e - 1 >= 0 /\ -e + 3 >= 0 /\ c + 1 >= 0 /\ a >= 0 /\ 0 >= 0 /\ f - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ a - b + 1 >= 0 /\ e + 1 >= a ]
		(?, 1)     f10(a, b, c, e, f, g) -> f21(a + 1, a + 1, h, e, f, i) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ i >= 0 /\ 1 >= i /\ h >= 0 /\ f >= 1 /\ e >= f /\ 0 >= b /\ 0 >= c ]
		(?, 1)     f10(a, b, c, e, f, g) -> f21(a, b, c - 1, e, f, h) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ h >= 0 /\ 1 >= h /\ f >= 1 /\ c >= 1 /\ e >= f ]
		(?, 1)     f21(a, b, c, e, f, g) -> f10(a, b, c, e, f - 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ 0 >= g ]
		(?, 1)     f21(a, b, c, e, f, g) -> f10(a, b, c, e, f + 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ g >= 1 ]
	start location:	f0
	leaf cost:	2

By chaining the transition f0(a, b, c, e, f, g) -> f21(2, 2, h'' - 1, 2, 2, h''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 ] with all transitions in problem 12, the following new transitions are obtained:
	f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 1, 2, 3, h''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ h''' >= 1 ]
	f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 1, 2, 1, h''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' ]
We thus obtain the following problem:
13:	T:
		(1, 9)     f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 1, 2, 3, h''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ h''' >= 1 ]
		(1, 9)     f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 1, 2, 1, h''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 0, h'', 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ 0 >= h'' ]
		(1, 7)     f0(a, b, c, e, f, g) -> f10(2, 2, h'', 2, 0, i) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ 0 >= i ]
		(1, 4)     f0(a, b, c, e, f, g) -> f21(1, 1, h - 2, 2, 2, h'') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ h'' >= 0 /\ 1 >= h'' /\ h - 1 >= 1 /\ 2 >= 2 ]
		(1, 3)     f0(a, b, c, e, f, g) -> f10(1, 1, h - 1, 2, 0, h') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ 0 >= h' ]
		(1, 3)     f0(a, b, c, e, f, g) -> f10(1, 0, h, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ 1 >= 1 /\ 2 >= 1 /\ 0 >= h /\ 1 >= 0 /\ 2 >= 0 /\ h + 1 >= 0 /\ 3 >= 1 ]
		(?, 2)     f10(a, b, c, e, f, g) -> f10(a, b - 1, c, e, f - 1, 0) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ f >= 1 /\ e >= f /\ b >= 1 /\ 0 >= c /\ 1 >= 0 /\ f >= 0 /\ -f + 3 >= 0 /\ e - 1 >= 0 /\ -e + 3 >= 0 /\ c + 1 >= 0 /\ a >= 0 /\ 0 >= 0 /\ f - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ a - b + 1 >= 0 /\ e + 1 >= a ]
		(?, 1)     f10(a, b, c, e, f, g) -> f21(a + 1, a + 1, h, e, f, i) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ i >= 0 /\ 1 >= i /\ h >= 0 /\ f >= 1 /\ e >= f /\ 0 >= b /\ 0 >= c ]
		(?, 1)     f10(a, b, c, e, f, g) -> f21(a, b, c - 1, e, f, h) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ h >= 0 /\ 1 >= h /\ f >= 1 /\ c >= 1 /\ e >= f ]
		(?, 1)     f21(a, b, c, e, f, g) -> f10(a, b, c, e, f - 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ 0 >= g ]
		(?, 1)     f21(a, b, c, e, f, g) -> f10(a, b, c, e, f + 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ g >= 1 ]
	start location:	f0
	leaf cost:	2

By chaining the transition f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 1, 2, 1, h''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' ] with all transitions in problem 13, the following new transitions are obtained:
	f0(a, b, c, e, f, g) -> f10(2, 1, h'' - 1, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ 0 >= h'' - 1 ]
	f0(a, b, c, e, f, g) -> f21(2, 2, h'' - 2, 2, 1, h'''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 ]
We thus obtain the following problem:
14:	T:
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 1, h'' - 1, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ 0 >= h'' - 1 ]
		(1, 10)    f0(a, b, c, e, f, g) -> f21(2, 2, h'' - 2, 2, 1, h'''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 ]
		(1, 9)     f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 1, 2, 3, h''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ h''' >= 1 ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 0, h'', 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ 0 >= h'' ]
		(1, 7)     f0(a, b, c, e, f, g) -> f10(2, 2, h'', 2, 0, i) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ 0 >= i ]
		(1, 4)     f0(a, b, c, e, f, g) -> f21(1, 1, h - 2, 2, 2, h'') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ h'' >= 0 /\ 1 >= h'' /\ h - 1 >= 1 /\ 2 >= 2 ]
		(1, 3)     f0(a, b, c, e, f, g) -> f10(1, 1, h - 1, 2, 0, h') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ 0 >= h' ]
		(1, 3)     f0(a, b, c, e, f, g) -> f10(1, 0, h, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ 1 >= 1 /\ 2 >= 1 /\ 0 >= h /\ 1 >= 0 /\ 2 >= 0 /\ h + 1 >= 0 /\ 3 >= 1 ]
		(?, 2)     f10(a, b, c, e, f, g) -> f10(a, b - 1, c, e, f - 1, 0) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ f >= 1 /\ e >= f /\ b >= 1 /\ 0 >= c /\ 1 >= 0 /\ f >= 0 /\ -f + 3 >= 0 /\ e - 1 >= 0 /\ -e + 3 >= 0 /\ c + 1 >= 0 /\ a >= 0 /\ 0 >= 0 /\ f - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ a - b + 1 >= 0 /\ e + 1 >= a ]
		(?, 1)     f10(a, b, c, e, f, g) -> f21(a + 1, a + 1, h, e, f, i) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ i >= 0 /\ 1 >= i /\ h >= 0 /\ f >= 1 /\ e >= f /\ 0 >= b /\ 0 >= c ]
		(?, 1)     f10(a, b, c, e, f, g) -> f21(a, b, c - 1, e, f, h) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ h >= 0 /\ 1 >= h /\ f >= 1 /\ c >= 1 /\ e >= f ]
		(?, 1)     f21(a, b, c, e, f, g) -> f10(a, b, c, e, f - 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ 0 >= g ]
		(?, 1)     f21(a, b, c, e, f, g) -> f10(a, b, c, e, f + 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ g >= 1 ]
	start location:	f0
	leaf cost:	2

By chaining the transition f0(a, b, c, e, f, g) -> f21(2, 2, h'' - 2, 2, 1, h'''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 ] with all transitions in problem 14, the following new transitions are obtained:
	f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 2, 2, 2, h'''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 ]
	f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 2, 2, 0, h'''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ 0 >= h'''' ]
We thus obtain the following problem:
15:	T:
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 2, 2, 2, h'''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 2, 2, 0, h'''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ 0 >= h'''' ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 1, h'' - 1, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ 0 >= h'' - 1 ]
		(1, 9)     f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 1, 2, 3, h''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ h''' >= 1 ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 0, h'', 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ 0 >= h'' ]
		(1, 7)     f0(a, b, c, e, f, g) -> f10(2, 2, h'', 2, 0, i) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ 0 >= i ]
		(1, 4)     f0(a, b, c, e, f, g) -> f21(1, 1, h - 2, 2, 2, h'') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ h'' >= 0 /\ 1 >= h'' /\ h - 1 >= 1 /\ 2 >= 2 ]
		(1, 3)     f0(a, b, c, e, f, g) -> f10(1, 1, h - 1, 2, 0, h') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ 0 >= h' ]
		(1, 3)     f0(a, b, c, e, f, g) -> f10(1, 0, h, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ 1 >= 1 /\ 2 >= 1 /\ 0 >= h /\ 1 >= 0 /\ 2 >= 0 /\ h + 1 >= 0 /\ 3 >= 1 ]
		(?, 2)     f10(a, b, c, e, f, g) -> f10(a, b - 1, c, e, f - 1, 0) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ f >= 1 /\ e >= f /\ b >= 1 /\ 0 >= c /\ 1 >= 0 /\ f >= 0 /\ -f + 3 >= 0 /\ e - 1 >= 0 /\ -e + 3 >= 0 /\ c + 1 >= 0 /\ a >= 0 /\ 0 >= 0 /\ f - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ a - b + 1 >= 0 /\ e + 1 >= a ]
		(?, 1)     f10(a, b, c, e, f, g) -> f21(a + 1, a + 1, h, e, f, i) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ i >= 0 /\ 1 >= i /\ h >= 0 /\ f >= 1 /\ e >= f /\ 0 >= b /\ 0 >= c ]
		(?, 1)     f10(a, b, c, e, f, g) -> f21(a, b, c - 1, e, f, h) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ h >= 0 /\ 1 >= h /\ f >= 1 /\ c >= 1 /\ e >= f ]
		(?, 1)     f21(a, b, c, e, f, g) -> f10(a, b, c, e, f - 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ 0 >= g ]
		(?, 1)     f21(a, b, c, e, f, g) -> f10(a, b, c, e, f + 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ g >= 1 ]
	start location:	f0
	leaf cost:	2

By chaining the transition f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 2, 2, 2, h'''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 ] with all transitions in problem 15, the following new transitions are obtained:
	f0(a, b, c, e, f, g) -> f10(2, 1, h'' - 2, 2, 1, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ 0 >= h'' - 2 ]
	f0(a, b, c, e, f, g) -> f21(2, 2, h'' - 3, 2, 2, h''''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ h''''' >= 0 /\ 1 >= h''''' /\ h'' - 2 >= 1 ]
We thus obtain the following problem:
16:	T:
		(1, 13)    f0(a, b, c, e, f, g) -> f10(2, 1, h'' - 2, 2, 1, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ 0 >= h'' - 2 ]
		(1, 12)    f0(a, b, c, e, f, g) -> f21(2, 2, h'' - 3, 2, 2, h''''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ h''''' >= 0 /\ 1 >= h''''' /\ h'' - 2 >= 1 ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 2, 2, 0, h'''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ 0 >= h'''' ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 1, h'' - 1, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ 0 >= h'' - 1 ]
		(1, 9)     f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 1, 2, 3, h''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ h''' >= 1 ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 0, h'', 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ 0 >= h'' ]
		(1, 7)     f0(a, b, c, e, f, g) -> f10(2, 2, h'', 2, 0, i) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ 0 >= i ]
		(1, 4)     f0(a, b, c, e, f, g) -> f21(1, 1, h - 2, 2, 2, h'') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ h'' >= 0 /\ 1 >= h'' /\ h - 1 >= 1 /\ 2 >= 2 ]
		(1, 3)     f0(a, b, c, e, f, g) -> f10(1, 1, h - 1, 2, 0, h') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ 0 >= h' ]
		(1, 3)     f0(a, b, c, e, f, g) -> f10(1, 0, h, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ 1 >= 1 /\ 2 >= 1 /\ 0 >= h /\ 1 >= 0 /\ 2 >= 0 /\ h + 1 >= 0 /\ 3 >= 1 ]
		(?, 2)     f10(a, b, c, e, f, g) -> f10(a, b - 1, c, e, f - 1, 0) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ f >= 1 /\ e >= f /\ b >= 1 /\ 0 >= c /\ 1 >= 0 /\ f >= 0 /\ -f + 3 >= 0 /\ e - 1 >= 0 /\ -e + 3 >= 0 /\ c + 1 >= 0 /\ a >= 0 /\ 0 >= 0 /\ f - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ a - b + 1 >= 0 /\ e + 1 >= a ]
		(?, 1)     f10(a, b, c, e, f, g) -> f21(a + 1, a + 1, h, e, f, i) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ i >= 0 /\ 1 >= i /\ h >= 0 /\ f >= 1 /\ e >= f /\ 0 >= b /\ 0 >= c ]
		(?, 1)     f10(a, b, c, e, f, g) -> f21(a, b, c - 1, e, f, h) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ h >= 0 /\ 1 >= h /\ f >= 1 /\ c >= 1 /\ e >= f ]
		(?, 1)     f21(a, b, c, e, f, g) -> f10(a, b, c, e, f - 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ 0 >= g ]
		(?, 1)     f21(a, b, c, e, f, g) -> f10(a, b, c, e, f + 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ g >= 1 ]
	start location:	f0
	leaf cost:	2

By chaining the transition f0(a, b, c, e, f, g) -> f10(2, 1, h'' - 2, 2, 1, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ 0 >= h'' - 2 ] with all transitions in problem 16, the following new transition is obtained:
	f0(a, b, c, e, f, g) -> f10(2, 0, h'' - 2, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ 0 >= h'' - 2 ]
We thus obtain the following problem:
17:	T:
		(1, 15)    f0(a, b, c, e, f, g) -> f10(2, 0, h'' - 2, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ 0 >= h'' - 2 ]
		(1, 12)    f0(a, b, c, e, f, g) -> f21(2, 2, h'' - 3, 2, 2, h''''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ h''''' >= 0 /\ 1 >= h''''' /\ h'' - 2 >= 1 ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 2, 2, 0, h'''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ 0 >= h'''' ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 1, h'' - 1, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ 0 >= h'' - 1 ]
		(1, 9)     f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 1, 2, 3, h''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ h''' >= 1 ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 0, h'', 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ 0 >= h'' ]
		(1, 7)     f0(a, b, c, e, f, g) -> f10(2, 2, h'', 2, 0, i) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ 0 >= i ]
		(1, 4)     f0(a, b, c, e, f, g) -> f21(1, 1, h - 2, 2, 2, h'') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ h'' >= 0 /\ 1 >= h'' /\ h - 1 >= 1 /\ 2 >= 2 ]
		(1, 3)     f0(a, b, c, e, f, g) -> f10(1, 1, h - 1, 2, 0, h') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ 0 >= h' ]
		(1, 3)     f0(a, b, c, e, f, g) -> f10(1, 0, h, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ 1 >= 1 /\ 2 >= 1 /\ 0 >= h /\ 1 >= 0 /\ 2 >= 0 /\ h + 1 >= 0 /\ 3 >= 1 ]
		(?, 2)     f10(a, b, c, e, f, g) -> f10(a, b - 1, c, e, f - 1, 0) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ f >= 1 /\ e >= f /\ b >= 1 /\ 0 >= c /\ 1 >= 0 /\ f >= 0 /\ -f + 3 >= 0 /\ e - 1 >= 0 /\ -e + 3 >= 0 /\ c + 1 >= 0 /\ a >= 0 /\ 0 >= 0 /\ f - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ a - b + 1 >= 0 /\ e + 1 >= a ]
		(?, 1)     f10(a, b, c, e, f, g) -> f21(a + 1, a + 1, h, e, f, i) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ i >= 0 /\ 1 >= i /\ h >= 0 /\ f >= 1 /\ e >= f /\ 0 >= b /\ 0 >= c ]
		(?, 1)     f10(a, b, c, e, f, g) -> f21(a, b, c - 1, e, f, h) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ h >= 0 /\ 1 >= h /\ f >= 1 /\ c >= 1 /\ e >= f ]
		(?, 1)     f21(a, b, c, e, f, g) -> f10(a, b, c, e, f - 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ 0 >= g ]
		(?, 1)     f21(a, b, c, e, f, g) -> f10(a, b, c, e, f + 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ g >= 1 ]
	start location:	f0
	leaf cost:	2

By chaining the transition f0(a, b, c, e, f, g) -> f21(2, 2, h'' - 3, 2, 2, h''''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ h''''' >= 0 /\ 1 >= h''''' /\ h'' - 2 >= 1 ] with all transitions in problem 17, the following new transitions are obtained:
	f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 3, 2, 3, h''''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ h''''' >= 0 /\ 1 >= h''''' /\ h'' - 2 >= 1 /\ -h''''' + 1 >= 0 /\ -h''''' + 2 >= 0 /\ h'' - h''''' - 2 >= 0 /\ h''''' + 1 >= 0 /\ h'' + h''''' - 3 >= 0 /\ h'' - 3 >= 0 /\ h''''' >= 1 ]
	f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 3, 2, 1, h''''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ h''''' >= 0 /\ 1 >= h''''' /\ h'' - 2 >= 1 /\ -h''''' + 1 >= 0 /\ -h''''' + 2 >= 0 /\ h'' - h''''' - 2 >= 0 /\ h''''' + 1 >= 0 /\ h'' + h''''' - 3 >= 0 /\ h'' - 3 >= 0 /\ 0 >= h''''' ]
We thus obtain the following problem:
18:	T:
		(1, 13)    f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 3, 2, 3, h''''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ h''''' >= 0 /\ 1 >= h''''' /\ h'' - 2 >= 1 /\ -h''''' + 1 >= 0 /\ -h''''' + 2 >= 0 /\ h'' - h''''' - 2 >= 0 /\ h''''' + 1 >= 0 /\ h'' + h''''' - 3 >= 0 /\ h'' - 3 >= 0 /\ h''''' >= 1 ]
		(1, 13)    f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 3, 2, 1, h''''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ h''''' >= 0 /\ 1 >= h''''' /\ h'' - 2 >= 1 /\ -h''''' + 1 >= 0 /\ -h''''' + 2 >= 0 /\ h'' - h''''' - 2 >= 0 /\ h''''' + 1 >= 0 /\ h'' + h''''' - 3 >= 0 /\ h'' - 3 >= 0 /\ 0 >= h''''' ]
		(1, 15)    f0(a, b, c, e, f, g) -> f10(2, 0, h'' - 2, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ 0 >= h'' - 2 ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 2, 2, 0, h'''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ 0 >= h'''' ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 1, h'' - 1, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ 0 >= h'' - 1 ]
		(1, 9)     f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 1, 2, 3, h''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ h''' >= 1 ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 0, h'', 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ 0 >= h'' ]
		(1, 7)     f0(a, b, c, e, f, g) -> f10(2, 2, h'', 2, 0, i) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ 0 >= i ]
		(1, 4)     f0(a, b, c, e, f, g) -> f21(1, 1, h - 2, 2, 2, h'') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ h'' >= 0 /\ 1 >= h'' /\ h - 1 >= 1 /\ 2 >= 2 ]
		(1, 3)     f0(a, b, c, e, f, g) -> f10(1, 1, h - 1, 2, 0, h') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ 0 >= h' ]
		(1, 3)     f0(a, b, c, e, f, g) -> f10(1, 0, h, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ 1 >= 1 /\ 2 >= 1 /\ 0 >= h /\ 1 >= 0 /\ 2 >= 0 /\ h + 1 >= 0 /\ 3 >= 1 ]
		(?, 2)     f10(a, b, c, e, f, g) -> f10(a, b - 1, c, e, f - 1, 0) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ f >= 1 /\ e >= f /\ b >= 1 /\ 0 >= c /\ 1 >= 0 /\ f >= 0 /\ -f + 3 >= 0 /\ e - 1 >= 0 /\ -e + 3 >= 0 /\ c + 1 >= 0 /\ a >= 0 /\ 0 >= 0 /\ f - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ a - b + 1 >= 0 /\ e + 1 >= a ]
		(?, 1)     f10(a, b, c, e, f, g) -> f21(a + 1, a + 1, h, e, f, i) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ i >= 0 /\ 1 >= i /\ h >= 0 /\ f >= 1 /\ e >= f /\ 0 >= b /\ 0 >= c ]
		(?, 1)     f10(a, b, c, e, f, g) -> f21(a, b, c - 1, e, f, h) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ h >= 0 /\ 1 >= h /\ f >= 1 /\ c >= 1 /\ e >= f ]
		(?, 1)     f21(a, b, c, e, f, g) -> f10(a, b, c, e, f - 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ 0 >= g ]
		(?, 1)     f21(a, b, c, e, f, g) -> f10(a, b, c, e, f + 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ g >= 1 ]
	start location:	f0
	leaf cost:	2

By chaining the transition f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 3, 2, 1, h''''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ h''''' >= 0 /\ 1 >= h''''' /\ h'' - 2 >= 1 /\ -h''''' + 1 >= 0 /\ -h''''' + 2 >= 0 /\ h'' - h''''' - 2 >= 0 /\ h''''' + 1 >= 0 /\ h'' + h''''' - 3 >= 0 /\ h'' - 3 >= 0 /\ 0 >= h''''' ] with all transitions in problem 18, the following new transitions are obtained:
	f0(a, b, c, e, f, g) -> f10(2, 1, h'' - 3, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ h''''' >= 0 /\ 1 >= h''''' /\ h'' - 2 >= 1 /\ -h''''' + 1 >= 0 /\ -h''''' + 2 >= 0 /\ h'' - h''''' - 2 >= 0 /\ h''''' + 1 >= 0 /\ h'' + h''''' - 3 >= 0 /\ h'' - 3 >= 0 /\ 0 >= h''''' /\ 0 >= h'' - 3 ]
	f0(a, b, c, e, f, g) -> f21(2, 2, h'' - 4, 2, 1, h'''''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ h''''' >= 0 /\ 1 >= h''''' /\ h'' - 2 >= 1 /\ -h''''' + 1 >= 0 /\ -h''''' + 2 >= 0 /\ h'' - h''''' - 2 >= 0 /\ h''''' + 1 >= 0 /\ h'' + h''''' - 3 >= 0 /\ h'' - 3 >= 0 /\ 0 >= h''''' /\ h'''''' >= 0 /\ 1 >= h'''''' /\ h'' - 3 >= 1 ]
We thus obtain the following problem:
19:	T:
		(1, 15)    f0(a, b, c, e, f, g) -> f10(2, 1, h'' - 3, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ h''''' >= 0 /\ 1 >= h''''' /\ h'' - 2 >= 1 /\ -h''''' + 1 >= 0 /\ -h''''' + 2 >= 0 /\ h'' - h''''' - 2 >= 0 /\ h''''' + 1 >= 0 /\ h'' + h''''' - 3 >= 0 /\ h'' - 3 >= 0 /\ 0 >= h''''' /\ 0 >= h'' - 3 ]
		(1, 14)    f0(a, b, c, e, f, g) -> f21(2, 2, h'' - 4, 2, 1, h'''''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ h''''' >= 0 /\ 1 >= h''''' /\ h'' - 2 >= 1 /\ -h''''' + 1 >= 0 /\ -h''''' + 2 >= 0 /\ h'' - h''''' - 2 >= 0 /\ h''''' + 1 >= 0 /\ h'' + h''''' - 3 >= 0 /\ h'' - 3 >= 0 /\ 0 >= h''''' /\ h'''''' >= 0 /\ 1 >= h'''''' /\ h'' - 3 >= 1 ]
		(1, 13)    f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 3, 2, 3, h''''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ h''''' >= 0 /\ 1 >= h''''' /\ h'' - 2 >= 1 /\ -h''''' + 1 >= 0 /\ -h''''' + 2 >= 0 /\ h'' - h''''' - 2 >= 0 /\ h''''' + 1 >= 0 /\ h'' + h''''' - 3 >= 0 /\ h'' - 3 >= 0 /\ h''''' >= 1 ]
		(1, 15)    f0(a, b, c, e, f, g) -> f10(2, 0, h'' - 2, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ h'''' >= 1 /\ 0 >= h'' - 2 ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 2, 2, 0, h'''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ h'''' >= 0 /\ 1 >= h'''' /\ h'' - 1 >= 1 /\ -h'''' + 1 >= 0 /\ -h'''' + 2 >= 0 /\ h'' - h'''' - 1 >= 0 /\ h'''' + 1 >= 0 /\ h'' + h'''' - 2 >= 0 /\ h'' - 2 >= 0 /\ 0 >= h'''' ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 1, h'' - 1, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ 0 >= h''' /\ 0 >= h'' - 1 ]
		(1, 9)     f0(a, b, c, e, f, g) -> f10(2, 2, h'' - 1, 2, 3, h''') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ h''' >= 0 /\ 1 >= h''' /\ h'' >= 1 /\ -h''' + 1 >= 0 /\ -h''' + 2 >= 0 /\ h'' - h''' >= 0 /\ h''' + 1 >= 0 /\ h'' + h''' - 1 >= 0 /\ h'' - 1 >= 0 /\ h''' >= 1 ]
		(1, 11)    f0(a, b, c, e, f, g) -> f10(2, 0, h'', 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ i >= 1 /\ 0 >= h'' ]
		(1, 7)     f0(a, b, c, e, f, g) -> f10(2, 2, h'', 2, 0, i) [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ 2 >= 2 /\ 0 >= h - 1 /\ 2 >= 0 /\ i >= 0 /\ 1 >= i /\ h'' >= 0 /\ -i + 1 >= 0 /\ -i + 2 >= 0 /\ h'' - i + 1 >= 0 /\ i + 1 >= 0 /\ h'' + i >= 0 /\ h'' + 1 >= 0 /\ 3 >= 2 /\ 0 >= i ]
		(1, 4)     f0(a, b, c, e, f, g) -> f21(1, 1, h - 2, 2, 2, h'') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ h' >= 1 /\ h'' >= 0 /\ 1 >= h'' /\ h - 1 >= 1 /\ 2 >= 2 ]
		(1, 3)     f0(a, b, c, e, f, g) -> f10(1, 1, h - 1, 2, 0, h') [ h >= 0 /\ 0 >= 0 /\ h' >= 0 /\ 1 >= h' /\ 1 >= 1 /\ h >= 1 /\ 2 >= 1 /\ -h' + 1 >= 0 /\ -h' + 2 >= 0 /\ h - h' >= 0 /\ h' + 1 >= 0 /\ h + h' - 1 >= 0 /\ 1 >= 0 /\ h - 1 >= 0 /\ 3 >= 1 /\ 0 >= h' ]
		(1, 3)     f0(a, b, c, e, f, g) -> f10(1, 0, h, 2, 0, 0) [ h >= 0 /\ 0 >= 0 /\ 1 >= 1 /\ 2 >= 1 /\ 0 >= h /\ 1 >= 0 /\ 2 >= 0 /\ h + 1 >= 0 /\ 3 >= 1 ]
		(?, 2)     f10(a, b, c, e, f, g) -> f10(a, b - 1, c, e, f - 1, 0) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ f >= 1 /\ e >= f /\ b >= 1 /\ 0 >= c /\ 1 >= 0 /\ f >= 0 /\ -f + 3 >= 0 /\ e - 1 >= 0 /\ -e + 3 >= 0 /\ c + 1 >= 0 /\ a >= 0 /\ 0 >= 0 /\ f - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ a - b + 1 >= 0 /\ e + 1 >= a ]
		(?, 1)     f10(a, b, c, e, f, g) -> f21(a + 1, a + 1, h, e, f, i) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ i >= 0 /\ 1 >= i /\ h >= 0 /\ f >= 1 /\ e >= f /\ 0 >= b /\ 0 >= c ]
		(?, 1)     f10(a, b, c, e, f, g) -> f21(a, b, c - 1, e, f, h) [ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ h >= 0 /\ 1 >= h /\ f >= 1 /\ c >= 1 /\ e >= f ]
		(?, 1)     f21(a, b, c, e, f, g) -> f10(a, b, c, e, f - 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ 0 >= g ]
		(?, 1)     f21(a, b, c, e, f, g) -> f10(a, b, c, e, f + 1, g) [ -g + 1 >= 0 /\ f - g >= 0 /\ -f - g + 3 >= 0 /\ e - g - 1 >= 0 /\ -e - g + 3 >= 0 /\ c - g + 1 >= 0 /\ a - g >= 0 /\ g >= 0 /\ f + g - 1 >= 0 /\ -f + g + 2 >= 0 /\ e + g - 2 >= 0 /\ -e + g + 2 >= 0 /\ c + g >= 0 /\ a + g - 1 >= 0 /\ -f + 2 >= 0 /\ e - f >= 0 /\ -e - f + 4 >= 0 /\ c - f + 2 >= 0 /\ a - f + 1 >= 0 /\ f - 1 >= 0 /\ e + f - 3 >= 0 /\ -e + f + 1 >= 0 /\ c + f - 1 >= 0 /\ a + f - 2 >= 0 /\ -e + 2 >= 0 /\ c - e + 2 >= 0 /\ a - e + 1 >= 0 /\ e - 2 >= 0 /\ c + e - 2 >= 0 /\ a + e - 3 >= 0 /\ c >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ a - 1 >= 0 /\ e + 1 >= a /\ g >= 1 ]
	start location:	f0
	leaf cost:	2

Complexity upper bound ?

Time: 5.163 sec (SMT: 4.144 sec)