MAYBE Initial complexity problem: 1: T: (?, 1) f78(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f80(0, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ a = 0 ] (?, 1) f37(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f41(a, b, b, h1, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ 0 >= b + 1 ] (?, 1) f37(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f41(a, b, b, h1, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ b >= 1 ] (?, 1) f89(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f48(a, b, c, d, e, h1, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ e >= 1 ] (?, 1) f61(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f66(a, b, c, d, e, f, g, g, 0, h1, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ 0 >= g + 1 ] (?, 1) f61(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f66(a, b, c, d, e, f, g, g, 0, h1, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ g >= 1 ] (?, 1) f80(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f84(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ 0 >= i + 1 ] (?, 1) f80(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f84(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ i >= 1 ] (?, 1) f77(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f78(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ 0 >= k + 1 ] (?, 1) f77(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f78(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ k >= 1 ] (?, 1) f77(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f80(a, b, c, d, e, f, g, h, i, j, 0, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ k = 0 ] (?, 1) f78(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f80(a, b, c, d, e, f, g, h, 1, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ 0 >= a + 1 ] (?, 1) f78(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f80(a, b, c, d, e, f, g, h, 1, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ a >= 1 ] (?, 1) f61(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f89(a, b, c, d, e - 1, f, 0, 0, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ g = 0 ] (?, 1) f84(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f89(a, b, c, d, e - 1, f, g, h, 0, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ i = 0 ] (?, 1) f94(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f94(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) (?, 1) f37(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f94(a, 0, 0, d, e, f, g, h, i, j, k, 1, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ b = 0 ] (?, 1) f41(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f94(a, b, c, 0, e, f, g, h, i, j, k, 1, 0, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ d = 0 ] (?, 1) f96(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f98(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) (?, 1) f89(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f94(a, b, c, d, e, f, g, h, i, j, k, 1, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ 0 >= e ] (?, 1) f84(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f89(a, b, c, d, e - 1, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ 0 >= i + 1 ] (?, 1) f84(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f89(a, b, c, d, e - 1, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ i >= 1 ] (?, 1) f80(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f84(a, b, c, d, e, f, g, h, 0, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ i = 0 ] (?, 1) f66(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f84(a, b, c, d, e, f, g, h, i, j, k, l, m, j, h1, h1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ 0 >= h1 + 1 ] (?, 1) f66(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f84(a, b, c, d, e, f, g, h, i, j, k, l, m, j, h1, h1, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ h1 >= 1 ] (?, 1) f66(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f80(a, b, c, d, e, f, g, h, i, j, k, l, m, j, 0, 0, 0, 0, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) (?, 1) f66(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f77(a, b, c, d, e, f, g, h, i, j, k, l, m, j, 0, 0, h1, h1, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ 0 >= h1 + 1 ] (?, 1) f66(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f77(a, b, c, d, e, f, g, h, i, j, k, l, m, j, 0, 0, h1, h1, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ h1 >= 1 ] (?, 1) f48(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f89(a, b, c, d, e - 1, f, g, h, i, j, k, l, m, n, o, p, q, r, f, 0, 0, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ f >= 0 ] (?, 1) f48(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f89(a, b, c, d, e - 1, f, g, h, i, j, k, l, m, n, o, p, q, r, f, 0, 0, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ 0 >= f + 2 ] (?, 1) f48(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f94(a, b, c, d, e, f, g, h, i, j, k, 1, m, n, o, p, q, r, f, h1, h1, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f94(a, b, c, d, e, f, g, h, i, j, k, 1, m, n, o, p, q, r, f, h1, h1, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ h1 >= 1 ] (?, 1) f48(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f61(a, b, c, d, e, -1, i1, h, i, j, k, l, m, n, o, p, q, r, -1, 0, 0, h1, h1, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f61(a, b, c, d, e, -1, i1, h, i, j, k, l, m, n, o, p, q, r, -1, 0, 0, h1, h1, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f89(a, b, c, d, e - 1, -1, g, h, i, j, k, l, m, n, o, p, q, r, -1, 0, 0, 0, 0, x, y, z, a1, b1, c1, d1, e1, f1, g1) [ f + 1 = 0 ] (?, 1) f41(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f48(a, b, c, d, h1, i1, g, h, i, j, k, l, d, n, o, p, q, r, s, t, u, v, w, h1, y, z, a1, b1, c1, d1, e1, f1, g1) [ 0 >= d + 1 ] (?, 1) f41(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f48(a, b, c, d, h1, i1, g, h, i, j, k, l, d, n, o, p, q, r, s, t, u, v, w, h1, y, z, a1, b1, c1, d1, e1, f1, g1) [ d >= 1 ] (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f94(a, b, c, d, l1, f, g, h, i, j, k, 1, m, n, o, p, q, r, s, t, u, v, w, x, h1, h1, i1, i1, j1, k1, k1, l1, g1) [ 0 >= i1 ] (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f37(a, n1, c, d, l1, f, g, h, i, j, k, j1, m, n, o, p, q, r, s, t, u, v, w, x, h1, 5, i1, i1, j1, k1, k1, l1, m1) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f37(a, n1, c, d, m1, f, g, h, i, j, k, k1, m, n, o, p, q, r, s, t, u, v, w, x, h1, i1, j1, j1, k1, l1, l1, m1, i1) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1) -> f37(a, n1, c, d, l1, f, g, h, i, j, k, j1, m, n, o, p, q, r, s, t, u, v, w, x, h1, 20, i1, i1, j1, k1, k1, l1, m1) [ i1 >= 1 /\ m1 >= 21 ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, d, e, f, g, i, k]. We thus obtain the following problem: 2: T: (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] (?, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (?, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ i = 0 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ i >= 1 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= i + 1 ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f96(a, b, d, e, f, g, i, k) -> f98(a, b, d, e, f, g, i, k) (?, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (?, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ i = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ g = 0 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ a >= 1 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ 0 >= a + 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, 0) [ k = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ 0 >= k + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ i >= 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ 0 >= i + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ 0 >= g + 1 ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (?, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(0, b, d, e, f, g, i, k) [ a = 0 ] start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] (?, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (?, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ i = 0 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ i >= 1 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= i + 1 ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (?, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ i = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ g = 0 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ a >= 1 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ 0 >= a + 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, 0) [ k = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ 0 >= k + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ i >= 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ 0 >= i + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ 0 >= g + 1 ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (?, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(0, b, d, e, f, g, i, k) [ a = 0 ] start location: f0 leaf cost: 1 Repeatedly propagating knowledge in problem 3 produces the following problem: 4: T: (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ i = 0 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ i >= 1 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= i + 1 ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ i = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ g = 0 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ a >= 1 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ 0 >= a + 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, 0) [ k = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ 0 >= k + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ i >= 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ 0 >= i + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ 0 >= g + 1 ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(0, b, d, e, f, g, i, k) [ a = 0 ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f0) = 1 Pol(f37) = 1 Pol(f94) = 0 Pol(f41) = 1 Pol(f48) = 1 Pol(f89) = 1 Pol(f61) = 1 Pol(f66) = 1 Pol(f77) = 1 Pol(f80) = 1 Pol(f84) = 1 Pol(f78) = 1 orients all transitions weakly and the transitions f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] strictly and produces the following problem: 5: T: (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ i = 0 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ i >= 1 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= i + 1 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ i = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ g = 0 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ a >= 1 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ 0 >= a + 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, 0) [ k = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ 0 >= k + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ i >= 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ 0 >= i + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ 0 >= g + 1 ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(0, b, d, e, f, g, i, k) [ a = 0 ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f0) = 1 Pol(f37) = 1 Pol(f94) = 0 Pol(f41) = 1 Pol(f48) = 1 Pol(f89) = 1 Pol(f61) = 1 Pol(f66) = 1 Pol(f77) = 1 Pol(f80) = 1 Pol(f84) = 1 Pol(f78) = 1 orients all transitions weakly and the transition f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] strictly and produces the following problem: 6: T: (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ i = 0 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ i >= 1 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= i + 1 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ i = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ g = 0 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ a >= 1 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ 0 >= a + 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, 0) [ k = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ 0 >= k + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ i >= 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ 0 >= i + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ 0 >= g + 1 ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(0, b, d, e, f, g, i, k) [ a = 0 ] start location: f0 leaf cost: 1 Applied AI with 'oct' on problem 6 to obtain the following invariants: For symbol f61: -X_5 - 1 >= 0 /\ X_5 + 1 >= 0 For symbol f66: -X_7 >= 0 /\ X_5 - X_7 + 1 >= 0 /\ -X_5 - X_7 - 1 >= 0 /\ X_7 >= 0 /\ X_5 + X_7 + 1 >= 0 /\ -X_5 + X_7 - 1 >= 0 /\ -X_5 - 1 >= 0 /\ X_5 + 1 >= 0 For symbol f77: -X_7 >= 0 /\ X_5 - X_7 + 1 >= 0 /\ -X_5 - X_7 - 1 >= 0 /\ X_7 >= 0 /\ X_5 + X_7 + 1 >= 0 /\ -X_5 + X_7 - 1 >= 0 /\ -X_5 - 1 >= 0 /\ X_5 + 1 >= 0 For symbol f78: -X_7 >= 0 /\ X_5 - X_7 + 1 >= 0 /\ -X_5 - X_7 - 1 >= 0 /\ X_7 >= 0 /\ X_5 + X_7 + 1 >= 0 /\ -X_5 + X_7 - 1 >= 0 /\ -X_5 - 1 >= 0 /\ X_5 + 1 >= 0 For symbol f80: -X_7 + 1 >= 0 /\ X_5 - X_7 + 2 >= 0 /\ -X_5 - X_7 >= 0 /\ X_7 >= 0 /\ X_5 + X_7 + 1 >= 0 /\ -X_5 + X_7 - 1 >= 0 /\ -X_5 - 1 >= 0 /\ X_5 + 1 >= 0 For symbol f84: -X_7 + 1 >= 0 /\ X_5 - X_7 + 2 >= 0 /\ -X_5 - X_7 >= 0 /\ X_7 >= 0 /\ X_5 + X_7 + 1 >= 0 /\ -X_5 + X_7 - 1 >= 0 /\ -X_5 - 1 >= 0 /\ X_5 + 1 >= 0 This yielded the following problem: 7: T: (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(0, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= i + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= i + 1 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] start location: f0 leaf cost: 1 Testing for unsatisfiable constraints removes the following transitions from problem 7: f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= i + 1 ] f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= i + 1 ] We thus obtain the following problem: 8: T: (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(0, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] start location: f0 leaf cost: 1 By chaining the transition f78(a, b, d, e, f, g, i, k) -> f80(0, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 ] with all transitions in problem 8, the following new transition is obtained: f78(a, b, d, e, f, g, i, k) -> f84(0, b, d, e, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] We thus obtain the following problem: 9: T: (?, 2) f78(a, b, d, e, f, g, i, k) -> f84(0, b, d, e, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] start location: f0 leaf cost: 1 By chaining the transition f78(a, b, d, e, f, g, i, k) -> f84(0, b, d, e, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] with all transitions in problem 9, the following new transition is obtained: f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] We thus obtain the following problem: 10: T: (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] start location: f0 leaf cost: 1 By chaining the transition f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] with all transitions in problem 10, the following new transition is obtained: f80(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] We thus obtain the following problem: 11: T: (?, 2) f80(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] start location: f0 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 11: f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] We thus obtain the following problem: 12: T: (?, 2) f80(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] start location: f0 leaf cost: 1 By chaining the transition f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 ] with all transitions in problem 12, the following new transition is obtained: f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] We thus obtain the following problem: 13: T: (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 2) f80(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] start location: f0 leaf cost: 1 By chaining the transition f78(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 ] with all transitions in problem 13, the following new transition is obtained: f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] We thus obtain the following problem: 14: T: (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 2) f80(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] start location: f0 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 14: f80(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i >= 1 ] We thus obtain the following problem: 15: T: (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] start location: f0 leaf cost: 1 By chaining the transition f77(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 ] with all transitions in problem 15, the following new transition is obtained: f77(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] We thus obtain the following problem: 16: T: (?, 2) f77(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] start location: f0 leaf cost: 1 By chaining the transition f77(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] with all transitions in problem 16, the following new transition is obtained: f77(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] We thus obtain the following problem: 17: T: (?, 3) f77(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 1) f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] start location: f0 leaf cost: 1 By chaining the transition f80(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] with all transitions in problem 17, the following new transition is obtained: f80(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] We thus obtain the following problem: 18: T: (?, 2) f80(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 3) f77(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] start location: f0 leaf cost: 1 By chaining the transition f66(a, b, d, e, f, g, i, k) -> f80(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 ] with all transitions in problem 18, the following new transition is obtained: f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] We thus obtain the following problem: 19: T: (?, 3) f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 2) f80(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 3) f77(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] start location: f0 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 19: f80(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] We thus obtain the following problem: 20: T: (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 3) f77(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 3) f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] start location: f0 leaf cost: 1 By chaining the transition f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] with all transitions in problem 20, the following new transition is obtained: f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] We thus obtain the following problem: 21: T: (?, 2) f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 3) f77(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 3) f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] start location: f0 leaf cost: 1 By chaining the transition f66(a, b, d, e, f, g, i, k) -> f84(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] with all transitions in problem 21, the following new transition is obtained: f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] We thus obtain the following problem: 22: T: (?, 2) f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] (?, 2) f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 3) f77(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 1) f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] (?, 3) f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] start location: f0 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 22: f84(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ i = 0 ] We thus obtain the following problem: 23: T: (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 3) f77(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 2) f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] (?, 2) f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] (?, 3) f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] start location: f0 leaf cost: 1 By chaining the transition f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] with all transitions in problem 23, the following new transitions are obtained: f78(a, b, d, e, f, g, i, k) -> f94(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 /\ 0 >= e - 1 ] f78(a, b, d, e, f, g, i, k) -> f48(a, b, d, e - 1, h1, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 /\ e - 1 >= 1 ] We thus obtain the following problem: 24: T: (?, 4) f78(a, b, d, e, f, g, i, k) -> f94(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 /\ 0 >= e - 1 ] (?, 4) f78(a, b, d, e, f, g, i, k) -> f48(a, b, d, e - 1, h1, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 /\ e - 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 3) f77(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 2) f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] (?, 2) f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] (?, 3) f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f78) = 1 Pol(f94) = 0 Pol(f48) = 1 Pol(f89) = 1 Pol(f77) = 1 Pol(f66) = 1 Pol(f61) = 1 Pol(f41) = 1 Pol(f37) = 1 Pol(f0) = 1 orients all transitions weakly and the transition f78(a, b, d, e, f, g, i, k) -> f94(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 /\ 0 >= e - 1 ] strictly and produces the following problem: 25: T: (1, 4) f78(a, b, d, e, f, g, i, k) -> f94(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 /\ 0 >= e - 1 ] (?, 4) f78(a, b, d, e, f, g, i, k) -> f48(a, b, d, e - 1, h1, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= a + 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 /\ e - 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 1, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a >= 1 /\ 0 >= 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 1 >= 1 ] (?, 3) f78(a, b, d, e, f, g, i, k) -> f89(0, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ a = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 3) f77(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, 0) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k = 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ k >= 1 ] (?, 1) f77(a, b, d, e, f, g, i, k) -> f78(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= k + 1 ] (?, 2) f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] (?, 2) f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 ] (?, 3) f66(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, 0, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ -i + 1 >= 0 /\ f - i + 2 >= 0 /\ -f - i >= 0 /\ i = 0 /\ 1 >= 0 /\ f + 2 >= 0 /\ -f >= 0 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ h1 >= 1 ] (?, 1) f66(a, b, d, e, f, g, i, k) -> f77(a, b, d, e, f, g, i, k) [ -i >= 0 /\ f - i + 1 >= 0 /\ -f - i - 1 >= 0 /\ i >= 0 /\ f + i + 1 >= 0 /\ -f + i - 1 >= 0 /\ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= h1 + 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, 0, i, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g = 0 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ g >= 1 ] (?, 1) f61(a, b, d, e, f, g, i, k) -> f66(a, b, d, e, f, g, 0, k) [ -f - 1 >= 0 /\ f + 1 >= 0 /\ 0 >= g + 1 ] (1, 1) f89(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= e ] (?, 1) f89(a, b, d, e, f, g, i, k) -> f48(a, b, d, e, h1, g, i, k) [ e >= 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, -1, g, i, k) [ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ h1 >= 1 /\ f + 1 = 0 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f61(a, b, d, e, -1, i1, i, k) [ 0 >= h1 + 1 /\ f + 1 = 0 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ h1 >= 1 ] (1, 1) f48(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) [ 0 >= h1 + 1 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ 0 >= f + 2 ] (?, 1) f48(a, b, d, e, f, g, i, k) -> f89(a, b, d, e - 1, f, g, i, k) [ f >= 0 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ d >= 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f48(a, b, d, h1, i1, g, i, k) [ 0 >= d + 1 ] (6, 1) f41(a, b, d, e, f, g, i, k) -> f94(a, b, 0, e, f, g, i, k) [ d = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f94(a, 0, d, e, f, g, i, k) [ b = 0 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ b >= 1 ] (3, 1) f37(a, b, d, e, f, g, i, k) -> f41(a, b, h1, e, f, g, i, k) [ 0 >= b + 1 ] (?, 1) f94(a, b, d, e, f, g, i, k) -> f94(a, b, d, e, f, g, i, k) (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ m1 >= 21 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, m1, f, g, i, k) [ j1 >= 1 /\ 20 >= i1 /\ i1 >= 5 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f37(a, n1, d, l1, f, g, i, k) [ i1 >= 1 /\ 4 >= m1 ] (1, 1) f0(a, b, d, e, f, g, i, k) -> f94(a, b, d, l1, f, g, i, k) [ 0 >= i1 ] start location: f0 leaf cost: 1 Complexity upper bound ? Time: 10.390 sec (SMT: 7.276 sec)