(benchmark FISCHER6_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_PROC6_SW_B_C_TAU)) :extrapreds ((AT1_PROC5_CS)) :extrafuns ((AT0_PROC1_X Int)) :extrapreds ((AT0_PROC6_C)) :extrapreds ((AT0_PROC6_B)) :extrapreds ((AT0_PROC6_A)) :extrapreds ((AT0_ID0)) :extrapreds ((AT1_PROC2_C)) :extrapreds ((AT0_ID1)) :extrapreds ((AT1_PROC2_B)) :extrapreds ((AT0_ID2)) :extrapreds ((AT0_PROC6_CS)) :extrapreds ((AT1_PROC2_A)) :extrapreds ((AT0_ID3)) :extrapreds ((AT0_PROC3_SW_CS_A_TAU)) :extrapreds ((AT0_ID4)) :extrapreds ((AT0_ID5)) :extrapreds ((AT1_PROC2_CS)) :extrapreds ((AT0_ID6)) :extrafuns ((AT0_PROC4_X Int)) :extrapreds ((AT0_PROC3_TAU)) :extrapreds ((AT0_PROC6_SW_A_B_TAU)) :extrapreds ((AT1_PROC5_C)) :extrapreds ((AT0_PROC2_SW_C_B_TAU)) :extrapreds ((AT1_PROC5_B)) :extrapreds ((AT1_PROC5_A)) :extrapreds ((AT0_PROC4_SW_C_B_TAU)) :extrapreds ((AT0_PROC1_C)) :extrapreds ((AT0_PROC1_B)) :extrapreds ((AT0_PROC1_A)) :extrapreds ((AT0_PROC6_WAIT)) :extrafuns ((AT1_PROC3_X Int)) :extrapreds ((AT0_PROC3_WAIT)) :extrapreds ((AT0_PROC2_CS)) :extrapreds ((AT0_PROC4_C)) :extrapreds ((AT0_PROC4_B)) :extrapreds ((AT1_ID0)) :extrapreds ((AT1_PROC6_CS)) :extrapreds ((AT0_PROC4_A)) :extrapreds ((AT1_ID1)) :extrapreds ((AT1_ID2)) :extrapreds ((AT1_ID3)) :extrapreds ((AT1_ID4)) :extrapreds ((AT1_ID5)) :extrapreds ((AT1_ID6)) :extrapreds ((AT0_PROC1_SW_CS_A_TAU)) :extrafuns ((AT1_PROC6_X Int)) :extrapreds ((AT0_PROC5_SW_C_B_TAU)) :extrapreds ((AT0_PROC5_CS)) :extrapreds ((AT0_PROC6_SW_C_B_TAU)) :extrapreds ((AT0_PROC5_SW_CS_A_TAU)) :extrapreds ((AT0_PROC4_TAU)) :extrafuns ((AT0_PROC2_X Int)) :extrapreds ((AT1_PROC3_CS)) :extrapreds ((AT0_PROC4_SW_A_B_TAU)) :extrapreds ((AT1_PROC3_C)) :extrapreds ((AT1_PROC3_B)) :extrapreds ((AT1_PROC3_A)) :extrafuns ((AT0_PROC5_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_PROC2_C)) :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_PROC5_SW_A_B_TAU)) :extrapreds ((AT0_PROC4_WAIT)) :extrapreds ((AT0_PROC1_TAU)) :extrapreds ((AT0_PROC1_SW_C_CS_TAU)) :extrafuns ((AT1_PROC4_X Int)) :extrapreds ((AT0_PROC4_SW_CS_A_TAU)) :extrapreds ((AT0_PROC1_WAIT)) :extrapreds ((AT0_PROC5_TAU)) :extrapreds ((AT0_PROC5_SW_C_CS_TAU)) :extrapreds ((AT0_PROC5_C)) :extrapreds ((AT0_PROC5_B)) :extrapreds ((AT0_PROC5_A)) :extrapreds ((AT0_PROC4_CS)) :extrapreds ((AT1_PROC1_C)) :extrapreds ((AT1_PROC1_B)) :extrapreds ((AT1_PROC4_CS)) :extrapreds ((AT1_PROC1_A)) :extrapreds ((AT0_PROC3_SW_A_B_TAU)) :extrapreds ((AT0_DELTA)) :extrapreds ((AT0_PROC5_SW_B_C_TAU)) :extrafuns ((AT0_PROC3_X Int)) :extrapreds ((AT0_PROC2_SW_B_C_TAU)) :extrapreds ((AT1_PROC4_C)) :extrapreds ((AT1_PROC1_CS)) :extrapreds ((AT1_PROC4_B)) :extrapreds ((AT0_PROC6_SW_CS_A_TAU)) :extrapreds ((AT1_PROC4_A)) :extrapreds ((AT0_PROC3_SW_C_CS_TAU)) :extrapreds ((AT0_PROC1_SW_A_B_TAU)) :extrapreds ((AT0_PROC2_SW_CS_A_TAU)) :extrafuns ((AT0_PROC6_X Int)) :extrapreds ((AT0_PROC2_TAU)) :extrafuns ((AT1_PROC2_X Int)) :extrapreds ((AT0_PROC4_SW_C_CS_TAU)) :extrafuns ((AT0_Z Int)) :extrapreds ((AT0_PROC6_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_PROC3_SW_C_B_TAU)) :extrapreds ((AT0_PROC2_WAIT)) :extrapreds ((AT0_PROC1_SW_B_C_TAU)) :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 (= AT0_PROC1_X AT0_Z)) (flet ($cvcl_49 (> AT0_PROC1_X AT0_Z)) (flet ($cvcl_139 (not $cvcl_48)) (flet ($cvcl_50 (= AT1_PROC1_X AT1_Z)) (flet ($cvcl_51 (> AT1_PROC1_X AT1_Z)) (flet ($cvcl_138 (not $cvcl_50)) (flet ($cvcl_52 (= AT0_PROC2_X AT0_Z)) (flet ($cvcl_53 (> AT0_PROC2_X AT0_Z)) (flet ($cvcl_144 (not $cvcl_52)) (flet ($cvcl_54 (= AT1_PROC2_X AT1_Z)) (flet ($cvcl_55 (> AT1_PROC2_X AT1_Z)) (flet ($cvcl_143 (not $cvcl_54)) (flet ($cvcl_56 (= AT0_PROC3_X AT0_Z)) (flet ($cvcl_57 (> AT0_PROC3_X AT0_Z)) (flet ($cvcl_148 (not $cvcl_56)) (flet ($cvcl_58 (= AT1_PROC3_X AT1_Z)) (flet ($cvcl_59 (> AT1_PROC3_X AT1_Z)) (flet ($cvcl_147 (not $cvcl_58)) (flet ($cvcl_60 (= AT0_PROC4_X AT0_Z)) (flet ($cvcl_61 (> AT0_PROC4_X AT0_Z)) (flet ($cvcl_152 (not $cvcl_60)) (flet ($cvcl_62 (= AT1_PROC4_X AT1_Z)) (flet ($cvcl_63 (> AT1_PROC4_X AT1_Z)) (flet ($cvcl_151 (not $cvcl_62)) (flet ($cvcl_64 (= AT0_PROC5_X AT0_Z)) (flet ($cvcl_65 (> AT0_PROC5_X AT0_Z)) (flet ($cvcl_156 (not $cvcl_64)) (flet ($cvcl_66 (= AT1_PROC5_X AT1_Z)) (flet ($cvcl_67 (> AT1_PROC5_X AT1_Z)) (flet ($cvcl_155 (not $cvcl_66)) (flet ($cvcl_68 (= AT0_PROC6_X AT0_Z)) (flet ($cvcl_69 (> AT0_PROC6_X AT0_Z)) (flet ($cvcl_160 (not $cvcl_68)) (flet ($cvcl_70 (= AT1_PROC6_X AT1_Z)) (flet ($cvcl_71 (> AT1_PROC6_X AT1_Z)) (flet ($cvcl_159 (not $cvcl_70)) (flet ($cvcl_74 (<= (- AT0_PROC1_X AT0_Z) 10)) (flet ($cvcl_81 (<= (- AT0_PROC2_X AT0_Z) 10)) (flet ($cvcl_87 (<= (- AT0_PROC3_X AT0_Z) 10)) (flet ($cvcl_93 (<= (- AT0_PROC4_X AT0_Z) 10)) (flet ($cvcl_99 (<= (- AT0_PROC5_X AT0_Z) 10)) (flet ($cvcl_105 (<= (- AT0_PROC6_X AT0_Z) 10)) (flet ($cvcl_72 (not AT0_PROC1_SW_A_B_TAU)) (flet ($cvcl_73 (not AT0_PROC1_SW_B_C_TAU)) (flet ($cvcl_75 (not AT0_PROC1_SW_C_B_TAU)) (flet ($cvcl_76 (not AT0_PROC1_SW_C_CS_TAU)) (flet ($cvcl_110 (= AT1_PROC1_X AT0_PROC1_X)) (flet ($cvcl_77 (not AT0_PROC1_SW_CS_A_TAU)) (flet ($cvcl_78 (= AT1_Z AT0_Z)) (flet ($cvcl_79 (not AT0_PROC2_SW_A_B_TAU)) (flet ($cvcl_80 (not AT0_PROC2_SW_B_C_TAU)) (flet ($cvcl_82 (not AT0_PROC2_SW_C_B_TAU)) (flet ($cvcl_83 (not AT0_PROC2_SW_C_CS_TAU)) (flet ($cvcl_112 (= AT1_PROC2_X AT0_PROC2_X)) (flet ($cvcl_84 (not AT0_PROC2_SW_CS_A_TAU)) (flet ($cvcl_85 (not AT0_PROC3_SW_A_B_TAU)) (flet ($cvcl_86 (not AT0_PROC3_SW_B_C_TAU)) (flet ($cvcl_88 (not AT0_PROC3_SW_C_B_TAU)) (flet ($cvcl_89 (not AT0_PROC3_SW_C_CS_TAU)) (flet ($cvcl_114 (= AT1_PROC3_X AT0_PROC3_X)) (flet ($cvcl_90 (not AT0_PROC3_SW_CS_A_TAU)) (flet ($cvcl_91 (not AT0_PROC4_SW_A_B_TAU)) (flet ($cvcl_92 (not AT0_PROC4_SW_B_C_TAU)) (flet ($cvcl_94 (not AT0_PROC4_SW_C_B_TAU)) (flet ($cvcl_95 (not AT0_PROC4_SW_C_CS_TAU)) (flet ($cvcl_116 (= AT1_PROC4_X AT0_PROC4_X)) (flet ($cvcl_96 (not AT0_PROC4_SW_CS_A_TAU)) (flet ($cvcl_97 (not AT0_PROC5_SW_A_B_TAU)) (flet ($cvcl_98 (not AT0_PROC5_SW_B_C_TAU)) (flet ($cvcl_100 (not AT0_PROC5_SW_C_B_TAU)) (flet ($cvcl_101 (not AT0_PROC5_SW_C_CS_TAU)) (flet ($cvcl_118 (= AT1_PROC5_X AT0_PROC5_X)) (flet ($cvcl_102 (not AT0_PROC5_SW_CS_A_TAU)) (flet ($cvcl_103 (not AT0_PROC6_SW_A_B_TAU)) (flet ($cvcl_104 (not AT0_PROC6_SW_B_C_TAU)) (flet ($cvcl_106 (not AT0_PROC6_SW_C_B_TAU)) (flet ($cvcl_107 (not AT0_PROC6_SW_C_CS_TAU)) (flet ($cvcl_120 (= AT1_PROC6_X AT0_PROC6_X)) (flet ($cvcl_108 (not AT0_PROC6_SW_CS_A_TAU)) (flet ($cvcl_109 (not AT0_PROC1_WAIT)) (flet ($cvcl_122 (not AT0_PROC1_TAU)) (flet ($cvcl_111 (not AT0_PROC2_WAIT)) (flet ($cvcl_123 (not AT0_PROC2_TAU)) (flet ($cvcl_113 (not AT0_PROC3_WAIT)) (flet ($cvcl_125 (not AT0_PROC3_TAU)) (flet ($cvcl_115 (not AT0_PROC4_WAIT)) (flet ($cvcl_126 (not AT0_PROC4_TAU)) (flet ($cvcl_117 (not AT0_PROC5_WAIT)) (flet ($cvcl_127 (not AT0_PROC5_TAU)) (flet ($cvcl_119 (not AT0_PROC6_WAIT)) (flet ($cvcl_128 (not AT0_PROC6_TAU)) (flet ($cvcl_121 (not AT0_DELTA)) (flet ($cvcl_135 (< AT1_Z AT0_Z)) (flet ($cvcl_124 (or $cvcl_121 $cvcl_135 )) (flet ($cvcl_129 (< AT1_PROC1_X AT0_PROC1_X)) (flet ($cvcl_136 (not $cvcl_110)) (flet ($cvcl_130 (< AT1_PROC2_X AT0_PROC2_X)) (flet ($cvcl_142 (not $cvcl_112)) (flet ($cvcl_131 (< AT1_PROC3_X AT0_PROC3_X)) (flet ($cvcl_146 (not $cvcl_114)) (flet ($cvcl_132 (< AT1_PROC4_X AT0_PROC4_X)) (flet ($cvcl_150 (not $cvcl_116)) (flet ($cvcl_133 (< AT1_PROC5_X AT0_PROC5_X)) (flet ($cvcl_154 (not $cvcl_118)) (flet ($cvcl_134 (< AT1_PROC6_X AT0_PROC6_X)) (flet ($cvcl_158 (not $cvcl_120)) (flet ($cvcl_137 (not $cvcl_78)) (flet ($cvcl_141 (not $cvcl_135)) (flet ($cvcl_140 (or $cvcl_139 $cvcl_136 )) (flet ($cvcl_145 (or $cvcl_144 $cvcl_142 )) (flet ($cvcl_149 (or $cvcl_148 $cvcl_146 )) (flet ($cvcl_153 (or $cvcl_152 $cvcl_150 )) (flet ($cvcl_157 (or $cvcl_156 $cvcl_154 )) (flet ($cvcl_161 (or $cvcl_160 $cvcl_158 )) (flet ($cvcl_162 (not AT0_ID0)) (flet ($cvcl_163 (not AT0_ID1)) (flet ($cvcl_164 (not AT0_ID2)) (flet ($cvcl_165 (not AT0_ID3)) (flet ($cvcl_166 (not AT0_ID4)) (flet ($cvcl_167 (not AT0_ID5)) (flet ($cvcl_168 (not AT0_ID6)) (flet ($cvcl_169 (not AT1_ID0)) (flet ($cvcl_170 (not AT1_ID1)) (flet ($cvcl_171 (not AT1_ID2)) (flet ($cvcl_172 (not AT1_ID3)) (flet ($cvcl_173 (not AT1_ID4)) (flet ($cvcl_174 (not AT1_ID5)) (flet ($cvcl_175 (not AT1_ID6)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (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_139 (not $cvcl_49) )) (or $cvcl_50 $cvcl_51 )) (or $cvcl_138 (not $cvcl_51) )) (or $cvcl_52 $cvcl_53 )) (or $cvcl_144 (not $cvcl_53) )) (or $cvcl_54 $cvcl_55 )) (or $cvcl_143 (not $cvcl_55) )) (or $cvcl_56 $cvcl_57 )) (or $cvcl_148 (not $cvcl_57) )) (or $cvcl_58 $cvcl_59 )) (or $cvcl_147 (not $cvcl_59) )) (or $cvcl_60 $cvcl_61 )) (or $cvcl_152 (not $cvcl_61) )) (or $cvcl_62 $cvcl_63 )) (or $cvcl_151 (not $cvcl_63) )) (or $cvcl_64 $cvcl_65 )) (or $cvcl_156 (not $cvcl_65) )) (or $cvcl_66 $cvcl_67 )) (or $cvcl_155 (not $cvcl_67) )) (or $cvcl_68 $cvcl_69 )) (or $cvcl_160 (not $cvcl_69) )) (or $cvcl_70 $cvcl_71 )) (or $cvcl_159 (not $cvcl_71) )) (or $cvcl_1 $cvcl_74 )) (or $cvcl_5 (<= (- AT1_PROC1_X AT1_Z) 10) )) (or $cvcl_9 $cvcl_81 )) (or $cvcl_13 (<= (- AT1_PROC2_X AT1_Z) 10) )) (or $cvcl_17 $cvcl_87 )) (or $cvcl_21 (<= (- AT1_PROC3_X AT1_Z) 10) )) (or $cvcl_25 $cvcl_93 )) (or $cvcl_29 (<= (- AT1_PROC4_X AT1_Z) 10) )) (or $cvcl_33 $cvcl_99 )) (or $cvcl_37 (<= (- AT1_PROC5_X AT1_Z) 10) )) (or $cvcl_41 $cvcl_105 )) (or $cvcl_45 (<= (- AT1_PROC6_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 $cvcl_72 AT0_PROC1_A )) (or $cvcl_72 AT0_PROC1_TAU )) (or $cvcl_72 AT1_PROC1_B )) (or $cvcl_72 $cvcl_50 )) (or $cvcl_73 AT0_PROC1_B )) (or $cvcl_73 AT0_PROC1_TAU )) (or $cvcl_73 AT1_PROC1_C )) (or $cvcl_73 $cvcl_74 )) (or $cvcl_73 $cvcl_50 )) (or $cvcl_75 AT0_PROC1_C )) (or $cvcl_75 AT0_PROC1_TAU )) (or $cvcl_75 AT1_PROC1_B )) (or $cvcl_75 $cvcl_50 )) (or $cvcl_76 AT0_PROC1_C )) (or $cvcl_76 AT0_PROC1_TAU )) (or $cvcl_76 AT1_PROC1_CS )) (or $cvcl_76 (> (- AT0_PROC1_X AT0_Z) 10) )) (or $cvcl_76 $cvcl_110 )) (or $cvcl_77 AT0_PROC1_CS )) (or $cvcl_77 AT0_PROC1_TAU )) (or $cvcl_77 AT1_PROC1_A )) (or $cvcl_77 $cvcl_50 )) (or $cvcl_72 $cvcl_78 )) (or $cvcl_73 $cvcl_78 )) (or $cvcl_75 $cvcl_78 )) (or $cvcl_76 $cvcl_78 )) (or $cvcl_77 $cvcl_78 )) (or $cvcl_79 AT0_PROC2_A )) (or $cvcl_79 AT0_PROC2_TAU )) (or $cvcl_79 AT1_PROC2_B )) (or $cvcl_79 $cvcl_54 )) (or $cvcl_80 AT0_PROC2_B )) (or $cvcl_80 AT0_PROC2_TAU )) (or $cvcl_80 AT1_PROC2_C )) (or $cvcl_80 $cvcl_81 )) (or $cvcl_80 $cvcl_54 )) (or $cvcl_82 AT0_PROC2_C )) (or $cvcl_82 AT0_PROC2_TAU )) (or $cvcl_82 AT1_PROC2_B )) (or $cvcl_82 $cvcl_54 )) (or $cvcl_83 AT0_PROC2_C )) (or $cvcl_83 AT0_PROC2_TAU )) (or $cvcl_83 AT1_PROC2_CS )) (or $cvcl_83 (> (- AT0_PROC2_X AT0_Z) 10) )) (or $cvcl_83 $cvcl_112 )) (or $cvcl_84 AT0_PROC2_CS )) (or $cvcl_84 AT0_PROC2_TAU )) (or $cvcl_84 AT1_PROC2_A )) (or $cvcl_84 $cvcl_54 )) (or $cvcl_79 $cvcl_78 )) (or $cvcl_80 $cvcl_78 )) (or $cvcl_82 $cvcl_78 )) (or $cvcl_83 $cvcl_78 )) (or $cvcl_84 $cvcl_78 )) (or $cvcl_85 AT0_PROC3_A )) (or $cvcl_85 AT0_PROC3_TAU )) (or $cvcl_85 AT1_PROC3_B )) (or $cvcl_85 $cvcl_58 )) (or $cvcl_86 AT0_PROC3_B )) (or $cvcl_86 AT0_PROC3_TAU )) (or $cvcl_86 AT1_PROC3_C )) (or $cvcl_86 $cvcl_87 )) (or $cvcl_86 $cvcl_58 )) (or $cvcl_88 AT0_PROC3_C )) (or $cvcl_88 AT0_PROC3_TAU )) (or $cvcl_88 AT1_PROC3_B )) (or $cvcl_88 $cvcl_58 )) (or $cvcl_89 AT0_PROC3_C )) (or $cvcl_89 AT0_PROC3_TAU )) (or $cvcl_89 AT1_PROC3_CS )) (or $cvcl_89 (> (- AT0_PROC3_X AT0_Z) 10) )) (or $cvcl_89 $cvcl_114 )) (or $cvcl_90 AT0_PROC3_CS )) (or $cvcl_90 AT0_PROC3_TAU )) (or $cvcl_90 AT1_PROC3_A )) (or $cvcl_90 $cvcl_58 )) (or $cvcl_85 $cvcl_78 )) (or $cvcl_86 $cvcl_78 )) (or $cvcl_88 $cvcl_78 )) (or $cvcl_89 $cvcl_78 )) (or $cvcl_90 $cvcl_78 )) (or $cvcl_91 AT0_PROC4_A )) (or $cvcl_91 AT0_PROC4_TAU )) (or $cvcl_91 AT1_PROC4_B )) (or $cvcl_91 $cvcl_62 )) (or $cvcl_92 AT0_PROC4_B )) (or $cvcl_92 AT0_PROC4_TAU )) (or $cvcl_92 AT1_PROC4_C )) (or $cvcl_92 $cvcl_93 )) (or $cvcl_92 $cvcl_62 )) (or $cvcl_94 AT0_PROC4_C )) (or $cvcl_94 AT0_PROC4_TAU )) (or $cvcl_94 AT1_PROC4_B )) (or $cvcl_94 $cvcl_62 )) (or $cvcl_95 AT0_PROC4_C )) (or $cvcl_95 AT0_PROC4_TAU )) (or $cvcl_95 AT1_PROC4_CS )) (or $cvcl_95 (> (- AT0_PROC4_X AT0_Z) 10) )) (or $cvcl_95 $cvcl_116 )) (or $cvcl_96 AT0_PROC4_CS )) (or $cvcl_96 AT0_PROC4_TAU )) (or $cvcl_96 AT1_PROC4_A )) (or $cvcl_96 $cvcl_62 )) (or $cvcl_91 $cvcl_78 )) (or $cvcl_92 $cvcl_78 )) (or $cvcl_94 $cvcl_78 )) (or $cvcl_95 $cvcl_78 )) (or $cvcl_96 $cvcl_78 )) (or $cvcl_97 AT0_PROC5_A )) (or $cvcl_97 AT0_PROC5_TAU )) (or $cvcl_97 AT1_PROC5_B )) (or $cvcl_97 $cvcl_66 )) (or $cvcl_98 AT0_PROC5_B )) (or $cvcl_98 AT0_PROC5_TAU )) (or $cvcl_98 AT1_PROC5_C )) (or $cvcl_98 $cvcl_99 )) (or $cvcl_98 $cvcl_66 )) (or $cvcl_100 AT0_PROC5_C )) (or $cvcl_100 AT0_PROC5_TAU )) (or $cvcl_100 AT1_PROC5_B )) (or $cvcl_100 $cvcl_66 )) (or $cvcl_101 AT0_PROC5_C )) (or $cvcl_101 AT0_PROC5_TAU )) (or $cvcl_101 AT1_PROC5_CS )) (or $cvcl_101 (> (- AT0_PROC5_X AT0_Z) 10) )) (or $cvcl_101 $cvcl_118 )) (or $cvcl_102 AT0_PROC5_CS )) (or $cvcl_102 AT0_PROC5_TAU )) (or $cvcl_102 AT1_PROC5_A )) (or $cvcl_102 $cvcl_66 )) (or $cvcl_97 $cvcl_78 )) (or $cvcl_98 $cvcl_78 )) (or $cvcl_100 $cvcl_78 )) (or $cvcl_101 $cvcl_78 )) (or $cvcl_102 $cvcl_78 )) (or $cvcl_103 AT0_PROC6_A )) (or $cvcl_103 AT0_PROC6_TAU )) (or $cvcl_103 AT1_PROC6_B )) (or $cvcl_103 $cvcl_70 )) (or $cvcl_104 AT0_PROC6_B )) (or $cvcl_104 AT0_PROC6_TAU )) (or $cvcl_104 AT1_PROC6_C )) (or $cvcl_104 $cvcl_105 )) (or $cvcl_104 $cvcl_70 )) (or $cvcl_106 AT0_PROC6_C )) (or $cvcl_106 AT0_PROC6_TAU )) (or $cvcl_106 AT1_PROC6_B )) (or $cvcl_106 $cvcl_70 )) (or $cvcl_107 AT0_PROC6_C )) (or $cvcl_107 AT0_PROC6_TAU )) (or $cvcl_107 AT1_PROC6_CS )) (or $cvcl_107 (> (- AT0_PROC6_X AT0_Z) 10) )) (or $cvcl_107 $cvcl_120 )) (or $cvcl_108 AT0_PROC6_CS )) (or $cvcl_108 AT0_PROC6_TAU )) (or $cvcl_108 AT1_PROC6_A )) (or $cvcl_108 $cvcl_70 )) (or $cvcl_103 $cvcl_78 )) (or $cvcl_104 $cvcl_78 )) (or $cvcl_106 $cvcl_78 )) (or $cvcl_107 $cvcl_78 )) (or $cvcl_108 $cvcl_78 )) (or (or $cvcl_109 $cvcl_0 ) AT1_PROC1_A )) (or (or $cvcl_109 AT0_PROC1_A ) $cvcl_4 )) (or (or $cvcl_109 $cvcl_1 ) AT1_PROC1_B )) (or (or $cvcl_109 AT0_PROC1_B ) $cvcl_5 )) (or (or $cvcl_109 $cvcl_2 ) AT1_PROC1_C )) (or (or $cvcl_109 AT0_PROC1_C ) $cvcl_6 )) (or (or $cvcl_109 $cvcl_3 ) AT1_PROC1_CS )) (or (or $cvcl_109 AT0_PROC1_CS ) $cvcl_7 )) (or $cvcl_109 $cvcl_122 )) (or $cvcl_109 $cvcl_110 )) (or $cvcl_109 $cvcl_78 )) (or (or $cvcl_111 $cvcl_8 ) AT1_PROC2_A )) (or (or $cvcl_111 AT0_PROC2_A ) $cvcl_12 )) (or (or $cvcl_111 $cvcl_9 ) AT1_PROC2_B )) (or (or $cvcl_111 AT0_PROC2_B ) $cvcl_13 )) (or (or $cvcl_111 $cvcl_10 ) AT1_PROC2_C )) (or (or $cvcl_111 AT0_PROC2_C ) $cvcl_14 )) (or (or $cvcl_111 $cvcl_11 ) AT1_PROC2_CS )) (or (or $cvcl_111 AT0_PROC2_CS ) $cvcl_15 )) (or $cvcl_111 $cvcl_123 )) (or $cvcl_111 $cvcl_112 )) (or $cvcl_111 $cvcl_78 )) (or (or $cvcl_113 $cvcl_16 ) AT1_PROC3_A )) (or (or $cvcl_113 AT0_PROC3_A ) $cvcl_20 )) (or (or $cvcl_113 $cvcl_17 ) AT1_PROC3_B )) (or (or $cvcl_113 AT0_PROC3_B ) $cvcl_21 )) (or (or $cvcl_113 $cvcl_18 ) AT1_PROC3_C )) (or (or $cvcl_113 AT0_PROC3_C ) $cvcl_22 )) (or (or $cvcl_113 $cvcl_19 ) AT1_PROC3_CS )) (or (or $cvcl_113 AT0_PROC3_CS ) $cvcl_23 )) (or $cvcl_113 $cvcl_125 )) (or $cvcl_113 $cvcl_114 )) (or $cvcl_113 $cvcl_78 )) (or (or $cvcl_115 $cvcl_24 ) AT1_PROC4_A )) (or (or $cvcl_115 AT0_PROC4_A ) $cvcl_28 )) (or (or $cvcl_115 $cvcl_25 ) AT1_PROC4_B )) (or (or $cvcl_115 AT0_PROC4_B ) $cvcl_29 )) (or (or $cvcl_115 $cvcl_26 ) AT1_PROC4_C )) (or (or $cvcl_115 AT0_PROC4_C ) $cvcl_30 )) (or (or $cvcl_115 $cvcl_27 ) AT1_PROC4_CS )) (or (or $cvcl_115 AT0_PROC4_CS ) $cvcl_31 )) (or $cvcl_115 $cvcl_126 )) (or $cvcl_115 $cvcl_116 )) (or $cvcl_115 $cvcl_78 )) (or (or $cvcl_117 $cvcl_32 ) AT1_PROC5_A )) (or (or $cvcl_117 AT0_PROC5_A ) $cvcl_36 )) (or (or $cvcl_117 $cvcl_33 ) AT1_PROC5_B )) (or (or $cvcl_117 AT0_PROC5_B ) $cvcl_37 )) (or (or $cvcl_117 $cvcl_34 ) AT1_PROC5_C )) (or (or $cvcl_117 AT0_PROC5_C ) $cvcl_38 )) (or (or $cvcl_117 $cvcl_35 ) AT1_PROC5_CS )) (or (or $cvcl_117 AT0_PROC5_CS ) $cvcl_39 )) (or $cvcl_117 $cvcl_127 )) (or $cvcl_117 $cvcl_118 )) (or $cvcl_117 $cvcl_78 )) (or (or $cvcl_119 $cvcl_40 ) AT1_PROC6_A )) (or (or $cvcl_119 AT0_PROC6_A ) $cvcl_44 )) (or (or $cvcl_119 $cvcl_41 ) AT1_PROC6_B )) (or (or $cvcl_119 AT0_PROC6_B ) $cvcl_45 )) (or (or $cvcl_119 $cvcl_42 ) AT1_PROC6_C )) (or (or $cvcl_119 AT0_PROC6_C ) $cvcl_46 )) (or (or $cvcl_119 $cvcl_43 ) AT1_PROC6_CS )) (or (or $cvcl_119 AT0_PROC6_CS ) $cvcl_47 )) (or $cvcl_119 $cvcl_128 )) (or $cvcl_119 $cvcl_120 )) (or $cvcl_119 $cvcl_78 )) (or (or $cvcl_121 $cvcl_0 ) AT1_PROC1_A )) (or (or $cvcl_121 AT0_PROC1_A ) $cvcl_4 )) (or (or $cvcl_121 $cvcl_1 ) AT1_PROC1_B )) (or (or $cvcl_121 AT0_PROC1_B ) $cvcl_5 )) (or (or $cvcl_121 $cvcl_2 ) AT1_PROC1_C )) (or (or $cvcl_121 AT0_PROC1_C ) $cvcl_6 )) (or (or $cvcl_121 $cvcl_3 ) AT1_PROC1_CS )) (or (or $cvcl_121 AT0_PROC1_CS ) $cvcl_7 )) (or $cvcl_121 $cvcl_110 )) (or $cvcl_121 $cvcl_122 )) $cvcl_124) (or (or $cvcl_121 $cvcl_8 ) AT1_PROC2_A )) (or (or $cvcl_121 AT0_PROC2_A ) $cvcl_12 )) (or (or $cvcl_121 $cvcl_9 ) AT1_PROC2_B )) (or (or $cvcl_121 AT0_PROC2_B ) $cvcl_13 )) (or (or $cvcl_121 $cvcl_10 ) AT1_PROC2_C )) (or (or $cvcl_121 AT0_PROC2_C ) $cvcl_14 )) (or (or $cvcl_121 $cvcl_11 ) AT1_PROC2_CS )) (or (or $cvcl_121 AT0_PROC2_CS ) $cvcl_15 )) (or $cvcl_121 $cvcl_112 )) (or $cvcl_121 $cvcl_123 )) $cvcl_124) (or (or $cvcl_121 $cvcl_16 ) AT1_PROC3_A )) (or (or $cvcl_121 AT0_PROC3_A ) $cvcl_20 )) (or (or $cvcl_121 $cvcl_17 ) AT1_PROC3_B )) (or (or $cvcl_121 AT0_PROC3_B ) $cvcl_21 )) (or (or $cvcl_121 $cvcl_18 ) AT1_PROC3_C )) (or (or $cvcl_121 AT0_PROC3_C ) $cvcl_22 )) (or (or $cvcl_121 $cvcl_19 ) AT1_PROC3_CS )) (or (or $cvcl_121 AT0_PROC3_CS ) $cvcl_23 )) (or $cvcl_121 $cvcl_114 )) (or $cvcl_121 $cvcl_125 )) $cvcl_124) (or (or $cvcl_121 $cvcl_24 ) AT1_PROC4_A )) (or (or $cvcl_121 AT0_PROC4_A ) $cvcl_28 )) (or (or $cvcl_121 $cvcl_25 ) AT1_PROC4_B )) (or (or $cvcl_121 AT0_PROC4_B ) $cvcl_29 )) (or (or $cvcl_121 $cvcl_26 ) AT1_PROC4_C )) (or (or $cvcl_121 AT0_PROC4_C ) $cvcl_30 )) (or (or $cvcl_121 $cvcl_27 ) AT1_PROC4_CS )) (or (or $cvcl_121 AT0_PROC4_CS ) $cvcl_31 )) (or $cvcl_121 $cvcl_116 )) (or $cvcl_121 $cvcl_126 )) $cvcl_124) (or (or $cvcl_121 $cvcl_32 ) AT1_PROC5_A )) (or (or $cvcl_121 AT0_PROC5_A ) $cvcl_36 )) (or (or $cvcl_121 $cvcl_33 ) AT1_PROC5_B )) (or (or $cvcl_121 AT0_PROC5_B ) $cvcl_37 )) (or (or $cvcl_121 $cvcl_34 ) AT1_PROC5_C )) (or (or $cvcl_121 AT0_PROC5_C ) $cvcl_38 )) (or (or $cvcl_121 $cvcl_35 ) AT1_PROC5_CS )) (or (or $cvcl_121 AT0_PROC5_CS ) $cvcl_39 )) (or $cvcl_121 $cvcl_118 )) (or $cvcl_121 $cvcl_127 )) $cvcl_124) (or (or $cvcl_121 $cvcl_40 ) AT1_PROC6_A )) (or (or $cvcl_121 AT0_PROC6_A ) $cvcl_44 )) (or (or $cvcl_121 $cvcl_41 ) AT1_PROC6_B )) (or (or $cvcl_121 AT0_PROC6_B ) $cvcl_45 )) (or (or $cvcl_121 $cvcl_42 ) AT1_PROC6_C )) (or (or $cvcl_121 AT0_PROC6_C ) $cvcl_46 )) (or (or $cvcl_121 $cvcl_43 ) AT1_PROC6_CS )) (or (or $cvcl_121 AT0_PROC6_CS ) $cvcl_47 )) (or $cvcl_121 $cvcl_120 )) (or $cvcl_121 $cvcl_128 )) $cvcl_124) (or $cvcl_110 $cvcl_129 )) (or $cvcl_136 (not $cvcl_129) )) (or $cvcl_112 $cvcl_130 )) (or $cvcl_142 (not $cvcl_130) )) (or $cvcl_114 $cvcl_131 )) (or $cvcl_146 (not $cvcl_131) )) (or $cvcl_116 $cvcl_132 )) (or $cvcl_150 (not $cvcl_132) )) (or $cvcl_118 $cvcl_133 )) (or $cvcl_154 (not $cvcl_133) )) (or $cvcl_120 $cvcl_134 )) (or $cvcl_158 (not $cvcl_134) )) (or $cvcl_78 $cvcl_135 )) (or $cvcl_137 $cvcl_141 )) (or (or (or $cvcl_48 $cvcl_136 ) $cvcl_137 ) $cvcl_138 )) (or (or (or $cvcl_139 $cvcl_110 ) $cvcl_137 ) $cvcl_138 )) (or (or $cvcl_140 $cvcl_78 ) $cvcl_138 )) (or (or $cvcl_140 $cvcl_137 ) $cvcl_50 )) (or (or (or (not (< AT0_Z AT0_PROC1_X)) $cvcl_136 ) $cvcl_141 ) (< AT1_Z AT1_PROC1_X) )) (or (or (or $cvcl_52 $cvcl_142 ) $cvcl_137 ) $cvcl_143 )) (or (or (or $cvcl_144 $cvcl_112 ) $cvcl_137 ) $cvcl_143 )) (or (or $cvcl_145 $cvcl_78 ) $cvcl_143 )) (or (or $cvcl_145 $cvcl_137 ) $cvcl_54 )) (or (or (or (not (< AT0_Z AT0_PROC2_X)) $cvcl_142 ) $cvcl_141 ) (< AT1_Z AT1_PROC2_X) )) (or (or (or $cvcl_56 $cvcl_146 ) $cvcl_137 ) $cvcl_147 )) (or (or (or $cvcl_148 $cvcl_114 ) $cvcl_137 ) $cvcl_147 )) (or (or $cvcl_149 $cvcl_78 ) $cvcl_147 )) (or (or $cvcl_149 $cvcl_137 ) $cvcl_58 )) (or (or (or (not (< AT0_Z AT0_PROC3_X)) $cvcl_146 ) $cvcl_141 ) (< AT1_Z AT1_PROC3_X) )) (or (or (or $cvcl_60 $cvcl_150 ) $cvcl_137 ) $cvcl_151 )) (or (or (or $cvcl_152 $cvcl_116 ) $cvcl_137 ) $cvcl_151 )) (or (or $cvcl_153 $cvcl_78 ) $cvcl_151 )) (or (or $cvcl_153 $cvcl_137 ) $cvcl_62 )) (or (or (or (not (< AT0_Z AT0_PROC4_X)) $cvcl_150 ) $cvcl_141 ) (< AT1_Z AT1_PROC4_X) )) (or (or (or $cvcl_64 $cvcl_154 ) $cvcl_137 ) $cvcl_155 )) (or (or (or $cvcl_156 $cvcl_118 ) $cvcl_137 ) $cvcl_155 )) (or (or $cvcl_157 $cvcl_78 ) $cvcl_155 )) (or (or $cvcl_157 $cvcl_137 ) $cvcl_66 )) (or (or (or (not (< AT0_Z AT0_PROC5_X)) $cvcl_154 ) $cvcl_141 ) (< AT1_Z AT1_PROC5_X) )) (or (or (or $cvcl_68 $cvcl_158 ) $cvcl_137 ) $cvcl_159 )) (or (or (or $cvcl_160 $cvcl_120 ) $cvcl_137 ) $cvcl_159 )) (or (or $cvcl_161 $cvcl_78 ) $cvcl_159 )) (or (or $cvcl_161 $cvcl_137 ) $cvcl_70 )) (or (or (or (not (< AT0_Z AT0_PROC6_X)) $cvcl_158 ) $cvcl_141 ) (< AT1_Z AT1_PROC6_X) )) AT0_PROC1_A) AT0_PROC2_A) AT0_PROC3_A) AT0_PROC4_A) AT0_PROC5_A) AT0_PROC6_A) $cvcl_48) $cvcl_52) $cvcl_56) $cvcl_60) $cvcl_64) $cvcl_68) AT0_ID0) (or (or (or (or (or $cvcl_109 $cvcl_111 ) $cvcl_113 ) $cvcl_115 ) $cvcl_117 ) $cvcl_119 )) (or $cvcl_162 $cvcl_163 )) (or $cvcl_162 $cvcl_164 )) (or $cvcl_162 $cvcl_165 )) (or $cvcl_162 $cvcl_166 )) (or $cvcl_162 $cvcl_167 )) (or $cvcl_162 $cvcl_168 )) (or $cvcl_163 $cvcl_164 )) (or $cvcl_163 $cvcl_165 )) (or $cvcl_163 $cvcl_166 )) (or $cvcl_163 $cvcl_167 )) (or $cvcl_163 $cvcl_168 )) (or $cvcl_164 $cvcl_165 )) (or $cvcl_164 $cvcl_166 )) (or $cvcl_164 $cvcl_167 )) (or $cvcl_164 $cvcl_168 )) (or $cvcl_165 $cvcl_166 )) (or $cvcl_165 $cvcl_167 )) (or $cvcl_165 $cvcl_168 )) (or $cvcl_166 $cvcl_167 )) (or $cvcl_166 $cvcl_168 )) (or $cvcl_167 $cvcl_168 )) (or $cvcl_169 $cvcl_170 )) (or $cvcl_169 $cvcl_171 )) (or $cvcl_169 $cvcl_172 )) (or $cvcl_169 $cvcl_173 )) (or $cvcl_169 $cvcl_174 )) (or $cvcl_169 $cvcl_175 )) (or $cvcl_170 $cvcl_171 )) (or $cvcl_170 $cvcl_172 )) (or $cvcl_170 $cvcl_173 )) (or $cvcl_170 $cvcl_174 )) (or $cvcl_170 $cvcl_175 )) (or $cvcl_171 $cvcl_172 )) (or $cvcl_171 $cvcl_173 )) (or $cvcl_171 $cvcl_174 )) (or $cvcl_171 $cvcl_175 )) (or $cvcl_172 $cvcl_173 )) (or $cvcl_172 $cvcl_174 )) (or $cvcl_172 $cvcl_175 )) (or $cvcl_173 $cvcl_174 )) (or $cvcl_173 $cvcl_175 )) (or $cvcl_174 $cvcl_175 )) (or $cvcl_72 AT0_ID0 )) (or $cvcl_72 AT1_ID0 )) (or $cvcl_73 AT1_ID1 )) (or $cvcl_75 AT0_ID0 )) (or $cvcl_75 AT1_ID0 )) (or $cvcl_76 AT0_ID1 )) (or $cvcl_76 AT1_ID1 )) (or $cvcl_77 AT1_ID0 )) (or (or $cvcl_121 $cvcl_163 ) AT1_ID1 )) (or $cvcl_79 AT0_ID0 )) (or $cvcl_79 AT1_ID0 )) (or $cvcl_80 AT1_ID2 )) (or $cvcl_82 AT0_ID0 )) (or $cvcl_82 AT1_ID0 )) (or $cvcl_83 AT0_ID2 )) (or $cvcl_83 AT1_ID2 )) (or $cvcl_84 AT1_ID0 )) (or (or $cvcl_121 $cvcl_164 ) AT1_ID2 )) (or $cvcl_85 AT0_ID0 )) (or $cvcl_85 AT1_ID0 )) (or $cvcl_86 AT1_ID3 )) (or $cvcl_88 AT0_ID0 )) (or $cvcl_88 AT1_ID0 )) (or $cvcl_89 AT0_ID3 )) (or $cvcl_89 AT1_ID3 )) (or $cvcl_90 AT1_ID0 )) (or (or $cvcl_121 $cvcl_165 ) AT1_ID3 )) (or $cvcl_91 AT0_ID0 )) (or $cvcl_91 AT1_ID0 )) (or $cvcl_92 AT1_ID4 )) (or $cvcl_94 AT0_ID0 )) (or $cvcl_94 AT1_ID0 )) (or $cvcl_95 AT0_ID4 )) (or $cvcl_95 AT1_ID4 )) (or $cvcl_96 AT1_ID0 )) (or (or $cvcl_121 $cvcl_166 ) AT1_ID4 )) (or $cvcl_97 AT0_ID0 )) (or $cvcl_97 AT1_ID0 )) (or $cvcl_98 AT1_ID5 )) (or $cvcl_100 AT0_ID0 )) (or $cvcl_100 AT1_ID0 )) (or $cvcl_101 AT0_ID5 )) (or $cvcl_101 AT1_ID5 )) (or $cvcl_102 AT1_ID0 )) (or (or $cvcl_121 $cvcl_167 ) AT1_ID5 )) (or $cvcl_103 AT0_ID0 )) (or $cvcl_103 AT1_ID0 )) (or $cvcl_104 AT1_ID6 )) (or $cvcl_106 AT0_ID0 )) (or $cvcl_106 AT1_ID0 )) (or $cvcl_107 AT0_ID6 )) (or $cvcl_107 AT1_ID6 )) (or $cvcl_108 AT1_ID0 )) (or (or $cvcl_121 $cvcl_168 ) AT1_ID6 )) (or (or $cvcl_121 $cvcl_162 ) 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_170 AT1_ID1 )) (or AT1_ID1 $cvcl_170 )) (= (- 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_171 AT1_ID2 )) (or AT1_ID2 $cvcl_171 )) (= (- 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_172 AT1_ID3 )) (or AT1_ID3 $cvcl_172 )) (= (- 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_173 AT1_ID4 )) (or AT1_ID4 $cvcl_173 )) (= (- 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_174 AT1_ID5 )) (or AT1_ID5 $cvcl_174 )) (= (- 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_175 AT1_ID6 )) (or AT1_ID6 $cvcl_175 )) (= (- AT1_PROC6_X AT1_Z) (- AT1_PROC6_X AT1_Z))) AT1_PROC1_B) $cvcl_7))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )