MAYBE Initial complexity problem: 1: T: (?, 1) f17(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) -> f17(a, q, c, d + 1, p, f, g, h, i, j, k, l, m, n, o) [ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) -> f17(a, q, c, d + 1, p, f, g, h, i, j, k, l, m, n, o) [ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f18(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) -> f17(a, q, c, 1, p, f, g, h, i, j, k, l, m, n, o) [ f >= 0 /\ a >= b + 1 ] (?, 1) f18(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) -> f17(a, q, c, 1, p, f, g, h, i, j, k, l, m, n, o) [ f >= 0 /\ b >= a + 1 ] (?, 1) f17(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) -> f20(b, b, c, d, e, f, p, h, i, j, k, l, m, n, o) [ c >= 0 /\ d >= 0 /\ b = a ] (1, 1) f22(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) -> f18(a, h, c, d, e, f, q, h, 2, p, p, p, p, 3, 0) [ a >= h + 1 /\ f >= 0 ] (1, 1) f22(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) -> f18(a, h, c, d, e, f, q, h, 2, p, p, p, p, 3, 0) [ h >= a + 1 /\ f >= 0 ] start location: f22 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, d, f, h]. We thus obtain the following problem: 2: T: (1, 1) f22(a, b, c, d, f, h) -> f18(a, h, c, d, f, h) [ h >= a + 1 /\ f >= 0 ] (1, 1) f22(a, b, c, d, f, h) -> f18(a, h, c, d, f, h) [ a >= h + 1 /\ f >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f20(b, b, c, d, f, h) [ c >= 0 /\ d >= 0 /\ b = a ] (?, 1) f18(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ f >= 0 /\ b >= a + 1 ] (?, 1) f18(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ f >= 0 /\ a >= b + 1 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ a >= b + 1 /\ c >= 0 /\ d >= 0 ] start location: f22 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (1, 1) f22(a, b, c, d, f, h) -> f18(a, h, c, d, f, h) [ h >= a + 1 /\ f >= 0 ] (1, 1) f22(a, b, c, d, f, h) -> f18(a, h, c, d, f, h) [ a >= h + 1 /\ f >= 0 ] (?, 1) f18(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ f >= 0 /\ b >= a + 1 ] (?, 1) f18(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ f >= 0 /\ a >= b + 1 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ a >= b + 1 /\ c >= 0 /\ d >= 0 ] start location: f22 leaf cost: 1 Repeatedly propagating knowledge in problem 3 produces the following problem: 4: T: (1, 1) f22(a, b, c, d, f, h) -> f18(a, h, c, d, f, h) [ h >= a + 1 /\ f >= 0 ] (1, 1) f22(a, b, c, d, f, h) -> f18(a, h, c, d, f, h) [ a >= h + 1 /\ f >= 0 ] (1, 1) f18(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ f >= 0 /\ b >= a + 1 ] (1, 1) f18(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ f >= 0 /\ a >= b + 1 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ a >= b + 1 /\ c >= 0 /\ d >= 0 ] start location: f22 leaf cost: 1 Applied AI with 'oct' on problem 4 to obtain the following invariants: For symbol f17: X_5 >= 0 /\ X_4 + X_5 - 1 >= 0 /\ X_4 - 1 >= 0 For symbol f18: X_2 - X_6 >= 0 /\ -X_2 + X_6 >= 0 /\ X_5 >= 0 This yielded the following problem: 5: T: (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (1, 1) f18(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ b - h >= 0 /\ -b + h >= 0 /\ f >= 0 /\ a >= b + 1 ] (1, 1) f18(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ b - h >= 0 /\ -b + h >= 0 /\ f >= 0 /\ b >= a + 1 ] (1, 1) f22(a, b, c, d, f, h) -> f18(a, h, c, d, f, h) [ a >= h + 1 /\ f >= 0 ] (1, 1) f22(a, b, c, d, f, h) -> f18(a, h, c, d, f, h) [ h >= a + 1 /\ f >= 0 ] start location: f22 leaf cost: 1 By chaining the transition f22(a, b, c, d, f, h) -> f18(a, h, c, d, f, h) [ a >= h + 1 /\ f >= 0 ] with all transitions in problem 5, the following new transition is obtained: f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] We thus obtain the following problem: 6: T: (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (1, 1) f18(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ b - h >= 0 /\ -b + h >= 0 /\ f >= 0 /\ a >= b + 1 ] (1, 1) f18(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ b - h >= 0 /\ -b + h >= 0 /\ f >= 0 /\ b >= a + 1 ] (1, 1) f22(a, b, c, d, f, h) -> f18(a, h, c, d, f, h) [ h >= a + 1 /\ f >= 0 ] start location: f22 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 6: f18(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ b - h >= 0 /\ -b + h >= 0 /\ f >= 0 /\ a >= b + 1 ] We thus obtain the following problem: 7: T: (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (1, 1) f18(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ b - h >= 0 /\ -b + h >= 0 /\ f >= 0 /\ b >= a + 1 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] (1, 1) f22(a, b, c, d, f, h) -> f18(a, h, c, d, f, h) [ h >= a + 1 /\ f >= 0 ] start location: f22 leaf cost: 1 By chaining the transition f22(a, b, c, d, f, h) -> f18(a, h, c, d, f, h) [ h >= a + 1 /\ f >= 0 ] with all transitions in problem 7, the following new transition is obtained: f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 ] We thus obtain the following problem: 8: T: (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (1, 1) f18(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ b - h >= 0 /\ -b + h >= 0 /\ f >= 0 /\ b >= a + 1 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] start location: f22 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 8: f18(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ b - h >= 0 /\ -b + h >= 0 /\ f >= 0 /\ b >= a + 1 ] We thus obtain the following problem: 9: T: (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] start location: f22 leaf cost: 1 By chaining the transition f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 ] with all transitions in problem 9, the following new transitions are obtained: f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 ] f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ a >= q + 1 /\ c >= 0 /\ 1 >= 0 ] We thus obtain the following problem: 10: T: (1, 3) f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 ] (1, 3) f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ a >= q + 1 /\ c >= 0 /\ 1 >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] start location: f22 leaf cost: 1 By chaining the transition f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 ] with all transitions in problem 10, the following new transitions are obtained: f22(a, b, c, d, f, h) -> f17(a, q'', c, 3, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 ] f22(a, b, c, d, f, h) -> f17(a, q'', c, 3, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ a >= q' + 1 /\ 2 >= 0 ] We thus obtain the following problem: 11: T: (1, 4) f22(a, b, c, d, f, h) -> f17(a, q'', c, 3, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 ] (1, 4) f22(a, b, c, d, f, h) -> f17(a, q'', c, 3, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ a >= q' + 1 /\ 2 >= 0 ] (1, 3) f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ a >= q + 1 /\ c >= 0 /\ 1 >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] start location: f22 leaf cost: 1 By chaining the transition f22(a, b, c, d, f, h) -> f17(a, q'', c, 3, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 ] with all transitions in problem 11, the following new transitions are obtained: f22(a, b, c, d, f, h) -> f17(a, q''', c, 4, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 ] f22(a, b, c, d, f, h) -> f17(a, q''', c, 4, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ a >= q'' + 1 /\ 3 >= 0 ] We thus obtain the following problem: 12: T: (1, 5) f22(a, b, c, d, f, h) -> f17(a, q''', c, 4, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 ] (1, 5) f22(a, b, c, d, f, h) -> f17(a, q''', c, 4, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ a >= q'' + 1 /\ 3 >= 0 ] (1, 4) f22(a, b, c, d, f, h) -> f17(a, q'', c, 3, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ a >= q' + 1 /\ 2 >= 0 ] (1, 3) f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ a >= q + 1 /\ c >= 0 /\ 1 >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] start location: f22 leaf cost: 1 By chaining the transition f22(a, b, c, d, f, h) -> f17(a, q''', c, 4, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 ] with all transitions in problem 12, the following new transitions are obtained: f22(a, b, c, d, f, h) -> f17(a, q'''', c, 5, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 ] f22(a, b, c, d, f, h) -> f17(a, q'''', c, 5, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ a >= q''' + 1 /\ 4 >= 0 ] We thus obtain the following problem: 13: T: (1, 6) f22(a, b, c, d, f, h) -> f17(a, q'''', c, 5, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 ] (1, 6) f22(a, b, c, d, f, h) -> f17(a, q'''', c, 5, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ a >= q''' + 1 /\ 4 >= 0 ] (1, 5) f22(a, b, c, d, f, h) -> f17(a, q''', c, 4, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ a >= q'' + 1 /\ 3 >= 0 ] (1, 4) f22(a, b, c, d, f, h) -> f17(a, q'', c, 3, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ a >= q' + 1 /\ 2 >= 0 ] (1, 3) f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ a >= q + 1 /\ c >= 0 /\ 1 >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] start location: f22 leaf cost: 1 By chaining the transition f22(a, b, c, d, f, h) -> f17(a, q'''', c, 5, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 ] with all transitions in problem 13, the following new transitions are obtained: f22(a, b, c, d, f, h) -> f17(a, q''''', c, 6, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 ] f22(a, b, c, d, f, h) -> f17(a, q''''', c, 6, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ a >= q'''' + 1 /\ 5 >= 0 ] We thus obtain the following problem: 14: T: (1, 7) f22(a, b, c, d, f, h) -> f17(a, q''''', c, 6, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 ] (1, 7) f22(a, b, c, d, f, h) -> f17(a, q''''', c, 6, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ a >= q'''' + 1 /\ 5 >= 0 ] (1, 6) f22(a, b, c, d, f, h) -> f17(a, q'''', c, 5, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ a >= q''' + 1 /\ 4 >= 0 ] (1, 5) f22(a, b, c, d, f, h) -> f17(a, q''', c, 4, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ a >= q'' + 1 /\ 3 >= 0 ] (1, 4) f22(a, b, c, d, f, h) -> f17(a, q'', c, 3, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ a >= q' + 1 /\ 2 >= 0 ] (1, 3) f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ a >= q + 1 /\ c >= 0 /\ 1 >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] start location: f22 leaf cost: 1 By chaining the transition f22(a, b, c, d, f, h) -> f17(a, q''''', c, 6, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 ] with all transitions in problem 14, the following new transitions are obtained: f22(a, b, c, d, f, h) -> f17(a, q'''''', c, 7, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 ] f22(a, b, c, d, f, h) -> f17(a, q'''''', c, 7, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ a >= q''''' + 1 /\ 6 >= 0 ] We thus obtain the following problem: 15: T: (1, 8) f22(a, b, c, d, f, h) -> f17(a, q'''''', c, 7, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 ] (1, 8) f22(a, b, c, d, f, h) -> f17(a, q'''''', c, 7, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ a >= q''''' + 1 /\ 6 >= 0 ] (1, 7) f22(a, b, c, d, f, h) -> f17(a, q''''', c, 6, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ a >= q'''' + 1 /\ 5 >= 0 ] (1, 6) f22(a, b, c, d, f, h) -> f17(a, q'''', c, 5, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ a >= q''' + 1 /\ 4 >= 0 ] (1, 5) f22(a, b, c, d, f, h) -> f17(a, q''', c, 4, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ a >= q'' + 1 /\ 3 >= 0 ] (1, 4) f22(a, b, c, d, f, h) -> f17(a, q'', c, 3, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ a >= q' + 1 /\ 2 >= 0 ] (1, 3) f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ a >= q + 1 /\ c >= 0 /\ 1 >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] start location: f22 leaf cost: 1 By chaining the transition f22(a, b, c, d, f, h) -> f17(a, q'''''', c, 7, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 ] with all transitions in problem 15, the following new transitions are obtained: f22(a, b, c, d, f, h) -> f17(a, q''''''', c, 8, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 ] f22(a, b, c, d, f, h) -> f17(a, q''''''', c, 8, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ a >= q'''''' + 1 /\ 7 >= 0 ] We thus obtain the following problem: 16: T: (1, 9) f22(a, b, c, d, f, h) -> f17(a, q''''''', c, 8, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 ] (1, 9) f22(a, b, c, d, f, h) -> f17(a, q''''''', c, 8, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ a >= q'''''' + 1 /\ 7 >= 0 ] (1, 8) f22(a, b, c, d, f, h) -> f17(a, q'''''', c, 7, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ a >= q''''' + 1 /\ 6 >= 0 ] (1, 7) f22(a, b, c, d, f, h) -> f17(a, q''''', c, 6, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ a >= q'''' + 1 /\ 5 >= 0 ] (1, 6) f22(a, b, c, d, f, h) -> f17(a, q'''', c, 5, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ a >= q''' + 1 /\ 4 >= 0 ] (1, 5) f22(a, b, c, d, f, h) -> f17(a, q''', c, 4, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ a >= q'' + 1 /\ 3 >= 0 ] (1, 4) f22(a, b, c, d, f, h) -> f17(a, q'', c, 3, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ a >= q' + 1 /\ 2 >= 0 ] (1, 3) f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ a >= q + 1 /\ c >= 0 /\ 1 >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] start location: f22 leaf cost: 1 By chaining the transition f22(a, b, c, d, f, h) -> f17(a, q''''''', c, 8, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 ] with all transitions in problem 16, the following new transitions are obtained: f22(a, b, c, d, f, h) -> f17(a, q'''''''', c, 9, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 ] f22(a, b, c, d, f, h) -> f17(a, q'''''''', c, 9, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ a >= q''''''' + 1 /\ 8 >= 0 ] We thus obtain the following problem: 17: T: (1, 10) f22(a, b, c, d, f, h) -> f17(a, q'''''''', c, 9, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 ] (1, 10) f22(a, b, c, d, f, h) -> f17(a, q'''''''', c, 9, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ a >= q''''''' + 1 /\ 8 >= 0 ] (1, 9) f22(a, b, c, d, f, h) -> f17(a, q''''''', c, 8, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ a >= q'''''' + 1 /\ 7 >= 0 ] (1, 8) f22(a, b, c, d, f, h) -> f17(a, q'''''', c, 7, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ a >= q''''' + 1 /\ 6 >= 0 ] (1, 7) f22(a, b, c, d, f, h) -> f17(a, q''''', c, 6, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ a >= q'''' + 1 /\ 5 >= 0 ] (1, 6) f22(a, b, c, d, f, h) -> f17(a, q'''', c, 5, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ a >= q''' + 1 /\ 4 >= 0 ] (1, 5) f22(a, b, c, d, f, h) -> f17(a, q''', c, 4, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ a >= q'' + 1 /\ 3 >= 0 ] (1, 4) f22(a, b, c, d, f, h) -> f17(a, q'', c, 3, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ a >= q' + 1 /\ 2 >= 0 ] (1, 3) f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ a >= q + 1 /\ c >= 0 /\ 1 >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] start location: f22 leaf cost: 1 By chaining the transition f22(a, b, c, d, f, h) -> f17(a, q'''''''', c, 9, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 ] with all transitions in problem 17, the following new transitions are obtained: f22(a, b, c, d, f, h) -> f17(a, q''''''''', c, 10, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 ] f22(a, b, c, d, f, h) -> f17(a, q''''''''', c, 10, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ a >= q'''''''' + 1 /\ 9 >= 0 ] We thus obtain the following problem: 18: T: (1, 11) f22(a, b, c, d, f, h) -> f17(a, q''''''''', c, 10, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 ] (1, 11) f22(a, b, c, d, f, h) -> f17(a, q''''''''', c, 10, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ a >= q'''''''' + 1 /\ 9 >= 0 ] (1, 10) f22(a, b, c, d, f, h) -> f17(a, q'''''''', c, 9, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ a >= q''''''' + 1 /\ 8 >= 0 ] (1, 9) f22(a, b, c, d, f, h) -> f17(a, q''''''', c, 8, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ a >= q'''''' + 1 /\ 7 >= 0 ] (1, 8) f22(a, b, c, d, f, h) -> f17(a, q'''''', c, 7, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ a >= q''''' + 1 /\ 6 >= 0 ] (1, 7) f22(a, b, c, d, f, h) -> f17(a, q''''', c, 6, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ a >= q'''' + 1 /\ 5 >= 0 ] (1, 6) f22(a, b, c, d, f, h) -> f17(a, q'''', c, 5, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ a >= q''' + 1 /\ 4 >= 0 ] (1, 5) f22(a, b, c, d, f, h) -> f17(a, q''', c, 4, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ a >= q'' + 1 /\ 3 >= 0 ] (1, 4) f22(a, b, c, d, f, h) -> f17(a, q'', c, 3, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ a >= q' + 1 /\ 2 >= 0 ] (1, 3) f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ a >= q + 1 /\ c >= 0 /\ 1 >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] start location: f22 leaf cost: 1 By chaining the transition f22(a, b, c, d, f, h) -> f17(a, q''''''''', c, 10, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 ] with all transitions in problem 18, the following new transitions are obtained: f22(a, b, c, d, f, h) -> f17(a, q'''''''''', c, 11, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 ] f22(a, b, c, d, f, h) -> f17(a, q'''''''''', c, 11, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ a >= q''''''''' + 1 /\ 10 >= 0 ] We thus obtain the following problem: 19: T: (1, 12) f22(a, b, c, d, f, h) -> f17(a, q'''''''''', c, 11, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 ] (1, 12) f22(a, b, c, d, f, h) -> f17(a, q'''''''''', c, 11, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ a >= q''''''''' + 1 /\ 10 >= 0 ] (1, 11) f22(a, b, c, d, f, h) -> f17(a, q''''''''', c, 10, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ a >= q'''''''' + 1 /\ 9 >= 0 ] (1, 10) f22(a, b, c, d, f, h) -> f17(a, q'''''''', c, 9, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ a >= q''''''' + 1 /\ 8 >= 0 ] (1, 9) f22(a, b, c, d, f, h) -> f17(a, q''''''', c, 8, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ a >= q'''''' + 1 /\ 7 >= 0 ] (1, 8) f22(a, b, c, d, f, h) -> f17(a, q'''''', c, 7, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ a >= q''''' + 1 /\ 6 >= 0 ] (1, 7) f22(a, b, c, d, f, h) -> f17(a, q''''', c, 6, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ a >= q'''' + 1 /\ 5 >= 0 ] (1, 6) f22(a, b, c, d, f, h) -> f17(a, q'''', c, 5, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ a >= q''' + 1 /\ 4 >= 0 ] (1, 5) f22(a, b, c, d, f, h) -> f17(a, q''', c, 4, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ a >= q'' + 1 /\ 3 >= 0 ] (1, 4) f22(a, b, c, d, f, h) -> f17(a, q'', c, 3, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ a >= q' + 1 /\ 2 >= 0 ] (1, 3) f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ a >= q + 1 /\ c >= 0 /\ 1 >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] start location: f22 leaf cost: 1 By chaining the transition f22(a, b, c, d, f, h) -> f17(a, q'''''''''', c, 11, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 ] with all transitions in problem 19, the following new transitions are obtained: f22(a, b, c, d, f, h) -> f17(a, q''''''''''', c, 12, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ q'''''''''' >= a + 1 /\ 11 >= 0 ] f22(a, b, c, d, f, h) -> f17(a, q''''''''''', c, 12, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ a >= q'''''''''' + 1 /\ 11 >= 0 ] We thus obtain the following problem: 20: T: (1, 13) f22(a, b, c, d, f, h) -> f17(a, q''''''''''', c, 12, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ q'''''''''' >= a + 1 /\ 11 >= 0 ] (1, 13) f22(a, b, c, d, f, h) -> f17(a, q''''''''''', c, 12, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ a >= q'''''''''' + 1 /\ 11 >= 0 ] (1, 12) f22(a, b, c, d, f, h) -> f17(a, q'''''''''', c, 11, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ a >= q''''''''' + 1 /\ 10 >= 0 ] (1, 11) f22(a, b, c, d, f, h) -> f17(a, q''''''''', c, 10, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ a >= q'''''''' + 1 /\ 9 >= 0 ] (1, 10) f22(a, b, c, d, f, h) -> f17(a, q'''''''', c, 9, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ a >= q''''''' + 1 /\ 8 >= 0 ] (1, 9) f22(a, b, c, d, f, h) -> f17(a, q''''''', c, 8, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ a >= q'''''' + 1 /\ 7 >= 0 ] (1, 8) f22(a, b, c, d, f, h) -> f17(a, q'''''', c, 7, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ a >= q''''' + 1 /\ 6 >= 0 ] (1, 7) f22(a, b, c, d, f, h) -> f17(a, q''''', c, 6, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ a >= q'''' + 1 /\ 5 >= 0 ] (1, 6) f22(a, b, c, d, f, h) -> f17(a, q'''', c, 5, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ a >= q''' + 1 /\ 4 >= 0 ] (1, 5) f22(a, b, c, d, f, h) -> f17(a, q''', c, 4, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ a >= q'' + 1 /\ 3 >= 0 ] (1, 4) f22(a, b, c, d, f, h) -> f17(a, q'', c, 3, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ a >= q' + 1 /\ 2 >= 0 ] (1, 3) f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ a >= q + 1 /\ c >= 0 /\ 1 >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] start location: f22 leaf cost: 1 By chaining the transition f22(a, b, c, d, f, h) -> f17(a, q''''''''''', c, 12, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ q'''''''''' >= a + 1 /\ 11 >= 0 ] with all transitions in problem 20, the following new transitions are obtained: f22(a, b, c, d, f, h) -> f17(a, q'''''''''''', c, 13, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ q'''''''''' >= a + 1 /\ 11 >= 0 /\ f + 11 >= 0 /\ q''''''''''' >= a + 1 /\ 12 >= 0 ] f22(a, b, c, d, f, h) -> f17(a, q'''''''''''', c, 13, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ q'''''''''' >= a + 1 /\ 11 >= 0 /\ f + 11 >= 0 /\ a >= q''''''''''' + 1 /\ 12 >= 0 ] We thus obtain the following problem: 21: T: (1, 14) f22(a, b, c, d, f, h) -> f17(a, q'''''''''''', c, 13, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ q'''''''''' >= a + 1 /\ 11 >= 0 /\ f + 11 >= 0 /\ q''''''''''' >= a + 1 /\ 12 >= 0 ] (1, 14) f22(a, b, c, d, f, h) -> f17(a, q'''''''''''', c, 13, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ q'''''''''' >= a + 1 /\ 11 >= 0 /\ f + 11 >= 0 /\ a >= q''''''''''' + 1 /\ 12 >= 0 ] (1, 13) f22(a, b, c, d, f, h) -> f17(a, q''''''''''', c, 12, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ a >= q'''''''''' + 1 /\ 11 >= 0 ] (1, 12) f22(a, b, c, d, f, h) -> f17(a, q'''''''''', c, 11, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ a >= q''''''''' + 1 /\ 10 >= 0 ] (1, 11) f22(a, b, c, d, f, h) -> f17(a, q''''''''', c, 10, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ a >= q'''''''' + 1 /\ 9 >= 0 ] (1, 10) f22(a, b, c, d, f, h) -> f17(a, q'''''''', c, 9, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ a >= q''''''' + 1 /\ 8 >= 0 ] (1, 9) f22(a, b, c, d, f, h) -> f17(a, q''''''', c, 8, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ a >= q'''''' + 1 /\ 7 >= 0 ] (1, 8) f22(a, b, c, d, f, h) -> f17(a, q'''''', c, 7, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ a >= q''''' + 1 /\ 6 >= 0 ] (1, 7) f22(a, b, c, d, f, h) -> f17(a, q''''', c, 6, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ a >= q'''' + 1 /\ 5 >= 0 ] (1, 6) f22(a, b, c, d, f, h) -> f17(a, q'''', c, 5, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ a >= q''' + 1 /\ 4 >= 0 ] (1, 5) f22(a, b, c, d, f, h) -> f17(a, q''', c, 4, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ a >= q'' + 1 /\ 3 >= 0 ] (1, 4) f22(a, b, c, d, f, h) -> f17(a, q'', c, 3, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ a >= q' + 1 /\ 2 >= 0 ] (1, 3) f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ a >= q + 1 /\ c >= 0 /\ 1 >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] start location: f22 leaf cost: 1 By chaining the transition f22(a, b, c, d, f, h) -> f17(a, q'''''''''''', c, 13, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ q'''''''''' >= a + 1 /\ 11 >= 0 /\ f + 11 >= 0 /\ q''''''''''' >= a + 1 /\ 12 >= 0 ] with all transitions in problem 21, the following new transitions are obtained: f22(a, b, c, d, f, h) -> f17(a, q''''''''''''', c, 14, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ q'''''''''' >= a + 1 /\ 11 >= 0 /\ f + 11 >= 0 /\ q''''''''''' >= a + 1 /\ 12 >= 0 /\ f + 12 >= 0 /\ q'''''''''''' >= a + 1 /\ 13 >= 0 ] f22(a, b, c, d, f, h) -> f17(a, q''''''''''''', c, 14, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ q'''''''''' >= a + 1 /\ 11 >= 0 /\ f + 11 >= 0 /\ q''''''''''' >= a + 1 /\ 12 >= 0 /\ f + 12 >= 0 /\ a >= q'''''''''''' + 1 /\ 13 >= 0 ] We thus obtain the following problem: 22: T: (1, 15) f22(a, b, c, d, f, h) -> f17(a, q''''''''''''', c, 14, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ q'''''''''' >= a + 1 /\ 11 >= 0 /\ f + 11 >= 0 /\ q''''''''''' >= a + 1 /\ 12 >= 0 /\ f + 12 >= 0 /\ q'''''''''''' >= a + 1 /\ 13 >= 0 ] (1, 15) f22(a, b, c, d, f, h) -> f17(a, q''''''''''''', c, 14, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ q'''''''''' >= a + 1 /\ 11 >= 0 /\ f + 11 >= 0 /\ q''''''''''' >= a + 1 /\ 12 >= 0 /\ f + 12 >= 0 /\ a >= q'''''''''''' + 1 /\ 13 >= 0 ] (1, 14) f22(a, b, c, d, f, h) -> f17(a, q'''''''''''', c, 13, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ q'''''''''' >= a + 1 /\ 11 >= 0 /\ f + 11 >= 0 /\ a >= q''''''''''' + 1 /\ 12 >= 0 ] (1, 13) f22(a, b, c, d, f, h) -> f17(a, q''''''''''', c, 12, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ q''''''''' >= a + 1 /\ 10 >= 0 /\ f + 10 >= 0 /\ a >= q'''''''''' + 1 /\ 11 >= 0 ] (1, 12) f22(a, b, c, d, f, h) -> f17(a, q'''''''''', c, 11, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ q'''''''' >= a + 1 /\ 9 >= 0 /\ f + 9 >= 0 /\ a >= q''''''''' + 1 /\ 10 >= 0 ] (1, 11) f22(a, b, c, d, f, h) -> f17(a, q''''''''', c, 10, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ q''''''' >= a + 1 /\ 8 >= 0 /\ f + 8 >= 0 /\ a >= q'''''''' + 1 /\ 9 >= 0 ] (1, 10) f22(a, b, c, d, f, h) -> f17(a, q'''''''', c, 9, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ q'''''' >= a + 1 /\ 7 >= 0 /\ f + 7 >= 0 /\ a >= q''''''' + 1 /\ 8 >= 0 ] (1, 9) f22(a, b, c, d, f, h) -> f17(a, q''''''', c, 8, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ q''''' >= a + 1 /\ 6 >= 0 /\ f + 6 >= 0 /\ a >= q'''''' + 1 /\ 7 >= 0 ] (1, 8) f22(a, b, c, d, f, h) -> f17(a, q'''''', c, 7, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ q'''' >= a + 1 /\ 5 >= 0 /\ f + 5 >= 0 /\ a >= q''''' + 1 /\ 6 >= 0 ] (1, 7) f22(a, b, c, d, f, h) -> f17(a, q''''', c, 6, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ q''' >= a + 1 /\ 4 >= 0 /\ f + 4 >= 0 /\ a >= q'''' + 1 /\ 5 >= 0 ] (1, 6) f22(a, b, c, d, f, h) -> f17(a, q'''', c, 5, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ q'' >= a + 1 /\ 3 >= 0 /\ f + 3 >= 0 /\ a >= q''' + 1 /\ 4 >= 0 ] (1, 5) f22(a, b, c, d, f, h) -> f17(a, q''', c, 4, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ q' >= a + 1 /\ 2 >= 0 /\ f + 2 >= 0 /\ a >= q'' + 1 /\ 3 >= 0 ] (1, 4) f22(a, b, c, d, f, h) -> f17(a, q'', c, 3, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ q >= a + 1 /\ c >= 0 /\ 1 >= 0 /\ f + 1 >= 0 /\ a >= q' + 1 /\ 2 >= 0 ] (1, 3) f22(a, b, c, d, f, h) -> f17(a, q', c, 2, f, h) [ h >= a + 1 /\ f >= 0 /\ 0 >= 0 /\ a >= q + 1 /\ c >= 0 /\ 1 >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ b >= a + 1 /\ c >= 0 /\ d >= 0 ] (?, 1) f17(a, b, c, d, f, h) -> f17(a, q, c, d + 1, f, h) [ f >= 0 /\ d + f - 1 >= 0 /\ d - 1 >= 0 /\ a >= b + 1 /\ c >= 0 /\ d >= 0 ] (1, 2) f22(a, b, c, d, f, h) -> f17(a, q, c, 1, f, h) [ a >= h + 1 /\ f >= 0 /\ 0 >= 0 ] start location: f22 leaf cost: 1 Complexity upper bound ? Time: 2.937 sec (SMT: 2.510 sec)