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 CCEHC2akms CCLS2akms Naps-1.02-ms Open-WBO16 Optiriss6 WMaxSatz+ WMaxSatz09 WPM3-2015-co ahms-1.70 ahms-ls-1.70 maxhs-b maxino16-c10 maxino16-dis mscg2015a mscg2015b
rsdecoder-debug.dimacs.cnf S = OPT
O = 1
T = 3.37		 S = N/A
O = N/A
T = TO
 S = N/A
O = 50168
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 1
T = 3.37
 S = OPT
O = 1
T = 50.52
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 1
T = 14.00
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 1
T = 102.60
 S = OPT
O = 1
T = 648.66
 S = OPT
O = 1
T = 320.47
 S = OPT
O = 1
T = 15.02
 S = OPT
O = 1
T = 15.23
sudoku-debug.dimacs.cnf S = OPT
O = 1
T = 3.14		 S = N/A
O = N/A
T = TO
 S = N/A
O = 10341
T = TO
 S = N/A
O = N/A
T = 56.11
 S = OPT
O = 1
T = 3.91
 S = OPT
O = 1
T = 4.64
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 1
T = 5.13
 S = N/A
O = N/A
T = 0.83
 S = N/A
O = N/A
T = 0.85
 S = OPT
O = 1
T = 31.86
 S = OPT
O = 1
T = 23.30
 S = OPT
O = 1
T = 24.23
 S = OPT
O = 1
T = 3.15
 S = OPT
O = 1
T = 3.14
wb-debug.dimacs.cnf S = OPT
O = 28
T = 2.45		 S = N/A
O = 4230
T = TO
 S = N/A
O = 2804
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 28
T = 11.51
 S = OPT
O = 28
T = 11.79
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 28
T = 2.45
 S = N/A
O = N/A
T = 0.41
 S = N/A
O = N/A
T = 0.42
 S = OPT
O = 28
T = 22.05
 S = OPT
O = 28
T = 82.38
 S = OPT
O = 28
T = 49.94
 S = OPT
O = 28
T = 3.62
 S = OPT
O = 28
T = 3.58
SM_AS_TOP_buggy1.dimacs.filtered.cnf S = OPT
O = 57
T = 69.77		 S = N/A
O = 3805
T = TO
 S = N/A
O = 3342
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 57
T = 113.78
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 57
T = 69.77
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 57
T = 873.22
 S = OPT
O = 57
T = 179.13
 S = OPT
O = 57
T = 70.85
 S = OPT
O = 57
T = 71.31
SM_MAIN_MEM_buggy1.dimacs.filtered.cnf S = OPT
O = 390
T = 430.51		 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 8005
T = 73.07
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = 685.84
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 390
T = 430.51
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 390
T = 1058.56
 S = N/A
O = 358
T = TO
 S = N/A
O = 343
T = TO
 S = OPT
O = 390
T = 816.20
 S = OPT
O = 390
T = 815.08
SM_RX_TOP.dimacs.filtered.cnf S = OPT
O = 6
T = 13.02		 S = N/A
O = 7229
T = TO
 S = N/A
O = 5811
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 6
T = 28.50
 S = OPT
O = 6
T = 91.61
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 6
T = 13.02
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 6
T = 135.28
 S = OPT
O = 6
T = 626.46
 S = OPT
O = 6
T = 58.14
 S = OPT
O = 6
T = 26.96
 S = OPT
O = 6
T = 27.21
b15-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 6.85		 S = N/A
O = N/A
T = TO
 S = N/A
O = 28811
T = TO
 S = N/A
O = N/A
T = 63.95
 S = OPT
O = 4
T = 6.85
 S = OPT
O = 4
T = 73.54
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 4
T = 53.99
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 4
T = 93.90
 S = OPT
O = 4
T = 821.63
 S = OPT
O = 4
T = 274.13
 S = OPT
O = 4
T = 72.94
 S = OPT
O = 4
T = 73.64
c1_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 1.73		 S = N/A
O = N/A
T = TO
 S = N/A
O = 7482
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 4
T = 3.48
 S = OPT
O = 4
T = 4.25
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 4
T = 2.47
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 4
T = 20.52
 S = OPT
O = 4
T = 3.98
 S = OPT
O = 4
T = 4.58
 S = OPT
O = 4
T = 1.74
 S = OPT
O = 4
T = 1.73
c2_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 3.99		 S = N/A
O = 11315
T = TO
 S = N/A
O = 11621
T = TO
 S = N/A
O = 7703
T = TO
 S = OPT
O = 4
T = 106.65
 S = OPT
O = 4
T = 5.52
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 4
T = 6.01
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 4
T = 124.66
 S = OPT
O = 4
T = 655.23
 S = OPT
O = 4
T = 50.20
 S = OPT
O = 4
T = 4.03
 S = OPT
O = 4
T = 3.99
c4_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 4.21		 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 8
T = 15.22
 S = OPT
O = 8
T = 10.81
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 8
T = 9.74
 S = N/A
O = N/A
T = 37.31
 S = N/A
O = N/A
T = TO
 S = OPT
O = 8
T = 62.45
 S = OPT
O = 8
T = 20.70
 S = OPT
O = 8
T = 34.30
 S = OPT
O = 8
T = 4.31
 S = OPT
O = 8
T = 4.21
c4_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 2.15		 S = N/A
O = N/A
T = TO
 S = N/A
O = 9756
T = TO
 S = N/A
O = N/A
T = 41.19
 S = OPT
O = 4
T = 6.00
 S = OPT
O = 4
T = 9.70
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 4
T = 74.64
 S = N/A
O = N/A
T = 15.41
 S = N/A
O = N/A
T = TO
 S = OPT
O = 4
T = 90.83
 S = OPT
O = 4
T = 25.20
 S = OPT
O = 4
T = 7.90
 S = OPT
O = 4
T = 2.17
 S = OPT
O = 4
T = 2.15
c5_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 1.10		 S = N/A
O = 2926
T = TO
 S = N/A
O = 2672
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 8
T = 3.86
 S = OPT
O = 8
T = 2.48
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 8
T = 1.91
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 8
T = 22.58
 S = OPT
O = 8
T = 7.80
 S = OPT
O = 8
T = 3.03
 S = OPT
O = 8
T = 1.10
 S = OPT
O = 8
T = 1.14
c5_DD_s3_f1_e1_v2-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 1.12		 S = N/A
O = 2913
T = TO
 S = N/A
O = 2685
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 8
T = 3.82
 S = OPT
O = 8
T = 2.40
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 8
T = 1.93
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 8
T = 24.32
 S = OPT
O = 8
T = 7.70
 S = OPT
O = 8
T = 2.61
 S = OPT
O = 8
T = 1.12
 S = OPT
O = 8
T = 1.12
c6_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 1.65		 S = N/A
O = 6066
T = TO
 S = N/A
O = 5203
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 8
T = 5.11
 S = OPT
O = 8
T = 3.51
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 8
T = 2.45
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 8
T = 21.57
 S = OPT
O = 8
T = 6.50
 S = OPT
O = 8
T = 6.01
 S = OPT
O = 8
T = 1.65
 S = OPT
O = 8
T = 1.66
divider-problem.dimacs_11.filtered.cnf S = OPT
O = 2
T = 7.90		 S = N/A
O = 6578
T = TO
 S = N/A
O = 5592
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 28.27
 S = OPT
O = 2
T = 51.42
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 2
T = 109.15
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 127.29
 S = OPT
O = 2
T = 63.29
 S = OPT
O = 2
T = 49.51
 S = OPT
O = 2
T = 8.11
 S = OPT
O = 2
T = 7.90
divider-problem.dimacs_2.filtered.cnf S = OPT
O = 2
T = 33.78		 S = N/A
O = 7203
T = TO
 S = N/A
O = 6275
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 38.43
 S = OPT
O = 2
T = 40.40
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 2
T = 63.16
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 621.74
 S = OPT
O = 2
T = 51.71
 S = OPT
O = 2
T = 34.38
 S = OPT
O = 2
T = 33.78
divider-problem.dimacs_5.filtered.cnf S = OPT
O = 2
T = 7.88		 S = N/A
O = 6990
T = TO
 S = N/A
O = 6260
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 30.20
 S = OPT
O = 2
T = 7.88
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 2
T = 48.87
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 118.18
 S = OPT
O = 2
T = 349.47
 S = OPT
O = 2
T = 65.83
 S = OPT
O = 2
T = 14.32
 S = OPT
O = 2
T = 14.40
divider-problem.dimacs_8.filtered.cnf S = OPT
O = 2
T = 6.97		 S = N/A
O = 7864
T = TO
 S = N/A
