Context Navigation

← Previous Revision
Latest Revision
Next Revision →
Blame
Revision Log

FISCHER3-4-ninc.smt @ 100

Last change on this file since 100 was 12, checked in by cecile, 13 years ago
cusp added
Property svn:executable set to ``*
File size: 57.1 KB

Line
1	(benchmark FISCHER3_4_ninc.smt
2	:source {
3	Source unknown
4	This benchmark was automatically translated into SMT-LIB format from
5	CVC format using CVC Lite
6	}
7	:status sat
8	:category { industrial }
9	:difficulty { 0 }
10	:logic QF_IDL
11	:extrapreds ((AT0_PROC3_CS))
12	:extrapreds ((AT3_PROC2_SW_C_B_TAU))
13	:extrafuns ((AT4_PROC1_X Int))
14	:extrapreds ((AT1_PROC2_TAU))
15	:extrapreds ((AT1_PROC2_SW_C_CS_TAU))
16	:extrafuns ((AT2_PROC1_X Int))
17	:extrafuns ((AT0_PROC1_X Int))
18	:extrapreds ((AT3_PROC3_SW_C_CS_TAU))
19	:extrapreds ((AT3_PROC1_SW_A_B_TAU))
20	:extrapreds ((AT1_PROC1_SW_B_C_TAU))
21	:extrapreds ((AT3_PROC2_C))
22	:extrapreds ((AT3_PROC2_B))
23	:extrapreds ((AT0_ID0))
24	:extrapreds ((AT3_PROC2_A))
25	:extrapreds ((AT1_PROC2_C))
26	:extrapreds ((AT0_ID1))
27	:extrapreds ((AT1_PROC2_B))
28	:extrapreds ((AT0_ID2))
29	:extrapreds ((AT1_PROC2_A))
30	:extrapreds ((AT0_ID3))
31	:extrapreds ((AT0_PROC3_SW_CS_A_TAU))
32	:extrapreds ((AT4_PROC1_CS))
33	:extrapreds ((AT4_ID0))
34	:extrapreds ((AT3_DELTA))
35	:extrapreds ((AT4_ID1))
36	:extrapreds ((AT1_PROC2_SW_A_B_TAU))
37	:extrapreds ((AT1_PROC2_CS))
38	:extrapreds ((AT4_ID2))
39	:extrapreds ((AT4_ID3))
40	:extrapreds ((AT2_PROC1_SW_B_C_TAU))
41	:extrapreds ((AT1_PROC1_WAIT))
42	:extrapreds ((AT0_PROC3_TAU))
43	:extrapreds ((AT2_PROC2_TAU))
44	:extrapreds ((AT2_PROC2_SW_A_B_TAU))
45	:extrapreds ((AT0_PROC2_SW_C_B_TAU))
46	:extrapreds ((AT4_PROC1_C))
47	:extrafuns ((AT2_Z Int))
48	:extrapreds ((AT4_PROC1_B))
49	:extrapreds ((AT3_PROC1_SW_B_C_TAU))
50	:extrapreds ((AT4_PROC1_A))
51	:extrapreds ((AT2_PROC1_C))
52	:extrapreds ((AT2_PROC1_B))
53	:extrapreds ((AT2_PROC1_A))
54	:extrapreds ((AT0_PROC1_C))
55	:extrapreds ((AT0_PROC1_B))
56	:extrapreds ((AT0_PROC1_A))
57	:extrapreds ((AT2_PROC1_CS))
58	:extrapreds ((AT3_PROC2_SW_A_B_TAU))
59	:extrapreds ((AT1_PROC2_SW_B_C_TAU))
60	:extrapreds ((AT3_PROC1_WAIT))
61	:extrafuns ((AT3_PROC3_X Int))
62	:extrafuns ((AT1_PROC3_X Int))
63	:extrapreds ((AT3_PROC3_CS))
64	:extrapreds ((AT1_PROC3_TAU))
65	:extrapreds ((AT2_PROC3_WAIT))
66	:extrapreds ((AT0_PROC3_WAIT))
67	:extrapreds ((AT0_PROC2_CS))
68	:extrapreds ((AT2_PROC2_SW_B_C_TAU))
69	:extrapreds ((AT1_ID0))
70	:extrapreds ((AT1_ID1))
71	:extrapreds ((AT1_ID2))
72	:extrapreds ((AT1_ID3))
73	:extrapreds ((AT0_PROC1_SW_CS_A_TAU))
74	:extrafuns ((AT4_PROC2_X Int))
75	:extrapreds ((AT3_PROC2_SW_B_C_TAU))
76	:extrapreds ((AT3_PROC3_SW_B_C_TAU))
77	:extrapreds ((AT2_PROC2_SW_CS_A_TAU))
78	:extrafuns ((AT2_PROC2_X Int))
79	:extrapreds ((AT4_PROC2_CS))
80	:extrafuns ((AT0_PROC2_X Int))
81	:extrapreds ((AT1_PROC3_CS))
82	:extrapreds ((AT2_PROC3_TAU))
83	:extrapreds ((AT3_PROC3_C))
84	:extrapreds ((AT3_PROC3_TAU))
85	:extrapreds ((AT3_PROC3_B))
86	:extrapreds ((AT3_PROC3_A))
87	:extrapreds ((AT1_PROC3_C))
88	:extrapreds ((AT3_PROC1_SW_C_CS_TAU))
89	:extrapreds ((AT1_PROC3_B))
90	:extrafuns ((AT4_Z Int))
91	:extrapreds ((AT1_PROC3_A))
92	:extrapreds ((AT2_PROC3_SW_B_C_TAU))
93	:extrapreds ((AT1_PROC3_WAIT))
94	:extrapreds ((AT1_PROC3_SW_CS_A_TAU))
95	:extrafuns ((AT3_PROC1_X Int))
96	:extrapreds ((AT3_PROC3_SW_A_B_TAU))
97	:extrapreds ((AT1_PROC3_SW_B_C_TAU))
98	:extrafuns ((AT1_PROC1_X Int))
99	:extrapreds ((AT2_PROC2_CS))
100	:extrapreds ((AT4_PROC2_C))
101	:extrafuns ((AT1_Z Int))
102	:extrapreds ((AT4_PROC2_B))
103	:extrapreds ((AT2_PROC3_SW_C_CS_TAU))
104	:extrapreds ((AT4_PROC2_A))
105	:extrapreds ((AT2_PROC2_C))
106	:extrapreds ((AT3_PROC2_WAIT))
107	:extrapreds ((AT2_PROC2_B))
108	:extrapreds ((AT2_PROC2_A))
109	:extrapreds ((AT0_PROC2_C))
110	:extrapreds ((AT2_ID0))
111	:extrapreds ((AT0_PROC2_SW_C_CS_TAU))
112	:extrapreds ((AT0_PROC2_B))
113	:extrapreds ((AT2_ID1))
114	:extrapreds ((AT0_PROC2_A))
115	:extrapreds ((AT2_ID2))
116	:extrapreds ((AT2_ID3))
117	:extrapreds ((AT2_PROC3_SW_A_B_TAU))
118	:extrapreds ((AT0_PROC3_SW_B_C_TAU))
119	:extrapreds ((AT2_PROC2_WAIT))
120	:extrapreds ((AT0_PROC1_SW_C_B_TAU))
121	:extrapreds ((AT0_PROC1_CS))
122	:extrapreds ((AT0_PROC1_TAU))
123	:extrapreds ((AT2_PROC1_SW_CS_A_TAU))
124	:extrapreds ((AT0_PROC1_SW_C_CS_TAU))
125	:extrapreds ((AT2_PROC2_SW_C_CS_TAU))
126	:extrapreds ((AT0_PROC1_WAIT))
127	:extrapreds ((AT3_PROC1_CS))
128	:extrapreds ((AT1_PROC3_SW_A_B_TAU))
129	:extrapreds ((AT1_PROC1_SW_C_B_TAU))
130	:extrapreds ((AT3_PROC2_TAU))
131	:extrapreds ((AT3_PROC2_SW_C_CS_TAU))
132	:extrapreds ((AT3_PROC1_C))
133	:extrapreds ((AT3_PROC1_B))
134	:extrapreds ((AT4_PROC3_CS))
135	:extrapreds ((AT3_PROC1_A))
136	:extrapreds ((AT1_PROC1_C))
137	:extrapreds ((AT3_PROC1_SW_CS_A_TAU))
138	:extrapreds ((AT1_PROC1_SW_C_CS_TAU))
139	:extrapreds ((AT1_PROC1_B))
140	:extrapreds ((AT1_PROC1_A))
141	:extrapreds ((AT0_PROC3_SW_A_B_TAU))
142	:extrapreds ((AT2_PROC1_SW_C_B_TAU))
143	:extrapreds ((AT0_DELTA))
144	:extrafuns ((AT4_PROC3_X Int))
145	:extrapreds ((AT1_PROC2_SW_CS_A_TAU))
146	:extrafuns ((AT2_PROC3_X Int))
147	:extrapreds ((AT1_PROC1_TAU))
148	:extrapreds ((AT3_PROC3_SW_C_B_TAU))
149	:extrafuns ((AT0_PROC3_X Int))
150	:extrapreds ((AT3_PROC3_SW_CS_A_TAU))
151	:extrapreds ((AT1_PROC3_SW_C_CS_TAU))
152	:extrapreds ((AT1_PROC2_WAIT))
153	:extrapreds ((AT0_PROC2_SW_B_C_TAU))
154	:extrapreds ((AT1_PROC1_CS))
155	:extrapreds ((AT3_PROC1_SW_C_B_TAU))
156	:extrafuns ((AT3_Z Int))
157	:extrapreds ((AT2_PROC3_SW_CS_A_TAU))
158	:extrapreds ((AT0_PROC3_SW_C_CS_TAU))
159	:extrapreds ((AT3_ID0))
160	:extrapreds ((AT2_PROC3_SW_C_B_TAU))
161	:extrapreds ((AT0_PROC1_SW_A_B_TAU))
162	:extrapreds ((AT2_PROC3_CS))
163	:extrapreds ((AT3_ID1))
164	:extrapreds ((AT0_PROC2_SW_CS_A_TAU))
165	:extrapreds ((AT3_ID2))
166	:extrapreds ((AT3_ID3))
167	:extrapreds ((AT1_DELTA))
168	:extrapreds ((AT1_PROC2_SW_C_B_TAU))
169	:extrapreds ((AT3_PROC3_WAIT))
170	:extrafuns ((AT3_PROC2_X Int))
171	:extrapreds ((AT0_PROC2_TAU))
172	:extrapreds ((AT2_PROC1_TAU))
173	:extrapreds ((AT2_PROC1_SW_C_CS_TAU))
174	:extrafuns ((AT1_PROC2_X Int))
175	:extrapreds ((AT1_PROC3_SW_C_B_TAU))
176	:extrapreds ((AT1_PROC1_SW_A_B_TAU))
177	:extrapreds ((AT4_PROC3_C))
178	:extrafuns ((AT0_Z Int))
179	:extrapreds ((AT4_PROC3_B))
180	:extrapreds ((AT2_PROC1_WAIT))
181	:extrapreds ((AT4_PROC3_A))
182	:extrapreds ((AT2_PROC3_C))
183	:extrapreds ((AT2_PROC3_B))
184	:extrapreds ((AT3_PROC1_TAU))
185	:extrapreds ((AT2_PROC2_SW_C_B_TAU))
186	:extrapreds ((AT0_PROC2_SW_A_B_TAU))
187	:extrapreds ((AT2_PROC3_A))
188	:extrapreds ((AT0_PROC3_C))
189	:extrapreds ((AT3_PROC2_SW_CS_A_TAU))
190	:extrapreds ((AT0_PROC3_B))
191	:extrapreds ((AT0_PROC3_A))
192	:extrapreds ((AT3_PROC2_CS))
193	:extrapreds ((AT1_PROC1_SW_CS_A_TAU))
194	:extrapreds ((AT0_PROC3_SW_C_B_TAU))
195	:extrapreds ((AT0_PROC2_WAIT))
196	:extrapreds ((AT2_PROC1_SW_A_B_TAU))
197	:extrapreds ((AT2_DELTA))
198	:extrapreds ((AT0_PROC1_SW_B_C_TAU))
199	:formula
200	(flet ($cvcl_0 (not AT0_PROC1_A)) (flet ($cvcl_1 (not AT0_PROC1_B)) (flet ($cvcl_2 (not AT0_PROC1_C)) (flet ($cvcl_3 (not AT0_PROC1_CS)) (flet ($cvcl_4 (not AT1_PROC1_A)) (flet ($cvcl_5 (not AT1_PROC1_B)) (flet ($cvcl_6 (not AT1_PROC1_C)) (flet ($cvcl_7 (not AT1_PROC1_CS)) (flet ($cvcl_8 (not AT2_PROC1_A)) (flet ($cvcl_9 (not AT2_PROC1_B)) (flet ($cvcl_10 (not AT2_PROC1_C)) (flet ($cvcl_11 (not AT2_PROC1_CS)) (flet ($cvcl_12 (not AT3_PROC1_A)) (flet ($cvcl_13 (not AT3_PROC1_B)) (flet ($cvcl_14 (not AT3_PROC1_C)) (flet ($cvcl_15 (not AT3_PROC1_CS)) (flet ($cvcl_16 (not AT4_PROC1_A)) (flet ($cvcl_17 (not AT4_PROC1_B)) (flet ($cvcl_18 (not AT4_PROC1_C)) (flet ($cvcl_19 (not AT4_PROC1_CS)) (flet ($cvcl_20 (not AT0_PROC2_A)) (flet ($cvcl_21 (not AT0_PROC2_B)) (flet ($cvcl_22 (not AT0_PROC2_C)) (flet ($cvcl_23 (not AT0_PROC2_CS)) (flet ($cvcl_24 (not AT1_PROC2_A)) (flet ($cvcl_25 (not AT1_PROC2_B)) (flet ($cvcl_26 (not AT1_PROC2_C)) (flet ($cvcl_27 (not AT1_PROC2_CS)) (flet ($cvcl_28 (not AT2_PROC2_A)) (flet ($cvcl_29 (not AT2_PROC2_B)) (flet ($cvcl_30 (not AT2_PROC2_C)) (flet ($cvcl_31 (not AT2_PROC2_CS)) (flet ($cvcl_32 (not AT3_PROC2_A)) (flet ($cvcl_33 (not AT3_PROC2_B)) (flet ($cvcl_34 (not AT3_PROC2_C)) (flet ($cvcl_35 (not AT3_PROC2_CS)) (flet ($cvcl_36 (not AT4_PROC2_A)) (flet ($cvcl_37 (not AT4_PROC2_B)) (flet ($cvcl_38 (not AT4_PROC2_C)) (flet ($cvcl_39 (not AT4_PROC2_CS)) (flet ($cvcl_40 (not AT0_PROC3_A)) (flet ($cvcl_41 (not AT0_PROC3_B)) (flet ($cvcl_42 (not AT0_PROC3_C)) (flet ($cvcl_43 (not AT0_PROC3_CS)) (flet ($cvcl_44 (not AT1_PROC3_A)) (flet ($cvcl_45 (not AT1_PROC3_B)) (flet ($cvcl_46 (not AT1_PROC3_C)) (flet ($cvcl_47 (not AT1_PROC3_CS)) (flet ($cvcl_48 (not AT2_PROC3_A)) (flet ($cvcl_49 (not AT2_PROC3_B)) (flet ($cvcl_50 (not AT2_PROC3_C)) (flet ($cvcl_51 (not AT2_PROC3_CS)) (flet ($cvcl_52 (not AT3_PROC3_A)) (flet ($cvcl_53 (not AT3_PROC3_B)) (flet ($cvcl_54 (not AT3_PROC3_C)) (flet ($cvcl_55 (not AT3_PROC3_CS)) (flet ($cvcl_56 (not AT4_PROC3_A)) (flet ($cvcl_57 (not AT4_PROC3_B)) (flet ($cvcl_58 (not AT4_PROC3_C)) (flet ($cvcl_59 (not AT4_PROC3_CS)) (flet ($cvcl_60 (= AT0_PROC1_X AT0_Z)) (flet ($cvcl_61 (> AT0_PROC1_X AT0_Z)) (flet ($cvcl_229 (not $cvcl_60)) (flet ($cvcl_62 (= AT1_PROC1_X AT1_Z)) (flet ($cvcl_63 (> AT1_PROC1_X AT1_Z)) (flet ($cvcl_228 (not $cvcl_62)) (flet ($cvcl_64 (= AT2_PROC1_X AT2_Z)) (flet ($cvcl_65 (> AT2_PROC1_X AT2_Z)) (flet ($cvcl_234 (not $cvcl_64)) (flet ($cvcl_66 (= AT3_PROC1_X AT3_Z)) (flet ($cvcl_67 (> AT3_PROC1_X AT3_Z)) (flet ($cvcl_240 (not $cvcl_66)) (flet ($cvcl_68 (= AT4_PROC1_X AT4_Z)) (flet ($cvcl_69 (> AT4_PROC1_X AT4_Z)) (flet ($cvcl_246 (not $cvcl_68)) (flet ($cvcl_70 (= AT0_PROC2_X AT0_Z)) (flet ($cvcl_71 (> AT0_PROC2_X AT0_Z)) (flet ($cvcl_252 (not $cvcl_70)) (flet ($cvcl_72 (= AT1_PROC2_X AT1_Z)) (flet ($cvcl_73 (> AT1_PROC2_X AT1_Z)) (flet ($cvcl_251 (not $cvcl_72)) (flet ($cvcl_74 (= AT2_PROC2_X AT2_Z)) (flet ($cvcl_75 (> AT2_PROC2_X AT2_Z)) (flet ($cvcl_255 (not $cvcl_74)) (flet ($cvcl_76 (= AT3_PROC2_X AT3_Z)) (flet ($cvcl_77 (> AT3_PROC2_X AT3_Z)) (flet ($cvcl_259 (not $cvcl_76)) (flet ($cvcl_78 (= AT4_PROC2_X AT4_Z)) (flet ($cvcl_79 (> AT4_PROC2_X AT4_Z)) (flet ($cvcl_263 (not $cvcl_78)) (flet ($cvcl_80 (= AT0_PROC3_X AT0_Z)) (flet ($cvcl_81 (> AT0_PROC3_X AT0_Z)) (flet ($cvcl_268 (not $cvcl_80)) (flet ($cvcl_82 (= AT1_PROC3_X AT1_Z)) (flet ($cvcl_83 (> AT1_PROC3_X AT1_Z)) (flet ($cvcl_267 (not $cvcl_82)) (flet ($cvcl_84 (= AT2_PROC3_X AT2_Z)) (flet ($cvcl_85 (> AT2_PROC3_X AT2_Z)) (flet ($cvcl_271 (not $cvcl_84)) (flet ($cvcl_86 (= AT3_PROC3_X AT3_Z)) (flet ($cvcl_87 (> AT3_PROC3_X AT3_Z)) (flet ($cvcl_275 (not $cvcl_86)) (flet ($cvcl_88 (= AT4_PROC3_X AT4_Z)) (flet ($cvcl_89 (> AT4_PROC3_X AT4_Z)) (flet ($cvcl_279 (not $cvcl_88)) (flet ($cvcl_92 (<= (- AT0_PROC1_X AT0_Z) 10)) (flet ($cvcl_98 (<= (- AT1_PROC1_X AT1_Z) 10)) (flet ($cvcl_104 (<= (- AT2_PROC1_X AT2_Z) 10)) (flet ($cvcl_110 (<= (- AT3_PROC1_X AT3_Z) 10)) (flet ($cvcl_120 (<= (- AT0_PROC2_X AT0_Z) 10)) (flet ($cvcl_126 (<= (- AT1_PROC2_X AT1_Z) 10)) (flet ($cvcl_132 (<= (- AT2_PROC2_X AT2_Z) 10)) (flet ($cvcl_138 (<= (- AT3_PROC2_X AT3_Z) 10)) (flet ($cvcl_144 (<= (- AT0_PROC3_X AT0_Z) 10)) (flet ($cvcl_150 (<= (- AT1_PROC3_X AT1_Z) 10)) (flet ($cvcl_156 (<= (- AT2_PROC3_X AT2_Z) 10)) (flet ($cvcl_162 (<= (- AT3_PROC3_X AT3_Z) 10)) (flet ($cvcl_90 (not AT0_PROC1_SW_A_B_TAU)) (flet ($cvcl_91 (not AT0_PROC1_SW_B_C_TAU)) (flet ($cvcl_93 (not AT0_PROC1_SW_C_B_TAU)) (flet ($cvcl_94 (not AT0_PROC1_SW_C_CS_TAU)) (flet ($cvcl_167 (= AT1_PROC1_X AT0_PROC1_X)) (flet ($cvcl_95 (not AT0_PROC1_SW_CS_A_TAU)) (flet ($cvcl_96 (not AT1_PROC1_SW_A_B_TAU)) (flet ($cvcl_97 (not AT1_PROC1_SW_B_C_TAU)) (flet ($cvcl_99 (not AT1_PROC1_SW_C_B_TAU)) (flet ($cvcl_100 (not AT1_PROC1_SW_C_CS_TAU)) (flet ($cvcl_169 (= AT2_PROC1_X AT1_PROC1_X)) (flet ($cvcl_101 (not AT1_PROC1_SW_CS_A_TAU)) (flet ($cvcl_102 (not AT2_PROC1_SW_A_B_TAU)) (flet ($cvcl_103 (not AT2_PROC1_SW_B_C_TAU)) (flet ($cvcl_105 (not AT2_PROC1_SW_C_B_TAU)) (flet ($cvcl_106 (not AT2_PROC1_SW_C_CS_TAU)) (flet ($cvcl_171 (= AT3_PROC1_X AT2_PROC1_X)) (flet ($cvcl_107 (not AT2_PROC1_SW_CS_A_TAU)) (flet ($cvcl_108 (not AT3_PROC1_SW_A_B_TAU)) (flet ($cvcl_109 (not AT3_PROC1_SW_B_C_TAU)) (flet ($cvcl_111 (not AT3_PROC1_SW_C_B_TAU)) (flet ($cvcl_112 (not AT3_PROC1_SW_C_CS_TAU)) (flet ($cvcl_173 (= AT4_PROC1_X AT3_PROC1_X)) (flet ($cvcl_113 (not AT3_PROC1_SW_CS_A_TAU)) (flet ($cvcl_114 (= AT1_Z AT0_Z)) (flet ($cvcl_115 (= AT2_Z AT1_Z)) (flet ($cvcl_116 (= AT3_Z AT2_Z)) (flet ($cvcl_117 (= AT4_Z AT3_Z)) (flet ($cvcl_118 (not AT0_PROC2_SW_A_B_TAU)) (flet ($cvcl_119 (not AT0_PROC2_SW_B_C_TAU)) (flet ($cvcl_121 (not AT0_PROC2_SW_C_B_TAU)) (flet ($cvcl_122 (not AT0_PROC2_SW_C_CS_TAU)) (flet ($cvcl_175 (= AT1_PROC2_X AT0_PROC2_X)) (flet ($cvcl_123 (not AT0_PROC2_SW_CS_A_TAU)) (flet ($cvcl_124 (not AT1_PROC2_SW_A_B_TAU)) (flet ($cvcl_125 (not AT1_PROC2_SW_B_C_TAU)) (flet ($cvcl_127 (not AT1_PROC2_SW_C_B_TAU)) (flet ($cvcl_128 (not AT1_PROC2_SW_C_CS_TAU)) (flet ($cvcl_177 (= AT2_PROC2_X AT1_PROC2_X)) (flet ($cvcl_129 (not AT1_PROC2_SW_CS_A_TAU)) (flet ($cvcl_130 (not AT2_PROC2_SW_A_B_TAU)) (flet ($cvcl_131 (not AT2_PROC2_SW_B_C_TAU)) (flet ($cvcl_133 (not AT2_PROC2_SW_C_B_TAU)) (flet ($cvcl_134 (not AT2_PROC2_SW_C_CS_TAU)) (flet ($cvcl_179 (= AT3_PROC2_X AT2_PROC2_X)) (flet ($cvcl_135 (not AT2_PROC2_SW_CS_A_TAU)) (flet ($cvcl_136 (not AT3_PROC2_SW_A_B_TAU)) (flet ($cvcl_137 (not AT3_PROC2_SW_B_C_TAU)) (flet ($cvcl_139 (not AT3_PROC2_SW_C_B_TAU)) (flet ($cvcl_140 (not AT3_PROC2_SW_C_CS_TAU)) (flet ($cvcl_181 (= AT4_PROC2_X AT3_PROC2_X)) (flet ($cvcl_141 (not AT3_PROC2_SW_CS_A_TAU)) (flet ($cvcl_142 (not AT0_PROC3_SW_A_B_TAU)) (flet ($cvcl_143 (not AT0_PROC3_SW_B_C_TAU)) (flet ($cvcl_145 (not AT0_PROC3_SW_C_B_TAU)) (flet ($cvcl_146 (not AT0_PROC3_SW_C_CS_TAU)) (flet ($cvcl_183 (= AT1_PROC3_X AT0_PROC3_X)) (flet ($cvcl_147 (not AT0_PROC3_SW_CS_A_TAU)) (flet ($cvcl_148 (not AT1_PROC3_SW_A_B_TAU)) (flet ($cvcl_149 (not AT1_PROC3_SW_B_C_TAU)) (flet ($cvcl_151 (not AT1_PROC3_SW_C_B_TAU)) (flet ($cvcl_152 (not AT1_PROC3_SW_C_CS_TAU)) (flet ($cvcl_185 (= AT2_PROC3_X AT1_PROC3_X)) (flet ($cvcl_153 (not AT1_PROC3_SW_CS_A_TAU)) (flet ($cvcl_154 (not AT2_PROC3_SW_A_B_TAU)) (flet ($cvcl_155 (not AT2_PROC3_SW_B_C_TAU)) (flet ($cvcl_157 (not AT2_PROC3_SW_C_B_TAU)) (flet ($cvcl_158 (not AT2_PROC3_SW_C_CS_TAU)) (flet ($cvcl_187 (= AT3_PROC3_X AT2_PROC3_X)) (flet ($cvcl_159 (not AT2_PROC3_SW_CS_A_TAU)) (flet ($cvcl_160 (not AT3_PROC3_SW_A_B_TAU)) (flet ($cvcl_161 (not AT3_PROC3_SW_B_C_TAU)) (flet ($cvcl_163 (not AT3_PROC3_SW_C_B_TAU)) (flet ($cvcl_164 (not AT3_PROC3_SW_C_CS_TAU)) (flet ($cvcl_189 (= AT4_PROC3_X AT3_PROC3_X)) (flet ($cvcl_165 (not AT3_PROC3_SW_CS_A_TAU)) (flet ($cvcl_166 (not AT0_PROC1_WAIT)) (flet ($cvcl_191 (not AT0_PROC1_TAU)) (flet ($cvcl_168 (not AT1_PROC1_WAIT)) (flet ($cvcl_193 (not AT1_PROC1_TAU)) (flet ($cvcl_170 (not AT2_PROC1_WAIT)) (flet ($cvcl_195 (not AT2_PROC1_TAU)) (flet ($cvcl_172 (not AT3_PROC1_WAIT)) (flet ($cvcl_197 (not AT3_PROC1_TAU)) (flet ($cvcl_174 (not AT0_PROC2_WAIT)) (flet ($cvcl_198 (not AT0_PROC2_TAU)) (flet ($cvcl_176 (not AT1_PROC2_WAIT)) (flet ($cvcl_200 (not AT1_PROC2_TAU)) (flet ($cvcl_178 (not AT2_PROC2_WAIT)) (flet ($cvcl_202 (not AT2_PROC2_TAU)) (flet ($cvcl_180 (not AT3_PROC2_WAIT)) (flet ($cvcl_204 (not AT3_PROC2_TAU)) (flet ($cvcl_182 (not AT0_PROC3_WAIT)) (flet ($cvcl_206 (not AT0_PROC3_TAU)) (flet ($cvcl_184 (not AT1_PROC3_WAIT)) (flet ($cvcl_207 (not AT1_PROC3_TAU)) (flet ($cvcl_186 (not AT2_PROC3_WAIT)) (flet ($cvcl_208 (not AT2_PROC3_TAU)) (flet ($cvcl_188 (not AT3_PROC3_WAIT)) (flet ($cvcl_209 (not AT3_PROC3_TAU)) (flet ($cvcl_190 (not AT0_DELTA)) (flet ($cvcl_222 (< AT1_Z AT0_Z)) (flet ($cvcl_199 (or $cvcl_190 $cvcl_222 )) (flet ($cvcl_192 (not AT1_DELTA)) (flet ($cvcl_223 (< AT2_Z AT1_Z)) (flet ($cvcl_201 (or $cvcl_192 $cvcl_223 )) (flet ($cvcl_194 (not AT2_DELTA)) (flet ($cvcl_224 (< AT3_Z AT2_Z)) (flet ($cvcl_203 (or $cvcl_194 $cvcl_224 )) (flet ($cvcl_196 (not AT3_DELTA)) (flet ($cvcl_225 (< AT4_Z AT3_Z)) (flet ($cvcl_205 (or $cvcl_196 $cvcl_225 )) (flet ($cvcl_210 (< AT1_PROC1_X AT0_PROC1_X)) (flet ($cvcl_226 (not $cvcl_167)) (flet ($cvcl_211 (< AT2_PROC1_X AT1_PROC1_X)) (flet ($cvcl_232 (not $cvcl_169)) (flet ($cvcl_212 (< AT3_PROC1_X AT2_PROC1_X)) (flet ($cvcl_238 (not $cvcl_171)) (flet ($cvcl_213 (< AT4_PROC1_X AT3_PROC1_X)) (flet ($cvcl_244 (not $cvcl_173)) (flet ($cvcl_214 (< AT1_PROC2_X AT0_PROC2_X)) (flet ($cvcl_250 (not $cvcl_175)) (flet ($cvcl_215 (< AT2_PROC2_X AT1_PROC2_X)) (flet ($cvcl_254 (not $cvcl_177)) (flet ($cvcl_216 (< AT3_PROC2_X AT2_PROC2_X)) (flet ($cvcl_258 (not $cvcl_179)) (flet ($cvcl_217 (< AT4_PROC2_X AT3_PROC2_X)) (flet ($cvcl_262 (not $cvcl_181)) (flet ($cvcl_218 (< AT1_PROC3_X AT0_PROC3_X)) (flet ($cvcl_266 (not $cvcl_183)) (flet ($cvcl_219 (< AT2_PROC3_X AT1_PROC3_X)) (flet ($cvcl_270 (not $cvcl_185)) (flet ($cvcl_220 (< AT3_PROC3_X AT2_PROC3_X)) (flet ($cvcl_274 (not $cvcl_187)) (flet ($cvcl_221 (< AT4_PROC3_X AT3_PROC3_X)) (flet ($cvcl_278 (not $cvcl_189)) (flet ($cvcl_227 (not $cvcl_114)) (flet ($cvcl_231 (not $cvcl_222)) (flet ($cvcl_233 (not $cvcl_115)) (flet ($cvcl_237 (not $cvcl_223)) (flet ($cvcl_239 (not $cvcl_116)) (flet ($cvcl_243 (not $cvcl_224)) (flet ($cvcl_245 (not $cvcl_117)) (flet ($cvcl_249 (not $cvcl_225)) (flet ($cvcl_230 (or $cvcl_229 $cvcl_226 )) (flet ($cvcl_236 (< AT1_Z AT1_PROC1_X)) (flet ($cvcl_235 (or $cvcl_228 $cvcl_232 )) (flet ($cvcl_242 (< AT2_Z AT2_PROC1_X)) (flet ($cvcl_241 (or $cvcl_234 $cvcl_238 )) (flet ($cvcl_248 (< AT3_Z AT3_PROC1_X)) (flet ($cvcl_247 (or $cvcl_240 $cvcl_244 )) (flet ($cvcl_253 (or $cvcl_252 $cvcl_250 )) (flet ($cvcl_257 (< AT1_Z AT1_PROC2_X)) (flet ($cvcl_256 (or $cvcl_251 $cvcl_254 )) (flet ($cvcl_261 (< AT2_Z AT2_PROC2_X)) (flet ($cvcl_260 (or $cvcl_255 $cvcl_258 )) (flet ($cvcl_265 (< AT3_Z AT3_PROC2_X)) (flet ($cvcl_264 (or $cvcl_259 $cvcl_262 )) (flet ($cvcl_269 (or $cvcl_268 $cvcl_266 )) (flet ($cvcl_273 (< AT1_Z AT1_PROC3_X)) (flet ($cvcl_272 (or $cvcl_267 $cvcl_270 )) (flet ($cvcl_277 (< AT2_Z AT2_PROC3_X)) (flet ($cvcl_276 (or $cvcl_271 $cvcl_274 )) (flet ($cvcl_281 (< AT3_Z AT3_PROC3_X)) (flet ($cvcl_280 (or $cvcl_275 $cvcl_278 )) (flet ($cvcl_282 (not AT0_ID0)) (flet ($cvcl_283 (not AT0_ID1)) (flet ($cvcl_284 (not AT0_ID2)) (flet ($cvcl_285 (not AT0_ID3)) (flet ($cvcl_286 (not AT1_ID0)) (flet ($cvcl_287 (not AT1_ID1)) (flet ($cvcl_288 (not AT1_ID2)) (flet ($cvcl_289 (not AT1_ID3)) (flet ($cvcl_290 (not AT2_ID0)) (flet ($cvcl_291 (not AT2_ID1)) (flet ($cvcl_292 (not AT2_ID2)) (flet ($cvcl_293 (not AT2_ID3)) (flet ($cvcl_294 (not AT3_ID0)) (flet ($cvcl_295 (not AT3_ID1)) (flet ($cvcl_296 (not AT3_ID2)) (flet ($cvcl_297 (not AT3_ID3)) (flet ($cvcl_298 (not AT4_ID0)) (flet ($cvcl_299 (not AT4_ID1)) (flet ($cvcl_300 (not AT4_ID2)) (flet ($cvcl_301 (not AT4_ID3)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or $cvcl_0 $cvcl_1 ) (or $cvcl_0 $cvcl_2 )) (or $cvcl_0 $cvcl_3 )) (or $cvcl_1 $cvcl_2 )) (or $cvcl_1 $cvcl_3 )) (or $cvcl_2 $cvcl_3 )) (or $cvcl_4 $cvcl_5 )) (or $cvcl_4 $cvcl_6 )) (or $cvcl_4 $cvcl_7 )) (or $cvcl_5 $cvcl_6 )) (or $cvcl_5 $cvcl_7 )) (or $cvcl_6 $cvcl_7 )) (or $cvcl_8 $cvcl_9 )) (or $cvcl_8 $cvcl_10 )) (or $cvcl_8 $cvcl_11 )) (or $cvcl_9 $cvcl_10 )) (or $cvcl_9 $cvcl_11 )) (or $cvcl_10 $cvcl_11 )) (or $cvcl_12 $cvcl_13 )) (or $cvcl_12 $cvcl_14 )) (or $cvcl_12 $cvcl_15 )) (or $cvcl_13 $cvcl_14 )) (or $cvcl_13 $cvcl_15 )) (or $cvcl_14 $cvcl_15 )) (or $cvcl_16 $cvcl_17 )) (or $cvcl_16 $cvcl_18 )) (or $cvcl_16 $cvcl_19 )) (or $cvcl_17 $cvcl_18 )) (or $cvcl_17 $cvcl_19 )) (or $cvcl_18 $cvcl_19 )) (or $cvcl_20 $cvcl_21 )) (or $cvcl_20 $cvcl_22 )) (or $cvcl_20 $cvcl_23 )) (or $cvcl_21 $cvcl_22 )) (or $cvcl_21 $cvcl_23 )) (or $cvcl_22 $cvcl_23 )) (or $cvcl_24 $cvcl_25 )) (or $cvcl_24 $cvcl_26 )) (or $cvcl_24 $cvcl_27 )) (or $cvcl_25 $cvcl_26 )) (or $cvcl_25 $cvcl_27 )) (or $cvcl_26 $cvcl_27 )) (or $cvcl_28 $cvcl_29 )) (or $cvcl_28 $cvcl_30 )) (or $cvcl_28 $cvcl_31 )) (or $cvcl_29 $cvcl_30 )) (or $cvcl_29 $cvcl_31 )) (or $cvcl_30 $cvcl_31 )) (or $cvcl_32 $cvcl_33 )) (or $cvcl_32 $cvcl_34 )) (or $cvcl_32 $cvcl_35 )) (or $cvcl_33 $cvcl_34 )) (or $cvcl_33 $cvcl_35 )) (or $cvcl_34 $cvcl_35 )) (or $cvcl_36 $cvcl_37 )) (or $cvcl_36 $cvcl_38 )) (or $cvcl_36 $cvcl_39 )) (or $cvcl_37 $cvcl_38 )) (or $cvcl_37 $cvcl_39 )) (or $cvcl_38 $cvcl_39 )) (or $cvcl_40 $cvcl_41 )) (or $cvcl_40 $cvcl_42 )) (or $cvcl_40 $cvcl_43 )) (or $cvcl_41 $cvcl_42 )) (or $cvcl_41 $cvcl_43 )) (or $cvcl_42 $cvcl_43 )) (or $cvcl_44 $cvcl_45 )) (or $cvcl_44 $cvcl_46 )) (or $cvcl_44 $cvcl_47 )) (or $cvcl_45 $cvcl_46 )) (or $cvcl_45 $cvcl_47 )) (or $cvcl_46 $cvcl_47 )) (or $cvcl_48 $cvcl_49 )) (or $cvcl_48 $cvcl_50 )) (or $cvcl_48 $cvcl_51 )) (or $cvcl_49 $cvcl_50 )) (or $cvcl_49 $cvcl_51 )) (or $cvcl_50 $cvcl_51 )) (or $cvcl_52 $cvcl_53 )) (or $cvcl_52 $cvcl_54 )) (or $cvcl_52 $cvcl_55 )) (or $cvcl_53 $cvcl_54 )) (or $cvcl_53 $cvcl_55 )) (or $cvcl_54 $cvcl_55 )) (or $cvcl_56 $cvcl_57 )) (or $cvcl_56 $cvcl_58 )) (or $cvcl_56 $cvcl_59 )) (or $cvcl_57 $cvcl_58 )) (or $cvcl_57 $cvcl_59 )) (or $cvcl_58 $cvcl_59 )) (or $cvcl_60 $cvcl_61 )) (or $cvcl_229 (not $cvcl_61) )) (or $cvcl_62 $cvcl_63 )) (or $cvcl_228 (not $cvcl_63) )) (or $cvcl_64 $cvcl_65 )) (or $cvcl_234 (not $cvcl_65) )) (or $cvcl_66 $cvcl_67 )) (or $cvcl_240 (not $cvcl_67) )) (or $cvcl_68 $cvcl_69 )) (or $cvcl_246 (not $cvcl_69) )) (or $cvcl_70 $cvcl_71 )) (or $cvcl_252 (not $cvcl_71) )) (or $cvcl_72 $cvcl_73 )) (or $cvcl_251 (not $cvcl_73) )) (or $cvcl_74 $cvcl_75 )) (or $cvcl_255 (not $cvcl_75) )) (or $cvcl_76 $cvcl_77 )) (or $cvcl_259 (not $cvcl_77) )) (or $cvcl_78 $cvcl_79 )) (or $cvcl_263 (not $cvcl_79) )) (or $cvcl_80 $cvcl_81 )) (or $cvcl_268 (not $cvcl_81) )) (or $cvcl_82 $cvcl_83 )) (or $cvcl_267 (not $cvcl_83) )) (or $cvcl_84 $cvcl_85 )) (or $cvcl_271 (not $cvcl_85) )) (or $cvcl_86 $cvcl_87 )) (or $cvcl_275 (not $cvcl_87) )) (or $cvcl_88 $cvcl_89 )) (or $cvcl_279 (not $cvcl_89) )) (or $cvcl_1 $cvcl_92 )) (or $cvcl_5 $cvcl_98 )) (or $cvcl_9 $cvcl_104 )) (or $cvcl_13 $cvcl_110 )) (or $cvcl_17 (<= (- AT4_PROC1_X AT4_Z) 10) )) (or $cvcl_21 $cvcl_120 )) (or $cvcl_25 $cvcl_126 )) (or $cvcl_29 $cvcl_132 )) (or $cvcl_33 $cvcl_138 )) (or $cvcl_37 (<= (- AT4_PROC2_X AT4_Z) 10) )) (or $cvcl_41 $cvcl_144 )) (or $cvcl_45 $cvcl_150 )) (or $cvcl_49 $cvcl_156 )) (or $cvcl_53 $cvcl_162 )) (or $cvcl_57 (<= (- AT4_PROC3_X AT4_Z) 10) )) (or (or (or (or (or (or AT0_PROC1_WAIT AT0_DELTA ) AT0_PROC1_SW_A_B_TAU ) AT0_PROC1_SW_B_C_TAU ) AT0_PROC1_SW_C_B_TAU ) AT0_PROC1_SW_C_CS_TAU ) AT0_PROC1_SW_CS_A_TAU )) (or (or (or (or (or (or AT1_PROC1_WAIT AT1_DELTA ) AT1_PROC1_SW_A_B_TAU ) AT1_PROC1_SW_B_C_TAU ) AT1_PROC1_SW_C_B_TAU ) AT1_PROC1_SW_C_CS_TAU ) AT1_PROC1_SW_CS_A_TAU )) (or (or (or (or (or (or AT2_PROC1_WAIT AT2_DELTA ) AT2_PROC1_SW_A_B_TAU ) AT2_PROC1_SW_B_C_TAU ) AT2_PROC1_SW_C_B_TAU ) AT2_PROC1_SW_C_CS_TAU ) AT2_PROC1_SW_CS_A_TAU )) (or (or (or (or (or (or AT3_PROC1_WAIT AT3_DELTA ) AT3_PROC1_SW_A_B_TAU ) AT3_PROC1_SW_B_C_TAU ) AT3_PROC1_SW_C_B_TAU ) AT3_PROC1_SW_C_CS_TAU ) AT3_PROC1_SW_CS_A_TAU )) (or (or (or (or (or (or AT0_PROC2_WAIT AT0_DELTA ) AT0_PROC2_SW_A_B_TAU ) AT0_PROC2_SW_B_C_TAU ) AT0_PROC2_SW_C_B_TAU ) AT0_PROC2_SW_C_CS_TAU ) AT0_PROC2_SW_CS_A_TAU )) (or (or (or (or (or (or AT1_PROC2_WAIT AT1_DELTA ) AT1_PROC2_SW_A_B_TAU ) AT1_PROC2_SW_B_C_TAU ) AT1_PROC2_SW_C_B_TAU ) AT1_PROC2_SW_C_CS_TAU ) AT1_PROC2_SW_CS_A_TAU )) (or (or (or (or (or (or AT2_PROC2_WAIT AT2_DELTA ) AT2_PROC2_SW_A_B_TAU ) AT2_PROC2_SW_B_C_TAU ) AT2_PROC2_SW_C_B_TAU ) AT2_PROC2_SW_C_CS_TAU ) AT2_PROC2_SW_CS_A_TAU )) (or (or (or (or (or (or AT3_PROC2_WAIT AT3_DELTA ) AT3_PROC2_SW_A_B_TAU ) AT3_PROC2_SW_B_C_TAU ) AT3_PROC2_SW_C_B_TAU ) AT3_PROC2_SW_C_CS_TAU ) AT3_PROC2_SW_CS_A_TAU )) (or (or (or (or (or (or AT0_PROC3_WAIT AT0_DELTA ) AT0_PROC3_SW_A_B_TAU ) AT0_PROC3_SW_B_C_TAU ) AT0_PROC3_SW_C_B_TAU ) AT0_PROC3_SW_C_CS_TAU ) AT0_PROC3_SW_CS_A_TAU )) (or (or (or (or (or (or AT1_PROC3_WAIT AT1_DELTA ) AT1_PROC3_SW_A_B_TAU ) AT1_PROC3_SW_B_C_TAU ) AT1_PROC3_SW_C_B_TAU ) AT1_PROC3_SW_C_CS_TAU ) AT1_PROC3_SW_CS_A_TAU )) (or (or (or (or (or (or AT2_PROC3_WAIT AT2_DELTA ) AT2_PROC3_SW_A_B_TAU ) AT2_PROC3_SW_B_C_TAU ) AT2_PROC3_SW_C_B_TAU ) AT2_PROC3_SW_C_CS_TAU ) AT2_PROC3_SW_CS_A_TAU )) (or (or (or (or (or (or AT3_PROC3_WAIT AT3_DELTA ) AT3_PROC3_SW_A_B_TAU ) AT3_PROC3_SW_B_C_TAU ) AT3_PROC3_SW_C_B_TAU ) AT3_PROC3_SW_C_CS_TAU ) AT3_PROC3_SW_CS_A_TAU )) (or $cvcl_90 AT0_PROC1_A )) (or $cvcl_90 AT0_PROC1_TAU )) (or $cvcl_90 AT1_PROC1_B )) (or $cvcl_90 $cvcl_62 )) (or $cvcl_91 AT0_PROC1_B )) (or $cvcl_91 AT0_PROC1_TAU )) (or $cvcl_91 AT1_PROC1_C )) (or $cvcl_91 $cvcl_92 )) (or $cvcl_91 $cvcl_62 )) (or $cvcl_93 AT0_PROC1_C )) (or $cvcl_93 AT0_PROC1_TAU )) (or $cvcl_93 AT1_PROC1_B )) (or $cvcl_93 $cvcl_62 )) (or $cvcl_94 AT0_PROC1_C )) (or $cvcl_94 AT0_PROC1_TAU )) (or $cvcl_94 AT1_PROC1_CS )) (or $cvcl_94 (> (- AT0_PROC1_X AT0_Z) 10) )) (or $cvcl_94 $cvcl_167 )) (or $cvcl_95 AT0_PROC1_CS )) (or $cvcl_95 AT0_PROC1_TAU )) (or $cvcl_95 AT1_PROC1_A )) (or $cvcl_95 $cvcl_62 )) (or $cvcl_96 AT1_PROC1_A )) (or $cvcl_96 AT1_PROC1_TAU )) (or $cvcl_96 AT2_PROC1_B )) (or $cvcl_96 $cvcl_64 )) (or $cvcl_97 AT1_PROC1_B )) (or $cvcl_97 AT1_PROC1_TAU )) (or $cvcl_97 AT2_PROC1_C )) (or $cvcl_97 $cvcl_98 )) (or $cvcl_97 $cvcl_64 )) (or $cvcl_99 AT1_PROC1_C )) (or $cvcl_99 AT1_PROC1_TAU )) (or $cvcl_99 AT2_PROC1_B )) (or $cvcl_99 $cvcl_64 )) (or $cvcl_100 AT1_PROC1_C )) (or $cvcl_100 AT1_PROC1_TAU )) (or $cvcl_100 AT2_PROC1_CS )) (or $cvcl_100 (> (- AT1_PROC1_X AT1_Z) 10) )) (or $cvcl_100 $cvcl_169 )) (or $cvcl_101 AT1_PROC1_CS )) (or $cvcl_101 AT1_PROC1_TAU )) (or $cvcl_101 AT2_PROC1_A )) (or $cvcl_101 $cvcl_64 )) (or $cvcl_102 AT2_PROC1_A )) (or $cvcl_102 AT2_PROC1_TAU )) (or $cvcl_102 AT3_PROC1_B )) (or $cvcl_102 $cvcl_66 )) (or $cvcl_103 AT2_PROC1_B )) (or $cvcl_103 AT2_PROC1_TAU )) (or $cvcl_103 AT3_PROC1_C )) (or $cvcl_103 $cvcl_104 )) (or $cvcl_103 $cvcl_66 )) (or $cvcl_105 AT2_PROC1_C )) (or $cvcl_105 AT2_PROC1_TAU )) (or $cvcl_105 AT3_PROC1_B )) (or $cvcl_105 $cvcl_66 )) (or $cvcl_106 AT2_PROC1_C )) (or $cvcl_106 AT2_PROC1_TAU )) (or $cvcl_106 AT3_PROC1_CS )) (or $cvcl_106 (> (- AT2_PROC1_X AT2_Z) 10) )) (or $cvcl_106 $cvcl_171 )) (or $cvcl_107 AT2_PROC1_CS )) (or $cvcl_107 AT2_PROC1_TAU )) (or $cvcl_107 AT3_PROC1_A )) (or $cvcl_107 $cvcl_66 )) (or $cvcl_108 AT3_PROC1_A )) (or $cvcl_108 AT3_PROC1_TAU )) (or $cvcl_108 AT4_PROC1_B )) (or $cvcl_108 $cvcl_68 )) (or $cvcl_109 AT3_PROC1_B )) (or $cvcl_109 AT3_PROC1_TAU )) (or $cvcl_109 AT4_PROC1_C )) (or $cvcl_109 $cvcl_110 )) (or $cvcl_109 $cvcl_68 )) (or $cvcl_111 AT3_PROC1_C )) (or $cvcl_111 AT3_PROC1_TAU )) (or $cvcl_111 AT4_PROC1_B )) (or $cvcl_111 $cvcl_68 )) (or $cvcl_112 AT3_PROC1_C )) (or $cvcl_112 AT3_PROC1_TAU )) (or $cvcl_112 AT4_PROC1_CS )) (or $cvcl_112 (> (- AT3_PROC1_X AT3_Z) 10) )) (or $cvcl_112 $cvcl_173 )) (or $cvcl_113 AT3_PROC1_CS )) (or $cvcl_113 AT3_PROC1_TAU )) (or $cvcl_113 AT4_PROC1_A )) (or $cvcl_113 $cvcl_68 )) (or $cvcl_90 $cvcl_114 )) (or $cvcl_91 $cvcl_114 )) (or $cvcl_93 $cvcl_114 )) (or $cvcl_94 $cvcl_114 )) (or $cvcl_95 $cvcl_114 )) (or $cvcl_96 $cvcl_115 )) (or $cvcl_97 $cvcl_115 )) (or $cvcl_99 $cvcl_115 )) (or $cvcl_100 $cvcl_115 )) (or $cvcl_101 $cvcl_115 )) (or $cvcl_102 $cvcl_116 )) (or $cvcl_103 $cvcl_116 )) (or $cvcl_105 $cvcl_116 )) (or $cvcl_106 $cvcl_116 )) (or $cvcl_107 $cvcl_116 )) (or $cvcl_108 $cvcl_117 )) (or $cvcl_109 $cvcl_117 )) (or $cvcl_111 $cvcl_117 )) (or $cvcl_112 $cvcl_117 )) (or $cvcl_113 $cvcl_117 )) (or $cvcl_118 AT0_PROC2_A )) (or $cvcl_118 AT0_PROC2_TAU )) (or $cvcl_118 AT1_PROC2_B )) (or $cvcl_118 $cvcl_72 )) (or $cvcl_119 AT0_PROC2_B )) (or $cvcl_119 AT0_PROC2_TAU )) (or $cvcl_119 AT1_PROC2_C )) (or $cvcl_119 $cvcl_120 )) (or $cvcl_119 $cvcl_72 )) (or $cvcl_121 AT0_PROC2_C )) (or $cvcl_121 AT0_PROC2_TAU )) (or $cvcl_121 AT1_PROC2_B )) (or $cvcl_121 $cvcl_72 )) (or $cvcl_122 AT0_PROC2_C )) (or $cvcl_122 AT0_PROC2_TAU )) (or $cvcl_122 AT1_PROC2_CS )) (or $cvcl_122 (> (- AT0_PROC2_X AT0_Z) 10) )) (or $cvcl_122 $cvcl_175 )) (or $cvcl_123 AT0_PROC2_CS )) (or $cvcl_123 AT0_PROC2_TAU )) (or $cvcl_123 AT1_PROC2_A )) (or $cvcl_123 $cvcl_72 )) (or $cvcl_124 AT1_PROC2_A )) (or $cvcl_124 AT1_PROC2_TAU )) (or $cvcl_124 AT2_PROC2_B )) (or $cvcl_124 $cvcl_74 )) (or $cvcl_125 AT1_PROC2_B )) (or $cvcl_125 AT1_PROC2_TAU )) (or $cvcl_125 AT2_PROC2_C )) (or $cvcl_125 $cvcl_126 )) (or $cvcl_125 $cvcl_74 )) (or $cvcl_127 AT1_PROC2_C )) (or $cvcl_127 AT1_PROC2_TAU )) (or $cvcl_127 AT2_PROC2_B )) (or $cvcl_127 $cvcl_74 )) (or $cvcl_128 AT1_PROC2_C )) (or $cvcl_128 AT1_PROC2_TAU )) (or $cvcl_128 AT2_PROC2_CS )) (or $cvcl_128 (> (- AT1_PROC2_X AT1_Z) 10) )) (or $cvcl_128 $cvcl_177 )) (or $cvcl_129 AT1_PROC2_CS )) (or $cvcl_129 AT1_PROC2_TAU )) (or $cvcl_129 AT2_PROC2_A )) (or $cvcl_129 $cvcl_74 )) (or $cvcl_130 AT2_PROC2_A )) (or $cvcl_130 AT2_PROC2_TAU )) (or $cvcl_130 AT3_PROC2_B )) (or $cvcl_130 $cvcl_76 )) (or $cvcl_131 AT2_PROC2_B )) (or $cvcl_131 AT2_PROC2_TAU )) (or $cvcl_131 AT3_PROC2_C )) (or $cvcl_131 $cvcl_132 )) (or $cvcl_131 $cvcl_76 )) (or $cvcl_133 AT2_PROC2_C )) (or $cvcl_133 AT2_PROC2_TAU )) (or $cvcl_133 AT3_PROC2_B )) (or $cvcl_133 $cvcl_76 )) (or $cvcl_134 AT2_PROC2_C )) (or $cvcl_134 AT2_PROC2_TAU )) (or $cvcl_134 AT3_PROC2_CS )) (or $cvcl_134 (> (- AT2_PROC2_X AT2_Z) 10) )) (or $cvcl_134 $cvcl_179 )) (or $cvcl_135 AT2_PROC2_CS )) (or $cvcl_135 AT2_PROC2_TAU )) (or $cvcl_135 AT3_PROC2_A )) (or $cvcl_135 $cvcl_76 )) (or $cvcl_136 AT3_PROC2_A )) (or $cvcl_136 AT3_PROC2_TAU )) (or $cvcl_136 AT4_PROC2_B )) (or $cvcl_136 $cvcl_78 )) (or $cvcl_137 AT3_PROC2_B )) (or $cvcl_137 AT3_PROC2_TAU )) (or $cvcl_137 AT4_PROC2_C )) (or $cvcl_137 $cvcl_138 )) (or $cvcl_137 $cvcl_78 )) (or $cvcl_139 AT3_PROC2_C )) (or $cvcl_139 AT3_PROC2_TAU )) (or $cvcl_139 AT4_PROC2_B )) (or $cvcl_139 $cvcl_78 )) (or $cvcl_140 AT3_PROC2_C )) (or $cvcl_140 AT3_PROC2_TAU )) (or $cvcl_140 AT4_PROC2_CS )) (or $cvcl_140 (> (- AT3_PROC2_X AT3_Z) 10) )) (or $cvcl_140 $cvcl_181 )) (or $cvcl_141 AT3_PROC2_CS )) (or $cvcl_141 AT3_PROC2_TAU )) (or $cvcl_141 AT4_PROC2_A )) (or $cvcl_141 $cvcl_78 )) (or $cvcl_118 $cvcl_114 )) (or $cvcl_119 $cvcl_114 )) (or $cvcl_121 $cvcl_114 )) (or $cvcl_122 $cvcl_114 )) (or $cvcl_123 $cvcl_114 )) (or $cvcl_124 $cvcl_115 )) (or $cvcl_125 $cvcl_115 )) (or $cvcl_127 $cvcl_115 )) (or $cvcl_128 $cvcl_115 )) (or $cvcl_129 $cvcl_115 )) (or $cvcl_130 $cvcl_116 )) (or $cvcl_131 $cvcl_116 )) (or $cvcl_133 $cvcl_116 )) (or $cvcl_134 $cvcl_116 )) (or $cvcl_135 $cvcl_116 )) (or $cvcl_136 $cvcl_117 )) (or $cvcl_137 $cvcl_117 )) (or $cvcl_139 $cvcl_117 )) (or $cvcl_140 $cvcl_117 )) (or $cvcl_141 $cvcl_117 )) (or $cvcl_142 AT0_PROC3_A )) (or $cvcl_142 AT0_PROC3_TAU )) (or $cvcl_142 AT1_PROC3_B )) (or $cvcl_142 $cvcl_82 )) (or $cvcl_143 AT0_PROC3_B )) (or $cvcl_143 AT0_PROC3_TAU )) (or $cvcl_143 AT1_PROC3_C )) (or $cvcl_143 $cvcl_144 )) (or $cvcl_143 $cvcl_82 )) (or $cvcl_145 AT0_PROC3_C )) (or $cvcl_145 AT0_PROC3_TAU )) (or $cvcl_145 AT1_PROC3_B )) (or $cvcl_145 $cvcl_82 )) (or $cvcl_146 AT0_PROC3_C )) (or $cvcl_146 AT0_PROC3_TAU )) (or $cvcl_146 AT1_PROC3_CS )) (or $cvcl_146 (> (- AT0_PROC3_X AT0_Z) 10) )) (or $cvcl_146 $cvcl_183 )) (or $cvcl_147 AT0_PROC3_CS )) (or $cvcl_147 AT0_PROC3_TAU )) (or $cvcl_147 AT1_PROC3_A )) (or $cvcl_147 $cvcl_82 )) (or $cvcl_148 AT1_PROC3_A )) (or $cvcl_148 AT1_PROC3_TAU )) (or $cvcl_148 AT2_PROC3_B )) (or $cvcl_148 $cvcl_84 )) (or $cvcl_149 AT1_PROC3_B )) (or $cvcl_149 AT1_PROC3_TAU )) (or $cvcl_149 AT2_PROC3_C )) (or $cvcl_149 $cvcl_150 )) (or $cvcl_149 $cvcl_84 )) (or $cvcl_151 AT1_PROC3_C )) (or $cvcl_151 AT1_PROC3_TAU )) (or $cvcl_151 AT2_PROC3_B )) (or $cvcl_151 $cvcl_84 )) (or $cvcl_152 AT1_PROC3_C )) (or $cvcl_152 AT1_PROC3_TAU )) (or $cvcl_152 AT2_PROC3_CS )) (or $cvcl_152 (> (- AT1_PROC3_X AT1_Z) 10) )) (or $cvcl_152 $cvcl_185 )) (or $cvcl_153 AT1_PROC3_CS )) (or $cvcl_153 AT1_PROC3_TAU )) (or $cvcl_153 AT2_PROC3_A )) (or $cvcl_153 $cvcl_84 )) (or $cvcl_154 AT2_PROC3_A )) (or $cvcl_154 AT2_PROC3_TAU )) (or $cvcl_154 AT3_PROC3_B )) (or $cvcl_154 $cvcl_86 )) (or $cvcl_155 AT2_PROC3_B )) (or $cvcl_155 AT2_PROC3_TAU )) (or $cvcl_155 AT3_PROC3_C )) (or $cvcl_155 $cvcl_156 )) (or $cvcl_155 $cvcl_86 )) (or $cvcl_157 AT2_PROC3_C )) (or $cvcl_157 AT2_PROC3_TAU )) (or $cvcl_157 AT3_PROC3_B )) (or $cvcl_157 $cvcl_86 )) (or $cvcl_158 AT2_PROC3_C )) (or $cvcl_158 AT2_PROC3_TAU )) (or $cvcl_158 AT3_PROC3_CS )) (or $cvcl_158 (> (- AT2_PROC3_X AT2_Z) 10) )) (or $cvcl_158 $cvcl_187 )) (or $cvcl_159 AT2_PROC3_CS )) (or $cvcl_159 AT2_PROC3_TAU )) (or $cvcl_159 AT3_PROC3_A )) (or $cvcl_159 $cvcl_86 )) (or $cvcl_160 AT3_PROC3_A )) (or $cvcl_160 AT3_PROC3_TAU )) (or $cvcl_160 AT4_PROC3_B )) (or $cvcl_160 $cvcl_88 )) (or $cvcl_161 AT3_PROC3_B )) (or $cvcl_161 AT3_PROC3_TAU )) (or $cvcl_161 AT4_PROC3_C )) (or $cvcl_161 $cvcl_162 )) (or $cvcl_161 $cvcl_88 )) (or $cvcl_163 AT3_PROC3_C )) (or $cvcl_163 AT3_PROC3_TAU )) (or $cvcl_163 AT4_PROC3_B )) (or $cvcl_163 $cvcl_88 )) (or $cvcl_164 AT3_PROC3_C )) (or $cvcl_164 AT3_PROC3_TAU )) (or $cvcl_164 AT4_PROC3_CS )) (or $cvcl_164 (> (- AT3_PROC3_X AT3_Z) 10) )) (or $cvcl_164 $cvcl_189 )) (or $cvcl_165 AT3_PROC3_CS )) (or $cvcl_165 AT3_PROC3_TAU )) (or $cvcl_165 AT4_PROC3_A )) (or $cvcl_165 $cvcl_88 )) (or $cvcl_142 $cvcl_114 )) (or $cvcl_143 $cvcl_114 )) (or $cvcl_145 $cvcl_114 )) (or $cvcl_146 $cvcl_114 )) (or $cvcl_147 $cvcl_114 )) (or $cvcl_148 $cvcl_115 )) (or $cvcl_149 $cvcl_115 )) (or $cvcl_151 $cvcl_115 )) (or $cvcl_152 $cvcl_115 )) (or $cvcl_153 $cvcl_115 )) (or $cvcl_154 $cvcl_116 )) (or $cvcl_155 $cvcl_116 )) (or $cvcl_157 $cvcl_116 )) (or $cvcl_158 $cvcl_116 )) (or $cvcl_159 $cvcl_116 )) (or $cvcl_160 $cvcl_117 )) (or $cvcl_161 $cvcl_117 )) (or $cvcl_163 $cvcl_117 )) (or $cvcl_164 $cvcl_117 )) (or $cvcl_165 $cvcl_117 )) (or (or $cvcl_166 $cvcl_0 ) AT1_PROC1_A )) (or (or $cvcl_166 AT0_PROC1_A ) $cvcl_4 )) (or (or $cvcl_166 $cvcl_1 ) AT1_PROC1_B )) (or (or $cvcl_166 AT0_PROC1_B ) $cvcl_5 )) (or (or $cvcl_166 $cvcl_2 ) AT1_PROC1_C )) (or (or $cvcl_166 AT0_PROC1_C ) $cvcl_6 )) (or (or $cvcl_166 $cvcl_3 ) AT1_PROC1_CS )) (or (or $cvcl_166 AT0_PROC1_CS ) $cvcl_7 )) (or $cvcl_166 $cvcl_191 )) (or $cvcl_166 $cvcl_167 )) (or $cvcl_166 $cvcl_114 )) (or (or $cvcl_168 $cvcl_4 ) AT2_PROC1_A )) (or (or $cvcl_168 AT1_PROC1_A ) $cvcl_8 )) (or (or $cvcl_168 $cvcl_5 ) AT2_PROC1_B )) (or (or $cvcl_168 AT1_PROC1_B ) $cvcl_9 )) (or (or $cvcl_168 $cvcl_6 ) AT2_PROC1_C )) (or (or $cvcl_168 AT1_PROC1_C ) $cvcl_10 )) (or (or $cvcl_168 $cvcl_7 ) AT2_PROC1_CS )) (or (or $cvcl_168 AT1_PROC1_CS ) $cvcl_11 )) (or $cvcl_168 $cvcl_193 )) (or $cvcl_168 $cvcl_169 )) (or $cvcl_168 $cvcl_115 )) (or (or $cvcl_170 $cvcl_8 ) AT3_PROC1_A )) (or (or $cvcl_170 AT2_PROC1_A ) $cvcl_12 )) (or (or $cvcl_170 $cvcl_9 ) AT3_PROC1_B )) (or (or $cvcl_170 AT2_PROC1_B ) $cvcl_13 )) (or (or $cvcl_170 $cvcl_10 ) AT3_PROC1_C )) (or (or $cvcl_170 AT2_PROC1_C ) $cvcl_14 )) (or (or $cvcl_170 $cvcl_11 ) AT3_PROC1_CS )) (or (or $cvcl_170 AT2_PROC1_CS ) $cvcl_15 )) (or $cvcl_170 $cvcl_195 )) (or $cvcl_170 $cvcl_171 )) (or $cvcl_170 $cvcl_116 )) (or (or $cvcl_172 $cvcl_12 ) AT4_PROC1_A )) (or (or $cvcl_172 AT3_PROC1_A ) $cvcl_16 )) (or (or $cvcl_172 $cvcl_13 ) AT4_PROC1_B )) (or (or $cvcl_172 AT3_PROC1_B ) $cvcl_17 )) (or (or $cvcl_172 $cvcl_14 ) AT4_PROC1_C )) (or (or $cvcl_172 AT3_PROC1_C ) $cvcl_18 )) (or (or $cvcl_172 $cvcl_15 ) AT4_PROC1_CS )) (or (or $cvcl_172 AT3_PROC1_CS ) $cvcl_19 )) (or $cvcl_172 $cvcl_197 )) (or $cvcl_172 $cvcl_173 )) (or $cvcl_172 $cvcl_117 )) (or (or $cvcl_174 $cvcl_20 ) AT1_PROC2_A )) (or (or $cvcl_174 AT0_PROC2_A ) $cvcl_24 )) (or (or $cvcl_174 $cvcl_21 ) AT1_PROC2_B )) (or (or $cvcl_174 AT0_PROC2_B ) $cvcl_25 )) (or (or $cvcl_174 $cvcl_22 ) AT1_PROC2_C )) (or (or $cvcl_174 AT0_PROC2_C ) $cvcl_26 )) (or (or $cvcl_174 $cvcl_23 ) AT1_PROC2_CS )) (or (or $cvcl_174 AT0_PROC2_CS ) $cvcl_27 )) (or $cvcl_174 $cvcl_198 )) (or $cvcl_174 $cvcl_175 )) (or $cvcl_174 $cvcl_114 )) (or (or $cvcl_176 $cvcl_24 ) AT2_PROC2_A )) (or (or $cvcl_176 AT1_PROC2_A ) $cvcl_28 )) (or (or $cvcl_176 $cvcl_25 ) AT2_PROC2_B )) (or (or $cvcl_176 AT1_PROC2_B ) $cvcl_29 )) (or (or $cvcl_176 $cvcl_26 ) AT2_PROC2_C )) (or (or $cvcl_176 AT1_PROC2_C ) $cvcl_30 )) (or (or $cvcl_176 $cvcl_27 ) AT2_PROC2_CS )) (or (or $cvcl_176 AT1_PROC2_CS ) $cvcl_31 )) (or $cvcl_176 $cvcl_200 )) (or $cvcl_176 $cvcl_177 )) (or $cvcl_176 $cvcl_115 )) (or (or $cvcl_178 $cvcl_28 ) AT3_PROC2_A )) (or (or $cvcl_178 AT2_PROC2_A ) $cvcl_32 )) (or (or $cvcl_178 $cvcl_29 ) AT3_PROC2_B )) (or (or $cvcl_178 AT2_PROC2_B ) $cvcl_33 )) (or (or $cvcl_178 $cvcl_30 ) AT3_PROC2_C )) (or (or $cvcl_178 AT2_PROC2_C ) $cvcl_34 )) (or (or $cvcl_178 $cvcl_31 ) AT3_PROC2_CS )) (or (or $cvcl_178 AT2_PROC2_CS ) $cvcl_35 )) (or $cvcl_178 $cvcl_202 )) (or $cvcl_178 $cvcl_179 )) (or $cvcl_178 $cvcl_116 )) (or (or $cvcl_180 $cvcl_32 ) AT4_PROC2_A )) (or (or $cvcl_180 AT3_PROC2_A ) $cvcl_36 )) (or (or $cvcl_180 $cvcl_33 ) AT4_PROC2_B )) (or (or $cvcl_180 AT3_PROC2_B ) $cvcl_37 )) (or (or $cvcl_180 $cvcl_34 ) AT4_PROC2_C )) (or (or $cvcl_180 AT3_PROC2_C ) $cvcl_38 )) (or (or $cvcl_180 $cvcl_35 ) AT4_PROC2_CS )) (or (or $cvcl_180 AT3_PROC2_CS ) $cvcl_39 )) (or $cvcl_180 $cvcl_204 )) (or $cvcl_180 $cvcl_181 )) (or $cvcl_180 $cvcl_117 )) (or (or $cvcl_182 $cvcl_40 ) AT1_PROC3_A )) (or (or $cvcl_182 AT0_PROC3_A ) $cvcl_44 )) (or (or $cvcl_182 $cvcl_41 ) AT1_PROC3_B )) (or (or $cvcl_182 AT0_PROC3_B ) $cvcl_45 )) (or (or $cvcl_182 $cvcl_42 ) AT1_PROC3_C )) (or (or $cvcl_182 AT0_PROC3_C ) $cvcl_46 )) (or (or $cvcl_182 $cvcl_43 ) AT1_PROC3_CS )) (or (or $cvcl_182 AT0_PROC3_CS ) $cvcl_47 )) (or $cvcl_182 $cvcl_206 )) (or $cvcl_182 $cvcl_183 )) (or $cvcl_182 $cvcl_114 )) (or (or $cvcl_184 $cvcl_44 ) AT2_PROC3_A )) (or (or $cvcl_184 AT1_PROC3_A ) $cvcl_48 )) (or (or $cvcl_184 $cvcl_45 ) AT2_PROC3_B )) (or (or $cvcl_184 AT1_PROC3_B ) $cvcl_49 )) (or (or $cvcl_184 $cvcl_46 ) AT2_PROC3_C )) (or (or $cvcl_184 AT1_PROC3_C ) $cvcl_50 )) (or (or $cvcl_184 $cvcl_47 ) AT2_PROC3_CS )) (or (or $cvcl_184 AT1_PROC3_CS ) $cvcl_51 )) (or $cvcl_184 $cvcl_207 )) (or $cvcl_184 $cvcl_185 )) (or $cvcl_184 $cvcl_115 )) (or (or $cvcl_186 $cvcl_48 ) AT3_PROC3_A )) (or (or $cvcl_186 AT2_PROC3_A ) $cvcl_52 )) (or (or $cvcl_186 $cvcl_49 ) AT3_PROC3_B )) (or (or $cvcl_186 AT2_PROC3_B ) $cvcl_53 )) (or (or $cvcl_186 $cvcl_50 ) AT3_PROC3_C )) (or (or $cvcl_186 AT2_PROC3_C ) $cvcl_54 )) (or (or $cvcl_186 $cvcl_51 ) AT3_PROC3_CS )) (or (or $cvcl_186 AT2_PROC3_CS ) $cvcl_55 )) (or $cvcl_186 $cvcl_208 )) (or $cvcl_186 $cvcl_187 )) (or $cvcl_186 $cvcl_116 )) (or (or $cvcl_188 $cvcl_52 ) AT4_PROC3_A )) (or (or $cvcl_188 AT3_PROC3_A ) $cvcl_56 )) (or (or $cvcl_188 $cvcl_53 ) AT4_PROC3_B )) (or (or $cvcl_188 AT3_PROC3_B ) $cvcl_57 )) (or (or $cvcl_188 $cvcl_54 ) AT4_PROC3_C )) (or (or $cvcl_188 AT3_PROC3_C ) $cvcl_58 )) (or (or $cvcl_188 $cvcl_55 ) AT4_PROC3_CS )) (or (or $cvcl_188 AT3_PROC3_CS ) $cvcl_59 )) (or $cvcl_188 $cvcl_209 )) (or $cvcl_188 $cvcl_189 )) (or $cvcl_188 $cvcl_117 )) (or (or $cvcl_190 $cvcl_0 ) AT1_PROC1_A )) (or (or $cvcl_190 AT0_PROC1_A ) $cvcl_4 )) (or (or $cvcl_190 $cvcl_1 ) AT1_PROC1_B )) (or (or $cvcl_190 AT0_PROC1_B ) $cvcl_5 )) (or (or $cvcl_190 $cvcl_2 ) AT1_PROC1_C )) (or (or $cvcl_190 AT0_PROC1_C ) $cvcl_6 )) (or (or $cvcl_190 $cvcl_3 ) AT1_PROC1_CS )) (or (or $cvcl_190 AT0_PROC1_CS ) $cvcl_7 )) (or $cvcl_190 $cvcl_167 )) (or $cvcl_190 $cvcl_191 )) $cvcl_199) (or (or $cvcl_192 $cvcl_4 ) AT2_PROC1_A )) (or (or $cvcl_192 AT1_PROC1_A ) $cvcl_8 )) (or (or $cvcl_192 $cvcl_5 ) AT2_PROC1_B )) (or (or $cvcl_192 AT1_PROC1_B ) $cvcl_9 )) (or (or $cvcl_192 $cvcl_6 ) AT2_PROC1_C )) (or (or $cvcl_192 AT1_PROC1_C ) $cvcl_10 )) (or (or $cvcl_192 $cvcl_7 ) AT2_PROC1_CS )) (or (or $cvcl_192 AT1_PROC1_CS ) $cvcl_11 )) (or $cvcl_192 $cvcl_169 )) (or $cvcl_192 $cvcl_193 )) $cvcl_201) (or (or $cvcl_194 $cvcl_8 ) AT3_PROC1_A )) (or (or $cvcl_194 AT2_PROC1_A ) $cvcl_12 )) (or (or $cvcl_194 $cvcl_9 ) AT3_PROC1_B )) (or (or $cvcl_194 AT2_PROC1_B ) $cvcl_13 )) (or (or $cvcl_194 $cvcl_10 ) AT3_PROC1_C )) (or (or $cvcl_194 AT2_PROC1_C ) $cvcl_14 )) (or (or $cvcl_194 $cvcl_11 ) AT3_PROC1_CS )) (or (or $cvcl_194 AT2_PROC1_CS ) $cvcl_15 )) (or $cvcl_194 $cvcl_171 )) (or $cvcl_194 $cvcl_195 )) $cvcl_203) (or (or $cvcl_196 $cvcl_12 ) AT4_PROC1_A )) (or (or $cvcl_196 AT3_PROC1_A ) $cvcl_16 )) (or (or $cvcl_196 $cvcl_13 ) AT4_PROC1_B )) (or (or $cvcl_196 AT3_PROC1_B ) $cvcl_17 )) (or (or $cvcl_196 $cvcl_14 ) AT4_PROC1_C )) (or (or $cvcl_196 AT3_PROC1_C ) $cvcl_18 )) (or (or $cvcl_196 $cvcl_15 ) AT4_PROC1_CS )) (or (or $cvcl_196 AT3_PROC1_CS ) $cvcl_19 )) (or $cvcl_196 $cvcl_173 )) (or $cvcl_196 $cvcl_197 )) $cvcl_205) (or (or $cvcl_190 $cvcl_20 ) AT1_PROC2_A )) (or (or $cvcl_190 AT0_PROC2_A ) $cvcl_24 )) (or (or $cvcl_190 $cvcl_21 ) AT1_PROC2_B )) (or (or $cvcl_190 AT0_PROC2_B ) $cvcl_25 )) (or (or $cvcl_190 $cvcl_22 ) AT1_PROC2_C )) (or (or $cvcl_190 AT0_PROC2_C ) $cvcl_26 )) (or (or $cvcl_190 $cvcl_23 ) AT1_PROC2_CS )) (or (or $cvcl_190 AT0_PROC2_CS ) $cvcl_27 )) (or $cvcl_190 $cvcl_175 )) (or $cvcl_190 $cvcl_198 )) $cvcl_199) (or (or $cvcl_192 $cvcl_24 ) AT2_PROC2_A )) (or (or $cvcl_192 AT1_PROC2_A ) $cvcl_28 )) (or (or $cvcl_192 $cvcl_25 ) AT2_PROC2_B )) (or (or $cvcl_192 AT1_PROC2_B ) $cvcl_29 )) (or (or $cvcl_192 $cvcl_26 ) AT2_PROC2_C )) (or (or $cvcl_192 AT1_PROC2_C ) $cvcl_30 )) (or (or $cvcl_192 $cvcl_27 ) AT2_PROC2_CS )) (or (or $cvcl_192 AT1_PROC2_CS ) $cvcl_31 )) (or $cvcl_192 $cvcl_177 )) (or $cvcl_192 $cvcl_200 )) $cvcl_201) (or (or $cvcl_194 $cvcl_28 ) AT3_PROC2_A )) (or (or $cvcl_194 AT2_PROC2_A ) $cvcl_32 )) (or (or $cvcl_194 $cvcl_29 ) AT3_PROC2_B )) (or (or $cvcl_194 AT2_PROC2_B ) $cvcl_33 )) (or (or $cvcl_194 $cvcl_30 ) AT3_PROC2_C )) (or (or $cvcl_194 AT2_PROC2_C ) $cvcl_34 )) (or (or $cvcl_194 $cvcl_31 ) AT3_PROC2_CS )) (or (or $cvcl_194 AT2_PROC2_CS ) $cvcl_35 )) (or $cvcl_194 $cvcl_179 )) (or $cvcl_194 $cvcl_202 )) $cvcl_203) (or (or $cvcl_196 $cvcl_32 ) AT4_PROC2_A )) (or (or $cvcl_196 AT3_PROC2_A ) $cvcl_36 )) (or (or $cvcl_196 $cvcl_33 ) AT4_PROC2_B )) (or (or $cvcl_196 AT3_PROC2_B ) $cvcl_37 )) (or (or $cvcl_196 $cvcl_34 ) AT4_PROC2_C )) (or (or $cvcl_196 AT3_PROC2_C ) $cvcl_38 )) (or (or $cvcl_196 $cvcl_35 ) AT4_PROC2_CS )) (or (or $cvcl_196 AT3_PROC2_CS ) $cvcl_39 )) (or $cvcl_196 $cvcl_181 )) (or $cvcl_196 $cvcl_204 )) $cvcl_205) (or (or $cvcl_190 $cvcl_40 ) AT1_PROC3_A )) (or (or $cvcl_190 AT0_PROC3_A ) $cvcl_44 )) (or (or $cvcl_190 $cvcl_41 ) AT1_PROC3_B )) (or (or $cvcl_190 AT0_PROC3_B ) $cvcl_45 )) (or (or $cvcl_190 $cvcl_42 ) AT1_PROC3_C )) (or (or $cvcl_190 AT0_PROC3_C ) $cvcl_46 )) (or (or $cvcl_190 $cvcl_43 ) AT1_PROC3_CS )) (or (or $cvcl_190 AT0_PROC3_CS ) $cvcl_47 )) (or $cvcl_190 $cvcl_183 )) (or $cvcl_190 $cvcl_206 )) $cvcl_199) (or (or $cvcl_192 $cvcl_44 ) AT2_PROC3_A )) (or (or $cvcl_192 AT1_PROC3_A ) $cvcl_48 )) (or (or $cvcl_192 $cvcl_45 ) AT2_PROC3_B )) (or (or $cvcl_192 AT1_PROC3_B ) $cvcl_49 )) (or (or $cvcl_192 $cvcl_46 ) AT2_PROC3_C )) (or (or $cvcl_192 AT1_PROC3_C ) $cvcl_50 )) (or (or $cvcl_192 $cvcl_47 ) AT2_PROC3_CS )) (or (or $cvcl_192 AT1_PROC3_CS ) $cvcl_51 )) (or $cvcl_192 $cvcl_185 )) (or $cvcl_192 $cvcl_207 )) $cvcl_201) (or (or $cvcl_194 $cvcl_48 ) AT3_PROC3_A )) (or (or $cvcl_194 AT2_PROC3_A ) $cvcl_52 )) (or (or $cvcl_194 $cvcl_49 ) AT3_PROC3_B )) (or (or $cvcl_194 AT2_PROC3_B ) $cvcl_53 )) (or (or $cvcl_194 $cvcl_50 ) AT3_PROC3_C )) (or (or $cvcl_194 AT2_PROC3_C ) $cvcl_54 )) (or (or $cvcl_194 $cvcl_51 ) AT3_PROC3_CS )) (or (or $cvcl_194 AT2_PROC3_CS ) $cvcl_55 )) (or $cvcl_194 $cvcl_187 )) (or $cvcl_194 $cvcl_208 )) $cvcl_203) (or (or $cvcl_196 $cvcl_52 ) AT4_PROC3_A )) (or (or $cvcl_196 AT3_PROC3_A ) $cvcl_56 )) (or (or $cvcl_196 $cvcl_53 ) AT4_PROC3_B )) (or (or $cvcl_196 AT3_PROC3_B ) $cvcl_57 )) (or (or $cvcl_196 $cvcl_54 ) AT4_PROC3_C )) (or (or $cvcl_196 AT3_PROC3_C ) $cvcl_58 )) (or (or $cvcl_196 $cvcl_55 ) AT4_PROC3_CS )) (or (or $cvcl_196 AT3_PROC3_CS ) $cvcl_59 )) (or $cvcl_196 $cvcl_189 )) (or $cvcl_196 $cvcl_209 )) $cvcl_205) (or $cvcl_167 $cvcl_210 )) (or $cvcl_226 (not $cvcl_210) )) (or $cvcl_169 $cvcl_211 )) (or $cvcl_232 (not $cvcl_211) )) (or $cvcl_171 $cvcl_212 )) (or $cvcl_238 (not $cvcl_212) )) (or $cvcl_173 $cvcl_213 )) (or $cvcl_244 (not $cvcl_213) )) (or $cvcl_175 $cvcl_214 )) (or $cvcl_250 (not $cvcl_214) )) (or $cvcl_177 $cvcl_215 )) (or $cvcl_254 (not $cvcl_215) )) (or $cvcl_179 $cvcl_216 )) (or $cvcl_258 (not $cvcl_216) )) (or $cvcl_181 $cvcl_217 )) (or $cvcl_262 (not $cvcl_217) )) (or $cvcl_183 $cvcl_218 )) (or $cvcl_266 (not $cvcl_218) )) (or $cvcl_185 $cvcl_219 )) (or $cvcl_270 (not $cvcl_219) )) (or $cvcl_187 $cvcl_220 )) (or $cvcl_274 (not $cvcl_220) )) (or $cvcl_189 $cvcl_221 )) (or $cvcl_278 (not $cvcl_221) )) (or $cvcl_190 $cvcl_192 )) (or $cvcl_192 $cvcl_194 )) (or $cvcl_194 $cvcl_196 )) (or $cvcl_114 $cvcl_222 )) (or $cvcl_227 $cvcl_231 )) (or $cvcl_115 $cvcl_223 )) (or $cvcl_233 $cvcl_237 )) (or $cvcl_116 $cvcl_224 )) (or $cvcl_239 $cvcl_243 )) (or $cvcl_117 $cvcl_225 )) (or $cvcl_245 $cvcl_249 )) (or (or (or $cvcl_60 $cvcl_226 ) $cvcl_227 ) $cvcl_228 )) (or (or (or $cvcl_229 $cvcl_167 ) $cvcl_227 ) $cvcl_228 )) (or (or $cvcl_230 $cvcl_114 ) $cvcl_228 )) (or (or $cvcl_230 $cvcl_227 ) $cvcl_62 )) (or (or (or (not (< AT0_Z AT0_PROC1_X)) $cvcl_226 ) $cvcl_231 ) $cvcl_236 )) (or (or (or $cvcl_62 $cvcl_232 ) $cvcl_233 ) $cvcl_234 )) (or (or (or $cvcl_228 $cvcl_169 ) $cvcl_233 ) $cvcl_234 )) (or (or $cvcl_235 $cvcl_115 ) $cvcl_234 )) (or (or $cvcl_235 $cvcl_233 ) $cvcl_64 )) (or (or (or (not $cvcl_236) $cvcl_232 ) $cvcl_237 ) $cvcl_242 )) (or (or (or $cvcl_64 $cvcl_238 ) $cvcl_239 ) $cvcl_240 )) (or (or (or $cvcl_234 $cvcl_171 ) $cvcl_239 ) $cvcl_240 )) (or (or $cvcl_241 $cvcl_116 ) $cvcl_240 )) (or (or $cvcl_241 $cvcl_239 ) $cvcl_66 )) (or (or (or (not $cvcl_242) $cvcl_238 ) $cvcl_243 ) $cvcl_248 )) (or (or (or $cvcl_66 $cvcl_244 ) $cvcl_245 ) $cvcl_246 )) (or (or (or $cvcl_240 $cvcl_173 ) $cvcl_245 ) $cvcl_246 )) (or (or $cvcl_247 $cvcl_117 ) $cvcl_246 )) (or (or $cvcl_247 $cvcl_245 ) $cvcl_68 )) (or (or (or (not $cvcl_248) $cvcl_244 ) $cvcl_249 ) (< AT4_Z AT4_PROC1_X) )) (or (or (or $cvcl_70 $cvcl_250 ) $cvcl_227 ) $cvcl_251 )) (or (or (or $cvcl_252 $cvcl_175 ) $cvcl_227 ) $cvcl_251 )) (or (or $cvcl_253 $cvcl_114 ) $cvcl_251 )) (or (or $cvcl_253 $cvcl_227 ) $cvcl_72 )) (or (or (or (not (< AT0_Z AT0_PROC2_X)) $cvcl_250 ) $cvcl_231 ) $cvcl_257 )) (or (or (or $cvcl_72 $cvcl_254 ) $cvcl_233 ) $cvcl_255 )) (or (or (or $cvcl_251 $cvcl_177 ) $cvcl_233 ) $cvcl_255 )) (or (or $cvcl_256 $cvcl_115 ) $cvcl_255 )) (or (or $cvcl_256 $cvcl_233 ) $cvcl_74 )) (or (or (or (not $cvcl_257) $cvcl_254 ) $cvcl_237 ) $cvcl_261 )) (or (or (or $cvcl_74 $cvcl_258 ) $cvcl_239 ) $cvcl_259 )) (or (or (or $cvcl_255 $cvcl_179 ) $cvcl_239 ) $cvcl_259 )) (or (or $cvcl_260 $cvcl_116 ) $cvcl_259 )) (or (or $cvcl_260 $cvcl_239 ) $cvcl_76 )) (or (or (or (not $cvcl_261) $cvcl_258 ) $cvcl_243 ) $cvcl_265 )) (or (or (or $cvcl_76 $cvcl_262 ) $cvcl_245 ) $cvcl_263 )) (or (or (or $cvcl_259 $cvcl_181 ) $cvcl_245 ) $cvcl_263 )) (or (or $cvcl_264 $cvcl_117 ) $cvcl_263 )) (or (or $cvcl_264 $cvcl_245 ) $cvcl_78 )) (or (or (or (not $cvcl_265) $cvcl_262 ) $cvcl_249 ) (< AT4_Z AT4_PROC2_X) )) (or (or (or $cvcl_80 $cvcl_266 ) $cvcl_227 ) $cvcl_267 )) (or (or (or $cvcl_268 $cvcl_183 ) $cvcl_227 ) $cvcl_267 )) (or (or $cvcl_269 $cvcl_114 ) $cvcl_267 )) (or (or $cvcl_269 $cvcl_227 ) $cvcl_82 )) (or (or (or (not (< AT0_Z AT0_PROC3_X)) $cvcl_266 ) $cvcl_231 ) $cvcl_273 )) (or (or (or $cvcl_82 $cvcl_270 ) $cvcl_233 ) $cvcl_271 )) (or (or (or $cvcl_267 $cvcl_185 ) $cvcl_233 ) $cvcl_271 )) (or (or $cvcl_272 $cvcl_115 ) $cvcl_271 )) (or (or $cvcl_272 $cvcl_233 ) $cvcl_84 )) (or (or (or (not $cvcl_273) $cvcl_270 ) $cvcl_237 ) $cvcl_277 )) (or (or (or $cvcl_84 $cvcl_274 ) $cvcl_239 ) $cvcl_275 )) (or (or (or $cvcl_271 $cvcl_187 ) $cvcl_239 ) $cvcl_275 )) (or (or $cvcl_276 $cvcl_116 ) $cvcl_275 )) (or (or $cvcl_276 $cvcl_239 ) $cvcl_86 )) (or (or (or (not $cvcl_277) $cvcl_274 ) $cvcl_243 ) $cvcl_281 )) (or (or (or $cvcl_86 $cvcl_278 ) $cvcl_245 ) $cvcl_279 )) (or (or (or $cvcl_275 $cvcl_189 ) $cvcl_245 ) $cvcl_279 )) (or (or $cvcl_280 $cvcl_117 ) $cvcl_279 )) (or (or $cvcl_280 $cvcl_245 ) $cvcl_88 )) (or (or (or (not $cvcl_281) $cvcl_278 ) $cvcl_249 ) (< AT4_Z AT4_PROC3_X) )) AT0_PROC1_A) AT0_PROC2_A) AT0_PROC3_A) $cvcl_60) $cvcl_70) $cvcl_80) AT0_ID0) (or (or $cvcl_166 $cvcl_174 ) $cvcl_182 )) (or (or $cvcl_168 $cvcl_176 ) $cvcl_184 )) (or (or $cvcl_170 $cvcl_178 ) $cvcl_186 )) (or (or $cvcl_172 $cvcl_180 ) $cvcl_188 )) (or $cvcl_282 $cvcl_283 )) (or $cvcl_282 $cvcl_284 )) (or $cvcl_282 $cvcl_285 )) (or $cvcl_283 $cvcl_284 )) (or $cvcl_283 $cvcl_285 )) (or $cvcl_284 $cvcl_285 )) (or $cvcl_286 $cvcl_287 )) (or $cvcl_286 $cvcl_288 )) (or $cvcl_286 $cvcl_289 )) (or $cvcl_287 $cvcl_288 )) (or $cvcl_287 $cvcl_289 )) (or $cvcl_288 $cvcl_289 )) (or $cvcl_290 $cvcl_291 )) (or $cvcl_290 $cvcl_292 )) (or $cvcl_290 $cvcl_293 )) (or $cvcl_291 $cvcl_292 )) (or $cvcl_291 $cvcl_293 )) (or $cvcl_292 $cvcl_293 )) (or $cvcl_294 $cvcl_295 )) (or $cvcl_294 $cvcl_296 )) (or $cvcl_294 $cvcl_297 )) (or $cvcl_295 $cvcl_296 )) (or $cvcl_295 $cvcl_297 )) (or $cvcl_296 $cvcl_297 )) (or $cvcl_298 $cvcl_299 )) (or $cvcl_298 $cvcl_300 )) (or $cvcl_298 $cvcl_301 )) (or $cvcl_299 $cvcl_300 )) (or $cvcl_299 $cvcl_301 )) (or $cvcl_300 $cvcl_301 )) (or $cvcl_90 AT0_ID0 )) (or $cvcl_90 AT1_ID0 )) (or $cvcl_91 AT1_ID1 )) (or $cvcl_93 AT0_ID0 )) (or $cvcl_93 AT1_ID0 )) (or $cvcl_94 AT0_ID1 )) (or $cvcl_94 AT1_ID1 )) (or $cvcl_95 AT1_ID0 )) (or (or $cvcl_190 $cvcl_283 ) AT1_ID1 )) (or $cvcl_118 AT0_ID0 )) (or $cvcl_118 AT1_ID0 )) (or $cvcl_119 AT1_ID2 )) (or $cvcl_121 AT0_ID0 )) (or $cvcl_121 AT1_ID0 )) (or $cvcl_122 AT0_ID2 )) (or $cvcl_122 AT1_ID2 )) (or $cvcl_123 AT1_ID0 )) (or (or $cvcl_190 $cvcl_284 ) AT1_ID2 )) (or $cvcl_142 AT0_ID0 )) (or $cvcl_142 AT1_ID0 )) (or $cvcl_143 AT1_ID3 )) (or $cvcl_145 AT0_ID0 )) (or $cvcl_145 AT1_ID0 )) (or $cvcl_146 AT0_ID3 )) (or $cvcl_146 AT1_ID3 )) (or $cvcl_147 AT1_ID0 )) (or (or $cvcl_190 $cvcl_285 ) AT1_ID3 )) (or (or $cvcl_190 $cvcl_282 ) AT1_ID0 )) (or $cvcl_96 AT1_ID0 )) (or $cvcl_96 AT2_ID0 )) (or $cvcl_97 AT2_ID1 )) (or $cvcl_99 AT1_ID0 )) (or $cvcl_99 AT2_ID0 )) (or $cvcl_100 AT1_ID1 )) (or $cvcl_100 AT2_ID1 )) (or $cvcl_101 AT2_ID0 )) (or (or $cvcl_192 $cvcl_287 ) AT2_ID1 )) (or $cvcl_124 AT1_ID0 )) (or $cvcl_124 AT2_ID0 )) (or $cvcl_125 AT2_ID2 )) (or $cvcl_127 AT1_ID0 )) (or $cvcl_127 AT2_ID0 )) (or $cvcl_128 AT1_ID2 )) (or $cvcl_128 AT2_ID2 )) (or $cvcl_129 AT2_ID0 )) (or (or $cvcl_192 $cvcl_288 ) AT2_ID2 )) (or $cvcl_148 AT1_ID0 )) (or $cvcl_148 AT2_ID0 )) (or $cvcl_149 AT2_ID3 )) (or $cvcl_151 AT1_ID0 )) (or $cvcl_151 AT2_ID0 )) (or $cvcl_152 AT1_ID3 )) (or $cvcl_152 AT2_ID3 )) (or $cvcl_153 AT2_ID0 )) (or (or $cvcl_192 $cvcl_289 ) AT2_ID3 )) (or (or $cvcl_192 $cvcl_286 ) AT2_ID0 )) (or $cvcl_102 AT2_ID0 )) (or $cvcl_102 AT3_ID0 )) (or $cvcl_103 AT3_ID1 )) (or $cvcl_105 AT2_ID0 )) (or $cvcl_105 AT3_ID0 )) (or $cvcl_106 AT2_ID1 )) (or $cvcl_106 AT3_ID1 )) (or $cvcl_107 AT3_ID0 )) (or (or $cvcl_194 $cvcl_291 ) AT3_ID1 )) (or $cvcl_130 AT2_ID0 )) (or $cvcl_130 AT3_ID0 )) (or $cvcl_131 AT3_ID2 )) (or $cvcl_133 AT2_ID0 )) (or $cvcl_133 AT3_ID0 )) (or $cvcl_134 AT2_ID2 )) (or $cvcl_134 AT3_ID2 )) (or $cvcl_135 AT3_ID0 )) (or (or $cvcl_194 $cvcl_292 ) AT3_ID2 )) (or $cvcl_154 AT2_ID0 )) (or $cvcl_154 AT3_ID0 )) (or $cvcl_155 AT3_ID3 )) (or $cvcl_157 AT2_ID0 )) (or $cvcl_157 AT3_ID0 )) (or $cvcl_158 AT2_ID3 )) (or $cvcl_158 AT3_ID3 )) (or $cvcl_159 AT3_ID0 )) (or (or $cvcl_194 $cvcl_293 ) AT3_ID3 )) (or (or $cvcl_194 $cvcl_290 ) AT3_ID0 )) (or $cvcl_108 AT3_ID0 )) (or $cvcl_108 AT4_ID0 )) (or $cvcl_109 AT4_ID1 )) (or $cvcl_111 AT3_ID0 )) (or $cvcl_111 AT4_ID0 )) (or $cvcl_112 AT3_ID1 )) (or $cvcl_112 AT4_ID1 )) (or $cvcl_113 AT4_ID0 )) (or (or $cvcl_196 $cvcl_295 ) AT4_ID1 )) (or $cvcl_136 AT3_ID0 )) (or $cvcl_136 AT4_ID0 )) (or $cvcl_137 AT4_ID2 )) (or $cvcl_139 AT3_ID0 )) (or $cvcl_139 AT4_ID0 )) (or $cvcl_140 AT3_ID2 )) (or $cvcl_140 AT4_ID2 )) (or $cvcl_141 AT4_ID0 )) (or (or $cvcl_196 $cvcl_296 ) AT4_ID2 )) (or $cvcl_160 AT3_ID0 )) (or $cvcl_160 AT4_ID0 )) (or $cvcl_161 AT4_ID3 )) (or $cvcl_163 AT3_ID0 )) (or $cvcl_163 AT4_ID0 )) (or $cvcl_164 AT3_ID3 )) (or $cvcl_164 AT4_ID3 )) (or $cvcl_165 AT4_ID0 )) (or (or $cvcl_196 $cvcl_297 ) AT4_ID3 )) (or (or $cvcl_196 $cvcl_294 ) AT4_ID0 )) AT4_PROC1_C) AT4_PROC2_C) AT4_PROC3_C)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
201	)

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format