% /homes/demoura/tmp/fischer-bruno2.ics
% Unsatisfiable
reset.
prop a_0 := [~ [x_0 < 0]] .
prop a_1 := x_0 <= 2 .
prop a_2 := [~ [x_1 < 0]] .
prop a_3 := x_1 <= 2 .
prop a_4 := [~ [x_2 < 0]] .
prop a_5 := x_2 <= 2 .
prop a_6 := [~ [x_3 < 0]] .
prop a_7 := x_3 <= 2 .
prop a_8 := [~ [x_4 < 0]] .
prop a_9 := x_4 <= 2 .
prop a_10 := [~ [x_5 < 0]] .
prop a_11 := x_5 <= 2 .
prop a_12 := [~ [x_6 < 0]] .
prop a_13 := x_6 <= 2 .
prop a_14 := [~ [x_7 < 0]] .
prop a_15 := x_7 <= 2 .
prop a_16 := [~ [x_8 < 0]] .
prop a_17 := x_8 <= 2 .
prop a_18 := [~ [x_9 < 0]] .
prop a_19 := x_9 <= 2 .
prop a_20 := [~ [x_10 < 0]] .
prop a_21 := x_10 <= 2 .
prop a_22 := x_11 = 0 .
prop a_23 := [[~ x_12]] & [[~ x_13]] .
prop a_24 := [[~ x_14]] & [[~ x_15]] .
prop a_25 := x_11 < x_16 .
prop a_26 := x_11 < x_17 .
prop a_27 := x_0 = 0 .
prop x_18 := x_9 <> 0 .
prop x_19 := x_20 = 3 .
prop x_21 := x_9 = 0 .
prop x_22 := x_20 = 2 .
prop x_23 := x_10 = 0 .
prop x_24 := x_20 = 5 .
prop a_28 := x_25 = (x_26 + 2) .
prop a_29 := x_27 = (x_26 + 3) .
prop x_28 := x_20 = 4 .
prop x_29 := x_20 = 0 .
prop x_30 := [[~ x_31]] & [[~ x_32]] .
prop x_33 := [[~ x_34]] & [[~ x_35]] .
prop x_36 := x_10 = x_9 .
prop x_37 := x_20 = 1 .
prop x_38 := [[~ x_39]] & [[~ x_40]] .
prop x_41 := [[~ x_39]] & x_40 .
prop x_42 := [[~ x_43]] & [[~ x_44]] .
prop x_45 := x_26 = x_46 .
prop x_47 := x_48 = x_46 .
prop x_49 := x_26 < x_50 .
prop x_51 := [x_34 <=> x_43] & [x_35 <=> x_44] .
prop x_52 := x_26 < x_48 .
prop x_53 := x_26 = x_54 .
prop x_55 := [x_31 <=> x_39] & [x_32 <=> x_40] .
prop x_56 := [[~ x_43]] & x_44 .
prop x_57 := x_50 = x_54 .
prop a_30 := if [x_46 < x_54] then [x_58 = x_46] else [x_58 = x_54] end .
prop a_31 := x_59 = x_58 .
prop x_60 := x_8 <> 0 .
prop x_61 := x_62 = 3 .
prop x_63 := x_8 = 0 .
prop x_64 := x_62 = 2 .
prop x_65 := x_9 = 0 .
prop x_66 := x_62 = 5 .
prop a_32 := x_67 = (x_68 + 2) .
prop a_33 := x_69 = (x_68 + 3) .
prop x_70 := x_62 = 4 .
prop x_71 := x_62 = 0 .
prop x_72 := [[~ x_39]] & [[~ x_40]] .
prop x_73 := [[~ x_43]] & [[~ x_44]] .
prop x_74 := x_9 = x_8 .
prop x_75 := x_62 = 1 .
prop x_76 := [[~ x_77]] & [[~ x_78]] .
prop x_79 := [[~ x_77]] & x_78 .
prop x_80 := [[~ x_81]] & [[~ x_82]] .
prop x_83 := x_68 = x_84 .
prop x_85 := x_46 = x_84 .
prop x_86 := x_68 < x_54 .
prop x_87 := [x_43 <=> x_81] & [x_44 <=> x_82] .
prop x_88 := x_68 < x_46 .
prop x_89 := x_68 = x_90 .
prop x_91 := [x_39 <=> x_77] & [x_40 <=> x_78] .
prop x_92 := [[~ x_81]] & x_82 .
prop x_93 := x_54 = x_90 .
prop a_34 := if [x_84 < x_90] then [x_94 = x_84] else [x_94 = x_90] end .
prop a_35 := x_95 = x_94 .
prop x_96 := x_7 <> 0 .
prop x_97 := x_98 = 3 .
prop x_99 := x_7 = 0 .
prop x_100 := x_98 = 2 .
prop x_101 := x_8 = 0 .
prop x_102 := x_98 = 5 .
prop a_36 := x_103 = (x_104 + 2) .
prop a_37 := x_105 = (x_104 + 3) .
prop x_106 := x_98 = 4 .
prop x_107 := x_98 = 0 .
prop x_108 := [[~ x_77]] & [[~ x_78]] .
prop x_109 := [[~ x_81]] & [[~ x_82]] .
prop x_110 := x_8 = x_7 .
prop x_111 := x_98 = 1 .
prop x_112 := [[~ x_113]] & [[~ x_114]] .
prop x_115 := [[~ x_113]] & x_114 .
prop x_116 := [[~ x_117]] & [[~ x_118]] .
prop x_119 := x_104 = x_120 .
prop x_121 := x_84 = x_120 .
prop x_122 := x_104 < x_90 .
prop x_123 := [x_81 <=> x_117] & [x_82 <=> x_118] .
prop x_124 := x_104 < x_84 .
prop x_125 := x_104 = x_126 .
prop x_127 := [x_77 <=> x_113] & [x_78 <=> x_114] .
prop x_128 := [[~ x_117]] & x_118 .
prop x_129 := x_90 = x_126 .
prop a_38 := if [x_120 < x_126] then [x_130 = x_120] else [x_130 = x_126] end .
prop a_39 := x_131 = x_130 .
prop x_132 := x_6 <> 0 .
prop x_133 := x_134 = 3 .
prop x_135 := x_6 = 0 .
prop x_136 := x_134 = 2 .
prop x_137 := x_7 = 0 .
prop x_138 := x_134 = 5 .
prop a_40 := x_139 = (x_140 + 2) .
prop a_41 := x_141 = (x_140 + 3) .
prop x_142 := x_134 = 4 .
prop x_143 := x_134 = 0 .
prop x_144 := [[~ x_113]] & [[~ x_114]] .
prop x_145 := [[~ x_117]] & [[~ x_118]] .
prop x_146 := x_7 = x_6 .
prop x_147 := x_134 = 1 .
prop x_148 := [[~ x_149]] & [[~ x_150]] .
prop x_151 := [[~ x_149]] & x_150 .
prop x_152 := [[~ x_153]] & [[~ x_154]] .
prop x_155 := x_140 = x_156 .
prop x_157 := x_120 = x_156 .
prop x_158 := x_140 < x_126 .
prop x_159 := [x_117 <=> x_153] & [x_118 <=> x_154] .
prop x_160 := x_140 < x_120 .
prop x_161 := x_140 = x_162 .
prop x_163 := [x_113 <=> x_149] & [x_114 <=> x_150] .
prop x_164 := [[~ x_153]] & x_154 .
prop x_165 := x_126 = x_162 .
prop a_42 := if [x_156 < x_162] then [x_166 = x_156] else [x_166 = x_162] end .
prop a_43 := x_167 = x_166 .
prop x_168 := x_5 <> 0 .
prop x_169 := x_170 = 3 .
prop x_171 := x_5 = 0 .
prop x_172 := x_170 = 2 .
prop x_173 := x_6 = 0 .
prop x_174 := x_170 = 5 .
prop a_44 := x_175 = (x_176 + 2) .
prop a_45 := x_177 = (x_176 + 3) .
prop x_178 := x_170 = 4 .
prop x_179 := x_170 = 0 .
prop x_180 := [[~ x_149]] & [[~ x_150]] .
prop x_181 := [[~ x_153]] & [[~ x_154]] .
prop x_182 := x_6 = x_5 .
prop x_183 := x_170 = 1 .
prop x_184 := [[~ x_185]] & [[~ x_186]] .
prop x_187 := [[~ x_185]] & x_186 .
prop x_188 := [[~ x_189]] & [[~ x_190]] .
prop x_191 := x_176 = x_192 .
prop x_193 := x_156 = x_192 .
prop x_194 := x_176 < x_162 .
prop x_195 := [x_153 <=> x_189] & [x_154 <=> x_190] .
prop x_196 := x_176 < x_156 .
prop x_197 := x_176 = x_198 .
prop x_199 := [x_149 <=> x_185] & [x_150 <=> x_186] .
prop x_200 := [[~ x_189]] & x_190 .
prop x_201 := x_162 = x_198 .
prop a_46 := if [x_192 < x_198] then [x_202 = x_192] else [x_202 = x_198] end .
prop a_47 := x_203 = x_202 .
prop x_204 := x_4 <> 0 .
prop x_205 := x_206 = 3 .
prop x_207 := x_4 = 0 .
prop x_208 := x_206 = 2 .
prop x_209 := x_5 = 0 .
prop x_210 := x_206 = 5 .
prop a_48 := x_211 = (x_212 + 2) .
prop a_49 := x_213 = (x_212 + 3) .
prop x_214 := x_206 = 4 .
prop x_215 := x_206 = 0 .
prop x_216 := [[~ x_185]] & [[~ x_186]] .
prop x_217 := [[~ x_189]] & [[~ x_190]] .
prop x_218 := x_5 = x_4 .
prop x_219 := x_206 = 1 .
prop x_220 := [[~ x_221]] & [[~ x_222]] .
prop x_223 := [[~ x_221]] & x_222 .
prop x_224 := [[~ x_225]] & [[~ x_226]] .
prop x_227 := x_212 = x_228 .
prop x_229 := x_192 = x_228 .
prop x_230 := x_212 < x_198 .
prop x_231 := [x_189 <=> x_225] & [x_190 <=> x_226] .
prop x_232 := x_212 < x_192 .
prop x_233 := x_212 = x_234 .
prop x_235 := [x_185 <=> x_221] & [x_186 <=> x_222] .
prop x_236 := [[~ x_225]] & x_226 .
prop x_237 := x_198 = x_234 .
prop a_50 := if [x_228 < x_234] then [x_238 = x_228] else [x_238 = x_234] end .
prop a_51 := x_239 = x_238 .
prop x_240 := x_3 <> 0 .
prop x_241 := x_242 = 3 .
prop x_243 := x_3 = 0 .
prop x_244 := x_242 = 2 .
prop x_245 := x_4 = 0 .
prop x_246 := x_242 = 5 .
prop a_52 := x_247 = (x_248 + 2) .
prop a_53 := x_249 = (x_248 + 3) .
prop x_250 := x_242 = 4 .
prop x_251 := x_242 = 0 .
prop x_252 := [[~ x_221]] & [[~ x_222]] .
prop x_253 := [[~ x_225]] & [[~ x_226]] .
prop x_254 := x_4 = x_3 .
prop x_255 := x_242 = 1 .
prop x_256 := [[~ x_257]] & [[~ x_258]] .
prop x_259 := [[~ x_257]] & x_258 .
prop x_260 := [[~ x_261]] & [[~ x_262]] .
prop x_263 := x_248 = x_264 .
prop x_265 := x_228 = x_264 .
prop x_266 := x_248 < x_234 .
prop x_267 := [x_225 <=> x_261] & [x_226 <=> x_262] .
prop x_268 := x_248 < x_228 .
prop x_269 := x_248 = x_270 .
prop x_271 := [x_221 <=> x_257] & [x_222 <=> x_258] .
prop x_272 := [[~ x_261]] & x_262 .
prop x_273 := x_234 = x_270 .
prop a_54 := if [x_264 < x_270] then [x_274 = x_264] else [x_274 = x_270] end .
prop a_55 := x_275 = x_274 .
prop x_276 := x_2 <> 0 .
prop x_277 := x_278 = 3 .
prop x_279 := x_2 = 0 .
prop x_280 := x_278 = 2 .
prop x_281 := x_3 = 0 .
prop x_282 := x_278 = 5 .
prop a_56 := x_283 = (x_284 + 2) .
prop a_57 := x_285 = (x_284 + 3) .
prop x_286 := x_278 = 4 .
prop x_287 := x_278 = 0 .
prop x_288 := [[~ x_257]] & [[~ x_258]] .
prop x_289 := [[~ x_261]] & [[~ x_262]] .
prop x_290 := x_3 = x_2 .
prop x_291 := x_278 = 1 .
prop x_292 := [[~ x_293]] & [[~ x_294]] .
prop x_295 := [[~ x_293]] & x_294 .
prop x_296 := [[~ x_297]] & [[~ x_298]] .
prop x_299 := x_284 = x_300 .
prop x_301 := x_264 = x_300 .
prop x_302 := x_284 < x_270 .
prop x_303 := [x_261 <=> x_297] & [x_262 <=> x_298] .
prop x_304 := x_284 < x_264 .
prop x_305 := x_284 = x_306 .
prop x_307 := [x_257 <=> x_293] & [x_258 <=> x_294] .
prop x_308 := [[~ x_297]] & x_298 .
prop x_309 := x_270 = x_306 .
prop a_58 := if [x_300 < x_306] then [x_310 = x_300] else [x_310 = x_306] end .
prop a_59 := x_311 = x_310 .
prop x_312 := x_1 <> 0 .
prop x_313 := x_314 = 3 .
prop x_315 := x_1 = 0 .
prop x_316 := x_314 = 2 .
prop x_317 := x_2 = 0 .
prop x_318 := x_314 = 5 .
prop a_60 := x_319 = (x_320 + 2) .
prop a_61 := x_321 = (x_320 + 3) .
prop x_322 := x_314 = 4 .
prop x_323 := x_314 = 0 .
prop x_324 := [[~ x_293]] & [[~ x_294]] .
prop x_325 := [[~ x_297]] & [[~ x_298]] .
prop x_326 := x_2 = x_1 .
prop x_327 := x_314 = 1 .
prop x_328 := [[~ x_329]] & [[~ x_330]] .
prop x_331 := [[~ x_329]] & x_330 .
prop x_332 := [[~ x_333]] & [[~ x_334]] .
prop x_335 := x_320 = x_336 .
prop x_337 := x_300 = x_336 .
prop x_338 := x_320 < x_306 .
prop x_339 := [x_297 <=> x_333] & [x_298 <=> x_334] .
prop x_340 := x_320 < x_300 .
prop x_341 := x_320 = x_342 .
prop x_343 := [x_293 <=> x_329] & [x_294 <=> x_330] .
prop x_344 := [[~ x_333]] & x_334 .
prop x_345 := x_306 = x_342 .
prop a_62 := if [x_336 < x_342] then [x_346 = x_336] else [x_346 = x_342] end .
prop a_63 := x_347 = x_346 .
prop x_348 := x_0 <> 0 .
prop x_349 := x_350 = 3 .
prop x_351 := x_0 = 0 .
prop x_352 := x_350 = 2 .
prop x_353 := x_1 = 0 .
prop x_354 := x_350 = 5 .
prop a_64 := x_355 = (x_11 + 2) .
prop a_65 := x_356 = (x_11 + 3) .
prop x_357 := x_350 = 4 .
prop x_358 := x_350 = 0 .
prop x_359 := [[~ x_329]] & [[~ x_330]] .
prop x_360 := [[~ x_333]] & [[~ x_334]] .
prop x_361 := x_1 = x_0 .
prop x_362 := x_350 = 1 .
prop x_363 := [[~ x_12]] & [[~ x_13]] .
prop x_364 := [[~ x_12]] & x_13 .
prop x_365 := [[~ x_14]] & [[~ x_15]] .
prop x_366 := x_11 = x_17 .
prop x_367 := x_336 = x_17 .
prop x_368 := x_11 < x_342 .
prop x_369 := [x_333 <=> x_14] & [x_334 <=> x_15] .
prop x_370 := x_11 < x_336 .
prop x_371 := x_11 = x_16 .
prop x_372 := [x_329 <=> x_12] & [x_330 <=> x_13] .
prop x_373 := [[~ x_14]] & x_15 .
prop x_374 := x_342 = x_16 .
prop a_66 := if [x_17 < x_16] then [x_375 = x_17] else [x_375 = x_16] end .
prop a_67 := x_376 = x_375 .
prop a_68 := [[x_377 = 0] & [x_26 < x_59] & [x_378 = x_59] & x_55 & x_51 & x_57 & x_47 & x_36] | [[x_377 = 1] & [[[x_379 = 1] & [[x_29 & x_38 & x_53 & x_21 & x_31 & [[~ x_32]] & [x_26 < x_50] & [x_50 <= x_25] & x_36] | [x_37 & x_38 & x_53 & x_18 & x_49 & x_36 & x_55] | [x_22 & x_39 & [[~ x_40]] & x_53 & [[~ x_31]] & x_32 & [x_10 = 1] & [x_27 <= x_50]] | [x_19 & x_41 & x_53 & [x_9 = 1] & x_31 & x_32 & x_49 & x_36] | [x_28 & x_41 & x_53 & [x_9 <> 1] & x_30 & x_49 & x_36] | [x_24 & x_39 & x_40 & x_53 & x_30 & x_23 & x_49]] & x_51 & x_47] | [[x_379 = 2] & [[x_29 & x_42 & x_45 & x_21 & x_34 & [[~ x_35]] & [x_26 < x_48] & [x_48 <= x_25] & x_36] | [x_37 & x_42 & x_45 & x_18 & x_52 & x_36 & x_51] | [x_22 & x_43 & [[~ x_44]] & x_45 & [[~ x_34]] & x_35 & [x_10 = 2] & [x_27 <= x_48]] | [x_19 & x_56 & x_45 & [x_9 = 2] & x_34 & x_35 & x_52 & x_36] | [x_28 & x_56 & x_45 & [x_9 <> 2] & x_33 & x_52 & x_36] | [x_24 & x_43 & x_44 & x_45 & x_33 & x_23 & x_52]] & x_55 & x_57]] & [x_378 = x_26]] .
prop a_69 := [[x_380 = 0] & [x_68 < x_95] & [x_26 = x_95] & x_91 & x_87 & x_93 & x_85 & x_74] | [[x_380 = 1] & [[[x_381 = 1] & [[x_71 & x_76 & x_89 & x_63 & x_39 & [[~ x_40]] & [x_68 < x_54] & [x_54 <= x_67] & x_74] | [x_75 & x_76 & x_89 & x_60 & x_86 & x_74 & x_91] | [x_64 & x_77 & [[~ x_78]] & x_89 & [[~ x_39]] & x_40 & [x_9 = 1] & [x_69 <= x_54]] | [x_61 & x_79 & x_89 & [x_8 = 1] & x_39 & x_40 & x_86 & x_74] | [x_70 & x_79 & x_89 & [x_8 <> 1] & x_72 & x_86 & x_74] | [x_66 & x_77 & x_78 & x_89 & x_72 & x_65 & x_86]] & x_87 & x_85] | [[x_381 = 2] & [[x_71 & x_80 & x_83 & x_63 & x_43 & [[~ x_44]] & [x_68 < x_46] & [x_46 <= x_67] & x_74] | [x_75 & x_80 & x_83 & x_60 & x_88 & x_74 & x_87] | [x_64 & x_81 & [[~ x_82]] & x_83 & [[~ x_43]] & x_44 & [x_9 = 2] & [x_69 <= x_46]] | [x_61 & x_92 & x_83 & [x_8 = 2] & x_43 & x_44 & x_88 & x_74] | [x_70 & x_92 & x_83 & [x_8 <> 2] & x_73 & x_88 & x_74] | [x_66 & x_81 & x_82 & x_83 & x_73 & x_65 & x_88]] & x_91 & x_93]] & [x_26 = x_68]] .
prop a_70 := [[x_382 = 0] & [x_104 < x_131] & [x_68 = x_131] & x_127 & x_123 & x_129 & x_121 & x_110] | [[x_382 = 1] & [[[x_383 = 1] & [[x_107 & x_112 & x_125 & x_99 & x_77 & [[~ x_78]] & [x_104 < x_90] & [x_90 <= x_103] & x_110] | [x_111 & x_112 & x_125 & x_96 & x_122 & x_110 & x_127] | [x_100 & x_113 & [[~ x_114]] & x_125 & [[~ x_77]] & x_78 & [x_8 = 1] & [x_105 <= x_90]] | [x_97 & x_115 & x_125 & [x_7 = 1] & x_77 & x_78 & x_122 & x_110] | [x_106 & x_115 & x_125 & [x_7 <> 1] & x_108 & x_122 & x_110] | [x_102 & x_113 & x_114 & x_125 & x_108 & x_101 & x_122]] & x_123 & x_121] | [[x_383 = 2] & [[x_107 & x_116 & x_119 & x_99 & x_81 & [[~ x_82]] & [x_104 < x_84] & [x_84 <= x_103] & x_110] | [x_111 & x_116 & x_119 & x_96 & x_124 & x_110 & x_123] | [x_100 & x_117 & [[~ x_118]] & x_119 & [[~ x_81]] & x_82 & [x_8 = 2] & [x_105 <= x_84]] | [x_97 & x_128 & x_119 & [x_7 = 2] & x_81 & x_82 & x_124 & x_110] | [x_106 & x_128 & x_119 & [x_7 <> 2] & x_109 & x_124 & x_110] | [x_102 & x_117 & x_118 & x_119 & x_109 & x_101 & x_124]] & x_127 & x_129]] & [x_68 = x_104]] .
prop a_71 := [[x_384 = 0] & [x_140 < x_167] & [x_104 = x_167] & x_163 & x_159 & x_165 & x_157 & x_146] | [[x_384 = 1] & [[[x_385 = 1] & [[x_143 & x_148 & x_161 & x_135 & x_113 & [[~ x_114]] & [x_140 < x_126] & [x_126 <= x_139] & x_146] | [x_147 & x_148 & x_161 & x_132 & x_158 & x_146 & x_163] | [x_136 & x_149 & [[~ x_150]] & x_161 & [[~ x_113]] & x_114 & [x_7 = 1] & [x_141 <= x_126]] | [x_133 & x_151 & x_161 & [x_6 = 1] & x_113 & x_114 & x_158 & x_146] | [x_142 & x_151 & x_161 & [x_6 <> 1] & x_144 & x_158 & x_146] | [x_138 & x_149 & x_150 & x_161 & x_144 & x_137 & x_158]] & x_159 & x_157] | [[x_385 = 2] & [[x_143 & x_152 & x_155 & x_135 & x_117 & [[~ x_118]] & [x_140 < x_120] & [x_120 <= x_139] & x_146] | [x_147 & x_152 & x_155 & x_132 & x_160 & x_146 & x_159] | [x_136 & x_153 & [[~ x_154]] & x_155 & [[~ x_117]] & x_118 & [x_7 = 2] & [x_141 <= x_120]] | [x_133 & x_164 & x_155 & [x_6 = 2] & x_117 & x_118 & x_160 & x_146] | [x_142 & x_164 & x_155 & [x_6 <> 2] & x_145 & x_160 & x_146] | [x_138 & x_153 & x_154 & x_155 & x_145 & x_137 & x_160]] & x_163 & x_165]] & [x_104 = x_140]] .
prop a_72 := [[x_386 = 0] & [x_176 < x_203] & [x_140 = x_203] & x_199 & x_195 & x_201 & x_193 & x_182] | [[x_386 = 1] & [[[x_387 = 1] & [[x_179 & x_184 & x_197 & x_171 & x_149 & [[~ x_150]] & [x_176 < x_162] & [x_162 <= x_175] & x_182] | [x_183 & x_184 & x_197 & x_168 & x_194 & x_182 & x_199] | [x_172 & x_185 & [[~ x_186]] & x_197 & [[~ x_149]] & x_150 & [x_6 = 1] & [x_177 <= x_162]] | [x_169 & x_187 & x_197 & [x_5 = 1] & x_149 & x_150 & x_194 & x_182] | [x_178 & x_187 & x_197 & [x_5 <> 1] & x_180 & x_194 & x_182] | [x_174 & x_185 & x_186 & x_197 & x_180 & x_173 & x_194]] & x_195 & x_193] | [[x_387 = 2] & [[x_179 & x_188 & x_191 & x_171 & x_153 & [[~ x_154]] & [x_176 < x_156] & [x_156 <= x_175] & x_182] | [x_183 & x_188 & x_191 & x_168 & x_196 & x_182 & x_195] | [x_172 & x_189 & [[~ x_190]] & x_191 & [[~ x_153]] & x_154 & [x_6 = 2] & [x_177 <= x_156]] | [x_169 & x_200 & x_191 & [x_5 = 2] & x_153 & x_154 & x_196 & x_182] | [x_178 & x_200 & x_191 & [x_5 <> 2] & x_181 & x_196 & x_182] | [x_174 & x_189 & x_190 & x_191 & x_181 & x_173 & x_196]] & x_199 & x_201]] & [x_140 = x_176]] .
prop a_73 := [[x_388 = 0] & [x_212 < x_239] & [x_176 = x_239] & x_235 & x_231 & x_237 & x_229 & x_218] | [[x_388 = 1] & [[[x_389 = 1] & [[x_215 & x_220 & x_233 & x_207 & x_185 & [[~ x_186]] & [x_212 < x_198] & [x_198 <= x_211] & x_218] | [x_219 & x_220 & x_233 & x_204 & x_230 & x_218 & x_235] | [x_208 & x_221 & [[~ x_222]] & x_233 & [[~ x_185]] & x_186 & [x_5 = 1] & [x_213 <= x_198]] | [x_205 & x_223 & x_233 & [x_4 = 1] & x_185 & x_186 & x_230 & x_218] | [x_214 & x_223 & x_233 & [x_4 <> 1] & x_216 & x_230 & x_218] | [x_210 & x_221 & x_222 & x_233 & x_216 & x_209 & x_230]] & x_231 & x_229] | [[x_389 = 2] & [[x_215 & x_224 & x_227 & x_207 & x_189 & [[~ x_190]] & [x_212 < x_192] & [x_192 <= x_211] & x_218] | [x_219 & x_224 & x_227 & x_204 & x_232 & x_218 & x_231] | [x_208 & x_225 & [[~ x_226]] & x_227 & [[~ x_189]] & x_190 & [x_5 = 2] & [x_213 <= x_192]] | [x_205 & x_236 & x_227 & [x_4 = 2] & x_189 & x_190 & x_232 & x_218] | [x_214 & x_236 & x_227 & [x_4 <> 2] & x_217 & x_232 & x_218] | [x_210 & x_225 & x_226 & x_227 & x_217 & x_209 & x_232]] & x_235 & x_237]] & [x_176 = x_212]] .
prop a_74 := [[x_390 = 0] & [x_248 < x_275] & [x_212 = x_275] & x_271 & x_267 & x_273 & x_265 & x_254] | [[x_390 = 1] & [[[x_391 = 1] & [[x_251 & x_256 & x_269 & x_243 & x_221 & [[~ x_222]] & [x_248 < x_234] & [x_234 <= x_247] & x_254] | [x_255 & x_256 & x_269 & x_240 & x_266 & x_254 & x_271] | [x_244 & x_257 & [[~ x_258]] & x_269 & [[~ x_221]] & x_222 & [x_4 = 1] & [x_249 <= x_234]] | [x_241 & x_259 & x_269 & [x_3 = 1] & x_221 & x_222 & x_266 & x_254] | [x_250 & x_259 & x_269 & [x_3 <> 1] & x_252 & x_266 & x_254] | [x_246 & x_257 & x_258 & x_269 & x_252 & x_245 & x_266]] & x_267 & x_265] | [[x_391 = 2] & [[x_251 & x_260 & x_263 & x_243 & x_225 & [[~ x_226]] & [x_248 < x_228] & [x_228 <= x_247] & x_254] | [x_255 & x_260 & x_263 & x_240 & x_268 & x_254 & x_267] | [x_244 & x_261 & [[~ x_262]] & x_263 & [[~ x_225]] & x_226 & [x_4 = 2] & [x_249 <= x_228]] | [x_241 & x_272 & x_263 & [x_3 = 2] & x_225 & x_226 & x_268 & x_254] | [x_250 & x_272 & x_263 & [x_3 <> 2] & x_253 & x_268 & x_254] | [x_246 & x_261 & x_262 & x_263 & x_253 & x_245 & x_268]] & x_271 & x_273]] & [x_212 = x_248]] .
prop a_75 := [[x_392 = 0] & [x_284 < x_311] & [x_248 = x_311] & x_307 & x_303 & x_309 & x_301 & x_290] | [[x_392 = 1] & [[[x_393 = 1] & [[x_287 & x_292 & x_305 & x_279 & x_257 & [[~ x_258]] & [x_284 < x_270] & [x_270 <= x_283] & x_290] | [x_291 & x_292 & x_305 & x_276 & x_302 & x_290 & x_307] | [x_280 & x_293 & [[~ x_294]] & x_305 & [[~ x_257]] & x_258 & [x_3 = 1] & [x_285 <= x_270]] | [x_277 & x_295 & x_305 & [x_2 = 1] & x_257 & x_258 & x_302 & x_290] | [x_286 & x_295 & x_305 & [x_2 <> 1] & x_288 & x_302 & x_290] | [x_282 & x_293 & x_294 & x_305 & x_288 & x_281 & x_302]] & x_303 & x_301] | [[x_393 = 2] & [[x_287 & x_296 & x_299 & x_279 & x_261 & [[~ x_262]] & [x_284 < x_264] & [x_264 <= x_283] & x_290] | [x_291 & x_296 & x_299 & x_276 & x_304 & x_290 & x_303] | [x_280 & x_297 & [[~ x_298]] & x_299 & [[~ x_261]] & x_262 & [x_3 = 2] & [x_285 <= x_264]] | [x_277 & x_308 & x_299 & [x_2 = 2] & x_261 & x_262 & x_304 & x_290] | [x_286 & x_308 & x_299 & [x_2 <> 2] & x_289 & x_304 & x_290] | [x_282 & x_297 & x_298 & x_299 & x_289 & x_281 & x_304]] & x_307 & x_309]] & [x_248 = x_284]] .
prop a_76 := [[x_394 = 0] & [x_320 < x_347] & [x_284 = x_347] & x_343 & x_339 & x_345 & x_337 & x_326] | [[x_394 = 1] & [[[x_395 = 1] & [[x_323 & x_328 & x_341 & x_315 & x_293 & [[~ x_294]] & [x_320 < x_306] & [x_306 <= x_319] & x_326] | [x_327 & x_328 & x_341 & x_312 & x_338 & x_326 & x_343] | [x_316 & x_329 & [[~ x_330]] & x_341 & [[~ x_293]] & x_294 & [x_2 = 1] & [x_321 <= x_306]] | [x_313 & x_331 & x_341 & [x_1 = 1] & x_293 & x_294 & x_338 & x_326] | [x_322 & x_331 & x_341 & [x_1 <> 1] & x_324 & x_338 & x_326] | [x_318 & x_329 & x_330 & x_341 & x_324 & x_317 & x_338]] & x_339 & x_337] | [[x_395 = 2] & [[x_323 & x_332 & x_335 & x_315 & x_297 & [[~ x_298]] & [x_320 < x_300] & [x_300 <= x_319] & x_326] | [x_327 & x_332 & x_335 & x_312 & x_340 & x_326 & x_339] | [x_316 & x_333 & [[~ x_334]] & x_335 & [[~ x_297]] & x_298 & [x_2 = 2] & [x_321 <= x_300]] | [x_313 & x_344 & x_335 & [x_1 = 2] & x_297 & x_298 & x_340 & x_326] | [x_322 & x_344 & x_335 & [x_1 <> 2] & x_325 & x_340 & x_326] | [x_318 & x_333 & x_334 & x_335 & x_325 & x_317 & x_340]] & x_343 & x_345]] & [x_284 = x_320]] .
prop a_77 := [[x_396 = 0] & [x_11 < x_376] & [x_320 = x_376] & x_372 & x_369 & x_374 & x_367 & x_361] | [[x_396 = 1] & [[[x_397 = 1] & [[x_358 & x_363 & x_371 & x_351 & x_329 & [[~ x_330]] & [x_11 < x_342] & [x_342 <= x_355] & x_361] | [x_362 & x_363 & x_371 & x_348 & x_368 & x_361 & x_372] | [x_352 & x_12 & [[~ x_13]] & x_371 & [[~ x_329]] & x_330 & [x_1 = 1] & [x_356 <= x_342]] | [x_349 & x_364 & x_371 & [x_0 = 1] & x_329 & x_330 & x_368 & x_361] | [x_357 & x_364 & x_371 & [x_0 <> 1] & x_359 & x_368 & x_361] | [x_354 & x_12 & x_13 & x_371 & x_359 & x_353 & x_368]] & x_369 & x_367] | [[x_397 = 2] & [[x_358 & x_365 & x_366 & x_351 & x_333 & [[~ x_334]] & [x_11 < x_336] & [x_336 <= x_355] & x_361] | [x_362 & x_365 & x_366 & x_348 & x_370 & x_361 & x_369] | [x_352 & x_14 & [[~ x_15]] & x_366 & [[~ x_333]] & x_334 & [x_1 = 2] & [x_356 <= x_336]] | [x_349 & x_373 & x_366 & [x_0 = 2] & x_333 & x_334 & x_370 & x_361] | [x_357 & x_373 & x_366 & [x_0 <> 2] & x_360 & x_370 & x_361] | [x_354 & x_14 & x_15 & x_366 & x_360 & x_353 & x_370]] & x_372 & x_374]] & [x_320 = x_11]] .
prop a_78 := [x_31 & x_32 & x_34 & x_35] | [x_34 & x_35 & x_31 & x_32] | [x_39 & x_40 & x_43 & x_44] | [x_43 & x_44 & x_39 & x_40] | [x_77 & x_78 & x_81 & x_82] | [x_81 & x_82 & x_77 & x_78] | [x_113 & x_114 & x_117 & x_118] | [x_117 & x_118 & x_113 & x_114] | [x_149 & x_150 & x_153 & x_154] | [x_153 & x_154 & x_149 & x_150] | [x_185 & x_186 & x_189 & x_190] | [x_189 & x_190 & x_185 & x_186] | [x_221 & x_222 & x_225 & x_226] | [x_225 & x_226 & x_221 & x_222] | [x_257 & x_258 & x_261 & x_262] | [x_261 & x_262 & x_257 & x_258] | [x_293 & x_294 & x_297 & x_298] | [x_297 & x_298 & x_293 & x_294] | [x_329 & x_330 & x_333 & x_334] | [x_333 & x_334 & x_329 & x_330] | [x_12 & x_13 & x_14 & x_15] | [x_14 & x_15 & x_12 & x_13] .
prop bb := 
tt
.
sat 
bb & a_0 & a_1 & a_2 & a_3 & a_4 & a_5 & a_6 & a_7 & a_8 & a_9 & a_10 & a_11 & a_12 & a_13 & a_14 & a_15 & a_16 & a_17 & a_18 & a_19 & a_20 & a_21 & a_22 & a_23 & a_24 & a_25 & a_26 & a_27 & a_28 & a_29 & a_30 & a_31 & a_32 & a_33 & a_34 & a_35 & a_36 & a_37 & a_38 & a_39 & a_40 & a_41 & a_42 & a_43 & a_44 & a_45 & a_46 & a_47 & a_48 & a_49 & a_50 & a_51 & a_52 & a_53 & a_54 & a_55 & a_56 & a_57 & a_58 & a_59 & a_60 & a_61 & a_62 & a_63 & a_64 & a_65 & a_66 & a_67 & a_68 & a_69 & a_70 & a_71 & a_72 & a_73 & a_74 & a_75 & a_76 & a_77 & a_78.