forked from jpsety/verilog_benchmark_circuits
-
Notifications
You must be signed in to change notification settings - Fork 0
/
cavlc.v
1424 lines (1420 loc) · 47.8 KB
/
cavlc.v
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
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
// Generated by Cadence Genus(TM) Synthesis Solution 16.22-s033_1
// Generated on: Jan 17 2020 11:37:12 EST (Jan 17 2020 16:37:12 UTC)
// Verification Directory fv/cavlc
module cavlc(\totalcoeffs[0] , \totalcoeffs[1] , \totalcoeffs[2] ,
\totalcoeffs[3] , \totalcoeffs[4] , \ctable[0] , \ctable[1] ,
\ctable[2] , \trailingones[0] , \trailingones[1] , \coeff_token[0]
, \coeff_token[1] , \coeff_token[2] , \coeff_token[3] ,
\coeff_token[4] , \coeff_token[5] , \ctoken_len[0] ,
\ctoken_len[1] , \ctoken_len[2] , \ctoken_len[3] , \ctoken_len[4]
);
input \totalcoeffs[0] , \totalcoeffs[1] , \totalcoeffs[2] ,
\totalcoeffs[3] , \totalcoeffs[4] , \ctable[0] , \ctable[1] ,
\ctable[2] , \trailingones[0] , \trailingones[1] ;
output \coeff_token[0] , \coeff_token[1] , \coeff_token[2] ,
\coeff_token[3] , \coeff_token[4] , \coeff_token[5] ,
\ctoken_len[0] , \ctoken_len[1] , \ctoken_len[2] ,
\ctoken_len[3] , \ctoken_len[4] ;
wire \totalcoeffs[0] , \totalcoeffs[1] , \totalcoeffs[2] ,
\totalcoeffs[3] , \totalcoeffs[4] , \ctable[0] , \ctable[1] ,
\ctable[2] , \trailingones[0] , \trailingones[1] ;
wire \coeff_token[0] , \coeff_token[1] , \coeff_token[2] ,
\coeff_token[3] , \coeff_token[4] , \coeff_token[5] ,
\ctoken_len[0] , \ctoken_len[1] , \ctoken_len[2] ,
\ctoken_len[3] , \ctoken_len[4] ;
wire n22, n23, n24, n25, n26, n27, n28, n29;
wire n30, n31, n32, n33, n34, n35, n36, n37;
wire n38, n39, n40, n41, n42, n43, n44, n45;
wire n46, n47, n48, n49, n50, n51, n52, n53;
wire n54, n55, n56, n57, n58, n59, n60, n61;
wire n62, n63, n64, n65, n66, n67, n68, n69;
wire n70, n71, n72, n73, n74, n75, n76, n77;
wire n78, n79, n80, n81, n82, n83, n84, n85;
wire n86, n87, n88, n89, n90, n91, n92, n93;
wire n94, n95, n96, n97, n98, n99, n100, n101;
wire n102, n103, n104, n105, n106, n107, n108, n109;
wire n110, n111, n112, n113, n114, n115, n116, n117;
wire n118, n121, n122, n123, n124, n125, n126, n127;
wire n128, n129, n130, n131, n132, n133, n134, n135;
wire n136, n137, n139, n140, n142, n144, n145, n146;
wire n147, n148, n149, n150, n151, n152, n153, n154;
wire n155, n156, n157, n158, n159, n160, n161, n162;
wire n163, n164, n165, n166, n167, n168, n169, n170;
wire n171, n172, n173, n174, n175, n176, n177, n178;
wire n179, n180, n181, n182, n183, n184, n185, n186;
wire n187, n188, n189, n190, n191, n192, n193, n194;
wire n195, n196, n197, n198, n199, n200, n201, n202;
wire n203, n204, n205, n206, n207, n208, n209, n210;
wire n211, n212, n213, n214, n215, n216, n217, n220;
wire n221, n222, n223, n224, n225, n226, n227, n228;
wire n229, n230, n231, n232, n233, n234, n235, n236;
wire n237, n238, n239, n240, n241, n242, n243, n244;
wire n245, n246, n247, n248, n249, n250, n253, n255;
wire n256, n257, n258, n259, n260, n261, n262, n263;
wire n264, n265, n266, n267, n268, n269, n270, n271;
wire n272, n273, n274, n275, n276, n277, n278, n279;
wire n280, n281, n282, n283, n284, n288, n289, n290;
wire n291, n292, n293, n296, n297, n298, n299, n300;
wire n301, n302, n303, n304, n305, n306, n307, n308;
wire n309, n310, n311, n312, n313, n314, n315, n316;
wire n317, n318, n319, n320, n321, n322, n323, n324;
wire n325, n326, n327, n328, n329, n330, n331, n332;
wire n333, n334, n335, n336, n337, n338, n339, n340;
wire n341, n342, n343, n344, n345, n346, n347, n350;
wire n352, n353, n354, n355, n356, n357, n358, n359;
wire n360, n361, n362, n363, n364, n365, n366, n367;
wire n368, n369, n370, n371, n372, n373, n374, n375;
wire n376, n377, n378, n379, n380, n381, n382, n383;
wire n384, n385, n386, n387, n388, n389, n390, n391;
wire n392, n393, n394, n395, n396, n397, n398, n399;
wire n400, n401, n402, n403, n404, n405, n406, n407;
wire n408, n409, n410, n411, n412, n413, n414, n415;
wire n418, n419, n420, n422, n423, n424, n425, n426;
wire n427, n428, n430, n431, n432, n433, n435, n436;
wire n437, n438, n439, n440, n441, n442, n443, n444;
wire n445, n446, n447, n448, n449, n450, n451, n452;
wire n453, n454, n455, n456, n457, n458, n459, n460;
wire n461, n462, n463, n464, n465, n466, n467, n468;
wire n469, n470, n471, n472, n473, n474, n475, n476;
wire n477, n478, n479, n480, n481, n482, n483, n484;
wire n485, n486, n487, n488, n489, n490, n491, n492;
wire n493, n494, n495, n496, n497, n498, n499, n500;
wire n501, n502, n503, n504, n505, n506, n507, n508;
wire n509, n510, n511, n512, n513, n514, n515, n516;
wire n517, n518, n520, n521, n522, n523, n524, n525;
wire n526, n527, n528, n529, n530, n531, n532, n533;
wire n534, n535, n536, n537, n538, n539, n540, n541;
wire n542, n543, n544, n545, n546, n547, n548, n549;
wire n550, n551, n552, n553, n554, n555, n556, n557;
wire n558, n559, n560, n561, n562, n563, n564, n565;
wire n566, n567, n568, n569, n570, n571, n572, n573;
wire n574, n575, n576, n577, n578, n579, n580, n581;
wire n582, n583, n584, n585, n586, n587, n588, n589;
wire n590, n591, n592, n593, n594, n595, n596, n597;
wire n598, n599, n600, n601, n603, n605, n607, n608;
wire n609, n610, n611, n614, n615, n616, n617, n618;
wire n619, n620, n621, n622, n623, n624, n625, n626;
wire n627, n628, n629, n630, n631, n632, n633, n634;
wire n635, n636, n637, n638, n639, n640, n641, n642;
wire n643, n644, n645, n646, n647, n648, n649, n650;
wire n651, n652, n653, n654, n655, n656, n657, n658;
wire n659, n660, n661, n662, n663, n664, n665, n666;
wire n667, n669, n670, n671, n672, n673, n674, n675;
wire n676, n677, n678, n679, n680, n681, n682, n683;
wire n684, n685, n686, n687, n688, n689, n690, n691;
wire n692, n693, n694, n695, n696, n697, n698, n699;
wire n700, n701, n708, n709, n710, n711, n712, n713;
wire n_3, n_4, n_6, n_9, n_10, n_11, n_12, n_13;
wire n_14, n_16, n_17, n_18, n_19, n_20, n_22, n_23;
wire n_24, n_25, n_26, n_27, n_28, n_29, n_30, n_31;
wire n_32, n_33, n_34, n_35, n_36, n_37, n_39, n_40;
wire n_41, n_42, n_43, n_44, n_45, n_46, n_47, n_48;
wire n_49, n_50, n_51, n_52, n_54, n_55, n_56, n_57;
wire n_58, n_59, n_60, n_61, n_62, n_63, n_64, n_65;
wire n_66, n_67, n_68, n_69, n_70, n_71, n_72, n_73;
wire n_74, n_75, n_76, n_77, n_78, n_79, n_80, n_81;
wire n_82, n_83, n_84, n_85, n_86, n_87, n_88, n_89;
wire n_90, n_95, n_96, n_97, n_99, n_100, n_101, n_102;
wire n_103, n_104, n_105, n_106, n_107, n_108, n_109, n_111;
wire n_112, n_113, n_114, n_115, n_116, n_117, n_118, n_119;
wire n_120, n_121, n_122, n_123, n_124, n_125, n_126, n_127;
wire n_128, n_129, n_130, n_131, n_132, n_133, n_134, n_135;
wire n_136, n_137, n_138, n_139, n_140, n_141, n_142, n_143;
wire n_144, n_145, n_146, n_147, n_148, n_149, n_150, n_151;
wire n_152, n_153, n_154, n_155, n_156, n_157, n_158, n_159;
wire n_160, n_161, n_162, n_163, n_164, n_165, n_166, n_167;
wire n_169, n_170, n_171, n_172, n_173, n_174, n_175, n_176;
wire n_177, n_178, n_179, n_180, n_181, n_182, n_183, n_184;
wire n_185, n_186, n_187, n_188, n_189, n_190, n_191, n_192;
wire n_193, n_194, n_195, n_196, n_197, n_198, n_199, n_200;
wire n_202, n_203, n_204, n_205, n_206, n_207, n_208, n_209;
wire n_210, n_211, n_212, n_213, n_214, n_215, n_216, n_217;
wire n_218, n_219, n_220, n_221, n_222, n_223, n_224, n_230;
wire n_231, n_233, n_234, n_235, n_236, n_237, n_238, n_239;
wire n_240, n_241, n_242, n_243, n_244, n_245, n_246, n_247;
wire n_248, n_249, n_250, n_251, n_252, n_253, n_254, n_255;
wire n_256, n_257, n_258, n_259, n_260, n_261, n_262, n_263;
wire n_264, n_265, n_266, n_267, n_268, n_269, n_270, n_271;
wire n_272, n_273, n_274, n_275, n_276, n_277, n_278, n_279;
wire n_280, n_281, n_282, n_284, n_285, n_286, n_287, n_288;
wire n_289, n_290, n_291, n_292, n_293, n_294, n_295, n_296;
wire n_297, n_298, n_299, n_300, n_301, n_302, n_303, n_304;
wire n_305, n_306, n_307, n_308, n_309, n_310, n_311, n_312;
wire n_313, n_314, n_315, n_316, n_317, n_318, n_319, n_320;
wire n_321, n_322, n_323, n_324, n_325, n_326, n_327, n_328;
wire n_329, n_330, n_331, n_332, n_333, n_334, n_335, n_336;
wire n_337, n_338, n_339, n_340, n_345, n_346, n_347, n_348;
wire n_349, n_350, n_351, n_352, n_353, n_354, n_355, n_356;
wire n_357, n_358, n_359, n_360, n_361, n_362, n_363, n_364;
wire n_365, n_366, n_367, n_368, n_369, n_370, n_371, n_372;
wire n_373, n_374, n_375, n_376, n_377, n_378, n_379, n_380;
wire n_381, n_382, n_383, n_384, n_385, n_386, n_387, n_388;
wire n_389, n_390, n_391, n_392, n_393, n_394, n_395, n_396;
wire n_397, n_398, n_399, n_400, n_401, n_402, n_403, n_404;
wire n_405, n_406, n_407, n_408, n_409, n_410, n_411, n_412;
wire n_413, n_414, n_415, n_416, n_417, n_418, n_419, n_420;
wire n_421, n_422, n_423, n_424, n_425, n_426, n_427, n_428;
wire n_429, n_430, n_431, n_432, n_433, n_434, n_435, n_436;
wire n_437, n_438, n_439, n_440, n_441, n_442, n_443, n_444;
wire n_445, n_446, n_447, n_448, n_449, n_450, n_451, n_452;
wire n_453, n_454, n_455, n_456, n_457, n_458, n_459, n_460;
wire n_461, n_462, n_463, n_464, n_465, n_466, n_467, n_468;
wire n_469, n_470, n_471, n_472, n_473, n_474, n_475, n_476;
wire n_477, n_478, n_479, n_480, n_481, n_482, n_483, n_484;
wire n_485, n_486, n_487, n_488, n_489, n_490, n_491, n_492;
wire n_493, n_494, n_495, n_496, n_497, n_498, n_499, n_500;
wire n_501, n_502, n_503, n_504, n_505, n_506, n_507, n_508;
wire n_509, n_510, n_511, n_512, n_513, n_514, n_515, n_516;
wire n_517, n_518, n_519, n_520, n_521, n_522, n_523, n_524;
wire n_525, n_526, n_527, n_528, n_529, n_530, n_531, n_532;
wire n_533, n_534, n_535, n_536, n_537, n_538, n_539, n_540;
wire n_541, n_542, n_543, n_544, n_545, n_546, n_547, n_548;
wire n_549, n_550, n_551, n_552, n_553, n_554, n_555, n_556;
wire n_557, n_558, n_559, n_560, n_561, n_562, n_563, n_564;
wire n_565, n_566, n_567, n_568, n_569, n_570, n_571, n_572;
wire n_573, n_574, n_575, n_576, n_577, n_578, n_579, n_580;
wire n_581, n_582, n_583, n_584, n_585, n_593, n_594, n_595;
wire n_596, n_608, n_609, n_610, n_611, n_612, n_613, n_614;
wire n_615, n_616, n_617, n_618, n_619, n_620;
not g1 (n_3, \totalcoeffs[3] );
not g2 (n_4, \ctable[0] );
and g3 (n22, n_3, n_4);
not g4 (n_6, \totalcoeffs[1] );
and g5 (n23, n_6, \trailingones[1] );
not g6 (n_9, \totalcoeffs[0] );
and g7 (n24, n_9, \trailingones[1] );
not g8 (n_10, n24);
and g9 (n25, \totalcoeffs[1] , n_10);
not g10 (n_11, n23);
not g11 (n_12, n25);
and g12 (n26, n_11, n_12);
and g13 (n27, n22, n26);
not g14 (n_13, \trailingones[1] );
and g15 (n28, \totalcoeffs[0] , n_13);
not g16 (n_14, n28);
and g17 (n29, n_6, n_14);
and g18 (n30, \totalcoeffs[1] , n_13);
not g19 (n_16, \ctable[2] );
not g20 (n_17, n30);
and g21 (n31, n_16, n_17);
not g22 (n_18, n29);
and g23 (n32, n_18, n31);
not g24 (n_19, n27);
not g25 (n_20, n32);
and g26 (n33, n_19, n_20);
not g27 (n_22, \totalcoeffs[2] );
not g28 (n_23, n33);
and g29 (n34, n_22, n_23);
and g30 (n35, n_22, n_4);
not g31 (n_24, n35);
and g32 (n36, n_9, n_24);
and g33 (n37, \totalcoeffs[1] , \totalcoeffs[2] );
not g34 (n_25, n36);
not g35 (n_26, n37);
and g36 (n38, n_25, n_26);
not g37 (n_27, n38);
and g38 (n39, n_13, n_27);
and g39 (n40, n_22, n_3);
not g40 (n_28, n40);
and g41 (n41, \trailingones[1] , n_28);
and g42 (n42, \totalcoeffs[0] , \totalcoeffs[3] );
not g43 (n_29, n41);
not g44 (n_30, n42);
and g45 (n43, n_29, n_30);
not g46 (n_31, n43);
and g47 (n44, n_6, n_31);
and g48 (n45, \totalcoeffs[1] , n_3);
not g49 (n_32, n44);
not g50 (n_33, n45);
and g51 (n46, n_32, n_33);
not g52 (n_34, n39);
and g53 (n47, n_34, n46);
not g54 (n_35, n47);
and g55 (n48, n_16, n_35);
not g56 (n_36, n34);
not g57 (n_37, n48);
and g58 (n49, n_36, n_37);
not g59 (n_39, \trailingones[0] );
not g60 (n_40, n49);
and g61 (n50, n_39, n_40);
and g62 (n51, \ctable[2] , \trailingones[0] );
and g63 (n52, n_4, n51);
and g64 (n53, n_16, \trailingones[1] );
not g65 (n_41, n52);
not g66 (n_42, n53);
and g67 (n54, n_41, n_42);
not g68 (n_43, n54);
and g69 (n55, \totalcoeffs[1] , n_43);
and g70 (n56, \totalcoeffs[1] , n_16);
and g71 (n57, n_4, n_13);
not g72 (n_44, n56);
and g73 (n58, n_44, n57);
not g74 (n_45, n55);
not g75 (n_46, n58);
and g76 (n59, n_45, n_46);
and g77 (n60, \totalcoeffs[0] , n_22);
not g78 (n_47, n59);
and g79 (n61, n_47, n60);
and g80 (n62, \totalcoeffs[2] , n_13);
and g81 (n63, n_9, n_6);
and g82 (n64, n62, n63);
and g83 (n65, n52, n64);
not g84 (n_48, n61);
not g85 (n_49, n65);
and g86 (n66, n_48, n_49);
not g87 (n_50, n66);
and g88 (n67, n_3, n_50);
not g89 (n_51, n50);
not g90 (n_52, n67);
and g91 (n68, n_51, n_52);
not g92 (n_54, \ctable[1] );
not g93 (n_55, n68);
and g94 (n69, n_54, n_55);
and g95 (n70, n_9, n_22);
and g96 (n71, n23, n70);
not g97 (n_56, n71);
and g98 (n72, n_4, n_56);
not g99 (n_57, n72);
and g100 (n73, \ctable[1] , n_57);
and g101 (n74, n_9, n_13);
and g102 (n75, \totalcoeffs[0] , \trailingones[1] );
not g103 (n_58, n74);
not g104 (n_59, n75);
and g105 (n76, n_58, n_59);
not g106 (n_60, n76);
and g107 (n77, \totalcoeffs[1] , n_60);
and g108 (n78, \totalcoeffs[2] , n77);
and g109 (n79, \ctable[0] , n78);
not g110 (n_61, n73);
not g111 (n_62, n79);
and g112 (n80, n_61, n_62);
not g113 (n_63, n80);
and g114 (n81, \trailingones[0] , n_63);
and g115 (n82, n_6, n_10);
not g116 (n_64, n82);
and g117 (n83, n_39, n_64);
and g118 (n84, n_6, \totalcoeffs[2] );
and g119 (n85, n28, n84);
not g120 (n_65, n83);
not g121 (n_66, n85);
and g122 (n86, n_65, n_66);
not g123 (n_67, n86);
and g124 (n87, n_4, n_67);
not g125 (n_68, n81);
not g126 (n_69, n87);
and g127 (n88, n_68, n_69);
not g128 (n_70, n88);
and g129 (n89, \totalcoeffs[3] , n_70);
and g130 (n90, n_22, n_14);
not g131 (n_71, n90);
and g132 (n91, \ctable[1] , n_71);
and g133 (n92, n40, n77);
not g134 (n_72, n91);
not g135 (n_73, n92);
and g136 (n93, n_72, n_73);
not g137 (n_74, n93);
and g138 (n94, \ctable[0] , n_74);
and g139 (n95, \totalcoeffs[2] , \trailingones[1] );
and g140 (n96, n_22, n30);
not g141 (n_75, n95);
not g142 (n_76, n96);
and g143 (n97, n_75, n_76);
and g144 (n98, n_9, n_3);
not g145 (n_77, n97);
and g146 (n99, n_77, n98);
and g147 (n100, \ctable[1] , n99);
not g148 (n_78, n94);
not g149 (n_79, n100);
and g150 (n101, n_78, n_79);
not g151 (n_80, n101);
and g152 (n102, \trailingones[0] , n_80);
and g153 (n103, \totalcoeffs[2] , n_3);
and g154 (n104, n23, n103);
and g155 (n105, \totalcoeffs[1] , n_39);
not g156 (n_81, n104);
not g157 (n_82, n105);
and g158 (n106, n_81, n_82);
not g159 (n_83, n106);
and g160 (n107, n_9, n_83);
and g161 (n108, n_6, n_13);
and g162 (n109, n_22, \ctable[1] );
not g163 (n_84, n109);
and g164 (n110, \totalcoeffs[3] , n_84);
not g165 (n_85, n110);
and g166 (n111, n108, n_85);
not g167 (n_86, n111);
and g168 (n112, n_75, n_86);
not g169 (n_87, n112);
and g170 (n113, n_39, n_87);
not g171 (n_88, n107);
not g172 (n_89, n113);
and g173 (n114, n_88, n_89);
not g174 (n_90, n114);
and g175 (n115, n_4, n_90);
and g176 (n116, n_9, n40);
and g177 (n117, n_39, n108);
and g178 (n118, n116, n117);
not g186 (n_95, n121);
and g187 (n122, n_16, n_95);
not g188 (n_96, n69);
not g189 (n_97, n122);
and g190 (n123, n_96, n_97);
not g191 (n_99, \totalcoeffs[4] );
not g192 (n_100, n123);
and g193 (n124, n_99, n_100);
and g194 (n125, n_39, n_13);
and g195 (n126, n_54, n125);
and g196 (n127, \totalcoeffs[4] , \trailingones[0] );
and g197 (n128, \ctable[1] , n127);
not g198 (n_101, n126);
not g199 (n_102, n128);
and g200 (n129, n_101, n_102);
not g201 (n_103, n129);
and g202 (n130, \ctable[0] , n_103);
and g203 (n131, \ctable[1] , n_13);
and g204 (n132, \totalcoeffs[4] , \trailingones[1] );
not g205 (n_104, n131);
not g206 (n_105, n132);
and g207 (n133, n_104, n_105);
and g208 (n134, \ctable[0] , \ctable[1] );
not g209 (n_106, n133);
not g210 (n_107, n134);
and g211 (n135, n_106, n_107);
and g212 (n136, n_39, n135);
not g213 (n_108, n130);
not g214 (n_109, n136);
and g215 (n137, n_108, n_109);
and g218 (n139, n_6, n_3);
and g219 (n140, n_22, n139);
or g222 (\coeff_token[0] , n124, n142);
and g223 (n144, \totalcoeffs[0] , \trailingones[0] );
and g224 (n145, n95, n144);
and g225 (n146, n_22, n_39);
and g226 (n147, n74, n146);
not g227 (n_111, n145);
not g228 (n_112, n147);
and g229 (n148, n_111, n_112);
not g230 (n_113, n148);
and g231 (n149, \ctable[0] , n_113);
and g232 (n150, n_4, \trailingones[0] );
and g233 (n151, \ctable[1] , \trailingones[1] );
not g234 (n_114, n150);
not g235 (n_115, n151);
and g236 (n152, n_114, n_115);
not g237 (n_116, n152);
and g238 (n153, n_9, n_116);
and g239 (n154, \trailingones[0] , n151);
and g240 (n155, n_39, n57);
not g241 (n_117, n154);
not g242 (n_118, n155);
and g243 (n156, n_117, n_118);
not g244 (n_119, n153);
and g245 (n157, n_119, n156);
not g246 (n_120, n157);
and g247 (n158, \totalcoeffs[2] , n_120);
not g248 (n_121, n149);
not g249 (n_122, n158);
and g250 (n159, n_121, n_122);
not g251 (n_123, n159);
and g252 (n160, n_99, n_123);
and g253 (n161, n_54, \trailingones[1] );
and g254 (n162, \ctable[0] , n_39);
not g255 (n_124, n127);
not g256 (n_125, n162);
and g257 (n163, n_124, n_125);
not g258 (n_126, n163);
and g259 (n164, n_54, n_126);
not g260 (n_127, n164);
and g261 (n165, n_105, n_127);
not g262 (n_128, n161);
not g263 (n_129, n165);
and g264 (n166, n_128, n_129);
and g265 (n167, n70, n166);
not g266 (n_130, n160);
not g267 (n_131, n167);
and g268 (n168, n_130, n_131);
not g269 (n_132, n168);
and g270 (n169, n_6, n_132);
and g271 (n170, \ctable[1] , \trailingones[0] );
not g272 (n_133, n170);
and g273 (n171, n_116, n_133);
and g274 (n172, \totalcoeffs[0] , n171);
and g275 (n173, n_9, \ctable[0] );
and g276 (n174, n_39, \trailingones[1] );
and g277 (n175, n173, n174);
not g278 (n_134, n172);
not g279 (n_135, n175);
and g280 (n176, n_134, n_135);
not g281 (n_136, n176);
and g282 (n177, n_22, n_136);
and g283 (n178, n_54, n_39);
and g284 (n179, n_9, \ctable[1] );
not g285 (n_137, n179);
and g286 (n180, n_22, n_137);
not g287 (n_138, n180);
and g288 (n181, n150, n_138);
not g289 (n_139, n178);
not g290 (n_140, n181);
and g291 (n182, n_139, n_140);
not g292 (n_141, n182);
and g293 (n183, n_13, n_141);
not g294 (n_142, n177);
not g295 (n_143, n183);
and g296 (n184, n_142, n_143);
not g297 (n_144, n184);
and g298 (n185, \totalcoeffs[1] , n_144);
and g299 (n186, n_54, \trailingones[0] );
and g300 (n187, n62, n186);
not g301 (n_145, n185);
not g302 (n_146, n187);
and g303 (n188, n_145, n_146);
not g304 (n_147, n188);
and g305 (n189, n_99, n_147);
not g306 (n_148, n169);
not g307 (n_149, n189);
and g308 (n190, n_148, n_149);
not g309 (n_150, n190);
and g310 (n191, n_3, n_150);
and g311 (n192, \ctable[0] , n146);
and g312 (n193, n_3, n_39);
not g313 (n_151, n193);
and g314 (n194, n_114, n_151);
and g315 (n195, \totalcoeffs[0] , n194);
not g316 (n_152, n192);
not g317 (n_153, n195);
and g318 (n196, n_152, n_153);
not g319 (n_154, n196);
and g320 (n197, n_6, n_154);
and g321 (n198, \totalcoeffs[3] , \trailingones[0] );
not g322 (n_155, n198);
and g323 (n199, n_22, n_155);
not g324 (n_156, n199);
and g325 (n200, n_9, n_156);
and g326 (n201, n_22, \trailingones[0] );
and g327 (n202, \totalcoeffs[0] , n201);
and g328 (n203, \totalcoeffs[0] , n_4);
not g329 (n_157, n173);
not g330 (n_158, n203);
and g331 (n204, n_157, n_158);
not g332 (n_159, n202);
and g333 (n205, n_159, n204);
not g334 (n_160, n205);
and g335 (n206, \totalcoeffs[1] , n_160);
not g336 (n_161, n200);
not g337 (n_162, n206);
and g338 (n207, n_161, n_162);
not g339 (n_163, n197);
and g340 (n208, n_163, n207);
not g341 (n_164, n208);
and g342 (n209, n_54, n_164);
and g343 (n210, n_6, \ctable[1] );
not g344 (n_165, n210);
and g345 (n211, \totalcoeffs[2] , n_165);
and g346 (n212, n_6, n_39);
not g347 (n_166, n211);
not g348 (n_167, n212);
and g349 (n213, n_166, n_167);
and g350 (n214, \totalcoeffs[3] , n213);
and g351 (n215, n_9, \trailingones[0] );
and g352 (n216, n_6, n_54);
and g353 (n217, \totalcoeffs[0] , \totalcoeffs[1] );
not g355 (n_169, n217);
not g357 (n_170, n215);
not g360 (n_171, n214);
not g361 (n_172, n220);
and g362 (n221, n_171, n_172);
not g363 (n_173, n221);
and g364 (n222, n_4, n_173);
not g365 (n_174, n209);
not g366 (n_175, n222);
and g367 (n223, n_174, n_175);
not g368 (n_176, n223);
and g369 (n224, n_13, n_176);
and g370 (n225, \totalcoeffs[1] , \ctable[0] );
and g371 (n226, \totalcoeffs[3] , n_39);
and g372 (n227, n_6, n_22);
and g373 (n228, n226, n227);
not g374 (n_177, n225);
not g375 (n_178, n228);
and g376 (n229, n_177, n_178);
not g377 (n_179, n229);
and g378 (n230, \totalcoeffs[0] , n_179);
and g379 (n231, \ctable[0] , n_28);
and g380 (n232, \totalcoeffs[3] , n37);
not g381 (n_180, n231);
not g382 (n_181, n232);
and g383 (n233, n_180, n_181);
not g384 (n_182, n230);
and g385 (n234, n_182, n233);
not g386 (n_183, n234);
and g387 (n235, \ctable[1] , n_183);
and g388 (n236, n162, n232);
not g389 (n_184, n235);
not g390 (n_185, n236);
and g391 (n237, n_184, n_185);
not g392 (n_186, n237);
and g393 (n238, \trailingones[1] , n_186);
not g394 (n_187, n224);
not g395 (n_188, n238);
and g396 (n239, n_187, n_188);
not g397 (n_189, n239);
and g398 (n240, n_99, n_189);
not g399 (n_190, n191);
not g400 (n_191, n240);
and g401 (n241, n_190, n_191);
not g402 (n_192, n241);
and g403 (n242, n_16, n_192);
not g404 (n_193, n63);
and g405 (n243, \totalcoeffs[2] , n_193);
and g406 (n244, n90, n_169);
not g407 (n_194, n243);
not g408 (n_195, n244);
and g409 (n245, n_194, n_195);
and g410 (n246, n_39, n245);
and g411 (n247, n30, n201);
not g412 (n_196, n246);
not g413 (n_197, n247);
and g414 (n248, n_196, n_197);
not g415 (n_198, n248);
and g416 (n249, \ctable[2] , n_198);
not g417 (n_199, n64);
not g418 (n_200, n249);
and g419 (n250, n_199, n_200);
or g424 (\coeff_token[1] , n242, n253);
and g425 (n255, n_3, \trailingones[1] );
not g426 (n_202, n174);
and g427 (n256, n_33, n_202);
not g428 (n_203, n255);
not g429 (n_204, n256);
and g430 (n257, n_203, n_204);
and g431 (n258, n_54, n257);
not g432 (n_205, n201);
and g433 (n259, \totalcoeffs[3] , n_205);
not g434 (n_206, n259);
and g435 (n260, \ctable[0] , n_206);
and g436 (n261, \totalcoeffs[2] , n_4);
not g437 (n_207, n261);
and g438 (n262, \totalcoeffs[3] , n_207);
not g439 (n_208, n262);
and g440 (n263, \trailingones[0] , n_208);
not g441 (n_209, n260);
not g442 (n_210, n263);
and g443 (n264, n_209, n_210);
not g444 (n_211, n264);
and g445 (n265, \totalcoeffs[1] , n_211);
and g446 (n266, n_4, \ctable[1] );
and g447 (n267, n_39, n266);
and g448 (n268, n139, n267);
not g449 (n_212, n265);
not g450 (n_213, n268);
and g451 (n269, n_212, n_213);
not g452 (n_214, n269);
and g453 (n270, n_13, n_214);
and g454 (n271, n_6, n_156);
not g455 (n_215, n186);
and g456 (n272, \totalcoeffs[2] , n_215);
not g457 (n_216, n271);
not g458 (n_217, n272);
and g459 (n273, n_216, n_217);
not g460 (n_218, n273);
and g461 (n274, \ctable[0] , n_218);
and g462 (n275, \totalcoeffs[1] , \trailingones[0] );
not g463 (n_219, n275);
and g464 (n276, \ctable[1] , n_219);
not g465 (n_220, n276);
and g466 (n277, n_13, n_220);
not g467 (n_221, n277);
and g468 (n278, n_22, n_221);
and g469 (n279, n_6, n174);
not g470 (n_222, n278);
not g471 (n_223, n279);
and g472 (n280, n_222, n_223);
not g473 (n_224, n280);
and g474 (n281, \totalcoeffs[3] , n_224);
and g475 (n282, \ctable[1] , n_39);
and g476 (n283, \totalcoeffs[1] , n255);
and g477 (n284, n282, n283);
not g487 (n_230, n288);
and g488 (n289, n_99, n_230);
and g489 (n290, \trailingones[0] , n_13);
not g490 (n_231, n290);
and g491 (n291, n_139, n_231);
and g492 (n292, n_4, n291);
and g493 (n293, n_3, \totalcoeffs[4] );
not g498 (n_233, n289);
not g499 (n_234, n296);
and g500 (n297, n_233, n_234);
not g501 (n_235, n297);
and g502 (n298, n_9, n_235);
and g503 (n299, \trailingones[0] , n75);
not g504 (n_236, n125);
not g505 (n_237, n299);
and g506 (n300, n_236, n_237);
not g507 (n_238, n300);
and g508 (n301, \ctable[0] , n_238);
and g509 (n302, n_4, n95);
not g510 (n_239, n301);
not g511 (n_240, n302);
and g512 (n303, n_239, n_240);
not g513 (n_241, n303);
and g514 (n304, \totalcoeffs[1] , n_241);
and g515 (n305, n_202, n_231);
not g516 (n_242, n108);
and g517 (n306, n_242, n305);
not g518 (n_243, n306);
and g519 (n307, \totalcoeffs[2] , n_243);
not g520 (n_244, n304);
not g521 (n_245, n307);
and g522 (n308, n_244, n_245);
not g523 (n_246, n308);
and g524 (n309, n_3, n_246);
and g525 (n310, n_6, \totalcoeffs[3] );
not g526 (n_247, n310);
and g527 (n311, \ctable[0] , n_247);
and g528 (n312, n_22, n125);
not g529 (n_248, n311);
and g530 (n313, n_248, n312);
and g531 (n314, n_6, \trailingones[0] );
and g532 (n315, n41, n314);
not g533 (n_249, n313);
not g534 (n_250, n315);
and g535 (n316, n_249, n_250);
not g536 (n_251, n316);
and g537 (n317, \totalcoeffs[0] , n_251);
not g538 (n_252, n309);
not g539 (n_253, n317);
and g540 (n318, n_252, n_253);
not g541 (n_254, n318);
and g542 (n319, n_54, n_254);
and g543 (n320, \totalcoeffs[1] , \trailingones[1] );
and g544 (n321, \totalcoeffs[2] , n320);
not g545 (n_255, n314);
not g546 (n_256, n321);
and g547 (n322, n_255, n_256);
not g548 (n_257, n322);
and g549 (n323, \ctable[1] , n_257);
not g550 (n_258, n62);
and g551 (n324, \trailingones[0] , n_258);
and g552 (n325, \totalcoeffs[2] , n125);
not g553 (n_259, n324);
not g554 (n_260, n325);
and g555 (n326, n_259, n_260);
not g556 (n_261, n323);
and g557 (n327, n_261, n326);
not g558 (n_262, n327);
and g559 (n328, \totalcoeffs[3] , n_262);
and g560 (n329, \ctable[1] , n_11);
not g561 (n_263, n329);
and g562 (n330, n_17, n_263);
not g563 (n_264, n330);
and g564 (n331, \trailingones[0] , n_264);
not g565 (n_265, n320);
and g566 (n332, n_242, n_265);
not g567 (n_266, n332);
and g568 (n333, n193, n_266);
not g569 (n_267, n331);
not g570 (n_268, n333);
and g571 (n334, n_267, n_268);
not g572 (n_269, n334);
and g573 (n335, n_22, n_269);
not g574 (n_270, n328);
not g575 (n_271, n335);
and g576 (n336, n_270, n_271);
not g577 (n_272, n336);
and g578 (n337, n203, n_272);
not g579 (n_273, n319);
not g580 (n_274, n337);
and g581 (n338, n_273, n_274);
not g582 (n_275, n338);
and g583 (n339, n_99, n_275);
not g584 (n_276, n298);
not g585 (n_277, n339);
and g586 (n340, n_276, n_277);
not g587 (n_278, n340);
and g588 (n341, n_16, n_278);
and g589 (n342, n_4, n_54);
and g590 (n343, n51, n75);
not g591 (n_279, n343);
and g592 (n344, n_58, n_279);
not g593 (n_280, n344);
and g594 (n345, \totalcoeffs[1] , n_280);
and g595 (n346, n28, n212);
not g596 (n_281, n345);
not g597 (n_282, n346);
and g598 (n347, n_281, n_282);
or g603 (\coeff_token[2] , n341, n350);
and g604 (n352, \totalcoeffs[3] , n_128);
and g605 (n353, \totalcoeffs[2] , \ctable[1] );
not g606 (n_284, n352);
not g607 (n_285, n353);
and g608 (n354, n_284, n_285);
not g609 (n_286, n354);
and g610 (n355, n_99, n_286);
and g611 (n356, \trailingones[0] , \trailingones[1] );
and g612 (n357, n342, n356);
not g613 (n_287, n357);
and g614 (n358, n_107, n_287);
and g615 (n359, n_22, n293);
not g616 (n_288, n358);
and g617 (n360, n_288, n359);
not g618 (n_289, n355);
not g619 (n_290, n360);
and g620 (n361, n_289, n_290);
not g621 (n_291, n361);
and g622 (n362, n_6, n_291);
and g623 (n363, \ctable[0] , \trailingones[0] );
and g624 (n364, n161, n363);
not g625 (n_292, n364);
and g626 (n365, n_118, n_292);
not g627 (n_293, n365);
and g628 (n366, \totalcoeffs[2] , n_293);
and g629 (n367, \ctable[0] , n_215);
not g630 (n_294, n367);
and g631 (n368, \totalcoeffs[3] , n_294);
not g632 (n_295, n267);
not g633 (n_296, n368);
and g634 (n369, n_295, n_296);
not g635 (n_297, n366);
and g636 (n370, n_297, n369);
not g637 (n_298, n370);
and g638 (n371, \totalcoeffs[1] , n_298);
and g639 (n372, \totalcoeffs[2] , n266);
not g640 (n_299, n371);
not g641 (n_300, n372);
and g642 (n373, n_299, n_300);
not g643 (n_301, n373);
and g644 (n374, n_99, n_301);
not g645 (n_302, n362);
not g646 (n_303, n374);
and g647 (n375, n_302, n_303);
not g648 (n_304, n375);
and g649 (n376, n_9, n_304);
not g650 (n_305, n194);
and g651 (n377, \totalcoeffs[2] , n_305);
and g652 (n378, n_22, n363);
not g653 (n_306, n377);
not g654 (n_307, n378);
and g655 (n379, n_306, n_307);
not g656 (n_308, n379);
and g657 (n380, n_13, n_308);
and g658 (n381, \ctable[0] , \trailingones[1] );
and g659 (n382, n_39, n381);
not g660 (n_309, n382);
and g661 (n383, n_3, n_309);
not g662 (n_310, n383);
and g663 (n384, n_22, n_310);
not g664 (n_311, n226);
and g665 (n385, n_54, n_311);
and g666 (n386, \totalcoeffs[3] , n_4);
not g667 (n_312, n385);
not g668 (n_313, n386);
and g669 (n387, n_312, n_313);
not g670 (n_314, n384);
not g671 (n_315, n387);
and g672 (n388, n_314, n_315);
not g673 (n_316, n380);
and g674 (n389, n_316, n388);
not g675 (n_317, n389);
and g676 (n390, \totalcoeffs[1] , n_317);
and g677 (n391, n_3, n266);
and g678 (n392, n192, n216);
not g679 (n_318, n391);
not g680 (n_319, n392);
and g681 (n393, n_318, n_319);
not g682 (n_320, n393);
and g683 (n394, n_13, n_320);
not g684 (n_321, n390);
not g685 (n_322, n394);
and g686 (n395, n_321, n_322);
not g687 (n_323, n395);
and g688 (n396, \totalcoeffs[0] , n_323);
and g689 (n397, n_28, n266);
and g690 (n398, \totalcoeffs[3] , n_54);
and g691 (n399, \totalcoeffs[2] , n398);
not g692 (n_324, n397);
not g693 (n_325, n399);
and g694 (n400, n_324, n_325);
not g695 (n_326, n400);
and g696 (n401, \trailingones[1] , n_326);
and g697 (n402, n_13, n266);
not g698 (n_327, n398);
not g699 (n_328, n402);
and g700 (n403, n_327, n_328);
not g701 (n_329, n403);
and g702 (n404, n_39, n_329);
not g703 (n_330, n401);
not g704 (n_331, n404);
and g705 (n405, n_330, n_331);
not g706 (n_332, n405);
and g707 (n406, n_6, n_332);
not g708 (n_333, n57);
and g709 (n407, n_333, n_139);
not g710 (n_334, n407);
and g711 (n408, n_22, n_334);
not g712 (n_335, n381);
and g713 (n409, n_54, n_335);
not g714 (n_336, n363);
and g715 (n410, n_265, n_336);
not g716 (n_337, n410);
and g717 (n411, n409, n_337);
not g718 (n_338, n408);
not g719 (n_339, n411);
and g720 (n412, n_338, n_339);
not g721 (n_340, n412);
and g722 (n413, \totalcoeffs[3] , n_340);
and g723 (n414, \totalcoeffs[1] , n290);
and g724 (n415, n266, n414);
not g732 (n_345, n418);
and g733 (n419, n_99, n_345);
not g734 (n_346, n376);
not g735 (n_347, n419);
and g736 (n420, n_346, n_347);
not g737 (n_348, n420);
and g738 (\coeff_token[3] , n_16, n_348);
and g739 (n422, n_99, n243);
and g740 (n423, \totalcoeffs[3] , n_99);
not g741 (n_349, n293);
not g742 (n_350, n423);
and g743 (n424, n_349, n_350);
and g744 (n425, n_9, n227);
not g745 (n_351, n424);
and g746 (n426, n_351, n425);
not g747 (n_352, n422);
not g748 (n_353, n426);
and g749 (n427, n_352, n_353);
not g750 (n_354, n427);
and g751 (n428, n_16, n_354);
and g752 (\coeff_token[4] , n134, n428);
and g753 (n430, n63, n359);
not g754 (n_355, n425);
and g755 (n431, n423, n_355);
not g756 (n_356, n430);
not g757 (n_357, n431);
and g758 (n432, n_356, n_357);
not g759 (n_358, n432);
and g760 (n433, n_16, n_358);
and g761 (\coeff_token[5] , n134, n433);
and g762 (n435, n_6, n_4);
not g763 (n_359, n435);
and g764 (n436, \totalcoeffs[2] , n_359);
not g765 (n_360, n436);
and g766 (n437, n_13, n_360);
and g767 (n438, n_54, n437);
and g768 (n439, \ctable[0] , n320);
not g769 (n_361, n438);
not g770 (n_362, n439);
and g771 (n440, n_361, n_362);
not g772 (n_363, n440);
and g773 (n441, \totalcoeffs[0] , n_363);
and g774 (n442, n_9, n_333);
and g775 (n443, \totalcoeffs[2] , n442);
not g776 (n_364, n441);
not g777 (n_365, n443);
and g778 (n444, n_364, n_365);
not g779 (n_366, n444);
and g780 (n445, \trailingones[0] , n_366);
and g781 (n446, \totalcoeffs[2] , n24);
not g782 (n_367, n117);
not g783 (n_368, n446);
and g784 (n447, n_367, n_368);
not g785 (n_369, n447);
and g786 (n448, \ctable[0] , n_369);
not g787 (n_370, n445);
not g788 (n_371, n448);
and g789 (n449, n_370, n_371);
not g790 (n_372, n356);
and g791 (n450, n_236, n_372);
not g792 (n_373, n450);
and g793 (n451, \ctable[1] , n_373);
and g794 (n452, n_22, \trailingones[1] );
not g795 (n_374, n452);
and g796 (n453, n_258, n_374);
and g797 (n454, n451, n453);
not g798 (n_375, n454);
and g799 (n455, n449, n_375);
not g800 (n_376, n455);
and g801 (n456, n_16, n_376);
and g802 (n457, \ctable[2] , n_13);
not g803 (n_377, n457);
and g804 (n458, \trailingones[0] , n_377);
not g805 (n_378, n458);
and g806 (n459, n84, n_378);
not g807 (n_379, n459);
and g808 (n460, n_76, n_379);
not g809 (n_380, n460);
and g810 (n461, n_9, n_380);
and g811 (n462, n144, n320);
not g812 (n_381, n462);
and g813 (n463, n_236, n_381);
not g814 (n_382, n463);
and g815 (n464, \ctable[2] , n_382);
and g816 (n465, n_22, n464);
not g817 (n_383, n461);
not g818 (n_384, n465);
and g819 (n466, n_383, n_384);
not g820 (n_385, n466);
and g821 (n467, n342, n_385);
not g822 (n_386, n456);
not g823 (n_387, n467);
and g824 (n468, n_386, n_387);
not g825 (n_388, n468);
and g826 (n469, n_3, n_388);
and g827 (n470, n_367, n_265);
not g828 (n_389, n470);
and g829 (n471, \totalcoeffs[0] , n_389);
and g830 (n472, \totalcoeffs[2] , n30);
not g831 (n_390, n471);
not g832 (n_391, n472);
and g833 (n473, n_390, n_391);
and g834 (n474, n_9, n_54);
and g835 (n475, n_167, n332);
and g836 (n476, n474, n475);
not g837 (n_392, n476);
and g838 (n477, n473, n_392);
not g839 (n_393, n477);
and g840 (n478, n_4, n_393);
and g841 (n479, n_39, n217);
and g842 (n480, \totalcoeffs[0] , n170);
not g843 (n_394, n480);
and g844 (n481, n_82, n_394);
not g845 (n_395, n481);
and g846 (n482, n_22, n_395);
not g847 (n_396, n479);
not g848 (n_397, n482);
and g849 (n483, n_396, n_397);
not g850 (n_398, n483);
and g851 (n484, \trailingones[1] , n_398);
and g852 (n485, n_9, n_39);
not g853 (n_399, n485);
and g854 (n486, n_158, n_399);
and g855 (n487, n30, n486);
not g856 (n_400, n484);
not g857 (n_401, n487);
and g858 (n488, n_400, n_401);
not g859 (n_402, n478);
and g860 (n489, n_402, n488);
not g861 (n_403, n489);
and g862 (n490, \totalcoeffs[3] , n_403);