/* BDD Calculator data file */

initial 41000 10000;

inputs
_1 _2 _3 _4 _5 _6 _7 _8 _11 _14 
_15 _16 _19 _20 _21 _22 _23 _24 _25 _26 
_27 _28 _29 _32 _33 _34 _35 _36 _37 _40 
_43 _44 _47 _48 _49 _50 _51 _52 _53 _54 
_55 _56 _57 _60 _61 _62 _63 _64 _65 _66 
_67 _68 _69 _72 _73 _74 _75 _76 _77 _78 
_79 _80 _81 _82 _85 _86 _87 _88 _89 _90 
_91 _92 _93 _94 _95 _96 _99 _100 _101 _102 
_103 _104 _105 _106 _107 _108 _111 _112 _113 _114 
_115 _116 _117 _118 _119 _120 _123 _124 _125 _126 
_127 _128 _129 _130 _131 _132 _135 _136 _137 _138 
_139 _140 _141 _142 _452 _483 _543 _559 _567 _651 
_661 _860 _868 _1083 _1341 _1348 _1384 _1956 _1961 _1966 
_1971 _1976 _1981 _1986 _1991 _1996 _2066 _2067 _2072 _2078 
_2084 _2090 _2096 _2100 _2104 _2105 _2106 _2427 _2430 _2435 
_2438 _2443 _2446 _2451 _2454 _2474 _2678 ;

actions
autoreorder 0 sift;

t2 = _860;
t3 = not t2;
t4 = _56;
t5 = _543;
t6 = not t5;
t7 = t4 and t6;
t8 = _651;
t9 = t7 and t8;
t10 = _81;
t11 = t10 and t6;
t12 = not t8;
t13 = t11 and t12;
t14 = _43;
t15 = t14 and t5;
t16 = t15 and t12;
t17 = t13 or t16;
t18 = t9 or t17;
t19 = _68;
t20 = t19 and t5;
t21 = t20 and t8;
t22 = t18 or t21;
t23 = t22 and t2;
t24 = t3 or t23;
t25 = t3 or t22;
t26 = t24 biimp t25;
t27 = t6 and t8;
t28 = _87;
t29 = t28 and t6;
t30 = t29 and t12;
t31 = _49;
t32 = t31 and t5;
t33 = t32 and t12;
t34 = t30 or t33;
t35 = t27 or t34;
t36 = _74;
t37 = t36 and t5;
t38 = t37 and t8;
t39 = t35 or t38;
t40 = t29 or t33;
t41 = t27 or t40;
t42 = t36 and t8;
t43 = t41 or t42;
t44 = t39 biimp t43;
t45 = _559;
t46 = not t45;
t47 = _66;
t48 = t47 and t6;
t49 = t48 and t8;
t50 = _92;
t51 = t50 and t6;
t52 = t51 and t12;
t53 = _54;
t54 = t53 and t5;
t55 = t54 and t12;
t56 = t52 or t55;
t57 = t49 or t56;
t58 = _79;
t59 = t58 and t5;
t60 = t59 and t8;
t61 = t57 or t60;
t62 = not t61;
t63 = t46 nand t62;
t64 = t63 and t3;
t65 = t61 and t2;
t66 = t64 or t65;
t67 = t64 or t61;
t68 = t66 biimp t67;
t69 = _2100;
t70 = not t69;
t71 = _2104;
t72 = not t71;
t73 = _2105;
t74 = t72 and t73;
t75 = not t73;
t76 = t72 and t75;
t77 = t71 and t75;
t78 = t76 or t77;
t79 = t74 or t78;
t80 = t71 and t73;
t81 = t79 or t80;
t82 = t70 nand t81;
t83 = t70 and t82;
t84 = t82 and t81;
t85 = t83 or t84;
t86 = not t85;
t87 = t85 and t86;
t88 = t87 or t86;
t89 = _2096;
t90 = not t89;
t91 = _123;
t92 = t91 and t72;
t93 = t92 and t73;
t94 = _135;
t95 = t94 and t72;
t96 = t95 and t75;
t97 = _99;
t98 = t97 and t71;
t99 = t98 and t75;
t100 = t96 or t99;
t101 = t93 or t100;
t102 = _111;
t103 = t102 and t71;
t104 = t103 and t73;
t105 = t101 or t104;
t106 = t90 nand t105;
t107 = t90 and t106;
t108 = t106 and t105;
t109 = t107 or t108;
t110 = not t109;
t111 = t109 and t110;
t112 = t111 or t110;
t113 = t88 nand t112;
t114 = not t70;
t115 = not t114;
t116 = t115 nand t110;
t117 = t113 biimp t116;
t118 = _23;
t119 = _16;
t120 = not t119;
t121 = t118 and t120;
t122 = t39 and t119;
t123 = t121 or t122;
t124 = _1976;
t125 = not t124;
t126 = not t125;
t127 = t123 nand t126;
t128 = not t123;
t129 = t125 nand t128;
t130 = t127 nand t129;
t131 = not t130;
t132 = _6;
t133 = t132 and t120;
t134 = _61;
t135 = t134 and t6;
t136 = t135 and t8;
t137 = _86;
t138 = t137 and t6;
t139 = t138 and t12;
t140 = _48;
t141 = t140 and t5;
t142 = t141 and t12;
t143 = t139 or t142;
t144 = t136 or t143;
t145 = _73;
t146 = t145 and t5;
t147 = t146 and t8;
t148 = t144 or t147;
t149 = t148 and t119;
t150 = t133 or t149;
t151 = _1981;
t152 = not t151;
t153 = not t152;
t154 = t150 nand t153;
t155 = not t150;
t156 = t152 nand t155;
t157 = t154 nand t156;
t158 = not t157;
t159 = _25;
t160 = _29;
t161 = not t160;
t162 = t159 and t161;
t163 = _119;
t164 = t163 and t72;
t165 = t164 and t73;
t166 = _131;
t167 = t166 and t72;
t168 = t167 and t75;
t169 = _95;
t170 = t169 and t71;
t171 = t170 and t75;
t172 = t168 or t171;
t173 = t165 or t172;
t174 = _107;
t175 = t174 and t71;
t176 = t175 and t73;
t177 = t173 or t176;
t178 = t177 and t160;
t179 = t162 or t178;
t180 = _1991;
t181 = not t180;
t182 = not t181;
t183 = t179 nand t182;
t184 = not t179;
t185 = t181 nand t184;
t186 = t183 nand t185;
t187 = not t186;
t188 = _24;
t189 = t188 and t120;
t190 = _60;
t191 = t190 and t6;
t192 = t191 and t8;
t193 = _85;
t194 = t193 and t6;
t195 = t194 and t12;
t196 = _47;
t197 = t196 and t5;
t198 = t197 and t12;
t199 = t195 or t198;
t200 = t192 or t199;
t201 = _72;
t202 = t201 and t5;
t203 = t202 and t8;
t204 = t200 or t203;
t205 = t204 and t119;
t206 = t189 or t205;
t207 = _1986;
t208 = not t207;
t209 = not t208;
t210 = t206 nand t209;
t211 = not t206;
t212 = t208 nand t211;
t213 = t210 nand t212;
t214 = not t213;
t215 = t187 and t214;
t216 = t158 and t215;
t217 = t131 and t216;
t218 = _22;
t219 = t218 and t120;
t220 = _62;
t221 = t220 and t6;
t222 = t221 and t8;
t223 = _88;
t224 = t223 and t6;
t225 = t224 and t12;
t226 = _50;
t227 = t226 and t5;
t228 = t227 and t12;
t229 = t225 or t228;
t230 = t222 or t229;
t231 = _75;
t232 = t231 and t5;
t233 = t232 and t8;
t234 = t230 or t233;
t235 = t234 and t119;
t236 = t219 or t235;
t237 = _1971;
t238 = not t237;
t239 = not t238;
t240 = t236 nand t239;
t241 = not t236;
t242 = t238 nand t241;
t243 = t240 nand t242;
t244 = not t243;
t245 = t217 and t244;
t246 = _4;
t247 = t246 and t120;
t248 = t61 and t119;
t249 = t247 or t248;
t250 = _1348;
t251 = not t250;
t252 = not t251;
t253 = t249 nand t252;
t254 = not t249;
t255 = t251 nand t254;
t256 = t253 nand t255;
t257 = not t256;
t258 = _20;
t259 = t258 and t120;
t260 = _65;
t261 = t260 and t6;
t262 = t261 and t8;
t263 = _91;
t264 = t263 and t6;
t265 = t264 and t12;
t266 = _53;
t267 = t266 and t5;
t268 = t267 and t12;
t269 = t265 or t268;
t270 = t262 or t269;
t271 = _78;
t272 = t271 and t5;
t273 = t272 and t8;
t274 = t270 or t273;
t275 = t274 and t119;
t276 = t259 or t275;
t277 = _1956;
t278 = not t277;
t279 = not t278;
t280 = t276 nand t279;
t281 = not t276;
t282 = t278 nand t281;
t283 = t280 nand t282;
t284 = not t283;
t285 = _21;
t286 = t285 and t120;
t287 = _63;
t288 = t287 and t6;
t289 = t288 and t8;
t290 = _89;
t291 = t290 and t6;
t292 = t291 and t12;
t293 = _51;
t294 = t293 and t5;
t295 = t294 and t12;
t296 = t292 or t295;
t297 = t289 or t296;
t298 = _76;
t299 = t298 and t5;
t300 = t299 and t8;
t301 = t297 or t300;
t302 = t301 and t119;
t303 = t286 or t302;
t304 = _1966;
t305 = not t304;
t306 = not t305;
t307 = t303 nand t306;
t308 = not t303;
t309 = t305 nand t308;
t310 = t307 nand t309;
t311 = not t310;
t312 = _5;
t313 = t312 and t120;
t314 = _64;
t315 = t314 and t6;
t316 = t315 and t8;
t317 = _90;
t318 = t317 and t6;
t319 = t318 and t12;
t320 = _52;
t321 = t320 and t5;
t322 = t321 and t12;
t323 = t319 or t322;
t324 = t316 or t323;
t325 = _77;
t326 = t325 and t5;
t327 = t326 and t8;
t328 = t324 or t327;
t329 = t328 and t119;
t330 = t313 or t329;
t331 = _1961;
t332 = not t331;
t333 = not t332;
t334 = t330 nand t333;
t335 = not t330;
t336 = t332 nand t335;
t337 = t334 nand t336;
t338 = not t337;
t339 = t311 and t338;
t340 = t284 and t339;
t341 = t257 and t340;
t342 = _19;
t343 = t342 and t120;
t344 = t22 and t119;
t345 = t343 or t344;
t346 = _1341;
t347 = not t346;
t348 = not t347;
t349 = t345 nand t348;
t350 = not t345;
t351 = t347 nand t350;
t352 = t349 nand t351;
t353 = not t352;
t354 = t341 and t353;
t355 = t245 and t354;
t356 = _28;
t357 = t356 and t161;
t358 = t105 and t160;
t359 = t357 or t358;
t360 = _35;
t361 = t360 and t161;
t362 = _124;
t363 = t362 and t72;
t364 = t363 and t73;
t365 = _136;
t366 = t365 and t72;
t367 = t366 and t75;
t368 = _100;
t369 = t368 and t71;
t370 = t369 and t75;
t371 = t367 or t370;
t372 = t364 or t371;
t373 = _112;
t374 = t373 and t71;
t375 = t374 and t73;
t376 = t372 or t375;
t377 = t376 and t160;
t378 = t361 or t377;
t379 = _2090;
t380 = not t379;
t381 = not t380;
t382 = t378 nand t381;
t383 = not t378;
t384 = t380 nand t383;
t385 = t382 nand t384;
t386 = not t385;
t387 = t359 and t386;
t388 = _26;
t389 = t388 and t161;
t390 = _128;
t391 = t390 and t72;
t392 = t391 and t73;
t393 = _140;
t394 = t393 and t72;
t395 = t394 and t75;
t396 = _104;
t397 = t396 and t71;
t398 = t397 and t75;
t399 = t395 or t398;
t400 = t392 or t399;
t401 = _116;
t402 = t401 and t71;
t403 = t402 and t73;
t404 = t400 or t403;
t405 = t404 and t160;
t406 = t389 or t405;
t407 = _2067;
t408 = not t407;
t409 = not t408;
t410 = t406 nand t409;
t411 = not t406;
t412 = t408 nand t411;
t413 = t410 nand t412;
t414 = not t413;
t415 = _33;
t416 = t415 and t161;
t417 = _127;
t418 = t417 and t72;
t419 = t418 and t73;
t420 = _139;
t421 = t420 and t72;
t422 = t421 and t75;
t423 = _103;
t424 = t423 and t71;
t425 = t424 and t75;
t426 = t422 or t425;
t427 = t419 or t426;
t428 = _115;
t429 = t428 and t71;
t430 = t429 and t73;
t431 = t427 or t430;
t432 = t431 and t160;
t433 = t416 or t432;
t434 = _2072;
t435 = not t434;
t436 = not t435;
t437 = t433 nand t436;
t438 = not t433;
t439 = t435 nand t438;
t440 = t437 nand t439;
t441 = not t440;
t442 = _34;
t443 = t442 and t161;
t444 = _125;
t445 = t444 and t72;
t446 = t445 and t73;
t447 = _137;
t448 = t447 and t72;
t449 = t448 and t75;
t450 = _101;
t451 = t450 and t71;
t452 = t451 and t75;
t453 = t449 or t452;
t454 = t446 or t453;
t455 = _113;
t456 = t455 and t71;
t457 = t456 and t73;
t458 = t454 or t457;
t459 = t458 and t160;
t460 = t443 or t459;
t461 = _2084;
t462 = not t461;
t463 = not t462;
t464 = t460 nand t463;
t465 = not t460;
t466 = t462 nand t465;
t467 = t464 nand t466;
t468 = not t467;
t469 = _27;
t470 = t469 and t161;
t471 = _126;
t472 = t471 and t72;
t473 = t472 and t73;
t474 = _138;
t475 = t474 and t72;
t476 = t475 and t75;
t477 = _102;
t478 = t477 and t71;
t479 = t478 and t75;
t480 = t476 or t479;
t481 = t473 or t480;
t482 = _114;
t483 = t482 and t71;
t484 = t483 and t73;
t485 = t481 or t484;
t486 = t485 and t160;
t487 = t470 or t486;
t488 = _2078;
t489 = not t488;
t490 = not t489;
t491 = t487 nand t490;
t492 = not t487;
t493 = t489 nand t492;
t494 = t491 nand t493;
t495 = not t494;
t496 = t468 and t495;
t497 = t441 and t496;
t498 = t414 and t497;
t499 = _32;
t500 = t499 and t161;
t501 = _129;
t502 = t501 and t72;
t503 = t502 and t73;
t504 = _141;
t505 = t504 and t72;
t506 = t505 and t75;
t507 = _105;
t508 = t507 and t71;
t509 = t508 and t75;
t510 = t506 or t509;
t511 = t503 or t510;
t512 = _117;
t513 = t512 and t71;
t514 = t513 and t73;
t515 = t511 or t514;
t516 = t515 and t160;
t517 = t500 or t516;
t518 = _1996;
t519 = not t518;
t520 = not t519;
t521 = t517 nand t520;
t522 = not t517;
t523 = t519 nand t522;
t524 = t521 nand t523;
t525 = not t524;
t526 = t498 and t525;
t527 = t387 and t526;
t528 = t355 and t527;
t529 = _11;
t530 = _868;
t531 = not t530;
t532 = t529 and t531;
t533 = t529 and t530;
t534 = t532 or t533;
t535 = t528 and t534;
t536 = t43 and t119;
t537 = t121 or t536;
t538 = t537 nand t126;
t539 = not t537;
t540 = t125 nand t539;
t541 = t538 nand t540;
t542 = not t541;
t543 = t542 and t216;
t544 = t543 and t244;
t545 = t544 and t354;
t546 = t545 and t527;
t547 = t546 and t529;
t548 = t535 biimp t547;
t549 = not t535;
t550 = not t547;
t551 = t549 biimp t550;
t552 = not t376;
t553 = t458 nand t552;
t554 = not t458;
t555 = t376 nand t554;
t556 = t553 nand t555;
t557 = not t81;
t558 = t105 nand t557;
t559 = not t105;
t560 = t81 nand t559;
t561 = t558 nand t560;
t562 = not t561;
t563 = t556 nand t562;
t564 = not t556;
t565 = t561 nand t564;
t566 = t563 nand t565;
t567 = _130;
t568 = t567 and t72;
t569 = t568 and t73;
t570 = _142;
t571 = t570 and t72;
t572 = t571 and t75;
t573 = _106;
t574 = t573 and t71;
t575 = t574 and t75;
t576 = t572 or t575;
t577 = t569 or t576;
t578 = _118;
t579 = t578 and t71;
t580 = t579 and t73;
t581 = t577 or t580;
t582 = not t177;
t583 = t581 nand t582;
t584 = not t581;
t585 = t177 nand t584;
t586 = t583 nand t585;
t587 = not t404;
t588 = t515 nand t587;
t589 = not t515;
t590 = t404 nand t589;
t591 = t588 nand t590;
t592 = not t591;
t593 = t586 and t592;
t594 = not t485;
t595 = t431 nand t594;
t596 = not t431;
t597 = t485 nand t596;
t598 = t595 nand t597;
t599 = not t598;
t600 = t593 and t599;
t601 = not t586;
t602 = t592 and t601;
t603 = t602 and t598;
t604 = t600 nor t603;
t605 = t601 and t591;
t606 = t605 and t599;
t607 = t591 and t586;
t608 = t607 and t598;
t609 = t606 nor t608;
t610 = t604 nand t609;
t611 = not t610;
t612 = t566 nand t611;
t613 = not t566;
t614 = t610 nand t613;
t615 = t612 nand t614;
t616 = not t615;
t617 = _37;
t618 = not t617;
t619 = t616 and t618;
t620 = not t559;
t621 = not t620;
t622 = not t621;
t623 = t556 nand t622;
t624 = t621 nand t564;
t625 = t623 nand t624;
t626 = t625 nand t611;
t627 = not t625;
t628 = t610 nand t627;
t629 = t626 nand t628;
t630 = not t629;
t631 = t630 and t618;
t632 = t619 biimp t631;
t633 = _67;
t634 = t633 and t6;
t635 = t634 and t8;
t636 = _93;
t637 = t636 and t6;
t638 = t637 and t12;
t639 = _55;
t640 = t639 and t5;
t641 = t640 and t12;
t642 = t638 or t641;
t643 = t635 or t642;
t644 = _80;
t645 = t644 and t5;
t646 = t645 and t8;
t647 = t643 or t646;
t648 = t647 and t531;
t649 = not t234;
t650 = not t39;
t651 = not t650;
t652 = t649 nand t651;
t653 = not t649;
t654 = t650 nand t653;
t655 = t652 nand t654;
t656 = not t148;
t657 = not t204;
t658 = not t657;
t659 = t656 nand t658;
t660 = not t656;
t661 = t657 nand t660;
t662 = t659 nand t661;
t663 = not t662;
t664 = t655 nand t663;
t665 = not t655;
t666 = t662 nand t665;
t667 = t664 nand t666;
t668 = not t647;
t669 = not t22;
t670 = not t669;
t671 = t668 nand t670;
t672 = not t668;
t673 = t669 nand t672;
t674 = t671 nand t673;
t675 = not t674;
t676 = t63 and t675;
t677 = not t274;
t678 = not t677;
t679 = t62 nand t678;
t680 = not t62;
t681 = t677 nand t680;
t682 = t679 nand t681;
t683 = not t682;
t684 = t676 and t683;
t685 = not t63;
t686 = t675 and t685;
t687 = t686 and t682;
t688 = t684 nor t687;
t689 = t685 and t674;
t690 = t689 and t683;
t691 = t674 and t63;
t692 = t691 and t682;
t693 = t690 nor t692;
t694 = t688 nand t693;
t695 = not t694;
t696 = t667 nand t695;
t697 = not t667;
t698 = t694 nand t697;
t699 = t696 nand t698;
t700 = t699 and t530;
t701 = t648 or t700;
t702 = not t43;
t703 = not t702;
t704 = t649 nand t703;
t705 = t702 nand t653;
t706 = t704 nand t705;
t707 = t706 nand t663;
t708 = not t706;
t709 = t662 nand t708;
t710 = t707 nand t709;
t711 = t710 nand t695;
t712 = not t710;
t713 = t694 nand t712;
t714 = t711 nand t713;
t715 = t714 and t530;
t716 = t648 or t715;
t717 = t701 biimp t716;
t718 = t674 and t683;
t719 = not t328;
t720 = not t301;
t721 = not t720;
t722 = t719 nand t721;
t723 = not t719;
t724 = t720 nand t723;
t725 = t722 nand t724;
t726 = not t725;
t727 = t718 and t726;
t728 = t683 and t675;
t729 = t728 and t725;
t730 = t727 nor t729;
t731 = t675 and t682;
t732 = t731 and t726;
t733 = t682 and t674;
t734 = t733 and t725;
t735 = t732 nor t734;
t736 = t730 nand t735;
t737 = not t736;
t738 = t667 nand t737;
t739 = t736 nand t697;
t740 = t738 nand t739;
t741 = not t740;
t742 = t741 and t618;
t743 = t710 nand t737;
t744 = t736 nand t712;
t745 = t743 nand t744;
t746 = not t745;
t747 = t746 and t618;
t748 = t742 biimp t747;
t749 = _1384;
t750 = not t749;
t751 = t485 and t750;
t752 = t554 and t751;
t753 = _40;
t754 = t752 and t753;
t755 = not t754;
t756 = t515 and t755;
t757 = t753 and t554;
t758 = not t751;
t759 = t757 and t758;
t760 = t756 and t759;
t761 = not t760;
t762 = t519 and t755;
t763 = t762 and t759;
t764 = not t763;
t765 = t761 nand t764;
t766 = not t761;
t767 = t763 nand t766;
t768 = t765 nand t767;
t769 = t404 and t755;
t770 = t769 and t759;
t771 = not t770;
t772 = t408 and t755;
t773 = t772 and t759;
t774 = not t773;
t775 = t771 nand t774;
t776 = not t771;
t777 = t773 nand t776;
t778 = t775 nand t777;
t779 = t768 and t778;
t780 = t181 and t755;
t781 = t780 and t759;
t782 = t177 and t755;
t783 = t782 and t759;
t784 = not t783;
t785 = t781 and t784;
t786 = t779 and t785;
t787 = t773 and t771;
t788 = t763 and t761;
t789 = t778 and t788;
t790 = t787 or t789;
t791 = t786 or t790;
t792 = t204 and t755;
t793 = t792 and t759;
t794 = not t793;
t795 = t208 and t755;
t796 = t795 and t759;
t797 = t794 and t796;
t798 = not t781;
t799 = t784 nand t798;
t800 = not t784;
t801 = t781 nand t800;
t802 = t799 nand t801;
t803 = t802 and t778;
t804 = t797 and t803;
t805 = t804 and t768;
t806 = t791 or t805;
t807 = not t755;
t808 = t462 and t807;
t809 = t305 and t755;
t810 = t808 or t809;
t811 = _8;
t812 = t810 and t811;
t813 = t301 and t755;
t814 = t301 and t754;
t815 = t813 or t814;
t816 = t815 and t811;
t817 = not t816;
t818 = t812 and t817;
t819 = t234 and t755;
t820 = t234 and t754;
t821 = t819 or t820;
t822 = t821 and t811;
t823 = not t822;
t824 = t380 and t807;
t825 = t238 and t755;
t826 = t824 or t825;
t827 = t826 and t811;
t828 = not t827;
t829 = t823 nand t828;
t830 = not t823;
t831 = t827 nand t830;
t832 = t829 nand t831;
t833 = t148 and t755;
t834 = t833 and t811;
t835 = not t834;
t836 = t152 and t755;
t837 = t836 and t811;
t838 = not t837;
t839 = t835 nand t838;
t840 = not t835;
t841 = t837 nand t840;
t842 = t839 nand t841;
t843 = t832 and t842;
t844 = t818 and t843;
t845 = t39 and t755;
t846 = t845 and t811;
t847 = not t846;
t848 = t125 and t755;
t849 = t848 and t811;
t850 = not t849;
t851 = t847 nand t850;
t852 = not t847;
t853 = t849 nand t852;
t854 = t851 nand t853;
t855 = t844 and t854;
t856 = t854 and t842;
t857 = t827 and t823;
t858 = t856 and t857;
t859 = t837 and t835;
t860 = t849 and t847;
t861 = t842 and t860;
t862 = t859 or t861;
t863 = t858 or t862;
t864 = t855 or t863;
t865 = t489 and t807;
t866 = t332 and t755;
t867 = t865 or t866;
t868 = t867 and t719;
t869 = not t812;
t870 = t817 nand t869;
t871 = not t817;
t872 = t812 nand t871;
t873 = t870 nand t872;
t874 = t873 and t832;
t875 = t842 and t874;
t876 = t868 and t875;
t877 = t876 and t854;
t878 = t864 or t877;
t879 = not t867;
t880 = t719 nand t879;
t881 = t867 nand t723;
t882 = t880 nand t881;
t883 = t854 and t882;
t884 = t832 and t883;
t885 = t842 and t884;
t886 = t885 and t873;
t887 = t435 and t807;
t888 = t278 and t755;
t889 = t887 or t888;
t890 = t889 and t677;
t891 = not t889;
t892 = t677 nand t891;
t893 = t889 nand t678;
t894 = t892 nand t893;
t895 = t408 and t807;
t896 = t251 and t755;
t897 = t895 or t896;
t898 = t897 and t62;
t899 = t894 and t898;
t900 = t890 or t899;
t901 = not t897;
t902 = t62 nand t901;
t903 = t897 nand t680;
t904 = t902 nand t903;
t905 = t904 and t894;
t906 = t519 and t807;
t907 = t347 and t755;
t908 = t906 or t907;
t909 = t908 and t669;
t910 = t905 and t909;
t911 = t900 or t910;
t912 = t886 and t911;
t913 = t878 or t912;
t914 = not t913;
t915 = t806 and t914;
t916 = not t806;
t917 = not t796;
t918 = t794 nand t917;
t919 = not t794;
t920 = t796 nand t919;
t921 = t918 nand t920;
t922 = t768 and t921;
t923 = t802 and t922;
t924 = t923 and t778;
t925 = not t924;
t926 = t916 nand t925;
t927 = t926 and t913;
t928 = t915 or t927;
t929 = t756 and t757;
t930 = not t929;
t931 = not t930;
t932 = t762 and t757;
t933 = not t932;
t934 = t931 nand t933;
t935 = t769 and t757;
t936 = not t935;
t937 = not t936;
t938 = t772 and t757;
t939 = not t938;
t940 = t937 nand t939;
t941 = t934 and t940;
t942 = t780 and t757;
t943 = t782 and t757;
t944 = not t943;
t945 = t942 and t944;
t946 = t941 and t945;
t947 = t938 and t936;
t948 = t932 and t930;
t949 = t940 and t948;
t950 = t947 or t949;
t951 = t946 or t950;
t952 = t792 and t757;
t953 = not t952;
t954 = t795 and t757;
t955 = t953 and t954;
t956 = not t944;
t957 = not t942;
t958 = t956 nand t957;
t959 = t958 and t940;
t960 = t955 and t959;
t961 = t960 and t934;
t962 = t951 or t961;
t963 = not t953;
t964 = not t954;
t965 = t963 nand t964;
t966 = t934 and t965;
t967 = t958 and t966;
t968 = t967 and t940;
t969 = not t968;
t970 = not t969;
t971 = t301 and t811;
t972 = not t971;
t973 = t812 and t972;
t974 = t234 and t811;
t975 = not t974;
t976 = not t975;
t977 = t976 nand t828;
t978 = t840 nand t838;
t979 = t977 and t978;
t980 = t973 and t979;
t981 = t43 and t755;
t982 = t981 and t811;
t983 = not t982;
t984 = not t983;
t985 = t984 nand t850;
t986 = t980 and t985;
t987 = t985 and t978;
t988 = t827 and t975;
t989 = t987 and t988;
t990 = t849 and t983;
t991 = t978 and t990;
t992 = t859 or t991;
t993 = t989 or t992;
t994 = t986 or t993;
t995 = not t972;
t996 = t995 nand t869;
t997 = t996 and t977;
t998 = t978 and t997;
t999 = t868 and t998;
t1000 = t999 and t985;
t1001 = t994 or t1000;
t1002 = t723 nand t879;
t1003 = t985 and t1002;
t1004 = t977 and t1003;
t1005 = t978 and t1004;
t1006 = t1005 and t996;
t1007 = t678 nand t891;
t1008 = t1007 and t898;
t1009 = t890 or t1008;
t1010 = t680 nand t901;
t1011 = t1010 and t1007;
t1012 = t1011 and t909;
t1013 = t1009 or t1012;
t1014 = t1006 and t1013;
t1015 = t1001 or t1014;
t1016 = t970 and t1015;
t1017 = t962 or t1016;
t1018 = t928 biimp t1017;
t1019 = not t619;
t1020 = not t742;
t1021 = t1019 and t1020;
t1022 = t89 nand t70;
t1023 = t69 nand t90;
t1024 = t1022 nand t1023;
t1025 = _2678;
t1026 = t1025 nand t408;
t1027 = not t1025;
t1028 = t407 nand t1027;
t1029 = t1026 nand t1028;
t1030 = t434 nand t489;
t1031 = t488 nand t435;
t1032 = t1030 nand t1031;
t1033 = not t1032;
t1034 = t1029 and t1033;
t1035 = t461 nand t380;
t1036 = t379 nand t462;
t1037 = t1035 nand t1036;
t1038 = not t1037;
t1039 = t1034 and t1038;
t1040 = not t1029;
t1041 = t1033 and t1040;
t1042 = t1041 and t1037;
t1043 = t1039 nor t1042;
t1044 = t1040 and t1032;
t1045 = t1044 and t1038;
t1046 = t1032 and t1029;
t1047 = t1046 and t1037;
t1048 = t1045 nor t1047;
t1049 = t1043 nand t1048;
t1050 = not t1049;
t1051 = t1024 nand t1050;
t1052 = not t1024;
t1053 = t1049 nand t1052;
t1054 = t1051 nand t1053;
t1055 = t1021 and t1054;
t1056 = t151 nand t208;
t1057 = t207 nand t152;
t1058 = t1056 nand t1057;
t1059 = t180 nand t519;
t1060 = t518 nand t181;
t1061 = t1059 nand t1060;
t1062 = not t1061;
t1063 = t1058 nand t1062;
t1064 = not t1058;
t1065 = t1061 nand t1064;
t1066 = t1063 nand t1065;
t1067 = _2474;
t1068 = t1067 nand t278;
t1069 = not t1067;
t1070 = t277 nand t1069;
t1071 = t1068 nand t1070;
t1072 = t331 nand t305;
t1073 = t304 nand t332;
t1074 = t1072 nand t1073;
t1075 = not t1074;
t1076 = t1071 and t1075;
t1077 = t237 nand t125;
t1078 = t124 nand t238;
t1079 = t1077 nand t1078;
t1080 = not t1079;
t1081 = t1076 and t1080;
t1082 = not t1071;
t1083 = t1075 and t1082;
t1084 = t1083 and t1079;
t1085 = t1081 nor t1084;
t1086 = t1082 and t1074;
t1087 = t1086 and t1080;
t1088 = t1074 and t1071;
t1089 = t1088 and t1079;
t1090 = t1087 nor t1089;
t1091 = t1085 nand t1090;
t1092 = not t1091;
t1093 = t1066 nand t1092;
t1094 = not t1066;
t1095 = t1091 nand t1094;
t1096 = t1093 nand t1095;
t1097 = _2454;
t1098 = _2451;
t1099 = not t1098;
t1100 = t1097 nand t1099;
t1101 = not t1097;
t1102 = t1098 nand t1101;
t1103 = t1100 nand t1102;
t1104 = t346 nand t251;
t1105 = t250 nand t347;
t1106 = t1104 nand t1105;
t1107 = not t1106;
t1108 = t1103 nand t1107;
t1109 = not t1103;
t1110 = t1106 nand t1109;
t1111 = t1108 nand t1110;
t1112 = _2430;
t1113 = _2427;
t1114 = not t1113;
t1115 = t1112 nand t1114;
t1116 = not t1112;
t1117 = t1113 nand t1116;
t1118 = t1115 nand t1117;
t1119 = _2438;
t1120 = _2435;
t1121 = not t1120;
t1122 = t1119 nand t1121;
t1123 = not t1119;
t1124 = t1120 nand t1123;
t1125 = t1122 nand t1124;
t1126 = not t1125;
t1127 = t1118 and t1126;
t1128 = _2446;
t1129 = _2443;
t1130 = not t1129;
t1131 = t1128 nand t1130;
t1132 = not t1128;
t1133 = t1129 nand t1132;
t1134 = t1131 nand t1133;
t1135 = not t1134;
t1136 = t1127 and t1135;
t1137 = not t1118;
t1138 = t1126 and t1137;
t1139 = t1138 and t1134;
t1140 = t1136 nor t1139;
t1141 = t1137 and t1125;
t1142 = t1141 and t1135;
t1143 = t1125 and t1118;
t1144 = t1143 and t1134;
t1145 = t1142 nor t1144;
t1146 = t1140 nand t1145;
t1147 = not t1146;
t1148 = t1111 nand t1147;
t1149 = not t1111;
t1150 = t1146 nand t1149;
t1151 = t1148 nand t1150;
t1152 = not t1151;
t1153 = _14;
t1154 = t1152 and t1153;
t1155 = not t1154;
t1156 = t1096 and t1155;
t1157 = not t928;
t1158 = t928 and t1157;
t1159 = t1157 and t928;
t1160 = t1158 or t1159;
t1161 = not t1160;
t1162 = t1160 and t1161;
t1163 = t1162 or t1161;
t1164 = t1156 and t1163;
t1165 = t1055 and t1164;
t1166 = _2106;
t1167 = _96;
t1168 = _132;
t1169 = _82;
t1170 = t1168 and t1169;
t1171 = t1167 and t1170;
t1172 = _44;
t1173 = t1171 and t1172;
t1174 = not t1173;
t1175 = t1166 and t1174;
t1176 = not t1175;
t1177 = _567;
t1178 = _108;
t1179 = _120;
t1180 = _57;
t1181 = t1179 and t1180;
t1182 = t1178 and t1181;
t1183 = _69;
t1184 = t1182 and t1183;
t1185 = not t1184;
t1186 = t1177 and t1185;
t1187 = not t1186;
t1188 = t1176 and t1187;
t1189 = t1165 and t1188;
t1190 = not t631;
t1191 = not t747;
t1192 = t1190 and t1191;
t1193 = t1192 and t1054;
t1194 = t1193 and t1156;
t1195 = t1194 and t1188;
t1196 = t1189 biimp t1195;
t1197 = not t1189;
t1198 = not t1195;
t1199 = t1197 biimp t1198;

tautology t26;
tautology t44;
tautology t68;
tautology t117;
tautology t548;
tautology t551;
tautology t632;
tautology t717;
tautology t717;
tautology t748;
tautology t1018;
tautology t1196;
tautology t1199;