MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f79(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f81(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ 0 >= a ]
		(?, 1)    f34(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f34(a, b - 1, g2, 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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ b >= 1 /\ 0 >= g2 ]
		(?, 1)    f34(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f44(a, b - 1, g2, h2, i2, 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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ 0 >= h2 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f81(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f65(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ 0 >= f ]
		(?, 1)    f65(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f75(a, b, c, d, e, g2, g - 1, h2, i2, 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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ g >= 1 /\ 0 >= h2 ]
		(?, 1)    f75(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f79(g2, 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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ 0 >= i ]
		(?, 1)    f209(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f209(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2)
		(?, 1)    f211(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f214(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2)
		(?, 1)    f190(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f190(a, b, c, d, e, f, g, h, i, j - 1, 1, 2, 1, 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, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ j >= 1 ]
		(?, 1)    f190(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f209(a, b, c, d, e, f, g, h, i, j, k, l, m, 2, 0, g2, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ 0 >= j /\ n = 2 ]
		(?, 1)    f190(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f209(a, b, c, d, e, f, g, h, i, j, k, l, m, n, 0, g2, 1, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ 1 >= n /\ 0 >= j ]
		(?, 1)    f190(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f209(a, b, c, d, e, f, g, h, i, j, k, l, m, n, 0, g2, 1, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ n >= 3 /\ 0 >= j ]
		(?, 1)    f130(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f190(a, b, c, d, e, f, g, h, i, i2, k, l, m, n, 0, p, q, 0, g2, g2, h2, i2, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ 0 >= g2 ]
		(?, 1)    f155(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f130(a, b, c, d, e, f, g, h, i, j, k, l, m, 0, o, p, q, 0, s, t, u, v, w, w, w, 0, b1, b1, w, 0, w, b1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ w >= 1 ]
		(?, 1)    f155(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f130(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, 0, s, t, u, v, w, w, y, z, a1, b1, c1, d1, e1, f1, b1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ 0 >= w ]
		(?, 1)    f130(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f130(a, b, c, d, e, f, g, h, i, j, k, l, m, n, 0, p, q, 0, g2, g2 - 1, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h2, i2, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ g2 >= 1 /\ 0 >= h2 ]
		(?, 1)    f130(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f130(a, b, c, d, e, f, g, h, i, j, k, l, m, n, 0, p, q, 0, g2, g2 - 1, u, v, w, j2, y, z, a1, 0, c1, d1, e1, f1, g1, h2, i2, 1, 0, 0, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ g2 >= 1 /\ h2 >= 1 ]
		(?, 1)    f100(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f130(a, b, c, d, e, f, g, h, i, j, k, l, m, n, 0, p, q, 0, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, g2, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ 0 >= m1 ]
		(?, 1)    f100(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f100(a, b, c, d, e, f, g, h, i, j, k, l, m, n, 0, p, q, 0, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1 - 1, n1, g2, h2, i2, g2, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ m1 >= 1 ]
		(?, 1)    f81(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f65(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ f >= 1 ]
		(?, 1)    f79(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f81(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ a >= 1 ]
		(?, 1)    f75(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f79(g2, 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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ i >= 1 ]
		(?, 1)    f65(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f75(a, b, c, d, e, g2, g - 1, h2, i2, 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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ g >= 1 /\ h2 >= 1 ]
		(?, 1)    f65(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f100(a, b, c, d, e, f, g, h, i, j, k, l, m, n, 0, p, q, 0, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, h2, n1, o1, p1, q1, r1, g2, h2, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ 0 >= g ]
		(?, 1)    f44(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f34(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, m1, n1, o1, p1, q1, r1, s1, t1, c, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ 0 >= e ]
		(?, 1)    f44(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f34(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, m1, n1, o1, p1, q1, r1, s1, t1, c, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ e >= 1 ]
		(?, 1)    f34(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f44(a, b - 1, g2, h2, i2, 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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ h2 >= 1 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f34(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f65(a, b, c, d, e, f, h2, h, i, j, k, l, m, n, 0, p, q, 0, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, g2, h2, x1, y1, z1, a2, b2, c2, d2, e2, f2) [ 0 >= b ]
		(1, 1)    f0(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f34(a, i2, c, d, e, f, g, h, i, j, 0, l, m, 0, 0, p, 0, 0, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, 0, 0, g2, h2, 0, i2, d2, e2, f2) [ 0 >= h2 ]
		(1, 1)    f0(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, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2) -> f34(a, j2, c, d, e, f, g, h, i, j, 0, l, m, 0, 0, p, 0, 0, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, 0, 0, g2, h2, 0, j2, 1, i2, 0) [ h2 >= 1 ]
	start location:	f0
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, e, f, g, i, j, n, w, m1].
We thus obtain the following problem:
2:	T:
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, j2, e, f, g, i, j, 0, w, m1) [ h2 >= 1 ]
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, i2, e, f, g, i, j, 0, w, m1) [ 0 >= h2 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, h2, i, j, n, w, m1) [ 0 >= b ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ h2 >= 1 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ e >= 1 ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ 0 >= e ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, h2) [ 0 >= g ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ g >= 1 /\ h2 >= 1 ]
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ i >= 1 ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ a >= 1 ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ f >= 1 ]
		(?, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, m1 - 1) [ m1 >= 1 ]
		(?, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ 0 >= m1 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ g2 >= 1 /\ h2 >= 1 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ g2 >= 1 /\ 0 >= h2 ]
		(?, 1)    f155(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ 0 >= w ]
		(?, 1)    f155(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, 0, w, m1) [ w >= 1 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, i2, n, w, m1) [ 0 >= g2 ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ n >= 3 /\ 0 >= j ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ 1 >= n /\ 0 >= j ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, 2, w, m1) [ 0 >= j /\ n = 2 ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, j - 1, n, w, m1) [ j >= 1 ]
		(?, 1)    f211(a, b, e, f, g, i, j, n, w, m1) -> f214(a, b, e, f, g, i, j, n, w, m1)
		(?, 1)    f209(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1)
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ 0 >= i ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ g >= 1 /\ 0 >= h2 ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ 0 >= f ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ 0 >= h2 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b - 1, e, f, g, i, j, n, w, m1) [ b >= 1 /\ 0 >= g2 ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ 0 >= a ]
	start location:	f0
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, j2, e, f, g, i, j, 0, w, m1) [ h2 >= 1 ]
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, i2, e, f, g, i, j, 0, w, m1) [ 0 >= h2 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, h2, i, j, n, w, m1) [ 0 >= b ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ h2 >= 1 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ e >= 1 ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ 0 >= e ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, h2) [ 0 >= g ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ g >= 1 /\ h2 >= 1 ]
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ i >= 1 ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ a >= 1 ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ f >= 1 ]
		(?, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, m1 - 1) [ m1 >= 1 ]
		(?, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ 0 >= m1 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ g2 >= 1 /\ h2 >= 1 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ g2 >= 1 /\ 0 >= h2 ]
		(?, 1)    f155(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ 0 >= w ]
		(?, 1)    f155(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, 0, w, m1) [ w >= 1 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, i2, n, w, m1) [ 0 >= g2 ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ n >= 3 /\ 0 >= j ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ 1 >= n /\ 0 >= j ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, 2, w, m1) [ 0 >= j /\ n = 2 ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, j - 1, n, w, m1) [ j >= 1 ]
		(?, 1)    f209(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1)
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ 0 >= i ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ g >= 1 /\ 0 >= h2 ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ 0 >= f ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ 0 >= h2 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b - 1, e, f, g, i, j, n, w, m1) [ b >= 1 /\ 0 >= g2 ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ 0 >= a ]
	start location:	f0
	leaf cost:	1

Testing for reachability in the complexity graph removes the following transitions from problem 3:
	f155(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ 0 >= w ]
	f155(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, 0, w, m1) [ w >= 1 ]
We thus obtain the following problem:
4:	T:
		(?, 1)    f209(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1)
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, j - 1, n, w, m1) [ j >= 1 ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, 2, w, m1) [ 0 >= j /\ n = 2 ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ 1 >= n /\ 0 >= j ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ n >= 3 /\ 0 >= j ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ 0 >= f ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ f >= 1 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, i2, n, w, m1) [ 0 >= g2 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ g2 >= 1 /\ 0 >= h2 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ g2 >= 1 /\ h2 >= 1 ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ 0 >= a ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ a >= 1 ]
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ 0 >= i ]
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ i >= 1 ]
		(?, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ 0 >= m1 ]
		(?, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, m1 - 1) [ m1 >= 1 ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ 0 >= e ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ e >= 1 ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ g >= 1 /\ 0 >= h2 ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ g >= 1 /\ h2 >= 1 ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, h2) [ 0 >= g ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b - 1, e, f, g, i, j, n, w, m1) [ b >= 1 /\ 0 >= g2 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ 0 >= h2 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ h2 >= 1 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, h2, i, j, n, w, m1) [ 0 >= b ]
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, i2, e, f, g, i, j, 0, w, m1) [ 0 >= h2 ]
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, j2, e, f, g, i, j, 0, w, m1) [ h2 >= 1 ]
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f209) = -4
	Pol(f190) = -3
	Pol(f81) = 1
	Pol(f65) = 1
	Pol(f130) = -2
	Pol(f79) = 1
	Pol(f75) = 1
	Pol(f100) = -1
	Pol(f44) = 2
	Pol(f34) = 2
	Pol(f0) = 2
orients all transitions weakly and the transitions
	f65(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, h2) [ 0 >= g ]
	f34(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, h2, i, j, n, w, m1) [ 0 >= b ]
strictly and produces the following problem:
5:	T:
		(?, 1)    f209(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1)
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, j - 1, n, w, m1) [ j >= 1 ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, 2, w, m1) [ 0 >= j /\ n = 2 ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ 1 >= n /\ 0 >= j ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ n >= 3 /\ 0 >= j ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ 0 >= f ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ f >= 1 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, i2, n, w, m1) [ 0 >= g2 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ g2 >= 1 /\ 0 >= h2 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ g2 >= 1 /\ h2 >= 1 ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ 0 >= a ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ a >= 1 ]
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ 0 >= i ]
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ i >= 1 ]
		(?, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ 0 >= m1 ]
		(?, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, m1 - 1) [ m1 >= 1 ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ 0 >= e ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ e >= 1 ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ g >= 1 /\ 0 >= h2 ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ g >= 1 /\ h2 >= 1 ]
		(2, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, h2) [ 0 >= g ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b - 1, e, f, g, i, j, n, w, m1) [ b >= 1 /\ 0 >= g2 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ 0 >= h2 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ h2 >= 1 /\ b >= 1 /\ g2 >= 1 ]
		(2, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, h2, i, j, n, w, m1) [ 0 >= b ]
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, i2, e, f, g, i, j, 0, w, m1) [ 0 >= h2 ]
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, j2, e, f, g, i, j, 0, w, m1) [ h2 >= 1 ]
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f209) = 0
	Pol(f190) = 1
	Pol(f81) = 3
	Pol(f65) = 3
	Pol(f130) = 2
	Pol(f79) = 3
	Pol(f75) = 3
	Pol(f100) = 3
	Pol(f44) = 3
	Pol(f34) = 3
	Pol(f0) = 3
orients all transitions weakly and the transitions
	f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ 1 >= n /\ 0 >= j ]
	f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ n >= 3 /\ 0 >= j ]
	f130(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, i2, n, w, m1) [ 0 >= g2 ]
	f100(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ 0 >= m1 ]
strictly and produces the following problem:
6:	T:
		(?, 1)    f209(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1)
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, j - 1, n, w, m1) [ j >= 1 ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, 2, w, m1) [ 0 >= j /\ n = 2 ]
		(3, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ 1 >= n /\ 0 >= j ]
		(3, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ n >= 3 /\ 0 >= j ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ 0 >= f ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ f >= 1 ]
		(3, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, i2, n, w, m1) [ 0 >= g2 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ g2 >= 1 /\ 0 >= h2 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ g2 >= 1 /\ h2 >= 1 ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ 0 >= a ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ a >= 1 ]
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ 0 >= i ]
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ i >= 1 ]
		(3, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ 0 >= m1 ]
		(?, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, m1 - 1) [ m1 >= 1 ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ 0 >= e ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ e >= 1 ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ g >= 1 /\ 0 >= h2 ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ g >= 1 /\ h2 >= 1 ]
		(2, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, h2) [ 0 >= g ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b - 1, e, f, g, i, j, n, w, m1) [ b >= 1 /\ 0 >= g2 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ 0 >= h2 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ h2 >= 1 /\ b >= 1 /\ g2 >= 1 ]
		(2, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, h2, i, j, n, w, m1) [ 0 >= b ]
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, i2, e, f, g, i, j, 0, w, m1) [ 0 >= h2 ]
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, j2, e, f, g, i, j, 0, w, m1) [ h2 >= 1 ]
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f209) = 0
	Pol(f190) = 1
	Pol(f81) = 1
	Pol(f65) = 1
	Pol(f130) = 1
	Pol(f79) = 1
	Pol(f75) = 1
	Pol(f100) = 1
	Pol(f44) = 1
	Pol(f34) = 1
	Pol(f0) = 1
orients all transitions weakly and the transition
	f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, 2, w, m1) [ 0 >= j /\ n = 2 ]
strictly and produces the following problem:
7:	T:
		(?, 1)    f209(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1)
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, j - 1, n, w, m1) [ j >= 1 ]
		(1, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, 2, w, m1) [ 0 >= j /\ n = 2 ]
		(3, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ 1 >= n /\ 0 >= j ]
		(3, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ n >= 3 /\ 0 >= j ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ 0 >= f ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ f >= 1 ]
		(3, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, i2, n, w, m1) [ 0 >= g2 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ g2 >= 1 /\ 0 >= h2 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ g2 >= 1 /\ h2 >= 1 ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ 0 >= a ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ a >= 1 ]
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ 0 >= i ]
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ i >= 1 ]
		(3, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ 0 >= m1 ]
		(?, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, m1 - 1) [ m1 >= 1 ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ 0 >= e ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ e >= 1 ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ g >= 1 /\ 0 >= h2 ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ g >= 1 /\ h2 >= 1 ]
		(2, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, h2) [ 0 >= g ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b - 1, e, f, g, i, j, n, w, m1) [ b >= 1 /\ 0 >= g2 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ 0 >= h2 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ h2 >= 1 /\ b >= 1 /\ g2 >= 1 ]
		(2, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, h2, i, j, n, w, m1) [ 0 >= b ]
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, i2, e, f, g, i, j, 0, w, m1) [ 0 >= h2 ]
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, j2, e, f, g, i, j, 0, w, m1) [ h2 >= 1 ]
	start location:	f0
	leaf cost:	1

