unknown

Initial ITS

Start location: l18
Program variables: i11^0 i13^0 i15^0 i17^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0
   0: l0 -> l1 : i11^0'=i11^post1, i13^0'=i13^post1, i15^0'=i15^post1, i17^0'=i17^post1, i7^0'=i7^post1, i9^0'=i9^post1, i^0'=i^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (i11^0-i11^post1 == 0 /\ -i9^post1+i9^0 == 0 /\ i13^0-i13^post1 == 0 /\ -i15^post1+i15^0 == 0 /\ -i^post1+i^0 == 0 /\ i7^0-i7^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ i17^0-i17^post1 == 0), cost: 1
  22: l1 -> l5 : i11^0'=i11^post23, i13^0'=i13^post23, i15^0'=i15^post23, i17^0'=i17^post23, i7^0'=i7^post23, i9^0'=i9^post23, i^0'=i^post23, tmp^0'=tmp^post23, tmp___0^0'=tmp___0^post23, (-tmp___0^post23+tmp___0^0 == 0 /\ i13^0-i13^post23 == 0 /\ i9^post23 == 0 /\ i9^1 == 0 /\ 50-i7^0 <= 0 /\ i11^0-i11^post23 == 0 /\ tmp^0-tmp^post23 == 0 /\ -i^post23+i^0 == 0 /\ -i15^post23+i15^0 == 0 /\ i7^0-i7^post23 == 0 /\ i17^0-i17^post23 == 0), cost: 1
  23: l1 -> l0 : i11^0'=i11^post24, i13^0'=i13^post24, i15^0'=i15^post24, i17^0'=i17^post24, i7^0'=i7^post24, i9^0'=i9^post24, i^0'=i^post24, tmp^0'=tmp^post24, tmp___0^0'=tmp___0^post24, (-i^post24+i^0 == 0 /\ -i15^post24+i15^0 == 0 /\ -i13^post24+i13^0 == 0 /\ i9^0-i9^post24 == 0 /\ i17^0-i17^post24 == 0 /\ tmp^0-tmp^post24 == 0 /\ tmp___0^0-tmp___0^post24 == 0 /\ i11^0-i11^post24 == 0 /\ -1+i7^post24-i7^0 == 0 /\ -49+i7^0 <= 0), cost: 1
   1: l2 -> l3 : i11^0'=i11^post2, i13^0'=i13^post2, i15^0'=i15^post2, i17^0'=i17^post2, i7^0'=i7^post2, i9^0'=i9^post2, i^0'=i^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (tmp___0^0-tmp___0^post2 == 0 /\ i9^0-i9^post2 == 0 /\ i17^0-i17^post2 == 0 /\ -i13^post2+i13^0 == 0 /\ 50-i^0 <= 0 /\ i11^0-i11^post2 == 0 /\ i15^0-i15^post2 == 0 /\ -i7^post2+i7^0 == 0 /\ -i^post2+i^0 == 0 /\ tmp^0-tmp^post2 == 0), cost: 1
   2: l2 -> l4 : i11^0'=i11^post3, i13^0'=i13^post3, i15^0'=i15^post3, i17^0'=i17^post3, i7^0'=i7^post3, i9^0'=i9^post3, i^0'=i^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (i15^0-i15^post3 == 0 /\ -i17^post3+i17^0 == 0 /\ -i13^post3+i13^0 == 0 /\ -49+i^0 <= 0 /\ tmp^0-tmp^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ i9^0-i9^post3 == 0 /\ -1-i^0+i^post3 == 0 /\ -i11^post3+i11^0 == 0 /\ -i7^post3+i7^0 == 0), cost: 1
  21: l4 -> l2 : i11^0'=i11^post22, i13^0'=i13^post22, i15^0'=i15^post22, i17^0'=i17^post22, i7^0'=i7^post22, i9^0'=i9^post22, i^0'=i^post22, tmp^0'=tmp^post22, tmp___0^0'=tmp___0^post22, (i11^0-i11^post22 == 0 /\ i13^0-i13^post22 == 0 /\ -i15^post22+i15^0 == 0 /\ -tmp___0^post22+tmp___0^0 == 0 /\ -i9^post22+i9^0 == 0 /\ -i^post22+i^0 == 0 /\ tmp^0-tmp^post22 == 0 /\ i7^0-i7^post22 == 0 /\ i17^0-i17^post22 == 0), cost: 1
   3: l5 -> l6 : i11^0'=i11^post4, i13^0'=i13^post4, i15^0'=i15^post4, i17^0'=i17^post4, i7^0'=i7^post4, i9^0'=i9^post4, i^0'=i^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (i17^0-i17^post4 == 0 /\ i15^0-i15^post4 == 0 /\ -i7^post4+i7^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ i^0-i^post4 == 0 /\ i11^0-i11^post4 == 0 /\ -tmp___0^post4+tmp___0^0 == 0 /\ -i13^post4+i13^0 == 0 /\ i9^0-i9^post4 == 0), cost: 1
  19: l6 -> l9 : i11^0'=i11^post20, i13^0'=i13^post20, i15^0'=i15^post20, i17^0'=i17^post20, i7^0'=i7^post20, i9^0'=i9^post20, i^0'=i^post20, tmp^0'=tmp^post20, tmp___0^0'=tmp___0^post20, (50-i9^0 <= 0 /\ i17^0-i17^post20 == 0 /\ tmp^0-tmp^post20 == 0 /\ i^0-i^post20 == 0 /\ i15^0-i15^post20 == 0 /\ -i7^post20+i7^0 == 0 /\ i11^1 == 0 /\ i9^0-i9^post20 == 0 /\ -i13^post20+i13^0 == 0 /\ -tmp___0^post20+tmp___0^0 == 0 /\ i11^post20 == 0), cost: 1
  20: l6 -> l5 : i11^0'=i11^post21, i13^0'=i13^post21, i15^0'=i15^post21, i17^0'=i17^post21, i7^0'=i7^post21, i9^0'=i9^post21, i^0'=i^post21, tmp^0'=tmp^post21, tmp___0^0'=tmp___0^post21, (-tmp___0^post21+tmp___0^0 == 0 /\ -tmp^post21+tmp^0 == 0 /\ i11^0-i11^post21 == 0 /\ i17^0-i17^post21 == 0 /\ i^0-i^post21 == 0 /\ -1-i9^0+i9^post21 == 0 /\ -i13^post21+i13^0 == 0 /\ -i15^post21+i15^0 == 0 /\ -49+i9^0 <= 0 /\ -i7^post21+i7^0 == 0), cost: 1
   4: l7 -> l4 : i11^0'=i11^post5, i13^0'=i13^post5, i15^0'=i15^post5, i17^0'=i17^post5, i7^0'=i7^post5, i9^0'=i9^post5, i^0'=i^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (-tmp___0^post5+tmp___0^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ 50-i17^0 <= 0 /\ i17^0-i17^post5 == 0 /\ -i7^post5+i7^0 == 0 /\ -i13^post5+i13^0 == 0 /\ -i9^post5+i9^0 == 0 /\ -i15^post5+i15^0 == 0 /\ i11^0-i11^post5 == 0 /\ i^post5 == 0), cost: 1
   5: l7 -> l8 : i11^0'=i11^post6, i13^0'=i13^post6, i15^0'=i15^post6, i17^0'=i17^post6, i7^0'=i7^post6, i9^0'=i9^post6, i^0'=i^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (i9^0-i9^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ -i7^post6+i7^0 == 0 /\ -i13^post6+i13^0 == 0 /\ -i15^post6+i15^0 == 0 /\ -tmp^post6+tmp^0 == 0 /\ -49+i17^0 <= 0 /\ i11^0-i11^post6 == 0 /\ i^0-i^post6 == 0 /\ -1-i17^0+i17^post6 == 0), cost: 1
  18: l8 -> l7 : i11^0'=i11^post19, i13^0'=i13^post19, i15^0'=i15^post19, i17^0'=i17^post19, i7^0'=i7^post19, i9^0'=i9^post19, i^0'=i^post19, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, (-tmp^post19+tmp^0 == 0 /\ -tmp___0^post19+tmp___0^0 == 0 /\ i17^0-i17^post19 == 0 /\ i9^0-i9^post19 == 0 /\ i11^0-i11^post19 == 0 /\ -i13^post19+i13^0 == 0 /\ -i15^post19+i15^0 == 0 /\ i^0-i^post19 == 0 /\ i7^0-i7^post19 == 0), cost: 1
   6: l9 -> l10 : i11^0'=i11^post7, i13^0'=i13^post7, i15^0'=i15^post7, i17^0'=i17^post7, i7^0'=i7^post7, i9^0'=i9^post7, i^0'=i^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (-i15^post7+i15^0 == 0 /\ i11^0-i11^post7 == 0 /\ i13^0-i13^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ -i9^post7+i9^0 == 0 /\ -i7^post7+i7^0 == 0 /\ i17^0-i17^post7 == 0 /\ -i^post7+i^0 == 0 /\ tmp^0-tmp^post7 == 0), cost: 1
  16: l10 -> l13 : i11^0'=i11^post17, i13^0'=i13^post17, i15^0'=i15^post17, i17^0'=i17^post17, i7^0'=i7^post17, i9^0'=i9^post17, i^0'=i^post17, tmp^0'=tmp^post17, tmp___0^0'=tmp___0^post17, (i9^0-i9^post17 == 0 /\ 50-i11^0 <= 0 /\ tmp^0-tmp^post17 == 0 /\ -i13^post17+i13^0 == 0 /\ i17^0-i17^post17 == 0 /\ -tmp___0^post17+tmp___0^0 == 0 /\ i^post17 == 0 /\ -i7^post17+i7^0 == 0 /\ -i15^post17+i15^0 == 0 /\ i11^0-i11^post17 == 0), cost: 1
  17: l10 -> l9 : i11^0'=i11^post18, i13^0'=i13^post18, i15^0'=i15^post18, i17^0'=i17^post18, i7^0'=i7^post18, i9^0'=i9^post18, i^0'=i^post18, tmp^0'=tmp^post18, tmp___0^0'=tmp___0^post18, (-i^post18+i^0 == 0 /\ -i15^post18+i15^0 == 0 /\ -1-i11^0+i11^post18 == 0 /\ i7^0-i7^post18 == 0 /\ i17^0-i17^post18 == 0 /\ -49+i11^0 <= 0 /\ -tmp___0^post18+tmp___0^0 == 0 /\ -i13^post18+i13^0 == 0 /\ -i9^post18+i9^0 == 0 /\ tmp^0-tmp^post18 == 0), cost: 1
   7: l11 -> l8 : i11^0'=i11^post8, i13^0'=i13^post8, i15^0'=i15^post8, i17^0'=i17^post8, i7^0'=i7^post8, i9^0'=i9^post8, i^0'=i^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (-tmp___0^post8+tmp___0^0 == 0 /\ -tmp^post8+tmp^0 == 0 /\ i9^0-i9^post8 == 0 /\ -i13^post8+i13^0 == 0 /\ i11^0-i11^post8 == 0 /\ i17^1 == 0 /\ i^0-i^post8 == 0 /\ i17^post8 == 0 /\ -i7^post8+i7^0 == 0 /\ -i15^post8+i15^0 == 0 /\ 50-i15^0 <= 0), cost: 1
   8: l11 -> l12 : i11^0'=i11^post9, i13^0'=i13^post9, i15^0'=i15^post9, i17^0'=i17^post9, i7^0'=i7^post9, i9^0'=i9^post9, i^0'=i^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, (i17^0-i17^post9 == 0 /\ -1+i15^post9-i15^0 == 0 /\ i11^0-i11^post9 == 0 /\ -49+i15^0 <= 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ tmp^0-tmp^post9 == 0 /\ -i13^post9+i13^0 == 0 /\ -i9^post9+i9^0 == 0 /\ -i^post9+i^0 == 0 /\ i7^0-i7^post9 == 0), cost: 1
  15: l12 -> l11 : i11^0'=i11^post16, i13^0'=i13^post16, i15^0'=i15^post16, i17^0'=i17^post16, i7^0'=i7^post16, i9^0'=i9^post16, i^0'=i^post16, tmp^0'=tmp^post16, tmp___0^0'=tmp___0^post16, (i^0-i^post16 == 0 /\ i15^0-i15^post16 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ -i17^post16+i17^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ -i13^post16+i13^0 == 0 /\ i9^0-i9^post16 == 0 /\ -i7^post16+i7^0 == 0 /\ -i11^post16+i11^0 == 0), cost: 1
   9: l13 -> l14 : i11^0'=i11^post10, i13^0'=i13^post10, i15^0'=i15^post10, i17^0'=i17^post10, i7^0'=i7^post10, i9^0'=i9^post10, i^0'=i^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, (tmp___0^0-tmp___0^post10 == 0 /\ i9^0-i9^post10 == 0 /\ i17^0-i17^post10 == 0 /\ -i13^post10+i13^0 == 0 /\ i15^0-i15^post10 == 0 /\ -i^post10+i^0 == 0 /\ -i7^post10+i7^0 == 0 /\ i11^0-i11^post10 == 0 /\ tmp^0-tmp^post10 == 0), cost: 1
  13: l14 -> l16 : i11^0'=i11^post14, i13^0'=i13^post14, i15^0'=i15^post14, i17^0'=i17^post14, i7^0'=i7^post14, i9^0'=i9^post14, i^0'=i^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, (-tmp___0^post14+tmp___0^0 == 0 /\ i13^1 == 0 /\ i11^0-i11^post14 == 0 /\ -i9^post14+i9^0 == 0 /\ 50-i^0 <= 0 /\ -i^post14+i^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ -i15^post14+i15^0 == 0 /\ i13^post14 == 0 /\ i7^0-i7^post14 == 0 /\ i17^0-i17^post14 == 0), cost: 1
  14: l14 -> l13 : i11^0'=i11^post15, i13^0'=i13^post15, i15^0'=i15^post15, i17^0'=i17^post15, i7^0'=i7^post15, i9^0'=i9^post15, i^0'=i^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, (i9^0-i9^post15 == 0 /\ -i13^post15+i13^0 == 0 /\ tmp^0-tmp^post15 == 0 /\ -i15^post15+i15^0 == 0 /\ -i7^post15+i7^0 == 0 /\ tmp___0^0-tmp___0^post15 == 0 /\ i17^0-i17^post15 == 0 /\ -49+i^0 <= 0 /\ i11^0-i11^post15 == 0 /\ -1+i^post15-i^0 == 0), cost: 1
  10: l15 -> l12 : i11^0'=i11^post11, i13^0'=i13^post11, i15^0'=i15^post11, i17^0'=i17^post11, i7^0'=i7^post11, i9^0'=i9^post11, i^0'=i^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, (50-i13^0 <= 0 /\ i17^0-i17^post11 == 0 /\ i15^post11 == 0 /\ i15^1 == 0 /\ i11^0-i11^post11 == 0 /\ -tmp___0^post11+tmp___0^0 == 0 /\ tmp^0-tmp^post11 == 0 /\ -i9^post11+i9^0 == 0 /\ -i13^post11+i13^0 == 0 /\ i7^0-i7^post11 == 0 /\ -i^post11+i^0 == 0), cost: 1
  11: l15 -> l16 : i11^0'=i11^post12, i13^0'=i13^post12, i15^0'=i15^post12, i17^0'=i17^post12, i7^0'=i7^post12, i9^0'=i9^post12, i^0'=i^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (-1+i13^post12-i13^0 == 0 /\ -i9^post12+i9^0 == 0 /\ -tmp___0^post12+tmp___0^0 == 0 /\ i17^0-i17^post12 == 0 /\ -i^post12+i^0 == 0 /\ -i7^post12+i7^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ i15^0-i15^post12 == 0 /\ i11^0-i11^post12 == 0 /\ -49+i13^0 <= 0), cost: 1
  12: l16 -> l15 : i11^0'=i11^post13, i13^0'=i13^post13, i15^0'=i15^post13, i17^0'=i17^post13, i7^0'=i7^post13, i9^0'=i9^post13, i^0'=i^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, (-i7^post13+i7^0 == 0 /\ -i15^post13+i15^0 == 0 /\ -i13^post13+i13^0 == 0 /\ i9^0-i9^post13 == 0 /\ tmp^0-tmp^post13 == 0 /\ i17^0-i17^post13 == 0 /\ tmp___0^0-tmp___0^post13 == 0 /\ -i^post13+i^0 == 0 /\ i11^0-i11^post13 == 0), cost: 1
  24: l17 -> l0 : i11^0'=i11^post25, i13^0'=i13^post25, i15^0'=i15^post25, i17^0'=i17^post25, i7^0'=i7^post25, i9^0'=i9^post25, i^0'=i^post25, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, (0 == 0 /\ i7^1 == 0 /\ i11^0-i11^post25 == 0 /\ -i9^post25+i9^0 == 0 /\ -i13^post25+i13^0 == 0 /\ i^post25 == 0 /\ i7^post25 == 0 /\ -i15^post25+i15^0 == 0 /\ i17^0-i17^post25 == 0), cost: 1
  25: l18 -> l17 : i11^0'=i11^post26, i13^0'=i13^post26, i15^0'=i15^post26, i17^0'=i17^post26, i7^0'=i7^post26, i9^0'=i9^post26, i^0'=i^post26, tmp^0'=tmp^post26, tmp___0^0'=tmp___0^post26, (-i7^post26+i7^0 == 0 /\ i9^0-i9^post26 == 0 /\ i17^0-i17^post26 == 0 /\ i^0-i^post26 == 0 /\ -tmp^post26+tmp^0 == 0 /\ -i13^post26+i13^0 == 0 /\ i15^0-i15^post26 == 0 /\ -tmp___0^post26+tmp___0^0 == 0 /\ i11^0-i11^post26 == 0), cost: 1

