MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f12(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) -> f16(a, 1, m1, o1, p1, g + 1, g, q1, g, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) [ a >= 0 /\ m1 >= 2 /\ n1 >= m1 /\ b = 1 ]
		(?, 1)    f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) -> f16(a, b, m1, o1, e, f, g, h, i, p1, q1, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) [ m1 >= 2 /\ i >= 0 ]
		(?, 1)    f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) -> f16(a, b + 1, m1, o1, p1, f, g - 1, h, i, j, k, m, m, q1, b + 1, g - 1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) [ b >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(?, 1)    f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) -> f1(a + 1, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, s, m1, s, o1, a, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) [ q >= a + 1 /\ a >= 0 ]
		(?, 1)    f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) -> f16(g, 0, m1, r, e, f, g, h, i, j, k, l, r, n, o, p, o1, p1, s1, n1, u, v, q1, t1, u1, r1, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) [ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)    f7(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) -> f8(a, b, m1, o1, e, f, g, h, i, j, k, l, 0, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, 0, o1, 0, o1, g1, g1, h1, i1, j1, k1, l1) [ m1 >= 2 /\ a1 >= 0 /\ b1 = 0 ]
		(?, 1)    f7(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) -> f10(a, b, m1, t1, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, u1, z, a1, n1, o1, p1, q1, r1, s1, h1, i1, j1, k1, l1) [ m1 >= 2 /\ a1 >= 0 /\ b1 = g1 ]
		(?, 1)    f8(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) -> f8(a, b, m1, o1, p1, f, g, h, i, j, k, l, 0, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, 0, o1, 0, o1, g1, g1, h1 - 1, h1 - 1, j1, k1, l1) [ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
		(?, 1)    f8(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) -> f10(a, b, m1, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, t1, z, a1, n1, o1, p1, q1, u1, s1, h1, i1, j1, k1, l1) [ m1 >= 2 /\ h1 >= 0 /\ b1 = g1 ]
		(?, 1)    f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) -> f8(a, h1 + 1, m1, d, e, f, g, h, 0, j, k, l, 0, n, o, p, q, r, s, t, u, v, w, x, y, z, h1, 0, d, 0, d, d, d, h1, i1, j1, k1, l1) [ o1 >= 2 /\ m1 >= 2 /\ m = 0 /\ i = 0 /\ b = 1 ]
		(?, 1)    f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) -> f8(a, h1 + 1, m1, d, e, f, g, h, i, j, k, l, 0, n, o, p, q, r, s, t, u, v, w, x, y, z, h1, 0, d, 0, d, d, d, h1, i1, j1, k1, l1) [ o1 >= 2 /\ m1 >= 2 /\ b >= 0 /\ g >= 0 /\ m = 0 ]
		(1, 1)    f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) -> f1(2, b, m1, d, e, f, g, h, i, j, k, l, m, n, o, p, m1, p1, q1, p1, u, v, p1, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, o1, n1, 2) [ m1 >= 2 ]
		(1, 1)    f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) -> f10(t1, b, m1, 0, e, f, g, h, i, j, k, l, 0, n, o, p, r1, y1, b2, a2, u, v, z1, c2, d2, z, a1, n1, o1, p1, q1, e2, s1, h1, i1, u1, k1, l1) [ 0 >= v1 /\ 0 >= w1 /\ 0 >= m1 /\ 0 >= x1 ]
		(1, 1)    f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) -> f10(t1, b, 1, s1, e, f, g, h, i, j, k, l, 0, n, o, p, r1, y1, b2, a2, u, v, z1, c2, d2, z, a1, q1, m1, o1, p1, e2, n1, h1, i1, u1, k1, l1) [ s = 0 ]
	start location:	f9
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, d, g, i, m, q, r, s, a1, b1, g1, h1].
We thus obtain the following problem:
2:	T:
		(1, 1)    f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f10(t1, b, s1, g, i, 0, r1, y1, b2, a1, q1, n1, h1) [ s = 0 ]
		(1, 1)    f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f10(t1, b, 0, g, i, 0, r1, y1, b2, a1, n1, s1, h1) [ 0 >= v1 /\ 0 >= w1 /\ 0 >= m1 /\ 0 >= x1 ]
		(1, 1)    f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(?, 1)    f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, d, g, i, 0, q, r, s, h1, 0, d, h1) [ o1 >= 2 /\ m1 >= 2 /\ b >= 0 /\ g >= 0 /\ m = 0 ]
		(?, 1)    f13(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, d, g, 0, 0, q, r, s, h1, 0, d, h1) [ o1 >= 2 /\ m1 >= 2 /\ m = 0 /\ i = 0 /\ b = 1 ]
		(?, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f10(a, b, d, g, i, m, q, r, s, a1, n1, s1, h1) [ m1 >= 2 /\ h1 >= 0 /\ b1 = g1 ]
		(?, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
		(?, 1)    f7(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f10(a, b, t1, g, i, m, q, r, s, a1, n1, s1, h1) [ m1 >= 2 /\ a1 >= 0 /\ b1 = g1 ]
		(?, 1)    f7(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1) [ m1 >= 2 /\ a1 >= 0 /\ b1 = 0 ]
		(?, 1)    f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)    f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q >= a + 1 /\ a >= 0 ]
		(?, 1)    f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ b >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(?, 1)    f13(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b, o1, g, i, m, q, r, s, a1, b1, g1, h1) [ m1 >= 2 /\ i >= 0 ]
		(?, 1)    f12(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, 1, o1, g, g, m, q, r, s, a1, b1, g1, h1) [ a >= 0 /\ m1 >= 2 /\ n1 >= m1 /\ b = 1 ]
	start location:	f9
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(1, 1)    f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(?, 1)    f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, d, g, i, 0, q, r, s, h1, 0, d, h1) [ o1 >= 2 /\ m1 >= 2 /\ b >= 0 /\ g >= 0 /\ m = 0 ]
		(?, 1)    f13(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, d, g, 0, 0, q, r, s, h1, 0, d, h1) [ o1 >= 2 /\ m1 >= 2 /\ m = 0 /\ i = 0 /\ b = 1 ]
		(?, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
		(?, 1)    f7(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1) [ m1 >= 2 /\ a1 >= 0 /\ b1 = 0 ]
		(?, 1)    f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)    f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q >= a + 1 /\ a >= 0 ]
		(?, 1)    f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ b >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(?, 1)    f13(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b, o1, g, i, m, q, r, s, a1, b1, g1, h1) [ m1 >= 2 /\ i >= 0 ]
		(?, 1)    f12(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, 1, o1, g, g, m, q, r, s, a1, b1, g1, h1) [ a >= 0 /\ m1 >= 2 /\ n1 >= m1 /\ b = 1 ]
	start location:	f9
	leaf cost:	4

Testing for reachability in the complexity graph removes the following transitions from problem 3:
	f13(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, d, g, 0, 0, q, r, s, h1, 0, d, h1) [ o1 >= 2 /\ m1 >= 2 /\ m = 0 /\ i = 0 /\ b = 1 ]
	f7(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1) [ m1 >= 2 /\ a1 >= 0 /\ b1 = 0 ]
	f13(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b, o1, g, i, m, q, r, s, a1, b1, g1, h1) [ m1 >= 2 /\ i >= 0 ]
	f12(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, 1, o1, g, g, m, q, r, s, a1, b1, g1, h1) [ a >= 0 /\ m1 >= 2 /\ n1 >= m1 /\ b = 1 ]
We thus obtain the following problem:
4:	T:
		(?, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
		(?, 1)    f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ b >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(?, 1)    f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, d, g, i, 0, q, r, s, h1, 0, d, h1) [ o1 >= 2 /\ m1 >= 2 /\ b >= 0 /\ g >= 0 /\ m = 0 ]
		(?, 1)    f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q >= a + 1 /\ a >= 0 ]
		(?, 1)    f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(1, 1)    f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
	start location:	f9
	leaf cost:	4

A polynomial rank function with
	Pol(f8) = -2
	Pol(f16) = 1
	Pol(f1) = 2
	Pol(f9) = 2
orients all transitions weakly and the transitions
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, d, g, i, 0, q, r, s, h1, 0, d, h1) [ o1 >= 2 /\ m1 >= 2 /\ b >= 0 /\ g >= 0 /\ m = 0 ]
	f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
strictly and produces the following problem:
5:	T:
		(?, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
		(?, 1)    f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ b >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(2, 1)    f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, d, g, i, 0, q, r, s, h1, 0, d, h1) [ o1 >= 2 /\ m1 >= 2 /\ b >= 0 /\ g >= 0 /\ m = 0 ]
		(?, 1)    f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q >= a + 1 /\ a >= 0 ]
		(2, 1)    f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(1, 1)    f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
	start location:	f9
	leaf cost:	4

