bddcalc/examples/c432.cal

/* BDD Calculator data file */

initial 10000 10000;

inputs
_1gat _4gat _8gat _11gat _14gat _17gat _21gat _24gat _27gat _30gat
_34gat _37gat _40gat _43gat _47gat _50gat _53gat _56gat _60gat _63gat
_66gat _69gat _73gat _76gat _79gat _82gat _86gat _89gat _92gat _95gat
_99gat _102gat _105gat _108gat _112gat _115gat ;

actions
autoreorder 0 win2ite;

t2 = _8gat;
t3 = _89gat;
t4 = not t3;
t5 = _95gat;
t6 = t4 nand t5;
t7 = _76gat;
t8 = not t7;
t9 = _82gat;
t10 = t8 nand t9;
t11 = _63gat;
t12 = not t11;
t13 = _69gat;
t14 = t12 nand t13;
t15 = _50gat;
t16 = not t15;
t17 = _56gat;
t18 = t16 nand t17;
t19 = _37gat;
t20 = not t19;
t21 = _43gat;
t22 = t20 nand t21;
t23 = _24gat;
t24 = not t23;
t25 = _30gat;
t26 = t24 nand t25;
t27 = _1gat;
t28 = not t27;
t29 = _4gat;
t30 = t28 nand t29;
t31 = _11gat;
t32 = not t31;
t33 = _17gat;
t34 = t32 nand t33;
t35 = t30 and t34;
t36 = t26 and t35;
t37 = t22 and t36;
t38 = t18 and t37;
t39 = t14 and t38;
t40 = t10 and t39;
t41 = t6 and t40;
t42 = _102gat;
t43 = not t42;
t44 = _108gat;
t45 = t43 nand t44;
t46 = t41 and t45;
t47 = not t46;
t48 = t47 xor t6;
t49 = _99gat;
t50 = not t5;
t51 = t49 nor t50;
t52 = t48 nand t51;
t53 = t47 xor t10;
t54 = _86gat;
t55 = not t9;
t56 = t54 nor t55;
t57 = t53 nand t56;
t58 = t47 xor t14;
t59 = _73gat;
t60 = not t13;
t61 = t59 nor t60;
t62 = t58 nand t61;
t63 = t47 xor t18;
t64 = _60gat;
t65 = not t17;
t66 = t64 nor t65;
t67 = t63 nand t66;
t68 = t47 xor t22;
t69 = _47gat;
t70 = not t21;
t71 = t69 nor t70;
t72 = t68 nand t71;
t73 = t47 xor t26;
t74 = _34gat;
t75 = not t25;
t76 = t74 nor t75;
t77 = t73 nand t76;
t78 = t47 xor t30;
t79 = not t29;
t80 = t2 nor t79;
t81 = t78 nand t80;
t82 = t47 xor t34;
t83 = _21gat;
t84 = not t33;
t85 = t83 nor t84;
t86 = t82 nand t85;
t87 = t81 and t86;
t88 = t77 and t87;
t89 = t72 and t88;
t90 = t67 and t89;
t91 = t62 and t90;
t92 = t57 and t91;
t93 = t52 and t92;
t94 = t47 xor t45;
t95 = _112gat;
t96 = not t44;
t97 = t95 nor t96;
t98 = t94 nand t97;
t99 = t93 and t98;
t100 = not t99;
t101 = t2 nand t100;
t102 = t27 nand t47;
t103 = t29 and t102;
t104 = t101 and t103;
t105 = _14gat;
t106 = t100 xor t52;
t107 = _105gat;
t108 = t107 nor t50;
t109 = t48 nand t108;
t110 = not t109;
t111 = t106 nand t110;
t112 = t100 xor t57;
t113 = _92gat;
t114 = t113 nor t55;
t115 = t53 nand t114;
t116 = not t115;
t117 = t112 nand t116;
t118 = t100 xor t62;
t119 = _79gat;
t120 = t119 nor t60;
t121 = t58 nand t120;
t122 = not t121;
t123 = t118 nand t122;
t124 = t100 xor t67;
t125 = _66gat;
t126 = t125 nor t65;
t127 = t63 nand t126;
t128 = not t127;
t129 = t124 nand t128;
t130 = t100 xor t72;
t131 = _53gat;
t132 = t131 nor t70;
t133 = t68 nand t132;
t134 = not t133;
t135 = t130 nand t134;
t136 = t100 xor t77;
t137 = _40gat;
t138 = t137 nor t75;
t139 = t73 nand t138;
t140 = not t139;
t141 = t136 nand t140;
t142 = t100 xor t81;
t143 = t105 nor t79;
t144 = t78 nand t143;
t145 = not t144;
t146 = t142 nand t145;
t147 = t100 xor t86;
t148 = _27gat;
t149 = t148 nor t84;
t150 = t82 nand t149;
t151 = not t150;
t152 = t147 nand t151;
t153 = t146 and t152;
t154 = t141 and t153;
t155 = t135 and t154;
t156 = t129 and t155;
t157 = t123 and t156;
t158 = t117 and t157;
t159 = t111 and t158;
t160 = t100 xor t98;
t161 = _115gat;
t162 = t161 nor t96;
t163 = t94 nand t162;
t164 = not t163;
t165 = t160 nand t164;
t166 = t159 and t165;
t167 = not t166;
t168 = t105 nand t167;
t169 = t104 nand t168;
t170 = not t169;
t171 = t167 nand t107;
t172 = t47 nand t3;
t173 = t100 nand t49;
t174 = t172 and t173;
t175 = t171 and t174;
t176 = t175 nand t5;
t177 = t167 nand t113;
t178 = t47 nand t7;
t179 = t100 nand t54;
t180 = t178 and t179;
t181 = t177 and t180;
t182 = t181 nand t9;
t183 = t167 nand t119;
t184 = t47 nand t11;
t185 = t100 nand t59;
t186 = t184 and t185;
t187 = t183 and t186;
t188 = t187 nand t13;
t189 = t167 nand t125;
t190 = t47 nand t15;
t191 = t100 nand t64;
t192 = t190 and t191;
t193 = t189 and t192;
t194 = t193 nand t17;
t195 = t167 nand t131;
t196 = t47 nand t19;
t197 = t100 nand t69;
t198 = t196 and t197;
t199 = t195 and t198;
t200 = t199 nand t21;
t201 = t167 nand t148;
t202 = t47 nand t31;
t203 = t100 nand t83;
t204 = t202 and t203;
t205 = t201 and t204;
t206 = t205 nand t33;
t207 = t167 nand t137;
t208 = t47 nand t23;
t209 = t100 nand t74;
t210 = t208 and t209;
t211 = t207 and t210;
t212 = t211 nand t25;
t213 = t206 and t212;
t214 = t200 and t213;
t215 = t194 and t214;
t216 = t188 and t215;
t217 = t182 and t216;
t218 = t176 and t217;
t219 = t167 nand t161;
t220 = t47 nand t42;
t221 = t100 nand t95;
t222 = t220 and t221;
t223 = t219 and t222;
t224 = t223 nand t44;
t225 = t218 and t224;
t226 = t170 nor t225;
t227 = t218 and t96;
t228 = t170 nor t227;
t229 = t226 biimp t228;
t230 = not t188;
t231 = t212 and t200;
t232 = t230 and t231;
t233 = t232 nand t194;
t234 = not t200;
t235 = t212 nand t234;
t236 = t206 and t235;
t237 = t233 and t236;
t238 = t182 and t231;
t239 = not t176;
t240 = t238 nand t239;
t241 = t237 nand t240;
t242 = t212 and t182;
t243 = t242 nand t239;
t244 = t237 nand t243;
t245 = t241 biimp t244;

tautology t229;
tautology t245;