Chained Linear Paths

Start location: l18
Program variables: i11^0 i13^0 i15^0 i17^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0
   0: l0 -> l1 : i11^0'=i11^post1, i13^0'=i13^post1, i15^0'=i15^post1, i17^0'=i17^post1, i7^0'=i7^post1, i9^0'=i9^post1, i^0'=i^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (i11^0-i11^post1 == 0 /\ -i9^post1+i9^0 == 0 /\ i13^0-i13^post1 == 0 /\ -i15^post1+i15^0 == 0 /\ -i^post1+i^0 == 0 /\ i7^0-i7^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ i17^0-i17^post1 == 0), cost: 1
  22: l1 -> l5 : i11^0'=i11^post23, i13^0'=i13^post23, i15^0'=i15^post23, i17^0'=i17^post23, i7^0'=i7^post23, i9^0'=i9^post23, i^0'=i^post23, tmp^0'=tmp^post23, tmp___0^0'=tmp___0^post23, (-tmp___0^post23+tmp___0^0 == 0 /\ i13^0-i13^post23 == 0 /\ i9^post23 == 0 /\ i9^1 == 0 /\ 50-i7^0 <= 0 /\ i11^0-i11^post23 == 0 /\ tmp^0-tmp^post23 == 0 /\ -i^post23+i^0 == 0 /\ -i15^post23+i15^0 == 0 /\ i7^0-i7^post23 == 0 /\ i17^0-i17^post23 == 0), cost: 1
  23: l1 -> l0 : i11^0'=i11^post24, i13^0'=i13^post24, i15^0'=i15^post24, i17^0'=i17^post24, i7^0'=i7^post24, i9^0'=i9^post24, i^0'=i^post24, tmp^0'=tmp^post24, tmp___0^0'=tmp___0^post24, (-i^post24+i^0 == 0 /\ -i15^post24+i15^0 == 0 /\ -i13^post24+i13^0 == 0 /\ i9^0-i9^post24 == 0 /\ i17^0-i17^post24 == 0 /\ tmp^0-tmp^post24 == 0 /\ tmp___0^0-tmp___0^post24 == 0 /\ i11^0-i11^post24 == 0 /\ -1+i7^post24-i7^0 == 0 /\ -49+i7^0 <= 0), cost: 1
   1: l2 -> l3 : i11^0'=i11^post2, i13^0'=i13^post2, i15^0'=i15^post2, i17^0'=i17^post2, i7^0'=i7^post2, i9^0'=i9^post2, i^0'=i^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (tmp___0^0-tmp___0^post2 == 0 /\ i9^0-i9^post2 == 0 /\ i17^0-i17^post2 == 0 /\ -i13^post2+i13^0 == 0 /\ 50-i^0 <= 0 /\ i11^0-i11^post2 == 0 /\ i15^0-i15^post2 == 0 /\ -i7^post2+i7^0 == 0 /\ -i^post2+i^0 == 0 /\ tmp^0-tmp^post2 == 0), cost: 1
   2: l2 -> l4 : i11^0'=i11^post3, i13^0'=i13^post3, i15^0'=i15^post3, i17^0'=i17^post3, i7^0'=i7^post3, i9^0'=i9^post3, i^0'=i^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (i15^0-i15^post3 == 0 /\ -i17^post3+i17^0 == 0 /\ -i13^post3+i13^0 == 0 /\ -49+i^0 <= 0 /\ tmp^0-tmp^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ i9^0-i9^post3 == 0 /\ -1-i^0+i^post3 == 0 /\ -i11^post3+i11^0 == 0 /\ -i7^post3+i7^0 == 0), cost: 1
  21: l4 -> l2 : i11^0'=i11^post22, i13^0'=i13^post22, i15^0'=i15^post22, i17^0'=i17^post22, i7^0'=i7^post22, i9^0'=i9^post22, i^0'=i^post22, tmp^0'=tmp^post22, tmp___0^0'=tmp___0^post22, (i11^0-i11^post22 == 0 /\ i13^0-i13^post22 == 0 /\ -i15^post22+i15^0 == 0 /\ -tmp___0^post22+tmp___0^0 == 0 /\ -i9^post22+i9^0 == 0 /\ -i^post22+i^0 == 0 /\ tmp^0-tmp^post22 == 0 /\ i7^0-i7^post22 == 0 /\ i17^0-i17^post22 == 0), cost: 1
   3: l5 -> l6 : i11^0'=i11^post4, i13^0'=i13^post4, i15^0'=i15^post4, i17^0'=i17^post4, i7^0'=i7^post4, i9^0'=i9^post4, i^0'=i^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (i17^0-i17^post4 == 0 /\ i15^0-i15^post4 == 0 /\ -i7^post4+i7^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ i^0-i^post4 == 0 /\ i11^0-i11^post4 == 0 /\ -tmp___0^post4+tmp___0^0 == 0 /\ -i13^post4+i13^0 == 0 /\ i9^0-i9^post4 == 0), cost: 1
  19: l6 -> l9 : i11^0'=i11^post20, i13^0'=i13^post20, i15^0'=i15^post20, i17^0'=i17^post20, i7^0'=i7^post20, i9^0'=i9^post20, i^0'=i^post20, tmp^0'=tmp^post20, tmp___0^0'=tmp___0^post20, (50-i9^0 <= 0 /\ i17^0-i17^post20 == 0 /\ tmp^0-tmp^post20 == 0 /\ i^0-i^post20 == 0 /\ i15^0-i15^post20 == 0 /\ -i7^post20+i7^0 == 0 /\ i11^1 == 0 /\ i9^0-i9^post20 == 0 /\ -i13^post20+i13^0 == 0 /\ -tmp___0^post20+tmp___0^0 == 0 /\ i11^post20 == 0), cost: 1
  20: l6 -> l5 : i11^0'=i11^post21, i13^0'=i13^post21, i15^0'=i15^post21, i17^0'=i17^post21, i7^0'=i7^post21, i9^0'=i9^post21, i^0'=i^post21, tmp^0'=tmp^post21, tmp___0^0'=tmp___0^post21, (-tmp___0^post21+tmp___0^0 == 0 /\ -tmp^post21+tmp^0 == 0 /\ i11^0-i11^post21 == 0 /\ i17^0-i17^post21 == 0 /\ i^0-i^post21 == 0 /\ -1-i9^0+i9^post21 == 0 /\ -i13^post21+i13^0 == 0 /\ -i15^post21+i15^0 == 0 /\ -49+i9^0 <= 0 /\ -i7^post21+i7^0 == 0), cost: 1
   4: l7 -> l4 : i11^0'=i11^post5, i13^0'=i13^post5, i15^0'=i15^post5, i17^0'=i17^post5, i7^0'=i7^post5, i9^0'=i9^post5, i^0'=i^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (-tmp___0^post5+tmp___0^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ 50-i17^0 <= 0 /\ i17^0-i17^post5 == 0 /\ -i7^post5+i7^0 == 0 /\ -i13^post5+i13^0 == 0 /\ -i9^post5+i9^0 == 0 /\ -i15^post5+i15^0 == 0 /\ i11^0-i11^post5 == 0 /\ i^post5 == 0), cost: 1
   5: l7 -> l8 : i11^0'=i11^post6, i13^0'=i13^post6, i15^0'=i15^post6, i17^0'=i17^post6, i7^0'=i7^post6, i9^0'=i9^post6, i^0'=i^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (i9^0-i9^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ -i7^post6+i7^0 == 0 /\ -i13^post6+i13^0 == 0 /\ -i15^post6+i15^0 == 0 /\ -tmp^post6+tmp^0 == 0 /\ -49+i17^0 <= 0 /\ i11^0-i11^post6 == 0 /\ i^0-i^post6 == 0 /\ -1-i17^0+i17^post6 == 0), cost: 1
  18: l8 -> l7 : i11^0'=i11^post19, i13^0'=i13^post19, i15^0'=i15^post19, i17^0'=i17^post19, i7^0'=i7^post19, i9^0'=i9^post19, i^0'=i^post19, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, (-tmp^post19+tmp^0 == 0 /\ -tmp___0^post19+tmp___0^0 == 0 /\ i17^0-i17^post19 == 0 /\ i9^0-i9^post19 == 0 /\ i11^0-i11^post19 == 0 /\ -i13^post19+i13^0 == 0 /\ -i15^post19+i15^0 == 0 /\ i^0-i^post19 == 0 /\ i7^0-i7^post19 == 0), cost: 1
   6: l9 -> l10 : i11^0'=i11^post7, i13^0'=i13^post7, i15^0'=i15^post7, i17^0'=i17^post7, i7^0'=i7^post7, i9^0'=i9^post7, i^0'=i^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (-i15^post7+i15^0 == 0 /\ i11^0-i11^post7 == 0 /\ i13^0-i13^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ -i9^post7+i9^0 == 0 /\ -i7^post7+i7^0 == 0 /\ i17^0-i17^post7 == 0 /\ -i^post7+i^0 == 0 /\ tmp^0-tmp^post7 == 0), cost: 1
  16: l10 -> l13 : i11^0'=i11^post17, i13^0'=i13^post17, i15^0'=i15^post17, i17^0'=i17^post17, i7^0'=i7^post17, i9^0'=i9^post17, i^0'=i^post17, tmp^0'=tmp^post17, tmp___0^0'=tmp___0^post17, (i9^0-i9^post17 == 0 /\ 50-i11^0 <= 0 /\ tmp^0-tmp^post17 == 0 /\ -i13^post17+i13^0 == 0 /\ i17^0-i17^post17 == 0 /\ -tmp___0^post17+tmp___0^0 == 0 /\ i^post17 == 0 /\ -i7^post17+i7^0 == 0 /\ -i15^post17+i15^0 == 0 /\ i11^0-i11^post17 == 0), cost: 1
  17: l10 -> l9 : i11^0'=i11^post18, i13^0'=i13^post18, i15^0'=i15^post18, i17^0'=i17^post18, i7^0'=i7^post18, i9^0'=i9^post18, i^0'=i^post18, tmp^0'=tmp^post18, tmp___0^0'=tmp___0^post18, (-i^post18+i^0 == 0 /\ -i15^post18+i15^0 == 0 /\ -1-i11^0+i11^post18 == 0 /\ i7^0-i7^post18 == 0 /\ i17^0-i17^post18 == 0 /\ -49+i11^0 <= 0 /\ -tmp___0^post18+tmp___0^0 == 0 /\ -i13^post18+i13^0 == 0 /\ -i9^post18+i9^0 == 0 /\ tmp^0-tmp^post18 == 0), cost: 1
   7: l11 -> l8 : i11^0'=i11^post8, i13^0'=i13^post8, i15^0'=i15^post8, i17^0'=i17^post8, i7^0'=i7^post8, i9^0'=i9^post8, i^0'=i^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (-tmp___0^post8+tmp___0^0 == 0 /\ -tmp^post8+tmp^0 == 0 /\ i9^0-i9^post8 == 0 /\ -i13^post8+i13^0 == 0 /\ i11^0-i11^post8 == 0 /\ i17^1 == 0 /\ i^0-i^post8 == 0 /\ i17^post8 == 0 /\ -i7^post8+i7^0 == 0 /\ -i15^post8+i15^0 == 0 /\ 50-i15^0 <= 0), cost: 1
   8: l11 -> l12 : i11^0'=i11^post9, i13^0'=i13^post9, i15^0'=i15^post9, i17^0'=i17^post9, i7^0'=i7^post9, i9^0'=i9^post9, i^0'=i^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, (i17^0-i17^post9 == 0 /\ -1+i15^post9-i15^0 == 0 /\ i11^0-i11^post9 == 0 /\ -49+i15^0 <= 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ tmp^0-tmp^post9 == 0 /\ -i13^post9+i13^0 == 0 /\ -i9^post9+i9^0 == 0 /\ -i^post9+i^0 == 0 /\ i7^0-i7^post9 == 0), cost: 1
  15: l12 -> l11 : i11^0'=i11^post16, i13^0'=i13^post16, i15^0'=i15^post16, i17^0'=i17^post16, i7^0'=i7^post16, i9^0'=i9^post16, i^0'=i^post16, tmp^0'=tmp^post16, tmp___0^0'=tmp___0^post16, (i^0-i^post16 == 0 /\ i15^0-i15^post16 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ -i17^post16+i17^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ -i13^post16+i13^0 == 0 /\ i9^0-i9^post16 == 0 /\ -i7^post16+i7^0 == 0 /\ -i11^post16+i11^0 == 0), cost: 1
   9: l13 -> l14 : i11^0'=i11^post10, i13^0'=i13^post10, i15^0'=i15^post10, i17^0'=i17^post10, i7^0'=i7^post10, i9^0'=i9^post10, i^0'=i^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, (tmp___0^0-tmp___0^post10 == 0 /\ i9^0-i9^post10 == 0 /\ i17^0-i17^post10 == 0 /\ -i13^post10+i13^0 == 0 /\ i15^0-i15^post10 == 0 /\ -i^post10+i^0 == 0 /\ -i7^post10+i7^0 == 0 /\ i11^0-i11^post10 == 0 /\ tmp^0-tmp^post10 == 0), cost: 1
  13: l14 -> l16 : i11^0'=i11^post14, i13^0'=i13^post14, i15^0'=i15^post14, i17^0'=i17^post14, i7^0'=i7^post14, i9^0'=i9^post14, i^0'=i^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, (-tmp___0^post14+tmp___0^0 == 0 /\ i13^1 == 0 /\ i11^0-i11^post14 == 0 /\ -i9^post14+i9^0 == 0 /\ 50-i^0 <= 0 /\ -i^post14+i^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ -i15^post14+i15^0 == 0 /\ i13^post14 == 0 /\ i7^0-i7^post14 == 0 /\ i17^0-i17^post14 == 0), cost: 1
  14: l14 -> l13 : i11^0'=i11^post15, i13^0'=i13^post15, i15^0'=i15^post15, i17^0'=i17^post15, i7^0'=i7^post15, i9^0'=i9^post15, i^0'=i^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, (i9^0-i9^post15 == 0 /\ -i13^post15+i13^0 == 0 /\ tmp^0-tmp^post15 == 0 /\ -i15^post15+i15^0 == 0 /\ -i7^post15+i7^0 == 0 /\ tmp___0^0-tmp___0^post15 == 0 /\ i17^0-i17^post15 == 0 /\ -49+i^0 <= 0 /\ i11^0-i11^post15 == 0 /\ -1+i^post15-i^0 == 0), cost: 1
  10: l15 -> l12 : i11^0'=i11^post11, i13^0'=i13^post11, i15^0'=i15^post11, i17^0'=i17^post11, i7^0'=i7^post11, i9^0'=i9^post11, i^0'=i^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, (50-i13^0 <= 0 /\ i17^0-i17^post11 == 0 /\ i15^post11 == 0 /\ i15^1 == 0 /\ i11^0-i11^post11 == 0 /\ -tmp___0^post11+tmp___0^0 == 0 /\ tmp^0-tmp^post11 == 0 /\ -i9^post11+i9^0 == 0 /\ -i13^post11+i13^0 == 0 /\ i7^0-i7^post11 == 0 /\ -i^post11+i^0 == 0), cost: 1
  11: l15 -> l16 : i11^0'=i11^post12, i13^0'=i13^post12, i15^0'=i15^post12, i17^0'=i17^post12, i7^0'=i7^post12, i9^0'=i9^post12, i^0'=i^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (-1+i13^post12-i13^0 == 0 /\ -i9^post12+i9^0 == 0 /\ -tmp___0^post12+tmp___0^0 == 0 /\ i17^0-i17^post12 == 0 /\ -i^post12+i^0 == 0 /\ -i7^post12+i7^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ i15^0-i15^post12 == 0 /\ i11^0-i11^post12 == 0 /\ -49+i13^0 <= 0), cost: 1
  12: l16 -> l15 : i11^0'=i11^post13, i13^0'=i13^post13, i15^0'=i15^post13, i17^0'=i17^post13, i7^0'=i7^post13, i9^0'=i9^post13, i^0'=i^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, (-i7^post13+i7^0 == 0 /\ -i15^post13+i15^0 == 0 /\ -i13^post13+i13^0 == 0 /\ i9^0-i9^post13 == 0 /\ tmp^0-tmp^post13 == 0 /\ i17^0-i17^post13 == 0 /\ tmp___0^0-tmp___0^post13 == 0 /\ -i^post13+i^0 == 0 /\ i11^0-i11^post13 == 0), cost: 1
  26: l18 -> l0 : i11^0'=i11^post25, i13^0'=i13^post25, i15^0'=i15^post25, i17^0'=i17^post25, i7^0'=i7^post25, i9^0'=i9^post25, i^0'=i^post25, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, (0 == 0 /\ -i15^post25+i15^post26 == 0 /\ -i7^post26+i7^0 == 0 /\ i9^0-i9^post26 == 0 /\ i13^post26-i13^post25 == 0 /\ i11^post26-i11^post25 == 0 /\ i17^0-i17^post26 == 0 /\ i^0-i^post26 == 0 /\ i7^1 == 0 /\ -tmp^post26+tmp^0 == 0 /\ -i13^post26+i13^0 == 0 /\ -i9^post25+i9^post26 == 0 /\ i^post25 == 0 /\ i15^0-i15^post26 == 0 /\ -i17^post25+i17^post26 == 0 /\ -tmp___0^post26+tmp___0^0 == 0 /\ i7^post25 == 0 /\ i11^0-i11^post26 == 0), cost: 1

	Eliminating location l17 by chaining:

	Applied chaining

	First rule:
	l18 -> l17 : i11^0'=i11^post26, i13^0'=i13^post26, i15^0'=i15^post26, i17^0'=i17^post26, i7^0'=i7^post26, i9^0'=i9^post26, i^0'=i^post26, tmp^0'=tmp^post26, tmp___0^0'=tmp___0^post26, (-i7^post26+i7^0 == 0 /\ i9^0-i9^post26 == 0 /\ i17^0-i17^post26 == 0 /\ i^0-i^post26 == 0 /\ -tmp^post26+tmp^0 == 0 /\ -i13^post26+i13^0 == 0 /\ i15^0-i15^post26 == 0 /\ -tmp___0^post26+tmp___0^0 == 0 /\ i11^0-i11^post26 == 0), cost: 1
	Second rule:
	l17 -> l0 : i11^0'=i11^post25, i13^0'=i13^post25, i15^0'=i15^post25, i17^0'=i17^post25, i7^0'=i7^post25, i9^0'=i9^post25, i^0'=i^post25, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, (0 == 0 /\ i7^1 == 0 /\ i11^0-i11^post25 == 0 /\ -i9^post25+i9^0 == 0 /\ -i13^post25+i13^0 == 0 /\ i^post25 == 0 /\ i7^post25 == 0 /\ -i15^post25+i15^0 == 0 /\ i17^0-i17^post25 == 0), cost: 1
	New rule:
	l18 -> l0 : i11^0'=i11^post25, i13^0'=i13^post25, i15^0'=i15^post25, i17^0'=i17^post25, i7^0'=i7^post25, i9^0'=i9^post25, i^0'=i^post25, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, (0 == 0 /\ -i15^post25+i15^post26 == 0 /\ -i7^post26+i7^0 == 0 /\ i9^0-i9^post26 == 0 /\ i13^post26-i13^post25 == 0 /\ i11^post26-i11^post25 == 0 /\ i17^0-i17^post26 == 0 /\ i^0-i^post26 == 0 /\ i7^1 == 0 /\ -tmp^post26+tmp^0 == 0 /\ -i13^post26+i13^0 == 0 /\ -i9^post25+i9^post26 == 0 /\ i^post25 == 0 /\ i15^0-i15^post26 == 0 /\ -i17^post25+i17^post26 == 0 /\ -tmp___0^post26+tmp___0^0 == 0 /\ i7^post25 == 0 /\ i11^0-i11^post26 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 24 25

