NO

Initial ITS

Start location: l7
Program variables: __disjvr_0^0 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 : __disjvr_0^0'=__disjvr_0^post1, 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, (-x_13^post1+x_13^0 == 0 /\ -rv_18^post1+rv_18^0 == 0 /\ nd_12^0-nd_12^post1 == 0 /\ p_14^post1-x_13^0 == 0 /\ y_16^0-y_16^post1 == 0 /\ -__disjvr_0^post1+__disjvr_0^0 == 0 /\ -lt_15^post1+lt_15^0 == 0 /\ lt_19^0-lt_19^post1 == 0 /\ rt_11^0-rt_11^post1 == 0 /\ st_17^0-st_17^post1 == 0), cost: 1
   1: l1 -> l2 : __disjvr_0^0'=__disjvr_0^post2, 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 /\ -y_16^post2+y_16^0 == 0 /\ -x_13^post2+x_13^0 == 0 /\ -rv_18^post2+rv_18^0 == 0 /\ y_16^0-lt_15^0 <= 0 /\ -p_14^post2+p_14^0 == 0 /\ nd_12^0-nd_12^post2 == 0 /\ -__disjvr_0^post2+__disjvr_0^0 == 0 /\ lt_19^0-lt_19^post2 == 0 /\ st_17^0-st_17^post2 == 0 /\ -st_17^0+rt_11^post2 == 0), cost: 1
   2: l1 -> l3 : __disjvr_0^0'=__disjvr_0^post3, 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 /\ __disjvr_0^0-__disjvr_0^post3 == 0 /\ p_14^0-p_14^post3 == 0 /\ -rv_18^post3 <= 0 /\ -lt_19^post3+lt_19^0 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -nd_12^1+rv_18^post3 == 0 /\ y_16^0-y_16^post3 == 0 /\ -rt_11^post3+rt_11^0 == 0 /\ rv_18^post3 <= 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ st_17^0-st_17^post3 == 0), cost: 1
   4: l1 -> l5 : __disjvr_0^0'=__disjvr_0^post5, 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 /\ -x_13^post5+x_13^0 == 0 /\ rv_18^post5-nd_12^1 == 0 /\ y_16^0-y_16^post5 == 0 /\ -p_14^post5+p_14^0 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ lt_19^0-lt_19^post5 == 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ rt_11^0-rt_11^post5 == 0 /\ st_17^0-st_17^post5 == 0), cost: 1
   3: l3 -> l1 : __disjvr_0^0'=__disjvr_0^post4, 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, (-st_17^post4+st_17^0 == 0 /\ -p_14^post4+p_14^0 == 0 /\ -rt_11^post4+rt_11^0 == 0 /\ -lt_15^post4+lt_15^0 == 0 /\ nd_12^0-nd_12^post4 == 0 /\ rv_18^0-rv_18^post4 == 0 /\ -x_13^post4+x_13^0 == 0 /\ y_16^0-y_16^post4 == 0 /\ -lt_19^post4+lt_19^0 == 0 /\ __disjvr_0^0-__disjvr_0^post4 == 0), cost: 1
   5: l5 -> l6 : __disjvr_0^0'=__disjvr_0^post6, 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^post6+p_14^0 == 0 /\ -x_13^post6+x_13^0 == 0 /\ st_17^0-st_17^post6 == 0 /\ -lt_15^post6+lt_15^0 == 0 /\ nd_12^0-nd_12^post6 == 0 /\ lt_19^0-lt_19^post6 == 0 /\ -rv_18^post6+rv_18^0 == 0 /\ -rt_11^post6+rt_11^0 == 0 /\ -__disjvr_0^0+__disjvr_0^post6 == 0 /\ y_16^0-y_16^post6 == 0 /\ __disjvr_0^0-__disjvr_0^post6 == 0), cost: 1
   6: l6 -> l4 : __disjvr_0^0'=__disjvr_0^post7, 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, (0 == 0 /\ nd_12^0-nd_12^post7 == 0 /\ rv_18^0-rv_18^post7 == 0 /\ p_14^0-p_14^post7 == 0 /\ __disjvr_0^0-__disjvr_0^post7 == 0 /\ -lt_15^post7+lt_15^0 == 0 /\ st_17^0-st_17^post7 == 0 /\ -rt_11^post7+rt_11^0 == 0 /\ y_16^0-y_16^post7 == 0 /\ -x_13^post7+x_13^0 == 0), cost: 1
   7: l4 -> l1 : __disjvr_0^0'=__disjvr_0^post8, 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, (nd_12^0-nd_12^post8 == 0 /\ __disjvr_0^0-__disjvr_0^post8 == 0 /\ rv_18^0-rv_18^post8 == 0 /\ st_17^0-st_17^post8 == 0 /\ p_14^0-p_14^post8 == 0 /\ -lt_19^post8+lt_19^0 == 0 /\ -lt_15^post8+lt_15^0 == 0 /\ -x_13^post8+x_13^0 == 0 /\ y_16^0-y_16^post8 == 0 /\ -rt_11^post8+rt_11^0 == 0), cost: 1
   8: l7 -> l0 : __disjvr_0^0'=__disjvr_0^post9, 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, (__disjvr_0^0-__disjvr_0^post9 == 0 /\ -rt_11^post9+rt_11^0 == 0 /\ rv_18^0-rv_18^post9 == 0 /\ lt_15^0-lt_15^post9 == 0 /\ -lt_19^post9+lt_19^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ p_14^0-p_14^post9 == 0 /\ y_16^0-y_16^post9 == 0 /\ nd_12^0-nd_12^post9 == 0 /\ st_17^0-st_17^post9 == 0), cost: 1

Chained Linear Paths

