WORST_CASE(Omega(0),?)

Initial ITS
Start location: l6
   0: l0 -> l1 : tmp1011^0'=tmp1011^post0, z317^0'=z317^post0, tmp58^0'=tmp58^post0, i20^0'=i20^post0, tmp710^0'=tmp710^post0, tmp25^0'=tmp25^post0, z519^0'=z519^post0, tmp1213^0'=tmp1213^post0, tmp03^0'=tmp03^post0, z216^0'=z216^post0, tmp47^0'=tmp47^post0, constant22^0'=constant22^post0, tmp14^0'=tmp14^post0, tmp1112^0'=tmp1112^post0, z418^0'=z418^post0, tmp69^0'=tmp69^post0, lx2^0'=lx2^post0, z115^0'=z115^post0, tmp36^0'=tmp36^post0, tmp1314^0'=tmp1314^post0, (tmp58^0-tmp58^post0 == 0 /\ tmp1011^0-tmp1011^post0 == 0 /\ -z115^post0+z115^0 == 0 /\ i20^post0 == 0 /\ -tmp1213^post0+tmp1213^0 == 0 /\ -tmp14^post0+tmp14^0 == 0 /\ tmp1112^0-tmp1112^post0 == 0 /\ z519^0-z519^post0 == 0 /\ -z418^post0+z418^0 == 0 /\ z216^0-z216^post0 == 0 /\ tmp47^0-tmp47^post0 == 0 /\ tmp710^0-tmp710^post0 == 0 /\ 8-i20^0 <= 0 /\ -tmp1314^post0+tmp1314^0 == 0 /\ -lx2^post0+lx2^0 == 0 /\ z317^0-z317^post0 == 0 /\ -tmp36^post0+tmp36^0 == 0 /\ -tmp03^post0+tmp03^0 == 0 /\ -constant22^post0+constant22^0 == 0 /\ tmp69^0-tmp69^post0 == 0 /\ tmp25^0-tmp25^post0 == 0), cost: 1
   1: l0 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^post1, tmp58^0'=tmp58^post1, i20^0'=i20^post1, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=tmp1213^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=constant22^post1, tmp14^0'=tmp14^post1, tmp1112^0'=tmp1112^post1, z418^0'=z418^post1, tmp69^0'=tmp69^post1, lx2^0'=lx2^post1, z115^0'=z115^post1, tmp36^0'=tmp36^post1, tmp1314^0'=tmp1314^post1, (0 == 0 /\ -6270+constant22^20 == 0 /\ -z317^20+z317^post1-z519^post1 == 0 /\ -25172+constant22^70 == 0 /\ 20995+constant22^100 == 0 /\ -9633+constant22^40 == 0 /\ -1+i20^post1-i20^0 == 0 /\ -7+i20^0 <= 0 /\ -tmp36^post1+tmp1011^post1-tmp03^post1 == 0 /\ -16819+constant22^60 == 0 /\ tmp1213^post1+tmp25^post1-tmp14^post1 == 0 /\ -tmp58^10+z216^10-tmp69^10 == 0 /\ 16069+constant22^110 == 0 /\ -tmp47^10-tmp710^10+z115^20 == 0 /\ -4433+constant22^12 == 0 /\ 7373+constant22^90 == 0 /\ -2446+constant22^50 == 0 /\ tmp1314^post1+tmp36^post1-tmp03^post1 == 0 /\ 15137+constant22^30 == 0 /\ 3196+constant22^post1 == 0 /\ tmp1112^post1-tmp25^post1-tmp14^post1 == 0 /\ -lx2^post1+lx2^0 == 0 /\ z317^10-tmp47^10-tmp69^10 == 0 /\ -tmp58^10-tmp710^10+z418^10 == 0 /\ z418^post1-z519^post1-z418^20 == 0 /\ -12299+constant22^80 == 0), cost: 1
   5: l1 -> l3 : tmp1011^0'=tmp1011^post5, z317^0'=z317^post5, tmp58^0'=tmp58^post5, i20^0'=i20^post5, tmp710^0'=tmp710^post5, tmp25^0'=tmp25^post5, z519^0'=z519^post5, tmp1213^0'=tmp1213^post5, tmp03^0'=tmp03^post5, z216^0'=z216^post5, tmp47^0'=tmp47^post5, constant22^0'=constant22^post5, tmp14^0'=tmp14^post5, tmp1112^0'=tmp1112^post5, z418^0'=z418^post5, tmp69^0'=tmp69^post5, lx2^0'=lx2^post5, z115^0'=z115^post5, tmp36^0'=tmp36^post5, tmp1314^0'=tmp1314^post5, (tmp1011^0-tmp1011^post5 == 0 /\ tmp58^0-tmp58^post5 == 0 /\ z519^0-z519^post5 == 0 /\ -constant22^post5+constant22^0 == 0 /\ -lx2^post5+lx2^0 == 0 /\ tmp47^0-tmp47^post5 == 0 /\ -tmp1112^post5+tmp1112^0 == 0 /\ tmp14^0-tmp14^post5 == 0 /\ -z115^post5+z115^0 == 0 /\ tmp36^0-tmp36^post5 == 0 /\ -z418^post5+z418^0 == 0 /\ z216^0-z216^post5 == 0 /\ i20^0-i20^post5 == 0 /\ -tmp69^post5+tmp69^0 == 0 /\ tmp25^0-tmp25^post5 == 0 /\ tmp710^0-tmp710^post5 == 0 /\ -tmp1314^post5+tmp1314^0 == 0 /\ tmp03^0-tmp03^post5 == 0 /\ -z317^post5+z317^0 == 0 /\ tmp1213^0-tmp1213^post5 == 0), cost: 1
   4: l2 -> l0 : tmp1011^0'=tmp1011^post4, z317^0'=z317^post4, tmp58^0'=tmp58^post4, i20^0'=i20^post4, tmp710^0'=tmp710^post4, tmp25^0'=tmp25^post4, z519^0'=z519^post4, tmp1213^0'=tmp1213^post4, tmp03^0'=tmp03^post4, z216^0'=z216^post4, tmp47^0'=tmp47^post4, constant22^0'=constant22^post4, tmp14^0'=tmp14^post4, tmp1112^0'=tmp1112^post4, z418^0'=z418^post4, tmp69^0'=tmp69^post4, lx2^0'=lx2^post4, z115^0'=z115^post4, tmp36^0'=tmp36^post4, tmp1314^0'=tmp1314^post4, (i20^0-i20^post4 == 0 /\ -z519^post4+z519^0 == 0 /\ z317^0-z317^post4 == 0 /\ tmp1011^0-tmp1011^post4 == 0 /\ -z418^post4+z418^0 == 0 /\ -tmp69^post4+tmp69^0 == 0 /\ constant22^0-constant22^post4 == 0 /\ -tmp36^post4+tmp36^0 == 0 /\ tmp03^0-tmp03^post4 == 0 /\ -z216^post4+z216^0 == 0 /\ tmp47^0-tmp47^post4 == 0 /\ -lx2^post4+lx2^0 == 0 /\ tmp58^0-tmp58^post4 == 0 /\ -tmp25^post4+tmp25^0 == 0 /\ -z115^post4+z115^0 == 0 /\ tmp710^0-tmp710^post4 == 0 /\ -tmp1314^post4+tmp1314^0 == 0 /\ tmp1213^0-tmp1213^post4 == 0 /\ -tmp14^post4+tmp14^0 == 0 /\ -tmp1112^post4+tmp1112^0 == 0), cost: 1
   2: l3 -> l4 : tmp1011^0'=tmp1011^post2, z317^0'=z317^post2, tmp58^0'=tmp58^post2, i20^0'=i20^post2, tmp710^0'=tmp710^post2, tmp25^0'=tmp25^post2, z519^0'=z519^post2, tmp1213^0'=tmp1213^post2, tmp03^0'=tmp03^post2, z216^0'=z216^post2, tmp47^0'=tmp47^post2, constant22^0'=constant22^post2, tmp14^0'=tmp14^post2, tmp1112^0'=tmp1112^post2, z418^0'=z418^post2, tmp69^0'=tmp69^post2, lx2^0'=lx2^post2, z115^0'=z115^post2, tmp36^0'=tmp36^post2, tmp1314^0'=tmp1314^post2, (-tmp1314^post2+tmp1314^0 == 0 /\ tmp47^0-tmp47^post2 == 0 /\ tmp14^0-tmp14^post2 == 0 /\ tmp58^0-tmp58^post2 == 0 /\ -z519^post2+z519^0 == 0 /\ i20^0-i20^post2 == 0 /\ -tmp36^post2+tmp36^0 == 0 /\ z115^0-z115^post2 == 0 /\ -constant22^post2+constant22^0 == 0 /\ tmp1011^0-tmp1011^post2 == 0 /\ z216^0-z216^post2 == 0 /\ tmp03^0-tmp03^post2 == 0 /\ 8-i20^0 <= 0 /\ -z418^post2+z418^0 == 0 /\ -tmp710^post2+tmp710^0 == 0 /\ -tmp69^post2+tmp69^0 == 0 /\ tmp25^0-tmp25^post2 == 0 /\ tmp1213^0-tmp1213^post2 == 0 /\ z317^0-z317^post2 == 0 /\ -tmp1112^post2+tmp1112^0 == 0 /\ -lx2^post2+lx2^0 == 0), cost: 1
   3: l3 -> l1 : tmp1011^0'=tmp1011^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=i20^post3, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=z519^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=constant22^post3, tmp14^0'=tmp14^post3, tmp1112^0'=tmp1112^post3, z418^0'=z418^post3, tmp69^0'=tmp69^post3, lx2^0'=lx2^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=tmp1314^post3, (0 == 0 /\ -1-i20^0+i20^post3 == 0 /\ -z317^210-z519^post3+z317^post3 == 0 /\ -12299+constant22^810 == 0 /\ lx2^0-lx2^post3 == 0 /\ -2446+constant22^510 == 0 /\ -7+i20^0 <= 0 /\ 16069+constant22^1110 == 0 /\ -4433+constant22^13 == 0 /\ z317^110-tmp47^110-tmp69^110 == 0 /\ -9633+constant22^410 == 0 /\ -tmp14^post3+tmp25^post3+tmp1213^post3 == 0 /\ 7373+constant22^910 == 0 /\ -6270+constant22^210 == 0 /\ -z418^210+z418^post3-z519^post3 == 0 /\ -tmp14^post3-tmp25^post3+tmp1112^post3 == 0 /\ 20995+constant22^1010 == 0 /\ 15137+constant22^310 == 0 /\ tmp1314^post3+tmp36^post3-tmp03^post3 == 0 /\ -tmp69^110-tmp58^110+z216^110 == 0 /\ z418^110-tmp710^110-tmp58^110 == 0 /\ -16819+constant22^610 == 0 /\ 3196+constant22^post3 == 0 /\ z115^210-tmp47^110-tmp710^110 == 0 /\ -25172+constant22^710 == 0 /\ tmp1011^post3-tmp36^post3-tmp03^post3 == 0), cost: 1
   6: l5 -> l2 : tmp1011^0'=tmp1011^post6, z317^0'=z317^post6, tmp58^0'=tmp58^post6, i20^0'=i20^post6, tmp710^0'=tmp710^post6, tmp25^0'=tmp25^post6, z519^0'=z519^post6, tmp1213^0'=tmp1213^post6, tmp03^0'=tmp03^post6, z216^0'=z216^post6, tmp47^0'=tmp47^post6, constant22^0'=constant22^post6, tmp14^0'=tmp14^post6, tmp1112^0'=tmp1112^post6, z418^0'=z418^post6, tmp69^0'=tmp69^post6, lx2^0'=lx2^post6, z115^0'=z115^post6, tmp36^0'=tmp36^post6, tmp1314^0'=tmp1314^post6, (z519^0-z519^post6 == 0 /\ z216^0-z216^post6 == 0 /\ -tmp710^post6+tmp710^0 == 0 /\ -8+lx2^post6 == 0 /\ tmp14^0-tmp14^post6 == 0 /\ -tmp1314^post6+tmp1314^0 == 0 /\ -z115^post6+z115^0 == 0 /\ -tmp1213^post6+tmp1213^0 == 0 /\ -tmp1112^post6+tmp1112^0 == 0 /\ tmp25^0-tmp25^post6 == 0 /\ tmp1011^0-tmp1011^post6 == 0 /\ z317^0-z317^post6 == 0 /\ z418^0-z418^post6 == 0 /\ tmp58^0-tmp58^post6 == 0 /\ -tmp69^post6+tmp69^0 == 0 /\ i20^post6 == 0 /\ -tmp36^post6+tmp36^0 == 0 /\ tmp03^0-tmp03^post6 == 0 /\ tmp47^0-tmp47^post6 == 0 /\ -constant22^post6+constant22^0 == 0), cost: 1
   7: l6 -> l5 : tmp1011^0'=tmp1011^post7, z317^0'=z317^post7, tmp58^0'=tmp58^post7, i20^0'=i20^post7, tmp710^0'=tmp710^post7, tmp25^0'=tmp25^post7, z519^0'=z519^post7, tmp1213^0'=tmp1213^post7, tmp03^0'=tmp03^post7, z216^0'=z216^post7, tmp47^0'=tmp47^post7, constant22^0'=constant22^post7, tmp14^0'=tmp14^post7, tmp1112^0'=tmp1112^post7, z418^0'=z418^post7, tmp69^0'=tmp69^post7, lx2^0'=lx2^post7, z115^0'=z115^post7, tmp36^0'=tmp36^post7, tmp1314^0'=tmp1314^post7, (tmp25^0-tmp25^post7 == 0 /\ -lx2^post7+lx2^0 == 0 /\ -tmp47^post7+tmp47^0 == 0 /\ tmp58^0-tmp58^post7 == 0 /\ -tmp03^post7+tmp03^0 == 0 /\ tmp1011^0-tmp1011^post7 == 0 /\ -z115^post7+z115^0 == 0 /\ -tmp1213^post7+tmp1213^0 == 0 /\ tmp710^0-tmp710^post7 == 0 /\ z418^0-z418^post7 == 0 /\ -tmp36^post7+tmp36^0 == 0 /\ constant22^0-constant22^post7 == 0 /\ tmp69^0-tmp69^post7 == 0 /\ -tmp14^post7+tmp14^0 == 0 /\ -tmp1112^post7+tmp1112^0 == 0 /\ z216^0-z216^post7 == 0 /\ z317^0-z317^post7 == 0 /\ z519^0-z519^post7 == 0 /\ -i20^post7+i20^0 == 0 /\ -tmp1314^post7+tmp1314^0 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l6
   0: l0 -> l1 : tmp1011^0'=tmp1011^post0, z317^0'=z317^post0, tmp58^0'=tmp58^post0, i20^0'=i20^post0, tmp710^0'=tmp710^post0, tmp25^0'=tmp25^post0, z519^0'=z519^post0, tmp1213^0'=tmp1213^post0, tmp03^0'=tmp03^post0, z216^0'=z216^post0, tmp47^0'=tmp47^post0, constant22^0'=constant22^post0, tmp14^0'=tmp14^post0, tmp1112^0'=tmp1112^post0, z418^0'=z418^post0, tmp69^0'=tmp69^post0, lx2^0'=lx2^post0, z115^0'=z115^post0, tmp36^0'=tmp36^post0, tmp1314^0'=tmp1314^post0, (tmp58^0-tmp58^post0 == 0 /\ tmp1011^0-tmp1011^post0 == 0 /\ -z115^post0+z115^0 == 0 /\ i20^post0 == 0 /\ -tmp1213^post0+tmp1213^0 == 0 /\ -tmp14^post0+tmp14^0 == 0 /\ tmp1112^0-tmp1112^post0 == 0 /\ z519^0-z519^post0 == 0 /\ -z418^post0+z418^0 == 0 /\ z216^0-z216^post0 == 0 /\ tmp47^0-tmp47^post0 == 0 /\ tmp710^0-tmp710^post0 == 0 /\ 8-i20^0 <= 0 /\ -tmp1314^post0+tmp1314^0 == 0 /\ -lx2^post0+lx2^0 == 0 /\ z317^0-z317^post0 == 0 /\ -tmp36^post0+tmp36^0 == 0 /\ -tmp03^post0+tmp03^0 == 0 /\ -constant22^post0+constant22^0 == 0 /\ tmp69^0-tmp69^post0 == 0 /\ tmp25^0-tmp25^post0 == 0), cost: 1
   1: l0 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^post1, tmp58^0'=tmp58^post1, i20^0'=i20^post1, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=tmp1213^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=constant22^post1, tmp14^0'=tmp14^post1, tmp1112^0'=tmp1112^post1, z418^0'=z418^post1, tmp69^0'=tmp69^post1, lx2^0'=lx2^post1, z115^0'=z115^post1, tmp36^0'=tmp36^post1, tmp1314^0'=tmp1314^post1, (0 == 0 /\ -6270+constant22^20 == 0 /\ -z317^20+z317^post1-z519^post1 == 0 /\ -25172+constant22^70 == 0 /\ 20995+constant22^100 == 0 /\ -9633+constant22^40 == 0 /\ -1+i20^post1-i20^0 == 0 /\ -7+i20^0 <= 0 /\ -tmp36^post1+tmp1011^post1-tmp03^post1 == 0 /\ -16819+constant22^60 == 0 /\ tmp1213^post1+tmp25^post1-tmp14^post1 == 0 /\ -tmp58^10+z216^10-tmp69^10 == 0 /\ 16069+constant22^110 == 0 /\ -tmp47^10-tmp710^10+z115^20 == 0 /\ -4433+constant22^12 == 0 /\ 7373+constant22^90 == 0 /\ -2446+constant22^50 == 0 /\ tmp1314^post1+tmp36^post1-tmp03^post1 == 0 /\ 15137+constant22^30 == 0 /\ 3196+constant22^post1 == 0 /\ tmp1112^post1-tmp25^post1-tmp14^post1 == 0 /\ -lx2^post1+lx2^0 == 0 /\ z317^10-tmp47^10-tmp69^10 == 0 /\ -tmp58^10-tmp710^10+z418^10 == 0 /\ z418^post1-z519^post1-z418^20 == 0 /\ -12299+constant22^80 == 0), cost: 1
   5: l1 -> l3 : tmp1011^0'=tmp1011^post5, z317^0'=z317^post5, tmp58^0'=tmp58^post5, i20^0'=i20^post5, tmp710^0'=tmp710^post5, tmp25^0'=tmp25^post5, z519^0'=z519^post5, tmp1213^0'=tmp1213^post5, tmp03^0'=tmp03^post5, z216^0'=z216^post5, tmp47^0'=tmp47^post5, constant22^0'=constant22^post5, tmp14^0'=tmp14^post5, tmp1112^0'=tmp1112^post5, z418^0'=z418^post5, tmp69^0'=tmp69^post5, lx2^0'=lx2^post5, z115^0'=z115^post5, tmp36^0'=tmp36^post5, tmp1314^0'=tmp1314^post5, (tmp1011^0-tmp1011^post5 == 0 /\ tmp58^0-tmp58^post5 == 0 /\ z519^0-z519^post5 == 0 /\ -constant22^post5+constant22^0 == 0 /\ -lx2^post5+lx2^0 == 0 /\ tmp47^0-tmp47^post5 == 0 /\ -tmp1112^post5+tmp1112^0 == 0 /\ tmp14^0-tmp14^post5 == 0 /\ -z115^post5+z115^0 == 0 /\ tmp36^0-tmp36^post5 == 0 /\ -z418^post5+z418^0 == 0 /\ z216^0-z216^post5 == 0 /\ i20^0-i20^post5 == 0 /\ -tmp69^post5+tmp69^0 == 0 /\ tmp25^0-tmp25^post5 == 0 /\ tmp710^0-tmp710^post5 == 0 /\ -tmp1314^post5+tmp1314^0 == 0 /\ tmp03^0-tmp03^post5 == 0 /\ -z317^post5+z317^0 == 0 /\ tmp1213^0-tmp1213^post5 == 0), cost: 1
   4: l2 -> l0 : tmp1011^0'=tmp1011^post4, z317^0'=z317^post4, tmp58^0'=tmp58^post4, i20^0'=i20^post4, tmp710^0'=tmp710^post4, tmp25^0'=tmp25^post4, z519^0'=z519^post4, tmp1213^0'=tmp1213^post4, tmp03^0'=tmp03^post4, z216^0'=z216^post4, tmp47^0'=tmp47^post4, constant22^0'=constant22^post4, tmp14^0'=tmp14^post4, tmp1112^0'=tmp1112^post4, z418^0'=z418^post4, tmp69^0'=tmp69^post4, lx2^0'=lx2^post4, z115^0'=z115^post4, tmp36^0'=tmp36^post4, tmp1314^0'=tmp1314^post4, (i20^0-i20^post4 == 0 /\ -z519^post4+z519^0 == 0 /\ z317^0-z317^post4 == 0 /\ tmp1011^0-tmp1011^post4 == 0 /\ -z418^post4+z418^0 == 0 /\ -tmp69^post4+tmp69^0 == 0 /\ constant22^0-constant22^post4 == 0 /\ -tmp36^post4+tmp36^0 == 0 /\ tmp03^0-tmp03^post4 == 0 /\ -z216^post4+z216^0 == 0 /\ tmp47^0-tmp47^post4 == 0 /\ -lx2^post4+lx2^0 == 0 /\ tmp58^0-tmp58^post4 == 0 /\ -tmp25^post4+tmp25^0 == 0 /\ -z115^post4+z115^0 == 0 /\ tmp710^0-tmp710^post4 == 0 /\ -tmp1314^post4+tmp1314^0 == 0 /\ tmp1213^0-tmp1213^post4 == 0 /\ -tmp14^post4+tmp14^0 == 0 /\ -tmp1112^post4+tmp1112^0 == 0), cost: 1
   3: l3 -> l1 : tmp1011^0'=tmp1011^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=i20^post3, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=z519^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=constant22^post3, tmp14^0'=tmp14^post3, tmp1112^0'=tmp1112^post3, z418^0'=z418^post3, tmp69^0'=tmp69^post3, lx2^0'=lx2^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=tmp1314^post3, (0 == 0 /\ -1-i20^0+i20^post3 == 0 /\ -z317^210-z519^post3+z317^post3 == 0 /\ -12299+constant22^810 == 0 /\ lx2^0-lx2^post3 == 0 /\ -2446+constant22^510 == 0 /\ -7+i20^0 <= 0 /\ 16069+constant22^1110 == 0 /\ -4433+constant22^13 == 0 /\ z317^110-tmp47^110-tmp69^110 == 0 /\ -9633+constant22^410 == 0 /\ -tmp14^post3+tmp25^post3+tmp1213^post3 == 0 /\ 7373+constant22^910 == 0 /\ -6270+constant22^210 == 0 /\ -z418^210+z418^post3-z519^post3 == 0 /\ -tmp14^post3-tmp25^post3+tmp1112^post3 == 0 /\ 20995+constant22^1010 == 0 /\ 15137+constant22^310 == 0 /\ tmp1314^post3+tmp36^post3-tmp03^post3 == 0 /\ -tmp69^110-tmp58^110+z216^110 == 0 /\ z418^110-tmp710^110-tmp58^110 == 0 /\ -16819+constant22^610 == 0 /\ 3196+constant22^post3 == 0 /\ z115^210-tmp47^110-tmp710^110 == 0 /\ -25172+constant22^710 == 0 /\ tmp1011^post3-tmp36^post3-tmp03^post3 == 0), cost: 1
   6: l5 -> l2 : tmp1011^0'=tmp1011^post6, z317^0'=z317^post6, tmp58^0'=tmp58^post6, i20^0'=i20^post6, tmp710^0'=tmp710^post6, tmp25^0'=tmp25^post6, z519^0'=z519^post6, tmp1213^0'=tmp1213^post6, tmp03^0'=tmp03^post6, z216^0'=z216^post6, tmp47^0'=tmp47^post6, constant22^0'=constant22^post6, tmp14^0'=tmp14^post6, tmp1112^0'=tmp1112^post6, z418^0'=z418^post6, tmp69^0'=tmp69^post6, lx2^0'=lx2^post6, z115^0'=z115^post6, tmp36^0'=tmp36^post6, tmp1314^0'=tmp1314^post6, (z519^0-z519^post6 == 0 /\ z216^0-z216^post6 == 0 /\ -tmp710^post6+tmp710^0 == 0 /\ -8+lx2^post6 == 0 /\ tmp14^0-tmp14^post6 == 0 /\ -tmp1314^post6+tmp1314^0 == 0 /\ -z115^post6+z115^0 == 0 /\ -tmp1213^post6+tmp1213^0 == 0 /\ -tmp1112^post6+tmp1112^0 == 0 /\ tmp25^0-tmp25^post6 == 0 /\ tmp1011^0-tmp1011^post6 == 0 /\ z317^0-z317^post6 == 0 /\ z418^0-z418^post6 == 0 /\ tmp58^0-tmp58^post6 == 0 /\ -tmp69^post6+tmp69^0 == 0 /\ i20^post6 == 0 /\ -tmp36^post6+tmp36^0 == 0 /\ tmp03^0-tmp03^post6 == 0 /\ tmp47^0-tmp47^post6 == 0 /\ -constant22^post6+constant22^0 == 0), cost: 1
   7: l6 -> l5 : tmp1011^0'=tmp1011^post7, z317^0'=z317^post7, tmp58^0'=tmp58^post7, i20^0'=i20^post7, tmp710^0'=tmp710^post7, tmp25^0'=tmp25^post7, z519^0'=z519^post7, tmp1213^0'=tmp1213^post7, tmp03^0'=tmp03^post7, z216^0'=z216^post7, tmp47^0'=tmp47^post7, constant22^0'=constant22^post7, tmp14^0'=tmp14^post7, tmp1112^0'=tmp1112^post7, z418^0'=z418^post7, tmp69^0'=tmp69^post7, lx2^0'=lx2^post7, z115^0'=z115^post7, tmp36^0'=tmp36^post7, tmp1314^0'=tmp1314^post7, (tmp25^0-tmp25^post7 == 0 /\ -lx2^post7+lx2^0 == 0 /\ -tmp47^post7+tmp47^0 == 0 /\ tmp58^0-tmp58^post7 == 0 /\ -tmp03^post7+tmp03^0 == 0 /\ tmp1011^0-tmp1011^post7 == 0 /\ -z115^post7+z115^0 == 0 /\ -tmp1213^post7+tmp1213^0 == 0 /\ tmp710^0-tmp710^post7 == 0 /\ z418^0-z418^post7 == 0 /\ -tmp36^post7+tmp36^0 == 0 /\ constant22^0-constant22^post7 == 0 /\ tmp69^0-tmp69^post7 == 0 /\ -tmp14^post7+tmp14^0 == 0 /\ -tmp1112^post7+tmp1112^0 == 0 /\ z216^0-z216^post7 == 0 /\ z317^0-z317^post7 == 0 /\ z519^0-z519^post7 == 0 /\ -i20^post7+i20^0 == 0 /\ -tmp1314^post7+tmp1314^0 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : tmp1011^0'=tmp1011^post0, z317^0'=z317^post0, tmp58^0'=tmp58^post0, i20^0'=i20^post0, tmp710^0'=tmp710^post0, tmp25^0'=tmp25^post0, z519^0'=z519^post0, tmp1213^0'=tmp1213^post0, tmp03^0'=tmp03^post0, z216^0'=z216^post0, tmp47^0'=tmp47^post0, constant22^0'=constant22^post0, tmp14^0'=tmp14^post0, tmp1112^0'=tmp1112^post0, z418^0'=z418^post0, tmp69^0'=tmp69^post0, lx2^0'=lx2^post0, z115^0'=z115^post0, tmp36^0'=tmp36^post0, tmp1314^0'=tmp1314^post0, (tmp58^0-tmp58^post0 == 0 /\ tmp1011^0-tmp1011^post0 == 0 /\ -z115^post0+z115^0 == 0 /\ i20^post0 == 0 /\ -tmp1213^post0+tmp1213^0 == 0 /\ -tmp14^post0+tmp14^0 == 0 /\ tmp1112^0-tmp1112^post0 == 0 /\ z519^0-z519^post0 == 0 /\ -z418^post0+z418^0 == 0 /\ z216^0-z216^post0 == 0 /\ tmp47^0-tmp47^post0 == 0 /\ tmp710^0-tmp710^post0 == 0 /\ 8-i20^0 <= 0 /\ -tmp1314^post0+tmp1314^0 == 0 /\ -lx2^post0+lx2^0 == 0 /\ z317^0-z317^post0 == 0 /\ -tmp36^post0+tmp36^0 == 0 /\ -tmp03^post0+tmp03^0 == 0 /\ -constant22^post0+constant22^0 == 0 /\ tmp69^0-tmp69^post0 == 0 /\ tmp25^0-tmp25^post0 == 0), cost: 1
New rule:
l0 -> l1 : i20^0'=0, -8+i20^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l0 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^post1, tmp58^0'=tmp58^post1, i20^0'=i20^post1, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=tmp1213^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=constant22^post1, tmp14^0'=tmp14^post1, tmp1112^0'=tmp1112^post1, z418^0'=z418^post1, tmp69^0'=tmp69^post1, lx2^0'=lx2^post1, z115^0'=z115^post1, tmp36^0'=tmp36^post1, tmp1314^0'=tmp1314^post1, (0 == 0 /\ -6270+constant22^20 == 0 /\ -z317^20+z317^post1-z519^post1 == 0 /\ -25172+constant22^70 == 0 /\ 20995+constant22^100 == 0 /\ -9633+constant22^40 == 0 /\ -1+i20^post1-i20^0 == 0 /\ -7+i20^0 <= 0 /\ -tmp36^post1+tmp1011^post1-tmp03^post1 == 0 /\ -16819+constant22^60 == 0 /\ tmp1213^post1+tmp25^post1-tmp14^post1 == 0 /\ -tmp58^10+z216^10-tmp69^10 == 0 /\ 16069+constant22^110 == 0 /\ -tmp47^10-tmp710^10+z115^20 == 0 /\ -4433+constant22^12 == 0 /\ 7373+constant22^90 == 0 /\ -2446+constant22^50 == 0 /\ tmp1314^post1+tmp36^post1-tmp03^post1 == 0 /\ 15137+constant22^30 == 0 /\ 3196+constant22^post1 == 0 /\ tmp1112^post1-tmp25^post1-tmp14^post1 == 0 /\ -lx2^post1+lx2^0 == 0 /\ z317^10-tmp47^10-tmp69^10 == 0 /\ -tmp58^10-tmp710^10+z418^10 == 0 /\ z418^post1-z519^post1-z418^20 == 0 /\ -12299+constant22^80 == 0), cost: 1
New rule:
l0 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=1+i20^0, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, -7+i20^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l1 : tmp1011^0'=tmp1011^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=i20^post3, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=z519^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=constant22^post3, tmp14^0'=tmp14^post3, tmp1112^0'=tmp1112^post3, z418^0'=z418^post3, tmp69^0'=tmp69^post3, lx2^0'=lx2^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=tmp1314^post3, (0 == 0 /\ -1-i20^0+i20^post3 == 0 /\ -z317^210-z519^post3+z317^post3 == 0 /\ -12299+constant22^810 == 0 /\ lx2^0-lx2^post3 == 0 /\ -2446+constant22^510 == 0 /\ -7+i20^0 <= 0 /\ 16069+constant22^1110 == 0 /\ -4433+constant22^13 == 0 /\ z317^110-tmp47^110-tmp69^110 == 0 /\ -9633+constant22^410 == 0 /\ -tmp14^post3+tmp25^post3+tmp1213^post3 == 0 /\ 7373+constant22^910 == 0 /\ -6270+constant22^210 == 0 /\ -z418^210+z418^post3-z519^post3 == 0 /\ -tmp14^post3-tmp25^post3+tmp1112^post3 == 0 /\ 20995+constant22^1010 == 0 /\ 15137+constant22^310 == 0 /\ tmp1314^post3+tmp36^post3-tmp03^post3 == 0 /\ -tmp69^110-tmp58^110+z216^110 == 0 /\ z418^110-tmp710^110-tmp58^110 == 0 /\ -16819+constant22^610 == 0 /\ 3196+constant22^post3 == 0 /\ z115^210-tmp47^110-tmp710^110 == 0 /\ -25172+constant22^710 == 0 /\ tmp1011^post3-tmp36^post3-tmp03^post3 == 0), cost: 1
New rule:
l3 -> l1 : tmp1011^0'=tmp36^post3+tmp03^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=1+i20^0, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=-z317^210+z317^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=-3196, tmp14^0'=tmp25^post3+tmp1213^post3, tmp1112^0'=2*tmp25^post3+tmp1213^post3, z418^0'=-z317^210+z418^210+z317^post3, tmp69^0'=tmp69^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=-tmp36^post3+tmp03^post3, -7+i20^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l0 : tmp1011^0'=tmp1011^post4, z317^0'=z317^post4, tmp58^0'=tmp58^post4, i20^0'=i20^post4, tmp710^0'=tmp710^post4, tmp25^0'=tmp25^post4, z519^0'=z519^post4, tmp1213^0'=tmp1213^post4, tmp03^0'=tmp03^post4, z216^0'=z216^post4, tmp47^0'=tmp47^post4, constant22^0'=constant22^post4, tmp14^0'=tmp14^post4, tmp1112^0'=tmp1112^post4, z418^0'=z418^post4, tmp69^0'=tmp69^post4, lx2^0'=lx2^post4, z115^0'=z115^post4, tmp36^0'=tmp36^post4, tmp1314^0'=tmp1314^post4, (i20^0-i20^post4 == 0 /\ -z519^post4+z519^0 == 0 /\ z317^0-z317^post4 == 0 /\ tmp1011^0-tmp1011^post4 == 0 /\ -z418^post4+z418^0 == 0 /\ -tmp69^post4+tmp69^0 == 0 /\ constant22^0-constant22^post4 == 0 /\ -tmp36^post4+tmp36^0 == 0 /\ tmp03^0-tmp03^post4 == 0 /\ -z216^post4+z216^0 == 0 /\ tmp47^0-tmp47^post4 == 0 /\ -lx2^post4+lx2^0 == 0 /\ tmp58^0-tmp58^post4 == 0 /\ -tmp25^post4+tmp25^0 == 0 /\ -z115^post4+z115^0 == 0 /\ tmp710^0-tmp710^post4 == 0 /\ -tmp1314^post4+tmp1314^0 == 0 /\ tmp1213^0-tmp1213^post4 == 0 /\ -tmp14^post4+tmp14^0 == 0 /\ -tmp1112^post4+tmp1112^0 == 0), cost: 1
New rule:
l2 -> l0 : TRUE, cost: 1

Applied preprocessing
Original rule:
l1 -> l3 : tmp1011^0'=tmp1011^post5, z317^0'=z317^post5, tmp58^0'=tmp58^post5, i20^0'=i20^post5, tmp710^0'=tmp710^post5, tmp25^0'=tmp25^post5, z519^0'=z519^post5, tmp1213^0'=tmp1213^post5, tmp03^0'=tmp03^post5, z216^0'=z216^post5, tmp47^0'=tmp47^post5, constant22^0'=constant22^post5, tmp14^0'=tmp14^post5, tmp1112^0'=tmp1112^post5, z418^0'=z418^post5, tmp69^0'=tmp69^post5, lx2^0'=lx2^post5, z115^0'=z115^post5, tmp36^0'=tmp36^post5, tmp1314^0'=tmp1314^post5, (tmp1011^0-tmp1011^post5 == 0 /\ tmp58^0-tmp58^post5 == 0 /\ z519^0-z519^post5 == 0 /\ -constant22^post5+constant22^0 == 0 /\ -lx2^post5+lx2^0 == 0 /\ tmp47^0-tmp47^post5 == 0 /\ -tmp1112^post5+tmp1112^0 == 0 /\ tmp14^0-tmp14^post5 == 0 /\ -z115^post5+z115^0 == 0 /\ tmp36^0-tmp36^post5 == 0 /\ -z418^post5+z418^0 == 0 /\ z216^0-z216^post5 == 0 /\ i20^0-i20^post5 == 0 /\ -tmp69^post5+tmp69^0 == 0 /\ tmp25^0-tmp25^post5 == 0 /\ tmp710^0-tmp710^post5 == 0 /\ -tmp1314^post5+tmp1314^0 == 0 /\ tmp03^0-tmp03^post5 == 0 /\ -z317^post5+z317^0 == 0 /\ tmp1213^0-tmp1213^post5 == 0), cost: 1
New rule:
l1 -> l3 : TRUE, cost: 1

Applied preprocessing
Original rule:
l5 -> l2 : tmp1011^0'=tmp1011^post6, z317^0'=z317^post6, tmp58^0'=tmp58^post6, i20^0'=i20^post6, tmp710^0'=tmp710^post6, tmp25^0'=tmp25^post6, z519^0'=z519^post6, tmp1213^0'=tmp1213^post6, tmp03^0'=tmp03^post6, z216^0'=z216^post6, tmp47^0'=tmp47^post6, constant22^0'=constant22^post6, tmp14^0'=tmp14^post6, tmp1112^0'=tmp1112^post6, z418^0'=z418^post6, tmp69^0'=tmp69^post6, lx2^0'=lx2^post6, z115^0'=z115^post6, tmp36^0'=tmp36^post6, tmp1314^0'=tmp1314^post6, (z519^0-z519^post6 == 0 /\ z216^0-z216^post6 == 0 /\ -tmp710^post6+tmp710^0 == 0 /\ -8+lx2^post6 == 0 /\ tmp14^0-tmp14^post6 == 0 /\ -tmp1314^post6+tmp1314^0 == 0 /\ -z115^post6+z115^0 == 0 /\ -tmp1213^post6+tmp1213^0 == 0 /\ -tmp1112^post6+tmp1112^0 == 0 /\ tmp25^0-tmp25^post6 == 0 /\ tmp1011^0-tmp1011^post6 == 0 /\ z317^0-z317^post6 == 0 /\ z418^0-z418^post6 == 0 /\ tmp58^0-tmp58^post6 == 0 /\ -tmp69^post6+tmp69^0 == 0 /\ i20^post6 == 0 /\ -tmp36^post6+tmp36^0 == 0 /\ tmp03^0-tmp03^post6 == 0 /\ tmp47^0-tmp47^post6 == 0 /\ -constant22^post6+constant22^0 == 0), cost: 1
New rule:
l5 -> l2 : i20^0'=0, lx2^0'=8, TRUE, cost: 1

Applied preprocessing
Original rule:
l6 -> l5 : tmp1011^0'=tmp1011^post7, z317^0'=z317^post7, tmp58^0'=tmp58^post7, i20^0'=i20^post7, tmp710^0'=tmp710^post7, tmp25^0'=tmp25^post7, z519^0'=z519^post7, tmp1213^0'=tmp1213^post7, tmp03^0'=tmp03^post7, z216^0'=z216^post7, tmp47^0'=tmp47^post7, constant22^0'=constant22^post7, tmp14^0'=tmp14^post7, tmp1112^0'=tmp1112^post7, z418^0'=z418^post7, tmp69^0'=tmp69^post7, lx2^0'=lx2^post7, z115^0'=z115^post7, tmp36^0'=tmp36^post7, tmp1314^0'=tmp1314^post7, (tmp25^0-tmp25^post7 == 0 /\ -lx2^post7+lx2^0 == 0 /\ -tmp47^post7+tmp47^0 == 0 /\ tmp58^0-tmp58^post7 == 0 /\ -tmp03^post7+tmp03^0 == 0 /\ tmp1011^0-tmp1011^post7 == 0 /\ -z115^post7+z115^0 == 0 /\ -tmp1213^post7+tmp1213^0 == 0 /\ tmp710^0-tmp710^post7 == 0 /\ z418^0-z418^post7 == 0 /\ -tmp36^post7+tmp36^0 == 0 /\ constant22^0-constant22^post7 == 0 /\ tmp69^0-tmp69^post7 == 0 /\ -tmp14^post7+tmp14^0 == 0 /\ -tmp1112^post7+tmp1112^0 == 0 /\ z216^0-z216^post7 == 0 /\ z317^0-z317^post7 == 0 /\ z519^0-z519^post7 == 0 /\ -i20^post7+i20^0 == 0 /\ -tmp1314^post7+tmp1314^0 == 0), cost: 1
New rule:
l6 -> l5 : TRUE, cost: 1

Simplified rules
Start location: l6
   8: l0 -> l1 : i20^0'=0, -8+i20^0 >= 0, cost: 1
   9: l0 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=1+i20^0, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, -7+i20^0 <= 0, cost: 1
  12: l1 -> l3 : TRUE, cost: 1
  11: l2 -> l0 : TRUE, cost: 1
  10: l3 -> l1 : tmp1011^0'=tmp36^post3+tmp03^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=1+i20^0, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=-z317^210+z317^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=-3196, tmp14^0'=tmp25^post3+tmp1213^post3, tmp1112^0'=2*tmp25^post3+tmp1213^post3, z418^0'=-z317^210+z418^210+z317^post3, tmp69^0'=tmp69^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=-tmp36^post3+tmp03^post3, -7+i20^0 <= 0, cost: 1
  13: l5 -> l2 : i20^0'=0, lx2^0'=8, TRUE, cost: 1
  14: l6 -> l5 : TRUE, cost: 1


Eliminating location l5 by chaining:

Applied chaining
First rule:
l6 -> l5 : TRUE, cost: 1
Second rule:
l5 -> l2 : i20^0'=0, lx2^0'=8, TRUE, cost: 1
New rule:
l6 -> l2 : i20^0'=0, lx2^0'=8, TRUE, cost: 2

Applied deletion
Removed the following rules: 13 14

Eliminating location l3 by chaining:

Applied chaining
First rule:
l1 -> l3 : TRUE, cost: 1
Second rule:
l3 -> l1 : tmp1011^0'=tmp36^post3+tmp03^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=1+i20^0, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=-z317^210+z317^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=-3196, tmp14^0'=tmp25^post3+tmp1213^post3, tmp1112^0'=2*tmp25^post3+tmp1213^post3, z418^0'=-z317^210+z418^210+z317^post3, tmp69^0'=tmp69^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=-tmp36^post3+tmp03^post3, -7+i20^0 <= 0, cost: 1
New rule:
l1 -> l1 : tmp1011^0'=tmp36^post3+tmp03^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=1+i20^0, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=-z317^210+z317^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=-3196, tmp14^0'=tmp25^post3+tmp1213^post3, tmp1112^0'=2*tmp25^post3+tmp1213^post3, z418^0'=-z317^210+z418^210+z317^post3, tmp69^0'=tmp69^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=-tmp36^post3+tmp03^post3, -7+i20^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 10 12

Eliminated locations on linear paths
Start location: l6
   8: l0 -> l1 : i20^0'=0, -8+i20^0 >= 0, cost: 1
   9: l0 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=1+i20^0, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, -7+i20^0 <= 0, cost: 1
  16: l1 -> l1 : tmp1011^0'=tmp36^post3+tmp03^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=1+i20^0, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=-z317^210+z317^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=-3196, tmp14^0'=tmp25^post3+tmp1213^post3, tmp1112^0'=2*tmp25^post3+tmp1213^post3, z418^0'=-z317^210+z418^210+z317^post3, tmp69^0'=tmp69^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=-tmp36^post3+tmp03^post3, -7+i20^0 <= 0, cost: 2
  11: l2 -> l0 : TRUE, cost: 1
  15: l6 -> l2 : i20^0'=0, lx2^0'=8, TRUE, cost: 2


Applied acceleration
Original rule:
l1 -> l1 : tmp1011^0'=tmp36^post3+tmp03^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=1+i20^0, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=-z317^210+z317^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=-3196, tmp14^0'=tmp25^post3+tmp1213^post3, tmp1112^0'=2*tmp25^post3+tmp1213^post3, z418^0'=-z317^210+z418^210+z317^post3, tmp69^0'=tmp69^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=-tmp36^post3+tmp03^post3, -7+i20^0 <= 0, cost: 2
New rule:
l1 -> l1 : tmp1011^0'=tmp36^post3+tmp03^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=i20^0+n, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=-z317^210+z317^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=-3196, tmp14^0'=tmp25^post3+tmp1213^post3, tmp1112^0'=2*tmp25^post3+tmp1213^post3, z418^0'=-z317^210+z418^210+z317^post3, tmp69^0'=tmp69^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=-tmp36^post3+tmp03^post3, (-1+n >= 0 /\ 8-i20^0-n >= 0), cost: 2*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_JHLNfB.txt

Applied instantiation
Original rule:
l1 -> l1 : tmp1011^0'=tmp36^post3+tmp03^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=i20^0+n, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=-z317^210+z317^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=-3196, tmp14^0'=tmp25^post3+tmp1213^post3, tmp1112^0'=2*tmp25^post3+tmp1213^post3, z418^0'=-z317^210+z418^210+z317^post3, tmp69^0'=tmp69^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=-tmp36^post3+tmp03^post3, (-1+n >= 0 /\ 8-i20^0-n >= 0), cost: 2*n
New rule:
l1 -> l1 : tmp1011^0'=tmp36^post3+tmp03^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=8, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=-z317^210+z317^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=-3196, tmp14^0'=tmp25^post3+tmp1213^post3, tmp1112^0'=2*tmp25^post3+tmp1213^post3, z418^0'=-z317^210+z418^210+z317^post3, tmp69^0'=tmp69^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=-tmp36^post3+tmp03^post3, (0 >= 0 /\ 7-i20^0 >= 0), cost: 16-2*i20^0

Applied simplification
Original rule:
l1 -> l1 : tmp1011^0'=tmp36^post3+tmp03^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=8, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=-z317^210+z317^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=-3196, tmp14^0'=tmp25^post3+tmp1213^post3, tmp1112^0'=2*tmp25^post3+tmp1213^post3, z418^0'=-z317^210+z418^210+z317^post3, tmp69^0'=tmp69^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=-tmp36^post3+tmp03^post3, (0 >= 0 /\ 7-i20^0 >= 0), cost: 16-2*i20^0
New rule:
l1 -> l1 : tmp1011^0'=tmp36^post3+tmp03^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=8, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=-z317^210+z317^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=-3196, tmp14^0'=tmp25^post3+tmp1213^post3, tmp1112^0'=2*tmp25^post3+tmp1213^post3, z418^0'=-z317^210+z418^210+z317^post3, tmp69^0'=tmp69^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=-tmp36^post3+tmp03^post3, -7+i20^0 <= 0, cost: 16-2*i20^0

Applied deletion
Removed the following rules: 16

Accelerated simple loops
Start location: l6
   8: l0 -> l1 : i20^0'=0, -8+i20^0 >= 0, cost: 1
   9: l0 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=1+i20^0, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, -7+i20^0 <= 0, cost: 1
  18: l1 -> l1 : tmp1011^0'=tmp36^post3+tmp03^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=8, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=-z317^210+z317^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=-3196, tmp14^0'=tmp25^post3+tmp1213^post3, tmp1112^0'=2*tmp25^post3+tmp1213^post3, z418^0'=-z317^210+z418^210+z317^post3, tmp69^0'=tmp69^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=-tmp36^post3+tmp03^post3, -7+i20^0 <= 0, cost: 16-2*i20^0
  11: l2 -> l0 : TRUE, cost: 1
  15: l6 -> l2 : i20^0'=0, lx2^0'=8, TRUE, cost: 2


Applied chaining
First rule:
l0 -> l1 : i20^0'=0, -8+i20^0 >= 0, cost: 1
Second rule:
l1 -> l1 : tmp1011^0'=tmp36^post3+tmp03^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=8, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=-z317^210+z317^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=-3196, tmp14^0'=tmp25^post3+tmp1213^post3, tmp1112^0'=2*tmp25^post3+tmp1213^post3, z418^0'=-z317^210+z418^210+z317^post3, tmp69^0'=tmp69^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=-tmp36^post3+tmp03^post3, -7+i20^0 <= 0, cost: 16-2*i20^0
New rule:
l0 -> l1 : tmp1011^0'=tmp36^post3+tmp03^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=8, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=-z317^210+z317^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=-3196, tmp14^0'=tmp25^post3+tmp1213^post3, tmp1112^0'=2*tmp25^post3+tmp1213^post3, z418^0'=-z317^210+z418^210+z317^post3, tmp69^0'=tmp69^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=-tmp36^post3+tmp03^post3, -8+i20^0 >= 0, cost: 17

Applied deletion
Removed the following rules: 18

Chained accelerated rules with incoming rules
Start location: l6
   8: l0 -> l1 : i20^0'=0, -8+i20^0 >= 0, cost: 1
   9: l0 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=1+i20^0, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, -7+i20^0 <= 0, cost: 1
  19: l0 -> l1 : tmp1011^0'=tmp36^post3+tmp03^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, i20^0'=8, tmp710^0'=tmp710^post3, tmp25^0'=tmp25^post3, z519^0'=-z317^210+z317^post3, tmp1213^0'=tmp1213^post3, tmp03^0'=tmp03^post3, z216^0'=z216^post3, tmp47^0'=tmp47^post3, constant22^0'=-3196, tmp14^0'=tmp25^post3+tmp1213^post3, tmp1112^0'=2*tmp25^post3+tmp1213^post3, z418^0'=-z317^210+z418^210+z317^post3, tmp69^0'=tmp69^post3, z115^0'=z115^post3, tmp36^0'=tmp36^post3, tmp1314^0'=-tmp36^post3+tmp03^post3, -8+i20^0 >= 0, cost: 17
  11: l2 -> l0 : TRUE, cost: 1
  15: l6 -> l2 : i20^0'=0, lx2^0'=8, TRUE, cost: 2


Removed unreachable locations and irrelevant leafs
Start location: l6
   9: l0 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=1+i20^0, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, -7+i20^0 <= 0, cost: 1
  11: l2 -> l0 : TRUE, cost: 1
  15: l6 -> l2 : i20^0'=0, lx2^0'=8, TRUE, cost: 2


Eliminating location l0 by chaining:

Applied chaining
First rule:
l2 -> l0 : TRUE, cost: 1
Second rule:
l0 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=1+i20^0, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, -7+i20^0 <= 0, cost: 1
New rule:
l2 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=1+i20^0, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, -7+i20^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 9 11

Eliminated locations on linear paths
Start location: l6
  20: l2 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=1+i20^0, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, -7+i20^0 <= 0, cost: 2
  15: l6 -> l2 : i20^0'=0, lx2^0'=8, TRUE, cost: 2


Applied acceleration
Original rule:
l2 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=1+i20^0, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, -7+i20^0 <= 0, cost: 2
New rule:
l2 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=i20^0+n0, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, (8-i20^0-n0 >= 0 /\ -1+n0 >= 0), cost: 2*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_pCcBFd.txt

Applied instantiation
Original rule:
l2 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=i20^0+n0, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, (8-i20^0-n0 >= 0 /\ -1+n0 >= 0), cost: 2*n0
New rule:
l2 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=8, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, (0 >= 0 /\ 7-i20^0 >= 0), cost: 16-2*i20^0

Applied simplification
Original rule:
l2 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=8, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, (0 >= 0 /\ 7-i20^0 >= 0), cost: 16-2*i20^0
New rule:
l2 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=8, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, -7+i20^0 <= 0, cost: 16-2*i20^0

Applied deletion
Removed the following rules: 20

Accelerated simple loops
Start location: l6
  22: l2 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=8, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, -7+i20^0 <= 0, cost: 16-2*i20^0
  15: l6 -> l2 : i20^0'=0, lx2^0'=8, TRUE, cost: 2


Applied chaining
First rule:
l6 -> l2 : i20^0'=0, lx2^0'=8, TRUE, cost: 2
Second rule:
l2 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=8, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, -7+i20^0 <= 0, cost: 16-2*i20^0
New rule:
l6 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=8, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, lx2^0'=8, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, -7 <= 0, cost: 18

Applied deletion
Removed the following rules: 22

Chained accelerated rules with incoming rules
Start location: l6
  15: l6 -> l2 : i20^0'=0, lx2^0'=8, TRUE, cost: 2
  23: l6 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z317^20+z519^post1, tmp58^0'=tmp58^post1, i20^0'=8, tmp710^0'=tmp710^post1, tmp25^0'=tmp25^post1, z519^0'=z519^post1, tmp1213^0'=-tmp25^post1+tmp14^post1, tmp03^0'=tmp03^post1, z216^0'=z216^post1, tmp47^0'=tmp47^post1, constant22^0'=-3196, tmp14^0'=tmp14^post1, tmp1112^0'=tmp25^post1+tmp14^post1, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, lx2^0'=8, z115^0'=z115^post1, tmp36^0'=tmp1011^post1-tmp03^post1, tmp1314^0'=-tmp1011^post1+2*tmp03^post1, -7 <= 0, cost: 18


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


Computing asymptotic complexity

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

Solved cost: 0
Rule cost:   0