Simplified Transitions

Start location: l18
Program variables: i11^0 i13^0 i15^0 i17^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0
  27: l0 -> l1 : T, cost: 1
  49: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1
  50: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1
  28: l2 -> l3 : 50-i^0 <= 0, cost: 1
  29: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  48: l4 -> l2 : T, cost: 1
  30: l5 -> l6 : T, cost: 1
  46: l6 -> l9 : i11^0'=0, 50-i9^0 <= 0, cost: 1
  47: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1
  31: l7 -> l4 : i^0'=0, 50-i17^0 <= 0, cost: 1
  32: l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1
  45: l8 -> l7 : T, cost: 1
  33: l9 -> l10 : T, cost: 1
  43: l10 -> l13 : i^0'=0, 50-i11^0 <= 0, cost: 1
  44: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1
  34: l11 -> l8 : i17^0'=0, 50-i15^0 <= 0, cost: 1
  35: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1
  42: l12 -> l11 : T, cost: 1
  36: l13 -> l14 : T, cost: 1
  40: l14 -> l16 : i13^0'=0, 50-i^0 <= 0, cost: 1
  41: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  37: l15 -> l12 : i15^0'=0, 50-i13^0 <= 0, cost: 1
  38: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1
  39: l16 -> l15 : T, cost: 1
  51: l18 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, T, cost: 1

	Propagated Equalities

	Original rule:
	l0 -> l1 : i11^0'=i11^post1, i13^0'=i13^post1, i15^0'=i15^post1, i17^0'=i17^post1, i7^0'=i7^post1, i9^0'=i9^post1, i^0'=i^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (i11^0-i11^post1 == 0 /\ -i9^post1+i9^0 == 0 /\ i13^0-i13^post1 == 0 /\ -i15^post1+i15^0 == 0 /\ -i^post1+i^0 == 0 /\ i7^0-i7^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ i17^0-i17^post1 == 0), cost: 1
	New rule:
	l0 -> l1 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	
		propagated equality i11^post1 = i11^0
		
		propagated equality i9^post1 = i9^0
		
		propagated equality i13^post1 = i13^0
		
		propagated equality i15^post1 = i15^0
		
		propagated equality i^post1 = i^0
		
		propagated equality i7^post1 = i7^0
		
		propagated equality tmp^post1 = tmp^0
		
		propagated equality tmp___0^post1 = tmp___0^0
		
		propagated equality i17^post1 = i17^0
		
	Simplified Guard

	Original rule:
	l0 -> l1 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	New rule:
	l0 -> l1 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l1 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	New rule:
	l0 -> l1 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l3 : i11^0'=i11^post2, i13^0'=i13^post2, i15^0'=i15^post2, i17^0'=i17^post2, i7^0'=i7^post2, i9^0'=i9^post2, i^0'=i^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (tmp___0^0-tmp___0^post2 == 0 /\ i9^0-i9^post2 == 0 /\ i17^0-i17^post2 == 0 /\ -i13^post2+i13^0 == 0 /\ 50-i^0 <= 0 /\ i11^0-i11^post2 == 0 /\ i15^0-i15^post2 == 0 /\ -i7^post2+i7^0 == 0 /\ -i^post2+i^0 == 0 /\ tmp^0-tmp^post2 == 0), cost: 1
	New rule:
	l2 -> l3 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i^0 <= 0), cost: 1
	
		propagated equality tmp___0^post2 = tmp___0^0
		
		propagated equality i9^post2 = i9^0
		
		propagated equality i17^post2 = i17^0
		
		propagated equality i13^post2 = i13^0
		
		propagated equality i11^post2 = i11^0
		
		propagated equality i15^post2 = i15^0
		
		propagated equality i7^post2 = i7^0
		
		propagated equality i^post2 = i^0
		
		propagated equality tmp^post2 = tmp^0
		
	Simplified Guard

	Original rule:
	l2 -> l3 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i^0 <= 0), cost: 1
	New rule:
	l2 -> l3 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l3 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i^0 <= 0, cost: 1
	New rule:
	l2 -> l3 : 50-i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l4 : i11^0'=i11^post3, i13^0'=i13^post3, i15^0'=i15^post3, i17^0'=i17^post3, i7^0'=i7^post3, i9^0'=i9^post3, i^0'=i^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (i15^0-i15^post3 == 0 /\ -i17^post3+i17^0 == 0 /\ -i13^post3+i13^0 == 0 /\ -49+i^0 <= 0 /\ tmp^0-tmp^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ i9^0-i9^post3 == 0 /\ -1-i^0+i^post3 == 0 /\ -i11^post3+i11^0 == 0 /\ -i7^post3+i7^0 == 0), cost: 1
	New rule:
	l2 -> l4 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=1+i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i^0 <= 0), cost: 1
	
		propagated equality i15^post3 = i15^0
		
		propagated equality i17^post3 = i17^0
		
		propagated equality i13^post3 = i13^0
		
		propagated equality tmp^post3 = tmp^0
		
		propagated equality tmp___0^post3 = tmp___0^0
		
		propagated equality i9^post3 = i9^0
		
		propagated equality i^post3 = 1+i^0
		
		propagated equality i11^post3 = i11^0
		
		propagated equality i7^post3 = i7^0
		
	Simplified Guard

	Original rule:
	l2 -> l4 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=1+i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i^0 <= 0), cost: 1
	New rule:
	l2 -> l4 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=1+i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l4 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=1+i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i^0 <= 0, cost: 1
	New rule:
	l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l5 -> l6 : i11^0'=i11^post4, i13^0'=i13^post4, i15^0'=i15^post4, i17^0'=i17^post4, i7^0'=i7^post4, i9^0'=i9^post4, i^0'=i^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (i17^0-i17^post4 == 0 /\ i15^0-i15^post4 == 0 /\ -i7^post4+i7^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ i^0-i^post4 == 0 /\ i11^0-i11^post4 == 0 /\ -tmp___0^post4+tmp___0^0 == 0 /\ -i13^post4+i13^0 == 0 /\ i9^0-i9^post4 == 0), cost: 1
	New rule:
	l5 -> l6 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	
		propagated equality i17^post4 = i17^0
		
		propagated equality i15^post4 = i15^0
		
		propagated equality i7^post4 = i7^0
		
		propagated equality tmp^post4 = tmp^0
		
		propagated equality i^post4 = i^0
		
		propagated equality i11^post4 = i11^0
		
		propagated equality tmp___0^post4 = tmp___0^0
		
		propagated equality i13^post4 = i13^0
		
		propagated equality i9^post4 = i9^0
		
	Simplified Guard

	Original rule:
	l5 -> l6 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	New rule:
	l5 -> l6 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l5 -> l6 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	New rule:
	l5 -> l6 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l4 : i11^0'=i11^post5, i13^0'=i13^post5, i15^0'=i15^post5, i17^0'=i17^post5, i7^0'=i7^post5, i9^0'=i9^post5, i^0'=i^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (-tmp___0^post5+tmp___0^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ 50-i17^0 <= 0 /\ i17^0-i17^post5 == 0 /\ -i7^post5+i7^0 == 0 /\ -i13^post5+i13^0 == 0 /\ -i9^post5+i9^0 == 0 /\ -i15^post5+i15^0 == 0 /\ i11^0-i11^post5 == 0 /\ i^post5 == 0), cost: 1
	New rule:
	l7 -> l4 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i17^0 <= 0), cost: 1
	
		propagated equality tmp___0^post5 = tmp___0^0
		
		propagated equality tmp^post5 = tmp^0
		
		propagated equality i17^post5 = i17^0
		
		propagated equality i7^post5 = i7^0
		
		propagated equality i13^post5 = i13^0
		
		propagated equality i9^post5 = i9^0
		
		propagated equality i15^post5 = i15^0
		
		propagated equality i11^post5 = i11^0
		
		propagated equality i^post5 = 0
		
	Simplified Guard

	Original rule:
	l7 -> l4 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i17^0 <= 0), cost: 1
	New rule:
	l7 -> l4 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i17^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l7 -> l4 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i17^0 <= 0, cost: 1
	New rule:
	l7 -> l4 : i^0'=0, 50-i17^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l8 : i11^0'=i11^post6, i13^0'=i13^post6, i15^0'=i15^post6, i17^0'=i17^post6, i7^0'=i7^post6, i9^0'=i9^post6, i^0'=i^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (i9^0-i9^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ -i7^post6+i7^0 == 0 /\ -i13^post6+i13^0 == 0 /\ -i15^post6+i15^0 == 0 /\ -tmp^post6+tmp^0 == 0 /\ -49+i17^0 <= 0 /\ i11^0-i11^post6 == 0 /\ i^0-i^post6 == 0 /\ -1-i17^0+i17^post6 == 0), cost: 1
	New rule:
	l7 -> l8 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=1+i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i17^0 <= 0), cost: 1
	
		propagated equality i9^post6 = i9^0
		
		propagated equality tmp___0^post6 = tmp___0^0
		
		propagated equality i7^post6 = i7^0
		
		propagated equality i13^post6 = i13^0
		
		propagated equality i15^post6 = i15^0
		
		propagated equality tmp^post6 = tmp^0
		
		propagated equality i11^post6 = i11^0
		
		propagated equality i^post6 = i^0
		
		propagated equality i17^post6 = 1+i17^0
		
	Simplified Guard

	Original rule:
	l7 -> l8 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=1+i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i17^0 <= 0), cost: 1
	New rule:
	l7 -> l8 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=1+i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i17^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l7 -> l8 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=1+i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i17^0 <= 0, cost: 1
	New rule:
	l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l9 -> l10 : i11^0'=i11^post7, i13^0'=i13^post7, i15^0'=i15^post7, i17^0'=i17^post7, i7^0'=i7^post7, i9^0'=i9^post7, i^0'=i^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (-i15^post7+i15^0 == 0 /\ i11^0-i11^post7 == 0 /\ i13^0-i13^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ -i9^post7+i9^0 == 0 /\ -i7^post7+i7^0 == 0 /\ i17^0-i17^post7 == 0 /\ -i^post7+i^0 == 0 /\ tmp^0-tmp^post7 == 0), cost: 1
	New rule:
	l9 -> l10 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	
		propagated equality i15^post7 = i15^0
		
		propagated equality i11^post7 = i11^0
		
		propagated equality i13^post7 = i13^0
		
		propagated equality tmp___0^post7 = tmp___0^0
		
		propagated equality i9^post7 = i9^0
		
		propagated equality i7^post7 = i7^0
		
		propagated equality i17^post7 = i17^0
		
		propagated equality i^post7 = i^0
		
		propagated equality tmp^post7 = tmp^0
		
	Simplified Guard

	Original rule:
	l9 -> l10 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	New rule:
	l9 -> l10 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l9 -> l10 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	New rule:
	l9 -> l10 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l11 -> l8 : i11^0'=i11^post8, i13^0'=i13^post8, i15^0'=i15^post8, i17^0'=i17^post8, i7^0'=i7^post8, i9^0'=i9^post8, i^0'=i^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (-tmp___0^post8+tmp___0^0 == 0 /\ -tmp^post8+tmp^0 == 0 /\ i9^0-i9^post8 == 0 /\ -i13^post8+i13^0 == 0 /\ i11^0-i11^post8 == 0 /\ i17^1 == 0 /\ i^0-i^post8 == 0 /\ i17^post8 == 0 /\ -i7^post8+i7^0 == 0 /\ -i15^post8+i15^0 == 0 /\ 50-i15^0 <= 0), cost: 1
	New rule:
	l11 -> l8 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ i17^1 == 0 /\ 50-i15^0 <= 0), cost: 1
	
		propagated equality tmp___0^post8 = tmp___0^0
		
		propagated equality tmp^post8 = tmp^0
		
		propagated equality i9^post8 = i9^0
		
		propagated equality i13^post8 = i13^0
		
		propagated equality i11^post8 = i11^0
		
		propagated equality i^post8 = i^0
		
		propagated equality i17^post8 = 0
		
		propagated equality i7^post8 = i7^0
		
		propagated equality i15^post8 = i15^0
		
	Propagated Equalities

	Original rule:
	l11 -> l8 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ i17^1 == 0 /\ 50-i15^0 <= 0), cost: 1
	New rule:
	l11 -> l8 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i15^0 <= 0), cost: 1
	
		propagated equality i17^1 = 0
		
	Simplified Guard

	Original rule:
	l11 -> l8 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i15^0 <= 0), cost: 1
	New rule:
	l11 -> l8 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i15^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l11 -> l8 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i15^0 <= 0, cost: 1
	New rule:
	l11 -> l8 : i17^0'=0, 50-i15^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l11 -> l12 : i11^0'=i11^post9, i13^0'=i13^post9, i15^0'=i15^post9, i17^0'=i17^post9, i7^0'=i7^post9, i9^0'=i9^post9, i^0'=i^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, (i17^0-i17^post9 == 0 /\ -1+i15^post9-i15^0 == 0 /\ i11^0-i11^post9 == 0 /\ -49+i15^0 <= 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ tmp^0-tmp^post9 == 0 /\ -i13^post9+i13^0 == 0 /\ -i9^post9+i9^0 == 0 /\ -i^post9+i^0 == 0 /\ i7^0-i7^post9 == 0), cost: 1
	New rule:
	l11 -> l12 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=1+i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i15^0 <= 0), cost: 1
	
		propagated equality i17^post9 = i17^0
		
		propagated equality i15^post9 = 1+i15^0
		
		propagated equality i11^post9 = i11^0
		
		propagated equality tmp___0^post9 = tmp___0^0
		
		propagated equality tmp^post9 = tmp^0
		
		propagated equality i13^post9 = i13^0
		
		propagated equality i9^post9 = i9^0
		
		propagated equality i^post9 = i^0
		
		propagated equality i7^post9 = i7^0
		
	Simplified Guard

	Original rule:
	l11 -> l12 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=1+i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i15^0 <= 0), cost: 1
	New rule:
	l11 -> l12 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=1+i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i15^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l11 -> l12 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=1+i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i15^0 <= 0, cost: 1
	New rule:
	l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l13 -> l14 : i11^0'=i11^post10, i13^0'=i13^post10, i15^0'=i15^post10, i17^0'=i17^post10, i7^0'=i7^post10, i9^0'=i9^post10, i^0'=i^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, (tmp___0^0-tmp___0^post10 == 0 /\ i9^0-i9^post10 == 0 /\ i17^0-i17^post10 == 0 /\ -i13^post10+i13^0 == 0 /\ i15^0-i15^post10 == 0 /\ -i^post10+i^0 == 0 /\ -i7^post10+i7^0 == 0 /\ i11^0-i11^post10 == 0 /\ tmp^0-tmp^post10 == 0), cost: 1
	New rule:
	l13 -> l14 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	
		propagated equality tmp___0^post10 = tmp___0^0
		
		propagated equality i9^post10 = i9^0
		
		propagated equality i17^post10 = i17^0
		
		propagated equality i13^post10 = i13^0
		
		propagated equality i15^post10 = i15^0
		
		propagated equality i^post10 = i^0
		
		propagated equality i7^post10 = i7^0
		
		propagated equality i11^post10 = i11^0
		
		propagated equality tmp^post10 = tmp^0
		
	Simplified Guard

	Original rule:
	l13 -> l14 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	New rule:
	l13 -> l14 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l13 -> l14 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	New rule:
	l13 -> l14 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l15 -> l12 : i11^0'=i11^post11, i13^0'=i13^post11, i15^0'=i15^post11, i17^0'=i17^post11, i7^0'=i7^post11, i9^0'=i9^post11, i^0'=i^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, (50-i13^0 <= 0 /\ i17^0-i17^post11 == 0 /\ i15^post11 == 0 /\ i15^1 == 0 /\ i11^0-i11^post11 == 0 /\ -tmp___0^post11+tmp___0^0 == 0 /\ tmp^0-tmp^post11 == 0 /\ -i9^post11+i9^0 == 0 /\ -i13^post11+i13^0 == 0 /\ i7^0-i7^post11 == 0 /\ -i^post11+i^0 == 0), cost: 1
	New rule:
	l15 -> l12 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i13^0 <= 0 /\ i15^1 == 0), cost: 1
	
		propagated equality i17^post11 = i17^0
		
		propagated equality i15^post11 = 0
		
		propagated equality i11^post11 = i11^0
		
		propagated equality tmp___0^post11 = tmp___0^0
		
		propagated equality tmp^post11 = tmp^0
		
		propagated equality i9^post11 = i9^0
		
		propagated equality i13^post11 = i13^0
		
		propagated equality i7^post11 = i7^0
		
		propagated equality i^post11 = i^0
		
	Propagated Equalities

	Original rule:
	l15 -> l12 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i13^0 <= 0 /\ i15^1 == 0), cost: 1
	New rule:
	l15 -> l12 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i13^0 <= 0), cost: 1
	
		propagated equality i15^1 = 0
		
	Simplified Guard

	Original rule:
	l15 -> l12 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i13^0 <= 0), cost: 1
	New rule:
	l15 -> l12 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i13^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l15 -> l12 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i13^0 <= 0, cost: 1
	New rule:
	l15 -> l12 : i15^0'=0, 50-i13^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l15 -> l16 : i11^0'=i11^post12, i13^0'=i13^post12, i15^0'=i15^post12, i17^0'=i17^post12, i7^0'=i7^post12, i9^0'=i9^post12, i^0'=i^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (-1+i13^post12-i13^0 == 0 /\ -i9^post12+i9^0 == 0 /\ -tmp___0^post12+tmp___0^0 == 0 /\ i17^0-i17^post12 == 0 /\ -i^post12+i^0 == 0 /\ -i7^post12+i7^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ i15^0-i15^post12 == 0 /\ i11^0-i11^post12 == 0 /\ -49+i13^0 <= 0), cost: 1
	New rule:
	l15 -> l16 : i11^0'=i11^0, i13^0'=1+i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i13^0 <= 0), cost: 1
	
		propagated equality i13^post12 = 1+i13^0
		
		propagated equality i9^post12 = i9^0
		
		propagated equality tmp___0^post12 = tmp___0^0
		
		propagated equality i17^post12 = i17^0
		
		propagated equality i^post12 = i^0
		
		propagated equality i7^post12 = i7^0
		
		propagated equality tmp^post12 = tmp^0
		
		propagated equality i15^post12 = i15^0
		
		propagated equality i11^post12 = i11^0
		
	Simplified Guard

	Original rule:
	l15 -> l16 : i11^0'=i11^0, i13^0'=1+i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i13^0 <= 0), cost: 1
	New rule:
	l15 -> l16 : i11^0'=i11^0, i13^0'=1+i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i13^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l15 -> l16 : i11^0'=i11^0, i13^0'=1+i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i13^0 <= 0, cost: 1
	New rule:
	l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l16 -> l15 : i11^0'=i11^post13, i13^0'=i13^post13, i15^0'=i15^post13, i17^0'=i17^post13, i7^0'=i7^post13, i9^0'=i9^post13, i^0'=i^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, (-i7^post13+i7^0 == 0 /\ -i15^post13+i15^0 == 0 /\ -i13^post13+i13^0 == 0 /\ i9^0-i9^post13 == 0 /\ tmp^0-tmp^post13 == 0 /\ i17^0-i17^post13 == 0 /\ tmp___0^0-tmp___0^post13 == 0 /\ -i^post13+i^0 == 0 /\ i11^0-i11^post13 == 0), cost: 1
	New rule:
	l16 -> l15 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	
		propagated equality i7^post13 = i7^0
		
		propagated equality i15^post13 = i15^0
		
		propagated equality i13^post13 = i13^0
		
		propagated equality i9^post13 = i9^0
		
		propagated equality tmp^post13 = tmp^0
		
		propagated equality i17^post13 = i17^0
		
		propagated equality tmp___0^post13 = tmp___0^0
		
		propagated equality i^post13 = i^0
		
		propagated equality i11^post13 = i11^0
		
	Simplified Guard

	Original rule:
	l16 -> l15 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	New rule:
	l16 -> l15 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l16 -> l15 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	New rule:
	l16 -> l15 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l14 -> l16 : i11^0'=i11^post14, i13^0'=i13^post14, i15^0'=i15^post14, i17^0'=i17^post14, i7^0'=i7^post14, i9^0'=i9^post14, i^0'=i^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, (-tmp___0^post14+tmp___0^0 == 0 /\ i13^1 == 0 /\ i11^0-i11^post14 == 0 /\ -i9^post14+i9^0 == 0 /\ 50-i^0 <= 0 /\ -i^post14+i^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ -i15^post14+i15^0 == 0 /\ i13^post14 == 0 /\ i7^0-i7^post14 == 0 /\ i17^0-i17^post14 == 0), cost: 1
	New rule:
	l14 -> l16 : i11^0'=i11^0, i13^0'=0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ i13^1 == 0 /\ 50-i^0 <= 0), cost: 1
	
		propagated equality tmp___0^post14 = tmp___0^0
		
		propagated equality i11^post14 = i11^0
		
		propagated equality i9^post14 = i9^0
		
		propagated equality i^post14 = i^0
		
		propagated equality tmp^post14 = tmp^0
		
		propagated equality i15^post14 = i15^0
		
		propagated equality i13^post14 = 0
		
		propagated equality i7^post14 = i7^0
		
		propagated equality i17^post14 = i17^0
		
	Propagated Equalities

	Original rule:
	l14 -> l16 : i11^0'=i11^0, i13^0'=0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ i13^1 == 0 /\ 50-i^0 <= 0), cost: 1
	New rule:
	l14 -> l16 : i11^0'=i11^0, i13^0'=0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i^0 <= 0), cost: 1
	
		propagated equality i13^1 = 0
		
	Simplified Guard

	Original rule:
	l14 -> l16 : i11^0'=i11^0, i13^0'=0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i^0 <= 0), cost: 1
	New rule:
	l14 -> l16 : i11^0'=i11^0, i13^0'=0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l14 -> l16 : i11^0'=i11^0, i13^0'=0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i^0 <= 0, cost: 1
	New rule:
	l14 -> l16 : i13^0'=0, 50-i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l14 -> l13 : i11^0'=i11^post15, i13^0'=i13^post15, i15^0'=i15^post15, i17^0'=i17^post15, i7^0'=i7^post15, i9^0'=i9^post15, i^0'=i^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, (i9^0-i9^post15 == 0 /\ -i13^post15+i13^0 == 0 /\ tmp^0-tmp^post15 == 0 /\ -i15^post15+i15^0 == 0 /\ -i7^post15+i7^0 == 0 /\ tmp___0^0-tmp___0^post15 == 0 /\ i17^0-i17^post15 == 0 /\ -49+i^0 <= 0 /\ i11^0-i11^post15 == 0 /\ -1+i^post15-i^0 == 0), cost: 1
	New rule:
	l14 -> l13 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=1+i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i^0 <= 0), cost: 1
	
		propagated equality i9^post15 = i9^0
		
		propagated equality i13^post15 = i13^0
		
		propagated equality tmp^post15 = tmp^0
		
		propagated equality i15^post15 = i15^0
		
		propagated equality i7^post15 = i7^0
		
		propagated equality tmp___0^post15 = tmp___0^0
		
		propagated equality i17^post15 = i17^0
		
		propagated equality i11^post15 = i11^0
		
		propagated equality i^post15 = 1+i^0
		
	Simplified Guard

	Original rule:
	l14 -> l13 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=1+i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i^0 <= 0), cost: 1
	New rule:
	l14 -> l13 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=1+i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l14 -> l13 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=1+i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i^0 <= 0, cost: 1
	New rule:
	l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l12 -> l11 : i11^0'=i11^post16, i13^0'=i13^post16, i15^0'=i15^post16, i17^0'=i17^post16, i7^0'=i7^post16, i9^0'=i9^post16, i^0'=i^post16, tmp^0'=tmp^post16, tmp___0^0'=tmp___0^post16, (i^0-i^post16 == 0 /\ i15^0-i15^post16 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ -i17^post16+i17^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ -i13^post16+i13^0 == 0 /\ i9^0-i9^post16 == 0 /\ -i7^post16+i7^0 == 0 /\ -i11^post16+i11^0 == 0), cost: 1
	New rule:
	l12 -> l11 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	
		propagated equality i^post16 = i^0
		
		propagated equality i15^post16 = i15^0
		
		propagated equality tmp___0^post16 = tmp___0^0
		
		propagated equality i17^post16 = i17^0
		
		propagated equality tmp^post16 = tmp^0
		
		propagated equality i13^post16 = i13^0
		
		propagated equality i9^post16 = i9^0
		
		propagated equality i7^post16 = i7^0
		
		propagated equality i11^post16 = i11^0
		
	Simplified Guard

	Original rule:
	l12 -> l11 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	New rule:
	l12 -> l11 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l12 -> l11 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	New rule:
	l12 -> l11 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l10 -> l13 : i11^0'=i11^post17, i13^0'=i13^post17, i15^0'=i15^post17, i17^0'=i17^post17, i7^0'=i7^post17, i9^0'=i9^post17, i^0'=i^post17, tmp^0'=tmp^post17, tmp___0^0'=tmp___0^post17, (i9^0-i9^post17 == 0 /\ 50-i11^0 <= 0 /\ tmp^0-tmp^post17 == 0 /\ -i13^post17+i13^0 == 0 /\ i17^0-i17^post17 == 0 /\ -tmp___0^post17+tmp___0^0 == 0 /\ i^post17 == 0 /\ -i7^post17+i7^0 == 0 /\ -i15^post17+i15^0 == 0 /\ i11^0-i11^post17 == 0), cost: 1
	New rule:
	l10 -> l13 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i11^0 <= 0), cost: 1
	
		propagated equality i9^post17 = i9^0
		
		propagated equality tmp^post17 = tmp^0
		
		propagated equality i13^post17 = i13^0
		
		propagated equality i17^post17 = i17^0
		
		propagated equality tmp___0^post17 = tmp___0^0
		
		propagated equality i^post17 = 0
		
		propagated equality i7^post17 = i7^0
		
		propagated equality i15^post17 = i15^0
		
		propagated equality i11^post17 = i11^0
		
	Simplified Guard

	Original rule:
	l10 -> l13 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i11^0 <= 0), cost: 1
	New rule:
	l10 -> l13 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i11^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l10 -> l13 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i11^0 <= 0, cost: 1
	New rule:
	l10 -> l13 : i^0'=0, 50-i11^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l10 -> l9 : i11^0'=i11^post18, i13^0'=i13^post18, i15^0'=i15^post18, i17^0'=i17^post18, i7^0'=i7^post18, i9^0'=i9^post18, i^0'=i^post18, tmp^0'=tmp^post18, tmp___0^0'=tmp___0^post18, (-i^post18+i^0 == 0 /\ -i15^post18+i15^0 == 0 /\ -1-i11^0+i11^post18 == 0 /\ i7^0-i7^post18 == 0 /\ i17^0-i17^post18 == 0 /\ -49+i11^0 <= 0 /\ -tmp___0^post18+tmp___0^0 == 0 /\ -i13^post18+i13^0 == 0 /\ -i9^post18+i9^0 == 0 /\ tmp^0-tmp^post18 == 0), cost: 1
	New rule:
	l10 -> l9 : i11^0'=1+i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i11^0 <= 0), cost: 1
	
		propagated equality i^post18 = i^0
		
		propagated equality i15^post18 = i15^0
		
		propagated equality i11^post18 = 1+i11^0
		
		propagated equality i7^post18 = i7^0
		
		propagated equality i17^post18 = i17^0
		
		propagated equality tmp___0^post18 = tmp___0^0
		
		propagated equality i13^post18 = i13^0
		
		propagated equality i9^post18 = i9^0
		
		propagated equality tmp^post18 = tmp^0
		
	Simplified Guard

	Original rule:
	l10 -> l9 : i11^0'=1+i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i11^0 <= 0), cost: 1
	New rule:
	l10 -> l9 : i11^0'=1+i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i11^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l10 -> l9 : i11^0'=1+i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i11^0 <= 0, cost: 1
	New rule:
	l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l8 -> l7 : i11^0'=i11^post19, i13^0'=i13^post19, i15^0'=i15^post19, i17^0'=i17^post19, i7^0'=i7^post19, i9^0'=i9^post19, i^0'=i^post19, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, (-tmp^post19+tmp^0 == 0 /\ -tmp___0^post19+tmp___0^0 == 0 /\ i17^0-i17^post19 == 0 /\ i9^0-i9^post19 == 0 /\ i11^0-i11^post19 == 0 /\ -i13^post19+i13^0 == 0 /\ -i15^post19+i15^0 == 0 /\ i^0-i^post19 == 0 /\ i7^0-i7^post19 == 0), cost: 1
	New rule:
	l8 -> l7 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	
		propagated equality tmp^post19 = tmp^0
		
		propagated equality tmp___0^post19 = tmp___0^0
		
		propagated equality i17^post19 = i17^0
		
		propagated equality i9^post19 = i9^0
		
		propagated equality i11^post19 = i11^0
		
		propagated equality i13^post19 = i13^0
		
		propagated equality i15^post19 = i15^0
		
		propagated equality i^post19 = i^0
		
		propagated equality i7^post19 = i7^0
		
	Simplified Guard

	Original rule:
	l8 -> l7 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	New rule:
	l8 -> l7 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l8 -> l7 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	New rule:
	l8 -> l7 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l6 -> l9 : i11^0'=i11^post20, i13^0'=i13^post20, i15^0'=i15^post20, i17^0'=i17^post20, i7^0'=i7^post20, i9^0'=i9^post20, i^0'=i^post20, tmp^0'=tmp^post20, tmp___0^0'=tmp___0^post20, (50-i9^0 <= 0 /\ i17^0-i17^post20 == 0 /\ tmp^0-tmp^post20 == 0 /\ i^0-i^post20 == 0 /\ i15^0-i15^post20 == 0 /\ -i7^post20+i7^0 == 0 /\ i11^1 == 0 /\ i9^0-i9^post20 == 0 /\ -i13^post20+i13^0 == 0 /\ -tmp___0^post20+tmp___0^0 == 0 /\ i11^post20 == 0), cost: 1
	New rule:
	l6 -> l9 : i11^0'=0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i9^0 <= 0 /\ i11^1 == 0), cost: 1
	
		propagated equality i17^post20 = i17^0
		
		propagated equality tmp^post20 = tmp^0
		
		propagated equality i^post20 = i^0
		
		propagated equality i15^post20 = i15^0
		
		propagated equality i7^post20 = i7^0
		
		propagated equality i9^post20 = i9^0
		
		propagated equality i13^post20 = i13^0
		
		propagated equality tmp___0^post20 = tmp___0^0
		
		propagated equality i11^post20 = 0
		
	Propagated Equalities

	Original rule:
	l6 -> l9 : i11^0'=0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i9^0 <= 0 /\ i11^1 == 0), cost: 1
	New rule:
	l6 -> l9 : i11^0'=0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i9^0 <= 0), cost: 1
	
		propagated equality i11^1 = 0
		
	Simplified Guard

	Original rule:
	l6 -> l9 : i11^0'=0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i9^0 <= 0), cost: 1
	New rule:
	l6 -> l9 : i11^0'=0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i9^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l6 -> l9 : i11^0'=0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i9^0 <= 0, cost: 1
	New rule:
	l6 -> l9 : i11^0'=0, 50-i9^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l6 -> l5 : i11^0'=i11^post21, i13^0'=i13^post21, i15^0'=i15^post21, i17^0'=i17^post21, i7^0'=i7^post21, i9^0'=i9^post21, i^0'=i^post21, tmp^0'=tmp^post21, tmp___0^0'=tmp___0^post21, (-tmp___0^post21+tmp___0^0 == 0 /\ -tmp^post21+tmp^0 == 0 /\ i11^0-i11^post21 == 0 /\ i17^0-i17^post21 == 0 /\ i^0-i^post21 == 0 /\ -1-i9^0+i9^post21 == 0 /\ -i13^post21+i13^0 == 0 /\ -i15^post21+i15^0 == 0 /\ -49+i9^0 <= 0 /\ -i7^post21+i7^0 == 0), cost: 1
	New rule:
	l6 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=1+i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i9^0 <= 0), cost: 1
	
		propagated equality tmp___0^post21 = tmp___0^0
		
		propagated equality tmp^post21 = tmp^0
		
		propagated equality i11^post21 = i11^0
		
		propagated equality i17^post21 = i17^0
		
		propagated equality i^post21 = i^0
		
		propagated equality i9^post21 = 1+i9^0
		
		propagated equality i13^post21 = i13^0
		
		propagated equality i15^post21 = i15^0
		
		propagated equality i7^post21 = i7^0
		
	Simplified Guard

	Original rule:
	l6 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=1+i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i9^0 <= 0), cost: 1
	New rule:
	l6 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=1+i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i9^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l6 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=1+i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i9^0 <= 0, cost: 1
	New rule:
	l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l2 : i11^0'=i11^post22, i13^0'=i13^post22, i15^0'=i15^post22, i17^0'=i17^post22, i7^0'=i7^post22, i9^0'=i9^post22, i^0'=i^post22, tmp^0'=tmp^post22, tmp___0^0'=tmp___0^post22, (i11^0-i11^post22 == 0 /\ i13^0-i13^post22 == 0 /\ -i15^post22+i15^0 == 0 /\ -tmp___0^post22+tmp___0^0 == 0 /\ -i9^post22+i9^0 == 0 /\ -i^post22+i^0 == 0 /\ tmp^0-tmp^post22 == 0 /\ i7^0-i7^post22 == 0 /\ i17^0-i17^post22 == 0), cost: 1
	New rule:
	l4 -> l2 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	
		propagated equality i11^post22 = i11^0
		
		propagated equality i13^post22 = i13^0
		
		propagated equality i15^post22 = i15^0
		
		propagated equality tmp___0^post22 = tmp___0^0
		
		propagated equality i9^post22 = i9^0
		
		propagated equality i^post22 = i^0
		
		propagated equality tmp^post22 = tmp^0
		
		propagated equality i7^post22 = i7^0
		
		propagated equality i17^post22 = i17^0
		
	Simplified Guard

	Original rule:
	l4 -> l2 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1
	New rule:
	l4 -> l2 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l2 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1
	New rule:
	l4 -> l2 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l5 : i11^0'=i11^post23, i13^0'=i13^post23, i15^0'=i15^post23, i17^0'=i17^post23, i7^0'=i7^post23, i9^0'=i9^post23, i^0'=i^post23, tmp^0'=tmp^post23, tmp___0^0'=tmp___0^post23, (-tmp___0^post23+tmp___0^0 == 0 /\ i13^0-i13^post23 == 0 /\ i9^post23 == 0 /\ i9^1 == 0 /\ 50-i7^0 <= 0 /\ i11^0-i11^post23 == 0 /\ tmp^0-tmp^post23 == 0 /\ -i^post23+i^0 == 0 /\ -i15^post23+i15^0 == 0 /\ i7^0-i7^post23 == 0 /\ i17^0-i17^post23 == 0), cost: 1
	New rule:
	l1 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ i9^1 == 0 /\ 50-i7^0 <= 0), cost: 1
	
		propagated equality tmp___0^post23 = tmp___0^0
		
		propagated equality i13^post23 = i13^0
		
		propagated equality i9^post23 = 0
		
		propagated equality i11^post23 = i11^0
		
		propagated equality tmp^post23 = tmp^0
		
		propagated equality i^post23 = i^0
		
		propagated equality i15^post23 = i15^0
		
		propagated equality i7^post23 = i7^0
		
		propagated equality i17^post23 = i17^0
		
	Propagated Equalities

	Original rule:
	l1 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ i9^1 == 0 /\ 50-i7^0 <= 0), cost: 1
	New rule:
	l1 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i7^0 <= 0), cost: 1
	
		propagated equality i9^1 = 0
		
	Simplified Guard

	Original rule:
	l1 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 50-i7^0 <= 0), cost: 1
	New rule:
	l1 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i7^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l5 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=i7^0, i9^0'=0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 50-i7^0 <= 0, cost: 1
	New rule:
	l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l0 : i11^0'=i11^post24, i13^0'=i13^post24, i15^0'=i15^post24, i17^0'=i17^post24, i7^0'=i7^post24, i9^0'=i9^post24, i^0'=i^post24, tmp^0'=tmp^post24, tmp___0^0'=tmp___0^post24, (-i^post24+i^0 == 0 /\ -i15^post24+i15^0 == 0 /\ -i13^post24+i13^0 == 0 /\ i9^0-i9^post24 == 0 /\ i17^0-i17^post24 == 0 /\ tmp^0-tmp^post24 == 0 /\ tmp___0^0-tmp___0^post24 == 0 /\ i11^0-i11^post24 == 0 /\ -1+i7^post24-i7^0 == 0 /\ -49+i7^0 <= 0), cost: 1
	New rule:
	l1 -> l0 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=1+i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i7^0 <= 0), cost: 1
	
		propagated equality i^post24 = i^0
		
		propagated equality i15^post24 = i15^0
		
		propagated equality i13^post24 = i13^0
		
		propagated equality i9^post24 = i9^0
		
		propagated equality i17^post24 = i17^0
		
		propagated equality tmp^post24 = tmp^0
		
		propagated equality tmp___0^post24 = tmp___0^0
		
		propagated equality i11^post24 = i11^0
		
		propagated equality i7^post24 = 1+i7^0
		
	Simplified Guard

	Original rule:
	l1 -> l0 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=1+i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -49+i7^0 <= 0), cost: 1
	New rule:
	l1 -> l0 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=1+i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i7^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l0 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=1+i7^0, i9^0'=i9^0, i^0'=i^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, -49+i7^0 <= 0, cost: 1
	New rule:
	l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l18 -> l0 : i11^0'=i11^post25, i13^0'=i13^post25, i15^0'=i15^post25, i17^0'=i17^post25, i7^0'=i7^post25, i9^0'=i9^post25, i^0'=i^post25, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, (0 == 0 /\ -i15^post25+i15^post26 == 0 /\ -i7^post26+i7^0 == 0 /\ i9^0-i9^post26 == 0 /\ i13^post26-i13^post25 == 0 /\ i11^post26-i11^post25 == 0 /\ i17^0-i17^post26 == 0 /\ i^0-i^post26 == 0 /\ i7^1 == 0 /\ -tmp^post26+tmp^0 == 0 /\ -i13^post26+i13^0 == 0 /\ -i9^post25+i9^post26 == 0 /\ i^post25 == 0 /\ i15^0-i15^post26 == 0 /\ -i17^post25+i17^post26 == 0 /\ -tmp___0^post26+tmp___0^0 == 0 /\ i7^post25 == 0 /\ i11^0-i11^post26 == 0), cost: 1
	New rule:
	l18 -> l0 : i11^0'=i11^post26, i13^0'=i13^post26, i15^0'=i15^post26, i17^0'=i17^post26, i7^0'=0, i9^0'=i9^post26, i^0'=0, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, (0 == 0 /\ -i7^post26+i7^0 == 0 /\ i9^0-i9^post26 == 0 /\ i17^0-i17^post26 == 0 /\ i^0-i^post26 == 0 /\ i7^1 == 0 /\ -tmp^post26+tmp^0 == 0 /\ -i13^post26+i13^0 == 0 /\ i15^0-i15^post26 == 0 /\ -tmp___0^post26+tmp___0^0 == 0 /\ i11^0-i11^post26 == 0), cost: 1
	
		propagated equality i15^post25 = i15^post26
		
		propagated equality i13^post25 = i13^post26
		
		propagated equality i11^post25 = i11^post26
		
		propagated equality i9^post25 = i9^post26
		
		propagated equality i^post25 = 0
		
		propagated equality i17^post25 = i17^post26
		
		propagated equality i7^post25 = 0
		
	Propagated Equalities

	Original rule:
	l18 -> l0 : i11^0'=i11^post26, i13^0'=i13^post26, i15^0'=i15^post26, i17^0'=i17^post26, i7^0'=0, i9^0'=i9^post26, i^0'=0, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, (0 == 0 /\ -i7^post26+i7^0 == 0 /\ i9^0-i9^post26 == 0 /\ i17^0-i17^post26 == 0 /\ i^0-i^post26 == 0 /\ i7^1 == 0 /\ -tmp^post26+tmp^0 == 0 /\ -i13^post26+i13^0 == 0 /\ i15^0-i15^post26 == 0 /\ -tmp___0^post26+tmp___0^0 == 0 /\ i11^0-i11^post26 == 0), cost: 1
	New rule:
	l18 -> l0 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, 0 == 0, cost: 1
	
		propagated equality i7^post26 = i7^0
		
		propagated equality i9^post26 = i9^0
		
		propagated equality i17^post26 = i17^0
		
		propagated equality i^post26 = i^0
		
		propagated equality i7^1 = 0
		
		propagated equality tmp^post26 = tmp^0
		
		propagated equality i13^post26 = i13^0
		
		propagated equality i15^post26 = i15^0
		
		propagated equality tmp___0^post26 = tmp___0^0
		
		propagated equality i11^post26 = i11^0
		
	Simplified Guard

	Original rule:
	l18 -> l0 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, 0 == 0, cost: 1
	New rule:
	l18 -> l0 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l18 -> l0 : i11^0'=i11^0, i13^0'=i13^0, i15^0'=i15^0, i17^0'=i17^0, i7^0'=0, i9^0'=i9^0, i^0'=0, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, T, cost: 1
	New rule:
	l18 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, T, cost: 1

