MAYBE Initial complexity problem: 1: T: (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f1(a, b + 1, d, o, d, p, b, h, i, j, k, l, m, n) [ a >= b + 1 /\ b >= 0 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f4(p, q, r, u, t, f, g, o, s, v, w, c, m, n) [ b >= a /\ b >= 0 /\ q >= o /\ o >= 2 ] (1, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f4(r, s, q, v, u, f, g, p, t, w, y, 0, o, n) [ 0 >= p /\ 0 >= x ] (1, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f1(p, 2, r, q, r, f, g, p, r, j, k, l, o, s) [ p >= 2 ] (1, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f4(p, q, r, u, t, f, g, 1, s, v, w, d, o, n) start location: f3 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b]. We thus obtain the following problem: 2: T: (1, 1) f3(a, b) -> f4(p, q) (1, 1) f3(a, b) -> f1(p, 2) [ p >= 2 ] (1, 1) f3(a, b) -> f4(r, s) [ 0 >= p /\ 0 >= x ] (?, 1) f1(a, b) -> f4(p, q) [ b >= a /\ b >= 0 /\ q >= o /\ o >= 2 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (1, 1) f3(a, b) -> f1(p, 2) [ p >= 2 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 3 Applied AI with 'oct' on problem 3 to obtain the following invariants: For symbol f1: X_1 - X_2 >= 0 /\ X_2 - 2 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ X_1 - 2 >= 0 This yielded the following problem: 4: T: (?, 1) f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] (1, 1) f3(a, b) -> f1(p, 2) [ p >= 2 ] start location: f3 leaf cost: 3 By chaining the transition f3(a, b) -> f1(p, 2) [ p >= 2 ] with all transitions in problem 4, the following new transition is obtained: f3(a, b) -> f1(p, 3) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 ] We thus obtain the following problem: 5: T: (1, 2) f3(a, b) -> f1(p, 3) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 3 By chaining the transition f3(a, b) -> f1(p, 3) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 ] with all transitions in problem 5, the following new transition is obtained: f3(a, b) -> f1(p, 4) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 ] We thus obtain the following problem: 6: T: (1, 3) f3(a, b) -> f1(p, 4) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 3 By chaining the transition f3(a, b) -> f1(p, 4) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 ] with all transitions in problem 6, the following new transition is obtained: f3(a, b) -> f1(p, 5) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 ] We thus obtain the following problem: 7: T: (1, 4) f3(a, b) -> f1(p, 5) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 3 By chaining the transition f3(a, b) -> f1(p, 5) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 ] with all transitions in problem 7, the following new transition is obtained: f3(a, b) -> f1(p, 6) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 ] We thus obtain the following problem: 8: T: (1, 5) f3(a, b) -> f1(p, 6) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 3 By chaining the transition f3(a, b) -> f1(p, 6) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 ] with all transitions in problem 8, the following new transition is obtained: f3(a, b) -> f1(p, 7) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 ] We thus obtain the following problem: 9: T: (1, 6) f3(a, b) -> f1(p, 7) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 3 By chaining the transition f3(a, b) -> f1(p, 7) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 ] with all transitions in problem 9, the following new transition is obtained: f3(a, b) -> f1(p, 8) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 ] We thus obtain the following problem: 10: T: (1, 7) f3(a, b) -> f1(p, 8) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 3 By chaining the transition f3(a, b) -> f1(p, 8) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 ] with all transitions in problem 10, the following new transition is obtained: f3(a, b) -> f1(p, 9) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 ] We thus obtain the following problem: 11: T: (1, 8) f3(a, b) -> f1(p, 9) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 3 By chaining the transition f3(a, b) -> f1(p, 9) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 ] with all transitions in problem 11, the following new transition is obtained: f3(a, b) -> f1(p, 10) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 ] We thus obtain the following problem: 12: T: (1, 9) f3(a, b) -> f1(p, 10) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 3 By chaining the transition f3(a, b) -> f1(p, 10) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 ] with all transitions in problem 12, the following new transition is obtained: f3(a, b) -> f1(p, 11) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 ] We thus obtain the following problem: 13: T: (1, 10) f3(a, b) -> f1(p, 11) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 3 By chaining the transition f3(a, b) -> f1(p, 11) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 ] with all transitions in problem 13, the following new transition is obtained: f3(a, b) -> f1(p, 12) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 ] We thus obtain the following problem: 14: T: (1, 11) f3(a, b) -> f1(p, 12) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 3 By chaining the transition f3(a, b) -> f1(p, 12) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 ] with all transitions in problem 14, the following new transition is obtained: f3(a, b) -> f1(p, 13) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 /\ p - 12 >= 0 /\ p + 8 >= 0 /\ p >= 13 /\ 12 >= 0 ] We thus obtain the following problem: 15: T: (1, 12) f3(a, b) -> f1(p, 13) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 /\ p - 12 >= 0 /\ p + 8 >= 0 /\ p >= 13 /\ 12 >= 0 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 3 By chaining the transition f3(a, b) -> f1(p, 13) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 /\ p - 12 >= 0 /\ p + 8 >= 0 /\ p >= 13 /\ 12 >= 0 ] with all transitions in problem 15, the following new transition is obtained: f3(a, b) -> f1(p, 14) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 /\ p - 12 >= 0 /\ p + 8 >= 0 /\ p >= 13 /\ 12 >= 0 /\ p - 13 >= 0 /\ p + 9 >= 0 /\ p >= 14 /\ 13 >= 0 ] We thus obtain the following problem: 16: T: (1, 13) f3(a, b) -> f1(p, 14) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 /\ p - 12 >= 0 /\ p + 8 >= 0 /\ p >= 13 /\ 12 >= 0 /\ p - 13 >= 0 /\ p + 9 >= 0 /\ p >= 14 /\ 13 >= 0 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 3 By chaining the transition f3(a, b) -> f1(p, 14) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 /\ p - 12 >= 0 /\ p + 8 >= 0 /\ p >= 13 /\ 12 >= 0 /\ p - 13 >= 0 /\ p + 9 >= 0 /\ p >= 14 /\ 13 >= 0 ] with all transitions in problem 16, the following new transition is obtained: f3(a, b) -> f1(p, 15) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 /\ p - 12 >= 0 /\ p + 8 >= 0 /\ p >= 13 /\ 12 >= 0 /\ p - 13 >= 0 /\ p + 9 >= 0 /\ p >= 14 /\ 13 >= 0 /\ p - 14 >= 0 /\ p + 10 >= 0 /\ p >= 15 /\ 14 >= 0 ] We thus obtain the following problem: 17: T: (1, 14) f3(a, b) -> f1(p, 15) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 /\ p - 12 >= 0 /\ p + 8 >= 0 /\ p >= 13 /\ 12 >= 0 /\ p - 13 >= 0 /\ p + 9 >= 0 /\ p >= 14 /\ 13 >= 0 /\ p - 14 >= 0 /\ p + 10 >= 0 /\ p >= 15 /\ 14 >= 0 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 3 By chaining the transition f3(a, b) -> f1(p, 15) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 /\ p - 12 >= 0 /\ p + 8 >= 0 /\ p >= 13 /\ 12 >= 0 /\ p - 13 >= 0 /\ p + 9 >= 0 /\ p >= 14 /\ 13 >= 0 /\ p - 14 >= 0 /\ p + 10 >= 0 /\ p >= 15 /\ 14 >= 0 ] with all transitions in problem 17, the following new transition is obtained: f3(a, b) -> f1(p, 16) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 /\ p - 12 >= 0 /\ p + 8 >= 0 /\ p >= 13 /\ 12 >= 0 /\ p - 13 >= 0 /\ p + 9 >= 0 /\ p >= 14 /\ 13 >= 0 /\ p - 14 >= 0 /\ p + 10 >= 0 /\ p >= 15 /\ 14 >= 0 /\ p - 15 >= 0 /\ p + 11 >= 0 /\ p >= 16 /\ 15 >= 0 ] We thus obtain the following problem: 18: T: (1, 15) f3(a, b) -> f1(p, 16) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 /\ p - 12 >= 0 /\ p + 8 >= 0 /\ p >= 13 /\ 12 >= 0 /\ p - 13 >= 0 /\ p + 9 >= 0 /\ p >= 14 /\ 13 >= 0 /\ p - 14 >= 0 /\ p + 10 >= 0 /\ p >= 15 /\ 14 >= 0 /\ p - 15 >= 0 /\ p + 11 >= 0 /\ p >= 16 /\ 15 >= 0 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 3 By chaining the transition f3(a, b) -> f1(p, 16) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 /\ p - 12 >= 0 /\ p + 8 >= 0 /\ p >= 13 /\ 12 >= 0 /\ p - 13 >= 0 /\ p + 9 >= 0 /\ p >= 14 /\ 13 >= 0 /\ p - 14 >= 0 /\ p + 10 >= 0 /\ p >= 15 /\ 14 >= 0 /\ p - 15 >= 0 /\ p + 11 >= 0 /\ p >= 16 /\ 15 >= 0 ] with all transitions in problem 18, the following new transition is obtained: f3(a, b) -> f1(p, 17) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 /\ p - 12 >= 0 /\ p + 8 >= 0 /\ p >= 13 /\ 12 >= 0 /\ p - 13 >= 0 /\ p + 9 >= 0 /\ p >= 14 /\ 13 >= 0 /\ p - 14 >= 0 /\ p + 10 >= 0 /\ p >= 15 /\ 14 >= 0 /\ p - 15 >= 0 /\ p + 11 >= 0 /\ p >= 16 /\ 15 >= 0 /\ p - 16 >= 0 /\ p + 12 >= 0 /\ p >= 17 /\ 16 >= 0 ] We thus obtain the following problem: 19: T: (1, 16) f3(a, b) -> f1(p, 17) [ p >= 2 /\ p - 2 >= 0 /\ 0 >= 0 /\ p >= 3 /\ 2 >= 0 /\ p - 3 >= 0 /\ 1 >= 0 /\ p - 1 >= 0 /\ p >= 4 /\ 3 >= 0 /\ p - 4 >= 0 /\ p >= 0 /\ p >= 5 /\ 4 >= 0 /\ p - 5 >= 0 /\ p + 1 >= 0 /\ p >= 6 /\ 5 >= 0 /\ p - 6 >= 0 /\ p + 2 >= 0 /\ p >= 7 /\ 6 >= 0 /\ p - 7 >= 0 /\ p + 3 >= 0 /\ p >= 8 /\ 7 >= 0 /\ p - 8 >= 0 /\ p + 4 >= 0 /\ p >= 9 /\ 8 >= 0 /\ p - 9 >= 0 /\ p + 5 >= 0 /\ p >= 10 /\ 9 >= 0 /\ p - 10 >= 0 /\ p + 6 >= 0 /\ p >= 11 /\ 10 >= 0 /\ p - 11 >= 0 /\ p + 7 >= 0 /\ p >= 12 /\ 11 >= 0 /\ p - 12 >= 0 /\ p + 8 >= 0 /\ p >= 13 /\ 12 >= 0 /\ p - 13 >= 0 /\ p + 9 >= 0 /\ p >= 14 /\ 13 >= 0 /\ p - 14 >= 0 /\ p + 10 >= 0 /\ p >= 15 /\ 14 >= 0 /\ p - 15 >= 0 /\ p + 11 >= 0 /\ p >= 16 /\ 15 >= 0 /\ p - 16 >= 0 /\ p + 12 >= 0 /\ p >= 17 /\ 16 >= 0 ] (?, 1) f1(a, b) -> f1(a, b + 1) [ a - b >= 0 /\ b - 2 >= 0 /\ a + b - 4 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ b >= 0 ] start location: f3 leaf cost: 3 Complexity upper bound ? Time: 0.859 sec (SMT: 0.745 sec)