;  combinational logic example "c5315"
;-------------------------------------------------------------
;
;
;  total number of lines in the netlist ..............  5315
;  simplistically reduced equivalent fault set size =   5350
;        lines from primary input  gates .......   178
;        lines from primary output gates .......   123
;        lines from interior gate outputs ......  2184
;        lines from **   806 ** fanout stems ...  2830
;
;        avg_fanin  =  1.90,     max_fanin  =  9
;        avg_fanout =  3.51,     max_fanout = 15
;
;
;
;
;
(:inputs
1                               	;... primary input
4                               	;... primary input
11                              	;... primary input
14                              	;... primary input
17                              	;... primary input
20                              	;... primary input
23                              	;... primary input
24                              	;... primary input
25                              	;... primary input
26                              	;... primary input
27                              	;... primary input
31                              	;... primary input
34                              	;... primary input
37                              	;... primary input
40                              	;... primary input
43                              	;... primary input
46                              	;... primary input
49                              	;... primary input
52                              	;... primary input
53                              	;... primary input
54                              	;... primary input
61                              	;... primary input
64                              	;... primary input
67                              	;... primary input
70                              	;... primary input
73                              	;... primary input
76                              	;... primary input
79                              	;... primary input
80                              	;... primary input
81                              	;... primary input
82                              	;... primary input
83                              	;... primary input
86                              	;... primary input
87                              	;... primary input
88                              	;... primary input
91                              	;... primary input
94                              	;... primary input
97                              	;... primary input
100                             	;... primary input
103                             	;... primary input
106                             	;... primary input
109                             	;... primary input
112                             	;... primary input
113                             	;... primary input
114                             	;... primary input
115                             	;... primary input
116                             	;... primary input
117                             	;... primary input
118                             	;... primary input
119                             	;... primary input
120                             	;... primary input
121                             	;... primary input
122                             	;... primary input
123                             	;... primary input
126                             	;... primary input
127                             	;... primary input
128                             	;... primary input
129                             	;... primary input
130                             	;... primary input
131                             	;... primary input
132                             	;... primary input
135                             	;... primary input
136                             	;... primary input
137                             	;... primary input
140                             	;... primary input
141                             	;... primary input
145                             	;... primary input
146                             	;... primary input
149                             	;... primary input
152                             	;... primary input
155                             	;... primary input
158                             	;... primary input
161                             	;... primary input
164                             	;... primary input
167                             	;... primary input
170                             	;... primary input
173                             	;... primary input
176                             	;... primary input
179                             	;... primary input
182                             	;... primary input
185                             	;... primary input
188                             	;... primary input
191                             	;... primary input
194                             	;... primary input
197                             	;... primary input
200                             	;... primary input
203                             	;... primary input
206                             	;... primary input
209                             	;... primary input
210                             	;... primary input
217                             	;... primary input
218                             	;... primary input
225                             	;... primary input
226                             	;... primary input
233                             	;... primary input
234                             	;... primary input
241                             	;... primary input
242                             	;... primary input
245                             	;... primary input
248                             	;... primary input
251                             	;... primary input
254                             	;... primary input
257                             	;... primary input
264                             	;... primary input
265                             	;... primary input
272                             	;... primary input
273                             	;... primary input
280                             	;... primary input
281                             	;... primary input
288                             	;... primary input
289                             	;... primary input
292                             	;... primary input
293                             	;... primary input
299                             	;... primary input
302                             	;... primary input
307                             	;... primary input
308                             	;... primary input
315                             	;... primary input
316                             	;... primary input
323                             	;... primary input
324                             	;... primary input
331                             	;... primary input
332                             	;... primary input
335                             	;... primary input
338                             	;... primary input
341                             	;... primary input
348                             	;... primary input
351                             	;... primary input
358                             	;... primary input
361                             	;... primary input
366                             	;... primary input
369                             	;... primary input
372                             	;... primary input
373                             	;... primary input
374                             	;... primary input
386                             	;... primary input
389                             	;... primary input
400                             	;... primary input
411                             	;... primary input
422                             	;... primary input
435                             	;... primary input
446                             	;... primary input
457                             	;... primary input
468                             	;... primary input
479                             	;... primary input
490                             	;... primary input
503                             	;... primary input
514                             	;... primary input
523                             	;... primary input
534                             	;... primary input
545                             	;... primary input
549                             	;... primary input
552                             	;... primary input
556                             	;... primary input
559                             	;... primary input
562                             	;... primary input
1497                            	;... primary input
1689                            	;... primary input
1690                            	;... primary input
1691                            	;... primary input
1694                            	;... primary input
2174                            	;... primary input
2358                            	;... primary input
2824                            	;... primary input
3173                            	;... primary input
3546                            	;... primary input
3548                            	;... primary input
3550                            	;... primary input
3552                            	;... primary input
3717                            	;... primary input
3724                            	;... primary input
4087                            	;... primary input
4088                            	;... primary input
4089                            	;... primary input
4090                            	;... primary input
4091                            	;... primary input
4092                            	;... primary input
4115                            	;... primary input
)                                	;... primary input
;
;
(:outputs
144                             	;... primary output
298                             	;... primary output
973                             	;... primary output
594                             	;... primary output
599                             	;... primary output
600                             	;... primary output
601                             	;... primary output
602                             	;... primary output
603                             	;... primary output
604                             	;... primary output
611                             	;... primary output
612                             	;... primary output
810                             	;... primary output
848                             	;... primary output
849                             	;... primary output
850                             	;... primary output
851                             	;... primary output
634                             	;... primary output
815                             	;... primary output
845                             	;... primary output
847                             	;... primary output
926                             	;... primary output
923                             	;... primary output
921                             	;... primary output
892                             	;... primary output
887                             	;... primary output
606                             	;... primary output
656                             	;... primary output
809                             	;... primary output
993                             	;... primary output
978                             	;... primary output
949                             	;... primary output
939                             	;... primary output
889                             	;... primary output
593                             	;... primary output
636                             	;... primary output
704                             	;... primary output
717                             	;... primary output
820                             	;... primary output
639                             	;... primary output
673                             	;... primary output
707                             	;... primary output
715                             	;... primary output
598                             	;... primary output
610                             	;... primary output
588                             	;... primary output
615                             	;... primary output
626                             	;... primary output
632                             	;... primary output
1002                            	;... primary output
1004                            	;... primary output
591                             	;... primary output
618                             	;... primary output
621                             	;... primary output
629                             	;... primary output
822                             	;... primary output
838                             	;... primary output
861                             	;... primary output
623                             	;... primary output
722                             	;... primary output
832                             	;... primary output
834                             	;... primary output
836                             	;... primary output
859                             	;... primary output
871                             	;... primary output
873                             	;... primary output
875                             	;... primary output
877                             	;... primary output
998                             	;... primary output
1000                            	;... primary output
575                             	;... primary output
585                             	;... primary output
661                             	;... primary output
693                             	;... primary output
747                             	;... primary output
752                             	;... primary output
757                             	;... primary output
762                             	;... primary output
787                             	;... primary output
792                             	;... primary output
797                             	;... primary output
802                             	;... primary output
642                             	;... primary output
664                             	;... primary output
667                             	;... primary output
670                             	;... primary output
676                             	;... primary output
696                             	;... primary output
699                             	;... primary output
702                             	;... primary output
818                             	;... primary output
813                             	;... primary output
824                             	;... primary output
826                             	;... primary output
828                             	;... primary output
830                             	;... primary output
854                             	;... primary output
863                             	;... primary output
865                             	;... primary output
867                             	;... primary output
869                             	;... primary output
712                             	;... primary output
727                             	;... primary output
732                             	;... primary output
737                             	;... primary output
742                             	;... primary output
772                             	;... primary output
777                             	;... primary output
782                             	;... primary output
645                             	;... primary output
648                             	;... primary output
651                             	;... primary output
654                             	;... primary output
679                             	;... primary output
682                             	;... primary output
685                             	;... primary output
688                             	;... primary output
843                             	;... primary output
882                             	;... primary output
767                             	;... primary output
807                             	;... primary output
658                             	;... primary output
690                             	;... primary output
)                                	;... primary output
;
;
;	Output	Type	Inputs...
;	------	----	---------
(:gates
	(144	buff	141)
	(298	buff	293)
	(4114	and	135	4115)
	(2825	not	2824)
	(973	buff	3173)
	(3547	not	3546)
	(3549	not	3548)
	(3551	not	3550)
	(3553	not	3552)
	(594	not	545)
	(599	not	348)
	(600	not	366)
	(601	and	552	562)
	(602	not	549)
	(603	not	545)
	(604	not	545)
	(611	not	338)
	(612	not	358)
	(633	nand	373	1)
	(810	and	141	145)
	(814	not	3173)
	(816	not	4114)
	(844	and	2825	27)
	(846	and	386	556)
	(848	not	245)
	(849	not	552)
	(850	not	562)
	(851	not	559)
	(852	and	386	559	556	552)
	(1502	not	1497)
	(1528	buff	1689)
	(1552	buff	1690)
	(1609	buff	1689)
	(1633	buff	1690)
	(1697	buff	137)
	(1698	buff	137)
	(1701	buff	141)
	(2179	not	2174)
	(2203	buff	1691)
	(2226	buff	1694)
	(2281	buff	1691)
	(2304	buff	1694)
	(2361	buff	254)
	(2370	buff	251)
	(2382	buff	251)
	(2393	buff	248)
	(2405	buff	248)
	(2418	buff	4088)
	(2442	buff	4087)
	(2476	buff	4089)
	(2500	buff	4090)
	(2533	buff	210)
	(2537	buff	210)
	(2541	buff	218)
	(2545	buff	218)
	(2549	buff	226)
	(2553	buff	226)
	(2557	buff	234)
	(2561	buff	234)
	(2627	buff	257)
	(2631	buff	257)
	(2635	buff	265)
	(2639	buff	265)
	(2643	buff	273)
	(2647	buff	273)
	(2651	buff	281)
	(2655	buff	281)
	(2721	buff	335)
	(2734	buff	335)
	(2816	buff	206)
	(2822	and	27	31)
	(2826	buff	1)
	(2828	buff	2358)
	(2882	buff	293)
	(2886	buff	302)
	(2890	buff	308)
	(2894	buff	308)
	(2898	buff	316)
	(2902	buff	316)
	(2948	buff	324)
	(2952	buff	324)
	(2956	buff	341)
	(2960	buff	341)
	(2964	buff	351)
	(2968	buff	351)
	(3024	buff	257)
	(3028	buff	257)
	(3032	buff	265)
	(3036	buff	265)
	(3040	buff	273)
	(3044	buff	273)
	(3048	buff	281)
	(3052	buff	281)
	(3092	buff	332)
	(3105	buff	332)
	(3175	buff	549)
	(3176	and	31	27)
	(3181	not	2358)
	(3204	buff	324)
	(3208	buff	324)
	(3212	buff	341)
	(3216	buff	341)
	(3220	buff	351)
	(3224	buff	351)
	(3256	buff	293)
	(3260	buff	302)
	(3264	buff	308)
	(3268	buff	308)
	(3272	buff	316)
	(3276	buff	316)
	(3302	buff	361)
	(3314	buff	361)
	(3354	buff	210)
	(3358	buff	210)
	(3362	buff	218)
	(3366	buff	218)
	(3370	buff	226)
	(3374	buff	226)
	(3378	buff	234)
	(3382	buff	234)
	(3440	not	324)
	(3554	buff	242)
	(3555	buff	242)
	(3556	buff	254)
	(3558	buff	4088)
	(3582	buff	4087)
	(3616	buff	4092)
	(3628	buff	4091)
	(3660	buff	4089)
	(3684	buff	4090)
	(3721	not	3717)
	(3728	not	3724)
	(3737	buff	4091)
	(3757	buff	4092)
	(3795	buff	4091)
	(3815	buff	4092)
	(3972	buff	4091)
	(3991	buff	4092)
	(4030	buff	4091)
	(4049	buff	4092)
	(4110	buff	299)
	(4119	buff	446)
	(4127	buff	457)
	(4135	buff	468)
	(4143	buff	422)
	(4151	buff	435)
	(4159	buff	389)
	(4167	buff	400)
	(4175	buff	411)
	(4183	buff	374)
	(4188	buff	4)
	(4276	buff	446)
	(4284	buff	457)
	(4292	buff	468)
	(4300	buff	435)
	(4308	buff	389)
	(4316	buff	400)
	(4324	buff	411)
	(4332	buff	422)
	(4340	buff	374)
	(4631	buff	479)
	(4639	buff	490)
	(4647	buff	503)
	(4655	buff	514)
	(4663	buff	523)
	(4671	buff	534)
	(4676	buff	54)
	(4764	buff	479)
	(4772	buff	503)
	(4780	buff	514)
	(4788	buff	523)
	(4796	buff	534)
	(4804	buff	490)
	(5082	buff	361)
	(5085	buff	369)
	(5090	buff	341)
	(5093	buff	351)
	(5098	buff	308)
	(5101	buff	316)
	(5108	buff	293)
	(5111	buff	302)
	(5332	buff	281)
	(5335	buff	289)
	(5340	buff	265)
	(5343	buff	273)
	(5348	buff	234)
	(5351	buff	257)
	(5356	buff	218)
	(5359	buff	226)
	(5369	buff	210)
	(634	not	633)
	(815	and	136	814)
	(845	not	844)
	(847	not	846)
	(926	buff	1697)
	(923	buff	1701)
	(921	buff	2826)
	(2979	and	3553	514)
	(2999	or	3547	514)
	(892	buff	3175)
	(887	buff	4110)
	(606	not	3175)
	(1580	and	170	1528	1552)
	(1586	and	173	1528	1552)
	(1592	and	167	1528	1552)
	(1598	and	164	1528	1552)
	(1604	and	161	1528	1552)
	(656	nand	2822	140)
	(1668	and	185	1609	1633)
	(1674	and	158	1609	1633)
	(1680	and	152	1609	1633)
	(1686	and	146	1609	1633)
	(2254	and	170	2203	2226)
	(2260	and	173	2203	2226)
	(2266	and	167	2203	2226)
	(2272	and	164	2203	2226)
	(2278	and	161	2203	2226)
	(2339	and	185	2281	2304)
	(2345	and	158	2281	2304)
	(2351	and	152	2281	2304)
	(2357	and	146	2281	2304)
	(711	and	106	3660	3684)
	(721	and	61	2418	2442)
	(726	and	106	3558	3582)
	(731	and	49	3558	3582)
	(736	and	103	3558	3582)
	(741	and	40	3558	3582)
	(746	and	37	3558	3582)
	(751	and	20	2418	2442)
	(756	and	17	2418	2442)
	(761	and	70	2418	2442)
	(766	and	64	2418	2442)
	(771	and	49	3660	3684)
	(776	and	103	3660	3684)
	(781	and	40	3660	3684)
	(786	and	37	3660	3684)
	(791	and	20	2476	2500)
	(796	and	17	2476	2500)
	(801	and	70	2476	2500)
	(806	and	64	2476	2500)
	(809	not	2822)
	(3734	and	123	3728	3717)
	(842	and	3795	3815)
	(858	and	61	2476	2500)
	(881	and	3737	3757)
	(4123	not	4119)
	(4131	not	4127)
	(4139	not	4135)
	(4147	not	4143)
	(4155	not	4151)
	(4163	not	4159)
	(4171	not	4167)
	(4179	not	4175)
	(4187	not	4183)
	(4194	not	4188)
	(4282	not	4276)
	(4290	not	4284)
	(4298	not	4292)
	(4306	not	4300)
	(4314	not	4308)
	(4322	not	4316)
	(4330	not	4324)
	(4338	not	4332)
	(4346	not	4340)
	(1526	buff	1697)
	(1540	not	1528)
	(1564	not	1552)
	(1606	buff	1697)
	(1621	not	1609)
	(1645	not	1633)
	(1661	and	179	1609	1633)
	(1688	buff	2826)
	(4635	not	4631)
	(4643	not	4639)
	(4651	not	4647)
	(4659	not	4655)
	(4667	not	4663)
	(4675	not	4671)
	(4682	not	4676)
	(4770	not	4764)
	(4778	not	4772)
	(4786	not	4780)
	(4794	not	4788)
	(4802	not	4796)
	(4810	not	4804)
	(2202	buff	1698)
	(2215	not	2203)
	(2238	not	2226)
	(2279	buff	1698)
	(2293	not	2281)
	(2316	not	2304)
	(2332	and	179	2281	2304)
	(2430	not	2418)
	(2454	not	2442)
	(2488	not	2476)
	(2512	not	2500)
	(2536	not	2533)
	(2540	not	2537)
	(2544	not	2541)
	(2548	not	2545)
	(2552	not	2549)
	(2556	not	2553)
	(2560	not	2557)
	(2564	not	2561)
	(2566	and	3553	457	2537)
	(2572	and	3553	468	2545)
	(2578	and	3553	422	2553)
	(2584	and	3553	435	2561)
	(2590	and	3547	2533)
	(2595	and	3547	2541)
	(2600	and	3547	2549)
	(2605	and	3547	2557)
	(2630	not	2627)
	(2634	not	2631)
	(2638	not	2635)
	(2642	not	2639)
	(2646	not	2643)
	(2650	not	2647)
	(2654	not	2651)
	(2658	not	2655)
	(2660	and	3553	389	2631)
	(2666	and	3553	400	2639)
	(2672	and	3553	411	2647)
	(2678	and	3553	374	2655)
	(2684	and	3547	2627)
	(2689	and	3547	2635)
	(2694	and	3547	2643)
	(2699	and	3547	2651)
	(2728	not	2721)
	(2741	not	2734)
	(2748	and	292	2721)
	(2750	and	288	2721)
	(2752	and	280	2721)
	(2754	and	272	2721)
	(2756	and	264	2721)
	(2758	and	241	2734)
	(2760	and	233	2734)
	(2762	and	225	2734)
	(2764	and	217	2734)
	(2766	and	209	2734)
	(2827	buff	1701)
	(2838	not	2828)
	(2847	not	2822)
	(2885	not	2882)
	(2889	not	2886)
	(2893	not	2890)
	(2897	not	2894)
	(2901	not	2898)
	(2905	not	2902)
	(2906	and	2393	2886)
	(2909	and	2393	479	2894)
	(2913	and	2393	490	2902)
	(2918	and	3554	2882)
	(2922	and	3554	2890)
	(2927	and	3554	2898)
	(2951	not	2948)
	(2955	not	2952)
	(2959	not	2956)
	(2963	not	2960)
	(2967	not	2964)
	(2971	not	2968)
	(2973	and	3553	503	2952)
	(2980	not	2979)
	(2982	and	3553	523	2960)
	(2988	and	3553	534	2968)
	(2994	and	3547	2948)
	(3001	and	3547	2956)
	(3006	and	3547	2964)
	(3027	not	3024)
	(3031	not	3028)
	(3035	not	3032)
	(3039	not	3036)
	(3043	not	3040)
	(3047	not	3044)
	(3051	not	3048)
	(3055	not	3052)
	(3056	and	2393	389	3028)
	(3060	and	2393	400	3036)
	(3064	and	2393	411	3044)
	(3068	and	2393	374	3052)
	(3073	and	3554	3024)
	(3078	and	3554	3032)
	(3083	and	3554	3040)
	(3088	and	3554	3048)
	(3099	not	3092)
	(3112	not	3105)
	(3119	and	372	3092)
	(3121	and	366	3092)
	(3123	and	358	3092)
	(3125	and	348	3092)
	(3126	and	338	3092)
	(3128	and	331	3105)
	(3130	and	323	3105)
	(3132	and	315	3105)
	(3134	and	307	3105)
	(3136	and	299	3105)
	(3187	not	3181)
	(3193	and	83	3181)
	(3196	and	86	3181)
	(3199	and	88	3181)
	(3202	and	88	3181)
	(3207	not	3204)
	(3211	not	3208)
	(3215	not	3212)
	(3219	not	3216)
	(3223	not	3220)
	(3227	not	3224)
	(3228	and	2405	503	3208)
	(3232	and	2405	514)
	(3234	and	2405	523	3216)
	(3238	and	2405	534	3224)
	(3243	and	3555	3204)
	(3247	or	3555	514)
	(3249	and	3555	3212)
	(3253	and	3555	3220)
	(3259	not	3256)
	(3263	not	3260)
	(3267	not	3264)
	(3271	not	3268)
	(3275	not	3272)
	(3279	not	3276)
	(3280	and	2405	3260)
	(3283	and	2405	479	3268)
	(3287	and	2405	490	3276)
	(3292	and	3555	3256)
	(3295	and	3555	3264)
	(3299	and	3555	3272)
	(3305	not	3302)
	(3306	buff	2816)
	(3310	buff	2816)
	(3317	not	3314)
	(3318	buff	2816)
	(3322	buff	2816)
	(3326	and	2405	3302)
	(3333	and	2405	3314)
	(3357	not	3354)
	(3361	not	3358)
	(3365	not	3362)
	(3369	not	3366)
	(3373	not	3370)
	(3377	not	3374)
	(3381	not	3378)
	(3385	not	3382)
	(3386	and	2393	457	3358)
	(3390	and	2393	468	3366)
	(3394	and	2393	422	3374)
	(3398	and	2393	435	3382)
	(3403	and	3554	3354)
	(3408	and	3554	3362)
	(3413	and	3554	3370)
	(3418	and	3554	3378)
	(5088	not	5082)
	(5089	not	5085)
	(5096	not	5090)
	(5097	not	5093)
	(3489	buff	3440)
	(3493	buff	3440)
	(3570	not	3558)
	(3594	not	3582)
	(3622	not	3616)
	(3632	not	3628)
	(3637	and	97	3616)
	(3640	and	94	3616)
	(3643	and	97	3616)
	(3646	and	94	3616)
	(3672	not	3660)
	(3696	not	3684)
	(3745	not	3737)
	(3765	not	3757)
	(3803	not	3795)
	(3823	not	3815)
	(5338	not	5332)
	(5339	not	5335)
	(5346	not	5340)
	(5347	not	5343)
	(5354	not	5348)
	(5355	not	5351)
	(3979	not	3972)
	(3998	not	3991)
	(4037	not	4030)
	(4056	not	4049)
	(4094	buff	4110)
	(5104	not	5098)
	(5105	not	5101)
	(5114	not	5108)
	(5115	not	5111)
	(5362	not	5356)
	(5363	not	5359)
	(5366	buff	2816)
	(5373	not	5369)
	(993	buff	1688)
	(978	buff	1688)
	(949	buff	1688)
	(939	buff	1688)
	(2568	and	457	3551	2540)
	(2574	and	468	3551	2548)
	(2580	and	422	3551	2556)
	(2586	and	435	3551	2564)
	(2592	and	3549	2536)
	(2597	and	3549	2544)
	(2602	and	3549	2552)
	(2607	and	3549	2560)
	(2662	and	389	3551	2634)
	(2668	and	400	3551	2642)
	(2674	and	411	3551	2650)
	(2680	and	374	3551	2658)
	(2686	and	3549	2630)
	(2691	and	3549	2638)
	(2696	and	3549	2646)
	(2701	and	3549	2654)
	(2907	and	2370	2889)
	(2910	and	479	2370	2897)
	(2914	and	490	2370	2905)
	(2920	and	3556	2885)
	(2924	and	3556	2893)
	(2929	and	3556	2901)
	(2975	and	503	3551	2955)
	(2984	and	523	3551	2963)
	(2990	and	534	3551	2971)
	(2996	and	3549	2951)
	(3003	and	3549	2959)
	(3008	and	3549	2967)
	(3015	and	2980	2999)
	(3057	and	389	2370	3031)
	(3061	and	400	2370	3039)
	(3065	and	411	2370	3047)
	(3069	and	374	2370	3055)
	(3075	and	3556	3027)
	(3080	and	3556	3035)
	(3085	and	3556	3043)
	(3090	and	3556	3051)
	(3229	and	503	2382	3211)
	(3233	not	3232)
	(3235	and	523	2382	3219)
	(3239	and	534	2382	3227)
	(3244	and	2361	3207)
	(3250	and	2361	3215)
	(3254	and	2361	3223)
	(3281	and	2382	3263)
	(3284	and	479	2382	3271)
	(3288	and	490	2382	3279)
	(3293	and	2361	3259)
	(3296	and	2361	3267)
	(3300	and	2361	3275)
	(3327	and	2382	3305)
	(3334	and	2382	3317)
	(3387	and	457	2370	3361)
	(3391	and	468	2370	3369)
	(3395	and	422	2370	3377)
	(3399	and	435	2370	3385)
	(3405	and	3556	3357)
	(3410	and	3556	3365)
	(3415	and	3556	3373)
	(3420	and	3556	3381)
	(3422	nand	5085	5088)
	(3423	nand	5082	5089)
	(3431	nand	5093	5096)
	(3432	nand	5090	5097)
	(3895	nand	5335	5338)
	(3896	nand	5332	5339)
	(3904	nand	5343	5346)
	(3905	nand	5340	5347)
	(3913	nand	5351	5354)
	(3914	nand	5348	5355)
	(889	buff	4094)
	(5106	nand	5101	5104)
	(5107	nand	5098	5105)
	(5116	nand	5111	5114)
	(5117	nand	5108	5115)
	(5364	nand	5359	5362)
	(5365	nand	5356	5363)
	(593	not	4094)
	(2880	and	2838	2847)
	(2881	and	2828	2847)
	(1579	and	200	1540	1552)
	(1585	and	203	1540	1552)
	(1591	and	197	1540	1552)
	(1597	and	194	1540	1552)
	(1603	and	191	1540	1552)
	(1667	and	182	1621	1633)
	(1673	and	188	1621	1633)
	(1679	and	155	1621	1633)
	(1685	and	149	1621	1633)
	(2876	and	2838	2847)
	(2877	and	2828	2847)
	(2253	and	200	2215	2226)
	(2259	and	203	2215	2226)
	(2265	and	197	2215	2226)
	(2271	and	194	2215	2226)
	(2277	and	191	2215	2226)
	(2338	and	182	2293	2304)
	(2344	and	188	2293	2304)
	(2350	and	155	2293	2304)
	(2356	and	149	2293	2304)
	(2868	and	2838	2847)
	(2869	and	2828	2847)
	(710	and	109	3672	3684)
	(2872	and	2838	2847)
	(2873	and	2828	2847)
	(720	and	11	2430	2442)
	(725	and	109	3570	3582)
	(730	and	46	3570	3582)
	(735	and	100	3570	3582)
	(740	and	91	3570	3582)
	(745	and	43	3570	3582)
	(750	and	76	2430	2442)
	(755	and	73	2430	2442)
	(760	and	67	2430	2442)
	(765	and	14	2430	2442)
	(770	and	46	3672	3684)
	(775	and	100	3672	3684)
	(780	and	91	3672	3684)
	(785	and	43	3672	3684)
	(790	and	76	2488	2500)
	(795	and	73	2488	2500)
	(800	and	67	2488	2500)
	(805	and	14	2488	2500)
	(841	and	120	3803	3815)
	(857	and	11	2488	2500)
	(880	and	118	3745	3757)
	(1660	and	176	1621	1633)
	(2331	and	176	2293	2304)
	(2569	or	2566	2568)
	(2575	or	2572	2574)
	(2581	or	2578	2580)
	(2587	or	2584	2586)
	(2593	or	2590	2592	457)
	(2598	or	2595	2597	468)
	(2603	or	2600	2602	422)
	(2608	or	2605	2607	435)
	(2663	or	2660	2662)
	(2669	or	2666	2668)
	(2675	or	2672	2674)
	(2681	or	2678	2680)
	(2687	or	2684	2686	389)
	(2692	or	2689	2691	400)
	(2697	or	2694	2696	411)
	(2702	or	2699	2701	374)
	(2747	and	289	2728)
	(2749	and	281	2728)
	(2751	and	273	2728)
	(2753	and	265	2728)
	(2755	and	257	2728)
	(2757	and	234	2741)
	(2759	and	226	2741)
	(2761	and	218	2741)
	(2763	and	210	2741)
	(2765	and	206	2741)
	(2857	not	2847)
	(2908	or	2906	2907)
	(2911	or	2909	2910)
	(2915	or	2913	2914)
	(2925	or	2922	2924	479)
	(2930	or	2927	2929	490)
	(2933	or	2918	2920)
	(2976	or	2973	2975)
	(2985	or	2982	2984)
	(2991	or	2988	2990)
	(2997	or	2994	2996	503)
	(3004	or	3001	3003	523)
	(3009	or	3006	3008	534)
	(3058	or	3056	3057)
	(3062	or	3060	3061)
	(3066	or	3064	3065)
	(3070	or	3068	3069)
	(3076	or	3073	3075	389)
	(3081	or	3078	3080	400)
	(3086	or	3083	3085	411)
	(3091	or	3088	3090	374)
	(3118	and	369	3099)
	(3120	and	361	3099)
	(3122	and	351	3099)
	(3124	and	341	3099)
	(3127	and	324	3112)
	(3129	and	316	3112)
	(3131	and	308	3112)
	(3133	and	302	3112)
	(3135	and	293	3112)
	(3147	or	3099	3126)
	(3192	and	83	3187)
	(3195	and	87	3187)
	(3198	and	34	3187)
	(3201	and	34	3187)
	(3230	or	3228	3229)
	(3236	or	3234	3235)
	(3240	or	3238	3239)
	(3245	or	3243	3244	503)
	(3251	or	3249	3250	523)
	(3255	or	3253	3254	534)
	(3282	or	3280	3281)
	(3285	or	3283	3284)
	(3289	or	3287	3288)
	(3297	or	3295	3296	479)
	(3301	or	3299	3300	490)
	(3309	not	3306)
	(3313	not	3310)
	(3321	not	3318)
	(3325	not	3322)
	(3328	or	3326	3327)
	(3329	and	2405	446	3310)
	(3335	or	3333	3334)
	(3336	and	2405	446	3322)
	(3341	and	3555	3306)
	(3345	and	3555	3318)
	(3388	or	3386	3387)
	(3392	or	3390	3391)
	(3396	or	3394	3395)
	(3400	or	3398	3399)
	(3406	or	3403	3405	457)
	(3411	or	3408	3410	468)
	(3416	or	3413	3415	422)
	(3421	or	3418	3420	435)
	(3424	nand	3422	3423)
	(3433	nand	3431	3432)
	(3492	not	3489)
	(3496	not	3493)
	(3780	and	117	3745	3757)
	(3783	and	126	3745	3757)
	(3786	and	127	3745	3757)
	(3789	and	128	3745	3757)
	(3838	and	131	3803	3815)
	(3841	and	129	3803	3815)
	(3844	and	119	3803	3815)
	(3847	and	130	3803	3815)
	(3897	nand	3895	3896)
	(3906	nand	3904	3905)
	(3915	nand	3913	3914)
	(4011	and	122	3979	3991)
	(4014	and	113	3979	3991)
	(4017	and	53	3979	3991)
	(4020	and	114	3979	3991)
	(4023	and	115	3979	3991)
	(4069	and	52	4037	4049)
	(4072	and	112	4037	4049)
	(4075	and	116	4037	4049)
	(4078	and	121	4037	4049)
	(4081	and	123	4037	4049)
	(5206	nand	5116	5117)
	(5209	nand	5106	5107)
	(5307	and	3233	3247)
	(5322	or	3292	3293)
	(5372	not	5366)
	(5375	nand	5366	5373)
	(5399	nand	5364	5365)
	(2813	not	3015)
	(3197	or	3195	3196)
	(3200	or	3198	3199)
	(3203	or	3201	3202)
	(3194	or	3192	3193)
	(2570	not	2569)
	(2576	not	2575)
	(2582	not	2581)
	(2588	not	2587)
	(2664	not	2663)
	(2670	not	2669)
	(2676	not	2675)
	(2682	not	2681)
	(2767	or	2749	2750)
	(2772	or	2751	2752)
	(2776	or	2753	2754)
	(2780	or	2755	2756)
	(2784	or	2757	2758)
	(2788	or	2759	2760)
	(2794	or	2761	2762)
	(2798	or	2763	2764)
	(2802	or	2765	2766)
	(2912	not	2911)
	(2916	not	2915)
	(2936	not	2908)
	(2977	not	2976)
	(2986	not	2985)
	(2992	not	2991)
	(3059	not	3058)
	(3063	not	3062)
	(3067	not	3066)
	(3071	not	3070)
	(3137	or	3120	3121)
	(3139	or	3122	3123)
	(3143	or	3124	3125)
	(3151	or	3127	3128)
	(3155	or	3129	3130)
	(3161	or	3131	3132)
	(3165	or	3133	3134)
	(3167	or	3135	3136)
	(3231	not	3230)
	(3237	not	3236)
	(3241	not	3240)
	(3286	not	3285)
	(3290	not	3289)
	(3330	and	446	2382	3313)
	(3337	and	446	2382	3325)
	(3342	and	2361	3309)
	(3346	and	2361	3321)
	(3348	not	3328)
	(3352	not	3335)
	(3389	not	3388)
	(3393	not	3392)
	(3397	not	3396)
	(3401	not	3400)
	(3845	and	3015	3803	3823)
	(5126	or	3118	3119)
	(5178	or	2747	2748)
	(5325	not	3282)
	(5374	nand	5369	5372)
	(2810	not	2933)
	(635	and	3197	3176)
	(2878	and	24	2838	2857)
	(2879	and	25	2828	2857)
	(2874	and	26	2838	2857)
	(2875	and	81	2828	2857)
	(703	and	3200	3176)
	(2866	and	79	2838	2857)
	(2867	and	23	2828	2857)
	(2870	and	82	2838	2857)
	(2871	and	80	2828	2857)
	(716	and	3203	3176)
	(819	and	3194	3176)
	(1789	and	3147	514)
	(2036	and	514	3147)
	(2611	and	2570	2593)
	(2615	and	2576	2598)
	(2619	and	2582	2603)
	(2623	and	2588	2608)
	(2705	and	2664	2687)
	(2709	and	2670	2692)
	(2713	and	2676	2697)
	(2717	and	2682	2702)
	(2939	and	2912	2925)
	(2942	and	2916	2930)
	(2945	buff	2933)
	(3012	and	2977	2997)
	(3018	and	2986	3004)
	(3021	and	2992	3009)
	(3331	or	3329	3330)
	(3338	or	3336	3337)
	(3343	or	3341	3342	446)
	(3347	or	3345	3346	446)
	(3428	not	3424)
	(3437	not	3433)
	(3514	and	3433	3424	3489)
	(3836	and	3352	3803	3823)
	(3852	and	3071	3091)
	(5311	not	5307)
	(3901	not	3897)
	(3910	not	3906)
	(3934	buff	3915)
	(3938	buff	3915)
	(4652	buff	3147)
	(4783	buff	3147)
	(5137	buff	3147)
	(5212	not	5206)
	(5213	not	5209)
	(5260	and	3063	3081)
	(5263	and	3067	3086)
	(5268	and	3401	3421)
	(5271	and	3059	3076)
	(5276	and	3393	3411)
	(5279	and	3397	3416)
	(5289	and	3389	3406)
	(5296	and	3237	3251)
	(5299	and	3241	3255)
	(5304	and	3231	3245)
	(5312	and	3286	3297)
	(5315	and	3290	3301)
	(5328	not	5322)
	(5396	nand	5374	5375)
	(5403	not	5399)
	(1286	and	446	2802)
	(2809	not	2936)
	(597	not	3348)
	(1031	and	2802	446)
	(636	not	635)
	(637	or	2878	2879	2880	2881)
	(671	or	2874	2875	2876	2877)
	(704	not	703)
	(705	or	2866	2867	2868	2869)
	(713	or	2870	2871	2872	2873)
	(717	not	716)
	(820	not	819)
	(1046	and	2798	457)
	(1064	and	2794	468)
	(1071	and	422	2788)
	(1097	and	2784	435)
	(1111	and	2780	389)
	(1128	and	2776	400)
	(1145	and	2772	411)
	(1160	and	2767	374)
	(1301	and	457	2798)
	(1318	and	468	2794)
	(1324	and	422	2788)
	(1341	and	435	2784)
	(1359	and	389	2780)
	(1382	and	400	2776)
	(1404	and	411	2772)
	(1412	and	374	2767)
	(1704	not	3167)
	(1712	not	3165)
	(1724	buff	3165)
	(1742	and	3161	479)
	(1749	and	490	3155)
	(1775	and	3151	503)
	(1806	and	3143	523)
	(1823	and	3139	534)
	(1829	not	3137)
	(1837	buff	3137)
	(1958	not	3167)
	(1966	not	3165)
	(1978	buff	3165)
	(1995	and	479	3161)
	(2001	and	490	3155)
	(2018	and	503	3151)
	(2059	and	523	3143)
	(2081	and	534	3139)
	(2089	buff	3137)
	(2106	not	3137)
	(3170	buff	3167)
	(3332	not	3331)
	(3339	not	3338)
	(5132	not	5126)
	(5184	not	5178)
	(3853	not	3852)
	(3874	not	3348)
	(4076	and	2936	4037	4056)
	(4116	buff	2802)
	(4124	buff	2798)
	(4132	buff	2794)
	(4140	buff	2788)
	(4148	buff	2784)
	(4156	buff	2780)
	(4164	buff	2776)
	(4172	buff	2772)
	(4180	buff	2767)
	(4228	nor	422	2788)
	(4279	buff	2802)
	(4287	buff	2798)
	(4295	buff	2794)
	(4303	buff	2784)
	(4311	buff	2780)
	(4319	buff	2776)
	(4327	buff	2772)
	(4335	buff	2788)
	(4343	buff	2767)
	(4348	nor	422	2788)
	(4464	nor	374	2767)
	(4628	buff	3161)
	(4636	buff	3155)
	(4644	buff	3151)
	(4660	buff	3143)
	(4668	buff	3139)
	(4716	nor	490	3155)
	(4767	buff	3161)
	(4775	buff	3151)
	(4791	buff	3143)
	(4799	buff	3139)
	(4807	buff	3155)
	(4812	nor	490	3155)
	(5118	buff	3139)
	(5121	buff	3143)
	(5129	buff	3137)
	(5134	buff	3151)
	(5142	buff	3161)
	(5145	buff	3155)
	(5152	buff	3167)
	(5155	buff	3165)
	(5162	buff	2788)
	(5165	buff	2784)
	(5170	buff	2798)
	(5173	buff	2794)
	(5181	buff	2802)
	(5186	buff	2772)
	(5189	buff	2767)
	(5196	buff	2780)
	(5199	buff	2776)
	(5214	nand	5209	5212)
	(5215	nand	5206	5213)
	(5329	not	5325)
	(5330	nand	5325	5328)
	(2807	not	2942)
	(2808	not	2939)
	(2811	not	3021)
	(2812	not	3018)
	(2814	not	3012)
	(2626	not	2623)
	(2622	not	2619)
	(2618	not	2615)
	(2614	not	2611)
	(2720	not	2717)
	(2716	not	2713)
	(2712	not	2709)
	(2708	not	2705)
	(639	and	637	2827)
	(673	and	671	2827)
	(707	and	705	2827)
	(715	and	713	2827)
	(3731	and	2945	3728	3721)
	(4658	not	4652)
	(1777	nand	4652	4659)
	(2019	nand	4783	4786)
	(4787	not	4783)
	(3350	and	3332	3343)
	(3353	and	3339	3347)
	(5141	not	5137)
	(3513	and	3428	3433	3492)
	(3516	and	3424	3437	3496)
	(3517	and	3437	3428	3493)
	(3778	and	2717	3745	3765)
	(3781	and	2713	3745	3765)
	(3784	and	2709	3745	3765)
	(3787	and	2705	3745	3765)
	(3839	and	3021	3803	3823)
	(3842	and	3018	3803	3823)
	(5266	not	5260)
	(5267	not	5263)
	(5274	not	5268)
	(5275	not	5271)
	(5302	not	5296)
	(5303	not	5299)
	(5310	not	5304)
	(3891	nand	5304	5311)
	(3937	not	3934)
	(3941	not	3938)
	(3955	and	3906	3897	3934)
	(3958	and	3910	3901	3938)
	(4009	and	2623	3979	3998)
	(4012	and	2619	3979	3998)
	(4015	and	2615	3979	3998)
	(4018	and	2611	3979	3998)
	(4067	and	3012	4037	4056)
	(4070	and	2942	4037	4056)
	(4073	and	2939	4037	4056)
	(4079	and	2945	4037	4056)
	(5239	nand	5214	5215)
	(5282	not	5276)
	(5283	not	5279)
	(5293	not	5289)
	(5318	not	5312)
	(5319	not	5315)
	(5331	nand	5322	5329)
	(5402	not	5396)
	(5405	nand	5396	5403)
	(595	and	2807	2808	2809	2810)
	(596	and	2811	2812	2813	2814)
	(607	and	2626	2622	2618	2614)
	(608	and	2720	2716	2712	2708)
	(1845	and	1704	1724)
	(1846	and	1712	1704	1742)
	(2115	and	1958	1978)
	(2116	and	1966	1958	1995)
	(4122	not	4116)
	(1022	nand	4116	4123)
	(4130	not	4124)
	(1033	nand	4124	4131)
	(4138	not	4132)
	(1051	nand	4132	4139)
	(4146	not	4140)
	(1079	nand	4140	4147)
	(4154	not	4148)
	(1088	nand	4148	4155)
	(4162	not	4156)
	(1099	nand	4156	4163)
	(4170	not	4164)
	(1115	nand	4164	4171)
	(4178	not	4172)
	(1133	nand	4172	4179)
	(4186	not	4180)
	(1151	nand	4180	4187)
	(4234	not	4228)
	(1276	nand	4279	4282)
	(4283	not	4279)
	(1287	nand	4287	4290)
	(4291	not	4287)
	(1305	nand	4295	4298)
	(4299	not	4295)
	(1330	nand	4303	4306)
	(4307	not	4303)
	(1342	nand	4311	4314)
	(4315	not	4311)
	(1363	nand	4319	4322)
	(4323	not	4319)
	(1388	nand	4327	4330)
	(4331	not	4327)
	(1420	nand	4335	4338)
	(4339	not	4335)
	(1428	nand	4343	4346)
	(4347	not	4343)
	(4634	not	4628)
	(1729	nand	4628	4635)
	(4642	not	4636)
	(1757	nand	4636	4643)
	(4650	not	4644)
	(1766	nand	4644	4651)
	(1776	nand	4655	4658)
	(4666	not	4660)
	(1793	nand	4660	4667)
	(4674	not	4668)
	(1811	nand	4668	4675)
	(1849	and	1712	1742)
	(1852	and	1712	1742)
	(1875	and	54	1829)
	(4722	not	4716)
	(1982	nand	4767	4770)
	(4771	not	4767)
	(2007	nand	4775	4778)
	(4779	not	4775)
	(2020	nand	4780	4787)
	(2040	nand	4791	4794)
	(4795	not	4791)
	(2065	nand	4799	4802)
	(4803	not	4799)
	(2097	nand	4807	4810)
	(4811	not	4807)
	(2119	and	1966	1995)
	(2122	and	1966	1995)
	(5124	not	5118)
	(5125	not	5121)
	(3452	nand	5129	5132)
	(5133	not	5129)
	(5140	not	5134)
	(3462	nand	5134	5141)
	(5168	not	5162)
	(5169	not	5165)
	(5176	not	5170)
	(5177	not	5173)
	(3484	nand	5181	5184)
	(5185	not	5181)
	(3515	nor	3513	3514)
	(3518	nor	3516	3517)
	(3857	not	3853)
	(3860	nand	5263	5266)
	(3861	nand	5260	5267)
	(3869	nand	5271	5274)
	(3870	nand	5268	5275)
	(3878	not	3874)
	(3881	nand	5299	5302)
	(3882	nand	5296	5303)
	(3890	nand	5307	5310)
	(3954	and	3901	3906	3937)
	(3957	and	3897	3910	3941)
	(4021	and	3353	3979	3998)
	(4099	not	3170)
	(4236	buff	1071)
	(4354	not	4348)
	(4406	buff	1324)
	(4470	not	4464)
	(4552	buff	1412)
	(4679	buff	1829)
	(4687	buff	1704)
	(4695	buff	1704)
	(4703	buff	1712)
	(4711	buff	1712)
	(4724	buff	1749)
	(4818	not	4812)
	(4855	buff	1958)
	(4865	buff	1966)
	(4870	buff	2001)
	(4913	buff	1958)
	(4923	buff	1966)
	(4951	buff	2106)
	(5006	buff	2089)
	(5039	buff	2106)
	(5148	not	5142)
	(5149	not	5145)
	(5158	not	5152)
	(5159	not	5155)
	(5192	not	5186)
	(5193	not	5189)
	(5202	not	5196)
	(5203	not	5199)
	(5284	nand	5279	5282)
	(5285	nand	5276	5283)
	(5320	nand	5315	5318)
	(5321	nand	5312	5319)
	(5386	nand	5330	5331)
	(5404	nand	5399	5402)
	(598	and	595	596	597)
	(609	not	3350)
	(1021	nand	4119	4122)
	(1032	nand	4127	4130)
	(1050	nand	4135	4138)
	(1078	nand	4143	4146)
	(1087	nand	4151	4154)
	(1098	nand	4159	4162)
	(1114	nand	4167	4170)
	(1132	nand	4175	4178)
	(1150	nand	4183	4186)
	(1277	nand	4276	4283)
	(1288	nand	4284	4291)
	(1306	nand	4292	4299)
	(1331	nand	4300	4307)
	(1343	nand	4308	4315)
	(1364	nand	4316	4323)
	(1389	nand	4324	4331)
	(1421	nand	4332	4339)
	(1429	nand	4340	4347)
	(1728	nand	4631	4634)
	(1756	nand	4639	4642)
	(1765	nand	4647	4650)
	(1778	nand	1776	1777)
	(1792	nand	4663	4666)
	(1810	nand	4671	4674)
	(1983	nand	4764	4771)
	(2008	nand	4772	4779)
	(2021	nand	2019	2020)
	(2041	nand	4788	4795)
	(2066	nand	4796	4803)
	(2098	nand	4804	4811)
	(3443	nand	5121	5124)
	(3444	nand	5118	5125)
	(3453	nand	5126	5133)
	(3461	nand	5137	5140)
	(3466	nand	5165	5168)
	(3467	nand	5162	5169)
	(3475	nand	5173	5176)
	(3476	nand	5170	5177)
	(3485	nand	5178	5185)
	(5243	not	5239)
	(3862	nand	3860	3861)
	(3871	nand	3869	3870)
	(3883	nand	3881	3882)
	(3892	nand	3890	3891)
	(3956	nor	3954	3955)
	(3959	nor	3957	3958)
	(4756	or	1837	1875)
	(5150	nand	5145	5148)
	(5151	nand	5142	5149)
	(5160	nand	5155	5158)
	(5161	nand	5152	5159)
	(5194	nand	5189	5192)
	(5195	nand	5186	5193)
	(5204	nand	5199	5202)
	(5205	nand	5196	5203)
	(5236	nand	3518	3515)
	(5286	buff	3350)
	(5379	nand	5284	5285)
	(5389	nand	5320	5321)
	(5425	nand	5404	5405)
	(610	and	607	608	609)
	(1023	nand	1021	1022)
	(1034	nand	1032	1033)
	(1052	nand	1050	1051)
	(1080	nand	1078	1079)
	(1089	nand	1087	1088)
	(1100	nand	1098	1099)
	(1116	nand	1114	1115)
	(1134	nand	1132	1133)
	(1152	nand	1150	1151)
	(4242	not	4236)
	(1278	nand	1276	1277)
	(1289	nand	1287	1288)
	(1307	nand	1305	1306)
	(1332	nand	1330	1331)
	(1344	nand	1342	1343)
	(1365	nand	1363	1364)
	(1390	nand	1388	1389)
	(1422	nand	1420	1421)
	(1430	nand	1428	1429)
	(1730	nand	1728	1729)
	(1758	nand	1756	1757)
	(1767	nand	1765	1766)
	(1794	nand	1792	1793)
	(1812	nand	1810	1811)
	(1876	nand	4679	4682)
	(4683	not	4679)
	(4691	not	4687)
	(4699	not	4695)
	(4707	not	4703)
	(4715	not	4711)
	(4730	not	4724)
	(1984	nand	1982	1983)
	(2009	nand	2007	2008)
	(2042	nand	2040	2041)
	(2067	nand	2065	2066)
	(2099	nand	2097	2098)
	(4869	not	4865)
	(4927	not	4923)
	(3445	nand	3443	3444)
	(3454	nand	3452	3453)
	(3463	nand	3461	3462)
	(3468	nand	3466	3467)
	(3477	nand	3475	3476)
	(3486	nand	3484	3485)
	(4103	and	4099	3170)
	(4412	not	4406)
	(4558	not	4552)
	(4859	not	4855)
	(4876	not	4870)
	(4917	not	4913)
	(4955	not	4951)
	(5012	not	5006)
	(5043	not	5039)
	(5216	nand	5160	5161)
	(5219	nand	5150	5151)
	(5226	nand	5204	5205)
	(5229	nand	5194	5195)
	(5392	not	5386)
	(5422	nand	3959	3956)
	(1866	and	1778	1806)
	(1877	nand	4676	4683)
	(4762	not	4756)
	(2142	and	2021	2059)
	(2146	and	2021	2059)
	(5242	not	5236)
	(3532	nand	5236	5243)
	(3866	not	3862)
	(3887	not	3883)
	(3918	buff	3871)
	(3922	buff	3871)
	(3926	buff	3892)
	(3930	buff	3892)
	(5429	not	5425)
	(4104	or	4099	4103)
	(4743	buff	1778)
	(4991	buff	2021)
	(5001	buff	2021)
	(5292	not	5286)
	(5295	nand	5286	5293)
	(5383	not	5379)
	(5393	not	5389)
	(5394	nand	5389	5392)
	(1439	and	1278	1301)
	(1440	and	1289	1278	1318)
	(1441	and	1307	1278	1324	1289)
	(1847	and	1730	1704	1749	1712)
	(1168	and	1023	1046)
	(1169	and	1034	1023	1064)
	(1170	and	1052	1023	1071	1034)
	(2117	and	1984	1958	2001	1966)
	(1086	not	1080)
	(1166	and	1034	1080	1052	1023)
	(1171	and	1034	1064)
	(1172	and	1052	1071	1034)
	(1173	and	1080	1052	1034)
	(1174	and	1034	1064)
	(1175	and	1071	1052	1034)
	(1176	and	1052	1071)
	(1177	and	1080	1052)
	(1178	and	1052	1071)
	(1179	and	1100	1152	1116	1089	1134)
	(1181	and	1089	1111)
	(1182	and	1100	1089	1128)
	(1183	and	1116	1089	1145	1100)
	(1184	and	1134	1116	1089	1160	1100)
	(1188	and	1100	1128)
	(1189	and	1116	1145	1100)
	(1190	and	1134	1116	1160	1100)
	(1191	and	4	1152	1116	1134	1100)
	(1192	and	1145	1116)
	(1193	and	1134	1116	1160)
	(1194	and	4	1152	1116	1134)
	(1195	and	1134	1160)
	(1196	and	4	1152	1134)
	(1197	and	4	1152)
	(1437	and	1422	1307	1289	1278)
	(1442	and	1289	1318)
	(1443	and	1307	1324	1289)
	(1444	and	1422	1307	1289)
	(1445	and	1289	1318)
	(1446	and	1307	1324	1289)
	(1447	and	1307	1324)
	(1451	and	1430	1390	1365	1344	1332)
	(1454	and	1332	1359)
	(1455	and	1344	1332	1382)
	(1456	and	1365	1332	1404	1344)
	(1457	and	1390	1365	1332	1412	1344)
	(1465	and	1344	1382)
	(1466	and	1365	1404	1344)
	(1467	and	1390	1365	1412	1344)
	(1468	and	1430	1365	1344	1390)
	(1469	and	1344	1382)
	(1470	and	1365	1404	1344)
	(1471	and	1390	1365	1412	1344)
	(1472	and	1365	1404)
	(1473	and	1390	1365	1412)
	(1474	and	1430	1365	1390)
	(1475	and	1365	1404)
	(1476	and	1390	1365	1412)
	(1477	and	1390	1412)
	(1481	and	1422	1307)
	(1482	and	1430	1390)
	(1764	not	1758)
	(1843	and	1712	1758	1730	1704)
	(1850	and	1730	1749	1712)
	(1851	and	1758	1730	1712)
	(1853	and	1749	1730	1712)
	(1854	and	1730	1749)
	(1855	and	1758	1730)
	(1856	and	1730	1749)
	(1857	and	1778	1829	1794	1767	1812)
	(1859	and	1767	1789)
	(1860	and	1778	1767	1806)
	(1861	and	1794	1767	1823	1778)
	(1862	and	1812	1794	1767	1837	1778)
	(1867	and	1794	1823	1778)
	(1868	and	1812	1794	1837	1778)
	(1869	and	54	1829	1794	1812	1778)
	(1870	and	1823	1794)
	(1871	and	1812	1794	1837)
	(1872	and	54	1829	1794	1812)
	(1873	and	1812	1837)
	(1874	and	54	1829	1812)
	(1878	nand	1876	1877)
	(2113	and	2099	1984	1966	1958)
	(2120	and	1984	2001	1966)
	(2121	and	2099	1984	1966)
	(2123	and	1984	2001	1966)
	(2124	and	1984	2001)
	(2128	and	2106	2067	2042	2021	2009)
	(2131	and	2009	2036)
	(2132	and	2021	2009	2059)
	(2133	and	2042	2009	2081	2021)
	(2134	and	2067	2042	2009	2089	2021)
	(2143	and	2042	2081	2021)
	(2144	and	2067	2042	2089	2021)
	(2145	and	2106	2042	2021	2067)
	(2147	and	2042	2081	2021)
	(2148	and	2067	2042	2089	2021)
	(2149	and	2042	2081)
	(2150	and	2067	2042	2089)
	(2151	and	2106	2042	2067)
	(2152	and	2042	2081)
	(2153	and	2067	2042	2089)
	(2154	and	2067	2089)
	(2158	and	2099	1984)
	(2159	and	2106	2067)
	(3449	not	3445)
	(3458	not	3454)
	(3472	not	3468)
	(3481	not	3477)
	(3497	buff	3463)
	(3501	buff	3463)
	(3505	buff	3486)
	(3509	buff	3486)
	(3531	nand	5239	5242)
	(5428	not	5422)
	(3967	nand	5422	5429)
	(4191	buff	1152)
	(4199	buff	1023)
	(4207	buff	1023)
	(4215	buff	1034)
	(4223	buff	1034)
	(4231	buff	1052)
	(4239	buff	1052)
	(4247	buff	1089)
	(4255	buff	1100)
	(4263	buff	1116)
	(4271	buff	1134)
	(4371	buff	1422)
	(4381	buff	1307)
	(4391	buff	1278)
	(4401	buff	1289)
	(4429	buff	1422)
	(4439	buff	1307)
	(4449	buff	1278)
	(4459	buff	1289)
	(4497	buff	1430)
	(4507	buff	1390)
	(4517	buff	1332)
	(4527	buff	1365)
	(4537	buff	1344)
	(4547	buff	1344)
	(4585	buff	1430)
	(4595	buff	1390)
	(4605	buff	1332)
	(4615	buff	1365)
	(4719	buff	1730)
	(4727	buff	1730)
	(4735	buff	1767)
	(4751	buff	1794)
	(4759	buff	1812)
	(4835	buff	2099)
	(4845	buff	1984)
	(4893	buff	2099)
	(4903	buff	1984)
	(4961	buff	2067)
	(4971	buff	2009)
	(4981	buff	2042)
	(5049	buff	2067)
	(5059	buff	2009)
	(5069	buff	2042)
	(5222	not	5216)
	(5223	not	5219)
	(5232	not	5226)
	(5233	not	5229)
	(5294	nand	5289	5292)
	(5395	nand	5386	5393)
	(589	or	1286	1439	1440	1441)
	(616	or	3167	1845	1846	1847)
	(619	or	1031	1168	1169	1170)
	(627	or	3167	2115	2116	2117)
	(1185	or	1097	1181	1182	1183	1184)
	(1448	or	1318	1447)
	(1458	or	1341	1454	1455	1456	1457)
	(1478	or	1404	1477)
	(1863	or	1775	1859	1860	1861	1862)
	(4747	not	4743)
	(2125	or	1995	2124)
	(2135	or	2018	2131	2132	2133	2134)
	(2155	or	2081	2154)
	(4995	not	4991)
	(5005	not	5001)
	(3533	nand	3531	3532)
	(3921	not	3918)
	(3925	not	3922)
	(3929	not	3926)
	(3933	not	3930)
	(3943	and	3862	3853	3918)
	(3946	and	3866	3857	3922)
	(3949	and	3883	3874	3926)
	(3952	and	3887	3878	3930)
	(3966	nand	5425	5428)
	(4107	nand	4104	132)
	(4196	or	1046	1171	1172	1173)
	(4204	nor	1046	1174	1175)
	(4212	or	1064	1176	1177)
	(4220	nor	1064	1178)
	(4244	or	1111	1188	1189	1190	1191)
	(4252	or	1128	1192	1193	1194)
	(4260	or	1145	1195	1196)
	(4268	or	1160	1197)
	(4361	or	1301	1442	1443	1444)
	(4419	nor	1301	1445	1446)
	(4467	or	1382	1472	1473	1474)
	(4487	or	1359	1465	1466	1467	1468)
	(4555	nor	1382	1475	1476)
	(4575	nor	1359	1469	1470	1471)
	(4684	or	1724	1849	1850	1851)
	(4692	nor	1724	1852	1853)
	(4700	or	1742	1854	1855)
	(4708	nor	1742	1856)
	(4732	or	1789	1866	1867	1868	1869)
	(4740	or	1806	1870	1871	1872)
	(4748	or	1823	1873	1874)
	(4825	or	1978	2119	2120	2121)
	(4883	nor	1978	2122	2123)
	(4928	or	2059	2149	2150	2151)
	(4941	or	2036	2142	2143	2144	2145)
	(5009	nor	2059	2152	2153)
	(5029	nor	2036	2146	2147	2148)
	(5224	nand	5219	5222)
	(5225	nand	5216	5223)
	(5234	nand	5229	5232)
	(5235	nand	5226	5233)
	(5376	nand	5294	5295)
	(5417	nand	5394	5395)
	(576	not	1878)
	(588	and	1437	1451)
	(615	and	1843	1857)
	(626	and	2113	2128)
	(632	and	1166	1179)
	(1198	nand	4191	4194)
	(4195	not	4191)
	(4203	not	4199)
	(4211	not	4207)
	(4219	not	4215)
	(4227	not	4223)
	(1217	nand	4231	4234)
	(4235	not	4231)
	(1221	nand	4239	4242)
	(4243	not	4239)
	(1224	and	1179	4)
	(4251	not	4247)
	(4259	not	4255)
	(4267	not	4263)
	(4275	not	4271)
	(1453	not	1451)
	(4405	not	4401)
	(4463	not	4459)
	(4541	not	4537)
	(4551	not	4547)
	(1895	nand	4719	4722)
	(4723	not	4719)
	(1899	nand	4727	4730)
	(4731	not	4727)
	(1902	and	1857	54)
	(4739	not	4735)
	(4755	not	4751)
	(1929	nand	4759	4762)
	(4763	not	4759)
	(2130	not	2128)
	(3500	not	3497)
	(3504	not	3501)
	(3508	not	3505)
	(3512	not	3509)
	(3520	and	3454	3445	3497)
	(3523	and	3458	3449	3501)
	(3526	and	3477	3468	3505)
	(3529	and	3481	3472	3509)
	(1002	buff	3533)
	(3837	and	1878	3795	3823)
	(3942	and	3857	3862	3921)
	(3945	and	3853	3866	3925)
	(3948	and	3878	3883	3929)
	(3951	and	3874	3887	3933)
	(3968	nand	3966	3967)
	(4375	not	4371)
	(4385	not	4381)
	(4395	not	4391)
	(4433	not	4429)
	(4443	not	4439)
	(4453	not	4449)
	(4501	not	4497)
	(4511	not	4507)
	(4521	not	4517)
	(4531	not	4527)
	(4619	not	4615)
	(4589	not	4585)
	(4599	not	4595)
	(4609	not	4605)
	(4839	not	4835)
	(4849	not	4845)
	(4897	not	4893)
	(4907	not	4903)
	(4965	not	4961)
	(4975	not	4971)
	(4985	not	4981)
	(5073	not	5069)
	(5053	not	5049)
	(5063	not	5059)
	(5247	nand	5224	5225)
	(5255	nand	5234	5235)
	(590	and	1437	1458)
	(617	and	1863	1843)
	(620	and	1185	1166)
	(628	and	2113	2135)
	(3535	not	3533)
	(1199	nand	4188	4195)
	(4202	not	4196)
	(1204	nand	4196	4203)
	(4210	not	4204)
	(1207	nand	4204	4211)
	(4218	not	4212)
	(1211	nand	4212	4219)
	(4226	not	4220)
	(1214	nand	4220	4227)
	(1218	nand	4228	4235)
	(1222	nand	4236	4243)
	(1225	or	1185	1224)
	(4250	not	4244)
	(1237	nand	4244	4251)
	(4258	not	4252)
	(1242	nand	4252	4259)
	(4266	not	4260)
	(1247	nand	4260	4267)
	(4274	not	4268)
	(1252	nand	4268	4275)
	(1462	not	1458)
	(4690	not	4684)
	(1882	nand	4684	4691)
	(4698	not	4692)
	(1885	nand	4692	4699)
	(4706	not	4700)
	(1889	nand	4700	4707)
	(4714	not	4708)
	(1892	nand	4708	4715)
	(1896	nand	4716	4723)
	(1900	nand	4724	4731)
	(1903	or	1863	1902)
	(4738	not	4732)
	(1915	nand	4732	4739)
	(4746	not	4740)
	(1920	nand	4740	4747)
	(4754	not	4748)
	(1925	nand	4748	4755)
	(1930	nand	4756	4763)
	(2139	not	2135)
	(3519	and	3449	3454	3500)
	(3522	and	3445	3458	3504)
	(3525	and	3472	3477	3508)
	(3528	and	3468	3481	3512)
	(3848	or	3836	3837	3838)
	(3944	nor	3942	3943)
	(3947	nor	3945	3946)
	(3950	nor	3948	3949)
	(3953	nor	3951	3952)
	(5421	not	5417)
	(1004	buff	3968)
	(4111	and	4104	4107)
	(4112	and	4107	132)
	(4351	or	1448	1481)
	(4365	not	4361)
	(4409	not	1448)
	(4423	not	4419)
	(4471	not	4467)
	(4472	nand	4467	4470)
	(4477	or	1478	1482)
	(4491	not	4487)
	(4559	not	4555)
	(4560	nand	4555	4558)
	(4565	not	1478)
	(4579	not	4575)
	(4815	or	2125	2158)
	(4829	not	4825)
	(4873	not	2125)
	(4887	not	4883)
	(4931	or	2155	2159)
	(4934	not	4928)
	(4945	not	4941)
	(5013	not	5009)
	(5014	nand	5009	5012)
	(5019	not	2155)
	(5033	not	5029)
	(5382	not	5376)
	(5385	nand	5376	5383)
	(591	or	589	590)
	(618	or	616	617)
	(621	or	619	620)
	(629	or	627	628)
	(3970	not	3968)
	(1200	nand	1198	1199)
	(1203	nand	4199	4202)
	(1206	nand	4207	4210)
	(1210	nand	4215	4218)
	(1213	nand	4223	4226)
	(1219	nand	1217	1218)
	(1223	nand	1221	1222)
	(1236	nand	4247	4250)
	(1241	nand	4255	4258)
	(1246	nand	4263	4266)
	(1251	nand	4271	4274)
	(1881	nand	4687	4690)
	(1884	nand	4695	4698)
	(1888	nand	4703	4706)
	(1891	nand	4711	4714)
	(1897	nand	1895	1896)
	(1901	nand	1899	1900)
	(1914	nand	4735	4738)
	(1919	nand	4743	4746)
	(1924	nand	4751	4754)
	(1931	nand	1929	1930)
	(3521	nor	3519	3520)
	(3524	nor	3522	3523)
	(3527	nor	3525	3526)
	(3530	nor	3528	3529)
	(5251	not	5247)
	(5259	not	5255)
	(4113	or	4111	4112)
	(4473	nand	4464	4471)
	(4561	nand	4552	4559)
	(5015	nand	5006	5013)
	(5384	nand	5379	5382)
	(5406	nand	3947	3944)
	(5414	nand	3953	3950)
	(1664	and	3848	1621	1645)
	(2335	and	3848	2293	2316)
	(718	and	3848	2430	2454)
	(822	not	3848)
	(855	and	3848	2488	2512)
	(1205	nand	1203	1204)
	(1208	nand	1206	1207)
	(1212	nand	1210	1211)
	(1215	nand	1213	1214)
	(1220	not	1219)
	(1231	not	1225)
	(1238	nand	1236	1237)
	(1243	nand	1241	1242)
	(1248	nand	1246	1247)
	(1253	nand	1251	1252)
	(1272	and	1225	1086)
	(1483	and	1462	1453)
	(1883	nand	1881	1882)
	(1886	nand	1884	1885)
	(1890	nand	1888	1889)
	(1893	nand	1891	1892)
	(1898	not	1897)
	(1909	not	1903)
	(1916	nand	1914	1915)
	(1921	nand	1919	1920)
	(1926	nand	1924	1925)
	(1953	and	1903	1764)
	(2160	and	2139	2130)
	(4355	not	4351)
	(4356	nand	4351	4354)
	(4413	not	4409)
	(4414	nand	4409	4412)
	(4474	nand	4472	4473)
	(4481	not	4477)
	(4562	nand	4560	4561)
	(4569	not	4565)
	(4819	not	4815)
	(4820	nand	4815	4818)
	(4877	not	4873)
	(4878	nand	4873	4876)
	(4935	not	4931)
	(4936	nand	4931	4934)
	(5016	nand	5014	5015)
	(5023	not	5019)
	(5244	nand	3524	3521)
	(5252	nand	3530	3527)
	(5409	nand	5384	5385)
	(566	not	1200)
	(577	not	1931)
	(3733	and	4113	3724	3721)
	(1209	not	1208)
	(1216	not	1215)
	(1257	and	1225	1205)
	(1262	and	1225	1212)
	(1267	and	1225	1220)
	(1887	not	1886)
	(1894	not	1893)
	(1935	and	1903	1883)
	(1943	and	1903	1890)
	(1948	and	1903	1898)
	(3779	and	1200	3737	3765)
	(3840	and	1931	3795	3823)
	(5412	not	5406)
	(5420	not	5414)
	(3964	nand	5414	5421)
	(4357	nand	4348	4355)
	(4415	nand	4406	4413)
	(4821	nand	4812	4819)
	(4879	nand	4870	4877)
	(4937	nand	4928	4935)
	(567	not	1253)
	(568	not	1248)
	(569	not	1243)
	(570	not	1238)
	(578	not	1926)
	(579	not	1921)
	(580	not	1916)
	(1256	and	1209	1231)
	(1261	and	1216	1231)
	(1266	and	1223	1231)
	(1271	and	1080	1231)
	(1486	not	1483)
	(1934	and	1887	1909)
	(1942	and	1894	1909)
	(1947	and	1901	1909)
	(1952	and	1758	1909)
	(2163	not	2160)
	(5250	not	5244)
	(3537	nand	5244	5251)
	(5258	not	5252)
	(3542	nand	5252	5259)
	(3782	and	1253	3737	3765)
	(3785	and	1248	3737	3765)
	(3788	and	1243	3737	3765)
	(3790	or	3778	3779	3780)
	(3843	and	1926	3795	3823)
	(3846	and	1921	3795	3823)
	(3849	or	3839	3840	3841)
	(3960	nand	5409	5412)
	(5413	not	5409)
	(3963	nand	5417	5420)
	(4010	and	1238	3972	3998)
	(4068	and	1916	4030	4056)
	(4358	nand	4356	4357)
	(4416	nand	4414	4415)
	(4480	not	4474)
	(4483	nand	4474	4481)
	(4568	not	4562)
	(4571	nand	4562	4569)
	(4822	nand	4820	4821)
	(4880	nand	4878	4879)
	(4938	nand	4936	4937)
	(5022	not	5016)
	(5025	nand	5016	5023)
	(1258	or	1256	1257)
	(1263	or	1261	1262)
	(1268	or	1266	1267)
	(1273	or	1271	1272)
	(1936	or	1934	1935)
	(1944	or	1942	1943)
	(1949	or	1947	1948)
	(1954	or	1952	1953)
	(3536	nand	5247	5250)
	(3541	nand	5255	5258)
	(3791	or	3781	3782	3783)
	(3792	or	3784	3785	3786)
	(3793	or	3787	3788	3789)
	(3850	or	3842	3843	3844)
	(3851	or	3845	3846	3847)
	(3961	nand	5406	5413)
	(3965	nand	3963	3964)
	(4024	or	4009	4010	4011)
	(4082	or	4067	4068	4069)
	(4482	nand	4477	4480)
	(4570	nand	4565	4568)
	(5024	nand	5019	5022)
	(1666	and	3790	1609	1645)
	(1670	and	3849	1621	1645)
	(2337	and	3790	2281	2316)
	(2341	and	3849	2293	2316)
	(719	and	3790	2418	2454)
	(758	and	3849	2430	2454)
	(798	and	3849	2488	2512)
	(838	not	3849)
	(856	and	3790	2476	2512)
	(861	not	3790)
	(3538	nand	3536	3537)
	(3543	nand	3541	3542)
	(3962	nand	3960	3961)
	(4364	not	4358)
	(4367	nand	4358	4365)
	(4422	not	4416)
	(4425	nand	4416	4423)
	(4484	nand	4482	4483)
	(4572	nand	4570	4571)
	(4828	not	4822)
	(4831	nand	4822	4829)
	(4886	not	4880)
	(4889	nand	4880	4887)
	(4944	not	4938)
	(4947	nand	4938	4945)
	(5026	nand	5024	5025)
	(571	not	1273)
	(572	not	1268)
	(573	not	1263)
	(574	not	1258)
	(581	not	1954)
	(582	not	1949)
	(583	not	1944)
	(584	not	1936)
	(623	not	1936)
	(1576	and	4082	1540	1564)
	(1578	and	4024	1528	1564)
	(659	or	1664	1666	1667	1668)
	(1672	and	3791	1609	1645)
	(1676	and	3850	1621	1645)
	(1678	and	3792	1609	1645)
	(1682	and	3851	1621	1645)
	(1684	and	3793	1609	1645)
	(2250	and	4082	2215	2238)
	(2252	and	4024	2203	2238)
	(691	or	2335	2337	2338	2339)
	(2343	and	3791	2281	2316)
	(2347	and	3850	2293	2316)
	(2349	and	3792	2281	2316)
	(2353	and	3851	2293	2316)
	(2355	and	3793	2281	2316)
	(722	or	718	719	720	721)
	(743	and	4082	3570	3594)
	(744	and	4024	3558	3594)
	(748	and	3851	2430	2454)
	(749	and	3793	2418	2454)
	(753	and	3850	2430	2454)
	(754	and	3792	2418	2454)
	(759	and	3791	2418	2454)
	(783	and	4082	3672	3696)
	(784	and	4024	3660	3696)
	(788	and	3851	2488	2512)
	(789	and	3793	2476	2512)
	(793	and	3850	2488	2512)
	(794	and	3792	2476	2512)
	(799	and	3791	2476	2512)
	(3735	and	1936	3724	3717)
	(832	not	4082)
	(834	not	3851)
	(836	not	3850)
	(3835	not	3965)
	(859	or	855	856	857	858)
	(871	not	4024)
	(873	not	3793)
	(875	not	3792)
	(877	not	3791)
	(998	buff	3538)
	(1000	buff	3543)
	(3651	and	3965	3632)
	(4013	and	1273	3972	3998)
	(4016	and	1268	3972	3998)
	(4019	and	1263	3972	3998)
	(4022	and	1258	3972	3998)
	(4071	and	1954	4030	4056)
	(4074	and	1949	4030	4056)
	(4077	and	1944	4030	4056)
	(4080	and	1936	4030	4056)
	(4096	nand	4113	1936)
	(4366	nand	4361	4364)
	(4424	nand	4419	4422)
	(4830	nand	4825	4828)
	(4888	nand	4883	4886)
	(4946	nand	4941	4944)
	(575	and	566	567	568	569	570	571	572	573	574)
	(585	and	576	577	578	579	580	581	582	583	584)
	(640	or	1576	1578	1579	1580)
	(661	and	659	1606)
	(662	or	1670	1672	1673	1674)
	(665	or	1676	1678	1679	1680)
	(668	or	1682	1684	1685	1686)
	(674	or	2250	2252	2253	2254)
	(693	and	691	2279)
	(694	or	2341	2343	2344	2345)
	(697	or	2347	2349	2350	2351)
	(700	or	2353	2355	2356	2357)
	(747	or	743	744	745	746)
	(752	or	748	749	750	751)
	(757	or	753	754	755	756)
	(762	or	758	759	760	761)
	(787	or	783	784	785	786)
	(792	or	788	789	790	791)
	(797	or	793	794	795	796)
	(802	or	798	799	800	801)
	(817	or	3731	3733	3734	3735)
	(839	and	3835	3803	3823)
	(3540	not	3538)
	(3545	not	3543)
	(3777	not	3962)
	(3648	and	3962	3632)
	(4025	or	4012	4013	4014)
	(4026	or	4015	4016	4017)
	(4027	or	4018	4019	4020)
	(4028	or	4021	4022	4023)
	(4083	or	4070	4071	4072)
	(4084	or	4073	4074	4075)
	(4085	or	4076	4077	4078)
	(4086	or	4079	4080	4081)
	(4368	nand	4366	4367)
	(4426	nand	4424	4425)
	(4490	not	4484)
	(4493	nand	4484	4491)
	(4578	not	4572)
	(4581	nand	4572	4579)
	(4832	nand	4830	4831)
	(4890	nand	4888	4889)
	(4948	nand	4946	4947)
	(5032	not	5026)
	(5035	nand	5026	5033)
	(642	and	640	1526)
	(664	and	662	1606)
	(667	and	665	1606)
	(670	and	668	1606)
	(676	and	674	2202)
	(696	and	694	2279)
	(699	and	697	2279)
	(702	and	700	2279)
	(811	and	4113	4096)
	(812	and	4096	1936)
	(818	and	816	817)
	(853	and	562	3540	3545	3535	3970)
	(878	and	3777	3745	3765)
	(4492	nand	4487	4490)
	(4580	nand	4575	4578)
	(5034	nand	5029	5032)
	(1582	and	4083	1540	1564)
	(1584	and	4025	1528	1564)
	(1588	and	4084	1540	1564)
	(1590	and	4026	1528	1564)
	(1594	and	4085	1540	1564)
	(1596	and	4027	1528	1564)
	(1600	and	4086	1540	1564)
	(1602	and	4028	1528	1564)
	(2256	and	4083	2215	2238)
	(2258	and	4025	2203	2238)
	(2262	and	4084	2215	2238)
	(2264	and	4026	2203	2238)
	(2268	and	4085	2215	2238)
	(2270	and	4027	2203	2238)
	(2274	and	4086	2215	2238)
	(2276	and	4028	2203	2238)
	(708	and	4086	3672	3696)
	(709	and	4028	3660	3696)
	(723	and	4086	3570	3594)
	(724	and	4028	3558	3594)
	(728	and	4085	3570	3594)
	(729	and	4027	3558	3594)
	(733	and	4084	3570	3594)
	(734	and	4026	3558	3594)
	(738	and	4083	3570	3594)
	(739	and	4025	3558	3594)
	(768	and	4085	3672	3696)
	(769	and	4027	3660	3696)
	(773	and	4084	3672	3696)
	(774	and	4026	3660	3696)
	(778	and	4083	3672	3696)
	(779	and	4025	3660	3696)
	(813	or	811	812)
	(824	not	4086)
	(826	not	4085)
	(828	not	4084)
	(830	not	4083)
	(854	and	852	853	245)
	(863	not	4028)
	(865	not	4027)
	(867	not	4026)
	(869	not	4025)
	(4374	not	4368)
	(4377	nand	4368	4375)
	(4432	not	4426)
	(4435	nand	4426	4433)
	(4494	nand	4492	4493)
	(4582	nand	4580	4581)
	(4838	not	4832)
	(4841	nand	4832	4839)
	(4896	not	4890)
	(4899	nand	4890	4897)
	(4954	not	4948)
	(4957	nand	4948	4955)
	(5036	nand	5034	5035)
	(643	or	1582	1584	1585	1586)
	(646	or	1588	1590	1591	1592)
	(649	or	1594	1596	1597	1598)
	(652	or	1600	1602	1603	1604)
	(677	or	2256	2258	2259	2260)
	(680	or	2262	2264	2265	2266)
	(683	or	2268	2270	2271	2272)
	(686	or	2274	2276	2277	2278)
	(712	or	708	709	710	711)
	(727	or	723	724	725	726)
	(732	or	728	729	730	731)
	(737	or	733	734	735	736)
	(742	or	738	739	740	741)
	(772	or	768	769	770	771)
	(777	or	773	774	775	776)
	(782	or	778	779	780	781)
	(4376	nand	4371	4374)
	(4434	nand	4429	4432)
	(4840	nand	4835	4838)
	(4898	nand	4893	4896)
	(4956	nand	4951	4954)
	(645	and	643	1526)
	(648	and	646	1526)
	(651	and	649	1526)
	(654	and	652	1526)
	(679	and	677	2202)
	(682	and	680	2202)
	(685	and	683	2202)
	(688	and	686	2202)
	(4378	nand	4376	4377)
	(4436	nand	4434	4435)
	(4500	not	4494)
	(4503	nand	4494	4501)
	(4588	not	4582)
	(4591	nand	4582	4589)
	(4842	nand	4840	4841)
	(4900	nand	4898	4899)
	(4958	nand	4956	4957)
	(5042	not	5036)
	(5045	nand	5036	5043)
	(4502	nand	4497	4500)
	(4590	nand	4585	4588)
	(5044	nand	5039	5042)
	(4384	not	4378)
	(4387	nand	4378	4385)
	(4442	not	4436)
	(4445	nand	4436	4443)
	(4504	nand	4502	4503)
	(4592	nand	4590	4591)
	(4848	not	4842)
	(4851	nand	4842	4849)
	(4906	not	4900)
	(4909	nand	4900	4907)
	(4964	not	4958)
	(4967	nand	4958	4965)
	(5046	nand	5044	5045)
	(4386	nand	4381	4384)
	(4444	nand	4439	4442)
	(4850	nand	4845	4848)
	(4908	nand	4903	4906)
	(4966	nand	4961	4964)
	(4388	nand	4386	4387)
	(4446	nand	4444	4445)
	(4510	not	4504)
	(4513	nand	4504	4511)
	(4598	not	4592)
	(4601	nand	4592	4599)
	(4852	nand	4850	4851)
	(4910	nand	4908	4909)
	(4968	nand	4966	4967)
	(5052	not	5046)
	(5055	nand	5046	5053)
	(4512	nand	4507	4510)
	(4600	nand	4595	4598)
	(5054	nand	5049	5052)
	(4394	not	4388)
	(4397	nand	4388	4395)
	(4452	not	4446)
	(4455	nand	4446	4453)
	(4514	nand	4512	4513)
	(4602	nand	4600	4601)
	(4858	not	4852)
	(4861	nand	4852	4859)
	(4916	not	4910)
	(4919	nand	4910	4917)
	(4974	not	4968)
	(4977	nand	4968	4975)
	(5056	nand	5054	5055)
	(4396	nand	4391	4394)
	(4454	nand	4449	4452)
	(4860	nand	4855	4858)
	(4918	nand	4913	4916)
	(4976	nand	4971	4974)
	(4398	nand	4396	4397)
	(4456	nand	4454	4455)
	(4520	not	4514)
	(4523	nand	4514	4521)
	(4608	not	4602)
	(4611	nand	4602	4609)
	(4862	nand	4860	4861)
	(4920	nand	4918	4919)
	(4978	nand	4976	4977)
	(5062	not	5056)
	(5065	nand	5056	5063)
	(4522	nand	4517	4520)
	(4610	nand	4605	4608)
	(5064	nand	5059	5062)
	(4404	not	4398)
	(1488	nand	4398	4405)
	(4462	not	4456)
	(1493	nand	4456	4463)
	(4868	not	4862)
	(2165	nand	4862	4869)
	(4926	not	4920)
	(2170	nand	4920	4927)
	(4524	nand	4522	4523)
	(4612	nand	4610	4611)
	(4984	not	4978)
	(4987	nand	4978	4985)
	(5066	nand	5064	5065)
	(1487	nand	4401	4404)
	(1492	nand	4459	4462)
	(2164	nand	4865	4868)
	(2169	nand	4923	4926)
	(4986	nand	4981	4984)
	(1489	nand	1487	1488)
	(1494	nand	1492	1493)
	(2166	nand	2164	2165)
	(2171	nand	2169	2170)
	(4530	not	4524)
	(4533	nand	4524	4531)
	(4618	not	4612)
	(4543	nand	4612	4619)
	(4988	nand	4986	4987)
	(5072	not	5066)
	(4997	nand	5066	5073)
	(4532	nand	4527	4530)
	(4542	nand	4615	4618)
	(4996	nand	5069	5072)
	(1513	and	1494	1462	1502)
	(1514	and	1489	1458	1502)
	(1515	and	1494	1483	1497)
	(1516	and	1489	1486	1497)
	(4994	not	4988)
	(2184	nand	4988	4995)
	(2190	and	2171	2139	2179)
	(2191	and	2166	2135	2179)
	(2192	and	2171	2160	2174)
	(2193	and	2166	2163	2174)
	(4534	nand	4532	4533)
	(4544	nand	4542	4543)
	(4998	nand	4996	4997)
	(2183	nand	4991	4994)
	(4620	or	1513	1514	1515	1516)
	(5074	or	2190	2191	2192	2193)
	(4540	not	4534)
	(1507	nand	4534	4541)
	(4550	not	4544)
	(1510	nand	4544	4551)
	(2185	nand	2183	2184)
	(5004	not	4998)
	(2187	nand	4998	5005)
	(1506	nand	4537	4540)
	(1509	nand	4547	4550)
	(4626	not	4620)
	(2186	nand	5001	5004)
	(2195	and	2174	2185)
	(5080	not	5074)
	(1508	nand	1506	1507)
	(1511	nand	1509	1510)
	(2188	nand	2186	2187)
	(1512	not	1511)
	(1518	and	1497	1508)
	(2189	not	2188)
	(1517	and	1512	1502)
	(2194	and	2189	2179)
	(4623	or	1517	1518)
	(5077	or	2194	2195)
	(1519	nand	4623	4626)
	(4627	not	4623)
	(2196	nand	5077	5080)
	(5081	not	5077)
	(1520	nand	4620	4627)
	(2197	nand	5074	5081)
	(1521	nand	1519	1520)
	(2198	nand	2196	2197)
	(840	and	2198	3795	3823)
	(879	and	1521	3737	3765)
	(1524	not	1521)
	(2201	not	2198)
	(843	or	839	840	841	842)
	(882	or	878	879	880	881)
	(3649	and	1524	3628)
	(3652	and	2201	3628)
	(3657	or	3648	3649)
	(3658	or	3651	3652)
	(3636	and	3657	3622)
	(3639	and	3658	3622)
	(3642	and	3657	3622)
	(3645	and	3658	3622)
	(3653	or	3636	3637)
	(3654	or	3639	3640)
	(3655	or	3642	3643)
	(3656	or	3645	3646)
	(763	and	3656	2430	2454)
	(764	and	3655	2418	2454)
	(803	and	3656	2488	2512)
	(804	and	3655	2476	2512)
	(1657	and	3654	1621	1645)
	(1659	and	3653	1609	1645)
	(2328	and	3654	2293	2316)
	(2330	and	3653	2281	2316)
	(1662	or	1657	1659	1660	1661)
	(2333	or	2328	2330	2331	2332)
	(767	or	763	764	765	766)
	(807	or	803	804	805	806)
	(657	and	1662	1606)
	(689	and	2333	2279)
	(658	not	657)
	(690	not	689)
)