Step with 51

	Trace

	51[T]
	
	Blocked

	[{}, {}]

Step with 27

	Trace

	51[T], 27[T]
	
	Blocked

	[{}, {}, {}]

Step with 50

	Trace

	51[T], 27[T], 50[(-49+i7^0 <= 0)]
	
	Blocked

	[{}, {}, {49[T]}, {}]

Accelerate

Start location: l18
Program variables: i11^0 i13^0 i15^0 i17^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0
  27: l0 -> l1 : T, cost: 1
  52: l0 -> l0 : i7^0'=n+i7^0, (50-n-i7^0 >= 0 /\ -1+n >= 0), cost: 1
  49: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1
  50: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1
  28: l2 -> l3 : 50-i^0 <= 0, cost: 1
  29: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  48: l4 -> l2 : T, cost: 1
  30: l5 -> l6 : T, cost: 1
  46: l6 -> l9 : i11^0'=0, 50-i9^0 <= 0, cost: 1
  47: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1
  31: l7 -> l4 : i^0'=0, 50-i17^0 <= 0, cost: 1
  32: l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1
  45: l8 -> l7 : T, cost: 1
  33: l9 -> l10 : T, cost: 1
  43: l10 -> l13 : i^0'=0, 50-i11^0 <= 0, cost: 1
  44: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1
  34: l11 -> l8 : i17^0'=0, 50-i15^0 <= 0, cost: 1
  35: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1
  42: l12 -> l11 : T, cost: 1
  36: l13 -> l14 : T, cost: 1
  40: l14 -> l16 : i13^0'=0, 50-i^0 <= 0, cost: 1
  41: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  37: l15 -> l12 : i15^0'=0, 50-i13^0 <= 0, cost: 1
  38: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1
  39: l16 -> l15 : T, cost: 1
  51: l18 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, T, cost: 1

	Loop Acceleration

	Original rule:
	l0 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1
	New rule:
	l0 -> l0 : i7^0'=n+i7^0, (50-n-i7^0 >= 0 /\ -1+n >= 0), cost: 1

		49-i7^0 >= 0 [0]: montonic decrease yields 50-n-i7^0 >= 0
		
		49-i7^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 49-i7^0 >= 0)
		
		Replacement map: {49-i7^0 >= 0 -> 50-n-i7^0 >= 0}

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {52[T]}]

