(benchmark FISCHER3_1_fair.smt :source { Older mathsat benchmarks. Contact Mathsat group at http://mathsat.itc.it/ for more information. This benchmark was automatically translated into SMT-LIB format from CVC format using CVC Lite } :status unknown :logic QF_LIA :extrapreds ((AT0_PROC3_CS)) :extrafuns ((AT0_PROC1_X Int)) :extrapreds ((AT0_ID0)) :extrapreds ((AT1_PROC2_C)) :extrapreds ((AT0_ID1)) :extrapreds ((AT1_PROC2_B)) :extrapreds ((AT0_ID2)) :extrapreds ((AT1_PROC2_A)) :extrapreds ((AT0_ID3)) :extrapreds ((AT0_PROC3_SW_CS_A_TAU)) :extrapreds ((AT1_PROC2_CS)) :extrapreds ((AT0_PROC3_TAU)) :extrapreds ((AT0_PROC2_SW_C_B_TAU)) :extrapreds ((AT0_PROC1_C)) :extrapreds ((AT0_PROC1_B)) :extrapreds ((AT0_PROC1_A)) :extrafuns ((AT1_PROC3_X Int)) :extrapreds ((AT0_PROC3_WAIT)) :extrapreds ((AT0_PROC2_CS)) :extrapreds ((AT1_ID0)) :extrapreds ((AT1_ID1)) :extrapreds ((AT1_ID2)) :extrapreds ((AT1_ID3)) :extrapreds ((AT0_PROC1_SW_CS_A_TAU)) :extrafuns ((AT0_PROC2_X Int)) :extrapreds ((AT1_PROC3_CS)) :extrapreds ((AT1_PROC3_C)) :extrapreds ((AT1_PROC3_B)) :extrapreds ((AT1_PROC3_A)) :extrafuns ((AT1_PROC1_X Int)) :extrafuns ((AT1_Z Int)) :extrapreds ((AT0_PROC2_C)) :extrapreds ((AT0_PROC2_SW_C_CS_TAU)) :extrapreds ((AT0_PROC2_B)) :extrapreds ((AT0_PROC2_A)) :extrapreds ((AT0_PROC3_SW_B_C_TAU)) :extrapreds ((AT0_PROC1_SW_C_B_TAU)) :extrapreds ((AT0_PROC1_CS)) :extrapreds ((AT0_PROC1_TAU)) :extrapreds ((AT0_PROC1_SW_C_CS_TAU)) :extrapreds ((AT0_PROC1_WAIT)) :extrapreds ((AT1_PROC1_C)) :extrapreds ((AT1_PROC1_B)) :extrapreds ((AT1_PROC1_A)) :extrapreds ((AT0_PROC3_SW_A_B_TAU)) :extrapreds ((AT0_DELTA)) :extrafuns ((AT0_PROC3_X Int)) :extrapreds ((AT0_PROC2_SW_B_C_TAU)) :extrapreds ((AT1_PROC1_CS)) :extrapreds ((AT0_PROC3_SW_C_CS_TAU)) :extrapreds ((AT0_PROC1_SW_A_B_TAU)) :extrapreds ((AT0_PROC2_SW_CS_A_TAU)) :extrapreds ((AT0_PROC2_TAU)) :extrafuns ((AT1_PROC2_X Int)) :extrafuns ((AT0_Z Int)) :extrapreds ((AT0_PROC2_SW_A_B_TAU)) :extrapreds ((AT0_PROC3_C)) :extrapreds ((AT0_PROC3_B)) :extrapreds ((AT0_PROC3_A)) :extrapreds ((AT0_PROC3_SW_C_B_TAU)) :extrapreds ((AT0_PROC2_WAIT)) :extrapreds ((AT0_PROC1_SW_B_C_TAU)) :formula (flet ($cvcl_0 (not AT0_PROC1_A)) (flet ($cvcl_1 (not AT0_PROC1_B)) (flet ($cvcl_2 (not AT0_PROC1_C)) (flet ($cvcl_3 (not AT0_PROC1_CS)) (flet ($cvcl_4 (not AT1_PROC1_A)) (flet ($cvcl_5 (not AT1_PROC1_B)) (flet ($cvcl_6 (not AT1_PROC1_C)) (flet ($cvcl_7 (not AT1_PROC1_CS)) (flet ($cvcl_8 (not AT0_PROC2_A)) (flet ($cvcl_9 (not AT0_PROC2_B)) (flet ($cvcl_10 (not AT0_PROC2_C)) (flet ($cvcl_11 (not AT0_PROC2_CS)) (flet ($cvcl_12 (not AT1_PROC2_A)) (flet ($cvcl_13 (not AT1_PROC2_B)) (flet ($cvcl_14 (not AT1_PROC2_C)) (flet ($cvcl_15 (not AT1_PROC2_CS)) (flet ($cvcl_16 (not AT0_PROC3_A)) (flet ($cvcl_17 (not AT0_PROC3_B)) (flet ($cvcl_18 (not AT0_PROC3_C)) (flet ($cvcl_19 (not AT0_PROC3_CS)) (flet ($cvcl_20 (not AT1_PROC3_A)) (flet ($cvcl_21 (not AT1_PROC3_B)) (flet ($cvcl_22 (not AT1_PROC3_C)) (flet ($cvcl_23 (not AT1_PROC3_CS)) (flet ($cvcl_24 (= AT0_PROC1_X AT0_Z)) (flet ($cvcl_25 (> AT0_PROC1_X AT0_Z)) (flet ($cvcl_73 (not $cvcl_24)) (flet ($cvcl_26 (= AT1_PROC1_X AT1_Z)) (flet ($cvcl_27 (> AT1_PROC1_X AT1_Z)) (flet ($cvcl_72 (not $cvcl_26)) (flet ($cvcl_28 (= AT0_PROC2_X AT0_Z)) (flet ($cvcl_29 (> AT0_PROC2_X AT0_Z)) (flet ($cvcl_78 (not $cvcl_28)) (flet ($cvcl_30 (= AT1_PROC2_X AT1_Z)) (flet ($cvcl_31 (> AT1_PROC2_X AT1_Z)) (flet ($cvcl_77 (not $cvcl_30)) (flet ($cvcl_32 (= AT0_PROC3_X AT0_Z)) (flet ($cvcl_33 (> AT0_PROC3_X AT0_Z)) (flet ($cvcl_82 (not $cvcl_32)) (flet ($cvcl_34 (= AT1_PROC3_X AT1_Z)) (flet ($cvcl_35 (> AT1_PROC3_X AT1_Z)) (flet ($cvcl_81 (not $cvcl_34)) (flet ($cvcl_38 (<= (- AT0_PROC1_X AT0_Z) 10)) (flet ($cvcl_45 (<= (- AT0_PROC2_X AT0_Z) 10)) (flet ($cvcl_51 (<= (- AT0_PROC3_X AT0_Z) 10)) (flet ($cvcl_36 (not AT0_PROC1_SW_A_B_TAU)) (flet ($cvcl_37 (not AT0_PROC1_SW_B_C_TAU)) (flet ($cvcl_39 (not AT0_PROC1_SW_C_B_TAU)) (flet ($cvcl_40 (not AT0_PROC1_SW_C_CS_TAU)) (flet ($cvcl_56 (= AT1_PROC1_X AT0_PROC1_X)) (flet ($cvcl_41 (not AT0_PROC1_SW_CS_A_TAU)) (flet ($cvcl_42 (= AT1_Z AT0_Z)) (flet ($cvcl_43 (not AT0_PROC2_SW_A_B_TAU)) (flet ($cvcl_44 (not AT0_PROC2_SW_B_C_TAU)) (flet ($cvcl_46 (not AT0_PROC2_SW_C_B_TAU)) (flet ($cvcl_47 (not AT0_PROC2_SW_C_CS_TAU)) (flet ($cvcl_58 (= AT1_PROC2_X AT0_PROC2_X)) (flet ($cvcl_48 (not AT0_PROC2_SW_CS_A_TAU)) (flet ($cvcl_49 (not AT0_PROC3_SW_A_B_TAU)) (flet ($cvcl_50 (not AT0_PROC3_SW_B_C_TAU)) (flet ($cvcl_52 (not AT0_PROC3_SW_C_B_TAU)) (flet ($cvcl_53 (not AT0_PROC3_SW_C_CS_TAU)) (flet ($cvcl_60 (= AT1_PROC3_X AT0_PROC3_X)) (flet ($cvcl_54 (not AT0_PROC3_SW_CS_A_TAU)) (flet ($cvcl_55 (not AT0_PROC1_WAIT)) (flet ($cvcl_62 (not AT0_PROC1_TAU)) (flet ($cvcl_57 (not AT0_PROC2_WAIT)) (flet ($cvcl_63 (not AT0_PROC2_TAU)) (flet ($cvcl_59 (not AT0_PROC3_WAIT)) (flet ($cvcl_65 (not AT0_PROC3_TAU)) (flet ($cvcl_61 (not AT0_DELTA)) (flet ($cvcl_69 (< AT1_Z AT0_Z)) (flet ($cvcl_64 (or $cvcl_61 $cvcl_69 )) (flet ($cvcl_66 (< AT1_PROC1_X AT0_PROC1_X)) (flet ($cvcl_70 (not $cvcl_56)) (flet ($cvcl_67 (< AT1_PROC2_X AT0_PROC2_X)) (flet ($cvcl_76 (not $cvcl_58)) (flet ($cvcl_68 (< AT1_PROC3_X AT0_PROC3_X)) (flet ($cvcl_80 (not $cvcl_60)) (flet ($cvcl_71 (not $cvcl_42)) (flet ($cvcl_75 (not $cvcl_69)) (flet ($cvcl_74 (or $cvcl_73 $cvcl_70 )) (flet ($cvcl_79 (or $cvcl_78 $cvcl_76 )) (flet ($cvcl_83 (or $cvcl_82 $cvcl_80 )) (flet ($cvcl_84 (not AT0_ID0)) (flet ($cvcl_85 (not AT0_ID1)) (flet ($cvcl_86 (not AT0_ID2)) (flet ($cvcl_87 (not AT0_ID3)) (flet ($cvcl_88 (not AT1_ID0)) (flet ($cvcl_89 (not AT1_ID1)) (flet ($cvcl_90 (not AT1_ID2)) (flet ($cvcl_91 (not AT1_ID3)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (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_73 (not $cvcl_25) )) (or $cvcl_26 $cvcl_27 )) (or $cvcl_72 (not $cvcl_27) )) (or $cvcl_28 $cvcl_29 )) (or $cvcl_78 (not $cvcl_29) )) (or $cvcl_30 $cvcl_31 )) (or $cvcl_77 (not $cvcl_31) )) (or $cvcl_32 $cvcl_33 )) (or $cvcl_82 (not $cvcl_33) )) (or $cvcl_34 $cvcl_35 )) (or $cvcl_81 (not $cvcl_35) )) (or $cvcl_1 $cvcl_38 )) (or $cvcl_5 (<= (- AT1_PROC1_X AT1_Z) 10) )) (or $cvcl_9 $cvcl_45 )) (or $cvcl_13 (<= (- AT1_PROC2_X AT1_Z) 10) )) (or $cvcl_17 $cvcl_51 )) (or $cvcl_21 (<= (- AT1_PROC3_X AT1_Z) 10) )) (or (or (or (or (or (or AT0_PROC1_WAIT AT0_DELTA ) AT0_PROC1_SW_A_B_TAU ) AT0_PROC1_SW_B_C_TAU ) AT0_PROC1_SW_C_B_TAU ) AT0_PROC1_SW_C_CS_TAU ) AT0_PROC1_SW_CS_A_TAU )) (or (or (or (or (or (or AT0_PROC2_WAIT AT0_DELTA ) AT0_PROC2_SW_A_B_TAU ) AT0_PROC2_SW_B_C_TAU ) AT0_PROC2_SW_C_B_TAU ) AT0_PROC2_SW_C_CS_TAU ) AT0_PROC2_SW_CS_A_TAU )) (or (or (or (or (or (or AT0_PROC3_WAIT AT0_DELTA ) AT0_PROC3_SW_A_B_TAU ) AT0_PROC3_SW_B_C_TAU ) AT0_PROC3_SW_C_B_TAU ) AT0_PROC3_SW_C_CS_TAU ) AT0_PROC3_SW_CS_A_TAU )) (or $cvcl_36 AT0_PROC1_A )) (or $cvcl_36 AT0_PROC1_TAU )) (or $cvcl_36 AT1_PROC1_B )) (or $cvcl_36 $cvcl_26 )) (or $cvcl_37 AT0_PROC1_B )) (or $cvcl_37 AT0_PROC1_TAU )) (or $cvcl_37 AT1_PROC1_C )) (or $cvcl_37 $cvcl_38 )) (or $cvcl_37 $cvcl_26 )) (or $cvcl_39 AT0_PROC1_C )) (or $cvcl_39 AT0_PROC1_TAU )) (or $cvcl_39 AT1_PROC1_B )) (or $cvcl_39 $cvcl_26 )) (or $cvcl_40 AT0_PROC1_C )) (or $cvcl_40 AT0_PROC1_TAU )) (or $cvcl_40 AT1_PROC1_CS )) (or $cvcl_40 (> (- AT0_PROC1_X AT0_Z) 10) )) (or $cvcl_40 $cvcl_56 )) (or $cvcl_41 AT0_PROC1_CS )) (or $cvcl_41 AT0_PROC1_TAU )) (or $cvcl_41 AT1_PROC1_A )) (or $cvcl_41 $cvcl_26 )) (or $cvcl_36 $cvcl_42 )) (or $cvcl_37 $cvcl_42 )) (or $cvcl_39 $cvcl_42 )) (or $cvcl_40 $cvcl_42 )) (or $cvcl_41 $cvcl_42 )) (or $cvcl_43 AT0_PROC2_A )) (or $cvcl_43 AT0_PROC2_TAU )) (or $cvcl_43 AT1_PROC2_B )) (or $cvcl_43 $cvcl_30 )) (or $cvcl_44 AT0_PROC2_B )) (or $cvcl_44 AT0_PROC2_TAU )) (or $cvcl_44 AT1_PROC2_C )) (or $cvcl_44 $cvcl_45 )) (or $cvcl_44 $cvcl_30 )) (or $cvcl_46 AT0_PROC2_C )) (or $cvcl_46 AT0_PROC2_TAU )) (or $cvcl_46 AT1_PROC2_B )) (or $cvcl_46 $cvcl_30 )) (or $cvcl_47 AT0_PROC2_C )) (or $cvcl_47 AT0_PROC2_TAU )) (or $cvcl_47 AT1_PROC2_CS )) (or $cvcl_47 (> (- AT0_PROC2_X AT0_Z) 10) )) (or $cvcl_47 $cvcl_58 )) (or $cvcl_48 AT0_PROC2_CS )) (or $cvcl_48 AT0_PROC2_TAU )) (or $cvcl_48 AT1_PROC2_A )) (or $cvcl_48 $cvcl_30 )) (or $cvcl_43 $cvcl_42 )) (or $cvcl_44 $cvcl_42 )) (or $cvcl_46 $cvcl_42 )) (or $cvcl_47 $cvcl_42 )) (or $cvcl_48 $cvcl_42 )) (or $cvcl_49 AT0_PROC3_A )) (or $cvcl_49 AT0_PROC3_TAU )) (or $cvcl_49 AT1_PROC3_B )) (or $cvcl_49 $cvcl_34 )) (or $cvcl_50 AT0_PROC3_B )) (or $cvcl_50 AT0_PROC3_TAU )) (or $cvcl_50 AT1_PROC3_C )) (or $cvcl_50 $cvcl_51 )) (or $cvcl_50 $cvcl_34 )) (or $cvcl_52 AT0_PROC3_C )) (or $cvcl_52 AT0_PROC3_TAU )) (or $cvcl_52 AT1_PROC3_B )) (or $cvcl_52 $cvcl_34 )) (or $cvcl_53 AT0_PROC3_C )) (or $cvcl_53 AT0_PROC3_TAU )) (or $cvcl_53 AT1_PROC3_CS )) (or $cvcl_53 (> (- AT0_PROC3_X AT0_Z) 10) )) (or $cvcl_53 $cvcl_60 )) (or $cvcl_54 AT0_PROC3_CS )) (or $cvcl_54 AT0_PROC3_TAU )) (or $cvcl_54 AT1_PROC3_A )) (or $cvcl_54 $cvcl_34 )) (or $cvcl_49 $cvcl_42 )) (or $cvcl_50 $cvcl_42 )) (or $cvcl_52 $cvcl_42 )) (or $cvcl_53 $cvcl_42 )) (or $cvcl_54 $cvcl_42 )) (or (or $cvcl_55 $cvcl_0 ) AT1_PROC1_A )) (or (or $cvcl_55 AT0_PROC1_A ) $cvcl_4 )) (or (or $cvcl_55 $cvcl_1 ) AT1_PROC1_B )) (or (or $cvcl_55 AT0_PROC1_B ) $cvcl_5 )) (or (or $cvcl_55 $cvcl_2 ) AT1_PROC1_C )) (or (or $cvcl_55 AT0_PROC1_C ) $cvcl_6 )) (or (or $cvcl_55 $cvcl_3 ) AT1_PROC1_CS )) (or (or $cvcl_55 AT0_PROC1_CS ) $cvcl_7 )) (or $cvcl_55 $cvcl_62 )) (or $cvcl_55 $cvcl_56 )) (or $cvcl_55 $cvcl_42 )) (or (or $cvcl_57 $cvcl_8 ) AT1_PROC2_A )) (or (or $cvcl_57 AT0_PROC2_A ) $cvcl_12 )) (or (or $cvcl_57 $cvcl_9 ) AT1_PROC2_B )) (or (or $cvcl_57 AT0_PROC2_B ) $cvcl_13 )) (or (or $cvcl_57 $cvcl_10 ) AT1_PROC2_C )) (or (or $cvcl_57 AT0_PROC2_C ) $cvcl_14 )) (or (or $cvcl_57 $cvcl_11 ) AT1_PROC2_CS )) (or (or $cvcl_57 AT0_PROC2_CS ) $cvcl_15 )) (or $cvcl_57 $cvcl_63 )) (or $cvcl_57 $cvcl_58 )) (or $cvcl_57 $cvcl_42 )) (or (or $cvcl_59 $cvcl_16 ) AT1_PROC3_A )) (or (or $cvcl_59 AT0_PROC3_A ) $cvcl_20 )) (or (or $cvcl_59 $cvcl_17 ) AT1_PROC3_B )) (or (or $cvcl_59 AT0_PROC3_B ) $cvcl_21 )) (or (or $cvcl_59 $cvcl_18 ) AT1_PROC3_C )) (or (or $cvcl_59 AT0_PROC3_C ) $cvcl_22 )) (or (or $cvcl_59 $cvcl_19 ) AT1_PROC3_CS )) (or (or $cvcl_59 AT0_PROC3_CS ) $cvcl_23 )) (or $cvcl_59 $cvcl_65 )) (or $cvcl_59 $cvcl_60 )) (or $cvcl_59 $cvcl_42 )) (or (or $cvcl_61 $cvcl_0 ) AT1_PROC1_A )) (or (or $cvcl_61 AT0_PROC1_A ) $cvcl_4 )) (or (or $cvcl_61 $cvcl_1 ) AT1_PROC1_B )) (or (or $cvcl_61 AT0_PROC1_B ) $cvcl_5 )) (or (or $cvcl_61 $cvcl_2 ) AT1_PROC1_C )) (or (or $cvcl_61 AT0_PROC1_C ) $cvcl_6 )) (or (or $cvcl_61 $cvcl_3 ) AT1_PROC1_CS )) (or (or $cvcl_61 AT0_PROC1_CS ) $cvcl_7 )) (or $cvcl_61 $cvcl_56 )) (or $cvcl_61 $cvcl_62 )) $cvcl_64) (or (or $cvcl_61 $cvcl_8 ) AT1_PROC2_A )) (or (or $cvcl_61 AT0_PROC2_A ) $cvcl_12 )) (or (or $cvcl_61 $cvcl_9 ) AT1_PROC2_B )) (or (or $cvcl_61 AT0_PROC2_B ) $cvcl_13 )) (or (or $cvcl_61 $cvcl_10 ) AT1_PROC2_C )) (or (or $cvcl_61 AT0_PROC2_C ) $cvcl_14 )) (or (or $cvcl_61 $cvcl_11 ) AT1_PROC2_CS )) (or (or $cvcl_61 AT0_PROC2_CS ) $cvcl_15 )) (or $cvcl_61 $cvcl_58 )) (or $cvcl_61 $cvcl_63 )) $cvcl_64) (or (or $cvcl_61 $cvcl_16 ) AT1_PROC3_A )) (or (or $cvcl_61 AT0_PROC3_A ) $cvcl_20 )) (or (or $cvcl_61 $cvcl_17 ) AT1_PROC3_B )) (or (or $cvcl_61 AT0_PROC3_B ) $cvcl_21 )) (or (or $cvcl_61 $cvcl_18 ) AT1_PROC3_C )) (or (or $cvcl_61 AT0_PROC3_C ) $cvcl_22 )) (or (or $cvcl_61 $cvcl_19 ) AT1_PROC3_CS )) (or (or $cvcl_61 AT0_PROC3_CS ) $cvcl_23 )) (or $cvcl_61 $cvcl_60 )) (or $cvcl_61 $cvcl_65 )) $cvcl_64) (or $cvcl_56 $cvcl_66 )) (or $cvcl_70 (not $cvcl_66) )) (or $cvcl_58 $cvcl_67 )) (or $cvcl_76 (not $cvcl_67) )) (or $cvcl_60 $cvcl_68 )) (or $cvcl_80 (not $cvcl_68) )) (or $cvcl_42 $cvcl_69 )) (or $cvcl_71 $cvcl_75 )) (or (or (or $cvcl_24 $cvcl_70 ) $cvcl_71 ) $cvcl_72 )) (or (or (or $cvcl_73 $cvcl_56 ) $cvcl_71 ) $cvcl_72 )) (or (or $cvcl_74 $cvcl_42 ) $cvcl_72 )) (or (or $cvcl_74 $cvcl_71 ) $cvcl_26 )) (or (or (or (not (< AT0_Z AT0_PROC1_X)) $cvcl_70 ) $cvcl_75 ) (< AT1_Z AT1_PROC1_X) )) (or (or (or $cvcl_28 $cvcl_76 ) $cvcl_71 ) $cvcl_77 )) (or (or (or $cvcl_78 $cvcl_58 ) $cvcl_71 ) $cvcl_77 )) (or (or $cvcl_79 $cvcl_42 ) $cvcl_77 )) (or (or $cvcl_79 $cvcl_71 ) $cvcl_30 )) (or (or (or (not (< AT0_Z AT0_PROC2_X)) $cvcl_76 ) $cvcl_75 ) (< AT1_Z AT1_PROC2_X) )) (or (or (or $cvcl_32 $cvcl_80 ) $cvcl_71 ) $cvcl_81 )) (or (or (or $cvcl_82 $cvcl_60 ) $cvcl_71 ) $cvcl_81 )) (or (or $cvcl_83 $cvcl_42 ) $cvcl_81 )) (or (or $cvcl_83 $cvcl_71 ) $cvcl_34 )) (or (or (or (not (< AT0_Z AT0_PROC3_X)) $cvcl_80 ) $cvcl_75 ) (< AT1_Z AT1_PROC3_X) )) AT0_PROC1_A) AT0_PROC2_A) AT0_PROC3_A) $cvcl_24) $cvcl_28) $cvcl_32) AT0_ID0) (or (or $cvcl_55 $cvcl_57 ) $cvcl_59 )) (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_36 AT0_ID0 )) (or $cvcl_36 AT1_ID0 )) (or $cvcl_37 AT1_ID1 )) (or $cvcl_39 AT0_ID0 )) (or $cvcl_39 AT1_ID0 )) (or $cvcl_40 AT0_ID1 )) (or $cvcl_40 AT1_ID1 )) (or $cvcl_41 AT1_ID0 )) (or (or $cvcl_61 $cvcl_85 ) AT1_ID1 )) (or $cvcl_43 AT0_ID0 )) (or $cvcl_43 AT1_ID0 )) (or $cvcl_44 AT1_ID2 )) (or $cvcl_46 AT0_ID0 )) (or $cvcl_46 AT1_ID0 )) (or $cvcl_47 AT0_ID2 )) (or $cvcl_47 AT1_ID2 )) (or $cvcl_48 AT1_ID0 )) (or (or $cvcl_61 $cvcl_86 ) AT1_ID2 )) (or $cvcl_49 AT0_ID0 )) (or $cvcl_49 AT1_ID0 )) (or $cvcl_50 AT1_ID3 )) (or $cvcl_52 AT0_ID0 )) (or $cvcl_52 AT1_ID0 )) (or $cvcl_53 AT0_ID3 )) (or $cvcl_53 AT1_ID3 )) (or $cvcl_54 AT1_ID0 )) (or (or $cvcl_61 $cvcl_87 ) AT1_ID3 )) (or (or $cvcl_61 $cvcl_84 ) AT1_ID0 )) (or $cvcl_4 AT1_PROC1_A )) (or AT1_PROC1_A $cvcl_4 )) (or $cvcl_5 AT1_PROC1_B )) (or AT1_PROC1_B $cvcl_5 )) (or $cvcl_6 AT1_PROC1_C )) (or AT1_PROC1_C $cvcl_6 )) (or $cvcl_7 AT1_PROC1_CS )) (or AT1_PROC1_CS $cvcl_7 )) (or $cvcl_89 AT1_ID1 )) (or AT1_ID1 $cvcl_89 )) (= (- AT1_PROC1_X AT1_Z) (- AT1_PROC1_X AT1_Z))) (or $cvcl_12 AT1_PROC2_A )) (or AT1_PROC2_A $cvcl_12 )) (or $cvcl_13 AT1_PROC2_B )) (or AT1_PROC2_B $cvcl_13 )) (or $cvcl_14 AT1_PROC2_C )) (or AT1_PROC2_C $cvcl_14 )) (or $cvcl_15 AT1_PROC2_CS )) (or AT1_PROC2_CS $cvcl_15 )) (or $cvcl_90 AT1_ID2 )) (or AT1_ID2 $cvcl_90 )) (= (- AT1_PROC2_X AT1_Z) (- AT1_PROC2_X AT1_Z))) (or $cvcl_20 AT1_PROC3_A )) (or AT1_PROC3_A $cvcl_20 )) (or $cvcl_21 AT1_PROC3_B )) (or AT1_PROC3_B $cvcl_21 )) (or $cvcl_22 AT1_PROC3_C )) (or AT1_PROC3_C $cvcl_22 )) (or $cvcl_23 AT1_PROC3_CS )) (or AT1_PROC3_CS $cvcl_23 )) (or $cvcl_91 AT1_ID3 )) (or AT1_ID3 $cvcl_91 )) (= (- AT1_PROC3_X AT1_Z) (- AT1_PROC3_X AT1_Z))) AT1_PROC1_B) $cvcl_7))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )