MAYBE Initial complexity problem: 1: T: (1, 1) f0(a, b, c) -> f15(2, b, c) (?, 1) f15(a, b, c) -> f18(a, a, c) [ 10 >= a ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] (?, 1) f18(a, b, c) -> f15(a + 1, b, c) (?, 1) f15(a, b, c) -> f28(a, b, c) [ a >= 11 ] start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (1, 1) f0(a, b, c) -> f15(2, b, c) (?, 1) f15(a, b, c) -> f18(a, a, c) [ 10 >= a ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] (?, 1) f18(a, b, c) -> f15(a + 1, b, c) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f0) = 17 Pol(f15) = -2*V_1 + 21 Pol(f18) = -2*V_1 + 20 orients all transitions weakly and the transition f15(a, b, c) -> f18(a, a, c) [ 10 >= a ] strictly and produces the following problem: 3: T: (1, 1) f0(a, b, c) -> f15(2, b, c) (17, 1) f15(a, b, c) -> f18(a, a, c) [ 10 >= a ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] (?, 1) f18(a, b, c) -> f15(a + 1, b, c) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f18) = 1 Pol(f15) = 0 and size complexities S("f18(a, b, c) -> f15(a + 1, b, c)", 0-0) = ? S("f18(a, b, c) -> f15(a + 1, b, c)", 0-1) = ? S("f18(a, b, c) -> f15(a + 1, b, c)", 0-2) = ? S("f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ]", 0-0) = ? S("f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ]", 0-1) = ? S("f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ]", 0-2) = ? S("f15(a, b, c) -> f18(a, a, c) [ 10 >= a ]", 0-0) = ? S("f15(a, b, c) -> f18(a, a, c) [ 10 >= a ]", 0-1) = ? S("f15(a, b, c) -> f18(a, a, c) [ 10 >= a ]", 0-2) = ? S("f0(a, b, c) -> f15(2, b, c)", 0-0) = 2 S("f0(a, b, c) -> f15(2, b, c)", 0-1) = b S("f0(a, b, c) -> f15(2, b, c)", 0-2) = c orients the transitions f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] f18(a, b, c) -> f15(a + 1, b, c) weakly and the transition f18(a, b, c) -> f15(a + 1, b, c) strictly and produces the following problem: 4: T: (1, 1) f0(a, b, c) -> f15(2, b, c) (17, 1) f15(a, b, c) -> f18(a, a, c) [ 10 >= a ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] (17, 1) f18(a, b, c) -> f15(a + 1, b, c) start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c) -> f15(2, b, c) with all transitions in problem 4, the following new transition is obtained: f0(a, b, c) -> f18(2, 2, c) [ 10 >= 2 ] We thus obtain the following problem: 5: T: (1, 2) f0(a, b, c) -> f18(2, 2, c) [ 10 >= 2 ] (17, 1) f15(a, b, c) -> f18(a, a, c) [ 10 >= a ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] (17, 1) f18(a, b, c) -> f15(a + 1, b, c) start location: f0 leaf cost: 1 By chaining the transition f18(a, b, c) -> f15(a + 1, b, c) with all transitions in problem 5, the following new transition is obtained: f18(a, b, c) -> f18(a + 1, a + 1, c) [ 10 >= a + 1 ] We thus obtain the following problem: 6: T: (17, 2) f18(a, b, c) -> f18(a + 1, a + 1, c) [ 10 >= a + 1 ] (1, 2) f0(a, b, c) -> f18(2, 2, c) [ 10 >= 2 ] (17, 1) f15(a, b, c) -> f18(a, a, c) [ 10 >= a ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] start location: f0 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 6: f15(a, b, c) -> f18(a, a, c) [ 10 >= a ] We thus obtain the following problem: 7: T: (17, 2) f18(a, b, c) -> f18(a + 1, a + 1, c) [ 10 >= a + 1 ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] (1, 2) f0(a, b, c) -> f18(2, 2, c) [ 10 >= 2 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c) -> f18(2, 2, c) [ 10 >= 2 ] with all transitions in problem 7, the following new transitions are obtained: f0(a, b, c) -> f18(3, 3, c) [ 10 >= 2 /\ 10 >= 3 ] f0(a, b, c) -> f18(2, 1, f) [ 10 >= 2 /\ d >= e + 1 ] We thus obtain the following problem: 8: T: (1, 4) f0(a, b, c) -> f18(3, 3, c) [ 10 >= 2 /\ 10 >= 3 ] (1, 3) f0(a, b, c) -> f18(2, 1, f) [ 10 >= 2 /\ d >= e + 1 ] (17, 2) f18(a, b, c) -> f18(a + 1, a + 1, c) [ 10 >= a + 1 ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c) -> f18(3, 3, c) [ 10 >= 2 /\ 10 >= 3 ] with all transitions in problem 8, the following new transitions are obtained: f0(a, b, c) -> f18(4, 4, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 ] f0(a, b, c) -> f18(3, 2, f) [ 10 >= 2 /\ 10 >= 3 /\ d >= e + 1 ] We thus obtain the following problem: 9: T: (1, 6) f0(a, b, c) -> f18(4, 4, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 ] (1, 5) f0(a, b, c) -> f18(3, 2, f) [ 10 >= 2 /\ 10 >= 3 /\ d >= e + 1 ] (1, 3) f0(a, b, c) -> f18(2, 1, f) [ 10 >= 2 /\ d >= e + 1 ] (17, 2) f18(a, b, c) -> f18(a + 1, a + 1, c) [ 10 >= a + 1 ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c) -> f18(4, 4, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 ] with all transitions in problem 9, the following new transitions are obtained: f0(a, b, c) -> f18(5, 5, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 ] f0(a, b, c) -> f18(4, 3, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ d >= e + 1 ] We thus obtain the following problem: 10: T: (1, 8) f0(a, b, c) -> f18(5, 5, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 ] (1, 7) f0(a, b, c) -> f18(4, 3, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ d >= e + 1 ] (1, 5) f0(a, b, c) -> f18(3, 2, f) [ 10 >= 2 /\ 10 >= 3 /\ d >= e + 1 ] (1, 3) f0(a, b, c) -> f18(2, 1, f) [ 10 >= 2 /\ d >= e + 1 ] (17, 2) f18(a, b, c) -> f18(a + 1, a + 1, c) [ 10 >= a + 1 ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c) -> f18(5, 5, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 ] with all transitions in problem 10, the following new transitions are obtained: f0(a, b, c) -> f18(6, 6, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 ] f0(a, b, c) -> f18(5, 4, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ d >= e + 1 ] We thus obtain the following problem: 11: T: (1, 10) f0(a, b, c) -> f18(6, 6, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 ] (1, 9) f0(a, b, c) -> f18(5, 4, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ d >= e + 1 ] (1, 7) f0(a, b, c) -> f18(4, 3, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ d >= e + 1 ] (1, 5) f0(a, b, c) -> f18(3, 2, f) [ 10 >= 2 /\ 10 >= 3 /\ d >= e + 1 ] (1, 3) f0(a, b, c) -> f18(2, 1, f) [ 10 >= 2 /\ d >= e + 1 ] (17, 2) f18(a, b, c) -> f18(a + 1, a + 1, c) [ 10 >= a + 1 ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c) -> f18(6, 6, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 ] with all transitions in problem 11, the following new transitions are obtained: f0(a, b, c) -> f18(7, 7, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 ] f0(a, b, c) -> f18(6, 5, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ d >= e + 1 ] We thus obtain the following problem: 12: T: (1, 12) f0(a, b, c) -> f18(7, 7, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 ] (1, 11) f0(a, b, c) -> f18(6, 5, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ d >= e + 1 ] (1, 9) f0(a, b, c) -> f18(5, 4, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ d >= e + 1 ] (1, 7) f0(a, b, c) -> f18(4, 3, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ d >= e + 1 ] (1, 5) f0(a, b, c) -> f18(3, 2, f) [ 10 >= 2 /\ 10 >= 3 /\ d >= e + 1 ] (1, 3) f0(a, b, c) -> f18(2, 1, f) [ 10 >= 2 /\ d >= e + 1 ] (17, 2) f18(a, b, c) -> f18(a + 1, a + 1, c) [ 10 >= a + 1 ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c) -> f18(7, 7, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 ] with all transitions in problem 12, the following new transitions are obtained: f0(a, b, c) -> f18(8, 8, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 ] f0(a, b, c) -> f18(7, 6, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ d >= e + 1 ] We thus obtain the following problem: 13: T: (1, 14) f0(a, b, c) -> f18(8, 8, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 ] (1, 13) f0(a, b, c) -> f18(7, 6, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ d >= e + 1 ] (1, 11) f0(a, b, c) -> f18(6, 5, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ d >= e + 1 ] (1, 9) f0(a, b, c) -> f18(5, 4, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ d >= e + 1 ] (1, 7) f0(a, b, c) -> f18(4, 3, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ d >= e + 1 ] (1, 5) f0(a, b, c) -> f18(3, 2, f) [ 10 >= 2 /\ 10 >= 3 /\ d >= e + 1 ] (1, 3) f0(a, b, c) -> f18(2, 1, f) [ 10 >= 2 /\ d >= e + 1 ] (17, 2) f18(a, b, c) -> f18(a + 1, a + 1, c) [ 10 >= a + 1 ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c) -> f18(8, 8, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 ] with all transitions in problem 13, the following new transitions are obtained: f0(a, b, c) -> f18(9, 9, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 ] f0(a, b, c) -> f18(8, 7, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ d >= e + 1 ] We thus obtain the following problem: 14: T: (1, 16) f0(a, b, c) -> f18(9, 9, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 ] (1, 15) f0(a, b, c) -> f18(8, 7, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ d >= e + 1 ] (1, 13) f0(a, b, c) -> f18(7, 6, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ d >= e + 1 ] (1, 11) f0(a, b, c) -> f18(6, 5, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ d >= e + 1 ] (1, 9) f0(a, b, c) -> f18(5, 4, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ d >= e + 1 ] (1, 7) f0(a, b, c) -> f18(4, 3, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ d >= e + 1 ] (1, 5) f0(a, b, c) -> f18(3, 2, f) [ 10 >= 2 /\ 10 >= 3 /\ d >= e + 1 ] (1, 3) f0(a, b, c) -> f18(2, 1, f) [ 10 >= 2 /\ d >= e + 1 ] (17, 2) f18(a, b, c) -> f18(a + 1, a + 1, c) [ 10 >= a + 1 ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c) -> f18(9, 9, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 ] with all transitions in problem 14, the following new transitions are obtained: f0(a, b, c) -> f18(10, 10, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 ] f0(a, b, c) -> f18(9, 8, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ d >= e + 1 ] We thus obtain the following problem: 15: T: (1, 18) f0(a, b, c) -> f18(10, 10, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 ] (1, 17) f0(a, b, c) -> f18(9, 8, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ d >= e + 1 ] (1, 15) f0(a, b, c) -> f18(8, 7, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ d >= e + 1 ] (1, 13) f0(a, b, c) -> f18(7, 6, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ d >= e + 1 ] (1, 11) f0(a, b, c) -> f18(6, 5, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ d >= e + 1 ] (1, 9) f0(a, b, c) -> f18(5, 4, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ d >= e + 1 ] (1, 7) f0(a, b, c) -> f18(4, 3, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ d >= e + 1 ] (1, 5) f0(a, b, c) -> f18(3, 2, f) [ 10 >= 2 /\ 10 >= 3 /\ d >= e + 1 ] (1, 3) f0(a, b, c) -> f18(2, 1, f) [ 10 >= 2 /\ d >= e + 1 ] (17, 2) f18(a, b, c) -> f18(a + 1, a + 1, c) [ 10 >= a + 1 ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c) -> f18(10, 10, c) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 ] with all transitions in problem 15, the following new transition is obtained: f0(a, b, c) -> f18(10, 9, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 /\ d >= e + 1 ] We thus obtain the following problem: 16: T: (1, 19) f0(a, b, c) -> f18(10, 9, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 /\ d >= e + 1 ] (1, 17) f0(a, b, c) -> f18(9, 8, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ d >= e + 1 ] (1, 15) f0(a, b, c) -> f18(8, 7, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ d >= e + 1 ] (1, 13) f0(a, b, c) -> f18(7, 6, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ d >= e + 1 ] (1, 11) f0(a, b, c) -> f18(6, 5, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ d >= e + 1 ] (1, 9) f0(a, b, c) -> f18(5, 4, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ d >= e + 1 ] (1, 7) f0(a, b, c) -> f18(4, 3, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ d >= e + 1 ] (1, 5) f0(a, b, c) -> f18(3, 2, f) [ 10 >= 2 /\ 10 >= 3 /\ d >= e + 1 ] (1, 3) f0(a, b, c) -> f18(2, 1, f) [ 10 >= 2 /\ d >= e + 1 ] (17, 2) f18(a, b, c) -> f18(a + 1, a + 1, c) [ 10 >= a + 1 ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c) -> f18(10, 9, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 /\ d >= e + 1 ] with all transitions in problem 16, the following new transition is obtained: f0(a, b, c) -> f18(10, 8, f') [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 /\ d >= e + 1 /\ d' >= e' + 1 ] We thus obtain the following problem: 17: T: (1, 20) f0(a, b, c) -> f18(10, 8, f') [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 /\ d >= e + 1 /\ d' >= e' + 1 ] (1, 17) f0(a, b, c) -> f18(9, 8, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ d >= e + 1 ] (1, 15) f0(a, b, c) -> f18(8, 7, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ d >= e + 1 ] (1, 13) f0(a, b, c) -> f18(7, 6, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ d >= e + 1 ] (1, 11) f0(a, b, c) -> f18(6, 5, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ d >= e + 1 ] (1, 9) f0(a, b, c) -> f18(5, 4, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ d >= e + 1 ] (1, 7) f0(a, b, c) -> f18(4, 3, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ d >= e + 1 ] (1, 5) f0(a, b, c) -> f18(3, 2, f) [ 10 >= 2 /\ 10 >= 3 /\ d >= e + 1 ] (1, 3) f0(a, b, c) -> f18(2, 1, f) [ 10 >= 2 /\ d >= e + 1 ] (17, 2) f18(a, b, c) -> f18(a + 1, a + 1, c) [ 10 >= a + 1 ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c) -> f18(10, 8, f') [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 /\ d >= e + 1 /\ d' >= e' + 1 ] with all transitions in problem 17, the following new transition is obtained: f0(a, b, c) -> f18(10, 7, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 /\ d >= e + 1 /\ d' >= e' + 1 /\ d'' >= e'' + 1 ] We thus obtain the following problem: 18: T: (1, 21) f0(a, b, c) -> f18(10, 7, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 /\ d >= e + 1 /\ d' >= e' + 1 /\ d'' >= e'' + 1 ] (1, 17) f0(a, b, c) -> f18(9, 8, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ d >= e + 1 ] (1, 15) f0(a, b, c) -> f18(8, 7, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ d >= e + 1 ] (1, 13) f0(a, b, c) -> f18(7, 6, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ d >= e + 1 ] (1, 11) f0(a, b, c) -> f18(6, 5, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ d >= e + 1 ] (1, 9) f0(a, b, c) -> f18(5, 4, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ d >= e + 1 ] (1, 7) f0(a, b, c) -> f18(4, 3, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ d >= e + 1 ] (1, 5) f0(a, b, c) -> f18(3, 2, f) [ 10 >= 2 /\ 10 >= 3 /\ d >= e + 1 ] (1, 3) f0(a, b, c) -> f18(2, 1, f) [ 10 >= 2 /\ d >= e + 1 ] (17, 2) f18(a, b, c) -> f18(a + 1, a + 1, c) [ 10 >= a + 1 ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c) -> f18(10, 7, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 /\ d >= e + 1 /\ d' >= e' + 1 /\ d'' >= e'' + 1 ] with all transitions in problem 18, the following new transition is obtained: f0(a, b, c) -> f18(10, 6, f') [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 /\ d >= e + 1 /\ d' >= e' + 1 /\ d'' >= e'' + 1 /\ d''' >= e''' + 1 ] We thus obtain the following problem: 19: T: (1, 22) f0(a, b, c) -> f18(10, 6, f') [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 /\ d >= e + 1 /\ d' >= e' + 1 /\ d'' >= e'' + 1 /\ d''' >= e''' + 1 ] (1, 17) f0(a, b, c) -> f18(9, 8, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ d >= e + 1 ] (1, 15) f0(a, b, c) -> f18(8, 7, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ d >= e + 1 ] (1, 13) f0(a, b, c) -> f18(7, 6, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ d >= e + 1 ] (1, 11) f0(a, b, c) -> f18(6, 5, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ d >= e + 1 ] (1, 9) f0(a, b, c) -> f18(5, 4, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ d >= e + 1 ] (1, 7) f0(a, b, c) -> f18(4, 3, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ d >= e + 1 ] (1, 5) f0(a, b, c) -> f18(3, 2, f) [ 10 >= 2 /\ 10 >= 3 /\ d >= e + 1 ] (1, 3) f0(a, b, c) -> f18(2, 1, f) [ 10 >= 2 /\ d >= e + 1 ] (17, 2) f18(a, b, c) -> f18(a + 1, a + 1, c) [ 10 >= a + 1 ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] start location: f0 leaf cost: 1 By chaining the transition f0(a, b, c) -> f18(10, 6, f') [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 /\ d >= e + 1 /\ d' >= e' + 1 /\ d'' >= e'' + 1 /\ d''' >= e''' + 1 ] with all transitions in problem 19, the following new transition is obtained: f0(a, b, c) -> f18(10, 5, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 /\ d >= e + 1 /\ d' >= e' + 1 /\ d'' >= e'' + 1 /\ d''' >= e''' + 1 /\ d'''' >= e'''' + 1 ] We thus obtain the following problem: 20: T: (1, 23) f0(a, b, c) -> f18(10, 5, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ 10 >= 10 /\ d >= e + 1 /\ d' >= e' + 1 /\ d'' >= e'' + 1 /\ d''' >= e''' + 1 /\ d'''' >= e'''' + 1 ] (1, 17) f0(a, b, c) -> f18(9, 8, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ 10 >= 9 /\ d >= e + 1 ] (1, 15) f0(a, b, c) -> f18(8, 7, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ 10 >= 8 /\ d >= e + 1 ] (1, 13) f0(a, b, c) -> f18(7, 6, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ 10 >= 7 /\ d >= e + 1 ] (1, 11) f0(a, b, c) -> f18(6, 5, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ 10 >= 6 /\ d >= e + 1 ] (1, 9) f0(a, b, c) -> f18(5, 4, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ 10 >= 5 /\ d >= e + 1 ] (1, 7) f0(a, b, c) -> f18(4, 3, f) [ 10 >= 2 /\ 10 >= 3 /\ 10 >= 4 /\ d >= e + 1 ] (1, 5) f0(a, b, c) -> f18(3, 2, f) [ 10 >= 2 /\ 10 >= 3 /\ d >= e + 1 ] (1, 3) f0(a, b, c) -> f18(2, 1, f) [ 10 >= 2 /\ d >= e + 1 ] (17, 2) f18(a, b, c) -> f18(a + 1, a + 1, c) [ 10 >= a + 1 ] (?, 1) f18(a, b, c) -> f18(a, b - 1, f) [ d >= e + 1 ] start location: f0 leaf cost: 1 Complexity upper bound ? Time: 4.195 sec (SMT: 3.849 sec)