Step with 27

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T]
	
	Blocked

	[{}, {}, {52[T]}, {}]

Step with 50

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 50[(-49+i7^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {}, {}]

Covered

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}]

Step with 49

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}]

Step with 30

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 30[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {}]

Step with 47

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 30[T], 47[(-49+i9^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {46[T]}, {}]

Accelerate

Start location: l18
Program variables: i11^0 i13^0 i15^0 i17^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0
  27: l0 -> l1 : T, cost: 1
  52: l0 -> l0 : i7^0'=n+i7^0, (50-n-i7^0 >= 0 /\ -1+n >= 0), cost: 1
  49: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1
  50: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1
  28: l2 -> l3 : 50-i^0 <= 0, cost: 1
  29: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  48: l4 -> l2 : T, cost: 1
  30: l5 -> l6 : T, cost: 1
  53: l5 -> l5 : i9^0'=n2+i9^0, (50-n2-i9^0 >= 0 /\ -1+n2 >= 0), cost: 1
  46: l6 -> l9 : i11^0'=0, 50-i9^0 <= 0, cost: 1
  47: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1
  31: l7 -> l4 : i^0'=0, 50-i17^0 <= 0, cost: 1
  32: l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1
  45: l8 -> l7 : T, cost: 1
  33: l9 -> l10 : T, cost: 1
  43: l10 -> l13 : i^0'=0, 50-i11^0 <= 0, cost: 1
  44: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1
  34: l11 -> l8 : i17^0'=0, 50-i15^0 <= 0, cost: 1
  35: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1
  42: l12 -> l11 : T, cost: 1
  36: l13 -> l14 : T, cost: 1
  40: l14 -> l16 : i13^0'=0, 50-i^0 <= 0, cost: 1
  41: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  37: l15 -> l12 : i15^0'=0, 50-i13^0 <= 0, cost: 1
  38: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1
  39: l16 -> l15 : T, cost: 1
  51: l18 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, T, cost: 1

	Loop Acceleration

	Original rule:
	l5 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1
	New rule:
	l5 -> l5 : i9^0'=n2+i9^0, (50-n2-i9^0 >= 0 /\ -1+n2 >= 0), cost: 1

		49-i9^0 >= 0 [0]: montonic decrease yields 50-n2-i9^0 >= 0
		
		49-i9^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 49-i9^0 >= 0)
		
		Replacement map: {49-i9^0 >= 0 -> 50-n2-i9^0 >= 0}

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}]

