WORST_CASE(Omega(0),?)

Initial ITS
Start location: l6
   0: l0 -> l1 : __const_20995^0'=__const_20995^post0, tmp1011^0'=tmp1011^post0, __const_9633^0'=__const_9633^post0, z317^0'=z317^post0, tmp58^0'=tmp58^post0, __const_15137^0'=__const_15137^post0, i20^0'=i20^post0, __const_6270^0'=__const_6270^post0, tmp25^0'=tmp25^post0, tmp1213^0'=tmp1213^post0, z519^0'=z519^post0, tmp710^0'=tmp710^post0, __const_25172^0'=__const_25172^post0, __const_16819^0'=__const_16819^post0, tmp03^0'=tmp03^post0, __const_8^0'=__const_8^post0, tmp47^0'=tmp47^post0, tmp14^0'=tmp14^post0, __const_12299^0'=__const_12299^post0, z216^0'=z216^post0, __const_4433^0'=__const_4433^post0, __const_2446^0'=__const_2446^post0, tmp1112^0'=tmp1112^post0, constant22^0'=constant22^post0, z418^0'=z418^post0, tmp69^0'=tmp69^post0, __const_16069^0'=__const_16069^post0, lx2^0'=lx2^post0, __const_7373^0'=__const_7373^post0, tmp36^0'=tmp36^post0, tmp1314^0'=tmp1314^post0, z115^0'=z115^post0, __const_3196^0'=__const_3196^post0, (__const_16819^0-__const_16819^post0 == 0 /\ tmp14^0-tmp14^post0 == 0 /\ __const_12299^0-__const_12299^post0 == 0 /\ -__const_25172^post0+__const_25172^0 == 0 /\ -constant22^post0+constant22^0 == 0 /\ -__const_16069^post0+__const_16069^0 == 0 /\ z216^0-z216^post0 == 0 /\ -tmp1112^post0+tmp1112^0 == 0 /\ -z115^post0+z115^0 == 0 /\ i20^post0 == 0 /\ -__const_7373^post0+__const_7373^0 == 0 /\ tmp1011^0-tmp1011^post0 == 0 /\ -__const_3196^post0+__const_3196^0 == 0 /\ __const_9633^0-__const_9633^post0 == 0 /\ -tmp69^post0+tmp69^0 == 0 /\ tmp1213^0-tmp1213^post0 == 0 /\ -z418^post0+z418^0 == 0 /\ tmp47^0-tmp47^post0 == 0 /\ tmp03^0-tmp03^post0 == 0 /\ -tmp36^post0+tmp36^0 == 0 /\ __const_2446^0-__const_2446^post0 == 0 /\ tmp710^0-tmp710^post0 == 0 /\ __const_6270^0-__const_6270^post0 == 0 /\ -z317^post0+z317^0 == 0 /\ z519^0-z519^post0 == 0 /\ -__const_4433^post0+__const_4433^0 == 0 /\ tmp58^0-tmp58^post0 == 0 /\ -tmp25^post0+tmp25^0 == 0 /\ -tmp1314^post0+tmp1314^0 == 0 /\ __const_15137^0-__const_15137^post0 == 0 /\ -i20^0+__const_8^0 <= 0 /\ -lx2^post0+lx2^0 == 0 /\ -__const_8^post0+__const_8^0 == 0 /\ __const_20995^0-__const_20995^post0 == 0), cost: 1
   1: l0 -> l2 : __const_20995^0'=__const_20995^post1, tmp1011^0'=tmp1011^post1, __const_9633^0'=__const_9633^post1, z317^0'=z317^post1, tmp58^0'=tmp58^post1, __const_15137^0'=__const_15137^post1, i20^0'=i20^post1, __const_6270^0'=__const_6270^post1, tmp25^0'=tmp25^post1, tmp1213^0'=tmp1213^post1, z519^0'=z519^post1, tmp710^0'=tmp710^post1, __const_25172^0'=__const_25172^post1, __const_16819^0'=__const_16819^post1, tmp03^0'=tmp03^post1, __const_8^0'=__const_8^post1, tmp47^0'=tmp47^post1, tmp14^0'=tmp14^post1, __const_12299^0'=__const_12299^post1, z216^0'=z216^post1, __const_4433^0'=__const_4433^post1, __const_2446^0'=__const_2446^post1, tmp1112^0'=tmp1112^post1, constant22^0'=constant22^post1, z418^0'=z418^post1, tmp69^0'=tmp69^post1, __const_16069^0'=__const_16069^post1, lx2^0'=lx2^post1, __const_7373^0'=__const_7373^post1, tmp36^0'=tmp36^post1, tmp1314^0'=tmp1314^post1, z115^0'=z115^post1, __const_3196^0'=__const_3196^post1, (0 == 0 /\ z317^post1-z519^post1-z317^20 == 0 /\ __const_15137^0+constant22^30 == 0 /\ constant22^12-__const_4433^0 == 0 /\ -__const_9633^0+constant22^40 == 0 /\ constant22^60-__const_16819^0 == 0 /\ -__const_16819^post1+__const_16819^0 == 0 /\ __const_9633^0-__const_9633^post1 == 0 /\ -__const_4433^post1+__const_4433^0 == 0 /\ -__const_7373^post1+__const_7373^0 == 0 /\ constant22^110+__const_16069^0 == 0 /\ constant22^70-__const_25172^0 == 0 /\ -__const_12299^0+constant22^80 == 0 /\ z317^10-tmp69^10-tmp47^10 == 0 /\ tmp1314^post1-tmp03^post1+tmp36^post1 == 0 /\ z216^10-tmp69^10-tmp58^10 == 0 /\ -__const_3196^post1+__const_3196^0 == 0 /\ -tmp710^10+z115^20-tmp47^10 == 0 /\ -1-i20^0+i20^post1 == 0 /\ __const_25172^0-__const_25172^post1 == 0 /\ __const_20995^0+constant22^100 == 0 /\ __const_6270^0-__const_6270^post1 == 0 /\ -lx2^post1+lx2^0 == 0 /\ __const_8^0-__const_8^post1 == 0 /\ z418^post1-z519^post1-z418^20 == 0 /\ -tmp14^post1-tmp25^post1+tmp1112^post1 == 0 /\ 1+i20^0-__const_8^0 <= 0 /\ -__const_15137^post1+__const_15137^0 == 0 /\ __const_2446^0-__const_2446^post1 == 0 /\ constant22^90+__const_7373^0 == 0 /\ -__const_12299^post1+__const_12299^0 == 0 /\ constant22^50-__const_2446^0 == 0 /\ constant22^post1+__const_3196^0 == 0 /\ -tmp14^post1+tmp1213^post1+tmp25^post1 == 0 /\ -tmp03^post1-tmp36^post1+tmp1011^post1 == 0 /\ -__const_6270^0+constant22^20 == 0 /\ __const_20995^0-__const_20995^post1 == 0 /\ -__const_16069^post1+__const_16069^0 == 0 /\ -tmp710^10+z418^10-tmp58^10 == 0), cost: 1
   5: l1 -> l3 : __const_20995^0'=__const_20995^post5, tmp1011^0'=tmp1011^post5, __const_9633^0'=__const_9633^post5, z317^0'=z317^post5, tmp58^0'=tmp58^post5, __const_15137^0'=__const_15137^post5, i20^0'=i20^post5, __const_6270^0'=__const_6270^post5, tmp25^0'=tmp25^post5, tmp1213^0'=tmp1213^post5, z519^0'=z519^post5, tmp710^0'=tmp710^post5, __const_25172^0'=__const_25172^post5, __const_16819^0'=__const_16819^post5, tmp03^0'=tmp03^post5, __const_8^0'=__const_8^post5, tmp47^0'=tmp47^post5, tmp14^0'=tmp14^post5, __const_12299^0'=__const_12299^post5, z216^0'=z216^post5, __const_4433^0'=__const_4433^post5, __const_2446^0'=__const_2446^post5, tmp1112^0'=tmp1112^post5, constant22^0'=constant22^post5, z418^0'=z418^post5, tmp69^0'=tmp69^post5, __const_16069^0'=__const_16069^post5, lx2^0'=lx2^post5, __const_7373^0'=__const_7373^post5, tmp36^0'=tmp36^post5, tmp1314^0'=tmp1314^post5, z115^0'=z115^post5, __const_3196^0'=__const_3196^post5, (-z115^post5+z115^0 == 0 /\ tmp710^0-tmp710^post5 == 0 /\ -tmp1314^post5+tmp1314^0 == 0 /\ tmp03^0-tmp03^post5 == 0 /\ -lx2^post5+lx2^0 == 0 /\ tmp25^0-tmp25^post5 == 0 /\ -z519^post5+z519^0 == 0 /\ -__const_25172^post5+__const_25172^0 == 0 /\ -__const_16069^post5+__const_16069^0 == 0 /\ -__const_16819^post5+__const_16819^0 == 0 /\ __const_9633^0-__const_9633^post5 == 0 /\ constant22^0-constant22^post5 == 0 /\ __const_12299^0-__const_12299^post5 == 0 /\ -__const_3196^post5+__const_3196^0 == 0 /\ __const_8^0-__const_8^post5 == 0 /\ z216^0-z216^post5 == 0 /\ __const_6270^0-__const_6270^post5 == 0 /\ -__const_4433^post5+__const_4433^0 == 0 /\ tmp58^0-tmp58^post5 == 0 /\ -tmp69^post5+tmp69^0 == 0 /\ -z418^post5+z418^0 == 0 /\ __const_15137^0-__const_15137^post5 == 0 /\ -tmp36^post5+tmp36^0 == 0 /\ i20^0-i20^post5 == 0 /\ -__const_2446^post5+__const_2446^0 == 0 /\ -tmp1213^post5+tmp1213^0 == 0 /\ __const_20995^0-__const_20995^post5 == 0 /\ tmp1112^0-tmp1112^post5 == 0 /\ z317^0-z317^post5 == 0 /\ tmp1011^0-tmp1011^post5 == 0 /\ -tmp47^post5+tmp47^0 == 0 /\ tmp14^0-tmp14^post5 == 0 /\ -__const_7373^post5+__const_7373^0 == 0), cost: 1
   4: l2 -> l0 : __const_20995^0'=__const_20995^post4, tmp1011^0'=tmp1011^post4, __const_9633^0'=__const_9633^post4, z317^0'=z317^post4, tmp58^0'=tmp58^post4, __const_15137^0'=__const_15137^post4, i20^0'=i20^post4, __const_6270^0'=__const_6270^post4, tmp25^0'=tmp25^post4, tmp1213^0'=tmp1213^post4, z519^0'=z519^post4, tmp710^0'=tmp710^post4, __const_25172^0'=__const_25172^post4, __const_16819^0'=__const_16819^post4, tmp03^0'=tmp03^post4, __const_8^0'=__const_8^post4, tmp47^0'=tmp47^post4, tmp14^0'=tmp14^post4, __const_12299^0'=__const_12299^post4, z216^0'=z216^post4, __const_4433^0'=__const_4433^post4, __const_2446^0'=__const_2446^post4, tmp1112^0'=tmp1112^post4, constant22^0'=constant22^post4, z418^0'=z418^post4, tmp69^0'=tmp69^post4, __const_16069^0'=__const_16069^post4, lx2^0'=lx2^post4, __const_7373^0'=__const_7373^post4, tmp36^0'=tmp36^post4, tmp1314^0'=tmp1314^post4, z115^0'=z115^post4, __const_3196^0'=__const_3196^post4, (-__const_4433^post4+__const_4433^0 == 0 /\ -tmp69^post4+tmp69^0 == 0 /\ lx2^0-lx2^post4 == 0 /\ z519^0-z519^post4 == 0 /\ tmp58^0-tmp58^post4 == 0 /\ -tmp1314^post4+tmp1314^0 == 0 /\ z317^0-z317^post4 == 0 /\ constant22^0-constant22^post4 == 0 /\ -z115^post4+z115^0 == 0 /\ -__const_12299^post4+__const_12299^0 == 0 /\ -__const_2446^post4+__const_2446^0 == 0 /\ -__const_6270^post4+__const_6270^0 == 0 /\ tmp1213^0-tmp1213^post4 == 0 /\ tmp1011^0-tmp1011^post4 == 0 /\ -__const_16069^post4+__const_16069^0 == 0 /\ i20^0-i20^post4 == 0 /\ tmp1112^0-tmp1112^post4 == 0 /\ -tmp710^post4+tmp710^0 == 0 /\ z418^0-z418^post4 == 0 /\ __const_9633^0-__const_9633^post4 == 0 /\ tmp25^0-tmp25^post4 == 0 /\ -tmp47^post4+tmp47^0 == 0 /\ __const_20995^0-__const_20995^post4 == 0 /\ tmp14^0-tmp14^post4 == 0 /\ tmp03^0-tmp03^post4 == 0 /\ -__const_16819^post4+__const_16819^0 == 0 /\ __const_15137^0-__const_15137^post4 == 0 /\ __const_25172^0-__const_25172^post4 == 0 /\ -__const_7373^post4+__const_7373^0 == 0 /\ -__const_3196^post4+__const_3196^0 == 0 /\ -z216^post4+z216^0 == 0 /\ __const_8^0-__const_8^post4 == 0 /\ -tmp36^post4+tmp36^0 == 0), cost: 1
   2: l3 -> l4 : __const_20995^0'=__const_20995^post2, tmp1011^0'=tmp1011^post2, __const_9633^0'=__const_9633^post2, z317^0'=z317^post2, tmp58^0'=tmp58^post2, __const_15137^0'=__const_15137^post2, i20^0'=i20^post2, __const_6270^0'=__const_6270^post2, tmp25^0'=tmp25^post2, tmp1213^0'=tmp1213^post2, z519^0'=z519^post2, tmp710^0'=tmp710^post2, __const_25172^0'=__const_25172^post2, __const_16819^0'=__const_16819^post2, tmp03^0'=tmp03^post2, __const_8^0'=__const_8^post2, tmp47^0'=tmp47^post2, tmp14^0'=tmp14^post2, __const_12299^0'=__const_12299^post2, z216^0'=z216^post2, __const_4433^0'=__const_4433^post2, __const_2446^0'=__const_2446^post2, tmp1112^0'=tmp1112^post2, constant22^0'=constant22^post2, z418^0'=z418^post2, tmp69^0'=tmp69^post2, __const_16069^0'=__const_16069^post2, lx2^0'=lx2^post2, __const_7373^0'=__const_7373^post2, tmp36^0'=tmp36^post2, tmp1314^0'=tmp1314^post2, z115^0'=z115^post2, __const_3196^0'=__const_3196^post2, (tmp1011^0-tmp1011^post2 == 0 /\ z317^0-z317^post2 == 0 /\ -tmp36^post2+tmp36^0 == 0 /\ tmp14^0-tmp14^post2 == 0 /\ -z418^post2+z418^0 == 0 /\ __const_6270^0-__const_6270^post2 == 0 /\ -__const_3196^post2+__const_3196^0 == 0 /\ -z519^post2+z519^0 == 0 /\ -__const_4433^post2+__const_4433^0 == 0 /\ -__const_16069^post2+__const_16069^0 == 0 /\ -tmp69^post2+tmp69^0 == 0 /\ -tmp1314^post2+tmp1314^0 == 0 /\ -__const_8^post2+__const_8^0 == 0 /\ -tmp47^post2+tmp47^0 == 0 /\ z216^0-z216^post2 == 0 /\ tmp25^0-tmp25^post2 == 0 /\ __const_20995^0-__const_20995^post2 == 0 /\ __const_2446^0-__const_2446^post2 == 0 /\ __const_15137^0-__const_15137^post2 == 0 /\ -__const_7373^post2+__const_7373^0 == 0 /\ -tmp1213^post2+tmp1213^0 == 0 /\ -z115^post2+z115^0 == 0 /\ -constant22^post2+constant22^0 == 0 /\ -__const_25172^post2+__const_25172^0 == 0 /\ __const_9633^0-__const_9633^post2 == 0 /\ -lx2^post2+lx2^0 == 0 /\ __const_12299^0-__const_12299^post2 == 0 /\ __const_16819^0-__const_16819^post2 == 0 /\ -i20^post2+i20^0 == 0 /\ tmp03^0-tmp03^post2 == 0 /\ -tmp1112^post2+tmp1112^0 == 0 /\ -i20^0+__const_8^0 <= 0 /\ tmp710^0-tmp710^post2 == 0 /\ tmp58^0-tmp58^post2 == 0), cost: 1
   3: l3 -> l1 : __const_20995^0'=__const_20995^post3, tmp1011^0'=tmp1011^post3, __const_9633^0'=__const_9633^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, __const_15137^0'=__const_15137^post3, i20^0'=i20^post3, __const_6270^0'=__const_6270^post3, tmp25^0'=tmp25^post3, tmp1213^0'=tmp1213^post3, z519^0'=z519^post3, tmp710^0'=tmp710^post3, __const_25172^0'=__const_25172^post3, __const_16819^0'=__const_16819^post3, tmp03^0'=tmp03^post3, __const_8^0'=__const_8^post3, tmp47^0'=tmp47^post3, tmp14^0'=tmp14^post3, __const_12299^0'=__const_12299^post3, z216^0'=z216^post3, __const_4433^0'=__const_4433^post3, __const_2446^0'=__const_2446^post3, tmp1112^0'=tmp1112^post3, constant22^0'=constant22^post3, z418^0'=z418^post3, tmp69^0'=tmp69^post3, __const_16069^0'=__const_16069^post3, lx2^0'=lx2^post3, __const_7373^0'=__const_7373^post3, tmp36^0'=tmp36^post3, tmp1314^0'=tmp1314^post3, z115^0'=z115^post3, __const_3196^0'=__const_3196^post3, (0 == 0 /\ __const_20995^0+constant22^1010 == 0 /\ constant22^810-__const_12299^0 == 0 /\ -__const_7373^post3+__const_7373^0 == 0 /\ __const_6270^0-__const_6270^post3 == 0 /\ __const_9633^0-__const_9633^post3 == 0 /\ -__const_16069^post3+__const_16069^0 == 0 /\ -__const_16819^0+constant22^610 == 0 /\ -z519^post3-z418^210+z418^post3 == 0 /\ __const_16819^0-__const_16819^post3 == 0 /\ constant22^710-__const_25172^0 == 0 /\ -tmp03^post3+tmp36^post3+tmp1314^post3 == 0 /\ __const_15137^0+constant22^310 == 0 /\ -__const_25172^post3+__const_25172^0 == 0 /\ -__const_4433^post3+__const_4433^0 == 0 /\ -__const_4433^0+constant22^13 == 0 /\ -lx2^post3+lx2^0 == 0 /\ __const_16069^0+constant22^1110 == 0 /\ -__const_3196^post3+__const_3196^0 == 0 /\ z317^post3-z519^post3-z317^210 == 0 /\ -tmp03^post3-tmp36^post3+tmp1011^post3 == 0 /\ -1-i20^0+i20^post3 == 0 /\ __const_20995^0-__const_20995^post3 == 0 /\ -tmp47^110+z115^210-tmp710^110 == 0 /\ constant22^510-__const_2446^0 == 0 /\ 1+i20^0-__const_8^0 <= 0 /\ -__const_9633^0+constant22^410 == 0 /\ -tmp47^110+z317^110-tmp69^110 == 0 /\ tmp25^post3-tmp14^post3+tmp1213^post3 == 0 /\ constant22^910+__const_7373^0 == 0 /\ tmp1112^post3-tmp25^post3-tmp14^post3 == 0 /\ -tmp58^110-tmp710^110+z418^110 == 0 /\ -tmp69^110-tmp58^110+z216^110 == 0 /\ __const_12299^0-__const_12299^post3 == 0 /\ __const_2446^0-__const_2446^post3 == 0 /\ __const_8^0-__const_8^post3 == 0 /\ constant22^210-__const_6270^0 == 0 /\ constant22^post3+__const_3196^0 == 0 /\ __const_15137^0-__const_15137^post3 == 0), cost: 1
   6: l5 -> l2 : __const_20995^0'=__const_20995^post6, tmp1011^0'=tmp1011^post6, __const_9633^0'=__const_9633^post6, z317^0'=z317^post6, tmp58^0'=tmp58^post6, __const_15137^0'=__const_15137^post6, i20^0'=i20^post6, __const_6270^0'=__const_6270^post6, tmp25^0'=tmp25^post6, tmp1213^0'=tmp1213^post6, z519^0'=z519^post6, tmp710^0'=tmp710^post6, __const_25172^0'=__const_25172^post6, __const_16819^0'=__const_16819^post6, tmp03^0'=tmp03^post6, __const_8^0'=__const_8^post6, tmp47^0'=tmp47^post6, tmp14^0'=tmp14^post6, __const_12299^0'=__const_12299^post6, z216^0'=z216^post6, __const_4433^0'=__const_4433^post6, __const_2446^0'=__const_2446^post6, tmp1112^0'=tmp1112^post6, constant22^0'=constant22^post6, z418^0'=z418^post6, tmp69^0'=tmp69^post6, __const_16069^0'=__const_16069^post6, lx2^0'=lx2^post6, __const_7373^0'=__const_7373^post6, tmp36^0'=tmp36^post6, tmp1314^0'=tmp1314^post6, z115^0'=z115^post6, __const_3196^0'=__const_3196^post6, (-__const_25172^post6+__const_25172^0 == 0 /\ __const_6270^0-__const_6270^post6 == 0 /\ __const_16819^0-__const_16819^post6 == 0 /\ -tmp1112^post6+tmp1112^0 == 0 /\ tmp14^0-tmp14^post6 == 0 /\ tmp1213^0-tmp1213^post6 == 0 /\ __const_12299^0-__const_12299^post6 == 0 /\ -__const_7373^post6+__const_7373^0 == 0 /\ -tmp47^post6+tmp47^0 == 0 /\ z216^0-z216^post6 == 0 /\ -z115^post6+z115^0 == 0 /\ -z519^post6+z519^0 == 0 /\ z317^0-z317^post6 == 0 /\ tmp58^0-tmp58^post6 == 0 /\ __const_16069^0-__const_16069^post6 == 0 /\ -z418^post6+z418^0 == 0 /\ __const_2446^0-__const_2446^post6 == 0 /\ -tmp25^post6+tmp25^0 == 0 /\ lx2^post6-__const_8^0 == 0 /\ __const_15137^0-__const_15137^post6 == 0 /\ -tmp69^post6+tmp69^0 == 0 /\ __const_20995^0-__const_20995^post6 == 0 /\ -__const_8^post6+__const_8^0 == 0 /\ tmp710^0-tmp710^post6 == 0 /\ tmp1011^0-tmp1011^post6 == 0 /\ -__const_3196^post6+__const_3196^0 == 0 /\ -constant22^post6+constant22^0 == 0 /\ tmp36^0-tmp36^post6 == 0 /\ -tmp1314^post6+tmp1314^0 == 0 /\ -__const_9633^post6+__const_9633^0 == 0 /\ -__const_4433^post6+__const_4433^0 == 0 /\ tmp03^0-tmp03^post6 == 0 /\ i20^post6 == 0), cost: 1
   7: l6 -> l5 : __const_20995^0'=__const_20995^post7, tmp1011^0'=tmp1011^post7, __const_9633^0'=__const_9633^post7, z317^0'=z317^post7, tmp58^0'=tmp58^post7, __const_15137^0'=__const_15137^post7, i20^0'=i20^post7, __const_6270^0'=__const_6270^post7, tmp25^0'=tmp25^post7, tmp1213^0'=tmp1213^post7, z519^0'=z519^post7, tmp710^0'=tmp710^post7, __const_25172^0'=__const_25172^post7, __const_16819^0'=__const_16819^post7, tmp03^0'=tmp03^post7, __const_8^0'=__const_8^post7, tmp47^0'=tmp47^post7, tmp14^0'=tmp14^post7, __const_12299^0'=__const_12299^post7, z216^0'=z216^post7, __const_4433^0'=__const_4433^post7, __const_2446^0'=__const_2446^post7, tmp1112^0'=tmp1112^post7, constant22^0'=constant22^post7, z418^0'=z418^post7, tmp69^0'=tmp69^post7, __const_16069^0'=__const_16069^post7, lx2^0'=lx2^post7, __const_7373^0'=__const_7373^post7, tmp36^0'=tmp36^post7, tmp1314^0'=tmp1314^post7, z115^0'=z115^post7, __const_3196^0'=__const_3196^post7, (-z418^post7+z418^0 == 0 /\ -i20^post7+i20^0 == 0 /\ tmp1011^0-tmp1011^post7 == 0 /\ tmp710^0-tmp710^post7 == 0 /\ __const_12299^0-__const_12299^post7 == 0 /\ -tmp36^post7+tmp36^0 == 0 /\ __const_9633^0-__const_9633^post7 == 0 /\ -tmp03^post7+tmp03^0 == 0 /\ -__const_7373^post7+__const_7373^0 == 0 /\ -__const_3196^post7+__const_3196^0 == 0 /\ -z216^post7+z216^0 == 0 /\ -tmp1314^post7+tmp1314^0 == 0 /\ __const_4433^0-__const_4433^post7 == 0 /\ __const_15137^0-__const_15137^post7 == 0 /\ -lx2^post7+lx2^0 == 0 /\ -tmp25^post7+tmp25^0 == 0 /\ -tmp69^post7+tmp69^0 == 0 /\ -constant22^post7+constant22^0 == 0 /\ __const_16819^0-__const_16819^post7 == 0 /\ __const_2446^0-__const_2446^post7 == 0 /\ -__const_8^post7+__const_8^0 == 0 /\ __const_6270^0-__const_6270^post7 == 0 /\ tmp1213^0-tmp1213^post7 == 0 /\ __const_20995^0-__const_20995^post7 == 0 /\ __const_25172^0-__const_25172^post7 == 0 /\ -z115^post7+z115^0 == 0 /\ tmp58^0-tmp58^post7 == 0 /\ tmp47^0-tmp47^post7 == 0 /\ z519^0-z519^post7 == 0 /\ -tmp14^post7+tmp14^0 == 0 /\ -__const_16069^post7+__const_16069^0 == 0 /\ -z317^post7+z317^0 == 0 /\ -tmp1112^post7+tmp1112^0 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l6
   0: l0 -> l1 : __const_20995^0'=__const_20995^post0, tmp1011^0'=tmp1011^post0, __const_9633^0'=__const_9633^post0, z317^0'=z317^post0, tmp58^0'=tmp58^post0, __const_15137^0'=__const_15137^post0, i20^0'=i20^post0, __const_6270^0'=__const_6270^post0, tmp25^0'=tmp25^post0, tmp1213^0'=tmp1213^post0, z519^0'=z519^post0, tmp710^0'=tmp710^post0, __const_25172^0'=__const_25172^post0, __const_16819^0'=__const_16819^post0, tmp03^0'=tmp03^post0, __const_8^0'=__const_8^post0, tmp47^0'=tmp47^post0, tmp14^0'=tmp14^post0, __const_12299^0'=__const_12299^post0, z216^0'=z216^post0, __const_4433^0'=__const_4433^post0, __const_2446^0'=__const_2446^post0, tmp1112^0'=tmp1112^post0, constant22^0'=constant22^post0, z418^0'=z418^post0, tmp69^0'=tmp69^post0, __const_16069^0'=__const_16069^post0, lx2^0'=lx2^post0, __const_7373^0'=__const_7373^post0, tmp36^0'=tmp36^post0, tmp1314^0'=tmp1314^post0, z115^0'=z115^post0, __const_3196^0'=__const_3196^post0, (__const_16819^0-__const_16819^post0 == 0 /\ tmp14^0-tmp14^post0 == 0 /\ __const_12299^0-__const_12299^post0 == 0 /\ -__const_25172^post0+__const_25172^0 == 0 /\ -constant22^post0+constant22^0 == 0 /\ -__const_16069^post0+__const_16069^0 == 0 /\ z216^0-z216^post0 == 0 /\ -tmp1112^post0+tmp1112^0 == 0 /\ -z115^post0+z115^0 == 0 /\ i20^post0 == 0 /\ -__const_7373^post0+__const_7373^0 == 0 /\ tmp1011^0-tmp1011^post0 == 0 /\ -__const_3196^post0+__const_3196^0 == 0 /\ __const_9633^0-__const_9633^post0 == 0 /\ -tmp69^post0+tmp69^0 == 0 /\ tmp1213^0-tmp1213^post0 == 0 /\ -z418^post0+z418^0 == 0 /\ tmp47^0-tmp47^post0 == 0 /\ tmp03^0-tmp03^post0 == 0 /\ -tmp36^post0+tmp36^0 == 0 /\ __const_2446^0-__const_2446^post0 == 0 /\ tmp710^0-tmp710^post0 == 0 /\ __const_6270^0-__const_6270^post0 == 0 /\ -z317^post0+z317^0 == 0 /\ z519^0-z519^post0 == 0 /\ -__const_4433^post0+__const_4433^0 == 0 /\ tmp58^0-tmp58^post0 == 0 /\ -tmp25^post0+tmp25^0 == 0 /\ -tmp1314^post0+tmp1314^0 == 0 /\ __const_15137^0-__const_15137^post0 == 0 /\ -i20^0+__const_8^0 <= 0 /\ -lx2^post0+lx2^0 == 0 /\ -__const_8^post0+__const_8^0 == 0 /\ __const_20995^0-__const_20995^post0 == 0), cost: 1
   1: l0 -> l2 : __const_20995^0'=__const_20995^post1, tmp1011^0'=tmp1011^post1, __const_9633^0'=__const_9633^post1, z317^0'=z317^post1, tmp58^0'=tmp58^post1, __const_15137^0'=__const_15137^post1, i20^0'=i20^post1, __const_6270^0'=__const_6270^post1, tmp25^0'=tmp25^post1, tmp1213^0'=tmp1213^post1, z519^0'=z519^post1, tmp710^0'=tmp710^post1, __const_25172^0'=__const_25172^post1, __const_16819^0'=__const_16819^post1, tmp03^0'=tmp03^post1, __const_8^0'=__const_8^post1, tmp47^0'=tmp47^post1, tmp14^0'=tmp14^post1, __const_12299^0'=__const_12299^post1, z216^0'=z216^post1, __const_4433^0'=__const_4433^post1, __const_2446^0'=__const_2446^post1, tmp1112^0'=tmp1112^post1, constant22^0'=constant22^post1, z418^0'=z418^post1, tmp69^0'=tmp69^post1, __const_16069^0'=__const_16069^post1, lx2^0'=lx2^post1, __const_7373^0'=__const_7373^post1, tmp36^0'=tmp36^post1, tmp1314^0'=tmp1314^post1, z115^0'=z115^post1, __const_3196^0'=__const_3196^post1, (0 == 0 /\ z317^post1-z519^post1-z317^20 == 0 /\ __const_15137^0+constant22^30 == 0 /\ constant22^12-__const_4433^0 == 0 /\ -__const_9633^0+constant22^40 == 0 /\ constant22^60-__const_16819^0 == 0 /\ -__const_16819^post1+__const_16819^0 == 0 /\ __const_9633^0-__const_9633^post1 == 0 /\ -__const_4433^post1+__const_4433^0 == 0 /\ -__const_7373^post1+__const_7373^0 == 0 /\ constant22^110+__const_16069^0 == 0 /\ constant22^70-__const_25172^0 == 0 /\ -__const_12299^0+constant22^80 == 0 /\ z317^10-tmp69^10-tmp47^10 == 0 /\ tmp1314^post1-tmp03^post1+tmp36^post1 == 0 /\ z216^10-tmp69^10-tmp58^10 == 0 /\ -__const_3196^post1+__const_3196^0 == 0 /\ -tmp710^10+z115^20-tmp47^10 == 0 /\ -1-i20^0+i20^post1 == 0 /\ __const_25172^0-__const_25172^post1 == 0 /\ __const_20995^0+constant22^100 == 0 /\ __const_6270^0-__const_6270^post1 == 0 /\ -lx2^post1+lx2^0 == 0 /\ __const_8^0-__const_8^post1 == 0 /\ z418^post1-z519^post1-z418^20 == 0 /\ -tmp14^post1-tmp25^post1+tmp1112^post1 == 0 /\ 1+i20^0-__const_8^0 <= 0 /\ -__const_15137^post1+__const_15137^0 == 0 /\ __const_2446^0-__const_2446^post1 == 0 /\ constant22^90+__const_7373^0 == 0 /\ -__const_12299^post1+__const_12299^0 == 0 /\ constant22^50-__const_2446^0 == 0 /\ constant22^post1+__const_3196^0 == 0 /\ -tmp14^post1+tmp1213^post1+tmp25^post1 == 0 /\ -tmp03^post1-tmp36^post1+tmp1011^post1 == 0 /\ -__const_6270^0+constant22^20 == 0 /\ __const_20995^0-__const_20995^post1 == 0 /\ -__const_16069^post1+__const_16069^0 == 0 /\ -tmp710^10+z418^10-tmp58^10 == 0), cost: 1
   5: l1 -> l3 : __const_20995^0'=__const_20995^post5, tmp1011^0'=tmp1011^post5, __const_9633^0'=__const_9633^post5, z317^0'=z317^post5, tmp58^0'=tmp58^post5, __const_15137^0'=__const_15137^post5, i20^0'=i20^post5, __const_6270^0'=__const_6270^post5, tmp25^0'=tmp25^post5, tmp1213^0'=tmp1213^post5, z519^0'=z519^post5, tmp710^0'=tmp710^post5, __const_25172^0'=__const_25172^post5, __const_16819^0'=__const_16819^post5, tmp03^0'=tmp03^post5, __const_8^0'=__const_8^post5, tmp47^0'=tmp47^post5, tmp14^0'=tmp14^post5, __const_12299^0'=__const_12299^post5, z216^0'=z216^post5, __const_4433^0'=__const_4433^post5, __const_2446^0'=__const_2446^post5, tmp1112^0'=tmp1112^post5, constant22^0'=constant22^post5, z418^0'=z418^post5, tmp69^0'=tmp69^post5, __const_16069^0'=__const_16069^post5, lx2^0'=lx2^post5, __const_7373^0'=__const_7373^post5, tmp36^0'=tmp36^post5, tmp1314^0'=tmp1314^post5, z115^0'=z115^post5, __const_3196^0'=__const_3196^post5, (-z115^post5+z115^0 == 0 /\ tmp710^0-tmp710^post5 == 0 /\ -tmp1314^post5+tmp1314^0 == 0 /\ tmp03^0-tmp03^post5 == 0 /\ -lx2^post5+lx2^0 == 0 /\ tmp25^0-tmp25^post5 == 0 /\ -z519^post5+z519^0 == 0 /\ -__const_25172^post5+__const_25172^0 == 0 /\ -__const_16069^post5+__const_16069^0 == 0 /\ -__const_16819^post5+__const_16819^0 == 0 /\ __const_9633^0-__const_9633^post5 == 0 /\ constant22^0-constant22^post5 == 0 /\ __const_12299^0-__const_12299^post5 == 0 /\ -__const_3196^post5+__const_3196^0 == 0 /\ __const_8^0-__const_8^post5 == 0 /\ z216^0-z216^post5 == 0 /\ __const_6270^0-__const_6270^post5 == 0 /\ -__const_4433^post5+__const_4433^0 == 0 /\ tmp58^0-tmp58^post5 == 0 /\ -tmp69^post5+tmp69^0 == 0 /\ -z418^post5+z418^0 == 0 /\ __const_15137^0-__const_15137^post5 == 0 /\ -tmp36^post5+tmp36^0 == 0 /\ i20^0-i20^post5 == 0 /\ -__const_2446^post5+__const_2446^0 == 0 /\ -tmp1213^post5+tmp1213^0 == 0 /\ __const_20995^0-__const_20995^post5 == 0 /\ tmp1112^0-tmp1112^post5 == 0 /\ z317^0-z317^post5 == 0 /\ tmp1011^0-tmp1011^post5 == 0 /\ -tmp47^post5+tmp47^0 == 0 /\ tmp14^0-tmp14^post5 == 0 /\ -__const_7373^post5+__const_7373^0 == 0), cost: 1
   4: l2 -> l0 : __const_20995^0'=__const_20995^post4, tmp1011^0'=tmp1011^post4, __const_9633^0'=__const_9633^post4, z317^0'=z317^post4, tmp58^0'=tmp58^post4, __const_15137^0'=__const_15137^post4, i20^0'=i20^post4, __const_6270^0'=__const_6270^post4, tmp25^0'=tmp25^post4, tmp1213^0'=tmp1213^post4, z519^0'=z519^post4, tmp710^0'=tmp710^post4, __const_25172^0'=__const_25172^post4, __const_16819^0'=__const_16819^post4, tmp03^0'=tmp03^post4, __const_8^0'=__const_8^post4, tmp47^0'=tmp47^post4, tmp14^0'=tmp14^post4, __const_12299^0'=__const_12299^post4, z216^0'=z216^post4, __const_4433^0'=__const_4433^post4, __const_2446^0'=__const_2446^post4, tmp1112^0'=tmp1112^post4, constant22^0'=constant22^post4, z418^0'=z418^post4, tmp69^0'=tmp69^post4, __const_16069^0'=__const_16069^post4, lx2^0'=lx2^post4, __const_7373^0'=__const_7373^post4, tmp36^0'=tmp36^post4, tmp1314^0'=tmp1314^post4, z115^0'=z115^post4, __const_3196^0'=__const_3196^post4, (-__const_4433^post4+__const_4433^0 == 0 /\ -tmp69^post4+tmp69^0 == 0 /\ lx2^0-lx2^post4 == 0 /\ z519^0-z519^post4 == 0 /\ tmp58^0-tmp58^post4 == 0 /\ -tmp1314^post4+tmp1314^0 == 0 /\ z317^0-z317^post4 == 0 /\ constant22^0-constant22^post4 == 0 /\ -z115^post4+z115^0 == 0 /\ -__const_12299^post4+__const_12299^0 == 0 /\ -__const_2446^post4+__const_2446^0 == 0 /\ -__const_6270^post4+__const_6270^0 == 0 /\ tmp1213^0-tmp1213^post4 == 0 /\ tmp1011^0-tmp1011^post4 == 0 /\ -__const_16069^post4+__const_16069^0 == 0 /\ i20^0-i20^post4 == 0 /\ tmp1112^0-tmp1112^post4 == 0 /\ -tmp710^post4+tmp710^0 == 0 /\ z418^0-z418^post4 == 0 /\ __const_9633^0-__const_9633^post4 == 0 /\ tmp25^0-tmp25^post4 == 0 /\ -tmp47^post4+tmp47^0 == 0 /\ __const_20995^0-__const_20995^post4 == 0 /\ tmp14^0-tmp14^post4 == 0 /\ tmp03^0-tmp03^post4 == 0 /\ -__const_16819^post4+__const_16819^0 == 0 /\ __const_15137^0-__const_15137^post4 == 0 /\ __const_25172^0-__const_25172^post4 == 0 /\ -__const_7373^post4+__const_7373^0 == 0 /\ -__const_3196^post4+__const_3196^0 == 0 /\ -z216^post4+z216^0 == 0 /\ __const_8^0-__const_8^post4 == 0 /\ -tmp36^post4+tmp36^0 == 0), cost: 1
   3: l3 -> l1 : __const_20995^0'=__const_20995^post3, tmp1011^0'=tmp1011^post3, __const_9633^0'=__const_9633^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, __const_15137^0'=__const_15137^post3, i20^0'=i20^post3, __const_6270^0'=__const_6270^post3, tmp25^0'=tmp25^post3, tmp1213^0'=tmp1213^post3, z519^0'=z519^post3, tmp710^0'=tmp710^post3, __const_25172^0'=__const_25172^post3, __const_16819^0'=__const_16819^post3, tmp03^0'=tmp03^post3, __const_8^0'=__const_8^post3, tmp47^0'=tmp47^post3, tmp14^0'=tmp14^post3, __const_12299^0'=__const_12299^post3, z216^0'=z216^post3, __const_4433^0'=__const_4433^post3, __const_2446^0'=__const_2446^post3, tmp1112^0'=tmp1112^post3, constant22^0'=constant22^post3, z418^0'=z418^post3, tmp69^0'=tmp69^post3, __const_16069^0'=__const_16069^post3, lx2^0'=lx2^post3, __const_7373^0'=__const_7373^post3, tmp36^0'=tmp36^post3, tmp1314^0'=tmp1314^post3, z115^0'=z115^post3, __const_3196^0'=__const_3196^post3, (0 == 0 /\ __const_20995^0+constant22^1010 == 0 /\ constant22^810-__const_12299^0 == 0 /\ -__const_7373^post3+__const_7373^0 == 0 /\ __const_6270^0-__const_6270^post3 == 0 /\ __const_9633^0-__const_9633^post3 == 0 /\ -__const_16069^post3+__const_16069^0 == 0 /\ -__const_16819^0+constant22^610 == 0 /\ -z519^post3-z418^210+z418^post3 == 0 /\ __const_16819^0-__const_16819^post3 == 0 /\ constant22^710-__const_25172^0 == 0 /\ -tmp03^post3+tmp36^post3+tmp1314^post3 == 0 /\ __const_15137^0+constant22^310 == 0 /\ -__const_25172^post3+__const_25172^0 == 0 /\ -__const_4433^post3+__const_4433^0 == 0 /\ -__const_4433^0+constant22^13 == 0 /\ -lx2^post3+lx2^0 == 0 /\ __const_16069^0+constant22^1110 == 0 /\ -__const_3196^post3+__const_3196^0 == 0 /\ z317^post3-z519^post3-z317^210 == 0 /\ -tmp03^post3-tmp36^post3+tmp1011^post3 == 0 /\ -1-i20^0+i20^post3 == 0 /\ __const_20995^0-__const_20995^post3 == 0 /\ -tmp47^110+z115^210-tmp710^110 == 0 /\ constant22^510-__const_2446^0 == 0 /\ 1+i20^0-__const_8^0 <= 0 /\ -__const_9633^0+constant22^410 == 0 /\ -tmp47^110+z317^110-tmp69^110 == 0 /\ tmp25^post3-tmp14^post3+tmp1213^post3 == 0 /\ constant22^910+__const_7373^0 == 0 /\ tmp1112^post3-tmp25^post3-tmp14^post3 == 0 /\ -tmp58^110-tmp710^110+z418^110 == 0 /\ -tmp69^110-tmp58^110+z216^110 == 0 /\ __const_12299^0-__const_12299^post3 == 0 /\ __const_2446^0-__const_2446^post3 == 0 /\ __const_8^0-__const_8^post3 == 0 /\ constant22^210-__const_6270^0 == 0 /\ constant22^post3+__const_3196^0 == 0 /\ __const_15137^0-__const_15137^post3 == 0), cost: 1
   6: l5 -> l2 : __const_20995^0'=__const_20995^post6, tmp1011^0'=tmp1011^post6, __const_9633^0'=__const_9633^post6, z317^0'=z317^post6, tmp58^0'=tmp58^post6, __const_15137^0'=__const_15137^post6, i20^0'=i20^post6, __const_6270^0'=__const_6270^post6, tmp25^0'=tmp25^post6, tmp1213^0'=tmp1213^post6, z519^0'=z519^post6, tmp710^0'=tmp710^post6, __const_25172^0'=__const_25172^post6, __const_16819^0'=__const_16819^post6, tmp03^0'=tmp03^post6, __const_8^0'=__const_8^post6, tmp47^0'=tmp47^post6, tmp14^0'=tmp14^post6, __const_12299^0'=__const_12299^post6, z216^0'=z216^post6, __const_4433^0'=__const_4433^post6, __const_2446^0'=__const_2446^post6, tmp1112^0'=tmp1112^post6, constant22^0'=constant22^post6, z418^0'=z418^post6, tmp69^0'=tmp69^post6, __const_16069^0'=__const_16069^post6, lx2^0'=lx2^post6, __const_7373^0'=__const_7373^post6, tmp36^0'=tmp36^post6, tmp1314^0'=tmp1314^post6, z115^0'=z115^post6, __const_3196^0'=__const_3196^post6, (-__const_25172^post6+__const_25172^0 == 0 /\ __const_6270^0-__const_6270^post6 == 0 /\ __const_16819^0-__const_16819^post6 == 0 /\ -tmp1112^post6+tmp1112^0 == 0 /\ tmp14^0-tmp14^post6 == 0 /\ tmp1213^0-tmp1213^post6 == 0 /\ __const_12299^0-__const_12299^post6 == 0 /\ -__const_7373^post6+__const_7373^0 == 0 /\ -tmp47^post6+tmp47^0 == 0 /\ z216^0-z216^post6 == 0 /\ -z115^post6+z115^0 == 0 /\ -z519^post6+z519^0 == 0 /\ z317^0-z317^post6 == 0 /\ tmp58^0-tmp58^post6 == 0 /\ __const_16069^0-__const_16069^post6 == 0 /\ -z418^post6+z418^0 == 0 /\ __const_2446^0-__const_2446^post6 == 0 /\ -tmp25^post6+tmp25^0 == 0 /\ lx2^post6-__const_8^0 == 0 /\ __const_15137^0-__const_15137^post6 == 0 /\ -tmp69^post6+tmp69^0 == 0 /\ __const_20995^0-__const_20995^post6 == 0 /\ -__const_8^post6+__const_8^0 == 0 /\ tmp710^0-tmp710^post6 == 0 /\ tmp1011^0-tmp1011^post6 == 0 /\ -__const_3196^post6+__const_3196^0 == 0 /\ -constant22^post6+constant22^0 == 0 /\ tmp36^0-tmp36^post6 == 0 /\ -tmp1314^post6+tmp1314^0 == 0 /\ -__const_9633^post6+__const_9633^0 == 0 /\ -__const_4433^post6+__const_4433^0 == 0 /\ tmp03^0-tmp03^post6 == 0 /\ i20^post6 == 0), cost: 1
   7: l6 -> l5 : __const_20995^0'=__const_20995^post7, tmp1011^0'=tmp1011^post7, __const_9633^0'=__const_9633^post7, z317^0'=z317^post7, tmp58^0'=tmp58^post7, __const_15137^0'=__const_15137^post7, i20^0'=i20^post7, __const_6270^0'=__const_6270^post7, tmp25^0'=tmp25^post7, tmp1213^0'=tmp1213^post7, z519^0'=z519^post7, tmp710^0'=tmp710^post7, __const_25172^0'=__const_25172^post7, __const_16819^0'=__const_16819^post7, tmp03^0'=tmp03^post7, __const_8^0'=__const_8^post7, tmp47^0'=tmp47^post7, tmp14^0'=tmp14^post7, __const_12299^0'=__const_12299^post7, z216^0'=z216^post7, __const_4433^0'=__const_4433^post7, __const_2446^0'=__const_2446^post7, tmp1112^0'=tmp1112^post7, constant22^0'=constant22^post7, z418^0'=z418^post7, tmp69^0'=tmp69^post7, __const_16069^0'=__const_16069^post7, lx2^0'=lx2^post7, __const_7373^0'=__const_7373^post7, tmp36^0'=tmp36^post7, tmp1314^0'=tmp1314^post7, z115^0'=z115^post7, __const_3196^0'=__const_3196^post7, (-z418^post7+z418^0 == 0 /\ -i20^post7+i20^0 == 0 /\ tmp1011^0-tmp1011^post7 == 0 /\ tmp710^0-tmp710^post7 == 0 /\ __const_12299^0-__const_12299^post7 == 0 /\ -tmp36^post7+tmp36^0 == 0 /\ __const_9633^0-__const_9633^post7 == 0 /\ -tmp03^post7+tmp03^0 == 0 /\ -__const_7373^post7+__const_7373^0 == 0 /\ -__const_3196^post7+__const_3196^0 == 0 /\ -z216^post7+z216^0 == 0 /\ -tmp1314^post7+tmp1314^0 == 0 /\ __const_4433^0-__const_4433^post7 == 0 /\ __const_15137^0-__const_15137^post7 == 0 /\ -lx2^post7+lx2^0 == 0 /\ -tmp25^post7+tmp25^0 == 0 /\ -tmp69^post7+tmp69^0 == 0 /\ -constant22^post7+constant22^0 == 0 /\ __const_16819^0-__const_16819^post7 == 0 /\ __const_2446^0-__const_2446^post7 == 0 /\ -__const_8^post7+__const_8^0 == 0 /\ __const_6270^0-__const_6270^post7 == 0 /\ tmp1213^0-tmp1213^post7 == 0 /\ __const_20995^0-__const_20995^post7 == 0 /\ __const_25172^0-__const_25172^post7 == 0 /\ -z115^post7+z115^0 == 0 /\ tmp58^0-tmp58^post7 == 0 /\ tmp47^0-tmp47^post7 == 0 /\ z519^0-z519^post7 == 0 /\ -tmp14^post7+tmp14^0 == 0 /\ -__const_16069^post7+__const_16069^0 == 0 /\ -z317^post7+z317^0 == 0 /\ -tmp1112^post7+tmp1112^0 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : __const_20995^0'=__const_20995^post0, tmp1011^0'=tmp1011^post0, __const_9633^0'=__const_9633^post0, z317^0'=z317^post0, tmp58^0'=tmp58^post0, __const_15137^0'=__const_15137^post0, i20^0'=i20^post0, __const_6270^0'=__const_6270^post0, tmp25^0'=tmp25^post0, tmp1213^0'=tmp1213^post0, z519^0'=z519^post0, tmp710^0'=tmp710^post0, __const_25172^0'=__const_25172^post0, __const_16819^0'=__const_16819^post0, tmp03^0'=tmp03^post0, __const_8^0'=__const_8^post0, tmp47^0'=tmp47^post0, tmp14^0'=tmp14^post0, __const_12299^0'=__const_12299^post0, z216^0'=z216^post0, __const_4433^0'=__const_4433^post0, __const_2446^0'=__const_2446^post0, tmp1112^0'=tmp1112^post0, constant22^0'=constant22^post0, z418^0'=z418^post0, tmp69^0'=tmp69^post0, __const_16069^0'=__const_16069^post0, lx2^0'=lx2^post0, __const_7373^0'=__const_7373^post0, tmp36^0'=tmp36^post0, tmp1314^0'=tmp1314^post0, z115^0'=z115^post0, __const_3196^0'=__const_3196^post0, (__const_16819^0-__const_16819^post0 == 0 /\ tmp14^0-tmp14^post0 == 0 /\ __const_12299^0-__const_12299^post0 == 0 /\ -__const_25172^post0+__const_25172^0 == 0 /\ -constant22^post0+constant22^0 == 0 /\ -__const_16069^post0+__const_16069^0 == 0 /\ z216^0-z216^post0 == 0 /\ -tmp1112^post0+tmp1112^0 == 0 /\ -z115^post0+z115^0 == 0 /\ i20^post0 == 0 /\ -__const_7373^post0+__const_7373^0 == 0 /\ tmp1011^0-tmp1011^post0 == 0 /\ -__const_3196^post0+__const_3196^0 == 0 /\ __const_9633^0-__const_9633^post0 == 0 /\ -tmp69^post0+tmp69^0 == 0 /\ tmp1213^0-tmp1213^post0 == 0 /\ -z418^post0+z418^0 == 0 /\ tmp47^0-tmp47^post0 == 0 /\ tmp03^0-tmp03^post0 == 0 /\ -tmp36^post0+tmp36^0 == 0 /\ __const_2446^0-__const_2446^post0 == 0 /\ tmp710^0-tmp710^post0 == 0 /\ __const_6270^0-__const_6270^post0 == 0 /\ -z317^post0+z317^0 == 0 /\ z519^0-z519^post0 == 0 /\ -__const_4433^post0+__const_4433^0 == 0 /\ tmp58^0-tmp58^post0 == 0 /\ -tmp25^post0+tmp25^0 == 0 /\ -tmp1314^post0+tmp1314^0 == 0 /\ __const_15137^0-__const_15137^post0 == 0 /\ -i20^0+__const_8^0 <= 0 /\ -lx2^post0+lx2^0 == 0 /\ -__const_8^post0+__const_8^0 == 0 /\ __const_20995^0-__const_20995^post0 == 0), cost: 1
