msc.smt2

;this file is automatically generated: Thu Nov 08 18:23:00 GMT 2018

;declarations generated

(declare-fun a_7_100 () Int )
(declare-fun a_0_115 () Int )
(declare-fun A0 () Int )
(declare-fun A1 () Int )
(declare-fun s31 () Int )
(declare-fun A2 () Int )
(declare-fun s30 () Int )
(declare-fun A3 () Int )
(declare-fun s33 () Int )
(declare-fun A4 () Int )
(declare-fun s32 () Int )
(declare-fun A5 () Int )
(declare-fun s35 () Int )
(declare-fun A6 () Int )
(declare-fun s34 () Int )
(declare-fun A7 () Int )
(declare-fun s37 () Int )
(declare-fun s36 () Int )
(declare-fun s39 () Int )
(declare-fun s38 () Int )
(declare-fun s0 () Int )
(declare-fun s1 () Int )
(declare-fun a_6_85 () Int )
(declare-fun s2 () Int )
(declare-fun s3 () Int )
(declare-fun s4 () Int )
(declare-fun s5 () Int )
(declare-fun s6 () Int )
(declare-fun s7 () Int )
(declare-fun s8 () Int )
(declare-fun s9 () Int )
(declare-fun a_0_100 () Int )
(declare-fun s40 () Int )
(declare-fun s42 () Int )
(declare-fun s41 () Int )
(declare-fun s44 () Int )
(declare-fun a_1_86 () Int )
(declare-fun s43 () Int )
(declare-fun s46 () Int )
(declare-fun s45 () Int )
(declare-fun s48 () Int )
(declare-fun s47 () Int )
(declare-fun s49 () Int )
(declare-fun a_7_116 () Int )
(declare-fun a_4_115 () Int )
(declare-fun s51 () Int )
(declare-fun s50 () Int )
(declare-fun s53 () Int )
(declare-fun s206 () Int )
(declare-fun s52 () Int )
(declare-fun s205 () Int )
(declare-fun s55 () Int )
(declare-fun s208 () Int )
(declare-fun s54 () Int )
(declare-fun s207 () Int )
(declare-fun a_0_86 () Int )
(declare-fun s57 () Int )
(declare-fun s202 () Int )
(declare-fun s56 () Int )
(declare-fun s201 () Int )
(declare-fun s59 () Int )
(declare-fun s204 () Int )
(declare-fun s58 () Int )
(declare-fun s203 () Int )
(declare-fun s209 () Int )
(declare-fun s200 () Int )
(declare-fun a_4_102 () Int )
(declare-fun s60 () Int )
(declare-fun s62 () Int )
(declare-fun s61 () Int )
(declare-fun s64 () Int )
(declare-fun s63 () Int )
(declare-fun s66 () Int )
(declare-fun s65 () Int )
(declare-fun s68 () Int )
(declare-fun s67 () Int )
(declare-fun s69 () Int )
(declare-fun s110 () Int )
(declare-fun s112 () Int )
(declare-fun s111 () Int )
(declare-fun s71 () Int )
(declare-fun s70 () Int )
(declare-fun s73 () Int )
(declare-fun s72 () Int )
(declare-fun s75 () Int )
(declare-fun s107 () Int )
(declare-fun s74 () Int )
(declare-fun s106 () Int )
(declare-fun s77 () Int )
(declare-fun s109 () Int )
(declare-fun s76 () Int )
(declare-fun s108 () Int )
(declare-fun s79 () Int )
(declare-fun s103 () Int )
(declare-fun s78 () Int )
(declare-fun s102 () Int )
(declare-fun s105 () Int )
(declare-fun s104 () Int )
(declare-fun s80 () Int )
(declare-fun s101 () Int )
(declare-fun s100 () Int )
(declare-fun s82 () Int )
(declare-fun s81 () Int )
(declare-fun s84 () Int )
(declare-fun s83 () Int )
(declare-fun s86 () Int )
(declare-fun s85 () Int )
(declare-fun s88 () Int )
(declare-fun s87 () Int )
(declare-fun s89 () Int )
(declare-fun a_5_86 () Int )
(declare-fun s132 () Int )
(declare-fun s131 () Int )
(declare-fun s91 () Int )
(declare-fun s134 () Int )
(declare-fun s90 () Int )
(declare-fun s133 () Int )
(declare-fun s93 () Int )
(declare-fun s92 () Int )
(declare-fun s95 () Int )
(declare-fun s130 () Int )
(declare-fun s94 () Int )
(declare-fun s97 () Int )
(declare-fun s129 () Int )
(declare-fun s96 () Int )
(declare-fun s128 () Int )
(declare-fun s99 () Int )
(declare-fun s98 () Int )
(declare-fun s125 () Int )
(declare-fun a_3_100 () Int )
(declare-fun s124 () Int )
(declare-fun s127 () Int )
(declare-fun s126 () Int )
(declare-fun a_4_85 () Int )
(declare-fun s121 () Int )
(declare-fun s120 () Int )
(declare-fun s123 () Int )
(declare-fun s122 () Int )
(declare-fun s118 () Int )
(declare-fun s117 () Int )
(declare-fun s119 () Int )
(declare-fun s114 () Int )
(declare-fun s113 () Int )
(declare-fun s116 () Int )
(declare-fun s115 () Int )
(declare-fun a_3_116 () Int )
(declare-fun s154 () Int )
(declare-fun s153 () Int )
(declare-fun s156 () Int )
(declare-fun s155 () Int )
(declare-fun s150 () Int )
(declare-fun s152 () Int )
(declare-fun s151 () Int )
(declare-fun s147 () Int )
(declare-fun s146 () Int )
(declare-fun s149 () Int )
(declare-fun s148 () Int )
(declare-fun s143 () Int )
(declare-fun s142 () Int )
(declare-fun s145 () Int )
(declare-fun s144 () Int )
(declare-fun s141 () Int )
(declare-fun s140 () Int )
(declare-fun s139 () Int )
(declare-fun s136 () Int )
(declare-fun s135 () Int )
(declare-fun s138 () Int )
(declare-fun s137 () Int )
(declare-fun s170 () Int )
(declare-fun a_2_100 () Int )
(declare-fun s176 () Int )
(declare-fun s175 () Int )
(declare-fun s178 () Int )
(declare-fun s177 () Int )
(declare-fun s172 () Int )
(declare-fun s171 () Int )
(declare-fun s174 () Int )
(declare-fun s173 () Int )
(declare-fun a_6_116 () Int )
(declare-fun s169 () Int )
(declare-fun s168 () Int )
(declare-fun s165 () Int )
(declare-fun s164 () Int )
(declare-fun s167 () Int )
(declare-fun s166 () Int )
(declare-fun s161 () Int )
(declare-fun s160 () Int )
(declare-fun s163 () Int )
(declare-fun s162 () Int )
(declare-fun a_2_115 () Int )
(declare-fun a_3_86 () Int )
(declare-fun a_6_102 () Int )
(declare-fun s158 () Int )
(declare-fun s157 () Int )
(declare-fun s159 () Int )
(declare-fun s190 () Int )
(declare-fun s192 () Int )
(declare-fun s191 () Int )
(declare-fun s198 () Int )
(declare-fun s197 () Int )
(declare-fun s199 () Int )
(declare-fun s194 () Int )
(declare-fun s193 () Int )
(declare-fun s196 () Int )
(declare-fun s195 () Int )
(declare-fun a_2_85 () Int )
(declare-fun a_1_115 () Int )
(declare-fun s181 () Int )
(declare-fun s180 () Int )
(declare-fun s187 () Int )
(declare-fun s186 () Int )
(declare-fun s189 () Int )
(declare-fun s188 () Int )
(declare-fun s183 () Int )
(declare-fun s182 () Int )
(declare-fun s185 () Int )
(declare-fun s184 () Int )
(declare-fun a_1_102 () Int )
(declare-fun s179 () Int )
(declare-fun a_5_116 () Int )
(declare-fun s11 () Int )
(declare-fun s10 () Int )
(declare-fun s13 () Int )
(declare-fun s12 () Int )
(declare-fun s15 () Int )
(declare-fun s14 () Int )
(declare-fun s17 () Int )
(declare-fun s16 () Int )
(declare-fun s19 () Int )
(declare-fun s18 () Int )
(declare-fun a_5_102 () Int )
(declare-fun s20 () Int )
(declare-fun s22 () Int )
(declare-fun s21 () Int )
(declare-fun s24 () Int )
(declare-fun s23 () Int )
(declare-fun s26 () Int )
(declare-fun s25 () Int )
(declare-fun s28 () Int )
(declare-fun a_7_85 () Int )
(declare-fun s27 () Int )
(declare-fun s29 () Int )

;formula(s) generated
(assert (and (>= A0 0) (<= A0 1)))
(assert (and (>= A1 0) (<= A1 1)))
(assert (and (>= A2 0) (<= A2 1)))
(assert (and (>= A3 0) (<= A3 1)))
(assert (and (>= A4 0) (<= A4 1)))
(assert (and (>= A5 0) (<= A5 1)))
(assert (and (>= A6 0) (<= A6 1)))
(assert (and (>= A7 0) (<= A7 1)))
(assert (and (>= s0 0) (<= s0 1)))
(assert (and (>= s1 0) (<= s1 1)))
(assert (and (>= s2 0) (<= s2 1)))
(assert (and (>= s3 0) (<= s3 1)))
(assert (and (>= s4 0) (<= s4 1)))
(assert (and (>= s5 0) (<= s5 1)))
(assert (and (>= s6 0) (<= s6 1)))
(assert (and (>= s7 0) (<= s7 1)))
(assert (and (>= s8 0) (<= s8 1)))
(assert (and (>= s9 0) (<= s9 1)))
(assert (and (>= s10 0) (<= s10 1)))
(assert (and (>= s11 0) (<= s11 1)))
(assert (and (>= s12 0) (<= s12 1)))
(assert (and (>= s13 0) (<= s13 1)))
(assert (and (>= s14 0) (<= s14 1)))
(assert (and (>= s15 0) (<= s15 1)))
(assert (and (>= s16 0) (<= s16 1)))
(assert (and (>= s17 0) (<= s17 1)))
(assert (and (>= s18 0) (<= s18 1)))
(assert (and (>= s19 0) (<= s19 1)))
(assert (and (>= s20 0) (<= s20 1)))
(assert (and (>= s21 0) (<= s21 1)))
(assert (and (>= s22 0) (<= s22 1)))
(assert (and (>= s23 0) (<= s23 1)))
(assert (and (>= s24 0) (<= s24 1)))
(assert (and (>= s25 0) (<= s25 1)))
(assert (and (>= s26 0) (<= s26 1)))
(assert (and (>= s27 0) (<= s27 1)))
(assert (and (>= s28 0) (<= s28 1)))
(assert (and (>= s29 0) (<= s29 1)))
(assert (and (>= s30 0) (<= s30 1)))
(assert (and (>= s31 0) (<= s31 1)))
(assert (and (>= s32 0) (<= s32 1)))
(assert (and (>= s33 0) (<= s33 1)))
(assert (and (>= s34 0) (<= s34 1)))
(assert (and (>= s35 0) (<= s35 1)))
(assert (and (>= s36 0) (<= s36 1)))
(assert (and (>= s37 0) (<= s37 1)))
(assert (and (>= s38 0) (<= s38 1)))
(assert (and (>= s39 0) (<= s39 1)))
(assert (and (>= s40 0) (<= s40 1)))
(assert (and (>= s41 0) (<= s41 1)))
(assert (and (>= s42 0) (<= s42 1)))
(assert (and (>= s43 0) (<= s43 1)))
(assert (and (>= s44 0) (<= s44 1)))
(assert (and (>= s45 0) (<= s45 1)))
(assert (and (>= s46 0) (<= s46 1)))
(assert (and (>= s47 0) (<= s47 1)))
(assert (and (>= s48 0) (<= s48 1)))
(assert (and (>= s49 0) (<= s49 1)))
(assert (and (>= s50 0) (<= s50 1)))
(assert (and (>= s51 0) (<= s51 1)))
(assert (and (>= s52 0) (<= s52 1)))
(assert (and (>= s53 0) (<= s53 1)))
(assert (and (>= s54 0) (<= s54 1)))
(assert (and (>= s55 0) (<= s55 1)))
(assert (and (>= s56 0) (<= s56 1)))
(assert (and (>= s57 0) (<= s57 1)))
(assert (and (>= s58 0) (<= s58 1)))
(assert (and (>= s59 0) (<= s59 1)))
(assert (and (>= s60 0) (<= s60 1)))
(assert (and (>= s61 0) (<= s61 1)))
(assert (and (>= s62 0) (<= s62 1)))
(assert (and (>= s63 0) (<= s63 1)))
(assert (and (>= s64 0) (<= s64 1)))
(assert (and (>= s65 0) (<= s65 1)))
(assert (and (>= s66 0) (<= s66 1)))
(assert (and (>= s67 0) (<= s67 1)))
(assert (and (>= s68 0) (<= s68 1)))
(assert (and (>= s69 0) (<= s69 1)))
(assert (and (>= s70 0) (<= s70 1)))
(assert (and (>= s71 0) (<= s71 1)))
(assert (and (>= s72 0) (<= s72 1)))
(assert (and (>= s73 0) (<= s73 1)))
(assert (and (>= s74 0) (<= s74 1)))
(assert (and (>= s75 0) (<= s75 1)))
(assert (and (>= s76 0) (<= s76 1)))
(assert (and (>= s77 0) (<= s77 1)))
(assert (and (>= s78 0) (<= s78 1)))
(assert (and (>= s79 0) (<= s79 1)))
(assert (and (>= s80 0) (<= s80 1)))
(assert (and (>= s81 0) (<= s81 1)))
(assert (and (>= s82 0) (<= s82 1)))
(assert (and (>= s83 0) (<= s83 1)))
(assert (and (>= s84 0) (<= s84 1)))
(assert (and (>= s85 0) (<= s85 1)))
(assert (and (>= s86 0) (<= s86 1)))
(assert (and (>= s87 0) (<= s87 1)))
(assert (and (>= s88 0) (<= s88 1)))
(assert (and (>= s89 0) (<= s89 1)))
(assert (and (>= s90 0) (<= s90 1)))
(assert (and (>= s91 0) (<= s91 1)))
(assert (and (>= s92 0) (<= s92 1)))
(assert (and (>= s93 0) (<= s93 1)))
(assert (and (>= s94 0) (<= s94 1)))
(assert (and (>= s95 0) (<= s95 1)))
(assert (and (>= s96 0) (<= s96 1)))
(assert (and (>= s97 0) (<= s97 1)))
(assert (and (>= s98 0) (<= s98 1)))
(assert (and (>= s99 0) (<= s99 1)))
(assert (and (>= s100 0) (<= s100 1)))
(assert (and (>= s101 0) (<= s101 1)))
(assert (and (>= s102 0) (<= s102 1)))
(assert (and (>= s103 0) (<= s103 1)))
(assert (and (>= s104 0) (<= s104 1)))
(assert (and (>= s105 0) (<= s105 1)))
(assert (and (>= s106 0) (<= s106 1)))
(assert (and (>= s107 0) (<= s107 1)))
(assert (and (>= s108 0) (<= s108 1)))
(assert (and (>= s109 0) (<= s109 1)))
(assert (and (>= s110 0) (<= s110 1)))
(assert (and (>= s111 0) (<= s111 1)))
(assert (and (>= s112 0) (<= s112 1)))
(assert (and (>= s113 0) (<= s113 1)))
(assert (and (>= s114 0) (<= s114 1)))
(assert (and (>= s115 0) (<= s115 1)))
(assert (and (>= s116 0) (<= s116 1)))
(assert (and (>= s117 0) (<= s117 1)))
(assert (and (>= s118 0) (<= s118 1)))
(assert (and (>= s119 0) (<= s119 1)))
(assert (and (>= s120 0) (<= s120 1)))
(assert (and (>= s121 0) (<= s121 1)))
(assert (and (>= s122 0) (<= s122 1)))
(assert (and (>= s123 0) (<= s123 1)))
(assert (and (>= s124 0) (<= s124 1)))
(assert (and (>= s125 0) (<= s125 1)))
(assert (and (>= s126 0) (<= s126 1)))
(assert (and (>= s127 0) (<= s127 1)))
(assert (and (>= s128 0) (<= s128 1)))
(assert (and (>= s129 0) (<= s129 1)))
(assert (and (>= s130 0) (<= s130 1)))
(assert (and (>= s131 0) (<= s131 1)))
(assert (and (>= s132 0) (<= s132 1)))
(assert (and (>= s133 0) (<= s133 1)))
(assert (and (>= s134 0) (<= s134 1)))
(assert (and (>= s135 0) (<= s135 1)))
(assert (and (>= s136 0) (<= s136 1)))
(assert (and (>= s137 0) (<= s137 1)))
(assert (and (>= s138 0) (<= s138 1)))
(assert (and (>= s139 0) (<= s139 1)))
(assert (and (>= s140 0) (<= s140 1)))
(assert (and (>= s141 0) (<= s141 1)))
(assert (and (>= s142 0) (<= s142 1)))
(assert (and (>= s143 0) (<= s143 1)))
(assert (and (>= s144 0) (<= s144 1)))
(assert (and (>= s145 0) (<= s145 1)))
(assert (and (>= s146 0) (<= s146 1)))
(assert (and (>= s147 0) (<= s147 1)))
(assert (and (>= s148 0) (<= s148 1)))
(assert (and (>= s149 0) (<= s149 1)))
(assert (and (>= s150 0) (<= s150 1)))
(assert (and (>= s151 0) (<= s151 1)))
(assert (and (>= s152 0) (<= s152 1)))
(assert (and (>= s153 0) (<= s153 1)))
(assert (and (>= s154 0) (<= s154 1)))
(assert (and (>= s155 0) (<= s155 1)))
(assert (and (>= s156 0) (<= s156 1)))
(assert (and (>= s157 0) (<= s157 1)))
(assert (and (>= s158 0) (<= s158 1)))
(assert (and (>= s159 0) (<= s159 1)))
(assert (and (>= s160 0) (<= s160 1)))
(assert (and (>= s161 0) (<= s161 1)))
(assert (and (>= s162 0) (<= s162 1)))
(assert (and (>= s163 0) (<= s163 1)))
(assert (and (>= s164 0) (<= s164 1)))
(assert (and (>= s165 0) (<= s165 1)))
(assert (and (>= s166 0) (<= s166 1)))
(assert (and (>= s167 0) (<= s167 1)))
(assert (and (>= s168 0) (<= s168 1)))
(assert (and (>= s169 0) (<= s169 1)))
(assert (and (>= s170 0) (<= s170 1)))
(assert (and (>= s171 0) (<= s171 1)))
(assert (and (>= s172 0) (<= s172 1)))
(assert (and (>= s173 0) (<= s173 1)))
(assert (and (>= s174 0) (<= s174 1)))
(assert (and (>= s175 0) (<= s175 1)))
(assert (and (>= s176 0) (<= s176 1)))
(assert (and (>= s177 0) (<= s177 1)))
(assert (and (>= s178 0) (<= s178 1)))
(assert (and (>= s179 0) (<= s179 1)))
(assert (and (>= s180 0) (<= s180 1)))
(assert (and (>= s181 0) (<= s181 1)))
(assert (and (>= s182 0) (<= s182 1)))
(assert (and (>= s183 0) (<= s183 1)))
(assert (and (>= s184 0) (<= s184 1)))
(assert (and (>= s185 0) (<= s185 1)))
(assert (and (>= s186 0) (<= s186 1)))
(assert (and (>= s187 0) (<= s187 1)))
(assert (and (>= s188 0) (<= s188 1)))
(assert (and (>= s189 0) (<= s189 1)))
(assert (and (>= s190 0) (<= s190 1)))
(assert (and (>= s191 0) (<= s191 1)))
(assert (and (>= s192 0) (<= s192 1)))
(assert (and (>= s193 0) (<= s193 1)))
(assert (and (>= s194 0) (<= s194 1)))
(assert (and (>= s195 0) (<= s195 1)))
(assert (and (>= s196 0) (<= s196 1)))
(assert (and (>= s197 0) (<= s197 1)))
(assert (and (>= s198 0) (<= s198 1)))
(assert (and (>= s199 0) (<= s199 1)))
(assert (and (>= s200 0) (<= s200 1)))
(assert (and (>= s201 0) (<= s201 1)))
(assert (and (>= s202 0) (<= s202 1)))
(assert (and (>= s203 0) (<= s203 1)))
(assert (and (>= s204 0) (<= s204 1)))
(assert (and (>= s205 0) (<= s205 1)))
(assert (and (>= s206 0) (<= s206 1)))
(assert (and (>= s207 0) (<= s207 1)))
(assert (and (>= s208 0) (<= s208 1)))
(assert (and (>= s209 0) (<= s209 1)))
(assert (and (>= a_0_86 0) (<= a_0_86 1)))
(assert (and (>= a_0_100 0) (<= a_0_100 1)))
(assert (and (>= a_0_115 0) (<= a_0_115 1)))
(assert (and (>= a_1_86 0) (<= a_1_86 1)))
(assert (and (>= a_1_102 0) (<= a_1_102 1)))
(assert (and (>= a_1_115 0) (<= a_1_115 1)))
(assert (and (>= a_2_85 0) (<= a_2_85 1)))
(assert (and (>= a_2_100 0) (<= a_2_100 1)))
(assert (and (>= a_2_115 0) (<= a_2_115 1)))
(assert (and (>= a_3_86 0) (<= a_3_86 1)))
(assert (and (>= a_3_100 0) (<= a_3_100 1)))
(assert (and (>= a_3_116 0) (<= a_3_116 1)))
(assert (and (>= a_4_85 0) (<= a_4_85 1)))
(assert (and (>= a_4_102 0) (<= a_4_102 1)))
(assert (and (>= a_4_115 0) (<= a_4_115 1)))
(assert (and (>= a_5_86 0) (<= a_5_86 1)))
(assert (and (>= a_5_102 0) (<= a_5_102 1)))
(assert (and (>= a_5_116 0) (<= a_5_116 1)))
(assert (and (>= a_6_85 0) (<= a_6_85 1)))
(assert (and (>= a_6_102 0) (<= a_6_102 1)))
(assert (and (>= a_6_116 0) (<= a_6_116 1)))
(assert (and (>= a_7_85 0) (<= a_7_85 1)))
(assert (and (>= a_7_100 0) (<= a_7_100 1)))
(assert (and (>= a_7_116 0) (<= a_7_116 1)))
(assert (= s0 0))
(assert (= s1 0))
(assert (= s2 0))
(assert (= s3 0))
(assert (= s4 0))
(assert (= s5 0))
(assert (= s6 0))
(assert (= s7 0))
(assert (= s8 0))
(assert (= s9 0))
(assert (= s10 0))
(assert (= s11 0))
(assert (= s12 0))
(assert (= s13 0))
(assert (= s14 0))
(assert (= s15 0))
(assert (= s16 0))
(assert (= s17 0))
(assert (= s18 0))
(assert (= s19 0))
(assert (= s20 0))
(assert (= s21 0))
(assert (= s22 0))
(assert (= s23 0))
(assert (= s24 0))
(assert (= s25 0))
(assert (= s26 0))
(assert (= s27 0))
(assert (= s28 0))
(assert (= s29 0))
(assert (= s30 0))
(assert (= s31 0))
(assert (= s32 0))
(assert (= s33 0))
(assert (= s34 0))
(assert (= s35 0))
(assert (= s36 0))
(assert (= s37 0))
(assert (= s38 0))
(assert (= s39 0))
(assert (= s40 0))
(assert (= s41 0))
(assert (= s42 0))
(assert (= s43 0))
(assert (= s44 0))
(assert (= s45 0))
(assert (= s46 0))
(assert (= s47 0))
(assert (= s48 0))
(assert (= s49 0))
(assert (= s50 0))
(assert (= s51 0))
(assert (= s52 0))
(assert (= s53 0))
(assert (= s54 0))
(assert (= s55 0))
(assert (= s56 0))
(assert (= s57 0))
(assert (= s58 0))
(assert (= s59 0))
(assert (= s60 0))
(assert (= s61 0))
(assert (= s62 0))
(assert (= s63 0))
(assert (= s64 0))
(assert (= s65 0))
(assert (= s66 0))
(assert (= s67 0))
(assert (= s68 0))
(assert (= s69 0))
(assert (= s70 0))
(assert (= s71 0))
(assert (= s72 0))
(assert (= s73 0))
(assert (= s74 0))
(assert (= s75 0))
(assert (= s76 0))
(assert (= s77 0))
(assert (= s78 0))
(assert (= s79 0))
(assert (= s80 0))
(assert (= s81 0))
(assert (= s82 0))
(assert (= s83 0))
(assert (= s84 0))
(assert (=> (= s85 1) (and (and (and (= a_2_85 1) (= a_4_85 1)) (= a_6_85 1)) (= a_7_85 1))))
(assert (=> (= s85 0) (and (and (and (= a_2_85 0) (= a_4_85 0)) (= a_6_85 0)) (= a_7_85 0))))
(assert (=> (= s86 1) (and (and (and (= a_0_86 1) (= a_1_86 1)) (= a_3_86 1)) (= a_5_86 1))))
(assert (=> (= s86 0) (and (and (and (= a_0_86 0) (= a_1_86 0)) (= a_3_86 0)) (= a_5_86 0))))
(assert (= s87 0))
(assert (= s88 0))
(assert (= s89 0))
(assert (= s90 0))
(assert (= s91 0))
(assert (= s92 0))
(assert (= s93 0))
(assert (= s94 0))
(assert (= s95 0))
(assert (= s96 0))
(assert (= s97 0))
(assert (= s98 0))
(assert (= s99 0))
(assert (=> (= s100 1) (and (and (and (= a_0_100 1) (= a_2_100 1)) (= a_3_100 1)) (= a_7_100 1))))
(assert (=> (= s100 0) (and (and (and (= a_0_100 0) (= a_2_100 0)) (= a_3_100 0)) (= a_7_100 0))))
(assert (= s101 0))
(assert (=> (= s102 1) (and (and (and (= a_1_102 1) (= a_4_102 1)) (= a_5_102 1)) (= a_6_102 1))))
(assert (=> (= s102 0) (and (and (and (= a_1_102 0) (= a_4_102 0)) (= a_5_102 0)) (= a_6_102 0))))
(assert (= s103 0))
(assert (= s104 0))
(assert (= s105 0))
(assert (= s106 0))
(assert (= s107 0))
(assert (= s108 0))
(assert (= s109 0))
(assert (= s110 0))
(assert (= s111 0))
(assert (= s112 0))
(assert (= s113 0))
(assert (= s114 0))
(assert (=> (= s115 1) (and (and (and (= a_0_115 1) (= a_1_115 1)) (= a_2_115 1)) (= a_4_115 1))))
(assert (=> (= s115 0) (and (and (and (= a_0_115 0) (= a_1_115 0)) (= a_2_115 0)) (= a_4_115 0))))
(assert (=> (= s116 1) (and (and (and (= a_3_116 1) (= a_5_116 1)) (= a_6_116 1)) (= a_7_116 1))))
(assert (=> (= s116 0) (and (and (and (= a_3_116 0) (= a_5_116 0)) (= a_6_116 0)) (= a_7_116 0))))
(assert (= s117 0))
(assert (= s118 0))
(assert (= s119 0))
(assert (= s120 0))
(assert (= s121 0))
(assert (= s122 0))
(assert (= s123 0))
(assert (= s124 0))
(assert (= s125 0))
(assert (= s126 0))
(assert (= s127 0))
(assert (= s128 0))
(assert (= s129 0))
(assert (= s130 0))
(assert (= s131 0))
(assert (= s132 0))
(assert (= s133 0))
(assert (= s134 0))
(assert (= s135 0))
(assert (= s136 0))
(assert (= s137 0))
(assert (= s138 0))
(assert (= s139 0))
(assert (= s140 0))
(assert (= s141 0))
(assert (= s142 0))
(assert (= s143 0))
(assert (= s144 0))
(assert (= s145 0))
(assert (= s146 0))
(assert (= s147 0))
(assert (= s148 0))
(assert (= s149 0))
(assert (= s150 0))
(assert (= s151 0))
(assert (= s152 0))
(assert (= s153 0))
(assert (= s154 0))
(assert (= s155 0))
(assert (= s156 0))
(assert (= s157 0))
(assert (= s158 0))
(assert (= s159 0))
(assert (= s160 0))
(assert (= s161 0))
(assert (= s162 0))
(assert (= s163 0))
(assert (= s164 0))
(assert (= s165 0))
(assert (= s166 0))
(assert (= s167 0))
(assert (= s168 0))
(assert (= s169 0))
(assert (= s170 0))
(assert (= s171 0))
(assert (= s172 0))
(assert (= s173 0))
(assert (= s174 0))
(assert (= s175 0))
(assert (= s176 0))
(assert (= s177 0))
(assert (= s178 0))
(assert (= s179 0))
(assert (= s180 0))
(assert (= s181 0))
(assert (= s182 0))
(assert (= s183 0))
(assert (= s184 0))
(assert (= s185 0))
(assert (= s186 0))
(assert (= s187 0))
(assert (= s188 0))
(assert (= s189 0))
(assert (= s190 0))
(assert (= s191 0))
(assert (= s192 0))
(assert (= s193 0))
(assert (= s194 0))
(assert (= s195 0))
(assert (= s196 0))
(assert (= s197 0))
(assert (= s198 0))
(assert (= s199 0))
(assert (= s200 0))
(assert (= s201 0))
(assert (= s202 0))
(assert (= s203 0))
(assert (= s204 0))
(assert (= s205 0))
(assert (= s206 0))
(assert (= s207 0))
(assert (= s208 0))
(assert (= s209 0))
(assert (=> (or (or (= a_0_86 1) (= a_0_100 1)) (= a_0_115 1)) (= A0 1)))
(assert (=> (and (and (= a_0_86 0) (= a_0_100 0)) (= a_0_115 0)) (= A0 0)))
(assert (=> (or (or (= a_1_86 1) (= a_1_102 1)) (= a_1_115 1)) (= A1 1)))
(assert (=> (and (and (= a_1_86 0) (= a_1_102 0)) (= a_1_115 0)) (= A1 0)))
(assert (=> (or (or (= a_2_85 1) (= a_2_100 1)) (= a_2_115 1)) (= A2 1)))
(assert (=> (and (and (= a_2_85 0) (= a_2_100 0)) (= a_2_115 0)) (= A2 0)))
(assert (=> (or (or (= a_3_86 1) (= a_3_100 1)) (= a_3_116 1)) (= A3 1)))
(assert (=> (and (and (= a_3_86 0) (= a_3_100 0)) (= a_3_116 0)) (= A3 0)))
(assert (=> (or (or (= a_4_85 1) (= a_4_102 1)) (= a_4_115 1)) (= A4 1)))
(assert (=> (and (and (= a_4_85 0) (= a_4_102 0)) (= a_4_115 0)) (= A4 0)))
(assert (=> (or (or (= a_5_86 1) (= a_5_102 1)) (= a_5_116 1)) (= A5 1)))
(assert (=> (and (and (= a_5_86 0) (= a_5_102 0)) (= a_5_116 0)) (= A5 0)))
(assert (=> (or (or (= a_6_85 1) (= a_6_102 1)) (= a_6_116 1)) (= A6 1)))
(assert (=> (and (and (= a_6_85 0) (= a_6_102 0)) (= a_6_116 0)) (= A6 0)))
(assert (=> (or (or (= a_7_85 1) (= a_7_100 1)) (= a_7_116 1)) (= A7 1)))
(assert (=> (and (and (= a_7_85 0) (= a_7_100 0)) (= a_7_116 0)) (= A7 0)))
(assert (= (+ (+ (+ (+ (+ (+ (+ A0 A1) A2) A3) A4) A5) A6) A7) 8))
(assert (not (and (= s85 1) (= s86 1)) ))
(assert (not (and (= s100 1) (= s102 1)) ))
(assert (not (and (= s115 1) (= s116 1)) ))
(assert (= (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ s0 s1) s2) s3) s4) s5) s6) s7) s8) s9) s10) s11) s12) s13) s14) s15) s16) s17) s18) s19) s20) s21) s22) s23) s24) s25) s26) s27) s28) s29) s30) s31) s32) s33) s34) s35) s36) s37) s38) s39) s40) s41) s42) s43) s44) s45) s46) s47) s48) s49) s50) s51) s52) s53) s54) s55) s56) s57) s58) s59) s60) s61) s62) s63) s64) s65) s66) s67) s68) s69) s70) s71) s72) s73) s74) s75) s76) s77) s78) s79) s80) s81) s82) s83) s84) s85) s86) s87) s88) s89) s90) s91) s92) s93) s94) s95) s96) s97) s98) s99) s100) s101) s102) s103) s104) s105) s106) s107) s108) s109) s110) s111) s112) s113) s114) s115) s116) s117) s118) s119) s120) s121) s122) s123) s124) s125) s126) s127) s128) s129) s130) s131) s132) s133) s134) s135) s136) s137) s138) s139) s140) s141) s142) s143) s144) s145) s146) s147) s148) s149) s150) s151) s152) s153) s154) s155) s156) s157) s158) s159) s160) s161) s162) s163) s164) s165) s166) s167) s168) s169) s170) s171) s172) s173) s174) s175) s176) s177) s178) s179) s180) s181) s182) s183) s184) s185) s186) s187) s188) s189) s190) s191) s192) s193) s194) s195) s196) s197) s198) s199) s200) s201) s202) s203) s204) s205) s206) s207) s208) s209) 211))