NO

Initial ITS
Start location: l31
   0: l0 -> l1 : __disjvr_4^0'=__disjvr_4^post0, x^0'=x^post0, __disjvr_1^0'=__disjvr_1^post0, r0^0'=r0^post0, __disjvr_6^0'=__disjvr_6^post0, __disjvr_3^0'=__disjvr_3^post0, x1^0'=x1^post0, __disjvr_0^0'=__disjvr_0^post0, __disjvr_8^0'=__disjvr_8^post0, __disjvr_5^0'=__disjvr_5^post0, __disjvr_2^0'=__disjvr_2^post0, r^0'=r^post0, __disjvr_7^0'=__disjvr_7^post0, (-__disjvr_3^post0+__disjvr_3^0 == 0 /\ r0^0 <= 0 /\ __disjvr_8^0-__disjvr_8^post0 == 0 /\ r0^0-r0^post0 == 0 /\ x1^0-x1^post0 == 0 /\ -__disjvr_7^post0+__disjvr_7^0 == 0 /\ -r^post0+r^0 == 0 /\ -__disjvr_0^post0+__disjvr_0^0 == 0 /\ __disjvr_1^0-__disjvr_1^post0 == 0 /\ -__disjvr_2^post0+__disjvr_2^0 == 0 /\ -r0^0 <= 0 /\ -x^post0+x^0 == 0 /\ __disjvr_4^0-__disjvr_4^post0 == 0 /\ -__disjvr_5^post0+__disjvr_5^0 == 0 /\ __disjvr_6^0-__disjvr_6^post0 == 0), cost: 1
   1: l2 -> l3 : __disjvr_4^0'=__disjvr_4^post1, x^0'=x^post1, __disjvr_1^0'=__disjvr_1^post1, r0^0'=r0^post1, __disjvr_6^0'=__disjvr_6^post1, __disjvr_3^0'=__disjvr_3^post1, x1^0'=x1^post1, __disjvr_0^0'=__disjvr_0^post1, __disjvr_8^0'=__disjvr_8^post1, __disjvr_5^0'=__disjvr_5^post1, __disjvr_2^0'=__disjvr_2^post1, r^0'=r^post1, __disjvr_7^0'=__disjvr_7^post1, (x^0-x^post1 == 0 /\ 1-r^0 <= 0 /\ -1+r^0 <= 0 /\ r0^0-r0^post1 == 0 /\ __disjvr_8^0-__disjvr_8^post1 == 0 /\ -__disjvr_0^post1+__disjvr_0^0 == 0 /\ x1^0-x1^post1 == 0 /\ -__disjvr_2^post1+__disjvr_2^0 == 0 /\ __disjvr_1^0-__disjvr_1^post1 == 0 /\ __disjvr_6^0-__disjvr_6^post1 == 0 /\ -__disjvr_3^post1+__disjvr_3^0 == 0 /\ -__disjvr_7^post1+__disjvr_7^0 == 0 /\ -r^post1+r^0 == 0 /\ __disjvr_4^0-__disjvr_4^post1 == 0 /\ -__disjvr_5^post1+__disjvr_5^0 == 0), cost: 1
   2: l4 -> l3 : __disjvr_4^0'=__disjvr_4^post2, x^0'=x^post2, __disjvr_1^0'=__disjvr_1^post2, r0^0'=r0^post2, __disjvr_6^0'=__disjvr_6^post2, __disjvr_3^0'=__disjvr_3^post2, x1^0'=x1^post2, __disjvr_0^0'=__disjvr_0^post2, __disjvr_8^0'=__disjvr_8^post2, __disjvr_5^0'=__disjvr_5^post2, __disjvr_2^0'=__disjvr_2^post2, r^0'=r^post2, __disjvr_7^0'=__disjvr_7^post2, (r0^0-r0^post2 == 0 /\ -__disjvr_6^post2+__disjvr_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post2 == 0 /\ x1^0-x1^post2 == 0 /\ __disjvr_4^0-__disjvr_4^post2 == 0 /\ __disjvr_8^0-__disjvr_8^post2 == 0 /\ 1-r^0 <= 0 /\ -1+r^0 <= 0 /\ -__disjvr_3^post2+__disjvr_3^0 == 0 /\ -__disjvr_5^post2+__disjvr_5^0 == 0 /\ -x^post2+x^0 == 0 /\ -r^post2+r^0 == 0 /\ -__disjvr_7^post2+__disjvr_7^0 == 0 /\ -__disjvr_0^post2+__disjvr_0^0 == 0 /\ __disjvr_1^0-__disjvr_1^post2 == 0), cost: 1
   3: l5 -> l3 : __disjvr_4^0'=__disjvr_4^post3, x^0'=x^post3, __disjvr_1^0'=__disjvr_1^post3, r0^0'=r0^post3, __disjvr_6^0'=__disjvr_6^post3, __disjvr_3^0'=__disjvr_3^post3, x1^0'=x1^post3, __disjvr_0^0'=__disjvr_0^post3, __disjvr_8^0'=__disjvr_8^post3, __disjvr_5^0'=__disjvr_5^post3, __disjvr_2^0'=__disjvr_2^post3, r^0'=r^post3, __disjvr_7^0'=__disjvr_7^post3, (-__disjvr_0^post3+__disjvr_0^0 == 0 /\ -__disjvr_5^post3+__disjvr_5^0 == 0 /\ x^0-x^post3 == 0 /\ -r^post3+r^0 == 0 /\ __disjvr_4^0-__disjvr_4^post3 == 0 /\ -__disjvr_2^post3+__disjvr_2^0 == 0 /\ 1-r^0 <= 0 /\ -1+r^0 <= 0 /\ r0^0-r0^post3 == 0 /\ __disjvr_8^0-__disjvr_8^post3 == 0 /\ x1^0-x1^post3 == 0 /\ __disjvr_1^0-__disjvr_1^post3 == 0 /\ -__disjvr_7^post3+__disjvr_7^0 == 0 /\ __disjvr_6^0-__disjvr_6^post3 == 0 /\ -__disjvr_3^post3+__disjvr_3^0 == 0), cost: 1
   4: l6 -> l7 : __disjvr_4^0'=__disjvr_4^post4, x^0'=x^post4, __disjvr_1^0'=__disjvr_1^post4, r0^0'=r0^post4, __disjvr_6^0'=__disjvr_6^post4, __disjvr_3^0'=__disjvr_3^post4, x1^0'=x1^post4, __disjvr_0^0'=__disjvr_0^post4, __disjvr_8^0'=__disjvr_8^post4, __disjvr_5^0'=__disjvr_5^post4, __disjvr_2^0'=__disjvr_2^post4, r^0'=r^post4, __disjvr_7^0'=__disjvr_7^post4, (__disjvr_8^0-__disjvr_8^post4 == 0 /\ -__disjvr_6^post4+__disjvr_6^0 == 0 /\ -__disjvr_7^post4+__disjvr_7^0 == 0 /\ r0^0-r0^post4 == 0 /\ __disjvr_2^0-__disjvr_2^post4 == 0 /\ -__disjvr_3^post4+__disjvr_3^0 == 0 /\ __disjvr_1^0-__disjvr_1^post4 == 0 /\ __disjvr_0^0-__disjvr_0^post4 == 0 /\ -__disjvr_5^post4+__disjvr_5^0 == 0 /\ -r^post4+r^0 == 0 /\ __disjvr_4^0-__disjvr_4^post4 == 0 /\ -x^0+x1^post4 == 0 /\ -x^post4+x^0 == 0), cost: 1
   5: l6 -> l8 : __disjvr_4^0'=__disjvr_4^post5, x^0'=x^post5, __disjvr_1^0'=__disjvr_1^post5, r0^0'=r0^post5, __disjvr_6^0'=__disjvr_6^post5, __disjvr_3^0'=__disjvr_3^post5, x1^0'=x1^post5, __disjvr_0^0'=__disjvr_0^post5, __disjvr_8^0'=__disjvr_8^post5, __disjvr_5^0'=__disjvr_5^post5, __disjvr_2^0'=__disjvr_2^post5, r^0'=r^post5, __disjvr_7^0'=__disjvr_7^post5, (__disjvr_4^0-__disjvr_4^post5 == 0 /\ x1^0-x1^post5 == 0 /\ -__disjvr_6^post5+__disjvr_6^0 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ -__disjvr_3^post5+__disjvr_3^0 == 0 /\ -r^post5+r^0 == 0 /\ __disjvr_8^0-__disjvr_8^post5 == 0 /\ -__disjvr_7^post5+__disjvr_7^0 == 0 /\ x^0-x^post5 == 0 /\ -__disjvr_2^post5+__disjvr_2^0 == 0 /\ -__disjvr_5^post5+__disjvr_5^0 == 0 /\ __disjvr_1^0-__disjvr_1^post5 == 0 /\ r0^0-r0^post5 == 0), cost: 1
   7: l6 -> l3 : __disjvr_4^0'=__disjvr_4^post7, x^0'=x^post7, __disjvr_1^0'=__disjvr_1^post7, r0^0'=r0^post7, __disjvr_6^0'=__disjvr_6^post7, __disjvr_3^0'=__disjvr_3^post7, x1^0'=x1^post7, __disjvr_0^0'=__disjvr_0^post7, __disjvr_8^0'=__disjvr_8^post7, __disjvr_5^0'=__disjvr_5^post7, __disjvr_2^0'=__disjvr_2^post7, r^0'=r^post7, __disjvr_7^0'=__disjvr_7^post7, (__disjvr_2^0-__disjvr_2^post7 == 0 /\ __disjvr_4^0-__disjvr_4^post7 == 0 /\ __disjvr_8^0-__disjvr_8^post7 == 0 /\ r0^0-r0^post7 == 0 /\ -__disjvr_3^post7+__disjvr_3^0 == 0 /\ x1^0-x1^post7 == 0 /\ -__disjvr_5^post7+__disjvr_5^0 == 0 /\ __disjvr_1^0-__disjvr_1^post7 == 0 /\ -x^post7+x^0 == 0 /\ -__disjvr_7^post7+__disjvr_7^0 == 0 /\ -r^post7+r^0 == 0 /\ -__disjvr_0^post7+__disjvr_0^0 == 0 /\ __disjvr_6^0-__disjvr_6^post7 == 0), cost: 1
   8: l7 -> l9 : __disjvr_4^0'=__disjvr_4^post8, x^0'=x^post8, __disjvr_1^0'=__disjvr_1^post8, r0^0'=r0^post8, __disjvr_6^0'=__disjvr_6^post8, __disjvr_3^0'=__disjvr_3^post8, x1^0'=x1^post8, __disjvr_0^0'=__disjvr_0^post8, __disjvr_8^0'=__disjvr_8^post8, __disjvr_5^0'=__disjvr_5^post8, __disjvr_2^0'=__disjvr_2^post8, r^0'=r^post8, __disjvr_7^0'=__disjvr_7^post8, (-__disjvr_5^post8+__disjvr_5^0 == 0 /\ -__disjvr_0^post8+__disjvr_0^0 == 0 /\ x^0-x^post8 == 0 /\ r0^0-r0^post8 == 0 /\ -__disjvr_7^post8+__disjvr_7^0 == 0 /\ -r^post8+r^0 == 0 /\ __disjvr_8^0-__disjvr_8^post8 == 0 /\ __disjvr_0^post8-__disjvr_0^0 == 0 /\ x1^0-x1^post8 == 0 /\ -__disjvr_2^post8+__disjvr_2^0 == 0 /\ __disjvr_1^0-__disjvr_1^post8 == 0 /\ __disjvr_6^0-__disjvr_6^post8 == 0 /\ -__disjvr_3^post8+__disjvr_3^0 == 0 /\ __disjvr_4^0-__disjvr_4^post8 == 0), cost: 1
  10: l7 -> l2 : __disjvr_4^0'=__disjvr_4^post10, x^0'=x^post10, __disjvr_1^0'=__disjvr_1^post10, r0^0'=r0^post10, __disjvr_6^0'=__disjvr_6^post10, __disjvr_3^0'=__disjvr_3^post10, x1^0'=x1^post10, __disjvr_0^0'=__disjvr_0^post10, __disjvr_8^0'=__disjvr_8^post10, __disjvr_5^0'=__disjvr_5^post10, __disjvr_2^0'=__disjvr_2^post10, r^0'=r^post10, __disjvr_7^0'=__disjvr_7^post10, (r0^0-r0^post10 == 0 /\ -__disjvr_6^post10+__disjvr_6^0 == 0 /\ -__disjvr_5^post10+__disjvr_5^0 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0 /\ __disjvr_4^0-__disjvr_4^post10 == 0 /\ __disjvr_8^0-__disjvr_8^post10 == 0 /\ x1^0-x1^post10 == 0 /\ -__disjvr_2^post10+__disjvr_2^0 == 0 /\ -__disjvr_3^post10+__disjvr_3^0 == 0 /\ -__disjvr_7^post10+__disjvr_7^0 == 0 /\ -1+r^post10 == 0 /\ x^0-x^post10 == 0 /\ __disjvr_1^0-__disjvr_1^post10 == 0), cost: 1
  11: l7 -> l10 : __disjvr_4^0'=__disjvr_4^post11, x^0'=x^post11, __disjvr_1^0'=__disjvr_1^post11, r0^0'=r0^post11, __disjvr_6^0'=__disjvr_6^post11, __disjvr_3^0'=__disjvr_3^post11, x1^0'=x1^post11, __disjvr_0^0'=__disjvr_0^post11, __disjvr_8^0'=__disjvr_8^post11, __disjvr_5^0'=__disjvr_5^post11, __disjvr_2^0'=__disjvr_2^post11, r^0'=r^post11, __disjvr_7^0'=__disjvr_7^post11, (-__disjvr_3^post11+__disjvr_3^0 == 0 /\ -__disjvr_7^post11+__disjvr_7^0 == 0 /\ r0^0-r0^post11 == 0 /\ -__disjvr_5^post11+__disjvr_5^0 == 0 /\ x1^0-x1^post11 == 0 /\ __disjvr_8^0-__disjvr_8^post11 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ __disjvr_0^0-__disjvr_0^post11 == 0 /\ -r^post11+r^0 == 0 /\ __disjvr_1^0-__disjvr_1^post11 == 0 /\ __disjvr_4^0-__disjvr_4^post11 == 0 /\ __disjvr_6^0-__disjvr_6^post11 == 0 /\ -x^post11+x^0 == 0), cost: 1
   6: l8 -> l6 : __disjvr_4^0'=__disjvr_4^post6, x^0'=x^post6, __disjvr_1^0'=__disjvr_1^post6, r0^0'=r0^post6, __disjvr_6^0'=__disjvr_6^post6, __disjvr_3^0'=__disjvr_3^post6, x1^0'=x1^post6, __disjvr_0^0'=__disjvr_0^post6, __disjvr_8^0'=__disjvr_8^post6, __disjvr_5^0'=__disjvr_5^post6, __disjvr_2^0'=__disjvr_2^post6, r^0'=r^post6, __disjvr_7^0'=__disjvr_7^post6, (x^0-x^post6 == 0 /\ __disjvr_2^0-__disjvr_2^post6 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ __disjvr_1^0-__disjvr_1^post6 == 0 /\ __disjvr_8^0-__disjvr_8^post6 == 0 /\ r0^0-r0^post6 == 0 /\ x1^0-x1^post6 == 0 /\ __disjvr_4^0-__disjvr_4^post6 == 0 /\ __disjvr_6^0-__disjvr_6^post6 == 0 /\ -__disjvr_3^post6+__disjvr_3^0 == 0 /\ -__disjvr_5^post6+__disjvr_5^0 == 0 /\ -__disjvr_7^post6+__disjvr_7^0 == 0 /\ -r^post6+r^0 == 0), cost: 1
   9: l9 -> l2 : __disjvr_4^0'=__disjvr_4^post9, x^0'=x^post9, __disjvr_1^0'=__disjvr_1^post9, r0^0'=r0^post9, __disjvr_6^0'=__disjvr_6^post9, __disjvr_3^0'=__disjvr_3^post9, x1^0'=x1^post9, __disjvr_0^0'=__disjvr_0^post9, __disjvr_8^0'=__disjvr_8^post9, __disjvr_5^0'=__disjvr_5^post9, __disjvr_2^0'=__disjvr_2^post9, r^0'=r^post9, __disjvr_7^0'=__disjvr_7^post9, (r0^0-r0^post9 == 0 /\ -__disjvr_6^post9+__disjvr_6^0 == 0 /\ __disjvr_8^0-__disjvr_8^post9 == 0 /\ x1^0-x1^post9 == 0 /\ x^0-x^post9 == 0 /\ r^post9 == 0 /\ -__disjvr_3^post9+__disjvr_3^0 == 0 /\ __disjvr_2^0-__disjvr_2^post9 == 0 /\ -__disjvr_5^post9+__disjvr_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post9 == 0 /\ __disjvr_1^0-__disjvr_1^post9 == 0 /\ -__disjvr_7^post9+__disjvr_7^0 == 0 /\ __disjvr_4^0-__disjvr_4^post9 == 0), cost: 1
  12: l10 -> l7 : __disjvr_4^0'=__disjvr_4^post12, x^0'=x^post12, __disjvr_1^0'=__disjvr_1^post12, r0^0'=r0^post12, __disjvr_6^0'=__disjvr_6^post12, __disjvr_3^0'=__disjvr_3^post12, x1^0'=x1^post12, __disjvr_0^0'=__disjvr_0^post12, __disjvr_8^0'=__disjvr_8^post12, __disjvr_5^0'=__disjvr_5^post12, __disjvr_2^0'=__disjvr_2^post12, r^0'=r^post12, __disjvr_7^0'=__disjvr_7^post12, (x1^0-x1^post12 == 0 /\ __disjvr_4^0-__disjvr_4^post12 == 0 /\ -__disjvr_6^post12+__disjvr_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post12 == 0 /\ __disjvr_0^0-__disjvr_0^post12 == 0 /\ -r^post12+r^0 == 0 /\ -__disjvr_7^post12+__disjvr_7^0 == 0 /\ x^0-x^post12 == 0 /\ -__disjvr_3^post12+__disjvr_3^0 == 0 /\ -__disjvr_5^post12+__disjvr_5^0 == 0 /\ __disjvr_1^0-__disjvr_1^post12 == 0 /\ r0^0-r0^post12 == 0 /\ -__disjvr_8^post12+__disjvr_8^0 == 0), cost: 1
  13: l11 -> l12 : __disjvr_4^0'=__disjvr_4^post13, x^0'=x^post13, __disjvr_1^0'=__disjvr_1^post13, r0^0'=r0^post13, __disjvr_6^0'=__disjvr_6^post13, __disjvr_3^0'=__disjvr_3^post13, x1^0'=x1^post13, __disjvr_0^0'=__disjvr_0^post13, __disjvr_8^0'=__disjvr_8^post13, __disjvr_5^0'=__disjvr_5^post13, __disjvr_2^0'=__disjvr_2^post13, r^0'=r^post13, __disjvr_7^0'=__disjvr_7^post13, (__disjvr_2^0-__disjvr_2^post13 == 0 /\ __disjvr_8^0-__disjvr_8^post13 == 0 /\ -__disjvr_3^post13+__disjvr_3^0 == 0 /\ r0^0-r0^post13 == 0 /\ -__disjvr_5^post13+__disjvr_5^0 == 0 /\ x1^0-x1^post13 == 0 /\ __disjvr_1^0-__disjvr_1^post13 == 0 /\ -__disjvr_0^post13+__disjvr_0^0 == 0 /\ -__disjvr_1^0+__disjvr_1^post13 == 0 /\ __disjvr_4^0-__disjvr_4^post13 == 0 /\ -x^post13+x^0 == 0 /\ -r^post13+r^0 == 0 /\ __disjvr_6^0-__disjvr_6^post13 == 0 /\ -__disjvr_7^post13+__disjvr_7^0 == 0), cost: 1
  15: l11 -> l4 : __disjvr_4^0'=__disjvr_4^post15, x^0'=x^post15, __disjvr_1^0'=__disjvr_1^post15, r0^0'=r0^post15, __disjvr_6^0'=__disjvr_6^post15, __disjvr_3^0'=__disjvr_3^post15, x1^0'=x1^post15, __disjvr_0^0'=__disjvr_0^post15, __disjvr_8^0'=__disjvr_8^post15, __disjvr_5^0'=__disjvr_5^post15, __disjvr_2^0'=__disjvr_2^post15, r^0'=r^post15, __disjvr_7^0'=__disjvr_7^post15, (x1^0-x1^post15 == 0 /\ __disjvr_1^0-__disjvr_1^post15 == 0 /\ __disjvr_2^0-__disjvr_2^post15 == 0 /\ -__disjvr_7^post15+__disjvr_7^0 == 0 /\ __disjvr_4^0-__disjvr_4^post15 == 0 /\ -1+r^post15 == 0 /\ -__disjvr_6^post15+__disjvr_6^0 == 0 /\ x^0-x^post15 == 0 /\ r0^0-r0^post15 == 0 /\ -__disjvr_8^post15+__disjvr_8^0 == 0 /\ -__disjvr_5^post15+__disjvr_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post15 == 0 /\ __disjvr_3^0-__disjvr_3^post15 == 0), cost: 1
  16: l11 -> l13 : __disjvr_4^0'=__disjvr_4^post16, x^0'=x^post16, __disjvr_1^0'=__disjvr_1^post16, r0^0'=r0^post16, __disjvr_6^0'=__disjvr_6^post16, __disjvr_3^0'=__disjvr_3^post16, x1^0'=x1^post16, __disjvr_0^0'=__disjvr_0^post16, __disjvr_8^0'=__disjvr_8^post16, __disjvr_5^0'=__disjvr_5^post16, __disjvr_2^0'=__disjvr_2^post16, r^0'=r^post16, __disjvr_7^0'=__disjvr_7^post16, (__disjvr_0^0-__disjvr_0^post16 == 0 /\ -__disjvr_2^post16+__disjvr_2^0 == 0 /\ __disjvr_1^0-__disjvr_1^post16 == 0 /\ __disjvr_4^0-__disjvr_4^post16 == 0 /\ -__disjvr_5^post16+__disjvr_5^0 == 0 /\ -__disjvr_6^post16+__disjvr_6^0 == 0 /\ x^0-x^post16 == 0 /\ -__disjvr_8^post16+__disjvr_8^0 == 0 /\ r0^0-r0^post16 == 0 /\ __disjvr_3^0-__disjvr_3^post16 == 0 /\ -__disjvr_7^post16+__disjvr_7^0 == 0 /\ -r^post16+r^0 == 0 /\ x1^0-x1^post16 == 0), cost: 1
  14: l12 -> l4 : __disjvr_4^0'=__disjvr_4^post14, x^0'=x^post14, __disjvr_1^0'=__disjvr_1^post14, r0^0'=r0^post14, __disjvr_6^0'=__disjvr_6^post14, __disjvr_3^0'=__disjvr_3^post14, x1^0'=x1^post14, __disjvr_0^0'=__disjvr_0^post14, __disjvr_8^0'=__disjvr_8^post14, __disjvr_5^0'=__disjvr_5^post14, __disjvr_2^0'=__disjvr_2^post14, r^0'=r^post14, __disjvr_7^0'=__disjvr_7^post14, (x1^0-x1^post14 == 0 /\ __disjvr_4^0-__disjvr_4^post14 == 0 /\ r^post14 == 0 /\ __disjvr_2^0-__disjvr_2^post14 == 0 /\ -__disjvr_7^post14+__disjvr_7^0 == 0 /\ -__disjvr_6^post14+__disjvr_6^0 == 0 /\ -x^post14+x^0 == 0 /\ __disjvr_1^0-__disjvr_1^post14 == 0 /\ -__disjvr_8^post14+__disjvr_8^0 == 0 /\ -__disjvr_5^post14+__disjvr_5^0 == 0 /\ r0^0-r0^post14 == 0 /\ __disjvr_3^0-__disjvr_3^post14 == 0 /\ __disjvr_0^0-__disjvr_0^post14 == 0), cost: 1
  17: l13 -> l11 : __disjvr_4^0'=__disjvr_4^post17, x^0'=x^post17, __disjvr_1^0'=__disjvr_1^post17, r0^0'=r0^post17, __disjvr_6^0'=__disjvr_6^post17, __disjvr_3^0'=__disjvr_3^post17, x1^0'=x1^post17, __disjvr_0^0'=__disjvr_0^post17, __disjvr_8^0'=__disjvr_8^post17, __disjvr_5^0'=__disjvr_5^post17, __disjvr_2^0'=__disjvr_2^post17, r^0'=r^post17, __disjvr_7^0'=__disjvr_7^post17, (__disjvr_3^0-__disjvr_3^post17 == 0 /\ -__disjvr_6^post17+__disjvr_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ -r^post17+r^0 == 0 /\ -__disjvr_8^post17+__disjvr_8^0 == 0 /\ x^0-x^post17 == 0 /\ __disjvr_1^0-__disjvr_1^post17 == 0 /\ r0^0-r0^post17 == 0 /\ -__disjvr_5^post17+__disjvr_5^0 == 0 /\ x1^0-x1^post17 == 0 /\ __disjvr_4^0-__disjvr_4^post17 == 0 /\ -__disjvr_7^post17+__disjvr_7^0 == 0), cost: 1
  18: l14 -> l15 : __disjvr_4^0'=__disjvr_4^post18, x^0'=x^post18, __disjvr_1^0'=__disjvr_1^post18, r0^0'=r0^post18, __disjvr_6^0'=__disjvr_6^post18, __disjvr_3^0'=__disjvr_3^post18, x1^0'=x1^post18, __disjvr_0^0'=__disjvr_0^post18, __disjvr_8^0'=__disjvr_8^post18, __disjvr_5^0'=__disjvr_5^post18, __disjvr_2^0'=__disjvr_2^post18, r^0'=r^post18, __disjvr_7^0'=__disjvr_7^post18, (__disjvr_2^post18-__disjvr_2^0 == 0 /\ -__disjvr_5^post18+__disjvr_5^0 == 0 /\ __disjvr_1^0-__disjvr_1^post18 == 0 /\ -r^post18+r^0 == 0 /\ __disjvr_4^0-__disjvr_4^post18 == 0 /\ -__disjvr_2^post18+__disjvr_2^0 == 0 /\ -__disjvr_8^post18+__disjvr_8^0 == 0 /\ x^0-x^post18 == 0 /\ -__disjvr_7^post18+__disjvr_7^0 == 0 /\ -__disjvr_6^post18+__disjvr_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post18 == 0 /\ r0^0-r0^post18 == 0 /\ __disjvr_3^0-__disjvr_3^post18 == 0 /\ x1^0-x1^post18 == 0), cost: 1
  20: l14 -> l5 : __disjvr_4^0'=__disjvr_4^post20, x^0'=x^post20, __disjvr_1^0'=__disjvr_1^post20, r0^0'=r0^post20, __disjvr_6^0'=__disjvr_6^post20, __disjvr_3^0'=__disjvr_3^post20, x1^0'=x1^post20, __disjvr_0^0'=__disjvr_0^post20, __disjvr_8^0'=__disjvr_8^post20, __disjvr_5^0'=__disjvr_5^post20, __disjvr_2^0'=__disjvr_2^post20, r^0'=r^post20, __disjvr_7^0'=__disjvr_7^post20, (-__disjvr_2^post20+__disjvr_2^0 == 0 /\ x^0-x^post20 == 0 /\ __disjvr_3^0-__disjvr_3^post20 == 0 /\ __disjvr_0^0-__disjvr_0^post20 == 0 /\ -1+r^post20 == 0 /\ -__disjvr_5^post20+__disjvr_5^0 == 0 /\ __disjvr_1^0-__disjvr_1^post20 == 0 /\ -__disjvr_8^post20+__disjvr_8^0 == 0 /\ -__disjvr_7^post20+__disjvr_7^0 == 0 /\ __disjvr_4^0-__disjvr_4^post20 == 0 /\ -r0^post20+r0^0 == 0 /\ x1^0-x1^post20 == 0 /\ -__disjvr_6^post20+__disjvr_6^0 == 0), cost: 1
  21: l14 -> l16 : __disjvr_4^0'=__disjvr_4^post21, x^0'=x^post21, __disjvr_1^0'=__disjvr_1^post21, r0^0'=r0^post21, __disjvr_6^0'=__disjvr_6^post21, __disjvr_3^0'=__disjvr_3^post21, x1^0'=x1^post21, __disjvr_0^0'=__disjvr_0^post21, __disjvr_8^0'=__disjvr_8^post21, __disjvr_5^0'=__disjvr_5^post21, __disjvr_2^0'=__disjvr_2^post21, r^0'=r^post21, __disjvr_7^0'=__disjvr_7^post21, (-__disjvr_7^post21+__disjvr_7^0 == 0 /\ __disjvr_1^0-__disjvr_1^post21 == 0 /\ __disjvr_3^0-__disjvr_3^post21 == 0 /\ x^0-x^post21 == 0 /\ __disjvr_4^0-__disjvr_4^post21 == 0 /\ -r^post21+r^0 == 0 /\ __disjvr_0^0-__disjvr_0^post21 == 0 /\ -__disjvr_2^post21+__disjvr_2^0 == 0 /\ r0^0-r0^post21 == 0 /\ -__disjvr_5^post21+__disjvr_5^0 == 0 /\ x1^0-x1^post21 == 0 /\ -__disjvr_6^post21+__disjvr_6^0 == 0 /\ -__disjvr_8^post21+__disjvr_8^0 == 0), cost: 1
  19: l15 -> l5 : __disjvr_4^0'=__disjvr_4^post19, x^0'=x^post19, __disjvr_1^0'=__disjvr_1^post19, r0^0'=r0^post19, __disjvr_6^0'=__disjvr_6^post19, __disjvr_3^0'=__disjvr_3^post19, x1^0'=x1^post19, __disjvr_0^0'=__disjvr_0^post19, __disjvr_8^0'=__disjvr_8^post19, __disjvr_5^0'=__disjvr_5^post19, __disjvr_2^0'=__disjvr_2^post19, r^0'=r^post19, __disjvr_7^0'=__disjvr_7^post19, (__disjvr_0^0-__disjvr_0^post19 == 0 /\ -__disjvr_8^post19+__disjvr_8^0 == 0 /\ __disjvr_3^0-__disjvr_3^post19 == 0 /\ x^0-x^post19 == 0 /\ -__disjvr_7^post19+__disjvr_7^0 == 0 /\ -__disjvr_6^post19+__disjvr_6^0 == 0 /\ __disjvr_4^0-__disjvr_4^post19 == 0 /\ __disjvr_1^0-__disjvr_1^post19 == 0 /\ r^post19 == 0 /\ r0^0-r0^post19 == 0 /\ -__disjvr_5^post19+__disjvr_5^0 == 0 /\ x1^0-x1^post19 == 0 /\ -__disjvr_2^post19+__disjvr_2^0 == 0), cost: 1
  22: l16 -> l14 : __disjvr_4^0'=__disjvr_4^post22, x^0'=x^post22, __disjvr_1^0'=__disjvr_1^post22, r0^0'=r0^post22, __disjvr_6^0'=__disjvr_6^post22, __disjvr_3^0'=__disjvr_3^post22, x1^0'=x1^post22, __disjvr_0^0'=__disjvr_0^post22, __disjvr_8^0'=__disjvr_8^post22, __disjvr_5^0'=__disjvr_5^post22, __disjvr_2^0'=__disjvr_2^post22, r^0'=r^post22, __disjvr_7^0'=__disjvr_7^post22, (x^0-x^post22 == 0 /\ -__disjvr_2^post22+__disjvr_2^0 == 0 /\ __disjvr_1^0-__disjvr_1^post22 == 0 /\ -__disjvr_6^post22+__disjvr_6^0 == 0 /\ __disjvr_3^0-__disjvr_3^post22 == 0 /\ __disjvr_0^0-__disjvr_0^post22 == 0 /\ x1^0-x1^post22 == 0 /\ __disjvr_4^0-__disjvr_4^post22 == 0 /\ -r0^post22+r0^0 == 0 /\ -__disjvr_5^post22+__disjvr_5^0 == 0 /\ -__disjvr_8^post22+__disjvr_8^0 == 0 /\ -__disjvr_7^post22+__disjvr_7^0 == 0 /\ -r^post22+r^0 == 0), cost: 1
  23: l17 -> l18 : __disjvr_4^0'=__disjvr_4^post23, x^0'=x^post23, __disjvr_1^0'=__disjvr_1^post23, r0^0'=r0^post23, __disjvr_6^0'=__disjvr_6^post23, __disjvr_3^0'=__disjvr_3^post23, x1^0'=x1^post23, __disjvr_0^0'=__disjvr_0^post23, __disjvr_8^0'=__disjvr_8^post23, __disjvr_5^0'=__disjvr_5^post23, __disjvr_2^0'=__disjvr_2^post23, r^0'=r^post23, __disjvr_7^0'=__disjvr_7^post23, (__disjvr_3^0-__disjvr_3^post23 == 0 /\ -__disjvr_6^post23+__disjvr_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post23 == 0 /\ -__disjvr_2^post23+__disjvr_2^0 == 0 /\ -__disjvr_3^0+__disjvr_3^post23 == 0 /\ -__disjvr_8^post23+__disjvr_8^0 == 0 /\ -__disjvr_5^post23+__disjvr_5^0 == 0 /\ x^0-x^post23 == 0 /\ __disjvr_1^0-__disjvr_1^post23 == 0 /\ r0^0-r0^post23 == 0 /\ x1^0-x1^post23 == 0 /\ -r^post23+r^0 == 0 /\ -__disjvr_4^post23+__disjvr_4^0 == 0 /\ -__disjvr_7^post23+__disjvr_7^0 == 0), cost: 1
  25: l17 -> l2 : __disjvr_4^0'=__disjvr_4^post25, x^0'=x^post25, __disjvr_1^0'=__disjvr_1^post25, r0^0'=r0^post25, __disjvr_6^0'=__disjvr_6^post25, __disjvr_3^0'=__disjvr_3^post25, x1^0'=x1^post25, __disjvr_0^0'=__disjvr_0^post25, __disjvr_8^0'=__disjvr_8^post25, __disjvr_5^0'=__disjvr_5^post25, __disjvr_2^0'=__disjvr_2^post25, r^0'=r^post25, __disjvr_7^0'=__disjvr_7^post25, (x^0-x^post25 == 0 /\ -__disjvr_5^post25+__disjvr_5^0 == 0 /\ -1+r^post25 == 0 /\ -__disjvr_2^post25+__disjvr_2^0 == 0 /\ -__disjvr_8^post25+__disjvr_8^0 == 0 /\ -__disjvr_7^post25+__disjvr_7^0 == 0 /\ __disjvr_1^0-__disjvr_1^post25 == 0 /\ r0^0-r0^post25 == 0 /\ -__disjvr_6^post25+__disjvr_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post25 == 0 /\ __disjvr_3^0-__disjvr_3^post25 == 0 /\ __disjvr_4^0-__disjvr_4^post25 == 0 /\ x1^0-x1^post25 == 0), cost: 1
  26: l17 -> l7 : __disjvr_4^0'=__disjvr_4^post26, x^0'=x^post26, __disjvr_1^0'=__disjvr_1^post26, r0^0'=r0^post26, __disjvr_6^0'=__disjvr_6^post26, __disjvr_3^0'=__disjvr_3^post26, x1^0'=x1^post26, __disjvr_0^0'=__disjvr_0^post26, __disjvr_8^0'=__disjvr_8^post26, __disjvr_5^0'=__disjvr_5^post26, __disjvr_2^0'=__disjvr_2^post26, r^0'=r^post26, __disjvr_7^0'=__disjvr_7^post26, (__disjvr_0^0-__disjvr_0^post26 == 0 /\ -__disjvr_8^post26+__disjvr_8^0 == 0 /\ __disjvr_1^0-__disjvr_1^post26 == 0 /\ -__disjvr_7^post26+__disjvr_7^0 == 0 /\ __disjvr_3^0-__disjvr_3^post26 == 0 /\ __disjvr_4^0-__disjvr_4^post26 == 0 /\ -2+x^post26 == 0 /\ -r^post26+r^0 == 0 /\ r0^0-r0^post26 == 0 /\ x1^0-x1^post26 == 0 /\ -__disjvr_5^post26+__disjvr_5^0 == 0 /\ -__disjvr_6^post26+__disjvr_6^0 == 0 /\ -__disjvr_2^post26+__disjvr_2^0 == 0), cost: 1
  24: l18 -> l2 : __disjvr_4^0'=__disjvr_4^post24, x^0'=x^post24, __disjvr_1^0'=__disjvr_1^post24, r0^0'=r0^post24, __disjvr_6^0'=__disjvr_6^post24, __disjvr_3^0'=__disjvr_3^post24, x1^0'=x1^post24, __disjvr_0^0'=__disjvr_0^post24, __disjvr_8^0'=__disjvr_8^post24, __disjvr_5^0'=__disjvr_5^post24, __disjvr_2^0'=__disjvr_2^post24, r^0'=r^post24, __disjvr_7^0'=__disjvr_7^post24, (x^0-x^post24 == 0 /\ -x1^post24+x1^0 == 0 /\ __disjvr_3^0-__disjvr_3^post24 == 0 /\ -__disjvr_7^post24+__disjvr_7^0 == 0 /\ __disjvr_0^0-__disjvr_0^post24 == 0 /\ r^post24 == 0 /\ -__disjvr_2^post24+__disjvr_2^0 == 0 /\ __disjvr_1^0-__disjvr_1^post24 == 0 /\ -__disjvr_8^post24+__disjvr_8^0 == 0 /\ __disjvr_6^0-__disjvr_6^post24 == 0 /\ -r0^post24+r0^0 == 0 /\ __disjvr_4^0-__disjvr_4^post24 == 0 /\ -__disjvr_5^post24+__disjvr_5^0 == 0), cost: 1
  27: l19 -> l20 : __disjvr_4^0'=__disjvr_4^post27, x^0'=x^post27, __disjvr_1^0'=__disjvr_1^post27, r0^0'=r0^post27, __disjvr_6^0'=__disjvr_6^post27, __disjvr_3^0'=__disjvr_3^post27, x1^0'=x1^post27, __disjvr_0^0'=__disjvr_0^post27, __disjvr_8^0'=__disjvr_8^post27, __disjvr_5^0'=__disjvr_5^post27, __disjvr_2^0'=__disjvr_2^post27, r^0'=r^post27, __disjvr_7^0'=__disjvr_7^post27, (x^0-x^post27 == 0 /\ -__disjvr_2^post27+__disjvr_2^0 == 0 /\ __disjvr_0^0-__disjvr_0^post27 == 0 /\ -__disjvr_6^post27+__disjvr_6^0 == 0 /\ __disjvr_1^0-__disjvr_1^post27 == 0 /\ __disjvr_3^0-__disjvr_3^post27 == 0 /\ x1^0-x1^post27 == 0 /\ __disjvr_4^0-__disjvr_4^post27 == 0 /\ -r0^post27+r0^0 == 0 /\ -__disjvr_5^post27+__disjvr_5^0 == 0 /\ -__disjvr_4^0+__disjvr_4^post27 == 0 /\ -__disjvr_8^post27+__disjvr_8^0 == 0 /\ -r^post27+r^0 == 0 /\ -__disjvr_7^post27+__disjvr_7^0 == 0), cost: 1
  29: l19 -> l4 : __disjvr_4^0'=__disjvr_4^post29, x^0'=x^post29, __disjvr_1^0'=__disjvr_1^post29, r0^0'=r0^post29, __disjvr_6^0'=__disjvr_6^post29, __disjvr_3^0'=__disjvr_3^post29, x1^0'=x1^post29, __disjvr_0^0'=__disjvr_0^post29, __disjvr_8^0'=__disjvr_8^post29, __disjvr_5^0'=__disjvr_5^post29, __disjvr_2^0'=__disjvr_2^post29, r^0'=r^post29, __disjvr_7^0'=__disjvr_7^post29, (x^0-x^post29 == 0 /\ __disjvr_1^0-__disjvr_1^post29 == 0 /\ -__disjvr_7^post29+__disjvr_7^0 == 0 /\ __disjvr_0^0-__disjvr_0^post29 == 0 /\ -__disjvr_6^post29+__disjvr_6^0 == 0 /\ __disjvr_3^0-__disjvr_3^post29 == 0 /\ -r0^post29+r0^0 == 0 /\ x1^0-x1^post29 == 0 /\ -__disjvr_2^post29+__disjvr_2^0 == 0 /\ -__disjvr_8^post29+__disjvr_8^0 == 0 /\ -__disjvr_5^post29+__disjvr_5^0 == 0 /\ __disjvr_4^0-__disjvr_4^post29 == 0 /\ -1+r^post29 == 0), cost: 1
  30: l19 -> l11 : __disjvr_4^0'=__disjvr_4^post30, x^0'=x^post30, __disjvr_1^0'=__disjvr_1^post30, r0^0'=r0^post30, __disjvr_6^0'=__disjvr_6^post30, __disjvr_3^0'=__disjvr_3^post30, x1^0'=x1^post30, __disjvr_0^0'=__disjvr_0^post30, __disjvr_8^0'=__disjvr_8^post30, __disjvr_5^0'=__disjvr_5^post30, __disjvr_2^0'=__disjvr_2^post30, r^0'=r^post30, __disjvr_7^0'=__disjvr_7^post30, (__disjvr_3^0-__disjvr_3^post30 == 0 /\ -__disjvr_6^post30+__disjvr_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post30 == 0 /\ -__disjvr_8^post30+__disjvr_8^0 == 0 /\ __disjvr_1^0-__disjvr_1^post30 == 0 /\ -__disjvr_5^post30+__disjvr_5^0 == 0 /\ r0^0-r0^post30 == 0 /\ x1^0-x1^post30 == 0 /\ -__disjvr_7^post30+__disjvr_7^0 == 0 /\ -r^post30+r^0 == 0 /\ -__disjvr_2^post30+__disjvr_2^0 == 0 /\ -2+x^post30 == 0 /\ __disjvr_4^0-__disjvr_4^post30 == 0), cost: 1
  28: l20 -> l4 : __disjvr_4^0'=__disjvr_4^post28, x^0'=x^post28, __disjvr_1^0'=__disjvr_1^post28, r0^0'=r0^post28, __disjvr_6^0'=__disjvr_6^post28, __disjvr_3^0'=__disjvr_3^post28, x1^0'=x1^post28, __disjvr_0^0'=__disjvr_0^post28, __disjvr_8^0'=__disjvr_8^post28, __disjvr_5^0'=__disjvr_5^post28, __disjvr_2^0'=__disjvr_2^post28, r^0'=r^post28, __disjvr_7^0'=__disjvr_7^post28, (__disjvr_1^0-__disjvr_1^post28 == 0 /\ -__disjvr_2^post28+__disjvr_2^0 == 0 /\ __disjvr_0^0-__disjvr_0^post28 == 0 /\ __disjvr_3^0-__disjvr_3^post28 == 0 /\ x^0-x^post28 == 0 /\ -__disjvr_8^post28+__disjvr_8^0 == 0 /\ r^post28 == 0 /\ -__disjvr_5^post28+__disjvr_5^0 == 0 /\ -__disjvr_7^post28+__disjvr_7^0 == 0 /\ r0^0-r0^post28 == 0 /\ x1^0-x1^post28 == 0 /\ -__disjvr_4^post28+__disjvr_4^0 == 0 /\ -__disjvr_6^post28+__disjvr_6^0 == 0), cost: 1
  31: l21 -> l22 : __disjvr_4^0'=__disjvr_4^post31, x^0'=x^post31, __disjvr_1^0'=__disjvr_1^post31, r0^0'=r0^post31, __disjvr_6^0'=__disjvr_6^post31, __disjvr_3^0'=__disjvr_3^post31, x1^0'=x1^post31, __disjvr_0^0'=__disjvr_0^post31, __disjvr_8^0'=__disjvr_8^post31, __disjvr_5^0'=__disjvr_5^post31, __disjvr_2^0'=__disjvr_2^post31, r^0'=r^post31, __disjvr_7^0'=__disjvr_7^post31, (-__disjvr_5^post31+__disjvr_5^0 == 0 /\ -x1^post31+x1^0 == 0 /\ -__disjvr_6^post31+__disjvr_6^0 == 0 /\ -r^post31+r^0 == 0 /\ __disjvr_5^post31-__disjvr_5^0 == 0 /\ -__disjvr_7^post31+__disjvr_7^0 == 0 /\ __disjvr_3^0-__disjvr_3^post31 == 0 /\ -__disjvr_2^post31+__disjvr_2^0 == 0 /\ __disjvr_0^0-__disjvr_0^post31 == 0 /\ x^0-x^post31 == 0 /\ __disjvr_1^0-__disjvr_1^post31 == 0 /\ r0^0-r0^post31 == 0 /\ -__disjvr_8^post31+__disjvr_8^0 == 0 /\ __disjvr_4^0-__disjvr_4^post31 == 0), cost: 1
  33: l21 -> l5 : __disjvr_4^0'=__disjvr_4^post33, x^0'=x^post33, __disjvr_1^0'=__disjvr_1^post33, r0^0'=r0^post33, __disjvr_6^0'=__disjvr_6^post33, __disjvr_3^0'=__disjvr_3^post33, x1^0'=x1^post33, __disjvr_0^0'=__disjvr_0^post33, __disjvr_8^0'=__disjvr_8^post33, __disjvr_5^0'=__disjvr_5^post33, __disjvr_2^0'=__disjvr_2^post33, r^0'=r^post33, __disjvr_7^0'=__disjvr_7^post33, (__disjvr_0^0-__disjvr_0^post33 == 0 /\ x^0-x^post33 == 0 /\ -__disjvr_6^post33+__disjvr_6^0 == 0 /\ __disjvr_1^0-__disjvr_1^post33 == 0 /\ __disjvr_3^0-__disjvr_3^post33 == 0 /\ x1^0-x1^post33 == 0 /\ __disjvr_4^0-__disjvr_4^post33 == 0 /\ -__disjvr_7^post33+__disjvr_7^0 == 0 /\ -__disjvr_5^post33+__disjvr_5^0 == 0 /\ -r0^post33+r0^0 == 0 /\ -1+r^post33 == 0 /\ -__disjvr_2^post33+__disjvr_2^0 == 0 /\ -__disjvr_8^post33+__disjvr_8^0 == 0), cost: 1
  34: l21 -> l14 : __disjvr_4^0'=__disjvr_4^post34, x^0'=x^post34, __disjvr_1^0'=__disjvr_1^post34, r0^0'=r0^post34, __disjvr_6^0'=__disjvr_6^post34, __disjvr_3^0'=__disjvr_3^post34, x1^0'=x1^post34, __disjvr_0^0'=__disjvr_0^post34, __disjvr_8^0'=__disjvr_8^post34, __disjvr_5^0'=__disjvr_5^post34, __disjvr_2^0'=__disjvr_2^post34, r^0'=r^post34, __disjvr_7^0'=__disjvr_7^post34, (-2+x^post34 == 0 /\ -r^post34+r^0 == 0 /\ -r0^post34+r0^0 == 0 /\ __disjvr_0^0-__disjvr_0^post34 == 0 /\ -__disjvr_2^post34+__disjvr_2^0 == 0 /\ -__disjvr_8^post34+__disjvr_8^0 == 0 /\ -x1^post34+x1^0 == 0 /\ __disjvr_5^0-__disjvr_5^post34 == 0 /\ -__disjvr_7^post34+__disjvr_7^0 == 0 /\ __disjvr_1^0-__disjvr_1^post34 == 0 /\ __disjvr_3^0-__disjvr_3^post34 == 0 /\ __disjvr_4^0-__disjvr_4^post34 == 0 /\ __disjvr_6^0-__disjvr_6^post34 == 0), cost: 1
  32: l22 -> l5 : __disjvr_4^0'=__disjvr_4^post32, x^0'=x^post32, __disjvr_1^0'=__disjvr_1^post32, r0^0'=r0^post32, __disjvr_6^0'=__disjvr_6^post32, __disjvr_3^0'=__disjvr_3^post32, x1^0'=x1^post32, __disjvr_0^0'=__disjvr_0^post32, __disjvr_8^0'=__disjvr_8^post32, __disjvr_5^0'=__disjvr_5^post32, __disjvr_2^0'=__disjvr_2^post32, r^0'=r^post32, __disjvr_7^0'=__disjvr_7^post32, (__disjvr_0^0-__disjvr_0^post32 == 0 /\ -x1^post32+x1^0 == 0 /\ x^0-x^post32 == 0 /\ -__disjvr_7^post32+__disjvr_7^0 == 0 /\ __disjvr_3^0-__disjvr_3^post32 == 0 /\ r^post32 == 0 /\ -__disjvr_8^post32+__disjvr_8^0 == 0 /\ -__disjvr_5^post32+__disjvr_5^0 == 0 /\ __disjvr_1^0-__disjvr_1^post32 == 0 /\ __disjvr_6^0-__disjvr_6^post32 == 0 /\ -r0^post32+r0^0 == 0 /\ -__disjvr_2^post32+__disjvr_2^0 == 0 /\ __disjvr_4^0-__disjvr_4^post32 == 0), cost: 1
  35: l23 -> l24 : __disjvr_4^0'=__disjvr_4^post35, x^0'=x^post35, __disjvr_1^0'=__disjvr_1^post35, r0^0'=r0^post35, __disjvr_6^0'=__disjvr_6^post35, __disjvr_3^0'=__disjvr_3^post35, x1^0'=x1^post35, __disjvr_0^0'=__disjvr_0^post35, __disjvr_8^0'=__disjvr_8^post35, __disjvr_5^0'=__disjvr_5^post35, __disjvr_2^0'=__disjvr_2^post35, r^0'=r^post35, __disjvr_7^0'=__disjvr_7^post35, (-r0^post35+r0^0 == 0 /\ -__disjvr_2^post35+__disjvr_2^0 == 0 /\ -x1^post35+x1^0 == 0 /\ -__disjvr_8^post35+__disjvr_8^0 == 0 /\ __disjvr_5^0-__disjvr_5^post35 == 0 /\ __disjvr_1^0-__disjvr_1^post35 == 0 /\ -__disjvr_6^0+__disjvr_6^post35 == 0 /\ __disjvr_3^0-__disjvr_3^post35 == 0 /\ x^0-x^post35 == 0 /\ __disjvr_4^0-__disjvr_4^post35 == 0 /\ -__disjvr_0^post35+__disjvr_0^0 == 0 /\ __disjvr_6^0-__disjvr_6^post35 == 0 /\ -r^post35+r^0 == 0 /\ -__disjvr_7^post35+__disjvr_7^0 == 0), cost: 1
  37: l23 -> l2 : __disjvr_4^0'=__disjvr_4^post37, x^0'=x^post37, __disjvr_1^0'=__disjvr_1^post37, r0^0'=r0^post37, __disjvr_6^0'=__disjvr_6^post37, __disjvr_3^0'=__disjvr_3^post37, x1^0'=x1^post37, __disjvr_0^0'=__disjvr_0^post37, __disjvr_8^0'=__disjvr_8^post37, __disjvr_5^0'=__disjvr_5^post37, __disjvr_2^0'=__disjvr_2^post37, r^0'=r^post37, __disjvr_7^0'=__disjvr_7^post37, (-__disjvr_2^post37+__disjvr_2^0 == 0 /\ __disjvr_6^0-__disjvr_6^post37 == 0 /\ -__disjvr_8^post37+__disjvr_8^0 == 0 /\ __disjvr_4^0-__disjvr_4^post37 == 0 /\ __disjvr_5^0-__disjvr_5^post37 == 0 /\ x^0-x^post37 == 0 /\ -1+r^post37 == 0 /\ __disjvr_1^0-__disjvr_1^post37 == 0 /\ -x1^post37+x1^0 == 0 /\ -__disjvr_7^post37+__disjvr_7^0 == 0 /\ r0^0-r0^post37 == 0 /\ __disjvr_3^0-__disjvr_3^post37 == 0 /\ -__disjvr_0^post37+__disjvr_0^0 == 0), cost: 1
  38: l23 -> l17 : __disjvr_4^0'=__disjvr_4^post38, x^0'=x^post38, __disjvr_1^0'=__disjvr_1^post38, r0^0'=r0^post38, __disjvr_6^0'=__disjvr_6^post38, __disjvr_3^0'=__disjvr_3^post38, x1^0'=x1^post38, __disjvr_0^0'=__disjvr_0^post38, __disjvr_8^0'=__disjvr_8^post38, __disjvr_5^0'=__disjvr_5^post38, __disjvr_2^0'=__disjvr_2^post38, r^0'=r^post38, __disjvr_7^0'=__disjvr_7^post38, (__disjvr_6^0-__disjvr_6^post38 == 0 /\ __disjvr_4^0-__disjvr_4^post38 == 0 /\ -__disjvr_8^post38+__disjvr_8^0 == 0 /\ -__disjvr_7^post38+__disjvr_7^0 == 0 /\ -r^post38+r^0 == 0 /\ -r0^post38+r0^0 == 0 /\ __disjvr_3^0-__disjvr_3^post38 == 0 /\ -__disjvr_0^post38+__disjvr_0^0 == 0 /\ __disjvr_5^0-__disjvr_5^post38 == 0 /\ -__disjvr_2^post38+__disjvr_2^0 == 0 /\ -x1^post38+x1^0 == 0 /\ -1+x^post38 == 0 /\ __disjvr_1^0-__disjvr_1^post38 == 0), cost: 1
  36: l24 -> l2 : __disjvr_4^0'=__disjvr_4^post36, x^0'=x^post36, __disjvr_1^0'=__disjvr_1^post36, r0^0'=r0^post36, __disjvr_6^0'=__disjvr_6^post36, __disjvr_3^0'=__disjvr_3^post36, x1^0'=x1^post36, __disjvr_0^0'=__disjvr_0^post36, __disjvr_8^0'=__disjvr_8^post36, __disjvr_5^0'=__disjvr_5^post36, __disjvr_2^0'=__disjvr_2^post36, r^0'=r^post36, __disjvr_7^0'=__disjvr_7^post36, (-r0^post36+r0^0 == 0 /\ __disjvr_6^0-__disjvr_6^post36 == 0 /\ -__disjvr_0^post36+__disjvr_0^0 == 0 /\ -__disjvr_7^post36+__disjvr_7^0 == 0 /\ __disjvr_1^0-__disjvr_1^post36 == 0 /\ -__disjvr_2^post36+__disjvr_2^0 == 0 /\ __disjvr_5^0-__disjvr_5^post36 == 0 /\ x^0-x^post36 == 0 /\ r^post36 == 0 /\ __disjvr_4^0-__disjvr_4^post36 == 0 /\ -__disjvr_8^post36+__disjvr_8^0 == 0 /\ __disjvr_3^0-__disjvr_3^post36 == 0 /\ -x1^post36+x1^0 == 0), cost: 1
  39: l25 -> l26 : __disjvr_4^0'=__disjvr_4^post39, x^0'=x^post39, __disjvr_1^0'=__disjvr_1^post39, r0^0'=r0^post39, __disjvr_6^0'=__disjvr_6^post39, __disjvr_3^0'=__disjvr_3^post39, x1^0'=x1^post39, __disjvr_0^0'=__disjvr_0^post39, __disjvr_8^0'=__disjvr_8^post39, __disjvr_5^0'=__disjvr_5^post39, __disjvr_2^0'=__disjvr_2^post39, r^0'=r^post39, __disjvr_7^0'=__disjvr_7^post39, (__disjvr_7^post39-__disjvr_7^0 == 0 /\ -__disjvr_0^post39+__disjvr_0^0 == 0 /\ -x1^post39+x1^0 == 0 /\ -__disjvr_7^post39+__disjvr_7^0 == 0 /\ -r^post39+r^0 == 0 /\ __disjvr_6^0-__disjvr_6^post39 == 0 /\ -__disjvr_2^post39+__disjvr_2^0 == 0 /\ __disjvr_4^0-__disjvr_4^post39 == 0 /\ -__disjvr_1^post39+__disjvr_1^0 == 0 /\ x^0-x^post39 == 0 /\ -__disjvr_8^post39+__disjvr_8^0 == 0 /\ r0^0-r0^post39 == 0 /\ __disjvr_3^0-__disjvr_3^post39 == 0 /\ __disjvr_5^0-__disjvr_5^post39 == 0), cost: 1
  41: l25 -> l4 : __disjvr_4^0'=__disjvr_4^post41, x^0'=x^post41, __disjvr_1^0'=__disjvr_1^post41, r0^0'=r0^post41, __disjvr_6^0'=__disjvr_6^post41, __disjvr_3^0'=__disjvr_3^post41, x1^0'=x1^post41, __disjvr_0^0'=__disjvr_0^post41, __disjvr_8^0'=__disjvr_8^post41, __disjvr_5^0'=__disjvr_5^post41, __disjvr_2^0'=__disjvr_2^post41, r^0'=r^post41, __disjvr_7^0'=__disjvr_7^post41, (-x1^post41+x1^0 == 0 /\ __disjvr_4^0-__disjvr_4^post41 == 0 /\ -__disjvr_0^post41+__disjvr_0^0 == 0 /\ -1+r^post41 == 0 /\ __disjvr_6^0-__disjvr_6^post41 == 0 /\ -__disjvr_2^post41+__disjvr_2^0 == 0 /\ -__disjvr_8^post41+__disjvr_8^0 == 0 /\ x^0-x^post41 == 0 /\ -__disjvr_7^post41+__disjvr_7^0 == 0 /\ __disjvr_5^0-__disjvr_5^post41 == 0 /\ r0^0-r0^post41 == 0 /\ __disjvr_1^0-__disjvr_1^post41 == 0 /\ __disjvr_3^0-__disjvr_3^post41 == 0), cost: 1
  42: l25 -> l19 : __disjvr_4^0'=__disjvr_4^post42, x^0'=x^post42, __disjvr_1^0'=__disjvr_1^post42, r0^0'=r0^post42, __disjvr_6^0'=__disjvr_6^post42, __disjvr_3^0'=__disjvr_3^post42, x1^0'=x1^post42, __disjvr_0^0'=__disjvr_0^post42, __disjvr_8^0'=__disjvr_8^post42, __disjvr_5^0'=__disjvr_5^post42, __disjvr_2^0'=__disjvr_2^post42, r^0'=r^post42, __disjvr_7^0'=__disjvr_7^post42, (-__disjvr_7^post42+__disjvr_7^0 == 0 /\ -__disjvr_3^post42+__disjvr_3^0 == 0 /\ __disjvr_4^0-__disjvr_4^post42 == 0 /\ -__disjvr_0^post42+__disjvr_0^0 == 0 /\ __disjvr_6^0-__disjvr_6^post42 == 0 /\ -1+x^post42 == 0 /\ -r^post42+r^0 == 0 /\ -__disjvr_2^post42+__disjvr_2^0 == 0 /\ r0^0-r0^post42 == 0 /\ __disjvr_5^0-__disjvr_5^post42 == 0 /\ -__disjvr_1^post42+__disjvr_1^0 == 0 /\ -x1^post42+x1^0 == 0 /\ -__disjvr_8^post42+__disjvr_8^0 == 0), cost: 1
  40: l26 -> l4 : __disjvr_4^0'=__disjvr_4^post40, x^0'=x^post40, __disjvr_1^0'=__disjvr_1^post40, r0^0'=r0^post40, __disjvr_6^0'=__disjvr_6^post40, __disjvr_3^0'=__disjvr_3^post40, x1^0'=x1^post40, __disjvr_0^0'=__disjvr_0^post40, __disjvr_8^0'=__disjvr_8^post40, __disjvr_5^0'=__disjvr_5^post40, __disjvr_2^0'=__disjvr_2^post40, r^0'=r^post40, __disjvr_7^0'=__disjvr_7^post40, (__disjvr_4^0-__disjvr_4^post40 == 0 /\ -__disjvr_8^post40+__disjvr_8^0 == 0 /\ r0^0-r0^post40 == 0 /\ __disjvr_6^0-__disjvr_6^post40 == 0 /\ -__disjvr_7^post40+__disjvr_7^0 == 0 /\ __disjvr_5^0-__disjvr_5^post40 == 0 /\ __disjvr_3^0-__disjvr_3^post40 == 0 /\ -x1^post40+x1^0 == 0 /\ x^0-x^post40 == 0 /\ r^post40 == 0 /\ -__disjvr_0^post40+__disjvr_0^0 == 0 /\ __disjvr_1^0-__disjvr_1^post40 == 0 /\ -__disjvr_2^post40+__disjvr_2^0 == 0), cost: 1
  43: l27 -> l28 : __disjvr_4^0'=__disjvr_4^post43, x^0'=x^post43, __disjvr_1^0'=__disjvr_1^post43, r0^0'=r0^post43, __disjvr_6^0'=__disjvr_6^post43, __disjvr_3^0'=__disjvr_3^post43, x1^0'=x1^post43, __disjvr_0^0'=__disjvr_0^post43, __disjvr_8^0'=__disjvr_8^post43, __disjvr_5^0'=__disjvr_5^post43, __disjvr_2^0'=__disjvr_2^post43, r^0'=r^post43, __disjvr_7^0'=__disjvr_7^post43, (-__disjvr_2^post43+__disjvr_2^0 == 0 /\ __disjvr_4^0-__disjvr_4^post43 == 0 /\ r^0-r^post43 == 0 /\ __disjvr_6^0-__disjvr_6^post43 == 0 /\ x^0-x^post43 == 0 /\ __disjvr_8^post43-__disjvr_8^0 == 0 /\ __disjvr_5^0-__disjvr_5^post43 == 0 /\ __disjvr_1^0-__disjvr_1^post43 == 0 /\ -x1^post43+x1^0 == 0 /\ -__disjvr_0^post43+__disjvr_0^0 == 0 /\ -__disjvr_8^post43+__disjvr_8^0 == 0 /\ __disjvr_3^0-__disjvr_3^post43 == 0 /\ -__disjvr_7^post43+__disjvr_7^0 == 0 /\ r0^0-r0^post43 == 0), cost: 1
  45: l27 -> l5 : __disjvr_4^0'=__disjvr_4^post45, x^0'=x^post45, __disjvr_1^0'=__disjvr_1^post45, r0^0'=r0^post45, __disjvr_6^0'=__disjvr_6^post45, __disjvr_3^0'=__disjvr_3^post45, x1^0'=x1^post45, __disjvr_0^0'=__disjvr_0^post45, __disjvr_8^0'=__disjvr_8^post45, __disjvr_5^0'=__disjvr_5^post45, __disjvr_2^0'=__disjvr_2^post45, r^0'=r^post45, __disjvr_7^0'=__disjvr_7^post45, (__disjvr_6^0-__disjvr_6^post45 == 0 /\ -__disjvr_8^post45+__disjvr_8^0 == 0 /\ __disjvr_4^0-__disjvr_4^post45 == 0 /\ -__disjvr_7^post45+__disjvr_7^0 == 0 /\ -r0^post45+r0^0 == 0 /\ __disjvr_3^0-__disjvr_3^post45 == 0 /\ __disjvr_5^0-__disjvr_5^post45 == 0 /\ -__disjvr_0^post45+__disjvr_0^0 == 0 /\ -1+r^post45 == 0 /\ -x1^post45+x1^0 == 0 /\ -__disjvr_2^post45+__disjvr_2^0 == 0 /\ __disjvr_1^0-__disjvr_1^post45 == 0 /\ x^0-x^post45 == 0), cost: 1
  46: l27 -> l21 : __disjvr_4^0'=__disjvr_4^post46, x^0'=x^post46, __disjvr_1^0'=__disjvr_1^post46, r0^0'=r0^post46, __disjvr_6^0'=__disjvr_6^post46, __disjvr_3^0'=__disjvr_3^post46, x1^0'=x1^post46, __disjvr_0^0'=__disjvr_0^post46, __disjvr_8^0'=__disjvr_8^post46, __disjvr_5^0'=__disjvr_5^post46, __disjvr_2^0'=__disjvr_2^post46, r^0'=r^post46, __disjvr_7^0'=__disjvr_7^post46, (-__disjvr_0^post46+__disjvr_0^0 == 0 /\ -x1^post46+x1^0 == 0 /\ __disjvr_4^0-__disjvr_4^post46 == 0 /\ -r^post46+r^0 == 0 /\ __disjvr_6^0-__disjvr_6^post46 == 0 /\ -__disjvr_2^post46+__disjvr_2^0 == 0 /\ -__disjvr_8^post46+__disjvr_8^0 == 0 /\ -__disjvr_1^post46+__disjvr_1^0 == 0 /\ -__disjvr_7^post46+__disjvr_7^0 == 0 /\ -1+x^post46 == 0 /\ __disjvr_3^0-__disjvr_3^post46 == 0 /\ __disjvr_5^0-__disjvr_5^post46 == 0 /\ r0^0-r0^post46 == 0), cost: 1
  44: l28 -> l5 : __disjvr_4^0'=__disjvr_4^post44, x^0'=x^post44, __disjvr_1^0'=__disjvr_1^post44, r0^0'=r0^post44, __disjvr_6^0'=__disjvr_6^post44, __disjvr_3^0'=__disjvr_3^post44, x1^0'=x1^post44, __disjvr_0^0'=__disjvr_0^post44, __disjvr_8^0'=__disjvr_8^post44, __disjvr_5^0'=__disjvr_5^post44, __disjvr_2^0'=__disjvr_2^post44, r^0'=r^post44, __disjvr_7^0'=__disjvr_7^post44, (-__disjvr_2^post44+__disjvr_2^0 == 0 /\ -__disjvr_3^post44+__disjvr_3^0 == 0 /\ x^0-x^post44 == 0 /\ -x1^post44+x1^0 == 0 /\ __disjvr_4^0-__disjvr_4^post44 == 0 /\ __disjvr_6^0-__disjvr_6^post44 == 0 /\ __disjvr_8^0-__disjvr_8^post44 == 0 /\ r0^0-r0^post44 == 0 /\ -__disjvr_0^post44+__disjvr_0^0 == 0 /\ -__disjvr_7^post44+__disjvr_7^0 == 0 /\ r^post44 == 0 /\ -__disjvr_1^post44+__disjvr_1^0 == 0 /\ __disjvr_5^0-__disjvr_5^post44 == 0), cost: 1
  47: l29 -> l19 : __disjvr_4^0'=__disjvr_4^post47, x^0'=x^post47, __disjvr_1^0'=__disjvr_1^post47, r0^0'=r0^post47, __disjvr_6^0'=__disjvr_6^post47, __disjvr_3^0'=__disjvr_3^post47, x1^0'=x1^post47, __disjvr_0^0'=__disjvr_0^post47, __disjvr_8^0'=__disjvr_8^post47, __disjvr_5^0'=__disjvr_5^post47, __disjvr_2^0'=__disjvr_2^post47, r^0'=r^post47, __disjvr_7^0'=__disjvr_7^post47, (-__disjvr_8^post47+__disjvr_8^0 == 0 /\ -__disjvr_7^post47+__disjvr_7^0 == 0 /\ __disjvr_4^0-__disjvr_4^post47 == 0 /\ __disjvr_6^0-__disjvr_6^post47 == 0 /\ __disjvr_5^0-__disjvr_5^post47 == 0 /\ __disjvr_3^0-__disjvr_3^post47 == 0 /\ -r^post47+r^0 == 0 /\ x^0-x^post47 == 0 /\ -__disjvr_1^post47+__disjvr_1^0 == 0 /\ -__disjvr_0^post47+__disjvr_0^0 == 0 /\ -x^0+x1^post47 == 0 /\ r0^0-r0^post47 == 0 /\ -__disjvr_2^post47+__disjvr_2^0 == 0), cost: 1
  48: l29 -> l6 : __disjvr_4^0'=__disjvr_4^post48, x^0'=x^post48, __disjvr_1^0'=__disjvr_1^post48, r0^0'=r0^post48, __disjvr_6^0'=__disjvr_6^post48, __disjvr_3^0'=__disjvr_3^post48, x1^0'=x1^post48, __disjvr_0^0'=__disjvr_0^post48, __disjvr_8^0'=__disjvr_8^post48, __disjvr_5^0'=__disjvr_5^post48, __disjvr_2^0'=__disjvr_2^post48, r^0'=r^post48, __disjvr_7^0'=__disjvr_7^post48, (__disjvr_4^0-__disjvr_4^post48 == 0 /\ __disjvr_6^0-__disjvr_6^post48 == 0 /\ -__disjvr_0^post48+__disjvr_0^0 == 0 /\ -2+x^post48 == 0 /\ r^0-r^post48 == 0 /\ -__disjvr_2^post48+__disjvr_2^0 == 0 /\ -__disjvr_7^post48+__disjvr_7^0 == 0 /\ __disjvr_5^0-__disjvr_5^post48 == 0 /\ __disjvr_1^0-__disjvr_1^post48 == 0 /\ r0^0-r0^post48 == 0 /\ __disjvr_3^0-__disjvr_3^post48 == 0 /\ -__disjvr_8^post48+__disjvr_8^0 == 0 /\ -x1^post48+x1^0 == 0), cost: 1
  49: l29 -> l3 : __disjvr_4^0'=__disjvr_4^post49, x^0'=x^post49, __disjvr_1^0'=__disjvr_1^post49, r0^0'=r0^post49, __disjvr_6^0'=__disjvr_6^post49, __disjvr_3^0'=__disjvr_3^post49, x1^0'=x1^post49, __disjvr_0^0'=__disjvr_0^post49, __disjvr_8^0'=__disjvr_8^post49, __disjvr_5^0'=__disjvr_5^post49, __disjvr_2^0'=__disjvr_2^post49, r^0'=r^post49, __disjvr_7^0'=__disjvr_7^post49, (-__disjvr_3^post49+__disjvr_3^0 == 0 /\ -__disjvr_2^post49+__disjvr_2^0 == 0 /\ x^0-x^post49 == 0 /\ __disjvr_4^0-__disjvr_4^post49 == 0 /\ -x1^post49+x1^0 == 0 /\ __disjvr_6^0-__disjvr_6^post49 == 0 /\ -__disjvr_7^post49+__disjvr_7^0 == 0 /\ -r^post49+r^0 == 0 /\ r0^0-r0^post49 == 0 /\ __disjvr_8^0-__disjvr_8^post49 == 0 /\ -__disjvr_1^post49+__disjvr_1^0 == 0 /\ -__disjvr_0^post49+__disjvr_0^0 == 0 /\ __disjvr_5^0-__disjvr_5^post49 == 0), cost: 1
  50: l30 -> l27 : __disjvr_4^0'=__disjvr_4^post50, x^0'=x^post50, __disjvr_1^0'=__disjvr_1^post50, r0^0'=r0^post50, __disjvr_6^0'=__disjvr_6^post50, __disjvr_3^0'=__disjvr_3^post50, x1^0'=x1^post50, __disjvr_0^0'=__disjvr_0^post50, __disjvr_8^0'=__disjvr_8^post50, __disjvr_5^0'=__disjvr_5^post50, __disjvr_2^0'=__disjvr_2^post50, r^0'=r^post50, __disjvr_7^0'=__disjvr_7^post50, (__disjvr_6^0-__disjvr_6^post50 == 0 /\ -__disjvr_7^post50+__disjvr_7^0 == 0 /\ __disjvr_4^0-__disjvr_4^post50 == 0 /\ -r^post50+r^0 == 0 /\ -__disjvr_0^post50+__disjvr_0^0 == 0 /\ __disjvr_5^0-__disjvr_5^post50 == 0 /\ -__disjvr_2^post50+__disjvr_2^0 == 0 /\ x^0-x^post50 == 0 /\ __disjvr_1^0-__disjvr_1^post50 == 0 /\ -__disjvr_8^post50+__disjvr_8^0 == 0 /\ -x^0+x1^post50 == 0 /\ r0^0-r0^post50 == 0 /\ __disjvr_3^0-__disjvr_3^post50 == 0), cost: 1
  51: l30 -> l29 : __disjvr_4^0'=__disjvr_4^post51, x^0'=x^post51, __disjvr_1^0'=__disjvr_1^post51, r0^0'=r0^post51, __disjvr_6^0'=__disjvr_6^post51, __disjvr_3^0'=__disjvr_3^post51, x1^0'=x1^post51, __disjvr_0^0'=__disjvr_0^post51, __disjvr_8^0'=__disjvr_8^post51, __disjvr_5^0'=__disjvr_5^post51, __disjvr_2^0'=__disjvr_2^post51, r^0'=r^post51, __disjvr_7^0'=__disjvr_7^post51, (-__disjvr_1^post51+__disjvr_1^0 == 0 /\ -__disjvr_3^post51+__disjvr_3^0 == 0 /\ r^0-r^post51 == 0 /\ -__disjvr_2^post51+__disjvr_2^0 == 0 /\ -x1^post51+x1^0 == 0 /\ -1+x^post51 == 0 /\ __disjvr_4^0-__disjvr_4^post51 == 0 /\ __disjvr_6^0-__disjvr_6^post51 == 0 /\ __disjvr_8^0-__disjvr_8^post51 == 0 /\ r0^0-r0^post51 == 0 /\ -__disjvr_7^post51+__disjvr_7^0 == 0 /\ __disjvr_5^0-__disjvr_5^post51 == 0 /\ -__disjvr_0^post51+__disjvr_0^0 == 0), cost: 1
  52: l30 -> l3 : __disjvr_4^0'=__disjvr_4^post52, x^0'=x^post52, __disjvr_1^0'=__disjvr_1^post52, r0^0'=r0^post52, __disjvr_6^0'=__disjvr_6^post52, __disjvr_3^0'=__disjvr_3^post52, x1^0'=x1^post52, __disjvr_0^0'=__disjvr_0^post52, __disjvr_8^0'=__disjvr_8^post52, __disjvr_5^0'=__disjvr_5^post52, __disjvr_2^0'=__disjvr_2^post52, r^0'=r^post52, __disjvr_7^0'=__disjvr_7^post52, (-__disjvr_1^post52+__disjvr_1^0 == 0 /\ -__disjvr_0^post52+__disjvr_0^0 == 0 /\ -x1^post52+x1^0 == 0 /\ -r^post52+r^0 == 0 /\ -__disjvr_7^post52+__disjvr_7^0 == 0 /\ __disjvr_6^0-__disjvr_6^post52 == 0 /\ -__disjvr_2^post52+__disjvr_2^0 == 0 /\ x^0-x^post52 == 0 /\ r0^0-r0^post52 == 0 /\ __disjvr_4^0-__disjvr_4^post52 == 0 /\ -__disjvr_8^post52+__disjvr_8^0 == 0 /\ __disjvr_3^0-__disjvr_3^post52 == 0 /\ __disjvr_5^0-__disjvr_5^post52 == 0), cost: 1
  53: l31 -> l30 : __disjvr_4^0'=__disjvr_4^post53, x^0'=x^post53, __disjvr_1^0'=__disjvr_1^post53, r0^0'=r0^post53, __disjvr_6^0'=__disjvr_6^post53, __disjvr_3^0'=__disjvr_3^post53, x1^0'=x1^post53, __disjvr_0^0'=__disjvr_0^post53, __disjvr_8^0'=__disjvr_8^post53, __disjvr_5^0'=__disjvr_5^post53, __disjvr_2^0'=__disjvr_2^post53, r^0'=r^post53, __disjvr_7^0'=__disjvr_7^post53, (r^0-r^post53 == 0 /\ -x1^post53+x1^0 == 0 /\ -__disjvr_7^post53+__disjvr_7^0 == 0 /\ __disjvr_6^0-__disjvr_6^post53 == 0 /\ __disjvr_4^0-__disjvr_4^post53 == 0 /\ -__disjvr_0^post53+__disjvr_0^0 == 0 /\ -__disjvr_5^post53+__disjvr_5^0 == 0 /\ __disjvr_8^0-__disjvr_8^post53 == 0 /\ x^0-x^post53 == 0 /\ -__disjvr_1^post53+__disjvr_1^0 == 0 /\ r0^0-r0^post53 == 0 /\ __disjvr_3^0-__disjvr_3^post53 == 0 /\ -__disjvr_2^post53+__disjvr_2^0 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l31
   4: l6 -> l7 : __disjvr_4^0'=__disjvr_4^post4, x^0'=x^post4, __disjvr_1^0'=__disjvr_1^post4, r0^0'=r0^post4, __disjvr_6^0'=__disjvr_6^post4, __disjvr_3^0'=__disjvr_3^post4, x1^0'=x1^post4, __disjvr_0^0'=__disjvr_0^post4, __disjvr_8^0'=__disjvr_8^post4, __disjvr_5^0'=__disjvr_5^post4, __disjvr_2^0'=__disjvr_2^post4, r^0'=r^post4, __disjvr_7^0'=__disjvr_7^post4, (__disjvr_8^0-__disjvr_8^post4 == 0 /\ -__disjvr_6^post4+__disjvr_6^0 == 0 /\ -__disjvr_7^post4+__disjvr_7^0 == 0 /\ r0^0-r0^post4 == 0 /\ __disjvr_2^0-__disjvr_2^post4 == 0 /\ -__disjvr_3^post4+__disjvr_3^0 == 0 /\ __disjvr_1^0-__disjvr_1^post4 == 0 /\ __disjvr_0^0-__disjvr_0^post4 == 0 /\ -__disjvr_5^post4+__disjvr_5^0 == 0 /\ -r^post4+r^0 == 0 /\ __disjvr_4^0-__disjvr_4^post4 == 0 /\ -x^0+x1^post4 == 0 /\ -x^post4+x^0 == 0), cost: 1
   5: l6 -> l8 : __disjvr_4^0'=__disjvr_4^post5, x^0'=x^post5, __disjvr_1^0'=__disjvr_1^post5, r0^0'=r0^post5, __disjvr_6^0'=__disjvr_6^post5, __disjvr_3^0'=__disjvr_3^post5, x1^0'=x1^post5, __disjvr_0^0'=__disjvr_0^post5, __disjvr_8^0'=__disjvr_8^post5, __disjvr_5^0'=__disjvr_5^post5, __disjvr_2^0'=__disjvr_2^post5, r^0'=r^post5, __disjvr_7^0'=__disjvr_7^post5, (__disjvr_4^0-__disjvr_4^post5 == 0 /\ x1^0-x1^post5 == 0 /\ -__disjvr_6^post5+__disjvr_6^0 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ -__disjvr_3^post5+__disjvr_3^0 == 0 /\ -r^post5+r^0 == 0 /\ __disjvr_8^0-__disjvr_8^post5 == 0 /\ -__disjvr_7^post5+__disjvr_7^0 == 0 /\ x^0-x^post5 == 0 /\ -__disjvr_2^post5+__disjvr_2^0 == 0 /\ -__disjvr_5^post5+__disjvr_5^0 == 0 /\ __disjvr_1^0-__disjvr_1^post5 == 0 /\ r0^0-r0^post5 == 0), cost: 1
  11: l7 -> l10 : __disjvr_4^0'=__disjvr_4^post11, x^0'=x^post11, __disjvr_1^0'=__disjvr_1^post11, r0^0'=r0^post11, __disjvr_6^0'=__disjvr_6^post11, __disjvr_3^0'=__disjvr_3^post11, x1^0'=x1^post11, __disjvr_0^0'=__disjvr_0^post11, __disjvr_8^0'=__disjvr_8^post11, __disjvr_5^0'=__disjvr_5^post11, __disjvr_2^0'=__disjvr_2^post11, r^0'=r^post11, __disjvr_7^0'=__disjvr_7^post11, (-__disjvr_3^post11+__disjvr_3^0 == 0 /\ -__disjvr_7^post11+__disjvr_7^0 == 0 /\ r0^0-r0^post11 == 0 /\ -__disjvr_5^post11+__disjvr_5^0 == 0 /\ x1^0-x1^post11 == 0 /\ __disjvr_8^0-__disjvr_8^post11 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ __disjvr_0^0-__disjvr_0^post11 == 0 /\ -r^post11+r^0 == 0 /\ __disjvr_1^0-__disjvr_1^post11 == 0 /\ __disjvr_4^0-__disjvr_4^post11 == 0 /\ __disjvr_6^0-__disjvr_6^post11 == 0 /\ -x^post11+x^0 == 0), cost: 1
   6: l8 -> l6 : __disjvr_4^0'=__disjvr_4^post6, x^0'=x^post6, __disjvr_1^0'=__disjvr_1^post6, r0^0'=r0^post6, __disjvr_6^0'=__disjvr_6^post6, __disjvr_3^0'=__disjvr_3^post6, x1^0'=x1^post6, __disjvr_0^0'=__disjvr_0^post6, __disjvr_8^0'=__disjvr_8^post6, __disjvr_5^0'=__disjvr_5^post6, __disjvr_2^0'=__disjvr_2^post6, r^0'=r^post6, __disjvr_7^0'=__disjvr_7^post6, (x^0-x^post6 == 0 /\ __disjvr_2^0-__disjvr_2^post6 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ __disjvr_1^0-__disjvr_1^post6 == 0 /\ __disjvr_8^0-__disjvr_8^post6 == 0 /\ r0^0-r0^post6 == 0 /\ x1^0-x1^post6 == 0 /\ __disjvr_4^0-__disjvr_4^post6 == 0 /\ __disjvr_6^0-__disjvr_6^post6 == 0 /\ -__disjvr_3^post6+__disjvr_3^0 == 0 /\ -__disjvr_5^post6+__disjvr_5^0 == 0 /\ -__disjvr_7^post6+__disjvr_7^0 == 0 /\ -r^post6+r^0 == 0), cost: 1
  12: l10 -> l7 : __disjvr_4^0'=__disjvr_4^post12, x^0'=x^post12, __disjvr_1^0'=__disjvr_1^post12, r0^0'=r0^post12, __disjvr_6^0'=__disjvr_6^post12, __disjvr_3^0'=__disjvr_3^post12, x1^0'=x1^post12, __disjvr_0^0'=__disjvr_0^post12, __disjvr_8^0'=__disjvr_8^post12, __disjvr_5^0'=__disjvr_5^post12, __disjvr_2^0'=__disjvr_2^post12, r^0'=r^post12, __disjvr_7^0'=__disjvr_7^post12, (x1^0-x1^post12 == 0 /\ __disjvr_4^0-__disjvr_4^post12 == 0 /\ -__disjvr_6^post12+__disjvr_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post12 == 0 /\ __disjvr_0^0-__disjvr_0^post12 == 0 /\ -r^post12+r^0 == 0 /\ -__disjvr_7^post12+__disjvr_7^0 == 0 /\ x^0-x^post12 == 0 /\ -__disjvr_3^post12+__disjvr_3^0 == 0 /\ -__disjvr_5^post12+__disjvr_5^0 == 0 /\ __disjvr_1^0-__disjvr_1^post12 == 0 /\ r0^0-r0^post12 == 0 /\ -__disjvr_8^post12+__disjvr_8^0 == 0), cost: 1
  16: l11 -> l13 : __disjvr_4^0'=__disjvr_4^post16, x^0'=x^post16, __disjvr_1^0'=__disjvr_1^post16, r0^0'=r0^post16, __disjvr_6^0'=__disjvr_6^post16, __disjvr_3^0'=__disjvr_3^post16, x1^0'=x1^post16, __disjvr_0^0'=__disjvr_0^post16, __disjvr_8^0'=__disjvr_8^post16, __disjvr_5^0'=__disjvr_5^post16, __disjvr_2^0'=__disjvr_2^post16, r^0'=r^post16, __disjvr_7^0'=__disjvr_7^post16, (__disjvr_0^0-__disjvr_0^post16 == 0 /\ -__disjvr_2^post16+__disjvr_2^0 == 0 /\ __disjvr_1^0-__disjvr_1^post16 == 0 /\ __disjvr_4^0-__disjvr_4^post16 == 0 /\ -__disjvr_5^post16+__disjvr_5^0 == 0 /\ -__disjvr_6^post16+__disjvr_6^0 == 0 /\ x^0-x^post16 == 0 /\ -__disjvr_8^post16+__disjvr_8^0 == 0 /\ r0^0-r0^post16 == 0 /\ __disjvr_3^0-__disjvr_3^post16 == 0 /\ -__disjvr_7^post16+__disjvr_7^0 == 0 /\ -r^post16+r^0 == 0 /\ x1^0-x1^post16 == 0), cost: 1
  17: l13 -> l11 : __disjvr_4^0'=__disjvr_4^post17, x^0'=x^post17, __disjvr_1^0'=__disjvr_1^post17, r0^0'=r0^post17, __disjvr_6^0'=__disjvr_6^post17, __disjvr_3^0'=__disjvr_3^post17, x1^0'=x1^post17, __disjvr_0^0'=__disjvr_0^post17, __disjvr_8^0'=__disjvr_8^post17, __disjvr_5^0'=__disjvr_5^post17, __disjvr_2^0'=__disjvr_2^post17, r^0'=r^post17, __disjvr_7^0'=__disjvr_7^post17, (__disjvr_3^0-__disjvr_3^post17 == 0 /\ -__disjvr_6^post17+__disjvr_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ -r^post17+r^0 == 0 /\ -__disjvr_8^post17+__disjvr_8^0 == 0 /\ x^0-x^post17 == 0 /\ __disjvr_1^0-__disjvr_1^post17 == 0 /\ r0^0-r0^post17 == 0 /\ -__disjvr_5^post17+__disjvr_5^0 == 0 /\ x1^0-x1^post17 == 0 /\ __disjvr_4^0-__disjvr_4^post17 == 0 /\ -__disjvr_7^post17+__disjvr_7^0 == 0), cost: 1
  21: l14 -> l16 : __disjvr_4^0'=__disjvr_4^post21, x^0'=x^post21, __disjvr_1^0'=__disjvr_1^post21, r0^0'=r0^post21, __disjvr_6^0'=__disjvr_6^post21, __disjvr_3^0'=__disjvr_3^post21, x1^0'=x1^post21, __disjvr_0^0'=__disjvr_0^post21, __disjvr_8^0'=__disjvr_8^post21, __disjvr_5^0'=__disjvr_5^post21, __disjvr_2^0'=__disjvr_2^post21, r^0'=r^post21, __disjvr_7^0'=__disjvr_7^post21, (-__disjvr_7^post21+__disjvr_7^0 == 0 /\ __disjvr_1^0-__disjvr_1^post21 == 0 /\ __disjvr_3^0-__disjvr_3^post21 == 0 /\ x^0-x^post21 == 0 /\ __disjvr_4^0-__disjvr_4^post21 == 0 /\ -r^post21+r^0 == 0 /\ __disjvr_0^0-__disjvr_0^post21 == 0 /\ -__disjvr_2^post21+__disjvr_2^0 == 0 /\ r0^0-r0^post21 == 0 /\ -__disjvr_5^post21+__disjvr_5^0 == 0 /\ x1^0-x1^post21 == 0 /\ -__disjvr_6^post21+__disjvr_6^0 == 0 /\ -__disjvr_8^post21+__disjvr_8^0 == 0), cost: 1
  22: l16 -> l14 : __disjvr_4^0'=__disjvr_4^post22, x^0'=x^post22, __disjvr_1^0'=__disjvr_1^post22, r0^0'=r0^post22, __disjvr_6^0'=__disjvr_6^post22, __disjvr_3^0'=__disjvr_3^post22, x1^0'=x1^post22, __disjvr_0^0'=__disjvr_0^post22, __disjvr_8^0'=__disjvr_8^post22, __disjvr_5^0'=__disjvr_5^post22, __disjvr_2^0'=__disjvr_2^post22, r^0'=r^post22, __disjvr_7^0'=__disjvr_7^post22, (x^0-x^post22 == 0 /\ -__disjvr_2^post22+__disjvr_2^0 == 0 /\ __disjvr_1^0-__disjvr_1^post22 == 0 /\ -__disjvr_6^post22+__disjvr_6^0 == 0 /\ __disjvr_3^0-__disjvr_3^post22 == 0 /\ __disjvr_0^0-__disjvr_0^post22 == 0 /\ x1^0-x1^post22 == 0 /\ __disjvr_4^0-__disjvr_4^post22 == 0 /\ -r0^post22+r0^0 == 0 /\ -__disjvr_5^post22+__disjvr_5^0 == 0 /\ -__disjvr_8^post22+__disjvr_8^0 == 0 /\ -__disjvr_7^post22+__disjvr_7^0 == 0 /\ -r^post22+r^0 == 0), cost: 1
  30: l19 -> l11 : __disjvr_4^0'=__disjvr_4^post30, x^0'=x^post30, __disjvr_1^0'=__disjvr_1^post30, r0^0'=r0^post30, __disjvr_6^0'=__disjvr_6^post30, __disjvr_3^0'=__disjvr_3^post30, x1^0'=x1^post30, __disjvr_0^0'=__disjvr_0^post30, __disjvr_8^0'=__disjvr_8^post30, __disjvr_5^0'=__disjvr_5^post30, __disjvr_2^0'=__disjvr_2^post30, r^0'=r^post30, __disjvr_7^0'=__disjvr_7^post30, (__disjvr_3^0-__disjvr_3^post30 == 0 /\ -__disjvr_6^post30+__disjvr_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post30 == 0 /\ -__disjvr_8^post30+__disjvr_8^0 == 0 /\ __disjvr_1^0-__disjvr_1^post30 == 0 /\ -__disjvr_5^post30+__disjvr_5^0 == 0 /\ r0^0-r0^post30 == 0 /\ x1^0-x1^post30 == 0 /\ -__disjvr_7^post30+__disjvr_7^0 == 0 /\ -r^post30+r^0 == 0 /\ -__disjvr_2^post30+__disjvr_2^0 == 0 /\ -2+x^post30 == 0 /\ __disjvr_4^0-__disjvr_4^post30 == 0), cost: 1
  34: l21 -> l14 : __disjvr_4^0'=__disjvr_4^post34, x^0'=x^post34, __disjvr_1^0'=__disjvr_1^post34, r0^0'=r0^post34, __disjvr_6^0'=__disjvr_6^post34, __disjvr_3^0'=__disjvr_3^post34, x1^0'=x1^post34, __disjvr_0^0'=__disjvr_0^post34, __disjvr_8^0'=__disjvr_8^post34, __disjvr_5^0'=__disjvr_5^post34, __disjvr_2^0'=__disjvr_2^post34, r^0'=r^post34, __disjvr_7^0'=__disjvr_7^post34, (-2+x^post34 == 0 /\ -r^post34+r^0 == 0 /\ -r0^post34+r0^0 == 0 /\ __disjvr_0^0-__disjvr_0^post34 == 0 /\ -__disjvr_2^post34+__disjvr_2^0 == 0 /\ -__disjvr_8^post34+__disjvr_8^0 == 0 /\ -x1^post34+x1^0 == 0 /\ __disjvr_5^0-__disjvr_5^post34 == 0 /\ -__disjvr_7^post34+__disjvr_7^0 == 0 /\ __disjvr_1^0-__disjvr_1^post34 == 0 /\ __disjvr_3^0-__disjvr_3^post34 == 0 /\ __disjvr_4^0-__disjvr_4^post34 == 0 /\ __disjvr_6^0-__disjvr_6^post34 == 0), cost: 1
  46: l27 -> l21 : __disjvr_4^0'=__disjvr_4^post46, x^0'=x^post46, __disjvr_1^0'=__disjvr_1^post46, r0^0'=r0^post46, __disjvr_6^0'=__disjvr_6^post46, __disjvr_3^0'=__disjvr_3^post46, x1^0'=x1^post46, __disjvr_0^0'=__disjvr_0^post46, __disjvr_8^0'=__disjvr_8^post46, __disjvr_5^0'=__disjvr_5^post46, __disjvr_2^0'=__disjvr_2^post46, r^0'=r^post46, __disjvr_7^0'=__disjvr_7^post46, (-__disjvr_0^post46+__disjvr_0^0 == 0 /\ -x1^post46+x1^0 == 0 /\ __disjvr_4^0-__disjvr_4^post46 == 0 /\ -r^post46+r^0 == 0 /\ __disjvr_6^0-__disjvr_6^post46 == 0 /\ -__disjvr_2^post46+__disjvr_2^0 == 0 /\ -__disjvr_8^post46+__disjvr_8^0 == 0 /\ -__disjvr_1^post46+__disjvr_1^0 == 0 /\ -__disjvr_7^post46+__disjvr_7^0 == 0 /\ -1+x^post46 == 0 /\ __disjvr_3^0-__disjvr_3^post46 == 0 /\ __disjvr_5^0-__disjvr_5^post46 == 0 /\ r0^0-r0^post46 == 0), cost: 1
  47: l29 -> l19 : __disjvr_4^0'=__disjvr_4^post47, x^0'=x^post47, __disjvr_1^0'=__disjvr_1^post47, r0^0'=r0^post47, __disjvr_6^0'=__disjvr_6^post47, __disjvr_3^0'=__disjvr_3^post47, x1^0'=x1^post47, __disjvr_0^0'=__disjvr_0^post47, __disjvr_8^0'=__disjvr_8^post47, __disjvr_5^0'=__disjvr_5^post47, __disjvr_2^0'=__disjvr_2^post47, r^0'=r^post47, __disjvr_7^0'=__disjvr_7^post47, (-__disjvr_8^post47+__disjvr_8^0 == 0 /\ -__disjvr_7^post47+__disjvr_7^0 == 0 /\ __disjvr_4^0-__disjvr_4^post47 == 0 /\ __disjvr_6^0-__disjvr_6^post47 == 0 /\ __disjvr_5^0-__disjvr_5^post47 == 0 /\ __disjvr_3^0-__disjvr_3^post47 == 0 /\ -r^post47+r^0 == 0 /\ x^0-x^post47 == 0 /\ -__disjvr_1^post47+__disjvr_1^0 == 0 /\ -__disjvr_0^post47+__disjvr_0^0 == 0 /\ -x^0+x1^post47 == 0 /\ r0^0-r0^post47 == 0 /\ -__disjvr_2^post47+__disjvr_2^0 == 0), cost: 1
  48: l29 -> l6 : __disjvr_4^0'=__disjvr_4^post48, x^0'=x^post48, __disjvr_1^0'=__disjvr_1^post48, r0^0'=r0^post48, __disjvr_6^0'=__disjvr_6^post48, __disjvr_3^0'=__disjvr_3^post48, x1^0'=x1^post48, __disjvr_0^0'=__disjvr_0^post48, __disjvr_8^0'=__disjvr_8^post48, __disjvr_5^0'=__disjvr_5^post48, __disjvr_2^0'=__disjvr_2^post48, r^0'=r^post48, __disjvr_7^0'=__disjvr_7^post48, (__disjvr_4^0-__disjvr_4^post48 == 0 /\ __disjvr_6^0-__disjvr_6^post48 == 0 /\ -__disjvr_0^post48+__disjvr_0^0 == 0 /\ -2+x^post48 == 0 /\ r^0-r^post48 == 0 /\ -__disjvr_2^post48+__disjvr_2^0 == 0 /\ -__disjvr_7^post48+__disjvr_7^0 == 0 /\ __disjvr_5^0-__disjvr_5^post48 == 0 /\ __disjvr_1^0-__disjvr_1^post48 == 0 /\ r0^0-r0^post48 == 0 /\ __disjvr_3^0-__disjvr_3^post48 == 0 /\ -__disjvr_8^post48+__disjvr_8^0 == 0 /\ -x1^post48+x1^0 == 0), cost: 1
  50: l30 -> l27 : __disjvr_4^0'=__disjvr_4^post50, x^0'=x^post50, __disjvr_1^0'=__disjvr_1^post50, r0^0'=r0^post50, __disjvr_6^0'=__disjvr_6^post50, __disjvr_3^0'=__disjvr_3^post50, x1^0'=x1^post50, __disjvr_0^0'=__disjvr_0^post50, __disjvr_8^0'=__disjvr_8^post50, __disjvr_5^0'=__disjvr_5^post50, __disjvr_2^0'=__disjvr_2^post50, r^0'=r^post50, __disjvr_7^0'=__disjvr_7^post50, (__disjvr_6^0-__disjvr_6^post50 == 0 /\ -__disjvr_7^post50+__disjvr_7^0 == 0 /\ __disjvr_4^0-__disjvr_4^post50 == 0 /\ -r^post50+r^0 == 0 /\ -__disjvr_0^post50+__disjvr_0^0 == 0 /\ __disjvr_5^0-__disjvr_5^post50 == 0 /\ -__disjvr_2^post50+__disjvr_2^0 == 0 /\ x^0-x^post50 == 0 /\ __disjvr_1^0-__disjvr_1^post50 == 0 /\ -__disjvr_8^post50+__disjvr_8^0 == 0 /\ -x^0+x1^post50 == 0 /\ r0^0-r0^post50 == 0 /\ __disjvr_3^0-__disjvr_3^post50 == 0), cost: 1
  51: l30 -> l29 : __disjvr_4^0'=__disjvr_4^post51, x^0'=x^post51, __disjvr_1^0'=__disjvr_1^post51, r0^0'=r0^post51, __disjvr_6^0'=__disjvr_6^post51, __disjvr_3^0'=__disjvr_3^post51, x1^0'=x1^post51, __disjvr_0^0'=__disjvr_0^post51, __disjvr_8^0'=__disjvr_8^post51, __disjvr_5^0'=__disjvr_5^post51, __disjvr_2^0'=__disjvr_2^post51, r^0'=r^post51, __disjvr_7^0'=__disjvr_7^post51, (-__disjvr_1^post51+__disjvr_1^0 == 0 /\ -__disjvr_3^post51+__disjvr_3^0 == 0 /\ r^0-r^post51 == 0 /\ -__disjvr_2^post51+__disjvr_2^0 == 0 /\ -x1^post51+x1^0 == 0 /\ -1+x^post51 == 0 /\ __disjvr_4^0-__disjvr_4^post51 == 0 /\ __disjvr_6^0-__disjvr_6^post51 == 0 /\ __disjvr_8^0-__disjvr_8^post51 == 0 /\ r0^0-r0^post51 == 0 /\ -__disjvr_7^post51+__disjvr_7^0 == 0 /\ __disjvr_5^0-__disjvr_5^post51 == 0 /\ -__disjvr_0^post51+__disjvr_0^0 == 0), cost: 1
  53: l31 -> l30 : __disjvr_4^0'=__disjvr_4^post53, x^0'=x^post53, __disjvr_1^0'=__disjvr_1^post53, r0^0'=r0^post53, __disjvr_6^0'=__disjvr_6^post53, __disjvr_3^0'=__disjvr_3^post53, x1^0'=x1^post53, __disjvr_0^0'=__disjvr_0^post53, __disjvr_8^0'=__disjvr_8^post53, __disjvr_5^0'=__disjvr_5^post53, __disjvr_2^0'=__disjvr_2^post53, r^0'=r^post53, __disjvr_7^0'=__disjvr_7^post53, (r^0-r^post53 == 0 /\ -x1^post53+x1^0 == 0 /\ -__disjvr_7^post53+__disjvr_7^0 == 0 /\ __disjvr_6^0-__disjvr_6^post53 == 0 /\ __disjvr_4^0-__disjvr_4^post53 == 0 /\ -__disjvr_0^post53+__disjvr_0^0 == 0 /\ -__disjvr_5^post53+__disjvr_5^0 == 0 /\ __disjvr_8^0-__disjvr_8^post53 == 0 /\ x^0-x^post53 == 0 /\ -__disjvr_1^post53+__disjvr_1^0 == 0 /\ r0^0-r0^post53 == 0 /\ __disjvr_3^0-__disjvr_3^post53 == 0 /\ -__disjvr_2^post53+__disjvr_2^0 == 0), cost: 1


Applied preprocessing
Original rule:
l6 -> l7 : __disjvr_4^0'=__disjvr_4^post4, x^0'=x^post4, __disjvr_1^0'=__disjvr_1^post4, r0^0'=r0^post4, __disjvr_6^0'=__disjvr_6^post4, __disjvr_3^0'=__disjvr_3^post4, x1^0'=x1^post4, __disjvr_0^0'=__disjvr_0^post4, __disjvr_8^0'=__disjvr_8^post4, __disjvr_5^0'=__disjvr_5^post4, __disjvr_2^0'=__disjvr_2^post4, r^0'=r^post4, __disjvr_7^0'=__disjvr_7^post4, (__disjvr_8^0-__disjvr_8^post4 == 0 /\ -__disjvr_6^post4+__disjvr_6^0 == 0 /\ -__disjvr_7^post4+__disjvr_7^0 == 0 /\ r0^0-r0^post4 == 0 /\ __disjvr_2^0-__disjvr_2^post4 == 0 /\ -__disjvr_3^post4+__disjvr_3^0 == 0 /\ __disjvr_1^0-__disjvr_1^post4 == 0 /\ __disjvr_0^0-__disjvr_0^post4 == 0 /\ -__disjvr_5^post4+__disjvr_5^0 == 0 /\ -r^post4+r^0 == 0 /\ __disjvr_4^0-__disjvr_4^post4 == 0 /\ -x^0+x1^post4 == 0 /\ -x^post4+x^0 == 0), cost: 1
New rule:
l6 -> l7 : x1^0'=x^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l6 -> l8 : __disjvr_4^0'=__disjvr_4^post5, x^0'=x^post5, __disjvr_1^0'=__disjvr_1^post5, r0^0'=r0^post5, __disjvr_6^0'=__disjvr_6^post5, __disjvr_3^0'=__disjvr_3^post5, x1^0'=x1^post5, __disjvr_0^0'=__disjvr_0^post5, __disjvr_8^0'=__disjvr_8^post5, __disjvr_5^0'=__disjvr_5^post5, __disjvr_2^0'=__disjvr_2^post5, r^0'=r^post5, __disjvr_7^0'=__disjvr_7^post5, (__disjvr_4^0-__disjvr_4^post5 == 0 /\ x1^0-x1^post5 == 0 /\ -__disjvr_6^post5+__disjvr_6^0 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ -__disjvr_3^post5+__disjvr_3^0 == 0 /\ -r^post5+r^0 == 0 /\ __disjvr_8^0-__disjvr_8^post5 == 0 /\ -__disjvr_7^post5+__disjvr_7^0 == 0 /\ x^0-x^post5 == 0 /\ -__disjvr_2^post5+__disjvr_2^0 == 0 /\ -__disjvr_5^post5+__disjvr_5^0 == 0 /\ __disjvr_1^0-__disjvr_1^post5 == 0 /\ r0^0-r0^post5 == 0), cost: 1
New rule:
l6 -> l8 : TRUE, cost: 1

Applied preprocessing
Original rule:
l8 -> l6 : __disjvr_4^0'=__disjvr_4^post6, x^0'=x^post6, __disjvr_1^0'=__disjvr_1^post6, r0^0'=r0^post6, __disjvr_6^0'=__disjvr_6^post6, __disjvr_3^0'=__disjvr_3^post6, x1^0'=x1^post6, __disjvr_0^0'=__disjvr_0^post6, __disjvr_8^0'=__disjvr_8^post6, __disjvr_5^0'=__disjvr_5^post6, __disjvr_2^0'=__disjvr_2^post6, r^0'=r^post6, __disjvr_7^0'=__disjvr_7^post6, (x^0-x^post6 == 0 /\ __disjvr_2^0-__disjvr_2^post6 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ __disjvr_1^0-__disjvr_1^post6 == 0 /\ __disjvr_8^0-__disjvr_8^post6 == 0 /\ r0^0-r0^post6 == 0 /\ x1^0-x1^post6 == 0 /\ __disjvr_4^0-__disjvr_4^post6 == 0 /\ __disjvr_6^0-__disjvr_6^post6 == 0 /\ -__disjvr_3^post6+__disjvr_3^0 == 0 /\ -__disjvr_5^post6+__disjvr_5^0 == 0 /\ -__disjvr_7^post6+__disjvr_7^0 == 0 /\ -r^post6+r^0 == 0), cost: 1
New rule:
l8 -> l6 : TRUE, cost: 1

Applied preprocessing
Original rule:
l7 -> l10 : __disjvr_4^0'=__disjvr_4^post11, x^0'=x^post11, __disjvr_1^0'=__disjvr_1^post11, r0^0'=r0^post11, __disjvr_6^0'=__disjvr_6^post11, __disjvr_3^0'=__disjvr_3^post11, x1^0'=x1^post11, __disjvr_0^0'=__disjvr_0^post11, __disjvr_8^0'=__disjvr_8^post11, __disjvr_5^0'=__disjvr_5^post11, __disjvr_2^0'=__disjvr_2^post11, r^0'=r^post11, __disjvr_7^0'=__disjvr_7^post11, (-__disjvr_3^post11+__disjvr_3^0 == 0 /\ -__disjvr_7^post11+__disjvr_7^0 == 0 /\ r0^0-r0^post11 == 0 /\ -__disjvr_5^post11+__disjvr_5^0 == 0 /\ x1^0-x1^post11 == 0 /\ __disjvr_8^0-__disjvr_8^post11 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ __disjvr_0^0-__disjvr_0^post11 == 0 /\ -r^post11+r^0 == 0 /\ __disjvr_1^0-__disjvr_1^post11 == 0 /\ __disjvr_4^0-__disjvr_4^post11 == 0 /\ __disjvr_6^0-__disjvr_6^post11 == 0 /\ -x^post11+x^0 == 0), cost: 1
New rule:
l7 -> l10 : TRUE, cost: 1

Applied preprocessing
Original rule:
l10 -> l7 : __disjvr_4^0'=__disjvr_4^post12, x^0'=x^post12, __disjvr_1^0'=__disjvr_1^post12, r0^0'=r0^post12, __disjvr_6^0'=__disjvr_6^post12, __disjvr_3^0'=__disjvr_3^post12, x1^0'=x1^post12, __disjvr_0^0'=__disjvr_0^post12, __disjvr_8^0'=__disjvr_8^post12, __disjvr_5^0'=__disjvr_5^post12, __disjvr_2^0'=__disjvr_2^post12, r^0'=r^post12, __disjvr_7^0'=__disjvr_7^post12, (x1^0-x1^post12 == 0 /\ __disjvr_4^0-__disjvr_4^post12 == 0 /\ -__disjvr_6^post12+__disjvr_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post12 == 0 /\ __disjvr_0^0-__disjvr_0^post12 == 0 /\ -r^post12+r^0 == 0 /\ -__disjvr_7^post12+__disjvr_7^0 == 0 /\ x^0-x^post12 == 0 /\ -__disjvr_3^post12+__disjvr_3^0 == 0 /\ -__disjvr_5^post12+__disjvr_5^0 == 0 /\ __disjvr_1^0-__disjvr_1^post12 == 0 /\ r0^0-r0^post12 == 0 /\ -__disjvr_8^post12+__disjvr_8^0 == 0), cost: 1
New rule:
l10 -> l7 : TRUE, cost: 1

Applied preprocessing
Original rule:
l11 -> l13 : __disjvr_4^0'=__disjvr_4^post16, x^0'=x^post16, __disjvr_1^0'=__disjvr_1^post16, r0^0'=r0^post16, __disjvr_6^0'=__disjvr_6^post16, __disjvr_3^0'=__disjvr_3^post16, x1^0'=x1^post16, __disjvr_0^0'=__disjvr_0^post16, __disjvr_8^0'=__disjvr_8^post16, __disjvr_5^0'=__disjvr_5^post16, __disjvr_2^0'=__disjvr_2^post16, r^0'=r^post16, __disjvr_7^0'=__disjvr_7^post16, (__disjvr_0^0-__disjvr_0^post16 == 0 /\ -__disjvr_2^post16+__disjvr_2^0 == 0 /\ __disjvr_1^0-__disjvr_1^post16 == 0 /\ __disjvr_4^0-__disjvr_4^post16 == 0 /\ -__disjvr_5^post16+__disjvr_5^0 == 0 /\ -__disjvr_6^post16+__disjvr_6^0 == 0 /\ x^0-x^post16 == 0 /\ -__disjvr_8^post16+__disjvr_8^0 == 0 /\ r0^0-r0^post16 == 0 /\ __disjvr_3^0-__disjvr_3^post16 == 0 /\ -__disjvr_7^post16+__disjvr_7^0 == 0 /\ -r^post16+r^0 == 0 /\ x1^0-x1^post16 == 0), cost: 1
New rule:
l11 -> l13 : TRUE, cost: 1

Applied preprocessing
Original rule:
l13 -> l11 : __disjvr_4^0'=__disjvr_4^post17, x^0'=x^post17, __disjvr_1^0'=__disjvr_1^post17, r0^0'=r0^post17, __disjvr_6^0'=__disjvr_6^post17, __disjvr_3^0'=__disjvr_3^post17, x1^0'=x1^post17, __disjvr_0^0'=__disjvr_0^post17, __disjvr_8^0'=__disjvr_8^post17, __disjvr_5^0'=__disjvr_5^post17, __disjvr_2^0'=__disjvr_2^post17, r^0'=r^post17, __disjvr_7^0'=__disjvr_7^post17, (__disjvr_3^0-__disjvr_3^post17 == 0 /\ -__disjvr_6^post17+__disjvr_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ -r^post17+r^0 == 0 /\ -__disjvr_8^post17+__disjvr_8^0 == 0 /\ x^0-x^post17 == 0 /\ __disjvr_1^0-__disjvr_1^post17 == 0 /\ r0^0-r0^post17 == 0 /\ -__disjvr_5^post17+__disjvr_5^0 == 0 /\ x1^0-x1^post17 == 0 /\ __disjvr_4^0-__disjvr_4^post17 == 0 /\ -__disjvr_7^post17+__disjvr_7^0 == 0), cost: 1
New rule:
l13 -> l11 : TRUE, cost: 1

Applied preprocessing
Original rule:
l14 -> l16 : __disjvr_4^0'=__disjvr_4^post21, x^0'=x^post21, __disjvr_1^0'=__disjvr_1^post21, r0^0'=r0^post21, __disjvr_6^0'=__disjvr_6^post21, __disjvr_3^0'=__disjvr_3^post21, x1^0'=x1^post21, __disjvr_0^0'=__disjvr_0^post21, __disjvr_8^0'=__disjvr_8^post21, __disjvr_5^0'=__disjvr_5^post21, __disjvr_2^0'=__disjvr_2^post21, r^0'=r^post21, __disjvr_7^0'=__disjvr_7^post21, (-__disjvr_7^post21+__disjvr_7^0 == 0 /\ __disjvr_1^0-__disjvr_1^post21 == 0 /\ __disjvr_3^0-__disjvr_3^post21 == 0 /\ x^0-x^post21 == 0 /\ __disjvr_4^0-__disjvr_4^post21 == 0 /\ -r^post21+r^0 == 0 /\ __disjvr_0^0-__disjvr_0^post21 == 0 /\ -__disjvr_2^post21+__disjvr_2^0 == 0 /\ r0^0-r0^post21 == 0 /\ -__disjvr_5^post21+__disjvr_5^0 == 0 /\ x1^0-x1^post21 == 0 /\ -__disjvr_6^post21+__disjvr_6^0 == 0 /\ -__disjvr_8^post21+__disjvr_8^0 == 0), cost: 1
New rule:
l14 -> l16 : TRUE, cost: 1

Applied preprocessing
Original rule:
l16 -> l14 : __disjvr_4^0'=__disjvr_4^post22, x^0'=x^post22, __disjvr_1^0'=__disjvr_1^post22, r0^0'=r0^post22, __disjvr_6^0'=__disjvr_6^post22, __disjvr_3^0'=__disjvr_3^post22, x1^0'=x1^post22, __disjvr_0^0'=__disjvr_0^post22, __disjvr_8^0'=__disjvr_8^post22, __disjvr_5^0'=__disjvr_5^post22, __disjvr_2^0'=__disjvr_2^post22, r^0'=r^post22, __disjvr_7^0'=__disjvr_7^post22, (x^0-x^post22 == 0 /\ -__disjvr_2^post22+__disjvr_2^0 == 0 /\ __disjvr_1^0-__disjvr_1^post22 == 0 /\ -__disjvr_6^post22+__disjvr_6^0 == 0 /\ __disjvr_3^0-__disjvr_3^post22 == 0 /\ __disjvr_0^0-__disjvr_0^post22 == 0 /\ x1^0-x1^post22 == 0 /\ __disjvr_4^0-__disjvr_4^post22 == 0 /\ -r0^post22+r0^0 == 0 /\ -__disjvr_5^post22+__disjvr_5^0 == 0 /\ -__disjvr_8^post22+__disjvr_8^0 == 0 /\ -__disjvr_7^post22+__disjvr_7^0 == 0 /\ -r^post22+r^0 == 0), cost: 1
New rule:
l16 -> l14 : TRUE, cost: 1

Applied preprocessing
Original rule:
l19 -> l11 : __disjvr_4^0'=__disjvr_4^post30, x^0'=x^post30, __disjvr_1^0'=__disjvr_1^post30, r0^0'=r0^post30, __disjvr_6^0'=__disjvr_6^post30, __disjvr_3^0'=__disjvr_3^post30, x1^0'=x1^post30, __disjvr_0^0'=__disjvr_0^post30, __disjvr_8^0'=__disjvr_8^post30, __disjvr_5^0'=__disjvr_5^post30, __disjvr_2^0'=__disjvr_2^post30, r^0'=r^post30, __disjvr_7^0'=__disjvr_7^post30, (__disjvr_3^0-__disjvr_3^post30 == 0 /\ -__disjvr_6^post30+__disjvr_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post30 == 0 /\ -__disjvr_8^post30+__disjvr_8^0 == 0 /\ __disjvr_1^0-__disjvr_1^post30 == 0 /\ -__disjvr_5^post30+__disjvr_5^0 == 0 /\ r0^0-r0^post30 == 0 /\ x1^0-x1^post30 == 0 /\ -__disjvr_7^post30+__disjvr_7^0 == 0 /\ -r^post30+r^0 == 0 /\ -__disjvr_2^post30+__disjvr_2^0 == 0 /\ -2+x^post30 == 0 /\ __disjvr_4^0-__disjvr_4^post30 == 0), cost: 1
New rule:
l19 -> l11 : x^0'=2, TRUE, cost: 1

Applied preprocessing
Original rule:
l21 -> l14 : __disjvr_4^0'=__disjvr_4^post34, x^0'=x^post34, __disjvr_1^0'=__disjvr_1^post34, r0^0'=r0^post34, __disjvr_6^0'=__disjvr_6^post34, __disjvr_3^0'=__disjvr_3^post34, x1^0'=x1^post34, __disjvr_0^0'=__disjvr_0^post34, __disjvr_8^0'=__disjvr_8^post34, __disjvr_5^0'=__disjvr_5^post34, __disjvr_2^0'=__disjvr_2^post34, r^0'=r^post34, __disjvr_7^0'=__disjvr_7^post34, (-2+x^post34 == 0 /\ -r^post34+r^0 == 0 /\ -r0^post34+r0^0 == 0 /\ __disjvr_0^0-__disjvr_0^post34 == 0 /\ -__disjvr_2^post34+__disjvr_2^0 == 0 /\ -__disjvr_8^post34+__disjvr_8^0 == 0 /\ -x1^post34+x1^0 == 0 /\ __disjvr_5^0-__disjvr_5^post34 == 0 /\ -__disjvr_7^post34+__disjvr_7^0 == 0 /\ __disjvr_1^0-__disjvr_1^post34 == 0 /\ __disjvr_3^0-__disjvr_3^post34 == 0 /\ __disjvr_4^0-__disjvr_4^post34 == 0 /\ __disjvr_6^0-__disjvr_6^post34 == 0), cost: 1
New rule:
l21 -> l14 : x^0'=2, TRUE, cost: 1

Applied preprocessing
Original rule:
l27 -> l21 : __disjvr_4^0'=__disjvr_4^post46, x^0'=x^post46, __disjvr_1^0'=__disjvr_1^post46, r0^0'=r0^post46, __disjvr_6^0'=__disjvr_6^post46, __disjvr_3^0'=__disjvr_3^post46, x1^0'=x1^post46, __disjvr_0^0'=__disjvr_0^post46, __disjvr_8^0'=__disjvr_8^post46, __disjvr_5^0'=__disjvr_5^post46, __disjvr_2^0'=__disjvr_2^post46, r^0'=r^post46, __disjvr_7^0'=__disjvr_7^post46, (-__disjvr_0^post46+__disjvr_0^0 == 0 /\ -x1^post46+x1^0 == 0 /\ __disjvr_4^0-__disjvr_4^post46 == 0 /\ -r^post46+r^0 == 0 /\ __disjvr_6^0-__disjvr_6^post46 == 0 /\ -__disjvr_2^post46+__disjvr_2^0 == 0 /\ -__disjvr_8^post46+__disjvr_8^0 == 0 /\ -__disjvr_1^post46+__disjvr_1^0 == 0 /\ -__disjvr_7^post46+__disjvr_7^0 == 0 /\ -1+x^post46 == 0 /\ __disjvr_3^0-__disjvr_3^post46 == 0 /\ __disjvr_5^0-__disjvr_5^post46 == 0 /\ r0^0-r0^post46 == 0), cost: 1
New rule:
l27 -> l21 : x^0'=1, TRUE, cost: 1

Applied preprocessing
Original rule:
l29 -> l19 : __disjvr_4^0'=__disjvr_4^post47, x^0'=x^post47, __disjvr_1^0'=__disjvr_1^post47, r0^0'=r0^post47, __disjvr_6^0'=__disjvr_6^post47, __disjvr_3^0'=__disjvr_3^post47, x1^0'=x1^post47, __disjvr_0^0'=__disjvr_0^post47, __disjvr_8^0'=__disjvr_8^post47, __disjvr_5^0'=__disjvr_5^post47, __disjvr_2^0'=__disjvr_2^post47, r^0'=r^post47, __disjvr_7^0'=__disjvr_7^post47, (-__disjvr_8^post47+__disjvr_8^0 == 0 /\ -__disjvr_7^post47+__disjvr_7^0 == 0 /\ __disjvr_4^0-__disjvr_4^post47 == 0 /\ __disjvr_6^0-__disjvr_6^post47 == 0 /\ __disjvr_5^0-__disjvr_5^post47 == 0 /\ __disjvr_3^0-__disjvr_3^post47 == 0 /\ -r^post47+r^0 == 0 /\ x^0-x^post47 == 0 /\ -__disjvr_1^post47+__disjvr_1^0 == 0 /\ -__disjvr_0^post47+__disjvr_0^0 == 0 /\ -x^0+x1^post47 == 0 /\ r0^0-r0^post47 == 0 /\ -__disjvr_2^post47+__disjvr_2^0 == 0), cost: 1
New rule:
l29 -> l19 : x1^0'=x^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l29 -> l6 : __disjvr_4^0'=__disjvr_4^post48, x^0'=x^post48, __disjvr_1^0'=__disjvr_1^post48, r0^0'=r0^post48, __disjvr_6^0'=__disjvr_6^post48, __disjvr_3^0'=__disjvr_3^post48, x1^0'=x1^post48, __disjvr_0^0'=__disjvr_0^post48, __disjvr_8^0'=__disjvr_8^post48, __disjvr_5^0'=__disjvr_5^post48, __disjvr_2^0'=__disjvr_2^post48, r^0'=r^post48, __disjvr_7^0'=__disjvr_7^post48, (__disjvr_4^0-__disjvr_4^post48 == 0 /\ __disjvr_6^0-__disjvr_6^post48 == 0 /\ -__disjvr_0^post48+__disjvr_0^0 == 0 /\ -2+x^post48 == 0 /\ r^0-r^post48 == 0 /\ -__disjvr_2^post48+__disjvr_2^0 == 0 /\ -__disjvr_7^post48+__disjvr_7^0 == 0 /\ __disjvr_5^0-__disjvr_5^post48 == 0 /\ __disjvr_1^0-__disjvr_1^post48 == 0 /\ r0^0-r0^post48 == 0 /\ __disjvr_3^0-__disjvr_3^post48 == 0 /\ -__disjvr_8^post48+__disjvr_8^0 == 0 /\ -x1^post48+x1^0 == 0), cost: 1
New rule:
l29 -> l6 : x^0'=2, TRUE, cost: 1

Applied preprocessing
Original rule:
l30 -> l27 : __disjvr_4^0'=__disjvr_4^post50, x^0'=x^post50, __disjvr_1^0'=__disjvr_1^post50, r0^0'=r0^post50, __disjvr_6^0'=__disjvr_6^post50, __disjvr_3^0'=__disjvr_3^post50, x1^0'=x1^post50, __disjvr_0^0'=__disjvr_0^post50, __disjvr_8^0'=__disjvr_8^post50, __disjvr_5^0'=__disjvr_5^post50, __disjvr_2^0'=__disjvr_2^post50, r^0'=r^post50, __disjvr_7^0'=__disjvr_7^post50, (__disjvr_6^0-__disjvr_6^post50 == 0 /\ -__disjvr_7^post50+__disjvr_7^0 == 0 /\ __disjvr_4^0-__disjvr_4^post50 == 0 /\ -r^post50+r^0 == 0 /\ -__disjvr_0^post50+__disjvr_0^0 == 0 /\ __disjvr_5^0-__disjvr_5^post50 == 0 /\ -__disjvr_2^post50+__disjvr_2^0 == 0 /\ x^0-x^post50 == 0 /\ __disjvr_1^0-__disjvr_1^post50 == 0 /\ -__disjvr_8^post50+__disjvr_8^0 == 0 /\ -x^0+x1^post50 == 0 /\ r0^0-r0^post50 == 0 /\ __disjvr_3^0-__disjvr_3^post50 == 0), cost: 1
New rule:
l30 -> l27 : x1^0'=x^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l30 -> l29 : __disjvr_4^0'=__disjvr_4^post51, x^0'=x^post51, __disjvr_1^0'=__disjvr_1^post51, r0^0'=r0^post51, __disjvr_6^0'=__disjvr_6^post51, __disjvr_3^0'=__disjvr_3^post51, x1^0'=x1^post51, __disjvr_0^0'=__disjvr_0^post51, __disjvr_8^0'=__disjvr_8^post51, __disjvr_5^0'=__disjvr_5^post51, __disjvr_2^0'=__disjvr_2^post51, r^0'=r^post51, __disjvr_7^0'=__disjvr_7^post51, (-__disjvr_1^post51+__disjvr_1^0 == 0 /\ -__disjvr_3^post51+__disjvr_3^0 == 0 /\ r^0-r^post51 == 0 /\ -__disjvr_2^post51+__disjvr_2^0 == 0 /\ -x1^post51+x1^0 == 0 /\ -1+x^post51 == 0 /\ __disjvr_4^0-__disjvr_4^post51 == 0 /\ __disjvr_6^0-__disjvr_6^post51 == 0 /\ __disjvr_8^0-__disjvr_8^post51 == 0 /\ r0^0-r0^post51 == 0 /\ -__disjvr_7^post51+__disjvr_7^0 == 0 /\ __disjvr_5^0-__disjvr_5^post51 == 0 /\ -__disjvr_0^post51+__disjvr_0^0 == 0), cost: 1
New rule:
l30 -> l29 : x^0'=1, TRUE, cost: 1

Applied preprocessing
Original rule:
l31 -> l30 : __disjvr_4^0'=__disjvr_4^post53, x^0'=x^post53, __disjvr_1^0'=__disjvr_1^post53, r0^0'=r0^post53, __disjvr_6^0'=__disjvr_6^post53, __disjvr_3^0'=__disjvr_3^post53, x1^0'=x1^post53, __disjvr_0^0'=__disjvr_0^post53, __disjvr_8^0'=__disjvr_8^post53, __disjvr_5^0'=__disjvr_5^post53, __disjvr_2^0'=__disjvr_2^post53, r^0'=r^post53, __disjvr_7^0'=__disjvr_7^post53, (r^0-r^post53 == 0 /\ -x1^post53+x1^0 == 0 /\ -__disjvr_7^post53+__disjvr_7^0 == 0 /\ __disjvr_6^0-__disjvr_6^post53 == 0 /\ __disjvr_4^0-__disjvr_4^post53 == 0 /\ -__disjvr_0^post53+__disjvr_0^0 == 0 /\ -__disjvr_5^post53+__disjvr_5^0 == 0 /\ __disjvr_8^0-__disjvr_8^post53 == 0 /\ x^0-x^post53 == 0 /\ -__disjvr_1^post53+__disjvr_1^0 == 0 /\ r0^0-r0^post53 == 0 /\ __disjvr_3^0-__disjvr_3^post53 == 0 /\ -__disjvr_2^post53+__disjvr_2^0 == 0), cost: 1
New rule:
l31 -> l30 : TRUE, cost: 1

Simplified rules
Start location: l31
  54: l6 -> l7 : x1^0'=x^0, TRUE, cost: 1
  55: l6 -> l8 : TRUE, cost: 1
  57: l7 -> l10 : TRUE, cost: 1
  56: l8 -> l6 : TRUE, cost: 1
  58: l10 -> l7 : TRUE, cost: 1
  59: l11 -> l13 : TRUE, cost: 1
  60: l13 -> l11 : TRUE, cost: 1
  61: l14 -> l16 : TRUE, cost: 1
  62: l16 -> l14 : TRUE, cost: 1
  63: l19 -> l11 : x^0'=2, TRUE, cost: 1
  64: l21 -> l14 : x^0'=2, TRUE, cost: 1
  65: l27 -> l21 : x^0'=1, TRUE, cost: 1
  66: l29 -> l19 : x1^0'=x^0, TRUE, cost: 1
  67: l29 -> l6 : x^0'=2, TRUE, cost: 1
  68: l30 -> l27 : x1^0'=x^0, TRUE, cost: 1
  69: l30 -> l29 : x^0'=1, TRUE, cost: 1
  70: l31 -> l30 : TRUE, cost: 1


Eliminating location l27 by chaining:

Applied chaining
First rule:
l30 -> l27 : x1^0'=x^0, TRUE, cost: 1
Second rule:
l27 -> l21 : x^0'=1, TRUE, cost: 1
New rule:
l30 -> l21 : x^0'=1, x1^0'=x^0, TRUE, cost: 2

Applied deletion
Removed the following rules: 65 68

Eliminating location l21 by chaining:

Applied chaining
First rule:
l30 -> l21 : x^0'=1, x1^0'=x^0, TRUE, cost: 2
Second rule:
l21 -> l14 : x^0'=2, TRUE, cost: 1
New rule:
l30 -> l14 : x^0'=2, x1^0'=x^0, TRUE, cost: 3

Applied deletion
Removed the following rules: 64 71

Eliminating location l16 by chaining:

Applied chaining
First rule:
l14 -> l16 : TRUE, cost: 1
Second rule:
l16 -> l14 : TRUE, cost: 1
New rule:
l14 -> l14 : TRUE, cost: 2

Applied deletion
Removed the following rules: 61 62

Eliminating location l19 by chaining:

Applied chaining
First rule:
l29 -> l19 : x1^0'=x^0, TRUE, cost: 1
Second rule:
l19 -> l11 : x^0'=2, TRUE, cost: 1
New rule:
l29 -> l11 : x^0'=2, x1^0'=x^0, TRUE, cost: 2

Applied deletion
Removed the following rules: 63 66

Eliminating location l8 by chaining:

Applied chaining
First rule:
l6 -> l8 : TRUE, cost: 1
Second rule:
l8 -> l6 : TRUE, cost: 1
New rule:
l6 -> l6 : TRUE, cost: 2

Applied deletion
Removed the following rules: 55 56

Eliminating location l10 by chaining:

Applied chaining
First rule:
l7 -> l10 : TRUE, cost: 1
Second rule:
l10 -> l7 : TRUE, cost: 1
New rule:
l7 -> l7 : TRUE, cost: 2

Applied deletion
Removed the following rules: 57 58

Eliminating location l13 by chaining:

Applied chaining
First rule:
l11 -> l13 : TRUE, cost: 1
Second rule:
l13 -> l11 : TRUE, cost: 1
New rule:
l11 -> l11 : TRUE, cost: 2

Applied deletion
Removed the following rules: 59 60

Eliminated locations on linear paths
Start location: l31
  54: l6 -> l7 : x1^0'=x^0, TRUE, cost: 1
  75: l6 -> l6 : TRUE, cost: 2
  76: l7 -> l7 : TRUE, cost: 2
  77: l11 -> l11 : TRUE, cost: 2
  73: l14 -> l14 : TRUE, cost: 2
  67: l29 -> l6 : x^0'=2, TRUE, cost: 1
  74: l29 -> l11 : x^0'=2, x1^0'=x^0, TRUE, cost: 2
  69: l30 -> l29 : x^0'=1, TRUE, cost: 1
  72: l30 -> l14 : x^0'=2, x1^0'=x^0, TRUE, cost: 3
  70: l31 -> l30 : TRUE, cost: 1


Applied nonterm
Original rule:
l6 -> l6 : TRUE, cost: 2
New rule:
l6 -> [32] : n >= 0, cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_BEdAiP.txt

Applied deletion
Removed the following rules: 75

Applied nonterm
Original rule:
l7 -> l7 : TRUE, cost: 2
New rule:
l7 -> [33] : n0 >= 0, cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_NjpHAh.txt

Applied deletion
Removed the following rules: 76

Applied nonterm
Original rule:
l11 -> l11 : TRUE, cost: 2
New rule:
l11 -> [34] : n1 >= 0, cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_CLdKkM.txt

Applied deletion
Removed the following rules: 77

Applied nonterm
Original rule:
l14 -> l14 : TRUE, cost: 2
New rule:
l14 -> [35] : n2 >= 0, cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_pjIglf.txt

Applied deletion
Removed the following rules: 73

Accelerated simple loops
Start location: l31
  54: l6 -> l7 : x1^0'=x^0, TRUE, cost: 1
  78: l6 -> [32] : n >= 0, cost: NONTERM
  79: l7 -> [33] : n0 >= 0, cost: NONTERM
  80: l11 -> [34] : n1 >= 0, cost: NONTERM
  81: l14 -> [35] : n2 >= 0, cost: NONTERM
  67: l29 -> l6 : x^0'=2, TRUE, cost: 1
  74: l29 -> l11 : x^0'=2, x1^0'=x^0, TRUE, cost: 2
  69: l30 -> l29 : x^0'=1, TRUE, cost: 1
  72: l30 -> l14 : x^0'=2, x1^0'=x^0, TRUE, cost: 3
  70: l31 -> l30 : TRUE, cost: 1


Applied chaining
First rule:
l29 -> l6 : x^0'=2, TRUE, cost: 1
Second rule:
l6 -> [32] : n >= 0, cost: NONTERM
New rule:
l29 -> [32] : TRUE, cost: NONTERM

Applied deletion
Removed the following rules: 78

Applied chaining
First rule:
l6 -> l7 : x1^0'=x^0, TRUE, cost: 1
Second rule:
l7 -> [33] : n0 >= 0, cost: NONTERM
New rule:
l6 -> [33] : TRUE, cost: NONTERM

Applied deletion
Removed the following rules: 79

Applied chaining
First rule:
l29 -> l11 : x^0'=2, x1^0'=x^0, TRUE, cost: 2
Second rule:
l11 -> [34] : n1 >= 0, cost: NONTERM
New rule:
l29 -> [34] : TRUE, cost: NONTERM

Applied deletion
Removed the following rules: 80

Applied chaining
First rule:
l30 -> l14 : x^0'=2, x1^0'=x^0, TRUE, cost: 3
Second rule:
l14 -> [35] : n2 >= 0, cost: NONTERM
New rule:
l30 -> [35] : TRUE, cost: NONTERM

Applied deletion
Removed the following rules: 81

Chained accelerated rules with incoming rules
Start location: l31
  54: l6 -> l7 : x1^0'=x^0, TRUE, cost: 1
  83: l6 -> [33] : TRUE, cost: NONTERM
  67: l29 -> l6 : x^0'=2, TRUE, cost: 1
  74: l29 -> l11 : x^0'=2, x1^0'=x^0, TRUE, cost: 2
  82: l29 -> [32] : TRUE, cost: NONTERM
  84: l29 -> [34] : TRUE, cost: NONTERM
  69: l30 -> l29 : x^0'=1, TRUE, cost: 1
  72: l30 -> l14 : x^0'=2, x1^0'=x^0, TRUE, cost: 3
  85: l30 -> [35] : TRUE, cost: NONTERM
  70: l31 -> l30 : TRUE, cost: 1


Removed unreachable locations and irrelevant leafs
Start location: l31
  83: l6 -> [33] : TRUE, cost: NONTERM
  67: l29 -> l6 : x^0'=2, TRUE, cost: 1
  82: l29 -> [32] : TRUE, cost: NONTERM
  84: l29 -> [34] : TRUE, cost: NONTERM
  69: l30 -> l29 : x^0'=1, TRUE, cost: 1
  85: l30 -> [35] : TRUE, cost: NONTERM
  70: l31 -> l30 : TRUE, cost: 1


Eliminating location l6 by chaining:

Applied chaining
First rule:
l29 -> l6 : x^0'=2, TRUE, cost: 1
Second rule:
l6 -> [33] : TRUE, cost: NONTERM
New rule:
l29 -> [33] : TRUE, cost: NONTERM

Applied deletion
Removed the following rules: 67 83

Eliminated locations on linear paths
Start location: l31
  82: l29 -> [32] : TRUE, cost: NONTERM
  84: l29 -> [34] : TRUE, cost: NONTERM
  86: l29 -> [33] : TRUE, cost: NONTERM
  69: l30 -> l29 : x^0'=1, TRUE, cost: 1
  85: l30 -> [35] : TRUE, cost: NONTERM
  70: l31 -> l30 : TRUE, cost: 1


Eliminating location l30 by chaining:

Applied chaining
First rule:
l31 -> l30 : TRUE, cost: 1
Second rule:
l30 -> l29 : x^0'=1, TRUE, cost: 1
New rule:
l31 -> l29 : x^0'=1, TRUE, cost: 2

Applied chaining
First rule:
l31 -> l30 : TRUE, cost: 1
Second rule:
l30 -> [35] : TRUE, cost: NONTERM
New rule:
l31 -> [35] : TRUE, cost: NONTERM

Applied deletion
Removed the following rules: 69 70 85

Eliminated locations on tree-shaped paths
Start location: l31
  82: l29 -> [32] : TRUE, cost: NONTERM
  84: l29 -> [34] : TRUE, cost: NONTERM
  86: l29 -> [33] : TRUE, cost: NONTERM
  87: l31 -> l29 : x^0'=1, TRUE, cost: 2
  88: l31 -> [35] : TRUE, cost: NONTERM


Eliminating location l29 by chaining:

Applied chaining
First rule:
l31 -> l29 : x^0'=1, TRUE, cost: 2
Second rule:
l29 -> [32] : TRUE, cost: NONTERM
New rule:
l31 -> [32] : TRUE, cost: NONTERM

Applied chaining
First rule:
l31 -> l29 : x^0'=1, TRUE, cost: 2
Second rule:
l29 -> [34] : TRUE, cost: NONTERM
New rule:
l31 -> [34] : TRUE, cost: NONTERM

Applied chaining
First rule:
l31 -> l29 : x^0'=1, TRUE, cost: 2
Second rule:
l29 -> [33] : TRUE, cost: NONTERM
New rule:
l31 -> [33] : TRUE, cost: NONTERM

Applied deletion
Removed the following rules: 82 84 86 87

Eliminated locations on tree-shaped paths
Start location: l31
  88: l31 -> [35] : TRUE, cost: NONTERM
  89: l31 -> [32] : TRUE, cost: NONTERM
  90: l31 -> [34] : TRUE, cost: NONTERM
  91: l31 -> [33] : TRUE, cost: NONTERM


Removed duplicate rules (ignoring updates)
Start location: l31
  91: l31 -> [33] : TRUE, cost: NONTERM


Computing asymptotic complexity
Proved nontermination of rule 91 via SMT.

Proved the following lower bound
Complexity:  Nonterm
Cpx degree: Nonterm

Solved cost: NONTERM
Rule cost:   NONTERM
Rule guard:  TRUE