Applied AI with 'oct' on problem 7 to obtain the following invariants:
  For symbol f100: -X_8 >= 0 /\ -X_5 - X_8 >= 0 /\ -X_2 - X_8 >= 0 /\ X_8 >= 0 /\ -X_5 + X_8 >= 0 /\ -X_2 + X_8 >= 0 /\ -X_5 >= 0 /\ -X_2 - X_5 >= 0 /\ -X_2 >= 0
  For symbol f130: -X_8 >= 0 /\ -X_5 - X_8 >= 0 /\ -X_2 - X_8 >= 0 /\ -X_10 - X_8 >= 0 /\ X_8 >= 0 /\ -X_5 + X_8 >= 0 /\ -X_2 + X_8 >= 0 /\ -X_10 + X_8 >= 0 /\ -X_5 >= 0 /\ -X_2 - X_5 >= 0 /\ -X_10 - X_5 >= 0 /\ -X_2 >= 0 /\ -X_10 - X_2 >= 0 /\ -X_10 >= 0
  For symbol f190: -X_8 >= 0 /\ -X_5 - X_8 >= 0 /\ -X_2 - X_8 >= 0 /\ -X_10 - X_8 >= 0 /\ X_8 >= 0 /\ -X_5 + X_8 >= 0 /\ -X_2 + X_8 >= 0 /\ -X_10 + X_8 >= 0 /\ -X_5 >= 0 /\ -X_2 - X_5 >= 0 /\ -X_10 - X_5 >= 0 /\ -X_2 >= 0 /\ -X_10 - X_2 >= 0 /\ -X_10 >= 0
  For symbol f209: -X_8 >= 0 /\ -X_7 - X_8 >= 0 /\ -X_5 - X_8 >= 0 /\ -X_2 - X_8 >= 0 /\ -X_10 - X_8 >= 0 /\ X_8 >= 0 /\ -X_7 + X_8 >= 0 /\ -X_5 + X_8 >= 0 /\ -X_2 + X_8 >= 0 /\ -X_10 + X_8 >= 0 /\ -X_7 >= 0 /\ -X_5 - X_7 >= 0 /\ -X_2 - X_7 >= 0 /\ -X_10 - X_7 >= 0 /\ -X_5 >= 0 /\ -X_2 - X_5 >= 0 /\ -X_10 - X_5 >= 0 /\ -X_2 >= 0 /\ -X_10 - X_2 >= 0 /\ -X_10 >= 0
  For symbol f34: -X_8 >= 0 /\ X_8 >= 0
  For symbol f44: -X_8 >= 0 /\ X_2 - X_8 >= 0 /\ X_8 >= 0 /\ X_2 + X_8 >= 0 /\ X_2 >= 0
  For symbol f65: -X_8 >= 0 /\ -X_2 - X_8 >= 0 /\ X_8 >= 0 /\ -X_2 + X_8 >= 0 /\ -X_2 >= 0
  For symbol f75: -X_8 >= 0 /\ X_5 - X_8 >= 0 /\ -X_2 - X_8 >= 0 /\ X_8 >= 0 /\ X_5 + X_8 >= 0 /\ -X_2 + X_8 >= 0 /\ X_5 >= 0 /\ -X_2 + X_5 >= 0 /\ -X_2 >= 0
  For symbol f79: -X_8 >= 0 /\ X_5 - X_8 >= 0 /\ -X_2 - X_8 >= 0 /\ X_8 >= 0 /\ X_5 + X_8 >= 0 /\ -X_2 + X_8 >= 0 /\ X_5 >= 0 /\ -X_2 + X_5 >= 0 /\ -X_2 >= 0
  For symbol f81: -X_8 >= 0 /\ X_5 - X_8 >= 0 /\ -X_2 - X_8 >= 0 /\ X_8 >= 0 /\ X_5 + X_8 >= 0 /\ -X_2 + X_8 >= 0 /\ X_5 >= 0 /\ -X_2 + X_5 >= 0 /\ -X_2 >= 0


This yielded the following problem:
8:	T:
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, j2, e, f, g, i, j, 0, w, m1) [ h2 >= 1 ]
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, i2, e, f, g, i, j, 0, w, m1) [ 0 >= h2 ]
		(2, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, h2, i, j, n, w, m1) [ -n >= 0 /\ n >= 0 /\ 0 >= b ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ -n >= 0 /\ n >= 0 /\ h2 >= 1 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ -n >= 0 /\ n >= 0 /\ 0 >= h2 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b - 1, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ n >= 0 /\ b >= 1 /\ 0 >= g2 ]
		(2, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, h2) [ -n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ -b + n >= 0 /\ -b >= 0 /\ 0 >= g ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ -n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ -b + n >= 0 /\ -b >= 0 /\ g >= 1 /\ h2 >= 1 ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ -n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ -b + n >= 0 /\ -b >= 0 /\ g >= 1 /\ 0 >= h2 ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ b - n >= 0 /\ n >= 0 /\ b + n >= 0 /\ b >= 0 /\ e >= 1 ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ b - n >= 0 /\ n >= 0 /\ b + n >= 0 /\ b >= 0 /\ 0 >= e ]
		(?, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, m1 - 1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -b >= 0 /\ m1 >= 1 ]
		(3, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -b >= 0 /\ 0 >= m1 ]
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ i >= 1 ]
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= i ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ a >= 1 ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= a ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ g2 >= 1 /\ h2 >= 1 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ g2 >= 1 /\ 0 >= h2 ]
		(3, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, i2, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ 0 >= g2 ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ f >= 1 ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= f ]
		(3, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ n >= 3 /\ 0 >= j ]
		(3, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ 1 >= n /\ 0 >= j ]
		(1, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, 2, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ 0 >= j /\ n = 2 ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, j - 1, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ j >= 1 ]
		(?, 1)    f209(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -j - n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -j + n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -j >= 0 /\ -g - j >= 0 /\ -b - j >= 0 /\ -m1 - j >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 ]
	start location:	f0
	leaf cost:	1

