chore: fix data collection script for HackersDelight

bv-evaluation/collect-data-hdel.py

@@ -5,7 +5,7 @@
 
 benchmark_dir = "../SSA/Projects/InstCombine/HackersDelight/"
 res_dir = "results/HackersDelight/"
-raw_data_dir = 'raw-data/'
+raw_data_dir = '../../paper-lean-bitvectors/raw-data/HackersDelight/'
 reps = 1
 
 bv_width = [4, 8, 16, 32, 64]
@@ -102,6 +102,7 @@
                         cegl = False
                         if "counter example" in l: 
                             tot = float(l.split("ms")[0].split("after ")[1])
+                            print(counter_leanSAT_rw_times_average)
                             if r == 0:
                                 counter_leanSAT_tot_times_average.append([tot])
                                 counter_leanSAT_rw_times_average.append([float(l.split(" SAT")[0].split("rewriting ")[1])])
@@ -185,13 +186,14 @@
         for thm in counter_bitwuzla_times_average: 
             counter_bitwuzla_times.append(np.mean(thm))
 
-        for counter_thm in counter_leanSAT_tot_times_average: 
+        for thm in counter_leanSAT_tot_times_average: 
             counter_leanSAT_tot_times.append(np.mean(thm))
 
-        for counter_thm in counter_leanSAT_rw_times_average: 
+        for thm in counter_leanSAT_rw_times_average: 
             counter_leanSAT_rw_times.append(np.mean(thm))
 
-        for counter_thm in counter_leanSAT_sat_times_average: 
+        for thm in counter_leanSAT_sat_times_average: 
+            print(counter_leanSAT_sat_times_average)
             counter_leanSAT_sat_times.append(np.mean(thm))
 
         print("\n\nwith bitwidth = "+str(bvw))

bv-evaluation/compare-leansat-vs-bitwuzla-hdel.py

@@ -14,7 +14,7 @@
 for file in os.listdir(benchmark_dir_list):
     print(file)
     for bvw in bv_width:
-        subprocess.Popen('sed -i -E \'s/variable \{x y z : BitVec .+\}/variable \{x y z : BitVec '+str(bvw)+'\}/g\' '+benchmark_dir_list+file, shell=True).wait()
+        subprocess.Popen('sed -i -E \'s/variable \\{x y z : BitVec .+\\}/variable \\{x y z : BitVec '+str(bvw)+'\\}/g\' '+benchmark_dir_list+file, shell=True).wait()
         # replace any sorrys with bv_compare'
         subprocess.Popen('sed -i -E \'s,all_goals sorry,bv_compare\'\\\'\',g\' '+benchmark_dir_list+file, shell=True).wait()
         for r in range(reps):

bv-evaluation/raw-data/bvw16_ch2_1DeMorgan_proved_data.csv

@@ -1,10 +1,10 @@
 ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-bb,leanSAT-sat,leanSAT-lrat-t,leanSAT-lrat-c
-0,74.298435,80.396675,16.455224,0.0,55.543381,0.0,5.826306
-1,72.01669,80.094915,16.808351,0.0,55.751404,0.0,5.068354
-2,11.793657,11.47676,11.465999,0.0,0.0,0.0,0.0
-3,77.392578,80.375295,18.610391,0.0,54.021159,2.60192,3.883349
-4,9.818269,10.249333,10.23753,0.0,0.0,0.0,0.0
-5,67.896485,73.55371,11.803626,0.0,54.080661,0.0,5.158505
-6,68.331224,77.304229,17.405027,0.0,53.308384,0.0,4.163286
-7,76.966923,108.454276,36.044964,0.0,56.201444,7.840046,6.606608
-8,80.67495,110.0302,34.368801,0.0,55.612192,10.60878,7.89479
+0,78.140528,85.550821,16.724231,0.0,60.400822,0.0,5.806677
+1,75.441052,81.788411,13.720732,0.0,60.51121,0.0,5.13553
+2,10.61995,10.376751,10.365901,0.0,0.0,0.0,0.0
+3,80.636247,89.963016,22.19868,0.0,59.972171,2.480871,3.927914
+4,9.864515,9.872,9.860588,0.0,0.0,0.0,0.0
+5,73.295454,84.502232,17.2349,0.0,59.461098,0.0,5.27291
+6,73.456558,80.359625,14.233079,0.0,59.348295,0.0,4.240562
+7,83.190798,106.426705,21.386167,0.0,60.115231,7.625069,15.072343
+8,83.178815,116.881543,29.029732,0.0,60.540695,11.33997,13.722085

bv-evaluation/raw-data/bvw16_ch2_2AdditionAndLogicalOps_proved_data.csv

@@ -1,23 +1,23 @@
 ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-bb,leanSAT-sat,leanSAT-lrat-t,leanSAT-lrat-c
-0,8.174278,7.65695,7.644376,0.0,0.0,0.0,0.0
-1,78.42752,90.602658,25.068318,0.0,54.191141,2.677073,6.757064
-2,10.874422,10.906604,10.894861,0.0,0.0,0.0,0.0
-3,7.866577,7.935004,7.923633,0.0,0.0,0.0,0.0
-4,10.635231,10.636444,10.624621,0.0,0.0,0.0,0.0
-5,81.666393,112.4303,26.026047,0.0,54.226658,15.454124,14.347696
-6,77.794867,89.042894,20.372748,0.0,53.899921,4.647902,7.327168
-7,73.168074,89.076487,21.169683,0.0,54.12713,3.949753,7.819377
-8,85.97836,117.532669,27.790827,0.0,53.855015,18.390898,14.133152
-9,81.330628,105.021699,29.78949,0.0,54.019646,8.750173,10.792768
-10,91.116929,148.51104,34.05666,1.011769,54.105998,33.394983,23.384232
-11,89.564709,115.880581,31.275522,0.0,54.207902,15.229031,13.268612
-12,93.220146,156.656225,39.34369,1.079917,54.524299,35.738034,23.28764
-13,80.48937,103.536145,29.548114,0.0,54.391539,5.746035,11.677116
-14,82.801154,91.51487,28.234944,0.0,55.678027,2.737216,3.436627
-15,78.907285,89.509414,25.591818,0.0,54.346253,4.204524,3.858132
-16,90.283095,142.930241,38.794563,0.0,54.219234,26.893785,21.091414
-17,79.74116,90.620159,21.25907,0.0,54.322919,5.499639,7.956997
-18,85.910472,105.73785,32.980011,0.0,54.334861,4.634808,11.469185
-19,72.960853,85.070616,22.808092,0.0,53.899109,0.0,5.876409
-20,70.037687,80.719704,17.392423,0.0,53.572121,1.704617,6.241921
-21,75.213112,93.486509,20.749439,0.0,53.368348,5.594748,11.718646
+0,9.015013,8.204822,8.190115,0.0,0.0,0.0,0.0
+1,82.260602,94.926454,26.60216,0.0,58.078881,2.736956,6.100241
+2,10.676999,9.998188,9.987447,0.0,0.0,0.0,0.0
+3,7.40803,7.3125,7.301448,0.0,0.0,0.0,0.0
+4,9.649029,9.758796,9.747905,0.0,0.0,0.0,0.0
+5,82.555569,116.197304,27.411438,0.0,57.812127,15.523424,13.122374
+6,80.094674,115.890182,30.336528,0.0,57.948212,6.628348,17.498672
+7,76.142116,89.945675,16.673935,0.0,58.037231,3.861647,9.439434
+8,87.30405,124.258446,29.933166,0.0,57.876887,17.809549,15.419026
+9,85.933484,124.030675,26.476032,0.0,58.302872,15.618643,21.206628
+10,95.452136,154.467581,35.980037,0.0,57.963402,32.973353,24.051507
+11,90.686793,117.734334,31.338909,0.0,58.062899,12.549452,13.884271
+12,93.922599,152.566395,34.383014,1.052176,57.843516,31.766556,24.729728
+13,85.100312,101.502213,25.6481,0.0,57.956188,5.561395,10.22353
+14,83.195486,96.125867,24.187965,0.0,58.047811,3.460762,8.385473
+15,82.650369,100.272362,26.949757,0.0,58.214716,4.250662,8.75996
+16,93.130305,143.136931,30.075164,0.0,58.170733,32.162553,20.779995
+17,81.946341,104.851071,21.400083,0.0,58.415173,11.10144,11.612664
+18,87.961381,100.298451,27.94295,0.0,58.501337,5.070007,6.957059
+19,77.990804,83.085248,17.939604,0.0,58.144644,1.00134,4.280739
+20,75.004439,80.619375,15.960338,0.0,57.971156,1.687745,3.686596
+21,82.867747,90.999503,22.262381,0.0,58.406217,3.593912,5.341962

bv-evaluation/raw-data/bvw16_ch2_3LogicalArithmeticIneq_ceg_data.csv

@@ -1,43 +1,43 @@
 ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-sat