A polynomial rank function with
	Pol(f8) = V_13 + 1
	Pol(f16) = V_4 + V_13 + 1
	Pol(f1) = V_2 + V_4 + V_13 + 1
	Pol(f9) = V_2 + V_4 + V_13 + 1
orients all transitions weakly and the transition
	f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
strictly and produces the following problem:
6:	T:
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
		(?, 1)                 f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ b >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(2, 1)                 f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, d, g, i, 0, q, r, s, h1, 0, d, h1) [ o1 >= 2 /\ m1 >= 2 /\ b >= 0 /\ g >= 0 /\ m = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q >= a + 1 /\ a >= 0 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
	start location:	f9
	leaf cost:	4

A polynomial rank function with
	Pol(f8) = V_2 + V_4 - V_10
	Pol(f16) = V_4 + 1
	Pol(f1) = V_2 + V_4 + 1
	Pol(f9) = V_2 + V_4 + 1
orients all transitions weakly and the transition
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ b >= 0 /\ g >= 0 /\ m1 >= 2 ]
strictly and produces the following problem:
7:	T:
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ b >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(2, 1)                 f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, d, g, i, 0, q, r, s, h1, 0, d, h1) [ o1 >= 2 /\ m1 >= 2 /\ b >= 0 /\ g >= 0 /\ m = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q >= a + 1 /\ a >= 0 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
	start location:	f9
	leaf cost:	4

Applied AI with 'oct' on problem 7 to obtain the following invariants:
  For symbol f1: X_7 - 2 >= 0 /\ X_1 + X_7 - 4 >= 0 /\ -X_1 + X_7 >= 0 /\ X_1 - 2 >= 0
  For symbol f16: X_1 - X_4 >= 0 /\ X_2 + X_4 - 2 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 2 >= 0
  For symbol f8: -X_6 >= 0 /\ X_4 - X_6 >= 0 /\ X_11 - X_6 >= 0 /\ -X_11 - X_6 >= 0 /\ X_1 - X_6 - 2 >= 0 /\ X_6 >= 0 /\ X_4 + X_6 >= 0 /\ X_11 + X_6 >= 0 /\ -X_11 + X_6 >= 0 /\ X_1 + X_6 - 2 >= 0 /\ X_1 - X_4 >= 0 /\ X_4 >= 0 /\ X_11 + X_4 >= 0 /\ -X_11 + X_4 >= 0 /\ X_1 + X_4 - 2 >= 0 /\ X_10 - X_2 + 1 >= 0 /\ -X_13 + X_2 - 1 >= 0 /\ -X_10 + X_2 - 1 >= 0 /\ X_10 - X_13 >= 0 /\ -X_11 >= 0 /\ X_1 - X_11 - 2 >= 0 /\ X_11 >= 0 /\ X_1 + X_11 - 2 >= 0 /\ X_1 - 2 >= 0


This yielded the following problem:
8:	T:
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ]
		(2, 1)                 f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, d, g, i, 0, q, r, s, h1, 0, d, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ -m >= 0 /\ g - m >= 0 /\ b1 - m >= 0 /\ -b1 - m >= 0 /\ a - m - 2 >= 0 /\ m >= 0 /\ g + m >= 0 /\ b1 + m >= 0 /\ -b1 + m >= 0 /\ a + m - 2 >= 0 /\ a - g >= 0 /\ g >= 0 /\ b1 + g >= 0 /\ -b1 + g >= 0 /\ a + g - 2 >= 0 /\ a1 - b + 1 >= 0 /\ -h1 + b - 1 >= 0 /\ -a1 + b - 1 >= 0 /\ a1 - h1 >= 0 /\ -b1 >= 0 /\ a - b1 - 2 >= 0 /\ b1 >= 0 /\ a + b1 - 2 >= 0 /\ a - 2 >= 0 /\ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
	start location:	f9
	leaf cost:	4

By chaining the transition f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, d, g, i, 0, q, r, s, h1, 0, d, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 ] with all transitions in problem 8, the following new transition is obtained:
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 ]
We thus obtain the following problem:
9:	T:
		(2, 2)                 f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ -m >= 0 /\ g - m >= 0 /\ b1 - m >= 0 /\ -b1 - m >= 0 /\ a - m - 2 >= 0 /\ m >= 0 /\ g + m >= 0 /\ b1 + m >= 0 /\ -b1 + m >= 0 /\ a + m - 2 >= 0 /\ a - g >= 0 /\ g >= 0 /\ b1 + g >= 0 /\ -b1 + g >= 0 /\ a + g - 2 >= 0 /\ a1 - b + 1 >= 0 /\ -h1 + b - 1 >= 0 /\ -a1 + b - 1 >= 0 /\ a1 - h1 >= 0 /\ -b1 >= 0 /\ a - b1 - 2 >= 0 /\ b1 >= 0 /\ a + b1 - 2 >= 0 /\ a - 2 >= 0 /\ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
	start location:	f9
	leaf cost:	4