Step with 30

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {}]

Step with 47

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 47[(-49+i9^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {}, {}]

Covered

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}]

Step with 46

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}]

Step with 33

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 33[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {}]

Step with 44

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 33[T], 44[(-49+i11^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {43[T]}, {}]

Accelerate

Start location: l18
Program variables: i11^0 i13^0 i15^0 i17^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0
  27: l0 -> l1 : T, cost: 1
  52: l0 -> l0 : i7^0'=n+i7^0, (50-n-i7^0 >= 0 /\ -1+n >= 0), cost: 1
  49: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1
  50: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1
  28: l2 -> l3 : 50-i^0 <= 0, cost: 1
  29: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  48: l4 -> l2 : T, cost: 1
  30: l5 -> l6 : T, cost: 1
  53: l5 -> l5 : i9^0'=n2+i9^0, (50-n2-i9^0 >= 0 /\ -1+n2 >= 0), cost: 1
  46: l6 -> l9 : i11^0'=0, 50-i9^0 <= 0, cost: 1
  47: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1
  31: l7 -> l4 : i^0'=0, 50-i17^0 <= 0, cost: 1
  32: l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1
  45: l8 -> l7 : T, cost: 1
  33: l9 -> l10 : T, cost: 1
  54: l9 -> l9 : i11^0'=i11^0+n3, (-1+n3 >= 0 /\ 50-i11^0-n3 >= 0), cost: 1
  43: l10 -> l13 : i^0'=0, 50-i11^0 <= 0, cost: 1
  44: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1
  34: l11 -> l8 : i17^0'=0, 50-i15^0 <= 0, cost: 1
  35: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1
  42: l12 -> l11 : T, cost: 1
  36: l13 -> l14 : T, cost: 1
  40: l14 -> l16 : i13^0'=0, 50-i^0 <= 0, cost: 1
  41: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  37: l15 -> l12 : i15^0'=0, 50-i13^0 <= 0, cost: 1
  38: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1
  39: l16 -> l15 : T, cost: 1
  51: l18 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, T, cost: 1

	Loop Acceleration

	Original rule:
	l9 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1
	New rule:
	l9 -> l9 : i11^0'=i11^0+n3, (-1+n3 >= 0 /\ 50-i11^0-n3 >= 0), cost: 1

		49-i11^0 >= 0 [0]: montonic decrease yields 50-i11^0-n3 >= 0
		
		49-i11^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 49-i11^0 >= 0)
		
		Replacement map: {49-i11^0 >= 0 -> 50-i11^0-n3 >= 0}

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}]

