MAYBE Initial complexity problem: 1: T: (?, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] (1, 1) start(a, b, c) -> eval(a, b, c) start location: start leaf cost: 0 A polynomial rank function with Pol(eval) = V_1 + 1 Pol(start) = V_1 + 1 orients all transitions weakly and the transition eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] strictly and produces the following problem: 2: T: (a + 1, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] (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 2, the following new transitions are obtained: start(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] start(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] We thus obtain the following problem: 3: T: (1, 2) start(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] (1, 2) start(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (a + 1, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] with all transitions in problem 3, the following new transitions are obtained: start(a, b, c) -> eval(a, b + 2*c - 1, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] start(a, b, c) -> eval(a - 1, b + c, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] We thus obtain the following problem: 4: T: (1, 3) start(a, b, c) -> eval(a, b + 2*c - 1, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] (1, 3) start(a, b, c) -> eval(a - 1, b + c, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] (1, 2) start(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (a + 1, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a, b + 2*c - 1, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] with all transitions in problem 4, the following new transitions are obtained: start(a, b, c) -> eval(a, b + 3*c - 3, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] start(a, b, c) -> eval(a - 1, b + 2*c - 1, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] We thus obtain the following problem: 5: T: (1, 4) start(a, b, c) -> eval(a, b + 3*c - 3, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] (1, 4) start(a, b, c) -> eval(a - 1, b + 2*c - 1, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] (1, 3) start(a, b, c) -> eval(a - 1, b + c, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] (1, 2) start(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (a + 1, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a, b + 3*c - 3, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] with all transitions in problem 5, the following new transitions are obtained: start(a, b, c) -> eval(a, b + 4*c - 6, c - 4) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 ] start(a, b, c) -> eval(a - 1, b + 3*c - 3, c - 4) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 ] We thus obtain the following problem: 6: T: (1, 5) start(a, b, c) -> eval(a, b + 4*c - 6, c - 4) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 ] (1, 5) start(a, b, c) -> eval(a - 1, b + 3*c - 3, c - 4) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 ] (1, 4) start(a, b, c) -> eval(a - 1, b + 2*c - 1, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] (1, 3) start(a, b, c) -> eval(a - 1, b + c, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] (1, 2) start(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (a + 1, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a, b + 4*c - 6, c - 4) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 ] with all transitions in problem 6, the following new transitions are obtained: start(a, b, c) -> eval(a, b + 5*c - 10, c - 5) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 ] start(a, b, c) -> eval(a - 1, b + 4*c - 6, c - 5) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 ] We thus obtain the following problem: 7: T: (1, 6) start(a, b, c) -> eval(a, b + 5*c - 10, c - 5) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 ] (1, 6) start(a, b, c) -> eval(a - 1, b + 4*c - 6, c - 5) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 ] (1, 5) start(a, b, c) -> eval(a - 1, b + 3*c - 3, c - 4) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 ] (1, 4) start(a, b, c) -> eval(a - 1, b + 2*c - 1, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] (1, 3) start(a, b, c) -> eval(a - 1, b + c, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] (1, 2) start(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (a + 1, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a, b + 5*c - 10, c - 5) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 ] with all transitions in problem 7, the following new transitions are obtained: start(a, b, c) -> eval(a, b + 6*c - 15, c - 6) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 ] start(a, b, c) -> eval(a - 1, b + 5*c - 10, c - 6) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 ] We thus obtain the following problem: 8: T: (1, 7) start(a, b, c) -> eval(a, b + 6*c - 15, c - 6) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 ] (1, 7) start(a, b, c) -> eval(a - 1, b + 5*c - 10, c - 6) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 ] (1, 6) start(a, b, c) -> eval(a - 1, b + 4*c - 6, c - 5) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 ] (1, 5) start(a, b, c) -> eval(a - 1, b + 3*c - 3, c - 4) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 ] (1, 4) start(a, b, c) -> eval(a - 1, b + 2*c - 1, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] (1, 3) start(a, b, c) -> eval(a - 1, b + c, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] (1, 2) start(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (a + 1, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a, b + 6*c - 15, c - 6) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 ] with all transitions in problem 8, the following new transitions are obtained: start(a, b, c) -> eval(a, b + 7*c - 21, c - 7) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 ] start(a, b, c) -> eval(a - 1, b + 6*c - 15, c - 7) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 ] We thus obtain the following problem: 9: T: (1, 8) start(a, b, c) -> eval(a, b + 7*c - 21, c - 7) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 ] (1, 8) start(a, b, c) -> eval(a - 1, b + 6*c - 15, c - 7) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 ] (1, 7) start(a, b, c) -> eval(a - 1, b + 5*c - 10, c - 6) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 ] (1, 6) start(a, b, c) -> eval(a - 1, b + 4*c - 6, c - 5) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 ] (1, 5) start(a, b, c) -> eval(a - 1, b + 3*c - 3, c - 4) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 ] (1, 4) start(a, b, c) -> eval(a - 1, b + 2*c - 1, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] (1, 3) start(a, b, c) -> eval(a - 1, b + c, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] (1, 2) start(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (a + 1, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a, b + 7*c - 21, c - 7) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 ] with all transitions in problem 9, the following new transitions are obtained: start(a, b, c) -> eval(a, b + 8*c - 28, c - 8) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 ] start(a, b, c) -> eval(a - 1, b + 7*c - 21, c - 8) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 ] We thus obtain the following problem: 10: T: (1, 9) start(a, b, c) -> eval(a, b + 8*c - 28, c - 8) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 ] (1, 9) start(a, b, c) -> eval(a - 1, b + 7*c - 21, c - 8) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 ] (1, 8) start(a, b, c) -> eval(a - 1, b + 6*c - 15, c - 7) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 ] (1, 7) start(a, b, c) -> eval(a - 1, b + 5*c - 10, c - 6) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 ] (1, 6) start(a, b, c) -> eval(a - 1, b + 4*c - 6, c - 5) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 ] (1, 5) start(a, b, c) -> eval(a - 1, b + 3*c - 3, c - 4) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 ] (1, 4) start(a, b, c) -> eval(a - 1, b + 2*c - 1, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] (1, 3) start(a, b, c) -> eval(a - 1, b + c, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] (1, 2) start(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (a + 1, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a, b + 8*c - 28, c - 8) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 ] with all transitions in problem 10, the following new transitions are obtained: start(a, b, c) -> eval(a, b + 9*c - 36, c - 9) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 ] start(a, b, c) -> eval(a - 1, b + 8*c - 28, c - 9) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 ] We thus obtain the following problem: 11: T: (1, 10) start(a, b, c) -> eval(a, b + 9*c - 36, c - 9) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 ] (1, 10) start(a, b, c) -> eval(a - 1, b + 8*c - 28, c - 9) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 ] (1, 9) start(a, b, c) -> eval(a - 1, b + 7*c - 21, c - 8) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 ] (1, 8) start(a, b, c) -> eval(a - 1, b + 6*c - 15, c - 7) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 ] (1, 7) start(a, b, c) -> eval(a - 1, b + 5*c - 10, c - 6) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 ] (1, 6) start(a, b, c) -> eval(a - 1, b + 4*c - 6, c - 5) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 ] (1, 5) start(a, b, c) -> eval(a - 1, b + 3*c - 3, c - 4) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 ] (1, 4) start(a, b, c) -> eval(a - 1, b + 2*c - 1, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] (1, 3) start(a, b, c) -> eval(a - 1, b + c, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] (1, 2) start(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (a + 1, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a, b + 9*c - 36, c - 9) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 ] with all transitions in problem 11, the following new transitions are obtained: start(a, b, c) -> eval(a, b + 10*c - 45, c - 10) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 ] start(a, b, c) -> eval(a - 1, b + 9*c - 36, c - 10) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 ] We thus obtain the following problem: 12: T: (1, 11) start(a, b, c) -> eval(a, b + 10*c - 45, c - 10) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 ] (1, 11) start(a, b, c) -> eval(a - 1, b + 9*c - 36, c - 10) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 ] (1, 10) start(a, b, c) -> eval(a - 1, b + 8*c - 28, c - 9) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 ] (1, 9) start(a, b, c) -> eval(a - 1, b + 7*c - 21, c - 8) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 ] (1, 8) start(a, b, c) -> eval(a - 1, b + 6*c - 15, c - 7) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 ] (1, 7) start(a, b, c) -> eval(a - 1, b + 5*c - 10, c - 6) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 ] (1, 6) start(a, b, c) -> eval(a - 1, b + 4*c - 6, c - 5) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 ] (1, 5) start(a, b, c) -> eval(a - 1, b + 3*c - 3, c - 4) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 ] (1, 4) start(a, b, c) -> eval(a - 1, b + 2*c - 1, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] (1, 3) start(a, b, c) -> eval(a - 1, b + c, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] (1, 2) start(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (a + 1, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a, b + 10*c - 45, c - 10) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 ] with all transitions in problem 12, the following new transitions are obtained: start(a, b, c) -> eval(a, b + 11*c - 55, c - 11) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 ] start(a, b, c) -> eval(a - 1, b + 10*c - 45, c - 11) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 ] We thus obtain the following problem: 13: T: (1, 12) start(a, b, c) -> eval(a, b + 11*c - 55, c - 11) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 ] (1, 12) start(a, b, c) -> eval(a - 1, b + 10*c - 45, c - 11) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 ] (1, 11) start(a, b, c) -> eval(a - 1, b + 9*c - 36, c - 10) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 ] (1, 10) start(a, b, c) -> eval(a - 1, b + 8*c - 28, c - 9) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 ] (1, 9) start(a, b, c) -> eval(a - 1, b + 7*c - 21, c - 8) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 ] (1, 8) start(a, b, c) -> eval(a - 1, b + 6*c - 15, c - 7) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 ] (1, 7) start(a, b, c) -> eval(a - 1, b + 5*c - 10, c - 6) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 ] (1, 6) start(a, b, c) -> eval(a - 1, b + 4*c - 6, c - 5) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 ] (1, 5) start(a, b, c) -> eval(a - 1, b + 3*c - 3, c - 4) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 ] (1, 4) start(a, b, c) -> eval(a - 1, b + 2*c - 1, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] (1, 3) start(a, b, c) -> eval(a - 1, b + c, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] (1, 2) start(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (a + 1, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a, b + 11*c - 55, c - 11) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 ] with all transitions in problem 13, the following new transitions are obtained: start(a, b, c) -> eval(a, b + 12*c - 66, c - 12) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 ] start(a, b, c) -> eval(a - 1, b + 11*c - 55, c - 12) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 ] We thus obtain the following problem: 14: T: (1, 13) start(a, b, c) -> eval(a, b + 12*c - 66, c - 12) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 ] (1, 13) start(a, b, c) -> eval(a - 1, b + 11*c - 55, c - 12) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 ] (1, 12) start(a, b, c) -> eval(a - 1, b + 10*c - 45, c - 11) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 ] (1, 11) start(a, b, c) -> eval(a - 1, b + 9*c - 36, c - 10) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 ] (1, 10) start(a, b, c) -> eval(a - 1, b + 8*c - 28, c - 9) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 ] (1, 9) start(a, b, c) -> eval(a - 1, b + 7*c - 21, c - 8) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 ] (1, 8) start(a, b, c) -> eval(a - 1, b + 6*c - 15, c - 7) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 ] (1, 7) start(a, b, c) -> eval(a - 1, b + 5*c - 10, c - 6) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 ] (1, 6) start(a, b, c) -> eval(a - 1, b + 4*c - 6, c - 5) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 ] (1, 5) start(a, b, c) -> eval(a - 1, b + 3*c - 3, c - 4) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 ] (1, 4) start(a, b, c) -> eval(a - 1, b + 2*c - 1, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] (1, 3) start(a, b, c) -> eval(a - 1, b + c, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] (1, 2) start(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (a + 1, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a, b + 12*c - 66, c - 12) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 ] with all transitions in problem 14, the following new transitions are obtained: start(a, b, c) -> eval(a, b + 13*c - 78, c - 13) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 ] start(a, b, c) -> eval(a - 1, b + 12*c - 66, c - 13) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 ] We thus obtain the following problem: 15: T: (1, 14) start(a, b, c) -> eval(a, b + 13*c - 78, c - 13) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 ] (1, 14) start(a, b, c) -> eval(a - 1, b + 12*c - 66, c - 13) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 ] (1, 13) start(a, b, c) -> eval(a - 1, b + 11*c - 55, c - 12) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 ] (1, 12) start(a, b, c) -> eval(a - 1, b + 10*c - 45, c - 11) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 ] (1, 11) start(a, b, c) -> eval(a - 1, b + 9*c - 36, c - 10) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 ] (1, 10) start(a, b, c) -> eval(a - 1, b + 8*c - 28, c - 9) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 ] (1, 9) start(a, b, c) -> eval(a - 1, b + 7*c - 21, c - 8) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 ] (1, 8) start(a, b, c) -> eval(a - 1, b + 6*c - 15, c - 7) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 ] (1, 7) start(a, b, c) -> eval(a - 1, b + 5*c - 10, c - 6) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 ] (1, 6) start(a, b, c) -> eval(a - 1, b + 4*c - 6, c - 5) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 ] (1, 5) start(a, b, c) -> eval(a - 1, b + 3*c - 3, c - 4) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 ] (1, 4) start(a, b, c) -> eval(a - 1, b + 2*c - 1, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] (1, 3) start(a, b, c) -> eval(a - 1, b + c, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] (1, 2) start(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (a + 1, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a, b + 13*c - 78, c - 13) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 ] with all transitions in problem 15, the following new transitions are obtained: start(a, b, c) -> eval(a, b + 14*c - 91, c - 14) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 /\ b^3 + 39*b^2*c + 507*b*c^2 - 234*b^2 - 6084*b*c + 2197*c^3 - 39546*c^2 + 18252*b + 237276*c - 474552 >= c - 13 ] start(a, b, c) -> eval(a - 1, b + 13*c - 78, c - 14) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 /\ b^3 + 39*b^2*c + 507*b*c^2 - 234*b^2 - 6084*b*c + 2197*c^3 - 39546*c^2 + 18252*b + 237276*c - 474552 >= c - 13 ] We thus obtain the following problem: 16: T: (1, 15) start(a, b, c) -> eval(a, b + 14*c - 91, c - 14) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 /\ b^3 + 39*b^2*c + 507*b*c^2 - 234*b^2 - 6084*b*c + 2197*c^3 - 39546*c^2 + 18252*b + 237276*c - 474552 >= c - 13 ] (1, 15) start(a, b, c) -> eval(a - 1, b + 13*c - 78, c - 14) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 /\ b^3 + 39*b^2*c + 507*b*c^2 - 234*b^2 - 6084*b*c + 2197*c^3 - 39546*c^2 + 18252*b + 237276*c - 474552 >= c - 13 ] (1, 14) start(a, b, c) -> eval(a - 1, b + 12*c - 66, c - 13) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 ] (1, 13) start(a, b, c) -> eval(a - 1, b + 11*c - 55, c - 12) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 ] (1, 12) start(a, b, c) -> eval(a - 1, b + 10*c - 45, c - 11) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 ] (1, 11) start(a, b, c) -> eval(a - 1, b + 9*c - 36, c - 10) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 ] (1, 10) start(a, b, c) -> eval(a - 1, b + 8*c - 28, c - 9) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 ] (1, 9) start(a, b, c) -> eval(a - 1, b + 7*c - 21, c - 8) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 ] (1, 8) start(a, b, c) -> eval(a - 1, b + 6*c - 15, c - 7) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 ] (1, 7) start(a, b, c) -> eval(a - 1, b + 5*c - 10, c - 6) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 ] (1, 6) start(a, b, c) -> eval(a - 1, b + 4*c - 6, c - 5) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 ] (1, 5) start(a, b, c) -> eval(a - 1, b + 3*c - 3, c - 4) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 ] (1, 4) start(a, b, c) -> eval(a - 1, b + 2*c - 1, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] (1, 3) start(a, b, c) -> eval(a - 1, b + c, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] (1, 2) start(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (a + 1, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] start location: start leaf cost: 0 By chaining the transition start(a, b, c) -> eval(a, b + 14*c - 91, c - 14) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 /\ b^3 + 39*b^2*c + 507*b*c^2 - 234*b^2 - 6084*b*c + 2197*c^3 - 39546*c^2 + 18252*b + 237276*c - 474552 >= c - 13 ] with all transitions in problem 16, the following new transitions are obtained: start(a, b, c) -> eval(a, b + 15*c - 105, c - 15) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 /\ b^3 + 39*b^2*c + 507*b*c^2 - 234*b^2 - 6084*b*c + 2197*c^3 - 39546*c^2 + 18252*b + 237276*c - 474552 >= c - 13 /\ b^3 + 42*b^2*c + 588*b*c^2 - 273*b^2 - 7644*b*c + 2744*c^3 - 53508*c^2 + 24843*b + 347802*c - 753571 >= c - 14 ] start(a, b, c) -> eval(a - 1, b + 14*c - 91, c - 15) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 /\ b^3 + 39*b^2*c + 507*b*c^2 - 234*b^2 - 6084*b*c + 2197*c^3 - 39546*c^2 + 18252*b + 237276*c - 474552 >= c - 13 /\ b^3 + 42*b^2*c + 588*b*c^2 - 273*b^2 - 7644*b*c + 2744*c^3 - 53508*c^2 + 24843*b + 347802*c - 753571 >= c - 14 ] We thus obtain the following problem: 17: T: (1, 16) start(a, b, c) -> eval(a, b + 15*c - 105, c - 15) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 /\ b^3 + 39*b^2*c + 507*b*c^2 - 234*b^2 - 6084*b*c + 2197*c^3 - 39546*c^2 + 18252*b + 237276*c - 474552 >= c - 13 /\ b^3 + 42*b^2*c + 588*b*c^2 - 273*b^2 - 7644*b*c + 2744*c^3 - 53508*c^2 + 24843*b + 347802*c - 753571 >= c - 14 ] (1, 16) start(a, b, c) -> eval(a - 1, b + 14*c - 91, c - 15) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 /\ b^3 + 39*b^2*c + 507*b*c^2 - 234*b^2 - 6084*b*c + 2197*c^3 - 39546*c^2 + 18252*b + 237276*c - 474552 >= c - 13 /\ b^3 + 42*b^2*c + 588*b*c^2 - 273*b^2 - 7644*b*c + 2744*c^3 - 53508*c^2 + 24843*b + 347802*c - 753571 >= c - 14 ] (1, 15) start(a, b, c) -> eval(a - 1, b + 13*c - 78, c - 14) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 /\ b^3 + 39*b^2*c + 507*b*c^2 - 234*b^2 - 6084*b*c + 2197*c^3 - 39546*c^2 + 18252*b + 237276*c - 474552 >= c - 13 ] (1, 14) start(a, b, c) -> eval(a - 1, b + 12*c - 66, c - 13) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 /\ b^3 + 36*b^2*c + 432*b*c^2 - 198*b^2 - 4752*b*c + 1728*c^3 - 28512*c^2 + 13068*b + 156816*c - 287496 >= c - 12 ] (1, 13) start(a, b, c) -> eval(a - 1, b + 11*c - 55, c - 12) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 /\ b^3 + 33*b^2*c + 363*b*c^2 - 165*b^2 - 3630*b*c + 1331*c^3 - 19965*c^2 + 9075*b + 99825*c - 166375 >= c - 11 ] (1, 12) start(a, b, c) -> eval(a - 1, b + 10*c - 45, c - 11) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 /\ b^3 + 30*b^2*c + 300*b*c^2 - 135*b^2 - 2700*b*c + 1000*c^3 - 13500*c^2 + 6075*b + 60750*c - 91125 >= c - 10 ] (1, 11) start(a, b, c) -> eval(a - 1, b + 9*c - 36, c - 10) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 /\ b^3 + 27*b^2*c + 243*b*c^2 - 108*b^2 - 1944*b*c + 729*c^3 - 8748*c^2 + 3888*b + 34992*c - 46656 >= c - 9 ] (1, 10) start(a, b, c) -> eval(a - 1, b + 8*c - 28, c - 9) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 /\ b^3 + 24*b^2*c + 192*b*c^2 - 84*b^2 - 1344*b*c + 512*c^3 - 5376*c^2 + 2352*b + 18816*c - 21952 >= c - 8 ] (1, 9) start(a, b, c) -> eval(a - 1, b + 7*c - 21, c - 8) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 /\ b^3 + 21*b^2*c + 147*b*c^2 - 63*b^2 - 882*b*c + 343*c^3 - 3087*c^2 + 1323*b + 9261*c - 9261 >= c - 7 ] (1, 8) start(a, b, c) -> eval(a - 1, b + 6*c - 15, c - 7) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 /\ b^3 + 18*b^2*c + 108*b*c^2 - 45*b^2 - 540*b*c + 216*c^3 - 1620*c^2 + 675*b + 4050*c - 3375 >= c - 6 ] (1, 7) start(a, b, c) -> eval(a - 1, b + 5*c - 10, c - 6) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 /\ b^3 + 15*b^2*c + 75*b*c^2 - 30*b^2 - 300*b*c + 125*c^3 - 750*c^2 + 300*b + 1500*c - 1000 >= c - 5 ] (1, 6) start(a, b, c) -> eval(a - 1, b + 4*c - 6, c - 5) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 /\ b^3 + 12*b^2*c + 48*b*c^2 - 18*b^2 - 144*b*c + 64*c^3 - 288*c^2 + 108*b + 432*c - 216 >= c - 4 ] (1, 5) start(a, b, c) -> eval(a - 1, b + 3*c - 3, c - 4) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 /\ b^3 + 9*b^2*c + 27*b*c^2 - 9*b^2 - 54*b*c + 27*c^3 - 81*c^2 + 27*b + 81*c - 27 >= c - 3 ] (1, 4) start(a, b, c) -> eval(a - 1, b + 2*c - 1, c - 3) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 /\ b^3 + 6*b^2*c + 12*b*c^2 - 3*b^2 - 12*b*c + 8*c^3 - 12*c^2 + 3*b + 6*c - 1 >= c - 2 ] (1, 3) start(a, b, c) -> eval(a - 1, b + c, c - 2) [ a >= 0 /\ b^3 >= c /\ b^3 + 3*b^2*c + 3*b*c^2 + c^3 >= c - 1 ] (1, 2) start(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (a + 1, 1) eval(a, b, c) -> eval(a - 1, b, c - 1) [ a >= 0 /\ b^3 >= c ] (?, 1) eval(a, b, c) -> eval(a, b + c, c - 1) [ a >= 0 /\ b^3 >= c ] start location: start leaf cost: 0 Complexity upper bound ? Time: 5.722 sec (SMT: 5.442 sec)