-0,67.624229,68.964006,68.964006,68.964006
-1,66.230327,68.964006,68.964006,68.964006
-2,96.254569,68.964006,68.964006,68.964006
-3,100.854038,68.964006,68.964006,68.964006
-4,83.936832,68.964006,68.964006,68.964006
-5,85.661196,68.964006,68.964006,68.964006
-6,79.697662,68.964006,68.964006,68.964006
-7,84.970864,68.964006,68.964006,68.964006
-8,88.605584,68.964006,68.964006,68.964006
-9,82.853197,68.964006,68.964006,68.964006
-10,88.093908,68.964006,68.964006,68.964006
-11,84.495567,68.964006,68.964006,68.964006
-12,72.740393,68.964006,68.964006,68.964006
-13,73.175164,68.964006,68.964006,68.964006
-14,77.93119,68.964006,68.964006,68.964006
-15,79.583596,68.964006,68.964006,68.964006
-16,75.650003,68.964006,68.964006,68.964006
-17,102.746881,68.964006,68.964006,68.964006
-18,73.568443,68.964006,68.964006,68.964006
-19,69.861851,68.964006,68.964006,68.964006
-20,79.956341,68.964006,68.964006,68.964006
-21,71.771344,68.964006,68.964006,68.964006
-22,78.553885,68.964006,68.964006,68.964006
-23,80.221991,68.964006,68.964006,68.964006
-24,72.658526,68.964006,68.964006,68.964006
-25,71.855393,68.964006,68.964006,68.964006
-26,82.627321,68.964006,68.964006,68.964006
-27,91.051617,68.964006,68.964006,68.964006
-28,87.400448,68.964006,68.964006,68.964006
-29,90.87753,68.964006,68.964006,68.964006
-30,93.458211,68.964006,68.964006,68.964006
-31,83.604526,68.964006,68.964006,68.964006
-32,92.505893,68.964006,68.964006,68.964006
-33,87.331698,68.964006,68.964006,68.964006
-34,98.325657,68.964006,68.964006,68.964006
-35,85.687817,68.964006,68.964006,68.964006
-36,87.550211,68.964006,68.964006,68.964006
-37,96.164056,68.964006,68.964006,68.964006
-38,99.407747,68.964006,68.964006,68.964006
-39,67.124815,68.964006,68.964006,68.964006
-40,67.676215,68.964006,68.964006,68.964006
-41,68.964006,68.964006,68.964006,68.964006
+0,71.689644,75.160494,75.160494,75.160494
+1,70.38942,75.160494,75.160494,75.160494
+2,97.902831,75.160494,75.160494,75.160494
+3,102.067008,75.160494,75.160494,75.160494
+4,87.57377,75.160494,75.160494,75.160494
+5,89.157016,75.160494,75.160494,75.160494
+6,83.965921,75.160494,75.160494,75.160494
+7,81.484967,75.160494,75.160494,75.160494
+8,92.168448,75.160494,75.160494,75.160494
+9,87.703365,75.160494,75.160494,75.160494
+10,91.604778,75.160494,75.160494,75.160494
+11,87.390073,75.160494,75.160494,75.160494
+12,76.383191,75.160494,75.160494,75.160494
+13,76.967794,75.160494,75.160494,75.160494
+14,80.476306,75.160494,75.160494,75.160494
+15,82.24915,75.160494,75.160494,75.160494
+16,79.099108,75.160494,75.160494,75.160494
+17,104.26692,75.160494,75.160494,75.160494
+18,78.086866,75.160494,75.160494,75.160494
+19,75.970493,75.160494,75.160494,75.160494
+20,82.311407,75.160494,75.160494,75.160494
+21,76.699738,75.160494,75.160494,75.160494
+22,82.53543,75.160494,75.160494,75.160494
+23,85.379258,75.160494,75.160494,75.160494
+24,76.479032,75.160494,75.160494,75.160494
+25,76.459996,75.160494,75.160494,75.160494
+26,87.185246,75.160494,75.160494,75.160494
+27,94.09772,75.160494,75.160494,75.160494
+28,92.29604,75.160494,75.160494,75.160494
+29,93.293152,75.160494,75.160494,75.160494
+30,96.145324,75.160494,75.160494,75.160494
+31,88.324015,75.160494,75.160494,75.160494
+32,94.832948,75.160494,75.160494,75.160494
+33,93.199326,75.160494,75.160494,75.160494
+34,100.530899,75.160494,75.160494,75.160494
+35,90.430068,75.160494,75.160494,75.160494
+36,90.500952,75.160494,75.160494,75.160494
+37,101.128157,75.160494,75.160494,75.160494
+38,101.85053,75.160494,75.160494,75.160494
+39,73.390183,75.160494,75.160494,75.160494
+40,74.503112,75.160494,75.160494,75.160494
+41,75.160494,75.160494,75.160494,75.160494

