(benchmark FISCHER4_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 ((AT0_ID4))
:extrapreds ((AT1_PROC2_CS))
:extrafuns ((AT0_PROC4_X Int))
:extrapreds ((AT0_PROC3_TAU))
:extrapreds ((AT0_PROC2_SW_C_B_TAU))
:extrapreds ((AT0_PROC4_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 ((AT0_PROC4_C))
:extrapreds ((AT0_PROC4_B))
:extrapreds ((AT1_ID0))
:extrapreds ((AT0_PROC4_A))
:extrapreds ((AT1_ID1))
:extrapreds ((AT1_ID2))
:extrapreds ((AT1_ID3))
:extrapreds ((AT1_ID4))
:extrapreds ((AT0_PROC1_SW_CS_A_TAU))
:extrapreds ((AT0_PROC4_TAU))
:extrafuns ((AT0_PROC2_X Int))
:extrapreds ((AT1_PROC3_CS))
:extrapreds ((AT0_PROC4_SW_A_B_TAU))
:extrapreds ((AT1_PROC3_C))
:extrapreds ((AT1_PROC3_B))
:extrapreds ((AT1_PROC3_A))
:extrafuns ((AT1_PROC1_X Int))
:extrafuns ((AT1_Z Int))
:extrapreds ((AT0_PROC4_SW_B_C_TAU))
:extrapreds ((AT0_PROC2_C))
:extrapreds ((AT0_PROC2_SW_C_CS_TAU))
:extrapreds ((AT0_PROC2_B))
:extrapreds ((AT0_PROC2_A))
:extrapreds ((AT0_PROC3_SW_B_C_TAU))
:extrapreds ((AT0_PROC1_SW_C_B_TAU))
:extrapreds ((AT0_PROC1_CS))
:extrapreds ((AT0_PROC4_WAIT))
:extrapreds ((AT0_PROC1_TAU))
:extrapreds ((AT0_PROC1_SW_C_CS_TAU))
:extrafuns ((AT1_PROC4_X Int))
:extrapreds ((AT0_PROC4_SW_CS_A_TAU))
:extrapreds ((AT0_PROC1_WAIT))
:extrapreds ((AT0_PROC4_CS))
:extrapreds ((AT1_PROC1_C))
:extrapreds ((AT1_PROC1_B))
:extrapreds ((AT1_PROC4_CS))
:extrapreds ((AT1_PROC1_A))
:extrapreds ((AT0_PROC3_SW_A_B_TAU))
:extrapreds ((AT0_DELTA))
:extrafuns ((AT0_PROC3_X Int))
:extrapreds ((AT0_PROC2_SW_B_C_TAU))
:extrapreds ((AT1_PROC4_C))
:extrapreds ((AT1_PROC1_CS))
:extrapreds ((AT1_PROC4_B))
:extrapreds ((AT1_PROC4_A))
: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))
:extrapreds ((AT0_PROC4_SW_C_CS_TAU))
: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 (not AT0_PROC4_A)) (flet ($cvcl_25 (not AT0_PROC4_B)) (flet ($cvcl_26 (not AT0_PROC4_C)) (flet ($cvcl_27 (not AT0_PROC4_CS)) (flet ($cvcl_28 (not AT1_PROC4_A)) (flet ($cvcl_29 (not AT1_PROC4_B)) (flet ($cvcl_30 (not AT1_PROC4_C)) (flet ($cvcl_31 (not AT1_PROC4_CS)) (flet ($cvcl_32 (= AT0_PROC1_X AT0_Z)) (flet ($cvcl_33 (> AT0_PROC1_X AT0_Z)) (flet ($cvcl_95 (not $cvcl_32)) (flet ($cvcl_34 (= AT1_PROC1_X AT1_Z)) (flet ($cvcl_35 (> AT1_PROC1_X AT1_Z)) (flet ($cvcl_94 (not $cvcl_34)) (flet ($cvcl_36 (= AT0_PROC2_X AT0_Z)) (flet ($cvcl_37 (> AT0_PROC2_X AT0_Z)) (flet ($cvcl_100 (not $cvcl_36)) (flet ($cvcl_38 (= AT1_PROC2_X AT1_Z)) (flet ($cvcl_39 (> AT1_PROC2_X AT1_Z)) (flet ($cvcl_99 (not $cvcl_38)) (flet ($cvcl_40 (= AT0_PROC3_X AT0_Z)) (flet ($cvcl_41 (> AT0_PROC3_X AT0_Z)) (flet ($cvcl_104 (not $cvcl_40)) (flet ($cvcl_42 (= AT1_PROC3_X AT1_Z)) (flet ($cvcl_43 (> AT1_PROC3_X AT1_Z)) (flet ($cvcl_103 (not $cvcl_42)) (flet ($cvcl_44 (= AT0_PROC4_X AT0_Z)) (flet ($cvcl_45 (> AT0_PROC4_X AT0_Z)) (flet ($cvcl_108 (not $cvcl_44)) (flet ($cvcl_46 (= AT1_PROC4_X AT1_Z)) (flet ($cvcl_47 (> AT1_PROC4_X AT1_Z)) (flet ($cvcl_107 (not $cvcl_46)) (flet ($cvcl_50 (<= (- AT0_PROC1_X AT0_Z) 10)) (flet ($cvcl_57 (<= (- AT0_PROC2_X AT0_Z) 10)) (flet ($cvcl_63 (<= (- AT0_PROC3_X AT0_Z) 10)) (flet ($cvcl_69 (<= (- AT0_PROC4_X AT0_Z) 10)) (flet ($cvcl_48 (not AT0_PROC1_SW_A_B_TAU)) (flet ($cvcl_49 (not AT0_PROC1_SW_B_C_TAU)) (flet ($cvcl_51 (not AT0_PROC1_SW_C_B_TAU)) (flet ($cvcl_52 (not AT0_PROC1_SW_C_CS_TAU)) (flet ($cvcl_74 (= AT1_PROC1_X AT0_PROC1_X)) (flet ($cvcl_53 (not AT0_PROC1_SW_CS_A_TAU)) (flet ($cvcl_54 (= AT1_Z AT0_Z)) (flet ($cvcl_55 (not AT0_PROC2_SW_A_B_TAU)) (flet ($cvcl_56 (not AT0_PROC2_SW_B_C_TAU)) (flet ($cvcl_58 (not AT0_PROC2_SW_C_B_TAU)) (flet ($cvcl_59 (not AT0_PROC2_SW_C_CS_TAU)) (flet ($cvcl_76 (= AT1_PROC2_X AT0_PROC2_X)) (flet ($cvcl_60 (not AT0_PROC2_SW_CS_A_TAU)) (flet ($cvcl_61 (not AT0_PROC3_SW_A_B_TAU)) (flet ($cvcl_62 (not AT0_PROC3_SW_B_C_TAU)) (flet ($cvcl_64 (not AT0_PROC3_SW_C_B_TAU)) (flet ($cvcl_65 (not AT0_PROC3_SW_C_CS_TAU)) (flet ($cvcl_78 (= AT1_PROC3_X AT0_PROC3_X)) (flet ($cvcl_66 (not AT0_PROC3_SW_CS_A_TAU)) (flet ($cvcl_67 (not AT0_PROC4_SW_A_B_TAU)) (flet ($cvcl_68 (not AT0_PROC4_SW_B_C_TAU)) (flet ($cvcl_70 (not AT0_PROC4_SW_C_B_TAU)) (flet ($cvcl_71 (not AT0_PROC4_SW_C_CS_TAU)) (flet ($cvcl_80 (= AT1_PROC4_X AT0_PROC4_X)) (flet ($cvcl_72 (not AT0_PROC4_SW_CS_A_TAU)) (flet ($cvcl_73 (not AT0_PROC1_WAIT)) (flet ($cvcl_82 (not AT0_PROC1_TAU)) (flet ($cvcl_75 (not AT0_PROC2_WAIT)) (flet ($cvcl_83 (not AT0_PROC2_TAU)) (flet ($cvcl_77 (not AT0_PROC3_WAIT)) (flet ($cvcl_85 (not AT0_PROC3_TAU)) (flet ($cvcl_79 (not AT0_PROC4_WAIT)) (flet ($cvcl_86 (not AT0_PROC4_TAU)) (flet ($cvcl_81 (not AT0_DELTA)) (flet ($cvcl_91 (< AT1_Z AT0_Z)) (flet ($cvcl_84 (or $cvcl_81 $cvcl_91 )) (flet ($cvcl_87 (< AT1_PROC1_X AT0_PROC1_X)) (flet ($cvcl_92 (not $cvcl_74)) (flet ($cvcl_88 (< AT1_PROC2_X AT0_PROC2_X)) (flet ($cvcl_98 (not $cvcl_76)) (flet ($cvcl_89 (< AT1_PROC3_X AT0_PROC3_X)) (flet ($cvcl_102 (not $cvcl_78)) (flet ($cvcl_90 (< AT1_PROC4_X AT0_PROC4_X)) (flet ($cvcl_106 (not $cvcl_80)) (flet ($cvcl_93 (not $cvcl_54)) (flet ($cvcl_97 (not $cvcl_91)) (flet ($cvcl_96 (or $cvcl_95 $cvcl_92 )) (flet ($cvcl_101 (or $cvcl_100 $cvcl_98 )) (flet ($cvcl_105 (or $cvcl_104 $cvcl_102 )) (flet ($cvcl_109 (or $cvcl_108 $cvcl_106 )) (flet ($cvcl_110 (not AT0_ID0)) (flet ($cvcl_111 (not AT0_ID1)) (flet ($cvcl_112 (not AT0_ID2)) (flet ($cvcl_113 (not AT0_ID3)) (flet ($cvcl_114 (not AT0_ID4)) (flet ($cvcl_115 (not AT1_ID0)) (flet ($cvcl_116 (not AT1_ID1)) (flet ($cvcl_117 (not AT1_ID2)) (flet ($cvcl_118 (not AT1_ID3)) (flet ($cvcl_119 (not AT1_ID4)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (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_95 (not $cvcl_33) )) (or $cvcl_34 $cvcl_35 )) (or $cvcl_94 (not $cvcl_35) )) (or $cvcl_36 $cvcl_37 )) (or $cvcl_100 (not $cvcl_37) )) (or $cvcl_38 $cvcl_39 )) (or $cvcl_99 (not $cvcl_39) )) (or $cvcl_40 $cvcl_41 )) (or $cvcl_104 (not $cvcl_41) )) (or $cvcl_42 $cvcl_43 )) (or $cvcl_103 (not $cvcl_43) )) (or $cvcl_44 $cvcl_45 )) (or $cvcl_108 (not $cvcl_45) )) (or $cvcl_46 $cvcl_47 )) (or $cvcl_107 (not $cvcl_47) )) (or $cvcl_1 $cvcl_50 )) (or $cvcl_5 (<= (- AT1_PROC1_X AT1_Z) 10) )) (or $cvcl_9 $cvcl_57 )) (or $cvcl_13 (<= (- AT1_PROC2_X AT1_Z) 10) )) (or $cvcl_17 $cvcl_63 )) (or $cvcl_21 (<= (- AT1_PROC3_X AT1_Z) 10) )) (or $cvcl_25 $cvcl_69 )) (or $cvcl_29 (<= (- AT1_PROC4_X AT1_Z) 10) )) (or (or (or (or (or (or AT0_PROC1_WAIT AT0_DELTA ) AT0_PROC1_SW_A_B_TAU ) AT0_PROC1_SW_B_C_TAU ) AT0_PROC1_SW_C_B_TAU ) AT0_PROC1_SW_C_CS_TAU ) AT0_PROC1_SW_CS_A_TAU )) (or (or (or (or (or (or AT0_PROC2_WAIT AT0_DELTA ) AT0_PROC2_SW_A_B_TAU ) AT0_PROC2_SW_B_C_TAU ) AT0_PROC2_SW_C_B_TAU ) AT0_PROC2_SW_C_CS_TAU ) AT0_PROC2_SW_CS_A_TAU )) (or (or (or (or (or (or AT0_PROC3_WAIT AT0_DELTA ) AT0_PROC3_SW_A_B_TAU ) AT0_PROC3_SW_B_C_TAU ) AT0_PROC3_SW_C_B_TAU ) AT0_PROC3_SW_C_CS_TAU ) AT0_PROC3_SW_CS_A_TAU )) (or (or (or (or (or (or AT0_PROC4_WAIT AT0_DELTA ) AT0_PROC4_SW_A_B_TAU ) AT0_PROC4_SW_B_C_TAU ) AT0_PROC4_SW_C_B_TAU ) AT0_PROC4_SW_C_CS_TAU ) AT0_PROC4_SW_CS_A_TAU )) (or $cvcl_48 AT0_PROC1_A )) (or $cvcl_48 AT0_PROC1_TAU )) (or $cvcl_48 AT1_PROC1_B )) (or $cvcl_48 $cvcl_34 )) (or $cvcl_49 AT0_PROC1_B )) (or $cvcl_49 AT0_PROC1_TAU )) (or $cvcl_49 AT1_PROC1_C )) (or $cvcl_49 $cvcl_50 )) (or $cvcl_49 $cvcl_34 )) (or $cvcl_51 AT0_PROC1_C )) (or $cvcl_51 AT0_PROC1_TAU )) (or $cvcl_51 AT1_PROC1_B )) (or $cvcl_51 $cvcl_34 )) (or $cvcl_52 AT0_PROC1_C )) (or $cvcl_52 AT0_PROC1_TAU )) (or $cvcl_52 AT1_PROC1_CS )) (or $cvcl_52 (> (- AT0_PROC1_X AT0_Z) 10) )) (or $cvcl_52 $cvcl_74 )) (or $cvcl_53 AT0_PROC1_CS )) (or $cvcl_53 AT0_PROC1_TAU )) (or $cvcl_53 AT1_PROC1_A )) (or $cvcl_53 $cvcl_34 )) (or $cvcl_48 $cvcl_54 )) (or $cvcl_49 $cvcl_54 )) (or $cvcl_51 $cvcl_54 )) (or $cvcl_52 $cvcl_54 )) (or $cvcl_53 $cvcl_54 )) (or $cvcl_55 AT0_PROC2_A )) (or $cvcl_55 AT0_PROC2_TAU )) (or $cvcl_55 AT1_PROC2_B )) (or $cvcl_55 $cvcl_38 )) (or $cvcl_56 AT0_PROC2_B )) (or $cvcl_56 AT0_PROC2_TAU )) (or $cvcl_56 AT1_PROC2_C )) (or $cvcl_56 $cvcl_57 )) (or $cvcl_56 $cvcl_38 )) (or $cvcl_58 AT0_PROC2_C )) (or $cvcl_58 AT0_PROC2_TAU )) (or $cvcl_58 AT1_PROC2_B )) (or $cvcl_58 $cvcl_38 )) (or $cvcl_59 AT0_PROC2_C )) (or $cvcl_59 AT0_PROC2_TAU )) (or $cvcl_59 AT1_PROC2_CS )) (or $cvcl_59 (> (- AT0_PROC2_X AT0_Z) 10) )) (or $cvcl_59 $cvcl_76 )) (or $cvcl_60 AT0_PROC2_CS )) (or $cvcl_60 AT0_PROC2_TAU )) (or $cvcl_60 AT1_PROC2_A )) (or $cvcl_60 $cvcl_38 )) (or $cvcl_55 $cvcl_54 )) (or $cvcl_56 $cvcl_54 )) (or $cvcl_58 $cvcl_54 )) (or $cvcl_59 $cvcl_54 )) (or $cvcl_60 $cvcl_54 )) (or $cvcl_61 AT0_PROC3_A )) (or $cvcl_61 AT0_PROC3_TAU )) (or $cvcl_61 AT1_PROC3_B )) (or $cvcl_61 $cvcl_42 )) (or $cvcl_62 AT0_PROC3_B )) (or $cvcl_62 AT0_PROC3_TAU )) (or $cvcl_62 AT1_PROC3_C )) (or $cvcl_62 $cvcl_63 )) (or $cvcl_62 $cvcl_42 )) (or $cvcl_64 AT0_PROC3_C )) (or $cvcl_64 AT0_PROC3_TAU )) (or $cvcl_64 AT1_PROC3_B )) (or $cvcl_64 $cvcl_42 )) (or $cvcl_65 AT0_PROC3_C )) (or $cvcl_65 AT0_PROC3_TAU )) (or $cvcl_65 AT1_PROC3_CS )) (or $cvcl_65 (> (- AT0_PROC3_X AT0_Z) 10) )) (or $cvcl_65 $cvcl_78 )) (or $cvcl_66 AT0_PROC3_CS )) (or $cvcl_66 AT0_PROC3_TAU )) (or $cvcl_66 AT1_PROC3_A )) (or $cvcl_66 $cvcl_42 )) (or $cvcl_61 $cvcl_54 )) (or $cvcl_62 $cvcl_54 )) (or $cvcl_64 $cvcl_54 )) (or $cvcl_65 $cvcl_54 )) (or $cvcl_66 $cvcl_54 )) (or $cvcl_67 AT0_PROC4_A )) (or $cvcl_67 AT0_PROC4_TAU )) (or $cvcl_67 AT1_PROC4_B )) (or $cvcl_67 $cvcl_46 )) (or $cvcl_68 AT0_PROC4_B )) (or $cvcl_68 AT0_PROC4_TAU )) (or $cvcl_68 AT1_PROC4_C )) (or $cvcl_68 $cvcl_69 )) (or $cvcl_68 $cvcl_46 )) (or $cvcl_70 AT0_PROC4_C )) (or $cvcl_70 AT0_PROC4_TAU )) (or $cvcl_70 AT1_PROC4_B )) (or $cvcl_70 $cvcl_46 )) (or $cvcl_71 AT0_PROC4_C )) (or $cvcl_71 AT0_PROC4_TAU )) (or $cvcl_71 AT1_PROC4_CS )) (or $cvcl_71 (> (- AT0_PROC4_X AT0_Z) 10) )) (or $cvcl_71 $cvcl_80 )) (or $cvcl_72 AT0_PROC4_CS )) (or $cvcl_72 AT0_PROC4_TAU )) (or $cvcl_72 AT1_PROC4_A )) (or $cvcl_72 $cvcl_46 )) (or $cvcl_67 $cvcl_54 )) (or $cvcl_68 $cvcl_54 )) (or $cvcl_70 $cvcl_54 )) (or $cvcl_71 $cvcl_54 )) (or $cvcl_72 $cvcl_54 )) (or (or $cvcl_73 $cvcl_0 ) AT1_PROC1_A )) (or (or $cvcl_73 AT0_PROC1_A ) $cvcl_4 )) (or (or $cvcl_73 $cvcl_1 ) AT1_PROC1_B )) (or (or $cvcl_73 AT0_PROC1_B ) $cvcl_5 )) (or (or $cvcl_73 $cvcl_2 ) AT1_PROC1_C )) (or (or $cvcl_73 AT0_PROC1_C ) $cvcl_6 )) (or (or $cvcl_73 $cvcl_3 ) AT1_PROC1_CS )) (or (or $cvcl_73 AT0_PROC1_CS ) $cvcl_7 )) (or $cvcl_73 $cvcl_82 )) (or $cvcl_73 $cvcl_74 )) (or $cvcl_73 $cvcl_54 )) (or (or $cvcl_75 $cvcl_8 ) AT1_PROC2_A )) (or (or $cvcl_75 AT0_PROC2_A ) $cvcl_12 )) (or (or $cvcl_75 $cvcl_9 ) AT1_PROC2_B )) (or (or $cvcl_75 AT0_PROC2_B ) $cvcl_13 )) (or (or $cvcl_75 $cvcl_10 ) AT1_PROC2_C )) (or (or $cvcl_75 AT0_PROC2_C ) $cvcl_14 )) (or (or $cvcl_75 $cvcl_11 ) AT1_PROC2_CS )) (or (or $cvcl_75 AT0_PROC2_CS ) $cvcl_15 )) (or $cvcl_75 $cvcl_83 )) (or $cvcl_75 $cvcl_76 )) (or $cvcl_75 $cvcl_54 )) (or (or $cvcl_77 $cvcl_16 ) AT1_PROC3_A )) (or (or $cvcl_77 AT0_PROC3_A ) $cvcl_20 )) (or (or $cvcl_77 $cvcl_17 ) AT1_PROC3_B )) (or (or $cvcl_77 AT0_PROC3_B ) $cvcl_21 )) (or (or $cvcl_77 $cvcl_18 ) AT1_PROC3_C )) (or (or $cvcl_77 AT0_PROC3_C ) $cvcl_22 )) (or (or $cvcl_77 $cvcl_19 ) AT1_PROC3_CS )) (or (or $cvcl_77 AT0_PROC3_CS ) $cvcl_23 )) (or $cvcl_77 $cvcl_85 )) (or $cvcl_77 $cvcl_78 )) (or $cvcl_77 $cvcl_54 )) (or (or $cvcl_79 $cvcl_24 ) AT1_PROC4_A )) (or (or $cvcl_79 AT0_PROC4_A ) $cvcl_28 )) (or (or $cvcl_79 $cvcl_25 ) AT1_PROC4_B )) (or (or $cvcl_79 AT0_PROC4_B ) $cvcl_29 )) (or (or $cvcl_79 $cvcl_26 ) AT1_PROC4_C )) (or (or $cvcl_79 AT0_PROC4_C ) $cvcl_30 )) (or (or $cvcl_79 $cvcl_27 ) AT1_PROC4_CS )) (or (or $cvcl_79 AT0_PROC4_CS ) $cvcl_31 )) (or $cvcl_79 $cvcl_86 )) (or $cvcl_79 $cvcl_80 )) (or $cvcl_79 $cvcl_54 )) (or (or $cvcl_81 $cvcl_0 ) AT1_PROC1_A )) (or (or $cvcl_81 AT0_PROC1_A ) $cvcl_4 )) (or (or $cvcl_81 $cvcl_1 ) AT1_PROC1_B )) (or (or $cvcl_81 AT0_PROC1_B ) $cvcl_5 )) (or (or $cvcl_81 $cvcl_2 ) AT1_PROC1_C )) (or (or $cvcl_81 AT0_PROC1_C ) $cvcl_6 )) (or (or $cvcl_81 $cvcl_3 ) AT1_PROC1_CS )) (or (or $cvcl_81 AT0_PROC1_CS ) $cvcl_7 )) (or $cvcl_81 $cvcl_74 )) (or $cvcl_81 $cvcl_82 )) $cvcl_84) (or (or $cvcl_81 $cvcl_8 ) AT1_PROC2_A )) (or (or $cvcl_81 AT0_PROC2_A ) $cvcl_12 )) (or (or $cvcl_81 $cvcl_9 ) AT1_PROC2_B )) (or (or $cvcl_81 AT0_PROC2_B ) $cvcl_13 )) (or (or $cvcl_81 $cvcl_10 ) AT1_PROC2_C )) (or (or $cvcl_81 AT0_PROC2_C ) $cvcl_14 )) (or (or $cvcl_81 $cvcl_11 ) AT1_PROC2_CS )) (or (or $cvcl_81 AT0_PROC2_CS ) $cvcl_15 )) (or $cvcl_81 $cvcl_76 )) (or $cvcl_81 $cvcl_83 )) $cvcl_84) (or (or $cvcl_81 $cvcl_16 ) AT1_PROC3_A )) (or (or $cvcl_81 AT0_PROC3_A ) $cvcl_20 )) (or (or $cvcl_81 $cvcl_17 ) AT1_PROC3_B )) (or (or $cvcl_81 AT0_PROC3_B ) $cvcl_21 )) (or (or $cvcl_81 $cvcl_18 ) AT1_PROC3_C )) (or (or $cvcl_81 AT0_PROC3_C ) $cvcl_22 )) (or (or $cvcl_81 $cvcl_19 ) AT1_PROC3_CS )) (or (or $cvcl_81 AT0_PROC3_CS ) $cvcl_23 )) (or $cvcl_81 $cvcl_78 )) (or $cvcl_81 $cvcl_85 )) $cvcl_84) (or (or $cvcl_81 $cvcl_24 ) AT1_PROC4_A )) (or (or $cvcl_81 AT0_PROC4_A ) $cvcl_28 )) (or (or $cvcl_81 $cvcl_25 ) AT1_PROC4_B )) (or (or $cvcl_81 AT0_PROC4_B ) $cvcl_29 )) (or (or $cvcl_81 $cvcl_26 ) AT1_PROC4_C )) (or (or $cvcl_81 AT0_PROC4_C ) $cvcl_30 )) (or (or $cvcl_81 $cvcl_27 ) AT1_PROC4_CS )) (or (or $cvcl_81 AT0_PROC4_CS ) $cvcl_31 )) (or $cvcl_81 $cvcl_80 )) (or $cvcl_81 $cvcl_86 )) $cvcl_84) (or $cvcl_74 $cvcl_87 )) (or $cvcl_92 (not $cvcl_87) )) (or $cvcl_76 $cvcl_88 )) (or $cvcl_98 (not $cvcl_88) )) (or $cvcl_78 $cvcl_89 )) (or $cvcl_102 (not $cvcl_89) )) (or $cvcl_80 $cvcl_90 )) (or $cvcl_106 (not $cvcl_90) )) (or $cvcl_54 $cvcl_91 )) (or $cvcl_93 $cvcl_97 )) (or (or (or $cvcl_32 $cvcl_92 ) $cvcl_93 ) $cvcl_94 )) (or (or (or $cvcl_95 $cvcl_74 ) $cvcl_93 ) $cvcl_94 )) (or (or $cvcl_96 $cvcl_54 ) $cvcl_94 )) (or (or $cvcl_96 $cvcl_93 ) $cvcl_34 )) (or (or (or (not (< AT0_Z AT0_PROC1_X)) $cvcl_92 ) $cvcl_97 ) (< AT1_Z AT1_PROC1_X) )) (or (or (or $cvcl_36 $cvcl_98 ) $cvcl_93 ) $cvcl_99 )) (or (or (or $cvcl_100 $cvcl_76 ) $cvcl_93 ) $cvcl_99 )) (or (or $cvcl_101 $cvcl_54 ) $cvcl_99 )) (or (or $cvcl_101 $cvcl_93 ) $cvcl_38 )) (or (or (or (not (< AT0_Z AT0_PROC2_X)) $cvcl_98 ) $cvcl_97 ) (< AT1_Z AT1_PROC2_X) )) (or (or (or $cvcl_40 $cvcl_102 ) $cvcl_93 ) $cvcl_103 )) (or (or (or $cvcl_104 $cvcl_78 ) $cvcl_93 ) $cvcl_103 )) (or (or $cvcl_105 $cvcl_54 ) $cvcl_103 )) (or (or $cvcl_105 $cvcl_93 ) $cvcl_42 )) (or (or (or (not (< AT0_Z AT0_PROC3_X)) $cvcl_102 ) $cvcl_97 ) (< AT1_Z AT1_PROC3_X) )) (or (or (or $cvcl_44 $cvcl_106 ) $cvcl_93 ) $cvcl_107 )) (or (or (or $cvcl_108 $cvcl_80 ) $cvcl_93 ) $cvcl_107 )) (or (or $cvcl_109 $cvcl_54 ) $cvcl_107 )) (or (or $cvcl_109 $cvcl_93 ) $cvcl_46 )) (or (or (or (not (< AT0_Z AT0_PROC4_X)) $cvcl_106 ) $cvcl_97 ) (< AT1_Z AT1_PROC4_X) )) AT0_PROC1_A) AT0_PROC2_A) AT0_PROC3_A) AT0_PROC4_A) $cvcl_32) $cvcl_36) $cvcl_40) $cvcl_44) AT0_ID0) (or (or (or $cvcl_73 $cvcl_75 ) $cvcl_77 ) $cvcl_79 )) (or $cvcl_110 $cvcl_111 )) (or $cvcl_110 $cvcl_112 )) (or $cvcl_110 $cvcl_113 )) (or $cvcl_110 $cvcl_114 )) (or $cvcl_111 $cvcl_112 )) (or $cvcl_111 $cvcl_113 )) (or $cvcl_111 $cvcl_114 )) (or $cvcl_112 $cvcl_113 )) (or $cvcl_112 $cvcl_114 )) (or $cvcl_113 $cvcl_114 )) (or $cvcl_115 $cvcl_116 )) (or $cvcl_115 $cvcl_117 )) (or $cvcl_115 $cvcl_118 )) (or $cvcl_115 $cvcl_119 )) (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_48 AT0_ID0 )) (or $cvcl_48 AT1_ID0 )) (or $cvcl_49 AT1_ID1 )) (or $cvcl_51 AT0_ID0 )) (or $cvcl_51 AT1_ID0 )) (or $cvcl_52 AT0_ID1 )) (or $cvcl_52 AT1_ID1 )) (or $cvcl_53 AT1_ID0 )) (or (or $cvcl_81 $cvcl_111 ) AT1_ID1 )) (or $cvcl_55 AT0_ID0 )) (or $cvcl_55 AT1_ID0 )) (or $cvcl_56 AT1_ID2 )) (or $cvcl_58 AT0_ID0 )) (or $cvcl_58 AT1_ID0 )) (or $cvcl_59 AT0_ID2 )) (or $cvcl_59 AT1_ID2 )) (or $cvcl_60 AT1_ID0 )) (or (or $cvcl_81 $cvcl_112 ) AT1_ID2 )) (or $cvcl_61 AT0_ID0 )) (or $cvcl_61 AT1_ID0 )) (or $cvcl_62 AT1_ID3 )) (or $cvcl_64 AT0_ID0 )) (or $cvcl_64 AT1_ID0 )) (or $cvcl_65 AT0_ID3 )) (or $cvcl_65 AT1_ID3 )) (or $cvcl_66 AT1_ID0 )) (or (or $cvcl_81 $cvcl_113 ) AT1_ID3 )) (or $cvcl_67 AT0_ID0 )) (or $cvcl_67 AT1_ID0 )) (or $cvcl_68 AT1_ID4 )) (or $cvcl_70 AT0_ID0 )) (or $cvcl_70 AT1_ID0 )) (or $cvcl_71 AT0_ID4 )) (or $cvcl_71 AT1_ID4 )) (or $cvcl_72 AT1_ID0 )) (or (or $cvcl_81 $cvcl_114 ) AT1_ID4 )) (or (or $cvcl_81 $cvcl_110 ) 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_116 AT1_ID1 )) (or AT1_ID1 $cvcl_116 )) (= (- 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_117 AT1_ID2 )) (or AT1_ID2 $cvcl_117 )) (= (- 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_118 AT1_ID3 )) (or AT1_ID3 $cvcl_118 )) (= (- AT1_PROC3_X AT1_Z) (- AT1_PROC3_X AT1_Z))) (or $cvcl_28 AT1_PROC4_A )) (or AT1_PROC4_A $cvcl_28 )) (or $cvcl_29 AT1_PROC4_B )) (or AT1_PROC4_B $cvcl_29 )) (or $cvcl_30 AT1_PROC4_C )) (or AT1_PROC4_C $cvcl_30 )) (or $cvcl_31 AT1_PROC4_CS )) (or AT1_PROC4_CS $cvcl_31 )) (or $cvcl_119 AT1_ID4 )) (or AT1_ID4 $cvcl_119 )) (= (- AT1_PROC4_X AT1_Z) (- AT1_PROC4_X AT1_Z))) AT1_PROC1_B) $cvcl_7)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)