WORST_CASE(Omega(0),?)

Initial ITS
Start location: l17
   0: l0 -> l1 : r^0'=r^post0, d^0'=d^post0, n^0'=n^post0, c^0'=c^post0, s^0'=s^post0, f^0'=f^post0, (-r^0+n^0 <= 0 /\ d^0-d^post0 == 0 /\ -n^post0+n^0 == 0 /\ -c^post0+c^0 == 0 /\ -f^post0+f^0 == 0 /\ s^0-s^post0 == 0 /\ r^0-r^post0 == 0), cost: 1
   1: l0 -> l2 : r^0'=r^post1, d^0'=d^post1, n^0'=n^post1, c^0'=c^post1, s^0'=s^post1, f^0'=f^post1, (-s^post1+s^0 == 0 /\ -c^post1+c^0 == 0 /\ -f^post1+f^0 == 0 /\ 1+r^0-n^0 <= 0 /\ r^0-r^post1 == 0 /\ n^0-n^post1 == 0 /\ d^0-d^post1 == 0), cost: 1
  20: l1 -> l6 : r^0'=r^post20, d^0'=d^post20, n^0'=n^post20, c^0'=c^post20, s^0'=s^post20, f^0'=f^post20, (d^0-d^post20 == 0 /\ -n^post20+n^0 == 0 /\ r^0-r^post20 == 0 /\ s^0-s^post20 == 0 /\ f^0-f^post20 == 0 /\ r^0-n^0 <= 0 /\ -c^post20+c^0 == 0), cost: 1
  21: l1 -> l12 : r^0'=r^post21, d^0'=d^post21, n^0'=n^post21, c^0'=c^post21, s^0'=s^post21, f^0'=f^post21, (f^0-f^post21 == 0 /\ 1-r^0+n^0 <= 0 /\ -c^post21+c^0 == 0 /\ -s^post21+s^0 == 0 /\ d^0-d^post21 == 0 /\ r^0-r^post21 == 0 /\ n^0-n^post21 == 0), cost: 1
  28: l2 -> l14 : r^0'=r^post28, d^0'=d^post28, n^0'=n^post28, c^0'=c^post28, s^0'=s^post28, f^0'=f^post28, (-s^post28+s^0 == 0 /\ -f^post28+f^0 == 0 /\ -c^post28+c^0 == 0 /\ d^0-d^post28 == 0 /\ n^0-n^post28 == 0 /\ -r^post28+r^0 == 0 /\ 2-d^0 <= 0), cost: 1
  29: l2 -> l14 : r^0'=r^post29, d^0'=d^post29, n^0'=n^post29, c^0'=c^post29, s^0'=s^post29, f^0'=f^post29, (-f^post29+f^0 == 0 /\ r^0-r^post29 == 0 /\ d^0 <= 0 /\ c^0-c^post29 == 0 /\ n^0-n^post29 == 0 /\ d^0-d^post29 == 0 /\ -s^post29+s^0 == 0), cost: 1
  30: l2 -> l15 : r^0'=r^post30, d^0'=d^post30, n^0'=n^post30, c^0'=c^post30, s^0'=s^post30, f^0'=f^post30, (r^0-r^post30 == 0 /\ -d^post30+d^0 == 0 /\ n^0-n^post30 == 0 /\ -f^post30+f^0 == 0 /\ -s^post30+s^0 == 0 /\ c^0-c^post30 == 0 /\ 1-d^0 <= 0 /\ -1+d^0 <= 0), cost: 1
   2: l3 -> l0 : r^0'=r^post2, d^0'=d^post2, n^0'=n^post2, c^0'=c^post2, s^0'=s^post2, f^0'=f^post2, (1-c^0+c^post2 == 0 /\ -f^post2+f^0 == 0 /\ d^0-d^post2 == 0 /\ r^0-r^post2 == 0 /\ n^0-n^post2 == 0 /\ -s^post2+s^0 == 0), cost: 1
   3: l4 -> l0 : r^0'=r^post3, d^0'=d^post3, n^0'=n^post3, c^0'=c^post3, s^0'=s^post3, f^0'=f^post3, (c^0-c^post3 == 0 /\ -f^post3+f^0 == 0 /\ n^0-n^post3 == 0 /\ -f^0 <= 0 /\ d^0-d^post3 == 0 /\ r^0-r^post3 == 0 /\ -s^post3+s^0 == 0 /\ f^0 <= 0), cost: 1
   4: l4 -> l3 : r^0'=r^post4, d^0'=d^post4, n^0'=n^post4, c^0'=c^post4, s^0'=s^post4, f^0'=f^post4, (n^0-n^post4 == 0 /\ c^0-c^post4 == 0 /\ 1-f^0 <= 0 /\ -d^post4+d^0 == 0 /\ r^0-r^post4 == 0 /\ -f^post4+f^0 == 0 /\ -s^post4+s^0 == 0), cost: 1
   5: l4 -> l3 : r^0'=r^post5, d^0'=d^post5, n^0'=n^post5, c^0'=c^post5, s^0'=s^post5, f^0'=f^post5, (-f^post5+f^0 == 0 /\ -n^post5+n^0 == 0 /\ r^0-r^post5 == 0 /\ 1+f^0 <= 0 /\ c^0-c^post5 == 0 /\ s^0-s^post5 == 0 /\ d^0-d^post5 == 0), cost: 1
   6: l5 -> l4 : r^0'=r^post6, d^0'=d^post6, n^0'=n^post6, c^0'=c^post6, s^0'=s^post6, f^0'=f^post6, (r^0-r^post6 == 0 /\ -f^post6+f^0 == 0 /\ -n^post6+n^0 == 0 /\ s^0-s^post6 == 0 /\ -c^post6+c^0 == 0 /\ d^0-d^post6 == 0 /\ 2-c^0 <= 0), cost: 1
   7: l5 -> l4 : r^0'=r^post7, d^0'=d^post7, n^0'=n^post7, c^0'=c^post7, s^0'=s^post7, f^0'=f^post7, (f^0-f^post7 == 0 /\ c^0 <= 0 /\ -s^post7+s^0 == 0 /\ r^0-r^post7 == 0 /\ n^0-n^post7 == 0 /\ d^0-d^post7 == 0 /\ -c^post7+c^0 == 0), cost: 1
   8: l5 -> l6 : r^0'=r^post8, d^0'=d^post8, n^0'=n^post8, c^0'=c^post8, s^0'=s^post8, f^0'=f^post8, (-s^post8+s^0 == 0 /\ -f^post8+f^0 == 0 /\ -c^post8+c^0 == 0 /\ n^0-n^post8 == 0 /\ d^0-d^post8 == 0 /\ 1-c^0 <= 0 /\ -1+c^0 <= 0 /\ r^0-r^post8 == 0), cost: 1
   9: l6 -> l7 : r^0'=r^post9, d^0'=d^post9, n^0'=n^post9, c^0'=c^post9, s^0'=s^post9, f^0'=f^post9, (-s^post9+s^0 == 0 /\ -c^post9+c^0 == 0 /\ d^0-d^post9 == 0 /\ -f^post9+f^0 == 0 /\ n^0-n^post9 == 0 /\ -r^post9+r^0 == 0), cost: 1
  10: l8 -> l9 : r^0'=r^post10, d^0'=d^post10, n^0'=n^post10, c^0'=c^post10, s^0'=s^post10, f^0'=f^post10, (r^0-r^post10 == 0 /\ -d^post10+d^0 == 0 /\ n^0-n^post10 == 0 /\ c^0-c^post10 == 0 /\ -f^post10+f^0 == 0 /\ -s^post10+s^0 == 0 /\ -s^0 <= 0), cost: 1
  11: l8 -> l6 : r^0'=r^post11, d^0'=d^post11, n^0'=n^post11, c^0'=c^post11, s^0'=s^post11, f^0'=f^post11, (c^0-c^post11 == 0 /\ -f^post11+f^0 == 0 /\ 1+s^0 <= 0 /\ r^0-r^post11 == 0 /\ n^0-n^post11 == 0 /\ d^0-d^post11 == 0 /\ s^0-s^post11 == 0), cost: 1
  16: l9 -> l5 : r^0'=r^post16, d^0'=d^post16, n^0'=n^post16, c^0'=c^post16, s^0'=s^post16, f^0'=f^post16, (0 == 0 /\ r^0-r^post16 == 0 /\ -d^post16+d^0 == 0 /\ -c^post16+c^0 == 0 /\ -f^post16+f^0 == 0 /\ -s^post16+s^0 == 0), cost: 1
  12: l10 -> l8 : r^0'=r^post12, d^0'=d^post12, n^0'=n^post12, c^0'=c^post12, s^0'=s^post12, f^0'=f^post12, (r^0-r^post12 == 0 /\ c^0-s^0+s^post12 == 0 /\ -1+d^post12 == 0 /\ -f^post12+f^0 == 0 /\ -n^post12+n^0 == 0 /\ -c^post12+c^0 == 0), cost: 1
  13: l11 -> l10 : r^0'=r^post13, d^0'=d^post13, n^0'=n^post13, c^0'=c^post13, s^0'=s^post13, f^0'=f^post13, (r^0-r^post13 == 0 /\ d^0-d^post13 == 0 /\ -n^post13+n^0 == 0 /\ -f^post13+f^0 == 0 /\ -c^post13+c^0 == 0 /\ 1-f^0 <= 0 /\ s^0-s^post13 == 0), cost: 1
  14: l11 -> l10 : r^0'=r^post14, d^0'=d^post14, n^0'=n^post14, c^0'=c^post14, s^0'=s^post14, f^0'=f^post14, (d^0-d^post14 == 0 /\ r^0-r^post14 == 0 /\ -n^post14+n^0 == 0 /\ s^0-s^post14 == 0 /\ f^0-f^post14 == 0 /\ 1+f^0 <= 0 /\ -c^post14+c^0 == 0), cost: 1
  15: l11 -> l10 : r^0'=r^post15, d^0'=d^post15, n^0'=n^post15, c^0'=c^post15, s^0'=s^post15, f^0'=f^post15, (-f^0 <= 0 /\ 1+c^post15-c^0 == 0 /\ -1+f^post15 == 0 /\ -s^post15+s^0 == 0 /\ f^0 <= 0 /\ d^0-d^post15 == 0 /\ r^0-r^post15 == 0 /\ n^0-n^post15 == 0), cost: 1
  17: l12 -> l10 : r^0'=r^post17, d^0'=d^post17, n^0'=n^post17, c^0'=c^post17, s^0'=s^post17, f^0'=f^post17, (-f^post17+f^0 == 0 /\ -s^post17+s^0 == 0 /\ r^0-r^post17 == 0 /\ -n^post17+n^0 == 0 /\ c^0-c^post17 == 0 /\ d^0-d^post17 == 0 /\ 3-d^0 <= 0), cost: 1
  18: l12 -> l10 : r^0'=r^post18, d^0'=d^post18, n^0'=n^post18, c^0'=c^post18, s^0'=s^post18, f^0'=f^post18, (r^0-r^post18 == 0 /\ d^0-d^post18 == 0 /\ -1+d^0 <= 0 /\ s^0-s^post18 == 0 /\ -n^post18+n^0 == 0 /\ -c^post18+c^0 == 0 /\ -f^post18+f^0 == 0), cost: 1
  19: l12 -> l11 : r^0'=r^post19, d^0'=d^post19, n^0'=n^post19, c^0'=c^post19, s^0'=s^post19, f^0'=f^post19, (r^0-r^post19 == 0 /\ -c^post19+c^0 == 0 /\ -2+d^0 <= 0 /\ -n^post19+n^0 == 0 /\ d^0-d^post19 == 0 /\ s^0-s^post19 == 0 /\ 2-d^0 <= 0 /\ -f^post19+f^0 == 0), cost: 1
  22: l13 -> l9 : r^0'=r^post22, d^0'=d^post22, n^0'=n^post22, c^0'=c^post22, s^0'=s^post22, f^0'=f^post22, (-f^post22+f^0 == 0 /\ d^0-d^post22 == 0 /\ c^0-c^post22 == 0 /\ r^0-r^post22 == 0 /\ n^0-n^post22 == 0 /\ -255+s^0 <= 0 /\ -s^post22+s^0 == 0), cost: 1
  23: l13 -> l6 : r^0'=r^post23, d^0'=d^post23, n^0'=n^post23, c^0'=c^post23, s^0'=s^post23, f^0'=f^post23, (-s^post23+s^0 == 0 /\ c^0-c^post23 == 0 /\ n^0-n^post23 == 0 /\ 256-s^0 <= 0 /\ -f^post23+f^0 == 0 /\ -d^post23+d^0 == 0 /\ r^0-r^post23 == 0), cost: 1
  24: l14 -> l13 : r^0'=r^post24, d^0'=d^post24, n^0'=n^post24, c^0'=c^post24, s^0'=s^post24, f^0'=f^post24, (-2+d^post24 == 0 /\ -c^0-s^0+s^post24 == 0 /\ -n^post24+n^0 == 0 /\ -f^post24+f^0 == 0 /\ r^0-r^post24 == 0 /\ c^0-c^post24 == 0), cost: 1
  25: l15 -> l14 : r^0'=r^post25, d^0'=d^post25, n^0'=n^post25, c^0'=c^post25, s^0'=s^post25, f^0'=f^post25, (-n^post25+n^0 == 0 /\ -f^post25+f^0 == 0 /\ 1-f^0 <= 0 /\ r^0-r^post25 == 0 /\ d^0-d^post25 == 0 /\ s^0-s^post25 == 0 /\ c^0-c^post25 == 0), cost: 1
  26: l15 -> l14 : r^0'=r^post26, d^0'=d^post26, n^0'=n^post26, c^0'=c^post26, s^0'=s^post26, f^0'=f^post26, (-f^post26+f^0 == 0 /\ -c^post26+c^0 == 0 /\ d^0-d^post26 == 0 /\ r^0-r^post26 == 0 /\ s^0-s^post26 == 0 /\ 1+f^0 <= 0 /\ -n^post26+n^0 == 0), cost: 1
  27: l15 -> l14 : r^0'=r^post27, d^0'=d^post27, n^0'=n^post27, c^0'=c^post27, s^0'=s^post27, f^0'=f^post27, (-n^post27+n^0 == 0 /\ -f^0 <= 0 /\ -1+f^post27 == 0 /\ -s^post27+s^0 == 0 /\ d^0-d^post27 == 0 /\ f^0 <= 0 /\ 1+c^post27-c^0 == 0 /\ r^0-r^post27 == 0), cost: 1
  31: l16 -> l9 : r^0'=r^post31, d^0'=d^post31, n^0'=n^post31, c^0'=c^post31, s^0'=s^post31, f^0'=f^post31, (d^post31 == 0 /\ f^post31 == 0 /\ -s^post31+s^0 == 0 /\ r^0-r^post31 == 0 /\ n^0-n^post31 == 0 /\ -4+c^post31 == 0), cost: 1
  32: l17 -> l16 : r^0'=r^post32, d^0'=d^post32, n^0'=n^post32, c^0'=c^post32, s^0'=s^post32, f^0'=f^post32, (-n^post32+n^0 == 0 /\ d^0-d^post32 == 0 /\ r^0-r^post32 == 0 /\ c^0-c^post32 == 0 /\ -f^post32+f^0 == 0 /\ s^0-s^post32 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l17
   0: l0 -> l1 : r^0'=r^post0, d^0'=d^post0, n^0'=n^post0, c^0'=c^post0, s^0'=s^post0, f^0'=f^post0, (-r^0+n^0 <= 0 /\ d^0-d^post0 == 0 /\ -n^post0+n^0 == 0 /\ -c^post0+c^0 == 0 /\ -f^post0+f^0 == 0 /\ s^0-s^post0 == 0 /\ r^0-r^post0 == 0), cost: 1
   1: l0 -> l2 : r^0'=r^post1, d^0'=d^post1, n^0'=n^post1, c^0'=c^post1, s^0'=s^post1, f^0'=f^post1, (-s^post1+s^0 == 0 /\ -c^post1+c^0 == 0 /\ -f^post1+f^0 == 0 /\ 1+r^0-n^0 <= 0 /\ r^0-r^post1 == 0 /\ n^0-n^post1 == 0 /\ d^0-d^post1 == 0), cost: 1
  21: l1 -> l12 : r^0'=r^post21, d^0'=d^post21, n^0'=n^post21, c^0'=c^post21, s^0'=s^post21, f^0'=f^post21, (f^0-f^post21 == 0 /\ 1-r^0+n^0 <= 0 /\ -c^post21+c^0 == 0 /\ -s^post21+s^0 == 0 /\ d^0-d^post21 == 0 /\ r^0-r^post21 == 0 /\ n^0-n^post21 == 0), cost: 1
  28: l2 -> l14 : r^0'=r^post28, d^0'=d^post28, n^0'=n^post28, c^0'=c^post28, s^0'=s^post28, f^0'=f^post28, (-s^post28+s^0 == 0 /\ -f^post28+f^0 == 0 /\ -c^post28+c^0 == 0 /\ d^0-d^post28 == 0 /\ n^0-n^post28 == 0 /\ -r^post28+r^0 == 0 /\ 2-d^0 <= 0), cost: 1
  29: l2 -> l14 : r^0'=r^post29, d^0'=d^post29, n^0'=n^post29, c^0'=c^post29, s^0'=s^post29, f^0'=f^post29, (-f^post29+f^0 == 0 /\ r^0-r^post29 == 0 /\ d^0 <= 0 /\ c^0-c^post29 == 0 /\ n^0-n^post29 == 0 /\ d^0-d^post29 == 0 /\ -s^post29+s^0 == 0), cost: 1
  30: l2 -> l15 : r^0'=r^post30, d^0'=d^post30, n^0'=n^post30, c^0'=c^post30, s^0'=s^post30, f^0'=f^post30, (r^0-r^post30 == 0 /\ -d^post30+d^0 == 0 /\ n^0-n^post30 == 0 /\ -f^post30+f^0 == 0 /\ -s^post30+s^0 == 0 /\ c^0-c^post30 == 0 /\ 1-d^0 <= 0 /\ -1+d^0 <= 0), cost: 1
   2: l3 -> l0 : r^0'=r^post2, d^0'=d^post2, n^0'=n^post2, c^0'=c^post2, s^0'=s^post2, f^0'=f^post2, (1-c^0+c^post2 == 0 /\ -f^post2+f^0 == 0 /\ d^0-d^post2 == 0 /\ r^0-r^post2 == 0 /\ n^0-n^post2 == 0 /\ -s^post2+s^0 == 0), cost: 1
   3: l4 -> l0 : r^0'=r^post3, d^0'=d^post3, n^0'=n^post3, c^0'=c^post3, s^0'=s^post3, f^0'=f^post3, (c^0-c^post3 == 0 /\ -f^post3+f^0 == 0 /\ n^0-n^post3 == 0 /\ -f^0 <= 0 /\ d^0-d^post3 == 0 /\ r^0-r^post3 == 0 /\ -s^post3+s^0 == 0 /\ f^0 <= 0), cost: 1
   4: l4 -> l3 : r^0'=r^post4, d^0'=d^post4, n^0'=n^post4, c^0'=c^post4, s^0'=s^post4, f^0'=f^post4, (n^0-n^post4 == 0 /\ c^0-c^post4 == 0 /\ 1-f^0 <= 0 /\ -d^post4+d^0 == 0 /\ r^0-r^post4 == 0 /\ -f^post4+f^0 == 0 /\ -s^post4+s^0 == 0), cost: 1
   5: l4 -> l3 : r^0'=r^post5, d^0'=d^post5, n^0'=n^post5, c^0'=c^post5, s^0'=s^post5, f^0'=f^post5, (-f^post5+f^0 == 0 /\ -n^post5+n^0 == 0 /\ r^0-r^post5 == 0 /\ 1+f^0 <= 0 /\ c^0-c^post5 == 0 /\ s^0-s^post5 == 0 /\ d^0-d^post5 == 0), cost: 1
   6: l5 -> l4 : r^0'=r^post6, d^0'=d^post6, n^0'=n^post6, c^0'=c^post6, s^0'=s^post6, f^0'=f^post6, (r^0-r^post6 == 0 /\ -f^post6+f^0 == 0 /\ -n^post6+n^0 == 0 /\ s^0-s^post6 == 0 /\ -c^post6+c^0 == 0 /\ d^0-d^post6 == 0 /\ 2-c^0 <= 0), cost: 1
   7: l5 -> l4 : r^0'=r^post7, d^0'=d^post7, n^0'=n^post7, c^0'=c^post7, s^0'=s^post7, f^0'=f^post7, (f^0-f^post7 == 0 /\ c^0 <= 0 /\ -s^post7+s^0 == 0 /\ r^0-r^post7 == 0 /\ n^0-n^post7 == 0 /\ d^0-d^post7 == 0 /\ -c^post7+c^0 == 0), cost: 1
  10: l8 -> l9 : r^0'=r^post10, d^0'=d^post10, n^0'=n^post10, c^0'=c^post10, s^0'=s^post10, f^0'=f^post10, (r^0-r^post10 == 0 /\ -d^post10+d^0 == 0 /\ n^0-n^post10 == 0 /\ c^0-c^post10 == 0 /\ -f^post10+f^0 == 0 /\ -s^post10+s^0 == 0 /\ -s^0 <= 0), cost: 1
  16: l9 -> l5 : r^0'=r^post16, d^0'=d^post16, n^0'=n^post16, c^0'=c^post16, s^0'=s^post16, f^0'=f^post16, (0 == 0 /\ r^0-r^post16 == 0 /\ -d^post16+d^0 == 0 /\ -c^post16+c^0 == 0 /\ -f^post16+f^0 == 0 /\ -s^post16+s^0 == 0), cost: 1
  12: l10 -> l8 : r^0'=r^post12, d^0'=d^post12, n^0'=n^post12, c^0'=c^post12, s^0'=s^post12, f^0'=f^post12, (r^0-r^post12 == 0 /\ c^0-s^0+s^post12 == 0 /\ -1+d^post12 == 0 /\ -f^post12+f^0 == 0 /\ -n^post12+n^0 == 0 /\ -c^post12+c^0 == 0), cost: 1
  13: l11 -> l10 : r^0'=r^post13, d^0'=d^post13, n^0'=n^post13, c^0'=c^post13, s^0'=s^post13, f^0'=f^post13, (r^0-r^post13 == 0 /\ d^0-d^post13 == 0 /\ -n^post13+n^0 == 0 /\ -f^post13+f^0 == 0 /\ -c^post13+c^0 == 0 /\ 1-f^0 <= 0 /\ s^0-s^post13 == 0), cost: 1
  14: l11 -> l10 : r^0'=r^post14, d^0'=d^post14, n^0'=n^post14, c^0'=c^post14, s^0'=s^post14, f^0'=f^post14, (d^0-d^post14 == 0 /\ r^0-r^post14 == 0 /\ -n^post14+n^0 == 0 /\ s^0-s^post14 == 0 /\ f^0-f^post14 == 0 /\ 1+f^0 <= 0 /\ -c^post14+c^0 == 0), cost: 1
  15: l11 -> l10 : r^0'=r^post15, d^0'=d^post15, n^0'=n^post15, c^0'=c^post15, s^0'=s^post15, f^0'=f^post15, (-f^0 <= 0 /\ 1+c^post15-c^0 == 0 /\ -1+f^post15 == 0 /\ -s^post15+s^0 == 0 /\ f^0 <= 0 /\ d^0-d^post15 == 0 /\ r^0-r^post15 == 0 /\ n^0-n^post15 == 0), cost: 1
  17: l12 -> l10 : r^0'=r^post17, d^0'=d^post17, n^0'=n^post17, c^0'=c^post17, s^0'=s^post17, f^0'=f^post17, (-f^post17+f^0 == 0 /\ -s^post17+s^0 == 0 /\ r^0-r^post17 == 0 /\ -n^post17+n^0 == 0 /\ c^0-c^post17 == 0 /\ d^0-d^post17 == 0 /\ 3-d^0 <= 0), cost: 1
  18: l12 -> l10 : r^0'=r^post18, d^0'=d^post18, n^0'=n^post18, c^0'=c^post18, s^0'=s^post18, f^0'=f^post18, (r^0-r^post18 == 0 /\ d^0-d^post18 == 0 /\ -1+d^0 <= 0 /\ s^0-s^post18 == 0 /\ -n^post18+n^0 == 0 /\ -c^post18+c^0 == 0 /\ -f^post18+f^0 == 0), cost: 1
  19: l12 -> l11 : r^0'=r^post19, d^0'=d^post19, n^0'=n^post19, c^0'=c^post19, s^0'=s^post19, f^0'=f^post19, (r^0-r^post19 == 0 /\ -c^post19+c^0 == 0 /\ -2+d^0 <= 0 /\ -n^post19+n^0 == 0 /\ d^0-d^post19 == 0 /\ s^0-s^post19 == 0 /\ 2-d^0 <= 0 /\ -f^post19+f^0 == 0), cost: 1
  22: l13 -> l9 : r^0'=r^post22, d^0'=d^post22, n^0'=n^post22, c^0'=c^post22, s^0'=s^post22, f^0'=f^post22, (-f^post22+f^0 == 0 /\ d^0-d^post22 == 0 /\ c^0-c^post22 == 0 /\ r^0-r^post22 == 0 /\ n^0-n^post22 == 0 /\ -255+s^0 <= 0 /\ -s^post22+s^0 == 0), cost: 1
  24: l14 -> l13 : r^0'=r^post24, d^0'=d^post24, n^0'=n^post24, c^0'=c^post24, s^0'=s^post24, f^0'=f^post24, (-2+d^post24 == 0 /\ -c^0-s^0+s^post24 == 0 /\ -n^post24+n^0 == 0 /\ -f^post24+f^0 == 0 /\ r^0-r^post24 == 0 /\ c^0-c^post24 == 0), cost: 1
  25: l15 -> l14 : r^0'=r^post25, d^0'=d^post25, n^0'=n^post25, c^0'=c^post25, s^0'=s^post25, f^0'=f^post25, (-n^post25+n^0 == 0 /\ -f^post25+f^0 == 0 /\ 1-f^0 <= 0 /\ r^0-r^post25 == 0 /\ d^0-d^post25 == 0 /\ s^0-s^post25 == 0 /\ c^0-c^post25 == 0), cost: 1
  26: l15 -> l14 : r^0'=r^post26, d^0'=d^post26, n^0'=n^post26, c^0'=c^post26, s^0'=s^post26, f^0'=f^post26, (-f^post26+f^0 == 0 /\ -c^post26+c^0 == 0 /\ d^0-d^post26 == 0 /\ r^0-r^post26 == 0 /\ s^0-s^post26 == 0 /\ 1+f^0 <= 0 /\ -n^post26+n^0 == 0), cost: 1
  27: l15 -> l14 : r^0'=r^post27, d^0'=d^post27, n^0'=n^post27, c^0'=c^post27, s^0'=s^post27, f^0'=f^post27, (-n^post27+n^0 == 0 /\ -f^0 <= 0 /\ -1+f^post27 == 0 /\ -s^post27+s^0 == 0 /\ d^0-d^post27 == 0 /\ f^0 <= 0 /\ 1+c^post27-c^0 == 0 /\ r^0-r^post27 == 0), cost: 1
  31: l16 -> l9 : r^0'=r^post31, d^0'=d^post31, n^0'=n^post31, c^0'=c^post31, s^0'=s^post31, f^0'=f^post31, (d^post31 == 0 /\ f^post31 == 0 /\ -s^post31+s^0 == 0 /\ r^0-r^post31 == 0 /\ n^0-n^post31 == 0 /\ -4+c^post31 == 0), cost: 1
  32: l17 -> l16 : r^0'=r^post32, d^0'=d^post32, n^0'=n^post32, c^0'=c^post32, s^0'=s^post32, f^0'=f^post32, (-n^post32+n^0 == 0 /\ d^0-d^post32 == 0 /\ r^0-r^post32 == 0 /\ c^0-c^post32 == 0 /\ -f^post32+f^0 == 0 /\ s^0-s^post32 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : r^0'=r^post0, d^0'=d^post0, n^0'=n^post0, c^0'=c^post0, s^0'=s^post0, f^0'=f^post0, (-r^0+n^0 <= 0 /\ d^0-d^post0 == 0 /\ -n^post0+n^0 == 0 /\ -c^post0+c^0 == 0 /\ -f^post0+f^0 == 0 /\ s^0-s^post0 == 0 /\ r^0-r^post0 == 0), cost: 1
New rule:
l0 -> l1 : -r^0+n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l0 -> l2 : r^0'=r^post1, d^0'=d^post1, n^0'=n^post1, c^0'=c^post1, s^0'=s^post1, f^0'=f^post1, (-s^post1+s^0 == 0 /\ -c^post1+c^0 == 0 /\ -f^post1+f^0 == 0 /\ 1+r^0-n^0 <= 0 /\ r^0-r^post1 == 0 /\ n^0-n^post1 == 0 /\ d^0-d^post1 == 0), cost: 1
New rule:
l0 -> l2 : 1+r^0-n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l0 : r^0'=r^post2, d^0'=d^post2, n^0'=n^post2, c^0'=c^post2, s^0'=s^post2, f^0'=f^post2, (1-c^0+c^post2 == 0 /\ -f^post2+f^0 == 0 /\ d^0-d^post2 == 0 /\ r^0-r^post2 == 0 /\ n^0-n^post2 == 0 /\ -s^post2+s^0 == 0), cost: 1
New rule:
l3 -> l0 : c^0'=-1+c^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l4 -> l0 : r^0'=r^post3, d^0'=d^post3, n^0'=n^post3, c^0'=c^post3, s^0'=s^post3, f^0'=f^post3, (c^0-c^post3 == 0 /\ -f^post3+f^0 == 0 /\ n^0-n^post3 == 0 /\ -f^0 <= 0 /\ d^0-d^post3 == 0 /\ r^0-r^post3 == 0 /\ -s^post3+s^0 == 0 /\ f^0 <= 0), cost: 1
New rule:
l4 -> l0 : f^0 == 0, cost: 1

Applied preprocessing
Original rule:
l4 -> l3 : r^0'=r^post4, d^0'=d^post4, n^0'=n^post4, c^0'=c^post4, s^0'=s^post4, f^0'=f^post4, (n^0-n^post4 == 0 /\ c^0-c^post4 == 0 /\ 1-f^0 <= 0 /\ -d^post4+d^0 == 0 /\ r^0-r^post4 == 0 /\ -f^post4+f^0 == 0 /\ -s^post4+s^0 == 0), cost: 1
New rule:
l4 -> l3 : -1+f^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l4 -> l3 : r^0'=r^post5, d^0'=d^post5, n^0'=n^post5, c^0'=c^post5, s^0'=s^post5, f^0'=f^post5, (-f^post5+f^0 == 0 /\ -n^post5+n^0 == 0 /\ r^0-r^post5 == 0 /\ 1+f^0 <= 0 /\ c^0-c^post5 == 0 /\ s^0-s^post5 == 0 /\ d^0-d^post5 == 0), cost: 1
New rule:
l4 -> l3 : 1+f^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l4 : r^0'=r^post6, d^0'=d^post6, n^0'=n^post6, c^0'=c^post6, s^0'=s^post6, f^0'=f^post6, (r^0-r^post6 == 0 /\ -f^post6+f^0 == 0 /\ -n^post6+n^0 == 0 /\ s^0-s^post6 == 0 /\ -c^post6+c^0 == 0 /\ d^0-d^post6 == 0 /\ 2-c^0 <= 0), cost: 1
New rule:
l5 -> l4 : -2+c^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l4 : r^0'=r^post7, d^0'=d^post7, n^0'=n^post7, c^0'=c^post7, s^0'=s^post7, f^0'=f^post7, (f^0-f^post7 == 0 /\ c^0 <= 0 /\ -s^post7+s^0 == 0 /\ r^0-r^post7 == 0 /\ n^0-n^post7 == 0 /\ d^0-d^post7 == 0 /\ -c^post7+c^0 == 0), cost: 1
New rule:
l5 -> l4 : c^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l9 : r^0'=r^post10, d^0'=d^post10, n^0'=n^post10, c^0'=c^post10, s^0'=s^post10, f^0'=f^post10, (r^0-r^post10 == 0 /\ -d^post10+d^0 == 0 /\ n^0-n^post10 == 0 /\ c^0-c^post10 == 0 /\ -f^post10+f^0 == 0 /\ -s^post10+s^0 == 0 /\ -s^0 <= 0), cost: 1
New rule:
l8 -> l9 : s^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l10 -> l8 : r^0'=r^post12, d^0'=d^post12, n^0'=n^post12, c^0'=c^post12, s^0'=s^post12, f^0'=f^post12, (r^0-r^post12 == 0 /\ c^0-s^0+s^post12 == 0 /\ -1+d^post12 == 0 /\ -f^post12+f^0 == 0 /\ -n^post12+n^0 == 0 /\ -c^post12+c^0 == 0), cost: 1
New rule:
l10 -> l8 : d^0'=1, s^0'=-c^0+s^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l11 -> l10 : r^0'=r^post13, d^0'=d^post13, n^0'=n^post13, c^0'=c^post13, s^0'=s^post13, f^0'=f^post13, (r^0-r^post13 == 0 /\ d^0-d^post13 == 0 /\ -n^post13+n^0 == 0 /\ -f^post13+f^0 == 0 /\ -c^post13+c^0 == 0 /\ 1-f^0 <= 0 /\ s^0-s^post13 == 0), cost: 1
New rule:
l11 -> l10 : -1+f^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l11 -> l10 : r^0'=r^post14, d^0'=d^post14, n^0'=n^post14, c^0'=c^post14, s^0'=s^post14, f^0'=f^post14, (d^0-d^post14 == 0 /\ r^0-r^post14 == 0 /\ -n^post14+n^0 == 0 /\ s^0-s^post14 == 0 /\ f^0-f^post14 == 0 /\ 1+f^0 <= 0 /\ -c^post14+c^0 == 0), cost: 1
New rule:
l11 -> l10 : 1+f^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l11 -> l10 : r^0'=r^post15, d^0'=d^post15, n^0'=n^post15, c^0'=c^post15, s^0'=s^post15, f^0'=f^post15, (-f^0 <= 0 /\ 1+c^post15-c^0 == 0 /\ -1+f^post15 == 0 /\ -s^post15+s^0 == 0 /\ f^0 <= 0 /\ d^0-d^post15 == 0 /\ r^0-r^post15 == 0 /\ n^0-n^post15 == 0), cost: 1
New rule:
l11 -> l10 : c^0'=-1+c^0, f^0'=1, f^0 == 0, cost: 1

Applied preprocessing
Original rule:
l9 -> l5 : r^0'=r^post16, d^0'=d^post16, n^0'=n^post16, c^0'=c^post16, s^0'=s^post16, f^0'=f^post16, (0 == 0 /\ r^0-r^post16 == 0 /\ -d^post16+d^0 == 0 /\ -c^post16+c^0 == 0 /\ -f^post16+f^0 == 0 /\ -s^post16+s^0 == 0), cost: 1
New rule:
l9 -> l5 : n^0'=n^post16, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l12 -> l10 : r^0'=r^post17, d^0'=d^post17, n^0'=n^post17, c^0'=c^post17, s^0'=s^post17, f^0'=f^post17, (-f^post17+f^0 == 0 /\ -s^post17+s^0 == 0 /\ r^0-r^post17 == 0 /\ -n^post17+n^0 == 0 /\ c^0-c^post17 == 0 /\ d^0-d^post17 == 0 /\ 3-d^0 <= 0), cost: 1
New rule:
l12 -> l10 : -3+d^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l12 -> l10 : r^0'=r^post18, d^0'=d^post18, n^0'=n^post18, c^0'=c^post18, s^0'=s^post18, f^0'=f^post18, (r^0-r^post18 == 0 /\ d^0-d^post18 == 0 /\ -1+d^0 <= 0 /\ s^0-s^post18 == 0 /\ -n^post18+n^0 == 0 /\ -c^post18+c^0 == 0 /\ -f^post18+f^0 == 0), cost: 1
New rule:
l12 -> l10 : -1+d^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l12 -> l11 : r^0'=r^post19, d^0'=d^post19, n^0'=n^post19, c^0'=c^post19, s^0'=s^post19, f^0'=f^post19, (r^0-r^post19 == 0 /\ -c^post19+c^0 == 0 /\ -2+d^0 <= 0 /\ -n^post19+n^0 == 0 /\ d^0-d^post19 == 0 /\ s^0-s^post19 == 0 /\ 2-d^0 <= 0 /\ -f^post19+f^0 == 0), cost: 1
New rule:
l12 -> l11 : -2+d^0 == 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l12 : r^0'=r^post21, d^0'=d^post21, n^0'=n^post21, c^0'=c^post21, s^0'=s^post21, f^0'=f^post21, (f^0-f^post21 == 0 /\ 1-r^0+n^0 <= 0 /\ -c^post21+c^0 == 0 /\ -s^post21+s^0 == 0 /\ d^0-d^post21 == 0 /\ r^0-r^post21 == 0 /\ n^0-n^post21 == 0), cost: 1
New rule:
l1 -> l12 : 1-r^0+n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l9 : r^0'=r^post22, d^0'=d^post22, n^0'=n^post22, c^0'=c^post22, s^0'=s^post22, f^0'=f^post22, (-f^post22+f^0 == 0 /\ d^0-d^post22 == 0 /\ c^0-c^post22 == 0 /\ r^0-r^post22 == 0 /\ n^0-n^post22 == 0 /\ -255+s^0 <= 0 /\ -s^post22+s^0 == 0), cost: 1
New rule:
l13 -> l9 : -255+s^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l14 -> l13 : r^0'=r^post24, d^0'=d^post24, n^0'=n^post24, c^0'=c^post24, s^0'=s^post24, f^0'=f^post24, (-2+d^post24 == 0 /\ -c^0-s^0+s^post24 == 0 /\ -n^post24+n^0 == 0 /\ -f^post24+f^0 == 0 /\ r^0-r^post24 == 0 /\ c^0-c^post24 == 0), cost: 1
New rule:
l14 -> l13 : d^0'=2, s^0'=c^0+s^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l15 -> l14 : r^0'=r^post25, d^0'=d^post25, n^0'=n^post25, c^0'=c^post25, s^0'=s^post25, f^0'=f^post25, (-n^post25+n^0 == 0 /\ -f^post25+f^0 == 0 /\ 1-f^0 <= 0 /\ r^0-r^post25 == 0 /\ d^0-d^post25 == 0 /\ s^0-s^post25 == 0 /\ c^0-c^post25 == 0), cost: 1
New rule:
l15 -> l14 : -1+f^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l15 -> l14 : r^0'=r^post26, d^0'=d^post26, n^0'=n^post26, c^0'=c^post26, s^0'=s^post26, f^0'=f^post26, (-f^post26+f^0 == 0 /\ -c^post26+c^0 == 0 /\ d^0-d^post26 == 0 /\ r^0-r^post26 == 0 /\ s^0-s^post26 == 0 /\ 1+f^0 <= 0 /\ -n^post26+n^0 == 0), cost: 1
New rule:
l15 -> l14 : 1+f^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l15 -> l14 : r^0'=r^post27, d^0'=d^post27, n^0'=n^post27, c^0'=c^post27, s^0'=s^post27, f^0'=f^post27, (-n^post27+n^0 == 0 /\ -f^0 <= 0 /\ -1+f^post27 == 0 /\ -s^post27+s^0 == 0 /\ d^0-d^post27 == 0 /\ f^0 <= 0 /\ 1+c^post27-c^0 == 0 /\ r^0-r^post27 == 0), cost: 1
New rule:
l15 -> l14 : c^0'=-1+c^0, f^0'=1, f^0 == 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l14 : r^0'=r^post28, d^0'=d^post28, n^0'=n^post28, c^0'=c^post28, s^0'=s^post28, f^0'=f^post28, (-s^post28+s^0 == 0 /\ -f^post28+f^0 == 0 /\ -c^post28+c^0 == 0 /\ d^0-d^post28 == 0 /\ n^0-n^post28 == 0 /\ -r^post28+r^0 == 0 /\ 2-d^0 <= 0), cost: 1
New rule:
l2 -> l14 : -2+d^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l14 : r^0'=r^post29, d^0'=d^post29, n^0'=n^post29, c^0'=c^post29, s^0'=s^post29, f^0'=f^post29, (-f^post29+f^0 == 0 /\ r^0-r^post29 == 0 /\ d^0 <= 0 /\ c^0-c^post29 == 0 /\ n^0-n^post29 == 0 /\ d^0-d^post29 == 0 /\ -s^post29+s^0 == 0), cost: 1
New rule:
l2 -> l14 : d^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l15 : r^0'=r^post30, d^0'=d^post30, n^0'=n^post30, c^0'=c^post30, s^0'=s^post30, f^0'=f^post30, (r^0-r^post30 == 0 /\ -d^post30+d^0 == 0 /\ n^0-n^post30 == 0 /\ -f^post30+f^0 == 0 /\ -s^post30+s^0 == 0 /\ c^0-c^post30 == 0 /\ 1-d^0 <= 0 /\ -1+d^0 <= 0), cost: 1
New rule:
l2 -> l15 : -1+d^0 == 0, cost: 1

Applied preprocessing
Original rule:
l16 -> l9 : r^0'=r^post31, d^0'=d^post31, n^0'=n^post31, c^0'=c^post31, s^0'=s^post31, f^0'=f^post31, (d^post31 == 0 /\ f^post31 == 0 /\ -s^post31+s^0 == 0 /\ r^0-r^post31 == 0 /\ n^0-n^post31 == 0 /\ -4+c^post31 == 0), cost: 1
New rule:
l16 -> l9 : d^0'=0, c^0'=4, f^0'=0, TRUE, cost: 1

Applied preprocessing
Original rule:
l17 -> l16 : r^0'=r^post32, d^0'=d^post32, n^0'=n^post32, c^0'=c^post32, s^0'=s^post32, f^0'=f^post32, (-n^post32+n^0 == 0 /\ d^0-d^post32 == 0 /\ r^0-r^post32 == 0 /\ c^0-c^post32 == 0 /\ -f^post32+f^0 == 0 /\ s^0-s^post32 == 0), cost: 1
New rule:
l17 -> l16 : TRUE, cost: 1

Simplified rules
Start location: l17
  33: l0 -> l1 : -r^0+n^0 <= 0, cost: 1
  34: l0 -> l2 : 1+r^0-n^0 <= 0, cost: 1
  50: l1 -> l12 : 1-r^0+n^0 <= 0, cost: 1
  56: l2 -> l14 : -2+d^0 >= 0, cost: 1
  57: l2 -> l14 : d^0 <= 0, cost: 1
  58: l2 -> l15 : -1+d^0 == 0, cost: 1
  35: l3 -> l0 : c^0'=-1+c^0, TRUE, cost: 1
  36: l4 -> l0 : f^0 == 0, cost: 1
  37: l4 -> l3 : -1+f^0 >= 0, cost: 1
  38: l4 -> l3 : 1+f^0 <= 0, cost: 1
  39: l5 -> l4 : -2+c^0 >= 0, cost: 1
  40: l5 -> l4 : c^0 <= 0, cost: 1
  41: l8 -> l9 : s^0 >= 0, cost: 1
  46: l9 -> l5 : n^0'=n^post16, 0 == 0, cost: 1
  42: l10 -> l8 : d^0'=1, s^0'=-c^0+s^0, TRUE, cost: 1
  43: l11 -> l10 : -1+f^0 >= 0, cost: 1
  44: l11 -> l10 : 1+f^0 <= 0, cost: 1
  45: l11 -> l10 : c^0'=-1+c^0, f^0'=1, f^0 == 0, cost: 1
  47: l12 -> l10 : -3+d^0 >= 0, cost: 1
  48: l12 -> l10 : -1+d^0 <= 0, cost: 1
  49: l12 -> l11 : -2+d^0 == 0, cost: 1
  51: l13 -> l9 : -255+s^0 <= 0, cost: 1
  52: l14 -> l13 : d^0'=2, s^0'=c^0+s^0, TRUE, cost: 1
  53: l15 -> l14 : -1+f^0 >= 0, cost: 1
  54: l15 -> l14 : 1+f^0 <= 0, cost: 1
  55: l15 -> l14 : c^0'=-1+c^0, f^0'=1, f^0 == 0, cost: 1
  59: l16 -> l9 : d^0'=0, c^0'=4, f^0'=0, TRUE, cost: 1
  60: l17 -> l16 : TRUE, cost: 1


Eliminating location l16 by chaining:

Applied chaining
First rule:
l17 -> l16 : TRUE, cost: 1
Second rule:
l16 -> l9 : d^0'=0, c^0'=4, f^0'=0, TRUE, cost: 1
New rule:
l17 -> l9 : d^0'=0, c^0'=4, f^0'=0, TRUE, cost: 2

Applied deletion
Removed the following rules: 59 60

Eliminating location l1 by chaining:

Applied chaining
First rule:
l0 -> l1 : -r^0+n^0 <= 0, cost: 1
Second rule:
l1 -> l12 : 1-r^0+n^0 <= 0, cost: 1
New rule:
l0 -> l12 : (1-r^0+n^0 <= 0 /\ -r^0+n^0 <= 0), cost: 2

Applied simplification
Original rule:
l0 -> l12 : (1-r^0+n^0 <= 0 /\ -r^0+n^0 <= 0), cost: 2
New rule:
l0 -> l12 : 1-r^0+n^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 33 50

Eliminating location l13 by chaining:

Applied chaining
First rule:
l14 -> l13 : d^0'=2, s^0'=c^0+s^0, TRUE, cost: 1
Second rule:
l13 -> l9 : -255+s^0 <= 0, cost: 1
New rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 51 52

Eliminating location l8 by chaining:

Applied chaining
First rule:
l10 -> l8 : d^0'=1, s^0'=-c^0+s^0, TRUE, cost: 1
Second rule:
l8 -> l9 : s^0 >= 0, cost: 1
New rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2

Applied deletion
Removed the following rules: 41 42

Eliminated locations on linear paths
Start location: l17
  34: l0 -> l2 : 1+r^0-n^0 <= 0, cost: 1
  62: l0 -> l12 : 1-r^0+n^0 <= 0, cost: 2
  56: l2 -> l14 : -2+d^0 >= 0, cost: 1
  57: l2 -> l14 : d^0 <= 0, cost: 1
  58: l2 -> l15 : -1+d^0 == 0, cost: 1
  35: l3 -> l0 : c^0'=-1+c^0, TRUE, cost: 1
  36: l4 -> l0 : f^0 == 0, cost: 1
  37: l4 -> l3 : -1+f^0 >= 0, cost: 1
  38: l4 -> l3 : 1+f^0 <= 0, cost: 1
  39: l5 -> l4 : -2+c^0 >= 0, cost: 1
  40: l5 -> l4 : c^0 <= 0, cost: 1
  46: l9 -> l5 : n^0'=n^post16, 0 == 0, cost: 1
  64: l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
  43: l11 -> l10 : -1+f^0 >= 0, cost: 1
  44: l11 -> l10 : 1+f^0 <= 0, cost: 1
  45: l11 -> l10 : c^0'=-1+c^0, f^0'=1, f^0 == 0, cost: 1
  47: l12 -> l10 : -3+d^0 >= 0, cost: 1
  48: l12 -> l10 : -1+d^0 <= 0, cost: 1
  49: l12 -> l11 : -2+d^0 == 0, cost: 1
  63: l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
  53: l15 -> l14 : -1+f^0 >= 0, cost: 1
  54: l15 -> l14 : 1+f^0 <= 0, cost: 1
  55: l15 -> l14 : c^0'=-1+c^0, f^0'=1, f^0 == 0, cost: 1
  61: l17 -> l9 : d^0'=0, c^0'=4, f^0'=0, TRUE, cost: 2


Eliminating location l5 by chaining:

Applied chaining
First rule:
l9 -> l5 : n^0'=n^post16, 0 == 0, cost: 1
Second rule:
l5 -> l4 : -2+c^0 >= 0, cost: 1
New rule:
l9 -> l4 : n^0'=n^post16, (0 == 0 /\ -2+c^0 >= 0), cost: 2

Applied simplification
Original rule:
l9 -> l4 : n^0'=n^post16, (0 == 0 /\ -2+c^0 >= 0), cost: 2
New rule:
l9 -> l4 : n^0'=n^post16, -2+c^0 >= 0, cost: 2

Applied chaining
First rule:
l9 -> l5 : n^0'=n^post16, 0 == 0, cost: 1
Second rule:
l5 -> l4 : c^0 <= 0, cost: 1
New rule:
l9 -> l4 : n^0'=n^post16, (0 == 0 /\ c^0 <= 0), cost: 2

Applied simplification
Original rule:
l9 -> l4 : n^0'=n^post16, (0 == 0 /\ c^0 <= 0), cost: 2
New rule:
l9 -> l4 : n^0'=n^post16, c^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 39 40 46

Eliminating location l3 by chaining:

Applied chaining
First rule:
l4 -> l3 : -1+f^0 >= 0, cost: 1
Second rule:
l3 -> l0 : c^0'=-1+c^0, TRUE, cost: 1
New rule:
l4 -> l0 : c^0'=-1+c^0, -1+f^0 >= 0, cost: 2

Applied chaining
First rule:
l4 -> l3 : 1+f^0 <= 0, cost: 1
Second rule:
l3 -> l0 : c^0'=-1+c^0, TRUE, cost: 1
New rule:
l4 -> l0 : c^0'=-1+c^0, 1+f^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 35 37 38

Eliminating location l2 by chaining:

Applied chaining
First rule:
l0 -> l2 : 1+r^0-n^0 <= 0, cost: 1
Second rule:
l2 -> l14 : -2+d^0 >= 0, cost: 1
New rule:
l0 -> l14 : (-2+d^0 >= 0 /\ 1+r^0-n^0 <= 0), cost: 2

Applied chaining
First rule:
l0 -> l2 : 1+r^0-n^0 <= 0, cost: 1
Second rule:
l2 -> l14 : d^0 <= 0, cost: 1
New rule:
l0 -> l14 : (d^0 <= 0 /\ 1+r^0-n^0 <= 0), cost: 2

Applied chaining
First rule:
l0 -> l2 : 1+r^0-n^0 <= 0, cost: 1
Second rule:
l2 -> l15 : -1+d^0 == 0, cost: 1
New rule:
l0 -> l15 : (1+r^0-n^0 <= 0 /\ -1+d^0 == 0), cost: 2

Applied deletion
Removed the following rules: 34 56 57 58

Eliminating location l12 by chaining:

Applied chaining
First rule:
l0 -> l12 : 1-r^0+n^0 <= 0, cost: 2
Second rule:
l12 -> l10 : -3+d^0 >= 0, cost: 1
New rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -3+d^0 >= 0), cost: 3

Applied chaining
First rule:
l0 -> l12 : 1-r^0+n^0 <= 0, cost: 2
Second rule:
l12 -> l10 : -1+d^0 <= 0, cost: 1
New rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -1+d^0 <= 0), cost: 3

