; EXPECT: unsat
(set-logic ALL)
(set-option :incremental false)
(declare-fun x_1 () Bool)
(declare-fun x_2 () Bool)
(declare-fun x_3 () Bool)
(declare-fun x_4 () Bool)
(declare-fun x_5 () Bool)
(declare-fun x_6 () Bool)
(declare-fun x_7 () Bool)
(declare-fun x_8 () Bool)
(declare-fun x_9 () Bool)
(declare-fun x_10 () Bool)
(declare-fun x_11 () Bool)
(declare-fun x_12 () Bool)
(declare-fun x_13 () Bool)
(declare-fun x_14 () Bool)
(declare-fun x_15 () Bool)
(declare-fun x_16 () Bool)
(declare-fun x_17 () Bool)
(declare-fun x_18 () Bool)
(declare-fun x_19 () Bool)
(declare-fun x_20 () Bool)
(declare-fun x_21 () Bool)
(declare-fun x_22 () Bool)
(declare-fun x_23 () Bool)
(declare-fun x_24 () Bool)
(declare-fun x_25 () Bool)
(declare-fun x_26 () Bool)
(declare-fun x_27 () Bool)
(declare-fun x_28 () Bool)
(declare-fun x_29 () Bool)
(declare-fun x_30 () Bool)
(declare-fun x_31 () Bool)
(declare-fun x_32 () Bool)
(declare-fun x_33 () Bool)
(declare-fun x_34 () Bool)
(declare-fun x_35 () Bool)
(declare-fun x_36 () Bool)
(declare-fun x_37 () Bool)
(declare-fun x_38 () Bool)
(declare-fun x_39 () Bool)
(declare-fun x_40 () Bool)
(declare-fun x_41 () Bool)
(declare-fun x_42 () Bool)
(declare-fun x_43 () Bool)
(declare-fun x_44 () Bool)
(declare-fun x_45 () Bool)
(declare-fun x_46 () Bool)
(declare-fun x_47 () Bool)
(declare-fun x_48 () Bool)
(declare-fun x_49 () Bool)
(declare-fun x_50 () Bool)
(declare-fun x_51 () Bool)
(declare-fun x_52 () Bool)
(declare-fun x_53 () Bool)
(declare-fun x_54 () Bool)
(declare-fun x_55 () Bool)
(declare-fun x_56 () Bool)
(declare-fun x_57 () Bool)
(declare-fun x_58 () Bool)
(declare-fun x_59 () Bool)
(declare-fun x_60 () Bool)
(declare-fun x_61 () Bool)
(declare-fun x_62 () Bool)
(declare-fun x_63 () Bool)
(declare-fun x_64 () Bool)
(declare-fun x_65 () Bool)
(declare-fun x_66 () Bool)
(declare-fun x_67 () Bool)
(declare-fun x_68 () Bool)
(declare-fun x_69 () Bool)
(declare-fun x_70 () Bool)
(declare-fun x_71 () Bool)
(declare-fun x_72 () Bool)
(declare-fun x_73 () Bool)
(declare-fun x_74 () Bool)
(declare-fun x_75 () Bool)
(declare-fun x_76 () Bool)
(declare-fun x_77 () Bool)
(declare-fun x_78 () Bool)
(declare-fun x_79 () Bool)
(declare-fun x_80 () Bool)
(declare-fun x_81 () Bool)
(declare-fun x_82 () Bool)
(declare-fun x_83 () Bool)
(declare-fun x_84 () Bool)
(declare-fun x_85 () Bool)
(declare-fun x_86 () Bool)
(declare-fun x_87 () Bool)
(declare-fun x_88 () Bool)
(declare-fun x_89 () Bool)
(declare-fun x_90 () Bool)
(assert (or (not x_1) (not x_10)))
(assert (or (not x_1) (not x_19)))
(assert (or (not x_1) (not x_28)))
(assert (or (not x_1) (not x_37)))
(assert (or (not x_1) (not x_46)))
(assert (or (not x_1) (not x_55)))
(assert (or (not x_1) (not x_64)))
(assert (or (not x_1) (not x_73)))
(assert (or (not x_1) (not x_82)))
(assert (or (not x_10) (not x_19)))
(assert (or (not x_10) (not x_28)))
(assert (or (not x_10) (not x_37)))
(assert (or (not x_10) (not x_46)))
(assert (or (not x_10) (not x_55)))
(assert (or (not x_10) (not x_64)))
(assert (or (not x_10) (not x_73)))
(assert (or (not x_10) (not x_82)))
(assert (or (not x_19) (not x_28)))
(assert (or (not x_19) (not x_37)))
(assert (or (not x_19) (not x_46)))
(assert (or (not x_19) (not x_55)))
(assert (or (not x_19) (not x_64)))
(assert (or (not x_19) (not x_73)))
(assert (or (not x_19) (not x_82)))
(assert (or (not x_28) (not x_37)))
(assert (or (not x_28) (not x_46)))
(assert (or (not x_28) (not x_55)))
(assert (or (not x_28) (not x_64)))
(assert (or (not x_28) (not x_73)))
(assert (or (not x_28) (not x_82)))
(assert (or (not x_37) (not x_46)))
(assert (or (not x_37) (not x_55)))
(assert (or (not x_37) (not x_64)))
(assert (or (not x_37) (not x_73)))
(assert (or (not x_37) (not x_82)))
(assert (or (not x_46) (not x_55)))
(assert (or (not x_46) (not x_64)))
(assert (or (not x_46) (not x_73)))
(assert (or (not x_46) (not x_82)))
(assert (or (not x_55) (not x_64)))
(assert (or (not x_55) (not x_73)))
(assert (or (not x_55) (not x_82)))
(assert (or (not x_64) (not x_73)))
(assert (or (not x_64) (not x_82)))
(assert (or (not x_73) (not x_82)))
(assert (or (not x_2) (not x_11)))
(assert (or (not x_2) (not x_20)))
(assert (or (not x_2) (not x_29)))
(assert (or (not x_2) (not x_38)))
(assert (or (not x_2) (not x_47)))
(assert (or (not x_2) (not x_56)))
(assert (or (not x_2) (not x_65)))
(assert (or (not x_2) (not x_74)))
(assert (or (not x_2) (not x_83)))
(assert (or (not x_11) (not x_20)))
(assert (or (not x_11) (not x_29)))
(assert (or (not x_11) (not x_38)))
(assert (or (not x_11) (not x_47)))
(assert (or (not x_11) (not x_56)))
(assert (or (not x_11) (not x_65)))
(assert (or (not x_11) (not x_74)))
(assert (or (not x_11) (not x_83)))
(assert (or (not x_20) (not x_29)))
(assert (or (not x_20) (not x_38)))
(assert (or (not x_20) (not x_47)))
(assert (or (not x_20) (not x_56)))
(assert (or (not x_20) (not x_65)))
(assert (or (not x_20) (not x_74)))
(assert (or (not x_20) (not x_83)))
(assert (or (not x_29) (not x_38)))
(assert (or (not x_29) (not x_47)))
(assert (or (not x_29) (not x_56)))
(assert (or (not x_29) (not x_65)))
(assert (or (not x_29) (not x_74)))
(assert (or (not x_29) (not x_83)))
(assert (or (not x_38) (not x_47)))
(assert (or (not x_38) (not x_56)))
(assert (or (not x_38) (not x_65)))
(assert (or (not x_38) (not x_74)))
(assert (or (not x_38) (not x_83)))
(assert (or (not x_47) (not x_56)))
(assert (or (not x_47) (not x_65)))
(assert (or (not x_47) (not x_74)))
(assert (or (not x_47) (not x_83)))
(assert (or (not x_56) (not x_65)))
(assert (or (not x_56) (not x_74)))
(assert (or (not x_56) (not x_83)))
(assert (or (not x_65) (not x_74)))
(assert (or (not x_65) (not x_83)))
(assert (or (not x_74) (not x_83)))
(assert (or (not x_3) (not x_12)))
(assert (or (not x_3) (not x_21)))
(assert (or (not x_3) (not x_30)))
(assert (or (not x_3) (not x_39)))
(assert (or (not x_3) (not x_48)))
(assert (or (not x_3) (not x_57)))
(assert (or (not x_3) (not x_66)))
(assert (or (not x_3) (not x_75)))
(assert (or (not x_3) (not x_84)))
(assert (or (not x_12) (not x_21)))
(assert (or (not x_12) (not x_30)))
(assert (or (not x_12) (not x_39)))
(assert (or (not x_12) (not x_48)))
(assert (or (not x_12) (not x_57)))
(assert (or (not x_12) (not x_66)))
(assert (or (not x_12) (not x_75)))
(assert (or (not x_12) (not x_84)))
(assert (or (not x_21) (not x_30)))
(assert (or (not x_21) (not x_39)))
(assert (or (not x_21) (not x_48)))
(assert (or (not x_21) (not x_57)))
(assert (or (not x_21) (not x_66)))
(assert (or (not x_21) (not x_75)))
(assert (or (not x_21) (not x_84)))
(assert (or (not x_30) (not x_39)))
(assert (or (not x_30) (not x_48)))
(assert (or (not x_30) (not x_57)))
(assert (or (not x_30) (not x_66)))
(assert (or (not x_30) (not x_75)))
(assert (or (not x_30) (not x_84)))
(assert (or (not x_39) (not x_48)))
(assert (or (not x_39) (not x_57)))
(assert (or (not x_39) (not x_66)))
(assert (or (not x_39) (not x_75)))
(assert (or (not x_39) (not x_84)))
(assert (or (not x_48) (not x_57)))
(assert (or (not x_48) (not x_66)))
(assert (or (not x_48) (not x_75)))
(assert (or (not x_48) (not x_84)))
(assert (or (not x_57) (not x_66)))
(assert (or (not x_57) (not x_75)))
(assert (or (not x_57) (not x_84)))
(assert (or (not x_66) (not x_75)))
(assert (or (not x_66) (not x_84)))
(assert (or (not x_75) (not x_84)))
(assert (or (not x_4) (not x_13)))
(assert (or (not x_4) (not x_22)))
(assert (or (not x_4) (not x_31)))
(assert (or (not x_4) (not x_40)))
(assert (or (not x_4) (not x_49)))
(assert (or (not x_4) (not x_58)))
(assert (or (not x_4) (not x_67)))
(assert (or (not x_4) (not x_76)))
(assert (or (not x_4) (not x_85)))
(assert (or (not x_13) (not x_22)))
(assert (or (not x_13) (not x_31)))
(assert (or (not x_13) (not x_40)))
(assert (or (not x_13) (not x_49)))
(assert (or (not x_13) (not x_58)))
(assert (or (not x_13) (not x_67)))
(assert (or (not x_13) (not x_76)))
(assert (or (not x_13) (not x_85)))
(assert (or (not x_22) (not x_31)))
(assert (or (not x_22) (not x_40)))
(assert (or (not x_22) (not x_49)))
(assert (or (not x_22) (not x_58)))
(assert (or (not x_22) (not x_67)))
(assert (or (not x_22) (not x_76)))
(assert (or (not x_22) (not x_85)))
(assert (or (not x_31) (not x_40)))
(assert (or (not x_31) (not x_49)))
(assert (or (not x_31) (not x_58)))
(assert (or (not x_31) (not x_67)))
(assert (or (not x_31) (not x_76)))
(assert (or (not x_31) (not x_85)))
(assert (or (not x_40) (not x_49)))
(assert (or (not x_40) (not x_58)))
(assert (or (not x_40) (not x_67)))
(assert (or (not x_40) (not x_76)))
(assert (or (not x_40) (not x_85)))
(assert (or (not x_49) (not x_58)))
(assert (or (not x_49) (not x_67)))
(assert (or (not x_49) (not x_76)))
(assert (or (not x_49) (not x_85)))
(assert (or (not x_58) (not x_67)))
(assert (or (not x_58) (not x_76)))
(assert (or (not x_58) (not x_85)))
(assert (or (not x_67) (not x_76)))
(assert (or (not x_67) (not x_85)))
(assert (or (not x_76) (not x_85)))
(assert (or (not x_5) (not x_14)))
(assert (or (not x_5) (not x_23)))
(assert (or (not x_5) (not x_32)))
(assert (or (not x_5) (not x_41)))
(assert (or (not x_5) (not x_50)))
(assert (or (not x_5) (not x_59)))
(assert (or (not x_5) (not x_68)))
(assert (or (not x_5) (not x_77)))
(assert (or (not x_5) (not x_86)))
(assert (or (not x_14) (not x_23)))
(assert (or (not x_14) (not x_32)))
(assert (or (not x_14) (not x_41)))
(assert (or (not x_14) (not x_50)))
(assert (or (not x_14) (not x_59)))
(assert (or (not x_14) (not x_68)))
(assert (or (not x_14) (not x_77)))
(assert (or (not x_14) (not x_86)))
(assert (or (not x_23) (not x_32)))
(assert (or (not x_23) (not x_41)))
(assert (or (not x_23) (not x_50)))
(assert (or (not x_23) (not x_59)))
(assert (or (not x_23) (not x_68)))
(assert (or (not x_23) (not x_77)))
(assert (or (not x_23) (not x_86)))
(assert (or (not x_32) (not x_41)))
(assert (or (not x_32) (not x_50)))
(assert (or (not x_32) (not x_59)))
(assert (or (not x_32) (not x_68)))
(assert (or (not x_32) (not x_77)))
(assert (or (not x_32) (not x_86)))
(assert (or (not x_41) (not x_50)))
(assert (or (not x_41) (not x_59)))
(assert (or (not x_41) (not x_68)))
(assert (or (not x_41) (not x_77)))
(assert (or (not x_41) (not x_86)))
(assert (or (not x_50) (not x_59)))
(assert (or (not x_50) (not x_68)))
(assert (or (not x_50) (not x_77)))
(assert (or (not x_50) (not x_86)))
(assert (or (not x_59) (not x_68)))
(assert (or (not x_59) (not x_77)))
(assert (or (not x_59) (not x_86)))
(assert (or (not x_68) (not x_77)))
(assert (or (not x_68) (not x_86)))
(assert (or (not x_77) (not x_86)))
(assert (or (not x_6) (not x_15)))
(assert (or (not x_6) (not x_24)))
(assert (or (not x_6) (not x_33)))
(assert (or (not x_6) (not x_42)))
(assert (or (not x_6) (not x_51)))
(assert (or (not x_6) (not x_60)))
(assert (or (not x_6) (not x_69)))
(assert (or (not x_6) (not x_78)))
(assert (or (not x_6) (not x_87)))
(assert (or (not x_15) (not x_24)))
(assert (or (not x_15) (not x_33)))
(assert (or (not x_15) (not x_42)))
(assert (or (not x_15) (not x_51)))
(assert (or (not x_15) (not x_60)))
(assert (or (not x_15) (not x_69)))
(assert (or (not x_15) (not x_78)))
(assert (or (not x_15) (not x_87)))
(assert (or (not x_24) (not x_33)))
(assert (or (not x_24) (not x_42)))
(assert (or (not x_24) (not x_51)))
(assert (or (not x_24) (not x_60)))
(assert (or (not x_24) (not x_69)))
(assert (or (not x_24) (not x_78)))
(assert (or (not x_24) (not x_87)))
(assert (or (not x_33) (not x_42)))
(assert (or (not x_33) (not x_51)))
(assert (or (not x_33) (not x_60)))
(assert (or (not x_33) (not x_69)))
(assert (or (not x_33) (not x_78)))
(assert (or (not x_33) (not x_87)))
(assert (or (not x_42) (not x_51)))
(assert (or (not x_42) (not x_60)))
(assert (or (not x_42) (not x_69)))
(assert (or (not x_42) (not x_78)))
(assert (or (not x_42) (not x_87)))
(assert (or (not x_51) (not x_60)))
(assert (or (not x_51) (not x_69)))
(assert (or (not x_51) (not x_78)))
(assert (or (not x_51) (not x_87)))
(assert (or (not x_60) (not x_69)))
(assert (or (not x_60) (not x_78)))
(assert (or (not x_60) (not x_87)))
(assert (or (not x_69) (not x_78)))
(assert (or (not x_69) (not x_87)))
(assert (or (not x_78) (not x_87)))
(assert (or (not x_7) (not x_16)))
(assert (or (not x_7) (not x_25)))
(assert (or (not x_7) (not x_34)))
(assert (or (not x_7) (not x_43)))
(assert (or (not x_7) (not x_52)))
(assert (or (not x_7) (not x_61)))
(assert (or (not x_7) (not x_70)))
(assert (or (not x_7) (not x_79)))
(assert (or (not x_7) (not x_88)))
(assert (or (not x_16) (not x_25)))
(assert (or (not x_16) (not x_34)))
(assert (or (not x_16) (not x_43)))
(assert (or (not x_16) (not x_52)))
(assert (or (not x_16) (not x_61)))
(assert (or (not x_16) (not x_70)))
(assert (or (not x_16) (not x_79)))
(assert (or (not x_16) (not x_88)))
(assert (or (not x_25) (not x_34)))
(assert (or (not x_25) (not x_43)))
(assert (or (not x_25) (not x_52)))
(assert (or (not x_25) (not x_61)))
(assert (or (not x_25) (not x_70)))
(assert (or (not x_25) (not x_79)))
(assert (or (not x_25) (not x_88)))
(assert (or (not x_34) (not x_43)))
(assert (or (not x_34) (not x_52)))
(assert (or (not x_34) (not x_61)))
(assert (or (not x_34) (not x_70)))
(assert (or (not x_34) (not x_79)))
(assert (or (not x_34) (not x_88)))
(assert (or (not x_43) (not x_52)))
(assert (or (not x_43) (not x_61)))
(assert (or (not x_43) (not x_70)))
(assert (or (not x_43) (not x_79)))
(assert (or (not x_43) (not x_88)))
(assert (or (not x_52) (not x_61)))
(assert (or (not x_52) (not x_70)))
(assert (or (not x_52) (not x_79)))
(assert (or (not x_52) (not x_88)))
(assert (or (not x_61) (not x_70)))
(assert (or (not x_61) (not x_79)))
(assert (or (not x_61) (not x_88)))
(assert (or (not x_70) (not x_79)))
(assert (or (not x_70) (not x_88)))
(assert (or (not x_79) (not x_88)))
(assert (or (not x_8) (not x_17)))
(assert (or (not x_8) (not x_26)))
(assert (or (not x_8) (not x_35)))
(assert (or (not x_8) (not x_44)))
(assert (or (not x_8) (not x_53)))
(assert (or (not x_8) (not x_62)))
(assert (or (not x_8) (not x_71)))
(assert (or (not x_8) (not x_80)))
(assert (or (not x_8) (not x_89)))
(assert (or (not x_17) (not x_26)))
(assert (or (not x_17) (not x_35)))
(assert (or (not x_17) (not x_44)))
(assert (or (not x_17) (not x_53)))
(assert (or (not x_17) (not x_62)))
(assert (or (not x_17) (not x_71)))
(assert (or (not x_17) (not x_80)))
(assert (or (not x_17) (not x_89)))
(assert (or (not x_26) (not x_35)))
(assert (or (not x_26) (not x_44)))
(assert (or (not x_26) (not x_53)))
(assert (or (not x_26) (not x_62)))
(assert (or (not x_26) (not x_71)))
(assert (or (not x_26) (not x_80)))
(assert (or (not x_26) (not x_89)))
(assert (or (not x_35) (not x_44)))
(assert (or (not x_35) (not x_53)))
(assert (or (not x_35) (not x_62)))
(assert (or (not x_35) (not x_71)))
(assert (or (not x_35) (not x_80)))
(assert (or (not x_35) (not x_89)))
(assert (or (not x_44) (not x_53)))
(assert (or (not x_44) (not x_62)))
(assert (or (not x_44) (not x_71)))
(assert (or (not x_44) (not x_80)))
(assert (or (not x_44) (not x_89)))
(assert (or (not x_53) (not x_62)))
(assert (or (not x_53) (not x_71)))
(assert (or (not x_53) (not x_80)))
(assert (or (not x_53) (not x_89)))
(assert (or (not x_62) (not x_71)))
(assert (or (not x_62) (not x_80)))
(assert (or (not x_62) (not x_89)))
(assert (or (not x_71) (not x_80)))
(assert (or (not x_71) (not x_89)))
(assert (or (not x_80) (not x_89)))
(assert (or (not x_9) (not x_18)))
(assert (or (not x_9) (not x_27)))
(assert (or (not x_9) (not x_36)))
(assert (or (not x_9) (not x_45)))
(assert (or (not x_9) (not x_54)))
(assert (or (not x_9) (not x_63)))
(assert (or (not x_9) (not x_72)))
(assert (or (not x_9) (not x_81)))
(assert (or (not x_9) (not x_90)))
(assert (or (not x_18) (not x_27)))
(assert (or (not x_18) (not x_36)))
(assert (or (not x_18) (not x_45)))
(assert (or (not x_18) (not x_54)))
(assert (or (not x_18) (not x_63)))
(assert (or (not x_18) (not x_72)))
(assert (or (not x_18) (not x_81)))
(assert (or (not x_18) (not x_90)))
(assert (or (not x_27) (not x_36)))
(assert (or (not x_27) (not x_45)))
(assert (or (not x_27) (not x_54)))
(assert (or (not x_27) (not x_63)))
(assert (or (not x_27) (not x_72)))
(assert (or (not x_27) (not x_81)))
(assert (or (not x_27) (not x_90)))
(assert (or (not x_36) (not x_45)))
(assert (or (not x_36) (not x_54)))
(assert (or (not x_36) (not x_63)))
(assert (or (not x_36) (not x_72)))
(assert (or (not x_36) (not x_81)))
(assert (or (not x_36) (not x_90)))
(assert (or (not x_45) (not x_54)))
(assert (or (not x_45) (not x_63)))
(assert (or (not x_45) (not x_72)))
(assert (or (not x_45) (not x_81)))
(assert (or (not x_45) (not x_90)))
(assert (or (not x_54) (not x_63)))
(assert (or (not x_54) (not x_72)))
(assert (or (not x_54) (not x_81)))
(assert (or (not x_54) (not x_90)))
(assert (or (not x_63) (not x_72)))
(assert (or (not x_63) (not x_81)))
(assert (or (not x_63) (not x_90)))
(assert (or (not x_72) (not x_81)))
(assert (or (not x_72) (not x_90)))
(assert (or (not x_81) (not x_90)))
(assert (or (or (or (or (or (or (or (or x_9 x_8) x_7) x_6) x_5) x_4) x_3) x_2) x_1))
(assert (or (or (or (or (or (or (or (or x_18 x_17) x_16) x_15) x_14) x_13) x_12) x_11) x_10))
(assert (or (or (or (or (or (or (or (or x_27 x_26) x_25) x_24) x_23) x_22) x_21) x_20) x_19))
(assert (or (or (or (or (or (or (or (or x_36 x_35) x_34) x_33) x_32) x_31) x_30) x_29) x_28))
(assert (or (or (or (or (or (or (or (or x_45 x_44) x_43) x_42) x_41) x_40) x_39) x_38) x_37))
(assert (or (or (or (or (or (or (or (or x_54 x_53) x_52) x_51) x_50) x_49) x_48) x_47) x_46))
(assert (or (or (or (or (or (or (or (or x_63 x_62) x_61) x_60) x_59) x_58) x_57) x_56) x_55))
(assert (or (or (or (or (or (or (or (or x_72 x_71) x_70) x_69) x_68) x_67) x_66) x_65) x_64))
(assert (or (or (or (or (or (or (or (or x_81 x_80) x_79) x_78) x_77) x_76) x_75) x_74) x_73))
(assert (or (or (or (or (or (or (or (or x_90 x_89) x_88) x_87) x_86) x_85) x_84) x_83) x_82))
(check-sat)