unknown Initial ITS Start location: [1] Program variables: x y 0: [1] -> [2] : x'=nondet, T, cost: 1 1: [2] -> [3] : y'=nondet1, T, cost: 1 2: [3] -> [4] : x > 0, cost: 1 6: [3] -> [7] : x <= 0, cost: 1 3: [4] -> [5] : x'=y+x, T, cost: 1 4: [5] -> [6] : y'=-1-y, T, cost: 1 5: [6] -> [3] : T, cost: 1 Chained Linear Paths Start location: [1] Program variables: x y 7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1 6: [3] -> [7] : x <= 0, cost: 1 10: [3] -> [3] : x'=y+x, y'=-1-y, x > 0, 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 [4] by chaining: Applied chaining First rule: [3] -> [4] : x > 0, cost: 1 Second rule: [4] -> [5] : x'=y+x, T, cost: 1 New rule: [3] -> [5] : x'=y+x, x > 0, cost: 1 Applied deletion Removed the following rules: 2 3 Eliminating location [5] by chaining: Applied chaining First rule: [3] -> [5] : x'=y+x, x > 0, cost: 1 Second rule: [5] -> [6] : y'=-1-y, T, cost: 1 New rule: [3] -> [6] : x'=y+x, y'=-1-y, x > 0, cost: 1 Applied deletion Removed the following rules: 4 8 Eliminating location [6] by chaining: Applied chaining First rule: [3] -> [6] : x'=y+x, y'=-1-y, x > 0, cost: 1 Second rule: [6] -> [3] : T, cost: 1 New rule: [3] -> [3] : x'=y+x, y'=-1-y, x > 0, cost: 1 Applied deletion Removed the following rules: 5 9 Unrolled Loops Start location: [1] Program variables: x y 7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1 6: [3] -> [7] : x <= 0, cost: 1 10: [3] -> [3] : x'=y+x, y'=-1-y, x > 0, cost: 1 11: [3] -> [3] : x'=-1+x, (y+x > 0 /\ x > 0), cost: 1 Unrolling Original rule: [3] -> [3] : x'=y+x, y'=-1-y, x > 0, cost: 1 New rule: [3] -> [3] : x'=-1+x, y'=y, (y+x > 0 /\ x > 0), cost: 1 Removed Trivial Updates Original rule: [3] -> [3] : x'=-1+x, y'=y, (y+x > 0 /\ x > 0), cost: 1 New rule: [3] -> [3] : x'=-1+x, (y+x > 0 /\ x > 0), cost: 1 Step with 7 Trace 7[T] Blocked [{}, {}] Step with 6 Trace 7[T], 6[(x <= 0)] Blocked [{}, {}, {}] Backtrack Trace 7[T] Blocked [{}, {6[T]}] Step with 10 Trace 7[T], 10[(x > 0)] Blocked [{}, {6[T]}, {}] Accelerate Start location: [1] Program variables: x y 7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1 6: [3] -> [7] : x <= 0, cost: 1 10: [3] -> [3] : x'=y+x, y'=-1-y, x > 0, cost: 1 11: [3] -> [3] : x'=-1+x, (y+x > 0 /\ x > 0), cost: 1 12: [3] -> [3] : x'=-n+x, (1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0), cost: 1 unrolling Original rule: [3] -> [3] : x'=y+x, y'=-1-y, (x > 0), cost: 1 New rule: [3] -> [3] : x'=-1+x, y'=y, (y+x > 0 /\ x > 0), cost: 1 Loop Acceleration Original rule: [3] -> [3] : x'=-1+x, y'=y, (y+x > 0 /\ x > 0), cost: 1 New rule: [3] -> [3] : x'=-n+x, y'=y, (1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0), cost: 1 y+x > 0 [0]: montonic decrease yields 1-n+y+x > 0 y+x > 0 [1]: eventual increase yields (1 <= 0 /\ y+x > 0) x > 0 [0]: montonic decrease yields 1-n+x > 0 x > 0 [1]: eventual increase yields (1 <= 0 /\ x > 0) Replacement map: {y+x > 0 -> 1-n+y+x > 0, x > 0 -> 1-n+x > 0} Removed Trivial Updates Original rule: [3] -> [3] : x'=-n+x, y'=y, (1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0), cost: 1 New rule: [3] -> [3] : x'=-n+x, (1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0), cost: 1 Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T]}, {10[T], 12[T]}] Step with 6 Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)], 6[(x <= 0)] Blocked [{}, {6[T]}, {10[T], 12[T]}, {}] Backtrack Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T]}, {6[T], 10[T], 12[T]}] Step with 11 Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)], 11[(y+x > 0 /\ x > 0)] Blocked [{}, {6[T]}, {6[T], 10[T], 12[T]}, {}] Accelerate Start location: [1] Program variables: x y 7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1 6: [3] -> [7] : x <= 0, cost: 1 10: [3] -> [3] : x'=y+x, y'=-1-y, x > 0, cost: 1 11: [3] -> [3] : x'=-1+x, (y+x > 0 /\ x > 0), cost: 1 12: [3] -> [3] : x'=-n+x, (1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0), cost: 1 13: [3] -> [3] : x'=-n2+x, (1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0), cost: 1 Loop Acceleration Original rule: [3] -> [3] : x'=-1+x, (y+x > 0 /\ x > 0), cost: 1 New rule: [3] -> [3] : x'=-n2+x, (1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0), cost: 1 y+x > 0 [0]: montonic decrease yields 1-n2+y+x > 0 y+x > 0 [1]: eventual increase yields (1 <= 0 /\ y+x > 0) x > 0 [0]: montonic decrease yields 1-n2+x > 0 x > 0 [1]: eventual increase yields (1 <= 0 /\ x > 0) Replacement map: {y+x > 0 -> 1-n2+y+x > 0, x > 0 -> 1-n2+x > 0} Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T]}, {6[T], 10[T], 12[T]}, {11[T], 13[T]}] Accelerate Start location: [1] Program variables: x y 7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1 6: [3] -> [7] : x <= 0, cost: 1 10: [3] -> [3] : x'=y+x, y'=-1-y, x > 0, cost: 1 11: [3] -> [3] : x'=-1+x, (y+x > 0 /\ x > 0), cost: 1 12: [3] -> [3] : x'=-n+x, (1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0), cost: 1 13: [3] -> [3] : x'=-n2+x, (1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0), cost: 1 14: [3] -> [3] : x'=-n2*n3-n3*n1+x, (-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0), cost: 1 Loop Acceleration Original rule: [3] -> [3] : x'=-n2-n1+x, (1-n1+y+x > 0 /\ -1+n1 >= 0 /\ 1-n1+x > 0 /\ -1+n2 >= 0 /\ 1-n2-n1+x > 0 /\ 1-n2-n1+y+x > 0), cost: 1 New rule: [3] -> [3] : x'=-n2*n3-n3*n1+x, (-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0), cost: 1 1-n1+y+x > 0 [0]: montonic decrease yields 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0, dependencies: -1+n1 >= 0 -1+n2 >= 0 1-n1+y+x > 0 [1]: eventual decrease yields (1-n1+y+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0), dependencies: -1+n1 >= 0 -1+n2 >= 0 1-n1+y+x > 0 [2]: eventual increase yields (1-n1+y+x > 0 /\ n2+n1 <= 0), dependencies: -1+n1 >= 0 -1+n2 >= 0 -1+n1 >= 0 [0]: monotonic increase yields -1+n1 >= 0 1-n1+x > 0 [0]: montonic decrease yields 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0, dependencies: -1+n1 >= 0 -1+n2 >= 0 1-n1+x > 0 [1]: eventual decrease yields (1-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0), dependencies: -1+n1 >= 0 -1+n2 >= 0 1-n1+x > 0 [2]: eventual increase yields (1-n1+x > 0 /\ n2+n1 <= 0), dependencies: -1+n1 >= 0 -1+n2 >= 0 -1+n2 >= 0 [0]: monotonic increase yields -1+n2 >= 0 1-n2-n1+x > 0 [0]: montonic decrease yields 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0, dependencies: -1+n1 >= 0 -1+n2 >= 0 1-n2-n1+x > 0 [1]: eventual increase yields (1-n2-n1+x > 0 /\ n2+n1 <= 0), dependencies: -1+n1 >= 0 -1+n2 >= 0 1-n2-n1+y+x > 0 [0]: montonic decrease yields 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0, dependencies: -1+n1 >= 0 -1+n2 >= 0 1-n2-n1+y+x > 0 [1]: eventual increase yields (1-n2-n1+y+x > 0 /\ n2+n1 <= 0), dependencies: -1+n1 >= 0 -1+n2 >= 0 Replacement map: {1-n1+y+x > 0 -> 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0, -1+n1 >= 0 -> -1+n1 >= 0, 1-n1+x > 0 -> 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0, -1+n2 >= 0 -> -1+n2 >= 0, 1-n2-n1+x > 0 -> 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0, 1-n2-n1+y+x > 0 -> 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0} Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T]}, {14[T]}] Step with 6 Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)], 6[(x <= 0)] Blocked [{}, {6[T]}, {14[T]}, {}] Backtrack Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T]}, {6[T], 14[T]}] Step with 10 Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)], 10[(x > 0)] Blocked [{}, {6[T]}, {6[T], 14[T]}, {}] Covered Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T]}, {6[T], 10[T], 14[T]}] Step with 11 Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)], 11[(y+x > 0 /\ x > 0)] Blocked [{}, {6[T]}, {6[T], 10[T], 14[T]}, {}] Covered Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T]}, {6[T], 10[T], 11[T], 14[T]}] Step with 12 Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T]}, {6[T], 10[T], 11[T], 14[T]}, {12[T]}] Accelerate Start location: [1] Program variables: x y 7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1 6: [3] -> [7] : x <= 0, cost: 1 10: [3] -> [3] : x'=y+x, y'=-1-y, x > 0, cost: 1 11: [3] -> [3] : x'=-1+x, (y+x > 0 /\ x > 0), cost: 1 12: [3] -> [3] : x'=-n+x, (1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0), cost: 1 13: [3] -> [3] : x'=-n2+x, (1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0), cost: 1 14: [3] -> [3] : x'=-n2*n3-n3*n1+x, (-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0), cost: 1 15: [3] -> [3] : x'=-n31*n5*n22-n31*n11*n5-n5*n+x, (-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0), cost: 1 Loop Acceleration Original rule: [3] -> [3] : x'=-n31*n11-n31*n22-n+x, (-1+n11 >= 0 /\ 1-(-1+n31)*n22-n11-(-1+n31)*n11-n22+x > 0 /\ -1+n31 >= 0 /\ 1-(-1+n31)*n22-n11-(-1+n31)*n11+y+x > 0 /\ 1-(-1+n31)*n22-n11-(-1+n31)*n11+x > 0 /\ 1-(-1+n31)*n22-n11-(-1+n31)*n11-n22+y+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-n31*n11-n31*n22-n+x > 0 /\ 1-n31*n11-n31*n22-n+y+x > 0), cost: 1 New rule: [3] -> [3] : x'=-n31*n5*n22-n31*n11*n5-n5*n+x, (-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0), cost: 1 -1+n11 >= 0 [0]: monotonic increase yields -1+n11 >= 0 1-(-1+n31)*n22-n11-(-1+n31)*n11-n22+x > 0 [0]: montonic decrease yields 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0, dependencies: -1+n >= 0 1-n31*n11-n31*n22-n+x > 0 1-(-1+n31)*n22-n11-(-1+n31)*n11-n22+x > 0 [1]: eventual decrease yields (1-(-1+n31)*n22-n11-(-1+n31)*n11-n22+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0) 1-(-1+n31)*n22-n11-(-1+n31)*n11-n22+x > 0 [2]: eventual increase yields (1-(-1+n31)*n22-n11-(-1+n31)*n11-n22+x > 0 /\ n31*n11+n31*n22+n <= 0) -1+n31 >= 0 [0]: monotonic increase yields -1+n31 >= 0 1-(-1+n31)*n22-n11-(-1+n31)*n11+y+x > 0 [0]: montonic decrease yields 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0, dependencies: 1-(-1+n31)*n22-n11-(-1+n31)*n11-n22+y+x > 0 -1+n22 >= 0 1-(-1+n31)*n22-n11-(-1+n31)*n11+y+x > 0 [1]: eventual decrease yields (1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ 1-(-1+n31)*n22-n11-(-1+n31)*n11+y+x > 0) 1-(-1+n31)*n22-n11-(-1+n31)*n11+y+x > 0 [2]: eventual increase yields (n31*n11+n31*n22+n <= 0 /\ 1-(-1+n31)*n22-n11-(-1+n31)*n11+y+x > 0) 1-(-1+n31)*n22-n11-(-1+n31)*n11+x > 0 [0]: montonic decrease yields 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0, dependencies: 1-(-1+n31)*n22-n11-(-1+n31)*n11-n22+x > 0 -1+n22 >= 0 1-(-1+n31)*n22-n11-(-1+n31)*n11+x > 0 [1]: eventual decrease yields (1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ 1-(-1+n31)*n22-n11-(-1+n31)*n11+x > 0) 1-(-1+n31)*n22-n11-(-1+n31)*n11+x > 0 [2]: eventual increase yields (n31*n11+n31*n22+n <= 0 /\ 1-(-1+n31)*n22-n11-(-1+n31)*n11+x > 0) 1-(-1+n31)*n22-n11-(-1+n31)*n11-n22+y+x > 0 [0]: montonic decrease yields 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0, dependencies: -1+n >= 0 1-n31*n11-n31*n22-n+y+x > 0 1-(-1+n31)*n22-n11-(-1+n31)*n11-n22+y+x > 0 [1]: eventual decrease yields (1-(-1+n31)*n22-n11-(-1+n31)*n11-n22+y+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0) 1-(-1+n31)*n22-n11-(-1+n31)*n11-n22+y+x > 0 [2]: eventual increase yields (n31*n11+n31*n22+n <= 0 /\ 1-(-1+n31)*n22-n11-(-1+n31)*n11-n22+y+x > 0) -1+n22 >= 0 [0]: monotonic increase yields -1+n22 >= 0 -1+n >= 0 [0]: monotonic increase yields -1+n >= 0 1-n31*n11-n31*n22-n+x > 0 [0]: montonic decrease yields 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0, dependencies: -1+n11 >= 0 -1+n31 >= 0 -1+n22 >= 0 -1+n >= 0 1-n31*n11-n31*n22-n+x > 0 [1]: eventual increase yields (n31*n11+n31*n22+n <= 0 /\ 1-n31*n11-n31*n22-n+x > 0) 1-n31*n11-n31*n22-n+y+x > 0 [0]: montonic decrease yields 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0, dependencies: -1+n11 >= 0 -1+n31 >= 0 -1+n22 >= 0 -1+n >= 0 1-n31*n11-n31*n22-n+y+x > 0 [1]: eventual increase yields (n31*n11+n31*n22+n <= 0 /\ 1-n31*n11-n31*n22-n+y+x > 0) Replacement map: {-1+n11 >= 0 -> -1+n11 >= 0, 1-(-1+n31)*n22-n11-(-1+n31)*n11-n22+x > 0 -> 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0, -1+n31 >= 0 -> -1+n31 >= 0, 1-(-1+n31)*n22-n11-(-1+n31)*n11+y+x > 0 -> 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0, 1-(-1+n31)*n22-n11-(-1+n31)*n11+x > 0 -> 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0, 1-(-1+n31)*n22-n11-(-1+n31)*n11-n22+y+x > 0 -> 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0, -1+n22 >= 0 -> -1+n22 >= 0, -1+n >= 0 -> -1+n >= 0, 1-n31*n11-n31*n22-n+x > 0 -> 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0, 1-n31*n11-n31*n22-n+y+x > 0 -> 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0} Trace 7[T], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)] Blocked [{}, {6[T]}, {15[T]}] Step with 6 Trace 7[T], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)], 6[(x <= 0)] Blocked [{}, {6[T]}, {15[T]}, {}] Backtrack Trace 7[T], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)] Blocked [{}, {6[T]}, {6[T], 15[T]}] Step with 10 Trace 7[T], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)], 10[(x > 0)] Blocked [{}, {6[T]}, {6[T], 15[T]}, {}] Covered Trace 7[T], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)] Blocked [{}, {6[T]}, {6[T], 10[T], 15[T]}] Step with 11 Trace 7[T], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)], 11[(y+x > 0 /\ x > 0)] Blocked [{}, {6[T]}, {6[T], 10[T], 15[T]}, {}] Covered Trace 7[T], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)] Blocked [{}, {6[T]}, {6[T], 10[T], 11[T], 15[T]}] Step with 12 Trace 7[T], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T]}, {6[T], 10[T], 11[T], 15[T]}, {12[T]}] Covered Trace 7[T], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)] Blocked [{}, {6[T]}, {6[T], 10[T], 11[T], 12[T], 15[T]}] Step with 13 Trace 7[T], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T]}, {6[T], 10[T], 11[T], 12[T], 15[T]}, {13[T]}] Covered Trace 7[T], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)] Blocked [{}, {6[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 15[T]}] Step with 14 Trace 7[T], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 15[T]}, {14[T]}] Covered Trace 7[T], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)] Blocked [{}, {6[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T]}] Backtrack Trace 7[T] Blocked [{}, {6[T], 15[T]}] Step with 14 Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T], 15[T]}, {14[T]}] Step with 15 Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)] Blocked [{}, {6[T], 15[T]}, {14[T]}, {15[T]}] Covered Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T], 15[T]}, {14[T], 15[T]}] Step with 6 Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)], 6[(x <= 0)] Blocked [{}, {6[T], 15[T]}, {14[T], 15[T]}, {}] Backtrack Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T], 15[T]}, {6[T], 14[T], 15[T]}] Step with 10 Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)], 10[(x > 0)] Blocked [{}, {6[T], 15[T]}, {6[T], 14[T], 15[T]}, {}] Covered Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T], 15[T]}, {6[T], 10[T], 14[T], 15[T]}] Step with 11 Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)], 11[(y+x > 0 /\ x > 0)] Blocked [{}, {6[T], 15[T]}, {6[T], 10[T], 14[T], 15[T]}, {}] Covered Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T], 15[T]}, {6[T], 10[T], 11[T], 14[T], 15[T]}] Step with 12 Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T], 15[T]}, {6[T], 10[T], 11[T], 14[T], 15[T]}, {12[T]}] Covered Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T]}] Step with 13 Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T]}, {13[T]}] Covered Trace 7[T], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T]}] Backtrack Trace 7[T] Blocked [{}, {6[T], 14[T], 15[T]}] Step with 13 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {13[T]}] Step with 14 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {13[T]}, {14[T]}] Accelerate Start location: [1] Program variables: x y 7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1 6: [3] -> [7] : x <= 0, cost: 1 10: [3] -> [3] : x'=y+x, y'=-1-y, x > 0, cost: 1 11: [3] -> [3] : x'=-1+x, (y+x > 0 /\ x > 0), cost: 1 12: [3] -> [3] : x'=-n+x, (1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0), cost: 1 13: [3] -> [3] : x'=-n2+x, (1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0), cost: 1 14: [3] -> [3] : x'=-n2*n3-n3*n1+x, (-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0), cost: 1 15: [3] -> [3] : x'=-n31*n5*n22-n31*n11*n5-n5*n+x, (-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0), cost: 1 16: [3] -> [3] : x'=-n27*n10-n2*n10*n3-n10*n3*n1+x, (-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0), cost: 1 Loop Acceleration Original rule: [3] -> [3] : x'=-n27-n2*n3-n3*n1+x, (-1+n27 >= 0 /\ -1+n3 >= 0 /\ 1-n27+y+x > 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0 /\ 1-n27-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-n27-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-n27-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n27+x > 0 /\ 1-n27-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0), cost: 1 New rule: [3] -> [3] : x'=-n27*n10-n2*n10*n3-n10*n3*n1+x, (-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0), cost: 1 -1+n27 >= 0 [0]: monotonic increase yields -1+n27 >= 0 -1+n3 >= 0 [0]: monotonic increase yields -1+n3 >= 0 1-n27+y+x > 0 [0]: montonic decrease yields 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0, dependencies: -1+n27 >= 0 -1+n3 >= 0 -1+n1 >= 0 -1+n2 >= 0 1-n27+y+x > 0 [1]: eventual decrease yields (1-n27+y+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0) 1-n27+y+x > 0 [2]: eventual increase yields (1-n27+y+x > 0 /\ n27+n2*n3+n3*n1 <= 0) -1+n1 >= 0 [0]: monotonic increase yields -1+n1 >= 0 -1+n2 >= 0 [0]: monotonic increase yields -1+n2 >= 0 1-n27-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 [0]: montonic decrease yields 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0, dependencies: -1+n27 >= 0 1-n27+x > 0 1-n27-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 [1]: eventual decrease yields (1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0) 1-n27-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 [2]: eventual increase yields (n27+n2*n3+n3*n1 <= 0 /\ 1-n27-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0) 1-n27-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 [0]: montonic decrease yields 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0, dependencies: -1+n2 >= 0 1-n27-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 1-n27-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 [1]: eventual increase yields (n27+n2*n3+n3*n1 <= 0 /\ 1-n27-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0) 1-n27-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 [0]: montonic decrease yields 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0, dependencies: -1+n27 >= 0 1-n27+y+x > 0 1-n27-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 [1]: eventual increase yields (n27+n2*n3+n3*n1 <= 0 /\ 1-n27-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0) 1-n27+x > 0 [0]: montonic decrease yields 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0, dependencies: -1+n27 >= 0 -1+n3 >= 0 -1+n1 >= 0 -1+n2 >= 0 1-n27+x > 0 [1]: eventual increase yields (n27+n2*n3+n3*n1 <= 0 /\ 1-n27+x > 0) 1-n27-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 [0]: montonic decrease yields 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0, dependencies: -1+n27 >= 0 1-n27+y+x > 0 -1+n2 >= 0 1-n27-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 [1]: eventual increase yields (n27+n2*n3+n3*n1 <= 0 /\ 1-n27-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0) Replacement map: {-1+n27 >= 0 -> -1+n27 >= 0, -1+n3 >= 0 -> -1+n3 >= 0, 1-n27+y+x > 0 -> 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0, -1+n1 >= 0 -> -1+n1 >= 0, -1+n2 >= 0 -> -1+n2 >= 0, 1-n27-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 -> 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0, 1-n27-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 -> 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0, 1-n27-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 -> 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0, 1-n27+x > 0 -> 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0, 1-n27-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 -> 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0} Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {16[T]}] Step with 6 Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)], 6[(x <= 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {16[T]}, {}] Backtrack Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 16[T]}] Step with 10 Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)], 10[(x > 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 16[T]}, {}] Covered Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 16[T]}] Step with 11 Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)], 11[(y+x > 0 /\ x > 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 16[T]}, {}] Covered Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 16[T]}] Step with 12 Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 16[T]}, {12[T]}] Accelerate Start location: [1] Program variables: x y 7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1 6: [3] -> [7] : x <= 0, cost: 1 10: [3] -> [3] : x'=y+x, y'=-1-y, x > 0, cost: 1 11: [3] -> [3] : x'=-1+x, (y+x > 0 /\ x > 0), cost: 1 12: [3] -> [3] : x'=-n+x, (1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0), cost: 1 13: [3] -> [3] : x'=-n2+x, (1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0), cost: 1 14: [3] -> [3] : x'=-n2*n3-n3*n1+x, (-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0), cost: 1 15: [3] -> [3] : x'=-n31*n5*n22-n31*n11*n5-n5*n+x, (-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0), cost: 1 16: [3] -> [3] : x'=-n27*n10-n2*n10*n3-n10*n3*n1+x, (-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0), cost: 1 17: [3] -> [3] : x'=-n15*n35*n101*n17-n17*n-n35*n101*n17*n29-n271*n101*n17+x, (1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0), cost: 1 Loop Acceleration Original rule: [3] -> [3] : x'=-n15*n35*n101-n271*n101-n35*n101*n29-n+x, (1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35-n29+x > 0 /\ -1+n35 >= 0 /\ 1-n15*n35*n101-n271*n101-n35*n101*n29-n+x > 0 /\ 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y-n29+x > 0 /\ -1+n101 >= 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+x > 0 /\ -1+n15 >= 0 /\ 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y+x > 0 /\ 1-(-1+n101)*n271-n271-(-1+n101)*n35*n29-(-1+n101)*n15*n35+x > 0 /\ -1+n >= 0 /\ 1-(-1+n101)*n271-n271-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y+x > 0 /\ 1-n15*n35*n101-n271*n101-n35*n101*n29-n+y+x > 0 /\ -1+n29 >= 0), cost: 1 New rule: [3] -> [3] : x'=-n15*n35*n101*n17-n17*n-n35*n101*n17*n29-n271*n101*n17+x, (1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0), cost: 1 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35-n29+x > 0 [0]: montonic decrease yields 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0, dependencies: 1-n15*n35*n101-n271*n101-n35*n101*n29-n+x > 0 -1+n >= 0 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35-n29+x > 0 [1]: eventual decrease yields (1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35-n29+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0) 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35-n29+x > 0 [2]: eventual increase yields (1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35-n29+x > 0 /\ n15*n35*n101+n271*n101+n35*n101*n29+n <= 0) -1+n35 >= 0 [0]: monotonic increase yields -1+n35 >= 0 1-n15*n35*n101-n271*n101-n35*n101*n29-n+x > 0 [0]: montonic decrease yields 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0, dependencies: -1+n35 >= 0 -1+n101 >= 0 -1+n271 >= 0 -1+n15 >= 0 -1+n >= 0 -1+n29 >= 0 1-n15*n35*n101-n271*n101-n35*n101*n29-n+x > 0 [1]: eventual decrease yields (1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-n15*n35*n101-n271*n101-n35*n101*n29-n+x > 0) 1-n15*n35*n101-n271*n101-n35*n101*n29-n+x > 0 [2]: eventual increase yields (1-n15*n35*n101-n271*n101-n35*n101*n29-n+x > 0 /\ n15*n35*n101+n271*n101+n35*n101*n29+n <= 0) 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y-n29+x > 0 [0]: montonic decrease yields 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0, dependencies: -1+n >= 0 1-n15*n35*n101-n271*n101-n35*n101*n29-n+y+x > 0 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y-n29+x > 0 [1]: eventual decrease yields (1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y-n29+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0) 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y-n29+x > 0 [2]: eventual increase yields (1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y-n29+x > 0 /\ n15*n35*n101+n271*n101+n35*n101*n29+n <= 0) -1+n101 >= 0 [0]: monotonic increase yields -1+n101 >= 0 -1+n271 >= 0 [0]: monotonic increase yields -1+n271 >= 0 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+x > 0 [0]: montonic decrease yields 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0, dependencies: 1-n15*n35*n101-n271*n101-n35*n101*n29-n+x > 0 -1+n >= 0 -1+n29 >= 0 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+x > 0 [1]: eventual decrease yields (1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+x > 0) 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+x > 0 [2]: eventual increase yields (1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+x > 0 /\ n15*n35*n101+n271*n101+n35*n101*n29+n <= 0) -1+n15 >= 0 [0]: monotonic increase yields -1+n15 >= 0 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y+x > 0 [0]: montonic decrease yields 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0, dependencies: 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y-n29+x > 0 -1+n29 >= 0 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y+x > 0 [1]: eventual decrease yields (1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0) 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y+x > 0 [2]: eventual increase yields (1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y+x > 0 /\ n15*n35*n101+n271*n101+n35*n101*n29+n <= 0) 1-(-1+n101)*n271-n271-(-1+n101)*n35*n29-(-1+n101)*n15*n35+x > 0 [0]: montonic decrease yields 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0, dependencies: -1+n35 >= 0 1-n15*n35*n101-n271*n101-n35*n101*n29-n+x > 0 -1+n15 >= 0 -1+n >= 0 -1+n29 >= 0 1-(-1+n101)*n271-n271-(-1+n101)*n35*n29-(-1+n101)*n15*n35+x > 0 [1]: eventual decrease yields (1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n101)*n271-n271-(-1+n101)*n35*n29-(-1+n101)*n15*n35+x > 0) 1-(-1+n101)*n271-n271-(-1+n101)*n35*n29-(-1+n101)*n15*n35+x > 0 [2]: eventual increase yields (1-(-1+n101)*n271-n271-(-1+n101)*n35*n29-(-1+n101)*n15*n35+x > 0 /\ n15*n35*n101+n271*n101+n35*n101*n29+n <= 0) -1+n >= 0 [0]: monotonic increase yields -1+n >= 0 1-(-1+n101)*n271-n271-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y+x > 0 [0]: montonic decrease yields 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0, dependencies: -1+n35 >= 0 -1+n15 >= 0 -1+n >= 0 1-n15*n35*n101-n271*n101-n35*n101*n29-n+y+x > 0 -1+n29 >= 0 1-(-1+n101)*n271-n271-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y+x > 0 [1]: eventual decrease yields (1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ 1-(-1+n101)*n271-n271-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y+x > 0) 1-(-1+n101)*n271-n271-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y+x > 0 [2]: eventual increase yields (n15*n35*n101+n271*n101+n35*n101*n29+n <= 0 /\ 1-(-1+n101)*n271-n271-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y+x > 0) 1-n15*n35*n101-n271*n101-n35*n101*n29-n+y+x > 0 [0]: montonic decrease yields 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0, dependencies: -1+n35 >= 0 -1+n101 >= 0 -1+n271 >= 0 -1+n15 >= 0 -1+n >= 0 -1+n29 >= 0 1-n15*n35*n101-n271*n101-n35*n101*n29-n+y+x > 0 [1]: eventual decrease yields (1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-n15*n35*n101-n271*n101-n35*n101*n29-n+y+x > 0) 1-n15*n35*n101-n271*n101-n35*n101*n29-n+y+x > 0 [2]: eventual increase yields (n15*n35*n101+n271*n101+n35*n101*n29+n <= 0 /\ 1-n15*n35*n101-n271*n101-n35*n101*n29-n+y+x > 0) -1+n29 >= 0 [0]: monotonic increase yields -1+n29 >= 0 Replacement map: {1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35-n29+x > 0 -> 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0, -1+n35 >= 0 -> -1+n35 >= 0, 1-n15*n35*n101-n271*n101-n35*n101*n29-n+x > 0 -> 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0, 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y-n29+x > 0 -> 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0, -1+n101 >= 0 -> -1+n101 >= 0, -1+n271 >= 0 -> -1+n271 >= 0, 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+x > 0 -> 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0, -1+n15 >= 0 -> -1+n15 >= 0, 1-(-1+n35)*n29-(-1+n101)*n271-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y+x > 0 -> 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0, 1-(-1+n101)*n271-n271-(-1+n101)*n35*n29-(-1+n101)*n15*n35+x > 0 -> 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0, -1+n >= 0 -> -1+n >= 0, 1-(-1+n101)*n271-n271-(-1+n101)*n35*n29-(-1+n101)*n15*n35+y+x > 0 -> 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0, 1-n15*n35*n101-n271*n101-n35*n101*n29-n+y+x > 0 -> 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0, -1+n29 >= 0 -> -1+n29 >= 0} Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {17[T]}] Step with 6 Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)], 6[(x <= 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {17[T]}, {}] Backtrack Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 17[T]}] Step with 10 Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)], 10[(x > 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 17[T]}, {}] Covered Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 17[T]}] Step with 11 Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)], 11[(y+x > 0 /\ x > 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 17[T]}, {}] Covered Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 17[T]}] Step with 12 Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 17[T]}, {12[T]}] Covered Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 17[T]}] Step with 13 Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 17[T]}, {13[T]}] Covered Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 17[T]}] Step with 14 Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 17[T]}, {14[T]}] Covered Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 17[T]}] Step with 15 Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 17[T]}, {15[T]}] Covered Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 17[T]}] Step with 16 Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 17[T]}, {16[T]}] Covered Trace 7[T], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)] Blocked [{}, {6[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}] Backtrack Trace 7[T] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}] Step with 16 Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {16[T]}] Step with 17 Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {16[T]}, {17[T]}] Covered Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {16[T], 17[T]}] Step with 6 Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)], 6[(x <= 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {16[T], 17[T]}, {}] Backtrack Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 16[T], 17[T]}] Step with 10 Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)], 10[(x > 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 16[T], 17[T]}, {}] Covered Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 16[T], 17[T]}] Step with 11 Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)], 11[(y+x > 0 /\ x > 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 16[T], 17[T]}, {}] Covered Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 16[T], 17[T]}] Step with 12 Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 16[T], 17[T]}, {12[T]}] Covered Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 16[T], 17[T]}] Step with 13 Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 16[T], 17[T]}, {13[T]}] Covered Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 16[T], 17[T]}] Step with 14 Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 16[T], 17[T]}, {14[T]}] Covered Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 16[T], 17[T]}] Step with 15 Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 16[T], 17[T]}, {15[T]}] Covered Trace 7[T], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 14[T], 15[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}] Backtrack Trace 7[T] Blocked [{}, {6[T], 14[T], 15[T], 16[T], 17[T]}] Step with 10 Trace 7[T], 10[(x > 0)] Blocked [{}, {6[T], 14[T], 15[T], 16[T], 17[T]}, {}] Covered Trace 7[T] Blocked [{}, {6[T], 10[T], 14[T], 15[T], 16[T], 17[T]}] Step with 11 Trace 7[T], 11[(y+x > 0 /\ x > 0)] Blocked [{}, {6[T], 10[T], 14[T], 15[T], 16[T], 17[T]}, {}] Covered Trace 7[T] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}] Step with 12 Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T]}] Step with 13 Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T]}, {13[T]}] Covered Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T]}] Step with 14 Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T]}, {14[T]}] Covered Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T], 14[T]}] Step with 15 Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T], 14[T]}, {15[T]}] Covered Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T], 14[T], 15[T]}] Step with 16 Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T], 14[T], 15[T]}, {16[T]}] Covered Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T], 14[T], 15[T], 16[T]}] Step with 17 Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T], 14[T], 15[T], 16[T]}, {17[T]}] Covered Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}] Step with 6 Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)], 6[(x <= 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}, {}] Backtrack Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}] Step with 10 Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)], 10[(x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}, {}] Covered Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}] Step with 11 Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)], 11[(y+x > 0 /\ x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}, {}] Covered Trace 7[T], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T]}] Backtrack Trace 7[T] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}] Step with 13 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T]}] Step with 14 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T]}, {14[T]}] Covered Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T], 14[T]}] Step with 15 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T], 14[T]}, {15[T]}] Covered Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T], 14[T], 15[T]}] Step with 16 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T], 14[T], 15[T]}, {16[T]}] Covered Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T], 14[T], 15[T], 16[T]}] Step with 17 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T], 14[T], 15[T], 16[T]}, {17[T]}] Covered Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T], 14[T], 15[T], 16[T], 17[T]}] Step with 6 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 6[(x <= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {13[T], 14[T], 15[T], 16[T], 17[T]}, {}] Backtrack Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 13[T], 14[T], 15[T], 16[T], 17[T]}] Step with 10 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 10[(x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 13[T], 14[T], 15[T], 16[T], 17[T]}, {}] Covered Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 13[T], 14[T], 15[T], 16[T], 17[T]}] Step with 11 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 11[(y+x > 0 /\ x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 13[T], 14[T], 15[T], 16[T], 17[T]}, {}] Covered Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 13[T], 14[T], 15[T], 16[T], 17[T]}] Step with 12 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 13[T], 14[T], 15[T], 16[T], 17[T]}, {12[T]}] Accelerate Start location: [1] Program variables: x y 7: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1 6: [3] -> [7] : x <= 0, cost: 1 10: [3] -> [3] : x'=y+x, y'=-1-y, x > 0, cost: 1 11: [3] -> [3] : x'=-1+x, (y+x > 0 /\ x > 0), cost: 1 12: [3] -> [3] : x'=-n+x, (1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0), cost: 1 13: [3] -> [3] : x'=-n2+x, (1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0), cost: 1 14: [3] -> [3] : x'=-n2*n3-n3*n1+x, (-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0), cost: 1 15: [3] -> [3] : x'=-n31*n5*n22-n31*n11*n5-n5*n+x, (-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0), cost: 1 16: [3] -> [3] : x'=-n27*n10-n2*n10*n3-n10*n3*n1+x, (-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0), cost: 1 17: [3] -> [3] : x'=-n15*n35*n101*n17-n17*n-n35*n101*n17*n29-n271*n101*n17+x, (1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0), cost: 1 18: [3] -> [3] : x'=-n*n47-n47*n219+x, (1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0), cost: 1 Loop Acceleration Original rule: [3] -> [3] : x'=-n-n219+x, (1-n219+x > 0 /\ 1-n+y-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n219 >= 0), cost: 1 New rule: [3] -> [3] : x'=-n*n47-n47*n219+x, (1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0), cost: 1 1-n219+x > 0 [0]: montonic decrease yields 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0, dependencies: 1-n-n219+x > 0 -1+n >= 0 1-n219+x > 0 [1]: eventual decrease yields (1-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0) 1-n219+x > 0 [2]: eventual increase yields (n+n219 <= 0 /\ 1-n219+x > 0) 1-n+y-n219+x > 0 [0]: montonic decrease yields 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0, dependencies: 1+y-n219+x > 0 -1+n219 >= 0 1-n+y-n219+x > 0 [1]: eventual decrease yields (1-n+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0) 1-n+y-n219+x > 0 [2]: eventual increase yields (n+n219 <= 0 /\ 1-n+y-n219+x > 0) 1-n-n219+x > 0 [0]: montonic decrease yields 1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0, dependencies: 1-n219+x > 0 -1+n219 >= 0 1-n-n219+x > 0 [1]: eventual decrease yields (1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0) 1-n-n219+x > 0 [2]: eventual increase yields (n+n219 <= 0 /\ 1-n-n219+x > 0) 1+y-n219+x > 0 [0]: montonic decrease yields 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0, dependencies: 1-n+y-n219+x > 0 -1+n >= 0 1+y-n219+x > 0 [1]: eventual decrease yields (1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0) 1+y-n219+x > 0 [2]: eventual increase yields (n+n219 <= 0 /\ 1+y-n219+x > 0) -1+n >= 0 [0]: monotonic increase yields -1+n >= 0 -1+n219 >= 0 [0]: monotonic increase yields -1+n219 >= 0 Replacement map: {1-n219+x > 0 -> 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0, 1-n+y-n219+x > 0 -> 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0, 1-n-n219+x > 0 -> (1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0), 1+y-n219+x > 0 -> (1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0), -1+n >= 0 -> -1+n >= 0, -1+n219 >= 0 -> -1+n219 >= 0} Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {18[T]}] Step with 6 Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)], 6[(x <= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {18[T]}, {}] Backtrack Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 18[T]}] Step with 10 Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)], 10[(x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 18[T]}, {}] Covered Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 18[T]}] Step with 11 Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)], 11[(y+x > 0 /\ x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 18[T]}, {}] Covered Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 18[T]}] Step with 12 Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 18[T]}, {12[T]}] Covered Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 18[T]}] Step with 13 Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 18[T]}, {13[T]}] Covered Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 18[T]}] Step with 14 Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 18[T]}, {14[T]}] Covered Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 18[T]}] Step with 15 Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 18[T]}, {15[T]}] Covered Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 18[T]}] Step with 16 Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 18[T]}, {16[T]}] Covered Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T], 18[T]}] Step with 17 Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T], 18[T]}, {17[T]}] Covered Trace 7[T], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}] Backtrack Trace 7[T] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}] Step with 13 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T]}] Step with 14 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 14[(-1+n3 >= 0 /\ -1+n1 >= 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ -1+n2 >= 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0 /\ 1-(-1+n3)*n1-(-1+n3)*n2-n1+y+x > 0 /\ 1-n2-(-1+n3)*n1-(-1+n3)*n2-n1+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T]}, {14[T]}] Covered Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T]}] Step with 15 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 15[(-1+n11 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+x > 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+y+x > 0 /\ -1+n31 >= 0 /\ -1+n5 >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11+x > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-(-1+n31)*n22-n31*(-1+n5)*n22-n11-(-1+n31)*n11-(-1+n5)*n-n31*(-1+n5)*n11-n22+y+x > 0 /\ 1-n31*n11-n31*(-1+n5)*n22-(-1+n5)*n-n31*n22-n31*(-1+n5)*n11-n+y+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T]}, {15[T]}] Covered Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T], 15[T]}] Step with 16 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 16[(-1+n27 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n3 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+y+x > 0 /\ -1+n1 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2-n2*n3*(-1+n10)-(-1+n3)*n1-(-1+n3)*n2-n1-n27*(-1+n10)+x > 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+y+x > 0 /\ -1+n2 >= 0 /\ -1+n10 >= 0 /\ 1-n27-n3*n1*(-1+n10)-n2*n3*(-1+n10)-n27*(-1+n10)+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T], 15[T]}, {16[T]}] Covered Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T], 15[T], 16[T]}] Step with 17 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 17[(1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+x > 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n35 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ -1+n17 >= 0 /\ -1+n101 >= 0 /\ 1-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n-n29+x > 0 /\ -1+n271 >= 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y-n29+x > 0 /\ -1+n15 >= 0 /\ -1+n >= 0 /\ 1-(-1+n17)*n35*n101*n29-n15*n35*n101-(-1+n17)*n271*n101-n271*n101-(-1+n17)*n15*n35*n101-n35*n101*n29-(-1+n17)*n-n+y+x > 0 /\ 1-(-1+n35)*n29-(-1+n17)*n35*n101*n29-(-1+n101)*n271-(-1+n17)*n271*n101-n271-n15-(-1+n35)*n15-(-1+n101)*n35*n29-(-1+n17)*n15*n35*n101-(-1+n101)*n15*n35-(-1+n17)*n+y+x > 0 /\ -1+n29 >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T], 15[T], 16[T]}, {17[T]}] Covered Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T], 15[T], 16[T], 17[T]}] Step with 18 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 18[(1-(-1+n47)*n-(-1+n47)*n219-n-n219+x > 0 /\ 1-n-n219+x > 0 /\ 1+y-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n219+x > 0 /\ 1-(-1+n47)*n-(-1+n47)*n219-n+y-n219+x > 0 /\ -1+n >= 0 /\ -1+n47 >= 0 /\ 1-(-1+n47)*n-(-1+n47)*n219+y-n219+x > 0 /\ -1+n219 >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T], 15[T], 16[T], 17[T]}, {18[T]}] Covered Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}] Step with 6 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 6[(x <= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {}] Backtrack Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {6[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}] Step with 10 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 10[(x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {6[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {}] Covered Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {6[T], 10[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}] Step with 11 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 11[(y+x > 0 /\ x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {6[T], 10[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {}] Covered Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {6[T], 10[T], 11[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}] Step with 12 Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)], 12[(1-n+x > 0 /\ 1-n+y+x > 0 /\ -1+n >= 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {6[T], 10[T], 11[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {12[T]}] Covered Trace 7[T], 13[(1-n2+y+x > 0 /\ -1+n2 >= 0 /\ 1-n2+x > 0)] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T], 16[T], 17[T], 18[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}] Backtrack Trace 7[T] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T], 17[T], 18[T]}] Backtrack Trace Blocked [{7[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b