MAYBE Initial complexity problem: 1: T: (1, 1) f30(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> 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, g1, h1, i1, j1) (?, 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, g1, h1, i1, j1) -> f2(k1, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) (?, 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, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> f3(a, 0, 0, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) (?, 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, g1, h1, i1, j1) -> f3(a, b + 1, c + 1, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) [ a >= b + 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, g1, h1, i1, j1) -> f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) [ b >= a ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> f5(a, b, c, 0, c, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) (?, 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, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> f5(a, b, c, d + 1, e - 1, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) [ e >= 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, g1, h1, i1, j1) -> f5(a, b, c, d, e, k1, l1, m1, n1, o1, p1, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> f1(a, b, c, d, e, k1, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) [ i >= h /\ f >= 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, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> f16(a, b, c, d, e, f + 1, g, h, i + 1, j, k, m, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) [ 0 >= e /\ f >= 0 ] (?, 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, g1, h1, i1, j1) -> f2(a, b, c, d, e, k1, g, h, i, j, k, l, o, o, o, 0, 0, o, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) [ l1 >= 1 /\ f >= 1 /\ n = 0 ] (?, 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, g1, h1, i1, j1) -> f25(a, b, c, d, e, k1, g, h, i, j, k, l, m, n, o, n, 0, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) [ f >= 1 /\ n >= 1 /\ k1 >= 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, g1, h1, i1, j1) -> f25(a, b, c, d, e, k1, g, h, i, j, k, l, m, n, o, n, 0, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) [ f >= 1 /\ 0 >= n + 1 /\ k1 >= 1 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> f17(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, j, 0, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) [ j >= 1 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> f17(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, j, 0, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) [ 0 >= j + 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, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> f18(a, b, c, d, e, k1, g, h, i, 0, k, l, m, n, o, p, q, r, 0, 0, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) [ k1 >= 0 /\ f >= 0 /\ j = 0 ] (?, 1) f12(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> f16(a, b, c, d, e, i, g, h, i + 1, j, k, m, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) (?, 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, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> f22(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, m, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> f21(a, b, c, d, e, f, g, h, i, 0, k, l, k1, n, o, p, q, r, 0, 0, 0, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) [ 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, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> f3(a, b, c, d, e, k1, n1, o1, p1, u1, k, m1, m, r1, t1, p, q, r, l1, 0, u, j, s1, v1, w1, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) [ f >= 0 /\ j >= 1 /\ q1 >= 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, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> f3(a, b, c, d, e, k1, n1, o1, p1, u1, k, m1, m, r1, t1, p, q, r, l1, 0, u, j, s1, v1, w1, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) [ f >= 0 /\ 0 >= j + 1 /\ q1 >= 0 ] (?, 1) f23(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> f4(a, b, c, d, e, f, k1, l1, m1, n1, k, 0, m, n, o, p, q, r, s, t, u, v, w, x, y, o1, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) [ 0 >= p1 ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> f16(a, b, c, d, e, k1 + 1, m1, n1, o1 + 1, j, k, l1, l1, n, o, p, q, r, s, t, u, v, w, x, y, z, l1, l1, l1, p1, r1, s1, t1, u1, i1, j1) [ f >= 0 /\ v1 >= 0 /\ h >= i + 1 /\ k1 >= 0 ] (?, 1) f23(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) -> f16(a, b, c, d, e, k1, m1, n1, k1 + 1, j, k, l1, l1, n, o, p, q, r, s, t, u, v, w, x, y, z, l1, l1, l1, o1, p1, r1, g1, h1, s1, t1) [ u1 >= 1 ] start location: f30 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, e, f, h, i, j, n, o]. We thus obtain the following problem: 2: T: (?, 1) f23(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, k1, n1, k1 + 1, j, n, o) [ u1 >= 1 ] (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, k1 + 1, n1, o1 + 1, j, n, o) [ f >= 0 /\ v1 >= 0 /\ h >= i + 1 /\ k1 >= 0 ] (?, 1) f23(a, b, c, e, f, h, i, j, n, o) -> f4(a, b, c, e, f, l1, m1, n1, n, o) [ 0 >= p1 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ 0 >= j + 1 /\ q1 >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ j >= 1 /\ q1 >= 0 ] (?, 1) f4(a, b, c, e, f, h, i, j, n, o) -> f21(a, b, c, e, f, h, i, 0, n, o) [ j = 0 ] (?, 1) f2(a, b, c, e, f, h, i, j, n, o) -> f22(a, b, c, e, f, h, i, j, n, o) (?, 1) f12(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, i, h, i + 1, j, n, o) (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f18(a, b, c, e, k1, h, i, 0, n, o) [ k1 >= 0 /\ f >= 0 /\ j = 0 ] (?, 1) f4(a, b, c, e, f, h, i, j, n, o) -> f17(a, b, c, e, f, h, i, j, n, o) [ 0 >= j + 1 ] (?, 1) f4(a, b, c, e, f, h, i, j, n, o) -> f17(a, b, c, e, f, h, i, j, n, o) [ j >= 1 ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f25(a, b, c, e, k1, h, i, j, n, o) [ f >= 1 /\ 0 >= n + 1 /\ k1 >= 1 ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f25(a, b, c, e, k1, h, i, j, n, o) [ f >= 1 /\ n >= 1 /\ k1 >= 1 ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f2(a, b, c, e, k1, h, i, j, o, o) [ l1 >= 1 /\ f >= 1 /\ n = 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, f + 1, h, i + 1, j, n, o) [ 0 >= e /\ f >= 0 ] (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, k1, h, i, j, n, o) [ i >= h /\ f >= 0 ] (?, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1, m1, n1, o1, n, o) (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e - 1, f, h, i, j, n, o) [ e >= 1 ] (?, 1) f4(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, c, f, h, i, j, n, o) (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f4(a, b, c, e, f, h, i, j, n, o) [ b >= a ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, b + 1, c + 1, e, f, h, i, j, n, o) [ a >= b + 1 ] (?, 1) f2(a, b, c, e, f, h, i, j, n, o) -> f3(a, 0, 0, e, f, h, i, j, n, o) (?, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f2(k1, b, c, e, f, h, i, j, n, o) (1, 1) f30(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, f, h, i, j, n, o) start location: f30 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f23(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, k1, n1, k1 + 1, j, n, o) [ u1 >= 1 ] (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, k1 + 1, n1, o1 + 1, j, n, o) [ f >= 0 /\ v1 >= 0 /\ h >= i + 1 /\ k1 >= 0 ] (?, 1) f23(a, b, c, e, f, h, i, j, n, o) -> f4(a, b, c, e, f, l1, m1, n1, n, o) [ 0 >= p1 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ 0 >= j + 1 /\ q1 >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ j >= 1 /\ q1 >= 0 ] (?, 1) f12(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, i, h, i + 1, j, n, o) (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f2(a, b, c, e, k1, h, i, j, o, o) [ l1 >= 1 /\ f >= 1 /\ n = 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, f + 1, h, i + 1, j, n, o) [ 0 >= e /\ f >= 0 ] (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, k1, h, i, j, n, o) [ i >= h /\ f >= 0 ] (?, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1, m1, n1, o1, n, o) (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e - 1, f, h, i, j, n, o) [ e >= 1 ] (?, 1) f4(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, c, f, h, i, j, n, o) (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f4(a, b, c, e, f, h, i, j, n, o) [ b >= a ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, b + 1, c + 1, e, f, h, i, j, n, o) [ a >= b + 1 ] (?, 1) f2(a, b, c, e, f, h, i, j, n, o) -> f3(a, 0, 0, e, f, h, i, j, n, o) (?, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f2(k1, b, c, e, f, h, i, j, n, o) (1, 1) f30(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, f, h, i, j, n, o) start location: f30 leaf cost: 7 Testing for reachability in the complexity graph removes the following transitions from problem 3: f23(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, k1, n1, k1 + 1, j, n, o) [ u1 >= 1 ] f23(a, b, c, e, f, h, i, j, n, o) -> f4(a, b, c, e, f, l1, m1, n1, n, o) [ 0 >= p1 ] f12(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, i, h, i + 1, j, n, o) We thus obtain the following problem: 4: T: (?, 1) f4(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, c, f, h, i, j, n, o) (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, k1, h, i, j, n, o) [ i >= h /\ f >= 0 ] (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, k1 + 1, n1, o1 + 1, j, n, o) [ f >= 0 /\ v1 >= 0 /\ h >= i + 1 /\ k1 >= 0 ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, b + 1, c + 1, e, f, h, i, j, n, o) [ a >= b + 1 ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f4(a, b, c, e, f, h, i, j, n, o) [ b >= a ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f2(a, b, c, e, k1, h, i, j, o, o) [ l1 >= 1 /\ f >= 1 /\ n = 0 ] (?, 1) f2(a, b, c, e, f, h, i, j, n, o) -> f3(a, 0, 0, e, f, h, i, j, n, o) (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e - 1, f, h, i, j, n, o) [ e >= 1 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, f + 1, h, i + 1, j, n, o) [ 0 >= e /\ f >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ j >= 1 /\ q1 >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ 0 >= j + 1 /\ q1 >= 0 ] (?, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f2(k1, b, c, e, f, h, i, j, n, o) (?, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1, m1, n1, o1, n, o) (1, 1) f30(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, f, h, i, j, n, o) start location: f30 leaf cost: 7 By chaining the transition f3(a, b, c, e, f, h, i, j, n, o) -> f4(a, b, c, e, f, h, i, j, n, o) [ b >= a ] with all transitions in problem 4, the following new transition is obtained: f3(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, c, f, h, i, j, n, o) [ b >= a ] We thus obtain the following problem: 5: T: (?, 2) f3(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, c, f, h, i, j, n, o) [ b >= a ] (?, 1) f4(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, c, f, h, i, j, n, o) (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, k1, h, i, j, n, o) [ i >= h /\ f >= 0 ] (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, k1 + 1, n1, o1 + 1, j, n, o) [ f >= 0 /\ v1 >= 0 /\ h >= i + 1 /\ k1 >= 0 ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, b + 1, c + 1, e, f, h, i, j, n, o) [ a >= b + 1 ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f2(a, b, c, e, k1, h, i, j, o, o) [ l1 >= 1 /\ f >= 1 /\ n = 0 ] (?, 1) f2(a, b, c, e, f, h, i, j, n, o) -> f3(a, 0, 0, e, f, h, i, j, n, o) (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e - 1, f, h, i, j, n, o) [ e >= 1 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, f + 1, h, i + 1, j, n, o) [ 0 >= e /\ f >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ j >= 1 /\ q1 >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ 0 >= j + 1 /\ q1 >= 0 ] (?, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f2(k1, b, c, e, f, h, i, j, n, o) (?, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1, m1, n1, o1, n, o) (1, 1) f30(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, f, h, i, j, n, o) start location: f30 leaf cost: 7 Testing for reachability in the complexity graph removes the following transition from problem 5: f4(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, c, f, h, i, j, n, o) We thus obtain the following problem: 6: T: (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, k1, h, i, j, n, o) [ i >= h /\ f >= 0 ] (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, k1 + 1, n1, o1 + 1, j, n, o) [ f >= 0 /\ v1 >= 0 /\ h >= i + 1 /\ k1 >= 0 ] (?, 2) f3(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, c, f, h, i, j, n, o) [ b >= a ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, b + 1, c + 1, e, f, h, i, j, n, o) [ a >= b + 1 ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f2(a, b, c, e, k1, h, i, j, o, o) [ l1 >= 1 /\ f >= 1 /\ n = 0 ] (?, 1) f2(a, b, c, e, f, h, i, j, n, o) -> f3(a, 0, 0, e, f, h, i, j, n, o) (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e - 1, f, h, i, j, n, o) [ e >= 1 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, f + 1, h, i + 1, j, n, o) [ 0 >= e /\ f >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ j >= 1 /\ q1 >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ 0 >= j + 1 /\ q1 >= 0 ] (?, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f2(k1, b, c, e, f, h, i, j, n, o) (?, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1, m1, n1, o1, n, o) (1, 1) f30(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, f, h, i, j, n, o) start location: f30 leaf cost: 7 By chaining the transition f3(a, b, c, e, f, h, i, j, n, o) -> f2(a, b, c, e, k1, h, i, j, o, o) [ l1 >= 1 /\ f >= 1 /\ n = 0 ] with all transitions in problem 6, the following new transition is obtained: f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, 0, 0, e, k1, h, i, j, o, o) [ l1 >= 1 /\ f >= 1 /\ n = 0 ] We thus obtain the following problem: 7: T: (?, 2) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, 0, 0, e, k1, h, i, j, o, o) [ l1 >= 1 /\ f >= 1 /\ n = 0 ] (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, k1, h, i, j, n, o) [ i >= h /\ f >= 0 ] (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, k1 + 1, n1, o1 + 1, j, n, o) [ f >= 0 /\ v1 >= 0 /\ h >= i + 1 /\ k1 >= 0 ] (?, 2) f3(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, c, f, h, i, j, n, o) [ b >= a ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, b + 1, c + 1, e, f, h, i, j, n, o) [ a >= b + 1 ] (?, 1) f2(a, b, c, e, f, h, i, j, n, o) -> f3(a, 0, 0, e, f, h, i, j, n, o) (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e - 1, f, h, i, j, n, o) [ e >= 1 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, f + 1, h, i + 1, j, n, o) [ 0 >= e /\ f >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ j >= 1 /\ q1 >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ 0 >= j + 1 /\ q1 >= 0 ] (?, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f2(k1, b, c, e, f, h, i, j, n, o) (?, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1, m1, n1, o1, n, o) (1, 1) f30(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, f, h, i, j, n, o) start location: f30 leaf cost: 7 By chaining the transition f1(a, b, c, e, f, h, i, j, n, o) -> f2(k1, b, c, e, f, h, i, j, n, o) with all transitions in problem 7, the following new transition is obtained: f1(a, b, c, e, f, h, i, j, n, o) -> f3(k1, 0, 0, e, f, h, i, j, n, o) We thus obtain the following problem: 8: T: (?, 2) f1(a, b, c, e, f, h, i, j, n, o) -> f3(k1, 0, 0, e, f, h, i, j, n, o) (?, 2) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, 0, 0, e, k1, h, i, j, o, o) [ l1 >= 1 /\ f >= 1 /\ n = 0 ] (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, k1, h, i, j, n, o) [ i >= h /\ f >= 0 ] (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, k1 + 1, n1, o1 + 1, j, n, o) [ f >= 0 /\ v1 >= 0 /\ h >= i + 1 /\ k1 >= 0 ] (?, 2) f3(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, c, f, h, i, j, n, o) [ b >= a ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, b + 1, c + 1, e, f, h, i, j, n, o) [ a >= b + 1 ] (?, 1) f2(a, b, c, e, f, h, i, j, n, o) -> f3(a, 0, 0, e, f, h, i, j, n, o) (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e - 1, f, h, i, j, n, o) [ e >= 1 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, f + 1, h, i + 1, j, n, o) [ 0 >= e /\ f >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ j >= 1 /\ q1 >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ 0 >= j + 1 /\ q1 >= 0 ] (?, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1, m1, n1, o1, n, o) (1, 1) f30(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, f, h, i, j, n, o) start location: f30 leaf cost: 7 Testing for reachability in the complexity graph removes the following transition from problem 8: f2(a, b, c, e, f, h, i, j, n, o) -> f3(a, 0, 0, e, f, h, i, j, n, o) We thus obtain the following problem: 9: T: (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, k1, h, i, j, n, o) [ i >= h /\ f >= 0 ] (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, k1 + 1, n1, o1 + 1, j, n, o) [ f >= 0 /\ v1 >= 0 /\ h >= i + 1 /\ k1 >= 0 ] (?, 2) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, 0, 0, e, k1, h, i, j, o, o) [ l1 >= 1 /\ f >= 1 /\ n = 0 ] (?, 2) f3(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, c, f, h, i, j, n, o) [ b >= a ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, b + 1, c + 1, e, f, h, i, j, n, o) [ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e - 1, f, h, i, j, n, o) [ e >= 1 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, f + 1, h, i + 1, j, n, o) [ 0 >= e /\ f >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ j >= 1 /\ q1 >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ 0 >= j + 1 /\ q1 >= 0 ] (?, 2) f1(a, b, c, e, f, h, i, j, n, o) -> f3(k1, 0, 0, e, f, h, i, j, n, o) (?, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1, m1, n1, o1, n, o) (1, 1) f30(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, f, h, i, j, n, o) start location: f30 leaf cost: 7 By chaining the transition f16(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, k1, h, i, j, n, o) [ i >= h /\ f >= 0 ] with all transitions in problem 9, the following new transitions are obtained: f16(a, b, c, e, f, h, i, j, n, o) -> f3(k1', 0, 0, e, k1, h, i, j, n, o) [ i >= h /\ f >= 0 ] f16(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1', m1, n1, o1, n, o) [ i >= h /\ f >= 0 ] We thus obtain the following problem: 10: T: (?, 3) f16(a, b, c, e, f, h, i, j, n, o) -> f3(k1', 0, 0, e, k1, h, i, j, n, o) [ i >= h /\ f >= 0 ] (?, 2) f16(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1', m1, n1, o1, n, o) [ i >= h /\ f >= 0 ] (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, k1 + 1, n1, o1 + 1, j, n, o) [ f >= 0 /\ v1 >= 0 /\ h >= i + 1 /\ k1 >= 0 ] (?, 2) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, 0, 0, e, k1, h, i, j, o, o) [ l1 >= 1 /\ f >= 1 /\ n = 0 ] (?, 2) f3(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, c, f, h, i, j, n, o) [ b >= a ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, b + 1, c + 1, e, f, h, i, j, n, o) [ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e - 1, f, h, i, j, n, o) [ e >= 1 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, f + 1, h, i + 1, j, n, o) [ 0 >= e /\ f >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ j >= 1 /\ q1 >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ 0 >= j + 1 /\ q1 >= 0 ] (?, 2) f1(a, b, c, e, f, h, i, j, n, o) -> f3(k1, 0, 0, e, f, h, i, j, n, o) (?, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1, m1, n1, o1, n, o) (1, 1) f30(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, f, h, i, j, n, o) start location: f30 leaf cost: 7 Repeatedly propagating knowledge in problem 10 produces the following problem: 11: T: (?, 3) f16(a, b, c, e, f, h, i, j, n, o) -> f3(k1', 0, 0, e, k1, h, i, j, n, o) [ i >= h /\ f >= 0 ] (?, 2) f16(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1', m1, n1, o1, n, o) [ i >= h /\ f >= 0 ] (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, k1 + 1, n1, o1 + 1, j, n, o) [ f >= 0 /\ v1 >= 0 /\ h >= i + 1 /\ k1 >= 0 ] (?, 2) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, 0, 0, e, k1, h, i, j, o, o) [ l1 >= 1 /\ f >= 1 /\ n = 0 ] (?, 2) f3(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, c, f, h, i, j, n, o) [ b >= a ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, b + 1, c + 1, e, f, h, i, j, n, o) [ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e - 1, f, h, i, j, n, o) [ e >= 1 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, f + 1, h, i + 1, j, n, o) [ 0 >= e /\ f >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ j >= 1 /\ q1 >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ 0 >= j + 1 /\ q1 >= 0 ] (1, 2) f1(a, b, c, e, f, h, i, j, n, o) -> f3(k1, 0, 0, e, f, h, i, j, n, o) (1, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1, m1, n1, o1, n, o) (1, 1) f30(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, f, h, i, j, n, o) start location: f30 leaf cost: 7 By chaining the transition f30(a, b, c, e, f, h, i, j, n, o) -> f1(a, b, c, e, f, h, i, j, n, o) with all transitions in problem 11, the following new transitions are obtained: f30(a, b, c, e, f, h, i, j, n, o) -> f3(k1, 0, 0, e, f, h, i, j, n, o) f30(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1, m1, n1, o1, n, o) We thus obtain the following problem: 12: T: (1, 3) f30(a, b, c, e, f, h, i, j, n, o) -> f3(k1, 0, 0, e, f, h, i, j, n, o) (1, 2) f30(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1, m1, n1, o1, n, o) (?, 3) f16(a, b, c, e, f, h, i, j, n, o) -> f3(k1', 0, 0, e, k1, h, i, j, n, o) [ i >= h /\ f >= 0 ] (?, 2) f16(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1', m1, n1, o1, n, o) [ i >= h /\ f >= 0 ] (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, k1 + 1, n1, o1 + 1, j, n, o) [ f >= 0 /\ v1 >= 0 /\ h >= i + 1 /\ k1 >= 0 ] (?, 2) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, 0, 0, e, k1, h, i, j, o, o) [ l1 >= 1 /\ f >= 1 /\ n = 0 ] (?, 2) f3(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, c, f, h, i, j, n, o) [ b >= a ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, b + 1, c + 1, e, f, h, i, j, n, o) [ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e - 1, f, h, i, j, n, o) [ e >= 1 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, f + 1, h, i + 1, j, n, o) [ 0 >= e /\ f >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ j >= 1 /\ q1 >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ 0 >= j + 1 /\ q1 >= 0 ] (1, 2) f1(a, b, c, e, f, h, i, j, n, o) -> f3(k1, 0, 0, e, f, h, i, j, n, o) (1, 1) f1(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1, m1, n1, o1, n, o) start location: f30 leaf cost: 7 Testing for reachability in the complexity graph removes the following transitions from problem 12: f1(a, b, c, e, f, h, i, j, n, o) -> f3(k1, 0, 0, e, f, h, i, j, n, o) f1(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1, m1, n1, o1, n, o) We thus obtain the following problem: 13: T: (?, 2) f16(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1', m1, n1, o1, n, o) [ i >= h /\ f >= 0 ] (?, 3) f16(a, b, c, e, f, h, i, j, n, o) -> f3(k1', 0, 0, e, k1, h, i, j, n, o) [ i >= h /\ f >= 0 ] (?, 1) f16(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, k1 + 1, n1, o1 + 1, j, n, o) [ f >= 0 /\ v1 >= 0 /\ h >= i + 1 /\ k1 >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e - 1, f, h, i, j, n, o) [ e >= 1 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f16(a, b, c, e, f + 1, h, i + 1, j, n, o) [ 0 >= e /\ f >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ j >= 1 /\ q1 >= 0 ] (?, 1) f5(a, b, c, e, f, h, i, j, n, o) -> f3(a, b, c, e, k1, o1, p1, u1, r1, t1) [ f >= 0 /\ 0 >= j + 1 /\ q1 >= 0 ] (?, 2) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, 0, 0, e, k1, h, i, j, o, o) [ l1 >= 1 /\ f >= 1 /\ n = 0 ] (?, 2) f3(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, c, f, h, i, j, n, o) [ b >= a ] (?, 1) f3(a, b, c, e, f, h, i, j, n, o) -> f3(a, b + 1, c + 1, e, f, h, i, j, n, o) [ a >= b + 1 ] (1, 2) f30(a, b, c, e, f, h, i, j, n, o) -> f5(a, b, c, e, k1, m1, n1, o1, n, o) (1, 3) f30(a, b, c, e, f, h, i, j, n, o) -> f3(k1, 0, 0, e, f, h, i, j, n, o) start location: f30 leaf cost: 7 Complexity upper bound ? Time: 19.533 sec (SMT: 12.007 sec)