YES(?, 16*j + 16*k + 16*m + 16*e1 + 16*w1 + n + 36) Initial complexity problem: 1: T: (?, 1) f1(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) -> f1(a, b + 1, d, c2, d, d2, 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) [ a >= b + 1 /\ b >= 0 ] (?, 1) f5(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, e1 + 1, 1, c2, p, p, d2, j, d2, h2, v, v, i, k, i2, j2, k2, g2, j, e1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, e1 + 1, 1, c2, p, p, d2, j, d2, h2, v, v, i, k, i2, j2, k2, g2, j, e1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, e1 + 1, 1, c2, p, p, d2, j, d2, h2, v, v, i, k, i2, j2, k2, g2, j, e1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, e1 + 1, 1, c2, p, p, d2, j, d2, h2, v, v, i, k, i2, j2, k2, g2, j, e1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, e1 + 1, 1, c2, p, p, d2, j, d2, h2, v, v, i, k, i2, j2, k2, g2, j, e1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, e1 + 1, 1, c2, p, p, d2, j, d2, h2, v, v, i, k, i2, j2, k2, g2, j, e1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, e1 + 1, 1, c2, p, p, d2, j, d2, h2, v, v, i, k, i2, j2, k2, g2, j, e1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, e1 + 1, 1, c2, p, p, d2, j, d2, h2, v, v, i, k, i2, j2, k2, g2, j, e1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, e1 + 1, 1, c2, p, p, d2, j, d2, h2, v, v, i, k, i2, j2, k2, g2, j, e1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, e1 + 1, 1, c2, p, p, d2, j, d2, h2, v, v, i, k, i2, j2, k2, g2, j, e1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, e1 + 1, 1, c2, p, p, d2, j, d2, h2, v, v, i, k, i2, j2, k2, g2, j, e1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, e1 + 1, 1, c2, p, p, d2, j, d2, h2, v, v, i, k, i2, j2, k2, g2, j, e1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, e1 + 1, 1, c2, p, p, d2, j, d2, h2, v, v, i, k, i2, j2, k2, g2, j, e1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, e1 + 1, 1, c2, p, p, d2, j, d2, h2, v, v, i, k, i2, j2, k2, g2, j, e1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, e1 + 1, 1, c2, p, p, d2, j, d2, h2, v, v, i, k, i2, j2, k2, g2, j, e1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, e1 + 1, 1, c2, p, p, d2, j, d2, h2, v, v, i, k, i2, j2, k2, g2, j, e1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(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) -> f4(a, b, c, d, e, f, g, h, i, h2, k, l, m, c2, d2, k2, j2, g2, s, t, u, v, w, x, y, z, a1, b1, e2, d1, e1, i2, f2, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ l >= 0 /\ d2 >= f2 + 1 /\ c2 >= 2 /\ j = p ] (?, 1) f5(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) -> f4(a, b, c, d, e, f, g, h, i, h2, k, l, m, c2, d2, k2, j2, g2, s, t, u, v, w, x, y, z, a1, b1, e2, d1, e1, i2, f2, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ l >= 0 /\ f2 >= d2 + 1 /\ c2 >= 2 /\ j = p ] (?, 1) f6(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1, f1, g1, h2, i2, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ j2 >= k + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1, f1, g1, h2, i2, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ j2 >= k + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1, f1, g1, h2, i2, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ j2 >= k + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1, f1, g1, h2, i2, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ j2 >= k + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1, f1, g1, h2, i2, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ k >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1, f1, g1, h2, i2, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ k >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1, f1, g1, h2, i2, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ k >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1, f1, g1, h2, i2, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ k >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(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) -> f4(a, b, c, d, e, f, g, h, i, h2, k, l, m, c2, d2, k2, j2, g2, s, t, u, v, w, x, y, z, a1, b1, e2, d1, e1, i2, g1, h1, i1, f2, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ d1 >= 0 /\ c2 >= 2 /\ d2 >= f2 + 1 /\ d2 >= k + 1 /\ j = p ] (?, 1) f6(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) -> f4(a, b, c, d, e, f, g, h, i, h2, k, l, m, c2, d2, k2, j2, g2, s, t, u, v, w, x, y, z, a1, b1, e2, d1, e1, i2, g1, h1, i1, f2, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ d1 >= 0 /\ c2 >= 2 /\ d2 >= f2 + 1 /\ k >= d2 + 1 /\ j = p ] (?, 1) f6(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) -> f4(a, b, c, d, e, f, g, h, i, h2, k, l, m, c2, d2, k2, j2, g2, s, t, u, v, w, x, y, z, a1, b1, e2, d1, e1, i2, g1, h1, i1, f2, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ d1 >= 0 /\ c2 >= 2 /\ f2 >= d2 + 1 /\ d2 >= k + 1 /\ j = p ] (?, 1) f6(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) -> f4(a, b, c, d, e, f, g, h, i, h2, k, l, m, c2, d2, k2, j2, g2, s, t, u, v, w, x, y, z, a1, b1, e2, d1, e1, i2, g1, h1, i1, f2, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ d1 >= 0 /\ c2 >= 2 /\ f2 >= d2 + 1 /\ k >= d2 + 1 /\ j = p ] (?, 1) f7(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1 - 1, f1, g1, h1, i1, j1, h2, i2, v, i, k, m + 1, e1 - 1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1 - 1, f1, g1, h1, i1, j1, h2, i2, v, i, k, m + 1, e1 - 1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1 - 1, f1, g1, h1, i1, j1, h2, i2, v, i, k, m + 1, e1 - 1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1 - 1, f1, g1, h1, i1, j1, h2, i2, v, i, k, m + 1, e1 - 1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1 - 1, f1, g1, h1, i1, j1, h2, i2, v, i, k, m + 1, e1 - 1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1 - 1, f1, g1, h1, i1, j1, h2, i2, v, i, k, m + 1, e1 - 1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1 - 1, f1, g1, h1, i1, j1, h2, i2, v, i, k, m + 1, e1 - 1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1 - 1, f1, g1, h1, i1, j1, h2, i2, v, i, k, m + 1, e1 - 1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1 - 1, f1, g1, h1, i1, j1, h2, i2, v, i, k, m + 1, e1 - 1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1 - 1, f1, g1, h1, i1, j1, h2, i2, v, i, k, m + 1, e1 - 1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1 - 1, f1, g1, h1, i1, j1, h2, i2, v, i, k, m + 1, e1 - 1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1 - 1, f1, g1, h1, i1, j1, h2, i2, v, i, k, m + 1, e1 - 1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1 - 1, f1, g1, h1, i1, j1, h2, i2, v, i, k, m + 1, e1 - 1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1 - 1, f1, g1, h1, i1, j1, h2, i2, v, i, k, m + 1, e1 - 1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1 - 1, f1, g1, h1, i1, j1, h2, i2, v, i, k, m + 1, e1 - 1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(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) -> f7(a, b, c, d, e, f, g, h, i, j, k, l, m + 1, c2, p, p, d2, j, d2, t, u, v, w, x, y, z, a1, b1, j, d1, e1 - 1, f1, g1, h1, i1, j1, h2, i2, v, i, k, m + 1, e1 - 1, r1, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(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) -> f4(a, b, c, d, e, f, g, h, i, h2, k, l, m, c2, d2, k2, j2, g2, s, t, u, v, w, x, y, z, a1, b1, e2, d1, e1, i2, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, f2, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ m >= 0 /\ e1 >= 0 /\ c2 >= 2 /\ d2 >= f2 + 1 /\ d2 >= k + 1 /\ j = p ] (?, 1) f7(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) -> f4(a, b, c, d, e, f, g, h, i, h2, k, l, m, c2, d2, k2, j2, g2, s, t, u, v, w, x, y, z, a1, b1, e2, d1, e1, i2, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, f2, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ m >= 0 /\ e1 >= 0 /\ c2 >= 2 /\ d2 >= f2 + 1 /\ k >= d2 + 1 /\ j = p ] (?, 1) f7(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) -> f4(a, b, c, d, e, f, g, h, i, h2, k, l, m, c2, d2, k2, j2, g2, s, t, u, v, w, x, y, z, a1, b1, e2, d1, e1, i2, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, f2, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ m >= 0 /\ e1 >= 0 /\ c2 >= 2 /\ f2 >= d2 + 1 /\ d2 >= k + 1 /\ j = p ] (?, 1) f7(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) -> f4(a, b, c, d, e, f, g, h, i, h2, k, l, m, c2, d2, k2, j2, g2, s, t, u, v, w, x, y, z, a1, b1, e2, d1, e1, i2, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, f2, s1, t1, u1, v1, w1, x1, y1, z1, a2, b2) [ m >= 0 /\ e1 >= 0 /\ c2 >= 2 /\ f2 >= d2 + 1 /\ k >= d2 + 1 /\ j = p ] (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) -> f4(c2, i2, h2, n2, m2, f, g, h, i, k2, k, l, m, j2, o, p2, o2, q2, s, t, u, v, w, x, y, z, a1, b1, r2, d1, e1, e2, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, d2, g2, f2, v1, w1, x1, y1, z1, a2, b2) [ 0 >= l2 /\ 0 >= n /\ 0 >= j2 ] (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) -> f1(n, 2, d2, h2, d2, f, g, h, i, j, k, l, m, n, c2, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, c2, t1, d2, i2, w1, x1, y1, z1, a2, b2) [ n >= 2 ] (?, 1) f1(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) -> f7(c2, i2, h2, m2, f2, f, g, h, i, j, j, e1, 0, j2, o, o, n2, j, n2, t, u, v, w, x, y, z, a1, b1, j, d1, e1, g2, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, d2, k2, e2, v1, e1 + 1, v, i, o2, p2, b2) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ o >= k + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] (?, 1) f1(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) -> f7(c2, i2, h2, m2, f2, f, g, h, i, j, j, e1, 0, j2, o, o, n2, j, n2, t, u, v, w, x, y, z, a1, b1, j, d1, e1, g2, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, d2, k2, e2, v1, e1 + 1, v, i, o2, p2, b2) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ k >= o + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] (?, 1) f1(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) -> f4(c2, i2, h2, n2, m2, f, g, h, i, k2, k, l, m, j2, o, p2, o2, q2, s, t, u, v, w, x, y, z, a1, b1, r2, d1, e1, e2, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, d2, g2, f2, v1, w1, x1, y1, z1, a2, b2) [ l2 >= 2 /\ w1 >= l2 /\ j2 >= 2 /\ w1 >= j2 /\ b >= a /\ w1 >= 0 /\ b >= 0 /\ o = j ] (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) -> f4(c2, i2, h2, m2, f2, f, g, h, i, j2, k, l, m, 1, j, o2, n2, p2, s, t, u, v, w, x, y, z, a1, b1, q2, d1, e1, g2, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, d2, k2, e2, v1, w1, x1, y1, z1, a2, b2) [ n = 1 ] (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) -> f4(c2, i2, h2, n2, m2, f, g, h, i, k2, k, l, m, 1, j2, p2, o2, q2, r2, t, u, v, w, x, y, z, a1, b1, l2, d1, e1, e2, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, d2, g2, f2, v1, w1, x1, y1, z1, a2, s2) [ 0 >= 1 /\ j2 >= s2 + 1 /\ n = 1 ] (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) -> f4(c2, i2, h2, n2, m2, f, g, h, i, k2, k, l, m, 1, j2, p2, o2, q2, r2, t, u, v, w, x, y, z, a1, b1, l2, d1, e1, e2, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, d2, g2, f2, v1, w1, x1, y1, z1, a2, s2) [ 0 >= 1 /\ s2 >= j2 + 1 /\ n = 1 ] (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) -> f4(c2, i2, h2, n2, m2, f, g, h, i, k2, k, l, m, 1, j2, p2, o2, q2, r2, t, u, v, w, x, y, z, a1, b1, l2, d1, e1, e2, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, d2, g2, f2, v1, w1, x1, y1, z1, a2, s2) [ 0 >= 1 /\ j2 >= s2 + 1 /\ n = 1 ] (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) -> f4(c2, i2, h2, n2, m2, f, g, h, i, k2, k, l, m, 1, j2, p2, o2, q2, r2, t, u, v, w, x, y, z, a1, b1, l2, d1, e1, e2, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, d2, g2, f2, v1, w1, x1, y1, z1, a2, s2) [ 0 >= 1 /\ s2 >= j2 + 1 /\ n = 1 ] start location: f3 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, j, k, l, m, n, o, p, d1, e1, w1]. We thus obtain the following problem: 2: T: (1, 1) f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(c2, i2, k2, k, l, m, 1, j2, p2, d1, e1, w1) [ 0 >= 1 /\ s2 >= j2 + 1 /\ n = 1 ] (1, 1) f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(c2, i2, k2, k, l, m, 1, j2, p2, d1, e1, w1) [ 0 >= 1 /\ j2 >= s2 + 1 /\ n = 1 ] (1, 1) f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(c2, i2, k2, k, l, m, 1, j2, p2, d1, e1, w1) [ 0 >= 1 /\ s2 >= j2 + 1 /\ n = 1 ] (1, 1) f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(c2, i2, k2, k, l, m, 1, j2, p2, d1, e1, w1) [ 0 >= 1 /\ j2 >= s2 + 1 /\ n = 1 ] (1, 1) f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(c2, i2, j2, k, l, m, 1, j, o2, d1, e1, w1) [ n = 1 ] (?, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(c2, i2, k2, k, l, m, j2, o, p2, d1, e1, w1) [ l2 >= 2 /\ w1 >= l2 /\ j2 >= 2 /\ w1 >= j2 /\ b >= a /\ w1 >= 0 /\ b >= 0 /\ o = j ] (?, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ k >= o + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] (?, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ o >= k + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] (1, 1) f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ] (1, 1) f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(c2, i2, k2, k, l, m, j2, o, p2, d1, e1, w1) [ 0 >= l2 /\ 0 >= n /\ 0 >= j2 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ m >= 0 /\ e1 >= 0 /\ c2 >= 2 /\ f2 >= d2 + 1 /\ k >= d2 + 1 /\ j = p ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ m >= 0 /\ e1 >= 0 /\ c2 >= 2 /\ f2 >= d2 + 1 /\ d2 >= k + 1 /\ j = p ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ m >= 0 /\ e1 >= 0 /\ c2 >= 2 /\ d2 >= f2 + 1 /\ k >= d2 + 1 /\ j = p ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ m >= 0 /\ e1 >= 0 /\ c2 >= 2 /\ d2 >= f2 + 1 /\ d2 >= k + 1 /\ j = p ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ d1 >= 0 /\ c2 >= 2 /\ f2 >= d2 + 1 /\ k >= d2 + 1 /\ j = p ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ d1 >= 0 /\ c2 >= 2 /\ f2 >= d2 + 1 /\ d2 >= k + 1 /\ j = p ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ d1 >= 0 /\ c2 >= 2 /\ d2 >= f2 + 1 /\ k >= d2 + 1 /\ j = p ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ d1 >= 0 /\ c2 >= 2 /\ d2 >= f2 + 1 /\ d2 >= k + 1 /\ j = p ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ k >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ k >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ k >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ k >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ j2 >= k + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ j2 >= k + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ j2 >= k + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ j2 >= k + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ l >= 0 /\ f2 >= d2 + 1 /\ c2 >= 2 /\ j = p ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ l >= 0 /\ d2 >= f2 + 1 /\ c2 >= 2 /\ j = p ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 0 Testing for unsatisfiable constraints removes the following transitions from problem 2: f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(c2, i2, k2, k, l, m, 1, j2, p2, d1, e1, w1) [ 0 >= 1 /\ s2 >= j2 + 1 /\ n = 1 ] f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(c2, i2, k2, k, l, m, 1, j2, p2, d1, e1, w1) [ 0 >= 1 /\ j2 >= s2 + 1 /\ n = 1 ] f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(c2, i2, k2, k, l, m, 1, j2, p2, d1, e1, w1) [ 0 >= 1 /\ s2 >= j2 + 1 /\ n = 1 ] f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(c2, i2, k2, k, l, m, 1, j2, p2, d1, e1, w1) [ 0 >= 1 /\ j2 >= s2 + 1 /\ n = 1 ] We thus obtain the following problem: 3: T: (1, 1) f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(c2, i2, j2, k, l, m, 1, j, o2, d1, e1, w1) [ n = 1 ] (?, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(c2, i2, k2, k, l, m, j2, o, p2, d1, e1, w1) [ l2 >= 2 /\ w1 >= l2 /\ j2 >= 2 /\ w1 >= j2 /\ b >= a /\ w1 >= 0 /\ b >= 0 /\ o = j ] (?, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ k >= o + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] (?, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ o >= k + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] (1, 1) f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ] (1, 1) f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(c2, i2, k2, k, l, m, j2, o, p2, d1, e1, w1) [ 0 >= l2 /\ 0 >= n /\ 0 >= j2 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ m >= 0 /\ e1 >= 0 /\ c2 >= 2 /\ f2 >= d2 + 1 /\ k >= d2 + 1 /\ j = p ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ m >= 0 /\ e1 >= 0 /\ c2 >= 2 /\ f2 >= d2 + 1 /\ d2 >= k + 1 /\ j = p ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ m >= 0 /\ e1 >= 0 /\ c2 >= 2 /\ d2 >= f2 + 1 /\ k >= d2 + 1 /\ j = p ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ m >= 0 /\ e1 >= 0 /\ c2 >= 2 /\ d2 >= f2 + 1 /\ d2 >= k + 1 /\ j = p ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ d1 >= 0 /\ c2 >= 2 /\ f2 >= d2 + 1 /\ k >= d2 + 1 /\ j = p ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ d1 >= 0 /\ c2 >= 2 /\ f2 >= d2 + 1 /\ d2 >= k + 1 /\ j = p ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ d1 >= 0 /\ c2 >= 2 /\ d2 >= f2 + 1 /\ k >= d2 + 1 /\ j = p ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ d1 >= 0 /\ c2 >= 2 /\ d2 >= f2 + 1 /\ d2 >= k + 1 /\ j = p ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ k >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ k >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ k >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ k >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ j2 >= k + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ j2 >= k + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ j2 >= k + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ j2 >= k + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ l >= 0 /\ f2 >= d2 + 1 /\ c2 >= 2 /\ j = p ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f4(a, b, h2, k, l, m, c2, d2, k2, d1, e1, w1) [ l >= 0 /\ d2 >= f2 + 1 /\ c2 >= 2 /\ j = p ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 3 produces the following problem: 4: T: (?, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ k >= o + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] (?, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ o >= k + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] (1, 1) f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ k >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ k >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ k >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ k >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ j2 >= k + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ j2 >= k + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ j2 >= k + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ j2 >= k + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] (?, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 13 Testing for reachability in the complexity graph removes the following transitions from problem 4: f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ k >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ k >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ k >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ k >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ j2 >= k + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ j2 >= k + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ j2 >= k + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] f6(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m, c2, p, p, d1, e1, w1) [ j2 >= k + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ c2 >= 2 /\ d1 >= 0 ] f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ f2 >= e2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ j >= e2 + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ k >= e2 + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ g2 >= e2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] f5(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, e1 + 1, 1, c2, p, p, e1, e1, w1) [ e2 >= f2 + 1 /\ e2 >= j + 1 /\ e2 >= k + 1 /\ e2 >= g2 + 1 /\ l >= 0 /\ c2 >= 2 /\ m = 1 ] We thus obtain the following problem: 5: T: (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\ b >= 0 ] (?, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ o >= k + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] (?, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ k >= o + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] (1, 1) f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ] start location: f3 leaf cost: 13 A polynomial rank function with Pol(f7) = -9 Pol(f1) = 2 Pol(f3) = 2 orients all transitions weakly and the transitions f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ o >= k + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ k >= o + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] strictly and produces the following problem: 6: T: (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\ b >= 0 ] (2, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ o >= k + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] (2, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ k >= o + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] (1, 1) f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ] start location: f3 leaf cost: 13 A polynomial rank function with Pol(f7) = V_11 + 3 Pol(f1) = -V_3 + V_4 + V_6 + V_11 + V_12 + 1 Pol(f3) = -V_3 + V_4 + V_6 + V_11 + V_12 + 1 orients all transitions weakly and the transitions f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] strictly and produces the following problem: 7: T: (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (?, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\ b >= 0 ] (2, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ o >= k + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] (2, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ k >= o + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] (1, 1) f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ] start location: f3 leaf cost: 13 A polynomial rank function with Pol(f1) = V_1 - V_2 and size complexities S("f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ]", 0-0) = n S("f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ]", 0-1) = 2 S("f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ]", 0-2) = j S("f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ]", 0-3) = k S("f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ]", 0-4) = l S("f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ]", 0-5) = m S("f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ]", 0-6) = n S("f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ]", 0-7) = ? S("f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ]", 0-8) = p S("f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ]", 0-9) = d1 S("f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ]", 0-10) = e1 S("f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ]", 0-11) = w1 S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ k >= o + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-0) = ? S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ k >= o + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-1) = ? S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ k >= o + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-2) = j S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ k >= o + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-3) = j S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ k >= o + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-4) = e1 S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ k >= o + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-5) = 0 S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ k >= o + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-6) = ? S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ k >= o + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-7) = ? S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ k >= o + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-8) = ? S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ k >= o + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-9) = d1 S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ k >= o + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-10) = e1 S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ k >= o + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-11) = e1 + 1 S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ o >= k + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-0) = ? S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ o >= k + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-1) = ? S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ o >= k + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-2) = j S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ o >= k + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-3) = j S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ o >= k + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-4) = e1 S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ o >= k + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-5) = 0 S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ o >= k + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-6) = ? S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ o >= k + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-7) = ? S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ o >= k + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-8) = ? S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ o >= k + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-9) = d1 S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ o >= k + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-10) = e1 S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\\ w1 >= q2 /\\ j2 >= 2 /\\ w1 >= j2 /\\ o >= k + 1 /\\ b >= a /\\ b >= 0 /\\ w1 >= 0 /\\ m = 0 /\\ j = k ]", 0-11) = e1 + 1 S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\\ b >= 0 ]", 0-0) = n S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\\ b >= 0 ]", 0-1) = n S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\\ b >= 0 ]", 0-2) = j S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\\ b >= 0 ]", 0-3) = k S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\\ b >= 0 ]", 0-4) = l S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\\ b >= 0 ]", 0-5) = m S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\\ b >= 0 ]", 0-6) = n S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\\ b >= 0 ]", 0-7) = ? S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\\ b >= 0 ]", 0-8) = p S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\\ b >= 0 ]", 0-9) = d1 S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\\ b >= 0 ]", 0-10) = e1 S("f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\\ b >= 0 ]", 0-11) = w1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-0) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-1) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-2) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-3) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-4) = e1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-5) = 16*j + 16*k + 16*m + 16*e1 + 16*w1 + 4096 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-6) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-7) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-8) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-9) = d1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-10) = e1 + 16 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-11) = e1 + 1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-0) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-1) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-2) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-3) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-4) = e1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-5) = 16*j + 16*k + 16*m + 16*e1 + 16*w1 + 4096 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-6) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-7) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-8) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-9) = d1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-10) = e1 + 16 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-11) = e1 + 1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-0) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-1) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-2) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-3) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-4) = e1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-5) = 16*j + 16*k + 16*m + 16*e1 + 16*w1 + 4096 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-6) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-7) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-8) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-9) = d1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-10) = e1 + 16 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-11) = e1 + 1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-0) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-1) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-2) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-3) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-4) = e1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-5) = 16*j + 16*k + 16*m + 16*e1 + 16*w1 + 4096 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-6) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-7) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-8) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-9) = d1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-10) = e1 + 16 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-11) = e1 + 1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-0) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-1) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-2) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-3) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-4) = e1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-5) = 16*j + 16*k + 16*m + 16*e1 + 16*w1 + 4096 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-6) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-7) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-8) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-9) = d1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-10) = e1 + 16 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-11) = e1 + 1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-0) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-1) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-2) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-3) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-4) = e1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-5) = 16*j + 16*k + 16*m + 16*e1 + 16*w1 + 4096 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-6) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-7) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-8) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-9) = d1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-10) = e1 + 16 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-11) = e1 + 1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-0) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-1) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-2) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-3) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-4) = e1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-5) = 16*j + 16*k + 16*m + 16*e1 + 16*w1 + 4096 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-6) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-7) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-8) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-9) = d1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-10) = e1 + 16 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-11) = e1 + 1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-0) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-1) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-2) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-3) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-4) = e1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-5) = 16*j + 16*k + 16*m + 16*e1 + 16*w1 + 4096 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-6) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-7) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-8) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-9) = d1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-10) = e1 + 16 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-11) = e1 + 1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-0) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-1) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-2) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-3) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-4) = e1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-5) = 16*j + 16*k + 16*m + 16*e1 + 16*w1 + 4096 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-6) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-7) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-8) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-9) = d1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-10) = e1 + 16 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-11) = e1 + 1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-0) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-1) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-2) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-3) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-4) = e1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-5) = 16*j + 16*k + 16*m + 16*e1 + 16*w1 + 4096 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-6) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-7) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-8) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-9) = d1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-10) = e1 + 16 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-11) = e1 + 1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-0) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-1) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-2) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-3) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-4) = e1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-5) = 16*j + 16*k + 16*m + 16*e1 + 16*w1 + 4096 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-6) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-7) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-8) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-9) = d1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-10) = e1 + 16 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-11) = e1 + 1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-0) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-1) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-2) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-3) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-4) = e1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-5) = 16*j + 16*k + 16*m + 16*e1 + 16*w1 + 4096 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-6) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-7) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-8) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-9) = d1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-10) = e1 + 16 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-11) = e1 + 1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-0) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-1) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-2) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-3) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-4) = e1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-5) = 16*j + 16*k + 16*m + 16*e1 + 16*w1 + 4096 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-6) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-7) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-8) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-9) = d1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-10) = e1 + 16 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ i2 >= j2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-11) = e1 + 1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-0) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-1) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-2) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-3) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-4) = e1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-5) = 16*j + 16*k + 16*m + 16*e1 + 16*w1 + 4096 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-6) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-7) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-8) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-9) = d1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-10) = e1 + 16 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j >= j2 + 1 /\\ j2 >= i2 + 1 /\\ j2 >= k + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-11) = e1 + 1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-0) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-1) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-2) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-3) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-4) = e1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-5) = 16*j + 16*k + 16*m + 16*e1 + 16*w1 + 4096 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-6) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-7) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-8) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-9) = d1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-10) = e1 + 16 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ i2 >= j2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-11) = e1 + 1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-0) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-1) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-2) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-3) = j S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-4) = e1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-5) = 16*j + 16*k + 16*m + 16*e1 + 16*w1 + 4096 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-6) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-7) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-8) = ? S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-9) = d1 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-10) = e1 + 16 S("f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\\ j2 >= j + 1 /\\ j2 >= i2 + 1 /\\ k >= j2 + 1 /\\ g2 >= 0 /\\ c2 >= 2 /\\ e1 >= 0 ]", 0-11) = e1 + 1 orients the transition f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\ b >= 0 ] weakly and the transition f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\ b >= 0 ] strictly and produces the following problem: 8: T: (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ j2 >= k2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ j2 >= i2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j2 >= j + 1 /\ i2 >= j2 + 1 /\ j2 >= k + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ j2 >= i2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (j + k + m + e1 + w1 + 1, 1) f7(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(a, b, j, k, l, m + 1, c2, p, p, d1, e1 - 1, w1) [ k2 >= j2 + 1 /\ j >= j2 + 1 /\ i2 >= j2 + 1 /\ k >= j2 + 1 /\ g2 >= 0 /\ c2 >= 2 /\ e1 >= 0 ] (n + 2, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(a, b + 1, j, k, l, m, n, o, p, d1, e1, w1) [ a >= b + 1 /\ b >= 0 ] (2, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ o >= k + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] (2, 1) f1(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f7(c2, i2, j, j, e1, 0, j2, o, o, d1, e1, e1 + 1) [ q2 >= 2 /\ w1 >= q2 /\ j2 >= 2 /\ w1 >= j2 /\ k >= o + 1 /\ b >= a /\ b >= 0 /\ w1 >= 0 /\ m = 0 /\ j = k ] (1, 1) f3(a, b, j, k, l, m, n, o, p, d1, e1, w1) -> f1(n, 2, j, k, l, m, n, c2, p, d1, e1, w1) [ n >= 2 ] start location: f3 leaf cost: 13 Complexity upper bound 16*j + 16*k + 16*m + 16*e1 + 16*w1 + n + 36 Time: 6.871 sec (SMT: 4.751 sec)