MAYBE Initial complexity problem: 1: T: (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f9(a, b + 1, d, o1, d, p1, b, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ a >= b + 1 /\ b >= 0 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(a, b, c, d, e, f, g, h, i, o1, l, l, p1, p1, s1, r1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ q1 >= h + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(a, b, c, d, e, f, g, h, i, o1, l, l, p1, p1, s1, r1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ q1 >= h + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(a, b, c, d, e, f, g, h, i, o1, l, l, p1, p1, s1, r1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ q1 >= h + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(a, b, c, d, e, f, g, h, i, o1, l, l, p1, p1, s1, r1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ q1 >= h + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(a, b, c, d, e, f, g, h, i, o1, l, l, p1, p1, s1, r1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ h >= q1 + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(a, b, c, d, e, f, g, h, i, o1, l, l, p1, p1, s1, r1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ h >= q1 + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(a, b, c, d, e, f, g, h, i, o1, l, l, p1, p1, s1, r1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ h >= q1 + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(a, b, c, d, e, f, g, h, i, o1, l, l, p1, p1, s1, r1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ h >= q1 + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(a, b, c, d, e, f, g, h, i, o1, l, l, p1, p1, o, p, q + 1, r - 1, s1, h, r1, q + 1, r - 1, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(a, b, c, d, e, f, g, h, i, o1, l, l, p1, p1, o, p, q + 1, r - 1, s1, h, r1, q + 1, r - 1, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(a, b, c, d, e, f, g, h, i, o1, l, l, p1, p1, o, p, q + 1, r - 1, s1, h, r1, q + 1, r - 1, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(a, b, c, d, e, f, g, h, i, o1, l, l, p1, p1, o, p, q + 1, r - 1, s1, h, r1, q + 1, r - 1, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(a, b, c, d, e, f, g, h, i, o1, l, l, p1, p1, o, p, q + 1, r - 1, s1, h, r1, q + 1, r - 1, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(a, b, c, d, e, f, g, h, i, o1, l, l, p1, p1, o, p, q + 1, r - 1, s1, h, r1, q + 1, r - 1, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(a, b, c, d, e, f, g, h, i, o1, l, l, p1, p1, o, p, q + 1, r - 1, s1, h, r1, q + 1, r - 1, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(a, b, c, d, e, f, g, h, i, o1, l, l, p1, p1, o, p, q + 1, r - 1, s1, h, r1, q + 1, r - 1, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 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) -> f7(a, b, c, d, e, f, g, h, i, o1, z, l, p1, n, o, p, q, r, s, t, u, v, w, x, y, z, p1, x, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= s1 + 1 ] (?, 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) -> f7(a, b, c, d, e, f, g, h, i, o1, z, l, p1, n, o, p, q, r, s, t, u, v, w, x, y, z, p1, x, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ s1 >= p1 + 1 ] (?, 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) -> f7(a, b, c, d, e, f, g, h, i, o1, z, l, p1, n, o, p, q, r, s, t, u, v, w, x, y, z, p1, x, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= s1 + 1 ] (?, 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) -> f7(a, b, c, d, e, f, g, h, i, o1, z, l, p1, n, o, p, q, r, s, t, u, v, w, x, y, z, p1, x, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ s1 >= p1 + 1 ] (?, 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) -> f7(a, b, c, d, e, f, g, h, i, o1, z, l, p1, n, o, p, q, r, s, t, u, v, w, x, y, z, p1, x, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= s1 + 1 ] (?, 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) -> f7(a, b, c, d, e, f, g, h, i, o1, z, l, p1, n, o, p, q, r, s, t, u, v, w, x, y, z, p1, x, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ s1 >= p1 + 1 ] (?, 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) -> f7(a, b, c, d, e, f, g, h, i, o1, z, l, p1, n, o, p, q, r, s, t, u, v, w, x, y, z, p1, x, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= s1 + 1 ] (?, 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) -> f7(a, b, c, d, e, f, g, h, i, o1, z, l, p1, n, o, p, q, r, s, t, u, v, w, x, y, z, p1, x, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ s1 >= p1 + 1 ] (?, 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) -> f18(a, b, c, d, e, f, g, h, i, o1, p1, l, r1, n, o, p, q, r, s, t, u, v, w, v1, y, t1, q1, w1, s1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= r1 + 1 /\ u1 >= 1 /\ z = x ] (?, 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) -> f18(a, b, c, d, e, f, g, h, i, o1, p1, l, r1, n, o, p, q, r, s, t, u, v, w, v1, y, t1, q1, w1, s1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= r1 + 1 /\ 0 >= u1 + 1 /\ z = x ] (?, 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) -> f18(a, b, c, d, e, f, g, h, i, o1, p1, l, r1, n, o, p, q, r, s, t, u, v, w, v1, y, t1, q1, w1, s1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ r1 >= p1 + 1 /\ u1 >= 1 /\ z = x ] (?, 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) -> f18(a, b, c, d, e, f, g, h, i, o1, p1, l, r1, n, o, p, q, r, s, t, u, v, w, v1, y, t1, q1, w1, s1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ r1 >= p1 + 1 /\ 0 >= u1 + 1 /\ z = x ] (?, 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) -> f7(a, b, c, d, e, f, g, h, i, o1, z, l, p1, n, o, p, q, 0, s1, t, u, v, w, x, y, z, p1, x, c1, r + d1 - 1, 0, r + d1 - 1, g1, h1, i1, j1, k1, l1, m1, n1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 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) -> f7(a, b, c, d, e, f, g, h, i, o1, z, l, p1, n, o, p, q, 0, s1, t, u, v, w, x, y, z, p1, x, c1, r + d1 - 1, 0, r + d1 - 1, g1, h1, i1, j1, k1, l1, m1, n1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 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) -> f7(a, b, c, d, e, f, g, h, i, o1, z, l, p1, n, o, p, q, 0, s1, t, u, v, w, x, y, z, p1, x, c1, r + d1 - 1, 0, r + d1 - 1, g1, h1, i1, j1, k1, l1, m1, n1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 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) -> f7(a, b, c, d, e, f, g, h, i, o1, z, l, p1, n, o, p, q, 0, s1, t, u, v, w, x, y, z, p1, x, c1, r + d1 - 1, 0, r + d1 - 1, g1, h1, i1, j1, k1, l1, m1, n1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 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) -> f7(a, b, c, d, e, f, g, h, i, o1, z, l, p1, n, o, p, q, 0, s1, t, u, v, w, x, y, z, p1, x, c1, r + d1 - 1, 0, r + d1 - 1, g1, h1, i1, j1, k1, l1, m1, n1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 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) -> f7(a, b, c, d, e, f, g, h, i, o1, z, l, p1, n, o, p, q, 0, s1, t, u, v, w, x, y, z, p1, x, c1, r + d1 - 1, 0, r + d1 - 1, g1, h1, i1, j1, k1, l1, m1, n1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 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) -> f7(a, b, c, d, e, f, g, h, i, o1, z, l, p1, n, o, p, q, 0, s1, t, u, v, w, x, y, z, p1, x, c1, r + d1 - 1, 0, r + d1 - 1, g1, h1, i1, j1, k1, l1, m1, n1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 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) -> f7(a, b, c, d, e, f, g, h, i, o1, z, l, p1, n, o, p, q, 0, s1, t, u, v, w, x, y, z, p1, x, c1, r + d1 - 1, 0, r + d1 - 1, g1, h1, i1, j1, k1, l1, m1, n1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 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) -> f18(a, b, c, d, e, f, g, h, i, o1, k, l, m, n, o, p, q, r, s, t, u, v, w, q1, y, r1, s1, t1, p1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ d1 >= 0 /\ r >= 0 /\ v1 >= 1 /\ o1 >= 2 /\ z = x ] (?, 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) -> f18(a, b, c, d, e, f, g, h, i, o1, k, l, m, n, o, p, q, r, s, t, u, v, w, q1, y, r1, s1, t1, p1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) [ d1 >= 0 /\ r >= 0 /\ 0 >= v1 + 1 /\ o1 >= 2 /\ z = x ] (1, 1) f17(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f9(p1, 2, r1, q1, r1, f, g, h, i, p1, s1, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, o1, s1, r1, t1, k1, l1, m1, n1) [ p1 >= 2 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(p1, q1, r1, a2, u1, f, g, c, r, o1, k, k, z1, z1, o, p, 1, r, b2, t, u, v, w, x, y, z, a1, b1, v1, d1, e1, f1, g1, s1, w1, j1, t1, r + 1, c2, n1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(p1, q1, r1, a2, u1, f, g, c, r, o1, k, k, z1, z1, o, p, 1, r, b2, t, u, v, w, x, y, z, a1, b1, v1, d1, e1, f1, g1, s1, w1, j1, t1, r + 1, c2, n1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(p1, q1, r1, a2, u1, f, g, c, r, o1, k, k, z1, z1, o, p, 1, r, b2, t, u, v, w, x, y, z, a1, b1, v1, d1, e1, f1, g1, s1, w1, j1, t1, r + 1, c2, n1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f16(p1, q1, r1, a2, u1, f, g, c, r, o1, k, k, z1, z1, o, p, 1, r, b2, t, u, v, w, x, y, z, a1, b1, v1, d1, e1, f1, g1, s1, w1, j1, t1, r + 1, c2, n1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (1, 1) f17(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f18(s1, t1, q1, z1, a2, f, g, x1, i, p1, k, c2, k, b2, o, p, q, r, s, t, u, v, w, h2, y, g2, y1, i2, w1, d1, e1, f1, o1, r1, u1, j1, v1, l1, m1, n1) [ 0 >= d2 /\ 0 >= e2 /\ 0 >= p1 /\ 0 >= f2 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f18(p1, q1, r1, a2, u1, f, g, c2, i, o1, c, b2, c, z1, o, p, q, r, s, t, u, v, w, g2, y, y1, x1, h2, v1, d1, e1, f1, g1, s1, w1, j1, t1, l1, m1, n1) [ i2 >= 2 /\ q1 >= i2 /\ d2 >= 2 /\ q1 >= d2 /\ b >= a /\ b >= 0 /\ q1 >= o1 /\ o1 >= 2 /\ q1 >= 0 /\ c = k ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f7(a, b, c, d, e, f, g, r1, q - 1, o1, k, s1, m, p1, o, p, d1 + 1, 0, s, t, u, v, w, m, d1, k, m, m, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, 0) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 1 /\ m >= k + 1 /\ i + 1 = q /\ r = 0 /\ l = h ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f7(a, b, c, d, e, f, g, r1, q - 1, o1, k, s1, m, p1, o, p, d1 + 1, 0, s, t, u, v, w, m, d1, k, m, m, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, 0) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 1 /\ i + 1 = q /\ r = 0 /\ l = h ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f7(a, b, c, d, e, f, g, r1, q - 1, o1, k, s1, m, p1, o, p, d1 + 1, 0, s, t, u, v, w, m, d1, k, m, m, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, 0) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 1 /\ i + 1 = q /\ r = 0 /\ l = h ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f7(a, b, c, d, e, f, g, r1, q - 1, o1, k, s1, m, p1, o, p, d1 + 1, 0, s, t, u, v, w, m, d1, k, m, m, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, 0) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 1 /\ k >= m + 1 /\ i + 1 = q /\ r = 0 /\ l = h ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f7(a, b, c, d, e, f, g, r1, i, o1, k, s1, m, p1, o, p, -r + d1 + 1, r, s, t, u, v, w, m, -r + d1, k, m, m, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, 0) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ m >= k + 1 /\ l = h ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f7(a, b, c, d, e, f, g, r1, i, o1, k, s1, m, p1, o, p, -r + d1 + 1, r, s, t, u, v, w, m, -r + d1, k, m, m, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, 0) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f7(a, b, c, d, e, f, g, r1, i, o1, k, s1, m, p1, o, p, -r + d1 + 1, r, s, t, u, v, w, m, -r + d1, k, m, m, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, 0) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f7(a, b, c, d, e, f, g, r1, i, o1, k, s1, m, p1, o, p, -r + d1 + 1, r, s, t, u, v, w, m, -r + d1, k, m, m, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, 0) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ k >= m + 1 /\ l = h ] (1, 1) f17(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f18(p1, q1, r1, a2, u1, f, g, c2, i, 1, d, b2, d, z1, o, p, q, r, s, t, u, v, w, g2, y, y1, x1, h2, v1, d1, e1, f1, o1, s1, w1, j1, t1, l1, m1, n1) (1, 1) f17(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f18(p1, q1, r1, z1, a2, f, g, y1, i, 1, t1, x1, b2, c2, o, p, q, r, s, t, u, v, w, i2, y, h2, g2, d2, w1, d1, e1, f1, o1, s1, u1, j1, v1, l1, m1, n1) [ 0 >= 1 /\ t1 >= b2 + 1 ] (1, 1) f17(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f18(p1, q1, r1, z1, a2, f, g, y1, i, 1, t1, x1, b2, c2, o, p, q, r, s, t, u, v, w, i2, y, h2, g2, d2, w1, d1, e1, f1, o1, s1, u1, j1, v1, l1, m1, n1) [ 0 >= 1 /\ b2 >= t1 + 1 ] (1, 1) f17(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f18(p1, q1, r1, z1, a2, f, g, y1, i, 1, t1, x1, b2, c2, o, p, q, r, s, t, u, v, w, i2, y, h2, g2, d2, w1, d1, e1, f1, o1, s1, u1, j1, v1, l1, m1, n1) [ 0 >= 1 /\ t1 >= b2 + 1 ] (1, 1) f17(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) -> f18(p1, q1, r1, z1, a2, f, g, y1, i, 1, t1, x1, b2, c2, o, p, q, r, s, t, u, v, w, i2, y, h2, g2, d2, w1, d1, e1, f1, o1, s1, u1, j1, v1, l1, m1, n1) [ 0 >= 1 /\ b2 >= t1 + 1 ] start location: f17 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1]. We thus obtain the following problem: 2: T: (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(p1, q1, r1, z1, y1, i, t1, x1, b2, q, r, i2, y, h2, d1) [ 0 >= 1 /\ b2 >= t1 + 1 ] (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(p1, q1, r1, z1, y1, i, t1, x1, b2, q, r, i2, y, h2, d1) [ 0 >= 1 /\ t1 >= b2 + 1 ] (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(p1, q1, r1, z1, y1, i, t1, x1, b2, q, r, i2, y, h2, d1) [ 0 >= 1 /\ b2 >= t1 + 1 ] (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(p1, q1, r1, z1, y1, i, t1, x1, b2, q, r, i2, y, h2, d1) [ 0 >= 1 /\ t1 >= b2 + 1 ] (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(p1, q1, r1, a2, c2, i, d, b2, d, q, r, g2, y, y1, d1) (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ k >= m + 1 /\ l = h ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ m >= k + 1 /\ l = h ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, q - 1, k, s1, m, d1 + 1, 0, m, d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 1 /\ k >= m + 1 /\ i + 1 = q /\ r = 0 /\ l = h ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, q - 1, k, s1, m, d1 + 1, 0, m, d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 1 /\ i + 1 = q /\ r = 0 /\ l = h ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, q - 1, k, s1, m, d1 + 1, 0, m, d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 1 /\ i + 1 = q /\ r = 0 /\ l = h ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, q - 1, k, s1, m, d1 + 1, 0, m, d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 1 /\ m >= k + 1 /\ i + 1 = q /\ r = 0 /\ l = h ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(p1, q1, r1, a2, c2, i, c, b2, c, q, r, g2, y, y1, d1) [ i2 >= 2 /\ q1 >= i2 /\ d2 >= 2 /\ q1 >= d2 /\ b >= a /\ b >= 0 /\ q1 >= o1 /\ o1 >= 2 /\ q1 >= 0 /\ c = k ] (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(s1, t1, q1, z1, x1, i, k, c2, k, q, r, h2, y, g2, d1) [ 0 >= d2 /\ 0 >= e2 /\ 0 >= p1 /\ 0 >= f2 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(p1, 2, r1, q1, h, i, s1, l, m, q, r, x, y, z, d1) [ p1 >= 2 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(a, b, c, d, h, i, k, l, m, q, r, q1, y, r1, d1) [ d1 >= 0 /\ r >= 0 /\ 0 >= v1 + 1 /\ o1 >= 2 /\ z = x ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(a, b, c, d, h, i, k, l, m, q, r, q1, y, r1, d1) [ d1 >= 0 /\ r >= 0 /\ v1 >= 1 /\ o1 >= 2 /\ z = x ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(a, b, c, d, h, i, p1, l, r1, q, r, v1, y, t1, d1) [ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ r1 >= p1 + 1 /\ 0 >= u1 + 1 /\ z = x ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(a, b, c, d, h, i, p1, l, r1, q, r, v1, y, t1, d1) [ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ r1 >= p1 + 1 /\ u1 >= 1 /\ z = x ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(a, b, c, d, h, i, p1, l, r1, q, r, v1, y, t1, d1) [ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= r1 + 1 /\ 0 >= u1 + 1 /\ z = x ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(a, b, c, d, h, i, p1, l, r1, q, r, v1, y, t1, d1) [ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= r1 + 1 /\ u1 >= 1 /\ z = x ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ s1 >= p1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= s1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ s1 >= p1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= s1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ s1 >= p1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= s1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ s1 >= p1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= s1 + 1 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ h >= q1 + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ h >= q1 + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ h >= q1 + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ h >= q1 + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ q1 >= h + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ q1 >= h + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ q1 >= h + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ q1 >= h + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(a, b + 1, d, o1, h, i, k, l, m, q, r, x, y, z, d1) [ a >= b + 1 /\ b >= 0 ] start location: f17 leaf cost: 0 Testing for unsatisfiable constraints removes the following transitions from problem 2: f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(p1, q1, r1, z1, y1, i, t1, x1, b2, q, r, i2, y, h2, d1) [ 0 >= 1 /\ b2 >= t1 + 1 ] f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(p1, q1, r1, z1, y1, i, t1, x1, b2, q, r, i2, y, h2, d1) [ 0 >= 1 /\ t1 >= b2 + 1 ] f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(p1, q1, r1, z1, y1, i, t1, x1, b2, q, r, i2, y, h2, d1) [ 0 >= 1 /\ b2 >= t1 + 1 ] f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(p1, q1, r1, z1, y1, i, t1, x1, b2, q, r, i2, y, h2, d1) [ 0 >= 1 /\ t1 >= b2 + 1 ] f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ k >= m + 1 /\ l = h ] f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ m >= k + 1 /\ l = h ] f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, q - 1, k, s1, m, d1 + 1, 0, m, d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 1 /\ k >= m + 1 /\ i + 1 = q /\ r = 0 /\ l = h ] f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, q - 1, k, s1, m, d1 + 1, 0, m, d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 1 /\ m >= k + 1 /\ i + 1 = q /\ r = 0 /\ l = h ] We thus obtain the following problem: 3: T: (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(p1, q1, r1, a2, c2, i, d, b2, d, q, r, g2, y, y1, d1) (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, q - 1, k, s1, m, d1 + 1, 0, m, d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 1 /\ i + 1 = q /\ r = 0 /\ l = h ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, q - 1, k, s1, m, d1 + 1, 0, m, d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 1 /\ i + 1 = q /\ r = 0 /\ l = h ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(p1, q1, r1, a2, c2, i, c, b2, c, q, r, g2, y, y1, d1) [ i2 >= 2 /\ q1 >= i2 /\ d2 >= 2 /\ q1 >= d2 /\ b >= a /\ b >= 0 /\ q1 >= o1 /\ o1 >= 2 /\ q1 >= 0 /\ c = k ] (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(s1, t1, q1, z1, x1, i, k, c2, k, q, r, h2, y, g2, d1) [ 0 >= d2 /\ 0 >= e2 /\ 0 >= p1 /\ 0 >= f2 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(p1, 2, r1, q1, h, i, s1, l, m, q, r, x, y, z, d1) [ p1 >= 2 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(a, b, c, d, h, i, k, l, m, q, r, q1, y, r1, d1) [ d1 >= 0 /\ r >= 0 /\ 0 >= v1 + 1 /\ o1 >= 2 /\ z = x ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(a, b, c, d, h, i, k, l, m, q, r, q1, y, r1, d1) [ d1 >= 0 /\ r >= 0 /\ v1 >= 1 /\ o1 >= 2 /\ z = x ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(a, b, c, d, h, i, p1, l, r1, q, r, v1, y, t1, d1) [ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ r1 >= p1 + 1 /\ 0 >= u1 + 1 /\ z = x ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(a, b, c, d, h, i, p1, l, r1, q, r, v1, y, t1, d1) [ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ r1 >= p1 + 1 /\ u1 >= 1 /\ z = x ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(a, b, c, d, h, i, p1, l, r1, q, r, v1, y, t1, d1) [ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= r1 + 1 /\ 0 >= u1 + 1 /\ z = x ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f18(a, b, c, d, h, i, p1, l, r1, q, r, v1, y, t1, d1) [ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= r1 + 1 /\ u1 >= 1 /\ z = x ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ s1 >= p1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= s1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ s1 >= p1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= s1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ s1 >= p1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= s1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ s1 >= p1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= s1 + 1 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ h >= q1 + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ h >= q1 + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ h >= q1 + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ h >= q1 + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ q1 >= h + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ q1 >= h + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ q1 >= h + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ q1 >= h + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(a, b + 1, d, o1, h, i, k, l, m, q, r, x, y, z, d1) [ a >= b + 1 /\ b >= 0 ] start location: f17 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 3 produces the following problem: 4: T: (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, q - 1, k, s1, m, d1 + 1, 0, m, d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 1 /\ i + 1 = q /\ r = 0 /\ l = h ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, q - 1, k, s1, m, d1 + 1, 0, m, d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 1 /\ i + 1 = q /\ r = 0 /\ l = h ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(p1, 2, r1, q1, h, i, s1, l, m, q, r, x, y, z, d1) [ p1 >= 2 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ s1 >= p1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= s1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ s1 >= p1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= s1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ s1 >= p1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= s1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ s1 >= p1 + 1 ] (?, 1) f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= s1 + 1 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ h >= q1 + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ h >= q1 + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ h >= q1 + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ h >= q1 + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ q1 >= h + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ q1 >= h + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ q1 >= h + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ q1 >= h + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(a, b + 1, d, o1, h, i, k, l, m, q, r, x, y, z, d1) [ a >= b + 1 /\ b >= 0 ] start location: f17 leaf cost: 9 Testing for reachability in the complexity graph removes the following transitions from problem 4: f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, q - 1, k, s1, m, d1 + 1, 0, m, d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 1 /\ i + 1 = q /\ r = 0 /\ l = h ] f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, q - 1, k, s1, m, d1 + 1, 0, m, d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 1 /\ i + 1 = q /\ r = 0 /\ l = h ] f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ s1 >= p1 + 1 ] f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= s1 + 1 ] f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ s1 >= p1 + 1 ] f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ x >= s1 + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= s1 + 1 ] f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ s1 >= p1 + 1 ] f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= s1 + 1 ] f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ s1 >= p1 + 1 ] f6(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, r, x, y, z, d1) [ s1 >= x + 1 /\ y >= 0 /\ r >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= s1 + 1 ] f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ h >= q1 + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ h >= q1 + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ h >= q1 + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ h >= q1 + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ q1 >= h + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ q1 >= h + 1 /\ r1 >= q1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ q1 >= h + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] f13(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q, r, x, y, z, d1) [ q1 >= h + 1 /\ q1 >= r1 + 1 /\ i >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] We thus obtain the following problem: 5: T: (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(a, b + 1, d, o1, h, i, k, l, m, q, r, x, y, z, d1) [ a >= b + 1 /\ b >= 0 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(p1, 2, r1, q1, h, i, s1, l, m, q, r, x, y, z, d1) [ p1 >= 2 ] start location: f17 leaf cost: 9 A polynomial rank function with Pol(f7) = -8 Pol(f16) = -7 Pol(f9) = 2 Pol(f17) = 2 orients all transitions weakly and the transitions f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] strictly and produces the following problem: 6: T: (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(a, b + 1, d, o1, h, i, k, l, m, q, r, x, y, z, d1) [ a >= b + 1 /\ b >= 0 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(p1, 2, r1, q1, h, i, s1, l, m, q, r, x, y, z, d1) [ p1 >= 2 ] start location: f17 leaf cost: 9 A polynomial rank function with Pol(f7) = -8 Pol(f16) = 1 Pol(f9) = 1 Pol(f17) = 1 orients all transitions weakly and the transition f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] strictly and produces the following problem: 7: T: (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (1, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(a, b + 1, d, o1, h, i, k, l, m, q, r, x, y, z, d1) [ a >= b + 1 /\ b >= 0 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(p1, 2, r1, q1, h, i, s1, l, m, q, r, x, y, z, d1) [ p1 >= 2 ] start location: f17 leaf cost: 9 A polynomial rank function with Pol(f7) = -8 Pol(f16) = 1 Pol(f9) = 1 Pol(f17) = 1 orients all transitions weakly and the transition f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] strictly and produces the following problem: 8: T: (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (1, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (1, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (?, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(a, b + 1, d, o1, h, i, k, l, m, q, r, x, y, z, d1) [ a >= b + 1 /\ b >= 0 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(p1, 2, r1, q1, h, i, s1, l, m, q, r, x, y, z, d1) [ p1 >= 2 ] start location: f17 leaf cost: 9 A polynomial rank function with Pol(f7) = -2*V_10 + V_11 + V_13 + V_15 - 6 Pol(f16) = V_10 + 2*V_11 + 1 Pol(f9) = -V_10 + 2*V_11 + 3 Pol(f17) = -V_10 + 2*V_11 + 3 orients all transitions weakly and the transitions f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] strictly and produces the following problem: 9: T: (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (1, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (1, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(a, b + 1, d, o1, h, i, k, l, m, q, r, x, y, z, d1) [ a >= b + 1 /\ b >= 0 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(p1, 2, r1, q1, h, i, s1, l, m, q, r, x, y, z, d1) [ p1 >= 2 ] start location: f17 leaf cost: 9 Applied AI with 'oct' on problem 9 to obtain the following invariants: For symbol f16: X_7 - X_8 >= 0 /\ -X_7 + X_8 >= 0 /\ -X_11 + X_6 >= 0 /\ X_2 - 2 >= 0 /\ X_10 + X_2 - 3 >= 0 /\ X_10 - 1 >= 0 For symbol f7: X_14 - X_7 >= 0 /\ -X_14 + X_7 >= 0 /\ X_6 >= 0 /\ X_2 + X_6 - 2 >= 0 /\ X_11 + X_6 >= 0 /\ -X_11 + X_6 >= 0 /\ X_2 - 2 >= 0 /\ X_11 + X_2 - 2 >= 0 /\ X_11 >= 0 For symbol f9: X_1 - X_2 >= 0 /\ X_2 - 2 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ X_1 - 2 >= 0 This yielded the following problem: 10: T: (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(p1, 2, r1, q1, h, i, s1, l, m, q, r, x, y, z, d1) [ p1 >= 2 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(a, b + 1, d, o1, h, i, k, l, m, q, r, x, y, z, d1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (1, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (1, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (?, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] start location: f17 leaf cost: 9 A polynomial rank function with Pol(f17) = V_10 + V_11 + V_15 Pol(f9) = V_10 + V_11 + V_15 Pol(f16) = V_6 + V_15 + 1 Pol(f7) = V_11 + V_15 + 1 orients all transitions weakly and the transitions f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] strictly and produces the following problem: 11: T: (1, 1) f17(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(p1, 2, r1, q1, h, i, s1, l, m, q, r, x, y, z, d1) [ p1 >= 2 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ k >= z1 + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ c >= k + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (2, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(p1, q1, r1, a2, c, r, k, k, z1, 1, r, x, y, z, d1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ x1 >= o1 /\ y1 >= 2 /\ q1 >= y1 /\ z1 >= k + 1 /\ b >= a /\ b >= 0 /\ k >= c + 1 /\ q1 >= 0 /\ o1 >= 2 /\ q = 1 ] (?, 1) f9(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f9(a, b + 1, d, o1, h, i, k, l, m, q, r, x, y, z, d1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ t1 >= q1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ t1 >= q1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ q1 >= t1 + 1 /\ r1 >= q1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ q1 >= p1 + 1 /\ o1 >= 2 ] (q + 2*r + 3, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f16(a, b, c, d, h, i, l, l, p1, q + 1, r - 1, x, y, z, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ q1 >= t1 + 1 /\ q1 >= r1 + 1 /\ q >= 0 /\ r >= 0 /\ p1 >= q1 + 1 /\ o1 >= 2 ] (1, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ q1 >= 2 /\ m >= k + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (1, 1) f16(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, r1, i, k, s1, m, -r + d1 + 1, r, m, -r + d1, k, d1) [ k - l >= 0 /\ -k + l >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ q + b - 3 >= 0 /\ q - 1 >= 0 /\ q1 >= 2 /\ k >= m + 1 /\ o1 >= 2 /\ q >= 0 /\ r >= 0 /\ l = h ] (q + r + d1, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (q + r + d1, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (q + r + d1, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (q + r + d1, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ x >= r1 + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] (q + r + d1, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ r1 >= p1 + 1 ] (q + r + d1, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ p1 >= z + 1 /\ p1 >= r1 + 1 ] (q + r + d1, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ r1 >= p1 + 1 ] (q + r + d1, 1) f7(a, b, c, d, h, i, k, l, m, q, r, x, y, z, d1) -> f7(a, b, c, d, h, i, z, l, p1, q, 0, x, y, z, r + d1 - 1) [ z - k >= 0 /\ -z + k >= 0 /\ i >= 0 /\ b + i - 2 >= 0 /\ r + i >= 0 /\ -r + i >= 0 /\ b - 2 >= 0 /\ r + b - 2 >= 0 /\ r >= 0 /\ r1 >= x + 1 /\ d1 >= 0 /\ q1 >= 0 /\ o1 >= 2 /\ z >= p1 + 1 /\ p1 >= r1 + 1 ] start location: f17 leaf cost: 9 Complexity upper bound ? Time: 15.484 sec (SMT: 8.876 sec)