O = 7004
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 6.97
 S = OPT
O = 2
T = 11.73
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 2
T = 70.76
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 139.46
 S = OPT
O = 2
T = 102.09
 S = OPT
O = 2
T = 31.71
 S = OPT
O = 2
T = 40.00
 S = OPT
O = 2
T = 40.22
dividers10.dimacs.filtered.cnf S = OPT
O = 2
T = 1.16		 S = N/A
O = 715
T = TO
 S = N/A
O = 870
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 2.27
 S = OPT
O = 2
T = 1.87
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 4.18
 S = N/A
O = N/A
T = 0.17
 S = N/A
O = N/A
T = 128.02
 S = OPT
O = 2
T = 92.99
 S = OPT
O = 2
T = 40.71
 S = OPT
O = 2
T = 5.06
 S = OPT
O = 2
T = 1.16
 S = OPT
O = 2
T = 1.18
dividers_multivec1.dimacs.filtered.cnf S = OPT
O = 2
T = 2.43		 S = N/A
O = 3646
T = TO
 S = N/A
O = 2600
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 2.65
 S = OPT
O = 2
T = 4.07
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 2
T = 3.15
 S = N/A
O = N/A
T = 0.37
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 45.73
 S = OPT
O = 2
T = 16.42
 S = OPT
O = 2
T = 7.66
 S = OPT
O = 2
T = 2.43
 S = OPT
O = 2
T = 2.43
fpu_multivec1-problem.dimacs_14.filtered.cnf S = OPT
O = 2
T = 3.96		 S = N/A
O = 8889
T = TO
 S = N/A
O = 7355
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 4.86
 S = OPT
O = 2
T = 13.61
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 2
T = 4.64
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 52.08
 S = OPT
O = 2
T = 4.03
 S = OPT
O = 2
T = 3.96
 S = OPT
O = 2
T = 7.28
 S = OPT
O = 2
T = 7.26
i2c-problem.dimacs_25.filtered.cnf S = OPT
O = 2
T = 6.98		 S = N/A
O = N/A
T = TO
 S = N/A
O = 14021
T = TO
 S = N/A
O = N/A
T = 60.66
 S = OPT
O = 2
T = 16.07
 S = OPT
O = 2
T = 14.88
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 2
T = 13.58
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 51.22
 S = OPT
O = 2
T = 57.52
 S = OPT
O = 2
T = 6.98
 S = OPT
O = 2
T = 8.68
i2c-problem.dimacs_26.filtered.cnf S = OPT
O = 2
T = 7.62		 S = N/A
O = N/A
T = TO
 S = N/A
O = 7980
T = TO
 S = N/A
O = N/A
T = 45.65
 S = OPT
O = 2
T = 14.38
 S = OPT
O = 2
T = 23.66
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 2
T = 28.04
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 138.36
 S = OPT
O = 2
T = 42.74
 S = OPT
O = 2
T = 50.48
 S = OPT
O = 2
T = 7.73
 S = OPT
O = 2
T = 7.62
mem_ctrl-problem.dimacs_27.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = 15983634
T = TO
 S = N/A
O = N/A
T = 0.02
 S = N/A
O = N/A
T = 0.01
 S = N/A
O = N/A
T = 25.95
 S = N/A
O = N/A
T = 5.43
 S = N/A
O = N/A
T = 5.53
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = 9.33
mem_ctrl1.dimacs.filtered.cnf S = OPT
O = 1
T = 8.06		 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 1
T = 9.64
 S = OPT
O = 1
T = 10.95
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 1
T = 11.90
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 1
T = 49.89
 S = OPT
O = 1
T = 250.56
 S = OPT
O = 1
T = 27.76
 S = OPT
O = 1
T = 8.06
 S = OPT
O = 1
T = 8.06
mem_ctrl2_blackbox_mc_dp-problem.dimacs_28.filtered.cnf S = OPT
O = 3
T = 39.70		 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 3
T = 40.47
 S = OPT
O = 3
T = 102.77
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 3
T = 39.70
 S = N/A
O = N/A
T = 0.18
 S = N/A
O = N/A
T = 0.17
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 3
T = 41.41
 S = OPT
O = 3
T = 42.27
mrisc_mem2wire-problem.dimacs_29.filtered.cnf S = OPT
O = 1
T = 4.53		 S = N/A
O = N/A
T = TO
 S = N/A
O = 50134
T = TO
 S = N/A