By chaining the transition f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 ] with all transitions in problem 9, the following new transition is obtained:
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 2) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 ]
We thus obtain the following problem:
10:	T:
		(2, 3)                 f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 2) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ -m >= 0 /\ g - m >= 0 /\ b1 - m >= 0 /\ -b1 - m >= 0 /\ a - m - 2 >= 0 /\ m >= 0 /\ g + m >= 0 /\ b1 + m >= 0 /\ -b1 + m >= 0 /\ a + m - 2 >= 0 /\ a - g >= 0 /\ g >= 0 /\ b1 + g >= 0 /\ -b1 + g >= 0 /\ a + g - 2 >= 0 /\ a1 - b + 1 >= 0 /\ -h1 + b - 1 >= 0 /\ -a1 + b - 1 >= 0 /\ a1 - h1 >= 0 /\ -b1 >= 0 /\ a - b1 - 2 >= 0 /\ b1 >= 0 /\ a + b1 - 2 >= 0 /\ a - 2 >= 0 /\ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
	start location:	f9
	leaf cost:	4

By chaining the transition f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 2) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 ] with all transitions in problem 10, the following new transition is obtained:
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 3) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 ]
We thus obtain the following problem:
11:	T:
		(2, 4)                 f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 3) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ -m >= 0 /\ g - m >= 0 /\ b1 - m >= 0 /\ -b1 - m >= 0 /\ a - m - 2 >= 0 /\ m >= 0 /\ g + m >= 0 /\ b1 + m >= 0 /\ -b1 + m >= 0 /\ a + m - 2 >= 0 /\ a - g >= 0 /\ g >= 0 /\ b1 + g >= 0 /\ -b1 + g >= 0 /\ a + g - 2 >= 0 /\ a1 - b + 1 >= 0 /\ -h1 + b - 1 >= 0 /\ -a1 + b - 1 >= 0 /\ a1 - h1 >= 0 /\ -b1 >= 0 /\ a - b1 - 2 >= 0 /\ b1 >= 0 /\ a + b1 - 2 >= 0 /\ a - 2 >= 0 /\ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
	start location:	f9
	leaf cost:	4

By chaining the transition f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 3) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 ] with all transitions in problem 11, the following new transition is obtained:
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 4) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 ]
We thus obtain the following problem:
12:	T:
		(2, 5)                 f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 4) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ -m >= 0 /\ g - m >= 0 /\ b1 - m >= 0 /\ -b1 - m >= 0 /\ a - m - 2 >= 0 /\ m >= 0 /\ g + m >= 0 /\ b1 + m >= 0 /\ -b1 + m >= 0 /\ a + m - 2 >= 0 /\ a - g >= 0 /\ g >= 0 /\ b1 + g >= 0 /\ -b1 + g >= 0 /\ a + g - 2 >= 0 /\ a1 - b + 1 >= 0 /\ -h1 + b - 1 >= 0 /\ -a1 + b - 1 >= 0 /\ a1 - h1 >= 0 /\ -b1 >= 0 /\ a - b1 - 2 >= 0 /\ b1 >= 0 /\ a + b1 - 2 >= 0 /\ a - 2 >= 0 /\ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
	start location:	f9
	leaf cost:	4

By chaining the transition f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 4) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 ] with all transitions in problem 12, the following new transition is obtained:
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 5) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 ]
We thus obtain the following problem:
13:	T:
		(2, 6)                 f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 5) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ -m >= 0 /\ g - m >= 0 /\ b1 - m >= 0 /\ -b1 - m >= 0 /\ a - m - 2 >= 0 /\ m >= 0 /\ g + m >= 0 /\ b1 + m >= 0 /\ -b1 + m >= 0 /\ a + m - 2 >= 0 /\ a - g >= 0 /\ g >= 0 /\ b1 + g >= 0 /\ -b1 + g >= 0 /\ a + g - 2 >= 0 /\ a1 - b + 1 >= 0 /\ -h1 + b - 1 >= 0 /\ -a1 + b - 1 >= 0 /\ a1 - h1 >= 0 /\ -b1 >= 0 /\ a - b1 - 2 >= 0 /\ b1 >= 0 /\ a + b1 - 2 >= 0 /\ a - 2 >= 0 /\ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
	start location:	f9
	leaf cost:	4

