MAYBE Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d) -> f1(a, b, c, d) (?, 1) f1(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c, d) -> f1(a, b, c, d) with all transitions in problem 1, the following new transitions are obtained: f0(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] f0(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] We thus obtain the following problem: 2: T: (1, 2) f0(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] (1, 2) f0(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] with all transitions in problem 2, the following new transitions are obtained: f0(a, b, c, d) -> f1(a - 2, b, c, d) [ a >= 1 /\ a - 1 >= 1 ] f0(a, b, c, d) -> f1(a + b - 1, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 ] We thus obtain the following problem: 3: T: (1, 3) f0(a, b, c, d) -> f1(a - 2, b, c, d) [ a >= 1 /\ a - 1 >= 1 ] (1, 3) f0(a, b, c, d) -> f1(a + b - 1, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 ] (1, 2) f0(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c, d) -> f1(a - 2, b, c, d) [ a >= 1 /\ a - 1 >= 1 ] with all transitions in problem 3, the following new transitions are obtained: f0(a, b, c, d) -> f1(a - 3, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] f0(a, b, c, d) -> f1(a + b - 2, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] We thus obtain the following problem: 4: T: (1, 4) f0(a, b, c, d) -> f1(a - 3, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] (1, 4) f0(a, b, c, d) -> f1(a + b - 2, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] (1, 3) f0(a, b, c, d) -> f1(a + b - 1, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 ] (1, 2) f0(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c, d) -> f1(a - 3, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] with all transitions in problem 4, the following new transitions are obtained: f0(a, b, c, d) -> f1(a - 4, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 ] f0(a, b, c, d) -> f1(a + b - 3, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 ] We thus obtain the following problem: 5: T: (1, 5) f0(a, b, c, d) -> f1(a - 4, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 ] (1, 5) f0(a, b, c, d) -> f1(a + b - 3, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 ] (1, 4) f0(a, b, c, d) -> f1(a + b - 2, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] (1, 3) f0(a, b, c, d) -> f1(a + b - 1, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 ] (1, 2) f0(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c, d) -> f1(a - 4, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 ] with all transitions in problem 5, the following new transitions are obtained: f0(a, b, c, d) -> f1(a - 5, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 ] f0(a, b, c, d) -> f1(a + b - 4, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 ] We thus obtain the following problem: 6: T: (1, 6) f0(a, b, c, d) -> f1(a - 5, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 ] (1, 6) f0(a, b, c, d) -> f1(a + b - 4, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 ] (1, 5) f0(a, b, c, d) -> f1(a + b - 3, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 ] (1, 4) f0(a, b, c, d) -> f1(a + b - 2, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] (1, 3) f0(a, b, c, d) -> f1(a + b - 1, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 ] (1, 2) f0(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c, d) -> f1(a - 5, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 ] with all transitions in problem 6, the following new transitions are obtained: f0(a, b, c, d) -> f1(a - 6, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 ] f0(a, b, c, d) -> f1(a + b - 5, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 ] We thus obtain the following problem: 7: T: (1, 7) f0(a, b, c, d) -> f1(a - 6, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 ] (1, 7) f0(a, b, c, d) -> f1(a + b - 5, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 ] (1, 6) f0(a, b, c, d) -> f1(a + b - 4, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 ] (1, 5) f0(a, b, c, d) -> f1(a + b - 3, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 ] (1, 4) f0(a, b, c, d) -> f1(a + b - 2, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] (1, 3) f0(a, b, c, d) -> f1(a + b - 1, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 ] (1, 2) f0(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c, d) -> f1(a - 6, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 ] with all transitions in problem 7, the following new transitions are obtained: f0(a, b, c, d) -> f1(a - 7, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 ] f0(a, b, c, d) -> f1(a + b - 6, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 ] We thus obtain the following problem: 8: T: (1, 8) f0(a, b, c, d) -> f1(a - 7, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 ] (1, 8) f0(a, b, c, d) -> f1(a + b - 6, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 ] (1, 7) f0(a, b, c, d) -> f1(a + b - 5, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 ] (1, 6) f0(a, b, c, d) -> f1(a + b - 4, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 ] (1, 5) f0(a, b, c, d) -> f1(a + b - 3, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 ] (1, 4) f0(a, b, c, d) -> f1(a + b - 2, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] (1, 3) f0(a, b, c, d) -> f1(a + b - 1, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 ] (1, 2) f0(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c, d) -> f1(a - 7, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 ] with all transitions in problem 8, the following new transitions are obtained: f0(a, b, c, d) -> f1(a - 8, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 ] f0(a, b, c, d) -> f1(a + b - 7, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 ] We thus obtain the following problem: 9: T: (1, 9) f0(a, b, c, d) -> f1(a - 8, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 ] (1, 9) f0(a, b, c, d) -> f1(a + b - 7, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 ] (1, 8) f0(a, b, c, d) -> f1(a + b - 6, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 ] (1, 7) f0(a, b, c, d) -> f1(a + b - 5, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 ] (1, 6) f0(a, b, c, d) -> f1(a + b - 4, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 ] (1, 5) f0(a, b, c, d) -> f1(a + b - 3, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 ] (1, 4) f0(a, b, c, d) -> f1(a + b - 2, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] (1, 3) f0(a, b, c, d) -> f1(a + b - 1, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 ] (1, 2) f0(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c, d) -> f1(a - 8, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 ] with all transitions in problem 9, the following new transitions are obtained: f0(a, b, c, d) -> f1(a - 9, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 ] f0(a, b, c, d) -> f1(a + b - 8, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 ] We thus obtain the following problem: 10: T: (1, 10) f0(a, b, c, d) -> f1(a - 9, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 ] (1, 10) f0(a, b, c, d) -> f1(a + b - 8, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 ] (1, 9) f0(a, b, c, d) -> f1(a + b - 7, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 ] (1, 8) f0(a, b, c, d) -> f1(a + b - 6, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 ] (1, 7) f0(a, b, c, d) -> f1(a + b - 5, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 ] (1, 6) f0(a, b, c, d) -> f1(a + b - 4, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 ] (1, 5) f0(a, b, c, d) -> f1(a + b - 3, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 ] (1, 4) f0(a, b, c, d) -> f1(a + b - 2, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] (1, 3) f0(a, b, c, d) -> f1(a + b - 1, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 ] (1, 2) f0(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c, d) -> f1(a - 9, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 ] with all transitions in problem 10, the following new transitions are obtained: f0(a, b, c, d) -> f1(a - 10, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 ] f0(a, b, c, d) -> f1(a + b - 9, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 ] We thus obtain the following problem: 11: T: (1, 11) f0(a, b, c, d) -> f1(a - 10, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 ] (1, 11) f0(a, b, c, d) -> f1(a + b - 9, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 ] (1, 10) f0(a, b, c, d) -> f1(a + b - 8, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 ] (1, 9) f0(a, b, c, d) -> f1(a + b - 7, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 ] (1, 8) f0(a, b, c, d) -> f1(a + b - 6, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 ] (1, 7) f0(a, b, c, d) -> f1(a + b - 5, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 ] (1, 6) f0(a, b, c, d) -> f1(a + b - 4, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 ] (1, 5) f0(a, b, c, d) -> f1(a + b - 3, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 ] (1, 4) f0(a, b, c, d) -> f1(a + b - 2, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] (1, 3) f0(a, b, c, d) -> f1(a + b - 1, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 ] (1, 2) f0(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c, d) -> f1(a - 10, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 ] with all transitions in problem 11, the following new transitions are obtained: f0(a, b, c, d) -> f1(a - 11, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 ] f0(a, b, c, d) -> f1(a + b - 10, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 ] We thus obtain the following problem: 12: T: (1, 12) f0(a, b, c, d) -> f1(a - 11, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 ] (1, 12) f0(a, b, c, d) -> f1(a + b - 10, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 ] (1, 11) f0(a, b, c, d) -> f1(a + b - 9, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 ] (1, 10) f0(a, b, c, d) -> f1(a + b - 8, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 ] (1, 9) f0(a, b, c, d) -> f1(a + b - 7, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 ] (1, 8) f0(a, b, c, d) -> f1(a + b - 6, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 ] (1, 7) f0(a, b, c, d) -> f1(a + b - 5, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 ] (1, 6) f0(a, b, c, d) -> f1(a + b - 4, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 ] (1, 5) f0(a, b, c, d) -> f1(a + b - 3, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 ] (1, 4) f0(a, b, c, d) -> f1(a + b - 2, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] (1, 3) f0(a, b, c, d) -> f1(a + b - 1, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 ] (1, 2) f0(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c, d) -> f1(a - 11, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 ] with all transitions in problem 12, the following new transitions are obtained: f0(a, b, c, d) -> f1(a - 12, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 ] f0(a, b, c, d) -> f1(a + b - 11, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 ] We thus obtain the following problem: 13: T: (1, 13) f0(a, b, c, d) -> f1(a - 12, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 ] (1, 13) f0(a, b, c, d) -> f1(a + b - 11, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 ] (1, 12) f0(a, b, c, d) -> f1(a + b - 10, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 ] (1, 11) f0(a, b, c, d) -> f1(a + b - 9, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 ] (1, 10) f0(a, b, c, d) -> f1(a + b - 8, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 ] (1, 9) f0(a, b, c, d) -> f1(a + b - 7, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 ] (1, 8) f0(a, b, c, d) -> f1(a + b - 6, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 ] (1, 7) f0(a, b, c, d) -> f1(a + b - 5, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 ] (1, 6) f0(a, b, c, d) -> f1(a + b - 4, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 ] (1, 5) f0(a, b, c, d) -> f1(a + b - 3, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 ] (1, 4) f0(a, b, c, d) -> f1(a + b - 2, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] (1, 3) f0(a, b, c, d) -> f1(a + b - 1, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 ] (1, 2) f0(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c, d) -> f1(a - 12, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 ] with all transitions in problem 13, the following new transitions are obtained: f0(a, b, c, d) -> f1(a - 13, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 ] f0(a, b, c, d) -> f1(a + b - 12, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 ] We thus obtain the following problem: 14: T: (1, 14) f0(a, b, c, d) -> f1(a - 13, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 ] (1, 14) f0(a, b, c, d) -> f1(a + b - 12, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 ] (1, 13) f0(a, b, c, d) -> f1(a + b - 11, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 ] (1, 12) f0(a, b, c, d) -> f1(a + b - 10, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 ] (1, 11) f0(a, b, c, d) -> f1(a + b - 9, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 ] (1, 10) f0(a, b, c, d) -> f1(a + b - 8, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 ] (1, 9) f0(a, b, c, d) -> f1(a + b - 7, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 ] (1, 8) f0(a, b, c, d) -> f1(a + b - 6, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 ] (1, 7) f0(a, b, c, d) -> f1(a + b - 5, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 ] (1, 6) f0(a, b, c, d) -> f1(a + b - 4, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 ] (1, 5) f0(a, b, c, d) -> f1(a + b - 3, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 ] (1, 4) f0(a, b, c, d) -> f1(a + b - 2, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] (1, 3) f0(a, b, c, d) -> f1(a + b - 1, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 ] (1, 2) f0(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c, d) -> f1(a - 13, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 ] with all transitions in problem 14, the following new transitions are obtained: f0(a, b, c, d) -> f1(a - 14, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 /\ a - 13 >= 1 ] f0(a, b, c, d) -> f1(a + b - 13, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 /\ a - 13 >= 1 ] We thus obtain the following problem: 15: T: (1, 15) f0(a, b, c, d) -> f1(a - 14, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 /\ a - 13 >= 1 ] (1, 15) f0(a, b, c, d) -> f1(a + b - 13, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 /\ a - 13 >= 1 ] (1, 14) f0(a, b, c, d) -> f1(a + b - 12, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 ] (1, 13) f0(a, b, c, d) -> f1(a + b - 11, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 ] (1, 12) f0(a, b, c, d) -> f1(a + b - 10, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 ] (1, 11) f0(a, b, c, d) -> f1(a + b - 9, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 ] (1, 10) f0(a, b, c, d) -> f1(a + b - 8, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 ] (1, 9) f0(a, b, c, d) -> f1(a + b - 7, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 ] (1, 8) f0(a, b, c, d) -> f1(a + b - 6, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 ] (1, 7) f0(a, b, c, d) -> f1(a + b - 5, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 ] (1, 6) f0(a, b, c, d) -> f1(a + b - 4, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 ] (1, 5) f0(a, b, c, d) -> f1(a + b - 3, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 ] (1, 4) f0(a, b, c, d) -> f1(a + b - 2, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] (1, 3) f0(a, b, c, d) -> f1(a + b - 1, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 ] (1, 2) f0(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c, d) -> f1(a - 14, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 /\ a - 13 >= 1 ] with all transitions in problem 15, the following new transitions are obtained: f0(a, b, c, d) -> f1(a - 15, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 /\ a - 13 >= 1 /\ a - 14 >= 1 ] f0(a, b, c, d) -> f1(a + b - 14, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 /\ a - 13 >= 1 /\ a - 14 >= 1 ] We thus obtain the following problem: 16: T: (1, 16) f0(a, b, c, d) -> f1(a - 15, b, c, d) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 /\ a - 13 >= 1 /\ a - 14 >= 1 ] (1, 16) f0(a, b, c, d) -> f1(a + b - 14, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 /\ a - 13 >= 1 /\ a - 14 >= 1 ] (1, 15) f0(a, b, c, d) -> f1(a + b - 13, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 /\ a - 13 >= 1 ] (1, 14) f0(a, b, c, d) -> f1(a + b - 12, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 /\ a - 12 >= 1 ] (1, 13) f0(a, b, c, d) -> f1(a + b - 11, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 /\ a - 11 >= 1 ] (1, 12) f0(a, b, c, d) -> f1(a + b - 10, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 /\ a - 10 >= 1 ] (1, 11) f0(a, b, c, d) -> f1(a + b - 9, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 /\ a - 9 >= 1 ] (1, 10) f0(a, b, c, d) -> f1(a + b - 8, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 /\ a - 8 >= 1 ] (1, 9) f0(a, b, c, d) -> f1(a + b - 7, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 /\ a - 7 >= 1 ] (1, 8) f0(a, b, c, d) -> f1(a + b - 6, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 /\ a - 6 >= 1 ] (1, 7) f0(a, b, c, d) -> f1(a + b - 5, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 /\ a - 5 >= 1 ] (1, 6) f0(a, b, c, d) -> f1(a + b - 4, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 /\ a - 4 >= 1 ] (1, 5) f0(a, b, c, d) -> f1(a + b - 3, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 /\ a - 3 >= 1 ] (1, 4) f0(a, b, c, d) -> f1(a + b - 2, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 /\ a - 2 >= 1 ] (1, 3) f0(a, b, c, d) -> f1(a + b - 1, b + c, c + d, d - 1) [ a >= 1 /\ a - 1 >= 1 ] (1, 2) f0(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a + b, b + c, c + d, d - 1) [ a >= 1 ] (?, 1) f1(a, b, c, d) -> f1(a - 1, b, c, d) [ a >= 1 ] start location: f0 leaf cost: 0 Complexity upper bound ? Time: 6.382 sec (SMT: 6.050 sec)