bv-evaluation/raw-data/bvw32_ch2_1DeMorgan_proved_data.csv

@@ -1,10 +1,10 @@
 ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-bb,leanSAT-sat,leanSAT-lrat-t,leanSAT-lrat-c
-0,74.852382,79.157458,13.186396,0.0,56.175826,1.455347,6.218676
-1,73.266689,79.6146,13.974813,0.0,56.146531,1.36704,6.149054
-2,10.695255,10.671971,10.66123,0.0,0.0,0.0,0.0
-3,76.881422,97.991299,19.896899,0.0,55.977201,6.086215,13.383457
-4,9.837144,9.811958,9.801628,0.0,0.0,0.0,0.0
-5,69.345351,84.211433,18.313351,0.0,55.617361,1.415702,6.800564
-6,70.159805,80.556507,16.641716,0.0,54.645719,1.476135,5.779026
-7,79.208353,111.266311,21.559116,0.0,55.784305,18.036749,13.460052
-8,80.023881,111.851597,22.179779,0.0,55.706639,18.611684,12.701591
+0,76.384173,83.679671,18.127277,0.0,54.86732,1.374974,7.157617
+1,71.237802,90.757546,20.795312,0.0,60.105856,1.382118,6.445021
+2,11.509629,11.211406,11.200245,0.0,0.0,0.0,0.0
+3,76.386407,95.312522,19.665691,0.0,54.03619,5.763066,13.460189
+4,10.292252,10.307752,10.295738,0.0,0.0,0.0,0.0
+5,68.008198,82.291089,18.314159,0.0,53.756113,1.366509,6.860747
+6,68.722374,83.24,16.858733,0.0,57.144437,1.428235,5.841564
+7,81.136761,97.401695,21.43025,0.0,53.295473,8.263875,12.008034
+8,76.094676,110.219243,21.213251,0.0,53.474601,18.094054,15.079957

bv-evaluation/raw-data/bvw32_ch2_2AdditionAndLogicalOps_proved_data.csv

@@ -1,23 +1,23 @@
 ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-bb,leanSAT-sat,leanSAT-lrat-t,leanSAT-lrat-c
