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 CCEHC CCLS CnC-LS HS-Greedy Naps-1.02-ms Optiriss6-in Ramp SC2016 SsMonteCarlo Swcca-ms WPM3-2015-in dsat-wpm3-in-ms dsat-wpm3-s-in-ms
rsdecoder-debug.dimacs.cnf O = 1
T = 2.94
O = 354830
T = 244.31
O = N/A
T = TO
O = 1
T = 2.94
O = N/A
T = TO
O = N/A
T = TO
O = 1
T = 45.33
O = N/A
T = TO
O = N/A
T = TO
O = 386166
T = 3.26
O = N/A
T = TO
O = 1
T = 4.08
O = 1
T = 11.33
O = 1
T = 4.29
sudoku-debug.dimacs.cnf O = 1
T = 2.58
O = 266351
T = 244.52
O = N/A
T = TO
O = 1
T = 2.58
O = N/A
T = TO
O = N/A
T = TO
O = 1
T = 4.32
O = N/A
T = TO
O = N/A
T = TO
O = 288383
T = 2.60
O = N/A
T = TO
O = 1
T = 4.76
O = 1
T = 11.43
O = 1
T = 4.80
wb-debug.dimacs.cnf O = 28
T = 2.22
O = N/A
T = TO
O = N/A
T = TO
O = 40
T = 244.80
O = N/A
T = TO
O = N/A
T = TO
O = 28
T = 11.42
O = N/A
T = TO
O = N/A
T = TO
O = 120414
T = 0.93
O = N/A
T = TO
O = 28
T = 2.22
O = 28
T = 8.74
O = 28
T = 2.56
SM_AS_TOP_buggy1.dimacs.filtered.cnf O = 57
T = 48.55
O = N/A
T = TO
O = N/A
T = TO
O = 57
T = 154.28
O = N/A
T = TO
O = N/A
T = TO
O = 57
T = 107.80
O = N/A
T = TO
O = N/A
T = TO
O = 8109
T = 86.70
O = N/A
T = TO
O = 57
T = 59.51
O = 57
T = 48.55
O = 57
T = 64.70
SM_MAIN_MEM_buggy1.dimacs.filtered.cnf O = 395
T = 106.76
O = 544376
T = 243.50
O = N/A
T = TO
O = 395
T = 106.76
O = N/A
T = TO
O = N/A
T = TO
O = 165270
T = 5.14
O = N/A
T = TO
O = N/A
T = TO
O = 575430
T = 5.46
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
SM_RX_TOP.dimacs.filtered.cnf O = 6
T = 12.22
O = 84636
T = 244.45
O = N/A
T = TO
O = 14
T = 159.52
O = N/A
T = TO
O = N/A
T = TO
O = 6
T = 88.02
O = N/A
T = TO
O = N/A
T = TO
O = 143136
T = 1.32
O = N/A
T = TO
O = 6
T = 12.22
O = 6
T = 17.24
O = 556
T = 3.53
b15-bug-fourvec-gate-0.dimacs.seq.filtered.cnf O = 4
T = 3.15
O = 312766
T = 244.44
O = N/A
T = TO
O = 4
T = 4.07
O = N/A
T = TO
O = N/A
T = TO
O = 4
T = 63.64
O = N/A
T = TO
O = N/A
T = TO
O = 319557
T = 2.44
O = N/A
T = TO
O = 4
T = 3.15
O = 4
T = 9.91
O = 4
T = 3.20
c1_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf O = 4
T = 0.89
O = 178802
T = 243.18
O = N/A
T = TO
O = 4
T = 0.89
O = N/A
T = TO
O = N/A
T = TO
O = 4
T = 4.20
O = N/A
T = TO
O = N/A
T = TO
O = 205251
T = 1.39
O = N/A
T = TO
O = 4
T = 1.72
O = 4
T = 8.15
O = N/A
T = TO
c2_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf O = 4
T = 4.88
O = 186083
T = 244.40
O = N/A
T = TO
O = 12
T = 198.51
O = N/A
T = TO
O = N/A
T = TO
O = 4
T = 4.88
O = N/A
T = TO
O = N/A
T = TO
O = 210084
T = 1.61
O = N/A
T = TO
O = 4
T = 5.20
O = 4
T = 13.95
O = N/A
T = TO
c4_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf O = 8
T = 3.77
O = 446449
T = 247.12
O = N/A
T = TO
O = 8
T = 3.77
O = N/A
T = TO
O = N/A
T = TO
O = 8
T = 10.21
O = N/A
T = TO
O = N/A
T = TO
O = 401269
T = 2.99
O = N/A
T = TO
O = 8
T = 4.18
O = 8
T = 11.02
O = N/A
T = TO
c4_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf O = 4
T = 2.27
O = 231528
T = 245.67
O = N/A
T = TO
O = 4
T = 2.50
O = N/A
T = TO
O = N/A
T = TO
O = 4
T = 9.05
O = N/A
T = TO
O = N/A
T = TO
O = 225153
T = 1.69
O = N/A
T = TO
O = 4
T = 2.27
O = 4
T = 8.62
O = N/A
T = TO
c5_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf O = 8
T = 1.47
O = 50893
T = 243.22
O = N/A
T = TO
O = 8
T = 1.47
O = N/A
T = TO
O = N/A
T = TO
O = 8
T = 2.20
O = N/A
T = TO
O = N/A
T = TO
O = 104096
T = 0.76
O = N/A
T = TO
O = 8
T = 1.72
O = 8
T = 7.82
O = N/A
T = TO
c5_DD_s3_f1_e1_v2-bug-gate-0.dimacs.seq.filtered.cnf O = 8
T = 0.99
O = N/A
T = TO
O = N/A
T = TO
O = 8
T = 0.99
O = N/A
T = TO
O = N/A
T = TO
O = 8
T = 2.21
O = N/A
T = TO
O = N/A
T = TO
O = 104560
T = 0.77
O = N/A
T = TO
O = 8
T = 1.70
O = 8
T = 7.92
O = 8
T = 1.94
c6_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf O = 8
T = 0.75
O = 124902
T = 244.42
O = N/A
T = TO
O = 8
T = 0.75
O = N/A
T = TO
O = N/A
T = TO
O = 8
T = 3.20
O = N/A
T = TO
O = N/A
T = TO
O = 158189
T = 1.11
O = N/A
T = TO
O = 8
T = 1.48
O = 8
T = 7.71
O = 8
T = 1.55
divider-problem.dimacs_11.filtered.cnf O = 2
T = 45.89
O = 55460
T = 242.71
O = N/A
T = TO
O = 2
T = 79.00
O = N/A
T = TO
O = N/A
T = TO
O = 2
T = 45.89
O = N/A
T = TO
O = N/A
T = TO
O = 120335
T = 1.00
O = N/A
T = TO
O = 2
T = 99.37
O = 2
T = 63.31
O = 2
T = 77.15
divider-problem.dimacs_2.filtered.cnf O = 2
T = 24.73
O = 63289
T = 242.24
O = N/A
T = TO
O = 2
T = 24.73
O = N/A
T = TO
O = N/A
T = TO
O = 2
T = 35.97
O = N/A
T = TO
O = N/A
T = TO
O = 127937
T = 1.06
O = N/A
T = TO
O = 2
T = 53.84
O = 2
T = 57.32
O = N/A
T = TO
divider-problem.dimacs_5.filtered.cnf O = 2
T = 7.09
O = 69358
T = 243.93
O = N/A
T = TO
O = 4
T = 244.01
O = N/A
T = TO
O = N/A
T = TO
O = 2
T = 7.09
O = N/A
T = TO
O = N/A
T = TO
O = 127875
T = 1.05
O = N/A
T = TO
O = 2
T = 43.33
O = 2
T = 59.79
O = 2
T = 74.64
divider-problem.dimacs_8.filtered.cnf O = 2
T = 11.04
O = 83187
T = 244.03
O = N/A
T = TO
O = 2
T = 23.27
O = N/A
T = TO
O = N/A
T = TO
O = 2
T = 11.04
O = N/A
T = TO
O = N/A
T = TO
O = 138096
T = 1.13
O = N/A
T = TO
O = 2
T = 65.54
O = 2
T = 39.47
O = 2
T = 52.53
dividers10.dimacs.filtered.cnf O = 2
T = 1.57
O = 684
T = 248.62
O = 258
T = 268.50
O = 2
T = 10.25
O = N/A
T = TO
O = N/A
T = TO
O = 2
T = 1.57
O = N/A
T = TO
O = N/A
T = TO
O = 2237
T = 123.05
O = N/A
T = TO
O = 2
T = 3.87
O = 2
T = 9.21
O = N/A
T = TO
dividers_multivec1.dimacs.filtered.cnf O = 2
T = 3.03
O = N/A
T = TO
O = N/A
T = TO
O = 2
T = 10.84
O = N/A
T = TO
O = N/A
T = TO
O = 2
T = 3.62
O = N/A
T = TO
O = N/A
T = TO
O = 7183
T = 115.69
O = N/A
T = TO
O = 2
T = 3.03
O = 2
T = 8.77
O = N/A
T = TO
fpu_multivec1-problem.dimacs_14.filtered.cnf O = 2
T = 4.22
O = 90125
T = 243.39
O = N/A
T = TO
O = 2
T = 23.87
O = N/A
T = TO
O = N/A
T = TO
O = 2
T = 12.96
O = N/A
T = TO
O = N/A
T = TO
O = 148405
T = 1.31
O = N/A
T = TO
O = 2
T = 4.30
O = 2
T = 12.05
O = 2
T = 4.22
i2c-problem.dimacs_25.filtered.cnf O = 2
T = 1.44
O = 260727
T = 243.53
O = N/A
T = TO
O = 2
T = 1.44
O = N/A
T = TO
O = N/A
T = TO
O = 2
T = 13.84
O = N/A
T = TO
O = N/A
T = TO
O = 291154
T = 2.14
O = N/A
T = TO
O = 2
T = 13.08
O = 2
T = 18.85
O = 2
T = 32.62
i2c-problem.dimacs_26.filtered.cnf O = 2
T = 1.74
O = 183126
T = 244.89
O = N/A
T = TO
O = 2
T = 1.74
O = N/A
T = TO
O = N/A
T = TO
O = 2
T = 23.04
O = N/A
T = TO
O = N/A
T = TO
O = 221704
T = 1.67
O = N/A
T = TO
O = 2
T = 26.31
O = 2
T = 37.07
O = N/A
T = TO
mem_ctrl-problem.dimacs_27.filtered.cnf O = 2534114
T = 239.84
O = 2727419
T = 245.80
O = 2534114
T = 239.84
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
mem_ctrl1.dimacs.filtered.cnf O = 1
T = 10.27
O = 676367
T = 243.01
O = N/A
T = TO
O = 1
T = 52.31
O = N/A
T = TO
O = N/A
T = TO
O = 1
T = 10.27
O = N/A
T = TO
O = N/A
T = TO
O = 697262
T = 6.30
O = N/A
T = TO
O = 1
T = 11.02
O = 1
T = 19.70
O = 1
T = 11.21
mem_ctrl2_blackbox_mc_dp-problem.dimacs_28.filtered.cnf O = 3
T = 41.38
O = 1099141
T = 250.72
O = 986056
T = 241.07
O = 3
T = 58.35
O = N/A
T = TO
O = N/A
T = TO
O = 3
T = 105.55
O = N/A
T = TO
O = N/A
T = TO
O = 1118045
T = 9.89
O = N/A
T = TO
O = 3
T = 41.38
O = N/A
T = TO
O = N/A
T = TO
mrisc_mem2wire-problem.dimacs_29.filtered.cnf O = 1
T = 4.54
O = 462364
T = 243.42
O = N/A
T = TO
O = 1
T = 4.54
O = N/A
T = TO
O = N/A
T = TO
O = 1
T = 7.12
O = N/A
T = TO
O = N/A
T = TO
O = 493761
T = 4.11
O = N/A
T = TO
O = 1
T = 9.50
O = 1
T = 18.62
O = N/A
T = TO
rsdecoder-problem.dimacs_31.filtered.cnf O = 2
T = 4.75
O = 648134
T = 246.03
O = N/A
T = TO
O = 2
T = 4.75
O = N/A
T = TO
O = N/A
T = TO
O = 221198
T = 5.42
O = N/A
T = TO
O = N/A
T = TO
O = 674955
T = 5.57
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
rsdecoder-problem.dimacs_36.filtered.cnf O = 1
T = 3.17
O = 666920
T = 245.61
O = N/A
T = TO
O = 1
T = 3.17
O = N/A
T = TO
O = N/A
T = TO
O = 1
T = 29.86
O = N/A
T = TO
O = N/A
T = TO
O = 687600
T = 5.65
O = N/A
T = TO
O = 1
T = 24.91
O = 1
T = 31.61
O = 1
T = 45.97
rsdecoder-problem.dimacs_37.filtered.cnf O = 1
T = 61.35
O = 837295
T = 247.98
O = N/A
T = TO
O = 1
T = 61.35
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = 853694
T = 7.06
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = 615
T = 12.32
rsdecoder-problem.dimacs_38.filtered.cnf O = 2
T = 3.51
O = 649648
T = 245.64
O = N/A
T = TO
O = 2
T = 3.51
O = N/A
T = TO
O = N/A
T = TO
O = 221410
T = 5.17
O = N/A
T = TO
O = N/A
T = TO
O = 675050
T = 5.64
O = N/A
T = TO
O = 448
T = 11.07
O = N/A
T = TO
O = 448
T = 11.04
rsdecoder-problem.dimacs_39.filtered.cnf O = 1
T = 8.95
O = 650939
T = 246.08
O = N/A
T = TO
O = 1
T = 8.95
O = N/A
T = TO
O = N/A
T = TO
O = 1
T = 87.17
O = N/A
T = TO
O = N/A
T = TO
O = 675562
T = 5.63
O = N/A
T = TO
O = 1
T = 48.55
O = 1
T = 60.53
O = 1
T = 67.79
rsdecoder-problem.dimacs_40.filtered.cnf O = 1
T = 3.67
O = 667887
T = 246.82
O = N/A
T = TO
O = 1
T = 3.67
O = N/A
T = TO
O = N/A
T = TO
O = 1
T = 37.30
O = N/A
T = TO
O = N/A
T = TO
O = 687860
T = 5.68
O = N/A
T = TO
O = 1
T = 75.44
O = 1
T = 47.94
O = 1
T = 62.24
rsdecoder-problem.dimacs_41.filtered.cnf O = 2
T = 6.08
O = 646547
T = 243.29
O = N/A
T = TO
O = 2
T = 6.08
O = N/A
T = TO
O = N/A
T = TO
O = 219331
T = 5.18
O = N/A
T = TO
O = N/A
T = TO
O = 668316
T = 5.53
O = N/A
T = TO
O = 2634
T = 12.99
O = N/A
T = TO
O = 2634
T = 12.27
rsdecoder1_blackbox_CSEEblock-problem.dimacs_32.filtered.cnf O = 4
T = 264.81
O = 83252
T = 243.42
O = N/A
T = TO
O = 5
T = 71.45
O = N/A
T = TO
O = N/A
T = TO
O = 45934
T = 1.02
O = N/A
T = TO
O = N/A
T = TO
O = 139935
T = 1.16
O = N/A
T = TO
O = 269
T = 1.97
O = 4
T = 264.81
O = 4
T = 282.64
rsdecoder1_blackbox_KESblock-problem.dimacs_30.filtered.cnf O = 4
T = 66.29
O = 146767
T = 242.72
O = N/A
T = TO
O = 4
T = 66.29
O = N/A
T = TO
O = N/A
T = TO
O = 55565
T = 1.59
O = N/A
T = TO
O = N/A
T = TO
O = 193339
T = 1.77
O = N/A
T = TO
O = 819
T = 3.72
O = N/A
T = TO
O = 819
T = 3.78
rsdecoder2.dimacs.filtered.cnf O = 1
T = 7.32
O = 206019
T = 244.45
O = N/A
T = TO
O = 1
T = 7.32
O = N/A
T = TO
O = N/A
T = TO
O = 1
T = 142.02
O = N/A
T = TO
O = N/A
T = TO
O = 248282
T = 2.36
O = N/A
T = TO
O = 1
T = 47.87
O = 1
T = 88.95
O = 1
T = 98.55
rsdecoder4.dimacs.filtered.cnf O = 7
T = 263.83
O = 79707
T = 243.63
O = N/A
T = TO
O = 7
T = 263.83
O = N/A
T = TO
O = N/A
T = TO
O = 80138
T = 1.15
O = N/A
T = TO
O = N/A
T = TO
O = 141737
T = 1.35
O = N/A
T = TO
O = 215
T = 2.46
O = N/A
T = TO
O = N/A
T = TO
rsdecoder5.dimacs.filtered.cnf O = 2
T = 9.95
O = 77431
T = 243.74
O = N/A
T = TO
O = 2
T = 9.95
O = N/A
T = TO
O = N/A
T = TO
O = 2
T = 74.60
O = N/A
T = TO
O = N/A
T = TO
O = 142170
T = 1.33
O = N/A
T = TO
O = 80
T = 1.64
O = 2
T = 154.79
O = N/A
T = TO
rsdecoder6.dimacs.filtered.cnf O = 6
T = 23.60
O = 89186
T = 244.01
O = N/A
T = TO
O = 6
T = 23.60
O = N/A
T = TO
O = N/A
T = TO
O = 80138
T = 1.09
O = N/A
T = TO
O = N/A
T = TO
O = 142415
T = 1.34
O = N/A
T = TO
O = 80
T = 1.71
O = N/A
T = TO
O = N/A
T = TO
rsdecoder_fsm2.dimacs.filtered.cnf O = 2
T = 5.34
O = 86755
T = 244.30
O = N/A
T = TO
O = 2
T = 5.34
O = N/A
T = TO
O = N/A
T = TO
O = 2
T = 10.92
O = N/A
T = TO
O = N/A
T = TO
O = 142216
T = 1.35
O = N/A
T = TO
O = 2
T = 7.36
O = 2
T = 22.26
O = 2
T = 7.21
rsdecoder_multivec1-problem.dimacs_33.filtered.cnf O = 4
T = 12.03
O = 316529
T = 244.18
O = N/A
T = TO
O = 4
T = 12.03
O = N/A
T = TO
O = N/A
T = TO
O = 4
T = 176.61
O = N/A
T = TO
O = N/A
T = TO
O = 357388
T = 3.07
O = N/A
T = TO
O = 4
T = 115.21
O = 4
T = 79.53
O = 4
T = 93.74
rsdecoder_multivec1.dimacs.filtered.cnf O = 4
T = 1.84
O = 192624
T = 243.63
O = N/A
T = TO
O = 4
T = 1.84
O = N/A
T = TO
O = N/A
T = TO
O = 4
T = 134.86
O = N/A
T = TO
O = N/A
T = TO
O = 239724
T = 2.39
O = N/A
T = TO
O = 4
T = 2.99
O = 4
T = 9.92
O = N/A
T = TO
wb-problem.dimacs_45.filtered.cnf O = 14
T = 2.32
O = 115498
T = 243.81
O = N/A
T = TO
O = 14
T = 5.52
O = N/A
T = TO
O = N/A
T = TO
O = 14
T = 2.56
O = N/A
T = TO
O = N/A
T = TO
O = 161930
T = 1.12
O = N/A
T = TO
O = 14
T = 2.32
O = 14
T = 8.56
O = N/A
T = TO
wb-problem.dimacs_46.filtered.cnf O = 476
T = 22.33
O = 110202
T = 243.52
O = N/A
T = TO
O = 476
T = 68.72
O = N/A
T = TO
O = N/A
T = TO
O = 42259
T = 1.05
O = N/A
T = TO
O = N/A
T = TO
O = 156994
T = 1.09
O = N/A
T = TO
O = 476
T = 22.33
O = 476
T = 27.80
O = 476
T = 41.87
wb1.dimacs.filtered.cnf O = 218
T = 2.29
O = 896
T = 248.97
O = N/A
T = TO
O = 218
T = 147.46
O = N/A
T = TO
O = N/A
T = TO
O = 218
T = 6.49
O = N/A
T = TO
O = N/A
T = TO
O = 1859
T = 99.19
O = 300
T = 254.86
O = 218
T = 2.29
O = 218
T = 8.04
O = N/A
T = TO
wb2.dimacs.filtered.cnf O = 588
T = 6.80
O = 1280
T = 263.66
O = 1100
T = 265.84
O = 598
T = 130.83
O = N/A
T = TO
O = N/A
T = TO
O = 588
T = 76.72
O = N/A
T = TO
O = N/A
T = TO
O = 2225
T = 111.17
O = N/A
T = TO
O = 588
T = 6.98
O = 588
T = 12.35
O = 588
T = 6.80
wb_4m8s-problem.dimacs_47.filtered.cnf O = 31
T = 208.62
O = 1520473
T = 247.86
O = 1426315
T = 240.90
O = 31
T = 208.62
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
wb_4m8s-problem.dimacs_48.filtered.cnf O = 8
T = 30.46
O = 1565283
T = 241.86
O = 1468418
T = 241.54
O = 8
T = 30.46
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
wb_4m8s-problem.dimacs_49.filtered.cnf O = 226
T = 155.11
O = 1572943
T = 243.64
O = 1478874
T = 241.01
O = 226
T = 155.11
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
O = N/A
T = TO
wb_4m8s1.dimacs.filtered.cnf O = 33
T = 73.10
O = 238286
T = 245.52
O = N/A
T = TO
O = 33
T = 73.10
O = N/A
T = TO
O = N/A
T = TO
O = 54829
T = 2.49
O = N/A
T = TO
O = N/A
T = TO
O = 280687
T = 2.50
O = N/A
T = TO
O = 460
T = 3.31
O = N/A
T = TO
O = N/A
T = TO
wb_4m8s3.dimacs.filtered.cnf O = 8
T = 5.14
O = 238592
T = 244.51
O = N/A
T = TO
O = 8
T = 79.68
O = N/A
T = TO
O = N/A
T = TO
O = 8
T = 5.55
O = N/A
T = TO
O = N/A
T = TO
O = 281519
T = 2.49
O = N/A
T = TO
O = 8
T = 5.14
O = 8
T = 11.94
O = N/A
T = TO
wb_4m8s4.dimacs.filtered.cnf O = 224
T = 249.62
O = 236680
T = 244.58
O = N/A
T = TO
O = 224
T = 249.62
O = N/A
T = TO
O = N/A
T = TO
O = 54829
T = 2.45
O = N/A
T = TO
O = N/A
T = TO
O = 279966
T = 2.52
O = N/A
T = TO
O = 230
T = 3.29
O = N/A
T = TO
O = N/A
T = TO
wb_conmax1.dimacs.filtered.cnf O = 40
T = 250.45
O = 128113
T = 243.79
O = N/A
T = TO
O = 45
T = 26.39
O = N/A
T = TO
O = N/A
T = TO
O = 21371
T = 1.66
O = N/A
T = TO
O = N/A
T = TO
O = 179502
T = 1.77
O = N/A
T = TO
O = 54
T = 2.46
O = 40
T = 266.75
O = 40
T = 250.45
wb_conmax3.dimacs.filtered.cnf O = 33
T = 17.41
O = 118802
T = 243.33
O = N/A
T = TO
O = 33
T = 231.66
O = N/A
T = TO
O = N/A
T = TO
O = 33
T = 100.00
O = N/A
T = TO
O = N/A
T = TO
O = 179668
T = 1.78
O = N/A
T = TO
O = 33
T = 17.41
O = 33
T = 21.28
O = 33
T = 33.60