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
TextBest solver column
TextOptimal solution with the best CPU time
TextOptimal solution and finished within the Time Out
TextOptimal solution and did not finish within the Time Out
TextTime Out
TextBuggy solution

Instance file name Best solver IncMaxSatz PM2 QMaxSat0.4-cnf WMaxSatz+ WMaxSatz-2009 WPM1 akmaxsat akmaxsat_ls claspMaxSat sat4j-maxsat wbo1.6-cnf
rsdecoder-debug.dimacs.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.90
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 9.04
(out)(err)		 S = N/A
O = N/A
T = 4.69
(out)(err)		 S = N/A
O = N/A
T = 4.74
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 36.89
(out)(err)		 S = N/A
O = N/A
T = 2.17
(out)(err)
sudoku-debug.dimacs.cnf S = OPT
O = 1
T = 31.82		 S = N/A
O = N/A
T = 0.85
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 1
T = 31.82
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 33.93
(out)(err)		 S = N/A
O = N/A
T = 2.09
(out)(err)
wb-debug.dimacs.cnf S = OPT
O = 28
T = 27.26		 S = N/A
O = N/A
T = 0.81
(out)(err)		 S = OPT
O = 28
T = 60.31
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 28
T = 27.26
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 5822
T = TO
(out)(err)		 S = N/A
O = N/A
T = 27.31
(out)(err)		 S = N/A
O = N/A
T = 1.96
(out)(err)
SM_AS_TOP_buggy1.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.83
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 5349
T = TO
(out)(err)		 S = N/A
O = 84
T = TO
(out)(err)		 S = N/A
O = 84
T = 23.46
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
SM_MAIN_MEM_buggy1.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.84
(out)(err)		 S = N/A
O = N/A
T = 10.66
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 12.40
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 7.44
(out)(err)		 S = N/A
O = N/A
T = 0.01
(out)(err)		 S = N/A
O = N/A
T = 28.98
(out)(err)		 S = N/A
O = N/A
T = 2.16
(out)(err)
SM_RX_TOP.dimacs.filtered.cnf S = OPT
O = 6
T = 51.13		 S = N/A
O = N/A
T = 0.83
(out)(err)		 S = OPT
O = 6
T = 120.53
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 6
T = 51.13
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 46.90
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
b15-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 302.22		 S = N/A
O = N/A
T = 0.69
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 4
T = 302.22
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 35.26
(out)(err)		 S = N/A
O = N/A
T = 2.12
(out)(err)
c1_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 12.28		 S = N/A
O = N/A
T = 0.66
(out)(err)		 S = OPT
O = 4
T = 27.11
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 4
T = 12.28
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 41.89
(out)(err)		 S = N/A
O = N/A
T = 1.40
(out)(err)
c2_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 17.11		 S = N/A
O = N/A
T = 0.67
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 4
T = 17.11
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 36.45
(out)(err)		 S = N/A
O = N/A
T = 1.49
(out)(err)
c4_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 46.41		 S = N/A
O = N/A
T = 0.68
(out)(err)		 S = N/A
O = N/A
T = 7.49
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 8
T = 46.41
(out)(err)		 S = N/A
O = N/A
T = 3.58
(out)(err)		 S = N/A
O = N/A
T = 3.64
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 26.05
(out)(err)		 S = N/A
O = N/A
T = 2.45
(out)(err)
c4_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 16.78		 S = N/A
O = N/A
T = 0.62
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 4
T = 16.78
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 34.11
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
c5_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 10.24		 S = N/A
O = N/A
T = 0.71
(out)(err)		 S = OPT
O = 8
T = 22.96
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 8
T = 10.24
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 8
T = TO
(out)(err)		 S = N/A
O = 8
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
c5_DD_s3_f1_e1_v2-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 10.07		 S = N/A
O = N/A
T = 0.72
(out)(err)		 S = OPT
O = 8
T = 22.96
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 8
T = 10.07
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 8
T = TO
(out)(err)		 S = N/A
O = 8
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
c6_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 16.12		 S = N/A
O = N/A
T = 0.65
(out)(err)		 S = OPT
O = 8
T = 30.79
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 8
T = 16.12
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 53.50
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
divider-problem.dimacs_11.filtered.cnf S = OPT
O = 2
T = 227.14		 S = N/A
O = N/A
T = 0.81
(out)(err)		 S = OPT
O = 2
T = 227.14
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 2
T = 817.15
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 2
T = TO
(out)(err)		 S = N/A
O = N/A
T = 15.40
(out)(err)		 S = N/A
O = N/A
T = 1.91
(out)(err)
divider-problem.dimacs_2.filtered.cnf S = OPT
O = 2
T = 518.75		 S = N/A
O = N/A
T = 0.83
(out)(err)		 S = OPT
O = 2
T = 518.75
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = 2
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 3
T = TO
(out)(err)		 S = N/A
O = N/A
T = 16.34
(out)(err)		 S = N/A
O = N/A
T = 2.05
(out)(err)
divider-problem.dimacs_5.filtered.cnf S = OPT
O = 2
T = 160.14		 S = N/A
O = N/A
T = 0.90
(out)(err)		 S = N/A
O = 2
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 2
T = 160.14
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 7
T = TO
(out)(err)		 S = N/A
O = N/A
T = 13.96
(out)(err)		 S = N/A
O = N/A
T = 2.10
(out)(err)
divider-problem.dimacs_8.filtered.cnf S = OPT
O = 2
T = 228.99		 S = N/A
O = N/A
T = 0.84
(out)(err)		 S = OPT
O = 2
T = 228.99
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 2
T = 863.50
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 56.57
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
dividers10.dimacs.filtered.cnf S = OPT
O = 2
T = 26.59		 S = N/A
O = N/A
T = 0.27
(out)(err)		 S = OPT
O = 2
T = 68.99
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 2
T = 80.49
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 1762
T = TO
(out)(err)		 S = OPT
O = 2
T = 464.72
(out)(err)		 S = N/A
O = 2
T = TO
(out)(err)		 S = OPT
O = 2
T = 26.59
(out)(err)
dividers_multivec1.dimacs.filtered.cnf S = OPT
O = 2
T = 7.73		 S = N/A
O = N/A
T = 0.66
(out)(err)		 S = OPT
O = 2
T = 12.97
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 2
T = 7.73
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 5642
T = TO
(out)(err)		 S = OPT
O = 2
T = 162.81
(out)(err)		 S = N/A
O = 2605
T = TO
(out)(err)		 S = OPT
O = 2
T = 9.81
(out)(err)
fpu_multivec1-problem.dimacs_14.filtered.cnf S = OPT
O = 2
T = 12.37		 S = N/A
O = N/A
T = 0.88
(out)(err)		 S = OPT
O = 2
T = 20.40
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 2
T = 12.37
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 44.49
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
i2c-problem.dimacs_25.filtered.cnf S = OPT
O = 2
T = 770.90		 S = N/A
O = N/A
T = 0.76
(out)(err)		 S = N/A
O = N/A
T = 6.70
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 2
T = 770.90
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 48.60
(out)(err)		 S = N/A
O = N/A
T = 1.78
(out)(err)
i2c-problem.dimacs_26.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.81
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 38.85
(out)(err)		 S = N/A
O = N/A
T = 1.42
(out)(err)
mem_ctrl-problem.dimacs_27.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.76
(out)(err)		 S = N/A
O = N/A
T = 11.56
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 12.65
(out)(err)		 S = N/A
O = N/A
T = 23.53
(out)(err)		 S = N/A
O = N/A
T = 23.33
(out)(err)		 S = N/A
O = N/A
T = 0.01
(out)(err)		 S = N/A
O = N/A
T = 2.17
(out)(err)		 S = N/A
O = N/A
T = 1.57
(out)(err)
mem_ctrl1.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.81
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 8.21
(out)(err)		 S = N/A
O = N/A
T = 8.12
(out)(err)		 S = N/A
O = N/A
T = 0.01
(out)(err)		 S = N/A
O = N/A
T = 29.24
(out)(err)		 S = N/A
O = N/A
T = 2.19
(out)(err)
mem_ctrl2_blackbox_mc_dp-problem.dimacs_28.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.81
(out)(err)		 S = N/A
O = N/A
T = 11.72
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 12.83
(out)(err)		 S = N/A
O = N/A
T = 12.51
(out)(err)		 S = N/A
O = N/A
T = 12.41
(out)(err)		 S = N/A
O = N/A
T = 0.01
(out)(err)		 S = N/A
O = N/A
T = 3.26
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
mrisc_mem2wire-problem.dimacs_29.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.72
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 5.82
(out)(err)		 S = N/A
O = N/A
T = 5.78
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 29.04
(out)(err)		 S = N/A
O = N/A
T = 2.06
(out)(err)
rsdecoder-problem.dimacs_31.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.83
(out)(err)		 S = N/A
O = N/A
T = 11.98
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 7.24
(out)(err)		 S = N/A
O = N/A
T = 0.01
(out)(err)		 S = N/A
O = N/A
T = 28.36
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder-problem.dimacs_36.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.77
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 7.39
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 31.39
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder-problem.dimacs_37.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.76
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 12.59
(out)(err)		 S = N/A
O = N/A
T = 9.12
(out)(err)		 S = N/A
O = N/A
T = 9.00
(out)(err)		 S = N/A
O = N/A
T = 0.01
(out)(err)		 S = N/A
O = N/A
T = 18.61
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder-problem.dimacs_38.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.78
(out)(err)		 S = N/A
O = N/A
T = 11.95
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 7.24
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.01
(out)(err)		 S = N/A
O = N/A
T = 27.57
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder-problem.dimacs_39.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.78
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 7.18
(out)(err)		 S = N/A
O = N/A
T = 0.01
(out)(err)		 S = N/A
O = N/A
T = 29.11
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder-problem.dimacs_40.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.81
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 7.32
(out)(err)		 S = N/A
O = N/A
T = 7.41
(out)(err)		 S = N/A
O = N/A
T = 0.01
(out)(err)		 S = N/A
O = N/A
T = 26.10
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder-problem.dimacs_41.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.79
(out)(err)		 S = N/A
O = N/A
T = 11.87
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 7.28
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 35.88
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder1_blackbox_CSEEblock-problem.dimacs_32.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.82
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 48.61
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder1_blackbox_KESblock-problem.dimacs_30.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.81
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 56.94
(out)(err)		 S = N/A
O = N/A
T = 1.55
(out)(err)
rsdecoder2.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.83
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 342.61
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 46.76
(out)(err)		 S = N/A
O = N/A
T = 1.88
(out)(err)
rsdecoder4.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.86
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 46.82
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder5.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.82
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 59.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder6.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.88
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 48.42
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder_fsm2.dimacs.filtered.cnf S = OPT
O = 2
T = 457.48		 S = N/A
O = N/A
T = 0.77
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 2
T = 457.48
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 44.58
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder_multivec1-problem.dimacs_33.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.81
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 5.20
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 45.35
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder_multivec1.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.81
(out)(err)		 S = N/A
O = N/A
T = 6.70
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 45.10
(out)(err)		 S = N/A
O = N/A
T = 1.83
(out)(err)
wb-problem.dimacs_45.filtered.cnf S = OPT
O = 14
T = 20.61		 S = N/A
O = N/A
T = 0.75
(out)(err)		 S = OPT
O = 14
T = 38.11
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 14
T = 20.61
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 43.72
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
wb-problem.dimacs_46.filtered.cnf S = OPT
O = 476
T = 443.94		 S = N/A
O = N/A
T = 0.74
(out)(err)		 S = OPT
O = 476
T = 989.89
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 476
T = 443.94
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 40.91
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
wb1.dimacs.filtered.cnf S = OPT
O = 218
T = 31.62		 S = N/A
O = N/A
T = 0.23
(out)(err)		 S = OPT
O = 218
T = 88.87
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 218
T = 31.62
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 1421
T = TO
(out)(err)		 S = N/A
O = 407
T = TO
(out)(err)		 S = N/A
O = 392
T = TO
(out)(err)		 S = OPT
O = 218
T = 60.32
(out)(err)
wb2.dimacs.filtered.cnf S = OPT
O = 588
T = 179.72		 S = N/A
O = N/A
T = 0.24
(out)(err)		 S = OPT
O = 588
T = 227.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 588
T = 532.20
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 1974
T = TO
(out)(err)		 S = N/A
O = 815
T = TO
(out)(err)		 S = N/A
O = 800
T = TO
(out)(err)		 S = OPT
O = 588
T = 179.72
(out)(err)
wb_4m8s-problem.dimacs_47.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.74
(out)(err)		 S = N/A
O = N/A
T = 11.31
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 12.36
(out)(err)		 S = N/A
O = N/A
T = 15.23
(out)(err)		 S = N/A
O = N/A
T = 15.33
(out)(err)		 S = N/A
O = N/A
T = 0.01
(out)(err)		 S = N/A
O = N/A
T = 2.94
(out)(err)		 S = N/A
O = N/A
T = 1.51
(out)(err)
wb_4m8s-problem.dimacs_48.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.78
(out)(err)		 S = N/A
O = N/A
T = 11.19
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 12.36
(out)(err)		 S = N/A
O = N/A
T = 15.84
(out)(err)		 S = N/A
O = N/A
T = 15.85
(out)(err)		 S = N/A
O = N/A
T = 0.01
(out)(err)		 S = N/A
O = N/A
T = 3.14
(out)(err)		 S = N/A
O = N/A
T = 1.52
(out)(err)
wb_4m8s-problem.dimacs_49.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.75
(out)(err)		 S = N/A
O = N/A
T = 11.43
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 15.61
(out)(err)		 S = N/A
O = N/A
T = 15.80
(out)(err)		 S = N/A
O = N/A
T = 0.01
(out)(err)		 S = N/A
O = N/A
T = 3.02
(out)(err)		 S = N/A
O = N/A
T = 1.51
(out)(err)
wb_4m8s1.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.77
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 39.26
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
wb_4m8s3.dimacs.filtered.cnf S = OPT
O = 8
T = 26.64		 S = N/A
O = N/A
T = 0.84
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 8
T = 26.64
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 45.95
(out)(err)		 S = N/A
O = N/A
T = 1.91
(out)(err)
wb_4m8s4.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.76
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 55.99
(out)(err)		 S = N/A
O = N/A
T = 1.98
(out)(err)
wb_conmax1.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.84
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 38.29
(out)(err)		 S = N/A
O = N/A
T = 1.55
(out)(err)
wb_conmax3.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 0.85
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 38.80
(out)(err)		 S = N/A
O = N/A
T = 1.50
(out)(err)