Applied chaining
First rule:
l0 -> l12 : 1-r^0+n^0 <= 0, cost: 2
Second rule:
l12 -> l11 : -2+d^0 == 0, cost: 1
New rule:
l0 -> l11 : (1-r^0+n^0 <= 0 /\ -2+d^0 == 0), cost: 3

Applied deletion
Removed the following rules: 47 48 49 62

Eliminated locations on tree-shaped paths
Start location: l17
  69: l0 -> l14 : (-2+d^0 >= 0 /\ 1+r^0-n^0 <= 0), cost: 2
  70: l0 -> l14 : (d^0 <= 0 /\ 1+r^0-n^0 <= 0), cost: 2
  71: l0 -> l15 : (1+r^0-n^0 <= 0 /\ -1+d^0 == 0), cost: 2
  72: l0 -> l10 : (1-r^0+n^0 <= 0 /\ -3+d^0 >= 0), cost: 3
  73: l0 -> l10 : (1-r^0+n^0 <= 0 /\ -1+d^0 <= 0), cost: 3
  74: l0 -> l11 : (1-r^0+n^0 <= 0 /\ -2+d^0 == 0), cost: 3
  36: l4 -> l0 : f^0 == 0, cost: 1
  67: l4 -> l0 : c^0'=-1+c^0, -1+f^0 >= 0, cost: 2
  68: l4 -> l0 : c^0'=-1+c^0, 1+f^0 <= 0, cost: 2
  65: l9 -> l4 : n^0'=n^post16, -2+c^0 >= 0, cost: 2
  66: l9 -> l4 : n^0'=n^post16, c^0 <= 0, cost: 2
  64: l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
  43: l11 -> l10 : -1+f^0 >= 0, cost: 1
  44: l11 -> l10 : 1+f^0 <= 0, cost: 1
  45: l11 -> l10 : c^0'=-1+c^0, f^0'=1, f^0 == 0, cost: 1
  63: l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
  53: l15 -> l14 : -1+f^0 >= 0, cost: 1
  54: l15 -> l14 : 1+f^0 <= 0, cost: 1
  55: l15 -> l14 : c^0'=-1+c^0, f^0'=1, f^0 == 0, cost: 1
  61: l17 -> l9 : d^0'=0, c^0'=4, f^0'=0, TRUE, cost: 2


