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 ILP-2013 ISAC+-ms MSUnCore MaxHS Maxsatz2013f Toulbar2 WMaxSatz+ WMaxSatz09 WPM1-2011 ahmaxsat ckmax-small glpk-maxsat optimax optimax-ni pmifumax scip-maxsat toysat wbo2.1-cnf
rsdecoder-debug.dimacs.cnf S = OPT
O = 1
T = 4.99		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 1
T = 574.12
(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 = 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 = 12.51
(out)(err)		 S = N/A
O = N/A
T = 0.09
(out)(err)		 S = N/A
O = N/A
T = 7.04
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 1
T = 74.86
(out)(err)		 S = OPT
O = 1
T = 19.27
(out)(err)		 S = OPT
O = 1
T = 4.99
(out)(err)		 S = N/A
O = N/A
T = 9.51
(out)(err)		 S = N/A
O = N/A
T = 42.96
(out)(err)		 S = OPT
O = 1
T = 1733.31
(out)(err)
sudoku-debug.dimacs.cnf S = OPT
O = 1
T = 3.04		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 1
T = 5.87
(out)(err)		 S = OPT
O = 1
T = 20.90
(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 = 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 = 12.11
(out)(err)		 S = N/A
O = N/A
T = 0.14
(out)(err)		 S = N/A
O = N/A
T = 742.53
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 1
T = 10.32
(out)(err)		 S = OPT
O = 1
T = 3.04
(out)(err)		 S = OPT
O = 1
T = 3.81
(out)(err)		 S = N/A
O = N/A
T = 6.86
(out)(err)		 S = N/A
O = N/A
T = 124.28
(out)(err)		 S = OPT
O = 1
T = 6.14
(out)(err)
wb-debug.dimacs.cnf S = OPT
O = 28
T = 2.08		 S = N/A
O = N/A
T = 27.80
(out)(err)		 S = OPT
O = 28
T = 10.27
(out)(err)		 S = OPT
O = 28
T = 20.19
(out)(err)		 S = OPT
O = 28
T = 757.64
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = 424
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 = 10.96
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 3.03
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 28
T = 2.08
(out)(err)		 S = OPT
O = 28
T = 8.01
(out)(err)		 S = OPT
O = 28
T = 8.57
(out)(err)		 S = N/A
O = 616635
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 28
T = 19.73
(out)(err)
SM_AS_TOP_buggy1.dimacs.filtered.cnf S = OPT
O = 57
T = 437.37		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 58
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 = 584
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 = 3.51
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 73
T = 1181.87
(out)(err)		 S = N/A
O = 61
T = TO
(out)(err)		 S = OPT
O = 57
T = 437.37
(out)(err)		 S = N/A
O = 688981
T = 26.77
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 57
T = 1755.18
(out)(err)
SM_MAIN_MEM_buggy1.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 6.35
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 576
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 = 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 = 0.14
(out)(err)		 S = N/A
O = N/A
T = 10.08
(out)(err)		 S = N/A
O = N/A
T = 0.74
(out)(err)		 S = N/A
O = 393
T = TO
(out)(err)		 S = N/A
O = 392
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 = TO
(out)(err)
SM_RX_TOP.dimacs.filtered.cnf S = OPT
O = 6
T = 16.89		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 6
T = 1267.79
(out)(err)		 S = OPT
O = 6
T = 227.17
(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 = 377
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 = 16.89
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 4.37
(out)(err)		 S = N/A
O = N/A
T = 0.23
(out)(err)		 S = OPT
O = 6
T = 94.42
(out)(err)		 S = OPT
O = 6
T = 40.23
(out)(err)		 S = OPT
O = 6
T = 100.80
(out)(err)		 S = N/A
O = 931316
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 1794.36
(out)(err)
b15-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 5.77		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 4
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 = 18457
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 = 124.22
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 6.81
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 4
T = 9.55
(out)(err)		 S = OPT
O = 4
T = 22.46
(out)(err)		 S = OPT
O = 4
T = 5.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 = 1795.82
(out)(err)
c1_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 1.46		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 4
T = 3.64
(out)(err)		 S = OPT
O = 4
T = 13.68
(out)(err)		 S = OPT
O = 4
T = 8.69
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = 868
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 = 5.11
(out)(err)		 S = N/A
O = N/A
T = 0.08
(out)(err)		 S = N/A
O = N/A
T = 4.09
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 4
T = 1.46
(out)(err)		 S = OPT
O = 4
T = 2.69
(out)(err)		 S = OPT
O = 4
T = 3.42
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 4
T = 6.53
(out)(err)
c2_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 5.44		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 4
T = 6.41
(out)(err)		 S = OPT
O = 4
T = 16.69
(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 = 6305
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 = 7.34
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 3.82
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 4
T = 78.29
(out)(err)		 S = OPT
O = 4
T = 45.58
(out)(err)		 S = OPT
O = 4
T = 5.44
(out)(err)		 S = N/A
O = N/A
T = 6.99
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 4
T = 18.78
(out)(err)
c4_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 5.27		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 11.13
(out)(err)		 S = OPT
O = 8
T = 38.23
(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 = 12933
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.35
(out)(err)		 S = N/A
O = N/A
T = 0.09
(out)(err)		 S = N/A
O = N/A
T = 6.95
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 5.27
(out)(err)		 S = OPT
O = 8
T = 11.57
(out)(err)		 S = OPT
O = 8
T = 11.34
(out)(err)		 S = N/A
O = N/A
T = 8.28
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 24.34
(out)(err)
c4_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 3.01		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 4
T = 6.85
(out)(err)		 S = OPT
O = 4
T = 14.59
(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 = 5523
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 = 6.37
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 3.31
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 4
T = 3.01
(out)(err)		 S = OPT
O = 4
T = 3.75
(out)(err)		 S = OPT
O = 4
T = 4.85
(out)(err)		 S = N/A
O = N/A
T = 8.62
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 4
T = 18.25
(out)(err)
c5_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 1.01		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 4.65
(out)(err)		 S = OPT
O = 8
T = 10.33
(out)(err)		 S = OPT
O = 8
T = 1399.50
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = 16
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 = 4.03
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 11.60
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 1.01
(out)(err)		 S = OPT
O = 8
T = 1.98
(out)(err)		 S = OPT
O = 8
T = 2.99
(out)(err)		 S = N/A
O = 92187
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 5.66
(out)(err)
c5_DD_s3_f1_e1_v2-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 1.85		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 4.85
(out)(err)		 S = OPT
O = 8
T = 9.46
(out)(err)		 S = OPT
O = 8
T = 1161.65
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = 16
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 = 4.04
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 11.15
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 1.85
(out)(err)		 S = OPT
O = 8
T = 1.87
(out)(err)		 S = OPT
O = 8
T = 2.79
(out)(err)		 S = N/A
O = 92157
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 5.64
(out)(err)
c6_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 1.58		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 4.99
(out)(err)		 S = OPT
O = 8
T = 14.15
(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 = 753
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 = 8.47
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 3.28
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 1.58
(out)(err)		 S = OPT
O = 8
T = 5.45
(out)(err)		 S = OPT
O = 8
T = 4.29
(out)(err)		 S = N/A
O = 789361
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 8.53
(out)(err)
divider-problem.dimacs_11.filtered.cnf S = OPT
O = 2
T = 46.54		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 210.61
(out)(err)		 S = N/A
O = 2
T = 796.05
(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 = 374
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 = 261.07
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 3.26
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 46.54
(out)(err)		 S = OPT
O = 2
T = 85.58
(out)(err)		 S = OPT
O = 2
T = 302.57
(out)(err)		 S = N/A
O = 708707
T = 24.86
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 766.47
(out)(err)
divider-problem.dimacs_2.filtered.cnf S = OPT
O = 2
T = 217.04		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 217.04
(out)(err)		 S = N/A
O = 28
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 = 215
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 = 650.77
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 3.40
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 4
T = 205.82
(out)(err)		 S = N/A
O = 3
T = TO
(out)(err)		 S = OPT
O = 2
T = 434.05
(out)(err)		 S = N/A
O = 749973
T = 25.70
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 660.24
(out)(err)
divider-problem.dimacs_5.filtered.cnf S = OPT
O = 2
T = 48.21		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 919.26
(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 = 49
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 = 48.21
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 4.82
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 205.24
(out)(err)		 S = OPT
O = 2
T = 196.20
(out)(err)		 S = OPT
O = 2
T = 459.83
(out)(err)		 S = N/A
O = 749972
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 1798.31
(out)(err)
divider-problem.dimacs_8.filtered.cnf S = OPT
O = 2
T = 17.31		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 35.40
(out)(err)		 S = N/A
O = 2
T = 1604.51
(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 = 229
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 = 268.66
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 3.62
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 17.31
(out)(err)		 S = OPT
O = 2
T = 22.21
(out)(err)		 S = OPT
O = 2
T = 652.84
(out)(err)		 S = N/A
O = 809321
T = 24.70
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 119.08
(out)(err)
dividers10.dimacs.filtered.cnf S = OPT
O = 2
T = 4.91		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 4.91
(out)(err)		 S = OPT
O = 2
T = 281.20
(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 = 285
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 = OPT
O = 2
T = 33.26
(out)(err)		 S = N/A
O = N/A
T = 0.06
(out)(err)		 S = N/A
O = N/A
T = 1.04
(out)(err)		 S = N/A
O = N/A
T = 0.07
(out)(err)		 S = OPT
O = 2
T = 5.48
(out)(err)		 S = OPT
O = 2
T = 5.55
(out)(err)		 S = OPT
O = 2
T = 26.73
(out)(err)		 S = N/A
O = 24836
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 10.46
(out)(err)
dividers_multivec1.dimacs.filtered.cnf S = OPT
O = 2
T = 1.67		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 4.34
(out)(err)		 S = OPT
O = 2
T = 6.67
(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 = 919
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 = 4.45
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 2.84
(out)(err)		 S = N/A
O = N/A
T = 0.19
(out)(err)		 S = OPT
O = 2
T = 4.11
(out)(err)		 S = OPT
O = 2
T = 5.56
(out)(err)		 S = OPT
O = 2
T = 1.67
(out)(err)		 S = N/A
O = 58962
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 4.86
(out)(err)
fpu_multivec1-problem.dimacs_14.filtered.cnf S = OPT
O = 2
T = 2.33		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 3.82
(out)(err)		 S = OPT
O = 2
T = 13.58
(out)(err)		 S = OPT
O = 2
T = 6.95
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = 2329
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 = 4.66
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 4.61
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 2.33
(out)(err)		 S = OPT
O = 2
T = 3.76
(out)(err)		 S = OPT
O = 2
T = 3.64
(out)(err)		 S = N/A
O = 927922
T = 12.63
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 11.15
(out)(err)
i2c-problem.dimacs_25.filtered.cnf S = OPT
O = 2
T = 35.47		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 241.12
(out)(err)		 S = OPT
O = 2
T = 35.47
(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 = 661
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 = 293.28
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 4.57
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 8
T = 1226.20
(out)(err)		 S = N/A
O = 6
T = 16.00
(out)(err)		 S = OPT
O = 2
T = 42.36
(out)(err)		 S = N/A
O = N/A
T = 6.83
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
i2c-problem.dimacs_26.filtered.cnf S = OPT
O = 2
T = 182.44		 S = N/A
O = N/A
T = 5.21
(out)(err)		 S = OPT
O = 2
T = 324.19
(out)(err)		 S = N/A
O = 3
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 = 550
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 = 944.55
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 3.50
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 4
T = TO
(out)(err)		 S = N/A
O = 4
T = 4.33
(out)(err)		 S = OPT
O = 2
T = 182.44
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 1195.70
(out)(err)
mem_ctrl-problem.dimacs_27.filtered.cnf S = OPT
O = 1
T = 70.55		 S = N/A
O = N/A
T = 18.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 = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 4.61
(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 = 70.55
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 23.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 = 6.28
(out)(err)		 S = N/A
O = N/A
T = 19.87
(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)
mem_ctrl1.dimacs.filtered.cnf S = OPT
O = 1
T = 6.30		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 1
T = 6.30
(out)(err)		 S = OPT
O = 1
T = 45.81
(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 = 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 = 17.27
(out)(err)		 S = N/A
O = N/A
T = 0.18
(out)(err)		 S = N/A
O = N/A
T = 11.66
(out)(err)		 S = N/A
O = N/A
T = 1.19
(out)(err)		 S = OPT
O = 1
T = 6.71
(out)(err)		 S = OPT
O = 1
T = 7.97
(out)(err)		 S = OPT
O = 1
T = 9.36
(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 = 10.25
(out)(err)
mem_ctrl2_blackbox_mc_dp-problem.dimacs_28.filtered.cnf S = OPT
O = 3
T = 27.98		 S = N/A
O = N/A
T = 10.16
(out)(err)		 S = OPT
O = 3
T = 321.34
(out)(err)		 S = N/A
O = N/A
T = 39.06
(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 = 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 = 3
T = 70.23
(out)(err)		 S = N/A
O = N/A
T = 0.24
(out)(err)		 S = N/A
O = N/A
T = 29.27
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 3
T = 27.98
(out)(err)		 S = OPT
O = 3
T = 77.03
(out)(err)		 S = OPT
O = 3
T = 29.60
(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 = 5.84
(out)(err)
mrisc_mem2wire-problem.dimacs_29.filtered.cnf S = OPT
O = 1
T = 6.46		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 1
T = 8.55
(out)(err)		 S = OPT
O = 1
T = 39.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 = 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 = 13.59
(out)(err)		 S = N/A
O = N/A
T = 0.09
(out)(err)		 S = N/A
O = N/A
T = 12.02
(out)(err)		 S = N/A
O = N/A
T = 19.84
(out)(err)		 S = OPT
O = 1
T = 6.46
(out)(err)		 S = OPT
O = 1
T = 11.19
(out)(err)		 S = OPT
O = 1
T = 6.90
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 1
T = 35.99
(out)(err)
rsdecoder-problem.dimacs_31.filtered.cnf S = OPT
O = 1
T = 301.13		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 817
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 = 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 = 0.13
(out)(err)		 S = N/A
O = N/A
T = 10.72
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 21
T = TO
(out)(err)		 S = N/A
O = 21
T = TO
(out)(err)		 S = OPT
O = 1
T = 301.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)
rsdecoder-problem.dimacs_36.filtered.cnf S = OPT
O = 1
T = 5.86		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 679
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 = 13.95
(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 = 741.61
(out)(err)		 S = N/A
O = N/A
T = 0.13
(out)(err)		 S = N/A
O = N/A
T = 11.95
(out)(err)		 S = N/A
O = N/A
T = 23.89
(out)(err)		 S = OPT
O = 1
T = 5.86
(out)(err)		 S = OPT
O = 1
T = 57.22
(out)(err)		 S = OPT
O = 1
T = 9.94
(out)(err)		 S = N/A
O = N/A
T = 10.51
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder-problem.dimacs_37.filtered.cnf S = OPT
O = 1
T = 17.62		 S = N/A
O = N/A
T = 7.68
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 692
T = 75.48
(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 = 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 = 0.17
(out)(err)		 S = N/A
O = N/A
T = 17.38
(out)(err)		 S = N/A
O = N/A
T = 26.96
(out)(err)		 S = N/A
O = 1
T = 265.26
(out)(err)		 S = OPT
O = 1
T = 17.62
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 8.06
(out)(err)		 S = N/A
O = N/A
T = TO
(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 = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 1025
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 = 13.82
(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 = 0.13
(out)(err)		 S = N/A
O = N/A
T = 11.14
(out)(err)		 S = N/A
O = N/A
T = 23.21
(out)(err)		 S = N/A
O = 48
T = TO
(out)(err)		 S = N/A
O = 965
T = TO
(out)(err)		 S = N/A
O = N/A
T = 860.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 = N/A
T = TO
(out)(err)
rsdecoder-problem.dimacs_39.filtered.cnf S = OPT
O = 1
T = 6.86		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 3199
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 = 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 = 195.70
(out)(err)		 S = N/A
O = N/A
T = 0.20
(out)(err)		 S = N/A
O = N/A
T = 11.74
(out)(err)		 S = N/A
O = N/A
T = 25.03
(out)(err)		 S = OPT
O = 1
T = 6.86
(out)(err)		 S = OPT
O = 1
T = 10.31
(out)(err)		 S = OPT
O = 1
T = 63.27
(out)(err)		 S = N/A
O = N/A
T = 8.68
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder-problem.dimacs_40.filtered.cnf S = OPT
O = 1
T = 42.34		 S = N/A
O = N/A
T = 6.87
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 472
T = 62.45
(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 = 14.20
(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 = 0.12
(out)(err)		 S = N/A
O = N/A
T = 11.43
(out)(err)		 S = N/A
O = N/A
T = 24.85
(out)(err)		 S = OPT
O = 1
T = 42.34
(out)(err)		 S = N/A
O = 3
T = 6.95
(out)(err)		 S = OPT
O = 1
T = 148.33
(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 = 875.40
(out)(err)
rsdecoder-problem.dimacs_41.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 83
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 = 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 = 0.14
(out)(err)		 S = N/A
O = N/A
T = 10.92
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 15
T = TO
(out)(err)		 S = N/A
O = 64
T = TO
(out)(err)		 S = N/A
O = N/A
T = 302.96
(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)
rsdecoder1_blackbox_CSEEblock-problem.dimacs_32.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 4
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 = 60
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 = 6.10
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 5
T = TO
(out)(err)		 S = N/A
O = 5
T = TO
(out)(err)		 S = N/A
O = N/A
T = 1174.33
(out)(err)		 S = N/A
O = 804080
T = 23.59
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 1793.28
(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 = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 11
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 = 70
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 = 0.13
(out)(err)		 S = N/A
O = N/A
T = 2.98
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 478
T = TO
(out)(err)		 S = N/A
O = 174
T = TO
(out)(err)		 S = N/A
O = N/A
T = 1245.50
(out)(err)		 S = N/A
O = N/A
T = 6.63
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 1778.39
(out)(err)
rsdecoder2.dimacs.filtered.cnf S = OPT
O = 1
T = 1154.96		 S = N/A
O = N/A
T = 5.56
(out)(err)		 S = OPT
O = 1
T = 1191.53
(out)(err)		 S = N/A
O = 679
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 = 78
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 = 4.40
(out)(err)		 S = N/A
O = N/A
T = 0.50
(out)(err)		 S = N/A
O = 3
T = TO
(out)(err)		 S = N/A
O = 3477
T = TO
(out)(err)		 S = OPT
O = 1
T = 1537.21
(out)(err)		 S = N/A
O = N/A
T = 7.38
(out)(err)		 S = N/A
O = N/A
T = 179.11
(out)(err)		 S = OPT
O = 1
T = 1154.96
(out)(err)
rsdecoder4.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 521
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 = 14
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 = 4.49
(out)(err)		 S = N/A
O = N/A
T = 0.32
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 1180
T = TO
(out)(err)		 S = N/A
O = N/A
T = 1577.10
(out)(err)		 S = N/A
O = 930413
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 1782.22
(out)(err)
rsdecoder5.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 79
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 = 10
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 = 4.51
(out)(err)		 S = N/A
O = N/A
T = 0.32
(out)(err)		 S = N/A
O = 4
T = 1479.41
(out)(err)		 S = N/A
O = 4
T = 661.17
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 932422
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 1796.27
(out)(err)
rsdecoder6.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 79
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 = 7
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 = 4.56
(out)(err)		 S = N/A
O = N/A
T = 0.32
(out)(err)		 S = N/A
O = 465
T = TO
(out)(err)		 S = N/A
O = 516
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 932422
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 1782.55
(out)(err)
rsdecoder_fsm2.dimacs.filtered.cnf S = OPT
O = 2
T = 44.40		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 55.77
(out)(err)		 S = N/A
O = 2
T = 12.44
(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 = 10
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 = 182.38
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 4.07
(out)(err)		 S = N/A
O = N/A
T = 0.32
(out)(err)		 S = N/A
O = 207
T = TO
(out)(err)		 S = N/A
O = 172
T = TO
(out)(err)		 S = OPT
O = 2
T = 44.40
(out)(err)		 S = N/A
O = 932422
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 424.98
(out)(err)
rsdecoder_multivec1-problem.dimacs_33.filtered.cnf S = OPT
O = 4
T = 15.42		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 1060
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 = 180
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 = 639.70
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 5.68
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 4
T = 15.42
(out)(err)		 S = N/A
O = 66
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 8.83
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 1795.57
(out)(err)
rsdecoder_multivec1.dimacs.filtered.cnf S = OPT
O = 4
T = 144.36		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 4
T = 371.95
(out)(err)		 S = N/A
O = 4
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 = 22
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 = 1577.02
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 6.82
(out)(err)		 S = N/A
O = N/A
T = 0.51
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 4
T = 144.36
(out)(err)		 S = N/A
O = N/A
T = 7.37
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 1791.03
(out)(err)
wb-problem.dimacs_45.filtered.cnf S = OPT
O = 14
T = 1.28		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 14
T = 5.56
(out)(err)		 S = OPT
O = 14
T = 18.06
(out)(err)		 S = OPT
O = 14
T = 20.10
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = 855
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 = 8.72
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 5.24
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 14
T = 1.28
(out)(err)		 S = OPT
O = 14
T = 3.18
(out)(err)		 S = OPT
O = 14
T = 5.60
(out)(err)		 S = N/A
O = 796971
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 14
T = 11.89
(out)(err)
wb-problem.dimacs_46.filtered.cnf S = OPT
O = 476
T = 17.66		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 476
T = 163.96
(out)(err)		 S = OPT
O = 476
T = 295.37
(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 = 1389
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 = 173.25
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 3.39
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 476
T = 17.66
(out)(err)		 S = OPT
O = 476
T = 85.19
(out)(err)		 S = OPT
O = 476
T = 148.41
(out)(err)		 S = N/A
O = 779721
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 476
T = 351.33
(out)(err)
wb1.dimacs.filtered.cnf S = OPT
O = 218
T = 1.65		 S = OPT
O = 218
T = 61.64
(out)(err)		 S = OPT
O = 218
T = 12.59
(out)(err)		 S = OPT
O = 218
T = 19.73
(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 = 369
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 = OPT
O = 218
T = 12.28
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 2.87
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 218
T = 1.65
(out)(err)		 S = OPT
O = 218
T = 6.71
(out)(err)		 S = OPT
O = 218
T = 11.50
(out)(err)		 S = OPT
O = 218
T = 319.18
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 218
T = 27.12
(out)(err)
wb2.dimacs.filtered.cnf S = OPT
O = 588
T = 4.00		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 588
T = 38.64
(out)(err)		 S = OPT
O = 588
T = 52.34
(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 = 814
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 = OPT
O = 588
T = 218.45
(out)(err)		 S = N/A
O = N/A
T = 0.04
(out)(err)		 S = N/A
O = N/A
T = 2.99
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 588
T = 4.00
(out)(err)		 S = OPT
O = 588
T = 16.94
(out)(err)		 S = OPT
O = 588
T = 45.85
(out)(err)		 S = N/A
O = 593
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 588
T = 102.58
(out)(err)
wb_4m8s-problem.dimacs_47.filtered.cnf S = N/A
O = N/A
T = TO		 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 = 0.00
(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 = 0.41
(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 = 539.24
(out)(err)		 S = N/A
O = N/A
T = 5.89
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 6.13
(out)(err)
wb_4m8s-problem.dimacs_48.filtered.cnf S = OPT
O = 8
T = 36.48		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 36.48
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 13.77
(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 = 0.00
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = OPT
O = 8
T = 66.92
(out)(err)		 S = N/A
O = N/A
T = 0.29
(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 = 6.45
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 46.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 = TO
(out)(err)
wb_4m8s-problem.dimacs_49.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 10.57
(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 = 13.74
(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 = 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 = 0.33
(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 = 5.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 = 42.85
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
wb_4m8s1.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 26
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 = 938
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 = 6.69
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 29
T = TO
(out)(err)		 S = N/A
O = 47
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 7.81
(out)(err)		 S = N/A
O = N/A
T = 66.22
(out)(err)		 S = N/A
O = N/A
T = 1791.68
(out)(err)
wb_4m8s3.dimacs.filtered.cnf S = OPT
O = 8
T = 2.70		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 8.45
(out)(err)		 S = OPT
O = 8
T = 26.36
(out)(err)		 S = OPT
O = 8
T = 196.36
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = 1111
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 = 11.37
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 6.33
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 2.70
(out)(err)		 S = OPT
O = 8
T = 6.04
(out)(err)		 S = OPT
O = 8
T = 8.51
(out)(err)		 S = N/A
O = N/A
T = 9.12
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 16.47
(out)(err)
wb_4m8s4.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 230
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 = 1258
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.63
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 210
T = TO
(out)(err)		 S = N/A
O = 215
T = TO
(out)(err)		 S = N/A
O = N/A
T = 965.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 = 1786.60
(out)(err)
wb_conmax1.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 4.79
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 41
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 = 510
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 = 40
T = TO
(out)(err)		 S = N/A
O = 57
T = TO
(out)(err)		 S = N/A
O = N/A
T = 1476.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 = 1799.19
(out)(err)
wb_conmax3.dimacs.filtered.cnf S = OPT
O = 33
T = 41.91		 S = N/A
O = N/A
T = 4.95
(out)(err)		 S = OPT
O = 33
T = 49.81
(out)(err)		 S = N/A
O = 33
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 = 523
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 = 33
T = 517.98
(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 = OPT
O = 33
T = 512.37
(out)(err)		 S = OPT
O = 33
T = 41.91
(out)(err)		 S = OPT
O = 33
T = 46.23
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 33
T = 129.59
(out)(err)