-0,8.670172,7.78957,7.776335,0.0,0.0,0.0,0.0
-1,79.75753,87.334579,19.985167,0.0,55.716879,4.227558,5.355878
-2,10.106763,10.354451,10.342779,0.0,0.0,0.0,0.0
-3,7.467382,7.362904,7.351483,0.0,0.0,0.0,0.0
-4,9.728289,9.744421,9.734151,0.0,0.0,0.0,0.0
-5,80.45753,187.942519,27.886589,0.0,105.782925,25.15342,26.294512
-6,79.759154,133.545147,22.799286,3.425505,55.97719,22.064492,23.980797
-7,74.223616,91.883713,20.172049,0.0,56.429553,6.786227,6.499307
-8,84.639072,158.352966,26.930464,3.700424,55.753529,28.854625,37.248587
-9,85.233496,129.958458,24.901113,0.0,54.033783,26.284916,22.066725
-10,92.337821,265.235426,35.149825,3.759004,106.178291,51.704287,61.988205
-11,92.743876,190.860325,31.168301,0.0,106.249555,26.640216,23.817348
-12,91.5791,271.927246,40.918642,4.029184,106.157803,49.524484,64.546664
-13,81.979102,114.041832,32.573384,0.0,56.18579,7.455224,14.856856
-14,81.274522,110.708521,37.730987,0.0,56.071669,7.251074,7.383403
-15,80.09112,101.862977,21.976324,0.0,54.14765,11.596793,11.447117
-16,89.087438,362.377996,33.146684,0.0,206.496333,59.090377,59.925964
-17,80.835353,112.612383,23.126224,0.0,56.479538,17.554828,12.672857
-18,86.380468,133.829795,29.2496,0.0,55.747748,23.725265,21.714941
-19,75.346295,82.265973,18.261262,0.0,56.147422,1.82262,4.097681
-20,74.020984,86.501388,18.856305,0.0,56.089142,2.727086,6.850197
-21,80.23449,114.94779,29.018755,0.0,56.589646,8.666205,17.748134
+0,8.697162,7.664523,7.650076,0.0,0.0,0.0,0.0
+1,83.308089,100.207901,28.09638,0.0,60.57479,4.105458,5.458199
+2,9.950386,10.250144,10.239113,0.0,0.0,0.0,0.0
+3,7.136397,7.26997,7.259289,0.0,0.0,0.0,0.0
+4,9.708501,10.060905,10.050386,0.0,0.0,0.0,0.0
+5,85.185703,187.905372,25.047237,0.0,110.357694,22.787332,27.140505
+6,81.423281,132.496882,21.281941,3.377484,59.936715,20.308574,22.406362
+7,78.463607,90.980197,17.798638,0.0,60.095013,5.14542,6.070786
+8,89.276571,166.685408,26.316582,3.572452,60.432922,35.742919,34.94302
+9,86.745145,184.064516,30.384066,0.0,110.456444,19.00317,21.407858
+10,96.175419,280.713429,41.610964,3.736021,110.848099,61.54498,56.649724
+11,93.341192,146.90978,30.722857,0.0,61.111453,28.941886,22.85515
+12,96.862568,269.878601,39.743049,3.856909,111.424936,48.605862,59.44099
+13,85.604632,103.088245,23.159814,0.0,61.182135,7.641269,8.815646
+14,85.489766,102.829166,21.952486,0.0,61.489766,7.306748,9.46517
+15,84.925782,112.184731,22.040241,0.0,61.422118,11.719947,14.200478
+16,93.186411,357.122877,29.870918,0.0,211.679824,58.084931,54.193407
+17,84.238004,116.862419,23.015493,0.0,61.532457,17.480035,12.334435
+18,91.149316,133.547775,27.688681,0.0,61.420205,23.029057,18.392508
+19,80.407777,96.662789,22.366677,0.0,61.534801,1.948967,8.315961
+20,79.174317,95.638257,14.667418,0.0,61.636425,4.871583,12.179124
+21,83.774139,111.377077,25.067724,0.0,61.699361,8.562168,13.309808

bv-evaluation/raw-data/bvw32_ch2_3LogicalArithmeticIneq_ceg_data.csv

@@ -1,43 +1,43 @@
 ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-sat
