c2670.cal

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

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;