unknown Initial ITS Start location: l3 Program variables: x^0 y^0 z^0 0: l0 -> l1 : x^0'=x^post1, y^0'=y^post1, z^0'=z^post1, (-z^post1+z^0 == 0 /\ -y^post1+y^0 == 0 /\ 1-x^0 <= 0 /\ x^0-x^post1 == 0 /\ 1-y^0 <= 0), cost: 1 1: l1 -> l0 : x^0'=x^post2, y^0'=y^post2, z^0'=z^post2, (-z^post2+z^0 == 0 /\ x^post2-z^0 == 0 /\ 1+y^post2-y^0 == 0), cost: 1 2: l1 -> l0 : x^0'=x^post3, y^0'=y^post3, z^0'=z^post3, (1-x^0+x^post3 == 0 /\ -z^post3+z^0 == 0 /\ -y^post3+y^0 == 0), cost: 1 3: l2 -> l0 : x^0'=x^post4, y^0'=y^post4, z^0'=z^post4, (-z^post4+z^0 == 0 /\ x^0-x^post4 == 0 /\ -y^post4+y^0 == 0), cost: 1 4: l3 -> l2 : x^0'=x^post5, y^0'=y^post5, z^0'=z^post5, (-y^post5+y^0 == 0 /\ -z^post5+z^0 == 0 /\ -x^post5+x^0 == 0), cost: 1 Chained Linear Paths Start location: l3 Program variables: x^0 y^0 z^0 0: l0 -> l1 : x^0'=x^post1, y^0'=y^post1, z^0'=z^post1, (-z^post1+z^0 == 0 /\ -y^post1+y^0 == 0 /\ 1-x^0 <= 0 /\ x^0-x^post1 == 0 /\ 1-y^0 <= 0), cost: 1 1: l1 -> l0 : x^0'=x^post2, y^0'=y^post2, z^0'=z^post2, (-z^post2+z^0 == 0 /\ x^post2-z^0 == 0 /\ 1+y^post2-y^0 == 0), cost: 1 2: l1 -> l0 : x^0'=x^post3, y^0'=y^post3, z^0'=z^post3, (1-x^0+x^post3 == 0 /\ -z^post3+z^0 == 0 /\ -y^post3+y^0 == 0), cost: 1 5: l3 -> l0 : x^0'=x^post4, y^0'=y^post4, z^0'=z^post4, (-y^post5+y^0 == 0 /\ x^post5-x^post4 == 0 /\ z^post5-z^post4 == 0 /\ -z^post5+z^0 == 0 /\ -x^post5+x^0 == 0 /\ -y^post4+y^post5 == 0), cost: 1 Eliminating location l2 by chaining: Applied chaining First rule: l3 -> l2 : x^0'=x^post5, y^0'=y^post5, z^0'=z^post5, (-y^post5+y^0 == 0 /\ -z^post5+z^0 == 0 /\ -x^post5+x^0 == 0), cost: 1 Second rule: l2 -> l0 : x^0'=x^post4, y^0'=y^post4, z^0'=z^post4, (-z^post4+z^0 == 0 /\ x^0-x^post4 == 0 /\ -y^post4+y^0 == 0), cost: 1 New rule: l3 -> l0 : x^0'=x^post4, y^0'=y^post4, z^0'=z^post4, (-y^post5+y^0 == 0 /\ x^post5-x^post4 == 0 /\ z^post5-z^post4 == 0 /\ -z^post5+z^0 == 0 /\ -x^post5+x^0 == 0 /\ -y^post4+y^post5 == 0), cost: 1 Applied deletion Removed the following rules: 3 4 Simplified Transitions Start location: l3 Program variables: x^0 y^0 z^0 6: l0 -> l1 : (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 7: l1 -> l0 : x^0'=z^0, y^0'=-1+y^0, T, cost: 1 8: l1 -> l0 : x^0'=-1+x^0, T, cost: 1 9: l3 -> l0 : T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : x^0'=x^post1, y^0'=y^post1, z^0'=z^post1, (-z^post1+z^0 == 0 /\ -y^post1+y^0 == 0 /\ 1-x^0 <= 0 /\ x^0-x^post1 == 0 /\ 1-y^0 <= 0), cost: 1 New rule: l0 -> l1 : x^0'=x^0, y^0'=y^0, z^0'=z^0, (0 == 0 /\ 1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 propagated equality z^post1 = z^0 propagated equality y^post1 = y^0 propagated equality x^post1 = x^0 Simplified Guard Original rule: l0 -> l1 : x^0'=x^0, y^0'=y^0, z^0'=z^0, (0 == 0 /\ 1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 New rule: l0 -> l1 : x^0'=x^0, y^0'=y^0, z^0'=z^0, (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : x^0'=x^0, y^0'=y^0, z^0'=z^0, (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 New rule: l0 -> l1 : (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 Propagated Equalities Original rule: l1 -> l0 : x^0'=x^post2, y^0'=y^post2, z^0'=z^post2, (-z^post2+z^0 == 0 /\ x^post2-z^0 == 0 /\ 1+y^post2-y^0 == 0), cost: 1 New rule: l1 -> l0 : x^0'=z^0, y^0'=-1+y^0, z^0'=z^0, 0 == 0, cost: 1 propagated equality z^post2 = z^0 propagated equality x^post2 = z^0 propagated equality y^post2 = -1+y^0 Simplified Guard Original rule: l1 -> l0 : x^0'=z^0, y^0'=-1+y^0, z^0'=z^0, 0 == 0, cost: 1 New rule: l1 -> l0 : x^0'=z^0, y^0'=-1+y^0, z^0'=z^0, T, cost: 1 Removed Trivial Updates Original rule: l1 -> l0 : x^0'=z^0, y^0'=-1+y^0, z^0'=z^0, T, cost: 1 New rule: l1 -> l0 : x^0'=z^0, y^0'=-1+y^0, T, cost: 1 Propagated Equalities Original rule: l1 -> l0 : x^0'=x^post3, y^0'=y^post3, z^0'=z^post3, (1-x^0+x^post3 == 0 /\ -z^post3+z^0 == 0 /\ -y^post3+y^0 == 0), cost: 1 New rule: l1 -> l0 : x^0'=-1+x^0, y^0'=y^0, z^0'=z^0, 0 == 0, cost: 1 propagated equality x^post3 = -1+x^0 propagated equality z^post3 = z^0 propagated equality y^post3 = y^0 Simplified Guard Original rule: l1 -> l0 : x^0'=-1+x^0, y^0'=y^0, z^0'=z^0, 0 == 0, cost: 1 New rule: l1 -> l0 : x^0'=-1+x^0, y^0'=y^0, z^0'=z^0, T, cost: 1 Removed Trivial Updates Original rule: l1 -> l0 : x^0'=-1+x^0, y^0'=y^0, z^0'=z^0, T, cost: 1 New rule: l1 -> l0 : x^0'=-1+x^0, T, cost: 1 Propagated Equalities Original rule: l3 -> l0 : x^0'=x^post4, y^0'=y^post4, z^0'=z^post4, (-y^post5+y^0 == 0 /\ x^post5-x^post4 == 0 /\ z^post5-z^post4 == 0 /\ -z^post5+z^0 == 0 /\ -x^post5+x^0 == 0 /\ -y^post4+y^post5 == 0), cost: 1 New rule: l3 -> l0 : x^0'=x^post5, y^0'=y^post5, z^0'=z^post5, (0 == 0 /\ -y^post5+y^0 == 0 /\ -z^post5+z^0 == 0 /\ -x^post5+x^0 == 0), cost: 1 propagated equality x^post4 = x^post5 propagated equality z^post4 = z^post5 propagated equality y^post4 = y^post5 Propagated Equalities Original rule: l3 -> l0 : x^0'=x^post5, y^0'=y^post5, z^0'=z^post5, (0 == 0 /\ -y^post5+y^0 == 0 /\ -z^post5+z^0 == 0 /\ -x^post5+x^0 == 0), cost: 1 New rule: l3 -> l0 : x^0'=x^0, y^0'=y^0, z^0'=z^0, 0 == 0, cost: 1 propagated equality y^post5 = y^0 propagated equality z^post5 = z^0 propagated equality x^post5 = x^0 Simplified Guard Original rule: l3 -> l0 : x^0'=x^0, y^0'=y^0, z^0'=z^0, 0 == 0, cost: 1 New rule: l3 -> l0 : x^0'=x^0, y^0'=y^0, z^0'=z^0, T, cost: 1 Removed Trivial Updates Original rule: l3 -> l0 : x^0'=x^0, y^0'=y^0, z^0'=z^0, T, cost: 1 New rule: l3 -> l0 : T, cost: 1 Step with 9 Trace 9[T] Blocked [{}, {}] Step with 6 Trace 9[T], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {}] Step with 7 Trace 9[T], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {}, {}, {}] Accelerate Start location: l3 Program variables: x^0 y^0 z^0 6: l0 -> l1 : (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 10: l0 -> l0 : x^0'=z^0, y^0'=-n+y^0, (-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0), cost: 1 7: l1 -> l0 : x^0'=z^0, y^0'=-1+y^0, T, cost: 1 8: l1 -> l0 : x^0'=-1+x^0, T, cost: 1 9: l3 -> l0 : T, cost: 1 Loop Acceleration Original rule: l0 -> l0 : x^0'=z^0, y^0'=-1+y^0, (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 New rule: l0 -> l0 : x^0'=z^0, y^0'=-n+y^0, (-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0), cost: 1 -1+x^0 >= 0 [0]: eventual decrease yields (-1+x^0 >= 0 /\ -1+z^0 >= 0) -1+x^0 >= 0 [1]: eventual increase yields (x^0-z^0 <= 0 /\ -1+x^0 >= 0) -1+y^0 >= 0 [0]: montonic decrease yields -n+y^0 >= 0 -1+y^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+y^0 >= 0) Replacement map: {-1+x^0 >= 0 -> (-1+x^0 >= 0 /\ -1+z^0 >= 0), -1+y^0 >= 0 -> -n+y^0 >= 0} Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {}, {10[T]}] Step with 6 Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {10[T]}, {}] Step with 7 Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {}, {10[T]}, {}, {}] Covered Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {10[T]}, {7[T]}] Step with 8 Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {}, {10[T]}, {7[T]}, {}] Accelerate Start location: l3 Program variables: x^0 y^0 z^0 6: l0 -> l1 : (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 10: l0 -> l0 : x^0'=z^0, y^0'=-n+y^0, (-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0), cost: 1 11: l0 -> l0 : x^0'=-n2+x^0, (-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0), cost: 1 7: l1 -> l0 : x^0'=z^0, y^0'=-1+y^0, T, cost: 1 8: l1 -> l0 : x^0'=-1+x^0, T, cost: 1 9: l3 -> l0 : T, cost: 1 Loop Acceleration Original rule: l0 -> l0 : x^0'=-1+x^0, (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 New rule: l0 -> l0 : x^0'=-n2+x^0, (-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0), cost: 1 -1+x^0 >= 0 [0]: montonic decrease yields -n2+x^0 >= 0 -1+x^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+x^0 >= 0) -1+y^0 >= 0 [0]: monotonic increase yields -1+y^0 >= 0 Replacement map: {-1+x^0 >= 0 -> -n2+x^0 >= 0, -1+y^0 >= 0 -> -1+y^0 >= 0} Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {}, {10[T]}, {11[T]}] Accelerate Start location: l3 Program variables: x^0 y^0 z^0 6: l0 -> l1 : (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 10: l0 -> l0 : x^0'=z^0, y^0'=-n+y^0, (-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0), cost: 1 11: l0 -> l0 : x^0'=-n2+x^0, (-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0), cost: 1 12: l0 -> l0 : x^0'=-n2+z^0, y^0'=-n3*n1+y^0, (-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0), cost: 1 7: l1 -> l0 : x^0'=z^0, y^0'=-1+y^0, T, cost: 1 8: l1 -> l0 : x^0'=-1+x^0, T, cost: 1 9: l3 -> l0 : T, cost: 1 Loop Acceleration Original rule: l0 -> l0 : x^0'=-n2+z^0, y^0'=-n1+y^0, (-n1+y^0 >= 0 /\ -n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1-n1+y^0 >= 0 /\ -1+z^0 >= 0), cost: 1 New rule: l0 -> l0 : x^0'=-n2+z^0, y^0'=-n3*n1+y^0, (-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0), cost: 1 -n1+y^0 >= 0 [0]: montonic decrease yields -n1-(-1+n3)*n1+y^0 >= 0, dependencies: -1-n1+y^0 >= 0 -n1+y^0 >= 0 [1]: eventual decrease yields (-n1+y^0 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0), dependencies: -1+n1 >= 0 -n1+y^0 >= 0 [2]: eventual increase yields (-n1+y^0 >= 0 /\ n1 <= 0), dependencies: -1+n1 >= 0 -n2+z^0 >= 0 [0]: monotonic increase yields -n2+z^0 >= 0 -1+x^0 >= 0 [0]: eventual decrease yields (-1+x^0 >= 0 /\ -1-n2+z^0 >= 0) -1+x^0 >= 0 [1]: eventual increase yields (n2+x^0-z^0 <= 0 /\ -1+x^0 >= 0) -1+n2 >= 0 [0]: monotonic increase yields -1+n2 >= 0 -1+n1 >= 0 [0]: monotonic increase yields -1+n1 >= 0 -1-n1+y^0 >= 0 [0]: montonic decrease yields -1-n1-(-1+n3)*n1+y^0 >= 0, dependencies: -1+n1 >= 0 -1-n1+y^0 >= 0 [1]: eventual increase yields (n1 <= 0 /\ -1-n1+y^0 >= 0), dependencies: -1+n1 >= 0 -1+z^0 >= 0 [0]: monotonic increase yields -1+z^0 >= 0, dependencies: -n2+z^0 >= 0 -1+n2 >= 0 Replacement map: {-n1+y^0 >= 0 -> -n1-(-1+n3)*n1+y^0 >= 0, -n2+z^0 >= 0 -> -n2+z^0 >= 0, -1+x^0 >= 0 -> (-1+x^0 >= 0 /\ -1-n2+z^0 >= 0), -1+n2 >= 0 -> -1+n2 >= 0, -1+n1 >= 0 -> -1+n1 >= 0, -1-n1+y^0 >= 0 -> -1-n1-(-1+n3)*n1+y^0 >= 0, -1+z^0 >= 0 -> -1+z^0 >= 0} Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)] Blocked [{}, {}, {12[T]}] Step with 6 Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {12[T]}, {}] Step with 8 Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {}, {12[T]}, {}, {}] Covered Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {12[T]}, {8[T]}] Step with 7 Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {}, {12[T]}, {8[T]}, {}] Covered Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {12[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)] Blocked [{}, {}, {6[T], 12[T]}] Step with 10 Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {}, {6[T], 12[T]}, {10[T]}] Acceleration Failed marked recursive suffix as redundant Step with 11 Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {}, {6[T], 12[T]}, {10[T]}, {11[T]}] Covered Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {}, {6[T], 12[T]}, {10[T], 11[T]}] Step with 12 Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)] Blocked [{}, {}, {6[T], 12[T]}, {10[T], 11[T]}, {12[T]}] Covered Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {}, {6[T], 12[T]}, {10[T], 11[T], 12[T]}] Step with 6 Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {6[T], 12[T]}, {10[T], 11[T], 12[T]}, {}] Step with 7 Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {}, {6[T], 12[T]}, {10[T], 11[T], 12[T]}, {}, {}] Covered Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {6[T], 12[T]}, {10[T], 11[T], 12[T]}, {7[T]}] Step with 8 Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {}, {6[T], 12[T]}, {10[T], 11[T], 12[T]}, {7[T]}, {}] Covered Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {6[T], 12[T]}, {10[T], 11[T], 12[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {}, {6[T], 12[T]}, {6[T], 10[T], 11[T], 12[T]}] Backtrack Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)] Blocked [{}, {}, {6[T], 10[T], 12[T]}] Step with 11 Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {}, {6[T], 10[T], 12[T]}, {11[T]}] Covered Trace 9[T], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)] Blocked [{}, {}, {6[T], 10[T], 11[T], 12[T]}] Backtrack Trace 9[T] Blocked [{}, {12[T]}] Step with 11 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {12[T]}, {11[T]}] Step with 12 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)] Blocked [{}, {12[T]}, {11[T]}, {12[T]}] Accelerate Start location: l3 Program variables: x^0 y^0 z^0 6: l0 -> l1 : (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 10: l0 -> l0 : x^0'=z^0, y^0'=-n+y^0, (-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0), cost: 1 11: l0 -> l0 : x^0'=-n2+x^0, (-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0), cost: 1 12: l0 -> l0 : x^0'=-n2+z^0, y^0'=-n3*n1+y^0, (-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0), cost: 1 13: l0 -> l0 : x^0'=-n2+z^0, y^0'=-n3*n1*n6+y^0, (-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0), cost: 1 7: l1 -> l0 : x^0'=z^0, y^0'=-1+y^0, T, cost: 1 8: l1 -> l0 : x^0'=-1+x^0, T, cost: 1 9: l3 -> l0 : T, cost: 1 Loop Acceleration Original rule: l0 -> l0 : x^0'=-n2+z^0, y^0'=-n3*n1+y^0, (-n2+z^0 >= 0 /\ 2-x^0 <= 0 /\ 1-x^0 <= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0), cost: 1 New rule: l0 -> l0 : x^0'=-n2+z^0, y^0'=-n3*n1*n6+y^0, (-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0), cost: 1 -n2+z^0 >= 0 [0]: monotonic increase yields -n2+z^0 >= 0 -1+x^0 >= 0 [0]: montonic decrease yields -1-n2+z^0 >= 0, dependencies: -2+x^0 >= 0 -1+x^0 >= 0 [1]: eventual decrease yields (-1+x^0 >= 0 /\ -1-n2+z^0 >= 0) -1+x^0 >= 0 [2]: eventual increase yields (n2+x^0-z^0 <= 0 /\ -1+x^0 >= 0) -1+n2 >= 0 [0]: monotonic increase yields -1+n2 >= 0 -1+n1 >= 0 [0]: monotonic increase yields -1+n1 >= 0 -n1-(-1+n3)*n1+y^0 >= 0 [0]: montonic decrease yields -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0, dependencies: -1-n1-(-1+n3)*n1+y^0 >= 0 -n1-(-1+n3)*n1+y^0 >= 0 [1]: eventual decrease yields (-n1-(-1+n3)*n1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0) -n1-(-1+n3)*n1+y^0 >= 0 [2]: eventual increase yields (-n1-(-1+n3)*n1+y^0 >= 0 /\ n3*n1 <= 0) -1+n3 >= 0 [0]: monotonic increase yields -1+n3 >= 0 -2+x^0 >= 0 [0]: eventual decrease yields (-2-n2+z^0 >= 0 /\ -2+x^0 >= 0) -2+x^0 >= 0 [1]: eventual increase yields (n2+x^0-z^0 <= 0 /\ -2+x^0 >= 0) -1-n1-(-1+n3)*n1+y^0 >= 0 [0]: montonic decrease yields -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0, dependencies: -1+y^0 >= 0 -1-n1-(-1+n3)*n1+y^0 >= 0 [1]: eventual decrease yields (-1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0) -1-n1-(-1+n3)*n1+y^0 >= 0 [2]: eventual increase yields (-1-n1-(-1+n3)*n1+y^0 >= 0 /\ n3*n1 <= 0) -1+z^0 >= 0 [0]: monotonic increase yields -1+z^0 >= 0 -1-n2+z^0 >= 0 [0]: monotonic increase yields -1-n2+z^0 >= 0 -1+y^0 >= 0 [0]: monotonic increase yields -1+y^0 >= 0, dependencies: -1-n1-(-1+n3)*n1+y^0 >= 0 Replacement map: {-n2+z^0 >= 0 -> -n2+z^0 >= 0, -1+x^0 >= 0 -> -1-n2+z^0 >= 0, -1+n2 >= 0 -> -1+n2 >= 0, -1+n1 >= 0 -> -1+n1 >= 0, -n1-(-1+n3)*n1+y^0 >= 0 -> -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0, -1+n3 >= 0 -> -1+n3 >= 0, -2+x^0 >= 0 -> (-2-n2+z^0 >= 0 /\ -2+x^0 >= 0), -1-n1-(-1+n3)*n1+y^0 >= 0 -> (-1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0), -1+z^0 >= 0 -> -1+z^0 >= 0, -1-n2+z^0 >= 0 -> -1-n2+z^0 >= 0, -1+y^0 >= 0 -> -1+y^0 >= 0} Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)] Blocked [{}, {12[T]}, {13[T]}] Step with 6 Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T]}, {13[T]}, {}] Step with 8 Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {12[T]}, {13[T]}, {}, {}] Covered Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T]}, {13[T]}, {8[T]}] Step with 7 Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {12[T]}, {13[T]}, {8[T]}, {}] Covered Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T]}, {13[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)] Blocked [{}, {12[T]}, {6[T], 13[T]}] Step with 10 Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {12[T]}, {6[T], 13[T]}, {10[T]}] Accelerate Start location: l3 Program variables: x^0 y^0 z^0 6: l0 -> l1 : (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 10: l0 -> l0 : x^0'=z^0, y^0'=-n+y^0, (-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0), cost: 1 11: l0 -> l0 : x^0'=-n2+x^0, (-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0), cost: 1 12: l0 -> l0 : x^0'=-n2+z^0, y^0'=-n3*n1+y^0, (-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0), cost: 1 13: l0 -> l0 : x^0'=-n2+z^0, y^0'=-n3*n1*n6+y^0, (-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0), cost: 1 14: l0 -> l0 : x^0'=z^0, y^0'=-n8*n-n61*n8*n14*n34+y^0, (-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0), cost: 1 7: l1 -> l0 : x^0'=z^0, y^0'=-1+y^0, T, cost: 1 8: l1 -> l0 : x^0'=-1+x^0, T, cost: 1 9: l3 -> l0 : T, cost: 1 Loop Acceleration Original rule: l0 -> l0 : x^0'=z^0, y^0'=-n-n61*n14*n34+y^0, (-1-n14*(-1+n34)-n14+y^0 >= 0 /\ -n-n61*n14*n34+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n14*(-1+n34)-n14-n14*(-1+n61)*n34+y^0 >= 0 /\ 3-z^0 <= 0 /\ -1+n34 >= 0 /\ -n14*(-1+n34)-n14-n14*(-1+n61)*n34+y^0 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ 2-z^0 <= 0 /\ 1-z^0 <= 0 /\ -1+z^0 >= 0 /\ -1+y^0 >= 0), cost: 1 New rule: l0 -> l0 : x^0'=z^0, y^0'=-n8*n-n61*n8*n14*n34+y^0, (-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0), cost: 1 -3+z^0 >= 0 [0]: monotonic increase yields -3+z^0 >= 0 -1-n14*(-1+n34)-n14+y^0 >= 0 [0]: montonic decrease yields -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0, dependencies: -1+n61 >= 0 -1+n14 >= 0 -1+n34 >= 0 -1+n >= 0 -1-n14*(-1+n34)-n14+y^0 >= 0 [1]: eventual decrease yields (-1-n14*(-1+n34)-n14+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0) -1-n14*(-1+n34)-n14+y^0 >= 0 [2]: eventual increase yields (-1-n14*(-1+n34)-n14+y^0 >= 0 /\ n+n61*n14*n34 <= 0) -2+z^0 >= 0 [0]: monotonic increase yields -2+z^0 >= 0 -n-n61*n14*n34+y^0 >= 0 [0]: montonic decrease yields -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0, dependencies: -1+y^0 >= 0 -n-n61*n14*n34+y^0 >= 0 [1]: eventual decrease yields (-n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -n-n61*n14*n34+y^0 >= 0) -n-n61*n14*n34+y^0 >= 0 [2]: eventual increase yields (-n-n61*n14*n34+y^0 >= 0 /\ n+n61*n14*n34 <= 0) -1+n61 >= 0 [0]: monotonic increase yields -1+n61 >= 0 -1+n14 >= 0 [0]: monotonic increase yields -1+n14 >= 0 -1-n14*(-1+n34)-n14-n14*(-1+n61)*n34+y^0 >= 0 [0]: montonic decrease yields -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0, dependencies: -1+n >= 0 -1+y^0 >= 0 -1-n14*(-1+n34)-n14-n14*(-1+n61)*n34+y^0 >= 0 [1]: eventual decrease yields (-1-n14*(-1+n34)-n14-n14*(-1+n61)*n34+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0) -1-n14*(-1+n34)-n14-n14*(-1+n61)*n34+y^0 >= 0 [2]: eventual increase yields (-1-n14*(-1+n34)-n14-n14*(-1+n61)*n34+y^0 >= 0 /\ n+n61*n14*n34 <= 0) -1+n34 >= 0 [0]: monotonic increase yields -1+n34 >= 0 -n14*(-1+n34)-n14-n14*(-1+n61)*n34+y^0 >= 0 [0]: montonic decrease yields -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0, dependencies: -1-n14*(-1+n34)-n14-n14*(-1+n61)*n34+y^0 >= 0 -n14*(-1+n34)-n14-n14*(-1+n61)*n34+y^0 >= 0 [1]: eventual increase yields (-n14*(-1+n34)-n14-n14*(-1+n61)*n34+y^0 >= 0 /\ n+n61*n14*n34 <= 0) -1+n >= 0 [0]: monotonic increase yields -1+n >= 0 -2+x^0 >= 0 [0]: monotonic increase yields -2+x^0 >= 0, dependencies: -3+z^0 >= 0 -1+z^0 >= 0 [0]: monotonic increase yields -1+z^0 >= 0 -1+y^0 >= 0 [0]: montonic decrease yields -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0, dependencies: -1+n61 >= 0 -1+n14 >= 0 -1+n34 >= 0 -1+n >= 0 -1+y^0 >= 0 [1]: eventual increase yields (n+n61*n14*n34 <= 0 /\ -1+y^0 >= 0) Replacement map: {-3+z^0 >= 0 -> -3+z^0 >= 0, -1-n14*(-1+n34)-n14+y^0 >= 0 -> -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0, -2+z^0 >= 0 -> -2+z^0 >= 0, -n-n61*n14*n34+y^0 >= 0 -> -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0, -1+n61 >= 0 -> -1+n61 >= 0, -1+n14 >= 0 -> -1+n14 >= 0, -1-n14*(-1+n34)-n14-n14*(-1+n61)*n34+y^0 >= 0 -> -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0, -1+n34 >= 0 -> -1+n34 >= 0, -n14*(-1+n34)-n14-n14*(-1+n61)*n34+y^0 >= 0 -> -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0, -1+n >= 0 -> -1+n >= 0, -2+x^0 >= 0 -> -2+x^0 >= 0, -1+z^0 >= 0 -> -1+z^0 >= 0, -1+y^0 >= 0 -> -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0} Trace 9[T], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)] Blocked [{}, {12[T]}, {14[T]}] Step with 6 Trace 9[T], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T]}, {14[T]}, {}] Step with 7 Trace 9[T], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {12[T]}, {14[T]}, {}, {}] Covered Trace 9[T], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T]}, {14[T]}, {7[T]}] Step with 8 Trace 9[T], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {12[T]}, {14[T]}, {7[T]}, {}] Covered Trace 9[T], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T]}, {14[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)] Blocked [{}, {12[T]}, {6[T], 14[T]}] Step with 10 Trace 9[T], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {12[T]}, {6[T], 14[T]}, {10[T]}] Covered Trace 9[T], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)] Blocked [{}, {12[T]}, {6[T], 10[T], 14[T]}] Step with 11 Trace 9[T], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {12[T]}, {6[T], 10[T], 14[T]}, {11[T]}] Covered Trace 9[T], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)] Blocked [{}, {12[T]}, {6[T], 10[T], 11[T], 14[T]}] Step with 12 Trace 9[T], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)] Blocked [{}, {12[T]}, {6[T], 10[T], 11[T], 14[T]}, {12[T]}] Covered Trace 9[T], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)] Blocked [{}, {12[T]}, {6[T], 10[T], 11[T], 12[T], 14[T]}] Step with 13 Trace 9[T], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)] Blocked [{}, {12[T]}, {6[T], 10[T], 11[T], 12[T], 14[T]}, {13[T]}] Covered Trace 9[T], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)] Blocked [{}, {12[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T]}] Backtrack Trace 9[T] Blocked [{}, {12[T], 14[T]}] Step with 13 Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)] Blocked [{}, {12[T], 14[T]}, {13[T]}] Step with 14 Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)] Blocked [{}, {12[T], 14[T]}, {13[T]}, {14[T]}] Covered Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)] Blocked [{}, {12[T], 14[T]}, {13[T], 14[T]}] Step with 6 Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 14[T]}, {13[T], 14[T]}, {}] Step with 8 Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {12[T], 14[T]}, {13[T], 14[T]}, {}, {}] Covered Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 14[T]}, {13[T], 14[T]}, {8[T]}] Step with 7 Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {12[T], 14[T]}, {13[T], 14[T]}, {8[T]}, {}] Covered Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 14[T]}, {13[T], 14[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)] Blocked [{}, {12[T], 14[T]}, {6[T], 13[T], 14[T]}] Step with 10 Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {12[T], 14[T]}, {6[T], 13[T], 14[T]}, {10[T]}] Covered Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)] Blocked [{}, {12[T], 14[T]}, {6[T], 10[T], 13[T], 14[T]}] Step with 11 Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {12[T], 14[T]}, {6[T], 10[T], 13[T], 14[T]}, {11[T]}] Covered Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)] Blocked [{}, {12[T], 14[T]}, {6[T], 10[T], 11[T], 13[T], 14[T]}] Step with 12 Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)] Blocked [{}, {12[T], 14[T]}, {6[T], 10[T], 11[T], 13[T], 14[T]}, {12[T]}] Covered Trace 9[T], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)] Blocked [{}, {12[T], 14[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T]}] Backtrack Trace 9[T] Blocked [{}, {12[T], 13[T], 14[T]}] Step with 6 Trace 9[T], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 13[T], 14[T]}, {}] Step with 7 Trace 9[T], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {12[T], 13[T], 14[T]}, {}, {}] Covered Trace 9[T], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 13[T], 14[T]}, {7[T]}] Step with 8 Trace 9[T], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {12[T], 13[T], 14[T]}, {7[T]}, {}] Covered Trace 9[T], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 13[T], 14[T]}, {7[T], 8[T]}] Backtrack Trace 9[T] Blocked [{}, {6[T], 12[T], 13[T], 14[T]}] Step with 10 Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T]}, {10[T]}] Step with 11 Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T]}, {10[T]}, {11[T]}] Covered Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T]}, {10[T], 11[T]}] Step with 12 Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T]}, {10[T], 11[T]}, {12[T]}] Covered Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T]}, {10[T], 11[T], 12[T]}] Step with 13 Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T]}, {10[T], 11[T], 12[T]}, {13[T]}] Covered Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T]}, {10[T], 11[T], 12[T], 13[T]}] Step with 14 Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T]}, {10[T], 11[T], 12[T], 13[T]}, {14[T]}] Covered Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T]}, {10[T], 11[T], 12[T], 13[T], 14[T]}] Step with 6 Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T]}, {10[T], 11[T], 12[T], 13[T], 14[T]}, {}] Step with 8 Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {6[T], 12[T], 13[T], 14[T]}, {10[T], 11[T], 12[T], 13[T], 14[T]}, {}, {}] Covered Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T]}, {10[T], 11[T], 12[T], 13[T], 14[T]}, {8[T]}] Step with 7 Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {6[T], 12[T], 13[T], 14[T]}, {10[T], 11[T], 12[T], 13[T], 14[T]}, {8[T]}, {}] Covered Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T]}, {10[T], 11[T], 12[T], 13[T], 14[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T]}] Backtrack Trace 9[T] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}] Step with 11 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {11[T]}] Step with 12 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {11[T]}, {12[T]}] Covered Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {11[T], 12[T]}] Step with 13 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {11[T], 12[T]}, {13[T]}] Covered Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {11[T], 12[T], 13[T]}] Step with 14 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {11[T], 12[T], 13[T]}, {14[T]}] Covered Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {11[T], 12[T], 13[T], 14[T]}] Step with 6 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {11[T], 12[T], 13[T], 14[T]}, {}] Step with 7 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {11[T], 12[T], 13[T], 14[T]}, {}, {}] Covered Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {11[T], 12[T], 13[T], 14[T]}, {7[T]}] Step with 8 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {11[T], 12[T], 13[T], 14[T]}, {7[T]}, {}] Covered Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {11[T], 12[T], 13[T], 14[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {6[T], 11[T], 12[T], 13[T], 14[T]}] Step with 10 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {6[T], 11[T], 12[T], 13[T], 14[T]}, {10[T]}] Accelerate Start location: l3 Program variables: x^0 y^0 z^0 6: l0 -> l1 : (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 10: l0 -> l0 : x^0'=z^0, y^0'=-n+y^0, (-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0), cost: 1 11: l0 -> l0 : x^0'=-n2+x^0, (-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0), cost: 1 12: l0 -> l0 : x^0'=-n2+z^0, y^0'=-n3*n1+y^0, (-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0), cost: 1 13: l0 -> l0 : x^0'=-n2+z^0, y^0'=-n3*n1*n6+y^0, (-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0), cost: 1 14: l0 -> l0 : x^0'=z^0, y^0'=-n8*n-n61*n8*n14*n34+y^0, (-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0), cost: 1 15: l0 -> l0 : x^0'=z^0, y^0'=-n*n42+y^0, (-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0), cost: 1 7: l1 -> l0 : x^0'=z^0, y^0'=-1+y^0, T, cost: 1 8: l1 -> l0 : x^0'=-1+x^0, T, cost: 1 9: l3 -> l0 : T, cost: 1 Loop Acceleration Original rule: l0 -> l0 : x^0'=z^0, y^0'=-n+y^0, (2-x^0 <= 0 /\ 1-x^0 <= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0 /\ -1+y^0 >= 0), cost: 1 New rule: l0 -> l0 : x^0'=z^0, y^0'=-n*n42+y^0, (-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0), cost: 1 -1+x^0 >= 0 [0]: montonic decrease yields -1+z^0 >= 0, dependencies: -2+x^0 >= 0 -1+x^0 >= 0 [1]: eventual decrease yields (-1+x^0 >= 0 /\ -1+z^0 >= 0) -1+x^0 >= 0 [2]: eventual increase yields (x^0-z^0 <= 0 /\ -1+x^0 >= 0) -n+y^0 >= 0 [0]: montonic decrease yields -n-n*(-1+n42)+y^0 >= 0, dependencies: -1+n >= 0 -n+y^0 >= 0 [1]: eventual decrease yields (-n+y^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0) -n+y^0 >= 0 [2]: eventual increase yields (n <= 0 /\ -n+y^0 >= 0) -1+n >= 0 [0]: monotonic increase yields -1+n >= 0 -2+x^0 >= 0 [0]: eventual decrease yields (-2+z^0 >= 0 /\ -2+x^0 >= 0) -2+x^0 >= 0 [1]: eventual increase yields (x^0-z^0 <= 0 /\ -2+x^0 >= 0) -1+z^0 >= 0 [0]: monotonic increase yields -1+z^0 >= 0 -1+y^0 >= 0 [0]: montonic decrease yields -1-n*(-1+n42)+y^0 >= 0, dependencies: -1+n >= 0 -1+y^0 >= 0 [1]: eventual increase yields (n <= 0 /\ -1+y^0 >= 0) Replacement map: {-1+x^0 >= 0 -> -1+z^0 >= 0, -n+y^0 >= 0 -> -n-n*(-1+n42)+y^0 >= 0, -1+n >= 0 -> -1+n >= 0, -2+x^0 >= 0 -> (-2+z^0 >= 0 /\ -2+x^0 >= 0), -1+z^0 >= 0 -> -1+z^0 >= 0, -1+y^0 >= 0 -> -1-n*(-1+n42)+y^0 >= 0} Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {15[T]}] Step with 6 Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {15[T]}, {}] Step with 8 Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {15[T]}, {}, {}] Covered Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {15[T]}, {8[T]}] Step with 7 Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {15[T]}, {8[T]}, {}] Covered Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {15[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {6[T], 15[T]}] Step with 10 Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {6[T], 15[T]}, {10[T]}] Covered Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {6[T], 10[T], 15[T]}] Step with 11 Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {6[T], 10[T], 15[T]}, {11[T]}] Covered Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {6[T], 10[T], 11[T], 15[T]}] Step with 12 Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {6[T], 10[T], 11[T], 15[T]}, {12[T]}] Covered Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {6[T], 10[T], 11[T], 12[T], 15[T]}] Step with 13 Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {6[T], 10[T], 11[T], 12[T], 15[T]}, {13[T]}] Covered Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 15[T]}] Step with 14 Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 15[T]}, {14[T]}] Covered Trace 9[T], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T]}] Backtrack Trace 9[T] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}] Step with 11 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {11[T]}] Step with 12 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 12[(-n2+z^0 >= 0 /\ -1+x^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n3 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {11[T]}, {12[T]}] Covered Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {11[T], 12[T]}] Step with 13 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 13[(-2-n2+z^0 >= 0 /\ -n2+z^0 >= 0 /\ -1-n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n2 >= 0 /\ -1+n1 >= 0 /\ -1+n3 >= 0 /\ -2+x^0 >= 0 /\ -1-n1-(-1+n3)*n1+y^0 >= 0 /\ -1+n6 >= 0 /\ -1+z^0 >= 0 /\ -1-n2+z^0 >= 0 /\ -1+y^0 >= 0 /\ -n3*n1*(-1+n6)-n1-(-1+n3)*n1+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {11[T], 12[T]}, {13[T]}] Covered Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {11[T], 12[T], 13[T]}] Step with 14 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 14[(-3+z^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n8 >= 0 /\ -n61*n14*(-1+n8)*n34-n-n61*n14*n34-(-1+n8)*n+y^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-(-1+n8)*n+y^0 >= 0 /\ -1+n61 >= 0 /\ -1+n14 >= 0 /\ -1-n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -1+n34 >= 0 /\ -1+n >= 0 /\ -n61*n14*(-1+n8)*n34-n14*(-1+n34)-n14-n14*(-1+n61)*n34-(-1+n8)*n+y^0 >= 0 /\ -2+x^0 >= 0 /\ -1+z^0 >= 0 /\ -1-n61*n14*(-1+n8)*n34-(-1+n8)*n+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {11[T], 12[T], 13[T]}, {14[T]}] Covered Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {11[T], 12[T], 13[T], 14[T]}] Step with 15 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 15[(-1-n*(-1+n42)+y^0 >= 0 /\ -2+z^0 >= 0 /\ -1+n42 >= 0 /\ -1+n >= 0 /\ -2+x^0 >= 0 /\ -n-n*(-1+n42)+y^0 >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {11[T], 12[T], 13[T], 14[T]}, {15[T]}] Covered Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {11[T], 12[T], 13[T], 14[T], 15[T]}] Step with 6 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {11[T], 12[T], 13[T], 14[T], 15[T]}, {}] Step with 7 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {11[T], 12[T], 13[T], 14[T], 15[T]}, {}, {}] Covered Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {11[T], 12[T], 13[T], 14[T], 15[T]}, {7[T]}] Step with 8 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {11[T], 12[T], 13[T], 14[T], 15[T]}, {7[T]}, {}] Covered Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {11[T], 12[T], 13[T], 14[T], 15[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {6[T], 11[T], 12[T], 13[T], 14[T], 15[T]}] Step with 10 Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)], 10[(-1+x^0 >= 0 /\ -n+y^0 >= 0 /\ -1+n >= 0 /\ -1+z^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {6[T], 11[T], 12[T], 13[T], 14[T], 15[T]}, {10[T]}] Covered Trace 9[T], 11[(-1+n2 >= 0 /\ -n2+x^0 >= 0 /\ -1+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T]}] Backtrack Trace 9[T] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T]}] Backtrack Trace Blocked [{9[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b