MAYBE Initial complexity problem: 1: T: (1, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f1(x, x, x, x, x, x, x, x, x, j, k, l, m, n, o, p, q, r, s, t, u, v, w) (?, 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) -> f1(a, b, c, d, e, f, g, h, i, j, x, z, a1, b1, c1, d1, q, r, s, t, u, v, w) [ 0 >= y /\ 0 >= j + 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) -> f1(a, b, c, d, e, f, g, h, i, j, x, z, a1, b1, o, p, c1, d1, y, t, u, v, w) [ 0 >= j + 1 /\ e1 >= 1 /\ f1 >= 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) -> f1(a, b, c, d, e, f, g, h, i, j, x, l, m, z, a1, b1, q, r, s, c1, d1, y, w) [ 0 >= e1 + 2 /\ j >= 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) -> f1(a, b, c, d, e, f, g, h, i, j, x, l, m, z, o, p, a1, b1, c1, d1, y, e1, w) [ j >= 1 /\ f1 >= 0 /\ g1 + 1 >= 0 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f300(a, b, c, d, e, f, g, h, i, j, x, z, a1, b1, o, p, c1, r, s, t, u, v, d1) [ 1 >= y /\ 0 >= j + 1 /\ e1 >= 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) -> f300(a, b, c, d, e, f, g, h, i, j, x, l, m, z, o, p, a1, r, s, b1, c1, d1, y) [ 0 >= e1 + 1 /\ j >= 1 /\ f1 + 1 >= 0 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f300(a, b, c, d, e, f, g, h, i, j, x, l, m, n, o, p, q, r, s, z, u, v, a1) [ j = 0 ] start location: f2 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [j]. We thus obtain the following problem: 2: T: (?, 1) f1(j) -> f300(j) [ j = 0 ] (?, 1) f1(j) -> f300(j) [ 0 >= e1 + 1 /\ j >= 1 /\ f1 + 1 >= 0 ] (?, 1) f1(j) -> f300(j) [ 1 >= y /\ 0 >= j + 1 /\ e1 >= 1 ] (?, 1) f1(j) -> f1(j) [ j >= 1 /\ f1 >= 0 /\ g1 + 1 >= 0 ] (?, 1) f1(j) -> f1(j) [ 0 >= e1 + 2 /\ j >= 1 ] (?, 1) f1(j) -> f1(j) [ 0 >= j + 1 /\ e1 >= 1 /\ f1 >= 2 ] (?, 1) f1(j) -> f1(j) [ 0 >= y /\ 0 >= j + 1 ] (1, 1) f2(j) -> f1(j) start location: f2 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f1(j) -> f1(j) [ j >= 1 /\ f1 >= 0 /\ g1 + 1 >= 0 ] (?, 1) f1(j) -> f1(j) [ 0 >= e1 + 2 /\ j >= 1 ] (?, 1) f1(j) -> f1(j) [ 0 >= j + 1 /\ e1 >= 1 /\ f1 >= 2 ] (?, 1) f1(j) -> f1(j) [ 0 >= y /\ 0 >= j + 1 ] (1, 1) f2(j) -> f1(j) start location: f2 leaf cost: 3 Complexity upper bound ? Time: 0.204 sec (SMT: 0.193 sec)