MAYBE Initial complexity problem: 1: T: (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ b >= c + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ c >= b + 1 ] (?, 1) f3(a, b, c) -> f2(a, b, 0) [ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 ] (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a >= c /\ c + 1 >= 0 ] start location: f1 leaf cost: 0 Applied AI with 'oct' on problem 1 to obtain the following invariants: For symbol f2: X_1 - X_3 + 1 >= 0 /\ X_1 - X_2 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 1 >= 0 For symbol f3: X_1 - X_3 + 1 >= 0 /\ X_1 - X_2 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 1 >= 0 This yielded the following problem: 2: T: (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c /\ c + 1 >= 0 ] (?, 1) f3(a, b, c) -> f2(a, b, 0) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= b + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= c + 1 ] (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] start location: f1 leaf cost: 0 By chaining the transition f3(a, b, c) -> f2(a, b, 0) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 ] with all transitions in problem 2, the following new transition is obtained: f3(a, b, c) -> f3(a, b, 0) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 ] We thus obtain the following problem: 3: T: (?, 2) f3(a, b, c) -> f3(a, b, 0) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 ] (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c /\ c + 1 >= 0 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= b + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= c + 1 ] (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] start location: f1 leaf cost: 0 By chaining the transition f3(a, b, c) -> f3(a, b, 0) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 ] with all transitions in problem 3, the following new transition is obtained: f3(a, b, c) -> f2(a, b, 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 ] We thus obtain the following problem: 4: T: (?, 3) f3(a, b, c) -> f2(a, b, 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 ] (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c /\ c + 1 >= 0 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= b + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= c + 1 ] (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] start location: f1 leaf cost: 0 By chaining the transition f3(a, b, c) -> f2(a, b, 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 ] with all transitions in problem 4, the following new transition is obtained: f3(a, b, c) -> f3(a, b, 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 ] We thus obtain the following problem: 5: T: (?, 4) f3(a, b, c) -> f3(a, b, 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 ] (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c /\ c + 1 >= 0 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= b + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= c + 1 ] (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] start location: f1 leaf cost: 0 By chaining the transition f3(a, b, c) -> f3(a, b, 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 ] with all transitions in problem 5, the following new transition is obtained: f3(a, b, c) -> f2(a, b, 2) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 ] We thus obtain the following problem: 6: T: (?, 5) f3(a, b, c) -> f2(a, b, 2) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 ] (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c /\ c + 1 >= 0 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= b + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= c + 1 ] (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] start location: f1 leaf cost: 0 By chaining the transition f3(a, b, c) -> f2(a, b, 2) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 ] with all transitions in problem 6, the following new transition is obtained: f3(a, b, c) -> f3(a, b, 2) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 ] We thus obtain the following problem: 7: T: (?, 6) f3(a, b, c) -> f3(a, b, 2) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 ] (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c /\ c + 1 >= 0 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= b + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= c + 1 ] (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] start location: f1 leaf cost: 0 By chaining the transition f3(a, b, c) -> f3(a, b, 2) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 ] with all transitions in problem 7, the following new transition is obtained: f3(a, b, c) -> f2(a, b, 3) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 ] We thus obtain the following problem: 8: T: (?, 7) f3(a, b, c) -> f2(a, b, 3) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 ] (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c /\ c + 1 >= 0 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= b + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= c + 1 ] (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] start location: f1 leaf cost: 0 By chaining the transition f3(a, b, c) -> f2(a, b, 3) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 ] with all transitions in problem 8, the following new transition is obtained: f3(a, b, c) -> f3(a, b, 3) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 ] We thus obtain the following problem: 9: T: (?, 8) f3(a, b, c) -> f3(a, b, 3) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 ] (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c /\ c + 1 >= 0 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= b + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= c + 1 ] (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] start location: f1 leaf cost: 0 By chaining the transition f3(a, b, c) -> f3(a, b, 3) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 ] with all transitions in problem 9, the following new transition is obtained: f3(a, b, c) -> f2(a, b, 4) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 ] We thus obtain the following problem: 10: T: (?, 9) f3(a, b, c) -> f2(a, b, 4) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 ] (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c /\ c + 1 >= 0 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= b + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= c + 1 ] (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] start location: f1 leaf cost: 0 By chaining the transition f3(a, b, c) -> f2(a, b, 4) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 ] with all transitions in problem 10, the following new transition is obtained: f3(a, b, c) -> f3(a, b, 4) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 ] We thus obtain the following problem: 11: T: (?, 10) f3(a, b, c) -> f3(a, b, 4) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 ] (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c /\ c + 1 >= 0 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= b + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= c + 1 ] (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] start location: f1 leaf cost: 0 By chaining the transition f3(a, b, c) -> f3(a, b, 4) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 ] with all transitions in problem 11, the following new transition is obtained: f3(a, b, c) -> f2(a, b, 5) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 ] We thus obtain the following problem: 12: T: (?, 11) f3(a, b, c) -> f2(a, b, 5) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 ] (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c /\ c + 1 >= 0 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= b + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= c + 1 ] (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] start location: f1 leaf cost: 0 By chaining the transition f3(a, b, c) -> f2(a, b, 5) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 ] with all transitions in problem 12, the following new transition is obtained: f3(a, b, c) -> f3(a, b, 5) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 /\ a - 4 >= 0 /\ b >= 6 ] We thus obtain the following problem: 13: T: (?, 12) f3(a, b, c) -> f3(a, b, 5) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 /\ a - 4 >= 0 /\ b >= 6 ] (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c /\ c + 1 >= 0 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= b + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= c + 1 ] (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] start location: f1 leaf cost: 0 By chaining the transition f3(a, b, c) -> f3(a, b, 5) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 /\ a - 4 >= 0 /\ b >= 6 ] with all transitions in problem 13, the following new transition is obtained: f3(a, b, c) -> f2(a, b, 6) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 /\ a - 4 >= 0 /\ b >= 6 /\ a >= 5 /\ 6 >= 0 ] We thus obtain the following problem: 14: T: (?, 13) f3(a, b, c) -> f2(a, b, 6) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 /\ a - 4 >= 0 /\ b >= 6 /\ a >= 5 /\ 6 >= 0 ] (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c /\ c + 1 >= 0 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= b + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= c + 1 ] (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] start location: f1 leaf cost: 0 By chaining the transition f3(a, b, c) -> f2(a, b, 6) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 /\ a - 4 >= 0 /\ b >= 6 /\ a >= 5 /\ 6 >= 0 ] with all transitions in problem 14, the following new transition is obtained: f3(a, b, c) -> f3(a, b, 6) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 /\ a - 4 >= 0 /\ b >= 6 /\ a >= 5 /\ 6 >= 0 /\ a - 5 >= 0 /\ b >= 7 ] We thus obtain the following problem: 15: T: (?, 14) f3(a, b, c) -> f3(a, b, 6) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 /\ a - 4 >= 0 /\ b >= 6 /\ a >= 5 /\ 6 >= 0 /\ a - 5 >= 0 /\ b >= 7 ] (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c /\ c + 1 >= 0 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= b + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= c + 1 ] (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] start location: f1 leaf cost: 0 By chaining the transition f3(a, b, c) -> f3(a, b, 6) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 /\ a - 4 >= 0 /\ b >= 6 /\ a >= 5 /\ 6 >= 0 /\ a - 5 >= 0 /\ b >= 7 ] with all transitions in problem 15, the following new transition is obtained: f3(a, b, c) -> f2(a, b, 7) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 /\ a - 4 >= 0 /\ b >= 6 /\ a >= 5 /\ 6 >= 0 /\ a - 5 >= 0 /\ b >= 7 /\ a >= 6 /\ 7 >= 0 ] We thus obtain the following problem: 16: T: (?, 15) f3(a, b, c) -> f2(a, b, 7) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 /\ a - 4 >= 0 /\ b >= 6 /\ a >= 5 /\ 6 >= 0 /\ a - 5 >= 0 /\ b >= 7 /\ a >= 6 /\ 7 >= 0 ] (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c /\ c + 1 >= 0 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= b + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= c + 1 ] (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] start location: f1 leaf cost: 0 By chaining the transition f3(a, b, c) -> f2(a, b, 7) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 /\ a - 4 >= 0 /\ b >= 6 /\ a >= 5 /\ 6 >= 0 /\ a - 5 >= 0 /\ b >= 7 /\ a >= 6 /\ 7 >= 0 ] with all transitions in problem 16, the following new transition is obtained: f3(a, b, c) -> f3(a, b, 7) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 /\ a - 4 >= 0 /\ b >= 6 /\ a >= 5 /\ 6 >= 0 /\ a - 5 >= 0 /\ b >= 7 /\ a >= 6 /\ 7 >= 0 /\ a - 6 >= 0 /\ b >= 8 ] We thus obtain the following problem: 17: T: (?, 16) f3(a, b, c) -> f3(a, b, 7) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 /\ c >= a + 1 /\ b >= 1 /\ a >= 0 /\ 1 >= 0 /\ b >= 2 /\ a >= 1 /\ 2 >= 0 /\ b >= 3 /\ a >= 2 /\ 3 >= 0 /\ a - 2 >= 0 /\ b >= 4 /\ a >= 3 /\ 4 >= 0 /\ a - 3 >= 0 /\ b >= 5 /\ a >= 4 /\ 5 >= 0 /\ a - 4 >= 0 /\ b >= 6 /\ a >= 5 /\ 6 >= 0 /\ a - 5 >= 0 /\ b >= 7 /\ a >= 6 /\ 7 >= 0 /\ a - 6 >= 0 /\ b >= 8 ] (?, 1) f3(a, b, c) -> f2(a, b, c + 1) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c /\ c + 1 >= 0 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= b + 1 ] (?, 1) f2(a, b, c) -> f3(a, b, c) [ a - c + 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= c + 1 ] (1, 1) f1(a, b, c) -> f2(a, b, b + 1) [ a >= b /\ a >= 1 /\ b >= 1 ] start location: f1 leaf cost: 0 Complexity upper bound ? Time: 1.482 sec (SMT: 1.305 sec)