(benchmark FISCHER8_3_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
  :extrafuns ((AT3_PROC5_X Int))
  :extrapreds ((AT0_PROC3_CS))
  :extrapreds ((AT2_PROC7_WAIT))
  :extrafuns ((AT1_PROC5_X Int))
  :extrapreds ((AT0_PROC7_SW_A_B_TAU))
  :extrapreds ((AT2_PROC6_SW_A_B_TAU))
  :extrapreds ((AT0_PROC6_SW_B_C_TAU))
  :extrapreds ((AT1_PROC5_CS))
  :extrapreds ((AT1_PROC2_TAU))
  :extrapreds ((AT1_PROC2_SW_C_CS_TAU))
  :extrafuns ((AT2_PROC1_X Int))
  :extrapreds ((AT2_PROC6_C))
  :extrapreds ((AT2_PROC8_SW_CS_A_TAU))
  :extrapreds ((AT2_PROC6_B))
  :extrapreds ((AT1_PROC8_SW_C_B_TAU))
  :extrafuns ((AT0_PROC1_X Int))
  :extrapreds ((AT2_PROC6_A))
  :extrapreds ((AT0_PROC6_C))
  :extrapreds ((AT1_PROC1_SW_B_C_TAU))
  :extrapreds ((AT0_PROC6_B))
  :extrapreds ((AT3_PROC2_C))
  :extrapreds ((AT1_PROC6_TAU))
  :extrapreds ((AT2_PROC7_SW_C_B_TAU))
  :extrapreds ((AT0_PROC7_SW_CS_A_TAU))
  :extrapreds ((AT1_PROC6_SW_C_CS_TAU))
  :extrapreds ((AT2_PROC7_CS))
  :extrapreds ((AT0_PROC6_A))
  :extrapreds ((AT3_PROC2_B))
  :extrapreds ((AT0_ID0))
  :extrapreds ((AT2_PROC4_SW_CS_A_TAU))
  :extrapreds ((AT3_PROC2_A))
  :extrapreds ((AT1_PROC2_C))
  :extrapreds ((AT0_ID1))
  :extrapreds ((AT1_PROC2_B))
  :extrapreds ((AT0_ID2))
  :extrapreds ((AT1_PROC7_SW_A_B_TAU))
  :extrapreds ((AT0_PROC6_CS))
  :extrapreds ((AT1_PROC2_A))
  :extrapreds ((AT0_ID3))
  :extrapreds ((AT1_PROC6_SW_A_B_TAU))
  :extrapreds ((AT0_PROC3_SW_CS_A_TAU))
  :extrafuns ((AT3_PROC8_X Int))
  :extrapreds ((AT0_ID4))
  :extrapreds ((AT0_ID5))
  :extrapreds ((AT1_PROC2_SW_A_B_TAU))
  :extrafuns ((AT1_PROC8_X Int))
  :extrapreds ((AT1_PROC2_CS))
  :extrapreds ((AT0_ID6))
  :extrapreds ((AT2_PROC8_SW_C_B_TAU))
  :extrapreds ((AT0_ID7))
  :extrapreds ((AT2_PROC1_SW_B_C_TAU))
  :extrapreds ((AT1_PROC1_WAIT))
  :extrapreds ((AT0_ID8))
  :extrafuns ((AT2_PROC4_X Int))
  :extrafuns ((AT0_PROC4_X Int))
  :extrapreds ((AT2_PROC4_CS))
  :extrapreds ((AT0_PROC3_TAU))
  :extrapreds ((AT0_PROC7_SW_B_C_TAU))
  :extrapreds ((AT3_PROC5_C))
  :extrapreds ((AT2_PROC2_TAU))
  :extrapreds ((AT0_PROC6_SW_A_B_TAU))
  :extrapreds ((AT1_PROC4_WAIT))
  :extrapreds ((AT3_PROC5_B))
  :extrapreds ((AT3_PROC5_A))
  :extrapreds ((AT1_PROC5_C))
  :extrapreds ((AT2_PROC2_SW_A_B_TAU))
  :extrapreds ((AT0_PROC2_SW_C_B_TAU))
  :extrapreds ((AT1_PROC5_B))
  :extrapreds ((AT0_PROC7_TAU))
  :extrafuns ((AT2_Z Int))
  :extrapreds ((AT3_PROC6_CS))
  :extrapreds ((AT1_PROC5_A))
  :extrapreds ((AT2_PROC6_TAU))
  :extrapreds ((AT0_PROC4_SW_C_B_TAU))
  :extrapreds ((AT2_PROC1_C))
  :extrapreds ((AT1_PROC7_WAIT))
  :extrapreds ((AT2_PROC1_B))
  :extrapreds ((AT0_PROC8_SW_A_B_TAU))
  :extrapreds ((AT2_PROC1_A))
  :extrapreds ((AT0_PROC1_C))
  :extrapreds ((AT0_PROC1_B))
  :extrapreds ((AT1_PROC7_SW_B_C_TAU))
  :extrapreds ((AT0_PROC1_A))
  :extrafuns ((AT2_PROC7_X Int))
  :extrapreds ((AT2_PROC1_CS))
  :extrapreds ((AT1_PROC2_SW_B_C_TAU))
  :extrafuns ((AT0_PROC7_X Int))
  :extrapreds ((AT2_PROC6_SW_C_B_TAU))
  :extrafuns ((AT3_PROC3_X Int))
  :extrapreds ((AT3_PROC8_C))
  :extrapreds ((AT0_PROC6_WAIT))
  :extrapreds ((AT1_PROC4_SW_C_B_TAU))
  :extrapreds ((AT3_PROC8_B))
  :extrafuns ((AT1_PROC3_X Int))
  :extrapreds ((AT3_PROC8_A))
  :extrapreds ((AT1_PROC8_C))
  :extrapreds ((AT3_PROC3_CS))
  :extrapreds ((AT1_PROC8_SW_A_B_TAU))
  :extrapreds ((AT1_PROC8_B))
  :extrapreds ((AT1_PROC3_TAU))
  :extrapreds ((AT2_PROC3_WAIT))
  :extrapreds ((AT1_PROC8_A))
  :extrapreds ((AT2_PROC4_C))
  :extrapreds ((AT0_PROC3_WAIT))
  :extrapreds ((AT2_PROC4_B))
  :extrapreds ((AT0_PROC2_CS))
  :extrapreds ((AT1_PROC8_SW_CS_A_TAU))
  :extrapreds ((AT2_PROC4_A))
  :extrapreds ((AT0_PROC4_C))
  :extrapreds ((AT1_PROC7_TAU))
  :extrapreds ((AT2_PROC2_SW_B_C_TAU))
  :extrapreds ((AT0_PROC4_B))
  :extrapreds ((AT1_ID0))
  :extrapreds ((AT2_PROC6_WAIT))
  :extrapreds ((AT1_PROC6_SW_C_B_TAU))
  :extrapreds ((AT1_PROC6_CS))
  :extrapreds ((AT0_PROC4_A))
  :extrapreds ((AT1_ID1))
  :extrapreds ((AT2_PROC4_SW_C_B_TAU))
  :extrapreds ((AT1_ID2))
  :extrapreds ((AT1_ID3))
  :extrapreds ((AT2_PROC8_SW_A_B_TAU))
  :extrapreds ((AT0_PROC8_SW_B_C_TAU))
  :extrapreds ((AT1_ID4))
  :extrafuns ((AT3_PROC6_X Int))
  :extrapreds ((AT1_ID5))
  :extrapreds ((AT2_PROC8_CS))
  :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 ((AT0_PROC6_SW_C_B_TAU))
  :extrapreds ((AT2_PROC2_SW_CS_A_TAU))
  :extrafuns ((AT2_PROC2_X Int))
  :extrapreds ((AT2_PROC7_C))
  :extrapreds ((AT0_PROC5_SW_CS_A_TAU))
  :extrapreds ((AT2_PROC7_B))
  :extrapreds ((AT0_PROC4_TAU))
  :extrafuns ((AT0_PROC2_X Int))
  :extrapreds ((AT2_PROC7_A))
  :extrapreds ((AT0_PROC7_C))
  :extrapreds ((AT1_PROC3_CS))
  :extrapreds ((AT2_PROC3_TAU))
  :extrapreds ((AT1_PROC8_SW_B_C_TAU))
  :extrapreds ((AT0_PROC7_B))
  :extrapreds ((AT3_PROC3_C))
  :extrapreds ((AT2_PROC6_SW_CS_A_TAU))
  :extrapreds ((AT0_PROC4_SW_A_B_TAU))
  :extrapreds ((AT0_PROC7_A))
  :extrapreds ((AT3_PROC3_B))
  :extrapreds ((AT1_PROC4_SW_C_CS_TAU))
  :extrapreds ((AT3_PROC3_A))
  :extrapreds ((AT1_PROC3_C))
  :extrapreds ((AT0_PROC8_TAU))
  :extrapreds ((AT1_PROC3_B))
  :extrapreds ((AT2_PROC7_TAU))
  :extrapreds ((AT2_PROC5_CS))
  :extrapreds ((AT1_PROC3_A))
  :extrapreds ((AT1_PROC5_SW_C_B_TAU))
  :extrapreds ((AT2_PROC3_SW_B_C_TAU))
  :extrapreds ((AT0_PROC8_CS))
  :extrapreds ((AT1_PROC3_WAIT))
  :extrapreds ((AT2_PROC8_SW_B_C_TAU))
  :extrapreds ((AT3_PROC7_CS))
  :extrapreds ((AT1_PROC4_SW_A_B_TAU))
  :extrafuns ((AT2_PROC5_X Int))
  :extrafuns ((AT0_PROC5_X Int))
  :extrapreds ((AT1_PROC6_WAIT))
  :extrapreds ((AT1_PROC3_SW_CS_A_TAU))
  :extrafuns ((AT3_PROC1_X Int))
  :extrapreds ((AT3_PROC6_C))
  :extrapreds ((AT2_PROC7_SW_C_CS_TAU))
  :extrapreds ((AT2_PROC5_SW_C_B_TAU))
  :extrapreds ((AT3_PROC6_B))
  :extrapreds ((AT1_PROC3_SW_B_C_TAU))
  :extrafuns ((AT1_PROC1_X Int))
  :extrapreds ((AT3_PROC6_A))
  :extrapreds ((AT1_PROC6_C))
  :extrapreds ((AT2_PROC2_CS))
  :extrapreds ((AT1_PROC4_TAU))
  :extrapreds ((AT1_PROC6_B))
  :extrapreds ((AT1_PROC7_SW_CS_A_TAU))
  :extrapreds ((AT0_PROC6_SW_C_CS_TAU))
  :extrafuns ((AT1_Z Int))
  :extrapreds ((AT1_PROC6_A))
  :extrapreds ((AT2_PROC3_SW_C_CS_TAU))
  :extrapreds ((AT2_PROC2_C))
  :extrapreds ((AT2_PROC4_SW_A_B_TAU))
  :extrapreds ((AT0_PROC4_SW_B_C_TAU))
  :extrapreds ((AT2_PROC2_B))
  :extrapreds ((AT1_PROC8_TAU))
  :extrapreds ((AT1_PROC8_SW_C_CS_TAU))
  :extrapreds ((AT3_PROC4_CS))
  :extrapreds ((AT2_PROC2_A))
  :extrapreds ((AT0_PROC2_C))
  :extrapreds ((AT2_ID0))
  :extrapreds ((AT0_PROC7_WAIT))
  :extrapreds ((AT0_PROC2_SW_C_CS_TAU))
  :extrapreds ((AT0_PROC2_B))
  :extrapreds ((AT2_ID1))
  :extrapreds ((AT0_PROC2_A))
  :extrapreds ((AT2_ID2))
  :extrafuns ((AT2_PROC8_X Int))
  :extrapreds ((AT2_ID3))
  :extrapreds ((AT2_PROC3_SW_A_B_TAU))
  :extrapreds ((AT0_PROC3_SW_B_C_TAU))
  :extrapreds ((AT2_PROC2_WAIT))
  :extrapreds ((AT0_PROC1_SW_C_B_TAU))
  :extrapreds ((AT0_PROC1_CS))
  :extrapreds ((AT2_ID4))
  :extrafuns ((AT0_PROC8_X Int))
  :extrapreds ((AT2_ID5))
  :extrapreds ((AT0_PROC5_SW_A_B_TAU))
  :extrapreds ((AT0_PROC4_WAIT))
  :extrafuns ((AT3_PROC4_X Int))
  :extrapreds ((AT2_ID6))
  :extrapreds ((AT1_PROC7_CS))
  :extrapreds ((AT2_ID7))
  :extrapreds ((AT0_PROC1_TAU))
  :extrapreds ((AT1_PROC4_SW_B_C_TAU))
  :extrapreds ((AT2_PROC1_SW_CS_A_TAU))
  :extrapreds ((AT0_PROC1_SW_C_CS_TAU))
  :extrafuns ((AT1_PROC4_X Int))
  :extrapreds ((AT2_ID8))
  :extrapreds ((AT2_PROC5_WAIT))
  :extrapreds ((AT0_PROC4_SW_CS_A_TAU))
  :extrapreds ((AT2_PROC2_SW_C_CS_TAU))
  :extrapreds ((AT0_PROC1_WAIT))
  :extrapreds ((AT2_PROC5_C))
  :extrapreds ((AT3_PROC1_CS))
  :extrapreds ((AT0_PROC5_TAU))
  :extrapreds ((AT2_PROC5_SW_CS_A_TAU))
  :extrapreds ((AT0_PROC5_SW_C_CS_TAU))
  :extrapreds ((AT2_PROC5_B))
  :extrapreds ((AT2_PROC4_TAU))
  :extrapreds ((AT0_PROC8_SW_CS_A_TAU))
  :extrapreds ((AT1_PROC5_SW_C_CS_TAU))
  :extrapreds ((AT1_PROC3_SW_A_B_TAU))
  :extrapreds ((AT1_PROC1_SW_C_B_TAU))
  :extrapreds ((AT2_PROC5_A))
  :extrapreds ((AT0_PROC5_C))
  :extrapreds ((AT2_PROC8_WAIT))
  :extrapreds ((AT2_PROC7_SW_B_C_TAU))
  :extrapreds ((AT0_PROC5_B))
  :extrapreds ((AT3_PROC1_C))
  :extrapreds ((AT2_PROC6_SW_C_CS_TAU))
  :extrapreds ((AT1_PROC5_SW_A_B_TAU))
  :extrapreds ((AT0_PROC5_A))
  :extrapreds ((AT0_PROC4_CS))
  :extrapreds ((AT3_PROC1_B))
  :extrapreds ((AT1_PROC4_SW_CS_A_TAU))
  :extrapreds ((AT3_PROC1_A))
  :extrapreds ((AT1_PROC1_C))
  :extrapreds ((AT2_PROC8_TAU))
  :extrapreds ((AT2_PROC4_SW_B_C_TAU))
  :extrapreds ((AT1_PROC1_SW_C_CS_TAU))
  :extrapreds ((AT1_PROC1_B))
  :extrapreds ((AT1_PROC4_CS))
  :extrapreds ((AT1_PROC1_A))
  :extrafuns ((AT3_PROC7_X Int))
  :extrafuns ((AT1_PROC7_X Int))
  :extrapreds ((AT0_PROC3_SW_A_B_TAU))
  :extrapreds ((AT2_PROC1_SW_C_B_TAU))
  :extrapreds ((AT0_DELTA))
  :extrapreds ((AT2_PROC6_CS))
  :extrapreds ((AT2_PROC5_SW_A_B_TAU))
  :extrapreds ((AT0_PROC5_SW_B_C_TAU))
  :extrapreds ((AT1_PROC2_SW_CS_A_TAU))
  :extrafuns ((AT2_PROC3_X Int))
  :extrapreds ((AT2_PROC8_C))
  :extrapreds ((AT1_PROC1_TAU))
  :extrapreds ((AT2_PROC8_SW_C_CS_TAU))
  :extrapreds ((AT2_PROC8_B))
  :extrapreds ((AT0_PROC7_SW_C_B_TAU))
  :extrafuns ((AT0_PROC3_X Int))
  :extrapreds ((AT2_PROC8_A))
  :extrapreds ((AT0_PROC8_C))
  :extrapreds ((AT0_PROC7_CS))
  :extrapreds ((AT1_PROC3_SW_C_CS_TAU))
  :extrapreds ((AT0_PROC8_B))
  :extrapreds ((AT3_PROC4_C))
  :extrapreds ((AT2_PROC7_SW_CS_A_TAU))
  :extrapreds ((AT0_PROC7_SW_C_CS_TAU))
  :extrapreds ((AT1_PROC6_SW_CS_A_TAU))
  :extrapreds ((AT3_PROC8_CS))
  :extrapreds ((AT0_PROC8_A))
  :extrapreds ((AT3_PROC4_B))
  :extrapreds ((AT1_PROC5_TAU))
  :extrapreds ((AT2_PROC4_SW_C_CS_TAU))
  :extrapreds ((AT1_PROC2_WAIT))
  :extrapreds ((AT0_PROC2_SW_B_C_TAU))
  :extrapreds ((AT3_PROC4_A))
  :extrapreds ((AT1_PROC4_C))
  :extrapreds ((AT1_PROC1_CS))
  :extrapreds ((AT1_PROC4_B))
  :extrapreds ((AT1_PROC7_SW_C_CS_TAU))
  :extrapreds ((AT0_PROC6_SW_CS_A_TAU))
  :extrafuns ((AT3_Z Int))
  :extrapreds ((AT1_PROC4_A))
  :extrapreds ((AT2_PROC7_SW_A_B_TAU))
  :extrapreds ((AT2_PROC3_SW_CS_A_TAU))
  :extrapreds ((AT0_PROC3_SW_C_CS_TAU))
  :extrapreds ((AT1_PROC5_SW_B_C_TAU))
  :extrapreds ((AT3_ID0))
  :extrapreds ((AT1_PROC5_WAIT))
  :extrapreds ((AT2_PROC3_SW_C_B_TAU))
  :extrapreds ((AT0_PROC1_SW_A_B_TAU))
  :extrapreds ((AT2_PROC3_CS))
  :extrapreds ((AT3_ID1))
  :extrapreds ((AT1_PROC7_SW_C_B_TAU))
  :extrapreds ((AT0_PROC2_SW_CS_A_TAU))
  :extrapreds ((AT3_ID2))
  :extrapreds ((AT3_ID3))
  :extrapreds ((AT1_DELTA))
  :extrafuns ((AT2_PROC6_X Int))
  :extrapreds ((AT3_ID4))
  :extrapreds ((AT1_PROC2_SW_C_B_TAU))
  :extrapreds ((AT3_ID5))
  :extrapreds ((AT1_PROC8_WAIT))
  :extrapreds ((AT2_PROC6_SW_B_C_TAU))
  :extrafuns ((AT0_PROC6_X Int))
  :extrapreds ((AT3_PROC5_CS))
  :extrapreds ((AT3_ID6))
  :extrafuns ((AT3_PROC2_X Int))
  :extrapreds ((AT3_PROC7_C))
  :extrapreds ((AT3_ID7))
  :extrapreds ((AT0_PROC2_TAU))
  :extrapreds ((AT3_PROC7_B))
  :extrapreds ((AT3_ID8))
  :extrapreds ((AT2_PROC1_TAU))
  :extrapreds ((AT0_PROC8_WAIT))
  :extrapreds ((AT2_PROC5_SW_B_C_TAU))
  :extrapreds ((AT2_PROC1_SW_C_CS_TAU))
  :extrafuns ((AT1_PROC2_X Int))
  :extrapreds ((AT3_PROC7_A))
  :extrapreds ((AT1_PROC7_C))
  :extrapreds ((AT0_PROC4_SW_C_CS_TAU))
  :extrapreds ((AT1_PROC3_SW_C_B_TAU))
  :extrapreds ((AT1_PROC1_SW_A_B_TAU))
  :extrapreds ((AT1_PROC7_B))
  :extrafuns ((AT0_Z Int))
  :extrapreds ((AT1_PROC7_A))
  :extrapreds ((AT0_PROC6_TAU))
  :extrapreds ((AT2_PROC1_WAIT))
  :extrapreds ((AT2_PROC3_C))
  :extrapreds ((AT2_PROC5_TAU))
  :extrapreds ((AT2_PROC5_SW_C_CS_TAU))
  :extrapreds ((AT1_PROC8_CS))
  :extrapreds ((AT2_PROC3_B))
  :extrapreds ((AT0_PROC8_SW_C_CS_TAU))
  :extrapreds ((AT1_PROC5_SW_CS_A_TAU))
  :extrapreds ((AT0_PROC5_WAIT))
  :extrapreds ((AT2_PROC2_SW_C_B_TAU))
  :extrapreds ((AT0_PROC2_SW_A_B_TAU))
  :extrapreds ((AT2_PROC3_A))
  :extrapreds ((AT0_PROC3_C))
  :extrapreds ((AT1_PROC6_SW_B_C_TAU))
  :extrapreds ((AT0_PROC3_B))
  :extrapreds ((AT0_PROC3_A))
  :extrapreds ((AT2_PROC4_WAIT))
  :extrapreds ((AT3_PROC2_CS))
  :extrapreds ((AT0_PROC8_SW_C_B_TAU))
  :extrapreds ((AT1_PROC1_SW_CS_A_TAU))
  :extrapreds ((AT0_PROC3_SW_C_B_TAU))
  :extrapreds ((AT0_PROC2_WAIT))
  :extrapreds ((AT2_PROC1_SW_A_B_TAU))
  :extrapreds ((AT2_DELTA))
  :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 AT2_PROC1_A)) (flet ($cvcl_9 (not AT2_PROC1_B)) (flet ($cvcl_10 (not AT2_PROC1_C)) (flet ($cvcl_11 (not AT2_PROC1_CS)) (flet ($cvcl_12 (not AT3_PROC1_A)) (flet ($cvcl_13 (not AT3_PROC1_B)) (flet ($cvcl_14 (not AT3_PROC1_C)) (flet ($cvcl_15 (not AT3_PROC1_CS)) (flet ($cvcl_16 (not AT0_PROC2_A)) (flet ($cvcl_17 (not AT0_PROC2_B)) (flet ($cvcl_18 (not AT0_PROC2_C)) (flet ($cvcl_19 (not AT0_PROC2_CS)) (flet ($cvcl_20 (not AT1_PROC2_A)) (flet ($cvcl_21 (not AT1_PROC2_B)) (flet ($cvcl_22 (not AT1_PROC2_C)) (flet ($cvcl_23 (not AT1_PROC2_CS)) (flet ($cvcl_24 (not AT2_PROC2_A)) (flet ($cvcl_25 (not AT2_PROC2_B)) (flet ($cvcl_26 (not AT2_PROC2_C)) (flet ($cvcl_27 (not AT2_PROC2_CS)) (flet ($cvcl_28 (not AT3_PROC2_A)) (flet ($cvcl_29 (not AT3_PROC2_B)) (flet ($cvcl_30 (not AT3_PROC2_C)) (flet ($cvcl_31 (not AT3_PROC2_CS)) (flet ($cvcl_32 (not AT0_PROC3_A)) (flet ($cvcl_33 (not AT0_PROC3_B)) (flet ($cvcl_34 (not AT0_PROC3_C)) (flet ($cvcl_35 (not AT0_PROC3_CS)) (flet ($cvcl_36 (not AT1_PROC3_A)) (flet ($cvcl_37 (not AT1_PROC3_B)) (flet ($cvcl_38 (not AT1_PROC3_C)) (flet ($cvcl_39 (not AT1_PROC3_CS)) (flet ($cvcl_40 (not AT2_PROC3_A)) (flet ($cvcl_41 (not AT2_PROC3_B)) (flet ($cvcl_42 (not AT2_PROC3_C)) (flet ($cvcl_43 (not AT2_PROC3_CS)) (flet ($cvcl_44 (not AT3_PROC3_A)) (flet ($cvcl_45 (not AT3_PROC3_B)) (flet ($cvcl_46 (not AT3_PROC3_C)) (flet ($cvcl_47 (not AT3_PROC3_CS)) (flet ($cvcl_48 (not AT0_PROC4_A)) (flet ($cvcl_49 (not AT0_PROC4_B)) (flet ($cvcl_50 (not AT0_PROC4_C)) (flet ($cvcl_51 (not AT0_PROC4_CS)) (flet ($cvcl_52 (not AT1_PROC4_A)) (flet ($cvcl_53 (not AT1_PROC4_B)) (flet ($cvcl_54 (not AT1_PROC4_C)) (flet ($cvcl_55 (not AT1_PROC4_CS)) (flet ($cvcl_56 (not AT2_PROC4_A)) (flet ($cvcl_57 (not AT2_PROC4_B)) (flet ($cvcl_58 (not AT2_PROC4_C)) (flet ($cvcl_59 (not AT2_PROC4_CS)) (flet ($cvcl_60 (not AT3_PROC4_A)) (flet ($cvcl_61 (not AT3_PROC4_B)) (flet ($cvcl_62 (not AT3_PROC4_C)) (flet ($cvcl_63 (not AT3_PROC4_CS)) (flet ($cvcl_64 (not AT0_PROC5_A)) (flet ($cvcl_65 (not AT0_PROC5_B)) (flet ($cvcl_66 (not AT0_PROC5_C)) (flet ($cvcl_67 (not AT0_PROC5_CS)) (flet ($cvcl_68 (not AT1_PROC5_A)) (flet ($cvcl_69 (not AT1_PROC5_B)) (flet ($cvcl_70 (not AT1_PROC5_C)) (flet ($cvcl_71 (not AT1_PROC5_CS)) (flet ($cvcl_72 (not AT2_PROC5_A)) (flet ($cvcl_73 (not AT2_PROC5_B)) (flet ($cvcl_74 (not AT2_PROC5_C)) (flet ($cvcl_75 (not AT2_PROC5_CS)) (flet ($cvcl_76 (not AT3_PROC5_A)) (flet ($cvcl_77 (not AT3_PROC5_B)) (flet ($cvcl_78 (not AT3_PROC5_C)) (flet ($cvcl_79 (not AT3_PROC5_CS)) (flet ($cvcl_80 (not AT0_PROC6_A)) (flet ($cvcl_81 (not AT0_PROC6_B)) (flet ($cvcl_82 (not AT0_PROC6_C)) (flet ($cvcl_83 (not AT0_PROC6_CS)) (flet ($cvcl_84 (not AT1_PROC6_A)) (flet ($cvcl_85 (not AT1_PROC6_B)) (flet ($cvcl_86 (not AT1_PROC6_C)) (flet ($cvcl_87 (not AT1_PROC6_CS)) (flet ($cvcl_88 (not AT2_PROC6_A)) (flet ($cvcl_89 (not AT2_PROC6_B)) (flet ($cvcl_90 (not AT2_PROC6_C)) (flet ($cvcl_91 (not AT2_PROC6_CS)) (flet ($cvcl_92 (not AT3_PROC6_A)) (flet ($cvcl_93 (not AT3_PROC6_B)) (flet ($cvcl_94 (not AT3_PROC6_C)) (flet ($cvcl_95 (not AT3_PROC6_CS)) (flet ($cvcl_96 (not AT0_PROC7_A)) (flet ($cvcl_97 (not AT0_PROC7_B)) (flet ($cvcl_98 (not AT0_PROC7_C)) (flet ($cvcl_99 (not AT0_PROC7_CS)) (flet ($cvcl_100 (not AT1_PROC7_A)) (flet ($cvcl_101 (not AT1_PROC7_B)) (flet ($cvcl_102 (not AT1_PROC7_C)) (flet ($cvcl_103 (not AT1_PROC7_CS)) (flet ($cvcl_104 (not AT2_PROC7_A)) (flet ($cvcl_105 (not AT2_PROC7_B)) (flet ($cvcl_106 (not AT2_PROC7_C)) (flet ($cvcl_107 (not AT2_PROC7_CS)) (flet ($cvcl_108 (not AT3_PROC7_A)) (flet ($cvcl_109 (not AT3_PROC7_B)) (flet ($cvcl_110 (not AT3_PROC7_C)) (flet ($cvcl_111 (not AT3_PROC7_CS)) (flet ($cvcl_112 (not AT0_PROC8_A)) (flet ($cvcl_113 (not AT0_PROC8_B)) (flet ($cvcl_114 (not AT0_PROC8_C)) (flet ($cvcl_115 (not AT0_PROC8_CS)) (flet ($cvcl_116 (not AT1_PROC8_A)) (flet ($cvcl_117 (not AT1_PROC8_B)) (flet ($cvcl_118 (not AT1_PROC8_C)) (flet ($cvcl_119 (not AT1_PROC8_CS)) (flet ($cvcl_120 (not AT2_PROC8_A)) (flet ($cvcl_121 (not AT2_PROC8_B)) (flet ($cvcl_122 (not AT2_PROC8_C)) (flet ($cvcl_123 (not AT2_PROC8_CS)) (flet ($cvcl_124 (not AT3_PROC8_A)) (flet ($cvcl_125 (not AT3_PROC8_B)) (flet ($cvcl_126 (not AT3_PROC8_C)) (flet ($cvcl_127 (not AT3_PROC8_CS)) (flet ($cvcl_128 (= AT0_PROC1_X AT0_Z)) (flet ($cvcl_129 (> AT0_PROC1_X AT0_Z)) (flet ($cvcl_447 (not $cvcl_128)) (flet ($cvcl_130 (= AT1_PROC1_X AT1_Z)) (flet ($cvcl_131 (> AT1_PROC1_X AT1_Z)) (flet ($cvcl_446 (not $cvcl_130)) (flet ($cvcl_132 (= AT2_PROC1_X AT2_Z)) (flet ($cvcl_133 (> AT2_PROC1_X AT2_Z)) (flet ($cvcl_452 (not $cvcl_132)) (flet ($cvcl_134 (= AT3_PROC1_X AT3_Z)) (flet ($cvcl_135 (> AT3_PROC1_X AT3_Z)) (flet ($cvcl_458 (not $cvcl_134)) (flet ($cvcl_136 (= AT0_PROC2_X AT0_Z)) (flet ($cvcl_137 (> AT0_PROC2_X AT0_Z)) (flet ($cvcl_464 (not $cvcl_136)) (flet ($cvcl_138 (= AT1_PROC2_X AT1_Z)) (flet ($cvcl_139 (> AT1_PROC2_X AT1_Z)) (flet ($cvcl_463 (not $cvcl_138)) (flet ($cvcl_140 (= AT2_PROC2_X AT2_Z)) (flet ($cvcl_141 (> AT2_PROC2_X AT2_Z)) (flet ($cvcl_467 (not $cvcl_140)) (flet ($cvcl_142 (= AT3_PROC2_X AT3_Z)) (flet ($cvcl_143 (> AT3_PROC2_X AT3_Z)) (flet ($cvcl_471 (not $cvcl_142)) (flet ($cvcl_144 (= AT0_PROC3_X AT0_Z)) (flet ($cvcl_145 (> AT0_PROC3_X AT0_Z)) (flet ($cvcl_476 (not $cvcl_144)) (flet ($cvcl_146 (= AT1_PROC3_X AT1_Z)) (flet ($cvcl_147 (> AT1_PROC3_X AT1_Z)) (flet ($cvcl_475 (not $cvcl_146)) (flet ($cvcl_148 (= AT2_PROC3_X AT2_Z)) (flet ($cvcl_149 (> AT2_PROC3_X AT2_Z)) (flet ($cvcl_479 (not $cvcl_148)) (flet ($cvcl_150 (= AT3_PROC3_X AT3_Z)) (flet ($cvcl_151 (> AT3_PROC3_X AT3_Z)) (flet ($cvcl_483 (not $cvcl_150)) (flet ($cvcl_152 (= AT0_PROC4_X AT0_Z)) (flet ($cvcl_153 (> AT0_PROC4_X AT0_Z)) (flet ($cvcl_488 (not $cvcl_152)) (flet ($cvcl_154 (= AT1_PROC4_X AT1_Z)) (flet ($cvcl_155 (> AT1_PROC4_X AT1_Z)) (flet ($cvcl_487 (not $cvcl_154)) (flet ($cvcl_156 (= AT2_PROC4_X AT2_Z)) (flet ($cvcl_157 (> AT2_PROC4_X AT2_Z)) (flet ($cvcl_491 (not $cvcl_156)) (flet ($cvcl_158 (= AT3_PROC4_X AT3_Z)) (flet ($cvcl_159 (> AT3_PROC4_X AT3_Z)) (flet ($cvcl_495 (not $cvcl_158)) (flet ($cvcl_160 (= AT0_PROC5_X AT0_Z)) (flet ($cvcl_161 (> AT0_PROC5_X AT0_Z)) (flet ($cvcl_500 (not $cvcl_160)) (flet ($cvcl_162 (= AT1_PROC5_X AT1_Z)) (flet ($cvcl_163 (> AT1_PROC5_X AT1_Z)) (flet ($cvcl_499 (not $cvcl_162)) (flet ($cvcl_164 (= AT2_PROC5_X AT2_Z)) (flet ($cvcl_165 (> AT2_PROC5_X AT2_Z)) (flet ($cvcl_503 (not $cvcl_164)) (flet ($cvcl_166 (= AT3_PROC5_X AT3_Z)) (flet ($cvcl_167 (> AT3_PROC5_X AT3_Z)) (flet ($cvcl_507 (not $cvcl_166)) (flet ($cvcl_168 (= AT0_PROC6_X AT0_Z)) (flet ($cvcl_169 (> AT0_PROC6_X AT0_Z)) (flet ($cvcl_512 (not $cvcl_168)) (flet ($cvcl_170 (= AT1_PROC6_X AT1_Z)) (flet ($cvcl_171 (> AT1_PROC6_X AT1_Z)) (flet ($cvcl_511 (not $cvcl_170)) (flet ($cvcl_172 (= AT2_PROC6_X AT2_Z)) (flet ($cvcl_173 (> AT2_PROC6_X AT2_Z)) (flet ($cvcl_515 (not $cvcl_172)) (flet ($cvcl_174 (= AT3_PROC6_X AT3_Z)) (flet ($cvcl_175 (> AT3_PROC6_X AT3_Z)) (flet ($cvcl_519 (not $cvcl_174)) (flet ($cvcl_176 (= AT0_PROC7_X AT0_Z)) (flet ($cvcl_177 (> AT0_PROC7_X AT0_Z)) (flet ($cvcl_524 (not $cvcl_176)) (flet ($cvcl_178 (= AT1_PROC7_X AT1_Z)) (flet ($cvcl_179 (> AT1_PROC7_X AT1_Z)) (flet ($cvcl_523 (not $cvcl_178)) (flet ($cvcl_180 (= AT2_PROC7_X AT2_Z)) (flet ($cvcl_181 (> AT2_PROC7_X AT2_Z)) (flet ($cvcl_527 (not $cvcl_180)) (flet ($cvcl_182 (= AT3_PROC7_X AT3_Z)) (flet ($cvcl_183 (> AT3_PROC7_X AT3_Z)) (flet ($cvcl_531 (not $cvcl_182)) (flet ($cvcl_184 (= AT0_PROC8_X AT0_Z)) (flet ($cvcl_185 (> AT0_PROC8_X AT0_Z)) (flet ($cvcl_536 (not $cvcl_184)) (flet ($cvcl_186 (= AT1_PROC8_X AT1_Z)) (flet ($cvcl_187 (> AT1_PROC8_X AT1_Z)) (flet ($cvcl_535 (not $cvcl_186)) (flet ($cvcl_188 (= AT2_PROC8_X AT2_Z)) (flet ($cvcl_189 (> AT2_PROC8_X AT2_Z)) (flet ($cvcl_539 (not $cvcl_188)) (flet ($cvcl_190 (= AT3_PROC8_X AT3_Z)) (flet ($cvcl_191 (> AT3_PROC8_X AT3_Z)) (flet ($cvcl_543 (not $cvcl_190)) (flet ($cvcl_194 (<= (- AT0_PROC1_X AT0_Z) 10)) (flet ($cvcl_200 (<= (- AT1_PROC1_X AT1_Z) 10)) (flet ($cvcl_206 (<= (- AT2_PROC1_X AT2_Z) 10)) (flet ($cvcl_215 (<= (- AT0_PROC2_X AT0_Z) 10)) (flet ($cvcl_221 (<= (- AT1_PROC2_X AT1_Z) 10)) (flet ($cvcl_227 (<= (- AT2_PROC2_X AT2_Z) 10)) (flet ($cvcl_233 (<= (- AT0_PROC3_X AT0_Z) 10)) (flet ($cvcl_239 (<= (- AT1_PROC3_X AT1_Z) 10)) (flet ($cvcl_245 (<= (- AT2_PROC3_X AT2_Z) 10)) (flet ($cvcl_251 (<= (- AT0_PROC4_X AT0_Z) 10)) (flet ($cvcl_257 (<= (- AT1_PROC4_X AT1_Z) 10)) (flet ($cvcl_263 (<= (- AT2_PROC4_X AT2_Z) 10)) (flet ($cvcl_269 (<= (- AT0_PROC5_X AT0_Z) 10)) (flet ($cvcl_275 (<= (- AT1_PROC5_X AT1_Z) 10)) (flet ($cvcl_281 (<= (- AT2_PROC5_X AT2_Z) 10)) (flet ($cvcl_287 (<= (- AT0_PROC6_X AT0_Z) 10)) (flet ($cvcl_293 (<= (- AT1_PROC6_X AT1_Z) 10)) (flet ($cvcl_299 (<= (- AT2_PROC6_X AT2_Z) 10)) (flet ($cvcl_305 (<= (- AT0_PROC7_X AT0_Z) 10)) (flet ($cvcl_311 (<= (- AT1_PROC7_X AT1_Z) 10)) (flet ($cvcl_317 (<= (- AT2_PROC7_X AT2_Z) 10)) (flet ($cvcl_323 (<= (- AT0_PROC8_X AT0_Z) 10)) (flet ($cvcl_329 (<= (- AT1_PROC8_X AT1_Z) 10)) (flet ($cvcl_335 (<= (- AT2_PROC8_X AT2_Z) 10)) (flet ($cvcl_192 (not AT0_PROC1_SW_A_B_TAU)) (flet ($cvcl_193 (not AT0_PROC1_SW_B_C_TAU)) (flet ($cvcl_195 (not AT0_PROC1_SW_C_B_TAU)) (flet ($cvcl_196 (not AT0_PROC1_SW_C_CS_TAU)) (flet ($cvcl_340 (= AT1_PROC1_X AT0_PROC1_X)) (flet ($cvcl_197 (not AT0_PROC1_SW_CS_A_TAU)) (flet ($cvcl_198 (not AT1_PROC1_SW_A_B_TAU)) (flet ($cvcl_199 (not AT1_PROC1_SW_B_C_TAU)) (flet ($cvcl_201 (not AT1_PROC1_SW_C_B_TAU)) (flet ($cvcl_202 (not AT1_PROC1_SW_C_CS_TAU)) (flet ($cvcl_342 (= AT2_PROC1_X AT1_PROC1_X)) (flet ($cvcl_203 (not AT1_PROC1_SW_CS_A_TAU)) (flet ($cvcl_204 (not AT2_PROC1_SW_A_B_TAU)) (flet ($cvcl_205 (not AT2_PROC1_SW_B_C_TAU)) (flet ($cvcl_207 (not AT2_PROC1_SW_C_B_TAU)) (flet ($cvcl_208 (not AT2_PROC1_SW_C_CS_TAU)) (flet ($cvcl_344 (= AT3_PROC1_X AT2_PROC1_X)) (flet ($cvcl_209 (not AT2_PROC1_SW_CS_A_TAU)) (flet ($cvcl_210 (= AT1_Z AT0_Z)) (flet ($cvcl_211 (= AT2_Z AT1_Z)) (flet ($cvcl_212 (= AT3_Z AT2_Z)) (flet ($cvcl_213 (not AT0_PROC2_SW_A_B_TAU)) (flet ($cvcl_214 (not AT0_PROC2_SW_B_C_TAU)) (flet ($cvcl_216 (not AT0_PROC2_SW_C_B_TAU)) (flet ($cvcl_217 (not AT0_PROC2_SW_C_CS_TAU)) (flet ($cvcl_346 (= AT1_PROC2_X AT0_PROC2_X)) (flet ($cvcl_218 (not AT0_PROC2_SW_CS_A_TAU)) (flet ($cvcl_219 (not AT1_PROC2_SW_A_B_TAU)) (flet ($cvcl_220 (not AT1_PROC2_SW_B_C_TAU)) (flet ($cvcl_222 (not AT1_PROC2_SW_C_B_TAU)) (flet ($cvcl_223 (not AT1_PROC2_SW_C_CS_TAU)) (flet ($cvcl_348 (= AT2_PROC2_X AT1_PROC2_X)) (flet ($cvcl_224 (not AT1_PROC2_SW_CS_A_TAU)) (flet ($cvcl_225 (not AT2_PROC2_SW_A_B_TAU)) (flet ($cvcl_226 (not AT2_PROC2_SW_B_C_TAU)) (flet ($cvcl_228 (not AT2_PROC2_SW_C_B_TAU)) (flet ($cvcl_229 (not AT2_PROC2_SW_C_CS_TAU)) (flet ($cvcl_350 (= AT3_PROC2_X AT2_PROC2_X)) (flet ($cvcl_230 (not AT2_PROC2_SW_CS_A_TAU)) (flet ($cvcl_231 (not AT0_PROC3_SW_A_B_TAU)) (flet ($cvcl_232 (not AT0_PROC3_SW_B_C_TAU)) (flet ($cvcl_234 (not AT0_PROC3_SW_C_B_TAU)) (flet ($cvcl_235 (not AT0_PROC3_SW_C_CS_TAU)) (flet ($cvcl_352 (= AT1_PROC3_X AT0_PROC3_X)) (flet ($cvcl_236 (not AT0_PROC3_SW_CS_A_TAU)) (flet ($cvcl_237 (not AT1_PROC3_SW_A_B_TAU)) (flet ($cvcl_238 (not AT1_PROC3_SW_B_C_TAU)) (flet ($cvcl_240 (not AT1_PROC3_SW_C_B_TAU)) (flet ($cvcl_241 (not AT1_PROC3_SW_C_CS_TAU)) (flet ($cvcl_354 (= AT2_PROC3_X AT1_PROC3_X)) (flet ($cvcl_242 (not AT1_PROC3_SW_CS_A_TAU)) (flet ($cvcl_243 (not AT2_PROC3_SW_A_B_TAU)) (flet ($cvcl_244 (not AT2_PROC3_SW_B_C_TAU)) (flet ($cvcl_246 (not AT2_PROC3_SW_C_B_TAU)) (flet ($cvcl_247 (not AT2_PROC3_SW_C_CS_TAU)) (flet ($cvcl_356 (= AT3_PROC3_X AT2_PROC3_X)) (flet ($cvcl_248 (not AT2_PROC3_SW_CS_A_TAU)) (flet ($cvcl_249 (not AT0_PROC4_SW_A_B_TAU)) (flet ($cvcl_250 (not AT0_PROC4_SW_B_C_TAU)) (flet ($cvcl_252 (not AT0_PROC4_SW_C_B_TAU)) (flet ($cvcl_253 (not AT0_PROC4_SW_C_CS_TAU)) (flet ($cvcl_358 (= AT1_PROC4_X AT0_PROC4_X)) (flet ($cvcl_254 (not AT0_PROC4_SW_CS_A_TAU)) (flet ($cvcl_255 (not AT1_PROC4_SW_A_B_TAU)) (flet ($cvcl_256 (not AT1_PROC4_SW_B_C_TAU)) (flet ($cvcl_258 (not AT1_PROC4_SW_C_B_TAU)) (flet ($cvcl_259 (not AT1_PROC4_SW_C_CS_TAU)) (flet ($cvcl_360 (= AT2_PROC4_X AT1_PROC4_X)) (flet ($cvcl_260 (not AT1_PROC4_SW_CS_A_TAU)) (flet ($cvcl_261 (not AT2_PROC4_SW_A_B_TAU)) (flet ($cvcl_262 (not AT2_PROC4_SW_B_C_TAU)) (flet ($cvcl_264 (not AT2_PROC4_SW_C_B_TAU)) (flet ($cvcl_265 (not AT2_PROC4_SW_C_CS_TAU)) (flet ($cvcl_362 (= AT3_PROC4_X AT2_PROC4_X)) (flet ($cvcl_266 (not AT2_PROC4_SW_CS_A_TAU)) (flet ($cvcl_267 (not AT0_PROC5_SW_A_B_TAU)) (flet ($cvcl_268 (not AT0_PROC5_SW_B_C_TAU)) (flet ($cvcl_270 (not AT0_PROC5_SW_C_B_TAU)) (flet ($cvcl_271 (not AT0_PROC5_SW_C_CS_TAU)) (flet ($cvcl_364 (= AT1_PROC5_X AT0_PROC5_X)) (flet ($cvcl_272 (not AT0_PROC5_SW_CS_A_TAU)) (flet ($cvcl_273 (not AT1_PROC5_SW_A_B_TAU)) (flet ($cvcl_274 (not AT1_PROC5_SW_B_C_TAU)) (flet ($cvcl_276 (not AT1_PROC5_SW_C_B_TAU)) (flet ($cvcl_277 (not AT1_PROC5_SW_C_CS_TAU)) (flet ($cvcl_366 (= AT2_PROC5_X AT1_PROC5_X)) (flet ($cvcl_278 (not AT1_PROC5_SW_CS_A_TAU)) (flet ($cvcl_279 (not AT2_PROC5_SW_A_B_TAU)) (flet ($cvcl_280 (not AT2_PROC5_SW_B_C_TAU)) (flet ($cvcl_282 (not AT2_PROC5_SW_C_B_TAU)) (flet ($cvcl_283 (not AT2_PROC5_SW_C_CS_TAU)) (flet ($cvcl_368 (= AT3_PROC5_X AT2_PROC5_X)) (flet ($cvcl_284 (not AT2_PROC5_SW_CS_A_TAU)) (flet ($cvcl_285 (not AT0_PROC6_SW_A_B_TAU)) (flet ($cvcl_286 (not AT0_PROC6_SW_B_C_TAU)) (flet ($cvcl_288 (not AT0_PROC6_SW_C_B_TAU)) (flet ($cvcl_289 (not AT0_PROC6_SW_C_CS_TAU)) (flet ($cvcl_370 (= AT1_PROC6_X AT0_PROC6_X)) (flet ($cvcl_290 (not AT0_PROC6_SW_CS_A_TAU)) (flet ($cvcl_291 (not AT1_PROC6_SW_A_B_TAU)) (flet ($cvcl_292 (not AT1_PROC6_SW_B_C_TAU)) (flet ($cvcl_294 (not AT1_PROC6_SW_C_B_TAU)) (flet ($cvcl_295 (not AT1_PROC6_SW_C_CS_TAU)) (flet ($cvcl_372 (= AT2_PROC6_X AT1_PROC6_X)) (flet ($cvcl_296 (not AT1_PROC6_SW_CS_A_TAU)) (flet ($cvcl_297 (not AT2_PROC6_SW_A_B_TAU)) (flet ($cvcl_298 (not AT2_PROC6_SW_B_C_TAU)) (flet ($cvcl_300 (not AT2_PROC6_SW_C_B_TAU)) (flet ($cvcl_301 (not AT2_PROC6_SW_C_CS_TAU)) (flet ($cvcl_374 (= AT3_PROC6_X AT2_PROC6_X)) (flet ($cvcl_302 (not AT2_PROC6_SW_CS_A_TAU)) (flet ($cvcl_303 (not AT0_PROC7_SW_A_B_TAU)) (flet ($cvcl_304 (not AT0_PROC7_SW_B_C_TAU)) (flet ($cvcl_306 (not AT0_PROC7_SW_C_B_TAU)) (flet ($cvcl_307 (not AT0_PROC7_SW_C_CS_TAU)) (flet ($cvcl_376 (= AT1_PROC7_X AT0_PROC7_X)) (flet ($cvcl_308 (not AT0_PROC7_SW_CS_A_TAU)) (flet ($cvcl_309 (not AT1_PROC7_SW_A_B_TAU)) (flet ($cvcl_310 (not AT1_PROC7_SW_B_C_TAU)) (flet ($cvcl_312 (not AT1_PROC7_SW_C_B_TAU)) (flet ($cvcl_313 (not AT1_PROC7_SW_C_CS_TAU)) (flet ($cvcl_378 (= AT2_PROC7_X AT1_PROC7_X)) (flet ($cvcl_314 (not AT1_PROC7_SW_CS_A_TAU)) (flet ($cvcl_315 (not AT2_PROC7_SW_A_B_TAU)) (flet ($cvcl_316 (not AT2_PROC7_SW_B_C_TAU)) (flet ($cvcl_318 (not AT2_PROC7_SW_C_B_TAU)) (flet ($cvcl_319 (not AT2_PROC7_SW_C_CS_TAU)) (flet ($cvcl_380 (= AT3_PROC7_X AT2_PROC7_X)) (flet ($cvcl_320 (not AT2_PROC7_SW_CS_A_TAU)) (flet ($cvcl_321 (not AT0_PROC8_SW_A_B_TAU)) (flet ($cvcl_322 (not AT0_PROC8_SW_B_C_TAU)) (flet ($cvcl_324 (not AT0_PROC8_SW_C_B_TAU)) (flet ($cvcl_325 (not AT0_PROC8_SW_C_CS_TAU)) (flet ($cvcl_382 (= AT1_PROC8_X AT0_PROC8_X)) (flet ($cvcl_326 (not AT0_PROC8_SW_CS_A_TAU)) (flet ($cvcl_327 (not AT1_PROC8_SW_A_B_TAU)) (flet ($cvcl_328 (not AT1_PROC8_SW_B_C_TAU)) (flet ($cvcl_330 (not AT1_PROC8_SW_C_B_TAU)) (flet ($cvcl_331 (not AT1_PROC8_SW_C_CS_TAU)) (flet ($cvcl_384 (= AT2_PROC8_X AT1_PROC8_X)) (flet ($cvcl_332 (not AT1_PROC8_SW_CS_A_TAU)) (flet ($cvcl_333 (not AT2_PROC8_SW_A_B_TAU)) (flet ($cvcl_334 (not AT2_PROC8_SW_B_C_TAU)) (flet ($cvcl_336 (not AT2_PROC8_SW_C_B_TAU)) (flet ($cvcl_337 (not AT2_PROC8_SW_C_CS_TAU)) (flet ($cvcl_386 (= AT3_PROC8_X AT2_PROC8_X)) (flet ($cvcl_338 (not AT2_PROC8_SW_CS_A_TAU)) (flet ($cvcl_339 (not AT0_PROC1_WAIT)) (flet ($cvcl_388 (not AT0_PROC1_TAU)) (flet ($cvcl_341 (not AT1_PROC1_WAIT)) (flet ($cvcl_390 (not AT1_PROC1_TAU)) (flet ($cvcl_343 (not AT2_PROC1_WAIT)) (flet ($cvcl_392 (not AT2_PROC1_TAU)) (flet ($cvcl_345 (not AT0_PROC2_WAIT)) (flet ($cvcl_393 (not AT0_PROC2_TAU)) (flet ($cvcl_347 (not AT1_PROC2_WAIT)) (flet ($cvcl_395 (not AT1_PROC2_TAU)) (flet ($cvcl_349 (not AT2_PROC2_WAIT)) (flet ($cvcl_397 (not AT2_PROC2_TAU)) (flet ($cvcl_351 (not AT0_PROC3_WAIT)) (flet ($cvcl_399 (not AT0_PROC3_TAU)) (flet ($cvcl_353 (not AT1_PROC3_WAIT)) (flet ($cvcl_400 (not AT1_PROC3_TAU)) (flet ($cvcl_355 (not AT2_PROC3_WAIT)) (flet ($cvcl_401 (not AT2_PROC3_TAU)) (flet ($cvcl_357 (not AT0_PROC4_WAIT)) (flet ($cvcl_402 (not AT0_PROC4_TAU)) (flet ($cvcl_359 (not AT1_PROC4_WAIT)) (flet ($cvcl_403 (not AT1_PROC4_TAU)) (flet ($cvcl_361 (not AT2_PROC4_WAIT)) (flet ($cvcl_404 (not AT2_PROC4_TAU)) (flet ($cvcl_363 (not AT0_PROC5_WAIT)) (flet ($cvcl_405 (not AT0_PROC5_TAU)) (flet ($cvcl_365 (not AT1_PROC5_WAIT)) (flet ($cvcl_406 (not AT1_PROC5_TAU)) (flet ($cvcl_367 (not AT2_PROC5_WAIT)) (flet ($cvcl_407 (not AT2_PROC5_TAU)) (flet ($cvcl_369 (not AT0_PROC6_WAIT)) (flet ($cvcl_408 (not AT0_PROC6_TAU)) (flet ($cvcl_371 (not AT1_PROC6_WAIT)) (flet ($cvcl_409 (not AT1_PROC6_TAU)) (flet ($cvcl_373 (not AT2_PROC6_WAIT)) (flet ($cvcl_410 (not AT2_PROC6_TAU)) (flet ($cvcl_375 (not AT0_PROC7_WAIT)) (flet ($cvcl_411 (not AT0_PROC7_TAU)) (flet ($cvcl_377 (not AT1_PROC7_WAIT)) (flet ($cvcl_412 (not AT1_PROC7_TAU)) (flet ($cvcl_379 (not AT2_PROC7_WAIT)) (flet ($cvcl_413 (not AT2_PROC7_TAU)) (flet ($cvcl_381 (not AT0_PROC8_WAIT)) (flet ($cvcl_414 (not AT0_PROC8_TAU)) (flet ($cvcl_383 (not AT1_PROC8_WAIT)) (flet ($cvcl_415 (not AT1_PROC8_TAU)) (flet ($cvcl_385 (not AT2_PROC8_WAIT)) (flet ($cvcl_416 (not AT2_PROC8_TAU)) (flet ($cvcl_387 (not AT0_DELTA)) (flet ($cvcl_441 (< AT1_Z AT0_Z)) (flet ($cvcl_394 (or $cvcl_387  $cvcl_441 )) (flet ($cvcl_389 (not AT1_DELTA)) (flet ($cvcl_442 (< AT2_Z AT1_Z)) (flet ($cvcl_396 (or $cvcl_389  $cvcl_442 )) (flet ($cvcl_391 (not AT2_DELTA)) (flet ($cvcl_443 (< AT3_Z AT2_Z)) (flet ($cvcl_398 (or $cvcl_391  $cvcl_443 )) (flet ($cvcl_417 (< AT1_PROC1_X AT0_PROC1_X)) (flet ($cvcl_444 (not $cvcl_340)) (flet ($cvcl_418 (< AT2_PROC1_X AT1_PROC1_X)) (flet ($cvcl_450 (not $cvcl_342)) (flet ($cvcl_419 (< AT3_PROC1_X AT2_PROC1_X)) (flet ($cvcl_456 (not $cvcl_344)) (flet ($cvcl_420 (< AT1_PROC2_X AT0_PROC2_X)) (flet ($cvcl_462 (not $cvcl_346)) (flet ($cvcl_421 (< AT2_PROC2_X AT1_PROC2_X)) (flet ($cvcl_466 (not $cvcl_348)) (flet ($cvcl_422 (< AT3_PROC2_X AT2_PROC2_X)) (flet ($cvcl_470 (not $cvcl_350)) (flet ($cvcl_423 (< AT1_PROC3_X AT0_PROC3_X)) (flet ($cvcl_474 (not $cvcl_352)) (flet ($cvcl_424 (< AT2_PROC3_X AT1_PROC3_X)) (flet ($cvcl_478 (not $cvcl_354)) (flet ($cvcl_425 (< AT3_PROC3_X AT2_PROC3_X)) (flet ($cvcl_482 (not $cvcl_356)) (flet ($cvcl_426 (< AT1_PROC4_X AT0_PROC4_X)) (flet ($cvcl_486 (not $cvcl_358)) (flet ($cvcl_427 (< AT2_PROC4_X AT1_PROC4_X)) (flet ($cvcl_490 (not $cvcl_360)) (flet ($cvcl_428 (< AT3_PROC4_X AT2_PROC4_X)) (flet ($cvcl_494 (not $cvcl_362)) (flet ($cvcl_429 (< AT1_PROC5_X AT0_PROC5_X)) (flet ($cvcl_498 (not $cvcl_364)) (flet ($cvcl_430 (< AT2_PROC5_X AT1_PROC5_X)) (flet ($cvcl_502 (not $cvcl_366)) (flet ($cvcl_431 (< AT3_PROC5_X AT2_PROC5_X)) (flet ($cvcl_506 (not $cvcl_368)) (flet ($cvcl_432 (< AT1_PROC6_X AT0_PROC6_X)) (flet ($cvcl_510 (not $cvcl_370)) (flet ($cvcl_433 (< AT2_PROC6_X AT1_PROC6_X)) (flet ($cvcl_514 (not $cvcl_372)) (flet ($cvcl_434 (< AT3_PROC6_X AT2_PROC6_X)) (flet ($cvcl_518 (not $cvcl_374)) (flet ($cvcl_435 (< AT1_PROC7_X AT0_PROC7_X)) (flet ($cvcl_522 (not $cvcl_376)) (flet ($cvcl_436 (< AT2_PROC7_X AT1_PROC7_X)) (flet ($cvcl_526 (not $cvcl_378)) (flet ($cvcl_437 (< AT3_PROC7_X AT2_PROC7_X)) (flet ($cvcl_530 (not $cvcl_380)) (flet ($cvcl_438 (< AT1_PROC8_X AT0_PROC8_X)) (flet ($cvcl_534 (not $cvcl_382)) (flet ($cvcl_439 (< AT2_PROC8_X AT1_PROC8_X)) (flet ($cvcl_538 (not $cvcl_384)) (flet ($cvcl_440 (< AT3_PROC8_X AT2_PROC8_X)) (flet ($cvcl_542 (not $cvcl_386)) (flet ($cvcl_445 (not $cvcl_210)) (flet ($cvcl_449 (not $cvcl_441)) (flet ($cvcl_451 (not $cvcl_211)) (flet ($cvcl_455 (not $cvcl_442)) (flet ($cvcl_457 (not $cvcl_212)) (flet ($cvcl_461 (not $cvcl_443)) (flet ($cvcl_448 (or $cvcl_447  $cvcl_444 )) (flet ($cvcl_454 (< AT1_Z AT1_PROC1_X)) (flet ($cvcl_453 (or $cvcl_446  $cvcl_450 )) (flet ($cvcl_460 (< AT2_Z AT2_PROC1_X)) (flet ($cvcl_459 (or $cvcl_452  $cvcl_456 )) (flet ($cvcl_465 (or $cvcl_464  $cvcl_462 )) (flet ($cvcl_469 (< AT1_Z AT1_PROC2_X)) (flet ($cvcl_468 (or $cvcl_463  $cvcl_466 )) (flet ($cvcl_473 (< AT2_Z AT2_PROC2_X)) (flet ($cvcl_472 (or $cvcl_467  $cvcl_470 )) (flet ($cvcl_477 (or $cvcl_476  $cvcl_474 )) (flet ($cvcl_481 (< AT1_Z AT1_PROC3_X)) (flet ($cvcl_480 (or $cvcl_475  $cvcl_478 )) (flet ($cvcl_485 (< AT2_Z AT2_PROC3_X)) (flet ($cvcl_484 (or $cvcl_479  $cvcl_482 )) (flet ($cvcl_489 (or $cvcl_488  $cvcl_486 )) (flet ($cvcl_493 (< AT1_Z AT1_PROC4_X)) (flet ($cvcl_492 (or $cvcl_487  $cvcl_490 )) (flet ($cvcl_497 (< AT2_Z AT2_PROC4_X)) (flet ($cvcl_496 (or $cvcl_491  $cvcl_494 )) (flet ($cvcl_501 (or $cvcl_500  $cvcl_498 )) (flet ($cvcl_505 (< AT1_Z AT1_PROC5_X)) (flet ($cvcl_504 (or $cvcl_499  $cvcl_502 )) (flet ($cvcl_509 (< AT2_Z AT2_PROC5_X)) (flet ($cvcl_508 (or $cvcl_503  $cvcl_506 )) (flet ($cvcl_513 (or $cvcl_512  $cvcl_510 )) (flet ($cvcl_517 (< AT1_Z AT1_PROC6_X)) (flet ($cvcl_516 (or $cvcl_511  $cvcl_514 )) (flet ($cvcl_521 (< AT2_Z AT2_PROC6_X)) (flet ($cvcl_520 (or $cvcl_515  $cvcl_518 )) (flet ($cvcl_525 (or $cvcl_524  $cvcl_522 )) (flet ($cvcl_529 (< AT1_Z AT1_PROC7_X)) (flet ($cvcl_528 (or $cvcl_523  $cvcl_526 )) (flet ($cvcl_533 (< AT2_Z AT2_PROC7_X)) (flet ($cvcl_532 (or $cvcl_527  $cvcl_530 )) (flet ($cvcl_537 (or $cvcl_536  $cvcl_534 )) (flet ($cvcl_541 (< AT1_Z AT1_PROC8_X)) (flet ($cvcl_540 (or $cvcl_535  $cvcl_538 )) (flet ($cvcl_545 (< AT2_Z AT2_PROC8_X)) (flet ($cvcl_544 (or $cvcl_539  $cvcl_542 )) (flet ($cvcl_546 (not AT0_ID0)) (flet ($cvcl_547 (not AT0_ID1)) (flet ($cvcl_548 (not AT0_ID2)) (flet ($cvcl_549 (not AT0_ID3)) (flet ($cvcl_550 (not AT0_ID4)) (flet ($cvcl_551 (not AT0_ID5)) (flet ($cvcl_552 (not AT0_ID6)) (flet ($cvcl_553 (not AT0_ID7)) (flet ($cvcl_554 (not AT0_ID8)) (flet ($cvcl_555 (not AT1_ID0)) (flet ($cvcl_556 (not AT1_ID1)) (flet ($cvcl_557 (not AT1_ID2)) (flet ($cvcl_558 (not AT1_ID3)) (flet ($cvcl_559 (not AT1_ID4)) (flet ($cvcl_560 (not AT1_ID5)) (flet ($cvcl_561 (not AT1_ID6)) (flet ($cvcl_562 (not AT1_ID7)) (flet ($cvcl_563 (not AT1_ID8)) (flet ($cvcl_564 (not AT2_ID0)) (flet ($cvcl_565 (not AT2_ID1)) (flet ($cvcl_566 (not AT2_ID2)) (flet ($cvcl_567 (not AT2_ID3)) (flet ($cvcl_568 (not AT2_ID4)) (flet ($cvcl_569 (not AT2_ID5)) (flet ($cvcl_570 (not AT2_ID6)) (flet ($cvcl_571 (not AT2_ID7)) (flet ($cvcl_572 (not AT2_ID8)) (flet ($cvcl_573 (not AT3_ID0)) (flet ($cvcl_574 (not AT3_ID1)) (flet ($cvcl_575 (not AT3_ID2)) (flet ($cvcl_576 (not AT3_ID3)) (flet ($cvcl_577 (not AT3_ID4)) (flet ($cvcl_578 (not AT3_ID5)) (flet ($cvcl_579 (not AT3_ID6)) (flet ($cvcl_580 (not AT3_ID7)) (flet ($cvcl_581 (not AT3_ID8)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (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_88  $cvcl_90 )) (or $cvcl_88  $cvcl_91 )) (or $cvcl_89  $cvcl_90 )) (or $cvcl_89  $cvcl_91 )) (or $cvcl_90  $cvcl_91 )) (or $cvcl_92  $cvcl_93 )) (or $cvcl_92  $cvcl_94 )) (or $cvcl_92  $cvcl_95 )) (or $cvcl_93  $cvcl_94 )) (or $cvcl_93  $cvcl_95 )) (or $cvcl_94  $cvcl_95 )) (or $cvcl_96  $cvcl_97 )) (or $cvcl_96  $cvcl_98 )) (or $cvcl_96  $cvcl_99 )) (or $cvcl_97  $cvcl_98 )) (or $cvcl_97  $cvcl_99 )) (or $cvcl_98  $cvcl_99 )) (or $cvcl_100  $cvcl_101 )) (or $cvcl_100  $cvcl_102 )) (or $cvcl_100  $cvcl_103 )) (or $cvcl_101  $cvcl_102 )) (or $cvcl_101  $cvcl_103 )) (or $cvcl_102  $cvcl_103 )) (or $cvcl_104  $cvcl_105 )) (or $cvcl_104  $cvcl_106 )) (or $cvcl_104  $cvcl_107 )) (or $cvcl_105  $cvcl_106 )) (or $cvcl_105  $cvcl_107 )) (or $cvcl_106  $cvcl_107 )) (or $cvcl_108  $cvcl_109 )) (or $cvcl_108  $cvcl_110 )) (or $cvcl_108  $cvcl_111 )) (or $cvcl_109  $cvcl_110 )) (or $cvcl_109  $cvcl_111 )) (or $cvcl_110  $cvcl_111 )) (or $cvcl_112  $cvcl_113 )) (or $cvcl_112  $cvcl_114 )) (or $cvcl_112  $cvcl_115 )) (or $cvcl_113  $cvcl_114 )) (or $cvcl_113  $cvcl_115 )) (or $cvcl_114  $cvcl_115 )) (or $cvcl_116  $cvcl_117 )) (or $cvcl_116  $cvcl_118 )) (or $cvcl_116  $cvcl_119 )) (or $cvcl_117  $cvcl_118 )) (or $cvcl_117  $cvcl_119 )) (or $cvcl_118  $cvcl_119 )) (or $cvcl_120  $cvcl_121 )) (or $cvcl_120  $cvcl_122 )) (or $cvcl_120  $cvcl_123 )) (or $cvcl_121  $cvcl_122 )) (or $cvcl_121  $cvcl_123 )) (or $cvcl_122  $cvcl_123 )) (or $cvcl_124  $cvcl_125 )) (or $cvcl_124  $cvcl_126 )) (or $cvcl_124  $cvcl_127 )) (or $cvcl_125  $cvcl_126 )) (or $cvcl_125  $cvcl_127 )) (or $cvcl_126  $cvcl_127 )) (or $cvcl_128  $cvcl_129 )) (or $cvcl_447  (not $cvcl_129) )) (or $cvcl_130  $cvcl_131 )) (or $cvcl_446  (not $cvcl_131) )) (or $cvcl_132  $cvcl_133 )) (or $cvcl_452  (not $cvcl_133) )) (or $cvcl_134  $cvcl_135 )) (or $cvcl_458  (not $cvcl_135) )) (or $cvcl_136  $cvcl_137 )) (or $cvcl_464  (not $cvcl_137) )) (or $cvcl_138  $cvcl_139 )) (or $cvcl_463  (not $cvcl_139) )) (or $cvcl_140  $cvcl_141 )) (or $cvcl_467  (not $cvcl_141) )) (or $cvcl_142  $cvcl_143 )) (or $cvcl_471  (not $cvcl_143) )) (or $cvcl_144  $cvcl_145 )) (or $cvcl_476  (not $cvcl_145) )) (or $cvcl_146  $cvcl_147 )) (or $cvcl_475  (not $cvcl_147) )) (or $cvcl_148  $cvcl_149 )) (or $cvcl_479  (not $cvcl_149) )) (or $cvcl_150  $cvcl_151 )) (or $cvcl_483  (not $cvcl_151) )) (or $cvcl_152  $cvcl_153 )) (or $cvcl_488  (not $cvcl_153) )) (or $cvcl_154  $cvcl_155 )) (or $cvcl_487  (not $cvcl_155) )) (or $cvcl_156  $cvcl_157 )) (or $cvcl_491  (not $cvcl_157) )) (or $cvcl_158  $cvcl_159 )) (or $cvcl_495  (not $cvcl_159) )) (or $cvcl_160  $cvcl_161 )) (or $cvcl_500  (not $cvcl_161) )) (or $cvcl_162  $cvcl_163 )) (or $cvcl_499  (not $cvcl_163) )) (or $cvcl_164  $cvcl_165 )) (or $cvcl_503  (not $cvcl_165) )) (or $cvcl_166  $cvcl_167 )) (or $cvcl_507  (not $cvcl_167) )) (or $cvcl_168  $cvcl_169 )) (or $cvcl_512  (not $cvcl_169) )) (or $cvcl_170  $cvcl_171 )) (or $cvcl_511  (not $cvcl_171) )) (or $cvcl_172  $cvcl_173 )) (or $cvcl_515  (not $cvcl_173) )) (or $cvcl_174  $cvcl_175 )) (or $cvcl_519  (not $cvcl_175) )) (or $cvcl_176  $cvcl_177 )) (or $cvcl_524  (not $cvcl_177) )) (or $cvcl_178  $cvcl_179 )) (or $cvcl_523  (not $cvcl_179) )) (or $cvcl_180  $cvcl_181 )) (or $cvcl_527  (not $cvcl_181) )) (or $cvcl_182  $cvcl_183 )) (or $cvcl_531  (not $cvcl_183) )) (or $cvcl_184  $cvcl_185 )) (or $cvcl_536  (not $cvcl_185) )) (or $cvcl_186  $cvcl_187 )) (or $cvcl_535  (not $cvcl_187) )) (or $cvcl_188  $cvcl_189 )) (or $cvcl_539  (not $cvcl_189) )) (or $cvcl_190  $cvcl_191 )) (or $cvcl_543  (not $cvcl_191) )) (or $cvcl_1  $cvcl_194 )) (or $cvcl_5  $cvcl_200 )) (or $cvcl_9  $cvcl_206 )) (or $cvcl_13  (<= (- AT3_PROC1_X AT3_Z) 10) )) (or $cvcl_17  $cvcl_215 )) (or $cvcl_21  $cvcl_221 )) (or $cvcl_25  $cvcl_227 )) (or $cvcl_29  (<= (- AT3_PROC2_X AT3_Z) 10) )) (or $cvcl_33  $cvcl_233 )) (or $cvcl_37  $cvcl_239 )) (or $cvcl_41  $cvcl_245 )) (or $cvcl_45  (<= (- AT3_PROC3_X AT3_Z) 10) )) (or $cvcl_49  $cvcl_251 )) (or $cvcl_53  $cvcl_257 )) (or $cvcl_57  $cvcl_263 )) (or $cvcl_61  (<= (- AT3_PROC4_X AT3_Z) 10) )) (or $cvcl_65  $cvcl_269 )) (or $cvcl_69  $cvcl_275 )) (or $cvcl_73  $cvcl_281 )) (or $cvcl_77  (<= (- AT3_PROC5_X AT3_Z) 10) )) (or $cvcl_81  $cvcl_287 )) (or $cvcl_85  $cvcl_293 )) (or $cvcl_89  $cvcl_299 )) (or $cvcl_93  (<= (- AT3_PROC6_X AT3_Z) 10) )) (or $cvcl_97  $cvcl_305 )) (or $cvcl_101  $cvcl_311 )) (or $cvcl_105  $cvcl_317 )) (or $cvcl_109  (<= (- AT3_PROC7_X AT3_Z) 10) )) (or $cvcl_113  $cvcl_323 )) (or $cvcl_117  $cvcl_329 )) (or $cvcl_121  $cvcl_335 )) (or $cvcl_125  (<= (- AT3_PROC8_X AT3_Z) 10) )) (or (or (or (or (or (or AT0_PROC1_WAIT  AT0_DELTA )  AT0_PROC1_SW_A_B_TAU )  AT0_PROC1_SW_B_C_TAU )  AT0_PROC1_SW_C_B_TAU )  AT0_PROC1_SW_C_CS_TAU )  AT0_PROC1_SW_CS_A_TAU )) (or (or (or (or (or (or AT1_PROC1_WAIT  AT1_DELTA )  AT1_PROC1_SW_A_B_TAU )  AT1_PROC1_SW_B_C_TAU )  AT1_PROC1_SW_C_B_TAU )  AT1_PROC1_SW_C_CS_TAU )  AT1_PROC1_SW_CS_A_TAU )) (or (or (or (or (or (or AT2_PROC1_WAIT  AT2_DELTA )  AT2_PROC1_SW_A_B_TAU )  AT2_PROC1_SW_B_C_TAU )  AT2_PROC1_SW_C_B_TAU )  AT2_PROC1_SW_C_CS_TAU )  AT2_PROC1_SW_CS_A_TAU )) (or (or (or (or (or (or AT0_PROC2_WAIT  AT0_DELTA )  AT0_PROC2_SW_A_B_TAU )  AT0_PROC2_SW_B_C_TAU )  AT0_PROC2_SW_C_B_TAU )  AT0_PROC2_SW_C_CS_TAU )  AT0_PROC2_SW_CS_A_TAU )) (or (or (or (or (or (or AT1_PROC2_WAIT  AT1_DELTA )  AT1_PROC2_SW_A_B_TAU )  AT1_PROC2_SW_B_C_TAU )  AT1_PROC2_SW_C_B_TAU )  AT1_PROC2_SW_C_CS_TAU )  AT1_PROC2_SW_CS_A_TAU )) (or (or (or (or (or (or AT2_PROC2_WAIT  AT2_DELTA )  AT2_PROC2_SW_A_B_TAU )  AT2_PROC2_SW_B_C_TAU )  AT2_PROC2_SW_C_B_TAU )  AT2_PROC2_SW_C_CS_TAU )  AT2_PROC2_SW_CS_A_TAU )) (or (or (or (or (or (or AT0_PROC3_WAIT  AT0_DELTA )  AT0_PROC3_SW_A_B_TAU )  AT0_PROC3_SW_B_C_TAU )  AT0_PROC3_SW_C_B_TAU )  AT0_PROC3_SW_C_CS_TAU )  AT0_PROC3_SW_CS_A_TAU )) (or (or (or (or (or (or AT1_PROC3_WAIT  AT1_DELTA )  AT1_PROC3_SW_A_B_TAU )  AT1_PROC3_SW_B_C_TAU )  AT1_PROC3_SW_C_B_TAU )  AT1_PROC3_SW_C_CS_TAU )  AT1_PROC3_SW_CS_A_TAU )) (or (or (or (or (or (or AT2_PROC3_WAIT  AT2_DELTA )  AT2_PROC3_SW_A_B_TAU )  AT2_PROC3_SW_B_C_TAU )  AT2_PROC3_SW_C_B_TAU )  AT2_PROC3_SW_C_CS_TAU )  AT2_PROC3_SW_CS_A_TAU )) (or (or (or (or (or (or 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 AT1_PROC4_WAIT  AT1_DELTA )  AT1_PROC4_SW_A_B_TAU )  AT1_PROC4_SW_B_C_TAU )  AT1_PROC4_SW_C_B_TAU )  AT1_PROC4_SW_C_CS_TAU )  AT1_PROC4_SW_CS_A_TAU )) (or (or (or (or (or (or AT2_PROC4_WAIT  AT2_DELTA )  AT2_PROC4_SW_A_B_TAU )  AT2_PROC4_SW_B_C_TAU )  AT2_PROC4_SW_C_B_TAU )  AT2_PROC4_SW_C_CS_TAU )  AT2_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 AT1_PROC5_WAIT  AT1_DELTA )  AT1_PROC5_SW_A_B_TAU )  AT1_PROC5_SW_B_C_TAU )  AT1_PROC5_SW_C_B_TAU )  AT1_PROC5_SW_C_CS_TAU )  AT1_PROC5_SW_CS_A_TAU )) (or (or (or (or (or (or AT2_PROC5_WAIT  AT2_DELTA )  AT2_PROC5_SW_A_B_TAU )  AT2_PROC5_SW_B_C_TAU )  AT2_PROC5_SW_C_B_TAU )  AT2_PROC5_SW_C_CS_TAU )  AT2_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 AT1_PROC6_WAIT  AT1_DELTA )  AT1_PROC6_SW_A_B_TAU )  AT1_PROC6_SW_B_C_TAU )  AT1_PROC6_SW_C_B_TAU )  AT1_PROC6_SW_C_CS_TAU )  AT1_PROC6_SW_CS_A_TAU )) (or (or (or (or (or (or AT2_PROC6_WAIT  AT2_DELTA )  AT2_PROC6_SW_A_B_TAU )  AT2_PROC6_SW_B_C_TAU )  AT2_PROC6_SW_C_B_TAU )  AT2_PROC6_SW_C_CS_TAU )  AT2_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 AT1_PROC7_WAIT  AT1_DELTA )  AT1_PROC7_SW_A_B_TAU )  AT1_PROC7_SW_B_C_TAU )  AT1_PROC7_SW_C_B_TAU )  AT1_PROC7_SW_C_CS_TAU )  AT1_PROC7_SW_CS_A_TAU )) (or (or (or (or (or (or AT2_PROC7_WAIT  AT2_DELTA )  AT2_PROC7_SW_A_B_TAU )  AT2_PROC7_SW_B_C_TAU )  AT2_PROC7_SW_C_B_TAU )  AT2_PROC7_SW_C_CS_TAU )  AT2_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 AT1_PROC8_WAIT  AT1_DELTA )  AT1_PROC8_SW_A_B_TAU )  AT1_PROC8_SW_B_C_TAU )  AT1_PROC8_SW_C_B_TAU )  AT1_PROC8_SW_C_CS_TAU )  AT1_PROC8_SW_CS_A_TAU )) (or (or (or (or (or (or AT2_PROC8_WAIT  AT2_DELTA )  AT2_PROC8_SW_A_B_TAU )  AT2_PROC8_SW_B_C_TAU )  AT2_PROC8_SW_C_B_TAU )  AT2_PROC8_SW_C_CS_TAU )  AT2_PROC8_SW_CS_A_TAU )) (or $cvcl_192  AT0_PROC1_A )) (or $cvcl_192  AT0_PROC1_TAU )) (or $cvcl_192  AT1_PROC1_B )) (or $cvcl_192  $cvcl_130 )) (or $cvcl_193  AT0_PROC1_B )) (or $cvcl_193  AT0_PROC1_TAU )) (or $cvcl_193  AT1_PROC1_C )) (or $cvcl_193  $cvcl_194 )) (or $cvcl_193  $cvcl_130 )) (or $cvcl_195  AT0_PROC1_C )) (or $cvcl_195  AT0_PROC1_TAU )) (or $cvcl_195  AT1_PROC1_B )) (or $cvcl_195  $cvcl_130 )) (or $cvcl_196  AT0_PROC1_C )) (or $cvcl_196  AT0_PROC1_TAU )) (or $cvcl_196  AT1_PROC1_CS )) (or $cvcl_196  (> (- AT0_PROC1_X AT0_Z) 10) )) (or $cvcl_196  $cvcl_340 )) (or $cvcl_197  AT0_PROC1_CS )) (or $cvcl_197  AT0_PROC1_TAU )) (or $cvcl_197  AT1_PROC1_A )) (or $cvcl_197  $cvcl_130 )) (or $cvcl_198  AT1_PROC1_A )) (or $cvcl_198  AT1_PROC1_TAU )) (or $cvcl_198  AT2_PROC1_B )) (or $cvcl_198  $cvcl_132 )) (or $cvcl_199  AT1_PROC1_B )) (or $cvcl_199  AT1_PROC1_TAU )) (or $cvcl_199  AT2_PROC1_C )) (or $cvcl_199  $cvcl_200 )) (or $cvcl_199  $cvcl_132 )) (or $cvcl_201  AT1_PROC1_C )) (or $cvcl_201  AT1_PROC1_TAU )) (or $cvcl_201  AT2_PROC1_B )) (or $cvcl_201  $cvcl_132 )) (or $cvcl_202  AT1_PROC1_C )) (or $cvcl_202  AT1_PROC1_TAU )) (or $cvcl_202  AT2_PROC1_CS )) (or $cvcl_202  (> (- AT1_PROC1_X AT1_Z) 10) )) (or $cvcl_202  $cvcl_342 )) (or $cvcl_203  AT1_PROC1_CS )) (or $cvcl_203  AT1_PROC1_TAU )) (or $cvcl_203  AT2_PROC1_A )) (or $cvcl_203  $cvcl_132 )) (or $cvcl_204  AT2_PROC1_A )) (or $cvcl_204  AT2_PROC1_TAU )) (or $cvcl_204  AT3_PROC1_B )) (or $cvcl_204  $cvcl_134 )) (or $cvcl_205  AT2_PROC1_B )) (or $cvcl_205  AT2_PROC1_TAU )) (or $cvcl_205  AT3_PROC1_C )) (or $cvcl_205  $cvcl_206 )) (or $cvcl_205  $cvcl_134 )) (or $cvcl_207  AT2_PROC1_C )) (or $cvcl_207  AT2_PROC1_TAU )) (or $cvcl_207  AT3_PROC1_B )) (or $cvcl_207  $cvcl_134 )) (or $cvcl_208  AT2_PROC1_C )) (or $cvcl_208  AT2_PROC1_TAU )) (or $cvcl_208  AT3_PROC1_CS )) (or $cvcl_208  (> (- AT2_PROC1_X AT2_Z) 10) )) (or $cvcl_208  $cvcl_344 )) (or $cvcl_209  AT2_PROC1_CS )) (or $cvcl_209  AT2_PROC1_TAU )) (or $cvcl_209  AT3_PROC1_A )) (or $cvcl_209  $cvcl_134 )) (or $cvcl_192  $cvcl_210 )) (or $cvcl_193  $cvcl_210 )) (or $cvcl_195  $cvcl_210 )) (or $cvcl_196  $cvcl_210 )) (or $cvcl_197  $cvcl_210 )) (or $cvcl_198  $cvcl_211 )) (or $cvcl_199  $cvcl_211 )) (or $cvcl_201  $cvcl_211 )) (or $cvcl_202  $cvcl_211 )) (or $cvcl_203  $cvcl_211 )) (or $cvcl_204  $cvcl_212 )) (or $cvcl_205  $cvcl_212 )) (or $cvcl_207  $cvcl_212 )) (or $cvcl_208  $cvcl_212 )) (or $cvcl_209  $cvcl_212 )) (or $cvcl_213  AT0_PROC2_A )) (or $cvcl_213  AT0_PROC2_TAU )) (or $cvcl_213  AT1_PROC2_B )) (or $cvcl_213  $cvcl_138 )) (or $cvcl_214  AT0_PROC2_B )) (or $cvcl_214  AT0_PROC2_TAU )) (or $cvcl_214  AT1_PROC2_C )) (or $cvcl_214  $cvcl_215 )) (or $cvcl_214  $cvcl_138 )) (or $cvcl_216  AT0_PROC2_C )) (or $cvcl_216  AT0_PROC2_TAU )) (or $cvcl_216  AT1_PROC2_B )) (or $cvcl_216  $cvcl_138 )) (or $cvcl_217  AT0_PROC2_C )) (or $cvcl_217  AT0_PROC2_TAU )) (or $cvcl_217  AT1_PROC2_CS )) (or $cvcl_217  (> (- AT0_PROC2_X AT0_Z) 10) )) (or $cvcl_217  $cvcl_346 )) (or $cvcl_218  AT0_PROC2_CS )) (or $cvcl_218  AT0_PROC2_TAU )) (or $cvcl_218  AT1_PROC2_A )) (or $cvcl_218  $cvcl_138 )) (or $cvcl_219  AT1_PROC2_A )) (or $cvcl_219  AT1_PROC2_TAU )) (or $cvcl_219  AT2_PROC2_B )) (or $cvcl_219  $cvcl_140 )) (or $cvcl_220  AT1_PROC2_B )) (or $cvcl_220  AT1_PROC2_TAU )) (or $cvcl_220  AT2_PROC2_C )) (or $cvcl_220  $cvcl_221 )) (or $cvcl_220  $cvcl_140 )) (or $cvcl_222  AT1_PROC2_C )) (or $cvcl_222  AT1_PROC2_TAU )) (or $cvcl_222  AT2_PROC2_B )) (or $cvcl_222  $cvcl_140 )) (or $cvcl_223  AT1_PROC2_C )) (or $cvcl_223  AT1_PROC2_TAU )) (or $cvcl_223  AT2_PROC2_CS )) (or $cvcl_223  (> (- AT1_PROC2_X AT1_Z) 10) )) (or $cvcl_223  $cvcl_348 )) (or $cvcl_224  AT1_PROC2_CS )) (or $cvcl_224  AT1_PROC2_TAU )) (or $cvcl_224  AT2_PROC2_A )) (or $cvcl_224  $cvcl_140 )) (or $cvcl_225  AT2_PROC2_A )) (or $cvcl_225  AT2_PROC2_TAU )) (or $cvcl_225  AT3_PROC2_B )) (or $cvcl_225  $cvcl_142 )) (or $cvcl_226  AT2_PROC2_B )) (or $cvcl_226  AT2_PROC2_TAU )) (or $cvcl_226  AT3_PROC2_C )) (or $cvcl_226  $cvcl_227 )) (or $cvcl_226  $cvcl_142 )) (or $cvcl_228  AT2_PROC2_C )) (or $cvcl_228  AT2_PROC2_TAU )) (or $cvcl_228  AT3_PROC2_B )) (or $cvcl_228  $cvcl_142 )) (or $cvcl_229  AT2_PROC2_C )) (or $cvcl_229  AT2_PROC2_TAU )) (or $cvcl_229  AT3_PROC2_CS )) (or $cvcl_229  (> (- AT2_PROC2_X AT2_Z) 10) )) (or $cvcl_229  $cvcl_350 )) (or $cvcl_230  AT2_PROC2_CS )) (or $cvcl_230  AT2_PROC2_TAU )) (or $cvcl_230  AT3_PROC2_A )) (or $cvcl_230  $cvcl_142 )) (or $cvcl_213  $cvcl_210 )) (or $cvcl_214  $cvcl_210 )) (or $cvcl_216  $cvcl_210 )) (or $cvcl_217  $cvcl_210 )) (or $cvcl_218  $cvcl_210 )) (or $cvcl_219  $cvcl_211 )) (or $cvcl_220  $cvcl_211 )) (or $cvcl_222  $cvcl_211 )) (or $cvcl_223  $cvcl_211 )) (or $cvcl_224  $cvcl_211 )) (or $cvcl_225  $cvcl_212 )) (or $cvcl_226  $cvcl_212 )) (or $cvcl_228  $cvcl_212 )) (or $cvcl_229  $cvcl_212 )) (or $cvcl_230  $cvcl_212 )) (or $cvcl_231  AT0_PROC3_A )) (or $cvcl_231  AT0_PROC3_TAU )) (or $cvcl_231  AT1_PROC3_B )) (or $cvcl_231  $cvcl_146 )) (or $cvcl_232  AT0_PROC3_B )) (or $cvcl_232  AT0_PROC3_TAU )) (or $cvcl_232  AT1_PROC3_C )) (or $cvcl_232  $cvcl_233 )) (or $cvcl_232  $cvcl_146 )) (or $cvcl_234  AT0_PROC3_C )) (or $cvcl_234  AT0_PROC3_TAU )) (or $cvcl_234  AT1_PROC3_B )) (or $cvcl_234  $cvcl_146 )) (or $cvcl_235  AT0_PROC3_C )) (or $cvcl_235  AT0_PROC3_TAU )) (or $cvcl_235  AT1_PROC3_CS )) (or $cvcl_235  (> (- AT0_PROC3_X AT0_Z) 10) )) (or $cvcl_235  $cvcl_352 )) (or $cvcl_236  AT0_PROC3_CS )) (or $cvcl_236  AT0_PROC3_TAU )) (or $cvcl_236  AT1_PROC3_A )) (or $cvcl_236  $cvcl_146 )) (or $cvcl_237  AT1_PROC3_A )) (or $cvcl_237  AT1_PROC3_TAU )) (or $cvcl_237  AT2_PROC3_B )) (or $cvcl_237  $cvcl_148 )) (or $cvcl_238  AT1_PROC3_B )) (or $cvcl_238  AT1_PROC3_TAU )) (or $cvcl_238  AT2_PROC3_C )) (or $cvcl_238  $cvcl_239 )) (or $cvcl_238  $cvcl_148 )) (or $cvcl_240  AT1_PROC3_C )) (or $cvcl_240  AT1_PROC3_TAU )) (or $cvcl_240  AT2_PROC3_B )) (or $cvcl_240  $cvcl_148 )) (or $cvcl_241  AT1_PROC3_C )) (or $cvcl_241  AT1_PROC3_TAU )) (or $cvcl_241  AT2_PROC3_CS )) (or $cvcl_241  (> (- AT1_PROC3_X AT1_Z) 10) )) (or $cvcl_241  $cvcl_354 )) (or $cvcl_242  AT1_PROC3_CS )) (or $cvcl_242  AT1_PROC3_TAU )) (or $cvcl_242  AT2_PROC3_A )) (or $cvcl_242  $cvcl_148 )) (or $cvcl_243  AT2_PROC3_A )) (or $cvcl_243  AT2_PROC3_TAU )) (or $cvcl_243  AT3_PROC3_B )) (or $cvcl_243  $cvcl_150 )) (or $cvcl_244  AT2_PROC3_B )) (or $cvcl_244  AT2_PROC3_TAU )) (or $cvcl_244  AT3_PROC3_C )) (or $cvcl_244  $cvcl_245 )) (or $cvcl_244  $cvcl_150 )) (or $cvcl_246  AT2_PROC3_C )) (or $cvcl_246  AT2_PROC3_TAU )) (or $cvcl_246  AT3_PROC3_B )) (or $cvcl_246  $cvcl_150 )) (or $cvcl_247  AT2_PROC3_C )) (or $cvcl_247  AT2_PROC3_TAU )) (or $cvcl_247  AT3_PROC3_CS )) (or $cvcl_247  (> (- AT2_PROC3_X AT2_Z) 10) )) (or $cvcl_247  $cvcl_356 )) (or $cvcl_248  AT2_PROC3_CS )) (or $cvcl_248  AT2_PROC3_TAU )) (or $cvcl_248  AT3_PROC3_A )) (or $cvcl_248  $cvcl_150 )) (or $cvcl_231  $cvcl_210 )) (or $cvcl_232  $cvcl_210 )) (or $cvcl_234  $cvcl_210 )) (or $cvcl_235  $cvcl_210 )) (or $cvcl_236  $cvcl_210 )) (or $cvcl_237  $cvcl_211 )) (or $cvcl_238  $cvcl_211 )) (or $cvcl_240  $cvcl_211 )) (or $cvcl_241  $cvcl_211 )) (or $cvcl_242  $cvcl_211 )) (or $cvcl_243  $cvcl_212 )) (or $cvcl_244  $cvcl_212 )) (or $cvcl_246  $cvcl_212 )) (or $cvcl_247  $cvcl_212 )) (or $cvcl_248  $cvcl_212 )) (or $cvcl_249  AT0_PROC4_A )) (or $cvcl_249  AT0_PROC4_TAU )) (or $cvcl_249  AT1_PROC4_B )) (or $cvcl_249  $cvcl_154 )) (or $cvcl_250  AT0_PROC4_B )) (or $cvcl_250  AT0_PROC4_TAU )) (or $cvcl_250  AT1_PROC4_C )) (or $cvcl_250  $cvcl_251 )) (or $cvcl_250  $cvcl_154 )) (or $cvcl_252  AT0_PROC4_C )) (or $cvcl_252  AT0_PROC4_TAU )) (or $cvcl_252  AT1_PROC4_B )) (or $cvcl_252  $cvcl_154 )) (or $cvcl_253  AT0_PROC4_C )) (or $cvcl_253  AT0_PROC4_TAU )) (or $cvcl_253  AT1_PROC4_CS )) (or $cvcl_253  (> (- AT0_PROC4_X AT0_Z) 10) )) (or $cvcl_253  $cvcl_358 )) (or $cvcl_254  AT0_PROC4_CS )) (or $cvcl_254  AT0_PROC4_TAU )) (or $cvcl_254  AT1_PROC4_A )) (or $cvcl_254  $cvcl_154 )) (or $cvcl_255  AT1_PROC4_A )) (or $cvcl_255  AT1_PROC4_TAU )) (or $cvcl_255  AT2_PROC4_B )) (or $cvcl_255  $cvcl_156 )) (or $cvcl_256  AT1_PROC4_B )) (or $cvcl_256  AT1_PROC4_TAU )) (or $cvcl_256  AT2_PROC4_C )) (or $cvcl_256  $cvcl_257 )) (or $cvcl_256  $cvcl_156 )) (or $cvcl_258  AT1_PROC4_C )) (or $cvcl_258  AT1_PROC4_TAU )) (or $cvcl_258  AT2_PROC4_B )) (or $cvcl_258  $cvcl_156 )) (or $cvcl_259  AT1_PROC4_C )) (or $cvcl_259  AT1_PROC4_TAU )) (or $cvcl_259  AT2_PROC4_CS )) (or $cvcl_259  (> (- AT1_PROC4_X AT1_Z) 10) )) (or $cvcl_259  $cvcl_360 )) (or $cvcl_260  AT1_PROC4_CS )) (or $cvcl_260  AT1_PROC4_TAU )) (or $cvcl_260  AT2_PROC4_A )) (or $cvcl_260  $cvcl_156 )) (or $cvcl_261  AT2_PROC4_A )) (or $cvcl_261  AT2_PROC4_TAU )) (or $cvcl_261  AT3_PROC4_B )) (or $cvcl_261  $cvcl_158 )) (or $cvcl_262  AT2_PROC4_B )) (or $cvcl_262  AT2_PROC4_TAU )) (or $cvcl_262  AT3_PROC4_C )) (or $cvcl_262  $cvcl_263 )) (or $cvcl_262  $cvcl_158 )) (or $cvcl_264  AT2_PROC4_C )) (or $cvcl_264  AT2_PROC4_TAU )) (or $cvcl_264  AT3_PROC4_B )) (or $cvcl_264  $cvcl_158 )) (or $cvcl_265  AT2_PROC4_C )) (or $cvcl_265  AT2_PROC4_TAU )) (or $cvcl_265  AT3_PROC4_CS )) (or $cvcl_265  (> (- AT2_PROC4_X AT2_Z) 10) )) (or $cvcl_265  $cvcl_362 )) (or $cvcl_266  AT2_PROC4_CS )) (or $cvcl_266  AT2_PROC4_TAU )) (or $cvcl_266  AT3_PROC4_A )) (or $cvcl_266  $cvcl_158 )) (or $cvcl_249  $cvcl_210 )) (or $cvcl_250  $cvcl_210 )) (or $cvcl_252  $cvcl_210 )) (or $cvcl_253  $cvcl_210 )) (or $cvcl_254  $cvcl_210 )) (or $cvcl_255  $cvcl_211 )) (or $cvcl_256  $cvcl_211 )) (or $cvcl_258  $cvcl_211 )) (or $cvcl_259  $cvcl_211 )) (or $cvcl_260  $cvcl_211 )) (or $cvcl_261  $cvcl_212 )) (or $cvcl_262  $cvcl_212 )) (or $cvcl_264  $cvcl_212 )) (or $cvcl_265  $cvcl_212 )) (or $cvcl_266  $cvcl_212 )) (or $cvcl_267  AT0_PROC5_A )) (or $cvcl_267  AT0_PROC5_TAU )) (or $cvcl_267  AT1_PROC5_B )) (or $cvcl_267  $cvcl_162 )) (or $cvcl_268  AT0_PROC5_B )) (or $cvcl_268  AT0_PROC5_TAU )) (or $cvcl_268  AT1_PROC5_C )) (or $cvcl_268  $cvcl_269 )) (or $cvcl_268  $cvcl_162 )) (or $cvcl_270  AT0_PROC5_C )) (or $cvcl_270  AT0_PROC5_TAU )) (or $cvcl_270  AT1_PROC5_B )) (or $cvcl_270  $cvcl_162 )) (or $cvcl_271  AT0_PROC5_C )) (or $cvcl_271  AT0_PROC5_TAU )) (or $cvcl_271  AT1_PROC5_CS )) (or $cvcl_271  (> (- AT0_PROC5_X AT0_Z) 10) )) (or $cvcl_271  $cvcl_364 )) (or $cvcl_272  AT0_PROC5_CS )) (or $cvcl_272  AT0_PROC5_TAU )) (or $cvcl_272  AT1_PROC5_A )) (or $cvcl_272  $cvcl_162 )) (or $cvcl_273  AT1_PROC5_A )) (or $cvcl_273  AT1_PROC5_TAU )) (or $cvcl_273  AT2_PROC5_B )) (or $cvcl_273  $cvcl_164 )) (or $cvcl_274  AT1_PROC5_B )) (or $cvcl_274  AT1_PROC5_TAU )) (or $cvcl_274  AT2_PROC5_C )) (or $cvcl_274  $cvcl_275 )) (or $cvcl_274  $cvcl_164 )) (or $cvcl_276  AT1_PROC5_C )) (or $cvcl_276  AT1_PROC5_TAU )) (or $cvcl_276  AT2_PROC5_B )) (or $cvcl_276  $cvcl_164 )) (or $cvcl_277  AT1_PROC5_C )) (or $cvcl_277  AT1_PROC5_TAU )) (or $cvcl_277  AT2_PROC5_CS )) (or $cvcl_277  (> (- AT1_PROC5_X AT1_Z) 10) )) (or $cvcl_277  $cvcl_366 )) (or $cvcl_278  AT1_PROC5_CS )) (or $cvcl_278  AT1_PROC5_TAU )) (or $cvcl_278  AT2_PROC5_A )) (or $cvcl_278  $cvcl_164 )) (or $cvcl_279  AT2_PROC5_A )) (or $cvcl_279  AT2_PROC5_TAU )) (or $cvcl_279  AT3_PROC5_B )) (or $cvcl_279  $cvcl_166 )) (or $cvcl_280  AT2_PROC5_B )) (or $cvcl_280  AT2_PROC5_TAU )) (or $cvcl_280  AT3_PROC5_C )) (or $cvcl_280  $cvcl_281 )) (or $cvcl_280  $cvcl_166 )) (or $cvcl_282  AT2_PROC5_C )) (or $cvcl_282  AT2_PROC5_TAU )) (or $cvcl_282  AT3_PROC5_B )) (or $cvcl_282  $cvcl_166 )) (or $cvcl_283  AT2_PROC5_C )) (or $cvcl_283  AT2_PROC5_TAU )) (or $cvcl_283  AT3_PROC5_CS )) (or $cvcl_283  (> (- AT2_PROC5_X AT2_Z) 10) )) (or $cvcl_283  $cvcl_368 )) (or $cvcl_284  AT2_PROC5_CS )) (or $cvcl_284  AT2_PROC5_TAU )) (or $cvcl_284  AT3_PROC5_A )) (or $cvcl_284  $cvcl_166 )) (or $cvcl_267  $cvcl_210 )) (or $cvcl_268  $cvcl_210 )) (or $cvcl_270  $cvcl_210 )) (or $cvcl_271  $cvcl_210 )) (or $cvcl_272  $cvcl_210 )) (or $cvcl_273  $cvcl_211 )) (or $cvcl_274  $cvcl_211 )) (or $cvcl_276  $cvcl_211 )) (or $cvcl_277  $cvcl_211 )) (or $cvcl_278  $cvcl_211 )) (or $cvcl_279  $cvcl_212 )) (or $cvcl_280  $cvcl_212 )) (or $cvcl_282  $cvcl_212 )) (or $cvcl_283  $cvcl_212 )) (or $cvcl_284  $cvcl_212 )) (or $cvcl_285  AT0_PROC6_A )) (or $cvcl_285  AT0_PROC6_TAU )) (or $cvcl_285  AT1_PROC6_B )) (or $cvcl_285  $cvcl_170 )) (or $cvcl_286  AT0_PROC6_B )) (or $cvcl_286  AT0_PROC6_TAU )) (or $cvcl_286  AT1_PROC6_C )) (or $cvcl_286  $cvcl_287 )) (or $cvcl_286  $cvcl_170 )) (or $cvcl_288  AT0_PROC6_C )) (or $cvcl_288  AT0_PROC6_TAU )) (or $cvcl_288  AT1_PROC6_B )) (or $cvcl_288  $cvcl_170 )) (or $cvcl_289  AT0_PROC6_C )) (or $cvcl_289  AT0_PROC6_TAU )) (or $cvcl_289  AT1_PROC6_CS )) (or $cvcl_289  (> (- AT0_PROC6_X AT0_Z) 10) )) (or $cvcl_289  $cvcl_370 )) (or $cvcl_290  AT0_PROC6_CS )) (or $cvcl_290  AT0_PROC6_TAU )) (or $cvcl_290  AT1_PROC6_A )) (or $cvcl_290  $cvcl_170 )) (or $cvcl_291  AT1_PROC6_A )) (or $cvcl_291  AT1_PROC6_TAU )) (or $cvcl_291  AT2_PROC6_B )) (or $cvcl_291  $cvcl_172 )) (or $cvcl_292  AT1_PROC6_B )) (or $cvcl_292  AT1_PROC6_TAU )) (or $cvcl_292  AT2_PROC6_C )) (or $cvcl_292  $cvcl_293 )) (or $cvcl_292  $cvcl_172 )) (or $cvcl_294  AT1_PROC6_C )) (or $cvcl_294  AT1_PROC6_TAU )) (or $cvcl_294  AT2_PROC6_B )) (or $cvcl_294  $cvcl_172 )) (or $cvcl_295  AT1_PROC6_C )) (or $cvcl_295  AT1_PROC6_TAU )) (or $cvcl_295  AT2_PROC6_CS )) (or $cvcl_295  (> (- AT1_PROC6_X AT1_Z) 10) )) (or $cvcl_295  $cvcl_372 )) (or $cvcl_296  AT1_PROC6_CS )) (or $cvcl_296  AT1_PROC6_TAU )) (or $cvcl_296  AT2_PROC6_A )) (or $cvcl_296  $cvcl_172 )) (or $cvcl_297  AT2_PROC6_A )) (or $cvcl_297  AT2_PROC6_TAU )) (or $cvcl_297  AT3_PROC6_B )) (or $cvcl_297  $cvcl_174 )) (or $cvcl_298  AT2_PROC6_B )) (or $cvcl_298  AT2_PROC6_TAU )) (or $cvcl_298  AT3_PROC6_C )) (or $cvcl_298  $cvcl_299 )) (or $cvcl_298  $cvcl_174 )) (or $cvcl_300  AT2_PROC6_C )) (or $cvcl_300  AT2_PROC6_TAU )) (or $cvcl_300  AT3_PROC6_B )) (or $cvcl_300  $cvcl_174 )) (or $cvcl_301  AT2_PROC6_C )) (or $cvcl_301  AT2_PROC6_TAU )) (or $cvcl_301  AT3_PROC6_CS )) (or $cvcl_301  (> (- AT2_PROC6_X AT2_Z) 10) )) (or $cvcl_301  $cvcl_374 )) (or $cvcl_302  AT2_PROC6_CS )) (or $cvcl_302  AT2_PROC6_TAU )) (or $cvcl_302  AT3_PROC6_A )) (or $cvcl_302  $cvcl_174 )) (or $cvcl_285  $cvcl_210 )) (or $cvcl_286  $cvcl_210 )) (or $cvcl_288  $cvcl_210 )) (or $cvcl_289  $cvcl_210 )) (or $cvcl_290  $cvcl_210 )) (or $cvcl_291  $cvcl_211 )) (or $cvcl_292  $cvcl_211 )) (or $cvcl_294  $cvcl_211 )) (or $cvcl_295  $cvcl_211 )) (or $cvcl_296  $cvcl_211 )) (or $cvcl_297  $cvcl_212 )) (or $cvcl_298  $cvcl_212 )) (or $cvcl_300  $cvcl_212 )) (or $cvcl_301  $cvcl_212 )) (or $cvcl_302  $cvcl_212 )) (or $cvcl_303  AT0_PROC7_A )) (or $cvcl_303  AT0_PROC7_TAU )) (or $cvcl_303  AT1_PROC7_B )) (or $cvcl_303  $cvcl_178 )) (or $cvcl_304  AT0_PROC7_B )) (or $cvcl_304  AT0_PROC7_TAU )) (or $cvcl_304  AT1_PROC7_C )) (or $cvcl_304  $cvcl_305 )) (or $cvcl_304  $cvcl_178 )) (or $cvcl_306  AT0_PROC7_C )) (or $cvcl_306  AT0_PROC7_TAU )) (or $cvcl_306  AT1_PROC7_B )) (or $cvcl_306  $cvcl_178 )) (or $cvcl_307  AT0_PROC7_C )) (or $cvcl_307  AT0_PROC7_TAU )) (or $cvcl_307  AT1_PROC7_CS )) (or $cvcl_307  (> (- AT0_PROC7_X AT0_Z) 10) )) (or $cvcl_307  $cvcl_376 )) (or $cvcl_308  AT0_PROC7_CS )) (or $cvcl_308  AT0_PROC7_TAU )) (or $cvcl_308  AT1_PROC7_A )) (or $cvcl_308  $cvcl_178 )) (or $cvcl_309  AT1_PROC7_A )) (or $cvcl_309  AT1_PROC7_TAU )) (or $cvcl_309  AT2_PROC7_B )) (or $cvcl_309  $cvcl_180 )) (or $cvcl_310  AT1_PROC7_B )) (or $cvcl_310  AT1_PROC7_TAU )) (or $cvcl_310  AT2_PROC7_C )) (or $cvcl_310  $cvcl_311 )) (or $cvcl_310  $cvcl_180 )) (or $cvcl_312  AT1_PROC7_C )) (or $cvcl_312  AT1_PROC7_TAU )) (or $cvcl_312  AT2_PROC7_B )) (or $cvcl_312  $cvcl_180 )) (or $cvcl_313  AT1_PROC7_C )) (or $cvcl_313  AT1_PROC7_TAU )) (or $cvcl_313  AT2_PROC7_CS )) (or $cvcl_313  (> (- AT1_PROC7_X AT1_Z) 10) )) (or $cvcl_313  $cvcl_378 )) (or $cvcl_314  AT1_PROC7_CS )) (or $cvcl_314  AT1_PROC7_TAU )) (or $cvcl_314  AT2_PROC7_A )) (or $cvcl_314  $cvcl_180 )) (or $cvcl_315  AT2_PROC7_A )) (or $cvcl_315  AT2_PROC7_TAU )) (or $cvcl_315  AT3_PROC7_B )) (or $cvcl_315  $cvcl_182 )) (or $cvcl_316  AT2_PROC7_B )) (or $cvcl_316  AT2_PROC7_TAU )) (or $cvcl_316  AT3_PROC7_C )) (or $cvcl_316  $cvcl_317 )) (or $cvcl_316  $cvcl_182 )) (or $cvcl_318  AT2_PROC7_C )) (or $cvcl_318  AT2_PROC7_TAU )) (or $cvcl_318  AT3_PROC7_B )) (or $cvcl_318  $cvcl_182 )) (or $cvcl_319  AT2_PROC7_C )) (or $cvcl_319  AT2_PROC7_TAU )) (or $cvcl_319  AT3_PROC7_CS )) (or $cvcl_319  (> (- AT2_PROC7_X AT2_Z) 10) )) (or $cvcl_319  $cvcl_380 )) (or $cvcl_320  AT2_PROC7_CS )) (or $cvcl_320  AT2_PROC7_TAU )) (or $cvcl_320  AT3_PROC7_A )) (or $cvcl_320  $cvcl_182 )) (or $cvcl_303  $cvcl_210 )) (or $cvcl_304  $cvcl_210 )) (or $cvcl_306  $cvcl_210 )) (or $cvcl_307  $cvcl_210 )) (or $cvcl_308  $cvcl_210 )) (or $cvcl_309  $cvcl_211 )) (or $cvcl_310  $cvcl_211 )) (or $cvcl_312  $cvcl_211 )) (or $cvcl_313  $cvcl_211 )) (or $cvcl_314  $cvcl_211 )) (or $cvcl_315  $cvcl_212 )) (or $cvcl_316  $cvcl_212 )) (or $cvcl_318  $cvcl_212 )) (or $cvcl_319  $cvcl_212 )) (or $cvcl_320  $cvcl_212 )) (or $cvcl_321  AT0_PROC8_A )) (or $cvcl_321  AT0_PROC8_TAU )) (or $cvcl_321  AT1_PROC8_B )) (or $cvcl_321  $cvcl_186 )) (or $cvcl_322  AT0_PROC8_B )) (or $cvcl_322  AT0_PROC8_TAU )) (or $cvcl_322  AT1_PROC8_C )) (or $cvcl_322  $cvcl_323 )) (or $cvcl_322  $cvcl_186 )) (or $cvcl_324  AT0_PROC8_C )) (or $cvcl_324  AT0_PROC8_TAU )) (or $cvcl_324  AT1_PROC8_B )) (or $cvcl_324  $cvcl_186 )) (or $cvcl_325  AT0_PROC8_C )) (or $cvcl_325  AT0_PROC8_TAU )) (or $cvcl_325  AT1_PROC8_CS )) (or $cvcl_325  (> (- AT0_PROC8_X AT0_Z) 10) )) (or $cvcl_325  $cvcl_382 )) (or $cvcl_326  AT0_PROC8_CS )) (or $cvcl_326  AT0_PROC8_TAU )) (or $cvcl_326  AT1_PROC8_A )) (or $cvcl_326  $cvcl_186 )) (or $cvcl_327  AT1_PROC8_A )) (or $cvcl_327  AT1_PROC8_TAU )) (or $cvcl_327  AT2_PROC8_B )) (or $cvcl_327  $cvcl_188 )) (or $cvcl_328  AT1_PROC8_B )) (or $cvcl_328  AT1_PROC8_TAU )) (or $cvcl_328  AT2_PROC8_C )) (or $cvcl_328  $cvcl_329 )) (or $cvcl_328  $cvcl_188 )) (or $cvcl_330  AT1_PROC8_C )) (or $cvcl_330  AT1_PROC8_TAU )) (or $cvcl_330  AT2_PROC8_B )) (or $cvcl_330  $cvcl_188 )) (or $cvcl_331  AT1_PROC8_C )) (or $cvcl_331  AT1_PROC8_TAU )) (or $cvcl_331  AT2_PROC8_CS )) (or $cvcl_331  (> (- AT1_PROC8_X AT1_Z) 10) )) (or $cvcl_331  $cvcl_384 )) (or $cvcl_332  AT1_PROC8_CS )) (or $cvcl_332  AT1_PROC8_TAU )) (or $cvcl_332  AT2_PROC8_A )) (or $cvcl_332  $cvcl_188 )) (or $cvcl_333  AT2_PROC8_A )) (or $cvcl_333  AT2_PROC8_TAU )) (or $cvcl_333  AT3_PROC8_B )) (or $cvcl_333  $cvcl_190 )) (or $cvcl_334  AT2_PROC8_B )) (or $cvcl_334  AT2_PROC8_TAU )) (or $cvcl_334  AT3_PROC8_C )) (or $cvcl_334  $cvcl_335 )) (or $cvcl_334  $cvcl_190 )) (or $cvcl_336  AT2_PROC8_C )) (or $cvcl_336  AT2_PROC8_TAU )) (or $cvcl_336  AT3_PROC8_B )) (or $cvcl_336  $cvcl_190 )) (or $cvcl_337  AT2_PROC8_C )) (or $cvcl_337  AT2_PROC8_TAU )) (or $cvcl_337  AT3_PROC8_CS )) (or $cvcl_337  (> (- AT2_PROC8_X AT2_Z) 10) )) (or $cvcl_337  $cvcl_386 )) (or $cvcl_338  AT2_PROC8_CS )) (or $cvcl_338  AT2_PROC8_TAU )) (or $cvcl_338  AT3_PROC8_A )) (or $cvcl_338  $cvcl_190 )) (or $cvcl_321  $cvcl_210 )) (or $cvcl_322  $cvcl_210 )) (or $cvcl_324  $cvcl_210 )) (or $cvcl_325  $cvcl_210 )) (or $cvcl_326  $cvcl_210 )) (or $cvcl_327  $cvcl_211 )) (or $cvcl_328  $cvcl_211 )) (or $cvcl_330  $cvcl_211 )) (or $cvcl_331  $cvcl_211 )) (or $cvcl_332  $cvcl_211 )) (or $cvcl_333  $cvcl_212 )) (or $cvcl_334  $cvcl_212 )) (or $cvcl_336  $cvcl_212 )) (or $cvcl_337  $cvcl_212 )) (or $cvcl_338  $cvcl_212 )) (or (or $cvcl_339  $cvcl_0 )  AT1_PROC1_A )) (or (or $cvcl_339  AT0_PROC1_A )  $cvcl_4 )) (or (or $cvcl_339  $cvcl_1 )  AT1_PROC1_B )) (or (or $cvcl_339  AT0_PROC1_B )  $cvcl_5 )) (or (or $cvcl_339  $cvcl_2 )  AT1_PROC1_C )) (or (or $cvcl_339  AT0_PROC1_C )  $cvcl_6 )) (or (or $cvcl_339  $cvcl_3 )  AT1_PROC1_CS )) (or (or $cvcl_339  AT0_PROC1_CS )  $cvcl_7 )) (or $cvcl_339  $cvcl_388 )) (or $cvcl_339  $cvcl_340 )) (or $cvcl_339  $cvcl_210 )) (or (or $cvcl_341  $cvcl_4 )  AT2_PROC1_A )) (or (or $cvcl_341  AT1_PROC1_A )  $cvcl_8 )) (or (or $cvcl_341  $cvcl_5 )  AT2_PROC1_B )) (or (or $cvcl_341  AT1_PROC1_B )  $cvcl_9 )) (or (or $cvcl_341  $cvcl_6 )  AT2_PROC1_C )) (or (or $cvcl_341  AT1_PROC1_C )  $cvcl_10 )) (or (or $cvcl_341  $cvcl_7 )  AT2_PROC1_CS )) (or (or $cvcl_341  AT1_PROC1_CS )  $cvcl_11 )) (or $cvcl_341  $cvcl_390 )) (or $cvcl_341  $cvcl_342 )) (or $cvcl_341  $cvcl_211 )) (or (or $cvcl_343  $cvcl_8 )  AT3_PROC1_A )) (or (or $cvcl_343  AT2_PROC1_A )  $cvcl_12 )) (or (or $cvcl_343  $cvcl_9 )  AT3_PROC1_B )) (or (or $cvcl_343  AT2_PROC1_B )  $cvcl_13 )) (or (or $cvcl_343  $cvcl_10 )  AT3_PROC1_C )) (or (or $cvcl_343  AT2_PROC1_C )  $cvcl_14 )) (or (or $cvcl_343  $cvcl_11 )  AT3_PROC1_CS )) (or (or $cvcl_343  AT2_PROC1_CS )  $cvcl_15 )) (or $cvcl_343  $cvcl_392 )) (or $cvcl_343  $cvcl_344 )) (or $cvcl_343  $cvcl_212 )) (or (or $cvcl_345  $cvcl_16 )  AT1_PROC2_A )) (or (or $cvcl_345  AT0_PROC2_A )  $cvcl_20 )) (or (or $cvcl_345  $cvcl_17 )  AT1_PROC2_B )) (or (or $cvcl_345  AT0_PROC2_B )  $cvcl_21 )) (or (or $cvcl_345  $cvcl_18 )  AT1_PROC2_C )) (or (or $cvcl_345  AT0_PROC2_C )  $cvcl_22 )) (or (or $cvcl_345  $cvcl_19 )  AT1_PROC2_CS )) (or (or $cvcl_345  AT0_PROC2_CS )  $cvcl_23 )) (or $cvcl_345  $cvcl_393 )) (or $cvcl_345  $cvcl_346 )) (or $cvcl_345  $cvcl_210 )) (or (or $cvcl_347  $cvcl_20 )  AT2_PROC2_A )) (or (or $cvcl_347  AT1_PROC2_A )  $cvcl_24 )) (or (or $cvcl_347  $cvcl_21 )  AT2_PROC2_B )) (or (or $cvcl_347  AT1_PROC2_B )  $cvcl_25 )) (or (or $cvcl_347  $cvcl_22 )  AT2_PROC2_C )) (or (or $cvcl_347  AT1_PROC2_C )  $cvcl_26 )) (or (or $cvcl_347  $cvcl_23 )  AT2_PROC2_CS )) (or (or $cvcl_347  AT1_PROC2_CS )  $cvcl_27 )) (or $cvcl_347  $cvcl_395 )) (or $cvcl_347  $cvcl_348 )) (or $cvcl_347  $cvcl_211 )) (or (or $cvcl_349  $cvcl_24 )  AT3_PROC2_A )) (or (or $cvcl_349  AT2_PROC2_A )  $cvcl_28 )) (or (or $cvcl_349  $cvcl_25 )  AT3_PROC2_B )) (or (or $cvcl_349  AT2_PROC2_B )  $cvcl_29 )) (or (or $cvcl_349  $cvcl_26 )  AT3_PROC2_C )) (or (or $cvcl_349  AT2_PROC2_C )  $cvcl_30 )) (or (or $cvcl_349  $cvcl_27 )  AT3_PROC2_CS )) (or (or $cvcl_349  AT2_PROC2_CS )  $cvcl_31 )) (or $cvcl_349  $cvcl_397 )) (or $cvcl_349  $cvcl_350 )) (or $cvcl_349  $cvcl_212 )) (or (or $cvcl_351  $cvcl_32 )  AT1_PROC3_A )) (or (or $cvcl_351  AT0_PROC3_A )  $cvcl_36 )) (or (or $cvcl_351  $cvcl_33 )  AT1_PROC3_B )) (or (or $cvcl_351  AT0_PROC3_B )  $cvcl_37 )) (or (or $cvcl_351  $cvcl_34 )  AT1_PROC3_C )) (or (or $cvcl_351  AT0_PROC3_C )  $cvcl_38 )) (or (or $cvcl_351  $cvcl_35 )  AT1_PROC3_CS )) (or (or $cvcl_351  AT0_PROC3_CS )  $cvcl_39 )) (or $cvcl_351  $cvcl_399 )) (or $cvcl_351  $cvcl_352 )) (or $cvcl_351  $cvcl_210 )) (or (or $cvcl_353  $cvcl_36 )  AT2_PROC3_A )) (or (or $cvcl_353  AT1_PROC3_A )  $cvcl_40 )) (or (or $cvcl_353  $cvcl_37 )  AT2_PROC3_B )) (or (or $cvcl_353  AT1_PROC3_B )  $cvcl_41 )) (or (or $cvcl_353  $cvcl_38 )  AT2_PROC3_C )) (or (or $cvcl_353  AT1_PROC3_C )  $cvcl_42 )) (or (or $cvcl_353  $cvcl_39 )  AT2_PROC3_CS )) (or (or $cvcl_353  AT1_PROC3_CS )  $cvcl_43 )) (or $cvcl_353  $cvcl_400 )) (or $cvcl_353  $cvcl_354 )) (or $cvcl_353  $cvcl_211 )) (or (or $cvcl_355  $cvcl_40 )  AT3_PROC3_A )) (or (or $cvcl_355  AT2_PROC3_A )  $cvcl_44 )) (or (or $cvcl_355  $cvcl_41 )  AT3_PROC3_B )) (or (or $cvcl_355  AT2_PROC3_B )  $cvcl_45 )) (or (or $cvcl_355  $cvcl_42 )  AT3_PROC3_C )) (or (or $cvcl_355  AT2_PROC3_C )  $cvcl_46 )) (or (or $cvcl_355  $cvcl_43 )  AT3_PROC3_CS )) (or (or $cvcl_355  AT2_PROC3_CS )  $cvcl_47 )) (or $cvcl_355  $cvcl_401 )) (or $cvcl_355  $cvcl_356 )) (or $cvcl_355  $cvcl_212 )) (or (or $cvcl_357  $cvcl_48 )  AT1_PROC4_A )) (or (or $cvcl_357  AT0_PROC4_A )  $cvcl_52 )) (or (or $cvcl_357  $cvcl_49 )  AT1_PROC4_B )) (or (or $cvcl_357  AT0_PROC4_B )  $cvcl_53 )) (or (or $cvcl_357  $cvcl_50 )  AT1_PROC4_C )) (or (or $cvcl_357  AT0_PROC4_C )  $cvcl_54 )) (or (or $cvcl_357  $cvcl_51 )  AT1_PROC4_CS )) (or (or $cvcl_357  AT0_PROC4_CS )  $cvcl_55 )) (or $cvcl_357  $cvcl_402 )) (or $cvcl_357  $cvcl_358 )) (or $cvcl_357  $cvcl_210 )) (or (or $cvcl_359  $cvcl_52 )  AT2_PROC4_A )) (or (or $cvcl_359  AT1_PROC4_A )  $cvcl_56 )) (or (or $cvcl_359  $cvcl_53 )  AT2_PROC4_B )) (or (or $cvcl_359  AT1_PROC4_B )  $cvcl_57 )) (or (or $cvcl_359  $cvcl_54 )  AT2_PROC4_C )) (or (or $cvcl_359  AT1_PROC4_C )  $cvcl_58 )) (or (or $cvcl_359  $cvcl_55 )  AT2_PROC4_CS )) (or (or $cvcl_359  AT1_PROC4_CS )  $cvcl_59 )) (or $cvcl_359  $cvcl_403 )) (or $cvcl_359  $cvcl_360 )) (or $cvcl_359  $cvcl_211 )) (or (or $cvcl_361  $cvcl_56 )  AT3_PROC4_A )) (or (or $cvcl_361  AT2_PROC4_A )  $cvcl_60 )) (or (or $cvcl_361  $cvcl_57 )  AT3_PROC4_B )) (or (or $cvcl_361  AT2_PROC4_B )  $cvcl_61 )) (or (or $cvcl_361  $cvcl_58 )  AT3_PROC4_C )) (or (or $cvcl_361  AT2_PROC4_C )  $cvcl_62 )) (or (or $cvcl_361  $cvcl_59 )  AT3_PROC4_CS )) (or (or $cvcl_361  AT2_PROC4_CS )  $cvcl_63 )) (or $cvcl_361  $cvcl_404 )) (or $cvcl_361  $cvcl_362 )) (or $cvcl_361  $cvcl_212 )) (or (or $cvcl_363  $cvcl_64 )  AT1_PROC5_A )) (or (or $cvcl_363  AT0_PROC5_A )  $cvcl_68 )) (or (or $cvcl_363  $cvcl_65 )  AT1_PROC5_B )) (or (or $cvcl_363  AT0_PROC5_B )  $cvcl_69 )) (or (or $cvcl_363  $cvcl_66 )  AT1_PROC5_C )) (or (or $cvcl_363  AT0_PROC5_C )  $cvcl_70 )) (or (or $cvcl_363  $cvcl_67 )  AT1_PROC5_CS )) (or (or $cvcl_363  AT0_PROC5_CS )  $cvcl_71 )) (or $cvcl_363  $cvcl_405 )) (or $cvcl_363  $cvcl_364 )) (or $cvcl_363  $cvcl_210 )) (or (or $cvcl_365  $cvcl_68 )  AT2_PROC5_A )) (or (or $cvcl_365  AT1_PROC5_A )  $cvcl_72 )) (or (or $cvcl_365  $cvcl_69 )  AT2_PROC5_B )) (or (or $cvcl_365  AT1_PROC5_B )  $cvcl_73 )) (or (or $cvcl_365  $cvcl_70 )  AT2_PROC5_C )) (or (or $cvcl_365  AT1_PROC5_C )  $cvcl_74 )) (or (or $cvcl_365  $cvcl_71 )  AT2_PROC5_CS )) (or (or $cvcl_365  AT1_PROC5_CS )  $cvcl_75 )) (or $cvcl_365  $cvcl_406 )) (or $cvcl_365  $cvcl_366 )) (or $cvcl_365  $cvcl_211 )) (or (or $cvcl_367  $cvcl_72 )  AT3_PROC5_A )) (or (or $cvcl_367  AT2_PROC5_A )  $cvcl_76 )) (or (or $cvcl_367  $cvcl_73 )  AT3_PROC5_B )) (or (or $cvcl_367  AT2_PROC5_B )  $cvcl_77 )) (or (or $cvcl_367  $cvcl_74 )  AT3_PROC5_C )) (or (or $cvcl_367  AT2_PROC5_C )  $cvcl_78 )) (or (or $cvcl_367  $cvcl_75 )  AT3_PROC5_CS )) (or (or $cvcl_367  AT2_PROC5_CS )  $cvcl_79 )) (or $cvcl_367  $cvcl_407 )) (or $cvcl_367  $cvcl_368 )) (or $cvcl_367  $cvcl_212 )) (or (or $cvcl_369  $cvcl_80 )  AT1_PROC6_A )) (or (or $cvcl_369  AT0_PROC6_A )  $cvcl_84 )) (or (or $cvcl_369  $cvcl_81 )  AT1_PROC6_B )) (or (or $cvcl_369  AT0_PROC6_B )  $cvcl_85 )) (or (or $cvcl_369  $cvcl_82 )  AT1_PROC6_C )) (or (or $cvcl_369  AT0_PROC6_C )  $cvcl_86 )) (or (or $cvcl_369  $cvcl_83 )  AT1_PROC6_CS )) (or (or $cvcl_369  AT0_PROC6_CS )  $cvcl_87 )) (or $cvcl_369  $cvcl_408 )) (or $cvcl_369  $cvcl_370 )) (or $cvcl_369  $cvcl_210 )) (or (or $cvcl_371  $cvcl_84 )  AT2_PROC6_A )) (or (or $cvcl_371  AT1_PROC6_A )  $cvcl_88 )) (or (or $cvcl_371  $cvcl_85 )  AT2_PROC6_B )) (or (or $cvcl_371  AT1_PROC6_B )  $cvcl_89 )) (or (or $cvcl_371  $cvcl_86 )  AT2_PROC6_C )) (or (or $cvcl_371  AT1_PROC6_C )  $cvcl_90 )) (or (or $cvcl_371  $cvcl_87 )  AT2_PROC6_CS )) (or (or $cvcl_371  AT1_PROC6_CS )  $cvcl_91 )) (or $cvcl_371  $cvcl_409 )) (or $cvcl_371  $cvcl_372 )) (or $cvcl_371  $cvcl_211 )) (or (or $cvcl_373  $cvcl_88 )  AT3_PROC6_A )) (or (or $cvcl_373  AT2_PROC6_A )  $cvcl_92 )) (or (or $cvcl_373  $cvcl_89 )  AT3_PROC6_B )) (or (or $cvcl_373  AT2_PROC6_B )  $cvcl_93 )) (or (or $cvcl_373  $cvcl_90 )  AT3_PROC6_C )) (or (or $cvcl_373  AT2_PROC6_C )  $cvcl_94 )) (or (or $cvcl_373  $cvcl_91 )  AT3_PROC6_CS )) (or (or $cvcl_373  AT2_PROC6_CS )  $cvcl_95 )) (or $cvcl_373  $cvcl_410 )) (or $cvcl_373  $cvcl_374 )) (or $cvcl_373  $cvcl_212 )) (or (or $cvcl_375  $cvcl_96 )  AT1_PROC7_A )) (or (or $cvcl_375  AT0_PROC7_A )  $cvcl_100 )) (or (or $cvcl_375  $cvcl_97 )  AT1_PROC7_B )) (or (or $cvcl_375  AT0_PROC7_B )  $cvcl_101 )) (or (or $cvcl_375  $cvcl_98 )  AT1_PROC7_C )) (or (or $cvcl_375  AT0_PROC7_C )  $cvcl_102 )) (or (or $cvcl_375  $cvcl_99 )  AT1_PROC7_CS )) (or (or $cvcl_375  AT0_PROC7_CS )  $cvcl_103 )) (or $cvcl_375  $cvcl_411 )) (or $cvcl_375  $cvcl_376 )) (or $cvcl_375  $cvcl_210 )) (or (or $cvcl_377  $cvcl_100 )  AT2_PROC7_A )) (or (or $cvcl_377  AT1_PROC7_A )  $cvcl_104 )) (or (or $cvcl_377  $cvcl_101 )  AT2_PROC7_B )) (or (or $cvcl_377  AT1_PROC7_B )  $cvcl_105 )) (or (or $cvcl_377  $cvcl_102 )  AT2_PROC7_C )) (or (or $cvcl_377  AT1_PROC7_C )  $cvcl_106 )) (or (or $cvcl_377  $cvcl_103 )  AT2_PROC7_CS )) (or (or $cvcl_377  AT1_PROC7_CS )  $cvcl_107 )) (or $cvcl_377  $cvcl_412 )) (or $cvcl_377  $cvcl_378 )) (or $cvcl_377  $cvcl_211 )) (or (or $cvcl_379  $cvcl_104 )  AT3_PROC7_A )) (or (or $cvcl_379  AT2_PROC7_A )  $cvcl_108 )) (or (or $cvcl_379  $cvcl_105 )  AT3_PROC7_B )) (or (or $cvcl_379  AT2_PROC7_B )  $cvcl_109 )) (or (or $cvcl_379  $cvcl_106 )  AT3_PROC7_C )) (or (or $cvcl_379  AT2_PROC7_C )  $cvcl_110 )) (or (or $cvcl_379  $cvcl_107 )  AT3_PROC7_CS )) (or (or $cvcl_379  AT2_PROC7_CS )  $cvcl_111 )) (or $cvcl_379  $cvcl_413 )) (or $cvcl_379  $cvcl_380 )) (or $cvcl_379  $cvcl_212 )) (or (or $cvcl_381  $cvcl_112 )  AT1_PROC8_A )) (or (or $cvcl_381  AT0_PROC8_A )  $cvcl_116 )) (or (or $cvcl_381  $cvcl_113 )  AT1_PROC8_B )) (or (or $cvcl_381  AT0_PROC8_B )  $cvcl_117 )) (or (or $cvcl_381  $cvcl_114 )  AT1_PROC8_C )) (or (or $cvcl_381  AT0_PROC8_C )  $cvcl_118 )) (or (or $cvcl_381  $cvcl_115 )  AT1_PROC8_CS )) (or (or $cvcl_381  AT0_PROC8_CS )  $cvcl_119 )) (or $cvcl_381  $cvcl_414 )) (or $cvcl_381  $cvcl_382 )) (or $cvcl_381  $cvcl_210 )) (or (or $cvcl_383  $cvcl_116 )  AT2_PROC8_A )) (or (or $cvcl_383  AT1_PROC8_A )  $cvcl_120 )) (or (or $cvcl_383  $cvcl_117 )  AT2_PROC8_B )) (or (or $cvcl_383  AT1_PROC8_B )  $cvcl_121 )) (or (or $cvcl_383  $cvcl_118 )  AT2_PROC8_C )) (or (or $cvcl_383  AT1_PROC8_C )  $cvcl_122 )) (or (or $cvcl_383  $cvcl_119 )  AT2_PROC8_CS )) (or (or $cvcl_383  AT1_PROC8_CS )  $cvcl_123 )) (or $cvcl_383  $cvcl_415 )) (or $cvcl_383  $cvcl_384 )) (or $cvcl_383  $cvcl_211 )) (or (or $cvcl_385  $cvcl_120 )  AT3_PROC8_A )) (or (or $cvcl_385  AT2_PROC8_A )  $cvcl_124 )) (or (or $cvcl_385  $cvcl_121 )  AT3_PROC8_B )) (or (or $cvcl_385  AT2_PROC8_B )  $cvcl_125 )) (or (or $cvcl_385  $cvcl_122 )  AT3_PROC8_C )) (or (or $cvcl_385  AT2_PROC8_C )  $cvcl_126 )) (or (or $cvcl_385  $cvcl_123 )  AT3_PROC8_CS )) (or (or $cvcl_385  AT2_PROC8_CS )  $cvcl_127 )) (or $cvcl_385  $cvcl_416 )) (or $cvcl_385  $cvcl_386 )) (or $cvcl_385  $cvcl_212 )) (or (or $cvcl_387  $cvcl_0 )  AT1_PROC1_A )) (or (or $cvcl_387  AT0_PROC1_A )  $cvcl_4 )) (or (or $cvcl_387  $cvcl_1 )  AT1_PROC1_B )) (or (or $cvcl_387  AT0_PROC1_B )  $cvcl_5 )) (or (or $cvcl_387  $cvcl_2 )  AT1_PROC1_C )) (or (or $cvcl_387  AT0_PROC1_C )  $cvcl_6 )) (or (or $cvcl_387  $cvcl_3 )  AT1_PROC1_CS )) (or (or $cvcl_387  AT0_PROC1_CS )  $cvcl_7 )) (or $cvcl_387  $cvcl_340 )) (or $cvcl_387  $cvcl_388 )) $cvcl_394) (or (or $cvcl_389  $cvcl_4 )  AT2_PROC1_A )) (or (or $cvcl_389  AT1_PROC1_A )  $cvcl_8 )) (or (or $cvcl_389  $cvcl_5 )  AT2_PROC1_B )) (or (or $cvcl_389  AT1_PROC1_B )  $cvcl_9 )) (or (or $cvcl_389  $cvcl_6 )  AT2_PROC1_C )) (or (or $cvcl_389  AT1_PROC1_C )  $cvcl_10 )) (or (or $cvcl_389  $cvcl_7 )  AT2_PROC1_CS )) (or (or $cvcl_389  AT1_PROC1_CS )  $cvcl_11 )) (or $cvcl_389  $cvcl_342 )) (or $cvcl_389  $cvcl_390 )) $cvcl_396) (or (or $cvcl_391  $cvcl_8 )  AT3_PROC1_A )) (or (or $cvcl_391  AT2_PROC1_A )  $cvcl_12 )) (or (or $cvcl_391  $cvcl_9 )  AT3_PROC1_B )) (or (or $cvcl_391  AT2_PROC1_B )  $cvcl_13 )) (or (or $cvcl_391  $cvcl_10 )  AT3_PROC1_C )) (or (or $cvcl_391  AT2_PROC1_C )  $cvcl_14 )) (or (or $cvcl_391  $cvcl_11 )  AT3_PROC1_CS )) (or (or $cvcl_391  AT2_PROC1_CS )  $cvcl_15 )) (or $cvcl_391  $cvcl_344 )) (or $cvcl_391  $cvcl_392 )) $cvcl_398) (or (or $cvcl_387  $cvcl_16 )  AT1_PROC2_A )) (or (or $cvcl_387  AT0_PROC2_A )  $cvcl_20 )) (or (or $cvcl_387  $cvcl_17 )  AT1_PROC2_B )) (or (or $cvcl_387  AT0_PROC2_B )  $cvcl_21 )) (or (or $cvcl_387  $cvcl_18 )  AT1_PROC2_C )) (or (or $cvcl_387  AT0_PROC2_C )  $cvcl_22 )) (or (or $cvcl_387  $cvcl_19 )  AT1_PROC2_CS )) (or (or $cvcl_387  AT0_PROC2_CS )  $cvcl_23 )) (or $cvcl_387  $cvcl_346 )) (or $cvcl_387  $cvcl_393 )) $cvcl_394) (or (or $cvcl_389  $cvcl_20 )  AT2_PROC2_A )) (or (or $cvcl_389  AT1_PROC2_A )  $cvcl_24 )) (or (or $cvcl_389  $cvcl_21 )  AT2_PROC2_B )) (or (or $cvcl_389  AT1_PROC2_B )  $cvcl_25 )) (or (or $cvcl_389  $cvcl_22 )  AT2_PROC2_C )) (or (or $cvcl_389  AT1_PROC2_C )  $cvcl_26 )) (or (or $cvcl_389  $cvcl_23 )  AT2_PROC2_CS )) (or (or $cvcl_389  AT1_PROC2_CS )  $cvcl_27 )) (or $cvcl_389  $cvcl_348 )) (or $cvcl_389  $cvcl_395 )) $cvcl_396) (or (or $cvcl_391  $cvcl_24 )  AT3_PROC2_A )) (or (or $cvcl_391  AT2_PROC2_A )  $cvcl_28 )) (or (or $cvcl_391  $cvcl_25 )  AT3_PROC2_B )) (or (or $cvcl_391  AT2_PROC2_B )  $cvcl_29 )) (or (or $cvcl_391  $cvcl_26 )  AT3_PROC2_C )) (or (or $cvcl_391  AT2_PROC2_C )  $cvcl_30 )) (or (or $cvcl_391  $cvcl_27 )  AT3_PROC2_CS )) (or (or $cvcl_391  AT2_PROC2_CS )  $cvcl_31 )) (or $cvcl_391  $cvcl_350 )) (or $cvcl_391  $cvcl_397 )) $cvcl_398) (or (or $cvcl_387  $cvcl_32 )  AT1_PROC3_A )) (or (or $cvcl_387  AT0_PROC3_A )  $cvcl_36 )) (or (or $cvcl_387  $cvcl_33 )  AT1_PROC3_B )) (or (or $cvcl_387  AT0_PROC3_B )  $cvcl_37 )) (or (or $cvcl_387  $cvcl_34 )  AT1_PROC3_C )) (or (or $cvcl_387  AT0_PROC3_C )  $cvcl_38 )) (or (or $cvcl_387  $cvcl_35 )  AT1_PROC3_CS )) (or (or $cvcl_387  AT0_PROC3_CS )  $cvcl_39 )) (or $cvcl_387  $cvcl_352 )) (or $cvcl_387  $cvcl_399 )) $cvcl_394) (or (or $cvcl_389  $cvcl_36 )  AT2_PROC3_A )) (or (or $cvcl_389  AT1_PROC3_A )  $cvcl_40 )) (or (or $cvcl_389  $cvcl_37 )  AT2_PROC3_B )) (or (or $cvcl_389  AT1_PROC3_B )  $cvcl_41 )) (or (or $cvcl_389  $cvcl_38 )  AT2_PROC3_C )) (or (or $cvcl_389  AT1_PROC3_C )  $cvcl_42 )) (or (or $cvcl_389  $cvcl_39 )  AT2_PROC3_CS )) (or (or $cvcl_389  AT1_PROC3_CS )  $cvcl_43 )) (or $cvcl_389  $cvcl_354 )) (or $cvcl_389  $cvcl_400 )) $cvcl_396) (or (or $cvcl_391  $cvcl_40 )  AT3_PROC3_A )) (or (or $cvcl_391  AT2_PROC3_A )  $cvcl_44 )) (or (or $cvcl_391  $cvcl_41 )  AT3_PROC3_B )) (or (or $cvcl_391  AT2_PROC3_B )  $cvcl_45 )) (or (or $cvcl_391  $cvcl_42 )  AT3_PROC3_C )) (or (or $cvcl_391  AT2_PROC3_C )  $cvcl_46 )) (or (or $cvcl_391  $cvcl_43 )  AT3_PROC3_CS )) (or (or $cvcl_391  AT2_PROC3_CS )  $cvcl_47 )) (or $cvcl_391  $cvcl_356 )) (or $cvcl_391  $cvcl_401 )) $cvcl_398) (or (or $cvcl_387  $cvcl_48 )  AT1_PROC4_A )) (or (or $cvcl_387  AT0_PROC4_A )  $cvcl_52 )) (or (or $cvcl_387  $cvcl_49 )  AT1_PROC4_B )) (or (or $cvcl_387  AT0_PROC4_B )  $cvcl_53 )) (or (or $cvcl_387  $cvcl_50 )  AT1_PROC4_C )) (or (or $cvcl_387  AT0_PROC4_C )  $cvcl_54 )) (or (or $cvcl_387  $cvcl_51 )  AT1_PROC4_CS )) (or (or $cvcl_387  AT0_PROC4_CS )  $cvcl_55 )) (or $cvcl_387  $cvcl_358 )) (or $cvcl_387  $cvcl_402 )) $cvcl_394) (or (or $cvcl_389  $cvcl_52 )  AT2_PROC4_A )) (or (or $cvcl_389  AT1_PROC4_A )  $cvcl_56 )) (or (or $cvcl_389  $cvcl_53 )  AT2_PROC4_B )) (or (or $cvcl_389  AT1_PROC4_B )  $cvcl_57 )) (or (or $cvcl_389  $cvcl_54 )  AT2_PROC4_C )) (or (or $cvcl_389  AT1_PROC4_C )  $cvcl_58 )) (or (or $cvcl_389  $cvcl_55 )  AT2_PROC4_CS )) (or (or $cvcl_389  AT1_PROC4_CS )  $cvcl_59 )) (or $cvcl_389  $cvcl_360 )) (or $cvcl_389  $cvcl_403 )) $cvcl_396) (or (or $cvcl_391  $cvcl_56 )  AT3_PROC4_A )) (or (or $cvcl_391  AT2_PROC4_A )  $cvcl_60 )) (or (or $cvcl_391  $cvcl_57 )  AT3_PROC4_B )) (or (or $cvcl_391  AT2_PROC4_B )  $cvcl_61 )) (or (or $cvcl_391  $cvcl_58 )  AT3_PROC4_C )) (or (or $cvcl_391  AT2_PROC4_C )  $cvcl_62 )) (or (or $cvcl_391  $cvcl_59 )  AT3_PROC4_CS )) (or (or $cvcl_391  AT2_PROC4_CS )  $cvcl_63 )) (or $cvcl_391  $cvcl_362 )) (or $cvcl_391  $cvcl_404 )) $cvcl_398) (or (or $cvcl_387  $cvcl_64 )  AT1_PROC5_A )) (or (or $cvcl_387  AT0_PROC5_A )  $cvcl_68 )) (or (or $cvcl_387  $cvcl_65 )  AT1_PROC5_B )) (or (or $cvcl_387  AT0_PROC5_B )  $cvcl_69 )) (or (or $cvcl_387  $cvcl_66 )  AT1_PROC5_C )) (or (or $cvcl_387  AT0_PROC5_C )  $cvcl_70 )) (or (or $cvcl_387  $cvcl_67 )  AT1_PROC5_CS )) (or (or $cvcl_387  AT0_PROC5_CS )  $cvcl_71 )) (or $cvcl_387  $cvcl_364 )) (or $cvcl_387  $cvcl_405 )) $cvcl_394) (or (or $cvcl_389  $cvcl_68 )  AT2_PROC5_A )) (or (or $cvcl_389  AT1_PROC5_A )  $cvcl_72 )) (or (or $cvcl_389  $cvcl_69 )  AT2_PROC5_B )) (or (or $cvcl_389  AT1_PROC5_B )  $cvcl_73 )) (or (or $cvcl_389  $cvcl_70 )  AT2_PROC5_C )) (or (or $cvcl_389  AT1_PROC5_C )  $cvcl_74 )) (or (or $cvcl_389  $cvcl_71 )  AT2_PROC5_CS )) (or (or $cvcl_389  AT1_PROC5_CS )  $cvcl_75 )) (or $cvcl_389  $cvcl_366 )) (or $cvcl_389  $cvcl_406 )) $cvcl_396) (or (or $cvcl_391  $cvcl_72 )  AT3_PROC5_A )) (or (or $cvcl_391  AT2_PROC5_A )  $cvcl_76 )) (or (or $cvcl_391  $cvcl_73 )  AT3_PROC5_B )) (or (or $cvcl_391  AT2_PROC5_B )  $cvcl_77 )) (or (or $cvcl_391  $cvcl_74 )  AT3_PROC5_C )) (or (or $cvcl_391  AT2_PROC5_C )  $cvcl_78 )) (or (or $cvcl_391  $cvcl_75 )  AT3_PROC5_CS )) (or (or $cvcl_391  AT2_PROC5_CS )  $cvcl_79 )) (or $cvcl_391  $cvcl_368 )) (or $cvcl_391  $cvcl_407 )) $cvcl_398) (or (or $cvcl_387  $cvcl_80 )  AT1_PROC6_A )) (or (or $cvcl_387  AT0_PROC6_A )  $cvcl_84 )) (or (or $cvcl_387  $cvcl_81 )  AT1_PROC6_B )) (or (or $cvcl_387  AT0_PROC6_B )  $cvcl_85 )) (or (or $cvcl_387  $cvcl_82 )  AT1_PROC6_C )) (or (or $cvcl_387  AT0_PROC6_C )  $cvcl_86 )) (or (or $cvcl_387  $cvcl_83 )  AT1_PROC6_CS )) (or (or $cvcl_387  AT0_PROC6_CS )  $cvcl_87 )) (or $cvcl_387  $cvcl_370 )) (or $cvcl_387  $cvcl_408 )) $cvcl_394) (or (or $cvcl_389  $cvcl_84 )  AT2_PROC6_A )) (or (or $cvcl_389  AT1_PROC6_A )  $cvcl_88 )) (or (or $cvcl_389  $cvcl_85 )  AT2_PROC6_B )) (or (or $cvcl_389  AT1_PROC6_B )  $cvcl_89 )) (or (or $cvcl_389  $cvcl_86 )  AT2_PROC6_C )) (or (or $cvcl_389  AT1_PROC6_C )  $cvcl_90 )) (or (or $cvcl_389  $cvcl_87 )  AT2_PROC6_CS )) (or (or $cvcl_389  AT1_PROC6_CS )  $cvcl_91 )) (or $cvcl_389  $cvcl_372 )) (or $cvcl_389  $cvcl_409 )) $cvcl_396) (or (or $cvcl_391  $cvcl_88 )  AT3_PROC6_A )) (or (or $cvcl_391  AT2_PROC6_A )  $cvcl_92 )) (or (or $cvcl_391  $cvcl_89 )  AT3_PROC6_B )) (or (or $cvcl_391  AT2_PROC6_B )  $cvcl_93 )) (or (or $cvcl_391  $cvcl_90 )  AT3_PROC6_C )) (or (or $cvcl_391  AT2_PROC6_C )  $cvcl_94 )) (or (or $cvcl_391  $cvcl_91 )  AT3_PROC6_CS )) (or (or $cvcl_391  AT2_PROC6_CS )  $cvcl_95 )) (or $cvcl_391  $cvcl_374 )) (or $cvcl_391  $cvcl_410 )) $cvcl_398) (or (or $cvcl_387  $cvcl_96 )  AT1_PROC7_A )) (or (or $cvcl_387  AT0_PROC7_A )  $cvcl_100 )) (or (or $cvcl_387  $cvcl_97 )  AT1_PROC7_B )) (or (or $cvcl_387  AT0_PROC7_B )  $cvcl_101 )) (or (or $cvcl_387  $cvcl_98 )  AT1_PROC7_C )) (or (or $cvcl_387  AT0_PROC7_C )  $cvcl_102 )) (or (or $cvcl_387  $cvcl_99 )  AT1_PROC7_CS )) (or (or $cvcl_387  AT0_PROC7_CS )  $cvcl_103 )) (or $cvcl_387  $cvcl_376 )) (or $cvcl_387  $cvcl_411 )) $cvcl_394) (or (or $cvcl_389  $cvcl_100 )  AT2_PROC7_A )) (or (or $cvcl_389  AT1_PROC7_A )  $cvcl_104 )) (or (or $cvcl_389  $cvcl_101 )  AT2_PROC7_B )) (or (or $cvcl_389  AT1_PROC7_B )  $cvcl_105 )) (or (or $cvcl_389  $cvcl_102 )  AT2_PROC7_C )) (or (or $cvcl_389  AT1_PROC7_C )  $cvcl_106 )) (or (or $cvcl_389  $cvcl_103 )  AT2_PROC7_CS )) (or (or $cvcl_389  AT1_PROC7_CS )  $cvcl_107 )) (or $cvcl_389  $cvcl_378 )) (or $cvcl_389  $cvcl_412 )) $cvcl_396) (or (or $cvcl_391  $cvcl_104 )  AT3_PROC7_A )) (or (or $cvcl_391  AT2_PROC7_A )  $cvcl_108 )) (or (or $cvcl_391  $cvcl_105 )  AT3_PROC7_B )) (or (or $cvcl_391  AT2_PROC7_B )  $cvcl_109 )) (or (or $cvcl_391  $cvcl_106 )  AT3_PROC7_C )) (or (or $cvcl_391  AT2_PROC7_C )  $cvcl_110 )) (or (or $cvcl_391  $cvcl_107 )  AT3_PROC7_CS )) (or (or $cvcl_391  AT2_PROC7_CS )  $cvcl_111 )) (or $cvcl_391  $cvcl_380 )) (or $cvcl_391  $cvcl_413 )) $cvcl_398) (or (or $cvcl_387  $cvcl_112 )  AT1_PROC8_A )) (or (or $cvcl_387  AT0_PROC8_A )  $cvcl_116 )) (or (or $cvcl_387  $cvcl_113 )  AT1_PROC8_B )) (or (or $cvcl_387  AT0_PROC8_B )  $cvcl_117 )) (or (or $cvcl_387  $cvcl_114 )  AT1_PROC8_C )) (or (or $cvcl_387  AT0_PROC8_C )  $cvcl_118 )) (or (or $cvcl_387  $cvcl_115 )  AT1_PROC8_CS )) (or (or $cvcl_387  AT0_PROC8_CS )  $cvcl_119 )) (or $cvcl_387  $cvcl_382 )) (or $cvcl_387  $cvcl_414 )) $cvcl_394) (or (or $cvcl_389  $cvcl_116 )  AT2_PROC8_A )) (or (or $cvcl_389  AT1_PROC8_A )  $cvcl_120 )) (or (or $cvcl_389  $cvcl_117 )  AT2_PROC8_B )) (or (or $cvcl_389  AT1_PROC8_B )  $cvcl_121 )) (or (or $cvcl_389  $cvcl_118 )  AT2_PROC8_C )) (or (or $cvcl_389  AT1_PROC8_C )  $cvcl_122 )) (or (or $cvcl_389  $cvcl_119 )  AT2_PROC8_CS )) (or (or $cvcl_389  AT1_PROC8_CS )  $cvcl_123 )) (or $cvcl_389  $cvcl_384 )) (or $cvcl_389  $cvcl_415 )) $cvcl_396) (or (or $cvcl_391  $cvcl_120 )  AT3_PROC8_A )) (or (or $cvcl_391  AT2_PROC8_A )  $cvcl_124 )) (or (or $cvcl_391  $cvcl_121 )  AT3_PROC8_B )) (or (or $cvcl_391  AT2_PROC8_B )  $cvcl_125 )) (or (or $cvcl_391  $cvcl_122 )  AT3_PROC8_C )) (or (or $cvcl_391  AT2_PROC8_C )  $cvcl_126 )) (or (or $cvcl_391  $cvcl_123 )  AT3_PROC8_CS )) (or (or $cvcl_391  AT2_PROC8_CS )  $cvcl_127 )) (or $cvcl_391  $cvcl_386 )) (or $cvcl_391  $cvcl_416 )) $cvcl_398) (or $cvcl_340  $cvcl_417 )) (or $cvcl_444  (not $cvcl_417) )) (or $cvcl_342  $cvcl_418 )) (or $cvcl_450  (not $cvcl_418) )) (or $cvcl_344  $cvcl_419 )) (or $cvcl_456  (not $cvcl_419) )) (or $cvcl_346  $cvcl_420 )) (or $cvcl_462  (not $cvcl_420) )) (or $cvcl_348  $cvcl_421 )) (or $cvcl_466  (not $cvcl_421) )) (or $cvcl_350  $cvcl_422 )) (or $cvcl_470  (not $cvcl_422) )) (or $cvcl_352  $cvcl_423 )) (or $cvcl_474  (not $cvcl_423) )) (or $cvcl_354  $cvcl_424 )) (or $cvcl_478  (not $cvcl_424) )) (or $cvcl_356  $cvcl_425 )) (or $cvcl_482  (not $cvcl_425) )) (or $cvcl_358  $cvcl_426 )) (or $cvcl_486  (not $cvcl_426) )) (or $cvcl_360  $cvcl_427 )) (or $cvcl_490  (not $cvcl_427) )) (or $cvcl_362  $cvcl_428 )) (or $cvcl_494  (not $cvcl_428) )) (or $cvcl_364  $cvcl_429 )) (or $cvcl_498  (not $cvcl_429) )) (or $cvcl_366  $cvcl_430 )) (or $cvcl_502  (not $cvcl_430) )) (or $cvcl_368  $cvcl_431 )) (or $cvcl_506  (not $cvcl_431) )) (or $cvcl_370  $cvcl_432 )) (or $cvcl_510  (not $cvcl_432) )) (or $cvcl_372  $cvcl_433 )) (or $cvcl_514  (not $cvcl_433) )) (or $cvcl_374  $cvcl_434 )) (or $cvcl_518  (not $cvcl_434) )) (or $cvcl_376  $cvcl_435 )) (or $cvcl_522  (not $cvcl_435) )) (or $cvcl_378  $cvcl_436 )) (or $cvcl_526  (not $cvcl_436) )) (or $cvcl_380  $cvcl_437 )) (or $cvcl_530  (not $cvcl_437) )) (or $cvcl_382  $cvcl_438 )) (or $cvcl_534  (not $cvcl_438) )) (or $cvcl_384  $cvcl_439 )) (or $cvcl_538  (not $cvcl_439) )) (or $cvcl_386  $cvcl_440 )) (or $cvcl_542  (not $cvcl_440) )) (or $cvcl_387  $cvcl_389 )) (or $cvcl_389  $cvcl_391 )) (or $cvcl_210  $cvcl_441 )) (or $cvcl_445  $cvcl_449 )) (or $cvcl_211  $cvcl_442 )) (or $cvcl_451  $cvcl_455 )) (or $cvcl_212  $cvcl_443 )) (or $cvcl_457  $cvcl_461 )) (or (or (or $cvcl_128  $cvcl_444 )  $cvcl_445 )  $cvcl_446 )) (or (or (or $cvcl_447  $cvcl_340 )  $cvcl_445 )  $cvcl_446 )) (or (or $cvcl_448  $cvcl_210 )  $cvcl_446 )) (or (or $cvcl_448  $cvcl_445 )  $cvcl_130 )) (or (or (or (not (< AT0_Z AT0_PROC1_X))  $cvcl_444 )  $cvcl_449 )  $cvcl_454 )) (or (or (or $cvcl_130  $cvcl_450 )  $cvcl_451 )  $cvcl_452 )) (or (or (or $cvcl_446  $cvcl_342 )  $cvcl_451 )  $cvcl_452 )) (or (or $cvcl_453  $cvcl_211 )  $cvcl_452 )) (or (or $cvcl_453  $cvcl_451 )  $cvcl_132 )) (or (or (or (not $cvcl_454)  $cvcl_450 )  $cvcl_455 )  $cvcl_460 )) (or (or (or $cvcl_132  $cvcl_456 )  $cvcl_457 )  $cvcl_458 )) (or (or (or $cvcl_452  $cvcl_344 )  $cvcl_457 )  $cvcl_458 )) (or (or $cvcl_459  $cvcl_212 )  $cvcl_458 )) (or (or $cvcl_459  $cvcl_457 )  $cvcl_134 )) (or (or (or (not $cvcl_460)  $cvcl_456 )  $cvcl_461 )  (< AT3_Z AT3_PROC1_X) )) (or (or (or $cvcl_136  $cvcl_462 )  $cvcl_445 )  $cvcl_463 )) (or (or (or $cvcl_464  $cvcl_346 )  $cvcl_445 )  $cvcl_463 )) (or (or $cvcl_465  $cvcl_210 )  $cvcl_463 )) (or (or $cvcl_465  $cvcl_445 )  $cvcl_138 )) (or (or (or (not (< AT0_Z AT0_PROC2_X))  $cvcl_462 )  $cvcl_449 )  $cvcl_469 )) (or (or (or $cvcl_138  $cvcl_466 )  $cvcl_451 )  $cvcl_467 )) (or (or (or $cvcl_463  $cvcl_348 )  $cvcl_451 )  $cvcl_467 )) (or (or $cvcl_468  $cvcl_211 )  $cvcl_467 )) (or (or $cvcl_468  $cvcl_451 )  $cvcl_140 )) (or (or (or (not $cvcl_469)  $cvcl_466 )  $cvcl_455 )  $cvcl_473 )) (or (or (or $cvcl_140  $cvcl_470 )  $cvcl_457 )  $cvcl_471 )) (or (or (or $cvcl_467  $cvcl_350 )  $cvcl_457 )  $cvcl_471 )) (or (or $cvcl_472  $cvcl_212 )  $cvcl_471 )) (or (or $cvcl_472  $cvcl_457 )  $cvcl_142 )) (or (or (or (not $cvcl_473)  $cvcl_470 )  $cvcl_461 )  (< AT3_Z AT3_PROC2_X) )) (or (or (or $cvcl_144  $cvcl_474 )  $cvcl_445 )  $cvcl_475 )) (or (or (or $cvcl_476  $cvcl_352 )  $cvcl_445 )  $cvcl_475 )) (or (or $cvcl_477  $cvcl_210 )  $cvcl_475 )) (or (or $cvcl_477  $cvcl_445 )  $cvcl_146 )) (or (or (or (not (< AT0_Z AT0_PROC3_X))  $cvcl_474 )  $cvcl_449 )  $cvcl_481 )) (or (or (or $cvcl_146  $cvcl_478 )  $cvcl_451 )  $cvcl_479 )) (or (or (or $cvcl_475  $cvcl_354 )  $cvcl_451 )  $cvcl_479 )) (or (or $cvcl_480  $cvcl_211 )  $cvcl_479 )) (or (or $cvcl_480  $cvcl_451 )  $cvcl_148 )) (or (or (or (not $cvcl_481)  $cvcl_478 )  $cvcl_455 )  $cvcl_485 )) (or (or (or $cvcl_148  $cvcl_482 )  $cvcl_457 )  $cvcl_483 )) (or (or (or $cvcl_479  $cvcl_356 )  $cvcl_457 )  $cvcl_483 )) (or (or $cvcl_484  $cvcl_212 )  $cvcl_483 )) (or (or $cvcl_484  $cvcl_457 )  $cvcl_150 )) (or (or (or (not $cvcl_485)  $cvcl_482 )  $cvcl_461 )  (< AT3_Z AT3_PROC3_X) )) (or (or (or $cvcl_152  $cvcl_486 )  $cvcl_445 )  $cvcl_487 )) (or (or (or $cvcl_488  $cvcl_358 )  $cvcl_445 )  $cvcl_487 )) (or (or $cvcl_489  $cvcl_210 )  $cvcl_487 )) (or (or $cvcl_489  $cvcl_445 )  $cvcl_154 )) (or (or (or (not (< AT0_Z AT0_PROC4_X))  $cvcl_486 )  $cvcl_449 )  $cvcl_493 )) (or (or (or $cvcl_154  $cvcl_490 )  $cvcl_451 )  $cvcl_491 )) (or (or (or $cvcl_487  $cvcl_360 )  $cvcl_451 )  $cvcl_491 )) (or (or $cvcl_492  $cvcl_211 )  $cvcl_491 )) (or (or $cvcl_492  $cvcl_451 )  $cvcl_156 )) (or (or (or (not $cvcl_493)  $cvcl_490 )  $cvcl_455 )  $cvcl_497 )) (or (or (or $cvcl_156  $cvcl_494 )  $cvcl_457 )  $cvcl_495 )) (or (or (or $cvcl_491  $cvcl_362 )  $cvcl_457 )  $cvcl_495 )) (or (or $cvcl_496  $cvcl_212 )  $cvcl_495 )) (or (or $cvcl_496  $cvcl_457 )  $cvcl_158 )) (or (or (or (not $cvcl_497)  $cvcl_494 )  $cvcl_461 )  (< AT3_Z AT3_PROC4_X) )) (or (or (or $cvcl_160  $cvcl_498 )  $cvcl_445 )  $cvcl_499 )) (or (or (or $cvcl_500  $cvcl_364 )  $cvcl_445 )  $cvcl_499 )) (or (or $cvcl_501  $cvcl_210 )  $cvcl_499 )) (or (or $cvcl_501  $cvcl_445 )  $cvcl_162 )) (or (or (or (not (< AT0_Z AT0_PROC5_X))  $cvcl_498 )  $cvcl_449 )  $cvcl_505 )) (or (or (or $cvcl_162  $cvcl_502 )  $cvcl_451 )  $cvcl_503 )) (or (or (or $cvcl_499  $cvcl_366 )  $cvcl_451 )  $cvcl_503 )) (or (or $cvcl_504  $cvcl_211 )  $cvcl_503 )) (or (or $cvcl_504  $cvcl_451 )  $cvcl_164 )) (or (or (or (not $cvcl_505)  $cvcl_502 )  $cvcl_455 )  $cvcl_509 )) (or (or (or $cvcl_164  $cvcl_506 )  $cvcl_457 )  $cvcl_507 )) (or (or (or $cvcl_503  $cvcl_368 )  $cvcl_457 )  $cvcl_507 )) (or (or $cvcl_508  $cvcl_212 )  $cvcl_507 )) (or (or $cvcl_508  $cvcl_457 )  $cvcl_166 )) (or (or (or (not $cvcl_509)  $cvcl_506 )  $cvcl_461 )  (< AT3_Z AT3_PROC5_X) )) (or (or (or $cvcl_168  $cvcl_510 )  $cvcl_445 )  $cvcl_511 )) (or (or (or $cvcl_512  $cvcl_370 )  $cvcl_445 )  $cvcl_511 )) (or (or $cvcl_513  $cvcl_210 )  $cvcl_511 )) (or (or $cvcl_513  $cvcl_445 )  $cvcl_170 )) (or (or (or (not (< AT0_Z AT0_PROC6_X))  $cvcl_510 )  $cvcl_449 )  $cvcl_517 )) (or (or (or $cvcl_170  $cvcl_514 )  $cvcl_451 )  $cvcl_515 )) (or (or (or $cvcl_511  $cvcl_372 )  $cvcl_451 )  $cvcl_515 )) (or (or $cvcl_516  $cvcl_211 )  $cvcl_515 )) (or (or $cvcl_516  $cvcl_451 )  $cvcl_172 )) (or (or (or (not $cvcl_517)  $cvcl_514 )  $cvcl_455 )  $cvcl_521 )) (or (or (or $cvcl_172  $cvcl_518 )  $cvcl_457 )  $cvcl_519 )) (or (or (or $cvcl_515  $cvcl_374 )  $cvcl_457 )  $cvcl_519 )) (or (or $cvcl_520  $cvcl_212 )  $cvcl_519 )) (or (or $cvcl_520  $cvcl_457 )  $cvcl_174 )) (or (or (or (not $cvcl_521)  $cvcl_518 )  $cvcl_461 )  (< AT3_Z AT3_PROC6_X) )) (or (or (or $cvcl_176  $cvcl_522 )  $cvcl_445 )  $cvcl_523 )) (or (or (or $cvcl_524  $cvcl_376 )  $cvcl_445 )  $cvcl_523 )) (or (or $cvcl_525  $cvcl_210 )  $cvcl_523 )) (or (or $cvcl_525  $cvcl_445 )  $cvcl_178 )) (or (or (or (not (< AT0_Z AT0_PROC7_X))  $cvcl_522 )  $cvcl_449 )  $cvcl_529 )) (or (or (or $cvcl_178  $cvcl_526 )  $cvcl_451 )  $cvcl_527 )) (or (or (or $cvcl_523  $cvcl_378 )  $cvcl_451 )  $cvcl_527 )) (or (or $cvcl_528  $cvcl_211 )  $cvcl_527 )) (or (or $cvcl_528  $cvcl_451 )  $cvcl_180 )) (or (or (or (not $cvcl_529)  $cvcl_526 )  $cvcl_455 )  $cvcl_533 )) (or (or (or $cvcl_180  $cvcl_530 )  $cvcl_457 )  $cvcl_531 )) (or (or (or $cvcl_527  $cvcl_380 )  $cvcl_457 )  $cvcl_531 )) (or (or $cvcl_532  $cvcl_212 )  $cvcl_531 )) (or (or $cvcl_532  $cvcl_457 )  $cvcl_182 )) (or (or (or (not $cvcl_533)  $cvcl_530 )  $cvcl_461 )  (< AT3_Z AT3_PROC7_X) )) (or (or (or $cvcl_184  $cvcl_534 )  $cvcl_445 )  $cvcl_535 )) (or (or (or $cvcl_536  $cvcl_382 )  $cvcl_445 )  $cvcl_535 )) (or (or $cvcl_537  $cvcl_210 )  $cvcl_535 )) (or (or $cvcl_537  $cvcl_445 )  $cvcl_186 )) (or (or (or (not (< AT0_Z AT0_PROC8_X))  $cvcl_534 )  $cvcl_449 )  $cvcl_541 )) (or (or (or $cvcl_186  $cvcl_538 )  $cvcl_451 )  $cvcl_539 )) (or (or (or $cvcl_535  $cvcl_384 )  $cvcl_451 )  $cvcl_539 )) (or (or $cvcl_540  $cvcl_211 )  $cvcl_539 )) (or (or $cvcl_540  $cvcl_451 )  $cvcl_188 )) (or (or (or (not $cvcl_541)  $cvcl_538 )  $cvcl_455 )  $cvcl_545 )) (or (or (or $cvcl_188  $cvcl_542 )  $cvcl_457 )  $cvcl_543 )) (or (or (or $cvcl_539  $cvcl_386 )  $cvcl_457 )  $cvcl_543 )) (or (or $cvcl_544  $cvcl_212 )  $cvcl_543 )) (or (or $cvcl_544  $cvcl_457 )  $cvcl_190 )) (or (or (or (not $cvcl_545)  $cvcl_542 )  $cvcl_461 )  (< AT3_Z AT3_PROC8_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) $cvcl_128) $cvcl_136) $cvcl_144) $cvcl_152) $cvcl_160) $cvcl_168) $cvcl_176) $cvcl_184) AT0_ID0) (or (or (or (or (or (or (or $cvcl_339  $cvcl_345 )  $cvcl_351 )  $cvcl_357 )  $cvcl_363 )  $cvcl_369 )  $cvcl_375 )  $cvcl_381 )) (or (or (or (or (or (or (or $cvcl_341  $cvcl_347 )  $cvcl_353 )  $cvcl_359 )  $cvcl_365 )  $cvcl_371 )  $cvcl_377 )  $cvcl_383 )) (or (or (or (or (or (or (or $cvcl_343  $cvcl_349 )  $cvcl_355 )  $cvcl_361 )  $cvcl_367 )  $cvcl_373 )  $cvcl_379 )  $cvcl_385 )) (or $cvcl_546  $cvcl_547 )) (or $cvcl_546  $cvcl_548 )) (or $cvcl_546  $cvcl_549 )) (or $cvcl_546  $cvcl_550 )) (or $cvcl_546  $cvcl_551 )) (or $cvcl_546  $cvcl_552 )) (or $cvcl_546  $cvcl_553 )) (or $cvcl_546  $cvcl_554 )) (or $cvcl_547  $cvcl_548 )) (or $cvcl_547  $cvcl_549 )) (or $cvcl_547  $cvcl_550 )) (or $cvcl_547  $cvcl_551 )) (or $cvcl_547  $cvcl_552 )) (or $cvcl_547  $cvcl_553 )) (or $cvcl_547  $cvcl_554 )) (or $cvcl_548  $cvcl_549 )) (or $cvcl_548  $cvcl_550 )) (or $cvcl_548  $cvcl_551 )) (or $cvcl_548  $cvcl_552 )) (or $cvcl_548  $cvcl_553 )) (or $cvcl_548  $cvcl_554 )) (or $cvcl_549  $cvcl_550 )) (or $cvcl_549  $cvcl_551 )) (or $cvcl_549  $cvcl_552 )) (or $cvcl_549  $cvcl_553 )) (or $cvcl_549  $cvcl_554 )) (or $cvcl_550  $cvcl_551 )) (or $cvcl_550  $cvcl_552 )) (or $cvcl_550  $cvcl_553 )) (or $cvcl_550  $cvcl_554 )) (or $cvcl_551  $cvcl_552 )) (or $cvcl_551  $cvcl_553 )) (or $cvcl_551  $cvcl_554 )) (or $cvcl_552  $cvcl_553 )) (or $cvcl_552  $cvcl_554 )) (or $cvcl_553  $cvcl_554 )) (or $cvcl_555  $cvcl_556 )) (or $cvcl_555  $cvcl_557 )) (or $cvcl_555  $cvcl_558 )) (or $cvcl_555  $cvcl_559 )) (or $cvcl_555  $cvcl_560 )) (or $cvcl_555  $cvcl_561 )) (or $cvcl_555  $cvcl_562 )) (or $cvcl_555  $cvcl_563 )) (or $cvcl_556  $cvcl_557 )) (or $cvcl_556  $cvcl_558 )) (or $cvcl_556  $cvcl_559 )) (or $cvcl_556  $cvcl_560 )) (or $cvcl_556  $cvcl_561 )) (or $cvcl_556  $cvcl_562 )) (or $cvcl_556  $cvcl_563 )) (or $cvcl_557  $cvcl_558 )) (or $cvcl_557  $cvcl_559 )) (or $cvcl_557  $cvcl_560 )) (or $cvcl_557  $cvcl_561 )) (or $cvcl_557  $cvcl_562 )) (or $cvcl_557  $cvcl_563 )) (or $cvcl_558  $cvcl_559 )) (or $cvcl_558  $cvcl_560 )) (or $cvcl_558  $cvcl_561 )) (or $cvcl_558  $cvcl_562 )) (or $cvcl_558  $cvcl_563 )) (or $cvcl_559  $cvcl_560 )) (or $cvcl_559  $cvcl_561 )) (or $cvcl_559  $cvcl_562 )) (or $cvcl_559  $cvcl_563 )) (or $cvcl_560  $cvcl_561 )) (or $cvcl_560  $cvcl_562 )) (or $cvcl_560  $cvcl_563 )) (or $cvcl_561  $cvcl_562 )) (or $cvcl_561  $cvcl_563 )) (or $cvcl_562  $cvcl_563 )) (or $cvcl_564  $cvcl_565 )) (or $cvcl_564  $cvcl_566 )) (or $cvcl_564  $cvcl_567 )) (or $cvcl_564  $cvcl_568 )) (or $cvcl_564  $cvcl_569 )) (or $cvcl_564  $cvcl_570 )) (or $cvcl_564  $cvcl_571 )) (or $cvcl_564  $cvcl_572 )) (or $cvcl_565  $cvcl_566 )) (or $cvcl_565  $cvcl_567 )) (or $cvcl_565  $cvcl_568 )) (or $cvcl_565  $cvcl_569 )) (or $cvcl_565  $cvcl_570 )) (or $cvcl_565  $cvcl_571 )) (or $cvcl_565  $cvcl_572 )) (or $cvcl_566  $cvcl_567 )) (or $cvcl_566  $cvcl_568 )) (or $cvcl_566  $cvcl_569 )) (or $cvcl_566  $cvcl_570 )) (or $cvcl_566  $cvcl_571 )) (or $cvcl_566  $cvcl_572 )) (or $cvcl_567  $cvcl_568 )) (or $cvcl_567  $cvcl_569 )) (or $cvcl_567  $cvcl_570 )) (or $cvcl_567  $cvcl_571 )) (or $cvcl_567  $cvcl_572 )) (or $cvcl_568  $cvcl_569 )) (or $cvcl_568  $cvcl_570 )) (or $cvcl_568  $cvcl_571 )) (or $cvcl_568  $cvcl_572 )) (or $cvcl_569  $cvcl_570 )) (or $cvcl_569  $cvcl_571 )) (or $cvcl_569  $cvcl_572 )) (or $cvcl_570  $cvcl_571 )) (or $cvcl_570  $cvcl_572 )) (or $cvcl_571  $cvcl_572 )) (or $cvcl_573  $cvcl_574 )) (or $cvcl_573  $cvcl_575 )) (or $cvcl_573  $cvcl_576 )) (or $cvcl_573  $cvcl_577 )) (or $cvcl_573  $cvcl_578 )) (or $cvcl_573  $cvcl_579 )) (or $cvcl_573  $cvcl_580 )) (or $cvcl_573  $cvcl_581 )) (or $cvcl_574  $cvcl_575 )) (or $cvcl_574  $cvcl_576 )) (or $cvcl_574  $cvcl_577 )) (or $cvcl_574  $cvcl_578 )) (or $cvcl_574  $cvcl_579 )) (or $cvcl_574  $cvcl_580 )) (or $cvcl_574  $cvcl_581 )) (or $cvcl_575  $cvcl_576 )) (or $cvcl_575  $cvcl_577 )) (or $cvcl_575  $cvcl_578 )) (or $cvcl_575  $cvcl_579 )) (or $cvcl_575  $cvcl_580 )) (or $cvcl_575  $cvcl_581 )) (or $cvcl_576  $cvcl_577 )) (or $cvcl_576  $cvcl_578 )) (or $cvcl_576  $cvcl_579 )) (or $cvcl_576  $cvcl_580 )) (or $cvcl_576  $cvcl_581 )) (or $cvcl_577  $cvcl_578 )) (or $cvcl_577  $cvcl_579 )) (or $cvcl_577  $cvcl_580 )) (or $cvcl_577  $cvcl_581 )) (or $cvcl_578  $cvcl_579 )) (or $cvcl_578  $cvcl_580 )) (or $cvcl_578  $cvcl_581 )) (or $cvcl_579  $cvcl_580 )) (or $cvcl_579  $cvcl_581 )) (or $cvcl_580  $cvcl_581 )) (or $cvcl_192  AT0_ID0 )) (or $cvcl_192  AT1_ID0 )) (or $cvcl_193  AT1_ID1 )) (or $cvcl_195  AT0_ID0 )) (or $cvcl_195  AT1_ID0 )) (or $cvcl_196  AT0_ID1 )) (or $cvcl_196  AT1_ID1 )) (or $cvcl_197  AT1_ID0 )) (or (or $cvcl_387  $cvcl_547 )  AT1_ID1 )) (or $cvcl_213  AT0_ID0 )) (or $cvcl_213  AT1_ID0 )) (or $cvcl_214  AT1_ID2 )) (or $cvcl_216  AT0_ID0 )) (or $cvcl_216  AT1_ID0 )) (or $cvcl_217  AT0_ID2 )) (or $cvcl_217  AT1_ID2 )) (or $cvcl_218  AT1_ID0 )) (or (or $cvcl_387  $cvcl_548 )  AT1_ID2 )) (or $cvcl_231  AT0_ID0 )) (or $cvcl_231  AT1_ID0 )) (or $cvcl_232  AT1_ID3 )) (or $cvcl_234  AT0_ID0 )) (or $cvcl_234  AT1_ID0 )) (or $cvcl_235  AT0_ID3 )) (or $cvcl_235  AT1_ID3 )) (or $cvcl_236  AT1_ID0 )) (or (or $cvcl_387  $cvcl_549 )  AT1_ID3 )) (or $cvcl_249  AT0_ID0 )) (or $cvcl_249  AT1_ID0 )) (or $cvcl_250  AT1_ID4 )) (or $cvcl_252  AT0_ID0 )) (or $cvcl_252  AT1_ID0 )) (or $cvcl_253  AT0_ID4 )) (or $cvcl_253  AT1_ID4 )) (or $cvcl_254  AT1_ID0 )) (or (or $cvcl_387  $cvcl_550 )  AT1_ID4 )) (or $cvcl_267  AT0_ID0 )) (or $cvcl_267  AT1_ID0 )) (or $cvcl_268  AT1_ID5 )) (or $cvcl_270  AT0_ID0 )) (or $cvcl_270  AT1_ID0 )) (or $cvcl_271  AT0_ID5 )) (or $cvcl_271  AT1_ID5 )) (or $cvcl_272  AT1_ID0 )) (or (or $cvcl_387  $cvcl_551 )  AT1_ID5 )) (or $cvcl_285  AT0_ID0 )) (or $cvcl_285  AT1_ID0 )) (or $cvcl_286  AT1_ID6 )) (or $cvcl_288  AT0_ID0 )) (or $cvcl_288  AT1_ID0 )) (or $cvcl_289  AT0_ID6 )) (or $cvcl_289  AT1_ID6 )) (or $cvcl_290  AT1_ID0 )) (or (or $cvcl_387  $cvcl_552 )  AT1_ID6 )) (or $cvcl_303  AT0_ID0 )) (or $cvcl_303  AT1_ID0 )) (or $cvcl_304  AT1_ID7 )) (or $cvcl_306  AT0_ID0 )) (or $cvcl_306  AT1_ID0 )) (or $cvcl_307  AT0_ID7 )) (or $cvcl_307  AT1_ID7 )) (or $cvcl_308  AT1_ID0 )) (or (or $cvcl_387  $cvcl_553 )  AT1_ID7 )) (or $cvcl_321  AT0_ID0 )) (or $cvcl_321  AT1_ID0 )) (or $cvcl_322  AT1_ID8 )) (or $cvcl_324  AT0_ID0 )) (or $cvcl_324  AT1_ID0 )) (or $cvcl_325  AT0_ID8 )) (or $cvcl_325  AT1_ID8 )) (or $cvcl_326  AT1_ID0 )) (or (or $cvcl_387  $cvcl_554 )  AT1_ID8 )) (or (or $cvcl_387  $cvcl_546 )  AT1_ID0 )) (or $cvcl_198  AT1_ID0 )) (or $cvcl_198  AT2_ID0 )) (or $cvcl_199  AT2_ID1 )) (or $cvcl_201  AT1_ID0 )) (or $cvcl_201  AT2_ID0 )) (or $cvcl_202  AT1_ID1 )) (or $cvcl_202  AT2_ID1 )) (or $cvcl_203  AT2_ID0 )) (or (or $cvcl_389  $cvcl_556 )  AT2_ID1 )) (or $cvcl_219  AT1_ID0 )) (or $cvcl_219  AT2_ID0 )) (or $cvcl_220  AT2_ID2 )) (or $cvcl_222  AT1_ID0 )) (or $cvcl_222  AT2_ID0 )) (or $cvcl_223  AT1_ID2 )) (or $cvcl_223  AT2_ID2 )) (or $cvcl_224  AT2_ID0 )) (or (or $cvcl_389  $cvcl_557 )  AT2_ID2 )) (or $cvcl_237  AT1_ID0 )) (or $cvcl_237  AT2_ID0 )) (or $cvcl_238  AT2_ID3 )) (or $cvcl_240  AT1_ID0 )) (or $cvcl_240  AT2_ID0 )) (or $cvcl_241  AT1_ID3 )) (or $cvcl_241  AT2_ID3 )) (or $cvcl_242  AT2_ID0 )) (or (or $cvcl_389  $cvcl_558 )  AT2_ID3 )) (or $cvcl_255  AT1_ID0 )) (or $cvcl_255  AT2_ID0 )) (or $cvcl_256  AT2_ID4 )) (or $cvcl_258  AT1_ID0 )) (or $cvcl_258  AT2_ID0 )) (or $cvcl_259  AT1_ID4 )) (or $cvcl_259  AT2_ID4 )) (or $cvcl_260  AT2_ID0 )) (or (or $cvcl_389  $cvcl_559 )  AT2_ID4 )) (or $cvcl_273  AT1_ID0 )) (or $cvcl_273  AT2_ID0 )) (or $cvcl_274  AT2_ID5 )) (or $cvcl_276  AT1_ID0 )) (or $cvcl_276  AT2_ID0 )) (or $cvcl_277  AT1_ID5 )) (or $cvcl_277  AT2_ID5 )) (or $cvcl_278  AT2_ID0 )) (or (or $cvcl_389  $cvcl_560 )  AT2_ID5 )) (or $cvcl_291  AT1_ID0 )) (or $cvcl_291  AT2_ID0 )) (or $cvcl_292  AT2_ID6 )) (or $cvcl_294  AT1_ID0 )) (or $cvcl_294  AT2_ID0 )) (or $cvcl_295  AT1_ID6 )) (or $cvcl_295  AT2_ID6 )) (or $cvcl_296  AT2_ID0 )) (or (or $cvcl_389  $cvcl_561 )  AT2_ID6 )) (or $cvcl_309  AT1_ID0 )) (or $cvcl_309  AT2_ID0 )) (or $cvcl_310  AT2_ID7 )) (or $cvcl_312  AT1_ID0 )) (or $cvcl_312  AT2_ID0 )) (or $cvcl_313  AT1_ID7 )) (or $cvcl_313  AT2_ID7 )) (or $cvcl_314  AT2_ID0 )) (or (or $cvcl_389  $cvcl_562 )  AT2_ID7 )) (or $cvcl_327  AT1_ID0 )) (or $cvcl_327  AT2_ID0 )) (or $cvcl_328  AT2_ID8 )) (or $cvcl_330  AT1_ID0 )) (or $cvcl_330  AT2_ID0 )) (or $cvcl_331  AT1_ID8 )) (or $cvcl_331  AT2_ID8 )) (or $cvcl_332  AT2_ID0 )) (or (or $cvcl_389  $cvcl_563 )  AT2_ID8 )) (or (or $cvcl_389  $cvcl_555 )  AT2_ID0 )) (or $cvcl_204  AT2_ID0 )) (or $cvcl_204  AT3_ID0 )) (or $cvcl_205  AT3_ID1 )) (or $cvcl_207  AT2_ID0 )) (or $cvcl_207  AT3_ID0 )) (or $cvcl_208  AT2_ID1 )) (or $cvcl_208  AT3_ID1 )) (or $cvcl_209  AT3_ID0 )) (or (or $cvcl_391  $cvcl_565 )  AT3_ID1 )) (or $cvcl_225  AT2_ID0 )) (or $cvcl_225  AT3_ID0 )) (or $cvcl_226  AT3_ID2 )) (or $cvcl_228  AT2_ID0 )) (or $cvcl_228  AT3_ID0 )) (or $cvcl_229  AT2_ID2 )) (or $cvcl_229  AT3_ID2 )) (or $cvcl_230  AT3_ID0 )) (or (or $cvcl_391  $cvcl_566 )  AT3_ID2 )) (or $cvcl_243  AT2_ID0 )) (or $cvcl_243  AT3_ID0 )) (or $cvcl_244  AT3_ID3 )) (or $cvcl_246  AT2_ID0 )) (or $cvcl_246  AT3_ID0 )) (or $cvcl_247  AT2_ID3 )) (or $cvcl_247  AT3_ID3 )) (or $cvcl_248  AT3_ID0 )) (or (or $cvcl_391  $cvcl_567 )  AT3_ID3 )) (or $cvcl_261  AT2_ID0 )) (or $cvcl_261  AT3_ID0 )) (or $cvcl_262  AT3_ID4 )) (or $cvcl_264  AT2_ID0 )) (or $cvcl_264  AT3_ID0 )) (or $cvcl_265  AT2_ID4 )) (or $cvcl_265  AT3_ID4 )) (or $cvcl_266  AT3_ID0 )) (or (or $cvcl_391  $cvcl_568 )  AT3_ID4 )) (or $cvcl_279  AT2_ID0 )) (or $cvcl_279  AT3_ID0 )) (or $cvcl_280  AT3_ID5 )) (or $cvcl_282  AT2_ID0 )) (or $cvcl_282  AT3_ID0 )) (or $cvcl_283  AT2_ID5 )) (or $cvcl_283  AT3_ID5 )) (or $cvcl_284  AT3_ID0 )) (or (or $cvcl_391  $cvcl_569 )  AT3_ID5 )) (or $cvcl_297  AT2_ID0 )) (or $cvcl_297  AT3_ID0 )) (or $cvcl_298  AT3_ID6 )) (or $cvcl_300  AT2_ID0 )) (or $cvcl_300  AT3_ID0 )) (or $cvcl_301  AT2_ID6 )) (or $cvcl_301  AT3_ID6 )) (or $cvcl_302  AT3_ID0 )) (or (or $cvcl_391  $cvcl_570 )  AT3_ID6 )) (or $cvcl_315  AT2_ID0 )) (or $cvcl_315  AT3_ID0 )) (or $cvcl_316  AT3_ID7 )) (or $cvcl_318  AT2_ID0 )) (or $cvcl_318  AT3_ID0 )) (or $cvcl_319  AT2_ID7 )) (or $cvcl_319  AT3_ID7 )) (or $cvcl_320  AT3_ID0 )) (or (or $cvcl_391  $cvcl_571 )  AT3_ID7 )) (or $cvcl_333  AT2_ID0 )) (or $cvcl_333  AT3_ID0 )) (or $cvcl_334  AT3_ID8 )) (or $cvcl_336  AT2_ID0 )) (or $cvcl_336  AT3_ID0 )) (or $cvcl_337  AT2_ID8 )) (or $cvcl_337  AT3_ID8 )) (or $cvcl_338  AT3_ID0 )) (or (or $cvcl_391  $cvcl_572 )  AT3_ID8 )) (or (or $cvcl_391  $cvcl_564 )  AT3_ID0 )) (or $cvcl_4  AT3_PROC1_A )) (or AT1_PROC1_A  $cvcl_12 )) (or $cvcl_5  AT3_PROC1_B )) (or AT1_PROC1_B  $cvcl_13 )) (or $cvcl_6  AT3_PROC1_C )) (or AT1_PROC1_C  $cvcl_14 )) (or $cvcl_7  AT3_PROC1_CS )) (or AT1_PROC1_CS  $cvcl_15 )) (or $cvcl_556  AT3_ID1 )) (or AT1_ID1  $cvcl_574 )) (= (- AT1_PROC1_X AT1_Z) (- AT3_PROC1_X AT3_Z))) (or $cvcl_20  AT3_PROC2_A )) (or AT1_PROC2_A  $cvcl_28 )) (or $cvcl_21  AT3_PROC2_B )) (or AT1_PROC2_B  $cvcl_29 )) (or $cvcl_22  AT3_PROC2_C )) (or AT1_PROC2_C  $cvcl_30 )) (or $cvcl_23  AT3_PROC2_CS )) (or AT1_PROC2_CS  $cvcl_31 )) (or $cvcl_557  AT3_ID2 )) (or AT1_ID2  $cvcl_575 )) (= (- AT1_PROC2_X AT1_Z) (- AT3_PROC2_X AT3_Z))) (or $cvcl_36  AT3_PROC3_A )) (or AT1_PROC3_A  $cvcl_44 )) (or $cvcl_37  AT3_PROC3_B )) (or AT1_PROC3_B  $cvcl_45 )) (or $cvcl_38  AT3_PROC3_C )) (or AT1_PROC3_C  $cvcl_46 )) (or $cvcl_39  AT3_PROC3_CS )) (or AT1_PROC3_CS  $cvcl_47 )) (or $cvcl_558  AT3_ID3 )) (or AT1_ID3  $cvcl_576 )) (= (- AT1_PROC3_X AT1_Z) (- AT3_PROC3_X AT3_Z))) (or $cvcl_52  AT3_PROC4_A )) (or AT1_PROC4_A  $cvcl_60 )) (or $cvcl_53  AT3_PROC4_B )) (or AT1_PROC4_B  $cvcl_61 )) (or $cvcl_54  AT3_PROC4_C )) (or AT1_PROC4_C  $cvcl_62 )) (or $cvcl_55  AT3_PROC4_CS )) (or AT1_PROC4_CS  $cvcl_63 )) (or $cvcl_559  AT3_ID4 )) (or AT1_ID4  $cvcl_577 )) (= (- AT1_PROC4_X AT1_Z) (- AT3_PROC4_X AT3_Z))) (or $cvcl_68  AT3_PROC5_A )) (or AT1_PROC5_A  $cvcl_76 )) (or $cvcl_69  AT3_PROC5_B )) (or AT1_PROC5_B  $cvcl_77 )) (or $cvcl_70  AT3_PROC5_C )) (or AT1_PROC5_C  $cvcl_78 )) (or $cvcl_71  AT3_PROC5_CS )) (or AT1_PROC5_CS  $cvcl_79 )) (or $cvcl_560  AT3_ID5 )) (or AT1_ID5  $cvcl_578 )) (= (- AT1_PROC5_X AT1_Z) (- AT3_PROC5_X AT3_Z))) (or $cvcl_84  AT3_PROC6_A )) (or AT1_PROC6_A  $cvcl_92 )) (or $cvcl_85  AT3_PROC6_B )) (or AT1_PROC6_B  $cvcl_93 )) (or $cvcl_86  AT3_PROC6_C )) (or AT1_PROC6_C  $cvcl_94 )) (or $cvcl_87  AT3_PROC6_CS )) (or AT1_PROC6_CS  $cvcl_95 )) (or $cvcl_561  AT3_ID6 )) (or AT1_ID6  $cvcl_579 )) (= (- AT1_PROC6_X AT1_Z) (- AT3_PROC6_X AT3_Z))) (or $cvcl_100  AT3_PROC7_A )) (or AT1_PROC7_A  $cvcl_108 )) (or $cvcl_101  AT3_PROC7_B )) (or AT1_PROC7_B  $cvcl_109 )) (or $cvcl_102  AT3_PROC7_C )) (or AT1_PROC7_C  $cvcl_110 )) (or $cvcl_103  AT3_PROC7_CS )) (or AT1_PROC7_CS  $cvcl_111 )) (or $cvcl_562  AT3_ID7 )) (or AT1_ID7  $cvcl_580 )) (= (- AT1_PROC7_X AT1_Z) (- AT3_PROC7_X AT3_Z))) (or $cvcl_116  AT3_PROC8_A )) (or AT1_PROC8_A  $cvcl_124 )) (or $cvcl_117  AT3_PROC8_B )) (or AT1_PROC8_B  $cvcl_125 )) (or $cvcl_118  AT3_PROC8_C )) (or AT1_PROC8_C  $cvcl_126 )) (or $cvcl_119  AT3_PROC8_CS )) (or AT1_PROC8_CS  $cvcl_127 )) (or $cvcl_563  AT3_ID8 )) (or AT1_ID8  $cvcl_581 )) (= (- AT1_PROC8_X AT1_Z) (- AT3_PROC8_X AT3_Z))) (or (or AT1_PROC1_B  AT2_PROC1_B )  AT3_PROC1_B )) $cvcl_7) $cvcl_11) $cvcl_15)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)