MAYBE Initial complexity problem: 1: T: (?, 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, g2, h2, i2, j2, k2, l2) -> f83(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, g2, h2, i2, j2, k2, l2) [ 0 >= a ] (?, 1) f31(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, g2, h2, i2, j2, k2, l2) -> f31(a, b - 1, m2, m2, 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, g2, h2, i2, j2, k2, l2) [ 0 >= m2 /\ b >= 1 ] (?, 1) f31(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, g2, h2, i2, j2, k2, l2) -> f42(a, b - 1, m2, m2, n2, o2, 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, g2, h2, i2, j2, k2, l2) [ b >= 1 /\ m2 >= 1 /\ 0 >= n2 ] (?, 1) f83(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, g2, h2, i2, j2, k2, l2) -> f67(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, g2, h2, i2, j2, k2, l2) [ 0 >= g ] (?, 1) f67(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, g2, h2, i2, j2, k2, l2) -> f77(a, b, c, d, e, f, m2, h - 1, n2, o2, 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, g2, h2, i2, j2, k2, l2) [ h >= 1 /\ 0 >= n2 ] (?, 1) f77(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, g2, h2, i2, j2, k2, l2) -> f81(m2, 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, g2, h2, i2, j2, k2, l2) [ 0 >= j ] (?, 1) f237(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, g2, h2, i2, j2, k2, l2) -> f237(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, g2, h2, i2, j2, k2, l2) (?, 1) f239(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, g2, h2, i2, j2, k2, l2) -> f242(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, g2, h2, i2, j2, k2, l2) (?, 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, g2, h2, i2, j2, k2, l2) -> f211(a, b, c, d, e, f, g, h, i, j, k, 0, m2, n2, 0, 0, 2, m2, 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, g2, h2, i2, j2, k2, l2) [ k >= 1 /\ 0 >= n2 ] (?, 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, g2, h2, i2, j2, k2, l2) -> f211(a, b, c, d, e, f, g, h, i, j, k - 1, 0, m2, n2, 0, 0, 2, m2, 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, g2, h2, i2, j2, k2, l2) [ k >= 1 /\ n2 >= 1 ] (?, 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, g2, h2, i2, j2, k2, l2) -> f237(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, 0, m2, 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, g2, h2, i2, j2, k2, l2) [ 0 >= k ] (?, 1) f144(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, g2, h2, i2, j2, k2, l2) -> f211(a, b, c, d, e, f, g, h, i, j, n2, l, m, n, o, p, q, r, 0, t, u, 0, m2, n2, 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, g2, h2, i2, j2, k2, l2) [ 0 >= u ] (?, 1) f172(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, g2, h2, i2, j2, k2, l2) -> f144(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, 0, w, x, y, 0, y, y, 0, e1, e1, y, 0, y, e1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2) [ y >= 1 ] (?, 1) f172(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, g2, h2, i2, j2, k2, l2) -> f144(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, 0, w, x, y, z, y, b1, c1, d1, e1, f1, g1, h1, i1, e1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2) [ 0 >= y ] (?, 1) f144(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, g2, h2, i2, j2, k2, l2) -> f144(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, 0, t, u - 1, 0, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, m2, m2, n2, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2) [ u >= 1 /\ 0 >= m2 ] (?, 1) f144(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, g2, h2, i2, j2, k2, l2) -> f144(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, 0, t, u - 1, 0, w, x, y, z, o2, b1, c1, d1, 0, f1, g1, h1, i1, j1, m2, m2, n2, p2, p2, 0, 0, 0, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2) [ u >= 1 /\ m2 >= 1 ] (?, 1) f144(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, g2, h2, i2, j2, k2, l2) -> f172(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, 0, t, u - 1, v, w, x, 0, z, o2, b1, c1, d1, p2, f1, g1, h1, i1, j1, m2, m2, n2, q2, q2, 0, p2, p2, 1, 0, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2) [ 0 >= p2 + 1 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f144(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, g2, h2, i2, j2, k2, l2) -> f172(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, 0, t, u - 1, v, w, x, 0, z, o2, b1, c1, d1, p2, f1, g1, h1, i1, j1, m2, m2, n2, q2, q2, 0, p2, p2, 1, 0, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2) [ p2 >= 1 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f104(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, g2, h2, i2, j2, k2, l2) -> f144(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, 0, t, o2, 0, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, m2, m2, n2, o2, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2) [ 0 >= m2 ] (?, 1) f104(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, g2, h2, i2, j2, k2, l2) -> f104(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, 0, t, u, 0, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, m2, m2 - 1, w1, x1, n2, o2, p2, n2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2) [ m2 >= 1 ] (?, 1) f83(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, g2, h2, i2, j2, k2, l2) -> f67(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, g2, h2, i2, j2, k2, l2) [ g >= 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, g2, h2, i2, j2, k2, l2) -> f83(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, g2, h2, i2, j2, k2, l2) [ a >= 1 ] (?, 1) f77(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, g2, h2, i2, j2, k2, l2) -> f81(m2, 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, g2, h2, i2, j2, k2, l2) [ j >= 1 ] (?, 1) f67(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, g2, h2, i2, j2, k2, l2) -> f77(a, b, c, d, e, f, m2, h - 1, n2, o2, 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, g2, h2, i2, j2, k2, l2) [ h >= 1 /\ n2 >= 1 ] (?, 1) f67(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, g2, h2, i2, j2, k2, l2) -> f104(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, 0, t, u, 0, 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, m2, d2, e2, f2, g2, h2, i2, j2, k2, l2) [ 0 >= h ] (?, 1) f42(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, g2, h2, i2, j2, k2, l2) -> f31(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, d, e2, f2, g2, h2, i2, j2, k2, l2) [ 0 >= f ] (?, 1) f42(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, g2, h2, i2, j2, k2, l2) -> f31(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, d, e2, f2, g2, h2, i2, j2, k2, l2) [ f >= 1 ] (?, 1) f31(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, g2, h2, i2, j2, k2, l2) -> f42(a, b - 1, m2, m2, n2, o2, 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, g2, h2, i2, j2, k2, l2) [ b >= 1 /\ m2 >= 1 /\ n2 >= 1 ] (?, 1) f31(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, g2, h2, i2, j2, k2, l2) -> f67(a, b, c, d, e, f, g, n2, i, j, k, l, m, n, o, p, q, r, 0, t, u, 0, 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, m2, n2, g2, h2, i2, j2, k2, l2) [ 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, g2, h2, i2, j2, k2, l2) -> f31(a, n2, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, 0, t, u, 0, w, x, y, 0, 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, m2, 0, n2, j2, k2, l2) [ 0 >= m2 ] (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, g2, h2, i2, j2, k2, l2) -> f31(a, p2, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, 0, t, u, 0, w, x, y, 0, 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, m2, 0, p2, n2, o2, 0) [ m2 >= 1 ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, f, g, h, j, k, u, y]. We thus obtain the following problem: 2: T: (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, p2, f, g, h, j, k, u, y) [ m2 >= 1 ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, n2, f, g, h, j, k, u, y) [ 0 >= m2 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, n2, j, k, u, y) [ 0 >= b ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ n2 >= 1 ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ f >= 1 ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ 0 >= f ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ 0 >= h ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ h >= 1 /\ n2 >= 1 ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ j >= 1 ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ a >= 1 ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ g >= 1 ] (?, 1) f104(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ m2 >= 1 ] (?, 1) f104(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, o2, y) [ 0 >= m2 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f172(a, b, f, g, h, j, k, u - 1, 0) [ p2 >= 1 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f172(a, b, f, g, h, j, k, u - 1, 0) [ 0 >= p2 + 1 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ u >= 1 /\ 0 >= m2 ] (?, 1) f172(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u, y) [ 0 >= y ] (?, 1) f172(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u, y) [ y >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, n2, u, y) [ 0 >= u ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ 0 >= k ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k - 1, u, y) [ k >= 1 /\ n2 >= 1 ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k, u, y) [ k >= 1 /\ 0 >= n2 ] (?, 1) f239(a, b, f, g, h, j, k, u, y) -> f242(a, b, f, g, h, j, k, u, y) (?, 1) f237(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ 0 >= j ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ h >= 1 /\ 0 >= n2 ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ 0 >= g ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ 0 >= n2 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f31(a, b - 1, f, g, h, j, k, u, y) [ 0 >= m2 /\ b >= 1 ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ 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, f, g, h, j, k, u, y) -> f31(a, p2, f, g, h, j, k, u, y) [ m2 >= 1 ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, n2, f, g, h, j, k, u, y) [ 0 >= m2 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, n2, j, k, u, y) [ 0 >= b ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ n2 >= 1 ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ f >= 1 ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ 0 >= f ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ 0 >= h ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ h >= 1 /\ n2 >= 1 ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ j >= 1 ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ a >= 1 ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ g >= 1 ] (?, 1) f104(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ m2 >= 1 ] (?, 1) f104(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, o2, y) [ 0 >= m2 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f172(a, b, f, g, h, j, k, u - 1, 0) [ p2 >= 1 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f172(a, b, f, g, h, j, k, u - 1, 0) [ 0 >= p2 + 1 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ u >= 1 /\ 0 >= m2 ] (?, 1) f172(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u, y) [ 0 >= y ] (?, 1) f172(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u, y) [ y >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, n2, u, y) [ 0 >= u ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ 0 >= k ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k - 1, u, y) [ k >= 1 /\ n2 >= 1 ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k, u, y) [ k >= 1 /\ 0 >= n2 ] (?, 1) f237(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ 0 >= j ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ h >= 1 /\ 0 >= n2 ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ 0 >= g ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ 0 >= n2 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f31(a, b - 1, f, g, h, j, k, u, y) [ 0 >= m2 /\ b >= 1 ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ 0 >= a ] start location: f0 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 3: f172(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u, y) [ y >= 1 ] We thus obtain the following problem: 4: T: (?, 1) f237(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k, u, y) [ k >= 1 /\ 0 >= n2 ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k - 1, u, y) [ k >= 1 /\ n2 >= 1 ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ 0 >= k ] (?, 1) f172(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u, y) [ 0 >= y ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ 0 >= g ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ g >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, n2, u, y) [ 0 >= u ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ u >= 1 /\ 0 >= m2 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f172(a, b, f, g, h, j, k, u - 1, 0) [ 0 >= p2 + 1 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f172(a, b, f, g, h, j, k, u - 1, 0) [ p2 >= 1 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ 0 >= a ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ a >= 1 ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ 0 >= j ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ j >= 1 ] (?, 1) f104(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, o2, y) [ 0 >= m2 ] (?, 1) f104(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ m2 >= 1 ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ 0 >= f ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ f >= 1 ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ h >= 1 /\ 0 >= n2 ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ h >= 1 /\ n2 >= 1 ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ 0 >= h ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f31(a, b - 1, f, g, h, j, k, u, y) [ 0 >= m2 /\ b >= 1 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ 0 >= n2 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ n2 >= 1 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, n2, j, k, u, y) [ 0 >= b ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, n2, f, g, h, j, k, u, y) [ 0 >= m2 ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, p2, f, g, h, j, k, u, y) [ m2 >= 1 ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f237) = -5 Pol(f211) = -4 Pol(f172) = -3 Pol(f144) = -3 Pol(f83) = 1 Pol(f67) = 1 Pol(f81) = 1 Pol(f77) = 1 Pol(f104) = -1 Pol(f42) = 2 Pol(f31) = 2 Pol(f0) = 2 orients all transitions weakly and the transitions f67(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ 0 >= h ] f31(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, n2, j, k, u, y) [ 0 >= b ] strictly and produces the following problem: 5: T: (?, 1) f237(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k, u, y) [ k >= 1 /\ 0 >= n2 ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k - 1, u, y) [ k >= 1 /\ n2 >= 1 ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ 0 >= k ] (?, 1) f172(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u, y) [ 0 >= y ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ 0 >= g ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ g >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, n2, u, y) [ 0 >= u ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ u >= 1 /\ 0 >= m2 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f172(a, b, f, g, h, j, k, u - 1, 0) [ 0 >= p2 + 1 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f172(a, b, f, g, h, j, k, u - 1, 0) [ p2 >= 1 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ 0 >= a ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ a >= 1 ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ 0 >= j ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ j >= 1 ] (?, 1) f104(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, o2, y) [ 0 >= m2 ] (?, 1) f104(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ m2 >= 1 ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ 0 >= f ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ f >= 1 ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ h >= 1 /\ 0 >= n2 ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ h >= 1 /\ n2 >= 1 ] (2, 1) f67(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ 0 >= h ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f31(a, b - 1, f, g, h, j, k, u, y) [ 0 >= m2 /\ b >= 1 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ 0 >= n2 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ n2 >= 1 ] (2, 1) f31(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, n2, j, k, u, y) [ 0 >= b ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, n2, f, g, h, j, k, u, y) [ 0 >= m2 ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, p2, f, g, h, j, k, u, y) [ m2 >= 1 ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f237) = 0 Pol(f211) = 1 Pol(f172) = 2 Pol(f144) = 2 Pol(f83) = 3 Pol(f67) = 3 Pol(f81) = 3 Pol(f77) = 3 Pol(f104) = 3 Pol(f42) = 3 Pol(f31) = 3 Pol(f0) = 3 orients all transitions weakly and the transitions f211(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ 0 >= k ] f144(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, n2, u, y) [ 0 >= u ] f104(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, o2, y) [ 0 >= m2 ] strictly and produces the following problem: 6: T: (?, 1) f237(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k, u, y) [ k >= 1 /\ 0 >= n2 ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k - 1, u, y) [ k >= 1 /\ n2 >= 1 ] (3, 1) f211(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ 0 >= k ] (?, 1) f172(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u, y) [ 0 >= y ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ 0 >= g ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ g >= 1 ] (3, 1) f144(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, n2, u, y) [ 0 >= u ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ u >= 1 /\ 0 >= m2 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f172(a, b, f, g, h, j, k, u - 1, 0) [ 0 >= p2 + 1 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f172(a, b, f, g, h, j, k, u - 1, 0) [ p2 >= 1 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ 0 >= a ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ a >= 1 ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ 0 >= j ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ j >= 1 ] (3, 1) f104(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, o2, y) [ 0 >= m2 ] (?, 1) f104(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ m2 >= 1 ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ 0 >= f ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ f >= 1 ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ h >= 1 /\ 0 >= n2 ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ h >= 1 /\ n2 >= 1 ] (2, 1) f67(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ 0 >= h ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f31(a, b - 1, f, g, h, j, k, u, y) [ 0 >= m2 /\ b >= 1 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ 0 >= n2 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ n2 >= 1 ] (2, 1) f31(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, n2, j, k, u, y) [ 0 >= b ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, n2, f, g, h, j, k, u, y) [ 0 >= m2 ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, p2, f, g, h, j, k, u, y) [ m2 >= 1 ] start location: f0 leaf cost: 1 Applied AI with 'oct' on problem 6 to obtain the following invariants: For symbol f104: -X_5 >= 0 /\ -X_2 - X_5 >= 0 /\ -X_2 >= 0 For symbol f144: -X_5 >= 0 /\ -X_2 - X_5 >= 0 /\ -X_2 >= 0 For symbol f172: -X_9 >= 0 /\ X_8 - X_9 >= 0 /\ -X_5 - X_9 >= 0 /\ -X_2 - X_9 >= 0 /\ X_9 >= 0 /\ X_8 + X_9 >= 0 /\ -X_5 + X_9 >= 0 /\ -X_2 + X_9 >= 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 f211: -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 f237: -X_8 >= 0 /\ -X_7 - X_8 >= 0 /\ -X_5 - X_8 >= 0 /\ -X_2 - X_8 >= 0 /\ -X_7 >= 0 /\ -X_5 - X_7 >= 0 /\ -X_2 - X_7 >= 0 /\ -X_5 >= 0 /\ -X_2 - X_5 >= 0 /\ -X_2 >= 0 For symbol f42: X_2 >= 0 For symbol f67: -X_2 >= 0 For symbol f77: X_5 >= 0 /\ -X_2 + X_5 >= 0 /\ -X_2 >= 0 For symbol f81: X_5 >= 0 /\ -X_2 + X_5 >= 0 /\ -X_2 >= 0 For symbol f83: X_5 >= 0 /\ -X_2 + X_5 >= 0 /\ -X_2 >= 0 This yielded the following problem: 7: T: (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, p2, f, g, h, j, k, u, y) [ m2 >= 1 ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, n2, f, g, h, j, k, u, y) [ 0 >= m2 ] (2, 1) f31(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, n2, j, k, u, y) [ 0 >= b ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ n2 >= 1 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ 0 >= n2 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f31(a, b - 1, f, g, h, j, k, u, y) [ 0 >= m2 /\ b >= 1 ] (2, 1) f67(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ -b >= 0 /\ 0 >= h ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ -b >= 0 /\ h >= 1 /\ n2 >= 1 ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ -b >= 0 /\ h >= 1 /\ 0 >= n2 ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ b >= 0 /\ f >= 1 ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ b >= 0 /\ 0 >= f ] (?, 1) f104(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ m2 >= 1 ] (3, 1) f104(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, o2, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= m2 ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ j >= 1 ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ 0 >= j ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ a >= 1 ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ 0 >= a ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f172(a, b, f, g, h, j, k, u - 1, 0) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ p2 >= 1 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f172(a, b, f, g, h, j, k, u - 1, 0) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= p2 + 1 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ u >= 1 /\ 0 >= m2 ] (3, 1) f144(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, n2, u, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= u ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ g >= 1 ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ 0 >= g ] (?, 1) f172(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u, y) [ -y >= 0 /\ u - y >= 0 /\ -h - y >= 0 /\ -b - y >= 0 /\ y >= 0 /\ u + y >= 0 /\ -h + y >= 0 /\ -b + y >= 0 /\ u >= 0 /\ -h + u >= 0 /\ -b + u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= y ] (3, 1) f211(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= k ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k - 1, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ k >= 1 /\ n2 >= 1 ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ k >= 1 /\ 0 >= n2 ] (?, 1) f237(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -k - u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -k >= 0 /\ -h - k >= 0 /\ -b - k >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 ] start location: f0 leaf cost: 1 By chaining the transition f144(a, b, f, g, h, j, k, u, y) -> f172(a, b, f, g, h, j, k, u - 1, 0) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ p2 >= 1 /\ u >= 1 /\ m2 >= 1 ] with all transitions in problem 7, the following new transition is obtained: f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, 0) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ p2 >= 1 /\ u >= 1 /\ m2 >= 1 /\ 0 >= 0 /\ u - 1 >= 0 /\ -h + u - 1 >= 0 /\ -b + u - 1 >= 0 ] We thus obtain the following problem: 8: T: (?, 2) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, 0) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ p2 >= 1 /\ u >= 1 /\ m2 >= 1 /\ 0 >= 0 /\ u - 1 >= 0 /\ -h + u - 1 >= 0 /\ -b + u - 1 >= 0 ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, p2, f, g, h, j, k, u, y) [ m2 >= 1 ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, n2, f, g, h, j, k, u, y) [ 0 >= m2 ] (2, 1) f31(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, n2, j, k, u, y) [ 0 >= b ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ n2 >= 1 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ 0 >= n2 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f31(a, b - 1, f, g, h, j, k, u, y) [ 0 >= m2 /\ b >= 1 ] (2, 1) f67(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ -b >= 0 /\ 0 >= h ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ -b >= 0 /\ h >= 1 /\ n2 >= 1 ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ -b >= 0 /\ h >= 1 /\ 0 >= n2 ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ b >= 0 /\ f >= 1 ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ b >= 0 /\ 0 >= f ] (?, 1) f104(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ m2 >= 1 ] (3, 1) f104(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, o2, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= m2 ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ j >= 1 ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ 0 >= j ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ a >= 1 ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ 0 >= a ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f172(a, b, f, g, h, j, k, u - 1, 0) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= p2 + 1 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ u >= 1 /\ 0 >= m2 ] (3, 1) f144(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, n2, u, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= u ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ g >= 1 ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ 0 >= g ] (?, 1) f172(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u, y) [ -y >= 0 /\ u - y >= 0 /\ -h - y >= 0 /\ -b - y >= 0 /\ y >= 0 /\ u + y >= 0 /\ -h + y >= 0 /\ -b + y >= 0 /\ u >= 0 /\ -h + u >= 0 /\ -b + u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= y ] (3, 1) f211(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= k ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k - 1, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ k >= 1 /\ n2 >= 1 ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ k >= 1 /\ 0 >= n2 ] (?, 1) f237(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -k - u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -k >= 0 /\ -h - k >= 0 /\ -b - k >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 ] start location: f0 leaf cost: 1 By chaining the transition f144(a, b, f, g, h, j, k, u, y) -> f172(a, b, f, g, h, j, k, u - 1, 0) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= p2 + 1 /\ u >= 1 /\ m2 >= 1 ] with all transitions in problem 8, the following new transition is obtained: f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, 0) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= p2 + 1 /\ u >= 1 /\ m2 >= 1 /\ 0 >= 0 /\ u - 1 >= 0 /\ -h + u - 1 >= 0 /\ -b + u - 1 >= 0 ] We thus obtain the following problem: 9: T: (?, 2) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, 0) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= p2 + 1 /\ u >= 1 /\ m2 >= 1 /\ 0 >= 0 /\ u - 1 >= 0 /\ -h + u - 1 >= 0 /\ -b + u - 1 >= 0 ] (?, 2) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, 0) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ p2 >= 1 /\ u >= 1 /\ m2 >= 1 /\ 0 >= 0 /\ u - 1 >= 0 /\ -h + u - 1 >= 0 /\ -b + u - 1 >= 0 ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, p2, f, g, h, j, k, u, y) [ m2 >= 1 ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, n2, f, g, h, j, k, u, y) [ 0 >= m2 ] (2, 1) f31(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, n2, j, k, u, y) [ 0 >= b ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ n2 >= 1 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ 0 >= n2 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f31(a, b - 1, f, g, h, j, k, u, y) [ 0 >= m2 /\ b >= 1 ] (2, 1) f67(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ -b >= 0 /\ 0 >= h ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ -b >= 0 /\ h >= 1 /\ n2 >= 1 ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ -b >= 0 /\ h >= 1 /\ 0 >= n2 ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ b >= 0 /\ f >= 1 ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ b >= 0 /\ 0 >= f ] (?, 1) f104(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ m2 >= 1 ] (3, 1) f104(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, o2, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= m2 ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ j >= 1 ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ 0 >= j ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ a >= 1 ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ 0 >= a ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ u >= 1 /\ 0 >= m2 ] (3, 1) f144(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, n2, u, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= u ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ g >= 1 ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ 0 >= g ] (?, 1) f172(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u, y) [ -y >= 0 /\ u - y >= 0 /\ -h - y >= 0 /\ -b - y >= 0 /\ y >= 0 /\ u + y >= 0 /\ -h + y >= 0 /\ -b + y >= 0 /\ u >= 0 /\ -h + u >= 0 /\ -b + u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= y ] (3, 1) f211(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= k ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k - 1, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ k >= 1 /\ n2 >= 1 ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ k >= 1 /\ 0 >= n2 ] (?, 1) f237(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -k - u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -k >= 0 /\ -h - k >= 0 /\ -b - k >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 ] start location: f0 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 9: f172(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u, y) [ -y >= 0 /\ u - y >= 0 /\ -h - y >= 0 /\ -b - y >= 0 /\ y >= 0 /\ u + y >= 0 /\ -h + y >= 0 /\ -b + y >= 0 /\ u >= 0 /\ -h + u >= 0 /\ -b + u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= y ] We thus obtain the following problem: 10: T: (?, 1) f237(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -k - u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -k >= 0 /\ -h - k >= 0 /\ -b - k >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ k >= 1 /\ 0 >= n2 ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k - 1, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ k >= 1 /\ n2 >= 1 ] (3, 1) f211(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= k ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ 0 >= g ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ g >= 1 ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ 0 >= a ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ a >= 1 ] (?, 2) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, 0) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= p2 + 1 /\ u >= 1 /\ m2 >= 1 /\ 0 >= 0 /\ u - 1 >= 0 /\ -h + u - 1 >= 0 /\ -b + u - 1 >= 0 ] (?, 2) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, 0) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ p2 >= 1 /\ u >= 1 /\ m2 >= 1 /\ 0 >= 0 /\ u - 1 >= 0 /\ -h + u - 1 >= 0 /\ -b + u - 1 >= 0 ] (3, 1) f144(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, n2, u, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= u ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ u >= 1 /\ 0 >= m2 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ 0 >= j ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ j >= 1 ] (3, 1) f104(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, o2, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= m2 ] (?, 1) f104(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ m2 >= 1 ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ b >= 0 /\ 0 >= f ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ b >= 0 /\ f >= 1 ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ -b >= 0 /\ h >= 1 /\ 0 >= n2 ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ -b >= 0 /\ h >= 1 /\ n2 >= 1 ] (2, 1) f67(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ -b >= 0 /\ 0 >= h ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f31(a, b - 1, f, g, h, j, k, u, y) [ 0 >= m2 /\ b >= 1 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ 0 >= n2 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ n2 >= 1 ] (2, 1) f31(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, n2, j, k, u, y) [ 0 >= b ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, n2, f, g, h, j, k, u, y) [ 0 >= m2 ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, p2, f, g, h, j, k, u, y) [ m2 >= 1 ] start location: f0 leaf cost: 1 By chaining the transition f211(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= k ] with all transitions in problem 10, the following new transition is obtained: f211(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= k /\ -k - u >= 0 /\ -k >= 0 /\ -h - k >= 0 /\ -b - k >= 0 ] We thus obtain the following problem: 11: T: (3, 2) f211(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= k /\ -k - u >= 0 /\ -k >= 0 /\ -h - k >= 0 /\ -b - k >= 0 ] (?, 1) f237(a, b, f, g, h, j, k, u, y) -> f237(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -k - u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -k >= 0 /\ -h - k >= 0 /\ -b - k >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ k >= 1 /\ 0 >= n2 ] (?, 1) f211(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, k - 1, u, y) [ -u >= 0 /\ -h - u >= 0 /\ -b - u >= 0 /\ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ k >= 1 /\ n2 >= 1 ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ 0 >= g ] (?, 1) f83(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ g >= 1 ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ 0 >= a ] (?, 1) f81(a, b, f, g, h, j, k, u, y) -> f83(a, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ a >= 1 ] (?, 2) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, 0) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= p2 + 1 /\ u >= 1 /\ m2 >= 1 /\ 0 >= 0 /\ u - 1 >= 0 /\ -h + u - 1 >= 0 /\ -b + u - 1 >= 0 ] (?, 2) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, 0) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ p2 >= 1 /\ u >= 1 /\ m2 >= 1 /\ 0 >= 0 /\ u - 1 >= 0 /\ -h + u - 1 >= 0 /\ -b + u - 1 >= 0 ] (3, 1) f144(a, b, f, g, h, j, k, u, y) -> f211(a, b, f, g, h, j, n2, u, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= u ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ u >= 1 /\ 0 >= m2 ] (?, 1) f144(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, u - 1, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ u >= 1 /\ m2 >= 1 ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ 0 >= j ] (?, 1) f77(a, b, f, g, h, j, k, u, y) -> f81(m2, b, f, g, h, j, k, u, y) [ h >= 0 /\ -b + h >= 0 /\ -b >= 0 /\ j >= 1 ] (3, 1) f104(a, b, f, g, h, j, k, u, y) -> f144(a, b, f, g, h, j, k, o2, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ 0 >= m2 ] (?, 1) f104(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ -h >= 0 /\ -b - h >= 0 /\ -b >= 0 /\ m2 >= 1 ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ b >= 0 /\ 0 >= f ] (?, 1) f42(a, b, f, g, h, j, k, u, y) -> f31(a, b, f, g, h, j, k, u, y) [ b >= 0 /\ f >= 1 ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ -b >= 0 /\ h >= 1 /\ 0 >= n2 ] (?, 1) f67(a, b, f, g, h, j, k, u, y) -> f77(a, b, f, m2, h - 1, o2, k, u, y) [ -b >= 0 /\ h >= 1 /\ n2 >= 1 ] (2, 1) f67(a, b, f, g, h, j, k, u, y) -> f104(a, b, f, g, h, j, k, u, y) [ -b >= 0 /\ 0 >= h ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f31(a, b - 1, f, g, h, j, k, u, y) [ 0 >= m2 /\ b >= 1 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ 0 >= n2 ] (?, 1) f31(a, b, f, g, h, j, k, u, y) -> f42(a, b - 1, o2, g, h, j, k, u, y) [ b >= 1 /\ m2 >= 1 /\ n2 >= 1 ] (2, 1) f31(a, b, f, g, h, j, k, u, y) -> f67(a, b, f, g, n2, j, k, u, y) [ 0 >= b ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, n2, f, g, h, j, k, u, y) [ 0 >= m2 ] (1, 1) f0(a, b, f, g, h, j, k, u, y) -> f31(a, p2, f, g, h, j, k, u, y) [ m2 >= 1 ] start location: f0 leaf cost: 1 Complexity upper bound ? Time: 5.510 sec (SMT: 4.307 sec)