NO Initial ITS Start location: l7 Program variables: lt_15^0 lt_19^0 nd_12^0 p_14^0 rt_11^0 rv_18^0 st_17^0 x_13^0 y_16^0 0: l0 -> l1 : lt_15^0'=lt_15^post1, lt_19^0'=lt_19^post1, nd_12^0'=nd_12^post1, p_14^0'=p_14^post1, rt_11^0'=rt_11^post1, rv_18^0'=rv_18^post1, st_17^0'=st_17^post1, x_13^0'=x_13^post1, y_16^0'=y_16^post1, (lt_15^0-lt_15^post1 == 0 /\ lt_19^0-lt_19^post1 == 0 /\ rt_11^0-rt_11^post1 == 0 /\ -nd_12^post1+nd_12^0 == 0 /\ -rv_18^post1+rv_18^0 == 0 /\ -y_16^post1+y_16^0 == 0 /\ -x_13^post1+x_13^0 == 0 /\ p_14^post1-x_13^0 == 0 /\ st_17^0-st_17^post1 == 0), cost: 1 1: l1 -> l2 : lt_15^0'=lt_15^post2, lt_19^0'=lt_19^post2, nd_12^0'=nd_12^post2, p_14^0'=p_14^post2, rt_11^0'=rt_11^post2, rv_18^0'=rv_18^post2, st_17^0'=st_17^post2, x_13^0'=x_13^post2, y_16^0'=y_16^post2, (0 == 0 /\ -x_13^post2+x_13^0 == 0 /\ -st_17^post2+st_17^0 == 0 /\ y_16^0-y_16^post2 == 0 /\ -lt_19^post2+lt_19^0 == 0 /\ nd_12^0-nd_12^post2 == 0 /\ -st_17^0+rt_11^post2 == 0 /\ p_14^0-p_14^post2 == 0 /\ rv_18^0-rv_18^post2 == 0 /\ -lt_15^0+y_16^0 <= 0), cost: 1 2: l1 -> l3 : lt_15^0'=lt_15^post3, lt_19^0'=lt_19^post3, nd_12^0'=nd_12^post3, p_14^0'=p_14^post3, rt_11^0'=rt_11^post3, rv_18^0'=rv_18^post3, st_17^0'=st_17^post3, x_13^0'=x_13^post3, y_16^0'=y_16^post3, (0 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -lt_19^post3+lt_19^0 == 0 /\ y_16^0-y_16^post3 == 0 /\ 1+lt_15^0-y_16^0 <= 0 /\ -nd_12^1+rv_18^post3 == 0 /\ rt_11^0-rt_11^post3 == 0 /\ -rv_18^post3 <= 0 /\ p_14^0-p_14^post3 == 0 /\ rv_18^post3 <= 0 /\ -st_17^post3+st_17^0 == 0), cost: 1 4: l1 -> l5 : lt_15^0'=lt_15^post5, lt_19^0'=lt_19^post5, nd_12^0'=nd_12^post5, p_14^0'=p_14^post5, rt_11^0'=rt_11^post5, rv_18^0'=rv_18^post5, st_17^0'=st_17^post5, x_13^0'=x_13^post5, y_16^0'=y_16^post5, (0 == 0 /\ y_16^0-y_16^post5 == 0 /\ -p_14^post5+p_14^0 == 0 /\ rt_11^0-rt_11^post5 == 0 /\ -lt_19^post5+lt_19^0 == 0 /\ -x_13^post5+x_13^0 == 0 /\ 1+lt_15^0-y_16^0 <= 0 /\ -nd_12^1+rv_18^post5 == 0 /\ -st_17^post5+st_17^0 == 0), cost: 1 3: l3 -> l1 : lt_15^0'=lt_15^post4, lt_19^0'=lt_19^post4, nd_12^0'=nd_12^post4, p_14^0'=p_14^post4, rt_11^0'=rt_11^post4, rv_18^0'=rv_18^post4, st_17^0'=st_17^post4, x_13^0'=x_13^post4, y_16^0'=y_16^post4, (-x_13^post4+x_13^0 == 0 /\ p_14^0-p_14^post4 == 0 /\ -st_17^post4+st_17^0 == 0 /\ y_16^0-y_16^post4 == 0 /\ -lt_19^post4+lt_19^0 == 0 /\ nd_12^0-nd_12^post4 == 0 /\ lt_15^0-lt_15^post4 == 0 /\ rv_18^0-rv_18^post4 == 0 /\ rt_11^0-rt_11^post4 == 0), cost: 1 5: l5 -> l6 : lt_15^0'=lt_15^post6, lt_19^0'=lt_19^post6, nd_12^0'=nd_12^post6, p_14^0'=p_14^post6, rt_11^0'=rt_11^post6, rv_18^0'=rv_18^post6, st_17^0'=st_17^post6, x_13^0'=x_13^post6, y_16^0'=y_16^post6, (p_14^0-p_14^post6 == 0 /\ rt_11^0-rt_11^post6 == 0 /\ -rv_18^post6+rv_18^0 == 0 /\ -lt_15^post6+lt_15^0 == 0 /\ 1-rv_18^0 <= 0 /\ y_16^0-y_16^post6 == 0 /\ -x_13^post6+x_13^0 == 0 /\ nd_12^0-nd_12^post6 == 0 /\ -st_17^post6+st_17^0 == 0 /\ -lt_19^post6+lt_19^0 == 0), cost: 1 6: l5 -> l6 : lt_15^0'=lt_15^post7, lt_19^0'=lt_19^post7, nd_12^0'=nd_12^post7, p_14^0'=p_14^post7, rt_11^0'=rt_11^post7, rv_18^0'=rv_18^post7, st_17^0'=st_17^post7, x_13^0'=x_13^post7, y_16^0'=y_16^post7, (st_17^0-st_17^post7 == 0 /\ -p_14^post7+p_14^0 == 0 /\ -rv_18^post7+rv_18^0 == 0 /\ nd_12^0-nd_12^post7 == 0 /\ 1+rv_18^0 <= 0 /\ rt_11^0-rt_11^post7 == 0 /\ lt_15^0-lt_15^post7 == 0 /\ -x_13^post7+x_13^0 == 0 /\ -lt_19^post7+lt_19^0 == 0 /\ y_16^0-y_16^post7 == 0), cost: 1 7: l6 -> l4 : lt_15^0'=lt_15^post8, lt_19^0'=lt_19^post8, nd_12^0'=nd_12^post8, p_14^0'=p_14^post8, rt_11^0'=rt_11^post8, rv_18^0'=rv_18^post8, st_17^0'=st_17^post8, x_13^0'=x_13^post8, y_16^0'=y_16^post8, (0 == 0 /\ -rv_18^post8+rv_18^0 == 0 /\ -rt_11^post8+rt_11^0 == 0 /\ lt_15^0-lt_15^post8 == 0 /\ st_17^0-st_17^post8 == 0 /\ -y_16^post8+y_16^0 == 0 /\ -nd_12^post8+nd_12^0 == 0 /\ p_14^0-p_14^post8 == 0 /\ -x_13^post8+x_13^0 == 0), cost: 1 8: l4 -> l1 : lt_15^0'=lt_15^post9, lt_19^0'=lt_19^post9, nd_12^0'=nd_12^post9, p_14^0'=p_14^post9, rt_11^0'=rt_11^post9, rv_18^0'=rv_18^post9, st_17^0'=st_17^post9, x_13^0'=x_13^post9, y_16^0'=y_16^post9, (-x_13^post9+x_13^0 == 0 /\ lt_15^0-lt_15^post9 == 0 /\ st_17^0-st_17^post9 == 0 /\ rt_11^0-rt_11^post9 == 0 /\ -nd_12^post9+nd_12^0 == 0 /\ -lt_19^post9+lt_19^0 == 0 /\ p_14^0-p_14^post9 == 0 /\ -y_16^post9+y_16^0 == 0 /\ -rv_18^post9+rv_18^0 == 0), cost: 1 9: l7 -> l0 : lt_15^0'=lt_15^post10, lt_19^0'=lt_19^post10, nd_12^0'=nd_12^post10, p_14^0'=p_14^post10, rt_11^0'=rt_11^post10, rv_18^0'=rv_18^post10, st_17^0'=st_17^post10, x_13^0'=x_13^post10, y_16^0'=y_16^post10, (y_16^0-y_16^post10 == 0 /\ -x_13^post10+x_13^0 == 0 /\ -st_17^post10+st_17^0 == 0 /\ -lt_19^post10+lt_19^0 == 0 /\ nd_12^0-nd_12^post10 == 0 /\ p_14^0-p_14^post10 == 0 /\ rv_18^0-rv_18^post10 == 0 /\ rt_11^0-rt_11^post10 == 0 /\ lt_15^0-lt_15^post10 == 0), cost: 1 Chained Linear Paths Start location: l7 Program variables: lt_15^0 lt_19^0 nd_12^0 p_14^0 rt_11^0 rv_18^0 st_17^0 x_13^0 y_16^0 1: l1 -> l2 : lt_15^0'=lt_15^post2, lt_19^0'=lt_19^post2, nd_12^0'=nd_12^post2, p_14^0'=p_14^post2, rt_11^0'=rt_11^post2, rv_18^0'=rv_18^post2, st_17^0'=st_17^post2, x_13^0'=x_13^post2, y_16^0'=y_16^post2, (0 == 0 /\ -x_13^post2+x_13^0 == 0 /\ -st_17^post2+st_17^0 == 0 /\ y_16^0-y_16^post2 == 0 /\ -lt_19^post2+lt_19^0 == 0 /\ nd_12^0-nd_12^post2 == 0 /\ -st_17^0+rt_11^post2 == 0 /\ p_14^0-p_14^post2 == 0 /\ rv_18^0-rv_18^post2 == 0 /\ -lt_15^0+y_16^0 <= 0), cost: 1 4: l1 -> l5 : lt_15^0'=lt_15^post5, lt_19^0'=lt_19^post5, nd_12^0'=nd_12^post5, p_14^0'=p_14^post5, rt_11^0'=rt_11^post5, rv_18^0'=rv_18^post5, st_17^0'=st_17^post5, x_13^0'=x_13^post5, y_16^0'=y_16^post5, (0 == 0 /\ y_16^0-y_16^post5 == 0 /\ -p_14^post5+p_14^0 == 0 /\ rt_11^0-rt_11^post5 == 0 /\ -lt_19^post5+lt_19^0 == 0 /\ -x_13^post5+x_13^0 == 0 /\ 1+lt_15^0-y_16^0 <= 0 /\ -nd_12^1+rv_18^post5 == 0 /\ -st_17^post5+st_17^0 == 0), cost: 1 11: l1 -> l1 : lt_15^0'=lt_15^post4, lt_19^0'=lt_19^post4, nd_12^0'=nd_12^post4, p_14^0'=p_14^post4, rt_11^0'=rt_11^post4, rv_18^0'=rv_18^post4, st_17^0'=st_17^post4, x_13^0'=x_13^post4, y_16^0'=y_16^post4, (0 == 0 /\ -st_17^post4+st_17^post3 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -lt_19^post3+lt_19^0 == 0 /\ -lt_19^post4+lt_19^post3 == 0 /\ y_16^0-y_16^post3 == 0 /\ -rt_11^post4+rt_11^post3 == 0 /\ -p_14^post4+p_14^post3 == 0 /\ 1+lt_15^0-y_16^0 <= 0 /\ nd_12^post3-nd_12^post4 == 0 /\ -rv_18^post4+rv_18^post3 == 0 /\ -nd_12^1+rv_18^post3 == 0 /\ -x_13^post4+x_13^post3 == 0 /\ rt_11^0-rt_11^post3 == 0 /\ -y_16^post4+y_16^post3 == 0 /\ -lt_15^post4+lt_15^post3 == 0 /\ -rv_18^post3 <= 0 /\ p_14^0-p_14^post3 == 0 /\ rv_18^post3 <= 0 /\ -st_17^post3+st_17^0 == 0), cost: 1 5: l5 -> l6 : lt_15^0'=lt_15^post6, lt_19^0'=lt_19^post6, nd_12^0'=nd_12^post6, p_14^0'=p_14^post6, rt_11^0'=rt_11^post6, rv_18^0'=rv_18^post6, st_17^0'=st_17^post6, x_13^0'=x_13^post6, y_16^0'=y_16^post6, (p_14^0-p_14^post6 == 0 /\ rt_11^0-rt_11^post6 == 0 /\ -rv_18^post6+rv_18^0 == 0 /\ -lt_15^post6+lt_15^0 == 0 /\ 1-rv_18^0 <= 0 /\ y_16^0-y_16^post6 == 0 /\ -x_13^post6+x_13^0 == 0 /\ nd_12^0-nd_12^post6 == 0 /\ -st_17^post6+st_17^0 == 0 /\ -lt_19^post6+lt_19^0 == 0), cost: 1 6: l5 -> l6 : lt_15^0'=lt_15^post7, lt_19^0'=lt_19^post7, nd_12^0'=nd_12^post7, p_14^0'=p_14^post7, rt_11^0'=rt_11^post7, rv_18^0'=rv_18^post7, st_17^0'=st_17^post7, x_13^0'=x_13^post7, y_16^0'=y_16^post7, (st_17^0-st_17^post7 == 0 /\ -p_14^post7+p_14^0 == 0 /\ -rv_18^post7+rv_18^0 == 0 /\ nd_12^0-nd_12^post7 == 0 /\ 1+rv_18^0 <= 0 /\ rt_11^0-rt_11^post7 == 0 /\ lt_15^0-lt_15^post7 == 0 /\ -x_13^post7+x_13^0 == 0 /\ -lt_19^post7+lt_19^0 == 0 /\ y_16^0-y_16^post7 == 0), cost: 1 12: l6 -> l1 : lt_15^0'=lt_15^post9, lt_19^0'=lt_19^post9, nd_12^0'=nd_12^post9, p_14^0'=p_14^post9, rt_11^0'=rt_11^post9, rv_18^0'=rv_18^post9, st_17^0'=st_17^post9, x_13^0'=x_13^post9, y_16^0'=y_16^post9, (0 == 0 /\ -rv_18^post8+rv_18^0 == 0 /\ -rt_11^post8+rt_11^0 == 0 /\ x_13^post8-x_13^post9 == 0 /\ -lt_15^post9+lt_15^post8 == 0 /\ -p_14^post9+p_14^post8 == 0 /\ lt_19^post8-lt_19^post9 == 0 /\ -nd_12^post9+nd_12^post8 == 0 /\ rt_11^post8-rt_11^post9 == 0 /\ -y_16^post9+y_16^post8 == 0 /\ lt_15^0-lt_15^post8 == 0 /\ st_17^0-st_17^post8 == 0 /\ -y_16^post8+y_16^0 == 0 /\ -rv_18^post9+rv_18^post8 == 0 /\ -st_17^post9+st_17^post8 == 0 /\ -nd_12^post8+nd_12^0 == 0 /\ p_14^0-p_14^post8 == 0 /\ -x_13^post8+x_13^0 == 0), cost: 1 10: l7 -> l1 : lt_15^0'=lt_15^post1, lt_19^0'=lt_19^post1, nd_12^0'=nd_12^post1, p_14^0'=p_14^post1, rt_11^0'=rt_11^post1, rv_18^0'=rv_18^post1, st_17^0'=st_17^post1, x_13^0'=x_13^post1, y_16^0'=y_16^post1, (lt_19^post10-lt_19^post1 == 0 /\ y_16^0-y_16^post10 == 0 /\ -x_13^post10+x_13^0 == 0 /\ x_13^post10-x_13^post1 == 0 /\ -rv_18^post1+rv_18^post10 == 0 /\ -st_17^post10+st_17^0 == 0 /\ lt_15^post10-lt_15^post1 == 0 /\ -y_16^post1+y_16^post10 == 0 /\ -lt_19^post10+lt_19^0 == 0 /\ nd_12^0-nd_12^post10 == 0 /\ p_14^0-p_14^post10 == 0 /\ rv_18^0-rv_18^post10 == 0 /\ -nd_12^post1+nd_12^post10 == 0 /\ rt_11^0-rt_11^post10 == 0 /\ st_17^post10-st_17^post1 == 0 /\ rt_11^post10-rt_11^post1 == 0 /\ lt_15^0-lt_15^post10 == 0 /\ -x_13^post10+p_14^post1 == 0), cost: 1 Eliminating location l0 by chaining: Applied chaining First rule: l7 -> l0 : lt_15^0'=lt_15^post10, lt_19^0'=lt_19^post10, nd_12^0'=nd_12^post10, p_14^0'=p_14^post10, rt_11^0'=rt_11^post10, rv_18^0'=rv_18^post10, st_17^0'=st_17^post10, x_13^0'=x_13^post10, y_16^0'=y_16^post10, (y_16^0-y_16^post10 == 0 /\ -x_13^post10+x_13^0 == 0 /\ -st_17^post10+st_17^0 == 0 /\ -lt_19^post10+lt_19^0 == 0 /\ nd_12^0-nd_12^post10 == 0 /\ p_14^0-p_14^post10 == 0 /\ rv_18^0-rv_18^post10 == 0 /\ rt_11^0-rt_11^post10 == 0 /\ lt_15^0-lt_15^post10 == 0), cost: 1 Second rule: l0 -> l1 : lt_15^0'=lt_15^post1, lt_19^0'=lt_19^post1, nd_12^0'=nd_12^post1, p_14^0'=p_14^post1, rt_11^0'=rt_11^post1, rv_18^0'=rv_18^post1, st_17^0'=st_17^post1, x_13^0'=x_13^post1, y_16^0'=y_16^post1, (lt_15^0-lt_15^post1 == 0 /\ lt_19^0-lt_19^post1 == 0 /\ rt_11^0-rt_11^post1 == 0 /\ -nd_12^post1+nd_12^0 == 0 /\ -rv_18^post1+rv_18^0 == 0 /\ -y_16^post1+y_16^0 == 0 /\ -x_13^post1+x_13^0 == 0 /\ p_14^post1-x_13^0 == 0 /\ st_17^0-st_17^post1 == 0), cost: 1 New rule: l7 -> l1 : lt_15^0'=lt_15^post1, lt_19^0'=lt_19^post1, nd_12^0'=nd_12^post1, p_14^0'=p_14^post1, rt_11^0'=rt_11^post1, rv_18^0'=rv_18^post1, st_17^0'=st_17^post1, x_13^0'=x_13^post1, y_16^0'=y_16^post1, (lt_19^post10-lt_19^post1 == 0 /\ y_16^0-y_16^post10 == 0 /\ -x_13^post10+x_13^0 == 0 /\ x_13^post10-x_13^post1 == 0 /\ -rv_18^post1+rv_18^post10 == 0 /\ -st_17^post10+st_17^0 == 0 /\ lt_15^post10-lt_15^post1 == 0 /\ -y_16^post1+y_16^post10 == 0 /\ -lt_19^post10+lt_19^0 == 0 /\ nd_12^0-nd_12^post10 == 0 /\ p_14^0-p_14^post10 == 0 /\ rv_18^0-rv_18^post10 == 0 /\ -nd_12^post1+nd_12^post10 == 0 /\ rt_11^0-rt_11^post10 == 0 /\ st_17^post10-st_17^post1 == 0 /\ rt_11^post10-rt_11^post1 == 0 /\ lt_15^0-lt_15^post10 == 0 /\ -x_13^post10+p_14^post1 == 0), cost: 1 Applied deletion Removed the following rules: 0 9 Eliminating location l3 by chaining: Applied chaining First rule: l1 -> l3 : lt_15^0'=lt_15^post3, lt_19^0'=lt_19^post3, nd_12^0'=nd_12^post3, p_14^0'=p_14^post3, rt_11^0'=rt_11^post3, rv_18^0'=rv_18^post3, st_17^0'=st_17^post3, x_13^0'=x_13^post3, y_16^0'=y_16^post3, (0 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -lt_19^post3+lt_19^0 == 0 /\ y_16^0-y_16^post3 == 0 /\ 1+lt_15^0-y_16^0 <= 0 /\ -nd_12^1+rv_18^post3 == 0 /\ rt_11^0-rt_11^post3 == 0 /\ -rv_18^post3 <= 0 /\ p_14^0-p_14^post3 == 0 /\ rv_18^post3 <= 0 /\ -st_17^post3+st_17^0 == 0), cost: 1 Second rule: l3 -> l1 : lt_15^0'=lt_15^post4, lt_19^0'=lt_19^post4, nd_12^0'=nd_12^post4, p_14^0'=p_14^post4, rt_11^0'=rt_11^post4, rv_18^0'=rv_18^post4, st_17^0'=st_17^post4, x_13^0'=x_13^post4, y_16^0'=y_16^post4, (-x_13^post4+x_13^0 == 0 /\ p_14^0-p_14^post4 == 0 /\ -st_17^post4+st_17^0 == 0 /\ y_16^0-y_16^post4 == 0 /\ -lt_19^post4+lt_19^0 == 0 /\ nd_12^0-nd_12^post4 == 0 /\ lt_15^0-lt_15^post4 == 0 /\ rv_18^0-rv_18^post4 == 0 /\ rt_11^0-rt_11^post4 == 0), cost: 1 New rule: l1 -> l1 : lt_15^0'=lt_15^post4, lt_19^0'=lt_19^post4, nd_12^0'=nd_12^post4, p_14^0'=p_14^post4, rt_11^0'=rt_11^post4, rv_18^0'=rv_18^post4, st_17^0'=st_17^post4, x_13^0'=x_13^post4, y_16^0'=y_16^post4, (0 == 0 /\ -st_17^post4+st_17^post3 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -lt_19^post3+lt_19^0 == 0 /\ -lt_19^post4+lt_19^post3 == 0 /\ y_16^0-y_16^post3 == 0 /\ -rt_11^post4+rt_11^post3 == 0 /\ -p_14^post4+p_14^post3 == 0 /\ 1+lt_15^0-y_16^0 <= 0 /\ nd_12^post3-nd_12^post4 == 0 /\ -rv_18^post4+rv_18^post3 == 0 /\ -nd_12^1+rv_18^post3 == 0 /\ -x_13^post4+x_13^post3 == 0 /\ rt_11^0-rt_11^post3 == 0 /\ -y_16^post4+y_16^post3 == 0 /\ -lt_15^post4+lt_15^post3 == 0 /\ -rv_18^post3 <= 0 /\ p_14^0-p_14^post3 == 0 /\ rv_18^post3 <= 0 /\ -st_17^post3+st_17^0 == 0), cost: 1 Applied deletion Removed the following rules: 2 3 Eliminating location l4 by chaining: Applied chaining First rule: l6 -> l4 : lt_15^0'=lt_15^post8, lt_19^0'=lt_19^post8, nd_12^0'=nd_12^post8, p_14^0'=p_14^post8, rt_11^0'=rt_11^post8, rv_18^0'=rv_18^post8, st_17^0'=st_17^post8, x_13^0'=x_13^post8, y_16^0'=y_16^post8, (0 == 0 /\ -rv_18^post8+rv_18^0 == 0 /\ -rt_11^post8+rt_11^0 == 0 /\ lt_15^0-lt_15^post8 == 0 /\ st_17^0-st_17^post8 == 0 /\ -y_16^post8+y_16^0 == 0 /\ -nd_12^post8+nd_12^0 == 0 /\ p_14^0-p_14^post8 == 0 /\ -x_13^post8+x_13^0 == 0), cost: 1 Second rule: l4 -> l1 : lt_15^0'=lt_15^post9, lt_19^0'=lt_19^post9, nd_12^0'=nd_12^post9, p_14^0'=p_14^post9, rt_11^0'=rt_11^post9, rv_18^0'=rv_18^post9, st_17^0'=st_17^post9, x_13^0'=x_13^post9, y_16^0'=y_16^post9, (-x_13^post9+x_13^0 == 0 /\ lt_15^0-lt_15^post9 == 0 /\ st_17^0-st_17^post9 == 0 /\ rt_11^0-rt_11^post9 == 0 /\ -nd_12^post9+nd_12^0 == 0 /\ -lt_19^post9+lt_19^0 == 0 /\ p_14^0-p_14^post9 == 0 /\ -y_16^post9+y_16^0 == 0 /\ -rv_18^post9+rv_18^0 == 0), cost: 1 New rule: l6 -> l1 : lt_15^0'=lt_15^post9, lt_19^0'=lt_19^post9, nd_12^0'=nd_12^post9, p_14^0'=p_14^post9, rt_11^0'=rt_11^post9, rv_18^0'=rv_18^post9, st_17^0'=st_17^post9, x_13^0'=x_13^post9, y_16^0'=y_16^post9, (0 == 0 /\ -rv_18^post8+rv_18^0 == 0 /\ -rt_11^post8+rt_11^0 == 0 /\ x_13^post8-x_13^post9 == 0 /\ -lt_15^post9+lt_15^post8 == 0 /\ -p_14^post9+p_14^post8 == 0 /\ lt_19^post8-lt_19^post9 == 0 /\ -nd_12^post9+nd_12^post8 == 0 /\ rt_11^post8-rt_11^post9 == 0 /\ -y_16^post9+y_16^post8 == 0 /\ lt_15^0-lt_15^post8 == 0 /\ st_17^0-st_17^post8 == 0 /\ -y_16^post8+y_16^0 == 0 /\ -rv_18^post9+rv_18^post8 == 0 /\ -st_17^post9+st_17^post8 == 0 /\ -nd_12^post8+nd_12^0 == 0 /\ p_14^0-p_14^post8 == 0 /\ -x_13^post8+x_13^0 == 0), cost: 1 Applied deletion Removed the following rules: 7 8 Simplified Transitions Start location: l7 Program variables: lt_15^0 lt_19^0 nd_12^0 p_14^0 rt_11^0 rv_18^0 st_17^0 x_13^0 y_16^0 13: l1 -> l2 : lt_15^0'=lt_15^post2, rt_11^0'=st_17^0, -lt_15^0+y_16^0 <= 0, cost: 1 14: l1 -> l5 : lt_15^0'=lt_15^post5, nd_12^0'=nd_12^post5, rv_18^0'=nd_12^1, 1+lt_15^0-y_16^0 <= 0, cost: 1 18: l1 -> l1 : lt_15^0'=lt_15^post3, nd_12^0'=nd_12^post3, rv_18^0'=0, 1+lt_15^0-y_16^0 <= 0, cost: 1 15: l5 -> l6 : 1-rv_18^0 <= 0, cost: 1 16: l5 -> l6 : 1+rv_18^0 <= 0, cost: 1 19: l6 -> l1 : lt_19^0'=lt_19^post8, T, cost: 1 17: l7 -> l1 : p_14^0'=x_13^0, T, cost: 1 Propagated Equalities Original rule: l1 -> l2 : lt_15^0'=lt_15^post2, lt_19^0'=lt_19^post2, nd_12^0'=nd_12^post2, p_14^0'=p_14^post2, rt_11^0'=rt_11^post2, rv_18^0'=rv_18^post2, st_17^0'=st_17^post2, x_13^0'=x_13^post2, y_16^0'=y_16^post2, (0 == 0 /\ -x_13^post2+x_13^0 == 0 /\ -st_17^post2+st_17^0 == 0 /\ y_16^0-y_16^post2 == 0 /\ -lt_19^post2+lt_19^0 == 0 /\ nd_12^0-nd_12^post2 == 0 /\ -st_17^0+rt_11^post2 == 0 /\ p_14^0-p_14^post2 == 0 /\ rv_18^0-rv_18^post2 == 0 /\ -lt_15^0+y_16^0 <= 0), cost: 1 New rule: l1 -> l2 : lt_15^0'=lt_15^post2, lt_19^0'=lt_19^0, nd_12^0'=nd_12^0, p_14^0'=p_14^0, rt_11^0'=st_17^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, (0 == 0 /\ -lt_15^0+y_16^0 <= 0), cost: 1 propagated equality x_13^post2 = x_13^0 propagated equality st_17^post2 = st_17^0 propagated equality y_16^post2 = y_16^0 propagated equality lt_19^post2 = lt_19^0 propagated equality nd_12^post2 = nd_12^0 propagated equality rt_11^post2 = st_17^0 propagated equality p_14^post2 = p_14^0 propagated equality rv_18^post2 = rv_18^0 Simplified Guard Original rule: l1 -> l2 : lt_15^0'=lt_15^post2, lt_19^0'=lt_19^0, nd_12^0'=nd_12^0, p_14^0'=p_14^0, rt_11^0'=st_17^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, (0 == 0 /\ -lt_15^0+y_16^0 <= 0), cost: 1 New rule: l1 -> l2 : lt_15^0'=lt_15^post2, lt_19^0'=lt_19^0, nd_12^0'=nd_12^0, p_14^0'=p_14^0, rt_11^0'=st_17^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, -lt_15^0+y_16^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l2 : lt_15^0'=lt_15^post2, lt_19^0'=lt_19^0, nd_12^0'=nd_12^0, p_14^0'=p_14^0, rt_11^0'=st_17^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, -lt_15^0+y_16^0 <= 0, cost: 1 New rule: l1 -> l2 : lt_15^0'=lt_15^post2, rt_11^0'=st_17^0, -lt_15^0+y_16^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l5 : lt_15^0'=lt_15^post5, lt_19^0'=lt_19^post5, nd_12^0'=nd_12^post5, p_14^0'=p_14^post5, rt_11^0'=rt_11^post5, rv_18^0'=rv_18^post5, st_17^0'=st_17^post5, x_13^0'=x_13^post5, y_16^0'=y_16^post5, (0 == 0 /\ y_16^0-y_16^post5 == 0 /\ -p_14^post5+p_14^0 == 0 /\ rt_11^0-rt_11^post5 == 0 /\ -lt_19^post5+lt_19^0 == 0 /\ -x_13^post5+x_13^0 == 0 /\ 1+lt_15^0-y_16^0 <= 0 /\ -nd_12^1+rv_18^post5 == 0 /\ -st_17^post5+st_17^0 == 0), cost: 1 New rule: l1 -> l5 : lt_15^0'=lt_15^post5, lt_19^0'=lt_19^0, nd_12^0'=nd_12^post5, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=nd_12^1, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, (0 == 0 /\ 1+lt_15^0-y_16^0 <= 0), cost: 1 propagated equality y_16^post5 = y_16^0 propagated equality p_14^post5 = p_14^0 propagated equality rt_11^post5 = rt_11^0 propagated equality lt_19^post5 = lt_19^0 propagated equality x_13^post5 = x_13^0 propagated equality rv_18^post5 = nd_12^1 propagated equality st_17^post5 = st_17^0 Simplified Guard Original rule: l1 -> l5 : lt_15^0'=lt_15^post5, lt_19^0'=lt_19^0, nd_12^0'=nd_12^post5, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=nd_12^1, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, (0 == 0 /\ 1+lt_15^0-y_16^0 <= 0), cost: 1 New rule: l1 -> l5 : lt_15^0'=lt_15^post5, lt_19^0'=lt_19^0, nd_12^0'=nd_12^post5, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=nd_12^1, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, 1+lt_15^0-y_16^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l5 : lt_15^0'=lt_15^post5, lt_19^0'=lt_19^0, nd_12^0'=nd_12^post5, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=nd_12^1, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, 1+lt_15^0-y_16^0 <= 0, cost: 1 New rule: l1 -> l5 : lt_15^0'=lt_15^post5, nd_12^0'=nd_12^post5, rv_18^0'=nd_12^1, 1+lt_15^0-y_16^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l6 : lt_15^0'=lt_15^post6, lt_19^0'=lt_19^post6, nd_12^0'=nd_12^post6, p_14^0'=p_14^post6, rt_11^0'=rt_11^post6, rv_18^0'=rv_18^post6, st_17^0'=st_17^post6, x_13^0'=x_13^post6, y_16^0'=y_16^post6, (p_14^0-p_14^post6 == 0 /\ rt_11^0-rt_11^post6 == 0 /\ -rv_18^post6+rv_18^0 == 0 /\ -lt_15^post6+lt_15^0 == 0 /\ 1-rv_18^0 <= 0 /\ y_16^0-y_16^post6 == 0 /\ -x_13^post6+x_13^0 == 0 /\ nd_12^0-nd_12^post6 == 0 /\ -st_17^post6+st_17^0 == 0 /\ -lt_19^post6+lt_19^0 == 0), cost: 1 New rule: l5 -> l6 : lt_15^0'=lt_15^0, lt_19^0'=lt_19^0, nd_12^0'=nd_12^0, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, (0 == 0 /\ 1-rv_18^0 <= 0), cost: 1 propagated equality p_14^post6 = p_14^0 propagated equality rt_11^post6 = rt_11^0 propagated equality rv_18^post6 = rv_18^0 propagated equality lt_15^post6 = lt_15^0 propagated equality y_16^post6 = y_16^0 propagated equality x_13^post6 = x_13^0 propagated equality nd_12^post6 = nd_12^0 propagated equality st_17^post6 = st_17^0 propagated equality lt_19^post6 = lt_19^0 Simplified Guard Original rule: l5 -> l6 : lt_15^0'=lt_15^0, lt_19^0'=lt_19^0, nd_12^0'=nd_12^0, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, (0 == 0 /\ 1-rv_18^0 <= 0), cost: 1 New rule: l5 -> l6 : lt_15^0'=lt_15^0, lt_19^0'=lt_19^0, nd_12^0'=nd_12^0, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, 1-rv_18^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l6 : lt_15^0'=lt_15^0, lt_19^0'=lt_19^0, nd_12^0'=nd_12^0, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, 1-rv_18^0 <= 0, cost: 1 New rule: l5 -> l6 : 1-rv_18^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l6 : lt_15^0'=lt_15^post7, lt_19^0'=lt_19^post7, nd_12^0'=nd_12^post7, p_14^0'=p_14^post7, rt_11^0'=rt_11^post7, rv_18^0'=rv_18^post7, st_17^0'=st_17^post7, x_13^0'=x_13^post7, y_16^0'=y_16^post7, (st_17^0-st_17^post7 == 0 /\ -p_14^post7+p_14^0 == 0 /\ -rv_18^post7+rv_18^0 == 0 /\ nd_12^0-nd_12^post7 == 0 /\ 1+rv_18^0 <= 0 /\ rt_11^0-rt_11^post7 == 0 /\ lt_15^0-lt_15^post7 == 0 /\ -x_13^post7+x_13^0 == 0 /\ -lt_19^post7+lt_19^0 == 0 /\ y_16^0-y_16^post7 == 0), cost: 1 New rule: l5 -> l6 : lt_15^0'=lt_15^0, lt_19^0'=lt_19^0, nd_12^0'=nd_12^0, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, (0 == 0 /\ 1+rv_18^0 <= 0), cost: 1 propagated equality st_17^post7 = st_17^0 propagated equality p_14^post7 = p_14^0 propagated equality rv_18^post7 = rv_18^0 propagated equality nd_12^post7 = nd_12^0 propagated equality rt_11^post7 = rt_11^0 propagated equality lt_15^post7 = lt_15^0 propagated equality x_13^post7 = x_13^0 propagated equality lt_19^post7 = lt_19^0 propagated equality y_16^post7 = y_16^0 Simplified Guard Original rule: l5 -> l6 : lt_15^0'=lt_15^0, lt_19^0'=lt_19^0, nd_12^0'=nd_12^0, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, (0 == 0 /\ 1+rv_18^0 <= 0), cost: 1 New rule: l5 -> l6 : lt_15^0'=lt_15^0, lt_19^0'=lt_19^0, nd_12^0'=nd_12^0, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, 1+rv_18^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l6 : lt_15^0'=lt_15^0, lt_19^0'=lt_19^0, nd_12^0'=nd_12^0, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, 1+rv_18^0 <= 0, cost: 1 New rule: l5 -> l6 : 1+rv_18^0 <= 0, cost: 1 Propagated Equalities Original rule: l7 -> l1 : lt_15^0'=lt_15^post1, lt_19^0'=lt_19^post1, nd_12^0'=nd_12^post1, p_14^0'=p_14^post1, rt_11^0'=rt_11^post1, rv_18^0'=rv_18^post1, st_17^0'=st_17^post1, x_13^0'=x_13^post1, y_16^0'=y_16^post1, (lt_19^post10-lt_19^post1 == 0 /\ y_16^0-y_16^post10 == 0 /\ -x_13^post10+x_13^0 == 0 /\ x_13^post10-x_13^post1 == 0 /\ -rv_18^post1+rv_18^post10 == 0 /\ -st_17^post10+st_17^0 == 0 /\ lt_15^post10-lt_15^post1 == 0 /\ -y_16^post1+y_16^post10 == 0 /\ -lt_19^post10+lt_19^0 == 0 /\ nd_12^0-nd_12^post10 == 0 /\ p_14^0-p_14^post10 == 0 /\ rv_18^0-rv_18^post10 == 0 /\ -nd_12^post1+nd_12^post10 == 0 /\ rt_11^0-rt_11^post10 == 0 /\ st_17^post10-st_17^post1 == 0 /\ rt_11^post10-rt_11^post1 == 0 /\ lt_15^0-lt_15^post10 == 0 /\ -x_13^post10+p_14^post1 == 0), cost: 1 New rule: l7 -> l1 : lt_15^0'=lt_15^post10, lt_19^0'=lt_19^post10, nd_12^0'=nd_12^post10, p_14^0'=x_13^post10, rt_11^0'=rt_11^post10, rv_18^0'=rv_18^post10, st_17^0'=st_17^post10, x_13^0'=x_13^post10, y_16^0'=y_16^post10, (0 == 0 /\ y_16^0-y_16^post10 == 0 /\ -x_13^post10+x_13^0 == 0 /\ -st_17^post10+st_17^0 == 0 /\ -lt_19^post10+lt_19^0 == 0 /\ nd_12^0-nd_12^post10 == 0 /\ p_14^0-p_14^post10 == 0 /\ rv_18^0-rv_18^post10 == 0 /\ rt_11^0-rt_11^post10 == 0 /\ lt_15^0-lt_15^post10 == 0), cost: 1 propagated equality lt_19^post1 = lt_19^post10 propagated equality x_13^post1 = x_13^post10 propagated equality rv_18^post1 = rv_18^post10 propagated equality lt_15^post1 = lt_15^post10 propagated equality y_16^post1 = y_16^post10 propagated equality nd_12^post1 = nd_12^post10 propagated equality st_17^post1 = st_17^post10 propagated equality rt_11^post1 = rt_11^post10 propagated equality p_14^post1 = x_13^post10 Propagated Equalities Original rule: l7 -> l1 : lt_15^0'=lt_15^post10, lt_19^0'=lt_19^post10, nd_12^0'=nd_12^post10, p_14^0'=x_13^post10, rt_11^0'=rt_11^post10, rv_18^0'=rv_18^post10, st_17^0'=st_17^post10, x_13^0'=x_13^post10, y_16^0'=y_16^post10, (0 == 0 /\ y_16^0-y_16^post10 == 0 /\ -x_13^post10+x_13^0 == 0 /\ -st_17^post10+st_17^0 == 0 /\ -lt_19^post10+lt_19^0 == 0 /\ nd_12^0-nd_12^post10 == 0 /\ p_14^0-p_14^post10 == 0 /\ rv_18^0-rv_18^post10 == 0 /\ rt_11^0-rt_11^post10 == 0 /\ lt_15^0-lt_15^post10 == 0), cost: 1 New rule: l7 -> l1 : lt_15^0'=lt_15^0, lt_19^0'=lt_19^0, nd_12^0'=nd_12^0, p_14^0'=x_13^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, 0 == 0, cost: 1 propagated equality y_16^post10 = y_16^0 propagated equality x_13^post10 = x_13^0 propagated equality st_17^post10 = st_17^0 propagated equality lt_19^post10 = lt_19^0 propagated equality nd_12^post10 = nd_12^0 propagated equality p_14^post10 = p_14^0 propagated equality rv_18^post10 = rv_18^0 propagated equality rt_11^post10 = rt_11^0 propagated equality lt_15^post10 = lt_15^0 Simplified Guard Original rule: l7 -> l1 : lt_15^0'=lt_15^0, lt_19^0'=lt_19^0, nd_12^0'=nd_12^0, p_14^0'=x_13^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, 0 == 0, cost: 1 New rule: l7 -> l1 : lt_15^0'=lt_15^0, lt_19^0'=lt_19^0, nd_12^0'=nd_12^0, p_14^0'=x_13^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, T, cost: 1 Removed Trivial Updates Original rule: l7 -> l1 : lt_15^0'=lt_15^0, lt_19^0'=lt_19^0, nd_12^0'=nd_12^0, p_14^0'=x_13^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, T, cost: 1 New rule: l7 -> l1 : p_14^0'=x_13^0, T, cost: 1 made implied equalities explicit Original rule: l1 -> l1 : lt_15^0'=lt_15^post4, lt_19^0'=lt_19^post4, nd_12^0'=nd_12^post4, p_14^0'=p_14^post4, rt_11^0'=rt_11^post4, rv_18^0'=rv_18^post4, st_17^0'=st_17^post4, x_13^0'=x_13^post4, y_16^0'=y_16^post4, (0 == 0 /\ -st_17^post4+st_17^post3 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -lt_19^post3+lt_19^0 == 0 /\ -lt_19^post4+lt_19^post3 == 0 /\ y_16^0-y_16^post3 == 0 /\ -rt_11^post4+rt_11^post3 == 0 /\ -p_14^post4+p_14^post3 == 0 /\ 1+lt_15^0-y_16^0 <= 0 /\ nd_12^post3-nd_12^post4 == 0 /\ -rv_18^post4+rv_18^post3 == 0 /\ -nd_12^1+rv_18^post3 == 0 /\ -x_13^post4+x_13^post3 == 0 /\ rt_11^0-rt_11^post3 == 0 /\ -y_16^post4+y_16^post3 == 0 /\ -lt_15^post4+lt_15^post3 == 0 /\ -rv_18^post3 <= 0 /\ p_14^0-p_14^post3 == 0 /\ rv_18^post3 <= 0 /\ -st_17^post3+st_17^0 == 0), cost: 1 New rule: l1 -> l1 : lt_15^0'=lt_15^post4, lt_19^0'=lt_19^post4, nd_12^0'=nd_12^post4, p_14^0'=p_14^post4, rt_11^0'=rt_11^post4, rv_18^0'=rv_18^post4, st_17^0'=st_17^post4, x_13^0'=x_13^post4, y_16^0'=y_16^post4, (0 == 0 /\ -st_17^post4+st_17^post3 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -lt_19^post3+lt_19^0 == 0 /\ -lt_19^post4+lt_19^post3 == 0 /\ y_16^0-y_16^post3 == 0 /\ -rt_11^post4+rt_11^post3 == 0 /\ -p_14^post4+p_14^post3 == 0 /\ 1+lt_15^0-y_16^0 <= 0 /\ nd_12^post3-nd_12^post4 == 0 /\ -rv_18^post4+rv_18^post3 == 0 /\ -nd_12^1+rv_18^post3 == 0 /\ -x_13^post4+x_13^post3 == 0 /\ rt_11^0-rt_11^post3 == 0 /\ -y_16^post4+y_16^post3 == 0 /\ -lt_15^post4+lt_15^post3 == 0 /\ -rv_18^post3 <= 0 /\ -rv_18^post3 == 0 /\ p_14^0-p_14^post3 == 0 /\ rv_18^post3 <= 0 /\ -st_17^post3+st_17^0 == 0), cost: 1 Propagated Equalities Original rule: l1 -> l1 : lt_15^0'=lt_15^post4, lt_19^0'=lt_19^post4, nd_12^0'=nd_12^post4, p_14^0'=p_14^post4, rt_11^0'=rt_11^post4, rv_18^0'=rv_18^post4, st_17^0'=st_17^post4, x_13^0'=x_13^post4, y_16^0'=y_16^post4, (0 == 0 /\ -st_17^post4+st_17^post3 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -lt_19^post3+lt_19^0 == 0 /\ -lt_19^post4+lt_19^post3 == 0 /\ y_16^0-y_16^post3 == 0 /\ -rt_11^post4+rt_11^post3 == 0 /\ -p_14^post4+p_14^post3 == 0 /\ 1+lt_15^0-y_16^0 <= 0 /\ nd_12^post3-nd_12^post4 == 0 /\ -rv_18^post4+rv_18^post3 == 0 /\ -nd_12^1+rv_18^post3 == 0 /\ -x_13^post4+x_13^post3 == 0 /\ rt_11^0-rt_11^post3 == 0 /\ -y_16^post4+y_16^post3 == 0 /\ -lt_15^post4+lt_15^post3 == 0 /\ -rv_18^post3 <= 0 /\ -rv_18^post3 == 0 /\ p_14^0-p_14^post3 == 0 /\ rv_18^post3 <= 0 /\ -st_17^post3+st_17^0 == 0), cost: 1 New rule: l1 -> l1 : lt_15^0'=lt_15^post3, lt_19^0'=lt_19^post3, nd_12^0'=nd_12^post3, p_14^0'=p_14^post3, rt_11^0'=rt_11^post3, rv_18^0'=rv_18^post3, st_17^0'=st_17^post3, x_13^0'=x_13^post3, y_16^0'=y_16^post3, (0 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -lt_19^post3+lt_19^0 == 0 /\ y_16^0-y_16^post3 == 0 /\ 1+lt_15^0-y_16^0 <= 0 /\ -nd_12^1+rv_18^post3 == 0 /\ rt_11^0-rt_11^post3 == 0 /\ -rv_18^post3 <= 0 /\ -rv_18^post3 == 0 /\ p_14^0-p_14^post3 == 0 /\ rv_18^post3 <= 0 /\ -st_17^post3+st_17^0 == 0), cost: 1 propagated equality st_17^post4 = st_17^post3 propagated equality lt_19^post4 = lt_19^post3 propagated equality rt_11^post4 = rt_11^post3 propagated equality p_14^post4 = p_14^post3 propagated equality nd_12^post4 = nd_12^post3 propagated equality rv_18^post4 = rv_18^post3 propagated equality x_13^post4 = x_13^post3 propagated equality y_16^post4 = y_16^post3 propagated equality lt_15^post4 = lt_15^post3 Propagated Equalities Original rule: l1 -> l1 : lt_15^0'=lt_15^post3, lt_19^0'=lt_19^post3, nd_12^0'=nd_12^post3, p_14^0'=p_14^post3, rt_11^0'=rt_11^post3, rv_18^0'=rv_18^post3, st_17^0'=st_17^post3, x_13^0'=x_13^post3, y_16^0'=y_16^post3, (0 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -lt_19^post3+lt_19^0 == 0 /\ y_16^0-y_16^post3 == 0 /\ 1+lt_15^0-y_16^0 <= 0 /\ -nd_12^1+rv_18^post3 == 0 /\ rt_11^0-rt_11^post3 == 0 /\ -rv_18^post3 <= 0 /\ -rv_18^post3 == 0 /\ p_14^0-p_14^post3 == 0 /\ rv_18^post3 <= 0 /\ -st_17^post3+st_17^0 == 0), cost: 1 New rule: l1 -> l1 : lt_15^0'=lt_15^post3, lt_19^0'=lt_19^0, nd_12^0'=nd_12^post3, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, (0 <= 0 /\ 0 == 0 /\ 1+lt_15^0-y_16^0 <= 0), cost: 1 propagated equality x_13^post3 = x_13^0 propagated equality lt_19^post3 = lt_19^0 propagated equality y_16^post3 = y_16^0 propagated equality nd_12^1 = rv_18^post3 propagated equality rt_11^post3 = rt_11^0 propagated equality rv_18^post3 = 0 propagated equality p_14^post3 = p_14^0 propagated equality st_17^post3 = st_17^0 Simplified Guard Original rule: l1 -> l1 : lt_15^0'=lt_15^post3, lt_19^0'=lt_19^0, nd_12^0'=nd_12^post3, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, (0 <= 0 /\ 0 == 0 /\ 1+lt_15^0-y_16^0 <= 0), cost: 1 New rule: l1 -> l1 : lt_15^0'=lt_15^post3, lt_19^0'=lt_19^0, nd_12^0'=nd_12^post3, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, 1+lt_15^0-y_16^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l1 : lt_15^0'=lt_15^post3, lt_19^0'=lt_19^0, nd_12^0'=nd_12^post3, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, 1+lt_15^0-y_16^0 <= 0, cost: 1 New rule: l1 -> l1 : lt_15^0'=lt_15^post3, nd_12^0'=nd_12^post3, rv_18^0'=0, 1+lt_15^0-y_16^0 <= 0, cost: 1 Propagated Equalities Original rule: l6 -> l1 : lt_15^0'=lt_15^post9, lt_19^0'=lt_19^post9, nd_12^0'=nd_12^post9, p_14^0'=p_14^post9, rt_11^0'=rt_11^post9, rv_18^0'=rv_18^post9, st_17^0'=st_17^post9, x_13^0'=x_13^post9, y_16^0'=y_16^post9, (0 == 0 /\ -rv_18^post8+rv_18^0 == 0 /\ -rt_11^post8+rt_11^0 == 0 /\ x_13^post8-x_13^post9 == 0 /\ -lt_15^post9+lt_15^post8 == 0 /\ -p_14^post9+p_14^post8 == 0 /\ lt_19^post8-lt_19^post9 == 0 /\ -nd_12^post9+nd_12^post8 == 0 /\ rt_11^post8-rt_11^post9 == 0 /\ -y_16^post9+y_16^post8 == 0 /\ lt_15^0-lt_15^post8 == 0 /\ st_17^0-st_17^post8 == 0 /\ -y_16^post8+y_16^0 == 0 /\ -rv_18^post9+rv_18^post8 == 0 /\ -st_17^post9+st_17^post8 == 0 /\ -nd_12^post8+nd_12^0 == 0 /\ p_14^0-p_14^post8 == 0 /\ -x_13^post8+x_13^0 == 0), cost: 1 New rule: l6 -> l1 : lt_15^0'=lt_15^post8, lt_19^0'=lt_19^post8, nd_12^0'=nd_12^post8, p_14^0'=p_14^post8, rt_11^0'=rt_11^post8, rv_18^0'=rv_18^post8, st_17^0'=st_17^post8, x_13^0'=x_13^post8, y_16^0'=y_16^post8, (0 == 0 /\ -rv_18^post8+rv_18^0 == 0 /\ -rt_11^post8+rt_11^0 == 0 /\ lt_15^0-lt_15^post8 == 0 /\ st_17^0-st_17^post8 == 0 /\ -y_16^post8+y_16^0 == 0 /\ -nd_12^post8+nd_12^0 == 0 /\ p_14^0-p_14^post8 == 0 /\ -x_13^post8+x_13^0 == 0), cost: 1 propagated equality x_13^post9 = x_13^post8 propagated equality lt_15^post9 = lt_15^post8 propagated equality p_14^post9 = p_14^post8 propagated equality lt_19^post9 = lt_19^post8 propagated equality nd_12^post9 = nd_12^post8 propagated equality rt_11^post9 = rt_11^post8 propagated equality y_16^post9 = y_16^post8 propagated equality rv_18^post9 = rv_18^post8 propagated equality st_17^post9 = st_17^post8 Propagated Equalities Original rule: l6 -> l1 : lt_15^0'=lt_15^post8, lt_19^0'=lt_19^post8, nd_12^0'=nd_12^post8, p_14^0'=p_14^post8, rt_11^0'=rt_11^post8, rv_18^0'=rv_18^post8, st_17^0'=st_17^post8, x_13^0'=x_13^post8, y_16^0'=y_16^post8, (0 == 0 /\ -rv_18^post8+rv_18^0 == 0 /\ -rt_11^post8+rt_11^0 == 0 /\ lt_15^0-lt_15^post8 == 0 /\ st_17^0-st_17^post8 == 0 /\ -y_16^post8+y_16^0 == 0 /\ -nd_12^post8+nd_12^0 == 0 /\ p_14^0-p_14^post8 == 0 /\ -x_13^post8+x_13^0 == 0), cost: 1 New rule: l6 -> l1 : lt_15^0'=lt_15^0, lt_19^0'=lt_19^post8, nd_12^0'=nd_12^0, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, 0 == 0, cost: 1 propagated equality rv_18^post8 = rv_18^0 propagated equality rt_11^post8 = rt_11^0 propagated equality lt_15^post8 = lt_15^0 propagated equality st_17^post8 = st_17^0 propagated equality y_16^post8 = y_16^0 propagated equality nd_12^post8 = nd_12^0 propagated equality p_14^post8 = p_14^0 propagated equality x_13^post8 = x_13^0 Simplified Guard Original rule: l6 -> l1 : lt_15^0'=lt_15^0, lt_19^0'=lt_19^post8, nd_12^0'=nd_12^0, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, 0 == 0, cost: 1 New rule: l6 -> l1 : lt_15^0'=lt_15^0, lt_19^0'=lt_19^post8, nd_12^0'=nd_12^0, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l1 : lt_15^0'=lt_15^0, lt_19^0'=lt_19^post8, nd_12^0'=nd_12^0, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^0, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, T, cost: 1 New rule: l6 -> l1 : lt_19^0'=lt_19^post8, T, cost: 1 Step with 17 Trace 17[T] Blocked [{}, {}] Step with 13 Trace 17[T], 13[(-lt_15^0+y_16^0 <= 0)] Blocked [{}, {}, {}] Backtrack Trace 17[T] Blocked [{}, {13[T]}] Step with 14 Trace 17[T], 14[(1+lt_15^0-y_16^0 <= 0)] Blocked [{}, {13[T]}, {}] Step with 15 Trace 17[T], 14[(1+lt_15^0-y_16^0 <= 0)], 15[(1-rv_18^0 <= 0)] Blocked [{}, {13[T]}, {}, {}] Step with 19 Trace 17[T], 14[(1+lt_15^0-y_16^0 <= 0)], 15[(1-rv_18^0 <= 0)], 19[T] Blocked [{}, {13[T]}, {}, {}, {}] Nonterm Start location: l7 Program variables: lt_15^0 lt_19^0 nd_12^0 p_14^0 rt_11^0 rv_18^0 st_17^0 x_13^0 y_16^0 13: l1 -> l2 : lt_15^0'=lt_15^post2, rt_11^0'=st_17^0, -lt_15^0+y_16^0 <= 0, cost: 1 14: l1 -> l5 : lt_15^0'=lt_15^post5, nd_12^0'=nd_12^post5, rv_18^0'=nd_12^1, 1+lt_15^0-y_16^0 <= 0, cost: 1 18: l1 -> l1 : lt_15^0'=lt_15^post3, nd_12^0'=nd_12^post3, rv_18^0'=0, 1+lt_15^0-y_16^0 <= 0, cost: 1 20: l1 -> LoAT_sink : (-1+nd_12^11 >= 0 /\ -1-lt_15^0+y_16^0 >= 0 /\ lt_15^post51-lt_15^0 <= 0), cost: NONTERM 15: l5 -> l6 : 1-rv_18^0 <= 0, cost: 1 16: l5 -> l6 : 1+rv_18^0 <= 0, cost: 1 19: l6 -> l1 : lt_19^0'=lt_19^post8, T, cost: 1 17: l7 -> l1 : p_14^0'=x_13^0, T, cost: 1 Certificate of Non-Termination Original rule: l1 -> l1 : lt_15^0'=lt_15^post51, lt_19^0'=lt_19^post8, nd_12^0'=nd_12^post51, rv_18^0'=nd_12^11, (1-nd_12^11 <= 0 /\ 1+lt_15^0-y_16^0 <= 0), cost: 1 New rule: l1 -> LoAT_sink : (-1+nd_12^11 >= 0 /\ -1-lt_15^0+y_16^0 >= 0 /\ lt_15^post51-lt_15^0 <= 0), cost: NONTERM -1+nd_12^11 >= 0 [0]: monotonic increase yields -1+nd_12^11 >= 0 -1-lt_15^0+y_16^0 >= 0 [0]: eventual decrease yields (-1-lt_15^0+y_16^0 >= 0 /\ -1-lt_15^post51+y_16^0 >= 0) -1-lt_15^0+y_16^0 >= 0 [1]: eventual increase yields (-1-lt_15^0+y_16^0 >= 0 /\ lt_15^post51-lt_15^0 <= 0) Replacement map: {-1+nd_12^11 >= 0 -> -1+nd_12^11 >= 0, -1-lt_15^0+y_16^0 >= 0 -> (-1-lt_15^0+y_16^0 >= 0 /\ lt_15^post51-lt_15^0 <= 0)} Step with 20 Trace 17[T], 20[(-1+nd_12^11 >= 0 /\ -1-lt_15^0+y_16^0 >= 0 /\ lt_15^post51-lt_15^0 <= 0)] Blocked [{}, {13[T]}, {20[T]}] Refute Counterexample [ lt_15^0=-1 lt_19^0=0 nd_12^0=0 p_14^0=0 rt_11^0=0 rv_18^0=0 st_17^0=0 x_13^0=0 y_16^0=0 ] 17 [ lt_15^0=-1 lt_19^0=0 nd_12^0=0 p_14^0=p_14^0 rt_11^0=0 rv_18^0=0 st_17^0=0 x_13^0=0 y_16^0=0 ] 20 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b