Eliminating location l4 by chaining:

Applied chaining
First rule:
l9 -> l4 : n^0'=n^post16, -2+c^0 >= 0, cost: 2
Second rule:
l4 -> l0 : f^0 == 0, cost: 1
New rule:
l9 -> l0 : n^0'=n^post16, (-2+c^0 >= 0 /\ f^0 == 0), cost: 3

Applied chaining
First rule:
l9 -> l4 : n^0'=n^post16, -2+c^0 >= 0, cost: 2
Second rule:
l4 -> l0 : c^0'=-1+c^0, -1+f^0 >= 0, cost: 2
New rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0), cost: 4

Applied chaining
First rule:
l9 -> l4 : n^0'=n^post16, -2+c^0 >= 0, cost: 2
Second rule:
l4 -> l0 : c^0'=-1+c^0, 1+f^0 <= 0, cost: 2
New rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+f^0 <= 0), cost: 4

Applied chaining
First rule:
l9 -> l4 : n^0'=n^post16, c^0 <= 0, cost: 2
Second rule:
l4 -> l0 : f^0 == 0, cost: 1
New rule:
l9 -> l0 : n^0'=n^post16, (c^0 <= 0 /\ f^0 == 0), cost: 3

Applied chaining
First rule:
l9 -> l4 : n^0'=n^post16, c^0 <= 0, cost: 2
Second rule:
l4 -> l0 : c^0'=-1+c^0, -1+f^0 >= 0, cost: 2
New rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-1+f^0 >= 0 /\ c^0 <= 0), cost: 4

Applied chaining
First rule:
l9 -> l4 : n^0'=n^post16, c^0 <= 0, cost: 2
Second rule:
l4 -> l0 : c^0'=-1+c^0, 1+f^0 <= 0, cost: 2
New rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (c^0 <= 0 /\ 1+f^0 <= 0), cost: 4

Applied deletion
Removed the following rules: 36 65 66 67 68

Eliminating location l11 by chaining:

Applied chaining
First rule:
l0 -> l11 : (1-r^0+n^0 <= 0 /\ -2+d^0 == 0), cost: 3
Second rule:
l11 -> l10 : -1+f^0 >= 0, cost: 1
New rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -2+d^0 == 0 /\ -1+f^0 >= 0), cost: 4

Applied chaining
First rule:
l0 -> l11 : (1-r^0+n^0 <= 0 /\ -2+d^0 == 0), cost: 3
Second rule:
l11 -> l10 : 1+f^0 <= 0, cost: 1
New rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -2+d^0 == 0 /\ 1+f^0 <= 0), cost: 4

Applied chaining
First rule:
l0 -> l11 : (1-r^0+n^0 <= 0 /\ -2+d^0 == 0), cost: 3
Second rule:
l11 -> l10 : c^0'=-1+c^0, f^0'=1, f^0 == 0, cost: 1
New rule:
l0 -> l10 : c^0'=-1+c^0, f^0'=1, (1-r^0+n^0 <= 0 /\ -2+d^0 == 0 /\ f^0 == 0), cost: 4

Applied deletion
Removed the following rules: 43 44 45 74

Eliminating location l15 by chaining:

Applied chaining
First rule:
l0 -> l15 : (1+r^0-n^0 <= 0 /\ -1+d^0 == 0), cost: 2
Second rule:
l15 -> l14 : -1+f^0 >= 0, cost: 1
New rule:
l0 -> l14 : (1+r^0-n^0 <= 0 /\ -1+f^0 >= 0 /\ -1+d^0 == 0), cost: 3

Applied chaining
First rule:
l0 -> l15 : (1+r^0-n^0 <= 0 /\ -1+d^0 == 0), cost: 2
Second rule:
l15 -> l14 : 1+f^0 <= 0, cost: 1
New rule:
l0 -> l14 : (1+r^0-n^0 <= 0 /\ -1+d^0 == 0 /\ 1+f^0 <= 0), cost: 3

Applied chaining
First rule:
l0 -> l15 : (1+r^0-n^0 <= 0 /\ -1+d^0 == 0), cost: 2
Second rule:
l15 -> l14 : c^0'=-1+c^0, f^0'=1, f^0 == 0, cost: 1
New rule:
l0 -> l14 : c^0'=-1+c^0, f^0'=1, (1+r^0-n^0 <= 0 /\ -1+d^0 == 0 /\ f^0 == 0), cost: 3

Applied deletion
Removed the following rules: 53 54 55 71

Eliminated locations on tree-shaped paths
Start location: l17
  69: l0 -> l14 : (-2+d^0 >= 0 /\ 1+r^0-n^0 <= 0), cost: 2
  70: l0 -> l14 : (d^0 <= 0 /\ 1+r^0-n^0 <= 0), cost: 2
  72: l0 -> l10 : (1-r^0+n^0 <= 0 /\ -3+d^0 >= 0), cost: 3
  73: l0 -> l10 : (1-r^0+n^0 <= 0 /\ -1+d^0 <= 0), cost: 3
  81: l0 -> l10 : (1-r^0+n^0 <= 0 /\ -2+d^0 == 0 /\ -1+f^0 >= 0), cost: 4
  82: l0 -> l10 : (1-r^0+n^0 <= 0 /\ -2+d^0 == 0 /\ 1+f^0 <= 0), cost: 4
  83: l0 -> l10 : c^0'=-1+c^0, f^0'=1, (1-r^0+n^0 <= 0 /\ -2+d^0 == 0 /\ f^0 == 0), cost: 4
  84: l0 -> l14 : (1+r^0-n^0 <= 0 /\ -1+f^0 >= 0 /\ -1+d^0 == 0), cost: 3
  85: l0 -> l14 : (1+r^0-n^0 <= 0 /\ -1+d^0 == 0 /\ 1+f^0 <= 0), cost: 3
  86: l0 -> l14 : c^0'=-1+c^0, f^0'=1, (1+r^0-n^0 <= 0 /\ -1+d^0 == 0 /\ f^0 == 0), cost: 3
  75: l9 -> l0 : n^0'=n^post16, (-2+c^0 >= 0 /\ f^0 == 0), cost: 3
  76: l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0), cost: 4
  77: l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+f^0 <= 0), cost: 4
  78: l9 -> l0 : n^0'=n^post16, (c^0 <= 0 /\ f^0 == 0), cost: 3
  79: l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-1+f^0 >= 0 /\ c^0 <= 0), cost: 4
  80: l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (c^0 <= 0 /\ 1+f^0 <= 0), cost: 4
  64: l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
  63: l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
  61: l17 -> l9 : d^0'=0, c^0'=4, f^0'=0, TRUE, cost: 2


Eliminating location l0 by chaining:

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, (-2+c^0 >= 0 /\ f^0 == 0), cost: 3
Second rule:
l0 -> l14 : (-2+d^0 >= 0 /\ 1+r^0-n^0 <= 0), cost: 2
New rule:
l9 -> l14 : n^0'=n^post16, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ f^0 == 0), cost: 5

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, (-2+c^0 >= 0 /\ f^0 == 0), cost: 3
Second rule:
l0 -> l14 : (d^0 <= 0 /\ 1+r^0-n^0 <= 0), cost: 2
New rule:
l9 -> l14 : n^0'=n^post16, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ f^0 == 0), cost: 5

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, (-2+c^0 >= 0 /\ f^0 == 0), cost: 3
Second rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -3+d^0 >= 0), cost: 3
New rule:
l9 -> l10 : n^0'=n^post16, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ f^0 == 0), cost: 6

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, (-2+c^0 >= 0 /\ f^0 == 0), cost: 3
Second rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -1+d^0 <= 0), cost: 3
New rule:
l9 -> l10 : n^0'=n^post16, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -1+d^0 <= 0 /\ f^0 == 0), cost: 6

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, (-2+c^0 >= 0 /\ f^0 == 0), cost: 3
Second rule:
l0 -> l10 : c^0'=-1+c^0, f^0'=1, (1-r^0+n^0 <= 0 /\ -2+d^0 == 0 /\ f^0 == 0), cost: 4
New rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, f^0'=1, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ f^0 == 0), cost: 7

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, (-2+c^0 >= 0 /\ f^0 == 0), cost: 3
Second rule:
l0 -> l14 : c^0'=-1+c^0, f^0'=1, (1+r^0-n^0 <= 0 /\ -1+d^0 == 0 /\ f^0 == 0), cost: 3
New rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, f^0'=1, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+d^0 == 0 /\ f^0 == 0), cost: 6

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0), cost: 4
Second rule:
l0 -> l14 : (-2+d^0 >= 0 /\ 1+r^0-n^0 <= 0), cost: 2
New rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0), cost: 6

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0), cost: 4
Second rule:
l0 -> l14 : (d^0 <= 0 /\ 1+r^0-n^0 <= 0), cost: 2
New rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0), cost: 6

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0), cost: 4
Second rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -3+d^0 >= 0), cost: 3
New rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0), cost: 7

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0), cost: 4
Second rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -1+d^0 <= 0), cost: 3
New rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -1+d^0 <= 0), cost: 7

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0), cost: 4
Second rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -2+d^0 == 0 /\ -1+f^0 >= 0), cost: 4
New rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0), cost: 8

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0), cost: 4
Second rule:
l0 -> l14 : (1+r^0-n^0 <= 0 /\ -1+f^0 >= 0 /\ -1+d^0 == 0), cost: 3
New rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ -1+d^0 == 0), cost: 7

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+f^0 <= 0), cost: 4
Second rule:
l0 -> l14 : (-2+d^0 >= 0 /\ 1+r^0-n^0 <= 0), cost: 2
New rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ 1+f^0 <= 0), cost: 6

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+f^0 <= 0), cost: 4
Second rule:
l0 -> l14 : (d^0 <= 0 /\ 1+r^0-n^0 <= 0), cost: 2
New rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ 1+f^0 <= 0), cost: 6

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+f^0 <= 0), cost: 4
Second rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -3+d^0 >= 0), cost: 3
New rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ 1+f^0 <= 0), cost: 7

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+f^0 <= 0), cost: 4
Second rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -1+d^0 <= 0), cost: 3
New rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -1+d^0 <= 0 /\ 1+f^0 <= 0), cost: 7

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+f^0 <= 0), cost: 4
Second rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -2+d^0 == 0 /\ 1+f^0 <= 0), cost: 4
New rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ 1+f^0 <= 0), cost: 8

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+f^0 <= 0), cost: 4
Second rule:
l0 -> l14 : (1+r^0-n^0 <= 0 /\ -1+d^0 == 0 /\ 1+f^0 <= 0), cost: 3
New rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+d^0 == 0 /\ 1+f^0 <= 0), cost: 7

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, (c^0 <= 0 /\ f^0 == 0), cost: 3
Second rule:
l0 -> l14 : (-2+d^0 >= 0 /\ 1+r^0-n^0 <= 0), cost: 2
New rule:
l9 -> l14 : n^0'=n^post16, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ c^0 <= 0 /\ f^0 == 0), cost: 5

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, (c^0 <= 0 /\ f^0 == 0), cost: 3
Second rule:
l0 -> l14 : (d^0 <= 0 /\ 1+r^0-n^0 <= 0), cost: 2
New rule:
l9 -> l14 : n^0'=n^post16, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ c^0 <= 0 /\ f^0 == 0), cost: 5

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, (c^0 <= 0 /\ f^0 == 0), cost: 3
Second rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -3+d^0 >= 0), cost: 3
New rule:
l9 -> l10 : n^0'=n^post16, (1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0 /\ f^0 == 0), cost: 6

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, (c^0 <= 0 /\ f^0 == 0), cost: 3
Second rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -1+d^0 <= 0), cost: 3
New rule:
l9 -> l10 : n^0'=n^post16, (1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 <= 0 /\ f^0 == 0), cost: 6

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, (c^0 <= 0 /\ f^0 == 0), cost: 3
Second rule:
l0 -> l10 : c^0'=-1+c^0, f^0'=1, (1-r^0+n^0 <= 0 /\ -2+d^0 == 0 /\ f^0 == 0), cost: 4
New rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, f^0'=1, (-2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ f^0 == 0), cost: 7

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, (c^0 <= 0 /\ f^0 == 0), cost: 3
Second rule:
l0 -> l14 : c^0'=-1+c^0, f^0'=1, (1+r^0-n^0 <= 0 /\ -1+d^0 == 0 /\ f^0 == 0), cost: 3
New rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, f^0'=1, (1+r^0-n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 == 0 /\ f^0 == 0), cost: 6

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-1+f^0 >= 0 /\ c^0 <= 0), cost: 4
Second rule:
l0 -> l14 : (-2+d^0 >= 0 /\ 1+r^0-n^0 <= 0), cost: 2
New rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0 /\ c^0 <= 0), cost: 6

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-1+f^0 >= 0 /\ c^0 <= 0), cost: 4
Second rule:
l0 -> l14 : (d^0 <= 0 /\ 1+r^0-n^0 <= 0), cost: 2
New rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ c^0 <= 0), cost: 6

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-1+f^0 >= 0 /\ c^0 <= 0), cost: 4
Second rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -3+d^0 >= 0), cost: 3
New rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0), cost: 7

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-1+f^0 >= 0 /\ c^0 <= 0), cost: 4
Second rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -1+d^0 <= 0), cost: 3
New rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 <= 0), cost: 7

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-1+f^0 >= 0 /\ c^0 <= 0), cost: 4
Second rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -2+d^0 == 0 /\ -1+f^0 >= 0), cost: 4
New rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+d^0 == 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0), cost: 8

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (-1+f^0 >= 0 /\ c^0 <= 0), cost: 4
Second rule:
l0 -> l14 : (1+r^0-n^0 <= 0 /\ -1+f^0 >= 0 /\ -1+d^0 == 0), cost: 3
New rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ c^0 <= 0 /\ -1+d^0 == 0), cost: 7

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (c^0 <= 0 /\ 1+f^0 <= 0), cost: 4
Second rule:
l0 -> l14 : (-2+d^0 >= 0 /\ 1+r^0-n^0 <= 0), cost: 2
New rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 6

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (c^0 <= 0 /\ 1+f^0 <= 0), cost: 4
Second rule:
l0 -> l14 : (d^0 <= 0 /\ 1+r^0-n^0 <= 0), cost: 2
New rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 6

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (c^0 <= 0 /\ 1+f^0 <= 0), cost: 4
Second rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -3+d^0 >= 0), cost: 3
New rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 7

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (c^0 <= 0 /\ 1+f^0 <= 0), cost: 4
Second rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -1+d^0 <= 0), cost: 3
New rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 <= 0 /\ 1+f^0 <= 0), cost: 7

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (c^0 <= 0 /\ 1+f^0 <= 0), cost: 4
Second rule:
l0 -> l10 : (1-r^0+n^0 <= 0 /\ -2+d^0 == 0 /\ 1+f^0 <= 0), cost: 4
New rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 8

