MAYBE Initial complexity problem: 1: T: (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f9(a, b + 1, c + 1, s, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ a >= b + 1 /\ c >= 0 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f0(a, b, c, d, e, f, s, g, v, w, x, l, m, n, o, p, q, r) [ u >= t + 1 /\ e >= 1 /\ f >= 0 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f5(a, b, c, d, e + 1, f - 1, m, 0, w, x, k, m, n, v, s, e, q, r) [ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f12(a, b, c, d, e, f, g, 0, v, w, k, m, m, 0, o, e, s, r) [ x >= t /\ e >= 0 /\ f >= 0 /\ n = 0 /\ h = 0 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f5(a, b, c, d, 1, t + c - 3, s, 0, u, a1, k, s, v, x, w, p, d, c - 2) [ c >= 2 /\ b >= a /\ y >= z ] (1, 1) f6(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f9(17, 1, 0, s, e, f, g, h, i, j, k, v, m, n, o, p, q, r) start location: f6 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, e, f, g, h, m, n]. We thus obtain the following problem: 2: T: (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) (?, 1) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 1, t + c - 3, s, 0, v, x) [ c >= 2 /\ b >= a /\ y >= z ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f12(a, b, c, e, f, g, 0, m, 0) [ x >= t /\ e >= 0 /\ f >= 0 /\ n = 0 /\ h = 0 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f0(a, b, c, e, f, s, g, m, n) [ u >= t + 1 /\ e >= 1 /\ f >= 0 ] (?, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ a >= b + 1 /\ c >= 0 ] start location: f6 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) (?, 1) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 1, t + c - 3, s, 0, v, x) [ c >= 2 /\ b >= a /\ y >= z ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (?, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ a >= b + 1 /\ c >= 0 ] start location: f6 leaf cost: 2 A polynomial rank function with Pol(f6) = 1 Pol(f9) = 1 Pol(f5) = 0 orients all transitions weakly and the transition f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 1, t + c - 3, s, 0, v, x) [ c >= 2 /\ b >= a /\ y >= z ] strictly and produces the following problem: 4: T: (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) (1, 1) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 1, t + c - 3, s, 0, v, x) [ c >= 2 /\ b >= a /\ y >= z ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (?, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ a >= b + 1 /\ c >= 0 ] start location: f6 leaf cost: 2 A polynomial rank function with Pol(f6) = 31 Pol(f9) = 2*V_1 - 2*V_2 + V_3 - 1 Pol(f5) = 2*V_1 - 2*V_2 + V_3 - V_4 orients all transitions weakly and the transition f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ a >= b + 1 /\ c >= 0 ] strictly and produces the following problem: 5: T: (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) (1, 1) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 1, t + c - 3, s, 0, v, x) [ c >= 2 /\ b >= a /\ y >= z ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ a >= b + 1 /\ c >= 0 ] start location: f6 leaf cost: 2 Applied AI with 'oct' on problem 5 to obtain the following invariants: For symbol f5: -X_7 >= 0 /\ X_4 - X_7 - 1 >= 0 /\ X_3 - X_7 - 16 >= 0 /\ X_2 - X_7 - 17 >= 0 /\ X_1 - X_7 - 17 >= 0 /\ -X_1 - X_7 + 17 >= 0 /\ X_7 >= 0 /\ X_4 + X_7 - 1 >= 0 /\ X_3 + X_7 - 16 >= 0 /\ X_2 + X_7 - 17 >= 0 /\ X_1 + X_7 - 17 >= 0 /\ -X_1 + X_7 + 17 >= 0 /\ X_4 - 1 >= 0 /\ X_3 + X_4 - 17 >= 0 /\ X_2 + X_4 - 18 >= 0 /\ X_1 + X_4 - 18 >= 0 /\ -X_1 + X_4 + 16 >= 0 /\ X_2 - X_3 - 1 >= 0 /\ X_3 - 16 >= 0 /\ X_2 + X_3 - 33 >= 0 /\ -X_2 + X_3 + 1 >= 0 /\ X_1 + X_3 - 33 >= 0 /\ -X_1 + X_3 + 1 >= 0 /\ X_2 - 17 >= 0 /\ X_1 + X_2 - 34 >= 0 /\ -X_1 + X_2 >= 0 /\ -X_1 + 17 >= 0 /\ X_1 - 17 >= 0 For symbol f9: X_2 - X_3 - 1 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ -X_2 + X_3 + 1 >= 0 /\ X_1 + X_3 - 17 >= 0 /\ -X_1 + X_3 + 17 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 18 >= 0 /\ -X_1 + X_2 + 16 >= 0 /\ -X_1 + 17 >= 0 /\ X_1 - 17 >= 0 This yielded the following problem: 6: T: (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ -h >= 0 /\ e - h - 1 >= 0 /\ c - h - 16 >= 0 /\ b - h - 17 >= 0 /\ a - h - 17 >= 0 /\ -a - h + 17 >= 0 /\ h >= 0 /\ e + h - 1 >= 0 /\ c + h - 16 >= 0 /\ b + h - 17 >= 0 /\ a + h - 17 >= 0 /\ -a + h + 17 >= 0 /\ e - 1 >= 0 /\ c + e - 17 >= 0 /\ b + e - 18 >= 0 /\ a + e - 18 >= 0 /\ -a + e + 16 >= 0 /\ b - c - 1 >= 0 /\ c - 16 >= 0 /\ b + c - 33 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ b - 17 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (1, 1) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 1, t + c - 3, s, 0, v, x) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z ] (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) start location: f6 leaf cost: 2 By chaining the transition f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 1, t + c - 3, s, 0, v, x) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z ] with all transitions in problem 6, the following new transition is obtained: f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 2, t + c - 4, v, 0, x, v') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 ] We thus obtain the following problem: 7: T: (1, 2) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 2, t + c - 4, v, 0, x, v') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 ] (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ -h >= 0 /\ e - h - 1 >= 0 /\ c - h - 16 >= 0 /\ b - h - 17 >= 0 /\ a - h - 17 >= 0 /\ -a - h + 17 >= 0 /\ h >= 0 /\ e + h - 1 >= 0 /\ c + h - 16 >= 0 /\ b + h - 17 >= 0 /\ a + h - 17 >= 0 /\ -a + h + 17 >= 0 /\ e - 1 >= 0 /\ c + e - 17 >= 0 /\ b + e - 18 >= 0 /\ a + e - 18 >= 0 /\ -a + e + 16 >= 0 /\ b - c - 1 >= 0 /\ c - 16 >= 0 /\ b + c - 33 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ b - 17 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) start location: f6 leaf cost: 2 By chaining the transition f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 2, t + c - 4, v, 0, x, v') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 ] with all transitions in problem 7, the following new transition is obtained: f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 3, t + c - 5, x, 0, v', v'') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 ] We thus obtain the following problem: 8: T: (1, 3) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 3, t + c - 5, x, 0, v', v'') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 ] (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ -h >= 0 /\ e - h - 1 >= 0 /\ c - h - 16 >= 0 /\ b - h - 17 >= 0 /\ a - h - 17 >= 0 /\ -a - h + 17 >= 0 /\ h >= 0 /\ e + h - 1 >= 0 /\ c + h - 16 >= 0 /\ b + h - 17 >= 0 /\ a + h - 17 >= 0 /\ -a + h + 17 >= 0 /\ e - 1 >= 0 /\ c + e - 17 >= 0 /\ b + e - 18 >= 0 /\ a + e - 18 >= 0 /\ -a + e + 16 >= 0 /\ b - c - 1 >= 0 /\ c - 16 >= 0 /\ b + c - 33 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ b - 17 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) start location: f6 leaf cost: 2 By chaining the transition f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 3, t + c - 5, x, 0, v', v'') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 ] with all transitions in problem 8, the following new transition is obtained: f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 4, t + c - 6, v', 0, v'', v) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 ] We thus obtain the following problem: 9: T: (1, 4) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 4, t + c - 6, v', 0, v'', v) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 ] (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ -h >= 0 /\ e - h - 1 >= 0 /\ c - h - 16 >= 0 /\ b - h - 17 >= 0 /\ a - h - 17 >= 0 /\ -a - h + 17 >= 0 /\ h >= 0 /\ e + h - 1 >= 0 /\ c + h - 16 >= 0 /\ b + h - 17 >= 0 /\ a + h - 17 >= 0 /\ -a + h + 17 >= 0 /\ e - 1 >= 0 /\ c + e - 17 >= 0 /\ b + e - 18 >= 0 /\ a + e - 18 >= 0 /\ -a + e + 16 >= 0 /\ b - c - 1 >= 0 /\ c - 16 >= 0 /\ b + c - 33 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ b - 17 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) start location: f6 leaf cost: 2 By chaining the transition f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 4, t + c - 6, v', 0, v'', v) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 ] with all transitions in problem 9, the following new transition is obtained: f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 5, t + c - 7, v'', 0, v, v''') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 ] We thus obtain the following problem: 10: T: (1, 5) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 5, t + c - 7, v'', 0, v, v''') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 ] (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ -h >= 0 /\ e - h - 1 >= 0 /\ c - h - 16 >= 0 /\ b - h - 17 >= 0 /\ a - h - 17 >= 0 /\ -a - h + 17 >= 0 /\ h >= 0 /\ e + h - 1 >= 0 /\ c + h - 16 >= 0 /\ b + h - 17 >= 0 /\ a + h - 17 >= 0 /\ -a + h + 17 >= 0 /\ e - 1 >= 0 /\ c + e - 17 >= 0 /\ b + e - 18 >= 0 /\ a + e - 18 >= 0 /\ -a + e + 16 >= 0 /\ b - c - 1 >= 0 /\ c - 16 >= 0 /\ b + c - 33 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ b - 17 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) start location: f6 leaf cost: 2 By chaining the transition f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 5, t + c - 7, v'', 0, v, v''') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 ] with all transitions in problem 10, the following new transition is obtained: f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 6, t + c - 8, v, 0, v''', v') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 ] We thus obtain the following problem: 11: T: (1, 6) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 6, t + c - 8, v, 0, v''', v') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 ] (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ -h >= 0 /\ e - h - 1 >= 0 /\ c - h - 16 >= 0 /\ b - h - 17 >= 0 /\ a - h - 17 >= 0 /\ -a - h + 17 >= 0 /\ h >= 0 /\ e + h - 1 >= 0 /\ c + h - 16 >= 0 /\ b + h - 17 >= 0 /\ a + h - 17 >= 0 /\ -a + h + 17 >= 0 /\ e - 1 >= 0 /\ c + e - 17 >= 0 /\ b + e - 18 >= 0 /\ a + e - 18 >= 0 /\ -a + e + 16 >= 0 /\ b - c - 1 >= 0 /\ c - 16 >= 0 /\ b + c - 33 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ b - 17 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) start location: f6 leaf cost: 2 By chaining the transition f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 6, t + c - 8, v, 0, v''', v') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 ] with all transitions in problem 11, the following new transition is obtained: f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 7, t + c - 9, v''', 0, v', v'') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 ] We thus obtain the following problem: 12: T: (1, 7) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 7, t + c - 9, v''', 0, v', v'') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 ] (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ -h >= 0 /\ e - h - 1 >= 0 /\ c - h - 16 >= 0 /\ b - h - 17 >= 0 /\ a - h - 17 >= 0 /\ -a - h + 17 >= 0 /\ h >= 0 /\ e + h - 1 >= 0 /\ c + h - 16 >= 0 /\ b + h - 17 >= 0 /\ a + h - 17 >= 0 /\ -a + h + 17 >= 0 /\ e - 1 >= 0 /\ c + e - 17 >= 0 /\ b + e - 18 >= 0 /\ a + e - 18 >= 0 /\ -a + e + 16 >= 0 /\ b - c - 1 >= 0 /\ c - 16 >= 0 /\ b + c - 33 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ b - 17 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) start location: f6 leaf cost: 2 By chaining the transition f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 7, t + c - 9, v''', 0, v', v'') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 ] with all transitions in problem 12, the following new transition is obtained: f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 8, t + c - 10, v', 0, v'', v) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 ] We thus obtain the following problem: 13: T: (1, 8) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 8, t + c - 10, v', 0, v'', v) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 ] (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ -h >= 0 /\ e - h - 1 >= 0 /\ c - h - 16 >= 0 /\ b - h - 17 >= 0 /\ a - h - 17 >= 0 /\ -a - h + 17 >= 0 /\ h >= 0 /\ e + h - 1 >= 0 /\ c + h - 16 >= 0 /\ b + h - 17 >= 0 /\ a + h - 17 >= 0 /\ -a + h + 17 >= 0 /\ e - 1 >= 0 /\ c + e - 17 >= 0 /\ b + e - 18 >= 0 /\ a + e - 18 >= 0 /\ -a + e + 16 >= 0 /\ b - c - 1 >= 0 /\ c - 16 >= 0 /\ b + c - 33 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ b - 17 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) start location: f6 leaf cost: 2 By chaining the transition f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 8, t + c - 10, v', 0, v'', v) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 ] with all transitions in problem 13, the following new transition is obtained: f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 9, t + c - 11, v'', 0, v, v''') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 ] We thus obtain the following problem: 14: T: (1, 9) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 9, t + c - 11, v'', 0, v, v''') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 ] (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ -h >= 0 /\ e - h - 1 >= 0 /\ c - h - 16 >= 0 /\ b - h - 17 >= 0 /\ a - h - 17 >= 0 /\ -a - h + 17 >= 0 /\ h >= 0 /\ e + h - 1 >= 0 /\ c + h - 16 >= 0 /\ b + h - 17 >= 0 /\ a + h - 17 >= 0 /\ -a + h + 17 >= 0 /\ e - 1 >= 0 /\ c + e - 17 >= 0 /\ b + e - 18 >= 0 /\ a + e - 18 >= 0 /\ -a + e + 16 >= 0 /\ b - c - 1 >= 0 /\ c - 16 >= 0 /\ b + c - 33 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ b - 17 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) start location: f6 leaf cost: 2 By chaining the transition f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 9, t + c - 11, v'', 0, v, v''') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 ] with all transitions in problem 14, the following new transition is obtained: f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 10, t + c - 12, v, 0, v''', v') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 ] We thus obtain the following problem: 15: T: (1, 10) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 10, t + c - 12, v, 0, v''', v') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 ] (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ -h >= 0 /\ e - h - 1 >= 0 /\ c - h - 16 >= 0 /\ b - h - 17 >= 0 /\ a - h - 17 >= 0 /\ -a - h + 17 >= 0 /\ h >= 0 /\ e + h - 1 >= 0 /\ c + h - 16 >= 0 /\ b + h - 17 >= 0 /\ a + h - 17 >= 0 /\ -a + h + 17 >= 0 /\ e - 1 >= 0 /\ c + e - 17 >= 0 /\ b + e - 18 >= 0 /\ a + e - 18 >= 0 /\ -a + e + 16 >= 0 /\ b - c - 1 >= 0 /\ c - 16 >= 0 /\ b + c - 33 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ b - 17 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) start location: f6 leaf cost: 2 By chaining the transition f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 10, t + c - 12, v, 0, v''', v') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 ] with all transitions in problem 15, the following new transition is obtained: f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 11, t + c - 13, v''', 0, v', v'') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 ] We thus obtain the following problem: 16: T: (1, 11) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 11, t + c - 13, v''', 0, v', v'') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 ] (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ -h >= 0 /\ e - h - 1 >= 0 /\ c - h - 16 >= 0 /\ b - h - 17 >= 0 /\ a - h - 17 >= 0 /\ -a - h + 17 >= 0 /\ h >= 0 /\ e + h - 1 >= 0 /\ c + h - 16 >= 0 /\ b + h - 17 >= 0 /\ a + h - 17 >= 0 /\ -a + h + 17 >= 0 /\ e - 1 >= 0 /\ c + e - 17 >= 0 /\ b + e - 18 >= 0 /\ a + e - 18 >= 0 /\ -a + e + 16 >= 0 /\ b - c - 1 >= 0 /\ c - 16 >= 0 /\ b + c - 33 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ b - 17 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) start location: f6 leaf cost: 2 By chaining the transition f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 11, t + c - 13, v''', 0, v', v'') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 ] with all transitions in problem 16, the following new transition is obtained: f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 12, t + c - 14, v', 0, v'', v) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 /\ c - 6 >= 0 /\ b - 7 >= 0 /\ a - 7 >= 0 /\ -a + 27 >= 0 /\ t''''''''''' >= u'''''''''' /\ 11 >= 0 /\ t + c - 13 >= 0 ] We thus obtain the following problem: 17: T: (1, 12) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 12, t + c - 14, v', 0, v'', v) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 /\ c - 6 >= 0 /\ b - 7 >= 0 /\ a - 7 >= 0 /\ -a + 27 >= 0 /\ t''''''''''' >= u'''''''''' /\ 11 >= 0 /\ t + c - 13 >= 0 ] (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ -h >= 0 /\ e - h - 1 >= 0 /\ c - h - 16 >= 0 /\ b - h - 17 >= 0 /\ a - h - 17 >= 0 /\ -a - h + 17 >= 0 /\ h >= 0 /\ e + h - 1 >= 0 /\ c + h - 16 >= 0 /\ b + h - 17 >= 0 /\ a + h - 17 >= 0 /\ -a + h + 17 >= 0 /\ e - 1 >= 0 /\ c + e - 17 >= 0 /\ b + e - 18 >= 0 /\ a + e - 18 >= 0 /\ -a + e + 16 >= 0 /\ b - c - 1 >= 0 /\ c - 16 >= 0 /\ b + c - 33 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ b - 17 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) start location: f6 leaf cost: 2 By chaining the transition f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 12, t + c - 14, v', 0, v'', v) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 /\ c - 6 >= 0 /\ b - 7 >= 0 /\ a - 7 >= 0 /\ -a + 27 >= 0 /\ t''''''''''' >= u'''''''''' /\ 11 >= 0 /\ t + c - 13 >= 0 ] with all transitions in problem 17, the following new transition is obtained: f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 13, t + c - 15, v'', 0, v, v''') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 /\ c - 6 >= 0 /\ b - 7 >= 0 /\ a - 7 >= 0 /\ -a + 27 >= 0 /\ t''''''''''' >= u'''''''''' /\ 11 >= 0 /\ t + c - 13 >= 0 /\ c - 5 >= 0 /\ b - 6 >= 0 /\ a - 6 >= 0 /\ -a + 28 >= 0 /\ t'''''''''''' >= u''''''''''' /\ 12 >= 0 /\ t + c - 14 >= 0 ] We thus obtain the following problem: 18: T: (1, 13) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 13, t + c - 15, v'', 0, v, v''') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 /\ c - 6 >= 0 /\ b - 7 >= 0 /\ a - 7 >= 0 /\ -a + 27 >= 0 /\ t''''''''''' >= u'''''''''' /\ 11 >= 0 /\ t + c - 13 >= 0 /\ c - 5 >= 0 /\ b - 6 >= 0 /\ a - 6 >= 0 /\ -a + 28 >= 0 /\ t'''''''''''' >= u''''''''''' /\ 12 >= 0 /\ t + c - 14 >= 0 ] (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ -h >= 0 /\ e - h - 1 >= 0 /\ c - h - 16 >= 0 /\ b - h - 17 >= 0 /\ a - h - 17 >= 0 /\ -a - h + 17 >= 0 /\ h >= 0 /\ e + h - 1 >= 0 /\ c + h - 16 >= 0 /\ b + h - 17 >= 0 /\ a + h - 17 >= 0 /\ -a + h + 17 >= 0 /\ e - 1 >= 0 /\ c + e - 17 >= 0 /\ b + e - 18 >= 0 /\ a + e - 18 >= 0 /\ -a + e + 16 >= 0 /\ b - c - 1 >= 0 /\ c - 16 >= 0 /\ b + c - 33 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ b - 17 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) start location: f6 leaf cost: 2 By chaining the transition f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 13, t + c - 15, v'', 0, v, v''') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 /\ c - 6 >= 0 /\ b - 7 >= 0 /\ a - 7 >= 0 /\ -a + 27 >= 0 /\ t''''''''''' >= u'''''''''' /\ 11 >= 0 /\ t + c - 13 >= 0 /\ c - 5 >= 0 /\ b - 6 >= 0 /\ a - 6 >= 0 /\ -a + 28 >= 0 /\ t'''''''''''' >= u''''''''''' /\ 12 >= 0 /\ t + c - 14 >= 0 ] with all transitions in problem 18, the following new transition is obtained: f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 14, t + c - 16, v, 0, v''', v') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 /\ c - 6 >= 0 /\ b - 7 >= 0 /\ a - 7 >= 0 /\ -a + 27 >= 0 /\ t''''''''''' >= u'''''''''' /\ 11 >= 0 /\ t + c - 13 >= 0 /\ c - 5 >= 0 /\ b - 6 >= 0 /\ a - 6 >= 0 /\ -a + 28 >= 0 /\ t'''''''''''' >= u''''''''''' /\ 12 >= 0 /\ t + c - 14 >= 0 /\ c - 4 >= 0 /\ b - 5 >= 0 /\ a - 5 >= 0 /\ -a + 29 >= 0 /\ t''''''''''''' >= u'''''''''''' /\ 13 >= 0 /\ t + c - 15 >= 0 ] We thus obtain the following problem: 19: T: (1, 14) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 14, t + c - 16, v, 0, v''', v') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 /\ c - 6 >= 0 /\ b - 7 >= 0 /\ a - 7 >= 0 /\ -a + 27 >= 0 /\ t''''''''''' >= u'''''''''' /\ 11 >= 0 /\ t + c - 13 >= 0 /\ c - 5 >= 0 /\ b - 6 >= 0 /\ a - 6 >= 0 /\ -a + 28 >= 0 /\ t'''''''''''' >= u''''''''''' /\ 12 >= 0 /\ t + c - 14 >= 0 /\ c - 4 >= 0 /\ b - 5 >= 0 /\ a - 5 >= 0 /\ -a + 29 >= 0 /\ t''''''''''''' >= u'''''''''''' /\ 13 >= 0 /\ t + c - 15 >= 0 ] (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ -h >= 0 /\ e - h - 1 >= 0 /\ c - h - 16 >= 0 /\ b - h - 17 >= 0 /\ a - h - 17 >= 0 /\ -a - h + 17 >= 0 /\ h >= 0 /\ e + h - 1 >= 0 /\ c + h - 16 >= 0 /\ b + h - 17 >= 0 /\ a + h - 17 >= 0 /\ -a + h + 17 >= 0 /\ e - 1 >= 0 /\ c + e - 17 >= 0 /\ b + e - 18 >= 0 /\ a + e - 18 >= 0 /\ -a + e + 16 >= 0 /\ b - c - 1 >= 0 /\ c - 16 >= 0 /\ b + c - 33 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ b - 17 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) start location: f6 leaf cost: 2 By chaining the transition f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 14, t + c - 16, v, 0, v''', v') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 /\ c - 6 >= 0 /\ b - 7 >= 0 /\ a - 7 >= 0 /\ -a + 27 >= 0 /\ t''''''''''' >= u'''''''''' /\ 11 >= 0 /\ t + c - 13 >= 0 /\ c - 5 >= 0 /\ b - 6 >= 0 /\ a - 6 >= 0 /\ -a + 28 >= 0 /\ t'''''''''''' >= u''''''''''' /\ 12 >= 0 /\ t + c - 14 >= 0 /\ c - 4 >= 0 /\ b - 5 >= 0 /\ a - 5 >= 0 /\ -a + 29 >= 0 /\ t''''''''''''' >= u'''''''''''' /\ 13 >= 0 /\ t + c - 15 >= 0 ] with all transitions in problem 19, the following new transition is obtained: f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 15, t + c - 17, v''', 0, v', v'') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 /\ c - 6 >= 0 /\ b - 7 >= 0 /\ a - 7 >= 0 /\ -a + 27 >= 0 /\ t''''''''''' >= u'''''''''' /\ 11 >= 0 /\ t + c - 13 >= 0 /\ c - 5 >= 0 /\ b - 6 >= 0 /\ a - 6 >= 0 /\ -a + 28 >= 0 /\ t'''''''''''' >= u''''''''''' /\ 12 >= 0 /\ t + c - 14 >= 0 /\ c - 4 >= 0 /\ b - 5 >= 0 /\ a - 5 >= 0 /\ -a + 29 >= 0 /\ t''''''''''''' >= u'''''''''''' /\ 13 >= 0 /\ t + c - 15 >= 0 /\ c - 3 >= 0 /\ b - 4 >= 0 /\ a - 4 >= 0 /\ -a + 30 >= 0 /\ t'''''''''''''' >= u''''''''''''' /\ 14 >= 0 /\ t + c - 16 >= 0 ] We thus obtain the following problem: 20: T: (1, 15) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 15, t + c - 17, v''', 0, v', v'') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 /\ c - 6 >= 0 /\ b - 7 >= 0 /\ a - 7 >= 0 /\ -a + 27 >= 0 /\ t''''''''''' >= u'''''''''' /\ 11 >= 0 /\ t + c - 13 >= 0 /\ c - 5 >= 0 /\ b - 6 >= 0 /\ a - 6 >= 0 /\ -a + 28 >= 0 /\ t'''''''''''' >= u''''''''''' /\ 12 >= 0 /\ t + c - 14 >= 0 /\ c - 4 >= 0 /\ b - 5 >= 0 /\ a - 5 >= 0 /\ -a + 29 >= 0 /\ t''''''''''''' >= u'''''''''''' /\ 13 >= 0 /\ t + c - 15 >= 0 /\ c - 3 >= 0 /\ b - 4 >= 0 /\ a - 4 >= 0 /\ -a + 30 >= 0 /\ t'''''''''''''' >= u''''''''''''' /\ 14 >= 0 /\ t + c - 16 >= 0 ] (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ -h >= 0 /\ e - h - 1 >= 0 /\ c - h - 16 >= 0 /\ b - h - 17 >= 0 /\ a - h - 17 >= 0 /\ -a - h + 17 >= 0 /\ h >= 0 /\ e + h - 1 >= 0 /\ c + h - 16 >= 0 /\ b + h - 17 >= 0 /\ a + h - 17 >= 0 /\ -a + h + 17 >= 0 /\ e - 1 >= 0 /\ c + e - 17 >= 0 /\ b + e - 18 >= 0 /\ a + e - 18 >= 0 /\ -a + e + 16 >= 0 /\ b - c - 1 >= 0 /\ c - 16 >= 0 /\ b + c - 33 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ b - 17 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) start location: f6 leaf cost: 2 By chaining the transition f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 15, t + c - 17, v''', 0, v', v'') [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 /\ c - 6 >= 0 /\ b - 7 >= 0 /\ a - 7 >= 0 /\ -a + 27 >= 0 /\ t''''''''''' >= u'''''''''' /\ 11 >= 0 /\ t + c - 13 >= 0 /\ c - 5 >= 0 /\ b - 6 >= 0 /\ a - 6 >= 0 /\ -a + 28 >= 0 /\ t'''''''''''' >= u''''''''''' /\ 12 >= 0 /\ t + c - 14 >= 0 /\ c - 4 >= 0 /\ b - 5 >= 0 /\ a - 5 >= 0 /\ -a + 29 >= 0 /\ t''''''''''''' >= u'''''''''''' /\ 13 >= 0 /\ t + c - 15 >= 0 /\ c - 3 >= 0 /\ b - 4 >= 0 /\ a - 4 >= 0 /\ -a + 30 >= 0 /\ t'''''''''''''' >= u''''''''''''' /\ 14 >= 0 /\ t + c - 16 >= 0 ] with all transitions in problem 20, the following new transition is obtained: f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 16, t + c - 18, v', 0, v'', v) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 /\ c - 6 >= 0 /\ b - 7 >= 0 /\ a - 7 >= 0 /\ -a + 27 >= 0 /\ t''''''''''' >= u'''''''''' /\ 11 >= 0 /\ t + c - 13 >= 0 /\ c - 5 >= 0 /\ b - 6 >= 0 /\ a - 6 >= 0 /\ -a + 28 >= 0 /\ t'''''''''''' >= u''''''''''' /\ 12 >= 0 /\ t + c - 14 >= 0 /\ c - 4 >= 0 /\ b - 5 >= 0 /\ a - 5 >= 0 /\ -a + 29 >= 0 /\ t''''''''''''' >= u'''''''''''' /\ 13 >= 0 /\ t + c - 15 >= 0 /\ c - 3 >= 0 /\ b - 4 >= 0 /\ a - 4 >= 0 /\ -a + 30 >= 0 /\ t'''''''''''''' >= u''''''''''''' /\ 14 >= 0 /\ t + c - 16 >= 0 /\ c - 2 >= 0 /\ b - 3 >= 0 /\ a - 3 >= 0 /\ -a + 31 >= 0 /\ t''''''''''''''' >= u'''''''''''''' /\ 15 >= 0 /\ t + c - 17 >= 0 ] We thus obtain the following problem: 21: T: (1, 16) f9(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, 16, t + c - 18, v', 0, v'', v) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ c >= 2 /\ b >= a /\ y >= z /\ 0 >= 0 /\ c - 16 >= 0 /\ b - 17 >= 0 /\ b + c - 33 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ t' >= u /\ 1 >= 0 /\ t + c - 3 >= 0 /\ 0 = 0 /\ c - 15 >= 0 /\ b - 16 >= 0 /\ a - 16 >= 0 /\ -a + 18 >= 0 /\ t'' >= u' /\ 2 >= 0 /\ t + c - 4 >= 0 /\ c - 14 >= 0 /\ b - 15 >= 0 /\ a - 15 >= 0 /\ -a + 19 >= 0 /\ t''' >= u'' /\ 3 >= 0 /\ t + c - 5 >= 0 /\ c - 13 >= 0 /\ b - 14 >= 0 /\ a - 14 >= 0 /\ -a + 20 >= 0 /\ t'''' >= u''' /\ 4 >= 0 /\ t + c - 6 >= 0 /\ c - 12 >= 0 /\ b - 13 >= 0 /\ a - 13 >= 0 /\ -a + 21 >= 0 /\ t''''' >= u'''' /\ 5 >= 0 /\ t + c - 7 >= 0 /\ c - 11 >= 0 /\ b - 12 >= 0 /\ a - 12 >= 0 /\ -a + 22 >= 0 /\ t'''''' >= u''''' /\ 6 >= 0 /\ t + c - 8 >= 0 /\ c - 10 >= 0 /\ b - 11 >= 0 /\ a - 11 >= 0 /\ -a + 23 >= 0 /\ t''''''' >= u'''''' /\ 7 >= 0 /\ t + c - 9 >= 0 /\ c - 9 >= 0 /\ b - 10 >= 0 /\ a - 10 >= 0 /\ -a + 24 >= 0 /\ t'''''''' >= u''''''' /\ 8 >= 0 /\ t + c - 10 >= 0 /\ c - 8 >= 0 /\ b - 9 >= 0 /\ a - 9 >= 0 /\ -a + 25 >= 0 /\ t''''''''' >= u'''''''' /\ 9 >= 0 /\ t + c - 11 >= 0 /\ c - 7 >= 0 /\ b - 8 >= 0 /\ a - 8 >= 0 /\ -a + 26 >= 0 /\ t'''''''''' >= u''''''''' /\ 10 >= 0 /\ t + c - 12 >= 0 /\ c - 6 >= 0 /\ b - 7 >= 0 /\ a - 7 >= 0 /\ -a + 27 >= 0 /\ t''''''''''' >= u'''''''''' /\ 11 >= 0 /\ t + c - 13 >= 0 /\ c - 5 >= 0 /\ b - 6 >= 0 /\ a - 6 >= 0 /\ -a + 28 >= 0 /\ t'''''''''''' >= u''''''''''' /\ 12 >= 0 /\ t + c - 14 >= 0 /\ c - 4 >= 0 /\ b - 5 >= 0 /\ a - 5 >= 0 /\ -a + 29 >= 0 /\ t''''''''''''' >= u'''''''''''' /\ 13 >= 0 /\ t + c - 15 >= 0 /\ c - 3 >= 0 /\ b - 4 >= 0 /\ a - 4 >= 0 /\ -a + 30 >= 0 /\ t'''''''''''''' >= u''''''''''''' /\ 14 >= 0 /\ t + c - 16 >= 0 /\ c - 2 >= 0 /\ b - 3 >= 0 /\ a - 3 >= 0 /\ -a + 31 >= 0 /\ t''''''''''''''' >= u'''''''''''''' /\ 15 >= 0 /\ t + c - 17 >= 0 ] (31, 1) f9(a, b, c, e, f, g, h, m, n) -> f9(a, b + 1, c + 1, e, f, g, h, m, n) [ b - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 17 >= 0 /\ -a + c + 17 >= 0 /\ b - 1 >= 0 /\ a + b - 18 >= 0 /\ -a + b + 16 >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ a >= b + 1 ] (?, 1) f5(a, b, c, e, f, g, h, m, n) -> f5(a, b, c, e + 1, f - 1, m, 0, n, v) [ -h >= 0 /\ e - h - 1 >= 0 /\ c - h - 16 >= 0 /\ b - h - 17 >= 0 /\ a - h - 17 >= 0 /\ -a - h + 17 >= 0 /\ h >= 0 /\ e + h - 1 >= 0 /\ c + h - 16 >= 0 /\ b + h - 17 >= 0 /\ a + h - 17 >= 0 /\ -a + h + 17 >= 0 /\ e - 1 >= 0 /\ c + e - 17 >= 0 /\ b + e - 18 >= 0 /\ a + e - 18 >= 0 /\ -a + e + 16 >= 0 /\ b - c - 1 >= 0 /\ c - 16 >= 0 /\ b + c - 33 >= 0 /\ -b + c + 1 >= 0 /\ a + c - 33 >= 0 /\ -a + c + 1 >= 0 /\ b - 17 >= 0 /\ a + b - 34 >= 0 /\ -a + b >= 0 /\ -a + 17 >= 0 /\ a - 17 >= 0 /\ t >= u /\ e >= 0 /\ f >= 0 /\ h = 0 ] (1, 1) f6(a, b, c, e, f, g, h, m, n) -> f9(17, 1, 0, e, f, g, h, m, n) start location: f6 leaf cost: 2 Complexity upper bound ? Time: 3.886 sec (SMT: 3.152 sec)