NO

Initial ITS

Start location: l14
Program variables: __disjvr_0^0 __disjvr_1^0 __disjvr_2^0 result_4^0 tmp_8^0 x_5^0 y_6^0 z_7^0
   0: l0 -> l1 : __disjvr_0^0'=__disjvr_0^post1, __disjvr_1^0'=__disjvr_1^post1, __disjvr_2^0'=__disjvr_2^post1, result_4^0'=result_4^post1, tmp_8^0'=tmp_8^post1, x_5^0'=x_5^post1, y_6^0'=y_6^post1, z_7^0'=z_7^post1, (result_4^0-result_4^post1 == 0 /\ y_6^0-y_6^post1 == 0 /\ __disjvr_2^0-__disjvr_2^post1 == 0 /\ z_7^0-z_7^post1 == 0 /\ tmp_8^0-tmp_8^post1 == 0 /\ -__disjvr_0^post1+__disjvr_0^0 == 0 /\ -__disjvr_1^post1+__disjvr_1^0 == 0 /\ -x_5^post1+x_5^0 == 0), cost: 1
   7: l1 -> l7 : __disjvr_0^0'=__disjvr_0^post8, __disjvr_1^0'=__disjvr_1^post8, __disjvr_2^0'=__disjvr_2^post8, result_4^0'=result_4^post8, tmp_8^0'=tmp_8^post8, x_5^0'=x_5^post8, y_6^0'=y_6^post8, z_7^0'=z_7^post8, (-__disjvr_2^post8+__disjvr_2^0 == 0 /\ __disjvr_0^0-__disjvr_0^post8 == 0 /\ -result_4^post8+result_4^0 == 0 /\ 1-y_6^0+x_5^0 <= 0 /\ __disjvr_1^0-__disjvr_1^post8 == 0 /\ -tmp_8^post8+tmp_8^0 == 0 /\ y_6^0-y_6^post8 == 0 /\ z_7^0-z_7^post8 == 0 /\ -x_5^post8+x_5^0 == 0), cost: 1
   8: l1 -> l8 : __disjvr_0^0'=__disjvr_0^post9, __disjvr_1^0'=__disjvr_1^post9, __disjvr_2^0'=__disjvr_2^post9, result_4^0'=result_4^post9, tmp_8^0'=tmp_8^post9, x_5^0'=x_5^post9, y_6^0'=y_6^post9, z_7^0'=z_7^post9, (0 == 0 /\ tmp_8^0-tmp_8^post9 == 0 /\ y_6^0-x_5^0 <= 0 /\ -y_6^post9+y_6^0 == 0 /\ -__disjvr_1^post9+__disjvr_1^0 == 0 /\ -__disjvr_0^post9+__disjvr_0^0 == 0 /\ __disjvr_2^0-__disjvr_2^post9 == 0 /\ z_7^0-z_7^post9 == 0 /\ x_5^0-x_5^post9 == 0), cost: 1
   1: l2 -> l3 : __disjvr_0^0'=__disjvr_0^post2, __disjvr_1^0'=__disjvr_1^post2, __disjvr_2^0'=__disjvr_2^post2, result_4^0'=result_4^post2, tmp_8^0'=tmp_8^post2, x_5^0'=x_5^post2, y_6^0'=y_6^post2, z_7^0'=z_7^post2, (0 == 0 /\ z_7^0-z_7^post2 == 0 /\ __disjvr_0^0-__disjvr_0^post2 == 0 /\ -tmp_8^post2 <= 0 /\ x_5^0-x_5^post2 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ tmp_8^post2 <= 0 /\ -__disjvr_2^post2+__disjvr_2^0 == 0 /\ -__disjvr_1^post2+__disjvr_1^0 == 0 /\ -result_4^post2+result_4^0 == 0 /\ -y_6^post2+y_6^0 == 0), cost: 1
   2: l2 -> l5 : __disjvr_0^0'=__disjvr_0^post3, __disjvr_1^0'=__disjvr_1^post3, __disjvr_2^0'=__disjvr_2^post3, result_4^0'=result_4^post3, tmp_8^0'=tmp_8^post3, x_5^0'=x_5^post3, y_6^0'=y_6^post3, z_7^0'=z_7^post3, (0 == 0 /\ -x_5^post3+x_5^0 == 0 /\ -z_7^post3+z_7^0 == 0 /\ -__disjvr_1^post3+__disjvr_1^0 == 0 /\ result_4^0-result_4^post3 == 0 /\ y_6^0-y_6^post3 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -__disjvr_2^post3+__disjvr_2^0 == 0 /\ __disjvr_0^0-__disjvr_0^post3 == 0), cost: 1
   6: l2 -> l1 : __disjvr_0^0'=__disjvr_0^post7, __disjvr_1^0'=__disjvr_1^post7, __disjvr_2^0'=__disjvr_2^post7, result_4^0'=result_4^post7, tmp_8^0'=tmp_8^post7, x_5^0'=x_5^post7, y_6^0'=y_6^post7, z_7^0'=z_7^post7, (tmp_8^0-tmp_8^post7 == 0 /\ -__disjvr_0^post7+__disjvr_0^0 == 0 /\ z_7^0-z_7^post7 == 0 /\ -1+x_5^post7-x_5^0 == 0 /\ z_7^0-y_6^0 <= 0 /\ __disjvr_2^0-__disjvr_2^post7 == 0 /\ -y_6^post7+y_6^0 == 0 /\ -result_4^post7+result_4^0 == 0 /\ -__disjvr_1^post7+__disjvr_1^0 == 0), cost: 1
  14: l3 -> l11 : __disjvr_0^0'=__disjvr_0^post15, __disjvr_1^0'=__disjvr_1^post15, __disjvr_2^0'=__disjvr_2^post15, result_4^0'=result_4^post15, tmp_8^0'=tmp_8^post15, x_5^0'=x_5^post15, y_6^0'=y_6^post15, z_7^0'=z_7^post15, (0 == 0 /\ -__disjvr_2^post15+__disjvr_2^0 == 0 /\ -__disjvr_1^post15+__disjvr_1^0 == 0 /\ -result_4^post15+result_4^0 == 0 /\ z_7^0-z_7^post15 == 0 /\ -tmp_8^post15 <= 0 /\ __disjvr_0^0-__disjvr_0^post15 == 0 /\ x_5^0-x_5^post15 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ tmp_8^post15 <= 0 /\ -y_6^post15+y_6^0 == 0), cost: 1
  16: l3 -> l12 : __disjvr_0^0'=__disjvr_0^post17, __disjvr_1^0'=__disjvr_1^post17, __disjvr_2^0'=__disjvr_2^post17, result_4^0'=result_4^post17, tmp_8^0'=tmp_8^post17, x_5^0'=x_5^post17, y_6^0'=y_6^post17, z_7^0'=z_7^post17, (0 == 0 /\ z_7^0-z_7^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -x_5^post17+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ -y_6^post17+y_6^0 == 0 /\ -result_4^post17+result_4^0 == 0 /\ -__disjvr_1^post17+__disjvr_1^0 == 0), cost: 1
   3: l5 -> l6 : __disjvr_0^0'=__disjvr_0^post4, __disjvr_1^0'=__disjvr_1^post4, __disjvr_2^0'=__disjvr_2^post4, result_4^0'=result_4^post4, tmp_8^0'=tmp_8^post4, x_5^0'=x_5^post4, y_6^0'=y_6^post4, z_7^0'=z_7^post4, (z_7^0-z_7^post4 == 0 /\ -result_4^post4+result_4^0 == 0 /\ -__disjvr_1^post4+__disjvr_1^0 == 0 /\ x_5^0-x_5^post4 == 0 /\ tmp_8^0-tmp_8^post4 == 0 /\ __disjvr_2^0-__disjvr_2^post4 == 0 /\ -__disjvr_0^0+__disjvr_0^post4 == 0 /\ -y_6^post4+y_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post4 == 0), cost: 1
   4: l6 -> l4 : __disjvr_0^0'=__disjvr_0^post5, __disjvr_1^0'=__disjvr_1^post5, __disjvr_2^0'=__disjvr_2^post5, result_4^0'=result_4^post5, tmp_8^0'=tmp_8^post5, x_5^0'=x_5^post5, y_6^0'=y_6^post5, z_7^0'=z_7^post5, (-__disjvr_1^post5+__disjvr_1^0 == 0 /\ -x_5^post5+x_5^0 == 0 /\ -z_7^post5+z_7^0 == 0 /\ __disjvr_2^0-__disjvr_2^post5 == 0 /\ result_4^0-result_4^post5 == 0 /\ __disjvr_0^0-__disjvr_0^post5 == 0 /\ tmp_8^0-tmp_8^post5 == 0 /\ -1-y_6^0+y_6^post5 == 0), cost: 1
   5: l4 -> l2 : __disjvr_0^0'=__disjvr_0^post6, __disjvr_1^0'=__disjvr_1^post6, __disjvr_2^0'=__disjvr_2^post6, result_4^0'=result_4^post6, tmp_8^0'=tmp_8^post6, x_5^0'=x_5^post6, y_6^0'=y_6^post6, z_7^0'=z_7^post6, (tmp_8^0-tmp_8^post6 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ -__disjvr_2^post6+__disjvr_2^0 == 0 /\ -result_4^post6+result_4^0 == 0 /\ __disjvr_0^0-__disjvr_0^post6 == 0 /\ -x_5^post6+x_5^0 == 0 /\ z_7^0-z_7^post6 == 0 /\ y_6^0-y_6^post6 == 0), cost: 1
   9: l7 -> l3 : __disjvr_0^0'=__disjvr_0^post10, __disjvr_1^0'=__disjvr_1^post10, __disjvr_2^0'=__disjvr_2^post10, result_4^0'=result_4^post10, tmp_8^0'=tmp_8^post10, x_5^0'=x_5^post10, y_6^0'=y_6^post10, z_7^0'=z_7^post10, (0 == 0 /\ -x_5^post10+x_5^0 == 0 /\ y_6^0-y_6^post10 == 0 /\ __disjvr_0^0-__disjvr_0^post10 == 0 /\ -__disjvr_2^post10+__disjvr_2^0 == 0 /\ z_7^0-z_7^post10 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -tmp_8^post10 <= 0 /\ -result_4^post10+result_4^0 == 0 /\ tmp_8^post10 <= 0 /\ -__disjvr_1^post10+__disjvr_1^0 == 0), cost: 1
  10: l7 -> l9 : __disjvr_0^0'=__disjvr_0^post11, __disjvr_1^0'=__disjvr_1^post11, __disjvr_2^0'=__disjvr_2^post11, result_4^0'=result_4^post11, tmp_8^0'=tmp_8^post11, x_5^0'=x_5^post11, y_6^0'=y_6^post11, z_7^0'=z_7^post11, (0 == 0 /\ y_6^0-y_6^post11 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ -x_5^post11+x_5^0 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ z_7^0-z_7^post11 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -__disjvr_0^post11+__disjvr_0^0 == 0), cost: 1
  13: l7 -> l1 : __disjvr_0^0'=__disjvr_0^post14, __disjvr_1^0'=__disjvr_1^post14, __disjvr_2^0'=__disjvr_2^post14, result_4^0'=result_4^post14, tmp_8^0'=tmp_8^post14, x_5^0'=x_5^post14, y_6^0'=y_6^post14, z_7^0'=z_7^post14, (__disjvr_1^0-__disjvr_1^post14 == 0 /\ z_7^0-z_7^post14 == 0 /\ -result_4^post14+result_4^0 == 0 /\ __disjvr_0^0-__disjvr_0^post14 == 0 /\ y_6^0-y_6^post14 == 0 /\ tmp_8^0-tmp_8^post14 == 0 /\ -1+x_5^post14-x_5^0 == 0 /\ z_7^0-y_6^0 <= 0 /\ -__disjvr_2^post14+__disjvr_2^0 == 0), cost: 1
  11: l9 -> l10 : __disjvr_0^0'=__disjvr_0^post12, __disjvr_1^0'=__disjvr_1^post12, __disjvr_2^0'=__disjvr_2^post12, result_4^0'=result_4^post12, tmp_8^0'=tmp_8^post12, x_5^0'=x_5^post12, y_6^0'=y_6^post12, z_7^0'=z_7^post12, (tmp_8^0-tmp_8^post12 == 0 /\ -x_5^post12+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post12 == 0 /\ -result_4^post12+result_4^0 == 0 /\ -__disjvr_1^post12+__disjvr_1^0 == 0 /\ -__disjvr_2^post12+__disjvr_2^0 == 0 /\ z_7^0-z_7^post12 == 0 /\ __disjvr_1^post12-__disjvr_1^0 == 0 /\ y_6^0-y_6^post12 == 0), cost: 1
  12: l10 -> l2 : __disjvr_0^0'=__disjvr_0^post13, __disjvr_1^0'=__disjvr_1^post13, __disjvr_2^0'=__disjvr_2^post13, result_4^0'=result_4^post13, tmp_8^0'=tmp_8^post13, x_5^0'=x_5^post13, y_6^0'=y_6^post13, z_7^0'=z_7^post13, (-__disjvr_0^post13+__disjvr_0^0 == 0 /\ -__disjvr_1^post13+__disjvr_1^0 == 0 /\ tmp_8^0-tmp_8^post13 == 0 /\ -result_4^post13+result_4^0 == 0 /\ -x_5^post13+x_5^0 == 0 /\ -1+y_6^post13-y_6^0 == 0 /\ z_7^0-z_7^post13 == 0 /\ __disjvr_2^0-__disjvr_2^post13 == 0), cost: 1
  15: l11 -> l3 : __disjvr_0^0'=__disjvr_0^post16, __disjvr_1^0'=__disjvr_1^post16, __disjvr_2^0'=__disjvr_2^post16, result_4^0'=result_4^post16, tmp_8^0'=tmp_8^post16, x_5^0'=x_5^post16, y_6^0'=y_6^post16, z_7^0'=z_7^post16, (-__disjvr_1^post16+__disjvr_1^0 == 0 /\ -__disjvr_2^post16+__disjvr_2^0 == 0 /\ z_7^0-z_7^post16 == 0 /\ y_6^0-y_6^post16 == 0 /\ result_4^0-result_4^post16 == 0 /\ __disjvr_0^0-__disjvr_0^post16 == 0 /\ tmp_8^0-tmp_8^post16 == 0 /\ -x_5^post16+x_5^0 == 0), cost: 1
  17: l12 -> l13 : __disjvr_0^0'=__disjvr_0^post18, __disjvr_1^0'=__disjvr_1^post18, __disjvr_2^0'=__disjvr_2^post18, result_4^0'=result_4^post18, tmp_8^0'=tmp_8^post18, x_5^0'=x_5^post18, y_6^0'=y_6^post18, z_7^0'=z_7^post18, (result_4^0-result_4^post18 == 0 /\ -z_7^post18+z_7^0 == 0 /\ -__disjvr_2^0+__disjvr_2^post18 == 0 /\ -x_5^post18+x_5^0 == 0 /\ -tmp_8^post18+tmp_8^0 == 0 /\ __disjvr_2^0-__disjvr_2^post18 == 0 /\ y_6^0-y_6^post18 == 0 /\ __disjvr_0^0-__disjvr_0^post18 == 0 /\ -__disjvr_1^post18+__disjvr_1^0 == 0), cost: 1
  18: l13 -> l2 : __disjvr_0^0'=__disjvr_0^post19, __disjvr_1^0'=__disjvr_1^post19, __disjvr_2^0'=__disjvr_2^post19, result_4^0'=result_4^post19, tmp_8^0'=tmp_8^post19, x_5^0'=x_5^post19, y_6^0'=y_6^post19, z_7^0'=z_7^post19, (-result_4^post19+result_4^0 == 0 /\ -__disjvr_1^post19+__disjvr_1^0 == 0 /\ __disjvr_2^0-__disjvr_2^post19 == 0 /\ x_5^0-x_5^post19 == 0 /\ -1+y_6^post19-y_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post19 == 0 /\ tmp_8^0-tmp_8^post19 == 0 /\ z_7^0-z_7^post19 == 0), cost: 1
  19: l14 -> l0 : __disjvr_0^0'=__disjvr_0^post20, __disjvr_1^0'=__disjvr_1^post20, __disjvr_2^0'=__disjvr_2^post20, result_4^0'=result_4^post20, tmp_8^0'=tmp_8^post20, x_5^0'=x_5^post20, y_6^0'=y_6^post20, z_7^0'=z_7^post20, (-z_7^post20+z_7^0 == 0 /\ y_6^0-y_6^post20 == 0 /\ -x_5^post20+x_5^0 == 0 /\ -__disjvr_1^post20+__disjvr_1^0 == 0 /\ result_4^0-result_4^post20 == 0 /\ -__disjvr_2^post20+__disjvr_2^0 == 0 /\ __disjvr_0^0-__disjvr_0^post20 == 0 /\ -tmp_8^post20+tmp_8^0 == 0), cost: 1

Chained Linear Paths

Start location: l14
Program variables: __disjvr_0^0 __disjvr_1^0 __disjvr_2^0 result_4^0 tmp_8^0 x_5^0 y_6^0 z_7^0
   7: l1 -> l7 : __disjvr_0^0'=__disjvr_0^post8, __disjvr_1^0'=__disjvr_1^post8, __disjvr_2^0'=__disjvr_2^post8, result_4^0'=result_4^post8, tmp_8^0'=tmp_8^post8, x_5^0'=x_5^post8, y_6^0'=y_6^post8, z_7^0'=z_7^post8, (-__disjvr_2^post8+__disjvr_2^0 == 0 /\ __disjvr_0^0-__disjvr_0^post8 == 0 /\ -result_4^post8+result_4^0 == 0 /\ 1-y_6^0+x_5^0 <= 0 /\ __disjvr_1^0-__disjvr_1^post8 == 0 /\ -tmp_8^post8+tmp_8^0 == 0 /\ y_6^0-y_6^post8 == 0 /\ z_7^0-z_7^post8 == 0 /\ -x_5^post8+x_5^0 == 0), cost: 1
   8: l1 -> l8 : __disjvr_0^0'=__disjvr_0^post9, __disjvr_1^0'=__disjvr_1^post9, __disjvr_2^0'=__disjvr_2^post9, result_4^0'=result_4^post9, tmp_8^0'=tmp_8^post9, x_5^0'=x_5^post9, y_6^0'=y_6^post9, z_7^0'=z_7^post9, (0 == 0 /\ tmp_8^0-tmp_8^post9 == 0 /\ y_6^0-x_5^0 <= 0 /\ -y_6^post9+y_6^0 == 0 /\ -__disjvr_1^post9+__disjvr_1^0 == 0 /\ -__disjvr_0^post9+__disjvr_0^0 == 0 /\ __disjvr_2^0-__disjvr_2^post9 == 0 /\ z_7^0-z_7^post9 == 0 /\ x_5^0-x_5^post9 == 0), cost: 1
   1: l2 -> l3 : __disjvr_0^0'=__disjvr_0^post2, __disjvr_1^0'=__disjvr_1^post2, __disjvr_2^0'=__disjvr_2^post2, result_4^0'=result_4^post2, tmp_8^0'=tmp_8^post2, x_5^0'=x_5^post2, y_6^0'=y_6^post2, z_7^0'=z_7^post2, (0 == 0 /\ z_7^0-z_7^post2 == 0 /\ __disjvr_0^0-__disjvr_0^post2 == 0 /\ -tmp_8^post2 <= 0 /\ x_5^0-x_5^post2 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ tmp_8^post2 <= 0 /\ -__disjvr_2^post2+__disjvr_2^0 == 0 /\ -__disjvr_1^post2+__disjvr_1^0 == 0 /\ -result_4^post2+result_4^0 == 0 /\ -y_6^post2+y_6^0 == 0), cost: 1
   6: l2 -> l1 : __disjvr_0^0'=__disjvr_0^post7, __disjvr_1^0'=__disjvr_1^post7, __disjvr_2^0'=__disjvr_2^post7, result_4^0'=result_4^post7, tmp_8^0'=tmp_8^post7, x_5^0'=x_5^post7, y_6^0'=y_6^post7, z_7^0'=z_7^post7, (tmp_8^0-tmp_8^post7 == 0 /\ -__disjvr_0^post7+__disjvr_0^0 == 0 /\ z_7^0-z_7^post7 == 0 /\ -1+x_5^post7-x_5^0 == 0 /\ z_7^0-y_6^0 <= 0 /\ __disjvr_2^0-__disjvr_2^post7 == 0 /\ -y_6^post7+y_6^0 == 0 /\ -result_4^post7+result_4^0 == 0 /\ -__disjvr_1^post7+__disjvr_1^0 == 0), cost: 1
  25: l2 -> l2 : __disjvr_0^0'=__disjvr_0^post6, __disjvr_1^0'=__disjvr_1^post6, __disjvr_2^0'=__disjvr_2^post6, result_4^0'=result_4^post6, tmp_8^0'=tmp_8^post6, x_5^0'=x_5^post6, y_6^0'=y_6^post6, z_7^0'=z_7^post6, (0 == 0 /\ -x_5^post3+x_5^0 == 0 /\ tmp_8^post5-tmp_8^post6 == 0 /\ x_5^post3-x_5^post4 == 0 /\ -z_7^post3+z_7^0 == 0 /\ -x_5^post5+x_5^post4 == 0 /\ -__disjvr_2^post6+__disjvr_2^post5 == 0 /\ -__disjvr_1^post3+__disjvr_1^0 == 0 /\ -1-y_6^post4+y_6^post5 == 0 /\ -z_7^post5+z_7^post4 == 0 /\ result_4^0-result_4^post3 == 0 /\ -__disjvr_0^post6+__disjvr_0^post5 == 0 /\ tmp_8^post3-tmp_8^post4 == 0 /\ -y_6^post4+y_6^post3 == 0 /\ z_7^post3-z_7^post4 == 0 /\ __disjvr_2^post3-__disjvr_2^post4 == 0 /\ -__disjvr_1^post5+__disjvr_1^post4 == 0 /\ __disjvr_0^post4-__disjvr_0^post3 == 0 /\ y_6^0-y_6^post3 == 0 /\ __disjvr_1^post3-__disjvr_1^post4 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -result_4^post4+result_4^post3 == 0 /\ result_4^post4-result_4^post5 == 0 /\ -__disjvr_0^post4+__disjvr_0^post3 == 0 /\ -x_5^post6+x_5^post5 == 0 /\ -__disjvr_2^post3+__disjvr_2^0 == 0 /\ -result_4^post6+result_4^post5 == 0 /\ __disjvr_1^post5-__disjvr_1^post6 == 0 /\ __disjvr_0^post4-__disjvr_0^post5 == 0 /\ -tmp_8^post5+tmp_8^post4 == 0 /\ -__disjvr_2^post5+__disjvr_2^post4 == 0 /\ __disjvr_0^0-__disjvr_0^post3 == 0 /\ z_7^post5-z_7^post6 == 0 /\ -y_6^post6+y_6^post5 == 0), cost: 1
  26: l3 -> l3 : __disjvr_0^0'=__disjvr_0^post16, __disjvr_1^0'=__disjvr_1^post16, __disjvr_2^0'=__disjvr_2^post16, result_4^0'=result_4^post16, tmp_8^0'=tmp_8^post16, x_5^0'=x_5^post16, y_6^0'=y_6^post16, z_7^0'=z_7^post16, (0 == 0 /\ -__disjvr_2^post15+__disjvr_2^0 == 0 /\ -__disjvr_1^post15+__disjvr_1^0 == 0 /\ -result_4^post15+result_4^0 == 0 /\ __disjvr_0^post15-__disjvr_0^post16 == 0 /\ z_7^0-z_7^post15 == 0 /\ __disjvr_2^post15-__disjvr_2^post16 == 0 /\ -tmp_8^post15 <= 0 /\ -__disjvr_1^post16+__disjvr_1^post15 == 0 /\ -tmp_8^post16+tmp_8^post15 == 0 /\ __disjvr_0^0-__disjvr_0^post15 == 0 /\ x_5^0-x_5^post15 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ result_4^post15-result_4^post16 == 0 /\ tmp_8^post15 <= 0 /\ -z_7^post16+z_7^post15 == 0 /\ y_6^post15-y_6^post16 == 0 /\ -x_5^post16+x_5^post15 == 0 /\ -y_6^post15+y_6^0 == 0), cost: 1
  28: l3 -> l2 : __disjvr_0^0'=__disjvr_0^post19, __disjvr_1^0'=__disjvr_1^post19, __disjvr_2^0'=__disjvr_2^post19, result_4^0'=result_4^post19, tmp_8^0'=tmp_8^post19, x_5^0'=x_5^post19, y_6^0'=y_6^post19, z_7^0'=z_7^post19, (0 == 0 /\ result_4^post17-result_4^post18 == 0 /\ -result_4^post19+result_4^post18 == 0 /\ -tmp_8^post18+tmp_8^post17 == 0 /\ __disjvr_2^post17-__disjvr_2^post18 == 0 /\ tmp_8^post18-tmp_8^post19 == 0 /\ z_7^0-z_7^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ x_5^post18-x_5^post19 == 0 /\ __disjvr_1^post18-__disjvr_1^post19 == 0 /\ y_6^post17-y_6^post18 == 0 /\ __disjvr_0^post17-__disjvr_0^post18 == 0 /\ -__disjvr_2^post17+__disjvr_2^post18 == 0 /\ -z_7^post18+z_7^post17 == 0 /\ -1+y_6^post19-y_6^post18 == 0 /\ -__disjvr_0^post19+__disjvr_0^post18 == 0 /\ z_7^post18-z_7^post19 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -x_5^post17+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ x_5^post17-x_5^post18 == 0 /\ -y_6^post17+y_6^0 == 0 /\ -__disjvr_1^post18+__disjvr_1^post17 == 0 /\ -result_4^post17+result_4^0 == 0 /\ -__disjvr_1^post17+__disjvr_1^0 == 0 /\ __disjvr_2^post18-__disjvr_2^post19 == 0), cost: 1
   9: l7 -> l3 : __disjvr_0^0'=__disjvr_0^post10, __disjvr_1^0'=__disjvr_1^post10, __disjvr_2^0'=__disjvr_2^post10, result_4^0'=result_4^post10, tmp_8^0'=tmp_8^post10, x_5^0'=x_5^post10, y_6^0'=y_6^post10, z_7^0'=z_7^post10, (0 == 0 /\ -x_5^post10+x_5^0 == 0 /\ y_6^0-y_6^post10 == 0 /\ __disjvr_0^0-__disjvr_0^post10 == 0 /\ -__disjvr_2^post10+__disjvr_2^0 == 0 /\ z_7^0-z_7^post10 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -tmp_8^post10 <= 0 /\ -result_4^post10+result_4^0 == 0 /\ tmp_8^post10 <= 0 /\ -__disjvr_1^post10+__disjvr_1^0 == 0), cost: 1
  13: l7 -> l1 : __disjvr_0^0'=__disjvr_0^post14, __disjvr_1^0'=__disjvr_1^post14, __disjvr_2^0'=__disjvr_2^post14, result_4^0'=result_4^post14, tmp_8^0'=tmp_8^post14, x_5^0'=x_5^post14, y_6^0'=y_6^post14, z_7^0'=z_7^post14, (__disjvr_1^0-__disjvr_1^post14 == 0 /\ z_7^0-z_7^post14 == 0 /\ -result_4^post14+result_4^0 == 0 /\ __disjvr_0^0-__disjvr_0^post14 == 0 /\ y_6^0-y_6^post14 == 0 /\ tmp_8^0-tmp_8^post14 == 0 /\ -1+x_5^post14-x_5^0 == 0 /\ z_7^0-y_6^0 <= 0 /\ -__disjvr_2^post14+__disjvr_2^0 == 0), cost: 1
  22: l7 -> l2 : __disjvr_0^0'=__disjvr_0^post13, __disjvr_1^0'=__disjvr_1^post13, __disjvr_2^0'=__disjvr_2^post13, result_4^0'=result_4^post13, tmp_8^0'=tmp_8^post13, x_5^0'=x_5^post13, y_6^0'=y_6^post13, z_7^0'=z_7^post13, (0 == 0 /\ -__disjvr_1^post11+__disjvr_1^post12 == 0 /\ y_6^0-y_6^post11 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ __disjvr_0^post11-__disjvr_0^post12 == 0 /\ -x_5^post11+x_5^0 == 0 /\ __disjvr_1^post11-__disjvr_1^post12 == 0 /\ -__disjvr_1^post13+__disjvr_1^post12 == 0 /\ __disjvr_2^post12-__disjvr_2^post13 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ -tmp_8^post13+tmp_8^post12 == 0 /\ -x_5^post12+x_5^post11 == 0 /\ z_7^0-z_7^post11 == 0 /\ result_4^post11-result_4^post12 == 0 /\ -result_4^post13+result_4^post12 == 0 /\ -__disjvr_0^post13+__disjvr_0^post12 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -z_7^post13+z_7^post12 == 0 /\ -1+y_6^post13-y_6^post12 == 0 /\ z_7^post11-z_7^post12 == 0 /\ -y_6^post12+y_6^post11 == 0 /\ x_5^post12-x_5^post13 == 0 /\ -__disjvr_0^post11+__disjvr_0^0 == 0 /\ -__disjvr_2^post12+__disjvr_2^post11 == 0 /\ tmp_8^post11-tmp_8^post12 == 0), cost: 1
  20: l14 -> l1 : __disjvr_0^0'=__disjvr_0^post1, __disjvr_1^0'=__disjvr_1^post1, __disjvr_2^0'=__disjvr_2^post1, result_4^0'=result_4^post1, tmp_8^0'=tmp_8^post1, x_5^0'=x_5^post1, y_6^0'=y_6^post1, z_7^0'=z_7^post1, (-z_7^post20+z_7^0 == 0 /\ z_7^post20-z_7^post1 == 0 /\ result_4^post20-result_4^post1 == 0 /\ y_6^0-y_6^post20 == 0 /\ tmp_8^post20-tmp_8^post1 == 0 /\ -x_5^post20+x_5^0 == 0 /\ x_5^post20-x_5^post1 == 0 /\ -__disjvr_0^post1+__disjvr_0^post20 == 0 /\ -__disjvr_1^post20+__disjvr_1^0 == 0 /\ y_6^post20-y_6^post1 == 0 /\ result_4^0-result_4^post20 == 0 /\ __disjvr_1^post20-__disjvr_1^post1 == 0 /\ -__disjvr_2^post20+__disjvr_2^0 == 0 /\ __disjvr_2^post20-__disjvr_2^post1 == 0 /\ __disjvr_0^0-__disjvr_0^post20 == 0 /\ -tmp_8^post20+tmp_8^0 == 0), cost: 1

	Eliminating location l0 by chaining:

	Applied chaining

	First rule:
	l14 -> l0 : __disjvr_0^0'=__disjvr_0^post20, __disjvr_1^0'=__disjvr_1^post20, __disjvr_2^0'=__disjvr_2^post20, result_4^0'=result_4^post20, tmp_8^0'=tmp_8^post20, x_5^0'=x_5^post20, y_6^0'=y_6^post20, z_7^0'=z_7^post20, (-z_7^post20+z_7^0 == 0 /\ y_6^0-y_6^post20 == 0 /\ -x_5^post20+x_5^0 == 0 /\ -__disjvr_1^post20+__disjvr_1^0 == 0 /\ result_4^0-result_4^post20 == 0 /\ -__disjvr_2^post20+__disjvr_2^0 == 0 /\ __disjvr_0^0-__disjvr_0^post20 == 0 /\ -tmp_8^post20+tmp_8^0 == 0), cost: 1
	Second rule:
	l0 -> l1 : __disjvr_0^0'=__disjvr_0^post1, __disjvr_1^0'=__disjvr_1^post1, __disjvr_2^0'=__disjvr_2^post1, result_4^0'=result_4^post1, tmp_8^0'=tmp_8^post1, x_5^0'=x_5^post1, y_6^0'=y_6^post1, z_7^0'=z_7^post1, (result_4^0-result_4^post1 == 0 /\ y_6^0-y_6^post1 == 0 /\ __disjvr_2^0-__disjvr_2^post1 == 0 /\ z_7^0-z_7^post1 == 0 /\ tmp_8^0-tmp_8^post1 == 0 /\ -__disjvr_0^post1+__disjvr_0^0 == 0 /\ -__disjvr_1^post1+__disjvr_1^0 == 0 /\ -x_5^post1+x_5^0 == 0), cost: 1
	New rule:
	l14 -> l1 : __disjvr_0^0'=__disjvr_0^post1, __disjvr_1^0'=__disjvr_1^post1, __disjvr_2^0'=__disjvr_2^post1, result_4^0'=result_4^post1, tmp_8^0'=tmp_8^post1, x_5^0'=x_5^post1, y_6^0'=y_6^post1, z_7^0'=z_7^post1, (-z_7^post20+z_7^0 == 0 /\ z_7^post20-z_7^post1 == 0 /\ result_4^post20-result_4^post1 == 0 /\ y_6^0-y_6^post20 == 0 /\ tmp_8^post20-tmp_8^post1 == 0 /\ -x_5^post20+x_5^0 == 0 /\ x_5^post20-x_5^post1 == 0 /\ -__disjvr_0^post1+__disjvr_0^post20 == 0 /\ -__disjvr_1^post20+__disjvr_1^0 == 0 /\ y_6^post20-y_6^post1 == 0 /\ result_4^0-result_4^post20 == 0 /\ __disjvr_1^post20-__disjvr_1^post1 == 0 /\ -__disjvr_2^post20+__disjvr_2^0 == 0 /\ __disjvr_2^post20-__disjvr_2^post1 == 0 /\ __disjvr_0^0-__disjvr_0^post20 == 0 /\ -tmp_8^post20+tmp_8^0 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 0 19
	
	Eliminating location l9 by chaining:

	Applied chaining

	First rule:
	l7 -> l9 : __disjvr_0^0'=__disjvr_0^post11, __disjvr_1^0'=__disjvr_1^post11, __disjvr_2^0'=__disjvr_2^post11, result_4^0'=result_4^post11, tmp_8^0'=tmp_8^post11, x_5^0'=x_5^post11, y_6^0'=y_6^post11, z_7^0'=z_7^post11, (0 == 0 /\ y_6^0-y_6^post11 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ -x_5^post11+x_5^0 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ z_7^0-z_7^post11 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -__disjvr_0^post11+__disjvr_0^0 == 0), cost: 1
	Second rule:
	l9 -> l10 : __disjvr_0^0'=__disjvr_0^post12, __disjvr_1^0'=__disjvr_1^post12, __disjvr_2^0'=__disjvr_2^post12, result_4^0'=result_4^post12, tmp_8^0'=tmp_8^post12, x_5^0'=x_5^post12, y_6^0'=y_6^post12, z_7^0'=z_7^post12, (tmp_8^0-tmp_8^post12 == 0 /\ -x_5^post12+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post12 == 0 /\ -result_4^post12+result_4^0 == 0 /\ -__disjvr_1^post12+__disjvr_1^0 == 0 /\ -__disjvr_2^post12+__disjvr_2^0 == 0 /\ z_7^0-z_7^post12 == 0 /\ __disjvr_1^post12-__disjvr_1^0 == 0 /\ y_6^0-y_6^post12 == 0), cost: 1
	New rule:
	l7 -> l10 : __disjvr_0^0'=__disjvr_0^post12, __disjvr_1^0'=__disjvr_1^post12, __disjvr_2^0'=__disjvr_2^post12, result_4^0'=result_4^post12, tmp_8^0'=tmp_8^post12, x_5^0'=x_5^post12, y_6^0'=y_6^post12, z_7^0'=z_7^post12, (0 == 0 /\ -__disjvr_1^post11+__disjvr_1^post12 == 0 /\ y_6^0-y_6^post11 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ __disjvr_0^post11-__disjvr_0^post12 == 0 /\ -x_5^post11+x_5^0 == 0 /\ __disjvr_1^post11-__disjvr_1^post12 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ -x_5^post12+x_5^post11 == 0 /\ z_7^0-z_7^post11 == 0 /\ result_4^post11-result_4^post12 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ z_7^post11-z_7^post12 == 0 /\ -y_6^post12+y_6^post11 == 0 /\ -__disjvr_0^post11+__disjvr_0^0 == 0 /\ -__disjvr_2^post12+__disjvr_2^post11 == 0 /\ tmp_8^post11-tmp_8^post12 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 10 11
	
	Eliminating location l10 by chaining:

	Applied chaining

	First rule:
	l7 -> l10 : __disjvr_0^0'=__disjvr_0^post12, __disjvr_1^0'=__disjvr_1^post12, __disjvr_2^0'=__disjvr_2^post12, result_4^0'=result_4^post12, tmp_8^0'=tmp_8^post12, x_5^0'=x_5^post12, y_6^0'=y_6^post12, z_7^0'=z_7^post12, (0 == 0 /\ -__disjvr_1^post11+__disjvr_1^post12 == 0 /\ y_6^0-y_6^post11 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ __disjvr_0^post11-__disjvr_0^post12 == 0 /\ -x_5^post11+x_5^0 == 0 /\ __disjvr_1^post11-__disjvr_1^post12 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ -x_5^post12+x_5^post11 == 0 /\ z_7^0-z_7^post11 == 0 /\ result_4^post11-result_4^post12 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ z_7^post11-z_7^post12 == 0 /\ -y_6^post12+y_6^post11 == 0 /\ -__disjvr_0^post11+__disjvr_0^0 == 0 /\ -__disjvr_2^post12+__disjvr_2^post11 == 0 /\ tmp_8^post11-tmp_8^post12 == 0), cost: 1
	Second rule:
	l10 -> l2 : __disjvr_0^0'=__disjvr_0^post13, __disjvr_1^0'=__disjvr_1^post13, __disjvr_2^0'=__disjvr_2^post13, result_4^0'=result_4^post13, tmp_8^0'=tmp_8^post13, x_5^0'=x_5^post13, y_6^0'=y_6^post13, z_7^0'=z_7^post13, (-__disjvr_0^post13+__disjvr_0^0 == 0 /\ -__disjvr_1^post13+__disjvr_1^0 == 0 /\ tmp_8^0-tmp_8^post13 == 0 /\ -result_4^post13+result_4^0 == 0 /\ -x_5^post13+x_5^0 == 0 /\ -1+y_6^post13-y_6^0 == 0 /\ z_7^0-z_7^post13 == 0 /\ __disjvr_2^0-__disjvr_2^post13 == 0), cost: 1
	New rule:
	l7 -> l2 : __disjvr_0^0'=__disjvr_0^post13, __disjvr_1^0'=__disjvr_1^post13, __disjvr_2^0'=__disjvr_2^post13, result_4^0'=result_4^post13, tmp_8^0'=tmp_8^post13, x_5^0'=x_5^post13, y_6^0'=y_6^post13, z_7^0'=z_7^post13, (0 == 0 /\ -__disjvr_1^post11+__disjvr_1^post12 == 0 /\ y_6^0-y_6^post11 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ __disjvr_0^post11-__disjvr_0^post12 == 0 /\ -x_5^post11+x_5^0 == 0 /\ __disjvr_1^post11-__disjvr_1^post12 == 0 /\ -__disjvr_1^post13+__disjvr_1^post12 == 0 /\ __disjvr_2^post12-__disjvr_2^post13 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ -tmp_8^post13+tmp_8^post12 == 0 /\ -x_5^post12+x_5^post11 == 0 /\ z_7^0-z_7^post11 == 0 /\ result_4^post11-result_4^post12 == 0 /\ -result_4^post13+result_4^post12 == 0 /\ -__disjvr_0^post13+__disjvr_0^post12 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -z_7^post13+z_7^post12 == 0 /\ -1+y_6^post13-y_6^post12 == 0 /\ z_7^post11-z_7^post12 == 0 /\ -y_6^post12+y_6^post11 == 0 /\ x_5^post12-x_5^post13 == 0 /\ -__disjvr_0^post11+__disjvr_0^0 == 0 /\ -__disjvr_2^post12+__disjvr_2^post11 == 0 /\ tmp_8^post11-tmp_8^post12 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 12 21
	
	Eliminating location l5 by chaining:

	Applied chaining

	First rule:
	l2 -> l5 : __disjvr_0^0'=__disjvr_0^post3, __disjvr_1^0'=__disjvr_1^post3, __disjvr_2^0'=__disjvr_2^post3, result_4^0'=result_4^post3, tmp_8^0'=tmp_8^post3, x_5^0'=x_5^post3, y_6^0'=y_6^post3, z_7^0'=z_7^post3, (0 == 0 /\ -x_5^post3+x_5^0 == 0 /\ -z_7^post3+z_7^0 == 0 /\ -__disjvr_1^post3+__disjvr_1^0 == 0 /\ result_4^0-result_4^post3 == 0 /\ y_6^0-y_6^post3 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -__disjvr_2^post3+__disjvr_2^0 == 0 /\ __disjvr_0^0-__disjvr_0^post3 == 0), cost: 1
	Second rule:
	l5 -> l6 : __disjvr_0^0'=__disjvr_0^post4, __disjvr_1^0'=__disjvr_1^post4, __disjvr_2^0'=__disjvr_2^post4, result_4^0'=result_4^post4, tmp_8^0'=tmp_8^post4, x_5^0'=x_5^post4, y_6^0'=y_6^post4, z_7^0'=z_7^post4, (z_7^0-z_7^post4 == 0 /\ -result_4^post4+result_4^0 == 0 /\ -__disjvr_1^post4+__disjvr_1^0 == 0 /\ x_5^0-x_5^post4 == 0 /\ tmp_8^0-tmp_8^post4 == 0 /\ __disjvr_2^0-__disjvr_2^post4 == 0 /\ -__disjvr_0^0+__disjvr_0^post4 == 0 /\ -y_6^post4+y_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post4 == 0), cost: 1
	New rule:
	l2 -> l6 : __disjvr_0^0'=__disjvr_0^post4, __disjvr_1^0'=__disjvr_1^post4, __disjvr_2^0'=__disjvr_2^post4, result_4^0'=result_4^post4, tmp_8^0'=tmp_8^post4, x_5^0'=x_5^post4, y_6^0'=y_6^post4, z_7^0'=z_7^post4, (0 == 0 /\ -x_5^post3+x_5^0 == 0 /\ x_5^post3-x_5^post4 == 0 /\ -z_7^post3+z_7^0 == 0 /\ -__disjvr_1^post3+__disjvr_1^0 == 0 /\ result_4^0-result_4^post3 == 0 /\ tmp_8^post3-tmp_8^post4 == 0 /\ -y_6^post4+y_6^post3 == 0 /\ z_7^post3-z_7^post4 == 0 /\ __disjvr_2^post3-__disjvr_2^post4 == 0 /\ __disjvr_0^post4-__disjvr_0^post3 == 0 /\ y_6^0-y_6^post3 == 0 /\ __disjvr_1^post3-__disjvr_1^post4 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -result_4^post4+result_4^post3 == 0 /\ -__disjvr_0^post4+__disjvr_0^post3 == 0 /\ -__disjvr_2^post3+__disjvr_2^0 == 0 /\ __disjvr_0^0-__disjvr_0^post3 == 0), cost: 1
	
	Applied deletion

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

	Applied chaining

	First rule:
	l2 -> l6 : __disjvr_0^0'=__disjvr_0^post4, __disjvr_1^0'=__disjvr_1^post4, __disjvr_2^0'=__disjvr_2^post4, result_4^0'=result_4^post4, tmp_8^0'=tmp_8^post4, x_5^0'=x_5^post4, y_6^0'=y_6^post4, z_7^0'=z_7^post4, (0 == 0 /\ -x_5^post3+x_5^0 == 0 /\ x_5^post3-x_5^post4 == 0 /\ -z_7^post3+z_7^0 == 0 /\ -__disjvr_1^post3+__disjvr_1^0 == 0 /\ result_4^0-result_4^post3 == 0 /\ tmp_8^post3-tmp_8^post4 == 0 /\ -y_6^post4+y_6^post3 == 0 /\ z_7^post3-z_7^post4 == 0 /\ __disjvr_2^post3-__disjvr_2^post4 == 0 /\ __disjvr_0^post4-__disjvr_0^post3 == 0 /\ y_6^0-y_6^post3 == 0 /\ __disjvr_1^post3-__disjvr_1^post4 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -result_4^post4+result_4^post3 == 0 /\ -__disjvr_0^post4+__disjvr_0^post3 == 0 /\ -__disjvr_2^post3+__disjvr_2^0 == 0 /\ __disjvr_0^0-__disjvr_0^post3 == 0), cost: 1
	Second rule:
	l6 -> l4 : __disjvr_0^0'=__disjvr_0^post5, __disjvr_1^0'=__disjvr_1^post5, __disjvr_2^0'=__disjvr_2^post5, result_4^0'=result_4^post5, tmp_8^0'=tmp_8^post5, x_5^0'=x_5^post5, y_6^0'=y_6^post5, z_7^0'=z_7^post5, (-__disjvr_1^post5+__disjvr_1^0 == 0 /\ -x_5^post5+x_5^0 == 0 /\ -z_7^post5+z_7^0 == 0 /\ __disjvr_2^0-__disjvr_2^post5 == 0 /\ result_4^0-result_4^post5 == 0 /\ __disjvr_0^0-__disjvr_0^post5 == 0 /\ tmp_8^0-tmp_8^post5 == 0 /\ -1-y_6^0+y_6^post5 == 0), cost: 1
	New rule:
	l2 -> l4 : __disjvr_0^0'=__disjvr_0^post5, __disjvr_1^0'=__disjvr_1^post5, __disjvr_2^0'=__disjvr_2^post5, result_4^0'=result_4^post5, tmp_8^0'=tmp_8^post5, x_5^0'=x_5^post5, y_6^0'=y_6^post5, z_7^0'=z_7^post5, (0 == 0 /\ -x_5^post3+x_5^0 == 0 /\ x_5^post3-x_5^post4 == 0 /\ -z_7^post3+z_7^0 == 0 /\ -x_5^post5+x_5^post4 == 0 /\ -__disjvr_1^post3+__disjvr_1^0 == 0 /\ -1-y_6^post4+y_6^post5 == 0 /\ -z_7^post5+z_7^post4 == 0 /\ result_4^0-result_4^post3 == 0 /\ tmp_8^post3-tmp_8^post4 == 0 /\ -y_6^post4+y_6^post3 == 0 /\ z_7^post3-z_7^post4 == 0 /\ __disjvr_2^post3-__disjvr_2^post4 == 0 /\ -__disjvr_1^post5+__disjvr_1^post4 == 0 /\ __disjvr_0^post4-__disjvr_0^post3 == 0 /\ y_6^0-y_6^post3 == 0 /\ __disjvr_1^post3-__disjvr_1^post4 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -result_4^post4+result_4^post3 == 0 /\ result_4^post4-result_4^post5 == 0 /\ -__disjvr_0^post4+__disjvr_0^post3 == 0 /\ -__disjvr_2^post3+__disjvr_2^0 == 0 /\ __disjvr_0^post4-__disjvr_0^post5 == 0 /\ -tmp_8^post5+tmp_8^post4 == 0 /\ -__disjvr_2^post5+__disjvr_2^post4 == 0 /\ __disjvr_0^0-__disjvr_0^post3 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 4 23
	
	Eliminating location l4 by chaining:

	Applied chaining

	First rule:
	l2 -> l4 : __disjvr_0^0'=__disjvr_0^post5, __disjvr_1^0'=__disjvr_1^post5, __disjvr_2^0'=__disjvr_2^post5, result_4^0'=result_4^post5, tmp_8^0'=tmp_8^post5, x_5^0'=x_5^post5, y_6^0'=y_6^post5, z_7^0'=z_7^post5, (0 == 0 /\ -x_5^post3+x_5^0 == 0 /\ x_5^post3-x_5^post4 == 0 /\ -z_7^post3+z_7^0 == 0 /\ -x_5^post5+x_5^post4 == 0 /\ -__disjvr_1^post3+__disjvr_1^0 == 0 /\ -1-y_6^post4+y_6^post5 == 0 /\ -z_7^post5+z_7^post4 == 0 /\ result_4^0-result_4^post3 == 0 /\ tmp_8^post3-tmp_8^post4 == 0 /\ -y_6^post4+y_6^post3 == 0 /\ z_7^post3-z_7^post4 == 0 /\ __disjvr_2^post3-__disjvr_2^post4 == 0 /\ -__disjvr_1^post5+__disjvr_1^post4 == 0 /\ __disjvr_0^post4-__disjvr_0^post3 == 0 /\ y_6^0-y_6^post3 == 0 /\ __disjvr_1^post3-__disjvr_1^post4 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -result_4^post4+result_4^post3 == 0 /\ result_4^post4-result_4^post5 == 0 /\ -__disjvr_0^post4+__disjvr_0^post3 == 0 /\ -__disjvr_2^post3+__disjvr_2^0 == 0 /\ __disjvr_0^post4-__disjvr_0^post5 == 0 /\ -tmp_8^post5+tmp_8^post4 == 0 /\ -__disjvr_2^post5+__disjvr_2^post4 == 0 /\ __disjvr_0^0-__disjvr_0^post3 == 0), cost: 1
	Second rule:
	l4 -> l2 : __disjvr_0^0'=__disjvr_0^post6, __disjvr_1^0'=__disjvr_1^post6, __disjvr_2^0'=__disjvr_2^post6, result_4^0'=result_4^post6, tmp_8^0'=tmp_8^post6, x_5^0'=x_5^post6, y_6^0'=y_6^post6, z_7^0'=z_7^post6, (tmp_8^0-tmp_8^post6 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ -__disjvr_2^post6+__disjvr_2^0 == 0 /\ -result_4^post6+result_4^0 == 0 /\ __disjvr_0^0-__disjvr_0^post6 == 0 /\ -x_5^post6+x_5^0 == 0 /\ z_7^0-z_7^post6 == 0 /\ y_6^0-y_6^post6 == 0), cost: 1
	New rule:
	l2 -> l2 : __disjvr_0^0'=__disjvr_0^post6, __disjvr_1^0'=__disjvr_1^post6, __disjvr_2^0'=__disjvr_2^post6, result_4^0'=result_4^post6, tmp_8^0'=tmp_8^post6, x_5^0'=x_5^post6, y_6^0'=y_6^post6, z_7^0'=z_7^post6, (0 == 0 /\ -x_5^post3+x_5^0 == 0 /\ tmp_8^post5-tmp_8^post6 == 0 /\ x_5^post3-x_5^post4 == 0 /\ -z_7^post3+z_7^0 == 0 /\ -x_5^post5+x_5^post4 == 0 /\ -__disjvr_2^post6+__disjvr_2^post5 == 0 /\ -__disjvr_1^post3+__disjvr_1^0 == 0 /\ -1-y_6^post4+y_6^post5 == 0 /\ -z_7^post5+z_7^post4 == 0 /\ result_4^0-result_4^post3 == 0 /\ -__disjvr_0^post6+__disjvr_0^post5 == 0 /\ tmp_8^post3-tmp_8^post4 == 0 /\ -y_6^post4+y_6^post3 == 0 /\ z_7^post3-z_7^post4 == 0 /\ __disjvr_2^post3-__disjvr_2^post4 == 0 /\ -__disjvr_1^post5+__disjvr_1^post4 == 0 /\ __disjvr_0^post4-__disjvr_0^post3 == 0 /\ y_6^0-y_6^post3 == 0 /\ __disjvr_1^post3-__disjvr_1^post4 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -result_4^post4+result_4^post3 == 0 /\ result_4^post4-result_4^post5 == 0 /\ -__disjvr_0^post4+__disjvr_0^post3 == 0 /\ -x_5^post6+x_5^post5 == 0 /\ -__disjvr_2^post3+__disjvr_2^0 == 0 /\ -result_4^post6+result_4^post5 == 0 /\ __disjvr_1^post5-__disjvr_1^post6 == 0 /\ __disjvr_0^post4-__disjvr_0^post5 == 0 /\ -tmp_8^post5+tmp_8^post4 == 0 /\ -__disjvr_2^post5+__disjvr_2^post4 == 0 /\ __disjvr_0^0-__disjvr_0^post3 == 0 /\ z_7^post5-z_7^post6 == 0 /\ -y_6^post6+y_6^post5 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 5 24
	
	Eliminating location l11 by chaining:

	Applied chaining

	First rule:
	l3 -> l11 : __disjvr_0^0'=__disjvr_0^post15, __disjvr_1^0'=__disjvr_1^post15, __disjvr_2^0'=__disjvr_2^post15, result_4^0'=result_4^post15, tmp_8^0'=tmp_8^post15, x_5^0'=x_5^post15, y_6^0'=y_6^post15, z_7^0'=z_7^post15, (0 == 0 /\ -__disjvr_2^post15+__disjvr_2^0 == 0 /\ -__disjvr_1^post15+__disjvr_1^0 == 0 /\ -result_4^post15+result_4^0 == 0 /\ z_7^0-z_7^post15 == 0 /\ -tmp_8^post15 <= 0 /\ __disjvr_0^0-__disjvr_0^post15 == 0 /\ x_5^0-x_5^post15 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ tmp_8^post15 <= 0 /\ -y_6^post15+y_6^0 == 0), cost: 1
	Second rule:
	l11 -> l3 : __disjvr_0^0'=__disjvr_0^post16, __disjvr_1^0'=__disjvr_1^post16, __disjvr_2^0'=__disjvr_2^post16, result_4^0'=result_4^post16, tmp_8^0'=tmp_8^post16, x_5^0'=x_5^post16, y_6^0'=y_6^post16, z_7^0'=z_7^post16, (-__disjvr_1^post16+__disjvr_1^0 == 0 /\ -__disjvr_2^post16+__disjvr_2^0 == 0 /\ z_7^0-z_7^post16 == 0 /\ y_6^0-y_6^post16 == 0 /\ result_4^0-result_4^post16 == 0 /\ __disjvr_0^0-__disjvr_0^post16 == 0 /\ tmp_8^0-tmp_8^post16 == 0 /\ -x_5^post16+x_5^0 == 0), cost: 1
	New rule:
	l3 -> l3 : __disjvr_0^0'=__disjvr_0^post16, __disjvr_1^0'=__disjvr_1^post16, __disjvr_2^0'=__disjvr_2^post16, result_4^0'=result_4^post16, tmp_8^0'=tmp_8^post16, x_5^0'=x_5^post16, y_6^0'=y_6^post16, z_7^0'=z_7^post16, (0 == 0 /\ -__disjvr_2^post15+__disjvr_2^0 == 0 /\ -__disjvr_1^post15+__disjvr_1^0 == 0 /\ -result_4^post15+result_4^0 == 0 /\ __disjvr_0^post15-__disjvr_0^post16 == 0 /\ z_7^0-z_7^post15 == 0 /\ __disjvr_2^post15-__disjvr_2^post16 == 0 /\ -tmp_8^post15 <= 0 /\ -__disjvr_1^post16+__disjvr_1^post15 == 0 /\ -tmp_8^post16+tmp_8^post15 == 0 /\ __disjvr_0^0-__disjvr_0^post15 == 0 /\ x_5^0-x_5^post15 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ result_4^post15-result_4^post16 == 0 /\ tmp_8^post15 <= 0 /\ -z_7^post16+z_7^post15 == 0 /\ y_6^post15-y_6^post16 == 0 /\ -x_5^post16+x_5^post15 == 0 /\ -y_6^post15+y_6^0 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 14 15
	
	Eliminating location l12 by chaining:

	Applied chaining

	First rule:
	l3 -> l12 : __disjvr_0^0'=__disjvr_0^post17, __disjvr_1^0'=__disjvr_1^post17, __disjvr_2^0'=__disjvr_2^post17, result_4^0'=result_4^post17, tmp_8^0'=tmp_8^post17, x_5^0'=x_5^post17, y_6^0'=y_6^post17, z_7^0'=z_7^post17, (0 == 0 /\ z_7^0-z_7^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -x_5^post17+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ -y_6^post17+y_6^0 == 0 /\ -result_4^post17+result_4^0 == 0 /\ -__disjvr_1^post17+__disjvr_1^0 == 0), cost: 1
	Second rule:
	l12 -> l13 : __disjvr_0^0'=__disjvr_0^post18, __disjvr_1^0'=__disjvr_1^post18, __disjvr_2^0'=__disjvr_2^post18, result_4^0'=result_4^post18, tmp_8^0'=tmp_8^post18, x_5^0'=x_5^post18, y_6^0'=y_6^post18, z_7^0'=z_7^post18, (result_4^0-result_4^post18 == 0 /\ -z_7^post18+z_7^0 == 0 /\ -__disjvr_2^0+__disjvr_2^post18 == 0 /\ -x_5^post18+x_5^0 == 0 /\ -tmp_8^post18+tmp_8^0 == 0 /\ __disjvr_2^0-__disjvr_2^post18 == 0 /\ y_6^0-y_6^post18 == 0 /\ __disjvr_0^0-__disjvr_0^post18 == 0 /\ -__disjvr_1^post18+__disjvr_1^0 == 0), cost: 1
	New rule:
	l3 -> l13 : __disjvr_0^0'=__disjvr_0^post18, __disjvr_1^0'=__disjvr_1^post18, __disjvr_2^0'=__disjvr_2^post18, result_4^0'=result_4^post18, tmp_8^0'=tmp_8^post18, x_5^0'=x_5^post18, y_6^0'=y_6^post18, z_7^0'=z_7^post18, (0 == 0 /\ result_4^post17-result_4^post18 == 0 /\ -tmp_8^post18+tmp_8^post17 == 0 /\ __disjvr_2^post17-__disjvr_2^post18 == 0 /\ z_7^0-z_7^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ y_6^post17-y_6^post18 == 0 /\ __disjvr_0^post17-__disjvr_0^post18 == 0 /\ -__disjvr_2^post17+__disjvr_2^post18 == 0 /\ -z_7^post18+z_7^post17 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -x_5^post17+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ x_5^post17-x_5^post18 == 0 /\ -y_6^post17+y_6^0 == 0 /\ -__disjvr_1^post18+__disjvr_1^post17 == 0 /\ -result_4^post17+result_4^0 == 0 /\ -__disjvr_1^post17+__disjvr_1^0 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 16 17
	
	Eliminating location l13 by chaining:

	Applied chaining

	First rule:
	l3 -> l13 : __disjvr_0^0'=__disjvr_0^post18, __disjvr_1^0'=__disjvr_1^post18, __disjvr_2^0'=__disjvr_2^post18, result_4^0'=result_4^post18, tmp_8^0'=tmp_8^post18, x_5^0'=x_5^post18, y_6^0'=y_6^post18, z_7^0'=z_7^post18, (0 == 0 /\ result_4^post17-result_4^post18 == 0 /\ -tmp_8^post18+tmp_8^post17 == 0 /\ __disjvr_2^post17-__disjvr_2^post18 == 0 /\ z_7^0-z_7^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ y_6^post17-y_6^post18 == 0 /\ __disjvr_0^post17-__disjvr_0^post18 == 0 /\ -__disjvr_2^post17+__disjvr_2^post18 == 0 /\ -z_7^post18+z_7^post17 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -x_5^post17+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ x_5^post17-x_5^post18 == 0 /\ -y_6^post17+y_6^0 == 0 /\ -__disjvr_1^post18+__disjvr_1^post17 == 0 /\ -result_4^post17+result_4^0 == 0 /\ -__disjvr_1^post17+__disjvr_1^0 == 0), cost: 1
	Second rule:
	l13 -> l2 : __disjvr_0^0'=__disjvr_0^post19, __disjvr_1^0'=__disjvr_1^post19, __disjvr_2^0'=__disjvr_2^post19, result_4^0'=result_4^post19, tmp_8^0'=tmp_8^post19, x_5^0'=x_5^post19, y_6^0'=y_6^post19, z_7^0'=z_7^post19, (-result_4^post19+result_4^0 == 0 /\ -__disjvr_1^post19+__disjvr_1^0 == 0 /\ __disjvr_2^0-__disjvr_2^post19 == 0 /\ x_5^0-x_5^post19 == 0 /\ -1+y_6^post19-y_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post19 == 0 /\ tmp_8^0-tmp_8^post19 == 0 /\ z_7^0-z_7^post19 == 0), cost: 1
	New rule:
	l3 -> l2 : __disjvr_0^0'=__disjvr_0^post19, __disjvr_1^0'=__disjvr_1^post19, __disjvr_2^0'=__disjvr_2^post19, result_4^0'=result_4^post19, tmp_8^0'=tmp_8^post19, x_5^0'=x_5^post19, y_6^0'=y_6^post19, z_7^0'=z_7^post19, (0 == 0 /\ result_4^post17-result_4^post18 == 0 /\ -result_4^post19+result_4^post18 == 0 /\ -tmp_8^post18+tmp_8^post17 == 0 /\ __disjvr_2^post17-__disjvr_2^post18 == 0 /\ tmp_8^post18-tmp_8^post19 == 0 /\ z_7^0-z_7^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ x_5^post18-x_5^post19 == 0 /\ __disjvr_1^post18-__disjvr_1^post19 == 0 /\ y_6^post17-y_6^post18 == 0 /\ __disjvr_0^post17-__disjvr_0^post18 == 0 /\ -__disjvr_2^post17+__disjvr_2^post18 == 0 /\ -z_7^post18+z_7^post17 == 0 /\ -1+y_6^post19-y_6^post18 == 0 /\ -__disjvr_0^post19+__disjvr_0^post18 == 0 /\ z_7^post18-z_7^post19 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -x_5^post17+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ x_5^post17-x_5^post18 == 0 /\ -y_6^post17+y_6^0 == 0 /\ -__disjvr_1^post18+__disjvr_1^post17 == 0 /\ -result_4^post17+result_4^0 == 0 /\ -__disjvr_1^post17+__disjvr_1^0 == 0 /\ __disjvr_2^post18-__disjvr_2^post19 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 18 27

Simplified Transitions

Start location: l14
Program variables: result_4^0 tmp_8^0 x_5^0 y_6^0 z_7^0
  31: l1 -> l7 : 1-y_6^0+x_5^0 <= 0, cost: 1
  32: l1 -> l8 : result_4^0'=result_4^post9, y_6^0-x_5^0 <= 0, cost: 1
  29: l2 -> l3 : tmp_8^0'=0, 1-z_7^0+y_6^0 <= 0, cost: 1
  30: l2 -> l1 : x_5^0'=1+x_5^0, z_7^0-y_6^0 <= 0, cost: 1
  37: l2 -> l2 : tmp_8^0'=tmp_8^post5, y_6^0'=1+y_6^0, 1-z_7^0+y_6^0 <= 0, cost: 1
  38: l3 -> l3 : tmp_8^0'=0, 1-z_7^0+y_6^0 <= 0, cost: 1
  39: l3 -> l2 : tmp_8^0'=tmp_8^post18, y_6^0'=1+y_6^0, 1-z_7^0+y_6^0 <= 0, cost: 1
  33: l7 -> l3 : tmp_8^0'=0, 1-z_7^0+y_6^0 <= 0, cost: 1
  34: l7 -> l1 : x_5^0'=1+x_5^0, z_7^0-y_6^0 <= 0, cost: 1
  36: l7 -> l2 : tmp_8^0'=tmp_8^post12, y_6^0'=1+y_6^0, 1-z_7^0+y_6^0 <= 0, cost: 1
  35: l14 -> l1 : T, cost: 1

	made implied equalities explicit

	Original rule:
	l2 -> l3 : __disjvr_0^0'=__disjvr_0^post2, __disjvr_1^0'=__disjvr_1^post2, __disjvr_2^0'=__disjvr_2^post2, result_4^0'=result_4^post2, tmp_8^0'=tmp_8^post2, x_5^0'=x_5^post2, y_6^0'=y_6^post2, z_7^0'=z_7^post2, (0 == 0 /\ z_7^0-z_7^post2 == 0 /\ __disjvr_0^0-__disjvr_0^post2 == 0 /\ -tmp_8^post2 <= 0 /\ x_5^0-x_5^post2 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ tmp_8^post2 <= 0 /\ -__disjvr_2^post2+__disjvr_2^0 == 0 /\ -__disjvr_1^post2+__disjvr_1^0 == 0 /\ -result_4^post2+result_4^0 == 0 /\ -y_6^post2+y_6^0 == 0), cost: 1
	New rule:
	l2 -> l3 : __disjvr_0^0'=__disjvr_0^post2, __disjvr_1^0'=__disjvr_1^post2, __disjvr_2^0'=__disjvr_2^post2, result_4^0'=result_4^post2, tmp_8^0'=tmp_8^post2, x_5^0'=x_5^post2, y_6^0'=y_6^post2, z_7^0'=z_7^post2, (0 == 0 /\ z_7^0-z_7^post2 == 0 /\ __disjvr_0^0-__disjvr_0^post2 == 0 /\ -tmp_8^post2 <= 0 /\ -tmp_8^post2 == 0 /\ x_5^0-x_5^post2 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ tmp_8^post2 <= 0 /\ -__disjvr_2^post2+__disjvr_2^0 == 0 /\ -__disjvr_1^post2+__disjvr_1^0 == 0 /\ -result_4^post2+result_4^0 == 0 /\ -y_6^post2+y_6^0 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l3 : __disjvr_0^0'=__disjvr_0^post2, __disjvr_1^0'=__disjvr_1^post2, __disjvr_2^0'=__disjvr_2^post2, result_4^0'=result_4^post2, tmp_8^0'=tmp_8^post2, x_5^0'=x_5^post2, y_6^0'=y_6^post2, z_7^0'=z_7^post2, (0 == 0 /\ z_7^0-z_7^post2 == 0 /\ __disjvr_0^0-__disjvr_0^post2 == 0 /\ -tmp_8^post2 <= 0 /\ -tmp_8^post2 == 0 /\ x_5^0-x_5^post2 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ tmp_8^post2 <= 0 /\ -__disjvr_2^post2+__disjvr_2^0 == 0 /\ -__disjvr_1^post2+__disjvr_1^0 == 0 /\ -result_4^post2+result_4^0 == 0 /\ -y_6^post2+y_6^0 == 0), cost: 1
	New rule:
	l2 -> l3 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, (0 <= 0 /\ 0 == 0 /\ 1-z_7^0+y_6^0 <= 0), cost: 1
	
		propagated equality z_7^post2 = z_7^0
		
		propagated equality __disjvr_0^post2 = __disjvr_0^0
		
		propagated equality tmp_8^post2 = 0
		
		propagated equality x_5^post2 = x_5^0
		
		propagated equality __disjvr_2^post2 = __disjvr_2^0
		
		propagated equality __disjvr_1^post2 = __disjvr_1^0
		
		propagated equality result_4^post2 = result_4^0
		
		propagated equality y_6^post2 = y_6^0
		
	Simplified Guard

	Original rule:
	l2 -> l3 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, (0 <= 0 /\ 0 == 0 /\ 1-z_7^0+y_6^0 <= 0), cost: 1
	New rule:
	l2 -> l3 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, 1-z_7^0+y_6^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l3 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, 1-z_7^0+y_6^0 <= 0, cost: 1
	New rule:
	l2 -> l3 : tmp_8^0'=0, 1-z_7^0+y_6^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l1 : __disjvr_0^0'=__disjvr_0^post7, __disjvr_1^0'=__disjvr_1^post7, __disjvr_2^0'=__disjvr_2^post7, result_4^0'=result_4^post7, tmp_8^0'=tmp_8^post7, x_5^0'=x_5^post7, y_6^0'=y_6^post7, z_7^0'=z_7^post7, (tmp_8^0-tmp_8^post7 == 0 /\ -__disjvr_0^post7+__disjvr_0^0 == 0 /\ z_7^0-z_7^post7 == 0 /\ -1+x_5^post7-x_5^0 == 0 /\ z_7^0-y_6^0 <= 0 /\ __disjvr_2^0-__disjvr_2^post7 == 0 /\ -y_6^post7+y_6^0 == 0 /\ -result_4^post7+result_4^0 == 0 /\ -__disjvr_1^post7+__disjvr_1^0 == 0), cost: 1
	New rule:
	l2 -> l1 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_5^0'=1+x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, (0 == 0 /\ z_7^0-y_6^0 <= 0), cost: 1
	
		propagated equality tmp_8^post7 = tmp_8^0
		
		propagated equality __disjvr_0^post7 = __disjvr_0^0
		
		propagated equality z_7^post7 = z_7^0
		
		propagated equality x_5^post7 = 1+x_5^0
		
		propagated equality __disjvr_2^post7 = __disjvr_2^0
		
		propagated equality y_6^post7 = y_6^0
		
		propagated equality result_4^post7 = result_4^0
		
		propagated equality __disjvr_1^post7 = __disjvr_1^0
		
	Simplified Guard

	Original rule:
	l2 -> l1 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_5^0'=1+x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, (0 == 0 /\ z_7^0-y_6^0 <= 0), cost: 1
	New rule:
	l2 -> l1 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_5^0'=1+x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, z_7^0-y_6^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l1 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_5^0'=1+x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, z_7^0-y_6^0 <= 0, cost: 1
	New rule:
	l2 -> l1 : x_5^0'=1+x_5^0, z_7^0-y_6^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l7 : __disjvr_0^0'=__disjvr_0^post8, __disjvr_1^0'=__disjvr_1^post8, __disjvr_2^0'=__disjvr_2^post8, result_4^0'=result_4^post8, tmp_8^0'=tmp_8^post8, x_5^0'=x_5^post8, y_6^0'=y_6^post8, z_7^0'=z_7^post8, (-__disjvr_2^post8+__disjvr_2^0 == 0 /\ __disjvr_0^0-__disjvr_0^post8 == 0 /\ -result_4^post8+result_4^0 == 0 /\ 1-y_6^0+x_5^0 <= 0 /\ __disjvr_1^0-__disjvr_1^post8 == 0 /\ -tmp_8^post8+tmp_8^0 == 0 /\ y_6^0-y_6^post8 == 0 /\ z_7^0-z_7^post8 == 0 /\ -x_5^post8+x_5^0 == 0), cost: 1
	New rule:
	l1 -> l7 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, (0 == 0 /\ 1-y_6^0+x_5^0 <= 0), cost: 1
	
		propagated equality __disjvr_2^post8 = __disjvr_2^0
		
		propagated equality __disjvr_0^post8 = __disjvr_0^0
		
		propagated equality result_4^post8 = result_4^0
		
		propagated equality __disjvr_1^post8 = __disjvr_1^0
		
		propagated equality tmp_8^post8 = tmp_8^0
		
		propagated equality y_6^post8 = y_6^0
		
		propagated equality z_7^post8 = z_7^0
		
		propagated equality x_5^post8 = x_5^0
		
	Simplified Guard

	Original rule:
	l1 -> l7 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, (0 == 0 /\ 1-y_6^0+x_5^0 <= 0), cost: 1
	New rule:
	l1 -> l7 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, 1-y_6^0+x_5^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l7 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, 1-y_6^0+x_5^0 <= 0, cost: 1
	New rule:
	l1 -> l7 : 1-y_6^0+x_5^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l8 : __disjvr_0^0'=__disjvr_0^post9, __disjvr_1^0'=__disjvr_1^post9, __disjvr_2^0'=__disjvr_2^post9, result_4^0'=result_4^post9, tmp_8^0'=tmp_8^post9, x_5^0'=x_5^post9, y_6^0'=y_6^post9, z_7^0'=z_7^post9, (0 == 0 /\ tmp_8^0-tmp_8^post9 == 0 /\ y_6^0-x_5^0 <= 0 /\ -y_6^post9+y_6^0 == 0 /\ -__disjvr_1^post9+__disjvr_1^0 == 0 /\ -__disjvr_0^post9+__disjvr_0^0 == 0 /\ __disjvr_2^0-__disjvr_2^post9 == 0 /\ z_7^0-z_7^post9 == 0 /\ x_5^0-x_5^post9 == 0), cost: 1
	New rule:
	l1 -> l8 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^post9, tmp_8^0'=tmp_8^0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, (0 == 0 /\ y_6^0-x_5^0 <= 0), cost: 1
	
		propagated equality tmp_8^post9 = tmp_8^0
		
		propagated equality y_6^post9 = y_6^0
		
		propagated equality __disjvr_1^post9 = __disjvr_1^0
		
		propagated equality __disjvr_0^post9 = __disjvr_0^0
		
		propagated equality __disjvr_2^post9 = __disjvr_2^0
		
		propagated equality z_7^post9 = z_7^0
		
		propagated equality x_5^post9 = x_5^0
		
	Simplified Guard

	Original rule:
	l1 -> l8 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^post9, tmp_8^0'=tmp_8^0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, (0 == 0 /\ y_6^0-x_5^0 <= 0), cost: 1
	New rule:
	l1 -> l8 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^post9, tmp_8^0'=tmp_8^0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, y_6^0-x_5^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l8 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^post9, tmp_8^0'=tmp_8^0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, y_6^0-x_5^0 <= 0, cost: 1
	New rule:
	l1 -> l8 : result_4^0'=result_4^post9, y_6^0-x_5^0 <= 0, cost: 1
	
	made implied equalities explicit

	Original rule:
	l7 -> l3 : __disjvr_0^0'=__disjvr_0^post10, __disjvr_1^0'=__disjvr_1^post10, __disjvr_2^0'=__disjvr_2^post10, result_4^0'=result_4^post10, tmp_8^0'=tmp_8^post10, x_5^0'=x_5^post10, y_6^0'=y_6^post10, z_7^0'=z_7^post10, (0 == 0 /\ -x_5^post10+x_5^0 == 0 /\ y_6^0-y_6^post10 == 0 /\ __disjvr_0^0-__disjvr_0^post10 == 0 /\ -__disjvr_2^post10+__disjvr_2^0 == 0 /\ z_7^0-z_7^post10 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -tmp_8^post10 <= 0 /\ -result_4^post10+result_4^0 == 0 /\ tmp_8^post10 <= 0 /\ -__disjvr_1^post10+__disjvr_1^0 == 0), cost: 1
	New rule:
	l7 -> l3 : __disjvr_0^0'=__disjvr_0^post10, __disjvr_1^0'=__disjvr_1^post10, __disjvr_2^0'=__disjvr_2^post10, result_4^0'=result_4^post10, tmp_8^0'=tmp_8^post10, x_5^0'=x_5^post10, y_6^0'=y_6^post10, z_7^0'=z_7^post10, (0 == 0 /\ -x_5^post10+x_5^0 == 0 /\ y_6^0-y_6^post10 == 0 /\ __disjvr_0^0-__disjvr_0^post10 == 0 /\ -__disjvr_2^post10+__disjvr_2^0 == 0 /\ z_7^0-z_7^post10 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -tmp_8^post10 <= 0 /\ -tmp_8^post10 == 0 /\ -result_4^post10+result_4^0 == 0 /\ tmp_8^post10 <= 0 /\ -__disjvr_1^post10+__disjvr_1^0 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l3 : __disjvr_0^0'=__disjvr_0^post10, __disjvr_1^0'=__disjvr_1^post10, __disjvr_2^0'=__disjvr_2^post10, result_4^0'=result_4^post10, tmp_8^0'=tmp_8^post10, x_5^0'=x_5^post10, y_6^0'=y_6^post10, z_7^0'=z_7^post10, (0 == 0 /\ -x_5^post10+x_5^0 == 0 /\ y_6^0-y_6^post10 == 0 /\ __disjvr_0^0-__disjvr_0^post10 == 0 /\ -__disjvr_2^post10+__disjvr_2^0 == 0 /\ z_7^0-z_7^post10 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -tmp_8^post10 <= 0 /\ -tmp_8^post10 == 0 /\ -result_4^post10+result_4^0 == 0 /\ tmp_8^post10 <= 0 /\ -__disjvr_1^post10+__disjvr_1^0 == 0), cost: 1
	New rule:
	l7 -> l3 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, (0 <= 0 /\ 0 == 0 /\ 1-z_7^0+y_6^0 <= 0), cost: 1
	
		propagated equality x_5^post10 = x_5^0
		
		propagated equality y_6^post10 = y_6^0
		
		propagated equality __disjvr_0^post10 = __disjvr_0^0
		
		propagated equality __disjvr_2^post10 = __disjvr_2^0
		
		propagated equality z_7^post10 = z_7^0
		
		propagated equality tmp_8^post10 = 0
		
		propagated equality result_4^post10 = result_4^0
		
		propagated equality __disjvr_1^post10 = __disjvr_1^0
		
	Simplified Guard

	Original rule:
	l7 -> l3 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, (0 <= 0 /\ 0 == 0 /\ 1-z_7^0+y_6^0 <= 0), cost: 1
	New rule:
	l7 -> l3 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, 1-z_7^0+y_6^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l7 -> l3 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, 1-z_7^0+y_6^0 <= 0, cost: 1
	New rule:
	l7 -> l3 : tmp_8^0'=0, 1-z_7^0+y_6^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l1 : __disjvr_0^0'=__disjvr_0^post14, __disjvr_1^0'=__disjvr_1^post14, __disjvr_2^0'=__disjvr_2^post14, result_4^0'=result_4^post14, tmp_8^0'=tmp_8^post14, x_5^0'=x_5^post14, y_6^0'=y_6^post14, z_7^0'=z_7^post14, (__disjvr_1^0-__disjvr_1^post14 == 0 /\ z_7^0-z_7^post14 == 0 /\ -result_4^post14+result_4^0 == 0 /\ __disjvr_0^0-__disjvr_0^post14 == 0 /\ y_6^0-y_6^post14 == 0 /\ tmp_8^0-tmp_8^post14 == 0 /\ -1+x_5^post14-x_5^0 == 0 /\ z_7^0-y_6^0 <= 0 /\ -__disjvr_2^post14+__disjvr_2^0 == 0), cost: 1
	New rule:
	l7 -> l1 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_5^0'=1+x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, (0 == 0 /\ z_7^0-y_6^0 <= 0), cost: 1
	
		propagated equality __disjvr_1^post14 = __disjvr_1^0
		
		propagated equality z_7^post14 = z_7^0
		
		propagated equality result_4^post14 = result_4^0
		
		propagated equality __disjvr_0^post14 = __disjvr_0^0
		
		propagated equality y_6^post14 = y_6^0
		
		propagated equality tmp_8^post14 = tmp_8^0
		
		propagated equality x_5^post14 = 1+x_5^0
		
		propagated equality __disjvr_2^post14 = __disjvr_2^0
		
	Simplified Guard

	Original rule:
	l7 -> l1 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_5^0'=1+x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, (0 == 0 /\ z_7^0-y_6^0 <= 0), cost: 1
	New rule:
	l7 -> l1 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_5^0'=1+x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, z_7^0-y_6^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l7 -> l1 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_5^0'=1+x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, z_7^0-y_6^0 <= 0, cost: 1
	New rule:
	l7 -> l1 : x_5^0'=1+x_5^0, z_7^0-y_6^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l14 -> l1 : __disjvr_0^0'=__disjvr_0^post1, __disjvr_1^0'=__disjvr_1^post1, __disjvr_2^0'=__disjvr_2^post1, result_4^0'=result_4^post1, tmp_8^0'=tmp_8^post1, x_5^0'=x_5^post1, y_6^0'=y_6^post1, z_7^0'=z_7^post1, (-z_7^post20+z_7^0 == 0 /\ z_7^post20-z_7^post1 == 0 /\ result_4^post20-result_4^post1 == 0 /\ y_6^0-y_6^post20 == 0 /\ tmp_8^post20-tmp_8^post1 == 0 /\ -x_5^post20+x_5^0 == 0 /\ x_5^post20-x_5^post1 == 0 /\ -__disjvr_0^post1+__disjvr_0^post20 == 0 /\ -__disjvr_1^post20+__disjvr_1^0 == 0 /\ y_6^post20-y_6^post1 == 0 /\ result_4^0-result_4^post20 == 0 /\ __disjvr_1^post20-__disjvr_1^post1 == 0 /\ -__disjvr_2^post20+__disjvr_2^0 == 0 /\ __disjvr_2^post20-__disjvr_2^post1 == 0 /\ __disjvr_0^0-__disjvr_0^post20 == 0 /\ -tmp_8^post20+tmp_8^0 == 0), cost: 1
	New rule:
	l14 -> l1 : __disjvr_0^0'=__disjvr_0^post20, __disjvr_1^0'=__disjvr_1^post20, __disjvr_2^0'=__disjvr_2^post20, result_4^0'=result_4^post20, tmp_8^0'=tmp_8^post20, x_5^0'=x_5^post20, y_6^0'=y_6^post20, z_7^0'=z_7^post20, (0 == 0 /\ -z_7^post20+z_7^0 == 0 /\ y_6^0-y_6^post20 == 0 /\ -x_5^post20+x_5^0 == 0 /\ -__disjvr_1^post20+__disjvr_1^0 == 0 /\ result_4^0-result_4^post20 == 0 /\ -__disjvr_2^post20+__disjvr_2^0 == 0 /\ __disjvr_0^0-__disjvr_0^post20 == 0 /\ -tmp_8^post20+tmp_8^0 == 0), cost: 1
	
		propagated equality z_7^post1 = z_7^post20
		
		propagated equality result_4^post1 = result_4^post20
		
		propagated equality tmp_8^post1 = tmp_8^post20
		
		propagated equality x_5^post1 = x_5^post20
		
		propagated equality __disjvr_0^post1 = __disjvr_0^post20
		
		propagated equality y_6^post1 = y_6^post20
		
		propagated equality __disjvr_1^post1 = __disjvr_1^post20
		
		propagated equality __disjvr_2^post1 = __disjvr_2^post20
		
	Propagated Equalities

	Original rule:
	l14 -> l1 : __disjvr_0^0'=__disjvr_0^post20, __disjvr_1^0'=__disjvr_1^post20, __disjvr_2^0'=__disjvr_2^post20, result_4^0'=result_4^post20, tmp_8^0'=tmp_8^post20, x_5^0'=x_5^post20, y_6^0'=y_6^post20, z_7^0'=z_7^post20, (0 == 0 /\ -z_7^post20+z_7^0 == 0 /\ y_6^0-y_6^post20 == 0 /\ -x_5^post20+x_5^0 == 0 /\ -__disjvr_1^post20+__disjvr_1^0 == 0 /\ result_4^0-result_4^post20 == 0 /\ -__disjvr_2^post20+__disjvr_2^0 == 0 /\ __disjvr_0^0-__disjvr_0^post20 == 0 /\ -tmp_8^post20+tmp_8^0 == 0), cost: 1
	New rule:
	l14 -> l1 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, 0 == 0, cost: 1
	
		propagated equality z_7^post20 = z_7^0
		
		propagated equality y_6^post20 = y_6^0
		
		propagated equality x_5^post20 = x_5^0
		
		propagated equality __disjvr_1^post20 = __disjvr_1^0
		
		propagated equality result_4^post20 = result_4^0
		
		propagated equality __disjvr_2^post20 = __disjvr_2^0
		
		propagated equality __disjvr_0^post20 = __disjvr_0^0
		
		propagated equality tmp_8^post20 = tmp_8^0
		
	Simplified Guard

	Original rule:
	l14 -> l1 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, 0 == 0, cost: 1
	New rule:
	l14 -> l1 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l14 -> l1 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, T, cost: 1
	New rule:
	l14 -> l1 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l2 : __disjvr_0^0'=__disjvr_0^post13, __disjvr_1^0'=__disjvr_1^post13, __disjvr_2^0'=__disjvr_2^post13, result_4^0'=result_4^post13, tmp_8^0'=tmp_8^post13, x_5^0'=x_5^post13, y_6^0'=y_6^post13, z_7^0'=z_7^post13, (0 == 0 /\ -__disjvr_1^post11+__disjvr_1^post12 == 0 /\ y_6^0-y_6^post11 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ __disjvr_0^post11-__disjvr_0^post12 == 0 /\ -x_5^post11+x_5^0 == 0 /\ __disjvr_1^post11-__disjvr_1^post12 == 0 /\ -__disjvr_1^post13+__disjvr_1^post12 == 0 /\ __disjvr_2^post12-__disjvr_2^post13 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ -tmp_8^post13+tmp_8^post12 == 0 /\ -x_5^post12+x_5^post11 == 0 /\ z_7^0-z_7^post11 == 0 /\ result_4^post11-result_4^post12 == 0 /\ -result_4^post13+result_4^post12 == 0 /\ -__disjvr_0^post13+__disjvr_0^post12 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -z_7^post13+z_7^post12 == 0 /\ -1+y_6^post13-y_6^post12 == 0 /\ z_7^post11-z_7^post12 == 0 /\ -y_6^post12+y_6^post11 == 0 /\ x_5^post12-x_5^post13 == 0 /\ -__disjvr_0^post11+__disjvr_0^0 == 0 /\ -__disjvr_2^post12+__disjvr_2^post11 == 0 /\ tmp_8^post11-tmp_8^post12 == 0), cost: 1
	New rule:
	l7 -> l2 : __disjvr_0^0'=__disjvr_0^post12, __disjvr_1^0'=__disjvr_1^post12, __disjvr_2^0'=__disjvr_2^post12, result_4^0'=result_4^post12, tmp_8^0'=tmp_8^post12, x_5^0'=x_5^post12, y_6^0'=1+y_6^post12, z_7^0'=z_7^post12, (0 == 0 /\ -__disjvr_1^post11+__disjvr_1^post12 == 0 /\ y_6^0-y_6^post11 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ __disjvr_0^post11-__disjvr_0^post12 == 0 /\ -x_5^post11+x_5^0 == 0 /\ __disjvr_1^post11-__disjvr_1^post12 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ -x_5^post12+x_5^post11 == 0 /\ z_7^0-z_7^post11 == 0 /\ result_4^post11-result_4^post12 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ z_7^post11-z_7^post12 == 0 /\ -y_6^post12+y_6^post11 == 0 /\ -__disjvr_0^post11+__disjvr_0^0 == 0 /\ -__disjvr_2^post12+__disjvr_2^post11 == 0 /\ tmp_8^post11-tmp_8^post12 == 0), cost: 1
	
		propagated equality __disjvr_1^post13 = __disjvr_1^post12
		
		propagated equality __disjvr_2^post13 = __disjvr_2^post12
		
		propagated equality tmp_8^post13 = tmp_8^post12
		
		propagated equality result_4^post13 = result_4^post12
		
		propagated equality __disjvr_0^post13 = __disjvr_0^post12
		
		propagated equality z_7^post13 = z_7^post12
		
		propagated equality y_6^post13 = 1+y_6^post12
		
		propagated equality x_5^post13 = x_5^post12
		
	Propagated Equalities

	Original rule:
	l7 -> l2 : __disjvr_0^0'=__disjvr_0^post12, __disjvr_1^0'=__disjvr_1^post12, __disjvr_2^0'=__disjvr_2^post12, result_4^0'=result_4^post12, tmp_8^0'=tmp_8^post12, x_5^0'=x_5^post12, y_6^0'=1+y_6^post12, z_7^0'=z_7^post12, (0 == 0 /\ -__disjvr_1^post11+__disjvr_1^post12 == 0 /\ y_6^0-y_6^post11 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ __disjvr_0^post11-__disjvr_0^post12 == 0 /\ -x_5^post11+x_5^0 == 0 /\ __disjvr_1^post11-__disjvr_1^post12 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ -x_5^post12+x_5^post11 == 0 /\ z_7^0-z_7^post11 == 0 /\ result_4^post11-result_4^post12 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ z_7^post11-z_7^post12 == 0 /\ -y_6^post12+y_6^post11 == 0 /\ -__disjvr_0^post11+__disjvr_0^0 == 0 /\ -__disjvr_2^post12+__disjvr_2^post11 == 0 /\ tmp_8^post11-tmp_8^post12 == 0), cost: 1
	New rule:
	l7 -> l2 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^post12, x_5^0'=x_5^0, y_6^0'=1+y_6^0, z_7^0'=z_7^0, (0 == 0 /\ 1-z_7^0+y_6^0 <= 0), cost: 1
	
		propagated equality __disjvr_1^post11 = __disjvr_1^post12
		
		propagated equality y_6^post11 = y_6^0
		
		propagated equality __disjvr_2^post11 = __disjvr_2^0
		
		propagated equality __disjvr_0^post11 = __disjvr_0^post12
		
		propagated equality x_5^post11 = x_5^0
		
		propagated equality result_4^post11 = result_4^0
		
		propagated equality __disjvr_1^post12 = __disjvr_1^0
		
		propagated equality x_5^post12 = x_5^0
		
		propagated equality z_7^post11 = z_7^0
		
		propagated equality result_4^post12 = result_4^0
		
		propagated equality z_7^post12 = z_7^0
		
		propagated equality y_6^post12 = y_6^0
		
		propagated equality __disjvr_0^post12 = __disjvr_0^0
		
		propagated equality __disjvr_2^post12 = __disjvr_2^0
		
		propagated equality tmp_8^post11 = tmp_8^post12
		
	Simplified Guard

	Original rule:
	l7 -> l2 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^post12, x_5^0'=x_5^0, y_6^0'=1+y_6^0, z_7^0'=z_7^0, (0 == 0 /\ 1-z_7^0+y_6^0 <= 0), cost: 1
	New rule:
	l7 -> l2 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^post12, x_5^0'=x_5^0, y_6^0'=1+y_6^0, z_7^0'=z_7^0, 1-z_7^0+y_6^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l7 -> l2 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^post12, x_5^0'=x_5^0, y_6^0'=1+y_6^0, z_7^0'=z_7^0, 1-z_7^0+y_6^0 <= 0, cost: 1
	New rule:
	l7 -> l2 : tmp_8^0'=tmp_8^post12, y_6^0'=1+y_6^0, 1-z_7^0+y_6^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l2 : __disjvr_0^0'=__disjvr_0^post6, __disjvr_1^0'=__disjvr_1^post6, __disjvr_2^0'=__disjvr_2^post6, result_4^0'=result_4^post6, tmp_8^0'=tmp_8^post6, x_5^0'=x_5^post6, y_6^0'=y_6^post6, z_7^0'=z_7^post6, (0 == 0 /\ -x_5^post3+x_5^0 == 0 /\ tmp_8^post5-tmp_8^post6 == 0 /\ x_5^post3-x_5^post4 == 0 /\ -z_7^post3+z_7^0 == 0 /\ -x_5^post5+x_5^post4 == 0 /\ -__disjvr_2^post6+__disjvr_2^post5 == 0 /\ -__disjvr_1^post3+__disjvr_1^0 == 0 /\ -1-y_6^post4+y_6^post5 == 0 /\ -z_7^post5+z_7^post4 == 0 /\ result_4^0-result_4^post3 == 0 /\ -__disjvr_0^post6+__disjvr_0^post5 == 0 /\ tmp_8^post3-tmp_8^post4 == 0 /\ -y_6^post4+y_6^post3 == 0 /\ z_7^post3-z_7^post4 == 0 /\ __disjvr_2^post3-__disjvr_2^post4 == 0 /\ -__disjvr_1^post5+__disjvr_1^post4 == 0 /\ __disjvr_0^post4-__disjvr_0^post3 == 0 /\ y_6^0-y_6^post3 == 0 /\ __disjvr_1^post3-__disjvr_1^post4 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -result_4^post4+result_4^post3 == 0 /\ result_4^post4-result_4^post5 == 0 /\ -__disjvr_0^post4+__disjvr_0^post3 == 0 /\ -x_5^post6+x_5^post5 == 0 /\ -__disjvr_2^post3+__disjvr_2^0 == 0 /\ -result_4^post6+result_4^post5 == 0 /\ __disjvr_1^post5-__disjvr_1^post6 == 0 /\ __disjvr_0^post4-__disjvr_0^post5 == 0 /\ -tmp_8^post5+tmp_8^post4 == 0 /\ -__disjvr_2^post5+__disjvr_2^post4 == 0 /\ __disjvr_0^0-__disjvr_0^post3 == 0 /\ z_7^post5-z_7^post6 == 0 /\ -y_6^post6+y_6^post5 == 0), cost: 1
	New rule:
	l2 -> l2 : __disjvr_0^0'=__disjvr_0^post5, __disjvr_1^0'=__disjvr_1^post5, __disjvr_2^0'=__disjvr_2^post5, result_4^0'=result_4^post5, tmp_8^0'=tmp_8^post5, x_5^0'=x_5^post5, y_6^0'=y_6^post5, z_7^0'=z_7^post5, (0 == 0 /\ -x_5^post3+x_5^0 == 0 /\ x_5^post3-x_5^post4 == 0 /\ -z_7^post3+z_7^0 == 0 /\ -x_5^post5+x_5^post4 == 0 /\ -__disjvr_1^post3+__disjvr_1^0 == 0 /\ -1-y_6^post4+y_6^post5 == 0 /\ -z_7^post5+z_7^post4 == 0 /\ result_4^0-result_4^post3 == 0 /\ tmp_8^post3-tmp_8^post4 == 0 /\ -y_6^post4+y_6^post3 == 0 /\ z_7^post3-z_7^post4 == 0 /\ __disjvr_2^post3-__disjvr_2^post4 == 0 /\ -__disjvr_1^post5+__disjvr_1^post4 == 0 /\ __disjvr_0^post4-__disjvr_0^post3 == 0 /\ y_6^0-y_6^post3 == 0 /\ __disjvr_1^post3-__disjvr_1^post4 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -result_4^post4+result_4^post3 == 0 /\ result_4^post4-result_4^post5 == 0 /\ -__disjvr_0^post4+__disjvr_0^post3 == 0 /\ -__disjvr_2^post3+__disjvr_2^0 == 0 /\ __disjvr_0^post4-__disjvr_0^post5 == 0 /\ -tmp_8^post5+tmp_8^post4 == 0 /\ -__disjvr_2^post5+__disjvr_2^post4 == 0 /\ __disjvr_0^0-__disjvr_0^post3 == 0), cost: 1
	
		propagated equality tmp_8^post6 = tmp_8^post5
		
		propagated equality __disjvr_2^post6 = __disjvr_2^post5
		
		propagated equality __disjvr_0^post6 = __disjvr_0^post5
		
		propagated equality x_5^post6 = x_5^post5
		
		propagated equality result_4^post6 = result_4^post5
		
		propagated equality __disjvr_1^post6 = __disjvr_1^post5
		
		propagated equality z_7^post6 = z_7^post5
		
		propagated equality y_6^post6 = y_6^post5
		
	Propagated Equalities

	Original rule:
	l2 -> l2 : __disjvr_0^0'=__disjvr_0^post5, __disjvr_1^0'=__disjvr_1^post5, __disjvr_2^0'=__disjvr_2^post5, result_4^0'=result_4^post5, tmp_8^0'=tmp_8^post5, x_5^0'=x_5^post5, y_6^0'=y_6^post5, z_7^0'=z_7^post5, (0 == 0 /\ -x_5^post3+x_5^0 == 0 /\ x_5^post3-x_5^post4 == 0 /\ -z_7^post3+z_7^0 == 0 /\ -x_5^post5+x_5^post4 == 0 /\ -__disjvr_1^post3+__disjvr_1^0 == 0 /\ -1-y_6^post4+y_6^post5 == 0 /\ -z_7^post5+z_7^post4 == 0 /\ result_4^0-result_4^post3 == 0 /\ tmp_8^post3-tmp_8^post4 == 0 /\ -y_6^post4+y_6^post3 == 0 /\ z_7^post3-z_7^post4 == 0 /\ __disjvr_2^post3-__disjvr_2^post4 == 0 /\ -__disjvr_1^post5+__disjvr_1^post4 == 0 /\ __disjvr_0^post4-__disjvr_0^post3 == 0 /\ y_6^0-y_6^post3 == 0 /\ __disjvr_1^post3-__disjvr_1^post4 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -result_4^post4+result_4^post3 == 0 /\ result_4^post4-result_4^post5 == 0 /\ -__disjvr_0^post4+__disjvr_0^post3 == 0 /\ -__disjvr_2^post3+__disjvr_2^0 == 0 /\ __disjvr_0^post4-__disjvr_0^post5 == 0 /\ -tmp_8^post5+tmp_8^post4 == 0 /\ -__disjvr_2^post5+__disjvr_2^post4 == 0 /\ __disjvr_0^0-__disjvr_0^post3 == 0), cost: 1
	New rule:
	l2 -> l2 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^post5, x_5^0'=x_5^0, y_6^0'=1+y_6^0, z_7^0'=z_7^0, (0 == 0 /\ 1-z_7^0+y_6^0 <= 0), cost: 1
	
		propagated equality x_5^post3 = x_5^0
		
		propagated equality x_5^post4 = x_5^0
		
		propagated equality z_7^post3 = z_7^0
		
		propagated equality x_5^post5 = x_5^0
		
		propagated equality __disjvr_1^post3 = __disjvr_1^0
		
		propagated equality y_6^post4 = -1+y_6^post5
		
		propagated equality z_7^post4 = z_7^post5
		
		propagated equality result_4^post3 = result_4^0
		
		propagated equality tmp_8^post3 = tmp_8^post4
		
		propagated equality y_6^post3 = -1+y_6^post5
		
		propagated equality z_7^post5 = z_7^0
		
		propagated equality __disjvr_2^post3 = __disjvr_2^post4
		
		propagated equality __disjvr_1^post4 = __disjvr_1^post5
		
		propagated equality __disjvr_0^post3 = __disjvr_0^post4
		
		propagated equality y_6^post5 = 1+y_6^0
		
		propagated equality __disjvr_1^post5 = __disjvr_1^0
		
		propagated equality result_4^post4 = result_4^0
		
		propagated equality result_4^post5 = result_4^0
		
		propagated equality __disjvr_2^post4 = __disjvr_2^0
		
		propagated equality __disjvr_0^post4 = __disjvr_0^post5
		
		propagated equality tmp_8^post4 = tmp_8^post5
		
		propagated equality __disjvr_2^post5 = __disjvr_2^0
		
		propagated equality __disjvr_0^post5 = __disjvr_0^0
		
	Simplified Guard

	Original rule:
	l2 -> l2 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^post5, x_5^0'=x_5^0, y_6^0'=1+y_6^0, z_7^0'=z_7^0, (0 == 0 /\ 1-z_7^0+y_6^0 <= 0), cost: 1
	New rule:
	l2 -> l2 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^post5, x_5^0'=x_5^0, y_6^0'=1+y_6^0, z_7^0'=z_7^0, 1-z_7^0+y_6^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l2 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^post5, x_5^0'=x_5^0, y_6^0'=1+y_6^0, z_7^0'=z_7^0, 1-z_7^0+y_6^0 <= 0, cost: 1
	New rule:
	l2 -> l2 : tmp_8^0'=tmp_8^post5, y_6^0'=1+y_6^0, 1-z_7^0+y_6^0 <= 0, cost: 1
	
	made implied equalities explicit

	Original rule:
	l3 -> l3 : __disjvr_0^0'=__disjvr_0^post16, __disjvr_1^0'=__disjvr_1^post16, __disjvr_2^0'=__disjvr_2^post16, result_4^0'=result_4^post16, tmp_8^0'=tmp_8^post16, x_5^0'=x_5^post16, y_6^0'=y_6^post16, z_7^0'=z_7^post16, (0 == 0 /\ -__disjvr_2^post15+__disjvr_2^0 == 0 /\ -__disjvr_1^post15+__disjvr_1^0 == 0 /\ -result_4^post15+result_4^0 == 0 /\ __disjvr_0^post15-__disjvr_0^post16 == 0 /\ z_7^0-z_7^post15 == 0 /\ __disjvr_2^post15-__disjvr_2^post16 == 0 /\ -tmp_8^post15 <= 0 /\ -__disjvr_1^post16+__disjvr_1^post15 == 0 /\ -tmp_8^post16+tmp_8^post15 == 0 /\ __disjvr_0^0-__disjvr_0^post15 == 0 /\ x_5^0-x_5^post15 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ result_4^post15-result_4^post16 == 0 /\ tmp_8^post15 <= 0 /\ -z_7^post16+z_7^post15 == 0 /\ y_6^post15-y_6^post16 == 0 /\ -x_5^post16+x_5^post15 == 0 /\ -y_6^post15+y_6^0 == 0), cost: 1
	New rule:
	l3 -> l3 : __disjvr_0^0'=__disjvr_0^post16, __disjvr_1^0'=__disjvr_1^post16, __disjvr_2^0'=__disjvr_2^post16, result_4^0'=result_4^post16, tmp_8^0'=tmp_8^post16, x_5^0'=x_5^post16, y_6^0'=y_6^post16, z_7^0'=z_7^post16, (0 == 0 /\ -__disjvr_2^post15+__disjvr_2^0 == 0 /\ -__disjvr_1^post15+__disjvr_1^0 == 0 /\ -result_4^post15+result_4^0 == 0 /\ __disjvr_0^post15-__disjvr_0^post16 == 0 /\ z_7^0-z_7^post15 == 0 /\ __disjvr_2^post15-__disjvr_2^post16 == 0 /\ -tmp_8^post15 <= 0 /\ -tmp_8^post15 == 0 /\ -__disjvr_1^post16+__disjvr_1^post15 == 0 /\ -tmp_8^post16+tmp_8^post15 == 0 /\ __disjvr_0^0-__disjvr_0^post15 == 0 /\ x_5^0-x_5^post15 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ result_4^post15-result_4^post16 == 0 /\ tmp_8^post15 <= 0 /\ -z_7^post16+z_7^post15 == 0 /\ y_6^post15-y_6^post16 == 0 /\ -x_5^post16+x_5^post15 == 0 /\ -y_6^post15+y_6^0 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l3 : __disjvr_0^0'=__disjvr_0^post16, __disjvr_1^0'=__disjvr_1^post16, __disjvr_2^0'=__disjvr_2^post16, result_4^0'=result_4^post16, tmp_8^0'=tmp_8^post16, x_5^0'=x_5^post16, y_6^0'=y_6^post16, z_7^0'=z_7^post16, (0 == 0 /\ -__disjvr_2^post15+__disjvr_2^0 == 0 /\ -__disjvr_1^post15+__disjvr_1^0 == 0 /\ -result_4^post15+result_4^0 == 0 /\ __disjvr_0^post15-__disjvr_0^post16 == 0 /\ z_7^0-z_7^post15 == 0 /\ __disjvr_2^post15-__disjvr_2^post16 == 0 /\ -tmp_8^post15 <= 0 /\ -tmp_8^post15 == 0 /\ -__disjvr_1^post16+__disjvr_1^post15 == 0 /\ -tmp_8^post16+tmp_8^post15 == 0 /\ __disjvr_0^0-__disjvr_0^post15 == 0 /\ x_5^0-x_5^post15 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ result_4^post15-result_4^post16 == 0 /\ tmp_8^post15 <= 0 /\ -z_7^post16+z_7^post15 == 0 /\ y_6^post15-y_6^post16 == 0 /\ -x_5^post16+x_5^post15 == 0 /\ -y_6^post15+y_6^0 == 0), cost: 1
	New rule:
	l3 -> l3 : __disjvr_0^0'=__disjvr_0^post15, __disjvr_1^0'=__disjvr_1^post15, __disjvr_2^0'=__disjvr_2^post15, result_4^0'=result_4^post15, tmp_8^0'=tmp_8^post15, x_5^0'=x_5^post15, y_6^0'=y_6^post15, z_7^0'=z_7^post15, (0 == 0 /\ -__disjvr_2^post15+__disjvr_2^0 == 0 /\ -__disjvr_1^post15+__disjvr_1^0 == 0 /\ -result_4^post15+result_4^0 == 0 /\ z_7^0-z_7^post15 == 0 /\ -tmp_8^post15 <= 0 /\ -tmp_8^post15 == 0 /\ __disjvr_0^0-__disjvr_0^post15 == 0 /\ x_5^0-x_5^post15 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ tmp_8^post15 <= 0 /\ -y_6^post15+y_6^0 == 0), cost: 1
	
		propagated equality __disjvr_0^post16 = __disjvr_0^post15
		
		propagated equality __disjvr_2^post16 = __disjvr_2^post15
		
		propagated equality __disjvr_1^post16 = __disjvr_1^post15
		
		propagated equality tmp_8^post16 = tmp_8^post15
		
		propagated equality result_4^post16 = result_4^post15
		
		propagated equality z_7^post16 = z_7^post15
		
		propagated equality y_6^post16 = y_6^post15
		
		propagated equality x_5^post16 = x_5^post15
		
	Propagated Equalities

	Original rule:
	l3 -> l3 : __disjvr_0^0'=__disjvr_0^post15, __disjvr_1^0'=__disjvr_1^post15, __disjvr_2^0'=__disjvr_2^post15, result_4^0'=result_4^post15, tmp_8^0'=tmp_8^post15, x_5^0'=x_5^post15, y_6^0'=y_6^post15, z_7^0'=z_7^post15, (0 == 0 /\ -__disjvr_2^post15+__disjvr_2^0 == 0 /\ -__disjvr_1^post15+__disjvr_1^0 == 0 /\ -result_4^post15+result_4^0 == 0 /\ z_7^0-z_7^post15 == 0 /\ -tmp_8^post15 <= 0 /\ -tmp_8^post15 == 0 /\ __disjvr_0^0-__disjvr_0^post15 == 0 /\ x_5^0-x_5^post15 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ tmp_8^post15 <= 0 /\ -y_6^post15+y_6^0 == 0), cost: 1
	New rule:
	l3 -> l3 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, (0 <= 0 /\ 0 == 0 /\ 1-z_7^0+y_6^0 <= 0), cost: 1
	
		propagated equality __disjvr_2^post15 = __disjvr_2^0
		
		propagated equality __disjvr_1^post15 = __disjvr_1^0
		
		propagated equality result_4^post15 = result_4^0
		
		propagated equality z_7^post15 = z_7^0
		
		propagated equality tmp_8^post15 = 0
		
		propagated equality __disjvr_0^post15 = __disjvr_0^0
		
		propagated equality x_5^post15 = x_5^0
		
		propagated equality y_6^post15 = y_6^0
		
	Simplified Guard

	Original rule:
	l3 -> l3 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, (0 <= 0 /\ 0 == 0 /\ 1-z_7^0+y_6^0 <= 0), cost: 1
	New rule:
	l3 -> l3 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, 1-z_7^0+y_6^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l3 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=0, x_5^0'=x_5^0, y_6^0'=y_6^0, z_7^0'=z_7^0, 1-z_7^0+y_6^0 <= 0, cost: 1
	New rule:
	l3 -> l3 : tmp_8^0'=0, 1-z_7^0+y_6^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l2 : __disjvr_0^0'=__disjvr_0^post19, __disjvr_1^0'=__disjvr_1^post19, __disjvr_2^0'=__disjvr_2^post19, result_4^0'=result_4^post19, tmp_8^0'=tmp_8^post19, x_5^0'=x_5^post19, y_6^0'=y_6^post19, z_7^0'=z_7^post19, (0 == 0 /\ result_4^post17-result_4^post18 == 0 /\ -result_4^post19+result_4^post18 == 0 /\ -tmp_8^post18+tmp_8^post17 == 0 /\ __disjvr_2^post17-__disjvr_2^post18 == 0 /\ tmp_8^post18-tmp_8^post19 == 0 /\ z_7^0-z_7^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ x_5^post18-x_5^post19 == 0 /\ __disjvr_1^post18-__disjvr_1^post19 == 0 /\ y_6^post17-y_6^post18 == 0 /\ __disjvr_0^post17-__disjvr_0^post18 == 0 /\ -__disjvr_2^post17+__disjvr_2^post18 == 0 /\ -z_7^post18+z_7^post17 == 0 /\ -1+y_6^post19-y_6^post18 == 0 /\ -__disjvr_0^post19+__disjvr_0^post18 == 0 /\ z_7^post18-z_7^post19 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -x_5^post17+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ x_5^post17-x_5^post18 == 0 /\ -y_6^post17+y_6^0 == 0 /\ -__disjvr_1^post18+__disjvr_1^post17 == 0 /\ -result_4^post17+result_4^0 == 0 /\ -__disjvr_1^post17+__disjvr_1^0 == 0 /\ __disjvr_2^post18-__disjvr_2^post19 == 0), cost: 1
	New rule:
	l3 -> l2 : __disjvr_0^0'=__disjvr_0^post18, __disjvr_1^0'=__disjvr_1^post18, __disjvr_2^0'=__disjvr_2^post18, result_4^0'=result_4^post18, tmp_8^0'=tmp_8^post18, x_5^0'=x_5^post18, y_6^0'=1+y_6^post18, z_7^0'=z_7^post18, (0 == 0 /\ result_4^post17-result_4^post18 == 0 /\ -tmp_8^post18+tmp_8^post17 == 0 /\ __disjvr_2^post17-__disjvr_2^post18 == 0 /\ z_7^0-z_7^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ y_6^post17-y_6^post18 == 0 /\ __disjvr_0^post17-__disjvr_0^post18 == 0 /\ -__disjvr_2^post17+__disjvr_2^post18 == 0 /\ -z_7^post18+z_7^post17 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -x_5^post17+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ x_5^post17-x_5^post18 == 0 /\ -y_6^post17+y_6^0 == 0 /\ -__disjvr_1^post18+__disjvr_1^post17 == 0 /\ -result_4^post17+result_4^0 == 0 /\ -__disjvr_1^post17+__disjvr_1^0 == 0), cost: 1
	
		propagated equality result_4^post19 = result_4^post18
		
		propagated equality tmp_8^post19 = tmp_8^post18
		
		propagated equality x_5^post19 = x_5^post18
		
		propagated equality __disjvr_1^post19 = __disjvr_1^post18
		
		propagated equality y_6^post19 = 1+y_6^post18
		
		propagated equality __disjvr_0^post19 = __disjvr_0^post18
		
		propagated equality z_7^post19 = z_7^post18
		
		propagated equality __disjvr_2^post19 = __disjvr_2^post18
		
	Propagated Equalities

	Original rule:
	l3 -> l2 : __disjvr_0^0'=__disjvr_0^post18, __disjvr_1^0'=__disjvr_1^post18, __disjvr_2^0'=__disjvr_2^post18, result_4^0'=result_4^post18, tmp_8^0'=tmp_8^post18, x_5^0'=x_5^post18, y_6^0'=1+y_6^post18, z_7^0'=z_7^post18, (0 == 0 /\ result_4^post17-result_4^post18 == 0 /\ -tmp_8^post18+tmp_8^post17 == 0 /\ __disjvr_2^post17-__disjvr_2^post18 == 0 /\ z_7^0-z_7^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ y_6^post17-y_6^post18 == 0 /\ __disjvr_0^post17-__disjvr_0^post18 == 0 /\ -__disjvr_2^post17+__disjvr_2^post18 == 0 /\ -z_7^post18+z_7^post17 == 0 /\ 1-z_7^0+y_6^0 <= 0 /\ -x_5^post17+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ x_5^post17-x_5^post18 == 0 /\ -y_6^post17+y_6^0 == 0 /\ -__disjvr_1^post18+__disjvr_1^post17 == 0 /\ -result_4^post17+result_4^0 == 0 /\ -__disjvr_1^post17+__disjvr_1^0 == 0), cost: 1
	New rule:
	l3 -> l2 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^post18, x_5^0'=x_5^0, y_6^0'=1+y_6^0, z_7^0'=z_7^0, (0 == 0 /\ 1-z_7^0+y_6^0 <= 0), cost: 1
	
		propagated equality result_4^post17 = result_4^post18
		
		propagated equality tmp_8^post17 = tmp_8^post18
		
		propagated equality __disjvr_2^post17 = __disjvr_2^post18
		
		propagated equality z_7^post17 = z_7^0
		
		propagated equality __disjvr_2^post18 = __disjvr_2^0
		
		propagated equality y_6^post17 = y_6^post18
		
		propagated equality __disjvr_0^post17 = __disjvr_0^post18
		
		propagated equality z_7^post18 = z_7^0
		
		propagated equality x_5^post17 = x_5^0
		
		propagated equality __disjvr_0^post18 = __disjvr_0^0
		
		propagated equality x_5^post18 = x_5^0
		
		propagated equality y_6^post18 = y_6^0
		
		propagated equality __disjvr_1^post17 = __disjvr_1^post18
		
		propagated equality result_4^post18 = result_4^0
		
		propagated equality __disjvr_1^post18 = __disjvr_1^0
		
	Simplified Guard

	Original rule:
	l3 -> l2 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^post18, x_5^0'=x_5^0, y_6^0'=1+y_6^0, z_7^0'=z_7^0, (0 == 0 /\ 1-z_7^0+y_6^0 <= 0), cost: 1
	New rule:
	l3 -> l2 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^post18, x_5^0'=x_5^0, y_6^0'=1+y_6^0, z_7^0'=z_7^0, 1-z_7^0+y_6^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l2 : __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, __disjvr_2^0'=__disjvr_2^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^post18, x_5^0'=x_5^0, y_6^0'=1+y_6^0, z_7^0'=z_7^0, 1-z_7^0+y_6^0 <= 0, cost: 1
	New rule:
	l3 -> l2 : tmp_8^0'=tmp_8^post18, y_6^0'=1+y_6^0, 1-z_7^0+y_6^0 <= 0, cost: 1

Step with 35

	Trace

	35[T]
	
	Blocked

	[{}, {}]

Step with 32

	Trace

	35[T], 32[(y_6^0-x_5^0 <= 0)]
	
	Blocked

	[{}, {}, {}]

Backtrack

	Trace

	35[T]
	
	Blocked

	[{}, {32[T]}]

Step with 31

	Trace

	35[T], 31[(1-y_6^0+x_5^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}]

Step with 33

	Trace

	35[T], 31[(1-y_6^0+x_5^0 <= 0)], 33[(1-z_7^0+y_6^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {}]

Step with 38

	Trace

	35[T], 31[(1-y_6^0+x_5^0 <= 0)], 33[(1-z_7^0+y_6^0 <= 0)], 38[(1-z_7^0+y_6^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {}, {}]

Nonterm

Start location: l14
Program variables: result_4^0 tmp_8^0 x_5^0 y_6^0 z_7^0
  31: l1 -> l7 : 1-y_6^0+x_5^0 <= 0, cost: 1
  32: l1 -> l8 : result_4^0'=result_4^post9, y_6^0-x_5^0 <= 0, cost: 1
  29: l2 -> l3 : tmp_8^0'=0, 1-z_7^0+y_6^0 <= 0, cost: 1
  30: l2 -> l1 : x_5^0'=1+x_5^0, z_7^0-y_6^0 <= 0, cost: 1
  37: l2 -> l2 : tmp_8^0'=tmp_8^post5, y_6^0'=1+y_6^0, 1-z_7^0+y_6^0 <= 0, cost: 1
  38: l3 -> l3 : tmp_8^0'=0, 1-z_7^0+y_6^0 <= 0, cost: 1
  39: l3 -> l2 : tmp_8^0'=tmp_8^post18, y_6^0'=1+y_6^0, 1-z_7^0+y_6^0 <= 0, cost: 1
  40: l3 -> LoAT_sink : (-1+z_7^0-y_6^0 >= 0 /\ -1+n >= 0), cost: NONTERM
  33: l7 -> l3 : tmp_8^0'=0, 1-z_7^0+y_6^0 <= 0, cost: 1
  34: l7 -> l1 : x_5^0'=1+x_5^0, z_7^0-y_6^0 <= 0, cost: 1
  36: l7 -> l2 : tmp_8^0'=tmp_8^post12, y_6^0'=1+y_6^0, 1-z_7^0+y_6^0 <= 0, cost: 1
  35: l14 -> l1 : T, cost: 1

	Certificate of Non-Termination

	Original rule:
	l3 -> l3 : tmp_8^0'=0, (1-z_7^0+y_6^0 <= 0), cost: 1
	New rule:
	l3 -> LoAT_sink : (-1+z_7^0-y_6^0 >= 0 /\ -1+n >= 0), cost: NONTERM

		-1+z_7^0-y_6^0 >= 0 [0]: monotonic increase yields -1+z_7^0-y_6^0 >= 0
		
		Replacement map: {-1+z_7^0-y_6^0 >= 0 -> -1+z_7^0-y_6^0 >= 0}

Step with 40

	Trace

	35[T], 31[(1-y_6^0+x_5^0 <= 0)], 33[(1-z_7^0+y_6^0 <= 0)], 40[(-1+z_7^0-y_6^0 >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {}, {40[T]}]

Refute

	Counterexample

	[ result_4^0=0 tmp_8^0=0 x_5^0=0 y_6^0=1 z_7^0=2 ] 35 [ result_4^0=0 tmp_8^0=0 x_5^0=0 y_6^0=1 z_7^0=2 ] 31 [ result_4^0=0 tmp_8^0=0 x_5^0=0 y_6^0=1 z_7^0=2 ] 33 [ result_4^0=0 tmp_8^0=0 x_5^0=0 y_6^0=1 z_7^0=2 ] 40
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b