(benchmark FISCHER2_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 :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 ((AT1_PROC2_CS)) :extrapreds ((AT0_PROC2_SW_C_B_TAU)) :extrapreds ((AT0_PROC1_C)) :extrapreds ((AT0_PROC1_B)) :extrapreds ((AT0_PROC1_A)) :extrapreds ((AT0_PROC2_CS)) :extrapreds ((AT1_ID0)) :extrapreds ((AT1_ID1)) :extrapreds ((AT1_ID2)) :extrapreds ((AT0_PROC1_SW_CS_A_TAU)) :extrafuns ((AT0_PROC2_X Int)) :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_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_DELTA)) :extrapreds ((AT0_PROC2_SW_B_C_TAU)) :extrapreds ((AT1_PROC1_CS)) :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_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 (= AT0_PROC1_X AT0_Z)) (flet ($cvcl_17 (> AT0_PROC1_X AT0_Z)) (flet ($cvcl_51 (not $cvcl_16)) (flet ($cvcl_18 (= AT1_PROC1_X AT1_Z)) (flet ($cvcl_19 (> AT1_PROC1_X AT1_Z)) (flet ($cvcl_50 (not $cvcl_18)) (flet ($cvcl_20 (= AT0_PROC2_X AT0_Z)) (flet ($cvcl_21 (> AT0_PROC2_X AT0_Z)) (flet ($cvcl_56 (not $cvcl_20)) (flet ($cvcl_22 (= AT1_PROC2_X AT1_Z)) (flet ($cvcl_23 (> AT1_PROC2_X AT1_Z)) (flet ($cvcl_55 (not $cvcl_22)) (flet ($cvcl_26 (<= (- AT0_PROC1_X AT0_Z) 10)) (flet ($cvcl_33 (<= (- AT0_PROC2_X AT0_Z) 10)) (flet ($cvcl_24 (not AT0_PROC1_SW_A_B_TAU)) (flet ($cvcl_25 (not AT0_PROC1_SW_B_C_TAU)) (flet ($cvcl_27 (not AT0_PROC1_SW_C_B_TAU)) (flet ($cvcl_28 (not AT0_PROC1_SW_C_CS_TAU)) (flet ($cvcl_38 (= AT1_PROC1_X AT0_PROC1_X)) (flet ($cvcl_29 (not AT0_PROC1_SW_CS_A_TAU)) (flet ($cvcl_30 (= AT1_Z AT0_Z)) (flet ($cvcl_31 (not AT0_PROC2_SW_A_B_TAU)) (flet ($cvcl_32 (not AT0_PROC2_SW_B_C_TAU)) (flet ($cvcl_34 (not AT0_PROC2_SW_C_B_TAU)) (flet ($cvcl_35 (not AT0_PROC2_SW_C_CS_TAU)) (flet ($cvcl_40 (= AT1_PROC2_X AT0_PROC2_X)) (flet ($cvcl_36 (not AT0_PROC2_SW_CS_A_TAU)) (flet ($cvcl_37 (not AT0_PROC1_WAIT)) (flet ($cvcl_42 (not AT0_PROC1_TAU)) (flet ($cvcl_39 (not AT0_PROC2_WAIT)) (flet ($cvcl_43 (not AT0_PROC2_TAU)) (flet ($cvcl_41 (not AT0_DELTA)) (flet ($cvcl_47 (< AT1_Z AT0_Z)) (flet ($cvcl_44 (or $cvcl_41 $cvcl_47 )) (flet ($cvcl_45 (< AT1_PROC1_X AT0_PROC1_X)) (flet ($cvcl_48 (not $cvcl_38)) (flet ($cvcl_46 (< AT1_PROC2_X AT0_PROC2_X)) (flet ($cvcl_54 (not $cvcl_40)) (flet ($cvcl_49 (not $cvcl_30)) (flet ($cvcl_53 (not $cvcl_47)) (flet ($cvcl_52 (or $cvcl_51 $cvcl_48 )) (flet ($cvcl_57 (or $cvcl_56 $cvcl_54 )) (flet ($cvcl_58 (not AT0_ID0)) (flet ($cvcl_59 (not AT0_ID1)) (flet ($cvcl_60 (not AT0_ID2)) (flet ($cvcl_61 (not AT1_ID0)) (flet ($cvcl_62 (not AT1_ID1)) (flet ($cvcl_63 (not AT1_ID2)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (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_51 (not $cvcl_17) )) (or $cvcl_18 $cvcl_19 )) (or $cvcl_50 (not $cvcl_19) )) (or $cvcl_20 $cvcl_21 )) (or $cvcl_56 (not $cvcl_21) )) (or $cvcl_22 $cvcl_23 )) (or $cvcl_55 (not $cvcl_23) )) (or $cvcl_1 $cvcl_26 )) (or $cvcl_5 (<= (- AT1_PROC1_X AT1_Z) 10) )) (or $cvcl_9 $cvcl_33 )) (or $cvcl_13 (<= (- AT1_PROC2_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 $cvcl_24 AT0_PROC1_A )) (or $cvcl_24 AT0_PROC1_TAU )) (or $cvcl_24 AT1_PROC1_B )) (or $cvcl_24 $cvcl_18 )) (or $cvcl_25 AT0_PROC1_B )) (or $cvcl_25 AT0_PROC1_TAU )) (or $cvcl_25 AT1_PROC1_C )) (or $cvcl_25 $cvcl_26 )) (or $cvcl_25 $cvcl_18 )) (or $cvcl_27 AT0_PROC1_C )) (or $cvcl_27 AT0_PROC1_TAU )) (or $cvcl_27 AT1_PROC1_B )) (or $cvcl_27 $cvcl_18 )) (or $cvcl_28 AT0_PROC1_C )) (or $cvcl_28 AT0_PROC1_TAU )) (or $cvcl_28 AT1_PROC1_CS )) (or $cvcl_28 (> (- AT0_PROC1_X AT0_Z) 10) )) (or $cvcl_28 $cvcl_38 )) (or $cvcl_29 AT0_PROC1_CS )) (or $cvcl_29 AT0_PROC1_TAU )) (or $cvcl_29 AT1_PROC1_A )) (or $cvcl_29 $cvcl_18 )) (or $cvcl_24 $cvcl_30 )) (or $cvcl_25 $cvcl_30 )) (or $cvcl_27 $cvcl_30 )) (or $cvcl_28 $cvcl_30 )) (or $cvcl_29 $cvcl_30 )) (or $cvcl_31 AT0_PROC2_A )) (or $cvcl_31 AT0_PROC2_TAU )) (or $cvcl_31 AT1_PROC2_B )) (or $cvcl_31 $cvcl_22 )) (or $cvcl_32 AT0_PROC2_B )) (or $cvcl_32 AT0_PROC2_TAU )) (or $cvcl_32 AT1_PROC2_C )) (or $cvcl_32 $cvcl_33 )) (or $cvcl_32 $cvcl_22 )) (or $cvcl_34 AT0_PROC2_C )) (or $cvcl_34 AT0_PROC2_TAU )) (or $cvcl_34 AT1_PROC2_B )) (or $cvcl_34 $cvcl_22 )) (or $cvcl_35 AT0_PROC2_C )) (or $cvcl_35 AT0_PROC2_TAU )) (or $cvcl_35 AT1_PROC2_CS )) (or $cvcl_35 (> (- AT0_PROC2_X AT0_Z) 10) )) (or $cvcl_35 $cvcl_40 )) (or $cvcl_36 AT0_PROC2_CS )) (or $cvcl_36 AT0_PROC2_TAU )) (or $cvcl_36 AT1_PROC2_A )) (or $cvcl_36 $cvcl_22 )) (or $cvcl_31 $cvcl_30 )) (or $cvcl_32 $cvcl_30 )) (or $cvcl_34 $cvcl_30 )) (or $cvcl_35 $cvcl_30 )) (or $cvcl_36 $cvcl_30 )) (or (or $cvcl_37 $cvcl_0 ) AT1_PROC1_A )) (or (or $cvcl_37 AT0_PROC1_A ) $cvcl_4 )) (or (or $cvcl_37 $cvcl_1 ) AT1_PROC1_B )) (or (or $cvcl_37 AT0_PROC1_B ) $cvcl_5 )) (or (or $cvcl_37 $cvcl_2 ) AT1_PROC1_C )) (or (or $cvcl_37 AT0_PROC1_C ) $cvcl_6 )) (or (or $cvcl_37 $cvcl_3 ) AT1_PROC1_CS )) (or (or $cvcl_37 AT0_PROC1_CS ) $cvcl_7 )) (or $cvcl_37 $cvcl_42 )) (or $cvcl_37 $cvcl_38 )) (or $cvcl_37 $cvcl_30 )) (or (or $cvcl_39 $cvcl_8 ) AT1_PROC2_A )) (or (or $cvcl_39 AT0_PROC2_A ) $cvcl_12 )) (or (or $cvcl_39 $cvcl_9 ) AT1_PROC2_B )) (or (or $cvcl_39 AT0_PROC2_B ) $cvcl_13 )) (or (or $cvcl_39 $cvcl_10 ) AT1_PROC2_C )) (or (or $cvcl_39 AT0_PROC2_C ) $cvcl_14 )) (or (or $cvcl_39 $cvcl_11 ) AT1_PROC2_CS )) (or (or $cvcl_39 AT0_PROC2_CS ) $cvcl_15 )) (or $cvcl_39 $cvcl_43 )) (or $cvcl_39 $cvcl_40 )) (or $cvcl_39 $cvcl_30 )) (or (or $cvcl_41 $cvcl_0 ) AT1_PROC1_A )) (or (or $cvcl_41 AT0_PROC1_A ) $cvcl_4 )) (or (or $cvcl_41 $cvcl_1 ) AT1_PROC1_B )) (or (or $cvcl_41 AT0_PROC1_B ) $cvcl_5 )) (or (or $cvcl_41 $cvcl_2 ) AT1_PROC1_C )) (or (or $cvcl_41 AT0_PROC1_C ) $cvcl_6 )) (or (or $cvcl_41 $cvcl_3 ) AT1_PROC1_CS )) (or (or $cvcl_41 AT0_PROC1_CS ) $cvcl_7 )) (or $cvcl_41 $cvcl_38 )) (or $cvcl_41 $cvcl_42 )) $cvcl_44) (or (or $cvcl_41 $cvcl_8 ) AT1_PROC2_A )) (or (or $cvcl_41 AT0_PROC2_A ) $cvcl_12 )) (or (or $cvcl_41 $cvcl_9 ) AT1_PROC2_B )) (or (or $cvcl_41 AT0_PROC2_B ) $cvcl_13 )) (or (or $cvcl_41 $cvcl_10 ) AT1_PROC2_C )) (or (or $cvcl_41 AT0_PROC2_C ) $cvcl_14 )) (or (or $cvcl_41 $cvcl_11 ) AT1_PROC2_CS )) (or (or $cvcl_41 AT0_PROC2_CS ) $cvcl_15 )) (or $cvcl_41 $cvcl_40 )) (or $cvcl_41 $cvcl_43 )) $cvcl_44) (or $cvcl_38 $cvcl_45 )) (or $cvcl_48 (not $cvcl_45) )) (or $cvcl_40 $cvcl_46 )) (or $cvcl_54 (not $cvcl_46) )) (or $cvcl_30 $cvcl_47 )) (or $cvcl_49 $cvcl_53 )) (or (or (or $cvcl_16 $cvcl_48 ) $cvcl_49 ) $cvcl_50 )) (or (or (or $cvcl_51 $cvcl_38 ) $cvcl_49 ) $cvcl_50 )) (or (or $cvcl_52 $cvcl_30 ) $cvcl_50 )) (or (or $cvcl_52 $cvcl_49 ) $cvcl_18 )) (or (or (or (not (< AT0_Z AT0_PROC1_X)) $cvcl_48 ) $cvcl_53 ) (< AT1_Z AT1_PROC1_X) )) (or (or (or $cvcl_20 $cvcl_54 ) $cvcl_49 ) $cvcl_55 )) (or (or (or $cvcl_56 $cvcl_40 ) $cvcl_49 ) $cvcl_55 )) (or (or $cvcl_57 $cvcl_30 ) $cvcl_55 )) (or (or $cvcl_57 $cvcl_49 ) $cvcl_22 )) (or (or (or (not (< AT0_Z AT0_PROC2_X)) $cvcl_54 ) $cvcl_53 ) (< AT1_Z AT1_PROC2_X) )) AT0_PROC1_A) AT0_PROC2_A) $cvcl_16) $cvcl_20) AT0_ID0) (or $cvcl_37 $cvcl_39 )) (or $cvcl_58 $cvcl_59 )) (or $cvcl_58 $cvcl_60 )) (or $cvcl_59 $cvcl_60 )) (or $cvcl_61 $cvcl_62 )) (or $cvcl_61 $cvcl_63 )) (or $cvcl_62 $cvcl_63 )) (or $cvcl_24 AT0_ID0 )) (or $cvcl_24 AT1_ID0 )) (or $cvcl_25 AT1_ID1 )) (or $cvcl_27 AT0_ID0 )) (or $cvcl_27 AT1_ID0 )) (or $cvcl_28 AT0_ID1 )) (or $cvcl_28 AT1_ID1 )) (or $cvcl_29 AT1_ID0 )) (or (or $cvcl_41 $cvcl_59 ) AT1_ID1 )) (or $cvcl_31 AT0_ID0 )) (or $cvcl_31 AT1_ID0 )) (or $cvcl_32 AT1_ID2 )) (or $cvcl_34 AT0_ID0 )) (or $cvcl_34 AT1_ID0 )) (or $cvcl_35 AT0_ID2 )) (or $cvcl_35 AT1_ID2 )) (or $cvcl_36 AT1_ID0 )) (or (or $cvcl_41 $cvcl_60 ) AT1_ID2 )) (or (or $cvcl_41 $cvcl_58 ) 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_62 AT1_ID1 )) (or AT1_ID1 $cvcl_62 )) (= (- 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_63 AT1_ID2 )) (or AT1_ID2 $cvcl_63 )) (= (- AT1_PROC2_X AT1_Z) (- AT1_PROC2_X AT1_Z))) AT1_PROC1_B) $cvcl_7))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )