1/* BDD Calculator data file */ 2 3initial 13000 10000; 4 5inputs 6_1 _13 _20 _33 _41 _45 _50 _58 _68 _77 7_87 _97 _107 _116 _124 _125 _128 _132 _137 _143 8_150 _159 _169 _179 _190 _200 _213 _222 _223 _226 9_232 _238 _244 _250 _257 _264 _270 _274 _283 _294 10_303 _311 _317 _322 _326 _329 _330 _343 _1698 _2897 11; 12 13actions 14autoreorder 0 sift; 15 16t695 = _330; 17t9 = _1; 18t10 = _13; 19t11 = t9 and t10; 20t154 = _33; 21t180 = _41; 22t181 = t154 and t180; 23t182 = not t181; 24t183 = t11 and t182; 25t184 = not t183; 26t47 = _270; 27t322 = t184 and t47; 28t186 = not t9; 29t187 = _45; 30t188 = t186 and t187; 31t189 = not t180; 32t190 = t188 and t189; 33t191 = not t190; 34t323 = t322 and t191; 35t193 = _274; 36t194 = t184 and t193; 37t195 = t194 and t190; 38t324 = t323 or t195; 39t325 = _303; 40t155 = not t154; 41t198 = not t155; 42t326 = t325 and t198; 43t17 = _257; 44t200 = _1698; 45t201 = t200 or t154; 46t202 = not t201; 47t327 = t17 and t202; 48t328 = t326 or t327; 49t18 = _264; 50t205 = t155 and t201; 51t329 = t18 and t205; 52t330 = t328 or t329; 53t331 = t183 and t330; 54t332 = t324 or t331; 55t185 = t184 and t18; 56t192 = t185 and t191; 57t196 = t192 or t195; 58t197 = _294; 59t199 = t197 and t198; 60t16 = _250; 61t203 = t16 and t202; 62t204 = t199 or t203; 63t206 = t17 and t205; 64t207 = t204 or t206; 65t208 = t183 and t207; 66t209 = t196 or t208; 67t241 = t184 and t16; 68t242 = not t188; 69t243 = t241 and t242; 70t244 = t194 and t188; 71t245 = t243 or t244; 72t48 = _116; 73t246 = t48 and t198; 74t27 = _238; 75t247 = t27 and t202; 76t248 = t246 or t247; 77t35 = _244; 78t249 = t35 and t205; 79t250 = t248 or t249; 80t251 = t183 and t250; 81t252 = t245 or t251; 82t283 = t184 and t17; 83t284 = t283 and t191; 84t285 = t284 or t195; 85t286 = _283; 86t287 = t286 and t198; 87t288 = t35 and t202; 88t289 = t287 or t288; 89t290 = t16 and t205; 90t291 = t289 or t290; 91t292 = t183 and t291; 92t293 = t285 or t292; 93t744 = t252 and t293; 94t745 = t209 and t744; 95t746 = t332 and t745; 96t211 = _179; 97t747 = not t211; 98t748 = t746 and t747; 99t335 = not t332; 100t213 = not t209; 101t255 = not t252; 102t296 = not t293; 103t749 = t255 and t296; 104t750 = t213 and t749; 105t751 = t335 and t750; 106t752 = t751 and t211; 107t753 = t748 or t752; 108t696 = t186 and t10; 109t12 = _20; 110t151 = not t12; 111t697 = t696 and t151; 112t698 = _213; 113t699 = t697 and t698; 114t700 = _343; 115t716 = t699 nand t700; 116t754 = not t716; 117t755 = t753 and t754; 118t150 = _169; 119t39 = _107; 120t103 = not t39; 121t152 = not t151; 122t153 = t103 and t152; 123t156 = t155 or t12; 124t157 = not t156; 125t158 = t48 and t157; 126t159 = t153 or t158; 127t41 = _87; 128t160 = t151 and t156; 129t161 = t41 and t160; 130t162 = t159 or t161; 131t163 = t9 nand t10; 132t164 = t9 and t12; 133t165 = t164 nand t154; 134t166 = t163 and t165; 135t167 = not t166; 136t168 = t162 and t167; 137t169 = t10 and t12; 138t170 = not t169; 139t171 = t9 or t170; 140t172 = t39 nor t171; 141t173 = t168 or t172; 142t174 = t155 or t9; 143t175 = t39 and t174; 144t176 = t166 and t171; 145t177 = t175 and t176; 146t178 = t173 or t177; 147t179 = t150 and t178; 148t210 = t179 and t209; 149t212 = t211 and t178; 150t214 = t212 and t213; 151t215 = t210 nor t214; 152t216 = _190; 153t217 = t173 nor t177; 154t218 = t216 and t217; 155t219 = t218 and t213; 156t220 = _200; 157t221 = t220 and t217; 158t222 = t221 and t209; 159t223 = t219 or t222; 160t224 = not t217; 161t225 = t223 or t224; 162t226 = t215 and t225; 163t110 = not t41; 164t43 = _97; 165t109 = not t43; 166t227 = t110 and t109; 167t228 = t227 nand t103; 168t229 = t228 and t152; 169t230 = t43 and t157; 170t231 = t229 or t230; 171t5 = _68; 172t232 = t5 and t160; 173t233 = t231 or t232; 174t234 = t233 and t167; 175t235 = t41 nor t171; 176t236 = t234 or t235; 177t237 = t41 and t174; 178t238 = t237 and t176; 179t239 = t236 or t238; 180t240 = t150 and t239; 181t253 = t240 and t252; 182t254 = t211 and t239; 183t256 = t254 and t255; 184t257 = t253 nor t256; 185t258 = t236 nor t238; 186t259 = t216 and t258; 187t260 = t259 and t255; 188t261 = t220 and t258; 189t262 = t261 and t252; 190t263 = t260 or t262; 191t264 = not t258; 192t265 = t263 or t264; 193t266 = t257 and t265; 194t267 = t39 nand t109; 195t268 = t43 nand t103; 196t269 = t267 nand t268; 197t270 = not t269; 198t271 = t270 and t152; 199t272 = t39 and t157; 200t273 = t271 or t272; 201t36 = _77; 202t274 = t36 and t160; 203t275 = t273 or t274; 204t276 = t275 and t167; 205t277 = t43 nor t171; 206t278 = t276 or t277; 207t279 = t43 and t174; 208t280 = t279 and t176; 209t281 = t278 or t280; 210t282 = t150 and t281; 211t294 = t282 and t293; 212t295 = t211 and t281; 213t297 = t295 and t296; 214t298 = t294 nor t297; 215t299 = t278 nor t280; 216t300 = t216 and t299; 217t301 = t300 and t296; 218t302 = t220 and t299; 219t303 = t302 and t293; 220t304 = t301 or t303; 221t305 = not t299; 222t306 = t304 or t305; 223t307 = t298 and t306; 224t308 = t266 and t307; 225t309 = t226 and t308; 226t310 = t48 and t152; 227t311 = t286 and t157; 228t312 = t310 or t311; 229t313 = t43 and t160; 230t314 = t312 or t313; 231t315 = t314 and t167; 232t316 = t48 nor t171; 233t317 = t315 or t316; 234t318 = t48 and t174; 235t319 = t318 and t176; 236t320 = t317 or t319; 237t321 = t150 and t320; 238t333 = t321 and t332; 239t334 = t211 and t320; 240t336 = t334 and t335; 241t337 = t333 nor t336; 242t338 = t317 nor t319; 243t339 = t216 and t338; 244t340 = t339 and t335; 245t341 = t220 and t338; 246t342 = t341 and t332; 247t343 = t340 or t342; 248t344 = not t338; 249t345 = t343 or t344; 250t346 = t337 and t345; 251t347 = t309 and t346; 252t756 = t347 and t716; 253t757 = t755 or t756; 254t758 = t695 and t757; 255t701 = t699 and t700; 256t473 = t36 and t152; 257t474 = t41 and t157; 258t475 = t473 or t474; 259t3 = _58; 260t476 = t3 and t160; 261t477 = t475 or t476; 262t478 = t477 and t167; 263t479 = t36 nor t171; 264t480 = t478 or t479; 265t356 = t151 or t9; 266t481 = t36 and t356; 267t482 = t481 and t176; 268t483 = t480 or t482; 269t938 = t701 and t483; 270t484 = t150 and t483; 271t485 = t184 and t35; 272t362 = t180 or t187; 273t363 = t186 and t362; 274t364 = not t363; 275t486 = t485 and t364; 276t366 = t194 and t363; 277t487 = t486 or t366; 278t488 = t39 and t198; 279t31 = _232; 280t489 = t31 and t202; 281t490 = t488 or t489; 282t491 = t27 and t205; 283t492 = t490 or t491; 284t493 = t183 and t492; 285t494 = t487 or t493; 286t495 = t484 and t494; 287t496 = t211 and t483; 288t497 = not t494; 289t498 = t496 and t497; 290t499 = t495 nor t498; 291t500 = t480 nor t482; 292t501 = t216 and t500; 293t502 = t501 and t497; 294t503 = t220 and t500; 295t504 = t503 and t494; 296t505 = t502 or t504; 297t506 = not t500; 298t507 = t505 or t506; 299t508 = t499 and t507; 300t939 = not t508; 301t940 = t938 nand t939; 302t941 = not t938; 303t942 = t508 nand t941; 304t943 = t940 nand t942; 305t634 = t210 or t214; 306t635 = t308 nand t634; 307t636 = t253 or t256; 308t637 = not t636; 309t638 = t294 or t297; 310t639 = t266 nand t638; 311t640 = t637 and t639; 312t641 = t635 and t640; 313t642 = t333 or t336; 314t643 = t642 and t307; 315t644 = t226 and t643; 316t645 = t644 nand t266; 317t646 = t641 nand t645; 318t759 = t646 and t716; 319t760 = not t759; 320t944 = t943 nand t760; 321t945 = not t943; 322t946 = t759 nand t945; 323t947 = t944 nand t946; 324t948 = not t947; 325t949 = t758 nand t948; 326t950 = not t758; 327t951 = t947 nand t950; 328t952 = t949 nand t951; 329t798 = t10 and t151; 330t799 = t798 nand t187; 331t800 = t9 and t799; 332t801 = not t800; 333t953 = t952 and t801; 334t21 = not t10; 335t22 = t9 and t21; 336t740 = t12 and t22; 337t741 = t740 nand t189; 338t742 = not t741; 339t954 = t952 and t742; 340t955 = t953 or t954; 341t956 = _143; 342t805 = t151 or t216; 343t806 = not t220; 344t807 = t12 and t211; 345t808 = t806 and t807; 346t809 = t805 nand t808; 347t810 = not t809; 348t957 = t956 and t810; 349t394 = _150; 350t812 = t151 nor t216; 351t813 = t220 and t807; 352t814 = t812 nand t813; 353t815 = not t814; 354t958 = t394 and t815; 355t437 = _159; 356t817 = t812 nand t808; 357t818 = not t817; 358t959 = t437 and t818; 359t2 = _50; 360t820 = t12 and t220; 361t821 = not t807; 362t822 = t820 and t821; 363t823 = t805 nand t822; 364t824 = not t823; 365t960 = t2 and t824; 366t826 = t12 nand t220; 367t827 = t826 and t821; 368t828 = t805 nand t827; 369t829 = not t828; 370t961 = t3 and t829; 371t962 = _132; 372t831 = t812 nand t827; 373t832 = not t831; 374t963 = t962 and t832; 375t834 = t812 nand t822; 376t835 = not t834; 377t964 = t5 and t835; 378t965 = t963 or t964; 379t966 = t961 or t965; 380t967 = t960 or t966; 381t968 = t959 or t967; 382t969 = t958 or t968; 383t970 = t957 or t969; 384t971 = _137; 385t843 = t805 nand t813; 386t844 = not t843; 387t972 = t971 and t844; 388t973 = t970 nor t972; 389t974 = t973 and t155; 390t975 = t197 and t810; 391t976 = t286 and t815; 392t977 = t48 and t818; 393t978 = t39 and t824; 394t830 = t43 and t829; 395t852 = _311; 396t979 = t852 and t832; 397t980 = t41 and t835; 398t981 = t979 or t980; 399t982 = t830 or t981; 400t983 = t978 or t982; 401t984 = t977 or t983; 402t985 = t976 or t984; 403t986 = t975 or t985; 404t987 = t325 and t844; 405t988 = t986 nor t987; 406t989 = t988 and t154; 407t990 = t974 or t989; 408t870 = t151 or t150; 409t871 = t11 nand t870; 410t872 = not t871; 411t991 = t990 and t872; 412t992 = t21 nand t155; 413t993 = not t992; 414t994 = t945 and t993; 415t995 = t991 or t994; 416t121 = not t36; 417t996 = t871 and t992; 418t997 = t121 and t996; 419t998 = t995 nor t997; 420t900 = t800 and t741; 421t999 = t998 and t900; 422t1000 = t955 or t999; 423t1001 = t955 nor t999; 424t1002 = not t1001; 425t1003 = t1000 and t1002; 426t511 = t193 and t190; 427t548 = t323 or t511; 428t549 = t548 or t331; 429t512 = t192 or t511; 430t513 = t512 or t208; 431t523 = t193 and t188; 432t524 = t243 or t523; 433t525 = t524 or t251; 434t535 = t284 or t511; 435t536 = t535 or t292; 436t773 = t525 and t536; 437t774 = t513 and t773; 438t775 = t549 and t774; 439t776 = t775 and t747; 440t551 = not t549; 441t515 = not t513; 442t527 = not t525; 443t538 = not t536; 444t777 = t527 and t538; 445t778 = t515 and t777; 446t779 = t551 and t778; 447t780 = t779 and t211; 448t781 = t776 or t780; 449t782 = t781 and t754; 450t514 = t179 and t513; 451t516 = t212 and t515; 452t517 = t514 nor t516; 453t518 = t216 and t515; 454t519 = t220 and t513; 455t520 = t518 or t519; 456t521 = t520 or t224; 457t522 = t517 and t521; 458t526 = t240 and t525; 459t528 = t254 and t527; 460t529 = t526 nor t528; 461t530 = t216 and t527; 462t531 = t220 and t525; 463t532 = t530 or t531; 464t533 = t532 or t264; 465t534 = t529 and t533; 466t537 = t282 and t536; 467t539 = t295 and t538; 468t540 = t537 nor t539; 469t541 = t216 and t538; 470t542 = t220 and t536; 471t543 = t541 or t542; 472t544 = t543 or t305; 473t545 = t540 and t544; 474t546 = t534 and t545; 475t547 = t522 and t546; 476t550 = t321 and t549; 477t552 = t334 and t551; 478t553 = t550 nor t552; 479t554 = t216 and t551; 480t555 = t220 and t549; 481t556 = t554 or t555; 482t557 = t556 or t344; 483t558 = t553 and t557; 484t559 = t547 and t558; 485t783 = t559 and t716; 486t784 = t782 or t783; 487t785 = t695 and t784; 488t614 = t481 and t166; 489t615 = t480 or t614; 490t1004 = t701 and t615; 491t616 = t150 and t615; 492t563 = t193 and t363; 493t617 = t486 or t563; 494t618 = t617 or t493; 495t619 = t616 and t618; 496t620 = t211 and t615; 497t621 = not t618; 498t622 = t620 and t621; 499t623 = t619 nor t622; 500t624 = t216 and t621; 501t625 = t220 and t618; 502t626 = t624 or t625; 503t627 = t480 nor t614; 504t628 = not t627; 505t629 = t626 or t628; 506t630 = t623 and t629; 507t1005 = not t630; 508t1006 = t1004 nand t1005; 509t1007 = not t1004; 510t1008 = t630 nand t1007; 511t1009 = t1006 nand t1008; 512t664 = t514 or t516; 513t665 = t546 nand t664; 514t666 = t526 or t528; 515t667 = not t666; 516t668 = t537 or t539; 517t669 = t534 nand t668; 518t670 = t667 and t669; 519t671 = t665 and t670; 520t672 = t550 or t552; 521t673 = t672 and t545; 522t674 = t522 and t673; 523t675 = t674 nand t534; 524t676 = t671 nand t675; 525t786 = t676 and t716; 526t1010 = not t786; 527t1011 = t1009 nand t1010; 528t1012 = not t1009; 529t1013 = t786 nand t1012; 530t1014 = t1011 nand t1013; 531t1015 = not t1014; 532t1016 = t785 nand t1015; 533t1017 = not t785; 534t1018 = t1014 nand t1017; 535t1019 = t1016 nand t1018; 536t1020 = t1019 and t801; 537t1021 = t1019 and t742; 538t1022 = t1020 or t1021; 539t913 = t10 nand t870; 540t914 = not t913; 541t1023 = t990 and t914; 542t1024 = not t1005; 543t1025 = not t1024; 544t1026 = t1025 and t993; 545t1027 = t1023 or t1026; 546t1028 = t913 and t992; 547t1029 = t121 and t1028; 548t1030 = t1027 nor t1029; 549t1031 = t1030 and t900; 550t1032 = t1022 nor t1031; 551t1033 = not t1032; 552t1034 = t1003 biimp t1033; 553t4 = not t3; 554t430 = t5 nand t4; 555t6 = not t5; 556t431 = t3 nand t6; 557t432 = t430 nand t431; 558t1035 = t432 and t36; 559t127 = not t2; 560t1036 = not t127; 561t1037 = t1035 and t1036; 562t1038 = t5 and t127; 563t1039 = t1037 or t1038; 564t1040 = t9 nand t21; 565t1041 = not t1040; 566t1042 = t1039 and t1041; 567t1043 = t48 and t269; 568t13 = t11 nand t12; 569t14 = not t13; 570t1044 = t1043 and t14; 571t1045 = t1042 or t1044; 572t348 = t6 and t152; 573t349 = t36 and t157; 574t350 = t348 or t349; 575t351 = t2 and t160; 576t352 = t350 or t351; 577t353 = t352 and t167; 578t354 = t5 nor t171; 579t355 = t353 or t354; 580t357 = t5 and t356; 581t358 = t357 and t176; 582t359 = t355 or t358; 583t1046 = t701 and t359; 584t360 = t150 and t359; 585t361 = t184 and t27; 586t365 = t361 and t364; 587t367 = t365 or t366; 588t368 = t43 and t198; 589t29 = _226; 590t369 = t29 and t202; 591t370 = t368 or t369; 592t371 = t31 and t205; 593t372 = t370 or t371; 594t373 = t183 and t372; 595t374 = t367 or t373; 596t375 = t360 and t374; 597t376 = t211 and t359; 598t377 = not t374; 599t378 = t376 and t377; 600t379 = t375 nor t378; 601t380 = t355 nor t358; 602t381 = t216 and t380; 603t382 = t381 and t377; 604t383 = t220 and t380; 605t384 = t383 and t374; 606t385 = t382 or t384; 607t386 = not t380; 608t387 = t385 or t386; 609t388 = t379 and t387; 610t1047 = not t388; 611t1048 = t1046 nand t1047; 612t1049 = not t1046; 613t1050 = t388 nand t1049; 614t1051 = t1048 nand t1050; 615t433 = not t432; 616t434 = t433 and t152; 617t435 = t5 and t157; 618t436 = t434 or t435; 619t438 = t437 and t160; 620t439 = t436 or t438; 621t440 = t439 and t167; 622t441 = t3 nor t171; 623t442 = t440 or t441; 624t443 = t3 and t356; 625t444 = t443 and t176; 626t445 = t442 or t444; 627t1052 = t699 and t445; 628t446 = t150 and t445; 629t447 = t184 and t31; 630t448 = t447 and t364; 631t449 = t448 or t366; 632t450 = t41 and t198; 633t411 = _223; 634t451 = t411 and t202; 635t452 = t450 or t451; 636t453 = t29 and t205; 637t454 = t452 or t453; 638t455 = t183 and t454; 639t456 = t449 or t455; 640t457 = t446 and t456; 641t458 = t211 and t445; 642t459 = not t456; 643t460 = t458 and t459; 644t461 = t457 nor t460; 645t462 = t442 nor t444; 646t463 = t216 and t462; 647t464 = t463 and t459; 648t465 = t220 and t462; 649t466 = t465 and t456; 650t467 = t464 or t466; 651t468 = not t462; 652t469 = t467 or t468; 653t470 = t461 and t469; 654t1053 = not t470; 655t1054 = t1052 nand t1053; 656t1055 = not t1052; 657t1056 = t470 nand t1055; 658t1057 = t1054 nand t1056; 659t1058 = t757 and t1057; 660t1059 = t1051 and t1058; 661t1060 = t1059 and t943; 662t389 = t127 and t4; 663t390 = t389 nand t6; 664t391 = t390 and t152; 665t392 = t3 and t157; 666t393 = t391 or t392; 667t395 = t394 and t160; 668t396 = t393 or t395; 669t397 = t396 and t167; 670t398 = t2 nor t171; 671t399 = t397 or t398; 672t400 = t2 and t356; 673t401 = t400 and t176; 674t402 = t399 or t401; 675t403 = t150 and t402; 676t404 = t184 and t29; 677t405 = t404 and t364; 678t406 = t405 or t366; 679t407 = t36 and t198; 680t408 = _222; 681t409 = t408 and t202; 682t410 = t407 or t409; 683t412 = t411 and t205; 684t413 = t410 or t412; 685t414 = t183 and t413; 686t415 = t406 or t414; 687t416 = t403 and t415; 688t417 = t211 and t402; 689t418 = not t415; 690t419 = t417 and t418; 691t420 = t416 nor t419; 692t421 = t399 nor t401; 693t422 = t216 and t421; 694t423 = t422 and t418; 695t424 = t220 and t421; 696t425 = t424 and t415; 697t426 = t423 or t425; 698t427 = not t421; 699t428 = t426 or t427; 700t429 = t420 and t428; 701t471 = t429 and t470; 702t472 = t388 and t471; 703t509 = t472 and t508; 704t1061 = t757 and t509; 705t1062 = not t1061; 706t1063 = t1060 nand t1062; 707t1064 = not t1060; 708t1065 = t1061 nand t1064; 709t1066 = t1063 nand t1065; 710t1067 = t695 and t1066; 711t648 = t375 or t378; 712t649 = t471 nand t648; 713t650 = t416 or t419; 714t651 = not t650; 715t652 = t457 or t460; 716t653 = t429 nand t652; 717t654 = t651 and t653; 718t655 = t649 and t654; 719t656 = t495 or t498; 720t657 = t656 and t470; 721t658 = t388 and t657; 722t659 = t658 nand t429; 723t660 = t655 nand t659; 724t1068 = t759 and t509; 725t1069 = t660 or t1068; 726t1070 = t1057 and t1051; 727t1071 = t656 and t716; 728t1072 = t1070 nand t1071; 729t1073 = t697 nand t698; 730t1074 = t652 and t1073; 731t1075 = not t1074; 732t1076 = t648 and t716; 733t1077 = t1057 nand t1076; 734t1078 = t1075 and t1077; 735t1079 = t1072 and t1078; 736t1080 = t943 and t1070; 737t1081 = t1080 nand t759; 738t1082 = t1079 nand t1081; 739t1083 = not t1082; 740t1084 = t1069 nand t1083; 741t1085 = not t1069; 742t1086 = t1082 nand t1085; 743t1087 = t1084 nand t1086; 744t1088 = not t1087; 745t1089 = t1067 nand t1088; 746t1090 = not t1067; 747t1091 = t1087 nand t1090; 748t1092 = t1089 nand t1091; 749t1093 = t1040 and t13; 750t1094 = t1092 and t1093; 751t1095 = t1045 or t1094; 752t1096 = t1045 nor t1094; 753t1097 = not t1096; 754t1098 = t1095 and t1097; 755t560 = t357 and t166; 756t561 = t355 or t560; 757t1099 = t701 and t561; 758t562 = t150 and t561; 759t564 = t365 or t563; 760t565 = t564 or t373; 761t566 = t562 and t565; 762t567 = t211 and t561; 763t568 = not t565; 764t569 = t567 and t568; 765t570 = t566 nor t569; 766t571 = t216 and t568; 767t572 = t220 and t565; 768t573 = t571 or t572; 769t574 = t355 nor t560; 770t575 = not t574; 771t576 = t573 or t575; 772t577 = t570 and t576; 773t1100 = not t577; 774t1101 = t1099 nand t1100; 775t1102 = not t1099; 776t1103 = t577 nand t1102; 777t1104 = t1101 nand t1103; 778t595 = t443 and t166; 779t596 = t442 or t595; 780t1105 = t699 and t596; 781t597 = t150 and t596; 782t598 = t448 or t563; 783t599 = t598 or t455; 784t600 = t597 and t599; 785t601 = t211 and t596; 786t602 = not t599; 787t603 = t601 and t602; 788t604 = t600 nor t603; 789t605 = t216 and t602; 790t606 = t220 and t599; 791t607 = t605 or t606; 792t608 = t442 nor t595; 793t609 = not t608; 794t610 = t607 or t609; 795t611 = t604 and t610; 796t1106 = not t611; 797t1107 = t1105 nand t1106; 798t1108 = not t1105; 799t1109 = t611 nand t1108; 800t1110 = t1107 nand t1109; 801t1111 = t784 and t1110; 802t1112 = t1104 and t1111; 803t1113 = t1112 and t1009; 804t578 = t400 and t166; 805t579 = t399 or t578; 806t580 = t150 and t579; 807t581 = t405 or t563; 808t582 = t581 or t414; 809t583 = t580 and t582; 810t584 = t211 and t579; 811t585 = not t582; 812t586 = t584 and t585; 813t587 = t583 nor t586; 814t588 = t216 and t585; 815t589 = t220 and t582; 816t590 = t588 or t589; 817t591 = t399 nor t578; 818t592 = not t591; 819t593 = t590 or t592; 820t594 = t587 and t593; 821t612 = t594 and t611; 822t613 = t577 and t612; 823t631 = t613 and t630; 824t1114 = t784 and t631; 825t1115 = not t1114; 826t1116 = t1113 nand t1115; 827t1117 = not t1113; 828t1118 = t1114 nand t1117; 829t1119 = t1116 nand t1118; 830t1120 = t695 and t1119; 831t678 = t566 or t569; 832t679 = t612 nand t678; 833t680 = t583 or t586; 834t681 = not t680; 835t682 = t600 or t603; 836t683 = t594 nand t682; 837t684 = t681 and t683; 838t685 = t679 and t684; 839t686 = t619 or t622; 840t687 = t686 and t611; 841t688 = t577 and t687; 842t689 = t688 nand t594; 843t690 = t685 nand t689; 844t1121 = t786 and t631; 845t1122 = t690 or t1121; 846t1123 = t1110 and t1104; 847t1124 = t686 and t716; 848t1125 = t1123 nand t1124; 849t1126 = t682 and t1073; 850t1127 = not t1126; 851t1128 = t678 and t716; 852t1129 = t1110 nand t1128; 853t1130 = t1127 and t1129; 854t1131 = t1125 and t1130; 855t1132 = t1009 and t1123; 856t1133 = t1132 nand t786; 857t1134 = t1131 nand t1133; 858t1135 = not t1134; 859t1136 = t1122 nand t1135; 860t1137 = not t1122; 861t1138 = t1134 nand t1137; 862t1139 = t1136 nand t1138; 863t1140 = not t1139; 864t1141 = t1120 nand t1140; 865t1142 = not t1120; 866t1143 = t1139 nand t1142; 867t1144 = t1141 nand t1143; 868t1145 = t1144 and t1093; 869t1146 = t1045 nor t1145; 870t1147 = not t1146; 871t1148 = t1098 biimp t1147; 872t702 = t701 and t320; 873t703 = not t346; 874t704 = t702 nand t703; 875t705 = not t702; 876t706 = t346 nand t705; 877t707 = t704 nand t706; 878t708 = t701 and t178; 879t709 = not t226; 880t710 = t708 nand t709; 881t711 = not t708; 882t712 = t226 nand t711; 883t713 = t710 nand t712; 884t714 = t707 and t713; 885t1149 = t701 and t281; 886t1150 = not t307; 887t1151 = t1149 nand t1150; 888t1152 = not t1149; 889t1153 = t307 nand t1152; 890t1154 = t1151 nand t1153; 891t1155 = t714 and t1154; 892t1156 = t695 and t1155; 893t1157 = t701 and t239; 894t1158 = not t266; 895t1159 = t1157 nand t1158; 896t1160 = not t1157; 897t1161 = t266 nand t1160; 898t1162 = t1159 nand t1161; 899t1163 = t638 and t716; 900t1164 = not t1163; 901t717 = t634 and t716; 902t1165 = t1154 nand t717; 903t1166 = t1164 and t1165; 904t1167 = t1154 and t713; 905t718 = t642 and t716; 906t1168 = t1167 nand t718; 907t1169 = t1166 nand t1168; 908t1170 = not t1169; 909t1171 = t1162 nand t1170; 910t1172 = not t1162; 911t1173 = t1169 nand t1172; 912t1174 = t1171 nand t1173; 913t1175 = not t1174; 914t1176 = t1156 nand t1175; 915t1177 = not t1156; 916t1178 = t1174 nand t1177; 917t1179 = t1176 nand t1178; 918t1180 = t1179 and t801; 919t1181 = not t1179; 920t761 = t758 and t760; 921t1182 = t761 nor t759; 922t1183 = t1181 nor t1182; 923t1184 = t695 and t707; 924t1185 = not t718; 925t1186 = t713 nand t1185; 926t1187 = not t713; 927t1188 = t718 nand t1187; 928t1189 = t1186 nand t1188; 929t1190 = not t1189; 930t1191 = t1184 nand t1190; 931t1192 = not t1184; 932t1193 = t1189 nand t1192; 933t1194 = t1191 nand t1193; 934t715 = t695 and t714; 935t719 = t713 and t718; 936t720 = t717 or t719; 937t721 = not t720; 938t1195 = t1154 nand t721; 939t1196 = not t1154; 940t1197 = t720 nand t1196; 941t1198 = t1195 nand t1197; 942t1199 = not t1198; 943t1200 = t715 nand t1199; 944t1201 = not t715; 945t1202 = t1198 nand t1201; 946t1203 = t1200 nand t1202; 947t1204 = t1194 and t1203; 948t1205 = t1179 and t1204; 949t1206 = t1205 and t1182; 950t1207 = t1183 or t1206; 951t1208 = t1207 and t742; 952t1209 = t1180 or t1208; 953t1210 = t394 and t810; 954t1211 = t437 and t815; 955t1212 = t2 and t818; 956t1213 = t3 and t824; 957t1214 = t5 and t829; 958t1215 = t971 and t832; 959t1216 = t36 and t835; 960t1217 = t1215 or t1216; 961t1218 = t1214 or t1217; 962t1219 = t1213 or t1218; 963t1220 = t1212 or t1219; 964t1221 = t1211 or t1220; 965t1222 = t1210 or t1221; 966t1223 = t956 and t844; 967t1224 = t1222 nor t1223; 968t1225 = t1224 and t155; 969t1226 = t325 and t810; 970t1227 = t197 and t815; 971t1228 = t286 and t818; 972t1229 = t48 and t824; 973t1230 = t39 and t829; 974t850 = _317; 975t1231 = t850 and t832; 976t1232 = t43 and t835; 977t1233 = t1231 or t1232; 978t1234 = t1230 or t1233; 979t1235 = t1229 or t1234; 980t1236 = t1228 or t1235; 981t1237 = t1227 or t1236; 982t1238 = t1226 or t1237; 983t1239 = t852 and t844; 984t1240 = t1238 nor t1239; 985t1241 = t1240 and t154; 986t1242 = t1225 or t1241; 987t1243 = t1242 and t872; 988t874 = t21 and t151; 989t875 = t874 nand t155; 990t876 = not t875; 991t1244 = t1172 and t876; 992t1245 = t1243 or t1244; 993t60 = not t18; 994t61 = t47 nand t60; 995t62 = not t47; 996t63 = t18 nand t62; 997t64 = t61 nand t63; 998t65 = not t16; 999t66 = t17 nand t65; 1000t67 = not t17; 1001t68 = t16 nand t67; 1002t69 = t66 nand t68; 1003t70 = not t69; 1004t71 = t64 nand t70; 1005t72 = not t64; 1006t73 = t69 nand t72; 1007t74 = t71 nand t73; 1008t884 = t22 and t12; 1009t885 = t884 nand t154; 1010t886 = not t885; 1011t1246 = t74 and t886; 1012t890 = t884 nand t155; 1013t891 = not t890; 1014t1247 = t1246 or t891; 1015t894 = t885 and t890; 1016t1248 = t110 and t894; 1017t1249 = t1247 or t1248; 1018t897 = t871 and t875; 1019t1250 = t1249 and t897; 1020t1251 = t1245 nor t1250; 1021t1252 = t1251 and t900; 1022t1253 = t1209 or t1252; 1023t1254 = t1209 nor t1252; 1024t1255 = not t1254; 1025t1256 = t1253 and t1255; 1026t724 = not t558; 1027t725 = t702 nand t724; 1028t726 = t558 nand t705; 1029t727 = t725 nand t726; 1030t728 = not t522; 1031t729 = t708 nand t728; 1032t730 = t522 nand t711; 1033t731 = t729 nand t730; 1034t732 = t727 and t731; 1035t1257 = not t545; 1036t1258 = t1149 nand t1257; 1037t1259 = t545 nand t1152; 1038t1260 = t1258 nand t1259; 1039t1261 = t732 and t1260; 1040t1262 = t695 and t1261; 1041t1263 = not t534; 1042t1264 = t1157 nand t1263; 1043t1265 = t534 nand t1160; 1044t1266 = t1264 nand t1265; 1045t1267 = t668 and t716; 1046t1268 = not t1267; 1047t734 = t664 and t716; 1048t1269 = t1260 nand t734; 1049t1270 = t1268 and t1269; 1050t1271 = t1260 and t731; 1051t735 = t672 and t716; 1052t1272 = t1271 nand t735; 1053t1273 = t1270 nand t1272; 1054t1274 = not t1273; 1055t1275 = t1266 nand t1274; 1056t1276 = not t1266; 1057t1277 = t1273 nand t1276; 1058t1278 = t1275 nand t1277; 1059t1279 = not t1278; 1060t1280 = t1262 nand t1279; 1061t1281 = not t1262; 1062t1282 = t1278 nand t1281; 1063t1283 = t1280 nand t1282; 1064t1284 = t1283 and t801; 1065t1285 = not t1283; 1066t1286 = t785 nor t786; 1067t1287 = t1285 nor t1286; 1068t1288 = t695 and t727; 1069t1289 = not t735; 1070t1290 = t731 nand t1289; 1071t1291 = not t731; 1072t1292 = t735 nand t1291; 1073t1293 = t1290 nand t1292; 1074t1294 = not t1293; 1075t1295 = t1288 nand t1294; 1076t1296 = not t1288; 1077t1297 = t1293 nand t1296; 1078t1298 = t1295 nand t1297; 1079t733 = t695 and t732; 1080t736 = t731 and t735; 1081t737 = t734 or t736; 1082t1299 = not t737; 1083t1300 = t1260 nand t1299; 1084t1301 = not t1260; 1085t1302 = t737 nand t1301; 1086t1303 = t1300 nand t1302; 1087t1304 = not t1303; 1088t1305 = t733 nand t1304; 1089t1306 = not t733; 1090t1307 = t1303 nand t1306; 1091t1308 = t1305 nand t1307; 1092t1309 = t1298 and t1308; 1093t1310 = t1309 and t1283; 1094t1311 = t1287 or t1310; 1095t1312 = t1311 and t742; 1096t1313 = t1284 or t1312; 1097t1314 = t1242 and t914; 1098t1315 = not t1263; 1099t1316 = not t1315; 1100t1317 = t1316 and t876; 1101t1318 = t1314 or t1317; 1102t920 = t21 and t12; 1103t921 = t920 nand t154; 1104t922 = not t921; 1105t1319 = t74 and t922; 1106t924 = t920 nand t155; 1107t925 = not t924; 1108t1320 = t1319 or t925; 1109t1321 = t110 and t921; 1110t1322 = t1320 or t1321; 1111t931 = t913 and t875; 1112t1323 = t1322 and t931; 1113t1324 = t1318 nor t1323; 1114t1325 = t1324 and t900; 1115t1326 = t1313 nor t1325; 1116t1327 = not t1326; 1117t1328 = t1256 biimp t1327; 1118t1329 = t1194 and t801; 1119t1330 = not t1194; 1120t1331 = not t1330; 1121t1332 = t1182 nand t1331; 1122t1333 = not t1182; 1123t1334 = t1330 nand t1333; 1124t1335 = t1332 nand t1334; 1125t1336 = not t1335; 1126t1337 = t1336 and t742; 1127t1338 = t1329 or t1337; 1128t1339 = t2 and t810; 1129t1340 = t3 and t815; 1130t1341 = t5 and t818; 1131t1342 = t36 and t824; 1132t1343 = t41 and t829; 1133t1344 = t394 and t832; 1134t1345 = t1344 or t1232; 1135t1346 = t1343 or t1345; 1136t1347 = t1342 or t1346; 1137t1348 = t1341 or t1347; 1138t1349 = t1340 or t1348; 1139t1350 = t1339 or t1349; 1140t1351 = t437 and t844; 1141t1352 = t1350 nor t1351; 1142t1353 = t1352 and t155; 1143t1354 = t850 and t810; 1144t1355 = t852 and t815; 1145t1356 = t325 and t818; 1146t1357 = t197 and t824; 1147t1358 = t286 and t829; 1148t865 = _326; 1149t1359 = t865 and t832; 1150t1360 = t48 and t835; 1151t1361 = t1359 or t1360; 1152t1362 = t1358 or t1361; 1153t1363 = t1357 or t1362; 1154t1364 = t1356 or t1363; 1155t1365 = t1355 or t1364; 1156t1366 = t1354 or t1365; 1157t848 = _322; 1158t1367 = t848 and t844; 1159t1368 = t1366 nor t1367; 1160t1369 = t1368 and t154; 1161t1370 = t1353 or t1369; 1162t1371 = t1370 and t872; 1163t1372 = t1187 and t876; 1164t1373 = t1371 or t1372; 1165t75 = not t27; 1166t76 = t35 nand t75; 1167t77 = not t35; 1168t78 = t27 nand t77; 1169t79 = t76 nand t78; 1170t80 = not t29; 1171t81 = t31 nand t80; 1172t82 = not t31; 1173t83 = t29 nand t82; 1174t84 = t81 nand t83; 1175t85 = not t84; 1176t86 = t79 nand t85; 1177t87 = not t79; 1178t88 = t84 nand t87; 1179t89 = t86 nand t88; 1180t90 = not t89; 1181t879 = not t187; 1182t880 = not t879; 1183t1374 = t90 and t880; 1184t102 = not t48; 1185t765 = t227 and t103; 1186t766 = t102 and t765; 1187t1375 = t5 nand t36; 1188t1376 = t766 and t1375; 1189t1377 = t127 and t1376; 1190t1378 = t1377 and t3; 1191t1379 = t1378 and t879; 1192t1380 = t1374 nor t1379; 1193t1381 = t1380 and t886; 1194t1382 = t102 nand t765; 1195t1383 = t1382 and t891; 1196t1384 = t1381 or t1383; 1197t1385 = t103 and t894; 1198t1386 = t1384 or t1385; 1199t1387 = t1386 and t897; 1200t1388 = t1373 nor t1387; 1201t1389 = t1388 and t900; 1202t1390 = t1338 or t1389; 1203t1391 = t1338 nor t1389; 1204t1392 = not t1391; 1205t1393 = t1390 and t1392; 1206t1394 = t1298 and t801; 1207t1395 = not t1298; 1208t1396 = not t1395; 1209t1397 = t1286 nand t1396; 1210t1398 = not t1286; 1211t1399 = t1395 nand t1398; 1212t1400 = t1397 nand t1399; 1213t1401 = not t1400; 1214t1402 = t1401 and t742; 1215t1403 = t1394 or t1402; 1216t1404 = t1370 and t914; 1217t1405 = not t728; 1218t1406 = not t1405; 1219t1407 = t1406 and t876; 1220t1408 = t1404 or t1407; 1221t1409 = t1380 and t922; 1222t1410 = t1382 and t925; 1223t1411 = t1409 or t1410; 1224t928 = t921 and t924; 1225t1412 = t103 and t928; 1226t1413 = t1411 or t1412; 1227t1414 = t1413 and t931; 1228t1415 = t1408 nor t1414; 1229t1416 = t1415 and t900; 1230t1417 = t1403 nor t1416; 1231t1418 = not t1417; 1232t1419 = t1393 biimp t1418; 1233t1420 = t1203 and t801; 1234t1421 = t1194 and t1182; 1235t1422 = not t1203; 1236t1423 = t1421 nand t1422; 1237t1424 = not t1421; 1238t1425 = t1203 nand t1424; 1239t1426 = t1423 nand t1425; 1240t1427 = t1426 and t742; 1241t1428 = t1420 or t1427; 1242t1429 = t437 and t810; 1243t1430 = t2 and t815; 1244t1431 = t3 and t818; 1245t1432 = t5 and t824; 1246t1433 = t36 and t829; 1247t1434 = t956 and t832; 1248t1435 = t1434 or t980; 1249t1436 = t1433 or t1435; 1250t1437 = t1432 or t1436; 1251t1438 = t1431 or t1437; 1252t1439 = t1430 or t1438; 1253t1440 = t1429 or t1439; 1254t1441 = t394 and t844; 1255t1442 = t1440 nor t1441; 1256t1443 = t1442 and t155; 1257t1444 = t852 and t810; 1258t1445 = t325 and t815; 1259t1446 = t197 and t818; 1260t1447 = t286 and t824; 1261t1448 = t48 and t829; 1262t1449 = t848 and t832; 1263t836 = t39 and t835; 1264t1450 = t1449 or t836; 1265t1451 = t1448 or t1450; 1266t1452 = t1447 or t1451; 1267t1453 = t1446 or t1452; 1268t1454 = t1445 or t1453; 1269t1455 = t1444 or t1454; 1270t1456 = t850 and t844; 1271t1457 = t1455 nor t1456; 1272t1458 = t1457 and t154; 1273t1459 = t1443 or t1458; 1274t1460 = t1459 and t872; 1275t1461 = t1196 and t876; 1276t1462 = t1460 or t1461; 1277t104 = not t103; 1278t105 = t102 nand t104; 1279t106 = not t102; 1280t107 = t103 nand t106; 1281t108 = t105 nand t107; 1282t111 = not t110; 1283t112 = t109 nand t111; 1284t113 = not t109; 1285t114 = t110 nand t113; 1286t115 = t112 nand t114; 1287t116 = not t115; 1288t117 = t108 nand t116; 1289t118 = not t108; 1290t119 = t115 nand t118; 1291t120 = t117 nand t119; 1292t1463 = t120 and t886; 1293t1464 = t1463 or t891; 1294t1465 = t109 and t894; 1295t1466 = t1464 or t1465; 1296t1467 = t1466 and t897; 1297t1468 = t1462 nor t1467; 1298t1469 = t1468 and t900; 1299t1470 = t1428 or t1469; 1300t1471 = t1428 nor t1469; 1301t1472 = not t1471; 1302t1473 = t1470 and t1472; 1303t1474 = t1308 and t801; 1304t1475 = t1298 and t1286; 1305t1476 = not t1308; 1306t1477 = t1475 nand t1476; 1307t1478 = not t1475; 1308t1479 = t1308 nand t1478; 1309t1480 = t1477 nand t1479; 1310t1481 = t1480 and t742; 1311t1482 = t1474 or t1481; 1312t1483 = t1459 and t914; 1313t1484 = not t1257; 1314t1485 = not t1484; 1315t1486 = t1485 and t876; 1316t1487 = t1483 or t1486; 1317t1488 = t120 and t922; 1318t1489 = t1488 or t925; 1319t1490 = t109 and t921; 1320t1491 = t1489 or t1490; 1321t1492 = t1491 and t931; 1322t1493 = t1487 nor t1492; 1323t1494 = t1493 and t900; 1324t1495 = t1482 nor t1494; 1325t1496 = not t1495; 1326t1497 = t1473 biimp t1496; 1327t1498 = t757 and t943; 1328t1499 = t1498 and t1051; 1329t1500 = t695 and t1499; 1330t1501 = not t1076; 1331t1502 = t1051 nand t1071; 1332t1503 = t1501 and t1502; 1333t1504 = t1051 and t943; 1334t1505 = t1504 nand t759; 1335t1506 = t1503 nand t1505; 1336t1507 = not t1506; 1337t1508 = t1057 nand t1507; 1338t1509 = not t1057; 1339t1510 = t1506 nand t1509; 1340t1511 = t1508 nand t1510; 1341t1512 = not t1511; 1342t1513 = t1500 nand t1512; 1343t1514 = not t1500; 1344t1515 = t1511 nand t1514; 1345t1516 = t1513 nand t1515; 1346t1517 = t1516 and t801; 1347t1518 = t695 and t1498; 1348t1519 = t759 and t943; 1349t1520 = t1071 or t1519; 1350t1521 = not t1520; 1351t1522 = t1051 nand t1521; 1352t1523 = not t1051; 1353t1524 = t1520 nand t1523; 1354t1525 = t1522 nand t1524; 1355t1526 = not t1525; 1356t1527 = t1518 nand t1526; 1357t1528 = not t1518; 1358t1529 = t1525 nand t1528; 1359t1530 = t1527 nand t1529; 1360t1531 = t695 and t1061; 1361t1532 = t1531 and t1085; 1362t1533 = t1532 nor t1069; 1363t1534 = t1530 and t1533; 1364t1535 = not t1516; 1365t1536 = t1534 nand t1535; 1366t1537 = not t1534; 1367t1538 = t1516 nand t1537; 1368t1539 = t1536 nand t1538; 1369t1540 = t1539 and t742; 1370t1541 = t1517 or t1540; 1371t1542 = t962 and t810; 1372t1543 = t971 and t815; 1373t1544 = t956 and t818; 1374t1545 = t394 and t824; 1375t1546 = t437 and t829; 1376t1547 = _125; 1377t1548 = t1547 and t832; 1378t1549 = t2 and t835; 1379t1550 = t1548 or t1549; 1380t1551 = t1546 or t1550; 1381t1552 = t1545 or t1551; 1382t1553 = t1544 or t1552; 1383t1554 = t1543 or t1553; 1384t1555 = t1542 or t1554; 1385t1556 = _128; 1386t1557 = t1556 and t844; 1387t1558 = t1555 nor t1557; 1388t1559 = t1558 and t155; 1389t1560 = t48 and t810; 1390t1561 = t39 and t815; 1391t1562 = t43 and t818; 1392t825 = t41 and t824; 1393t1563 = t197 and t832; 1394t1564 = t1563 or t964; 1395t1565 = t1433 or t1564; 1396t1566 = t825 or t1565; 1397t1567 = t1562 or t1566; 1398t1568 = t1561 or t1567; 1399t1569 = t1560 or t1568; 1400t1570 = t286 and t844; 1401t1571 = t1569 nor t1570; 1402t1572 = t1571 and t154; 1403t1573 = t1559 or t1572; 1404t1574 = t1573 and t872; 1405t1575 = t1509 and t993; 1406t1576 = t1574 or t1575; 1407t1577 = t4 and t996; 1408t1578 = t1576 nor t1577; 1409t1579 = t1578 and t900; 1410t1580 = t1541 or t1579; 1411t1581 = t784 and t1009; 1412t1582 = t1581 and t1104; 1413t1583 = t695 and t1582; 1414t1584 = not t1128; 1415t1585 = t1104 nand t1124; 1416t1586 = t1584 and t1585; 1417t1587 = t1104 and t1009; 1418t1588 = t1587 nand t786; 1419t1589 = t1586 nand t1588; 1420t1590 = not t1589; 1421t1591 = t1110 nand t1590; 1422t1592 = not t1110; 1423t1593 = t1589 nand t1592; 1424t1594 = t1591 nand t1593; 1425t1595 = not t1594; 1426t1596 = t1583 nand t1595; 1427t1597 = not t1583; 1428t1598 = t1594 nand t1597; 1429t1599 = t1596 nand t1598; 1430t1600 = t1599 and t801; 1431t1601 = t695 and t1581; 1432t1602 = t786 and t1009; 1433t1603 = t1124 or t1602; 1434t1604 = not t1603; 1435t1605 = t1104 nand t1604; 1436t1606 = not t1104; 1437t1607 = t1603 nand t1606; 1438t1608 = t1605 nand t1607; 1439t1609 = not t1608; 1440t1610 = t1601 nand t1609; 1441t1611 = not t1601; 1442t1612 = t1608 nand t1611; 1443t1613 = t1610 nand t1612; 1444t1614 = t695 and t1114; 1445t1615 = t1614 nor t1122; 1446t1616 = t1613 and t1615; 1447t1617 = not t1599; 1448t1618 = t1616 nand t1617; 1449t1619 = not t1616; 1450t1620 = t1599 nand t1619; 1451t1621 = t1618 nand t1620; 1452t1622 = t1621 and t742; 1453t1623 = t1600 or t1622; 1454t1624 = t1573 and t914; 1455t1625 = not t1106; 1456t1626 = not t1625; 1457t1627 = t1626 and t993; 1458t1628 = t1624 or t1627; 1459t1629 = t4 and t1028; 1460t1630 = t1628 nor t1629; 1461t1631 = t1630 and t900; 1462t1632 = t1623 or t1631; 1463t1633 = t1580 biimp t1632; 1464t1634 = t695 and t1060; 1465t1635 = t699 and t402; 1466t1636 = not t429; 1467t1637 = t1635 nand t1636; 1468t1638 = not t1635; 1469t1639 = t429 nand t1638; 1470t1640 = t1637 nand t1639; 1471t1641 = t1640 nand t1083; 1472t1642 = not t1640; 1473t1643 = t1082 nand t1642; 1474t1644 = t1641 nand t1643; 1475t1645 = not t1644; 1476t1646 = t1634 nand t1645; 1477t1647 = not t1634; 1478t1648 = t1644 nand t1647; 1479t1649 = t1646 nand t1648; 1480t1650 = t1649 and t801; 1481t1651 = not t1649; 1482t1652 = t1651 nor t1533; 1483t1653 = t1530 and t1516; 1484t1654 = t1649 and t1653; 1485t1655 = t1654 and t1533; 1486t1656 = t1652 or t1655; 1487t1657 = t1656 and t742; 1488t1658 = t1650 or t1657; 1489t1659 = t1556 and t810; 1490t1660 = t962 and t815; 1491t1661 = t971 and t818; 1492t1662 = t956 and t824; 1493t1663 = t394 and t829; 1494t1664 = _124; 1495t1665 = t1664 and t832; 1496t1666 = t437 and t835; 1497t1667 = t1665 or t1666; 1498t1668 = t1663 or t1667; 1499t1669 = t1662 or t1668; 1500t1670 = t1661 or t1669; 1501t1671 = t1660 or t1670; 1502t1672 = t1659 or t1671; 1503t1673 = t1547 and t844; 1504t1674 = t1672 nor t1673; 1505t1675 = t155 nand t189; 1506t1676 = not t1675; 1507t1677 = t1674 and t1676; 1508t1678 = t39 and t810; 1509t1679 = t43 and t815; 1510t1680 = t41 and t818; 1511t1681 = t286 and t832; 1512t1682 = t3 and t835; 1513t1683 = t1681 or t1682; 1514t1684 = t1214 or t1683; 1515t1685 = t1342 or t1684; 1516t1686 = t1680 or t1685; 1517t1687 = t1679 or t1686; 1518t1688 = t1678 or t1687; 1519t1689 = t48 and t844; 1520t1690 = t1688 nor t1689; 1521t1691 = t154 nand t189; 1522t1692 = not t1691; 1523t1693 = t1690 and t1692; 1524t1694 = t1677 or t1693; 1525t1695 = t1675 and t1691; 1526t1696 = t127 and t1695; 1527t1697 = t1694 or t1696; 1528t1698 = t1697 and t872; 1529t1699 = t1642 and t993; 1530t1700 = t1698 or t1699; 1531t1701 = t127 and t996; 1532t1702 = t1700 nor t1701; 1533t1703 = t1702 and t900; 1534t1704 = t1658 or t1703; 1535t1705 = t695 and t1113; 1536t1706 = t699 and t579; 1537t1707 = not t594; 1538t1708 = t1706 nand t1707; 1539t1709 = not t1706; 1540t1710 = t594 nand t1709; 1541t1711 = t1708 nand t1710; 1542t1712 = t1711 nand t1135; 1543t1713 = not t1711; 1544t1714 = t1134 nand t1713; 1545t1715 = t1712 nand t1714; 1546t1716 = not t1715; 1547t1717 = t1705 nand t1716; 1548t1718 = not t1705; 1549t1719 = t1715 nand t1718; 1550t1720 = t1717 nand t1719; 1551t1721 = t1720 and t801; 1552t1722 = not t1720; 1553t1723 = t1722 nor t1615; 1554t1724 = t1613 and t1599; 1555t1725 = t1724 and t1720; 1556t1726 = t1723 or t1725; 1557t1727 = t1726 and t742; 1558t1728 = t1721 or t1727; 1559t1729 = t1697 and t914; 1560t1730 = not t1707; 1561t1731 = not t1730; 1562t1732 = t1731 and t993; 1563t1733 = t1729 or t1732; 1564t1734 = t127 and t1028; 1565t1735 = t1733 nor t1734; 1566t1736 = t1735 and t900; 1567t1737 = t1728 or t1736; 1568t1738 = t1704 biimp t1737; 1569t1739 = t1530 and t801; 1570t1740 = not t1530; 1571t1741 = not t1740; 1572t1742 = t1533 nand t1741; 1573t1743 = not t1533; 1574t1744 = t1740 nand t1743; 1575t1745 = t1742 nand t1744; 1576t1746 = not t1745; 1577t1747 = t1746 and t742; 1578t1748 = t1739 or t1747; 1579t1749 = t971 and t810; 1580t1750 = t956 and t815; 1581t1751 = t394 and t818; 1582t1752 = t437 and t824; 1583t1753 = t2 and t829; 1584t1754 = t1556 and t832; 1585t1755 = t1754 or t1682; 1586t1756 = t1753 or t1755; 1587t1757 = t1752 or t1756; 1588t1758 = t1751 or t1757; 1589t1759 = t1750 or t1758; 1590t1760 = t1749 or t1759; 1591t1761 = t962 and t844; 1592t1762 = t1760 nor t1761; 1593t1763 = t1762 and t155; 1594t1764 = t286 and t810; 1595t1765 = t48 and t815; 1596t1766 = t39 and t818; 1597t1767 = t43 and t824; 1598t1768 = t325 and t832; 1599t1769 = t1768 or t1216; 1600t1770 = t1343 or t1769; 1601t1771 = t1767 or t1770; 1602t1772 = t1766 or t1771; 1603t1773 = t1765 or t1772; 1604t1774 = t1764 or t1773; 1605t1775 = t197 and t844; 1606t1776 = t1774 nor t1775; 1607t1777 = t1776 and t154; 1608t1778 = t1763 or t1777; 1609t1779 = t1778 and t872; 1610t1780 = t1523 and t993; 1611t1781 = t1779 or t1780; 1612t1782 = t6 and t996; 1613t1783 = t1781 nor t1782; 1614t1784 = t1783 and t900; 1615t1785 = t1748 or t1784; 1616t1786 = t1748 nor t1784; 1617t1787 = not t1786; 1618t1788 = t1785 and t1787; 1619t1789 = t1613 and t801; 1620t1790 = not t1613; 1621t1791 = not t1790; 1622t1792 = t1615 nand t1791; 1623t1793 = not t1615; 1624t1794 = t1790 nand t1793; 1625t1795 = t1792 nand t1794; 1626t1796 = not t1795; 1627t1797 = t1796 and t742; 1628t1798 = t1789 or t1797; 1629t1799 = t1778 and t914; 1630t1800 = not t1100; 1631t1801 = not t1800; 1632t1802 = t1801 and t993; 1633t1803 = t1799 or t1802; 1634t1804 = t6 and t1028; 1635t1805 = t1803 nor t1804; 1636t1806 = t1805 and t900; 1637t1807 = t1798 nor t1806; 1638t1808 = not t1807; 1639t1809 = t1788 biimp t1808; 1640t793 = not t695; 1641t794 = t707 nand t793; 1642t795 = not t707; 1643t796 = t695 nand t795; 1644t797 = t794 nand t796; 1645t802 = t797 and t801; 1646t803 = t797 and t742; 1647t804 = t802 or t803; 1648t811 = t3 and t810; 1649t816 = t5 and t815; 1650t819 = t36 and t818; 1651t833 = t437 and t832; 1652t837 = t833 or t836; 1653t838 = t830 or t837; 1654t839 = t825 or t838; 1655t840 = t819 or t839; 1656t841 = t816 or t840; 1657t842 = t811 or t841; 1658t845 = t2 and t844; 1659t846 = t842 nor t845; 1660t847 = t846 and t155; 1661t849 = t848 and t810; 1662t851 = t850 and t815; 1663t853 = t852 and t818; 1664t854 = t325 and t824; 1665t855 = t197 and t829; 1666t856 = _329; 1667t857 = t856 and t832; 1668t858 = t286 and t835; 1669t859 = t857 or t858; 1670t860 = t855 or t859; 1671t861 = t854 or t860; 1672t862 = t853 or t861; 1673t863 = t851 or t862; 1674t864 = t849 or t863; 1675t866 = t865 and t844; 1676t867 = t864 nor t866; 1677t868 = t867 and t154; 1678t869 = t847 or t868; 1679t873 = t869 and t872; 1680t877 = t795 and t876; 1681t878 = t873 or t877; 1682t122 = not t6; 1683t123 = t121 nand t122; 1684t124 = not t121; 1685t125 = t6 nand t124; 1686t126 = t123 nand t125; 1687t128 = t4 nand t127; 1688t129 = not t4; 1689t130 = t2 nand t129; 1690t131 = t128 nand t130; 1691t132 = not t131; 1692t133 = t126 nand t132; 1693t134 = not t126; 1694t135 = t131 nand t134; 1695t136 = t133 nand t135; 1696t881 = t136 and t880; 1697t7 = t4 nand t6; 1698t8 = t2 and t7; 1699t882 = t8 and t879; 1700t883 = t881 nor t882; 1701t887 = t883 and t886; 1702t888 = t109 nand t103; 1703t889 = t41 nand t888; 1704t892 = t889 and t891; 1705t893 = t887 or t892; 1706t895 = t102 and t894; 1707t896 = t893 or t895; 1708t898 = t896 and t897; 1709t899 = t878 nor t898; 1710t901 = t899 and t900; 1711t903 = t804 nor t901; 1712t1810 = t903 and t1391; 1713t1811 = t1471 and t1810; 1714t1812 = t1811 and t1254; 1715t1813 = t1541 nor t1579; 1716t1814 = t1001 and t1786; 1717t1815 = t1813 and t1814; 1718t1816 = t1658 nor t1703; 1719t1817 = t1815 and t1816; 1720t1818 = t1812 and t1817; 1721t1819 = not t1818; 1722t906 = t727 nand t793; 1723t907 = not t727; 1724t908 = t695 nand t907; 1725t909 = t906 nand t908; 1726t910 = t909 and t801; 1727t911 = t909 and t742; 1728t912 = t910 or t911; 1729t915 = t869 and t914; 1730t916 = not t724; 1731t917 = not t916; 1732t918 = t917 and t876; 1733t919 = t915 or t918; 1734t923 = t883 and t922; 1735t926 = t889 and t925; 1736t927 = t923 or t926; 1737t929 = t102 and t928; 1738t930 = t927 or t929; 1739t932 = t930 and t931; 1740t933 = t919 nor t932; 1741t934 = t933 and t900; 1742t935 = t912 nor t934; 1743t1820 = t935 and t1417; 1744t1821 = t1495 and t1820; 1745t1822 = t1821 and t1326; 1746t1823 = t1623 nor t1631; 1747t1824 = t1032 and t1807; 1748t1825 = t1823 and t1824; 1749t1826 = t1728 nor t1736; 1750t1827 = t1825 and t1826; 1751t1828 = t1822 and t1827; 1752t1829 = not t1828; 1753t1830 = t1819 biimp t1829; 1754t1831 = t1813 and t1816; 1755t1832 = not t698; 1756t1833 = t1832 nor t700; 1757t1834 = t1831 and t1833; 1758t1835 = t1834 nor t1818; 1759t1836 = t698 and t1835; 1760t1837 = not t1836; 1761t1838 = t1823 and t1826; 1762t1839 = t1838 and t1833; 1763t1840 = t1839 nor t1828; 1764t1841 = t698 and t1840; 1765t1842 = not t1841; 1766t1843 = t1837 biimp t1842; 1767t15 = t8 and t14; 1768t19 = t17 or t18; 1769t20 = t16 and t19; 1770t23 = t22 nand t12; 1771t24 = not t23; 1772t25 = t20 and t24; 1773t26 = t15 or t25; 1774t28 = t27 nand t5; 1775t30 = t29 nand t2; 1776t32 = t31 nand t3; 1777t33 = t30 and t32; 1778t34 = t28 and t33; 1779t37 = t35 nand t36; 1780t38 = t34 and t37; 1781t40 = t18 nand t39; 1782t42 = t16 nand t41; 1783t44 = t17 nand t43; 1784t45 = t42 and t44; 1785t46 = t40 and t45; 1786t49 = t47 nand t48; 1787t50 = t46 and t49; 1788t51 = t38 nand t50; 1789t52 = t13 and t23; 1790t53 = t51 and t52; 1791t54 = t26 or t53; 1792t55 = t26 nor t53; 1793t56 = not t55; 1794t57 = t54 nand t56; 1795t58 = not t56; 1796t59 = t57 biimp t58; 1797t1844 = not t1470; 1798t1845 = t1253 nand t1844; 1799t1846 = not t1253; 1800t1847 = t1470 nand t1846; 1801t1848 = t1845 nand t1847; 1802t902 = t804 or t901; 1803t1849 = not t902; 1804t1850 = t1390 nand t1849; 1805t1851 = not t1390; 1806t1852 = t902 nand t1851; 1807t1853 = t1850 nand t1852; 1808t1854 = not t1853; 1809t1855 = t1848 nand t1854; 1810t1856 = not t1848; 1811t1857 = t1853 nand t1856; 1812t1858 = t1855 nand t1857; 1813t1859 = not t1858; 1814t1860 = not t1000; 1815t1861 = t1785 nand t1860; 1816t1862 = not t1785; 1817t1863 = t1000 nand t1862; 1818t1864 = t1861 nand t1863; 1819t1865 = not t1864; 1820t1866 = t1832 or t700; 1821t1867 = t1580 and t1866; 1822t1868 = t1866 and t1704; 1823t1869 = not t1868; 1824t1870 = t1867 nand t1869; 1825t1871 = not t1867; 1826t1872 = t1868 nand t1871; 1827t1873 = t1870 nand t1872; 1828t1874 = t1865 and t1873; 1829t1875 = _2897; 1830t1876 = t1833 nand t1875; 1831t1877 = t1874 and t1876; 1832t1878 = t1864 and t1873; 1833t1879 = t1833 and t1875; 1834t1880 = t1878 and t1879; 1835t1881 = not t1873; 1836t1882 = t1864 and t1881; 1837t1883 = t1882 and t1876; 1838t1884 = t1880 or t1883; 1839t1885 = t1877 or t1884; 1840t1886 = t1865 and t1881; 1841t1887 = t1886 and t1879; 1842t1888 = t1885 or t1887; 1843t1889 = not t1888; 1844t1890 = t1859 nand t1889; 1845t1891 = not t1859; 1846t1892 = t1888 nand t1891; 1847t1893 = t1890 nand t1892; 1848t1894 = t1798 or t1806; 1849t1895 = t1022 or t1031; 1850t1896 = not t1895; 1851t1897 = t1894 nand t1896; 1852t1898 = not t1894; 1853t1899 = t1895 nand t1898; 1854t1900 = t1897 nand t1899; 1855t1901 = t1632 and t1866; 1856t1902 = t1866 and t1737; 1857t1903 = not t1902; 1858t1904 = t1901 nand t1903; 1859t1905 = not t1901; 1860t1906 = t1902 nand t1905; 1861t1907 = t1904 nand t1906; 1862t1908 = not t1907; 1863t1909 = t1900 and t1908; 1864t1910 = t1909 and t1876; 1865t1911 = not t1900; 1866t1912 = t1911 and t1907; 1867t1913 = t1910 or t1912; 1868t1914 = t1911 and t1879; 1869t1915 = t1913 or t1914; 1870t1916 = not t1915; 1871t1917 = not t1916; 1872t1918 = t1313 or t1325; 1873t1919 = t1482 or t1494; 1874t1920 = not t1919; 1875t1921 = t1918 nand t1920; 1876t1922 = not t1918; 1877t1923 = t1919 nand t1922; 1878t1924 = t1921 nand t1923; 1879t1925 = t1403 or t1416; 1880t1926 = t912 or t934; 1881t1927 = not t1926; 1882t1928 = t1925 nand t1927; 1883t1929 = not t1925; 1884t1930 = t1926 nand t1929; 1885t1931 = t1928 nand t1930; 1886t1932 = not t1931; 1887t1933 = t1924 nand t1932; 1888t1934 = not t1924; 1889t1935 = t1931 nand t1934; 1890t1936 = t1933 nand t1935; 1891t1937 = not t1936; 1892t1938 = not t1937; 1893t1939 = not t1938; 1894t1940 = t1917 nand t1939; 1895t1941 = t1938 nand t1916; 1896t1942 = t1940 and t1941; 1897t1943 = t1893 biimp t1942; 1898t1944 = not t1580; 1899t1945 = t1704 nand t1944; 1900t1946 = not t1704; 1901t1947 = t1580 nand t1946; 1902t1948 = t1945 nand t1947; 1903t1949 = t1948 nand t1865; 1904t1950 = not t1948; 1905t1951 = t1864 nand t1950; 1906t1952 = t1949 nand t1951; 1907t1953 = t1952 nand t1859; 1908t1954 = not t1952; 1909t1955 = t1858 nand t1954; 1910t1956 = t1953 nand t1955; 1911t1957 = not t1956; 1912t1958 = not t1632; 1913t1959 = t1737 nand t1958; 1914t1960 = not t1737; 1915t1961 = t1632 nand t1960; 1916t1962 = t1959 nand t1961; 1917t1963 = t1962 nand t1911; 1918t1964 = not t1962; 1919t1965 = t1900 nand t1964; 1920t1966 = t1963 nand t1965; 1921t1967 = not t1966; 1922t1968 = not t1967; 1923t1969 = t1938 nand t1968; 1924t1970 = t1967 nand t1937; 1925t1971 = t1969 nand t1970; 1926t1972 = t1957 biimp t1971; 1927t91 = t74 nand t90; 1928t92 = not t74; 1929t93 = t89 nand t92; 1930t94 = t91 nand t93; 1931t95 = not t94; 1932t96 = not t90; 1933t97 = not t92; 1934t98 = t96 nand t97; 1935t99 = t92 nand t90; 1936t100 = t98 nand t99; 1937t101 = t95 biimp t100; 1938t137 = not t136; 1939t138 = t120 nand t137; 1940t139 = not t120; 1941t140 = t136 nand t139; 1942t141 = t138 nand t140; 1943t142 = not t141; 1944t143 = not t142; 1945t144 = not t140; 1946t145 = not t144; 1947t146 = not t138; 1948t147 = not t146; 1949t148 = t145 nand t147; 1950t149 = t143 biimp t148; 1951t510 = t347 and t509; 1952t632 = t559 and t631; 1953t633 = t510 biimp t632; 1954t647 = t509 nand t646; 1955t661 = not t660; 1956t662 = t647 and t661; 1957t663 = not t662; 1958t677 = t631 nand t676; 1959t691 = not t690; 1960t692 = t677 and t691; 1961t693 = not t692; 1962t694 = t663 biimp t693; 1963t722 = t715 and t721; 1964t723 = t722 or t720; 1965t738 = t733 or t737; 1966t739 = t723 biimp t738; 1967t743 = t8 and t742; 1968t762 = t761 or t759; 1969t763 = t762 and t186; 1970t764 = t743 or t763; 1971t767 = t741 and t9; 1972t768 = t766 and t767; 1973t769 = t764 or t768; 1974t770 = t764 nor t768; 1975t771 = not t770; 1976t772 = t769 and t771; 1977t787 = t785 or t786; 1978t788 = t787 and t186; 1979t789 = t743 or t788; 1980t790 = t789 nor t768; 1981t791 = not t790; 1982t792 = t772 biimp t791; 1983t904 = not t903; 1984t905 = t902 and t904; 1985t936 = not t935; 1986t937 = t905 biimp t936; 1987 1988tautology t1034; 1989tautology t1148; 1990tautology t1328; 1991tautology t1419; 1992tautology t1497; 1993tautology t1633; 1994tautology t1738; 1995tautology t1809; 1996tautology t1830; 1997tautology t1843; 1998tautology t59; 1999tautology t1943; 2000tautology t1972; 2001tautology t101; 2002tautology t149; 2003tautology t633; 2004tautology t694; 2005tautology t739; 2006tautology t792; 2007tautology t937; 2008