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 Sat4j-i ubcsat-irots
mul_8_11.wcnf O = 188
T = 6.98
O = 188
T = 6.98
(out)(err)
O = 451
T = 17.95
(out)(err)
mul_8_13.wcnf O = 156
T = 7.11
O = 156
T = 7.11
(out)(err)
O = 436
T = 37.77
(out)(err)
mul_8_14.wcnf O = 104
T = 6.36
O = 104
T = 6.36
(out)(err)
O = 492
T = 63.15
(out)(err)
mul_8_3.wcnf O = 44
T = 3.57
O = 44
T = 3.57
(out)(err)
O = 102
T = 9.13
(out)(err)
mul_8_9.wcnf O = 82
T = 4.38
O = 82
T = 4.38
(out)(err)
O = 163
T = 76.63
(out)(err)
sbox_4.wcnf O = 22
T = 10.71
O = 30
T = 0.76
(out)(err)
O = 22
T = 10.71
(out)(err)
sbox_8.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
normalized-f20c10b_001_area_delay.wcnf O = 40
T = 3.22
O = 40
T = 3.22
(out)(err)
O = 115
T = 5.11
(out)(err)
normalized-f20c10b_002_area_delay.wcnf O = 36
T = 3.98
O = 36
T = 3.98
(out)(err)
O = 104
T = 14.32
(out)(err)
normalized-f20c10b_003_area_delay.wcnf O = 40
T = 3.82
O = 40
T = 3.82
(out)(err)
O = 99
T = 9.80
(out)(err)
normalized-f20c10b_004_area_delay.wcnf O = 39
T = 3.46
O = 39
T = 3.46
(out)(err)
O = 109
T = 4.50
(out)(err)
normalized-f20c10b_005_area_delay.wcnf O = 43
T = 3.61
O = 43
T = 3.61
(out)(err)
O = 215
T = 12.26
(out)(err)
normalized-f20c10b_006_area_delay.wcnf O = 30
T = 4.84
O = 30
T = 4.84
(out)(err)
O = 115
T = 42.74
(out)(err)
normalized-f20c10b_007_area_delay.wcnf O = 36
T = 4.24
O = 36
T = 4.24
(out)(err)
O = 100
T = 66.55
(out)(err)
normalized-f20c10b_008_area_delay.wcnf O = 39
T = 3.27
O = 39
T = 3.27
(out)(err)
O = 88
T = 83.42
(out)(err)
normalized-f20c10b_009_area_delay.wcnf O = 36
T = 1.84
O = 36
T = 1.84
(out)(err)
O = 98
T = 80.04
(out)(err)
normalized-f20c10b_010_area_delay.wcnf O = 40
T = 4.17
O = 40
T = 4.17
(out)(err)
O = 105
T = 59.79
(out)(err)
normalized-f20c10b_011_area_delay.wcnf O = 42
T = 3.75
O = 42
T = 3.75
(out)(err)
O = 127
T = 113.48
(out)(err)
normalized-f20c10b_012_area_delay.wcnf O = 46
T = 4.07
O = 46
T = 4.07
(out)(err)
O = 116
T = 84.50
(out)(err)
normalized-f20c10b_013_area_delay.wcnf O = 35
T = 4.24
O = 35
T = 4.24
(out)(err)
O = 282
T = 67.19
(out)(err)
normalized-f20c10b_014_area_delay.wcnf O = 42
T = 2.53
O = 42
T = 2.53
(out)(err)
O = 105
T = 15.70
(out)(err)
normalized-f20c10b_015_area_delay.wcnf O = 38
T = 4.11
O = 38
T = 4.11
(out)(err)
O = 123
T = 14.15
(out)(err)
normalized-f20c10b_016_area_delay.wcnf O = 36
T = 4.09
O = 36
T = 4.09
(out)(err)
O = 124
T = 19.35
(out)(err)
normalized-f20c10b_017_area_delay.wcnf O = 38
T = 2.79
O = 38
T = 2.79
(out)(err)
O = 112
T = 40.48
(out)(err)
normalized-f20c10b_018_area_delay.wcnf O = 34
T = 5.25
O = 34
T = 5.25
(out)(err)
O = 93
T = 213.52
(out)(err)
normalized-f20c10b_019_area_delay.wcnf O = 37
T = 4.73
O = 37
T = 4.73
(out)(err)
O = 86
T = 20.24
(out)(err)
normalized-f20c10b_020_area_delay.wcnf O = 33
T = 2.62
O = 33
T = 2.62
(out)(err)
O = 84
T = 69.09
(out)(err)
normalized-f20c10b_021_area_delay.wcnf O = 34
T = 2.93
O = 34
T = 2.93
(out)(err)
O = 115
T = 46.16
(out)(err)
normalized-f20c10b_022_area_delay.wcnf O = 40
T = 19.44
O = 40
T = 19.44
(out)(err)
O = 119
T = 53.61
(out)(err)
normalized-f20c10b_023_area_delay.wcnf O = 37
T = 3.69
O = 37
T = 3.69
(out)(err)
O = 325
T = 64.29
(out)(err)
normalized-f20c10b_024_area_delay.wcnf O = 32
T = 4.38
O = 32
T = 4.38
(out)(err)
O = 97
T = 63.11
(out)(err)
normalized-f20c10b_025_area_delay.wcnf O = 44
T = 4.43
O = 44
T = 4.43
(out)(err)
O = 241
T = 132.57
(out)(err)
normalized-f20c10b_026_area_delay.wcnf O = 38
T = 2.32
O = 38
T = 2.32
(out)(err)
O = 137
T = 75.52
(out)(err)
normalized-f20c10b_027_area_delay.wcnf O = 37
T = 6.09
O = 37
T = 6.09
(out)(err)
O = 120
T = 77.98
(out)(err)
normalized-f20c10b_028_area_delay.wcnf O = 33
T = 4.23
O = 33
T = 4.23
(out)(err)
O = 324
T = 110.74
(out)(err)
normalized-f20c10b_029_area_delay.wcnf O = 39
T = 5.08
O = 39
T = 5.08
(out)(err)
O = 299
T = 28.31
(out)(err)
normalized-f20c10b_030_area_delay.wcnf O = 35
T = 5.45
O = 35
T = 5.45
(out)(err)
O = 117
T = 80.61
(out)(err)
normalized-fir01_area_delay.wcnf O = 5
T = 0.83
O = 5
T = 0.83
(out)(err)
O = 5
T = 3.09
(out)(err)
normalized-fir01_area_opers.wcnf O = 10
T = 2.73
O = 10
T = 2.73
(out)(err)
O = 10
T = 4.64
(out)(err)
normalized-fir02_area_delay.wcnf O = 8
T = 5.04
O = 8
T = 5.04
(out)(err)
O = 10
T = 148.82
(out)(err)
normalized-fir02_area_opers.wcnf O = 24
T = 3.69
O = 24
T = 3.69
(out)(err)
O = 33
T = 52.20
(out)(err)
normalized-fir02_area_partials.wcnf O = 19
T = 0.37
O = 19
T = 0.37
(out)(err)
O = 19
T = 0.39
(out)(err)
normalized-fir03_area_delay.wcnf O = 13
T = 237.48
O = 13
T = 237.48
(out)(err)
O = 23
T = 52.27
(out)(err)
normalized-fir03_area_opers.wcnf O = 27
T = 2.95
O = 27
T = 2.95
(out)(err)
O = 166
T = 10.61
(out)(err)
normalized-fir03_area_partials.wcnf O = 18
T = 2.12
O = 18
T = 2.12
(out)(err)
O = 27
T = 43.66
(out)(err)
normalized-fir04_area_delay.wcnf O = 15
T = 10.34
O = 15
T = 10.34
(out)(err)
O = 15
T = 49.29
(out)(err)
normalized-fir04_area_opers.wcnf O = 37
T = 2.31
O = 37
T = 2.31
(out)(err)
O = 49
T = 266.14
(out)(err)
normalized-fir04_area_partials.wcnf O = 30
T = 0.35
O = 30
T = 0.35
(out)(err)
O = 30
T = 1.39
(out)(err)
normalized-fir05_area_delay.wcnf O = 17
T = 5.63
O = 17
T = 5.63
(out)(err)
O = 33
T = 261.11
(out)(err)
normalized-fir05_area_opers.wcnf O = 44
T = 2.34
O = 44
T = 2.34
(out)(err)
O = 110
T = 36.36
(out)(err)
normalized-fir05_area_partials.wcnf O = 36
T = 0.81
O = 36
T = 0.81
(out)(err)
O = 43
T = 20.46
(out)(err)
normalized-fir06_area_delay.wcnf O = 19
T = 4.45
O = 19
T = 4.45
(out)(err)
O = 34
T = 59.98
(out)(err)
normalized-fir06_area_opers.wcnf O = 37
T = 192.87
O = 37
T = 192.87
(out)(err)
O = 220
T = 5.59
(out)(err)
normalized-fir06_area_partials.wcnf O = 24
T = 1.42
O = 24
T = 1.42
(out)(err)
O = 27
T = 26.90
(out)(err)
normalized-fir07_area_delay.wcnf O = 27
T = 4.35
O = 27
T = 4.35
(out)(err)
O = 45
T = 35.07
(out)(err)
normalized-fir07_area_opers.wcnf O = 51
T = 5.19
O = 51
T = 5.19
(out)(err)
O = 444
T = 80.75
(out)(err)
normalized-fir07_area_partials.wcnf O = 33
T = 0.78
O = 33
T = 0.78
(out)(err)
O = 33
T = 6.78
(out)(err)
normalized-fir08_area_delay.wcnf O = N/A
T = TO
O = 43
T = 15.88
(out)(err)
O = 123309
T = 239.00
(out)(err)
normalized-fir08_area_opers.wcnf O = N/A
T = TO
O = 83
T = 34.77
(out)(err)
O = 158
T = 182.72
(out)(err)
normalized-fir08_area_partials.wcnf O = 52
T = 50.91
O = 52
T = 50.91
(out)(err)
O = 1014
T = 12.73
(out)(err)
normalized-fir09_area_delay.wcnf O = 24
T = 4.52
O = 24
T = 4.52
(out)(err)
O = 67
T = 14.90
(out)(err)
normalized-fir09_area_opers.wcnf O = 58
T = 146.55
O = 58
T = 146.55
(out)(err)
O = 362
T = 71.82
(out)(err)
normalized-fir09_area_partials.wcnf O = 35
T = 40.39
O = 35
T = 40.39
(out)(err)
O = 141
T = 46.61
(out)(err)
normalized-fir10_area_delay.wcnf O = 49
T = 6.77
O = 49
T = 6.77
(out)(err)
O = 161
T = 122.51
(out)(err)
normalized-fir10_area_opers.wcnf O = 87
T = 8.55
O = 87
T = 8.55
(out)(err)
O = 1020
T = 82.36
(out)(err)
normalized-fir10_area_partials.wcnf O = 53
T = 11.30
O = 53
T = 11.30
(out)(err)
O = 81
T = 23.78
(out)(err)
simp-ibd_50.01.wcnf O = 53
T = 6.10
O = 53
T = 6.10
(out)(err)
O = 62
T = 227.40
(out)(err)
simp-ibd_50.02.wcnf O = 56
T = 80.95
O = 56
T = 80.95
(out)(err)
O = 67
T = 93.20
(out)(err)
simp-ibd_50.03.wcnf O = 54
T = 5.61
O = 54
T = 5.61
(out)(err)
O = 65
T = 108.70
(out)(err)
simp-ibd_50.04.wcnf O = 55
T = 16.21
O = 55
T = 16.21
(out)(err)
O = 72
T = 263.51
(out)(err)
simp-ibd_50.05.wcnf O = 59
T = 9.43
O = 59
T = 9.43
(out)(err)
O = 77
T = 237.85
(out)(err)
simp-ibd_50.06.wcnf O = 55
T = 243.17
O = 55
T = 243.17
(out)(err)
O = 64
T = 142.97
(out)(err)
simp-ibd_50.07.wcnf O = 57
T = 40.65
O = 57
T = 40.65
(out)(err)
O = 67
T = 271.84
(out)(err)
simp-ibd_50.08.wcnf O = 58
T = 152.78
O = 58
T = 152.78
(out)(err)
O = 73
T = 127.87
(out)(err)
simp-ibd_50.09.wcnf O = 57
T = 40.28
O = 57
T = 40.28
(out)(err)
O = 64
T = 53.79
(out)(err)
simp-test_chr10_CEU_75.wcnf O = 16
T = 0.36
O = 16
T = 0.36
(out)(err)
O = 16
T = 3.11
(out)(err)
simp-test_chr10_HCB_75.wcnf O = 15
T = 1.09
O = 15
T = 1.09
(out)(err)
O = 15
T = 1.38
(out)(err)
simp-test_chr10_JPT_75.wcnf O = 17
T = 1.18
O = 17
T = 1.18
(out)(err)
O = 17
T = 8.05
(out)(err)
simp-test_chr10_YRI_75.wcnf O = 30
T = 3.26
O = 30
T = 3.26
(out)(err)
O = 36
T = 23.50
(out)(err)
simp-test_chr21_CEU_75.wcnf O = 14
T = 1.74
O = 14
T = 1.74
(out)(err)
O = 15
T = 24.89
(out)(err)
simp-test_chr21_HCB_75.wcnf O = 15
T = 1.15
O = 15
T = 1.15
(out)(err)
O = 15
T = 9.09
(out)(err)
simp-test_chr21_JPT_75.wcnf O = 18
T = 3.61
O = 18
T = 3.61
(out)(err)
O = 18
T = 63.28
(out)(err)
simp-test_chr21_YRI_75.wcnf O = 46
T = 47.89
O = 46
T = 47.89
(out)(err)
O = 60
T = 36.62
(out)(err)
SU1__simp-genos.haps.1.wcnf O = 73
T = 14.60
O = 73
T = 14.60
(out)(err)
O = 510
T = 258.28
(out)(err)
SU1__simp-genos.haps.10.wcnf O = 91
T = 187.73
O = 91
T = 187.73
(out)(err)
O = 342
T = 140.06
(out)(err)
SU1__simp-genos.haps.18.wcnf O = 75
T = 120.33
O = 75
T = 120.33
(out)(err)
O = 170
T = 271.61
(out)(err)
SU1__simp-genos.haps.19.wcnf O = 81
T = 69.77
O = 81
T = 69.77
(out)(err)
O = 863
T = 178.01
(out)(err)
SU1__simp-genos.haps.26.wcnf O = 88
T = 42.15
O = 88
T = 42.15
(out)(err)
O = 700
T = 251.16
(out)(err)
SU1__simp-genos.haps.27.wcnf O = 97
T = 231.87
O = 97
T = 231.87
(out)(err)
O = 344
T = 194.66
(out)(err)
SU1__simp-genos.haps.29.wcnf O = 72
T = 12.94
O = 72
T = 12.94
(out)(err)
O = 136
T = 283.82
(out)(err)
SU1__simp-genos.haps.30.wcnf O = 71
T = 53.93
O = 71
T = 53.93
(out)(err)
O = 320
T = 280.13
(out)(err)
SU1__simp-genos.haps.32.wcnf O = 77
T = 18.82
O = 77
T = 18.82
(out)(err)
O = 507
T = 257.44
(out)(err)
SU1__simp-genos.haps.34.wcnf O = 75
T = 63.32
O = 75
T = 63.32
(out)(err)
O = 143
T = 195.91
(out)(err)
SU1__simp-genos.haps.37.wcnf O = 77
T = 82.53
O = 77
T = 82.53
(out)(err)
O = 338
T = 271.16
(out)(err)
SU1__simp-genos.haps.38.wcnf O = 94
T = 135.93
O = 94
T = 135.93
(out)(err)
O = 162
T = 235.68
(out)(err)
SU1__simp-genos.haps.50.wcnf O = 61
T = 53.56
O = 61
T = 53.56
(out)(err)
O = 129
T = 223.05
(out)(err)
SU1__simp-genos.haps.54.wcnf O = 72
T = 116.92
O = 72
T = 116.92
(out)(err)
O = 338
T = 281.32
(out)(err)
SU1__simp-genos.haps.58.wcnf O = 88
T = 184.13
O = 88
T = 184.13
(out)(err)
O = 702
T = 266.75
(out)(err)
SU1__simp-genos.haps.62.wcnf O = 68
T = 84.62
O = 68
T = 84.62
(out)(err)
O = 341
T = 254.63
(out)(err)
SU1__simp-genos.haps.69.wcnf O = 79
T = 111.08
O = 79
T = 111.08
(out)(err)
O = 834
T = 192.50
(out)(err)
SU1__simp-genos.haps.7.wcnf O = 80
T = 142.16
O = 80
T = 142.16
(out)(err)
O = 151
T = 196.34
(out)(err)
SU1__simp-genos.haps.70.wcnf O = 58
T = 40.30
O = 58
T = 40.30
(out)(err)
O = 116
T = 189.96
(out)(err)
SU1__simp-genos.haps.8.wcnf O = 63
T = 10.61
O = 63
T = 10.61
(out)(err)
O = 661
T = 57.63
(out)(err)
SU1__simp-genos.haps.85.wcnf O = 65
T = 28.92
O = 65
T = 28.92
(out)(err)
O = 159
T = 261.18
(out)(err)
SU1__simp-genos.haps.86.wcnf O = 56
T = 17.36
O = 56
T = 17.36
(out)(err)
O = 336
T = 281.72
(out)(err)
SU3__simp-genos.haps.21.wcnf O = 115
T = 89.16
O = 115
T = 89.16
(out)(err)
O = 354
T = 273.56
(out)(err)
SU3__simp-genos.haps.23.wcnf O = 113
T = 173.01
O = 113
T = 173.01
(out)(err)
O = 1080
T = 44.65
(out)(err)
SU3__simp-genos.haps.27.wcnf O = 102
T = 123.74
O = 102
T = 123.74
(out)(err)
O = 720
T = 55.06
(out)(err)
SU3__simp-genos.haps.33.wcnf O = 118
T = 11.74
O = 118
T = 11.74
(out)(err)
O = 355
T = 166.27
(out)(err)
SU3__simp-genos.haps.38.wcnf O = 107
T = 198.52
O = 107
T = 198.52
(out)(err)
O = 531
T = 286.00
(out)(err)
SU3__simp-genos.haps.53.wcnf O = 113
T = 13.47
O = 113
T = 13.47
(out)(err)
O = 1078
T = 39.31
(out)(err)
SU3__simp-genos.haps.58.wcnf O = 102
T = 14.48
O = 102
T = 14.48
(out)(err)
O = 711
T = 219.06
(out)(err)
SU3__simp-genos.haps.60.wcnf O = 108
T = 95.36
O = 108
T = 95.36
(out)(err)
O = 536
T = 170.65
(out)(err)
SU3__simp-genos.haps.63.wcnf O = 96
T = 87.07
O = 96
T = 87.07
(out)(err)
O = 160
T = 172.86
(out)(err)
SU3__simp-genos.haps.64.wcnf O = 105
T = 44.18
O = 105
T = 44.18
(out)(err)
O = 355
T = 268.68
(out)(err)
SU3__simp-genos.haps.72.wcnf O = 103
T = 179.51
O = 103
T = 179.51
(out)(err)
O = 538
T = 17.81
(out)(err)
SU3__simp-genos.haps.74.wcnf O = 102
T = 184.79
O = 102
T = 184.79
(out)(err)
O = 697
T = 96.60
(out)(err)
SU3__simp-genos.haps.80.wcnf O = 109
T = 33.78
O = 109
T = 33.78
(out)(err)
O = 532
T = 258.29
(out)(err)
SU3__simp-genos.haps.86.wcnf O = 103
T = 130.17
O = 103
T = 130.17
(out)(err)
O = 1077
T = 229.92
(out)(err)
SU3__simp-genos.haps.88.wcnf O = 110
T = 281.72
O = 110
T = 281.72
(out)(err)
O = 711
T = 203.74
(out)(err)
SU3__simp-genos.haps.9.wcnf O = 112
T = 49.93
O = 112
T = 49.93
(out)(err)
O = 354
T = 207.25
(out)(err)
normalized-f1000.wcnf O = 14936
T = 218.07
O = N/A
T = TO
(out)(err)
O = 14936
T = 218.07
(out)(err)
normalized-f2000.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = 85965
T = 27.76
(out)(err)
normalized-f600.wcnf O = 2957
T = 80.41
O = N/A
T = TO
(out)(err)
O = 2957
T = 80.41
(out)(err)
normalized-g125.17.wcnf O = 99882
T = 17.60
O = N/A
T = TO
(out)(err)
O = 99882
T = 17.60
(out)(err)
normalized-g125.18.wcnf O = 74246
T = 41.85
O = N/A
T = TO
(out)(err)
O = 74246
T = 41.85
(out)(err)
normalized-g250.15.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = 618826
T = 28.07
(out)(err)
normalized-g250.29.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = 1007737
T = 50.83
(out)(err)
normalized-hanoi4.wcnf O = 718
T = 3.59
O = 718
T = 3.59
(out)(err)
O = 10775
T = 70.94
(out)(err)
normalized-hanoi5.wcnf O = 1931
T = 9.94
O = 1931
T = 9.94
(out)(err)
O = 125552
T = 41.69
(out)(err)
normalized-ii16a1.wcnf O = 1534
T = 3.14
O = 1534
T = 3.14
(out)(err)
O = 11232
T = 270.16
(out)(err)
normalized-ii16a2.wcnf O = 1445
T = 5.10
O = 1445
T = 5.10
(out)(err)
O = 19663
T = 148.94
(out)(err)
normalized-ii16b1.wcnf O = 1686
T = 276.30
O = 1686
T = 276.30
(out)(err)
O = 42283
T = 123.47
(out)(err)
normalized-ii16b2.wcnf O = 1035
T = 93.41
O = 1035
T = 93.41
(out)(err)
O = 17597
T = 14.53
(out)(err)
normalized-ii16c1.wcnf O = 1425
T = 1.99
O = 1425
T = 1.99
(out)(err)
O = 10820
T = 87.81
(out)(err)
normalized-ii16c2.wcnf O = 861
T = 6.46
O = 861
T = 6.46
(out)(err)
O = 15127
T = 12.06
(out)(err)
normalized-ii16d1.wcnf O = 1147
T = 9.62
O = 1147
T = 9.62
(out)(err)
O = 6014
T = 244.49
(out)(err)
normalized-ii16d2.wcnf O = 803
T = 189.34
O = 803
T = 189.34
(out)(err)
O = 8875
T = 211.53
(out)(err)
normalized-ii16e1.wcnf O = 1194
T = 97.93
O = 1194
T = 97.93
(out)(err)
O = 11056
T = 204.26
(out)(err)
normalized-ii16e2.wcnf O = 520
T = 2.98
O = 520
T = 2.98
(out)(err)
O = 2598
T = 92.43
(out)(err)
normalized-ii32a1.wcnf O = 444
T = 3.95
O = 444
T = 3.95
(out)(err)
O = 2241
T = 202.33
(out)(err)
normalized-ii32b1.wcnf O = 192
T = 36.32
O = 192
T = 36.32
(out)(err)
O = 198
T = 17.19
(out)(err)
normalized-ii32b2.wcnf O = 244
T = 5.68
O = 244
T = 5.68
(out)(err)
O = 1251
T = 39.45
(out)(err)
normalized-ii32b3.wcnf O = 331
T = 4.66
O = 331
T = 4.66
(out)(err)
O = 1686
T = 211.52
(out)(err)
normalized-ii32b4.wcnf O = 376
T = 2.52
O = 376
T = 2.52
(out)(err)
O = 1847
T = 127.99
(out)(err)
normalized-ii32c1.wcnf O = 168
T = 36.71
O = 187
T = 139.13
(out)(err)
O = 168
T = 36.71
(out)(err)
normalized-ii32c2.wcnf O = 214
T = 54.28
O = 214
T = 54.28
(out)(err)
O = 214
T = 159.96
(out)(err)
normalized-ii32c3.wcnf O = 261
T = 29.83
O = 261
T = 29.83
(out)(err)
O = 783
T = 26.51
(out)(err)
normalized-ii32c4.wcnf O = 736
T = 4.53
O = 736
T = 4.53
(out)(err)
O = 2230
T = 46.94
(out)(err)
normalized-ii32d1.wcnf O = 296
T = 91.71
O = 296
T = 91.71
(out)(err)
O = 1576
T = 236.62
(out)(err)
normalized-ii32d2.wcnf O = 373
T = 17.72
O = 373
T = 17.72
(out)(err)
O = 1938
T = 151.20
(out)(err)
normalized-ii32d3.wcnf O = 802
T = 24.03
O = 802
T = 24.03
(out)(err)
O = 4043
T = 38.45
(out)(err)
normalized-ii32e1.wcnf O = 162
T = 161.91
O = 174
T = 111.43
(out)(err)
O = 162
T = 161.91
(out)(err)
normalized-ii32e2.wcnf O = 235
T = 7.15
O = 235
T = 7.15
(out)(err)
O = 237
T = 67.70
(out)(err)
normalized-ii32e3.wcnf O = 310
T = 27.09
O = 310
T = 27.09
(out)(err)
O = 1598
T = 47.96
(out)(err)
normalized-ii32e4.wcnf O = 365
T = 248.03
O = 365
T = 248.03
(out)(err)
O = 1876
T = 40.21
(out)(err)
normalized-ii32e5.wcnf O = 503
T = 39.90
O = 503
T = 39.90
(out)(err)
O = 2529
T = 63.53
(out)(err)
normalized-ii8a1.wcnf O = 54
T = 1.93
O = 54
T = 1.93
(out)(err)
O = 54
T = 7.43
(out)(err)
normalized-ii8a2.wcnf O = 139
T = 15.68
O = 150
T = 2.84
(out)(err)
O = 139
T = 15.68
(out)(err)
normalized-ii8a3.wcnf O = 192
T = 68.40
O = 193
T = 212.56
(out)(err)
O = 192
T = 68.40
(out)(err)
normalized-ii8a4.wcnf O = 313
T = 4.61
O = 313
T = 4.61
(out)(err)
O = 1829
T = 133.47
(out)(err)
normalized-ii8b1.wcnf O = 198
T = 57.01
O = 220
T = 37.81
(out)(err)
O = 198
T = 57.01
(out)(err)
normalized-ii8b2.wcnf O = 413
T = 4.67
O = 413
T = 4.67
(out)(err)
O = 5972
T = 54.29
(out)(err)
normalized-ii8b3.wcnf O = 559
T = 2.02
O = 559
T = 2.02
(out)(err)
O = 10020
T = 44.17
(out)(err)
normalized-ii8b4.wcnf O = 718
T = 4.24
O = 718
T = 4.24
(out)(err)
O = 13086
T = 32.92
(out)(err)
normalized-ii8c1.wcnf O = 314
T = 14.48
O = 314
T = 14.48
(out)(err)
O = 330
T = 64.63
(out)(err)
normalized-ii8c2.wcnf O = 536
T = 5.12
O = 536
T = 5.12
(out)(err)
O = 8106
T = 238.24
(out)(err)
normalized-ii8d1.wcnf O = 351
T = 231.16
O = 374
T = 25.61
(out)(err)
O = 351
T = 231.16
(out)(err)
normalized-ii8d2.wcnf O = 581
T = 3.61
O = 581
T = 3.61
(out)(err)
O = 6143
T = 56.29
(out)(err)
normalized-ii8e1.wcnf O = 371
T = 58.92
O = 419
T = 20.90
(out)(err)
O = 371
T = 58.92
(out)(err)
normalized-ii8e2.wcnf O = 521
T = 2.44
O = 521
T = 2.44
(out)(err)
O = 7431
T = 98.05
(out)(err)
normalized-par32-1-c.wcnf O = 90339
T = 228.19
O = N/A
T = TO
(out)(err)
O = 90339
T = 228.19
(out)(err)
normalized-par32-1.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = 339445
T = 8.74
(out)(err)
normalized-par32-2-c.wcnf O = 102114
T = 197.33
O = N/A
T = TO
(out)(err)
O = 102114
T = 197.33
(out)(err)
normalized-par32-2.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = 326719
T = 51.63
(out)(err)
normalized-par32-3-c.wcnf O = 103829
T = 54.41
O = N/A
T = TO
(out)(err)
O = 103829
T = 54.41
(out)(err)
normalized-par32-3.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = 345797
T = 61.63
(out)(err)
normalized-par32-4-c.wcnf O = 101785
T = 107.40
O = N/A
T = TO
(out)(err)
O = 101785
T = 107.40
(out)(err)
normalized-par32-4.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = 352117
T = 61.14
(out)(err)
normalized-par32-5-c.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = 104920
T = 9.94
(out)(err)
normalized-par32-5.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = 358534
T = 8.47
(out)(err)
normalized-ssa7552-038.wcnf O = 1448
T = 4.19
O = 1448
T = 4.19
(out)(err)
O = 25375
T = 34.88
(out)(err)
normalized-ssa7552-158.wcnf O = 1327
T = 3.62
O = 1327
T = 3.62
(out)(err)
O = 14786
T = 94.93
(out)(err)
normalized-ssa7552-159.wcnf O = 1327
T = 4.76
O = 1327
T = 4.76
(out)(err)
O = 14787
T = 45.22
(out)(err)
normalized-ssa7552-160.wcnf O = 1359
T = 1.96
O = 1359
T = 1.96
(out)(err)
O = 15104
T = 226.40
(out)(err)
c1355_F1001gat-1048gat@1.wcnf O = 21
T = 8.08
O = 21
T = 8.08
(out)(err)
O = 173
T = 9.70
(out)(err)
c1355_F1001gat@1.wcnf O = 21
T = 8.27
O = 21
T = 8.27
(out)(err)
O = 178
T = 14.39
(out)(err)
c1355_F1036gat-1229gat@1.wcnf O = 13
T = 24.15
O = 13
T = 24.15
(out)(err)
O = 89
T = 5.75
(out)(err)
c1355_F1051gat@1.wcnf O = 13
T = 4.63
O = 13
T = 4.63
(out)(err)
O = 88
T = 136.22
(out)(err)
c1355_F106gat-409gat@1.wcnf O = 41
T = 4.38
O = 41
T = 4.38
(out)(err)
O = 1598
T = 191.05
(out)(err)
c1355_F106gat@0.wcnf O = 14
T = 55.72
O = 14
T = 55.72
(out)(err)
O = 2020
T = 42.87
(out)(err)
c1355_F113gat-1260gat@1.wcnf O = 13
T = 27.81
O = 13
T = 27.81
(out)(err)
O = 89
T = 61.54
(out)(err)
c1355_F1150gat@0.wcnf O = 13
T = 6.17
O = 13
T = 6.17
(out)(err)
O = 88
T = 131.67
(out)(err)
c1355_F1183gat-1262gat@1.wcnf O = 33
T = 5.04
O = 33
T = 5.04
(out)(err)
O = 91
T = 74.69
(out)(err)
c1355_F120gat-414gat@1.wcnf O = 33
T = 4.33
O = 33
T = 4.33
(out)(err)
O = 1778
T = 194.93
(out)(err)
c1355_F1229gat@1.wcnf O = 41
T = 4.93
O = 41
T = 4.93
(out)(err)
O = 93
T = 104.96
(out)(err)
c1355_F127gat-418gat@1.wcnf O = 41
T = 4.29
O = 41
T = 4.29
(out)(err)
O = 1772
T = 48.94
(out)(err)
c1355_F141gat@0.wcnf O = 14
T = 5.24
O = 14
T = 5.24
(out)(err)
O = 2267
T = 10.31
(out)(err)
c1355_F155gat@1.wcnf O = 14
T = 4.49
O = 14
T = 4.49
(out)(err)
O = 2025
T = 118.55
(out)(err)
c1355_F176gat-1278gat@1.wcnf O = 13
T = 18.92
O = 13
T = 18.92
(out)(err)
O = 91
T = 40.51
(out)(err)
c1355_F183gat@0.wcnf O = 14
T = 5.05
O = 14
T = 5.05
(out)(err)
O = 2015
T = 36.91
(out)(err)
c1355_F197gat-308gat@1.wcnf O = 33
T = 4.56
O = 33
T = 4.56
(out)(err)
O = 1935
T = 9.77
(out)(err)
c1355_F1gat@0.wcnf O = 14
T = 189.43
O = 14
T = 189.43
(out)(err)
O = 2184
T = 23.18
(out)(err)
c1355_F43gat@1.wcnf O = 14
T = 25.21
O = 14
T = 25.21
(out)(err)
O = 2106
T = 43.46
(out)(err)
c1355_F50gat@1.wcnf O = 14
T = 41.26
O = 14
T = 41.26
(out)(err)
O = 2105
T = 242.49
(out)(err)
c1355_F543gat@1.wcnf O = 33
T = 4.85
O = 33
T = 4.85
(out)(err)
O = 1436
T = 19.47
(out)(err)
c1355_F57gat@1.wcnf O = 14
T = 24.56
O = 14
T = 24.56
(out)(err)
O = 1861
T = 271.36
(out)(err)
c1355_F71gat@1.wcnf O = 14
T = 4.80
O = 14
T = 4.80
(out)(err)
O = 2190
T = 29.92
(out)(err)
c3540_F20@1.wcnf O = 6
T = 23.36
O = 6
T = 23.36
(out)(err)
O = 18210
T = 51.71
(out)(err)
c3540_F41@1.wcnf O = 7
T = 11.39
O = 7
T = 11.39
(out)(err)
O = 13874
T = 73.11
(out)(err)
c3540_F45@0.wcnf O = 9
T = 5.83
O = 9
T = 5.83
(out)(err)
O = 13761
T = 49.74
(out)(err)
c3540_F45@1.wcnf O = 9
T = 21.86
O = 9
T = 21.86
(out)(err)
O = 14272
T = 77.32
(out)(err)
c499_Fic0@1.wcnf O = 41
T = 1.63
O = 41
T = 1.63
(out)(err)
O = 369
T = 41.52
(out)(err)
c499_Fic2@1.wcnf O = 41
T = 1.55
O = 41
T = 1.55
(out)(err)
O = 442
T = 81.23
(out)(err)
c499_Fic6@1.wcnf O = 41
T = 4.49
O = 41
T = 4.49
(out)(err)
O = 361
T = 23.95
(out)(err)
c499_Fid11@1.wcnf O = 14
T = 5.96
O = 14
T = 5.96
(out)(err)
O = 369
T = 137.06
(out)(err)
c499_Fid18@0.wcnf O = 14
T = 5.50
O = 14
T = 5.50
(out)(err)
O = 446
T = 83.28
(out)(err)
c499_Fid20-xa10@0.wcnf O = 33
T = 2.36
O = 33
T = 2.36
(out)(err)
O = 451
T = 140.36
(out)(err)
c499_Fid26@0.wcnf O = 14
T = 1.93
O = 14
T = 1.93
(out)(err)
O = 520
T = 30.77
(out)(err)
c499_Fxa10@0.wcnf O = 33
T = 4.83
O = 33
T = 4.83
(out)(err)
O = 534
T = 43.78
(out)(err)
c6288_F137gat@1.wcnf O = 10
T = 135.54
O = 10
T = 135.54
(out)(err)
O = 13678
T = 27.24
(out)(err)
c6288_F18gat@0.wcnf O = 3
T = 3.36
O = 3
T = 3.36
(out)(err)
O = 9000
T = 57.05
(out)(err)
c6288_F205gat@1.wcnf O = 20
T = 109.84
O = 20
T = 109.84
(out)(err)
O = 14461
T = 49.66
(out)(err)
c6288_F35gat@1.wcnf O = 4
T = 4.88
O = 4
T = 4.88
(out)(err)
O = 10556
T = 148.05
(out)(err)
c6288_F69gat@1.wcnf O = 6
T = 10.08
O = 6
T = 10.08
(out)(err)
O = 11144
T = 37.47
(out)(err)
normalized-5xp1.b.wcnf O = 13
T = 7.95
O = 15
T = 13.13
(out)(err)
O = 13
T = 7.95
(out)(err)
normalized-9sym.b.wcnf O = 5
T = 13.83
O = 5
T = 4.22
(out)(err)
O = 5
T = 13.83
(out)(err)
normalized-C499.a.wcnf O = 82
T = 51.44
O = 83
T = 2.13
(out)(err)
O = 82
T = 51.44
(out)(err)
normalized-C499.b.wcnf O = 83
T = 71.08
O = 83
T = 4.54
(out)(err)
O = 83
T = 71.08
(out)(err)
normalized-C880.a.wcnf O = 89
T = 13.90
O = 91
T = 4.85
(out)(err)
O = 89
T = 13.90
(out)(err)
normalized-C880.b.wcnf O = 70
T = 93.23
O = 80
T = 3.63
(out)(err)
O = 70
T = 93.23
(out)(err)
normalized-addm4.r.wcnf O = 173
T = 32.79
O = 189
T = 2.45
(out)(err)
O = 173
T = 32.79
(out)(err)
normalized-alu2.b.wcnf O = 64
T = 37.41
O = 81
T = 184.44
(out)(err)
O = 64
T = 37.41
(out)(err)
normalized-alu4.b.wcnf O = 52
T = 21.05
O = 61
T = 119.60
(out)(err)
O = 52
T = 21.05
(out)(err)
normalized-apex4.a.wcnf O = N/A
T = TO
O = 803
T = 138.55
(out)(err)
O = 807
T = 57.30
(out)(err)
normalized-apex6.b.wcnf O = 148
T = 207.80
O = 174
T = 59.07
(out)(err)
O = 148
T = 207.80
(out)(err)
normalized-apex7.b.wcnf O = 40
T = 166.47
O = 51
T = 3.87
(out)(err)
O = 40
T = 166.47
(out)(err)
normalized-bbara.r.wcnf O = 7
T = 0.12
O = 7
T = 0.76
(out)(err)
O = 7
T = 0.12
(out)(err)
normalized-bench1.pi.wcnf O = N/A
T = TO
O = 159
T = 3.53
(out)(err)
O = 166
T = 30.97
(out)(err)
normalized-bench1.r.wcnf O = N/A
T = TO
O = 167
T = 11.17
(out)(err)
O = 166
T = 0.01
(out)(err)
normalized-bw.b.wcnf O = 33
T = 127.39
O = 34
T = 5.30
(out)(err)
O = 33
T = 127.39
(out)(err)
normalized-clip.b.wcnf O = 15
T = 35.73
O = 17
T = 40.31
(out)(err)
O = 15
T = 35.73
(out)(err)
normalized-count.b.wcnf O = 25
T = 15.93
O = 26
T = 19.66
(out)(err)
O = 25
T = 15.93
(out)(err)
normalized-des.a.wcnf O = 1054
T = 207.02
O = 999
T = 5.78
(out)(err)
O = 1054
T = 207.02
(out)(err)
normalized-dk512x.r.wcnf O = 6
T = 1.41
O = 6
T = 3.64
(out)(err)
O = 6
T = 1.41
(out)(err)
normalized-duke2.b.wcnf O = 75
T = 59.66
O = 95
T = 91.84
(out)(err)
O = 75
T = 59.66
(out)(err)
normalized-e64.b.wcnf O = 52
T = 22.72
O = 79
T = 146.11
(out)(err)
O = 52
T = 22.72
(out)(err)
normalized-ex1010.pi.wcnf O = N/A
T = TO
O = 423
T = 3.15
(out)(err)
O = 433
T = 77.19
(out)(err)
normalized-ex4inp.r.wcnf O = 5
T = 9.31
O = 5
T = 4.52
(out)(err)
O = 5
T = 9.31
(out)(err)
normalized-ex5.pi.wcnf O = 72
T = 122.63
O = 80
T = 4.73
(out)(err)
O = 72
T = 122.63
(out)(err)
normalized-ex5.r.wcnf O = 48
T = 9.65
O = 55
T = 75.95
(out)(err)
O = 48
T = 9.65
(out)(err)
normalized-ex5inp.r.wcnf O = 4
T = 0.88
O = 4
T = 0.88
(out)(err)
O = 4
T = 1.03
(out)(err)
normalized-ex6inp.r.wcnf O = 4
T = 2.32
O = 4
T = 1.43
(out)(err)
O = 4
T = 2.32
(out)(err)
normalized-exam.pi.wcnf O = N/A
T = TO
O = 87
T = 62.69
(out)(err)
O = 100
T = 1.81
(out)(err)
normalized-exps.r.wcnf O = 79
T = 239.25
O = 86
T = 2.47
(out)(err)
O = 79
T = 239.25
(out)(err)
normalized-f51m.b.wcnf O = 18
T = 31.06
O = 20
T = 28.91
(out)(err)
O = 18
T = 31.06
(out)(err)
normalized-fout.r.wcnf O = 39
T = 161.41
O = 45
T = 28.61
(out)(err)
O = 39
T = 161.41
(out)(err)
normalized-jac3.wcnf O = 17
T = 61.13
O = 24
T = 145.88
(out)(err)
O = 17
T = 61.13
(out)(err)
normalized-lin.rom.r.wcnf O = 138
T = 141.94
O = 174
T = 1.26
(out)(err)
O = 138
T = 141.94
(out)(err)
normalized-m100_100_10_10.r.wcnf O = 13
T = 3.07
O = 16
T = 4.58
(out)(err)
O = 13
T = 3.07
(out)(err)
normalized-m100_100_10_15.r.wcnf O = 10
T = 7.24
O = 11
T = 45.71
(out)(err)
O = 10
T = 7.24
(out)(err)
normalized-m100_100_10_30.r.wcnf O = 8
T = 47.14
O = 9
T = 52.19
(out)(err)
O = 8
T = 47.14
(out)(err)
normalized-m100_100_30_30.r.wcnf O = 5
T = 5.65
O = 5
T = 5.65
(out)(err)
O = 5
T = 9.23
(out)(err)
normalized-m100_100_50_50.r.wcnf O = 4
T = 1.42
O = 4
T = 1.42
(out)(err)
O = 4
T = 4.01
(out)(err)
normalized-m100_100_70_70.r.wcnf O = 3
T = 2.40
O = 3
T = 2.40
(out)(err)
O = 3
T = 3.06
(out)(err)
normalized-m100_100_90_90.r.wcnf O = 2
T = 0.84
O = 2
T = 0.84
(out)(err)
O = 2
T = 3.66
(out)(err)
normalized-m100_300_10_10.r.wcnf O = 24
T = 99.27
O = 32
T = 2.79
(out)(err)
O = 24
T = 99.27
(out)(err)
normalized-m100_300_10_14.r.wcnf O = 20
T = 37.27
O = 28
T = 29.27
(out)(err)
O = 20
T = 37.27
(out)(err)
normalized-m100_300_10_15.r.wcnf O = 20
T = 11.38
O = 30
T = 8.76
(out)(err)
O = 20
T = 11.38
(out)(err)
normalized-m100_300_10_20.r.wcnf O = 18
T = 25.07
O = 27
T = 4.17
(out)(err)
O = 18
T = 25.07
(out)(err)
normalized-m100_50_10_10.r.wcnf O = 8
T = 2.03
O = 8
T = 215.14
(out)(err)
O = 8
T = 2.03
(out)(err)
normalized-m100_50_20_20.r.wcnf O = 5
T = 2.11
O = 5
T = 4.25
(out)(err)
O = 5
T = 2.11
(out)(err)
normalized-m100_50_30_30.r.wcnf O = 3
T = 1.14
O = 3
T = 1.14
(out)(err)
O = 3
T = 1.55
(out)(err)
normalized-m100_50_40_40.r.wcnf O = 2
T = 0.55
O = 2
T = 0.55
(out)(err)
O = 2
T = 2.00
(out)(err)
normalized-m200_500_10_10.r.wcnf O = 44
T = 169.90
O = 58
T = 3.85
(out)(err)
O = 44
T = 169.90
(out)(err)
normalized-m4.r.wcnf O = 97
T = 20.70
O = 108
T = 1.86
(out)(err)
O = 97
T = 20.70
(out)(err)
normalized-m50_100_10_10.r.wcnf O = 8
T = 2.00
O = 9
T = 1.32
(out)(err)
O = 8
T = 2.00
(out)(err)
normalized-m50_100_10_15.r.wcnf O = 8
T = 2.59
O = 9
T = 5.32
(out)(err)
O = 8
T = 2.59
(out)(err)
normalized-m50_100_30_30.r.wcnf O = 4
T = 2.97
O = 4
T = 15.52
(out)(err)
O = 4
T = 2.97
(out)(err)
normalized-m50_100_50_50.r.wcnf O = 3
T = 0.77
O = 3
T = 1.18
(out)(err)
O = 3
T = 0.77
(out)(err)
normalized-m50_100_70_70.r.wcnf O = 2
T = 0.89
O = 2
T = 0.89
(out)(err)
O = 2
T = 1.81
(out)(err)
normalized-m50_100_90_90.r.wcnf O = 2
T = 2.55
O = 2
T = 0.57
(out)(err)
O = 2
T = 2.55
(out)(err)
normalized-maincont.r.wcnf O = 7
T = 1.40
O = 7
T = 3.55
(out)(err)
O = 7
T = 1.40
(out)(err)
normalized-max1024.pi.wcnf O = 283
T = 229.78
O = 303
T = 2.71
(out)(err)
O = 283
T = 229.78
(out)(err)
normalized-max1024.r.wcnf O = 270
T = 151.22
O = 300
T = 23.79
(out)(err)
O = 270
T = 151.22
(out)(err)
normalized-max512.r.wcnf O = 119
T = 176.88
O = 138
T = 5.01
(out)(err)
O = 119
T = 176.88
(out)(err)
normalized-mlp4.r.wcnf O = 115
T = 18.57
O = 128
T = 2.75
(out)(err)
O = 115
T = 18.57
(out)(err)
normalized-opus.r.wcnf O = 5
T = 2.29
O = 5
T = 1.14
(out)(err)
O = 5
T = 2.29
(out)(err)
normalized-pdc.r.wcnf O = 206
T = 28.29
O = 138
T = 5.48
(out)(err)
O = 206
T = 28.29
(out)(err)
normalized-prom2.pi.wcnf O = 361
T = 183.13
O = 429
T = 3.52
(out)(err)
O = 361
T = 183.13
(out)(err)
normalized-prom2.r.wcnf O = 352
T = 130.40
O = 437
T = 4.88
(out)(err)
O = 352
T = 130.40
(out)(err)
normalized-rd73.b.wcnf O = 4
T = 6.38
O = 4
T = 2.73
(out)(err)
O = 4
T = 6.38
(out)(err)
normalized-rd84.b.wcnf O = 7
T = 48.12
O = 7
T = 73.00
(out)(err)
O = 7
T = 48.12
(out)(err)
normalized-ricks.r.wcnf O = 5
T = 14.97
O = 5
T = 3.00
(out)(err)
O = 5
T = 14.97
(out)(err)
normalized-rot.b.wcnf O = 127
T = 35.53
O = 152
T = 2.90
(out)(err)
O = 127
T = 35.53
(out)(err)
normalized-sao2.b.wcnf O = 27
T = 36.13
O = 31
T = 17.01
(out)(err)
O = 27
T = 36.13
(out)(err)
normalized-saucier.r.wcnf O = 7
T = 109.50
O = 10
T = 53.95
(out)(err)
O = 7
T = 109.50
(out)(err)
normalized-test1.r.wcnf O = N/A
T = TO
O = 137
T = 193.97
(out)(err)
O = 138
T = 14.81
(out)(err)
normalized-test4.pi.wcnf O = 140
T = 56.80
O = 178
T = 46.51
(out)(err)
O = 140
T = 56.80
(out)(err)
ctrl.wcnf O = N/A
T = TO
O = 15
T = 2.87
(out)(err)
O = 5806
T = 24.24
(out)(err)
mrisc_mem2wire.wcnf O = N/A
T = TO
O = 5
T = 55.77
(out)(err)
O = 1011645
T = 212.66
(out)(err)
spi.wcnf O = N/A
T = TO
O = 46
T = 27.35
(out)(err)
O = 154347
T = 148.02
(out)(err)
sudoku.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
splitedReads_0.matrix.wcnf O = 3105
T = 3.97
O = 3105
T = 3.97
(out)(err)
O = 5051
T = 45.70
(out)(err)
splitedReads_137.matrix.wcnf O = 472
T = 2.62
O = 472
T = 2.62
(out)(err)
O = 3411
T = 11.24
(out)(err)
splitedReads_158.matrix.wcnf O = 568
T = 3.56
O = 568
T = 3.56
(out)(err)
O = 4458
T = 28.82
(out)(err)
splitedReads_160.matrix.wcnf O = 614
T = 4.03
O = 614
T = 4.03
(out)(err)
O = 5110
T = 10.47
(out)(err)
splitedReads_18.matrix.wcnf O = 553
T = 3.62
O = 553
T = 3.62
(out)(err)
O = 3917
T = 70.84
(out)(err)
splitedReads_414.matrix.wcnf O = 618
T = 3.01
O = 618
T = 3.01
(out)(err)
O = 4185
T = 69.49
(out)(err)
10tree1005p.wcnf O = 10
T = 37.89
O = 10
T = 37.89
(out)(err)
O = 34188
T = 65.51
(out)(err)
10tree1010p.wcnf O = 20
T = 80.49
O = 20
T = 80.49
(out)(err)
O = 35034
T = 13.67
(out)(err)
10tree1015p.wcnf O = 31
T = 171.30
O = 31
T = 171.30
(out)(err)
O = 36099
T = 44.71
(out)(err)
10tree1020p.wcnf O = 42
T = 53.82
O = 42
T = 53.82
(out)(err)
O = 36097
T = 15.42
(out)(err)
10tree1025p.wcnf O = 52
T = 68.23
O = 52
T = 68.23
(out)(err)
O = 37805
T = 40.39
(out)(err)
10tree1030p.wcnf O = 63
T = 208.25
O = 63
T = 208.25
(out)(err)
O = 40950
T = 61.54
(out)(err)
10tree110p.wcnf O = 20
T = 116.52
O = 20
T = 116.52
(out)(err)
O = 34203
T = 81.87
(out)(err)
10tree115p.wcnf O = 29
T = 25.22
O = 29
T = 25.22
(out)(err)
O = 35247
T = 87.05
(out)(err)
10tree120p.wcnf O = 41
T = 144.70
O = 41
T = 144.70
(out)(err)
O = 39491
T = 51.26
(out)(err)
10tree125p.wcnf O = 57
T = 287.93
O = 57
T = 287.93
(out)(err)
O = 36113
T = 123.92
(out)(err)
10tree130p.wcnf O = 86
T = 246.57
O = 86
T = 246.57
(out)(err)
O = 38017
T = 222.47
(out)(err)
10tree210p.wcnf O = 21
T = 194.32
O = 21
T = 194.32
(out)(err)
O = 32302
T = 46.47
(out)(err)
10tree215p.wcnf O = 31
T = 215.41
O = 31
T = 215.41
(out)(err)
O = 35466
T = 52.01
(out)(err)
10tree220p.wcnf O = 70
T = 271.42
O = 70
T = 271.42
(out)(err)
O = 38211
T = 19.87
(out)(err)
10tree225p.wcnf O = 59
T = 260.02
O = 59
T = 260.02
(out)(err)
O = 35263
T = 68.11
(out)(err)
10tree230p.wcnf O = 82
T = 177.56
O = 82
T = 177.56
(out)(err)
O = 33149
T = 47.97
(out)(err)
10tree305p.wcnf O = 9
T = 12.04
O = 9
T = 12.04
(out)(err)
O = 35467
T = 56.74
(out)(err)
10tree310p.wcnf O = 20
T = 41.92
O = 20
T = 41.92
(out)(err)
O = 36097
T = 83.94
(out)(err)
10tree315p.wcnf O = 30
T = 56.01
O = 30
T = 56.01
(out)(err)
O = 38843
T = 59.17
(out)(err)
10tree320p.wcnf O = 42
T = 55.69
O = 42
T = 55.69
(out)(err)
O = 34205
T = 5.37
(out)(err)
10tree325p.wcnf O = 53
T = 241.42
O = 53
T = 241.42
(out)(err)
O = 38841
T = 73.20
(out)(err)
10tree330p.wcnf O = 74
T = 152.34
O = 74
T = 152.34
(out)(err)
O = 38015
T = 76.44
(out)(err)
10tree405p.wcnf O = 9
T = 38.56
O = 9
T = 38.56
(out)(err)
O = 36937
T = 66.34
(out)(err)
10tree405posib.wcnf O = 35032
T = 63.71
O = 10
T = 4.85
(out)(err)
O = 35032
T = 63.71
(out)(err)
10tree410p.wcnf O = 21
T = 227.90
O = 21
T = 227.90
(out)(err)
O = 34407
T = 78.74
(out)(err)
10tree415p.wcnf O = 31
T = 166.60
O = 31
T = 166.60
(out)(err)
O = 32928
T = 52.61
(out)(err)
10tree420p.wcnf O = 41
T = 256.06
O = 41
T = 256.06
(out)(err)
O = 35468
T = 86.65
(out)(err)
10tree425p.wcnf O = 68
T = 239.04
O = 68
T = 239.04
(out)(err)
O = 37152
T = 35.89
(out)(err)
10tree430p.wcnf O = 70
T = 275.11
O = 70
T = 275.11
(out)(err)
O = 40529
T = 42.69
(out)(err)
10tree505p.wcnf O = 10
T = 20.20
O = 10
T = 20.20
(out)(err)
O = 36512
T = 61.03
(out)(err)
10tree505posib.wcnf O = 33351
T = 16.07
O = 10
T = 10.13
(out)(err)
O = 33351
T = 16.07
(out)(err)
10tree510p.wcnf O = 21
T = 121.97
O = 21
T = 121.97
(out)(err)
O = 33356
T = 70.83
(out)(err)
10tree515p.wcnf O = 29
T = 181.29
O = 29
T = 181.29
(out)(err)
O = 35044
T = 83.83
(out)(err)
10tree520p.wcnf O = 48
T = 247.18
O = 48
T = 247.18
(out)(err)
O = 35272
T = 30.27
(out)(err)
10tree525p.wcnf O = 62
T = 129.53
O = 62
T = 129.53
(out)(err)
O = 40108
T = 82.79
(out)(err)
10tree530p.wcnf O = 78
T = 240.63
O = 78
T = 240.63
(out)(err)
O = 35910
T = 49.96
(out)(err)
10tree605p.wcnf O = 9
T = 53.19
O = 9
T = 53.19
(out)(err)
O = 34399
T = 93.78
(out)(err)
10tree605posib.wcnf O = 32716
T = 51.30
O = 9
T = 8.67
(out)(err)
O = 32716
T = 51.30
(out)(err)
10tree610p.wcnf O = 19
T = 171.09
O = 19
T = 171.09
(out)(err)
O = 37370
T = 49.84
(out)(err)
10tree615p.wcnf O = 26
T = 269.58
O = 26
T = 269.58
(out)(err)
O = 36104
T = 67.45
(out)(err)
10tree620p.wcnf O = 60
T = 245.25
O = 60
T = 245.25
(out)(err)
O = 35045
T = 37.55
(out)(err)
10tree625p.wcnf O = 56
T = 246.93
O = 56
T = 246.93
(out)(err)
O = 35257
T = 35.92
(out)(err)
10tree630p.wcnf O = 72
T = 131.87
O = 72
T = 131.87
(out)(err)
O = 31456
T = 86.14
(out)(err)
10tree705p.wcnf O = 10
T = 46.59
O = 10
T = 46.59
(out)(err)
O = 30396
T = 106.51
(out)(err)
10tree705posib.wcnf O = 31042
T = 227.38
O = 10
T = 35.22
(out)(err)
O = 31042
T = 227.38
(out)(err)
10tree710p.wcnf O = 21
T = 50.09
O = 21
T = 50.09
(out)(err)
O = 34208
T = 152.41
(out)(err)
10tree715p.wcnf O = 54
T = 167.07
O = 54
T = 167.07
(out)(err)
O = 40324
T = 68.89
(out)(err)
10tree720p.wcnf O = 66
T = 258.03
O = 66
T = 258.03
(out)(err)
O = 33783
T = 8.44
(out)(err)
10tree725p.wcnf O = 66
T = 266.10
O = 66
T = 266.10
(out)(err)
O = 38639
T = 10.93
(out)(err)
10tree730p.wcnf O = 91
T = 131.73
O = 91
T = 131.73
(out)(err)
O = 41377
T = 79.94
(out)(err)
10tree805p.wcnf O = 9
T = 16.79
O = 9
T = 16.79
(out)(err)
O = 38833
T = 5.51
(out)(err)
10tree805posib.wcnf O = 35457
T = 79.75
O = 10
T = 13.30
(out)(err)
O = 35457
T = 79.75
(out)(err)
10tree810p.wcnf O = 21
T = 22.10
O = 21
T = 22.10
(out)(err)
O = 32085
T = 9.22
(out)(err)
10tree815p.wcnf O = 31
T = 46.56
O = 31
T = 46.56
(out)(err)
O = 40310
T = 35.36
(out)(err)
10tree820p.wcnf O = 42
T = 151.94
O = 42
T = 151.94
(out)(err)
O = 32944
T = 11.55
(out)(err)
10tree825p.wcnf O = 68
T = 263.22
O = 68
T = 263.22
(out)(err)
O = 34225
T = 12.38
(out)(err)
10tree830p.wcnf O = 83
T = 186.99
O = 83
T = 186.99
(out)(err)
O = 38431
T = 12.66
(out)(err)
10tree905p.wcnf O = 10
T = 26.07
O = 10
T = 26.07
(out)(err)
O = 36508
T = 48.20
(out)(err)
10tree905posib.wcnf O = 39691
T = 86.91
O = 10
T = 10.27
(out)(err)
O = 39691
T = 86.91
(out)(err)
10tree910p.wcnf O = 20
T = 13.50
O = 20
T = 13.50
(out)(err)
O = 36108
T = 60.59
(out)(err)
10tree915p.wcnf O = 47
T = 286.43
O = 47
T = 286.43
(out)(err)
O = 37782
T = 66.72
(out)(err)
10tree920p.wcnf O = 52
T = 241.29
O = 52
T = 241.29
(out)(err)
O = 38217
T = 13.92
(out)(err)
10tree925p.wcnf O = 66
T = 167.78
O = 66
T = 167.78
(out)(err)
O = 38020
T = 212.52
(out)(err)
10tree930p.wcnf O = 78
T = 286.07
O = 78
T = 286.07
(out)(err)
O = 40945
T = 49.80
(out)(err)
15tree1001p.wcnf O = 463
T = 45.27
O = 463
T = 45.27
(out)(err)
O = 1124274
T = 84.65
(out)(err)
15tree1001posib.wcnf O = N/A
T = TO
O = 151
T = 4.60
(out)(err)
O = 1008141
T = 94.83
(out)(err)
15tree101p.wcnf O = 447
T = 95.83
O = 447
T = 95.83
(out)(err)
O = 1107890
T = 88.56
(out)(err)
15tree101posib.wcnf O = N/A
T = TO
O = 273
T = 203.62
(out)(err)
O = 1122907
T = 86.53
(out)(err)
15tree201p.wcnf O = 689
T = 5.83
O = 689
T = 5.83
(out)(err)
O = 1049139
T = 94.99
(out)(err)
15tree201posib.wcnf O = N/A
T = TO
O = 573
T = 173.07
(out)(err)
O = 1084631
T = 111.07
(out)(err)
15tree301p.wcnf O = 642
T = 4.17
O = 642
T = 4.17
(out)(err)
O = 1080553
T = 100.09
(out)(err)
15tree301posib.wcnf O = N/A
T = TO
O = 13
T = 92.66
(out)(err)
O = 1165276
T = 67.69
(out)(err)
15tree401p.wcnf O = 348
T = 228.43
O = 348
T = 228.43
(out)(err)
O = 1101048
T = 83.96
(out)(err)
15tree401posib.wcnf O = N/A
T = TO
O = 200
T = 186.03
(out)(err)
O = 1132477
T = 77.14
(out)(err)
15tree501p.wcnf O = 508
T = 7.37
O = 508
T = 7.37
(out)(err)
O = 1025878
T = 90.74
(out)(err)
15tree501posib.wcnf O = N/A
T = TO
O = 13
T = 280.11
(out)(err)
O = 984921
T = 96.22
(out)(err)
15tree601p.wcnf O = 483
T = 5.38
O = 483
T = 5.38
(out)(err)
O = 1102412
T = 83.97
(out)(err)
15tree601posib.wcnf O = N/A
T = TO
O = 313
T = 198.49
(out)(err)
O = 1042298
T = 99.88
(out)(err)
15tree701p.wcnf O = 544
T = 152.67
O = 544
T = 152.67
(out)(err)
O = 1229447
T = 90.96
(out)(err)
15tree701posib.wcnf O = N/A
T = TO
O = 13
T = 273.34
(out)(err)
O = 1002684
T = 88.51
(out)(err)
15tree801p.wcnf O = 646
T = 237.32
O = 646
T = 237.32
(out)(err)
O = 994476
T = 110.22
(out)(err)
15tree801posib.wcnf O = N/A
T = TO
O = 13
T = 273.77
(out)(err)
O = 1192580
T = 69.27
(out)(err)
15tree901p.wcnf O = 594
T = 4.07
O = 594
T = 4.07
(out)(err)
O = 1050504
T = 101.57
(out)(err)
15tree901posib.wcnf O = N/A
T = TO
O = 13
T = 102.97
(out)(err)
O = 1042312
T = 100.05
(out)(err)
10tree1005p.wcnf O = 10
T = 44.41
O = 10
T = 44.41
(out)(err)
O = 23873
T = 185.04
(out)(err)
10tree1010p.wcnf O = 20
T = 30.74
O = 20
T = 30.74
(out)(err)
O = 25553
T = 28.30
(out)(err)
10tree1015p.wcnf O = 31
T = 30.78
O = 31
T = 30.78
(out)(err)
O = 23441
T = 85.62
(out)(err)
10tree1020p.wcnf O = 42
T = 7.95
O = 42
T = 7.95
(out)(err)
O = 26399
T = 194.43
(out)(err)
10tree1025p.wcnf O = 52
T = 43.06
O = 52
T = 43.06
(out)(err)
O = 27478
T = 21.04
(out)(err)
10tree1030p.wcnf O = 63
T = 143.36
O = 63
T = 143.36
(out)(err)
O = 25371
T = 229.31
(out)(err)
10tree110p.wcnf O = 21
T = 5.88
O = 21
T = 5.88
(out)(err)
O = 24077
T = 56.75
(out)(err)
10tree115p.wcnf O = 31
T = 47.68
O = 31
T = 47.68
(out)(err)
O = 24091
T = 67.07
(out)(err)
10tree120p.wcnf O = 42
T = 108.21
O = 42
T = 108.21
(out)(err)
O = 23447
T = 104.22
(out)(err)
10tree125p.wcnf O = 52
T = 75.62
O = 52
T = 75.62
(out)(err)
O = 26619
T = 212.24
(out)(err)
10tree130p.wcnf O = 90
T = 219.03
O = 90
T = 219.03
(out)(err)
O = 25580
T = 144.34
(out)(err)
10tree210p.wcnf O = 21
T = 74.23
O = 21
T = 74.23
(out)(err)
O = 23865
T = 85.15
(out)(err)
10tree215p.wcnf O = 31
T = 98.72
O = 31
T = 98.72
(out)(err)
O = 22404
T = 247.93
(out)(err)
10tree220p.wcnf O = 42
T = 221.64
O = 42
T = 221.64
(out)(err)
O = 23665
T = 122.86
(out)(err)
10tree225p.wcnf O = 68
T = 267.77
O = 68
T = 267.77
(out)(err)
O = 24111
T = 14.37
(out)(err)
10tree230p.wcnf O = 79
T = 265.86
O = 79
T = 265.86
(out)(err)
O = 29174
T = 14.80
(out)(err)
10tree305p.wcnf O = 10
T = 4.83
O = 10
T = 4.83
(out)(err)
O = 19639
T = 53.80
(out)(err)
10tree310p.wcnf O = 21
T = 31.32
O = 21
T = 31.32
(out)(err)
O = 21958
T = 42.06
(out)(err)
10tree315p.wcnf O = 31
T = 15.17
O = 31
T = 15.17
(out)(err)
O = 24935
T = 40.22
(out)(err)
10tree320p.wcnf O = 42
T = 29.65
O = 42
T = 29.65
(out)(err)
O = 25780
T = 131.08
(out)(err)
10tree325p.wcnf O = 52
T = 137.53
O = 52
T = 137.53
(out)(err)
O = 26619
T = 83.54
(out)(err)
10tree330p.wcnf O = 63
T = 241.89
O = 63
T = 241.89
(out)(err)
O = 27488
T = 59.56
(out)(err)
10tree405p.wcnf O = 10
T = 7.14
O = 10
T = 7.14
(out)(err)
O = 24916
T = 78.79
(out)(err)
10tree405posib.wcnf O = 22592
T = 58.21
O = 10
T = 4.95
(out)(err)
O = 22592
T = 58.21
(out)(err)
10tree410p.wcnf O = 21
T = 21.69
O = 21
T = 21.69
(out)(err)
O = 24716
T = 84.14
(out)(err)
10tree415p.wcnf O = 31
T = 31.19
O = 31
T = 31.19
(out)(err)
O = 23023
T = 261.70
(out)(err)
10tree420p.wcnf O = 42
T = 56.47
O = 42
T = 56.47
(out)(err)
O = 25144
T = 119.30
(out)(err)
10tree425p.wcnf O = 52
T = 153.96
O = 52
T = 153.96
(out)(err)
O = 28116
T = 173.50
(out)(err)
10tree430p.wcnf O = 63
T = 126.37
O = 63
T = 126.37
(out)(err)
O = 26850
T = 87.81
(out)(err)
10tree505p.wcnf O = 10
T = 5.41
O = 10
T = 5.41
(out)(err)
O = 23014
T = 106.35
(out)(err)
10tree505posib.wcnf O = 23008
T = 86.78
O = 10
T = 3.66
(out)(err)
O = 23008
T = 86.78
(out)(err)
10tree510p.wcnf O = 21
T = 8.36
O = 21
T = 8.36
(out)(err)
O = 25569
T = 51.06
(out)(err)
10tree515p.wcnf O = 31
T = 61.39
O = 31
T = 61.39
(out)(err)
O = 22620
T = 68.53
(out)(err)
10tree520p.wcnf O = 42
T = 98.88
O = 42
T = 98.88
(out)(err)
O = 23034
T = 44.44
(out)(err)
10tree525p.wcnf O = 52
T = 136.28
O = 52
T = 136.28
(out)(err)
O = 24302
T = 141.85
(out)(err)
10tree530p.wcnf O = 70
T = 274.13
O = 70
T = 274.13
(out)(err)
O = 28522
T = 245.60
(out)(err)
10tree605p.wcnf O = 9
T = 8.53
O = 9
T = 8.53
(out)(err)
O = 22590
T = 186.59
(out)(err)
10tree605posib.wcnf O = 17316
T = 249.20
O = 9
T = 4.40
(out)(err)
O = 17316
T = 249.20
(out)(err)
10tree610p.wcnf O = 19
T = 63.59
O = 19
T = 63.59
(out)(err)
O = 20484
T = 142.28
(out)(err)
10tree615p.wcnf O = 26
T = 46.43
O = 26
T = 46.43
(out)(err)
O = 23235
T = 192.15
(out)(err)
10tree620p.wcnf O = 39
T = 172.46
O = 39
T = 172.46
(out)(err)
O = 24509
T = 117.30
(out)(err)
10tree625p.wcnf O = 52
T = 242.46
O = 52
T = 242.46
(out)(err)
O = 25785
T = 157.03
(out)(err)
10tree630p.wcnf O = 63
T = 222.14
O = 63
T = 222.14
(out)(err)
O = 20099
T = 284.78
(out)(err)
10tree705p.wcnf O = 10
T = 3.96
O = 10
T = 3.96
(out)(err)
O = 24288
T = 59.68
(out)(err)
10tree705posib.wcnf O = 23860
T = 54.78
O = 10
T = 6.33
(out)(err)
O = 23860
T = 54.78
(out)(err)
10tree710p.wcnf O = 21
T = 37.75
O = 21
T = 37.75
(out)(err)
O = 22389
T = 74.91
(out)(err)
10tree715p.wcnf O = 31
T = 103.01
O = 31
T = 103.01
(out)(err)
O = 21761
T = 124.68
(out)(err)
10tree720p.wcnf O = 42
T = 149.91
O = 42
T = 149.91
(out)(err)
O = 26193
T = 101.80
(out)(err)
10tree725p.wcnf O = 52
T = 235.58
O = 52
T = 235.58
(out)(err)
O = 26835
T = 40.93
(out)(err)
10tree730p.wcnf O = 79
T = 272.86
O = 79
T = 272.86
(out)(err)
O = 29803
T = 101.43
(out)(err)
10tree805p.wcnf O = 10
T = 14.10
O = 10
T = 14.10
(out)(err)
O = 22387
T = 183.24
(out)(err)
10tree805posib.wcnf O = 18587
T = 27.15
O = 10
T = 7.08
(out)(err)
O = 18587
T = 27.15
(out)(err)
10tree810p.wcnf O = 21
T = 13.96
O = 21
T = 13.96
(out)(err)
O = 21328
T = 82.77
(out)(err)
10tree815p.wcnf O = 31
T = 9.67
O = 31
T = 9.67
(out)(err)
O = 26838
T = 60.56
(out)(err)
10tree820p.wcnf O = 42
T = 4.79
O = 42
T = 4.79
(out)(err)
O = 27047
T = 221.85
(out)(err)
10tree825p.wcnf O = 81
T = 272.63
O = 81
T = 272.63
(out)(err)
O = 30831
T = 81.74
(out)(err)
10tree830p.wcnf O = 63
T = 282.75
O = 63
T = 282.75
(out)(err)
O = 23901
T = 37.84
(out)(err)
10tree905p.wcnf O = 10
T = 28.29
O = 10
T = 28.29
(out)(err)
O = 23858
T = 209.18
(out)(err)
10tree905posib.wcnf O = 26604
T = 62.25
O = 10
T = 7.32
(out)(err)
O = 26604
T = 62.25
(out)(err)
10tree910p.wcnf O = 21
T = 17.81
O = 21
T = 17.81
(out)(err)
O = 23664
T = 234.55
(out)(err)
10tree915p.wcnf O = 31
T = 58.14
O = 31
T = 58.14
(out)(err)
O = 25975
T = 75.14
(out)(err)
10tree920p.wcnf O = 42
T = 12.46
O = 42
T = 12.46
(out)(err)
O = 27042
T = 65.75
(out)(err)
10tree925p.wcnf O = 52
T = 6.54
O = 52
T = 6.54
(out)(err)
O = 20085
T = 187.73
(out)(err)
10tree930p.wcnf O = 63
T = 69.59
O = 63
T = 69.59
(out)(err)
O = 28314
T = 26.73
(out)(err)
15tree1001p.wcnf O = 465
T = 3.96
O = 465
T = 3.96
(out)(err)
O = 900267
T = 32.70
(out)(err)
15tree1001posib.wcnf O = N/A
T = TO
O = 13
T = 189.10
(out)(err)
O = 1010969
T = 228.08
(out)(err)
15tree101p.wcnf O = 528
T = 36.27
O = 528
T = 36.27
(out)(err)
O = 1228078
T = 34.21
(out)(err)
15tree101posib.wcnf O = N/A
T = TO
O = 436
T = 82.95
(out)(err)
O = 984960
T = 33.47
(out)(err)
15tree201p.wcnf O = 439
T = 4.92
O = 439
T = 4.92
(out)(err)
O = 1
T = 259.86
(out)(err)
15tree201posib.wcnf O = N/A
T = TO
O = 13
T = 57.94
(out)(err)
O = 1020479
T = 37.32
(out)(err)
15tree301p.wcnf O = 621
T = 68.36
O = 621
T = 68.36
(out)(err)
O = 905724
T = 43.98
(out)(err)
15tree301posib.wcnf O = N/A
T = TO
O = 13
T = 237.51
(out)(err)
O = 874309
T = 38.09
(out)(err)
15tree401p.wcnf O = 617
T = 4.95
O = 617
T = 4.95
(out)(err)
O = 1110655
T = 81.86
(out)(err)
15tree401posib.wcnf O = N/A
T = TO
O = 13
T = 190.75
(out)(err)
O = 961744
T = 75.29
(out)(err)
15tree501p.wcnf O = 699
T = 3.39
O = 699
T = 3.39
(out)(err)
O = 1077879
T = 39.00
(out)(err)
15tree501posib.wcnf O = N/A
T = TO
O = 230
T = 187.05
(out)(err)
O = 954883
T = 75.27
(out)(err)
15tree601p.wcnf O = 359
T = 4.30
O = 359
T = 4.30
(out)(err)
O = 983607
T = 70.13
(out)(err)
15tree601posib.wcnf O = N/A
T = TO
O = 368
T = 259.68
(out)(err)
O = 954960
T = 160.53
(out)(err)
15tree701p.wcnf O = 597
T = 4.04
O = 597
T = 4.04
(out)(err)
O = 938488
T = 71.88
(out)(err)
15tree701posib.wcnf O = N/A
T = TO
O = 13
T = 168.20
(out)(err)
O = 1096959
T = 61.16
(out)(err)
15tree801p.wcnf O = 13
T = 227.35
O = 13
T = 227.35
(out)(err)
O = 956275
T = 34.48
(out)(err)
15tree801posib.wcnf O = N/A
T = TO
O = 13
T = 49.98
(out)(err)
O = 918014
T = 79.22
(out)(err)
15tree901p.wcnf O = 13
T = 255.08
O = 13
T = 255.08
(out)(err)
O = 893415
T = 50.34
(out)(err)
15tree901posib.wcnf O = N/A
T = TO
O = 13
T = 26.90
(out)(err)
O = 868835
T = 55.29
(out)(err)
normalized-s3-3-3-1pb.wcnf O = 36
T = 1.56
O = 36
T = 1.56
(out)(err)
O = 1121
T = 27.24
(out)(err)
normalized-s3-3-3-2pb.wcnf O = 36
T = 1.98
O = 36
T = 1.98
(out)(err)
O = 1358
T = 263.56
(out)(err)
normalized-s3-3-3-3pb.wcnf O = 36
T = 2.02
O = 36
T = 2.02
(out)(err)
O = 1477
T = 82.23
(out)(err)
normalized-s3-3-3-4pb.wcnf O = 36
T = 2.16
O = 36
T = 2.16
(out)(err)
O = 947
T = 67.95
(out)(err)
normalized-s3-3-3-5pb.wcnf O = 34
T = 2.35
O = 34
T = 2.35
(out)(err)
O = 755
T = 79.48
(out)(err)
normalized-s4-4-3-10pb.wcnf O = 70
T = 6.19
O = 70
T = 6.19
(out)(err)
O = 15209
T = 48.49
(out)(err)
normalized-s4-4-3-1pb.wcnf O = 62
T = 24.05
O = 62
T = 24.05
(out)(err)
O = 9473
T = 239.58
(out)(err)
normalized-s4-4-3-2pb.wcnf O = 64
T = 151.42
O = 64
T = 151.42
(out)(err)
O = 9791
T = 15.13
(out)(err)
normalized-s4-4-3-3pb.wcnf O = 62
T = 84.78
O = 62
T = 84.78
(out)(err)
O = 10447
T = 194.07
(out)(err)
normalized-s4-4-3-4pb.wcnf O = 60
T = 176.00
O = 60
T = 176.00
(out)(err)
O = 11201
T = 56.25
(out)(err)
normalized-s4-4-3-5pb.wcnf O = 62
T = 110.94
O = 62
T = 110.94
(out)(err)
O = 10871
T = 77.78
(out)(err)
normalized-s4-4-3-6pb.wcnf O = 66
T = 13.65
O = 66
T = 13.65
(out)(err)
O = 10684
T = 72.35
(out)(err)
normalized-s4-4-3-7pb.wcnf O = 64
T = 37.73
O = 64
T = 37.73
(out)(err)
O = 10833
T = 37.51
(out)(err)
normalized-s4-4-3-8pb.wcnf O = 38
T = 213.69
O = 38
T = 213.69
(out)(err)
O = 1347
T = 30.86
(out)(err)
normalized-s4-4-3-9pb.wcnf O = 68
T = 11.28
O = 68
T = 11.28
(out)(err)
O = 16869
T = 27.93
(out)(err)
1bpi_.2knt_.g.wcnf.t.wcnf O = 37
T = 64.82
O = 45
T = 114.03
(out)(err)
O = 37
T = 64.82
(out)(err)
1bpi_.5pti_.g.wcnf.t.wcnf O = N/A
T = TO
O = 48
T = 259.08
(out)(err)
O = N/A
T = TO
(out)(err)
1knt_.1bpi_.g.wcnf.t.wcnf O = 36
T = 25.45
O = 47
T = 258.37
(out)(err)
O = 36
T = 25.45
(out)(err)
1knt_.2knt_.g.wcnf.t.wcnf O = 16
T = 178.01
O = 17
T = 263.44
(out)(err)
O = 16
T = 178.01
(out)(err)
1knt_.5pti_.g.wcnf.t.wcnf O = 31
T = 68.74
O = 39
T = 294.85
(out)(err)
O = 31
T = 68.74
(out)(err)
1vii_.1cph_.g.wcnf.t.wcnf O = 7
T = 2.25
O = 7
T = 2.25
(out)(err)
O = 7
T = 7.93
(out)(err)
2knt_.5pti_.g.wcnf.t.wcnf O = 34
T = 81.06
O = 38
T = 275.46
(out)(err)
O = 34
T = 81.06
(out)(err)
3ebx_.1era_.g.wcnf.t.wcnf O = 34
T = 82.35
O = 46
T = 271.28
(out)(err)
O = 34
T = 82.35
(out)(err)
3ebx_.6ebx_.g.wcnf.t.wcnf O = 26
T = 51.64
O = 29
T = 268.15
(out)(err)
O = 26
T = 51.64
(out)(err)
6ebx_.1era_.g.wcnf.t.wcnf O = 30
T = 54.81
O = 31
T = 145.73
(out)(err)
O = 30
T = 54.81
(out)(err)
p1.wcnf.t.wcnf O = 39
T = 227.65
O = 46
T = 256.32
(out)(err)
O = 39
T = 227.65
(out)(err)
sandiaprotein.g.wcnf.t.wcnf O = 32
T = 107.77
O = 40
T = 146.98
(out)(err)
O = 32
T = 107.77
(out)(err)