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 Sat4j ShinMaxSat WMaxSatz+ WMaxSatz09 WPM1 akmaxsat akmaxsat_ls iut_rr_ls iut_rr_rv wbo1.6
frb10-6-1.wcnf S = OPT
O = 50
T = 0.01
S = OPT
O = 50
T = 2.73
(out)(err)
S = OPT
O = 50
T = 0.09
(out)(err)
S = OPT
O = 50
T = 0.04
(out)(err)
S = OPT
O = 50
T = 0.04
(out)(err)
S = OPT
O = 50
T = 27.16
(out)(err)
S = OPT
O = 50
T = 0.01
(out)(err)
S = OPT
O = 50
T = 0.10
(out)(err)
S = OPT
O = 50
T = 0.14
(out)(err)
S = OPT
O = 50
T = 0.14
(out)(err)
S = OPT
O = 50
T = 2.61
(out)(err)
frb10-6-2.wcnf S = OPT
O = 50
T = 0.01
S = OPT
O = 50
T = 3.55
(out)(err)
S = OPT
O = 50
T = 0.11
(out)(err)
S = OPT
O = 50
T = 0.05
(out)(err)
S = OPT
O = 50
T = 0.05
(out)(err)
S = OPT
O = 50
T = 43.33
(out)(err)
S = OPT
O = 50
T = 0.01
(out)(err)
S = OPT
O = 50
T = 0.10
(out)(err)
S = OPT
O = 50
T = 0.14
(out)(err)
S = OPT
O = 50
T = 0.14
(out)(err)
S = OPT
O = 50
T = 55.66
(out)(err)
frb10-6-3.wcnf S = OPT
O = 50
T = 0.01
S = OPT
O = 50
T = 3.37
(out)(err)
S = OPT
O = 50
T = 0.09
(out)(err)
S = OPT
O = 50
T = 0.05
(out)(err)
S = OPT
O = 50
T = 0.06
(out)(err)
S = OPT
O = 50
T = 30.46
(out)(err)
S = OPT
O = 50
T = 0.01
(out)(err)
S = OPT
O = 50
T = 0.10
(out)(err)
S = OPT
O = 50
T = 0.13
(out)(err)
S = OPT
O = 50
T = 0.13
(out)(err)
S = OPT
O = 50
T = 14.59
(out)(err)
frb10-6-4.wcnf S = OPT
O = 50
T = 0.01
S = OPT
O = 50
T = 3.12
(out)(err)
S = OPT
O = 50
T = 0.10
(out)(err)
S = OPT
O = 50
T = 0.04
(out)(err)
S = OPT
O = 50
T = 0.04
(out)(err)
S = OPT
O = 50
T = 26.57
(out)(err)
S = OPT
O = 50
T = 0.01
(out)(err)
S = OPT
O = 50
T = 0.11
(out)(err)
S = OPT
O = 50
T = 0.15
(out)(err)
S = OPT
O = 50
T = 0.14
(out)(err)
S = OPT
O = 50
T = 31.27
(out)(err)
frb15-9-1.wcnf S = OPT
O = 120
T = 0.81
S = N/A
O = 120
T = TO
(out)(err)
S = OPT
O = 120
T = 0.81
(out)(err)
S = OPT
O = 120
T = 44.61
(out)(err)
S = OPT
O = 120
T = 44.21
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 120
T = 2.55
(out)(err)
S = OPT
O = 120
T = 2.42
(out)(err)
S = OPT
O = 120
T = 9.75
(out)(err)
S = OPT
O = 120
T = 9.40
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
frb15-9-2.wcnf S = OPT
O = 120
T = 0.94
S = N/A
O = 122
T = TO
(out)(err)
S = OPT
O = 120
T = 0.94
(out)(err)
S = OPT
O = 120
T = 42.81
(out)(err)
S = OPT
O = 120
T = 42.58
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 120
T = 2.87
(out)(err)
S = OPT
O = 120
T = 2.16
(out)(err)
S = OPT
O = 120
T = 8.82
(out)(err)
S = OPT
O = 120
T = 8.60
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
frb15-9-3.wcnf S = OPT
O = 120
T = 0.81
S = N/A
O = 122
T = TO
(out)(err)
S = OPT
O = 120
T = 0.81
(out)(err)
S = OPT
O = 120
T = 38.53
(out)(err)
S = OPT
O = 120
T = 38.26
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 120
T = 2.75
(out)(err)
S = OPT
O = 120
T = 2.46
(out)(err)
S = OPT
O = 120
T = 10.22
(out)(err)
S = OPT
O = 120
T = 9.91
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb15-9-4.wcnf S = OPT
O = 120
T = 1.03
S = N/A
O = 121
T = TO
(out)(err)
S = OPT
O = 120
T = 1.03
(out)(err)
S = OPT
O = 120
T = 42.01
(out)(err)
S = OPT
O = 120
T = 42.01
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 120
T = 1.85
(out)(err)
S = OPT
O = 120
T = 2.21
(out)(err)
S = OPT
O = 120
T = 9.28
(out)(err)
S = OPT
O = 120
T = 9.01
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
frb15-9-5.wcnf S = OPT
O = 120
T = 0.91
S = N/A
O = 121
T = TO
(out)(err)
S = OPT
O = 120
T = 0.91
(out)(err)
S = OPT
O = 120
T = 29.18
(out)(err)
S = OPT
O = 120
T = 29.13
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 120
T = 2.28
(out)(err)
S = OPT
O = 120
T = 2.34
(out)(err)
S = OPT
O = 120
T = 9.69
(out)(err)
S = OPT
O = 120
T = 9.33
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb20-11-1.wcnf S = OPT
O = 200
T = 6.31
S = N/A
O = 204
T = TO
(out)(err)
S = OPT
O = 200
T = 6.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 = TO
(out)(err)
S = OPT
O = 200
T = 318.22
(out)(err)
S = OPT
O = 200
T = 275.68
(out)(err)
S = OPT
O = 200
T = 1141.29
(out)(err)
S = OPT
O = 200
T = 1104.47
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb20-11-2.wcnf S = OPT
O = 200
T = 5.18
S = N/A
O = 204
T = TO
(out)(err)
S = OPT
O = 200
T = 5.18
(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 = 200
T = 255.43
(out)(err)
S = OPT
O = 200
T = 263.79
(out)(err)
S = OPT
O = 200
T = 1117.58
(out)(err)
S = OPT
O = 200
T = 1080.21
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb20-11-3.wcnf S = OPT
O = 200
T = 4.75
S = N/A
O = 204
T = TO
(out)(err)
S = OPT
O = 200
T = 4.75
(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 = 200
T = 325.66
(out)(err)
S = OPT
O = 200
T = 278.01
(out)(err)
S = OPT
O = 200
T = 1154.06
(out)(err)
S = OPT
O = 200
T = 1119.09
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
frb20-11-4.wcnf S = OPT
O = 200
T = 5.35
S = N/A
O = 203
T = TO
(out)(err)
S = OPT
O = 200
T = 5.35
(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 = 200
T = 226.35
(out)(err)
S = OPT
O = 200
T = 214.04
(out)(err)
S = OPT
O = 200
T = 922.78
(out)(err)
S = OPT
O = 200
T = 887.35
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
frb20-11-5.wcnf S = OPT
O = 200
T = 5.94
S = N/A
O = 204
T = TO
(out)(err)
S = OPT
O = 200
T = 5.94
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 200
T = 348.10
(out)(err)
S = OPT
O = 200
T = 328.91
(out)(err)
S = OPT
O = 200
T = 1349.04
(out)(err)
S = OPT
O = 200
T = 1316.07
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
frb25-13-1.wcnf S = OPT
O = 300
T = 24.46
S = N/A
O = 305
T = TO
(out)(err)
S = OPT
O = 300
T = 24.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 = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = 301
T = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb25-13-2.wcnf S = OPT
O = 300
T = 30.39
S = N/A
O = 306
T = TO
(out)(err)
S = OPT
O = 300
T = 30.39
(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 = 302
T = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb25-13-3.wcnf S = OPT
O = 300
T = 26.55
S = N/A
O = 307
T = TO
(out)(err)
S = OPT
O = 300
T = 26.55
(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 = 302
T = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
frb25-13-4.wcnf S = OPT
O = 300
T = 15.57
S = N/A
O = 305
T = TO
(out)(err)
S = OPT
O = 300
T = 15.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 = TO
(out)(err)
S = N/A
O = 303
T = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb25-13-5.wcnf S = OPT
O = 300
T = 42.76
S = N/A
O = 306
T = TO
(out)(err)
S = OPT
O = 300
T = 42.76
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb30-15-1.wcnf S = OPT
O = 420
T = 205.64
S = N/A
O = 427
T = TO
(out)(err)
S = OPT
O = 420
T = 205.64
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb30-15-2.wcnf S = OPT
O = 420
T = 273.84
S = N/A
O = 428
T = TO
(out)(err)
S = OPT
O = 420
T = 273.84
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = 423
T = TO
(out)(err)
S = N/A
O = 423
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb30-15-3.wcnf S = OPT
O = 420
T = 179.28
S = N/A
O = 428
T = TO
(out)(err)
S = OPT
O = 420
T = 179.28
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb30-15-4.wcnf S = OPT
O = 420
T = 137.63
S = N/A
O = 430
T = TO
(out)(err)
S = OPT
O = 420
T = 137.63
(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 = 423
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb30-15-5.wcnf S = OPT
O = 420
T = 30.20
S = N/A
O = 429
T = TO
(out)(err)
S = OPT
O = 420
T = 30.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 = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb35-17-1.wcnf S = OPT
O = 560
T = 960.01
S = N/A
O = 570
T = TO
(out)(err)
S = OPT
O = 560
T = 960.01
(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 = 565
T = TO
(out)(err)
S = N/A
O = 566
T = TO
(out)(err)
S = N/A
O = 566
T = TO
(out)(err)
S = N/A
O = 566
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb35-17-2.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 568
T = TO
(out)(err)
S = N/A
O = 560
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 = 567
T = TO
(out)(err)
S = N/A
O = 565
T = TO
(out)(err)
S = N/A
O = 565
T = TO
(out)(err)
S = N/A
O = 565
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb35-17-3.wcnf S = OPT
O = 560
T = 611.73
S = N/A
O = 572
T = TO
(out)(err)
S = OPT
O = 560
T = 611.73
(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 = 566
T = TO
(out)(err)
S = N/A
O = 565
T = TO
(out)(err)
S = N/A
O = 565
T = TO
(out)(err)
S = N/A
O = 565
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb35-17-4.wcnf S = OPT
O = 560
T = 396.79
S = N/A
O = 572
T = TO
(out)(err)
S = OPT
O = 560
T = 396.79
(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 = 567
T = TO
(out)(err)
S = N/A
O = 566
T = TO
(out)(err)
S = N/A
O = 566
T = TO
(out)(err)
S = N/A
O = 566
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb35-17-5.wcnf S = OPT
O = 560
T = 508.13
S = N/A
O = 571
T = TO
(out)(err)
S = OPT
O = 560
T = 508.13
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = 565
T = TO
(out)(err)
S = N/A
O = 565
T = TO
(out)(err)
S = N/A
O = 565
T = TO
(out)(err)
S = N/A
O = 565
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb40-19-1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 731
T = TO
(out)(err)
S = N/A
O = 725
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 = 728
T = TO
(out)(err)
S = N/A
O = 727
T = TO
(out)(err)
S = N/A
O = 727
T = TO
(out)(err)
S = N/A
O = 727
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb40-19-2.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 731
T = TO
(out)(err)
S = N/A
O = 721
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 = 728
T = TO
(out)(err)
S = N/A
O = 727
T = TO
(out)(err)
S = N/A
O = 727
T = TO
(out)(err)
S = N/A
O = 727
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb40-19-3.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 729
T = TO
(out)(err)
S = N/A
O = 723
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 = 728
T = TO
(out)(err)
S = N/A
O = 727
T = TO
(out)(err)
S = N/A
O = 727
T = TO
(out)(err)
S = N/A
O = 727
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb40-19-4.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 731
T = TO
(out)(err)
S = N/A
O = 722
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 = 728
T = TO
(out)(err)
S = N/A
O = 727
T = TO
(out)(err)
S = N/A
O = 727
T = TO
(out)(err)
S = N/A
O = 727
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb40-19-5.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 732
T = TO
(out)(err)
S = N/A
O = 722
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 = 727
T = TO
(out)(err)
S = N/A
O = 726
T = TO
(out)(err)
S = N/A
O = 726
T = TO
(out)(err)
S = N/A
O = 726
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
ram_k3_n10.ra1.wcnf S = OPT
O = 232
T = 3.48
S = OPT
O = 232
T = 17.01
(out)(err)
S = N/A
O = 433
T = 320.41
(out)(err)
S = OPT
O = 232
T = 3.48
(out)(err)
S = OPT
O = 232
T = 3.49
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 232
T = 5.05
(out)(err)
S = OPT
O = 232
T = 4.80
(out)(err)
S = OPT
O = 232
T = 7.69
(out)(err)
S = OPT
O = 232
T = 7.48
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
ram_k3_n11.ra1.wcnf S = OPT
O = 318
T = 29.93
S = OPT
O = 318
T = 55.24
(out)(err)
S = N/A
O = 7985
T = TO
(out)(err)
S = OPT
O = 318
T = 29.93
(out)(err)
S = OPT
O = 318
T = 30.12
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 318
T = 50.32
(out)(err)
S = OPT
O = 318
T = 33.59
(out)(err)
S = OPT
O = 318
T = 50.95
(out)(err)
S = OPT
O = 318
T = 49.26
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
ram_k3_n12.ra1.wcnf S = OPT
O = 524
T = 224.06
S = OPT
O = 524
T = 266.11
(out)(err)
S = N/A
O = 11772
T = TO
(out)(err)
S = OPT
O = 524
T = 568.32
(out)(err)
S = OPT
O = 524
T = 572.08
(out)(err)
S = N/A
O = N/A
T = 749.99
(out)(err)
S = OPT
O = 524
T = 268.47
(out)(err)
S = OPT
O = 524
T = 224.06
(out)(err)
S = OPT
O = 524
T = 309.83
(out)(err)
S = OPT
O = 524
T = 311.27
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
ram_k3_n13.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 2061
T = TO
(out)(err)
S = N/A
O = 46853
T = 204.54
(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 = 2353
T = TO
(out)(err)
S = N/A
O = 1453
T = TO
(out)(err)
S = N/A
O = 1453
T = TO
(out)(err)
S = N/A
O = 1453
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
ram_k3_n14.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 11553
T = TO
(out)(err)
S = N/A
O = 29602
T = 254.54
(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 = 6708
T = TO
(out)(err)
S = N/A
O = 3171
T = TO
(out)(err)
S = N/A
O = 3171
T = TO
(out)(err)
S = N/A
O = 3171
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
ram_k3_n15.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 15295
T = TO
(out)(err)
S = N/A
O = 25999
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 = 9939
T = TO
(out)(err)
S = N/A
O = 4884
T = TO
(out)(err)
S = N/A
O = 4884
T = TO
(out)(err)
S = N/A
O = 4884
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
ram_k3_n16.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 28799
T = TO
(out)(err)
S = N/A
O = 38263
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 = 17868
T = TO
(out)(err)
S = N/A
O = 7849
T = TO
(out)(err)
S = N/A
O = 7849
T = TO
(out)(err)
S = N/A
O = 7849
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
ram_k3_n17.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 33677
T = TO
(out)(err)
S = N/A
O = 63912
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 = 26755
T = TO
(out)(err)
S = N/A
O = 10554
T = TO
(out)(err)
S = N/A
O = 10554
T = TO
(out)(err)
S = N/A
O = 10554
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
ram_k3_n18.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 43528
T = TO
(out)(err)
S = N/A
O = 72422
T = 85.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 = TO
(out)(err)
S = N/A
O = 32196
T = TO
(out)(err)
S = N/A
O = 16166
T = TO
(out)(err)
S = N/A
O = 16166
T = TO
(out)(err)
S = N/A
O = 16166
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
ram_k3_n19.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 56493
T = TO
(out)(err)
S = N/A
O = 236176
T = 119.90
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = 41858
T = TO
(out)(err)
S = N/A
O = 21705
T = TO
(out)(err)
S = N/A
O = 21705
T = TO
(out)(err)
S = N/A
O = 21705
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
ram_k3_n20.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 75939
T = TO
(out)(err)
S = N/A
O = 146872
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 = 58780
T = TO
(out)(err)
S = N/A
O = 24822
T = TO
(out)(err)
S = N/A
O = 24822
T = TO
(out)(err)
S = N/A
O = 24822
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
ram_k3_n9.ra1.wcnf S = OPT
O = 7
T = 0.29
S = OPT
O = 7
T = 4.83
(out)(err)
S = OPT
O = 7
T = 41.78
(out)(err)
S = OPT
O = 7
T = 0.31
(out)(err)
S = OPT
O = 7
T = 0.31
(out)(err)
S = OPT
O = 7
T = 0.29
(out)(err)
S = OPT
O = 7
T = 0.37
(out)(err)
S = OPT
O = 7
T = 0.42
(out)(err)
S = OPT
O = 7
T = 0.58
(out)(err)
S = OPT
O = 7
T = 0.57
(out)(err)
S = OPT
O = 7
T = 1.33
(out)(err)
ram_k4_n18.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 12511
T = TO
(out)(err)
S = N/A
O = 29227
T = 117.50
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = 2259
T = TO
(out)(err)
S = N/A
O = 750
T = TO
(out)(err)
S = N/A
O = 750
T = TO
(out)(err)
S = N/A
O = 750
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
ram_k4_n19.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 23218
T = TO
(out)(err)
S = N/A
O = 45361
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 = 8717
T = TO
(out)(err)
S = N/A
O = 2109
T = TO
(out)(err)
S = N/A
O = 2109
T = TO
(out)(err)
S = N/A
O = 2109
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
ram_k4_n20.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 26335
T = TO
(out)(err)
S = N/A
O = 76243
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 = 13349
T = TO
(out)(err)
S = N/A
O = 4414
T = TO
(out)(err)
S = N/A
O = 4414
T = TO
(out)(err)
S = N/A
O = 4414
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
MANN_a27.clq.wcnf S = OPT
O = 2049
T = 519.89
S = N/A
O = 2203
T = TO
(out)(err)
S = N/A
O = 4058
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 = OPT
O = 2049
T = 568.17
(out)(err)
S = OPT
O = 2049
T = 519.89
(out)(err)
S = OPT
O = 2049
T = 556.62
(out)(err)
S = OPT
O = 2049
T = 542.47
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
MANN_a45.clq.wcnf S = OPT
O = 2057
T = 311.25
S = N/A
O = 2231
T = TO
(out)(err)
S = N/A
O = 4314
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 = OPT
O = 2057
T = 336.46
(out)(err)
S = OPT
O = 2057
T = 311.25
(out)(err)
S = OPT
O = 2057
T = 342.39
(out)(err)
S = OPT
O = 2057
T = 331.76
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
MANN_a81.clq.wcnf S = OPT
O = 1995
T = 359.23
S = N/A
O = 2136
T = TO
(out)(err)
S = N/A
O = 4061
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 = OPT
O = 1995
T = 368.87
(out)(err)
S = OPT
O = 1995
T = 359.23
(out)(err)
S = OPT
O = 1995
T = 393.17
(out)(err)
S = OPT
O = 1995
T = 383.63
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
MANN_a9.clq.wcnf S = OPT
O = 2179
T = 412.24
S = N/A
O = 2320
T = TO
(out)(err)
S = N/A
O = 4747
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 = OPT
O = 2179
T = 499.65
(out)(err)
S = OPT
O = 2179
T = 412.24
(out)(err)
S = OPT
O = 2179
T = 443.60
(out)(err)
S = OPT
O = 2179
T = 431.12
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
brock200_1.clq.wcnf S = OPT
O = 1254
T = 2.73
S = N/A
O = 1408
T = TO
(out)(err)
S = N/A
O = 2537
T = TO
(out)(err)
S = OPT
O = 1254
T = 17.36
(out)(err)
S = OPT
O = 1254
T = 17.91
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1254
T = 3.55
(out)(err)
S = OPT
O = 1254
T = 2.73
(out)(err)
S = OPT
O = 1254
T = 3.00
(out)(err)
S = OPT
O = 1254
T = 2.92
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
brock200_2.clq.wcnf S = OPT
O = 753
T = 0.15
S = N/A
O = 844
T = TO
(out)(err)
S = N/A
O = 1396
T = TO
(out)(err)
S = OPT
O = 753
T = 0.51
(out)(err)
S = OPT
O = 753
T = 0.53
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 753
T = 0.15
(out)(err)
S = OPT
O = 753
T = 0.18
(out)(err)
S = OPT
O = 753
T = 0.19
(out)(err)
S = OPT
O = 753
T = 0.18
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
brock200_3.clq.wcnf S = OPT
O = 1102
T = 0.84
S = N/A
O = 1285
T = TO
(out)(err)
S = N/A
O = 2232
T = TO
(out)(err)
S = OPT
O = 1102
T = 5.12
(out)(err)
S = OPT
O = 1102
T = 5.05
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1102
T = 1.26
(out)(err)
S = OPT
O = 1102
T = 0.84
(out)(err)
S = OPT
O = 1102
T = 0.91
(out)(err)
S = OPT
O = 1102
T = 0.89
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
brock200_4.clq.wcnf S = OPT
O = 1105
T = 1.26
S = N/A
O = 1265
T = TO
(out)(err)
S = N/A
O = 1766
T = TO
(out)(err)
S = OPT
O = 1105
T = 8.26
(out)(err)
S = OPT
O = 1105
T = 8.51
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1105
T = 2.21
(out)(err)
S = OPT
O = 1105
T = 1.26
(out)(err)
S = OPT
O = 1105
T = 1.36
(out)(err)
S = OPT
O = 1105
T = 1.37
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
brock400_1.clq.wcnf S = OPT
O = 1361
T = 9.13
S = N/A
O = 1504
T = TO
(out)(err)
S = N/A
O = 2415
T = TO
(out)(err)
S = OPT
O = 1361
T = 50.29
(out)(err)
S = OPT
O = 1361
T = 51.17
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1361
T = 9.91
(out)(err)
S = OPT
O = 1361
T = 9.13
(out)(err)
S = OPT
O = 1361
T = 9.97
(out)(err)
S = OPT
O = 1361
T = 9.70
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
brock400_2.clq.wcnf S = OPT
O = 1355
T = 7.33
S = N/A
O = 1498
T = TO
(out)(err)
S = N/A
O = 2561
T = 660.48
(out)(err)
S = OPT
O = 1355
T = 42.85
(out)(err)
S = OPT
O = 1355
T = 43.39
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1355
T = 7.67
(out)(err)
S = OPT
O = 1355
T = 7.33
(out)(err)
S = OPT
O = 1355
T = 7.88
(out)(err)
S = OPT
O = 1355
T = 7.78
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
brock400_3.clq.wcnf S = OPT
O = 1259
T = 2.92
S = N/A
O = 1395
T = TO
(out)(err)
S = N/A
O = 2693
T = TO
(out)(err)
S = OPT
O = 1259
T = 19.47
(out)(err)
S = OPT
O = 1259
T = 20.64
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1259
T = 3.24
(out)(err)
S = OPT
O = 1259
T = 2.92
(out)(err)
S = OPT
O = 1259
T = 3.19
(out)(err)
S = OPT
O = 1259
T = 3.10
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
brock400_4.clq.wcnf S = OPT
O = 1290
T = 1.75
S = N/A
O = 1462
T = TO
(out)(err)
S = N/A
O = 2577
T = TO
(out)(err)
S = OPT
O = 1290
T = 8.54
(out)(err)
S = OPT
O = 1290
T = 8.68
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1290
T = 3.15
(out)(err)
S = OPT
O = 1290
T = 1.75
(out)(err)
S = OPT
O = 1290
T = 1.89
(out)(err)
S = OPT
O = 1290
T = 1.86
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
brock800_1.clq.wcnf S = OPT
O = 1071
T = 0.84
S = N/A
O = 1232
T = TO
(out)(err)
S = N/A
O = 2118
T = TO
(out)(err)
S = OPT
O = 1071
T = 4.58
(out)(err)
S = OPT
O = 1071
T = 4.66
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1071
T = 0.89
(out)(err)
S = OPT
O = 1071
T = 0.84
(out)(err)
S = OPT
O = 1071
T = 0.93
(out)(err)
S = OPT
O = 1071
T = 0.91
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
brock800_2.clq.wcnf S = OPT
O = 1076
T = 0.89
S = N/A
O = 1320
T = TO
(out)(err)
S = N/A
O = 1759
T = TO
(out)(err)
S = OPT
O = 1076
T = 3.36
(out)(err)
S = OPT
O = 1076
T = 3.35
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1076
T = 1.26
(out)(err)
S = OPT
O = 1076
T = 0.89
(out)(err)
S = OPT
O = 1076
T = 0.96
(out)(err)
S = OPT
O = 1076
T = 0.94
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
brock800_3.clq.wcnf S = OPT
O = 1079
T = 1.33
S = N/A
O = 1210
T = TO
(out)(err)
S = N/A
O = 2073
T = TO
(out)(err)
S = OPT
O = 1079
T = 10.20
(out)(err)
S = OPT
O = 1079
T = 10.33
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1079
T = 1.46
(out)(err)
S = OPT
O = 1079
T = 1.33
(out)(err)
S = OPT
O = 1079
T = 1.47
(out)(err)
S = OPT
O = 1079
T = 1.43
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
brock800_4.clq.wcnf S = OPT
O = 1050
T = 0.97
S = N/A
O = 1225
T = TO
(out)(err)
S = N/A
O = 1917
T = TO
(out)(err)
S = OPT
O = 1050
T = 7.22
(out)(err)
S = OPT
O = 1050
T = 7.23
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1050
T = 0.98
(out)(err)
S = OPT
O = 1050
T = 0.97
(out)(err)
S = OPT
O = 1050
T = 1.05
(out)(err)
S = OPT
O = 1050
T = 1.03
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
c-fat200-1.clq.wcnf S = OPT
O = 14
T = 0.00
S = OPT
O = 14
T = 0.53
(out)(err)
S = OPT
O = 14
T = 0.15
(out)(err)
S = OPT
O = 14
T = 0.00
(out)(err)
S = OPT
O = 14
T = 0.00
(out)(err)
S = OPT
O = 14
T = 0.01
(out)(err)
S = OPT
O = 14
T = 0.00
(out)(err)
S = OPT
O = 14
T = 0.04
(out)(err)
S = OPT
O = 14
T = 0.04
(out)(err)
S = OPT
O = 14
T = 0.04
(out)(err)
S = OPT
O = 14
T = 0.00
(out)(err)
c-fat200-2.clq.wcnf S = OPT
O = 167
T = 0.01
S = N/A
O = 215
T = TO
(out)(err)
S = N/A
O = 180
T = TO
(out)(err)
S = OPT
O = 167
T = 0.01
(out)(err)
S = OPT
O = 167
T = 0.01
(out)(err)
S = OPT
O = 167
T = 0.46
(out)(err)
S = OPT
O = 167
T = 0.01
(out)(err)
S = OPT
O = 167
T = 0.05
(out)(err)
S = OPT
O = 167
T = 0.05
(out)(err)
S = OPT
O = 167
T = 0.05
(out)(err)
S = OPT
O = 167
T = 0.07
(out)(err)
c-fat200-5.clq.wcnf S = OPT
O = 613
T = 0.15
S = N/A
O = 753
T = TO
(out)(err)
S = N/A
O = 1074
T = TO
(out)(err)
S = OPT
O = 613
T = 0.42
(out)(err)
S = OPT
O = 613
T = 0.46
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 613
T = 0.16
(out)(err)
S = OPT
O = 613
T = 0.15
(out)(err)
S = OPT
O = 613
T = 0.15
(out)(err)
S = OPT
O = 613
T = 0.16
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
c-fat500-1.clq.wcnf S = OPT
O = 10
T = 0.00
S = OPT
O = 10
T = 0.35
(out)(err)
S = OPT
O = 10
T = 0.04
(out)(err)
S = OPT
O = 10
T = 0.00
(out)(err)
S = OPT
O = 10
T = 0.00
(out)(err)
S = OPT
O = 10
T = 0.00
(out)(err)
S = OPT
O = 10
T = 0.00
(out)(err)
S = OPT
O = 10
T = 0.04
(out)(err)
S = OPT
O = 10
T = 0.03
(out)(err)
S = OPT
O = 10
T = 0.03
(out)(err)
S = OPT
O = 10
T = 0.00
(out)(err)
c-fat500-10.clq.wcnf S = OPT
O = 947
T = 7.91
S = N/A
O = 1039
T = TO
(out)(err)
S = N/A
O = 1711
T = TO
(out)(err)
S = OPT
O = 947
T = 55.98
(out)(err)
S = OPT
O = 947
T = 57.76
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 947
T = 7.91
(out)(err)
S = OPT
O = 947
T = 8.04
(out)(err)
S = OPT
O = 947
T = 8.87
(out)(err)
S = OPT
O = 947
T = 8.91
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
c-fat500-2.clq.wcnf S = OPT
O = 97
T = 0.00
S = N/A
O = 102
T = TO
(out)(err)
S = OPT
O = 97
T = 50.60
(out)(err)
S = OPT
O = 97
T = 0.01
(out)(err)
S = OPT
O = 97
T = 0.00
(out)(err)
S = OPT
O = 97
T = 0.04
(out)(err)
S = OPT
O = 97
T = 0.00
(out)(err)
S = OPT
O = 97
T = 0.04
(out)(err)
S = OPT
O = 97
T = 0.04
(out)(err)
S = OPT
O = 97
T = 0.04
(out)(err)
S = OPT
O = 97
T = 0.02
(out)(err)
c-fat500-5.clq.wcnf S = OPT
O = 404
T = 0.14
S = N/A
O = 452
T = TO
(out)(err)
S = N/A
O = 433
T = TO
(out)(err)
S = OPT
O = 404
T = 1.49
(out)(err)
S = OPT
O = 404
T = 1.49
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 404
T = 0.14
(out)(err)
S = OPT
O = 404
T = 0.23
(out)(err)
S = OPT
O = 404
T = 0.23
(out)(err)
S = OPT
O = 404
T = 0.23
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
hamming10-2.clq.wcnf S = OPT
O = 1929
T = 56.11
S = N/A
O = 2104
T = TO
(out)(err)
S = N/A
O = 4309
T = TO
(out)(err)
S = OPT
O = 1929
T = 339.63
(out)(err)
S = OPT
O = 1929
T = 345.15
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1929
T = 63.45
(out)(err)
S = OPT
O = 1929
T = 56.11
(out)(err)
S = OPT
O = 1929
T = 59.76
(out)(err)
S = OPT
O = 1929
T = 58.99
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
hamming10-4.clq.wcnf S = OPT
O = 1683
T = 48.76
S = N/A
O = 1812
T = TO
(out)(err)
S = N/A
O = 3476
T = TO
(out)(err)
S = OPT
O = 1683
T = 305.15
(out)(err)
S = OPT
O = 1683
T = 309.33
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1683
T = 68.15
(out)(err)
S = OPT
O = 1683
T = 48.76
(out)(err)
S = OPT
O = 1683
T = 52.29
(out)(err)
S = OPT
O = 1683
T = 51.45
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
hamming6-2.clq.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 4732
T = TO
(out)(err)
S = N/A
O = 10122
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 = 4495
T = TO
(out)(err)
S = N/A
O = 4391
T = TO
(out)(err)
S = N/A
O = 4391
T = TO
(out)(err)
S = N/A
O = 4391
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
hamming6-4.clq.wcnf S = OPT
O = 1035
T = 0.22
S = N/A
O = 1483
T = TO
(out)(err)
S = N/A
O = 2230
T = TO
(out)(err)
S = OPT
O = 1035
T = 1.52
(out)(err)
S = OPT
O = 1035
T = 1.51
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1035
T = 0.22
(out)(err)
S = OPT
O = 1035
T = 0.32
(out)(err)
S = OPT
O = 1035
T = 0.34
(out)(err)
S = OPT
O = 1035
T = 0.33
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
hamming8-2.clq.wcnf S = OPT
O = 2213
T = 1353.79
S = N/A
O = 2328
T = TO
(out)(err)
S = N/A
O = 4598
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 = OPT
O = 2213
T = 1434.23
(out)(err)
S = OPT
O = 2213
T = 1353.79
(out)(err)
S = OPT
O = 2213
T = 1482.49
(out)(err)
S = OPT
O = 2213
T = 1455.79
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
hamming8-4.clq.wcnf S = OPT
O = 917
T = 0.17
S = N/A
O = 1191
T = TO
(out)(err)
S = N/A
O = 1745
T = TO
(out)(err)
S = OPT
O = 917
T = 1.11
(out)(err)
S = OPT
O = 917
T = 1.12
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 917
T = 0.20
(out)(err)
S = OPT
O = 917
T = 0.17
(out)(err)
S = OPT
O = 917
T = 0.17
(out)(err)
S = OPT
O = 917
T = 0.17
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
johnson16-2-4.clq.wcnf S = OPT
O = 1170
T = 0.25
S = N/A
O = 1396
T = TO
(out)(err)
S = N/A
O = 2658
T = TO
(out)(err)
S = OPT
O = 1170
T = 0.96
(out)(err)
S = OPT
O = 1170
T = 0.96
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1170
T = 0.33
(out)(err)
S = OPT
O = 1170
T = 0.25
(out)(err)
S = OPT
O = 1170
T = 0.26
(out)(err)
S = OPT
O = 1170
T = 0.26
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
johnson32-2-4.clq.wcnf S = OPT
O = 1788
T = 49.25
S = N/A
O = 2030
T = TO
(out)(err)
S = N/A
O = 3922
T = TO
(out)(err)
S = OPT
O = 1788
T = 348.38
(out)(err)
S = OPT
O = 1788
T = 353.25
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1788
T = 52.33
(out)(err)
S = OPT
O = 1788
T = 49.25
(out)(err)
S = OPT
O = 1788
T = 53.76
(out)(err)
S = OPT
O = 1788
T = 52.60
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
johnson8-2-4.clq.wcnf S = OPT
O = 392
T = 0.03
S = N/A
O = 444
T = TO
(out)(err)
S = N/A
O = 626
T = TO
(out)(err)
S = OPT
O = 392
T = 0.03
(out)(err)
S = OPT
O = 392
T = 0.03
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 392
T = 0.03
(out)(err)
S = OPT
O = 392
T = 0.06
(out)(err)
S = OPT
O = 392
T = 0.06
(out)(err)
S = OPT
O = 392
T = 0.06
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
johnson8-4-4.clq.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 4759
T = 1741.66
(out)(err)
S = N/A
O = 10451
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 = 4191
T = TO
(out)(err)
S = N/A
O = 4154
T = TO
(out)(err)
S = N/A
O = 4154
T = TO
(out)(err)
S = N/A
O = 4154
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
keller4.clq.wcnf S = OPT
O = 1133
T = 0.17
S = N/A
O = 1398
T = TO
(out)(err)
S = N/A
O = 2271
T = TO
(out)(err)
S = OPT
O = 1133
T = 0.73
(out)(err)
S = OPT
O = 1133
T = 0.73
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1133
T = 0.20
(out)(err)
S = OPT
O = 1133
T = 0.17
(out)(err)
S = OPT
O = 1133
T = 0.17
(out)(err)
S = OPT
O = 1133
T = 0.17
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
keller5.clq.wcnf S = OPT
O = 1383
T = 5.32
S = N/A
O = 1543
T = TO
(out)(err)
S = N/A
O = 2495
T = TO
(out)(err)
S = OPT
O = 1383
T = 28.63
(out)(err)
S = OPT
O = 1383
T = 28.96
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1383
T = 5.57
(out)(err)
S = OPT
O = 1383
T = 5.32
(out)(err)
S = OPT
O = 1383
T = 5.94
(out)(err)
S = OPT
O = 1383
T = 5.75
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
p_hat1000-1.clq.wcnf S = OPT
O = 248
T = 0.02
S = N/A
O = 344
T = TO
(out)(err)
S = N/A
O = 284
T = TO
(out)(err)
S = OPT
O = 248
T = 0.02
(out)(err)
S = OPT
O = 248
T = 0.02
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 248
T = 0.02
(out)(err)
S = OPT
O = 248
T = 0.06
(out)(err)
S = OPT
O = 248
T = 0.06
(out)(err)
S = OPT
O = 248
T = 0.07
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
p_hat1000-2.clq.wcnf S = OPT
O = 752
T = 0.20
S = N/A
O = 802
T = TO
(out)(err)
S = N/A
O = 1188
T = TO
(out)(err)
S = OPT
O = 752
T = 0.68
(out)(err)
S = OPT
O = 752
T = 0.70
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 752
T = 0.20
(out)(err)
S = OPT
O = 752
T = 0.23
(out)(err)
S = OPT
O = 752
T = 0.25
(out)(err)
S = OPT
O = 752
T = 0.24
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
p_hat1000-3.clq.wcnf S = OPT
O = 1251
T = 2.17
S = N/A
O = 1451
T = TO
(out)(err)
S = N/A
O = 2539
T = TO
(out)(err)
S = OPT
O = 1251
T = 14.18
(out)(err)
S = OPT
O = 1251
T = 14.39
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1251
T = 2.95
(out)(err)
S = OPT
O = 1251
T = 2.17
(out)(err)
S = OPT
O = 1251
T = 2.32
(out)(err)
S = OPT
O = 1251
T = 2.28
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
p_hat300-1.clq.wcnf S = OPT
O = 243
T = 0.02
S = N/A
O = 296
T = TO
(out)(err)
S = N/A
O = 258
T = TO
(out)(err)
S = OPT
O = 243
T = 0.03
(out)(err)
S = OPT
O = 243
T = 0.03
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 243
T = 0.02
(out)(err)
S = OPT
O = 243
T = 0.07
(out)(err)
S = OPT
O = 243
T = 0.08
(out)(err)
S = OPT
O = 243
T = 0.08
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
p_hat300-2.clq.wcnf S = OPT
O = 711
T = 0.13
S = N/A
O = 850
T = TO
(out)(err)
S = N/A
O = 1232
T = TO
(out)(err)
S = OPT
O = 711
T = 0.26
(out)(err)
S = OPT
O = 711
T = 0.26
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 711
T = 0.13
(out)(err)
S = OPT
O = 711
T = 0.17
(out)(err)
S = OPT
O = 711
T = 0.17
(out)(err)
S = OPT
O = 711
T = 0.17
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
p_hat300-3.clq.wcnf S = OPT
O = 1439
T = 7.20
S = N/A
O = 1616
T = TO
(out)(err)
S = N/A
O = 3113
T = TO
(out)(err)
S = OPT
O = 1439
T = 33.16
(out)(err)
S = OPT
O = 1439
T = 33.63
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1439
T = 7.72
(out)(err)
S = OPT
O = 1439
T = 7.20
(out)(err)
S = OPT
O = 1439
T = 7.67
(out)(err)
S = OPT
O = 1439
T = 7.55
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
p_hat500-1.clq.wcnf S = OPT
O = 395
T = 0.03
S = N/A
O = 496
T = TO
(out)(err)
S = N/A
O = 584
T = TO
(out)(err)
S = OPT
O = 395
T = 0.07
(out)(err)
S = OPT
O = 395
T = 0.07
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 395
T = 0.03
(out)(err)
S = OPT
O = 395
T = 0.09
(out)(err)
S = OPT
O = 395
T = 0.09
(out)(err)
S = OPT
O = 395
T = 0.09
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
p_hat500-2.clq.wcnf S = OPT
O = 931
T = 0.57
S = N/A
O = 1006
T = TO
(out)(err)
S = N/A
O = 1839
T = TO
(out)(err)
S = OPT
O = 931
T = 1.78
(out)(err)
S = OPT
O = 931
T = 1.85
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 931
T = 0.57
(out)(err)
S = OPT
O = 931
T = 0.60
(out)(err)
S = OPT
O = 931
T = 0.64
(out)(err)
S = OPT
O = 931
T = 0.63
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
p_hat500-3.clq.wcnf S = OPT
O = 1501
T = 8.31
S = N/A
O = 1679
T = TO
(out)(err)
S = N/A
O = 2837
T = TO
(out)(err)
S = OPT
O = 1501
T = 62.41
(out)(err)
S = OPT
O = 1501
T = 62.99
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1501
T = 9.30
(out)(err)
S = OPT
O = 1501
T = 8.31
(out)(err)
S = OPT
O = 1501
T = 8.90
(out)(err)
S = OPT
O = 1501
T = 8.67
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
p_hat700-1.clq.wcnf S = OPT
O = 329
T = 0.03
S = N/A
O = 390
T = TO
(out)(err)
S = N/A
O = 547
T = TO
(out)(err)
S = OPT
O = 329
T = 0.04
(out)(err)
S = OPT
O = 329
T = 0.04
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 329
T = 0.03
(out)(err)
S = OPT
O = 329
T = 0.08
(out)(err)
S = OPT
O = 329
T = 0.08
(out)(err)
S = OPT
O = 329
T = 0.08
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
p_hat700-2.clq.wcnf S = OPT
O = 834
T = 0.33
S = N/A
O = 905
T = TO
(out)(err)
S = N/A
O = 1385
T = TO
(out)(err)
S = OPT
O = 834
T = 1.09
(out)(err)
S = OPT
O = 834
T = 1.08
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 834
T = 0.33
(out)(err)
S = OPT
O = 834
T = 0.35
(out)(err)
S = OPT
O = 834
T = 0.38
(out)(err)
S = OPT
O = 834
T = 0.37
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
p_hat700-3.clq.wcnf S = OPT
O = 1432
T = 5.63
S = N/A
O = 1625
T = TO
(out)(err)
S = N/A
O = 2732
T = TO
(out)(err)
S = OPT
O = 1432
T = 55.79
(out)(err)
S = OPT
O = 1432
T = 56.23
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1432
T = 6.50
(out)(err)
S = OPT
O = 1432
T = 5.63
(out)(err)
S = OPT
O = 1432
T = 6.07
(out)(err)
S = OPT
O = 1432
T = 5.96
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
san1000.clq.wcnf S = OPT
O = 744
T = 0.20
S = N/A
O = 840
T = TO
(out)(err)
S = N/A
O = 1380
T = 1030.97
(out)(err)
S = OPT
O = 744
T = 0.50
(out)(err)
S = OPT
O = 744
T = 0.50
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 744
T = 0.21
(out)(err)
S = OPT
O = 744
T = 0.20
(out)(err)
S = OPT
O = 744
T = 0.22
(out)(err)
S = OPT
O = 744
T = 0.21
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
san200_0.7_1.clq.wcnf S = OPT
O = 1256
T = 4.28
S = N/A
O = 1422
T = TO
(out)(err)
S = N/A
O = 2528
T = TO
(out)(err)
S = OPT
O = 1256
T = 24.44
(out)(err)
S = OPT
O = 1256
T = 24.70
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1256
T = 5.45
(out)(err)
S = OPT
O = 1256
T = 4.28
(out)(err)
S = OPT
O = 1256
T = 4.69
(out)(err)
S = OPT
O = 1256
T = 4.58
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
san200_0.7_2.clq.wcnf S = OPT
O = 1243
T = 2.33
S = N/A
O = 1446
T = TO
(out)(err)
S = N/A
O = 2335
T = TO
(out)(err)
S = OPT
O = 1243
T = 11.51
(out)(err)
S = OPT
O = 1243
T = 11.74
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1243
T = 2.67
(out)(err)
S = OPT
O = 1243
T = 2.33
(out)(err)
S = OPT
O = 1243
T = 2.49
(out)(err)
S = OPT
O = 1243
T = 2.44
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
san200_0.9_1.clq.wcnf S = OPT
O = 1672
T = 104.33
S = N/A
O = 1778
T = TO
(out)(err)
S = N/A
O = 3370
T = TO
(out)(err)
S = OPT
O = 1672
T = 759.34
(out)(err)
S = OPT
O = 1672
T = 768.93
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1672
T = 106.28
(out)(err)
S = OPT
O = 1672
T = 104.33
(out)(err)
S = OPT
O = 1672
T = 112.92
(out)(err)
S = OPT
O = 1672
T = 111.28
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
san200_0.9_2.clq.wcnf S = OPT
O = 1647
T = 24.09
S = N/A
O = 1810
T = TO
(out)(err)
S = N/A
O = 3461
T = TO
(out)(err)
S = OPT
O = 1647
T = 190.28
(out)(err)
S = OPT
O = 1647
T = 193.98
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1647
T = 29.37
(out)(err)
S = OPT
O = 1647
T = 24.09
(out)(err)
S = OPT
O = 1647
T = 26.00
(out)(err)
S = OPT
O = 1647
T = 25.51
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
san200_0.9_3.clq.wcnf S = OPT
O = 1670
T = 37.87
S = N/A
O = 1830
T = TO
(out)(err)
S = N/A
O = 3466
T = TO
(out)(err)
S = OPT
O = 1670
T = 313.24
(out)(err)
S = OPT
O = 1670
T = 317.28
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1670
T = 47.04
(out)(err)
S = OPT
O = 1670
T = 37.87
(out)(err)
S = OPT
O = 1670
T = 40.88
(out)(err)
S = OPT
O = 1670
T = 39.82
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
san400_0.5_1.clq.wcnf S = OPT
O = 718
T = 0.10
S = N/A
O = 962
T = TO
(out)(err)
S = N/A
O = 1440
T = TO
(out)(err)
S = OPT
O = 718
T = 0.34
(out)(err)
S = OPT
O = 718
T = 0.34
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 718
T = 0.10
(out)(err)
S = OPT
O = 718
T = 0.12
(out)(err)
S = OPT
O = 718
T = 0.13
(out)(err)
S = OPT
O = 718
T = 0.12
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
san400_0.7_1.clq.wcnf S = OPT
O = 1258
T = 5.86
S = N/A
O = 1359
T = TO
(out)(err)
S = N/A
O = 2508
T = TO
(out)(err)
S = OPT
O = 1258
T = 33.70
(out)(err)
S = OPT
O = 1258
T = 33.98
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1258
T = 6.85
(out)(err)
S = OPT
O = 1258
T = 5.86
(out)(err)
S = OPT
O = 1258
T = 6.36
(out)(err)
S = OPT
O = 1258
T = 6.31
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
san400_0.7_2.clq.wcnf S = OPT
O = 1237
T = 2.17
S = N/A
O = 1357
T = TO
(out)(err)
S = N/A
O = 2692
T = TO
(out)(err)
S = OPT
O = 1237
T = 20.10
(out)(err)
S = OPT
O = 1237
T = 20.73
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1237
T = 3.34
(out)(err)
S = OPT
O = 1237
T = 2.17
(out)(err)
S = OPT
O = 1237
T = 2.36
(out)(err)
S = OPT
O = 1237
T = 2.31
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
san400_0.7_3.clq.wcnf S = OPT
O = 1201
T = 2.09
S = N/A
O = 1408
T = TO
(out)(err)
S = N/A
O = 2482
T = TO
(out)(err)
S = OPT
O = 1201
T = 8.36
(out)(err)
S = OPT
O = 1201
T = 8.16
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1201
T = 2.28
(out)(err)
S = OPT
O = 1201
T = 2.09
(out)(err)
S = OPT
O = 1201
T = 2.27
(out)(err)
S = OPT
O = 1201
T = 2.22
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
san400_0.9_1.clq.wcnf S = OPT
O = 1604
T = 40.66
S = N/A
O = 1767
T = TO
(out)(err)
S = N/A
O = 3030
T = TO
(out)(err)
S = OPT
O = 1604
T = 334.25
(out)(err)
S = OPT
O = 1604
T = 338.87
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1604
T = 41.18
(out)(err)
S = OPT
O = 1604
T = 40.66
(out)(err)
S = OPT
O = 1604
T = 44.39
(out)(err)
S = OPT
O = 1604
T = 43.54
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
sanr200_0.7.clq.wcnf S = OPT
O = 1171
T = 1.00
S = N/A
O = 1389
T = TO
(out)(err)
S = N/A
O = 2199
T = TO
(out)(err)
S = OPT
O = 1171
T = 5.23
(out)(err)
S = OPT
O = 1171
T = 5.29
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1171
T = 1.54
(out)(err)
S = OPT
O = 1171
T = 1.00
(out)(err)
S = OPT
O = 1171
T = 1.07
(out)(err)
S = OPT
O = 1171
T = 1.06
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
sanr200_0.9.clq.wcnf S = OPT
O = 1610
T = 37.93
S = N/A
O = 1759
T = TO
(out)(err)
S = N/A
O = 3003
T = TO
(out)(err)
S = OPT
O = 1610
T = 301.89
(out)(err)
S = OPT
O = 1610
T = 308.29
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1610
T = 42.48
(out)(err)
S = OPT
O = 1610
T = 37.93
(out)(err)
S = OPT
O = 1610
T = 40.87
(out)(err)
S = OPT
O = 1610
T = 40.38
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
sanr400_0.5.clq.wcnf S = OPT
O = 763
T = 0.17
S = N/A
O = 991
T = TO
(out)(err)
S = N/A
O = 1426
T = TO
(out)(err)
S = OPT
O = 763
T = 0.73
(out)(err)
S = OPT
O = 763
T = 0.73
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 763
T = 0.20
(out)(err)
S = OPT
O = 763
T = 0.17
(out)(err)
S = OPT
O = 763
T = 0.17
(out)(err)
S = OPT
O = 763
T = 0.17
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
sanr400_0.7.clq.wcnf S = OPT
O = 1198
T = 1.42
S = N/A
O = 1386
T = TO
(out)(err)
S = N/A
O = 2427
T = TO
(out)(err)
S = OPT
O = 1198
T = 9.58
(out)(err)
S = OPT
O = 1198
T = 9.81
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1198
T = 1.73
(out)(err)
S = OPT
O = 1198
T = 1.42
(out)(err)
S = OPT
O = 1198
T = 1.56
(out)(err)
S = OPT
O = 1198
T = 1.55
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
t3g3-5555.spn.wcnf S = OPT
O = 1100610
T = 0.01
S = N/A
O = 1190133
T = TO
(out)(err)
S = N/A
O = 1608001
T = TO
(out)(err)
S = OPT
O = 1100610
T = 0.01
(out)(err)
S = OPT
O = 1100610
T = 0.01
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1100610
T = 0.01
(out)(err)
S = OPT
O = 1100610
T = 0.03
(out)(err)
S = OPT
O = 1100610
T = 0.04
(out)(err)
S = OPT
O = 1100610
T = 0.03
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
t4g3-6666.spn.wcnf S = OPT
O = 2275606
T = 0.12
S = N/A
O = 3111368
T = TO
(out)(err)
S = N/A
O = 5428697
T = 903.00
(out)(err)
S = OPT
O = 2275606
T = 0.12
(out)(err)
S = OPT
O = 2275606
T = 0.12
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 2275606
T = 0.17
(out)(err)
S = OPT
O = 2275606
T = 0.14
(out)(err)
S = OPT
O = 2275606
T = 0.16
(out)(err)
S = OPT
O = 2275606
T = 0.15
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
t5g3-7777.spn.wcnf S = OPT
O = 4241951
T = 0.62
S = N/A
O = 5056683
T = TO
(out)(err)
S = N/A
O = 9486181
T = 1157.80
(out)(err)
S = OPT
O = 4241951
T = 4.46
(out)(err)
S = OPT
O = 4241951
T = 4.45
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 4241951
T = 2.62
(out)(err)
S = OPT
O = 4241951
T = 0.62
(out)(err)
S = OPT
O = 4241951
T = 0.73
(out)(err)
S = OPT
O = 4241951
T = 0.71
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
t6g3-8888.spn.wcnf S = OPT
O = 7844119
T = 47.11
S = N/A
O = 10619955
T = TO
(out)(err)
S = N/A
O = 17514836
T = TO
(out)(err)
S = OPT
O = 7844119
T = 196.81
(out)(err)
S = OPT
O = 7844119
T = 196.15
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 7844119
T = 62.93
(out)(err)
S = OPT
O = 7844119
T = 47.11
(out)(err)
S = OPT
O = 7844119
T = 56.45
(out)(err)
S = OPT
O = 7844119
T = 54.41
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
t7g3-9999.spn.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = 15917405
T = TO
(out)(err)
S = N/A
O = 27953586
T = TO
(out)(err)
S = N/A
O = 14832554
T = TO
(out)(err)
S = N/A
O = 14832554
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = 12630233
T = TO
(out)(err)
S = N/A
O = 12471605
T = TO
(out)(err)
S = N/A
O = 12541437
T = TO
(out)(err)
S = N/A
O = 12541437
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)