Applied chaining
First rule:
l9 -> l0 : n^0'=n^post16, c^0'=-1+c^0, (c^0 <= 0 /\ 1+f^0 <= 0), cost: 4
Second rule:
l0 -> l14 : (1+r^0-n^0 <= 0 /\ -1+d^0 == 0 /\ 1+f^0 <= 0), cost: 3
New rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (1+r^0-n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 == 0 /\ 1+f^0 <= 0), cost: 7

Applied deletion
Removed the following rules: 69 70 72 73 75 76 77 78 79 80 81 82 83 84 85 86

Eliminated locations on tree-shaped paths
Start location: l17
  87: l9 -> l14 : n^0'=n^post16, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ f^0 == 0), cost: 5
  88: l9 -> l14 : n^0'=n^post16, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ f^0 == 0), cost: 5
  89: l9 -> l10 : n^0'=n^post16, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ f^0 == 0), cost: 6
  90: l9 -> l10 : n^0'=n^post16, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -1+d^0 <= 0 /\ f^0 == 0), cost: 6
  91: l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, f^0'=1, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ f^0 == 0), cost: 7
  92: l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, f^0'=1, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+d^0 == 0 /\ f^0 == 0), cost: 6
  93: l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0), cost: 6
  94: l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0), cost: 6
  95: l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0), cost: 7
  96: l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -1+d^0 <= 0), cost: 7
  97: l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0), cost: 8
  98: l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ -1+d^0 == 0), cost: 7
  99: l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ 1+f^0 <= 0), cost: 6
 100: l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ 1+f^0 <= 0), cost: 6
 101: l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ 1+f^0 <= 0), cost: 7
 102: l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -1+d^0 <= 0 /\ 1+f^0 <= 0), cost: 7
 103: l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ 1+f^0 <= 0), cost: 8
 104: l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+d^0 == 0 /\ 1+f^0 <= 0), cost: 7
 105: l9 -> l14 : n^0'=n^post16, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ c^0 <= 0 /\ f^0 == 0), cost: 5
 106: l9 -> l14 : n^0'=n^post16, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ c^0 <= 0 /\ f^0 == 0), cost: 5
 107: l9 -> l10 : n^0'=n^post16, (1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0 /\ f^0 == 0), cost: 6
 108: l9 -> l10 : n^0'=n^post16, (1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 <= 0 /\ f^0 == 0), cost: 6
 109: l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, f^0'=1, (-2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ f^0 == 0), cost: 7
 110: l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, f^0'=1, (1+r^0-n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 == 0 /\ f^0 == 0), cost: 6
 111: l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0 /\ c^0 <= 0), cost: 6
 112: l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ c^0 <= 0), cost: 6
 113: l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0), cost: 7
 114: l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 <= 0), cost: 7
 115: l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+d^0 == 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0), cost: 8
 116: l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ c^0 <= 0 /\ -1+d^0 == 0), cost: 7
 117: l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 6
 118: l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 6
 119: l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 7
 120: l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 <= 0 /\ 1+f^0 <= 0), cost: 7
 121: l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 8
 122: l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (1+r^0-n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 == 0 /\ 1+f^0 <= 0), cost: 7
  64: l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
  63: l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
  61: l17 -> l9 : d^0'=0, c^0'=4, f^0'=0, TRUE, cost: 2


Eliminating location l10 by chaining:

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ f^0 == 0), cost: 6
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=-c^0+s^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ -c^0+s^0 >= 0 /\ f^0 == 0), cost: 8

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -1+d^0 <= 0 /\ f^0 == 0), cost: 6
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=-c^0+s^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -1+d^0 <= 0 /\ -c^0+s^0 >= 0 /\ f^0 == 0), cost: 8

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, f^0'=1, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ f^0 == 0), cost: 7
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, f^0'=1, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ 1-c^0+s^0 >= 0 /\ f^0 == 0), cost: 9

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0), cost: 7
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ 1-c^0+s^0 >= 0), cost: 9

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -1+d^0 <= 0), cost: 7
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ 1-c^0+s^0 >= 0 /\ -1+d^0 <= 0), cost: 9

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0), cost: 8
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ 1-c^0+s^0 >= 0), cost: 10

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ 1+f^0 <= 0), cost: 7
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ 1-c^0+s^0 >= 0 /\ 1+f^0 <= 0), cost: 9

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -1+d^0 <= 0 /\ 1+f^0 <= 0), cost: 7
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ 1-c^0+s^0 >= 0 /\ -1+d^0 <= 0 /\ 1+f^0 <= 0), cost: 9

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ 1+f^0 <= 0), cost: 8
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ 1-c^0+s^0 >= 0 /\ 1+f^0 <= 0), cost: 10

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, (1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0 /\ f^0 == 0), cost: 6
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=-c^0+s^0, (1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0 /\ -c^0+s^0 >= 0 /\ f^0 == 0), cost: 8

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, (1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 <= 0 /\ f^0 == 0), cost: 6
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=-c^0+s^0, (1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 <= 0 /\ -c^0+s^0 >= 0 /\ f^0 == 0), cost: 8

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, f^0'=1, (-2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ f^0 == 0), cost: 7
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, f^0'=1, (-2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0 /\ f^0 == 0), cost: 9

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0), cost: 7
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0), cost: 9

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 <= 0), cost: 7
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0 /\ -1+d^0 <= 0), cost: 9

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+d^0 == 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0), cost: 8
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+d^0 == 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0), cost: 10

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 7
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0 /\ 1+f^0 <= 0), cost: 9

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 <= 0 /\ 1+f^0 <= 0), cost: 7
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0 /\ -1+d^0 <= 0 /\ 1+f^0 <= 0), cost: 9

Applied chaining
First rule:
l9 -> l10 : n^0'=n^post16, c^0'=-1+c^0, (-2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 8
Second rule:
l10 -> l9 : d^0'=1, s^0'=-c^0+s^0, -c^0+s^0 >= 0, cost: 2
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0 /\ 1+f^0 <= 0), cost: 10

Applied deletion
Removed the following rules: 64 89 90 91 95 96 97 101 102 103 107 108 109 113 114 115 119 120 121

Eliminating location l14 by chaining:

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ f^0 == 0), cost: 5
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=c^0+s^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -255+c^0+s^0 <= 0 /\ f^0 == 0), cost: 7

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ f^0 == 0), cost: 5
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=c^0+s^0, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -255+c^0+s^0 <= 0 /\ f^0 == 0), cost: 7

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, f^0'=1, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+d^0 == 0 /\ f^0 == 0), cost: 6
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, f^0'=1, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ -1+d^0 == 0 /\ f^0 == 0), cost: 8

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0), cost: 6
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0), cost: 8

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0), cost: 6
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0), cost: 8

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ -1+d^0 == 0), cost: 7
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ -1+d^0 == 0), cost: 9

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ 1+f^0 <= 0), cost: 6
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ 1+f^0 <= 0), cost: 8

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ 1+f^0 <= 0), cost: 6
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ 1+f^0 <= 0), cost: 8

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+d^0 == 0 /\ 1+f^0 <= 0), cost: 7
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ -1+d^0 == 0 /\ 1+f^0 <= 0), cost: 9

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ c^0 <= 0 /\ f^0 == 0), cost: 5
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=c^0+s^0, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ c^0 <= 0 /\ -255+c^0+s^0 <= 0 /\ f^0 == 0), cost: 7

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ c^0 <= 0 /\ f^0 == 0), cost: 5
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=c^0+s^0, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ c^0 <= 0 /\ -255+c^0+s^0 <= 0 /\ f^0 == 0), cost: 7

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, f^0'=1, (1+r^0-n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 == 0 /\ f^0 == 0), cost: 6
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, f^0'=1, (1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0 /\ -1+d^0 == 0 /\ f^0 == 0), cost: 8

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0 /\ c^0 <= 0), cost: 6
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0), cost: 8

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ c^0 <= 0), cost: 6
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0), cost: 8

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ c^0 <= 0 /\ -1+d^0 == 0), cost: 7
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0 /\ -1+d^0 == 0), cost: 9

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 6
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 8

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 6
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 8

Applied chaining
First rule:
l9 -> l14 : n^0'=n^post16, c^0'=-1+c^0, (1+r^0-n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 == 0 /\ 1+f^0 <= 0), cost: 7
Second rule:
l14 -> l9 : d^0'=2, s^0'=c^0+s^0, -255+c^0+s^0 <= 0, cost: 2
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0 /\ -1+d^0 == 0 /\ 1+f^0 <= 0), cost: 9

Applied deletion
Removed the following rules: 63 87 88 92 93 94 98 99 100 104 105 106 110 111 112 116 117 118 122

Eliminated locations on tree-shaped paths
Start location: l17
 123: l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=-c^0+s^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ -c^0+s^0 >= 0 /\ f^0 == 0), cost: 8
 124: l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=-c^0+s^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -1+d^0 <= 0 /\ -c^0+s^0 >= 0 /\ f^0 == 0), cost: 8
 125: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, f^0'=1, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ 1-c^0+s^0 >= 0 /\ f^0 == 0), cost: 9
 126: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ 1-c^0+s^0 >= 0), cost: 9
 127: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ 1-c^0+s^0 >= 0 /\ -1+d^0 <= 0), cost: 9
 128: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ 1-c^0+s^0 >= 0), cost: 10
 129: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ 1-c^0+s^0 >= 0 /\ 1+f^0 <= 0), cost: 9
 130: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ 1-c^0+s^0 >= 0 /\ -1+d^0 <= 0 /\ 1+f^0 <= 0), cost: 9
 131: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ 1-c^0+s^0 >= 0 /\ 1+f^0 <= 0), cost: 10
 132: l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=-c^0+s^0, (1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0 /\ -c^0+s^0 >= 0 /\ f^0 == 0), cost: 8
 133: l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=-c^0+s^0, (1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 <= 0 /\ -c^0+s^0 >= 0 /\ f^0 == 0), cost: 8
 134: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, f^0'=1, (-2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0 /\ f^0 == 0), cost: 9
 135: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0), cost: 9
 136: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0 /\ -1+d^0 <= 0), cost: 9
 137: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+d^0 == 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0), cost: 10
 138: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0 /\ 1+f^0 <= 0), cost: 9
 139: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0 /\ -1+d^0 <= 0 /\ 1+f^0 <= 0), cost: 9
 140: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0 /\ 1+f^0 <= 0), cost: 10
 141: l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=c^0+s^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -255+c^0+s^0 <= 0 /\ f^0 == 0), cost: 7
 142: l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=c^0+s^0, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -255+c^0+s^0 <= 0 /\ f^0 == 0), cost: 7
 143: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, f^0'=1, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ -1+d^0 == 0 /\ f^0 == 0), cost: 8
 144: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0), cost: 8
 145: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0), cost: 8
 146: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ -1+d^0 == 0), cost: 9
 147: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ 1+f^0 <= 0), cost: 8
 148: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ 1+f^0 <= 0), cost: 8
 149: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ -1+d^0 == 0 /\ 1+f^0 <= 0), cost: 9
 150: l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=c^0+s^0, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ c^0 <= 0 /\ -255+c^0+s^0 <= 0 /\ f^0 == 0), cost: 7
 151: l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=c^0+s^0, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ c^0 <= 0 /\ -255+c^0+s^0 <= 0 /\ f^0 == 0), cost: 7
 152: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, f^0'=1, (1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0 /\ -1+d^0 == 0 /\ f^0 == 0), cost: 8
 153: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0), cost: 8
 154: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0), cost: 8
 155: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0 /\ -1+d^0 == 0), cost: 9
 156: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 8
 157: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 8
 158: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0 /\ -1+d^0 == 0 /\ 1+f^0 <= 0), cost: 9
  61: l17 -> l9 : d^0'=0, c^0'=4, f^0'=0, TRUE, cost: 2


Applied acceleration
Original rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=-c^0+s^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -1+d^0 <= 0 /\ -c^0+s^0 >= 0 /\ f^0 == 0), cost: 8
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=s^0-n0*c^0, (-1+n0 >= 0 /\ -2+c^0 >= 0 /\ -f^0 >= 0 /\ -(-1+n0)*c^0-c^0+s^0 >= 0 /\ 1-d^0 >= 0 /\ f^0 >= 0 /\ -1+r^0-n^post16 >= 0), cost: 8*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_CoANHe.txt

Applied acceleration
Original rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ 1-c^0+s^0 >= 0 /\ -1+d^0 <= 0), cost: 9
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=c^0-n3, s^0'=1/2*n3^2-c^0*n3+s^0+1/2*n3, (-2+c^0 >= 0 /\ -1+n3 >= 0 /\ -1+f^0 >= 0 /\ 1-d^0 >= 0 /\ -1/2-(-1+n3)*c^0+1/2*(-1+n3)^2-c^0+s^0+3/2*n3 >= 0 /\ -1+c^0-n3 >= 0 /\ -1+r^0-n^post16 >= 0), cost: 9*n3
Sub-proof via acceration calculus written to file:///tmp/tmpnam_fGLGoE.txt

