MAYBE Initial complexity problem: 1: T: (1, 1) f0(a, b, c) -> f1(a, b, c) (?, 1) f1(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a, b, c) with all transitions in problem 1, the following new transitions are obtained: f0(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] f0(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] We thus obtain the following problem: 2: T: (1, 2) f0(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] (1, 2) f0(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] with all transitions in problem 2, the following new transitions are obtained: f0(a, b, c) -> f1(a - 2*c + 1, b - 4*c + 2, c - 2) [ a >= b /\ a - c >= b - 2*c ] f0(a, b, c) -> f1(a - c + 1, b - 3*c + a + 1, c - 1) [ a >= b /\ a - c >= b - 2*c ] We thus obtain the following problem: 3: T: (1, 3) f0(a, b, c) -> f1(a - 2*c + 1, b - 4*c + 2, c - 2) [ a >= b /\ a - c >= b - 2*c ] (1, 3) f0(a, b, c) -> f1(a - c + 1, b - 3*c + a + 1, c - 1) [ a >= b /\ a - c >= b - 2*c ] (1, 2) f0(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a - 2*c + 1, b - 4*c + 2, c - 2) [ a >= b /\ a - c >= b - 2*c ] with all transitions in problem 3, the following new transitions are obtained: f0(a, b, c) -> f1(a - 3*c + 3, b - 6*c + 6, c - 3) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] f0(a, b, c) -> f1(a - 2*c + 2, b - 6*c + a + 4, c - 2) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] We thus obtain the following problem: 4: T: (1, 4) f0(a, b, c) -> f1(a - 3*c + 3, b - 6*c + 6, c - 3) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] (1, 4) f0(a, b, c) -> f1(a - 2*c + 2, b - 6*c + a + 4, c - 2) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] (1, 3) f0(a, b, c) -> f1(a - c + 1, b - 3*c + a + 1, c - 1) [ a >= b /\ a - c >= b - 2*c ] (1, 2) f0(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a - 3*c + 3, b - 6*c + 6, c - 3) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] with all transitions in problem 4, the following new transitions are obtained: f0(a, b, c) -> f1(a - 4*c + 6, b - 8*c + 12, c - 4) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 ] f0(a, b, c) -> f1(a - 3*c + 4, b - 9*c + a + 10, c - 3) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 ] We thus obtain the following problem: 5: T: (1, 5) f0(a, b, c) -> f1(a - 4*c + 6, b - 8*c + 12, c - 4) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 ] (1, 5) f0(a, b, c) -> f1(a - 3*c + 4, b - 9*c + a + 10, c - 3) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 ] (1, 4) f0(a, b, c) -> f1(a - 2*c + 2, b - 6*c + a + 4, c - 2) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] (1, 3) f0(a, b, c) -> f1(a - c + 1, b - 3*c + a + 1, c - 1) [ a >= b /\ a - c >= b - 2*c ] (1, 2) f0(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a - 4*c + 6, b - 8*c + 12, c - 4) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 ] with all transitions in problem 5, the following new transitions are obtained: f0(a, b, c) -> f1(a - 5*c + 10, b - 10*c + 20, c - 5) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 ] f0(a, b, c) -> f1(a - 4*c + 7, b - 12*c + a + 19, c - 4) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 ] We thus obtain the following problem: 6: T: (1, 6) f0(a, b, c) -> f1(a - 5*c + 10, b - 10*c + 20, c - 5) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 ] (1, 6) f0(a, b, c) -> f1(a - 4*c + 7, b - 12*c + a + 19, c - 4) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 ] (1, 5) f0(a, b, c) -> f1(a - 3*c + 4, b - 9*c + a + 10, c - 3) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 ] (1, 4) f0(a, b, c) -> f1(a - 2*c + 2, b - 6*c + a + 4, c - 2) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] (1, 3) f0(a, b, c) -> f1(a - c + 1, b - 3*c + a + 1, c - 1) [ a >= b /\ a - c >= b - 2*c ] (1, 2) f0(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a - 5*c + 10, b - 10*c + 20, c - 5) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 ] with all transitions in problem 6, the following new transitions are obtained: f0(a, b, c) -> f1(a - 6*c + 15, b - 12*c + 30, c - 6) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 ] f0(a, b, c) -> f1(a - 5*c + 11, b - 15*c + a + 31, c - 5) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 ] We thus obtain the following problem: 7: T: (1, 7) f0(a, b, c) -> f1(a - 6*c + 15, b - 12*c + 30, c - 6) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 ] (1, 7) f0(a, b, c) -> f1(a - 5*c + 11, b - 15*c + a + 31, c - 5) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 ] (1, 6) f0(a, b, c) -> f1(a - 4*c + 7, b - 12*c + a + 19, c - 4) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 ] (1, 5) f0(a, b, c) -> f1(a - 3*c + 4, b - 9*c + a + 10, c - 3) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 ] (1, 4) f0(a, b, c) -> f1(a - 2*c + 2, b - 6*c + a + 4, c - 2) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] (1, 3) f0(a, b, c) -> f1(a - c + 1, b - 3*c + a + 1, c - 1) [ a >= b /\ a - c >= b - 2*c ] (1, 2) f0(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a - 6*c + 15, b - 12*c + 30, c - 6) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 ] with all transitions in problem 7, the following new transitions are obtained: f0(a, b, c) -> f1(a - 7*c + 21, b - 14*c + 42, c - 7) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 ] f0(a, b, c) -> f1(a - 6*c + 16, b - 18*c + a + 46, c - 6) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 ] We thus obtain the following problem: 8: T: (1, 8) f0(a, b, c) -> f1(a - 7*c + 21, b - 14*c + 42, c - 7) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 ] (1, 8) f0(a, b, c) -> f1(a - 6*c + 16, b - 18*c + a + 46, c - 6) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 ] (1, 7) f0(a, b, c) -> f1(a - 5*c + 11, b - 15*c + a + 31, c - 5) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 ] (1, 6) f0(a, b, c) -> f1(a - 4*c + 7, b - 12*c + a + 19, c - 4) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 ] (1, 5) f0(a, b, c) -> f1(a - 3*c + 4, b - 9*c + a + 10, c - 3) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 ] (1, 4) f0(a, b, c) -> f1(a - 2*c + 2, b - 6*c + a + 4, c - 2) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] (1, 3) f0(a, b, c) -> f1(a - c + 1, b - 3*c + a + 1, c - 1) [ a >= b /\ a - c >= b - 2*c ] (1, 2) f0(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a - 7*c + 21, b - 14*c + 42, c - 7) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 ] with all transitions in problem 8, the following new transitions are obtained: f0(a, b, c) -> f1(a - 8*c + 28, b - 16*c + 56, c - 8) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 ] f0(a, b, c) -> f1(a - 7*c + 22, b - 21*c + a + 64, c - 7) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 ] We thus obtain the following problem: 9: T: (1, 9) f0(a, b, c) -> f1(a - 8*c + 28, b - 16*c + 56, c - 8) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 ] (1, 9) f0(a, b, c) -> f1(a - 7*c + 22, b - 21*c + a + 64, c - 7) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 ] (1, 8) f0(a, b, c) -> f1(a - 6*c + 16, b - 18*c + a + 46, c - 6) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 ] (1, 7) f0(a, b, c) -> f1(a - 5*c + 11, b - 15*c + a + 31, c - 5) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 ] (1, 6) f0(a, b, c) -> f1(a - 4*c + 7, b - 12*c + a + 19, c - 4) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 ] (1, 5) f0(a, b, c) -> f1(a - 3*c + 4, b - 9*c + a + 10, c - 3) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 ] (1, 4) f0(a, b, c) -> f1(a - 2*c + 2, b - 6*c + a + 4, c - 2) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] (1, 3) f0(a, b, c) -> f1(a - c + 1, b - 3*c + a + 1, c - 1) [ a >= b /\ a - c >= b - 2*c ] (1, 2) f0(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a - 8*c + 28, b - 16*c + 56, c - 8) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 ] with all transitions in problem 9, the following new transitions are obtained: f0(a, b, c) -> f1(a - 9*c + 36, b - 18*c + 72, c - 9) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 ] f0(a, b, c) -> f1(a - 8*c + 29, b - 24*c + a + 85, c - 8) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 ] We thus obtain the following problem: 10: T: (1, 10) f0(a, b, c) -> f1(a - 9*c + 36, b - 18*c + 72, c - 9) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 ] (1, 10) f0(a, b, c) -> f1(a - 8*c + 29, b - 24*c + a + 85, c - 8) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 ] (1, 9) f0(a, b, c) -> f1(a - 7*c + 22, b - 21*c + a + 64, c - 7) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 ] (1, 8) f0(a, b, c) -> f1(a - 6*c + 16, b - 18*c + a + 46, c - 6) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 ] (1, 7) f0(a, b, c) -> f1(a - 5*c + 11, b - 15*c + a + 31, c - 5) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 ] (1, 6) f0(a, b, c) -> f1(a - 4*c + 7, b - 12*c + a + 19, c - 4) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 ] (1, 5) f0(a, b, c) -> f1(a - 3*c + 4, b - 9*c + a + 10, c - 3) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 ] (1, 4) f0(a, b, c) -> f1(a - 2*c + 2, b - 6*c + a + 4, c - 2) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] (1, 3) f0(a, b, c) -> f1(a - c + 1, b - 3*c + a + 1, c - 1) [ a >= b /\ a - c >= b - 2*c ] (1, 2) f0(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a - 9*c + 36, b - 18*c + 72, c - 9) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 ] with all transitions in problem 10, the following new transitions are obtained: f0(a, b, c) -> f1(a - 10*c + 45, b - 20*c + 90, c - 10) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 ] f0(a, b, c) -> f1(a - 9*c + 37, b - 27*c + a + 109, c - 9) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 ] We thus obtain the following problem: 11: T: (1, 11) f0(a, b, c) -> f1(a - 10*c + 45, b - 20*c + 90, c - 10) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 ] (1, 11) f0(a, b, c) -> f1(a - 9*c + 37, b - 27*c + a + 109, c - 9) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 ] (1, 10) f0(a, b, c) -> f1(a - 8*c + 29, b - 24*c + a + 85, c - 8) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 ] (1, 9) f0(a, b, c) -> f1(a - 7*c + 22, b - 21*c + a + 64, c - 7) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 ] (1, 8) f0(a, b, c) -> f1(a - 6*c + 16, b - 18*c + a + 46, c - 6) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 ] (1, 7) f0(a, b, c) -> f1(a - 5*c + 11, b - 15*c + a + 31, c - 5) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 ] (1, 6) f0(a, b, c) -> f1(a - 4*c + 7, b - 12*c + a + 19, c - 4) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 ] (1, 5) f0(a, b, c) -> f1(a - 3*c + 4, b - 9*c + a + 10, c - 3) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 ] (1, 4) f0(a, b, c) -> f1(a - 2*c + 2, b - 6*c + a + 4, c - 2) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] (1, 3) f0(a, b, c) -> f1(a - c + 1, b - 3*c + a + 1, c - 1) [ a >= b /\ a - c >= b - 2*c ] (1, 2) f0(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a - 10*c + 45, b - 20*c + 90, c - 10) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 ] with all transitions in problem 11, the following new transitions are obtained: f0(a, b, c) -> f1(a - 11*c + 55, b - 22*c + 110, c - 11) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 ] f0(a, b, c) -> f1(a - 10*c + 46, b - 30*c + a + 136, c - 10) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 ] We thus obtain the following problem: 12: T: (1, 12) f0(a, b, c) -> f1(a - 11*c + 55, b - 22*c + 110, c - 11) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 ] (1, 12) f0(a, b, c) -> f1(a - 10*c + 46, b - 30*c + a + 136, c - 10) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 ] (1, 11) f0(a, b, c) -> f1(a - 9*c + 37, b - 27*c + a + 109, c - 9) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 ] (1, 10) f0(a, b, c) -> f1(a - 8*c + 29, b - 24*c + a + 85, c - 8) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 ] (1, 9) f0(a, b, c) -> f1(a - 7*c + 22, b - 21*c + a + 64, c - 7) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 ] (1, 8) f0(a, b, c) -> f1(a - 6*c + 16, b - 18*c + a + 46, c - 6) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 ] (1, 7) f0(a, b, c) -> f1(a - 5*c + 11, b - 15*c + a + 31, c - 5) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 ] (1, 6) f0(a, b, c) -> f1(a - 4*c + 7, b - 12*c + a + 19, c - 4) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 ] (1, 5) f0(a, b, c) -> f1(a - 3*c + 4, b - 9*c + a + 10, c - 3) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 ] (1, 4) f0(a, b, c) -> f1(a - 2*c + 2, b - 6*c + a + 4, c - 2) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] (1, 3) f0(a, b, c) -> f1(a - c + 1, b - 3*c + a + 1, c - 1) [ a >= b /\ a - c >= b - 2*c ] (1, 2) f0(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a - 11*c + 55, b - 22*c + 110, c - 11) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 ] with all transitions in problem 12, the following new transitions are obtained: f0(a, b, c) -> f1(a - 12*c + 66, b - 24*c + 132, c - 12) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 ] f0(a, b, c) -> f1(a - 11*c + 56, b - 33*c + a + 166, c - 11) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 ] We thus obtain the following problem: 13: T: (1, 13) f0(a, b, c) -> f1(a - 12*c + 66, b - 24*c + 132, c - 12) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 ] (1, 13) f0(a, b, c) -> f1(a - 11*c + 56, b - 33*c + a + 166, c - 11) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 ] (1, 12) f0(a, b, c) -> f1(a - 10*c + 46, b - 30*c + a + 136, c - 10) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 ] (1, 11) f0(a, b, c) -> f1(a - 9*c + 37, b - 27*c + a + 109, c - 9) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 ] (1, 10) f0(a, b, c) -> f1(a - 8*c + 29, b - 24*c + a + 85, c - 8) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 ] (1, 9) f0(a, b, c) -> f1(a - 7*c + 22, b - 21*c + a + 64, c - 7) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 ] (1, 8) f0(a, b, c) -> f1(a - 6*c + 16, b - 18*c + a + 46, c - 6) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 ] (1, 7) f0(a, b, c) -> f1(a - 5*c + 11, b - 15*c + a + 31, c - 5) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 ] (1, 6) f0(a, b, c) -> f1(a - 4*c + 7, b - 12*c + a + 19, c - 4) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 ] (1, 5) f0(a, b, c) -> f1(a - 3*c + 4, b - 9*c + a + 10, c - 3) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 ] (1, 4) f0(a, b, c) -> f1(a - 2*c + 2, b - 6*c + a + 4, c - 2) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] (1, 3) f0(a, b, c) -> f1(a - c + 1, b - 3*c + a + 1, c - 1) [ a >= b /\ a - c >= b - 2*c ] (1, 2) f0(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a - 12*c + 66, b - 24*c + 132, c - 12) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 ] with all transitions in problem 13, the following new transitions are obtained: f0(a, b, c) -> f1(a - 13*c + 78, b - 26*c + 156, c - 13) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 ] f0(a, b, c) -> f1(a - 12*c + 67, b - 36*c + a + 199, c - 12) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 ] We thus obtain the following problem: 14: T: (1, 14) f0(a, b, c) -> f1(a - 13*c + 78, b - 26*c + 156, c - 13) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 ] (1, 14) f0(a, b, c) -> f1(a - 12*c + 67, b - 36*c + a + 199, c - 12) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 ] (1, 13) f0(a, b, c) -> f1(a - 11*c + 56, b - 33*c + a + 166, c - 11) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 ] (1, 12) f0(a, b, c) -> f1(a - 10*c + 46, b - 30*c + a + 136, c - 10) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 ] (1, 11) f0(a, b, c) -> f1(a - 9*c + 37, b - 27*c + a + 109, c - 9) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 ] (1, 10) f0(a, b, c) -> f1(a - 8*c + 29, b - 24*c + a + 85, c - 8) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 ] (1, 9) f0(a, b, c) -> f1(a - 7*c + 22, b - 21*c + a + 64, c - 7) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 ] (1, 8) f0(a, b, c) -> f1(a - 6*c + 16, b - 18*c + a + 46, c - 6) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 ] (1, 7) f0(a, b, c) -> f1(a - 5*c + 11, b - 15*c + a + 31, c - 5) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 ] (1, 6) f0(a, b, c) -> f1(a - 4*c + 7, b - 12*c + a + 19, c - 4) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 ] (1, 5) f0(a, b, c) -> f1(a - 3*c + 4, b - 9*c + a + 10, c - 3) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 ] (1, 4) f0(a, b, c) -> f1(a - 2*c + 2, b - 6*c + a + 4, c - 2) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] (1, 3) f0(a, b, c) -> f1(a - c + 1, b - 3*c + a + 1, c - 1) [ a >= b /\ a - c >= b - 2*c ] (1, 2) f0(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a - 13*c + 78, b - 26*c + 156, c - 13) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 ] with all transitions in problem 14, the following new transitions are obtained: f0(a, b, c) -> f1(a - 14*c + 91, b - 28*c + 182, c - 14) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 /\ a - 13*c + 78 >= b - 26*c + 156 ] f0(a, b, c) -> f1(a - 13*c + 79, b - 39*c + a + 235, c - 13) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 /\ a - 13*c + 78 >= b - 26*c + 156 ] We thus obtain the following problem: 15: T: (1, 15) f0(a, b, c) -> f1(a - 14*c + 91, b - 28*c + 182, c - 14) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 /\ a - 13*c + 78 >= b - 26*c + 156 ] (1, 15) f0(a, b, c) -> f1(a - 13*c + 79, b - 39*c + a + 235, c - 13) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 /\ a - 13*c + 78 >= b - 26*c + 156 ] (1, 14) f0(a, b, c) -> f1(a - 12*c + 67, b - 36*c + a + 199, c - 12) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 ] (1, 13) f0(a, b, c) -> f1(a - 11*c + 56, b - 33*c + a + 166, c - 11) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 ] (1, 12) f0(a, b, c) -> f1(a - 10*c + 46, b - 30*c + a + 136, c - 10) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 ] (1, 11) f0(a, b, c) -> f1(a - 9*c + 37, b - 27*c + a + 109, c - 9) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 ] (1, 10) f0(a, b, c) -> f1(a - 8*c + 29, b - 24*c + a + 85, c - 8) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 ] (1, 9) f0(a, b, c) -> f1(a - 7*c + 22, b - 21*c + a + 64, c - 7) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 ] (1, 8) f0(a, b, c) -> f1(a - 6*c + 16, b - 18*c + a + 46, c - 6) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 ] (1, 7) f0(a, b, c) -> f1(a - 5*c + 11, b - 15*c + a + 31, c - 5) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 ] (1, 6) f0(a, b, c) -> f1(a - 4*c + 7, b - 12*c + a + 19, c - 4) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 ] (1, 5) f0(a, b, c) -> f1(a - 3*c + 4, b - 9*c + a + 10, c - 3) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 ] (1, 4) f0(a, b, c) -> f1(a - 2*c + 2, b - 6*c + a + 4, c - 2) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] (1, 3) f0(a, b, c) -> f1(a - c + 1, b - 3*c + a + 1, c - 1) [ a >= b /\ a - c >= b - 2*c ] (1, 2) f0(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a - 14*c + 91, b - 28*c + 182, c - 14) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 /\ a - 13*c + 78 >= b - 26*c + 156 ] with all transitions in problem 15, the following new transitions are obtained: f0(a, b, c) -> f1(a - 15*c + 105, b - 30*c + 210, c - 15) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 /\ a - 13*c + 78 >= b - 26*c + 156 /\ a - 14*c + 91 >= b - 28*c + 182 ] f0(a, b, c) -> f1(a - 14*c + 92, b - 42*c + a + 274, c - 14) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 /\ a - 13*c + 78 >= b - 26*c + 156 /\ a - 14*c + 91 >= b - 28*c + 182 ] We thus obtain the following problem: 16: T: (1, 16) f0(a, b, c) -> f1(a - 15*c + 105, b - 30*c + 210, c - 15) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 /\ a - 13*c + 78 >= b - 26*c + 156 /\ a - 14*c + 91 >= b - 28*c + 182 ] (1, 16) f0(a, b, c) -> f1(a - 14*c + 92, b - 42*c + a + 274, c - 14) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 /\ a - 13*c + 78 >= b - 26*c + 156 /\ a - 14*c + 91 >= b - 28*c + 182 ] (1, 15) f0(a, b, c) -> f1(a - 13*c + 79, b - 39*c + a + 235, c - 13) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 /\ a - 13*c + 78 >= b - 26*c + 156 ] (1, 14) f0(a, b, c) -> f1(a - 12*c + 67, b - 36*c + a + 199, c - 12) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 /\ a - 12*c + 66 >= b - 24*c + 132 ] (1, 13) f0(a, b, c) -> f1(a - 11*c + 56, b - 33*c + a + 166, c - 11) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 /\ a - 11*c + 55 >= b - 22*c + 110 ] (1, 12) f0(a, b, c) -> f1(a - 10*c + 46, b - 30*c + a + 136, c - 10) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 /\ a - 10*c + 45 >= b - 20*c + 90 ] (1, 11) f0(a, b, c) -> f1(a - 9*c + 37, b - 27*c + a + 109, c - 9) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 /\ a - 9*c + 36 >= b - 18*c + 72 ] (1, 10) f0(a, b, c) -> f1(a - 8*c + 29, b - 24*c + a + 85, c - 8) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 /\ a - 8*c + 28 >= b - 16*c + 56 ] (1, 9) f0(a, b, c) -> f1(a - 7*c + 22, b - 21*c + a + 64, c - 7) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 /\ a - 7*c + 21 >= b - 14*c + 42 ] (1, 8) f0(a, b, c) -> f1(a - 6*c + 16, b - 18*c + a + 46, c - 6) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 /\ a - 6*c + 15 >= b - 12*c + 30 ] (1, 7) f0(a, b, c) -> f1(a - 5*c + 11, b - 15*c + a + 31, c - 5) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 /\ a - 5*c + 10 >= b - 10*c + 20 ] (1, 6) f0(a, b, c) -> f1(a - 4*c + 7, b - 12*c + a + 19, c - 4) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 /\ a - 4*c + 6 >= b - 8*c + 12 ] (1, 5) f0(a, b, c) -> f1(a - 3*c + 4, b - 9*c + a + 10, c - 3) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 /\ a - 3*c + 3 >= b - 6*c + 6 ] (1, 4) f0(a, b, c) -> f1(a - 2*c + 2, b - 6*c + a + 4, c - 2) [ a >= b /\ a - c >= b - 2*c /\ a - 2*c + 1 >= b - 4*c + 2 ] (1, 3) f0(a, b, c) -> f1(a - c + 1, b - 3*c + a + 1, c - 1) [ a >= b /\ a - c >= b - 2*c ] (1, 2) f0(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a + 1, b + a + 1, c) [ a >= b ] (?, 1) f1(a, b, c) -> f1(a - c, b - 2*c, c - 1) [ a >= b ] start location: f0 leaf cost: 0 Complexity upper bound ? Time: 10.935 sec (SMT: 10.421 sec)