By chaining the transition f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 5) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 ] with all transitions in problem 13, the following new transition is obtained:
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 6) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 ]
We thus obtain the following problem:
14:	T:
		(2, 7)                 f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 6) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ -m >= 0 /\ g - m >= 0 /\ b1 - m >= 0 /\ -b1 - m >= 0 /\ a - m - 2 >= 0 /\ m >= 0 /\ g + m >= 0 /\ b1 + m >= 0 /\ -b1 + m >= 0 /\ a + m - 2 >= 0 /\ a - g >= 0 /\ g >= 0 /\ b1 + g >= 0 /\ -b1 + g >= 0 /\ a + g - 2 >= 0 /\ a1 - b + 1 >= 0 /\ -h1 + b - 1 >= 0 /\ -a1 + b - 1 >= 0 /\ a1 - h1 >= 0 /\ -b1 >= 0 /\ a - b1 - 2 >= 0 /\ b1 >= 0 /\ a + b1 - 2 >= 0 /\ a - 2 >= 0 /\ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
	start location:	f9
	leaf cost:	4

By chaining the transition f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 6) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 ] with all transitions in problem 14, the following new transition is obtained:
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 7) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 ]
We thus obtain the following problem:
15:	T:
		(2, 8)                 f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 7) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ -m >= 0 /\ g - m >= 0 /\ b1 - m >= 0 /\ -b1 - m >= 0 /\ a - m - 2 >= 0 /\ m >= 0 /\ g + m >= 0 /\ b1 + m >= 0 /\ -b1 + m >= 0 /\ a + m - 2 >= 0 /\ a - g >= 0 /\ g >= 0 /\ b1 + g >= 0 /\ -b1 + g >= 0 /\ a + g - 2 >= 0 /\ a1 - b + 1 >= 0 /\ -h1 + b - 1 >= 0 /\ -a1 + b - 1 >= 0 /\ a1 - h1 >= 0 /\ -b1 >= 0 /\ a - b1 - 2 >= 0 /\ b1 >= 0 /\ a + b1 - 2 >= 0 /\ a - 2 >= 0 /\ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
	start location:	f9
	leaf cost:	4

By chaining the transition f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 7) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 ] with all transitions in problem 15, the following new transition is obtained:
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 8) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 ]
We thus obtain the following problem:
16:	T:
		(2, 9)                 f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 8) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ -m >= 0 /\ g - m >= 0 /\ b1 - m >= 0 /\ -b1 - m >= 0 /\ a - m - 2 >= 0 /\ m >= 0 /\ g + m >= 0 /\ b1 + m >= 0 /\ -b1 + m >= 0 /\ a + m - 2 >= 0 /\ a - g >= 0 /\ g >= 0 /\ b1 + g >= 0 /\ -b1 + g >= 0 /\ a + g - 2 >= 0 /\ a1 - b + 1 >= 0 /\ -h1 + b - 1 >= 0 /\ -a1 + b - 1 >= 0 /\ a1 - h1 >= 0 /\ -b1 >= 0 /\ a - b1 - 2 >= 0 /\ b1 >= 0 /\ a + b1 - 2 >= 0 /\ a - 2 >= 0 /\ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
	start location:	f9
	leaf cost:	4

By chaining the transition f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 8) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 ] with all transitions in problem 16, the following new transition is obtained:
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 9) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 ]
We thus obtain the following problem:
17:	T:
		(2, 10)                f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 9) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ -m >= 0 /\ g - m >= 0 /\ b1 - m >= 0 /\ -b1 - m >= 0 /\ a - m - 2 >= 0 /\ m >= 0 /\ g + m >= 0 /\ b1 + m >= 0 /\ -b1 + m >= 0 /\ a + m - 2 >= 0 /\ a - g >= 0 /\ g >= 0 /\ b1 + g >= 0 /\ -b1 + g >= 0 /\ a + g - 2 >= 0 /\ a1 - b + 1 >= 0 /\ -h1 + b - 1 >= 0 /\ -a1 + b - 1 >= 0 /\ a1 - h1 >= 0 /\ -b1 >= 0 /\ a - b1 - 2 >= 0 /\ b1 >= 0 /\ a + b1 - 2 >= 0 /\ a - 2 >= 0 /\ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
	start location:	f9
	leaf cost:	4

By chaining the transition f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 9) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 ] with all transitions in problem 17, the following new transition is obtained:
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 10) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 ]
We thus obtain the following problem:
18:	T:
		(2, 11)                f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 10) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ -m >= 0 /\ g - m >= 0 /\ b1 - m >= 0 /\ -b1 - m >= 0 /\ a - m - 2 >= 0 /\ m >= 0 /\ g + m >= 0 /\ b1 + m >= 0 /\ -b1 + m >= 0 /\ a + m - 2 >= 0 /\ a - g >= 0 /\ g >= 0 /\ b1 + g >= 0 /\ -b1 + g >= 0 /\ a + g - 2 >= 0 /\ a1 - b + 1 >= 0 /\ -h1 + b - 1 >= 0 /\ -a1 + b - 1 >= 0 /\ a1 - h1 >= 0 /\ -b1 >= 0 /\ a - b1 - 2 >= 0 /\ b1 >= 0 /\ a + b1 - 2 >= 0 /\ a - 2 >= 0 /\ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
	start location:	f9
	leaf cost:	4

By chaining the transition f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 10) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 ] with all transitions in problem 18, the following new transition is obtained:
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 11) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 /\ 10 >= 0 /\ m1''''''''''' >= 2 /\ h1 - 10 >= 0 ]
We thus obtain the following problem:
19:	T:
		(2, 12)                f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 11) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 /\ 10 >= 0 /\ m1''''''''''' >= 2 /\ h1 - 10 >= 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ -m >= 0 /\ g - m >= 0 /\ b1 - m >= 0 /\ -b1 - m >= 0 /\ a - m - 2 >= 0 /\ m >= 0 /\ g + m >= 0 /\ b1 + m >= 0 /\ -b1 + m >= 0 /\ a + m - 2 >= 0 /\ a - g >= 0 /\ g >= 0 /\ b1 + g >= 0 /\ -b1 + g >= 0 /\ a + g - 2 >= 0 /\ a1 - b + 1 >= 0 /\ -h1 + b - 1 >= 0 /\ -a1 + b - 1 >= 0 /\ a1 - h1 >= 0 /\ -b1 >= 0 /\ a - b1 - 2 >= 0 /\ b1 >= 0 /\ a + b1 - 2 >= 0 /\ a - 2 >= 0 /\ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
	start location:	f9
	leaf cost:	4

By chaining the transition f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 11) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 /\ 10 >= 0 /\ m1''''''''''' >= 2 /\ h1 - 10 >= 0 ] with all transitions in problem 19, the following new transition is obtained:
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 12) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 /\ 10 >= 0 /\ m1''''''''''' >= 2 /\ h1 - 10 >= 0 /\ 11 >= 0 /\ m1'''''''''''' >= 2 /\ h1 - 11 >= 0 ]
We thus obtain the following problem:
20:	T:
		(2, 13)                f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 12) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 /\ 10 >= 0 /\ m1''''''''''' >= 2 /\ h1 - 10 >= 0 /\ 11 >= 0 /\ m1'''''''''''' >= 2 /\ h1 - 11 >= 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ -m >= 0 /\ g - m >= 0 /\ b1 - m >= 0 /\ -b1 - m >= 0 /\ a - m - 2 >= 0 /\ m >= 0 /\ g + m >= 0 /\ b1 + m >= 0 /\ -b1 + m >= 0 /\ a + m - 2 >= 0 /\ a - g >= 0 /\ g >= 0 /\ b1 + g >= 0 /\ -b1 + g >= 0 /\ a + g - 2 >= 0 /\ a1 - b + 1 >= 0 /\ -h1 + b - 1 >= 0 /\ -a1 + b - 1 >= 0 /\ a1 - h1 >= 0 /\ -b1 >= 0 /\ a - b1 - 2 >= 0 /\ b1 >= 0 /\ a + b1 - 2 >= 0 /\ a - 2 >= 0 /\ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
	start location:	f9
	leaf cost:	4

By chaining the transition f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 12) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 /\ 10 >= 0 /\ m1''''''''''' >= 2 /\ h1 - 10 >= 0 /\ 11 >= 0 /\ m1'''''''''''' >= 2 /\ h1 - 11 >= 0 ] with all transitions in problem 20, the following new transition is obtained:
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 13) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 /\ 10 >= 0 /\ m1''''''''''' >= 2 /\ h1 - 10 >= 0 /\ 11 >= 0 /\ m1'''''''''''' >= 2 /\ h1 - 11 >= 0 /\ 12 >= 0 /\ m1''''''''''''' >= 2 /\ h1 - 12 >= 0 ]
We thus obtain the following problem:
21:	T:
		(2, 14)                f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 13) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 /\ 10 >= 0 /\ m1''''''''''' >= 2 /\ h1 - 10 >= 0 /\ 11 >= 0 /\ m1'''''''''''' >= 2 /\ h1 - 11 >= 0 /\ 12 >= 0 /\ m1''''''''''''' >= 2 /\ h1 - 12 >= 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ -m >= 0 /\ g - m >= 0 /\ b1 - m >= 0 /\ -b1 - m >= 0 /\ a - m - 2 >= 0 /\ m >= 0 /\ g + m >= 0 /\ b1 + m >= 0 /\ -b1 + m >= 0 /\ a + m - 2 >= 0 /\ a - g >= 0 /\ g >= 0 /\ b1 + g >= 0 /\ -b1 + g >= 0 /\ a + g - 2 >= 0 /\ a1 - b + 1 >= 0 /\ -h1 + b - 1 >= 0 /\ -a1 + b - 1 >= 0 /\ a1 - h1 >= 0 /\ -b1 >= 0 /\ a - b1 - 2 >= 0 /\ b1 >= 0 /\ a + b1 - 2 >= 0 /\ a - 2 >= 0 /\ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
	start location:	f9
	leaf cost:	4