New rule:
l0 -> l1 : i20^0'=0, -i20^0+__const_8^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l0 -> l2 : __const_20995^0'=__const_20995^post1, tmp1011^0'=tmp1011^post1, __const_9633^0'=__const_9633^post1, z317^0'=z317^post1, tmp58^0'=tmp58^post1, __const_15137^0'=__const_15137^post1, i20^0'=i20^post1, __const_6270^0'=__const_6270^post1, tmp25^0'=tmp25^post1, tmp1213^0'=tmp1213^post1, z519^0'=z519^post1, tmp710^0'=tmp710^post1, __const_25172^0'=__const_25172^post1, __const_16819^0'=__const_16819^post1, tmp03^0'=tmp03^post1, __const_8^0'=__const_8^post1, tmp47^0'=tmp47^post1, tmp14^0'=tmp14^post1, __const_12299^0'=__const_12299^post1, z216^0'=z216^post1, __const_4433^0'=__const_4433^post1, __const_2446^0'=__const_2446^post1, tmp1112^0'=tmp1112^post1, constant22^0'=constant22^post1, z418^0'=z418^post1, tmp69^0'=tmp69^post1, __const_16069^0'=__const_16069^post1, lx2^0'=lx2^post1, __const_7373^0'=__const_7373^post1, tmp36^0'=tmp36^post1, tmp1314^0'=tmp1314^post1, z115^0'=z115^post1, __const_3196^0'=__const_3196^post1, (0 == 0 /\ z317^post1-z519^post1-z317^20 == 0 /\ __const_15137^0+constant22^30 == 0 /\ constant22^12-__const_4433^0 == 0 /\ -__const_9633^0+constant22^40 == 0 /\ constant22^60-__const_16819^0 == 0 /\ -__const_16819^post1+__const_16819^0 == 0 /\ __const_9633^0-__const_9633^post1 == 0 /\ -__const_4433^post1+__const_4433^0 == 0 /\ -__const_7373^post1+__const_7373^0 == 0 /\ constant22^110+__const_16069^0 == 0 /\ constant22^70-__const_25172^0 == 0 /\ -__const_12299^0+constant22^80 == 0 /\ z317^10-tmp69^10-tmp47^10 == 0 /\ tmp1314^post1-tmp03^post1+tmp36^post1 == 0 /\ z216^10-tmp69^10-tmp58^10 == 0 /\ -__const_3196^post1+__const_3196^0 == 0 /\ -tmp710^10+z115^20-tmp47^10 == 0 /\ -1-i20^0+i20^post1 == 0 /\ __const_25172^0-__const_25172^post1 == 0 /\ __const_20995^0+constant22^100 == 0 /\ __const_6270^0-__const_6270^post1 == 0 /\ -lx2^post1+lx2^0 == 0 /\ __const_8^0-__const_8^post1 == 0 /\ z418^post1-z519^post1-z418^20 == 0 /\ -tmp14^post1-tmp25^post1+tmp1112^post1 == 0 /\ 1+i20^0-__const_8^0 <= 0 /\ -__const_15137^post1+__const_15137^0 == 0 /\ __const_2446^0-__const_2446^post1 == 0 /\ constant22^90+__const_7373^0 == 0 /\ -__const_12299^post1+__const_12299^0 == 0 /\ constant22^50-__const_2446^0 == 0 /\ constant22^post1+__const_3196^0 == 0 /\ -tmp14^post1+tmp1213^post1+tmp25^post1 == 0 /\ -tmp03^post1-tmp36^post1+tmp1011^post1 == 0 /\ -__const_6270^0+constant22^20 == 0 /\ __const_20995^0-__const_20995^post1 == 0 /\ -__const_16069^post1+__const_16069^0 == 0 /\ -tmp710^10+z418^10-tmp58^10 == 0), cost: 1
New rule:
l0 -> l2 : tmp1011^0'=tmp1011^post1, z317^0'=z519^post1+z317^20, tmp58^0'=tmp58^post1, i20^0'=1+i20^0, tmp25^0'=tmp25^post1, tmp1213^0'=-2*tmp25^post1+tmp1112^post1, z519^0'=z519^post1, tmp710^0'=tmp710^post1, tmp03^0'=-tmp36^post1+tmp1011^post1, tmp47^0'=tmp47^post1, tmp14^0'=-tmp25^post1+tmp1112^post1, z216^0'=z216^post1, tmp1112^0'=tmp1112^post1, constant22^0'=-__const_3196^0, z418^0'=z519^post1+z418^20, tmp69^0'=tmp69^post1, tmp36^0'=tmp36^post1, tmp1314^0'=-2*tmp36^post1+tmp1011^post1, z115^0'=z115^post1, 1+i20^0-__const_8^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l1 : __const_20995^0'=__const_20995^post3, tmp1011^0'=tmp1011^post3, __const_9633^0'=__const_9633^post3, z317^0'=z317^post3, tmp58^0'=tmp58^post3, __const_15137^0'=__const_15137^post3, i20^0'=i20^post3, __const_6270^0'=__const_6270^post3, tmp25^0'=tmp25^post3, tmp1213^0'=tmp1213^post3, z519^0'=z519^post3, tmp710^0'=tmp710^post3, __const_25172^0'=__const_25172^post3, __const_16819^0'=__const_16819^post3, tmp03^0'=tmp03^post3, __const_8^0'=__const_8^post3, tmp47^0'=tmp47^post3, tmp14^0'=tmp14^post3, __const_12299^0'=__const_12299^post3, z216^0'=z216^post3, __const_4433^0'=__const_4433^post3, __const_2446^0'=__const_2446^post3, tmp1112^0'=tmp1112^post3, constant22^0'=constant22^post3, z418^0'=z418^post3, tmp69^0'=tmp69^post3, __const_16069^0'=__const_16069^post3, lx2^0'=lx2^post3, __const_7373^0'=__const_7373^post3, tmp36^0'=tmp36^post3, tmp1314^0'=tmp1314^post3, z115^0'=z115^post3, __const_3196^0'=__const_3196^post3, (0 == 0 /\ __const_20995^0+constant22^1010 == 0 /\ constant22^810-__const_12299^0 == 0 /\ -__const_7373^post3+__const_7373^0 == 0 /\ __const_6270^0-__const_6270^post3 == 0 /\ __const_9633^0-__const_9633^post3 == 0 /\ -__const_16069^post3+__const_16069^0 == 0 /\ -__const_16819^0+constant22^610 == 0 /\ -z519^post3-z418^210+z418^post3 == 0 /\ __const_16819^0-__const_16819^post3 == 0 /\ constant22^710-__const_25172^0 == 0 /\ -tmp03^post3+tmp36^post3+tmp1314^post3 == 0 /\ __const_15137^0+constant22^310 == 0 /\ -__const_25172^post3+__const_25172^0 == 0 /\ -__const_4433^post3+__const_4433^0 == 0 /\ -__const_4433^0+constant22^13 == 0 /\ -lx2^post3+lx2^0 == 0 /\ __const_16069^0+constant22^1110 == 0 /\ -__const_3196^post3+__const_3196^0 == 0 /\ z317^post3-z519^post3-z317^210 == 0 /\ -tmp03^post3-tmp36^post3+tmp1011^post3 == 0 /\ -1-i20^0+i20^post3 == 0 /\ __const_20995^0-__const_20995^post3 == 0 /\ -tmp47^110+z115^210-tmp710^110 == 0 /\ constant22^510-__const_2446^0 == 0 /\ 1+i20^0-__const_8^0 <= 0 /\ -__const_9633^0+constant22^410 == 0 /\ -tmp47^110+z317^110-tmp69^110 == 0 /\ tmp25^post3-tmp14^post3+tmp1213^post3 == 0 /\ constant22^910+__const_7373^0 == 0 /\ tmp1112^post3-tmp25^post3-tmp14^post3 == 0 /\ -tmp58^110-tmp710^110+z418^110 == 0 /\ -tmp69^110-tmp58^110+z216^110 == 0 /\ __const_12299^0-__const_12299^post3 == 0 /\ __const_2446^0-__const_2446^post3 == 0 /\ __const_8^0-__const_8^post3 == 0 /\ constant22^210-__const_6270^0 == 0 /\ constant22^post3+__const_3196^0 == 0 /\ __const_15137^0-__const_15137^post3 == 0), cost: 1
New rule:
l3 -> l1 : tmp1011^0'=2*tmp36^post3+tmp1314^post3, z317^0'=z317^210-z418^210+z418^post3, tmp58^0'=tmp58^post3, i20^0'=1+i20^0, tmp25^0'=tmp14^post3-tmp1213^post3, tmp1213^0'=tmp1213^post3, z519^0'=-z418^210+z418^post3, tmp710^0'=tmp710^post3, tmp03^0'=tmp36^post3+tmp1314^post3, tmp47^0'=tmp47^post3, tmp14^0'=tmp14^post3, z216^0'=z216^post3, tmp1112^0'=2*tmp14^post3-tmp1213^post3, constant22^0'=-__const_3196^0, z418^0'=z418^post3, tmp69^0'=tmp69^post3, tmp36^0'=tmp36^post3, tmp1314^0'=tmp1314^post3, z115^0'=z115^post3, 1+i20^0-__const_8^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l0 : __const_20995^0'=__const_20995^post4, tmp1011^0'=tmp1011^post4, __const_9633^0'=__const_9633^post4, z317^0'=z317^post4, tmp58^0'=tmp58^post4, __const_15137^0'=__const_15137^post4, i20^0'=i20^post4, __const_6270^0'=__const_6270^post4, tmp25^0'=tmp25^post4, tmp1213^0'=tmp1213^post4, z519^0'=z519^post4, tmp710^0'=tmp710^post4, __const_25172^0'=__const_25172^post4, __const_16819^0'=__const_16819^post4, tmp03^0'=tmp03^post4, __const_8^0'=__const_8^post4, tmp47^0'=tmp47^post4, tmp14^0'=tmp14^post4, __const_12299^0'=__const_12299^post4, z216^0'=z216^post4, __const_4433^0'=__const_4433^post4, __const_2446^0'=__const_2446^post4, tmp1112^0'=tmp1112^post4, constant22^0'=constant22^post4, z418^0'=z418^post4, tmp69^0'=tmp69^post4, __const_16069^0'=__const_16069^post4, lx2^0'=lx2^post4, __const_7373^0'=__const_7373^post4, tmp36^0'=tmp36^post4, tmp1314^0'=tmp1314^post4, z115^0'=z115^post4, __const_3196^0'=__const_3196^post4, (-__const_4433^post4+__const_4433^0 == 0 /\ -tmp69^post4+tmp69^0 == 0 /\ lx2^0-lx2^post4 == 0 /\ z519^0-z519^post4 == 0 /\ tmp58^0-tmp58^post4 == 0 /\ -tmp1314^post4+tmp1314^0 == 0 /\ z317^0-z317^post4 == 0 /\ constant22^0-constant22^post4 == 0 /\ -z115^post4+z115^0 == 0 /\ -__const_12299^post4+__const_12299^0 == 0 /\ -__const_2446^post4+__const_2446^0 == 0 /\ -__const_6270^post4+__const_6270^0 == 0 /\ tmp1213^0-tmp1213^post4 == 0 /\ tmp1011^0-tmp1011^post4 == 0 /\ -__const_16069^post4+__const_16069^0 == 0 /\ i20^0-i20^post4 == 0 /\ tmp1112^0-tmp1112^post4 == 0 /\ -tmp710^post4+tmp710^0 == 0 /\ z418^0-z418^post4 == 0 /\ __const_9633^0-__const_9633^post4 == 0 /\ tmp25^0-tmp25^post4 == 0 /\ -tmp47^post4+tmp47^0 == 0 /\ __const_20995^0-__const_20995^post4 == 0 /\ tmp14^0-tmp14^post4 == 0 /\ tmp03^0-tmp03^post4 == 0 /\ -__const_16819^post4+__const_16819^0 == 0 /\ __const_15137^0-__const_15137^post4 == 0 /\ __const_25172^0-__const_25172^post4 == 0 /\ -__const_7373^post4+__const_7373^0 == 0 /\ -__const_3196^post4+__const_3196^0 == 0 /\ -z216^post4+z216^0 == 0 /\ __const_8^0-__const_8^post4 == 0 /\ -tmp36^post4+tmp36^0 == 0), cost: 1
New rule:
l2 -> l0 : TRUE, cost: 1

Applied preprocessing
Original rule:
l1 -> l3 : __const_20995^0'=__const_20995^post5, tmp1011^0'=tmp1011^post5, __const_9633^0'=__const_9633^post5, z317^0'=z317^post5, tmp58^0'=tmp58^post5, __const_15137^0'=__const_15137^post5, i20^0'=i20^post5, __const_6270^0'=__const_6270^post5, tmp25^0'=tmp25^post5, tmp1213^0'=tmp1213^post5, z519^0'=z519^post5, tmp710^0'=tmp710^post5, __const_25172^0'=__const_25172^post5, __const_16819^0'=__const_16819^post5, tmp03^0'=tmp03^post5, __const_8^0'=__const_8^post5, tmp47^0'=tmp47^post5, tmp14^0'=tmp14^post5, __const_12299^0'=__const_12299^post5, z216^0'=z216^post5, __const_4433^0'=__const_4433^post5, __const_2446^0'=__const_2446^post5, tmp1112^0'=tmp1112^post5, constant22^0'=constant22^post5, z418^0'=z418^post5, tmp69^0'=tmp69^post5, __const_16069^0'=__const_16069^post5, lx2^0'=lx2^post5, __const_7373^0'=__const_7373^post5, tmp36^0'=tmp36^post5, tmp1314^0'=tmp1314^post5, z115^0'=z115^post5, __const_3196^0'=__const_3196^post5, (-z115^post5+z115^0 == 0 /\ tmp710^0-tmp710^post5 == 0 /\ -tmp1314^post5+tmp1314^0 == 0 /\ tmp03^0-tmp03^post5 == 0 /\ -lx2^post5+lx2^0 == 0 /\ tmp25^0-tmp25^post5 == 0 /\ -z519^post5+z519^0 == 0 /\ -__const_25172^post5+__const_25172^0 == 0 /\ -__const_16069^post5+__const_16069^0 == 0 /\ -__const_16819^post5+__const_16819^0 == 0 /\ __const_9633^0-__const_9633^post5 == 0 /\ constant22^0-constant22^post5 == 0 /\ __const_12299^0-__const_12299^post5 == 0 /\ -__const_3196^post5+__const_3196^0 == 0 /\ __const_8^0-__const_8^post5 == 0 /\ z216^0-z216^post5 == 0 /\ __const_6270^0-__const_6270^post5 == 0 /\ -__const_4433^post5+__const_4433^0 == 0 /\ tmp58^0-tmp58^post5 == 0 /\ -tmp69^post5+tmp69^0 == 0 /\ -z418^post5+z418^0 == 0 /\ __const_15137^0-__const_15137^post5 == 0 /\ -tmp36^post5+tmp36^0 == 0 /\ i20^0-i20^post5 == 0 /\ -__const_2446^post5+__const_2446^0 == 0 /\ -tmp1213^post5+tmp1213^0 == 0 /\ __const_20995^0-__const_20995^post5 == 0 /\ tmp1112^0-tmp1112^post5 == 0 /\ z317^0-z317^post5 == 0 /\ tmp1011^0-tmp1011^post5 == 0 /\ -tmp47^post5+tmp47^0 == 0 /\ tmp14^0-tmp14^post5 == 0 /\ -__const_7373^post5+__const_7373^0 == 0), cost: 1
New rule:
l1 -> l3 : TRUE, cost: 1

