c3540.cal

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

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;