By chaining the transition f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 13) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 /\ 10 >= 0 /\ m1''''''''''' >= 2 /\ h1 - 10 >= 0 /\ 11 >= 0 /\ m1'''''''''''' >= 2 /\ h1 - 11 >= 0 /\ 12 >= 0 /\ m1''''''''''''' >= 2 /\ h1 - 12 >= 0 ] with all transitions in problem 21, the following new transition is obtained:
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 14) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 /\ 10 >= 0 /\ m1''''''''''' >= 2 /\ h1 - 10 >= 0 /\ 11 >= 0 /\ m1'''''''''''' >= 2 /\ h1 - 11 >= 0 /\ 12 >= 0 /\ m1''''''''''''' >= 2 /\ h1 - 12 >= 0 /\ 13 >= 0 /\ m1'''''''''''''' >= 2 /\ h1 - 13 >= 0 ]
We thus obtain the following problem:
22:	T:
		(2, 15)                f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 14) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 /\ 10 >= 0 /\ m1''''''''''' >= 2 /\ h1 - 10 >= 0 /\ 11 >= 0 /\ m1'''''''''''' >= 2 /\ h1 - 11 >= 0 /\ 12 >= 0 /\ m1''''''''''''' >= 2 /\ h1 - 12 >= 0 /\ 13 >= 0 /\ m1'''''''''''''' >= 2 /\ h1 - 13 >= 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ -m >= 0 /\ g - m >= 0 /\ b1 - m >= 0 /\ -b1 - m >= 0 /\ a - m - 2 >= 0 /\ m >= 0 /\ g + m >= 0 /\ b1 + m >= 0 /\ -b1 + m >= 0 /\ a + m - 2 >= 0 /\ a - g >= 0 /\ g >= 0 /\ b1 + g >= 0 /\ -b1 + g >= 0 /\ a + g - 2 >= 0 /\ a1 - b + 1 >= 0 /\ -h1 + b - 1 >= 0 /\ -a1 + b - 1 >= 0 /\ a1 - h1 >= 0 /\ -b1 >= 0 /\ a - b1 - 2 >= 0 /\ b1 >= 0 /\ a + b1 - 2 >= 0 /\ a - 2 >= 0 /\ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
	start location:	f9
	leaf cost:	4

By chaining the transition f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1'', g, i, 0, q, r, s, h1, 0, d, h1 - 14) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 /\ 10 >= 0 /\ m1''''''''''' >= 2 /\ h1 - 10 >= 0 /\ 11 >= 0 /\ m1'''''''''''' >= 2 /\ h1 - 11 >= 0 /\ 12 >= 0 /\ m1''''''''''''' >= 2 /\ h1 - 12 >= 0 /\ 13 >= 0 /\ m1'''''''''''''' >= 2 /\ h1 - 13 >= 0 ] with all transitions in problem 22, the following new transition is obtained:
	f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 15) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 /\ 10 >= 0 /\ m1''''''''''' >= 2 /\ h1 - 10 >= 0 /\ 11 >= 0 /\ m1'''''''''''' >= 2 /\ h1 - 11 >= 0 /\ 12 >= 0 /\ m1''''''''''''' >= 2 /\ h1 - 12 >= 0 /\ 13 >= 0 /\ m1'''''''''''''' >= 2 /\ h1 - 13 >= 0 /\ 14 >= 0 /\ m1''''''''''''''' >= 2 /\ h1 - 14 >= 0 ]
