correct filename and path

opencompl · Nov 4, 2024 · 11ce2f2 · 11ce2f2
1 parent abfa940
commit 11ce2f2
Show file tree

Hide file tree

Showing 7 changed files with 9,637 additions and 773 deletions.
diff --git a/bv-evaluation/collect-data-hdel.py b/bv-evaluation/collect-data-hdel.py
@@ -213,7 +213,7 @@
 
 df_err_sorted = df_err.drop(columns='msg_count')
 
-df_err_sorted.to_csv(raw_data_dir+'err-llvm.csv')
+df_err_sorted.to_csv(raw_data_dir+'err-hackersdelight.csv')
 
 
 df = pd.DataFrame({'bitwuzla':bitwuzla_times, 'leanSAT':leanSAT_tot_times,
@@ -224,5 +224,5 @@
                     'leanSAT-rw':counter_leanSAT_rw_times, 'leanSAT-sat':counter_leanSAT_sat_times})
 
 
-df.to_csv(raw_data_dir+'llvm-proved-data.csv')
-df_ceg.to_csv(raw_data_dir+'llvm-ceg-data.csv')
+df.to_csv(raw_data_dir+'hackersdelight-proved-data.csv')
+df_ceg.to_csv(raw_data_dir+'hackersdelight-ceg-data.csv')
diff --git a/bv-evaluation/raw-data/err-hackersdelight.csv b/bv-evaluation/raw-data/err-hackersdelight.csv
diff --git a/bv-evaluation/raw-data/err-llvm.csv b/bv-evaluation/raw-data/err-llvm.csv
diff --git a/bv-evaluation/raw-data/hackersdelight-ceg-data.csv b/bv-evaluation/raw-data/hackersdelight-ceg-data.csv
@@ -0,0 +1,211 @@
+,bitwuzla,leanSAT,leanSAT-rw,leanSAT-sat
+0,68.486702,66.991842,66.991842,66.991842
+1,64.499262,66.991842,66.991842,66.991842
+2,95.098941,66.991842,66.991842,66.991842
+3,95.027003,66.991842,66.991842,66.991842
+4,83.665605,66.991842,66.991842,66.991842
+5,90.695154,66.991842,66.991842,66.991842
+6,85.429693,66.991842,66.991842,66.991842
+7,74.119614,66.991842,66.991842,66.991842
+8,88.441103,66.991842,66.991842,66.991842
+9,89.021926,66.991842,66.991842,66.991842
+10,93.046807,66.991842,66.991842,66.991842
+11,81.653753,66.991842,66.991842,66.991842
+12,78.475159,66.991842,66.991842,66.991842
+13,68.965134,66.991842,66.991842,66.991842
+14,82.323445,66.991842,66.991842,66.991842
+15,84.048219,66.991842,66.991842,66.991842
+16,70.586041,66.991842,66.991842,66.991842
+17,107.379285,66.991842,66.991842,66.991842
+18,69.643743,66.991842,66.991842,66.991842
+19,77.790487,66.991842,66.991842,66.991842
+20,84.673266,66.991842,66.991842,66.991842
+21,77.020013,66.991842,66.991842,66.991842
+22,73.864163,66.991842,66.991842,66.991842
+23,87.795605,66.991842,66.991842,66.991842
+24,77.623753,66.991842,66.991842,66.991842
+25,76.9063,66.991842,66.991842,66.991842
+26,77.577325,66.991842,66.991842,66.991842
+27,94.261609,66.991842,66.991842,66.991842
+28,89.746062,66.991842,66.991842,66.991842
+29,86.942791,66.991842,66.991842,66.991842
+30,92.760017,66.991842,66.991842,66.991842
+31,81.924969,66.991842,66.991842,66.991842
+32,92.548558,66.991842,66.991842,66.991842
+33,87.878461,66.991842,66.991842,66.991842
+34,101.256257,66.991842,66.991842,66.991842
+35,86.598068,66.991842,66.991842,66.991842
+36,83.004981,66.991842,66.991842,66.991842
+37,103.747144,66.991842,66.991842,66.991842
+38,96.784846,66.991842,66.991842,66.991842
+39,72.141572,66.991842,66.991842,66.991842
+40,70.495195,66.991842,66.991842,66.991842
+41,66.991842,66.991842,66.991842,66.991842
+42,69.293372,74.051886,74.051886,74.051886
+43,66.233322,74.051886,74.051886,74.051886
+44,98.145613,74.051886,74.051886,74.051886
+45,103.232653,74.051886,74.051886,74.051886
+46,88.619899,74.051886,74.051886,74.051886
+47,90.845897,74.051886,74.051886,74.051886
+48,77.765591,74.051886,74.051886,74.051886
+49,82.324847,74.051886,74.051886,74.051886
+50,92.474437,74.051886,74.051886,74.051886
+51,88.646366,74.051886,74.051886,74.051886
+52,92.710063,74.051886,74.051886,74.051886
+53,87.755349,74.051886,74.051886,74.051886
+54,78.694011,74.051886,74.051886,74.051886
+55,77.414848,74.051886,74.051886,74.051886
+56,82.382627,74.051886,74.051886,74.051886
+57,84.462921,74.051886,74.051886,74.051886
+58,79.096049,74.051886,74.051886,74.051886
+59,105.282302,74.051886,74.051886,74.051886
+60,70.106015,74.051886,74.051886,74.051886
+61,71.959592,74.051886,74.051886,74.051886
+62,82.633169,74.051886,74.051886,74.051886
+63,71.53505,74.051886,74.051886,74.051886
+64,82.185045,74.051886,74.051886,74.051886
+65,81.133964,74.051886,74.051886,74.051886
+66,76.762721,74.051886,74.051886,74.051886
+67,77.197086,74.051886,74.051886,74.051886
+68,82.357821,74.051886,74.051886,74.051886
+69,93.714837,74.051886,74.051886,74.051886
+70,94.902827,74.051886,74.051886,74.051886
+71,93.877964,74.051886,74.051886,74.051886
+72,92.17346,74.051886,74.051886,74.051886
+73,89.66472,74.051886,74.051886,74.051886
+74,95.541021,74.051886,74.051886,74.051886
+75,94.203509,74.051886,74.051886,74.051886
+76,99.34285,74.051886,74.051886,74.051886
+77,84.96634,74.051886,74.051886,74.051886
+78,91.392156,74.051886,74.051886,74.051886
+79,96.905584,74.051886,74.051886,74.051886
+80,101.790907,74.051886,74.051886,74.051886
+81,73.514252,74.051886,74.051886,74.051886
+82,74.141166,74.051886,74.051886,74.051886
+83,74.051886,74.051886,74.051886,74.051886
+84,68.967579,64.716764,64.716764,64.716764
+85,68.168513,64.716764,64.716764,64.716764
+86,91.283453,64.716764,64.716764,64.716764
+87,95.448676,64.716764,64.716764,64.716764
+88,85.005884,64.716764,64.716764,64.716764
+89,91.168956,64.716764,64.716764,64.716764
+90,77.096451,64.716764,64.716764,64.716764
+91,78.617738,64.716764,64.716764,64.716764
+92,92.731974,64.716764,64.716764,64.716764
+93,84.785799,64.716764,64.716764,64.716764
+94,84.024662,64.716764,64.716764,64.716764
+95,80.284869,64.716764,64.716764,64.716764
+96,77.540074,64.716764,64.716764,64.716764
+97,73.181666,64.716764,64.716764,64.716764
+98,73.15747,64.716764,64.716764,64.716764
+99,80.612208,64.716764,64.716764,64.716764
+100,75.792759,64.716764,64.716764,64.716764
+101,95.730609,64.716764,64.716764,64.716764
+102,72.146574,64.716764,64.716764,64.716764
+103,68.534673,64.716764,64.716764,64.716764
+104,75.641274,64.716764,64.716764,64.716764
+105,68.914939,64.716764,64.716764,64.716764
+106,77.298398,64.716764,64.716764,64.716764
+107,79.134061,64.716764,64.716764,64.716764
+108,69.065003,64.716764,64.716764,64.716764
+109,72.726738,64.716764,64.716764,64.716764
+110,80.031774,64.716764,64.716764,64.716764
+111,90.815009,64.716764,64.716764,64.716764
+112,89.161131,64.716764,64.716764,64.716764
+113,86.672337,64.716764,64.716764,64.716764
+114,91.856973,64.716764,64.716764,64.716764
+115,80.461955,64.716764,64.716764,64.716764
+116,86.39307,64.716764,64.716764,64.716764
+117,86.131054,64.716764,64.716764,64.716764
+118,90.986511,64.716764,64.716764,64.716764
+119,80.227513,64.716764,64.716764,64.716764
+120,81.192711,64.716764,64.716764,64.716764
+121,96.978591,64.716764,64.716764,64.716764
+122,91.629764,64.716764,64.716764,64.716764
+123,63.769736,64.716764,64.716764,64.716764
+124,64.802464,64.716764,64.716764,64.716764
+125,64.716764,64.716764,64.716764,64.716764
+126,66.151018,70.128266,70.128266,70.128266
+127,68.898619,70.128266,70.128266,70.128266
+128,95.656699,70.128266,70.128266,70.128266
+129,94.865999,70.128266,70.128266,70.128266
+130,84.331133,70.128266,70.128266,70.128266
+131,87.166929,70.128266,70.128266,70.128266
+132,81.507385,70.128266,70.128266,70.128266
+133,75.505859,70.128266,70.128266,70.128266
+134,88.28125,70.128266,70.128266,70.128266
+135,84.33547,70.128266,70.128266,70.128266
+136,88.472701,70.128266,70.128266,70.128266
+137,86.503788,70.128266,70.128266,70.128266
+138,73.127192,70.128266,70.128266,70.128266
+139,73.447788,70.128266,70.128266,70.128266
+140,79.096229,70.128266,70.128266,70.128266
+141,80.099291,70.128266,70.128266,70.128266
+142,75.6498,70.128266,70.128266,70.128266
+143,100.399222,70.128266,70.128266,70.128266
+144,70.610026,70.128266,70.128266,70.128266
+145,72.842856,70.128266,70.128266,70.128266
+146,79.382268,70.128266,70.128266,70.128266
+147,72.550707,70.128266,70.128266,70.128266
+148,79.106789,70.128266,70.128266,70.128266
+149,82.227154,70.128266,70.128266,70.128266
+150,73.73623,70.128266,70.128266,70.128266
+151,72.674458,70.128266,70.128266,70.128266
+152,82.859395,70.128266,70.128266,70.128266
+153,90.056508,70.128266,70.128266,70.128266
+154,88.574825,70.128266,70.128266,70.128266
+155,89.131844,70.128266,70.128266,70.128266
+156,92.235297,70.128266,70.128266,70.128266
+157,84.779364,70.128266,70.128266,70.128266
+158,91.939269,70.128266,70.128266,70.128266
+159,89.307376,70.128266,70.128266,70.128266
+160,96.308238,70.128266,70.128266,70.128266
+161,86.370337,70.128266,70.128266,70.128266
+162,87.129699,70.128266,70.128266,70.128266
+163,98.925073,70.128266,70.128266,70.128266
+164,99.753764,70.128266,70.128266,70.128266
+165,69.3659,70.128266,70.128266,70.128266
+166,71.500064,70.128266,70.128266,70.128266
+167,70.128266,70.128266,70.128266,70.128266
+168,69.179648,77.774427,77.774427,77.774427
+169,68.52839,77.774427,77.774427,77.774427
+170,92.190863,77.774427,77.774427,77.774427
+171,100.812361,77.774427,77.774427,77.774427
+172,86.072925,77.774427,77.774427,77.774427
+173,87.785586,77.774427,77.774427,77.774427
+174,82.669959,77.774427,77.774427,77.774427
+175,79.348014,77.774427,77.774427,77.774427
+176,88.930505,77.774427,77.774427,77.774427
+177,85.984548,77.774427,77.774427,77.774427
+178,88.816049,77.774427,77.774427,77.774427
+179,84.843987,77.774427,77.774427,77.774427
+180,74.530089,77.774427,77.774427,77.774427
+181,74.31854,77.774427,77.774427,77.774427
+182,78.388975,77.774427,77.774427,77.774427
+183,80.10367,77.774427,77.774427,77.774427
+184,75.478588,77.774427,77.774427,77.774427
+185,100.845264,77.774427,77.774427,77.774427
+186,122.88259,77.774427,77.774427,77.774427
+187,74.322958,77.774427,77.774427,77.774427
+188,81.719917,77.774427,77.774427,77.774427
+189,74.336538,77.774427,77.774427,77.774427
+190,80.527799,77.774427,77.774427,77.774427
+191,84.179516,77.774427,77.774427,77.774427
+192,74.052849,77.774427,77.774427,77.774427
+193,74.19165,77.774427,77.774427,77.774427
+194,86.031437,77.774427,77.774427,77.774427
+195,91.344427,77.774427,77.774427,77.774427
+196,86.247094,77.774427,77.774427,77.774427
+197,98.06477,77.774427,77.774427,77.774427
+198,89.35783,77.774427,77.774427,77.774427
+199,94.62948,77.774427,77.774427,77.774427
+200,99.37996,77.774427,77.774427,77.774427
+201,99.247349,77.774427,77.774427,77.774427
+202,98.348074,77.774427,77.774427,77.774427
+203,92.391913,77.774427,77.774427,77.774427
+204,94.164565,77.774427,77.774427,77.774427
+205,107.403048,77.774427,77.774427,77.774427
+206,105.448243,77.774427,77.774427,77.774427
+207,75.810563,77.774427,77.774427,77.774427
+208,80.1044,77.774427,77.774427,77.774427
+209,77.774427,77.774427,77.774427,77.774427
diff --git a/bv-evaluation/raw-data/hackersdelight-proved-data.csv b/bv-evaluation/raw-data/hackersdelight-proved-data.csv
@@ -0,0 +1,156 @@
+,bitwuzla,leanSAT,leanSAT-rw,leanSAT-bb,leanSAT-sat,leanSAT-lrat-t,leanSAT-lrat-c
+0,8.669248,7.549957,7.535049,0.0,0.0,0.0,0.0
+1,80.80288,84.762224,19.232478,0.0,57.449729,0.0,5.877383
+2,10.0328,10.294724,10.283794,0.0,0.0,0.0,0.0
+3,7.207451,7.391449,7.380818,0.0,0.0,0.0,0.0
+4,9.817344,9.989969,9.979069,0.0,0.0,0.0,0.0
+5,86.606713,99.714167,29.272071,0.0,57.452336,3.067094,8.207187
+6,79.39843,86.491305,19.932077,0.0,57.597066,1.207517,6.114451
+7,76.75267,79.585553,16.248923,0.0,57.085501,1.035102,3.059911
+8,87.891646,96.902509,28.419042,0.0,57.277334,1.920893,7.512889
+9,85.671469,97.848162,27.03391,0.0,57.436465,3.21339,8.466927
+10,92.937041,114.749204,42.511068,0.0,57.523837,5.47199,7.868129
+11,90.74093,105.431041,34.259777,0.0,57.476647,3.167153,8.862623
+12,95.24291,108.191858,37.392645,0.0,57.289176,4.63426,7.202062
+13,87.093261,91.819835,28.964401,0.0,57.541602,1.086769,2.364058
+14,81.500704,91.28237,26.24344,0.0,57.427587,1.019874,5.032691
+15,81.139643,94.11388,30.162661,0.0,57.605443,1.249307,4.123957
+16,91.262752,118.019541,40.179021,0.0,62.008976,4.906964,9.31151
+17,80.979992,88.231096,21.549248,0.0,57.227158,1.475703,6.450625
+18,87.308417,96.348755,28.313083,0.0,57.224776,1.813292,7.295058
+19,76.533808,86.657359,22.714836,0.0,57.632985,0.0,4.272978
+20,70.347651,79.342744,16.062831,0.0,57.431605,0.0,3.9557
+21,79.29285,92.940137,28.093969,0.0,57.719458,1.354674,3.646587
+22,8.845982,8.246491,8.233036,0.0,0.0,0.0,0.0
+23,82.103652,87.868832,20.145138,0.0,57.181732,1.665,7.156657
+24,10.183965,10.095397,10.084237,0.0,0.0,0.0,0.0
+25,7.400616,7.479074,7.468084,0.0,0.0,0.0,0.0
+26,10.029773,10.753089,10.741807,0.0,0.0,0.0,0.0
+27,81.040204,102.861046,32.271538,0.0,56.80915,5.904325,6.693423
+28,79.961071,91.306365,20.814792,0.0,57.39267,2.380039,8.567377
+29,72.624526,81.108103,17.067205,0.0,57.097174,1.930942,3.988421
+30,87.777802,111.006817,26.866004,0.0,57.528437,14.86397,10.239439
+31,84.232977,112.773997,31.686926,0.0,57.283603,8.30963,13.58001
+32,89.798894,108.535135,34.279594,0.0,57.263659,7.132862,8.131574
+33,90.73026,119.073509,39.532259,0.0,57.173979,10.345018,10.084457
+34,93.104567,134.064639,33.786475,0.0,57.182784,25.266257,15.910163
+35,82.626427,98.416944,24.478452,0.0,57.512217,4.94846,9.72613
+36,81.972403,90.906773,26.455511,0.0,57.843442,2.40731,3.144499
+37,81.841416,96.417283,24.602554,0.0,57.730579,3.604847,8.778647
+38,90.29008,126.283164,33.197725,0.0,57.279277,16.479056,17.367801
+39,80.210903,99.712587,22.149549,0.0,57.179049,6.853674,11.679263
+40,87.67704,110.236925,37.799944,0.0,57.536713,3.391276,9.620272
+41,73.270905,88.047661,23.449923,0.0,57.264219,0.0,4.865564
+42,70.435928,80.759577,16.336618,0.0,57.243961,0.0,4.716253
+43,79.40912,101.648478,28.186405,0.0,57.944171,4.047162,9.718859
+44,8.746694,8.280565,8.266749,0.0,0.0,0.0,0.0
+45,83.071317,82.832024,19.401957,0.0,53.595391,2.689152,5.782604
+46,9.931448,10.014476,10.002994,0.0,0.0,0.0,0.0
+47,7.307389,7.511295,7.500344,0.0,0.0,0.0,0.0
+48,9.670096,9.74686,9.736221,0.0,0.0,0.0,0.0
+49,78.3327,118.351588,29.85957,0.0,53.707572,15.561636,16.882877
+50,80.191246,90.227531,20.991746,0.0,53.436611,5.632762,7.374207
+51,76.812013,85.378947,18.517721,0.0,53.747667,3.855581,7.358466
+52,86.538215,117.417185,27.080307,0.0,53.490573,19.115176,14.427988
+53,85.228684,112.406816,28.396229,0.0,53.577607,15.724493,12.862566
+54,94.15625,151.984352,35.495358,1.055541,53.532171,33.891092,25.262641
+55,91.905976,125.181826,37.127374,0.0,53.753289,18.364561,14.094328
+56,92.703079,158.174525,38.895669,0.0,57.454147,33.589944,24.650495
+57,85.078933,101.442781,24.601725,0.0,57.790913,5.638524,11.354634
+58,82.013131,98.140392,26.650728,0.0,57.629597,3.474873,8.267882
+59,81.234021,95.697787,28.800773,0.0,57.606784,4.105341,3.747699
+60,93.002612,152.085873,36.137468,0.0,57.90117,33.661218,22.331091
+61,81.899397,103.036907,23.274059,0.0,53.636778,10.893693,12.96121
+62,85.298346,98.448485,30.118517,0.0,53.878874,3.982059,8.382006
+63,73.204228,88.08459,21.941356,0.0,57.396057,1.135332,5.77437
+64,70.741675,82.637136,15.168554,0.0,57.525429,1.780458,6.297176
+65,77.618672,98.216257,21.614031,0.0,57.279346,5.410444,11.899138
+66,8.740173,8.304881,8.291536,0.0,0.0,0.0,0.0
+67,81.352964,95.202073,25.082711,0.0,57.845666,4.098368,6.07652
+68,11.189871,10.29318,10.28257,0.0,0.0,0.0,0.0
+69,7.272174,7.362414,7.351975,0.0,0.0,0.0,0.0
+70,9.770264,9.974661,9.964029,0.0,0.0,0.0,0.0
+71,82.337764,141.427643,25.304118,0.0,57.732282,29.188905,26.501698
+72,81.649374,147.310447,23.834597,4.191814,57.764462,28.967177,26.889898
+73,77.445597,114.693218,32.932644,0.0,57.292462,7.01038,14.772829
+74,88.178767,222.952261,41.873996,3.915995,107.867676,25.888831,37.368461
+75,87.852092,146.900255,36.663841,0.0,58.08623,25.81378,23.331718
+76,147.781215,296.444675,50.226578,4.091736,108.017138,65.200305,61.956938
+77,93.481856,199.1946,35.098488,0.0,108.313437,27.931944,24.515682
+78,96.386586,284.469492,50.018405,4.247339,108.202569,49.323514,65.571575
+79,84.461247,111.339985,31.037891,0.0,56.961177,7.481268,12.853049
+80,83.950623,107.341425,24.759812,0.0,58.332674,7.449858,13.964946
+81,84.225493,111.907826,29.334468,0.0,56.923386,11.839928,10.73361
+82,92.305389,375.657344,35.514754,0.0,208.074627,65.019423,63.237944
+83,84.407686,116.8109,26.942376,0.0,57.295357,11.717166,17.580465
+84,90.757992,125.028428,32.080828,0.0,58.639291,13.557426,17.819284
+85,77.301043,86.641629,20.912606,0.0,57.877866,1.090516,4.722857
+86,75.589175,92.368358,20.001648,0.0,60.889145,2.755847,6.773323
+87,82.016526,104.460541,30.446325,0.0,57.278586,4.802696,9.606016
+88,8.795127,8.209252,8.194394,0.0,0.0,0.0,0.0
+89,82.572725,115.613244,27.330559,0.0,57.929282,10.258335,16.091476
+90,11.118407,10.993933,10.981829,0.0,0.0,0.0,0.0
+91,7.810099,8.057886,8.046204,0.0,0.0,0.0,0.0
+92,10.586564,10.714956,10.703304,0.0,0.0,0.0,0.0
+93,84.052145,459.012615,30.690947,0.0,257.649464,79.731689,85.848523
+94,82.516189,372.718663,32.783604,14.765515,158.545645,61.942781,86.622905
+95,78.482653,119.512707,25.940247,0.0,54.288738,14.277565,21.109438
+96,89.020234,593.008967,36.014706,16.291542,308.541987,105.724756,107.15882
+97,88.636872,403.572565,35.160004,0.0,205.011498,80.121062,77.865858
+98,198.290316,831.795277,43.951685,16.351856,460.512333,132.370673,157.610412
+99,94.962511,318.753165,33.880692,0.0,159.958239,57.687566,61.409055
+100,248.776753,1038.98836,39.196024,17.140133,561.028407,185.870844,214.497677
+101,88.976943,145.133642,29.451098,0.0,59.33311,28.363288,23.361526
+102,84.960338,130.795946,37.916153,0.0,59.515544,13.43179,15.520929
+103,85.270323,133.198646,31.26532,0.0,59.618568,21.901251,16.602501
+104,95.33321,789.560912,39.399119,0.0,460.733509,139.778323,143.066055
+105,84.201558,269.421243,21.841078,0.0,159.505103,43.310926,40.432327
+106,91.469673,162.890288,28.383585,0.0,59.197545,38.347716,32.534914
+107,73.800333,94.388849,21.866395,0.0,59.312321,3.968815,6.389809
+108,71.028815,108.777773,22.78087,0.0,59.412381,10.712561,13.329868
+109,81.577719,125.349152,22.964767,0.0,58.726304,17.849149,21.052811
+110,74.44569,73.048505,12.715218,0.0,53.707121,0.0,3.850532
+111,73.023097,78.29517,15.390232,0.0,57.141316,0.0,3.060832
+112,10.744031,10.54224,10.531731,0.0,0.0,0.0,0.0
+113,74.373866,83.925815,19.029405,0.0,57.228599,0.0,5.443867
+114,9.883268,9.801934,9.791565,0.0,0.0,0.0,0.0
+115,70.59599,71.636892,12.066335,0.0,53.573639,0.0,3.148507
+116,70.047595,74.943569,16.849185,0.0,53.395573,0.0,2.988877
+117,80.471203,82.628631,21.734617,0.0,53.322916,2.192384,4.402974
+118,81.766505,91.003254,25.98924,0.0,57.148671,2.086205,3.95018
+119,75.906073,77.521511,13.81941,0.0,57.07866,0.0,3.710689
+120,73.967257,78.115231,14.442507,0.0,57.416256,0.0,4.224025
+121,10.863166,10.630056,10.619857,0.0,0.0,0.0,0.0
+122,74.974417,81.205456,18.741313,0.0,56.95245,1.525357,2.973197
+123,10.149359,9.963449,9.952428,0.0,0.0,0.0,0.0
+124,70.905443,82.331608,18.916243,0.0,56.712296,0.0,4.509935
+125,70.647788,78.739027,16.19987,0.0,56.928716,0.0,3.735194
+126,80.741072,94.754168,22.506392,0.0,57.205328,3.797621,9.415224
+127,79.988863,98.409221,29.043098,0.0,57.033413,5.948629,5.243908
+128,75.037826,81.125376,15.77036,0.0,57.09008,0.0,5.650876
+129,73.567654,83.677939,19.348035,0.0,56.863965,0.0,4.962089
+130,11.012608,10.778005,10.767075,0.0,0.0,0.0,0.0
+131,78.888078,89.771922,20.191096,0.0,56.721516,2.590285,8.348413
+132,10.177903,10.348465,10.337084,0.0,0.0,0.0,0.0
+133,67.48859,83.041511,18.006095,0.0,57.220467,0.0,5.280537
+134,66.936699,82.423976,18.851981,0.0,56.981086,0.0,4.119658
+135,76.708978,104.798536,24.441923,0.0,56.345386,7.541763,14.202473
+136,78.441377,102.470107,28.674002,0.0,57.058341,7.304253,7.888215
+137,75.891786,88.305838,20.435007,0.0,57.151946,1.278972,7.245043
+138,73.954265,78.222141,14.865493,0.0,53.6218,1.285343,6.427611
+139,11.068032,10.429567,10.419118,0.0,0.0,0.0,0.0
+140,77.978162,93.961192,18.770317,0.0,53.487637,5.873296,13.367318
+141,9.922613,10.236795,10.226014,0.0,0.0,0.0,0.0
+142,70.761052,84.396676,16.712736,0.0,57.393603,1.384281,6.886215
+143,70.864917,82.494317,16.037903,0.0,57.543776,1.257983,5.703376
+144,77.227905,113.317775,22.703233,0.0,57.322278,18.160386,12.53046
+145,82.20436,125.538801,30.506278,0.0,57.560928,18.401191,15.903823
+146,75.09311,84.506341,15.504508,0.0,53.831285,2.41834,9.804498
+147,69.927809,81.526182,14.982684,0.0,53.303009,1.842465,8.932376
+148,10.898172,10.567208,10.556417,0.0,0.0,0.0,0.0
+149,73.93703,99.34273,18.759697,0.0,56.696878,9.247789,11.797528
+150,10.230643,10.124313,10.113042,0.0,0.0,0.0,0.0
+151,70.44699,80.684855,11.660699,0.0,56.942171,2.494464,6.823228
+152,70.956189,85.185172,13.568237,0.0,57.298924,2.461032,9.065595
+153,80.625885,135.966745,22.563409,0.0,57.00519,28.008258,24.076653
+154,81.133963,265.908559,21.937369,0.0,157.278154,44.277227,38.168608