Testing for unsatisfiable constraints removes the following transitions from problem 8:
	f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ n >= 3 /\ 0 >= j ]
	f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, 2, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ 0 >= j /\ n = 2 ]
We thus obtain the following problem:
9:	T:
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, j2, e, f, g, i, j, 0, w, m1) [ h2 >= 1 ]
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, i2, e, f, g, i, j, 0, w, m1) [ 0 >= h2 ]
		(2, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, h2, i, j, n, w, m1) [ -n >= 0 /\ n >= 0 /\ 0 >= b ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ -n >= 0 /\ n >= 0 /\ h2 >= 1 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ -n >= 0 /\ n >= 0 /\ 0 >= h2 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b - 1, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ n >= 0 /\ b >= 1 /\ 0 >= g2 ]
		(2, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, h2) [ -n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ -b + n >= 0 /\ -b >= 0 /\ 0 >= g ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ -n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ -b + n >= 0 /\ -b >= 0 /\ g >= 1 /\ h2 >= 1 ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ -n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ -b + n >= 0 /\ -b >= 0 /\ g >= 1 /\ 0 >= h2 ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ b - n >= 0 /\ n >= 0 /\ b + n >= 0 /\ b >= 0 /\ e >= 1 ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ b - n >= 0 /\ n >= 0 /\ b + n >= 0 /\ b >= 0 /\ 0 >= e ]
		(?, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, m1 - 1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -b >= 0 /\ m1 >= 1 ]
		(3, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -b >= 0 /\ 0 >= m1 ]
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ i >= 1 ]
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= i ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ a >= 1 ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= a ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ g2 >= 1 /\ h2 >= 1 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ g2 >= 1 /\ 0 >= h2 ]
		(3, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, i2, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ 0 >= g2 ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ f >= 1 ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= f ]
		(3, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ 1 >= n /\ 0 >= j ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, j - 1, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ j >= 1 ]
		(?, 1)    f209(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -j - n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -j + n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -j >= 0 /\ -g - j >= 0 /\ -b - j >= 0 /\ -m1 - j >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 ]
	start location:	f0
	leaf cost:	1