Applied preprocessing
Original rule:
l5 -> l2 : __const_20995^0'=__const_20995^post6, tmp1011^0'=tmp1011^post6, __const_9633^0'=__const_9633^post6, z317^0'=z317^post6, tmp58^0'=tmp58^post6, __const_15137^0'=__const_15137^post6, i20^0'=i20^post6, __const_6270^0'=__const_6270^post6, tmp25^0'=tmp25^post6, tmp1213^0'=tmp1213^post6, z519^0'=z519^post6, tmp710^0'=tmp710^post6, __const_25172^0'=__const_25172^post6, __const_16819^0'=__const_16819^post6, tmp03^0'=tmp03^post6, __const_8^0'=__const_8^post6, tmp47^0'=tmp47^post6, tmp14^0'=tmp14^post6, __const_12299^0'=__const_12299^post6, z216^0'=z216^post6, __const_4433^0'=__const_4433^post6, __const_2446^0'=__const_2446^post6, tmp1112^0'=tmp1112^post6, constant22^0'=constant22^post6, z418^0'=z418^post6, tmp69^0'=tmp69^post6, __const_16069^0'=__const_16069^post6, lx2^0'=lx2^post6, __const_7373^0'=__const_7373^post6, tmp36^0'=tmp36^post6, tmp1314^0'=tmp1314^post6, z115^0'=z115^post6, __const_3196^0'=__const_3196^post6, (-__const_25172^post6+__const_25172^0 == 0 /\ __const_6270^0-__const_6270^post6 == 0 /\ __const_16819^0-__const_16819^post6 == 0 /\ -tmp1112^post6+tmp1112^0 == 0 /\ tmp14^0-tmp14^post6 == 0 /\ tmp1213^0-tmp1213^post6 == 0 /\ __const_12299^0-__const_12299^post6 == 0 /\ -__const_7373^post6+__const_7373^0 == 0 /\ -tmp47^post6+tmp47^0 == 0 /\ z216^0-z216^post6 == 0 /\ -z115^post6+z115^0 == 0 /\ -z519^post6+z519^0 == 0 /\ z317^0-z317^post6 == 0 /\ tmp58^0-tmp58^post6 == 0 /\ __const_16069^0-__const_16069^post6 == 0 /\ -z418^post6+z418^0 == 0 /\ __const_2446^0-__const_2446^post6 == 0 /\ -tmp25^post6+tmp25^0 == 0 /\ lx2^post6-__const_8^0 == 0 /\ __const_15137^0-__const_15137^post6 == 0 /\ -tmp69^post6+tmp69^0 == 0 /\ __const_20995^0-__const_20995^post6 == 0 /\ -__const_8^post6+__const_8^0 == 0 /\ tmp710^0-tmp710^post6 == 0 /\ tmp1011^0-tmp1011^post6 == 0 /\ -__const_3196^post6+__const_3196^0 == 0 /\ -constant22^post6+constant22^0 == 0 /\ tmp36^0-tmp36^post6 == 0 /\ -tmp1314^post6+tmp1314^0 == 0 /\ -__const_9633^post6+__const_9633^0 == 0 /\ -__const_4433^post6+__const_4433^0 == 0 /\ tmp03^0-tmp03^post6 == 0 /\ i20^post6 == 0), cost: 1
New rule:
l5 -> l2 : i20^0'=0, lx2^0'=__const_8^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l6 -> l5 : __const_20995^0'=__const_20995^post7, tmp1011^0'=tmp1011^post7, __const_9633^0'=__const_9633^post7, z317^0'=z317^post7, tmp58^0'=tmp58^post7, __const_15137^0'=__const_15137^post7, i20^0'=i20^post7, __const_6270^0'=__const_6270^post7, tmp25^0'=tmp25^post7, tmp1213^0'=tmp1213^post7, z519^0'=z519^post7, tmp710^0'=tmp710^post7, __const_25172^0'=__const_25172^post7, __const_16819^0'=__const_16819^post7, tmp03^0'=tmp03^post7, __const_8^0'=__const_8^post7, tmp47^0'=tmp47^post7, tmp14^0'=tmp14^post7, __const_12299^0'=__const_12299^post7, z216^0'=z216^post7, __const_4433^0'=__const_4433^post7, __const_2446^0'=__const_2446^post7, tmp1112^0'=tmp1112^post7, constant22^0'=constant22^post7, z418^0'=z418^post7, tmp69^0'=tmp69^post7, __const_16069^0'=__const_16069^post7, lx2^0'=lx2^post7, __const_7373^0'=__const_7373^post7, tmp36^0'=tmp36^post7, tmp1314^0'=tmp1314^post7, z115^0'=z115^post7, __const_3196^0'=__const_3196^post7, (-z418^post7+z418^0 == 0 /\ -i20^post7+i20^0 == 0 /\ tmp1011^0-tmp1011^post7 == 0 /\ tmp710^0-tmp710^post7 == 0 /\ __const_12299^0-__const_12299^post7 == 0 /\ -tmp36^post7+tmp36^0 == 0 /\ __const_9633^0-__const_9633^post7 == 0 /\ -tmp03^post7+tmp03^0 == 0 /\ -__const_7373^post7+__const_7373^0 == 0 /\ -__const_3196^post7+__const_3196^0 == 0 /\ -z216^post7+z216^0 == 0 /\ -tmp1314^post7+tmp1314^0 == 0 /\ __const_4433^0-__const_4433^post7 == 0 /\ __const_15137^0-__const_15137^post7 == 0 /\ -lx2^post7+lx2^0 == 0 /\ -tmp25^post7+tmp25^0 == 0 /\ -tmp69^post7+tmp69^0 == 0 /\ -constant22^post7+constant22^0 == 0 /\ __const_16819^0-__const_16819^post7 == 0 /\ __const_2446^0-__const_2446^post7 == 0 /\ -__const_8^post7+__const_8^0 == 0 /\ __const_6270^0-__const_6270^post7 == 0 /\ tmp1213^0-tmp1213^post7 == 0 /\ __const_20995^0-__const_20995^post7 == 0 /\ __const_25172^0-__const_25172^post7 == 0 /\ -z115^post7+z115^0 == 0 /\ tmp58^0-tmp58^post7 == 0 /\ tmp47^0-tmp47^post7 == 0 /\ z519^0-z519^post7 == 0 /\ -tmp14^post7+tmp14^0 == 0 /\ -__const_16069^post7+__const_16069^0 == 0 /\ -z317^post7+z317^0 == 0 /\ -tmp1112^post7+tmp1112^0 == 0), cost: 1
New rule:
l6 -> l5 : TRUE, cost: 1

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


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

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

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

