MAYBE Initial complexity problem: 1: T: (?, 1) f154(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f166(7, 7, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ a = 7 ] (?, 1) f154(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f156(a, a, u3, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ 6 >= a ] (?, 1) f154(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f156(a, a, u3, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ a >= 8 ] (?, 1) f159(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f159(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) (?, 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, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f159(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ d >= 1 /\ c >= 1 /\ e >= 1 ] (?, 1) f187(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f190(a, 7, c, d, e, u3, u3, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ b = 7 ] (?, 1) f190(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f200(a, b, c, d, e, f, g, u3, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ 0 >= g ] (?, 1) f200(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f115(a, b, c, d, e, f, g, h, h, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ h = i ] (?, 1) f187(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f115(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ 6 >= b ] (?, 1) f187(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f115(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ b >= 8 ] (?, 1) f200(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f115(a, b, c, d, e, f, g, h, i, 1, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ h >= i + 1 ] (?, 1) f200(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f115(a, b, c, d, e, f, g, h, i, 1, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ i >= h + 1 ] (?, 1) f208(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f208(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) (?, 1) f161(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> 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, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) (?, 1) f210(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> 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, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) (?, 1) f190(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f200(a, b, c, d, e, f, g, v3, i, j, 1, g, u3, g, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ g >= 1 ] (?, 1) f177(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f187(a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, p, p, u3, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ 3 >= b ] (?, 1) f177(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f187(a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, p, p, u3, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ b >= 5 ] (?, 1) f177(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f190(a, 4, c, d, e, w3, w3, h, i, j, k, l, m, n, p, p, p, u3, 1, v3, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ b = 4 ] (?, 1) f166(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f177(a, u3, c, d, e, f, g, h, i, j, k, l, m, n, o, v3, q, r, s, t, u, v, 1, v3, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ u >= v + 1 ] (?, 1) f166(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f177(a, u3, c, d, e, f, g, h, i, j, k, l, m, n, o, v3, q, r, s, t, u, 0, 1, v3, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ v >= 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, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f166(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, 1, u3, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ 0 >= c ] (?, 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, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f154(v3, 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, u3, -1, v3, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ c >= 1 /\ 0 >= e ] (?, 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, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f154(v3, 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, u3, -1, v3, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ 0 >= d /\ c >= 1 /\ e >= 1 ] (?, 1) f133(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f154(x3, 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, w3, -1, x3, d1, 0, u3, u3, u3, u3, v3, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ 0 >= d1 ] (?, 1) f133(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f154(x3, 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, w3, -1, x3, d1, 0, u3, u3, u3, u3, v3, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ d1 >= 2 ] (?, 1) f133(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f177(a, u3, c, d, e, f, g, h, i, j, k, l, m, n, o, x3, q, r, s, t, u, v, k1, x3, y, z, a1, b1, c1, 1, 0, v3, v3, v3, v3, w3, 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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ d1 = 1 ] (?, 1) f115(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f133(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, u3, v3, 1, 0, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ 0 >= j /\ 0 >= l1 ] (?, 1) f115(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f133(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, u3, v3, 1, 0, q1 + 1, q1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ l1 >= q1 + 1 /\ 0 >= j /\ l1 >= 1 ] (?, 1) f115(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f133(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, u3, w3, 1, 0, q1 + 1, q1, 0, v3, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ l1 >= 1 /\ 0 >= j /\ q1 >= l1 ] (?, 1) f115(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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f208(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, 0, u3, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ j >= 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, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> 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 - 1, 0, 6, 1, 5, w, u3, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ w1 >= 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, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f115(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, 8, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) [ 0 >= w1 ] (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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f100(a, 7, c, d, e, f, g, h, i, 0, 0, l, m, n, o, p, q, r, s, t, u, 0, v3, x, y, z, a1, b1, c1, y3, 0, f1, g1, h1, i1, j1, v3, l1, m1, n1, o1, p1, 0, r1, s1, t1, u1, v1, y3, x1, y1, z1, a2, b2, c2, 9, u3, 0, 0, 0, 0, 0, 256, 0, u3, w3, w3, w3, x3, z3, a4, b4, 0, c4, d4, e4, f4, g4, h4, 0, 0, i4, j4, 7, 7, k4, l4, m4, u3, 0, n4, 1, 0, d1, o4, 0, s3, t3) [ v3 >= 1 /\ y3 >= 1 /\ u3 >= 1 ] (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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f100(a, k4, c, d, e, f, g, h, i, 0, 0, l, m, n, o, p, q, r, s, t, u, 0, v3, x, y, z, a1, b1, c1, p4, 0, f1, g1, h1, i1, j1, v3, l1, m1, n1, o1, p1, 0, r1, s1, t1, u1, v1, p4, x1, y1, z1, a2, b2, c2, 9, u3, 0, 0, 0, 0, 0, 256, 0, u3, w3, w3, w3, x3, z3, a4, b4, 0, c4, d4, e4, f4, g4, h4, 0, 0, i4, j4, k4, k4, m4, n4, o4, u3, 0, y3, 1, 0, d1, q4, 0, 1, l4) [ v3 >= 1 /\ u3 >= 1 /\ 6 >= k4 /\ p4 >= 1 ] (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, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2, a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3) -> f100(a, k4, c, d, e, f, g, h, i, 0, 0, l, m, n, o, p, q, r, s, t, u, 0, v3, x, y, z, a1, b1, c1, p4, 0, f1, g1, h1, i1, j1, v3, l1, m1, n1, o1, p1, 0, r1, s1, t1, u1, v1, p4, x1, y1, z1, a2, b2, c2, 9, u3, 0, 0, 0, 0, 0, 256, 0, u3, w3, w3, w3, x3, z3, a4, b4, 0, c4, d4, e4, f4, g4, h4, 0, 0, i4, j4, k4, k4, m4, n4, o4, u3, 0, y3, 1, 0, d1, q4, 0, 1, l4) [ v3 >= 1 /\ u3 >= 1 /\ k4 >= 8 /\ p4 >= 1 ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1]. We thus obtain the following problem: 2: T: (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ k4 >= 8 /\ p4 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ 6 >= k4 /\ p4 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, 7, c, d, e, g, h, i, 0, u, 0, y3, l1, 0, y3) [ v3 >= 1 /\ y3 >= 1 /\ u3 >= 1 ] (?, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= w1 ] (?, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1 - 1) [ w1 >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ j >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ l1 >= 1 /\ 0 >= j /\ q1 >= l1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ l1 >= q1 + 1 /\ 0 >= j /\ l1 >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= j /\ 0 >= l1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, 1, l1, q1, w1) [ d1 = 1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ d1 >= 2 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= d1 ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= d /\ c >= 1 /\ e >= 1 ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ c >= 1 /\ 0 >= e ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= c ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, 0, d1, l1, q1, w1) [ v >= u ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ u >= v + 1 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 4, c, d, e, w3, h, i, j, u, v, d1, l1, q1, w1) [ b = 4 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ b >= 5 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 3 >= b ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, v3, i, j, u, v, d1, l1, q1, w1) [ g >= 1 ] (?, 1) f210(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f213(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) (?, 1) f161(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f213(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) (?, 1) f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ i >= h + 1 ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ h >= i + 1 ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ b >= 8 ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 6 >= b ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, h, j, u, v, d1, l1, q1, w1) [ h = i ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, u3, i, j, u, v, d1, l1, q1, w1) [ 0 >= g ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 7, c, d, e, u3, h, i, j, u, v, d1, l1, q1, w1) [ b = 7 ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ d >= 1 /\ c >= 1 /\ e >= 1 ] (?, 1) f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ a >= 8 ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 6 >= a ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(7, 7, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ a = 7 ] 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, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ k4 >= 8 /\ p4 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ 6 >= k4 /\ p4 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, 7, c, d, e, g, h, i, 0, u, 0, y3, l1, 0, y3) [ v3 >= 1 /\ y3 >= 1 /\ u3 >= 1 ] (?, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= w1 ] (?, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1 - 1) [ w1 >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ j >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ l1 >= 1 /\ 0 >= j /\ q1 >= l1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ l1 >= q1 + 1 /\ 0 >= j /\ l1 >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= j /\ 0 >= l1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, 1, l1, q1, w1) [ d1 = 1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ d1 >= 2 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= d1 ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= d /\ c >= 1 /\ e >= 1 ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ c >= 1 /\ 0 >= e ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= c ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, 0, d1, l1, q1, w1) [ v >= u ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ u >= v + 1 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 4, c, d, e, w3, h, i, j, u, v, d1, l1, q1, w1) [ b = 4 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ b >= 5 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 3 >= b ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, v3, i, j, u, v, d1, l1, q1, w1) [ g >= 1 ] (?, 1) f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ i >= h + 1 ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ h >= i + 1 ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ b >= 8 ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 6 >= b ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, h, j, u, v, d1, l1, q1, w1) [ h = i ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, u3, i, j, u, v, d1, l1, q1, w1) [ 0 >= g ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 7, c, d, e, u3, h, i, j, u, v, d1, l1, q1, w1) [ b = 7 ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ d >= 1 /\ c >= 1 /\ e >= 1 ] (?, 1) f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ a >= 8 ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 6 >= a ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(7, 7, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ a = 7 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f0) = 1 Pol(f100) = 1 Pol(f115) = -8 Pol(f208) = -9 Pol(f133) = -8 Pol(f177) = -8 Pol(f154) = -8 Pol(f156) = -8 Pol(f166) = -8 Pol(f190) = -8 Pol(f187) = -8 Pol(f200) = -8 Pol(f159) = -9 orients all transitions weakly and the transition f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= w1 ] strictly and produces the following problem: 4: T: (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ k4 >= 8 /\ p4 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ 6 >= k4 /\ p4 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, 7, c, d, e, g, h, i, 0, u, 0, y3, l1, 0, y3) [ v3 >= 1 /\ y3 >= 1 /\ u3 >= 1 ] (1, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= w1 ] (?, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1 - 1) [ w1 >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ j >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ l1 >= 1 /\ 0 >= j /\ q1 >= l1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ l1 >= q1 + 1 /\ 0 >= j /\ l1 >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= j /\ 0 >= l1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, 1, l1, q1, w1) [ d1 = 1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ d1 >= 2 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= d1 ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= d /\ c >= 1 /\ e >= 1 ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ c >= 1 /\ 0 >= e ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= c ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, 0, d1, l1, q1, w1) [ v >= u ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ u >= v + 1 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 4, c, d, e, w3, h, i, j, u, v, d1, l1, q1, w1) [ b = 4 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ b >= 5 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 3 >= b ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, v3, i, j, u, v, d1, l1, q1, w1) [ g >= 1 ] (?, 1) f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ i >= h + 1 ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ h >= i + 1 ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ b >= 8 ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 6 >= b ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, h, j, u, v, d1, l1, q1, w1) [ h = i ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, u3, i, j, u, v, d1, l1, q1, w1) [ 0 >= g ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 7, c, d, e, u3, h, i, j, u, v, d1, l1, q1, w1) [ b = 7 ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ d >= 1 /\ c >= 1 /\ e >= 1 ] (?, 1) f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ a >= 8 ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 6 >= a ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(7, 7, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ a = 7 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f0) = 1 Pol(f100) = 1 Pol(f115) = 1 Pol(f208) = 0 Pol(f133) = 1 Pol(f177) = 1 Pol(f154) = 1 Pol(f156) = 1 Pol(f166) = 1 Pol(f190) = 1 Pol(f187) = 1 Pol(f200) = 1 Pol(f159) = 0 orients all transitions weakly and the transition f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ d >= 1 /\ c >= 1 /\ e >= 1 ] strictly and produces the following problem: 5: T: (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ k4 >= 8 /\ p4 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ 6 >= k4 /\ p4 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, 7, c, d, e, g, h, i, 0, u, 0, y3, l1, 0, y3) [ v3 >= 1 /\ y3 >= 1 /\ u3 >= 1 ] (1, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= w1 ] (?, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1 - 1) [ w1 >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ j >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ l1 >= 1 /\ 0 >= j /\ q1 >= l1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ l1 >= q1 + 1 /\ 0 >= j /\ l1 >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= j /\ 0 >= l1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, 1, l1, q1, w1) [ d1 = 1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ d1 >= 2 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= d1 ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= d /\ c >= 1 /\ e >= 1 ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ c >= 1 /\ 0 >= e ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= c ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, 0, d1, l1, q1, w1) [ v >= u ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ u >= v + 1 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 4, c, d, e, w3, h, i, j, u, v, d1, l1, q1, w1) [ b = 4 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ b >= 5 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 3 >= b ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, v3, i, j, u, v, d1, l1, q1, w1) [ g >= 1 ] (?, 1) f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ i >= h + 1 ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ h >= i + 1 ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ b >= 8 ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 6 >= b ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, h, j, u, v, d1, l1, q1, w1) [ h = i ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, u3, i, j, u, v, d1, l1, q1, w1) [ 0 >= g ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 7, c, d, e, u3, h, i, j, u, v, d1, l1, q1, w1) [ b = 7 ] (1, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ d >= 1 /\ c >= 1 /\ e >= 1 ] (?, 1) f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ a >= 8 ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 6 >= a ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(7, 7, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ a = 7 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f0) = 1 Pol(f100) = 1 Pol(f115) = 1 Pol(f208) = 0 Pol(f133) = 1 Pol(f177) = 1 Pol(f154) = 1 Pol(f156) = 1 Pol(f166) = 1 Pol(f190) = 1 Pol(f187) = 1 Pol(f200) = 1 Pol(f159) = 1 orients all transitions weakly and the transition f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ j >= 1 ] strictly and produces the following problem: 6: T: (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ k4 >= 8 /\ p4 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ 6 >= k4 /\ p4 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, 7, c, d, e, g, h, i, 0, u, 0, y3, l1, 0, y3) [ v3 >= 1 /\ y3 >= 1 /\ u3 >= 1 ] (1, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= w1 ] (?, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1 - 1) [ w1 >= 1 ] (1, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ j >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ l1 >= 1 /\ 0 >= j /\ q1 >= l1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ l1 >= q1 + 1 /\ 0 >= j /\ l1 >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= j /\ 0 >= l1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, 1, l1, q1, w1) [ d1 = 1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ d1 >= 2 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= d1 ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= d /\ c >= 1 /\ e >= 1 ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ c >= 1 /\ 0 >= e ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= c ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, 0, d1, l1, q1, w1) [ v >= u ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ u >= v + 1 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 4, c, d, e, w3, h, i, j, u, v, d1, l1, q1, w1) [ b = 4 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ b >= 5 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 3 >= b ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, v3, i, j, u, v, d1, l1, q1, w1) [ g >= 1 ] (?, 1) f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ i >= h + 1 ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ h >= i + 1 ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ b >= 8 ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 6 >= b ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, h, j, u, v, d1, l1, q1, w1) [ h = i ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, u3, i, j, u, v, d1, l1, q1, w1) [ 0 >= g ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 7, c, d, e, u3, h, i, j, u, v, d1, l1, q1, w1) [ b = 7 ] (1, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ d >= 1 /\ c >= 1 /\ e >= 1 ] (?, 1) f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ a >= 8 ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 6 >= a ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(7, 7, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ a = 7 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f0) = 15*V_13 - 14 Pol(f100) = 15*V_13 - 2*V_14 - 14 Pol(f115) = 15*V_13 - 2*V_14 - 14 Pol(f208) = 15*V_13 - 2*V_14 - 14 Pol(f133) = 15*V_13 - 2*V_14 - 14 Pol(f177) = 15*V_13 - 2*V_14 - 14 Pol(f154) = 15*V_13 - 2*V_14 - 14 Pol(f156) = 15*V_13 - 2*V_14 - 14 Pol(f166) = 15*V_13 - 2*V_14 - 14 Pol(f190) = 15*V_13 - 2*V_14 - 14 Pol(f187) = 15*V_13 - 2*V_14 - 14 Pol(f200) = 15*V_13 - 2*V_14 - 14 Pol(f159) = 15*V_13 - 2*V_14 - 14 orients all transitions weakly and the transition f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ l1 >= q1 + 1 /\ 0 >= j /\ l1 >= 1 ] strictly and produces the following problem: 7: T: (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ k4 >= 8 /\ p4 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ 6 >= k4 /\ p4 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, 7, c, d, e, g, h, i, 0, u, 0, y3, l1, 0, y3) [ v3 >= 1 /\ y3 >= 1 /\ u3 >= 1 ] (1, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= w1 ] (?, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1 - 1) [ w1 >= 1 ] (1, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ j >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ l1 >= 1 /\ 0 >= j /\ q1 >= l1 ] (15*l1 + 14, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ l1 >= q1 + 1 /\ 0 >= j /\ l1 >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= j /\ 0 >= l1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, 1, l1, q1, w1) [ d1 = 1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ d1 >= 2 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= d1 ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= d /\ c >= 1 /\ e >= 1 ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ c >= 1 /\ 0 >= e ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 0 >= c ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, 0, d1, l1, q1, w1) [ v >= u ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ u >= v + 1 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 4, c, d, e, w3, h, i, j, u, v, d1, l1, q1, w1) [ b = 4 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ b >= 5 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 3 >= b ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, v3, i, j, u, v, d1, l1, q1, w1) [ g >= 1 ] (?, 1) f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ i >= h + 1 ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ h >= i + 1 ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ b >= 8 ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 6 >= b ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, h, j, u, v, d1, l1, q1, w1) [ h = i ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, u3, i, j, u, v, d1, l1, q1, w1) [ 0 >= g ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 7, c, d, e, u3, h, i, j, u, v, d1, l1, q1, w1) [ b = 7 ] (1, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ d >= 1 /\ c >= 1 /\ e >= 1 ] (?, 1) f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ a >= 8 ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ 6 >= a ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(7, 7, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ a = 7 ] start location: f0 leaf cost: 2 Applied AI with 'oct' on problem 7 to obtain the following invariants: For symbol f100: -X_9 >= 0 /\ X_14 - X_9 >= 0 /\ -X_14 - X_9 >= 0 /\ X_11 - X_9 >= 0 /\ -X_11 - X_9 >= 0 /\ X_9 >= 0 /\ X_14 + X_9 >= 0 /\ -X_14 + X_9 >= 0 /\ X_11 + X_9 >= 0 /\ -X_11 + X_9 >= 0 /\ -X_14 >= 0 /\ X_11 - X_14 >= 0 /\ -X_11 - X_14 >= 0 /\ X_14 >= 0 /\ X_11 + X_14 >= 0 /\ -X_11 + X_14 >= 0 /\ -X_11 >= 0 /\ X_11 >= 0 For symbol f115: X_9 >= 0 /\ -X_15 + X_9 >= 0 /\ X_14 + X_9 >= 0 /\ X_11 + X_9 >= 0 /\ -X_11 + X_9 >= 0 /\ -X_15 >= 0 /\ X_14 - X_15 >= 0 /\ X_11 - X_15 >= 0 /\ -X_11 - X_15 >= 0 /\ X_14 >= 0 /\ X_11 + X_14 >= 0 /\ -X_11 + X_14 >= 0 /\ -X_11 >= 0 /\ X_11 >= 0 For symbol f133: -X_9 >= 0 /\ -X_15 - X_9 >= 0 /\ X_14 - X_9 >= 0 /\ X_11 - X_9 >= 0 /\ -X_11 - X_9 >= 0 /\ X_9 >= 0 /\ -X_15 + X_9 >= 0 /\ X_14 + X_9 >= 0 /\ X_11 + X_9 >= 0 /\ -X_11 + X_9 >= 0 /\ -X_15 >= 0 /\ X_14 - X_15 >= 0 /\ X_11 - X_15 >= 0 /\ -X_11 - X_15 >= 0 /\ X_14 >= 0 /\ X_11 + X_14 >= 0 /\ -X_11 + X_14 >= 0 /\ -X_11 >= 0 /\ X_11 >= 0 For symbol f154: -X_9 >= 0 /\ -X_15 - X_9 >= 0 /\ X_14 - X_9 >= 0 /\ X_11 - X_9 >= 0 /\ -X_11 - X_9 >= 0 /\ X_9 >= 0 /\ -X_15 + X_9 >= 0 /\ X_14 + X_9 >= 0 /\ X_11 + X_9 >= 0 /\ -X_11 + X_9 >= 0 /\ -X_15 >= 0 /\ X_14 - X_15 >= 0 /\ X_11 - X_15 >= 0 /\ -X_11 - X_15 >= 0 /\ X_14 >= 0 /\ X_11 + X_14 >= 0 /\ -X_11 + X_14 >= 0 /\ -X_11 >= 0 /\ X_11 >= 0 For symbol f156: -X_9 >= 0 /\ -X_15 - X_9 >= 0 /\ X_14 - X_9 >= 0 /\ X_11 - X_9 >= 0 /\ -X_11 - X_9 >= 0 /\ X_9 >= 0 /\ -X_15 + X_9 >= 0 /\ X_14 + X_9 >= 0 /\ X_11 + X_9 >= 0 /\ -X_11 + X_9 >= 0 /\ X_1 - X_2 >= 0 /\ -X_1 + X_2 >= 0 /\ -X_15 >= 0 /\ X_14 - X_15 >= 0 /\ X_11 - X_15 >= 0 /\ -X_11 - X_15 >= 0 /\ X_14 >= 0 /\ X_11 + X_14 >= 0 /\ -X_11 + X_14 >= 0 /\ -X_11 >= 0 /\ X_11 >= 0 For symbol f159: -X_9 >= 0 /\ X_5 - X_9 - 1 >= 0 /\ X_4 - X_9 - 1 >= 0 /\ X_3 - X_9 - 1 >= 0 /\ -X_15 - X_9 >= 0 /\ X_14 - X_9 >= 0 /\ X_11 - X_9 >= 0 /\ -X_11 - X_9 >= 0 /\ X_9 >= 0 /\ X_5 + X_9 - 1 >= 0 /\ X_4 + X_9 - 1 >= 0 /\ X_3 + X_9 - 1 >= 0 /\ -X_15 + X_9 >= 0 /\ X_14 + X_9 >= 0 /\ X_11 + X_9 >= 0 /\ -X_11 + X_9 >= 0 /\ X_5 - 1 >= 0 /\ X_4 + X_5 - 2 >= 0 /\ X_3 + X_5 - 2 >= 0 /\ -X_15 + X_5 - 1 >= 0 /\ X_14 + X_5 - 1 >= 0 /\ X_11 + X_5 - 1 >= 0 /\ -X_11 + X_5 - 1 >= 0 /\ X_4 - 1 >= 0 /\ X_3 + X_4 - 2 >= 0 /\ -X_15 + X_4 - 1 >= 0 /\ X_14 + X_4 - 1 >= 0 /\ X_11 + X_4 - 1 >= 0 /\ -X_11 + X_4 - 1 >= 0 /\ X_3 - 1 >= 0 /\ -X_15 + X_3 - 1 >= 0 /\ X_14 + X_3 - 1 >= 0 /\ X_11 + X_3 - 1 >= 0 /\ -X_11 + X_3 - 1 >= 0 /\ X_1 - X_2 >= 0 /\ -X_1 + X_2 >= 0 /\ -X_15 >= 0 /\ X_14 - X_15 >= 0 /\ X_11 - X_15 >= 0 /\ -X_11 - X_15 >= 0 /\ X_14 >= 0 /\ X_11 + X_14 >= 0 /\ -X_11 + X_14 >= 0 /\ -X_11 >= 0 /\ X_11 >= 0 For symbol f166: -X_9 >= 0 /\ -X_15 - X_9 >= 0 /\ X_14 - X_9 >= 0 /\ X_11 - X_9 >= 0 /\ -X_11 - X_9 >= 0 /\ X_9 >= 0 /\ -X_15 + X_9 >= 0 /\ X_14 + X_9 >= 0 /\ X_11 + X_9 >= 0 /\ -X_11 + X_9 >= 0 /\ X_1 - X_2 >= 0 /\ -X_1 + X_2 >= 0 /\ -X_15 >= 0 /\ X_14 - X_15 >= 0 /\ X_11 - X_15 >= 0 /\ -X_11 - X_15 >= 0 /\ X_14 >= 0 /\ X_11 + X_14 >= 0 /\ -X_11 + X_14 >= 0 /\ -X_11 >= 0 /\ X_11 >= 0 For symbol f177: -X_9 >= 0 /\ -X_15 - X_9 >= 0 /\ X_14 - X_9 >= 0 /\ X_11 - X_9 >= 0 /\ -X_11 - X_9 >= 0 /\ X_9 >= 0 /\ -X_15 + X_9 >= 0 /\ X_14 + X_9 >= 0 /\ X_11 + X_9 >= 0 /\ -X_11 + X_9 >= 0 /\ -X_15 >= 0 /\ X_14 - X_15 >= 0 /\ X_11 - X_15 >= 0 /\ -X_11 - X_15 >= 0 /\ X_14 >= 0 /\ X_11 + X_14 >= 0 /\ -X_11 + X_14 >= 0 /\ -X_11 >= 0 /\ X_11 >= 0 For symbol f187: -X_9 >= 0 /\ -X_15 - X_9 >= 0 /\ X_14 - X_9 >= 0 /\ X_11 - X_9 >= 0 /\ -X_11 - X_9 >= 0 /\ X_9 >= 0 /\ -X_15 + X_9 >= 0 /\ X_14 + X_9 >= 0 /\ X_11 + X_9 >= 0 /\ -X_11 + X_9 >= 0 /\ -X_15 >= 0 /\ X_14 - X_15 >= 0 /\ X_11 - X_15 >= 0 /\ -X_11 - X_15 >= 0 /\ X_14 >= 0 /\ X_11 + X_14 >= 0 /\ -X_11 + X_14 >= 0 /\ -X_11 >= 0 /\ X_11 >= 0 For symbol f190: -X_9 >= 0 /\ X_2 - X_9 - 4 >= 0 /\ -X_2 - X_9 + 7 >= 0 /\ -X_15 - X_9 >= 0 /\ X_14 - X_9 >= 0 /\ X_11 - X_9 >= 0 /\ -X_11 - X_9 >= 0 /\ X_9 >= 0 /\ X_2 + X_9 - 4 >= 0 /\ -X_2 + X_9 + 7 >= 0 /\ -X_15 + X_9 >= 0 /\ X_14 + X_9 >= 0 /\ X_11 + X_9 >= 0 /\ -X_11 + X_9 >= 0 /\ -X_2 + 7 >= 0 /\ -X_15 - X_2 + 7 >= 0 /\ X_14 - X_2 + 7 >= 0 /\ X_11 - X_2 + 7 >= 0 /\ -X_11 - X_2 + 7 >= 0 /\ X_2 - 4 >= 0 /\ -X_15 + X_2 - 4 >= 0 /\ X_14 + X_2 - 4 >= 0 /\ X_11 + X_2 - 4 >= 0 /\ -X_11 + X_2 - 4 >= 0 /\ -X_15 >= 0 /\ X_14 - X_15 >= 0 /\ X_11 - X_15 >= 0 /\ -X_11 - X_15 >= 0 /\ X_14 >= 0 /\ X_11 + X_14 >= 0 /\ -X_11 + X_14 >= 0 /\ -X_11 >= 0 /\ X_11 >= 0 For symbol f200: -X_9 >= 0 /\ X_2 - X_9 - 4 >= 0 /\ -X_2 - X_9 + 7 >= 0 /\ -X_15 - X_9 >= 0 /\ X_14 - X_9 >= 0 /\ X_11 - X_9 >= 0 /\ -X_11 - X_9 >= 0 /\ X_9 >= 0 /\ X_2 + X_9 - 4 >= 0 /\ -X_2 + X_9 + 7 >= 0 /\ -X_15 + X_9 >= 0 /\ X_14 + X_9 >= 0 /\ X_11 + X_9 >= 0 /\ -X_11 + X_9 >= 0 /\ -X_2 + 7 >= 0 /\ -X_15 - X_2 + 7 >= 0 /\ X_14 - X_2 + 7 >= 0 /\ X_11 - X_2 + 7 >= 0 /\ -X_11 - X_2 + 7 >= 0 /\ X_2 - 4 >= 0 /\ -X_15 + X_2 - 4 >= 0 /\ X_14 + X_2 - 4 >= 0 /\ X_11 + X_2 - 4 >= 0 /\ -X_11 + X_2 - 4 >= 0 /\ -X_15 >= 0 /\ X_14 - X_15 >= 0 /\ X_11 - X_15 >= 0 /\ -X_11 - X_15 >= 0 /\ X_14 >= 0 /\ X_11 + X_14 >= 0 /\ -X_11 + X_14 >= 0 /\ -X_11 >= 0 /\ X_11 >= 0 For symbol f208: X_9 - 1 >= 0 /\ -X_15 + X_9 - 1 >= 0 /\ X_14 + X_9 - 1 >= 0 /\ X_11 + X_9 - 1 >= 0 /\ -X_11 + X_9 - 1 >= 0 /\ -X_15 >= 0 /\ X_14 - X_15 >= 0 /\ X_11 - X_15 >= 0 /\ -X_11 - X_15 >= 0 /\ X_14 >= 0 /\ X_11 + X_14 >= 0 /\ -X_11 + X_14 >= 0 /\ -X_11 >= 0 /\ X_11 >= 0 This yielded the following problem: 8: T: (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(7, 7, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ a = 7 ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 6 >= a ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ a >= 8 ] (?, 1) f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ e - j - 1 >= 0 /\ d - j - 1 >= 0 /\ c - j - 1 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ e + j - 1 >= 0 /\ d + j - 1 >= 0 /\ c + j - 1 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ e - 1 >= 0 /\ d + e - 2 >= 0 /\ c + e - 2 >= 0 /\ -w1 + e - 1 >= 0 /\ q1 + e - 1 >= 0 /\ v + e - 1 >= 0 /\ -v + e - 1 >= 0 /\ d - 1 >= 0 /\ c + d - 2 >= 0 /\ -w1 + d - 1 >= 0 /\ q1 + d - 1 >= 0 /\ v + d - 1 >= 0 /\ -v + d - 1 >= 0 /\ c - 1 >= 0 /\ -w1 + c - 1 >= 0 /\ q1 + c - 1 >= 0 /\ v + c - 1 >= 0 /\ -v + c - 1 >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 ] (1, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ d >= 1 /\ c >= 1 /\ e >= 1 ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 7, c, d, e, u3, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ b = 7 ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, u3, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= g ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, h, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ h = i ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 6 >= b ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ b >= 8 ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ h >= i + 1 ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ i >= h + 1 ] (?, 1) f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ j - 1 >= 0 /\ -w1 + j - 1 >= 0 /\ q1 + j - 1 >= 0 /\ v + j - 1 >= 0 /\ -v + j - 1 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, v3, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ g >= 1 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 3 >= b ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ b >= 5 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 4, c, d, e, w3, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ b = 4 ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ u >= v + 1 ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, 0, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ v >= u ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= c ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ c >= 1 /\ 0 >= e ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= d /\ c >= 1 /\ e >= 1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= d1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ d1 >= 2 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, 1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ d1 = 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= j /\ 0 >= l1 ] (15*l1 + 14, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ l1 >= q1 + 1 /\ 0 >= j /\ l1 >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ l1 >= 1 /\ 0 >= j /\ q1 >= l1 ] (1, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ j >= 1 ] (?, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1 - 1) [ -j >= 0 /\ q1 - j >= 0 /\ -q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ q1 + j >= 0 /\ -q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -q1 >= 0 /\ v - q1 >= 0 /\ -v - q1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ w1 >= 1 ] (1, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ q1 - j >= 0 /\ -q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ q1 + j >= 0 /\ -q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -q1 >= 0 /\ v - q1 >= 0 /\ -v - q1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= w1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, 7, c, d, e, g, h, i, 0, u, 0, y3, l1, 0, y3) [ v3 >= 1 /\ y3 >= 1 /\ u3 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ 6 >= k4 /\ p4 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ k4 >= 8 /\ p4 >= 1 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f154) = -V_9 + 1 Pol(f166) = -V_9 + 1 Pol(f156) = -V_9 + 1 Pol(f159) = -8*V_3 - 8*V_4 - 8*V_5 + 7*V_9 - 8*V_14 + 10*V_15 + 25 Pol(f187) = -V_9 + 1 Pol(f190) = 1 Pol(f200) = 1 Pol(f115) = -V_9 + 1 Pol(f208) = -5*V_9 - 4*V_14 + 6*V_15 + 5 Pol(f177) = -V_9 + 1 Pol(f133) = -V_9 + 1 Pol(f100) = -V_9 + 1 Pol(f0) = 1 orients all transitions weakly and the transitions f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ i >= h + 1 ] f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ h >= i + 1 ] strictly and produces the following problem: 9: T: (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(7, 7, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ a = 7 ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 6 >= a ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ a >= 8 ] (?, 1) f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ e - j - 1 >= 0 /\ d - j - 1 >= 0 /\ c - j - 1 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ e + j - 1 >= 0 /\ d + j - 1 >= 0 /\ c + j - 1 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ e - 1 >= 0 /\ d + e - 2 >= 0 /\ c + e - 2 >= 0 /\ -w1 + e - 1 >= 0 /\ q1 + e - 1 >= 0 /\ v + e - 1 >= 0 /\ -v + e - 1 >= 0 /\ d - 1 >= 0 /\ c + d - 2 >= 0 /\ -w1 + d - 1 >= 0 /\ q1 + d - 1 >= 0 /\ v + d - 1 >= 0 /\ -v + d - 1 >= 0 /\ c - 1 >= 0 /\ -w1 + c - 1 >= 0 /\ q1 + c - 1 >= 0 /\ v + c - 1 >= 0 /\ -v + c - 1 >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 ] (1, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ d >= 1 /\ c >= 1 /\ e >= 1 ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 7, c, d, e, u3, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ b = 7 ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, u3, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= g ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, h, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ h = i ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 6 >= b ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ b >= 8 ] (1, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ h >= i + 1 ] (1, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ i >= h + 1 ] (?, 1) f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ j - 1 >= 0 /\ -w1 + j - 1 >= 0 /\ q1 + j - 1 >= 0 /\ v + j - 1 >= 0 /\ -v + j - 1 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, v3, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ g >= 1 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 3 >= b ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ b >= 5 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 4, c, d, e, w3, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ b = 4 ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ u >= v + 1 ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, 0, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ v >= u ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= c ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ c >= 1 /\ 0 >= e ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= d /\ c >= 1 /\ e >= 1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= d1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ d1 >= 2 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, 1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ d1 = 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= j /\ 0 >= l1 ] (15*l1 + 14, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ l1 >= q1 + 1 /\ 0 >= j /\ l1 >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ l1 >= 1 /\ 0 >= j /\ q1 >= l1 ] (1, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ j >= 1 ] (?, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1 - 1) [ -j >= 0 /\ q1 - j >= 0 /\ -q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ q1 + j >= 0 /\ -q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -q1 >= 0 /\ v - q1 >= 0 /\ -v - q1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ w1 >= 1 ] (1, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ q1 - j >= 0 /\ -q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ q1 + j >= 0 /\ -q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -q1 >= 0 /\ v - q1 >= 0 /\ -v - q1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= w1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, 7, c, d, e, g, h, i, 0, u, 0, y3, l1, 0, y3) [ v3 >= 1 /\ y3 >= 1 /\ u3 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ 6 >= k4 /\ p4 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ k4 >= 8 /\ p4 >= 1 ] start location: f0 leaf cost: 2 By chaining the transition f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ d >= 1 /\ c >= 1 /\ e >= 1 ] with all transitions in problem 9, the following new transition is obtained: f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ d >= 1 /\ c >= 1 /\ e >= 1 /\ e - j - 1 >= 0 /\ d - j - 1 >= 0 /\ c - j - 1 >= 0 /\ e + j - 1 >= 0 /\ d + j - 1 >= 0 /\ c + j - 1 >= 0 /\ e - 1 >= 0 /\ d + e - 2 >= 0 /\ c + e - 2 >= 0 /\ -w1 + e - 1 >= 0 /\ q1 + e - 1 >= 0 /\ v + e - 1 >= 0 /\ -v + e - 1 >= 0 /\ d - 1 >= 0 /\ c + d - 2 >= 0 /\ -w1 + d - 1 >= 0 /\ q1 + d - 1 >= 0 /\ v + d - 1 >= 0 /\ -v + d - 1 >= 0 /\ c - 1 >= 0 /\ -w1 + c - 1 >= 0 /\ q1 + c - 1 >= 0 /\ v + c - 1 >= 0 /\ -v + c - 1 >= 0 ] We thus obtain the following problem: 10: T: (1, 2) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ d >= 1 /\ c >= 1 /\ e >= 1 /\ e - j - 1 >= 0 /\ d - j - 1 >= 0 /\ c - j - 1 >= 0 /\ e + j - 1 >= 0 /\ d + j - 1 >= 0 /\ c + j - 1 >= 0 /\ e - 1 >= 0 /\ d + e - 2 >= 0 /\ c + e - 2 >= 0 /\ -w1 + e - 1 >= 0 /\ q1 + e - 1 >= 0 /\ v + e - 1 >= 0 /\ -v + e - 1 >= 0 /\ d - 1 >= 0 /\ c + d - 2 >= 0 /\ -w1 + d - 1 >= 0 /\ q1 + d - 1 >= 0 /\ v + d - 1 >= 0 /\ -v + d - 1 >= 0 /\ c - 1 >= 0 /\ -w1 + c - 1 >= 0 /\ q1 + c - 1 >= 0 /\ v + c - 1 >= 0 /\ -v + c - 1 >= 0 ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(7, 7, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ a = 7 ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 6 >= a ] (?, 1) f154(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f156(a, a, u3, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ a >= 8 ] (?, 1) f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f159(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ e - j - 1 >= 0 /\ d - j - 1 >= 0 /\ c - j - 1 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ e + j - 1 >= 0 /\ d + j - 1 >= 0 /\ c + j - 1 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ e - 1 >= 0 /\ d + e - 2 >= 0 /\ c + e - 2 >= 0 /\ -w1 + e - 1 >= 0 /\ q1 + e - 1 >= 0 /\ v + e - 1 >= 0 /\ -v + e - 1 >= 0 /\ d - 1 >= 0 /\ c + d - 2 >= 0 /\ -w1 + d - 1 >= 0 /\ q1 + d - 1 >= 0 /\ v + d - 1 >= 0 /\ -v + d - 1 >= 0 /\ c - 1 >= 0 /\ -w1 + c - 1 >= 0 /\ q1 + c - 1 >= 0 /\ v + c - 1 >= 0 /\ -v + c - 1 >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 7, c, d, e, u3, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ b = 7 ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, u3, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= g ] (?, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, h, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ h = i ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 6 >= b ] (?, 1) f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ b >= 8 ] (1, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ h >= i + 1 ] (1, 1) f200(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, 1, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ i >= h + 1 ] (?, 1) f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ j - 1 >= 0 /\ -w1 + j - 1 >= 0 /\ q1 + j - 1 >= 0 /\ v + j - 1 >= 0 /\ -v + j - 1 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 ] (?, 1) f190(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f200(a, b, c, d, e, g, v3, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ b - j - 4 >= 0 /\ -b - j + 7 >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ b + j - 4 >= 0 /\ -b + j + 7 >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -b + 7 >= 0 /\ -w1 - b + 7 >= 0 /\ q1 - b + 7 >= 0 /\ v - b + 7 >= 0 /\ -v - b + 7 >= 0 /\ b - 4 >= 0 /\ -w1 + b - 4 >= 0 /\ q1 + b - 4 >= 0 /\ v + b - 4 >= 0 /\ -v + b - 4 >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ g >= 1 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 3 >= b ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f187(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ b >= 5 ] (?, 1) f177(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f190(a, 4, c, d, e, w3, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ b = 4 ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ u >= v + 1 ] (?, 1) f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, 0, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ v >= u ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f166(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= c ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ c >= 1 /\ 0 >= e ] (?, 1) f156(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(v3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ a - b >= 0 /\ -a + b >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= d /\ c >= 1 /\ e >= 1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= d1 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f154(x3, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ d1 >= 2 ] (?, 1) f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f177(a, u3, c, d, e, g, h, i, j, u, v, 1, l1, q1, w1) [ -j >= 0 /\ -w1 - j >= 0 /\ q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ d1 = 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= j /\ 0 >= l1 ] (15*l1 + 14, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ l1 >= q1 + 1 /\ 0 >= j /\ l1 >= 1 ] (?, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f133(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1 + 1, w1) [ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ l1 >= 1 /\ 0 >= j /\ q1 >= l1 ] (1, 1) f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f208(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ j >= 0 /\ -w1 + j >= 0 /\ q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -w1 >= 0 /\ q1 - w1 >= 0 /\ v - w1 >= 0 /\ -v - w1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ j >= 1 ] (?, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1 - 1) [ -j >= 0 /\ q1 - j >= 0 /\ -q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ q1 + j >= 0 /\ -q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -q1 >= 0 /\ v - q1 >= 0 /\ -v - q1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ w1 >= 1 ] (1, 1) f100(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f115(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) [ -j >= 0 /\ q1 - j >= 0 /\ -q1 - j >= 0 /\ v - j >= 0 /\ -v - j >= 0 /\ j >= 0 /\ q1 + j >= 0 /\ -q1 + j >= 0 /\ v + j >= 0 /\ -v + j >= 0 /\ -q1 >= 0 /\ v - q1 >= 0 /\ -v - q1 >= 0 /\ q1 >= 0 /\ v + q1 >= 0 /\ -v + q1 >= 0 /\ -v >= 0 /\ v >= 0 /\ 0 >= w1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, 7, c, d, e, g, h, i, 0, u, 0, y3, l1, 0, y3) [ v3 >= 1 /\ y3 >= 1 /\ u3 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ 6 >= k4 /\ p4 >= 1 ] (1, 1) f0(a, b, c, d, e, g, h, i, j, u, v, d1, l1, q1, w1) -> f100(a, k4, c, d, e, g, h, i, 0, u, 0, p4, l1, 0, p4) [ v3 >= 1 /\ u3 >= 1 /\ k4 >= 8 /\ p4 >= 1 ] start location: f0 leaf cost: 2 Complexity upper bound ? Time: 12.920 sec (SMT: 7.763 sec)