Max-SAT (Industrial)

LabelMeaning
SSolution {OPTIMUM FOUND or OPTIMUM | UNSATISFIABLE or UNSAT | UNKNOWN | Not available or N/A}
OBest solution found
TCPU time

ColorMeaning
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 IncMaxsatz MSUnCore SAT4J-Maxsat WMaxSatz-1.6 WMaxSatz-2.5 pm2 wbo wpm1
ac97_ctrl-debug.dimacs.cnf S = N/A | O = N/A
T = 0.32 | (out)(err)
S = OPTIMUM | O = 1
T = 10.66 | (out)(err)
S = N/A | O = N/A
T = 3.72 | (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 = OPTIMUM | O = 1
T = 10.28 | (out)(err)
S = OPTIMUM | O = 1
T = 1.75 | (out)(err)
S = OPTIMUM | O = 1
T = 10.35 | (out)(err)
divider-debug.dimacs.cnf S = N/A | O = N/A
T = 0.89 | (out)(err)
S = OPTIMUM | O = 1
T = 9.42 | (out)(err)
S = OPTIMUM | O = 1
T = 12.24 | (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 = OPTIMUM | O = 1
T = 10.47 | (out)(err)
S = OPTIMUM | O = 1
T = 3.97 | (out)(err)
S = OPTIMUM | O = 1
T = 9.74 | (out)(err)
mem_ctrl-debug.dimacs.cnf S = N/A | O = N/A
T = 0.80 | (out)(err)
S = OPTIMUM | O = 1
T = 7.61 | (out)(err)
S = OPTIMUM | O = 1
T = 54.51 | (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 = OPTIMUM | O = 1
T = 10.43 | (out)(err)
S = OPTIMUM | O = 1
T = 1.77 | (out)(err)
S = OPTIMUM | O = 1
T = 10.77 | (out)(err)
mrisc-debug.dimacs.cnf S = N/A | O = N/A
T = 1.16 | (out)(err)
S = OPTIMUM | O = 1
T = 20.07 | (out)(err)
S = N/A | O = N/A
T = 12.76 | (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 = 4.17 | (out)(err)
S = OPTIMUM | O = 1
T = 9.21 | (out)(err)
S = N/A | O = N/A
T = 4.22 | (out)(err)
rsdecoder-debug.dimacs.cnf S = N/A | O = N/A
T = 1.12 | (out)(err)
S = N/A | O = N/A
T = 13.91 | (out)(err)
S = N/A | O = N/A
T = 11.27 | (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 = 4.96 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 5.02 | (out)(err)
spi-debug.dimacs.cnf S = N/A | O = N/A
T = 1.11 | (out)(err)
S = OPTIMUM | O = 1
T = 26.14 | (out)(err)
S = N/A | O = N/A
T = 12.86 | (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 = 4.56 | (out)(err)
S = OPTIMUM | O = 1
T = 1372.22 | (out)(err)
S = N/A | O = N/A
T = 4.38 | (out)(err)
sudoku-debug.dimacs.cnf S = N/A | O = N/A
T = 1.24 | (out)(err)
S = OPTIMUM | O = 1
T = 25.69 | (out)(err)
S = N/A | O = N/A
T = 17.09 | (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 = 3.71 | (out)(err)
S = OPTIMUM | O = 1
T = 12.27 | (out)(err)
S = N/A | O = N/A
T = 3.81 | (out)(err)
vga-debug.dimacs.cnf S = N/A | O = N/A
T = 1.03 | (out)(err)
S = OPTIMUM | O = 1
T = 13.19 | (out)(err)
S = N/A | O = N/A
T = 15.42 | (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 = OPTIMUM | O = 1
T = 18.81 | (out)(err)
S = OPTIMUM | O = 1
T = 3.27 | (out)(err)
S = OPTIMUM | O = 1
T = 17.00 | (out)(err)
wb-debug.dimacs.cnf S = N/A | O = N/A
T = 0.84 | (out)(err)
S = OPTIMUM | O = 28
T = 27.31 | (out)(err)
S = N/A | O = N/A
T = 10.53 | (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 = OPTIMUM | O = 28
T = 51.62 | (out)(err)
S = OPTIMUM | O = 28
T = 26.58 | (out)(err)
S = OPTIMUM | O = 28
T = 49.77 | (out)(err)
SM_AS_TOP_buggy1.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.90 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = 84
T = 19.67 | (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 = 121.10 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
SM_MAIN_MEM_buggy1.dimacs.filtered.cnf S = N/A | O = N/A
T = 1.12 | (out)(err)
S = N/A | O = N/A
T = 11.83 | (out)(err)
S = N/A | O = N/A
T = 9.87 | (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 = 6.21 | (out)(err)
S = N/A | O = N/A
T = 4.56 | (out)(err)
S = N/A | O = N/A
T = 6.06 | (out)(err)
SM_RX_TOP.dimacs.filtered.cnf S = N/A | O = N/A
T = 1.00 | (out)(err)
S = OPTIMUM | O = 6
T = 38.07 | (out)(err)
S = N/A | O = N/A
T = 15.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 = Time Out | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = OPTIMUM | O = 6
T = 89.44 | (out)(err)
b14_opt_bug2_vec1-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.58 | (out)(err)
S = OPTIMUM | O = 1
T = 9.97 | (out)(err)
S = OPTIMUM | O = 1
T = 6.26 | (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 = OPTIMUM | O = 1
T = 10.36 | (out)(err)
S = OPTIMUM | O = 1
T = 1.28 | (out)(err)
S = OPTIMUM | O = 1
T = 9.38 | (out)(err)
b15-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.90 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 24.26 | (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 = 4.00 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 3.96 | (out)(err)
b15-bug-onevec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.52 | (out)(err)
S = OPTIMUM | O = 1
T = 14.35 | (out)(err)
S = OPTIMUM | O = 1
T = 5.99 | (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 = 1.37 | (out)(err)
S = OPTIMUM | O = 1
T = 829.44 | (out)(err)
S = OPTIMUM | O = 1
T = 15.66 | (out)(err)
c1_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.78 | (out)(err)
S = OPTIMUM | O = 4
T = 12.57 | (out)(err)
S = N/A | O = N/A
T = 11.57 | (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 = OPTIMUM | O = 4
T = 22.70 | (out)(err)
S = OPTIMUM | O = 4
T = 6.80 | (out)(err)
S = OPTIMUM | O = 4
T = 22.20 | (out)(err)
c1_DD_s3_f1_e2_v1-bug-onevec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.36 | (out)(err)
S = OPTIMUM | O = 1
T = 1.98 | (out)(err)
S = OPTIMUM | O = 1
T = 4.19 | (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 = OPTIMUM | O = 1
T = 3.49 | (out)(err)
S = OPTIMUM | O = 1
T = 0.69 | (out)(err)
S = OPTIMUM | O = 1
T = 3.87 | (out)(err)
c2_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.85 | (out)(err)
S = OPTIMUM | O = 4
T = 22.33 | (out)(err)
S = N/A | O = N/A
T = 11.07 | (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 = 3.96 | (out)(err)
S = OPTIMUM | O = 4
T = 18.58 | (out)(err)
S = N/A | O = N/A
T = 4.28 | (out)(err)
c2_DD_s3_f1_e2_v1-bug-onevec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.36 | (out)(err)
S = OPTIMUM | O = 1
T = 3.64 | (out)(err)
S = N/A | O = 3
T = Time Out | (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 = OPTIMUM | O = 1
T = 10.54 | (out)(err)
S = OPTIMUM | O = 1
T = 1.22 | (out)(err)
S = OPTIMUM | O = 1
T = 6.46 | (out)(err)
c3_DD_s3_f1_e1_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.14 | (out)(err)
S = OPTIMUM | O = 4
T = 1.02 | (out)(err)
S = N/A | O = 4
T = Time Out | (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 = OPTIMUM | O = 4
T = 2.08 | (out)(err)
S = OPTIMUM | O = 4
T = 0.62 | (out)(err)
S = OPTIMUM | O = 4
T = 1.96 | (out)(err)
c3_DD_s3_f1_e1_v1-bug-onevec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = Time Out | (out)(err)
S = OPTIMUM | O = 1
T = 0.14 | (out)(err)
S = OPTIMUM | O = 1
T = 1.54 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = OPTIMUM | O = 1
T = 0.27 | (out)(err)
S = OPTIMUM | O = 1
T = 0.05 | (out)(err)
S = OPTIMUM | O = 1
T = 0.27 | (out)(err)
c4_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.96 | (out)(err)
S = OPTIMUM | O = 8
T = 40.98 | (out)(err)
S = N/A | O = N/A
T = 10.70 | (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 = Time Out | (out)(err)
S = OPTIMUM | O = 8
T = 29.02 | (out)(err)
S = N/A | O = N/A
T = 4.70 | (out)(err)
c4_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.83 | (out)(err)
S = OPTIMUM | O = 4
T = 15.72 | (out)(err)
S = N/A | O = N/A
T = 10.19 | (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 = 14.27 | (out)(err)
S = OPTIMUM | O = 4
T = 14.56 | (out)(err)
S = N/A | O = N/A
T = 15.14 | (out)(err)
c4_DD_s3_f1_e2_v1-bug-onevec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.45 | (out)(err)
S = OPTIMUM | O = 1
T = 2.76 | (out)(err)
S = OPTIMUM | O = 1
T = 5.14 | (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 = OPTIMUM | O = 1
T = 5.08 | (out)(err)
S = OPTIMUM | O = 1
T = 1.60 | (out)(err)
S = OPTIMUM | O = 1
T = 5.03 | (out)(err)
c5315-bug-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = Time Out | (out)(err)
S = OPTIMUM | O = 1
T = 0.03 | (out)(err)
S = OPTIMUM | O = 1
T = 1.60 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = OPTIMUM | O = 1
T = 0.05 | (out)(err)
S = OPTIMUM | O = 1
T = 0.01 | (out)(err)
S = OPTIMUM | O = 1
T = 0.05 | (out)(err)
c5_DD_s3_f1_e1_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.41 | (out)(err)
S = OPTIMUM | O = 4
T = 3.41 | (out)(err)
S = N/A | O = 4
T = Time Out | (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 = OPTIMUM | O = 4
T = 6.28 | (out)(err)
S = OPTIMUM | O = 4
T = 1.91 | (out)(err)
S = OPTIMUM | O = 4
T = 6.34 | (out)(err)
c5_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.70 | (out)(err)
S = OPTIMUM | O = 8
T = 10.23 | (out)(err)
S = N/A | O = 8
T = Time Out | (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 = OPTIMUM | O = 8
T = 19.47 | (out)(err)
S = OPTIMUM | O = 8
T = 7.02 | (out)(err)
S = OPTIMUM | O = 8
T = 20.17 | (out)(err)
c5_DD_s3_f1_e1_v1-bug-onevec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.12 | (out)(err)
S = OPTIMUM | O = 1
T = 0.55 | (out)(err)
S = OPTIMUM | O = 1
T = 2.23 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = OPTIMUM | O = 1
T = 0.93 | (out)(err)
S = OPTIMUM | O = 1
T = 0.20 | (out)(err)
S = OPTIMUM | O = 1
T = 0.97 | (out)(err)
c5_DD_s3_f1_e1_v2-bug-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.71 | (out)(err)
S = OPTIMUM | O = 8
T = 10.07 | (out)(err)
S = N/A | O = 8
T = Time Out | (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 = OPTIMUM | O = 8
T = 19.59 | (out)(err)
S = OPTIMUM | O = 8
T = 7.24 | (out)(err)
S = OPTIMUM | O = 8
T = 20.52 | (out)(err)
c6288-bug-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = Time Out | (out)(err)
S = OPTIMUM | O = 1
T = 0.82 | (out)(err)
S = N/A | O = 4
T = Time Out | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = OPTIMUM | O = 1
T = 1.81 | (out)(err)
S = OPTIMUM | O = 1
T = 0.04 | (out)(err)
S = OPTIMUM | O = 1
T = 1.82 | (out)(err)
c6_DD_s3_f1_e1_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.66 | (out)(err)
S = OPTIMUM | O = 4
T = 6.34 | (out)(err)
S = N/A | O = 4
T = Time Out | (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 = OPTIMUM | O = 4
T = 11.10 | (out)(err)
S = OPTIMUM | O = 4
T = 3.17 | (out)(err)
S = OPTIMUM | O = 4
T = 11.05 | (out)(err)
c6_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.77 | (out)(err)
S = OPTIMUM | O = 8
T = 16.75 | (out)(err)
S = N/A | O = N/A
T = 10.46 | (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 = OPTIMUM | O = 8
T = 28.96 | (out)(err)
S = OPTIMUM | O = 8
T = 10.30 | (out)(err)
S = OPTIMUM | O = 8
T = 28.11 | (out)(err)
c6_DD_s3_f1_e1_v1-bug-onevec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.17 | (out)(err)
S = OPTIMUM | O = 1
T = 0.97 | (out)(err)
S = OPTIMUM | O = 1
T = 2.12 | (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 = OPTIMUM | O = 1
T = 1.71 | (out)(err)
S = OPTIMUM | O = 1
T = 0.30 | (out)(err)
S = OPTIMUM | O = 1
T = 1.72 | (out)(err)
c6_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.66 | (out)(err)
S = OPTIMUM | O = 4
T = 7.06 | (out)(err)
S = N/A | O = 4
T = Time Out | (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 = OPTIMUM | O = 4
T = 11.70 | (out)(err)
S = OPTIMUM | O = 4
T = 3.15 | (out)(err)
S = OPTIMUM | O = 4
T = 11.78 | (out)(err)
c7552-bug-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = Time Out | (out)(err)
S = OPTIMUM | O = 1
T = 0.18 | (out)(err)
S = OPTIMUM | O = 1
T = 1.31 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = OPTIMUM | O = 1
T = 0.25 | (out)(err)
S = OPTIMUM | O = 1
T = 0.02 | (out)(err)
S = OPTIMUM | O = 1
T = 0.27 | (out)(err)
divider-problem.dimacs_1.filtered.cnf S = N/A | O = N/A
T = 0.91 | (out)(err)
S = OPTIMUM | O = 1
T = 12.49 | (out)(err)
S = N/A | O = N/A
T = 11.78 | (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 = OPTIMUM | O = 1
T = 24.57 | (out)(err)
S = OPTIMUM | O = 1
T = 315.62 | (out)(err)
S = OPTIMUM | O = 1
T = 20.73 | (out)(err)
divider-problem.dimacs_10.filtered.cnf S = N/A | O = N/A
T = 0.95 | (out)(err)
S = OPTIMUM | O = 0
T = 10.29 | (out)(err)
S = N/A | O = N/A
T = 10.73 | (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 = OPTIMUM | O = 0
T = 9.41 | (out)(err)
S = OPTIMUM | O = 0
T = 2.56 | (out)(err)
S = OPTIMUM | O = 0
T = 9.30 | (out)(err)
divider-problem.dimacs_11.filtered.cnf S = N/A | O = N/A
T = 0.93 | (out)(err)
S = OPTIMUM | O = 2
T = 212.14 | (out)(err)
S = N/A | O = N/A
T = 11.73 | (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 = 28.51 | (out)(err)
S = OPTIMUM | O = 2
T = 685.54 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
divider-problem.dimacs_12.filtered.cnf S = N/A | O = N/A
T = 0.91 | (out)(err)
S = OPTIMUM | O = 1
T = 16.93 | (out)(err)
S = N/A | O = N/A
T = 10.73 | (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 = OPTIMUM | O = 1
T = 26.55 | (out)(err)
S = OPTIMUM | O = 1
T = 22.38 | (out)(err)
S = OPTIMUM | O = 1
T = 21.43 | (out)(err)
divider-problem.dimacs_2.filtered.cnf S = N/A | O = N/A
T = 0.89 | (out)(err)
S = OPTIMUM | O = 2
T = 331.16 | (out)(err)
S = N/A | O = N/A
T = 11.07 | (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 = 14.24 | (out)(err)
S = OPTIMUM | O = 2
T = 754.96 | (out)(err)
S = OPTIMUM | O = 2
T = 199.76 | (out)(err)
divider-problem.dimacs_3.filtered.cnf S = N/A | O = N/A
T = 0.99 | (out)(err)
S = OPTIMUM | O = 1
T = 12.60 | (out)(err)
S = N/A | O = N/A
T = 16.64 | (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 = OPTIMUM | O = 1
T = 19.34 | (out)(err)
S = OPTIMUM | O = 1
T = 14.67 | (out)(err)
S = OPTIMUM | O = 1
T = 20.60 | (out)(err)
divider-problem.dimacs_4.filtered.cnf S = N/A | O = N/A
T = 0.95 | (out)(err)
S = OPTIMUM | O = 1
T = 13.90 | (out)(err)
S = N/A | O = N/A
T = 10.79 | (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 = OPTIMUM | O = 1
T = 18.28 | (out)(err)
S = OPTIMUM | O = 1
T = 47.29 | (out)(err)
S = OPTIMUM | O = 1
T = 17.69 | (out)(err)
divider-problem.dimacs_5.filtered.cnf S = N/A | O = N/A
T = 0.93 | (out)(err)
S = OPTIMUM | O = 2
T = 163.53 | (out)(err)
S = N/A | O = N/A
T = 11.33 | (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 = 35.71 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = OPTIMUM | O = 2
T = 602.72 | (out)(err)
divider-problem.dimacs_6.filtered.cnf S = N/A | O = N/A
T = 0.92 | (out)(err)
S = OPTIMUM | O = 0
T = 10.52 | (out)(err)
S = N/A | O = N/A
T = 12.36 | (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 = OPTIMUM | O = 0
T = 9.38 | (out)(err)
S = OPTIMUM | O = 0
T = 2.59 | (out)(err)
S = OPTIMUM | O = 0
T = 9.53 | (out)(err)
divider-problem.dimacs_7.filtered.cnf S = N/A | O = N/A
T = 0.92 | (out)(err)
S = OPTIMUM | O = 1
T = 12.91 | (out)(err)
S = N/A | O = N/A
T = 10.70 | (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 = OPTIMUM | O = 1
T = 25.29 | (out)(err)
S = OPTIMUM | O = 1
T = 248.69 | (out)(err)
S = OPTIMUM | O = 1
T = 24.87 | (out)(err)
divider-problem.dimacs_8.filtered.cnf S = N/A | O = N/A
T = 0.99 | (out)(err)
S = OPTIMUM | O = 2
T = 126.60 | (out)(err)
S = N/A | O = N/A
T = 12.24 | (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 = 27.83 | (out)(err)
S = OPTIMUM | O = 2
T = 121.02 | (out)(err)
S = OPTIMUM | O = 2
T = 543.22 | (out)(err)
divider-problem.dimacs_9.filtered.cnf S = N/A | O = N/A
T = 0.92 | (out)(err)
S = OPTIMUM | O = 1
T = 12.93 | (out)(err)
S = N/A | O = N/A
T = 11.58 | (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 = OPTIMUM | O = 1
T = 18.41 | (out)(err)
S = OPTIMUM | O = 1
T = 41.67 | (out)(err)
S = OPTIMUM | O = 1
T = 22.02 | (out)(err)
dividers1.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.28 | (out)(err)
S = OPTIMUM | O = 1
T = 6.78 | (out)(err)
S = OPTIMUM | O = 1
T = 3.94 | (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 = OPTIMUM | O = 1
T = 7.56 | (out)(err)
S = OPTIMUM | O = 1
T = 5.36 | (out)(err)
S = OPTIMUM | O = 1
T = 7.81 | (out)(err)
dividers10.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.29 | (out)(err)
S = OPTIMUM | O = 2
T = 35.28 | (out)(err)
S = N/A | O = 2
T = Time Out | (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 = Time Out | (out)(err)
S = OPTIMUM | O = 2
T = 9.01 | (out)(err)
S = OPTIMUM | O = 2
T = 50.89 | (out)(err)
dividers11.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.27 | (out)(err)
S = OPTIMUM | O = 1
T = 6.15 | (out)(err)
S = OPTIMUM | O = 1
T = 48.10 | (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 = OPTIMUM | O = 1
T = 7.51 | (out)(err)
S = OPTIMUM | O = 1
T = 0.74 | (out)(err)
S = OPTIMUM | O = 1
T = 8.43 | (out)(err)
dividers2.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.29 | (out)(err)
S = OPTIMUM | O = 1
T = 1.56 | (out)(err)
S = OPTIMUM | O = 1
T = 3.93 | (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 = OPTIMUM | O = 1
T = 2.85 | (out)(err)
S = OPTIMUM | O = 1
T = 0.87 | (out)(err)
S = OPTIMUM | O = 1
T = 2.38 | (out)(err)
dividers3.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.29 | (out)(err)
S = OPTIMUM | O = 1
T = 6.70 | (out)(err)
S = OPTIMUM | O = 1
T = 3.90 | (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 = OPTIMUM | O = 1
T = 7.52 | (out)(err)
S = OPTIMUM | O = 1
T = 0.66 | (out)(err)
S = OPTIMUM | O = 1
T = 8.16 | (out)(err)
dividers4.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.28 | (out)(err)
S = OPTIMUM | O = 2
T = 6.63 | (out)(err)
S = OPTIMUM | O = 2
T = 29.71 | (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 = OPTIMUM | O = 2
T = 9.29 | (out)(err)
S = OPTIMUM | O = 2
T = 1.89 | (out)(err)
S = OPTIMUM | O = 2
T = 10.64 | (out)(err)
dividers5.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.28 | (out)(err)
S = OPTIMUM | O = 1
T = 6.79 | (out)(err)
S = OPTIMUM | O = 1
T = 111.77 | (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 = OPTIMUM | O = 1
T = 7.83 | (out)(err)
S = OPTIMUM | O = 1
T = 0.93 | (out)(err)
S = OPTIMUM | O = 1
T = 7.11 | (out)(err)
dividers6_hack.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.24 | (out)(err)
S = OPTIMUM | O = 1
T = 8.42 | (out)(err)
S = OPTIMUM | O = 1
T = 3.47 | (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 = OPTIMUM | O = 1
T = 6.45 | (out)(err)
S = OPTIMUM | O = 1
T = 0.34 | (out)(err)
S = OPTIMUM | O = 1
T = 8.10 | (out)(err)
dividers7.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.40 | (out)(err)
S = OPTIMUM | O = 1
T = 4.89 | (out)(err)
S = N/A | O = 3
T = Time Out | (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 = OPTIMUM | O = 1
T = 9.28 | (out)(err)
S = OPTIMUM | O = 1
T = 12.80 | (out)(err)
S = OPTIMUM | O = 1
T = 9.78 | (out)(err)
dividers8.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.28 | (out)(err)
S = OPTIMUM | O = 1
T = 6.20 | (out)(err)
S = OPTIMUM | O = 1
T = 9.97 | (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 = OPTIMUM | O = 1
T = 7.49 | (out)(err)
S = OPTIMUM | O = 1
T = 0.77 | (out)(err)
S = OPTIMUM | O = 1
T = 8.76 | (out)(err)
dividers9.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.27 | (out)(err)
S = OPTIMUM | O = 1
T = 7.11 | (out)(err)
S = OPTIMUM | O = 1
T = 855.23 | (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 = OPTIMUM | O = 1
T = 8.08 | (out)(err)
S = OPTIMUM | O = 1
T = 1.23 | (out)(err)
S = OPTIMUM | O = 1
T = 8.84 | (out)(err)
dividers_multivec1.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.72 | (out)(err)
S = OPTIMUM | O = 2
T = 9.29 | (out)(err)
S = OPTIMUM | O = 2
T = 1567.52 | (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 = OPTIMUM | O = 2
T = 11.63 | (out)(err)
S = OPTIMUM | O = 2
T = 5.84 | (out)(err)
S = OPTIMUM | O = 2
T = 13.14 | (out)(err)
fpu1-problem.dimacs_13.filtered.cnf S = N/A | O = N/A
T = 0.75 | (out)(err)
S = OPTIMUM | O = 1
T = 6.56 | (out)(err)
S = OPTIMUM | O = 1
T = 801.21 | (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 = OPTIMUM | O = 1
T = 12.04 | (out)(err)
S = OPTIMUM | O = 1
T = 2.44 | (out)(err)
S = OPTIMUM | O = 1
T = 6.14 | (out)(err)
fpu2-problem.dimacs_16.filtered.cnf S = N/A | O = N/A
T = 0.84 | (out)(err)
S = OPTIMUM | O = 1
T = 7.89 | (out)(err)
S = OPTIMUM | O = 1
T = 14.12 | (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 = OPTIMUM | O = 1
T = 7.65 | (out)(err)
S = OPTIMUM | O = 1
T = 2.58 | (out)(err)
S = OPTIMUM | O = 1
T = 7.57 | (out)(err)
fpu3-problem.dimacs_18.filtered.cnf S = N/A | O = N/A
T = 0.71 | (out)(err)
S = OPTIMUM | O = 1
T = 6.46 | (out)(err)
S = OPTIMUM | O = 1
T = 648.41 | (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 = OPTIMUM | O = 1
T = 10.49 | (out)(err)
S = OPTIMUM | O = 1
T = 1.51 | (out)(err)
S = OPTIMUM | O = 1
T = 5.96 | (out)(err)
fpu3_hack-problem.dimacs_17.filtered.cnf S = N/A | O = N/A
T = 0.62 | (out)(err)
S = OPTIMUM | O = 1
T = 5.73 | (out)(err)
S = N/A | O = 27
T = Time Out | (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 = OPTIMUM | O = 1
T = 4.93 | (out)(err)
S = OPTIMUM | O = 1
T = 1.29 | (out)(err)
S = OPTIMUM | O = 1
T = 4.85 | (out)(err)
fpu4-problem.dimacs_19.filtered.cnf S = N/A | O = N/A
T = 0.78 | (out)(err)
S = OPTIMUM | O = 1
T = 6.65 | (out)(err)
S = OPTIMUM | O = 1
T = 1237.77 | (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 = OPTIMUM | O = 1
T = 10.42 | (out)(err)
S = OPTIMUM | O = 1
T = 1.91 | (out)(err)
S = OPTIMUM | O = 1
T = 6.66 | (out)(err)
fpu5-problem.dimacs_20.filtered.cnf S = N/A | O = N/A
T = 1.07 | (out)(err)
S = OPTIMUM | O = 1
T = 12.22 | (out)(err)
S = N/A | O = N/A
T = 11.66 | (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 = OPTIMUM | O = 1
T = 24.47 | (out)(err)
S = OPTIMUM | O = 1
T = 7.64 | (out)(err)
S = OPTIMUM | O = 1
T = 21.53 | (out)(err)
fpu6-problem.dimacs_21.filtered.cnf S = N/A | O = N/A
T = 0.91 | (out)(err)
S = OPTIMUM | O = 0
T = 7.43 | (out)(err)
S = N/A | O = 4670
T = Time Out | (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 = OPTIMUM | O = 0
T = 6.49 | (out)(err)
S = OPTIMUM | O = 0
T = 1.30 | (out)(err)
S = OPTIMUM | O = 0
T = 6.89 | (out)(err)
fpu7-problem.dimacs_22.filtered.cnf S = N/A | O = N/A
T = 0.77 | (out)(err)
S = OPTIMUM | O = 1
T = 9.38 | (out)(err)
S = OPTIMUM | O = 1
T = 14.32 | (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 = OPTIMUM | O = 1
T = 17.17 | (out)(err)
S = OPTIMUM | O = 1
T = 2.48 | (out)(err)
S = OPTIMUM | O = 1
T = 16.46 | (out)(err)
fpu7_hack-problem.dimacs_23.filtered.cnf S = N/A | O = N/A
T = 0.62 | (out)(err)
S = OPTIMUM | O = 1
T = 8.33 | (out)(err)
S = OPTIMUM | O = 1
T = 24.78 | (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 = OPTIMUM | O = 1
T = 14.86 | (out)(err)
S = OPTIMUM | O = 1
T = 2.30 | (out)(err)
S = OPTIMUM | O = 1
T = 12.75 | (out)(err)
fpu8-problem.dimacs_24.filtered.cnf S = N/A | O = N/A
T = 0.85 | (out)(err)
S = OPTIMUM | O = 1
T = 10.34 | (out)(err)
S = N/A | O = 303
T = Time Out | (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 = OPTIMUM | O = 1
T = 19.00 | (out)(err)
S = OPTIMUM | O = 1
T = 6.80 | (out)(err)
S = OPTIMUM | O = 1
T = 18.67 | (out)(err)
fpu_fsm1-problem.dimacs_15.filtered.cnf S = N/A | O = N/A
T = 0.85 | (out)(err)
S = OPTIMUM | O = 1
T = 7.89 | (out)(err)
S = N/A | O = 297
T = Time Out | (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 = OPTIMUM | O = 1
T = 10.29 | (out)(err)
S = OPTIMUM | O = 1
T = 1.96 | (out)(err)
S = OPTIMUM | O = 1
T = 10.51 | (out)(err)
fpu_multivec1-problem.dimacs_14.filtered.cnf S = N/A | O = N/A
T = 1.07 | (out)(err)
S = OPTIMUM | O = 2
T = 11.57 | (out)(err)
S = N/A | O = N/A
T = 11.03 | (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 = OPTIMUM | O = 2
T = 15.71 | (out)(err)
S = OPTIMUM | O = 2
T = 7.37 | (out)(err)
S = OPTIMUM | O = 2
T = 15.82 | (out)(err)
i2c-problem.dimacs_25.filtered.cnf S = N/A | O = N/A
T = 1.06 | (out)(err)
S = OPTIMUM | O = 2
T = 148.71 | (out)(err)
S = N/A | O = N/A
T = 11.17 | (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 = 4.14 | (out)(err)
S = OPTIMUM | O = 2
T = 1254.26 | (out)(err)
S = N/A | O = N/A
T = 4.32 | (out)(err)
i2c-problem.dimacs_26.filtered.cnf S = N/A | O = N/A
T = 1.07 | (out)(err)
S = OPTIMUM | O = 2
T = 86.04 | (out)(err)
S = N/A | O = N/A
T = 10.34 | (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 = 3.92 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 3.96 | (out)(err)
i2c_master1.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.48 | (out)(err)
S = OPTIMUM | O = 1
T = 12.85 | (out)(err)
S = N/A | O = 85
T = Time Out | (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 = 4.90 | (out)(err)
S = OPTIMUM | O = 1
T = 1.19 | (out)(err)
S = OPTIMUM | O = 1
T = 11.87 | (out)(err)
i2c_master2.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.37 | (out)(err)
S = OPTIMUM | O = 1
T = 10.96 | (out)(err)
S = OPTIMUM | O = 1
T = 111.87 | (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 = 0.85 | (out)(err)
S = OPTIMUM | O = 1
T = 5.91 | (out)(err)
S = OPTIMUM | O = 1
T = 10.65 | (out)(err)
mem_ctrl-problem.dimacs_27.filtered.cnf S = N/A | O = N/A
T = 1.04 | (out)(err)
S = N/A | O = N/A
T = 16.00 | (out)(err)
S = N/A | O = N/A
T = 2.13 | (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 = 6.21 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 5.99 | (out)(err)
mem_ctrl1.dimacs.filtered.cnf S = N/A | O = N/A
T = 1.21 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 9.53 | (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 = 5.84 | (out)(err)
S = N/A | O = N/A
T = 4.35 | (out)(err)
S = N/A | O = N/A
T = 5.75 | (out)(err)
mem_ctrl2_blackbox_mc_dp-problem.dimacs_28.filtered.cnf S = N/A | O = N/A
T = 1.01 | (out)(err)
S = N/A | O = N/A
T = 16.35 | (out)(err)
S = N/A | O = N/A
T = 2.78 | (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 = 6.28 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 6.10 | (out)(err)
mot_comb1._red-gate-0.dimacs.seq.filtered.cnf S = OPTIMUM | O = 1
T = 0.48 | (out)(err)
S = OPTIMUM | O = 1
T = 0.02 | (out)(err)
S = OPTIMUM | O = 1
T = 1.08 | (out)(err)
S = OPTIMUM | O = 1
T = 0.77 | (out)(err)
S = OPTIMUM | O = 1
T = 0.16 | (out)(err)
S = OPTIMUM | O = 1
T = 0.06 | (out)(err)
S = OPTIMUM | O = 1
T = 0.01 | (out)(err)
S = OPTIMUM | O = 1
T = 0.05 | (out)(err)
mot_comb2._red-gate-0.dimacs.seq.filtered.cnf S = OPTIMUM | O = 1
T = 6.72 | (out)(err)
S = OPTIMUM | O = 1
T = 0.08 | (out)(err)
S = OPTIMUM | O = 1
T = 1.56 | (out)(err)
S = OPTIMUM | O = 1
T = 168.61 | (out)(err)
S = OPTIMUM | O = 1
T = 11.97 | (out)(err)
S = OPTIMUM | O = 1
T = 0.17 | (out)(err)
S = OPTIMUM | O = 1
T = 0.03 | (out)(err)
S = OPTIMUM | O = 1
T = 0.16 | (out)(err)
mot_comb3._red-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.04 | (out)(err)
S = OPTIMUM | O = 1
T = 0.20 | (out)(err)
S = OPTIMUM | O = 1
T = 2.65 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = OPTIMUM | O = 1
T = 0.38 | (out)(err)
S = OPTIMUM | O = 1
T = 0.07 | (out)(err)
S = OPTIMUM | O = 1
T = 0.39 | (out)(err)
mrisc_mem2wire-problem.dimacs_29.filtered.cnf S = N/A | O = N/A
T = 1.13 | (out)(err)
S = OPTIMUM | O = 1
T = 30.58 | (out)(err)
S = N/A | O = N/A
T = 13.42 | (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 = 5.59 | (out)(err)
S = OPTIMUM | O = 1
T = 20.12 | (out)(err)
S = N/A | O = N/A
T = 5.60 | (out)(err)
mrisc_mem2wire1.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.85 | (out)(err)
S = OPTIMUM | O = 1
T = 9.73 | (out)(err)
S = OPTIMUM | O = 1
T = 43.91 | (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 = OPTIMUM | O = 1
T = 12.99 | (out)(err)
S = OPTIMUM | O = 1
T = 1.89 | (out)(err)
S = OPTIMUM | O = 1
T = 13.15 | (out)(err)
rsdecoder-problem.dimacs_31.filtered.cnf S = N/A | O = N/A
T = 1.13 | (out)(err)
S = N/A | O = N/A
T = 13.27 | (out)(err)
S = N/A | O = N/A
T = 8.26 | (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 = Time Out | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 6.54 | (out)(err)
rsdecoder-problem.dimacs_34.filtered.cnf S = N/A | O = N/A
T = 0.95 | (out)(err)
S = OPTIMUM | O = 1
T = 14.80 | (out)(err)
S = N/A | O = N/A
T = 11.88 | (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 = 3.18 | (out)(err)
S = OPTIMUM | O = 1
T = 7.09 | (out)(err)
S = OPTIMUM | O = 1
T = 27.11 | (out)(err)
rsdecoder-problem.dimacs_36.filtered.cnf S = N/A | O = N/A
T = 1.11 | (out)(err)
S = N/A | O = N/A
T = 13.05 | (out)(err)
S = N/A | O = N/A
T = 15.22 | (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 = Time Out | (out)(err)
S = N/A | O = N/A
T = 56.09 | (out)(err)
S = N/A | O = N/A
T = 6.76 | (out)(err)
rsdecoder-problem.dimacs_37.filtered.cnf S = N/A | O = N/A
T = 1.19 | (out)(err)
S = N/A | O = N/A
T = 13.44 | (out)(err)
S = N/A | O = N/A
T = 50.98 | (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 = 6.30 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 6.11 | (out)(err)
rsdecoder-problem.dimacs_38.filtered.cnf S = N/A | O = N/A
T = 1.11 | (out)(err)
S = N/A | O = N/A
T = 12.80 | (out)(err)
S = N/A | O = N/A
T = 8.41 | (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 = Time Out | (out)(err)
S = N/A | O = N/A
T = 186.01 | (out)(err)
S = N/A | O = N/A
T = 6.62 | (out)(err)
rsdecoder-problem.dimacs_39.filtered.cnf S = N/A | O = N/A
T = 1.05 | (out)(err)
S = N/A | O = N/A
T = 12.96 | (out)(err)
S = N/A | O = N/A
T = 8.09 | (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 = 6.63 | (out)(err)
S = N/A | O = N/A
T = 289.19 | (out)(err)
S = N/A | O = N/A
T = 6.42 | (out)(err)
rsdecoder-problem.dimacs_40.filtered.cnf S = N/A | O = N/A
T = 1.12 | (out)(err)
S = N/A | O = N/A
T = 12.89 | (out)(err)
S = N/A | O = N/A
T = 8.10 | (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 = 6.74 | (out)(err)
S = N/A | O = N/A
T = 185.78 | (out)(err)
S = N/A | O = N/A
T = 6.50 | (out)(err)
rsdecoder-problem.dimacs_41.filtered.cnf S = N/A | O = N/A
T = 1.18 | (out)(err)
S = N/A | O = N/A
T = 13.75 | (out)(err)
S = N/A | O = N/A
T = 18.75 | (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 = Time Out | (out)(err)
S = N/A | O = N/A
T = 26.87 | (out)(err)
S = N/A | O = N/A
T = 6.54 | (out)(err)
rsdecoder1.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.98 | (out)(err)
S = OPTIMUM | O = 1
T = 35.39 | (out)(err)
S = N/A | O = N/A
T = 10.98 | (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 = OPTIMUM | O = 1
T = 40.85 | (out)(err)
S = OPTIMUM | O = 1
T = 36.37 | (out)(err)
S = OPTIMUM | O = 1
T = 45.80 | (out)(err)
rsdecoder1_blackbox_CSEEblock-problem.dimacs_32.filtered.cnf S = N/A | O = N/A
T = 0.98 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 12.97 | (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 = Time Out | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
rsdecoder1_blackbox_KESblock-problem.dimacs_30.filtered.cnf S = N/A | O = N/A
T = 1.01 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 10.01 | (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 = 15.67 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 16.08 | (out)(err)
rsdecoder2.dimacs.filtered.cnf S = N/A | O = N/A
T = 1.15 | (out)(err)
S = N/A | O = N/A
T = 14.54 | (out)(err)
S = N/A | O = N/A
T = 11.27 | (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 = 4.53 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 4.33 | (out)(err)
rsdecoder2_blackbox-problem.dimacs_35.filtered.cnf S = N/A | O = N/A
T = 0.98 | (out)(err)
S = OPTIMUM | O = 0
T = 134.50 | (out)(err)
S = N/A | O = N/A
T = 16.66 | (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 = Time Out | (out)(err)
S = OPTIMUM | O = 0
T = 428.79 | (out)(err)
S = N/A | O = N/A
T = 5.38 | (out)(err)
rsdecoder3.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.98 | (out)(err)
S = OPTIMUM | O = 1
T = 29.08 | (out)(err)
S = N/A | O = N/A
T = 11.04 | (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.76 | (out)(err)
S = OPTIMUM | O = 1
T = 544.58 | (out)(err)
S = OPTIMUM | O = 1
T = 107.31 | (out)(err)
rsdecoder4.dimacs.filtered.cnf S = N/A | O = N/A
T = 1.11 | (out)(err)
S = N/A | O = N/A
T = 183.19 | (out)(err)
S = N/A | O = N/A
T = 11.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 = 14.03 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
rsdecoder5.dimacs.filtered.cnf S = N/A | O = N/A
T = 1.02 | (out)(err)
S = N/A | O = N/A
T = 181.08 | (out)(err)
S = N/A | O = N/A
T = 11.44 | (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.43 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
rsdecoder6.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.96 | (out)(err)
S = N/A | O = N/A
T = 245.41 | (out)(err)
S = N/A | O = N/A
T = 11.30 | (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.88 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
rsdecoder_fsm1.dimacs.filtered.cnf S = N/A | O = N/A
T = 1.02 | (out)(err)
S = OPTIMUM | O = 1
T = 32.27 | (out)(err)
S = N/A | O = N/A
T = 10.54 | (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 = 15.05 | (out)(err)
S = OPTIMUM | O = 1
T = 4.70 | (out)(err)
S = OPTIMUM | O = 1
T = 51.04 | (out)(err)
rsdecoder_fsm2.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.97 | (out)(err)
S = OPTIMUM | O = 2
T = 140.27 | (out)(err)
S = N/A | O = N/A
T = 10.93 | (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 = 26.70 | (out)(err)
S = OPTIMUM | O = 2
T = 124.86 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
rsdecoder_multivec1-problem.dimacs_33.filtered.cnf S = N/A | O = N/A
T = 1.09 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 12.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 = N/A | O = N/A
T = 5.20 | (out)(err)
S = N/A | O = N/A
T = 1010.15 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
rsdecoder_multivec1.dimacs.filtered.cnf S = N/A | O = N/A
T = 1.18 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 15.58 | (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 = 4.47 | (out)(err)
S = OPTIMUM | O = 4
T = 1428.04 | (out)(err)
S = N/A | O = N/A
T = 4.47 | (out)(err)
s15850-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.28 | (out)(err)
S = OPTIMUM | O = 4
T = 2.45 | (out)(err)
S = N/A | O = 4
T = Time Out | (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 = OPTIMUM | O = 4
T = 4.96 | (out)(err)
S = OPTIMUM | O = 4
T = 1.49 | (out)(err)
S = OPTIMUM | O = 4
T = 4.77 | (out)(err)
s15850-bug-onevec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.07 | (out)(err)
S = OPTIMUM | O = 1
T = 0.36 | (out)(err)
S = OPTIMUM | O = 1
T = 1.78 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = OPTIMUM | O = 1
T = 0.71 | (out)(err)
S = OPTIMUM | O = 1
T = 0.13 | (out)(err)
S = OPTIMUM | O = 1
T = 0.68 | (out)(err)
s38584-bug-onevec-gate-0.dimacs.seq.filtered.cnf S = N/A | O = N/A
T = 0.79 | (out)(err)
S = OPTIMUM | O = 1
T = 8.46 | (out)(err)
S = N/A | O = N/A
T = 10.69 | (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 = OPTIMUM | O = 1
T = 18.61 | (out)(err)
S = OPTIMUM | O = 1
T = 2.68 | (out)(err)
S = OPTIMUM | O = 1
T = 19.10 | (out)(err)
spi-problem.dimacs_42.filtered.cnf S = N/A | O = N/A
T = 1.00 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 11.05 | (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 = 5.28 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 5.25 | (out)(err)
spi2.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.89 | (out)(err)
S = OPTIMUM | O = 1
T = 12.69 | (out)(err)
S = OPTIMUM | O = 1
T = 10.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 = 1.89 | (out)(err)
S = OPTIMUM | O = 1
T = 1128.25 | (out)(err)
S = OPTIMUM | O = 1
T = 18.12 | (out)(err)
wb-problem.dimacs_45.filtered.cnf S = N/A | O = N/A
T = 0.93 | (out)(err)
S = OPTIMUM | O = 14
T = 19.43 | (out)(err)
S = N/A | O = N/A
T = 12.80 | (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 = OPTIMUM | O = 14
T = 38.15 | (out)(err)
S = OPTIMUM | O = 14
T = 12.94 | (out)(err)
S = OPTIMUM | O = 14
T = 38.11 | (out)(err)
wb-problem.dimacs_46.filtered.cnf S = N/A | O = N/A
T = 0.90 | (out)(err)
S = OPTIMUM | O = 476
T = 492.25 | (out)(err)
S = N/A | O = N/A
T = 12.30 | (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 = OPTIMUM | O = 476
T = 909.49 | (out)(err)
S = OPTIMUM | O = 476
T = 457.81 | (out)(err)
S = OPTIMUM | O = 476
T = 881.53 | (out)(err)
wb1.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.23 | (out)(err)
S = OPTIMUM | O = 218
T = 35.53 | (out)(err)
S = N/A | O = 385
T = Time Out | (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 = OPTIMUM | O = 218
T = 74.80 | (out)(err)
S = OPTIMUM | O = 218
T = 34.82 | (out)(err)
S = OPTIMUM | O = 218
T = 73.61 | (out)(err)
wb2.dimacs.filtered.cnf S = N/A | O = N/A
T = 0.24 | (out)(err)
S = OPTIMUM | O = 588
T = 113.49 | (out)(err)
S = N/A | O = 793
T = Time Out | (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 = OPTIMUM | O = 588
T = 207.43 | (out)(err)
S = OPTIMUM | O = 588
T = 120.67 | (out)(err)
S = OPTIMUM | O = 588
T = 226.69 | (out)(err)
wb_4m8s-problem.dimacs_47.filtered.cnf S = N/A | O = N/A
T = 1.01 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 2.52 | (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 = 6.05 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 5.97 | (out)(err)
wb_4m8s-problem.dimacs_48.filtered.cnf S = N/A | O = N/A
T = 1.00 | (out)(err)
S = N/A | O = N/A
T = 15.62 | (out)(err)
S = N/A | O = N/A
T = 2.67 | (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 = 6.07 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 6.01 | (out)(err)
wb_4m8s-problem.dimacs_49.filtered.cnf S = N/A | O = N/A
T = 1.10 | (out)(err)
S = N/A | O = N/A
T = 15.57 | (out)(err)
S = N/A | O = N/A
T = 2.53 | (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 = 6.22 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 6.01 | (out)(err)
wb_4m8s1.dimacs.filtered.cnf S = N/A | O = N/A
T = 1.11 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 11.54 | (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 = 4.51 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 4.36 | (out)(err)
wb_4m8s3.dimacs.filtered.cnf S = N/A | O = N/A
T = 1.11 | (out)(err)
S = OPTIMUM | O = 8
T = 28.09 | (out)(err)
S = N/A | O = N/A
T = 13.46 | (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 = 4.47 | (out)(err)
S = OPTIMUM | O = 8
T = 18.30 | (out)(err)
S = N/A | O = N/A
T = 4.45 | (out)(err)
wb_4m8s4.dimacs.filtered.cnf S = N/A | O = N/A
T = 1.10 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 9.63 | (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 = 4.37 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 4.45 | (out)(err)
wb_conmax1.dimacs.filtered.cnf S = N/A | O = N/A
T = 1.08 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 10.15 | (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 = 3.92 | (out)(err)
S = N/A | O = N/A
T = Time Out | (out)(err)
S = N/A | O = N/A
T = 4.32 | (out)(err)
wb_conmax3.dimacs.filtered.cnf S = N/A | O = N/A
T = 1.28 | (out)(err)
S = OPTIMUM | O = 33
T = 429.17 | (out)(err)
S = N/A | O = N/A
T = 27.06 | (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 = 4.08 | (out)(err)
S = OPTIMUM | O = 33
T = 134.77 | (out)(err)
S = N/A | O = N/A
T = 4.04 | (out)(err)