Applied deletion
Removed the following rules: 16

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


Applied chaining
First rule:
l0 -> l1 : i20^0'=0, -i20^0+__const_8^0 <= 0, cost: 1
Second rule:
l1 -> l1 : tmp1011^0'=2*tmp36^post3+tmp1314^post3, z317^0'=z317^210-z418^210+z418^post3, tmp58^0'=tmp58^post3, i20^0'=__const_8^0, tmp25^0'=tmp14^post3-tmp1213^post3, tmp1213^0'=tmp1213^post3, z519^0'=-z418^210+z418^post3, tmp710^0'=tmp710^post3, tmp03^0'=tmp36^post3+tmp1314^post3, tmp47^0'=tmp47^post3, tmp14^0'=tmp14^post3, z216^0'=z216^post3, tmp1112^0'=2*tmp14^post3-tmp1213^post3, constant22^0'=-__const_3196^0, z418^0'=z418^post3, tmp69^0'=tmp69^post3, tmp36^0'=tmp36^post3, tmp1314^0'=tmp1314^post3, z115^0'=z115^post3, -1-i20^0+__const_8^0 >= 0, cost: -2*i20^0+2*__const_8^0
New rule:
l0 -> l1 : tmp1011^0'=2*tmp36^post3+tmp1314^post3, z317^0'=z317^210-z418^210+z418^post3, tmp58^0'=tmp58^post3, i20^0'=__const_8^0, tmp25^0'=tmp14^post3-tmp1213^post3, tmp1213^0'=tmp1213^post3, z519^0'=-z418^210+z418^post3, tmp710^0'=tmp710^post3, tmp03^0'=tmp36^post3+tmp1314^post3, tmp47^0'=tmp47^post3, tmp14^0'=tmp14^post3, z216^0'=z216^post3, tmp1112^0'=2*tmp14^post3-tmp1213^post3, constant22^0'=-__const_3196^0, z418^0'=z418^post3, tmp69^0'=tmp69^post3, tmp36^0'=tmp36^post3, tmp1314^0'=tmp1314^post3, z115^0'=z115^post3, (-1+__const_8^0 >= 0 /\ -i20^0+__const_8^0 <= 0), cost: 1+2*__const_8^0

Applied deletion
Removed the following rules: 18

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


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


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

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

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

Applied deletion
Removed the following rules: 20

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


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

Applied deletion
Removed the following rules: 22

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


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