Applied instantiation
Original rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=c^0-n3, s^0'=1/2*n3^2-c^0*n3+s^0+1/2*n3, (-2+c^0 >= 0 /\ -1+n3 >= 0 /\ -1+f^0 >= 0 /\ 1-d^0 >= 0 /\ -1/2-(-1+n3)*c^0+1/2*(-1+n3)^2-c^0+s^0+3/2*n3 >= 0 /\ -1+c^0-n3 >= 0 /\ -1+r^0-n^post16 >= 0), cost: 9*n3
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=1, s^0'=-1/2+1/2*(-1+c^0)^2+1/2*c^0+s^0-c^0*(-1+c^0), (0 >= 0 /\ -2+c^0 >= 0 /\ -1+f^0 >= 0 /\ 1-d^0 >= 0 /\ -2-(-2+c^0)*c^0+1/2*c^0+s^0+1/2*(-2+c^0)^2 >= 0 /\ -1+r^0-n^post16 >= 0), cost: -9+9*c^0

Applied acceleration
Original rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ 1-c^0+s^0 >= 0 /\ -1+d^0 <= 0 /\ 1+f^0 <= 0), cost: 9
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-n6+c^0, s^0'=-n6*c^0+1/2*n6+s^0+1/2*n6^2, (-1-n6+c^0 >= 0 /\ -2+c^0 >= 0 /\ 1-d^0 >= 0 /\ -1-f^0 >= 0 /\ -1/2+1/2*(-1+n6)^2+3/2*n6-c^0+s^0-c^0*(-1+n6) >= 0 /\ -1+r^0-n^post16 >= 0 /\ -1+n6 >= 0), cost: 9*n6
Sub-proof via acceration calculus written to file:///tmp/tmpnam_AjoPjo.txt

Applied instantiation
Original rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-n6+c^0, s^0'=-n6*c^0+1/2*n6+s^0+1/2*n6^2, (-1-n6+c^0 >= 0 /\ -2+c^0 >= 0 /\ 1-d^0 >= 0 /\ -1-f^0 >= 0 /\ -1/2+1/2*(-1+n6)^2+3/2*n6-c^0+s^0-c^0*(-1+n6) >= 0 /\ -1+r^0-n^post16 >= 0 /\ -1+n6 >= 0), cost: 9*n6
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=1, s^0'=-1/2+1/2*(-1+c^0)^2+1/2*c^0+s^0-c^0*(-1+c^0), (0 >= 0 /\ -2+c^0 >= 0 /\ 1-d^0 >= 0 /\ -1-f^0 >= 0 /\ -2-(-2+c^0)*c^0+1/2*c^0+s^0+1/2*(-2+c^0)^2 >= 0 /\ -1+r^0-n^post16 >= 0), cost: -9+9*c^0

Applied nonterm
Original rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=-c^0+s^0, (1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ -1+d^0 <= 0 /\ -c^0+s^0 >= 0 /\ f^0 == 0), cost: 8
New rule:
l9 -> [18] : (-1+n9 >= 0 /\ -f^0 >= 0 /\ 1-d^0 >= 0 /\ -c^0+s^0 >= 0 /\ -c^0 >= 0 /\ f^0 >= 0 /\ -1+r^0-n^post16 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_gaMaIi.txt

Applied nonterm
Original rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0 /\ -1+d^0 <= 0), cost: 9
New rule:
l9 -> [18] : (-1+f^0 >= 0 /\ -1+n12 >= 0 /\ 1-c^0+s^0 >= 0 /\ 1-d^0 >= 0 /\ -c^0 >= 0 /\ -1+r^0-n^post16 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_dfcCke.txt

Applied nonterm
Original rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0 /\ -1+d^0 <= 0 /\ 1+f^0 <= 0), cost: 9
New rule:
l9 -> [18] : (1-c^0+s^0 >= 0 /\ 1-d^0 >= 0 /\ -1-f^0 >= 0 /\ -c^0 >= 0 /\ -1+n15 >= 0 /\ -1+r^0-n^post16 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_EFmPhG.txt

Applied acceleration
Original rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=c^0+s^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -255+c^0+s^0 <= 0 /\ f^0 == 0), cost: 7
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=s^0+c^0*n17, (-2+c^0 >= 0 /\ -1+n17 >= 0 /\ -f^0 >= 0 /\ -2+d^0 >= 0 /\ 255-(-1+n17)*c^0-c^0-s^0 >= 0 /\ -1-r^0+n^post16 >= 0 /\ f^0 >= 0), cost: 7*n17
Sub-proof via acceration calculus written to file:///tmp/tmpnam_MdmDcH.txt

Applied acceleration
Original rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0), cost: 8
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-n20+c^0, s^0'=n20*c^0-1/2*n20+s^0-1/2*n20^2, (-1-n20+c^0 >= 0 /\ -2+c^0 >= 0 /\ 509/2+1/2*(-1+n20)^2+3/2*n20-c^0-s^0-c^0*(-1+n20) >= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0 /\ -1-r^0+n^post16 >= 0 /\ -1+n20 >= 0), cost: 8*n20
Sub-proof via acceration calculus written to file:///tmp/tmpnam_PAbFJG.txt

Applied instantiation
Original rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-n20+c^0, s^0'=n20*c^0-1/2*n20+s^0-1/2*n20^2, (-1-n20+c^0 >= 0 /\ -2+c^0 >= 0 /\ 509/2+1/2*(-1+n20)^2+3/2*n20-c^0-s^0-c^0*(-1+n20) >= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0 /\ -1-r^0+n^post16 >= 0 /\ -1+n20 >= 0), cost: 8*n20
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=1, s^0'=1/2-1/2*(-1+c^0)^2-1/2*c^0+s^0+c^0*(-1+c^0), (0 >= 0 /\ -2+c^0 >= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0 /\ 253-(-2+c^0)*c^0+1/2*c^0-s^0+1/2*(-2+c^0)^2 >= 0 /\ -1-r^0+n^post16 >= 0), cost: -8+8*c^0

Applied acceleration
Original rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ 1+f^0 <= 0), cost: 8
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=c^0-n23, s^0'=c^0*n23-1/2*n23^2+s^0-1/2*n23, (-2+c^0 >= 0 /\ -1+c^0-n23 >= 0 /\ -2+d^0 >= 0 /\ 509/2-c^0*(-1+n23)-c^0+1/2*(-1+n23)^2-s^0+3/2*n23 >= 0 /\ -1+n23 >= 0 /\ -1-f^0 >= 0 /\ -1-r^0+n^post16 >= 0), cost: 8*n23
Sub-proof via acceration calculus written to file:///tmp/tmpnam_PbMDPA.txt

Applied instantiation
Original rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=c^0-n23, s^0'=c^0*n23-1/2*n23^2+s^0-1/2*n23, (-2+c^0 >= 0 /\ -1+c^0-n23 >= 0 /\ -2+d^0 >= 0 /\ 509/2-c^0*(-1+n23)-c^0+1/2*(-1+n23)^2-s^0+3/2*n23 >= 0 /\ -1+n23 >= 0 /\ -1-f^0 >= 0 /\ -1-r^0+n^post16 >= 0), cost: 8*n23
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=1, s^0'=1/2-1/2*(-1+c^0)^2-1/2*c^0+s^0+c^0*(-1+c^0), (0 >= 0 /\ -2+c^0 >= 0 /\ -2+d^0 >= 0 /\ 253-(-2+c^0)*c^0+1/2*c^0-s^0+1/2*(-2+c^0)^2 >= 0 /\ -1-f^0 >= 0 /\ -1-r^0+n^post16 >= 0), cost: -8+8*c^0

