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 SAT4Jms-ext-i SAT4Jms-int-i optimax-it
frb20-11-1.partial.wcnf O = 200
T = 65.74		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 200
T = 65.74
(out)(err)
frb20-11-2.partial.wcnf O = 204
T = 27.95		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 204
T = 27.95
(out)(err)
frb20-11-3.partial.wcnf O = 203
T = 43.18		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 203
T = 43.18
(out)(err)
frb20-11-4.partial.wcnf O = 217
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 217
T = 0.13
(out)(err)
frb20-11-5.partial.wcnf O = 200
T = 123.54		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 200
T = 123.54
(out)(err)
frb25-13-1.partial.wcnf O = 305
T = 92.93		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 305
T = 92.93
(out)(err)
frb25-13-2.partial.wcnf O = 321
T = 0.10		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 321
T = 0.10
(out)(err)
frb25-13-3.partial.wcnf O = 302
T = 44.10		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 302
T = 44.10
(out)(err)
frb25-13-4.partial.wcnf O = 305
T = 121.86		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 305
T = 121.86
(out)(err)
frb25-13-5.partial.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 322
T = 0.10
(out)(err)
frb30-15-1.partial.wcnf O = 449
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 449
T = 0.13
(out)(err)
frb30-15-2.partial.wcnf O = 446
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 446
T = 0.09
(out)(err)
frb30-15-3.partial.wcnf O = 449
T = 0.11		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 449
T = 0.11
(out)(err)
frb30-15-4.partial.wcnf O = 447
T = 0.12		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 447
T = 0.12
(out)(err)
frb30-15-5.partial.wcnf O = 447
T = 0.12		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 447
T = 0.12
(out)(err)
frb35-17-1.partial.wcnf O = 592
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 592
T = 0.09
(out)(err)
frb35-17-2.partial.wcnf O = 591
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 591
T = 0.13
(out)(err)
frb35-17-3.partial.wcnf O = 591
T = 0.11		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 591
T = 0.11
(out)(err)
frb35-17-4.partial.wcnf O = 592
T = 0.14		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 592
T = 0.14
(out)(err)
frb35-17-5.partial.wcnf O = 594
T = 0.11		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 594
T = 0.11
(out)(err)
frb40-19-1.partial.wcnf O = 757
T = 0.17		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 757
T = 0.17
(out)(err)
frb40-19-2.partial.wcnf O = 757
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 757
T = 0.13
(out)(err)
frb40-19-3.partial.wcnf O = 758
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 758
T = 0.13
(out)(err)
frb40-19-4.partial.wcnf O = 757
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 757
T = 0.13
(out)(err)
frb40-19-5.partial.wcnf O = 758
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 758
T = 0.13
(out)(err)
ft10-808-1090.wcnf O = 122
T = 108.36		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 122
T = 108.36
(out)(err)
la04-567-0696.wcnf O = 23
T = 2.25		 O = 23
T = 21.99
(out)(err)		 O = 23
T = 11.01
(out)(err)		 O = 23
T = 2.25
(out)(err)
orb08-894-1058.wcnf O = 5
T = 26.96		 O = N/A
T = TO
(out)(err)		 O = 5
T = 65.26
(out)(err)		 O = 5
T = 26.96
(out)(err)
max_clq_150-0-447-1.clq.wcnf O = 147
T = 0.17		 O = 147
T = 1.47
(out)(err)		 O = 147
T = 1.51
(out)(err)		 O = 147
T = 0.17
(out)(err)
max_clq_150-0-447-2.clq.wcnf O = 147
T = 0.18		 O = 147
T = 1.34
(out)(err)		 O = 147
T = 1.44
(out)(err)		 O = 147
T = 0.18
(out)(err)
max_clq_150-0-447-3.clq.wcnf O = 147
T = 0.19		 O = 147
T = 1.48
(out)(err)		 O = 147
T = 1.35
(out)(err)		 O = 147
T = 0.19
(out)(err)
max_clq_150-0-447-4.clq.wcnf O = 147
T = 0.18		 O = 147
T = 1.64
(out)(err)		 O = 147
T = 1.50
(out)(err)		 O = 147
T = 0.18
(out)(err)
max_clq_150-1-894-1.clq.wcnf O = 146
T = 0.24		 O = 146
T = 1.64
(out)(err)		 O = 146
T = 1.61
(out)(err)		 O = 146
T = 0.24
(out)(err)
max_clq_150-1-894-2.clq.wcnf O = 146
T = 0.19		 O = 146
T = 1.63
(out)(err)		 O = 146
T = 1.62
(out)(err)		 O = 146
T = 0.19
(out)(err)
max_clq_150-1-894-3.clq.wcnf O = 146
T = 0.24		 O = 146
T = 1.61
(out)(err)		 O = 146
T = 1.67
(out)(err)		 O = 146
T = 0.24
(out)(err)
max_clq_150-1-894-4.clq.wcnf O = 146
T = 0.24		 O = 146
T = 2.00
(out)(err)		 O = 146
T = 1.71
(out)(err)		 O = 146
T = 0.24
(out)(err)
max_clq_150-10-4917-1.clq.wcnf O = 141
T = 3.01		 O = 141
T = 8.39
(out)(err)		 O = 141
T = 3.01
(out)(err)		 O = 141
T = 35.06
(out)(err)
max_clq_150-10-4917-2.clq.wcnf O = 141
T = 2.42		 O = 141
T = 2.42
(out)(err)		 O = 141
T = 3.97
(out)(err)		 O = 141
T = 32.75
(out)(err)
max_clq_150-10-4917-3.clq.wcnf O = 141
T = 1.78		 O = 141
T = 1.78
(out)(err)		 O = 141
T = 2.83
(out)(err)		 O = 141
T = 36.36
(out)(err)
max_clq_150-10-4917-4.clq.wcnf O = 141
T = 2.87		 O = 141
T = 4.86
(out)(err)		 O = 141
T = 2.87
(out)(err)		 O = 141
T = 34.64
(out)(err)
max_clq_150-11-5364-1.clq.wcnf O = 140
T = 2.31		 O = 140
T = 2.31
(out)(err)		 O = 140
T = 3.34
(out)(err)		 O = 140
T = 57.87
(out)(err)
max_clq_150-11-5364-2.clq.wcnf O = 141
T = 2.56		 O = 141
T = 2.56
(out)(err)		 O = 141
T = 2.69
(out)(err)		 O = 141
T = 64.74
(out)(err)
max_clq_150-11-5364-3.clq.wcnf O = 140
T = 2.99		 O = 140
T = 2.99
(out)(err)		 O = 140
T = 6.52
(out)(err)		 O = 140
T = 48.85
(out)(err)
max_clq_150-11-5364-4.clq.wcnf O = 140
T = 3.56		 O = 140
T = 3.56
(out)(err)		 O = 140
T = 7.45
(out)(err)		 O = 140
T = 30.38
(out)(err)
max_clq_150-12-5811-1.clq.wcnf O = 140
T = 2.53		 O = 140
T = 2.65
(out)(err)		 O = 140
T = 2.53
(out)(err)		 O = 140
T = 90.07
(out)(err)
max_clq_150-12-5811-2.clq.wcnf O = 140
T = 2.72		 O = 140
T = 3.00
(out)(err)		 O = 140
T = 2.72
(out)(err)		 O = 140
T = 44.40
(out)(err)
max_clq_150-12-5811-3.clq.wcnf O = 139
T = 2.75		 O = 139
T = 22.45
(out)(err)		 O = 139
T = 2.75
(out)(err)		 O = 139
T = 34.08
(out)(err)
max_clq_150-12-5811-4.clq.wcnf O = 140
T = 3.01		 O = 140
T = 3.33
(out)(err)		 O = 140
T = 3.01
(out)(err)		 O = 140
T = 63.01
(out)(err)
max_clq_150-13-6258-1.clq.wcnf O = 138
T = 13.86		 O = 138
T = 13.86
(out)(err)		 O = 138
T = 25.08
(out)(err)		 O = 138
T = 119.25
(out)(err)
max_clq_150-13-6258-2.clq.wcnf O = 139
T = 2.99		 O = 139
T = 2.99
(out)(err)		 O = 139
T = 4.63
(out)(err)		 O = 139
T = 127.55
(out)(err)
max_clq_150-13-6258-3.clq.wcnf O = 138
T = 19.05		 O = 138
T = 136.38
(out)(err)		 O = 138
T = 19.05
(out)(err)		 O = 138
T = 62.52
(out)(err)
max_clq_150-13-6258-4.clq.wcnf O = 138
T = 3.00		 O = 138
T = 11.74
(out)(err)		 O = 138
T = 3.00
(out)(err)		 O = 138
T = 50.86
(out)(err)
max_clq_150-14-6705-1.clq.wcnf O = 138
T = 226.72		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 138
T = 226.72
(out)(err)
max_clq_150-14-6705-2.clq.wcnf O = 137
T = 192.78		 O = 137
T = 269.99
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 137
T = 192.78
(out)(err)
max_clq_150-14-6705-3.clq.wcnf O = 137
T = 64.58		 O = 137
T = 64.58
(out)(err)		 O = 137
T = 133.94
(out)(err)		 O = 137
T = 146.54
(out)(err)
max_clq_150-14-6705-4.clq.wcnf O = 137
T = 17.70		 O = 137
T = 17.70
(out)(err)		 O = 137
T = 32.39
(out)(err)		 O = 137
T = 173.82
(out)(err)
max_clq_150-15-7152-1.clq.wcnf O = 135
T = 189.02		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 135
T = 189.02
(out)(err)
max_clq_150-15-7152-2.clq.wcnf O = 136
T = 169.54		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 136
T = 169.54
(out)(err)
max_clq_150-15-7152-3.clq.wcnf O = 135
T = 171.48		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 135
T = 171.48
(out)(err)
max_clq_150-15-7152-4.clq.wcnf O = 136
T = 144.38		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 136
T = 144.38
(out)(err)
max_clq_150-16-7599-1.clq.wcnf O = 145
T = 0.12		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 145
T = 0.12
(out)(err)
max_clq_150-16-7599-2.clq.wcnf O = 144
T = 0.11		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 144
T = 0.11
(out)(err)
max_clq_150-16-7599-3.clq.wcnf O = 144
T = 0.08		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 144
T = 0.08
(out)(err)
max_clq_150-16-7599-4.clq.wcnf O = 146
T = 0.08		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 146
T = 0.08
(out)(err)
max_clq_150-17-8046-1.clq.wcnf O = 134
T = 7.08		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 134
T = 7.08
(out)(err)
max_clq_150-17-8046-2.clq.wcnf O = 142
T = 0.08		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 142
T = 0.08
(out)(err)
max_clq_150-17-8046-3.clq.wcnf O = 132
T = 5.83		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 132
T = 5.83
(out)(err)
max_clq_150-17-8046-4.clq.wcnf O = 141
T = 0.11		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 141
T = 0.11
(out)(err)
max_clq_150-18-8493-1.clq.wcnf O = 132
T = 7.66		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 132
T = 7.66
(out)(err)
max_clq_150-18-8493-2.clq.wcnf O = 144
T = 0.10		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 144
T = 0.10
(out)(err)
max_clq_150-18-8493-3.clq.wcnf O = 132
T = 4.38		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 132
T = 4.38
(out)(err)
max_clq_150-18-8493-4.clq.wcnf O = 132
T = 9.17		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 132
T = 9.17
(out)(err)
max_clq_150-19-8940-1.clq.wcnf O = 129
T = 15.58		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 129
T = 15.58
(out)(err)
max_clq_150-19-8940-2.clq.wcnf O = 130
T = 30.96		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 130
T = 30.96
(out)(err)
max_clq_150-19-8940-3.clq.wcnf O = 129
T = 16.80		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 129
T = 16.80
(out)(err)
max_clq_150-19-8940-4.clq.wcnf O = 129
T = 18.38		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 129
T = 18.38
(out)(err)
max_clq_150-2-1341-1.clq.wcnf O = 146
T = 0.32		 O = 146
T = 1.28
(out)(err)		 O = 146
T = 1.32
(out)(err)		 O = 146
T = 0.32
(out)(err)
max_clq_150-2-1341-2.clq.wcnf O = 146
T = 0.43		 O = 146
T = 1.19
(out)(err)		 O = 146
T = 1.24
(out)(err)		 O = 146
T = 0.43
(out)(err)
max_clq_150-2-1341-3.clq.wcnf O = 146
T = 0.30		 O = 146
T = 1.30
(out)(err)		 O = 146
T = 1.22
(out)(err)		 O = 146
T = 0.30
(out)(err)
max_clq_150-2-1341-4.clq.wcnf O = 145
T = 0.32		 O = 145
T = 1.36
(out)(err)		 O = 145
T = 1.25
(out)(err)		 O = 145
T = 0.32
(out)(err)
max_clq_150-20-9387-1.clq.wcnf O = 140
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 140
T = 0.09
(out)(err)
max_clq_150-20-9387-2.clq.wcnf O = 129
T = 226.05		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 129
T = 226.05
(out)(err)
max_clq_150-20-9387-3.clq.wcnf O = 140
T = 0.10		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 140
T = 0.10
(out)(err)
max_clq_150-20-9387-4.clq.wcnf O = 138
T = 0.12		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 138
T = 0.12
(out)(err)
max_clq_150-21-9834-1.clq.wcnf O = 117
T = 295.26		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 117
T = 295.26
(out)(err)
max_clq_150-21-9834-2.clq.wcnf O = 135
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 135
T = 0.09
(out)(err)
max_clq_150-21-9834-3.clq.wcnf O = 135
T = 0.10		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 135
T = 0.10
(out)(err)
max_clq_150-21-9834-4.clq.wcnf O = 135
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 135
T = 0.09
(out)(err)
max_clq_150-22-10281-1.clq.wcnf O = 109
T = 16.20		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 109
T = 16.20
(out)(err)
max_clq_150-22-10281-2.clq.wcnf O = 127
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 127
T = 0.09
(out)(err)
max_clq_150-22-10281-3.clq.wcnf O = 128
T = 0.10		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 128
T = 0.10
(out)(err)
max_clq_150-22-10281-4.clq.wcnf O = 108
T = 45.75		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 108
T = 45.75
(out)(err)
max_clq_150-23-10728-1.clq.wcnf O = 91
T = 298.12		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 91
T = 298.12
(out)(err)
max_clq_150-23-10728-2.clq.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 91
T = 0.22
(out)(err)
max_clq_150-23-10728-3.clq.wcnf O = 91
T = 267.91		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 91
T = 267.91
(out)(err)
max_clq_150-23-10728-4.clq.wcnf O = 90
T = 257.78		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 90
T = 257.78
(out)(err)
max_clq_150-3-1788-1.clq.wcnf O = 145
T = 0.77		 O = 145
T = 1.47
(out)(err)		 O = 145
T = 1.43
(out)(err)		 O = 145
T = 0.77
(out)(err)
max_clq_150-3-1788-2.clq.wcnf O = 145
T = 0.62		 O = 145
T = 1.31
(out)(err)		 O = 145
T = 1.39
(out)(err)		 O = 145
T = 0.62
(out)(err)
max_clq_150-3-1788-3.clq.wcnf O = 145
T = 0.61		 O = 145
T = 1.29
(out)(err)		 O = 145
T = 1.28
(out)(err)		 O = 145
T = 0.61
(out)(err)
max_clq_150-3-1788-4.clq.wcnf O = 145
T = 0.58		 O = 145
T = 1.24
(out)(err)		 O = 145
T = 1.25
(out)(err)		 O = 145
T = 0.58
(out)(err)
max_clq_150-4-2235-1.clq.wcnf O = 144
T = 1.05		 O = 144
T = 1.46
(out)(err)		 O = 144
T = 1.51
(out)(err)		 O = 144
T = 1.05
(out)(err)
max_clq_150-4-2235-2.clq.wcnf O = 145
T = 1.08		 O = 145
T = 1.25
(out)(err)		 O = 145
T = 1.45
(out)(err)		 O = 145
T = 1.08
(out)(err)
max_clq_150-4-2235-3.clq.wcnf O = 144
T = 1.50		 O = 144
T = 1.62
(out)(err)		 O = 144
T = 1.54
(out)(err)		 O = 144
T = 1.50
(out)(err)
max_clq_150-4-2235-4.clq.wcnf O = 145
T = 1.04		 O = 145
T = 1.30
(out)(err)		 O = 145
T = 1.62
(out)(err)		 O = 145
T = 1.04
(out)(err)
max_clq_150-5-2682-1.clq.wcnf O = 144
T = 1.12		 O = 144
T = 1.63
(out)(err)		 O = 144
T = 1.73
(out)(err)		 O = 144
T = 1.12
(out)(err)
max_clq_150-5-2682-2.clq.wcnf O = 144
T = 1.33		 O = 144
T = 1.74
(out)(err)		 O = 144
T = 1.80
(out)(err)		 O = 144
T = 1.33
(out)(err)
max_clq_150-5-2682-3.clq.wcnf O = 144
T = 1.27		 O = 144
T = 1.80
(out)(err)		 O = 144
T = 1.46
(out)(err)		 O = 144
T = 1.27
(out)(err)
max_clq_150-5-2682-4.clq.wcnf O = 144
T = 1.63		 O = 144
T = 1.63
(out)(err)		 O = 144
T = 1.73
(out)(err)		 O = 144
T = 1.70
(out)(err)
max_clq_150-6-3129-1.clq.wcnf O = 144
T = 2.37		 O = 144
T = 2.37
(out)(err)		 O = 144
T = 2.70
(out)(err)		 O = 144
T = 3.01
(out)(err)
max_clq_150-6-3129-2.clq.wcnf O = 143
T = 1.93		 O = 143
T = 1.93
(out)(err)		 O = 143
T = 1.97
(out)(err)		 O = 143
T = 2.03
(out)(err)
max_clq_150-6-3129-3.clq.wcnf O = 143
T = 1.85		 O = 143
T = 1.85
(out)(err)		 O = 143
T = 2.58
(out)(err)		 O = 143
T = 2.60
(out)(err)
max_clq_150-6-3129-4.clq.wcnf O = 144
T = 1.86		 O = 144
T = 2.89
(out)(err)		 O = 144
T = 2.55
(out)(err)		 O = 144
T = 1.86
(out)(err)
max_clq_150-7-3576-1.clq.wcnf O = 144
T = 2.78		 O = 144
T = 3.07
(out)(err)		 O = 144
T = 2.78
(out)(err)		 O = 144
T = 4.34
(out)(err)
max_clq_150-7-3576-2.clq.wcnf O = 143
T = 2.76		 O = 143
T = 2.76
(out)(err)		 O = 143
T = 3.18
(out)(err)		 O = 143
T = 7.13
(out)(err)
max_clq_150-7-3576-3.clq.wcnf O = 143
T = 3.20		 O = 143
T = 3.20
(out)(err)		 O = 143
T = 3.31
(out)(err)		 O = 143
T = 5.92
(out)(err)
max_clq_150-7-3576-4.clq.wcnf O = 143
T = 2.81		 O = 143
T = 2.81
(out)(err)		 O = 143
T = 2.92
(out)(err)		 O = 143
T = 6.41
(out)(err)
max_clq_150-8-4023-1.clq.wcnf O = 143
T = 3.02		 O = 143
T = 3.35
(out)(err)		 O = 143
T = 3.02
(out)(err)		 O = 143
T = 8.11
(out)(err)
max_clq_150-8-4023-2.clq.wcnf O = 142
T = 3.08		 O = 142
T = 3.57
(out)(err)		 O = 142
T = 3.08
(out)(err)		 O = 142
T = 10.48
(out)(err)
max_clq_150-8-4023-3.clq.wcnf O = 143
T = 2.99		 O = 143
T = 3.25
(out)(err)		 O = 143
T = 2.99
(out)(err)		 O = 143
T = 13.53
(out)(err)
max_clq_150-8-4023-4.clq.wcnf O = 142
T = 2.78		 O = 142
T = 3.18
(out)(err)		 O = 142
T = 2.78
(out)(err)		 O = 142
T = 7.94
(out)(err)
max_clq_150-9-4470-1.clq.wcnf O = 142
T = 2.90		 O = 142
T = 2.90
(out)(err)		 O = 142
T = 2.97
(out)(err)		 O = 142
T = 14.35
(out)(err)
max_clq_150-9-4470-2.clq.wcnf O = 142
T = 2.22		 O = 142
T = 2.22
(out)(err)		 O = 142
T = 3.22
(out)(err)		 O = 142
T = 19.18
(out)(err)
max_clq_150-9-4470-3.clq.wcnf O = 142
T = 2.03		 O = 142
T = 2.78
(out)(err)		 O = 142
T = 2.03
(out)(err)		 O = 142
T = 23.87
(out)(err)
max_clq_150-9-4470-4.clq.wcnf O = 142
T = 2.13		 O = 142
T = 2.71
(out)(err)		 O = 142
T = 2.13
(out)(err)		 O = 142
T = 21.99
(out)(err)
MANN_a27.clq.wcnf O = 253
T = 0.74		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 253
T = 0.74
(out)(err)
MANN_a45.clq.wcnf O = 705
T = 0.08		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 705
T = 0.08
(out)(err)
MANN_a81.clq.wcnf O = 2239
T = 0.29		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 2239
T = 0.29
(out)(err)
MANN_a9.clq.wcnf O = 29
T = 0.00		 O = 29
T = 2.73
(out)(err)		 O = 29
T = 3.02
(out)(err)		 O = 29
T = 0.00
(out)(err)
brock200_1.clq.wcnf O = 194
T = 0.08		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 194
T = 0.08
(out)(err)
brock200_2.clq.wcnf O = 188
T = 11.74		 O = 188
T = 28.30
(out)(err)		 O = 188
T = 11.74
(out)(err)		 O = 188
T = 219.92
(out)(err)
brock200_3.clq.wcnf O = 187
T = 103.82		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 187
T = 103.82
(out)(err)
brock200_4.clq.wcnf O = 195
T = 0.08		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 195
T = 0.08
(out)(err)
brock400_1.clq.wcnf O = 394
T = 0.10		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 394
T = 0.10
(out)(err)
brock400_2.clq.wcnf O = 393
T = 0.10		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 393
T = 0.10
(out)(err)
brock400_3.clq.wcnf O = 392
T = 0.07		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 392
T = 0.07
(out)(err)
brock400_4.clq.wcnf O = 392
T = 0.07		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 392
T = 0.07
(out)(err)
brock800_1.clq.wcnf O = 794
T = 0.29		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 794
T = 0.29
(out)(err)
brock800_2.clq.wcnf O = 795
T = 0.32		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 795
T = 0.32
(out)(err)
brock800_3.clq.wcnf O = 794
T = 0.39		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 794
T = 0.39
(out)(err)
brock800_4.clq.wcnf O = 796
T = 0.37		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 796
T = 0.37
(out)(err)
c-fat200-1.clq.wcnf O = 188
T = 0.34		 O = 188
T = 1.46
(out)(err)		 O = 188
T = 1.76
(out)(err)		 O = 188
T = 0.34
(out)(err)
c-fat200-2.clq.wcnf O = 176
T = 0.50		 O = 176
T = 1.56
(out)(err)		 O = 176
T = 1.75
(out)(err)		 O = 176
T = 0.50
(out)(err)
c-fat200-5.clq.wcnf O = 142
T = 0.60		 O = 142
T = 1.91
(out)(err)		 O = 142
T = 1.65
(out)(err)		 O = 142
T = 0.60
(out)(err)
c-fat500-1.clq.wcnf O = 486
T = 1.72		 O = 486
T = 2.06
(out)(err)		 O = 486
T = 1.72
(out)(err)		 O = 486
T = 3.25
(out)(err)
c-fat500-10.clq.wcnf O = 374
T = 1.43		 O = 374
T = 2.78
(out)(err)		 O = 374
T = 1.76
(out)(err)		 O = 374
T = 1.43
(out)(err)
c-fat500-2.clq.wcnf O = 474
T = 1.67		 O = 474
T = 2.42
(out)(err)		 O = 474
T = 1.67
(out)(err)		 O = 474
T = 6.96
(out)(err)
c-fat500-5.clq.wcnf O = 436
T = 1.50		 O = 436
T = 2.53
(out)(err)		 O = 436
T = 1.50
(out)(err)		 O = 436
T = 13.81
(out)(err)
hamming10-2.clq.wcnf O = 512
T = 0.04		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 512
T = 0.04
(out)(err)
hamming10-4.clq.wcnf O = 1023
T = 0.30		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 1023
T = 0.30
(out)(err)
hamming6-2.clq.wcnf O = 32
T = 0.00		 O = 32
T = 1.71
(out)(err)		 O = 32
T = 1.48
(out)(err)		 O = 32
T = 0.00
(out)(err)
hamming6-4.clq.wcnf O = 60
T = 0.06		 O = 60
T = 0.71
(out)(err)		 O = 60
T = 0.83
(out)(err)		 O = 60
T = 0.06
(out)(err)
hamming8-2.clq.wcnf O = 128
T = 0.00		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 128
T = 0.00
(out)(err)
hamming8-4.clq.wcnf O = 240
T = 39.88		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 240
T = 39.88
(out)(err)
johnson16-2-4.clq.wcnf O = 112
T = 9.64		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 112
T = 9.64
(out)(err)
johnson32-2-4.clq.wcnf O = 494
T = 0.10		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 494
T = 0.10
(out)(err)
johnson8-2-4.clq.wcnf O = 24
T = 0.00		 O = 24
T = 0.40
(out)(err)		 O = 24
T = 0.45
(out)(err)		 O = 24
T = 0.00
(out)(err)
johnson8-4-4.clq.wcnf O = 56
T = 0.15		 O = 56
T = 3.03
(out)(err)		 O = 56
T = 1.01
(out)(err)		 O = 56
T = 0.15
(out)(err)
keller4.clq.wcnf O = 160
T = 153.96		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 160
T = 153.96
(out)(err)
keller5.clq.wcnf O = 775
T = 0.19		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 775
T = 0.19
(out)(err)
p_hat1000-1.clq.wcnf O = 998
T = 1.26		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 998
T = 1.26
(out)(err)
p_hat1000-2.clq.wcnf O = 996
T = 0.91		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 996
T = 0.91
(out)(err)
p_hat1000-3.clq.wcnf O = 990
T = 0.44		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 990
T = 0.44
(out)(err)
p_hat300-1.clq.wcnf O = 292
T = 3.38		 O = 292
T = 6.41
(out)(err)		 O = 292
T = 3.38
(out)(err)		 O = 292
T = 185.08
(out)(err)
p_hat300-2.clq.wcnf O = 295
T = 0.08		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 295
T = 0.08
(out)(err)
p_hat300-3.clq.wcnf O = 291
T = 0.08		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 291
T = 0.08
(out)(err)
p_hat500-1.clq.wcnf O = 499
T = 0.17		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 499
T = 0.17
(out)(err)
p_hat500-2.clq.wcnf O = 496
T = 0.15		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 496
T = 0.15
(out)(err)
p_hat500-3.clq.wcnf O = 486
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 486
T = 0.09
(out)(err)
p_hat700-1.clq.wcnf O = 699
T = 0.80		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 699
T = 0.80
(out)(err)
p_hat700-2.clq.wcnf O = 698
T = 0.31		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 698
T = 0.31
(out)(err)
p_hat700-3.clq.wcnf O = 689
T = 0.20		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 689
T = 0.20
(out)(err)
san1000.clq.wcnf O = 997
T = 1.26		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 997
T = 1.26
(out)(err)
san200_0.7_1.clq.wcnf O = 176
T = 267.58		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 176
T = 267.58
(out)(err)
san200_0.7_2.clq.wcnf O = 189
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 189
T = 0.09
(out)(err)
san200_0.9_1.clq.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 130
T = 1.72
(out)(err)
san200_0.9_2.clq.wcnf O = 146
T = 0.46		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 146
T = 0.46
(out)(err)
san200_0.9_3.clq.wcnf O = 186
T = 0.10		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 186
T = 0.10
(out)(err)
san400_0.5_1.clq.wcnf O = 396
T = 0.08		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 396
T = 0.08
(out)(err)
san400_0.7_1.clq.wcnf O = 382
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 382
T = 0.09
(out)(err)
san400_0.7_2.clq.wcnf O = 392
T = 0.12		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 392
T = 0.12
(out)(err)
san400_0.7_3.clq.wcnf O = 395
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 395
T = 0.09
(out)(err)
san400_0.9_1.clq.wcnf O = 380
T = 0.08		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 380
T = 0.08
(out)(err)
sanr200_0.7.clq.wcnf O = 194
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 194
T = 0.13
(out)(err)
sanr200_0.9.clq.wcnf O = 182
T = 0.11		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 182
T = 0.11
(out)(err)
sanr400_0.5.clq.wcnf O = 398
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 398
T = 0.09
(out)(err)
sanr400_0.7.clq.wcnf O = 396
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 396
T = 0.09
(out)(err)
cnf3.150.250.832706.cnf.wcnf O = 15
T = 0.00		 O = 15
T = 12.09
(out)(err)		 O = 15
T = 49.28
(out)(err)		 O = 15
T = 0.00
(out)(err)
cnf3.150.250.832707.cnf.wcnf O = 18
T = 0.00		 O = N/A
T = TO
(out)(err)		 O = 18
T = 222.65
(out)(err)		 O = 18
T = 0.00
(out)(err)
cnf3.150.250.832708.cnf.wcnf O = 20
T = 0.00		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 20
T = 0.00
(out)(err)
cnf3.150.250.832709.cnf.wcnf O = 24
T = 0.15		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 24
T = 0.15
(out)(err)
cnf3.150.250.832710.cnf.wcnf O = 24
T = 0.17		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 24
T = 0.17
(out)(err)
cnf3.150.250.832711.cnf.wcnf O = 20
T = 0.22		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 20
T = 0.22
(out)(err)
cnf3.150.250.832712.cnf.wcnf O = 23
T = 0.01		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 23
T = 0.01
(out)(err)
cnf3.150.250.832713.cnf.wcnf O = 16
T = 0.00		 O = 16
T = 199.87
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 16
T = 0.00
(out)(err)
cnf3.150.250.832714.cnf.wcnf O = 23
T = 0.04		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 23
T = 0.04
(out)(err)
cnf3.150.250.832715.cnf.wcnf O = 24
T = 3.16		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 24
T = 3.16
(out)(err)
cnf3.150.300.195561.cnf.wcnf O = 22
T = 1.35		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 22
T = 1.35
(out)(err)
cnf3.150.300.195562.cnf.wcnf O = 22
T = 1.83		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 22
T = 1.83
(out)(err)
cnf3.150.300.195563.cnf.wcnf O = 20
T = 0.05		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 20
T = 0.05
(out)(err)
cnf3.150.300.195564.cnf.wcnf O = 26
T = 1.11		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 26
T = 1.11
(out)(err)
cnf3.150.300.195565.cnf.wcnf O = 27
T = 2.14		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 27
T = 2.14
(out)(err)
cnf3.150.300.195566.cnf.wcnf O = 21
T = 0.10		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 21
T = 0.10
(out)(err)
cnf3.150.300.195567.cnf.wcnf O = 26
T = 0.97		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 26
T = 0.97
(out)(err)
cnf3.150.300.195568.cnf.wcnf O = 25
T = 2.97		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 25
T = 2.97
(out)(err)
cnf3.150.300.195569.cnf.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 27
T = 1.01
(out)(err)
cnf3.150.300.195570.cnf.wcnf O = 20
T = 0.01		 O = N/A
T = TO
(out)(err)		 O = 20
T = 194.36
(out)(err)		 O = 20
T = 0.01
(out)(err)
cnf3.150.350.558416.cnf.wcnf O = 32
T = 85.34		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 32
T = 85.34
(out)(err)
cnf3.150.350.558417.cnf.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 30
T = 53.59
(out)(err)
cnf3.150.350.558418.cnf.wcnf O = 29
T = 42.38		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 29
T = 42.38
(out)(err)
cnf3.150.350.558419.cnf.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 29
T = 1.20
(out)(err)
cnf3.150.350.558420.cnf.wcnf O = 32
T = 9.33		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 32
T = 9.33
(out)(err)
cnf3.150.350.558421.cnf.wcnf O = 30
T = 134.15		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 30
T = 134.15
(out)(err)
cnf3.150.350.558422.cnf.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 30
T = 3.73
(out)(err)
cnf3.150.350.558423.cnf.wcnf O = 26
T = 35.04		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 26
T = 35.04
(out)(err)
cnf3.150.350.558424.cnf.wcnf O = 24
T = 1.40		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 24
T = 1.40
(out)(err)
cnf3.150.350.558425.cnf.wcnf O = 27
T = 11.04		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 27
T = 11.04
(out)(err)
cnf3.150.400.921271.cnf.wcnf O = 57
T = 0.14		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 57
T = 0.14
(out)(err)
cnf3.150.400.921272.cnf.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 33
T = 79.49
(out)(err)
cnf3.150.400.921273.cnf.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 31
T = 51.88
(out)(err)
cnf3.150.400.921274.cnf.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 34
T = 25.65
(out)(err)
cnf3.150.400.921275.cnf.wcnf O = 39
T = 231.73		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 39
T = 231.73
(out)(err)
cnf3.150.400.921276.cnf.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 35
T = 10.61
(out)(err)
cnf3.150.400.921277.cnf.wcnf O = 33
T = 263.49		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 33
T = 263.49
(out)(err)
cnf3.150.400.921278.cnf.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 31
T = 12.36
(out)(err)
cnf3.150.400.921279.cnf.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 30
T = 0.74
(out)(err)
cnf3.150.400.921280.cnf.wcnf O = 30
T = 297.44		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 30
T = 297.44
(out)(err)
cnf3.150.450.284126.cnf.wcnf O = 67
T = 0.10		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 67
T = 0.10
(out)(err)
cnf3.150.450.284127.cnf.wcnf O = 50
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 50
T = 0.09
(out)(err)
cnf3.150.450.284128.cnf.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 35
T = 232.78
(out)(err)
cnf3.150.450.284129.cnf.wcnf O = 33
T = 116.62		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 33
T = 116.62
(out)(err)
cnf3.150.450.284130.cnf.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 38
T = 20.43
(out)(err)
cnf3.150.450.284131.cnf.wcnf O = 31
T = 155.91		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 31
T = 155.91
(out)(err)
cnf3.150.450.284132.cnf.wcnf O = 32
T = 254.57		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 32
T = 254.57
(out)(err)
cnf3.150.450.284133.cnf.wcnf O = 42
T = 295.54		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 42
T = 295.54
(out)(err)
cnf3.150.450.284134.cnf.wcnf O = 41
T = 36.48		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 41
T = 36.48
(out)(err)
cnf3.150.450.284135.cnf.wcnf O = 50
T = 0.14		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 50
T = 0.14
(out)(err)
cnf3.150.500.646981.cnf.wcnf O = 47
T = 19.01		 O = 47
T = 24.73
(out)(err)		 O = 47
T = 19.01
(out)(err)		 O = 47
T = 140.67
(out)(err)
cnf3.150.500.646982.cnf.wcnf O = 46
T = 21.17		 O = 46
T = 26.86
(out)(err)		 O = 46
T = 21.17
(out)(err)		 O = 46
T = 228.65
(out)(err)
cnf3.150.500.646983.cnf.wcnf O = 47
T = 243.83		 O = 47
T = 243.83
(out)(err)		 O = 47
T = 255.86
(out)(err)		 O = 72
T = 0.15
(out)(err)
cnf3.150.500.646984.cnf.wcnf O = 42
T = 18.29		 O = 42
T = 33.27
(out)(err)		 O = 42
T = 18.29
(out)(err)		 O = 42
T = 298.89
(out)(err)
cnf3.150.500.646985.cnf.wcnf O = 53
T = 7.14		 O = 53
T = 9.43
(out)(err)		 O = 53
T = 7.14
(out)(err)		 O = 53
T = 137.92
(out)(err)
cnf3.150.500.646986.cnf.wcnf O = 47
T = 5.16		 O = 47
T = 5.16
(out)(err)		 O = 47
T = 18.71
(out)(err)		 O = 73
T = 0.09
(out)(err)
cnf3.150.500.646987.cnf.wcnf O = 43
T = 5.81		 O = 43
T = 5.81
(out)(err)		 O = 43
T = 5.85
(out)(err)		 O = 45
T = 22.33
(out)(err)
cnf3.150.500.646988.cnf.wcnf O = 41
T = 10.05		 O = 41
T = 14.23
(out)(err)		 O = 41
T = 10.05
(out)(err)		 O = 41
T = 61.73
(out)(err)
cnf3.150.500.646989.cnf.wcnf O = 49
T = 6.20		 O = 49
T = 21.61
(out)(err)		 O = 49
T = 6.20
(out)(err)		 O = 52
T = 93.61
(out)(err)
cnf3.150.500.646990.cnf.wcnf O = 44
T = 6.66		 O = 44
T = 6.66
(out)(err)		 O = 44
T = 22.64
(out)(err)		 O = 44
T = 119.76
(out)(err)
cnf3.150.550.009836.cnf.wcnf O = 54
T = 1.78		 O = 54
T = 1.78
(out)(err)		 O = 54
T = 2.25
(out)(err)		 O = 66
T = 0.09
(out)(err)
cnf3.150.550.009837.cnf.wcnf O = 52
T = 4.97		 O = 52
T = 4.97
(out)(err)		 O = 52
T = 5.65
(out)(err)		 O = 52
T = 12.79
(out)(err)
cnf3.150.550.009838.cnf.wcnf O = 45
T = 5.58		 O = 45
T = 6.59
(out)(err)		 O = 45
T = 5.58
(out)(err)		 O = 45
T = 7.43
(out)(err)
cnf3.150.550.009839.cnf.wcnf O = 39
T = 4.65		 O = 39
T = 4.65
(out)(err)		 O = 39
T = 20.48
(out)(err)		 O = 39
T = 26.25
(out)(err)
cnf3.150.550.009840.cnf.wcnf O = 52
T = 4.75		 O = 52
T = 5.14
(out)(err)		 O = 52
T = 4.75
(out)(err)		 O = 55
T = 3.43
(out)(err)
cnf3.150.550.009841.cnf.wcnf O = 57
T = 4.73		 O = 57
T = 4.73
(out)(err)		 O = 57
T = 6.28
(out)(err)		 O = 57
T = 21.25
(out)(err)
cnf3.150.550.009842.cnf.wcnf O = 45
T = 5.04		 O = 45
T = 5.35
(out)(err)		 O = 45
T = 5.04
(out)(err)		 O = 45
T = 1.60
(out)(err)
cnf3.150.550.009843.cnf.wcnf O = 40
T = 4.72		 O = 40
T = 5.54
(out)(err)		 O = 40
T = 4.72
(out)(err)		 O = 40
T = 6.28
(out)(err)
cnf3.150.550.009844.cnf.wcnf O = 47
T = 7.01		 O = 47
T = 7.01
(out)(err)		 O = 47
T = 8.91
(out)(err)		 O = 47
T = 45.43
(out)(err)
cnf3.150.550.009845.cnf.wcnf O = 50
T = 4.45		 O = 50
T = 4.45
(out)(err)		 O = 50
T = 4.93
(out)(err)		 O = 50
T = 13.65
(out)(err)
cnf3.150.600.372691.cnf.wcnf O = 63
T = 0.37		 O = 63
T = 1.75
(out)(err)		 O = 63
T = 1.86
(out)(err)		 O = 63
T = 0.37
(out)(err)
cnf3.150.600.372692.cnf.wcnf O = 49
T = 1.71		 O = 49
T = 2.65
(out)(err)		 O = 49
T = 2.57
(out)(err)		 O = 49
T = 1.71
(out)(err)
cnf3.150.600.372693.cnf.wcnf O = 69
T = 0.14		 O = 69
T = 1.33
(out)(err)		 O = 69
T = 1.27
(out)(err)		 O = 69
T = 0.14
(out)(err)
cnf3.150.600.372694.cnf.wcnf O = 62
T = 0.25		 O = 62
T = 1.34
(out)(err)		 O = 62
T = 1.79
(out)(err)		 O = 62
T = 0.25
(out)(err)
cnf3.150.600.372695.cnf.wcnf O = 53
T = 0.46		 O = 53
T = 1.97
(out)(err)		 O = 53
T = 1.90
(out)(err)		 O = 53
T = 0.46
(out)(err)
cnf3.150.600.372696.cnf.wcnf O = 53
T = 0.74		 O = 53
T = 1.51
(out)(err)		 O = 53
T = 2.04
(out)(err)		 O = 53
T = 0.74
(out)(err)
cnf3.150.600.372697.cnf.wcnf O = 46
T = 3.96		 O = 46
T = 3.96
(out)(err)		 O = 46
T = 4.26
(out)(err)		 O = 46
T = 4.00
(out)(err)
cnf3.150.600.372698.cnf.wcnf O = 57
T = 0.79		 O = 57
T = 3.03
(out)(err)		 O = 57
T = 2.86
(out)(err)		 O = 57
T = 0.79
(out)(err)
cnf3.150.600.372699.cnf.wcnf O = 65
T = 0.28		 O = 65
T = 1.41
(out)(err)		 O = 65
T = 1.54
(out)(err)		 O = 65
T = 0.28
(out)(err)
cnf3.150.600.372700.cnf.wcnf O = 60
T = 1.37		 O = 60
T = 2.39
(out)(err)		 O = 60
T = 2.27
(out)(err)		 O = 60
T = 1.37
(out)(err)
3col100_5_1.shuffled.cnf.wcnf O = 100
T = 0.47		 O = 100
T = 1.79
(out)(err)		 O = 100
T = 1.70
(out)(err)		 O = 100
T = 0.47
(out)(err)
3col100_5_10.shuffled.cnf.wcnf O = 94
T = 0.46		 O = 94
T = 1.63
(out)(err)		 O = 94
T = 0.94
(out)(err)		 O = 94
T = 0.46
(out)(err)
3col100_5_2.shuffled.cnf.wcnf O = 104
T = 0.46		 O = 104
T = 1.67
(out)(err)		 O = 104
T = 1.31
(out)(err)		 O = 104
T = 0.46
(out)(err)
3col100_5_3.shuffled.cnf.wcnf O = 92
T = 0.32		 O = 92
T = 2.02
(out)(err)		 O = 92
T = 1.58
(out)(err)		 O = 92
T = 0.32
(out)(err)
3col100_5_4.shuffled.cnf.wcnf O = 97
T = 0.38		 O = 97
T = 1.62
(out)(err)		 O = 97
T = 1.44
(out)(err)		 O = 97
T = 0.38
(out)(err)
3col100_5_5.shuffled.cnf.wcnf O = 86
T = 0.18		 O = 86
T = 1.65
(out)(err)		 O = 86
T = 1.40
(out)(err)		 O = 86
T = 0.18
(out)(err)
3col100_5_6.shuffled.cnf.wcnf O = 90
T = 0.42		 O = 90
T = 1.48
(out)(err)		 O = 90
T = 1.48
(out)(err)		 O = 90
T = 0.42
(out)(err)
3col100_5_7.shuffled.cnf.wcnf O = 85
T = 0.50		 O = 85
T = 1.53
(out)(err)		 O = 85
T = 1.43
(out)(err)		 O = 85
T = 0.50
(out)(err)
3col100_5_8.shuffled.cnf.wcnf O = 94
T = 0.52		 O = 94
T = 1.55
(out)(err)		 O = 94
T = 1.33
(out)(err)		 O = 94
T = 0.52
(out)(err)
3col100_5_9.shuffled.cnf.wcnf O = 94
T = 0.34		 O = 94
T = 1.53
(out)(err)		 O = 94
T = 1.56
(out)(err)		 O = 94
T = 0.34
(out)(err)
3col120_5_1.shuffled.cnf.wcnf O = 123
T = 2.22		 O = 123
T = 3.26
(out)(err)		 O = 123
T = 2.70
(out)(err)		 O = 123
T = 2.22
(out)(err)
3col120_5_10.shuffled.cnf.wcnf O = 125
T = 3.14		 O = 125
T = 4.23
(out)(err)		 O = 125
T = 4.11
(out)(err)		 O = 125
T = 3.14
(out)(err)
3col120_5_2.shuffled.cnf.wcnf O = 124
T = 3.48		 O = 124
T = 3.48
(out)(err)		 O = 124
T = 3.64
(out)(err)		 O = 124
T = 4.57
(out)(err)
3col120_5_3.shuffled.cnf.wcnf O = 119
T = 2.97		 O = 119
T = 2.97
(out)(err)		 O = 119
T = 3.23
(out)(err)		 O = 119
T = 4.97
(out)(err)
3col120_5_4.shuffled.cnf.wcnf O = 122
T = 4.06		 O = 122
T = 4.06
(out)(err)		 O = 122
T = 4.30
(out)(err)		 O = 122
T = 4.91
(out)(err)
3col120_5_5.shuffled.cnf.wcnf O = 112
T = 2.03		 O = 112
T = 2.69
(out)(err)		 O = 112
T = 3.17
(out)(err)		 O = 112
T = 2.03
(out)(err)
3col120_5_6.shuffled.cnf.wcnf O = 121
T = 2.87		 O = 121
T = 2.87
(out)(err)		 O = 121
T = 3.44
(out)(err)		 O = 121
T = 3.10
(out)(err)
3col120_5_7.shuffled.cnf.wcnf O = 120
T = 3.19		 O = 120
T = 4.52
(out)(err)		 O = 120
T = 4.29
(out)(err)		 O = 120
T = 3.19
(out)(err)
3col120_5_8.shuffled.cnf.wcnf O = 110
T = 4.06		 O = 110
T = 4.25
(out)(err)		 O = 110
T = 4.06
(out)(err)		 O = 110
T = 4.47
(out)(err)
3col120_5_9.shuffled.cnf.wcnf O = 117
T = 3.04		 O = 117
T = 3.04
(out)(err)		 O = 117
T = 3.12
(out)(err)		 O = 117
T = 3.94
(out)(err)
3col140_5_1.shuffled.cnf.wcnf O = 121
T = 4.60		 O = 121
T = 5.40
(out)(err)		 O = 121
T = 4.60
(out)(err)		 O = 121
T = 28.12
(out)(err)
3col140_5_10.shuffled.cnf.wcnf O = 122
T = 2.75		 O = 122
T = 2.75
(out)(err)		 O = 122
T = 4.73
(out)(err)		 O = 122
T = 10.79
(out)(err)
3col140_5_2.shuffled.cnf.wcnf O = 131
T = 4.52		 O = 131
T = 4.84
(out)(err)		 O = 131
T = 4.52
(out)(err)		 O = 146
T = 0.24
(out)(err)
3col140_5_3.shuffled.cnf.wcnf O = 128
T = 4.93		 O = 128
T = 5.81
(out)(err)		 O = 128
T = 4.93
(out)(err)		 O = 128
T = 19.66
(out)(err)
3col140_5_4.shuffled.cnf.wcnf O = 128
T = 5.36		 O = 128
T = 5.36
(out)(err)		 O = 128
T = 5.45
(out)(err)		 O = 128
T = 9.73
(out)(err)
3col140_5_5.shuffled.cnf.wcnf O = 124
T = 5.61		 O = 124
T = 5.97
(out)(err)		 O = 124
T = 5.61
(out)(err)		 O = 124
T = 10.91
(out)(err)
3col140_5_6.shuffled.cnf.wcnf O = 120
T = 5.21		 O = 120
T = 5.41
(out)(err)		 O = 120
T = 5.21
(out)(err)		 O = 129
T = 0.11
(out)(err)
3col140_5_7.shuffled.cnf.wcnf O = 119
T = 4.83		 O = 119
T = 4.83
(out)(err)		 O = 119
T = 5.23
(out)(err)		 O = 119
T = 8.56
(out)(err)
3col140_5_8.shuffled.cnf.wcnf O = 123
T = 4.57		 O = 123
T = 4.57
(out)(err)		 O = 123
T = 5.98
(out)(err)		 O = 127
T = 0.12
(out)(err)
3col140_5_9.shuffled.cnf.wcnf O = 134
T = 4.36		 O = 134
T = 4.36
(out)(err)		 O = 134
T = 4.54
(out)(err)		 O = 134
T = 9.94
(out)(err)
3col80_5_1.shuffled.cnf.wcnf O = 79
T = 0.23		 O = 79
T = 0.90
(out)(err)		 O = 79
T = 0.93
(out)(err)		 O = 79
T = 0.23
(out)(err)
3col80_5_10.shuffled.cnf.wcnf O = 75
T = 0.07		 O = 75
T = 0.92
(out)(err)		 O = 75
T = 1.06
(out)(err)		 O = 75
T = 0.07
(out)(err)
3col80_5_2.shuffled.cnf.wcnf O = 71
T = 0.10		 O = 71
T = 0.91
(out)(err)		 O = 71
T = 0.89
(out)(err)		 O = 71
T = 0.10
(out)(err)
3col80_5_3.shuffled.cnf.wcnf O = 88
T = 0.08		 O = 88
T = 0.73
(out)(err)		 O = 88
T = 0.92
(out)(err)		 O = 88
T = 0.08
(out)(err)
3col80_5_4.shuffled.cnf.wcnf O = 73
T = 0.12		 O = 73
T = 0.68
(out)(err)		 O = 73
T = 0.84
(out)(err)		 O = 73
T = 0.12
(out)(err)
3col80_5_5.shuffled.cnf.wcnf O = 78
T = 0.12		 O = 78
T = 0.97
(out)(err)		 O = 78
T = 0.93
(out)(err)		 O = 78
T = 0.12
(out)(err)
3col80_5_6.shuffled.cnf.wcnf O = 76
T = 0.10		 O = 76
T = 0.96
(out)(err)		 O = 76
T = 0.96
(out)(err)		 O = 76
T = 0.10
(out)(err)
3col80_5_7.shuffled.cnf.wcnf O = 80
T = 0.06		 O = 80
T = 0.94
(out)(err)		 O = 80
T = 0.78
(out)(err)		 O = 80
T = 0.06
(out)(err)
3col80_5_8.shuffled.cnf.wcnf O = 82
T = 0.09		 O = 82
T = 0.87
(out)(err)		 O = 82
T = 0.88
(out)(err)		 O = 82
T = 0.09
(out)(err)
3col80_5_9.shuffled.cnf.wcnf O = 79
T = 0.07		 O = 79
T = 0.92
(out)(err)		 O = 79
T = 0.94
(out)(err)		 O = 79
T = 0.07
(out)(err)
cnt05.shuffled.cnf.wcnf O = 174
T = 0.24		 O = 174
T = 0.67
(out)(err)		 O = 174
T = 0.73
(out)(err)		 O = 174
T = 0.24
(out)(err)
cnt06.shuffled.cnf.wcnf O = 365
T = 1.17		 O = 365
T = 1.29
(out)(err)		 O = 365
T = 1.21
(out)(err)		 O = 365
T = 1.17
(out)(err)
cnt07.shuffled.cnf.wcnf O = 877
T = 1.94		 O = 877
T = 2.20
(out)(err)		 O = 877
T = 1.94
(out)(err)		 O = 877
T = 13.45
(out)(err)
dp02s02.shuffled.cnf.wcnf O = 100
T = 0.03		 O = 100
T = 0.44
(out)(err)		 O = 100
T = 0.45
(out)(err)		 O = 100
T = 0.03
(out)(err)
dp03s03.shuffled.cnf.wcnf O = 254
T = 0.53		 O = 254
T = 0.99
(out)(err)		 O = 254
T = 0.68
(out)(err)		 O = 254
T = 0.53
(out)(err)
dp04s04.shuffled.cnf.wcnf O = 533
T = 1.81		 O = 533
T = 2.01
(out)(err)		 O = 533
T = 1.81
(out)(err)		 O = 533
T = 2.75
(out)(err)
dp05s05.shuffled.cnf.wcnf O = 765
T = 2.09		 O = 765
T = 2.43
(out)(err)		 O = 765
T = 2.09
(out)(err)		 O = 765
T = 11.26
(out)(err)
dp06s06.shuffled.cnf.wcnf O = 1164
T = 4.57		 O = 1164
T = 4.57
(out)(err)		 O = 1164
T = 4.90
(out)(err)		 O = 1195
T = 0.74
(out)(err)
dp07s07.shuffled.cnf.wcnf O = 1563
T = 6.28		 O = 1563
T = 21.98
(out)(err)		 O = 1563
T = 6.28
(out)(err)		 O = 1599
T = 1.37
(out)(err)
ezfact32_1.shuffled.cnf.wcnf O = 400
T = 0.58		 O = 400
T = 2.04
(out)(err)		 O = 400
T = 2.03
(out)(err)		 O = 400
T = 0.58
(out)(err)
ezfact32_10.shuffled.cnf.wcnf O = 389
T = 1.47		 O = 389
T = 4.46
(out)(err)		 O = 389
T = 4.64
(out)(err)		 O = 389
T = 1.47
(out)(err)
ezfact32_2.shuffled.cnf.wcnf O = 364
T = 0.23		 O = 364
T = 1.17
(out)(err)		 O = 364
T = 1.11
(out)(err)		 O = 364
T = 0.23
(out)(err)
ezfact32_3.shuffled.cnf.wcnf O = 397
T = 1.29		 O = 397
T = 7.75
(out)(err)		 O = 397
T = 7.76
(out)(err)		 O = 397
T = 1.29
(out)(err)
ezfact32_4.shuffled.cnf.wcnf O = 379
T = 2.05		 O = 379
T = 2.05
(out)(err)		 O = 379
T = 2.05
(out)(err)		 O = 379
T = 2.19
(out)(err)
ezfact32_5.shuffled.cnf.wcnf O = 394
T = 1.39		 O = 394
T = 1.43
(out)(err)		 O = 394
T = 1.39
(out)(err)		 O = 394
T = 1.40
(out)(err)
ezfact32_6.shuffled.cnf.wcnf O = 382
T = 1.40		 O = 382
T = 1.42
(out)(err)		 O = 382
T = 1.40
(out)(err)		 O = 382
T = 2.21
(out)(err)
ezfact32_7.shuffled.cnf.wcnf O = 394
T = 1.19		 O = 394
T = 1.22
(out)(err)		 O = 394
T = 1.19
(out)(err)		 O = 394
T = 1.86
(out)(err)
ezfact32_8.shuffled.cnf.wcnf O = 392
T = 1.30		 O = 392
T = 1.31
(out)(err)		 O = 392
T = 1.30
(out)(err)		 O = 392
T = 1.45
(out)(err)
ezfact32_9.shuffled.cnf.wcnf O = 382
T = 0.66		 O = 382
T = 1.12
(out)(err)		 O = 382
T = 1.16
(out)(err)		 O = 382
T = 0.66
(out)(err)
med11.shuffled.cnf.wcnf O = 164
T = 5.94		 O = 164
T = 8.48
(out)(err)		 O = 164
T = 5.94
(out)(err)		 O = 166
T = 0.15
(out)(err)
kbtree9_7_3_5_30_1.wcsp.wcnf O = 10
T = 213.31		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 10
T = 213.31
(out)(err)
kbtree9_7_3_5_30_2.wcsp.wcnf O = 7
T = 137.87		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 7
T = 137.87
(out)(err)
kbtree9_7_3_5_30_3.wcsp.wcnf O = 12
T = 0.14		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 12
T = 0.14
(out)(err)
kbtree9_7_3_5_30_4.wcsp.wcnf O = 6
T = 11.04		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 6
T = 11.04
(out)(err)
kbtree9_7_3_5_30_5.wcsp.wcnf O = 6
T = 44.32		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 6
T = 44.32
(out)(err)
kbtree9_7_3_5_30_6.wcsp.wcnf O = 9
T = 280.79		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 9
T = 280.79
(out)(err)
kbtree9_7_3_5_40_1.wcsp.wcnf O = 48
T = 0.11		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 48
T = 0.11
(out)(err)
kbtree9_7_3_5_40_2.wcsp.wcnf O = 46
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 46
T = 0.13
(out)(err)
kbtree9_7_3_5_40_3.wcsp.wcnf O = 41
T = 0.10		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 41
T = 0.10
(out)(err)
kbtree9_7_3_5_40_4.wcsp.wcnf O = 42
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 42
T = 0.09
(out)(err)
kbtree9_7_3_5_40_5.wcsp.wcnf O = 28
T = 295.98		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 28
T = 295.98
(out)(err)
kbtree9_7_3_5_40_6.wcsp.wcnf O = 57
T = 0.10		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 57
T = 0.10
(out)(err)
kbtree9_7_3_5_50_1.wcsp.wcnf O = 69
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 69
T = 0.09
(out)(err)
kbtree9_7_3_5_50_2.wcsp.wcnf O = 65
T = 0.12		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 65
T = 0.12
(out)(err)
kbtree9_7_3_5_50_3.wcsp.wcnf O = 64
T = 0.14		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 64
T = 0.14
(out)(err)
kbtree9_7_3_5_50_4.wcsp.wcnf O = 57
T = 0.14		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 57
T = 0.14
(out)(err)
kbtree9_7_3_5_50_5.wcsp.wcnf O = 60
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 60
T = 0.13
(out)(err)
kbtree9_7_3_5_50_6.wcsp.wcnf O = 62
T = 0.11		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 62
T = 0.11
(out)(err)
kbtree9_7_3_5_60_1.wcsp.wcnf O = 91
T = 0.12		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 91
T = 0.12
(out)(err)
kbtree9_7_3_5_60_2.wcsp.wcnf O = 89
T = 0.08		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 89
T = 0.08
(out)(err)
kbtree9_7_3_5_60_3.wcsp.wcnf O = 85
T = 0.12		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 85
T = 0.12
(out)(err)
kbtree9_7_3_5_60_4.wcsp.wcnf O = 92
T = 0.12		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 92
T = 0.12
(out)(err)
kbtree9_7_3_5_60_5.wcsp.wcnf O = 97
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 97
T = 0.13
(out)(err)
kbtree9_7_3_5_60_6.wcsp.wcnf O = 88
T = 0.10		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 88
T = 0.10
(out)(err)
kbtree9_7_3_5_70_1.wcsp.wcnf O = 107
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 107
T = 0.09
(out)(err)
kbtree9_7_3_5_70_2.wcsp.wcnf O = 112
T = 0.12		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 112
T = 0.12
(out)(err)
kbtree9_7_3_5_70_3.wcsp.wcnf O = 105
T = 0.08		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 105
T = 0.08
(out)(err)
kbtree9_7_3_5_70_4.wcsp.wcnf O = 113
T = 0.08		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 113
T = 0.08
(out)(err)
kbtree9_7_3_5_70_5.wcsp.wcnf O = 111
T = 0.14		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 111
T = 0.14
(out)(err)
kbtree9_7_3_5_70_6.wcsp.wcnf O = 106
T = 0.14		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 106
T = 0.14
(out)(err)
kbtree9_7_3_5_80_1.wcsp.wcnf O = 137
T = 0.14		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 137
T = 0.14
(out)(err)
kbtree9_7_3_5_80_2.wcsp.wcnf O = 133
T = 0.14		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 133
T = 0.14
(out)(err)
kbtree9_7_3_5_80_3.wcsp.wcnf O = 113
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 113
T = 0.13
(out)(err)
kbtree9_7_3_5_80_4.wcsp.wcnf O = 136
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 136
T = 0.13
(out)(err)
kbtree9_7_3_5_80_5.wcsp.wcnf O = 129
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 129
T = 0.13
(out)(err)
kbtree9_7_3_5_80_6.wcsp.wcnf O = 136
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 136
T = 0.09
(out)(err)
kbtree9_7_3_5_90_1.wcsp.wcnf O = 142
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 142
T = 0.13
(out)(err)
kbtree9_7_3_5_90_2.wcsp.wcnf O = 145
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 145
T = 0.13
(out)(err)
kbtree9_7_3_5_90_3.wcsp.wcnf O = 143
T = 0.10		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 143
T = 0.10
(out)(err)
kbtree9_7_3_5_90_4.wcsp.wcnf O = 148
T = 0.14		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 148
T = 0.14
(out)(err)
kbtree9_7_3_5_90_5.wcsp.wcnf O = 150
T = 0.09		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 150
T = 0.09
(out)(err)
kbtree9_7_3_5_90_6.wcsp.wcnf O = 152
T = 0.13		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 152
T = 0.13
(out)(err)
normalized-mps-v2-20-10-stein15.opb.msat.wcnf O = 9
T = 0.00		 O = 9
T = 0.53
(out)(err)		 O = 9
T = 0.45
(out)(err)		 O = 9
T = 0.00
(out)(err)
normalized-mps-v2-20-10-stein27.opb.msat.wcnf O = 18
T = 0.28		 O = 18
T = 3.24
(out)(err)		 O = 18
T = 3.18
(out)(err)		 O = 18
T = 0.28
(out)(err)
normalized-mps-v2-20-10-stein45.opb.msat.wcnf O = 30
T = 29.21		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 30
T = 29.21
(out)(err)
normalized-mps-v2-20-10-stein9.opb.msat.wcnf O = 5
T = 0.00		 O = 5
T = 0.31
(out)(err)		 O = 5
T = 0.24
(out)(err)		 O = 5
T = 0.00
(out)(err)
cnf_10.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)
cnf_10_center.wcnf O = 164
T = 4.87		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 164
T = 4.87
(out)(err)
cnf_12.wcnf O = N/A
T = TO		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)
cnf_12_center.wcnf O = 242
T = 8.96		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 242
T = 8.96
(out)(err)
cnf_small.wcnf O = 29
T = 93.41		 O = N/A
T = TO
(out)(err)		 O = N/A
T = TO
(out)(err)		 O = 29
T = 93.41
(out)(err)