source: vis_dev/cusp-1.1/examples/FISCHER3-4-ninc/FISCHER3-4-ninc.smt @ 74

Last change on this file since 74 was 12, checked in by cecile, 13 years ago

cusp added
  • Property svn:executable set to *
File size: 57.1 KB
RevLine 
[12]1(benchmark FISCHER3_4_ninc.smt
2  :source {
3Source unknown
4This benchmark was automatically translated into SMT-LIB format from
5CVC 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.