Applied nonterm
Original rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=c^0+s^0, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ c^0 <= 0 /\ -255+c^0+s^0 <= 0 /\ f^0 == 0), cost: 7
New rule:
l9 -> [18] : (-1+n26 >= 0 /\ 255-c^0-s^0 >= 0 /\ -f^0 >= 0 /\ -2+d^0 >= 0 /\ -1-r^0+n^post16 >= 0 /\ -c^0 >= 0 /\ f^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_fOKNdK.txt

Applied nonterm
Original rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0), cost: 8
New rule:
l9 -> [18] : (-2+d^0 >= 0 /\ -1+f^0 >= 0 /\ -1-r^0+n^post16 >= 0 /\ -c^0 >= 0 /\ -1+n29 >= 0 /\ 256-c^0-s^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_pfpbdB.txt

Applied nonterm
Original rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (1+r^0-n^post16 <= 0 /\ -2+d^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 8
New rule:
l9 -> [18] : (-1+n32 >= 0 /\ -2+d^0 >= 0 /\ -1-f^0 >= 0 /\ -1-r^0+n^post16 >= 0 /\ -c^0 >= 0 /\ 256-c^0-s^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_NmpJjB.txt

Applied simplification
Original rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=s^0-n0*c^0, (-1+n0 >= 0 /\ -2+c^0 >= 0 /\ -f^0 >= 0 /\ -(-1+n0)*c^0-c^0+s^0 >= 0 /\ 1-d^0 >= 0 /\ f^0 >= 0 /\ -1+r^0-n^post16 >= 0), cost: 8*n0
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=s^0-n0*c^0, (-1+n0 >= 0 /\ -2+c^0 >= 0 /\ -(-1+n0)*c^0-c^0+s^0 >= 0 /\ -1+d^0 <= 0 /\ f^0 <= 0 /\ f^0 >= 0 /\ -1+r^0-n^post16 >= 0), cost: 8*n0

Applied simplification
Original rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=1, s^0'=-1/2+1/2*(-1+c^0)^2+1/2*c^0+s^0-c^0*(-1+c^0), (0 >= 0 /\ -2+c^0 >= 0 /\ -1+f^0 >= 0 /\ 1-d^0 >= 0 /\ -2-(-2+c^0)*c^0+1/2*c^0+s^0+1/2*(-2+c^0)^2 >= 0 /\ -1+r^0-n^post16 >= 0), cost: -9+9*c^0
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=1, s^0'=-1/2+1/2*(-1+c^0)^2+1/2*c^0+s^0-c^0*(-1+c^0), (-2+c^0 >= 0 /\ -1+f^0 >= 0 /\ -1+d^0 <= 0 /\ -2-(-2+c^0)*c^0+1/2*c^0+s^0+1/2*(-2+c^0)^2 >= 0 /\ -1+r^0-n^post16 >= 0), cost: -9+9*c^0

Applied simplification
Original rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=1, s^0'=-1/2+1/2*(-1+c^0)^2+1/2*c^0+s^0-c^0*(-1+c^0), (0 >= 0 /\ -2+c^0 >= 0 /\ 1-d^0 >= 0 /\ -1-f^0 >= 0 /\ -2-(-2+c^0)*c^0+1/2*c^0+s^0+1/2*(-2+c^0)^2 >= 0 /\ -1+r^0-n^post16 >= 0), cost: -9+9*c^0
New rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=1, s^0'=-1/2+1/2*(-1+c^0)^2+1/2*c^0+s^0-c^0*(-1+c^0), (-2+c^0 >= 0 /\ -1+d^0 <= 0 /\ 1+f^0 <= 0 /\ -2-(-2+c^0)*c^0+1/2*c^0+s^0+1/2*(-2+c^0)^2 >= 0 /\ -1+r^0-n^post16 >= 0), cost: -9+9*c^0

Applied simplification
Original rule:
l9 -> [18] : (-1+n9 >= 0 /\ -f^0 >= 0 /\ 1-d^0 >= 0 /\ -c^0+s^0 >= 0 /\ -c^0 >= 0 /\ f^0 >= 0 /\ -1+r^0-n^post16 >= 0), cost: NONTERM
New rule:
l9 -> [18] : (-1+n9 >= 0 /\ -1+d^0 <= 0 /\ -c^0+s^0 >= 0 /\ -c^0 >= 0 /\ f^0 <= 0 /\ f^0 >= 0 /\ -1+r^0-n^post16 >= 0), cost: NONTERM

Applied simplification
Original rule:
l9 -> [18] : (-1+f^0 >= 0 /\ -1+n12 >= 0 /\ 1-c^0+s^0 >= 0 /\ 1-d^0 >= 0 /\ -c^0 >= 0 /\ -1+r^0-n^post16 >= 0), cost: NONTERM
New rule:
l9 -> [18] : (-1+f^0 >= 0 /\ -1+n12 >= 0 /\ 1-c^0+s^0 >= 0 /\ -1+d^0 <= 0 /\ -c^0 >= 0 /\ -1+r^0-n^post16 >= 0), cost: NONTERM

Applied simplification
Original rule:
l9 -> [18] : (1-c^0+s^0 >= 0 /\ 1-d^0 >= 0 /\ -1-f^0 >= 0 /\ -c^0 >= 0 /\ -1+n15 >= 0 /\ -1+r^0-n^post16 >= 0), cost: NONTERM
New rule:
l9 -> [18] : (1-c^0+s^0 >= 0 /\ -1+d^0 <= 0 /\ 1+f^0 <= 0 /\ -c^0 >= 0 /\ -1+n15 >= 0 /\ -1+r^0-n^post16 >= 0), cost: NONTERM

Applied simplification
Original rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=s^0+c^0*n17, (-2+c^0 >= 0 /\ -1+n17 >= 0 /\ -f^0 >= 0 /\ -2+d^0 >= 0 /\ 255-(-1+n17)*c^0-c^0-s^0 >= 0 /\ -1-r^0+n^post16 >= 0 /\ f^0 >= 0), cost: 7*n17
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=s^0+c^0*n17, (-2+c^0 >= 0 /\ -1+n17 >= 0 /\ -2+d^0 >= 0 /\ 255-(-1+n17)*c^0-c^0-s^0 >= 0 /\ -1-r^0+n^post16 >= 0 /\ f^0 <= 0 /\ f^0 >= 0), cost: 7*n17

Applied simplification
Original rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=1, s^0'=1/2-1/2*(-1+c^0)^2-1/2*c^0+s^0+c^0*(-1+c^0), (0 >= 0 /\ -2+c^0 >= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0 /\ 253-(-2+c^0)*c^0+1/2*c^0-s^0+1/2*(-2+c^0)^2 >= 0 /\ -1-r^0+n^post16 >= 0), cost: -8+8*c^0
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=1, s^0'=1/2-1/2*(-1+c^0)^2-1/2*c^0+s^0+c^0*(-1+c^0), (-2+c^0 >= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0 /\ 253-(-2+c^0)*c^0+1/2*c^0-s^0+1/2*(-2+c^0)^2 >= 0 /\ -1-r^0+n^post16 >= 0), cost: -8+8*c^0

Applied simplification
Original rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=1, s^0'=1/2-1/2*(-1+c^0)^2-1/2*c^0+s^0+c^0*(-1+c^0), (0 >= 0 /\ -2+c^0 >= 0 /\ -2+d^0 >= 0 /\ 253-(-2+c^0)*c^0+1/2*c^0-s^0+1/2*(-2+c^0)^2 >= 0 /\ -1-f^0 >= 0 /\ -1-r^0+n^post16 >= 0), cost: -8+8*c^0
New rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=1, s^0'=1/2-1/2*(-1+c^0)^2-1/2*c^0+s^0+c^0*(-1+c^0), (-2+c^0 >= 0 /\ -2+d^0 >= 0 /\ 253-(-2+c^0)*c^0+1/2*c^0-s^0+1/2*(-2+c^0)^2 >= 0 /\ 1+f^0 <= 0 /\ -1-r^0+n^post16 >= 0), cost: -8+8*c^0

Applied simplification
Original rule:
l9 -> [18] : (-1+n26 >= 0 /\ 255-c^0-s^0 >= 0 /\ -f^0 >= 0 /\ -2+d^0 >= 0 /\ -1-r^0+n^post16 >= 0 /\ -c^0 >= 0 /\ f^0 >= 0), cost: NONTERM
New rule:
l9 -> [18] : (-1+n26 >= 0 /\ 255-c^0-s^0 >= 0 /\ -2+d^0 >= 0 /\ -1-r^0+n^post16 >= 0 /\ -c^0 >= 0 /\ f^0 <= 0 /\ f^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l9 -> [18] : (-2+d^0 >= 0 /\ -1+f^0 >= 0 /\ -1-r^0+n^post16 >= 0 /\ -c^0 >= 0 /\ -1+n29 >= 0 /\ 256-c^0-s^0 >= 0), cost: NONTERM
New rule:
l9 -> [18] : (-2+d^0 >= 0 /\ -1+f^0 >= 0 /\ c^0 <= 0 /\ -1-r^0+n^post16 >= 0 /\ -1+n29 >= 0 /\ 256-c^0-s^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l9 -> [18] : (-1+n32 >= 0 /\ -2+d^0 >= 0 /\ -1-f^0 >= 0 /\ -1-r^0+n^post16 >= 0 /\ -c^0 >= 0 /\ 256-c^0-s^0 >= 0), cost: NONTERM
New rule:
l9 -> [18] : (-1+n32 >= 0 /\ -2+d^0 >= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0 /\ -1-r^0+n^post16 >= 0 /\ 256-c^0-s^0 >= 0), cost: NONTERM

Applied deletion
Removed the following rules: 124 127 130 133 136 139 141 144 147 150 153 156

Accelerated simple loops
Start location: l17
 123: l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=-c^0+s^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ -c^0+s^0 >= 0 /\ f^0 == 0), cost: 8
 125: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, f^0'=1, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ 1-c^0+s^0 >= 0 /\ f^0 == 0), cost: 9
 126: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ 1-c^0+s^0 >= 0), cost: 9
 128: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ 1-c^0+s^0 >= 0), cost: 10
 129: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ 1-c^0+s^0 >= 0 /\ 1+f^0 <= 0), cost: 9
 131: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+c^0 >= 0 /\ -2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ 1-c^0+s^0 >= 0 /\ 1+f^0 <= 0), cost: 10
 132: l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=-c^0+s^0, (1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0 /\ -c^0+s^0 >= 0 /\ f^0 == 0), cost: 8
 134: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, f^0'=1, (-2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0 /\ f^0 == 0), cost: 9
 135: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0), cost: 9
 137: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+d^0 == 0 /\ -1+f^0 >= 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0), cost: 10
 138: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (1-r^0+n^post16 <= 0 /\ -3+d^0 >= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0 /\ 1+f^0 <= 0), cost: 9
 140: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=-1+c^0, s^0'=1-c^0+s^0, (-2+d^0 == 0 /\ 1-r^0+n^post16 <= 0 /\ c^0 <= 0 /\ 1-c^0+s^0 >= 0 /\ 1+f^0 <= 0), cost: 10
 142: l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=c^0+s^0, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -255+c^0+s^0 <= 0 /\ f^0 == 0), cost: 7
 143: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, f^0'=1, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ -1+d^0 == 0 /\ f^0 == 0), cost: 8
 145: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0), cost: 8
 146: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ -1+d^0 == 0), cost: 9
 148: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ 1+f^0 <= 0), cost: 8
 149: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (-2+c^0 >= 0 /\ 1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ -1+d^0 == 0 /\ 1+f^0 <= 0), cost: 9
 151: l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=c^0+s^0, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ c^0 <= 0 /\ -255+c^0+s^0 <= 0 /\ f^0 == 0), cost: 7
 152: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, f^0'=1, (1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0 /\ -1+d^0 == 0 /\ f^0 == 0), cost: 8
 154: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0), cost: 8
 155: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (1+r^0-n^post16 <= 0 /\ -1+f^0 >= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0 /\ -1+d^0 == 0), cost: 9
 157: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0), cost: 8
 158: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=-1+c^0, s^0'=-1+c^0+s^0, (1+r^0-n^post16 <= 0 /\ -256+c^0+s^0 <= 0 /\ c^0 <= 0 /\ -1+d^0 == 0 /\ 1+f^0 <= 0), cost: 9
 171: l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=s^0-n0*c^0, (-1+n0 >= 0 /\ -2+c^0 >= 0 /\ -(-1+n0)*c^0-c^0+s^0 >= 0 /\ -1+d^0 <= 0 /\ f^0 <= 0 /\ f^0 >= 0 /\ -1+r^0-n^post16 >= 0), cost: 8*n0
 172: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=1, s^0'=-1/2+1/2*(-1+c^0)^2+1/2*c^0+s^0-c^0*(-1+c^0), (-2+c^0 >= 0 /\ -1+f^0 >= 0 /\ -1+d^0 <= 0 /\ -2-(-2+c^0)*c^0+1/2*c^0+s^0+1/2*(-2+c^0)^2 >= 0 /\ -1+r^0-n^post16 >= 0), cost: -9+9*c^0
 173: l9 -> l9 : d^0'=1, n^0'=n^post16, c^0'=1, s^0'=-1/2+1/2*(-1+c^0)^2+1/2*c^0+s^0-c^0*(-1+c^0), (-2+c^0 >= 0 /\ -1+d^0 <= 0 /\ 1+f^0 <= 0 /\ -2-(-2+c^0)*c^0+1/2*c^0+s^0+1/2*(-2+c^0)^2 >= 0 /\ -1+r^0-n^post16 >= 0), cost: -9+9*c^0
 174: l9 -> [18] : (-1+n9 >= 0 /\ -1+d^0 <= 0 /\ -c^0+s^0 >= 0 /\ -c^0 >= 0 /\ f^0 <= 0 /\ f^0 >= 0 /\ -1+r^0-n^post16 >= 0), cost: NONTERM
 175: l9 -> [18] : (-1+f^0 >= 0 /\ -1+n12 >= 0 /\ 1-c^0+s^0 >= 0 /\ -1+d^0 <= 0 /\ -c^0 >= 0 /\ -1+r^0-n^post16 >= 0), cost: NONTERM
 176: l9 -> [18] : (1-c^0+s^0 >= 0 /\ -1+d^0 <= 0 /\ 1+f^0 <= 0 /\ -c^0 >= 0 /\ -1+n15 >= 0 /\ -1+r^0-n^post16 >= 0), cost: NONTERM
 177: l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=s^0+c^0*n17, (-2+c^0 >= 0 /\ -1+n17 >= 0 /\ -2+d^0 >= 0 /\ 255-(-1+n17)*c^0-c^0-s^0 >= 0 /\ -1-r^0+n^post16 >= 0 /\ f^0 <= 0 /\ f^0 >= 0), cost: 7*n17
 178: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=1, s^0'=1/2-1/2*(-1+c^0)^2-1/2*c^0+s^0+c^0*(-1+c^0), (-2+c^0 >= 0 /\ -2+d^0 >= 0 /\ -1+f^0 >= 0 /\ 253-(-2+c^0)*c^0+1/2*c^0-s^0+1/2*(-2+c^0)^2 >= 0 /\ -1-r^0+n^post16 >= 0), cost: -8+8*c^0
 179: l9 -> l9 : d^0'=2, n^0'=n^post16, c^0'=1, s^0'=1/2-1/2*(-1+c^0)^2-1/2*c^0+s^0+c^0*(-1+c^0), (-2+c^0 >= 0 /\ -2+d^0 >= 0 /\ 253-(-2+c^0)*c^0+1/2*c^0-s^0+1/2*(-2+c^0)^2 >= 0 /\ 1+f^0 <= 0 /\ -1-r^0+n^post16 >= 0), cost: -8+8*c^0
 180: l9 -> [18] : (-1+n26 >= 0 /\ 255-c^0-s^0 >= 0 /\ -2+d^0 >= 0 /\ -1-r^0+n^post16 >= 0 /\ -c^0 >= 0 /\ f^0 <= 0 /\ f^0 >= 0), cost: NONTERM
 181: l9 -> [18] : (-2+d^0 >= 0 /\ -1+f^0 >= 0 /\ c^0 <= 0 /\ -1-r^0+n^post16 >= 0 /\ -1+n29 >= 0 /\ 256-c^0-s^0 >= 0), cost: NONTERM
 182: l9 -> [18] : (-1+n32 >= 0 /\ -2+d^0 >= 0 /\ c^0 <= 0 /\ 1+f^0 <= 0 /\ -1-r^0+n^post16 >= 0 /\ 256-c^0-s^0 >= 0), cost: NONTERM
  61: l17 -> l9 : d^0'=0, c^0'=4, f^0'=0, TRUE, cost: 2


Applied chaining
First rule:
l17 -> l9 : d^0'=0, c^0'=4, f^0'=0, TRUE, cost: 2
Second rule:
l9 -> l9 : d^0'=2, n^0'=n^post16, s^0'=c^0+s^0, (-2+c^0 >= 0 /\ d^0 <= 0 /\ 1+r^0-n^post16 <= 0 /\ -255+c^0+s^0 <= 0 /\ f^0 == 0), cost: 7
New rule:
l17 -> l9 : d^0'=2, n^0'=n^post16, c^0'=4, s^0'=4+s^0, f^0'=0, (1+r^0-n^post16 <= 0 /\ -251+s^0 <= 0), cost: 9

Applied chaining
First rule:
l17 -> l9 : d^0'=0, c^0'=4, f^0'=0, TRUE, cost: 2
Second rule:
l9 -> l9 : d^0'=1, n^0'=n^post16, s^0'=s^0-n0*c^0, (-1+n0 >= 0 /\ -2+c^0 >= 0 /\ -(-1+n0)*c^0-c^0+s^0 >= 0 /\ -1+d^0 <= 0 /\ f^0 <= 0 /\ f^0 >= 0 /\ -1+r^0-n^post16 >= 0), cost: 8*n0
New rule:
l17 -> l9 : d^0'=1, n^0'=n^post16, c^0'=4, s^0'=-4*n0+s^0, f^0'=0, (-1+n0 >= 0 /\ -4*n0+s^0 >= 0 /\ -1+r^0-n^post16 >= 0), cost: 2+8*n0

Applied deletion
Removed the following rules: 123 125 126 128 129 131 132 134 135 137 138 140 142 143 145 146 148 149 151 152 154 155 157 158 171 172 173 174 175 176 177 178 179 180 181 182

Chained accelerated rules with incoming rules
Start location: l17
  61: l17 -> l9 : d^0'=0, c^0'=4, f^0'=0, TRUE, cost: 2
 183: l17 -> l9 : d^0'=2, n^0'=n^post16, c^0'=4, s^0'=4+s^0, f^0'=0, (1+r^0-n^post16 <= 0 /\ -251+s^0 <= 0), cost: 9
 184: l17 -> l9 : d^0'=1, n^0'=n^post16, c^0'=4, s^0'=-4*n0+s^0, f^0'=0, (-1+n0 >= 0 /\ -4*n0+s^0 >= 0 /\ -1+r^0-n^post16 >= 0), cost: 2+8*n0


Removed unreachable locations and irrelevant leafs
Start location: l17
  <empty>


Computing asymptotic complexity

Proved the following lower bound
Complexity:  Unknown
Cpx degree: ?

Solved cost: 0
Rule cost:   0