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 IncWMaxSatz WMaxSatz+ WMaxSatz-2009 WPM1 WPM2 akmaxsat akmaxsat_ls claspMaxSat sat4j-maxsat wbo1.6
frb10-6-1.wcnf S = OPT
O = 50
T = 0.01
S = OPT
O = 50
T = 0.01
(out)(err)
S = OPT
O = 50
T = 0.04
(out)(err)
S = OPT
O = 50
T = 0.04
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 50
T = 1.07
(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.15
(out)(err)
S = OPT
O = 50
T = 2.55
(out)(err)
S = OPT
O = 50
T = 2.55
(out)(err)
frb10-6-2.wcnf S = OPT
O = 50
T = 0.01
S = OPT
O = 50
T = 0.01
(out)(err)
S = OPT
O = 50
T = 0.06
(out)(err)
S = OPT
O = 50
T = 0.06
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 50
T = 1.05
(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.11
(out)(err)
S = OPT
O = 50
T = 2.45
(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 = 0.01
(out)(err)
S = OPT
O = 50
T = 0.06
(out)(err)
S = OPT
O = 50
T = 0.05
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 50
T = 0.99
(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.21
(out)(err)
S = OPT
O = 50
T = 3.26
(out)(err)
S = OPT
O = 50
T = 14.63
(out)(err)
frb10-6-4.wcnf S = OPT
O = 50
T = 0.01
S = OPT
O = 50
T = 0.01
(out)(err)
S = OPT
O = 50
T = 0.04
(out)(err)
S = OPT
O = 50
T = 0.04
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 50
T = 1.06
(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.10
(out)(err)
S = OPT
O = 50
T = 2.40
(out)(err)
S = OPT
O = 50
T = 29.25
(out)(err)
frb15-9-1.wcnf S = OPT
O = 120
T = 2.21
S = OPT
O = 120
T = 2.59
(out)(err)
S = OPT
O = 120
T = 44.56
(out)(err)
S = OPT
O = 120
T = 44.24
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 120
T = 7.52
(out)(err)
S = OPT
O = 120
T = 2.56
(out)(err)
S = OPT
O = 120
T = 2.21
(out)(err)
S = OPT
O = 120
T = 636.49
(out)(err)
S = OPT
O = 120
T = 1791.06
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
frb15-9-2.wcnf S = OPT
O = 120
T = 2.03
S = OPT
O = 120
T = 2.56
(out)(err)
S = OPT
O = 120
T = 42.76
(out)(err)
S = OPT
O = 120
T = 42.68
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 120
T = 7.52
(out)(err)
S = OPT
O = 120
T = 2.86
(out)(err)
S = OPT
O = 120
T = 2.03
(out)(err)
S = OPT
O = 120
T = 471.39
(out)(err)
S = OPT
O = 120
T = 1556.44
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
frb15-9-3.wcnf S = OPT
O = 120
T = 2.18
S = OPT
O = 120
T = 2.18
(out)(err)
S = OPT
O = 120
T = 38.48
(out)(err)
S = OPT
O = 120
T = 38.20
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 120
T = 7.34
(out)(err)
S = OPT
O = 120
T = 2.76
(out)(err)
S = OPT
O = 120
T = 2.30
(out)(err)
S = OPT
O = 120
T = 436.45
(out)(err)
S = OPT
O = 120
T = 1425.16
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb15-9-4.wcnf S = OPT
O = 120
T = 1.85
S = OPT
O = 120
T = 2.15
(out)(err)
S = OPT
O = 120
T = 41.99
(out)(err)
S = OPT
O = 120
T = 41.84
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 120
T = 7.44
(out)(err)
S = OPT
O = 120
T = 1.85
(out)(err)
S = OPT
O = 120
T = 2.03
(out)(err)
S = OPT
O = 120
T = 533.46
(out)(err)
S = OPT
O = 120
T = 1528.03
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
frb15-9-5.wcnf S = OPT
O = 120
T = 2.01
S = OPT
O = 120
T = 2.01
(out)(err)
S = OPT
O = 120
T = 29.21
(out)(err)
S = OPT
O = 120
T = 29.16
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 120
T = 7.49
(out)(err)
S = OPT
O = 120
T = 2.27
(out)(err)
S = OPT
O = 120
T = 2.22
(out)(err)
S = OPT
O = 120
T = 365.63
(out)(err)
S = OPT
O = 120
T = 1189.64
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb20-11-1.wcnf S = OPT
O = 200
T = 126.88
S = OPT
O = 200
T = 323.99
(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 = 126.88
(out)(err)
S = OPT
O = 200
T = 317.10
(out)(err)
S = OPT
O = 200
T = 258.23
(out)(err)
S = N/A
O = 200
T = TO
(out)(err)
S = N/A
O = 202
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
frb20-11-2.wcnf S = OPT
O = 200
T = 111.34
S = OPT
O = 200
T = 299.88
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 200
T = 111.34
(out)(err)
S = OPT
O = 200
T = 255.59
(out)(err)
S = OPT
O = 200
T = 261.73
(out)(err)
S = N/A
O = 201
T = TO
(out)(err)
S = N/A
O = 201
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb20-11-3.wcnf S = OPT
O = 200
T = 110.88
S = OPT
O = 200
T = 415.09
(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 = 110.88
(out)(err)
S = OPT
O = 200
T = 327.02
(out)(err)
S = OPT
O = 200
T = 269.71
(out)(err)
S = N/A
O = 201
T = TO
(out)(err)
S = N/A
O = 201
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
frb20-11-4.wcnf S = OPT
O = 200
T = 102.23
S = OPT
O = 200
T = 339.08
(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 = 102.23
(out)(err)
S = OPT
O = 200
T = 226.06
(out)(err)
S = OPT
O = 200
T = 202.41
(out)(err)
S = N/A
O = 201
T = TO
(out)(err)
S = N/A
O = 202
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb20-11-5.wcnf S = OPT
O = 200
T = 121.22
S = OPT
O = 200
T = 485.49
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 200
T = 121.22
(out)(err)
S = OPT
O = 200
T = 347.01
(out)(err)
S = OPT
O = 200
T = 243.17
(out)(err)
S = N/A
O = 201
T = TO
(out)(err)
S = N/A
O = 201
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb25-13-1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 1509.68
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 300
T = 1509.68
(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 = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 303
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb25-13-4.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 303
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb25-13-5.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 303
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
frb30-15-1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 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 = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 424
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
frb30-15-3.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 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 = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 566
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-2.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 566
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
frb35-17-3.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = 566
T = TO
(out)(err)
S = N/A
O = 564
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 = N/A
T = TO
(out)(err)
frb35-17-4.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 565
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 = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 566
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 = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 726
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 = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 726
T = TO
(out)(err)
S = N/A
O = 726
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 = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 728
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 = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 727
T = TO
(out)(err)
S = N/A
O = 727
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
ram_k3_n10.ra1.wcnf S = OPT
O = 232
T = 2.71
S = OPT
O = 232
T = 2.71
(out)(err)
S = OPT
O = 232
T = 3.46
(out)(err)
S = OPT
O = 232
T = 3.47
(out)(err)
S = OPT
O = 232
T = 574.78
(out)(err)
S = OPT
O = 232
T = 352.74
(out)(err)
S = OPT
O = 232
T = 5.16
(out)(err)
S = OPT
O = 232
T = 4.84
(out)(err)
S = OPT
O = 232
T = 14.69
(out)(err)
S = OPT
O = 232
T = 25.15
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
ram_k3_n11.ra1.wcnf S = OPT
O = 318
T = 21.09
S = OPT
O = 318
T = 21.09
(out)(err)
S = OPT
O = 318
T = 29.79
(out)(err)
S = OPT
O = 318
T = 29.85
(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 = 318
T = 50.47
(out)(err)
S = OPT
O = 318
T = 33.83
(out)(err)
S = OPT
O = 318
T = 154.96
(out)(err)
S = OPT
O = 318
T = 55.49
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
ram_k3_n12.ra1.wcnf S = OPT
O = 524
T = 221.82
S = OPT
O = 524
T = 221.82
(out)(err)
S = OPT
O = 524
T = 569.24
(out)(err)
S = OPT
O = 524
T = 569.79
(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 = 524
T = 267.76
(out)(err)
S = OPT
O = 524
T = 225.84
(out)(err)
S = OPT
O = 524
T = 519.90
(out)(err)
S = OPT
O = 524
T = 319.10
(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 = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 1832
T = TO
(out)(err)
S = N/A
O = 2061
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 = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 96192
T = TO
(out)(err)
S = N/A
O = 13401
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
ram_k3_n15.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 95579
T = TO
(out)(err)
S = N/A
O = 19212
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
ram_k3_n16.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 33877
T = TO
(out)(err)
S = N/A
O = 27825
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
ram_k3_n17.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = 27143
T = TO
(out)(err)
S = N/A
O = 10554
T = TO
(out)(err)
S = N/A
O = 35945
T = TO
(out)(err)
S = N/A
O = 26957
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 = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 47772
T = TO
(out)(err)
S = N/A
O = 44074
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
ram_k3_n19.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 61798
T = TO
(out)(err)
S = N/A
O = 53801
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 = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 76364
T = TO
(out)(err)
S = N/A
O = 71942
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.25
S = OPT
O = 7
T = 0.25
(out)(err)
S = OPT
O = 7
T = 0.32
(out)(err)
S = OPT
O = 7
T = 0.31
(out)(err)
S = OPT
O = 7
T = 0.36
(out)(err)
S = OPT
O = 7
T = 0.30
(out)(err)
S = OPT
O = 7
T = 0.37
(out)(err)
S = OPT
O = 7
T = 0.41
(out)(err)
S = OPT
O = 7
T = 0.76
(out)(err)
S = OPT
O = 7
T = 4.65
(out)(err)
S = OPT
O = 7
T = 1.32
(out)(err)
ram_k4_n18.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 487036
T = TO
(out)(err)
S = N/A
O = 71288
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
ram_k4_n19.ra1.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 576069
T = TO
(out)(err)
S = N/A
O = 56286
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 = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 545627
T = TO
(out)(err)
S = N/A
O = 77997
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
MANN_a27.clq.wcnf S = OPT
O = 2049
T = 564.74
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 2049
T = 564.74
(out)(err)
S = OPT
O = 2049
T = 754.15
(out)(err)
S = N/A
O = 2115
T = TO
(out)(err)
S = N/A
O = 2183
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
MANN_a45.clq.wcnf S = OPT
O = 2057
T = 334.15
S = N/A
O = 2057
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 2057
T = 334.15
(out)(err)
S = OPT
O = 2057
T = 471.00
(out)(err)
S = N/A
O = 2156
T = TO
(out)(err)
S = N/A
O = 2232
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
MANN_a81.clq.wcnf S = OPT
O = 1995
T = 368.92
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1995
T = 368.92
(out)(err)
S = OPT
O = 1995
T = 539.39
(out)(err)
S = N/A
O = 2045
T = TO
(out)(err)
S = N/A
O = 2136
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
MANN_a9.clq.wcnf S = OPT
O = 2179
T = 496.27
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 2179
T = 496.27
(out)(err)
S = OPT
O = 2179
T = 622.30
(out)(err)
S = N/A
O = 2267
T = TO
(out)(err)
S = N/A
O = 2320
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
brock200_1.clq.wcnf S = OPT
O = 1254
T = 3.53
S = OPT
O = 1254
T = 16.48
(out)(err)
S = OPT
O = 1254
T = 17.43
(out)(err)
S = OPT
O = 1254
T = 17.87
(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 = 1254
T = 3.55
(out)(err)
S = OPT
O = 1254
T = 3.53
(out)(err)
S = N/A
O = 1318
T = TO
(out)(err)
S = N/A
O = 1408
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
brock200_2.clq.wcnf S = OPT
O = 753
T = 0.15
S = OPT
O = 753
T = 0.55
(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 = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 753
T = 0.15
(out)(err)
S = OPT
O = 753
T = 0.19
(out)(err)
S = N/A
O = 790
T = TO
(out)(err)
S = N/A
O = 838
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
brock200_3.clq.wcnf S = OPT
O = 1102
T = 1.00
S = OPT
O = 1102
T = 4.87
(out)(err)
S = OPT
O = 1102
T = 5.12
(out)(err)
S = OPT
O = 1102
T = 5.04
(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 = 1102
T = 1.25
(out)(err)
S = OPT
O = 1102
T = 1.00
(out)(err)
S = N/A
O = 1173
T = TO
(out)(err)
S = N/A
O = 1216
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
brock200_4.clq.wcnf S = OPT
O = 1105
T = 1.48
S = OPT
O = 1105
T = 6.63
(out)(err)
S = OPT
O = 1105
T = 8.27
(out)(err)
S = OPT
O = 1105
T = 8.52
(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 = 1105
T = 2.19
(out)(err)
S = OPT
O = 1105
T = 1.48
(out)(err)
S = N/A
O = 1153
T = TO
(out)(err)
S = N/A
O = 1264
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
brock400_1.clq.wcnf S = OPT
O = 1361
T = 9.75
S = OPT
O = 1361
T = 35.36
(out)(err)
S = OPT
O = 1361
T = 50.25
(out)(err)
S = OPT
O = 1361
T = 51.22
(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 = 1361
T = 9.75
(out)(err)
S = OPT
O = 1361
T = 12.54
(out)(err)
S = N/A
O = 1415
T = TO
(out)(err)
S = N/A
O = 1502
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
brock400_2.clq.wcnf S = OPT
O = 1355
T = 7.70
S = OPT
O = 1355
T = 39.48
(out)(err)
S = OPT
O = 1355
T = 42.82
(out)(err)
S = OPT
O = 1355
T = 43.55
(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 = 1355
T = 7.70
(out)(err)
S = OPT
O = 1355
T = 9.27
(out)(err)
S = N/A
O = 1409
T = TO
(out)(err)
S = N/A
O = 1420
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
brock400_3.clq.wcnf S = OPT
O = 1259
T = 3.22
S = OPT
O = 1259
T = 16.33
(out)(err)
S = OPT
O = 1259
T = 19.55
(out)(err)
S = OPT
O = 1259
T = 20.65
(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 = 1259
T = 3.22
(out)(err)
S = OPT
O = 1259
T = 3.64
(out)(err)
S = N/A
O = 1313
T = TO
(out)(err)
S = N/A
O = 1394
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
brock400_4.clq.wcnf S = OPT
O = 1290
T = 2.12
S = OPT
O = 1290
T = 7.88
(out)(err)
S = OPT
O = 1290
T = 8.56
(out)(err)
S = OPT
O = 1290
T = 8.69
(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 = 1290
T = 3.16
(out)(err)
S = OPT
O = 1290
T = 2.12
(out)(err)
S = N/A
O = 1370
T = TO
(out)(err)
S = N/A
O = 1462
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
brock800_1.clq.wcnf S = OPT
O = 1071
T = 0.88
S = OPT
O = 1071
T = 3.60
(out)(err)
S = OPT
O = 1071
T = 4.57
(out)(err)
S = OPT
O = 1071
T = 4.66
(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 = 1071
T = 0.88
(out)(err)
S = OPT
O = 1071
T = 1.03
(out)(err)
S = N/A
O = 1108
T = TO
(out)(err)
S = N/A
O = 1159
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
brock800_2.clq.wcnf S = OPT
O = 1076
T = 0.96
S = OPT
O = 1076
T = 2.83
(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 = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1076
T = 1.29
(out)(err)
S = OPT
O = 1076
T = 0.96
(out)(err)
S = N/A
O = 1131
T = TO
(out)(err)
S = N/A
O = 1180
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
brock800_3.clq.wcnf S = OPT
O = 1079
T = 1.46
S = OPT
O = 1079
T = 5.83
(out)(err)
S = OPT
O = 1079
T = 10.18
(out)(err)
S = OPT
O = 1079
T = 10.34
(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 = 1079
T = 1.46
(out)(err)
S = OPT
O = 1079
T = 1.56
(out)(err)
S = N/A
O = 1126
T = TO
(out)(err)
S = N/A
O = 1210
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
brock800_4.clq.wcnf S = OPT
O = 1050
T = 0.99
S = OPT
O = 1050
T = 6.49
(out)(err)
S = OPT
O = 1050
T = 7.18
(out)(err)
S = OPT
O = 1050
T = 7.24
(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 = 1050
T = 0.99
(out)(err)
S = OPT
O = 1050
T = 1.10
(out)(err)
S = N/A
O = 1113
T = TO
(out)(err)
S = N/A
O = 1153
T = TO
(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.00
(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.05
(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.00
(out)(err)
S = OPT
O = 14
T = 0.79
(out)(err)
S = OPT
O = 14
T = 0.00
(out)(err)
c-fat200-2.clq.wcnf S = OPT
O = 167
T = 0.01
S = OPT
O = 167
T = 0.01
(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.44
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 167
T = 0.01
(out)(err)
S = OPT
O = 167
T = 0.05
(out)(err)
S = N/A
O = 167
T = TO
(out)(err)
S = N/A
O = 183
T = TO
(out)(err)
S = OPT
O = 167
T = 0.07
(out)(err)
c-fat200-5.clq.wcnf S = OPT
O = 613
T = 0.15
S = OPT
O = 613
T = 0.28
(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 = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 613
T = 0.15
(out)(err)
S = OPT
O = 613
T = 0.16
(out)(err)
S = N/A
O = 640
T = TO
(out)(err)
S = N/A
O = 707
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
c-fat500-1.clq.wcnf S = OPT
O = 10
T = 0.00
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.01
(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.00
(out)(err)
S = OPT
O = 10
T = 0.61
(out)(err)
S = OPT
O = 10
T = 0.00
(out)(err)
c-fat500-10.clq.wcnf S = OPT
O = 947
T = 7.91
S = OPT
O = 947
T = 41.22
(out)(err)
S = OPT
O = 947
T = 56.01
(out)(err)
S = OPT
O = 947
T = 57.98
(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 = 947
T = 7.91
(out)(err)
S = OPT
O = 947
T = 10.25
(out)(err)
S = N/A
O = 987
T = TO
(out)(err)
S = N/A
O = 997
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
c-fat500-2.clq.wcnf S = OPT
O = 97
T = 0.00
S = OPT
O = 97
T = 0.03
(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.65
(out)(err)
S = OPT
O = 97
T = 0.00
(out)(err)
S = OPT
O = 97
T = 0.05
(out)(err)
S = N/A
O = 97
T = TO
(out)(err)
S = N/A
O = 97
T = TO
(out)(err)
S = OPT
O = 97
T = 0.02
(out)(err)
c-fat500-5.clq.wcnf S = OPT
O = 404
T = 0.14
S = OPT
O = 404
T = 0.57
(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 = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 404
T = 0.14
(out)(err)
S = OPT
O = 404
T = 0.22
(out)(err)
S = N/A
O = 410
T = TO
(out)(err)
S = N/A
O = 450
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
hamming10-2.clq.wcnf S = OPT
O = 1929
T = 63.71
S = OPT
O = 1929
T = 304.37
(out)(err)
S = OPT
O = 1929
T = 340.41
(out)(err)
S = OPT
O = 1929
T = 346.13
(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 = 1929
T = 63.71
(out)(err)
S = OPT
O = 1929
T = 86.78
(out)(err)
S = N/A
O = 2036
T = TO
(out)(err)
S = N/A
O = 2062
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
hamming10-4.clq.wcnf S = OPT
O = 1683
T = 64.46
S = OPT
O = 1683
T = 268.36
(out)(err)
S = OPT
O = 1683
T = 304.58
(out)(err)
S = OPT
O = 1683
T = 309.55
(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 = 1683
T = 68.65
(out)(err)
S = OPT
O = 1683
T = 64.46
(out)(err)
S = N/A
O = 1733
T = TO
(out)(err)
S = N/A
O = 1812
T = TO
(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 = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 4646
T = TO
(out)(err)
S = N/A
O = 4732
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 = OPT
O = 1035
T = 2.54
(out)(err)
S = OPT
O = 1035
T = 1.52
(out)(err)
S = OPT
O = 1035
T = 1.52
(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 = 1035
T = 0.22
(out)(err)
S = OPT
O = 1035
T = 0.37
(out)(err)
S = N/A
O = 1390
T = TO
(out)(err)
S = N/A
O = 1483
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
hamming8-2.clq.wcnf S = OPT
O = 2213
T = 1415.50
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 2213
T = 1415.50
(out)(err)
S = N/A
O = 2213
T = TO
(out)(err)
S = N/A
O = 2287
T = TO
(out)(err)
S = N/A
O = 2329
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
hamming8-4.clq.wcnf S = OPT
O = 917
T = 0.20
S = OPT
O = 917
T = 1.02
(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 = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 917
T = 0.20
(out)(err)
S = OPT
O = 917
T = 0.20
(out)(err)
S = N/A
O = 999
T = TO
(out)(err)
S = N/A
O = 1014
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
johnson16-2-4.clq.wcnf S = OPT
O = 1170
T = 0.33
S = OPT
O = 1170
T = 1.20
(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 = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1170
T = 0.33
(out)(err)
S = OPT
O = 1170
T = 0.35
(out)(err)
S = N/A
O = 1247
T = TO
(out)(err)
S = N/A
O = 1288
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
johnson32-2-4.clq.wcnf S = OPT
O = 1788
T = 52.53
S = OPT
O = 1788
T = 398.02
(out)(err)
S = OPT
O = 1788
T = 348.46
(out)(err)
S = OPT
O = 1788
T = 353.90
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1788
T = 52.53
(out)(err)
S = OPT
O = 1788
T = 69.88
(out)(err)
S = N/A
O = 1863
T = TO
(out)(err)
S = N/A
O = 1903
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
johnson8-2-4.clq.wcnf S = OPT
O = 392
T = 0.03
S = OPT
O = 392
T = 0.04
(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 = 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 = N/A
O = 392
T = TO
(out)(err)
S = N/A
O = 392
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
johnson8-4-4.clq.wcnf S = N/A
O = N/A
T = TO
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = 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 = 4569
T = TO
(out)(err)
S = N/A
O = 4759
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
keller4.clq.wcnf S = OPT
O = 1133
T = 0.20
S = OPT
O = 1133
T = 0.86
(out)(err)
S = OPT
O = 1133
T = 0.74
(out)(err)
S = OPT
O = 1133
T = 0.72
(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 = 1133
T = 0.20
(out)(err)
S = OPT
O = 1133
T = 0.20
(out)(err)
S = N/A
O = 1233
T = TO
(out)(err)
S = N/A
O = 1335
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
keller5.clq.wcnf S = OPT
O = 1383
T = 5.61
S = OPT
O = 1383
T = 24.08
(out)(err)
S = OPT
O = 1383
T = 28.63
(out)(err)
S = OPT
O = 1383
T = 28.88
(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 = 1383
T = 5.61
(out)(err)
S = OPT
O = 1383
T = 6.17
(out)(err)
S = N/A
O = 1447
T = TO
(out)(err)
S = N/A
O = 1543
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
p_hat1000-1.clq.wcnf S = OPT
O = 248
T = 0.01
S = OPT
O = 248
T = 0.01
(out)(err)
S = OPT
O = 248
T = 0.03
(out)(err)
S = OPT
O = 248
T = 0.02
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 248
T = 0.02
(out)(err)
S = OPT
O = 248
T = 0.07
(out)(err)
S = N/A
O = 248
T = TO
(out)(err)
S = N/A
O = 254
T = TO
(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 = OPT
O = 752
T = 0.49
(out)(err)
S = OPT
O = 752
T = 0.68
(out)(err)
S = OPT
O = 752
T = 0.69
(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 = 752
T = 0.20
(out)(err)
S = OPT
O = 752
T = 0.25
(out)(err)
S = N/A
O = 766
T = TO
(out)(err)
S = N/A
O = 802
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
p_hat1000-3.clq.wcnf S = OPT
O = 1251
T = 2.69
S = OPT
O = 1251
T = 10.41
(out)(err)
S = OPT
O = 1251
T = 14.13
(out)(err)
S = OPT
O = 1251
T = 14.38
(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 = 1251
T = 2.96
(out)(err)
S = OPT
O = 1251
T = 2.69
(out)(err)
S = N/A
O = 1309
T = TO
(out)(err)
S = N/A
O = 1408
T = TO
(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 = OPT
O = 243
T = 0.02
(out)(err)
S = OPT
O = 243
T = 0.04
(out)(err)
S = OPT
O = 243
T = 0.03
(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 = 243
T = 0.02
(out)(err)
S = OPT
O = 243
T = 0.08
(out)(err)
S = N/A
O = 243
T = TO
(out)(err)
S = N/A
O = 243
T = TO
(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 = OPT
O = 711
T = 0.24
(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 = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 711
T = 0.13
(out)(err)
S = OPT
O = 711
T = 0.18
(out)(err)
S = N/A
O = 736
T = TO
(out)(err)
S = N/A
O = 772
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
p_hat300-3.clq.wcnf S = OPT
O = 1439
T = 7.73
S = OPT
O = 1439
T = 22.70
(out)(err)
S = OPT
O = 1439
T = 33.10
(out)(err)
S = OPT
O = 1439
T = 33.59
(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 = 1439
T = 7.73
(out)(err)
S = OPT
O = 1439
T = 8.30
(out)(err)
S = N/A
O = 1515
T = TO
(out)(err)
S = N/A
O = 1616
T = TO
(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 = OPT
O = 395
T = 0.04
(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 = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 395
T = 0.03
(out)(err)
S = OPT
O = 395
T = 0.10
(out)(err)
S = N/A
O = 402
T = TO
(out)(err)
S = N/A
O = 405
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
p_hat500-2.clq.wcnf S = OPT
O = 931
T = 0.57
S = OPT
O = 931
T = 1.53
(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 = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 931
T = 0.57
(out)(err)
S = OPT
O = 931
T = 0.66
(out)(err)
S = N/A
O = 953
T = TO
(out)(err)
S = N/A
O = 1004
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
p_hat500-3.clq.wcnf S = OPT
O = 1501
T = 9.22
S = OPT
O = 1501
T = 39.73
(out)(err)
S = OPT
O = 1501
T = 62.37
(out)(err)
S = OPT
O = 1501
T = 63.26
(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 = 1501
T = 9.22
(out)(err)
S = OPT
O = 1501
T = 10.03
(out)(err)
S = N/A
O = 1582
T = TO
(out)(err)
S = N/A
O = 1679
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
p_hat700-1.clq.wcnf S = OPT
O = 329
T = 0.02
S = OPT
O = 329
T = 0.02
(out)(err)
S = OPT
O = 329
T = 0.05
(out)(err)
S = OPT
O = 329
T = 0.04
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 329
T = 0.03
(out)(err)
S = OPT
O = 329
T = 0.08
(out)(err)
S = N/A
O = 332
T = TO
(out)(err)
S = N/A
O = 344
T = TO
(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 = OPT
O = 834
T = 0.89
(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 = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 834
T = 0.33
(out)(err)
S = OPT
O = 834
T = 0.36
(out)(err)
S = N/A
O = 852
T = TO
(out)(err)
S = N/A
O = 876
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
p_hat700-3.clq.wcnf S = OPT
O = 1432
T = 6.46
S = OPT
O = 1432
T = 36.18
(out)(err)
S = OPT
O = 1432
T = 55.76
(out)(err)
S = OPT
O = 1432
T = 56.30
(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 = 1432
T = 6.46
(out)(err)
S = OPT
O = 1432
T = 6.98
(out)(err)
S = N/A
O = 1493
T = TO
(out)(err)
S = N/A
O = 1518
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
san1000.clq.wcnf S = OPT
O = 744
T = 0.21
S = OPT
O = 744
T = 0.48
(out)(err)
S = OPT
O = 744
T = 0.49
(out)(err)
S = OPT
O = 744
T = 0.51
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 744
T = 0.21
(out)(err)
S = OPT
O = 744
T = 0.22
(out)(err)
S = N/A
O = 765
T = TO
(out)(err)
S = N/A
O = 809
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
san200_0.7_1.clq.wcnf S = OPT
O = 1256
T = 5.38
S = OPT
O = 1256
T = 18.76
(out)(err)
S = OPT
O = 1256
T = 24.42
(out)(err)
S = OPT
O = 1256
T = 24.77
(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 = 1256
T = 5.48
(out)(err)
S = OPT
O = 1256
T = 5.38
(out)(err)
S = N/A
O = 1313
T = TO
(out)(err)
S = N/A
O = 1389
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
san200_0.7_2.clq.wcnf S = OPT
O = 1243
T = 2.66
S = OPT
O = 1243
T = 7.78
(out)(err)
S = OPT
O = 1243
T = 11.53
(out)(err)
S = OPT
O = 1243
T = 11.75
(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 = 1243
T = 2.66
(out)(err)
S = OPT
O = 1243
T = 2.83
(out)(err)
S = N/A
O = 1305
T = TO
(out)(err)
S = N/A
O = 1286
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
san200_0.9_1.clq.wcnf S = OPT
O = 1672
T = 105.59
S = OPT
O = 1672
T = 722.87
(out)(err)
S = OPT
O = 1672
T = 758.25
(out)(err)
S = OPT
O = 1672
T = 770.17
(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 = 1672
T = 105.59
(out)(err)
S = OPT
O = 1672
T = 139.95
(out)(err)
S = N/A
O = 1714
T = TO
(out)(err)
S = N/A
O = 1778
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
san200_0.9_2.clq.wcnf S = OPT
O = 1647
T = 29.59
S = OPT
O = 1647
T = 146.28
(out)(err)
S = OPT
O = 1647
T = 190.85
(out)(err)
S = OPT
O = 1647
T = 193.95
(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 = 1647
T = 29.59
(out)(err)
S = OPT
O = 1647
T = 33.58
(out)(err)
S = N/A
O = 1718
T = TO
(out)(err)
S = N/A
O = 1812
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
san200_0.9_3.clq.wcnf S = OPT
O = 1670
T = 47.29
S = OPT
O = 1670
T = 178.86
(out)(err)
S = OPT
O = 1670
T = 313.19
(out)(err)
S = OPT
O = 1670
T = 317.69
(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 = 1670
T = 47.29
(out)(err)
S = OPT
O = 1670
T = 52.94
(out)(err)
S = N/A
O = 1734
T = TO
(out)(err)
S = N/A
O = 1763
T = TO
(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 = OPT
O = 718
T = 0.23
(out)(err)
S = OPT
O = 718
T = 0.34
(out)(err)
S = OPT
O = 718
T = 0.35
(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 = 718
T = 0.10
(out)(err)
S = OPT
O = 718
T = 0.14
(out)(err)
S = N/A
O = 742
T = TO
(out)(err)
S = N/A
O = 827
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
san400_0.7_1.clq.wcnf S = OPT
O = 1258
T = 6.79
S = OPT
O = 1258
T = 22.34
(out)(err)
S = OPT
O = 1258
T = 33.66
(out)(err)
S = OPT
O = 1258
T = 34.02
(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 = 1258
T = 6.79
(out)(err)
S = OPT
O = 1258
T = 7.07
(out)(err)
S = N/A
O = 1297
T = TO
(out)(err)
S = N/A
O = 1359
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
san400_0.7_2.clq.wcnf S = OPT
O = 1237
T = 2.66
S = OPT
O = 1237
T = 11.62
(out)(err)
S = OPT
O = 1237
T = 20.07
(out)(err)
S = OPT
O = 1237
T = 20.67
(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 = 1237
T = 3.33
(out)(err)
S = OPT
O = 1237
T = 2.66
(out)(err)
S = N/A
O = 1298
T = TO
(out)(err)
S = N/A
O = 1357
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
san400_0.7_3.clq.wcnf S = OPT
O = 1201
T = 2.29
S = OPT
O = 1201
T = 6.24
(out)(err)
S = OPT
O = 1201
T = 8.41
(out)(err)
S = OPT
O = 1201
T = 8.13
(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 = 1201
T = 2.29
(out)(err)
S = OPT
O = 1201
T = 2.48
(out)(err)
S = N/A
O = 1254
T = TO
(out)(err)
S = N/A
O = 1326
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
san400_0.9_1.clq.wcnf S = OPT
O = 1604
T = 41.41
S = OPT
O = 1604
T = 230.44
(out)(err)
S = OPT
O = 1604
T = 335.74
(out)(err)
S = OPT
O = 1604
T = 338.80
(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 = 1604
T = 41.41
(out)(err)
S = OPT
O = 1604
T = 57.26
(out)(err)
S = N/A
O = 1651
T = TO
(out)(err)
S = N/A
O = 1674
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
sanr200_0.7.clq.wcnf S = OPT
O = 1171
T = 1.26
S = OPT
O = 1171
T = 6.34
(out)(err)
S = OPT
O = 1171
T = 5.22
(out)(err)
S = OPT
O = 1171
T = 5.32
(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 = 1171
T = 1.52
(out)(err)
S = OPT
O = 1171
T = 1.26
(out)(err)
S = N/A
O = 1242
T = TO
(out)(err)
S = N/A
O = 1308
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
sanr200_0.9.clq.wcnf S = OPT
O = 1610
T = 42.42
S = OPT
O = 1610
T = 235.16
(out)(err)
S = OPT
O = 1610
T = 303.71
(out)(err)
S = OPT
O = 1610
T = 309.10
(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 = 1610
T = 42.42
(out)(err)
S = OPT
O = 1610
T = 50.37
(out)(err)
S = N/A
O = 1666
T = TO
(out)(err)
S = N/A
O = 1714
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
sanr400_0.5.clq.wcnf S = OPT
O = 763
T = 0.18
S = OPT
O = 763
T = 0.49
(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 = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 763
T = 0.20
(out)(err)
S = OPT
O = 763
T = 0.18
(out)(err)
S = N/A
O = 803
T = TO
(out)(err)
S = N/A
O = 891
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
sanr400_0.7.clq.wcnf S = OPT
O = 1198
T = 1.71
S = OPT
O = 1198
T = 5.95
(out)(err)
S = OPT
O = 1198
T = 9.63
(out)(err)
S = OPT
O = 1198
T = 9.81
(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 = 1198
T = 1.73
(out)(err)
S = OPT
O = 1198
T = 1.71
(out)(err)
S = N/A
O = 1269
T = TO
(out)(err)
S = N/A
O = 1328
T = TO
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
t3g3-5555.spn.wcnf S = OPT
O = 1100610
T = 0.00
S = OPT
O = 1100610
T = 0.00
(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 = 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 = 1.83
(out)(err)
S = OPT
O = 1100610
T = 15.51
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
t4g3-6666.spn.wcnf S = OPT
O = 2275606
T = 0.05
S = OPT
O = 2275606
T = 0.05
(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 = 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 = N/A
O = 2558926
T = TO
(out)(err)
S = N/A
O = 2702998
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
t5g3-7777.spn.wcnf S = OPT
O = 4241951
T = 0.64
S = OPT
O = 4241951
T = 1.20
(out)(err)
S = OPT
O = 4241951
T = 4.45
(out)(err)
S = OPT
O = 4241951
T = 4.45
(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 = 4241951
T = 2.61
(out)(err)
S = OPT
O = 4241951
T = 0.64
(out)(err)
S = N/A
O = 5056683
T = TO
(out)(err)
S = N/A
O = 5056683
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
t6g3-8888.spn.wcnf S = OPT
O = 7844119
T = 44.34
S = OPT
O = 7844119
T = 136.55
(out)(err)
S = OPT
O = 7844119
T = 196.73
(out)(err)
S = OPT
O = 7844119
T = 196.17
(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 = 7844119
T = 63.00
(out)(err)
S = OPT
O = 7844119
T = 44.34
(out)(err)
S = N/A
O = 10510608
T = TO
(out)(err)
S = N/A
O = 10510608
T = TO
(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 = 16052
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 = N/A
T = TO
(out)(err)
S = N/A
O = 12630233
T = TO
(out)(err)
S = N/A
O = 12235317
T = TO
(out)(err)
S = N/A
O = 15715857
T = TO
(out)(err)
S = N/A
O = 15881403
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)