Step with 33

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {}]

Step with 44

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 44[(-49+i11^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {}, {}]

Covered

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}]

Step with 43

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}]

Step with 36

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 36[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {}]

Step with 41

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 36[T], 41[(-49+i^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {40[T]}, {}]

Accelerate

Start location: l18
Program variables: i11^0 i13^0 i15^0 i17^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0
  27: l0 -> l1 : T, cost: 1
  52: l0 -> l0 : i7^0'=n+i7^0, (50-n-i7^0 >= 0 /\ -1+n >= 0), cost: 1
  49: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1
  50: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1
  28: l2 -> l3 : 50-i^0 <= 0, cost: 1
  29: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  48: l4 -> l2 : T, cost: 1
  30: l5 -> l6 : T, cost: 1
  53: l5 -> l5 : i9^0'=n2+i9^0, (50-n2-i9^0 >= 0 /\ -1+n2 >= 0), cost: 1
  46: l6 -> l9 : i11^0'=0, 50-i9^0 <= 0, cost: 1
  47: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1
  31: l7 -> l4 : i^0'=0, 50-i17^0 <= 0, cost: 1
  32: l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1
  45: l8 -> l7 : T, cost: 1
  33: l9 -> l10 : T, cost: 1
  54: l9 -> l9 : i11^0'=i11^0+n3, (-1+n3 >= 0 /\ 50-i11^0-n3 >= 0), cost: 1
  43: l10 -> l13 : i^0'=0, 50-i11^0 <= 0, cost: 1
  44: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1
  34: l11 -> l8 : i17^0'=0, 50-i15^0 <= 0, cost: 1
  35: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1
  42: l12 -> l11 : T, cost: 1
  36: l13 -> l14 : T, cost: 1
  55: l13 -> l13 : i^0'=i^0+n4, (50-i^0-n4 >= 0 /\ -1+n4 >= 0), cost: 1
  40: l14 -> l16 : i13^0'=0, 50-i^0 <= 0, cost: 1
  41: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  37: l15 -> l12 : i15^0'=0, 50-i13^0 <= 0, cost: 1
  38: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1
  39: l16 -> l15 : T, cost: 1
  51: l18 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, T, cost: 1

	Loop Acceleration

	Original rule:
	l13 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
	New rule:
	l13 -> l13 : i^0'=i^0+n4, (50-i^0-n4 >= 0 /\ -1+n4 >= 0), cost: 1

		49-i^0 >= 0 [0]: montonic decrease yields 50-i^0-n4 >= 0
		
		49-i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 49-i^0 >= 0)
		
		Replacement map: {49-i^0 >= 0 -> 50-i^0-n4 >= 0}

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}]

Step with 36

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {}]

Step with 41

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 41[(-49+i^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {}, {}]

Covered

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}]

Step with 40

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}]

Step with 39

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 39[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {}]

Step with 38

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 39[T], 38[(-49+i13^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {37[T]}, {}]

Accelerate

Start location: l18
Program variables: i11^0 i13^0 i15^0 i17^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0
  27: l0 -> l1 : T, cost: 1
  52: l0 -> l0 : i7^0'=n+i7^0, (50-n-i7^0 >= 0 /\ -1+n >= 0), cost: 1
  49: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1
  50: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1
  28: l2 -> l3 : 50-i^0 <= 0, cost: 1
  29: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  48: l4 -> l2 : T, cost: 1
  30: l5 -> l6 : T, cost: 1
  53: l5 -> l5 : i9^0'=n2+i9^0, (50-n2-i9^0 >= 0 /\ -1+n2 >= 0), cost: 1
  46: l6 -> l9 : i11^0'=0, 50-i9^0 <= 0, cost: 1
  47: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1
  31: l7 -> l4 : i^0'=0, 50-i17^0 <= 0, cost: 1
  32: l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1
  45: l8 -> l7 : T, cost: 1
  33: l9 -> l10 : T, cost: 1
  54: l9 -> l9 : i11^0'=i11^0+n3, (-1+n3 >= 0 /\ 50-i11^0-n3 >= 0), cost: 1
  43: l10 -> l13 : i^0'=0, 50-i11^0 <= 0, cost: 1
  44: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1
  34: l11 -> l8 : i17^0'=0, 50-i15^0 <= 0, cost: 1
  35: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1
  42: l12 -> l11 : T, cost: 1
  36: l13 -> l14 : T, cost: 1
  55: l13 -> l13 : i^0'=i^0+n4, (50-i^0-n4 >= 0 /\ -1+n4 >= 0), cost: 1
  40: l14 -> l16 : i13^0'=0, 50-i^0 <= 0, cost: 1
  41: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  37: l15 -> l12 : i15^0'=0, 50-i13^0 <= 0, cost: 1
  38: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1
  39: l16 -> l15 : T, cost: 1
  56: l16 -> l16 : i13^0'=n5+i13^0, (-1+n5 >= 0 /\ 50-n5-i13^0 >= 0), cost: 1
  51: l18 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, T, cost: 1

	Loop Acceleration

	Original rule:
	l16 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1
	New rule:
	l16 -> l16 : i13^0'=n5+i13^0, (-1+n5 >= 0 /\ 50-n5-i13^0 >= 0), cost: 1

		49-i13^0 >= 0 [0]: montonic decrease yields 50-n5-i13^0 >= 0
		
		49-i13^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 49-i13^0 >= 0)
		
		Replacement map: {49-i13^0 >= 0 -> 50-n5-i13^0 >= 0}

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}]

Step with 39

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {}]

Step with 38

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 38[(-49+i13^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {}, {}]

Covered

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}]

Step with 37

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}]

Step with 42

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 42[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {}]

Step with 35

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 42[T], 35[(-49+i15^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {34[T]}, {}]

Accelerate

Start location: l18
Program variables: i11^0 i13^0 i15^0 i17^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0
  27: l0 -> l1 : T, cost: 1
  52: l0 -> l0 : i7^0'=n+i7^0, (50-n-i7^0 >= 0 /\ -1+n >= 0), cost: 1
  49: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1
  50: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1
  28: l2 -> l3 : 50-i^0 <= 0, cost: 1
  29: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  48: l4 -> l2 : T, cost: 1
  30: l5 -> l6 : T, cost: 1
  53: l5 -> l5 : i9^0'=n2+i9^0, (50-n2-i9^0 >= 0 /\ -1+n2 >= 0), cost: 1
  46: l6 -> l9 : i11^0'=0, 50-i9^0 <= 0, cost: 1
  47: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1
  31: l7 -> l4 : i^0'=0, 50-i17^0 <= 0, cost: 1
  32: l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1
  45: l8 -> l7 : T, cost: 1
  33: l9 -> l10 : T, cost: 1
  54: l9 -> l9 : i11^0'=i11^0+n3, (-1+n3 >= 0 /\ 50-i11^0-n3 >= 0), cost: 1
  43: l10 -> l13 : i^0'=0, 50-i11^0 <= 0, cost: 1
  44: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1
  34: l11 -> l8 : i17^0'=0, 50-i15^0 <= 0, cost: 1
  35: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1
  42: l12 -> l11 : T, cost: 1
  57: l12 -> l12 : i15^0'=n6+i15^0, (50-n6-i15^0 >= 0 /\ -1+n6 >= 0), cost: 1
  36: l13 -> l14 : T, cost: 1
  55: l13 -> l13 : i^0'=i^0+n4, (50-i^0-n4 >= 0 /\ -1+n4 >= 0), cost: 1
  40: l14 -> l16 : i13^0'=0, 50-i^0 <= 0, cost: 1
  41: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  37: l15 -> l12 : i15^0'=0, 50-i13^0 <= 0, cost: 1
  38: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1
  39: l16 -> l15 : T, cost: 1
  56: l16 -> l16 : i13^0'=n5+i13^0, (-1+n5 >= 0 /\ 50-n5-i13^0 >= 0), cost: 1
  51: l18 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, T, cost: 1

	Loop Acceleration

	Original rule:
	l12 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1
	New rule:
	l12 -> l12 : i15^0'=n6+i15^0, (50-n6-i15^0 >= 0 /\ -1+n6 >= 0), cost: 1

		49-i15^0 >= 0 [0]: montonic decrease yields 50-n6-i15^0 >= 0
		
		49-i15^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 49-i15^0 >= 0)
		
		Replacement map: {49-i15^0 >= 0 -> 50-n6-i15^0 >= 0}

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}]