We thus obtain the following problem:
23:	T:
		(2, 16)                f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, h1 + 1, o1', g, i, 0, q, r, s, h1, 0, d, h1 - 15) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ o1 >= 2 /\ m1 >= 2 /\ g >= 0 /\ m = 0 /\ 0 >= 0 /\ a + g - 2 >= 0 /\ m1' >= 2 /\ h1 >= 0 /\ 0 = 0 /\ 1 >= 0 /\ m1'' >= 2 /\ h1 - 1 >= 0 /\ 2 >= 0 /\ m1''' >= 2 /\ h1 - 2 >= 0 /\ 3 >= 0 /\ m1'''' >= 2 /\ h1 - 3 >= 0 /\ 4 >= 0 /\ m1''''' >= 2 /\ h1 - 4 >= 0 /\ 5 >= 0 /\ m1'''''' >= 2 /\ h1 - 5 >= 0 /\ 6 >= 0 /\ m1''''''' >= 2 /\ h1 - 6 >= 0 /\ 7 >= 0 /\ m1'''''''' >= 2 /\ h1 - 7 >= 0 /\ 8 >= 0 /\ m1''''''''' >= 2 /\ h1 - 8 >= 0 /\ 9 >= 0 /\ m1'''''''''' >= 2 /\ h1 - 9 >= 0 /\ 10 >= 0 /\ m1''''''''''' >= 2 /\ h1 - 10 >= 0 /\ 11 >= 0 /\ m1'''''''''''' >= 2 /\ h1 - 11 >= 0 /\ 12 >= 0 /\ m1''''''''''''' >= 2 /\ h1 - 12 >= 0 /\ 13 >= 0 /\ m1'''''''''''''' >= 2 /\ h1 - 13 >= 0 /\ 14 >= 0 /\ m1''''''''''''''' >= 2 /\ h1 - 14 >= 0 ]
		(1, 1)                 f9(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(2, b, d, g, i, m, m1, p1, q1, a1, b1, g1, h1) [ m1 >= 2 ]
		(2, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(g, 0, r, g, i, r, o1, p1, s1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ a >= q /\ a >= 0 /\ m1 >= 2 /\ r1 >= m1 /\ g >= m1 /\ b = 0 ]
		(?, 1)                 f1(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f1(a + 1, b, d, g, i, m, q, s, m1, a1, b1, g1, h1) [ q - 2 >= 0 /\ a + q - 4 >= 0 /\ -a + q >= 0 /\ a - 2 >= 0 /\ q >= a + 1 /\ a >= 0 ]
		(b + g + 1, 1)         f16(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f16(a, b + 1, o1, g - 1, i, m, q, r, s, a1, b1, g1, h1) [ a - g >= 0 /\ b + g - 2 >= 0 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ g >= 0 /\ m1 >= 2 ]
		(b + g + h1 + 1, 1)    f8(a, b, d, g, i, m, q, r, s, a1, b1, g1, h1) -> f8(a, b, o1, g, i, 0, q, r, s, a1, 0, g1, h1 - 1) [ -m >= 0 /\ g - m >= 0 /\ b1 - m >= 0 /\ -b1 - m >= 0 /\ a - m - 2 >= 0 /\ m >= 0 /\ g + m >= 0 /\ b1 + m >= 0 /\ -b1 + m >= 0 /\ a + m - 2 >= 0 /\ a - g >= 0 /\ g >= 0 /\ b1 + g >= 0 /\ -b1 + g >= 0 /\ a + g - 2 >= 0 /\ a1 - b + 1 >= 0 /\ -h1 + b - 1 >= 0 /\ -a1 + b - 1 >= 0 /\ a1 - h1 >= 0 /\ -b1 >= 0 /\ a - b1 - 2 >= 0 /\ b1 >= 0 /\ a + b1 - 2 >= 0 /\ a - 2 >= 0 /\ m1 >= 2 /\ h1 >= 0 /\ b1 = 0 ]
	start location:	f9
	leaf cost:	4

Complexity upper bound ?

Time: 4.905 sec (SMT: 4.311 sec)