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