MAYBE Initial complexity problem: 1: T: (?, 1) f8(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f32(a, b, n, d, e, f, g, h, i, j, k, l, m) [ a >= b ] (1, 1) f15(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f8(a, b, c, n, e, f, g, h, i, j, k, l, m) (?, 1) f300(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f8(a + 1, b, c, d, e, f, g, h, i, j, k, l, m) [ b >= e ] (?, 1) f8(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f8(a + 1, b, c, d, e, f, g, h, i, j, k, l, m) [ b >= a + 1 /\ b >= e ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f1(a, b, n, d, e, o, p, 0, 2, 0, 0, l, m) (?, 1) f12(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f1(a, b, n, d, e, o, p, 0, i, 0, 0, i + 1, m) [ 4 >= i ] (?, 1) f10(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f1(a, b, n, d, e, o, p, 0, i, 0, 0, l, 2) (?, 1) f8(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f1(a, b, n, d, e, o, p, 0, i, 0, 0, l, m) [ b >= a + 1 /\ e >= b + 1 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f1(a, b, n, d, e, o, p, 0, i, 0, 0, l, m) [ e >= b + 1 /\ 4 >= m ] (?, 1) f300(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f1(a, b, n, d, e, o, p, 0, i, 0, 0, l, m) [ e >= b + 1 ] (?, 1) f12(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f300(a, b + 1, n, d, e, o, g, 1, i, 1, 1, l, m) [ i >= 5 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f300(a, b + 1, n, d, e, o, g, 1, i, 1, 1, l, m) [ e >= b + 1 /\ m >= 5 ] start location: f15 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, e, i, m]. We thus obtain the following problem: 2: T: (?, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\ m >= 5 ] (?, 1) f12(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ i >= 5 ] (?, 1) f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\ 4 >= m ] (?, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (?, 1) f10(a, b, e, i, m) -> f1(a, b, e, i, 2) (?, 1) f12(a, b, e, i, m) -> f1(a, b, e, i, m) [ 4 >= i ] (?, 1) f13(a, b, e, i, m) -> f1(a, b, e, 2, m) (?, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (?, 1) f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (?, 1) f8(a, b, e, i, m) -> f32(a, b, e, i, m) [ a >= b ] start location: f15 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\ m >= 5 ] (?, 1) f12(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ i >= 5 ] (?, 1) f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\ 4 >= m ] (?, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (?, 1) f10(a, b, e, i, m) -> f1(a, b, e, i, 2) (?, 1) f12(a, b, e, i, m) -> f1(a, b, e, i, m) [ 4 >= i ] (?, 1) f13(a, b, e, i, m) -> f1(a, b, e, 2, m) (?, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (?, 1) f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) start location: f15 leaf cost: 1 Testing for reachability in the complexity graph removes the following transitions from problem 3: f12(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ i >= 5 ] f10(a, b, e, i, m) -> f1(a, b, e, i, 2) f12(a, b, e, i, m) -> f1(a, b, e, i, m) [ 4 >= i ] f13(a, b, e, i, m) -> f1(a, b, e, 2, m) We thus obtain the following problem: 4: T: (?, 1) f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ] (?, 1) f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\ 4 >= m ] (?, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\ m >= 5 ] (?, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (?, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) start location: f15 leaf cost: 1 Repeatedly propagating knowledge in problem 4 produces the following problem: 5: T: (?, 1) f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ] (?, 1) f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\ 4 >= m ] (?, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\ m >= 5 ] (?, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) start location: f15 leaf cost: 1 A polynomial rank function with Pol(f8) = 0 Pol(f300) = 1 Pol(f1) = 1 and size complexities S("f15(a, b, e, i, m) -> f8(a, b, e, i, m)", 0-0) = a S("f15(a, b, e, i, m) -> f8(a, b, e, i, m)", 0-1) = b S("f15(a, b, e, i, m) -> f8(a, b, e, i, m)", 0-2) = e S("f15(a, b, e, i, m) -> f8(a, b, e, i, m)", 0-3) = i S("f15(a, b, e, i, m) -> f8(a, b, e, i, m)", 0-4) = m S("f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\\ e >= b + 1 ]", 0-0) = a S("f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\\ e >= b + 1 ]", 0-1) = b S("f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\\ e >= b + 1 ]", 0-2) = e S("f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\\ e >= b + 1 ]", 0-3) = i S("f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\\ e >= b + 1 ]", 0-4) = m S("f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\\ b >= e ]", 0-0) = ? S("f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\\ b >= e ]", 0-1) = ? S("f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\\ b >= e ]", 0-2) = e S("f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\\ b >= e ]", 0-3) = i S("f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\\ b >= e ]", 0-4) = m S("f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\\ m >= 5 ]", 0-0) = a S("f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\\ m >= 5 ]", 0-1) = ? S("f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\\ m >= 5 ]", 0-2) = e S("f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\\ m >= 5 ]", 0-3) = i S("f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\\ m >= 5 ]", 0-4) = m S("f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\\ 4 >= m ]", 0-0) = a S("f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\\ 4 >= m ]", 0-1) = ? S("f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\\ 4 >= m ]", 0-2) = e S("f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\\ 4 >= m ]", 0-3) = i S("f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\\ 4 >= m ]", 0-4) = m S("f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ]", 0-0) = a S("f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ]", 0-1) = ? S("f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ]", 0-2) = e S("f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ]", 0-3) = i S("f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ]", 0-4) = m S("f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ]", 0-0) = a + 1 S("f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ]", 0-1) = ? S("f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ]", 0-2) = e S("f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ]", 0-3) = i S("f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ]", 0-4) = m orients the transitions f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ] f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ] f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\ m >= 5 ] f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\ 4 >= m ] weakly and the transition f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ] strictly and produces the following problem: 6: T: (1, 1) f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ] (?, 1) f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\ 4 >= m ] (?, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\ m >= 5 ] (?, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) start location: f15 leaf cost: 1 A polynomial rank function with Pol(f300) = -2*V_2 + 2*V_3 + 3 Pol(f8) = -3*V_2 + 3*V_3 + 1 Pol(f1) = -2*V_2 + 2*V_3 + 2 Pol(f15) = -3*V_2 + 3*V_3 + 1 orients all transitions weakly and the transitions f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ] f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\ m >= 5 ] strictly and produces the following problem: 7: T: (1, 1) f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ] (3*b + 3*e + 1, 1) f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\ 4 >= m ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\ m >= 5 ] (?, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) start location: f15 leaf cost: 1 A polynomial rank function with Pol(f8) = -V_1 + V_2 Pol(f1) = V_1 + 2*V_2 + V_4 + 2*V_5 - 3 and size complexities S("f15(a, b, e, i, m) -> f8(a, b, e, i, m)", 0-0) = a S("f15(a, b, e, i, m) -> f8(a, b, e, i, m)", 0-1) = b S("f15(a, b, e, i, m) -> f8(a, b, e, i, m)", 0-2) = e S("f15(a, b, e, i, m) -> f8(a, b, e, i, m)", 0-3) = i S("f15(a, b, e, i, m) -> f8(a, b, e, i, m)", 0-4) = m S("f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\\ e >= b + 1 ]", 0-0) = a S("f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\\ e >= b + 1 ]", 0-1) = b S("f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\\ e >= b + 1 ]", 0-2) = e S("f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\\ e >= b + 1 ]", 0-3) = i S("f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\\ e >= b + 1 ]", 0-4) = m S("f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\\ b >= e ]", 0-0) = ? S("f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\\ b >= e ]", 0-1) = 4*b + 4*e + 256 S("f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\\ b >= e ]", 0-2) = e S("f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\\ b >= e ]", 0-3) = i S("f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\\ b >= e ]", 0-4) = m S("f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\\ m >= 5 ]", 0-0) = a S("f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\\ m >= 5 ]", 0-1) = 4*b + 4*e + 16 S("f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\\ m >= 5 ]", 0-2) = e S("f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\\ m >= 5 ]", 0-3) = i S("f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\\ m >= 5 ]", 0-4) = m S("f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\\ 4 >= m ]", 0-0) = a S("f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\\ 4 >= m ]", 0-1) = 4*b + 4*e + 64 S("f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\\ 4 >= m ]", 0-2) = e S("f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\\ 4 >= m ]", 0-3) = i S("f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\\ 4 >= m ]", 0-4) = m S("f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ]", 0-0) = a S("f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ]", 0-1) = 4*b + 4*e + 16 S("f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ]", 0-2) = e S("f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ]", 0-3) = i S("f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ]", 0-4) = m S("f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ]", 0-0) = a + 1 S("f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ]", 0-1) = 4*b + 4*e + 64 S("f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ]", 0-2) = e S("f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ]", 0-3) = i S("f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ]", 0-4) = m orients the transitions f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\ 4 >= m ] weakly and the transition f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] strictly and produces the following problem: 8: T: (1, 1) f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= e ] (3*b + 3*e + 1, 1) f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ e >= b + 1 /\ 4 >= m ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ e >= b + 1 /\ m >= 5 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) start location: f15 leaf cost: 1 Applied AI with 'oct' on problem 8 to obtain the following invariants: For symbol f1: -X_2 + X_3 - 1 >= 0 /\ -X_1 + X_3 - 2 >= 0 /\ -X_1 + X_2 - 1 >= 0 For symbol f300: X_5 - 5 >= 0 /\ -X_2 + X_3 >= 0 /\ -X_1 + X_3 - 2 >= 0 /\ -X_1 + X_2 - 2 >= 0 This yielded the following problem: 9: T: (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ m >= 5 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ 4 >= m ] (3*b + 3*e + 1, 1) f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 ] (1, 1) f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e ] start location: f15 leaf cost: 1 By chaining the transition f300(a, b, e, i, m) -> f1(a, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 ] with all transitions in problem 9, the following new transition is obtained: f300(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 /\ -b + e - 1 >= 0 /\ -a + b - 1 >= 0 /\ m >= 5 ] We thus obtain the following problem: 10: T: (3*b + 3*e + 1, 2) f300(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 /\ -b + e - 1 >= 0 /\ -a + b - 1 >= 0 /\ m >= 5 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ m >= 5 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ 4 >= m ] (1, 1) f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e ] start location: f15 leaf cost: 1 By chaining the transition f300(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e ] with all transitions in problem 10, the following new transition is obtained: f300(a, b, e, i, m) -> f8(a + 2, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 ] We thus obtain the following problem: 11: T: (1, 2) f300(a, b, e, i, m) -> f8(a + 2, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 ] (3*b + 3*e + 1, 2) f300(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 /\ -b + e - 1 >= 0 /\ -a + b - 1 >= 0 /\ m >= 5 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ m >= 5 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ 4 >= m ] start location: f15 leaf cost: 1 By chaining the transition f300(a, b, e, i, m) -> f8(a + 2, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 ] with all transitions in problem 11, the following new transition is obtained: f300(a, b, e, i, m) -> f8(a + 3, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 ] We thus obtain the following problem: 12: T: (1, 3) f300(a, b, e, i, m) -> f8(a + 3, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 ] (3*b + 3*e + 1, 2) f300(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 /\ -b + e - 1 >= 0 /\ -a + b - 1 >= 0 /\ m >= 5 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ m >= 5 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ 4 >= m ] start location: f15 leaf cost: 1 By chaining the transition f300(a, b, e, i, m) -> f8(a + 3, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 ] with all transitions in problem 12, the following new transition is obtained: f300(a, b, e, i, m) -> f8(a + 4, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 ] We thus obtain the following problem: 13: T: (1, 4) f300(a, b, e, i, m) -> f8(a + 4, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 ] (3*b + 3*e + 1, 2) f300(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 /\ -b + e - 1 >= 0 /\ -a + b - 1 >= 0 /\ m >= 5 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ m >= 5 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ 4 >= m ] start location: f15 leaf cost: 1 By chaining the transition f300(a, b, e, i, m) -> f8(a + 4, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 ] with all transitions in problem 13, the following new transition is obtained: f300(a, b, e, i, m) -> f8(a + 5, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 ] We thus obtain the following problem: 14: T: (1, 5) f300(a, b, e, i, m) -> f8(a + 5, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 ] (3*b + 3*e + 1, 2) f300(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 /\ -b + e - 1 >= 0 /\ -a + b - 1 >= 0 /\ m >= 5 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ m >= 5 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ 4 >= m ] start location: f15 leaf cost: 1 By chaining the transition f300(a, b, e, i, m) -> f8(a + 5, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 ] with all transitions in problem 14, the following new transition is obtained: f300(a, b, e, i, m) -> f8(a + 6, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 ] We thus obtain the following problem: 15: T: (1, 6) f300(a, b, e, i, m) -> f8(a + 6, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 ] (3*b + 3*e + 1, 2) f300(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 /\ -b + e - 1 >= 0 /\ -a + b - 1 >= 0 /\ m >= 5 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ m >= 5 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ 4 >= m ] start location: f15 leaf cost: 1 By chaining the transition f300(a, b, e, i, m) -> f8(a + 6, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 ] with all transitions in problem 15, the following new transition is obtained: f300(a, b, e, i, m) -> f8(a + 7, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 ] We thus obtain the following problem: 16: T: (1, 7) f300(a, b, e, i, m) -> f8(a + 7, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 ] (3*b + 3*e + 1, 2) f300(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 /\ -b + e - 1 >= 0 /\ -a + b - 1 >= 0 /\ m >= 5 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ m >= 5 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ 4 >= m ] start location: f15 leaf cost: 1 By chaining the transition f300(a, b, e, i, m) -> f8(a + 7, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 ] with all transitions in problem 16, the following new transition is obtained: f300(a, b, e, i, m) -> f8(a + 8, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 ] We thus obtain the following problem: 17: T: (1, 8) f300(a, b, e, i, m) -> f8(a + 8, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 ] (3*b + 3*e + 1, 2) f300(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 /\ -b + e - 1 >= 0 /\ -a + b - 1 >= 0 /\ m >= 5 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ m >= 5 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ 4 >= m ] start location: f15 leaf cost: 1 By chaining the transition f300(a, b, e, i, m) -> f8(a + 8, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 ] with all transitions in problem 17, the following new transition is obtained: f300(a, b, e, i, m) -> f8(a + 9, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 ] We thus obtain the following problem: 18: T: (1, 9) f300(a, b, e, i, m) -> f8(a + 9, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 ] (3*b + 3*e + 1, 2) f300(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 /\ -b + e - 1 >= 0 /\ -a + b - 1 >= 0 /\ m >= 5 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ m >= 5 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ 4 >= m ] start location: f15 leaf cost: 1 By chaining the transition f300(a, b, e, i, m) -> f8(a + 9, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 ] with all transitions in problem 18, the following new transition is obtained: f300(a, b, e, i, m) -> f8(a + 10, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 ] We thus obtain the following problem: 19: T: (1, 10) f300(a, b, e, i, m) -> f8(a + 10, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 ] (3*b + 3*e + 1, 2) f300(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 /\ -b + e - 1 >= 0 /\ -a + b - 1 >= 0 /\ m >= 5 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ m >= 5 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ 4 >= m ] start location: f15 leaf cost: 1 By chaining the transition f300(a, b, e, i, m) -> f8(a + 10, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 ] with all transitions in problem 19, the following new transition is obtained: f300(a, b, e, i, m) -> f8(a + 11, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 /\ b >= a + 11 ] We thus obtain the following problem: 20: T: (1, 11) f300(a, b, e, i, m) -> f8(a + 11, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 /\ b >= a + 11 ] (3*b + 3*e + 1, 2) f300(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 /\ -b + e - 1 >= 0 /\ -a + b - 1 >= 0 /\ m >= 5 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ m >= 5 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ 4 >= m ] start location: f15 leaf cost: 1 By chaining the transition f300(a, b, e, i, m) -> f8(a + 11, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 /\ b >= a + 11 ] with all transitions in problem 20, the following new transition is obtained: f300(a, b, e, i, m) -> f8(a + 12, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 /\ b >= a + 11 /\ b >= a + 12 ] We thus obtain the following problem: 21: T: (1, 12) f300(a, b, e, i, m) -> f8(a + 12, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 /\ b >= a + 11 /\ b >= a + 12 ] (3*b + 3*e + 1, 2) f300(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 /\ -b + e - 1 >= 0 /\ -a + b - 1 >= 0 /\ m >= 5 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ m >= 5 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ 4 >= m ] start location: f15 leaf cost: 1 By chaining the transition f300(a, b, e, i, m) -> f8(a + 12, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 /\ b >= a + 11 /\ b >= a + 12 ] with all transitions in problem 21, the following new transition is obtained: f300(a, b, e, i, m) -> f8(a + 13, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 /\ b >= a + 11 /\ b >= a + 12 /\ b >= a + 13 ] We thus obtain the following problem: 22: T: (1, 13) f300(a, b, e, i, m) -> f8(a + 13, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 /\ b >= a + 11 /\ b >= a + 12 /\ b >= a + 13 ] (3*b + 3*e + 1, 2) f300(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 /\ -b + e - 1 >= 0 /\ -a + b - 1 >= 0 /\ m >= 5 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ m >= 5 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ 4 >= m ] start location: f15 leaf cost: 1 By chaining the transition f300(a, b, e, i, m) -> f8(a + 13, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 /\ b >= a + 11 /\ b >= a + 12 /\ b >= a + 13 ] with all transitions in problem 22, the following new transition is obtained: f300(a, b, e, i, m) -> f8(a + 14, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 /\ b >= a + 11 /\ b >= a + 12 /\ b >= a + 13 /\ b >= a + 14 ] We thus obtain the following problem: 23: T: (1, 14) f300(a, b, e, i, m) -> f8(a + 14, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 /\ b >= a + 11 /\ b >= a + 12 /\ b >= a + 13 /\ b >= a + 14 ] (3*b + 3*e + 1, 2) f300(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 /\ -b + e - 1 >= 0 /\ -a + b - 1 >= 0 /\ m >= 5 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ m >= 5 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ 4 >= m ] start location: f15 leaf cost: 1 By chaining the transition f300(a, b, e, i, m) -> f8(a + 14, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 /\ b >= a + 11 /\ b >= a + 12 /\ b >= a + 13 /\ b >= a + 14 ] with all transitions in problem 23, the following new transition is obtained: f300(a, b, e, i, m) -> f8(a + 15, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 /\ b >= a + 11 /\ b >= a + 12 /\ b >= a + 13 /\ b >= a + 14 /\ b >= a + 15 ] We thus obtain the following problem: 24: T: (1, 15) f300(a, b, e, i, m) -> f8(a + 15, b, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ b >= e /\ b >= a + 2 /\ b >= a + 3 /\ b >= a + 4 /\ b >= a + 5 /\ b >= a + 6 /\ b >= a + 7 /\ b >= a + 8 /\ b >= a + 9 /\ b >= a + 10 /\ b >= a + 11 /\ b >= a + 12 /\ b >= a + 13 /\ b >= a + 14 /\ b >= a + 15 ] (3*b + 3*e + 1, 2) f300(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ m - 5 >= 0 /\ -b + e >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 2 >= 0 /\ e >= b + 1 /\ -b + e - 1 >= 0 /\ -a + b - 1 >= 0 /\ m >= 5 ] (1, 1) f15(a, b, e, i, m) -> f8(a, b, e, i, m) (1, 1) f8(a, b, e, i, m) -> f1(a, b, e, i, m) [ b >= a + 1 /\ e >= b + 1 ] (4*a + 120*b + 117*e + 2*i + 4*m + 3*a*b + 3*a*e + 24*b^2 + 48*b*e + 24*e^2 + 3*b*i + 3*e*i + 6*b*m + 6*e*m + 103, 1) f8(a, b, e, i, m) -> f8(a + 1, b, e, i, m) [ b >= a + 1 /\ b >= e ] (3*b + 3*e + 1, 1) f1(a, b, e, i, m) -> f300(a, b + 1, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ m >= 5 ] (?, 1) f1(a, b, e, i, m) -> f1(a, b, e, i, m) [ -b + e - 1 >= 0 /\ -a + e - 2 >= 0 /\ -a + b - 1 >= 0 /\ e >= b + 1 /\ 4 >= m ] start location: f15 leaf cost: 1 Complexity upper bound ? Time: 2.584 sec (SMT: 2.385 sec)