unknown Initial ITS Start location: l7 Program variables: result^0 x^0 y^0 0: l0 -> l1 : result^0'=result^post1, x^0'=x^post1, y^0'=y^post1, (0 == 0 /\ -x^0 <= 0 /\ -y^post1+y^0 == 0 /\ -x^post1+x^0 == 0), cost: 1 1: l0 -> l3 : result^0'=result^post2, x^0'=x^post2, y^0'=y^post2, (-x^post2+x^0 == 0 /\ result^0-result^post2 == 0 /\ -y^post2+y^0 == 0 /\ 1+x^0 <= 0), cost: 1 6: l0 -> l5 : result^0'=result^post7, x^0'=x^post7, y^0'=y^post7, (-1+y^post7-y^0 == 0 /\ 1+x^0 <= 0 /\ result^0-result^post7 == 0 /\ 99-x^0+x^post7 == 0 /\ 1+y^0 <= 0 /\ -1-y^0 <= 0), cost: 1 2: l3 -> l4 : result^0'=result^post3, x^0'=x^post3, y^0'=y^post3, (-x^post3+x^0 == 0 /\ result^0-result^post3 == 0 /\ 2+y^0 <= 0 /\ -y^post3+y^0 == 0), cost: 1 3: l3 -> l4 : result^0'=result^post4, x^0'=x^post4, y^0'=y^post4, (-y^0 <= 0 /\ -x^post4+x^0 == 0 /\ -y^post4+y^0 == 0 /\ result^0-result^post4 == 0), cost: 1 4: l4 -> l2 : result^0'=result^post5, x^0'=x^post5, y^0'=y^post5, (-1+y^post5-y^0 == 0 /\ -1-x^0+x^post5 == 0 /\ result^0-result^post5 == 0), cost: 1 5: l2 -> l0 : result^0'=result^post6, x^0'=x^post6, y^0'=y^post6, (x^0-x^post6 == 0 /\ result^0-result^post6 == 0 /\ -y^post6+y^0 == 0), cost: 1 7: l5 -> l0 : result^0'=result^post8, x^0'=x^post8, y^0'=y^post8, (result^0-result^post8 == 0 /\ y^0-y^post8 == 0 /\ -x^post8+x^0 == 0), cost: 1 8: l6 -> l0 : result^0'=result^post9, x^0'=x^post9, y^0'=y^post9, (result^0-result^post9 == 0 /\ -x^post9+x^0 == 0 /\ y^0-y^post9 == 0), cost: 1 9: l7 -> l6 : result^0'=result^post10, x^0'=x^post10, y^0'=y^post10, (-x^post10+x^0 == 0 /\ y^0-y^post10 == 0 /\ -result^post10+result^0 == 0), cost: 1 Chained Linear Paths Start location: l7 Program variables: result^0 x^0 y^0 0: l0 -> l1 : result^0'=result^post1, x^0'=x^post1, y^0'=y^post1, (0 == 0 /\ -x^0 <= 0 /\ -y^post1+y^0 == 0 /\ -x^post1+x^0 == 0), cost: 1 1: l0 -> l3 : result^0'=result^post2, x^0'=x^post2, y^0'=y^post2, (-x^post2+x^0 == 0 /\ result^0-result^post2 == 0 /\ -y^post2+y^0 == 0 /\ 1+x^0 <= 0), cost: 1 11: l0 -> l0 : result^0'=result^post8, x^0'=x^post8, y^0'=y^post8, (-1+y^post7-y^0 == 0 /\ y^post7-y^post8 == 0 /\ -x^post8+x^post7 == 0 /\ 1+x^0 <= 0 /\ -result^post8+result^post7 == 0 /\ result^0-result^post7 == 0 /\ 99-x^0+x^post7 == 0 /\ 1+y^0 <= 0 /\ -1-y^0 <= 0), cost: 1 2: l3 -> l4 : result^0'=result^post3, x^0'=x^post3, y^0'=y^post3, (-x^post3+x^0 == 0 /\ result^0-result^post3 == 0 /\ 2+y^0 <= 0 /\ -y^post3+y^0 == 0), cost: 1 3: l3 -> l4 : result^0'=result^post4, x^0'=x^post4, y^0'=y^post4, (-y^0 <= 0 /\ -x^post4+x^0 == 0 /\ -y^post4+y^0 == 0 /\ result^0-result^post4 == 0), cost: 1 12: l4 -> l0 : result^0'=result^post6, x^0'=x^post6, y^0'=y^post6, (-result^post6+result^post5 == 0 /\ -x^post6+x^post5 == 0 /\ -y^post6+y^post5 == 0 /\ -1+y^post5-y^0 == 0 /\ -1-x^0+x^post5 == 0 /\ result^0-result^post5 == 0), cost: 1 10: l7 -> l0 : result^0'=result^post9, x^0'=x^post9, y^0'=y^post9, (result^post10-result^post9 == 0 /\ -x^post10+x^0 == 0 /\ x^post10-x^post9 == 0 /\ y^0-y^post10 == 0 /\ y^post10-y^post9 == 0 /\ -result^post10+result^0 == 0), cost: 1 Eliminating location l6 by chaining: Applied chaining First rule: l7 -> l6 : result^0'=result^post10, x^0'=x^post10, y^0'=y^post10, (-x^post10+x^0 == 0 /\ y^0-y^post10 == 0 /\ -result^post10+result^0 == 0), cost: 1 Second rule: l6 -> l0 : result^0'=result^post9, x^0'=x^post9, y^0'=y^post9, (result^0-result^post9 == 0 /\ -x^post9+x^0 == 0 /\ y^0-y^post9 == 0), cost: 1 New rule: l7 -> l0 : result^0'=result^post9, x^0'=x^post9, y^0'=y^post9, (result^post10-result^post9 == 0 /\ -x^post10+x^0 == 0 /\ x^post10-x^post9 == 0 /\ y^0-y^post10 == 0 /\ y^post10-y^post9 == 0 /\ -result^post10+result^0 == 0), cost: 1 Applied deletion Removed the following rules: 8 9 Eliminating location l5 by chaining: Applied chaining First rule: l0 -> l5 : result^0'=result^post7, x^0'=x^post7, y^0'=y^post7, (-1+y^post7-y^0 == 0 /\ 1+x^0 <= 0 /\ result^0-result^post7 == 0 /\ 99-x^0+x^post7 == 0 /\ 1+y^0 <= 0 /\ -1-y^0 <= 0), cost: 1 Second rule: l5 -> l0 : result^0'=result^post8, x^0'=x^post8, y^0'=y^post8, (result^0-result^post8 == 0 /\ y^0-y^post8 == 0 /\ -x^post8+x^0 == 0), cost: 1 New rule: l0 -> l0 : result^0'=result^post8, x^0'=x^post8, y^0'=y^post8, (-1+y^post7-y^0 == 0 /\ y^post7-y^post8 == 0 /\ -x^post8+x^post7 == 0 /\ 1+x^0 <= 0 /\ -result^post8+result^post7 == 0 /\ result^0-result^post7 == 0 /\ 99-x^0+x^post7 == 0 /\ 1+y^0 <= 0 /\ -1-y^0 <= 0), cost: 1 Applied deletion Removed the following rules: 6 7 Eliminating location l2 by chaining: Applied chaining First rule: l4 -> l2 : result^0'=result^post5, x^0'=x^post5, y^0'=y^post5, (-1+y^post5-y^0 == 0 /\ -1-x^0+x^post5 == 0 /\ result^0-result^post5 == 0), cost: 1 Second rule: l2 -> l0 : result^0'=result^post6, x^0'=x^post6, y^0'=y^post6, (x^0-x^post6 == 0 /\ result^0-result^post6 == 0 /\ -y^post6+y^0 == 0), cost: 1 New rule: l4 -> l0 : result^0'=result^post6, x^0'=x^post6, y^0'=y^post6, (-result^post6+result^post5 == 0 /\ -x^post6+x^post5 == 0 /\ -y^post6+y^post5 == 0 /\ -1+y^post5-y^0 == 0 /\ -1-x^0+x^post5 == 0 /\ result^0-result^post5 == 0), cost: 1 Applied deletion Removed the following rules: 4 5 Simplified Transitions Start location: l7 Program variables: result^0 x^0 y^0 13: l0 -> l1 : result^0'=result^post1, -x^0 <= 0, cost: 1 14: l0 -> l3 : 1+x^0 <= 0, cost: 1 18: l0 -> l0 : x^0'=-99+x^0, y^0'=1+y^0, (1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0), cost: 1 15: l3 -> l4 : 2+y^0 <= 0, cost: 1 16: l3 -> l4 : -y^0 <= 0, cost: 1 19: l4 -> l0 : x^0'=1+x^0, y^0'=1+y^0, T, cost: 1 17: l7 -> l0 : T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : result^0'=result^post1, x^0'=x^post1, y^0'=y^post1, (0 == 0 /\ -x^0 <= 0 /\ -y^post1+y^0 == 0 /\ -x^post1+x^0 == 0), cost: 1 New rule: l0 -> l1 : result^0'=result^post1, x^0'=x^0, y^0'=y^0, (0 == 0 /\ -x^0 <= 0), cost: 1 propagated equality y^post1 = y^0 propagated equality x^post1 = x^0 Simplified Guard Original rule: l0 -> l1 : result^0'=result^post1, x^0'=x^0, y^0'=y^0, (0 == 0 /\ -x^0 <= 0), cost: 1 New rule: l0 -> l1 : result^0'=result^post1, x^0'=x^0, y^0'=y^0, -x^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : result^0'=result^post1, x^0'=x^0, y^0'=y^0, -x^0 <= 0, cost: 1 New rule: l0 -> l1 : result^0'=result^post1, -x^0 <= 0, cost: 1 Propagated Equalities Original rule: l0 -> l3 : result^0'=result^post2, x^0'=x^post2, y^0'=y^post2, (-x^post2+x^0 == 0 /\ result^0-result^post2 == 0 /\ -y^post2+y^0 == 0 /\ 1+x^0 <= 0), cost: 1 New rule: l0 -> l3 : result^0'=result^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ 1+x^0 <= 0), cost: 1 propagated equality x^post2 = x^0 propagated equality result^post2 = result^0 propagated equality y^post2 = y^0 Simplified Guard Original rule: l0 -> l3 : result^0'=result^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ 1+x^0 <= 0), cost: 1 New rule: l0 -> l3 : result^0'=result^0, x^0'=x^0, y^0'=y^0, 1+x^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l3 : result^0'=result^0, x^0'=x^0, y^0'=y^0, 1+x^0 <= 0, cost: 1 New rule: l0 -> l3 : 1+x^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l4 : result^0'=result^post3, x^0'=x^post3, y^0'=y^post3, (-x^post3+x^0 == 0 /\ result^0-result^post3 == 0 /\ 2+y^0 <= 0 /\ -y^post3+y^0 == 0), cost: 1 New rule: l3 -> l4 : result^0'=result^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ 2+y^0 <= 0), cost: 1 propagated equality x^post3 = x^0 propagated equality result^post3 = result^0 propagated equality y^post3 = y^0 Simplified Guard Original rule: l3 -> l4 : result^0'=result^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ 2+y^0 <= 0), cost: 1 New rule: l3 -> l4 : result^0'=result^0, x^0'=x^0, y^0'=y^0, 2+y^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l4 : result^0'=result^0, x^0'=x^0, y^0'=y^0, 2+y^0 <= 0, cost: 1 New rule: l3 -> l4 : 2+y^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l4 : result^0'=result^post4, x^0'=x^post4, y^0'=y^post4, (-y^0 <= 0 /\ -x^post4+x^0 == 0 /\ -y^post4+y^0 == 0 /\ result^0-result^post4 == 0), cost: 1 New rule: l3 -> l4 : result^0'=result^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ -y^0 <= 0), cost: 1 propagated equality x^post4 = x^0 propagated equality y^post4 = y^0 propagated equality result^post4 = result^0 Simplified Guard Original rule: l3 -> l4 : result^0'=result^0, x^0'=x^0, y^0'=y^0, (0 == 0 /\ -y^0 <= 0), cost: 1 New rule: l3 -> l4 : result^0'=result^0, x^0'=x^0, y^0'=y^0, -y^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l4 : result^0'=result^0, x^0'=x^0, y^0'=y^0, -y^0 <= 0, cost: 1 New rule: l3 -> l4 : -y^0 <= 0, cost: 1 Propagated Equalities Original rule: l7 -> l0 : result^0'=result^post9, x^0'=x^post9, y^0'=y^post9, (result^post10-result^post9 == 0 /\ -x^post10+x^0 == 0 /\ x^post10-x^post9 == 0 /\ y^0-y^post10 == 0 /\ y^post10-y^post9 == 0 /\ -result^post10+result^0 == 0), cost: 1 New rule: l7 -> l0 : result^0'=result^post10, x^0'=x^post10, y^0'=y^post10, (0 == 0 /\ -x^post10+x^0 == 0 /\ y^0-y^post10 == 0 /\ -result^post10+result^0 == 0), cost: 1 propagated equality result^post9 = result^post10 propagated equality x^post9 = x^post10 propagated equality y^post9 = y^post10 Propagated Equalities Original rule: l7 -> l0 : result^0'=result^post10, x^0'=x^post10, y^0'=y^post10, (0 == 0 /\ -x^post10+x^0 == 0 /\ y^0-y^post10 == 0 /\ -result^post10+result^0 == 0), cost: 1 New rule: l7 -> l0 : result^0'=result^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1 propagated equality x^post10 = x^0 propagated equality y^post10 = y^0 propagated equality result^post10 = result^0 Simplified Guard Original rule: l7 -> l0 : result^0'=result^0, x^0'=x^0, y^0'=y^0, 0 == 0, cost: 1 New rule: l7 -> l0 : result^0'=result^0, x^0'=x^0, y^0'=y^0, T, cost: 1 Removed Trivial Updates Original rule: l7 -> l0 : result^0'=result^0, x^0'=x^0, y^0'=y^0, T, cost: 1 New rule: l7 -> l0 : T, cost: 1 made implied equalities explicit Original rule: l0 -> l0 : result^0'=result^post8, x^0'=x^post8, y^0'=y^post8, (-1+y^post7-y^0 == 0 /\ y^post7-y^post8 == 0 /\ -x^post8+x^post7 == 0 /\ 1+x^0 <= 0 /\ -result^post8+result^post7 == 0 /\ result^0-result^post7 == 0 /\ 99-x^0+x^post7 == 0 /\ 1+y^0 <= 0 /\ -1-y^0 <= 0), cost: 1 New rule: l0 -> l0 : result^0'=result^post8, x^0'=x^post8, y^0'=y^post8, (-1+y^post7-y^0 == 0 /\ y^post7-y^post8 == 0 /\ -x^post8+x^post7 == 0 /\ 1+x^0 <= 0 /\ -result^post8+result^post7 == 0 /\ result^0-result^post7 == 0 /\ 99-x^0+x^post7 == 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0), cost: 1 Propagated Equalities Original rule: l0 -> l0 : result^0'=result^post8, x^0'=x^post8, y^0'=y^post8, (-1+y^post7-y^0 == 0 /\ y^post7-y^post8 == 0 /\ -x^post8+x^post7 == 0 /\ 1+x^0 <= 0 /\ -result^post8+result^post7 == 0 /\ result^0-result^post7 == 0 /\ 99-x^0+x^post7 == 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0), cost: 1 New rule: l0 -> l0 : result^0'=result^post7, x^0'=x^post7, y^0'=y^post7, (0 == 0 /\ -1+y^post7-y^0 == 0 /\ 1+x^0 <= 0 /\ result^0-result^post7 == 0 /\ 99-x^0+x^post7 == 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0), cost: 1 propagated equality y^post8 = y^post7 propagated equality x^post8 = x^post7 propagated equality result^post8 = result^post7 Propagated Equalities Original rule: l0 -> l0 : result^0'=result^post7, x^0'=x^post7, y^0'=y^post7, (0 == 0 /\ -1+y^post7-y^0 == 0 /\ 1+x^0 <= 0 /\ result^0-result^post7 == 0 /\ 99-x^0+x^post7 == 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0), cost: 1 New rule: l0 -> l0 : result^0'=result^0, x^0'=-99+x^0, y^0'=1+y^0, (0 == 0 /\ 1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0), cost: 1 propagated equality y^post7 = 1+y^0 propagated equality result^post7 = result^0 propagated equality x^post7 = -99+x^0 Simplified Guard Original rule: l0 -> l0 : result^0'=result^0, x^0'=-99+x^0, y^0'=1+y^0, (0 == 0 /\ 1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0), cost: 1 New rule: l0 -> l0 : result^0'=result^0, x^0'=-99+x^0, y^0'=1+y^0, (1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0), cost: 1 made implied equalities explicit Original rule: l0 -> l0 : result^0'=result^0, x^0'=-99+x^0, y^0'=1+y^0, (1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0), cost: 1 New rule: l0 -> l0 : result^0'=result^0, x^0'=-99+x^0, y^0'=1+y^0, (1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l0 -> l0 : result^0'=result^0, x^0'=-99+x^0, y^0'=1+y^0, (1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0), cost: 1 New rule: l0 -> l0 : x^0'=-99+x^0, y^0'=1+y^0, (1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0), cost: 1 Propagated Equalities Original rule: l4 -> l0 : result^0'=result^post6, x^0'=x^post6, y^0'=y^post6, (-result^post6+result^post5 == 0 /\ -x^post6+x^post5 == 0 /\ -y^post6+y^post5 == 0 /\ -1+y^post5-y^0 == 0 /\ -1-x^0+x^post5 == 0 /\ result^0-result^post5 == 0), cost: 1 New rule: l4 -> l0 : result^0'=result^post5, x^0'=x^post5, y^0'=y^post5, (0 == 0 /\ -1+y^post5-y^0 == 0 /\ -1-x^0+x^post5 == 0 /\ result^0-result^post5 == 0), cost: 1 propagated equality result^post6 = result^post5 propagated equality x^post6 = x^post5 propagated equality y^post6 = y^post5 Propagated Equalities Original rule: l4 -> l0 : result^0'=result^post5, x^0'=x^post5, y^0'=y^post5, (0 == 0 /\ -1+y^post5-y^0 == 0 /\ -1-x^0+x^post5 == 0 /\ result^0-result^post5 == 0), cost: 1 New rule: l4 -> l0 : result^0'=result^0, x^0'=1+x^0, y^0'=1+y^0, 0 == 0, cost: 1 propagated equality y^post5 = 1+y^0 propagated equality x^post5 = 1+x^0 propagated equality result^post5 = result^0 Simplified Guard Original rule: l4 -> l0 : result^0'=result^0, x^0'=1+x^0, y^0'=1+y^0, 0 == 0, cost: 1 New rule: l4 -> l0 : result^0'=result^0, x^0'=1+x^0, y^0'=1+y^0, T, cost: 1 Removed Trivial Updates Original rule: l4 -> l0 : result^0'=result^0, x^0'=1+x^0, y^0'=1+y^0, T, cost: 1 New rule: l4 -> l0 : x^0'=1+x^0, y^0'=1+y^0, T, cost: 1 Step with 17 Trace 17[T] Blocked [{}, {}] Step with 13 Trace 17[T], 13[(-x^0 <= 0)] Blocked [{}, {}, {}] Backtrack Trace 17[T] Blocked [{}, {13[T]}] Step with 14 Trace 17[T], 14[(1+x^0 <= 0)] Blocked [{}, {13[T]}, {}] Step with 15 Trace 17[T], 14[(1+x^0 <= 0)], 15[(2+y^0 <= 0)] Blocked [{}, {13[T]}, {}, {}] Step with 19 Trace 17[T], 14[(1+x^0 <= 0)], 15[(2+y^0 <= 0)], 19[T] Blocked [{}, {13[T]}, {}, {}, {}] Accelerate Start location: l7 Program variables: result^0 x^0 y^0 13: l0 -> l1 : result^0'=result^post1, -x^0 <= 0, cost: 1 14: l0 -> l3 : 1+x^0 <= 0, cost: 1 18: l0 -> l0 : x^0'=-99+x^0, y^0'=1+y^0, (1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0), cost: 1 20: l0 -> l0 : x^0'=n+x^0, y^0'=n+y^0, (-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0), cost: 1 15: l3 -> l4 : 2+y^0 <= 0, cost: 1 16: l3 -> l4 : -y^0 <= 0, cost: 1 19: l4 -> l0 : x^0'=1+x^0, y^0'=1+y^0, T, cost: 1 17: l7 -> l0 : T, cost: 1 Loop Acceleration Original rule: l0 -> l0 : x^0'=1+x^0, y^0'=1+y^0, (2+y^0 <= 0 /\ 1+x^0 <= 0), cost: 1 New rule: l0 -> l0 : x^0'=n+x^0, y^0'=n+y^0, (-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0), cost: 1 -2-y^0 >= 0 [0]: montonic decrease yields -1-n-y^0 >= 0 -2-y^0 >= 0 [1]: eventual increase yields (-2-y^0 >= 0 /\ 1 <= 0) -1-x^0 >= 0 [0]: montonic decrease yields -n-x^0 >= 0 -1-x^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1-x^0 >= 0) Replacement map: {-2-y^0 >= 0 -> -1-n-y^0 >= 0, -1-x^0 >= 0 -> -n-x^0 >= 0} Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)] Blocked [{}, {13[T]}, {20[T]}] Step with 13 Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 13[(-x^0 <= 0)] Blocked [{}, {13[T]}, {20[T]}, {}] Backtrack Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)] Blocked [{}, {13[T]}, {13[T], 20[T]}] Step with 14 Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 14[(1+x^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 20[T]}, {}] Step with 15 Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 14[(1+x^0 <= 0)], 15[(2+y^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 20[T]}, {}, {}] Step with 19 Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 14[(1+x^0 <= 0)], 15[(2+y^0 <= 0)], 19[T] Blocked [{}, {13[T]}, {13[T], 20[T]}, {}, {}, {}] Covered Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 14[(1+x^0 <= 0)], 15[(2+y^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 20[T]}, {}, {19[T]}] Backtrack Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 14[(1+x^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 20[T]}, {15[T]}] Backtrack Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}] Step with 18 Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {}] Acceleration Failed marked recursive suffix as redundant Acceleration Failed marked recursive suffix as redundant Step with 14 Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 14[(1+x^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T]}, {}] Step with 16 Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T]}, {15[T]}, {}] Step with 19 Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)], 19[T] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T]}, {15[T]}, {}, {}] Accelerate Start location: l7 Program variables: result^0 x^0 y^0 13: l0 -> l1 : result^0'=result^post1, -x^0 <= 0, cost: 1 14: l0 -> l3 : 1+x^0 <= 0, cost: 1 18: l0 -> l0 : x^0'=-99+x^0, y^0'=1+y^0, (1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0), cost: 1 20: l0 -> l0 : x^0'=n+x^0, y^0'=n+y^0, (-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0), cost: 1 21: l0 -> l0 : x^0'=x^0+n2, y^0'=y^0+n2, (y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 15: l3 -> l4 : 2+y^0 <= 0, cost: 1 16: l3 -> l4 : -y^0 <= 0, cost: 1 19: l4 -> l0 : x^0'=1+x^0, y^0'=1+y^0, T, cost: 1 17: l7 -> l0 : T, cost: 1 Loop Acceleration Original rule: l0 -> l0 : x^0'=1+x^0, y^0'=1+y^0, (-y^0 <= 0 /\ 1+x^0 <= 0), cost: 1 New rule: l0 -> l0 : x^0'=x^0+n2, y^0'=y^0+n2, (y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 y^0 >= 0 [0]: monotonic increase yields y^0 >= 0 -1-x^0 >= 0 [0]: montonic decrease yields -x^0-n2 >= 0 -1-x^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1-x^0 >= 0) Replacement map: {y^0 >= 0 -> y^0 >= 0, -1-x^0 >= 0 -> -x^0-n2 >= 0} Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T]}, {21[T]}] Acceleration Failed marked recursive suffix as redundant Acceleration Failed marked recursive suffix as redundant Step with 13 Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 13[(-x^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T]}, {21[T]}, {}] Backtrack Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T]}, {13[T], 21[T]}] Step with 14 Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 14[(1+x^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T]}, {13[T], 21[T]}, {}] Step with 16 Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T]}, {13[T], 21[T]}, {}, {}] Step with 19 Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)], 19[T] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T]}, {13[T], 21[T]}, {}, {}, {}] Covered Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T]}, {13[T], 21[T]}, {}, {19[T]}] Backtrack Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 14[(1+x^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T]}, {13[T], 21[T]}, {16[T]}] Backtrack Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T]}, {13[T], 14[T], 21[T]}] Backtrack Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T], 21[T]}] Step with 14 Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 14[(1+x^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T], 21[T]}, {}] Step with 16 Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T], 21[T]}, {}, {}] Step with 19 Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)], 19[T] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T], 21[T]}, {}, {}, {}] Covered Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T], 21[T]}, {}, {19[T]}] Backtrack Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 14[(1+x^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 18[T], 20[T], 21[T]}, {16[T]}] Backtrack Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 20[T]}, {13[T], 14[T], 18[T], 20[T], 21[T]}] Backtrack Trace 17[T], 20[(-1+n >= 0 /\ -1-n-y^0 >= 0 /\ -n-x^0 >= 0)] Blocked [{}, {13[T]}, {13[T], 14[T], 18[T], 20[T]}] Backtrack Trace 17[T] Blocked [{}, {13[T], 20[T]}] Step with 14 Trace 17[T], 14[(1+x^0 <= 0)] Blocked [{}, {13[T], 20[T]}, {}] Step with 16 Trace 17[T], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)] Blocked [{}, {13[T], 20[T]}, {}, {}] Step with 19 Trace 17[T], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)], 19[T] Blocked [{}, {13[T], 20[T]}, {}, {}, {}] Covered Trace 17[T], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)] Blocked [{}, {13[T], 20[T]}, {}, {19[T]}] Backtrack Trace 17[T], 14[(1+x^0 <= 0)] Blocked [{}, {13[T], 20[T]}, {16[T]}] Step with 15 Trace 17[T], 14[(1+x^0 <= 0)], 15[(2+y^0 <= 0)] Blocked [{}, {13[T], 20[T]}, {16[T]}, {}] Step with 19 Trace 17[T], 14[(1+x^0 <= 0)], 15[(2+y^0 <= 0)], 19[T] Blocked [{}, {13[T], 20[T]}, {16[T]}, {}, {}] Covered Trace 17[T], 14[(1+x^0 <= 0)], 15[(2+y^0 <= 0)] Blocked [{}, {13[T], 20[T]}, {16[T]}, {19[T]}] Backtrack Trace 17[T], 14[(1+x^0 <= 0)] Blocked [{}, {13[T], 20[T]}, {15[T], 16[T]}] Backtrack Trace 17[T] Blocked [{}, {13[T], 14[T], 20[T]}] Step with 18 Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)] Blocked [{}, {13[T], 14[T], 20[T]}, {}] Step with 21 Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {13[T], 14[T], 20[T]}, {18[T], 20[T]}, {21[T]}] Step with 13 Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 13[(-x^0 <= 0)] Blocked [{}, {13[T], 14[T], 20[T]}, {18[T], 20[T]}, {21[T]}, {}] Backtrack Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {13[T], 14[T], 20[T]}, {18[T], 20[T]}, {13[T], 21[T]}] Step with 14 Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 14[(1+x^0 <= 0)] Blocked [{}, {13[T], 14[T], 20[T]}, {18[T], 20[T]}, {13[T], 21[T]}, {}] Step with 16 Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)] Blocked [{}, {13[T], 14[T], 20[T]}, {18[T], 20[T]}, {13[T], 21[T]}, {15[T]}, {}] Step with 19 Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)], 19[T] Blocked [{}, {13[T], 14[T], 20[T]}, {18[T], 20[T]}, {13[T], 21[T]}, {15[T]}, {}, {}] Covered Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)] Blocked [{}, {13[T], 14[T], 20[T]}, {18[T], 20[T]}, {13[T], 21[T]}, {15[T]}, {19[T]}] Backtrack Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 14[(1+x^0 <= 0)] Blocked [{}, {13[T], 14[T], 20[T]}, {18[T], 20[T]}, {13[T], 21[T]}, {15[T], 16[T]}] Backtrack Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {13[T], 14[T], 20[T]}, {18[T], 20[T]}, {13[T], 14[T], 21[T]}] Backtrack Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)] Blocked [{}, {13[T], 14[T], 20[T]}, {18[T], 20[T], 21[T]}] Step with 14 Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 14[(1+x^0 <= 0)] Blocked [{}, {13[T], 14[T], 20[T]}, {18[T], 20[T], 21[T]}, {}] Step with 16 Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)] Blocked [{}, {13[T], 14[T], 20[T]}, {18[T], 20[T], 21[T]}, {}, {}] Step with 19 Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)], 19[T] Blocked [{}, {13[T], 14[T], 20[T]}, {18[T], 20[T], 21[T]}, {}, {}, {}] Covered Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)] Blocked [{}, {13[T], 14[T], 20[T]}, {18[T], 20[T], 21[T]}, {}, {19[T]}] Backtrack Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)], 14[(1+x^0 <= 0)] Blocked [{}, {13[T], 14[T], 20[T]}, {18[T], 20[T], 21[T]}, {16[T]}] Backtrack Trace 17[T], 18[(1+x^0 <= 0 /\ 1+y^0 <= 0 /\ 1+y^0 == 0 /\ -1-y^0 <= 0)] Blocked [{}, {13[T], 14[T], 20[T]}, {14[T], 18[T], 20[T], 21[T]}] Backtrack Trace 17[T] Blocked [{}, {13[T], 14[T], 18[T], 20[T]}] Step with 21 Trace 17[T], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {13[T], 14[T], 18[T], 20[T]}, {21[T]}] Step with 13 Trace 17[T], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 13[(-x^0 <= 0)] Blocked [{}, {13[T], 14[T], 18[T], 20[T]}, {21[T]}, {}] Backtrack Trace 17[T], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {13[T], 14[T], 18[T], 20[T]}, {13[T], 21[T]}] Step with 14 Trace 17[T], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 14[(1+x^0 <= 0)] Blocked [{}, {13[T], 14[T], 18[T], 20[T]}, {13[T], 21[T]}, {}] Step with 16 Trace 17[T], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)] Blocked [{}, {13[T], 14[T], 18[T], 20[T]}, {13[T], 21[T]}, {}, {}] Step with 19 Trace 17[T], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)], 19[T] Blocked [{}, {13[T], 14[T], 18[T], 20[T]}, {13[T], 21[T]}, {}, {}, {}] Covered Trace 17[T], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 14[(1+x^0 <= 0)], 16[(-y^0 <= 0)] Blocked [{}, {13[T], 14[T], 18[T], 20[T]}, {13[T], 21[T]}, {}, {19[T]}] Backtrack Trace 17[T], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)], 14[(1+x^0 <= 0)] Blocked [{}, {13[T], 14[T], 18[T], 20[T]}, {13[T], 21[T]}, {16[T]}] Backtrack Trace 17[T], 21[(y^0 >= 0 /\ -x^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {13[T], 14[T], 18[T], 20[T]}, {13[T], 14[T], 21[T]}] Backtrack Trace 17[T] Blocked [{}, {13[T], 14[T], 18[T], 20[T], 21[T]}] Backtrack Trace Blocked [{17[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b