MAYBE Initial complexity problem: 1: T: (?, 1) f20(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) -> f26(a, 1, d, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) [ a >= 1 ] (?, 1) f20(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) -> f26(a, 1, d, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) [ 0 >= d /\ 0 >= a ] (?, 1) f20(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) -> f26(a, 0, d, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) [ d >= 1 /\ 0 >= a ] (?, 1) f26(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) -> f68(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) [ c >= e ] (?, 1) f26(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) -> f33(a, b, c, d, e, z, a1, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) [ z >= 1 /\ e >= c + 1 ] (?, 1) f26(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) -> f33(a, b, c, d, e, z, a1, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) [ e >= c + 1 /\ 0 >= z /\ 0 >= a1 ] (?, 1) f33(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) -> f39(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) [ h >= i + 1 ] (?, 1) f33(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) -> f39(a, b, c, d, e, f, g, h, i, -1, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) [ i >= h /\ j + 1 = 0 ] (?, 1) f33(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) -> f33(a, b, c, d, e, f, g, h, i + 1, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) [ i >= h /\ 0 >= j + 2 ] (?, 1) f33(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) -> f33(a, b, c, d, e, f, g, h, i + 1, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) [ i >= h /\ j >= 0 ] (?, 1) f39(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) -> f68(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) [ i >= h ] (?, 1) f39(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) -> f52(a, b, c, d, e, f, g, h, i, j, z, z, a1, b1, b1, p, q, r, s, t, u, v, w, x, y) [ 0 >= a1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f39(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) -> f52(a, b, c, d, e, f, g, h, i, j, z, z, a1, c1, c1, b1, q, r, s, t, u, v, w, x, y) [ 0 >= b1 /\ a1 >= 1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f52(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) -> f68(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, 3, z, s, t, u, v, w, x, y) [ o >= 0 /\ 0 >= z /\ q = 3 ] (?, 1) f52(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) -> f68(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, 3, z, s, t, u, v, w, x, y) [ o >= 0 /\ z >= 2 /\ q = 3 ] (?, 1) f52(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) -> f59(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, z, t, u, v, w, x, y) [ o >= 0 /\ 2 >= q ] (?, 1) f52(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) -> f59(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, z, t, u, v, w, x, y) [ o >= 0 /\ q >= 4 ] (?, 1) f52(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) -> f59(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, 3, 1, z, t, u, v, w, x, y) [ o >= 0 /\ q = 3 ] (?, 1) f59(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) -> f63(a, b, c, d, e, f, g, h, i, j, k, l, m, n, z, p, q, r, s, z, u, v, w, x, y) [ 10 >= s ] (?, 1) f59(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) -> f63(a, b, c, d, e, f, g, h, i, j, k, l, m, n, z, p, q, r, 10, z, u, v, w, x, y) [ s >= 11 ] (?, 1) f63(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) -> f26(a, b, c + 1, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) [ 0 >= o + 1 ] (?, 1) f26(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) -> f26(a, b, c + 1, d, e, z, a1, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) [ e >= c + 1 /\ 0 >= z /\ a1 >= 1 ] (?, 1) f39(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) -> f26(a, b, c + 1, d, e, f, g, h, i, j, z, z, m, n, o, p, q, r, s, t, u, v, w, x, y) [ h >= i + 1 /\ z >= 1 ] (?, 1) f39(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) -> f26(a, b, c + 1, d, e, f, g, h, i, j, z, z, a1, n, o, b1, q, r, s, t, u, v, w, x, y) [ b1 >= 1 /\ a1 >= 1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f52(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) -> f26(a, b, c + 1, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) [ 0 >= o + 1 ] (?, 1) f63(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) -> f26(a, b, c + 1, d, e, f, g, h, i, l, k, l, m, n, o, p, q, r, s, t, u + 1, v, w, x, y) [ o >= 0 ] (?, 1) f71(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) -> f71(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) (?, 1) f68(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) -> f71(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) [ 0 >= u ] (?, 1) f68(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) -> f71(1, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) [ u >= 1 ] (?, 1) f73(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) -> f76(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) (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) -> f20(c1, b, c, a1, z, f, g, h, 0, j, k, l, m, n, o, p, q, r, s, t, 0, 3, 1, b1, c1) [ a1 >= 0 /\ b1 >= 1 /\ v = 3 ] (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) -> f20(c1, b, c, a1, z, f, g, h, 0, j, k, l, m, n, o, p, q, r, s, t, 0, v, 1, b1, c1) [ 2 >= v /\ a1 >= 0 /\ b1 >= 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) -> f20(c1, b, c, a1, z, f, g, h, 0, j, k, l, m, n, o, p, q, r, s, t, 0, v, 1, b1, c1) [ v >= 4 /\ a1 >= 0 /\ b1 >= 1 ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, c, d, e, h, i, j, l, o, q, s, u, v]. We thus obtain the following problem: 2: T: (1, 1) f0(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f20(c1, c, a1, z, h, 0, j, l, o, q, s, 0, v) [ v >= 4 /\ a1 >= 0 /\ b1 >= 1 ] (1, 1) f0(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f20(c1, c, a1, z, h, 0, j, l, o, q, s, 0, v) [ 2 >= v /\ a1 >= 0 /\ b1 >= 1 ] (1, 1) f0(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f20(c1, c, a1, z, h, 0, j, l, o, q, s, 0, 3) [ a1 >= 0 /\ b1 >= 1 /\ v = 3 ] (?, 1) f73(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f76(a, c, d, e, h, i, j, l, o, q, s, u, v) (?, 1) f68(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(1, c, d, e, h, i, j, l, o, q, s, u, v) [ u >= 1 ] (?, 1) f68(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(0, c, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= u ] (?, 1) f71(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(a, c, d, e, h, i, j, l, o, q, s, u, v) (?, 1) f63(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, l, l, o, q, s, u + 1, v) [ o >= 0 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= o + 1 ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, z, o, q, s, u, v) [ b1 >= 1 /\ a1 >= 1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, z, o, q, s, u, v) [ h >= i + 1 /\ z >= 1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, l, o, q, s, u, v) [ e >= c + 1 /\ 0 >= z /\ a1 >= 1 ] (?, 1) f63(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= o + 1 ] (?, 1) f59(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f63(a, c, d, e, h, i, j, l, z, q, 10, u, v) [ s >= 11 ] (?, 1) f59(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f63(a, c, d, e, h, i, j, l, z, q, s, u, v) [ 10 >= s ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f59(a, c, d, e, h, i, j, l, o, 3, z, u, v) [ o >= 0 /\ q = 3 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f59(a, c, d, e, h, i, j, l, o, q, z, u, v) [ o >= 0 /\ q >= 4 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f59(a, c, d, e, h, i, j, l, o, q, z, u, v) [ o >= 0 /\ 2 >= q ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, 3, s, u, v) [ o >= 0 /\ z >= 2 /\ q = 3 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, 3, s, u, v) [ o >= 0 /\ 0 >= z /\ q = 3 ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f52(a, c, d, e, h, i, j, z, c1, q, s, u, v) [ 0 >= b1 /\ a1 >= 1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f52(a, c, d, e, h, i, j, z, b1, q, s, u, v) [ 0 >= a1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, q, s, u, v) [ i >= h ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i + 1, j, l, o, q, s, u, v) [ i >= h /\ j >= 0 ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i + 1, j, l, o, q, s, u, v) [ i >= h /\ 0 >= j + 2 ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f39(a, c, d, e, h, i, -1, l, o, q, s, u, v) [ i >= h /\ j + 1 = 0 ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f39(a, c, d, e, h, i, j, l, o, q, s, u, v) [ h >= i + 1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i, j, l, o, q, s, u, v) [ e >= c + 1 /\ 0 >= z /\ 0 >= a1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i, j, l, o, q, s, u, v) [ z >= 1 /\ e >= c + 1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, q, s, u, v) [ c >= e ] (?, 1) f20(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, d, d, e, h, i, j, l, o, q, s, u, v) [ d >= 1 /\ 0 >= a ] (?, 1) f20(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, d, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= d /\ 0 >= a ] (?, 1) f20(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, d, d, e, h, i, j, l, o, q, s, u, v) [ a >= 1 ] 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, c, d, e, h, i, j, l, o, q, s, u, v) -> f20(c1, c, a1, z, h, 0, j, l, o, q, s, 0, v) [ v >= 4 /\ a1 >= 0 /\ b1 >= 1 ] (1, 1) f0(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f20(c1, c, a1, z, h, 0, j, l, o, q, s, 0, v) [ 2 >= v /\ a1 >= 0 /\ b1 >= 1 ] (1, 1) f0(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f20(c1, c, a1, z, h, 0, j, l, o, q, s, 0, 3) [ a1 >= 0 /\ b1 >= 1 /\ v = 3 ] (?, 1) f68(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(1, c, d, e, h, i, j, l, o, q, s, u, v) [ u >= 1 ] (?, 1) f68(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(0, c, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= u ] (?, 1) f71(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(a, c, d, e, h, i, j, l, o, q, s, u, v) (?, 1) f63(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, l, l, o, q, s, u + 1, v) [ o >= 0 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= o + 1 ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, z, o, q, s, u, v) [ b1 >= 1 /\ a1 >= 1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, z, o, q, s, u, v) [ h >= i + 1 /\ z >= 1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, l, o, q, s, u, v) [ e >= c + 1 /\ 0 >= z /\ a1 >= 1 ] (?, 1) f63(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= o + 1 ] (?, 1) f59(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f63(a, c, d, e, h, i, j, l, z, q, 10, u, v) [ s >= 11 ] (?, 1) f59(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f63(a, c, d, e, h, i, j, l, z, q, s, u, v) [ 10 >= s ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f59(a, c, d, e, h, i, j, l, o, 3, z, u, v) [ o >= 0 /\ q = 3 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f59(a, c, d, e, h, i, j, l, o, q, z, u, v) [ o >= 0 /\ q >= 4 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f59(a, c, d, e, h, i, j, l, o, q, z, u, v) [ o >= 0 /\ 2 >= q ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, 3, s, u, v) [ o >= 0 /\ z >= 2 /\ q = 3 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, 3, s, u, v) [ o >= 0 /\ 0 >= z /\ q = 3 ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f52(a, c, d, e, h, i, j, z, c1, q, s, u, v) [ 0 >= b1 /\ a1 >= 1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f52(a, c, d, e, h, i, j, z, b1, q, s, u, v) [ 0 >= a1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, q, s, u, v) [ i >= h ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i + 1, j, l, o, q, s, u, v) [ i >= h /\ j >= 0 ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i + 1, j, l, o, q, s, u, v) [ i >= h /\ 0 >= j + 2 ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f39(a, c, d, e, h, i, -1, l, o, q, s, u, v) [ i >= h /\ j + 1 = 0 ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f39(a, c, d, e, h, i, j, l, o, q, s, u, v) [ h >= i + 1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i, j, l, o, q, s, u, v) [ e >= c + 1 /\ 0 >= z /\ 0 >= a1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i, j, l, o, q, s, u, v) [ z >= 1 /\ e >= c + 1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, q, s, u, v) [ c >= e ] (?, 1) f20(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, d, d, e, h, i, j, l, o, q, s, u, v) [ d >= 1 /\ 0 >= a ] (?, 1) f20(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, d, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= d /\ 0 >= a ] (?, 1) f20(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, d, d, e, h, i, j, l, o, q, s, u, v) [ a >= 1 ] start location: f0 leaf cost: 1 Repeatedly propagating knowledge in problem 3 produces the following problem: 4: T: (1, 1) f0(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f20(c1, c, a1, z, h, 0, j, l, o, q, s, 0, v) [ v >= 4 /\ a1 >= 0 /\ b1 >= 1 ] (1, 1) f0(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f20(c1, c, a1, z, h, 0, j, l, o, q, s, 0, v) [ 2 >= v /\ a1 >= 0 /\ b1 >= 1 ] (1, 1) f0(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f20(c1, c, a1, z, h, 0, j, l, o, q, s, 0, 3) [ a1 >= 0 /\ b1 >= 1 /\ v = 3 ] (?, 1) f68(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(1, c, d, e, h, i, j, l, o, q, s, u, v) [ u >= 1 ] (?, 1) f68(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(0, c, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= u ] (?, 1) f71(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(a, c, d, e, h, i, j, l, o, q, s, u, v) (?, 1) f63(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, l, l, o, q, s, u + 1, v) [ o >= 0 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= o + 1 ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, z, o, q, s, u, v) [ b1 >= 1 /\ a1 >= 1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, z, o, q, s, u, v) [ h >= i + 1 /\ z >= 1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, l, o, q, s, u, v) [ e >= c + 1 /\ 0 >= z /\ a1 >= 1 ] (?, 1) f63(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= o + 1 ] (?, 1) f59(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f63(a, c, d, e, h, i, j, l, z, q, 10, u, v) [ s >= 11 ] (?, 1) f59(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f63(a, c, d, e, h, i, j, l, z, q, s, u, v) [ 10 >= s ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f59(a, c, d, e, h, i, j, l, o, 3, z, u, v) [ o >= 0 /\ q = 3 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f59(a, c, d, e, h, i, j, l, o, q, z, u, v) [ o >= 0 /\ q >= 4 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f59(a, c, d, e, h, i, j, l, o, q, z, u, v) [ o >= 0 /\ 2 >= q ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, 3, s, u, v) [ o >= 0 /\ z >= 2 /\ q = 3 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, 3, s, u, v) [ o >= 0 /\ 0 >= z /\ q = 3 ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f52(a, c, d, e, h, i, j, z, c1, q, s, u, v) [ 0 >= b1 /\ a1 >= 1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f52(a, c, d, e, h, i, j, z, b1, q, s, u, v) [ 0 >= a1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, q, s, u, v) [ i >= h ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i + 1, j, l, o, q, s, u, v) [ i >= h /\ j >= 0 ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i + 1, j, l, o, q, s, u, v) [ i >= h /\ 0 >= j + 2 ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f39(a, c, d, e, h, i, -1, l, o, q, s, u, v) [ i >= h /\ j + 1 = 0 ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f39(a, c, d, e, h, i, j, l, o, q, s, u, v) [ h >= i + 1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i, j, l, o, q, s, u, v) [ e >= c + 1 /\ 0 >= z /\ 0 >= a1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i, j, l, o, q, s, u, v) [ z >= 1 /\ e >= c + 1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, q, s, u, v) [ c >= e ] (3, 1) f20(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, d, d, e, h, i, j, l, o, q, s, u, v) [ d >= 1 /\ 0 >= a ] (3, 1) f20(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, d, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= d /\ 0 >= a ] (3, 1) f20(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, d, d, e, h, i, j, l, o, q, s, u, v) [ a >= 1 ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f0) = 8 Pol(f20) = 8 Pol(f68) = 7 Pol(f71) = 6 Pol(f63) = 8 Pol(f26) = 8 Pol(f52) = 8 Pol(f39) = 8 Pol(f59) = 8 Pol(f33) = 8 orients all transitions weakly and the transitions f68(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(1, c, d, e, h, i, j, l, o, q, s, u, v) [ u >= 1 ] f68(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(0, c, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= u ] f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, 3, s, u, v) [ o >= 0 /\ z >= 2 /\ q = 3 ] f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, 3, s, u, v) [ o >= 0 /\ 0 >= z /\ q = 3 ] f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, q, s, u, v) [ c >= e ] strictly and produces the following problem: 5: T: (1, 1) f0(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f20(c1, c, a1, z, h, 0, j, l, o, q, s, 0, v) [ v >= 4 /\ a1 >= 0 /\ b1 >= 1 ] (1, 1) f0(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f20(c1, c, a1, z, h, 0, j, l, o, q, s, 0, v) [ 2 >= v /\ a1 >= 0 /\ b1 >= 1 ] (1, 1) f0(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f20(c1, c, a1, z, h, 0, j, l, o, q, s, 0, 3) [ a1 >= 0 /\ b1 >= 1 /\ v = 3 ] (8, 1) f68(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(1, c, d, e, h, i, j, l, o, q, s, u, v) [ u >= 1 ] (8, 1) f68(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(0, c, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= u ] (?, 1) f71(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(a, c, d, e, h, i, j, l, o, q, s, u, v) (?, 1) f63(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, l, l, o, q, s, u + 1, v) [ o >= 0 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= o + 1 ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, z, o, q, s, u, v) [ b1 >= 1 /\ a1 >= 1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, z, o, q, s, u, v) [ h >= i + 1 /\ z >= 1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, l, o, q, s, u, v) [ e >= c + 1 /\ 0 >= z /\ a1 >= 1 ] (?, 1) f63(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= o + 1 ] (?, 1) f59(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f63(a, c, d, e, h, i, j, l, z, q, 10, u, v) [ s >= 11 ] (?, 1) f59(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f63(a, c, d, e, h, i, j, l, z, q, s, u, v) [ 10 >= s ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f59(a, c, d, e, h, i, j, l, o, 3, z, u, v) [ o >= 0 /\ q = 3 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f59(a, c, d, e, h, i, j, l, o, q, z, u, v) [ o >= 0 /\ q >= 4 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f59(a, c, d, e, h, i, j, l, o, q, z, u, v) [ o >= 0 /\ 2 >= q ] (8, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, 3, s, u, v) [ o >= 0 /\ z >= 2 /\ q = 3 ] (8, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, 3, s, u, v) [ o >= 0 /\ 0 >= z /\ q = 3 ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f52(a, c, d, e, h, i, j, z, c1, q, s, u, v) [ 0 >= b1 /\ a1 >= 1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f52(a, c, d, e, h, i, j, z, b1, q, s, u, v) [ 0 >= a1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, q, s, u, v) [ i >= h ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i + 1, j, l, o, q, s, u, v) [ i >= h /\ j >= 0 ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i + 1, j, l, o, q, s, u, v) [ i >= h /\ 0 >= j + 2 ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f39(a, c, d, e, h, i, -1, l, o, q, s, u, v) [ i >= h /\ j + 1 = 0 ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f39(a, c, d, e, h, i, j, l, o, q, s, u, v) [ h >= i + 1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i, j, l, o, q, s, u, v) [ e >= c + 1 /\ 0 >= z /\ 0 >= a1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i, j, l, o, q, s, u, v) [ z >= 1 /\ e >= c + 1 ] (8, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, q, s, u, v) [ c >= e ] (3, 1) f20(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, d, d, e, h, i, j, l, o, q, s, u, v) [ d >= 1 /\ 0 >= a ] (3, 1) f20(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, d, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= d /\ 0 >= a ] (3, 1) f20(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, d, d, e, h, i, j, l, o, q, s, u, v) [ a >= 1 ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f0) = 1 Pol(f20) = 1 Pol(f68) = 0 Pol(f71) = 0 Pol(f63) = 1 Pol(f26) = 1 Pol(f52) = 1 Pol(f39) = 1 Pol(f59) = 1 Pol(f33) = 1 orients all transitions weakly and the transition f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, q, s, u, v) [ i >= h ] strictly and produces the following problem: 6: T: (1, 1) f0(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f20(c1, c, a1, z, h, 0, j, l, o, q, s, 0, v) [ v >= 4 /\ a1 >= 0 /\ b1 >= 1 ] (1, 1) f0(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f20(c1, c, a1, z, h, 0, j, l, o, q, s, 0, v) [ 2 >= v /\ a1 >= 0 /\ b1 >= 1 ] (1, 1) f0(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f20(c1, c, a1, z, h, 0, j, l, o, q, s, 0, 3) [ a1 >= 0 /\ b1 >= 1 /\ v = 3 ] (8, 1) f68(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(1, c, d, e, h, i, j, l, o, q, s, u, v) [ u >= 1 ] (8, 1) f68(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(0, c, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= u ] (?, 1) f71(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f71(a, c, d, e, h, i, j, l, o, q, s, u, v) (?, 1) f63(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, l, l, o, q, s, u + 1, v) [ o >= 0 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= o + 1 ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, z, o, q, s, u, v) [ b1 >= 1 /\ a1 >= 1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, z, o, q, s, u, v) [ h >= i + 1 /\ z >= 1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, l, o, q, s, u, v) [ e >= c + 1 /\ 0 >= z /\ a1 >= 1 ] (?, 1) f63(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, c + 1, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= o + 1 ] (?, 1) f59(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f63(a, c, d, e, h, i, j, l, z, q, 10, u, v) [ s >= 11 ] (?, 1) f59(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f63(a, c, d, e, h, i, j, l, z, q, s, u, v) [ 10 >= s ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f59(a, c, d, e, h, i, j, l, o, 3, z, u, v) [ o >= 0 /\ q = 3 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f59(a, c, d, e, h, i, j, l, o, q, z, u, v) [ o >= 0 /\ q >= 4 ] (?, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f59(a, c, d, e, h, i, j, l, o, q, z, u, v) [ o >= 0 /\ 2 >= q ] (8, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, 3, s, u, v) [ o >= 0 /\ z >= 2 /\ q = 3 ] (8, 1) f52(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, 3, s, u, v) [ o >= 0 /\ 0 >= z /\ q = 3 ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f52(a, c, d, e, h, i, j, z, c1, q, s, u, v) [ 0 >= b1 /\ a1 >= 1 /\ h >= i + 1 /\ 0 >= z ] (?, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f52(a, c, d, e, h, i, j, z, b1, q, s, u, v) [ 0 >= a1 /\ h >= i + 1 /\ 0 >= z ] (1, 1) f39(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, q, s, u, v) [ i >= h ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i + 1, j, l, o, q, s, u, v) [ i >= h /\ j >= 0 ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i + 1, j, l, o, q, s, u, v) [ i >= h /\ 0 >= j + 2 ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f39(a, c, d, e, h, i, -1, l, o, q, s, u, v) [ i >= h /\ j + 1 = 0 ] (?, 1) f33(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f39(a, c, d, e, h, i, j, l, o, q, s, u, v) [ h >= i + 1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i, j, l, o, q, s, u, v) [ e >= c + 1 /\ 0 >= z /\ 0 >= a1 ] (?, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f33(a, c, d, e, h, i, j, l, o, q, s, u, v) [ z >= 1 /\ e >= c + 1 ] (8, 1) f26(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f68(a, c, d, e, h, i, j, l, o, q, s, u, v) [ c >= e ] (3, 1) f20(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, d, d, e, h, i, j, l, o, q, s, u, v) [ d >= 1 /\ 0 >= a ] (3, 1) f20(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, d, d, e, h, i, j, l, o, q, s, u, v) [ 0 >= d /\ 0 >= a ] (3, 1) f20(a, c, d, e, h, i, j, l, o, q, s, u, v) -> f26(a, d, d, e, h, i, j, l, o, q, s, u, v) [ a >= 1 ] start location: f0 leaf cost: 1 Complexity upper bound ? Time: 14.396 sec (SMT: 8.862 sec)