Label | Meaning |
---|---|
S | Solution {OPTIMUM FOUND or OPT | UNSATISFIABLE or UNSAT | UNKNOWN | Not available or N/A} |
O | Best solution found |
T | CPU time (TO for Time Out) |
(out)(err) | Standard output and standard error for each solver |
Color | Meaning for Complete Solvers | Meaning for Incomplete Solvers |
---|---|---|
Text | Best solver column | Best solver column |
Text | Optimal solution with the best CPU time | Best solution with the best CPU time |
Text | Optimal solution and finished within the Time Out | Best solution without the best CPU time |
Text | Optimal solution and did not finish within the Time Out | Solution found but not the best |
Text | Time Out | Time Out |
Text | Buggy solution | Buggy 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) |