unknown Initial ITS Start location: [1] Program variables: i x y z 0: [1] -> [2] : x'=nondet, T, cost: 1 1: [2] -> [3] : y'=nondet1, T, cost: 1 2: [3] -> [4] : z'=nondet2, T, cost: 1 3: [4] -> [5] : i'=nondet3, T, cost: 1 4: [5] -> [6] : -y+x < 0, cost: 1 13: [5] -> [13] : -y+x >= 0, cost: 1 5: [6] -> [7] : i'=1+i, T, cost: 1 6: [7] -> [9] : z-x > 0, cost: 1 9: [7] -> [11] : z-x <= 0, cost: 1 12: [8] -> [5] : T, cost: 1 7: [9] -> [10] : x'=1+x, T, cost: 1 8: [10] -> [8] : T, cost: 1 10: [11] -> [12] : z'=1+z, T, cost: 1 11: [12] -> [8] : T, cost: 1 Chained Linear Paths Start location: [1] Program variables: i x y z 16: [1] -> [5] : i'=nondet3, x'=nondet, y'=nondet1, z'=nondet2, T, cost: 1 13: [5] -> [13] : -y+x >= 0, cost: 1 17: [5] -> [7] : i'=1+i, -y+x < 0, cost: 1 20: [7] -> [8] : x'=1+x, z-x > 0, cost: 1 21: [7] -> [8] : z'=1+z, z-x <= 0, cost: 1 12: [8] -> [5] : T, cost: 1 Eliminating location [2] by chaining: Applied chaining First rule: [1] -> [2] : x'=nondet, T, cost: 1 Second rule: [2] -> [3] : y'=nondet1, T, cost: 1 New rule: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1 Applied deletion Removed the following rules: 0 1 Eliminating location [3] by chaining: Applied chaining First rule: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1 Second rule: [3] -> [4] : z'=nondet2, T, cost: 1 New rule: [1] -> [4] : x'=nondet, y'=nondet1, z'=nondet2, T, cost: 1 Applied deletion Removed the following rules: 2 14 Eliminating location [4] by chaining: Applied chaining First rule: [1] -> [4] : x'=nondet, y'=nondet1, z'=nondet2, T, cost: 1 Second rule: [4] -> [5] : i'=nondet3, T, cost: 1 New rule: [1] -> [5] : i'=nondet3, x'=nondet, y'=nondet1, z'=nondet2, T, cost: 1 Applied deletion Removed the following rules: 3 15 Eliminating location [6] by chaining: Applied chaining First rule: [5] -> [6] : -y+x < 0, cost: 1 Second rule: [6] -> [7] : i'=1+i, T, cost: 1 New rule: [5] -> [7] : i'=1+i, -y+x < 0, cost: 1 Applied deletion Removed the following rules: 4 5 Eliminating location [9] by chaining: Applied chaining First rule: [7] -> [9] : z-x > 0, cost: 1 Second rule: [9] -> [10] : x'=1+x, T, cost: 1 New rule: [7] -> [10] : x'=1+x, z-x > 0, cost: 1 Applied deletion Removed the following rules: 6 7 Eliminating location [11] by chaining: Applied chaining First rule: [7] -> [11] : z-x <= 0, cost: 1 Second rule: [11] -> [12] : z'=1+z, T, cost: 1 New rule: [7] -> [12] : z'=1+z, z-x <= 0, cost: 1 Applied deletion Removed the following rules: 9 10 Eliminating location [10] by chaining: Applied chaining First rule: [7] -> [10] : x'=1+x, z-x > 0, cost: 1 Second rule: [10] -> [8] : T, cost: 1 New rule: [7] -> [8] : x'=1+x, z-x > 0, cost: 1 Applied deletion Removed the following rules: 8 18 Eliminating location [12] by chaining: Applied chaining First rule: [7] -> [12] : z'=1+z, z-x <= 0, cost: 1 Second rule: [12] -> [8] : T, cost: 1 New rule: [7] -> [8] : z'=1+z, z-x <= 0, cost: 1 Applied deletion Removed the following rules: 11 19 Step with 16 Trace 16[T] Blocked [{}, {}] Step with 13 Trace 16[T], 13[(-y+x >= 0)] Blocked [{}, {}, {}] Backtrack Trace 16[T] Blocked [{}, {13[T]}] Step with 17 Trace 16[T], 17[(-y+x < 0)] Blocked [{}, {13[T]}, {}] Step with 20 Trace 16[T], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T]}, {}, {}] Step with 12 Trace 16[T], 17[(-y+x < 0)], 20[(z-x > 0)], 12[T] Blocked [{}, {13[T]}, {}, {}, {}] Accelerate Start location: [1] Program variables: i x y z 16: [1] -> [5] : i'=nondet3, x'=nondet, y'=nondet1, z'=nondet2, T, cost: 1 13: [5] -> [13] : -y+x >= 0, cost: 1 17: [5] -> [7] : i'=1+i, -y+x < 0, cost: 1 22: [5] -> [5] : i'=i+n, x'=x+n, (1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0), cost: 1 20: [7] -> [8] : x'=1+x, z-x > 0, cost: 1 21: [7] -> [8] : z'=1+z, z-x <= 0, cost: 1 12: [8] -> [5] : T, cost: 1 Loop Acceleration Original rule: [5] -> [5] : i'=1+i, x'=1+x, (-y+x < 0 /\ z-x > 0), cost: 1 New rule: [5] -> [5] : i'=i+n, x'=x+n, (1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0), cost: 1 y-x > 0 [0]: montonic decrease yields 1+y-x-n > 0 y-x > 0 [1]: eventual increase yields (1 <= 0 /\ y-x > 0) z-x > 0 [0]: montonic decrease yields 1+z-x-n > 0 z-x > 0 [1]: eventual increase yields (1 <= 0 /\ z-x > 0) Replacement map: {y-x > 0 -> 1+y-x-n > 0, z-x > 0 -> 1+z-x-n > 0} Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)] Blocked [{}, {13[T]}, {22[T]}] Step with 13 Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 13[(-y+x >= 0)] Blocked [{}, {13[T]}, {22[T]}, {}] Backtrack Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)] Blocked [{}, {13[T]}, {13[T], 22[T]}] Step with 17 Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)] Blocked [{}, {13[T]}, {13[T], 22[T]}, {}] Step with 20 Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T]}, {13[T], 22[T]}, {}, {}] Step with 12 Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 20[(z-x > 0)], 12[T] Blocked [{}, {13[T]}, {13[T], 22[T]}, {}, {}, {}] Covered Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T]}, {13[T], 22[T]}, {}, {12[T]}] Backtrack Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)] Blocked [{}, {13[T]}, {13[T], 22[T]}, {20[T]}] Step with 21 Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)] Blocked [{}, {13[T]}, {13[T], 22[T]}, {20[T]}, {}] Step with 12 Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)], 12[T] Blocked [{}, {13[T]}, {13[T], 22[T]}, {20[T]}, {}, {}] Accelerate Start location: [1] Program variables: i x y z 16: [1] -> [5] : i'=nondet3, x'=nondet, y'=nondet1, z'=nondet2, T, cost: 1 13: [5] -> [13] : -y+x >= 0, cost: 1 17: [5] -> [7] : i'=1+i, -y+x < 0, cost: 1 22: [5] -> [5] : i'=i+n, x'=x+n, (1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0), cost: 1 23: [5] -> [5] : i'=i+n2, z'=z+n2, (y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0), cost: 1 20: [7] -> [8] : x'=1+x, z-x > 0, cost: 1 21: [7] -> [8] : z'=1+z, z-x <= 0, cost: 1 12: [8] -> [5] : T, cost: 1 Loop Acceleration Original rule: [5] -> [5] : i'=1+i, z'=1+z, (-y+x < 0 /\ z-x <= 0), cost: 1 New rule: [5] -> [5] : i'=i+n2, z'=z+n2, (y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0), cost: 1 y-x > 0 [0]: monotonic increase yields y-x > 0 -z+x >= 0 [0]: montonic decrease yields 1-z-n2+x >= 0 -z+x >= 0 [1]: eventual increase yields (1 <= 0 /\ -z+x >= 0) Replacement map: {y-x > 0 -> y-x > 0, -z+x >= 0 -> 1-z-n2+x >= 0} Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)] Blocked [{}, {13[T]}, {13[T], 22[T]}, {23[T]}] Accelerate Start location: [1] Program variables: i x y z 16: [1] -> [5] : i'=nondet3, x'=nondet, y'=nondet1, z'=nondet2, T, cost: 1 13: [5] -> [13] : -y+x >= 0, cost: 1 17: [5] -> [7] : i'=1+i, -y+x < 0, cost: 1 22: [5] -> [5] : i'=i+n, x'=x+n, (1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0), cost: 1 23: [5] -> [5] : i'=i+n2, z'=z+n2, (y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0), cost: 1 24: [5] -> [5] : i'=i+n1*n3+n2*n3, x'=n1*n3+x, z'=z+n2*n3, (1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0), cost: 1 20: [7] -> [8] : x'=1+x, z-x > 0, cost: 1 21: [7] -> [8] : z'=1+z, z-x <= 0, cost: 1 12: [8] -> [5] : T, cost: 1 Loop Acceleration Original rule: [5] -> [5] : i'=i+n1+n2, x'=n1+x, z'=z+n2, (1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1-n1+y-x > 0 /\ -n1+y-x > 0 /\ 1+z-n1-x > 0), cost: 1 New rule: [5] -> [5] : i'=i+n1*n3+n2*n3, x'=n1*n3+x, z'=z+n2*n3, (1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0), cost: 1 1-z+n1-n2+x >= 0 [0]: monotonic increase yields 1-z+n1-n2+x >= 0, dependencies: -1+n1 >= 0 1+z-n1-x > 0 1-z+n1-n2+x >= 0 [1]: eventual decrease yields (1-z+n1-n2+x >= 0 /\ 1+n1*(-1+n3)-z+n1-n2-n2*(-1+n3)+x >= 0) 1-z+n1-n2+x >= 0 [2]: eventual increase yields (1-z+n1-n2+x >= 0 /\ -n1+n2 <= 0) -1+n1 >= 0 [0]: monotonic increase yields -1+n1 >= 0 -1+n2 >= 0 [0]: monotonic increase yields -1+n2 >= 0 1-n1+y-x > 0 [0]: montonic decrease yields 1-n1*(-1+n3)-n1+y-x > 0, dependencies: -1+n1 >= 0 1-n1+y-x > 0 [1]: eventual increase yields (n1 <= 0 /\ 1-n1+y-x > 0), dependencies: -1+n1 >= 0 -n1+y-x > 0 [0]: montonic decrease yields -n1*(-1+n3)-n1+y-x > 0, dependencies: -1+n1 >= 0 -n1+y-x > 0 [1]: eventual increase yields (n1 <= 0 /\ -n1+y-x > 0), dependencies: -1+n1 >= 0 1+z-n1-x > 0 [0]: eventual decrease yields (1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ 1+z-n1-x > 0) 1+z-n1-x > 0 [1]: eventual increase yields (n1-n2 <= 0 /\ 1+z-n1-x > 0) Replacement map: {1-z+n1-n2+x >= 0 -> 1-z+n1-n2+x >= 0, -1+n1 >= 0 -> -1+n1 >= 0, -1+n2 >= 0 -> -1+n2 >= 0, 1-n1+y-x > 0 -> 1-n1*(-1+n3)-n1+y-x > 0, -n1+y-x > 0 -> -n1*(-1+n3)-n1+y-x > 0, 1+z-n1-x > 0 -> (1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ 1+z-n1-x > 0)} Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)] Blocked [{}, {13[T]}, {24[T]}] Step with 17 Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)] Blocked [{}, {13[T]}, {13[T], 24[T]}, {}] Step with 20 Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T]}, {13[T], 24[T]}, {21[T]}, {}] Step with 12 Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)], 20[(z-x > 0)], 12[T] Blocked [{}, {13[T]}, {13[T], 24[T]}, {21[T]}, {}, {}] Covered Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T]}, {13[T], 24[T]}, {21[T]}, {12[T]}] Backtrack Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)] Blocked [{}, {13[T]}, {13[T], 24[T]}, {20[T], 21[T]}] Backtrack Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)] Blocked [{}, {13[T]}, {13[T], 17[T], 24[T]}] Step with 22 Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)] Blocked [{}, {13[T]}, {13[T], 17[T], 24[T]}, {22[T]}] Acceleration Failed marked recursive suffix as redundant Step with 23 Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)] Blocked [{}, {13[T]}, {13[T], 17[T], 24[T]}, {22[T]}, {23[T]}] Covered Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)] Blocked [{}, {13[T]}, {13[T], 17[T], 24[T]}, {22[T], 23[T]}] Step with 13 Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 13[(-y+x >= 0)] Blocked [{}, {13[T]}, {13[T], 17[T], 24[T]}, {22[T], 23[T], 24[T]}, {}] Backtrack Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)] Blocked [{}, {13[T]}, {13[T], 17[T], 24[T]}, {13[T], 22[T], 23[T], 24[T]}] Step with 17 Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)] Blocked [{}, {13[T]}, {13[T], 17[T], 24[T]}, {13[T], 22[T], 23[T], 24[T]}, {}] Step with 21 Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)] Blocked [{}, {13[T]}, {13[T], 17[T], 24[T]}, {13[T], 22[T], 23[T], 24[T]}, {20[T]}, {}] Step with 12 Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)], 12[T] Blocked [{}, {13[T]}, {13[T], 17[T], 24[T]}, {13[T], 22[T], 23[T], 24[T]}, {20[T]}, {}, {}] Covered Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)] Blocked [{}, {13[T]}, {13[T], 17[T], 24[T]}, {13[T], 22[T], 23[T], 24[T]}, {20[T]}, {12[T]}] Backtrack Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)] Blocked [{}, {13[T]}, {13[T], 17[T], 24[T]}, {13[T], 22[T], 23[T], 24[T]}, {20[T], 21[T]}] Backtrack Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)] Blocked [{}, {13[T]}, {13[T], 17[T], 24[T]}, {13[T], 17[T], 22[T], 23[T], 24[T]}] Backtrack Trace 16[T], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)] Blocked [{}, {13[T]}, {13[T], 17[T], 22[T], 24[T]}] Backtrack Trace 16[T] Blocked [{}, {13[T], 24[T]}] Step with 17 Trace 16[T], 17[(-y+x < 0)] Blocked [{}, {13[T], 24[T]}, {}] Step with 21 Trace 16[T], 17[(-y+x < 0)], 21[(z-x <= 0)] Blocked [{}, {13[T], 24[T]}, {}, {}] Step with 12 Trace 16[T], 17[(-y+x < 0)], 21[(z-x <= 0)], 12[T] Blocked [{}, {13[T], 24[T]}, {}, {}, {}] Covered Trace 16[T], 17[(-y+x < 0)], 21[(z-x <= 0)] Blocked [{}, {13[T], 24[T]}, {}, {12[T]}] Backtrack Trace 16[T], 17[(-y+x < 0)] Blocked [{}, {13[T], 24[T]}, {21[T]}] Step with 20 Trace 16[T], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T], 24[T]}, {21[T]}, {}] Step with 12 Trace 16[T], 17[(-y+x < 0)], 20[(z-x > 0)], 12[T] Blocked [{}, {13[T], 24[T]}, {21[T]}, {}, {}] Covered Trace 16[T], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T], 24[T]}, {21[T]}, {12[T]}] Backtrack Trace 16[T], 17[(-y+x < 0)] Blocked [{}, {13[T], 24[T]}, {20[T], 21[T]}] Backtrack Trace 16[T] Blocked [{}, {13[T], 17[T], 24[T]}] Step with 22 Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 17[T], 24[T]}, {22[T]}] Step with 23 Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)] Blocked [{}, {13[T], 17[T], 24[T]}, {22[T]}, {23[T]}] Covered Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 17[T], 24[T]}, {22[T], 23[T]}] Step with 24 Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)] Blocked [{}, {13[T], 17[T], 24[T]}, {22[T], 23[T]}, {24[T]}] Covered Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 17[T], 24[T]}, {22[T], 23[T], 24[T]}] Step with 13 Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 13[(-y+x >= 0)] Blocked [{}, {13[T], 17[T], 24[T]}, {22[T], 23[T], 24[T]}, {}] Backtrack Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 17[T], 24[T]}, {13[T], 22[T], 23[T], 24[T]}] Step with 17 Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)] Blocked [{}, {13[T], 17[T], 24[T]}, {13[T], 22[T], 23[T], 24[T]}, {}] Step with 20 Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T], 17[T], 24[T]}, {13[T], 22[T], 23[T], 24[T]}, {}, {}] Step with 12 Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 20[(z-x > 0)], 12[T] Blocked [{}, {13[T], 17[T], 24[T]}, {13[T], 22[T], 23[T], 24[T]}, {}, {}, {}] Covered Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T], 17[T], 24[T]}, {13[T], 22[T], 23[T], 24[T]}, {}, {12[T]}] Backtrack Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)] Blocked [{}, {13[T], 17[T], 24[T]}, {13[T], 22[T], 23[T], 24[T]}, {20[T]}] Step with 21 Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)] Blocked [{}, {13[T], 17[T], 24[T]}, {13[T], 22[T], 23[T], 24[T]}, {20[T]}, {}] Step with 12 Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)], 12[T] Blocked [{}, {13[T], 17[T], 24[T]}, {13[T], 22[T], 23[T], 24[T]}, {20[T]}, {}, {}] Covered Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)] Blocked [{}, {13[T], 17[T], 24[T]}, {13[T], 22[T], 23[T], 24[T]}, {20[T]}, {12[T]}] Backtrack Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)], 17[(-y+x < 0)] Blocked [{}, {13[T], 17[T], 24[T]}, {13[T], 22[T], 23[T], 24[T]}, {20[T], 21[T]}] Backtrack Trace 16[T], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 17[T], 24[T]}, {13[T], 17[T], 22[T], 23[T], 24[T]}] Backtrack Trace 16[T] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}] Step with 23 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {23[T]}] Step with 24 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {23[T]}, {24[T]}] Acceleration Failed marked recursive suffix as redundant Step with 17 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {23[T]}, {13[T], 24[T]}, {}] Step with 20 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {23[T]}, {13[T], 24[T]}, {21[T]}, {}] Step with 12 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)], 20[(z-x > 0)], 12[T] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {23[T]}, {13[T], 24[T]}, {21[T]}, {}, {}] Covered Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {23[T]}, {13[T], 24[T]}, {21[T]}, {12[T]}] Backtrack Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {23[T]}, {13[T], 24[T]}, {20[T], 21[T]}] Backtrack Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {23[T]}, {13[T], 17[T], 24[T]}] Step with 22 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {23[T]}, {13[T], 17[T], 24[T]}, {22[T]}] Accelerate Start location: [1] Program variables: i x y z 16: [1] -> [5] : i'=nondet3, x'=nondet, y'=nondet1, z'=nondet2, T, cost: 1 13: [5] -> [13] : -y+x >= 0, cost: 1 17: [5] -> [7] : i'=1+i, -y+x < 0, cost: 1 22: [5] -> [5] : i'=i+n, x'=x+n, (1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0), cost: 1 23: [5] -> [5] : i'=i+n2, z'=z+n2, (y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0), cost: 1 24: [5] -> [5] : i'=i+n1*n3+n2*n3, x'=n1*n3+x, z'=z+n2*n3, (1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0), cost: 1 25: [5] -> [5] : i'=i+n33*n13*n7+n26*n7+n7*n+n33*n7*n27, x'=n33*n13*n7+n7*n+x, z'=n26*n7+z+n33*n7*n27, (-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -1+n26 >= 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0 /\ -1+n13 >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0), cost: 1 20: [7] -> [8] : x'=1+x, z-x > 0, cost: 1 21: [7] -> [8] : z'=1+z, z-x <= 0, cost: 1 12: [8] -> [5] : T, cost: 1 Loop Acceleration Original rule: [5] -> [5] : i'=n26+i+n33*n27+n33*n13+n, x'=n33*n13+x+n, z'=n26+n33*n27+z, (-1+n26 >= 0 /\ -(-1+n33)*n13-n13+y-x > 0 /\ y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n33*n13+y-x-n > 0 /\ 1-(-1+n33)*n13-n13+y-x > 0 /\ -1+n13 >= 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ 1-n26-z+n13-n27+x >= 0 /\ -1+n >= 0 /\ -1+n27 >= 0), cost: 1 New rule: [5] -> [5] : i'=i+n33*n13*n7+n26*n7+n7*n+n33*n7*n27, x'=n33*n13*n7+n7*n+x, z'=n26*n7+z+n33*n7*n27, (-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -1+n26 >= 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0 /\ -1+n13 >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0), cost: 1 -1+n26 >= 0 [0]: monotonic increase yields -1+n26 >= 0 -(-1+n33)*n13-n13+y-x > 0 [0]: montonic decrease yields -n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0, dependencies: 1-n33*n13+y-x-n > 0 -1+n >= 0 -(-1+n33)*n13-n13+y-x > 0 [1]: eventual decrease yields (-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -(-1+n33)*n13-n13+y-x > 0) -(-1+n33)*n13-n13+y-x > 0 [2]: eventual increase yields (-(-1+n33)*n13-n13+y-x > 0 /\ n33*n13+n <= 0) y-x > 0 [0]: montonic decrease yields -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0, dependencies: -1+n13 >= 0 -1+n33 >= 0 -1+n >= 0 y-x > 0 [1]: eventual decrease yields (y-x > 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0) y-x > 0 [2]: eventual increase yields (y-x > 0 /\ n33*n13+n <= 0) 1-n26-z+x >= 0 [0]: eventual decrease yields (1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0) 1-n26-z+x >= 0 [1]: eventual increase yields (1-n26-z+x >= 0 /\ n26+n33*n27-n33*n13-n <= 0) 1-n33*n13+y-x-n > 0 [0]: montonic decrease yields 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0, dependencies: y-x > 0 1-n33*n13+y-x-n > 0 [1]: eventual increase yields (1-n33*n13+y-x-n > 0 /\ n33*n13+n <= 0) 1-(-1+n33)*n13-n13+y-x > 0 [0]: montonic decrease yields 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0, dependencies: -(-1+n33)*n13-n13+y-x > 0 1-(-1+n33)*n13-n13+y-x > 0 [1]: eventual increase yields (1-(-1+n33)*n13-n13+y-x > 0 /\ n33*n13+n <= 0) -1+n13 >= 0 [0]: monotonic increase yields -1+n13 >= 0 1+n26+n33*n27+z-n33*n13-x-n > 0 [0]: monotonic increase yields 1+n26+n33*n27+z-n33*n13-x-n > 0, dependencies: -1+n26 >= 0 1-n26-z+x >= 0 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 [0]: monotonic increase yields 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0, dependencies: -1+n26 >= 0 1-n26-z+x >= 0 1+n26+n33*n27+z-n33*n13-x-n > 0 -1+n33 >= 0 [0]: monotonic increase yields -1+n33 >= 0 1+n26+z-n13-x > 0 [0]: monotonic increase yields 1+n26+z-n13-x > 0, dependencies: -1+n26 >= 0 1-n26-z+x >= 0 1+n26+n33*n27+z-n33*n13-x-n > 0 1-n26-z+n13-n27+x >= 0 [0]: montonic decrease yields 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0, dependencies: -1+n26 >= 0 1-n26-z+x >= 0 1+n26+n33*n27+z-n33*n13-x-n > 0 1-n26-z+n13-n27+x >= 0 [1]: eventual increase yields (n26+n33*n27-n33*n13-n <= 0 /\ 1-n26-z+n13-n27+x >= 0) -1+n >= 0 [0]: monotonic increase yields -1+n >= 0 -1+n27 >= 0 [0]: monotonic increase yields -1+n27 >= 0 Replacement map: {-1+n26 >= 0 -> -1+n26 >= 0, -(-1+n33)*n13-n13+y-x > 0 -> -n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0, y-x > 0 -> -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0, 1-n26-z+x >= 0 -> (1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0), 1-n33*n13+y-x-n > 0 -> 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0, 1-(-1+n33)*n13-n13+y-x > 0 -> 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0, -1+n13 >= 0 -> -1+n13 >= 0, 1+n26+n33*n27+z-n33*n13-x-n > 0 -> 1+n26+n33*n27+z-n33*n13-x-n > 0, 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 -> 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0, -1+n33 >= 0 -> -1+n33 >= 0, 1+n26+z-n13-x > 0 -> 1+n26+z-n13-x > 0, 1-n26-z+n13-n27+x >= 0 -> 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0, -1+n >= 0 -> -1+n >= 0, -1+n27 >= 0 -> -1+n27 >= 0} Trace 16[T], 25[(-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -1+n26 >= 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0 /\ -1+n13 >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {25[T]}] Step with 13 Trace 16[T], 25[(-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -1+n26 >= 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0 /\ -1+n13 >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0)], 13[(-y+x >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {25[T]}, {}] Backtrack Trace 16[T], 25[(-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -1+n26 >= 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0 /\ -1+n13 >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {13[T], 25[T]}] Step with 17 Trace 16[T], 25[(-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -1+n26 >= 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0 /\ -1+n13 >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0)], 17[(-y+x < 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {13[T], 25[T]}, {}] Step with 21 Trace 16[T], 25[(-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -1+n26 >= 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0 /\ -1+n13 >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {13[T], 25[T]}, {20[T]}, {}] Step with 12 Trace 16[T], 25[(-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -1+n26 >= 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0 /\ -1+n13 >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)], 12[T] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {13[T], 25[T]}, {20[T]}, {}, {}] Covered Trace 16[T], 25[(-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -1+n26 >= 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0 /\ -1+n13 >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {13[T], 25[T]}, {20[T]}, {12[T]}] Backtrack Trace 16[T], 25[(-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -1+n26 >= 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0 /\ -1+n13 >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0)], 17[(-y+x < 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {13[T], 25[T]}, {20[T], 21[T]}] Backtrack Trace 16[T], 25[(-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -1+n26 >= 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0 /\ -1+n13 >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {13[T], 17[T], 25[T]}] Step with 23 Trace 16[T], 25[(-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -1+n26 >= 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0 /\ -1+n13 >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0)], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {13[T], 17[T], 22[T], 25[T]}, {23[T]}] Covered Trace 16[T], 25[(-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -1+n26 >= 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0 /\ -1+n13 >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T]}, {13[T], 17[T], 22[T], 23[T], 25[T]}] Backtrack Trace 16[T] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}] Step with 23 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {23[T]}] Step with 24 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {23[T]}, {24[T]}] Step with 17 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {23[T]}, {13[T], 24[T], 25[T]}, {}] Step with 20 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {23[T]}, {13[T], 24[T], 25[T]}, {21[T]}, {}] Step with 12 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)], 20[(z-x > 0)], 12[T] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {23[T]}, {13[T], 24[T], 25[T]}, {21[T]}, {}, {}] Covered Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {23[T]}, {13[T], 24[T], 25[T]}, {21[T]}, {12[T]}] Backtrack Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {23[T]}, {13[T], 24[T], 25[T]}, {20[T], 21[T]}] Backtrack Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {23[T]}, {13[T], 17[T], 24[T], 25[T]}] Step with 22 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {23[T]}, {13[T], 17[T], 24[T], 25[T]}, {22[T]}] Covered Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {23[T]}, {13[T], 17[T], 22[T], 24[T], 25[T]}] Backtrack Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {23[T], 24[T]}] Step with 22 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {23[T], 24[T]}, {22[T]}] Accelerate Start location: [1] Program variables: i x y z 16: [1] -> [5] : i'=nondet3, x'=nondet, y'=nondet1, z'=nondet2, T, cost: 1 13: [5] -> [13] : -y+x >= 0, cost: 1 17: [5] -> [7] : i'=1+i, -y+x < 0, cost: 1 22: [5] -> [5] : i'=i+n, x'=x+n, (1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0), cost: 1 23: [5] -> [5] : i'=i+n2, z'=z+n2, (y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0), cost: 1 24: [5] -> [5] : i'=i+n1*n3+n2*n3, x'=n1*n3+x, z'=z+n2*n3, (1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0), cost: 1 25: [5] -> [5] : i'=i+n33*n13*n7+n26*n7+n7*n+n33*n7*n27, x'=n33*n13*n7+n7*n+x, z'=n26*n7+z+n33*n7*n27, (-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -1+n26 >= 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0 /\ -1+n13 >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0), cost: 1 26: [5] -> [5] : i'=n15*n+i+n15*n29, x'=n15*n+x, z'=n15*n29+z, (1+n29+z-x-n > 0 /\ 1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ y-x-(-1+n15)*n > 0 /\ 1+y-x-(-1+n15)*n-n > 0 /\ -1+n15 >= 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0), cost: 1 20: [7] -> [8] : x'=1+x, z-x > 0, cost: 1 21: [7] -> [8] : z'=1+z, z-x <= 0, cost: 1 12: [8] -> [5] : T, cost: 1 Loop Acceleration Original rule: [5] -> [5] : i'=i+n29+n, x'=x+n, z'=n29+z, (y-x > 0 /\ 1+n29+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0), cost: 1 New rule: [5] -> [5] : i'=n15*n+i+n15*n29, x'=n15*n+x, z'=n15*n29+z, (1+n29+z-x-n > 0 /\ 1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ y-x-(-1+n15)*n > 0 /\ 1+y-x-(-1+n15)*n-n > 0 /\ -1+n15 >= 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0), cost: 1 y-x > 0 [0]: montonic decrease yields y-x-(-1+n15)*n > 0, dependencies: -1+n >= 0 y-x > 0 [1]: eventual decrease yields (y-x > 0 /\ y-x-(-1+n15)*n > 0), dependencies: -1+n >= 0 y-x > 0 [2]: eventual increase yields (y-x > 0 /\ n <= 0), dependencies: -1+n >= 0 1+n29+z-x-n > 0 [0]: monotonic increase yields 1+n29+z-x-n > 0, dependencies: -1+n29 >= 0 1-n29-z+x >= 0 1+n29+z-x-n > 0 [1]: eventual decrease yields (1+n29+z-x-n > 0 /\ 1+n29+z+n29*(-1+n15)-x-(-1+n15)*n-n > 0) 1+n29+z-x-n > 0 [2]: eventual increase yields (1+n29+z-x-n > 0 /\ -n29+n <= 0) 1+y-x-n > 0 [0]: montonic decrease yields 1+y-x-(-1+n15)*n-n > 0, dependencies: y-x > 0 1+y-x-n > 0 [1]: eventual decrease yields (1+y-x-n > 0 /\ 1+y-x-(-1+n15)*n-n > 0), dependencies: -1+n >= 0 1+y-x-n > 0 [2]: eventual increase yields (1+y-x-n > 0 /\ n <= 0), dependencies: -1+n >= 0 -1+n29 >= 0 [0]: monotonic increase yields -1+n29 >= 0 1-n29-z+x >= 0 [0]: eventual decrease yields (1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ 1-n29-z+x >= 0) 1-n29-z+x >= 0 [1]: eventual increase yields (1-n29-z+x >= 0 /\ n29-n <= 0) -1+n >= 0 [0]: monotonic increase yields -1+n >= 0 Replacement map: {y-x > 0 -> y-x-(-1+n15)*n > 0, 1+n29+z-x-n > 0 -> 1+n29+z-x-n > 0, 1+y-x-n > 0 -> 1+y-x-(-1+n15)*n-n > 0, -1+n29 >= 0 -> -1+n29 >= 0, 1-n29-z+x >= 0 -> (1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ 1-n29-z+x >= 0), -1+n >= 0 -> -1+n >= 0} Trace 16[T], 26[(1+n29+z-x-n > 0 /\ 1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ y-x-(-1+n15)*n > 0 /\ 1+y-x-(-1+n15)*n-n > 0 /\ -1+n15 >= 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {26[T]}] Step with 13 Trace 16[T], 26[(1+n29+z-x-n > 0 /\ 1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ y-x-(-1+n15)*n > 0 /\ 1+y-x-(-1+n15)*n-n > 0 /\ -1+n15 >= 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0)], 13[(-y+x >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {26[T]}, {}] Backtrack Trace 16[T], 26[(1+n29+z-x-n > 0 /\ 1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ y-x-(-1+n15)*n > 0 /\ 1+y-x-(-1+n15)*n-n > 0 /\ -1+n15 >= 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {13[T], 26[T]}] Step with 17 Trace 16[T], 26[(1+n29+z-x-n > 0 /\ 1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ y-x-(-1+n15)*n > 0 /\ 1+y-x-(-1+n15)*n-n > 0 /\ -1+n15 >= 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0)], 17[(-y+x < 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {13[T], 26[T]}, {}] Step with 21 Trace 16[T], 26[(1+n29+z-x-n > 0 /\ 1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ y-x-(-1+n15)*n > 0 /\ 1+y-x-(-1+n15)*n-n > 0 /\ -1+n15 >= 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {13[T], 26[T]}, {20[T]}, {}] Step with 12 Trace 16[T], 26[(1+n29+z-x-n > 0 /\ 1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ y-x-(-1+n15)*n > 0 /\ 1+y-x-(-1+n15)*n-n > 0 /\ -1+n15 >= 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)], 12[T] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {13[T], 26[T]}, {20[T]}, {}, {}] Covered Trace 16[T], 26[(1+n29+z-x-n > 0 /\ 1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ y-x-(-1+n15)*n > 0 /\ 1+y-x-(-1+n15)*n-n > 0 /\ -1+n15 >= 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {13[T], 26[T]}, {20[T]}, {12[T]}] Backtrack Trace 16[T], 26[(1+n29+z-x-n > 0 /\ 1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ y-x-(-1+n15)*n > 0 /\ 1+y-x-(-1+n15)*n-n > 0 /\ -1+n15 >= 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0)], 17[(-y+x < 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {13[T], 26[T]}, {20[T], 21[T]}] Backtrack Trace 16[T], 26[(1+n29+z-x-n > 0 /\ 1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ y-x-(-1+n15)*n > 0 /\ 1+y-x-(-1+n15)*n-n > 0 /\ -1+n15 >= 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {13[T], 17[T], 26[T]}] Step with 23 Trace 16[T], 26[(1+n29+z-x-n > 0 /\ 1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ y-x-(-1+n15)*n > 0 /\ 1+y-x-(-1+n15)*n-n > 0 /\ -1+n15 >= 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0)], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {13[T], 17[T], 22[T], 26[T]}, {23[T]}] Covered Trace 16[T], 26[(1+n29+z-x-n > 0 /\ 1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ y-x-(-1+n15)*n > 0 /\ 1+y-x-(-1+n15)*n-n > 0 /\ -1+n15 >= 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {13[T], 17[T], 22[T], 23[T], 26[T]}] Step with 25 Trace 16[T], 26[(1+n29+z-x-n > 0 /\ 1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ y-x-(-1+n15)*n > 0 /\ 1+y-x-(-1+n15)*n-n > 0 /\ -1+n15 >= 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0)], 25[(-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -1+n26 >= 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0 /\ -1+n13 >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {13[T], 17[T], 22[T], 23[T], 24[T], 26[T]}, {25[T]}] Covered Trace 16[T], 26[(1+n29+z-x-n > 0 /\ 1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ y-x-(-1+n15)*n > 0 /\ 1+y-x-(-1+n15)*n-n > 0 /\ -1+n15 >= 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T]}, {13[T], 17[T], 22[T], 23[T], 24[T], 25[T], 26[T]}] Backtrack Trace 16[T] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}] Step with 23 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {23[T]}] Step with 24 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {23[T]}, {24[T]}] Step with 17 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {23[T]}, {13[T], 24[T], 25[T], 26[T]}, {}] Step with 20 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {23[T]}, {13[T], 24[T], 25[T], 26[T]}, {21[T]}, {}] Step with 12 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)], 20[(z-x > 0)], 12[T] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {23[T]}, {13[T], 24[T], 25[T], 26[T]}, {21[T]}, {}, {}] Covered Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {23[T]}, {13[T], 24[T], 25[T], 26[T]}, {21[T]}, {12[T]}] Backtrack Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 17[(-y+x < 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {23[T]}, {13[T], 24[T], 25[T], 26[T]}, {20[T], 21[T]}] Backtrack Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {23[T]}, {13[T], 17[T], 24[T], 25[T], 26[T]}] Step with 22 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {23[T]}, {13[T], 17[T], 24[T], 25[T], 26[T]}, {22[T]}] Covered Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 24[(1-z+n1-n2+x >= 0 /\ -1+n1 >= 0 /\ 1-n1*(-1+n3)+z-n1+n2*(-1+n3)-x > 0 /\ -1+n2 >= 0 /\ 1-n1*(-1+n3)-n1+y-x > 0 /\ -n1*(-1+n3)-n1+y-x > 0 /\ -1+n3 >= 0 /\ 1+z-n1-x > 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {23[T]}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}] Backtrack Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {23[T], 24[T]}] Step with 22 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 22[(1+z-x-n > 0 /\ 1+y-x-n > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {23[T], 24[T]}, {22[T]}] Covered Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {22[T], 23[T], 24[T]}] Step with 25 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 25[(-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ -1+n26 >= 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-n33*n13+y-x-n > 0 /\ 1-n33*(-1+n7)*n13-(-1+n7)*n-(-1+n33)*n13-n13+y-x > 0 /\ 1-n26-z+x >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)-n33*(-1+n7)*n27+x >= 0 /\ -1+n13 >= 0 /\ 1-n26+n33*(-1+n7)*n13+(-1+n7)*n-z-n26*(-1+n7)+n13-n33*(-1+n7)*n27-n27+x >= 0 /\ -n33*(-1+n7)*n13-(-1+n7)*n+y-x > 0 /\ 1+n26+n33*n27+z-n33*n13-x-n > 0 /\ 1+n26+(-1+n33)*n27+z-(-1+n33)*n13-n13-x > 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1+n26+z-n13-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {22[T], 23[T], 24[T]}, {25[T]}] Covered Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {22[T], 23[T], 24[T], 25[T]}] Step with 26 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 26[(1+n29+z-x-n > 0 /\ 1-n29-z-n29*(-1+n15)+x+(-1+n15)*n >= 0 /\ y-x-(-1+n15)*n > 0 /\ 1+y-x-(-1+n15)*n-n > 0 /\ -1+n15 >= 0 /\ -1+n29 >= 0 /\ 1-n29-z+x >= 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {22[T], 23[T], 24[T], 25[T]}, {26[T]}] Covered Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {22[T], 23[T], 24[T], 25[T], 26[T]}] Step with 17 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 17[(-y+x < 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {13[T], 22[T], 23[T], 24[T], 25[T], 26[T]}, {}] Step with 20 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {13[T], 22[T], 23[T], 24[T], 25[T], 26[T]}, {}, {}] Step with 12 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 17[(-y+x < 0)], 20[(z-x > 0)], 12[T] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {13[T], 22[T], 23[T], 24[T], 25[T], 26[T]}, {}, {}, {}] Covered Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 17[(-y+x < 0)], 20[(z-x > 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {13[T], 22[T], 23[T], 24[T], 25[T], 26[T]}, {}, {12[T]}] Backtrack Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 17[(-y+x < 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {13[T], 22[T], 23[T], 24[T], 25[T], 26[T]}, {20[T]}] Step with 21 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {13[T], 22[T], 23[T], 24[T], 25[T], 26[T]}, {20[T]}, {}] Step with 12 Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)], 12[T] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {13[T], 22[T], 23[T], 24[T], 25[T], 26[T]}, {20[T]}, {}, {}] Covered Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 17[(-y+x < 0)], 21[(z-x <= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {13[T], 22[T], 23[T], 24[T], 25[T], 26[T]}, {20[T]}, {12[T]}] Backtrack Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)], 17[(-y+x < 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {13[T], 22[T], 23[T], 24[T], 25[T], 26[T]}, {20[T], 21[T]}] Backtrack Trace 16[T], 23[(y-x > 0 /\ -1+n2 >= 0 /\ 1-z-n2+x >= 0)] Blocked [{}, {13[T], 17[T], 22[T], 24[T], 25[T], 26[T]}, {13[T], 17[T], 22[T], 23[T], 24[T], 25[T], 26[T]}] Backtrack Trace 16[T] Blocked [{}, {13[T], 17[T], 22[T], 23[T], 24[T], 25[T], 26[T]}] Backtrack Trace Blocked [{16[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b