O = 3565
T = TO
 S = OPT
O = 1
T = 8.11
 S = OPT
O = 1
T = 7.21
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 1
T = 10.07
 S = N/A
O = N/A
T = 0.48
 S = N/A
O = N/A
T = 0.47
 S = OPT
O = 1
T = 304.40
 S = OPT
O = 1
T = 105.28
 S = OPT
O = 1
T = 34.73
 S = OPT
O = 1
T = 4.53
 S = OPT
O = 1
T = 4.83
rsdecoder-problem.dimacs_31.filtered.cnf S = OPT
O = 1
T = 32.79		 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 1
T = 325.75
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = 3
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 1
T = 162.24
 S = OPT
O = 1
T = 129.96
 S = OPT
O = 1
T = 332.81
 S = OPT
O = 1
T = 32.99
 S = OPT
O = 1
T = 32.79
rsdecoder-problem.dimacs_36.filtered.cnf S = OPT
O = 1
T = 20.64		 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 1
T = 20.64
 S = OPT
O = 1
T = 32.13
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 1
T = 26.82
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 548
T = 527.92
 S = OPT
O = 1
T = 776.73
 S = OPT
O = 1
T = 166.89
 S = OPT
O = 1
T = 89.46
 S = OPT
O = 1
T = 88.09
rsdecoder-problem.dimacs_37.filtered.cnf S = OPT
O = 1
T = 378.86		 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 615
T = 37.13
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = 615
T = 508.16
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 1
T = 1025.30
 S = OPT
O = 1
T = 378.86
 S = N/A
O = N/A
T = 122.80
 S = N/A
O = N/A
T = 123.23
rsdecoder-problem.dimacs_38.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 2053
T = 73.36
 S = N/A
O = 448
T = 872.94
 S = N/A
O = 221410
T = 525.65
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = 448
T = 1222.87
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 1
T = 1529.57
 S = N/A
O = 1
T = 855.45
 S = N/A
O = N/A
T = 419.60
 S = N/A
O = N/A
T = 406.97
rsdecoder-problem.dimacs_39.filtered.cnf S = OPT
O = 1
T = 6.46		 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 1
T = 49.17
 S = OPT
O = 1
T = 79.32
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 1
T = 51.41
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 1
T = 154.03
 S = OPT
O = 1
T = 188.34
 S = OPT
O = 1
T = 6.46
 S = OPT
O = 1
T = 6.59
rsdecoder-problem.dimacs_40.filtered.cnf S = OPT
O = 1
T = 23.33		 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 1
T = 23.33
 S = OPT
O = 1
T = 40.42
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 1
T = 78.12
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 1
T = 822.42
 S = OPT
O = 1
T = 129.16
 S = OPT
O = 1
T = 41.92
 S = OPT
O = 1
T = 42.34
rsdecoder-problem.dimacs_41.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 2020
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 219331
T = 507.99
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = 2634
T = 715.55
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 646
T = 509.99
 S = N/A
O = 1
T = 1476.47
 S = N/A
O = 1
T = 510.46
 S = N/A
O = N/A
T = 362.33
 S = N/A
O = N/A
T = 360.75
rsdecoder1_blackbox_CSEEblock-problem.dimacs_32.filtered.cnf S = OPT
O = 4
T = 654.22		 S = N/A
O = 6199
T = TO
 S = N/A
O = 5696
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 4
T = 1364.72
 S = N/A
O = N/A
T = 1449.86
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 4
T = 654.22
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 3
T = TO
 S = N/A
O = 4
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
rsdecoder1_blackbox_KESblock-problem.dimacs_30.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = 8529
T = TO
 S = N/A
O = 8769
T = TO
 S = N/A
O = N/A
T = 39.31
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = 1695.39
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = 819
T = TO
 S = N/A
O = N/A
T = 0.75
 S = N/A
O = N/A
T = 0.76
 S = N/A
O = 1997
T = 1003.65
 S = N/A
O = 1
T = TO
 S = N/A
O = 1
T = TO
 S = N/A
O = N/A
T = 1566.25
 S = N/A
O = N/A
T = 1552.38
rsdecoder2.dimacs.filtered.cnf S = OPT
O = 1
T = 11.48		 S = N/A
O = N/A
T = TO
 S = N/A
O = 18657
T = TO
 S = N/A
O = N/A
T = 57.03
 S = OPT
