Benchmark

LabelMeaning
SSolution {OPTIMUM FOUND or OPT | UNSATISFIABLE or UNSAT | UNKNOWN | Not available or N/A}
OBest solution found
TCPU time (TO for Time Out)
(out)(err)Standard output and standard error for each solver

ColorMeaning for Complete SolversMeaning for Incomplete Solvers
TextBest solver columnBest solver column
TextOptimal solution with the best CPU timeBest solution with the best CPU time
TextOptimal solution and finished within the Time OutBest solution without the best CPU time
TextOptimal solution and did not finish within the Time OutSolution found but not the best
TextTime OutTime Out
TextBuggy solutionBuggy solution

Instance file name Best solver CCLS SAT4Jms-ext-i SAT4Jms-int-i iraNovelty++ optimax-it
frb10-6-1.wcnf O = 50
T = 0.02
O = 50
T = 1.87
(out)(err)
O = 50
T = 2.20
(out)(err)
O = 50
T = 1.89
(out)(err)
O = 50
T = 1.13
(out)(err)
O = 50
T = 0.02
(out)(err)
frb10-6-2.wcnf O = 50
T = 0.06
O = 50
T = 1.84
(out)(err)
O = 50
T = 1.63
(out)(err)
O = 50
T = 2.06
(out)(err)
O = 50
T = 1.03
(out)(err)
O = 50
T = 0.06
(out)(err)
frb10-6-3.wcnf O = 50
T = 0.01
O = 50
T = 1.61
(out)(err)
O = 50
T = 2.45
(out)(err)
O = 50
T = 2.24
(out)(err)
O = 50
T = 0.85
(out)(err)
O = 50
T = 0.01
(out)(err)
frb10-6-4.wcnf O = 50
T = 0.01
O = 50
T = 1.72
(out)(err)
O = 50
T = 1.35
(out)(err)
O = 50
T = 2.13
(out)(err)
O = 50
T = 0.84
(out)(err)
O = 50
T = 0.01
(out)(err)
frb15-9-1.wcnf O = 120
T = 1.33
O = 120
T = 2.82
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 120
T = 44.25
(out)(err)
O = 120
T = 1.33
(out)(err)
frb15-9-2.wcnf O = 120
T = 3.04
O = 120
T = 3.04
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 120
T = 12.90
(out)(err)
O = 120
T = 12.37
(out)(err)
frb15-9-3.wcnf O = 120
T = 0.78
O = 120
T = 2.13
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 120
T = 288.84
(out)(err)
O = 120
T = 0.78
(out)(err)
frb15-9-4.wcnf O = 120
T = 1.22
O = 120
T = 3.36
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 120
T = 3.49
(out)(err)
O = 120
T = 1.22
(out)(err)
frb15-9-5.wcnf O = 120
T = 3.75
O = 120
T = 3.75
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 120
T = 16.45
(out)(err)
O = 120
T = 5.49
(out)(err)
frb20-11-1.wcnf O = 200
T = 4.70
O = 200
T = 4.70
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 202
T = 13.21
(out)(err)
O = 200
T = 40.47
(out)(err)
frb20-11-2.wcnf O = 200
T = 5.66
O = 200
T = 5.66
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 200
T = 124.68
(out)(err)
O = 200
T = 12.23
(out)(err)
frb20-11-3.wcnf O = 200
T = 5.48
O = 200
T = 5.48
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 201
T = 73.32
(out)(err)
O = 200
T = 15.55
(out)(err)
frb20-11-4.wcnf O = 200
T = 5.27
O = 200
T = 5.27
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 202
T = 52.75
(out)(err)
O = 200
T = 24.35
(out)(err)
frb20-11-5.wcnf O = 200
T = 0.31
O = 200
T = 5.57
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 201
T = 102.57
(out)(err)
O = 200
T = 0.31
(out)(err)
frb25-13-1.wcnf O = 300
T = 6.84
O = 300
T = 6.84
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 303
T = 7.10
(out)(err)
O = 300
T = 15.66
(out)(err)
frb25-13-2.wcnf O = 300
T = 7.07
O = 300
T = 7.07
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 300
T = 132.26
(out)(err)
frb25-13-3.wcnf O = 300
T = 1.27
O = 300
T = 7.11
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 302
T = 33.80
(out)(err)
O = 300
T = 1.27
(out)(err)
frb25-13-4.wcnf O = 300
T = 4.52
O = 300
T = 6.97
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 300
T = 4.52
(out)(err)
frb25-13-5.wcnf O = 300
T = 6.80
O = 300
T = 6.80
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 303
T = 7.00
(out)(err)
O = 300
T = 188.72
(out)(err)
frb30-15-1.wcnf O = 420
T = 8.51
O = 420
T = 8.51
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 420
T = 25.21
(out)(err)
frb30-15-2.wcnf O = 420
T = 8.72
O = 420
T = 8.72
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 425
T = 7.71
(out)(err)
O = 420
T = 51.16
(out)(err)
frb30-15-3.wcnf O = 420
T = 11.27
O = 420
T = 11.27
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 423
T = 64.05
(out)(err)
O = 421
T = 12.16
(out)(err)
frb30-15-4.wcnf O = 420
T = 11.25
O = 420
T = 11.25
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 424
T = 150.49
(out)(err)
O = 420
T = 13.51
(out)(err)
frb30-15-5.wcnf O = 420
T = 11.47
O = 420
T = 11.47
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 424
T = 61.87
(out)(err)
O = 420
T = 61.10
(out)(err)
frb35-17-1.wcnf O = 560
T = 17.89
O = 560
T = 17.89
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 562
T = 120.71
(out)(err)
frb35-17-2.wcnf O = 560
T = 14.76
O = 560
T = 14.76
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 562
T = 10.50
(out)(err)
frb35-17-3.wcnf O = 560
T = 14.98
O = 560
T = 14.98
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 560
T = 76.47
(out)(err)
frb35-17-4.wcnf O = 560
T = 59.89
O = 560
T = 59.89
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 567
T = 10.25
(out)(err)
O = 1774
T = 0.43
(out)(err)
frb35-17-5.wcnf O = 560
T = 14.49
O = 560
T = 14.49
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 565
T = 10.89
(out)(err)
O = 582
T = 0.39
(out)(err)
frb40-19-1.wcnf O = 720
T = 16.45
O = 720
T = 16.45
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 720
T = 138.08
(out)(err)
frb40-19-2.wcnf O = 720
T = 29.61
O = 720
T = 29.61
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 723
T = 5.91
(out)(err)
frb40-19-3.wcnf O = 720
T = 15.67
O = 720
T = 15.67
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 722
T = 26.07
(out)(err)
frb40-19-4.wcnf O = 720
T = 16.02
O = 720
T = 16.02
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 3789
T = 0.66
(out)(err)
frb40-19-5.wcnf O = 720
T = 13.99
O = 720
T = 13.99
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 729
T = 10.68
(out)(err)
O = 720
T = 207.33
(out)(err)
ram_k3_n10.ra1.wcnf O = 232
T = 1.65
O = 232
T = 1.65
(out)(err)
O = 232
T = 9.14
(out)(err)
O = 232
T = 7.06
(out)(err)
O = 232
T = 2.51
(out)(err)
O = N/A
T = TO
(out)(err)
ram_k3_n11.ra1.wcnf O = 318
T = 1.85
O = 318
T = 1.85
(out)(err)
O = 318
T = 22.36
(out)(err)
O = 318
T = 26.99
(out)(err)
O = 318
T = 7.38
(out)(err)
O = N/A
T = TO
(out)(err)
ram_k3_n12.ra1.wcnf O = 524
T = 1.06
O = 524
T = 2.65
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 524
T = 1.06
(out)(err)
O = N/A
T = TO
(out)(err)
ram_k3_n13.ra1.wcnf O = 1417
T = 2.02
O = 1417
T = 2.64
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1417
T = 2.02
(out)(err)
O = N/A
T = TO
(out)(err)
ram_k3_n14.ra1.wcnf O = 3025
T = 2.79
O = 3025
T = 2.79
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 3025
T = 32.13
(out)(err)
O = N/A
T = TO
(out)(err)
ram_k3_n15.ra1.wcnf O = 4884
T = 3.01
O = 4884
T = 3.01
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 4922
T = 122.90
(out)(err)
O = N/A
T = TO
(out)(err)
ram_k3_n16.ra1.wcnf O = 7271
T = 2.92
O = 7271
T = 2.92
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 7271
T = 18.35
(out)(err)
O = N/A
T = TO
(out)(err)
ram_k3_n17.ra1.wcnf O = 10372
T = 4.01
O = 10372
T = 4.01
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 10379
T = 64.86
(out)(err)
O = N/A
T = TO
(out)(err)
ram_k3_n18.ra1.wcnf O = 15621
T = 38.69
O = 15621
T = 38.69
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 15786
T = 55.71
(out)(err)
O = N/A
T = TO
(out)(err)
ram_k3_n19.ra1.wcnf O = 20665
T = 153.58
O = 20665
T = 153.58
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 21016
T = 167.08
(out)(err)
O = N/A
T = TO
(out)(err)
ram_k3_n20.ra1.wcnf O = 23898
T = 75.08
O = 23898
T = 75.08
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 24404
T = 117.88
(out)(err)
O = N/A
T = TO
(out)(err)
ram_k3_n9.ra1.wcnf O = 7
T = 0.47
O = 7
T = 0.90
(out)(err)
O = 7
T = 2.48
(out)(err)
O = 7
T = 3.04
(out)(err)
O = 7
T = 0.47
(out)(err)
O = N/A
T = TO
(out)(err)
ram_k4_n18.ra1.wcnf O = 437
T = 52.61
O = 437
T = 52.61
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 585
T = 100.46
(out)(err)
O = N/A
T = TO
(out)(err)
ram_k4_n19.ra1.wcnf O = 1181
T = 289.38
O = 1274
T = 236.45
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1181
T = 289.38
(out)(err)
O = N/A
T = TO
(out)(err)
ram_k4_n20.ra1.wcnf O = 2845
T = 19.80
O = 2845
T = 19.80
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 4062
T = 179.31
(out)(err)
O = N/A
T = TO
(out)(err)
MANN_a27.clq.wcnf O = 2049
T = 1.03
O = 2049
T = 1.03
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 2049
T = 1.05
(out)(err)
O = 2772
T = 0.09
(out)(err)
MANN_a45.clq.wcnf O = 2057
T = 1.00
O = 2057
T = 1.00
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 2057
T = 1.04
(out)(err)
O = 2912
T = 0.11
(out)(err)
MANN_a81.clq.wcnf O = 1995
T = 0.85
O = 1995
T = 0.85
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1995
T = 0.94
(out)(err)
O = 2458
T = 0.10
(out)(err)
MANN_a9.clq.wcnf O = 2179
T = 0.90
O = 2179
T = 0.90
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 2179
T = 1.18
(out)(err)
O = 3260
T = 0.10
(out)(err)
brock200_1.clq.wcnf O = 1254
T = 0.77
O = 1254
T = 0.77
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1254
T = 0.79
(out)(err)
O = 1930
T = 0.10
(out)(err)
brock200_2.clq.wcnf O = 753
T = 0.90
O = 753
T = 1.23
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 753
T = 0.90
(out)(err)
O = 1246
T = 0.10
(out)(err)
brock200_3.clq.wcnf O = 1102
T = 0.84
O = 1102
T = 0.84
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1102
T = 1.04
(out)(err)
O = 1964
T = 0.09
(out)(err)
brock200_4.clq.wcnf O = 1105
T = 0.70
O = 1105
T = 1.17
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1105
T = 0.70
(out)(err)
O = 1685
T = 0.12
(out)(err)
brock400_1.clq.wcnf O = 1361
T = 1.41
O = 1361
T = 1.41
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1361
T = 4.75
(out)(err)
O = 1970
T = 0.10
(out)(err)
brock400_2.clq.wcnf O = 1355
T = 0.99
O = 1355
T = 1.33
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1355
T = 0.99
(out)(err)
O = 1755
T = 0.11
(out)(err)
brock400_3.clq.wcnf O = 1259
T = 0.71
O = 1259
T = 1.23
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1259
T = 0.71
(out)(err)
O = 1643
T = 0.12
(out)(err)
brock400_4.clq.wcnf O = 1290
T = 0.98
O = 1290
T = 0.98
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1290
T = 1.22
(out)(err)
O = 2143
T = 0.10
(out)(err)
brock800_1.clq.wcnf O = 1071
T = 0.85
O = 1071
T = 1.09
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1071
T = 0.85
(out)(err)
O = 1499
T = 0.10
(out)(err)
brock800_2.clq.wcnf O = 1076
T = 1.48
O = 1076
T = 1.48
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1076
T = 5.99
(out)(err)
O = 1481
T = 0.10
(out)(err)
brock800_3.clq.wcnf O = 1079
T = 1.18
O = 1079
T = 1.38
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1079
T = 1.18
(out)(err)
O = 1781
T = 0.12
(out)(err)
brock800_4.clq.wcnf O = 1050
T = 1.25
O = 1050
T = 1.32
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1050
T = 1.25
(out)(err)
O = 1713
T = 0.09
(out)(err)
c-fat200-1.clq.wcnf O = 14
T = 0.00
O = 14
T = 0.97
(out)(err)
O = 14
T = 0.43
(out)(err)
O = 14
T = 0.42
(out)(err)
O = 14
T = 0.69
(out)(err)
O = 14
T = 0.00
(out)(err)
c-fat200-2.clq.wcnf O = 167
T = 0.96
O = 167
T = 1.04
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 167
T = 0.96
(out)(err)
O = 197
T = 244.75
(out)(err)
c-fat200-5.clq.wcnf O = 613
T = 0.61
O = 613
T = 1.19
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 613
T = 0.61
(out)(err)
O = 974
T = 0.12
(out)(err)
c-fat500-1.clq.wcnf O = 10
T = 0.00
O = 10
T = 0.96
(out)(err)
O = 10
T = 0.26
(out)(err)
O = 10
T = 0.24
(out)(err)
O = 10
T = 0.00
(out)(err)
O = 10
T = 0.00
(out)(err)
c-fat500-10.clq.wcnf O = 947
T = 0.96
O = 947
T = 0.98
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 947
T = 0.96
(out)(err)
O = 1307
T = 0.11
(out)(err)
c-fat500-2.clq.wcnf O = 97
T = 0.01
O = 97
T = 0.77
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 97
T = 0.61
(out)(err)
O = 97
T = 0.01
(out)(err)
c-fat500-5.clq.wcnf O = 404
T = 0.65
O = 404
T = 0.94
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 404
T = 0.65
(out)(err)
O = 404
T = 2.59
(out)(err)
hamming10-2.clq.wcnf O = 1929
T = 1.29
O = 1929
T = 1.29
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1929
T = 1.37
(out)(err)
O = 2989
T = 0.13
(out)(err)
hamming10-4.clq.wcnf O = 1683
T = 1.20
O = 1683
T = 1.20
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1683
T = 1.72
(out)(err)
O = 1885
T = 0.09
(out)(err)
hamming6-2.clq.wcnf O = 4391
T = 2.01
O = 4391
T = 2.01
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 4391
T = 36.73
(out)(err)
O = 6065
T = 0.13
(out)(err)
hamming6-4.clq.wcnf O = 1035
T = 1.41
O = 1035
T = 1.75
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1035
T = 1.41
(out)(err)
O = 1800
T = 0.09
(out)(err)
hamming8-2.clq.wcnf O = 2213
T = 1.17
O = 2213
T = 1.34
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 2213
T = 1.17
(out)(err)
O = 3111
T = 0.12
(out)(err)
hamming8-4.clq.wcnf O = 917
T = 1.17
O = 917
T = 1.17
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 917
T = 1.41
(out)(err)
O = 1409
T = 0.11
(out)(err)
johnson16-2-4.clq.wcnf O = 1170
T = 0.94
O = 1170
T = 0.94
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1170
T = 1.00
(out)(err)
O = 1905
T = 0.12
(out)(err)
johnson32-2-4.clq.wcnf O = 1788
T = 0.95
O = 1788
T = 1.20
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1788
T = 0.95
(out)(err)
O = 2774
T = 0.10
(out)(err)
johnson8-2-4.clq.wcnf O = 392
T = 0.65
O = 392
T = 1.14
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 392
T = 0.65
(out)(err)
O = 565
T = 0.08
(out)(err)
johnson8-4-4.clq.wcnf O = 4154
T = 1.86
O = 4154
T = 1.86
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 4154
T = 2.50
(out)(err)
O = 5837
T = 0.11
(out)(err)
keller4.clq.wcnf O = 1133
T = 1.12
O = 1133
T = 1.12
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1133
T = 1.42
(out)(err)
O = 2017
T = 0.10
(out)(err)
keller5.clq.wcnf O = 1383
T = 1.10
O = 1383
T = 1.10
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1383
T = 1.13
(out)(err)
O = 1859
T = 0.07
(out)(err)
p_hat1000-1.clq.wcnf O = 248
T = 1.06
O = 248
T = 1.42
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 248
T = 1.06
(out)(err)
O = 429
T = 0.07
(out)(err)
p_hat1000-2.clq.wcnf O = 752
T = 0.78
O = 752
T = 1.39
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 752
T = 0.78
(out)(err)
O = 1003
T = 0.07
(out)(err)
p_hat1000-3.clq.wcnf O = 1251
T = 0.69
O = 1251
T = 1.16
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1251
T = 0.69
(out)(err)
O = 2002
T = 0.04
(out)(err)
p_hat300-1.clq.wcnf O = 243
T = 0.69
O = 243
T = 1.49
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 243
T = 0.69
(out)(err)
O = 384
T = 0.07
(out)(err)
p_hat300-2.clq.wcnf O = 711
T = 0.95
O = 711
T = 0.95
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 711
T = 1.79
(out)(err)
O = 1021
T = 0.08
(out)(err)
p_hat300-3.clq.wcnf O = 1439
T = 1.26
O = 1439
T = 1.26
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1439
T = 4.25
(out)(err)
O = 1826
T = 0.10
(out)(err)
p_hat500-1.clq.wcnf O = 395
T = 0.84
O = 395
T = 1.61
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 395
T = 0.84
(out)(err)
O = 595
T = 0.10
(out)(err)
p_hat500-2.clq.wcnf O = 931
T = 0.84
O = 931
T = 0.84
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 931
T = 0.89
(out)(err)
O = 1369
T = 0.09
(out)(err)
p_hat500-3.clq.wcnf O = 1501
T = 0.66
O = 1501
T = 1.04
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1501
T = 0.66
(out)(err)
O = 2459
T = 0.09
(out)(err)
p_hat700-1.clq.wcnf O = 329
T = 1.25
O = 329
T = 1.31
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 329
T = 1.25
(out)(err)
O = 559
T = 0.08
(out)(err)
p_hat700-2.clq.wcnf O = 834
T = 1.35
O = 834
T = 1.35
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 834
T = 2.15
(out)(err)
O = 1297
T = 0.10
(out)(err)
p_hat700-3.clq.wcnf O = 1432
T = 1.35
O = 1432
T = 1.67
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1432
T = 1.35
(out)(err)
O = 2259
T = 0.11
(out)(err)
san1000.clq.wcnf O = 744
T = 0.90
O = 744
T = 1.22
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 744
T = 0.90
(out)(err)
O = 1308
T = 0.09
(out)(err)
san200_0.7_1.clq.wcnf O = 1256
T = 0.86
O = 1256
T = 1.28
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1256
T = 0.86
(out)(err)
O = 1733
T = 0.08
(out)(err)
san200_0.7_2.clq.wcnf O = 1243
T = 0.92
O = 1243
T = 1.39
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1243
T = 0.92
(out)(err)
O = 1637
T = 0.11
(out)(err)
san200_0.9_1.clq.wcnf O = 1672
T = 1.22
O = 1672
T = 1.22
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1672
T = 10.57
(out)(err)
O = 2280
T = 0.10
(out)(err)
san200_0.9_2.clq.wcnf O = 1647
T = 0.75
O = 1647
T = 1.12
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1647
T = 0.75
(out)(err)
O = 2472
T = 0.10
(out)(err)
san200_0.9_3.clq.wcnf O = 1670
T = 0.82
O = 1670
T = 1.39
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1670
T = 0.82
(out)(err)
O = 2418
T = 0.12
(out)(err)
san400_0.5_1.clq.wcnf O = 718
T = 1.46
O = 718
T = 1.48
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 718
T = 1.46
(out)(err)
O = 1242
T = 0.10
(out)(err)
san400_0.7_1.clq.wcnf O = 1258
T = 1.05
O = 1258
T = 1.09
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1258
T = 1.05
(out)(err)
O = 1929
T = 0.08
(out)(err)
san400_0.7_2.clq.wcnf O = 1237
T = 1.28
O = 1237
T = 1.28
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1237
T = 1.79
(out)(err)
O = 1752
T = 0.11
(out)(err)
san400_0.7_3.clq.wcnf O = 1201
T = 0.88
O = 1201
T = 0.88
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1201
T = 3.39
(out)(err)
O = 1681
T = 0.10
(out)(err)
san400_0.9_1.clq.wcnf O = 1604
T = 1.36
O = 1604
T = 1.36
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1604
T = 13.24
(out)(err)
O = 2656
T = 0.09
(out)(err)
sanr200_0.7.clq.wcnf O = 1171
T = 1.30
O = 1171
T = 1.56
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1171
T = 1.30
(out)(err)
O = 1546
T = 0.11
(out)(err)
sanr200_0.9.clq.wcnf O = 1610
T = 1.08
O = 1610
T = 1.49
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1610
T = 1.08
(out)(err)
O = 2351
T = 0.12
(out)(err)
sanr400_0.5.clq.wcnf O = 763
T = 0.85
O = 763
T = 1.44
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 763
T = 0.85
(out)(err)
O = 1025
T = 0.14
(out)(err)
sanr400_0.7.clq.wcnf O = 1198
T = 0.72
O = 1198
T = 1.23
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1198
T = 0.72
(out)(err)
O = 1834
T = 0.13
(out)(err)
t3g3-5555.spn.wcnf O = 1100610
T = 0.59
O = 1100610
T = 1.34
(out)(err)
O = 1100610
T = 275.61
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1100610
T = 0.59
(out)(err)
O = 1128668
T = 178.06
(out)(err)
t4g3-6666.spn.wcnf O = 2275606
T = 1.65
O = 2275606
T = 1.92
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 2275606
T = 1.65
(out)(err)
O = 5449756
T = 0.13
(out)(err)
t5g3-7777.spn.wcnf O = 4241951
T = 3.16
O = 4241951
T = 3.16
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 4241951
T = 39.29
(out)(err)
O = 8202693
T = 0.11
(out)(err)
t6g3-8888.spn.wcnf O = 7844119
T = 5.19
O = 7844119
T = 5.19
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 8015335
T = 153.02
(out)(err)
O = 18418298
T = 0.13
(out)(err)
t7g3-9999.spn.wcnf O = 12140924
T = 164.91
O = 12140924
T = 164.91
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 12415992
T = 26.59
(out)(err)
O = 30381168
T = 0.08
(out)(err)