MAYBE Initial complexity problem: 1: T: (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f1(a, b + 1, d, g1, d, h1, b, i, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) [ a >= b + 1 /\ b >= 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, b1, c1, d1, e1, f1) -> f10(a, b, c, d, e, f, g, h, i, j, k, m, m, m, g1, h1, h1, j, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) [ i1 >= j + 1 /\ k >= 0 /\ h1 >= i1 + 1 /\ g1 >= 2 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f10(a, b, c, d, e, f, g, h, i, j, k, m, m, m, g1, h1, h1, j, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) [ i1 >= j + 1 /\ k >= 0 /\ i1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f10(a, b, c, d, e, f, g, h, i, j, k, m, m, m, g1, h1, h1, j, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) [ j >= i1 + 1 /\ k >= 0 /\ h1 >= i1 + 1 /\ g1 >= 2 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f10(a, b, c, d, e, f, g, h, i, j, k, m, m, m, g1, h1, h1, j, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) [ j >= i1 + 1 /\ k >= 0 /\ i1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f4(a, b, c, d, e, f, g, h, i, m1, k, g1, l1, n, h1, j1, k1, n1, i1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) [ k >= 0 /\ g1 >= j1 + 1 /\ h1 >= 2 /\ m = j ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f4(a, b, c, d, e, f, g, h, i, m1, k, g1, l1, n, h1, j1, k1, n1, i1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) [ k >= 0 /\ j1 >= g1 + 1 /\ h1 >= 2 /\ m = j ] (?, 1) f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f10(a, b, c, d, e, f, g, h, i, j, k, m, m, m, g1, h1, h1, j, s, t - 1, i1, i, t - 1, x, y, z, a1, b1, c1, d1, e1, f1) [ j1 >= j + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f10(a, b, c, d, e, f, g, h, i, j, k, m, m, m, g1, h1, h1, j, s, t - 1, i1, i, t - 1, x, y, z, a1, b1, c1, d1, e1, f1) [ j1 >= j + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f10(a, b, c, d, e, f, g, h, i, j, k, m, m, m, g1, h1, h1, j, s, t - 1, i1, i, t - 1, x, y, z, a1, b1, c1, d1, e1, f1) [ j >= j1 + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f10(a, b, c, d, e, f, g, h, i, j, k, m, m, m, g1, h1, h1, j, s, t - 1, i1, i, t - 1, x, y, z, a1, b1, c1, d1, e1, f1) [ j >= j1 + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f4(a, b, c, d, e, f, g, h, i, k1, k, l, j1, n, g1, p, i1, l1, h1, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) [ g1 >= 2 /\ t >= 0 /\ m = j ] (1, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f4(j1, m1, l1, t1, s1, f, g, h, i, w1, k, x, v1, x, i1, x, u1, x1, q1, t, u, v, w, g1, h1, k1, n1, r1, c1, d1, e1, f1) [ 0 >= o1 /\ 0 >= i1 /\ 0 >= p1 ] (1, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f1(j1, 2, k1, l1, k1, f, g, h, i, j, k, g1, m, g1, j1, p, q, r, s, t, u, v, w, h1, i1, g1, a1, k1, m1, d1, e1, f1) [ j1 >= 2 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f10(h1, k1, j1, r1, q1, f, g, h, i, c, t, n, n, n, g1, c, c, c, m1, t, u, v, w, x, y, i1, l1, n1, c1, t + 1, i, s1) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ c >= n + 1 /\ k1 >= 0 /\ g1 >= 2 /\ n >= c + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f10(h1, k1, j1, r1, q1, f, g, h, i, c, t, n, n, n, g1, c, c, c, m1, t, u, v, w, x, y, i1, l1, n1, c1, t + 1, i, s1) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ c >= n + 1 /\ k1 >= 0 /\ g1 >= 2 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f10(h1, k1, j1, r1, q1, f, g, h, i, c, t, n, n, n, g1, c, c, c, m1, t, u, v, w, x, y, i1, l1, n1, c1, t + 1, i, s1) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ n >= c + 1 /\ k1 >= 0 /\ g1 >= 2 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f10(h1, k1, j1, r1, q1, f, g, h, i, c, t, n, n, n, g1, c, c, c, m1, t, u, v, w, x, y, i1, l1, n1, c1, t + 1, i, s1) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ n >= c + 1 /\ k1 >= 0 /\ g1 >= 2 /\ c >= n + 1 ] (1, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f4(j1, m1, l1, t1, s1, f, g, h, i, x1, k, g1, w1, d, 1, u1, v1, o1, q1, t, u, v, w, h1, i1, k1, n1, r1, c1, d1, e1, f1) [ 0 >= 1 /\ g1 >= u1 + 1 ] (1, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f4(j1, m1, l1, t1, s1, f, g, h, i, x1, k, g1, w1, d, 1, u1, v1, o1, q1, t, u, v, w, h1, i1, k1, n1, r1, c1, d1, e1, f1) [ 0 >= 1 /\ u1 >= g1 + 1 ] (1, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f4(j1, m1, l1, t1, s1, f, g, h, i, x1, k, g1, w1, d, 1, u1, v1, o1, q1, t, u, v, w, h1, i1, k1, n1, r1, c1, d1, e1, f1) [ 0 >= 1 /\ g1 >= u1 + 1 ] (1, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1) -> f4(j1, m1, l1, t1, s1, f, g, h, i, x1, k, g1, w1, d, 1, u1, v1, o1, q1, t, u, v, w, h1, i1, k1, n1, r1, c1, d1, e1, f1) [ 0 >= 1 /\ u1 >= g1 + 1 ] start location: f3 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, d, j, k, m, n, t, x]. We thus obtain the following problem: 2: T: (1, 1) f3(a, b, c, d, j, k, m, n, t, x) -> f4(j1, m1, l1, t1, x1, k, w1, d, t, h1) [ 0 >= 1 /\ u1 >= g1 + 1 ] (1, 1) f3(a, b, c, d, j, k, m, n, t, x) -> f4(j1, m1, l1, t1, x1, k, w1, d, t, h1) [ 0 >= 1 /\ g1 >= u1 + 1 ] (1, 1) f3(a, b, c, d, j, k, m, n, t, x) -> f4(j1, m1, l1, t1, x1, k, w1, d, t, h1) [ 0 >= 1 /\ u1 >= g1 + 1 ] (1, 1) f3(a, b, c, d, j, k, m, n, t, x) -> f4(j1, m1, l1, t1, x1, k, w1, d, t, h1) [ 0 >= 1 /\ g1 >= u1 + 1 ] (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ n >= c + 1 /\ k1 >= 0 /\ g1 >= 2 /\ c >= n + 1 ] (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ n >= c + 1 /\ k1 >= 0 /\ g1 >= 2 ] (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ c >= n + 1 /\ k1 >= 0 /\ g1 >= 2 ] (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ c >= n + 1 /\ k1 >= 0 /\ g1 >= 2 /\ n >= c + 1 ] (1, 1) f3(a, b, c, d, j, k, m, n, t, x) -> f1(j1, 2, k1, l1, j, k, m, g1, t, h1) [ j1 >= 2 ] (1, 1) f3(a, b, c, d, j, k, m, n, t, x) -> f4(j1, m1, l1, t1, w1, k, v1, x, t, g1) [ 0 >= o1 /\ 0 >= i1 /\ 0 >= p1 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f4(a, b, c, d, k1, k, j1, n, t, x) [ g1 >= 2 /\ t >= 0 /\ m = j ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j >= j1 + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j >= j1 + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j1 >= j + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j1 >= j + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] (?, 1) f9(a, b, c, d, j, k, m, n, t, x) -> f4(a, b, c, d, m1, k, l1, n, t, x) [ k >= 0 /\ j1 >= g1 + 1 /\ h1 >= 2 /\ m = j ] (?, 1) f9(a, b, c, d, j, k, m, n, t, x) -> f4(a, b, c, d, m1, k, l1, n, t, x) [ k >= 0 /\ g1 >= j1 + 1 /\ h1 >= 2 /\ m = j ] (?, 1) f9(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t, x) [ j >= i1 + 1 /\ k >= 0 /\ i1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f9(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t, x) [ j >= i1 + 1 /\ k >= 0 /\ h1 >= i1 + 1 /\ g1 >= 2 ] (?, 1) f9(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t, x) [ i1 >= j + 1 /\ k >= 0 /\ i1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f9(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t, x) [ i1 >= j + 1 /\ k >= 0 /\ h1 >= i1 + 1 /\ g1 >= 2 ] (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f1(a, b + 1, d, g1, j, k, m, n, t, x) [ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 0 Testing for unsatisfiable constraints removes the following transitions from problem 2: f3(a, b, c, d, j, k, m, n, t, x) -> f4(j1, m1, l1, t1, x1, k, w1, d, t, h1) [ 0 >= 1 /\ u1 >= g1 + 1 ] f3(a, b, c, d, j, k, m, n, t, x) -> f4(j1, m1, l1, t1, x1, k, w1, d, t, h1) [ 0 >= 1 /\ g1 >= u1 + 1 ] f3(a, b, c, d, j, k, m, n, t, x) -> f4(j1, m1, l1, t1, x1, k, w1, d, t, h1) [ 0 >= 1 /\ u1 >= g1 + 1 ] f3(a, b, c, d, j, k, m, n, t, x) -> f4(j1, m1, l1, t1, x1, k, w1, d, t, h1) [ 0 >= 1 /\ g1 >= u1 + 1 ] f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ n >= c + 1 /\ k1 >= 0 /\ g1 >= 2 /\ c >= n + 1 ] f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ c >= n + 1 /\ k1 >= 0 /\ g1 >= 2 /\ n >= c + 1 ] We thus obtain the following problem: 3: T: (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ n >= c + 1 /\ k1 >= 0 /\ g1 >= 2 ] (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ c >= n + 1 /\ k1 >= 0 /\ g1 >= 2 ] (1, 1) f3(a, b, c, d, j, k, m, n, t, x) -> f1(j1, 2, k1, l1, j, k, m, g1, t, h1) [ j1 >= 2 ] (1, 1) f3(a, b, c, d, j, k, m, n, t, x) -> f4(j1, m1, l1, t1, w1, k, v1, x, t, g1) [ 0 >= o1 /\ 0 >= i1 /\ 0 >= p1 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f4(a, b, c, d, k1, k, j1, n, t, x) [ g1 >= 2 /\ t >= 0 /\ m = j ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j >= j1 + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j >= j1 + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j1 >= j + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j1 >= j + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] (?, 1) f9(a, b, c, d, j, k, m, n, t, x) -> f4(a, b, c, d, m1, k, l1, n, t, x) [ k >= 0 /\ j1 >= g1 + 1 /\ h1 >= 2 /\ m = j ] (?, 1) f9(a, b, c, d, j, k, m, n, t, x) -> f4(a, b, c, d, m1, k, l1, n, t, x) [ k >= 0 /\ g1 >= j1 + 1 /\ h1 >= 2 /\ m = j ] (?, 1) f9(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t, x) [ j >= i1 + 1 /\ k >= 0 /\ i1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f9(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t, x) [ j >= i1 + 1 /\ k >= 0 /\ h1 >= i1 + 1 /\ g1 >= 2 ] (?, 1) f9(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t, x) [ i1 >= j + 1 /\ k >= 0 /\ i1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f9(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t, x) [ i1 >= j + 1 /\ k >= 0 /\ h1 >= i1 + 1 /\ g1 >= 2 ] (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f1(a, b + 1, d, g1, j, k, m, n, t, x) [ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 3 produces the following problem: 4: T: (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ n >= c + 1 /\ k1 >= 0 /\ g1 >= 2 ] (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ c >= n + 1 /\ k1 >= 0 /\ g1 >= 2 ] (1, 1) f3(a, b, c, d, j, k, m, n, t, x) -> f1(j1, 2, k1, l1, j, k, m, g1, t, h1) [ j1 >= 2 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j >= j1 + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j >= j1 + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j1 >= j + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j1 >= j + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] (?, 1) f9(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t, x) [ j >= i1 + 1 /\ k >= 0 /\ i1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f9(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t, x) [ j >= i1 + 1 /\ k >= 0 /\ h1 >= i1 + 1 /\ g1 >= 2 ] (?, 1) f9(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t, x) [ i1 >= j + 1 /\ k >= 0 /\ i1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f9(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t, x) [ i1 >= j + 1 /\ k >= 0 /\ h1 >= i1 + 1 /\ g1 >= 2 ] (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f1(a, b + 1, d, g1, j, k, m, n, t, x) [ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 4 Testing for reachability in the complexity graph removes the following transitions from problem 4: f9(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t, x) [ j >= i1 + 1 /\ k >= 0 /\ i1 >= h1 + 1 /\ g1 >= 2 ] f9(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t, x) [ j >= i1 + 1 /\ k >= 0 /\ h1 >= i1 + 1 /\ g1 >= 2 ] f9(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t, x) [ i1 >= j + 1 /\ k >= 0 /\ i1 >= h1 + 1 /\ g1 >= 2 ] f9(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t, x) [ i1 >= j + 1 /\ k >= 0 /\ h1 >= i1 + 1 /\ g1 >= 2 ] We thus obtain the following problem: 5: T: (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j1 >= j + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j1 >= j + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j >= j1 + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j >= j1 + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f1(a, b + 1, d, g1, j, k, m, n, t, x) [ a >= b + 1 /\ b >= 0 ] (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ c >= n + 1 /\ k1 >= 0 /\ g1 >= 2 ] (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ n >= c + 1 /\ k1 >= 0 /\ g1 >= 2 ] (1, 1) f3(a, b, c, d, j, k, m, n, t, x) -> f1(j1, 2, k1, l1, j, k, m, g1, t, h1) [ j1 >= 2 ] start location: f3 leaf cost: 4 A polynomial rank function with Pol(f10) = -5 Pol(f1) = 2 Pol(f3) = 2 orients all transitions weakly and the transitions f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ n >= c + 1 /\ k1 >= 0 /\ g1 >= 2 ] f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ c >= n + 1 /\ k1 >= 0 /\ g1 >= 2 ] strictly and produces the following problem: 6: T: (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j1 >= j + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j1 >= j + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j >= j1 + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] (?, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j >= j1 + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f1(a, b + 1, d, g1, j, k, m, n, t, x) [ a >= b + 1 /\ b >= 0 ] (2, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ c >= n + 1 /\ k1 >= 0 /\ g1 >= 2 ] (2, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ n >= c + 1 /\ k1 >= 0 /\ g1 >= 2 ] (1, 1) f3(a, b, c, d, j, k, m, n, t, x) -> f1(j1, 2, k1, l1, j, k, m, g1, t, h1) [ j1 >= 2 ] start location: f3 leaf cost: 4 A polynomial rank function with Pol(f10) = V_9 + 1 Pol(f1) = V_9 + 1 Pol(f3) = V_9 + 1 orients all transitions weakly and the transitions f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j1 >= j + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j1 >= j + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j >= j1 + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j >= j1 + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] strictly and produces the following problem: 7: T: (t + 1, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j1 >= j + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] (t + 1, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j1 >= j + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] (t + 1, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j >= j1 + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] (t + 1, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ j >= j1 + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f1(a, b + 1, d, g1, j, k, m, n, t, x) [ a >= b + 1 /\ b >= 0 ] (2, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ c >= n + 1 /\ k1 >= 0 /\ g1 >= 2 ] (2, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ n >= c + 1 /\ k1 >= 0 /\ g1 >= 2 ] (1, 1) f3(a, b, c, d, j, k, m, n, t, x) -> f1(j1, 2, k1, l1, j, k, m, g1, t, h1) [ j1 >= 2 ] start location: f3 leaf cost: 4 Applied AI with 'oct' on problem 7 to obtain the following invariants: For symbol f1: X_1 - X_2 >= 0 /\ X_2 - 2 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ X_1 - 2 >= 0 For symbol f10: X_6 - X_9 >= 0 /\ X_7 - X_8 >= 0 /\ -X_7 + X_8 >= 0 /\ X_2 - 2 >= 0 This yielded the following problem: 8: T: (1, 1) f3(a, b, c, d, j, k, m, n, t, x) -> f1(j1, 2, k1, l1, j, k, m, g1, t, h1) [ j1 >= 2 ] (2, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ n >= c + 1 /\ k1 >= 0 /\ g1 >= 2 ] (2, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f10(h1, k1, j1, r1, c, t, n, n, t, x) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ b >= a /\ b >= 0 /\ t1 >= g1 /\ u1 >= 2 /\ k1 >= u1 /\ c >= n + 1 /\ k1 >= 0 /\ g1 >= 2 ] (?, 1) f1(a, b, c, d, j, k, m, n, t, x) -> f1(a, b + 1, d, g1, j, k, m, n, t, x) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] (t + 1, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ k - t >= 0 /\ m - n >= 0 /\ -m + n >= 0 /\ b - 2 >= 0 /\ j >= j1 + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] (t + 1, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ k - t >= 0 /\ m - n >= 0 /\ -m + n >= 0 /\ b - 2 >= 0 /\ j >= j1 + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] (t + 1, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ k - t >= 0 /\ m - n >= 0 /\ -m + n >= 0 /\ b - 2 >= 0 /\ j1 >= j + 1 /\ t >= 0 /\ j1 >= h1 + 1 /\ g1 >= 2 ] (t + 1, 1) f10(a, b, c, d, j, k, m, n, t, x) -> f10(a, b, c, d, j, k, m, m, t - 1, x) [ k - t >= 0 /\ m - n >= 0 /\ -m + n >= 0 /\ b - 2 >= 0 /\ j1 >= j + 1 /\ t >= 0 /\ h1 >= j1 + 1 /\ g1 >= 2 ] start location: f3 leaf cost: 4 Complexity upper bound ? Time: 1.399 sec (SMT: 1.225 sec)