unknown Initial ITS Start location: l3 Program variables: x^0 y^0 0: l0 -> l1 : x^0'=x^post1, y^0'=y^post1, (1-x^0 <= 0 /\ -x^post1+x^0 == 0 /\ -y^post1+y^0 == 0 /\ 1-y^0 <= 0), cost: 1 1: l1 -> l0 : x^0'=x^post2, y^0'=y^post2, (0 == 0 /\ 1+y^post2-y^0 == 0), cost: 1 2: l1 -> l0 : x^0'=x^post3, y^0'=y^post3, (-y^post3+y^0 == 0 /\ 1+x^post3-x^0 == 0), cost: 1 3: l2 -> l0 : x^0'=x^post4, y^0'=y^post4, (-x^post4+x^0 == 0 /\ -y^post4+y^0 == 0), cost: 1 4: l3 -> l2 : x^0'=x^post5, y^0'=y^post5, (x^0-x^post5 == 0 /\ -y^post5+y^0 == 0), cost: 1 Chained Linear Paths Start location: l3 Program variables: x^0 y^0 0: l0 -> l1 : x^0'=x^post1, y^0'=y^post1, (1-x^0 <= 0 /\ -x^post1+x^0 == 0 /\ -y^post1+y^0 == 0 /\ 1-y^0 <= 0), cost: 1 1: l1 -> l0 : x^0'=x^post2, y^0'=y^post2, (0 == 0 /\ 1+y^post2-y^0 == 0), cost: 1 2: l1 -> l0 : x^0'=x^post3, y^0'=y^post3, (-y^post3+y^0 == 0 /\ 1+x^post3-x^0 == 0), cost: 1 5: l3 -> l0 : x^0'=x^post4, y^0'=y^post4, (x^0-x^post5 == 0 /\ -y^post5+y^0 == 0 /\ y^post5-y^post4 == 0 /\ -x^post4+x^post5 == 0), cost: 1 Eliminating location l2 by chaining: Applied chaining First rule: l3 -> l2 : x^0'=x^post5, y^0'=y^post5, (x^0-x^post5 == 0 /\ -y^post5+y^0 == 0), cost: 1 Second rule: l2 -> l0 : x^0'=x^post4, y^0'=y^post4, (-x^post4+x^0 == 0 /\ -y^post4+y^0 == 0), cost: 1 New rule: l3 -> l0 : x^0'=x^post4, y^0'=y^post4, (x^0-x^post5 == 0 /\ -y^post5+y^0 == 0 /\ y^post5-y^post4 == 0 /\ -x^post4+x^post5 == 0), cost: 1 Applied deletion Removed the following rules: 3 4 Simplified Transitions Start location: l3 Program variables: x^0 y^0 6: l0 -> l1 : (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 7: l1 -> l0 : x^0'=x^post2, 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, (1-x^0 <= 0 /\ -x^post1+x^0 == 0 /\ -y^post1+y^0 == 0 /\ 1-y^0 <= 0), cost: 1 New rule: l0 -> l1 : x^0'=x^0, y^0'=y^0, (0 == 0 /\ 1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 propagated equality x^post1 = x^0 propagated equality y^post1 = y^0 Simplified Guard Original rule: l0 -> l1 : x^0'=x^0, y^0'=y^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, (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, (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, (0 == 0 /\ 1+y^post2-y^0 == 0), cost: 1 New rule: l1 -> l0 : x^0'=x^post2, y^0'=-1+y^0, 0 == 0, cost: 1 propagated equality y^post2 = -1+y^0 Simplified Guard Original rule: l1 -> l0 : x^0'=x^post2, y^0'=-1+y^0, 0 == 0, cost: 1 New rule: l1 -> l0 : x^0'=x^post2, y^0'=-1+y^0, T, cost: 1 Propagated Equalities Original rule: l1 -> l0 : x^0'=x^post3, y^0'=y^post3, (-y^post3+y^0 == 0 /\ 1+x^post3-x^0 == 0), cost: 1 New rule: l1 -> l0 : x^0'=-1+x^0, y^0'=y^0, 0 == 0, cost: 1 propagated equality y^post3 = y^0 propagated equality x^post3 = -1+x^0 Simplified Guard Original rule: l1 -> l0 : x^0'=-1+x^0, y^0'=y^0, 0 == 0, cost: 1 New rule: l1 -> l0 : x^0'=-1+x^0, y^0'=y^0, T, cost: 1 Removed Trivial Updates Original rule: l1 -> l0 : x^0'=-1+x^0, y^0'=y^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, (x^0-x^post5 == 0 /\ -y^post5+y^0 == 0 /\ y^post5-y^post4 == 0 /\ -x^post4+x^post5 == 0), cost: 1 New rule: l3 -> l0 : x^0'=x^post5, y^0'=y^post5, (0 == 0 /\ x^0-x^post5 == 0 /\ -y^post5+y^0 == 0), cost: 1 propagated equality y^post4 = y^post5 propagated equality x^post4 = x^post5 Propagated Equalities Original rule: l3 -> l0 : x^0'=x^post5, y^0'=y^post5, (0 == 0 /\ x^0-x^post5 == 0 /\ -y^post5+y^0 == 0), cost: 1 New rule: l3 -> l0 : x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1 propagated equality x^post5 = x^0 propagated equality y^post5 = y^0 Simplified Guard Original rule: l3 -> l0 : x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1 New rule: l3 -> l0 : x^0'=x^0, y^0'=y^0, T, cost: 1 Removed Trivial Updates Original rule: l3 -> l0 : x^0'=x^0, y^0'=y^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 6: l0 -> l1 : (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 10: l0 -> l0 : x^0'=x^post2, y^0'=-n+y^0, (-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0), cost: 1 7: l1 -> l0 : x^0'=x^post2, 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'=x^post2, y^0'=-1+y^0, (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 New rule: l0 -> l0 : x^0'=x^post2, y^0'=-n+y^0, (-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0), cost: 1 -1+x^0 >= 0 [0]: eventual decrease yields (-1+x^0 >= 0 /\ -1+x^post2 >= 0) -1+x^0 >= 0 [1]: eventual increase yields (-1+x^0 >= 0 /\ x^0-x^post2 <= 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+x^post2 >= 0), -1+y^0 >= 0 -> -n+y^0 >= 0} Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)] Blocked [{}, {}, {10[T]}] Step with 6 Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {10[T]}, {}] Step with 7 Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {}, {10[T]}, {}, {}] Covered Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {10[T]}, {7[T]}] Step with 8 Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^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 6: l0 -> l1 : (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 10: l0 -> l0 : x^0'=x^post2, y^0'=-n+y^0, (-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0), cost: 1 11: l0 -> l0 : x^0'=-n2+x^0, (-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0), cost: 1 7: l1 -> l0 : x^0'=x^post2, 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, (-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 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+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {10[T]}, {11[T]}] Accelerate Start location: l3 Program variables: x^0 y^0 6: l0 -> l1 : (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 10: l0 -> l0 : x^0'=x^post2, y^0'=-n+y^0, (-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0), cost: 1 11: l0 -> l0 : x^0'=-n2+x^0, (-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0), cost: 1 12: l0 -> l0 : x^0'=-n2+x^post22, y^0'=-n3*n1+y^0, (-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0), cost: 1 7: l1 -> l0 : x^0'=x^post2, 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+x^post22, y^0'=-n1+y^0, (-n1+y^0 >= 0 /\ -n2+x^post22 >= 0 /\ -1+x^0 >= 0 /\ -1+x^post22 >= 0 /\ -1-n1+y^0 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0), cost: 1 New rule: l0 -> l0 : x^0'=-n2+x^post22, y^0'=-n3*n1+y^0, (-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0), cost: 1 -n1+y^0 >= 0 [0]: montonic decrease yields -n1-n1*(-1+n3)+y^0 >= 0, dependencies: -1-n1+y^0 >= 0 -n1+y^0 >= 0 [1]: eventual decrease yields (-n1+y^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0) -n1+y^0 >= 0 [2]: eventual increase yields (-n1+y^0 >= 0 /\ n1 <= 0) -n2+x^post22 >= 0 [0]: monotonic increase yields -n2+x^post22 >= 0 -1+x^0 >= 0 [0]: eventual decrease yields (-1+x^0 >= 0 /\ -1-n2+x^post22 >= 0) -1+x^0 >= 0 [1]: eventual increase yields (-1+x^0 >= 0 /\ n2+x^0-x^post22 <= 0) -1+x^post22 >= 0 [0]: monotonic increase yields -1+x^post22 >= 0 -1-n1+y^0 >= 0 [0]: montonic decrease yields -1-n1-n1*(-1+n3)+y^0 >= 0, dependencies: -1+n1 >= 0 -1-n1+y^0 >= 0 [1]: eventual decrease yields (-1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1+y^0 >= 0) -1-n1+y^0 >= 0 [2]: eventual increase yields (n1 <= 0 /\ -1-n1+y^0 >= 0) -1+n1 >= 0 [0]: monotonic increase yields -1+n1 >= 0 -1+n2 >= 0 [0]: monotonic increase yields -1+n2 >= 0 Replacement map: {-n1+y^0 >= 0 -> -n1-n1*(-1+n3)+y^0 >= 0, -n2+x^post22 >= 0 -> -n2+x^post22 >= 0, -1+x^0 >= 0 -> (-1+x^0 >= 0 /\ -1-n2+x^post22 >= 0), -1+x^post22 >= 0 -> -1+x^post22 >= 0, -1-n1+y^0 >= 0 -> -1-n1-n1*(-1+n3)+y^0 >= 0, -1+n1 >= 0 -> -1+n1 >= 0, -1+n2 >= 0 -> -1+n2 >= 0} Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {12[T]}] Step with 6 Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {12[T]}, {}] Step with 8 Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {}, {12[T]}, {}, {}] Covered Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {12[T]}, {8[T]}] Step with 7 Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {}, {12[T]}, {8[T]}, {}] Covered Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {12[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {6[T], 12[T]}] Step with 10 Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)] Blocked [{}, {}, {6[T], 12[T]}, {10[T]}] Accelerate Start location: l3 Program variables: x^0 y^0 6: l0 -> l1 : (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 10: l0 -> l0 : x^0'=x^post2, y^0'=-n+y^0, (-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0), cost: 1 11: l0 -> l0 : x^0'=-n2+x^0, (-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0), cost: 1 12: l0 -> l0 : x^0'=-n2+x^post22, y^0'=-n3*n1+y^0, (-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0), cost: 1 13: l0 -> l0 : x^0'=x^post2, y^0'=-n*n5-n11*n5*n31+y^0, (-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0), cost: 1 7: l1 -> l0 : x^0'=x^post2, 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'=x^post2, y^0'=-n11*n31-n+y^0, (-1+n >= 0 /\ -1+x^0 >= 0 /\ -n11*(-1+n31)-n11+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1-n11*(-1+n31)-n11+y^0 >= 0 /\ -1+n11 >= 0 /\ -1+n31 >= 0), cost: 1 New rule: l0 -> l0 : x^0'=x^post2, y^0'=-n*n5-n11*n5*n31+y^0, (-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0), cost: 1 -1+n >= 0 [0]: monotonic increase yields -1+n >= 0 -1+x^0 >= 0 [0]: eventual decrease yields (-1+x^0 >= 0 /\ -1+x^post2 >= 0) -1+x^0 >= 0 [1]: eventual increase yields (-1+x^0 >= 0 /\ x^0-x^post2 <= 0) -n11*(-1+n31)-n11+y^0 >= 0 [0]: montonic decrease yields -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0, dependencies: -1-n11*(-1+n31)-n11+y^0 >= 0 -n11*(-1+n31)-n11+y^0 >= 0 [1]: eventual decrease yields (-n11*(-1+n31)-n11+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0) -n11*(-1+n31)-n11+y^0 >= 0 [2]: eventual increase yields (n11*n31+n <= 0 /\ -n11*(-1+n31)-n11+y^0 >= 0) -n11*n31-n+y^0 >= 0 [0]: montonic decrease yields -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0, dependencies: -1-n11*(-1+n31)-n11+y^0 >= 0 -1+n11 >= 0 -1+n31 >= 0 -n11*n31-n+y^0 >= 0 [1]: eventual decrease yields (-n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0) -n11*n31-n+y^0 >= 0 [2]: eventual increase yields (n11*n31+n <= 0 /\ -n11*n31-n+y^0 >= 0) -1+x^post2 >= 0 [0]: monotonic increase yields -1+x^post2 >= 0 -1-n11*(-1+n31)-n11+y^0 >= 0 [0]: montonic decrease yields -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0, dependencies: -1+n >= 0 -n11*n31-n+y^0 >= 0 -1-n11*(-1+n31)-n11+y^0 >= 0 [1]: eventual increase yields (n11*n31+n <= 0 /\ -1-n11*(-1+n31)-n11+y^0 >= 0) -1+n11 >= 0 [0]: monotonic increase yields -1+n11 >= 0 -1+n31 >= 0 [0]: monotonic increase yields -1+n31 >= 0 Replacement map: {-1+n >= 0 -> -1+n >= 0, -1+x^0 >= 0 -> (-1+x^0 >= 0 /\ -1+x^post2 >= 0), -n11*(-1+n31)-n11+y^0 >= 0 -> -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0, -n11*n31-n+y^0 >= 0 -> (-n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0), -1+x^post2 >= 0 -> -1+x^post2 >= 0, -1-n11*(-1+n31)-n11+y^0 >= 0 -> -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0, -1+n11 >= 0 -> -1+n11 >= 0, -1+n31 >= 0 -> -1+n31 >= 0} Trace 9[T], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)] Blocked [{}, {}, {13[T]}] Step with 6 Trace 9[T], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {13[T]}, {}] Step with 7 Trace 9[T], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {}, {13[T]}, {}, {}] Covered Trace 9[T], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {13[T]}, {7[T]}] Step with 8 Trace 9[T], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {}, {13[T]}, {7[T]}, {}] Covered Trace 9[T], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {}, {13[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)] Blocked [{}, {}, {6[T], 13[T]}] Step with 10 Trace 9[T], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)] Blocked [{}, {}, {6[T], 13[T]}, {10[T]}] Covered Trace 9[T], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)] Blocked [{}, {}, {6[T], 10[T], 13[T]}] Step with 11 Trace 9[T], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {6[T], 10[T], 13[T]}, {11[T]}] Covered Trace 9[T], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)] Blocked [{}, {}, {6[T], 10[T], 11[T], 13[T]}] Step with 12 Trace 9[T], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {6[T], 10[T], 11[T], 13[T]}, {12[T]}] Covered Trace 9[T], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)] Blocked [{}, {}, {6[T], 10[T], 11[T], 12[T], 13[T]}] Backtrack Trace 9[T] Blocked [{}, {13[T]}] Step with 12 Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {13[T]}, {12[T]}] Step with 13 Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)] Blocked [{}, {13[T]}, {12[T]}, {13[T]}] Covered Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {13[T]}, {12[T], 13[T]}] Step with 6 Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {13[T]}, {12[T], 13[T]}, {}] Step with 8 Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {13[T]}, {12[T], 13[T]}, {}, {}] Covered Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {13[T]}, {12[T], 13[T]}, {8[T]}] Step with 7 Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {13[T]}, {12[T], 13[T]}, {8[T]}, {}] Covered Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {13[T]}, {12[T], 13[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {13[T]}, {6[T], 12[T], 13[T]}] Step with 10 Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)] Blocked [{}, {13[T]}, {6[T], 12[T], 13[T]}, {10[T]}] Covered Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {13[T]}, {6[T], 10[T], 12[T], 13[T]}] Step with 11 Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {13[T]}, {6[T], 10[T], 12[T], 13[T]}, {11[T]}] Covered Trace 9[T], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {13[T]}, {6[T], 10[T], 11[T], 12[T], 13[T]}] Backtrack Trace 9[T] Blocked [{}, {12[T], 13[T]}] Step with 11 Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {12[T], 13[T]}, {11[T]}] Step with 12 Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {12[T], 13[T]}, {11[T]}, {12[T]}] Accelerate Start location: l3 Program variables: x^0 y^0 6: l0 -> l1 : (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 10: l0 -> l0 : x^0'=x^post2, y^0'=-n+y^0, (-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0), cost: 1 11: l0 -> l0 : x^0'=-n2+x^0, (-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0), cost: 1 12: l0 -> l0 : x^0'=-n2+x^post22, y^0'=-n3*n1+y^0, (-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0), cost: 1 13: l0 -> l0 : x^0'=x^post2, y^0'=-n*n5-n11*n5*n31+y^0, (-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0), cost: 1 14: l0 -> l0 : x^0'=-n2+x^post22, y^0'=-n3*n1*n10+y^0, (-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0), cost: 1 7: l1 -> l0 : x^0'=x^post2, 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+x^post22, y^0'=-n3*n1+y^0, (2-x^0 <= 0 /\ -n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ 1-x^0 <= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0), cost: 1 New rule: l0 -> l0 : x^0'=-n2+x^post22, y^0'=-n3*n1*n10+y^0, (-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0), cost: 1 -n2+x^post22 >= 0 [0]: monotonic increase yields -n2+x^post22 >= 0 -1-n1-n1*(-1+n3)+y^0 >= 0 [0]: montonic decrease yields -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0, dependencies: -1+y^0 >= 0 -1-n1-n1*(-1+n3)+y^0 >= 0 [1]: eventual decrease yields (-1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0) -1-n1-n1*(-1+n3)+y^0 >= 0 [2]: eventual increase yields (-1-n1-n1*(-1+n3)+y^0 >= 0 /\ n3*n1 <= 0) -1+x^0 >= 0 [0]: montonic decrease yields -1-n2+x^post22 >= 0, dependencies: -2+x^0 >= 0 -1+x^0 >= 0 [1]: eventual decrease yields (-1+x^0 >= 0 /\ -1-n2+x^post22 >= 0) -1+x^0 >= 0 [2]: eventual increase yields (-1+x^0 >= 0 /\ n2+x^0-x^post22 <= 0) -n1-n1*(-1+n3)+y^0 >= 0 [0]: montonic decrease yields -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0, dependencies: -1-n1-n1*(-1+n3)+y^0 >= 0 -n1-n1*(-1+n3)+y^0 >= 0 [1]: eventual increase yields (n3*n1 <= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0) -1-n2+x^post22 >= 0 [0]: monotonic increase yields -1-n2+x^post22 >= 0 -1+x^post22 >= 0 [0]: monotonic increase yields -1+x^post22 >= 0 -2+x^0 >= 0 [0]: eventual decrease yields (-2-n2+x^post22 >= 0 /\ -2+x^0 >= 0) -2+x^0 >= 0 [1]: eventual increase yields (n2+x^0-x^post22 <= 0 /\ -2+x^0 >= 0) -1+n3 >= 0 [0]: monotonic increase yields -1+n3 >= 0 -1+n1 >= 0 [0]: monotonic increase yields -1+n1 >= 0 -1+y^0 >= 0 [0]: monotonic increase yields -1+y^0 >= 0, dependencies: -1-n1-n1*(-1+n3)+y^0 >= 0 -1+n2 >= 0 [0]: monotonic increase yields -1+n2 >= 0 Replacement map: {-n2+x^post22 >= 0 -> -n2+x^post22 >= 0, -1-n1-n1*(-1+n3)+y^0 >= 0 -> (-1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0), -1+x^0 >= 0 -> -1-n2+x^post22 >= 0, -n1-n1*(-1+n3)+y^0 >= 0 -> -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0, -1-n2+x^post22 >= 0 -> -1-n2+x^post22 >= 0, -1+x^post22 >= 0 -> -1+x^post22 >= 0, -2+x^0 >= 0 -> (-2-n2+x^post22 >= 0 /\ -2+x^0 >= 0), -1+n3 >= 0 -> -1+n3 >= 0, -1+n1 >= 0 -> -1+n1 >= 0, -1+y^0 >= 0 -> -1+y^0 >= 0, -1+n2 >= 0 -> -1+n2 >= 0} Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {12[T], 13[T]}, {14[T]}] Step with 6 Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 13[T]}, {14[T]}, {}] Step with 7 Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {12[T], 13[T]}, {14[T]}, {}, {}] Covered Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 13[T]}, {14[T]}, {7[T]}] Step with 8 Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {12[T], 13[T]}, {14[T]}, {7[T]}, {}] Covered Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 13[T]}, {14[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {12[T], 13[T]}, {6[T], 14[T]}] Step with 10 Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)] Blocked [{}, {12[T], 13[T]}, {6[T], 14[T]}, {10[T]}] Accelerate Start location: l3 Program variables: x^0 y^0 6: l0 -> l1 : (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 10: l0 -> l0 : x^0'=x^post2, y^0'=-n+y^0, (-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0), cost: 1 11: l0 -> l0 : x^0'=-n2+x^0, (-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0), cost: 1 12: l0 -> l0 : x^0'=-n2+x^post22, y^0'=-n3*n1+y^0, (-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0), cost: 1 13: l0 -> l0 : x^0'=x^post2, y^0'=-n*n5-n11*n5*n31+y^0, (-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0), cost: 1 14: l0 -> l0 : x^0'=-n2+x^post22, y^0'=-n3*n1*n10+y^0, (-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0), cost: 1 15: l0 -> l0 : x^0'=x^post2, y^0'=-n17*n-n101*n17*n35*n15+y^0, (-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0), cost: 1 7: l1 -> l0 : x^0'=x^post2, 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'=x^post2, y^0'=-n101*n35*n15-n+y^0, (-1+n >= 0 /\ -1-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n+y^0 >= 0 /\ -1+n15 >= 0 /\ -1-(-1+n101)*n35*n15-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+y^0 >= 0), cost: 1 New rule: l0 -> l0 : x^0'=x^post2, y^0'=-n17*n-n101*n17*n35*n15+y^0, (-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0), cost: 1 -1+n >= 0 [0]: monotonic increase yields -1+n >= 0 -1-n15-(-1+n35)*n15+y^0 >= 0 [0]: montonic decrease yields -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0, dependencies: -1+n >= 0 -1+n101 >= 0 -1+n35 >= 0 -1+n15 >= 0 -1-n15-(-1+n35)*n15+y^0 >= 0 [1]: eventual decrease yields (-1-n15-(-1+n35)*n15+y^0 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0) -1-n15-(-1+n35)*n15+y^0 >= 0 [2]: eventual increase yields (-1-n15-(-1+n35)*n15+y^0 >= 0 /\ n101*n35*n15+n <= 0) -(-1+n101)*n35*n15-n15-(-1+n35)*n15+y^0 >= 0 [0]: montonic decrease yields -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0, dependencies: -1-(-1+n101)*n35*n15-n15-(-1+n35)*n15+y^0 >= 0 -(-1+n101)*n35*n15-n15-(-1+n35)*n15+y^0 >= 0 [1]: eventual decrease yields (-(-1+n101)*n35*n15-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0) -(-1+n101)*n35*n15-n15-(-1+n35)*n15+y^0 >= 0 [2]: eventual increase yields (-(-1+n101)*n35*n15-n15-(-1+n35)*n15+y^0 >= 0 /\ n101*n35*n15+n <= 0) -1+n101 >= 0 [0]: monotonic increase yields -1+n101 >= 0 -1+n35 >= 0 [0]: monotonic increase yields -1+n35 >= 0 -1+x^post2 >= 0 [0]: monotonic increase yields -1+x^post2 >= 0 -2+x^0 >= 0 [0]: eventual decrease yields (-2+x^post2 >= 0 /\ -2+x^0 >= 0) -2+x^0 >= 0 [1]: eventual increase yields (x^0-x^post2 <= 0 /\ -2+x^0 >= 0) -n101*n35*n15-n+y^0 >= 0 [0]: montonic decrease yields -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0, dependencies: -1+y^0 >= 0 -n101*n35*n15-n+y^0 >= 0 [1]: eventual decrease yields (-n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -n101*n35*n15-n+y^0 >= 0) -n101*n35*n15-n+y^0 >= 0 [2]: eventual increase yields (-n101*n35*n15-n+y^0 >= 0 /\ n101*n35*n15+n <= 0) -1+n15 >= 0 [0]: monotonic increase yields -1+n15 >= 0 -1-(-1+n101)*n35*n15-n15-(-1+n35)*n15+y^0 >= 0 [0]: montonic decrease yields -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0, dependencies: -1+n >= 0 -1+y^0 >= 0 -1-(-1+n101)*n35*n15-n15-(-1+n35)*n15+y^0 >= 0 [1]: eventual decrease yields (-1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1-(-1+n101)*n35*n15-n15-(-1+n35)*n15+y^0 >= 0) -1-(-1+n101)*n35*n15-n15-(-1+n35)*n15+y^0 >= 0 [2]: eventual increase yields (n101*n35*n15+n <= 0 /\ -1-(-1+n101)*n35*n15-n15-(-1+n35)*n15+y^0 >= 0) -1+y^0 >= 0 [0]: montonic decrease yields -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0, dependencies: -1+n >= 0 -1+n101 >= 0 -1+n35 >= 0 -1+n15 >= 0 -1+y^0 >= 0 [1]: eventual increase yields (n101*n35*n15+n <= 0 /\ -1+y^0 >= 0) Replacement map: {-1+n >= 0 -> -1+n >= 0, -1-n15-(-1+n35)*n15+y^0 >= 0 -> -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0, -(-1+n101)*n35*n15-n15-(-1+n35)*n15+y^0 >= 0 -> -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0, -1+n101 >= 0 -> -1+n101 >= 0, -1+n35 >= 0 -> -1+n35 >= 0, -1+x^post2 >= 0 -> -1+x^post2 >= 0, -2+x^0 >= 0 -> (-2+x^post2 >= 0 /\ -2+x^0 >= 0), -n101*n35*n15-n+y^0 >= 0 -> -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0, -1+n15 >= 0 -> -1+n15 >= 0, -1-(-1+n101)*n35*n15-n15-(-1+n35)*n15+y^0 >= 0 -> -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0, -1+y^0 >= 0 -> -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0} Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)] Blocked [{}, {12[T], 13[T]}, {15[T]}] Step with 6 Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 13[T]}, {15[T]}, {}] Step with 8 Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {12[T], 13[T]}, {15[T]}, {}, {}] Covered Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 13[T]}, {15[T]}, {8[T]}] Step with 7 Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {12[T], 13[T]}, {15[T]}, {8[T]}, {}] Covered Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 13[T]}, {15[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)] Blocked [{}, {12[T], 13[T]}, {6[T], 15[T]}] Step with 10 Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)] Blocked [{}, {12[T], 13[T]}, {6[T], 15[T]}, {10[T]}] Covered Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)] Blocked [{}, {12[T], 13[T]}, {6[T], 10[T], 15[T]}] Step with 11 Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {12[T], 13[T]}, {6[T], 10[T], 15[T]}, {11[T]}] Covered Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)] Blocked [{}, {12[T], 13[T]}, {6[T], 10[T], 11[T], 15[T]}] Step with 12 Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {12[T], 13[T]}, {6[T], 10[T], 11[T], 15[T]}, {12[T]}] Covered Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)] Blocked [{}, {12[T], 13[T]}, {6[T], 10[T], 11[T], 12[T], 15[T]}] Step with 13 Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)] Blocked [{}, {12[T], 13[T]}, {6[T], 10[T], 11[T], 12[T], 15[T]}, {13[T]}] Covered Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)] Blocked [{}, {12[T], 13[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 15[T]}] Step with 14 Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {12[T], 13[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 15[T]}, {14[T]}] Covered Trace 9[T], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)] Blocked [{}, {12[T], 13[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T]}] Backtrack Trace 9[T] Blocked [{}, {12[T], 13[T], 15[T]}] Step with 14 Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {12[T], 13[T], 15[T]}, {14[T]}] Step with 15 Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)] Blocked [{}, {12[T], 13[T], 15[T]}, {14[T]}, {15[T]}] Covered Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {12[T], 13[T], 15[T]}, {14[T], 15[T]}] Step with 6 Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 13[T], 15[T]}, {14[T], 15[T]}, {}] Step with 7 Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {12[T], 13[T], 15[T]}, {14[T], 15[T]}, {}, {}] Covered Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 13[T], 15[T]}, {14[T], 15[T]}, {7[T]}] Step with 8 Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {12[T], 13[T], 15[T]}, {14[T], 15[T]}, {7[T]}, {}] Covered Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 13[T], 15[T]}, {14[T], 15[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {12[T], 13[T], 15[T]}, {6[T], 14[T], 15[T]}] Step with 10 Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)] Blocked [{}, {12[T], 13[T], 15[T]}, {6[T], 14[T], 15[T]}, {10[T]}] Covered Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {12[T], 13[T], 15[T]}, {6[T], 10[T], 14[T], 15[T]}] Step with 11 Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {12[T], 13[T], 15[T]}, {6[T], 10[T], 14[T], 15[T]}, {11[T]}] Covered Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {12[T], 13[T], 15[T]}, {6[T], 10[T], 11[T], 14[T], 15[T]}] Step with 12 Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {12[T], 13[T], 15[T]}, {6[T], 10[T], 11[T], 14[T], 15[T]}, {12[T]}] Covered Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {12[T], 13[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T]}] Step with 13 Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)] Blocked [{}, {12[T], 13[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 14[T], 15[T]}, {13[T]}] Covered Trace 9[T], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {12[T], 13[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T]}] Backtrack Trace 9[T] Blocked [{}, {12[T], 13[T], 14[T], 15[T]}] Step with 6 Trace 9[T], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 13[T], 14[T], 15[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], 15[T]}, {}, {}] Covered Trace 9[T], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 13[T], 14[T], 15[T]}, {8[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], 15[T]}, {8[T]}, {}] Covered Trace 9[T], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {12[T], 13[T], 14[T], 15[T]}, {7[T], 8[T]}] Backtrack Trace 9[T] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}] Step with 10 Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}, {10[T]}] Step with 11 Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}, {10[T]}, {11[T]}] Covered Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}, {10[T], 11[T]}] Step with 12 Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}, {10[T], 11[T]}, {12[T]}] Covered Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}, {10[T], 11[T], 12[T]}] Step with 13 Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}, {10[T], 11[T], 12[T]}, {13[T]}] Covered Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}, {10[T], 11[T], 12[T], 13[T]}] Step with 14 Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}, {10[T], 11[T], 12[T], 13[T]}, {14[T]}] Covered Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}, {10[T], 11[T], 12[T], 13[T], 14[T]}] Step with 15 Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}, {10[T], 11[T], 12[T], 13[T], 14[T]}, {15[T]}] Covered Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}, {10[T], 11[T], 12[T], 13[T], 14[T], 15[T]}] Step with 6 Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}, {10[T], 11[T], 12[T], 13[T], 14[T], 15[T]}, {}] Step with 7 Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 7[T] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}, {10[T], 11[T], 12[T], 13[T], 14[T], 15[T]}, {}, {}] Covered Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}, {10[T], 11[T], 12[T], 13[T], 14[T], 15[T]}, {7[T]}] Step with 8 Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)], 8[T] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}, {10[T], 11[T], 12[T], 13[T], 14[T], 15[T]}, {7[T]}, {}] Covered Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 12[T], 13[T], 14[T], 15[T]}, {10[T], 11[T], 12[T], 13[T], 14[T], 15[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)] Blocked [{}, {6[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], 12[T], 13[T], 14[T], 15[T]}] Step with 11 Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {11[T]}] Step with 12 Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {11[T]}, {12[T]}] Covered Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 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[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 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[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 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[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 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[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 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[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 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[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 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[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 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 8 Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 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]}, {}, {}] Covered Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 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]}, {8[T]}] Step with 7 Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 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]}, {8[T]}, {}] Covered Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 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[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 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[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+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]}, {10[T]}] Accelerate Start location: l3 Program variables: x^0 y^0 6: l0 -> l1 : (1-x^0 <= 0 /\ 1-y^0 <= 0), cost: 1 10: l0 -> l0 : x^0'=x^post2, y^0'=-n+y^0, (-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0), cost: 1 11: l0 -> l0 : x^0'=-n2+x^0, (-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0), cost: 1 12: l0 -> l0 : x^0'=-n2+x^post22, y^0'=-n3*n1+y^0, (-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0), cost: 1 13: l0 -> l0 : x^0'=x^post2, y^0'=-n*n5-n11*n5*n31+y^0, (-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0), cost: 1 14: l0 -> l0 : x^0'=-n2+x^post22, y^0'=-n3*n1*n10+y^0, (-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0), cost: 1 15: l0 -> l0 : x^0'=x^post2, y^0'=-n17*n-n101*n17*n35*n15+y^0, (-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0), cost: 1 16: l0 -> l0 : x^0'=x^post2, y^0'=-n*n47+y^0, (-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0), cost: 1 7: l1 -> l0 : x^0'=x^post2, 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'=x^post2, y^0'=-n+y^0, (-1+n >= 0 /\ 2-x^0 <= 0 /\ 1-x^0 <= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0 /\ -1+y^0 >= 0), cost: 1 New rule: l0 -> l0 : x^0'=x^post2, y^0'=-n*n47+y^0, (-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0), cost: 1 -1+n >= 0 [0]: monotonic increase yields -1+n >= 0 -1+x^0 >= 0 [0]: montonic decrease yields -1+x^post2 >= 0, dependencies: -2+x^0 >= 0 -1+x^0 >= 0 [1]: eventual decrease yields (-1+x^0 >= 0 /\ -1+x^post2 >= 0) -1+x^0 >= 0 [2]: eventual increase yields (-1+x^0 >= 0 /\ x^0-x^post2 <= 0) -1+x^post2 >= 0 [0]: monotonic increase yields -1+x^post2 >= 0 -2+x^0 >= 0 [0]: eventual decrease yields (-2+x^post2 >= 0 /\ -2+x^0 >= 0) -2+x^0 >= 0 [1]: eventual increase yields (x^0-x^post2 <= 0 /\ -2+x^0 >= 0) -n+y^0 >= 0 [0]: montonic decrease yields -n*(-1+n47)-n+y^0 >= 0, dependencies: -1+n >= 0 -n+y^0 >= 0 [1]: eventual increase yields (n <= 0 /\ -n+y^0 >= 0), dependencies: -1+n >= 0 -1+y^0 >= 0 [0]: montonic decrease yields -1-n*(-1+n47)+y^0 >= 0, dependencies: -1+n >= 0 -1+y^0 >= 0 [1]: eventual increase yields (n <= 0 /\ -1+y^0 >= 0), dependencies: -1+n >= 0 Replacement map: {-1+n >= 0 -> -1+n >= 0, -1+x^0 >= 0 -> -1+x^post2 >= 0, -1+x^post2 >= 0 -> -1+x^post2 >= 0, -2+x^0 >= 0 -> (-2+x^post2 >= 0 /\ -2+x^0 >= 0), -n+y^0 >= 0 -> -n*(-1+n47)-n+y^0 >= 0, -1+y^0 >= 0 -> -1-n*(-1+n47)+y^0 >= 0} Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {16[T]}] Step with 6 Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {16[T]}, {}] Step with 7 Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 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]}, {16[T]}, {}, {}] Covered Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {16[T]}, {7[T]}] Step with 8 Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 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]}, {16[T]}, {7[T]}, {}] Covered Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {16[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {6[T], 16[T]}] Step with 10 Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0)], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {6[T], 16[T]}, {10[T]}] Covered Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {6[T], 10[T], 16[T]}] Step with 11 Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0)], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {6[T], 10[T], 16[T]}, {11[T]}] Covered Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 16[T]}] Step with 12 Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0)], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 16[T]}, {12[T]}] Covered Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 16[T]}] Step with 13 Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0)], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 16[T]}, {13[T]}] Covered Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 16[T]}] Step with 14 Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0)], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 16[T]}, {14[T]}] Covered Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 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], 16[T]}] Step with 15 Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0)], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 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], 16[T]}, {15[T]}] Covered Trace 9[T], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 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], 16[T]}] Backtrack Trace 9[T] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}] Step with 11 Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {11[T]}] Step with 12 Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 12[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1+x^0 >= 0 /\ -n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {11[T]}, {12[T]}] Covered Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {11[T], 12[T]}] Step with 13 Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 13[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1-n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*(-1+n31)-n*(-1+n5)-n11-n11*(-1+n5)*n31+y^0 >= 0 /\ -n11*n31-n+y^0 >= 0 /\ -n11*n31-n*(-1+n5)-n-n11*(-1+n5)*n31+y^0 >= 0 /\ -1+x^post2 >= 0 /\ -1+n11 >= 0 /\ -1+n5 >= 0 /\ -1+n31 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {11[T], 12[T]}, {13[T]}] Covered Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {11[T], 12[T], 13[T]}] Step with 14 Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 14[(-n2+x^post22 >= 0 /\ -1-n1-n1*(-1+n3)+y^0 >= 0 /\ -1-n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -2-n2+x^post22 >= 0 /\ -1-n2+x^post22 >= 0 /\ -1+x^post22 >= 0 /\ -2+x^0 >= 0 /\ -n1-n1*(-1+n3)-n3*n1*(-1+n10)+y^0 >= 0 /\ -1+n3 >= 0 /\ -1+n10 >= 0 /\ -1+n1 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {11[T], 12[T], 13[T]}, {14[T]}] Covered Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {11[T], 12[T], 13[T], 14[T]}] Step with 15 Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 15[(-1+n17 >= 0 /\ -1+n >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n101 >= 0 /\ -1-(-1+n101)*n35*n15-(-1+n17)*n101*n35*n15-(-1+n17)*n-n15-(-1+n35)*n15+y^0 >= 0 /\ -1+n35 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -n101*n35*n15-n-(-1+n17)*n101*n35*n15-(-1+n17)*n+y^0 >= 0 /\ -1+n15 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {11[T], 12[T], 13[T], 14[T]}, {15[T]}] Covered Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {11[T], 12[T], 13[T], 14[T], 15[T]}] Step with 16 Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 16[(-1+n >= 0 /\ -1-n*(-1+n47)+y^0 >= 0 /\ -n*(-1+n47)-n+y^0 >= 0 /\ -2+x^post2 >= 0 /\ -1+x^post2 >= 0 /\ -2+x^0 >= 0 /\ -1+n47 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {11[T], 12[T], 13[T], 14[T], 15[T]}, {16[T]}] Covered Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {11[T], 12[T], 13[T], 14[T], 15[T], 16[T]}] Step with 6 Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {11[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {}] Step with 8 Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 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], 16[T]}, {11[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {}, {}] Covered Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {11[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {8[T]}] Step with 7 Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 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], 16[T]}, {11[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {8[T]}, {}] Covered Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 6[(1-x^0 <= 0 /\ 1-y^0 <= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {11[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {7[T], 8[T]}] Backtrack Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {6[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T]}] Step with 10 Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)], 10[(-1+n >= 0 /\ -1+x^0 >= 0 /\ -1+x^post2 >= 0 /\ -n+y^0 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {6[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {10[T]}] Covered Trace 9[T], 11[(-n2+x^0 >= 0 /\ -1+y^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {6[T], 10[T], 12[T], 13[T], 14[T], 15[T], 16[T]}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T]}] Backtrack Trace 9[T] Blocked [{}, {6[T], 10[T], 11[T], 12[T], 13[T], 14[T], 15[T], 16[T]}] Backtrack Trace Blocked [{9[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b