MAYBE Initial complexity problem: 1: T: (?, 1) f11(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f11(a, p, b, o, e, f, g, h, i, j, k, l, m, n) [ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f11(a, p, b, o, e, f, g, h, i, j, k, l, m, n) [ a >= 0 /\ 0 >= b + 1 ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f16(a, b, c, d, e, f, g + 1, o, o, o, k, l, m, n) [ e >= 0 /\ f >= g + 2 ] (?, 1) f11(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f13(a, 0, c, d, e, f, g, h, i, j, o, l, m, n) [ a >= 0 /\ b = 0 ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f11(a, r, p, q, e, f, g, h, i, j, o, j, j, n) [ g + 1 >= f /\ p >= 1 /\ e >= 0 ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f11(a, r, p, q, e, f, g, h, i, j, o, j, j, n) [ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f16(a, b, c, d, e, f, 1, o, o, o, k, l, m, p) [ f >= 2 ] (1, 1) f300(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f13(a, 0, c, d, e, f, 0, h, i, 0, o, 0, 0, p) [ 1 >= f ] start location: f300 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, e, f, g]. We thus obtain the following problem: 2: T: (1, 1) f300(a, b, e, f, g) -> f13(a, 0, e, f, 0) [ 1 >= f ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] (?, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (?, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ g + 1 >= f /\ p >= 1 /\ e >= 0 ] (?, 1) f11(a, b, e, f, g) -> f13(a, 0, e, f, g) [ a >= 0 /\ b = 0 ] (?, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ e >= 0 /\ f >= g + 2 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ a >= 0 /\ 0 >= b + 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ a >= 0 /\ b >= 1 ] start location: f300 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] (?, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (?, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ g + 1 >= f /\ p >= 1 /\ e >= 0 ] (?, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ e >= 0 /\ f >= g + 2 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ a >= 0 /\ 0 >= b + 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ a >= 0 /\ b >= 1 ] start location: f300 leaf cost: 2 A polynomial rank function with Pol(f300) = 1 Pol(f16) = 1 Pol(f11) = -1 orients all transitions weakly and the transition f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ g + 1 >= f /\ p >= 1 /\ e >= 0 ] strictly and produces the following problem: 4: T: (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] (?, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ g + 1 >= f /\ p >= 1 /\ e >= 0 ] (?, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ e >= 0 /\ f >= g + 2 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ a >= 0 /\ 0 >= b + 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ a >= 0 /\ b >= 1 ] start location: f300 leaf cost: 2 A polynomial rank function with Pol(f300) = 1 Pol(f16) = 1 Pol(f11) = -1 orients all transitions weakly and the transition f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] strictly and produces the following problem: 5: T: (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ g + 1 >= f /\ p >= 1 /\ e >= 0 ] (?, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ e >= 0 /\ f >= g + 2 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ a >= 0 /\ 0 >= b + 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ a >= 0 /\ b >= 1 ] start location: f300 leaf cost: 2 A polynomial rank function with Pol(f300) = V_3 + V_4 - 1 Pol(f16) = V_3 + V_4 - V_5 - 1 Pol(f11) = V_3 + V_4 - V_5 - 1 orients all transitions weakly and the transition f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ e >= 0 /\ f >= g + 2 ] strictly and produces the following problem: 6: T: (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ g + 1 >= f /\ p >= 1 /\ e >= 0 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ e >= 0 /\ f >= g + 2 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ a >= 0 /\ 0 >= b + 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ a >= 0 /\ b >= 1 ] start location: f300 leaf cost: 2 Applied AI with 'oct' on problem 6 to obtain the following invariants: For symbol f11: X_4 - X_5 - 1 >= 0 /\ X_5 - 1 >= 0 /\ X_4 + X_5 - 3 >= 0 /\ -X_4 + X_5 + 1 >= 0 /\ X_3 + X_5 - 1 >= 0 /\ X_4 - 2 >= 0 /\ X_3 + X_4 - 2 >= 0 /\ X_3 >= 0 For symbol f16: X_4 - X_5 - 1 >= 0 /\ X_5 - 1 >= 0 /\ X_4 + X_5 - 3 >= 0 /\ X_4 - 2 >= 0 This yielded the following problem: 7: T: (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ 0 >= b + 1 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ e >= 0 /\ f >= g + 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] start location: f300 leaf cost: 2 By chaining the transition f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 ] with all transitions in problem 7, the following new transitions are obtained: f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 ] f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ r >= 1 ] We thus obtain the following problem: 8: T: (1, 2) f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 ] (1, 2) f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ r >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ 0 >= b + 1 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ e >= 0 /\ f >= g + 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] start location: f300 leaf cost: 2 By chaining the transition f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 ] with all transitions in problem 8, the following new transitions are obtained: f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 ] f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ p' >= 1 ] We thus obtain the following problem: 9: T: (1, 3) f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 ] (1, 3) f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ p' >= 1 ] (1, 2) f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ r >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ 0 >= b + 1 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ e >= 0 /\ f >= g + 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] start location: f300 leaf cost: 2 By chaining the transition f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 ] with all transitions in problem 9, the following new transitions are obtained: f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 ] f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ p'' >= 1 ] We thus obtain the following problem: 10: T: (1, 4) f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 ] (1, 4) f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ p'' >= 1 ] (1, 3) f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ p' >= 1 ] (1, 2) f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ r >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ 0 >= b + 1 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ e >= 0 /\ f >= g + 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] start location: f300 leaf cost: 2 By chaining the transition f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 ] with all transitions in problem 10, the following new transitions are obtained: f16(a, b, e, f, g) -> f11(a, p'''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 ] f16(a, b, e, f, g) -> f11(a, p'''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ p''' >= 1 ] We thus obtain the following problem: 11: T: (1, 5) f16(a, b, e, f, g) -> f11(a, p'''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 ] (1, 5) f16(a, b, e, f, g) -> f11(a, p'''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ p''' >= 1 ] (1, 4) f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ p'' >= 1 ] (1, 3) f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ p' >= 1 ] (1, 2) f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ r >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ 0 >= b + 1 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ e >= 0 /\ f >= g + 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] start location: f300 leaf cost: 2 By chaining the transition f16(a, b, e, f, g) -> f11(a, p'''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 ] with all transitions in problem 11, the following new transitions are obtained: f16(a, b, e, f, g) -> f11(a, p''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 ] f16(a, b, e, f, g) -> f11(a, p''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ p'''' >= 1 ] We thus obtain the following problem: 12: T: (1, 6) f16(a, b, e, f, g) -> f11(a, p''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 ] (1, 6) f16(a, b, e, f, g) -> f11(a, p''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ p'''' >= 1 ] (1, 5) f16(a, b, e, f, g) -> f11(a, p'''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ p''' >= 1 ] (1, 4) f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ p'' >= 1 ] (1, 3) f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ p' >= 1 ] (1, 2) f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ r >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ 0 >= b + 1 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ e >= 0 /\ f >= g + 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] start location: f300 leaf cost: 2 By chaining the transition f16(a, b, e, f, g) -> f11(a, p''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 ] with all transitions in problem 12, the following new transitions are obtained: f16(a, b, e, f, g) -> f11(a, p'''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 ] f16(a, b, e, f, g) -> f11(a, p'''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ p''''' >= 1 ] We thus obtain the following problem: 13: T: (1, 7) f16(a, b, e, f, g) -> f11(a, p'''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 ] (1, 7) f16(a, b, e, f, g) -> f11(a, p'''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ p''''' >= 1 ] (1, 6) f16(a, b, e, f, g) -> f11(a, p''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ p'''' >= 1 ] (1, 5) f16(a, b, e, f, g) -> f11(a, p'''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ p''' >= 1 ] (1, 4) f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ p'' >= 1 ] (1, 3) f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ p' >= 1 ] (1, 2) f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ r >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ 0 >= b + 1 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ e >= 0 /\ f >= g + 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] start location: f300 leaf cost: 2 By chaining the transition f16(a, b, e, f, g) -> f11(a, p'''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 ] with all transitions in problem 13, the following new transitions are obtained: f16(a, b, e, f, g) -> f11(a, p''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 ] f16(a, b, e, f, g) -> f11(a, p''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ p'''''' >= 1 ] We thus obtain the following problem: 14: T: (1, 8) f16(a, b, e, f, g) -> f11(a, p''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 ] (1, 8) f16(a, b, e, f, g) -> f11(a, p''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ p'''''' >= 1 ] (1, 7) f16(a, b, e, f, g) -> f11(a, p'''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ p''''' >= 1 ] (1, 6) f16(a, b, e, f, g) -> f11(a, p''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ p'''' >= 1 ] (1, 5) f16(a, b, e, f, g) -> f11(a, p'''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ p''' >= 1 ] (1, 4) f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ p'' >= 1 ] (1, 3) f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ p' >= 1 ] (1, 2) f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ r >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ 0 >= b + 1 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ e >= 0 /\ f >= g + 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] start location: f300 leaf cost: 2 By chaining the transition f16(a, b, e, f, g) -> f11(a, p''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 ] with all transitions in problem 14, the following new transitions are obtained: f16(a, b, e, f, g) -> f11(a, p'''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 ] f16(a, b, e, f, g) -> f11(a, p'''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ p''''''' >= 1 ] We thus obtain the following problem: 15: T: (1, 9) f16(a, b, e, f, g) -> f11(a, p'''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 ] (1, 9) f16(a, b, e, f, g) -> f11(a, p'''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ p''''''' >= 1 ] (1, 8) f16(a, b, e, f, g) -> f11(a, p''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ p'''''' >= 1 ] (1, 7) f16(a, b, e, f, g) -> f11(a, p'''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ p''''' >= 1 ] (1, 6) f16(a, b, e, f, g) -> f11(a, p''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ p'''' >= 1 ] (1, 5) f16(a, b, e, f, g) -> f11(a, p'''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ p''' >= 1 ] (1, 4) f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ p'' >= 1 ] (1, 3) f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ p' >= 1 ] (1, 2) f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ r >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ 0 >= b + 1 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ e >= 0 /\ f >= g + 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] start location: f300 leaf cost: 2 By chaining the transition f16(a, b, e, f, g) -> f11(a, p'''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 ] with all transitions in problem 15, the following new transitions are obtained: f16(a, b, e, f, g) -> f11(a, p''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 ] f16(a, b, e, f, g) -> f11(a, p''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ p'''''''' >= 1 ] We thus obtain the following problem: 16: T: (1, 10) f16(a, b, e, f, g) -> f11(a, p''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 ] (1, 10) f16(a, b, e, f, g) -> f11(a, p''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ p'''''''' >= 1 ] (1, 9) f16(a, b, e, f, g) -> f11(a, p'''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ p''''''' >= 1 ] (1, 8) f16(a, b, e, f, g) -> f11(a, p''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ p'''''' >= 1 ] (1, 7) f16(a, b, e, f, g) -> f11(a, p'''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ p''''' >= 1 ] (1, 6) f16(a, b, e, f, g) -> f11(a, p''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ p'''' >= 1 ] (1, 5) f16(a, b, e, f, g) -> f11(a, p'''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ p''' >= 1 ] (1, 4) f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ p'' >= 1 ] (1, 3) f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ p' >= 1 ] (1, 2) f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ r >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ 0 >= b + 1 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ e >= 0 /\ f >= g + 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] start location: f300 leaf cost: 2 By chaining the transition f16(a, b, e, f, g) -> f11(a, p''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 ] with all transitions in problem 16, the following new transitions are obtained: f16(a, b, e, f, g) -> f11(a, p'''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 ] f16(a, b, e, f, g) -> f11(a, p'''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ p''''''''' >= 1 ] We thus obtain the following problem: 17: T: (1, 11) f16(a, b, e, f, g) -> f11(a, p'''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 ] (1, 11) f16(a, b, e, f, g) -> f11(a, p'''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ p''''''''' >= 1 ] (1, 10) f16(a, b, e, f, g) -> f11(a, p''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ p'''''''' >= 1 ] (1, 9) f16(a, b, e, f, g) -> f11(a, p'''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ p''''''' >= 1 ] (1, 8) f16(a, b, e, f, g) -> f11(a, p''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ p'''''' >= 1 ] (1, 7) f16(a, b, e, f, g) -> f11(a, p'''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ p''''' >= 1 ] (1, 6) f16(a, b, e, f, g) -> f11(a, p''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ p'''' >= 1 ] (1, 5) f16(a, b, e, f, g) -> f11(a, p'''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ p''' >= 1 ] (1, 4) f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ p'' >= 1 ] (1, 3) f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ p' >= 1 ] (1, 2) f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ r >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ 0 >= b + 1 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ e >= 0 /\ f >= g + 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] start location: f300 leaf cost: 2 By chaining the transition f16(a, b, e, f, g) -> f11(a, p'''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 ] with all transitions in problem 17, the following new transitions are obtained: f16(a, b, e, f, g) -> f11(a, p''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 ] f16(a, b, e, f, g) -> f11(a, p''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ p'''''''''' >= 1 ] We thus obtain the following problem: 18: T: (1, 12) f16(a, b, e, f, g) -> f11(a, p''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 ] (1, 12) f16(a, b, e, f, g) -> f11(a, p''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ p'''''''''' >= 1 ] (1, 11) f16(a, b, e, f, g) -> f11(a, p'''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ p''''''''' >= 1 ] (1, 10) f16(a, b, e, f, g) -> f11(a, p''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ p'''''''' >= 1 ] (1, 9) f16(a, b, e, f, g) -> f11(a, p'''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ p''''''' >= 1 ] (1, 8) f16(a, b, e, f, g) -> f11(a, p''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ p'''''' >= 1 ] (1, 7) f16(a, b, e, f, g) -> f11(a, p'''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ p''''' >= 1 ] (1, 6) f16(a, b, e, f, g) -> f11(a, p''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ p'''' >= 1 ] (1, 5) f16(a, b, e, f, g) -> f11(a, p'''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ p''' >= 1 ] (1, 4) f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ p'' >= 1 ] (1, 3) f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ p' >= 1 ] (1, 2) f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ r >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ 0 >= b + 1 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ e >= 0 /\ f >= g + 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] start location: f300 leaf cost: 2 By chaining the transition f16(a, b, e, f, g) -> f11(a, p''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 ] with all transitions in problem 18, the following new transitions are obtained: f16(a, b, e, f, g) -> f11(a, p'''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 ] f16(a, b, e, f, g) -> f11(a, p'''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ p''''''''''' >= 1 ] We thus obtain the following problem: 19: T: (1, 13) f16(a, b, e, f, g) -> f11(a, p'''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 ] (1, 13) f16(a, b, e, f, g) -> f11(a, p'''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ p''''''''''' >= 1 ] (1, 12) f16(a, b, e, f, g) -> f11(a, p''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ p'''''''''' >= 1 ] (1, 11) f16(a, b, e, f, g) -> f11(a, p'''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ p''''''''' >= 1 ] (1, 10) f16(a, b, e, f, g) -> f11(a, p''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ p'''''''' >= 1 ] (1, 9) f16(a, b, e, f, g) -> f11(a, p'''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ p''''''' >= 1 ] (1, 8) f16(a, b, e, f, g) -> f11(a, p''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ p'''''' >= 1 ] (1, 7) f16(a, b, e, f, g) -> f11(a, p'''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ p''''' >= 1 ] (1, 6) f16(a, b, e, f, g) -> f11(a, p''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ p'''' >= 1 ] (1, 5) f16(a, b, e, f, g) -> f11(a, p'''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ p''' >= 1 ] (1, 4) f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ p'' >= 1 ] (1, 3) f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ p' >= 1 ] (1, 2) f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ r >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ 0 >= b + 1 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ e >= 0 /\ f >= g + 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] start location: f300 leaf cost: 2 By chaining the transition f16(a, b, e, f, g) -> f11(a, p'''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 ] with all transitions in problem 19, the following new transitions are obtained: f16(a, b, e, f, g) -> f11(a, p''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ 0 >= p'''''''''''' + 1 ] f16(a, b, e, f, g) -> f11(a, p''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ p'''''''''''' >= 1 ] We thus obtain the following problem: 20: T: (1, 14) f16(a, b, e, f, g) -> f11(a, p''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ 0 >= p'''''''''''' + 1 ] (1, 14) f16(a, b, e, f, g) -> f11(a, p''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ p'''''''''''' >= 1 ] (1, 13) f16(a, b, e, f, g) -> f11(a, p'''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ p''''''''''' >= 1 ] (1, 12) f16(a, b, e, f, g) -> f11(a, p''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ p'''''''''' >= 1 ] (1, 11) f16(a, b, e, f, g) -> f11(a, p'''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ p''''''''' >= 1 ] (1, 10) f16(a, b, e, f, g) -> f11(a, p''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ p'''''''' >= 1 ] (1, 9) f16(a, b, e, f, g) -> f11(a, p'''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ p''''''' >= 1 ] (1, 8) f16(a, b, e, f, g) -> f11(a, p''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ p'''''' >= 1 ] (1, 7) f16(a, b, e, f, g) -> f11(a, p'''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ p''''' >= 1 ] (1, 6) f16(a, b, e, f, g) -> f11(a, p''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ p'''' >= 1 ] (1, 5) f16(a, b, e, f, g) -> f11(a, p'''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ p''' >= 1 ] (1, 4) f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ p'' >= 1 ] (1, 3) f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ p' >= 1 ] (1, 2) f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ r >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ 0 >= b + 1 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ e >= 0 /\ f >= g + 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] start location: f300 leaf cost: 2 By chaining the transition f16(a, b, e, f, g) -> f11(a, p''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ 0 >= p'''''''''''' + 1 ] with all transitions in problem 20, the following new transitions are obtained: f16(a, b, e, f, g) -> f11(a, p'''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ 0 >= p'''''''''''' + 1 /\ 0 >= p''''''''''''' + 1 ] f16(a, b, e, f, g) -> f11(a, p'''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ 0 >= p'''''''''''' + 1 /\ p''''''''''''' >= 1 ] We thus obtain the following problem: 21: T: (1, 15) f16(a, b, e, f, g) -> f11(a, p'''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ 0 >= p'''''''''''' + 1 /\ 0 >= p''''''''''''' + 1 ] (1, 15) f16(a, b, e, f, g) -> f11(a, p'''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ 0 >= p'''''''''''' + 1 /\ p''''''''''''' >= 1 ] (1, 14) f16(a, b, e, f, g) -> f11(a, p''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ p'''''''''''' >= 1 ] (1, 13) f16(a, b, e, f, g) -> f11(a, p'''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ p''''''''''' >= 1 ] (1, 12) f16(a, b, e, f, g) -> f11(a, p''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ p'''''''''' >= 1 ] (1, 11) f16(a, b, e, f, g) -> f11(a, p'''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ p''''''''' >= 1 ] (1, 10) f16(a, b, e, f, g) -> f11(a, p''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ p'''''''' >= 1 ] (1, 9) f16(a, b, e, f, g) -> f11(a, p'''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ p''''''' >= 1 ] (1, 8) f16(a, b, e, f, g) -> f11(a, p''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ p'''''' >= 1 ] (1, 7) f16(a, b, e, f, g) -> f11(a, p'''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ p''''' >= 1 ] (1, 6) f16(a, b, e, f, g) -> f11(a, p''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ p'''' >= 1 ] (1, 5) f16(a, b, e, f, g) -> f11(a, p'''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ p''' >= 1 ] (1, 4) f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ p'' >= 1 ] (1, 3) f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ p' >= 1 ] (1, 2) f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ r >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ 0 >= b + 1 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ e >= 0 /\ f >= g + 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] start location: f300 leaf cost: 2 By chaining the transition f16(a, b, e, f, g) -> f11(a, p'''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ 0 >= p'''''''''''' + 1 /\ 0 >= p''''''''''''' + 1 ] with all transitions in problem 21, the following new transitions are obtained: f16(a, b, e, f, g) -> f11(a, p''''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ 0 >= p'''''''''''' + 1 /\ 0 >= p''''''''''''' + 1 /\ 0 >= p'''''''''''''' + 1 ] f16(a, b, e, f, g) -> f11(a, p''''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ 0 >= p'''''''''''' + 1 /\ 0 >= p''''''''''''' + 1 /\ p'''''''''''''' >= 1 ] We thus obtain the following problem: 22: T: (1, 16) f16(a, b, e, f, g) -> f11(a, p''''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ 0 >= p'''''''''''' + 1 /\ 0 >= p''''''''''''' + 1 /\ 0 >= p'''''''''''''' + 1 ] (1, 16) f16(a, b, e, f, g) -> f11(a, p''''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ 0 >= p'''''''''''' + 1 /\ 0 >= p''''''''''''' + 1 /\ p'''''''''''''' >= 1 ] (1, 15) f16(a, b, e, f, g) -> f11(a, p'''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ 0 >= p'''''''''''' + 1 /\ p''''''''''''' >= 1 ] (1, 14) f16(a, b, e, f, g) -> f11(a, p''''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ 0 >= p''''''''''' + 1 /\ p'''''''''''' >= 1 ] (1, 13) f16(a, b, e, f, g) -> f11(a, p'''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ 0 >= p'''''''''' + 1 /\ p''''''''''' >= 1 ] (1, 12) f16(a, b, e, f, g) -> f11(a, p''''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ 0 >= p''''''''' + 1 /\ p'''''''''' >= 1 ] (1, 11) f16(a, b, e, f, g) -> f11(a, p'''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ 0 >= p'''''''' + 1 /\ p''''''''' >= 1 ] (1, 10) f16(a, b, e, f, g) -> f11(a, p''''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ 0 >= p''''''' + 1 /\ p'''''''' >= 1 ] (1, 9) f16(a, b, e, f, g) -> f11(a, p'''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ 0 >= p'''''' + 1 /\ p''''''' >= 1 ] (1, 8) f16(a, b, e, f, g) -> f11(a, p''''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ 0 >= p''''' + 1 /\ p'''''' >= 1 ] (1, 7) f16(a, b, e, f, g) -> f11(a, p'''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ 0 >= p'''' + 1 /\ p''''' >= 1 ] (1, 6) f16(a, b, e, f, g) -> f11(a, p''''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ 0 >= p''' + 1 /\ p'''' >= 1 ] (1, 5) f16(a, b, e, f, g) -> f11(a, p'''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ 0 >= p'' + 1 /\ p''' >= 1 ] (1, 4) f16(a, b, e, f, g) -> f11(a, p''', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ 0 >= p' + 1 /\ p'' >= 1 ] (1, 3) f16(a, b, e, f, g) -> f11(a, p'', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ 0 >= r + 1 /\ p' >= 1 ] (1, 2) f16(a, b, e, f, g) -> f11(a, p', e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ p >= 1 /\ e >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ e + f - 2 >= 0 /\ a >= 0 /\ r >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f11(a, b, e, f, g) -> f11(a, p, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ -f + g + 1 >= 0 /\ e + g - 1 >= 0 /\ f - 2 >= 0 /\ e + f - 2 >= 0 /\ e >= 0 /\ a >= 0 /\ 0 >= b + 1 ] (e + f + 1, 1) f16(a, b, e, f, g) -> f16(a, b, e, f, g + 1) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ e >= 0 /\ f >= g + 2 ] (1, 1) f16(a, b, e, f, g) -> f11(a, r, e, f, g) [ f - g - 1 >= 0 /\ g - 1 >= 0 /\ f + g - 3 >= 0 /\ f - 2 >= 0 /\ g + 1 >= f /\ 0 >= p + 1 /\ e >= 0 ] (1, 1) f300(a, b, e, f, g) -> f16(a, b, e, f, 1) [ f >= 2 ] start location: f300 leaf cost: 2 Complexity upper bound ? Time: 4.003 sec (SMT: 3.400 sec)