Start location: l7
Program variables: __disjvr_0^0 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 : __disjvr_0^0'=__disjvr_0^post2, 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 /\ -y_16^post2+y_16^0 == 0 /\ -x_13^post2+x_13^0 == 0 /\ -rv_18^post2+rv_18^0 == 0 /\ y_16^0-lt_15^0 <= 0 /\ -p_14^post2+p_14^0 == 0 /\ nd_12^0-nd_12^post2 == 0 /\ -__disjvr_0^post2+__disjvr_0^0 == 0 /\ lt_19^0-lt_19^post2 == 0 /\ st_17^0-st_17^post2 == 0 /\ -st_17^0+rt_11^post2 == 0), cost: 1
  10: l1 -> l1 : __disjvr_0^0'=__disjvr_0^post4, 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 /\ __disjvr_0^0-__disjvr_0^post3 == 0 /\ p_14^0-p_14^post3 == 0 /\ nd_12^post3-nd_12^post4 == 0 /\ x_13^post3-x_13^post4 == 0 /\ -rv_18^post3 <= 0 /\ -lt_19^post3+lt_19^0 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -nd_12^1+rv_18^post3 == 0 /\ __disjvr_0^post3-__disjvr_0^post4 == 0 /\ y_16^0-y_16^post3 == 0 /\ -lt_15^post4+lt_15^post3 == 0 /\ rv_18^post3-rv_18^post4 == 0 /\ -p_14^post4+p_14^post3 == 0 /\ lt_19^post3-lt_19^post4 == 0 /\ rt_11^post3-rt_11^post4 == 0 /\ -rt_11^post3+rt_11^0 == 0 /\ rv_18^post3 <= 0 /\ y_16^post3-y_16^post4 == 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ st_17^0-st_17^post3 == 0 /\ -st_17^post4+st_17^post3 == 0), cost: 1
  13: l1 -> l1 : __disjvr_0^0'=__disjvr_0^post8, 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 /\ lt_19^post5-lt_19^post6 == 0 /\ lt_15^post6-lt_15^post7 == 0 /\ nd_12^post5-nd_12^post6 == 0 /\ -x_13^post8+x_13^post7 == 0 /\ -x_13^post5+x_13^0 == 0 /\ __disjvr_0^post6-__disjvr_0^post7 == 0 /\ -nd_12^post8+nd_12^post7 == 0 /\ -rt_11^post8+rt_11^post7 == 0 /\ rt_11^post6-rt_11^post7 == 0 /\ rv_18^post5-rv_18^post6 == 0 /\ rv_18^post5-nd_12^1 == 0 /\ p_14^post5-p_14^post6 == 0 /\ y_16^0-y_16^post5 == 0 /\ -p_14^post5+p_14^0 == 0 /\ -rv_18^post8+rv_18^post7 == 0 /\ lt_15^post5-lt_15^post6 == 0 /\ __disjvr_0^post7-__disjvr_0^post8 == 0 /\ x_13^post5-x_13^post6 == 0 /\ st_17^post6-st_17^post7 == 0 /\ -__disjvr_0^post5+__disjvr_0^post6 == 0 /\ -st_17^post8+st_17^post7 == 0 /\ -lt_15^post8+lt_15^post7 == 0 /\ p_14^post6-p_14^post7 == 0 /\ -rt_11^post6+rt_11^post5 == 0 /\ -p_14^post8+p_14^post7 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ lt_19^0-lt_19^post5 == 0 /\ nd_12^post6-nd_12^post7 == 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ __disjvr_0^post5-__disjvr_0^post6 == 0 /\ rt_11^0-rt_11^post5 == 0 /\ -lt_19^post8+lt_19^post7 == 0 /\ y_16^post5-y_16^post6 == 0 /\ -y_16^post8+y_16^post7 == 0 /\ y_16^post6-y_16^post7 == 0 /\ st_17^0-st_17^post5 == 0 /\ -x_13^post7+x_13^post6 == 0 /\ rv_18^post6-rv_18^post7 == 0 /\ st_17^post5-st_17^post6 == 0), cost: 1
   9: l7 -> l1 : __disjvr_0^0'=__disjvr_0^post1, 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, (__disjvr_0^0-__disjvr_0^post9 == 0 /\ -rt_11^post9+rt_11^0 == 0 /\ rv_18^0-rv_18^post9 == 0 /\ lt_15^0-lt_15^post9 == 0 /\ -lt_19^post9+lt_19^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ p_14^0-p_14^post9 == 0 /\ -st_17^post1+st_17^post9 == 0 /\ y_16^0-y_16^post9 == 0 /\ -rv_18^post1+rv_18^post9 == 0 /\ -__disjvr_0^post1+__disjvr_0^post9 == 0 /\ rt_11^post9-rt_11^post1 == 0 /\ -lt_15^post1+lt_15^post9 == 0 /\ y_16^post9-y_16^post1 == 0 /\ lt_19^post9-lt_19^post1 == 0 /\ x_13^post9-x_13^post1 == 0 /\ -x_13^post9+p_14^post1 == 0 /\ -nd_12^post1+nd_12^post9 == 0 /\ nd_12^0-nd_12^post9 == 0 /\ st_17^0-st_17^post9 == 0), cost: 1

	Eliminating location l0 by chaining:

	Applied chaining

	First rule:
	l7 -> l0 : __disjvr_0^0'=__disjvr_0^post9, 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, (__disjvr_0^0-__disjvr_0^post9 == 0 /\ -rt_11^post9+rt_11^0 == 0 /\ rv_18^0-rv_18^post9 == 0 /\ lt_15^0-lt_15^post9 == 0 /\ -lt_19^post9+lt_19^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ p_14^0-p_14^post9 == 0 /\ y_16^0-y_16^post9 == 0 /\ nd_12^0-nd_12^post9 == 0 /\ st_17^0-st_17^post9 == 0), cost: 1
	Second rule:
	l0 -> l1 : __disjvr_0^0'=__disjvr_0^post1, 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, (-x_13^post1+x_13^0 == 0 /\ -rv_18^post1+rv_18^0 == 0 /\ nd_12^0-nd_12^post1 == 0 /\ p_14^post1-x_13^0 == 0 /\ y_16^0-y_16^post1 == 0 /\ -__disjvr_0^post1+__disjvr_0^0 == 0 /\ -lt_15^post1+lt_15^0 == 0 /\ lt_19^0-lt_19^post1 == 0 /\ rt_11^0-rt_11^post1 == 0 /\ st_17^0-st_17^post1 == 0), cost: 1
	New rule:
	l7 -> l1 : __disjvr_0^0'=__disjvr_0^post1, 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, (__disjvr_0^0-__disjvr_0^post9 == 0 /\ -rt_11^post9+rt_11^0 == 0 /\ rv_18^0-rv_18^post9 == 0 /\ lt_15^0-lt_15^post9 == 0 /\ -lt_19^post9+lt_19^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ p_14^0-p_14^post9 == 0 /\ -st_17^post1+st_17^post9 == 0 /\ y_16^0-y_16^post9 == 0 /\ -rv_18^post1+rv_18^post9 == 0 /\ -__disjvr_0^post1+__disjvr_0^post9 == 0 /\ rt_11^post9-rt_11^post1 == 0 /\ -lt_15^post1+lt_15^post9 == 0 /\ y_16^post9-y_16^post1 == 0 /\ lt_19^post9-lt_19^post1 == 0 /\ x_13^post9-x_13^post1 == 0 /\ -x_13^post9+p_14^post1 == 0 /\ -nd_12^post1+nd_12^post9 == 0 /\ nd_12^0-nd_12^post9 == 0 /\ st_17^0-st_17^post9 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 0 8
	
	Eliminating location l3 by chaining:

	Applied chaining

	First rule:
	l1 -> l3 : __disjvr_0^0'=__disjvr_0^post3, 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 /\ __disjvr_0^0-__disjvr_0^post3 == 0 /\ p_14^0-p_14^post3 == 0 /\ -rv_18^post3 <= 0 /\ -lt_19^post3+lt_19^0 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -nd_12^1+rv_18^post3 == 0 /\ y_16^0-y_16^post3 == 0 /\ -rt_11^post3+rt_11^0 == 0 /\ rv_18^post3 <= 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ st_17^0-st_17^post3 == 0), cost: 1
	Second rule:
	l3 -> l1 : __disjvr_0^0'=__disjvr_0^post4, 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, (-st_17^post4+st_17^0 == 0 /\ -p_14^post4+p_14^0 == 0 /\ -rt_11^post4+rt_11^0 == 0 /\ -lt_15^post4+lt_15^0 == 0 /\ nd_12^0-nd_12^post4 == 0 /\ rv_18^0-rv_18^post4 == 0 /\ -x_13^post4+x_13^0 == 0 /\ y_16^0-y_16^post4 == 0 /\ -lt_19^post4+lt_19^0 == 0 /\ __disjvr_0^0-__disjvr_0^post4 == 0), cost: 1
	New rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^post4, 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 /\ __disjvr_0^0-__disjvr_0^post3 == 0 /\ p_14^0-p_14^post3 == 0 /\ nd_12^post3-nd_12^post4 == 0 /\ x_13^post3-x_13^post4 == 0 /\ -rv_18^post3 <= 0 /\ -lt_19^post3+lt_19^0 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -nd_12^1+rv_18^post3 == 0 /\ __disjvr_0^post3-__disjvr_0^post4 == 0 /\ y_16^0-y_16^post3 == 0 /\ -lt_15^post4+lt_15^post3 == 0 /\ rv_18^post3-rv_18^post4 == 0 /\ -p_14^post4+p_14^post3 == 0 /\ lt_19^post3-lt_19^post4 == 0 /\ rt_11^post3-rt_11^post4 == 0 /\ -rt_11^post3+rt_11^0 == 0 /\ rv_18^post3 <= 0 /\ y_16^post3-y_16^post4 == 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ st_17^0-st_17^post3 == 0 /\ -st_17^post4+st_17^post3 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 2 3
	
	Eliminating location l5 by chaining:

	Applied chaining

	First rule:
	l1 -> l5 : __disjvr_0^0'=__disjvr_0^post5, 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 /\ -x_13^post5+x_13^0 == 0 /\ rv_18^post5-nd_12^1 == 0 /\ y_16^0-y_16^post5 == 0 /\ -p_14^post5+p_14^0 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ lt_19^0-lt_19^post5 == 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ rt_11^0-rt_11^post5 == 0 /\ st_17^0-st_17^post5 == 0), cost: 1
	Second rule:
	l5 -> l6 : __disjvr_0^0'=__disjvr_0^post6, 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^post6+p_14^0 == 0 /\ -x_13^post6+x_13^0 == 0 /\ st_17^0-st_17^post6 == 0 /\ -lt_15^post6+lt_15^0 == 0 /\ nd_12^0-nd_12^post6 == 0 /\ lt_19^0-lt_19^post6 == 0 /\ -rv_18^post6+rv_18^0 == 0 /\ -rt_11^post6+rt_11^0 == 0 /\ -__disjvr_0^0+__disjvr_0^post6 == 0 /\ y_16^0-y_16^post6 == 0 /\ __disjvr_0^0-__disjvr_0^post6 == 0), cost: 1
	New rule:
	l1 -> l6 : __disjvr_0^0'=__disjvr_0^post6, 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, (0 == 0 /\ lt_19^post5-lt_19^post6 == 0 /\ nd_12^post5-nd_12^post6 == 0 /\ -x_13^post5+x_13^0 == 0 /\ rv_18^post5-rv_18^post6 == 0 /\ rv_18^post5-nd_12^1 == 0 /\ p_14^post5-p_14^post6 == 0 /\ y_16^0-y_16^post5 == 0 /\ -p_14^post5+p_14^0 == 0 /\ lt_15^post5-lt_15^post6 == 0 /\ x_13^post5-x_13^post6 == 0 /\ -__disjvr_0^post5+__disjvr_0^post6 == 0 /\ -rt_11^post6+rt_11^post5 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ lt_19^0-lt_19^post5 == 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ __disjvr_0^post5-__disjvr_0^post6 == 0 /\ rt_11^0-rt_11^post5 == 0 /\ y_16^post5-y_16^post6 == 0 /\ st_17^0-st_17^post5 == 0 /\ st_17^post5-st_17^post6 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 4 5
	
	Eliminating location l6 by chaining:

	Applied chaining

	First rule:
	l1 -> l6 : __disjvr_0^0'=__disjvr_0^post6, 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, (0 == 0 /\ lt_19^post5-lt_19^post6 == 0 /\ nd_12^post5-nd_12^post6 == 0 /\ -x_13^post5+x_13^0 == 0 /\ rv_18^post5-rv_18^post6 == 0 /\ rv_18^post5-nd_12^1 == 0 /\ p_14^post5-p_14^post6 == 0 /\ y_16^0-y_16^post5 == 0 /\ -p_14^post5+p_14^0 == 0 /\ lt_15^post5-lt_15^post6 == 0 /\ x_13^post5-x_13^post6 == 0 /\ -__disjvr_0^post5+__disjvr_0^post6 == 0 /\ -rt_11^post6+rt_11^post5 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ lt_19^0-lt_19^post5 == 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ __disjvr_0^post5-__disjvr_0^post6 == 0 /\ rt_11^0-rt_11^post5 == 0 /\ y_16^post5-y_16^post6 == 0 /\ st_17^0-st_17^post5 == 0 /\ st_17^post5-st_17^post6 == 0), cost: 1
	Second rule:
	l6 -> l4 : __disjvr_0^0'=__disjvr_0^post7, 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, (0 == 0 /\ nd_12^0-nd_12^post7 == 0 /\ rv_18^0-rv_18^post7 == 0 /\ p_14^0-p_14^post7 == 0 /\ __disjvr_0^0-__disjvr_0^post7 == 0 /\ -lt_15^post7+lt_15^0 == 0 /\ st_17^0-st_17^post7 == 0 /\ -rt_11^post7+rt_11^0 == 0 /\ y_16^0-y_16^post7 == 0 /\ -x_13^post7+x_13^0 == 0), cost: 1
	New rule:
	l1 -> l4 : __disjvr_0^0'=__disjvr_0^post7, 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, (0 == 0 /\ lt_19^post5-lt_19^post6 == 0 /\ lt_15^post6-lt_15^post7 == 0 /\ nd_12^post5-nd_12^post6 == 0 /\ -x_13^post5+x_13^0 == 0 /\ __disjvr_0^post6-__disjvr_0^post7 == 0 /\ rt_11^post6-rt_11^post7 == 0 /\ rv_18^post5-rv_18^post6 == 0 /\ rv_18^post5-nd_12^1 == 0 /\ p_14^post5-p_14^post6 == 0 /\ y_16^0-y_16^post5 == 0 /\ -p_14^post5+p_14^0 == 0 /\ lt_15^post5-lt_15^post6 == 0 /\ x_13^post5-x_13^post6 == 0 /\ st_17^post6-st_17^post7 == 0 /\ -__disjvr_0^post5+__disjvr_0^post6 == 0 /\ p_14^post6-p_14^post7 == 0 /\ -rt_11^post6+rt_11^post5 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ lt_19^0-lt_19^post5 == 0 /\ nd_12^post6-nd_12^post7 == 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ __disjvr_0^post5-__disjvr_0^post6 == 0 /\ rt_11^0-rt_11^post5 == 0 /\ y_16^post5-y_16^post6 == 0 /\ y_16^post6-y_16^post7 == 0 /\ st_17^0-st_17^post5 == 0 /\ -x_13^post7+x_13^post6 == 0 /\ rv_18^post6-rv_18^post7 == 0 /\ st_17^post5-st_17^post6 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 6 11
	
	Eliminating location l4 by chaining:

	Applied chaining

	First rule:
	l1 -> l4 : __disjvr_0^0'=__disjvr_0^post7, 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, (0 == 0 /\ lt_19^post5-lt_19^post6 == 0 /\ lt_15^post6-lt_15^post7 == 0 /\ nd_12^post5-nd_12^post6 == 0 /\ -x_13^post5+x_13^0 == 0 /\ __disjvr_0^post6-__disjvr_0^post7 == 0 /\ rt_11^post6-rt_11^post7 == 0 /\ rv_18^post5-rv_18^post6 == 0 /\ rv_18^post5-nd_12^1 == 0 /\ p_14^post5-p_14^post6 == 0 /\ y_16^0-y_16^post5 == 0 /\ -p_14^post5+p_14^0 == 0 /\ lt_15^post5-lt_15^post6 == 0 /\ x_13^post5-x_13^post6 == 0 /\ st_17^post6-st_17^post7 == 0 /\ -__disjvr_0^post5+__disjvr_0^post6 == 0 /\ p_14^post6-p_14^post7 == 0 /\ -rt_11^post6+rt_11^post5 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ lt_19^0-lt_19^post5 == 0 /\ nd_12^post6-nd_12^post7 == 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ __disjvr_0^post5-__disjvr_0^post6 == 0 /\ rt_11^0-rt_11^post5 == 0 /\ y_16^post5-y_16^post6 == 0 /\ y_16^post6-y_16^post7 == 0 /\ st_17^0-st_17^post5 == 0 /\ -x_13^post7+x_13^post6 == 0 /\ rv_18^post6-rv_18^post7 == 0 /\ st_17^post5-st_17^post6 == 0), cost: 1
	Second rule:
	l4 -> l1 : __disjvr_0^0'=__disjvr_0^post8, 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, (nd_12^0-nd_12^post8 == 0 /\ __disjvr_0^0-__disjvr_0^post8 == 0 /\ rv_18^0-rv_18^post8 == 0 /\ st_17^0-st_17^post8 == 0 /\ p_14^0-p_14^post8 == 0 /\ -lt_19^post8+lt_19^0 == 0 /\ -lt_15^post8+lt_15^0 == 0 /\ -x_13^post8+x_13^0 == 0 /\ y_16^0-y_16^post8 == 0 /\ -rt_11^post8+rt_11^0 == 0), cost: 1
	New rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^post8, 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 /\ lt_19^post5-lt_19^post6 == 0 /\ lt_15^post6-lt_15^post7 == 0 /\ nd_12^post5-nd_12^post6 == 0 /\ -x_13^post8+x_13^post7 == 0 /\ -x_13^post5+x_13^0 == 0 /\ __disjvr_0^post6-__disjvr_0^post7 == 0 /\ -nd_12^post8+nd_12^post7 == 0 /\ -rt_11^post8+rt_11^post7 == 0 /\ rt_11^post6-rt_11^post7 == 0 /\ rv_18^post5-rv_18^post6 == 0 /\ rv_18^post5-nd_12^1 == 0 /\ p_14^post5-p_14^post6 == 0 /\ y_16^0-y_16^post5 == 0 /\ -p_14^post5+p_14^0 == 0 /\ -rv_18^post8+rv_18^post7 == 0 /\ lt_15^post5-lt_15^post6 == 0 /\ __disjvr_0^post7-__disjvr_0^post8 == 0 /\ x_13^post5-x_13^post6 == 0 /\ st_17^post6-st_17^post7 == 0 /\ -__disjvr_0^post5+__disjvr_0^post6 == 0 /\ -st_17^post8+st_17^post7 == 0 /\ -lt_15^post8+lt_15^post7 == 0 /\ p_14^post6-p_14^post7 == 0 /\ -rt_11^post6+rt_11^post5 == 0 /\ -p_14^post8+p_14^post7 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ lt_19^0-lt_19^post5 == 0 /\ nd_12^post6-nd_12^post7 == 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ __disjvr_0^post5-__disjvr_0^post6 == 0 /\ rt_11^0-rt_11^post5 == 0 /\ -lt_19^post8+lt_19^post7 == 0 /\ y_16^post5-y_16^post6 == 0 /\ -y_16^post8+y_16^post7 == 0 /\ y_16^post6-y_16^post7 == 0 /\ st_17^0-st_17^post5 == 0 /\ -x_13^post7+x_13^post6 == 0 /\ rv_18^post6-rv_18^post7 == 0 /\ st_17^post5-st_17^post6 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 7 12

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
  14: l1 -> l2 : lt_15^0'=lt_15^post2, rt_11^0'=st_17^0, y_16^0-lt_15^0 <= 0, cost: 1
  16: l1 -> l1 : lt_15^0'=lt_15^post3, nd_12^0'=nd_12^post3, rv_18^0'=0, 1-y_16^0+lt_15^0 <= 0, cost: 1
  17: l1 -> l1 : lt_15^0'=lt_15^post7, lt_19^0'=lt_19^post7, nd_12^0'=nd_12^post7, rv_18^0'=rv_18^post7, 1-y_16^0+lt_15^0 <= 0, cost: 1
  15: l7 -> l1 : p_14^0'=x_13^0, T, cost: 1

	Propagated Equalities

	Original rule:
	l1 -> l2 : __disjvr_0^0'=__disjvr_0^post2, 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 /\ -y_16^post2+y_16^0 == 0 /\ -x_13^post2+x_13^0 == 0 /\ -rv_18^post2+rv_18^0 == 0 /\ y_16^0-lt_15^0 <= 0 /\ -p_14^post2+p_14^0 == 0 /\ nd_12^0-nd_12^post2 == 0 /\ -__disjvr_0^post2+__disjvr_0^0 == 0 /\ lt_19^0-lt_19^post2 == 0 /\ st_17^0-st_17^post2 == 0 /\ -st_17^0+rt_11^post2 == 0), cost: 1
	New rule:
	l1 -> l2 : __disjvr_0^0'=__disjvr_0^0, 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 /\ y_16^0-lt_15^0 <= 0), cost: 1
	
		propagated equality y_16^post2 = y_16^0
		
		propagated equality x_13^post2 = x_13^0
		
		propagated equality rv_18^post2 = rv_18^0
		
		propagated equality p_14^post2 = p_14^0
		
		propagated equality nd_12^post2 = nd_12^0
		
		propagated equality __disjvr_0^post2 = __disjvr_0^0
		
		propagated equality lt_19^post2 = lt_19^0
		
		propagated equality st_17^post2 = st_17^0
		
		propagated equality rt_11^post2 = st_17^0
		
	Simplified Guard

	Original rule:
	l1 -> l2 : __disjvr_0^0'=__disjvr_0^0, 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 /\ y_16^0-lt_15^0 <= 0), cost: 1
	New rule:
	l1 -> l2 : __disjvr_0^0'=__disjvr_0^0, 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, y_16^0-lt_15^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l2 : __disjvr_0^0'=__disjvr_0^0, 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, y_16^0-lt_15^0 <= 0, cost: 1
	New rule:
	l1 -> l2 : lt_15^0'=lt_15^post2, rt_11^0'=st_17^0, y_16^0-lt_15^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l1 : __disjvr_0^0'=__disjvr_0^post1, 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, (__disjvr_0^0-__disjvr_0^post9 == 0 /\ -rt_11^post9+rt_11^0 == 0 /\ rv_18^0-rv_18^post9 == 0 /\ lt_15^0-lt_15^post9 == 0 /\ -lt_19^post9+lt_19^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ p_14^0-p_14^post9 == 0 /\ -st_17^post1+st_17^post9 == 0 /\ y_16^0-y_16^post9 == 0 /\ -rv_18^post1+rv_18^post9 == 0 /\ -__disjvr_0^post1+__disjvr_0^post9 == 0 /\ rt_11^post9-rt_11^post1 == 0 /\ -lt_15^post1+lt_15^post9 == 0 /\ y_16^post9-y_16^post1 == 0 /\ lt_19^post9-lt_19^post1 == 0 /\ x_13^post9-x_13^post1 == 0 /\ -x_13^post9+p_14^post1 == 0 /\ -nd_12^post1+nd_12^post9 == 0 /\ nd_12^0-nd_12^post9 == 0 /\ st_17^0-st_17^post9 == 0), cost: 1
	New rule:
	l7 -> l1 : __disjvr_0^0'=__disjvr_0^post9, lt_15^0'=lt_15^post9, lt_19^0'=lt_19^post9, nd_12^0'=nd_12^post9, p_14^0'=x_13^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 /\ __disjvr_0^0-__disjvr_0^post9 == 0 /\ -rt_11^post9+rt_11^0 == 0 /\ rv_18^0-rv_18^post9 == 0 /\ lt_15^0-lt_15^post9 == 0 /\ -lt_19^post9+lt_19^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ p_14^0-p_14^post9 == 0 /\ y_16^0-y_16^post9 == 0 /\ nd_12^0-nd_12^post9 == 0 /\ st_17^0-st_17^post9 == 0), cost: 1
	
		propagated equality st_17^post1 = st_17^post9
		
		propagated equality rv_18^post1 = rv_18^post9
		
		propagated equality __disjvr_0^post1 = __disjvr_0^post9
		
		propagated equality rt_11^post1 = rt_11^post9
		
		propagated equality lt_15^post1 = lt_15^post9
		
		propagated equality y_16^post1 = y_16^post9
		
		propagated equality lt_19^post1 = lt_19^post9
		
		propagated equality x_13^post1 = x_13^post9
		
		propagated equality p_14^post1 = x_13^post9
		
		propagated equality nd_12^post1 = nd_12^post9
		
	Propagated Equalities

	Original rule:
	l7 -> l1 : __disjvr_0^0'=__disjvr_0^post9, lt_15^0'=lt_15^post9, lt_19^0'=lt_19^post9, nd_12^0'=nd_12^post9, p_14^0'=x_13^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 /\ __disjvr_0^0-__disjvr_0^post9 == 0 /\ -rt_11^post9+rt_11^0 == 0 /\ rv_18^0-rv_18^post9 == 0 /\ lt_15^0-lt_15^post9 == 0 /\ -lt_19^post9+lt_19^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ p_14^0-p_14^post9 == 0 /\ y_16^0-y_16^post9 == 0 /\ nd_12^0-nd_12^post9 == 0 /\ st_17^0-st_17^post9 == 0), cost: 1
	New rule:
	l7 -> l1 : __disjvr_0^0'=__disjvr_0^0, 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 __disjvr_0^post9 = __disjvr_0^0
		
		propagated equality rt_11^post9 = rt_11^0
		
		propagated equality rv_18^post9 = rv_18^0
		
		propagated equality lt_15^post9 = lt_15^0
		
		propagated equality lt_19^post9 = lt_19^0
		
		propagated equality x_13^post9 = x_13^0
		
		propagated equality p_14^post9 = p_14^0
		
		propagated equality y_16^post9 = y_16^0
		
		propagated equality nd_12^post9 = nd_12^0
		
		propagated equality st_17^post9 = st_17^0
		
	Simplified Guard

	Original rule:
	l7 -> l1 : __disjvr_0^0'=__disjvr_0^0, 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 : __disjvr_0^0'=__disjvr_0^0, 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 : __disjvr_0^0'=__disjvr_0^0, 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 : __disjvr_0^0'=__disjvr_0^post4, 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 /\ __disjvr_0^0-__disjvr_0^post3 == 0 /\ p_14^0-p_14^post3 == 0 /\ nd_12^post3-nd_12^post4 == 0 /\ x_13^post3-x_13^post4 == 0 /\ -rv_18^post3 <= 0 /\ -lt_19^post3+lt_19^0 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -nd_12^1+rv_18^post3 == 0 /\ __disjvr_0^post3-__disjvr_0^post4 == 0 /\ y_16^0-y_16^post3 == 0 /\ -lt_15^post4+lt_15^post3 == 0 /\ rv_18^post3-rv_18^post4 == 0 /\ -p_14^post4+p_14^post3 == 0 /\ lt_19^post3-lt_19^post4 == 0 /\ rt_11^post3-rt_11^post4 == 0 /\ -rt_11^post3+rt_11^0 == 0 /\ rv_18^post3 <= 0 /\ y_16^post3-y_16^post4 == 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ st_17^0-st_17^post3 == 0 /\ -st_17^post4+st_17^post3 == 0), cost: 1
	New rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^post4, 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 /\ __disjvr_0^0-__disjvr_0^post3 == 0 /\ p_14^0-p_14^post3 == 0 /\ nd_12^post3-nd_12^post4 == 0 /\ x_13^post3-x_13^post4 == 0 /\ -rv_18^post3 <= 0 /\ -rv_18^post3 == 0 /\ -lt_19^post3+lt_19^0 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -nd_12^1+rv_18^post3 == 0 /\ __disjvr_0^post3-__disjvr_0^post4 == 0 /\ y_16^0-y_16^post3 == 0 /\ -lt_15^post4+lt_15^post3 == 0 /\ rv_18^post3-rv_18^post4 == 0 /\ -p_14^post4+p_14^post3 == 0 /\ lt_19^post3-lt_19^post4 == 0 /\ rt_11^post3-rt_11^post4 == 0 /\ -rt_11^post3+rt_11^0 == 0 /\ rv_18^post3 <= 0 /\ y_16^post3-y_16^post4 == 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ st_17^0-st_17^post3 == 0 /\ -st_17^post4+st_17^post3 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^post4, 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 /\ __disjvr_0^0-__disjvr_0^post3 == 0 /\ p_14^0-p_14^post3 == 0 /\ nd_12^post3-nd_12^post4 == 0 /\ x_13^post3-x_13^post4 == 0 /\ -rv_18^post3 <= 0 /\ -rv_18^post3 == 0 /\ -lt_19^post3+lt_19^0 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -nd_12^1+rv_18^post3 == 0 /\ __disjvr_0^post3-__disjvr_0^post4 == 0 /\ y_16^0-y_16^post3 == 0 /\ -lt_15^post4+lt_15^post3 == 0 /\ rv_18^post3-rv_18^post4 == 0 /\ -p_14^post4+p_14^post3 == 0 /\ lt_19^post3-lt_19^post4 == 0 /\ rt_11^post3-rt_11^post4 == 0 /\ -rt_11^post3+rt_11^0 == 0 /\ rv_18^post3 <= 0 /\ y_16^post3-y_16^post4 == 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ st_17^0-st_17^post3 == 0 /\ -st_17^post4+st_17^post3 == 0), cost: 1
	New rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^post3, 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 /\ __disjvr_0^0-__disjvr_0^post3 == 0 /\ p_14^0-p_14^post3 == 0 /\ -rv_18^post3 <= 0 /\ -rv_18^post3 == 0 /\ -lt_19^post3+lt_19^0 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -nd_12^1+rv_18^post3 == 0 /\ y_16^0-y_16^post3 == 0 /\ -rt_11^post3+rt_11^0 == 0 /\ rv_18^post3 <= 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ st_17^0-st_17^post3 == 0), cost: 1
	
		propagated equality nd_12^post4 = nd_12^post3
		
		propagated equality x_13^post4 = x_13^post3
		
		propagated equality __disjvr_0^post4 = __disjvr_0^post3
		
		propagated equality lt_15^post4 = lt_15^post3
		
		propagated equality rv_18^post4 = rv_18^post3
		
		propagated equality p_14^post4 = p_14^post3
		
		propagated equality lt_19^post4 = lt_19^post3
		
		propagated equality rt_11^post4 = rt_11^post3
		
		propagated equality y_16^post4 = y_16^post3
		
		propagated equality st_17^post4 = st_17^post3
		
	Propagated Equalities

	Original rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^post3, 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 /\ __disjvr_0^0-__disjvr_0^post3 == 0 /\ p_14^0-p_14^post3 == 0 /\ -rv_18^post3 <= 0 /\ -rv_18^post3 == 0 /\ -lt_19^post3+lt_19^0 == 0 /\ -x_13^post3+x_13^0 == 0 /\ -nd_12^1+rv_18^post3 == 0 /\ y_16^0-y_16^post3 == 0 /\ -rt_11^post3+rt_11^0 == 0 /\ rv_18^post3 <= 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ st_17^0-st_17^post3 == 0), cost: 1
	New rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^0, 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-y_16^0+lt_15^0 <= 0), cost: 1
	
		propagated equality __disjvr_0^post3 = __disjvr_0^0
		
		propagated equality p_14^post3 = p_14^0
		
		propagated equality rv_18^post3 = 0
		
		propagated equality lt_19^post3 = lt_19^0
		
		propagated equality x_13^post3 = x_13^0
		
		propagated equality nd_12^1 = 0
		
		propagated equality y_16^post3 = y_16^0
		
		propagated equality rt_11^post3 = rt_11^0
		
		propagated equality st_17^post3 = st_17^0
		
	Simplified Guard

	Original rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^0, 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-y_16^0+lt_15^0 <= 0), cost: 1
	New rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^0, 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-y_16^0+lt_15^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^0, 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-y_16^0+lt_15^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-y_16^0+lt_15^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^post8, 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 /\ lt_19^post5-lt_19^post6 == 0 /\ lt_15^post6-lt_15^post7 == 0 /\ nd_12^post5-nd_12^post6 == 0 /\ -x_13^post8+x_13^post7 == 0 /\ -x_13^post5+x_13^0 == 0 /\ __disjvr_0^post6-__disjvr_0^post7 == 0 /\ -nd_12^post8+nd_12^post7 == 0 /\ -rt_11^post8+rt_11^post7 == 0 /\ rt_11^post6-rt_11^post7 == 0 /\ rv_18^post5-rv_18^post6 == 0 /\ rv_18^post5-nd_12^1 == 0 /\ p_14^post5-p_14^post6 == 0 /\ y_16^0-y_16^post5 == 0 /\ -p_14^post5+p_14^0 == 0 /\ -rv_18^post8+rv_18^post7 == 0 /\ lt_15^post5-lt_15^post6 == 0 /\ __disjvr_0^post7-__disjvr_0^post8 == 0 /\ x_13^post5-x_13^post6 == 0 /\ st_17^post6-st_17^post7 == 0 /\ -__disjvr_0^post5+__disjvr_0^post6 == 0 /\ -st_17^post8+st_17^post7 == 0 /\ -lt_15^post8+lt_15^post7 == 0 /\ p_14^post6-p_14^post7 == 0 /\ -rt_11^post6+rt_11^post5 == 0 /\ -p_14^post8+p_14^post7 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ lt_19^0-lt_19^post5 == 0 /\ nd_12^post6-nd_12^post7 == 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ __disjvr_0^post5-__disjvr_0^post6 == 0 /\ rt_11^0-rt_11^post5 == 0 /\ -lt_19^post8+lt_19^post7 == 0 /\ y_16^post5-y_16^post6 == 0 /\ -y_16^post8+y_16^post7 == 0 /\ y_16^post6-y_16^post7 == 0 /\ st_17^0-st_17^post5 == 0 /\ -x_13^post7+x_13^post6 == 0 /\ rv_18^post6-rv_18^post7 == 0 /\ st_17^post5-st_17^post6 == 0), cost: 1
	New rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^post7, 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, (0 == 0 /\ lt_19^post5-lt_19^post6 == 0 /\ lt_15^post6-lt_15^post7 == 0 /\ nd_12^post5-nd_12^post6 == 0 /\ -x_13^post5+x_13^0 == 0 /\ __disjvr_0^post6-__disjvr_0^post7 == 0 /\ rt_11^post6-rt_11^post7 == 0 /\ rv_18^post5-rv_18^post6 == 0 /\ rv_18^post5-nd_12^1 == 0 /\ p_14^post5-p_14^post6 == 0 /\ y_16^0-y_16^post5 == 0 /\ -p_14^post5+p_14^0 == 0 /\ lt_15^post5-lt_15^post6 == 0 /\ x_13^post5-x_13^post6 == 0 /\ st_17^post6-st_17^post7 == 0 /\ -__disjvr_0^post5+__disjvr_0^post6 == 0 /\ p_14^post6-p_14^post7 == 0 /\ -rt_11^post6+rt_11^post5 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ lt_19^0-lt_19^post5 == 0 /\ nd_12^post6-nd_12^post7 == 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ __disjvr_0^post5-__disjvr_0^post6 == 0 /\ rt_11^0-rt_11^post5 == 0 /\ y_16^post5-y_16^post6 == 0 /\ y_16^post6-y_16^post7 == 0 /\ st_17^0-st_17^post5 == 0 /\ -x_13^post7+x_13^post6 == 0 /\ rv_18^post6-rv_18^post7 == 0 /\ st_17^post5-st_17^post6 == 0), cost: 1
	
		propagated equality x_13^post8 = x_13^post7
		
		propagated equality nd_12^post8 = nd_12^post7
		
		propagated equality rt_11^post8 = rt_11^post7
		
		propagated equality rv_18^post8 = rv_18^post7
		
		propagated equality __disjvr_0^post8 = __disjvr_0^post7
		
		propagated equality st_17^post8 = st_17^post7
		
		propagated equality lt_15^post8 = lt_15^post7
		
		propagated equality p_14^post8 = p_14^post7
		
		propagated equality lt_19^post8 = lt_19^post7
		
		propagated equality y_16^post8 = y_16^post7
		
	Propagated Equalities

	Original rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^post7, 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, (0 == 0 /\ lt_19^post5-lt_19^post6 == 0 /\ lt_15^post6-lt_15^post7 == 0 /\ nd_12^post5-nd_12^post6 == 0 /\ -x_13^post5+x_13^0 == 0 /\ __disjvr_0^post6-__disjvr_0^post7 == 0 /\ rt_11^post6-rt_11^post7 == 0 /\ rv_18^post5-rv_18^post6 == 0 /\ rv_18^post5-nd_12^1 == 0 /\ p_14^post5-p_14^post6 == 0 /\ y_16^0-y_16^post5 == 0 /\ -p_14^post5+p_14^0 == 0 /\ lt_15^post5-lt_15^post6 == 0 /\ x_13^post5-x_13^post6 == 0 /\ st_17^post6-st_17^post7 == 0 /\ -__disjvr_0^post5+__disjvr_0^post6 == 0 /\ p_14^post6-p_14^post7 == 0 /\ -rt_11^post6+rt_11^post5 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ lt_19^0-lt_19^post5 == 0 /\ nd_12^post6-nd_12^post7 == 0 /\ 1-y_16^0+lt_15^0 <= 0 /\ __disjvr_0^post5-__disjvr_0^post6 == 0 /\ rt_11^0-rt_11^post5 == 0 /\ y_16^post5-y_16^post6 == 0 /\ y_16^post6-y_16^post7 == 0 /\ st_17^0-st_17^post5 == 0 /\ -x_13^post7+x_13^post6 == 0 /\ rv_18^post6-rv_18^post7 == 0 /\ st_17^post5-st_17^post6 == 0), cost: 1
	New rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^0, lt_15^0'=lt_15^post7, lt_19^0'=lt_19^post7, nd_12^0'=nd_12^post7, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^post7, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, (0 == 0 /\ 1-y_16^0+lt_15^0 <= 0), cost: 1
	
		propagated equality lt_19^post5 = lt_19^post6
		
		propagated equality lt_15^post6 = lt_15^post7
		
		propagated equality nd_12^post5 = nd_12^post6
		
		propagated equality x_13^post5 = x_13^0
		
		propagated equality __disjvr_0^post6 = __disjvr_0^post7
		
		propagated equality rt_11^post6 = rt_11^post7
		
		propagated equality rv_18^post5 = rv_18^post6
		
		propagated equality nd_12^1 = rv_18^post6
		
		propagated equality p_14^post5 = p_14^post6
		
		propagated equality y_16^post5 = y_16^0
		
		propagated equality p_14^post6 = p_14^0
		
		propagated equality lt_15^post5 = lt_15^post7
		
		propagated equality x_13^post6 = x_13^0
		
		propagated equality st_17^post6 = st_17^post7
		
		propagated equality __disjvr_0^post5 = __disjvr_0^post7
		
		propagated equality p_14^post7 = p_14^0
		
		propagated equality rt_11^post5 = rt_11^post7
		
		propagated equality __disjvr_0^post7 = __disjvr_0^0
		
		propagated equality lt_19^post6 = lt_19^0
		
		propagated equality nd_12^post6 = nd_12^post7
		
		propagated equality rt_11^post7 = rt_11^0
		
		propagated equality y_16^post6 = y_16^0
		
		propagated equality y_16^post7 = y_16^0
		
		propagated equality st_17^post5 = st_17^0
		
		propagated equality x_13^post7 = x_13^0
		
		propagated equality rv_18^post6 = rv_18^post7
		
		propagated equality st_17^post7 = st_17^0
		
	Simplified Guard

	Original rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^0, lt_15^0'=lt_15^post7, lt_19^0'=lt_19^post7, nd_12^0'=nd_12^post7, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^post7, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, (0 == 0 /\ 1-y_16^0+lt_15^0 <= 0), cost: 1
	New rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^0, lt_15^0'=lt_15^post7, lt_19^0'=lt_19^post7, nd_12^0'=nd_12^post7, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^post7, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, 1-y_16^0+lt_15^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l1 : __disjvr_0^0'=__disjvr_0^0, lt_15^0'=lt_15^post7, lt_19^0'=lt_19^post7, nd_12^0'=nd_12^post7, p_14^0'=p_14^0, rt_11^0'=rt_11^0, rv_18^0'=rv_18^post7, st_17^0'=st_17^0, x_13^0'=x_13^0, y_16^0'=y_16^0, 1-y_16^0+lt_15^0 <= 0, cost: 1
	New rule:
	l1 -> l1 : lt_15^0'=lt_15^post7, lt_19^0'=lt_19^post7, nd_12^0'=nd_12^post7, rv_18^0'=rv_18^post7, 1-y_16^0+lt_15^0 <= 0, cost: 1

Step with 15

	Trace

	15[T]
	
	Blocked

	[{}, {}]

Step with 14

	Trace

	15[T], 14[(y_16^0-lt_15^0 <= 0)]
	
	Blocked

	[{}, {}, {}]

Backtrack

	Trace

	15[T]
	
	Blocked

	[{}, {14[T]}]

Step with 16

	Trace

	15[T], 16[(1-y_16^0+lt_15^0 <= 0)]
	
	Blocked

	[{}, {14[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
  14: l1 -> l2 : lt_15^0'=lt_15^post2, rt_11^0'=st_17^0, y_16^0-lt_15^0 <= 0, cost: 1
  16: l1 -> l1 : lt_15^0'=lt_15^post3, nd_12^0'=nd_12^post3, rv_18^0'=0, 1-y_16^0+lt_15^0 <= 0, cost: 1
  17: l1 -> l1 : lt_15^0'=lt_15^post7, lt_19^0'=lt_19^post7, nd_12^0'=nd_12^post7, rv_18^0'=rv_18^post7, 1-y_16^0+lt_15^0 <= 0, cost: 1
  18: l1 -> LoAT_sink : (-1+y_16^0-lt_15^0 >= 0 /\ -lt_15^0+lt_15^post3 <= 0), cost: NONTERM
  15: l7 -> l1 : p_14^0'=x_13^0, T, cost: 1

	Certificate of Non-Termination

	Original rule:
	l1 -> l1 : lt_15^0'=lt_15^post3, nd_12^0'=nd_12^post3, rv_18^0'=0, (1-y_16^0+lt_15^0 <= 0), cost: 1
	New rule:
	l1 -> LoAT_sink : (-1+y_16^0-lt_15^0 >= 0 /\ -lt_15^0+lt_15^post3 <= 0), cost: NONTERM

		-1+y_16^0-lt_15^0 >= 0 [0]: eventual decrease yields (-1+y_16^0-lt_15^0 >= 0 /\ -1+y_16^0-lt_15^post3 >= 0)
		
		-1+y_16^0-lt_15^0 >= 0 [1]: eventual increase yields (-1+y_16^0-lt_15^0 >= 0 /\ -lt_15^0+lt_15^post3 <= 0)
		
		Replacement map: {-1+y_16^0-lt_15^0 >= 0 -> (-1+y_16^0-lt_15^0 >= 0 /\ -lt_15^0+lt_15^post3 <= 0)}

Step with 18

	Trace

	15[T], 18[(-1+y_16^0-lt_15^0 >= 0 /\ -lt_15^0+lt_15^post3 <= 0)]
	
	Blocked

	[{}, {14[T]}, {18[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 ] 15 [ 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 ] 18
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b