By chaining the transition f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ 1 >= n /\ 0 >= j ] with all transitions in problem 9, the following new transition is obtained:
	f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ 1 >= n /\ 0 >= j /\ -j - n >= 0 /\ -j + n >= 0 /\ -j >= 0 /\ -g - j >= 0 /\ -b - j >= 0 /\ -m1 - j >= 0 ]
We thus obtain the following problem:
10:	T:
		(3, 2)    f190(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ 1 >= n /\ 0 >= j /\ -j - n >= 0 /\ -j + n >= 0 /\ -j >= 0 /\ -g - j >= 0 /\ -b - j >= 0 /\ -m1 - j >= 0 ]
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, j2, e, f, g, i, j, 0, w, m1) [ h2 >= 1 ]
		(1, 1)    f0(a, b, e, f, g, i, j, n, w, m1) -> f34(a, i2, e, f, g, i, j, 0, w, m1) [ 0 >= h2 ]
		(2, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, h2, i, j, n, w, m1) [ -n >= 0 /\ n >= 0 /\ 0 >= b ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ -n >= 0 /\ n >= 0 /\ h2 >= 1 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f44(a, b - 1, i2, f, g, i, j, n, w, m1) [ -n >= 0 /\ n >= 0 /\ 0 >= h2 /\ b >= 1 /\ g2 >= 1 ]
		(?, 1)    f34(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b - 1, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ n >= 0 /\ b >= 1 /\ 0 >= g2 ]
		(2, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, h2) [ -n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ -b + n >= 0 /\ -b >= 0 /\ 0 >= g ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ -n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ -b + n >= 0 /\ -b >= 0 /\ g >= 1 /\ h2 >= 1 ]
		(?, 1)    f65(a, b, e, f, g, i, j, n, w, m1) -> f75(a, b, e, g2, g - 1, i2, j, n, w, m1) [ -n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ -b + n >= 0 /\ -b >= 0 /\ g >= 1 /\ 0 >= h2 ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ b - n >= 0 /\ n >= 0 /\ b + n >= 0 /\ b >= 0 /\ e >= 1 ]
		(?, 1)    f44(a, b, e, f, g, i, j, n, w, m1) -> f34(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ b - n >= 0 /\ n >= 0 /\ b + n >= 0 /\ b >= 0 /\ 0 >= e ]
		(?, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f100(a, b, e, f, g, i, j, n, w, m1 - 1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -b >= 0 /\ m1 >= 1 ]
		(3, 1)    f100(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -b >= 0 /\ 0 >= m1 ]
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ i >= 1 ]
		(?, 1)    f75(a, b, e, f, g, i, j, n, w, m1) -> f79(g2, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= i ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ a >= 1 ]
		(?, 1)    f79(a, b, e, f, g, i, j, n, w, m1) -> f81(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= a ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ g2 >= 1 /\ h2 >= 1 ]
		(?, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f130(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ g2 >= 1 /\ 0 >= h2 ]
		(3, 1)    f130(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, i2, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ 0 >= g2 ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ f >= 1 ]
		(?, 1)    f81(a, b, e, f, g, i, j, n, w, m1) -> f65(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ g - n >= 0 /\ -b - n >= 0 /\ n >= 0 /\ g + n >= 0 /\ -b + n >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= f ]
		(?, 1)    f190(a, b, e, f, g, i, j, n, w, m1) -> f190(a, b, e, f, g, i, j - 1, n, w, m1) [ -n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 /\ j >= 1 ]
		(?, 1)    f209(a, b, e, f, g, i, j, n, w, m1) -> f209(a, b, e, f, g, i, j, n, w, m1) [ -n >= 0 /\ -j - n >= 0 /\ -g - n >= 0 /\ -b - n >= 0 /\ -m1 - n >= 0 /\ n >= 0 /\ -j + n >= 0 /\ -g + n >= 0 /\ -b + n >= 0 /\ -m1 + n >= 0 /\ -j >= 0 /\ -g - j >= 0 /\ -b - j >= 0 /\ -m1 - j >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -m1 - g >= 0 /\ -b >= 0 /\ -m1 - b >= 0 /\ -m1 >= 0 ]
	start location:	f0
	leaf cost:	1

Complexity upper bound ?

Time: 5.092 sec (SMT: 4.104 sec)