| 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 |
|---|---|---|---|
| cat_paths_60_100_0000.txt.wcnf | O = 68579 T = 3.28 |
O = 69035 T = 65.39 (out)(err) |
O = 68579 T = 3.28 (out)(err) |
| cat_paths_60_100_0001.txt.wcnf | O = 70359 T = 5.10 |
O = 70931 T = 74.53 (out)(err) |
O = 70359 T = 5.10 (out)(err) |
| cat_paths_60_100_0002.txt.wcnf | O = 63604 T = 4.44 |
O = 65288 T = 145.61 (out)(err) |
O = 63604 T = 4.44 (out)(err) |
| cat_paths_60_100_0003.txt.wcnf | O = 67524 T = 3.96 |
O = 68026 T = 37.06 (out)(err) |
O = 67524 T = 3.96 (out)(err) |
| cat_paths_60_100_0004.txt.wcnf | O = 66261 T = 3.68 |
O = 66564 T = 186.01 (out)(err) |
O = 66261 T = 3.68 (out)(err) |
| cat_paths_60_100_0005.txt.wcnf | O = 58665 T = 1.70 |
O = 58997 T = 273.83 (out)(err) |
O = 58665 T = 1.70 (out)(err) |
| cat_paths_60_100_0006.txt.wcnf | O = 62561 T = 3.05 |
O = 62561 T = 210.28 (out)(err) |
O = 62561 T = 3.05 (out)(err) |
| cat_paths_60_100_0007.txt.wcnf | O = 63697 T = 2.58 |
O = 63697 T = 4.45 (out)(err) |
O = 63697 T = 2.58 (out)(err) |
| cat_paths_60_110_0000.txt.wcnf | O = 67487 T = 3.68 |
O = 68350 T = 61.91 (out)(err) |
O = 67487 T = 3.68 (out)(err) |
| cat_paths_60_110_0001.txt.wcnf | O = 57187 T = 4.73 |
O = 58329 T = 67.22 (out)(err) |
O = 57187 T = 4.73 (out)(err) |
| cat_paths_60_110_0002.txt.wcnf | O = 68460 T = 3.19 |
O = 69319 T = 135.05 (out)(err) |
O = 68460 T = 3.19 (out)(err) |
| cat_paths_60_110_0003.txt.wcnf | O = 72855 T = 1.01 |
O = 75295 T = 14.32 (out)(err) |
O = 72855 T = 1.01 (out)(err) |
| cat_paths_60_110_0004.txt.wcnf | O = 56823 T = 21.68 |
O = 57525 T = 35.29 (out)(err) |
O = 56823 T = 21.68 (out)(err) |
| cat_paths_60_110_0005.txt.wcnf | O = 78796 T = 4.29 |
O = 78796 T = 105.35 (out)(err) |
O = 78796 T = 4.29 (out)(err) |
| cat_paths_60_110_0006.txt.wcnf | O = 67797 T = 4.81 |
O = 69976 T = 281.91 (out)(err) |
O = 67797 T = 4.81 (out)(err) |
| cat_paths_60_110_0007.txt.wcnf | O = 60477 T = 4.83 |
O = 61234 T = 124.72 (out)(err) |
O = 60477 T = 4.83 (out)(err) |
| cat_paths_60_120_0000.txt.wcnf | O = 77836 T = 86.02 |
O = 79020 T = 279.18 (out)(err) |
O = 77836 T = 86.02 (out)(err) |
| cat_paths_60_120_0001.txt.wcnf | O = 66708 T = 5.33 |
O = 67408 T = 155.72 (out)(err) |
O = 66708 T = 5.33 (out)(err) |
| cat_paths_60_120_0002.txt.wcnf | O = 73372 T = 5.25 |
O = 74273 T = 20.69 (out)(err) |
O = 73372 T = 5.25 (out)(err) |
| cat_paths_60_120_0003.txt.wcnf | O = 74335 T = 5.79 |
O = 75776 T = 45.92 (out)(err) |
O = 74335 T = 5.79 (out)(err) |
| cat_paths_60_120_0004.txt.wcnf | O = 73582 T = 5.99 |
O = 75392 T = 4.13 (out)(err) |
O = 73582 T = 5.99 (out)(err) |
| cat_paths_60_120_0005.txt.wcnf | O = 79014 T = 4.91 |
O = 79294 T = 156.72 (out)(err) |
O = 79014 T = 4.91 (out)(err) |
| cat_paths_60_120_0006.txt.wcnf | O = 69173 T = 4.69 |
O = 70668 T = 80.43 (out)(err) |
O = 69173 T = 4.69 (out)(err) |
| cat_paths_60_120_0007.txt.wcnf | O = 73799 T = 5.54 |
O = 74757 T = 279.12 (out)(err) |
O = 73799 T = 5.54 (out)(err) |
| cat_paths_60_130_0000.txt.wcnf | O = 78708 T = 5.23 |
O = 80594 T = 256.51 (out)(err) |
O = 78708 T = 5.23 (out)(err) |
| cat_paths_60_130_0001.txt.wcnf | O = 80743 T = 4.97 |
O = 80951 T = 217.49 (out)(err) |
O = 80743 T = 4.97 (out)(err) |
| cat_paths_60_130_0002.txt.wcnf | O = 71385 T = 5.54 |
O = 71737 T = 231.52 (out)(err) |
O = 71385 T = 5.54 (out)(err) |
| cat_paths_60_130_0003.txt.wcnf | O = 86981 T = 5.62 |
O = 88847 T = 61.71 (out)(err) |
O = 86981 T = 5.62 (out)(err) |
| cat_paths_60_130_0004.txt.wcnf | O = 92310 T = 28.12 |
O = 93533 T = 17.22 (out)(err) |
O = 92310 T = 28.12 (out)(err) |
| cat_paths_60_130_0005.txt.wcnf | O = 74325 T = 4.23 |
O = 76445 T = 265.37 (out)(err) |
O = 74325 T = 4.23 (out)(err) |
| cat_paths_60_130_0006.txt.wcnf | O = 77394 T = 67.61 |
O = 78275 T = 224.81 (out)(err) |
O = 77394 T = 67.61 (out)(err) |
| cat_paths_60_130_0007.txt.wcnf | O = 73518 T = 4.79 |
O = 74742 T = 130.32 (out)(err) |
O = 73518 T = 4.79 (out)(err) |
| cat_paths_60_140_0000.txt.wcnf | O = 98394 T = 6.25 |
O = 100010 T = 87.76 (out)(err) |
O = 98394 T = 6.25 (out)(err) |
| cat_paths_60_140_0001.txt.wcnf | O = 97718 T = 14.98 |
O = 100080 T = 5.87 (out)(err) |
O = 97718 T = 14.98 (out)(err) |
| cat_paths_60_140_0002.txt.wcnf | O = 92818 T = 107.14 |
O = 94415 T = 46.96 (out)(err) |
O = 92818 T = 107.14 (out)(err) |
| cat_paths_60_140_0003.txt.wcnf | O = 92696 T = 5.67 |
O = 95255 T = 277.09 (out)(err) |
O = 92696 T = 5.67 (out)(err) |
| cat_paths_60_140_0004.txt.wcnf | O = 96711 T = 5.90 |
O = 98823 T = 129.89 (out)(err) |
O = 96711 T = 5.90 (out)(err) |
| cat_paths_60_140_0005.txt.wcnf | O = 102646 T = 5.04 |
O = 103212 T = 278.65 (out)(err) |
O = 102646 T = 5.04 (out)(err) |
| cat_paths_60_140_0006.txt.wcnf | O = 97369 T = 5.04 |
O = 98946 T = 7.15 (out)(err) |
O = 97369 T = 5.04 (out)(err) |
| cat_paths_60_140_0007.txt.wcnf | O = 85215 T = 5.24 |
O = 86383 T = 268.45 (out)(err) |
O = 85215 T = 5.24 (out)(err) |
| cat_paths_60_150_0000.txt.wcnf | O = 82179 T = 5.07 |
O = 84685 T = 133.00 (out)(err) |
O = 82179 T = 5.07 (out)(err) |
| cat_paths_60_150_0001.txt.wcnf | O = 92304 T = 198.77 |
O = 93434 T = 275.95 (out)(err) |
O = 92304 T = 198.77 (out)(err) |
| cat_paths_60_150_0002.txt.wcnf | O = 101547 T = 6.11 |
O = 102625 T = 106.78 (out)(err) |
O = 101547 T = 6.11 (out)(err) |
| cat_paths_60_150_0003.txt.wcnf | O = 106294 T = 6.34 |
O = 107813 T = 15.75 (out)(err) |
O = 106294 T = 6.34 (out)(err) |
| cat_paths_60_150_0004.txt.wcnf | O = 93389 T = 3.43 |
O = 95774 T = 2.00 (out)(err) |
O = 93389 T = 3.43 (out)(err) |
| cat_paths_60_150_0005.txt.wcnf | O = 112036 T = 6.97 |
O = 114945 T = 216.90 (out)(err) |
O = 112036 T = 6.97 (out)(err) |
| cat_paths_60_150_0006.txt.wcnf | O = 86848 T = 11.55 |
O = 89438 T = 114.73 (out)(err) |
O = 86848 T = 11.55 (out)(err) |
| cat_paths_60_150_0007.txt.wcnf | O = 110670 T = 141.62 |
O = 112006 T = 5.86 (out)(err) |
O = 110670 T = 141.62 (out)(err) |
| cat_paths_60_160_0000.txt.wcnf | O = 104199 T = 2.30 |
O = 108215 T = 49.69 (out)(err) |
O = 104199 T = 2.30 (out)(err) |
| cat_paths_60_160_0001.txt.wcnf | O = 99297 T = 5.79 |
O = 102453 T = 283.77 (out)(err) |
O = 99297 T = 5.79 (out)(err) |
| cat_paths_60_160_0002.txt.wcnf | O = 102352 T = 139.17 |
O = 104612 T = 4.86 (out)(err) |
O = 102352 T = 139.17 (out)(err) |
| cat_paths_60_160_0003.txt.wcnf | O = 107262 T = 6.19 |
O = 109195 T = 106.52 (out)(err) |
O = 107262 T = 6.19 (out)(err) |
| cat_paths_60_160_0004.txt.wcnf | O = 102901 T = 7.18 |
O = 104526 T = 1.44 (out)(err) |
O = 102901 T = 7.18 (out)(err) |
| cat_paths_60_160_0005.txt.wcnf | O = 121967 T = 5.33 |
O = 125374 T = 205.51 (out)(err) |
O = 121967 T = 5.33 (out)(err) |
| cat_paths_60_160_0006.txt.wcnf | O = 95039 T = 12.60 |
O = 96008 T = 4.55 (out)(err) |
O = 95039 T = 12.60 (out)(err) |
| cat_paths_60_160_0007.txt.wcnf | O = 103455 T = 15.29 |
O = 105119 T = 69.59 (out)(err) |
O = 103455 T = 15.29 (out)(err) |
| cat_paths_60_170_0000.txt.wcnf | O = 122170 T = 54.40 |
O = 123805 T = 95.61 (out)(err) |
O = 122170 T = 54.40 (out)(err) |
| cat_paths_60_170_0003.txt.wcnf | O = 122748 T = 70.83 |
O = 125099 T = 223.37 (out)(err) |
O = 122748 T = 70.83 (out)(err) |
| cat_paths_60_170_0004.txt.wcnf | O = 99105 T = 22.27 |
O = 100439 T = 9.46 (out)(err) |
O = 99105 T = 22.27 (out)(err) |
| cat_paths_60_170_0005.txt.wcnf | O = 114608 T = 121.57 |
O = 115953 T = 4.99 (out)(err) |
O = 114608 T = 121.57 (out)(err) |
| cat_paths_60_170_0006.txt.wcnf | O = 101774 T = 7.38 |
O = 103802 T = 4.77 (out)(err) |
O = 101774 T = 7.38 (out)(err) |
| cat_paths_60_170_0007.txt.wcnf | O = 94165 T = 7.74 |
O = 96859 T = 104.01 (out)(err) |
O = 94165 T = 7.74 (out)(err) |
| cat_paths_60_70_0000.txt.wcnf | O = 48609 T = 2.56 |
O = 48609 T = 9.40 (out)(err) |
O = 48609 T = 2.56 (out)(err) |
| cat_paths_60_70_0001.txt.wcnf | O = 40870 T = 1.95 |
O = 40870 T = 147.87 (out)(err) |
O = 40870 T = 1.95 (out)(err) |
| cat_paths_60_70_0002.txt.wcnf | O = 38495 T = 2.35 |
O = 38495 T = 3.81 (out)(err) |
O = 38495 T = 2.35 (out)(err) |
| cat_paths_60_70_0003.txt.wcnf | O = 44555 T = 2.41 |
O = 44555 T = 3.51 (out)(err) |
O = 44555 T = 2.41 (out)(err) |
| cat_paths_60_70_0004.txt.wcnf | O = 33405 T = 2.78 |
O = 33405 T = 16.43 (out)(err) |
O = 33405 T = 2.78 (out)(err) |
| cat_paths_60_70_0005.txt.wcnf | O = 42222 T = 1.99 |
O = 42222 T = 15.22 (out)(err) |
O = 42222 T = 1.99 (out)(err) |
| cat_paths_60_70_0006.txt.wcnf | O = 44103 T = 2.36 |
O = 44103 T = 15.64 (out)(err) |
O = 44103 T = 2.36 (out)(err) |
| cat_paths_60_70_0007.txt.wcnf | O = 43384 T = 3.67 |
O = 43384 T = 27.86 (out)(err) |
O = 43384 T = 3.67 (out)(err) |
| cat_paths_60_80_0000.txt.wcnf | O = 46604 T = 2.07 |
O = 46604 T = 25.79 (out)(err) |
O = 46604 T = 2.07 (out)(err) |
| cat_paths_60_80_0001.txt.wcnf | O = 43891 T = 2.17 |
O = 43891 T = 53.74 (out)(err) |
O = 43891 T = 2.17 (out)(err) |
| cat_paths_60_80_0002.txt.wcnf | O = 45128 T = 3.34 |
O = 45128 T = 45.73 (out)(err) |
O = 45128 T = 3.34 (out)(err) |
| cat_paths_60_80_0003.txt.wcnf | O = 51870 T = 2.65 |
O = 51870 T = 177.27 (out)(err) |
O = 51870 T = 2.65 (out)(err) |
| cat_paths_60_80_0004.txt.wcnf | O = 46183 T = 3.57 |
O = 46183 T = 13.02 (out)(err) |
O = 46183 T = 3.57 (out)(err) |
| cat_paths_60_80_0005.txt.wcnf | O = 57352 T = 0.65 |
O = 57352 T = 35.28 (out)(err) |
O = 57352 T = 0.65 (out)(err) |
| cat_paths_60_80_0006.txt.wcnf | O = 54851 T = 3.14 |
O = 54851 T = 116.65 (out)(err) |
O = 54851 T = 3.14 (out)(err) |
| cat_paths_60_80_0007.txt.wcnf | O = 53183 T = 2.87 |
O = 53183 T = 45.17 (out)(err) |
O = 53183 T = 2.87 (out)(err) |
| cat_paths_60_90_0000.txt.wcnf | O = 51257 T = 4.05 |
O = 52350 T = 253.62 (out)(err) |
O = 51257 T = 4.05 (out)(err) |
| cat_paths_60_90_0001.txt.wcnf | O = 67562 T = 3.59 |
O = 67576 T = 5.01 (out)(err) |
O = 67562 T = 3.59 (out)(err) |
| cat_paths_60_90_0002.txt.wcnf | O = 66497 T = 4.42 |
O = 66497 T = 53.59 (out)(err) |
O = 66497 T = 4.42 (out)(err) |
| cat_paths_60_90_0003.txt.wcnf | O = 46882 T = 4.25 |
O = 47638 T = 31.58 (out)(err) |
O = 46882 T = 4.25 (out)(err) |
| cat_paths_60_90_0004.txt.wcnf | O = 56174 T = 4.77 |
O = 56830 T = 195.68 (out)(err) |
O = 56174 T = 4.77 (out)(err) |
| cat_paths_60_90_0005.txt.wcnf | O = 63761 T = 4.55 |
O = 64517 T = 189.70 (out)(err) |
O = 63761 T = 4.55 (out)(err) |
| cat_paths_60_90_0006.txt.wcnf | O = 47852 T = 2.63 |
O = 47852 T = 189.24 (out)(err) |
O = 47852 T = 2.63 (out)(err) |
| cat_paths_60_90_0007.txt.wcnf | O = 58739 T = 3.95 |
O = 59595 T = 131.16 (out)(err) |
O = 58739 T = 3.95 (out)(err) |
| cat_sched_60_100_0000.txt.wcnf | O = 114652 T = 5.20 |
O = 114652 T = 5.20 (out)(err) |
O = 114652 T = 6.66 (out)(err) |
| cat_sched_60_100_0001.txt.wcnf | O = 93703 T = 3.27 |
O = 93703 T = 3.27 (out)(err) |
O = 93703 T = 5.48 (out)(err) |
| cat_sched_60_100_0002.txt.wcnf | O = 132213 T = 4.08 |
O = 132213 T = 4.95 (out)(err) |
O = 132213 T = 4.08 (out)(err) |
| cat_sched_60_100_0003.txt.wcnf | O = 77536 T = 1.19 |
O = 77536 T = 1.19 (out)(err) |
O = 77536 T = 6.47 (out)(err) |
| cat_sched_60_100_0004.txt.wcnf | O = 60696 T = 2.68 |
O = 60696 T = 2.68 (out)(err) |
O = 60696 T = 5.32 (out)(err) |
| cat_sched_60_100_0005.txt.wcnf | O = 56308 T = 1.88 |
O = 56308 T = 1.88 (out)(err) |
O = 56308 T = 4.09 (out)(err) |
| cat_sched_60_110_0000.txt.wcnf | O = 82948 T = 3.01 |
O = 82948 T = 3.01 (out)(err) |
O = 82948 T = 6.99 (out)(err) |
| cat_sched_60_110_0001.txt.wcnf | O = 73693 T = 2.08 |
O = 73693 T = 2.08 (out)(err) |
O = 73693 T = 6.39 (out)(err) |
| cat_sched_60_110_0002.txt.wcnf | O = 80642 T = 4.59 |
O = 80642 T = 4.59 (out)(err) |
O = 80642 T = 5.47 (out)(err) |
| cat_sched_60_110_0003.txt.wcnf | O = 96555 T = 3.24 |
O = 96555 T = 3.24 (out)(err) |
O = 96555 T = 6.13 (out)(err) |
| cat_sched_60_110_0004.txt.wcnf | O = 79464 T = 4.18 |
O = 79464 T = 4.18 (out)(err) |
O = 79464 T = 5.25 (out)(err) |
| cat_sched_60_110_0005.txt.wcnf | O = 75228 T = 4.29 |
O = 75228 T = 4.29 (out)(err) |
O = 75228 T = 5.55 (out)(err) |
| cat_sched_60_120_0000.txt.wcnf | O = 94786 T = 5.24 |
O = 94786 T = 5.24 (out)(err) |
O = 94786 T = 6.90 (out)(err) |
| cat_sched_60_120_0001.txt.wcnf | O = 113216 T = 4.42 |
O = 113216 T = 4.42 (out)(err) |
O = 113216 T = 8.41 (out)(err) |
| cat_sched_60_120_0002.txt.wcnf | O = 78795 T = 4.21 |
O = 78795 T = 8.54 (out)(err) |
O = 78795 T = 4.21 (out)(err) |
| cat_sched_60_120_0003.txt.wcnf | O = 101400 T = 4.67 |
O = 101400 T = 4.67 (out)(err) |
O = 101400 T = 5.46 (out)(err) |
| cat_sched_60_120_0004.txt.wcnf | O = 82385 T = 2.73 |
O = 82385 T = 2.73 (out)(err) |
O = 82385 T = 6.52 (out)(err) |
| cat_sched_60_120_0005.txt.wcnf | O = 170793 T = 2.09 |
O = 170793 T = 2.09 (out)(err) |
O = 170793 T = 6.40 (out)(err) |
| cat_sched_60_130_0000.txt.wcnf | O = 108599 T = 5.71 |
O = 108599 T = 5.71 (out)(err) |
O = 108599 T = 7.73 (out)(err) |
| cat_sched_60_130_0001.txt.wcnf | O = 71588 T = 1.89 |
O = 71588 T = 1.89 (out)(err) |
O = 71588 T = 7.31 (out)(err) |
| cat_sched_60_130_0002.txt.wcnf | O = 81955 T = 7.40 |
O = 81955 T = 33.49 (out)(err) |
O = 81955 T = 7.40 (out)(err) |
| cat_sched_60_130_0003.txt.wcnf | O = 161231 T = 4.43 |
O = 161231 T = 4.43 (out)(err) |
O = 161231 T = 4.95 (out)(err) |
| cat_sched_60_130_0004.txt.wcnf | O = 81678 T = 3.69 |
O = 81678 T = 3.69 (out)(err) |
O = 81678 T = 5.98 (out)(err) |
| cat_sched_60_130_0005.txt.wcnf | O = 137429 T = 0.73 |
O = 137429 T = 3.56 (out)(err) |
O = 137429 T = 0.73 (out)(err) |
| cat_sched_60_140_0000.txt.wcnf | O = 114104 T = 2.81 |
O = 114104 T = 2.81 (out)(err) |
O = 114104 T = 7.41 (out)(err) |
| cat_sched_60_140_0001.txt.wcnf | O = 122958 T = 2.20 |
O = 122958 T = 2.20 (out)(err) |
O = 122958 T = 7.01 (out)(err) |
| cat_sched_60_140_0002.txt.wcnf | O = 61273 T = 4.04 |
O = 61273 T = 4.04 (out)(err) |
O = 61273 T = 7.33 (out)(err) |
| cat_sched_60_140_0003.txt.wcnf | O = 150048 T = 5.41 |
O = 150048 T = 5.41 (out)(err) |
O = 150048 T = 6.95 (out)(err) |
| cat_sched_60_140_0004.txt.wcnf | O = 86193 T = 2.41 |
O = 86193 T = 2.41 (out)(err) |
O = 86193 T = 7.63 (out)(err) |
| cat_sched_60_140_0005.txt.wcnf | O = 127199 T = 3.94 |
O = 127199 T = 3.94 (out)(err) |
O = 127199 T = 6.80 (out)(err) |
| cat_sched_60_150_0000.txt.wcnf | O = 137542 T = 2.72 |
O = 137542 T = 2.72 (out)(err) |
O = 137542 T = 6.45 (out)(err) |
| cat_sched_60_150_0001.txt.wcnf | O = 87430 T = 7.96 |
O = 87430 T = 171.03 (out)(err) |
O = 87430 T = 7.96 (out)(err) |
| cat_sched_60_150_0002.txt.wcnf | O = 50886 T = 1.16 |
O = 50886 T = 1.16 (out)(err) |
O = 50886 T = 6.15 (out)(err) |
| cat_sched_60_150_0003.txt.wcnf | O = 85895 T = 4.67 |
O = 85895 T = 4.67 (out)(err) |
O = 85895 T = 6.20 (out)(err) |
| cat_sched_60_150_0004.txt.wcnf | O = 107684 T = 3.52 |
O = 107684 T = 3.52 (out)(err) |
O = 107684 T = 6.91 (out)(err) |
| cat_sched_60_150_0005.txt.wcnf | O = 153808 T = 2.02 |
O = 153808 T = 2.02 (out)(err) |
O = 153808 T = 8.85 (out)(err) |
| cat_sched_60_160_0000.txt.wcnf | O = 42672 T = 3.94 |
O = 42672 T = 3.94 (out)(err) |
O = 42672 T = 6.54 (out)(err) |
| cat_sched_60_160_0001.txt.wcnf | O = 72012 T = 1.61 |
O = 72012 T = 1.61 (out)(err) |
O = 72012 T = 4.39 (out)(err) |
| cat_sched_60_160_0002.txt.wcnf | O = 173386 T = 7.71 |
O = 173830 T = 41.05 (out)(err) |
O = 173386 T = 7.71 (out)(err) |
| cat_sched_60_160_0003.txt.wcnf | O = 118883 T = 3.59 |
O = 118883 T = 57.36 (out)(err) |
O = 118883 T = 3.59 (out)(err) |
| cat_sched_60_160_0004.txt.wcnf | O = 116193 T = 1.70 |
O = 116193 T = 1.70 (out)(err) |
O = 116193 T = 7.98 (out)(err) |
| cat_sched_60_160_0005.txt.wcnf | O = 117991 T = 1.64 |
O = 117991 T = 1.64 (out)(err) |
O = 117991 T = 6.06 (out)(err) |
| cat_sched_60_170_0000.txt.wcnf | O = 128737 T = 4.45 |
O = 128737 T = 4.45 (out)(err) |
O = 128737 T = 6.24 (out)(err) |
| cat_sched_60_170_0001.txt.wcnf | O = 62218 T = 9.90 |
O = 62511 T = 206.27 (out)(err) |
O = 62218 T = 9.90 (out)(err) |
| cat_sched_60_170_0002.txt.wcnf | O = 64664 T = 2.33 |
O = 64664 T = 2.33 (out)(err) |
O = 64664 T = 7.73 (out)(err) |
| cat_sched_60_170_0003.txt.wcnf | O = 169415 T = 5.00 |
O = 169415 T = 5.00 (out)(err) |
O = 169415 T = 10.56 (out)(err) |
| cat_sched_60_170_0004.txt.wcnf | O = 132643 T = 7.86 |
O = 132643 T = 31.50 (out)(err) |
O = 132643 T = 7.86 (out)(err) |
| cat_sched_60_170_0005.txt.wcnf | O = 206173 T = 3.66 |
O = 206173 T = 3.66 (out)(err) |
O = 206173 T = 9.44 (out)(err) |
| cat_sched_60_180_0000.txt.wcnf | O = 112247 T = 8.69 |
O = 112677 T = 1.24 (out)(err) |
O = 112247 T = 8.69 (out)(err) |
| cat_sched_60_180_0001.txt.wcnf | O = 154599 T = 6.63 |
O = 154599 T = 45.05 (out)(err) |
O = 154599 T = 6.63 (out)(err) |
| cat_sched_60_180_0002.txt.wcnf | O = 95338 T = 4.37 |
O = 95338 T = 4.37 (out)(err) |
O = 95338 T = 9.92 (out)(err) |
| cat_sched_60_180_0003.txt.wcnf | O = 104416 T = 3.01 |
O = 104416 T = 3.01 (out)(err) |
O = 104416 T = 8.88 (out)(err) |
| cat_sched_60_180_0004.txt.wcnf | O = 122528 T = 9.01 |
O = 122528 T = 39.48 (out)(err) |
O = 122528 T = 9.01 (out)(err) |
| cat_sched_60_180_0005.txt.wcnf | O = 156974 T = 1.44 |
O = 156974 T = 1.44 (out)(err) |
O = 156974 T = 9.72 (out)(err) |
| cat_sched_60_190_0000.txt.wcnf | O = 152878 T = 9.54 |
O = 152909 T = 150.95 (out)(err) |
O = 152878 T = 9.54 (out)(err) |
| cat_sched_60_190_0001.txt.wcnf | O = 71645 T = 10.99 |
O = 71726 T = 137.24 (out)(err) |
O = 71645 T = 10.99 (out)(err) |
| cat_sched_60_190_0002.txt.wcnf | O = 90463 T = 10.24 |
O = 90837 T = 3.51 (out)(err) |
O = 90463 T = 10.24 (out)(err) |
| cat_sched_60_190_0003.txt.wcnf | O = 87812 T = 1.62 |
O = 87812 T = 1.62 (out)(err) |
O = 87812 T = 7.71 (out)(err) |
| cat_sched_60_190_0004.txt.wcnf | O = 133679 T = 5.14 |
O = 133679 T = 5.14 (out)(err) |
O = 133679 T = 10.32 (out)(err) |
| cat_sched_60_190_0005.txt.wcnf | O = 163308 T = 8.62 |
O = 163557 T = 234.93 (out)(err) |
O = 163308 T = 8.62 (out)(err) |
| cat_sched_60_200_0000.txt.wcnf | O = 242832 T = 9.87 |
O = 242832 T = 36.82 (out)(err) |
O = 242832 T = 9.87 (out)(err) |
| cat_sched_60_200_0001.txt.wcnf | O = 46823 T = 1.53 |
O = 46823 T = 1.53 (out)(err) |
O = 46823 T = 9.13 (out)(err) |
| cat_sched_60_200_0002.txt.wcnf | O = 145851 T = 9.20 |
O = 145851 T = 22.96 (out)(err) |
O = 145851 T = 9.20 (out)(err) |
| cat_sched_60_200_0003.txt.wcnf | O = 187411 T = 9.13 |
O = 187411 T = 12.46 (out)(err) |
O = 187411 T = 9.13 (out)(err) |
| cat_sched_60_200_0004.txt.wcnf | O = 146947 T = 11.18 |
O = 147088 T = 143.67 (out)(err) |
O = 146947 T = 11.18 (out)(err) |
| cat_sched_60_200_0005.txt.wcnf | O = 134394 T = 4.36 |
O = 134394 T = 4.36 (out)(err) |
O = 134394 T = 7.40 (out)(err) |
| cat_sched_60_70_0000.txt.wcnf | O = 35750 T = 1.82 |
O = 35750 T = 1.82 (out)(err) |
O = 35750 T = 4.29 (out)(err) |
| cat_sched_60_70_0001.txt.wcnf | O = 83682 T = 2.28 |
O = 83682 T = 2.28 (out)(err) |
O = 83682 T = 3.98 (out)(err) |
| cat_sched_60_70_0002.txt.wcnf | O = 39227 T = 4.22 |
O = 39227 T = 4.22 (out)(err) |
O = 39227 T = 5.63 (out)(err) |
| cat_sched_60_70_0003.txt.wcnf | O = 61169 T = 1.71 |
O = 61169 T = 1.71 (out)(err) |
O = 61169 T = 3.72 (out)(err) |
| cat_sched_60_70_0004.txt.wcnf | O = 40136 T = 2.50 |
O = 40136 T = 2.50 (out)(err) |
O = 40136 T = 4.21 (out)(err) |
| cat_sched_60_70_0005.txt.wcnf | O = 105072 T = 2.43 |
O = 105072 T = 2.43 (out)(err) |
O = 105072 T = 4.11 (out)(err) |
| cat_sched_60_80_0000.txt.wcnf | O = 37448 T = 2.56 |
O = 37448 T = 2.56 (out)(err) |
O = 37448 T = 4.84 (out)(err) |
| cat_sched_60_80_0001.txt.wcnf | O = 22634 T = 1.07 |
O = 22634 T = 1.07 (out)(err) |
O = 22634 T = 3.89 (out)(err) |
| cat_sched_60_80_0002.txt.wcnf | O = 78029 T = 1.69 |
O = 78029 T = 1.69 (out)(err) |
O = 78029 T = 5.75 (out)(err) |
| cat_sched_60_80_0003.txt.wcnf | O = 40212 T = 4.25 |
O = 40212 T = 4.25 (out)(err) |
O = 40212 T = 5.15 (out)(err) |
| cat_sched_60_80_0004.txt.wcnf | O = 10390 T = 3.17 |
O = 10390 T = 3.17 (out)(err) |
O = 10390 T = 3.71 (out)(err) |
| cat_sched_60_80_0005.txt.wcnf | O = 34950 T = 1.67 |
O = 34950 T = 1.67 (out)(err) |
O = 34950 T = 4.07 (out)(err) |
| cat_sched_60_90_0000.txt.wcnf | O = 96833 T = 0.42 |
O = 96833 T = 1.24 (out)(err) |
O = 96833 T = 0.42 (out)(err) |
| cat_sched_60_90_0001.txt.wcnf | O = 82847 T = 2.58 |
O = 82847 T = 2.58 (out)(err) |
O = 82847 T = 4.68 (out)(err) |
| cat_sched_60_90_0002.txt.wcnf | O = 66464 T = 2.54 |
O = 66464 T = 2.54 (out)(err) |
O = 66464 T = 4.31 (out)(err) |
| cat_sched_60_90_0003.txt.wcnf | O = 37704 T = 3.16 |
O = 37704 T = 3.16 (out)(err) |
O = 37704 T = 4.70 (out)(err) |
| cat_sched_60_90_0004.txt.wcnf | O = 82537 T = 2.20 |
O = 82537 T = 2.20 (out)(err) |
O = 82537 T = 4.40 (out)(err) |
| cat_sched_60_90_0005.txt.wcnf | O = 49851 T = 3.80 |
O = 49851 T = 3.80 (out)(err) |
O = 49851 T = 4.33 (out)(err) |
| bwt3cc.wcsp.wcnf | O = 177 T = 0.43 |
O = 177 T = 0.43 (out)(err) |
O = 177 T = 17.96 (out)(err) |
| bwt4bc.wcsp.wcnf | O = 355 T = 1.28 |
O = 355 T = 1.28 (out)(err) |
O = 17481 T = 209.05 (out)(err) |
| bwt4c.wcsp.wcnf | O = 600 T = 1.02 |
O = 600 T = 1.02 (out)(err) |
O = 33903 T = 35.78 (out)(err) |
| bwt5ac.wcsp.wcnf | O = 800 T = 2.51 |
O = 800 T = 2.51 (out)(err) |
O = 252709 T = 137.21 (out)(err) |
| bwt5c.wcsp.wcnf | O = 800 T = 1.87 |
O = 800 T = 1.87 (out)(err) |
O = 280685 T = 23.22 (out)(err) |
| bwt5cc.wcsp.wcnf | O = 866 T = 2.17 |
O = 866 T = 2.17 (out)(err) |
O = 243693 T = 25.98 (out)(err) |
| bwt6.wcsp.wcnf | O = 650 T = 2.54 |
O = 650 T = 2.54 (out)(err) |
O = 681615 T = 17.19 (out)(err) |
| bwt7.wcsp.wcnf | O = 780 T = 2.68 |
O = 780 T = 2.68 (out)(err) |
O = 1594040 T = 52.70 (out)(err) |
| depot01ac.wcsp.wcnf | O = 1720 T = 0.42 |
O = 1720 T = 0.42 (out)(err) |
O = 2270 T = 52.71 (out)(err) |
| depot01bc.wcsp.wcnf | O = 1965 T = 0.48 |
O = 1965 T = 0.48 (out)(err) |
O = 15046 T = 104.11 (out)(err) |
| depot01c.wcsp.wcnf | O = 1720 T = 0.45 |
O = 1720 T = 0.45 (out)(err) |
O = 14311 T = 103.04 (out)(err) |
| depot01cc.wcsp.wcnf | O = 2142 T = 0.45 |
O = 2142 T = 0.45 (out)(err) |
O = 10934 T = 96.73 (out)(err) |
| driverlog01c.wcsp.wcnf | O = 1145 T = 0.44 |
O = 1145 T = 0.44 (out)(err) |
O = 1175 T = 67.50 (out)(err) |
| driverlog01cc.wcsp.wcnf | O = 1117 T = 0.42 |
O = 1117 T = 0.42 (out)(err) |
O = 1117 T = 92.00 (out)(err) |
| driverlog02bc.wcsp.wcnf | O = 2085 T = 4.90 |
O = 2085 T = 4.90 (out)(err) |
O = 439601 T = 41.15 (out)(err) |
| driverlog02c.wcsp.wcnf | O = 2010 T = 5.77 |
O = 2010 T = 5.77 (out)(err) |
O = 411407 T = 213.01 (out)(err) |
| driverlog02cc.wcsp.wcnf | O = 2428 T = 3.36 |
O = 2428 T = 3.36 (out)(err) |
O = 556070 T = 73.77 (out)(err) |
| driverlog04ac.wcsp.wcnf | O = 1790 T = 3.99 |
O = 1790 T = 3.99 (out)(err) |
O = 426544 T = 140.35 (out)(err) |
| driverlog04bc.wcsp.wcnf | O = 1921 T = 3.59 |
O = 1921 T = 3.59 (out)(err) |
O = 521723 T = 182.68 (out)(err) |
| driverlog04cc.wcsp.wcnf | O = 2932 T = 3.68 |
O = 2932 T = 3.68 (out)(err) |
O = 674126 T = 222.17 (out)(err) |
| driverlog05ac.wcsp.wcnf | O = 1350 T = 5.05 |
O = 1350 T = 5.05 (out)(err) |
O = 594984 T = 191.78 (out)(err) |
| driverlog05bc.wcsp.wcnf | O = 1344 T = 4.50 |
O = 1344 T = 4.50 (out)(err) |
O = 632754 T = 156.11 (out)(err) |
| driverlog05c.wcsp.wcnf | O = 1350 T = 3.97 |
O = 1350 T = 3.97 (out)(err) |
O = 530168 T = 86.09 (out)(err) |
| driverlog08ac.wcsp.wcnf | O = 2220 T = 3.73 |
O = 2220 T = 3.73 (out)(err) |
O = 835967 T = 60.14 (out)(err) |
| driverlog08c.wcsp.wcnf | O = 2220 T = 4.35 |
O = 2220 T = 4.35 (out)(err) |
O = 766126 T = 55.90 (out)(err) |
| driverlog08cc.wcsp.wcnf | O = 4052 T = 4.24 |
O = 4052 T = 4.24 (out)(err) |
O = 1529641 T = 60.73 (out)(err) |
| driverlog09.wcsp.wcnf | O = 960 T = 4.29 |
O = 960 T = 4.29 (out)(err) |
O = 575300 T = 50.95 (out)(err) |
| driverlogs03.wcsp.wcnf | O = 1225 T = 2.85 |
O = 1225 T = 2.85 (out)(err) |
O = 216305 T = 178.74 (out)(err) |
| driverlogs06.wcsp.wcnf | O = 1055 T = 2.78 |
O = 1055 T = 2.78 (out)(err) |
O = 301497 T = 153.59 (out)(err) |
| logistics01bc.wcsp.wcnf | O = 8035 T = 1.45 |
O = 8035 T = 1.45 (out)(err) |
O = 262785 T = 172.79 (out)(err) |
| logistics01c.wcsp.wcnf | O = 8865 T = 1.41 |
O = 8865 T = 1.41 (out)(err) |
O = 354370 T = 161.08 (out)(err) |
| logistics01cc.wcsp.wcnf | O = 4282 T = 1.77 |
O = 4282 T = 1.77 (out)(err) |
O = 167960 T = 174.81 (out)(err) |
| mprime01ac.wcsp.wcnf | O = 250 T = 2.38 |
O = 250 T = 2.38 (out)(err) |
O = 23402 T = 87.67 (out)(err) |
| mprime01bc.wcsp.wcnf | O = 284 T = 2.25 |
O = 284 T = 2.25 (out)(err) |
O = 23697 T = 213.24 (out)(err) |
| mprime01cc.wcsp.wcnf | O = 603 T = 2.19 |
O = 603 T = 2.19 (out)(err) |
O = 81395 T = 89.50 (out)(err) |
| mprime03ac.wcsp.wcnf | O = 320 T = 0.41 |
O = 320 T = 0.41 (out)(err) |
O = 320 T = 7.71 (out)(err) |
| mprime03bc.wcsp.wcnf | O = 380 T = 0.41 |
O = 380 T = 0.41 (out)(err) |
O = 380 T = 2.61 (out)(err) |
| mprime03c.wcsp.wcnf | O = 320 T = 0.43 |
O = 320 T = 0.43 (out)(err) |
O = 320 T = 9.06 (out)(err) |
| mprime04bc.wcsp.wcnf | O = 600 T = 2.30 |
O = 600 T = 2.30 (out)(err) |
O = 187785 T = 148.15 (out)(err) |
| mprime04c.wcsp.wcnf | O = 590 T = 2.09 |
O = 590 T = 2.09 (out)(err) |
O = 198372 T = 123.86 (out)(err) |
| mprime04cc.wcsp.wcnf | O = 931 T = 1.66 |
O = 931 T = 1.66 (out)(err) |
O = 299528 T = 67.65 (out)(err) |
| rovers02ac.wcsp.wcnf | O = 1660 T = 1.66 |
O = 1660 T = 1.66 (out)(err) |
O = 73680 T = 141.31 (out)(err) |
| rovers02c.wcsp.wcnf | O = 1660 T = 1.29 |
O = 1660 T = 1.29 (out)(err) |
O = 73505 T = 216.81 (out)(err) |
| rovers02cc.wcsp.wcnf | O = 1668 T = 1.57 |
O = 1668 T = 1.57 (out)(err) |
O = 86769 T = 205.58 (out)(err) |
| satellite01ac.wcsp.wcnf | O = 1530 T = 1.67 |
O = 1530 T = 1.67 (out)(err) |
O = 242358 T = 25.18 (out)(err) |
| satellite01bc.wcsp.wcnf | O = 1827 T = 1.26 |
O = 1827 T = 1.26 (out)(err) |
O = 279600 T = 29.40 (out)(err) |
| satellite01cc.wcsp.wcnf | O = 1530 T = 1.68 |
O = 1530 T = 1.68 (out)(err) |
O = 242358 T = 31.06 (out)(err) |
| satellite02ac.wcsp.wcnf | O = 1611 T = 7.22 |
O = 1611 T = 7.22 (out)(err) |
O = 780890 T = 106.73 (out)(err) |
| satellite02bc.wcsp.wcnf | O = 2289 T = 8.49 |
O = 2289 T = 8.49 (out)(err) |
O = 1074869 T = 95.38 (out)(err) |
| zenotravel02ac.wcsp.wcnf | O = 2485 T = 1.64 |
O = 2485 T = 1.64 (out)(err) |
O = 101381 T = 102.76 (out)(err) |
| zenotravel02bc.wcsp.wcnf | O = 2335 T = 1.46 |
O = 2335 T = 1.46 (out)(err) |
O = 90576 T = 217.65 (out)(err) |
| zenotravel02c.wcsp.wcnf | O = 2485 T = 1.53 |
O = 2485 T = 1.53 (out)(err) |
O = 200942 T = 42.69 (out)(err) |
| zenotravel02cc.wcsp.wcnf | O = 742 T = 1.20 |
O = 742 T = 1.20 (out)(err) |
O = 24054 T = 223.86 (out)(err) |
| zenotravel04bc.wcsp.wcnf | O = 4110 T = 3.05 |
O = 4110 T = 3.05 (out)(err) |
O = 956175 T = 64.65 (out)(err) |
| zenotravel04c.wcsp.wcnf | O = 4270 T = 2.57 |
O = 4270 T = 2.57 (out)(err) |
O = 831864 T = 148.27 (out)(err) |
| zenotravel04cc.wcsp.wcnf | O = 1599 T = 1.94 |
O = 1599 T = 1.94 (out)(err) |
O = 209015 T = 230.12 (out)(err) |
| cap101.wcsp.wcnf | O = 8210005 T = 3.37 |
O = 8210005 T = 3.37 (out)(err) |
O = 12974269 T = 45.47 (out)(err) |
| cap102.wcsp.wcnf | O = 8838799 T = 12.39 |
O = 8838799 T = 12.39 (out)(err) |
O = 12815223 T = 215.14 (out)(err) |
| cap111.wcsp.wcnf | O = 8406208 T = 15.12 |
O = 8406208 T = 15.12 (out)(err) |
O = 17001841 T = 31.10 (out)(err) |
| cap112.wcsp.wcnf | O = 9024805 T = 3.02 |
O = 9024805 T = 3.02 (out)(err) |
O = 15750847 T = 40.64 (out)(err) |
| cap121.wcsp.wcnf | O = 8406208 T = 13.14 |
O = 8406208 T = 13.14 (out)(err) |
O = 16646915 T = 22.00 (out)(err) |
| cap122.wcsp.wcnf | O = 9024805 T = 3.57 |
O = 9024805 T = 3.57 (out)(err) |
O = 14547472 T = 2.70 (out)(err) |
| cap131.wcsp.wcnf | O = 8406208 T = 11.98 |
O = 8406208 T = 11.98 (out)(err) |
O = 14949911 T = 15.98 (out)(err) |
| cap132.wcsp.wcnf | O = 9024805 T = 3.84 |
O = 9024805 T = 3.84 (out)(err) |
O = 18363873 T = 40.60 (out)(err) |
| cap61.wcsp.wcnf | O = 9403819 T = 7.29 |
O = 9403819 T = 7.29 (out)(err) |
O = 11905152 T = 156.02 (out)(err) |
| cap62.wcsp.wcnf | O = 9915858 T = 1.76 |
O = 9915858 T = 1.76 (out)(err) |
O = 12431126 T = 119.71 (out)(err) |
| cap71.wcsp.wcnf | O = 9403819 T = 6.88 |
O = 9403819 T = 6.88 (out)(err) |
O = 12393663 T = 41.61 (out)(err) |
| cap72.wcsp.wcnf | O = 9915858 T = 1.84 |
O = 9915858 T = 1.84 (out)(err) |
O = 12429252 T = 208.44 (out)(err) |
| cap81.wcsp.wcnf | O = 8210005 T = 2.27 |
O = 8210005 T = 2.27 (out)(err) |
O = 12834429 T = 6.41 (out)(err) |
| cap82.wcsp.wcnf | O = 8838799 T = 12.24 |
O = 8838799 T = 12.24 (out)(err) |
O = 13782225 T = 41.62 (out)(err) |
| cap91.wcsp.wcnf | O = 8210005 T = 4.05 |
O = 8210005 T = 4.05 (out)(err) |
O = 13038760 T = 126.43 (out)(err) |
| cap92.wcsp.wcnf | O = 8838799 T = 12.28 |
O = 8838799 T = 12.28 (out)(err) |
O = 12723568 T = 150.94 (out)(err) |
| warehouse0.wcsp.wcnf | O = 328 T = 0.54 |
O = 328 T = 0.54 (out)(err) |
O = 328 T = 5.45 (out)(err) |
| warehouse1.wcsp.wcnf | O = 760418 T = 236.98 |
O = 760418 T = 236.98 (out)(err) |
O = 780173 T = 95.88 (out)(err) |
| normalized-mps-v2-20-10-bm23.opb.msat.wcnf | O = 34 T = 15.90 |
O = 34 T = 15.90 (out)(err) |
O = 1903 T = 46.74 (out)(err) |
| normalized-mps-v2-20-10-cracpb1.opb.msat.wcnf | O = 41418 T = 129.01 |
O = 41418 T = 129.01 (out)(err) |
O = 163358373 T = 39.22 (out)(err) |
| normalized-mps-v2-20-10-l152lav.opb.msat.wcnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 155029084 T = 102.25 (out)(err) |
| normalized-mps-v2-20-10-lp4l.opb.msat.wcnf | O = 4001 T = 144.72 |
O = 4001 T = 144.72 (out)(err) |
O = 29031982 T = 61.28 (out)(err) |
| normalized-mps-v2-20-10-lseu.opb.msat.wcnf | O = 1128 T = 122.13 |
O = 1128 T = 122.13 (out)(err) |
O = 299020 T = 54.99 (out)(err) |
| normalized-mps-v2-20-10-mod008.opb.msat.wcnf | O = 322 T = 19.27 |
O = 322 T = 19.27 (out)(err) |
O = 9291625 T = 73.27 (out)(err) |
| normalized-mps-v2-20-10-mod010.opb.msat.wcnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 137591790 T = 101.83 (out)(err) |
| normalized-mps-v2-20-10-p0033.opb.msat.wcnf | O = 3089 T = 1.55 |
O = 3089 T = 1.55 (out)(err) |
O = 3089 T = 33.19 (out)(err) |
| normalized-mps-v2-20-10-p0040.opb.msat.wcnf | O = 62027 T = 3.99 |
O = 62027 T = 5.45 (out)(err) |
O = 62027 T = 3.99 (out)(err) |
| normalized-mps-v2-20-10-p0201.opb.msat.wcnf | O = 1561 T = 5.82 |
O = 1561 T = 5.82 (out)(err) |
O = 629052 T = 23.43 (out)(err) |
| normalized-mps-v2-20-10-p0548.opb.msat.wcnf | O = 38973 T = 205.99 |
O = 38973 T = 205.99 (out)(err) |
O = 9320402 T = 53.49 (out)(err) |
| normalized-mps-v2-20-10-sentoy.opb.msat.wcnf | O = 4520 T = 261.09 |
O = 4520 T = 261.09 (out)(err) |
O = 4622456 T = 48.14 (out)(err) |
| random-net-100-2_network-10.net.wcnf | O = 96578 T = 14.43 |
O = 97603 T = 4.51 (out)(err) |
O = 96578 T = 14.43 (out)(err) |
| random-net-100-2_network-3.net.wcnf | O = 90211 T = 171.70 |
O = 96146 T = 4.39 (out)(err) |
O = 90211 T = 171.70 (out)(err) |
| random-net-100-2_network-5.net.wcnf | O = 94122 T = 176.83 |
O = 96403 T = 5.38 (out)(err) |
O = 94122 T = 176.83 (out)(err) |
| random-net-100-2_network-6.net.wcnf | O = 103262 T = 6.20 |
O = 103262 T = 6.20 (out)(err) |
O = 105441 T = 196.55 (out)(err) |
| random-net-100-2_network-8.net.wcnf | O = 95893 T = 14.32 |
O = 104642 T = 4.60 (out)(err) |
O = 95893 T = 14.32 (out)(err) |
| random-net-100-2_network-9.net.wcnf | O = 95718 T = 212.62 |
O = 97110 T = 4.93 (out)(err) |
O = 95718 T = 212.62 (out)(err) |
| random-net-200-1_network-1.net.wcnf | O = 182536 T = 17.47 |
O = 183347 T = 4.83 (out)(err) |
O = 182536 T = 17.47 (out)(err) |
| random-net-200-1_network-10.net.wcnf | O = 196916 T = 223.34 |
O = 198726 T = 1.45 (out)(err) |
O = 196916 T = 223.34 (out)(err) |
| random-net-200-1_network-3.net.wcnf | O = 199893 T = 25.99 |
O = 200083 T = 4.50 (out)(err) |
O = 199893 T = 25.99 (out)(err) |
| random-net-200-1_network-4.net.wcnf | O = 214653 T = 5.58 |
O = 214653 T = 5.58 (out)(err) |
O = 215488 T = 123.39 (out)(err) |
| random-net-200-1_network-5.net.wcnf | O = 192090 T = 4.21 |
O = 192090 T = 4.21 (out)(err) |
O = 195861 T = 123.94 (out)(err) |
| random-net-200-1_network-6.net.wcnf | O = 189081 T = 92.80 |
O = 191362 T = 2.48 (out)(err) |
O = 189081 T = 92.80 (out)(err) |
| random-net-200-1_network-7.net.wcnf | O = 196969 T = 2.29 |
O = 196969 T = 2.29 (out)(err) |
O = 197039 T = 75.62 (out)(err) |
| random-net-200-1_network-8.net.wcnf | O = 191067 T = 2.87 |
O = 191067 T = 2.87 (out)(err) |
O = 191916 T = 26.41 (out)(err) |
| random-net-200-1_network-9.net.wcnf | O = 201079 T = 5.02 |
O = 201079 T = 5.02 (out)(err) |
O = 203574 T = 95.00 (out)(err) |
| random-net-240-1_network-1.net.wcnf | O = 240940 T = 3.46 |
O = 240940 T = 3.46 (out)(err) |
O = 247332 T = 204.01 (out)(err) |
| random-net-240-1_network-10.net.wcnf | O = 240164 T = 4.96 |
O = 240164 T = 4.96 (out)(err) |
O = 242007 T = 153.55 (out)(err) |
| random-net-240-1_network-2.net.wcnf | O = 237263 T = 19.07 |
O = 244394 T = 2.70 (out)(err) |
O = 237263 T = 19.07 (out)(err) |
| random-net-240-1_network-3.net.wcnf | O = 230210 T = 4.78 |
O = 230210 T = 4.78 (out)(err) |
O = 231555 T = 153.97 (out)(err) |
| random-net-240-1_network-4.net.wcnf | O = 249914 T = 5.49 |
O = 249914 T = 5.49 (out)(err) |
O = 251009 T = 97.38 (out)(err) |
| random-net-240-1_network-5.net.wcnf | O = 240776 T = 3.87 |
O = 240776 T = 3.87 (out)(err) |
O = 245542 T = 121.61 (out)(err) |
| random-net-240-1_network-6.net.wcnf | O = 242720 T = 45.35 |
O = 250020 T = 2.44 (out)(err) |
O = 242720 T = 45.35 (out)(err) |
| random-net-240-1_network-7.net.wcnf | O = 239780 T = 4.05 |
O = 239780 T = 4.05 (out)(err) |
O = 242233 T = 221.74 (out)(err) |
| random-net-240-1_network-8.net.wcnf | O = 249984 T = 134.59 |
O = 253357 T = 7.23 (out)(err) |
O = 249984 T = 134.59 (out)(err) |
| random-net-240-1_network-9.net.wcnf | O = 233054 T = 3.00 |
O = 233054 T = 3.00 (out)(err) |
O = 236123 T = 217.12 (out)(err) |
| random-net-280-1_network-10.net.wcnf | O = 278934 T = 4.82 |
O = 278934 T = 4.82 (out)(err) |
O = 279286 T = 47.17 (out)(err) |
| random-net-280-1_network-2.net.wcnf | O = 283834 T = 3.93 |
O = 283834 T = 3.93 (out)(err) |
O = 289034 T = 175.75 (out)(err) |
| random-net-280-1_network-3.net.wcnf | O = 271619 T = 4.32 |
O = 271619 T = 4.32 (out)(err) |
O = 279327 T = 183.37 (out)(err) |
| random-net-280-1_network-4.net.wcnf | O = 268759 T = 2.79 |
O = 268759 T = 2.79 (out)(err) |
O = 272505 T = 99.83 (out)(err) |
| random-net-280-1_network-5.net.wcnf | O = 268452 T = 4.86 |
O = 268452 T = 4.86 (out)(err) |
O = 276103 T = 84.00 (out)(err) |
| random-net-280-1_network-6.net.wcnf | O = 284501 T = 6.44 |
O = 284501 T = 6.44 (out)(err) |
O = 290476 T = 49.46 (out)(err) |
| random-net-280-1_network-7.net.wcnf | O = 274004 T = 3.99 |
O = 274004 T = 3.99 (out)(err) |
O = 288773 T = 90.36 (out)(err) |
| random-net-280-1_network-8.net.wcnf | O = 284946 T = 5.93 |
O = 284946 T = 5.93 (out)(err) |
O = 289630 T = 198.28 (out)(err) |
| random-net-280-1_network-9.net.wcnf | O = 283837 T = 6.01 |
O = 283837 T = 6.01 (out)(err) |
O = 290775 T = 170.66 (out)(err) |
| random-net-300-1_network-1.net.wcnf | O = 305999 T = 3.63 |
O = 305999 T = 3.63 (out)(err) |
O = 316826 T = 230.01 (out)(err) |
| random-net-300-1_network-10.net.wcnf | O = 285482 T = 5.62 |
O = 285482 T = 5.62 (out)(err) |
O = 296847 T = 92.78 (out)(err) |
| random-net-300-1_network-2.net.wcnf | O = 311334 T = 3.51 |
O = 311334 T = 3.51 (out)(err) |
O = 321408 T = 221.37 (out)(err) |
| random-net-300-1_network-3.net.wcnf | O = 286632 T = 5.82 |
O = 286632 T = 5.82 (out)(err) |
O = 299825 T = 46.00 (out)(err) |
| random-net-300-1_network-4.net.wcnf | O = 304305 T = 5.74 |
O = 304305 T = 5.74 (out)(err) |
O = 304843 T = 50.70 (out)(err) |
| random-net-300-1_network-5.net.wcnf | O = 284274 T = 5.40 |
O = 284274 T = 5.40 (out)(err) |
O = 295322 T = 178.88 (out)(err) |
| random-net-300-1_network-6.net.wcnf | O = 286771 T = 3.46 |
O = 286771 T = 3.46 (out)(err) |
O = 288971 T = 62.68 (out)(err) |
| random-net-300-1_network-7.net.wcnf | O = 309992 T = 4.75 |
O = 309992 T = 4.75 (out)(err) |
O = 320274 T = 188.53 (out)(err) |
| random-net-300-1_network-8.net.wcnf | O = 294782 T = 4.46 |
O = 294782 T = 4.46 (out)(err) |
O = 299562 T = 35.10 (out)(err) |
| random-net-300-1_network-9.net.wcnf | O = 288106 T = 4.62 |
O = 288106 T = 4.62 (out)(err) |
O = 294999 T = 113.00 (out)(err) |
| random-net-50-2_network-1.net.wcnf | O = 49211 T = 46.39 |
O = 52652 T = 2.40 (out)(err) |
O = 49211 T = 46.39 (out)(err) |
| random-net-50-2_network-10.net.wcnf | O = 45280 T = 89.31 |
O = 47659 T = 5.06 (out)(err) |
O = 45280 T = 89.31 (out)(err) |
| random-net-50-2_network-2.net.wcnf | O = 43782 T = 20.69 |
O = 52689 T = 5.06 (out)(err) |
O = 43782 T = 20.69 (out)(err) |
| random-net-50-2_network-3.net.wcnf | O = 47460 T = 146.23 |
O = 50377 T = 4.75 (out)(err) |
O = 47460 T = 146.23 (out)(err) |
| random-net-50-2_network-4.net.wcnf | O = 45413 T = 72.98 |
O = 48133 T = 2.99 (out)(err) |
O = 45413 T = 72.98 (out)(err) |
| random-net-50-2_network-5.net.wcnf | O = 50723 T = 141.21 |
O = 53391 T = 5.93 (out)(err) |
O = 50723 T = 141.21 (out)(err) |
| random-net-50-2_network-6.net.wcnf | O = 43465 T = 42.18 |
O = 49783 T = 4.65 (out)(err) |
O = 43465 T = 42.18 (out)(err) |
| random-net-50-2_network-7.net.wcnf | O = 47477 T = 106.36 |
O = 50173 T = 4.25 (out)(err) |
O = 47477 T = 106.36 (out)(err) |
| random-net-50-2_network-8.net.wcnf | O = 48254 T = 48.68 |
O = 49345 T = 5.11 (out)(err) |
O = 48254 T = 48.68 (out)(err) |
| random-net-50-2_network-9.net.wcnf | O = 49381 T = 48.70 |
O = 52968 T = 1.15 (out)(err) |
O = 49381 T = 48.70 (out)(err) |
| random-net-60-2_network-1.net.wcnf | O = 55064 T = 26.40 |
O = 57244 T = 4.87 (out)(err) |
O = 55064 T = 26.40 (out)(err) |
| random-net-60-2_network-10.net.wcnf | O = 48893 T = 9.27 |
O = 55003 T = 1.65 (out)(err) |
O = 48893 T = 9.27 (out)(err) |
| random-net-60-2_network-2.net.wcnf | O = 58772 T = 168.45 |
O = 64469 T = 4.78 (out)(err) |
O = 58772 T = 168.45 (out)(err) |
| random-net-60-2_network-3.net.wcnf | O = 57978 T = 5.82 |
O = 61697 T = 1.17 (out)(err) |
O = 57978 T = 5.82 (out)(err) |
| random-net-60-2_network-4.net.wcnf | O = 56512 T = 180.43 |
O = 60160 T = 3.73 (out)(err) |
O = 56512 T = 180.43 (out)(err) |
| random-net-60-2_network-5.net.wcnf | O = 59266 T = 84.41 |
O = 60282 T = 4.83 (out)(err) |
O = 59266 T = 84.41 (out)(err) |
| random-net-60-2_network-6.net.wcnf | O = 57246 T = 26.30 |
O = 60527 T = 4.63 (out)(err) |
O = 57246 T = 26.30 (out)(err) |
| random-net-60-2_network-7.net.wcnf | O = 56705 T = 106.26 |
O = 58281 T = 3.80 (out)(err) |
O = 56705 T = 106.26 (out)(err) |
| random-net-60-2_network-8.net.wcnf | O = 50192 T = 130.38 |
O = 55132 T = 2.05 (out)(err) |
O = 50192 T = 130.38 (out)(err) |
| random-net-60-2_network-9.net.wcnf | O = 53526 T = 40.95 |
O = 56803 T = 5.44 (out)(err) |
O = 53526 T = 40.95 (out)(err) |
| random-net-80-2_network-1.net.wcnf | O = 69768 T = 54.31 |
O = 73917 T = 4.15 (out)(err) |
O = 69768 T = 54.31 (out)(err) |
| random-net-80-2_network-10.net.wcnf | O = 76052 T = 17.44 |
O = 79146 T = 2.24 (out)(err) |
O = 76052 T = 17.44 (out)(err) |
| random-net-80-2_network-2.net.wcnf | O = 77408 T = 6.15 |
O = 77408 T = 6.15 (out)(err) |
O = 77532 T = 59.24 (out)(err) |
| random-net-80-2_network-3.net.wcnf | O = 73231 T = 125.98 |
O = 79940 T = 2.54 (out)(err) |
O = 73231 T = 125.98 (out)(err) |
| random-net-80-2_network-4.net.wcnf | O = 80704 T = 36.11 |
O = 83744 T = 2.32 (out)(err) |
O = 80704 T = 36.11 (out)(err) |
| random-net-80-2_network-5.net.wcnf | O = 76215 T = 109.03 |
O = 78969 T = 4.76 (out)(err) |
O = 76215 T = 109.03 (out)(err) |
| random-net-80-2_network-6.net.wcnf | O = 72102 T = 119.41 |
O = 73389 T = 2.37 (out)(err) |
O = 72102 T = 119.41 (out)(err) |
| random-net-80-2_network-7.net.wcnf | O = 73987 T = 5.44 |
O = 73987 T = 5.44 (out)(err) |
O = 76685 T = 39.31 (out)(err) |
| random-net-80-2_network-8.net.wcnf | O = 74317 T = 205.22 |
O = 79666 T = 5.16 (out)(err) |
O = 74317 T = 205.22 (out)(err) |
| random-net-80-2_network-9.net.wcnf | O = 73215 T = 71.72 |
O = 76225 T = 5.94 (out)(err) |
O = 73215 T = 71.72 (out)(err) |
| 1401.wcsp.dir.wcnf | O = 475112 T = 128.82 |
O = 499114 T = 1.98 (out)(err) |
O = 475112 T = 128.82 (out)(err) |
| 1403.wcsp.dir.wcnf | O = 481264 T = 240.45 |
O = 506264 T = 4.12 (out)(err) |
O = 481264 T = 240.45 (out)(err) |
| 1405.wcsp.dir.wcnf | O = 481447 T = 265.27 |
O = 486450 T = 29.04 (out)(err) |
O = 481447 T = 265.27 (out)(err) |
| 1407.wcsp.dir.wcnf | O = 477626 T = 210.14 |
O = 505617 T = 2.97 (out)(err) |
O = 477626 T = 210.14 (out)(err) |
| 1502.wcsp.dir.wcnf | O = 28042 T = 0.59 |
O = 28042 T = 0.59 (out)(err) |
O = 28042 T = 11.50 (out)(err) |
| 1504.wcsp.dir.wcnf | O = 166312 T = 156.12 |
O = 180325 T = 2.23 (out)(err) |
O = 166312 T = 156.12 (out)(err) |
| 1506.wcsp.dir.wcnf | O = 376579 T = 69.91 |
O = 391570 T = 4.94 (out)(err) |
O = 376579 T = 69.91 (out)(err) |
| 28.wcsp.dir.wcnf | O = 271105 T = 60.64 |
O = 285115 T = 28.83 (out)(err) |
O = 271105 T = 60.64 (out)(err) |
| 29.wcsp.dir.wcnf | O = 8059 T = 4.68 |
O = 9059 T = 205.61 (out)(err) |
O = 8059 T = 4.68 (out)(err) |
| 404.wcsp.dir.wcnf | O = 114 T = 4.63 |
O = 118 T = 0.44 (out)(err) |
O = 114 T = 4.63 (out)(err) |
| 408.wcsp.dir.wcnf | O = 6229 T = 62.61 |
O = 6234 T = 51.61 (out)(err) |
O = 6229 T = 62.61 (out)(err) |
| 412.wcsp.dir.wcnf | O = 32391 T = 234.60 |
O = 35412 T = 4.12 (out)(err) |
O = 32391 T = 234.60 (out)(err) |
| 414.wcsp.dir.wcnf | O = 38501 T = 42.26 |
O = 42512 T = 45.95 (out)(err) |
O = 38501 T = 42.26 (out)(err) |
| 42.wcsp.dir.wcnf | O = 157050 T = 182.20 |
O = 163050 T = 36.48 (out)(err) |
O = 157050 T = 182.20 (out)(err) |
| 5.wcsp.dir.wcnf | O = 269 T = 17.81 |
O = 276 T = 2.45 (out)(err) |
O = 269 T = 17.81 (out)(err) |
| 503.wcsp.dir.wcnf | O = 11113 T = 23.40 |
O = 11123 T = 0.59 (out)(err) |
O = 11113 T = 23.40 (out)(err) |
| 505.wcsp.dir.wcnf | O = 21259 T = 132.89 |
O = 22269 T = 4.75 (out)(err) |
O = 21259 T = 132.89 (out)(err) |
| 507.wcsp.dir.wcnf | O = 27396 T = 39.00 |
O = 28429 T = 5.02 (out)(err) |
O = 27396 T = 39.00 (out)(err) |
| 509.wcsp.dir.wcnf | O = 36460 T = 60.74 |
O = 40471 T = 6.80 (out)(err) |
O = 36460 T = 60.74 (out)(err) |
| 54.wcsp.dir.wcnf | O = 37 T = 4.50 |
O = 37 T = 4.50 (out)(err) |
O = 37 T = 4.88 (out)(err) |
| 8.wcsp.dir.wcnf | O = 2 T = 0.33 |
O = 2 T = 0.33 (out)(err) |
O = 2 T = 0.48 (out)(err) |
| 1401.wcsp.log.wcnf | O = 488111 T = 188.61 |
O = 503113 T = 5.35 (out)(err) |
O = 488111 T = 188.61 (out)(err) |
| 1403.wcsp.log.wcnf | O = 491273 T = 236.94 |
O = 510272 T = 4.32 (out)(err) |
O = 491273 T = 236.94 (out)(err) |
| 1405.wcsp.log.wcnf | O = 493442 T = 151.97 |
O = 522453 T = 4.71 (out)(err) |
O = 493442 T = 151.97 (out)(err) |
| 1407.wcsp.log.wcnf | O = 492626 T = 189.24 |
O = 516637 T = 5.32 (out)(err) |
O = 492626 T = 189.24 (out)(err) |
| 1502.wcsp.log.wcnf | O = 28042 T = 5.79 |
O = 29042 T = 4.12 (out)(err) |
O = 28042 T = 5.79 (out)(err) |
| 1504.wcsp.log.wcnf | O = 170312 T = 27.15 |
O = 179318 T = 3.79 (out)(err) |
O = 170312 T = 27.15 (out)(err) |
| 1506.wcsp.log.wcnf | O = 384564 T = 38.43 |
O = 396566 T = 3.92 (out)(err) |
O = 384564 T = 38.43 (out)(err) |
| 28.wcsp.log.wcnf | O = 271110 T = 82.01 |
O = 288115 T = 4.56 (out)(err) |
O = 271110 T = 82.01 (out)(err) |
| 29.wcsp.log.wcnf | O = 8059 T = 3.09 |
O = 8059 T = 73.61 (out)(err) |
O = 8059 T = 3.09 (out)(err) |
| 404.wcsp.log.wcnf | O = 114 T = 3.75 |
O = 118 T = 5.21 (out)(err) |
O = 114 T = 3.75 (out)(err) |
| 408.wcsp.log.wcnf | O = 6230 T = 9.32 |
O = 6239 T = 26.87 (out)(err) |
O = 6230 T = 9.32 (out)(err) |
| 412.wcsp.log.wcnf | O = 32393 T = 19.62 |
O = 34411 T = 5.34 (out)(err) |
O = 32393 T = 19.62 (out)(err) |
| 414.wcsp.log.wcnf | O = 39495 T = 117.36 |
O = 41509 T = 4.60 (out)(err) |
O = 39495 T = 117.36 (out)(err) |
| 42.wcsp.log.wcnf | O = 160050 T = 90.82 |
O = 175055 T = 2.88 (out)(err) |
O = 160050 T = 90.82 (out)(err) |
| 5.wcsp.log.wcnf | O = 272 T = 22.54 |
O = 281 T = 9.24 (out)(err) |
O = 272 T = 22.54 (out)(err) |
| 503.wcsp.log.wcnf | O = 11113 T = 28.25 |
O = 12122 T = 4.47 (out)(err) |
O = 11113 T = 28.25 (out)(err) |
| 505.wcsp.log.wcnf | O = 21256 T = 20.86 |
O = 23268 T = 5.20 (out)(err) |
O = 21256 T = 20.86 (out)(err) |
| 507.wcsp.log.wcnf | O = 27401 T = 156.99 |
O = 29439 T = 4.11 (out)(err) |
O = 27401 T = 156.99 (out)(err) |
| 509.wcsp.log.wcnf | O = 36458 T = 187.94 |
O = 40471 T = 5.58 (out)(err) |
O = 36458 T = 187.94 (out)(err) |
| 54.wcsp.log.wcnf | O = 37 T = 2.60 |
O = 37 T = 5.92 (out)(err) |
O = 37 T = 2.60 (out)(err) |
| 8.wcsp.log.wcnf | O = 2 T = 0.34 |
O = 2 T = 0.34 (out)(err) |
O = 2 T = 0.74 (out)(err) |