YES(?, 1068) Initial complexity problem: 1: T: (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f9(a, b + 1, c + 1, b1, b1, b1, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) [ a >= b + 1 /\ c >= 0 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f0(a, b, c, d, e, f, g, b1, i, h, e1, f1, c1, d1, g1, p, q, r, s, t, u, v, w, x, y, z, a1) [ d1 >= c1 + 1 /\ g >= 0 /\ h >= 1 /\ i >= 1 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f0(a, b, c, d, e, f, g, b1, i, h, e1, f1, c1, d1, g1, p, q, r, s, t, u, v, w, x, y, z, a1) [ d1 >= c1 + 1 /\ g >= 0 /\ 0 >= h + 1 /\ i >= 1 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f5(a, b, c, d, e, f, g - 1, r, i + 1, 0, f1, c1, m, d1, o, e1, r, p, b1, i + 1, g - 1, i, w, x, y, z, a1) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ h >= 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f5(a, b, c, d, e, f, g - 1, r, i + 1, 0, f1, c1, m, d1, o, e1, r, p, b1, i + 1, g - 1, i, w, x, y, z, a1) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ 0 >= h + 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f5(a, b, c, d, e, f, g - 1, r, i + 1, 0, f1, c1, m, d1, o, e1, r, p, b1, i + 1, g - 1, i, w, x, y, z, a1) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ h >= 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f5(a, b, c, d, e, f, g - 1, r, i + 1, 0, f1, c1, m, d1, o, e1, r, p, b1, i + 1, g - 1, i, w, x, y, z, a1) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ 0 >= h + 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f12(a, b, c, d, e, f, g, h, i, 0, e1, f1, m, c1, o, 0, r, r, s, t, u, i, b1, x, y, z, a1) [ m >= c1 /\ g >= 0 /\ h >= 1 /\ i >= 0 /\ p = 0 /\ j = 0 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f12(a, b, c, d, e, f, g, h, i, 0, e1, f1, m, c1, o, 0, r, r, s, t, u, i, b1, x, y, z, a1) [ m >= c1 /\ g >= 0 /\ 0 >= h + 1 /\ i >= 0 /\ p = 0 /\ j = 0 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f5(a, b, c, d, e, f, c - 3, b1, 1, 0, h1, i1, m, n, o, c1, b1, e1, f1, 1, c - 3, v, d, d, c - 2, d1, g1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ b1 >= 1 /\ b >= a /\ d >= 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f5(a, b, c, d, e, f, c - 3, b1, 1, 0, h1, i1, m, n, o, c1, b1, e1, f1, 1, c - 3, v, d, d, c - 2, d1, g1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ b1 >= 1 /\ b >= a /\ 0 >= d + 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f5(a, b, c, d, e, f, c - 3, b1, 1, 0, h1, i1, m, n, o, c1, b1, e1, f1, 1, c - 3, v, d, d, c - 2, d1, g1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ 0 >= b1 + 1 /\ b >= a /\ d >= 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f5(a, b, c, d, e, f, c - 3, b1, 1, 0, h1, i1, m, n, o, c1, b1, e1, f1, 1, c - 3, v, d, d, c - 2, d1, g1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ 0 >= b1 + 1 /\ b >= a /\ 0 >= d + 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f5(a, b, c, d, e, f, c - 3, b1, 1, 0, h1, i1, m, n, o, c1, b1, e1, f1, 1, c - 3, v, d, d, c - 2, d1, g1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ b1 >= 1 /\ b >= a /\ d >= 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f5(a, b, c, d, e, f, c - 3, b1, 1, 0, h1, i1, m, n, o, c1, b1, e1, f1, 1, c - 3, v, d, d, c - 2, d1, g1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ b1 >= 1 /\ b >= a /\ 0 >= d + 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f5(a, b, c, d, e, f, c - 3, b1, 1, 0, h1, i1, m, n, o, c1, b1, e1, f1, 1, c - 3, v, d, d, c - 2, d1, g1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ 0 >= b1 + 1 /\ b >= a /\ d >= 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f5(a, b, c, d, e, f, c - 3, b1, 1, 0, h1, i1, m, n, o, c1, b1, e1, f1, 1, c - 3, v, d, d, c - 2, d1, g1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ 0 >= b1 + 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f6(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1) -> f9(17, 1, 0, b1, b1, b1, g, h, i, j, k, l, m, n, o, p, e1, r, s, t, u, v, w, x, y, z, a1) start location: f6 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, d, g, h, i, j, m, p, r]. We thus obtain the following problem: 2: T: (1, 1) f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r) (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ 0 >= b1 + 1 /\ b >= a /\ 0 >= d + 1 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ 0 >= b1 + 1 /\ b >= a /\ d >= 1 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ b1 >= 1 /\ b >= a /\ 0 >= d + 1 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ b1 >= 1 /\ b >= a /\ d >= 1 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ 0 >= b1 + 1 /\ b >= a /\ 0 >= d + 1 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ 0 >= b1 + 1 /\ b >= a /\ d >= 1 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ b1 >= 1 /\ b >= a /\ 0 >= d + 1 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ b1 >= 1 /\ b >= a /\ d >= 1 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f12(a, b, c, d, g, h, i, 0, m, 0, r) [ m >= c1 /\ g >= 0 /\ 0 >= h + 1 /\ i >= 0 /\ p = 0 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f12(a, b, c, d, g, h, i, 0, m, 0, r) [ m >= c1 /\ g >= 0 /\ h >= 1 /\ i >= 0 /\ p = 0 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ 0 >= h + 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ h >= 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ 0 >= h + 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ h >= 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f0(a, b, c, d, g, b1, i, h, c1, p, r) [ d1 >= c1 + 1 /\ g >= 0 /\ 0 >= h + 1 /\ i >= 1 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f0(a, b, c, d, g, b1, i, h, c1, p, r) [ d1 >= c1 + 1 /\ g >= 0 /\ h >= 1 /\ i >= 1 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\ c >= 0 ] start location: f6 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (1, 1) f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r) (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ 0 >= b1 + 1 /\ b >= a /\ 0 >= d + 1 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ 0 >= b1 + 1 /\ b >= a /\ d >= 1 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ b1 >= 1 /\ b >= a /\ 0 >= d + 1 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ b1 >= 1 /\ b >= a /\ d >= 1 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ 0 >= b1 + 1 /\ b >= a /\ 0 >= d + 1 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ 0 >= b1 + 1 /\ b >= a /\ d >= 1 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ b1 >= 1 /\ b >= a /\ 0 >= d + 1 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ b1 >= 1 /\ b >= a /\ d >= 1 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ 0 >= h + 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ h >= 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ 0 >= h + 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ h >= 1 /\ j = 0 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\ c >= 0 ] start location: f6 leaf cost: 4 A polynomial rank function with Pol(f6) = 1 Pol(f9) = 1 Pol(f5) = -2 orients all transitions weakly and the transitions f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ b1 >= 1 /\ b >= a /\ d >= 1 ] f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ b1 >= 1 /\ b >= a /\ 0 >= d + 1 ] f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ 0 >= b1 + 1 /\ b >= a /\ d >= 1 ] f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ 0 >= b1 + 1 /\ b >= a /\ 0 >= d + 1 ] f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ b1 >= 1 /\ b >= a /\ d >= 1 ] f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ b1 >= 1 /\ b >= a /\ 0 >= d + 1 ] f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ 0 >= b1 + 1 /\ b >= a /\ d >= 1 ] strictly and produces the following problem: 4: T: (1, 1) f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r) (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ 0 >= b1 + 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ 0 >= b1 + 1 /\ b >= a /\ d >= 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ b1 >= 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ b1 >= 1 /\ b >= a /\ d >= 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ 0 >= b1 + 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ 0 >= b1 + 1 /\ b >= a /\ d >= 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ b1 >= 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ b1 >= 1 /\ b >= a /\ d >= 1 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ 0 >= h + 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ h >= 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ 0 >= h + 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ h >= 1 /\ j = 0 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\ c >= 0 ] start location: f6 leaf cost: 4 A polynomial rank function with Pol(f6) = 1 Pol(f9) = 1 Pol(f5) = -2 orients all transitions weakly and the transition f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ 0 >= b1 + 1 /\ b >= a /\ 0 >= d + 1 ] strictly and produces the following problem: 5: T: (1, 1) f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r) (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ 0 >= b1 + 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ 0 >= b1 + 1 /\ b >= a /\ d >= 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ b1 >= 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ b1 >= 1 /\ b >= a /\ d >= 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ 0 >= b1 + 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ 0 >= b1 + 1 /\ b >= a /\ d >= 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ b1 >= 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ b1 >= 1 /\ b >= a /\ d >= 1 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ 0 >= h + 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ h >= 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ 0 >= h + 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ h >= 1 /\ j = 0 ] (?, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\ c >= 0 ] start location: f6 leaf cost: 4 A polynomial rank function with Pol(f6) = 31 Pol(f9) = 2*V_1 - 2*V_2 - 1 Pol(f5) = 2*V_1 - 2*V_2 + V_3 - V_5 - 2*V_7 - 2 orients all transitions weakly and the transition f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\ c >= 0 ] strictly and produces the following problem: 6: T: (1, 1) f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r) (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ 0 >= b1 + 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ 0 >= b1 + 1 /\ b >= a /\ d >= 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ b1 >= 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ b1 >= 1 /\ b >= a /\ d >= 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ 0 >= b1 + 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ 0 >= b1 + 1 /\ b >= a /\ d >= 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ b1 >= 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ b1 >= 1 /\ b >= a /\ d >= 1 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ 0 >= h + 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ h >= 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ 0 >= h + 1 /\ j = 0 ] (?, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ h >= 1 /\ j = 0 ] (31, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\ c >= 0 ] start location: f6 leaf cost: 4 A polynomial rank function with Pol(f5) = V_5 + 1 and size complexities S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\\ c >= 0 ]", 0-0) = 17 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\\ c >= 0 ]", 0-1) = 32 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\\ c >= 0 ]", 0-2) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\\ c >= 0 ]", 0-3) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\\ c >= 0 ]", 0-4) = g S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\\ c >= 0 ]", 0-5) = h S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\\ c >= 0 ]", 0-6) = i S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\\ c >= 0 ]", 0-7) = j S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\\ c >= 0 ]", 0-8) = m S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\\ c >= 0 ]", 0-9) = p S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\\ c >= 0 ]", 0-10) = r S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ h >= 1 /\\ j = 0 ]", 0-0) = 17 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ h >= 1 /\\ j = 0 ]", 0-1) = 32 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ h >= 1 /\\ j = 0 ]", 0-2) = 31 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ h >= 1 /\\ j = 0 ]", 0-3) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ h >= 1 /\\ j = 0 ]", 0-4) = 31 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ h >= 1 /\\ j = 0 ]", 0-5) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ h >= 1 /\\ j = 0 ]", 0-6) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ h >= 1 /\\ j = 0 ]", 0-7) = 0 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ h >= 1 /\\ j = 0 ]", 0-8) = m S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ h >= 1 /\\ j = 0 ]", 0-9) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ h >= 1 /\\ j = 0 ]", 0-10) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-0) = 17 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-1) = 32 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-2) = 31 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-3) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-4) = 31 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-5) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-6) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-7) = 0 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-8) = m S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-9) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ p >= 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-10) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ h >= 1 /\\ j = 0 ]", 0-0) = 17 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ h >= 1 /\\ j = 0 ]", 0-1) = 32 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ h >= 1 /\\ j = 0 ]", 0-2) = 31 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ h >= 1 /\\ j = 0 ]", 0-3) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ h >= 1 /\\ j = 0 ]", 0-4) = 31 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ h >= 1 /\\ j = 0 ]", 0-5) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ h >= 1 /\\ j = 0 ]", 0-6) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ h >= 1 /\\ j = 0 ]", 0-7) = 0 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ h >= 1 /\\ j = 0 ]", 0-8) = m S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ h >= 1 /\\ j = 0 ]", 0-9) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ h >= 1 /\\ j = 0 ]", 0-10) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-0) = 17 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-1) = 32 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-2) = 31 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-3) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-4) = 31 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-5) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-6) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-7) = 0 S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-8) = m S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-9) = ? S("f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\\ g >= 0 /\\ i >= 0 /\\ 0 >= p + 1 /\\ 0 >= h + 1 /\\ j = 0 ]", 0-10) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-0) = 17 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-1) = 32 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-2) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-3) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-4) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-5) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-6) = 1 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-7) = 0 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-8) = m S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-9) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-10) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-0) = 17 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-1) = 32 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-2) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-3) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-4) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-5) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-6) = 1 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-7) = 0 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-8) = m S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-9) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-10) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-0) = 17 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-1) = 32 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-2) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-3) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-4) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-5) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-6) = 1 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-7) = 0 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-8) = m S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-9) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-10) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-0) = 17 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-1) = 32 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-2) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-3) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-4) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-5) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-6) = 1 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-7) = 0 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-8) = m S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-9) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ e1 >= 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-10) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-0) = 17 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-1) = 32 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-2) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-3) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-4) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-5) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-6) = 1 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-7) = 0 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-8) = m S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-9) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ d >= 1 ]", 0-10) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-0) = 17 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-1) = 32 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-2) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-3) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-4) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-5) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-6) = 1 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-7) = 0 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-8) = m S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-9) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ b1 >= 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-10) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-0) = 17 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-1) = 32 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-2) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-3) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-4) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-5) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-6) = 1 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-7) = 0 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-8) = m S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-9) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ d >= 1 ]", 0-10) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-0) = 17 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-1) = 32 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-2) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-3) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-4) = 31 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-5) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-6) = 1 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-7) = 0 S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-8) = m S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-9) = ? S("f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\\ c >= 2 /\\ 0 >= e1 + 1 /\\ 0 >= b1 + 1 /\\ b >= a /\\ 0 >= d + 1 ]", 0-10) = ? S("f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r)", 0-0) = 17 S("f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r)", 0-1) = 1 S("f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r)", 0-2) = 0 S("f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r)", 0-3) = ? S("f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r)", 0-4) = g S("f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r)", 0-5) = h S("f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r)", 0-6) = i S("f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r)", 0-7) = j S("f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r)", 0-8) = m S("f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r)", 0-9) = p S("f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r)", 0-10) = r orients the transitions f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ h >= 1 /\ j = 0 ] f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ 0 >= h + 1 /\ j = 0 ] f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ h >= 1 /\ j = 0 ] f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ 0 >= h + 1 /\ j = 0 ] weakly and the transitions f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ h >= 1 /\ j = 0 ] f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ 0 >= h + 1 /\ j = 0 ] f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ h >= 1 /\ j = 0 ] f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ 0 >= h + 1 /\ j = 0 ] strictly and produces the following problem: 7: T: (1, 1) f6(a, b, c, d, g, h, i, j, m, p, r) -> f9(17, 1, 0, b1, g, h, i, j, m, p, r) (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ 0 >= b1 + 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ 0 >= b1 + 1 /\ b >= a /\ d >= 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ b1 >= 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ 0 >= e1 + 1 /\ b1 >= 1 /\ b >= a /\ d >= 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ 0 >= b1 + 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ 0 >= b1 + 1 /\ b >= a /\ d >= 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ b1 >= 1 /\ b >= a /\ 0 >= d + 1 ] (1, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, c - 3, b1, 1, 0, m, c1, e1) [ d1 >= g1 /\ c >= 2 /\ e1 >= 1 /\ b1 >= 1 /\ b >= a /\ d >= 1 ] (256, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ 0 >= h + 1 /\ j = 0 ] (256, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ 0 >= p + 1 /\ h >= 1 /\ j = 0 ] (256, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ 0 >= h + 1 /\ j = 0 ] (256, 1) f5(a, b, c, d, g, h, i, j, m, p, r) -> f5(a, b, c, d, g - 1, r, i + 1, 0, m, e1, p) [ m >= d1 /\ g >= 0 /\ i >= 0 /\ p >= 1 /\ h >= 1 /\ j = 0 ] (31, 1) f9(a, b, c, d, g, h, i, j, m, p, r) -> f9(a, b + 1, c + 1, b1, g, h, i, j, m, p, r) [ a >= b + 1 /\ c >= 0 ] start location: f6 leaf cost: 4 Complexity upper bound 1068 Time: 1.945 sec (SMT: 1.519 sec)