MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f4(a, b, c, d, e, f) -> f14(a, b, c, d, e, f) [ 0 >= a ]
		(?, 1)    f13(a, b, c, d, e, f) -> f4(a, b, c, d, e, f)
		(?, 1)    f13(a, b, c, d, e, f) -> f400(a, b, c, d, e, f) [ b >= a + 1 ]
		(1, 1)    f2(a, b, c, d, e, f) -> f23(g, i, h, j, 1, f) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
		(1, 1)    f2(a, b, c, d, e, f) -> f23(g, i, h, j, 1, 0) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(?, 1)    f23(a, b, c, d, e, f) -> f4(a, b, c, d, e, f) [ e >= c ]
		(?, 1)    f23(a, b, c, d, e, f) -> f4(a, b, c, d, e, 1) [ c >= e + 1 ]
		(?, 1)    f4(a, b, c, d, e, f) -> f33(a - 1, b, h, j, c, f) [ h >= c /\ 0 >= b /\ a >= 1 ]
		(?, 1)    f4(a, b, c, d, e, f) -> f33(a - 1, b, h, j, c, 0) [ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 1)    f33(a, b, c, d, e, f) -> f6(a, b, c, d, e, f) [ e >= c ]
		(?, 1)    f33(a, b, c, d, e, f) -> f6(a, b, c, d, e, 1) [ c >= e + 1 ]
		(?, 1)    f6(a, b, c, d, e, f) -> f43(a, b, h, j, c, f) [ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f6(a, b, c, d, e, f) -> f43(a, b, h, j, c, 0) [ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f43(a, b, c, d, e, f) -> f6(a, b, c, d, c, f) [ c = e ]
		(?, 1)    f43(a, b, c, d, e, f) -> f6(a, b, c, d, e, 1) [ c >= e + 1 ]
		(?, 1)    f6(a, b, c, d, e, f) -> f53(a, b, h, j, c - 1, f) [ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, d, e, f) -> f53(a, b, h, j, c - 1, 0) [ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f53(a, b, c, d, e, f) -> f61(a, a, c, d, c, f) [ e >= c ]
		(?, 1)    f53(a, b, c, d, e, f) -> f61(a, a, c, d, c, 1) [ c >= e + 1 ]
		(?, 1)    f61(a, b, c, d, e, f) -> f63(a, b, h, j, e, f) [ 0 >= b /\ h >= e ]
		(?, 1)    f61(a, b, c, d, e, f) -> f63(a, b, h, j, e, 0) [ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, d, e, f) -> f71(a, b, c, d + 1, c, f) [ e >= c ]
		(?, 1)    f63(a, b, c, d, e, f) -> f71(a, b, c, d + 1, c, 1) [ c >= e + 1 ]
		(?, 1)    f71(a, b, c, d, e, f) -> f73(a, b, h, j, e, f) [ 0 >= b /\ h >= e ]
		(?, 1)    f71(a, b, c, d, e, f) -> f73(a, b, h, j, e, 0) [ b >= 1 /\ h >= e ]
		(?, 1)    f73(a, b, c, d, e, f) -> f13(a, b, c, d, e, f) [ e >= c ]
		(?, 1)    f73(a, b, c, d, e, f) -> f13(a, b, c, d, e, 1) [ c >= e + 1 ]
	start location:	f2
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, e].
We thus obtain the following problem:
2:	T:
		(?, 1)    f73(a, b, c, e) -> f13(a, b, c, e) [ c >= e + 1 ]
		(?, 1)    f73(a, b, c, e) -> f13(a, b, c, e) [ e >= c ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ b >= 1 /\ h >= e ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ 0 >= b /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c >= e + 1 ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ e >= c ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ b >= 1 /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ 0 >= b /\ h >= e ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c >= e + 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ e >= c ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ c >= e + 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ c = e ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c >= e + 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ e >= c ]
		(?, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ h >= c /\ 0 >= b /\ a >= 1 ]
		(?, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ c >= e + 1 ]
		(?, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ e >= c ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
		(?, 1)    f13(a, b, c, e) -> f400(a, b, c, e) [ b >= a + 1 ]
		(?, 1)    f13(a, b, c, e) -> f4(a, b, c, e)
		(?, 1)    f4(a, b, c, e) -> f14(a, b, c, e) [ 0 >= a ]
	start location:	f2
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(?, 1)    f73(a, b, c, e) -> f13(a, b, c, e) [ c >= e + 1 ]
		(?, 1)    f73(a, b, c, e) -> f13(a, b, c, e) [ e >= c ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ b >= 1 /\ h >= e ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ 0 >= b /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c >= e + 1 ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ e >= c ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ b >= 1 /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ 0 >= b /\ h >= e ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c >= e + 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ e >= c ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ c >= e + 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ c = e ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c >= e + 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ e >= c ]
		(?, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ h >= c /\ 0 >= b /\ a >= 1 ]
		(?, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ c >= e + 1 ]
		(?, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ e >= c ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
		(?, 1)    f13(a, b, c, e) -> f4(a, b, c, e)
	start location:	f2
	leaf cost:	2

Repeatedly propagating knowledge in problem 3 produces the following problem:
4:	T:
		(?, 1)    f73(a, b, c, e) -> f13(a, b, c, e) [ c >= e + 1 ]
		(?, 1)    f73(a, b, c, e) -> f13(a, b, c, e) [ e >= c ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ b >= 1 /\ h >= e ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ 0 >= b /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c >= e + 1 ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ e >= c ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ b >= 1 /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ 0 >= b /\ h >= e ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c >= e + 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ e >= c ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ c >= e + 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ c = e ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c >= e + 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ e >= c ]
		(?, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ h >= c /\ 0 >= b /\ a >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ c >= e + 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ e >= c ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
		(?, 1)    f13(a, b, c, e) -> f4(a, b, c, e)
	start location:	f2
	leaf cost:	2

Applied AI with 'oct' on problem 4 to obtain the following invariants:
  For symbol f13: X_3 - X_4 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ X_2 + X_4 >= 0 /\ X_1 + X_4 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 >= 0 /\ X_1 - X_2 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 >= 0 /\ -X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol f23: -X_4 + 1 >= 0 /\ X_3 - X_4 >= 0 /\ X_1 - X_4 >= 0 /\ X_4 - 1 >= 0 /\ X_3 + X_4 - 2 >= 0 /\ X_1 + X_4 - 2 >= 0 /\ X_3 - 1 >= 0 /\ X_1 + X_3 - 2 >= 0 /\ X_1 - 1 >= 0
  For symbol f33: X_3 - X_4 >= 0 /\ X_1 >= 0
  For symbol f4: X_3 - X_4 >= 0
  For symbol f43: -X_4 >= 0 /\ X_3 - X_4 >= 0 /\ X_1 - X_4 >= 0 /\ X_1 >= 0
  For symbol f53: X_3 - X_4 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ X_1 + X_4 >= 0 /\ X_3 >= 0 /\ X_1 + X_3 >= 0 /\ X_1 >= 0
  For symbol f6: X_3 - X_4 >= 0 /\ X_1 >= 0
  For symbol f61: X_3 - X_4 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ -X_3 + X_4 >= 0 /\ X_2 + X_4 >= 0 /\ X_1 + X_4 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 >= 0 /\ X_1 - X_2 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 >= 0 /\ -X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol f63: X_3 - X_4 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ X_2 + X_4 >= 0 /\ X_1 + X_4 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 >= 0 /\ X_1 - X_2 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 >= 0 /\ -X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol f71: X_3 - X_4 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ -X_3 + X_4 >= 0 /\ X_2 + X_4 >= 0 /\ X_1 + X_4 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 >= 0 /\ X_1 - X_2 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 >= 0 /\ -X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol f73: X_3 - X_4 >= 0 /\ X_4 >= 0 /\ X_3 + X_4 >= 0 /\ X_2 + X_4 >= 0 /\ X_1 + X_4 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 >= 0 /\ X_1 - X_2 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 >= 0 /\ -X_1 + X_2 >= 0 /\ X_1 >= 0


This yielded the following problem:
5:	T:
		(?, 1)    f13(a, b, c, e) -> f4(a, b, c, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(?, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(?, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f73(a, b, c, e) -> f13(a, b, c, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f73(a, b, c, e) -> f13(a, b, c, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
	start location:	f2
	leaf cost:	2

Repeatedly propagating knowledge in problem 5 produces the following problem:
6:	T:
		(?, 1)    f13(a, b, c, e) -> f4(a, b, c, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(?, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f73(a, b, c, e) -> f13(a, b, c, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f73(a, b, c, e) -> f13(a, b, c, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
	start location:	f2
	leaf cost:	2

By chaining the transition f13(a, b, c, e) -> f4(a, b, c, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 ] with all transitions in problem 6, the following new transition is obtained:
	f13(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
We thus obtain the following problem:
7:	T:
		(?, 2)    f13(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(?, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f73(a, b, c, e) -> f13(a, b, c, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f73(a, b, c, e) -> f13(a, b, c, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
	start location:	f2
	leaf cost:	2

Repeatedly propagating knowledge in problem 7 produces the following problem:
8:	T:
		(?, 2)    f13(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f73(a, b, c, e) -> f13(a, b, c, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f73(a, b, c, e) -> f13(a, b, c, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
	start location:	f2
	leaf cost:	2

By chaining the transition f73(a, b, c, e) -> f13(a, b, c, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ] with all transitions in problem 8, the following new transition is obtained:
	f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
We thus obtain the following problem:
9:	T:
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 2)    f13(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f73(a, b, c, e) -> f13(a, b, c, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
	start location:	f2
	leaf cost:	2

By chaining the transition f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ] with all transitions in problem 9, the following new transition is obtained:
	f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
We thus obtain the following problem:
10:	T:
		(?, 2)    f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 2)    f13(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f73(a, b, c, e) -> f13(a, b, c, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
	start location:	f2
	leaf cost:	2

By chaining the transition f73(a, b, c, e) -> f13(a, b, c, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ] with all transitions in problem 10, the following new transition is obtained:
	f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 ]
We thus obtain the following problem:
11:	T:
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 2)    f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 2)    f13(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
	start location:	f2
	leaf cost:	2

Testing for reachability in the complexity graph removes the following transition from problem 11:
	f13(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
We thus obtain the following problem:
12:	T:
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 2)    f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
	start location:	f2
	leaf cost:	2

A polynomial rank function with
	Pol(f73) = 1
	Pol(f33) = 1
	Pol(f71) = 1
	Pol(f13) = 0
	Pol(f63) = 1
	Pol(f61) = 1
	Pol(f53) = 1
	Pol(f43) = 1
	Pol(f6) = 1
	Pol(f4) = 1
	Pol(f23) = 1
	Pol(f2) = 1
orients all transitions weakly and the transition
	f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
strictly and produces the following problem:
13:	T:
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 2)    f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
	start location:	f2
	leaf cost:	2

By chaining the transition f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 ] with all transitions in problem 13, the following new transitions are obtained:
	f73(a, b, c, e) -> f6(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ h >= c + 1 ]
	f73(a, b, c, e) -> f6(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h ]
We thus obtain the following problem:
14:	T:
		(?, 4)    f73(a, b, c, e) -> f6(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ h >= c + 1 ]
		(?, 4)    f73(a, b, c, e) -> f6(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h ]
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 2)    f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
	start location:	f2
	leaf cost:	2

By chaining the transition f73(a, b, c, e) -> f6(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ h >= c + 1 ] with all transitions in problem 14, the following new transition is obtained:
	f73(a, b, c, e) -> f53(a - 1, b, h', h - 1) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ h >= c + 1 /\ h' + 1 >= h /\ h >= 1 ]
We thus obtain the following problem:
15:	T:
		(?, 5)    f73(a, b, c, e) -> f53(a - 1, b, h', h - 1) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ h >= c + 1 /\ h' + 1 >= h /\ h >= 1 ]
		(?, 4)    f73(a, b, c, e) -> f6(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h ]
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 2)    f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
	start location:	f2
	leaf cost:	2

By chaining the transition f73(a, b, c, e) -> f6(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h ] with all transitions in problem 15, the following new transition is obtained:
	f73(a, b, c, e) -> f53(a - 1, b, h', h - 1) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 ]
We thus obtain the following problem:
16:	T:
		(?, 5)    f73(a, b, c, e) -> f53(a - 1, b, h', h - 1) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 ]
		(?, 5)    f73(a, b, c, e) -> f53(a - 1, b, h', h - 1) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ h >= c + 1 /\ h' + 1 >= h /\ h >= 1 ]
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 2)    f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
	start location:	f2
	leaf cost:	2

By chaining the transition f73(a, b, c, e) -> f53(a - 1, b, h', h - 1) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 ] with all transitions in problem 16, the following new transitions are obtained:
	f73(a, b, c, e) -> f61(a - 1, a - 1, h', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h ]
	f73(a, b, c, e) -> f61(a - 1, a - 1, h', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h - 1 >= h' ]
We thus obtain the following problem:
17:	T:
		(?, 6)    f73(a, b, c, e) -> f61(a - 1, a - 1, h', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h ]
		(?, 6)    f73(a, b, c, e) -> f61(a - 1, a - 1, h', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h - 1 >= h' ]
		(?, 5)    f73(a, b, c, e) -> f53(a - 1, b, h', h - 1) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ h >= c + 1 /\ h' + 1 >= h /\ h >= 1 ]
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 2)    f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
	start location:	f2
	leaf cost:	2

By chaining the transition f73(a, b, c, e) -> f61(a - 1, a - 1, h', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h ] with all transitions in problem 17, the following new transitions are obtained:
	f73(a, b, c, e) -> f63(a - 1, a - 1, h'', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' ]
	f73(a, b, c, e) -> f63(a - 1, a - 1, h'', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' ]
We thus obtain the following problem:
18:	T:
		(?, 7)    f73(a, b, c, e) -> f63(a - 1, a - 1, h'', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' ]
		(?, 7)    f73(a, b, c, e) -> f63(a - 1, a - 1, h'', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' ]
		(?, 6)    f73(a, b, c, e) -> f61(a - 1, a - 1, h', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h - 1 >= h' ]
		(?, 5)    f73(a, b, c, e) -> f53(a - 1, b, h', h - 1) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ h >= c + 1 /\ h' + 1 >= h /\ h >= 1 ]
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 2)    f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
	start location:	f2
	leaf cost:	2

By chaining the transition f73(a, b, c, e) -> f63(a - 1, a - 1, h'', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' ] with all transitions in problem 18, the following new transitions are obtained:
	f73(a, b, c, e) -> f71(a - 1, a - 1, h'', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 ]
	f73(a, b, c, e) -> f71(a - 1, a - 1, h'', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' ]
We thus obtain the following problem:
19:	T:
		(?, 8)    f73(a, b, c, e) -> f71(a - 1, a - 1, h'', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 ]
		(?, 8)    f73(a, b, c, e) -> f71(a - 1, a - 1, h'', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' ]
		(?, 7)    f73(a, b, c, e) -> f63(a - 1, a - 1, h'', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' ]
		(?, 6)    f73(a, b, c, e) -> f61(a - 1, a - 1, h', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h - 1 >= h' ]
		(?, 5)    f73(a, b, c, e) -> f53(a - 1, b, h', h - 1) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ h >= c + 1 /\ h' + 1 >= h /\ h >= 1 ]
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 2)    f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
	start location:	f2
	leaf cost:	2

By chaining the transition f73(a, b, c, e) -> f71(a - 1, a - 1, h'', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 ] with all transitions in problem 19, the following new transition is obtained:
	f73(a, b, c, e) -> f73(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 /\ 2*h'' >= 0 /\ h''' >= h'' ]
We thus obtain the following problem:
20:	T:
		(?, 9)    f73(a, b, c, e) -> f73(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 /\ 2*h'' >= 0 /\ h''' >= h'' ]
		(?, 8)    f73(a, b, c, e) -> f71(a - 1, a - 1, h'', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' ]
		(?, 7)    f73(a, b, c, e) -> f63(a - 1, a - 1, h'', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' ]
		(?, 6)    f73(a, b, c, e) -> f61(a - 1, a - 1, h', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h - 1 >= h' ]
		(?, 5)    f73(a, b, c, e) -> f53(a - 1, b, h', h - 1) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ h >= c + 1 /\ h' + 1 >= h /\ h >= 1 ]
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 2)    f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
	start location:	f2
	leaf cost:	2

By chaining the transition f73(a, b, c, e) -> f71(a - 1, a - 1, h'', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' ] with all transitions in problem 20, the following new transition is obtained:
	f73(a, b, c, e) -> f73(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' /\ 2*h'' >= 0 /\ h''' >= h'' ]
We thus obtain the following problem:
21:	T:
		(?, 9)    f73(a, b, c, e) -> f73(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' /\ 2*h'' >= 0 /\ h''' >= h'' ]
		(?, 9)    f73(a, b, c, e) -> f73(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 /\ 2*h'' >= 0 /\ h''' >= h'' ]
		(?, 7)    f73(a, b, c, e) -> f63(a - 1, a - 1, h'', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' ]
		(?, 6)    f73(a, b, c, e) -> f61(a - 1, a - 1, h', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h - 1 >= h' ]
		(?, 5)    f73(a, b, c, e) -> f53(a - 1, b, h', h - 1) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ h >= c + 1 /\ h' + 1 >= h /\ h >= 1 ]
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 2)    f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
	start location:	f2
	leaf cost:	2

By chaining the transition f73(a, b, c, e) -> f63(a - 1, a - 1, h'', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' ] with all transitions in problem 21, the following new transitions are obtained:
	f73(a, b, c, e) -> f71(a - 1, a - 1, h'', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 ]
	f73(a, b, c, e) -> f71(a - 1, a - 1, h'', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' ]
We thus obtain the following problem:
22:	T:
		(?, 8)    f73(a, b, c, e) -> f71(a - 1, a - 1, h'', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 ]
		(?, 8)    f73(a, b, c, e) -> f71(a - 1, a - 1, h'', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' ]
		(?, 9)    f73(a, b, c, e) -> f73(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' /\ 2*h'' >= 0 /\ h''' >= h'' ]
		(?, 9)    f73(a, b, c, e) -> f73(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 /\ 2*h'' >= 0 /\ h''' >= h'' ]
		(?, 6)    f73(a, b, c, e) -> f61(a - 1, a - 1, h', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h - 1 >= h' ]
		(?, 5)    f73(a, b, c, e) -> f53(a - 1, b, h', h - 1) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ h >= c + 1 /\ h' + 1 >= h /\ h >= 1 ]
		(?, 3)    f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 2)    f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 1)    f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)    f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)    f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)    f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(4, 1)    f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(2, 1)    f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)    f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
	start location:	f2
	leaf cost:	2

By chaining the transition f73(a, b, c, e) -> f71(a - 1, a - 1, h'', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 ] with all transitions in problem 22, the following new transition is obtained:
	f73(a, b, c, e) -> f13(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 /\ 2*h'' >= 0 /\ h''' >= h'' /\ h''' - h'' >= 0 /\ h''' + h'' >= 0 /\ h''' >= 0 /\ a + h''' - 1 >= 0 /\ h''' >= h'' + 1 ]
We thus obtain the following problem:
23:	T:
		(?, 10)    f73(a, b, c, e) -> f13(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 /\ 2*h'' >= 0 /\ h''' >= h'' /\ h''' - h'' >= 0 /\ h''' + h'' >= 0 /\ h''' >= 0 /\ a + h''' - 1 >= 0 /\ h''' >= h'' + 1 ]
		(?, 8)     f73(a, b, c, e) -> f71(a - 1, a - 1, h'', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' ]
		(?, 9)     f73(a, b, c, e) -> f73(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' /\ 2*h'' >= 0 /\ h''' >= h'' ]
		(?, 9)     f73(a, b, c, e) -> f73(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 /\ 2*h'' >= 0 /\ h''' >= h'' ]
		(?, 6)     f73(a, b, c, e) -> f61(a - 1, a - 1, h', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h - 1 >= h' ]
		(?, 5)     f73(a, b, c, e) -> f53(a - 1, b, h', h - 1) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ h >= c + 1 /\ h' + 1 >= h /\ h >= 1 ]
		(?, 3)     f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 2)     f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 1)     f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)     f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)     f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)     f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)     f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)     f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)     f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)     f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)     f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)     f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)     f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)     f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)     f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)     f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)     f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(4, 1)     f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(4, 1)     f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(2, 1)     f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(2, 1)     f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(1, 1)     f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)     f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
	start location:	f2
	leaf cost:	2

A polynomial rank function with
	Pol(f73) = 1
	Pol(f13) = 0
	Pol(f71) = 1
	Pol(f61) = 1
	Pol(f53) = 1
	Pol(f33) = 1
	Pol(f63) = 1
	Pol(f43) = 1
	Pol(f6) = 1
	Pol(f4) = 1
	Pol(f23) = 1
	Pol(f2) = 1
orients all transitions weakly and the transition
	f73(a, b, c, e) -> f13(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 /\ 2*h'' >= 0 /\ h''' >= h'' /\ h''' - h'' >= 0 /\ h''' + h'' >= 0 /\ h''' >= 0 /\ a + h''' - 1 >= 0 /\ h''' >= h'' + 1 ]
strictly and produces the following problem:
24:	T:
		(1, 10)    f73(a, b, c, e) -> f13(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 /\ 2*h'' >= 0 /\ h''' >= h'' /\ h''' - h'' >= 0 /\ h''' + h'' >= 0 /\ h''' >= 0 /\ a + h''' - 1 >= 0 /\ h''' >= h'' + 1 ]
		(?, 8)     f73(a, b, c, e) -> f71(a - 1, a - 1, h'', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' ]
		(?, 9)     f73(a, b, c, e) -> f73(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' /\ 2*h'' >= 0 /\ h''' >= h'' ]
		(?, 9)     f73(a, b, c, e) -> f73(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 /\ 2*h'' >= 0 /\ h''' >= h'' ]
		(?, 6)     f73(a, b, c, e) -> f61(a - 1, a - 1, h', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h - 1 >= h' ]
		(?, 5)     f73(a, b, c, e) -> f53(a - 1, b, h', h - 1) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ h >= c + 1 /\ h' + 1 >= h /\ h >= 1 ]
		(?, 3)     f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 2)     f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 1)     f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)     f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)     f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)     f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)     f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)     f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)     f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)     f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)     f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)     f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)     f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)     f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)     f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)     f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)     f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(4, 1)     f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(4, 1)     f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(2, 1)     f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(2, 1)     f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(1, 1)     f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)     f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
	start location:	f2
	leaf cost:	2

By chaining the transition f73(a, b, c, e) -> f71(a - 1, a - 1, h'', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' ] with all transitions in problem 24, the following new transition is obtained:
	f73(a, b, c, e) -> f13(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' /\ 2*h'' >= 0 /\ h''' >= h'' /\ h''' - h'' >= 0 /\ h''' + h'' >= 0 /\ h''' >= 0 /\ a + h''' - 1 >= 0 /\ h''' >= h'' + 1 ]
We thus obtain the following problem:
25:	T:
		(?, 10)    f73(a, b, c, e) -> f13(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' /\ 2*h'' >= 0 /\ h''' >= h'' /\ h''' - h'' >= 0 /\ h''' + h'' >= 0 /\ h''' >= 0 /\ a + h''' - 1 >= 0 /\ h''' >= h'' + 1 ]
		(1, 10)    f73(a, b, c, e) -> f13(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 /\ 2*h'' >= 0 /\ h''' >= h'' /\ h''' - h'' >= 0 /\ h''' + h'' >= 0 /\ h''' >= 0 /\ a + h''' - 1 >= 0 /\ h''' >= h'' + 1 ]
		(?, 9)     f73(a, b, c, e) -> f73(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' /\ 2*h'' >= 0 /\ h''' >= h'' ]
		(?, 9)     f73(a, b, c, e) -> f73(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 /\ 2*h'' >= 0 /\ h''' >= h'' ]
		(?, 6)     f73(a, b, c, e) -> f61(a - 1, a - 1, h', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h - 1 >= h' ]
		(?, 5)     f73(a, b, c, e) -> f53(a - 1, b, h', h - 1) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ h >= c + 1 /\ h' + 1 >= h /\ h >= 1 ]
		(?, 3)     f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 2)     f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 1)     f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)     f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)     f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)     f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)     f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)     f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)     f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)     f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)     f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)     f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)     f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)     f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)     f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)     f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)     f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(4, 1)     f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(4, 1)     f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(2, 1)     f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(2, 1)     f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(1, 1)     f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)     f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
	start location:	f2
	leaf cost:	2

A polynomial rank function with
	Pol(f73) = 1
	Pol(f13) = 0
	Pol(f61) = 1
	Pol(f53) = 1
	Pol(f33) = 1
	Pol(f71) = 1
	Pol(f63) = 1
	Pol(f43) = 1
	Pol(f6) = 1
	Pol(f4) = 1
	Pol(f23) = 1
	Pol(f2) = 1
orients all transitions weakly and the transition
	f73(a, b, c, e) -> f13(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' /\ 2*h'' >= 0 /\ h''' >= h'' /\ h''' - h'' >= 0 /\ h''' + h'' >= 0 /\ h''' >= 0 /\ a + h''' - 1 >= 0 /\ h''' >= h'' + 1 ]
strictly and produces the following problem:
26:	T:
		(1, 10)    f73(a, b, c, e) -> f13(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' /\ 2*h'' >= 0 /\ h''' >= h'' /\ h''' - h'' >= 0 /\ h''' + h'' >= 0 /\ h''' >= 0 /\ a + h''' - 1 >= 0 /\ h''' >= h'' + 1 ]
		(1, 10)    f73(a, b, c, e) -> f13(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ 0 >= a - 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 /\ 2*h'' >= 0 /\ h''' >= h'' /\ h''' - h'' >= 0 /\ h''' + h'' >= 0 /\ h''' >= 0 /\ a + h''' - 1 >= 0 /\ h''' >= h'' + 1 ]
		(?, 9)     f73(a, b, c, e) -> f73(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h' >= h'' /\ 2*h'' >= 0 /\ h''' >= h'' ]
		(?, 9)     f73(a, b, c, e) -> f73(a - 1, a - 1, h''', h'') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h' >= h /\ 0 >= 0 /\ 2*h' >= 0 /\ 2*a - 2 >= 0 /\ a - 1 >= 1 /\ h'' >= h' /\ h'' - h' >= 0 /\ h'' + h' >= 0 /\ h'' >= 0 /\ a + h'' - 1 >= 0 /\ h'' >= h' + 1 /\ 2*h'' >= 0 /\ h''' >= h'' ]
		(?, 6)     f73(a, b, c, e) -> f61(a - 1, a - 1, h', h') [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ c >= h /\ h' + 1 >= h /\ h >= 1 /\ h' - h + 1 >= 0 /\ h - 1 >= 0 /\ h' + h - 1 >= 0 /\ a + h - 2 >= 0 /\ h' >= 0 /\ a + h' - 1 >= 0 /\ h - 1 >= h' ]
		(?, 5)     f73(a, b, c, e) -> f53(a - 1, b, h', h - 1) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 /\ h >= c /\ b >= 1 /\ a >= 1 /\ h - c >= 0 /\ a - 1 >= 0 /\ h >= c + 1 /\ h' + 1 >= h /\ h >= 1 ]
		(?, 3)     f73(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(1, 2)     f71(a, b, c, e) -> f13(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e /\ h - e >= 0 /\ h + e >= 0 /\ h >= 0 /\ b + h >= 0 /\ a + h >= 0 /\ h >= e + 1 ]
		(?, 1)     f71(a, b, c, e) -> f73(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)     f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)     f63(a, b, c, e) -> f71(a, b, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)     f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ b >= 1 /\ h >= e ]
		(?, 1)     f61(a, b, c, e) -> f63(a, b, h, e) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ -c + e >= 0 /\ b + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c >= 0 /\ a - b >= 0 /\ b >= 0 /\ a + b >= 0 /\ -a + b >= 0 /\ a >= 0 /\ 0 >= b /\ h >= e ]
		(?, 1)     f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)     f53(a, b, c, e) -> f61(a, a, c, c) [ c - e >= 0 /\ e >= 0 /\ c + e >= 0 /\ a + e >= 0 /\ c >= 0 /\ a + c >= 0 /\ a >= 0 /\ e >= c ]
		(?, 1)     f43(a, b, c, e) -> f6(a, b, c, e) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)     f43(a, b, c, e) -> f6(a, b, c, c) [ -e >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ a >= 0 /\ c = e ]
		(?, 1)     f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ b >= 1 ]
		(?, 1)     f6(a, b, c, e) -> f53(a, b, h, c - 1) [ c - e >= 0 /\ a >= 0 /\ h + 1 >= c /\ c >= 1 /\ 0 >= b ]
		(?, 1)     f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ b >= 1 ]
		(?, 1)     f6(a, b, c, e) -> f43(a, b, h, c) [ c - e >= 0 /\ a >= 0 /\ h >= c /\ 0 >= c /\ 0 >= b ]
		(?, 1)     f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ c >= e + 1 ]
		(?, 1)     f33(a, b, c, e) -> f6(a, b, c, e) [ c - e >= 0 /\ a >= 0 /\ e >= c ]
		(4, 1)     f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ b >= 1 /\ a >= 1 ]
		(4, 1)     f4(a, b, c, e) -> f33(a - 1, b, h, c) [ c - e >= 0 /\ h >= c /\ 0 >= b /\ a >= 1 ]
		(2, 1)     f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ c >= e + 1 ]
		(2, 1)     f23(a, b, c, e) -> f4(a, b, c, e) [ -e + 1 >= 0 /\ c - e >= 0 /\ a - e >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ a + e - 2 >= 0 /\ c - 1 >= 0 /\ a + c - 2 >= 0 /\ a - 1 >= 0 /\ e >= c ]
		(1, 1)     f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ i >= 1 ]
		(1, 1)     f2(a, b, c, e) -> f23(g, i, h, 1) [ g >= 1 /\ h >= 1 /\ 0 >= i ]
	start location:	f2
	leaf cost:	2

Complexity upper bound ?

Time: 6.323 sec (SMT: 5.162 sec)