-
Notifications
You must be signed in to change notification settings - Fork 6
/
Copy pathc1355.cal
818 lines (813 loc) · 17.3 KB
/
c1355.cal
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
/* BDD Calculator data file */
initial 10000 10000;
inputs
_1gat _8gat _15gat _22gat _29gat _36gat _43gat _50gat _57gat _64gat
_71gat _78gat _85gat _92gat _99gat _106gat _113gat _120gat _127gat _134gat
_141gat _148gat _155gat _162gat _169gat _176gat _183gat _190gat _197gat _204gat
_211gat _218gat _225gat _226gat _227gat _228gat _229gat _230gat _231gat _232gat
_233gat ;
actions
autoreorder 0 sift;
t2 = _1gat;
t3 = _29gat;
t4 = t2 nand t3;
t5 = t2 nand t4;
t6 = t3 nand t4;
t7 = t5 nand t6;
t8 = _57gat;
t9 = _85gat;
t10 = t8 nand t9;
t11 = t8 nand t10;
t12 = t9 nand t10;
t13 = t11 nand t12;
t14 = t7 nand t13;
t15 = t7 nand t14;
t16 = t13 nand t14;
t17 = t15 nand t16;
t18 = _225gat;
t19 = _233gat;
t20 = t18 and t19;
t21 = _113gat;
t22 = _120gat;
t23 = t21 nand t22;
t24 = t21 nand t23;
t25 = t22 nand t23;
t26 = t24 nand t25;
t27 = _127gat;
t28 = _134gat;
t29 = t27 nand t28;
t30 = t27 nand t29;
t31 = t28 nand t29;
t32 = t30 nand t31;
t33 = t26 nand t32;
t34 = t26 nand t33;
t35 = t32 nand t33;
t36 = t34 nand t35;
t37 = _141gat;
t38 = _148gat;
t39 = t37 nand t38;
t40 = t37 nand t39;
t41 = t38 nand t39;
t42 = t40 nand t41;
t43 = _155gat;
t44 = _162gat;
t45 = t43 nand t44;
t46 = t43 nand t45;
t47 = t44 nand t45;
t48 = t46 nand t47;
t49 = t42 nand t48;
t50 = t42 nand t49;
t51 = t48 nand t49;
t52 = t50 nand t51;
t53 = t36 nand t52;
t54 = t36 nand t53;
t55 = t52 nand t53;
t56 = t54 nand t55;
t57 = t20 nand t56;
t58 = t20 nand t57;
t59 = t56 nand t57;
t60 = t58 nand t59;
t61 = t17 nand t60;
t62 = t17 nand t61;
t63 = t60 nand t61;
t64 = t62 nand t63;
t65 = t28 nand t44;
t66 = t28 nand t65;
t67 = t44 nand t65;
t68 = t66 nand t67;
t69 = _190gat;
t70 = _218gat;
t71 = t69 nand t70;
t72 = t69 nand t71;
t73 = t70 nand t71;
t74 = t72 nand t73;
t75 = t68 nand t74;
t76 = t68 nand t75;
t77 = t74 nand t75;
t78 = t76 nand t77;
t79 = _232gat;
t80 = t79 and t19;
t81 = _36gat;
t82 = t3 nand t81;
t83 = t3 nand t82;
t84 = t81 nand t82;
t85 = t83 nand t84;
t86 = _43gat;
t87 = _50gat;
t88 = t86 nand t87;
t89 = t86 nand t88;
t90 = t87 nand t88;
t91 = t89 nand t90;
t92 = t85 nand t91;
t93 = t85 nand t92;
t94 = t91 nand t92;
t95 = t93 nand t94;
t96 = _92gat;
t97 = t9 nand t96;
t98 = t9 nand t97;
t99 = t96 nand t97;
t100 = t98 nand t99;
t101 = _99gat;
t102 = _106gat;
t103 = t101 nand t102;
t104 = t101 nand t103;
t105 = t102 nand t103;
t106 = t104 nand t105;
t107 = t100 nand t106;
t108 = t100 nand t107;
t109 = t106 nand t107;
t110 = t108 nand t109;
t111 = t95 nand t110;
t112 = t95 nand t111;
t113 = t110 nand t111;
t114 = t112 nand t113;
t115 = t80 nand t114;
t116 = t80 nand t115;
t117 = t114 nand t115;
t118 = t116 nand t117;
t119 = t78 nand t118;
t120 = t78 nand t119;
t121 = t118 nand t119;
t122 = t120 nand t121;
t123 = not t122;
t124 = t27 nand t43;
t125 = t27 nand t124;
t126 = t43 nand t124;
t127 = t125 nand t126;
t128 = _183gat;
t129 = _211gat;
t130 = t128 nand t129;
t131 = t128 nand t130;
t132 = t129 nand t130;
t133 = t131 nand t132;
t134 = t127 nand t133;
t135 = t127 nand t134;
t136 = t133 nand t134;
t137 = t135 nand t136;
t138 = _231gat;
t139 = t138 and t19;
t140 = _8gat;
t141 = t2 nand t140;
t142 = t2 nand t141;
t143 = t140 nand t141;
t144 = t142 nand t143;
t145 = _15gat;
t146 = _22gat;
t147 = t145 nand t146;
t148 = t145 nand t147;
t149 = t146 nand t147;
t150 = t148 nand t149;
t151 = t144 nand t150;
t152 = t144 nand t151;
t153 = t150 nand t151;
t154 = t152 nand t153;
t155 = _64gat;
t156 = t8 nand t155;
t157 = t8 nand t156;
t158 = t155 nand t156;
t159 = t157 nand t158;
t160 = _71gat;
t161 = _78gat;
t162 = t160 nand t161;
t163 = t160 nand t162;
t164 = t161 nand t162;
t165 = t163 nand t164;
t166 = t159 nand t165;
t167 = t159 nand t166;
t168 = t165 nand t166;
t169 = t167 nand t168;
t170 = t154 nand t169;
t171 = t154 nand t170;
t172 = t169 nand t170;
t173 = t171 nand t172;
t174 = t139 nand t173;
t175 = t139 nand t174;
t176 = t173 nand t174;
t177 = t175 nand t176;
t178 = t137 nand t177;
t179 = t137 nand t178;
t180 = t177 nand t178;
t181 = t179 nand t180;
t182 = t21 nand t37;
t183 = t21 nand t182;
t184 = t37 nand t182;
t185 = t183 nand t184;
t186 = _169gat;
t187 = _197gat;
t188 = t186 nand t187;
t189 = t186 nand t188;
t190 = t187 nand t188;
t191 = t189 nand t190;
t192 = t185 nand t191;
t193 = t185 nand t192;
t194 = t191 nand t192;
t195 = t193 nand t194;
t196 = _229gat;
t197 = t196 and t19;
t198 = t154 nand t95;
t199 = t154 nand t198;
t200 = t95 nand t198;
t201 = t199 nand t200;
t202 = t197 nand t201;
t203 = t197 nand t202;
t204 = t201 nand t202;
t205 = t203 nand t204;
t206 = t195 nand t205;
t207 = t195 nand t206;
t208 = t205 nand t206;
t209 = t207 nand t208;
t210 = t22 nand t38;
t211 = t22 nand t210;
t212 = t38 nand t210;
t213 = t211 nand t212;
t214 = _176gat;
t215 = _204gat;
t216 = t214 nand t215;
t217 = t214 nand t216;
t218 = t215 nand t216;
t219 = t217 nand t218;
t220 = t213 nand t219;
t221 = t213 nand t220;
t222 = t219 nand t220;
t223 = t221 nand t222;
t224 = _230gat;
t225 = t224 and t19;
t226 = t169 nand t110;
t227 = t169 nand t226;
t228 = t110 nand t226;
t229 = t227 nand t228;
t230 = t225 nand t229;
t231 = t225 nand t230;
t232 = t229 nand t230;
t233 = t231 nand t232;
t234 = t223 nand t233;
t235 = t223 nand t234;
t236 = t233 nand t234;
t237 = t235 nand t236;
t238 = not t237;
t239 = t209 and t238;
t240 = t181 and t239;
t241 = t123 and t240;
t242 = t145 nand t86;
t243 = t145 nand t242;
t244 = t86 nand t242;
t245 = t243 nand t244;
t246 = t160 nand t101;
t247 = t160 nand t246;
t248 = t101 nand t246;
t249 = t247 nand t248;
t250 = t245 nand t249;
t251 = t245 nand t250;
t252 = t249 nand t250;
t253 = t251 nand t252;
t254 = _227gat;
t255 = t254 and t19;
t256 = t186 nand t214;
t257 = t186 nand t256;
t258 = t214 nand t256;
t259 = t257 nand t258;
t260 = t128 nand t69;
t261 = t128 nand t260;
t262 = t69 nand t260;
t263 = t261 nand t262;
t264 = t259 nand t263;
t265 = t259 nand t264;
t266 = t263 nand t264;
t267 = t265 nand t266;
t268 = t36 nand t267;
t269 = t36 nand t268;
t270 = t267 nand t268;
t271 = t269 nand t270;
t272 = t255 nand t271;
t273 = t255 nand t272;
t274 = t271 nand t272;
t275 = t273 nand t274;
t276 = t253 nand t275;
t277 = t253 nand t276;
t278 = t275 nand t276;
t279 = t277 nand t278;
t280 = not t279;
t281 = not t64;
t282 = t140 nand t81;
t283 = t140 nand t282;
t284 = t81 nand t282;
t285 = t283 nand t284;
t286 = t155 nand t96;
t287 = t155 nand t286;
t288 = t96 nand t286;
t289 = t287 nand t288;
t290 = t285 nand t289;
t291 = t285 nand t290;
t292 = t289 nand t290;
t293 = t291 nand t292;
t294 = _226gat;
t295 = t294 and t19;
t296 = t187 nand t215;
t297 = t187 nand t296;
t298 = t215 nand t296;
t299 = t297 nand t298;
t300 = t129 nand t70;
t301 = t129 nand t300;
t302 = t70 nand t300;
t303 = t301 nand t302;
t304 = t299 nand t303;
t305 = t299 nand t304;
t306 = t303 nand t304;
t307 = t305 nand t306;
t308 = t267 nand t307;
t309 = t267 nand t308;
t310 = t307 nand t308;
t311 = t309 nand t310;
t312 = t295 nand t311;
t313 = t295 nand t312;
t314 = t311 nand t312;
t315 = t313 nand t314;
t316 = t293 nand t315;
t317 = t293 nand t316;
t318 = t315 nand t316;
t319 = t317 nand t318;
t320 = t281 and t319;
t321 = t280 and t320;
t322 = t146 nand t87;
t323 = t146 nand t322;
t324 = t87 nand t322;
t325 = t323 nand t324;
t326 = t161 nand t102;
t327 = t161 nand t326;
t328 = t102 nand t326;
t329 = t327 nand t328;
t330 = t325 nand t329;
t331 = t325 nand t330;
t332 = t329 nand t330;
t333 = t331 nand t332;
t334 = _228gat;
t335 = t334 and t19;
t336 = t52 nand t307;
t337 = t52 nand t336;
t338 = t307 nand t336;
t339 = t337 nand t338;
t340 = t335 nand t339;
t341 = t335 nand t340;
t342 = t339 nand t340;
t343 = t341 nand t342;
t344 = t333 nand t343;
t345 = t333 nand t344;
t346 = t343 nand t344;
t347 = t345 nand t346;
t348 = not t347;
t349 = t321 and t348;
t350 = not t319;
t351 = t281 and t350;
t352 = t280 and t351;
t353 = t352 and t347;
t354 = t279 and t351;
t355 = t354 and t348;
t356 = t353 or t355;
t357 = t349 or t356;
t358 = t64 and t350;
t359 = t280 and t358;
t360 = t359 and t348;
t361 = t357 or t360;
t362 = t241 and t361;
t363 = t64 and t362;
t364 = t2 nand t363;
t365 = t2 nand t364;
t366 = t363 nand t364;
t367 = t365 nand t366;
t368 = t281 and t280;
t369 = t368 and t348;
t370 = t351 and t280;
t371 = t351 and t348;
t372 = t370 or t371;
t373 = t369 or t372;
t374 = t350 and t280;
t375 = t374 and t348;
t376 = t373 or t375;
t377 = t241 and t376;
t378 = t64 and t377;
t379 = t2 nand t378;
t380 = t2 nand t379;
t381 = t378 nand t379;
t382 = t380 nand t381;
t383 = t367 biimp t382;
t384 = t319 and t362;
t385 = t140 nand t384;
t386 = t140 nand t385;
t387 = t384 nand t385;
t388 = t386 nand t387;
t389 = t319 and t377;
t390 = t140 nand t389;
t391 = t140 nand t390;
t392 = t389 nand t390;
t393 = t391 nand t392;
t394 = t388 biimp t393;
t466 = not t209;
t467 = t466 and t237;
t468 = t181 and t467;
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;