WORST_CASE(Omega(0),?)

Initial ITS
Start location: l13
   0: l0 -> l1 : c12^0'=c12^post0, z^0'=z^post0, tmp^0'=tmp^post0, a15^0'=a15^post0, tmp___1^0'=tmp___1^post0, tmp620^0'=tmp620^post0, m13^0'=m13^post0, b16^0'=b16^post0, y_promoted_2^0'=y_promoted_2^post0, tmp9^0'=tmp9^post0, a10^0'=a10^post0, ret_min14^0'=ret_min14^post0, c17^0'=c17^post0, tmp___0^0'=tmp___0^post0, b11^0'=b11^post0, x_promoted_1^0'=x_promoted_1^post0, tmp923^0'=tmp923^post0, ret_max24^0'=ret_max24^post0, (-a15^post0+a15^0 == 0 /\ z^0-z^post0 == 0 /\ y_promoted_2^0-y_promoted_2^post0 == 0 /\ -tmp___0^post0+tmp___0^0 == 0 /\ ret_min14^0-ret_min14^post0 == 0 /\ -tmp9^post0+tmp9^0 == 0 /\ tmp^0-tmp^post0 == 0 /\ -ret_max24^post0+ret_max24^0 == 0 /\ -m13^post0+m13^0 == 0 /\ -b11^post0+b11^0 == 0 /\ x_promoted_1^0-x_promoted_1^post0 == 0 /\ -c17^post0+c17^0 == 0 /\ -b16^post0+b16^0 == 0 /\ -a10^post0+a10^0 == 0 /\ tmp___1^0-tmp___1^post0 == 0 /\ -tmp923^post0+tmp923^0 == 0 /\ c12^0-c12^post0 == 0 /\ tmp620^0-tmp620^post0 == 0), cost: 1
   1: l2 -> l3 : c12^0'=c12^post1, z^0'=z^post1, tmp^0'=tmp^post1, a15^0'=a15^post1, tmp___1^0'=tmp___1^post1, tmp620^0'=tmp620^post1, m13^0'=m13^post1, b16^0'=b16^post1, y_promoted_2^0'=y_promoted_2^post1, tmp9^0'=tmp9^post1, a10^0'=a10^post1, ret_min14^0'=ret_min14^post1, c17^0'=c17^post1, tmp___0^0'=tmp___0^post1, b11^0'=b11^post1, x_promoted_1^0'=x_promoted_1^post1, tmp923^0'=tmp923^post1, ret_max24^0'=ret_max24^post1, (0 == 0 /\ a15^0-a15^post1 == 0 /\ -tmp923^post1+tmp923^0 == 0 /\ m13^0-m13^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ -x_promoted_1^post1+x_promoted_1^0 == 0 /\ a10^0-a10^post1 == 0 /\ c12^0-c12^post1 == 0 /\ tmp___0^post1-ret_max24^post1 == 0 /\ -b11^post1+b11^0 == 0 /\ -tmp620^post1+tmp620^0 == 0 /\ -ret_min14^post1+ret_min14^0 == 0 /\ c17^0-c17^post1 == 0 /\ tmp___1^0-tmp___1^post1 == 0 /\ b16^0-b16^post1 == 0 /\ -y_promoted_2^post1+y_promoted_2^0 == 0 /\ -tmp9^post1+tmp9^0 == 0 /\ -a15^0+ret_max24^post1 == 0), cost: 1
  17: l3 -> l0 : c12^0'=c12^post17, z^0'=z^post17, tmp^0'=tmp^post17, a15^0'=a15^post17, tmp___1^0'=tmp___1^post17, tmp620^0'=tmp620^post17, m13^0'=m13^post17, b16^0'=b16^post17, y_promoted_2^0'=y_promoted_2^post17, tmp9^0'=tmp9^post17, a10^0'=a10^post17, ret_min14^0'=ret_min14^post17, c17^0'=c17^post17, tmp___0^0'=tmp___0^post17, b11^0'=b11^post17, x_promoted_1^0'=x_promoted_1^post17, tmp923^0'=tmp923^post17, ret_max24^0'=ret_max24^post17, (z^0-z^post17 == 0 /\ -y_promoted_2^post17+y_promoted_2^0 == 0 /\ -ret_max24^post17+ret_max24^0 == 0 /\ tmp^0-tmp^post17 == 0 /\ 1+z^0-y_promoted_2^0 <= 0 /\ -tmp9^post17+tmp9^0 == 0 /\ b16^0-b16^post17 == 0 /\ b11^0-b11^post17 == 0 /\ -tmp923^post17+tmp923^0 == 0 /\ tmp___0^0-tmp___0^post17 == 0 /\ -x_promoted_1^post17+x_promoted_1^0 == 0 /\ -tmp620^post17+tmp620^0 == 0 /\ z^0-y_promoted_2^0+tmp___1^post17 == 0 /\ a15^0-a15^post17 == 0 /\ m13^0-m13^post17 == 0 /\ -c17^post17+c17^0 == 0 /\ -ret_min14^post17+ret_min14^0 == 0 /\ a10^0-a10^post17 == 0 /\ c12^0-c12^post17 == 0), cost: 1
  18: l3 -> l0 : c12^0'=c12^post18, z^0'=z^post18, tmp^0'=tmp^post18, a15^0'=a15^post18, tmp___1^0'=tmp___1^post18, tmp620^0'=tmp620^post18, m13^0'=m13^post18, b16^0'=b16^post18, y_promoted_2^0'=y_promoted_2^post18, tmp9^0'=tmp9^post18, a10^0'=a10^post18, ret_min14^0'=ret_min14^post18, c17^0'=c17^post18, tmp___0^0'=tmp___0^post18, b11^0'=b11^post18, x_promoted_1^0'=x_promoted_1^post18, tmp923^0'=tmp923^post18, ret_max24^0'=ret_max24^post18, (tmp^0-tmp^post18 == 0 /\ -b11^post18+b11^0 == 0 /\ ret_min14^0-ret_min14^post18 == 0 /\ c12^0-c12^post18 == 0 /\ -tmp9^post18+tmp9^0 == 0 /\ y_promoted_2^0-y_promoted_2^post18 == 0 /\ -a15^post18+a15^0 == 0 /\ -tmp923^post18+tmp923^0 == 0 /\ -tmp___0^post18+tmp___0^0 == 0 /\ -z^0+y_promoted_2^0 <= 0 /\ -m13^post18+m13^0 == 0 /\ -x_promoted_1^post18+x_promoted_1^0 == 0 /\ -c17^post18+c17^0 == 0 /\ -b16^post18+b16^0 == 0 /\ -a10^post18+a10^0 == 0 /\ -z^0-y_promoted_2^0+tmp___1^post18 == 0 /\ -ret_max24^post18+ret_max24^0 == 0 /\ z^0-z^post18 == 0 /\ tmp620^0-tmp620^post18 == 0), cost: 1
   2: l4 -> l5 : c12^0'=c12^post2, z^0'=z^post2, tmp^0'=tmp^post2, a15^0'=a15^post2, tmp___1^0'=tmp___1^post2, tmp620^0'=tmp620^post2, m13^0'=m13^post2, b16^0'=b16^post2, y_promoted_2^0'=y_promoted_2^post2, tmp9^0'=tmp9^post2, a10^0'=a10^post2, ret_min14^0'=ret_min14^post2, c17^0'=c17^post2, tmp___0^0'=tmp___0^post2, b11^0'=b11^post2, x_promoted_1^0'=x_promoted_1^post2, tmp923^0'=tmp923^post2, ret_max24^0'=ret_max24^post2, (-a10^post2+a10^0 == 0 /\ b16^0-b16^post2 == 0 /\ -tmp923^post2+tmp923^0 == 0 /\ -ret_max24^post2+ret_max24^0 == 0 /\ c12^0-c12^post2 == 0 /\ tmp___1^0-tmp___1^post2 == 0 /\ -x_promoted_1^post2+x_promoted_1^0 == 0 /\ z^0-z^post2 == 0 /\ tmp620^0-tmp620^post2 == 0 /\ -tmp9^post2+tmp9^0 == 0 /\ a15^0-a15^post2 == 0 /\ -ret_min14^post2+ret_min14^0 == 0 /\ -tmp^post2+tmp^0 == 0 /\ -m13^post2+m13^0 == 0 /\ tmp___0^0-tmp___0^post2 == 0 /\ y_promoted_2^0-y_promoted_2^post2 == 0 /\ -b11^post2+b11^0 == 0 /\ 1+y_promoted_2^0-x_promoted_1^0 <= 0 /\ -c17^post2+c17^0 == 0), cost: 1
   3: l4 -> l3 : c12^0'=c12^post3, z^0'=z^post3, tmp^0'=tmp^post3, a15^0'=a15^post3, tmp___1^0'=tmp___1^post3, tmp620^0'=tmp620^post3, m13^0'=m13^post3, b16^0'=b16^post3, y_promoted_2^0'=y_promoted_2^post3, tmp9^0'=tmp9^post3, a10^0'=a10^post3, ret_min14^0'=ret_min14^post3, c17^0'=c17^post3, tmp___0^0'=tmp___0^post3, b11^0'=b11^post3, x_promoted_1^0'=x_promoted_1^post3, tmp923^0'=tmp923^post3, ret_max24^0'=ret_max24^post3, (0 == 0 /\ c12^0-c12^post3 == 0 /\ a15^0-a15^post3 == 0 /\ tmp620^0-tmp620^post3 == 0 /\ tmp^0-tmp^post3 == 0 /\ m13^0-m13^post3 == 0 /\ a10^0-a10^post3 == 0 /\ -ret_min14^post3+ret_min14^0 == 0 /\ -tmp923^post3+tmp923^0 == 0 /\ tmp___1^0-tmp___1^post3 == 0 /\ -y_promoted_2^post3+y_promoted_2^0 == 0 /\ b16^0-b16^post3 == 0 /\ -y_promoted_2^0+x_promoted_1^0 <= 0 /\ -x_promoted_1^post3+x_promoted_1^0 == 0 /\ c17^0-c17^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ -b11^post3+b11^0 == 0 /\ -z^post3+z^0 == 0 /\ -ret_max24^post3+ret_max24^0 == 0), cost: 1
  15: l5 -> l7 : c12^0'=c12^post15, z^0'=z^post15, tmp^0'=tmp^post15, a15^0'=a15^post15, tmp___1^0'=tmp___1^post15, tmp620^0'=tmp620^post15, m13^0'=m13^post15, b16^0'=b16^post15, y_promoted_2^0'=y_promoted_2^post15, tmp9^0'=tmp9^post15, a10^0'=a10^post15, ret_min14^0'=ret_min14^post15, c17^0'=c17^post15, tmp___0^0'=tmp___0^post15, b11^0'=b11^post15, x_promoted_1^0'=x_promoted_1^post15, tmp923^0'=tmp923^post15, ret_max24^0'=ret_max24^post15, (c12^0-c12^post15 == 0 /\ z^0-z^post15 == 0 /\ -y_promoted_2^post15+y_promoted_2^0 == 0 /\ -y_promoted_2^0+b16^post15 == 0 /\ -tmp9^post15+tmp9^0 == 0 /\ tmp^0-tmp^post15 == 0 /\ c17^post15-x_promoted_1^0 == 0 /\ b11^0-b11^post15 == 0 /\ 1+z^0-x_promoted_1^0 <= 0 /\ -tmp923^post15+tmp923^0 == 0 /\ tmp___1^0-tmp___1^post15 == 0 /\ -ret_max24^post15+ret_max24^0 == 0 /\ -z^0+a15^post15 == 0 /\ tmp___0^0-tmp___0^post15 == 0 /\ m13^0-m13^post15 == 0 /\ -tmp620^post15+tmp620^0 == 0 /\ -x_promoted_1^post15+x_promoted_1^0 == 0 /\ a10^0-a10^post15 == 0 /\ -ret_min14^post15+ret_min14^0 == 0), cost: 1
  16: l5 -> l11 : c12^0'=c12^post16, z^0'=z^post16, tmp^0'=tmp^post16, a15^0'=a15^post16, tmp___1^0'=tmp___1^post16, tmp620^0'=tmp620^post16, m13^0'=m13^post16, b16^0'=b16^post16, y_promoted_2^0'=y_promoted_2^post16, tmp9^0'=tmp9^post16, a10^0'=a10^post16, ret_min14^0'=ret_min14^post16, c17^0'=c17^post16, tmp___0^0'=tmp___0^post16, b11^0'=b11^post16, x_promoted_1^0'=x_promoted_1^post16, tmp923^0'=tmp923^post16, ret_max24^0'=ret_max24^post16, (-a15^post16+a15^0 == 0 /\ -y_promoted_2^0+b11^post16 == 0 /\ z^0-z^post16 == 0 /\ y_promoted_2^0-y_promoted_2^post16 == 0 /\ ret_min14^0-ret_min14^post16 == 0 /\ -z^0+x_promoted_1^0 <= 0 /\ -tmp9^post16+tmp9^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ -ret_max24^post16+ret_max24^0 == 0 /\ -m13^post16+m13^0 == 0 /\ x_promoted_1^0-x_promoted_1^post16 == 0 /\ a10^post16-x_promoted_1^0 == 0 /\ -c17^post16+c17^0 == 0 /\ -b16^post16+b16^0 == 0 /\ tmp___1^0-tmp___1^post16 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ -tmp923^post16+tmp923^0 == 0 /\ tmp620^0-tmp620^post16 == 0 /\ -z^0+c12^post16 == 0), cost: 1
   4: l6 -> l2 : c12^0'=c12^post4, z^0'=z^post4, tmp^0'=tmp^post4, a15^0'=a15^post4, tmp___1^0'=tmp___1^post4, tmp620^0'=tmp620^post4, m13^0'=m13^post4, b16^0'=b16^post4, y_promoted_2^0'=y_promoted_2^post4, tmp9^0'=tmp9^post4, a10^0'=a10^post4, ret_min14^0'=ret_min14^post4, c17^0'=c17^post4, tmp___0^0'=tmp___0^post4, b11^0'=b11^post4, x_promoted_1^0'=x_promoted_1^post4, tmp923^0'=tmp923^post4, ret_max24^0'=ret_max24^post4, (-b11^post4+b11^0 == 0 /\ -a10^post4+a10^0 == 0 /\ -tmp___0^post4+tmp___0^0 == 0 /\ x_promoted_1^0-x_promoted_1^post4 == 0 /\ ret_min14^0-ret_min14^post4 == 0 /\ 1-a15^0+c17^0 <= 0 /\ b16^0-b16^post4 == 0 /\ -ret_max24^post4+ret_max24^0 == 0 /\ c12^0-c12^post4 == 0 /\ tmp___1^0-tmp___1^post4 == 0 /\ -c17^post4+c17^0 == 0 /\ z^0-z^post4 == 0 /\ a15^0-a15^post4 == 0 /\ -tmp9^post4+tmp9^0 == 0 /\ -tmp923^post4+tmp923^0 == 0 /\ tmp620^0-tmp620^post4 == 0 /\ -tmp^post4+tmp^0 == 0 /\ -m13^post4+m13^0 == 0 /\ y_promoted_2^0-y_promoted_2^post4 == 0), cost: 1
   5: l6 -> l2 : c12^0'=c12^post5, z^0'=z^post5, tmp^0'=tmp^post5, a15^0'=a15^post5, tmp___1^0'=tmp___1^post5, tmp620^0'=tmp620^post5, m13^0'=m13^post5, b16^0'=b16^post5, y_promoted_2^0'=y_promoted_2^post5, tmp9^0'=tmp9^post5, a10^0'=a10^post5, ret_min14^0'=ret_min14^post5, c17^0'=c17^post5, tmp___0^0'=tmp___0^post5, b11^0'=b11^post5, x_promoted_1^0'=x_promoted_1^post5, tmp923^0'=tmp923^post5, ret_max24^0'=ret_max24^post5, (0 == 0 /\ tmp9^0-tmp9^post5 == 0 /\ -y_promoted_2^post5+y_promoted_2^0 == 0 /\ -x_promoted_1^post5+x_promoted_1^0 == 0 /\ c12^0-c12^post5 == 0 /\ a15^0-a15^post5 == 0 /\ -b11^post5+b11^0 == 0 /\ m13^0-m13^post5 == 0 /\ -ret_max24^post5+ret_max24^0 == 0 /\ a15^0-c17^0 <= 0 /\ z^0-z^post5 == 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ ret_min14^0-ret_min14^post5 == 0 /\ -a10^post5+a10^0 == 0 /\ tmp620^0-tmp620^post5 == 0 /\ b16^0-b16^post5 == 0 /\ tmp^0-tmp^post5 == 0 /\ c17^0-c17^post5 == 0 /\ -tmp___0^post5+tmp___0^0 == 0), cost: 1
   6: l7 -> l6 : c12^0'=c12^post6, z^0'=z^post6, tmp^0'=tmp^post6, a15^0'=a15^post6, tmp___1^0'=tmp___1^post6, tmp620^0'=tmp620^post6, m13^0'=m13^post6, b16^0'=b16^post6, y_promoted_2^0'=y_promoted_2^post6, tmp9^0'=tmp9^post6, a10^0'=a10^post6, ret_min14^0'=ret_min14^post6, c17^0'=c17^post6, tmp___0^0'=tmp___0^post6, b11^0'=b11^post6, x_promoted_1^0'=x_promoted_1^post6, tmp923^0'=tmp923^post6, ret_max24^0'=ret_max24^post6, (-c17^post6+c17^0 == 0 /\ tmp___1^0-tmp___1^post6 == 0 /\ b16^0-b16^post6 == 0 /\ -tmp923^post6+tmp923^0 == 0 /\ -a10^post6+a10^0 == 0 /\ z^0-z^post6 == 0 /\ -m13^post6+m13^0 == 0 /\ -x_promoted_1^post6+x_promoted_1^0 == 0 /\ tmp^0-tmp^post6 == 0 /\ -b11^post6+b11^0 == 0 /\ -tmp9^post6+tmp9^0 == 0 /\ -tmp620^post6+tmp620^0 == 0 /\ c12^0-c12^post6 == 0 /\ -ret_min14^post6+ret_min14^0 == 0 /\ 1-a15^0+b16^0 <= 0 /\ -ret_max24^post6+ret_max24^0 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ a15^0-a15^post6 == 0 /\ y_promoted_2^0-y_promoted_2^post6 == 0), cost: 1
   7: l7 -> l6 : c12^0'=c12^post7, z^0'=z^post7, tmp^0'=tmp^post7, a15^0'=a15^post7, tmp___1^0'=tmp___1^post7, tmp620^0'=tmp620^post7, m13^0'=m13^post7, b16^0'=b16^post7, y_promoted_2^0'=y_promoted_2^post7, tmp9^0'=tmp9^post7, a10^0'=a10^post7, ret_min14^0'=ret_min14^post7, c17^0'=c17^post7, tmp___0^0'=tmp___0^post7, b11^0'=b11^post7, x_promoted_1^0'=x_promoted_1^post7, tmp923^0'=tmp923^post7, ret_max24^0'=ret_max24^post7, (0 == 0 /\ -tmp___1^post7+tmp___1^0 == 0 /\ y_promoted_2^0-y_promoted_2^post7 == 0 /\ z^0-z^post7 == 0 /\ -a10^post7+a10^0 == 0 /\ ret_min14^0-ret_min14^post7 == 0 /\ -tmp923^post7+tmp923^0 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ c12^0-c12^post7 == 0 /\ a15^0-a15^post7 == 0 /\ tmp^0-tmp^post7 == 0 /\ -x_promoted_1^post7+x_promoted_1^0 == 0 /\ -c17^post7+c17^0 == 0 /\ tmp9^0-tmp9^post7 == 0 /\ m13^0-m13^post7 == 0 /\ -b11^post7+b11^0 == 0 /\ a15^0-b16^0 <= 0 /\ -b16^post7+b16^0 == 0 /\ -ret_max24^post7+ret_max24^0 == 0), cost: 1
   8: l8 -> l9 : c12^0'=c12^post8, z^0'=z^post8, tmp^0'=tmp^post8, a15^0'=a15^post8, tmp___1^0'=tmp___1^post8, tmp620^0'=tmp620^post8, m13^0'=m13^post8, b16^0'=b16^post8, y_promoted_2^0'=y_promoted_2^post8, tmp9^0'=tmp9^post8, a10^0'=a10^post8, ret_min14^0'=ret_min14^post8, c17^0'=c17^post8, tmp___0^0'=tmp___0^post8, b11^0'=b11^post8, x_promoted_1^0'=x_promoted_1^post8, tmp923^0'=tmp923^post8, ret_max24^0'=ret_max24^post8, (b11^0-b11^post8 == 0 /\ -tmp9^post8+tmp9^0 == 0 /\ z^0-z^post8 == 0 /\ tmp___1^0-tmp___1^post8 == 0 /\ -ret_min14^post8+ret_min14^0 == 0 /\ 1+c12^0-b11^0 <= 0 /\ tmp^0-tmp^post8 == 0 /\ -ret_max24^post8+ret_max24^0 == 0 /\ -c12^0+m13^post8 == 0 /\ b16^0-b16^post8 == 0 /\ -tmp620^post8+tmp620^0 == 0 /\ tmp___0^0-tmp___0^post8 == 0 /\ a10^0-a10^post8 == 0 /\ -c17^post8+c17^0 == 0 /\ -tmp923^post8+tmp923^0 == 0 /\ y_promoted_2^0-y_promoted_2^post8 == 0 /\ c12^0-c12^post8 == 0 /\ a15^0-a15^post8 == 0 /\ -x_promoted_1^post8+x_promoted_1^0 == 0), cost: 1
   9: l8 -> l9 : c12^0'=c12^post9, z^0'=z^post9, tmp^0'=tmp^post9, a15^0'=a15^post9, tmp___1^0'=tmp___1^post9, tmp620^0'=tmp620^post9, m13^0'=m13^post9, b16^0'=b16^post9, y_promoted_2^0'=y_promoted_2^post9, tmp9^0'=tmp9^post9, a10^0'=a10^post9, ret_min14^0'=ret_min14^post9, c17^0'=c17^post9, tmp___0^0'=tmp___0^post9, b11^0'=b11^post9, x_promoted_1^0'=x_promoted_1^post9, tmp923^0'=tmp923^post9, ret_max24^0'=ret_max24^post9, (y_promoted_2^0-y_promoted_2^post9 == 0 /\ tmp620^0-tmp620^post9 == 0 /\ -x_promoted_1^post9+x_promoted_1^0 == 0 /\ ret_min14^0-ret_min14^post9 == 0 /\ m13^post9-b11^0 == 0 /\ z^0-z^post9 == 0 /\ c12^0-c12^post9 == 0 /\ -c17^post9+c17^0 == 0 /\ -b11^post9+b11^0 == 0 /\ tmp^0-tmp^post9 == 0 /\ -c12^0+b11^0 <= 0 /\ -b16^post9+b16^0 == 0 /\ -ret_max24^post9+ret_max24^0 == 0 /\ tmp9^0-tmp9^post9 == 0 /\ tmp___1^0-tmp___1^post9 == 0 /\ -a10^post9+a10^0 == 0 /\ -a15^post9+a15^0 == 0 /\ -tmp923^post9+tmp923^0 == 0 /\ -tmp___0^post9+tmp___0^0 == 0), cost: 1
  10: l9 -> l3 : c12^0'=c12^post10, z^0'=z^post10, tmp^0'=tmp^post10, a15^0'=a15^post10, tmp___1^0'=tmp___1^post10, tmp620^0'=tmp620^post10, m13^0'=m13^post10, b16^0'=b16^post10, y_promoted_2^0'=y_promoted_2^post10, tmp9^0'=tmp9^post10, a10^0'=a10^post10, ret_min14^0'=ret_min14^post10, c17^0'=c17^post10, tmp___0^0'=tmp___0^post10, b11^0'=b11^post10, x_promoted_1^0'=x_promoted_1^post10, tmp923^0'=tmp923^post10, ret_max24^0'=ret_max24^post10, (a10^0-a10^post10 == 0 /\ c12^0-c12^post10 == 0 /\ -b11^post10+b11^0 == 0 /\ -tmp___0^post10+tmp___0^0 == 0 /\ m13^0-m13^post10 == 0 /\ -tmp923^post10+tmp923^0 == 0 /\ a15^0-a15^post10 == 0 /\ tmp9^0-tmp9^post10 == 0 /\ -tmp^post10+x_promoted_1^post10-x_promoted_1^0 == 0 /\ c17^0-c17^post10 == 0 /\ -m13^0+ret_min14^post10 == 0 /\ tmp___1^0-tmp___1^post10 == 0 /\ -ret_max24^post10+ret_max24^0 == 0 /\ -z^post10+z^0 == 0 /\ tmp^post10-ret_min14^post10 == 0 /\ b16^0-b16^post10 == 0 /\ -y_promoted_2^post10+y_promoted_2^0 == 0 /\ tmp620^0-tmp620^post10 == 0), cost: 1
  11: l10 -> l9 : c12^0'=c12^post11, z^0'=z^post11, tmp^0'=tmp^post11, a15^0'=a15^post11, tmp___1^0'=tmp___1^post11, tmp620^0'=tmp620^post11, m13^0'=m13^post11, b16^0'=b16^post11, y_promoted_2^0'=y_promoted_2^post11, tmp9^0'=tmp9^post11, a10^0'=a10^post11, ret_min14^0'=ret_min14^post11, c17^0'=c17^post11, tmp___0^0'=tmp___0^post11, b11^0'=b11^post11, x_promoted_1^0'=x_promoted_1^post11, tmp923^0'=tmp923^post11, ret_max24^0'=ret_max24^post11, (b16^0-b16^post11 == 0 /\ tmp___1^0-tmp___1^post11 == 0 /\ x_promoted_1^0-x_promoted_1^post11 == 0 /\ -c12^0+m13^post11 == 0 /\ tmp620^0-tmp620^post11 == 0 /\ -ret_min14^post11+ret_min14^0 == 0 /\ y_promoted_2^0-y_promoted_2^post11 == 0 /\ -tmp923^post11+tmp923^0 == 0 /\ -ret_max24^post11+ret_max24^0 == 0 /\ a15^0-a15^post11 == 0 /\ 1+c12^0-a10^0 <= 0 /\ c12^0-c12^post11 == 0 /\ z^0-z^post11 == 0 /\ -c17^post11+c17^0 == 0 /\ -b11^post11+b11^0 == 0 /\ -a10^post11+a10^0 == 0 /\ tmp^0-tmp^post11 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ -tmp9^post11+tmp9^0 == 0), cost: 1
  12: l10 -> l9 : c12^0'=c12^post12, z^0'=z^post12, tmp^0'=tmp^post12, a15^0'=a15^post12, tmp___1^0'=tmp___1^post12, tmp620^0'=tmp620^post12, m13^0'=m13^post12, b16^0'=b16^post12, y_promoted_2^0'=y_promoted_2^post12, tmp9^0'=tmp9^post12, a10^0'=a10^post12, ret_min14^0'=ret_min14^post12, c17^0'=c17^post12, tmp___0^0'=tmp___0^post12, b11^0'=b11^post12, x_promoted_1^0'=x_promoted_1^post12, tmp923^0'=tmp923^post12, ret_max24^0'=ret_max24^post12, (-b16^post12+b16^0 == 0 /\ -x_promoted_1^post12+x_promoted_1^0 == 0 /\ -tmp___0^post12+tmp___0^0 == 0 /\ tmp9^0-tmp9^post12 == 0 /\ tmp923^0-tmp923^post12 == 0 /\ -ret_max24^post12+ret_max24^0 == 0 /\ a10^0-a10^post12 == 0 /\ c12^0-c12^post12 == 0 /\ -b11^post12+b11^0 == 0 /\ -y_promoted_2^post12+y_promoted_2^0 == 0 /\ -a10^0+m13^post12 == 0 /\ z^0-z^post12 == 0 /\ a15^0-a15^post12 == 0 /\ ret_min14^0-ret_min14^post12 == 0 /\ tmp620^0-tmp620^post12 == 0 /\ tmp^0-tmp^post12 == 0 /\ -tmp___1^post12+tmp___1^0 == 0 /\ c17^0-c17^post12 == 0 /\ -c12^0+a10^0 <= 0), cost: 1
  13: l11 -> l8 : c12^0'=c12^post13, z^0'=z^post13, tmp^0'=tmp^post13, a15^0'=a15^post13, tmp___1^0'=tmp___1^post13, tmp620^0'=tmp620^post13, m13^0'=m13^post13, b16^0'=b16^post13, y_promoted_2^0'=y_promoted_2^post13, tmp9^0'=tmp9^post13, a10^0'=a10^post13, ret_min14^0'=ret_min14^post13, c17^0'=c17^post13, tmp___0^0'=tmp___0^post13, b11^0'=b11^post13, x_promoted_1^0'=x_promoted_1^post13, tmp923^0'=tmp923^post13, ret_max24^0'=ret_max24^post13, (-tmp923^post13+tmp923^0 == 0 /\ -ret_max24^post13+ret_max24^0 == 0 /\ -y_promoted_2^post13+y_promoted_2^0 == 0 /\ -x_promoted_1^post13+x_promoted_1^0 == 0 /\ b16^0-b16^post13 == 0 /\ -c17^post13+c17^0 == 0 /\ -b11^post13+b11^0 == 0 /\ -ret_min14^post13+ret_min14^0 == 0 /\ z^0-z^post13 == 0 /\ 1-a10^0+b11^0 <= 0 /\ tmp^0-tmp^post13 == 0 /\ -a10^post13+a10^0 == 0 /\ m13^0-m13^post13 == 0 /\ tmp___1^0-tmp___1^post13 == 0 /\ a15^0-a15^post13 == 0 /\ -tmp9^post13+tmp9^0 == 0 /\ -tmp620^post13+tmp620^0 == 0 /\ tmp___0^0-tmp___0^post13 == 0 /\ c12^0-c12^post13 == 0), cost: 1
  14: l11 -> l10 : c12^0'=c12^post14, z^0'=z^post14, tmp^0'=tmp^post14, a15^0'=a15^post14, tmp___1^0'=tmp___1^post14, tmp620^0'=tmp620^post14, m13^0'=m13^post14, b16^0'=b16^post14, y_promoted_2^0'=y_promoted_2^post14, tmp9^0'=tmp9^post14, a10^0'=a10^post14, ret_min14^0'=ret_min14^post14, c17^0'=c17^post14, tmp___0^0'=tmp___0^post14, b11^0'=b11^post14, x_promoted_1^0'=x_promoted_1^post14, tmp923^0'=tmp923^post14, ret_max24^0'=ret_max24^post14, (-a10^post14+a10^0 == 0 /\ -b16^post14+b16^0 == 0 /\ a10^0-b11^0 <= 0 /\ tmp___1^0-tmp___1^post14 == 0 /\ -tmp923^post14+tmp923^0 == 0 /\ z^0-z^post14 == 0 /\ y_promoted_2^0-y_promoted_2^post14 == 0 /\ ret_min14^0-ret_min14^post14 == 0 /\ tmp620^0-tmp620^post14 == 0 /\ tmp^0-tmp^post14 == 0 /\ c12^0-c12^post14 == 0 /\ -x_promoted_1^post14+x_promoted_1^0 == 0 /\ tmp9^0-tmp9^post14 == 0 /\ -tmp___0^post14+tmp___0^0 == 0 /\ m13^0-m13^post14 == 0 /\ -ret_max24^post14+ret_max24^0 == 0 /\ a15^0-a15^post14 == 0 /\ -b11^post14+b11^0 == 0 /\ -c17^post14+c17^0 == 0), cost: 1
  19: l12 -> l4 : c12^0'=c12^post19, z^0'=z^post19, tmp^0'=tmp^post19, a15^0'=a15^post19, tmp___1^0'=tmp___1^post19, tmp620^0'=tmp620^post19, m13^0'=m13^post19, b16^0'=b16^post19, y_promoted_2^0'=y_promoted_2^post19, tmp9^0'=tmp9^post19, a10^0'=a10^post19, ret_min14^0'=ret_min14^post19, c17^0'=c17^post19, tmp___0^0'=tmp___0^post19, b11^0'=b11^post19, x_promoted_1^0'=x_promoted_1^post19, tmp923^0'=tmp923^post19, ret_max24^0'=ret_max24^post19, (a15^0-a15^post19 == 0 /\ tmp620^0-tmp620^post19 == 0 /\ tmp^0-tmp^post19 == 0 /\ m13^0-m13^post19 == 0 /\ a10^0-a10^post19 == 0 /\ c12^0-c12^post19 == 0 /\ -2+y_promoted_2^post19 == 0 /\ -ret_min14^post19+ret_min14^0 == 0 /\ -10+x_promoted_1^post19 == 0 /\ tmp___1^0-tmp___1^post19 == 0 /\ -tmp923^post19+tmp923^0 == 0 /\ b16^0-b16^post19 == 0 /\ tmp9^0-tmp9^post19 == 0 /\ c17^0-c17^post19 == 0 /\ -b11^post19+b11^0 == 0 /\ -tmp___0^post19+tmp___0^0 == 0 /\ -ret_max24^post19+ret_max24^0 == 0 /\ -1+z^post19 == 0), cost: 1
  20: l13 -> l12 : c12^0'=c12^post20, z^0'=z^post20, tmp^0'=tmp^post20, a15^0'=a15^post20, tmp___1^0'=tmp___1^post20, tmp620^0'=tmp620^post20, m13^0'=m13^post20, b16^0'=b16^post20, y_promoted_2^0'=y_promoted_2^post20, tmp9^0'=tmp9^post20, a10^0'=a10^post20, ret_min14^0'=ret_min14^post20, c17^0'=c17^post20, tmp___0^0'=tmp___0^post20, b11^0'=b11^post20, x_promoted_1^0'=x_promoted_1^post20, tmp923^0'=tmp923^post20, ret_max24^0'=ret_max24^post20, (-b11^post20+b11^0 == 0 /\ -a10^post20+a10^0 == 0 /\ x_promoted_1^0-x_promoted_1^post20 == 0 /\ ret_min14^0-ret_min14^post20 == 0 /\ b16^0-b16^post20 == 0 /\ -tmp___0^post20+tmp___0^0 == 0 /\ -ret_max24^post20+ret_max24^0 == 0 /\ c12^0-c12^post20 == 0 /\ tmp___1^0-tmp___1^post20 == 0 /\ -c17^post20+c17^0 == 0 /\ z^0-z^post20 == 0 /\ -tmp9^post20+tmp9^0 == 0 /\ a15^0-a15^post20 == 0 /\ tmp620^0-tmp620^post20 == 0 /\ -tmp923^post20+tmp923^0 == 0 /\ -tmp^post20+tmp^0 == 0 /\ y_promoted_2^0-y_promoted_2^post20 == 0 /\ -m13^post20+m13^0 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l13
  <empty>


Computing asymptotic complexity

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

Solved cost: 0
Rule cost:   0