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 PM2 QMaxSat-g2-ms Sat4j ShinMaxSat WMaxSatz+ WMaxSatz09 WPM1 akmaxsat akmaxsat_ls iut_rr_ls iut_rr_rv wbo1.6-cnf
rsdecoder-debug.dimacs.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 = 48.35
(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 = 8.42
(out)(err)		 S = N/A
O = N/A
T = 4.76
(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 = 5.37
(out)(err)		 S = N/A
O = N/A
T = 161.34
(out)(err)
sudoku-debug.dimacs.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 = 47.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 = 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.02
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 2.42
(out)(err)
wb-debug.dimacs.cnf S = OPT
O = 28
T = 27.50		 S = OPT
O = 28
T = 61.13
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 28.30
(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.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 = 0.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 28
T = 28.63
(out)(err)
SM_AS_TOP_buggy1.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 = N/A
T = 32.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 = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 81.73
(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 = N/A
T = 0.00
(out)(err)		 S = N/A
O = 5349
T = TO
(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 = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 49.61
(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.52
(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 = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
SM_RX_TOP.dimacs.filtered.cnf S = OPT
O = 6
T = 48.96		 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 = 15.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 = N/A
T = 0.00
(out)(err)		 S = OPT
O = 6
T = 48.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 = 0.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
b15-bug-fourvec-gate-0.dimacs.seq.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 = 43.33
(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 = 0.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
c1_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 8.23		 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 = 49.18
(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 = 11.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 = 0.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 4
T = 8.23
(out)(err)
c2_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 15.50		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 25
T = 5.87
(out)(err)		 S = N/A
O = N/A
T = 48.07
(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 = 19.21
(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.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 4
T = 15.50
(out)(err)
c4_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.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 = 40.16
(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 = 3.67
(out)(err)		 S = N/A
O = N/A
T = 3.94
(out)(err)		 S = N/A
O = N/A
T = 0.01
(out)(err)		 S = N/A
O = N/A
T = 4.23
(out)(err)		 S = N/A
O = N/A
T = 3.23
(out)(err)
c4_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 15.82		 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.21
(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.34
(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.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 4
T = 15.82
(out)(err)
c5_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 8.18		 S = OPT
O = 8
T = 22.76
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 16
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 = 10.47
(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 = OPT
O = 8
T = 8.18
(out)(err)
c5_DD_s3_f1_e1_v2-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 8.16		 S = OPT
O = 8
T = 23.03
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 16
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 = 9.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 = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 8.16
(out)(err)
c6_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 12.32		 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.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 = 0.00
(out)(err)		 S = OPT
O = 8
T = 16.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 = 0.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 8
T = 12.32
(out)(err)
divider-problem.dimacs_11.filtered.cnf S = OPT
O = 2
T = 472.20		 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.18
(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 = 31.89
(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.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 472.20
(out)(err)
divider-problem.dimacs_2.filtered.cnf S = OPT
O = 2
T = 405.46		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 8
T = 5.50
(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 = OPT
O = 2
T = 405.46
(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 = OPT
O = 2
T = 681.62
(out)(err)
divider-problem.dimacs_5.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 = 13.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 = 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 = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
divider-problem.dimacs_8.filtered.cnf S = OPT
O = 2
T = 114.38		 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 = 18.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 = 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 = OPT
O = 2
T = 114.38
(out)(err)
dividers10.dimacs.filtered.cnf S = OPT
O = 2
T = 8.71		 S = OPT
O = 2
T = 139.57
(out)(err)		 S = OPT
O = 2
T = 130.52
(out)(err)		 S = N/A
O = 4
T = TO
(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 = 2
T = 36.26
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 1762
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = 1762
T = TO
(out)(err)		 S = OPT
O = 2
T = 8.71
(out)(err)
dividers_multivec1.dimacs.filtered.cnf S = OPT
O = 2
T = 6.65		 S = OPT
O = 2
T = 17.59
(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 = 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 = 9.19
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = 5642
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.00
(out)(err)		 S = N/A
O = 5642
T = TO
(out)(err)		 S = OPT
O = 2
T = 6.65
(out)(err)
fpu_multivec1-problem.dimacs_14.filtered.cnf S = OPT
O = 2
T = 7.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 = N/A
T = 60.78
(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.49
(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.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 7.13
(out)(err)
i2c-problem.dimacs_25.filtered.cnf S = OPT
O = 2
T = 859.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 = N/A
T = 53.55
(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 = 859.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.01
(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 = 1563.44		 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 = 50.16
(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 = 1571.68
(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.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 1563.44
(out)(err)
mem_ctrl-problem.dimacs_27.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 11.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 2.30
(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.13
(out)(err)		 S = N/A
O = N/A
T = 23.03
(out)(err)		 S = N/A
O = N/A
T = 24.95
(out)(err)		 S = N/A
O = N/A
T = 0.07
(out)(err)		 S = N/A
O = N/A
T = 27.08
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
mem_ctrl1.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 = N/A
T = 44.27
(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 = 11.42
(out)(err)		 S = N/A
O = N/A
T = 7.98
(out)(err)		 S = N/A
O = N/A
T = 8.81
(out)(err)		 S = N/A
O = N/A
T = 0.02
(out)(err)		 S = N/A
O = N/A
T = 9.38
(out)(err)		 S = N/A
O = N/A
T = TO
(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 = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 34.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 = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 12.29
(out)(err)		 S = N/A
O = N/A
T = 12.70
(out)(err)		 S = N/A
O = N/A
T = 13.72
(out)(err)		 S = N/A
O = N/A
T = 0.03
(out)(err)		 S = N/A
O = N/A
T = 14.45
(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 = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 47.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 = N/A
O = N/A
T = 10.11
(out)(err)		 S = N/A
O = N/A
T = 5.91
(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 = 6.71
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder-problem.dimacs_31.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 = 76.85
(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.05
(out)(err)		 S = N/A
O = N/A
T = 7.43
(out)(err)		 S = N/A
O = N/A
T = 0.02
(out)(err)		 S = N/A
O = N/A
T = 8.34
(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 = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 50.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 = 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.68
(out)(err)		 S = N/A
O = N/A
T = 0.03
(out)(err)		 S = N/A
O = N/A
T = 8.55
(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 = 11.41
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 42.24
(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.14
(out)(err)		 S = N/A
O = N/A
T = 9.21
(out)(err)		 S = N/A
O = N/A
T = 9.56
(out)(err)		 S = N/A
O = N/A
T = 0.03
(out)(err)		 S = N/A
O = N/A
T = 10.39
(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 = 10.78
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 44.77
(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.04
(out)(err)		 S = N/A
O = N/A
T = 7.53
(out)(err)		 S = N/A
O = N/A
T = 0.01
(out)(err)		 S = N/A
O = N/A
T = 8.33
(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 = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 46.54
(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.19
(out)(err)		 S = N/A
O = N/A
T = 7.38
(out)(err)		 S = N/A
O = N/A
T = 0.02
(out)(err)		 S = N/A
O = N/A
T = 8.42
(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 = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 46.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 = 12.46
(out)(err)		 S = N/A
O = N/A
T = 7.27
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.02
(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_41.filtered.cnf S = N/A
O = N/A
T = TO		 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 = N/A
T = 46.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 = N/A
T = 0.00
(out)(err)		 S = N/A
O = N/A
T = 11.94
(out)(err)		 S = N/A
O = N/A
T = 7.01
(out)(err)		 S = N/A
O = N/A
T = 7.36
(out)(err)		 S = N/A
O = N/A
T = 0.02
(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 = N/A
T = 48.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 = 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 = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(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 = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 52.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 = TO
(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 = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder2.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 = N/A
T = 66.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 = 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 = 0.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(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 = N/A
T = 17.55
(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 = 502.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 = 0.01
(out)(err)		 S = N/A
O = N/A
T = TO
(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 = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 21.27
(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 = 442.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 = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(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 = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 23.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 = N/A
O = N/A
T = 504.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 = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
rsdecoder_fsm2.dimacs.filtered.cnf S = OPT
O = 2
T = 178.29		 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 = 17.88
(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 = 0.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 2
T = 178.29
(out)(err)
rsdecoder_multivec1-problem.dimacs_33.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 7.06
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 15.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 = 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 = 4.92
(out)(err)		 S = N/A
O = N/A
T = 0.01
(out)(err)		 S = N/A
O = N/A
T = 5.18
(out)(err)		 S = N/A
O = N/A
T = 2.99
(out)(err)
rsdecoder_multivec1.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 = N/A
T = 48.38
(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 = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
wb-problem.dimacs_45.filtered.cnf S = OPT
O = 14
T = 13.56		 S = OPT
O = 14
T = 37.83
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 53.52
(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 = 21.92
(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.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 14
T = 13.56
(out)(err)
wb-problem.dimacs_46.filtered.cnf S = OPT
O = 476
T = 371.41		 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 = 64.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 = N/A
T = 0.00
(out)(err)		 S = OPT
O = 476
T = 472.95
(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 = OPT
O = 476
T = 371.41
(out)(err)
wb1.dimacs.filtered.cnf S = OPT
O = 218
T = 36.27		 S = OPT
O = 218
T = 89.88
(out)(err)		 S = N/A
O = 404
T = 3.24
(out)(err)		 S = N/A
O = 453
T = TO
(out)(err)		 S = N/A
O = 2725
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 = 36.44
(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 = N/A
T = 0.00
(out)(err)		 S = N/A
O = 1421
T = TO
(out)(err)		 S = OPT
O = 218
T = 36.27
(out)(err)
wb2.dimacs.filtered.cnf S = OPT
O = 588
T = 116.80		 S = OPT
O = 588
T = 261.81
(out)(err)		 S = N/A
O = 812
T = 3.38
(out)(err)		 S = N/A
O = 802
T = TO
(out)(err)		 S = N/A
O = 2725
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 = 113.77
(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 = N/A
T = 0.00
(out)(err)		 S = N/A
O = 1974
T = TO
(out)(err)		 S = OPT
O = 588
T = 116.80
(out)(err)
wb_4m8s-problem.dimacs_47.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 11.05
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 25.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 = N/A
O = N/A
T = 12.06
(out)(err)		 S = N/A
O = N/A
T = 15.09
(out)(err)		 S = N/A
O = N/A
T = 16.71
(out)(err)		 S = N/A
O = N/A
T = 0.04
(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_48.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 10.97
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 18.63
(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.07
(out)(err)		 S = N/A
O = N/A
T = 16.04
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 0.04
(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 = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = 24.03
(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.09
(out)(err)		 S = N/A
O = N/A
T = 15.73
(out)(err)		 S = N/A
O = N/A
T = 17.01
(out)(err)		 S = N/A
O = N/A
T = 0.04
(out)(err)		 S = N/A
O = N/A
T = 18.02
(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 = N/A
T = 54.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 = 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 = 0.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
wb_4m8s3.dimacs.filtered.cnf S = OPT
O = 8
T = 29.31		 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 = 54.88
(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 = 29.31
(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.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(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 = N/A
T = 49.24
(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 = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
wb_conmax1.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 = N/A
T = 40.88
(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 = 0.00
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)
wb_conmax3.dimacs.filtered.cnf S = OPT
O = 33
T = 118.70		 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 = 54.71
(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 = 88.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 = 0.01
(out)(err)		 S = N/A
O = N/A
T = TO
(out)(err)		 S = OPT
O = 33
T = 118.70
(out)(err)