MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f13(a, b, c, d, e, f, g, h, i, j) -> f31(l, k, c - 1, c - 1, e, f, g, h, i, j) [ 0 >= k + 1 ]
		(?, 1)    f13(a, b, c, d, e, f, g, h, i, j) -> f31(l, k, c - 1, c - 1, e, f, g, h, i, j) [ k >= 1 ]
		(?, 1)    f13(a, b, c, d, e, f, g, h, i, j) -> f29(l, 0, d - 2, d - 1, e, f, g, h, i, j)
		(?, 1)    f19(a, b, c, d, e, f, g, h, i, j) -> f31(l, k, c - 1, c - 1, e, f, g, h, i, j) [ 0 >= k + 1 ]
		(?, 1)    f19(a, b, c, d, e, f, g, h, i, j) -> f31(l, k, c - 1, c - 1, e, f, g, h, i, j) [ k >= 1 ]
		(?, 1)    f19(a, b, c, d, e, f, g, h, i, j) -> f29(l, 0, d - 2, d - 1, e, f, g, h, i, j)
		(1, 1)    f8(a, b, c, d, e, f, g, h, i, j) -> f27(a, b, c, d, 0, 0, g, h, i, j)
		(?, 1)    f27(a, b, c, d, e, f, g, h, i, j) -> f27(l, 0, d - 2, d - 1, 0, f, 0, h, i, j) [ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 0 ]
		(?, 1)    f27(a, b, c, d, e, f, g, h, i, j) -> f27(l, k, c - 1, c - 1, 0, f, 0, h, i, j) [ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(a, b, c, d, e, f, g, h, i, j) -> f27(l, k, c - 1, c - 1, 0, f, 0, h, i, j) [ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(a, b, c, d, e, f, g, h, i, j) -> f30(l, k, c - 1, c - 1, 1, f, m, c, d, j) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ 0 >= k + 1 /\ 0 >= m + 1 /\ e = 0 ]
		(?, 1)    f27(a, b, c, d, e, f, g, h, i, j) -> f30(l, k, c - 1, c - 1, 1, f, m, c, d, j) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ 0 >= k + 1 /\ m >= 1 /\ e = 0 ]
		(?, 1)    f27(a, b, c, d, e, f, g, h, i, j) -> f30(l, k, c - 1, c - 1, 1, f, m, c, d, j) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ k >= 1 /\ 0 >= m + 1 /\ e = 0 ]
		(?, 1)    f27(a, b, c, d, e, f, g, h, i, j) -> f30(l, k, c - 1, c - 1, 1, f, m, c, d, j) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ k >= 1 /\ m >= 1 /\ e = 0 ]
		(?, 1)    f27(a, b, c, d, e, f, g, h, i, j) -> f28(l, 0, d - 2, d - 1, 1, f, k, c, d, j) [ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(a, b, c, d, e, f, g, h, i, j) -> f28(l, 0, d - 2, d - 1, 1, f, k, c, d, j) [ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(a, b, c, d, e, f, g, h, i, j) -> f9(a, b, c, d, e, f, g, h, i, l) [ 0 >= c ]
		(?, 1)    f27(a, b, c, d, e, f, g, h, i, j) -> f9(a, b, c, d, e, f, g, h, i, l) [ c >= 1 /\ 0 >= d ]
		(?, 1)    f28(a, b, c, d, e, f, g, h, i, j) -> f300(a, b, c, d, 1, 1, g, h, i, j) [ d >= i /\ c >= h /\ c + d >= h + i /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f28(a, b, c, d, e, f, g, h, i, j) -> f30(l, k, c - 1, c - 1, 1, f, g, h, i, j) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(a, b, c, d, e, f, g, h, i, j) -> f30(l, k, c - 1, c - 1, 1, f, g, h, i, j) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(a, b, c, d, e, f, g, h, i, j) -> f28(l, 0, d - 2, d - 1, 1, f, g, h, i, j) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f28(a, b, c, d, e, f, g, h, i, j) -> f30(l, k, c - 1, c - 1, 1, f, g, h, i, j) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(a, b, c, d, e, f, g, h, i, j) -> f30(l, k, c - 1, c - 1, 1, f, g, h, i, j) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(a, b, c, d, e, f, g, h, i, j) -> f28(l, 0, d - 2, d - 1, 1, f, g, h, i, j) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f28(a, b, c, d, e, f, g, h, i, j) -> f9(a, b, c, d, e, f, g, h, i, l) [ 0 >= c ]
		(?, 1)    f28(a, b, c, d, e, f, g, h, i, j) -> f9(a, b, c, d, e, f, g, h, i, l) [ c >= 1 /\ 0 >= d ]
		(?, 1)    f29(a, b, c, d, e, f, g, h, i, j) -> f300(a, b, c, d, 1, 1, g, h, i, j) [ d >= i /\ c >= h /\ c + d >= h + i /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f29(a, b, c, d, e, f, g, h, i, j) -> f31(l, k, c - 1, c - 1, 1, f, g, h, i, j) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f29(a, b, c, d, e, f, g, h, i, j) -> f31(l, k, c - 1, c - 1, 1, f, g, h, i, j) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f29(a, b, c, d, e, f, g, h, i, j) -> f29(l, 0, d - 2, d - 1, 1, f, g, h, i, j) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f29(a, b, c, d, e, f, g, h, i, j) -> f31(l, k, c - 1, c - 1, 1, f, g, h, i, j) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f29(a, b, c, d, e, f, g, h, i, j) -> f31(l, k, c - 1, c - 1, 1, f, g, h, i, j) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f29(a, b, c, d, e, f, g, h, i, j) -> f29(l, 0, d - 2, d - 1, 1, f, g, h, i, j) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f29(a, b, c, d, e, f, g, h, i, j) -> f9(a, b, c, d, e, f, g, h, i, l) [ 0 >= c ]
		(?, 1)    f29(a, b, c, d, e, f, g, h, i, j) -> f9(a, b, c, d, e, f, g, h, i, l) [ c >= 1 /\ 0 >= d ]
		(?, 1)    f30(a, b, c, d, e, f, g, h, i, j) -> f300(a, b, c, d, 1, 1, g, h, i, j) [ d >= i /\ c >= h /\ c + d >= h + i /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f30(a, b, c, d, e, f, g, h, i, j) -> f30(l, k, c - 1, c - 1, 1, f, g, h, i, j) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(a, b, c, d, e, f, g, h, i, j) -> f30(l, k, c - 1, c - 1, 1, f, g, h, i, j) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(a, b, c, d, e, f, g, h, i, j) -> f28(l, 0, d - 2, d - 1, 1, f, g, h, i, j) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f30(a, b, c, d, e, f, g, h, i, j) -> f30(l, k, c - 1, c - 1, 1, f, g, h, i, j) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(a, b, c, d, e, f, g, h, i, j) -> f30(l, k, c - 1, c - 1, 1, f, g, h, i, j) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(a, b, c, d, e, f, g, h, i, j) -> f28(l, 0, d - 2, d - 1, 1, f, g, h, i, j) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f30(a, b, c, d, e, f, g, h, i, j) -> f9(a, b, c, d, e, f, g, h, i, l) [ 0 >= c ]
		(?, 1)    f31(a, b, c, d, e, f, g, h, i, j) -> f300(a, b, c, d, 1, 1, g, h, i, j) [ d >= i /\ c >= h /\ c + d >= h + i /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f31(a, b, c, d, e, f, g, h, i, j) -> f31(l, k, c - 1, c - 1, 1, f, g, h, i, j) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f31(a, b, c, d, e, f, g, h, i, j) -> f31(l, k, c - 1, c - 1, 1, f, g, h, i, j) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f31(a, b, c, d, e, f, g, h, i, j) -> f29(l, 0, d - 2, d - 1, 1, f, g, h, i, j) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f31(a, b, c, d, e, f, g, h, i, j) -> f31(l, k, c - 1, c - 1, 1, f, g, h, i, j) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f31(a, b, c, d, e, f, g, h, i, j) -> f31(l, k, c - 1, c - 1, 1, f, g, h, i, j) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f31(a, b, c, d, e, f, g, h, i, j) -> f29(l, 0, d - 2, d - 1, 1, f, g, h, i, j) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f31(a, b, c, d, e, f, g, h, i, j) -> f9(a, b, c, d, e, f, g, h, i, l) [ 0 >= c ]
	start location:	f8
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [c, d, e, h, i].
We thus obtain the following problem:
2:	T:
		(?, 1)    f31(c, d, e, h, i) -> f9(c, d, e, h, i) [ 0 >= c ]
		(?, 1)    f31(c, d, e, h, i) -> f29(d - 2, d - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f31(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f31(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f31(c, d, e, h, i) -> f29(d - 2, d - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f31(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f31(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f31(c, d, e, h, i) -> f300(c, d, 1, h, i) [ d >= i /\ c >= h /\ c + d >= h + i /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f9(c, d, e, h, i) [ 0 >= c ]
		(?, 1)    f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f300(c, d, 1, h, i) [ d >= i /\ c >= h /\ c + d >= h + i /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f29(c, d, e, h, i) -> f9(c, d, e, h, i) [ c >= 1 /\ 0 >= d ]
		(?, 1)    f29(c, d, e, h, i) -> f9(c, d, e, h, i) [ 0 >= c ]
		(?, 1)    f29(c, d, e, h, i) -> f29(d - 2, d - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f29(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f29(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f29(c, d, e, h, i) -> f29(d - 2, d - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f29(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f29(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f29(c, d, e, h, i) -> f300(c, d, 1, h, i) [ d >= i /\ c >= h /\ c + d >= h + i /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f9(c, d, e, h, i) [ c >= 1 /\ 0 >= d ]
		(?, 1)    f28(c, d, e, h, i) -> f9(c, d, e, h, i) [ 0 >= c ]
		(?, 1)    f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f300(c, d, 1, h, i) [ d >= i /\ c >= h /\ c + d >= h + i /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f27(c, d, e, h, i) -> f9(c, d, e, h, i) [ c >= 1 /\ 0 >= d ]
		(?, 1)    f27(c, d, e, h, i) -> f9(c, d, e, h, i) [ 0 >= c ]
		(?, 1)    f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ k >= 1 /\ m >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ k >= 1 /\ 0 >= m + 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ 0 >= k + 1 /\ m >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ 0 >= k + 1 /\ 0 >= m + 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f27(d - 2, d - 1, 0, h, i) [ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 0 ]
		(1, 1)    f8(c, d, e, h, i) -> f27(c, d, 0, h, i)
		(?, 1)    f19(c, d, e, h, i) -> f29(d - 2, d - 1, e, h, i)
		(?, 1)    f19(c, d, e, h, i) -> f31(c - 1, c - 1, e, h, i) [ k >= 1 ]
		(?, 1)    f19(c, d, e, h, i) -> f31(c - 1, c - 1, e, h, i) [ 0 >= k + 1 ]
		(?, 1)    f13(c, d, e, h, i) -> f29(d - 2, d - 1, e, h, i)
		(?, 1)    f13(c, d, e, h, i) -> f31(c - 1, c - 1, e, h, i) [ k >= 1 ]
		(?, 1)    f13(c, d, e, h, i) -> f31(c - 1, c - 1, e, h, i) [ 0 >= k + 1 ]
	start location:	f8
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(?, 1)    f31(c, d, e, h, i) -> f29(d - 2, d - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f31(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f31(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f31(c, d, e, h, i) -> f29(d - 2, d - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f31(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f31(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f29(c, d, e, h, i) -> f29(d - 2, d - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f29(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f29(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f29(c, d, e, h, i) -> f29(d - 2, d - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f29(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f29(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ k >= 1 /\ m >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ k >= 1 /\ 0 >= m + 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ 0 >= k + 1 /\ m >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ 0 >= k + 1 /\ 0 >= m + 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f27(d - 2, d - 1, 0, h, i) [ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 0 ]
		(1, 1)    f8(c, d, e, h, i) -> f27(c, d, 0, h, i)
		(?, 1)    f19(c, d, e, h, i) -> f29(d - 2, d - 1, e, h, i)
		(?, 1)    f19(c, d, e, h, i) -> f31(c - 1, c - 1, e, h, i) [ k >= 1 ]
		(?, 1)    f19(c, d, e, h, i) -> f31(c - 1, c - 1, e, h, i) [ 0 >= k + 1 ]
		(?, 1)    f13(c, d, e, h, i) -> f29(d - 2, d - 1, e, h, i)
		(?, 1)    f13(c, d, e, h, i) -> f31(c - 1, c - 1, e, h, i) [ k >= 1 ]
		(?, 1)    f13(c, d, e, h, i) -> f31(c - 1, c - 1, e, h, i) [ 0 >= k + 1 ]
	start location:	f8
	leaf cost:	12

Testing for reachability in the complexity graph removes the following transitions from problem 3:
	f31(c, d, e, h, i) -> f29(d - 2, d - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
	f31(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
	f31(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
	f31(c, d, e, h, i) -> f29(d - 2, d - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
	f31(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
	f31(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
	f29(c, d, e, h, i) -> f29(d - 2, d - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
	f29(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
	f29(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
	f29(c, d, e, h, i) -> f29(d - 2, d - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
	f29(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
	f29(c, d, e, h, i) -> f31(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
	f19(c, d, e, h, i) -> f29(d - 2, d - 1, e, h, i)
	f19(c, d, e, h, i) -> f31(c - 1, c - 1, e, h, i) [ k >= 1 ]
	f19(c, d, e, h, i) -> f31(c - 1, c - 1, e, h, i) [ 0 >= k + 1 ]
	f13(c, d, e, h, i) -> f29(d - 2, d - 1, e, h, i)
	f13(c, d, e, h, i) -> f31(c - 1, c - 1, e, h, i) [ k >= 1 ]
	f13(c, d, e, h, i) -> f31(c - 1, c - 1, e, h, i) [ 0 >= k + 1 ]
We thus obtain the following problem:
4:	T:
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f27(c, d, e, h, i) -> f27(d - 2, d - 1, 0, h, i) [ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ 0 >= k + 1 /\ 0 >= m + 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ 0 >= k + 1 /\ m >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ k >= 1 /\ 0 >= m + 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ k >= 1 /\ m >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 0 ]
		(1, 1)    f8(c, d, e, h, i) -> f27(c, d, 0, h, i)
	start location:	f8
	leaf cost:	12

A polynomial rank function with
	Pol(f30) = 0
	Pol(f28) = 0
	Pol(f27) = 1
	Pol(f8) = 1
orients all transitions weakly and the transitions
	f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ k >= 1 /\ m >= 1 /\ e = 0 ]
	f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ k >= 1 /\ 0 >= m + 1 /\ e = 0 ]
	f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ 0 >= k + 1 /\ m >= 1 /\ e = 0 ]
	f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ 0 >= k + 1 /\ 0 >= m + 1 /\ e = 0 ]
	f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 0 ]
	f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 0 ]
strictly and produces the following problem:
5:	T:
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f27(c, d, e, h, i) -> f27(d - 2, d - 1, 0, h, i) [ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 0 ]
		(1, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ 0 >= k + 1 /\ 0 >= m + 1 /\ e = 0 ]
		(1, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ 0 >= k + 1 /\ m >= 1 /\ e = 0 ]
		(1, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ k >= 1 /\ 0 >= m + 1 /\ e = 0 ]
		(1, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ k >= 1 /\ m >= 1 /\ e = 0 ]
		(1, 1)    f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 0 ]
		(1, 1)    f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 0 ]
		(1, 1)    f8(c, d, e, h, i) -> f27(c, d, 0, h, i)
	start location:	f8
	leaf cost:	12

Applied AI with 'oct' on problem 5 to obtain the following invariants:
  For symbol f27: -X_3 >= 0 /\ X_3 >= 0
  For symbol f28: X_5 - 1 >= 0 /\ X_4 + X_5 - 2 >= 0 /\ X_3 + X_5 - 2 >= 0 /\ -X_3 + X_5 >= 0 /\ X_2 + X_5 - 1 >= 0 /\ X_1 + X_5 >= 0 /\ X_4 - 1 >= 0 /\ X_3 + X_4 - 2 >= 0 /\ -X_3 + X_4 >= 0 /\ X_2 + X_4 - 1 >= 0 /\ X_1 + X_4 >= 0 /\ -X_3 + 1 >= 0 /\ X_2 - X_3 + 1 >= 0 /\ X_1 - X_3 + 2 >= 0 /\ X_3 - 1 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 >= 0 /\ X_1 - X_2 + 1 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 + 1 >= 0 /\ -X_1 + X_2 - 1 >= 0 /\ X_1 + 1 >= 0
  For symbol f30: X_5 - 1 >= 0 /\ X_4 + X_5 - 2 >= 0 /\ X_3 + X_5 - 2 >= 0 /\ -X_3 + X_5 >= 0 /\ X_2 + X_5 - 1 >= 0 /\ X_1 + X_5 - 1 >= 0 /\ X_4 - 1 >= 0 /\ X_3 + X_4 - 2 >= 0 /\ -X_3 + X_4 >= 0 /\ X_2 + X_4 - 1 >= 0 /\ X_1 + X_4 - 1 >= 0 /\ -X_3 + 1 >= 0 /\ X_2 - X_3 + 1 >= 0 /\ X_1 - X_3 + 1 >= 0 /\ X_3 - 1 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 - 1 >= 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:
6:	T:
		(1, 1)    f8(c, d, e, h, i) -> f27(c, d, 0, h, i)
		(1, 1)    f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 0 ]
		(1, 1)    f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 0 ]
		(1, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ k >= 1 /\ m >= 1 /\ e = 0 ]
		(1, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ k >= 1 /\ 0 >= m + 1 /\ e = 0 ]
		(1, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ 0 >= k + 1 /\ m >= 1 /\ e = 0 ]
		(1, 1)    f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ 0 >= k + 1 /\ 0 >= m + 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)    f27(c, d, e, h, i) -> f27(d - 2, d - 1, 0, h, i) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 0 ]
		(?, 1)    f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(?, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
	start location:	f8
	leaf cost:	12

A polynomial rank function with
	Pol(f30) = V_1 + 2
	Pol(f28) = V_2 + 1
	Pol(f27) = V_4 + V_5 + 2
and size complexities
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-0) = c + d
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-1) = c + d
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-2) = 1
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-3) = c + d
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-4) = c + d
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-0) = c + d
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-1) = c + d
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-2) = 1
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-3) = c + d
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-4) = c + d
	S("f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-0) = c + d
	S("f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-1) = c + d
	S("f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-2) = 1
	S("f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-3) = c + d
	S("f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-4) = c + d
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-0) = c + d
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-1) = c + d
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-2) = 1
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-3) = c + d
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-4) = c + d
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-0) = c + d
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-1) = c + d
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-2) = 1
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-3) = c + d
	S("f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-4) = c + d
	S("f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-0) = c + d
	S("f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-1) = c + d
	S("f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-2) = 1
	S("f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-3) = c + d
	S("f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i - 1 >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h - 1 >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 1 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e - 1 >= 0 /\\ c - d >= 0 /\\ d >= 0 /\\ c + d >= 0 /\\ -c + d >= 0 /\\ c >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-4) = c + d
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-0) = c + d
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-1) = c + d
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-2) = 1
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-3) = c + d
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-4) = c + d
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-0) = c + d
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-1) = c + d
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-2) = 1
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-3) = c + d
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-4) = c + d
	S("f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-0) = c + d
	S("f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-1) = c + d
	S("f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-2) = 1
	S("f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-3) = c + d
	S("f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ h >= c + 1 /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-4) = c + d
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-0) = c + d
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-1) = c + d
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-2) = 1
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-3) = c + d
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-4) = c + d
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-0) = c + d
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-1) = c + d
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-2) = 1
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-3) = c + d
	S("f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 1 ]", 0-4) = c + d
	S("f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-0) = c + d
	S("f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-1) = c + d
	S("f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-2) = 1
	S("f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-3) = c + d
	S("f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\\ h + i - 2 >= 0 /\\ e + i - 2 >= 0 /\\ -e + i >= 0 /\\ d + i - 1 >= 0 /\\ c + i >= 0 /\\ h - 1 >= 0 /\\ e + h - 2 >= 0 /\\ -e + h >= 0 /\\ d + h - 1 >= 0 /\\ c + h >= 0 /\\ -e + 1 >= 0 /\\ d - e + 1 >= 0 /\\ c - e + 2 >= 0 /\\ e - 1 >= 0 /\\ d + e - 1 >= 0 /\\ c + e >= 0 /\\ c - d + 1 >= 0 /\\ d >= 0 /\\ c + d + 1 >= 0 /\\ -c + d - 1 >= 0 /\\ c + 1 >= 0 /\\ i >= d + 1 /\\ c >= h /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 1 ]", 0-4) = c + d
	S("f27(c, d, e, h, i) -> f27(d - 2, d - 1, 0, h, i) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 0 ]", 0-0) = c + d
	S("f27(c, d, e, h, i) -> f27(d - 2, d - 1, 0, h, i) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 0 ]", 0-1) = c + d
	S("f27(c, d, e, h, i) -> f27(d - 2, d - 1, 0, h, i) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 0 ]", 0-2) = 0
	S("f27(c, d, e, h, i) -> f27(d - 2, d - 1, 0, h, i) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 0 ]", 0-3) = h
	S("f27(c, d, e, h, i) -> f27(d - 2, d - 1, 0, h, i) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c + d >= 1 /\\ c >= 1 /\\ e = 0 ]", 0-4) = i
	S("f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-0) = c + d
	S("f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-1) = c + d
	S("f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-2) = 0
	S("f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-3) = h
	S("f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-4) = i
	S("f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-0) = c + d
	S("f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-1) = c + d
	S("f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-2) = 0
	S("f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-3) = h
	S("f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-4) = i
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ 0 >= k + 1 /\\ 0 >= m + 1 /\\ e = 0 ]", 0-0) = c + d
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ 0 >= k + 1 /\\ 0 >= m + 1 /\\ e = 0 ]", 0-1) = c + d
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ 0 >= k + 1 /\\ 0 >= m + 1 /\\ e = 0 ]", 0-2) = 1
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ 0 >= k + 1 /\\ 0 >= m + 1 /\\ e = 0 ]", 0-3) = c + d
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ 0 >= k + 1 /\\ 0 >= m + 1 /\\ e = 0 ]", 0-4) = c + d
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ 0 >= k + 1 /\\ m >= 1 /\\ e = 0 ]", 0-0) = c + d
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ 0 >= k + 1 /\\ m >= 1 /\\ e = 0 ]", 0-1) = c + d
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ 0 >= k + 1 /\\ m >= 1 /\\ e = 0 ]", 0-2) = 1
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ 0 >= k + 1 /\\ m >= 1 /\\ e = 0 ]", 0-3) = c + d
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ 0 >= k + 1 /\\ m >= 1 /\\ e = 0 ]", 0-4) = c + d
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ k >= 1 /\\ 0 >= m + 1 /\\ e = 0 ]", 0-0) = c + d
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ k >= 1 /\\ 0 >= m + 1 /\\ e = 0 ]", 0-1) = c + d
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ k >= 1 /\\ 0 >= m + 1 /\\ e = 0 ]", 0-2) = 1
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ k >= 1 /\\ 0 >= m + 1 /\\ e = 0 ]", 0-3) = c + d
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ k >= 1 /\\ 0 >= m + 1 /\\ e = 0 ]", 0-4) = c + d
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ k >= 1 /\\ m >= 1 /\\ e = 0 ]", 0-0) = c + d
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ k >= 1 /\\ m >= 1 /\\ e = 0 ]", 0-1) = c + d
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ k >= 1 /\\ m >= 1 /\\ e = 0 ]", 0-2) = 1
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ k >= 1 /\\ m >= 1 /\\ e = 0 ]", 0-3) = c + d
	S("f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ c + d >= 1 /\\ k >= 1 /\\ m >= 1 /\\ e = 0 ]", 0-4) = c + d
	S("f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-0) = c + d
	S("f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-1) = c + d
	S("f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-2) = 1
	S("f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-3) = c + d
	S("f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ 0 >= k + 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-4) = c + d
	S("f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-0) = c + d
	S("f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-1) = c + d
	S("f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-2) = 1
	S("f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-3) = c + d
	S("f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ -e >= 0 /\\ e >= 0 /\\ d >= 1 /\\ c >= 1 /\\ k >= 1 /\\ c + d >= 1 /\\ e = 0 ]", 0-4) = c + d
	S("f8(c, d, e, h, i) -> f27(c, d, 0, h, i)", 0-0) = c
	S("f8(c, d, e, h, i) -> f27(c, d, 0, h, i)", 0-1) = d
	S("f8(c, d, e, h, i) -> f27(c, d, 0, h, i)", 0-2) = 0
	S("f8(c, d, e, h, i) -> f27(c, d, 0, h, i)", 0-3) = h
	S("f8(c, d, e, h, i) -> f27(c, d, 0, h, i)", 0-4) = i
orients the transitions
	f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
	f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
	f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
	f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
	f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
	f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
	f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
	f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
	f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
	f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
	f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
	f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
	f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 0 ]
	f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 0 ]
	f27(c, d, e, h, i) -> f27(d - 2, d - 1, 0, h, i) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 0 ]
weakly and the transitions
	f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
	f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
	f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
	f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
	f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
	f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
	f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
	f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
	f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
	f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
	f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
	f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
strictly and produces the following problem:
7:	T:
		(1, 1)                         f8(c, d, e, h, i) -> f27(c, d, 0, h, i)
		(1, 1)                         f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 0 ]
		(1, 1)                         f27(c, d, e, h, i) -> f28(d - 2, d - 1, 1, c, d) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 0 ]
		(1, 1)                         f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ k >= 1 /\ m >= 1 /\ e = 0 ]
		(1, 1)                         f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ k >= 1 /\ 0 >= m + 1 /\ e = 0 ]
		(1, 1)                         f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ 0 >= k + 1 /\ m >= 1 /\ e = 0 ]
		(1, 1)                         f27(c, d, e, h, i) -> f30(c - 1, c - 1, 1, c, d) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ c + d >= 1 /\ 0 >= k + 1 /\ 0 >= m + 1 /\ e = 0 ]
		(?, 1)                         f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)                         f27(c, d, e, h, i) -> f27(c - 1, c - 1, 0, h, i) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 0 ]
		(?, 1)                         f27(c, d, e, h, i) -> f27(d - 2, d - 1, 0, h, i) [ -e >= 0 /\ e >= 0 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 0 ]
		(6*c + 6*d + h + i + 12, 1)    f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(6*c + 6*d + h + i + 12, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(6*c + 6*d + h + i + 12, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(6*c + 6*d + h + i + 12, 1)    f28(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(6*c + 6*d + h + i + 12, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(6*c + 6*d + h + i + 12, 1)    f28(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 2 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e >= 0 /\ c - d + 1 >= 0 /\ d >= 0 /\ c + d + 1 >= 0 /\ -c + d - 1 >= 0 /\ c + 1 >= 0 /\ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(6*c + 6*d + h + i + 12, 1)    f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ h >= c + 1 /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(6*c + 6*d + h + i + 12, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(6*c + 6*d + h + i + 12, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ h >= c + 1 /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
		(6*c + 6*d + h + i + 12, 1)    f30(c, d, e, h, i) -> f28(d - 2, d - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c + d >= 1 /\ c >= 1 /\ e = 1 ]
		(6*c + 6*d + h + i + 12, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ k >= 1 /\ c + d >= 1 /\ e = 1 ]
		(6*c + 6*d + h + i + 12, 1)    f30(c, d, e, h, i) -> f30(c - 1, c - 1, 1, h, i) [ i - 1 >= 0 /\ h + i - 2 >= 0 /\ e + i - 2 >= 0 /\ -e + i >= 0 /\ d + i - 1 >= 0 /\ c + i - 1 >= 0 /\ h - 1 >= 0 /\ e + h - 2 >= 0 /\ -e + h >= 0 /\ d + h - 1 >= 0 /\ c + h - 1 >= 0 /\ -e + 1 >= 0 /\ d - e + 1 >= 0 /\ c - e + 1 >= 0 /\ e - 1 >= 0 /\ d + e - 1 >= 0 /\ c + e - 1 >= 0 /\ c - d >= 0 /\ d >= 0 /\ c + d >= 0 /\ -c + d >= 0 /\ c >= 0 /\ i >= d + 1 /\ c >= h /\ d >= 1 /\ c >= 1 /\ 0 >= k + 1 /\ c + d >= 1 /\ e = 1 ]
	start location:	f8
	leaf cost:	12

Complexity upper bound ?

Time: 6.277 sec (SMT: 5.726 sec)