(benchmark FISCHER11_1_fair.smt :source { Older mathsat benchmarks. Contact Mathsat group at http://mathsat.itc.it/ for more information. This benchmark was automatically translated into SMT-LIB format from CVC format using CVC Lite } :status unknown :logic QF_LIA :extrapreds ((AT0_PROC3_CS)) :extrafuns ((AT1_PROC5_X Int)) :extrapreds ((AT0_PROC7_SW_A_B_TAU)) :extrapreds ((AT0_PROC6_SW_B_C_TAU)) :extrapreds ((AT1_PROC5_CS)) :extrapreds ((AT0_PROC10_SW_C_B_TAU)) :extrafuns ((AT0_PROC1_X Int)) :extrapreds ((AT0_PROC10_CS)) :extrapreds ((AT0_PROC6_C)) :extrapreds ((AT0_PROC6_B)) :extrapreds ((AT0_PROC7_SW_CS_A_TAU)) :extrapreds ((AT0_PROC6_A)) :extrapreds ((AT0_ID0)) :extrapreds ((AT1_PROC11_C)) :extrapreds ((AT1_PROC2_C)) :extrapreds ((AT0_ID10)) :extrapreds ((AT0_ID1)) :extrapreds ((AT1_PROC11_B)) :extrapreds ((AT1_PROC2_B)) :extrapreds ((AT0_ID11)) :extrapreds ((AT0_ID2)) :extrapreds ((AT1_PROC11_A)) :extrapreds ((AT0_PROC6_CS)) :extrapreds ((AT1_PROC2_A)) :extrapreds ((AT0_ID3)) :extrapreds ((AT0_PROC3_SW_CS_A_TAU)) :extrapreds ((AT0_ID4)) :extrapreds ((AT0_PROC10_WAIT)) :extrapreds ((AT0_ID5)) :extrafuns ((AT1_PROC8_X Int)) :extrapreds ((AT1_PROC2_CS)) :extrapreds ((AT0_ID6)) :extrapreds ((AT0_ID7)) :extrapreds ((AT0_ID8)) :extrapreds ((AT0_ID9)) :extrafuns ((AT0_PROC4_X Int)) :extrapreds ((AT0_PROC9_C)) :extrapreds ((AT0_PROC3_TAU)) :extrapreds ((AT0_PROC7_SW_B_C_TAU)) :extrapreds ((AT0_PROC9_B)) :extrapreds ((AT0_PROC6_SW_A_B_TAU)) :extrapreds ((AT0_PROC9_A)) :extrapreds ((AT0_PROC9_CS)) :extrapreds ((AT1_PROC5_C)) :extrapreds ((AT0_PROC2_SW_C_B_TAU)) :extrapreds ((AT1_PROC10_CS)) :extrapreds ((AT1_PROC5_B)) :extrapreds ((AT0_PROC7_TAU)) :extrapreds ((AT1_PROC5_A)) :extrapreds ((AT0_PROC4_SW_C_B_TAU)) :extrapreds ((AT0_PROC8_SW_A_B_TAU)) :extrapreds ((AT0_PROC1_C)) :extrapreds ((AT0_PROC1_B)) :extrapreds ((AT0_PROC9_WAIT)) :extrapreds ((AT0_PROC1_A)) :extrapreds ((AT0_PROC11_SW_C_B_TAU)) :extrapreds ((AT1_PROC9_CS)) :extrafuns ((AT0_PROC7_X Int)) :extrapreds ((AT0_PROC6_WAIT)) :extrafuns ((AT1_PROC3_X Int)) :extrapreds ((AT1_PROC8_C)) :extrapreds ((AT0_PROC10_SW_A_B_TAU)) :extrapreds ((AT1_PROC8_B)) :extrapreds ((AT1_PROC8_A)) :extrapreds ((AT0_PROC3_WAIT)) :extrapreds ((AT0_PROC2_CS)) :extrapreds ((AT0_PROC4_C)) :extrapreds ((AT0_PROC4_B)) :extrapreds ((AT1_ID0)) :extrapreds ((AT0_PROC11_A)) :extrapreds ((AT1_PROC6_CS)) :extrapreds ((AT0_PROC4_A)) :extrapreds ((AT1_ID1)) :extrapreds ((AT0_PROC11_B)) :extrapreds ((AT1_ID2)) :extrapreds ((AT0_PROC11_C)) :extrapreds ((AT1_ID3)) :extrapreds ((AT0_PROC8_SW_B_C_TAU)) :extrapreds ((AT1_ID4)) :extrapreds ((AT1_ID5)) :extrapreds ((AT1_ID6)) :extrapreds ((AT0_PROC1_SW_CS_A_TAU)) :extrafuns ((AT1_PROC6_X Int)) :extrapreds ((AT1_ID7)) :extrapreds ((AT1_ID8)) :extrapreds ((AT0_PROC5_SW_C_B_TAU)) :extrapreds ((AT0_PROC5_CS)) :extrapreds ((AT1_ID10)) :extrapreds ((AT1_ID9)) :extrapreds ((AT0_PROC6_SW_C_B_TAU)) :extrapreds ((AT1_ID11)) :extrapreds ((AT0_PROC10_SW_C_CS_TAU)) :extrapreds ((AT0_PROC5_SW_CS_A_TAU)) :extrapreds ((AT0_PROC4_TAU)) :extrafuns ((AT0_PROC2_X Int)) :extrapreds ((AT0_PROC7_C)) :extrapreds ((AT1_PROC3_CS)) :extrapreds ((AT0_PROC11_WAIT)) :extrapreds ((AT0_PROC10_SW_B_C_TAU)) :extrapreds ((AT0_PROC7_B)) :extrapreds ((AT0_PROC4_SW_A_B_TAU)) :extrapreds ((AT0_PROC7_A)) :extrapreds ((AT0_PROC9_SW_CS_A_TAU)) :extrapreds ((AT0_PROC9_SW_B_C_TAU)) :extrapreds ((AT1_PROC3_C)) :extrapreds ((AT0_PROC8_TAU)) :extrapreds ((AT1_PROC3_B)) :extrapreds ((AT1_PROC3_A)) :extrapreds ((AT0_PROC11_SW_A_B_TAU)) :extrafuns ((AT1_PROC9_X Int)) :extrapreds ((AT0_PROC8_CS)) :extrafuns ((AT0_PROC11_X Int)) :extrafuns ((AT0_PROC5_X Int)) :extrafuns ((AT1_PROC10_X Int)) :extrafuns ((AT1_PROC1_X Int)) :extrapreds ((AT1_PROC6_C)) :extrapreds ((AT1_PROC6_B)) :extrapreds ((AT0_PROC6_SW_C_CS_TAU)) :extrafuns ((AT1_Z Int)) :extrapreds ((AT1_PROC6_A)) :extrapreds ((AT0_PROC4_SW_B_C_TAU)) :extrapreds ((AT0_PROC10_TAU)) :extrapreds ((AT0_PROC9_SW_A_B_TAU)) :extrapreds ((AT0_PROC2_C)) :extrapreds ((AT0_PROC7_WAIT)) :extrapreds ((AT0_PROC2_SW_C_CS_TAU)) :extrapreds ((AT0_PROC2_B)) :extrapreds ((AT0_PROC2_A)) :extrapreds ((AT0_PROC3_SW_B_C_TAU)) :extrapreds ((AT0_PROC1_SW_C_B_TAU)) :extrapreds ((AT0_PROC1_CS)) :extrapreds ((AT0_PROC11_SW_B_C_TAU)) :extrafuns ((AT0_PROC8_X Int)) :extrapreds ((AT0_PROC5_SW_A_B_TAU)) :extrapreds ((AT0_PROC4_WAIT)) :extrapreds ((AT1_PROC7_CS)) :extrapreds ((AT0_PROC1_TAU)) :extrapreds ((AT0_PROC1_SW_C_CS_TAU)) :extrafuns ((AT1_PROC4_X Int)) :extrapreds ((AT1_PROC9_C)) :extrapreds ((AT0_PROC11_SW_C_CS_TAU)) :extrapreds ((AT0_PROC4_SW_CS_A_TAU)) :extrapreds ((AT1_PROC9_B)) :extrapreds ((AT1_PROC9_A)) :extrapreds ((AT0_PROC1_WAIT)) :extrapreds ((AT0_PROC5_TAU)) :extrapreds ((AT0_PROC10_SW_CS_A_TAU)) :extrapreds ((AT0_PROC5_SW_C_CS_TAU)) :extrapreds ((AT0_PROC8_SW_CS_A_TAU)) :extrapreds ((AT0_PROC5_C)) :extrapreds ((AT0_PROC5_B)) :extrapreds ((AT0_PROC10_A)) :extrapreds ((AT0_PROC5_A)) :extrapreds ((AT0_PROC4_CS)) :extrapreds ((AT0_PROC9_TAU)) :extrapreds ((AT0_PROC9_SW_C_CS_TAU)) :extrapreds ((AT1_PROC10_C)) :extrapreds ((AT0_PROC10_B)) :extrapreds ((AT1_PROC1_C)) :extrapreds ((AT1_PROC10_B)) :extrapreds ((AT0_PROC10_C)) :extrapreds ((AT1_PROC1_B)) :extrapreds ((AT1_PROC10_A)) :extrapreds ((AT1_PROC4_CS)) :extrapreds ((AT1_PROC1_A)) :extrafuns ((AT1_PROC7_X Int)) :extrapreds ((AT0_PROC11_CS)) :extrapreds ((AT0_PROC3_SW_A_B_TAU)) :extrapreds ((AT0_DELTA)) :extrapreds ((AT0_PROC5_SW_B_C_TAU)) :extrapreds ((AT0_PROC7_SW_C_B_TAU)) :extrafuns ((AT0_PROC3_X Int)) :extrapreds ((AT0_PROC8_C)) :extrapreds ((AT0_PROC7_CS)) :extrapreds ((AT0_PROC8_B)) :extrapreds ((AT0_PROC7_SW_C_CS_TAU)) :extrapreds ((AT0_PROC8_A)) :extrapreds ((AT0_PROC2_SW_B_C_TAU)) :extrapreds ((AT1_PROC4_C)) :extrapreds ((AT1_PROC1_CS)) :extrapreds ((AT0_PROC9_SW_C_B_TAU)) :extrapreds ((AT1_PROC4_B)) :extrapreds ((AT0_PROC6_SW_CS_A_TAU)) :extrapreds ((AT1_PROC4_A)) :extrapreds ((AT0_PROC3_SW_C_CS_TAU)) :extrapreds ((AT0_PROC11_TAU)) :extrapreds ((AT0_PROC1_SW_A_B_TAU)) :extrapreds ((AT0_PROC2_SW_CS_A_TAU)) :extrafuns ((AT0_PROC10_X Int)) :extrapreds ((AT1_PROC11_CS)) :extrafuns ((AT0_PROC6_X Int)) :extrapreds ((AT0_PROC2_TAU)) :extrapreds ((AT0_PROC8_WAIT)) :extrafuns ((AT1_PROC11_X Int)) :extrafuns ((AT1_PROC2_X Int)) :extrapreds ((AT1_PROC7_C)) :extrapreds ((AT0_PROC11_SW_CS_A_TAU)) :extrapreds ((AT0_PROC4_SW_C_CS_TAU)) :extrapreds ((AT1_PROC7_B)) :extrafuns ((AT0_Z Int)) :extrapreds ((AT1_PROC7_A)) :extrapreds ((AT0_PROC6_TAU)) :extrapreds ((AT1_PROC8_CS)) :extrapreds ((AT0_PROC8_SW_C_CS_TAU)) :extrapreds ((AT0_PROC5_WAIT)) :extrapreds ((AT0_PROC2_SW_A_B_TAU)) :extrapreds ((AT0_PROC3_C)) :extrapreds ((AT0_PROC3_B)) :extrapreds ((AT0_PROC3_A)) :extrapreds ((AT0_PROC8_SW_C_B_TAU)) :extrapreds ((AT0_PROC3_SW_C_B_TAU)) :extrapreds ((AT0_PROC2_WAIT)) :extrapreds ((AT0_PROC1_SW_B_C_TAU)) :extrafuns ((AT0_PROC9_X Int)) :formula (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 AT0_PROC2_A)) (flet ($cvcl_9 (not AT0_PROC2_B)) (flet ($cvcl_10 (not AT0_PROC2_C)) (flet ($cvcl_11 (not AT0_PROC2_CS)) (flet ($cvcl_12 (not AT1_PROC2_A)) (flet ($cvcl_13 (not AT1_PROC2_B)) (flet ($cvcl_14 (not AT1_PROC2_C)) (flet ($cvcl_15 (not AT1_PROC2_CS)) (flet ($cvcl_16 (not AT0_PROC3_A)) (flet ($cvcl_17 (not AT0_PROC3_B)) (flet ($cvcl_18 (not AT0_PROC3_C)) (flet ($cvcl_19 (not AT0_PROC3_CS)) (flet ($cvcl_20 (not AT1_PROC3_A)) (flet ($cvcl_21 (not AT1_PROC3_B)) (flet ($cvcl_22 (not AT1_PROC3_C)) (flet ($cvcl_23 (not AT1_PROC3_CS)) (flet ($cvcl_24 (not AT0_PROC4_A)) (flet ($cvcl_25 (not AT0_PROC4_B)) (flet ($cvcl_26 (not AT0_PROC4_C)) (flet ($cvcl_27 (not AT0_PROC4_CS)) (flet ($cvcl_28 (not AT1_PROC4_A)) (flet ($cvcl_29 (not AT1_PROC4_B)) (flet ($cvcl_30 (not AT1_PROC4_C)) (flet ($cvcl_31 (not AT1_PROC4_CS)) (flet ($cvcl_32 (not AT0_PROC5_A)) (flet ($cvcl_33 (not AT0_PROC5_B)) (flet ($cvcl_34 (not AT0_PROC5_C)) (flet ($cvcl_35 (not AT0_PROC5_CS)) (flet ($cvcl_36 (not AT1_PROC5_A)) (flet ($cvcl_37 (not AT1_PROC5_B)) (flet ($cvcl_38 (not AT1_PROC5_C)) (flet ($cvcl_39 (not AT1_PROC5_CS)) (flet ($cvcl_40 (not AT0_PROC6_A)) (flet ($cvcl_41 (not AT0_PROC6_B)) (flet ($cvcl_42 (not AT0_PROC6_C)) (flet ($cvcl_43 (not AT0_PROC6_CS)) (flet ($cvcl_44 (not AT1_PROC6_A)) (flet ($cvcl_45 (not AT1_PROC6_B)) (flet ($cvcl_46 (not AT1_PROC6_C)) (flet ($cvcl_47 (not AT1_PROC6_CS)) (flet ($cvcl_48 (not AT0_PROC7_A)) (flet ($cvcl_49 (not AT0_PROC7_B)) (flet ($cvcl_50 (not AT0_PROC7_C)) (flet ($cvcl_51 (not AT0_PROC7_CS)) (flet ($cvcl_52 (not AT1_PROC7_A)) (flet ($cvcl_53 (not AT1_PROC7_B)) (flet ($cvcl_54 (not AT1_PROC7_C)) (flet ($cvcl_55 (not AT1_PROC7_CS)) (flet ($cvcl_56 (not AT0_PROC8_A)) (flet ($cvcl_57 (not AT0_PROC8_B)) (flet ($cvcl_58 (not AT0_PROC8_C)) (flet ($cvcl_59 (not AT0_PROC8_CS)) (flet ($cvcl_60 (not AT1_PROC8_A)) (flet ($cvcl_61 (not AT1_PROC8_B)) (flet ($cvcl_62 (not AT1_PROC8_C)) (flet ($cvcl_63 (not AT1_PROC8_CS)) (flet ($cvcl_64 (not AT0_PROC9_A)) (flet ($cvcl_65 (not AT0_PROC9_B)) (flet ($cvcl_66 (not AT0_PROC9_C)) (flet ($cvcl_67 (not AT0_PROC9_CS)) (flet ($cvcl_68 (not AT1_PROC9_A)) (flet ($cvcl_69 (not AT1_PROC9_B)) (flet ($cvcl_70 (not AT1_PROC9_C)) (flet ($cvcl_71 (not AT1_PROC9_CS)) (flet ($cvcl_72 (not AT0_PROC10_A)) (flet ($cvcl_73 (not AT0_PROC10_B)) (flet ($cvcl_74 (not AT0_PROC10_C)) (flet ($cvcl_75 (not AT0_PROC10_CS)) (flet ($cvcl_76 (not AT1_PROC10_A)) (flet ($cvcl_77 (not AT1_PROC10_B)) (flet ($cvcl_78 (not AT1_PROC10_C)) (flet ($cvcl_79 (not AT1_PROC10_CS)) (flet ($cvcl_80 (not AT0_PROC11_A)) (flet ($cvcl_81 (not AT0_PROC11_B)) (flet ($cvcl_82 (not AT0_PROC11_C)) (flet ($cvcl_83 (not AT0_PROC11_CS)) (flet ($cvcl_84 (not AT1_PROC11_A)) (flet ($cvcl_85 (not AT1_PROC11_B)) (flet ($cvcl_86 (not AT1_PROC11_C)) (flet ($cvcl_87 (not AT1_PROC11_CS)) (flet ($cvcl_88 (= AT0_PROC1_X AT0_Z)) (flet ($cvcl_89 (> AT0_PROC1_X AT0_Z)) (flet ($cvcl_249 (not $cvcl_88)) (flet ($cvcl_90 (= AT1_PROC1_X AT1_Z)) (flet ($cvcl_91 (> AT1_PROC1_X AT1_Z)) (flet ($cvcl_248 (not $cvcl_90)) (flet ($cvcl_92 (= AT0_PROC2_X AT0_Z)) (flet ($cvcl_93 (> AT0_PROC2_X AT0_Z)) (flet ($cvcl_254 (not $cvcl_92)) (flet ($cvcl_94 (= AT1_PROC2_X AT1_Z)) (flet ($cvcl_95 (> AT1_PROC2_X AT1_Z)) (flet ($cvcl_253 (not $cvcl_94)) (flet ($cvcl_96 (= AT0_PROC3_X AT0_Z)) (flet ($cvcl_97 (> AT0_PROC3_X AT0_Z)) (flet ($cvcl_258 (not $cvcl_96)) (flet ($cvcl_98 (= AT1_PROC3_X AT1_Z)) (flet ($cvcl_99 (> AT1_PROC3_X AT1_Z)) (flet ($cvcl_257 (not $cvcl_98)) (flet ($cvcl_100 (= AT0_PROC4_X AT0_Z)) (flet ($cvcl_101 (> AT0_PROC4_X AT0_Z)) (flet ($cvcl_262 (not $cvcl_100)) (flet ($cvcl_102 (= AT1_PROC4_X AT1_Z)) (flet ($cvcl_103 (> AT1_PROC4_X AT1_Z)) (flet ($cvcl_261 (not $cvcl_102)) (flet ($cvcl_104 (= AT0_PROC5_X AT0_Z)) (flet ($cvcl_105 (> AT0_PROC5_X AT0_Z)) (flet ($cvcl_266 (not $cvcl_104)) (flet ($cvcl_106 (= AT1_PROC5_X AT1_Z)) (flet ($cvcl_107 (> AT1_PROC5_X AT1_Z)) (flet ($cvcl_265 (not $cvcl_106)) (flet ($cvcl_108 (= AT0_PROC6_X AT0_Z)) (flet ($cvcl_109 (> AT0_PROC6_X AT0_Z)) (flet ($cvcl_270 (not $cvcl_108)) (flet ($cvcl_110 (= AT1_PROC6_X AT1_Z)) (flet ($cvcl_111 (> AT1_PROC6_X AT1_Z)) (flet ($cvcl_269 (not $cvcl_110)) (flet ($cvcl_112 (= AT0_PROC7_X AT0_Z)) (flet ($cvcl_113 (> AT0_PROC7_X AT0_Z)) (flet ($cvcl_274 (not $cvcl_112)) (flet ($cvcl_114 (= AT1_PROC7_X AT1_Z)) (flet ($cvcl_115 (> AT1_PROC7_X AT1_Z)) (flet ($cvcl_273 (not $cvcl_114)) (flet ($cvcl_116 (= AT0_PROC8_X AT0_Z)) (flet ($cvcl_117 (> AT0_PROC8_X AT0_Z)) (flet ($cvcl_278 (not $cvcl_116)) (flet ($cvcl_118 (= AT1_PROC8_X AT1_Z)) (flet ($cvcl_119 (> AT1_PROC8_X AT1_Z)) (flet ($cvcl_277 (not $cvcl_118)) (flet ($cvcl_120 (= AT0_PROC9_X AT0_Z)) (flet ($cvcl_121 (> AT0_PROC9_X AT0_Z)) (flet ($cvcl_282 (not $cvcl_120)) (flet ($cvcl_122 (= AT1_PROC9_X AT1_Z)) (flet ($cvcl_123 (> AT1_PROC9_X AT1_Z)) (flet ($cvcl_281 (not $cvcl_122)) (flet ($cvcl_124 (= AT0_PROC10_X AT0_Z)) (flet ($cvcl_125 (> AT0_PROC10_X AT0_Z)) (flet ($cvcl_286 (not $cvcl_124)) (flet ($cvcl_126 (= AT1_PROC10_X AT1_Z)) (flet ($cvcl_127 (> AT1_PROC10_X AT1_Z)) (flet ($cvcl_285 (not $cvcl_126)) (flet ($cvcl_128 (= AT0_PROC11_X AT0_Z)) (flet ($cvcl_129 (> AT0_PROC11_X AT0_Z)) (flet ($cvcl_290 (not $cvcl_128)) (flet ($cvcl_130 (= AT1_PROC11_X AT1_Z)) (flet ($cvcl_131 (> AT1_PROC11_X AT1_Z)) (flet ($cvcl_289 (not $cvcl_130)) (flet ($cvcl_134 (<= (- AT0_PROC1_X AT0_Z) 10)) (flet ($cvcl_141 (<= (- AT0_PROC2_X AT0_Z) 10)) (flet ($cvcl_147 (<= (- AT0_PROC3_X AT0_Z) 10)) (flet ($cvcl_153 (<= (- AT0_PROC4_X AT0_Z) 10)) (flet ($cvcl_159 (<= (- AT0_PROC5_X AT0_Z) 10)) (flet ($cvcl_165 (<= (- AT0_PROC6_X AT0_Z) 10)) (flet ($cvcl_171 (<= (- AT0_PROC7_X AT0_Z) 10)) (flet ($cvcl_177 (<= (- AT0_PROC8_X AT0_Z) 10)) (flet ($cvcl_183 (<= (- AT0_PROC9_X AT0_Z) 10)) (flet ($cvcl_189 (<= (- AT0_PROC10_X AT0_Z) 10)) (flet ($cvcl_195 (<= (- AT0_PROC11_X AT0_Z) 10)) (flet ($cvcl_132 (not AT0_PROC1_SW_A_B_TAU)) (flet ($cvcl_133 (not AT0_PROC1_SW_B_C_TAU)) (flet ($cvcl_135 (not AT0_PROC1_SW_C_B_TAU)) (flet ($cvcl_136 (not AT0_PROC1_SW_C_CS_TAU)) (flet ($cvcl_200 (= AT1_PROC1_X AT0_PROC1_X)) (flet ($cvcl_137 (not AT0_PROC1_SW_CS_A_TAU)) (flet ($cvcl_138 (= AT1_Z AT0_Z)) (flet ($cvcl_139 (not AT0_PROC2_SW_A_B_TAU)) (flet ($cvcl_140 (not AT0_PROC2_SW_B_C_TAU)) (flet ($cvcl_142 (not AT0_PROC2_SW_C_B_TAU)) (flet ($cvcl_143 (not AT0_PROC2_SW_C_CS_TAU)) (flet ($cvcl_202 (= AT1_PROC2_X AT0_PROC2_X)) (flet ($cvcl_144 (not AT0_PROC2_SW_CS_A_TAU)) (flet ($cvcl_145 (not AT0_PROC3_SW_A_B_TAU)) (flet ($cvcl_146 (not AT0_PROC3_SW_B_C_TAU)) (flet ($cvcl_148 (not AT0_PROC3_SW_C_B_TAU)) (flet ($cvcl_149 (not AT0_PROC3_SW_C_CS_TAU)) (flet ($cvcl_204 (= AT1_PROC3_X AT0_PROC3_X)) (flet ($cvcl_150 (not AT0_PROC3_SW_CS_A_TAU)) (flet ($cvcl_151 (not AT0_PROC4_SW_A_B_TAU)) (flet ($cvcl_152 (not AT0_PROC4_SW_B_C_TAU)) (flet ($cvcl_154 (not AT0_PROC4_SW_C_B_TAU)) (flet ($cvcl_155 (not AT0_PROC4_SW_C_CS_TAU)) (flet ($cvcl_206 (= AT1_PROC4_X AT0_PROC4_X)) (flet ($cvcl_156 (not AT0_PROC4_SW_CS_A_TAU)) (flet ($cvcl_157 (not AT0_PROC5_SW_A_B_TAU)) (flet ($cvcl_158 (not AT0_PROC5_SW_B_C_TAU)) (flet ($cvcl_160 (not AT0_PROC5_SW_C_B_TAU)) (flet ($cvcl_161 (not AT0_PROC5_SW_C_CS_TAU)) (flet ($cvcl_208 (= AT1_PROC5_X AT0_PROC5_X)) (flet ($cvcl_162 (not AT0_PROC5_SW_CS_A_TAU)) (flet ($cvcl_163 (not AT0_PROC6_SW_A_B_TAU)) (flet ($cvcl_164 (not AT0_PROC6_SW_B_C_TAU)) (flet ($cvcl_166 (not AT0_PROC6_SW_C_B_TAU)) (flet ($cvcl_167 (not AT0_PROC6_SW_C_CS_TAU)) (flet ($cvcl_210 (= AT1_PROC6_X AT0_PROC6_X)) (flet ($cvcl_168 (not AT0_PROC6_SW_CS_A_TAU)) (flet ($cvcl_169 (not AT0_PROC7_SW_A_B_TAU)) (flet ($cvcl_170 (not AT0_PROC7_SW_B_C_TAU)) (flet ($cvcl_172 (not AT0_PROC7_SW_C_B_TAU)) (flet ($cvcl_173 (not AT0_PROC7_SW_C_CS_TAU)) (flet ($cvcl_212 (= AT1_PROC7_X AT0_PROC7_X)) (flet ($cvcl_174 (not AT0_PROC7_SW_CS_A_TAU)) (flet ($cvcl_175 (not AT0_PROC8_SW_A_B_TAU)) (flet ($cvcl_176 (not AT0_PROC8_SW_B_C_TAU)) (flet ($cvcl_178 (not AT0_PROC8_SW_C_B_TAU)) (flet ($cvcl_179 (not AT0_PROC8_SW_C_CS_TAU)) (flet ($cvcl_214 (= AT1_PROC8_X AT0_PROC8_X)) (flet ($cvcl_180 (not AT0_PROC8_SW_CS_A_TAU)) (flet ($cvcl_181 (not AT0_PROC9_SW_A_B_TAU)) (flet ($cvcl_182 (not AT0_PROC9_SW_B_C_TAU)) (flet ($cvcl_184 (not AT0_PROC9_SW_C_B_TAU)) (flet ($cvcl_185 (not AT0_PROC9_SW_C_CS_TAU)) (flet ($cvcl_216 (= AT1_PROC9_X AT0_PROC9_X)) (flet ($cvcl_186 (not AT0_PROC9_SW_CS_A_TAU)) (flet ($cvcl_187 (not AT0_PROC10_SW_A_B_TAU)) (flet ($cvcl_188 (not AT0_PROC10_SW_B_C_TAU)) (flet ($cvcl_190 (not AT0_PROC10_SW_C_B_TAU)) (flet ($cvcl_191 (not AT0_PROC10_SW_C_CS_TAU)) (flet ($cvcl_218 (= AT1_PROC10_X AT0_PROC10_X)) (flet ($cvcl_192 (not AT0_PROC10_SW_CS_A_TAU)) (flet ($cvcl_193 (not AT0_PROC11_SW_A_B_TAU)) (flet ($cvcl_194 (not AT0_PROC11_SW_B_C_TAU)) (flet ($cvcl_196 (not AT0_PROC11_SW_C_B_TAU)) (flet ($cvcl_197 (not AT0_PROC11_SW_C_CS_TAU)) (flet ($cvcl_220 (= AT1_PROC11_X AT0_PROC11_X)) (flet ($cvcl_198 (not AT0_PROC11_SW_CS_A_TAU)) (flet ($cvcl_199 (not AT0_PROC1_WAIT)) (flet ($cvcl_222 (not AT0_PROC1_TAU)) (flet ($cvcl_201 (not AT0_PROC2_WAIT)) (flet ($cvcl_223 (not AT0_PROC2_TAU)) (flet ($cvcl_203 (not AT0_PROC3_WAIT)) (flet ($cvcl_225 (not AT0_PROC3_TAU)) (flet ($cvcl_205 (not AT0_PROC4_WAIT)) (flet ($cvcl_226 (not AT0_PROC4_TAU)) (flet ($cvcl_207 (not AT0_PROC5_WAIT)) (flet ($cvcl_227 (not AT0_PROC5_TAU)) (flet ($cvcl_209 (not AT0_PROC6_WAIT)) (flet ($cvcl_228 (not AT0_PROC6_TAU)) (flet ($cvcl_211 (not AT0_PROC7_WAIT)) (flet ($cvcl_229 (not AT0_PROC7_TAU)) (flet ($cvcl_213 (not AT0_PROC8_WAIT)) (flet ($cvcl_230 (not AT0_PROC8_TAU)) (flet ($cvcl_215 (not AT0_PROC9_WAIT)) (flet ($cvcl_231 (not AT0_PROC9_TAU)) (flet ($cvcl_217 (not AT0_PROC10_WAIT)) (flet ($cvcl_232 (not AT0_PROC10_TAU)) (flet ($cvcl_219 (not AT0_PROC11_WAIT)) (flet ($cvcl_233 (not AT0_PROC11_TAU)) (flet ($cvcl_221 (not AT0_DELTA)) (flet ($cvcl_245 (< AT1_Z AT0_Z)) (flet ($cvcl_224 (or $cvcl_221 $cvcl_245 )) (flet ($cvcl_234 (< AT1_PROC1_X AT0_PROC1_X)) (flet ($cvcl_246 (not $cvcl_200)) (flet ($cvcl_235 (< AT1_PROC2_X AT0_PROC2_X)) (flet ($cvcl_252 (not $cvcl_202)) (flet ($cvcl_236 (< AT1_PROC3_X AT0_PROC3_X)) (flet ($cvcl_256 (not $cvcl_204)) (flet ($cvcl_237 (< AT1_PROC4_X AT0_PROC4_X)) (flet ($cvcl_260 (not $cvcl_206)) (flet ($cvcl_238 (< AT1_PROC5_X AT0_PROC5_X)) (flet ($cvcl_264 (not $cvcl_208)) (flet ($cvcl_239 (< AT1_PROC6_X AT0_PROC6_X)) (flet ($cvcl_268 (not $cvcl_210)) (flet ($cvcl_240 (< AT1_PROC7_X AT0_PROC7_X)) (flet ($cvcl_272 (not $cvcl_212)) (flet ($cvcl_241 (< AT1_PROC8_X AT0_PROC8_X)) (flet ($cvcl_276 (not $cvcl_214)) (flet ($cvcl_242 (< AT1_PROC9_X AT0_PROC9_X)) (flet ($cvcl_280 (not $cvcl_216)) (flet ($cvcl_243 (< AT1_PROC10_X AT0_PROC10_X)) (flet ($cvcl_284 (not $cvcl_218)) (flet ($cvcl_244 (< AT1_PROC11_X AT0_PROC11_X)) (flet ($cvcl_288 (not $cvcl_220)) (flet ($cvcl_247 (not $cvcl_138)) (flet ($cvcl_251 (not $cvcl_245)) (flet ($cvcl_250 (or $cvcl_249 $cvcl_246 )) (flet ($cvcl_255 (or $cvcl_254 $cvcl_252 )) (flet ($cvcl_259 (or $cvcl_258 $cvcl_256 )) (flet ($cvcl_263 (or $cvcl_262 $cvcl_260 )) (flet ($cvcl_267 (or $cvcl_266 $cvcl_264 )) (flet ($cvcl_271 (or $cvcl_270 $cvcl_268 )) (flet ($cvcl_275 (or $cvcl_274 $cvcl_272 )) (flet ($cvcl_279 (or $cvcl_278 $cvcl_276 )) (flet ($cvcl_283 (or $cvcl_282 $cvcl_280 )) (flet ($cvcl_287 (or $cvcl_286 $cvcl_284 )) (flet ($cvcl_291 (or $cvcl_290 $cvcl_288 )) (flet ($cvcl_292 (not AT0_ID0)) (flet ($cvcl_293 (not AT0_ID1)) (flet ($cvcl_294 (not AT0_ID2)) (flet ($cvcl_295 (not AT0_ID3)) (flet ($cvcl_296 (not AT0_ID4)) (flet ($cvcl_297 (not AT0_ID5)) (flet ($cvcl_298 (not AT0_ID6)) (flet ($cvcl_299 (not AT0_ID7)) (flet ($cvcl_300 (not AT0_ID8)) (flet ($cvcl_301 (not AT0_ID9)) (flet ($cvcl_302 (not AT0_ID10)) (flet ($cvcl_303 (not AT0_ID11)) (flet ($cvcl_304 (not AT1_ID0)) (flet ($cvcl_305 (not AT1_ID1)) (flet ($cvcl_306 (not AT1_ID2)) (flet ($cvcl_307 (not AT1_ID3)) (flet ($cvcl_308 (not AT1_ID4)) (flet ($cvcl_309 (not AT1_ID5)) (flet ($cvcl_310 (not AT1_ID6)) (flet ($cvcl_311 (not AT1_ID7)) (flet ($cvcl_312 (not AT1_ID8)) (flet ($cvcl_313 (not AT1_ID9)) (flet ($cvcl_314 (not AT1_ID10)) (flet ($cvcl_315 (not AT1_ID11)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (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_60 $cvcl_62 )) (or $cvcl_60 $cvcl_63 )) (or $cvcl_61 $cvcl_62 )) (or $cvcl_61 $cvcl_63 )) (or $cvcl_62 $cvcl_63 )) (or $cvcl_64 $cvcl_65 )) (or $cvcl_64 $cvcl_66 )) (or $cvcl_64 $cvcl_67 )) (or $cvcl_65 $cvcl_66 )) (or $cvcl_65 $cvcl_67 )) (or $cvcl_66 $cvcl_67 )) (or $cvcl_68 $cvcl_69 )) (or $cvcl_68 $cvcl_70 )) (or $cvcl_68 $cvcl_71 )) (or $cvcl_69 $cvcl_70 )) (or $cvcl_69 $cvcl_71 )) (or $cvcl_70 $cvcl_71 )) (or $cvcl_72 $cvcl_73 )) (or $cvcl_72 $cvcl_74 )) (or $cvcl_72 $cvcl_75 )) (or $cvcl_73 $cvcl_74 )) (or $cvcl_73 $cvcl_75 )) (or $cvcl_74 $cvcl_75 )) (or $cvcl_76 $cvcl_77 )) (or $cvcl_76 $cvcl_78 )) (or $cvcl_76 $cvcl_79 )) (or $cvcl_77 $cvcl_78 )) (or $cvcl_77 $cvcl_79 )) (or $cvcl_78 $cvcl_79 )) (or $cvcl_80 $cvcl_81 )) (or $cvcl_80 $cvcl_82 )) (or $cvcl_80 $cvcl_83 )) (or $cvcl_81 $cvcl_82 )) (or $cvcl_81 $cvcl_83 )) (or $cvcl_82 $cvcl_83 )) (or $cvcl_84 $cvcl_85 )) (or $cvcl_84 $cvcl_86 )) (or $cvcl_84 $cvcl_87 )) (or $cvcl_85 $cvcl_86 )) (or $cvcl_85 $cvcl_87 )) (or $cvcl_86 $cvcl_87 )) (or $cvcl_88 $cvcl_89 )) (or $cvcl_249 (not $cvcl_89) )) (or $cvcl_90 $cvcl_91 )) (or $cvcl_248 (not $cvcl_91) )) (or $cvcl_92 $cvcl_93 )) (or $cvcl_254 (not $cvcl_93) )) (or $cvcl_94 $cvcl_95 )) (or $cvcl_253 (not $cvcl_95) )) (or $cvcl_96 $cvcl_97 )) (or $cvcl_258 (not $cvcl_97) )) (or $cvcl_98 $cvcl_99 )) (or $cvcl_257 (not $cvcl_99) )) (or $cvcl_100 $cvcl_101 )) (or $cvcl_262 (not $cvcl_101) )) (or $cvcl_102 $cvcl_103 )) (or $cvcl_261 (not $cvcl_103) )) (or $cvcl_104 $cvcl_105 )) (or $cvcl_266 (not $cvcl_105) )) (or $cvcl_106 $cvcl_107 )) (or $cvcl_265 (not $cvcl_107) )) (or $cvcl_108 $cvcl_109 )) (or $cvcl_270 (not $cvcl_109) )) (or $cvcl_110 $cvcl_111 )) (or $cvcl_269 (not $cvcl_111) )) (or $cvcl_112 $cvcl_113 )) (or $cvcl_274 (not $cvcl_113) )) (or $cvcl_114 $cvcl_115 )) (or $cvcl_273 (not $cvcl_115) )) (or $cvcl_116 $cvcl_117 )) (or $cvcl_278 (not $cvcl_117) )) (or $cvcl_118 $cvcl_119 )) (or $cvcl_277 (not $cvcl_119) )) (or $cvcl_120 $cvcl_121 )) (or $cvcl_282 (not $cvcl_121) )) (or $cvcl_122 $cvcl_123 )) (or $cvcl_281 (not $cvcl_123) )) (or $cvcl_124 $cvcl_125 )) (or $cvcl_286 (not $cvcl_125) )) (or $cvcl_126 $cvcl_127 )) (or $cvcl_285 (not $cvcl_127) )) (or $cvcl_128 $cvcl_129 )) (or $cvcl_290 (not $cvcl_129) )) (or $cvcl_130 $cvcl_131 )) (or $cvcl_289 (not $cvcl_131) )) (or $cvcl_1 $cvcl_134 )) (or $cvcl_5 (<= (- AT1_PROC1_X AT1_Z) 10) )) (or $cvcl_9 $cvcl_141 )) (or $cvcl_13 (<= (- AT1_PROC2_X AT1_Z) 10) )) (or $cvcl_17 $cvcl_147 )) (or $cvcl_21 (<= (- AT1_PROC3_X AT1_Z) 10) )) (or $cvcl_25 $cvcl_153 )) (or $cvcl_29 (<= (- AT1_PROC4_X AT1_Z) 10) )) (or $cvcl_33 $cvcl_159 )) (or $cvcl_37 (<= (- AT1_PROC5_X AT1_Z) 10) )) (or $cvcl_41 $cvcl_165 )) (or $cvcl_45 (<= (- AT1_PROC6_X AT1_Z) 10) )) (or $cvcl_49 $cvcl_171 )) (or $cvcl_53 (<= (- AT1_PROC7_X AT1_Z) 10) )) (or $cvcl_57 $cvcl_177 )) (or $cvcl_61 (<= (- AT1_PROC8_X AT1_Z) 10) )) (or $cvcl_65 $cvcl_183 )) (or $cvcl_69 (<= (- AT1_PROC9_X AT1_Z) 10) )) (or $cvcl_73 $cvcl_189 )) (or $cvcl_77 (<= (- AT1_PROC10_X AT1_Z) 10) )) (or $cvcl_81 $cvcl_195 )) (or $cvcl_85 (<= (- AT1_PROC11_X AT1_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 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 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 AT0_PROC4_WAIT AT0_DELTA ) AT0_PROC4_SW_A_B_TAU ) AT0_PROC4_SW_B_C_TAU ) AT0_PROC4_SW_C_B_TAU ) AT0_PROC4_SW_C_CS_TAU ) AT0_PROC4_SW_CS_A_TAU )) (or (or (or (or (or (or AT0_PROC5_WAIT AT0_DELTA ) AT0_PROC5_SW_A_B_TAU ) AT0_PROC5_SW_B_C_TAU ) AT0_PROC5_SW_C_B_TAU ) AT0_PROC5_SW_C_CS_TAU ) AT0_PROC5_SW_CS_A_TAU )) (or (or (or (or (or (or AT0_PROC6_WAIT AT0_DELTA ) AT0_PROC6_SW_A_B_TAU ) AT0_PROC6_SW_B_C_TAU ) AT0_PROC6_SW_C_B_TAU ) AT0_PROC6_SW_C_CS_TAU ) AT0_PROC6_SW_CS_A_TAU )) (or (or (or (or (or (or AT0_PROC7_WAIT AT0_DELTA ) AT0_PROC7_SW_A_B_TAU ) AT0_PROC7_SW_B_C_TAU ) AT0_PROC7_SW_C_B_TAU ) AT0_PROC7_SW_C_CS_TAU ) AT0_PROC7_SW_CS_A_TAU )) (or (or (or (or (or (or AT0_PROC8_WAIT AT0_DELTA ) AT0_PROC8_SW_A_B_TAU ) AT0_PROC8_SW_B_C_TAU ) AT0_PROC8_SW_C_B_TAU ) AT0_PROC8_SW_C_CS_TAU ) AT0_PROC8_SW_CS_A_TAU )) (or (or (or (or (or (or AT0_PROC9_WAIT AT0_DELTA ) AT0_PROC9_SW_A_B_TAU ) AT0_PROC9_SW_B_C_TAU ) AT0_PROC9_SW_C_B_TAU ) AT0_PROC9_SW_C_CS_TAU ) AT0_PROC9_SW_CS_A_TAU )) (or (or (or (or (or (or AT0_PROC10_WAIT AT0_DELTA ) AT0_PROC10_SW_A_B_TAU ) AT0_PROC10_SW_B_C_TAU ) AT0_PROC10_SW_C_B_TAU ) AT0_PROC10_SW_C_CS_TAU ) AT0_PROC10_SW_CS_A_TAU )) (or (or (or (or (or (or AT0_PROC11_WAIT AT0_DELTA ) AT0_PROC11_SW_A_B_TAU ) AT0_PROC11_SW_B_C_TAU ) AT0_PROC11_SW_C_B_TAU ) AT0_PROC11_SW_C_CS_TAU ) AT0_PROC11_SW_CS_A_TAU )) (or $cvcl_132 AT0_PROC1_A )) (or $cvcl_132 AT0_PROC1_TAU )) (or $cvcl_132 AT1_PROC1_B )) (or $cvcl_132 $cvcl_90 )) (or $cvcl_133 AT0_PROC1_B )) (or $cvcl_133 AT0_PROC1_TAU )) (or $cvcl_133 AT1_PROC1_C )) (or $cvcl_133 $cvcl_134 )) (or $cvcl_133 $cvcl_90 )) (or $cvcl_135 AT0_PROC1_C )) (or $cvcl_135 AT0_PROC1_TAU )) (or $cvcl_135 AT1_PROC1_B )) (or $cvcl_135 $cvcl_90 )) (or $cvcl_136 AT0_PROC1_C )) (or $cvcl_136 AT0_PROC1_TAU )) (or $cvcl_136 AT1_PROC1_CS )) (or $cvcl_136 (> (- AT0_PROC1_X AT0_Z) 10) )) (or $cvcl_136 $cvcl_200 )) (or $cvcl_137 AT0_PROC1_CS )) (or $cvcl_137 AT0_PROC1_TAU )) (or $cvcl_137 AT1_PROC1_A )) (or $cvcl_137 $cvcl_90 )) (or $cvcl_132 $cvcl_138 )) (or $cvcl_133 $cvcl_138 )) (or $cvcl_135 $cvcl_138 )) (or $cvcl_136 $cvcl_138 )) (or $cvcl_137 $cvcl_138 )) (or $cvcl_139 AT0_PROC2_A )) (or $cvcl_139 AT0_PROC2_TAU )) (or $cvcl_139 AT1_PROC2_B )) (or $cvcl_139 $cvcl_94 )) (or $cvcl_140 AT0_PROC2_B )) (or $cvcl_140 AT0_PROC2_TAU )) (or $cvcl_140 AT1_PROC2_C )) (or $cvcl_140 $cvcl_141 )) (or $cvcl_140 $cvcl_94 )) (or $cvcl_142 AT0_PROC2_C )) (or $cvcl_142 AT0_PROC2_TAU )) (or $cvcl_142 AT1_PROC2_B )) (or $cvcl_142 $cvcl_94 )) (or $cvcl_143 AT0_PROC2_C )) (or $cvcl_143 AT0_PROC2_TAU )) (or $cvcl_143 AT1_PROC2_CS )) (or $cvcl_143 (> (- AT0_PROC2_X AT0_Z) 10) )) (or $cvcl_143 $cvcl_202 )) (or $cvcl_144 AT0_PROC2_CS )) (or $cvcl_144 AT0_PROC2_TAU )) (or $cvcl_144 AT1_PROC2_A )) (or $cvcl_144 $cvcl_94 )) (or $cvcl_139 $cvcl_138 )) (or $cvcl_140 $cvcl_138 )) (or $cvcl_142 $cvcl_138 )) (or $cvcl_143 $cvcl_138 )) (or $cvcl_144 $cvcl_138 )) (or $cvcl_145 AT0_PROC3_A )) (or $cvcl_145 AT0_PROC3_TAU )) (or $cvcl_145 AT1_PROC3_B )) (or $cvcl_145 $cvcl_98 )) (or $cvcl_146 AT0_PROC3_B )) (or $cvcl_146 AT0_PROC3_TAU )) (or $cvcl_146 AT1_PROC3_C )) (or $cvcl_146 $cvcl_147 )) (or $cvcl_146 $cvcl_98 )) (or $cvcl_148 AT0_PROC3_C )) (or $cvcl_148 AT0_PROC3_TAU )) (or $cvcl_148 AT1_PROC3_B )) (or $cvcl_148 $cvcl_98 )) (or $cvcl_149 AT0_PROC3_C )) (or $cvcl_149 AT0_PROC3_TAU )) (or $cvcl_149 AT1_PROC3_CS )) (or $cvcl_149 (> (- AT0_PROC3_X AT0_Z) 10) )) (or $cvcl_149 $cvcl_204 )) (or $cvcl_150 AT0_PROC3_CS )) (or $cvcl_150 AT0_PROC3_TAU )) (or $cvcl_150 AT1_PROC3_A )) (or $cvcl_150 $cvcl_98 )) (or $cvcl_145 $cvcl_138 )) (or $cvcl_146 $cvcl_138 )) (or $cvcl_148 $cvcl_138 )) (or $cvcl_149 $cvcl_138 )) (or $cvcl_150 $cvcl_138 )) (or $cvcl_151 AT0_PROC4_A )) (or $cvcl_151 AT0_PROC4_TAU )) (or $cvcl_151 AT1_PROC4_B )) (or $cvcl_151 $cvcl_102 )) (or $cvcl_152 AT0_PROC4_B )) (or $cvcl_152 AT0_PROC4_TAU )) (or $cvcl_152 AT1_PROC4_C )) (or $cvcl_152 $cvcl_153 )) (or $cvcl_152 $cvcl_102 )) (or $cvcl_154 AT0_PROC4_C )) (or $cvcl_154 AT0_PROC4_TAU )) (or $cvcl_154 AT1_PROC4_B )) (or $cvcl_154 $cvcl_102 )) (or $cvcl_155 AT0_PROC4_C )) (or $cvcl_155 AT0_PROC4_TAU )) (or $cvcl_155 AT1_PROC4_CS )) (or $cvcl_155 (> (- AT0_PROC4_X AT0_Z) 10) )) (or $cvcl_155 $cvcl_206 )) (or $cvcl_156 AT0_PROC4_CS )) (or $cvcl_156 AT0_PROC4_TAU )) (or $cvcl_156 AT1_PROC4_A )) (or $cvcl_156 $cvcl_102 )) (or $cvcl_151 $cvcl_138 )) (or $cvcl_152 $cvcl_138 )) (or $cvcl_154 $cvcl_138 )) (or $cvcl_155 $cvcl_138 )) (or $cvcl_156 $cvcl_138 )) (or $cvcl_157 AT0_PROC5_A )) (or $cvcl_157 AT0_PROC5_TAU )) (or $cvcl_157 AT1_PROC5_B )) (or $cvcl_157 $cvcl_106 )) (or $cvcl_158 AT0_PROC5_B )) (or $cvcl_158 AT0_PROC5_TAU )) (or $cvcl_158 AT1_PROC5_C )) (or $cvcl_158 $cvcl_159 )) (or $cvcl_158 $cvcl_106 )) (or $cvcl_160 AT0_PROC5_C )) (or $cvcl_160 AT0_PROC5_TAU )) (or $cvcl_160 AT1_PROC5_B )) (or $cvcl_160 $cvcl_106 )) (or $cvcl_161 AT0_PROC5_C )) (or $cvcl_161 AT0_PROC5_TAU )) (or $cvcl_161 AT1_PROC5_CS )) (or $cvcl_161 (> (- AT0_PROC5_X AT0_Z) 10) )) (or $cvcl_161 $cvcl_208 )) (or $cvcl_162 AT0_PROC5_CS )) (or $cvcl_162 AT0_PROC5_TAU )) (or $cvcl_162 AT1_PROC5_A )) (or $cvcl_162 $cvcl_106 )) (or $cvcl_157 $cvcl_138 )) (or $cvcl_158 $cvcl_138 )) (or $cvcl_160 $cvcl_138 )) (or $cvcl_161 $cvcl_138 )) (or $cvcl_162 $cvcl_138 )) (or $cvcl_163 AT0_PROC6_A )) (or $cvcl_163 AT0_PROC6_TAU )) (or $cvcl_163 AT1_PROC6_B )) (or $cvcl_163 $cvcl_110 )) (or $cvcl_164 AT0_PROC6_B )) (or $cvcl_164 AT0_PROC6_TAU )) (or $cvcl_164 AT1_PROC6_C )) (or $cvcl_164 $cvcl_165 )) (or $cvcl_164 $cvcl_110 )) (or $cvcl_166 AT0_PROC6_C )) (or $cvcl_166 AT0_PROC6_TAU )) (or $cvcl_166 AT1_PROC6_B )) (or $cvcl_166 $cvcl_110 )) (or $cvcl_167 AT0_PROC6_C )) (or $cvcl_167 AT0_PROC6_TAU )) (or $cvcl_167 AT1_PROC6_CS )) (or $cvcl_167 (> (- AT0_PROC6_X AT0_Z) 10) )) (or $cvcl_167 $cvcl_210 )) (or $cvcl_168 AT0_PROC6_CS )) (or $cvcl_168 AT0_PROC6_TAU )) (or $cvcl_168 AT1_PROC6_A )) (or $cvcl_168 $cvcl_110 )) (or $cvcl_163 $cvcl_138 )) (or $cvcl_164 $cvcl_138 )) (or $cvcl_166 $cvcl_138 )) (or $cvcl_167 $cvcl_138 )) (or $cvcl_168 $cvcl_138 )) (or $cvcl_169 AT0_PROC7_A )) (or $cvcl_169 AT0_PROC7_TAU )) (or $cvcl_169 AT1_PROC7_B )) (or $cvcl_169 $cvcl_114 )) (or $cvcl_170 AT0_PROC7_B )) (or $cvcl_170 AT0_PROC7_TAU )) (or $cvcl_170 AT1_PROC7_C )) (or $cvcl_170 $cvcl_171 )) (or $cvcl_170 $cvcl_114 )) (or $cvcl_172 AT0_PROC7_C )) (or $cvcl_172 AT0_PROC7_TAU )) (or $cvcl_172 AT1_PROC7_B )) (or $cvcl_172 $cvcl_114 )) (or $cvcl_173 AT0_PROC7_C )) (or $cvcl_173 AT0_PROC7_TAU )) (or $cvcl_173 AT1_PROC7_CS )) (or $cvcl_173 (> (- AT0_PROC7_X AT0_Z) 10) )) (or $cvcl_173 $cvcl_212 )) (or $cvcl_174 AT0_PROC7_CS )) (or $cvcl_174 AT0_PROC7_TAU )) (or $cvcl_174 AT1_PROC7_A )) (or $cvcl_174 $cvcl_114 )) (or $cvcl_169 $cvcl_138 )) (or $cvcl_170 $cvcl_138 )) (or $cvcl_172 $cvcl_138 )) (or $cvcl_173 $cvcl_138 )) (or $cvcl_174 $cvcl_138 )) (or $cvcl_175 AT0_PROC8_A )) (or $cvcl_175 AT0_PROC8_TAU )) (or $cvcl_175 AT1_PROC8_B )) (or $cvcl_175 $cvcl_118 )) (or $cvcl_176 AT0_PROC8_B )) (or $cvcl_176 AT0_PROC8_TAU )) (or $cvcl_176 AT1_PROC8_C )) (or $cvcl_176 $cvcl_177 )) (or $cvcl_176 $cvcl_118 )) (or $cvcl_178 AT0_PROC8_C )) (or $cvcl_178 AT0_PROC8_TAU )) (or $cvcl_178 AT1_PROC8_B )) (or $cvcl_178 $cvcl_118 )) (or $cvcl_179 AT0_PROC8_C )) (or $cvcl_179 AT0_PROC8_TAU )) (or $cvcl_179 AT1_PROC8_CS )) (or $cvcl_179 (> (- AT0_PROC8_X AT0_Z) 10) )) (or $cvcl_179 $cvcl_214 )) (or $cvcl_180 AT0_PROC8_CS )) (or $cvcl_180 AT0_PROC8_TAU )) (or $cvcl_180 AT1_PROC8_A )) (or $cvcl_180 $cvcl_118 )) (or $cvcl_175 $cvcl_138 )) (or $cvcl_176 $cvcl_138 )) (or $cvcl_178 $cvcl_138 )) (or $cvcl_179 $cvcl_138 )) (or $cvcl_180 $cvcl_138 )) (or $cvcl_181 AT0_PROC9_A )) (or $cvcl_181 AT0_PROC9_TAU )) (or $cvcl_181 AT1_PROC9_B )) (or $cvcl_181 $cvcl_122 )) (or $cvcl_182 AT0_PROC9_B )) (or $cvcl_182 AT0_PROC9_TAU )) (or $cvcl_182 AT1_PROC9_C )) (or $cvcl_182 $cvcl_183 )) (or $cvcl_182 $cvcl_122 )) (or $cvcl_184 AT0_PROC9_C )) (or $cvcl_184 AT0_PROC9_TAU )) (or $cvcl_184 AT1_PROC9_B )) (or $cvcl_184 $cvcl_122 )) (or $cvcl_185 AT0_PROC9_C )) (or $cvcl_185 AT0_PROC9_TAU )) (or $cvcl_185 AT1_PROC9_CS )) (or $cvcl_185 (> (- AT0_PROC9_X AT0_Z) 10) )) (or $cvcl_185 $cvcl_216 )) (or $cvcl_186 AT0_PROC9_CS )) (or $cvcl_186 AT0_PROC9_TAU )) (or $cvcl_186 AT1_PROC9_A )) (or $cvcl_186 $cvcl_122 )) (or $cvcl_181 $cvcl_138 )) (or $cvcl_182 $cvcl_138 )) (or $cvcl_184 $cvcl_138 )) (or $cvcl_185 $cvcl_138 )) (or $cvcl_186 $cvcl_138 )) (or $cvcl_187 AT0_PROC10_A )) (or $cvcl_187 AT0_PROC10_TAU )) (or $cvcl_187 AT1_PROC10_B )) (or $cvcl_187 $cvcl_126 )) (or $cvcl_188 AT0_PROC10_B )) (or $cvcl_188 AT0_PROC10_TAU )) (or $cvcl_188 AT1_PROC10_C )) (or $cvcl_188 $cvcl_189 )) (or $cvcl_188 $cvcl_126 )) (or $cvcl_190 AT0_PROC10_C )) (or $cvcl_190 AT0_PROC10_TAU )) (or $cvcl_190 AT1_PROC10_B )) (or $cvcl_190 $cvcl_126 )) (or $cvcl_191 AT0_PROC10_C )) (or $cvcl_191 AT0_PROC10_TAU )) (or $cvcl_191 AT1_PROC10_CS )) (or $cvcl_191 (> (- AT0_PROC10_X AT0_Z) 10) )) (or $cvcl_191 $cvcl_218 )) (or $cvcl_192 AT0_PROC10_CS )) (or $cvcl_192 AT0_PROC10_TAU )) (or $cvcl_192 AT1_PROC10_A )) (or $cvcl_192 $cvcl_126 )) (or $cvcl_187 $cvcl_138 )) (or $cvcl_188 $cvcl_138 )) (or $cvcl_190 $cvcl_138 )) (or $cvcl_191 $cvcl_138 )) (or $cvcl_192 $cvcl_138 )) (or $cvcl_193 AT0_PROC11_A )) (or $cvcl_193 AT0_PROC11_TAU )) (or $cvcl_193 AT1_PROC11_B )) (or $cvcl_193 $cvcl_130 )) (or $cvcl_194 AT0_PROC11_B )) (or $cvcl_194 AT0_PROC11_TAU )) (or $cvcl_194 AT1_PROC11_C )) (or $cvcl_194 $cvcl_195 )) (or $cvcl_194 $cvcl_130 )) (or $cvcl_196 AT0_PROC11_C )) (or $cvcl_196 AT0_PROC11_TAU )) (or $cvcl_196 AT1_PROC11_B )) (or $cvcl_196 $cvcl_130 )) (or $cvcl_197 AT0_PROC11_C )) (or $cvcl_197 AT0_PROC11_TAU )) (or $cvcl_197 AT1_PROC11_CS )) (or $cvcl_197 (> (- AT0_PROC11_X AT0_Z) 10) )) (or $cvcl_197 $cvcl_220 )) (or $cvcl_198 AT0_PROC11_CS )) (or $cvcl_198 AT0_PROC11_TAU )) (or $cvcl_198 AT1_PROC11_A )) (or $cvcl_198 $cvcl_130 )) (or $cvcl_193 $cvcl_138 )) (or $cvcl_194 $cvcl_138 )) (or $cvcl_196 $cvcl_138 )) (or $cvcl_197 $cvcl_138 )) (or $cvcl_198 $cvcl_138 )) (or (or $cvcl_199 $cvcl_0 ) AT1_PROC1_A )) (or (or $cvcl_199 AT0_PROC1_A ) $cvcl_4 )) (or (or $cvcl_199 $cvcl_1 ) AT1_PROC1_B )) (or (or $cvcl_199 AT0_PROC1_B ) $cvcl_5 )) (or (or $cvcl_199 $cvcl_2 ) AT1_PROC1_C )) (or (or $cvcl_199 AT0_PROC1_C ) $cvcl_6 )) (or (or $cvcl_199 $cvcl_3 ) AT1_PROC1_CS )) (or (or $cvcl_199 AT0_PROC1_CS ) $cvcl_7 )) (or $cvcl_199 $cvcl_222 )) (or $cvcl_199 $cvcl_200 )) (or $cvcl_199 $cvcl_138 )) (or (or $cvcl_201 $cvcl_8 ) AT1_PROC2_A )) (or (or $cvcl_201 AT0_PROC2_A ) $cvcl_12 )) (or (or $cvcl_201 $cvcl_9 ) AT1_PROC2_B )) (or (or $cvcl_201 AT0_PROC2_B ) $cvcl_13 )) (or (or $cvcl_201 $cvcl_10 ) AT1_PROC2_C )) (or (or $cvcl_201 AT0_PROC2_C ) $cvcl_14 )) (or (or $cvcl_201 $cvcl_11 ) AT1_PROC2_CS )) (or (or $cvcl_201 AT0_PROC2_CS ) $cvcl_15 )) (or $cvcl_201 $cvcl_223 )) (or $cvcl_201 $cvcl_202 )) (or $cvcl_201 $cvcl_138 )) (or (or $cvcl_203 $cvcl_16 ) AT1_PROC3_A )) (or (or $cvcl_203 AT0_PROC3_A ) $cvcl_20 )) (or (or $cvcl_203 $cvcl_17 ) AT1_PROC3_B )) (or (or $cvcl_203 AT0_PROC3_B ) $cvcl_21 )) (or (or $cvcl_203 $cvcl_18 ) AT1_PROC3_C )) (or (or $cvcl_203 AT0_PROC3_C ) $cvcl_22 )) (or (or $cvcl_203 $cvcl_19 ) AT1_PROC3_CS )) (or (or $cvcl_203 AT0_PROC3_CS ) $cvcl_23 )) (or $cvcl_203 $cvcl_225 )) (or $cvcl_203 $cvcl_204 )) (or $cvcl_203 $cvcl_138 )) (or (or $cvcl_205 $cvcl_24 ) AT1_PROC4_A )) (or (or $cvcl_205 AT0_PROC4_A ) $cvcl_28 )) (or (or $cvcl_205 $cvcl_25 ) AT1_PROC4_B )) (or (or $cvcl_205 AT0_PROC4_B ) $cvcl_29 )) (or (or $cvcl_205 $cvcl_26 ) AT1_PROC4_C )) (or (or $cvcl_205 AT0_PROC4_C ) $cvcl_30 )) (or (or $cvcl_205 $cvcl_27 ) AT1_PROC4_CS )) (or (or $cvcl_205 AT0_PROC4_CS ) $cvcl_31 )) (or $cvcl_205 $cvcl_226 )) (or $cvcl_205 $cvcl_206 )) (or $cvcl_205 $cvcl_138 )) (or (or $cvcl_207 $cvcl_32 ) AT1_PROC5_A )) (or (or $cvcl_207 AT0_PROC5_A ) $cvcl_36 )) (or (or $cvcl_207 $cvcl_33 ) AT1_PROC5_B )) (or (or $cvcl_207 AT0_PROC5_B ) $cvcl_37 )) (or (or $cvcl_207 $cvcl_34 ) AT1_PROC5_C )) (or (or $cvcl_207 AT0_PROC5_C ) $cvcl_38 )) (or (or $cvcl_207 $cvcl_35 ) AT1_PROC5_CS )) (or (or $cvcl_207 AT0_PROC5_CS ) $cvcl_39 )) (or $cvcl_207 $cvcl_227 )) (or $cvcl_207 $cvcl_208 )) (or $cvcl_207 $cvcl_138 )) (or (or $cvcl_209 $cvcl_40 ) AT1_PROC6_A )) (or (or $cvcl_209 AT0_PROC6_A ) $cvcl_44 )) (or (or $cvcl_209 $cvcl_41 ) AT1_PROC6_B )) (or (or $cvcl_209 AT0_PROC6_B ) $cvcl_45 )) (or (or $cvcl_209 $cvcl_42 ) AT1_PROC6_C )) (or (or $cvcl_209 AT0_PROC6_C ) $cvcl_46 )) (or (or $cvcl_209 $cvcl_43 ) AT1_PROC6_CS )) (or (or $cvcl_209 AT0_PROC6_CS ) $cvcl_47 )) (or $cvcl_209 $cvcl_228 )) (or $cvcl_209 $cvcl_210 )) (or $cvcl_209 $cvcl_138 )) (or (or $cvcl_211 $cvcl_48 ) AT1_PROC7_A )) (or (or $cvcl_211 AT0_PROC7_A ) $cvcl_52 )) (or (or $cvcl_211 $cvcl_49 ) AT1_PROC7_B )) (or (or $cvcl_211 AT0_PROC7_B ) $cvcl_53 )) (or (or $cvcl_211 $cvcl_50 ) AT1_PROC7_C )) (or (or $cvcl_211 AT0_PROC7_C ) $cvcl_54 )) (or (or $cvcl_211 $cvcl_51 ) AT1_PROC7_CS )) (or (or $cvcl_211 AT0_PROC7_CS ) $cvcl_55 )) (or $cvcl_211 $cvcl_229 )) (or $cvcl_211 $cvcl_212 )) (or $cvcl_211 $cvcl_138 )) (or (or $cvcl_213 $cvcl_56 ) AT1_PROC8_A )) (or (or $cvcl_213 AT0_PROC8_A ) $cvcl_60 )) (or (or $cvcl_213 $cvcl_57 ) AT1_PROC8_B )) (or (or $cvcl_213 AT0_PROC8_B ) $cvcl_61 )) (or (or $cvcl_213 $cvcl_58 ) AT1_PROC8_C )) (or (or $cvcl_213 AT0_PROC8_C ) $cvcl_62 )) (or (or $cvcl_213 $cvcl_59 ) AT1_PROC8_CS )) (or (or $cvcl_213 AT0_PROC8_CS ) $cvcl_63 )) (or $cvcl_213 $cvcl_230 )) (or $cvcl_213 $cvcl_214 )) (or $cvcl_213 $cvcl_138 )) (or (or $cvcl_215 $cvcl_64 ) AT1_PROC9_A )) (or (or $cvcl_215 AT0_PROC9_A ) $cvcl_68 )) (or (or $cvcl_215 $cvcl_65 ) AT1_PROC9_B )) (or (or $cvcl_215 AT0_PROC9_B ) $cvcl_69 )) (or (or $cvcl_215 $cvcl_66 ) AT1_PROC9_C )) (or (or $cvcl_215 AT0_PROC9_C ) $cvcl_70 )) (or (or $cvcl_215 $cvcl_67 ) AT1_PROC9_CS )) (or (or $cvcl_215 AT0_PROC9_CS ) $cvcl_71 )) (or $cvcl_215 $cvcl_231 )) (or $cvcl_215 $cvcl_216 )) (or $cvcl_215 $cvcl_138 )) (or (or $cvcl_217 $cvcl_72 ) AT1_PROC10_A )) (or (or $cvcl_217 AT0_PROC10_A ) $cvcl_76 )) (or (or $cvcl_217 $cvcl_73 ) AT1_PROC10_B )) (or (or $cvcl_217 AT0_PROC10_B ) $cvcl_77 )) (or (or $cvcl_217 $cvcl_74 ) AT1_PROC10_C )) (or (or $cvcl_217 AT0_PROC10_C ) $cvcl_78 )) (or (or $cvcl_217 $cvcl_75 ) AT1_PROC10_CS )) (or (or $cvcl_217 AT0_PROC10_CS ) $cvcl_79 )) (or $cvcl_217 $cvcl_232 )) (or $cvcl_217 $cvcl_218 )) (or $cvcl_217 $cvcl_138 )) (or (or $cvcl_219 $cvcl_80 ) AT1_PROC11_A )) (or (or $cvcl_219 AT0_PROC11_A ) $cvcl_84 )) (or (or $cvcl_219 $cvcl_81 ) AT1_PROC11_B )) (or (or $cvcl_219 AT0_PROC11_B ) $cvcl_85 )) (or (or $cvcl_219 $cvcl_82 ) AT1_PROC11_C )) (or (or $cvcl_219 AT0_PROC11_C ) $cvcl_86 )) (or (or $cvcl_219 $cvcl_83 ) AT1_PROC11_CS )) (or (or $cvcl_219 AT0_PROC11_CS ) $cvcl_87 )) (or $cvcl_219 $cvcl_233 )) (or $cvcl_219 $cvcl_220 )) (or $cvcl_219 $cvcl_138 )) (or (or $cvcl_221 $cvcl_0 ) AT1_PROC1_A )) (or (or $cvcl_221 AT0_PROC1_A ) $cvcl_4 )) (or (or $cvcl_221 $cvcl_1 ) AT1_PROC1_B )) (or (or $cvcl_221 AT0_PROC1_B ) $cvcl_5 )) (or (or $cvcl_221 $cvcl_2 ) AT1_PROC1_C )) (or (or $cvcl_221 AT0_PROC1_C ) $cvcl_6 )) (or (or $cvcl_221 $cvcl_3 ) AT1_PROC1_CS )) (or (or $cvcl_221 AT0_PROC1_CS ) $cvcl_7 )) (or $cvcl_221 $cvcl_200 )) (or $cvcl_221 $cvcl_222 )) $cvcl_224) (or (or $cvcl_221 $cvcl_8 ) AT1_PROC2_A )) (or (or $cvcl_221 AT0_PROC2_A ) $cvcl_12 )) (or (or $cvcl_221 $cvcl_9 ) AT1_PROC2_B )) (or (or $cvcl_221 AT0_PROC2_B ) $cvcl_13 )) (or (or $cvcl_221 $cvcl_10 ) AT1_PROC2_C )) (or (or $cvcl_221 AT0_PROC2_C ) $cvcl_14 )) (or (or $cvcl_221 $cvcl_11 ) AT1_PROC2_CS )) (or (or $cvcl_221 AT0_PROC2_CS ) $cvcl_15 )) (or $cvcl_221 $cvcl_202 )) (or $cvcl_221 $cvcl_223 )) $cvcl_224) (or (or $cvcl_221 $cvcl_16 ) AT1_PROC3_A )) (or (or $cvcl_221 AT0_PROC3_A ) $cvcl_20 )) (or (or $cvcl_221 $cvcl_17 ) AT1_PROC3_B )) (or (or $cvcl_221 AT0_PROC3_B ) $cvcl_21 )) (or (or $cvcl_221 $cvcl_18 ) AT1_PROC3_C )) (or (or $cvcl_221 AT0_PROC3_C ) $cvcl_22 )) (or (or $cvcl_221 $cvcl_19 ) AT1_PROC3_CS )) (or (or $cvcl_221 AT0_PROC3_CS ) $cvcl_23 )) (or $cvcl_221 $cvcl_204 )) (or $cvcl_221 $cvcl_225 )) $cvcl_224) (or (or $cvcl_221 $cvcl_24 ) AT1_PROC4_A )) (or (or $cvcl_221 AT0_PROC4_A ) $cvcl_28 )) (or (or $cvcl_221 $cvcl_25 ) AT1_PROC4_B )) (or (or $cvcl_221 AT0_PROC4_B ) $cvcl_29 )) (or (or $cvcl_221 $cvcl_26 ) AT1_PROC4_C )) (or (or $cvcl_221 AT0_PROC4_C ) $cvcl_30 )) (or (or $cvcl_221 $cvcl_27 ) AT1_PROC4_CS )) (or (or $cvcl_221 AT0_PROC4_CS ) $cvcl_31 )) (or $cvcl_221 $cvcl_206 )) (or $cvcl_221 $cvcl_226 )) $cvcl_224) (or (or $cvcl_221 $cvcl_32 ) AT1_PROC5_A )) (or (or $cvcl_221 AT0_PROC5_A ) $cvcl_36 )) (or (or $cvcl_221 $cvcl_33 ) AT1_PROC5_B )) (or (or $cvcl_221 AT0_PROC5_B ) $cvcl_37 )) (or (or $cvcl_221 $cvcl_34 ) AT1_PROC5_C )) (or (or $cvcl_221 AT0_PROC5_C ) $cvcl_38 )) (or (or $cvcl_221 $cvcl_35 ) AT1_PROC5_CS )) (or (or $cvcl_221 AT0_PROC5_CS ) $cvcl_39 )) (or $cvcl_221 $cvcl_208 )) (or $cvcl_221 $cvcl_227 )) $cvcl_224) (or (or $cvcl_221 $cvcl_40 ) AT1_PROC6_A )) (or (or $cvcl_221 AT0_PROC6_A ) $cvcl_44 )) (or (or $cvcl_221 $cvcl_41 ) AT1_PROC6_B )) (or (or $cvcl_221 AT0_PROC6_B ) $cvcl_45 )) (or (or $cvcl_221 $cvcl_42 ) AT1_PROC6_C )) (or (or $cvcl_221 AT0_PROC6_C ) $cvcl_46 )) (or (or $cvcl_221 $cvcl_43 ) AT1_PROC6_CS )) (or (or $cvcl_221 AT0_PROC6_CS ) $cvcl_47 )) (or $cvcl_221 $cvcl_210 )) (or $cvcl_221 $cvcl_228 )) $cvcl_224) (or (or $cvcl_221 $cvcl_48 ) AT1_PROC7_A )) (or (or $cvcl_221 AT0_PROC7_A ) $cvcl_52 )) (or (or $cvcl_221 $cvcl_49 ) AT1_PROC7_B )) (or (or $cvcl_221 AT0_PROC7_B ) $cvcl_53 )) (or (or $cvcl_221 $cvcl_50 ) AT1_PROC7_C )) (or (or $cvcl_221 AT0_PROC7_C ) $cvcl_54 )) (or (or $cvcl_221 $cvcl_51 ) AT1_PROC7_CS )) (or (or $cvcl_221 AT0_PROC7_CS ) $cvcl_55 )) (or $cvcl_221 $cvcl_212 )) (or $cvcl_221 $cvcl_229 )) $cvcl_224) (or (or $cvcl_221 $cvcl_56 ) AT1_PROC8_A )) (or (or $cvcl_221 AT0_PROC8_A ) $cvcl_60 )) (or (or $cvcl_221 $cvcl_57 ) AT1_PROC8_B )) (or (or $cvcl_221 AT0_PROC8_B ) $cvcl_61 )) (or (or $cvcl_221 $cvcl_58 ) AT1_PROC8_C )) (or (or $cvcl_221 AT0_PROC8_C ) $cvcl_62 )) (or (or $cvcl_221 $cvcl_59 ) AT1_PROC8_CS )) (or (or $cvcl_221 AT0_PROC8_CS ) $cvcl_63 )) (or $cvcl_221 $cvcl_214 )) (or $cvcl_221 $cvcl_230 )) $cvcl_224) (or (or $cvcl_221 $cvcl_64 ) AT1_PROC9_A )) (or (or $cvcl_221 AT0_PROC9_A ) $cvcl_68 )) (or (or $cvcl_221 $cvcl_65 ) AT1_PROC9_B )) (or (or $cvcl_221 AT0_PROC9_B ) $cvcl_69 )) (or (or $cvcl_221 $cvcl_66 ) AT1_PROC9_C )) (or (or $cvcl_221 AT0_PROC9_C ) $cvcl_70 )) (or (or $cvcl_221 $cvcl_67 ) AT1_PROC9_CS )) (or (or $cvcl_221 AT0_PROC9_CS ) $cvcl_71 )) (or $cvcl_221 $cvcl_216 )) (or $cvcl_221 $cvcl_231 )) $cvcl_224) (or (or $cvcl_221 $cvcl_72 ) AT1_PROC10_A )) (or (or $cvcl_221 AT0_PROC10_A ) $cvcl_76 )) (or (or $cvcl_221 $cvcl_73 ) AT1_PROC10_B )) (or (or $cvcl_221 AT0_PROC10_B ) $cvcl_77 )) (or (or $cvcl_221 $cvcl_74 ) AT1_PROC10_C )) (or (or $cvcl_221 AT0_PROC10_C ) $cvcl_78 )) (or (or $cvcl_221 $cvcl_75 ) AT1_PROC10_CS )) (or (or $cvcl_221 AT0_PROC10_CS ) $cvcl_79 )) (or $cvcl_221 $cvcl_218 )) (or $cvcl_221 $cvcl_232 )) $cvcl_224) (or (or $cvcl_221 $cvcl_80 ) AT1_PROC11_A )) (or (or $cvcl_221 AT0_PROC11_A ) $cvcl_84 )) (or (or $cvcl_221 $cvcl_81 ) AT1_PROC11_B )) (or (or $cvcl_221 AT0_PROC11_B ) $cvcl_85 )) (or (or $cvcl_221 $cvcl_82 ) AT1_PROC11_C )) (or (or $cvcl_221 AT0_PROC11_C ) $cvcl_86 )) (or (or $cvcl_221 $cvcl_83 ) AT1_PROC11_CS )) (or (or $cvcl_221 AT0_PROC11_CS ) $cvcl_87 )) (or $cvcl_221 $cvcl_220 )) (or $cvcl_221 $cvcl_233 )) $cvcl_224) (or $cvcl_200 $cvcl_234 )) (or $cvcl_246 (not $cvcl_234) )) (or $cvcl_202 $cvcl_235 )) (or $cvcl_252 (not $cvcl_235) )) (or $cvcl_204 $cvcl_236 )) (or $cvcl_256 (not $cvcl_236) )) (or $cvcl_206 $cvcl_237 )) (or $cvcl_260 (not $cvcl_237) )) (or $cvcl_208 $cvcl_238 )) (or $cvcl_264 (not $cvcl_238) )) (or $cvcl_210 $cvcl_239 )) (or $cvcl_268 (not $cvcl_239) )) (or $cvcl_212 $cvcl_240 )) (or $cvcl_272 (not $cvcl_240) )) (or $cvcl_214 $cvcl_241 )) (or $cvcl_276 (not $cvcl_241) )) (or $cvcl_216 $cvcl_242 )) (or $cvcl_280 (not $cvcl_242) )) (or $cvcl_218 $cvcl_243 )) (or $cvcl_284 (not $cvcl_243) )) (or $cvcl_220 $cvcl_244 )) (or $cvcl_288 (not $cvcl_244) )) (or $cvcl_138 $cvcl_245 )) (or $cvcl_247 $cvcl_251 )) (or (or (or $cvcl_88 $cvcl_246 ) $cvcl_247 ) $cvcl_248 )) (or (or (or $cvcl_249 $cvcl_200 ) $cvcl_247 ) $cvcl_248 )) (or (or $cvcl_250 $cvcl_138 ) $cvcl_248 )) (or (or $cvcl_250 $cvcl_247 ) $cvcl_90 )) (or (or (or (not (< AT0_Z AT0_PROC1_X)) $cvcl_246 ) $cvcl_251 ) (< AT1_Z AT1_PROC1_X) )) (or (or (or $cvcl_92 $cvcl_252 ) $cvcl_247 ) $cvcl_253 )) (or (or (or $cvcl_254 $cvcl_202 ) $cvcl_247 ) $cvcl_253 )) (or (or $cvcl_255 $cvcl_138 ) $cvcl_253 )) (or (or $cvcl_255 $cvcl_247 ) $cvcl_94 )) (or (or (or (not (< AT0_Z AT0_PROC2_X)) $cvcl_252 ) $cvcl_251 ) (< AT1_Z AT1_PROC2_X) )) (or (or (or $cvcl_96 $cvcl_256 ) $cvcl_247 ) $cvcl_257 )) (or (or (or $cvcl_258 $cvcl_204 ) $cvcl_247 ) $cvcl_257 )) (or (or $cvcl_259 $cvcl_138 ) $cvcl_257 )) (or (or $cvcl_259 $cvcl_247 ) $cvcl_98 )) (or (or (or (not (< AT0_Z AT0_PROC3_X)) $cvcl_256 ) $cvcl_251 ) (< AT1_Z AT1_PROC3_X) )) (or (or (or $cvcl_100 $cvcl_260 ) $cvcl_247 ) $cvcl_261 )) (or (or (or $cvcl_262 $cvcl_206 ) $cvcl_247 ) $cvcl_261 )) (or (or $cvcl_263 $cvcl_138 ) $cvcl_261 )) (or (or $cvcl_263 $cvcl_247 ) $cvcl_102 )) (or (or (or (not (< AT0_Z AT0_PROC4_X)) $cvcl_260 ) $cvcl_251 ) (< AT1_Z AT1_PROC4_X) )) (or (or (or $cvcl_104 $cvcl_264 ) $cvcl_247 ) $cvcl_265 )) (or (or (or $cvcl_266 $cvcl_208 ) $cvcl_247 ) $cvcl_265 )) (or (or $cvcl_267 $cvcl_138 ) $cvcl_265 )) (or (or $cvcl_267 $cvcl_247 ) $cvcl_106 )) (or (or (or (not (< AT0_Z AT0_PROC5_X)) $cvcl_264 ) $cvcl_251 ) (< AT1_Z AT1_PROC5_X) )) (or (or (or $cvcl_108 $cvcl_268 ) $cvcl_247 ) $cvcl_269 )) (or (or (or $cvcl_270 $cvcl_210 ) $cvcl_247 ) $cvcl_269 )) (or (or $cvcl_271 $cvcl_138 ) $cvcl_269 )) (or (or $cvcl_271 $cvcl_247 ) $cvcl_110 )) (or (or (or (not (< AT0_Z AT0_PROC6_X)) $cvcl_268 ) $cvcl_251 ) (< AT1_Z AT1_PROC6_X) )) (or (or (or $cvcl_112 $cvcl_272 ) $cvcl_247 ) $cvcl_273 )) (or (or (or $cvcl_274 $cvcl_212 ) $cvcl_247 ) $cvcl_273 )) (or (or $cvcl_275 $cvcl_138 ) $cvcl_273 )) (or (or $cvcl_275 $cvcl_247 ) $cvcl_114 )) (or (or (or (not (< AT0_Z AT0_PROC7_X)) $cvcl_272 ) $cvcl_251 ) (< AT1_Z AT1_PROC7_X) )) (or (or (or $cvcl_116 $cvcl_276 ) $cvcl_247 ) $cvcl_277 )) (or (or (or $cvcl_278 $cvcl_214 ) $cvcl_247 ) $cvcl_277 )) (or (or $cvcl_279 $cvcl_138 ) $cvcl_277 )) (or (or $cvcl_279 $cvcl_247 ) $cvcl_118 )) (or (or (or (not (< AT0_Z AT0_PROC8_X)) $cvcl_276 ) $cvcl_251 ) (< AT1_Z AT1_PROC8_X) )) (or (or (or $cvcl_120 $cvcl_280 ) $cvcl_247 ) $cvcl_281 )) (or (or (or $cvcl_282 $cvcl_216 ) $cvcl_247 ) $cvcl_281 )) (or (or $cvcl_283 $cvcl_138 ) $cvcl_281 )) (or (or $cvcl_283 $cvcl_247 ) $cvcl_122 )) (or (or (or (not (< AT0_Z AT0_PROC9_X)) $cvcl_280 ) $cvcl_251 ) (< AT1_Z AT1_PROC9_X) )) (or (or (or $cvcl_124 $cvcl_284 ) $cvcl_247 ) $cvcl_285 )) (or (or (or $cvcl_286 $cvcl_218 ) $cvcl_247 ) $cvcl_285 )) (or (or $cvcl_287 $cvcl_138 ) $cvcl_285 )) (or (or $cvcl_287 $cvcl_247 ) $cvcl_126 )) (or (or (or (not (< AT0_Z AT0_PROC10_X)) $cvcl_284 ) $cvcl_251 ) (< AT1_Z AT1_PROC10_X) )) (or (or (or $cvcl_128 $cvcl_288 ) $cvcl_247 ) $cvcl_289 )) (or (or (or $cvcl_290 $cvcl_220 ) $cvcl_247 ) $cvcl_289 )) (or (or $cvcl_291 $cvcl_138 ) $cvcl_289 )) (or (or $cvcl_291 $cvcl_247 ) $cvcl_130 )) (or (or (or (not (< AT0_Z AT0_PROC11_X)) $cvcl_288 ) $cvcl_251 ) (< AT1_Z AT1_PROC11_X) )) AT0_PROC1_A) AT0_PROC2_A) AT0_PROC3_A) AT0_PROC4_A) AT0_PROC5_A) AT0_PROC6_A) AT0_PROC7_A) AT0_PROC8_A) AT0_PROC9_A) AT0_PROC10_A) AT0_PROC11_A) $cvcl_88) $cvcl_92) $cvcl_96) $cvcl_100) $cvcl_104) $cvcl_108) $cvcl_112) $cvcl_116) $cvcl_120) $cvcl_124) $cvcl_128) AT0_ID0) (or (or (or (or (or (or (or (or (or (or $cvcl_199 $cvcl_201 ) $cvcl_203 ) $cvcl_205 ) $cvcl_207 ) $cvcl_209 ) $cvcl_211 ) $cvcl_213 ) $cvcl_215 ) $cvcl_217 ) $cvcl_219 )) (or $cvcl_292 $cvcl_293 )) (or $cvcl_292 $cvcl_294 )) (or $cvcl_292 $cvcl_295 )) (or $cvcl_292 $cvcl_296 )) (or $cvcl_292 $cvcl_297 )) (or $cvcl_292 $cvcl_298 )) (or $cvcl_292 $cvcl_299 )) (or $cvcl_292 $cvcl_300 )) (or $cvcl_292 $cvcl_301 )) (or $cvcl_292 $cvcl_302 )) (or $cvcl_292 $cvcl_303 )) (or $cvcl_293 $cvcl_294 )) (or $cvcl_293 $cvcl_295 )) (or $cvcl_293 $cvcl_296 )) (or $cvcl_293 $cvcl_297 )) (or $cvcl_293 $cvcl_298 )) (or $cvcl_293 $cvcl_299 )) (or $cvcl_293 $cvcl_300 )) (or $cvcl_293 $cvcl_301 )) (or $cvcl_293 $cvcl_302 )) (or $cvcl_293 $cvcl_303 )) (or $cvcl_294 $cvcl_295 )) (or $cvcl_294 $cvcl_296 )) (or $cvcl_294 $cvcl_297 )) (or $cvcl_294 $cvcl_298 )) (or $cvcl_294 $cvcl_299 )) (or $cvcl_294 $cvcl_300 )) (or $cvcl_294 $cvcl_301 )) (or $cvcl_294 $cvcl_302 )) (or $cvcl_294 $cvcl_303 )) (or $cvcl_295 $cvcl_296 )) (or $cvcl_295 $cvcl_297 )) (or $cvcl_295 $cvcl_298 )) (or $cvcl_295 $cvcl_299 )) (or $cvcl_295 $cvcl_300 )) (or $cvcl_295 $cvcl_301 )) (or $cvcl_295 $cvcl_302 )) (or $cvcl_295 $cvcl_303 )) (or $cvcl_296 $cvcl_297 )) (or $cvcl_296 $cvcl_298 )) (or $cvcl_296 $cvcl_299 )) (or $cvcl_296 $cvcl_300 )) (or $cvcl_296 $cvcl_301 )) (or $cvcl_296 $cvcl_302 )) (or $cvcl_296 $cvcl_303 )) (or $cvcl_297 $cvcl_298 )) (or $cvcl_297 $cvcl_299 )) (or $cvcl_297 $cvcl_300 )) (or $cvcl_297 $cvcl_301 )) (or $cvcl_297 $cvcl_302 )) (or $cvcl_297 $cvcl_303 )) (or $cvcl_298 $cvcl_299 )) (or $cvcl_298 $cvcl_300 )) (or $cvcl_298 $cvcl_301 )) (or $cvcl_298 $cvcl_302 )) (or $cvcl_298 $cvcl_303 )) (or $cvcl_299 $cvcl_300 )) (or $cvcl_299 $cvcl_301 )) (or $cvcl_299 $cvcl_302 )) (or $cvcl_299 $cvcl_303 )) (or $cvcl_300 $cvcl_301 )) (or $cvcl_300 $cvcl_302 )) (or $cvcl_300 $cvcl_303 )) (or $cvcl_301 $cvcl_302 )) (or $cvcl_301 $cvcl_303 )) (or $cvcl_302 $cvcl_303 )) (or $cvcl_304 $cvcl_305 )) (or $cvcl_304 $cvcl_306 )) (or $cvcl_304 $cvcl_307 )) (or $cvcl_304 $cvcl_308 )) (or $cvcl_304 $cvcl_309 )) (or $cvcl_304 $cvcl_310 )) (or $cvcl_304 $cvcl_311 )) (or $cvcl_304 $cvcl_312 )) (or $cvcl_304 $cvcl_313 )) (or $cvcl_304 $cvcl_314 )) (or $cvcl_304 $cvcl_315 )) (or $cvcl_305 $cvcl_306 )) (or $cvcl_305 $cvcl_307 )) (or $cvcl_305 $cvcl_308 )) (or $cvcl_305 $cvcl_309 )) (or $cvcl_305 $cvcl_310 )) (or $cvcl_305 $cvcl_311 )) (or $cvcl_305 $cvcl_312 )) (or $cvcl_305 $cvcl_313 )) (or $cvcl_305 $cvcl_314 )) (or $cvcl_305 $cvcl_315 )) (or $cvcl_306 $cvcl_307 )) (or $cvcl_306 $cvcl_308 )) (or $cvcl_306 $cvcl_309 )) (or $cvcl_306 $cvcl_310 )) (or $cvcl_306 $cvcl_311 )) (or $cvcl_306 $cvcl_312 )) (or $cvcl_306 $cvcl_313 )) (or $cvcl_306 $cvcl_314 )) (or $cvcl_306 $cvcl_315 )) (or $cvcl_307 $cvcl_308 )) (or $cvcl_307 $cvcl_309 )) (or $cvcl_307 $cvcl_310 )) (or $cvcl_307 $cvcl_311 )) (or $cvcl_307 $cvcl_312 )) (or $cvcl_307 $cvcl_313 )) (or $cvcl_307 $cvcl_314 )) (or $cvcl_307 $cvcl_315 )) (or $cvcl_308 $cvcl_309 )) (or $cvcl_308 $cvcl_310 )) (or $cvcl_308 $cvcl_311 )) (or $cvcl_308 $cvcl_312 )) (or $cvcl_308 $cvcl_313 )) (or $cvcl_308 $cvcl_314 )) (or $cvcl_308 $cvcl_315 )) (or $cvcl_309 $cvcl_310 )) (or $cvcl_309 $cvcl_311 )) (or $cvcl_309 $cvcl_312 )) (or $cvcl_309 $cvcl_313 )) (or $cvcl_309 $cvcl_314 )) (or $cvcl_309 $cvcl_315 )) (or $cvcl_310 $cvcl_311 )) (or $cvcl_310 $cvcl_312 )) (or $cvcl_310 $cvcl_313 )) (or $cvcl_310 $cvcl_314 )) (or $cvcl_310 $cvcl_315 )) (or $cvcl_311 $cvcl_312 )) (or $cvcl_311 $cvcl_313 )) (or $cvcl_311 $cvcl_314 )) (or $cvcl_311 $cvcl_315 )) (or $cvcl_312 $cvcl_313 )) (or $cvcl_312 $cvcl_314 )) (or $cvcl_312 $cvcl_315 )) (or $cvcl_313 $cvcl_314 )) (or $cvcl_313 $cvcl_315 )) (or $cvcl_314 $cvcl_315 )) (or $cvcl_132 AT0_ID0 )) (or $cvcl_132 AT1_ID0 )) (or $cvcl_133 AT1_ID1 )) (or $cvcl_135 AT0_ID0 )) (or $cvcl_135 AT1_ID0 )) (or $cvcl_136 AT0_ID1 )) (or $cvcl_136 AT1_ID1 )) (or $cvcl_137 AT1_ID0 )) (or (or $cvcl_221 $cvcl_293 ) AT1_ID1 )) (or $cvcl_139 AT0_ID0 )) (or $cvcl_139 AT1_ID0 )) (or $cvcl_140 AT1_ID2 )) (or $cvcl_142 AT0_ID0 )) (or $cvcl_142 AT1_ID0 )) (or $cvcl_143 AT0_ID2 )) (or $cvcl_143 AT1_ID2 )) (or $cvcl_144 AT1_ID0 )) (or (or $cvcl_221 $cvcl_294 ) AT1_ID2 )) (or $cvcl_145 AT0_ID0 )) (or $cvcl_145 AT1_ID0 )) (or $cvcl_146 AT1_ID3 )) (or $cvcl_148 AT0_ID0 )) (or $cvcl_148 AT1_ID0 )) (or $cvcl_149 AT0_ID3 )) (or $cvcl_149 AT1_ID3 )) (or $cvcl_150 AT1_ID0 )) (or (or $cvcl_221 $cvcl_295 ) AT1_ID3 )) (or $cvcl_151 AT0_ID0 )) (or $cvcl_151 AT1_ID0 )) (or $cvcl_152 AT1_ID4 )) (or $cvcl_154 AT0_ID0 )) (or $cvcl_154 AT1_ID0 )) (or $cvcl_155 AT0_ID4 )) (or $cvcl_155 AT1_ID4 )) (or $cvcl_156 AT1_ID0 )) (or (or $cvcl_221 $cvcl_296 ) AT1_ID4 )) (or $cvcl_157 AT0_ID0 )) (or $cvcl_157 AT1_ID0 )) (or $cvcl_158 AT1_ID5 )) (or $cvcl_160 AT0_ID0 )) (or $cvcl_160 AT1_ID0 )) (or $cvcl_161 AT0_ID5 )) (or $cvcl_161 AT1_ID5 )) (or $cvcl_162 AT1_ID0 )) (or (or $cvcl_221 $cvcl_297 ) AT1_ID5 )) (or $cvcl_163 AT0_ID0 )) (or $cvcl_163 AT1_ID0 )) (or $cvcl_164 AT1_ID6 )) (or $cvcl_166 AT0_ID0 )) (or $cvcl_166 AT1_ID0 )) (or $cvcl_167 AT0_ID6 )) (or $cvcl_167 AT1_ID6 )) (or $cvcl_168 AT1_ID0 )) (or (or $cvcl_221 $cvcl_298 ) AT1_ID6 )) (or $cvcl_169 AT0_ID0 )) (or $cvcl_169 AT1_ID0 )) (or $cvcl_170 AT1_ID7 )) (or $cvcl_172 AT0_ID0 )) (or $cvcl_172 AT1_ID0 )) (or $cvcl_173 AT0_ID7 )) (or $cvcl_173 AT1_ID7 )) (or $cvcl_174 AT1_ID0 )) (or (or $cvcl_221 $cvcl_299 ) AT1_ID7 )) (or $cvcl_175 AT0_ID0 )) (or $cvcl_175 AT1_ID0 )) (or $cvcl_176 AT1_ID8 )) (or $cvcl_178 AT0_ID0 )) (or $cvcl_178 AT1_ID0 )) (or $cvcl_179 AT0_ID8 )) (or $cvcl_179 AT1_ID8 )) (or $cvcl_180 AT1_ID0 )) (or (or $cvcl_221 $cvcl_300 ) AT1_ID8 )) (or $cvcl_181 AT0_ID0 )) (or $cvcl_181 AT1_ID0 )) (or $cvcl_182 AT1_ID9 )) (or $cvcl_184 AT0_ID0 )) (or $cvcl_184 AT1_ID0 )) (or $cvcl_185 AT0_ID9 )) (or $cvcl_185 AT1_ID9 )) (or $cvcl_186 AT1_ID0 )) (or (or $cvcl_221 $cvcl_301 ) AT1_ID9 )) (or $cvcl_187 AT0_ID0 )) (or $cvcl_187 AT1_ID0 )) (or $cvcl_188 AT1_ID10 )) (or $cvcl_190 AT0_ID0 )) (or $cvcl_190 AT1_ID0 )) (or $cvcl_191 AT0_ID10 )) (or $cvcl_191 AT1_ID10 )) (or $cvcl_192 AT1_ID0 )) (or (or $cvcl_221 $cvcl_302 ) AT1_ID10 )) (or $cvcl_193 AT0_ID0 )) (or $cvcl_193 AT1_ID0 )) (or $cvcl_194 AT1_ID11 )) (or $cvcl_196 AT0_ID0 )) (or $cvcl_196 AT1_ID0 )) (or $cvcl_197 AT0_ID11 )) (or $cvcl_197 AT1_ID11 )) (or $cvcl_198 AT1_ID0 )) (or (or $cvcl_221 $cvcl_303 ) AT1_ID11 )) (or (or $cvcl_221 $cvcl_292 ) AT1_ID0 )) (or $cvcl_4 AT1_PROC1_A )) (or AT1_PROC1_A $cvcl_4 )) (or $cvcl_5 AT1_PROC1_B )) (or AT1_PROC1_B $cvcl_5 )) (or $cvcl_6 AT1_PROC1_C )) (or AT1_PROC1_C $cvcl_6 )) (or $cvcl_7 AT1_PROC1_CS )) (or AT1_PROC1_CS $cvcl_7 )) (or $cvcl_305 AT1_ID1 )) (or AT1_ID1 $cvcl_305 )) (= (- AT1_PROC1_X AT1_Z) (- AT1_PROC1_X AT1_Z))) (or $cvcl_12 AT1_PROC2_A )) (or AT1_PROC2_A $cvcl_12 )) (or $cvcl_13 AT1_PROC2_B )) (or AT1_PROC2_B $cvcl_13 )) (or $cvcl_14 AT1_PROC2_C )) (or AT1_PROC2_C $cvcl_14 )) (or $cvcl_15 AT1_PROC2_CS )) (or AT1_PROC2_CS $cvcl_15 )) (or $cvcl_306 AT1_ID2 )) (or AT1_ID2 $cvcl_306 )) (= (- AT1_PROC2_X AT1_Z) (- AT1_PROC2_X AT1_Z))) (or $cvcl_20 AT1_PROC3_A )) (or AT1_PROC3_A $cvcl_20 )) (or $cvcl_21 AT1_PROC3_B )) (or AT1_PROC3_B $cvcl_21 )) (or $cvcl_22 AT1_PROC3_C )) (or AT1_PROC3_C $cvcl_22 )) (or $cvcl_23 AT1_PROC3_CS )) (or AT1_PROC3_CS $cvcl_23 )) (or $cvcl_307 AT1_ID3 )) (or AT1_ID3 $cvcl_307 )) (= (- AT1_PROC3_X AT1_Z) (- AT1_PROC3_X AT1_Z))) (or $cvcl_28 AT1_PROC4_A )) (or AT1_PROC4_A $cvcl_28 )) (or $cvcl_29 AT1_PROC4_B )) (or AT1_PROC4_B $cvcl_29 )) (or $cvcl_30 AT1_PROC4_C )) (or AT1_PROC4_C $cvcl_30 )) (or $cvcl_31 AT1_PROC4_CS )) (or AT1_PROC4_CS $cvcl_31 )) (or $cvcl_308 AT1_ID4 )) (or AT1_ID4 $cvcl_308 )) (= (- AT1_PROC4_X AT1_Z) (- AT1_PROC4_X AT1_Z))) (or $cvcl_36 AT1_PROC5_A )) (or AT1_PROC5_A $cvcl_36 )) (or $cvcl_37 AT1_PROC5_B )) (or AT1_PROC5_B $cvcl_37 )) (or $cvcl_38 AT1_PROC5_C )) (or AT1_PROC5_C $cvcl_38 )) (or $cvcl_39 AT1_PROC5_CS )) (or AT1_PROC5_CS $cvcl_39 )) (or $cvcl_309 AT1_ID5 )) (or AT1_ID5 $cvcl_309 )) (= (- AT1_PROC5_X AT1_Z) (- AT1_PROC5_X AT1_Z))) (or $cvcl_44 AT1_PROC6_A )) (or AT1_PROC6_A $cvcl_44 )) (or $cvcl_45 AT1_PROC6_B )) (or AT1_PROC6_B $cvcl_45 )) (or $cvcl_46 AT1_PROC6_C )) (or AT1_PROC6_C $cvcl_46 )) (or $cvcl_47 AT1_PROC6_CS )) (or AT1_PROC6_CS $cvcl_47 )) (or $cvcl_310 AT1_ID6 )) (or AT1_ID6 $cvcl_310 )) (= (- AT1_PROC6_X AT1_Z) (- AT1_PROC6_X AT1_Z))) (or $cvcl_52 AT1_PROC7_A )) (or AT1_PROC7_A $cvcl_52 )) (or $cvcl_53 AT1_PROC7_B )) (or AT1_PROC7_B $cvcl_53 )) (or $cvcl_54 AT1_PROC7_C )) (or AT1_PROC7_C $cvcl_54 )) (or $cvcl_55 AT1_PROC7_CS )) (or AT1_PROC7_CS $cvcl_55 )) (or $cvcl_311 AT1_ID7 )) (or AT1_ID7 $cvcl_311 )) (= (- AT1_PROC7_X AT1_Z) (- AT1_PROC7_X AT1_Z))) (or $cvcl_60 AT1_PROC8_A )) (or AT1_PROC8_A $cvcl_60 )) (or $cvcl_61 AT1_PROC8_B )) (or AT1_PROC8_B $cvcl_61 )) (or $cvcl_62 AT1_PROC8_C )) (or AT1_PROC8_C $cvcl_62 )) (or $cvcl_63 AT1_PROC8_CS )) (or AT1_PROC8_CS $cvcl_63 )) (or $cvcl_312 AT1_ID8 )) (or AT1_ID8 $cvcl_312 )) (= (- AT1_PROC8_X AT1_Z) (- AT1_PROC8_X AT1_Z))) (or $cvcl_68 AT1_PROC9_A )) (or AT1_PROC9_A $cvcl_68 )) (or $cvcl_69 AT1_PROC9_B )) (or AT1_PROC9_B $cvcl_69 )) (or $cvcl_70 AT1_PROC9_C )) (or AT1_PROC9_C $cvcl_70 )) (or $cvcl_71 AT1_PROC9_CS )) (or AT1_PROC9_CS $cvcl_71 )) (or $cvcl_313 AT1_ID9 )) (or AT1_ID9 $cvcl_313 )) (= (- AT1_PROC9_X AT1_Z) (- AT1_PROC9_X AT1_Z))) (or $cvcl_76 AT1_PROC10_A )) (or AT1_PROC10_A $cvcl_76 )) (or $cvcl_77 AT1_PROC10_B )) (or AT1_PROC10_B $cvcl_77 )) (or $cvcl_78 AT1_PROC10_C )) (or AT1_PROC10_C $cvcl_78 )) (or $cvcl_79 AT1_PROC10_CS )) (or AT1_PROC10_CS $cvcl_79 )) (or $cvcl_314 AT1_ID10 )) (or AT1_ID10 $cvcl_314 )) (= (- AT1_PROC10_X AT1_Z) (- AT1_PROC10_X AT1_Z))) (or $cvcl_84 AT1_PROC11_A )) (or AT1_PROC11_A $cvcl_84 )) (or $cvcl_85 AT1_PROC11_B )) (or AT1_PROC11_B $cvcl_85 )) (or $cvcl_86 AT1_PROC11_C )) (or AT1_PROC11_C $cvcl_86 )) (or $cvcl_87 AT1_PROC11_CS )) (or AT1_PROC11_CS $cvcl_87 )) (or $cvcl_315 AT1_ID11 )) (or AT1_ID11 $cvcl_315 )) (= (- AT1_PROC11_X AT1_Z) (- AT1_PROC11_X AT1_Z))) AT1_PROC1_B) $cvcl_7))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )