NO

Initial ITS

Start location: l12
Program variables: nondet_7^0 nondet_8^0 result_6^0 temp5_9^0 temp6_11^0 x_10^0
   0: l0 -> l1 : nondet_7^0'=nondet_7^post1, nondet_8^0'=nondet_8^post1, result_6^0'=result_6^post1, temp5_9^0'=temp5_9^post1, temp6_11^0'=temp6_11^post1, x_10^0'=x_10^post1, (0 == 0 /\ -nondet_8^post1+nondet_8^0 == 0 /\ -temp5_9^post1+temp5_9^0 == 0 /\ -temp6_11^post1+x_10^post1 == 0 /\ -result_6^post1+result_6^0 == 0 /\ temp6_11^post1-nondet_7^post1 == 0), cost: 1
  12: l1 -> l3 : nondet_7^0'=nondet_7^post13, nondet_8^0'=nondet_8^post13, result_6^0'=result_6^post13, temp5_9^0'=temp5_9^post13, temp6_11^0'=temp6_11^post13, x_10^0'=x_10^post13, (0 == 0 /\ -x_10^post13+x_10^0 == 0 /\ temp5_9^post13-nondet_8^post13 == 0 /\ -temp6_11^post13+temp6_11^0 == 0 /\ nondet_7^0-nondet_7^post13 == 0 /\ temp5_9^post13 <= 0 /\ -temp5_9^post13 <= 0), cost: 1
  13: l1 -> l10 : nondet_7^0'=nondet_7^post14, nondet_8^0'=nondet_8^post14, result_6^0'=result_6^post14, temp5_9^0'=temp5_9^post14, temp6_11^0'=temp6_11^post14, x_10^0'=x_10^post14, (0 == 0 /\ -temp6_11^post14+temp6_11^0 == 0 /\ temp5_9^post14-nondet_8^post14 == 0 /\ -nondet_7^post14+nondet_7^0 == 0 /\ result_6^0-result_6^post14 == 0 /\ x_10^0-x_10^post14 == 0), cost: 1
   1: l2 -> l3 : nondet_7^0'=nondet_7^post2, nondet_8^0'=nondet_8^post2, result_6^0'=result_6^post2, temp5_9^0'=temp5_9^post2, temp6_11^0'=temp6_11^post2, x_10^0'=x_10^post2, (0 == 0 /\ -temp5_9^post2 <= 0 /\ x_10^0-x_10^post2 == 0 /\ temp5_9^post2 <= 0 /\ temp6_11^0-temp6_11^post2 == 0 /\ temp5_9^post2-nondet_8^post2 == 0 /\ nondet_7^0-nondet_7^post2 == 0), cost: 1
   2: l2 -> l5 : nondet_7^0'=nondet_7^post3, nondet_8^0'=nondet_8^post3, result_6^0'=result_6^post3, temp5_9^0'=temp5_9^post3, temp6_11^0'=temp6_11^post3, x_10^0'=x_10^post3, (0 == 0 /\ -temp6_11^post3+temp6_11^0 == 0 /\ temp5_9^post3-nondet_8^post3 == 0 /\ -result_6^post3+result_6^0 == 0 /\ nondet_7^0-nondet_7^post3 == 0 /\ x_10^0-x_10^post3 == 0), cost: 1
   3: l5 -> l6 : nondet_7^0'=nondet_7^post4, nondet_8^0'=nondet_8^post4, result_6^0'=result_6^post4, temp5_9^0'=temp5_9^post4, temp6_11^0'=temp6_11^post4, x_10^0'=x_10^post4, (-temp5_9^post4+temp5_9^0 == 0 /\ -temp6_11^post4+temp6_11^0 == 0 /\ 1+temp5_9^0 <= 0 /\ nondet_8^0-nondet_8^post4 == 0 /\ x_10^0-x_10^post4 == 0 /\ result_6^0-result_6^post4 == 0 /\ -nondet_7^post4+nondet_7^0 == 0), cost: 1
   4: l5 -> l6 : nondet_7^0'=nondet_7^post5, nondet_8^0'=nondet_8^post5, result_6^0'=result_6^post5, temp5_9^0'=temp5_9^post5, temp6_11^0'=temp6_11^post5, x_10^0'=x_10^post5, (x_10^0-x_10^post5 == 0 /\ nondet_8^0-nondet_8^post5 == 0 /\ result_6^0-result_6^post5 == 0 /\ 1-temp5_9^0 <= 0 /\ -nondet_7^post5+nondet_7^0 == 0 /\ -temp5_9^post5+temp5_9^0 == 0 /\ -temp6_11^post5+temp6_11^0 == 0), cost: 1
   5: l6 -> l4 : nondet_7^0'=nondet_7^post6, nondet_8^0'=nondet_8^post6, result_6^0'=result_6^post6, temp5_9^0'=temp5_9^post6, temp6_11^0'=temp6_11^post6, x_10^0'=x_10^post6, (1-x_10^0 <= 0 /\ nondet_8^0-nondet_8^post6 == 0 /\ nondet_7^0-nondet_7^post6 == 0 /\ result_6^0-result_6^post6 == 0 /\ -1-x_10^0+x_10^post6 == 0 /\ -temp6_11^post6+temp6_11^0 == 0 /\ temp5_9^0-temp5_9^post6 == 0), cost: 1
   6: l4 -> l3 : nondet_7^0'=nondet_7^post7, nondet_8^0'=nondet_8^post7, result_6^0'=result_6^post7, temp5_9^0'=temp5_9^post7, temp6_11^0'=temp6_11^post7, x_10^0'=x_10^post7, (0 == 0 /\ -temp6_11^post7+temp6_11^0 == 0 /\ nondet_7^0-nondet_7^post7 == 0 /\ -nondet_8^post7+temp5_9^post7 == 0 /\ -temp5_9^post7 <= 0 /\ temp5_9^post7 <= 0 /\ x_10^0-x_10^post7 == 0), cost: 1
   7: l4 -> l8 : nondet_7^0'=nondet_7^post8, nondet_8^0'=nondet_8^post8, result_6^0'=result_6^post8, temp5_9^0'=temp5_9^post8, temp6_11^0'=temp6_11^post8, x_10^0'=x_10^post8, (0 == 0 /\ -nondet_8^post8+temp5_9^post8 == 0 /\ nondet_7^0-nondet_7^post8 == 0 /\ -result_6^post8+result_6^0 == 0 /\ x_10^0-x_10^post8 == 0 /\ -temp6_11^post8+temp6_11^0 == 0), cost: 1
   8: l8 -> l9 : nondet_7^0'=nondet_7^post9, nondet_8^0'=nondet_8^post9, result_6^0'=result_6^post9, temp5_9^0'=temp5_9^post9, temp6_11^0'=temp6_11^post9, x_10^0'=x_10^post9, (x_10^0-x_10^post9 == 0 /\ nondet_8^0-nondet_8^post9 == 0 /\ -result_6^post9+result_6^0 == 0 /\ nondet_7^0-nondet_7^post9 == 0 /\ 1+temp5_9^0 <= 0 /\ -temp6_11^post9+temp6_11^0 == 0 /\ temp5_9^0-temp5_9^post9 == 0), cost: 1
   9: l8 -> l9 : nondet_7^0'=nondet_7^post10, nondet_8^0'=nondet_8^post10, result_6^0'=result_6^post10, temp5_9^0'=temp5_9^post10, temp6_11^0'=temp6_11^post10, x_10^0'=x_10^post10, (nondet_7^0-nondet_7^post10 == 0 /\ -temp5_9^post10+temp5_9^0 == 0 /\ x_10^0-x_10^post10 == 0 /\ -temp6_11^post10+temp6_11^0 == 0 /\ 1-temp5_9^0 <= 0 /\ -nondet_8^post10+nondet_8^0 == 0 /\ -result_6^post10+result_6^0 == 0), cost: 1
  10: l9 -> l7 : nondet_7^0'=nondet_7^post11, nondet_8^0'=nondet_8^post11, result_6^0'=result_6^post11, temp5_9^0'=temp5_9^post11, temp6_11^0'=temp6_11^post11, x_10^0'=x_10^post11, (-1-x_10^0+x_10^post11 == 0 /\ 1-x_10^0 <= 0 /\ -result_6^post11+result_6^0 == 0 /\ nondet_8^0-nondet_8^post11 == 0 /\ -temp6_11^post11+temp6_11^0 == 0 /\ -temp5_9^post11+temp5_9^0 == 0 /\ nondet_7^0-nondet_7^post11 == 0), cost: 1
  11: l7 -> l4 : nondet_7^0'=nondet_7^post12, nondet_8^0'=nondet_8^post12, result_6^0'=result_6^post12, temp5_9^0'=temp5_9^post12, temp6_11^0'=temp6_11^post12, x_10^0'=x_10^post12, (-result_6^post12+result_6^0 == 0 /\ nondet_8^0-nondet_8^post12 == 0 /\ x_10^0-x_10^post12 == 0 /\ temp6_11^0-temp6_11^post12 == 0 /\ -temp5_9^post12+temp5_9^0 == 0 /\ nondet_7^0-nondet_7^post12 == 0), cost: 1
  14: l10 -> l11 : nondet_7^0'=nondet_7^post15, nondet_8^0'=nondet_8^post15, result_6^0'=result_6^post15, temp5_9^0'=temp5_9^post15, temp6_11^0'=temp6_11^post15, x_10^0'=x_10^post15, (1+temp5_9^0 <= 0 /\ x_10^0-x_10^post15 == 0 /\ result_6^0-result_6^post15 == 0 /\ nondet_8^0-nondet_8^post15 == 0 /\ -temp5_9^post15+temp5_9^0 == 0 /\ -nondet_7^post15+nondet_7^0 == 0 /\ -temp6_11^post15+temp6_11^0 == 0), cost: 1
  15: l10 -> l11 : nondet_7^0'=nondet_7^post16, nondet_8^0'=nondet_8^post16, result_6^0'=result_6^post16, temp5_9^0'=temp5_9^post16, temp6_11^0'=temp6_11^post16, x_10^0'=x_10^post16, (-temp6_11^post16+temp6_11^0 == 0 /\ nondet_8^0-nondet_8^post16 == 0 /\ nondet_7^0-nondet_7^post16 == 0 /\ -result_6^post16+result_6^0 == 0 /\ temp5_9^0-temp5_9^post16 == 0 /\ 1-temp5_9^0 <= 0 /\ x_10^0-x_10^post16 == 0), cost: 1
  16: l11 -> l4 : nondet_7^0'=nondet_7^post17, nondet_8^0'=nondet_8^post17, result_6^0'=result_6^post17, temp5_9^0'=temp5_9^post17, temp6_11^0'=temp6_11^post17, x_10^0'=x_10^post17, (-result_6^post17+result_6^0 == 0 /\ 1-x_10^0 <= 0 /\ -temp6_11^post17+temp6_11^0 == 0 /\ -1-x_10^0+x_10^post17 == 0 /\ nondet_7^0-nondet_7^post17 == 0 /\ temp5_9^0-temp5_9^post17 == 0 /\ nondet_8^0-nondet_8^post17 == 0), cost: 1
  17: l12 -> l0 : nondet_7^0'=nondet_7^post18, nondet_8^0'=nondet_8^post18, result_6^0'=result_6^post18, temp5_9^0'=temp5_9^post18, temp6_11^0'=temp6_11^post18, x_10^0'=x_10^post18, (-nondet_8^post18+nondet_8^0 == 0 /\ nondet_7^0-nondet_7^post18 == 0 /\ -temp5_9^post18+temp5_9^0 == 0 /\ -result_6^post18+result_6^0 == 0 /\ -temp6_11^post18+temp6_11^0 == 0 /\ x_10^0-x_10^post18 == 0), cost: 1

Chained Linear Paths

Start location: l12
Program variables: nondet_7^0 nondet_8^0 result_6^0 temp5_9^0 temp6_11^0 x_10^0
  12: l1 -> l3 : nondet_7^0'=nondet_7^post13, nondet_8^0'=nondet_8^post13, result_6^0'=result_6^post13, temp5_9^0'=temp5_9^post13, temp6_11^0'=temp6_11^post13, x_10^0'=x_10^post13, (0 == 0 /\ -x_10^post13+x_10^0 == 0 /\ temp5_9^post13-nondet_8^post13 == 0 /\ -temp6_11^post13+temp6_11^0 == 0 /\ nondet_7^0-nondet_7^post13 == 0 /\ temp5_9^post13 <= 0 /\ -temp5_9^post13 <= 0), cost: 1
  13: l1 -> l10 : nondet_7^0'=nondet_7^post14, nondet_8^0'=nondet_8^post14, result_6^0'=result_6^post14, temp5_9^0'=temp5_9^post14, temp6_11^0'=temp6_11^post14, x_10^0'=x_10^post14, (0 == 0 /\ -temp6_11^post14+temp6_11^0 == 0 /\ temp5_9^post14-nondet_8^post14 == 0 /\ -nondet_7^post14+nondet_7^0 == 0 /\ result_6^0-result_6^post14 == 0 /\ x_10^0-x_10^post14 == 0), cost: 1
   1: l2 -> l3 : nondet_7^0'=nondet_7^post2, nondet_8^0'=nondet_8^post2, result_6^0'=result_6^post2, temp5_9^0'=temp5_9^post2, temp6_11^0'=temp6_11^post2, x_10^0'=x_10^post2, (0 == 0 /\ -temp5_9^post2 <= 0 /\ x_10^0-x_10^post2 == 0 /\ temp5_9^post2 <= 0 /\ temp6_11^0-temp6_11^post2 == 0 /\ temp5_9^post2-nondet_8^post2 == 0 /\ nondet_7^0-nondet_7^post2 == 0), cost: 1
   2: l2 -> l5 : nondet_7^0'=nondet_7^post3, nondet_8^0'=nondet_8^post3, result_6^0'=result_6^post3, temp5_9^0'=temp5_9^post3, temp6_11^0'=temp6_11^post3, x_10^0'=x_10^post3, (0 == 0 /\ -temp6_11^post3+temp6_11^0 == 0 /\ temp5_9^post3-nondet_8^post3 == 0 /\ -result_6^post3+result_6^0 == 0 /\ nondet_7^0-nondet_7^post3 == 0 /\ x_10^0-x_10^post3 == 0), cost: 1
   3: l5 -> l6 : nondet_7^0'=nondet_7^post4, nondet_8^0'=nondet_8^post4, result_6^0'=result_6^post4, temp5_9^0'=temp5_9^post4, temp6_11^0'=temp6_11^post4, x_10^0'=x_10^post4, (-temp5_9^post4+temp5_9^0 == 0 /\ -temp6_11^post4+temp6_11^0 == 0 /\ 1+temp5_9^0 <= 0 /\ nondet_8^0-nondet_8^post4 == 0 /\ x_10^0-x_10^post4 == 0 /\ result_6^0-result_6^post4 == 0 /\ -nondet_7^post4+nondet_7^0 == 0), cost: 1
   4: l5 -> l6 : nondet_7^0'=nondet_7^post5, nondet_8^0'=nondet_8^post5, result_6^0'=result_6^post5, temp5_9^0'=temp5_9^post5, temp6_11^0'=temp6_11^post5, x_10^0'=x_10^post5, (x_10^0-x_10^post5 == 0 /\ nondet_8^0-nondet_8^post5 == 0 /\ result_6^0-result_6^post5 == 0 /\ 1-temp5_9^0 <= 0 /\ -nondet_7^post5+nondet_7^0 == 0 /\ -temp5_9^post5+temp5_9^0 == 0 /\ -temp6_11^post5+temp6_11^0 == 0), cost: 1
   5: l6 -> l4 : nondet_7^0'=nondet_7^post6, nondet_8^0'=nondet_8^post6, result_6^0'=result_6^post6, temp5_9^0'=temp5_9^post6, temp6_11^0'=temp6_11^post6, x_10^0'=x_10^post6, (1-x_10^0 <= 0 /\ nondet_8^0-nondet_8^post6 == 0 /\ nondet_7^0-nondet_7^post6 == 0 /\ result_6^0-result_6^post6 == 0 /\ -1-x_10^0+x_10^post6 == 0 /\ -temp6_11^post6+temp6_11^0 == 0 /\ temp5_9^0-temp5_9^post6 == 0), cost: 1
   6: l4 -> l3 : nondet_7^0'=nondet_7^post7, nondet_8^0'=nondet_8^post7, result_6^0'=result_6^post7, temp5_9^0'=temp5_9^post7, temp6_11^0'=temp6_11^post7, x_10^0'=x_10^post7, (0 == 0 /\ -temp6_11^post7+temp6_11^0 == 0 /\ nondet_7^0-nondet_7^post7 == 0 /\ -nondet_8^post7+temp5_9^post7 == 0 /\ -temp5_9^post7 <= 0 /\ temp5_9^post7 <= 0 /\ x_10^0-x_10^post7 == 0), cost: 1
   7: l4 -> l8 : nondet_7^0'=nondet_7^post8, nondet_8^0'=nondet_8^post8, result_6^0'=result_6^post8, temp5_9^0'=temp5_9^post8, temp6_11^0'=temp6_11^post8, x_10^0'=x_10^post8, (0 == 0 /\ -nondet_8^post8+temp5_9^post8 == 0 /\ nondet_7^0-nondet_7^post8 == 0 /\ -result_6^post8+result_6^0 == 0 /\ x_10^0-x_10^post8 == 0 /\ -temp6_11^post8+temp6_11^0 == 0), cost: 1
   8: l8 -> l9 : nondet_7^0'=nondet_7^post9, nondet_8^0'=nondet_8^post9, result_6^0'=result_6^post9, temp5_9^0'=temp5_9^post9, temp6_11^0'=temp6_11^post9, x_10^0'=x_10^post9, (x_10^0-x_10^post9 == 0 /\ nondet_8^0-nondet_8^post9 == 0 /\ -result_6^post9+result_6^0 == 0 /\ nondet_7^0-nondet_7^post9 == 0 /\ 1+temp5_9^0 <= 0 /\ -temp6_11^post9+temp6_11^0 == 0 /\ temp5_9^0-temp5_9^post9 == 0), cost: 1
   9: l8 -> l9 : nondet_7^0'=nondet_7^post10, nondet_8^0'=nondet_8^post10, result_6^0'=result_6^post10, temp5_9^0'=temp5_9^post10, temp6_11^0'=temp6_11^post10, x_10^0'=x_10^post10, (nondet_7^0-nondet_7^post10 == 0 /\ -temp5_9^post10+temp5_9^0 == 0 /\ x_10^0-x_10^post10 == 0 /\ -temp6_11^post10+temp6_11^0 == 0 /\ 1-temp5_9^0 <= 0 /\ -nondet_8^post10+nondet_8^0 == 0 /\ -result_6^post10+result_6^0 == 0), cost: 1
  19: l9 -> l4 : nondet_7^0'=nondet_7^post12, nondet_8^0'=nondet_8^post12, result_6^0'=result_6^post12, temp5_9^0'=temp5_9^post12, temp6_11^0'=temp6_11^post12, x_10^0'=x_10^post12, (-1-x_10^0+x_10^post11 == 0 /\ -nondet_8^post12+nondet_8^post11 == 0 /\ 1-x_10^0 <= 0 /\ -x_10^post12+x_10^post11 == 0 /\ -result_6^post11+result_6^0 == 0 /\ nondet_8^0-nondet_8^post11 == 0 /\ -temp5_9^post12+temp5_9^post11 == 0 /\ temp6_11^post11-temp6_11^post12 == 0 /\ -temp6_11^post11+temp6_11^0 == 0 /\ -result_6^post12+result_6^post11 == 0 /\ -temp5_9^post11+temp5_9^0 == 0 /\ -nondet_7^post12+nondet_7^post11 == 0 /\ nondet_7^0-nondet_7^post11 == 0), cost: 1
  14: l10 -> l11 : nondet_7^0'=nondet_7^post15, nondet_8^0'=nondet_8^post15, result_6^0'=result_6^post15, temp5_9^0'=temp5_9^post15, temp6_11^0'=temp6_11^post15, x_10^0'=x_10^post15, (1+temp5_9^0 <= 0 /\ x_10^0-x_10^post15 == 0 /\ result_6^0-result_6^post15 == 0 /\ nondet_8^0-nondet_8^post15 == 0 /\ -temp5_9^post15+temp5_9^0 == 0 /\ -nondet_7^post15+nondet_7^0 == 0 /\ -temp6_11^post15+temp6_11^0 == 0), cost: 1
  15: l10 -> l11 : nondet_7^0'=nondet_7^post16, nondet_8^0'=nondet_8^post16, result_6^0'=result_6^post16, temp5_9^0'=temp5_9^post16, temp6_11^0'=temp6_11^post16, x_10^0'=x_10^post16, (-temp6_11^post16+temp6_11^0 == 0 /\ nondet_8^0-nondet_8^post16 == 0 /\ nondet_7^0-nondet_7^post16 == 0 /\ -result_6^post16+result_6^0 == 0 /\ temp5_9^0-temp5_9^post16 == 0 /\ 1-temp5_9^0 <= 0 /\ x_10^0-x_10^post16 == 0), cost: 1
  16: l11 -> l4 : nondet_7^0'=nondet_7^post17, nondet_8^0'=nondet_8^post17, result_6^0'=result_6^post17, temp5_9^0'=temp5_9^post17, temp6_11^0'=temp6_11^post17, x_10^0'=x_10^post17, (-result_6^post17+result_6^0 == 0 /\ 1-x_10^0 <= 0 /\ -temp6_11^post17+temp6_11^0 == 0 /\ -1-x_10^0+x_10^post17 == 0 /\ nondet_7^0-nondet_7^post17 == 0 /\ temp5_9^0-temp5_9^post17 == 0 /\ nondet_8^0-nondet_8^post17 == 0), cost: 1
  18: l12 -> l1 : nondet_7^0'=nondet_7^post1, nondet_8^0'=nondet_8^post1, result_6^0'=result_6^post1, temp5_9^0'=temp5_9^post1, temp6_11^0'=temp6_11^post1, x_10^0'=x_10^post1, (0 == 0 /\ -nondet_8^post18+nondet_8^0 == 0 /\ nondet_8^post18-nondet_8^post1 == 0 /\ nondet_7^0-nondet_7^post18 == 0 /\ result_6^post18-result_6^post1 == 0 /\ -temp5_9^post18+temp5_9^0 == 0 /\ -result_6^post18+result_6^0 == 0 /\ -temp6_11^post18+temp6_11^0 == 0 /\ x_10^0-x_10^post18 == 0 /\ -temp6_11^post1+x_10^post1 == 0 /\ temp5_9^post18-temp5_9^post1 == 0 /\ temp6_11^post1-nondet_7^post1 == 0), cost: 1

	Eliminating location l0 by chaining:

	Applied chaining

	First rule:
	l12 -> l0 : nondet_7^0'=nondet_7^post18, nondet_8^0'=nondet_8^post18, result_6^0'=result_6^post18, temp5_9^0'=temp5_9^post18, temp6_11^0'=temp6_11^post18, x_10^0'=x_10^post18, (-nondet_8^post18+nondet_8^0 == 0 /\ nondet_7^0-nondet_7^post18 == 0 /\ -temp5_9^post18+temp5_9^0 == 0 /\ -result_6^post18+result_6^0 == 0 /\ -temp6_11^post18+temp6_11^0 == 0 /\ x_10^0-x_10^post18 == 0), cost: 1
	Second rule:
	l0 -> l1 : nondet_7^0'=nondet_7^post1, nondet_8^0'=nondet_8^post1, result_6^0'=result_6^post1, temp5_9^0'=temp5_9^post1, temp6_11^0'=temp6_11^post1, x_10^0'=x_10^post1, (0 == 0 /\ -nondet_8^post1+nondet_8^0 == 0 /\ -temp5_9^post1+temp5_9^0 == 0 /\ -temp6_11^post1+x_10^post1 == 0 /\ -result_6^post1+result_6^0 == 0 /\ temp6_11^post1-nondet_7^post1 == 0), cost: 1
	New rule:
	l12 -> l1 : nondet_7^0'=nondet_7^post1, nondet_8^0'=nondet_8^post1, result_6^0'=result_6^post1, temp5_9^0'=temp5_9^post1, temp6_11^0'=temp6_11^post1, x_10^0'=x_10^post1, (0 == 0 /\ -nondet_8^post18+nondet_8^0 == 0 /\ nondet_8^post18-nondet_8^post1 == 0 /\ nondet_7^0-nondet_7^post18 == 0 /\ result_6^post18-result_6^post1 == 0 /\ -temp5_9^post18+temp5_9^0 == 0 /\ -result_6^post18+result_6^0 == 0 /\ -temp6_11^post18+temp6_11^0 == 0 /\ x_10^0-x_10^post18 == 0 /\ -temp6_11^post1+x_10^post1 == 0 /\ temp5_9^post18-temp5_9^post1 == 0 /\ temp6_11^post1-nondet_7^post1 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 0 17
	
	Eliminating location l7 by chaining:

	Applied chaining

	First rule:
	l9 -> l7 : nondet_7^0'=nondet_7^post11, nondet_8^0'=nondet_8^post11, result_6^0'=result_6^post11, temp5_9^0'=temp5_9^post11, temp6_11^0'=temp6_11^post11, x_10^0'=x_10^post11, (-1-x_10^0+x_10^post11 == 0 /\ 1-x_10^0 <= 0 /\ -result_6^post11+result_6^0 == 0 /\ nondet_8^0-nondet_8^post11 == 0 /\ -temp6_11^post11+temp6_11^0 == 0 /\ -temp5_9^post11+temp5_9^0 == 0 /\ nondet_7^0-nondet_7^post11 == 0), cost: 1
	Second rule:
	l7 -> l4 : nondet_7^0'=nondet_7^post12, nondet_8^0'=nondet_8^post12, result_6^0'=result_6^post12, temp5_9^0'=temp5_9^post12, temp6_11^0'=temp6_11^post12, x_10^0'=x_10^post12, (-result_6^post12+result_6^0 == 0 /\ nondet_8^0-nondet_8^post12 == 0 /\ x_10^0-x_10^post12 == 0 /\ temp6_11^0-temp6_11^post12 == 0 /\ -temp5_9^post12+temp5_9^0 == 0 /\ nondet_7^0-nondet_7^post12 == 0), cost: 1
	New rule:
	l9 -> l4 : nondet_7^0'=nondet_7^post12, nondet_8^0'=nondet_8^post12, result_6^0'=result_6^post12, temp5_9^0'=temp5_9^post12, temp6_11^0'=temp6_11^post12, x_10^0'=x_10^post12, (-1-x_10^0+x_10^post11 == 0 /\ -nondet_8^post12+nondet_8^post11 == 0 /\ 1-x_10^0 <= 0 /\ -x_10^post12+x_10^post11 == 0 /\ -result_6^post11+result_6^0 == 0 /\ nondet_8^0-nondet_8^post11 == 0 /\ -temp5_9^post12+temp5_9^post11 == 0 /\ temp6_11^post11-temp6_11^post12 == 0 /\ -temp6_11^post11+temp6_11^0 == 0 /\ -result_6^post12+result_6^post11 == 0 /\ -temp5_9^post11+temp5_9^0 == 0 /\ -nondet_7^post12+nondet_7^post11 == 0 /\ nondet_7^0-nondet_7^post11 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 10 11

Simplified Transitions

Start location: l12
Program variables: nondet_7^0 nondet_8^0 result_6^0 temp5_9^0 temp6_11^0 x_10^0
  29: l1 -> l3 : nondet_8^0'=0, result_6^0'=result_6^post13, temp5_9^0'=0, T, cost: 1
  30: l1 -> l10 : nondet_8^0'=temp5_9^post14, temp5_9^0'=temp5_9^post14, T, cost: 1
  20: l2 -> l3 : nondet_8^0'=0, result_6^0'=result_6^post2, temp5_9^0'=0, T, cost: 1
  21: l2 -> l5 : nondet_8^0'=temp5_9^post3, temp5_9^0'=temp5_9^post3, T, cost: 1
  22: l5 -> l6 : 1+temp5_9^0 <= 0, cost: 1
  23: l5 -> l6 : 1-temp5_9^0 <= 0, cost: 1
  24: l6 -> l4 : x_10^0'=1+x_10^0, 1-x_10^0 <= 0, cost: 1
  25: l4 -> l3 : nondet_8^0'=0, result_6^0'=result_6^post7, temp5_9^0'=0, T, cost: 1
  26: l4 -> l8 : nondet_8^0'=temp5_9^post8, temp5_9^0'=temp5_9^post8, T, cost: 1
  27: l8 -> l9 : 1+temp5_9^0 <= 0, cost: 1
  28: l8 -> l9 : 1-temp5_9^0 <= 0, cost: 1
  35: l9 -> l4 : x_10^0'=1+x_10^0, 1-x_10^0 <= 0, cost: 1
  31: l10 -> l11 : 1+temp5_9^0 <= 0, cost: 1
  32: l10 -> l11 : 1-temp5_9^0 <= 0, cost: 1
  33: l11 -> l4 : x_10^0'=1+x_10^0, 1-x_10^0 <= 0, cost: 1
  34: l12 -> l1 : nondet_7^0'=x_10^post1, temp6_11^0'=x_10^post1, x_10^0'=x_10^post1, T, cost: 1

	made implied equalities explicit

	Original rule:
	l2 -> l3 : nondet_7^0'=nondet_7^post2, nondet_8^0'=nondet_8^post2, result_6^0'=result_6^post2, temp5_9^0'=temp5_9^post2, temp6_11^0'=temp6_11^post2, x_10^0'=x_10^post2, (0 == 0 /\ -temp5_9^post2 <= 0 /\ x_10^0-x_10^post2 == 0 /\ temp5_9^post2 <= 0 /\ temp6_11^0-temp6_11^post2 == 0 /\ temp5_9^post2-nondet_8^post2 == 0 /\ nondet_7^0-nondet_7^post2 == 0), cost: 1
	New rule:
	l2 -> l3 : nondet_7^0'=nondet_7^post2, nondet_8^0'=nondet_8^post2, result_6^0'=result_6^post2, temp5_9^0'=temp5_9^post2, temp6_11^0'=temp6_11^post2, x_10^0'=x_10^post2, (0 == 0 /\ -temp5_9^post2 <= 0 /\ -temp5_9^post2 == 0 /\ x_10^0-x_10^post2 == 0 /\ temp5_9^post2 <= 0 /\ temp6_11^0-temp6_11^post2 == 0 /\ temp5_9^post2-nondet_8^post2 == 0 /\ nondet_7^0-nondet_7^post2 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l3 : nondet_7^0'=nondet_7^post2, nondet_8^0'=nondet_8^post2, result_6^0'=result_6^post2, temp5_9^0'=temp5_9^post2, temp6_11^0'=temp6_11^post2, x_10^0'=x_10^post2, (0 == 0 /\ -temp5_9^post2 <= 0 /\ -temp5_9^post2 == 0 /\ x_10^0-x_10^post2 == 0 /\ temp5_9^post2 <= 0 /\ temp6_11^0-temp6_11^post2 == 0 /\ temp5_9^post2-nondet_8^post2 == 0 /\ nondet_7^0-nondet_7^post2 == 0), cost: 1
	New rule:
	l2 -> l3 : nondet_7^0'=nondet_7^0, nondet_8^0'=0, result_6^0'=result_6^post2, temp5_9^0'=0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 <= 0 /\ 0 == 0), cost: 1
	
		propagated equality temp5_9^post2 = 0
		
		propagated equality x_10^post2 = x_10^0
		
		propagated equality temp6_11^post2 = temp6_11^0
		
		propagated equality nondet_8^post2 = 0
		
		propagated equality nondet_7^post2 = nondet_7^0
		
	Simplified Guard

	Original rule:
	l2 -> l3 : nondet_7^0'=nondet_7^0, nondet_8^0'=0, result_6^0'=result_6^post2, temp5_9^0'=0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 <= 0 /\ 0 == 0), cost: 1
	New rule:
	l2 -> l3 : nondet_7^0'=nondet_7^0, nondet_8^0'=0, result_6^0'=result_6^post2, temp5_9^0'=0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l3 : nondet_7^0'=nondet_7^0, nondet_8^0'=0, result_6^0'=result_6^post2, temp5_9^0'=0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, T, cost: 1
	New rule:
	l2 -> l3 : nondet_8^0'=0, result_6^0'=result_6^post2, temp5_9^0'=0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l5 : nondet_7^0'=nondet_7^post3, nondet_8^0'=nondet_8^post3, result_6^0'=result_6^post3, temp5_9^0'=temp5_9^post3, temp6_11^0'=temp6_11^post3, x_10^0'=x_10^post3, (0 == 0 /\ -temp6_11^post3+temp6_11^0 == 0 /\ temp5_9^post3-nondet_8^post3 == 0 /\ -result_6^post3+result_6^0 == 0 /\ nondet_7^0-nondet_7^post3 == 0 /\ x_10^0-x_10^post3 == 0), cost: 1
	New rule:
	l2 -> l5 : nondet_7^0'=nondet_7^0, nondet_8^0'=temp5_9^post3, result_6^0'=result_6^0, temp5_9^0'=temp5_9^post3, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 0 == 0, cost: 1
	
		propagated equality temp6_11^post3 = temp6_11^0
		
		propagated equality nondet_8^post3 = temp5_9^post3
		
		propagated equality result_6^post3 = result_6^0
		
		propagated equality nondet_7^post3 = nondet_7^0
		
		propagated equality x_10^post3 = x_10^0
		
	Simplified Guard

	Original rule:
	l2 -> l5 : nondet_7^0'=nondet_7^0, nondet_8^0'=temp5_9^post3, result_6^0'=result_6^0, temp5_9^0'=temp5_9^post3, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 0 == 0, cost: 1
	New rule:
	l2 -> l5 : nondet_7^0'=nondet_7^0, nondet_8^0'=temp5_9^post3, result_6^0'=result_6^0, temp5_9^0'=temp5_9^post3, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l5 : nondet_7^0'=nondet_7^0, nondet_8^0'=temp5_9^post3, result_6^0'=result_6^0, temp5_9^0'=temp5_9^post3, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, T, cost: 1
	New rule:
	l2 -> l5 : nondet_8^0'=temp5_9^post3, temp5_9^0'=temp5_9^post3, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l5 -> l6 : nondet_7^0'=nondet_7^post4, nondet_8^0'=nondet_8^post4, result_6^0'=result_6^post4, temp5_9^0'=temp5_9^post4, temp6_11^0'=temp6_11^post4, x_10^0'=x_10^post4, (-temp5_9^post4+temp5_9^0 == 0 /\ -temp6_11^post4+temp6_11^0 == 0 /\ 1+temp5_9^0 <= 0 /\ nondet_8^0-nondet_8^post4 == 0 /\ x_10^0-x_10^post4 == 0 /\ result_6^0-result_6^post4 == 0 /\ -nondet_7^post4+nondet_7^0 == 0), cost: 1
	New rule:
	l5 -> l6 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 == 0 /\ 1+temp5_9^0 <= 0), cost: 1
	
		propagated equality temp5_9^post4 = temp5_9^0
		
		propagated equality temp6_11^post4 = temp6_11^0
		
		propagated equality nondet_8^post4 = nondet_8^0
		
		propagated equality x_10^post4 = x_10^0
		
		propagated equality result_6^post4 = result_6^0
		
		propagated equality nondet_7^post4 = nondet_7^0
		
	Simplified Guard

	Original rule:
	l5 -> l6 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 == 0 /\ 1+temp5_9^0 <= 0), cost: 1
	New rule:
	l5 -> l6 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 1+temp5_9^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l5 -> l6 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 1+temp5_9^0 <= 0, cost: 1
	New rule:
	l5 -> l6 : 1+temp5_9^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l5 -> l6 : nondet_7^0'=nondet_7^post5, nondet_8^0'=nondet_8^post5, result_6^0'=result_6^post5, temp5_9^0'=temp5_9^post5, temp6_11^0'=temp6_11^post5, x_10^0'=x_10^post5, (x_10^0-x_10^post5 == 0 /\ nondet_8^0-nondet_8^post5 == 0 /\ result_6^0-result_6^post5 == 0 /\ 1-temp5_9^0 <= 0 /\ -nondet_7^post5+nondet_7^0 == 0 /\ -temp5_9^post5+temp5_9^0 == 0 /\ -temp6_11^post5+temp6_11^0 == 0), cost: 1
	New rule:
	l5 -> l6 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 == 0 /\ 1-temp5_9^0 <= 0), cost: 1
	
		propagated equality x_10^post5 = x_10^0
		
		propagated equality nondet_8^post5 = nondet_8^0
		
		propagated equality result_6^post5 = result_6^0
		
		propagated equality nondet_7^post5 = nondet_7^0
		
		propagated equality temp5_9^post5 = temp5_9^0
		
		propagated equality temp6_11^post5 = temp6_11^0
		
	Simplified Guard

	Original rule:
	l5 -> l6 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 == 0 /\ 1-temp5_9^0 <= 0), cost: 1
	New rule:
	l5 -> l6 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 1-temp5_9^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l5 -> l6 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 1-temp5_9^0 <= 0, cost: 1
	New rule:
	l5 -> l6 : 1-temp5_9^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l6 -> l4 : nondet_7^0'=nondet_7^post6, nondet_8^0'=nondet_8^post6, result_6^0'=result_6^post6, temp5_9^0'=temp5_9^post6, temp6_11^0'=temp6_11^post6, x_10^0'=x_10^post6, (1-x_10^0 <= 0 /\ nondet_8^0-nondet_8^post6 == 0 /\ nondet_7^0-nondet_7^post6 == 0 /\ result_6^0-result_6^post6 == 0 /\ -1-x_10^0+x_10^post6 == 0 /\ -temp6_11^post6+temp6_11^0 == 0 /\ temp5_9^0-temp5_9^post6 == 0), cost: 1
	New rule:
	l6 -> l4 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=1+x_10^0, (0 == 0 /\ 1-x_10^0 <= 0), cost: 1
	
		propagated equality nondet_8^post6 = nondet_8^0
		
		propagated equality nondet_7^post6 = nondet_7^0
		
		propagated equality result_6^post6 = result_6^0
		
		propagated equality x_10^post6 = 1+x_10^0
		
		propagated equality temp6_11^post6 = temp6_11^0
		
		propagated equality temp5_9^post6 = temp5_9^0
		
	Simplified Guard

	Original rule:
	l6 -> l4 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=1+x_10^0, (0 == 0 /\ 1-x_10^0 <= 0), cost: 1
	New rule:
	l6 -> l4 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=1+x_10^0, 1-x_10^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l6 -> l4 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=1+x_10^0, 1-x_10^0 <= 0, cost: 1
	New rule:
	l6 -> l4 : x_10^0'=1+x_10^0, 1-x_10^0 <= 0, cost: 1
	
	made implied equalities explicit

	Original rule:
	l4 -> l3 : nondet_7^0'=nondet_7^post7, nondet_8^0'=nondet_8^post7, result_6^0'=result_6^post7, temp5_9^0'=temp5_9^post7, temp6_11^0'=temp6_11^post7, x_10^0'=x_10^post7, (0 == 0 /\ -temp6_11^post7+temp6_11^0 == 0 /\ nondet_7^0-nondet_7^post7 == 0 /\ -nondet_8^post7+temp5_9^post7 == 0 /\ -temp5_9^post7 <= 0 /\ temp5_9^post7 <= 0 /\ x_10^0-x_10^post7 == 0), cost: 1
	New rule:
	l4 -> l3 : nondet_7^0'=nondet_7^post7, nondet_8^0'=nondet_8^post7, result_6^0'=result_6^post7, temp5_9^0'=temp5_9^post7, temp6_11^0'=temp6_11^post7, x_10^0'=x_10^post7, (0 == 0 /\ -temp6_11^post7+temp6_11^0 == 0 /\ nondet_7^0-nondet_7^post7 == 0 /\ -nondet_8^post7+temp5_9^post7 == 0 /\ -temp5_9^post7 <= 0 /\ -temp5_9^post7 == 0 /\ temp5_9^post7 <= 0 /\ x_10^0-x_10^post7 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l3 : nondet_7^0'=nondet_7^post7, nondet_8^0'=nondet_8^post7, result_6^0'=result_6^post7, temp5_9^0'=temp5_9^post7, temp6_11^0'=temp6_11^post7, x_10^0'=x_10^post7, (0 == 0 /\ -temp6_11^post7+temp6_11^0 == 0 /\ nondet_7^0-nondet_7^post7 == 0 /\ -nondet_8^post7+temp5_9^post7 == 0 /\ -temp5_9^post7 <= 0 /\ -temp5_9^post7 == 0 /\ temp5_9^post7 <= 0 /\ x_10^0-x_10^post7 == 0), cost: 1
	New rule:
	l4 -> l3 : nondet_7^0'=nondet_7^0, nondet_8^0'=0, result_6^0'=result_6^post7, temp5_9^0'=0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 <= 0 /\ 0 == 0), cost: 1
	
		propagated equality temp6_11^post7 = temp6_11^0
		
		propagated equality nondet_7^post7 = nondet_7^0
		
		propagated equality nondet_8^post7 = temp5_9^post7
		
		propagated equality temp5_9^post7 = 0
		
		propagated equality x_10^post7 = x_10^0
		
	Simplified Guard

	Original rule:
	l4 -> l3 : nondet_7^0'=nondet_7^0, nondet_8^0'=0, result_6^0'=result_6^post7, temp5_9^0'=0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 <= 0 /\ 0 == 0), cost: 1
	New rule:
	l4 -> l3 : nondet_7^0'=nondet_7^0, nondet_8^0'=0, result_6^0'=result_6^post7, temp5_9^0'=0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l3 : nondet_7^0'=nondet_7^0, nondet_8^0'=0, result_6^0'=result_6^post7, temp5_9^0'=0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, T, cost: 1
	New rule:
	l4 -> l3 : nondet_8^0'=0, result_6^0'=result_6^post7, temp5_9^0'=0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l8 : nondet_7^0'=nondet_7^post8, nondet_8^0'=nondet_8^post8, result_6^0'=result_6^post8, temp5_9^0'=temp5_9^post8, temp6_11^0'=temp6_11^post8, x_10^0'=x_10^post8, (0 == 0 /\ -nondet_8^post8+temp5_9^post8 == 0 /\ nondet_7^0-nondet_7^post8 == 0 /\ -result_6^post8+result_6^0 == 0 /\ x_10^0-x_10^post8 == 0 /\ -temp6_11^post8+temp6_11^0 == 0), cost: 1
	New rule:
	l4 -> l8 : nondet_7^0'=nondet_7^0, nondet_8^0'=temp5_9^post8, result_6^0'=result_6^0, temp5_9^0'=temp5_9^post8, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 0 == 0, cost: 1
	
		propagated equality nondet_8^post8 = temp5_9^post8
		
		propagated equality nondet_7^post8 = nondet_7^0
		
		propagated equality result_6^post8 = result_6^0
		
		propagated equality x_10^post8 = x_10^0
		
		propagated equality temp6_11^post8 = temp6_11^0
		
	Simplified Guard

	Original rule:
	l4 -> l8 : nondet_7^0'=nondet_7^0, nondet_8^0'=temp5_9^post8, result_6^0'=result_6^0, temp5_9^0'=temp5_9^post8, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 0 == 0, cost: 1
	New rule:
	l4 -> l8 : nondet_7^0'=nondet_7^0, nondet_8^0'=temp5_9^post8, result_6^0'=result_6^0, temp5_9^0'=temp5_9^post8, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l8 : nondet_7^0'=nondet_7^0, nondet_8^0'=temp5_9^post8, result_6^0'=result_6^0, temp5_9^0'=temp5_9^post8, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, T, cost: 1
	New rule:
	l4 -> l8 : nondet_8^0'=temp5_9^post8, temp5_9^0'=temp5_9^post8, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l8 -> l9 : nondet_7^0'=nondet_7^post9, nondet_8^0'=nondet_8^post9, result_6^0'=result_6^post9, temp5_9^0'=temp5_9^post9, temp6_11^0'=temp6_11^post9, x_10^0'=x_10^post9, (x_10^0-x_10^post9 == 0 /\ nondet_8^0-nondet_8^post9 == 0 /\ -result_6^post9+result_6^0 == 0 /\ nondet_7^0-nondet_7^post9 == 0 /\ 1+temp5_9^0 <= 0 /\ -temp6_11^post9+temp6_11^0 == 0 /\ temp5_9^0-temp5_9^post9 == 0), cost: 1
	New rule:
	l8 -> l9 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 == 0 /\ 1+temp5_9^0 <= 0), cost: 1
	
		propagated equality x_10^post9 = x_10^0
		
		propagated equality nondet_8^post9 = nondet_8^0
		
		propagated equality result_6^post9 = result_6^0
		
		propagated equality nondet_7^post9 = nondet_7^0
		
		propagated equality temp6_11^post9 = temp6_11^0
		
		propagated equality temp5_9^post9 = temp5_9^0
		
	Simplified Guard

	Original rule:
	l8 -> l9 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 == 0 /\ 1+temp5_9^0 <= 0), cost: 1
	New rule:
	l8 -> l9 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 1+temp5_9^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l8 -> l9 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 1+temp5_9^0 <= 0, cost: 1
	New rule:
	l8 -> l9 : 1+temp5_9^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l8 -> l9 : nondet_7^0'=nondet_7^post10, nondet_8^0'=nondet_8^post10, result_6^0'=result_6^post10, temp5_9^0'=temp5_9^post10, temp6_11^0'=temp6_11^post10, x_10^0'=x_10^post10, (nondet_7^0-nondet_7^post10 == 0 /\ -temp5_9^post10+temp5_9^0 == 0 /\ x_10^0-x_10^post10 == 0 /\ -temp6_11^post10+temp6_11^0 == 0 /\ 1-temp5_9^0 <= 0 /\ -nondet_8^post10+nondet_8^0 == 0 /\ -result_6^post10+result_6^0 == 0), cost: 1
	New rule:
	l8 -> l9 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 == 0 /\ 1-temp5_9^0 <= 0), cost: 1
	
		propagated equality nondet_7^post10 = nondet_7^0
		
		propagated equality temp5_9^post10 = temp5_9^0
		
		propagated equality x_10^post10 = x_10^0
		
		propagated equality temp6_11^post10 = temp6_11^0
		
		propagated equality nondet_8^post10 = nondet_8^0
		
		propagated equality result_6^post10 = result_6^0
		
	Simplified Guard

	Original rule:
	l8 -> l9 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 == 0 /\ 1-temp5_9^0 <= 0), cost: 1
	New rule:
	l8 -> l9 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 1-temp5_9^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l8 -> l9 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 1-temp5_9^0 <= 0, cost: 1
	New rule:
	l8 -> l9 : 1-temp5_9^0 <= 0, cost: 1
	
	made implied equalities explicit

	Original rule:
	l1 -> l3 : nondet_7^0'=nondet_7^post13, nondet_8^0'=nondet_8^post13, result_6^0'=result_6^post13, temp5_9^0'=temp5_9^post13, temp6_11^0'=temp6_11^post13, x_10^0'=x_10^post13, (0 == 0 /\ -x_10^post13+x_10^0 == 0 /\ temp5_9^post13-nondet_8^post13 == 0 /\ -temp6_11^post13+temp6_11^0 == 0 /\ nondet_7^0-nondet_7^post13 == 0 /\ temp5_9^post13 <= 0 /\ -temp5_9^post13 <= 0), cost: 1
	New rule:
	l1 -> l3 : nondet_7^0'=nondet_7^post13, nondet_8^0'=nondet_8^post13, result_6^0'=result_6^post13, temp5_9^0'=temp5_9^post13, temp6_11^0'=temp6_11^post13, x_10^0'=x_10^post13, (0 == 0 /\ -x_10^post13+x_10^0 == 0 /\ temp5_9^post13-nondet_8^post13 == 0 /\ -temp6_11^post13+temp6_11^0 == 0 /\ nondet_7^0-nondet_7^post13 == 0 /\ temp5_9^post13 <= 0 /\ temp5_9^post13 == 0 /\ -temp5_9^post13 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l3 : nondet_7^0'=nondet_7^post13, nondet_8^0'=nondet_8^post13, result_6^0'=result_6^post13, temp5_9^0'=temp5_9^post13, temp6_11^0'=temp6_11^post13, x_10^0'=x_10^post13, (0 == 0 /\ -x_10^post13+x_10^0 == 0 /\ temp5_9^post13-nondet_8^post13 == 0 /\ -temp6_11^post13+temp6_11^0 == 0 /\ nondet_7^0-nondet_7^post13 == 0 /\ temp5_9^post13 <= 0 /\ temp5_9^post13 == 0 /\ -temp5_9^post13 <= 0), cost: 1
	New rule:
	l1 -> l3 : nondet_7^0'=nondet_7^0, nondet_8^0'=0, result_6^0'=result_6^post13, temp5_9^0'=0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 <= 0 /\ 0 == 0), cost: 1
	
		propagated equality x_10^post13 = x_10^0
		
		propagated equality nondet_8^post13 = temp5_9^post13
		
		propagated equality temp6_11^post13 = temp6_11^0
		
		propagated equality nondet_7^post13 = nondet_7^0
		
		propagated equality temp5_9^post13 = 0
		
	Simplified Guard

	Original rule:
	l1 -> l3 : nondet_7^0'=nondet_7^0, nondet_8^0'=0, result_6^0'=result_6^post13, temp5_9^0'=0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 <= 0 /\ 0 == 0), cost: 1
	New rule:
	l1 -> l3 : nondet_7^0'=nondet_7^0, nondet_8^0'=0, result_6^0'=result_6^post13, temp5_9^0'=0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l3 : nondet_7^0'=nondet_7^0, nondet_8^0'=0, result_6^0'=result_6^post13, temp5_9^0'=0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, T, cost: 1
	New rule:
	l1 -> l3 : nondet_8^0'=0, result_6^0'=result_6^post13, temp5_9^0'=0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l10 : nondet_7^0'=nondet_7^post14, nondet_8^0'=nondet_8^post14, result_6^0'=result_6^post14, temp5_9^0'=temp5_9^post14, temp6_11^0'=temp6_11^post14, x_10^0'=x_10^post14, (0 == 0 /\ -temp6_11^post14+temp6_11^0 == 0 /\ temp5_9^post14-nondet_8^post14 == 0 /\ -nondet_7^post14+nondet_7^0 == 0 /\ result_6^0-result_6^post14 == 0 /\ x_10^0-x_10^post14 == 0), cost: 1
	New rule:
	l1 -> l10 : nondet_7^0'=nondet_7^0, nondet_8^0'=temp5_9^post14, result_6^0'=result_6^0, temp5_9^0'=temp5_9^post14, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 0 == 0, cost: 1
	
		propagated equality temp6_11^post14 = temp6_11^0
		
		propagated equality nondet_8^post14 = temp5_9^post14
		
		propagated equality nondet_7^post14 = nondet_7^0
		
		propagated equality result_6^post14 = result_6^0
		
		propagated equality x_10^post14 = x_10^0
		
	Simplified Guard

	Original rule:
	l1 -> l10 : nondet_7^0'=nondet_7^0, nondet_8^0'=temp5_9^post14, result_6^0'=result_6^0, temp5_9^0'=temp5_9^post14, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 0 == 0, cost: 1
	New rule:
	l1 -> l10 : nondet_7^0'=nondet_7^0, nondet_8^0'=temp5_9^post14, result_6^0'=result_6^0, temp5_9^0'=temp5_9^post14, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l10 : nondet_7^0'=nondet_7^0, nondet_8^0'=temp5_9^post14, result_6^0'=result_6^0, temp5_9^0'=temp5_9^post14, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, T, cost: 1
	New rule:
	l1 -> l10 : nondet_8^0'=temp5_9^post14, temp5_9^0'=temp5_9^post14, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l10 -> l11 : nondet_7^0'=nondet_7^post15, nondet_8^0'=nondet_8^post15, result_6^0'=result_6^post15, temp5_9^0'=temp5_9^post15, temp6_11^0'=temp6_11^post15, x_10^0'=x_10^post15, (1+temp5_9^0 <= 0 /\ x_10^0-x_10^post15 == 0 /\ result_6^0-result_6^post15 == 0 /\ nondet_8^0-nondet_8^post15 == 0 /\ -temp5_9^post15+temp5_9^0 == 0 /\ -nondet_7^post15+nondet_7^0 == 0 /\ -temp6_11^post15+temp6_11^0 == 0), cost: 1
	New rule:
	l10 -> l11 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 == 0 /\ 1+temp5_9^0 <= 0), cost: 1
	
		propagated equality x_10^post15 = x_10^0
		
		propagated equality result_6^post15 = result_6^0
		
		propagated equality nondet_8^post15 = nondet_8^0
		
		propagated equality temp5_9^post15 = temp5_9^0
		
		propagated equality nondet_7^post15 = nondet_7^0
		
		propagated equality temp6_11^post15 = temp6_11^0
		
	Simplified Guard

	Original rule:
	l10 -> l11 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 == 0 /\ 1+temp5_9^0 <= 0), cost: 1
	New rule:
	l10 -> l11 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 1+temp5_9^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l10 -> l11 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 1+temp5_9^0 <= 0, cost: 1
	New rule:
	l10 -> l11 : 1+temp5_9^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l10 -> l11 : nondet_7^0'=nondet_7^post16, nondet_8^0'=nondet_8^post16, result_6^0'=result_6^post16, temp5_9^0'=temp5_9^post16, temp6_11^0'=temp6_11^post16, x_10^0'=x_10^post16, (-temp6_11^post16+temp6_11^0 == 0 /\ nondet_8^0-nondet_8^post16 == 0 /\ nondet_7^0-nondet_7^post16 == 0 /\ -result_6^post16+result_6^0 == 0 /\ temp5_9^0-temp5_9^post16 == 0 /\ 1-temp5_9^0 <= 0 /\ x_10^0-x_10^post16 == 0), cost: 1
	New rule:
	l10 -> l11 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 == 0 /\ 1-temp5_9^0 <= 0), cost: 1
	
		propagated equality temp6_11^post16 = temp6_11^0
		
		propagated equality nondet_8^post16 = nondet_8^0
		
		propagated equality nondet_7^post16 = nondet_7^0
		
		propagated equality result_6^post16 = result_6^0
		
		propagated equality temp5_9^post16 = temp5_9^0
		
		propagated equality x_10^post16 = x_10^0
		
	Simplified Guard

	Original rule:
	l10 -> l11 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, (0 == 0 /\ 1-temp5_9^0 <= 0), cost: 1
	New rule:
	l10 -> l11 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 1-temp5_9^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l10 -> l11 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=x_10^0, 1-temp5_9^0 <= 0, cost: 1
	New rule:
	l10 -> l11 : 1-temp5_9^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l11 -> l4 : nondet_7^0'=nondet_7^post17, nondet_8^0'=nondet_8^post17, result_6^0'=result_6^post17, temp5_9^0'=temp5_9^post17, temp6_11^0'=temp6_11^post17, x_10^0'=x_10^post17, (-result_6^post17+result_6^0 == 0 /\ 1-x_10^0 <= 0 /\ -temp6_11^post17+temp6_11^0 == 0 /\ -1-x_10^0+x_10^post17 == 0 /\ nondet_7^0-nondet_7^post17 == 0 /\ temp5_9^0-temp5_9^post17 == 0 /\ nondet_8^0-nondet_8^post17 == 0), cost: 1
	New rule:
	l11 -> l4 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=1+x_10^0, (0 == 0 /\ 1-x_10^0 <= 0), cost: 1
	
		propagated equality result_6^post17 = result_6^0
		
		propagated equality temp6_11^post17 = temp6_11^0
		
		propagated equality x_10^post17 = 1+x_10^0
		
		propagated equality nondet_7^post17 = nondet_7^0
		
		propagated equality temp5_9^post17 = temp5_9^0
		
		propagated equality nondet_8^post17 = nondet_8^0
		
	Simplified Guard

	Original rule:
	l11 -> l4 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=1+x_10^0, (0 == 0 /\ 1-x_10^0 <= 0), cost: 1
	New rule:
	l11 -> l4 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=1+x_10^0, 1-x_10^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l11 -> l4 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=1+x_10^0, 1-x_10^0 <= 0, cost: 1
	New rule:
	l11 -> l4 : x_10^0'=1+x_10^0, 1-x_10^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l12 -> l1 : nondet_7^0'=nondet_7^post1, nondet_8^0'=nondet_8^post1, result_6^0'=result_6^post1, temp5_9^0'=temp5_9^post1, temp6_11^0'=temp6_11^post1, x_10^0'=x_10^post1, (0 == 0 /\ -nondet_8^post18+nondet_8^0 == 0 /\ nondet_8^post18-nondet_8^post1 == 0 /\ nondet_7^0-nondet_7^post18 == 0 /\ result_6^post18-result_6^post1 == 0 /\ -temp5_9^post18+temp5_9^0 == 0 /\ -result_6^post18+result_6^0 == 0 /\ -temp6_11^post18+temp6_11^0 == 0 /\ x_10^0-x_10^post18 == 0 /\ -temp6_11^post1+x_10^post1 == 0 /\ temp5_9^post18-temp5_9^post1 == 0 /\ temp6_11^post1-nondet_7^post1 == 0), cost: 1
	New rule:
	l12 -> l1 : nondet_7^0'=x_10^post1, nondet_8^0'=nondet_8^post18, result_6^0'=result_6^post18, temp5_9^0'=temp5_9^post18, temp6_11^0'=x_10^post1, x_10^0'=x_10^post1, (0 == 0 /\ -nondet_8^post18+nondet_8^0 == 0 /\ nondet_7^0-nondet_7^post18 == 0 /\ -temp5_9^post18+temp5_9^0 == 0 /\ -result_6^post18+result_6^0 == 0 /\ -temp6_11^post18+temp6_11^0 == 0 /\ x_10^0-x_10^post18 == 0), cost: 1
	
		propagated equality nondet_8^post1 = nondet_8^post18
		
		propagated equality result_6^post1 = result_6^post18
		
		propagated equality temp6_11^post1 = x_10^post1
		
		propagated equality temp5_9^post1 = temp5_9^post18
		
		propagated equality nondet_7^post1 = x_10^post1
		
	Propagated Equalities

	Original rule:
	l12 -> l1 : nondet_7^0'=x_10^post1, nondet_8^0'=nondet_8^post18, result_6^0'=result_6^post18, temp5_9^0'=temp5_9^post18, temp6_11^0'=x_10^post1, x_10^0'=x_10^post1, (0 == 0 /\ -nondet_8^post18+nondet_8^0 == 0 /\ nondet_7^0-nondet_7^post18 == 0 /\ -temp5_9^post18+temp5_9^0 == 0 /\ -result_6^post18+result_6^0 == 0 /\ -temp6_11^post18+temp6_11^0 == 0 /\ x_10^0-x_10^post18 == 0), cost: 1
	New rule:
	l12 -> l1 : nondet_7^0'=x_10^post1, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=x_10^post1, x_10^0'=x_10^post1, 0 == 0, cost: 1
	
		propagated equality nondet_8^post18 = nondet_8^0
		
		propagated equality nondet_7^post18 = nondet_7^0
		
		propagated equality temp5_9^post18 = temp5_9^0
		
		propagated equality result_6^post18 = result_6^0
		
		propagated equality temp6_11^post18 = temp6_11^0
		
		propagated equality x_10^post18 = x_10^0
		
	Simplified Guard

	Original rule:
	l12 -> l1 : nondet_7^0'=x_10^post1, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=x_10^post1, x_10^0'=x_10^post1, 0 == 0, cost: 1
	New rule:
	l12 -> l1 : nondet_7^0'=x_10^post1, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=x_10^post1, x_10^0'=x_10^post1, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l12 -> l1 : nondet_7^0'=x_10^post1, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=x_10^post1, x_10^0'=x_10^post1, T, cost: 1
	New rule:
	l12 -> l1 : nondet_7^0'=x_10^post1, temp6_11^0'=x_10^post1, x_10^0'=x_10^post1, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l9 -> l4 : nondet_7^0'=nondet_7^post12, nondet_8^0'=nondet_8^post12, result_6^0'=result_6^post12, temp5_9^0'=temp5_9^post12, temp6_11^0'=temp6_11^post12, x_10^0'=x_10^post12, (-1-x_10^0+x_10^post11 == 0 /\ -nondet_8^post12+nondet_8^post11 == 0 /\ 1-x_10^0 <= 0 /\ -x_10^post12+x_10^post11 == 0 /\ -result_6^post11+result_6^0 == 0 /\ nondet_8^0-nondet_8^post11 == 0 /\ -temp5_9^post12+temp5_9^post11 == 0 /\ temp6_11^post11-temp6_11^post12 == 0 /\ -temp6_11^post11+temp6_11^0 == 0 /\ -result_6^post12+result_6^post11 == 0 /\ -temp5_9^post11+temp5_9^0 == 0 /\ -nondet_7^post12+nondet_7^post11 == 0 /\ nondet_7^0-nondet_7^post11 == 0), cost: 1
	New rule:
	l9 -> l4 : nondet_7^0'=nondet_7^post11, nondet_8^0'=nondet_8^post11, result_6^0'=result_6^post11, temp5_9^0'=temp5_9^post11, temp6_11^0'=temp6_11^post11, x_10^0'=x_10^post11, (0 == 0 /\ -1-x_10^0+x_10^post11 == 0 /\ 1-x_10^0 <= 0 /\ -result_6^post11+result_6^0 == 0 /\ nondet_8^0-nondet_8^post11 == 0 /\ -temp6_11^post11+temp6_11^0 == 0 /\ -temp5_9^post11+temp5_9^0 == 0 /\ nondet_7^0-nondet_7^post11 == 0), cost: 1
	
		propagated equality nondet_8^post12 = nondet_8^post11
		
		propagated equality x_10^post12 = x_10^post11
		
		propagated equality temp5_9^post12 = temp5_9^post11
		
		propagated equality temp6_11^post12 = temp6_11^post11
		
		propagated equality result_6^post12 = result_6^post11
		
		propagated equality nondet_7^post12 = nondet_7^post11
		
	Propagated Equalities

	Original rule:
	l9 -> l4 : nondet_7^0'=nondet_7^post11, nondet_8^0'=nondet_8^post11, result_6^0'=result_6^post11, temp5_9^0'=temp5_9^post11, temp6_11^0'=temp6_11^post11, x_10^0'=x_10^post11, (0 == 0 /\ -1-x_10^0+x_10^post11 == 0 /\ 1-x_10^0 <= 0 /\ -result_6^post11+result_6^0 == 0 /\ nondet_8^0-nondet_8^post11 == 0 /\ -temp6_11^post11+temp6_11^0 == 0 /\ -temp5_9^post11+temp5_9^0 == 0 /\ nondet_7^0-nondet_7^post11 == 0), cost: 1
	New rule:
	l9 -> l4 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=1+x_10^0, (0 == 0 /\ 1-x_10^0 <= 0), cost: 1
	
		propagated equality x_10^post11 = 1+x_10^0
		
		propagated equality result_6^post11 = result_6^0
		
		propagated equality nondet_8^post11 = nondet_8^0
		
		propagated equality temp6_11^post11 = temp6_11^0
		
		propagated equality temp5_9^post11 = temp5_9^0
		
		propagated equality nondet_7^post11 = nondet_7^0
		
	Simplified Guard

	Original rule:
	l9 -> l4 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=1+x_10^0, (0 == 0 /\ 1-x_10^0 <= 0), cost: 1
	New rule:
	l9 -> l4 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=1+x_10^0, 1-x_10^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l9 -> l4 : nondet_7^0'=nondet_7^0, nondet_8^0'=nondet_8^0, result_6^0'=result_6^0, temp5_9^0'=temp5_9^0, temp6_11^0'=temp6_11^0, x_10^0'=1+x_10^0, 1-x_10^0 <= 0, cost: 1
	New rule:
	l9 -> l4 : x_10^0'=1+x_10^0, 1-x_10^0 <= 0, cost: 1

Step with 34

	Trace

	34[T]
	
	Blocked

	[{}, {}]

Step with 29

	Trace

	34[T], 29[T]
	
	Blocked

	[{}, {}, {}]

Backtrack

	Trace

	34[T]
	
	Blocked

	[{}, {29[T]}]

Step with 30

	Trace

	34[T], 30[T]
	
	Blocked

	[{}, {29[T]}, {}]

Step with 31

	Trace

	34[T], 30[T], 31[(1+temp5_9^0 <= 0)]
	
	Blocked

	[{}, {29[T]}, {}, {}]

Step with 33

	Trace

	34[T], 30[T], 31[(1+temp5_9^0 <= 0)], 33[(1-x_10^0 <= 0)]
	
	Blocked

	[{}, {29[T]}, {}, {}, {}]

Step with 25

	Trace

	34[T], 30[T], 31[(1+temp5_9^0 <= 0)], 33[(1-x_10^0 <= 0)], 25[T]
	
	Blocked

	[{}, {29[T]}, {}, {}, {}, {}]

Backtrack

	Trace

	34[T], 30[T], 31[(1+temp5_9^0 <= 0)], 33[(1-x_10^0 <= 0)]
	
	Blocked

	[{}, {29[T]}, {}, {}, {25[T]}]

Step with 26

	Trace

	34[T], 30[T], 31[(1+temp5_9^0 <= 0)], 33[(1-x_10^0 <= 0)], 26[T]
	
	Blocked

	[{}, {29[T]}, {}, {}, {25[T]}, {}]

Step with 27

	Trace

	34[T], 30[T], 31[(1+temp5_9^0 <= 0)], 33[(1-x_10^0 <= 0)], 26[T], 27[(1+temp5_9^0 <= 0)]
	
	Blocked

	[{}, {29[T]}, {}, {}, {25[T]}, {}, {}]

Step with 35

	Trace

	34[T], 30[T], 31[(1+temp5_9^0 <= 0)], 33[(1-x_10^0 <= 0)], 26[T], 27[(1+temp5_9^0 <= 0)], 35[(1-x_10^0 <= 0)]
	
	Blocked

	[{}, {29[T]}, {}, {}, {25[T]}, {}, {}, {}]

Nonterm

Start location: l12
Program variables: nondet_7^0 nondet_8^0 result_6^0 temp5_9^0 temp6_11^0 x_10^0
  29: l1 -> l3 : nondet_8^0'=0, result_6^0'=result_6^post13, temp5_9^0'=0, T, cost: 1
  30: l1 -> l10 : nondet_8^0'=temp5_9^post14, temp5_9^0'=temp5_9^post14, T, cost: 1
  20: l2 -> l3 : nondet_8^0'=0, result_6^0'=result_6^post2, temp5_9^0'=0, T, cost: 1
  21: l2 -> l5 : nondet_8^0'=temp5_9^post3, temp5_9^0'=temp5_9^post3, T, cost: 1
  22: l5 -> l6 : 1+temp5_9^0 <= 0, cost: 1
  23: l5 -> l6 : 1-temp5_9^0 <= 0, cost: 1
  24: l6 -> l4 : x_10^0'=1+x_10^0, 1-x_10^0 <= 0, cost: 1
  25: l4 -> l3 : nondet_8^0'=0, result_6^0'=result_6^post7, temp5_9^0'=0, T, cost: 1
  26: l4 -> l8 : nondet_8^0'=temp5_9^post8, temp5_9^0'=temp5_9^post8, T, cost: 1
  36: l4 -> LoAT_sink : (-1+x_10^0 >= 0 /\ -1+n >= 0 /\ -1-temp5_9^post81 >= 0), cost: NONTERM
  37: l4 -> l4 : nondet_8^0'=temp5_9^post81, temp5_9^0'=temp5_9^post81, x_10^0'=x_10^0+n, (-1+x_10^0 >= 0 /\ -1+n >= 0 /\ -1-temp5_9^post81 >= 0), cost: 1
  27: l8 -> l9 : 1+temp5_9^0 <= 0, cost: 1
  28: l8 -> l9 : 1-temp5_9^0 <= 0, cost: 1
  35: l9 -> l4 : x_10^0'=1+x_10^0, 1-x_10^0 <= 0, cost: 1
  31: l10 -> l11 : 1+temp5_9^0 <= 0, cost: 1
  32: l10 -> l11 : 1-temp5_9^0 <= 0, cost: 1
  33: l11 -> l4 : x_10^0'=1+x_10^0, 1-x_10^0 <= 0, cost: 1
  34: l12 -> l1 : nondet_7^0'=x_10^post1, temp6_11^0'=x_10^post1, x_10^0'=x_10^post1, T, cost: 1

	Certificate of Non-Termination

	Original rule:
	l4 -> l4 : nondet_8^0'=temp5_9^post81, temp5_9^0'=temp5_9^post81, x_10^0'=1+x_10^0, (1-x_10^0 <= 0 /\ 1+temp5_9^post81 <= 0), cost: 1
	New rule:
	l4 -> LoAT_sink : (-1+x_10^0 >= 0 /\ -1+n >= 0 /\ -1-temp5_9^post81 >= 0), cost: NONTERM

		-1+x_10^0 >= 0 [0]: monotonic increase yields -1+x_10^0 >= 0
		
		-1-temp5_9^post81 >= 0 [0]: monotonic increase yields -1-temp5_9^post81 >= 0
		
		Replacement map: {-1+x_10^0 >= 0 -> -1+x_10^0 >= 0, -1-temp5_9^post81 >= 0 -> -1-temp5_9^post81 >= 0}

	Loop Acceleration

	Original rule:
	l4 -> l4 : nondet_8^0'=temp5_9^post81, temp5_9^0'=temp5_9^post81, x_10^0'=1+x_10^0, (1-x_10^0 <= 0 /\ 1+temp5_9^post81 <= 0), cost: 1
	New rule:
	l4 -> l4 : nondet_8^0'=temp5_9^post81, temp5_9^0'=temp5_9^post81, x_10^0'=x_10^0+n, (-1+x_10^0 >= 0 /\ -1+n >= 0 /\ -1-temp5_9^post81 >= 0), cost: 1

		-1+x_10^0 >= 0 [0]: monotonic increase yields -1+x_10^0 >= 0
		
		-1-temp5_9^post81 >= 0 [0]: monotonic increase yields -1-temp5_9^post81 >= 0
		
		Replacement map: {-1+x_10^0 >= 0 -> -1+x_10^0 >= 0, -1-temp5_9^post81 >= 0 -> -1-temp5_9^post81 >= 0}

Step with 36

	Trace

	34[T], 30[T], 31[(1+temp5_9^0 <= 0)], 33[(1-x_10^0 <= 0)], 36[(-1+x_10^0 >= 0 /\ -1+n >= 0 /\ -1-temp5_9^post81 >= 0)]
	
	Blocked

	[{}, {29[T]}, {}, {}, {25[T]}, {36[T]}]

Refute

	Counterexample

	[ nondet_7^0=1 nondet_8^0=0 result_6^0=0 temp5_9^0=0 temp6_11^0=1 x_10^0=1 ] 34 [ nondet_7^0=1 nondet_8^0=-1 result_6^0=0 temp5_9^0=-1 temp6_11^0=1 x_10^0=1 ] 30 [ nondet_7^0=1 nondet_8^0=-1 result_6^0=0 temp5_9^0=-1 temp6_11^0=1 x_10^0=1 ] 31 [ nondet_7^0=1 nondet_8^0=-1 result_6^0=0 temp5_9^0=-1 temp6_11^0=1 x_10^0=2 ] 33 [ nondet_7^0=nondet_7^0 nondet_8^0=0 result_6^0=0 temp5_9^0=0 temp6_11^0=temp6_11^0 x_10^0=x_10^0 ] 36
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b