Step with 42

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {}]

Step with 35

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 35[(-49+i15^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {}, {}]

Covered

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}]

Step with 34

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}]

Step with 45

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 45[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {}]

Step with 32

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 45[T], 32[(-49+i17^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {31[T]}, {}]

Accelerate

Start location: l18
Program variables: i11^0 i13^0 i15^0 i17^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0
  27: l0 -> l1 : T, cost: 1
  52: l0 -> l0 : i7^0'=n+i7^0, (50-n-i7^0 >= 0 /\ -1+n >= 0), cost: 1
  49: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1
  50: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1
  28: l2 -> l3 : 50-i^0 <= 0, cost: 1
  29: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  48: l4 -> l2 : T, cost: 1
  30: l5 -> l6 : T, cost: 1
  53: l5 -> l5 : i9^0'=n2+i9^0, (50-n2-i9^0 >= 0 /\ -1+n2 >= 0), cost: 1
  46: l6 -> l9 : i11^0'=0, 50-i9^0 <= 0, cost: 1
  47: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1
  31: l7 -> l4 : i^0'=0, 50-i17^0 <= 0, cost: 1
  32: l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1
  45: l8 -> l7 : T, cost: 1
  58: l8 -> l8 : i17^0'=i17^0+n7, (50-i17^0-n7 >= 0 /\ -1+n7 >= 0), cost: 1
  33: l9 -> l10 : T, cost: 1
  54: l9 -> l9 : i11^0'=i11^0+n3, (-1+n3 >= 0 /\ 50-i11^0-n3 >= 0), cost: 1
  43: l10 -> l13 : i^0'=0, 50-i11^0 <= 0, cost: 1
  44: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1
  34: l11 -> l8 : i17^0'=0, 50-i15^0 <= 0, cost: 1
  35: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1
  42: l12 -> l11 : T, cost: 1
  57: l12 -> l12 : i15^0'=n6+i15^0, (50-n6-i15^0 >= 0 /\ -1+n6 >= 0), cost: 1
  36: l13 -> l14 : T, cost: 1
  55: l13 -> l13 : i^0'=i^0+n4, (50-i^0-n4 >= 0 /\ -1+n4 >= 0), cost: 1
  40: l14 -> l16 : i13^0'=0, 50-i^0 <= 0, cost: 1
  41: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  37: l15 -> l12 : i15^0'=0, 50-i13^0 <= 0, cost: 1
  38: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1
  39: l16 -> l15 : T, cost: 1
  56: l16 -> l16 : i13^0'=n5+i13^0, (-1+n5 >= 0 /\ 50-n5-i13^0 >= 0), cost: 1
  51: l18 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, T, cost: 1

	Loop Acceleration

	Original rule:
	l8 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1
	New rule:
	l8 -> l8 : i17^0'=i17^0+n7, (50-i17^0-n7 >= 0 /\ -1+n7 >= 0), cost: 1

		49-i17^0 >= 0 [0]: montonic decrease yields 50-i17^0-n7 >= 0
		
		49-i17^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 49-i17^0 >= 0)
		
		Replacement map: {49-i17^0 >= 0 -> 50-i17^0-n7 >= 0}

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}]

Step with 45

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {}]

Step with 32

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T], 32[(-49+i17^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {}, {}]

Covered

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {32[T]}]

Step with 31

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T], 31[(50-i17^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {32[T]}, {}]

Step with 48

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T], 31[(50-i17^0 <= 0)], 48[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {32[T]}, {}, {}]

Step with 29

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T], 31[(50-i17^0 <= 0)], 48[T], 29[(-49+i^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {32[T]}, {}, {28[T]}, {}]

Accelerate

Start location: l18
Program variables: i11^0 i13^0 i15^0 i17^0 i7^0 i9^0 i^0 tmp^0 tmp___0^0
  27: l0 -> l1 : T, cost: 1
  52: l0 -> l0 : i7^0'=n+i7^0, (50-n-i7^0 >= 0 /\ -1+n >= 0), cost: 1
  49: l1 -> l5 : i9^0'=0, 50-i7^0 <= 0, cost: 1
  50: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1
  28: l2 -> l3 : 50-i^0 <= 0, cost: 1
  29: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  48: l4 -> l2 : T, cost: 1
  59: l4 -> l4 : i^0'=n8+i^0, (50-n8-i^0 >= 0 /\ -1+n8 >= 0), cost: 1
  30: l5 -> l6 : T, cost: 1
  53: l5 -> l5 : i9^0'=n2+i9^0, (50-n2-i9^0 >= 0 /\ -1+n2 >= 0), cost: 1
  46: l6 -> l9 : i11^0'=0, 50-i9^0 <= 0, cost: 1
  47: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1
  31: l7 -> l4 : i^0'=0, 50-i17^0 <= 0, cost: 1
  32: l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1
  45: l8 -> l7 : T, cost: 1
  58: l8 -> l8 : i17^0'=i17^0+n7, (50-i17^0-n7 >= 0 /\ -1+n7 >= 0), cost: 1
  33: l9 -> l10 : T, cost: 1
  54: l9 -> l9 : i11^0'=i11^0+n3, (-1+n3 >= 0 /\ 50-i11^0-n3 >= 0), cost: 1
  43: l10 -> l13 : i^0'=0, 50-i11^0 <= 0, cost: 1
  44: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1
  34: l11 -> l8 : i17^0'=0, 50-i15^0 <= 0, cost: 1
  35: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1
  42: l12 -> l11 : T, cost: 1
  57: l12 -> l12 : i15^0'=n6+i15^0, (50-n6-i15^0 >= 0 /\ -1+n6 >= 0), cost: 1
  36: l13 -> l14 : T, cost: 1
  55: l13 -> l13 : i^0'=i^0+n4, (50-i^0-n4 >= 0 /\ -1+n4 >= 0), cost: 1
  40: l14 -> l16 : i13^0'=0, 50-i^0 <= 0, cost: 1
  41: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
  37: l15 -> l12 : i15^0'=0, 50-i13^0 <= 0, cost: 1
  38: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1
  39: l16 -> l15 : T, cost: 1
  56: l16 -> l16 : i13^0'=n5+i13^0, (-1+n5 >= 0 /\ 50-n5-i13^0 >= 0), cost: 1
  51: l18 -> l0 : i7^0'=0, i^0'=0, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, T, cost: 1

	Loop Acceleration

	Original rule:
	l4 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1
	New rule:
	l4 -> l4 : i^0'=n8+i^0, (50-n8-i^0 >= 0 /\ -1+n8 >= 0), cost: 1

		49-i^0 >= 0 [0]: montonic decrease yields 50-n8-i^0 >= 0
		
		49-i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 49-i^0 >= 0)
		
		Replacement map: {49-i^0 >= 0 -> 50-n8-i^0 >= 0}

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T], 31[(50-i17^0 <= 0)], 59[(50-n8-i^0 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {32[T]}, {}, {59[T]}]

Step with 48

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T], 31[(50-i17^0 <= 0)], 59[(50-n8-i^0 >= 0 /\ -1+n8 >= 0)], 48[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {32[T]}, {}, {59[T]}, {}]

Step with 29

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T], 31[(50-i17^0 <= 0)], 59[(50-n8-i^0 >= 0 /\ -1+n8 >= 0)], 48[T], 29[(-49+i^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {32[T]}, {}, {59[T]}, {}, {}]

Covered

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T], 31[(50-i17^0 <= 0)], 59[(50-n8-i^0 >= 0 /\ -1+n8 >= 0)], 48[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {32[T]}, {}, {59[T]}, {29[T]}]

Step with 28

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T], 31[(50-i17^0 <= 0)], 59[(50-n8-i^0 >= 0 /\ -1+n8 >= 0)], 48[T], 28[(50-i^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {32[T]}, {}, {59[T]}, {29[T]}, {}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T], 31[(50-i17^0 <= 0)], 59[(50-n8-i^0 >= 0 /\ -1+n8 >= 0)], 48[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {32[T]}, {}, {59[T]}, {28[T], 29[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T], 31[(50-i17^0 <= 0)], 59[(50-n8-i^0 >= 0 /\ -1+n8 >= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {32[T]}, {}, {48[T], 59[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T], 31[(50-i17^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {32[T]}, {59[T]}]

Step with 48

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T], 31[(50-i17^0 <= 0)], 48[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {32[T]}, {59[T]}, {}]

Step with 29

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T], 31[(50-i17^0 <= 0)], 48[T], 29[(-49+i^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {32[T]}, {59[T]}, {28[T]}, {}]

Covered

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T], 31[(50-i17^0 <= 0)], 48[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {32[T]}, {59[T]}, {28[T], 29[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T], 31[(50-i17^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {32[T]}, {48[T], 59[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)], 45[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {58[T]}, {31[T], 32[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 58[(50-i17^0-n7 >= 0 /\ -1+n7 >= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {}, {45[T], 58[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {58[T]}]

Step with 45

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 45[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {58[T]}, {}]

Step with 32

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 45[T], 32[(-49+i17^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {58[T]}, {31[T]}, {}]

Covered

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)], 45[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {58[T]}, {31[T], 32[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T], 34[(50-i15^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {35[T]}, {45[T], 58[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)], 42[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {57[T]}, {34[T], 35[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 57[(50-n6-i15^0 >= 0 /\ -1+n6 >= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {}, {42[T], 57[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {57[T]}]

Step with 42

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 42[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {57[T]}, {}]

Step with 35

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 42[T], 35[(-49+i15^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {57[T]}, {34[T]}, {}]

Covered

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)], 42[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {57[T]}, {34[T], 35[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T], 37[(50-i13^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {38[T]}, {42[T], 57[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)], 39[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {56[T]}, {37[T], 38[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 56[(-1+n5 >= 0 /\ 50-n5-i13^0 >= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {}, {39[T], 56[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {56[T]}]

Step with 39

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 39[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {56[T]}, {}]

Step with 38

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 39[T], 38[(-49+i13^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {56[T]}, {37[T]}, {}]

Covered

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)], 39[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {56[T]}, {37[T], 38[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T], 40[(50-i^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {41[T]}, {39[T], 56[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)], 36[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {55[T]}, {40[T], 41[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 55[(50-i^0-n4 >= 0 /\ -1+n4 >= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {}, {36[T], 55[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {55[T]}]

Step with 36

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 36[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {55[T]}, {}]

Step with 41

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 36[T], 41[(-49+i^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {55[T]}, {40[T]}, {}]

Covered

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)], 36[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {55[T]}, {40[T], 41[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T], 43[(50-i11^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {44[T]}, {36[T], 55[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)], 33[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {54[T]}, {43[T], 44[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 54[(-1+n3 >= 0 /\ 50-i11^0-n3 >= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {}, {33[T], 54[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {54[T]}]

Step with 33

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 33[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {54[T]}, {}]

Step with 44

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 33[T], 44[(-49+i11^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {54[T]}, {43[T]}, {}]

Covered

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)], 33[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {54[T]}, {43[T], 44[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T], 46[(50-i9^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {47[T]}, {33[T], 54[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)], 30[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {53[T]}, {46[T], 47[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 53[(50-n2-i9^0 >= 0 /\ -1+n2 >= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {}, {30[T], 53[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {53[T]}]

Step with 30

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 30[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {53[T]}, {}]

Step with 47

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 30[T], 47[(-49+i9^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {53[T]}, {46[T]}, {}]

Covered

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)], 30[T]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {53[T]}, {46[T], 47[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T], 49[(50-i7^0 <= 0)]
	
	Blocked

	[{}, {}, {52[T]}, {50[T]}, {30[T], 53[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)], 27[T]
	
	Blocked

	[{}, {}, {52[T]}, {49[T], 50[T]}]

Backtrack

	Trace

	51[T], 52[(50-n-i7^0 >= 0 /\ -1+n >= 0)]
	
	Blocked

	[{}, {}, {27[T], 52[T]}]

Backtrack

	Trace

	51[T]
	
	Blocked

	[{}, {52[T]}]

Step with 27

	Trace

	51[T], 27[T]
	
	Blocked

	[{}, {52[T]}, {}]

Step with 50

	Trace

	51[T], 27[T], 50[(-49+i7^0 <= 0)]
	
	Blocked

	[{}, {52[T]}, {49[T]}, {}]

Covered

	Trace

	51[T], 27[T]
	
	Blocked

	[{}, {52[T]}, {49[T], 50[T]}]

Backtrack

	Trace

	51[T]
	
	Blocked

	[{}, {27[T], 52[T]}]

Backtrack

	Trace

	Blocked

	[{51[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b