O = 1
T = 46.24
 S = OPT
O = 1
T = 148.34
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 1
T = 50.34
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 1
T = 156.84
 S = OPT
O = 1
T = 192.04
 S = OPT
O = 1
T = 369.94
 S = OPT
O = 1
T = 11.48
 S = OPT
O = 1
T = 11.50
rsdecoder4.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = 10913
T = TO
 S = N/A
O = 8039
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 215
T = 1500.57
 S = N/A
O = 80138
T = 1289.71
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = 215
T = 976.25
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 1231
T = 282.90
 S = N/A
O = 3
T = TO
 S = N/A
O = 3
T = TO
 S = N/A
O = N/A
T = 1143.28
 S = N/A
O = N/A
T = 1142.75
rsdecoder5.dimacs.filtered.cnf S = OPT
O = 2
T = 22.42		 S = N/A
O = 9020
T = TO
 S = N/A
O = 8014
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 96.79
 S = OPT
O = 2
T = 79.84
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 2
T = 454.12
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 368
T = 270.45
 S = OPT
O = 2
T = 1169.60
 S = OPT
O = 2
T = 290.63
 S = OPT
O = 2
T = 22.42
 S = OPT
O = 2
T = 23.32
rsdecoder6.dimacs.filtered.cnf S = OPT
O = 3
T = 360.25		 S = N/A
O = 9360
T = TO
 S = N/A
O = 8134
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 3
T = 965.49
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = 80
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 4
T = 677.91
 S = N/A
O = 3
T = TO
 S = OPT
O = 3
T = 647.97
 S = OPT
O = 3
T = 361.02
 S = OPT
O = 3
T = 360.25
rsdecoder_fsm2.dimacs.filtered.cnf S = OPT
O = 2
T = 5.30		 S = N/A
O = 9295
T = TO
 S = N/A
O = 8082
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 2
T = 20.61
 S = OPT
O = 2
T = 12.02
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 2
T = 8.18
 S = N/A
O = N/A
T = 834.59
 S = N/A
O = N/A
T = TO
 S = N/A
O = 4
T = 590.28
 S = OPT
O = 2
T = 673.47
 S = OPT
O = 2
T = 41.62
 S = OPT
O = 2
T = 5.33
 S = OPT
O = 2
T = 5.30
rsdecoder_multivec1-problem.dimacs_33.filtered.cnf S = OPT
O = 4
T = 36.19		 S = N/A
O = N/A
T = TO
 S = N/A
O = 36879
T = TO
 S = N/A
O = N/A
T = 75.11
 S = OPT
O = 4
T = 758.88
 S = OPT
O = 4
T = 186.28
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 4
T = 439.11
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 17
T = 383.25
 S = OPT
O = 4
T = 904.89
 S = N/A
O = 2
T = TO
 S = OPT
O = 4
T = 36.47
 S = OPT
O = 4
T = 36.19
rsdecoder_multivec1.dimacs.filtered.cnf S = OPT
O = 4
T = 17.82		 S = N/A
O = N/A
T = TO
 S = N/A
O = 19815
T = TO
 S = N/A
O = N/A
T = 56.89
 S = OPT
O = 4
T = 68.31
 S = OPT
O = 4
T = 139.73
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 4
T = 69.38
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 16548
T = 345.71
 S = OPT
O = 4
T = 785.85
 S = N/A
O = 3
T = TO
 S = OPT
O = 4
T = 17.82
 S = OPT
O = 4
T = 17.92
wb-problem.dimacs_45.filtered.cnf S = OPT
O = 14
T = 1.51		 S = N/A
O = 4749
T = TO
 S = N/A
O = 4134
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 14
T = 7.45
 S = OPT
O = 14
T = 2.64
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 14
T = 2.60
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 14
T = 19.76
 S = OPT
O = 14
T = 3.55
 S = OPT
O = 14
T = 3.66
 S = OPT
O = 14
T = 1.51
 S = OPT
O = 14
T = 1.55
wb-problem.dimacs_46.filtered.cnf S = OPT
O = 476
T = 16.44		 S = N/A
O = 4822
T = TO
 S = N/A
O = 4743
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 476
T = 251.14
 S = OPT
O = 476
T = 135.27
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 476
T = 25.15
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 476
T = 36.30
 S = OPT
O = 476
T = 54.25
 S = OPT
O = 476
T = 56.87
 S = OPT
O = 476
T = 16.44
 S = OPT
O = 476
T = 16.46
wb1.dimacs.filtered.cnf S = OPT
O = 218
T = 1.55		 S = N/A
O = 1166
T = TO
 S = N/A
O = 912
T = TO
 S = N/A
O = 1035
T = 93.12
 S = OPT
O = 218
T = 27.13
 S = OPT
O = 218
T = 6.91
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 218
T = 2.84
 S = N/A
O = N/A
T = 1.43
 S = N/A
O = N/A
T = 164.75
 S = OPT
O = 218
T = 80.32
 S = OPT
O = 218
T = 7.36
 S = OPT
O = 218
T = 3.06
 S = OPT
O = 218
T = 1.56
 S = OPT
O = 218
T = 1.55
wb2.dimacs.filtered.cnf S = OPT
O = 588
T = 3.88		 S = N/A
O = 1556
T = TO
 S = N/A
O = 1286
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 588
T = 76.15
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 588
T = 8.45
 S = N/A
O = N/A
T = 0.20
 S = N/A
O = N/A
T = 159.86
 S = OPT
O = 588
T = 118.61
 S = OPT
O = 588
T = 179.89
 S = OPT
O = 588
T = 172.10
 S = OPT
O = 588
T = 3.94
 S = OPT
O = 588
T = 3.88
wb_4m8s-problem.dimacs_47.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = 8517028
T = TO
 S = N/A
O = N/A
T = 0.21
 S = N/A
O = N/A
T = 0.22
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = 7.25
 S = N/A
O = N/A
T = 7.30
wb_4m8s-problem.dimacs_48.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = 8774656
T = TO
 S = N/A
O = N/A
T = 0.21
 S = N/A
O = N/A
T = 0.22
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = 7.30
 S = N/A
O = N/A
T = 7.49
wb_4m8s-problem.dimacs_49.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = 8812800
T = TO
 S = N/A
O = N/A
T = 0.22
 S = N/A
O = N/A
T = 0.23
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = 7.53
wb_4m8s1.dimacs.filtered.cnf S = OPT
O = 18
T = 664.32		 S = N/A
O = N/A
T = TO
 S = N/A
O = 21382
T = TO
 S = N/A
O = N/A
T = 60.83
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = 1328.23
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 18
T = 664.32
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 11
T = TO
 S = N/A
O = 16
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
wb_4m8s3.dimacs.filtered.cnf S = OPT
O = 8
T = 3.16		 S = N/A
O = N/A
T = TO
 S = N/A
O = 22002
T = TO
 S = N/A
O = N/A
T = 60.70
 S = OPT
O = 8
T = 10.87
 S = OPT
O = 8
T = 5.94
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 8
T = 5.50
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 8
T = 23.98
 S = OPT
O = 8
T = 7.77
 S = OPT
O = 8
T = 8.15
 S = OPT
O = 8
T = 3.16
 S = OPT
O = 8
T = 3.19
wb_4m8s4.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
 S = N/A
O = 21913
T = TO
 S = N/A
O = N/A
T = 61.01
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = 896.93
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = 230
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = 196
T = TO
 S = N/A
O = 199
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
wb_conmax1.dimacs.filtered.cnf S = OPT
O = 40
T = 38.48		 S = N/A
O = 4815
T = TO
 S = N/A
O = 4393
T = TO
 S = N/A
O = N/A
T = 42.72
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = 1465.31
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 40
T = 323.82
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 40
T = 1256.12
 S = OPT
O = 40
T = 623.22
 S = OPT
O = 40
T = 38.48
 S = OPT
O = 40
T = 39.16
wb_conmax3.dimacs.filtered.cnf S = OPT
O = 33
T = 13.09		 S = N/A
O = 4973
T = TO
 S = N/A
O = 4602
T = TO
 S = N/A
O = N/A
T = 43.59
 S = N/A
O = N/A
T = TO
 S = OPT
O = 33
T = 100.39
 S = N/A
O = N/A
T = 0.00
 S = N/A
O = N/A
T = 0.00
 S = OPT
O = 33
T = 17.05
 S = N/A
O = N/A
T = TO
 S = N/A
O = N/A
T = TO
 S = OPT
O = 33
T = 719.33
 S = N/A
O = 31
T = TO
 S = OPT
O = 33
T = 216.53
 S = OPT
O = 33
T = 13.13
 S = OPT
O = 33
T = 13.09