c1355.cal

当前最完善的OBDD程序实现。可用于并行计算分析

t469 = t123 and t468;
t470 = t469 and t361;
t494 = t279 and t470;
t495 = t160 nand t494;
t496 = t160 nand t495;
t497 = t494 nand t495;
t498 = t496 nand t497;
t476 = t469 and t376;
t499 = t279 and t476;
t500 = t160 nand t499;
t501 = t160 nand t500;
t502 = t499 nand t500;
t503 = t501 nand t502;
t504 = t498 biimp t503;
t505 = t347 and t470;
t506 = t161 nand t505;
t507 = t161 nand t506;
t508 = t505 nand t506;
t509 = t507 nand t508;
t510 = t347 and t476;
t511 = t161 nand t510;
t512 = t161 nand t511;
t513 = t510 nand t511;
t514 = t512 nand t513;
t515 = t509 biimp t514;
t417 = not t181;
t516 = t417 and t467;
t517 = t122 and t516;
t518 = t517 and t361;
t519 = t64 and t518;
t520 = t9 nand t519;
t521 = t9 nand t520;
t522 = t519 nand t520;
t523 = t521 nand t522;
t524 = t517 and t376;
t525 = t64 and t524;
t526 = t9 nand t525;
t527 = t9 nand t526;
t528 = t525 nand t526;
t529 = t527 nand t528;
t530 = t523 biimp t529;
t531 = t319 and t518;
t532 = t96 nand t531;
t533 = t96 nand t532;
t534 = t531 nand t532;
t535 = t533 nand t534;
t536 = t319 and t524;
t537 = t96 nand t536;
t538 = t96 nand t537;
t539 = t536 nand t537;
t540 = t538 nand t539;
t541 = t535 biimp t540;
t542 = t279 and t518;
t543 = t101 nand t542;
t544 = t101 nand t543;
t545 = t542 nand t543;
t546 = t544 nand t545;
t547 = t279 and t524;
t548 = t101 nand t547;
t549 = t101 nand t548;
t550 = t547 nand t548;
t551 = t549 nand t550;
t552 = t546 biimp t551;
t553 = t347 and t518;
t554 = t102 nand t553;
t555 = t102 nand t554;
t556 = t553 nand t554;
t557 = t555 nand t556;
t558 = t347 and t524;
t559 = t102 nand t558;
t560 = t102 nand t559;
t561 = t558 nand t559;
t562 = t560 nand t561;
t563 = t557 biimp t562;
t564 = t279 and t358;
t565 = t348 and t564;
t566 = t516 and t123;
t567 = t466 and t238;
t568 = t417 and t567;
t569 = t568 and t122;
t570 = t181 and t567;
t571 = t570 and t123;
t572 = t569 or t571;
t573 = t566 or t572;
t418 = t417 and t239;
t574 = t418 and t123;
t575 = t573 or t574;
t576 = t565 and t575;
t577 = t209 and t576;
t578 = t21 nand t577;
t579 = t21 nand t578;
t580 = t577 nand t578;
t581 = t579 nand t580;
t582 = t466 and t417;
t583 = t582 and t123;
t584 = t567 and t417;
t585 = t567 and t123;
t586 = t584 or t585;
t587 = t583 or t586;
t588 = t238 and t417;
t589 = t588 and t123;
t590 = t587 or t589;
t591 = t565 and t590;
t592 = t209 and t591;
t593 = t21 nand t592;
t594 = t21 nand t593;
t595 = t592 nand t593;
t596 = t594 nand t595;
t597 = t581 biimp t596;
t598 = t237 and t576;
t599 = t22 nand t598;
t600 = t22 nand t599;
t601 = t598 nand t599;
t602 = t600 nand t601;
t603 = t237 and t591;
t604 = t22 nand t603;
t605 = t22 nand t604;
t606 = t603 nand t604;
t607 = t605 nand t606;
t608 = t602 biimp t607;
t609 = t181 and t576;
t610 = t27 nand t609;
t611 = t27 nand t610;
t612 = t609 nand t610;
t613 = t611 nand t612;
t614 = t181 and t591;
t615 = t27 nand t614;
t616 = t27 nand t615;
t617 = t614 nand t615;
t618 = t616 nand t617;
t619 = t613 biimp t618;
t620 = t122 and t576;
t621 = t28 nand t620;
t622 = t28 nand t621;
t623 = t620 nand t621;
t624 = t622 nand t623;
t625 = t122 and t591;
t626 = t28 nand t625;
t627 = t28 nand t626;
t628 = t625 nand t626;
t629 = t627 nand t628;
t630 = t624 biimp t629;
t395 = t279 and t362;
t396 = t145 nand t395;
t397 = t145 nand t396;
t398 = t395 nand t396;
t399 = t397 nand t398;
t400 = t279 and t377;
t401 = t145 nand t400;
t402 = t145 nand t401;
t403 = t400 nand t401;
t404 = t402 nand t403;
t405 = t399 biimp t404;
t631 = t347 and t359;
t632 = t631 and t575;
t633 = t209 and t632;
t634 = t37 nand t633;
t635 = t37 nand t634;
t636 = t633 nand t634;
t637 = t635 nand t636;
t638 = t631 and t590;
t639 = t209 and t638;
t640 = t37 nand t639;
t641 = t37 nand t640;
t642 = t639 nand t640;
t643 = t641 nand t642;
t644 = t637 biimp t643;
t645 = t237 and t632;
t646 = t38 nand t645;
t647 = t38 nand t646;
t648 = t645 nand t646;
t649 = t647 nand t648;
t650 = t237 and t638;
t651 = t38 nand t650;
t652 = t38 nand t651;
t653 = t650 nand t651;
t654 = t652 nand t653;
t655 = t649 biimp t654;
t656 = t181 and t632;
t657 = t43 nand t656;
t658 = t43 nand t657;
t659 = t656 nand t657;
t660 = t658 nand t659;
t661 = t181 and t638;
t662 = t43 nand t661;
t663 = t43 nand t662;
t664 = t661 nand t662;
t665 = t663 nand t664;
t666 = t660 biimp t665;
t667 = t122 and t632;
t668 = t44 nand t667;
t669 = t44 nand t668;
t670 = t667 nand t668;
t671 = t669 nand t670;
t672 = t122 and t638;
t673 = t44 nand t672;
t674 = t44 nand t673;
t675 = t672 nand t673;
t676 = t674 nand t675;
t677 = t671 biimp t676;
t678 = t279 and t320;
t679 = t348 and t678;
t680 = t679 and t575;
t681 = t209 and t680;
t682 = t186 nand t681;
t683 = t186 nand t682;
t684 = t681 nand t682;
t685 = t683 nand t684;
t686 = t679 and t590;
t687 = t209 and t686;
t688 = t186 nand t687;
t689 = t186 nand t688;
t690 = t687 nand t688;
t691 = t689 nand t690;
t692 = t685 biimp t691;
t693 = t237 and t680;
t694 = t214 nand t693;
t695 = t214 nand t694;
t696 = t693 nand t694;
t697 = t695 nand t696;
t698 = t237 and t686;
t699 = t214 nand t698;
t700 = t214 nand t699;
t701 = t698 nand t699;
t702 = t700 nand t701;
t703 = t697 biimp t702;
t704 = t181 and t680;
t705 = t128 nand t704;
t706 = t128 nand t705;
t707 = t704 nand t705;
t708 = t706 nand t707;
t709 = t181 and t686;
t710 = t128 nand t709;
t711 = t128 nand t710;
t712 = t709 nand t710;
t713 = t711 nand t712;
t714 = t708 biimp t713;
t715 = t122 and t680;
t716 = t69 nand t715;
t717 = t69 nand t716;
t718 = t715 nand t716;
t719 = t717 nand t718;
t720 = t122 and t686;
t721 = t69 nand t720;
t722 = t69 nand t721;
t723 = t720 nand t721;
t724 = t722 nand t723;
t725 = t719 biimp t724;
t726 = t347 and t321;
t727 = t726 and t575;
t728 = t209 and t727;
t729 = t187 nand t728;
t730 = t187 nand t729;
t731 = t728 nand t729;
t732 = t730 nand t731;
t733 = t726 and t590;
t734 = t209 and t733;
t735 = t187 nand t734;
t736 = t187 nand t735;
t737 = t734 nand t735;
t738 = t736 nand t737;
t739 = t732 biimp t738;
t740 = t237 and t727;
t741 = t215 nand t740;
t742 = t215 nand t741;
t743 = t740 nand t741;
t744 = t742 nand t743;
t745 = t237 and t733;
t746 = t215 nand t745;
t747 = t215 nand t746;
t748 = t745 nand t746;
t749 = t747 nand t748;
t750 = t744 biimp t749;
t406 = t347 and t362;
t407 = t146 nand t406;
t408 = t146 nand t407;
t409 = t406 nand t407;
t410 = t408 nand t409;
t411 = t347 and t377;
t412 = t146 nand t411;
t413 = t146 nand t412;
t414 = t411 nand t412;
t415 = t413 nand t414;
t416 = t410 biimp t415;
t751 = t181 and t727;
t752 = t129 nand t751;
t753 = t129 nand t752;
t754 = t751 nand t752;
t755 = t753 nand t754;
t756 = t181 and t733;
t757 = t129 nand t756;
t758 = t129 nand t757;
t759 = t756 nand t757;
t760 = t758 nand t759;
t761 = t755 biimp t760;
t762 = t122 and t727;
t763 = t70 nand t762;
t764 = t70 nand t763;
t765 = t762 nand t763;
t766 = t764 nand t765;
t767 = t122 and t733;
t768 = t70 nand t767;
t769 = t70 nand t768;
t770 = t767 nand t768;
t771 = t769 nand t770;
t772 = t766 biimp t771;
t419 = t122 and t418;
t420 = t419 and t361;
t421 = t64 and t420;
t422 = t3 nand t421;
t423 = t3 nand t422;
t424 = t421 nand t422;
t425 = t423 nand t424;
t426 = t419 and t376;
t427 = t64 and t426;
t428 = t3 nand t427;
t429 = t3 nand t428;
t430 = t427 nand t428;
t431 = t429 nand t430;
t432 = t425 biimp t431;
t433 = t319 and t420;
t434 = t81 nand t433;
t435 = t81 nand t434;
t436 = t433 nand t434;
t437 = t435 nand t436;
t438 = t319 and t426;
t439 = t81 nand t438;
t440 = t81 nand t439;
t441 = t438 nand t439;
t442 = t440 nand t441;
t443 = t437 biimp t442;
t444 = t279 and t420;
t445 = t86 nand t444;
t446 = t86 nand t445;
t447 = t444 nand t445;
t448 = t446 nand t447;
t449 = t279 and t426;
t450 = t86 nand t449;
t451 = t86 nand t450;
t452 = t449 nand t450;
t453 = t451 nand t452;
t454 = t448 biimp t453;
t455 = t347 and t420;
t456 = t87 nand t455;
t457 = t87 nand t456;
t458 = t455 nand t456;
t459 = t457 nand t458;
t460 = t347 and t426;
t461 = t87 nand t460;
t462 = t87 nand t461;
t463 = t460 nand t461;
t464 = t462 nand t463;
t465 = t459 biimp t464;
t471 = t64 and t470;
t472 = t8 nand t471;
t473 = t8 nand t472;
t474 = t471 nand t472;
t475 = t473 nand t474;
t477 = t64 and t476;
t478 = t8 nand t477;
t479 = t8 nand t478;
t480 = t477 nand t478;
t481 = t479 nand t480;
t482 = t475 biimp t481;
t483 = t319 and t470;
t484 = t155 nand t483;
t485 = t155 nand t484;
t486 = t483 nand t484;
t487 = t485 nand t486;
t488 = t319 and t476;
t489 = t155 nand t488;
t490 = t155 nand t489;
t491 = t488 nand t489;
t492 = t490 nand t491;
t493 = t487 biimp t492;

tautology t383;
tautology t394;
tautology t504;
tautology t515;
tautology t530;
tautology t541;
tautology t552;
tautology t563;
tautology t597;
tautology t608;
tautology t619;
tautology t630;
tautology t405;
tautology t644;
tautology t655;
tautology t666;
tautology t677;
tautology t692;
tautology t703;
tautology t714;
tautology t725;
tautology t739;
tautology t750;
tautology t416;
tautology t761;
tautology t772;
tautology t432;
tautology t443;
tautology t454;
tautology t465;
tautology t482;
tautology t493;