*** This is NuSMV 2.3.1 (compiled on Mon Nov 21 15:48:12 UTC 2005)
*** For more information on NuSMV see <http://nusmv.irst.itc.it>
*** or email to <nusmv-users@irst.itc.it>.
*** Please report bugs to <nusmv@irst.itc.it>.

WARNING *** This version of NuSMV is linked to the MiniSat SAT solver       ***
WARNING *** See http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat ***
WARNING *** Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson           ***
WARNING *** MiniSat is used in Bounded Model Checking when the              ***
WARNING *** environment variable sat_solver is set to 'minisat'.            ***
WARNING *** THE SOFTWARE IS PROVIDED 'AS IS', WITHOUT WARRANTY OF ANY KIND, ***
WARNING *** EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES ***
WARNING *** OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND        ***
WARNING *** NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT     ***
WARNING *** HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,    ***
WARNING *** WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING    ***
WARNING *** FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR   ***
WARNING *** OTHER DEALINGS IN THE SOFTWARE.                                 ***

Starting the batch interaction.
Parsing file /workspace/gabe/AMBA_AHB_Performance_Evaluation_64x64_Tiles.smv ......done.
Flattening hierarchy ......done.
Encoding variables ...... done.
Building Model ...checking for multiple assignments...
Done
checking for circular assignments...
Done
... done.
... done.
evaluating specification  AG (START4 -> TIME < 1100)  
Computing the set of fair <state>x<input> pairs
  size of res0 = 3.86856e+25 <states>x<input>, 1 BDD nodes
  size of res1 = 7.59127e+19 <states>x<input>, 2892 BDD nodes
done
eu: computing fixed point approximations for AG (START4 -> TIME < 1100) ...
size of Y1 = 1.85334e+16 states, 6820 BDD nodes
size of Y2 = 1.93954e+16 states, 7307 BDD nodes
size of Y3 = 2.04729e+16 states, 7703 BDD nodes
size of Y4 = 2.11194e+16 states, 7956 BDD nodes
size of Y5 = 2.28165e+16 states, 8795 BDD nodes
size of Y6 = 2.47857e+16 states, 9973 BDD nodes
size of Y7 = 2.58211e+16 states, 10514 BDD nodes
size of Y8 = 2.61633e+16 states, 10982 BDD nodes
size of Y9 = 2.6596e+16 states, 12130 BDD nodes
size of Y10 = 2.69939e+16 states, 14321 BDD nodes
size of Y11 = 2.73817e+16 states, 16678 BDD nodes
size of Y12 = 2.76272e+16 states, 18393 BDD nodes
size of Y13 = 2.80224e+16 states, 21575 BDD nodes
size of Y14 = 2.84951e+16 states, 25038 BDD nodes
size of Y15 = 2.88274e+16 states, 28053 BDD nodes
size of Y16 = 2.90568e+16 states, 30918 BDD nodes
size of Y17 = 2.93355e+16 states, 34664 BDD nodes
size of Y18 = 2.9661e+16 states, 37641 BDD nodes
size of Y19 = 3.00046e+16 states, 41890 BDD nodes
size of Y20 = 3.02643e+16 states, 45367 BDD nodes
size of Y21 = 3.05682e+16 states, 49528 BDD nodes
size of Y22 = 3.08829e+16 states, 54497 BDD nodes
size of Y23 = 3.11324e+16 states, 58834 BDD nodes
size of Y24 = 3.13398e+16 states, 63545 BDD nodes
size of Y25 = 3.15465e+16 states, 67763 BDD nodes
size of Y26 = 3.17511e+16 states, 71242 BDD nodes
size of Y27 = 3.19589e+16 states, 77295 BDD nodes
size of Y28 = 3.21603e+16 states, 82644 BDD nodes
size of Y29 = 3.23656e+16 states, 88053 BDD nodes
size of Y30 = 3.25741e+16 states, 92729 BDD nodes
size of Y31 = 3.27787e+16 states, 98027 BDD nodes
size of Y32 = 3.29822e+16 states, 103282 BDD nodes
size of Y33 = 3.31883e+16 states, 107584 BDD nodes
size of Y34 = 3.33951e+16 states, 113053 BDD nodes
size of Y35 = 3.36039e+16 states, 118923 BDD nodes
size of Y36 = 3.38145e+16 states, 124579 BDD nodes
size of Y37 = 3.40273e+16 states, 130718 BDD nodes
size of Y38 = 3.42421e+16 states, 136426 BDD nodes
size of Y39 = 3.44588e+16 states, 142594 BDD nodes
size of Y40 = 3.46775e+16 states, 148593 BDD nodes
size of Y41 = 3.48983e+16 states, 154677 BDD nodes
size of Y42 = 3.51211e+16 states, 160692 BDD nodes
size of Y43 = 3.53459e+16 states, 167010 BDD nodes
size of Y44 = 3.55728e+16 states, 172924 BDD nodes
size of Y45 = 3.58018e+16 states, 179528 BDD nodes
size of Y46 = 3.60327e+16 states, 185459 BDD nodes
size of Y47 = 3.62658e+16 states, 191728 BDD nodes
size of Y48 = 3.65008e+16 states, 197782 BDD nodes
size of Y49 = 3.6738e+16 states, 204071 BDD nodes
size of Y50 = 3.6977e+16 states, 209947 BDD nodes
size of Y51 = 3.7218e+16 states, 216455 BDD nodes
size of Y52 = 3.74607e+16 states, 222495 BDD nodes
size of Y53 = 3.77053e+16 states, 228909 BDD nodes
size of Y54 = 3.79513e+16 states, 234480 BDD nodes
size of Y55 = 3.81988e+16 states, 240555 BDD nodes
size of Y56 = 3.84481e+16 states, 246678 BDD nodes
size of Y57 = 3.86989e+16 states, 252251 BDD nodes
size of Y58 = 3.89596e+16 states, 257930 BDD nodes
size of Y59 = 3.92223e+16 states, 264381 BDD nodes
size of Y60 = 3.94829e+16 states, 269433 BDD nodes
size of Y61 = 3.98054e+16 states, 275680 BDD nodes
size of Y62 = 4.00922e+16 states, 282038 BDD nodes
size of Y63 = 4.03702e+16 states, 287940 BDD nodes
size of Y64 = 4.06535e+16 states, 293855 BDD nodes
size of Y65 = 4.0946e+16 states, 299897 BDD nodes
size of Y66 = 4.12279e+16 states, 305282 BDD nodes
size of Y67 = 4.15064e+16 states, 310903 BDD nodes
size of Y68 = 4.17926e+16 states, 314251 BDD nodes
size of Y69 = 4.20726e+16 states, 320243 BDD nodes
size of Y70 = 4.2358e+16 states, 326892 BDD nodes
size of Y71 = 4.26444e+16 states, 333217 BDD nodes
size of Y72 = 4.29417e+16 states, 338904 BDD nodes
size of Y73 = 4.32356e+16 states, 344732 BDD nodes
size of Y74 = 4.35313e+16 states, 348489 BDD nodes
size of Y75 = 4.38249e+16 states, 357294 BDD nodes
size of Y76 = 4.41185e+16 states, 365007 BDD nodes
size of Y77 = 4.44142e+16 states, 364957 BDD nodes
size of Y78 = 4.4862e+16 states, 371883 BDD nodes
size of Y79 = 4.53131e+16 states, 379964 BDD nodes
size of Y80 = 4.57679e+16 states, 381849 BDD nodes
size of Y81 = 4.62269e+16 states, 377727 BDD nodes
size of Y82 = 4.66898e+16 states, 376156 BDD nodes
size of Y83 = 4.71565e+16 states, 374921 BDD nodes
size of Y84 = 4.76271e+16 states, 371185 BDD nodes
size of Y85 = 4.81017e+16 states, 359341 BDD nodes
size of Y86 = 4.85801e+16 states, 364103 BDD nodes
size of Y87 = 4.90625e+16 states, 369041 BDD nodes
size of Y88 = 4.95489e+16 states, 373955 BDD nodes
size of Y89 = 5.00391e+16 states, 379363 BDD nodes
size of Y90 = 5.05334e+16 states, 384206 BDD nodes
size of Y91 = 5.10315e+16 states, 389303 BDD nodes
size of Y92 = 5.15336e+16 states, 394357 BDD nodes
size of Y93 = 5.20397e+16 states, 399958 BDD nodes
size of Y94 = 5.25497e+16 states, 405004 BDD nodes
size of Y95 = 5.30636e+16 states, 410263 BDD nodes
size of Y96 = 5.35815e+16 states, 415494 BDD nodes
size of Y97 = 5.41033e+16 states, 421370 BDD nodes
size of Y98 = 5.4629e+16 states, 426513 BDD nodes
size of Y99 = 5.51587e+16 states, 431943 BDD nodes
size of Y100 = 5.56923e+16 states, 437417 BDD nodes
size of Y101 = 5.62299e+16 states, 443423 BDD nodes
size of Y102 = 5.67714e+16 states, 448812 BDD nodes
size of Y103 = 5.73168e+16 states, 454450 BDD nodes
size of Y104 = 5.78662e+16 states, 460084 BDD nodes
size of Y105 = 5.84195e+16 states, 466333 BDD nodes
size of Y106 = 5.89767e+16 states, 471907 BDD nodes
size of Y107 = 5.95379e+16 states, 477771 BDD nodes
size of Y108 = 6.0103e+16 states, 483626 BDD nodes
size of Y109 = 6.0672e+16 states, 490197 BDD nodes
size of Y110 = 6.1245e+16 states, 496013 BDD nodes
size of Y111 = 6.18219e+16 states, 502064 BDD nodes
size of Y112 = 6.24027e+16 states, 508144 BDD nodes
size of Y113 = 6.29875e+16 states, 514840 BDD nodes
size of Y114 = 6.35762e+16 states, 520931 BDD nodes
size of Y115 = 6.41689e+16 states, 527397 BDD nodes
size of Y116 = 6.47655e+16 states, 533916 BDD nodes
size of Y117 = 6.53661e+16 states, 540960 BDD nodes
size of Y118 = 6.59707e+16 states, 547254 BDD nodes
size of Y119 = 6.65793e+16 states, 553808 BDD nodes
size of Y120 = 6.71919e+16 states, 560283 BDD nodes
size of Y121 = 6.78083e+16 states, 567396 BDD nodes
size of Y122 = 6.84284e+16 states, 573690 BDD nodes
size of Y123 = 6.90525e+16 states, 580240 BDD nodes
size of Y124 = 6.96783e+16 states, 586877 BDD nodes
size of Y125 = 7.03073e+16 states, 594149 BDD nodes
size of Y126 = 7.09399e+16 states, 600526 BDD nodes
size of Y127 = 7.15759e+16 states, 607190 BDD nodes
size of Y128 = 7.22154e+16 states, 613846 BDD nodes
size of Y129 = 7.28585e+16 states, 621270 BDD nodes
size of Y130 = 7.35054e+16 states, 627673 BDD nodes
size of Y131 = 7.41562e+16 states, 634473 BDD nodes
size of Y132 = 7.48109e+16 states, 641350 BDD nodes
size of Y133 = 7.54695e+16 states, 648831 BDD nodes
size of Y134 = 7.6132e+16 states, 655359 BDD nodes
size of Y135 = 7.6798e+16 states, 662249 BDD nodes
size of Y136 = 7.74678e+16 states, 669193 BDD nodes
size of Y137 = 7.81413e+16 states, 676930 BDD nodes
size of Y138 = 7.88187e+16 states, 683775 BDD nodes
size of Y139 = 7.95001e+16 states, 690906 BDD nodes
size of Y140 = 8.01855e+16 states, 698295 BDD nodes
size of Y141 = 8.08748e+16 states, 706728 BDD nodes
size of Y142 = 8.15682e+16 states, 714091 BDD nodes
size of Y143 = 8.22653e+16 states, 721721 BDD nodes
size of Y144 = 8.29665e+16 states, 729451 BDD nodes
size of Y145 = 8.36717e+16 states, 738047 BDD nodes
size of Y146 = 8.43808e+16 states, 745398 BDD nodes
size of Y147 = 8.50939e+16 states, 753070 BDD nodes
size of Y148 = 8.5811e+16 states, 760883 BDD nodes
size of Y149 = 8.65321e+16 states, 769310 BDD nodes
size of Y150 = 8.72572e+16 states, 776584 BDD nodes
size of Y151 = 8.79862e+16 states, 784186 BDD nodes
size of Y152 = 8.87192e+16 states, 791829 BDD nodes
size of Y153 = 8.94563e+16 states, 800195 BDD nodes
size of Y154 = 9.01972e+16 states, 807429 BDD nodes
size of Y155 = 9.09422e+16 states, 815027 BDD nodes
size of Y156 = 9.16912e+16 states, 822643 BDD nodes
size of Y157 = 9.24441e+16 states, 831114 BDD nodes
size of Y158 = 9.3201e+16 states, 838278 BDD nodes
size of Y159 = 9.39619e+16 states, 845768 BDD nodes
size of Y160 = 9.47268e+16 states, 853331 BDD nodes
size of Y161 = 9.54956e+16 states, 861705 BDD nodes
size of Y162 = 9.62685e+16 states, 868756 BDD nodes
size of Y163 = 9.70453e+16 states, 876225 BDD nodes
size of Y164 = 9.78261e+16 states, 883815 BDD nodes
size of Y165 = 9.86109e+16 states, 892076 BDD nodes
size of Y166 = 9.93996e+16 states, 899053 BDD nodes
size of Y167 = 1.00192e+17 states, 906376 BDD nodes
size of Y168 = 1.00989e+17 states, 913725 BDD nodes
size of Y169 = 1.0179e+17 states, 921850 BDD nodes
size of Y170 = 1.02594e+17 states, 928691 BDD nodes
size of Y171 = 1.03403e+17 states, 935889 BDD nodes
size of Y172 = 1.04216e+17 states, 943070 BDD nodes
size of Y173 = 1.05032e+17 states, 951271 BDD nodes
size of Y174 = 1.05853e+17 states, 957912 BDD nodes
size of Y175 = 1.06678e+17 states, 964895 BDD nodes
size of Y176 = 1.07506e+17 states, 972017 BDD nodes
size of Y177 = 1.08339e+17 states, 980016 BDD nodes
size of Y178 = 1.09175e+17 states, 986499 BDD nodes
size of Y179 = 1.10016e+17 states, 993464 BDD nodes
size of Y180 = 1.1086e+17 states, 1000595 BDD nodes
size of Y181 = 1.11709e+17 states, 1008415 BDD nodes
size of Y182 = 1.12561e+17 states, 1014822 BDD nodes
size of Y183 = 1.13418e+17 states, 1021637 BDD nodes
size of Y184 = 1.14278e+17 states, 1028539 BDD nodes
size of Y185 = 1.15142e+17 states, 1036337 BDD nodes
size of Y186 = 1.16011e+17 states, 1042745 BDD nodes
size of Y187 = 1.16883e+17 states, 1049602 BDD nodes
size of Y188 = 1.1776e+17 states, 1056487 BDD nodes
size of Y189 = 1.1864e+17 states, 1064433 BDD nodes
size of Y190 = 1.19524e+17 states, 1070798 BDD nodes
size of Y191 = 1.20412e+17 states, 1077574 BDD nodes
size of Y192 = 1.21305e+17 states, 1084469 BDD nodes
size of Y193 = 1.22201e+17 states, 1092350 BDD nodes
size of Y194 = 1.23101e+17 states, 1098656 BDD nodes
size of Y195 = 1.24005e+17 states, 1105517 BDD nodes
size of Y196 = 1.24913e+17 states, 1112533 BDD nodes
size of Y197 = 1.25826e+17 states, 1120398 BDD nodes
size of Y198 = 1.26742e+17 states, 1126738 BDD nodes
size of Y199 = 1.27662e+17 states, 1133533 BDD nodes
size of Y200 = 1.28586e+17 states, 1140396 BDD nodes
size of Y201 = 1.29514e+17 states, 1148227 BDD nodes
size of Y202 = 1.30446e+17 states, 1154541 BDD nodes
size of Y203 = 1.31382e+17 states, 1161354 BDD nodes
size of Y204 = 1.32322e+17 states, 1168167 BDD nodes
size of Y205 = 1.33266e+17 states, 1176207 BDD nodes
size of Y206 = 1.34214e+17 states, 1182475 BDD nodes
size of Y207 = 1.35166e+17 states, 1189203 BDD nodes
size of Y208 = 1.36122e+17 states, 1196108 BDD nodes
size of Y209 = 1.37082e+17 states, 1204078 BDD nodes
size of Y210 = 1.38045e+17 states, 1210305 BDD nodes
size of Y211 = 1.39013e+17 states, 1217151 BDD nodes
size of Y212 = 1.39985e+17 states, 1224198 BDD nodes
size of Y213 = 1.40961e+17 states, 1232130 BDD nodes
size of Y214 = 1.41941e+17 states, 1238410 BDD nodes
size of Y215 = 1.42924e+17 states, 1245187 BDD nodes
size of Y216 = 1.43912e+17 states, 1252036 BDD nodes
size of Y217 = 1.44904e+17 states, 1259942 BDD nodes
size of Y218 = 1.45899e+17 states, 1266195 BDD nodes
size of Y219 = 1.46899e+17 states, 1273024 BDD nodes
size of Y220 = 1.47903e+17 states, 1279852 BDD nodes
size of Y221 = 1.4891e+17 states, 1287938 BDD nodes
size of Y222 = 1.49922e+17 states, 1294175 BDD nodes
size of Y223 = 1.50938e+17 states, 1300915 BDD nodes
size of Y224 = 1.51957e+17 states, 1307798 BDD nodes
size of Y225 = 1.52981e+17 states, 1315828 BDD nodes
size of Y226 = 1.54008e+17 states, 1322005 BDD nodes
size of Y227 = 1.5504e+17 states, 1328834 BDD nodes
size of Y228 = 1.56075e+17 states, 1335828 BDD nodes
size of Y229 = 1.57115e+17 states, 1343812 BDD nodes
size of Y230 = 1.58158e+17 states, 1350029 BDD nodes
size of Y231 = 1.59206e+17 states, 1356777 BDD nodes
size of Y232 = 1.60257e+17 states, 1363603 BDD nodes
size of Y233 = 1.61312e+17 states, 1371558 BDD nodes
size of Y234 = 1.62372e+17 states, 1377719 BDD nodes
size of Y235 = 1.63435e+17 states, 1384449 BDD nodes
size of Y236 = 1.64502e+17 states, 1391152 BDD nodes
size of Y237 = 1.65574e+17 states, 1399337 BDD nodes
size of Y238 = 1.66649e+17 states, 1405383 BDD nodes
size of Y239 = 1.67728e+17 states, 1411942 BDD nodes
size of Y240 = 1.68811e+17 states, 1418729 BDD nodes
size of Y241 = 1.69899e+17 states, 1426729 BDD nodes
size of Y242 = 1.7099e+17 states, 1432639 BDD nodes
size of Y243 = 1.72085e+17 states, 1439269 BDD nodes
size of Y244 = 1.73184e+17 states, 1446142 BDD nodes
size of Y245 = 1.74287e+17 states, 1453945 BDD nodes
size of Y246 = 1.75394e+17 states, 1459825 BDD nodes
size of Y247 = 1.76505e+17 states, 1466276 BDD nodes
size of Y248 = 1.7762e+17 states, 1472813 BDD nodes
size of Y249 = 1.78739e+17 states, 1480570 BDD nodes
size of Y250 = 1.79862e+17 states, 1486413 BDD nodes
size of Y251 = 1.80989e+17 states, 1492911 BDD nodes
size of Y252 = 1.8212e+17 states, 1499411 BDD nodes
size of Y253 = 1.83255e+17 states, 1507358 BDD nodes
size of Y254 = 1.84394e+17 states, 1513170 BDD nodes
size of Y255 = 1.85536e+17 states, 1519545 BDD nodes
size of Y256 = 1.86683e+17 states, 1526092 BDD nodes
size of Y257 = 1.87834e+17 states, 1533960 BDD nodes
size of Y258 = 1.88989e+17 states, 1539695 BDD nodes
size of Y259 = 1.90148e+17 states, 1546209 BDD nodes
size of Y260 = 1.9131e+17 states, 1552887 BDD nodes
size of Y261 = 1.92477e+17 states, 1560708 BDD nodes
size of Y262 = 1.93648e+17 states, 1566501 BDD nodes
size of Y263 = 1.94822e+17 states, 1572903 BDD nodes
size of Y264 = 1.96001e+17 states, 1579397 BDD nodes
size of Y265 = 1.97184e+17 states, 1587175 BDD nodes
size of Y266 = 1.9837e+17 states, 1592899 BDD nodes
size of Y267 = 1.99561e+17 states, 1599274 BDD nodes
size of Y268 = 2.00756e+17 states, 1605625 BDD nodes
size of Y269 = 2.01954e+17 states, 1613592 BDD nodes
size of Y270 = 2.03157e+17 states, 1619187 BDD nodes
size of Y271 = 2.04363e+17 states, 1625365 BDD nodes
size of Y272 = 2.05574e+17 states, 1631781 BDD nodes
size of Y273 = 2.06788e+17 states, 1639598 BDD nodes
size of Y274 = 2.08007e+17 states, 1645098 BDD nodes
size of Y275 = 2.09229e+17 states, 1651441 BDD nodes
size of Y276 = 2.10455e+17 states, 1658016 BDD nodes
size of Y277 = 2.11686e+17 states, 1665762 BDD nodes
size of Y278 = 2.1292e+17 states, 1671345 BDD nodes
size of Y279 = 2.14159e+17 states, 1677575 BDD nodes
size of Y280 = 2.15401e+17 states, 1683907 BDD nodes
size of Y281 = 2.16647e+17 states, 1691621 BDD nodes
size of Y282 = 2.17898e+17 states, 1697159 BDD nodes
size of Y283 = 2.19152e+17 states, 1703459 BDD nodes
size of Y284 = 2.2041e+17 states, 1709745 BDD nodes
size of Y285 = 2.21672e+17 states, 1717670 BDD nodes
size of Y286 = 2.22939e+17 states, 1723190 BDD nodes
size of Y287 = 2.24209e+17 states, 1729351 BDD nodes
size of Y288 = 2.25483e+17 states, 1735721 BDD nodes
size of Y289 = 2.26761e+17 states, 1743572 BDD nodes
size of Y290 = 2.28043e+17 states, 1748996 BDD nodes
size of Y291 = 2.29329e+17 states, 1755316 BDD nodes
size of Y292 = 2.3062e+17 states, 1761829 BDD nodes
size of Y293 = 2.31914e+17 states, 1769618 BDD nodes
size of Y294 = 2.33212e+17 states, 1775146 BDD nodes
size of Y295 = 2.34514e+17 states, 1781361 BDD nodes
size of Y296 = 2.3582e+17 states, 1787684 BDD nodes
size of Y297 = 2.3713e+17 states, 1795467 BDD nodes
size of Y298 = 2.38444e+17 states, 1800945 BDD nodes
size of Y299 = 2.39762e+17 states, 1807196 BDD nodes
size of Y300 = 2.41084e+17 states, 1813392 BDD nodes
size of Y301 = 2.4241e+17 states, 1821490 BDD nodes
size of Y302 = 2.43739e+17 states, 1826906 BDD nodes
size of Y303 = 2.45073e+17 states, 1832981 BDD nodes
size of Y304 = 2.46411e+17 states, 1839372 BDD nodes
size of Y305 = 2.47753e+17 states, 1847345 BDD nodes
size of Y306 = 2.49099e+17 states, 1852693 BDD nodes
size of Y307 = 2.50449e+17 states, 1859012 BDD nodes
size of Y308 = 2.51803e+17 states, 1865629 BDD nodes
size of Y309 = 2.5316e+17 states, 1873514 BDD nodes
size of Y310 = 2.54522e+17 states, 1878989 BDD nodes
size of Y311 = 2.55888e+17 states, 1885186 BDD nodes
size of Y312 = 2.57257e+17 states, 1891498 BDD nodes
size of Y313 = 2.58631e+17 states, 1899357 BDD nodes
size of Y314 = 2.60009e+17 states, 1904777 BDD nodes
size of Y315 = 2.6139e+17 states, 1911050 BDD nodes
size of Y316 = 2.62776e+17 states, 1917306 BDD nodes
size of Y317 = 2.64166e+17 states, 1925389 BDD nodes
size of Y318 = 2.65559e+17 states, 1930791 BDD nodes
size of Y319 = 2.66957e+17 states, 1936902 BDD nodes
size of Y320 = 2.68358e+17 states, 1943255 BDD nodes
size of Y321 = 2.69764e+17 states, 1951250 BDD nodes
size of Y322 = 2.71173e+17 states, 1956550 BDD nodes
size of Y323 = 2.72587e+17 states, 1962852 BDD nodes
size of Y324 = 2.74004e+17 states, 1969361 BDD nodes
size of Y325 = 2.75426e+17 states, 1977303 BDD nodes
size of Y326 = 2.76851e+17 states, 1982722 BDD nodes
size of Y327 = 2.78281e+17 states, 1988904 BDD nodes
size of Y328 = 2.79714e+17 states, 1995208 BDD nodes
size of Y329 = 2.81152e+17 states, 2003134 BDD nodes
size of Y330 = 2.82593e+17 states, 2008495 BDD nodes
size of Y331 = 2.84038e+17 states, 2014732 BDD nodes
size of Y332 = 2.85488e+17 states, 2020917 BDD nodes
size of Y333 = 2.86941e+17 states, 2029141 BDD nodes
size of Y334 = 2.88398e+17 states, 2034458 BDD nodes
size of Y335 = 2.89859e+17 states, 2040514 BDD nodes
size of Y336 = 2.91325e+17 states, 2046882 BDD nodes
size of Y337 = 2.92794e+17 states, 2054993 BDD nodes
size of Y338 = 2.94267e+17 states, 2060227 BDD nodes
size of Y339 = 2.95744e+17 states, 2066528 BDD nodes
size of Y340 = 2.97225e+17 states, 2073111 BDD nodes
size of Y341 = 2.9871e+17 states, 2081142 BDD nodes
size of Y342 = 3.002e+17 states, 2086511 BDD nodes
size of Y343 = 3.01693e+17 states, 2092681 BDD nodes
size of Y344 = 3.0319e+17 states, 2098980 BDD nodes
size of Y345 = 3.04691e+17 states, 2106990 BDD nodes
size of Y346 = 3.06196e+17 states, 2112300 BDD nodes
size of Y347 = 3.07705e+17 states, 2118564 BDD nodes
size of Y348 = 3.09218e+17 states, 2124796 BDD nodes
size of Y349 = 3.10735e+17 states, 2133046 BDD nodes
size of Y350 = 3.12256e+17 states, 2138345 BDD nodes
size of Y351 = 3.13781e+17 states, 2144432 BDD nodes
size of Y352 = 3.1531e+17 states, 2150775 BDD nodes
size of Y353 = 3.16843e+17 states, 2158934 BDD nodes
size of Y354 = 3.18379e+17 states, 2164108 BDD nodes
size of Y355 = 3.1992e+17 states, 2170394 BDD nodes
size of Y356 = 3.21465e+17 states, 2176899 BDD nodes
size of Y357 = 3.23014e+17 states, 2184971 BDD nodes
size of Y358 = 3.24567e+17 states, 2190277 BDD nodes
size of Y359 = 3.26124e+17 states, 2196422 BDD nodes
size of Y360 = 3.27684e+17 states, 2202703 BDD nodes
size of Y361 = 3.29249e+17 states, 2210772 BDD nodes
size of Y362 = 3.30818e+17 states, 2216012 BDD nodes
size of Y363 = 3.3239e+17 states, 2222204 BDD nodes
size of Y364 = 3.34036e+17 states, 2228314 BDD nodes
size of Y365 = 3.36122e+17 states, 2236786 BDD nodes
size of Y366 = 3.38354e+17 states, 2241953 BDD nodes
size of Y367 = 3.40663e+17 states, 2247921 BDD nodes
size of Y368 = 3.43137e+17 states, 2254297 BDD nodes
size of Y369 = 3.4578e+17 states, 2262603 BDD nodes
size of Y370 = 3.48507e+17 states, 2267678 BDD nodes
size of Y371 = 3.51267e+17 states, 2273965 BDD nodes
size of Y372 = 3.54061e+17 states, 2280634 BDD nodes
size of Y373 = 3.56876e+17 states, 2288802 BDD nodes
size of Y374 = 3.59711e+17 states, 2294056 BDD nodes
size of Y375 = 3.62563e+17 states, 2300188 BDD nodes
size of Y376 = 3.65431e+17 states, 2306462 BDD nodes
size of Y377 = 3.68318e+17 states, 2314612 BDD nodes
size of Y378 = 3.71221e+17 states, 2319800 BDD nodes
size of Y379 = 3.74138e+17 states, 2326023 BDD nodes
size of Y380 = 3.77071e+17 states, 2332216 BDD nodes
size of Y381 = 3.8002e+17 states, 2340616 BDD nodes
size of Y382 = 3.82986e+17 states, 2345785 BDD nodes
size of Y383 = 3.85966e+17 states, 2351805 BDD nodes
size of Y384 = 3.8896e+17 states, 2358120 BDD nodes
size of Y385 = 3.91968e+17 states, 2366413 BDD nodes
size of Y386 = 3.94989e+17 states, 2371447 BDD nodes
size of Y387 = 3.98022e+17 states, 2377702 BDD nodes
size of Y388 = 4.01067e+17 states, 2384193 BDD nodes
size of Y389 = 4.04123e+17 states, 2392404 BDD nodes
size of Y390 = 4.0719e+17 states, 2397587 BDD nodes
size of Y391 = 4.1027e+17 states, 2403683 BDD nodes
size of Y392 = 4.1336e+17 states, 2409927 BDD nodes
size of Y393 = 4.16462e+17 states, 2418121 BDD nodes
size of Y394 = 4.19576e+17 states, 2423226 BDD nodes
size of Y395 = 4.22701e+17 states, 2429393 BDD nodes
size of Y396 = 4.25837e+17 states, 2435484 BDD nodes
size of Y397 = 4.28985e+17 states, 2444022 BDD nodes
size of Y398 = 4.32144e+17 states, 2449080 BDD nodes
size of Y399 = 4.35315e+17 states, 2455017 BDD nodes
size of Y400 = 4.38497e+17 states, 2461333 BDD nodes
size of Y401 = 4.4169e+17 states, 2469732 BDD nodes
size of Y402 = 4.44895e+17 states, 2474684 BDD nodes
size of Y403 = 4.48111e+17 states, 2480924 BDD nodes
size of Y404 = 4.51339e+17 states, 2487488 BDD nodes
size of Y405 = 4.54578e+17 states, 2495779 BDD nodes
size of Y406 = 4.57828e+17 states, 2500904 BDD nodes
size of Y407 = 4.6109e+17 states, 2506982 BDD nodes
size of Y408 = 4.64364e+17 states, 2513217 BDD nodes
size of Y409 = 4.67648e+17 states, 2521491 BDD nodes
size of Y410 = 4.70944e+17 states, 2526541 BDD nodes
size of Y411 = 4.74252e+17 states, 2532733 BDD nodes
size of Y412 = 4.77571e+17 states, 2538879 BDD nodes
size of Y413 = 4.809e+17 states, 2547425 BDD nodes
size of Y414 = 4.84238e+17 states, 2552469 BDD nodes
size of Y415 = 4.87586e+17 states, 2558442 BDD nodes
size of Y416 = 4.90943e+17 states, 2564733 BDD nodes
size of Y417 = 4.94309e+17 states, 2573179 BDD nodes
size of Y418 = 4.97683e+17 states, 2578058 BDD nodes
size of Y419 = 5.01065e+17 states, 2584286 BDD nodes
size of Y420 = 5.04455e+17 states, 2590763 BDD nodes
size of Y421 = 5.07854e+17 states, 2599086 BDD nodes
size of Y422 = 5.1126e+17 states, 2604158 BDD nodes
size of Y423 = 5.14675e+17 states, 2610221 BDD nodes
size of Y424 = 5.18098e+17 states, 2616448 BDD nodes
size of Y425 = 5.21529e+17 states, 2624791 BDD nodes
size of Y426 = 5.24968e+17 states, 2629781 BDD nodes
size of Y427 = 5.28416e+17 states, 2635915 BDD nodes
size of Y428 = 5.31871e+17 states, 2641932 BDD nodes
size of Y429 = 5.35335e+17 states, 2650689 BDD nodes
size of Y430 = 5.38807e+17 states, 2655612 BDD nodes
size of Y431 = 5.42286e+17 states, 2661466 BDD nodes
size of Y432 = 5.45774e+17 states, 2667789 BDD nodes
size of Y433 = 5.49269e+17 states, 2676378 BDD nodes
size of Y434 = 5.52773e+17 states, 2681190 BDD nodes
size of Y435 = 5.56285e+17 states, 2687420 BDD nodes
size of Y436 = 5.59804e+17 states, 2694046 BDD nodes
size of Y437 = 5.63332e+17 states, 2702483 BDD nodes
size of Y438 = 5.66867e+17 states, 2707502 BDD nodes
size of Y439 = 5.70411e+17 states, 2713547 BDD nodes
size of Y440 = 5.73962e+17 states, 2719763 BDD nodes
size of Y441 = 5.77522e+17 states, 2728182 BDD nodes
size of Y442 = 5.81089e+17 states, 2733114 BDD nodes
size of Y443 = 5.84665e+17 states, 2739279 BDD nodes
size of Y444 = 5.88248e+17 states, 2745395 BDD nodes
size of Y445 = 5.9184e+17 states, 2754098 BDD nodes
size of Y446 = 5.95439e+17 states, 2759024 BDD nodes
size of Y447 = 5.99047e+17 states, 2764947 BDD nodes
size of Y448 = 6.02662e+17 states, 2771220 BDD nodes
size of Y449 = 6.06285e+17 states, 2779807 BDD nodes
size of Y450 = 6.09917e+17 states, 2784573 BDD nodes
size of Y451 = 6.13556e+17 states, 2790783 BDD nodes
size of Y452 = 6.17203e+17 states, 2797256 BDD nodes
size of Y453 = 6.20859e+17 states, 2805742 BDD nodes
size of Y454 = 6.24522e+17 states, 2810705 BDD nodes
size of Y455 = 6.28193e+17 states, 2816735 BDD nodes
size of Y456 = 6.31873e+17 states, 2822943 BDD nodes
size of Y457 = 6.3556e+17 states, 2831429 BDD nodes
size of Y458 = 6.39255e+17 states, 2836302 BDD nodes
size of Y459 = 6.42959e+17 states, 2842425 BDD nodes
size of Y460 = 6.4667e+17 states, 2848448 BDD nodes
size of Y461 = 6.50389e+17 states, 2857322 BDD nodes
size of Y462 = 6.54116e+17 states, 2862150 BDD nodes
size of Y463 = 6.57852e+17 states, 2867997 BDD nodes
size of Y464 = 6.61595e+17 states, 2874290 BDD nodes
size of Y465 = 6.65346e+17 states, 2883006 BDD nodes
size of Y466 = 6.69105e+17 states, 2887705 BDD nodes
size of Y467 = 6.72872e+17 states, 2893913 BDD nodes
size of Y468 = 6.76647e+17 states, 2900487 BDD nodes
size of Y469 = 6.8043e+17 states, 2909067 BDD nodes
size of Y470 = 6.84222e+17 states, 2913977 BDD nodes
size of Y471 = 6.88021e+17 states, 2919992 BDD nodes
size of Y472 = 6.91828e+17 states, 2926192 BDD nodes
size of Y473 = 6.95643e+17 states, 2934759 BDD nodes
size of Y474 = 6.99374e+17 states, 2939925 BDD nodes
size of Y475 = 7.02529e+17 states, 2947700 BDD nodes
size of Y476 = 7.05505e+17 states, 2953803 BDD nodes
size of Y477 = 7.08392e+17 states, 2962538 BDD nodes
size of Y478 = 7.11075e+17 states, 2968114 BDD nodes
size of Y479 = 7.13548e+17 states, 2976211 BDD nodes
size of Y480 = 7.15923e+17 states, 2981551 BDD nodes
size of Y481 = 7.18269e+17 states, 2989724 BDD nodes
size of Y482 = 7.20588e+17 states, 2995617 BDD nodes
size of Y483 = 7.22893e+17 states, 3003817 BDD nodes
size of Y484 = 7.25187e+17 states, 3009493 BDD nodes
size of Y485 = 7.27475e+17 states, 3017490 BDD nodes
size of Y486 = 7.29757e+17 states, 3023220 BDD nodes
size of Y487 = 7.32029e+17 states, 3031178 BDD nodes
size of Y488 = 7.34295e+17 states, 3036507 BDD nodes
size of Y489 = 7.36558e+17 states, 3044497 BDD nodes
size of Y490 = 7.38817e+17 states, 3050026 BDD nodes
size of Y491 = 7.41069e+17 states, 3058274 BDD nodes
size of Y492 = 7.43315e+17 states, 3063365 BDD nodes
size of Y493 = 7.45559e+17 states, 3071780 BDD nodes
size of Y494 = 7.47798e+17 states, 3077404 BDD nodes
size of Y495 = 7.50035e+17 states, 3085307 BDD nodes
size of Y496 = 7.5227e+17 states, 3090639 BDD nodes
size of Y497 = 7.54505e+17 states, 3098936 BDD nodes
size of Y498 = 7.56741e+17 states, 3104576 BDD nodes
size of Y499 = 7.58977e+17 states, 3112827 BDD nodes
size of Y500 = 7.61213e+17 states, 3118595 BDD nodes
size of Y501 = 7.6345e+17 states, 3126638 BDD nodes
size of Y502 = 7.65687e+17 states, 3132345 BDD nodes
size of Y503 = 7.67925e+17 states, 3140349 BDD nodes
size of Y504 = 7.70163e+17 states, 3145580 BDD nodes
size of Y505 = 7.72402e+17 states, 3153595 BDD nodes
size of Y506 = 7.74641e+17 states, 3159025 BDD nodes
size of Y507 = 7.76881e+17 states, 3167472 BDD nodes
size of Y508 = 7.79121e+17 states, 3172596 BDD nodes
size of Y509 = 7.81362e+17 states, 3180843 BDD nodes
size of Y510 = 7.83603e+17 states, 3186522 BDD nodes
size of Y511 = 7.85845e+17 states, 3194593 BDD nodes
size of Y512 = 7.88087e+17 states, 3199821 BDD nodes
size of Y513 = 7.9033e+17 states, 3208079 BDD nodes
size of Y514 = 7.92574e+17 states, 3213789 BDD nodes
size of Y515 = 7.94818e+17 states, 3222078 BDD nodes
size of Y516 = 7.97063e+17 states, 3227637 BDD nodes
size of Y517 = 7.99308e+17 states, 3235683 BDD nodes
size of Y518 = 8.01553e+17 states, 3241305 BDD nodes
size of Y519 = 8.038e+17 states, 3249290 BDD nodes
size of Y520 = 8.06046e+17 states, 3254468 BDD nodes
size of Y521 = 8.08294e+17 states, 3262513 BDD nodes
size of Y522 = 8.10542e+17 states, 3267867 BDD nodes
size of Y523 = 8.12792e+17 states, 3276132 BDD nodes
size of Y524 = 8.15044e+17 states, 3281040 BDD nodes
size of Y525 = 8.17298e+17 states, 3289328 BDD nodes
size of Y526 = 8.19556e+17 states, 3294759 BDD nodes
size of Y527 = 8.21817e+17 states, 3302616 BDD nodes
size of Y528 = 8.24081e+17 states, 3307703 BDD nodes
size of Y529 = 8.2635e+17 states, 3315921 BDD nodes
size of Y530 = 8.28622e+17 states, 3321303 BDD nodes
size of Y531 = 8.30897e+17 states, 3328943 BDD nodes
size of Y532 = 8.33177e+17 states, 3334258 BDD nodes
size of Y533 = 8.3546e+17 states, 3342241 BDD nodes
size of Y534 = 8.37747e+17 states, 3347624 BDD nodes
size of Y535 = 8.40038e+17 states, 3355145 BDD nodes
size of Y536 = 8.42333e+17 states, 3359876 BDD nodes
size of Y537 = 8.44631e+17 states, 3367836 BDD nodes
size of Y538 = 8.46933e+17 states, 3372969 BDD nodes
size of Y539 = 8.49239e+17 states, 3380928 BDD nodes
size of Y540 = 8.51549e+17 states, 3385644 BDD nodes
size of Y541 = 8.53863e+17 states, 3393336 BDD nodes
size of Y542 = 8.5618e+17 states, 3398576 BDD nodes
size of Y543 = 8.58502e+17 states, 3406224 BDD nodes
size of Y544 = 8.60827e+17 states, 3410818 BDD nodes
size of Y545 = 8.63157e+17 states, 3418750 BDD nodes
size of Y546 = 8.65491e+17 states, 3423941 BDD nodes
size of Y547 = 8.67828e+17 states, 3431609 BDD nodes
size of Y548 = 8.70169e+17 states, 3436818 BDD nodes
size of Y549 = 8.72515e+17 states, 3444411 BDD nodes
size of Y550 = 8.74864e+17 states, 3449580 BDD nodes
size of Y551 = 8.77217e+17 states, 3457086 BDD nodes
size of Y552 = 8.79575e+17 states, 3461750 BDD nodes
size of Y553 = 8.81936e+17 states, 3469487 BDD nodes
size of Y554 = 8.84301e+17 states, 3474222 BDD nodes
size of Y555 = 8.8667e+17 states, 3481940 BDD nodes
size of Y556 = 8.89043e+17 states, 3486521 BDD nodes
size of Y557 = 8.9142e+17 states, 3494504 BDD nodes
size of Y558 = 8.93801e+17 states, 3499538 BDD nodes
size of Y559 = 8.96186e+17 states, 3506940 BDD nodes
size of Y560 = 8.98575e+17 states, 3511584 BDD nodes
size of Y561 = 9.00967e+17 states, 3519666 BDD nodes
size of Y562 = 9.03364e+17 states, 3524608 BDD nodes
size of Y563 = 9.05765e+17 states, 3532226 BDD nodes
size of Y564 = 9.0817e+17 states, 3537587 BDD nodes
size of Y565 = 9.10578e+17 states, 3545301 BDD nodes
size of Y566 = 9.12991e+17 states, 3550418 BDD nodes
size of Y567 = 9.15407e+17 states, 3557905 BDD nodes
size of Y568 = 9.17828e+17 states, 3562564 BDD nodes
size of Y569 = 9.20252e+17 states, 3570365 BDD nodes
size of Y570 = 9.22681e+17 states, 3575030 BDD nodes
size of Y571 = 9.25113e+17 states, 3582907 BDD nodes
size of Y572 = 9.27549e+17 states, 3587627 BDD nodes
size of Y573 = 9.2999e+17 states, 3595517 BDD nodes
size of Y574 = 9.32434e+17 states, 3600630 BDD nodes
size of Y575 = 9.34882e+17 states, 3608192 BDD nodes
size of Y576 = 9.37334e+17 states, 3612791 BDD nodes
size of Y577 = 9.3979e+17 states, 3620860 BDD nodes
size of Y578 = 9.4225e+17 states, 3625896 BDD nodes
size of Y579 = 9.44714e+17 states, 3633526 BDD nodes
size of Y580 = 9.47182e+17 states, 3638742 BDD nodes
size of Y581 = 9.49654e+17 states, 3646497 BDD nodes
size of Y582 = 9.5213e+17 states, 3651565 BDD nodes
size of Y583 = 9.5461e+17 states, 3659044 BDD nodes
size of Y584 = 9.57093e+17 states, 3663698 BDD nodes
size of Y585 = 9.59581e+17 states, 3671570 BDD nodes
size of Y586 = 9.62073e+17 states, 3676197 BDD nodes
size of Y587 = 9.64569e+17 states, 3683890 BDD nodes
size of Y588 = 9.67068e+17 states, 3688484 BDD nodes
size of Y589 = 9.69572e+17 states, 3696569 BDD nodes
size of Y590 = 9.72079e+17 states, 3701521 BDD nodes
size of Y591 = 9.74591e+17 states, 3708924 BDD nodes
size of Y592 = 9.77106e+17 states, 3713525 BDD nodes
size of Y593 = 9.79625e+17 states, 3721722 BDD nodes
size of Y594 = 9.82149e+17 states, 3726573 BDD nodes
size of Y595 = 9.84676e+17 states, 3734139 BDD nodes
size of Y596 = 9.87207e+17 states, 3739449 BDD nodes
size of Y597 = 9.89743e+17 states, 3747306 BDD nodes
size of Y598 = 9.92282e+17 states, 3752328 BDD nodes
size of Y599 = 9.94825e+17 states, 3759797 BDD nodes
size of Y600 = 9.97372e+17 states, 3764449 BDD nodes
size of Y601 = 9.99923e+17 states, 3772370 BDD nodes
size of Y602 = 1.00248e+18 states, 3776873 BDD nodes
size of Y603 = 1.00504e+18 states, 3784774 BDD nodes
size of Y604 = 1.0076e+18 states, 3789452 BDD nodes
size of Y605 = 1.01017e+18 states, 3797460 BDD nodes
size of Y606 = 1.01274e+18 states, 3802494 BDD nodes
size of Y607 = 1.01531e+18 states, 3810076 BDD nodes
size of Y608 = 1.01789e+18 states, 3814645 BDD nodes
size of Y609 = 1.02047e+18 states, 3822868 BDD nodes
size of Y610 = 1.02306e+18 states, 3827848 BDD nodes
size of Y611 = 1.02565e+18 states, 3835445 BDD nodes
size of Y612 = 1.02825e+18 states, 3840668 BDD nodes
size of Y613 = 1.03084e+18 states, 3848542 BDD nodes
size of Y614 = 1.03345e+18 states, 3853515 BDD nodes
size of Y615 = 1.03605e+18 states, 3860972 BDD nodes
size of Y616 = 1.03866e+18 states, 3865608 BDD nodes
size of Y617 = 1.04128e+18 states, 3873617 BDD nodes
size of Y618 = 1.0439e+18 states, 3878135 BDD nodes
size of Y619 = 1.04652e+18 states, 3885771 BDD nodes
size of Y620 = 1.04914e+18 states, 3890295 BDD nodes
size of Y621 = 1.05178e+18 states, 3898664 BDD nodes
size of Y622 = 1.05441e+18 states, 3903469 BDD nodes
size of Y623 = 1.05705e+18 states, 3910768 BDD nodes
size of Y624 = 1.05969e+18 states, 3915407 BDD nodes
size of Y625 = 1.06234e+18 states, 3923820 BDD nodes
size of Y626 = 1.06499e+18 states, 3928506 BDD nodes
size of Y627 = 1.06764e+18 states, 3936056 BDD nodes
size of Y628 = 1.0703e+18 states, 3941506 BDD nodes
size of Y629 = 1.07296e+18 states, 3949486 BDD nodes
size of Y630 = 1.07563e+18 states, 3954400 BDD nodes
size of Y631 = 1.0783e+18 states, 3961832 BDD nodes
size of Y632 = 1.08097e+18 states, 3966448 BDD nodes
size of Y633 = 1.08365e+18 states, 3974516 BDD nodes
size of Y634 = 1.08633e+18 states, 3978950 BDD nodes
size of Y635 = 1.08901e+18 states, 3986744 BDD nodes
size of Y636 = 1.0917e+18 states, 3991412 BDD nodes
size of Y637 = 1.0944e+18 states, 3999586 BDD nodes
size of Y638 = 1.09709e+18 states, 4004475 BDD nodes
size of Y639 = 1.0998e+18 states, 4011936 BDD nodes
size of Y640 = 1.1025e+18 states, 4016475 BDD nodes
size of Y641 = 1.10521e+18 states, 4024817 BDD nodes
size of Y642 = 1.10792e+18 states, 4029587 BDD nodes
size of Y643 = 1.11064e+18 states, 4037126 BDD nodes
size of Y644 = 1.11336e+18 states, 4042329 BDD nodes
size of Y645 = 1.11609e+18 states, 4050321 BDD nodes
size of Y646 = 1.11882e+18 states, 4055158 BDD nodes
size of Y647 = 1.12155e+18 states, 4062539 BDD nodes
size of Y648 = 1.12429e+18 states, 4067117 BDD nodes
size of Y649 = 1.12703e+18 states, 4075234 BDD nodes
size of Y650 = 1.12978e+18 states, 4079583 BDD nodes
size of Y651 = 1.13253e+18 states, 4087160 BDD nodes
size of Y652 = 1.13528e+18 states, 4091673 BDD nodes
size of Y653 = 1.13804e+18 states, 4100040 BDD nodes
size of Y654 = 1.1408e+18 states, 4104736 BDD nodes
size of Y655 = 1.14356e+18 states, 4111976 BDD nodes
size of Y656 = 1.14633e+18 states, 4116495 BDD nodes
size of Y657 = 1.14911e+18 states, 4124977 BDD nodes
size of Y658 = 1.15188e+18 states, 4129518 BDD nodes
size of Y659 = 1.15466e+18 states, 4136956 BDD nodes
size of Y660 = 1.15745e+18 states, 4142266 BDD nodes
size of Y661 = 1.16024e+18 states, 4150355 BDD nodes
size of Y662 = 1.16303e+18 states, 4155140 BDD nodes
size of Y663 = 1.16583e+18 states, 4162472 BDD nodes
size of Y664 = 1.16863e+18 states, 4167052 BDD nodes
size of Y665 = 1.17143e+18 states, 4175250 BDD nodes
size of Y666 = 1.17424e+18 states, 4179464 BDD nodes
size of Y667 = 1.17706e+18 states, 4187232 BDD nodes
size of Y668 = 1.17987e+18 states, 4191860 BDD nodes
size of Y669 = 1.18269e+18 states, 4200132 BDD nodes
size of Y670 = 1.18552e+18 states, 4204908 BDD nodes
size of Y671 = 1.18835e+18 states, 4212312 BDD nodes
size of Y672 = 1.19118e+18 states, 4216823 BDD nodes
size of Y673 = 1.19402e+18 states, 4225338 BDD nodes
size of Y674 = 1.19686e+18 states, 4229967 BDD nodes
size of Y675 = 1.1997e+18 states, 4237456 BDD nodes
size of Y676 = 1.20255e+18 states, 4242666 BDD nodes
size of Y677 = 1.2054e+18 states, 4250758 BDD nodes
size of Y678 = 1.20826e+18 states, 4255490 BDD nodes
size of Y679 = 1.21112e+18 states, 4262807 BDD nodes
size of Y680 = 1.21399e+18 states, 4267379 BDD nodes
size of Y681 = 1.21686e+18 states, 4275665 BDD nodes
size of Y682 = 1.21973e+18 states, 4279892 BDD nodes
size of Y683 = 1.22261e+18 states, 4287424 BDD nodes
size of Y684 = 1.22549e+18 states, 4291869 BDD nodes
size of Y685 = 1.22837e+18 states, 4300481 BDD nodes
size of Y686 = 1.23126e+18 states, 4305040 BDD nodes
size of Y687 = 1.23415e+18 states, 4312171 BDD nodes
size of Y688 = 1.23705e+18 states, 4316742 BDD nodes
size of Y689 = 1.23995e+18 states, 4325433 BDD nodes
size of Y690 = 1.24285e+18 states, 4329825 BDD nodes
size of Y691 = 1.24576e+18 states, 4337276 BDD nodes
size of Y692 = 1.24867e+18 states, 4342680 BDD nodes
size of Y693 = 1.25159e+18 states, 4350915 BDD nodes
size of Y694 = 1.25451e+18 states, 4355594 BDD nodes
size of Y695 = 1.25744e+18 states, 4362893 BDD nodes
size of Y696 = 1.26036e+18 states, 4367454 BDD nodes
size of Y697 = 1.2633e+18 states, 4375808 BDD nodes
size of Y698 = 1.26623e+18 states, 4379959 BDD nodes
size of Y699 = 1.26917e+18 states, 4387664 BDD nodes
size of Y700 = 1.27212e+18 states, 4392281 BDD nodes
size of Y701 = 1.27507e+18 states, 4400751 BDD nodes
size of Y702 = 1.27802e+18 states, 4405398 BDD nodes
size of Y703 = 1.28097e+18 states, 4412722 BDD nodes
size of Y704 = 1.28394e+18 states, 4417230 BDD nodes
size of Y705 = 1.2869e+18 states, 4425886 BDD nodes
size of Y706 = 1.28987e+18 states, 4430367 BDD nodes
size of Y707 = 1.29284e+18 states, 4437838 BDD nodes
size of Y708 = 1.29582e+18 states, 4443044 BDD nodes
size of Y709 = 1.2988e+18 states, 4451312 BDD nodes
size of Y710 = 1.30178e+18 states, 4455935 BDD nodes
size of Y711 = 1.30477e+18 states, 4463219 BDD nodes
size of Y712 = 1.30776e+18 states, 4467772 BDD nodes
size of Y713 = 1.31076e+18 states, 4476201 BDD nodes
size of Y714 = 1.31376e+18 states, 4480311 BDD nodes
size of Y715 = 1.31676e+18 states, 4487834 BDD nodes
size of Y716 = 1.31977e+18 states, 4492295 BDD nodes
size of Y717 = 1.32278e+18 states, 4500998 BDD nodes
size of Y718 = 1.3258e+18 states, 4505467 BDD nodes
size of Y719 = 1.32882e+18 states, 4512610 BDD nodes
size of Y720 = 1.33184e+18 states, 4517120 BDD nodes
size of Y721 = 1.33487e+18 states, 4525922 BDD nodes
size of Y722 = 1.3379e+18 states, 4530209 BDD nodes
size of Y723 = 1.34094e+18 states, 4537621 BDD nodes
size of Y724 = 1.34398e+18 states, 4542943 BDD nodes
size of Y725 = 1.34702e+18 states, 4551321 BDD nodes
size of Y726 = 1.35007e+18 states, 4555891 BDD nodes
size of Y727 = 1.35312e+18 states, 4563160 BDD nodes
size of Y728 = 1.35618e+18 states, 4567705 BDD nodes
size of Y729 = 1.35924e+18 states, 4576189 BDD nodes
size of Y730 = 1.3623e+18 states, 4580166 BDD nodes
size of Y731 = 1.36537e+18 states, 4587922 BDD nodes
size of Y732 = 1.36844e+18 states, 4592480 BDD nodes
size of Y733 = 1.37151e+18 states, 4601067 BDD nodes
size of Y734 = 1.37459e+18 states, 4605632 BDD nodes
size of Y735 = 1.37768e+18 states, 4612987 BDD nodes
size of Y736 = 1.38077e+18 states, 4617459 BDD nodes
size of Y737 = 1.38386e+18 states, 4626280 BDD nodes
size of Y738 = 1.38695e+18 states, 4630706 BDD nodes
size of Y739 = 1.39005e+18 states, 4638162 BDD nodes
size of Y740 = 1.39316e+18 states, 4643367 BDD nodes
size of Y741 = 1.39626e+18 states, 4651758 BDD nodes
size of Y742 = 1.39937e+18 states, 4656275 BDD nodes
size of Y743 = 1.40249e+18 states, 4663529 BDD nodes
size of Y744 = 1.40561e+18 states, 4668066 BDD nodes
size of Y745 = 1.40873e+18 states, 4676645 BDD nodes
size of Y746 = 1.41186e+18 states, 4680641 BDD nodes
size of Y747 = 1.41499e+18 states, 4688122 BDD nodes
size of Y748 = 1.41813e+18 states, 4692503 BDD nodes
size of Y749 = 1.42127e+18 states, 4701505 BDD nodes
size of Y750 = 1.42441e+18 states, 4705822 BDD nodes
size of Y751 = 1.42756e+18 states, 4712863 BDD nodes
size of Y752 = 1.43071e+18 states, 4717432 BDD nodes
size of Y753 = 1.43386e+18 states, 4726470 BDD nodes
size of Y754 = 1.43702e+18 states, 4730594 BDD nodes
size of Y755 = 1.44019e+18 states, 4738019 BDD nodes
size of Y756 = 1.44335e+18 states, 4743493 BDD nodes
size of Y757 = 1.44653e+18 states, 4752017 BDD nodes
size of Y758 = 1.4497e+18 states, 4756481 BDD nodes
size of Y759 = 1.45288e+18 states, 4763720 BDD nodes
size of Y760 = 1.45606e+18 states, 4768249 BDD nodes
size of Y761 = 1.45925e+18 states, 4776899 BDD nodes
size of Y762 = 1.46244e+18 states, 4780822 BDD nodes
size of Y763 = 1.46564e+18 states, 4788489 BDD nodes
size of Y764 = 1.46884e+18 states, 4793052 BDD nodes
size of Y765 = 1.47204e+18 states, 4801848 BDD nodes
size of Y766 = 1.47525e+18 states, 4806273 BDD nodes
size of Y767 = 1.47846e+18 states, 4813519 BDD nodes
size of Y768 = 1.48167e+18 states, 4818003 BDD nodes
size of Y769 = 1.48489e+18 states, 4826971 BDD nodes
size of Y770 = 1.48811e+18 states, 4831201 BDD nodes
size of Y771 = 1.49134e+18 states, 4838642 BDD nodes
size of Y772 = 1.49457e+18 states, 4843846 BDD nodes
size of Y773 = 1.49781e+18 states, 4852402 BDD nodes
size of Y774 = 1.50104e+18 states, 4856813 BDD nodes
size of Y775 = 1.50429e+18 states, 4864037 BDD nodes
size of Y776 = 1.50753e+18 states, 4868558 BDD nodes
size of Y777 = 1.51079e+18 states, 4877283 BDD nodes
size of Y778 = 1.51404e+18 states, 4881165 BDD nodes
size of Y779 = 1.5173e+18 states, 4888647 BDD nodes
size of Y780 = 1.52056e+18 states, 4893043 BDD nodes
size of Y781 = 1.52383e+18 states, 4902085 BDD nodes
size of Y782 = 1.5271e+18 states, 4906327 BDD nodes
size of Y783 = 1.53037e+18 states, 4913383 BDD nodes
size of Y784 = 1.53365e+18 states, 4917860 BDD nodes
size of Y785 = 1.53694e+18 states, 4926982 BDD nodes
size of Y786 = 1.54022e+18 states, 4931019 BDD nodes
size of Y787 = 1.54351e+18 states, 4938392 BDD nodes
size of Y788 = 1.54681e+18 states, 4943727 BDD nodes
size of Y789 = 1.55011e+18 states, 4952397 BDD nodes
size of Y790 = 1.55341e+18 states, 4956755 BDD nodes
size of Y791 = 1.55671e+18 states, 4963964 BDD nodes
size of Y792 = 1.56003e+18 states, 4968477 BDD nodes
size of Y793 = 1.56334e+18 states, 4977264 BDD nodes
size of Y794 = 1.56666e+18 states, 4981016 BDD nodes
size of Y795 = 1.56998e+18 states, 4988705 BDD nodes
size of Y796 = 1.57331e+18 states, 4993222 BDD nodes
size of Y797 = 1.57664e+18 states, 5002139 BDD nodes
size of Y798 = 1.57997e+18 states, 5006468 BDD nodes
size of Y799 = 1.58331e+18 states, 5013713 BDD nodes
size of Y800 = 1.58665e+18 states, 5018172 BDD nodes
size of Y801 = 1.59e+18 states, 5027305 BDD nodes
size of Y802 = 1.59335e+18 states, 5031427 BDD nodes
size of Y803 = 1.5967e+18 states, 5038853 BDD nodes
size of Y804 = 1.60006e+18 states, 5044056 BDD nodes
size of Y805 = 1.60342e+18 states, 5052720 BDD nodes
size of Y806 = 1.60679e+18 states, 5057025 BDD nodes
size of Y807 = 1.61016e+18 states, 5064219 BDD nodes
size of Y808 = 1.61354e+18 states, 5068724 BDD nodes
size of Y809 = 1.61691e+18 states, 5077599 BDD nodes
size of Y810 = 1.6203e+18 states, 5081367 BDD nodes
size of Y811 = 1.62368e+18 states, 5088811 BDD nodes
size of Y812 = 1.62707e+18 states, 5093115 BDD nodes
size of Y813 = 1.63047e+18 states, 5102415 BDD nodes
size of Y814 = 1.63386e+18 states, 5106513 BDD nodes
size of Y815 = 1.63727e+18 states, 5113461 BDD nodes
size of Y816 = 1.64067e+18 states, 5117993 BDD nodes
size of Y817 = 1.64408e+18 states, 5127329 BDD nodes
size of Y818 = 1.6475e+18 states, 5131214 BDD nodes
size of Y819 = 1.65091e+18 states, 5138605 BDD nodes
size of Y820 = 1.65434e+18 states, 5144047 BDD nodes
size of Y821 = 1.65776e+18 states, 5152863 BDD nodes
size of Y822 = 1.66119e+18 states, 5157115 BDD nodes
size of Y823 = 1.66463e+18 states, 5164294 BDD nodes
size of Y824 = 1.66806e+18 states, 5168791 BDD nodes
size of Y825 = 1.67151e+18 states, 5177737 BDD nodes
size of Y826 = 1.67495e+18 states, 5181432 BDD nodes
size of Y827 = 1.6784e+18 states, 5189061 BDD nodes
size of Y828 = 1.68186e+18 states, 5193570 BDD nodes
size of Y829 = 1.68531e+18 states, 5202692 BDD nodes
size of Y830 = 1.68877e+18 states, 5206895 BDD nodes
size of Y831 = 1.69224e+18 states, 5214063 BDD nodes
size of Y832 = 1.69571e+18 states, 5218523 BDD nodes
size of Y833 = 1.69918e+18 states, 5227803 BDD nodes
size of Y834 = 1.70266e+18 states, 5231782 BDD nodes
size of Y835 = 1.70614e+18 states, 5239193 BDD nodes
size of Y836 = 1.70963e+18 states, 5244395 BDD nodes
size of Y837 = 1.71312e+18 states, 5253239 BDD nodes
size of Y838 = 1.71661e+18 states, 5257438 BDD nodes
size of Y839 = 1.72011e+18 states, 5264602 BDD nodes
size of Y840 = 1.72361e+18 states, 5269091 BDD nodes
size of Y841 = 1.72712e+18 states, 5278112 BDD nodes
size of Y842 = 1.73063e+18 states, 5281766 BDD nodes
size of Y843 = 1.73414e+18 states, 5289207 BDD nodes
size of Y844 = 1.73766e+18 states, 5293538 BDD nodes
size of Y845 = 1.74118e+18 states, 5302919 BDD nodes
size of Y846 = 1.7447e+18 states, 5306934 BDD nodes
size of Y847 = 1.74823e+18 states, 5313903 BDD nodes
size of Y848 = 1.75177e+18 states, 5318373 BDD nodes
size of Y849 = 1.7553e+18 states, 5327815 BDD nodes
size of Y850 = 1.75885e+18 states, 5331602 BDD nodes
size of Y851 = 1.76239e+18 states, 5338956 BDD nodes
size of Y852 = 1.76594e+18 states, 5344304 BDD nodes
size of Y853 = 1.76949e+18 states, 5353266 BDD nodes
size of Y854 = 1.77305e+18 states, 5357412 BDD nodes
size of Y855 = 1.77661e+18 states, 5364561 BDD nodes
size of Y856 = 1.78018e+18 states, 5369042 BDD nodes
size of Y857 = 1.78375e+18 states, 5378119 BDD nodes
size of Y858 = 1.78732e+18 states, 5381640 BDD nodes
size of Y859 = 1.7909e+18 states, 5389306 BDD nodes
size of Y860 = 1.79448e+18 states, 5393759 BDD nodes
size of Y861 = 1.79806e+18 states, 5403001 BDD nodes
size of Y862 = 1.80165e+18 states, 5407114 BDD nodes
size of Y863 = 1.80525e+18 states, 5414301 BDD nodes
size of Y864 = 1.80884e+18 states, 5418728 BDD nodes
size of Y865 = 1.81244e+18 states, 5428170 BDD nodes
size of Y866 = 1.81605e+18 states, 5432071 BDD nodes
size of Y867 = 1.81966e+18 states, 5439467 BDD nodes
size of Y868 = 1.82327e+18 states, 5444668 BDD nodes
size of Y869 = 1.82689e+18 states, 5453631 BDD nodes
size of Y870 = 1.83051e+18 states, 5457724 BDD nodes
size of Y871 = 1.83413e+18 states, 5464858 BDD nodes
size of Y872 = 1.83776e+18 states, 5469331 BDD nodes
size of Y873 = 1.8414e+18 states, 5478502 BDD nodes
size of Y874 = 1.84503e+18 states, 5482042 BDD nodes
size of Y875 = 1.84867e+18 states, 5489096 BDD nodes
size of Y876 = 1.85214e+18 states, 5492009 BDD nodes
size of Y877 = 1.8545e+18 states, 5496929 BDD nodes
size of Y878 = 1.8565e+18 states, 5502302 BDD nodes
size of Y879 = 1.85832e+18 states, 5506156 BDD nodes
size of Y880 = 1.85974e+18 states, 5508687 BDD nodes
size of Y881 = 1.86076e+18 states, 5508756 BDD nodes
size of Y882 = 1.86158e+18 states, 5513754 BDD nodes
size of Y883 = 1.86235e+18 states, 5515154 BDD nodes
size of Y884 = 2.06921e+18 states, 5500348 BDD nodes
size of Y885 = 2.10694e+18 states, 5477103 BDD nodes
size of Y886 = 2.13236e+18 states, 5454203 BDD nodes
size of Y887 = 2.16699e+18 states, 5426010 BDD nodes
size of Y888 = 2.21214e+18 states, 5399131 BDD nodes
size of Y889 = 2.2407e+18 states, 5371720 BDD nodes
size of Y890 = 2.25138e+18 states, 5345565 BDD nodes
size of Y891 = 2.27281e+18 states, 5325370 BDD nodes
size of Y892 = 2.29634e+18 states, 5271362 BDD nodes
size of Y893 = 2.33595e+18 states, 5249132 BDD nodes
size of Y894 = 2.35877e+18 states, 5217509 BDD nodes
size of Y895 = 2.38362e+18 states, 5187185 BDD nodes
size of Y896 = 2.41733e+18 states, 4991903 BDD nodes
size of Y897 = 2.44204e+18 states, 4796888 BDD nodes
size of Y898 = 2.45251e+18 states, 4754901 BDD nodes
size of Y899 = 2.45978e+18 states, 4713870 BDD nodes
size of Y900 = 2.46711e+18 states, 4508629 BDD nodes
size of Y901 = 2.47039e+18 states, 4320458 BDD nodes
size of Y902 = 2.47292e+18 states, 4132110 BDD nodes
size of Y903 = 2.47559e+18 states, 3941903 BDD nodes
size of Y904 = 2.47855e+18 states, 3750420 BDD nodes
size of Y905 = 2.48076e+18 states, 3559590 BDD nodes
size of Y906 = 2.48234e+18 states, 3368105 BDD nodes
size of Y907 = 2.48405e+18 states, 3176609 BDD nodes
size of Y908 = 2.48554e+18 states, 2984062 BDD nodes
size of Y909 = 2.48687e+18 states, 2950870 BDD nodes
size of Y910 = 2.4882e+18 states, 2919728 BDD nodes
size of Y911 = 2.48953e+18 states, 2887900 BDD nodes
size of Y912 = 2.49085e+18 states, 2853894 BDD nodes
size of Y913 = 2.49218e+18 states, 2822217 BDD nodes
size of Y914 = 2.49349e+18 states, 2789095 BDD nodes
size of Y915 = 2.49481e+18 states, 2756275 BDD nodes
size of Y916 = 2.49612e+18 states, 2721669 BDD nodes
size of Y917 = 2.49743e+18 states, 2687716 BDD nodes
size of Y918 = 2.49874e+18 states, 2653959 BDD nodes
size of Y919 = 2.50004e+18 states, 2619397 BDD nodes
size of Y920 = 2.50134e+18 states, 2581383 BDD nodes
size of Y921 = 2.50264e+18 states, 2545735 BDD nodes
size of Y922 = 2.50393e+18 states, 2508468 BDD nodes
size of Y923 = 2.50522e+18 states, 2471867 BDD nodes
size of Y924 = 2.50651e+18 states, 2431644 BDD nodes
size of Y925 = 2.5078e+18 states, 2395750 BDD nodes
size of Y926 = 2.50908e+18 states, 2355041 BDD nodes
size of Y927 = 2.51036e+18 states, 2323749 BDD nodes
size of Y928 = 2.51162e+18 states, 2286423 BDD nodes
size of Y929 = 2.51282e+18 states, 2253039 BDD nodes
size of Y930 = 2.51401e+18 states, 2214012 BDD nodes
size of Y931 = 2.51518e+18 states, 2175765 BDD nodes
size of Y932 = 2.5161e+18 states, 2141205 BDD nodes
size of Y933 = 2.51696e+18 states, 2111702 BDD nodes
size of Y934 = 2.51778e+18 states, 2093769 BDD nodes
size of Y935 = 2.5191e+18 states, 2067753 BDD nodes
size of Y936 = 2.53046e+18 states, 2041559 BDD nodes
size of Y937 = 2.53242e+18 states, 2015324 BDD nodes
size of Y938 = 2.53443e+18 states, 1980958 BDD nodes
size of Y939 = 2.53662e+18 states, 1950180 BDD nodes
size of Y940 = 2.53878e+18 states, 1916858 BDD nodes
size of Y941 = 2.54043e+18 states, 1883729 BDD nodes
size of Y942 = 2.54183e+18 states, 1854540 BDD nodes
size of Y943 = 2.54349e+18 states, 1810038 BDD nodes
size of Y944 = 2.54457e+18 states, 1811051 BDD nodes
size of Y945 = 2.54597e+18 states, 1812642 BDD nodes
size of Y946 = 2.54661e+18 states, 1814109 BDD nodes
size of Y947 = 2.54776e+18 states, 1815559 BDD nodes
size of Y948 = 2.54841e+18 states, 1817026 BDD nodes
size of Y949 = 2.54905e+18 states, 1818437 BDD nodes
size of Y950 = 2.5497e+18 states, 1820063 BDD nodes
size of Y951 = 2.55034e+18 states, 1821529 BDD nodes
size of Y952 = 2.55098e+18 states, 1822822 BDD nodes
size of Y953 = 2.55163e+18 states, 1824280 BDD nodes
size of Y954 = 2.55227e+18 states, 1825775 BDD nodes
size of Y955 = 2.55291e+18 states, 1827113 BDD nodes
size of Y956 = 2.55355e+18 states, 1828389 BDD nodes
size of Y957 = 2.5542e+18 states, 1829566 BDD nodes
size of Y958 = 2.55484e+18 states, 1830981 BDD nodes
size of Y959 = 2.55548e+18 states, 1832237 BDD nodes
size of Y960 = 2.55612e+18 states, 1833299 BDD nodes
size of Y961 = 2.55676e+18 states, 1834720 BDD nodes
size of Y962 = 2.5574e+18 states, 1836101 BDD nodes
size of Y963 = 2.55804e+18 states, 1837391 BDD nodes
size of Y964 = 2.55868e+18 states, 1838641 BDD nodes
size of Y965 = 2.55932e+18 states, 1839857 BDD nodes
size of Y966 = 2.55996e+18 states, 1841259 BDD nodes
size of Y967 = 2.5606e+18 states, 1842575 BDD nodes
size of Y968 = 2.56124e+18 states, 1843740 BDD nodes
size of Y969 = 2.56188e+18 states, 1845020 BDD nodes
size of Y970 = 2.56251e+18 states, 1846316 BDD nodes
size of Y971 = 2.56315e+18 states, 1847596 BDD nodes
size of Y972 = 2.56379e+18 states, 1848752 BDD nodes
size of Y973 = 2.56443e+18 states, 1849729 BDD nodes
size of Y974 = 2.56507e+18 states, 1851275 BDD nodes
size of Y975 = 2.5657e+18 states, 1852524 BDD nodes
size of Y976 = 2.56634e+18 states, 1853616 BDD nodes
size of Y977 = 2.56698e+18 states, 1854942 BDD nodes
size of Y978 = 2.56761e+18 states, 1856230 BDD nodes
size of Y979 = 2.56825e+18 states, 1857444 BDD nodes
size of Y980 = 2.56889e+18 states, 1858590 BDD nodes
size of Y981 = 2.56952e+18 states, 1859738 BDD nodes
size of Y982 = 2.57016e+18 states, 1861025 BDD nodes
size of Y983 = 2.57079e+18 states, 1862189 BDD nodes
size of Y984 = 2.57143e+18 states, 1863248 BDD nodes
size of Y985 = 2.57206e+18 states, 1864449 BDD nodes
size of Y986 = 2.5727e+18 states, 1865665 BDD nodes
size of Y987 = 2.57333e+18 states, 1866824 BDD nodes
size of Y988 = 2.57397e+18 states, 1867924 BDD nodes
size of Y989 = 2.5746e+18 states, 1868955 BDD nodes
size of Y990 = 2.57523e+18 states, 1870228 BDD nodes
size of Y991 = 2.57587e+18 states, 1871361 BDD nodes
size of Y992 = 2.5765e+18 states, 1872314 BDD nodes
size of Y993 = 2.57713e+18 states, 1873605 BDD nodes
size of Y994 = 2.57776e+18 states, 1874802 BDD nodes
size of Y995 = 2.5784e+18 states, 1875948 BDD nodes
size of Y996 = 2.57903e+18 states, 1877021 BDD nodes
size of Y997 = 2.57966e+18 states, 1878126 BDD nodes
size of Y998 = 2.58029e+18 states, 1879355 BDD nodes
size of Y999 = 2.58092e+18 states, 1880482 BDD nodes
size of Y1000 = 2.58156e+18 states, 1881479 BDD nodes
size of Y1001 = 2.58219e+18 states, 1882628 BDD nodes
size of Y1002 = 2.58282e+18 states, 1883779 BDD nodes
size of Y1003 = 2.58345e+18 states, 1884883 BDD nodes
size of Y1004 = 2.58408e+18 states, 1885916 BDD nodes
size of Y1005 = 2.58471e+18 states, 1886876 BDD nodes
size of Y1006 = 2.58534e+18 states, 1888142 BDD nodes
size of Y1007 = 2.58597e+18 states, 1889250 BDD nodes
size of Y1008 = 2.5866e+18 states, 1890218 BDD nodes
size of Y1009 = 2.58723e+18 states, 1891418 BDD nodes
size of Y1010 = 2.58785e+18 states, 1892563 BDD nodes
size of Y1011 = 2.58848e+18 states, 1893652 BDD nodes
size of Y1012 = 2.58911e+18 states, 1894667 BDD nodes
size of Y1013 = 2.58974e+18 states, 1895706 BDD nodes
size of Y1014 = 2.59037e+18 states, 1896862 BDD nodes
size of Y1015 = 2.591e+18 states, 1897920 BDD nodes
size of Y1016 = 2.59162e+18 states, 1898849 BDD nodes
size of Y1017 = 2.59225e+18 states, 1899933 BDD nodes
size of Y1018 = 2.59288e+18 states, 1901010 BDD nodes
size of Y1019 = 2.5935e+18 states, 1902044 BDD nodes
size of Y1020 = 2.59413e+18 states, 1903012 BDD nodes
size of Y1021 = 2.59476e+18 states, 1903941 BDD nodes
size of Y1022 = 2.59538e+18 states, 1905085 BDD nodes
size of Y1023 = 2.59601e+18 states, 1906124 BDD nodes
size of Y1024 = 2.59663e+18 states, 1906774 BDD nodes
size of Y1025 = 2.59695e+18 states, 1908117 BDD nodes
size of Y1026 = 2.59726e+18 states, 1909361 BDD nodes
size of Y1027 = 2.59757e+18 states, 1910533 BDD nodes
size of Y1028 = 2.59788e+18 states, 1911720 BDD nodes
size of Y1029 = 2.5982e+18 states, 1912831 BDD nodes
size of Y1030 = 2.59851e+18 states, 1914110 BDD nodes
size of Y1031 = 2.59882e+18 states, 1915260 BDD nodes
size of Y1032 = 2.59913e+18 states, 1916354 BDD nodes
size of Y1033 = 2.59945e+18 states, 1917447 BDD nodes
size of Y1034 = 2.59976e+18 states, 1918606 BDD nodes
size of Y1035 = 2.60007e+18 states, 1919700 BDD nodes
size of Y1036 = 2.60038e+18 states, 1920812 BDD nodes
size of Y1037 = 2.60069e+18 states, 1921552 BDD nodes
size of Y1038 = 2.601e+18 states, 1922728 BDD nodes
size of Y1039 = 2.60132e+18 states, 1923550 BDD nodes
size of Y1040 = 2.60163e+18 states, 1924340 BDD nodes
size of Y1041 = 2.60194e+18 states, 1925095 BDD nodes
size of Y1042 = 2.60225e+18 states, 1925905 BDD nodes
size of Y1043 = 2.60256e+18 states, 1926578 BDD nodes
size of Y1044 = 2.60287e+18 states, 1927190 BDD nodes
size of Y1045 = 2.60318e+18 states, 1927661 BDD nodes
size of Y1046 = 2.60348e+18 states, 1928236 BDD nodes
size of Y1047 = 2.60378e+18 states, 1928642 BDD nodes
size of Y1048 = 2.60407e+18 states, 1929039 BDD nodes
size of Y1049 = 2.60437e+18 states, 1929452 BDD nodes
size of Y1050 = 2.60467e+18 states, 1929880 BDD nodes
size of Y1051 = 2.60497e+18 states, 1930183 BDD nodes
size of Y1052 = 2.60526e+18 states, 1930469 BDD nodes
size of Y1053 = 2.60556e+18 states, 1930623 BDD nodes
size of Y1054 = 2.60585e+18 states, 1930917 BDD nodes
size of Y1055 = 2.60615e+18 states, 1931147 BDD nodes
size of Y1056 = 2.60644e+18 states, 1931302 BDD nodes
size of Y1057 = 2.60674e+18 states, 1931587 BDD nodes
size of Y1058 = 2.60703e+18 states, 1931828 BDD nodes
size of Y1059 = 2.60733e+18 states, 1932043 BDD nodes
size of Y1060 = 2.60762e+18 states, 1932253 BDD nodes
size of Y1061 = 2.60792e+18 states, 1932485 BDD nodes
size of Y1062 = 2.60821e+18 states, 1932745 BDD nodes
size of Y1063 = 2.6085e+18 states, 1932963 BDD nodes
size of Y1064 = 2.6088e+18 states, 1933133 BDD nodes
size of Y1065 = 2.60909e+18 states, 1933354 BDD nodes
size of Y1066 = 2.60939e+18 states, 1933545 BDD nodes
size of Y1067 = 2.60968e+18 states, 1933729 BDD nodes
size of Y1068 = 2.60998e+18 states, 1933904 BDD nodes
size of Y1069 = 2.61027e+18 states, 1934013 BDD nodes
size of Y1070 = 2.61057e+18 states, 1934311 BDD nodes
size of Y1071 = 2.61086e+18 states, 1934504 BDD nodes
size of Y1072 = 2.61116e+18 states, 1934661 BDD nodes
size of Y1073 = 2.61145e+18 states, 1934911 BDD nodes
size of Y1074 = 2.61174e+18 states, 1935135 BDD nodes
size of Y1075 = 2.61204e+18 states, 1935336 BDD nodes
size of Y1076 = 2.61233e+18 states, 1935528 BDD nodes
size of Y1077 = 2.61263e+18 states, 1935688 BDD nodes
size of Y1078 = 2.61292e+18 states, 1935917 BDD nodes
size of Y1079 = 2.61322e+18 states, 1936097 BDD nodes
size of Y1080 = 2.61351e+18 states, 1936235 BDD nodes
size of Y1081 = 2.61381e+18 states, 1936424 BDD nodes
size of Y1082 = 2.6141e+18 states, 1936595 BDD nodes
size of Y1083 = 2.6144e+18 states, 1936753 BDD nodes
size of Y1084 = 2.61469e+18 states, 1936902 BDD nodes
size of Y1085 = 2.61499e+18 states, 1936995 BDD nodes
size of Y1086 = 2.61528e+18 states, 1937210 BDD nodes
size of Y1087 = 2.61557e+18 states, 1937367 BDD nodes
size of Y1088 = 2.61587e+18 states, 1937433 BDD nodes
size of Y1089 = 2.61616e+18 states, 1937705 BDD nodes
size of Y1090 = 2.61646e+18 states, 1937912 BDD nodes
size of Y1091 = 2.61675e+18 states, 1938100 BDD nodes
size of Y1092 = 2.61705e+18 states, 1938278 BDD nodes
size of Y1093 = 2.61734e+18 states, 1938440 BDD nodes
size of Y1094 = 2.61764e+18 states, 1938671 BDD nodes
size of Y1095 = 2.61793e+18 states, 1938833 BDD nodes
size of Y1096 = 2.61823e+18 states, 1938943 BDD nodes
size of Y1097 = 2.61852e+18 states, 1939103 BDD nodes
size of Y1098 = 2.61881e+18 states, 1939258 BDD nodes
size of Y1099 = 2.61911e+18 states, 1939401 BDD nodes
size of Y1100 = 2.6194e+18 states, 1939538 BDD nodes
size of Y1101 = 2.6197e+18 states, 1939432 BDD nodes
size of Y1102 = 2.6197e+18 states, 1939602 BDD nodes
size of Y1103 = 2.6197e+18 states, 1939772 BDD nodes
size of Y1104 = 2.6197e+18 states, 1939942 BDD nodes
size of Y1105 = 2.6197e+18 states, 1940112 BDD nodes
size of Y1106 = 2.6197e+18 states, 1940282 BDD nodes
size of Y1107 = 2.6197e+18 states, 1940452 BDD nodes
size of Y1108 = 2.6197e+18 states, 1940622 BDD nodes
size of Y1109 = 2.6197e+18 states, 1940792 BDD nodes
size of Y1110 = 2.6197e+18 states, 1940962 BDD nodes
size of Y1111 = 2.6197e+18 states, 1941132 BDD nodes
size of Y1112 = 2.6197e+18 states, 1941302 BDD nodes
size of Y1113 = 2.6197e+18 states, 1941472 BDD nodes
size of Y1114 = 2.6197e+18 states, 1941642 BDD nodes
size of Y1115 = 2.61971e+18 states, 1941812 BDD nodes
size of Y1116 = 2.61971e+18 states, 1941982 BDD nodes
size of Y1117 = 2.61971e+18 states, 1942152 BDD nodes
size of Y1118 = 2.61971e+18 states, 1942322 BDD nodes
size of Y1119 = 2.61971e+18 states, 1942492 BDD nodes
size of Y1120 = 2.61971e+18 states, 1942662 BDD nodes
size of Y1121 = 2.61971e+18 states, 1942832 BDD nodes
size of Y1122 = 2.61971e+18 states, 1943002 BDD nodes
size of Y1123 = 2.61971e+18 states, 1943172 BDD nodes
size of Y1124 = 2.61971e+18 states, 1943342 BDD nodes
size of Y1125 = 2.61971e+18 states, 1943512 BDD nodes
size of Y1126 = 2.61971e+18 states, 1943682 BDD nodes
size of Y1127 = 2.61971e+18 states, 1943852 BDD nodes
size of Y1128 = 2.61971e+18 states, 1944022 BDD nodes
size of Y1129 = 2.61971e+18 states, 1944192 BDD nodes
size of Y1130 = 2.61971e+18 states, 1944362 BDD nodes
size of Y1131 = 2.61971e+18 states, 1944532 BDD nodes
size of Y1132 = 2.61971e+18 states, 1944702 BDD nodes
size of Y1133 = 2.61971e+18 states, 1944872 BDD nodes
size of Y1134 = 2.61971e+18 states, 1945042 BDD nodes
size of Y1135 = 2.61971e+18 states, 1945212 BDD nodes
size of Y1136 = 2.61972e+18 states, 1945382 BDD nodes
size of Y1137 = 2.61972e+18 states, 1945552 BDD nodes
size of Y1138 = 2.61972e+18 states, 1945722 BDD nodes
size of Y1139 = 2.61972e+18 states, 1945892 BDD nodes
size of Y1140 = 2.61972e+18 states, 1946062 BDD nodes
size of Y1141 = 2.61972e+18 states, 1946232 BDD nodes
size of Y1142 = 2.61972e+18 states, 1946402 BDD nodes
size of Y1143 = 2.61972e+18 states, 1946572 BDD nodes
size of Y1144 = 2.61972e+18 states, 1946742 BDD nodes
size of Y1145 = 2.61972e+18 states, 1946912 BDD nodes
size of Y1146 = 2.61972e+18 states, 1947082 BDD nodes
size of Y1147 = 2.61972e+18 states, 1947252 BDD nodes
size of Y1148 = 2.61972e+18 states, 1947422 BDD nodes
size of Y1149 = 2.61972e+18 states, 1947592 BDD nodes
size of Y1150 = 2.61972e+18 states, 1947762 BDD nodes
size of Y1151 = 2.61972e+18 states, 1947932 BDD nodes
size of Y1152 = 2.61972e+18 states, 1948102 BDD nodes
size of Y1153 = 2.61972e+18 states, 1948272 BDD nodes
size of Y1154 = 2.61972e+18 states, 1948442 BDD nodes
size of Y1155 = 2.61972e+18 states, 1948612 BDD nodes
size of Y1156 = 2.61972e+18 states, 1948782 BDD nodes
size of Y1157 = 2.61972e+18 states, 1948952 BDD nodes
size of Y1158 = 2.61973e+18 states, 1949122 BDD nodes
size of Y1159 = 2.61973e+18 states, 1949292 BDD nodes
size of Y1160 = 2.61973e+18 states, 1949462 BDD nodes
size of Y1161 = 2.61973e+18 states, 1949632 BDD nodes
size of Y1162 = 2.61973e+18 states, 1949802 BDD nodes
size of Y1163 = 2.61973e+18 states, 1949972 BDD nodes
size of Y1164 = 2.61973e+18 states, 1950142 BDD nodes
size of Y1165 = 2.61973e+18 states, 1950312 BDD nodes
size of Y1166 = 2.61973e+18 states, 1950482 BDD nodes
size of Y1167 = 2.61973e+18 states, 1950652 BDD nodes
size of Y1168 = 2.61973e+18 states, 1950822 BDD nodes
size of Y1169 = 2.61973e+18 states, 1950992 BDD nodes
size of Y1170 = 2.61973e+18 states, 1951162 BDD nodes
size of Y1171 = 2.61973e+18 states, 1951332 BDD nodes
size of Y1172 = 2.61973e+18 states, 1951502 BDD nodes
size of Y1173 = 2.61973e+18 states, 1951672 BDD nodes
size of Y1174 = 2.61973e+18 states, 1951842 BDD nodes
size of Y1175 = 2.61973e+18 states, 1952012 BDD nodes
size of Y1176 = 2.61973e+18 states, 1952182 BDD nodes
size of Y1177 = 2.61973e+18 states, 1952352 BDD nodes
size of Y1178 = 2.61973e+18 states, 1952522 BDD nodes
size of Y1179 = 2.61974e+18 states, 1952692 BDD nodes
size of Y1180 = 2.61974e+18 states, 1952862 BDD nodes
size of Y1181 = 2.61974e+18 states, 1953032 BDD nodes
size of Y1182 = 2.61974e+18 states, 1953202 BDD nodes
size of Y1183 = 2.61974e+18 states, 1953372 BDD nodes
size of Y1184 = 2.61974e+18 states, 1953542 BDD nodes
size of Y1185 = 2.61974e+18 states, 1953712 BDD nodes
size of Y1186 = 2.61974e+18 states, 1953882 BDD nodes
size of Y1187 = 2.61974e+18 states, 1954052 BDD nodes
size of Y1188 = 2.61974e+18 states, 1954222 BDD nodes
size of Y1189 = 2.61974e+18 states, 1954392 BDD nodes
size of Y1190 = 2.61974e+18 states, 1954562 BDD nodes
size of Y1191 = 2.61974e+18 states, 1954732 BDD nodes
size of Y1192 = 2.61974e+18 states, 1954900 BDD nodes
size of Y1193 = 2.61974e+18 states, 1955068 BDD nodes
size of Y1194 = 2.61974e+18 states, 1955236 BDD nodes
size of Y1195 = 2.61974e+18 states, 1955402 BDD nodes
size of Y1196 = 2.61974e+18 states, 1955566 BDD nodes
size of Y1197 = 2.61974e+18 states, 1955734 BDD nodes
size of Y1198 = 2.61974e+18 states, 1955902 BDD nodes
size of Y1199 = 2.61974e+18 states, 1956066 BDD nodes
size of Y1200 = 2.61974e+18 states, 1956232 BDD nodes
size of Y1201 = 2.61975e+18 states, 1956395 BDD nodes
size of Y1202 = 2.61975e+18 states, 1956558 BDD nodes
size of Y1203 = 2.61975e+18 states, 1956719 BDD nodes
size of Y1204 = 2.61975e+18 states, 1956875 BDD nodes
size of Y1205 = 2.61975e+18 states, 1957029 BDD nodes
size of Y1206 = 2.61975e+18 states, 1957185 BDD nodes
size of Y1207 = 2.61975e+18 states, 1957341 BDD nodes
size of Y1208 = 2.61975e+18 states, 1957494 BDD nodes
size of Y1209 = 2.61975e+18 states, 1957648 BDD nodes
size of Y1210 = 2.61975e+18 states, 1957800 BDD nodes
size of Y1211 = 2.61975e+18 states, 1957954 BDD nodes
size of Y1212 = 2.61975e+18 states, 1958106 BDD nodes
size of Y1213 = 2.61975e+18 states, 1958253 BDD nodes
size of Y1214 = 2.61975e+18 states, 1958401 BDD nodes
size of Y1215 = 2.61975e+18 states, 1958548 BDD nodes
size of Y1216 = 2.61975e+18 states, 1958694 BDD nodes
size of Y1217 = 2.61975e+18 states, 1958841 BDD nodes
size of Y1218 = 2.61975e+18 states, 1958986 BDD nodes
size of Y1219 = 2.61975e+18 states, 1959131 BDD nodes
size of Y1220 = 2.61975e+18 states, 1959276 BDD nodes
size of Y1221 = 2.61975e+18 states, 1959421 BDD nodes
size of Y1222 = 2.61976e+18 states, 1959566 BDD nodes
size of Y1223 = 2.61976e+18 states, 1959711 BDD nodes
size of Y1224 = 2.61976e+18 states, 1959856 BDD nodes
size of Y1225 = 2.61976e+18 states, 1960001 BDD nodes
size of Y1226 = 2.61976e+18 states, 1960146 BDD nodes
size of Y1227 = 2.61976e+18 states, 1960291 BDD nodes
size of Y1228 = 2.61976e+18 states, 1960436 BDD nodes
size of Y1229 = 2.61976e+18 states, 1960581 BDD nodes
size of Y1230 = 2.61976e+18 states, 1960726 BDD nodes
size of Y1231 = 2.61976e+18 states, 1960871 BDD nodes
size of Y1232 = 2.61976e+18 states, 1961016 BDD nodes
size of Y1233 = 2.61976e+18 states, 1961161 BDD nodes
size of Y1234 = 2.61976e+18 states, 1961306 BDD nodes
size of Y1235 = 2.61976e+18 states, 1961451 BDD nodes
size of Y1236 = 2.61976e+18 states, 1961596 BDD nodes
size of Y1237 = 2.61976e+18 states, 1961741 BDD nodes
size of Y1238 = 2.61976e+18 states, 1961886 BDD nodes
size of Y1239 = 2.61976e+18 states, 1962031 BDD nodes
size of Y1240 = 2.61976e+18 states, 1962176 BDD nodes
size of Y1241 = 2.61976e+18 states, 1962321 BDD nodes
size of Y1242 = 2.61976e+18 states, 1962466 BDD nodes
size of Y1243 = 2.61977e+18 states, 1962611 BDD nodes
size of Y1244 = 2.61977e+18 states, 1962756 BDD nodes
size of Y1245 = 2.61977e+18 states, 1962901 BDD nodes
size of Y1246 = 2.61977e+18 states, 1963046 BDD nodes
size of Y1247 = 2.61977e+18 states, 1963191 BDD nodes
size of Y1248 = 2.61977e+18 states, 1963336 BDD nodes
size of Y1249 = 2.61977e+18 states, 1963481 BDD nodes
size of Y1250 = 2.61977e+18 states, 1963626 BDD nodes
size of Y1251 = 2.61977e+18 states, 1963771 BDD nodes
size of Y1252 = 2.61977e+18 states, 1963916 BDD nodes
size of Y1253 = 2.61977e+18 states, 1964061 BDD nodes
size of Y1254 = 2.61977e+18 states, 1964206 BDD nodes
size of Y1255 = 2.61977e+18 states, 1964351 BDD nodes
size of Y1256 = 2.61977e+18 states, 1964496 BDD nodes
size of Y1257 = 2.61977e+18 states, 1964641 BDD nodes
size of Y1258 = 2.61977e+18 states, 1964786 BDD nodes
size of Y1259 = 2.61977e+18 states, 1964931 BDD nodes
size of Y1260 = 2.61977e+18 states, 1965076 BDD nodes
size of Y1261 = 2.61977e+18 states, 1965221 BDD nodes
size of Y1262 = 2.61977e+18 states, 1965366 BDD nodes
size of Y1263 = 2.61977e+18 states, 1965511 BDD nodes
size of Y1264 = 2.61977e+18 states, 1965656 BDD nodes
size of Y1265 = 2.61978e+18 states, 1965801 BDD nodes
size of Y1266 = 2.61978e+18 states, 1965946 BDD nodes
size of Y1267 = 2.61978e+18 states, 1966091 BDD nodes
size of Y1268 = 2.61978e+18 states, 1966236 BDD nodes
size of Y1269 = 2.61978e+18 states, 1966381 BDD nodes
size of Y1270 = 2.61978e+18 states, 1966526 BDD nodes
size of Y1271 = 2.61978e+18 states, 1966671 BDD nodes
size of Y1272 = 2.61978e+18 states, 1966816 BDD nodes
size of Y1273 = 2.61978e+18 states, 1966961 BDD nodes
size of Y1274 = 2.61978e+18 states, 1967106 BDD nodes
size of Y1275 = 2.61978e+18 states, 1967251 BDD nodes
size of Y1276 = 2.61978e+18 states, 1967396 BDD nodes
size of Y1277 = 2.61978e+18 states, 1967541 BDD nodes
size of Y1278 = 2.61978e+18 states, 1967686 BDD nodes
size of Y1279 = 2.61978e+18 states, 1967831 BDD nodes
size of Y1280 = 2.61978e+18 states, 1967976 BDD nodes
size of Y1281 = 2.61978e+18 states, 1968121 BDD nodes
size of Y1282 = 2.61978e+18 states, 1968266 BDD nodes
size of Y1283 = 2.61978e+18 states, 1968411 BDD nodes
size of Y1284 = 2.61978e+18 states, 1968556 BDD nodes
size of Y1285 = 2.61978e+18 states, 1968701 BDD nodes
size of Y1286 = 2.61979e+18 states, 1968846 BDD nodes
size of Y1287 = 2.61979e+18 states, 1968991 BDD nodes
size of Y1288 = 2.61979e+18 states, 1969136 BDD nodes
size of Y1289 = 2.61979e+18 states, 1969281 BDD nodes
size of Y1290 = 2.61979e+18 states, 1969426 BDD nodes
size of Y1291 = 2.61979e+18 states, 1969571 BDD nodes
size of Y1292 = 2.61979e+18 states, 1969716 BDD nodes
size of Y1293 = 2.61979e+18 states, 1969861 BDD nodes
size of Y1294 = 2.61979e+18 states, 1970006 BDD nodes
size of Y1295 = 2.61979e+18 states, 1970151 BDD nodes
size of Y1296 = 2.61979e+18 states, 1970296 BDD nodes
size of Y1297 = 2.61979e+18 states, 1970441 BDD nodes
size of Y1298 = 2.61979e+18 states, 1970586 BDD nodes
size of Y1299 = 2.61979e+18 states, 1970731 BDD nodes
size of Y1300 = 2.61979e+18 states, 1970876 BDD nodes
size of Y1301 = 2.61979e+18 states, 1971021 BDD nodes
size of Y1302 = 2.61979e+18 states, 1971166 BDD nodes
size of Y1303 = 2.61979e+18 states, 1971311 BDD nodes
size of Y1304 = 2.61979e+18 states, 1971456 BDD nodes
size of Y1305 = 2.61979e+18 states, 1971601 BDD nodes
size of Y1306 = 2.6198e+18 states, 1971746 BDD nodes
size of Y1307 = 2.6198e+18 states, 1971891 BDD nodes
size of Y1308 = 2.6198e+18 states, 1972036 BDD nodes
size of Y1309 = 2.6198e+18 states, 1972181 BDD nodes
size of Y1310 = 2.6198e+18 states, 1972326 BDD nodes
size of Y1311 = 2.6198e+18 states, 1972471 BDD nodes
size of Y1312 = 2.6198e+18 states, 1972616 BDD nodes
size of Y1313 = 2.6198e+18 states, 1972761 BDD nodes
size of Y1314 = 2.6198e+18 states, 1972906 BDD nodes
size of Y1315 = 2.6198e+18 states, 1973051 BDD nodes
size of Y1316 = 2.6198e+18 states, 1973196 BDD nodes
size of Y1317 = 2.6198e+18 states, 1973341 BDD nodes
size of Y1318 = 2.6198e+18 states, 1973486 BDD nodes
size of Y1319 = 2.61981e+18 states, 1973631 BDD nodes
size of Y1320 = 2.61981e+18 states, 1973776 BDD nodes
size of Y1321 = 2.61981e+18 states, 1973921 BDD nodes
size of Y1322 = 2.61981e+18 states, 1974066 BDD nodes
size of Y1323 = 2.61981e+18 states, 1974211 BDD nodes
size of Y1324 = 2.61981e+18 states, 1974356 BDD nodes
size of Y1325 = 2.61981e+18 states, 1974501 BDD nodes
size of Y1326 = 2.61981e+18 states, 1974646 BDD nodes
size of Y1327 = 2.61981e+18 states, 1974791 BDD nodes
size of Y1328 = 2.61981e+18 states, 1974936 BDD nodes
size of Y1329 = 2.61981e+18 states, 1975081 BDD nodes
size of Y1330 = 2.61981e+18 states, 1975226 BDD nodes
size of Y1331 = 2.61981e+18 states, 1975371 BDD nodes
size of Y1332 = 2.61982e+18 states, 1975516 BDD nodes
size of Y1333 = 2.61982e+18 states, 1975657 BDD nodes
size of Y1334 = 2.61982e+18 states, 1975798 BDD nodes
size of Y1335 = 2.61982e+18 states, 1975939 BDD nodes
size of Y1336 = 2.61982e+18 states, 1976080 BDD nodes
size of Y1337 = 2.61982e+18 states, 1976221 BDD nodes
size of Y1338 = 2.61982e+18 states, 1976362 BDD nodes
size of Y1339 = 2.61982e+18 states, 1976503 BDD nodes
size of Y1340 = 2.61982e+18 states, 1976644 BDD nodes
size of Y1341 = 2.61982e+18 states, 1976785 BDD nodes
size of Y1342 = 2.61982e+18 states, 1976926 BDD nodes
size of Y1343 = 2.61982e+18 states, 1977067 BDD nodes
size of Y1344 = 2.61983e+18 states, 1977208 BDD nodes
size of Y1345 = 2.61983e+18 states, 1977347 BDD nodes
size of Y1346 = 2.61983e+18 states, 1977486 BDD nodes
size of Y1347 = 2.61983e+18 states, 1977625 BDD nodes
size of Y1348 = 2.61983e+18 states, 1977764 BDD nodes
size of Y1349 = 2.61983e+18 states, 1977901 BDD nodes
size of Y1350 = 2.61983e+18 states, 1978038 BDD nodes
size of Y1351 = 2.61983e+18 states, 1978173 BDD nodes
size of Y1352 = 2.61983e+18 states, 1978306 BDD nodes
size of Y1353 = 2.61983e+18 states, 1978434 BDD nodes
size of Y1354 = 2.61983e+18 states, 1978562 BDD nodes
size of Y1355 = 2.61983e+18 states, 1978690 BDD nodes
size of Y1356 = 2.61984e+18 states, 1978818 BDD nodes
size of Y1357 = 2.61984e+18 states, 1978946 BDD nodes
size of Y1358 = 2.61984e+18 states, 1979074 BDD nodes
size of Y1359 = 2.61984e+18 states, 1979202 BDD nodes
size of Y1360 = 2.61984e+18 states, 1979330 BDD nodes
size of Y1361 = 2.61984e+18 states, 1979458 BDD nodes
size of Y1362 = 2.61984e+18 states, 1979586 BDD nodes
size of Y1363 = 2.61984e+18 states, 1979714 BDD nodes
size of Y1364 = 2.61984e+18 states, 1979842 BDD nodes
size of Y1365 = 2.61984e+18 states, 1979970 BDD nodes
size of Y1366 = 2.61985e+18 states, 1980098 BDD nodes
size of Y1367 = 2.61985e+18 states, 1980226 BDD nodes
size of Y1368 = 2.61985e+18 states, 1980354 BDD nodes
size of Y1369 = 2.61985e+18 states, 1980482 BDD nodes
size of Y1370 = 2.61985e+18 states, 1980610 BDD nodes
size of Y1371 = 2.61985e+18 states, 1980738 BDD nodes
size of Y1372 = 2.61985e+18 states, 1980866 BDD nodes
size of Y1373 = 2.61985e+18 states, 1980994 BDD nodes
size of Y1374 = 2.61985e+18 states, 1981122 BDD nodes
size of Y1375 = 2.61985e+18 states, 1981250 BDD nodes
size of Y1376 = 2.61985e+18 states, 1981378 BDD nodes
size of Y1377 = 2.61986e+18 states, 1981506 BDD nodes
size of Y1378 = 2.61986e+18 states, 1981634 BDD nodes
size of Y1379 = 2.61986e+18 states, 1981762 BDD nodes
size of Y1380 = 2.61986e+18 states, 1981890 BDD nodes
size of Y1381 = 2.61986e+18 states, 1982018 BDD nodes
size of Y1382 = 2.61986e+18 states, 1982146 BDD nodes
size of Y1383 = 2.61986e+18 states, 1982274 BDD nodes
size of Y1384 = 2.61986e+18 states, 1982402 BDD nodes
size of Y1385 = 2.61986e+18 states, 1982530 BDD nodes
size of Y1386 = 2.61986e+18 states, 1982658 BDD nodes
size of Y1387 = 2.61986e+18 states, 1982786 BDD nodes
size of Y1388 = 2.61987e+18 states, 1982914 BDD nodes
size of Y1389 = 2.61987e+18 states, 1983042 BDD nodes
size of Y1390 = 2.61987e+18 states, 1983170 BDD nodes
size of Y1391 = 2.61987e+18 states, 1983298 BDD nodes
size of Y1392 = 2.61987e+18 states, 1983426 BDD nodes
size of Y1393 = 2.61987e+18 states, 1983554 BDD nodes
size of Y1394 = 2.61987e+18 states, 1983682 BDD nodes
size of Y1395 = 2.61987e+18 states, 1983810 BDD nodes
size of Y1396 = 2.61987e+18 states, 1983938 BDD nodes
size of Y1397 = 2.61987e+18 states, 1984066 BDD nodes
size of Y1398 = 2.61987e+18 states, 1984194 BDD nodes
size of Y1399 = 2.61988e+18 states, 1984322 BDD nodes
size of Y1400 = 2.61988e+18 states, 1984450 BDD nodes
size of Y1401 = 2.61988e+18 states, 1984578 BDD nodes
size of Y1402 = 2.61988e+18 states, 1984706 BDD nodes
size of Y1403 = 2.61988e+18 states, 1984834 BDD nodes
size of Y1404 = 2.61988e+18 states, 1984962 BDD nodes
size of Y1405 = 2.61988e+18 states, 1985090 BDD nodes
size of Y1406 = 2.61988e+18 states, 1985218 BDD nodes
size of Y1407 = 2.61988e+18 states, 1985346 BDD nodes
size of Y1408 = 2.61988e+18 states, 1985474 BDD nodes
size of Y1409 = 2.61989e+18 states, 1985602 BDD nodes
size of Y1410 = 2.61989e+18 states, 1985730 BDD nodes
size of Y1411 = 2.61989e+18 states, 1985858 BDD nodes
size of Y1412 = 2.61989e+18 states, 1985986 BDD nodes
size of Y1413 = 2.61989e+18 states, 1986114 BDD nodes
size of Y1414 = 2.61989e+18 states, 1986242 BDD nodes
size of Y1415 = 2.61989e+18 states, 1986370 BDD nodes
size of Y1416 = 2.61989e+18 states, 1986498 BDD nodes
size of Y1417 = 2.61989e+18 states, 1986626 BDD nodes
size of Y1418 = 2.61989e+18 states, 1986754 BDD nodes
size of Y1419 = 2.61989e+18 states, 1986882 BDD nodes
size of Y1420 = 2.61989e+18 states, 1987010 BDD nodes
size of Y1421 = 2.61989e+18 states, 1987138 BDD nodes
size of Y1422 = 2.6199e+18 states, 1987266 BDD nodes
size of Y1423 = 2.6199e+18 states, 1987394 BDD nodes
size of Y1424 = 2.6199e+18 states, 1987522 BDD nodes
size of Y1425 = 2.6199e+18 states, 1987650 BDD nodes
size of Y1426 = 2.6199e+18 states, 1987778 BDD nodes
size of Y1427 = 2.6199e+18 states, 1987906 BDD nodes
size of Y1428 = 2.6199e+18 states, 1988034 BDD nodes
size of Y1429 = 2.6199e+18 states, 1988162 BDD nodes
size of Y1430 = 2.6199e+18 states, 1988290 BDD nodes
size of Y1431 = 2.6199e+18 states, 1988418 BDD nodes
size of Y1432 = 2.6199e+18 states, 1988546 BDD nodes
size of Y1433 = 2.6199e+18 states, 1988674 BDD nodes
size of Y1434 = 2.6199e+18 states, 1988802 BDD nodes
size of Y1435 = 2.6199e+18 states, 1988930 BDD nodes
size of Y1436 = 2.6199e+18 states, 1989058 BDD nodes
size of Y1437 = 2.6199e+18 states, 1989186 BDD nodes
size of Y1438 = 2.6199e+18 states, 1989314 BDD nodes
size of Y1439 = 2.61991e+18 states, 1989442 BDD nodes
size of Y1440 = 2.61991e+18 states, 1989570 BDD nodes
size of Y1441 = 2.61991e+18 states, 1989698 BDD nodes
size of Y1442 = 2.61991e+18 states, 1989826 BDD nodes
size of Y1443 = 2.61991e+18 states, 1989954 BDD nodes
size of Y1444 = 2.61991e+18 states, 1990082 BDD nodes
size of Y1445 = 2.61991e+18 states, 1990210 BDD nodes
size of Y1446 = 2.61991e+18 states, 1990351 BDD nodes
size of Y1447 = 2.61991e+18 states, 1990479 BDD nodes
size of Y1448 = 2.61991e+18 states, 1990605 BDD nodes
size of Y1449 = 2.61991e+18 states, 1990731 BDD nodes
size of Y1450 = 2.61991e+18 states, 1990857 BDD nodes
size of Y1451 = 2.61991e+18 states, 1990981 BDD nodes
size of Y1452 = 2.61991e+18 states, 1991103 BDD nodes
size of Y1453 = 2.61991e+18 states, 1991229 BDD nodes
size of Y1454 = 2.61991e+18 states, 1991355 BDD nodes
size of Y1455 = 2.61991e+18 states, 1991477 BDD nodes
size of Y1456 = 2.61992e+18 states, 1991601 BDD nodes
size of Y1457 = 2.61992e+18 states, 1991722 BDD nodes
size of Y1458 = 2.61992e+18 states, 1991843 BDD nodes
size of Y1459 = 2.61992e+18 states, 1991962 BDD nodes
size of Y1460 = 2.61992e+18 states, 1992076 BDD nodes
size of Y1461 = 2.61992e+18 states, 1992188 BDD nodes
size of Y1462 = 2.61992e+18 states, 1992302 BDD nodes
size of Y1463 = 2.61992e+18 states, 1992416 BDD nodes
size of Y1464 = 2.61992e+18 states, 1992527 BDD nodes
size of Y1465 = 2.61992e+18 states, 1992639 BDD nodes
size of Y1466 = 2.61992e+18 states, 1992749 BDD nodes
size of Y1467 = 2.61992e+18 states, 1992860 BDD nodes
size of Y1468 = 2.61992e+18 states, 1992969 BDD nodes
size of Y1469 = 2.61992e+18 states, 1993073 BDD nodes
size of Y1470 = 2.61992e+18 states, 1993178 BDD nodes
size of Y1471 = 2.61992e+18 states, 1993281 BDD nodes
size of Y1472 = 2.61992e+18 states, 1993383 BDD nodes
size of Y1473 = 2.61992e+18 states, 1993485 BDD nodes
size of Y1474 = 2.61992e+18 states, 1993584 BDD nodes
size of Y1475 = 2.61992e+18 states, 1993681 BDD nodes
size of Y1476 = 2.61993e+18 states, 1993778 BDD nodes
size of Y1477 = 2.61993e+18 states, 1993875 BDD nodes
size of Y1478 = 2.61993e+18 states, 1993972 BDD nodes
size of Y1479 = 2.61993e+18 states, 1994069 BDD nodes
size of Y1480 = 2.61993e+18 states, 1994166 BDD nodes
size of Y1481 = 2.61993e+18 states, 1994263 BDD nodes
size of Y1482 = 2.61993e+18 states, 1994360 BDD nodes
size of Y1483 = 2.61993e+18 states, 1994457 BDD nodes
size of Y1484 = 2.61993e+18 states, 1994554 BDD nodes
size of Y1485 = 2.61993e+18 states, 1994651 BDD nodes
size of Y1486 = 2.61993e+18 states, 1994748 BDD nodes
size of Y1487 = 2.61993e+18 states, 1994845 BDD nodes
size of Y1488 = 2.61993e+18 states, 1994942 BDD nodes
size of Y1489 = 2.61993e+18 states, 1995039 BDD nodes
size of Y1490 = 2.61993e+18 states, 1995136 BDD nodes
size of Y1491 = 2.61993e+18 states, 1995233 BDD nodes
size of Y1492 = 2.61993e+18 states, 1995330 BDD nodes
size of Y1493 = 2.61993e+18 states, 1995427 BDD nodes
size of Y1494 = 2.61993e+18 states, 1995524 BDD nodes
size of Y1495 = 2.61993e+18 states, 1995621 BDD nodes
size of Y1496 = 2.61993e+18 states, 1995718 BDD nodes
size of Y1497 = 2.61994e+18 states, 1995815 BDD nodes
size of Y1498 = 2.61994e+18 states, 1995912 BDD nodes
size of Y1499 = 2.61994e+18 states, 1996009 BDD nodes
size of Y1500 = 2.61994e+18 states, 1996106 BDD nodes
size of Y1501 = 2.61994e+18 states, 1996203 BDD nodes
size of Y1502 = 2.61994e+18 states, 1996300 BDD nodes
size of Y1503 = 2.61994e+18 states, 1996397 BDD nodes
size of Y1504 = 2.61994e+18 states, 1996494 BDD nodes
size of Y1505 = 2.61994e+18 states, 1996591 BDD nodes
size of Y1506 = 2.61994e+18 states, 1996688 BDD nodes
size of Y1507 = 2.61994e+18 states, 1996785 BDD nodes
size of Y1508 = 2.61994e+18 states, 1996882 BDD nodes
size of Y1509 = 2.61994e+18 states, 1996979 BDD nodes
size of Y1510 = 2.61994e+18 states, 1997076 BDD nodes
size of Y1511 = 2.61994e+18 states, 1997173 BDD nodes
size of Y1512 = 2.61994e+18 states, 1997270 BDD nodes
size of Y1513 = 2.61994e+18 states, 1997367 BDD nodes
size of Y1514 = 2.61994e+18 states, 1997464 BDD nodes
size of Y1515 = 2.61994e+18 states, 1997561 BDD nodes
size of Y1516 = 2.61994e+18 states, 1997658 BDD nodes
size of Y1517 = 2.61994e+18 states, 1997755 BDD nodes
size of Y1518 = 2.61994e+18 states, 1997852 BDD nodes
size of Y1519 = 2.61995e+18 states, 1997949 BDD nodes
size of Y1520 = 2.61995e+18 states, 1998046 BDD nodes
size of Y1521 = 2.61995e+18 states, 1998143 BDD nodes
size of Y1522 = 2.61995e+18 states, 1998240 BDD nodes
size of Y1523 = 2.61995e+18 states, 1998346 BDD nodes
size of Y1524 = 2.61995e+18 states, 1998439 BDD nodes
size of Y1525 = 2.61995e+18 states, 1998532 BDD nodes
size of Y1526 = 2.61995e+18 states, 1998625 BDD nodes
size of Y1527 = 2.61995e+18 states, 1998718 BDD nodes
size of Y1528 = 2.61995e+18 states, 1998811 BDD nodes
size of Y1529 = 2.61995e+18 states, 1998904 BDD nodes
size of Y1530 = 2.61995e+18 states, 1998997 BDD nodes
size of Y1531 = 2.61995e+18 states, 1999090 BDD nodes
size of Y1532 = 2.61995e+18 states, 1999189 BDD nodes
size of Y1533 = 2.61995e+18 states, 1999282 BDD nodes
size of Y1534 = 2.61995e+18 states, 1999375 BDD nodes
size of Y1535 = 2.61995e+18 states, 1999468 BDD nodes
size of Y1536 = 2.61995e+18 states, 1999561 BDD nodes
size of Y1537 = 2.61995e+18 states, 1999654 BDD nodes
size of Y1538 = 2.61995e+18 states, 1999747 BDD nodes
size of Y1539 = 2.61995e+18 states, 1999840 BDD nodes
size of Y1540 = 2.61996e+18 states, 1999933 BDD nodes
size of Y1541 = 2.61996e+18 states, 2000026 BDD nodes
size of Y1542 = 2.61996e+18 states, 2000119 BDD nodes
size of Y1543 = 2.61996e+18 states, 2000212 BDD nodes
size of Y1544 = 2.61996e+18 states, 2000305 BDD nodes
size of Y1545 = 2.61996e+18 states, 2000398 BDD nodes
size of Y1546 = 2.61996e+18 states, 2000491 BDD nodes
size of Y1547 = 2.61996e+18 states, 2000584 BDD nodes
size of Y1548 = 2.61996e+18 states, 2000677 BDD nodes
size of Y1549 = 2.61996e+18 states, 2000770 BDD nodes
size of Y1550 = 2.61996e+18 states, 2000863 BDD nodes
size of Y1551 = 2.61996e+18 states, 2000956 BDD nodes
size of Y1552 = 2.61996e+18 states, 2001049 BDD nodes
size of Y1553 = 2.61996e+18 states, 2001142 BDD nodes
size of Y1554 = 2.61996e+18 states, 2001235 BDD nodes
size of Y1555 = 2.61996e+18 states, 2001328 BDD nodes
size of Y1556 = 2.61996e+18 states, 2001421 BDD nodes
size of Y1557 = 2.61996e+18 states, 2001514 BDD nodes
size of Y1558 = 2.61996e+18 states, 2001607 BDD nodes
size of Y1559 = 2.61996e+18 states, 2001700 BDD nodes
size of Y1560 = 2.61996e+18 states, 2001793 BDD nodes
size of Y1561 = 2.61996e+18 states, 2001886 BDD nodes
size of Y1562 = 2.61997e+18 states, 2001979 BDD nodes
size of Y1563 = 2.61997e+18 states, 2002072 BDD nodes
size of Y1564 = 2.61997e+18 states, 2002165 BDD nodes
size of Y1565 = 2.61997e+18 states, 2002258 BDD nodes
size of Y1566 = 2.61997e+18 states, 2002351 BDD nodes
size of Y1567 = 2.61997e+18 states, 2002444 BDD nodes
size of Y1568 = 2.61997e+18 states, 2002537 BDD nodes
size of Y1569 = 2.61997e+18 states, 2002630 BDD nodes
size of Y1570 = 2.61997e+18 states, 2002723 BDD nodes
size of Y1571 = 2.61997e+18 states, 2002816 BDD nodes
size of Y1572 = 2.61997e+18 states, 2002909 BDD nodes
size of Y1573 = 2.61997e+18 states, 2003002 BDD nodes
size of Y1574 = 2.61997e+18 states, 2003095 BDD nodes
size of Y1575 = 2.61997e+18 states, 2003188 BDD nodes
size of Y1576 = 2.61997e+18 states, 2003281 BDD nodes
size of Y1577 = 2.61997e+18 states, 2003374 BDD nodes
size of Y1578 = 2.61997e+18 states, 2003467 BDD nodes
size of Y1579 = 2.61997e+18 states, 2003560 BDD nodes
size of Y1580 = 2.61997e+18 states, 2003653 BDD nodes
size of Y1581 = 2.61997e+18 states, 2003746 BDD nodes
size of Y1582 = 2.61997e+18 states, 2003839 BDD nodes
size of Y1583 = 2.61998e+18 states, 2003932 BDD nodes
size of Y1584 = 2.61998e+18 states, 2004025 BDD nodes
size of Y1585 = 2.61998e+18 states, 2004118 BDD nodes
size of Y1586 = 2.61998e+18 states, 2004211 BDD nodes
size of Y1587 = 2.61998e+18 states, 2004304 BDD nodes
size of Y1588 = 2.61998e+18 states, 2004397 BDD nodes
size of Y1589 = 2.61998e+18 states, 2004490 BDD nodes
size of Y1590 = 2.61998e+18 states, 2004583 BDD nodes
size of Y1591 = 2.61998e+18 states, 2004676 BDD nodes
size of Y1592 = 2.61998e+18 states, 2004769 BDD nodes
size of Y1593 = 2.61998e+18 states, 2004862 BDD nodes
size of Y1594 = 2.61998e+18 states, 2004955 BDD nodes
size of Y1595 = 2.61998e+18 states, 2005048 BDD nodes
size of Y1596 = 2.61998e+18 states, 2005141 BDD nodes
size of Y1597 = 2.61998e+18 states, 2005234 BDD nodes
size of Y1598 = 2.61998e+18 states, 2005327 BDD nodes
size of Y1599 = 2.61998e+18 states, 2005420 BDD nodes
size of Y1600 = 2.61998e+18 states, 2005513 BDD nodes
size of Y1601 = 2.61998e+18 states, 2005604 BDD nodes
size of Y1602 = 2.61998e+18 states, 2005695 BDD nodes
size of Y1603 = 2.61998e+18 states, 2005786 BDD nodes
size of Y1604 = 2.61999e+18 states, 2005877 BDD nodes
size of Y1605 = 2.61999e+18 states, 2005966 BDD nodes
size of Y1606 = 2.61999e+18 states, 2006055 BDD nodes
size of Y1607 = 2.61999e+18 states, 2006142 BDD nodes
size of Y1608 = 2.61999e+18 states, 2006227 BDD nodes
size of Y1609 = 2.61999e+18 states, 2006307 BDD nodes
size of Y1610 = 2.61999e+18 states, 2006387 BDD nodes
size of Y1611 = 2.61999e+18 states, 2006467 BDD nodes
size of Y1612 = 2.61999e+18 states, 2006547 BDD nodes
size of Y1613 = 2.61999e+18 states, 2006627 BDD nodes
size of Y1614 = 2.61999e+18 states, 2006707 BDD nodes
size of Y1615 = 2.61999e+18 states, 2006787 BDD nodes
size of Y1616 = 2.61999e+18 states, 2006867 BDD nodes
size of Y1617 = 2.61999e+18 states, 2006947 BDD nodes
size of Y1618 = 2.61999e+18 states, 2007027 BDD nodes
size of Y1619 = 2.61999e+18 states, 2007107 BDD nodes
size of Y1620 = 2.61999e+18 states, 2007187 BDD nodes
size of Y1621 = 2.61999e+18 states, 2007267 BDD nodes
size of Y1622 = 2.61999e+18 states, 2007347 BDD nodes
size of Y1623 = 2.61999e+18 states, 2007427 BDD nodes
size of Y1624 = 2.61999e+18 states, 2007507 BDD nodes
size of Y1625 = 2.61999e+18 states, 2007587 BDD nodes
size of Y1626 = 2.62e+18 states, 2007667 BDD nodes
size of Y1627 = 2.62e+18 states, 2007747 BDD nodes
size of Y1628 = 2.62e+18 states, 2007827 BDD nodes
size of Y1629 = 2.62e+18 states, 2007907 BDD nodes
size of Y1630 = 2.62e+18 states, 2007987 BDD nodes
size of Y1631 = 2.62e+18 states, 2008067 BDD nodes
size of Y1632 = 2.62e+18 states, 2008147 BDD nodes
size of Y1633 = 2.62e+18 states, 2008227 BDD nodes
size of Y1634 = 2.62e+18 states, 2008307 BDD nodes
size of Y1635 = 2.62e+18 states, 2008387 BDD nodes
size of Y1636 = 2.62e+18 states, 2008467 BDD nodes
size of Y1637 = 2.62e+18 states, 2008547 BDD nodes
size of Y1638 = 2.62e+18 states, 2008627 BDD nodes
size of Y1639 = 2.62e+18 states, 2008707 BDD nodes
size of Y1640 = 2.62e+18 states, 2008787 BDD nodes
size of Y1641 = 2.62e+18 states, 2008867 BDD nodes
size of Y1642 = 2.62e+18 states, 2008947 BDD nodes
size of Y1643 = 2.62e+18 states, 2009027 BDD nodes
size of Y1644 = 2.62e+18 states, 2009107 BDD nodes
size of Y1645 = 2.62e+18 states, 2009187 BDD nodes
size of Y1646 = 2.62e+18 states, 2009267 BDD nodes
size of Y1647 = 2.62001e+18 states, 2009347 BDD nodes
size of Y1648 = 2.62001e+18 states, 2009427 BDD nodes
size of Y1649 = 2.62001e+18 states, 2009507 BDD nodes
size of Y1650 = 2.62001e+18 states, 2009587 BDD nodes
size of Y1651 = 2.62001e+18 states, 2009667 BDD nodes
size of Y1652 = 2.62001e+18 states, 2009747 BDD nodes
size of Y1653 = 2.62001e+18 states, 2009827 BDD nodes
size of Y1654 = 2.62001e+18 states, 2009907 BDD nodes
size of Y1655 = 2.62001e+18 states, 2009987 BDD nodes
size of Y1656 = 2.62001e+18 states, 2010067 BDD nodes
size of Y1657 = 2.62001e+18 states, 2010147 BDD nodes
size of Y1658 = 2.62001e+18 states, 2010227 BDD nodes
size of Y1659 = 2.62001e+18 states, 2010307 BDD nodes
size of Y1660 = 2.62001e+18 states, 2010387 BDD nodes
size of Y1661 = 2.62001e+18 states, 2010467 BDD nodes
size of Y1662 = 2.62001e+18 states, 2010547 BDD nodes
size of Y1663 = 2.62001e+18 states, 2010627 BDD nodes
size of Y1664 = 2.62001e+18 states, 2010707 BDD nodes
size of Y1665 = 2.62001e+18 states, 2010787 BDD nodes
size of Y1666 = 2.62001e+18 states, 2010867 BDD nodes
size of Y1667 = 2.62001e+18 states, 2010947 BDD nodes
size of Y1668 = 2.62001e+18 states, 2011027 BDD nodes
size of Y1669 = 2.62002e+18 states, 2011107 BDD nodes
size of Y1670 = 2.62002e+18 states, 2011187 BDD nodes
size of Y1671 = 2.62002e+18 states, 2011267 BDD nodes
size of Y1672 = 2.62002e+18 states, 2011347 BDD nodes
size of Y1673 = 2.62002e+18 states, 2011427 BDD nodes
size of Y1674 = 2.62002e+18 states, 2011507 BDD nodes
size of Y1675 = 2.62002e+18 states, 2011587 BDD nodes
size of Y1676 = 2.62002e+18 states, 2011667 BDD nodes
size of Y1677 = 2.62002e+18 states, 2011747 BDD nodes
size of Y1678 = 2.62002e+18 states, 2011827 BDD nodes
size of Y1679 = 2.62002e+18 states, 2011907 BDD nodes
size of Y1680 = 2.62002e+18 states, 2011987 BDD nodes
size of Y1681 = 2.62002e+18 states, 2012067 BDD nodes
size of Y1682 = 2.62002e+18 states, 2012147 BDD nodes
size of Y1683 = 2.62002e+18 states, 2012227 BDD nodes
size of Y1684 = 2.62002e+18 states, 2012307 BDD nodes
size of Y1685 = 2.62002e+18 states, 2012387 BDD nodes
size of Y1686 = 2.62002e+18 states, 2012467 BDD nodes
size of Y1687 = 2.62002e+18 states, 2012547 BDD nodes
size of Y1688 = 2.62002e+18 states, 2012627 BDD nodes
size of Y1689 = 2.62002e+18 states, 2012707 BDD nodes
size of Y1690 = 2.62003e+18 states, 2012787 BDD nodes
size of Y1691 = 2.62003e+18 states, 2012867 BDD nodes
size of Y1692 = 2.62003e+18 states, 2012947 BDD nodes
size of Y1693 = 2.62003e+18 states, 2013027 BDD nodes
size of Y1694 = 2.62003e+18 states, 2013107 BDD nodes
size of Y1695 = 2.62003e+18 states, 2013187 BDD nodes
size of Y1696 = 2.62003e+18 states, 2013267 BDD nodes
size of Y1697 = 2.62003e+18 states, 2013347 BDD nodes
size of Y1698 = 2.62003e+18 states, 2013427 BDD nodes
size of Y1699 = 2.62003e+18 states, 2013507 BDD nodes
size of Y1700 = 2.62003e+18 states, 2013587 BDD nodes
size of Y1701 = 2.62003e+18 states, 2013667 BDD nodes
size of Y1702 = 2.62003e+18 states, 2013760 BDD nodes
size of Y1703 = 2.62003e+18 states, 2013840 BDD nodes
size of Y1704 = 2.62003e+18 states, 2013920 BDD nodes
size of Y1705 = 2.62003e+18 states, 2014000 BDD nodes
size of Y1706 = 2.62003e+18 states, 2014080 BDD nodes
size of Y1707 = 2.62003e+18 states, 2014160 BDD nodes
size of Y1708 = 2.62003e+18 states, 2014240 BDD nodes
size of Y1709 = 2.62003e+18 states, 2014320 BDD nodes
size of Y1710 = 2.62003e+18 states, 2014400 BDD nodes
size of Y1711 = 2.62004e+18 states, 2014480 BDD nodes
size of Y1712 = 2.62004e+18 states, 2014560 BDD nodes
size of Y1713 = 2.62004e+18 states, 2014640 BDD nodes
size of Y1714 = 2.62004e+18 states, 2014720 BDD nodes
size of Y1715 = 2.62004e+18 states, 2014800 BDD nodes
size of Y1716 = 2.62004e+18 states, 2014880 BDD nodes
size of Y1717 = 2.62004e+18 states, 2014960 BDD nodes
size of Y1718 = 2.62004e+18 states, 2015040 BDD nodes
size of Y1719 = 2.62004e+18 states, 2015120 BDD nodes
size of Y1720 = 2.62004e+18 states, 2015200 BDD nodes
size of Y1721 = 2.62004e+18 states, 2015280 BDD nodes
size of Y1722 = 2.62004e+18 states, 2015360 BDD nodes
size of Y1723 = 2.62004e+18 states, 2015439 BDD nodes
size of Y1724 = 2.62004e+18 states, 2015518 BDD nodes
size of Y1725 = 2.62004e+18 states, 2015597 BDD nodes
size of Y1726 = 2.62004e+18 states, 2015676 BDD nodes
size of Y1727 = 2.62004e+18 states, 2015754 BDD nodes
size of Y1728 = 2.62004e+18 states, 2015832 BDD nodes
size of Y1729 = 2.62004e+18 states, 2015907 BDD nodes
size of Y1730 = 2.62004e+18 states, 2015981 BDD nodes
size of Y1731 = 2.62004e+18 states, 2016053 BDD nodes
size of Y1732 = 2.62004e+18 states, 2016125 BDD nodes
size of Y1733 = 2.62005e+18 states, 2016195 BDD nodes
size of Y1734 = 2.62005e+18 states, 2016265 BDD nodes
size of Y1735 = 2.62005e+18 states, 2016333 BDD nodes
size of Y1736 = 2.62005e+18 states, 2016399 BDD nodes
size of Y1737 = 2.62005e+18 states, 2016460 BDD nodes
size of Y1738 = 2.62005e+18 states, 2016521 BDD nodes
size of Y1739 = 2.62005e+18 states, 2016582 BDD nodes
size of Y1740 = 2.62005e+18 states, 2016643 BDD nodes
size of Y1741 = 2.62005e+18 states, 2016704 BDD nodes
size of Y1742 = 2.62005e+18 states, 2016765 BDD nodes
size of Y1743 = 2.62005e+18 states, 2016826 BDD nodes
size of Y1744 = 2.62005e+18 states, 2016887 BDD nodes
size of Y1745 = 2.62005e+18 states, 2016948 BDD nodes
size of Y1746 = 2.62005e+18 states, 2017009 BDD nodes
size of Y1747 = 2.62005e+18 states, 2017070 BDD nodes
size of Y1748 = 2.62005e+18 states, 2017131 BDD nodes
size of Y1749 = 2.62005e+18 states, 2017192 BDD nodes
size of Y1750 = 2.62005e+18 states, 2017253 BDD nodes
size of Y1751 = 2.62005e+18 states, 2017314 BDD nodes
size of Y1752 = 2.62005e+18 states, 2017375 BDD nodes
size of Y1753 = 2.62005e+18 states, 2017436 BDD nodes
size of Y1754 = 2.62006e+18 states, 2017497 BDD nodes
size of Y1755 = 2.62006e+18 states, 2017558 BDD nodes
size of Y1756 = 2.62006e+18 states, 2017619 BDD nodes
size of Y1757 = 2.62006e+18 states, 2017680 BDD nodes
size of Y1758 = 2.62006e+18 states, 2017741 BDD nodes
size of Y1759 = 2.62006e+18 states, 2017802 BDD nodes
size of Y1760 = 2.62006e+18 states, 2017863 BDD nodes
size of Y1761 = 2.62006e+18 states, 2017924 BDD nodes
size of Y1762 = 2.62006e+18 states, 2017985 BDD nodes
size of Y1763 = 2.62006e+18 states, 2018046 BDD nodes
size of Y1764 = 2.62006e+18 states, 2018107 BDD nodes
size of Y1765 = 2.62006e+18 states, 2018168 BDD nodes
size of Y1766 = 2.62006e+18 states, 2018229 BDD nodes
size of Y1767 = 2.62006e+18 states, 2018290 BDD nodes
size of Y1768 = 2.62006e+18 states, 2018351 BDD nodes
size of Y1769 = 2.62006e+18 states, 2018412 BDD nodes
size of Y1770 = 2.62006e+18 states, 2018473 BDD nodes
size of Y1771 = 2.62006e+18 states, 2018534 BDD nodes
size of Y1772 = 2.62006e+18 states, 2018595 BDD nodes
size of Y1773 = 2.62006e+18 states, 2018656 BDD nodes
size of Y1774 = 2.62006e+18 states, 2018717 BDD nodes
size of Y1775 = 2.62006e+18 states, 2018778 BDD nodes
size of Y1776 = 2.62007e+18 states, 2018839 BDD nodes
size of Y1777 = 2.62007e+18 states, 2018900 BDD nodes
size of Y1778 = 2.62007e+18 states, 2018961 BDD nodes
size of Y1779 = 2.62007e+18 states, 2019044 BDD nodes
size of Y1780 = 2.62007e+18 states, 2019101 BDD nodes
size of Y1781 = 2.62007e+18 states, 2019158 BDD nodes
size of Y1782 = 2.62007e+18 states, 2019215 BDD nodes
size of Y1783 = 2.62007e+18 states, 2019272 BDD nodes
size of Y1784 = 2.62007e+18 states, 2019329 BDD nodes
size of Y1785 = 2.62007e+18 states, 2019386 BDD nodes
size of Y1786 = 2.62007e+18 states, 2019443 BDD nodes
size of Y1787 = 2.62007e+18 states, 2019500 BDD nodes
size of Y1788 = 2.62007e+18 states, 2019563 BDD nodes
size of Y1789 = 2.62007e+18 states, 2019620 BDD nodes
size of Y1790 = 2.62007e+18 states, 2019677 BDD nodes
size of Y1791 = 2.62007e+18 states, 2019734 BDD nodes
size of Y1792 = 2.62007e+18 states, 2019791 BDD nodes
size of Y1793 = 2.62007e+18 states, 2019846 BDD nodes
size of Y1794 = 2.62007e+18 states, 2019901 BDD nodes
size of Y1795 = 2.62007e+18 states, 2019956 BDD nodes
size of Y1796 = 2.62007e+18 states, 2020011 BDD nodes
size of Y1797 = 2.62008e+18 states, 2020064 BDD nodes
size of Y1798 = 2.62008e+18 states, 2020117 BDD nodes
size of Y1799 = 2.62008e+18 states, 2020168 BDD nodes
size of Y1800 = 2.62008e+18 states, 2020217 BDD nodes
size of Y1801 = 2.62008e+18 states, 2020261 BDD nodes
size of Y1802 = 2.62008e+18 states, 2020305 BDD nodes
size of Y1803 = 2.62008e+18 states, 2020349 BDD nodes
size of Y1804 = 2.62008e+18 states, 2020393 BDD nodes
size of Y1805 = 2.62008e+18 states, 2020437 BDD nodes
size of Y1806 = 2.62008e+18 states, 2020481 BDD nodes
size of Y1807 = 2.62008e+18 states, 2020525 BDD nodes
size of Y1808 = 2.62008e+18 states, 2020569 BDD nodes
size of Y1809 = 2.62008e+18 states, 2020613 BDD nodes
size of Y1810 = 2.62008e+18 states, 2020666 BDD nodes
size of Y1811 = 2.62008e+18 states, 2020685 BDD nodes
size of Y1812 = 2.62008e+18 states, 2020704 BDD nodes
size of Y1813 = 2.62008e+18 states, 2020732 BDD nodes
size of Y1814 = 2.62008e+18 states, 2020736 BDD nodes
size of Y1815 = 2.62008e+18 states, 2020708 BDD nodes
size of Y1816 = 2.62008e+18 states, 2020677 BDD nodes
size of Y1817 = 2.62008e+18 states, 2020630 BDD nodes
size of Y1818 = 2.62008e+18 states, 2020522 BDD nodes
size of Y1819 = 2.62008e+18 states, 2020399 BDD nodes
size of Y1820 = 2.62008e+18 states, 2020226 BDD nodes
size of Y1821 = 2.62009e+18 states, 2020036 BDD nodes
size of Y1822 = 2.62009e+18 states, 2019917 BDD nodes
size of Y1823 = 2.62009e+18 states, 2019648 BDD nodes
size of Y1824 = 2.62009e+18 states, 2019364 BDD nodes
size of Y1825 = 2.62009e+18 states, 2019089 BDD nodes
size of Y1826 = 2.62009e+18 states, 2018790 BDD nodes
size of Y1827 = 2.62009e+18 states, 2018440 BDD nodes
size of Y1828 = 2.62009e+18 states, 2018090 BDD nodes
size of Y1829 = 2.62009e+18 states, 2017795 BDD nodes
size of Y1830 = 2.62009e+18 states, 2017566 BDD nodes
size of Y1831 = 2.62009e+18 states, 2017245 BDD nodes
size of Y1832 = 2.62009e+18 states, 2016923 BDD nodes
size of Y1833 = 2.62009e+18 states, 2016589 BDD nodes
size of Y1834 = 2.62009e+18 states, 2016257 BDD nodes
size of Y1835 = 2.62009e+18 states, 2015917 BDD nodes
size of Y1836 = 2.62009e+18 states, 2015585 BDD nodes
size of Y1837 = 2.62009e+18 states, 2015266 BDD nodes
size of Y1838 = 2.62009e+18 states, 2014944 BDD nodes
size of Y1839 = 2.62009e+18 states, 2014617 BDD nodes
size of Y1840 = 2.62009e+18 states, 2014293 BDD nodes
size of Y1841 = 2.62009e+18 states, 2013971 BDD nodes
size of Y1842 = 2.62009e+18 states, 2013647 BDD nodes
size of Y1843 = 2.62009e+18 states, 2013344 BDD nodes
size of Y1844 = 2.62009e+18 states, 2013017 BDD nodes
size of Y1845 = 2.62009e+18 states, 2012692 BDD nodes
size of Y1846 = 2.62009e+18 states, 2012375 BDD nodes
size of Y1847 = 2.62009e+18 states, 2012047 BDD nodes
size of Y1848 = 2.62009e+18 states, 2011718 BDD nodes
size of Y1849 = 2.62009e+18 states, 2011385 BDD nodes
size of Y1850 = 2.62009e+18 states, 2011052 BDD nodes
size of Y1851 = 2.62009e+18 states, 2010714 BDD nodes
size of Y1852 = 2.62009e+18 states, 2010379 BDD nodes
size of Y1853 = 2.62009e+18 states, 2010046 BDD nodes
size of Y1854 = 2.62009e+18 states, 2009716 BDD nodes
size of Y1855 = 2.62009e+18 states, 2009378 BDD nodes
size of Y1856 = 2.62009e+18 states, 2009037 BDD nodes
size of Y1857 = 2.62009e+18 states, 2008695 BDD nodes
size of Y1858 = 2.62009e+18 states, 2008354 BDD nodes
size of Y1859 = 2.62009e+18 states, 2008033 BDD nodes
size of Y1860 = 2.62009e+18 states, 2007689 BDD nodes
size of Y1861 = 2.62009e+18 states, 2007348 BDD nodes
size of Y1862 = 2.62009e+18 states, 2007045 BDD nodes
size of Y1863 = 2.62009e+18 states, 2006725 BDD nodes
size of Y1864 = 2.62009e+18 states, 2006383 BDD nodes
size of Y1865 = 2.62009e+18 states, 2006080 BDD nodes
size of Y1866 = 2.62009e+18 states, 2005812 BDD nodes
size of Y1867 = 2.62009e+18 states, 2005568 BDD nodes
size of Y1868 = 2.62009e+18 states, 2005316 BDD nodes
size of Y1869 = 2.62009e+18 states, 2005099 BDD nodes
size of Y1870 = 2.62009e+18 states, 2004899 BDD nodes
size of Y1871 = 2.6201e+18 states, 2004720 BDD nodes
size of Y1872 = 2.6201e+18 states, 2004594 BDD nodes
size of Y1873 = 2.6201e+18 states, 2004512 BDD nodes
size of Y1874 = 2.6201e+18 states, 2004547 BDD nodes
size of Y1875 = 2.62011e+18 states, 2004545 BDD nodes
size of Y1876 = 2.62011e+18 states, 2004541 BDD nodes
size of Y1877 = 2.62011e+18 states, 2004521 BDD nodes
size of Y1878 = 2.62012e+18 states, 2004558 BDD nodes
size of Y1879 = 2.62012e+18 states, 2004562 BDD nodes
size of Y1880 = 2.62012e+18 states, 2004554 BDD nodes
size of Y1881 = 2.62012e+18 states, 2004559 BDD nodes
size of Y1882 = 2.62012e+18 states, 2004601 BDD nodes
size of Y1883 = 2.62012e+18 states, 2004611 BDD nodes
size of Y1884 = 2.62012e+18 states, 2004615 BDD nodes
size of Y1885 = 2.62012e+18 states, 2004619 BDD nodes
size of Y1886 = 2.62012e+18 states, 2004646 BDD nodes
size of Y1887 = 2.62012e+18 states, 2004675 BDD nodes
size of Y1888 = 2.62012e+18 states, 2004703 BDD nodes
size of Y1889 = 2.62012e+18 states, 2004726 BDD nodes
size of Y1890 = 2.62012e+18 states, 2004754 BDD nodes
size of Y1891 = 2.62012e+18 states, 2004769 BDD nodes
size of Y1892 = 2.62012e+18 states, 2004791 BDD nodes
size of Y1893 = 2.62012e+18 states, 2004811 BDD nodes
size of Y1894 = 2.62012e+18 states, 2004812 BDD nodes
size of Y1895 = 2.62012e+18 states, 2004830 BDD nodes
size of Y1896 = 2.62012e+18 states, 2004848 BDD nodes
size of Y1897 = 2.62012e+18 states, 2004863 BDD nodes
size of Y1898 = 2.62012e+18 states, 2004880 BDD nodes
size of Y1899 = 2.62012e+18 states, 2004896 BDD nodes
size of Y1900 = 2.62012e+18 states, 2004912 BDD nodes
size of Y1901 = 2.62012e+18 states, 2004940 BDD nodes
size of Y1902 = 2.62012e+18 states, 2004971 BDD nodes
size of Y1903 = 2.62012e+18 states, 2004983 BDD nodes
size of Y1904 = 2.62012e+18 states, 2004995 BDD nodes
size of Y1905 = 2.62012e+18 states, 2005008 BDD nodes
size of Y1906 = 2.62012e+18 states, 2005021 BDD nodes
size of Y1907 = 2.62012e+18 states, 2005011 BDD nodes
size of Y1908 = 2.62012e+18 states, 2005022 BDD nodes
size of Y1909 = 2.62012e+18 states, 2005032 BDD nodes
size of Y1910 = 2.62012e+18 states, 2005040 BDD nodes
size of Y1911 = 2.62012e+18 states, 2005051 BDD nodes
size of Y1912 = 2.62012e+18 states, 2005062 BDD nodes
size of Y1913 = 2.62012e+18 states, 2005070 BDD nodes
size of Y1914 = 2.62012e+18 states, 2005098 BDD nodes
size of Y1915 = 2.62012e+18 states, 2005118 BDD nodes
size of Y1916 = 2.62012e+18 states, 2005132 BDD nodes
size of Y1917 = 2.62012e+18 states, 2005138 BDD nodes
size of Y1918 = 2.62012e+18 states, 2005146 BDD nodes
size of Y1919 = 2.62012e+18 states, 2005147 BDD nodes
size of Y1920 = 2.62012e+18 states, 2005147 BDD nodes
size of Y1921 = 2.62012e+18 states, 2005145 BDD nodes
size of Y1922 = 2.62012e+18 states, 2005140 BDD nodes
size of Y1923 = 2.62012e+18 states, 2005125 BDD nodes
size of Y1924 = 2.62012e+18 states, 2005117 BDD nodes
size of Y1925 = 2.62012e+18 states, 2005109 BDD nodes
size of Y1926 = 2.62012e+18 states, 2005094 BDD nodes
size of Y1927 = 2.62012e+18 states, 2005086 BDD nodes
size of Y1928 = 2.62012e+18 states, 2005078 BDD nodes
size of Y1929 = 2.62012e+18 states, 2005070 BDD nodes
size of Y1930 = 2.62012e+18 states, 2005062 BDD nodes
size of Y1931 = 2.62012e+18 states, 2005054 BDD nodes
size of Y1932 = 2.62012e+18 states, 2005046 BDD nodes
size of Y1933 = 2.62012e+18 states, 2005038 BDD nodes
size of Y1934 = 2.62012e+18 states, 2005042 BDD nodes
size of Y1935 = 2.62012e+18 states, 2005034 BDD nodes
size of Y1936 = 2.62012e+18 states, 2005026 BDD nodes
size of Y1937 = 2.62012e+18 states, 2005019 BDD nodes
size of Y1938 = 2.62012e+18 states, 2005012 BDD nodes
size of Y1939 = 2.62012e+18 states, 2004989 BDD nodes
size of Y1940 = 2.62012e+18 states, 2004980 BDD nodes
size of Y1941 = 2.62012e+18 states, 2004970 BDD nodes
size of Y1942 = 2.62012e+18 states, 2004958 BDD nodes
size of Y1943 = 2.62012e+18 states, 2004949 BDD nodes
size of Y1944 = 2.62012e+18 states, 2004940 BDD nodes
size of Y1945 = 2.62012e+18 states, 2004928 BDD nodes
size of Y1946 = 2.62012e+18 states, 2004918 BDD nodes
size of Y1947 = 2.62012e+18 states, 2004911 BDD nodes
size of Y1948 = 2.62012e+18 states, 2004899 BDD nodes
size of Y1949 = 2.62012e+18 states, 2004885 BDD nodes
size of Y1950 = 2.62012e+18 states, 2004873 BDD nodes
size of Y1951 = 2.62012e+18 states, 2004854 BDD nodes
size of Y1952 = 2.62012e+18 states, 2004834 BDD nodes
size of Y1953 = 2.62012e+18 states, 2004812 BDD nodes
size of Y1954 = 2.62012e+18 states, 2004787 BDD nodes
size of Y1955 = 2.62012e+18 states, 2004752 BDD nodes
size of Y1956 = 2.62012e+18 states, 2004724 BDD nodes
size of Y1957 = 2.62012e+18 states, 2004696 BDD nodes
size of Y1958 = 2.62012e+18 states, 2004668 BDD nodes
size of Y1959 = 2.62012e+18 states, 2004640 BDD nodes
size of Y1960 = 2.62012e+18 states, 2004612 BDD nodes
size of Y1961 = 2.62012e+18 states, 2004584 BDD nodes
size of Y1962 = 2.62012e+18 states, 2004556 BDD nodes
size of Y1963 = 2.62012e+18 states, 2004526 BDD nodes
size of Y1964 = 2.62012e+18 states, 2004497 BDD nodes
size of Y1965 = 2.62012e+18 states, 2004495 BDD nodes
size of Y1966 = 2.62012e+18 states, 2004470 BDD nodes
size of Y1967 = 2.62012e+18 states, 2004476 BDD nodes
size of Y1968 = 2.62012e+18 states, 2004443 BDD nodes
size of Y1969 = 2.62012e+18 states, 2004408 BDD nodes
size of Y1970 = 2.62012e+18 states, 2004369 BDD nodes
size of Y1971 = 2.62012e+18 states, 2004326 BDD nodes
size of Y1972 = 2.62012e+18 states, 2004284 BDD nodes
size of Y1973 = 2.62012e+18 states, 2004241 BDD nodes
size of Y1974 = 2.62012e+18 states, 2004197 BDD nodes
size of Y1975 = 2.62012e+18 states, 2004161 BDD nodes
size of Y1976 = 2.62012e+18 states, 2004108 BDD nodes
size of Y1977 = 2.62012e+18 states, 2004059 BDD nodes
size of Y1978 = 2.62012e+18 states, 2004026 BDD nodes
size of Y1979 = 2.62012e+18 states, 2004017 BDD nodes
size of Y1980 = 2.62012e+18 states, 2003981 BDD nodes
size of Y1981 = 2.62012e+18 states, 2003937 BDD nodes
size of Y1982 = 2.62012e+18 states, 2003904 BDD nodes
size of Y1983 = 2.62012e+18 states, 2003861 BDD nodes
size of Y1984 = 2.62012e+18 states, 2003835 BDD nodes
size of Y1985 = 2.62012e+18 states, 2003811 BDD nodes
size of Y1986 = 2.62012e+18 states, 2003798 BDD nodes
size of Y1987 = 2.62013e+18 states, 2003831 BDD nodes
-- specification  AG (START4 -> TIME < 1100)  is true
######################################################################
Runtime Statistics
------------------
Machine name: node-xeon-8
User time   28153.420 seconds
System time 311.530 seconds

Average resident text size       =     0K
Average resident data+stack size =     0K
Maximum resident size            =     0K

Virtual text size                = 132044K
Virtual data size                = 215817K
    data size initialized        =   234K
    data size uninitialized      =   362K
    data size sbrk               = 215221K
Virtual memory limit             = 4194304K (4194304K)

Major page faults = 400
Minor page faults = 33249483
Swaps = 0
Input blocks = 0
Output blocks = 0
Context switch (voluntary) = 0
Context switch (involuntary) = 0
######################################################################
BDD statistics
--------------------
BDD nodes allocated: 2303246
--------------------
BDD nodes representing init set of states: 34
BDD nodes representing state constraints: 2892
BDD nodes representing input constraints: 1
Forward Partitioning Schedule BDD cluster size (#nodes):
cluster 1	:	5415
cluster 2	:	3096
Backward Partitioning Schedule BDD cluster size (#nodes):
cluster 1	:	5415
cluster 2	:	3096