/* BDD Calculator data file */

initial 13000 10000;

inputs
_1 _13 _20 _33 _41 _45 _50 _58 _68 _77 
_87 _97 _107 _116 _124 _125 _128 _132 _137 _143 
_150 _159 _169 _179 _190 _200 _213 _222 _223 _226 
_232 _238 _244 _250 _257 _264 _270 _274 _283 _294 
_303 _311 _317 _322 _326 _329 _330 _343 _1698 _2897 
;

actions
autoreorder 0 sift;

t695 = _330;
t9 = _1;
t10 = _13;
t11 = t9 and t10;
t154 = _33;
t180 = _41;
t181 = t154 and t180;
t182 = not t181;
t183 = t11 and t182;
t184 = not t183;
t47 = _270;
t322 = t184 and t47;
t186 = not t9;
t187 = _45;
t188 = t186 and t187;
t189 = not t180;
t190 = t188 and t189;
t191 = not t190;
t323 = t322 and t191;
t193 = _274;
t194 = t184 and t193;
t195 = t194 and t190;
t324 = t323 or t195;
t325 = _303;
t155 = not t154;
t198 = not t155;
t326 = t325 and t198;
t17 = _257;
t200 = _1698;
t201 = t200 or t154;
t202 = not t201;
t327 = t17 and t202;
t328 = t326 or t327;
t18 = _264;
t205 = t155 and t201;
t329 = t18 and t205;
t330 = t328 or t329;
t331 = t183 and t330;
t332 = t324 or t331;
t185 = t184 and t18;
t192 = t185 and t191;
t196 = t192 or t195;
t197 = _294;
t199 = t197 and t198;
t16 = _250;
t203 = t16 and t202;
t204 = t199 or t203;
t206 = t17 and t205;
t207 = t204 or t206;
t208 = t183 and t207;
t209 = t196 or t208;
t241 = t184 and t16;
t242 = not t188;
t243 = t241 and t242;
t244 = t194 and t188;
t245 = t243 or t244;
t48 = _116;
t246 = t48 and t198;
t27 = _238;
t247 = t27 and t202;
t248 = t246 or t247;
t35 = _244;
t249 = t35 and t205;
t250 = t248 or t249;
t251 = t183 and t250;
t252 = t245 or t251;
t283 = t184 and t17;
t284 = t283 and t191;
t285 = t284 or t195;
t286 = _283;
t287 = t286 and t198;
t288 = t35 and t202;
t289 = t287 or t288;
t290 = t16 and t205;
t291 = t289 or t290;
t292 = t183 and t291;
t293 = t285 or t292;
t744 = t252 and t293;
t745 = t209 and t744;
t746 = t332 and t745;
t211 = _179;
t747 = not t211;
t748 = t746 and t747;
t335 = not t332;
t213 = not t209;
t255 = not t252;
t296 = not t293;
t749 = t255 and t296;
t750 = t213 and t749;
t751 = t335 and t750;
t752 = t751 and t211;
t753 = t748 or t752;
t696 = t186 and t10;
t12 = _20;
t151 = not t12;
t697 = t696 and t151;
t698 = _213;
t699 = t697 and t698;
t700 = _343;
t716 = t699 nand t700;
t754 = not t716;
t755 = t753 and t754;
t150 = _169;
t39 = _107;
t103 = not t39;
t152 = not t151;
t153 = t103 and t152;
t156 = t155 or t12;
t157 = not t156;
t158 = t48 and t157;
t159 = t153 or t158;
t41 = _87;
t160 = t151 and t156;
t161 = t41 and t160;
t162 = t159 or t161;
t163 = t9 nand t10;
t164 = t9 and t12;
t165 = t164 nand t154;
t166 = t163 and t165;
t167 = not t166;
t168 = t162 and t167;
t169 = t10 and t12;
t170 = not t169;
t171 = t9 or t170;
t172 = t39 nor t171;
t173 = t168 or t172;
t174 = t155 or t9;
t175 = t39 and t174;
t176 = t166 and t171;
t177 = t175 and t176;
t178 = t173 or t177;
t179 = t150 and t178;
t210 = t179 and t209;
t212 = t211 and t178;
t214 = t212 and t213;
t215 = t210 nor t214;
t216 = _190;
t217 = t173 nor t177;
t218 = t216 and t217;
t219 = t218 and t213;
t220 = _200;
t221 = t220 and t217;
t222 = t221 and t209;
t223 = t219 or t222;
t224 = not t217;
t225 = t223 or t224;
t226 = t215 and t225;
t110 = not t41;
t43 = _97;
t109 = not t43;
t227 = t110 and t109;
t228 = t227 nand t103;
t229 = t228 and t152;
t230 = t43 and t157;
t231 = t229 or t230;
t5 = _68;
t232 = t5 and t160;
t233 = t231 or t232;
t234 = t233 and t167;
t235 = t41 nor t171;
t236 = t234 or t235;
t237 = t41 and t174;
t238 = t237 and t176;
t239 = t236 or t238;
t240 = t150 and t239;
t253 = t240 and t252;
t254 = t211 and t239;
t256 = t254 and t255;
t257 = t253 nor t256;
t258 = t236 nor t238;
t259 = t216 and t258;
t260 = t259 and t255;
t261 = t220 and t258;
t262 = t261 and t252;
t263 = t260 or t262;
t264 = not t258;
t265 = t263 or t264;
t266 = t257 and t265;
t267 = t39 nand t109;
t268 = t43 nand t103;
t269 = t267 nand t268;
t270 = not t269;
t271 = t270 and t152;
t272 = t39 and t157;
t273 = t271 or t272;
t36 = _77;
t274 = t36 and t160;
t275 = t273 or t274;
t276 = t275 and t167;
t277 = t43 nor t171;
t278 = t276 or t277;
t279 = t43 and t174;
t280 = t279 and t176;
t281 = t278 or t280;
t282 = t150 and t281;
t294 = t282 and t293;
t295 = t211 and t281;
t297 = t295 and t296;
t298 = t294 nor t297;
t299 = t278 nor t280;
t300 = t216 and t299;
t301 = t300 and t296;
t302 = t220 and t299;
t303 = t302 and t293;
t304 = t301 or t303;
t305 = not t299;
t306 = t304 or t305;
t307 = t298 and t306;
t308 = t266 and t307;
t309 = t226 and t308;
t310 = t48 and t152;
t311 = t286 and t157;
t312 = t310 or t311;
t313 = t43 and t160;
t314 = t312 or t313;
t315 = t314 and t167;
t316 = t48 nor t171;
t317 = t315 or t316;
t318 = t48 and t174;
t319 = t318 and t176;
t320 = t317 or t319;
t321 = t150 and t320;
t333 = t321 and t332;
t334 = t211 and t320;
t336 = t334 and t335;
t337 = t333 nor t336;
t338 = t317 nor t319;
t339 = t216 and t338;
t340 = t339 and t335;
t341 = t220 and t338;
t342 = t341 and t332;
t343 = t340 or t342;
t344 = not t338;
t345 = t343 or t344;
t346 = t337 and t345;
t347 = t309 and t346;
t756 = t347 and t716;
t757 = t755 or t756;
t758 = t695 and t757;
t701 = t699 and t700;
t473 = t36 and t152;
t474 = t41 and t157;
t475 = t473 or t474;
t3 = _58;
t476 = t3 and t160;
t477 = t475 or t476;
t478 = t477 and t167;
t479 = t36 nor t171;
t480 = t478 or t479;
t356 = t151 or t9;
t481 = t36 and t356;
t482 = t481 and t176;
t483 = t480 or t482;
t938 = t701 and t483;
t484 = t150 and t483;
t485 = t184 and t35;
t362 = t180 or t187;
t363 = t186 and t362;
t364 = not t363;
t486 = t485 and t364;
t366 = t194 and t363;
t487 = t486 or t366;
t488 = t39 and t198;
t31 = _232;
t489 = t31 and t202;
t490 = t488 or t489;
t491 = t27 and t205;
t492 = t490 or t491;
t493 = t183 and t492;
t494 = t487 or t493;
t495 = t484 and t494;
t496 = t211 and t483;
t497 = not t494;
t498 = t496 and t497;
t499 = t495 nor t498;
t500 = t480 nor t482;
t501 = t216 and t500;
t502 = t501 and t497;
t503 = t220 and t500;
t504 = t503 and t494;
t505 = t502 or t504;
t506 = not t500;
t507 = t505 or t506;
t508 = t499 and t507;
t939 = not t508;
t940 = t938 nand t939;
t941 = not t938;
t942 = t508 nand t941;
t943 = t940 nand t942;
t634 = t210 or t214;
t635 = t308 nand t634;
t636 = t253 or t256;
t637 = not t636;
t638 = t294 or t297;
t639 = t266 nand t638;
t640 = t637 and t639;
t641 = t635 and t640;
t642 = t333 or t336;
t643 = t642 and t307;
t644 = t226 and t643;
t645 = t644 nand t266;
t646 = t641 nand t645;
t759 = t646 and t716;
t760 = not t759;
t944 = t943 nand t760;
t945 = not t943;
t946 = t759 nand t945;
t947 = t944 nand t946;
t948 = not t947;
t949 = t758 nand t948;
t950 = not t758;
t951 = t947 nand t950;
t952 = t949 nand t951;
t798 = t10 and t151;
t799 = t798 nand t187;
t800 = t9 and t799;
t801 = not t800;
t953 = t952 and t801;
t21 = not t10;
t22 = t9 and t21;
t740 = t12 and t22;
t741 = t740 nand t189;
t742 = not t741;
t954 = t952 and t742;
t955 = t953 or t954;
t956 = _143;
t805 = t151 or t216;
t806 = not t220;
t807 = t12 and t211;
t808 = t806 and t807;
t809 = t805 nand t808;
t810 = not t809;
t957 = t956 and t810;
t394 = _150;
t812 = t151 nor t216;
t813 = t220 and t807;
t814 = t812 nand t813;
t815 = not t814;
t958 = t394 and t815;
t437 = _159;
t817 = t812 nand t808;
t818 = not t817;
t959 = t437 and t818;
t2 = _50;
t820 = t12 and t220;
t821 = not t807;
t822 = t820 and t821;
t823 = t805 nand t822;
t824 = not t823;
t960 = t2 and t824;
t826 = t12 nand t220;
t827 = t826 and t821;
t828 = t805 nand t827;
t829 = not t828;
t961 = t3 and t829;
t962 = _132;
t831 = t812 nand t827;
t832 = not t831;
t963 = t962 and t832;
t834 = t812 nand t822;
t835 = not t834;
t964 = t5 and t835;
t965 = t963 or t964;
t966 = t961 or t965;
t967 = t960 or t966;
t968 = t959 or t967;
t969 = t958 or t968;
t970 = t957 or t969;
t971 = _137;
t843 = t805 nand t813;
t844 = not t843;
t972 = t971 and t844;
t973 = t970 nor t972;
t974 = t973 and t155;
t975 = t197 and t810;
t976 = t286 and t815;
t977 = t48 and t818;
t978 = t39 and t824;
t830 = t43 and t829;
t852 = _311;
t979 = t852 and t832;
t980 = t41 and t835;
t981 = t979 or t980;
t982 = t830 or t981;
t983 = t978 or t982;
t984 = t977 or t983;
t985 = t976 or t984;
t986 = t975 or t985;
t987 = t325 and t844;
t988 = t986 nor t987;
t989 = t988 and t154;
t990 = t974 or t989;
t870 = t151 or t150;
t871 = t11 nand t870;
t872 = not t871;
t991 = t990 and t872;
t992 = t21 nand t155;
t993 = not t992;
t994 = t945 and t993;
t995 = t991 or t994;
t121 = not t36;
t996 = t871 and t992;
t997 = t121 and t996;
t998 = t995 nor t997;
t900 = t800 and t741;
t999 = t998 and t900;
t1000 = t955 or t999;
t1001 = t955 nor t999;
t1002 = not t1001;
t1003 = t1000 and t1002;
t511 = t193 and t190;
t548 = t323 or t511;
t549 = t548 or t331;
t512 = t192 or t511;
t513 = t512 or t208;
t523 = t193 and t188;
t524 = t243 or t523;
t525 = t524 or t251;
t535 = t284 or t511;
t536 = t535 or t292;
t773 = t525 and t536;
t774 = t513 and t773;
t775 = t549 and t774;
t776 = t775 and t747;
t551 = not t549;
t515 = not t513;
t527 = not t525;
t538 = not t536;
t777 = t527 and t538;
t778 = t515 and t777;
t779 = t551 and t778;
t780 = t779 and t211;
t781 = t776 or t780;
t782 = t781 and t754;
t514 = t179 and t513;
t516 = t212 and t515;
t517 = t514 nor t516;
t518 = t216 and t515;
t519 = t220 and t513;
t520 = t518 or t519;
t521 = t520 or t224;
t522 = t517 and t521;
t526 = t240 and t525;
t528 = t254 and t527;
t529 = t526 nor t528;
t530 = t216 and t527;
t531 = t220 and t525;
t532 = t530 or t531;
t533 = t532 or t264;
t534 = t529 and t533;
t537 = t282 and t536;
t539 = t295 and t538;
t540 = t537 nor t539;
t541 = t216 and t538;
t542 = t220 and t536;
t543 = t541 or t542;
t544 = t543 or t305;
t545 = t540 and t544;
t546 = t534 and t545;
t547 = t522 and t546;
t550 = t321 and t549;
t552 = t334 and t551;
t553 = t550 nor t552;
t554 = t216 and t551;
t555 = t220 and t549;
t556 = t554 or t555;
t557 = t556 or t344;
t558 = t553 and t557;
t559 = t547 and t558;
t783 = t559 and t716;
t784 = t782 or t783;
t785 = t695 and t784;
t614 = t481 and t166;
t615 = t480 or t614;
t1004 = t701 and t615;
t616 = t150 and t615;
t563 = t193 and t363;
t617 = t486 or t563;
t618 = t617 or t493;
t619 = t616 and t618;
t620 = t211 and t615;
t621 = not t618;
t622 = t620 and t621;
t623 = t619 nor t622;
t624 = t216 and t621;
t625 = t220 and t618;
t626 = t624 or t625;
t627 = t480 nor t614;
t628 = not t627;
t629 = t626 or t628;
t630 = t623 and t629;
t1005 = not t630;
t1006 = t1004 nand t1005;
t1007 = not t1004;
t1008 = t630 nand t1007;
t1009 = t1006 nand t1008;
t664 = t514 or t516;
t665 = t546 nand t664;
t666 = t526 or t528;
t667 = not t666;
t668 = t537 or t539;
t669 = t534 nand t668;
t670 = t667 and t669;
t671 = t665 and t670;
t672 = t550 or t552;
t673 = t672 and t545;
t674 = t522 and t673;
t675 = t674 nand t534;
t676 = t671 nand t675;
t786 = t676 and t716;
t1010 = not t786;
t1011 = t1009 nand t1010;
t1012 = not t1009;
t1013 = t786 nand t1012;
t1014 = t1011 nand t1013;
t1015 = not t1014;
t1016 = t785 nand t1015;
t1017 = not t785;
t1018 = t1014 nand t1017;
t1019 = t1016 nand t1018;
t1020 = t1019 and t801;
t1021 = t1019 and t742;
t1022 = t1020 or t1021;
t913 = t10 nand t870;
t914 = not t913;
t1023 = t990 and t914;
t1024 = not t1005;
t1025 = not t1024;
t1026 = t1025 and t993;
t1027 = t1023 or t1026;
t1028 = t913 and t992;
t1029 = t121 and t1028;
t1030 = t1027 nor t1029;
t1031 = t1030 and t900;
t1032 = t1022 nor t1031;
t1033 = not t1032;
t1034 = t1003 biimp t1033;
t4 = not t3;
t430 = t5 nand t4;
t6 = not t5;
t431 = t3 nand t6;
t432 = t430 nand t431;
t1035 = t432 and t36;
t127 = not t2;
t1036 = not t127;
t1037 = t1035 and t1036;
t1038 = t5 and t127;
t1039 = t1037 or t1038;
t1040 = t9 nand t21;
t1041 = not t1040;
t1042 = t1039 and t1041;
t1043 = t48 and t269;
t13 = t11 nand t12;
t14 = not t13;
t1044 = t1043 and t14;
t1045 = t1042 or t1044;
t348 = t6 and t152;
t349 = t36 and t157;
t350 = t348 or t349;
t351 = t2 and t160;
t352 = t350 or t351;
t353 = t352 and t167;
t354 = t5 nor t171;
t355 = t353 or t354;
t357 = t5 and t356;
t358 = t357 and t176;
t359 = t355 or t358;
t1046 = t701 and t359;
t360 = t150 and t359;
t361 = t184 and t27;
t365 = t361 and t364;
t367 = t365 or t366;
t368 = t43 and t198;
t29 = _226;
t369 = t29 and t202;
t370 = t368 or t369;
t371 = t31 and t205;
t372 = t370 or t371;
t373 = t183 and t372;
t374 = t367 or t373;
t375 = t360 and t374;
t376 = t211 and t359;
t377 = not t374;
t378 = t376 and t377;
t379 = t375 nor t378;
t380 = t355 nor t358;
t381 = t216 and t380;
t382 = t381 and t377;
t383 = t220 and t380;
t384 = t383 and t374;
t385 = t382 or t384;
t386 = not t380;
t387 = t385 or t386;
t388 = t379 and t387;
t1047 = not t388;
t1048 = t1046 nand t1047;
t1049 = not t1046;
t1050 = t388 nand t1049;
t1051 = t1048 nand t1050;
t433 = not t432;
t434 = t433 and t152;
t435 = t5 and t157;
t436 = t434 or t435;
t438 = t437 and t160;
t439 = t436 or t438;
t440 = t439 and t167;
t441 = t3 nor t171;
t442 = t440 or t441;
t443 = t3 and t356;
t444 = t443 and t176;
t445 = t442 or t444;
t1052 = t699 and t445;
t446 = t150 and t445;
t447 = t184 and t31;
t448 = t447 and t364;
t449 = t448 or t366;
t450 = t41 and t198;
t411 = _223;
t451 = t411 and t202;
t452 = t450 or t451;
t453 = t29 and t205;
t454 = t452 or t453;
t455 = t183 and t454;
t456 = t449 or t455;
t457 = t446 and t456;
t458 = t211 and t445;
t459 = not t456;
t460 = t458 and t459;
t461 = t457 nor t460;
t462 = t442 nor t444;
t463 = t216 and t462;
t464 = t463 and t459;
t465 = t220 and t462;
t466 = t465 and t456;
t467 = t464 or t466;
t468 = not t462;
t469 = t467 or t468;
t470 = t461 and t469;
t1053 = not t470;
t1054 = t1052 nand t1053;
t1055 = not t1052;
t1056 = t470 nand t1055;
t1057 = t1054 nand t1056;
t1058 = t757 and t1057;
t1059 = t1051 and t1058;
t1060 = t1059 and t943;
t389 = t127 and t4;
t390 = t389 nand t6;
t391 = t390 and t152;
t392 = t3 and t157;
t393 = t391 or t392;
t395 = t394 and t160;
t396 = t393 or t395;
t397 = t396 and t167;
t398 = t2 nor t171;
t399 = t397 or t398;
t400 = t2 and t356;
t401 = t400 and t176;
t402 = t399 or t401;
t403 = t150 and t402;
t404 = t184 and t29;
t405 = t404 and t364;
t406 = t405 or t366;
t407 = t36 and t198;
t408 = _222;
t409 = t408 and t202;
t410 = t407 or t409;
t412 = t411 and t205;
t413 = t410 or t412;
t414 = t183 and t413;
t415 = t406 or t414;
t416 = t403 and t415;
t417 = t211 and t402;
t418 = not t415;
t419 = t417 and t418;
t420 = t416 nor t419;
t421 = t399 nor t401;
t422 = t216 and t421;
t423 = t422 and t418;
t424 = t220 and t421;
t425 = t424 and t415;
t426 = t423 or t425;
t427 = not t421;
t428 = t426 or t427;
t429 = t420 and t428;
t471 = t429 and t470;
t472 = t388 and t471;
t509 = t472 and t508;
t1061 = t757 and t509;
t1062 = not t1061;
t1063 = t1060 nand t1062;
t1064 = not t1060;
t1065 = t1061 nand t1064;
t1066 = t1063 nand t1065;
t1067 = t695 and t1066;
t648 = t375 or t378;
t649 = t471 nand t648;
t650 = t416 or t419;
t651 = not t650;
t652 = t457 or t460;
t653 = t429 nand t652;
t654 = t651 and t653;
t655 = t649 and t654;
t656 = t495 or t498;
t657 = t656 and t470;
t658 = t388 and t657;
t659 = t658 nand t429;
t660 = t655 nand t659;
t1068 = t759 and t509;
t1069 = t660 or t1068;
t1070 = t1057 and t1051;
t1071 = t656 and t716;
t1072 = t1070 nand t1071;
t1073 = t697 nand t698;
t1074 = t652 and t1073;
t1075 = not t1074;
t1076 = t648 and t716;
t1077 = t1057 nand t1076;
t1078 = t1075 and t1077;
t1079 = t1072 and t1078;
t1080 = t943 and t1070;
t1081 = t1080 nand t759;
t1082 = t1079 nand t1081;
t1083 = not t1082;
t1084 = t1069 nand t1083;
t1085 = not t1069;
t1086 = t1082 nand t1085;
t1087 = t1084 nand t1086;
t1088 = not t1087;
t1089 = t1067 nand t1088;
t1090 = not t1067;
t1091 = t1087 nand t1090;
t1092 = t1089 nand t1091;
t1093 = t1040 and t13;
t1094 = t1092 and t1093;
t1095 = t1045 or t1094;
t1096 = t1045 nor t1094;
t1097 = not t1096;
t1098 = t1095 and t1097;
t560 = t357 and t166;
t561 = t355 or t560;
t1099 = t701 and t561;
t562 = t150 and t561;
t564 = t365 or t563;
t565 = t564 or t373;
t566 = t562 and t565;
t567 = t211 and t561;
t568 = not t565;
t569 = t567 and t568;
t570 = t566 nor t569;
t571 = t216 and t568;
t572 = t220 and t565;
t573 = t571 or t572;
t574 = t355 nor t560;
t575 = not t574;
t576 = t573 or t575;
t577 = t570 and t576;
t1100 = not t577;
t1101 = t1099 nand t1100;
t1102 = not t1099;
t1103 = t577 nand t1102;
t1104 = t1101 nand t1103;
t595 = t443 and t166;
t596 = t442 or t595;
t1105 = t699 and t596;
t597 = t150 and t596;
t598 = t448 or t563;
t599 = t598 or t455;
t600 = t597 and t599;
t601 = t211 and t596;
t602 = not t599;
t603 = t601 and t602;
t604 = t600 nor t603;
t605 = t216 and t602;
t606 = t220 and t599;
t607 = t605 or t606;
t608 = t442 nor t595;
t609 = not t608;
t610 = t607 or t609;
t611 = t604 and t610;
t1106 = not t611;
t1107 = t1105 nand t1106;
t1108 = not t1105;
t1109 = t611 nand t1108;
t1110 = t1107 nand t1109;
t1111 = t784 and t1110;
t1112 = t1104 and t1111;
t1113 = t1112 and t1009;
t578 = t400 and t166;
t579 = t399 or t578;
t580 = t150 and t579;
t581 = t405 or t563;
t582 = t581 or t414;
t583 = t580 and t582;
t584 = t211 and t579;
t585 = not t582;
t586 = t584 and t585;
t587 = t583 nor t586;
t588 = t216 and t585;
t589 = t220 and t582;
t590 = t588 or t589;
t591 = t399 nor t578;
t592 = not t591;
t593 = t590 or t592;
t594 = t587 and t593;
t612 = t594 and t611;
t613 = t577 and t612;
t631 = t613 and t630;
t1114 = t784 and t631;
t1115 = not t1114;
t1116 = t1113 nand t1115;
t1117 = not t1113;
t1118 = t1114 nand t1117;
t1119 = t1116 nand t1118;
t1120 = t695 and t1119;
t678 = t566 or t569;
t679 = t612 nand t678;
t680 = t583 or t586;
t681 = not t680;
t682 = t600 or t603;
t683 = t594 nand t682;
t684 = t681 and t683;
t685 = t679 and t684;
t686 = t619 or t622;
t687 = t686 and t611;
t688 = t577 and t687;
t689 = t688 nand t594;
t690 = t685 nand t689;
t1121 = t786 and t631;
t1122 = t690 or t1121;
t1123 = t1110 and t1104;
t1124 = t686 and t716;
t1125 = t1123 nand t1124;
t1126 = t682 and t1073;
t1127 = not t1126;
t1128 = t678 and t716;
t1129 = t1110 nand t1128;
t1130 = t1127 and t1129;
t1131 = t1125 and t1130;
t1132 = t1009 and t1123;
t1133 = t1132 nand t786;
t1134 = t1131 nand t1133;
t1135 = not t1134;
t1136 = t1122 nand t1135;
t1137 = not t1122;
t1138 = t1134 nand t1137;
t1139 = t1136 nand t1138;
t1140 = not t1139;
t1141 = t1120 nand t1140;
t1142 = not t1120;
t1143 = t1139 nand t1142;
t1144 = t1141 nand t1143;
t1145 = t1144 and t1093;
t1146 = t1045 nor t1145;
t1147 = not t1146;
t1148 = t1098 biimp t1147;
t702 = t701 and t320;
t703 = not t346;
t704 = t702 nand t703;
t705 = not t702;
t706 = t346 nand t705;
t707 = t704 nand t706;
t708 = t701 and t178;
t709 = not t226;
t710 = t708 nand t709;
t711 = not t708;
t712 = t226 nand t711;
t713 = t710 nand t712;
t714 = t707 and t713;
t1149 = t701 and t281;
t1150 = not t307;
t1151 = t1149 nand t1150;
t1152 = not t1149;
t1153 = t307 nand t1152;
t1154 = t1151 nand t1153;
t1155 = t714 and t1154;
t1156 = t695 and t1155;
t1157 = t701 and t239;
t1158 = not t266;
t1159 = t1157 nand t1158;
t1160 = not t1157;
t1161 = t266 nand t1160;
t1162 = t1159 nand t1161;
t1163 = t638 and t716;
t1164 = not t1163;
t717 = t634 and t716;
t1165 = t1154 nand t717;
t1166 = t1164 and t1165;
t1167 = t1154 and t713;
t718 = t642 and t716;
t1168 = t1167 nand t718;
t1169 = t1166 nand t1168;
t1170 = not t1169;
t1171 = t1162 nand t1170;
t1172 = not t1162;
t1173 = t1169 nand t1172;
t1174 = t1171 nand t1173;
t1175 = not t1174;
t1176 = t1156 nand t1175;
t1177 = not t1156;
t1178 = t1174 nand t1177;
t1179 = t1176 nand t1178;
t1180 = t1179 and t801;
t1181 = not t1179;
t761 = t758 and t760;
t1182 = t761 nor t759;
t1183 = t1181 nor t1182;
t1184 = t695 and t707;
t1185 = not t718;
t1186 = t713 nand t1185;
t1187 = not t713;
t1188 = t718 nand t1187;
t1189 = t1186 nand t1188;
t1190 = not t1189;
t1191 = t1184 nand t1190;
t1192 = not t1184;
t1193 = t1189 nand t1192;
t1194 = t1191 nand t1193;
t715 = t695 and t714;
t719 = t713 and t718;
t720 = t717 or t719;
t721 = not t720;
t1195 = t1154 nand t721;
t1196 = not t1154;
t1197 = t720 nand t1196;
t1198 = t1195 nand t1197;
t1199 = not t1198;
t1200 = t715 nand t1199;
t1201 = not t715;
t1202 = t1198 nand t1201;
t1203 = t1200 nand t1202;
t1204 = t1194 and t1203;
t1205 = t1179 and t1204;
t1206 = t1205 and t1182;
t1207 = t1183 or t1206;
t1208 = t1207 and t742;
t1209 = t1180 or t1208;
t1210 = t394 and t810;
t1211 = t437 and t815;
t1212 = t2 and t818;
t1213 = t3 and t824;
t1214 = t5 and t829;
t1215 = t971 and t832;
t1216 = t36 and t835;
t1217 = t1215 or t1216;
t1218 = t1214 or t1217;
t1219 = t1213 or t1218;
t1220 = t1212 or t1219;
t1221 = t1211 or t1220;
t1222 = t1210 or t1221;
t1223 = t956 and t844;
t1224 = t1222 nor t1223;
t1225 = t1224 and t155;
t1226 = t325 and t810;
t1227 = t197 and t815;
t1228 = t286 and t818;
t1229 = t48 and t824;
t1230 = t39 and t829;
t850 = _317;
t1231 = t850 and t832;
t1232 = t43 and t835;
t1233 = t1231 or t1232;
t1234 = t1230 or t1233;
t1235 = t1229 or t1234;
t1236 = t1228 or t1235;
t1237 = t1227 or t1236;
t1238 = t1226 or t1237;
t1239 = t852 and t844;
t1240 = t1238 nor t1239;
t1241 = t1240 and t154;
t1242 = t1225 or t1241;
t1243 = t1242 and t872;
t874 = t21 and t151;
t875 = t874 nand t155;
t876 = not t875;
t1244 = t1172 and t876;
t1245 = t1243 or t1244;
t60 = not t18;
t61 = t47 nand t60;
t62 = not t47;
t63 = t18 nand t62;
t64 = t61 nand t63;
t65 = not t16;
t66 = t17 nand t65;
t67 = not t17;
t68 = t16 nand t67;
t69 = t66 nand t68;
t70 = not t69;
t71 = t64 nand t70;
t72 = not t64;
t73 = t69 nand t72;
t74 = t71 nand t73;
t884 = t22 and t12;
t885 = t884 nand t154;
t886 = not t885;
t1246 = t74 and t886;
t890 = t884 nand t155;
t891 = not t890;
t1247 = t1246 or t891;
t894 = t885 and t890;
t1248 = t110 and t894;
t1249 = t1247 or t1248;
t897 = t871 and t875;
t1250 = t1249 and t897;
t1251 = t1245 nor t1250;
t1252 = t1251 and t900;
t1253 = t1209 or t1252;
t1254 = t1209 nor t1252;
t1255 = not t1254;
t1256 = t1253 and t1255;
t724 = not t558;
t725 = t702 nand t724;
t726 = t558 nand t705;
t727 = t725 nand t726;
t728 = not t522;
t729 = t708 nand t728;
t730 = t522 nand t711;
t731 = t729 nand t730;
t732 = t727 and t731;
t1257 = not t545;
t1258 = t1149 nand t1257;
t1259 = t545 nand t1152;
t1260 = t1258 nand t1259;
t1261 = t732 and t1260;
t1262 = t695 and t1261;
t1263 = not t534;
t1264 = t1157 nand t1263;
t1265 = t534 nand t1160;
t1266 = t1264 nand t1265;
t1267 = t668 and t716;
t1268 = not t1267;
t734 = t664 and t716;
t1269 = t1260 nand t734;
t1270 = t1268 and t1269;
t1271 = t1260 and t731;
t735 = t672 and t716;
t1272 = t1271 nand t735;
t1273 = t1270 nand t1272;
t1274 = not t1273;
t1275 = t1266 nand t1274;
t1276 = not t1266;
t1277 = t1273 nand t1276;
t1278 = t1275 nand t1277;
t1279 = not t1278;
t1280 = t1262 nand t1279;
t1281 = not t1262;
t1282 = t1278 nand t1281;
t1283 = t1280 nand t1282;
t1284 = t1283 and t801;
t1285 = not t1283;
t1286 = t785 nor t786;
t1287 = t1285 nor t1286;
t1288 = t695 and t727;
t1289 = not t735;
t1290 = t731 nand t1289;
t1291 = not t731;
t1292 = t735 nand t1291;
t1293 = t1290 nand t1292;
t1294 = not t1293;
t1295 = t1288 nand t1294;
t1296 = not t1288;
t1297 = t1293 nand t1296;
t1298 = t1295 nand t1297;
t733 = t695 and t732;
t736 = t731 and t735;
t737 = t734 or t736;
t1299 = not t737;
t1300 = t1260 nand t1299;
t1301 = not t1260;
t1302 = t737 nand t1301;
t1303 = t1300 nand t1302;
t1304 = not t1303;
t1305 = t733 nand t1304;
t1306 = not t733;
t1307 = t1303 nand t1306;
t1308 = t1305 nand t1307;
t1309 = t1298 and t1308;
t1310 = t1309 and t1283;
t1311 = t1287 or t1310;
t1312 = t1311 and t742;
t1313 = t1284 or t1312;
t1314 = t1242 and t914;
t1315 = not t1263;
t1316 = not t1315;
t1317 = t1316 and t876;
t1318 = t1314 or t1317;
t920 = t21 and t12;
t921 = t920 nand t154;
t922 = not t921;
t1319 = t74 and t922;
t924 = t920 nand t155;
t925 = not t924;
t1320 = t1319 or t925;
t1321 = t110 and t921;
t1322 = t1320 or t1321;
t931 = t913 and t875;
t1323 = t1322 and t931;
t1324 = t1318 nor t1323;
t1325 = t1324 and t900;
t1326 = t1313 nor t1325;
t1327 = not t1326;
t1328 = t1256 biimp t1327;
t1329 = t1194 and t801;
t1330 = not t1194;
t1331 = not t1330;
t1332 = t1182 nand t1331;
t1333 = not t1182;
t1334 = t1330 nand t1333;
t1335 = t1332 nand t1334;
t1336 = not t1335;
t1337 = t1336 and t742;
t1338 = t1329 or t1337;
t1339 = t2 and t810;
t1340 = t3 and t815;
t1341 = t5 and t818;
t1342 = t36 and t824;
t1343 = t41 and t829;
t1344 = t394 and t832;
t1345 = t1344 or t1232;
t1346 = t1343 or t1345;
t1347 = t1342 or t1346;
t1348 = t1341 or t1347;
t1349 = t1340 or t1348;
t1350 = t1339 or t1349;
t1351 = t437 and t844;
t1352 = t1350 nor t1351;
t1353 = t1352 and t155;
t1354 = t850 and t810;
t1355 = t852 and t815;
t1356 = t325 and t818;
t1357 = t197 and t824;
t1358 = t286 and t829;
t865 = _326;
t1359 = t865 and t832;
t1360 = t48 and t835;
t1361 = t1359 or t1360;
t1362 = t1358 or t1361;
t1363 = t1357 or t1362;
t1364 = t1356 or t1363;
t1365 = t1355 or t1364;
t1366 = t1354 or t1365;
t848 = _322;
t1367 = t848 and t844;
t1368 = t1366 nor t1367;
t1369 = t1368 and t154;
t1370 = t1353 or t1369;
t1371 = t1370 and t872;
t1372 = t1187 and t876;
t1373 = t1371 or t1372;
t75 = not t27;
t76 = t35 nand t75;
t77 = not t35;
t78 = t27 nand t77;
t79 = t76 nand t78;
t80 = not t29;
t81 = t31 nand t80;
t82 = not t31;
t83 = t29 nand t82;
t84 = t81 nand t83;
t85 = not t84;
t86 = t79 nand t85;
t87 = not t79;
t88 = t84 nand t87;
t89 = t86 nand t88;
t90 = not t89;
t879 = not t187;
t880 = not t879;
t1374 = t90 and t880;
t102 = not t48;
t765 = t227 and t103;
t766 = t102 and t765;
t1375 = t5 nand t36;
t1376 = t766 and t1375;
t1377 = t127 and t1376;
t1378 = t1377 and t3;
t1379 = t1378 and t879;
t1380 = t1374 nor t1379;
t1381 = t1380 and t886;
t1382 = t102 nand t765;
t1383 = t1382 and t891;
t1384 = t1381 or t1383;
t1385 = t103 and t894;
t1386 = t1384 or t1385;
t1387 = t1386 and t897;
t1388 = t1373 nor t1387;
t1389 = t1388 and t900;
t1390 = t1338 or t1389;
t1391 = t1338 nor t1389;
t1392 = not t1391;
t1393 = t1390 and t1392;
t1394 = t1298 and t801;
t1395 = not t1298;
t1396 = not t1395;
t1397 = t1286 nand t1396;
t1398 = not t1286;
t1399 = t1395 nand t1398;
t1400 = t1397 nand t1399;
t1401 = not t1400;
t1402 = t1401 and t742;
t1403 = t1394 or t1402;
t1404 = t1370 and t914;
t1405 = not t728;
t1406 = not t1405;
t1407 = t1406 and t876;
t1408 = t1404 or t1407;
t1409 = t1380 and t922;
t1410 = t1382 and t925;
t1411 = t1409 or t1410;
t928 = t921 and t924;
t1412 = t103 and t928;
t1413 = t1411 or t1412;
t1414 = t1413 and t931;
t1415 = t1408 nor t1414;
t1416 = t1415 and t900;
t1417 = t1403 nor t1416;
t1418 = not t1417;
t1419 = t1393 biimp t1418;
t1420 = t1203 and t801;
t1421 = t1194 and t1182;
t1422 = not t1203;
t1423 = t1421 nand t1422;
t1424 = not t1421;
t1425 = t1203 nand t1424;
t1426 = t1423 nand t1425;
t1427 = t1426 and t742;
t1428 = t1420 or t1427;
t1429 = t437 and t810;
t1430 = t2 and t815;
t1431 = t3 and t818;
t1432 = t5 and t824;
t1433 = t36 and t829;
t1434 = t956 and t832;
t1435 = t1434 or t980;
t1436 = t1433 or t1435;
t1437 = t1432 or t1436;
t1438 = t1431 or t1437;
t1439 = t1430 or t1438;
t1440 = t1429 or t1439;
t1441 = t394 and t844;
t1442 = t1440 nor t1441;
t1443 = t1442 and t155;
t1444 = t852 and t810;
t1445 = t325 and t815;
t1446 = t197 and t818;
t1447 = t286 and t824;
t1448 = t48 and t829;
t1449 = t848 and t832;
t836 = t39 and t835;
t1450 = t1449 or t836;
t1451 = t1448 or t1450;
t1452 = t1447 or t1451;
t1453 = t1446 or t1452;
t1454 = t1445 or t1453;
t1455 = t1444 or t1454;
t1456 = t850 and t844;
t1457 = t1455 nor t1456;
t1458 = t1457 and t154;
t1459 = t1443 or t1458;
t1460 = t1459 and t872;
t1461 = t1196 and t876;
t1462 = t1460 or t1461;
t104 = not t103;
t105 = t102 nand t104;
t106 = not t102;
t107 = t103 nand t106;
t108 = t105 nand t107;
t111 = not t110;
t112 = t109 nand t111;
t113 = not t109;
t114 = t110 nand t113;
t115 = t112 nand t114;
t116 = not t115;
t117 = t108 nand t116;
t118 = not t108;
t119 = t115 nand t118;
t120 = t117 nand t119;
t1463 = t120 and t886;
t1464 = t1463 or t891;
t1465 = t109 and t894;
t1466 = t1464 or t1465;
t1467 = t1466 and t897;
t1468 = t1462 nor t1467;
t1469 = t1468 and t900;
t1470 = t1428 or t1469;
t1471 = t1428 nor t1469;
t1472 = not t1471;
t1473 = t1470 and t1472;
t1474 = t1308 and t801;
t1475 = t1298 and t1286;
t1476 = not t1308;
t1477 = t1475 nand t1476;
t1478 = not t1475;
t1479 = t1308 nand t1478;
t1480 = t1477 nand t1479;
t1481 = t1480 and t742;
t1482 = t1474 or t1481;
t1483 = t1459 and t914;
t1484 = not t1257;
t1485 = not t1484;
t1486 = t1485 and t876;
t1487 = t1483 or t1486;
t1488 = t120 and t922;
t1489 = t1488 or t925;
t1490 = t109 and t921;
t1491 = t1489 or t1490;
t1492 = t1491 and t931;
t1493 = t1487 nor t1492;
t1494 = t1493 and t900;
t1495 = t1482 nor t1494;
t1496 = not t1495;
t1497 = t1473 biimp t1496;
t1498 = t757 and t943;
t1499 = t1498 and t1051;
t1500 = t695 and t1499;
t1501 = not t1076;
t1502 = t1051 nand t1071;
t1503 = t1501 and t1502;
t1504 = t1051 and t943;
t1505 = t1504 nand t759;
t1506 = t1503 nand t1505;
t1507 = not t1506;
t1508 = t1057 nand t1507;
t1509 = not t1057;
t1510 = t1506 nand t1509;
t1511 = t1508 nand t1510;
t1512 = not t1511;
t1513 = t1500 nand t1512;
t1514 = not t1500;
t1515 = t1511 nand t1514;
t1516 = t1513 nand t1515;
t1517 = t1516 and t801;
t1518 = t695 and t1498;
t1519 = t759 and t943;
t1520 = t1071 or t1519;
t1521 = not t1520;
t1522 = t1051 nand t1521;
t1523 = not t1051;
t1524 = t1520 nand t1523;
t1525 = t1522 nand t1524;
t1526 = not t1525;
t1527 = t1518 nand t1526;
t1528 = not t1518;
t1529 = t1525 nand t1528;
t1530 = t1527 nand t1529;
t1531 = t695 and t1061;
t1532 = t1531 and t1085;
t1533 = t1532 nor t1069;
t1534 = t1530 and t1533;
t1535 = not t1516;
t1536 = t1534 nand t1535;
t1537 = not t1534;
t1538 = t1516 nand t1537;
t1539 = t1536 nand t1538;
t1540 = t1539 and t742;
t1541 = t1517 or t1540;
t1542 = t962 and t810;
t1543 = t971 and t815;
t1544 = t956 and t818;
t1545 = t394 and t824;
t1546 = t437 and t829;
t1547 = _125;
t1548 = t1547 and t832;
t1549 = t2 and t835;
t1550 = t1548 or t1549;
t1551 = t1546 or t1550;
t1552 = t1545 or t1551;
t1553 = t1544 or t1552;
t1554 = t1543 or t1553;
t1555 = t1542 or t1554;
t1556 = _128;
t1557 = t1556 and t844;
t1558 = t1555 nor t1557;
t1559 = t1558 and t155;
t1560 = t48 and t810;
t1561 = t39 and t815;
t1562 = t43 and t818;
t825 = t41 and t824;
t1563 = t197 and t832;
t1564 = t1563 or t964;
t1565 = t1433 or t1564;
t1566 = t825 or t1565;
t1567 = t1562 or t1566;
t1568 = t1561 or t1567;
t1569 = t1560 or t1568;
t1570 = t286 and t844;
t1571 = t1569 nor t1570;
t1572 = t1571 and t154;
t1573 = t1559 or t1572;
t1574 = t1573 and t872;
t1575 = t1509 and t993;
t1576 = t1574 or t1575;
t1577 = t4 and t996;
t1578 = t1576 nor t1577;
t1579 = t1578 and t900;
t1580 = t1541 or t1579;
t1581 = t784 and t1009;
t1582 = t1581 and t1104;
t1583 = t695 and t1582;
t1584 = not t1128;
t1585 = t1104 nand t1124;
t1586 = t1584 and t1585;
t1587 = t1104 and t1009;
t1588 = t1587 nand t786;
t1589 = t1586 nand t1588;
t1590 = not t1589;
t1591 = t1110 nand t1590;
t1592 = not t1110;
t1593 = t1589 nand t1592;
t1594 = t1591 nand t1593;
t1595 = not t1594;
t1596 = t1583 nand t1595;
t1597 = not t1583;
t1598 = t1594 nand t1597;
t1599 = t1596 nand t1598;
t1600 = t1599 and t801;
t1601 = t695 and t1581;
t1602 = t786 and t1009;
t1603 = t1124 or t1602;
t1604 = not t1603;
t1605 = t1104 nand t1604;
t1606 = not t1104;
t1607 = t1603 nand t1606;
t1608 = t1605 nand t1607;
t1609 = not t1608;
t1610 = t1601 nand t1609;
t1611 = not t1601;
t1612 = t1608 nand t1611;
t1613 = t1610 nand t1612;
t1614 = t695 and t1114;
t1615 = t1614 nor t1122;
t1616 = t1613 and t1615;
t1617 = not t1599;
t1618 = t1616 nand t1617;
t1619 = not t1616;
t1620 = t1599 nand t1619;
t1621 = t1618 nand t1620;
t1622 = t1621 and t742;
t1623 = t1600 or t1622;
t1624 = t1573 and t914;
t1625 = not t1106;
t1626 = not t1625;
t1627 = t1626 and t993;
t1628 = t1624 or t1627;
t1629 = t4 and t1028;
t1630 = t1628 nor t1629;
t1631 = t1630 and t900;
t1632 = t1623 or t1631;
t1633 = t1580 biimp t1632;
t1634 = t695 and t1060;
t1635 = t699 and t402;
t1636 = not t429;
t1637 = t1635 nand t1636;
t1638 = not t1635;
t1639 = t429 nand t1638;
t1640 = t1637 nand t1639;
t1641 = t1640 nand t1083;
t1642 = not t1640;
t1643 = t1082 nand t1642;
t1644 = t1641 nand t1643;
t1645 = not t1644;
t1646 = t1634 nand t1645;
t1647 = not t1634;
t1648 = t1644 nand t1647;
t1649 = t1646 nand t1648;
t1650 = t1649 and t801;
t1651 = not t1649;
t1652 = t1651 nor t1533;
t1653 = t1530 and t1516;
t1654 = t1649 and t1653;
t1655 = t1654 and t1533;
t1656 = t1652 or t1655;
t1657 = t1656 and t742;
t1658 = t1650 or t1657;
t1659 = t1556 and t810;
t1660 = t962 and t815;
t1661 = t971 and t818;
t1662 = t956 and t824;
t1663 = t394 and t829;
t1664 = _124;
t1665 = t1664 and t832;
t1666 = t437 and t835;
t1667 = t1665 or t1666;
t1668 = t1663 or t1667;
t1669 = t1662 or t1668;
t1670 = t1661 or t1669;
t1671 = t1660 or t1670;
t1672 = t1659 or t1671;
t1673 = t1547 and t844;
t1674 = t1672 nor t1673;
t1675 = t155 nand t189;
t1676 = not t1675;
t1677 = t1674 and t1676;
t1678 = t39 and t810;
t1679 = t43 and t815;
t1680 = t41 and t818;
t1681 = t286 and t832;
t1682 = t3 and t835;
t1683 = t1681 or t1682;
t1684 = t1214 or t1683;
t1685 = t1342 or t1684;
t1686 = t1680 or t1685;
t1687 = t1679 or t1686;
t1688 = t1678 or t1687;
t1689 = t48 and t844;
t1690 = t1688 nor t1689;
t1691 = t154 nand t189;
t1692 = not t1691;
t1693 = t1690 and t1692;
t1694 = t1677 or t1693;
t1695 = t1675 and t1691;
t1696 = t127 and t1695;
t1697 = t1694 or t1696;
t1698 = t1697 and t872;
t1699 = t1642 and t993;
t1700 = t1698 or t1699;
t1701 = t127 and t996;
t1702 = t1700 nor t1701;
t1703 = t1702 and t900;
t1704 = t1658 or t1703;
t1705 = t695 and t1113;
t1706 = t699 and t579;
t1707 = not t594;
t1708 = t1706 nand t1707;
t1709 = not t1706;
t1710 = t594 nand t1709;
t1711 = t1708 nand t1710;
t1712 = t1711 nand t1135;
t1713 = not t1711;
t1714 = t1134 nand t1713;
t1715 = t1712 nand t1714;
t1716 = not t1715;
t1717 = t1705 nand t1716;
t1718 = not t1705;
t1719 = t1715 nand t1718;
t1720 = t1717 nand t1719;
t1721 = t1720 and t801;
t1722 = not t1720;
t1723 = t1722 nor t1615;
t1724 = t1613 and t1599;
t1725 = t1724 and t1720;
t1726 = t1723 or t1725;
t1727 = t1726 and t742;
t1728 = t1721 or t1727;
t1729 = t1697 and t914;
t1730 = not t1707;
t1731 = not t1730;
t1732 = t1731 and t993;
t1733 = t1729 or t1732;
t1734 = t127 and t1028;
t1735 = t1733 nor t1734;
t1736 = t1735 and t900;
t1737 = t1728 or t1736;
t1738 = t1704 biimp t1737;
t1739 = t1530 and t801;
t1740 = not t1530;
t1741 = not t1740;
t1742 = t1533 nand t1741;
t1743 = not t1533;
t1744 = t1740 nand t1743;
t1745 = t1742 nand t1744;
t1746 = not t1745;
t1747 = t1746 and t742;
t1748 = t1739 or t1747;
t1749 = t971 and t810;
t1750 = t956 and t815;
t1751 = t394 and t818;
t1752 = t437 and t824;
t1753 = t2 and t829;
t1754 = t1556 and t832;
t1755 = t1754 or t1682;
t1756 = t1753 or t1755;
t1757 = t1752 or t1756;
t1758 = t1751 or t1757;
t1759 = t1750 or t1758;
t1760 = t1749 or t1759;
t1761 = t962 and t844;
t1762 = t1760 nor t1761;
t1763 = t1762 and t155;
t1764 = t286 and t810;
t1765 = t48 and t815;
t1766 = t39 and t818;
t1767 = t43 and t824;
t1768 = t325 and t832;
t1769 = t1768 or t1216;
t1770 = t1343 or t1769;
t1771 = t1767 or t1770;
t1772 = t1766 or t1771;
t1773 = t1765 or t1772;
t1774 = t1764 or t1773;
t1775 = t197 and t844;
t1776 = t1774 nor t1775;
t1777 = t1776 and t154;
t1778 = t1763 or t1777;
t1779 = t1778 and t872;
t1780 = t1523 and t993;
t1781 = t1779 or t1780;
t1782 = t6 and t996;
t1783 = t1781 nor t1782;
t1784 = t1783 and t900;
t1785 = t1748 or t1784;
t1786 = t1748 nor t1784;
t1787 = not t1786;
t1788 = t1785 and t1787;
t1789 = t1613 and t801;
t1790 = not t1613;
t1791 = not t1790;
t1792 = t1615 nand t1791;
t1793 = not t1615;
t1794 = t1790 nand t1793;
t1795 = t1792 nand t1794;
t1796 = not t1795;
t1797 = t1796 and t742;
t1798 = t1789 or t1797;
t1799 = t1778 and t914;
t1800 = not t1100;
t1801 = not t1800;
t1802 = t1801 and t993;
t1803 = t1799 or t1802;
t1804 = t6 and t1028;
t1805 = t1803 nor t1804;
t1806 = t1805 and t900;
t1807 = t1798 nor t1806;
t1808 = not t1807;
t1809 = t1788 biimp t1808;
t793 = not t695;
t794 = t707 nand t793;
t795 = not t707;
t796 = t695 nand t795;
t797 = t794 nand t796;
t802 = t797 and t801;
t803 = t797 and t742;
t804 = t802 or t803;
t811 = t3 and t810;
t816 = t5 and t815;
t819 = t36 and t818;
t833 = t437 and t832;
t837 = t833 or t836;
t838 = t830 or t837;
t839 = t825 or t838;
t840 = t819 or t839;
t841 = t816 or t840;
t842 = t811 or t841;
t845 = t2 and t844;
t846 = t842 nor t845;
t847 = t846 and t155;
t849 = t848 and t810;
t851 = t850 and t815;
t853 = t852 and t818;
t854 = t325 and t824;
t855 = t197 and t829;
t856 = _329;
t857 = t856 and t832;
t858 = t286 and t835;
t859 = t857 or t858;
t860 = t855 or t859;
t861 = t854 or t860;
t862 = t853 or t861;
t863 = t851 or t862;
t864 = t849 or t863;
t866 = t865 and t844;
t867 = t864 nor t866;
t868 = t867 and t154;
t869 = t847 or t868;
t873 = t869 and t872;
t877 = t795 and t876;
t878 = t873 or t877;
t122 = not t6;
t123 = t121 nand t122;
t124 = not t121;
t125 = t6 nand t124;
t126 = t123 nand t125;
t128 = t4 nand t127;
t129 = not t4;
t130 = t2 nand t129;
t131 = t128 nand t130;
t132 = not t131;
t133 = t126 nand t132;
t134 = not t126;
t135 = t131 nand t134;
t136 = t133 nand t135;
t881 = t136 and t880;
t7 = t4 nand t6;
t8 = t2 and t7;
t882 = t8 and t879;
t883 = t881 nor t882;
t887 = t883 and t886;
t888 = t109 nand t103;
t889 = t41 nand t888;
t892 = t889 and t891;
t893 = t887 or t892;
t895 = t102 and t894;
t896 = t893 or t895;
t898 = t896 and t897;
t899 = t878 nor t898;
t901 = t899 and t900;
t903 = t804 nor t901;
t1810 = t903 and t1391;
t1811 = t1471 and t1810;
t1812 = t1811 and t1254;
t1813 = t1541 nor t1579;
t1814 = t1001 and t1786;
t1815 = t1813 and t1814;
t1816 = t1658 nor t1703;
t1817 = t1815 and t1816;
t1818 = t1812 and t1817;
t1819 = not t1818;
t906 = t727 nand t793;
t907 = not t727;
t908 = t695 nand t907;
t909 = t906 nand t908;
t910 = t909 and t801;
t911 = t909 and t742;
t912 = t910 or t911;
t915 = t869 and t914;
t916 = not t724;
t917 = not t916;
t918 = t917 and t876;
t919 = t915 or t918;
t923 = t883 and t922;
t926 = t889 and t925;
t927 = t923 or t926;
t929 = t102 and t928;
t930 = t927 or t929;
t932 = t930 and t931;
t933 = t919 nor t932;
t934 = t933 and t900;
t935 = t912 nor t934;
t1820 = t935 and t1417;
t1821 = t1495 and t1820;
t1822 = t1821 and t1326;
t1823 = t1623 nor t1631;
t1824 = t1032 and t1807;
t1825 = t1823 and t1824;
t1826 = t1728 nor t1736;
t1827 = t1825 and t1826;
t1828 = t1822 and t1827;
t1829 = not t1828;
t1830 = t1819 biimp t1829;
t1831 = t1813 and t1816;
t1832 = not t698;
t1833 = t1832 nor t700;
t1834 = t1831 and t1833;
t1835 = t1834 nor t1818;
t1836 = t698 and t1835;
t1837 = not t1836;
t1838 = t1823 and t1826;
t1839 = t1838 and t1833;
t1840 = t1839 nor t1828;
t1841 = t698 and t1840;
t1842 = not t1841;
t1843 = t1837 biimp t1842;
t15 = t8 and t14;
t19 = t17 or t18;
t20 = t16 and t19;
t23 = t22 nand t12;
t24 = not t23;
t25 = t20 and t24;
t26 = t15 or t25;
t28 = t27 nand t5;
t30 = t29 nand t2;
t32 = t31 nand t3;
t33 = t30 and t32;
t34 = t28 and t33;
t37 = t35 nand t36;
t38 = t34 and t37;
t40 = t18 nand t39;
t42 = t16 nand t41;
t44 = t17 nand t43;
t45 = t42 and t44;
t46 = t40 and t45;
t49 = t47 nand t48;
t50 = t46 and t49;
t51 = t38 nand t50;
t52 = t13 and t23;
t53 = t51 and t52;
t54 = t26 or t53;
t55 = t26 nor t53;
t56 = not t55;
t57 = t54 nand t56;
t58 = not t56;
t59 = t57 biimp t58;
t1844 = not t1470;
t1845 = t1253 nand t1844;
t1846 = not t1253;
t1847 = t1470 nand t1846;
t1848 = t1845 nand t1847;
t902 = t804 or t901;
t1849 = not t902;
t1850 = t1390 nand t1849;
t1851 = not t1390;
t1852 = t902 nand t1851;
t1853 = t1850 nand t1852;
t1854 = not t1853;
t1855 = t1848 nand t1854;
t1856 = not t1848;
t1857 = t1853 nand t1856;
t1858 = t1855 nand t1857;
t1859 = not t1858;
t1860 = not t1000;
t1861 = t1785 nand t1860;
t1862 = not t1785;
t1863 = t1000 nand t1862;
t1864 = t1861 nand t1863;
t1865 = not t1864;
t1866 = t1832 or t700;
t1867 = t1580 and t1866;
t1868 = t1866 and t1704;
t1869 = not t1868;
t1870 = t1867 nand t1869;
t1871 = not t1867;
t1872 = t1868 nand t1871;
t1873 = t1870 nand t1872;
t1874 = t1865 and t1873;
t1875 = _2897;
t1876 = t1833 nand t1875;
t1877 = t1874 and t1876;
t1878 = t1864 and t1873;
t1879 = t1833 and t1875;
t1880 = t1878 and t1879;
t1881 = not t1873;
t1882 = t1864 and t1881;
t1883 = t1882 and t1876;
t1884 = t1880 or t1883;
t1885 = t1877 or t1884;
t1886 = t1865 and t1881;
t1887 = t1886 and t1879;
t1888 = t1885 or t1887;
t1889 = not t1888;
t1890 = t1859 nand t1889;
t1891 = not t1859;
t1892 = t1888 nand t1891;
t1893 = t1890 nand t1892;
t1894 = t1798 or t1806;
t1895 = t1022 or t1031;
t1896 = not t1895;
t1897 = t1894 nand t1896;
t1898 = not t1894;
t1899 = t1895 nand t1898;
t1900 = t1897 nand t1899;
t1901 = t1632 and t1866;
t1902 = t1866 and t1737;
t1903 = not t1902;
t1904 = t1901 nand t1903;
t1905 = not t1901;
t1906 = t1902 nand t1905;
t1907 = t1904 nand t1906;
t1908 = not t1907;
t1909 = t1900 and t1908;
t1910 = t1909 and t1876;
t1911 = not t1900;
t1912 = t1911 and t1907;
t1913 = t1910 or t1912;
t1914 = t1911 and t1879;
t1915 = t1913 or t1914;
t1916 = not t1915;
t1917 = not t1916;
t1918 = t1313 or t1325;
t1919 = t1482 or t1494;
t1920 = not t1919;
t1921 = t1918 nand t1920;
t1922 = not t1918;
t1923 = t1919 nand t1922;
t1924 = t1921 nand t1923;
t1925 = t1403 or t1416;
t1926 = t912 or t934;
t1927 = not t1926;
t1928 = t1925 nand t1927;
t1929 = not t1925;
t1930 = t1926 nand t1929;
t1931 = t1928 nand t1930;
t1932 = not t1931;
t1933 = t1924 nand t1932;
t1934 = not t1924;
t1935 = t1931 nand t1934;
t1936 = t1933 nand t1935;
t1937 = not t1936;
t1938 = not t1937;
t1939 = not t1938;
t1940 = t1917 nand t1939;
t1941 = t1938 nand t1916;
t1942 = t1940 and t1941;
t1943 = t1893 biimp t1942;
t1944 = not t1580;
t1945 = t1704 nand t1944;
t1946 = not t1704;
t1947 = t1580 nand t1946;
t1948 = t1945 nand t1947;
t1949 = t1948 nand t1865;
t1950 = not t1948;
t1951 = t1864 nand t1950;
t1952 = t1949 nand t1951;
t1953 = t1952 nand t1859;
t1954 = not t1952;
t1955 = t1858 nand t1954;
t1956 = t1953 nand t1955;
t1957 = not t1956;
t1958 = not t1632;
t1959 = t1737 nand t1958;
t1960 = not t1737;
t1961 = t1632 nand t1960;
t1962 = t1959 nand t1961;
t1963 = t1962 nand t1911;
t1964 = not t1962;
t1965 = t1900 nand t1964;
t1966 = t1963 nand t1965;
t1967 = not t1966;
t1968 = not t1967;
t1969 = t1938 nand t1968;
t1970 = t1967 nand t1937;
t1971 = t1969 nand t1970;
t1972 = t1957 biimp t1971;
t91 = t74 nand t90;
t92 = not t74;
t93 = t89 nand t92;
t94 = t91 nand t93;
t95 = not t94;
t96 = not t90;
t97 = not t92;
t98 = t96 nand t97;
t99 = t92 nand t90;
t100 = t98 nand t99;
t101 = t95 biimp t100;
t137 = not t136;
t138 = t120 nand t137;
t139 = not t120;
t140 = t136 nand t139;
t141 = t138 nand t140;
t142 = not t141;
t143 = not t142;
t144 = not t140;
t145 = not t144;
t146 = not t138;
t147 = not t146;
t148 = t145 nand t147;
t149 = t143 biimp t148;
t510 = t347 and t509;
t632 = t559 and t631;
t633 = t510 biimp t632;
t647 = t509 nand t646;
t661 = not t660;
t662 = t647 and t661;
t663 = not t662;
t677 = t631 nand t676;
t691 = not t690;
t692 = t677 and t691;
t693 = not t692;
t694 = t663 biimp t693;
t722 = t715 and t721;
t723 = t722 or t720;
t738 = t733 or t737;
t739 = t723 biimp t738;
t743 = t8 and t742;
t762 = t761 or t759;
t763 = t762 and t186;
t764 = t743 or t763;
t767 = t741 and t9;
t768 = t766 and t767;
t769 = t764 or t768;
t770 = t764 nor t768;
t771 = not t770;
t772 = t769 and t771;
t787 = t785 or t786;
t788 = t787 and t186;
t789 = t743 or t788;
t790 = t789 nor t768;
t791 = not t790;
t792 = t772 biimp t791;
t904 = not t903;
t905 = t902 and t904;
t936 = not t935;
t937 = t905 biimp t936;

tautology t1034;
tautology t1148;
tautology t1328;
tautology t1419;
tautology t1497;
tautology t1633;
tautology t1738;
tautology t1809;
tautology t1830;
tautology t1843;
tautology t59;
tautology t1943;
tautology t1972;
tautology t101;
tautology t149;
tautology t633;
tautology t694;
tautology t739;
tautology t792;
tautology t937;