-0,69.112455,71.859619,71.859619,71.859619
-1,67.032781,71.859619,71.859619,71.859619
-2,95.977914,71.859619,71.859619,71.859619
-3,101.204479,71.859619,71.859619,71.859619
-4,83.669478,71.859619,71.859619,71.859619
-5,85.576565,71.859619,71.859619,71.859619
-6,82.237323,71.859619,71.859619,71.859619
-7,78.575414,71.859619,71.859619,71.859619
-8,89.35144,71.859619,71.859619,71.859619
-9,84.797505,71.859619,71.859619,71.859619
-10,88.611963,71.859619,71.859619,71.859619
-11,84.636571,71.859619,71.859619,71.859619
-12,73.175653,71.859619,71.859619,71.859619
-13,73.546854,71.859619,71.859619,71.859619
-14,78.022931,71.859619,71.859619,71.859619
-15,79.81887,71.859619,71.859619,71.859619
-16,74.592868,71.859619,71.859619,71.859619
-17,100.371336,71.859619,71.859619,71.859619
-18,67.312838,71.859619,71.859619,71.859619
-19,68.83954,71.859619,71.859619,71.859619
-20,77.851756,71.859619,71.859619,71.859619
-21,68.671553,71.859619,71.859619,71.859619
-22,80.812285,71.859619,71.859619,71.859619
-23,80.323141,71.859619,71.859619,71.859619
-24,71.178574,71.859619,71.859619,71.859619
-25,72.198991,71.859619,71.859619,71.859619
-26,81.768599,71.859619,71.859619,71.859619
-27,90.033245,71.859619,71.859619,71.859619
-28,88.809476,71.859619,71.859619,71.859619
-29,89.310251,71.859619,71.859619,71.859619
-30,96.601401,71.859619,71.859619,71.859619
-31,83.276906,71.859619,71.859619,71.859619
-32,91.439218,71.859619,71.859619,71.859619
-33,89.884054,71.859619,71.859619,71.859619
-34,97.310979,71.859619,71.859619,71.859619
-35,86.862823,71.859619,71.859619,71.859619
-36,88.903092,71.859619,71.859619,71.859619
-37,99.188273,71.859619,71.859619,71.859619
-38,101.672108,71.859619,71.859619,71.859619
-39,70.73617,71.859619,71.859619,71.859619
-40,71.332794,71.859619,71.859619,71.859619
-41,71.859619,71.859619,71.859619,71.859619
+0,71.035048,74.92517,74.92517,74.92517
+1,70.471054,74.92517,74.92517,74.92517
+2,98.504036,74.92517,74.92517,74.92517
+3,102.935909,74.92517,74.92517,74.92517
+4,87.681793,74.92517,74.92517,74.92517
+5,89.749614,74.92517,74.92517,74.92517
+6,84.6381,74.92517,74.92517,74.92517
+7,82.441484,74.92517,74.92517,74.92517
+8,92.198797,74.92517,74.92517,74.92517
+9,88.721676,74.92517,74.92517,74.92517
+10,92.0633,74.92517,74.92517,74.92517
+11,87.993781,74.92517,74.92517,74.92517
+12,77.402663,74.92517,74.92517,74.92517
+13,77.052916,74.92517,74.92517,74.92517
+14,80.784025,74.92517,74.92517,74.92517
+15,85.131971,74.92517,74.92517,74.92517
+16,79.300068,74.92517,74.92517,74.92517
+17,104.251231,74.92517,74.92517,74.92517
+18,79.077375,74.92517,74.92517,74.92517
+19,77.881528,74.92517,74.92517,74.92517
+20,83.101249,74.92517,74.92517,74.92517
+21,77.534894,74.92517,74.92517,74.92517
+22,83.822319,74.92517,74.92517,74.92517
+23,86.512215,74.92517,74.92517,74.92517
+24,77.916765,74.92517,74.92517,74.92517
+25,77.906035,74.92517,74.92517,74.92517
+26,88.51741,74.92517,74.92517,74.92517
+27,95.162851,74.92517,74.92517,74.92517
+28,93.03342,74.92517,74.92517,74.92517
+29,94.2672,74.92517,74.92517,74.92517
+30,96.95931,74.92517,74.92517,74.92517
+31,89.295278,74.92517,74.92517,74.92517
+32,96.098446,74.92517,74.92517,74.92517
+33,93.987562,74.92517,74.92517,74.92517
+34,101.595968,74.92517,74.92517,74.92517
+35,90.735936,74.92517,74.92517,74.92517
+36,92.235125,74.92517,74.92517,74.92517
+37,102.398965,74.92517,74.92517,74.92517
+38,102.713808,74.92517,74.92517,74.92517
+39,74.508494,74.92517,74.92517,74.92517
+40,76.054321,74.92517,74.92517,74.92517
+41,74.92517,74.92517,74.92517,74.92517

bv-evaluation/raw-data/bvw4_ch2_1DeMorgan_proved_data.csv

@@ -1,10 +1,10 @@
 ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-bb,leanSAT-sat,leanSAT-lrat-t,leanSAT-lrat-c
-0,74.461205,73.197468,12.692883,0.0,53.914048,0.0,3.718748
-1,69.419551,77.738157,18.062958,0.0,53.770716,0.0,3.227462
-2,10.706354,10.488705,10.478475,0.0,0.0,0.0,0.0
-3,74.149025,79.960994,18.765715,0.0,53.392925,0.0,5.492936
-4,9.766822,10.257989,10.247508,0.0,0.0,0.0,0.0
-5,70.369092,72.787695,11.639977,0.0,55.357381,0.0,3.060986
-6,67.821773,75.910159,16.738419,0.0,54.489584,0.0,1.996798
-7,79.294185,88.018779,23.692803,0.0,53.700014,2.147492,6.924257
-8,80.050421,81.635464,21.402421,0.0,53.348422,2.011636,3.949815
+0,77.698052,79.192392,12.773354,0.0,60.105394,0.0,3.79779
+1,76.015272,78.633615,13.680425,0.0,59.456348,0.0,3.153842
+2,10.618583,10.45503,10.443889,0.0,0.0,0.0,0.0
+3,81.124809,86.510744,18.670191,0.0,60.252653,0.0,5.396835
+4,9.789224,9.813289,9.801748,0.0,0.0,0.0,0.0
+5,73.206736,77.071451,11.380606,0.0,59.792914,0.0,3.045728
+6,73.05502,78.422029,13.905241,0.0,59.807612,0.0,2.022257
+7,82.849855,92.494374,21.428277,0.0,60.396342,2.180786,6.944975
+8,84.311441,95.958152,25.252343,0.0,60.244857,2.080065,6.812766