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, g2, h2, i2, j2) -> 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) [ 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, g2, h2, i2, j2) -> f34(a, b - 1, k2, 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) [ b >= 1 /\ 0 >= k2 ] (?, 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, g2, h2, i2, j2) -> f44(a, b - 1, k2, l2, m2, 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) [ 0 >= l2 /\ b >= 1 /\ k2 >= 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) -> 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, g2, h2, i2, j2) [ 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, g2, h2, i2, j2) -> f75(a, b, c, d, e, k2, g - 1, l2, m2, 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) [ g >= 1 /\ 0 >= l2 ] (?, 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, g2, h2, i2, j2) -> f79(k2, 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) [ 0 >= i ] (?, 1) f213(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) -> f213(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) (?, 1) f215(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) -> f218(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) (?, 1) f191(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) -> f191(a, b, c, d, e, f, g, h, i, j - 1, 1, 0, k2, 0, 0, k2, 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) [ j >= 1 ] (?, 1) f191(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) -> f213(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, 2, 0, k2, 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) [ 0 >= j /\ q = 2 ] (?, 1) f191(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) -> f213(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, 0, k2, 1, 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) [ 1 >= q /\ 0 >= j ] (?, 1) f191(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) -> f213(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, 0, k2, 1, 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) [ q >= 3 /\ 0 >= j ] (?, 1) f132(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) -> f191(a, b, c, d, e, f, g, h, i, l2, k, l, m, n, o, p, q, 0, s, t, u, 0, k2, l2, 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) [ 0 >= u ] (?, 1) f156(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) -> f132(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, 0, r, s, t, u, 0, w, x, y, y, y, 0, d1, d1, y, 0, y, d1, 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) [ y >= 1 ] (?, 1) f156(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) -> f132(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, y, a1, b1, c1, d1, e1, f1, g1, h1, d1, 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) [ 0 >= y ] (?, 1) f132(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) -> f132(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, 0, s, t, u - 1, 0, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, k2, l2, 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) [ u >= 1 /\ 0 >= k2 ] (?, 1) f132(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) -> f132(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, 0, s, t, u - 1, 0, w, x, y, m2, a1, b1, c1, 0, e1, f1, g1, h1, i1, k2, l2, n2, n2, 0, 0, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2) [ u >= 1 /\ k2 >= 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, g2, h2, i2, j2) -> f132(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, 0, s, t, l2, 0, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, k2, l2, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2) [ 0 >= p1 ] (?, 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, g2, h2, i2, j2) -> f100(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, 0, s, t, u, 0, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1 - 1, q1, r1, k2, l2, m2, k2, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2) [ p1 >= 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) -> 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, g2, h2, i2, j2) [ 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, g2, h2, i2, j2) -> 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) [ 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, g2, h2, i2, j2) -> f79(k2, 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) [ 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, g2, h2, i2, j2) -> f75(a, b, c, d, e, k2, g - 1, l2, m2, 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) [ g >= 1 /\ l2 >= 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, g2, h2, i2, j2) -> f100(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, 0, s, t, u, 0, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, l2, q1, r1, s1, t1, u1, v1, k2, l2, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2) [ 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, g2, h2, i2, j2) -> 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, c, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2) [ 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, g2, h2, i2, j2) -> 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, c, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2) [ 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, g2, h2, i2, j2) -> f44(a, b - 1, k2, l2, m2, 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) [ l2 >= 1 /\ b >= 1 /\ k2 >= 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, g2, h2, i2, j2) -> f65(a, b, c, d, e, f, l2, h, i, j, k, l, m, n, o, p, q, 0, s, 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, k2, l2, b2, c2, d2, e2, f2, g2, h2, i2, j2) [ 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) -> f34(a, m2, c, d, e, f, g, h, i, j, 0, l, m, n, o, p, 0, 0, s, 0, 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, 0, 0, k2, l2, 0, m2, h2, i2, j2) [ 0 >= l2 ] (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) -> f34(a, o2, c, d, e, f, g, h, i, j, 0, l, m, n, o, p, 0, 0, s, 0, 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, 0, 0, k2, l2, 0, o2, m2, n2, 0) [ l2 >= 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, q, u, y, p1]. We thus obtain the following problem: 2: T: (1, 1) f0(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, o2, e, f, g, i, j, 0, u, y, p1) [ l2 >= 1 ] (1, 1) f0(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, m2, e, f, g, i, j, 0, u, y, p1) [ 0 >= l2 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, l2, i, j, q, u, y, p1) [ 0 >= b ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ l2 >= 1 /\ b >= 1 /\ k2 >= 1 ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ e >= 1 ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= e ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, l2) [ 0 >= g ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ g >= 1 /\ l2 >= 1 ] (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ i >= 1 ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ a >= 1 ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ f >= 1 ] (?, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, p1 - 1) [ p1 >= 1 ] (?, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, l2, y, p1) [ 0 >= p1 ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ u >= 1 /\ k2 >= 1 ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ u >= 1 /\ 0 >= k2 ] (?, 1) f156(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= y ] (?, 1) f156(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, 0, u, y, p1) [ y >= 1 ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, l2, q, u, y, p1) [ 0 >= u ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ q >= 3 /\ 0 >= j ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ 1 >= q /\ 0 >= j ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, 2, u, y, p1) [ 0 >= j /\ q = 2 ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, j - 1, q, u, y, p1) [ j >= 1 ] (?, 1) f215(a, b, e, f, g, i, j, q, u, y, p1) -> f218(a, b, e, f, g, i, j, q, u, y, p1) (?, 1) f213(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ 0 >= i ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ g >= 1 /\ 0 >= l2 ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= f ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ 0 >= l2 /\ b >= 1 /\ k2 >= 1 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b - 1, e, f, g, i, j, q, u, y, p1) [ b >= 1 /\ 0 >= k2 ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ 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, q, u, y, p1) -> f34(a, o2, e, f, g, i, j, 0, u, y, p1) [ l2 >= 1 ] (1, 1) f0(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, m2, e, f, g, i, j, 0, u, y, p1) [ 0 >= l2 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, l2, i, j, q, u, y, p1) [ 0 >= b ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ l2 >= 1 /\ b >= 1 /\ k2 >= 1 ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ e >= 1 ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= e ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, l2) [ 0 >= g ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ g >= 1 /\ l2 >= 1 ] (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ i >= 1 ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ a >= 1 ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ f >= 1 ] (?, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, p1 - 1) [ p1 >= 1 ] (?, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, l2, y, p1) [ 0 >= p1 ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ u >= 1 /\ k2 >= 1 ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ u >= 1 /\ 0 >= k2 ] (?, 1) f156(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= y ] (?, 1) f156(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, 0, u, y, p1) [ y >= 1 ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, l2, q, u, y, p1) [ 0 >= u ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ q >= 3 /\ 0 >= j ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ 1 >= q /\ 0 >= j ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, 2, u, y, p1) [ 0 >= j /\ q = 2 ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, j - 1, q, u, y, p1) [ j >= 1 ] (?, 1) f213(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ 0 >= i ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ g >= 1 /\ 0 >= l2 ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= f ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ 0 >= l2 /\ b >= 1 /\ k2 >= 1 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b - 1, e, f, g, i, j, q, u, y, p1) [ b >= 1 /\ 0 >= k2 ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= a ] start location: f0 leaf cost: 1 Testing for reachability in the complexity graph removes the following transitions from problem 3: f156(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= y ] f156(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, 0, u, y, p1) [ y >= 1 ] We thus obtain the following problem: 4: T: (?, 1) f213(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, j - 1, q, u, y, p1) [ j >= 1 ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, 2, u, y, p1) [ 0 >= j /\ q = 2 ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ 1 >= q /\ 0 >= j ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ q >= 3 /\ 0 >= j ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= f ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ f >= 1 ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, l2, q, u, y, p1) [ 0 >= u ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ u >= 1 /\ 0 >= k2 ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ u >= 1 /\ k2 >= 1 ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= a ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ a >= 1 ] (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ 0 >= i ] (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ i >= 1 ] (?, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, l2, y, p1) [ 0 >= p1 ] (?, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, p1 - 1) [ p1 >= 1 ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= e ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ e >= 1 ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ g >= 1 /\ 0 >= l2 ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ g >= 1 /\ l2 >= 1 ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, l2) [ 0 >= g ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b - 1, e, f, g, i, j, q, u, y, p1) [ b >= 1 /\ 0 >= k2 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ 0 >= l2 /\ b >= 1 /\ k2 >= 1 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ l2 >= 1 /\ b >= 1 /\ k2 >= 1 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, l2, i, j, q, u, y, p1) [ 0 >= b ] (1, 1) f0(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, m2, e, f, g, i, j, 0, u, y, p1) [ 0 >= l2 ] (1, 1) f0(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, o2, e, f, g, i, j, 0, u, y, p1) [ l2 >= 1 ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f213) = -4 Pol(f191) = -3 Pol(f81) = 1 Pol(f65) = 1 Pol(f132) = -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, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, l2) [ 0 >= g ] f34(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, l2, i, j, q, u, y, p1) [ 0 >= b ] strictly and produces the following problem: 5: T: (?, 1) f213(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, j - 1, q, u, y, p1) [ j >= 1 ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, 2, u, y, p1) [ 0 >= j /\ q = 2 ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ 1 >= q /\ 0 >= j ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ q >= 3 /\ 0 >= j ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= f ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ f >= 1 ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, l2, q, u, y, p1) [ 0 >= u ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ u >= 1 /\ 0 >= k2 ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ u >= 1 /\ k2 >= 1 ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= a ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ a >= 1 ] (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ 0 >= i ] (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ i >= 1 ] (?, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, l2, y, p1) [ 0 >= p1 ] (?, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, p1 - 1) [ p1 >= 1 ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= e ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ e >= 1 ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ g >= 1 /\ 0 >= l2 ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ g >= 1 /\ l2 >= 1 ] (2, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, l2) [ 0 >= g ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b - 1, e, f, g, i, j, q, u, y, p1) [ b >= 1 /\ 0 >= k2 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ 0 >= l2 /\ b >= 1 /\ k2 >= 1 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ l2 >= 1 /\ b >= 1 /\ k2 >= 1 ] (2, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, l2, i, j, q, u, y, p1) [ 0 >= b ] (1, 1) f0(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, m2, e, f, g, i, j, 0, u, y, p1) [ 0 >= l2 ] (1, 1) f0(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, o2, e, f, g, i, j, 0, u, y, p1) [ l2 >= 1 ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f213) = 0 Pol(f191) = 1 Pol(f81) = 3 Pol(f65) = 3 Pol(f132) = 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 f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ 1 >= q /\ 0 >= j ] f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ q >= 3 /\ 0 >= j ] f132(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, l2, q, u, y, p1) [ 0 >= u ] f100(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, l2, y, p1) [ 0 >= p1 ] strictly and produces the following problem: 6: T: (?, 1) f213(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, j - 1, q, u, y, p1) [ j >= 1 ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, 2, u, y, p1) [ 0 >= j /\ q = 2 ] (3, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ 1 >= q /\ 0 >= j ] (3, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ q >= 3 /\ 0 >= j ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= f ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ f >= 1 ] (3, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, l2, q, u, y, p1) [ 0 >= u ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ u >= 1 /\ 0 >= k2 ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ u >= 1 /\ k2 >= 1 ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= a ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ a >= 1 ] (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ 0 >= i ] (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ i >= 1 ] (3, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, l2, y, p1) [ 0 >= p1 ] (?, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, p1 - 1) [ p1 >= 1 ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= e ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ e >= 1 ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ g >= 1 /\ 0 >= l2 ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ g >= 1 /\ l2 >= 1 ] (2, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, l2) [ 0 >= g ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b - 1, e, f, g, i, j, q, u, y, p1) [ b >= 1 /\ 0 >= k2 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ 0 >= l2 /\ b >= 1 /\ k2 >= 1 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ l2 >= 1 /\ b >= 1 /\ k2 >= 1 ] (2, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, l2, i, j, q, u, y, p1) [ 0 >= b ] (1, 1) f0(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, m2, e, f, g, i, j, 0, u, y, p1) [ 0 >= l2 ] (1, 1) f0(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, o2, e, f, g, i, j, 0, u, y, p1) [ l2 >= 1 ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f213) = 0 Pol(f191) = 1 Pol(f81) = 1 Pol(f65) = 1 Pol(f132) = 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 f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, 2, u, y, p1) [ 0 >= j /\ q = 2 ] strictly and produces the following problem: 7: T: (?, 1) f213(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, j - 1, q, u, y, p1) [ j >= 1 ] (1, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, 2, u, y, p1) [ 0 >= j /\ q = 2 ] (3, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ 1 >= q /\ 0 >= j ] (3, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ q >= 3 /\ 0 >= j ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= f ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ f >= 1 ] (3, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, l2, q, u, y, p1) [ 0 >= u ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ u >= 1 /\ 0 >= k2 ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ u >= 1 /\ k2 >= 1 ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= a ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ a >= 1 ] (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ 0 >= i ] (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ i >= 1 ] (3, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, l2, y, p1) [ 0 >= p1 ] (?, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, p1 - 1) [ p1 >= 1 ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ 0 >= e ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ e >= 1 ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ g >= 1 /\ 0 >= l2 ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ g >= 1 /\ l2 >= 1 ] (2, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, l2) [ 0 >= g ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b - 1, e, f, g, i, j, q, u, y, p1) [ b >= 1 /\ 0 >= k2 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ 0 >= l2 /\ b >= 1 /\ k2 >= 1 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ l2 >= 1 /\ b >= 1 /\ k2 >= 1 ] (2, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, l2, i, j, q, u, y, p1) [ 0 >= b ] (1, 1) f0(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, m2, e, f, g, i, j, 0, u, y, p1) [ 0 >= l2 ] (1, 1) f0(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, o2, e, f, g, i, j, 0, u, y, p1) [ l2 >= 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 f132: -X_8 >= 0 /\ -X_5 - X_8 >= 0 /\ -X_2 - X_8 >= 0 /\ -X_11 - X_8 >= 0 /\ X_8 >= 0 /\ -X_5 + X_8 >= 0 /\ -X_2 + X_8 >= 0 /\ -X_11 + X_8 >= 0 /\ -X_5 >= 0 /\ -X_2 - X_5 >= 0 /\ -X_11 - X_5 >= 0 /\ -X_2 >= 0 /\ -X_11 - X_2 >= 0 /\ -X_11 >= 0 For symbol f191: -X_9 >= 0 /\ X_8 - X_9 >= 0 /\ -X_8 - X_9 >= 0 /\ -X_5 - X_9 >= 0 /\ -X_2 - X_9 >= 0 /\ -X_11 - X_9 >= 0 /\ -X_8 >= 0 /\ -X_5 - X_8 >= 0 /\ -X_2 - X_8 >= 0 /\ -X_11 - X_8 >= 0 /\ X_8 >= 0 /\ -X_5 + X_8 >= 0 /\ -X_2 + X_8 >= 0 /\ -X_11 + X_8 >= 0 /\ -X_5 >= 0 /\ -X_2 - X_5 >= 0 /\ -X_11 - X_5 >= 0 /\ -X_2 >= 0 /\ -X_11 - X_2 >= 0 /\ -X_11 >= 0 For symbol f213: -X_9 >= 0 /\ X_8 - X_9 >= 0 /\ -X_8 - X_9 >= 0 /\ -X_7 - X_9 >= 0 /\ -X_5 - X_9 >= 0 /\ -X_2 - X_9 >= 0 /\ -X_11 - X_9 >= 0 /\ -X_8 >= 0 /\ -X_7 - X_8 >= 0 /\ -X_5 - X_8 >= 0 /\ -X_2 - X_8 >= 0 /\ -X_11 - X_8 >= 0 /\ X_8 >= 0 /\ -X_7 + X_8 >= 0 /\ -X_5 + X_8 >= 0 /\ -X_2 + X_8 >= 0 /\ -X_11 + X_8 >= 0 /\ -X_7 >= 0 /\ -X_5 - X_7 >= 0 /\ -X_2 - X_7 >= 0 /\ -X_11 - X_7 >= 0 /\ -X_5 >= 0 /\ -X_2 - X_5 >= 0 /\ -X_11 - X_5 >= 0 /\ -X_2 >= 0 /\ -X_11 - X_2 >= 0 /\ -X_11 >= 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, q, u, y, p1) -> f34(a, o2, e, f, g, i, j, 0, u, y, p1) [ l2 >= 1 ] (1, 1) f0(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, m2, e, f, g, i, j, 0, u, y, p1) [ 0 >= l2 ] (2, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, l2, i, j, q, u, y, p1) [ -q >= 0 /\ q >= 0 /\ 0 >= b ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ q >= 0 /\ l2 >= 1 /\ b >= 1 /\ k2 >= 1 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ q >= 0 /\ 0 >= l2 /\ b >= 1 /\ k2 >= 1 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b - 1, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ q >= 0 /\ b >= 1 /\ 0 >= k2 ] (2, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, l2) [ -q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ -b + q >= 0 /\ -b >= 0 /\ 0 >= g ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ -q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ -b + q >= 0 /\ -b >= 0 /\ g >= 1 /\ l2 >= 1 ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ -q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ -b + q >= 0 /\ -b >= 0 /\ g >= 1 /\ 0 >= l2 ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ b - q >= 0 /\ q >= 0 /\ b + q >= 0 /\ b >= 0 /\ e >= 1 ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ b - q >= 0 /\ q >= 0 /\ b + q >= 0 /\ b >= 0 /\ 0 >= e ] (?, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, p1 - 1) [ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -b >= 0 /\ p1 >= 1 ] (3, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, l2, y, p1) [ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -b >= 0 /\ 0 >= p1 ] (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ i >= 1 ] (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= i ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ a >= 1 ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= a ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ u >= 1 /\ k2 >= 1 ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ u >= 1 /\ 0 >= k2 ] (3, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, l2, q, u, y, p1) [ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ 0 >= u ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ f >= 1 ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= f ] (3, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ -u >= 0 /\ q - u >= 0 /\ -q - u >= 0 /\ -g - u >= 0 /\ -b - u >= 0 /\ -p1 - u >= 0 /\ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ q >= 3 /\ 0 >= j ] (3, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ -u >= 0 /\ q - u >= 0 /\ -q - u >= 0 /\ -g - u >= 0 /\ -b - u >= 0 /\ -p1 - u >= 0 /\ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ 1 >= q /\ 0 >= j ] (1, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, 2, u, y, p1) [ -u >= 0 /\ q - u >= 0 /\ -q - u >= 0 /\ -g - u >= 0 /\ -b - u >= 0 /\ -p1 - u >= 0 /\ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ 0 >= j /\ q = 2 ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, j - 1, q, u, y, p1) [ -u >= 0 /\ q - u >= 0 /\ -q - u >= 0 /\ -g - u >= 0 /\ -b - u >= 0 /\ -p1 - u >= 0 /\ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ j >= 1 ] (?, 1) f213(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ -u >= 0 /\ q - u >= 0 /\ -q - u >= 0 /\ -j - u >= 0 /\ -g - u >= 0 /\ -b - u >= 0 /\ -p1 - u >= 0 /\ -q >= 0 /\ -j - q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -j + q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -j >= 0 /\ -g - j >= 0 /\ -b - j >= 0 /\ -p1 - j >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 ] start location: f0 leaf cost: 1 Testing for unsatisfiable constraints removes the following transitions from problem 8: f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ -u >= 0 /\ q - u >= 0 /\ -q - u >= 0 /\ -g - u >= 0 /\ -b - u >= 0 /\ -p1 - u >= 0 /\ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ q >= 3 /\ 0 >= j ] f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, 2, u, y, p1) [ -u >= 0 /\ q - u >= 0 /\ -q - u >= 0 /\ -g - u >= 0 /\ -b - u >= 0 /\ -p1 - u >= 0 /\ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ 0 >= j /\ q = 2 ] We thus obtain the following problem: 9: T: (1, 1) f0(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, o2, e, f, g, i, j, 0, u, y, p1) [ l2 >= 1 ] (1, 1) f0(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, m2, e, f, g, i, j, 0, u, y, p1) [ 0 >= l2 ] (2, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, l2, i, j, q, u, y, p1) [ -q >= 0 /\ q >= 0 /\ 0 >= b ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ q >= 0 /\ l2 >= 1 /\ b >= 1 /\ k2 >= 1 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ q >= 0 /\ 0 >= l2 /\ b >= 1 /\ k2 >= 1 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b - 1, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ q >= 0 /\ b >= 1 /\ 0 >= k2 ] (2, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, l2) [ -q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ -b + q >= 0 /\ -b >= 0 /\ 0 >= g ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ -q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ -b + q >= 0 /\ -b >= 0 /\ g >= 1 /\ l2 >= 1 ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ -q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ -b + q >= 0 /\ -b >= 0 /\ g >= 1 /\ 0 >= l2 ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ b - q >= 0 /\ q >= 0 /\ b + q >= 0 /\ b >= 0 /\ e >= 1 ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ b - q >= 0 /\ q >= 0 /\ b + q >= 0 /\ b >= 0 /\ 0 >= e ] (?, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, p1 - 1) [ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -b >= 0 /\ p1 >= 1 ] (3, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, l2, y, p1) [ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -b >= 0 /\ 0 >= p1 ] (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ i >= 1 ] (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= i ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ a >= 1 ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= a ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ u >= 1 /\ k2 >= 1 ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ u >= 1 /\ 0 >= k2 ] (3, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, l2, q, u, y, p1) [ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ 0 >= u ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ f >= 1 ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= f ] (3, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ -u >= 0 /\ q - u >= 0 /\ -q - u >= 0 /\ -g - u >= 0 /\ -b - u >= 0 /\ -p1 - u >= 0 /\ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ 1 >= q /\ 0 >= j ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, j - 1, q, u, y, p1) [ -u >= 0 /\ q - u >= 0 /\ -q - u >= 0 /\ -g - u >= 0 /\ -b - u >= 0 /\ -p1 - u >= 0 /\ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ j >= 1 ] (?, 1) f213(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ -u >= 0 /\ q - u >= 0 /\ -q - u >= 0 /\ -j - u >= 0 /\ -g - u >= 0 /\ -b - u >= 0 /\ -p1 - u >= 0 /\ -q >= 0 /\ -j - q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -j + q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -j >= 0 /\ -g - j >= 0 /\ -b - j >= 0 /\ -p1 - j >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 ] start location: f0 leaf cost: 1 By chaining the transition f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ -u >= 0 /\ q - u >= 0 /\ -q - u >= 0 /\ -g - u >= 0 /\ -b - u >= 0 /\ -p1 - u >= 0 /\ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ 1 >= q /\ 0 >= j ] with all transitions in problem 9, the following new transition is obtained: f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ -u >= 0 /\ q - u >= 0 /\ -q - u >= 0 /\ -g - u >= 0 /\ -b - u >= 0 /\ -p1 - u >= 0 /\ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ 1 >= q /\ 0 >= j /\ -j - u >= 0 /\ -j - q >= 0 /\ -j + q >= 0 /\ -j >= 0 /\ -g - j >= 0 /\ -b - j >= 0 /\ -p1 - j >= 0 ] We thus obtain the following problem: 10: T: (3, 2) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ -u >= 0 /\ q - u >= 0 /\ -q - u >= 0 /\ -g - u >= 0 /\ -b - u >= 0 /\ -p1 - u >= 0 /\ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ 1 >= q /\ 0 >= j /\ -j - u >= 0 /\ -j - q >= 0 /\ -j + q >= 0 /\ -j >= 0 /\ -g - j >= 0 /\ -b - j >= 0 /\ -p1 - j >= 0 ] (1, 1) f0(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, o2, e, f, g, i, j, 0, u, y, p1) [ l2 >= 1 ] (1, 1) f0(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, m2, e, f, g, i, j, 0, u, y, p1) [ 0 >= l2 ] (2, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, l2, i, j, q, u, y, p1) [ -q >= 0 /\ q >= 0 /\ 0 >= b ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ q >= 0 /\ l2 >= 1 /\ b >= 1 /\ k2 >= 1 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f44(a, b - 1, m2, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ q >= 0 /\ 0 >= l2 /\ b >= 1 /\ k2 >= 1 ] (?, 1) f34(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b - 1, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ q >= 0 /\ b >= 1 /\ 0 >= k2 ] (2, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, l2) [ -q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ -b + q >= 0 /\ -b >= 0 /\ 0 >= g ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ -q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ -b + q >= 0 /\ -b >= 0 /\ g >= 1 /\ l2 >= 1 ] (?, 1) f65(a, b, e, f, g, i, j, q, u, y, p1) -> f75(a, b, e, k2, g - 1, m2, j, q, u, y, p1) [ -q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ -b + q >= 0 /\ -b >= 0 /\ g >= 1 /\ 0 >= l2 ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ b - q >= 0 /\ q >= 0 /\ b + q >= 0 /\ b >= 0 /\ e >= 1 ] (?, 1) f44(a, b, e, f, g, i, j, q, u, y, p1) -> f34(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ b - q >= 0 /\ q >= 0 /\ b + q >= 0 /\ b >= 0 /\ 0 >= e ] (?, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f100(a, b, e, f, g, i, j, q, u, y, p1 - 1) [ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -b >= 0 /\ p1 >= 1 ] (3, 1) f100(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, l2, y, p1) [ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -b >= 0 /\ 0 >= p1 ] (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ i >= 1 ] (?, 1) f75(a, b, e, f, g, i, j, q, u, y, p1) -> f79(k2, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= i ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ a >= 1 ] (?, 1) f79(a, b, e, f, g, i, j, q, u, y, p1) -> f81(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= a ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ u >= 1 /\ k2 >= 1 ] (?, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f132(a, b, e, f, g, i, j, q, u - 1, y, p1) [ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ u >= 1 /\ 0 >= k2 ] (3, 1) f132(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, l2, q, u, y, p1) [ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ 0 >= u ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ f >= 1 ] (?, 1) f81(a, b, e, f, g, i, j, q, u, y, p1) -> f65(a, b, e, f, g, i, j, q, u, y, p1) [ -q >= 0 /\ g - q >= 0 /\ -b - q >= 0 /\ q >= 0 /\ g + q >= 0 /\ -b + q >= 0 /\ g >= 0 /\ -b + g >= 0 /\ -b >= 0 /\ 0 >= f ] (?, 1) f191(a, b, e, f, g, i, j, q, u, y, p1) -> f191(a, b, e, f, g, i, j - 1, q, u, y, p1) [ -u >= 0 /\ q - u >= 0 /\ -q - u >= 0 /\ -g - u >= 0 /\ -b - u >= 0 /\ -p1 - u >= 0 /\ -q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 /\ j >= 1 ] (?, 1) f213(a, b, e, f, g, i, j, q, u, y, p1) -> f213(a, b, e, f, g, i, j, q, u, y, p1) [ -u >= 0 /\ q - u >= 0 /\ -q - u >= 0 /\ -j - u >= 0 /\ -g - u >= 0 /\ -b - u >= 0 /\ -p1 - u >= 0 /\ -q >= 0 /\ -j - q >= 0 /\ -g - q >= 0 /\ -b - q >= 0 /\ -p1 - q >= 0 /\ q >= 0 /\ -j + q >= 0 /\ -g + q >= 0 /\ -b + q >= 0 /\ -p1 + q >= 0 /\ -j >= 0 /\ -g - j >= 0 /\ -b - j >= 0 /\ -p1 - j >= 0 /\ -g >= 0 /\ -b - g >= 0 /\ -p1 - g >= 0 /\ -b >= 0 /\ -p1 - b >= 0 /\ -p1 >= 0 ] start location: f0 leaf cost: 1 Complexity upper bound ? Time: 5.918 sec (SMT: 4.708 sec)