Benchmark

LabelMeaning
SSolution {OPTIMUM FOUND or OPT | UNSATISFIABLE or UNSAT | UNKNOWN | Not available or N/A}
OBest solution found
TCPU time (TO for Time Out)
(out)(err)Standard output and standard error for each solver

ColorMeaning for Complete SolversMeaning for Incomplete Solvers
TextBest solver columnBest solver column
TextOptimal solution with the best CPU timeBest solution with the best CPU time
TextOptimal solution and finished within the Time OutBest solution without the best CPU time
TextOptimal solution and did not finish within the Time OutSolution found but not the best
TextTime OutTime Out
TextBuggy solutionBuggy solution

Instance file name Best solver ISAC+-2016-co
CSG140-140-46.wcnf S = OPT
O = 16960
T = 22.03		 S = OPT
O = 16960
T = 22.03
CSG140-140-6.wcnf S = OPT
O = 52385
T = 38.12		 S = OPT
O = 52385
T = 38.12
CSG150-150-55.wcnf S = OPT
O = 27533
T = 32.40		 S = OPT
O = 27533
T = 32.40
CSG40-40-95.wcnf S = OPT
O = 8847
T = 6.47		 S = OPT
O = 8847
T = 6.47
CSG60-60-88.wcnf S = OPT
O = 7714
T = 6.64		 S = OPT
O = 7714
T = 6.64
CSGNaive140-140-0.wcnf S = OPT
O = 18185
T = 22.55		 S = OPT
O = 18185
T = 22.55
CSGNaive140-140-6.wcnf S = OPT
O = 56309
T = 40.15		 S = OPT
O = 56309
T = 40.15
CSGNaive150-150-55.wcnf S = OPT
O = 30495
T = 33.71		 S = OPT
O = 30495
T = 33.71
CSGNaive60-60-53.wcnf S = OPT
O = 9829
T = 6.70		 S = OPT
O = 9829
T = 6.70
CSGNaive70-70-91.wcnf S = OPT
O = 11177
T = 6.72		 S = OPT
O = 11177
T = 6.72
cat_paths_60_130_0000.txt.wcnf S = OPT
O = 78708
T = 6.38		 S = OPT
O = 78708
T = 6.38
cat_paths_60_130_0001.txt.wcnf S = OPT
O = 80743
T = 6.43		 S = OPT
O = 80743
T = 6.43
cat_paths_60_130_0002.txt.wcnf S = OPT
O = 71385
T = 6.46		 S = OPT
O = 71385
T = 6.46
cat_paths_60_130_0003.txt.wcnf S = OPT
O = 86981
T = 6.40		 S = OPT
O = 86981
T = 6.40
cat_paths_60_140_0000.txt.wcnf S = OPT
O = 98394
T = 6.42		 S = OPT
O = 98394
T = 6.42
cat_paths_60_140_0001.txt.wcnf S = OPT
O = 97718
T = 6.42		 S = OPT
O = 97718
T = 6.42
cat_paths_60_140_0002.txt.wcnf S = OPT
O = 92818
T = 6.43		 S = OPT
O = 92818
T = 6.43
cat_paths_60_140_0003.txt.wcnf S = OPT
O = 92696
T = 6.43		 S = OPT
O = 92696
T = 6.43
cat_paths_60_150_0000.txt.wcnf S = OPT
O = 82179
T = 6.46		 S = OPT
O = 82179
T = 6.46
cat_paths_60_150_0001.txt.wcnf S = OPT
O = 92299
T = 6.45		 S = OPT
O = 92299
T = 6.45
cat_paths_60_150_0002.txt.wcnf S = OPT
O = 101547
T = 6.37		 S = OPT
O = 101547
T = 6.37
cat_paths_60_150_0003.txt.wcnf S = OPT
O = 106294
T = 6.39		 S = OPT
O = 106294
T = 6.39
cat_paths_60_160_0000.txt.wcnf S = OPT
O = 104199
T = 6.42		 S = OPT
O = 104199
T = 6.42
cat_paths_60_160_0001.txt.wcnf S = OPT
O = 99297
T = 6.40		 S = OPT
O = 99297
T = 6.40
cat_paths_60_160_0002.txt.wcnf S = OPT
O = 102352
T = 6.41		 S = OPT
O = 102352
T = 6.41
cat_paths_60_160_0003.txt.wcnf S = OPT
O = 107262
T = 6.47		 S = OPT
O = 107262
T = 6.47
cat_paths_60_170_0000.txt.wcnf S = OPT
O = 122170
T = 6.41		 S = OPT
O = 122170
T = 6.41
cat_paths_60_170_0003.txt.wcnf S = OPT
O = 122748
T = 6.38		 S = OPT
O = 122748
T = 6.38
cat_paths_60_170_0004.txt.wcnf S = OPT
O = 99105
T = 6.39		 S = OPT
O = 99105
T = 6.39
cat_paths_60_170_0005.txt.wcnf S = OPT
O = 114493
T = 6.42		 S = OPT
O = 114493
T = 6.42
cat_sched_60_160_0000.txt.wcnf S = OPT
O = 42672
T = 6.40		 S = OPT
O = 42672
T = 6.40
cat_sched_60_160_0001.txt.wcnf S = OPT
O = 72012
T = 6.41		 S = OPT
O = 72012
T = 6.41
cat_sched_60_160_0002.txt.wcnf S = OPT
O = 173386
T = 6.48		 S = OPT
O = 173386
T = 6.48
cat_sched_60_160_0003.txt.wcnf S = OPT
O = 118883
T = 6.48		 S = OPT
O = 118883
T = 6.48
cat_sched_60_170_0000.txt.wcnf S = OPT
O = 128737
T = 6.47		 S = OPT
O = 128737
T = 6.47
cat_sched_60_170_0001.txt.wcnf S = OPT
O = 62218
T = 6.48		 S = OPT
O = 62218
T = 6.48
cat_sched_60_170_0002.txt.wcnf S = OPT
O = 64664
T = 6.50		 S = OPT
O = 64664
T = 6.50
cat_sched_60_170_0003.txt.wcnf S = OPT
O = 169415
T = 6.46		 S = OPT
O = 169415
T = 6.46
cat_sched_60_180_0000.txt.wcnf S = OPT
O = 112247
T = 6.41		 S = OPT
O = 112247
T = 6.41
cat_sched_60_180_0001.txt.wcnf S = OPT
O = 154599
T = 6.46		 S = OPT
O = 154599
T = 6.46
cat_sched_60_180_0002.txt.wcnf S = OPT
O = 95338
T = 6.45		 S = OPT
O = 95338
T = 6.45
cat_sched_60_180_0003.txt.wcnf S = OPT
O = 104416
T = 6.42		 S = OPT
O = 104416
T = 6.42
cat_sched_60_190_0000.txt.wcnf S = OPT
O = 152878
T = 6.46		 S = OPT
O = 152878
T = 6.46
cat_sched_60_190_0001.txt.wcnf S = OPT
O = 71645
T = 6.45		 S = OPT
O = 71645
T = 6.45
cat_sched_60_190_0002.txt.wcnf S = OPT
O = 90463
T = 6.51		 S = OPT
O = 90463
T = 6.51
cat_sched_60_190_0003.txt.wcnf S = OPT
O = 87812
T = 6.44		 S = OPT
O = 87812
T = 6.44
cat_sched_60_200_0000.txt.wcnf S = OPT
O = 242832
T = 6.48		 S = OPT
O = 242832
T = 6.48
cat_sched_60_200_0001.txt.wcnf S = OPT
O = 46823
T = 6.41		 S = OPT
O = 46823
T = 6.41
cat_sched_60_200_0002.txt.wcnf S = OPT
O = 145851
T = 6.44		 S = OPT
O = 145851
T = 6.44
cat_sched_60_200_0003.txt.wcnf S = OPT
O = 187411
T = 6.43		 S = OPT
O = 187411
T = 6.43
causal_n5_i10_N1000_uai13_log_int.wcnf S = OPT
O = 75755143
T = 20.91		 S = OPT
O = 75755143
T = 20.91
causal_n5_i10_N500_uai13_log_int.wcnf S = OPT
O = 75755143
T = 15.04		 S = OPT
O = 75755143
T = 15.04
causal_n5_i5_N10000_uai13_log_int.wcnf S = OPT
O = 46030289
T = 23.64		 S = OPT
O = 46030289
T = 23.64
causal_n5_i5_N1000_uai13_log_int.wcnf S = OPT
O = 46030289
T = 16.60		 S = OPT
O = 46030289
T = 16.60
causal_n5_i5_N500_uai13_log_int.wcnf S = OPT
O = 46030289
T = 21.08		 S = OPT
O = 46030289
T = 21.08
causal_n5_i9_N10000_uai13_log_int.wcnf S = OPT
O = 127884075
T = 31.38		 S = OPT
O = 127884075
T = 31.38
causal_n5_i9_N1000_uai13_log_int.wcnf S = OPT
O = 127884075
T = 37.85		 S = OPT
O = 127884075
T = 37.85
causal_n6_i10_N500_uai13_log_int.wcnf S = OPT
O = 183312821
T = 240.82		 S = OPT
O = 183312821
T = 240.82
causal_n6_i10_N500_uai14_log_int.wcnf S = OPT
O = 183312821
T = 14.62		 S = OPT
O = 183312821
T = 14.62
causal_n6_i1_N10000_uai14_log_int.wcnf S = OPT
O = 1510725680
T = 12.90		 S = OPT
O = 1510725680
T = 12.90
causal_n6_i2_N1000_uai13_log_int.wcnf S = OPT
O = 877436991
T = 100.05		 S = OPT
O = 877436991
T = 100.05
causal_n6_i2_N500_uai13_log_int.wcnf S = OPT
O = 877436991
T = 139.72		 S = OPT
O = 877436991
T = 139.72
causal_n6_i3_N10000_uai13_log_int.wcnf S = OPT
O = 10860281582
T = 56.40		 S = OPT
O = 10860281582
T = 56.40
causal_n6_i5_N10000_uai13_log_int.wcnf S = OPT
O = 355929820
T = 42.88		 S = OPT
O = 355929820
T = 42.88
causal_n6_i5_N1000_uai13_log_int.wcnf S = OPT
O = 355929820
T = 45.39		 S = OPT
O = 355929820
T = 45.39
causal_n6_i5_N500_uai13_log_int.wcnf S = OPT
O = 355929820
T = 36.45		 S = OPT
O = 355929820
T = 36.45
causal_n6_i6_N1000_uai14_log_int.wcnf S = OPT
O = 126257527700
T = 14.54		 S = OPT
O = 126257527700
T = 14.54
causal_n6_i7_N1000_uai14_log_int.wcnf S = OPT
O = 1633212419
T = 19.15		 S = OPT
O = 1633212419
T = 19.15
causal_n6_i8_N1000_uai14_log_int.wcnf S = OPT
O = 19596713347
T = 16.59		 S = OPT
O = 19596713347
T = 16.59
causal_n6_i9_N10000_uai14_log_int.wcnf S = OPT
O = 1913093684
T = 14.72		 S = OPT
O = 1913093684
T = 14.72
causal_n7_i10_N10000_uai14_log_int.wcnf S = OPT
O = 3246397504
T = 21.30		 S = OPT
O = 3246397504
T = 21.30
causal_n7_i10_N1000_uai14_log_int.wcnf S = OPT
O = 3246397504
T = 20.12		 S = OPT
O = 3246397504
T = 20.12
causal_n7_i10_N500_uai14_log_int.wcnf S = OPT
O = 3246397504
T = 20.51		 S = OPT
O = 3246397504
T = 20.51
causal_n7_i4_N10000_uai14_log_int.wcnf S = OPT
O = 37532020924
T = 116.64		 S = OPT
O = 37532020924
T = 116.64
causal_n7_i4_N1000_uai14_log_int.wcnf S = OPT
O = 37532020924
T = 105.81		 S = OPT
O = 37532020924
T = 105.81
causal_n7_i4_N500_uai14_log_int.wcnf S = OPT
O = 37532020924
T = 72.31		 S = OPT
O = 37532020924
T = 72.31
causal_n7_i5_N10000_uai14_log_int.wcnf S = OPT
O = 20711646820
T = 15.22		 S = OPT
O = 20711646820
T = 15.22
causal_n7_i5_N1000_uai14_log_int.wcnf S = OPT
O = 20711646820
T = 14.79		 S = OPT
O = 20711646820
T = 14.79
causal_n7_i5_N500_uai14_log_int.wcnf S = OPT
O = 20711646820
T = 13.19		 S = OPT
O = 20711646820
T = 13.19
causal_n7_i8_N10000_uai14_log_int.wcnf S = OPT
O = 11486104693
T = 9.57		 S = OPT
O = 11486104693
T = 9.57
causal_n7_i8_N1000_uai14_log_int.wcnf S = OPT
O = 11486104693
T = 9.78		 S = OPT
O = 11486104693
T = 9.78
causal_n7_i8_N500_uai14_log_int.wcnf S = OPT
O = 11486104693
T = 10.57		 S = OPT
O = 11486104693
T = 10.57
causal_n7_i9_N10000_uai14_log_int.wcnf S = OPT
O = 43638470640
T = 197.79		 S = OPT
O = 43638470640
T = 197.79
causal_n7_i9_N1000_uai14_log_int.wcnf S = OPT
O = 43638470640
T = 172.31		 S = OPT
O = 43638470640
T = 172.31
causal_n7_i9_N500_uai14_log_int.wcnf S = OPT
O = 43638470640
T = 208.12		 S = OPT
O = 43638470640
T = 208.12
frb10-6-1.wcnf S = OPT
O = 50
T = 6.38		 S = OPT
O = 50
T = 6.38
frb10-6-2.wcnf S = OPT
O = 50
T = 6.24		 S = OPT
O = 50
T = 6.24
frb10-6-3.wcnf S = OPT
O = 50
T = 6.44		 S = OPT
O = 50
T = 6.44
frb10-6-4.wcnf S = OPT
O = 50
T = 6.41		 S = OPT
O = 50
T = 6.41
frb15-9-1.wcnf S = OPT
O = 120
T = 6.40		 S = OPT
O = 120
T = 6.40
frb15-9-2.wcnf S = OPT
O = 120
T = 6.44		 S = OPT
O = 120
T = 6.44
frb15-9-3.wcnf S = OPT
O = 120
T = 6.49		 S = OPT
O = 120
T = 6.49
frb15-9-4.wcnf S = OPT
O = 120
T = 6.46		 S = OPT
O = 120
T = 6.46
frb15-9-5.wcnf S = OPT
O = 120
T = 6.57		 S = OPT
O = 120
T = 6.57
frb20-11-1.wcnf S = OPT
O = 200
T = 6.49		 S = OPT
O = 200
T = 6.49
frb20-11-2.wcnf S = OPT
O = 200
T = 6.50		 S = OPT
O = 200
T = 6.50
frb20-11-3.wcnf S = OPT
O = 200
T = 6.60		 S = OPT
O = 200
T = 6.60
frb20-11-4.wcnf S = OPT
O = 200
T = 6.55		 S = OPT
O = 200
T = 6.55
frb20-11-5.wcnf S = OPT
O = 200
T = 6.44		 S = OPT
O = 200
T = 6.44
frb25-13-1.wcnf S = OPT
O = 300
T = 9.85		 S = OPT
O = 300
T = 9.85
frb25-13-2.wcnf S = OPT
O = 300
T = 7.32		 S = OPT
O = 300
T = 7.32
frb25-13-3.wcnf S = OPT
O = 300
T = 8.08		 S = OPT
O = 300
T = 8.08
frb25-13-4.wcnf S = OPT
O = 300
T = 7.66		 S = OPT
O = 300
T = 7.66
frb25-13-5.wcnf S = OPT
O = 300
T = 7.62		 S = OPT
O = 300
T = 7.62
frb30-15-1.wcnf S = OPT
O = 420
T = 11.30		 S = OPT
O = 420
T = 11.30
frb30-15-2.wcnf S = OPT
O = 420
T = 9.40		 S = OPT
O = 420
T = 9.40
frb30-15-3.wcnf S = OPT
O = 420
T = 9.89		 S = OPT
O = 420
T = 9.89
frb30-15-4.wcnf S = OPT
O = 420
T = 11.04		 S = OPT
O = 420
T = 11.04
frb30-15-5.wcnf S = OPT
O = 420
T = 11.34		 S = OPT
O = 420
T = 11.34
frb35-17-1.wcnf S = OPT
O = 560
T = 40.03		 S = OPT
O = 560
T = 40.03
frb35-17-2.wcnf S = OPT
O = 560
T = 36.18		 S = OPT
O = 560
T = 36.18
frb35-17-3.wcnf S = OPT
O = 560
T = 17.44		 S = OPT
O = 560
T = 17.44
frb35-17-4.wcnf S = OPT
O = 560
T = 21.16		 S = OPT
O = 560
T = 21.16
frb35-17-5.wcnf S = OPT
O = 560
T = 48.97		 S = OPT
O = 560
T = 48.97
frb40-19-1.wcnf S = OPT
O = 720
T = 21.17		 S = OPT
O = 720
T = 21.17
frb40-19-2.wcnf S = OPT
O = 720
T = 37.43		 S = OPT
O = 720
T = 37.43
frb40-19-3.wcnf S = OPT
O = 720
T = 190.35		 S = OPT
O = 720
T = 190.35
frb40-19-4.wcnf S = OPT
O = 720
T = 614.33		 S = OPT
O = 720
T = 614.33
frb40-19-5.wcnf S = OPT
O = 720
T = 261.62		 S = OPT
O = 720
T = 261.62
driverlog02bc.wcsp.wcnf S = OPT
O = 2085
T = 6.58		 S = OPT
O = 2085
T = 6.58
driverlog02c.wcsp.wcnf S = OPT
O = 2010
T = 6.55		 S = OPT
O = 2010
T = 6.55
driverlog02cc.wcsp.wcnf S = OPT
O = 2428
T = 6.60		 S = OPT
O = 2428
T = 6.60
driverlog04ac.wcsp.wcnf S = OPT
O = 1790
T = 6.47		 S = OPT
O = 1790
T = 6.47
driverlog04bc.wcsp.wcnf S = OPT
O = 1921
T = 6.55		 S = OPT
O = 1921
T = 6.55
driverlog04cc.wcsp.wcnf S = OPT
O = 2932
T = 6.53		 S = OPT
O = 2932
T = 6.53
driverlog05ac.wcsp.wcnf S = OPT
O = 1350
T = 6.65		 S = OPT
O = 1350
T = 6.65
driverlog05bc.wcsp.wcnf S = OPT
O = 1344
T = 6.71		 S = OPT
O = 1344
T = 6.71
driverlog05c.wcsp.wcnf S = OPT
O = 1350
T = 6.65		 S = OPT
O = 1350
T = 6.65
driverlog08ac.wcsp.wcnf S = OPT
O = 2220
T = 6.98		 S = OPT
O = 2220
T = 6.98
driverlog08c.wcsp.wcnf S = OPT
O = 2220
T = 6.90		 S = OPT
O = 2220
T = 6.90
driverlog08cc.wcsp.wcnf S = OPT
O = 4052
T = 7.09		 S = OPT
O = 4052
T = 7.09
driverlog09.wcsp.wcnf S = OPT
O = 960
T = 6.81		 S = OPT
O = 960
T = 6.81
driverlogs03.wcsp.wcnf S = OPT
O = 1225
T = 6.41		 S = OPT
O = 1225
T = 6.41
driverlogs06.wcsp.wcnf S = OPT
O = 1055
T = 6.44		 S = OPT
O = 1055
T = 6.44
logistics01bc.wcsp.wcnf S = OPT
O = 8035
T = 6.38		 S = OPT
O = 8035
T = 6.38
logistics01c.wcsp.wcnf S = OPT
O = 8865
T = 6.41		 S = OPT
O = 8865
T = 6.41
logistics01cc.wcsp.wcnf S = OPT
O = 4282
T = 6.38		 S = OPT
O = 4282
T = 6.38
satellite01ac.wcsp.wcnf S = OPT
O = 1530
T = 6.41		 S = OPT
O = 1530
T = 6.41
satellite01bc.wcsp.wcnf S = OPT
O = 1827
T = 6.41		 S = OPT
O = 1827
T = 6.41
satellite01cc.wcsp.wcnf S = OPT
O = 1530
T = 6.45		 S = OPT
O = 1530
T = 6.45
satellite02ac.wcsp.wcnf S = OPT
O = 1611
T = 7.08		 S = OPT
O = 1611
T = 7.08
satellite02bc.wcsp.wcnf S = OPT
O = 2289
T = 6.94		 S = OPT
O = 2289
T = 6.94
zenotravel02ac.wcsp.wcnf S = OPT
O = 2485
T = 6.41		 S = OPT
O = 2485
T = 6.41
zenotravel02bc.wcsp.wcnf S = OPT
O = 2335
T = 6.41		 S = OPT
O = 2335
T = 6.41
zenotravel02c.wcsp.wcnf S = OPT
O = 2485
T = 6.38		 S = OPT
O = 2485
T = 6.38
zenotravel02cc.wcsp.wcnf S = OPT
O = 742
T = 6.42		 S = OPT
O = 742
T = 6.42
zenotravel04bc.wcsp.wcnf S = OPT
O = 4110
T = 6.47		 S = OPT
O = 4110
T = 6.47
zenotravel04c.wcsp.wcnf S = OPT
O = 4270
T = 6.45		 S = OPT
O = 4270
T = 6.45
zenotravel04cc.wcsp.wcnf S = OPT
O = 1599
T = 6.43		 S = OPT
O = 1599
T = 6.43
cap101.wcsp.wcnf S = OPT
O = 7966472
T = 6.61		 S = OPT
O = 7966472
T = 6.61
cap102.wcsp.wcnf S = OPT
O = 8547029
T = 6.61		 S = OPT
O = 8547029
T = 6.61
cap111.wcsp.wcnf S = OPT
O = 7934385
T = 7.25		 S = OPT
O = 7934385
T = 7.25
cap112.wcsp.wcnf S = OPT
O = 8514942
T = 7.19		 S = OPT
O = 8514942
T = 7.19
cap121.wcsp.wcnf S = OPT
O = 7934385
T = 7.24		 S = OPT
O = 7934385
T = 7.24
cap122.wcsp.wcnf S = OPT
O = 8514942
T = 7.22		 S = OPT
O = 8514942
T = 7.22
cap131.wcsp.wcnf S = OPT
O = 7934385
T = 7.26		 S = OPT
O = 7934385
T = 7.26
cap132.wcsp.wcnf S = OPT
O = 8514942
T = 7.17		 S = OPT
O = 8514942
T = 7.17
cap61.wcsp.wcnf S = OPT
O = 9326144
T = 6.53		 S = OPT
O = 9326144
T = 6.53
cap62.wcsp.wcnf S = OPT
O = 9777981
T = 6.50		 S = OPT
O = 9777981
T = 6.50
cap71.wcsp.wcnf S = OPT
O = 9326144
T = 6.48		 S = OPT
O = 9326144
T = 6.48
cap72.wcsp.wcnf S = OPT
O = 9777981
T = 6.46		 S = OPT
O = 9777981
T = 6.46
cap81.wcsp.wcnf S = OPT
O = 7966472
T = 6.61		 S = OPT
O = 7966472
T = 6.61
cap82.wcsp.wcnf S = OPT
O = 8547029
T = 6.60		 S = OPT
O = 8547029
T = 6.60
cap91.wcsp.wcnf S = OPT
O = 7966472
T = 6.63		 S = OPT
O = 7966472
T = 6.63
cap92.wcsp.wcnf S = OPT
O = 8547029
T = 6.56		 S = OPT
O = 8547029
T = 6.56
warehouse0.wcsp.wcnf S = OPT
O = 328
T = 6.33		 S = OPT
O = 328
T = 6.33
warehouse1.wcsp.wcnf S = OPT
O = 730567
T = 6.42		 S = OPT
O = 730567
T = 6.42
normalized-mps-v2-20-10-bm23.opb.msat.wcnf S = OPT
O = 34
T = 11.66		 S = OPT
O = 34
T = 11.66
normalized-mps-v2-20-10-cracpb1.opb.msat.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-mps-v2-20-10-l152lav.opb.msat.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-mps-v2-20-10-lp4l.opb.msat.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-mps-v2-20-10-lseu.opb.msat.wcnf S = OPT
O = 1120
T = 48.03		 S = OPT
O = 1120
T = 48.03
normalized-mps-v2-20-10-mod008.opb.msat.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-mps-v2-20-10-mod010.opb.msat.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-mps-v2-20-10-p0033.opb.msat.wcnf S = OPT
O = 3089
T = 6.38		 S = OPT
O = 3089
T = 6.38
normalized-mps-v2-20-10-p0040.opb.msat.wcnf S = OPT
O = 62027
T = 6.41		 S = OPT
O = 62027
T = 6.41
normalized-mps-v2-20-10-p0201.opb.msat.wcnf S = OPT
O = 1523
T = 15.46		 S = OPT
O = 1523
T = 15.46
normalized-mps-v2-20-10-p0548.opb.msat.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-mps-v2-20-10-sentoy.opb.msat.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
ram_k3_n10.ra1.wcnf S = OPT
O = 232
T = 9.90		 S = OPT
O = 232
T = 9.90
ram_k3_n11.ra1.wcnf S = OPT
O = 318
T = 28.48		 S = OPT
O = 318
T = 28.48
ram_k3_n12.ra1.wcnf S = OPT
O = 524
T = 152.46		 S = OPT
O = 524
T = 152.46
ram_k3_n13.ra1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
ram_k3_n14.ra1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
ram_k3_n15.ra1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
ram_k3_n16.ra1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
ram_k3_n17.ra1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
ram_k3_n18.ra1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
ram_k3_n19.ra1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
ram_k3_n20.ra1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
ram_k3_n9.ra1.wcnf S = OPT
O = 7
T = 6.80		 S = OPT
O = 7
T = 6.80
ram_k4_n18.ra1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
ram_k4_n19.ra1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
ram_k4_n20.ra1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
random-net-200-1_network-1.net.wcnf S = OPT
O = 172132
T = 6.93		 S = OPT
O = 172132
T = 6.93
random-net-200-1_network-3.net.wcnf S = OPT
O = 187891
T = 7.62		 S = OPT
O = 187891
T = 7.62
random-net-200-1_network-4.net.wcnf S = OPT
O = 202191
T = 7.57		 S = OPT
O = 202191
T = 7.57
random-net-240-1_network-1.net.wcnf S = OPT
O = 224300
T = 7.43		 S = OPT
O = 224300
T = 7.43
random-net-240-1_network-2.net.wcnf S = OPT
O = 220878
T = 7.48		 S = OPT
O = 220878
T = 7.48
random-net-240-1_network-3.net.wcnf S = OPT
O = 213755
T = 7.45		 S = OPT
O = 213755
T = 7.45
random-net-240-1_network-4.net.wcnf S = OPT
O = 231994
T = 8.15		 S = OPT
O = 231994
T = 8.15
random-net-240-1_network-5.net.wcnf S = OPT
O = 227363
T = 7.73		 S = OPT
O = 227363
T = 7.73
random-net-280-1_network-2.net.wcnf S = OPT
O = 263706
T = 7.82		 S = OPT
O = 263706
T = 7.82
random-net-280-1_network-3.net.wcnf S = OPT
O = 257943
T = 8.07		 S = OPT
O = 257943
T = 8.07
random-net-280-1_network-4.net.wcnf S = OPT
O = 251789
T = 7.34		 S = OPT
O = 251789
T = 7.34
random-net-280-1_network-5.net.wcnf S = OPT
O = 254206
T = 7.77		 S = OPT
O = 254206
T = 7.77
random-net-300-1_network-1.net.wcnf S = OPT
O = 285555
T = 8.15		 S = OPT
O = 285555
T = 8.15
random-net-300-1_network-2.net.wcnf S = OPT
O = 293088
T = 7.51		 S = OPT
O = 293088
T = 7.51
random-net-300-1_network-3.net.wcnf S = OPT
O = 271896
T = 7.78		 S = OPT
O = 271896
T = 7.78
random-net-300-1_network-4.net.wcnf S = OPT
O = 284120
T = 7.64		 S = OPT
O = 284120
T = 7.64
random-net-300-1_network-5.net.wcnf S = OPT
O = 267307
T = 7.55		 S = OPT
O = 267307
T = 7.55
random-net-50-2_network-1.net.wcnf S = OPT
O = 48636
T = 8.49		 S = OPT
O = 48636
T = 8.49
random-net-50-2_network-2.net.wcnf S = OPT
O = 43675
T = 9.66		 S = OPT
O = 43675
T = 9.66
random-net-50-2_network-3.net.wcnf S = OPT
O = 46924
T = 8.63		 S = OPT
O = 46924
T = 8.63
random-net-50-2_network-4.net.wcnf S = OPT
O = 45279
T = 7.12		 S = OPT
O = 45279
T = 7.12
random-net-50-2_network-5.net.wcnf S = OPT
O = 50309
T = 10.75		 S = OPT
O = 50309
T = 10.75
random-net-60-2_network-1.net.wcnf S = OPT
O = 53630
T = 10.41		 S = OPT
O = 53630
T = 10.41
random-net-60-2_network-2.net.wcnf S = OPT
O = 55787
T = 12.94		 S = OPT
O = 55787
T = 12.94
random-net-60-2_network-3.net.wcnf S = OPT
O = 57045
T = 12.87		 S = OPT
O = 57045
T = 12.87
random-net-60-2_network-4.net.wcnf S = OPT
O = 54951
T = 10.04		 S = OPT
O = 54951
T = 10.04
random-net-60-2_network-5.net.wcnf S = OPT
O = 56931
T = 16.43		 S = OPT
O = 56931
T = 16.43
random-net-80-2_network-1.net.wcnf S = OPT
O = 67550
T = 14.25		 S = OPT
O = 67550
T = 14.25
random-net-80-2_network-2.net.wcnf S = OPT
O = 73602
T = 17.47		 S = OPT
O = 73602
T = 17.47
random-net-80-2_network-3.net.wcnf S = OPT
O = 70391
T = 24.68		 S = OPT
O = 70391
T = 24.68
random-net-80-2_network-4.net.wcnf S = OPT
O = 77792
T = 18.61		 S = OPT
O = 77792
T = 18.61
random-net-80-2_network-5.net.wcnf S = OPT
O = 71287
T = 7.62		 S = OPT
O = 71287
T = 7.62
scp410_weighted.wcnf S = OPT
O = 514
T = 6.38		 S = OPT
O = 514
T = 6.38
scp41_weighted.wcnf S = OPT
O = 429
T = 6.47		 S = OPT
O = 429
T = 6.47
scp42_weighted.wcnf S = OPT
O = 512
T = 6.39		 S = OPT
O = 512
T = 6.39
scp43_weighted.wcnf S = OPT
O = 516
T = 6.44		 S = OPT
O = 516
T = 6.44
scp44_weighted.wcnf S = OPT
O = 494
T = 6.41		 S = OPT
O = 494
T = 6.41
scp45_weighted.wcnf S = OPT
O = 512
T = 6.46		 S = OPT
O = 512
T = 6.46
scp46_weighted.wcnf S = OPT
O = 560
T = 6.43		 S = OPT
O = 560
T = 6.43
scp47_weighted.wcnf S = OPT
O = 430
T = 6.41		 S = OPT
O = 430
T = 6.41
scp48_weighted.wcnf S = OPT
O = 492
T = 6.47		 S = OPT
O = 492
T = 6.47
scp49_weighted.wcnf S = OPT
O = 641
T = 6.43		 S = OPT
O = 641
T = 6.43
scp510_weighted.wcnf S = OPT
O = 265
T = 6.41		 S = OPT
O = 265
T = 6.41
scp51_weighted.wcnf S = OPT
O = 253
T = 6.44		 S = OPT
O = 253
T = 6.44
scp52_weighted.wcnf S = OPT
O = 302
T = 6.50		 S = OPT
O = 302
T = 6.50
scp53_weighted.wcnf S = OPT
O = 226
T = 6.46		 S = OPT
O = 226
T = 6.46
scp54_weighted.wcnf S = OPT
O = 242
T = 6.42		 S = OPT
O = 242
T = 6.42
scp55_weighted.wcnf S = OPT
O = 211
T = 6.43		 S = OPT
O = 211
T = 6.43
scp56_weighted.wcnf S = OPT
O = 213
T = 6.45		 S = OPT
O = 213
T = 6.45
scp57_weighted.wcnf S = OPT
O = 293
T = 6.48		 S = OPT
O = 293
T = 6.48
scp58_weighted.wcnf S = OPT
O = 288
T = 6.24		 S = OPT
O = 288
T = 6.24
scp59_weighted.wcnf S = OPT
O = 279
T = 6.42		 S = OPT
O = 279
T = 6.42
scp61_weighted.wcnf S = OPT
O = 138
T = 6.87		 S = OPT
O = 138
T = 6.87
scp62_weighted.wcnf S = OPT
O = 146
T = 7.29		 S = OPT
O = 146
T = 7.29
scp63_weighted.wcnf S = OPT
O = 145
T = 6.93		 S = OPT
O = 145
T = 6.93
scp64_weighted.wcnf S = OPT
O = 131
T = 6.49		 S = OPT
O = 131
T = 6.49
scp65_weighted.wcnf S = OPT
O = 161
T = 7.17		 S = OPT
O = 161
T = 7.17
scpnre1_weighted.wcnf S = OPT
O = 29
T = 65.16		 S = OPT
O = 29
T = 65.16
scpnre2_weighted.wcnf S = OPT
O = 30
T = 459.15		 S = OPT
O = 30
T = 459.15
scpnre3_weighted.wcnf S = OPT
O = 27
T = 43.55		 S = OPT
O = 27
T = 43.55
scpnre4_weighted.wcnf S = OPT
O = 28
T = 113.51		 S = OPT
O = 28
T = 113.51
scpnre5_weighted.wcnf S = OPT
O = 28
T = 45.76		 S = OPT
O = 28
T = 45.76
scpnrf1_weighted.wcnf S = OPT
O = 14
T = 99.38		 S = OPT
O = 14
T = 99.38
scpnrf2_weighted.wcnf S = OPT
O = 15
T = 53.38		 S = OPT
O = 15
T = 53.38
scpnrf3_weighted.wcnf S = OPT
O = 14
T = 27.49		 S = OPT
O = 14
T = 27.49
scpnrf4_weighted.wcnf S = OPT
O = 14
T = 158.00		 S = OPT
O = 14
T = 158.00
scpnrf5_weighted.wcnf S = OPT
O = 13
T = 653.07		 S = OPT
O = 13
T = 653.07
scpnrg1_weighted.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
scpnrg2_weighted.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
scpnrg3_weighted.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
scpnrg4_weighted.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
scpnrg5_weighted.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
scpnrh1_weighted.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
scpnrh2_weighted.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
scpnrh3_weighted.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
scpnrh4_weighted.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
scpnrh5_weighted.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
instance1.wcnf S = OPT
O = 607
T = 6.47		 S = OPT
O = 607
T = 6.47
instance10.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
instance11.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
instance12.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
instance2.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
instance3.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
instance4.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
instance5.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
instance6.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
instance7.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
instance8.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
instance9.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
MANN_a27.clq.wcnf S = OPT
O = 2049
T = 272.88		 S = OPT
O = 2049
T = 272.88
MANN_a45.clq.wcnf S = OPT
O = 2057
T = 166.10		 S = OPT
O = 2057
T = 166.10
MANN_a81.clq.wcnf S = OPT
O = 1995
T = 196.21		 S = OPT
O = 1995
T = 196.21
MANN_a9.clq.wcnf S = OPT
O = 2179
T = 218.75		 S = OPT
O = 2179
T = 218.75
hamming10-2.clq.wcnf S = OPT
O = 1929
T = 35.68		 S = OPT
O = 1929
T = 35.68
hamming10-4.clq.wcnf S = OPT
O = 1683
T = 31.56		 S = OPT
O = 1683
T = 31.56
hamming6-2.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
hamming6-4.clq.wcnf S = OPT
O = 1035
T = 6.79		 S = OPT
O = 1035
T = 6.79
hamming8-2.clq.wcnf S = OPT
O = 2213
T = 708.94		 S = OPT
O = 2213
T = 708.94
hamming8-4.clq.wcnf S = OPT
O = 917
T = 6.65		 S = OPT
O = 917
T = 6.65
johnson16-2-4.clq.wcnf S = OPT
O = 1170
T = 6.74		 S = OPT
O = 1170
T = 6.74
johnson32-2-4.clq.wcnf S = OPT
O = 1788
T = 32.91		 S = OPT
O = 1788
T = 32.91
johnson8-2-4.clq.wcnf S = OPT
O = 392
T = 6.61		 S = OPT
O = 392
T = 6.61
johnson8-4-4.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
keller4.clq.wcnf S = OPT
O = 1133
T = 6.64		 S = OPT
O = 1133
T = 6.64
keller5.clq.wcnf S = OPT
O = 1383
T = 9.54		 S = OPT
O = 1383
T = 9.54
p_hat1000-1.clq.wcnf S = OPT
O = 248
T = 6.56		 S = OPT
O = 248
T = 6.56
p_hat1000-2.clq.wcnf S = OPT
O = 752
T = 6.69		 S = OPT
O = 752
T = 6.69
p_hat1000-3.clq.wcnf S = OPT
O = 1251
T = 7.78		 S = OPT
O = 1251
T = 7.78
p_hat300-1.clq.wcnf S = OPT
O = 243
T = 6.55		 S = OPT
O = 243
T = 6.55
p_hat300-2.clq.wcnf S = OPT
O = 711
T = 6.63		 S = OPT
O = 711
T = 6.63
p_hat300-3.clq.wcnf S = OPT
O = 1439
T = 10.20		 S = OPT
O = 1439
T = 10.20
p_hat500-1.clq.wcnf S = OPT
O = 395
T = 6.60		 S = OPT
O = 395
T = 6.60
p_hat500-2.clq.wcnf S = OPT
O = 931
T = 6.92		 S = OPT
O = 931
T = 6.92
p_hat500-3.clq.wcnf S = OPT
O = 1501
T = 10.97		 S = OPT
O = 1501
T = 10.97
p_hat700-1.clq.wcnf S = OPT
O = 329
T = 6.57		 S = OPT
O = 329
T = 6.57
p_hat700-2.clq.wcnf S = OPT
O = 834
T = 6.84		 S = OPT
O = 834
T = 6.84
p_hat700-3.clq.wcnf S = OPT
O = 1432
T = 9.73		 S = OPT
O = 1432
T = 9.73
san1000.clq.wcnf S = OPT
O = 744
T = 6.72		 S = OPT
O = 744
T = 6.72
san200_0.7_1.clq.wcnf S = OPT
O = 1256
T = 8.99		 S = OPT
O = 1256
T = 8.99
san200_0.7_2.clq.wcnf S = OPT
O = 1243
T = 7.85		 S = OPT
O = 1243
T = 7.85
san200_0.9_1.clq.wcnf S = OPT
O = 1672
T = 62.49		 S = OPT
O = 1672
T = 62.49
san200_0.9_2.clq.wcnf S = OPT
O = 1647
T = 19.61		 S = OPT
O = 1647
T = 19.61
san200_0.9_3.clq.wcnf S = OPT
O = 1670
T = 26.31		 S = OPT
O = 1670
T = 26.31
san400_0.5_1.clq.wcnf S = OPT
O = 718
T = 6.67		 S = OPT
O = 718
T = 6.67
san400_0.7_1.clq.wcnf S = OPT
O = 1258
T = 9.89		 S = OPT
O = 1258
T = 9.89
san400_0.7_2.clq.wcnf S = OPT
O = 1237
T = 7.77		 S = OPT
O = 1237
T = 7.77
san400_0.7_3.clq.wcnf S = OPT
O = 1201
T = 7.78		 S = OPT
O = 1201
T = 7.78
san400_0.9_1.clq.wcnf S = OPT
O = 1604
T = 28.04		 S = OPT
O = 1604
T = 28.04
sanr200_0.7.clq.wcnf S = OPT
O = 1171
T = 7.14		 S = OPT
O = 1171
T = 7.14
sanr200_0.9.clq.wcnf S = OPT
O = 1610
T = 27.24		 S = OPT
O = 1610
T = 27.24
sanr400_0.5.clq.wcnf S = OPT
O = 763
T = 6.64		 S = OPT
O = 763
T = 6.64
sanr400_0.7.clq.wcnf S = OPT
O = 1198
T = 7.36		 S = OPT
O = 1198
T = 7.36
t3g3-5555.spn.wcnf S = OPT
O = 1100610
T = 6.51		 S = OPT
O = 1100610
T = 6.51
t4g3-6666.spn.wcnf S = OPT
O = 2275606
T = 6.62		 S = OPT
O = 2275606
T = 6.62
t5g3-7777.spn.wcnf S = OPT
O = 4241951
T = 7.11		 S = OPT
O = 4241951
T = 7.11
t6g3-8888.spn.wcnf S = OPT
O = 7844119
T = 25.74		 S = OPT
O = 7844119
T = 25.74
t7g3-9999.spn.wcnf S = OPT
O = 11954769
T = 387.17		 S = OPT
O = 11954769
T = 387.17