MAYBE Initial complexity problem: 1: T: (?, 1) eval(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] (1, 1) start(a, b, c) -> eval(a, b, c) start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a, b, c) with all transitions in problem 1, the following new transitions are obtained: start(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] start(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] We thus obtain the following problem: 2: T: (1, 2) start(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] (1, 2) start(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] with all transitions in problem 2, the following new transitions are obtained: start(a, b, c) -> eval(a - 2*c + 1, b + 2*c^2 - 2*c + 1, c - 2) [ a >= b /\ a - c >= b + c^2 ] start(a, b, c) -> eval(a - c + 1, b + c^2 + a - c, c - 1) [ a >= b /\ a - c >= b + c^2 ] We thus obtain the following problem: 3: T: (1, 3) start(a, b, c) -> eval(a - 2*c + 1, b + 2*c^2 - 2*c + 1, c - 2) [ a >= b /\ a - c >= b + c^2 ] (1, 3) start(a, b, c) -> eval(a - c + 1, b + c^2 + a - c, c - 1) [ a >= b /\ a - c >= b + c^2 ] (1, 2) start(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a - 2*c + 1, b + 2*c^2 - 2*c + 1, c - 2) [ a >= b /\ a - c >= b + c^2 ] with all transitions in problem 3, the following new transitions are obtained: start(a, b, c) -> eval(a - 3*c + 3, b + 3*c^2 - 6*c + 5, c - 3) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] start(a, b, c) -> eval(a - 2*c + 2, b + 2*c^2 - 4*c + a + 2, c - 2) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] We thus obtain the following problem: 4: T: (1, 4) start(a, b, c) -> eval(a - 3*c + 3, b + 3*c^2 - 6*c + 5, c - 3) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] (1, 4) start(a, b, c) -> eval(a - 2*c + 2, b + 2*c^2 - 4*c + a + 2, c - 2) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] (1, 3) start(a, b, c) -> eval(a - c + 1, b + c^2 + a - c, c - 1) [ a >= b /\ a - c >= b + c^2 ] (1, 2) start(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a - 3*c + 3, b + 3*c^2 - 6*c + 5, c - 3) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] with all transitions in problem 4, the following new transitions are obtained: start(a, b, c) -> eval(a - 4*c + 6, b + 4*c^2 - 12*c + 14, c - 4) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 ] start(a, b, c) -> eval(a - 3*c + 4, b + 3*c^2 - 9*c + a + 8, c - 3) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 ] We thus obtain the following problem: 5: T: (1, 5) start(a, b, c) -> eval(a - 4*c + 6, b + 4*c^2 - 12*c + 14, c - 4) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 ] (1, 5) start(a, b, c) -> eval(a - 3*c + 4, b + 3*c^2 - 9*c + a + 8, c - 3) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 ] (1, 4) start(a, b, c) -> eval(a - 2*c + 2, b + 2*c^2 - 4*c + a + 2, c - 2) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] (1, 3) start(a, b, c) -> eval(a - c + 1, b + c^2 + a - c, c - 1) [ a >= b /\ a - c >= b + c^2 ] (1, 2) start(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a - 4*c + 6, b + 4*c^2 - 12*c + 14, c - 4) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 ] with all transitions in problem 5, the following new transitions are obtained: start(a, b, c) -> eval(a - 5*c + 10, b + 5*c^2 - 20*c + 30, c - 5) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 ] start(a, b, c) -> eval(a - 4*c + 7, b + 4*c^2 - 16*c + a + 20, c - 4) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 ] We thus obtain the following problem: 6: T: (1, 6) start(a, b, c) -> eval(a - 5*c + 10, b + 5*c^2 - 20*c + 30, c - 5) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 ] (1, 6) start(a, b, c) -> eval(a - 4*c + 7, b + 4*c^2 - 16*c + a + 20, c - 4) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 ] (1, 5) start(a, b, c) -> eval(a - 3*c + 4, b + 3*c^2 - 9*c + a + 8, c - 3) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 ] (1, 4) start(a, b, c) -> eval(a - 2*c + 2, b + 2*c^2 - 4*c + a + 2, c - 2) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] (1, 3) start(a, b, c) -> eval(a - c + 1, b + c^2 + a - c, c - 1) [ a >= b /\ a - c >= b + c^2 ] (1, 2) start(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a - 5*c + 10, b + 5*c^2 - 20*c + 30, c - 5) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 ] with all transitions in problem 6, the following new transitions are obtained: start(a, b, c) -> eval(a - 6*c + 15, b + 6*c^2 - 30*c + 55, c - 6) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 ] start(a, b, c) -> eval(a - 5*c + 11, b + 5*c^2 - 25*c + a + 40, c - 5) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 ] We thus obtain the following problem: 7: T: (1, 7) start(a, b, c) -> eval(a - 6*c + 15, b + 6*c^2 - 30*c + 55, c - 6) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 ] (1, 7) start(a, b, c) -> eval(a - 5*c + 11, b + 5*c^2 - 25*c + a + 40, c - 5) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 ] (1, 6) start(a, b, c) -> eval(a - 4*c + 7, b + 4*c^2 - 16*c + a + 20, c - 4) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 ] (1, 5) start(a, b, c) -> eval(a - 3*c + 4, b + 3*c^2 - 9*c + a + 8, c - 3) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 ] (1, 4) start(a, b, c) -> eval(a - 2*c + 2, b + 2*c^2 - 4*c + a + 2, c - 2) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] (1, 3) start(a, b, c) -> eval(a - c + 1, b + c^2 + a - c, c - 1) [ a >= b /\ a - c >= b + c^2 ] (1, 2) start(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a - 6*c + 15, b + 6*c^2 - 30*c + 55, c - 6) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 ] with all transitions in problem 7, the following new transitions are obtained: start(a, b, c) -> eval(a - 7*c + 21, b + 7*c^2 - 42*c + 91, c - 7) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 ] start(a, b, c) -> eval(a - 6*c + 16, b + 6*c^2 - 36*c + a + 70, c - 6) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 ] We thus obtain the following problem: 8: T: (1, 8) start(a, b, c) -> eval(a - 7*c + 21, b + 7*c^2 - 42*c + 91, c - 7) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 ] (1, 8) start(a, b, c) -> eval(a - 6*c + 16, b + 6*c^2 - 36*c + a + 70, c - 6) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 ] (1, 7) start(a, b, c) -> eval(a - 5*c + 11, b + 5*c^2 - 25*c + a + 40, c - 5) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 ] (1, 6) start(a, b, c) -> eval(a - 4*c + 7, b + 4*c^2 - 16*c + a + 20, c - 4) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 ] (1, 5) start(a, b, c) -> eval(a - 3*c + 4, b + 3*c^2 - 9*c + a + 8, c - 3) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 ] (1, 4) start(a, b, c) -> eval(a - 2*c + 2, b + 2*c^2 - 4*c + a + 2, c - 2) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] (1, 3) start(a, b, c) -> eval(a - c + 1, b + c^2 + a - c, c - 1) [ a >= b /\ a - c >= b + c^2 ] (1, 2) start(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a - 7*c + 21, b + 7*c^2 - 42*c + 91, c - 7) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 ] with all transitions in problem 8, the following new transitions are obtained: start(a, b, c) -> eval(a - 8*c + 28, b + 8*c^2 - 56*c + 140, c - 8) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 ] start(a, b, c) -> eval(a - 7*c + 22, b + 7*c^2 - 49*c + a + 112, c - 7) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 ] We thus obtain the following problem: 9: T: (1, 9) start(a, b, c) -> eval(a - 8*c + 28, b + 8*c^2 - 56*c + 140, c - 8) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 ] (1, 9) start(a, b, c) -> eval(a - 7*c + 22, b + 7*c^2 - 49*c + a + 112, c - 7) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 ] (1, 8) start(a, b, c) -> eval(a - 6*c + 16, b + 6*c^2 - 36*c + a + 70, c - 6) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 ] (1, 7) start(a, b, c) -> eval(a - 5*c + 11, b + 5*c^2 - 25*c + a + 40, c - 5) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 ] (1, 6) start(a, b, c) -> eval(a - 4*c + 7, b + 4*c^2 - 16*c + a + 20, c - 4) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 ] (1, 5) start(a, b, c) -> eval(a - 3*c + 4, b + 3*c^2 - 9*c + a + 8, c - 3) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 ] (1, 4) start(a, b, c) -> eval(a - 2*c + 2, b + 2*c^2 - 4*c + a + 2, c - 2) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] (1, 3) start(a, b, c) -> eval(a - c + 1, b + c^2 + a - c, c - 1) [ a >= b /\ a - c >= b + c^2 ] (1, 2) start(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a - 8*c + 28, b + 8*c^2 - 56*c + 140, c - 8) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 ] with all transitions in problem 9, the following new transitions are obtained: start(a, b, c) -> eval(a - 9*c + 36, b + 9*c^2 - 72*c + 204, c - 9) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 ] start(a, b, c) -> eval(a - 8*c + 29, b + 8*c^2 - 64*c + a + 168, c - 8) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 ] We thus obtain the following problem: 10: T: (1, 10) start(a, b, c) -> eval(a - 9*c + 36, b + 9*c^2 - 72*c + 204, c - 9) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 ] (1, 10) start(a, b, c) -> eval(a - 8*c + 29, b + 8*c^2 - 64*c + a + 168, c - 8) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 ] (1, 9) start(a, b, c) -> eval(a - 7*c + 22, b + 7*c^2 - 49*c + a + 112, c - 7) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 ] (1, 8) start(a, b, c) -> eval(a - 6*c + 16, b + 6*c^2 - 36*c + a + 70, c - 6) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 ] (1, 7) start(a, b, c) -> eval(a - 5*c + 11, b + 5*c^2 - 25*c + a + 40, c - 5) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 ] (1, 6) start(a, b, c) -> eval(a - 4*c + 7, b + 4*c^2 - 16*c + a + 20, c - 4) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 ] (1, 5) start(a, b, c) -> eval(a - 3*c + 4, b + 3*c^2 - 9*c + a + 8, c - 3) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 ] (1, 4) start(a, b, c) -> eval(a - 2*c + 2, b + 2*c^2 - 4*c + a + 2, c - 2) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] (1, 3) start(a, b, c) -> eval(a - c + 1, b + c^2 + a - c, c - 1) [ a >= b /\ a - c >= b + c^2 ] (1, 2) start(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a - 9*c + 36, b + 9*c^2 - 72*c + 204, c - 9) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 ] with all transitions in problem 10, the following new transitions are obtained: start(a, b, c) -> eval(a - 10*c + 45, b + 10*c^2 - 90*c + 285, c - 10) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 ] start(a, b, c) -> eval(a - 9*c + 37, b + 9*c^2 - 81*c + a + 240, c - 9) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 ] We thus obtain the following problem: 11: T: (1, 11) start(a, b, c) -> eval(a - 10*c + 45, b + 10*c^2 - 90*c + 285, c - 10) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 ] (1, 11) start(a, b, c) -> eval(a - 9*c + 37, b + 9*c^2 - 81*c + a + 240, c - 9) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 ] (1, 10) start(a, b, c) -> eval(a - 8*c + 29, b + 8*c^2 - 64*c + a + 168, c - 8) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 ] (1, 9) start(a, b, c) -> eval(a - 7*c + 22, b + 7*c^2 - 49*c + a + 112, c - 7) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 ] (1, 8) start(a, b, c) -> eval(a - 6*c + 16, b + 6*c^2 - 36*c + a + 70, c - 6) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 ] (1, 7) start(a, b, c) -> eval(a - 5*c + 11, b + 5*c^2 - 25*c + a + 40, c - 5) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 ] (1, 6) start(a, b, c) -> eval(a - 4*c + 7, b + 4*c^2 - 16*c + a + 20, c - 4) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 ] (1, 5) start(a, b, c) -> eval(a - 3*c + 4, b + 3*c^2 - 9*c + a + 8, c - 3) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 ] (1, 4) start(a, b, c) -> eval(a - 2*c + 2, b + 2*c^2 - 4*c + a + 2, c - 2) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] (1, 3) start(a, b, c) -> eval(a - c + 1, b + c^2 + a - c, c - 1) [ a >= b /\ a - c >= b + c^2 ] (1, 2) start(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a - 10*c + 45, b + 10*c^2 - 90*c + 285, c - 10) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 ] with all transitions in problem 11, the following new transitions are obtained: start(a, b, c) -> eval(a - 11*c + 55, b + 11*c^2 - 110*c + 385, c - 11) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 ] start(a, b, c) -> eval(a - 10*c + 46, b + 10*c^2 - 100*c + a + 330, c - 10) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 ] We thus obtain the following problem: 12: T: (1, 12) start(a, b, c) -> eval(a - 11*c + 55, b + 11*c^2 - 110*c + 385, c - 11) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 ] (1, 12) start(a, b, c) -> eval(a - 10*c + 46, b + 10*c^2 - 100*c + a + 330, c - 10) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 ] (1, 11) start(a, b, c) -> eval(a - 9*c + 37, b + 9*c^2 - 81*c + a + 240, c - 9) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 ] (1, 10) start(a, b, c) -> eval(a - 8*c + 29, b + 8*c^2 - 64*c + a + 168, c - 8) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 ] (1, 9) start(a, b, c) -> eval(a - 7*c + 22, b + 7*c^2 - 49*c + a + 112, c - 7) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 ] (1, 8) start(a, b, c) -> eval(a - 6*c + 16, b + 6*c^2 - 36*c + a + 70, c - 6) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 ] (1, 7) start(a, b, c) -> eval(a - 5*c + 11, b + 5*c^2 - 25*c + a + 40, c - 5) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 ] (1, 6) start(a, b, c) -> eval(a - 4*c + 7, b + 4*c^2 - 16*c + a + 20, c - 4) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 ] (1, 5) start(a, b, c) -> eval(a - 3*c + 4, b + 3*c^2 - 9*c + a + 8, c - 3) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 ] (1, 4) start(a, b, c) -> eval(a - 2*c + 2, b + 2*c^2 - 4*c + a + 2, c - 2) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] (1, 3) start(a, b, c) -> eval(a - c + 1, b + c^2 + a - c, c - 1) [ a >= b /\ a - c >= b + c^2 ] (1, 2) start(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a - 11*c + 55, b + 11*c^2 - 110*c + 385, c - 11) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 ] with all transitions in problem 12, the following new transitions are obtained: start(a, b, c) -> eval(a - 12*c + 66, b + 12*c^2 - 132*c + 506, c - 12) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 ] start(a, b, c) -> eval(a - 11*c + 56, b + 11*c^2 - 121*c + a + 440, c - 11) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 ] We thus obtain the following problem: 13: T: (1, 13) start(a, b, c) -> eval(a - 12*c + 66, b + 12*c^2 - 132*c + 506, c - 12) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 ] (1, 13) start(a, b, c) -> eval(a - 11*c + 56, b + 11*c^2 - 121*c + a + 440, c - 11) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 ] (1, 12) start(a, b, c) -> eval(a - 10*c + 46, b + 10*c^2 - 100*c + a + 330, c - 10) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 ] (1, 11) start(a, b, c) -> eval(a - 9*c + 37, b + 9*c^2 - 81*c + a + 240, c - 9) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 ] (1, 10) start(a, b, c) -> eval(a - 8*c + 29, b + 8*c^2 - 64*c + a + 168, c - 8) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 ] (1, 9) start(a, b, c) -> eval(a - 7*c + 22, b + 7*c^2 - 49*c + a + 112, c - 7) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 ] (1, 8) start(a, b, c) -> eval(a - 6*c + 16, b + 6*c^2 - 36*c + a + 70, c - 6) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 ] (1, 7) start(a, b, c) -> eval(a - 5*c + 11, b + 5*c^2 - 25*c + a + 40, c - 5) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 ] (1, 6) start(a, b, c) -> eval(a - 4*c + 7, b + 4*c^2 - 16*c + a + 20, c - 4) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 ] (1, 5) start(a, b, c) -> eval(a - 3*c + 4, b + 3*c^2 - 9*c + a + 8, c - 3) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 ] (1, 4) start(a, b, c) -> eval(a - 2*c + 2, b + 2*c^2 - 4*c + a + 2, c - 2) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] (1, 3) start(a, b, c) -> eval(a - c + 1, b + c^2 + a - c, c - 1) [ a >= b /\ a - c >= b + c^2 ] (1, 2) start(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a - 12*c + 66, b + 12*c^2 - 132*c + 506, c - 12) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 ] with all transitions in problem 13, the following new transitions are obtained: start(a, b, c) -> eval(a - 13*c + 78, b + 13*c^2 - 156*c + 650, c - 13) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 ] start(a, b, c) -> eval(a - 12*c + 67, b + 12*c^2 - 144*c + a + 572, c - 12) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 ] We thus obtain the following problem: 14: T: (1, 14) start(a, b, c) -> eval(a - 13*c + 78, b + 13*c^2 - 156*c + 650, c - 13) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 ] (1, 14) start(a, b, c) -> eval(a - 12*c + 67, b + 12*c^2 - 144*c + a + 572, c - 12) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 ] (1, 13) start(a, b, c) -> eval(a - 11*c + 56, b + 11*c^2 - 121*c + a + 440, c - 11) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 ] (1, 12) start(a, b, c) -> eval(a - 10*c + 46, b + 10*c^2 - 100*c + a + 330, c - 10) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 ] (1, 11) start(a, b, c) -> eval(a - 9*c + 37, b + 9*c^2 - 81*c + a + 240, c - 9) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 ] (1, 10) start(a, b, c) -> eval(a - 8*c + 29, b + 8*c^2 - 64*c + a + 168, c - 8) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 ] (1, 9) start(a, b, c) -> eval(a - 7*c + 22, b + 7*c^2 - 49*c + a + 112, c - 7) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 ] (1, 8) start(a, b, c) -> eval(a - 6*c + 16, b + 6*c^2 - 36*c + a + 70, c - 6) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 ] (1, 7) start(a, b, c) -> eval(a - 5*c + 11, b + 5*c^2 - 25*c + a + 40, c - 5) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 ] (1, 6) start(a, b, c) -> eval(a - 4*c + 7, b + 4*c^2 - 16*c + a + 20, c - 4) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 ] (1, 5) start(a, b, c) -> eval(a - 3*c + 4, b + 3*c^2 - 9*c + a + 8, c - 3) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 ] (1, 4) start(a, b, c) -> eval(a - 2*c + 2, b + 2*c^2 - 4*c + a + 2, c - 2) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] (1, 3) start(a, b, c) -> eval(a - c + 1, b + c^2 + a - c, c - 1) [ a >= b /\ a - c >= b + c^2 ] (1, 2) start(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a - 13*c + 78, b + 13*c^2 - 156*c + 650, c - 13) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 ] with all transitions in problem 14, the following new transitions are obtained: start(a, b, c) -> eval(a - 14*c + 91, b + 14*c^2 - 182*c + 819, c - 14) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 /\ a - 13*c + 78 >= b + 13*c^2 - 156*c + 650 ] start(a, b, c) -> eval(a - 13*c + 79, b + 13*c^2 - 169*c + a + 728, c - 13) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 /\ a - 13*c + 78 >= b + 13*c^2 - 156*c + 650 ] We thus obtain the following problem: 15: T: (1, 15) start(a, b, c) -> eval(a - 14*c + 91, b + 14*c^2 - 182*c + 819, c - 14) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 /\ a - 13*c + 78 >= b + 13*c^2 - 156*c + 650 ] (1, 15) start(a, b, c) -> eval(a - 13*c + 79, b + 13*c^2 - 169*c + a + 728, c - 13) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 /\ a - 13*c + 78 >= b + 13*c^2 - 156*c + 650 ] (1, 14) start(a, b, c) -> eval(a - 12*c + 67, b + 12*c^2 - 144*c + a + 572, c - 12) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 ] (1, 13) start(a, b, c) -> eval(a - 11*c + 56, b + 11*c^2 - 121*c + a + 440, c - 11) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 ] (1, 12) start(a, b, c) -> eval(a - 10*c + 46, b + 10*c^2 - 100*c + a + 330, c - 10) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 ] (1, 11) start(a, b, c) -> eval(a - 9*c + 37, b + 9*c^2 - 81*c + a + 240, c - 9) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 ] (1, 10) start(a, b, c) -> eval(a - 8*c + 29, b + 8*c^2 - 64*c + a + 168, c - 8) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 ] (1, 9) start(a, b, c) -> eval(a - 7*c + 22, b + 7*c^2 - 49*c + a + 112, c - 7) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 ] (1, 8) start(a, b, c) -> eval(a - 6*c + 16, b + 6*c^2 - 36*c + a + 70, c - 6) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 ] (1, 7) start(a, b, c) -> eval(a - 5*c + 11, b + 5*c^2 - 25*c + a + 40, c - 5) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 ] (1, 6) start(a, b, c) -> eval(a - 4*c + 7, b + 4*c^2 - 16*c + a + 20, c - 4) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 ] (1, 5) start(a, b, c) -> eval(a - 3*c + 4, b + 3*c^2 - 9*c + a + 8, c - 3) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 ] (1, 4) start(a, b, c) -> eval(a - 2*c + 2, b + 2*c^2 - 4*c + a + 2, c - 2) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] (1, 3) start(a, b, c) -> eval(a - c + 1, b + c^2 + a - c, c - 1) [ a >= b /\ a - c >= b + c^2 ] (1, 2) start(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a - 14*c + 91, b + 14*c^2 - 182*c + 819, c - 14) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 /\ a - 13*c + 78 >= b + 13*c^2 - 156*c + 650 ] with all transitions in problem 15, the following new transitions are obtained: start(a, b, c) -> eval(a - 15*c + 105, b + 15*c^2 - 210*c + 1015, c - 15) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 /\ a - 13*c + 78 >= b + 13*c^2 - 156*c + 650 /\ a - 14*c + 91 >= b + 14*c^2 - 182*c + 819 ] start(a, b, c) -> eval(a - 14*c + 92, b + 14*c^2 - 196*c + a + 910, c - 14) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 /\ a - 13*c + 78 >= b + 13*c^2 - 156*c + 650 /\ a - 14*c + 91 >= b + 14*c^2 - 182*c + 819 ] We thus obtain the following problem: 16: T: (1, 16) start(a, b, c) -> eval(a - 15*c + 105, b + 15*c^2 - 210*c + 1015, c - 15) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 /\ a - 13*c + 78 >= b + 13*c^2 - 156*c + 650 /\ a - 14*c + 91 >= b + 14*c^2 - 182*c + 819 ] (1, 16) start(a, b, c) -> eval(a - 14*c + 92, b + 14*c^2 - 196*c + a + 910, c - 14) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 /\ a - 13*c + 78 >= b + 13*c^2 - 156*c + 650 /\ a - 14*c + 91 >= b + 14*c^2 - 182*c + 819 ] (1, 15) start(a, b, c) -> eval(a - 13*c + 79, b + 13*c^2 - 169*c + a + 728, c - 13) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 /\ a - 13*c + 78 >= b + 13*c^2 - 156*c + 650 ] (1, 14) start(a, b, c) -> eval(a - 12*c + 67, b + 12*c^2 - 144*c + a + 572, c - 12) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 /\ a - 12*c + 66 >= b + 12*c^2 - 132*c + 506 ] (1, 13) start(a, b, c) -> eval(a - 11*c + 56, b + 11*c^2 - 121*c + a + 440, c - 11) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 /\ a - 11*c + 55 >= b + 11*c^2 - 110*c + 385 ] (1, 12) start(a, b, c) -> eval(a - 10*c + 46, b + 10*c^2 - 100*c + a + 330, c - 10) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 /\ a - 10*c + 45 >= b + 10*c^2 - 90*c + 285 ] (1, 11) start(a, b, c) -> eval(a - 9*c + 37, b + 9*c^2 - 81*c + a + 240, c - 9) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 /\ a - 9*c + 36 >= b + 9*c^2 - 72*c + 204 ] (1, 10) start(a, b, c) -> eval(a - 8*c + 29, b + 8*c^2 - 64*c + a + 168, c - 8) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 /\ a - 8*c + 28 >= b + 8*c^2 - 56*c + 140 ] (1, 9) start(a, b, c) -> eval(a - 7*c + 22, b + 7*c^2 - 49*c + a + 112, c - 7) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 /\ a - 7*c + 21 >= b + 7*c^2 - 42*c + 91 ] (1, 8) start(a, b, c) -> eval(a - 6*c + 16, b + 6*c^2 - 36*c + a + 70, c - 6) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 /\ a - 6*c + 15 >= b + 6*c^2 - 30*c + 55 ] (1, 7) start(a, b, c) -> eval(a - 5*c + 11, b + 5*c^2 - 25*c + a + 40, c - 5) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 /\ a - 5*c + 10 >= b + 5*c^2 - 20*c + 30 ] (1, 6) start(a, b, c) -> eval(a - 4*c + 7, b + 4*c^2 - 16*c + a + 20, c - 4) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 /\ a - 4*c + 6 >= b + 4*c^2 - 12*c + 14 ] (1, 5) start(a, b, c) -> eval(a - 3*c + 4, b + 3*c^2 - 9*c + a + 8, c - 3) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 /\ a - 3*c + 3 >= b + 3*c^2 - 6*c + 5 ] (1, 4) start(a, b, c) -> eval(a - 2*c + 2, b + 2*c^2 - 4*c + a + 2, c - 2) [ a >= b /\ a - c >= b + c^2 /\ a - 2*c + 1 >= b + 2*c^2 - 2*c + 1 ] (1, 3) start(a, b, c) -> eval(a - c + 1, b + c^2 + a - c, c - 1) [ a >= b /\ a - c >= b + c^2 ] (1, 2) start(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a + 1, b + a, c) [ a >= b ] (?, 1) eval(a, b, c) -> eval(a - c, b + c^2, c - 1) [ a >= b ] start location: start leaf cost: 0 Complexity upper bound ? Time: 5.592 sec (SMT: 5.336 sec)