(benchmark pursuit_safety_18.smt :source { SAL benchmark suite. Created at SRI by Bruno Dutertre, John Rushby, Maria Sorea, and Leonardo de Moura. Contact demoura@csl.sri.com for more information. This benchmark was automatically translated into SMT-LIB format from CVC format using CVC Lite } :status unknown :logic QF_LRA :extrasorts (ANY) :extrapreds ((x_0)) :extrapreds ((x_1)) :extrafuns ((x_2 Real)) :extrafuns ((x_3 Real)) :extrapreds ((x_4)) :extrapreds ((x_5)) :extrafuns ((x_6 Real)) :extrafuns ((x_7 Real)) :extrapreds ((x_8)) :extrafuns ((x_9 Real)) :extrafuns ((x_10 Real)) :extrafuns ((x_11 Real)) :extrafuns ((x_12 Real)) :extrafuns ((x_13 Real)) :extrapreds ((x_14)) :extrapreds ((x_15)) :extrafuns ((x_16 Real)) :extrafuns ((x_17 Real)) :extrafuns ((x_18 Real)) :extrafuns ((x_19 Real)) :extrafuns ((x_20 Real)) :extrafuns ((x_21 Real)) :extrafuns ((x_22 Real)) :extrapreds ((x_23)) :extrapreds ((x_24)) :extrafuns ((x_25 Real)) :extrafuns ((x_26 Real)) :extrafuns ((x_27 Real)) :extrafuns ((x_28 Real)) :extrafuns ((x_29 Real)) :extrafuns ((x_30 Real)) :extrafuns ((x_31 Real)) :extrapreds ((x_32)) :extrapreds ((x_33)) :extrafuns ((x_34 Real)) :extrafuns ((x_35 Real)) :extrafuns ((x_36 Real)) :extrafuns ((x_37 Real)) :extrafuns ((x_38 Real)) :extrafuns ((x_39 Real)) :extrafuns ((x_40 Real)) :extrapreds ((x_41)) :extrapreds ((x_42)) :extrafuns ((x_43 Real)) :extrafuns ((x_44 Real)) :extrafuns ((x_45 Real)) :extrafuns ((x_46 Real)) :extrafuns ((x_47 Real)) :extrafuns ((x_48 Real)) :extrafuns ((x_49 Real)) :extrapreds ((x_50)) :extrapreds ((x_51)) :extrafuns ((x_52 Real)) :extrafuns ((x_53 Real)) :extrafuns ((x_54 Real)) :extrafuns ((x_55 Real)) :extrafuns ((x_56 Real)) :extrafuns ((x_57 Real)) :extrafuns ((x_58 Real)) :extrapreds ((x_59)) :extrapreds ((x_60)) :extrafuns ((x_61 Real)) :extrafuns ((x_62 Real)) :extrafuns ((x_63 Real)) :extrafuns ((x_64 Real)) :extrafuns ((x_65 Real)) :extrafuns ((x_66 Real)) :extrafuns ((x_67 Real)) :extrapreds ((x_68)) :extrapreds ((x_69)) :extrafuns ((x_70 Real)) :extrafuns ((x_71 Real)) :extrafuns ((x_72 Real)) :extrafuns ((x_73 Real)) :extrafuns ((x_74 Real)) :extrafuns ((x_75 Real)) :extrafuns ((x_76 Real)) :extrapreds ((x_77)) :extrapreds ((x_78)) :extrafuns ((x_79 Real)) :extrafuns ((x_80 Real)) :extrafuns ((x_81 Real)) :extrafuns ((x_82 Real)) :extrafuns ((x_83 Real)) :extrafuns ((x_84 Real)) :extrafuns ((x_85 Real)) :extrapreds ((x_86)) :extrapreds ((x_87)) :extrafuns ((x_88 Real)) :extrafuns ((x_89 Real)) :extrafuns ((x_90 Real)) :extrafuns ((x_91 Real)) :extrafuns ((x_92 Real)) :extrafuns ((x_93 Real)) :extrafuns ((x_94 Real)) :extrapreds ((x_95)) :extrapreds ((x_96)) :extrafuns ((x_97 Real)) :extrafuns ((x_98 Real)) :extrafuns ((x_99 Real)) :extrafuns ((x_100 Real)) :extrafuns ((x_101 Real)) :extrafuns ((x_102 Real)) :extrafuns ((x_103 Real)) :extrapreds ((x_104)) :extrapreds ((x_105)) :extrafuns ((x_106 Real)) :extrafuns ((x_107 Real)) :extrafuns ((x_108 Real)) :extrafuns ((x_109 Real)) :extrafuns ((x_110 Real)) :extrafuns ((x_111 Real)) :extrafuns ((x_112 Real)) :extrapreds ((x_113)) :extrapreds ((x_114)) :extrafuns ((x_115 Real)) :extrafuns ((x_116 Real)) :extrafuns ((x_117 Real)) :extrafuns ((x_118 Real)) :extrafuns ((x_119 Real)) :extrafuns ((x_120 Real)) :extrafuns ((x_121 Real)) :extrapreds ((x_122)) :extrapreds ((x_123)) :extrafuns ((x_124 Real)) :extrafuns ((x_125 Real)) :extrafuns ((x_126 Real)) :extrafuns ((x_127 Real)) :extrafuns ((x_128 Real)) :extrafuns ((x_129 Real)) :extrafuns ((x_130 Real)) :extrapreds ((x_131)) :extrapreds ((x_132)) :extrafuns ((x_133 Real)) :extrafuns ((x_134 Real)) :extrafuns ((x_135 Real)) :extrafuns ((x_136 Real)) :extrafuns ((x_137 Real)) :extrafuns ((x_138 Real)) :extrafuns ((x_139 Real)) :extrapreds ((x_140)) :extrapreds ((x_141)) :extrafuns ((x_142 Real)) :extrafuns ((x_143 Real)) :extrafuns ((x_144 Real)) :extrafuns ((x_145 Real)) :extrafuns ((x_146 Real)) :extrafuns ((x_147 Real)) :extrafuns ((x_148 Real)) :extrapreds ((x_149)) :extrapreds ((x_150)) :extrafuns ((x_151 Real)) :extrafuns ((x_152 Real)) :extrafuns ((x_153 Real)) :extrafuns ((x_154 Real)) :extrafuns ((x_155 Real)) :extrafuns ((x_156 Real)) :extrafuns ((x_157 Real)) :extrapreds ((x_158)) :extrapreds ((x_159)) :extrafuns ((x_160 Real)) :extrafuns ((x_161 Real)) :extrafuns ((x_162 Real)) :extrafuns ((x_163 Real)) :extrafuns ((x_164 Real)) :extrafuns ((x_165 Real)) :formula (flet ($cvcl_3 (= x_151 40)) (flet ($cvcl_4 (= x_151 0)) (flet ($cvcl_2 (= x_148 40)) (flet ($cvcl_6 (= x_148 0)) (flet ($cvcl_13 (< (+ (- (* x_151 5) (* x_148 6)) 40) 0)) (flet ($cvcl_10 (= x_152 2)) (flet ($cvcl_7 (= x_157 x_148)) (flet ($cvcl_24 (not x_149)) (flet ($cvcl_28 (and $cvcl_24 x_150)) (flet ($cvcl_15 (not x_150)) (flet ($cvcl_18 (and x_149 $cvcl_15)) (flet ($cvcl_5 (and (iff x_158 x_149) (iff x_159 x_150))) (flet ($cvcl_8 (= x_160 x_151)) (flet ($cvcl_1 (and $cvcl_24 $cvcl_15)) (flet ($cvcl_14 (= x_161 0)) (flet ($cvcl_21 (not x_158)) (flet ($cvcl_17 (and $cvcl_21 x_159)) (flet ($cvcl_0 (= x_154 0)) (flet ($cvcl_12 (not $cvcl_2)) (flet ($cvcl_9 (= x_161 x_152)) (flet ($cvcl_27 (or $cvcl_24 x_150 )) (flet ($cvcl_11 (not $cvcl_6)) (flet ($cvcl_26 (or x_149 x_150 )) (flet ($cvcl_33 (= x_142 40)) (flet ($cvcl_34 (= x_142 0)) (flet ($cvcl_32 (= x_139 40)) (flet ($cvcl_36 (= x_139 0)) (flet ($cvcl_43 (< (+ (- (* x_142 5) (* x_139 6)) 40) 0)) (flet ($cvcl_40 (= x_143 2)) (flet ($cvcl_37 (= x_148 x_139)) (flet ($cvcl_51 (not x_140)) (flet ($cvcl_55 (and $cvcl_51 x_141)) (flet ($cvcl_45 (not x_141)) (flet ($cvcl_47 (and x_140 $cvcl_45)) (flet ($cvcl_35 (and (iff x_149 x_140) (iff x_150 x_141))) (flet ($cvcl_38 (= x_151 x_142)) (flet ($cvcl_31 (and $cvcl_51 $cvcl_45)) (flet ($cvcl_44 (= x_152 0)) (flet ($cvcl_30 (= x_145 0)) (flet ($cvcl_42 (not $cvcl_32)) (flet ($cvcl_39 (= x_152 x_143)) (flet ($cvcl_54 (or $cvcl_51 x_141 )) (flet ($cvcl_41 (not $cvcl_36)) (flet ($cvcl_53 (or x_140 x_141 )) (flet ($cvcl_60 (= x_133 40)) (flet ($cvcl_61 (= x_133 0)) (flet ($cvcl_59 (= x_130 40)) (flet ($cvcl_63 (= x_130 0)) (flet ($cvcl_70 (< (+ (- (* x_133 5) (* x_130 6)) 40) 0)) (flet ($cvcl_67 (= x_134 2)) (flet ($cvcl_64 (= x_139 x_130)) (flet ($cvcl_78 (not x_131)) (flet ($cvcl_82 (and $cvcl_78 x_132)) (flet ($cvcl_72 (not x_132)) (flet ($cvcl_74 (and x_131 $cvcl_72)) (flet ($cvcl_62 (and (iff x_140 x_131) (iff x_141 x_132))) (flet ($cvcl_65 (= x_142 x_133)) (flet ($cvcl_58 (and $cvcl_78 $cvcl_72)) (flet ($cvcl_71 (= x_143 0)) (flet ($cvcl_57 (= x_136 0)) (flet ($cvcl_69 (not $cvcl_59)) (flet ($cvcl_66 (= x_143 x_134)) (flet ($cvcl_81 (or $cvcl_78 x_132 )) (flet ($cvcl_68 (not $cvcl_63)) (flet ($cvcl_80 (or x_131 x_132 )) (flet ($cvcl_87 (= x_124 40)) (flet ($cvcl_88 (= x_124 0)) (flet ($cvcl_86 (= x_121 40)) (flet ($cvcl_90 (= x_121 0)) (flet ($cvcl_97 (< (+ (- (* x_124 5) (* x_121 6)) 40) 0)) (flet ($cvcl_94 (= x_125 2)) (flet ($cvcl_91 (= x_130 x_121)) (flet ($cvcl_105 (not x_122)) (flet ($cvcl_109 (and $cvcl_105 x_123)) (flet ($cvcl_99 (not x_123)) (flet ($cvcl_101 (and x_122 $cvcl_99)) (flet ($cvcl_89 (and (iff x_131 x_122) (iff x_132 x_123))) (flet ($cvcl_92 (= x_133 x_124)) (flet ($cvcl_85 (and $cvcl_105 $cvcl_99)) (flet ($cvcl_98 (= x_134 0)) (flet ($cvcl_84 (= x_127 0)) (flet ($cvcl_96 (not $cvcl_86)) (flet ($cvcl_93 (= x_134 x_125)) (flet ($cvcl_108 (or $cvcl_105 x_123 )) (flet ($cvcl_95 (not $cvcl_90)) (flet ($cvcl_107 (or x_122 x_123 )) (flet ($cvcl_114 (= x_115 40)) (flet ($cvcl_115 (= x_115 0)) (flet ($cvcl_113 (= x_112 40)) (flet ($cvcl_117 (= x_112 0)) (flet ($cvcl_124 (< (+ (- (* x_115 5) (* x_112 6)) 40) 0)) (flet ($cvcl_121 (= x_116 2)) (flet ($cvcl_118 (= x_121 x_112)) (flet ($cvcl_132 (not x_113)) (flet ($cvcl_136 (and $cvcl_132 x_114)) (flet ($cvcl_126 (not x_114)) (flet ($cvcl_128 (and x_113 $cvcl_126)) (flet ($cvcl_116 (and (iff x_122 x_113) (iff x_123 x_114))) (flet ($cvcl_119 (= x_124 x_115)) (flet ($cvcl_112 (and $cvcl_132 $cvcl_126)) (flet ($cvcl_125 (= x_125 0)) (flet ($cvcl_111 (= x_118 0)) (flet ($cvcl_123 (not $cvcl_113)) (flet ($cvcl_120 (= x_125 x_116)) (flet ($cvcl_135 (or $cvcl_132 x_114 )) (flet ($cvcl_122 (not $cvcl_117)) (flet ($cvcl_134 (or x_113 x_114 )) (flet ($cvcl_141 (= x_106 40)) (flet ($cvcl_142 (= x_106 0)) (flet ($cvcl_140 (= x_103 40)) (flet ($cvcl_144 (= x_103 0)) (flet ($cvcl_151 (< (+ (- (* x_106 5) (* x_103 6)) 40) 0)) (flet ($cvcl_148 (= x_107 2)) (flet ($cvcl_145 (= x_112 x_103)) (flet ($cvcl_159 (not x_104)) (flet ($cvcl_163 (and $cvcl_159 x_105)) (flet ($cvcl_153 (not x_105)) (flet ($cvcl_155 (and x_104 $cvcl_153)) (flet ($cvcl_143 (and (iff x_113 x_104) (iff x_114 x_105))) (flet ($cvcl_146 (= x_115 x_106)) (flet ($cvcl_139 (and $cvcl_159 $cvcl_153)) (flet ($cvcl_152 (= x_116 0)) (flet ($cvcl_138 (= x_109 0)) (flet ($cvcl_150 (not $cvcl_140)) (flet ($cvcl_147 (= x_116 x_107)) (flet ($cvcl_162 (or $cvcl_159 x_105 )) (flet ($cvcl_149 (not $cvcl_144)) (flet ($cvcl_161 (or x_104 x_105 )) (flet ($cvcl_168 (= x_97 40)) (flet ($cvcl_169 (= x_97 0)) (flet ($cvcl_167 (= x_94 40)) (flet ($cvcl_171 (= x_94 0)) (flet ($cvcl_178 (< (+ (- (* x_97 5) (* x_94 6)) 40) 0)) (flet ($cvcl_175 (= x_98 2)) (flet ($cvcl_172 (= x_103 x_94)) (flet ($cvcl_186 (not x_95)) (flet ($cvcl_190 (and $cvcl_186 x_96)) (flet ($cvcl_180 (not x_96)) (flet ($cvcl_182 (and x_95 $cvcl_180)) (flet ($cvcl_170 (and (iff x_104 x_95) (iff x_105 x_96))) (flet ($cvcl_173 (= x_106 x_97)) (flet ($cvcl_166 (and $cvcl_186 $cvcl_180)) (flet ($cvcl_179 (= x_107 0)) (flet ($cvcl_165 (= x_100 0)) (flet ($cvcl_177 (not $cvcl_167)) (flet ($cvcl_174 (= x_107 x_98)) (flet ($cvcl_189 (or $cvcl_186 x_96 )) (flet ($cvcl_176 (not $cvcl_171)) (flet ($cvcl_188 (or x_95 x_96 )) (flet ($cvcl_195 (= x_88 40)) (flet ($cvcl_196 (= x_88 0)) (flet ($cvcl_194 (= x_85 40)) (flet ($cvcl_198 (= x_85 0)) (flet ($cvcl_205 (< (+ (- (* x_88 5) (* x_85 6)) 40) 0)) (flet ($cvcl_202 (= x_89 2)) (flet ($cvcl_199 (= x_94 x_85)) (flet ($cvcl_213 (not x_86)) (flet ($cvcl_217 (and $cvcl_213 x_87)) (flet ($cvcl_207 (not x_87)) (flet ($cvcl_209 (and x_86 $cvcl_207)) (flet ($cvcl_197 (and (iff x_95 x_86) (iff x_96 x_87))) (flet ($cvcl_200 (= x_97 x_88)) (flet ($cvcl_193 (and $cvcl_213 $cvcl_207)) (flet ($cvcl_206 (= x_98 0)) (flet ($cvcl_192 (= x_91 0)) (flet ($cvcl_204 (not $cvcl_194)) (flet ($cvcl_201 (= x_98 x_89)) (flet ($cvcl_216 (or $cvcl_213 x_87 )) (flet ($cvcl_203 (not $cvcl_198)) (flet ($cvcl_215 (or x_86 x_87 )) (flet ($cvcl_222 (= x_79 40)) (flet ($cvcl_223 (= x_79 0)) (flet ($cvcl_221 (= x_76 40)) (flet ($cvcl_225 (= x_76 0)) (flet ($cvcl_232 (< (+ (- (* x_79 5) (* x_76 6)) 40) 0)) (flet ($cvcl_229 (= x_80 2)) (flet ($cvcl_226 (= x_85 x_76)) (flet ($cvcl_240 (not x_77)) (flet ($cvcl_244 (and $cvcl_240 x_78)) (flet ($cvcl_234 (not x_78)) (flet ($cvcl_236 (and x_77 $cvcl_234)) (flet ($cvcl_224 (and (iff x_86 x_77) (iff x_87 x_78))) (flet ($cvcl_227 (= x_88 x_79)) (flet ($cvcl_220 (and $cvcl_240 $cvcl_234)) (flet ($cvcl_233 (= x_89 0)) (flet ($cvcl_219 (= x_82 0)) (flet ($cvcl_231 (not $cvcl_221)) (flet ($cvcl_228 (= x_89 x_80)) (flet ($cvcl_243 (or $cvcl_240 x_78 )) (flet ($cvcl_230 (not $cvcl_225)) (flet ($cvcl_242 (or x_77 x_78 )) (flet ($cvcl_249 (= x_70 40)) (flet ($cvcl_250 (= x_70 0)) (flet ($cvcl_248 (= x_67 40)) (flet ($cvcl_252 (= x_67 0)) (flet ($cvcl_259 (< (+ (- (* x_70 5) (* x_67 6)) 40) 0)) (flet ($cvcl_256 (= x_71 2)) (flet ($cvcl_253 (= x_76 x_67)) (flet ($cvcl_267 (not x_68)) (flet ($cvcl_271 (and $cvcl_267 x_69)) (flet ($cvcl_261 (not x_69)) (flet ($cvcl_263 (and x_68 $cvcl_261)) (flet ($cvcl_251 (and (iff x_77 x_68) (iff x_78 x_69))) (flet ($cvcl_254 (= x_79 x_70)) (flet ($cvcl_247 (and $cvcl_267 $cvcl_261)) (flet ($cvcl_260 (= x_80 0)) (flet ($cvcl_246 (= x_73 0)) (flet ($cvcl_258 (not $cvcl_248)) (flet ($cvcl_255 (= x_80 x_71)) (flet ($cvcl_270 (or $cvcl_267 x_69 )) (flet ($cvcl_257 (not $cvcl_252)) (flet ($cvcl_269 (or x_68 x_69 )) (flet ($cvcl_276 (= x_61 40)) (flet ($cvcl_277 (= x_61 0)) (flet ($cvcl_275 (= x_58 40)) (flet ($cvcl_279 (= x_58 0)) (flet ($cvcl_286 (< (+ (- (* x_61 5) (* x_58 6)) 40) 0)) (flet ($cvcl_283 (= x_62 2)) (flet ($cvcl_280 (= x_67 x_58)) (flet ($cvcl_294 (not x_59)) (flet ($cvcl_298 (and $cvcl_294 x_60)) (flet ($cvcl_288 (not x_60)) (flet ($cvcl_290 (and x_59 $cvcl_288)) (flet ($cvcl_278 (and (iff x_68 x_59) (iff x_69 x_60))) (flet ($cvcl_281 (= x_70 x_61)) (flet ($cvcl_274 (and $cvcl_294 $cvcl_288)) (flet ($cvcl_287 (= x_71 0)) (flet ($cvcl_273 (= x_64 0)) (flet ($cvcl_285 (not $cvcl_275)) (flet ($cvcl_282 (= x_71 x_62)) (flet ($cvcl_297 (or $cvcl_294 x_60 )) (flet ($cvcl_284 (not $cvcl_279)) (flet ($cvcl_296 (or x_59 x_60 )) (flet ($cvcl_303 (= x_52 40)) (flet ($cvcl_304 (= x_52 0)) (flet ($cvcl_302 (= x_49 40)) (flet ($cvcl_306 (= x_49 0)) (flet ($cvcl_313 (< (+ (- (* x_52 5) (* x_49 6)) 40) 0)) (flet ($cvcl_310 (= x_53 2)) (flet ($cvcl_307 (= x_58 x_49)) (flet ($cvcl_321 (not x_50)) (flet ($cvcl_325 (and $cvcl_321 x_51)) (flet ($cvcl_315 (not x_51)) (flet ($cvcl_317 (and x_50 $cvcl_315)) (flet ($cvcl_305 (and (iff x_59 x_50) (iff x_60 x_51))) (flet ($cvcl_308 (= x_61 x_52)) (flet ($cvcl_301 (and $cvcl_321 $cvcl_315)) (flet ($cvcl_314 (= x_62 0)) (flet ($cvcl_300 (= x_55 0)) (flet ($cvcl_312 (not $cvcl_302)) (flet ($cvcl_309 (= x_62 x_53)) (flet ($cvcl_324 (or $cvcl_321 x_51 )) (flet ($cvcl_311 (not $cvcl_306)) (flet ($cvcl_323 (or x_50 x_51 )) (flet ($cvcl_330 (= x_43 40)) (flet ($cvcl_331 (= x_43 0)) (flet ($cvcl_329 (= x_40 40)) (flet ($cvcl_333 (= x_40 0)) (flet ($cvcl_340 (< (+ (- (* x_43 5) (* x_40 6)) 40) 0)) (flet ($cvcl_337 (= x_44 2)) (flet ($cvcl_334 (= x_49 x_40)) (flet ($cvcl_348 (not x_41)) (flet ($cvcl_352 (and $cvcl_348 x_42)) (flet ($cvcl_342 (not x_42)) (flet ($cvcl_344 (and x_41 $cvcl_342)) (flet ($cvcl_332 (and (iff x_50 x_41) (iff x_51 x_42))) (flet ($cvcl_335 (= x_52 x_43)) (flet ($cvcl_328 (and $cvcl_348 $cvcl_342)) (flet ($cvcl_341 (= x_53 0)) (flet ($cvcl_327 (= x_46 0)) (flet ($cvcl_339 (not $cvcl_329)) (flet ($cvcl_336 (= x_53 x_44)) (flet ($cvcl_351 (or $cvcl_348 x_42 )) (flet ($cvcl_338 (not $cvcl_333)) (flet ($cvcl_350 (or x_41 x_42 )) (flet ($cvcl_357 (= x_34 40)) (flet ($cvcl_358 (= x_34 0)) (flet ($cvcl_356 (= x_31 40)) (flet ($cvcl_360 (= x_31 0)) (flet ($cvcl_367 (< (+ (- (* x_34 5) (* x_31 6)) 40) 0)) (flet ($cvcl_364 (= x_35 2)) (flet ($cvcl_361 (= x_40 x_31)) (flet ($cvcl_375 (not x_32)) (flet ($cvcl_379 (and $cvcl_375 x_33)) (flet ($cvcl_369 (not x_33)) (flet ($cvcl_371 (and x_32 $cvcl_369)) (flet ($cvcl_359 (and (iff x_41 x_32) (iff x_42 x_33))) (flet ($cvcl_362 (= x_43 x_34)) (flet ($cvcl_355 (and $cvcl_375 $cvcl_369)) (flet ($cvcl_368 (= x_44 0)) (flet ($cvcl_354 (= x_37 0)) (flet ($cvcl_366 (not $cvcl_356)) (flet ($cvcl_363 (= x_44 x_35)) (flet ($cvcl_378 (or $cvcl_375 x_33 )) (flet ($cvcl_365 (not $cvcl_360)) (flet ($cvcl_377 (or x_32 x_33 )) (flet ($cvcl_384 (= x_25 40)) (flet ($cvcl_385 (= x_25 0)) (flet ($cvcl_383 (= x_22 40)) (flet ($cvcl_387 (= x_22 0)) (flet ($cvcl_394 (< (+ (- (* x_25 5) (* x_22 6)) 40) 0)) (flet ($cvcl_391 (= x_26 2)) (flet ($cvcl_388 (= x_31 x_22)) (flet ($cvcl_402 (not x_23)) (flet ($cvcl_406 (and $cvcl_402 x_24)) (flet ($cvcl_396 (not x_24)) (flet ($cvcl_398 (and x_23 $cvcl_396)) (flet ($cvcl_386 (and (iff x_32 x_23) (iff x_33 x_24))) (flet ($cvcl_389 (= x_34 x_25)) (flet ($cvcl_382 (and $cvcl_402 $cvcl_396)) (flet ($cvcl_395 (= x_35 0)) (flet ($cvcl_381 (= x_28 0)) (flet ($cvcl_393 (not $cvcl_383)) (flet ($cvcl_390 (= x_35 x_26)) (flet ($cvcl_405 (or $cvcl_402 x_24 )) (flet ($cvcl_392 (not $cvcl_387)) (flet ($cvcl_404 (or x_23 x_24 )) (flet ($cvcl_411 (= x_16 40)) (flet ($cvcl_412 (= x_16 0)) (flet ($cvcl_410 (= x_13 40)) (flet ($cvcl_414 (= x_13 0)) (flet ($cvcl_421 (< (+ (- (* x_16 5) (* x_13 6)) 40) 0)) (flet ($cvcl_418 (= x_17 2)) (flet ($cvcl_415 (= x_22 x_13)) (flet ($cvcl_429 (not x_14)) (flet ($cvcl_433 (and $cvcl_429 x_15)) (flet ($cvcl_423 (not x_15)) (flet ($cvcl_425 (and x_14 $cvcl_423)) (flet ($cvcl_413 (and (iff x_23 x_14) (iff x_24 x_15))) (flet ($cvcl_416 (= x_25 x_16)) (flet ($cvcl_409 (and $cvcl_429 $cvcl_423)) (flet ($cvcl_422 (= x_26 0)) (flet ($cvcl_408 (= x_19 0)) (flet ($cvcl_420 (not $cvcl_410)) (flet ($cvcl_417 (= x_26 x_17)) (flet ($cvcl_432 (or $cvcl_429 x_15 )) (flet ($cvcl_419 (not $cvcl_414)) (flet ($cvcl_431 (or x_14 x_15 )) (flet ($cvcl_438 (= x_6 40)) (flet ($cvcl_439 (= x_6 0)) (flet ($cvcl_437 (= x_3 40)) (flet ($cvcl_441 (= x_3 0)) (flet ($cvcl_448 (< (+ (- (* x_6 5) (* x_3 6)) 40) 0)) (flet ($cvcl_445 (= x_7 2)) (flet ($cvcl_442 (= x_13 x_3)) (flet ($cvcl_456 (not x_4)) (flet ($cvcl_460 (and $cvcl_456 x_5)) (flet ($cvcl_450 (not x_5)) (flet ($cvcl_452 (and x_4 $cvcl_450)) (flet ($cvcl_440 (and (iff x_14 x_4) (iff x_15 x_5))) (flet ($cvcl_443 (= x_16 x_6)) (flet ($cvcl_436 (and $cvcl_456 $cvcl_450)) (flet ($cvcl_449 (= x_17 0)) (flet ($cvcl_435 (= x_10 0)) (flet ($cvcl_447 (not $cvcl_437)) (flet ($cvcl_444 (= x_17 x_7)) (flet ($cvcl_459 (or $cvcl_456 x_5 )) (flet ($cvcl_446 (not $cvcl_441)) (flet ($cvcl_458 (or x_4 x_5 )) (flet ($cvcl_481 (not x_0)) (flet ($cvcl_485 (and $cvcl_481 x_1)) (flet ($cvcl_476 (not x_1)) (flet ($cvcl_478 (and x_0 $cvcl_476)) (flet ($cvcl_467 (and (iff x_4 x_0) (iff x_5 x_1))) (flet ($cvcl_462 (and $cvcl_481 $cvcl_476)) (flet ($cvcl_475 (= x_7 0)) (flet ($cvcl_463 (not x_8)) (flet ($cvcl_484 (or $cvcl_481 x_1 )) (flet ($cvcl_483 (or x_0 x_1 )) (flet ($cvcl_23 (= x_154 1)) (flet ($cvcl_22 (not x_159)) (flet ($cvcl_29 (not (< x_153 0))) (flet ($cvcl_50 (= x_145 1)) (flet ($cvcl_56 (not (< x_144 0))) (flet ($cvcl_77 (= x_136 1)) (flet ($cvcl_83 (not (< x_135 0))) (flet ($cvcl_104 (= x_127 1)) (flet ($cvcl_110 (not (< x_126 0))) (flet ($cvcl_131 (= x_118 1)) (flet ($cvcl_137 (not (< x_117 0))) (flet ($cvcl_158 (= x_109 1)) (flet ($cvcl_164 (not (< x_108 0))) (flet ($cvcl_185 (= x_100 1)) (flet ($cvcl_191 (not (< x_99 0))) (flet ($cvcl_212 (= x_91 1)) (flet ($cvcl_218 (not (< x_90 0))) (flet ($cvcl_239 (= x_82 1)) (flet ($cvcl_245 (not (< x_81 0))) (flet ($cvcl_266 (= x_73 1)) (flet ($cvcl_272 (not (< x_72 0))) (flet ($cvcl_293 (= x_64 1)) (flet ($cvcl_299 (not (< x_63 0))) (flet ($cvcl_320 (= x_55 1)) (flet ($cvcl_326 (not (< x_54 0))) (flet ($cvcl_347 (= x_46 1)) (flet ($cvcl_353 (not (< x_45 0))) (flet ($cvcl_374 (= x_37 1)) (flet ($cvcl_380 (not (< x_36 0))) (flet ($cvcl_401 (= x_28 1)) (flet ($cvcl_407 (not (< x_27 0))) (flet ($cvcl_428 (= x_19 1)) (flet ($cvcl_434 (not (< x_18 0))) (flet ($cvcl_455 (= x_10 1)) (flet ($cvcl_461 (not (< x_9 0))) (flet ($cvcl_19 (= x_160 (ite $cvcl_3 0 (ite $cvcl_4 40 x_151)))) (flet ($cvcl_16 (or $cvcl_6 $cvcl_2 )) (flet ($cvcl_20 (not $cvcl_13)) (flet ($cvcl_25 (and (and (<= (+ x_152 x_153) 2) (not (< (+ x_148 (* x_153 5)) 0))) (<= (+ x_151 (* x_153 6)) 40))) (flet ($cvcl_48 (= x_151 (ite $cvcl_33 0 (ite $cvcl_34 40 x_142)))) (flet ($cvcl_46 (or $cvcl_36 $cvcl_32 )) (flet ($cvcl_49 (not $cvcl_43)) (flet ($cvcl_52 (and (and (<= (+ x_143 x_144) 2) (not (< (+ x_139 (* x_144 5)) 0))) (<= (+ x_142 (* x_144 6)) 40))) (flet ($cvcl_75 (= x_142 (ite $cvcl_60 0 (ite $cvcl_61 40 x_133)))) (flet ($cvcl_73 (or $cvcl_63 $cvcl_59 )) (flet ($cvcl_76 (not $cvcl_70)) (flet ($cvcl_79 (and (and (<= (+ x_134 x_135) 2) (not (< (+ x_130 (* x_135 5)) 0))) (<= (+ x_133 (* x_135 6)) 40))) (flet ($cvcl_102 (= x_133 (ite $cvcl_87 0 (ite $cvcl_88 40 x_124)))) (flet ($cvcl_100 (or $cvcl_90 $cvcl_86 )) (flet ($cvcl_103 (not $cvcl_97)) (flet ($cvcl_106 (and (and (<= (+ x_125 x_126) 2) (not (< (+ x_121 (* x_126 5)) 0))) (<= (+ x_124 (* x_126 6)) 40))) (flet ($cvcl_129 (= x_124 (ite $cvcl_114 0 (ite $cvcl_115 40 x_115)))) (flet ($cvcl_127 (or $cvcl_117 $cvcl_113 )) (flet ($cvcl_130 (not $cvcl_124)) (flet ($cvcl_133 (and (and (<= (+ x_116 x_117) 2) (not (< (+ x_112 (* x_117 5)) 0))) (<= (+ x_115 (* x_117 6)) 40))) (flet ($cvcl_156 (= x_115 (ite $cvcl_141 0 (ite $cvcl_142 40 x_106)))) (flet ($cvcl_154 (or $cvcl_144 $cvcl_140 )) (flet ($cvcl_157 (not $cvcl_151)) (flet ($cvcl_160 (and (and (<= (+ x_107 x_108) 2) (not (< (+ x_103 (* x_108 5)) 0))) (<= (+ x_106 (* x_108 6)) 40))) (flet ($cvcl_183 (= x_106 (ite $cvcl_168 0 (ite $cvcl_169 40 x_97)))) (flet ($cvcl_181 (or $cvcl_171 $cvcl_167 )) (flet ($cvcl_184 (not $cvcl_178)) (flet ($cvcl_187 (and (and (<= (+ x_98 x_99) 2) (not (< (+ x_94 (* x_99 5)) 0))) (<= (+ x_97 (* x_99 6)) 40))) (flet ($cvcl_210 (= x_97 (ite $cvcl_195 0 (ite $cvcl_196 40 x_88)))) (flet ($cvcl_208 (or $cvcl_198 $cvcl_194 )) (flet ($cvcl_211 (not $cvcl_205)) (flet ($cvcl_214 (and (and (<= (+ x_89 x_90) 2) (not (< (+ x_85 (* x_90 5)) 0))) (<= (+ x_88 (* x_90 6)) 40))) (flet ($cvcl_237 (= x_88 (ite $cvcl_222 0 (ite $cvcl_223 40 x_79)))) (flet ($cvcl_235 (or $cvcl_225 $cvcl_221 )) (flet ($cvcl_238 (not $cvcl_232)) (flet ($cvcl_241 (and (and (<= (+ x_80 x_81) 2) (not (< (+ x_76 (* x_81 5)) 0))) (<= (+ x_79 (* x_81 6)) 40))) (flet ($cvcl_264 (= x_79 (ite $cvcl_249 0 (ite $cvcl_250 40 x_70)))) (flet ($cvcl_262 (or $cvcl_252 $cvcl_248 )) (flet ($cvcl_265 (not $cvcl_259)) (flet ($cvcl_268 (and (and (<= (+ x_71 x_72) 2) (not (< (+ x_67 (* x_72 5)) 0))) (<= (+ x_70 (* x_72 6)) 40))) (flet ($cvcl_291 (= x_70 (ite $cvcl_276 0 (ite $cvcl_277 40 x_61)))) (flet ($cvcl_289 (or $cvcl_279 $cvcl_275 )) (flet ($cvcl_292 (not $cvcl_286)) (flet ($cvcl_295 (and (and (<= (+ x_62 x_63) 2) (not (< (+ x_58 (* x_63 5)) 0))) (<= (+ x_61 (* x_63 6)) 40))) (flet ($cvcl_318 (= x_61 (ite $cvcl_303 0 (ite $cvcl_304 40 x_52)))) (flet ($cvcl_316 (or $cvcl_306 $cvcl_302 )) (flet ($cvcl_319 (not $cvcl_313)) (flet ($cvcl_322 (and (and (<= (+ x_53 x_54) 2) (not (< (+ x_49 (* x_54 5)) 0))) (<= (+ x_52 (* x_54 6)) 40))) (flet ($cvcl_345 (= x_52 (ite $cvcl_330 0 (ite $cvcl_331 40 x_43)))) (flet ($cvcl_343 (or $cvcl_333 $cvcl_329 )) (flet ($cvcl_346 (not $cvcl_340)) (flet ($cvcl_349 (and (and (<= (+ x_44 x_45) 2) (not (< (+ x_40 (* x_45 5)) 0))) (<= (+ x_43 (* x_45 6)) 40))) (flet ($cvcl_372 (= x_43 (ite $cvcl_357 0 (ite $cvcl_358 40 x_34)))) (flet ($cvcl_370 (or $cvcl_360 $cvcl_356 )) (flet ($cvcl_373 (not $cvcl_367)) (flet ($cvcl_376 (and (and (<= (+ x_35 x_36) 2) (not (< (+ x_31 (* x_36 5)) 0))) (<= (+ x_34 (* x_36 6)) 40))) (flet ($cvcl_399 (= x_34 (ite $cvcl_384 0 (ite $cvcl_385 40 x_25)))) (flet ($cvcl_397 (or $cvcl_387 $cvcl_383 )) (flet ($cvcl_400 (not $cvcl_394)) (flet ($cvcl_403 (and (and (<= (+ x_26 x_27) 2) (not (< (+ x_22 (* x_27 5)) 0))) (<= (+ x_25 (* x_27 6)) 40))) (flet ($cvcl_426 (= x_25 (ite $cvcl_411 0 (ite $cvcl_412 40 x_16)))) (flet ($cvcl_424 (or $cvcl_414 $cvcl_410 )) (flet ($cvcl_427 (not $cvcl_421)) (flet ($cvcl_430 (and (and (<= (+ x_17 x_18) 2) (not (< (+ x_13 (* x_18 5)) 0))) (<= (+ x_16 (* x_18 6)) 40))) (flet ($cvcl_453 (= x_16 (ite $cvcl_438 0 (ite $cvcl_439 40 x_6)))) (flet ($cvcl_451 (or $cvcl_441 $cvcl_437 )) (flet ($cvcl_454 (not $cvcl_448)) (flet ($cvcl_457 (and (and (<= (+ x_7 x_9) 2) (not (< (+ x_3 (* x_9 5)) 0))) (<= (+ x_6 (* x_9 6)) 40))) (flet ($cvcl_471 (= 2 2)) (flet ($cvcl_468 (= 20 0)) (flet ($cvcl_472 (not $cvcl_468)) (flet ($cvcl_464 (= 20 40)) (flet ($cvcl_473 (not $cvcl_464)) (flet ($cvcl_474 (< (+ (- (* 10 5) (* 20 6)) 40) 0)) (flet ($cvcl_469 (= x_3 20)) (flet ($cvcl_470 (= x_6 10)) (flet ($cvcl_466 (= 10 0)) (flet ($cvcl_465 (= 10 40)) (flet ($cvcl_479 (= x_6 (ite $cvcl_465 0 (ite $cvcl_466 40 10)))) (flet ($cvcl_477 (or $cvcl_468 $cvcl_464 )) (flet ($cvcl_480 (not $cvcl_474)) (flet ($cvcl_482 (and (and (<= (+ 2 x_2) 2) (not (< (+ 20 (* x_2 5)) 0))) (<= (+ 10 (* x_2 6)) 40))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_163 1) (>= x_163 0)) (<= x_154 1)) (>= x_154 0)) (<= x_145 1)) (>= x_145 0)) (<= x_136 1)) (>= x_136 0)) (<= x_127 1)) (>= x_127 0)) (<= x_118 1)) (>= x_118 0)) (<= x_109 1)) (>= x_109 0)) (<= x_100 1)) (>= x_100 0)) (<= x_91 1)) (>= x_91 0)) (<= x_82 1)) (>= x_82 0)) (<= x_73 1)) (>= x_73 0)) (<= x_64 1)) (>= x_64 0)) (<= x_55 1)) (>= x_55 0)) (<= x_46 1)) (>= x_46 0)) (<= x_37 1)) (>= x_37 0)) (<= x_28 1)) (>= x_28 0)) (<= x_19 1)) (>= x_19 0)) (<= x_10 1)) (>= x_10 0)) $cvcl_462) (not (< x_162 0))) (= x_163 (ite $cvcl_23 0 1))) (not (< x_164 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_165 0) $cvcl_0) $cvcl_1) $cvcl_10) $cvcl_11) $cvcl_12) $cvcl_13) $cvcl_14) $cvcl_7) $cvcl_8) $cvcl_5) (and (and (and (and (and (and (and (= x_165 1) $cvcl_0) $cvcl_1) (or (or $cvcl_2 $cvcl_4 ) $cvcl_3 )) (= x_157 (ite $cvcl_2 0 x_148))) $cvcl_19) $cvcl_5) $cvcl_9) ) (and (and (and (and (and (and (and (= x_165 2) $cvcl_0) $cvcl_1) $cvcl_16) $cvcl_17) $cvcl_7) $cvcl_8) $cvcl_9) ) (and (and (and (and (and (and (and (and (and (and (and (= x_165 3) $cvcl_0) $cvcl_1) $cvcl_10) $cvcl_11) $cvcl_12) $cvcl_20) x_158) $cvcl_22) $cvcl_14) $cvcl_7) $cvcl_8) ) (and (and (and (and (and (and (and (= x_165 4) $cvcl_0) $cvcl_18) $cvcl_16) $cvcl_17) $cvcl_7) $cvcl_8) $cvcl_9) ) (and (and (and (and (and (and (and (= x_165 5) $cvcl_0) $cvcl_18) (or (or $cvcl_6 $cvcl_4 ) $cvcl_3 )) (= x_157 (ite $cvcl_6 40 x_148))) $cvcl_19) $cvcl_5) $cvcl_9) ) (and (and (and (and (and (and (and (and (and (and (= x_165 6) $cvcl_0) $cvcl_18) $cvcl_10) $cvcl_11) $cvcl_12) $cvcl_20) $cvcl_14) $cvcl_7) $cvcl_8) $cvcl_5) ) (and (and (and (and (and (and (and (and (and (and (and (= x_165 7) $cvcl_0) $cvcl_18) $cvcl_10) $cvcl_11) $cvcl_12) $cvcl_13) $cvcl_21) $cvcl_22) $cvcl_14) $cvcl_7) $cvcl_8) ) (and (and (and (and (and (and (and (and (and (= x_165 8) $cvcl_23) $cvcl_29) (or $cvcl_26 $cvcl_25 )) (or $cvcl_27 $cvcl_25 )) (or (and $cvcl_26 $cvcl_27) (and (not (< (* x_164 2) (- (* x_151 2) x_153))) (<= x_164 (+ x_151 (* x_153 6)))) )) (= x_161 (ite $cvcl_28 x_152 (+ x_152 x_153)))) (= x_157 (ite $cvcl_28 x_148 (+ x_148 (* x_153 5))))) (= x_160 (ite $cvcl_28 x_151 x_164))) $cvcl_5) )) $cvcl_29) (= x_154 (ite $cvcl_50 0 1))) (not (< x_155 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_156 0) $cvcl_30) $cvcl_31) $cvcl_40) $cvcl_41) $cvcl_42) $cvcl_43) $cvcl_44) $cvcl_37) $cvcl_38) $cvcl_35) (and (and (and (and (and (and (and (= x_156 1) $cvcl_30) $cvcl_31) (or (or $cvcl_32 $cvcl_34 ) $cvcl_33 )) (= x_148 (ite $cvcl_32 0 x_139))) $cvcl_48) $cvcl_35) $cvcl_39) ) (and (and (and (and (and (and (and (= x_156 2) $cvcl_30) $cvcl_31) $cvcl_46) $cvcl_28) $cvcl_37) $cvcl_38) $cvcl_39) ) (and (and (and (and (and (and (and (and (and (and (and (= x_156 3) $cvcl_30) $cvcl_31) $cvcl_40) $cvcl_41) $cvcl_42) $cvcl_49) x_149) $cvcl_15) $cvcl_44) $cvcl_37) $cvcl_38) ) (and (and (and (and (and (and (and (= x_156 4) $cvcl_30) $cvcl_47) $cvcl_46) $cvcl_28) $cvcl_37) $cvcl_38) $cvcl_39) ) (and (and (and (and (and (and (and (= x_156 5) $cvcl_30) $cvcl_47) (or (or $cvcl_36 $cvcl_34 ) $cvcl_33 )) (= x_148 (ite $cvcl_36 40 x_139))) $cvcl_48) $cvcl_35) $cvcl_39) ) (and (and (and (and (and (and (and (and (and (and (= x_156 6) $cvcl_30) $cvcl_47) $cvcl_40) $cvcl_41) $cvcl_42) $cvcl_49) $cvcl_44) $cvcl_37) $cvcl_38) $cvcl_35) ) (and (and (and (and (and (and (and (and (and (and (and (= x_156 7) $cvcl_30) $cvcl_47) $cvcl_40) $cvcl_41) $cvcl_42) $cvcl_43) $cvcl_24) $cvcl_15) $cvcl_44) $cvcl_37) $cvcl_38) ) (and (and (and (and (and (and (and (and (and (= x_156 8) $cvcl_50) $cvcl_56) (or $cvcl_53 $cvcl_52 )) (or $cvcl_54 $cvcl_52 )) (or (and $cvcl_53 $cvcl_54) (and (not (< (* x_155 2) (- (* x_142 2) x_144))) (<= x_155 (+ x_142 (* x_144 6)))) )) (= x_152 (ite $cvcl_55 x_143 (+ x_143 x_144)))) (= x_148 (ite $cvcl_55 x_139 (+ x_139 (* x_144 5))))) (= x_151 (ite $cvcl_55 x_142 x_155))) $cvcl_35) )) $cvcl_56) (= x_145 (ite $cvcl_77 0 1))) (not (< x_146 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_147 0) $cvcl_57) $cvcl_58) $cvcl_67) $cvcl_68) $cvcl_69) $cvcl_70) $cvcl_71) $cvcl_64) $cvcl_65) $cvcl_62) (and (and (and (and (and (and (and (= x_147 1) $cvcl_57) $cvcl_58) (or (or $cvcl_59 $cvcl_61 ) $cvcl_60 )) (= x_139 (ite $cvcl_59 0 x_130))) $cvcl_75) $cvcl_62) $cvcl_66) ) (and (and (and (and (and (and (and (= x_147 2) $cvcl_57) $cvcl_58) $cvcl_73) $cvcl_55) $cvcl_64) $cvcl_65) $cvcl_66) ) (and (and (and (and (and (and (and (and (and (and (and (= x_147 3) $cvcl_57) $cvcl_58) $cvcl_67) $cvcl_68) $cvcl_69) $cvcl_76) x_140) $cvcl_45) $cvcl_71) $cvcl_64) $cvcl_65) ) (and (and (and (and (and (and (and (= x_147 4) $cvcl_57) $cvcl_74) $cvcl_73) $cvcl_55) $cvcl_64) $cvcl_65) $cvcl_66) ) (and (and (and (and (and (and (and (= x_147 5) $cvcl_57) $cvcl_74) (or (or $cvcl_63 $cvcl_61 ) $cvcl_60 )) (= x_139 (ite $cvcl_63 40 x_130))) $cvcl_75) $cvcl_62) $cvcl_66) ) (and (and (and (and (and (and (and (and (and (and (= x_147 6) $cvcl_57) $cvcl_74) $cvcl_67) $cvcl_68) $cvcl_69) $cvcl_76) $cvcl_71) $cvcl_64) $cvcl_65) $cvcl_62) ) (and (and (and (and (and (and (and (and (and (and (and (= x_147 7) $cvcl_57) $cvcl_74) $cvcl_67) $cvcl_68) $cvcl_69) $cvcl_70) $cvcl_51) $cvcl_45) $cvcl_71) $cvcl_64) $cvcl_65) ) (and (and (and (and (and (and (and (and (and (= x_147 8) $cvcl_77) $cvcl_83) (or $cvcl_80 $cvcl_79 )) (or $cvcl_81 $cvcl_79 )) (or (and $cvcl_80 $cvcl_81) (and (not (< (* x_146 2) (- (* x_133 2) x_135))) (<= x_146 (+ x_133 (* x_135 6)))) )) (= x_143 (ite $cvcl_82 x_134 (+ x_134 x_135)))) (= x_139 (ite $cvcl_82 x_130 (+ x_130 (* x_135 5))))) (= x_142 (ite $cvcl_82 x_133 x_146))) $cvcl_62) )) $cvcl_83) (= x_136 (ite $cvcl_104 0 1))) (not (< x_137 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_138 0) $cvcl_84) $cvcl_85) $cvcl_94) $cvcl_95) $cvcl_96) $cvcl_97) $cvcl_98) $cvcl_91) $cvcl_92) $cvcl_89) (and (and (and (and (and (and (and (= x_138 1) $cvcl_84) $cvcl_85) (or (or $cvcl_86 $cvcl_88 ) $cvcl_87 )) (= x_130 (ite $cvcl_86 0 x_121))) $cvcl_102) $cvcl_89) $cvcl_93) ) (and (and (and (and (and (and (and (= x_138 2) $cvcl_84) $cvcl_85) $cvcl_100) $cvcl_82) $cvcl_91) $cvcl_92) $cvcl_93) ) (and (and (and (and (and (and (and (and (and (and (and (= x_138 3) $cvcl_84) $cvcl_85) $cvcl_94) $cvcl_95) $cvcl_96) $cvcl_103) x_131) $cvcl_72) $cvcl_98) $cvcl_91) $cvcl_92) ) (and (and (and (and (and (and (and (= x_138 4) $cvcl_84) $cvcl_101) $cvcl_100) $cvcl_82) $cvcl_91) $cvcl_92) $cvcl_93) ) (and (and (and (and (and (and (and (= x_138 5) $cvcl_84) $cvcl_101) (or (or $cvcl_90 $cvcl_88 ) $cvcl_87 )) (= x_130 (ite $cvcl_90 40 x_121))) $cvcl_102) $cvcl_89) $cvcl_93) ) (and (and (and (and (and (and (and (and (and (and (= x_138 6) $cvcl_84) $cvcl_101) $cvcl_94) $cvcl_95) $cvcl_96) $cvcl_103) $cvcl_98) $cvcl_91) $cvcl_92) $cvcl_89) ) (and (and (and (and (and (and (and (and (and (and (and (= x_138 7) $cvcl_84) $cvcl_101) $cvcl_94) $cvcl_95) $cvcl_96) $cvcl_97) $cvcl_78) $cvcl_72) $cvcl_98) $cvcl_91) $cvcl_92) ) (and (and (and (and (and (and (and (and (and (= x_138 8) $cvcl_104) $cvcl_110) (or $cvcl_107 $cvcl_106 )) (or $cvcl_108 $cvcl_106 )) (or (and $cvcl_107 $cvcl_108) (and (not (< (* x_137 2) (- (* x_124 2) x_126))) (<= x_137 (+ x_124 (* x_126 6)))) )) (= x_134 (ite $cvcl_109 x_125 (+ x_125 x_126)))) (= x_130 (ite $cvcl_109 x_121 (+ x_121 (* x_126 5))))) (= x_133 (ite $cvcl_109 x_124 x_137))) $cvcl_89) )) $cvcl_110) (= x_127 (ite $cvcl_131 0 1))) (not (< x_128 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_129 0) $cvcl_111) $cvcl_112) $cvcl_121) $cvcl_122) $cvcl_123) $cvcl_124) $cvcl_125) $cvcl_118) $cvcl_119) $cvcl_116) (and (and (and (and (and (and (and (= x_129 1) $cvcl_111) $cvcl_112) (or (or $cvcl_113 $cvcl_115 ) $cvcl_114 )) (= x_121 (ite $cvcl_113 0 x_112))) $cvcl_129) $cvcl_116) $cvcl_120) ) (and (and (and (and (and (and (and (= x_129 2) $cvcl_111) $cvcl_112) $cvcl_127) $cvcl_109) $cvcl_118) $cvcl_119) $cvcl_120) ) (and (and (and (and (and (and (and (and (and (and (and (= x_129 3) $cvcl_111) $cvcl_112) $cvcl_121) $cvcl_122) $cvcl_123) $cvcl_130) x_122) $cvcl_99) $cvcl_125) $cvcl_118) $cvcl_119) ) (and (and (and (and (and (and (and (= x_129 4) $cvcl_111) $cvcl_128) $cvcl_127) $cvcl_109) $cvcl_118) $cvcl_119) $cvcl_120) ) (and (and (and (and (and (and (and (= x_129 5) $cvcl_111) $cvcl_128) (or (or $cvcl_117 $cvcl_115 ) $cvcl_114 )) (= x_121 (ite $cvcl_117 40 x_112))) $cvcl_129) $cvcl_116) $cvcl_120) ) (and (and (and (and (and (and (and (and (and (and (= x_129 6) $cvcl_111) $cvcl_128) $cvcl_121) $cvcl_122) $cvcl_123) $cvcl_130) $cvcl_125) $cvcl_118) $cvcl_119) $cvcl_116) ) (and (and (and (and (and (and (and (and (and (and (and (= x_129 7) $cvcl_111) $cvcl_128) $cvcl_121) $cvcl_122) $cvcl_123) $cvcl_124) $cvcl_105) $cvcl_99) $cvcl_125) $cvcl_118) $cvcl_119) ) (and (and (and (and (and (and (and (and (and (= x_129 8) $cvcl_131) $cvcl_137) (or $cvcl_134 $cvcl_133 )) (or $cvcl_135 $cvcl_133 )) (or (and $cvcl_134 $cvcl_135) (and (not (< (* x_128 2) (- (* x_115 2) x_117))) (<= x_128 (+ x_115 (* x_117 6)))) )) (= x_125 (ite $cvcl_136 x_116 (+ x_116 x_117)))) (= x_121 (ite $cvcl_136 x_112 (+ x_112 (* x_117 5))))) (= x_124 (ite $cvcl_136 x_115 x_128))) $cvcl_116) )) $cvcl_137) (= x_118 (ite $cvcl_158 0 1))) (not (< x_119 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_120 0) $cvcl_138) $cvcl_139) $cvcl_148) $cvcl_149) $cvcl_150) $cvcl_151) $cvcl_152) $cvcl_145) $cvcl_146) $cvcl_143) (and (and (and (and (and (and (and (= x_120 1) $cvcl_138) $cvcl_139) (or (or $cvcl_140 $cvcl_142 ) $cvcl_141 )) (= x_112 (ite $cvcl_140 0 x_103))) $cvcl_156) $cvcl_143) $cvcl_147) ) (and (and (and (and (and (and (and (= x_120 2) $cvcl_138) $cvcl_139) $cvcl_154) $cvcl_136) $cvcl_145) $cvcl_146) $cvcl_147) ) (and (and (and (and (and (and (and (and (and (and (and (= x_120 3) $cvcl_138) $cvcl_139) $cvcl_148) $cvcl_149) $cvcl_150) $cvcl_157) x_113) $cvcl_126) $cvcl_152) $cvcl_145) $cvcl_146) ) (and (and (and (and (and (and (and (= x_120 4) $cvcl_138) $cvcl_155) $cvcl_154) $cvcl_136) $cvcl_145) $cvcl_146) $cvcl_147) ) (and (and (and (and (and (and (and (= x_120 5) $cvcl_138) $cvcl_155) (or (or $cvcl_144 $cvcl_142 ) $cvcl_141 )) (= x_112 (ite $cvcl_144 40 x_103))) $cvcl_156) $cvcl_143) $cvcl_147) ) (and (and (and (and (and (and (and (and (and (and (= x_120 6) $cvcl_138) $cvcl_155) $cvcl_148) $cvcl_149) $cvcl_150) $cvcl_157) $cvcl_152) $cvcl_145) $cvcl_146) $cvcl_143) ) (and (and (and (and (and (and (and (and (and (and (and (= x_120 7) $cvcl_138) $cvcl_155) $cvcl_148) $cvcl_149) $cvcl_150) $cvcl_151) $cvcl_132) $cvcl_126) $cvcl_152) $cvcl_145) $cvcl_146) ) (and (and (and (and (and (and (and (and (and (= x_120 8) $cvcl_158) $cvcl_164) (or $cvcl_161 $cvcl_160 )) (or $cvcl_162 $cvcl_160 )) (or (and $cvcl_161 $cvcl_162) (and (not (< (* x_119 2) (- (* x_106 2) x_108))) (<= x_119 (+ x_106 (* x_108 6)))) )) (= x_116 (ite $cvcl_163 x_107 (+ x_107 x_108)))) (= x_112 (ite $cvcl_163 x_103 (+ x_103 (* x_108 5))))) (= x_115 (ite $cvcl_163 x_106 x_119))) $cvcl_143) )) $cvcl_164) (= x_109 (ite $cvcl_185 0 1))) (not (< x_110 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_111 0) $cvcl_165) $cvcl_166) $cvcl_175) $cvcl_176) $cvcl_177) $cvcl_178) $cvcl_179) $cvcl_172) $cvcl_173) $cvcl_170) (and (and (and (and (and (and (and (= x_111 1) $cvcl_165) $cvcl_166) (or (or $cvcl_167 $cvcl_169 ) $cvcl_168 )) (= x_103 (ite $cvcl_167 0 x_94))) $cvcl_183) $cvcl_170) $cvcl_174) ) (and (and (and (and (and (and (and (= x_111 2) $cvcl_165) $cvcl_166) $cvcl_181) $cvcl_163) $cvcl_172) $cvcl_173) $cvcl_174) ) (and (and (and (and (and (and (and (and (and (and (and (= x_111 3) $cvcl_165) $cvcl_166) $cvcl_175) $cvcl_176) $cvcl_177) $cvcl_184) x_104) $cvcl_153) $cvcl_179) $cvcl_172) $cvcl_173) ) (and (and (and (and (and (and (and (= x_111 4) $cvcl_165) $cvcl_182) $cvcl_181) $cvcl_163) $cvcl_172) $cvcl_173) $cvcl_174) ) (and (and (and (and (and (and (and (= x_111 5) $cvcl_165) $cvcl_182) (or (or $cvcl_171 $cvcl_169 ) $cvcl_168 )) (= x_103 (ite $cvcl_171 40 x_94))) $cvcl_183) $cvcl_170) $cvcl_174) ) (and (and (and (and (and (and (and (and (and (and (= x_111 6) $cvcl_165) $cvcl_182) $cvcl_175) $cvcl_176) $cvcl_177) $cvcl_184) $cvcl_179) $cvcl_172) $cvcl_173) $cvcl_170) ) (and (and (and (and (and (and (and (and (and (and (and (= x_111 7) $cvcl_165) $cvcl_182) $cvcl_175) $cvcl_176) $cvcl_177) $cvcl_178) $cvcl_159) $cvcl_153) $cvcl_179) $cvcl_172) $cvcl_173) ) (and (and (and (and (and (and (and (and (and (= x_111 8) $cvcl_185) $cvcl_191) (or $cvcl_188 $cvcl_187 )) (or $cvcl_189 $cvcl_187 )) (or (and $cvcl_188 $cvcl_189) (and (not (< (* x_110 2) (- (* x_97 2) x_99))) (<= x_110 (+ x_97 (* x_99 6)))) )) (= x_107 (ite $cvcl_190 x_98 (+ x_98 x_99)))) (= x_103 (ite $cvcl_190 x_94 (+ x_94 (* x_99 5))))) (= x_106 (ite $cvcl_190 x_97 x_110))) $cvcl_170) )) $cvcl_191) (= x_100 (ite $cvcl_212 0 1))) (not (< x_101 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_102 0) $cvcl_192) $cvcl_193) $cvcl_202) $cvcl_203) $cvcl_204) $cvcl_205) $cvcl_206) $cvcl_199) $cvcl_200) $cvcl_197) (and (and (and (and (and (and (and (= x_102 1) $cvcl_192) $cvcl_193) (or (or $cvcl_194 $cvcl_196 ) $cvcl_195 )) (= x_94 (ite $cvcl_194 0 x_85))) $cvcl_210) $cvcl_197) $cvcl_201) ) (and (and (and (and (and (and (and (= x_102 2) $cvcl_192) $cvcl_193) $cvcl_208) $cvcl_190) $cvcl_199) $cvcl_200) $cvcl_201) ) (and (and (and (and (and (and (and (and (and (and (and (= x_102 3) $cvcl_192) $cvcl_193) $cvcl_202) $cvcl_203) $cvcl_204) $cvcl_211) x_95) $cvcl_180) $cvcl_206) $cvcl_199) $cvcl_200) ) (and (and (and (and (and (and (and (= x_102 4) $cvcl_192) $cvcl_209) $cvcl_208) $cvcl_190) $cvcl_199) $cvcl_200) $cvcl_201) ) (and (and (and (and (and (and (and (= x_102 5) $cvcl_192) $cvcl_209) (or (or $cvcl_198 $cvcl_196 ) $cvcl_195 )) (= x_94 (ite $cvcl_198 40 x_85))) $cvcl_210) $cvcl_197) $cvcl_201) ) (and (and (and (and (and (and (and (and (and (and (= x_102 6) $cvcl_192) $cvcl_209) $cvcl_202) $cvcl_203) $cvcl_204) $cvcl_211) $cvcl_206) $cvcl_199) $cvcl_200) $cvcl_197) ) (and (and (and (and (and (and (and (and (and (and (and (= x_102 7) $cvcl_192) $cvcl_209) $cvcl_202) $cvcl_203) $cvcl_204) $cvcl_205) $cvcl_186) $cvcl_180) $cvcl_206) $cvcl_199) $cvcl_200) ) (and (and (and (and (and (and (and (and (and (= x_102 8) $cvcl_212) $cvcl_218) (or $cvcl_215 $cvcl_214 )) (or $cvcl_216 $cvcl_214 )) (or (and $cvcl_215 $cvcl_216) (and (not (< (* x_101 2) (- (* x_88 2) x_90))) (<= x_101 (+ x_88 (* x_90 6)))) )) (= x_98 (ite $cvcl_217 x_89 (+ x_89 x_90)))) (= x_94 (ite $cvcl_217 x_85 (+ x_85 (* x_90 5))))) (= x_97 (ite $cvcl_217 x_88 x_101))) $cvcl_197) )) $cvcl_218) (= x_91 (ite $cvcl_239 0 1))) (not (< x_92 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_93 0) $cvcl_219) $cvcl_220) $cvcl_229) $cvcl_230) $cvcl_231) $cvcl_232) $cvcl_233) $cvcl_226) $cvcl_227) $cvcl_224) (and (and (and (and (and (and (and (= x_93 1) $cvcl_219) $cvcl_220) (or (or $cvcl_221 $cvcl_223 ) $cvcl_222 )) (= x_85 (ite $cvcl_221 0 x_76))) $cvcl_237) $cvcl_224) $cvcl_228) ) (and (and (and (and (and (and (and (= x_93 2) $cvcl_219) $cvcl_220) $cvcl_235) $cvcl_217) $cvcl_226) $cvcl_227) $cvcl_228) ) (and (and (and (and (and (and (and (and (and (and (and (= x_93 3) $cvcl_219) $cvcl_220) $cvcl_229) $cvcl_230) $cvcl_231) $cvcl_238) x_86) $cvcl_207) $cvcl_233) $cvcl_226) $cvcl_227) ) (and (and (and (and (and (and (and (= x_93 4) $cvcl_219) $cvcl_236) $cvcl_235) $cvcl_217) $cvcl_226) $cvcl_227) $cvcl_228) ) (and (and (and (and (and (and (and (= x_93 5) $cvcl_219) $cvcl_236) (or (or $cvcl_225 $cvcl_223 ) $cvcl_222 )) (= x_85 (ite $cvcl_225 40 x_76))) $cvcl_237) $cvcl_224) $cvcl_228) ) (and (and (and (and (and (and (and (and (and (and (= x_93 6) $cvcl_219) $cvcl_236) $cvcl_229) $cvcl_230) $cvcl_231) $cvcl_238) $cvcl_233) $cvcl_226) $cvcl_227) $cvcl_224) ) (and (and (and (and (and (and (and (and (and (and (and (= x_93 7) $cvcl_219) $cvcl_236) $cvcl_229) $cvcl_230) $cvcl_231) $cvcl_232) $cvcl_213) $cvcl_207) $cvcl_233) $cvcl_226) $cvcl_227) ) (and (and (and (and (and (and (and (and (and (= x_93 8) $cvcl_239) $cvcl_245) (or $cvcl_242 $cvcl_241 )) (or $cvcl_243 $cvcl_241 )) (or (and $cvcl_242 $cvcl_243) (and (not (< (* x_92 2) (- (* x_79 2) x_81))) (<= x_92 (+ x_79 (* x_81 6)))) )) (= x_89 (ite $cvcl_244 x_80 (+ x_80 x_81)))) (= x_85 (ite $cvcl_244 x_76 (+ x_76 (* x_81 5))))) (= x_88 (ite $cvcl_244 x_79 x_92))) $cvcl_224) )) $cvcl_245) (= x_82 (ite $cvcl_266 0 1))) (not (< x_83 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_84 0) $cvcl_246) $cvcl_247) $cvcl_256) $cvcl_257) $cvcl_258) $cvcl_259) $cvcl_260) $cvcl_253) $cvcl_254) $cvcl_251) (and (and (and (and (and (and (and (= x_84 1) $cvcl_246) $cvcl_247) (or (or $cvcl_248 $cvcl_250 ) $cvcl_249 )) (= x_76 (ite $cvcl_248 0 x_67))) $cvcl_264) $cvcl_251) $cvcl_255) ) (and (and (and (and (and (and (and (= x_84 2) $cvcl_246) $cvcl_247) $cvcl_262) $cvcl_244) $cvcl_253) $cvcl_254) $cvcl_255) ) (and (and (and (and (and (and (and (and (and (and (and (= x_84 3) $cvcl_246) $cvcl_247) $cvcl_256) $cvcl_257) $cvcl_258) $cvcl_265) x_77) $cvcl_234) $cvcl_260) $cvcl_253) $cvcl_254) ) (and (and (and (and (and (and (and (= x_84 4) $cvcl_246) $cvcl_263) $cvcl_262) $cvcl_244) $cvcl_253) $cvcl_254) $cvcl_255) ) (and (and (and (and (and (and (and (= x_84 5) $cvcl_246) $cvcl_263) (or (or $cvcl_252 $cvcl_250 ) $cvcl_249 )) (= x_76 (ite $cvcl_252 40 x_67))) $cvcl_264) $cvcl_251) $cvcl_255) ) (and (and (and (and (and (and (and (and (and (and (= x_84 6) $cvcl_246) $cvcl_263) $cvcl_256) $cvcl_257) $cvcl_258) $cvcl_265) $cvcl_260) $cvcl_253) $cvcl_254) $cvcl_251) ) (and (and (and (and (and (and (and (and (and (and (and (= x_84 7) $cvcl_246) $cvcl_263) $cvcl_256) $cvcl_257) $cvcl_258) $cvcl_259) $cvcl_240) $cvcl_234) $cvcl_260) $cvcl_253) $cvcl_254) ) (and (and (and (and (and (and (and (and (and (= x_84 8) $cvcl_266) $cvcl_272) (or $cvcl_269 $cvcl_268 )) (or $cvcl_270 $cvcl_268 )) (or (and $cvcl_269 $cvcl_270) (and (not (< (* x_83 2) (- (* x_70 2) x_72))) (<= x_83 (+ x_70 (* x_72 6)))) )) (= x_80 (ite $cvcl_271 x_71 (+ x_71 x_72)))) (= x_76 (ite $cvcl_271 x_67 (+ x_67 (* x_72 5))))) (= x_79 (ite $cvcl_271 x_70 x_83))) $cvcl_251) )) $cvcl_272) (= x_73 (ite $cvcl_293 0 1))) (not (< x_74 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_75 0) $cvcl_273) $cvcl_274) $cvcl_283) $cvcl_284) $cvcl_285) $cvcl_286) $cvcl_287) $cvcl_280) $cvcl_281) $cvcl_278) (and (and (and (and (and (and (and (= x_75 1) $cvcl_273) $cvcl_274) (or (or $cvcl_275 $cvcl_277 ) $cvcl_276 )) (= x_67 (ite $cvcl_275 0 x_58))) $cvcl_291) $cvcl_278) $cvcl_282) ) (and (and (and (and (and (and (and (= x_75 2) $cvcl_273) $cvcl_274) $cvcl_289) $cvcl_271) $cvcl_280) $cvcl_281) $cvcl_282) ) (and (and (and (and (and (and (and (and (and (and (and (= x_75 3) $cvcl_273) $cvcl_274) $cvcl_283) $cvcl_284) $cvcl_285) $cvcl_292) x_68) $cvcl_261) $cvcl_287) $cvcl_280) $cvcl_281) ) (and (and (and (and (and (and (and (= x_75 4) $cvcl_273) $cvcl_290) $cvcl_289) $cvcl_271) $cvcl_280) $cvcl_281) $cvcl_282) ) (and (and (and (and (and (and (and (= x_75 5) $cvcl_273) $cvcl_290) (or (or $cvcl_279 $cvcl_277 ) $cvcl_276 )) (= x_67 (ite $cvcl_279 40 x_58))) $cvcl_291) $cvcl_278) $cvcl_282) ) (and (and (and (and (and (and (and (and (and (and (= x_75 6) $cvcl_273) $cvcl_290) $cvcl_283) $cvcl_284) $cvcl_285) $cvcl_292) $cvcl_287) $cvcl_280) $cvcl_281) $cvcl_278) ) (and (and (and (and (and (and (and (and (and (and (and (= x_75 7) $cvcl_273) $cvcl_290) $cvcl_283) $cvcl_284) $cvcl_285) $cvcl_286) $cvcl_267) $cvcl_261) $cvcl_287) $cvcl_280) $cvcl_281) ) (and (and (and (and (and (and (and (and (and (= x_75 8) $cvcl_293) $cvcl_299) (or $cvcl_296 $cvcl_295 )) (or $cvcl_297 $cvcl_295 )) (or (and $cvcl_296 $cvcl_297) (and (not (< (* x_74 2) (- (* x_61 2) x_63))) (<= x_74 (+ x_61 (* x_63 6)))) )) (= x_71 (ite $cvcl_298 x_62 (+ x_62 x_63)))) (= x_67 (ite $cvcl_298 x_58 (+ x_58 (* x_63 5))))) (= x_70 (ite $cvcl_298 x_61 x_74))) $cvcl_278) )) $cvcl_299) (= x_64 (ite $cvcl_320 0 1))) (not (< x_65 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_66 0) $cvcl_300) $cvcl_301) $cvcl_310) $cvcl_311) $cvcl_312) $cvcl_313) $cvcl_314) $cvcl_307) $cvcl_308) $cvcl_305) (and (and (and (and (and (and (and (= x_66 1) $cvcl_300) $cvcl_301) (or (or $cvcl_302 $cvcl_304 ) $cvcl_303 )) (= x_58 (ite $cvcl_302 0 x_49))) $cvcl_318) $cvcl_305) $cvcl_309) ) (and (and (and (and (and (and (and (= x_66 2) $cvcl_300) $cvcl_301) $cvcl_316) $cvcl_298) $cvcl_307) $cvcl_308) $cvcl_309) ) (and (and (and (and (and (and (and (and (and (and (and (= x_66 3) $cvcl_300) $cvcl_301) $cvcl_310) $cvcl_311) $cvcl_312) $cvcl_319) x_59) $cvcl_288) $cvcl_314) $cvcl_307) $cvcl_308) ) (and (and (and (and (and (and (and (= x_66 4) $cvcl_300) $cvcl_317) $cvcl_316) $cvcl_298) $cvcl_307) $cvcl_308) $cvcl_309) ) (and (and (and (and (and (and (and (= x_66 5) $cvcl_300) $cvcl_317) (or (or $cvcl_306 $cvcl_304 ) $cvcl_303 )) (= x_58 (ite $cvcl_306 40 x_49))) $cvcl_318) $cvcl_305) $cvcl_309) ) (and (and (and (and (and (and (and (and (and (and (= x_66 6) $cvcl_300) $cvcl_317) $cvcl_310) $cvcl_311) $cvcl_312) $cvcl_319) $cvcl_314) $cvcl_307) $cvcl_308) $cvcl_305) ) (and (and (and (and (and (and (and (and (and (and (and (= x_66 7) $cvcl_300) $cvcl_317) $cvcl_310) $cvcl_311) $cvcl_312) $cvcl_313) $cvcl_294) $cvcl_288) $cvcl_314) $cvcl_307) $cvcl_308) ) (and (and (and (and (and (and (and (and (and (= x_66 8) $cvcl_320) $cvcl_326) (or $cvcl_323 $cvcl_322 )) (or $cvcl_324 $cvcl_322 )) (or (and $cvcl_323 $cvcl_324) (and (not (< (* x_65 2) (- (* x_52 2) x_54))) (<= x_65 (+ x_52 (* x_54 6)))) )) (= x_62 (ite $cvcl_325 x_53 (+ x_53 x_54)))) (= x_58 (ite $cvcl_325 x_49 (+ x_49 (* x_54 5))))) (= x_61 (ite $cvcl_325 x_52 x_65))) $cvcl_305) )) $cvcl_326) (= x_55 (ite $cvcl_347 0 1))) (not (< x_56 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_57 0) $cvcl_327) $cvcl_328) $cvcl_337) $cvcl_338) $cvcl_339) $cvcl_340) $cvcl_341) $cvcl_334) $cvcl_335) $cvcl_332) (and (and (and (and (and (and (and (= x_57 1) $cvcl_327) $cvcl_328) (or (or $cvcl_329 $cvcl_331 ) $cvcl_330 )) (= x_49 (ite $cvcl_329 0 x_40))) $cvcl_345) $cvcl_332) $cvcl_336) ) (and (and (and (and (and (and (and (= x_57 2) $cvcl_327) $cvcl_328) $cvcl_343) $cvcl_325) $cvcl_334) $cvcl_335) $cvcl_336) ) (and (and (and (and (and (and (and (and (and (and (and (= x_57 3) $cvcl_327) $cvcl_328) $cvcl_337) $cvcl_338) $cvcl_339) $cvcl_346) x_50) $cvcl_315) $cvcl_341) $cvcl_334) $cvcl_335) ) (and (and (and (and (and (and (and (= x_57 4) $cvcl_327) $cvcl_344) $cvcl_343) $cvcl_325) $cvcl_334) $cvcl_335) $cvcl_336) ) (and (and (and (and (and (and (and (= x_57 5) $cvcl_327) $cvcl_344) (or (or $cvcl_333 $cvcl_331 ) $cvcl_330 )) (= x_49 (ite $cvcl_333 40 x_40))) $cvcl_345) $cvcl_332) $cvcl_336) ) (and (and (and (and (and (and (and (and (and (and (= x_57 6) $cvcl_327) $cvcl_344) $cvcl_337) $cvcl_338) $cvcl_339) $cvcl_346) $cvcl_341) $cvcl_334) $cvcl_335) $cvcl_332) ) (and (and (and (and (and (and (and (and (and (and (and (= x_57 7) $cvcl_327) $cvcl_344) $cvcl_337) $cvcl_338) $cvcl_339) $cvcl_340) $cvcl_321) $cvcl_315) $cvcl_341) $cvcl_334) $cvcl_335) ) (and (and (and (and (and (and (and (and (and (= x_57 8) $cvcl_347) $cvcl_353) (or $cvcl_350 $cvcl_349 )) (or $cvcl_351 $cvcl_349 )) (or (and $cvcl_350 $cvcl_351) (and (not (< (* x_56 2) (- (* x_43 2) x_45))) (<= x_56 (+ x_43 (* x_45 6)))) )) (= x_53 (ite $cvcl_352 x_44 (+ x_44 x_45)))) (= x_49 (ite $cvcl_352 x_40 (+ x_40 (* x_45 5))))) (= x_52 (ite $cvcl_352 x_43 x_56))) $cvcl_332) )) $cvcl_353) (= x_46 (ite $cvcl_374 0 1))) (not (< x_47 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_48 0) $cvcl_354) $cvcl_355) $cvcl_364) $cvcl_365) $cvcl_366) $cvcl_367) $cvcl_368) $cvcl_361) $cvcl_362) $cvcl_359) (and (and (and (and (and (and (and (= x_48 1) $cvcl_354) $cvcl_355) (or (or $cvcl_356 $cvcl_358 ) $cvcl_357 )) (= x_40 (ite $cvcl_356 0 x_31))) $cvcl_372) $cvcl_359) $cvcl_363) ) (and (and (and (and (and (and (and (= x_48 2) $cvcl_354) $cvcl_355) $cvcl_370) $cvcl_352) $cvcl_361) $cvcl_362) $cvcl_363) ) (and (and (and (and (and (and (and (and (and (and (and (= x_48 3) $cvcl_354) $cvcl_355) $cvcl_364) $cvcl_365) $cvcl_366) $cvcl_373) x_41) $cvcl_342) $cvcl_368) $cvcl_361) $cvcl_362) ) (and (and (and (and (and (and (and (= x_48 4) $cvcl_354) $cvcl_371) $cvcl_370) $cvcl_352) $cvcl_361) $cvcl_362) $cvcl_363) ) (and (and (and (and (and (and (and (= x_48 5) $cvcl_354) $cvcl_371) (or (or $cvcl_360 $cvcl_358 ) $cvcl_357 )) (= x_40 (ite $cvcl_360 40 x_31))) $cvcl_372) $cvcl_359) $cvcl_363) ) (and (and (and (and (and (and (and (and (and (and (= x_48 6) $cvcl_354) $cvcl_371) $cvcl_364) $cvcl_365) $cvcl_366) $cvcl_373) $cvcl_368) $cvcl_361) $cvcl_362) $cvcl_359) ) (and (and (and (and (and (and (and (and (and (and (and (= x_48 7) $cvcl_354) $cvcl_371) $cvcl_364) $cvcl_365) $cvcl_366) $cvcl_367) $cvcl_348) $cvcl_342) $cvcl_368) $cvcl_361) $cvcl_362) ) (and (and (and (and (and (and (and (and (and (= x_48 8) $cvcl_374) $cvcl_380) (or $cvcl_377 $cvcl_376 )) (or $cvcl_378 $cvcl_376 )) (or (and $cvcl_377 $cvcl_378) (and (not (< (* x_47 2) (- (* x_34 2) x_36))) (<= x_47 (+ x_34 (* x_36 6)))) )) (= x_44 (ite $cvcl_379 x_35 (+ x_35 x_36)))) (= x_40 (ite $cvcl_379 x_31 (+ x_31 (* x_36 5))))) (= x_43 (ite $cvcl_379 x_34 x_47))) $cvcl_359) )) $cvcl_380) (= x_37 (ite $cvcl_401 0 1))) (not (< x_38 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_39 0) $cvcl_381) $cvcl_382) $cvcl_391) $cvcl_392) $cvcl_393) $cvcl_394) $cvcl_395) $cvcl_388) $cvcl_389) $cvcl_386) (and (and (and (and (and (and (and (= x_39 1) $cvcl_381) $cvcl_382) (or (or $cvcl_383 $cvcl_385 ) $cvcl_384 )) (= x_31 (ite $cvcl_383 0 x_22))) $cvcl_399) $cvcl_386) $cvcl_390) ) (and (and (and (and (and (and (and (= x_39 2) $cvcl_381) $cvcl_382) $cvcl_397) $cvcl_379) $cvcl_388) $cvcl_389) $cvcl_390) ) (and (and (and (and (and (and (and (and (and (and (and (= x_39 3) $cvcl_381) $cvcl_382) $cvcl_391) $cvcl_392) $cvcl_393) $cvcl_400) x_32) $cvcl_369) $cvcl_395) $cvcl_388) $cvcl_389) ) (and (and (and (and (and (and (and (= x_39 4) $cvcl_381) $cvcl_398) $cvcl_397) $cvcl_379) $cvcl_388) $cvcl_389) $cvcl_390) ) (and (and (and (and (and (and (and (= x_39 5) $cvcl_381) $cvcl_398) (or (or $cvcl_387 $cvcl_385 ) $cvcl_384 )) (= x_31 (ite $cvcl_387 40 x_22))) $cvcl_399) $cvcl_386) $cvcl_390) ) (and (and (and (and (and (and (and (and (and (and (= x_39 6) $cvcl_381) $cvcl_398) $cvcl_391) $cvcl_392) $cvcl_393) $cvcl_400) $cvcl_395) $cvcl_388) $cvcl_389) $cvcl_386) ) (and (and (and (and (and (and (and (and (and (and (and (= x_39 7) $cvcl_381) $cvcl_398) $cvcl_391) $cvcl_392) $cvcl_393) $cvcl_394) $cvcl_375) $cvcl_369) $cvcl_395) $cvcl_388) $cvcl_389) ) (and (and (and (and (and (and (and (and (and (= x_39 8) $cvcl_401) $cvcl_407) (or $cvcl_404 $cvcl_403 )) (or $cvcl_405 $cvcl_403 )) (or (and $cvcl_404 $cvcl_405) (and (not (< (* x_38 2) (- (* x_25 2) x_27))) (<= x_38 (+ x_25 (* x_27 6)))) )) (= x_35 (ite $cvcl_406 x_26 (+ x_26 x_27)))) (= x_31 (ite $cvcl_406 x_22 (+ x_22 (* x_27 5))))) (= x_34 (ite $cvcl_406 x_25 x_38))) $cvcl_386) )) $cvcl_407) (= x_28 (ite $cvcl_428 0 1))) (not (< x_29 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_30 0) $cvcl_408) $cvcl_409) $cvcl_418) $cvcl_419) $cvcl_420) $cvcl_421) $cvcl_422) $cvcl_415) $cvcl_416) $cvcl_413) (and (and (and (and (and (and (and (= x_30 1) $cvcl_408) $cvcl_409) (or (or $cvcl_410 $cvcl_412 ) $cvcl_411 )) (= x_22 (ite $cvcl_410 0 x_13))) $cvcl_426) $cvcl_413) $cvcl_417) ) (and (and (and (and (and (and (and (= x_30 2) $cvcl_408) $cvcl_409) $cvcl_424) $cvcl_406) $cvcl_415) $cvcl_416) $cvcl_417) ) (and (and (and (and (and (and (and (and (and (and (and (= x_30 3) $cvcl_408) $cvcl_409) $cvcl_418) $cvcl_419) $cvcl_420) $cvcl_427) x_23) $cvcl_396) $cvcl_422) $cvcl_415) $cvcl_416) ) (and (and (and (and (and (and (and (= x_30 4) $cvcl_408) $cvcl_425) $cvcl_424) $cvcl_406) $cvcl_415) $cvcl_416) $cvcl_417) ) (and (and (and (and (and (and (and (= x_30 5) $cvcl_408) $cvcl_425) (or (or $cvcl_414 $cvcl_412 ) $cvcl_411 )) (= x_22 (ite $cvcl_414 40 x_13))) $cvcl_426) $cvcl_413) $cvcl_417) ) (and (and (and (and (and (and (and (and (and (and (= x_30 6) $cvcl_408) $cvcl_425) $cvcl_418) $cvcl_419) $cvcl_420) $cvcl_427) $cvcl_422) $cvcl_415) $cvcl_416) $cvcl_413) ) (and (and (and (and (and (and (and (and (and (and (and (= x_30 7) $cvcl_408) $cvcl_425) $cvcl_418) $cvcl_419) $cvcl_420) $cvcl_421) $cvcl_402) $cvcl_396) $cvcl_422) $cvcl_415) $cvcl_416) ) (and (and (and (and (and (and (and (and (and (= x_30 8) $cvcl_428) $cvcl_434) (or $cvcl_431 $cvcl_430 )) (or $cvcl_432 $cvcl_430 )) (or (and $cvcl_431 $cvcl_432) (and (not (< (* x_29 2) (- (* x_16 2) x_18))) (<= x_29 (+ x_16 (* x_18 6)))) )) (= x_26 (ite $cvcl_433 x_17 (+ x_17 x_18)))) (= x_22 (ite $cvcl_433 x_13 (+ x_13 (* x_18 5))))) (= x_25 (ite $cvcl_433 x_16 x_29))) $cvcl_413) )) $cvcl_434) (= x_19 (ite $cvcl_455 0 1))) (not (< x_20 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_21 0) $cvcl_435) $cvcl_436) $cvcl_445) $cvcl_446) $cvcl_447) $cvcl_448) $cvcl_449) $cvcl_442) $cvcl_443) $cvcl_440) (and (and (and (and (and (and (and (= x_21 1) $cvcl_435) $cvcl_436) (or (or $cvcl_437 $cvcl_439 ) $cvcl_438 )) (= x_13 (ite $cvcl_437 0 x_3))) $cvcl_453) $cvcl_440) $cvcl_444) ) (and (and (and (and (and (and (and (= x_21 2) $cvcl_435) $cvcl_436) $cvcl_451) $cvcl_433) $cvcl_442) $cvcl_443) $cvcl_444) ) (and (and (and (and (and (and (and (and (and (and (and (= x_21 3) $cvcl_435) $cvcl_436) $cvcl_445) $cvcl_446) $cvcl_447) $cvcl_454) x_14) $cvcl_423) $cvcl_449) $cvcl_442) $cvcl_443) ) (and (and (and (and (and (and (and (= x_21 4) $cvcl_435) $cvcl_452) $cvcl_451) $cvcl_433) $cvcl_442) $cvcl_443) $cvcl_444) ) (and (and (and (and (and (and (and (= x_21 5) $cvcl_435) $cvcl_452) (or (or $cvcl_441 $cvcl_439 ) $cvcl_438 )) (= x_13 (ite $cvcl_441 40 x_3))) $cvcl_453) $cvcl_440) $cvcl_444) ) (and (and (and (and (and (and (and (and (and (and (= x_21 6) $cvcl_435) $cvcl_452) $cvcl_445) $cvcl_446) $cvcl_447) $cvcl_454) $cvcl_449) $cvcl_442) $cvcl_443) $cvcl_440) ) (and (and (and (and (and (and (and (and (and (and (and (= x_21 7) $cvcl_435) $cvcl_452) $cvcl_445) $cvcl_446) $cvcl_447) $cvcl_448) $cvcl_429) $cvcl_423) $cvcl_449) $cvcl_442) $cvcl_443) ) (and (and (and (and (and (and (and (and (and (= x_21 8) $cvcl_455) $cvcl_461) (or $cvcl_458 $cvcl_457 )) (or $cvcl_459 $cvcl_457 )) (or (and $cvcl_458 $cvcl_459) (and (not (< (* x_20 2) (- (* x_6 2) x_9))) (<= x_20 (+ x_6 (* x_9 6)))) )) (= x_17 (ite $cvcl_460 x_7 (+ x_7 x_9)))) (= x_13 (ite $cvcl_460 x_3 (+ x_3 (* x_9 5))))) (= x_16 (ite $cvcl_460 x_6 x_20))) $cvcl_440) )) $cvcl_461) (= x_10 (ite x_8 0 1))) (not (< x_11 0))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_12 0) $cvcl_463) $cvcl_462) $cvcl_471) $cvcl_472) $cvcl_473) $cvcl_474) $cvcl_475) $cvcl_469) $cvcl_470) $cvcl_467) (and (and (and (and (and (and (and (= x_12 1) $cvcl_463) $cvcl_462) (or (or $cvcl_464 $cvcl_466 ) $cvcl_465 )) (= x_3 (ite $cvcl_464 0 20))) $cvcl_479) $cvcl_467) $cvcl_445) ) (and (and (and (and (and (and (and (= x_12 2) $cvcl_463) $cvcl_462) $cvcl_477) $cvcl_460) $cvcl_469) $cvcl_470) $cvcl_445) ) (and (and (and (and (and (and (and (and (and (and (and (= x_12 3) $cvcl_463) $cvcl_462) $cvcl_471) $cvcl_472) $cvcl_473) $cvcl_480) x_4) $cvcl_450) $cvcl_475) $cvcl_469) $cvcl_470) ) (and (and (and (and (and (and (and (= x_12 4) $cvcl_463) $cvcl_478) $cvcl_477) $cvcl_460) $cvcl_469) $cvcl_470) $cvcl_445) ) (and (and (and (and (and (and (and (= x_12 5) $cvcl_463) $cvcl_478) (or (or $cvcl_468 $cvcl_466 ) $cvcl_465 )) (= x_3 (ite $cvcl_468 40 20))) $cvcl_479) $cvcl_467) $cvcl_445) ) (and (and (and (and (and (and (and (and (and (and (= x_12 6) $cvcl_463) $cvcl_478) $cvcl_471) $cvcl_472) $cvcl_473) $cvcl_480) $cvcl_475) $cvcl_469) $cvcl_470) $cvcl_467) ) (and (and (and (and (and (and (and (and (and (and (and (= x_12 7) $cvcl_463) $cvcl_478) $cvcl_471) $cvcl_472) $cvcl_473) $cvcl_474) $cvcl_456) $cvcl_450) $cvcl_475) $cvcl_469) $cvcl_470) ) (and (and (and (and (and (and (and (and (and (= x_12 8) x_8) (not (< x_2 0))) (or $cvcl_483 $cvcl_482 )) (or $cvcl_484 $cvcl_482 )) (or (and $cvcl_483 $cvcl_484) (and (not (< (* x_11 2) (- (* 10 2) x_2))) (<= x_11 (+ 10 (* x_2 6)))) )) (= x_7 (ite $cvcl_485 2 (+ 2 x_2)))) (= x_3 (ite $cvcl_485 20 (+ 20 (* x_2 5))))) (= x_6 (ite $cvcl_485 10 x_11))) $cvcl_467) )) (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (= x_157 x_160) (= x_148 x_151) ) (= x_139 x_142) ) (= x_130 x_133) ) (= x_121 x_124) ) (= x_112 x_115) ) (= x_103 x_106) ) (= x_94 x_97) ) (= x_85 x_88) ) (= x_76 x_79) ) (= x_67 x_70) ) (= x_58 x_61) ) (= x_49 x_52) ) (= x_40 x_43) ) (= x_31 x_34) ) (= x_22 x_25) ) (= x_13 x_16) ) (= x_3 x_6) ) (= 20 10) )) (or $cvcl_476 $cvcl_481 )) (or $cvcl_450 $cvcl_456 )) (or $cvcl_423 $cvcl_429 )) (or $cvcl_396 $cvcl_402 )) (or $cvcl_369 $cvcl_375 )) (or $cvcl_342 $cvcl_348 )) (or $cvcl_315 $cvcl_321 )) (or $cvcl_288 $cvcl_294 )) (or $cvcl_261 $cvcl_267 )) (or $cvcl_234 $cvcl_240 )) (or $cvcl_207 $cvcl_213 )) (or $cvcl_180 $cvcl_186 )) (or $cvcl_153 $cvcl_159 )) (or $cvcl_126 $cvcl_132 )) (or $cvcl_99 $cvcl_105 )) (or $cvcl_72 $cvcl_78 )) (or $cvcl_45 $cvcl_51 )) (or $cvcl_15 $cvcl_24 )) (or $cvcl_22 $cvcl_21 )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )