MAYBE Initial complexity problem: 1: T: (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, 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) -> f16(a, b + 1, d, n2, d, o2, b, i, 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) [ a >= b + 1 /\ b >= 0 ] (?, 1) f2(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) -> f4(a, b, c, d, e, f, g, h, i, s + 1, k, l, 1, n2, o2, k, o2, k, s, r2, v, v, i, l, s2, t2, u2, q2, s, 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) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(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) -> f4(a, b, c, d, e, f, g, h, i, s + 1, k, l, 1, n2, o2, k, o2, k, s, r2, v, v, i, l, s2, t2, u2, q2, s, 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) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(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) -> f4(a, b, c, d, e, f, g, h, i, s + 1, k, l, 1, n2, o2, k, o2, k, s, r2, v, v, i, l, s2, t2, u2, q2, s, 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) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(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) -> f4(a, b, c, d, e, f, g, h, i, s + 1, k, l, 1, n2, o2, k, o2, k, s, r2, v, v, i, l, s2, t2, u2, q2, s, 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) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(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) -> f4(a, b, c, d, e, f, g, h, i, s + 1, k, l, 1, n2, o2, k, o2, k, s, r2, v, v, i, l, s2, t2, u2, q2, s, 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) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(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) -> f4(a, b, c, d, e, f, g, h, i, s + 1, k, l, 1, n2, o2, k, o2, k, s, r2, v, v, i, l, s2, t2, u2, q2, s, 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) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(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) -> f4(a, b, c, d, e, f, g, h, i, s + 1, k, l, 1, n2, o2, k, o2, k, s, r2, v, v, i, l, s2, t2, u2, q2, s, 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) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(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) -> f4(a, b, c, d, e, f, g, h, i, s + 1, k, l, 1, n2, o2, k, o2, k, s, r2, v, v, i, l, s2, t2, u2, q2, s, 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) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(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) -> f4(a, b, c, d, e, f, g, h, i, s + 1, k, l, 1, n2, o2, k, o2, k, s, r2, v, v, i, l, s2, t2, u2, q2, s, 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) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(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) -> f4(a, b, c, d, e, f, g, h, i, s + 1, k, l, 1, n2, o2, k, o2, k, s, r2, v, v, i, l, s2, t2, u2, q2, s, 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) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(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) -> f4(a, b, c, d, e, f, g, h, i, s + 1, k, l, 1, n2, o2, k, o2, k, s, r2, v, v, i, l, s2, t2, u2, q2, s, 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) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(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) -> f4(a, b, c, d, e, f, g, h, i, s + 1, k, l, 1, n2, o2, k, o2, k, s, r2, v, v, i, l, s2, t2, u2, q2, s, 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) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(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) -> f4(a, b, c, d, e, f, g, h, i, s + 1, k, l, 1, n2, o2, k, o2, k, s, r2, v, v, i, l, s2, t2, u2, q2, s, 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) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(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) -> f4(a, b, c, d, e, f, g, h, i, s + 1, k, l, 1, n2, o2, k, o2, k, s, r2, v, v, i, l, s2, t2, u2, q2, s, 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) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(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) -> f4(a, b, c, d, e, f, g, h, i, s + 1, k, l, 1, n2, o2, k, o2, k, s, r2, v, v, i, l, s2, t2, u2, q2, s, 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) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(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) -> f4(a, b, c, d, e, f, g, h, i, s + 1, k, l, 1, n2, o2, k, o2, k, s, r2, v, v, i, l, s2, t2, u2, q2, s, 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) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] (?, 1) f3(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o2, k, o2, k, s, t, u, v, w, x, y, z, a1, b1, c1, r2, s2, 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) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ 0 >= s2 + 1 /\ 0 >= k + 1 ] (?, 1) f3(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o2, k, o2, k, s, t, u, v, w, x, y, z, a1, b1, c1, r2, s2, 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) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ 0 >= s2 + 1 /\ k >= 1 ] (?, 1) f3(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o2, k, o2, k, s, t, u, v, w, x, y, z, a1, b1, c1, r2, s2, 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) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ s2 >= 1 /\ 0 >= k + 1 ] (?, 1) f3(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o2, k, o2, k, s, t, u, v, w, x, y, z, a1, b1, c1, r2, s2, 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) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ s2 >= 1 /\ k >= 1 ] (?, 1) f3(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o2, k, o2, k, s, t, u, v, w, x, y, z, a1, b1, c1, r2, s2, 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) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ 0 >= s2 + 1 /\ 0 >= k + 1 ] (?, 1) f3(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o2, k, o2, k, s, t, u, v, w, x, y, z, a1, b1, c1, r2, s2, 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) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ 0 >= s2 + 1 /\ k >= 1 ] (?, 1) f3(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o2, k, o2, k, s, t, u, v, w, x, y, z, a1, b1, c1, r2, s2, 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) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ s2 >= 1 /\ 0 >= k + 1 ] (?, 1) f3(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o2, k, o2, k, s, t, u, v, w, x, y, z, a1, b1, c1, r2, s2, 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) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ s2 >= 1 /\ k >= 1 ] (?, 1) f4(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, n2, o2, k, o2, k, s - 1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, r2, s2, v, i, l, m + 1, s - 1, 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) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, n2, o2, k, o2, k, s - 1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, r2, s2, v, i, l, m + 1, s - 1, 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) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, n2, o2, k, o2, k, s - 1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, r2, s2, v, i, l, m + 1, s - 1, 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) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, n2, o2, k, o2, k, s - 1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, r2, s2, v, i, l, m + 1, s - 1, 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) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, n2, o2, k, o2, k, s - 1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, r2, s2, v, i, l, m + 1, s - 1, 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) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, n2, o2, k, o2, k, s - 1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, r2, s2, v, i, l, m + 1, s - 1, 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) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, n2, o2, k, o2, k, s - 1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, r2, s2, v, i, l, m + 1, s - 1, 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) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, n2, o2, k, o2, k, s - 1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, r2, s2, v, i, l, m + 1, s - 1, 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) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, n2, o2, k, o2, k, s - 1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, r2, s2, v, i, l, m + 1, s - 1, 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) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, n2, o2, k, o2, k, s - 1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, r2, s2, v, i, l, m + 1, s - 1, 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) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, n2, o2, k, o2, k, s - 1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, r2, s2, v, i, l, m + 1, s - 1, 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) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, n2, o2, k, o2, k, s - 1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, r2, s2, v, i, l, m + 1, s - 1, 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) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, n2, o2, k, o2, k, s - 1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, r2, s2, v, i, l, m + 1, s - 1, 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) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, n2, o2, k, o2, k, s - 1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, r2, s2, v, i, l, m + 1, s - 1, 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) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, n2, o2, k, o2, k, s - 1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, r2, s2, v, i, l, m + 1, s - 1, 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) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(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) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, n2, o2, k, o2, k, s - 1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, r2, s2, v, i, l, m + 1, s - 1, 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) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, 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) -> f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, 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, 0, o2, 0, o2, o2, m1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, 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) -> f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, 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, 0, o2, 0, o2, o2, m1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, 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) -> f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, 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, 0, o2, 0, o2, o2, m1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, 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) -> f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, 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, 0, o2, 0, o2, o2, m1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, 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) -> f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, 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, 0, o2, 0, o2, o2, m1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, 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) -> f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, 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, 0, o2, 0, o2, o2, m1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, 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) -> f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, 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, 0, o2, 0, o2, o2, m1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, 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) -> f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, 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, 0, o2, 0, o2, o2, m1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, 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) -> f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, q2, n1, u2, r2, s2, t2, p2, w2, o2, v2, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ n1 >= 0 /\ 0 >= v2 + 1 /\ n2 >= 2 /\ o1 = m1 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, 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) -> f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, q2, n1, u2, r2, s2, t2, p2, w2, o2, v2, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ n1 >= 0 /\ v2 >= 1 /\ n2 >= 2 /\ o1 = m1 ] (?, 1) f14(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) -> f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o, p, q, r, s, t, u, r2, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, 0, o2, 0, o2, o2, m1, u1, v1, w1 - 1, i, w1 - 1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f14(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) -> f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o, p, q, r, s, t, u, r2, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, 0, o2, 0, o2, o2, m1, u1, v1, w1 - 1, i, w1 - 1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f14(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) -> f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o, p, q, r, s, t, u, r2, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, 0, o2, 0, o2, o2, m1, u1, v1, w1 - 1, i, w1 - 1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f14(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) -> f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o, p, q, r, s, t, u, r2, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, 0, o2, 0, o2, o2, m1, u1, v1, w1 - 1, i, w1 - 1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f14(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) -> f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o, p, q, r, s, t, u, r2, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, 0, o2, 0, o2, o2, m1, u1, v1, w1 - 1, i, w1 - 1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f14(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) -> f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o, p, q, r, s, t, u, r2, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, 0, o2, 0, o2, o2, m1, u1, v1, w1 - 1, i, w1 - 1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f14(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) -> f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o, p, q, r, s, t, u, r2, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, 0, o2, 0, o2, o2, m1, u1, v1, w1 - 1, i, w1 - 1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f14(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) -> f14(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o, p, q, r, s, t, u, r2, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, 0, o2, 0, o2, o2, m1, u1, v1, w1 - 1, i, w1 - 1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f14(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) -> f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n2, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, q2, n1, u2, r2, s2, t2, p2, w2, o2, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ n2 >= 2 /\ w1 >= 0 /\ o1 = m1 ] (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) -> f16(o2, 2, r2, s2, r2, f, g, h, i, j, k, l, m, o2, 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, n2, r2, t2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ o2 >= 2 ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, 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) -> f4(o2, s2, r2, w2, p2, f, g, h, i, s, k, k, 0, n2, v2, k, v2, k, 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, u2, v1, w1, x1, y1, z1, q2, b2, s + 1, t2, v, i, y2, z2, i2, j2, k2, l2, m2) [ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ 0 >= l + 1 /\ m = 0 /\ k = l ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, 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) -> f4(o2, s2, r2, w2, p2, f, g, h, i, s, k, k, 0, n2, v2, k, v2, k, 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, u2, v1, w1, x1, y1, z1, q2, b2, s + 1, t2, v, i, y2, z2, i2, j2, k2, l2, m2) [ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ l >= 1 /\ m = 0 /\ k = l ] (?, 1) f2(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, i, i, u2, m2) [ q2 >= 2 /\ n2 >= 2 /\ s1 >= 1 /\ j >= 0 /\ 0 >= s1 + 1 /\ k = 0 /\ i2 = 1 ] (?, 1) f2(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, i, i, u2, m2) [ q2 >= 2 /\ n2 >= 2 /\ s1 >= 1 /\ j >= 0 /\ k = 0 /\ i2 = 1 ] (?, 1) f2(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, i, i, u2, m2) [ q2 >= 2 /\ n2 >= 2 /\ 0 >= s1 + 1 /\ j >= 0 /\ k = 0 /\ i2 = 1 ] (?, 1) f2(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, i, i, u2, m2) [ q2 >= 2 /\ n2 >= 2 /\ 0 >= s1 + 1 /\ j >= 0 /\ s1 >= 1 /\ k = 0 /\ i2 = 1 ] (?, 1) f3(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, j2, i, u2, i) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ s1 >= 1 /\ 0 >= s1 + 1 /\ 0 >= l + 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, j2, i, u2, i) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ s1 >= 1 /\ 0 >= s1 + 1 /\ l >= 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, j2, i, u2, i) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ s1 >= 1 /\ 0 >= l + 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, j2, i, u2, i) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ s1 >= 1 /\ l >= 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, j2, i, u2, i) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ 0 >= s1 + 1 /\ 0 >= l + 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, j2, i, u2, i) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ 0 >= s1 + 1 /\ l >= 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, j2, i, u2, i) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ 0 >= s1 + 1 /\ s1 >= 1 /\ 0 >= l + 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, j2, i, u2, i) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ 0 >= s1 + 1 /\ s1 >= 1 /\ l >= 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f4(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, j2, i, u2, m2) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ s1 >= 1 /\ i2 >= 0 /\ 0 >= s1 + 1 /\ 0 >= l + 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, j2, i, u2, m2) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ s1 >= 1 /\ i2 >= 0 /\ 0 >= s1 + 1 /\ l >= 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, j2, i, u2, m2) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ s1 >= 1 /\ i2 >= 0 /\ 0 >= l + 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, j2, i, u2, m2) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ s1 >= 1 /\ i2 >= 0 /\ l >= 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, j2, i, u2, m2) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ 0 >= s1 + 1 /\ i2 >= 0 /\ 0 >= l + 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, j2, i, u2, m2) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ 0 >= s1 + 1 /\ i2 >= 0 /\ l >= 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, j2, i, u2, m2) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ 0 >= s1 + 1 /\ i2 >= 0 /\ s1 >= 1 /\ 0 >= l + 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(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) -> f14(a, b, c, d, e, f, g, h, i, j, o2, l, m, n2, r2, s2, q, t2, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, s1, w1, 0, s1, 0, s1, s1, s1, u1, v1, w1, x1, y1, z1, a2, b2, c2, d2, e2, f2, g2, h2, w1 + 1, j2, i, u2, m2) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ 0 >= s1 + 1 /\ i2 >= 0 /\ s1 >= 1 /\ l >= 1 /\ m + 1 = i2 /\ k = 0 ] (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) -> f1(r2, t2, s2, y2, v2, f, g, h, i, j, u2, l, m, o2, z2, x2, q, d3, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, i3, n1, h3, e3, f3, g3, j3, k3, p2, v1, w1, x1, y1, n2, w2, b2, c2, q2, e2, f2, g2, h2, i2, j2, k2, l2, m2) [ 0 >= a3 /\ 0 >= b3 /\ 0 >= o2 /\ 0 >= c3 /\ s1 = 0 ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2]. We thus obtain the following problem: 2: T: (1, 1) f0(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f1(r2, t2, j, u2, l, m, s, c1, i3, n1, h3, j3, w1, c2, i2) [ 0 >= a3 /\ 0 >= b3 /\ 0 >= o2 /\ 0 >= c3 /\ s1 = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ 0 >= s1 + 1 /\ i2 >= 0 /\ s1 >= 1 /\ l >= 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ 0 >= s1 + 1 /\ i2 >= 0 /\ s1 >= 1 /\ 0 >= l + 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ 0 >= s1 + 1 /\ i2 >= 0 /\ l >= 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ 0 >= s1 + 1 /\ i2 >= 0 /\ 0 >= l + 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ s1 >= 1 /\ i2 >= 0 /\ l >= 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ s1 >= 1 /\ i2 >= 0 /\ 0 >= l + 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ s1 >= 1 /\ i2 >= 0 /\ 0 >= s1 + 1 /\ l >= 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ s1 >= 1 /\ i2 >= 0 /\ 0 >= s1 + 1 /\ 0 >= l + 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ 0 >= s1 + 1 /\ s1 >= 1 /\ l >= 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ 0 >= s1 + 1 /\ s1 >= 1 /\ 0 >= l + 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ 0 >= s1 + 1 /\ l >= 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ 0 >= s1 + 1 /\ 0 >= l + 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ s1 >= 1 /\ l >= 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ s1 >= 1 /\ 0 >= l + 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ s1 >= 1 /\ 0 >= s1 + 1 /\ l >= 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ s1 >= 1 /\ 0 >= s1 + 1 /\ 0 >= l + 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ 0 >= s1 + 1 /\ j >= 0 /\ s1 >= 1 /\ k = 0 /\ i2 = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ 0 >= s1 + 1 /\ j >= 0 /\ k = 0 /\ i2 = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ s1 >= 1 /\ j >= 0 /\ k = 0 /\ i2 = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ s1 >= 1 /\ j >= 0 /\ 0 >= s1 + 1 /\ k = 0 /\ i2 = 1 ] (?, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(o2, s2, s, k, k, 0, s, c1, m1, n1, o1, s1, w1, s + 1, i2) [ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ l >= 1 /\ m = 0 /\ k = l ] (?, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(o2, s2, s, k, k, 0, s, c1, m1, n1, o1, s1, w1, s + 1, i2) [ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ 0 >= l + 1 /\ m = 0 /\ k = l ] (1, 1) f0(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f16(o2, 2, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ o2 >= 2 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f1(a, b, j, k, l, m, s, c1, q2, n1, u2, p2, w1, c2, i2) [ n2 >= 2 /\ w1 >= 0 /\ o1 = m1 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f1(a, b, j, k, l, m, s, c1, q2, n1, u2, p2, w1, c2, i2) [ n1 >= 0 /\ v2 >= 1 /\ n2 >= 2 /\ o1 = m1 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f1(a, b, j, k, l, m, s, c1, q2, n1, u2, p2, w1, c2, i2) [ n1 >= 0 /\ 0 >= v2 + 1 /\ n2 >= 2 /\ o1 = m1 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ s2 >= 1 /\ k >= 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ s2 >= 1 /\ 0 >= k + 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ 0 >= s2 + 1 /\ k >= 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ 0 >= s2 + 1 /\ 0 >= k + 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ s2 >= 1 /\ k >= 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ s2 >= 1 /\ 0 >= k + 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ 0 >= s2 + 1 /\ k >= 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ 0 >= s2 + 1 /\ 0 >= k + 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f16(a, b + 1, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ a >= b + 1 /\ b >= 0 ] start location: f0 leaf cost: 0 Testing for unsatisfiable constraints removes the following transitions from problem 2: f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ 0 >= s1 + 1 /\ i2 >= 0 /\ s1 >= 1 /\ l >= 1 /\ m + 1 = i2 /\ k = 0 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ 0 >= s1 + 1 /\ i2 >= 0 /\ s1 >= 1 /\ 0 >= l + 1 /\ m + 1 = i2 /\ k = 0 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ s1 >= 1 /\ i2 >= 0 /\ 0 >= s1 + 1 /\ l >= 1 /\ m + 1 = i2 /\ k = 0 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ s1 >= 1 /\ i2 >= 0 /\ 0 >= s1 + 1 /\ 0 >= l + 1 /\ m + 1 = i2 /\ k = 0 ] f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ 0 >= s1 + 1 /\ s1 >= 1 /\ l >= 1 /\ k = 0 /\ i2 = 2 ] f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ 0 >= s1 + 1 /\ s1 >= 1 /\ 0 >= l + 1 /\ k = 0 /\ i2 = 2 ] f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ s1 >= 1 /\ 0 >= s1 + 1 /\ l >= 1 /\ k = 0 /\ i2 = 2 ] f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ s1 >= 1 /\ 0 >= s1 + 1 /\ 0 >= l + 1 /\ k = 0 /\ i2 = 2 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ 0 >= s1 + 1 /\ j >= 0 /\ s1 >= 1 /\ k = 0 /\ i2 = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ s1 >= 1 /\ j >= 0 /\ 0 >= s1 + 1 /\ k = 0 /\ i2 = 1 ] We thus obtain the following problem: 3: T: (1, 1) f0(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f1(r2, t2, j, u2, l, m, s, c1, i3, n1, h3, j3, w1, c2, i2) [ 0 >= a3 /\ 0 >= b3 /\ 0 >= o2 /\ 0 >= c3 /\ s1 = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ 0 >= s1 + 1 /\ i2 >= 0 /\ l >= 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ 0 >= s1 + 1 /\ i2 >= 0 /\ 0 >= l + 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ s1 >= 1 /\ i2 >= 0 /\ l >= 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ s1 >= 1 /\ i2 >= 0 /\ 0 >= l + 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ 0 >= s1 + 1 /\ l >= 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ 0 >= s1 + 1 /\ 0 >= l + 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ s1 >= 1 /\ l >= 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ s1 >= 1 /\ 0 >= l + 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ 0 >= s1 + 1 /\ j >= 0 /\ k = 0 /\ i2 = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ s1 >= 1 /\ j >= 0 /\ k = 0 /\ i2 = 1 ] (?, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(o2, s2, s, k, k, 0, s, c1, m1, n1, o1, s1, w1, s + 1, i2) [ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ l >= 1 /\ m = 0 /\ k = l ] (?, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(o2, s2, s, k, k, 0, s, c1, m1, n1, o1, s1, w1, s + 1, i2) [ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ 0 >= l + 1 /\ m = 0 /\ k = l ] (1, 1) f0(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f16(o2, 2, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ o2 >= 2 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f1(a, b, j, k, l, m, s, c1, q2, n1, u2, p2, w1, c2, i2) [ n2 >= 2 /\ w1 >= 0 /\ o1 = m1 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f1(a, b, j, k, l, m, s, c1, q2, n1, u2, p2, w1, c2, i2) [ n1 >= 0 /\ v2 >= 1 /\ n2 >= 2 /\ o1 = m1 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f1(a, b, j, k, l, m, s, c1, q2, n1, u2, p2, w1, c2, i2) [ n1 >= 0 /\ 0 >= v2 + 1 /\ n2 >= 2 /\ o1 = m1 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ s2 >= 1 /\ k >= 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ s2 >= 1 /\ 0 >= k + 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ 0 >= s2 + 1 /\ k >= 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ 0 >= s2 + 1 /\ 0 >= k + 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ s2 >= 1 /\ k >= 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ s2 >= 1 /\ 0 >= k + 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ 0 >= s2 + 1 /\ k >= 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ 0 >= s2 + 1 /\ 0 >= k + 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f16(a, b + 1, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ a >= b + 1 /\ b >= 0 ] start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 3 produces the following problem: 4: T: (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ 0 >= s1 + 1 /\ i2 >= 0 /\ l >= 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ 0 >= s1 + 1 /\ i2 >= 0 /\ 0 >= l + 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ s1 >= 1 /\ i2 >= 0 /\ l >= 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ s1 >= 1 /\ i2 >= 0 /\ 0 >= l + 1 /\ m + 1 = i2 /\ k = 0 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ 0 >= s1 + 1 /\ l >= 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ 0 >= s1 + 1 /\ 0 >= l + 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ s1 >= 1 /\ l >= 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ s1 >= 1 /\ 0 >= l + 1 /\ k = 0 /\ i2 = 2 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ 0 >= s1 + 1 /\ j >= 0 /\ k = 0 /\ i2 = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ s1 >= 1 /\ j >= 0 /\ k = 0 /\ i2 = 1 ] (?, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(o2, s2, s, k, k, 0, s, c1, m1, n1, o1, s1, w1, s + 1, i2) [ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ l >= 1 /\ m = 0 /\ k = l ] (?, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(o2, s2, s, k, k, 0, s, c1, m1, n1, o1, s1, w1, s + 1, i2) [ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ 0 >= l + 1 /\ m = 0 /\ k = l ] (1, 1) f0(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f16(o2, 2, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ o2 >= 2 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ o2 >= 1 /\ o1 = 0 ] (?, 1) f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ s2 >= 1 /\ k >= 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ s2 >= 1 /\ 0 >= k + 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ 0 >= s2 + 1 /\ k >= 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ 0 >= s2 + 1 /\ 0 >= k + 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ s2 >= 1 /\ k >= 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ s2 >= 1 /\ 0 >= k + 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ 0 >= s2 + 1 /\ k >= 1 ] (?, 1) f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ 0 >= s2 + 1 /\ 0 >= k + 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] (?, 1) f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] (?, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f16(a, b + 1, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ a >= b + 1 /\ b >= 0 ] start location: f0 leaf cost: 4 Testing for reachability in the complexity graph removes the following transitions from problem 4: f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ 0 >= s1 + 1 /\ i2 >= 0 /\ l >= 1 /\ m + 1 = i2 /\ k = 0 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ 0 >= s1 + 1 /\ i2 >= 0 /\ 0 >= l + 1 /\ m + 1 = i2 /\ k = 0 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ s1 >= 1 /\ i2 >= 0 /\ l >= 1 /\ m + 1 = i2 /\ k = 0 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ i2 >= 1 /\ s >= 0 /\ s1 >= 1 /\ i2 >= 0 /\ 0 >= l + 1 /\ m + 1 = i2 /\ k = 0 ] f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ 0 >= s1 + 1 /\ l >= 1 /\ k = 0 /\ i2 = 2 ] f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ 0 >= s1 + 1 /\ 0 >= l + 1 /\ k = 0 /\ i2 = 2 ] f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ s1 >= 1 /\ l >= 1 /\ k = 0 /\ i2 = 2 ] f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ c1 >= 0 /\ s1 >= 1 /\ 0 >= l + 1 /\ k = 0 /\ i2 = 2 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ 0 >= s1 + 1 /\ j >= 0 /\ k = 0 /\ i2 = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, o2, l, m, s, c1, s1, w1, 0, s1, w1, c2, w1 + 1) [ q2 >= 2 /\ n2 >= 2 /\ s1 >= 1 /\ j >= 0 /\ k = 0 /\ i2 = 1 ] f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ o2 >= 1 /\ o1 = 0 ] f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ m1 >= s2 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ s2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ o2 >= 1 /\ o1 = 0 ] f14(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1 - 1, c2, i2) [ s2 >= m1 + 1 /\ w1 >= 0 /\ n2 >= 2 /\ o2 >= s2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ o2 >= 1 /\ o1 = 0 ] f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ m1 >= r2 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ o2 >= 1 /\ o1 = 0 ] f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ r2 >= o2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ o2 >= 1 /\ o1 = 0 ] f13(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f14(a, b, j, k, l, m, s, c1, m1, n1, 0, o2, w1, c2, i2) [ r2 >= m1 + 1 /\ n1 >= 0 /\ n2 >= 2 /\ o2 >= r2 + 1 /\ 0 >= o2 + 1 /\ o1 = 0 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ 0 >= l + 1 /\ s2 >= 1 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ l >= 1 /\ s2 >= 1 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ l >= 1 /\ 0 >= s2 + 1 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ 0 >= l + 1 /\ s2 >= 1 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ l >= 1 /\ s2 >= 1 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ l >= 1 /\ 0 >= s2 + 1 ] f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ s2 >= 1 /\ k >= 1 ] f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ s2 >= 1 /\ 0 >= k + 1 ] f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ 0 >= s2 + 1 /\ k >= 1 ] f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ l >= 1 /\ 0 >= s2 + 1 /\ 0 >= k + 1 ] f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ s2 >= 1 /\ k >= 1 ] f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ s2 >= 1 /\ 0 >= k + 1 ] f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ 0 >= s2 + 1 /\ k >= 1 ] f3(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ c1 >= 0 /\ n2 >= 2 /\ 0 >= l + 1 /\ 0 >= s2 + 1 /\ 0 >= k + 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ p2 >= 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ k >= 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ l >= 1 /\ m = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ q2 >= 1 /\ 0 >= l + 1 /\ m = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ l >= 1 /\ m = 1 ] f2(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, s + 1, k, l, 1, s, s, m1, n1, o1, s1, w1, c2, i2) [ j >= 0 /\ n2 >= 2 /\ 0 >= p2 + 1 /\ 0 >= k + 1 /\ 0 >= q2 + 1 /\ 0 >= l + 1 /\ m = 1 ] We thus obtain the following problem: 5: T: (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f16(a, b + 1, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ a >= b + 1 /\ b >= 0 ] (?, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(o2, s2, s, k, k, 0, s, c1, m1, n1, o1, s1, w1, s + 1, i2) [ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ 0 >= l + 1 /\ m = 0 /\ k = l ] (?, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(o2, s2, s, k, k, 0, s, c1, m1, n1, o1, s1, w1, s + 1, i2) [ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ l >= 1 /\ m = 0 /\ k = l ] (1, 1) f0(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f16(o2, 2, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ o2 >= 2 ] start location: f0 leaf cost: 4 A polynomial rank function with Pol(f4) = -6 Pol(f16) = 2 Pol(f0) = 2 orients all transitions weakly and the transitions f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(o2, s2, s, k, k, 0, s, c1, m1, n1, o1, s1, w1, s + 1, i2) [ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ l >= 1 /\ m = 0 /\ k = l ] f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(o2, s2, s, k, k, 0, s, c1, m1, n1, o1, s1, w1, s + 1, i2) [ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ 0 >= l + 1 /\ m = 0 /\ k = l ] strictly and produces the following problem: 6: T: (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (?, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f16(a, b + 1, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ a >= b + 1 /\ b >= 0 ] (2, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(o2, s2, s, k, k, 0, s, c1, m1, n1, o1, s1, w1, s + 1, i2) [ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ 0 >= l + 1 /\ m = 0 /\ k = l ] (2, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(o2, s2, s, k, k, 0, s, c1, m1, n1, o1, s1, w1, s + 1, i2) [ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ l >= 1 /\ m = 0 /\ k = l ] (1, 1) f0(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f16(o2, 2, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ o2 >= 2 ] start location: f0 leaf cost: 4 A polynomial rank function with Pol(f4) = V_7 + 1 Pol(f16) = -V_4 + V_5 + V_6 + V_7 + V_14 - 1 Pol(f0) = -V_4 + V_5 + V_6 + V_7 + V_14 - 1 orients all transitions weakly and the transitions f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] strictly and produces the following problem: 7: T: (k + l + m + s + c2 + 1, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (k + l + m + s + c2 + 1, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (k + l + m + s + c2 + 1, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (k + l + m + s + c2 + 1, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (k + l + m + s + c2 + 1, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (k + l + m + s + c2 + 1, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] (k + l + m + s + c2 + 1, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (k + l + m + s + c2 + 1, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] (?, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f16(a, b + 1, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ a >= b + 1 /\ b >= 0 ] (2, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(o2, s2, s, k, k, 0, s, c1, m1, n1, o1, s1, w1, s + 1, i2) [ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ 0 >= l + 1 /\ m = 0 /\ k = l ] (2, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(o2, s2, s, k, k, 0, s, c1, m1, n1, o1, s1, w1, s + 1, i2) [ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ l >= 1 /\ m = 0 /\ k = l ] (1, 1) f0(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f16(o2, 2, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ o2 >= 2 ] start location: f0 leaf cost: 4 Applied AI with 'oct' on problem 7 to obtain the following invariants: For symbol f16: X_1 - X_2 >= 0 /\ X_2 - 2 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ X_1 - 2 >= 0 For symbol f4: X_3 - X_7 >= 0 /\ X_14 - X_7 - 1 >= 0 /\ X_6 >= 0 /\ X_4 - X_5 >= 0 /\ -X_4 + X_5 >= 0 /\ X_14 - X_3 - 1 >= 0 /\ -X_14 + X_3 + 1 >= 0 This yielded the following problem: 8: T: (1, 1) f0(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f16(o2, 2, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ o2 >= 2 ] (2, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(o2, s2, s, k, k, 0, s, c1, m1, n1, o1, s1, w1, s + 1, i2) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ l >= 1 /\ m = 0 /\ k = l ] (2, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(o2, s2, s, k, k, 0, s, c1, m1, n1, o1, s1, w1, s + 1, i2) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ x2 >= 2 /\ c2 >= x2 /\ n2 >= 2 /\ c2 >= n2 /\ b >= a /\ b >= 0 /\ c2 >= 0 /\ 0 >= l + 1 /\ m = 0 /\ k = l ] (?, 1) f16(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f16(a, b + 1, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] (k + l + m + s + c2 + 1, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ j - s >= 0 /\ c2 - s - 1 >= 0 /\ m >= 0 /\ k - l >= 0 /\ -k + l >= 0 /\ c2 - j - 1 >= 0 /\ -c2 + j + 1 >= 0 /\ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] (k + l + m + s + c2 + 1, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ j - s >= 0 /\ c2 - s - 1 >= 0 /\ m >= 0 /\ k - l >= 0 /\ -k + l >= 0 /\ c2 - j - 1 >= 0 /\ -c2 + j + 1 >= 0 /\ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (k + l + m + s + c2 + 1, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ j - s >= 0 /\ c2 - s - 1 >= 0 /\ m >= 0 /\ k - l >= 0 /\ -k + l >= 0 /\ c2 - j - 1 >= 0 /\ -c2 + j + 1 >= 0 /\ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ s2 >= 1 ] (k + l + m + s + c2 + 1, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ j - s >= 0 /\ c2 - s - 1 >= 0 /\ m >= 0 /\ k - l >= 0 /\ -k + l >= 0 /\ c2 - j - 1 >= 0 /\ -c2 + j + 1 >= 0 /\ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ k >= 1 /\ l >= 1 /\ 0 >= s2 + 1 ] (k + l + m + s + c2 + 1, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ j - s >= 0 /\ c2 - s - 1 >= 0 /\ m >= 0 /\ k - l >= 0 /\ -k + l >= 0 /\ c2 - j - 1 >= 0 /\ -c2 + j + 1 >= 0 /\ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (k + l + m + s + c2 + 1, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ j - s >= 0 /\ c2 - s - 1 >= 0 /\ m >= 0 /\ k - l >= 0 /\ -k + l >= 0 /\ c2 - j - 1 >= 0 /\ -c2 + j + 1 >= 0 /\ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ u2 >= 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] (k + l + m + s + c2 + 1, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ j - s >= 0 /\ c2 - s - 1 >= 0 /\ m >= 0 /\ k - l >= 0 /\ -k + l >= 0 /\ c2 - j - 1 >= 0 /\ -c2 + j + 1 >= 0 /\ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ s2 >= 1 ] (k + l + m + s + c2 + 1, 1) f4(a, b, j, k, l, m, s, c1, m1, n1, o1, s1, w1, c2, i2) -> f4(a, b, j, k, l, m + 1, s - 1, c1, m1, n1, o1, s1, w1, c2, i2) [ j - s >= 0 /\ c2 - s - 1 >= 0 /\ m >= 0 /\ k - l >= 0 /\ -k + l >= 0 /\ c2 - j - 1 >= 0 /\ -c2 + j + 1 >= 0 /\ t2 >= 0 /\ s >= 0 /\ n2 >= 2 /\ 0 >= u2 + 1 /\ 0 >= k + 1 /\ 0 >= l + 1 /\ 0 >= s2 + 1 ] start location: f0 leaf cost: 4 Complexity upper bound ? Time: 9.685 sec (SMT: 7.383 sec)