diff options
Diffstat (limited to 'test/regress/regress2/arith/pursuit-safety-12.smt')
| -rw-r--r-- | test/regress/regress2/arith/pursuit-safety-12.smt | 130 |
1 files changed, 0 insertions, 130 deletions
diff --git a/test/regress/regress2/arith/pursuit-safety-12.smt b/test/regress/regress2/arith/pursuit-safety-12.smt deleted file mode 100644 index 56ebea066..000000000 --- a/test/regress/regress2/arith/pursuit-safety-12.smt +++ /dev/null @@ -1,130 +0,0 @@ -; COMMAND-LINE: --no-check-proofs -(benchmark pursuit_safety_12.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 unsat -:category { industrial } -:difficulty { 0 } - :logic QF_LRA - - :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)) - :formula -(let (?cvcl_376 20) (let (?cvcl_377 10) (let (?cvcl_385 2) (flet ($cvcl_4 (= x_97 40)) (let (?cvcl_30 (+ x_97 (* x_99 6))) (flet ($cvcl_5 (= x_97 0)) (flet ($cvcl_2 (= x_94 40)) (flet ($cvcl_3 $cvcl_2) (flet ($cvcl_7 (= x_94 0)) (flet ($cvcl_20 $cvcl_7) (flet ($cvcl_14 (< (+ (- (* x_97 5) (* x_94 6)) 40) 0)) (let (?cvcl_33 (+ x_94 (* x_99 5))) (let (?cvcl_31 (+ x_98 x_99)) (flet ($cvcl_11 (= x_98 2)) (flet ($cvcl_8 (= x_103 x_94)) (flet ($cvcl_26 (not x_95)) (flet ($cvcl_43 (and $cvcl_26 x_96)) (flet ($cvcl_32 $cvcl_43) (flet ($cvcl_16 (not x_96)) (flet ($cvcl_19 (and x_95 $cvcl_16)) (flet ($cvcl_6 (and (iff x_104 x_95) (iff x_105 x_96))) (flet ($cvcl_9 (= x_106 x_97)) (flet ($cvcl_1 (and $cvcl_26 $cvcl_16)) (flet ($cvcl_15 (= x_107 0)) (flet ($cvcl_23 (not x_104)) (flet ($cvcl_18 (and $cvcl_23 x_105)) (flet ($cvcl_0 (= x_100 0)) (flet ($cvcl_13 (not $cvcl_2)) (flet ($cvcl_10 (= x_107 x_98)) (flet ($cvcl_29 (or $cvcl_26 x_96 )) (flet ($cvcl_12 (not $cvcl_7)) (flet ($cvcl_28 (or x_95 x_96 )) (flet ($cvcl_22 (not $cvcl_14)) (flet ($cvcl_17 (or $cvcl_20 $cvcl_3 )) (flet ($cvcl_21 (= x_106 (ite $cvcl_4 0 (ite $cvcl_5 40 x_97)))) (flet ($cvcl_27 (and (and (<= ?cvcl_31 2) (not (< ?cvcl_33 0))) (<= ?cvcl_30 40))) (flet ($cvcl_39 (= x_88 40)) (let (?cvcl_64 (+ x_88 (* x_90 6))) (flet ($cvcl_40 (= x_88 0)) (flet ($cvcl_37 (= x_85 40)) (flet ($cvcl_38 $cvcl_37) (flet ($cvcl_42 (= x_85 0)) (flet ($cvcl_56 $cvcl_42) (flet ($cvcl_50 (< (+ (- (* x_88 5) (* x_85 6)) 40) 0)) (let (?cvcl_67 (+ x_85 (* x_90 5))) (let (?cvcl_65 (+ x_89 x_90)) (flet ($cvcl_47 (= x_89 2)) (flet ($cvcl_44 (= x_94 x_85)) (flet ($cvcl_60 (not x_86)) (flet ($cvcl_77 (and $cvcl_60 x_87)) (flet ($cvcl_66 $cvcl_77) (flet ($cvcl_52 (not x_87)) (flet ($cvcl_55 (and x_86 $cvcl_52)) (flet ($cvcl_41 (and (iff x_95 x_86) (iff x_96 x_87))) (flet ($cvcl_45 (= x_97 x_88)) (flet ($cvcl_36 (and $cvcl_60 $cvcl_52)) (flet ($cvcl_51 (= x_98 0)) (flet ($cvcl_54 $cvcl_43) (flet ($cvcl_35 (= x_91 0)) (flet ($cvcl_49 (not $cvcl_37)) (flet ($cvcl_46 (= x_98 x_89)) (flet ($cvcl_63 (or $cvcl_60 x_87 )) (flet ($cvcl_48 (not $cvcl_42)) (flet ($cvcl_62 (or x_86 x_87 )) (flet ($cvcl_58 (not $cvcl_50)) (flet ($cvcl_53 (or $cvcl_56 $cvcl_38 )) (flet ($cvcl_57 (= x_97 (ite $cvcl_39 0 (ite $cvcl_40 40 x_88)))) (flet ($cvcl_61 (and (and (<= ?cvcl_65 2) (not (< ?cvcl_67 0))) (<= ?cvcl_64 40))) (flet ($cvcl_73 (= x_79 40)) (let (?cvcl_98 (+ x_79 (* x_81 6))) (flet ($cvcl_74 (= x_79 0)) (flet ($cvcl_71 (= x_76 40)) (flet ($cvcl_72 $cvcl_71) (flet ($cvcl_76 (= x_76 0)) (flet ($cvcl_90 $cvcl_76) (flet ($cvcl_84 (< (+ (- (* x_79 5) (* x_76 6)) 40) 0)) (let (?cvcl_101 (+ x_76 (* x_81 5))) (let (?cvcl_99 (+ x_80 x_81)) (flet ($cvcl_81 (= x_80 2)) (flet ($cvcl_78 (= x_85 x_76)) (flet ($cvcl_94 (not x_77)) (flet ($cvcl_111 (and $cvcl_94 x_78)) (flet ($cvcl_100 $cvcl_111) (flet ($cvcl_86 (not x_78)) (flet ($cvcl_89 (and x_77 $cvcl_86)) (flet ($cvcl_75 (and (iff x_86 x_77) (iff x_87 x_78))) (flet ($cvcl_79 (= x_88 x_79)) (flet ($cvcl_70 (and $cvcl_94 $cvcl_86)) (flet ($cvcl_85 (= x_89 0)) (flet ($cvcl_88 $cvcl_77) (flet ($cvcl_69 (= x_82 0)) (flet ($cvcl_83 (not $cvcl_71)) (flet ($cvcl_80 (= x_89 x_80)) (flet ($cvcl_97 (or $cvcl_94 x_78 )) (flet ($cvcl_82 (not $cvcl_76)) (flet ($cvcl_96 (or x_77 x_78 )) (flet ($cvcl_92 (not $cvcl_84)) (flet ($cvcl_87 (or $cvcl_90 $cvcl_72 )) (flet ($cvcl_91 (= x_88 (ite $cvcl_73 0 (ite $cvcl_74 40 x_79)))) (flet ($cvcl_95 (and (and (<= ?cvcl_99 2) (not (< ?cvcl_101 0))) (<= ?cvcl_98 40))) (flet ($cvcl_107 (= x_70 40)) (let (?cvcl_132 (+ x_70 (* x_72 6))) (flet ($cvcl_108 (= x_70 0)) (flet ($cvcl_105 (= x_67 40)) (flet ($cvcl_106 $cvcl_105) (flet ($cvcl_110 (= x_67 0)) (flet ($cvcl_124 $cvcl_110) (flet ($cvcl_118 (< (+ (- (* x_70 5) (* x_67 6)) 40) 0)) (let (?cvcl_135 (+ x_67 (* x_72 5))) (let (?cvcl_133 (+ x_71 x_72)) (flet ($cvcl_115 (= x_71 2)) (flet ($cvcl_112 (= x_76 x_67)) (flet ($cvcl_128 (not x_68)) (flet ($cvcl_145 (and $cvcl_128 x_69)) (flet ($cvcl_134 $cvcl_145) (flet ($cvcl_120 (not x_69)) (flet ($cvcl_123 (and x_68 $cvcl_120)) (flet ($cvcl_109 (and (iff x_77 x_68) (iff x_78 x_69))) (flet ($cvcl_113 (= x_79 x_70)) (flet ($cvcl_104 (and $cvcl_128 $cvcl_120)) (flet ($cvcl_119 (= x_80 0)) (flet ($cvcl_122 $cvcl_111) (flet ($cvcl_103 (= x_73 0)) (flet ($cvcl_117 (not $cvcl_105)) (flet ($cvcl_114 (= x_80 x_71)) (flet ($cvcl_131 (or $cvcl_128 x_69 )) (flet ($cvcl_116 (not $cvcl_110)) (flet ($cvcl_130 (or x_68 x_69 )) (flet ($cvcl_126 (not $cvcl_118)) (flet ($cvcl_121 (or $cvcl_124 $cvcl_106 )) (flet ($cvcl_125 (= x_79 (ite $cvcl_107 0 (ite $cvcl_108 40 x_70)))) (flet ($cvcl_129 (and (and (<= ?cvcl_133 2) (not (< ?cvcl_135 0))) (<= ?cvcl_132 40))) (flet ($cvcl_141 (= x_61 40)) (let (?cvcl_166 (+ x_61 (* x_63 6))) (flet ($cvcl_142 (= x_61 0)) (flet ($cvcl_139 (= x_58 40)) (flet ($cvcl_140 $cvcl_139) (flet ($cvcl_144 (= x_58 0)) (flet ($cvcl_158 $cvcl_144) (flet ($cvcl_152 (< (+ (- (* x_61 5) (* x_58 6)) 40) 0)) (let (?cvcl_169 (+ x_58 (* x_63 5))) (let (?cvcl_167 (+ x_62 x_63)) (flet ($cvcl_149 (= x_62 2)) (flet ($cvcl_146 (= x_67 x_58)) (flet ($cvcl_162 (not x_59)) (flet ($cvcl_179 (and $cvcl_162 x_60)) (flet ($cvcl_168 $cvcl_179) (flet ($cvcl_154 (not x_60)) (flet ($cvcl_157 (and x_59 $cvcl_154)) (flet ($cvcl_143 (and (iff x_68 x_59) (iff x_69 x_60))) (flet ($cvcl_147 (= x_70 x_61)) (flet ($cvcl_138 (and $cvcl_162 $cvcl_154)) (flet ($cvcl_153 (= x_71 0)) (flet ($cvcl_156 $cvcl_145) (flet ($cvcl_137 (= x_64 0)) (flet ($cvcl_151 (not $cvcl_139)) (flet ($cvcl_148 (= x_71 x_62)) (flet ($cvcl_165 (or $cvcl_162 x_60 )) (flet ($cvcl_150 (not $cvcl_144)) (flet ($cvcl_164 (or x_59 x_60 )) (flet ($cvcl_160 (not $cvcl_152)) (flet ($cvcl_155 (or $cvcl_158 $cvcl_140 )) (flet ($cvcl_159 (= x_70 (ite $cvcl_141 0 (ite $cvcl_142 40 x_61)))) (flet ($cvcl_163 (and (and (<= ?cvcl_167 2) (not (< ?cvcl_169 0))) (<= ?cvcl_166 40))) (flet ($cvcl_175 (= x_52 40)) (let (?cvcl_200 (+ x_52 (* x_54 6))) (flet ($cvcl_176 (= x_52 0)) (flet ($cvcl_173 (= x_49 40)) (flet ($cvcl_174 $cvcl_173) (flet ($cvcl_178 (= x_49 0)) (flet ($cvcl_192 $cvcl_178) (flet ($cvcl_186 (< (+ (- (* x_52 5) (* x_49 6)) 40) 0)) (let (?cvcl_203 (+ x_49 (* x_54 5))) (let (?cvcl_201 (+ x_53 x_54)) (flet ($cvcl_183 (= x_53 2)) (flet ($cvcl_180 (= x_58 x_49)) (flet ($cvcl_196 (not x_50)) (flet ($cvcl_213 (and $cvcl_196 x_51)) (flet ($cvcl_202 $cvcl_213) (flet ($cvcl_188 (not x_51)) (flet ($cvcl_191 (and x_50 $cvcl_188)) (flet ($cvcl_177 (and (iff x_59 x_50) (iff x_60 x_51))) (flet ($cvcl_181 (= x_61 x_52)) (flet ($cvcl_172 (and $cvcl_196 $cvcl_188)) (flet ($cvcl_187 (= x_62 0)) (flet ($cvcl_190 $cvcl_179) (flet ($cvcl_171 (= x_55 0)) (flet ($cvcl_185 (not $cvcl_173)) (flet ($cvcl_182 (= x_62 x_53)) (flet ($cvcl_199 (or $cvcl_196 x_51 )) (flet ($cvcl_184 (not $cvcl_178)) (flet ($cvcl_198 (or x_50 x_51 )) (flet ($cvcl_194 (not $cvcl_186)) (flet ($cvcl_189 (or $cvcl_192 $cvcl_174 )) (flet ($cvcl_193 (= x_61 (ite $cvcl_175 0 (ite $cvcl_176 40 x_52)))) (flet ($cvcl_197 (and (and (<= ?cvcl_201 2) (not (< ?cvcl_203 0))) (<= ?cvcl_200 40))) (flet ($cvcl_209 (= x_43 40)) (let (?cvcl_234 (+ x_43 (* x_45 6))) (flet ($cvcl_210 (= x_43 0)) (flet ($cvcl_207 (= x_40 40)) (flet ($cvcl_208 $cvcl_207) (flet ($cvcl_212 (= x_40 0)) (flet ($cvcl_226 $cvcl_212) (flet ($cvcl_220 (< (+ (- (* x_43 5) (* x_40 6)) 40) 0)) (let (?cvcl_237 (+ x_40 (* x_45 5))) (let (?cvcl_235 (+ x_44 x_45)) (flet ($cvcl_217 (= x_44 2)) (flet ($cvcl_214 (= x_49 x_40)) (flet ($cvcl_230 (not x_41)) (flet ($cvcl_247 (and $cvcl_230 x_42)) (flet ($cvcl_236 $cvcl_247) (flet ($cvcl_222 (not x_42)) (flet ($cvcl_225 (and x_41 $cvcl_222)) (flet ($cvcl_211 (and (iff x_50 x_41) (iff x_51 x_42))) (flet ($cvcl_215 (= x_52 x_43)) (flet ($cvcl_206 (and $cvcl_230 $cvcl_222)) (flet ($cvcl_221 (= x_53 0)) (flet ($cvcl_224 $cvcl_213) (flet ($cvcl_205 (= x_46 0)) (flet ($cvcl_219 (not $cvcl_207)) (flet ($cvcl_216 (= x_53 x_44)) (flet ($cvcl_233 (or $cvcl_230 x_42 )) (flet ($cvcl_218 (not $cvcl_212)) (flet ($cvcl_232 (or x_41 x_42 )) (flet ($cvcl_228 (not $cvcl_220)) (flet ($cvcl_223 (or $cvcl_226 $cvcl_208 )) (flet ($cvcl_227 (= x_52 (ite $cvcl_209 0 (ite $cvcl_210 40 x_43)))) (flet ($cvcl_231 (and (and (<= ?cvcl_235 2) (not (< ?cvcl_237 0))) (<= ?cvcl_234 40))) (flet ($cvcl_243 (= x_34 40)) (let (?cvcl_268 (+ x_34 (* x_36 6))) (flet ($cvcl_244 (= x_34 0)) (flet ($cvcl_241 (= x_31 40)) (flet ($cvcl_242 $cvcl_241) (flet ($cvcl_246 (= x_31 0)) (flet ($cvcl_260 $cvcl_246) (flet ($cvcl_254 (< (+ (- (* x_34 5) (* x_31 6)) 40) 0)) (let (?cvcl_271 (+ x_31 (* x_36 5))) (let (?cvcl_269 (+ x_35 x_36)) (flet ($cvcl_251 (= x_35 2)) (flet ($cvcl_248 (= x_40 x_31)) (flet ($cvcl_264 (not x_32)) (flet ($cvcl_281 (and $cvcl_264 x_33)) (flet ($cvcl_270 $cvcl_281) (flet ($cvcl_256 (not x_33)) (flet ($cvcl_259 (and x_32 $cvcl_256)) (flet ($cvcl_245 (and (iff x_41 x_32) (iff x_42 x_33))) (flet ($cvcl_249 (= x_43 x_34)) (flet ($cvcl_240 (and $cvcl_264 $cvcl_256)) (flet ($cvcl_255 (= x_44 0)) (flet ($cvcl_258 $cvcl_247) (flet ($cvcl_239 (= x_37 0)) (flet ($cvcl_253 (not $cvcl_241)) (flet ($cvcl_250 (= x_44 x_35)) (flet ($cvcl_267 (or $cvcl_264 x_33 )) (flet ($cvcl_252 (not $cvcl_246)) (flet ($cvcl_266 (or x_32 x_33 )) (flet ($cvcl_262 (not $cvcl_254)) (flet ($cvcl_257 (or $cvcl_260 $cvcl_242 )) (flet ($cvcl_261 (= x_43 (ite $cvcl_243 0 (ite $cvcl_244 40 x_34)))) (flet ($cvcl_265 (and (and (<= ?cvcl_269 2) (not (< ?cvcl_271 0))) (<= ?cvcl_268 40))) (flet ($cvcl_277 (= x_25 40)) (let (?cvcl_302 (+ x_25 (* x_27 6))) (flet ($cvcl_278 (= x_25 0)) (flet ($cvcl_275 (= x_22 40)) (flet ($cvcl_276 $cvcl_275) (flet ($cvcl_280 (= x_22 0)) (flet ($cvcl_294 $cvcl_280) (flet ($cvcl_288 (< (+ (- (* x_25 5) (* x_22 6)) 40) 0)) (let (?cvcl_305 (+ x_22 (* x_27 5))) (let (?cvcl_303 (+ x_26 x_27)) (flet ($cvcl_285 (= x_26 2)) (flet ($cvcl_282 (= x_31 x_22)) (flet ($cvcl_298 (not x_23)) (flet ($cvcl_315 (and $cvcl_298 x_24)) (flet ($cvcl_304 $cvcl_315) (flet ($cvcl_290 (not x_24)) (flet ($cvcl_293 (and x_23 $cvcl_290)) (flet ($cvcl_279 (and (iff x_32 x_23) (iff x_33 x_24))) (flet ($cvcl_283 (= x_34 x_25)) (flet ($cvcl_274 (and $cvcl_298 $cvcl_290)) (flet ($cvcl_289 (= x_35 0)) (flet ($cvcl_292 $cvcl_281) (flet ($cvcl_273 (= x_28 0)) (flet ($cvcl_287 (not $cvcl_275)) (flet ($cvcl_284 (= x_35 x_26)) (flet ($cvcl_301 (or $cvcl_298 x_24 )) (flet ($cvcl_286 (not $cvcl_280)) (flet ($cvcl_300 (or x_23 x_24 )) (flet ($cvcl_296 (not $cvcl_288)) (flet ($cvcl_291 (or $cvcl_294 $cvcl_276 )) (flet ($cvcl_295 (= x_34 (ite $cvcl_277 0 (ite $cvcl_278 40 x_25)))) (flet ($cvcl_299 (and (and (<= ?cvcl_303 2) (not (< ?cvcl_305 0))) (<= ?cvcl_302 40))) (flet ($cvcl_311 (= x_16 40)) (let (?cvcl_336 (+ x_16 (* x_18 6))) (flet ($cvcl_312 (= x_16 0)) (flet ($cvcl_309 (= x_13 40)) (flet ($cvcl_310 $cvcl_309) (flet ($cvcl_314 (= x_13 0)) (flet ($cvcl_328 $cvcl_314) (flet ($cvcl_322 (< (+ (- (* x_16 5) (* x_13 6)) 40) 0)) (let (?cvcl_339 (+ x_13 (* x_18 5))) (let (?cvcl_337 (+ x_17 x_18)) (flet ($cvcl_319 (= x_17 2)) (flet ($cvcl_316 (= x_22 x_13)) (flet ($cvcl_332 (not x_14)) (flet ($cvcl_349 (and $cvcl_332 x_15)) (flet ($cvcl_338 $cvcl_349) (flet ($cvcl_324 (not x_15)) (flet ($cvcl_327 (and x_14 $cvcl_324)) (flet ($cvcl_313 (and (iff x_23 x_14) (iff x_24 x_15))) (flet ($cvcl_317 (= x_25 x_16)) (flet ($cvcl_308 (and $cvcl_332 $cvcl_324)) (flet ($cvcl_323 (= x_26 0)) (flet ($cvcl_326 $cvcl_315) (flet ($cvcl_307 (= x_19 0)) (flet ($cvcl_321 (not $cvcl_309)) (flet ($cvcl_318 (= x_26 x_17)) (flet ($cvcl_335 (or $cvcl_332 x_15 )) (flet ($cvcl_320 (not $cvcl_314)) (flet ($cvcl_334 (or x_14 x_15 )) (flet ($cvcl_330 (not $cvcl_322)) (flet ($cvcl_325 (or $cvcl_328 $cvcl_310 )) (flet ($cvcl_329 (= x_25 (ite $cvcl_311 0 (ite $cvcl_312 40 x_16)))) (flet ($cvcl_333 (and (and (<= ?cvcl_337 2) (not (< ?cvcl_339 0))) (<= ?cvcl_336 40))) (flet ($cvcl_345 (= x_6 40)) (let (?cvcl_370 (+ x_6 (* x_9 6))) (flet ($cvcl_346 (= x_6 0)) (flet ($cvcl_343 (= x_3 40)) (flet ($cvcl_344 $cvcl_343) (flet ($cvcl_348 (= x_3 0)) (flet ($cvcl_362 $cvcl_348) (flet ($cvcl_356 (< (+ (- (* x_6 5) (* x_3 6)) 40) 0)) (let (?cvcl_373 (+ x_3 (* x_9 5))) (let (?cvcl_371 (+ x_7 x_9)) (flet ($cvcl_353 (= x_7 2)) (flet ($cvcl_350 (= x_13 x_3)) (flet ($cvcl_366 (not x_4)) (flet ($cvcl_387 (and $cvcl_366 x_5)) (flet ($cvcl_372 $cvcl_387) (flet ($cvcl_358 (not x_5)) (flet ($cvcl_361 (and x_4 $cvcl_358)) (flet ($cvcl_347 (and (iff x_14 x_4) (iff x_15 x_5))) (flet ($cvcl_351 (= x_16 x_6)) (flet ($cvcl_342 (and $cvcl_366 $cvcl_358)) (flet ($cvcl_357 (= x_17 0)) (flet ($cvcl_360 $cvcl_349) (flet ($cvcl_341 (= x_10 0)) (flet ($cvcl_355 (not $cvcl_343)) (flet ($cvcl_352 (= x_17 x_7)) (flet ($cvcl_369 (or $cvcl_366 x_5 )) (flet ($cvcl_354 (not $cvcl_348)) (flet ($cvcl_368 (or x_4 x_5 )) (flet ($cvcl_364 (not $cvcl_356)) (flet ($cvcl_359 (or $cvcl_362 $cvcl_344 )) (flet ($cvcl_363 (= x_16 (ite $cvcl_345 0 (ite $cvcl_346 40 x_6)))) (flet ($cvcl_367 (and (and (<= ?cvcl_371 2) (not (< ?cvcl_373 0))) (<= ?cvcl_370 40))) (flet ($cvcl_382 (= ?cvcl_377 40)) (let (?cvcl_407 (+ ?cvcl_377 (* x_2 6))) (flet ($cvcl_383 (= ?cvcl_377 0)) (flet ($cvcl_380 (= ?cvcl_376 40)) (flet ($cvcl_381 $cvcl_380) (flet ($cvcl_386 (= ?cvcl_376 0)) (flet ($cvcl_400 $cvcl_386) (flet ($cvcl_394 (< (+ (- (* ?cvcl_377 5) (* ?cvcl_376 6)) 40) 0)) (let (?cvcl_410 (+ ?cvcl_376 (* x_2 5))) (let (?cvcl_408 (+ ?cvcl_385 x_2)) (flet ($cvcl_391 (= ?cvcl_385 2)) (flet ($cvcl_388 (= x_3 ?cvcl_376)) (flet ($cvcl_403 (not x_0)) (flet ($cvcl_409 (and $cvcl_403 x_1)) (flet ($cvcl_396 (not x_1)) (flet ($cvcl_399 (and x_0 $cvcl_396)) (flet ($cvcl_384 (and (iff x_4 x_0) (iff x_5 x_1))) (flet ($cvcl_389 (= x_6 ?cvcl_377)) (flet ($cvcl_375 (and $cvcl_403 $cvcl_396)) (flet ($cvcl_379 $cvcl_375) (flet ($cvcl_395 (= x_7 0)) (flet ($cvcl_398 $cvcl_387) (flet ($cvcl_378 (not x_8)) (flet ($cvcl_393 (not $cvcl_380)) (flet ($cvcl_390 (= x_7 ?cvcl_385)) (flet ($cvcl_406 (or $cvcl_403 x_1 )) (flet ($cvcl_392 (not $cvcl_386)) (flet ($cvcl_405 (or x_0 x_1 )) (flet ($cvcl_402 (not $cvcl_394)) (flet ($cvcl_397 (or $cvcl_400 $cvcl_381 )) (flet ($cvcl_401 (= x_6 (ite $cvcl_382 0 (ite $cvcl_383 40 ?cvcl_377)))) (flet ($cvcl_404 (and (and (<= ?cvcl_408 2) (not (< ?cvcl_410 0))) (<= ?cvcl_407 40))) (flet ($cvcl_25 (= x_100 1)) (flet ($cvcl_24 (not x_105)) (flet ($cvcl_34 (not (< x_99 0))) (flet ($cvcl_59 (= x_91 1)) (flet ($cvcl_68 (not (< x_90 0))) (flet ($cvcl_93 (= x_82 1)) (flet ($cvcl_102 (not (< x_81 0))) (flet ($cvcl_127 (= x_73 1)) (flet ($cvcl_136 (not (< x_72 0))) (flet ($cvcl_161 (= x_64 1)) (flet ($cvcl_170 (not (< x_63 0))) (flet ($cvcl_195 (= x_55 1)) (flet ($cvcl_204 (not (< x_54 0))) (flet ($cvcl_229 (= x_46 1)) (flet ($cvcl_238 (not (< x_45 0))) (flet ($cvcl_263 (= x_37 1)) (flet ($cvcl_272 (not (< x_36 0))) (flet ($cvcl_297 (= x_28 1)) (flet ($cvcl_306 (not (< x_27 0))) (flet ($cvcl_331 (= x_19 1)) (flet ($cvcl_340 (not (< x_18 0))) (flet ($cvcl_365 (= x_10 1)) (flet ($cvcl_374 (not (< x_9 0))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (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_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_375) (not (< x_108 0))) (= x_109 (ite $cvcl_25 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_0) $cvcl_1) $cvcl_11) $cvcl_12) $cvcl_13) $cvcl_14) $cvcl_15) $cvcl_8) $cvcl_9) $cvcl_6) (and (and (and (and (and (and (and (= x_111 1) $cvcl_0) $cvcl_1) (or (or $cvcl_3 $cvcl_5 ) $cvcl_4 )) (= x_103 (ite $cvcl_3 0 x_94))) $cvcl_21) $cvcl_6) $cvcl_10) ) (and (and (and (and (and (and (and (= x_111 2) $cvcl_0) $cvcl_1) $cvcl_17) $cvcl_18) $cvcl_8) $cvcl_9) $cvcl_10) ) (and (and (and (and (and (and (and (and (and (and (and (= x_111 3) $cvcl_0) $cvcl_1) $cvcl_11) $cvcl_12) $cvcl_13) $cvcl_22) x_104) $cvcl_24) $cvcl_15) $cvcl_8) $cvcl_9) ) (and (and (and (and (and (and (and (= x_111 4) $cvcl_0) $cvcl_19) $cvcl_17) $cvcl_18) $cvcl_8) $cvcl_9) $cvcl_10) ) (and (and (and (and (and (and (and (= x_111 5) $cvcl_0) $cvcl_19) (or (or $cvcl_20 $cvcl_5 ) $cvcl_4 )) (= x_103 (ite $cvcl_20 40 x_94))) $cvcl_21) $cvcl_6) $cvcl_10) ) (and (and (and (and (and (and (and (and (and (and (= x_111 6) $cvcl_0) $cvcl_19) $cvcl_11) $cvcl_12) $cvcl_13) $cvcl_22) $cvcl_15) $cvcl_8) $cvcl_9) $cvcl_6) ) (and (and (and (and (and (and (and (and (and (and (and (= x_111 7) $cvcl_0) $cvcl_19) $cvcl_11) $cvcl_12) $cvcl_13) $cvcl_14) $cvcl_23) $cvcl_24) $cvcl_15) $cvcl_8) $cvcl_9) ) (and (and (and (and (and (and (and (and (and (= x_111 8) $cvcl_25) $cvcl_34) (or $cvcl_28 $cvcl_27 )) (or $cvcl_29 $cvcl_27 )) (or (and $cvcl_28 $cvcl_29) (and (not (< (* x_110 2) (- (* x_97 2) x_99))) (<= x_110 ?cvcl_30)) )) (= x_107 (ite $cvcl_32 x_98 ?cvcl_31))) (= x_103 (ite $cvcl_32 x_94 ?cvcl_33))) (= x_106 (ite $cvcl_32 x_97 x_110))) $cvcl_6) )) $cvcl_34) (= x_100 (ite $cvcl_59 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_35) $cvcl_36) $cvcl_47) $cvcl_48) $cvcl_49) $cvcl_50) $cvcl_51) $cvcl_44) $cvcl_45) $cvcl_41) (and (and (and (and (and (and (and (= x_102 1) $cvcl_35) $cvcl_36) (or (or $cvcl_38 $cvcl_40 ) $cvcl_39 )) (= x_94 (ite $cvcl_38 0 x_85))) $cvcl_57) $cvcl_41) $cvcl_46) ) (and (and (and (and (and (and (and (= x_102 2) $cvcl_35) $cvcl_36) $cvcl_53) $cvcl_54) $cvcl_44) $cvcl_45) $cvcl_46) ) (and (and (and (and (and (and (and (and (and (and (and (= x_102 3) $cvcl_35) $cvcl_36) $cvcl_47) $cvcl_48) $cvcl_49) $cvcl_58) x_95) $cvcl_16) $cvcl_51) $cvcl_44) $cvcl_45) ) (and (and (and (and (and (and (and (= x_102 4) $cvcl_35) $cvcl_55) $cvcl_53) $cvcl_54) $cvcl_44) $cvcl_45) $cvcl_46) ) (and (and (and (and (and (and (and (= x_102 5) $cvcl_35) $cvcl_55) (or (or $cvcl_56 $cvcl_40 ) $cvcl_39 )) (= x_94 (ite $cvcl_56 40 x_85))) $cvcl_57) $cvcl_41) $cvcl_46) ) (and (and (and (and (and (and (and (and (and (and (= x_102 6) $cvcl_35) $cvcl_55) $cvcl_47) $cvcl_48) $cvcl_49) $cvcl_58) $cvcl_51) $cvcl_44) $cvcl_45) $cvcl_41) ) (and (and (and (and (and (and (and (and (and (and (and (= x_102 7) $cvcl_35) $cvcl_55) $cvcl_47) $cvcl_48) $cvcl_49) $cvcl_50) $cvcl_26) $cvcl_16) $cvcl_51) $cvcl_44) $cvcl_45) ) (and (and (and (and (and (and (and (and (and (= x_102 8) $cvcl_59) $cvcl_68) (or $cvcl_62 $cvcl_61 )) (or $cvcl_63 $cvcl_61 )) (or (and $cvcl_62 $cvcl_63) (and (not (< (* x_101 2) (- (* x_88 2) x_90))) (<= x_101 ?cvcl_64)) )) (= x_98 (ite $cvcl_66 x_89 ?cvcl_65))) (= x_94 (ite $cvcl_66 x_85 ?cvcl_67))) (= x_97 (ite $cvcl_66 x_88 x_101))) $cvcl_41) )) $cvcl_68) (= x_91 (ite $cvcl_93 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_69) $cvcl_70) $cvcl_81) $cvcl_82) $cvcl_83) $cvcl_84) $cvcl_85) $cvcl_78) $cvcl_79) $cvcl_75) (and (and (and (and (and (and (and (= x_93 1) $cvcl_69) $cvcl_70) (or (or $cvcl_72 $cvcl_74 ) $cvcl_73 )) (= x_85 (ite $cvcl_72 0 x_76))) $cvcl_91) $cvcl_75) $cvcl_80) ) (and (and (and (and (and (and (and (= x_93 2) $cvcl_69) $cvcl_70) $cvcl_87) $cvcl_88) $cvcl_78) $cvcl_79) $cvcl_80) ) (and (and (and (and (and (and (and (and (and (and (and (= x_93 3) $cvcl_69) $cvcl_70) $cvcl_81) $cvcl_82) $cvcl_83) $cvcl_92) x_86) $cvcl_52) $cvcl_85) $cvcl_78) $cvcl_79) ) (and (and (and (and (and (and (and (= x_93 4) $cvcl_69) $cvcl_89) $cvcl_87) $cvcl_88) $cvcl_78) $cvcl_79) $cvcl_80) ) (and (and (and (and (and (and (and (= x_93 5) $cvcl_69) $cvcl_89) (or (or $cvcl_90 $cvcl_74 ) $cvcl_73 )) (= x_85 (ite $cvcl_90 40 x_76))) $cvcl_91) $cvcl_75) $cvcl_80) ) (and (and (and (and (and (and (and (and (and (and (= x_93 6) $cvcl_69) $cvcl_89) $cvcl_81) $cvcl_82) $cvcl_83) $cvcl_92) $cvcl_85) $cvcl_78) $cvcl_79) $cvcl_75) ) (and (and (and (and (and (and (and (and (and (and (and (= x_93 7) $cvcl_69) $cvcl_89) $cvcl_81) $cvcl_82) $cvcl_83) $cvcl_84) $cvcl_60) $cvcl_52) $cvcl_85) $cvcl_78) $cvcl_79) ) (and (and (and (and (and (and (and (and (and (= x_93 8) $cvcl_93) $cvcl_102) (or $cvcl_96 $cvcl_95 )) (or $cvcl_97 $cvcl_95 )) (or (and $cvcl_96 $cvcl_97) (and (not (< (* x_92 2) (- (* x_79 2) x_81))) (<= x_92 ?cvcl_98)) )) (= x_89 (ite $cvcl_100 x_80 ?cvcl_99))) (= x_85 (ite $cvcl_100 x_76 ?cvcl_101))) (= x_88 (ite $cvcl_100 x_79 x_92))) $cvcl_75) )) $cvcl_102) (= x_82 (ite $cvcl_127 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_103) $cvcl_104) $cvcl_115) $cvcl_116) $cvcl_117) $cvcl_118) $cvcl_119) $cvcl_112) $cvcl_113) $cvcl_109) (and (and (and (and (and (and (and (= x_84 1) $cvcl_103) $cvcl_104) (or (or $cvcl_106 $cvcl_108 ) $cvcl_107 )) (= x_76 (ite $cvcl_106 0 x_67))) $cvcl_125) $cvcl_109) $cvcl_114) ) (and (and (and (and (and (and (and (= x_84 2) $cvcl_103) $cvcl_104) $cvcl_121) $cvcl_122) $cvcl_112) $cvcl_113) $cvcl_114) ) (and (and (and (and (and (and (and (and (and (and (and (= x_84 3) $cvcl_103) $cvcl_104) $cvcl_115) $cvcl_116) $cvcl_117) $cvcl_126) x_77) $cvcl_86) $cvcl_119) $cvcl_112) $cvcl_113) ) (and (and (and (and (and (and (and (= x_84 4) $cvcl_103) $cvcl_123) $cvcl_121) $cvcl_122) $cvcl_112) $cvcl_113) $cvcl_114) ) (and (and (and (and (and (and (and (= x_84 5) $cvcl_103) $cvcl_123) (or (or $cvcl_124 $cvcl_108 ) $cvcl_107 )) (= x_76 (ite $cvcl_124 40 x_67))) $cvcl_125) $cvcl_109) $cvcl_114) ) (and (and (and (and (and (and (and (and (and (and (= x_84 6) $cvcl_103) $cvcl_123) $cvcl_115) $cvcl_116) $cvcl_117) $cvcl_126) $cvcl_119) $cvcl_112) $cvcl_113) $cvcl_109) ) (and (and (and (and (and (and (and (and (and (and (and (= x_84 7) $cvcl_103) $cvcl_123) $cvcl_115) $cvcl_116) $cvcl_117) $cvcl_118) $cvcl_94) $cvcl_86) $cvcl_119) $cvcl_112) $cvcl_113) ) (and (and (and (and (and (and (and (and (and (= x_84 8) $cvcl_127) $cvcl_136) (or $cvcl_130 $cvcl_129 )) (or $cvcl_131 $cvcl_129 )) (or (and $cvcl_130 $cvcl_131) (and (not (< (* x_83 2) (- (* x_70 2) x_72))) (<= x_83 ?cvcl_132)) )) (= x_80 (ite $cvcl_134 x_71 ?cvcl_133))) (= x_76 (ite $cvcl_134 x_67 ?cvcl_135))) (= x_79 (ite $cvcl_134 x_70 x_83))) $cvcl_109) )) $cvcl_136) (= x_73 (ite $cvcl_161 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_137) $cvcl_138) $cvcl_149) $cvcl_150) $cvcl_151) $cvcl_152) $cvcl_153) $cvcl_146) $cvcl_147) $cvcl_143) (and (and (and (and (and (and (and (= x_75 1) $cvcl_137) $cvcl_138) (or (or $cvcl_140 $cvcl_142 ) $cvcl_141 )) (= x_67 (ite $cvcl_140 0 x_58))) $cvcl_159) $cvcl_143) $cvcl_148) ) (and (and (and (and (and (and (and (= x_75 2) $cvcl_137) $cvcl_138) $cvcl_155) $cvcl_156) $cvcl_146) $cvcl_147) $cvcl_148) ) (and (and (and (and (and (and (and (and (and (and (and (= x_75 3) $cvcl_137) $cvcl_138) $cvcl_149) $cvcl_150) $cvcl_151) $cvcl_160) x_68) $cvcl_120) $cvcl_153) $cvcl_146) $cvcl_147) ) (and (and (and (and (and (and (and (= x_75 4) $cvcl_137) $cvcl_157) $cvcl_155) $cvcl_156) $cvcl_146) $cvcl_147) $cvcl_148) ) (and (and (and (and (and (and (and (= x_75 5) $cvcl_137) $cvcl_157) (or (or $cvcl_158 $cvcl_142 ) $cvcl_141 )) (= x_67 (ite $cvcl_158 40 x_58))) $cvcl_159) $cvcl_143) $cvcl_148) ) (and (and (and (and (and (and (and (and (and (and (= x_75 6) $cvcl_137) $cvcl_157) $cvcl_149) $cvcl_150) $cvcl_151) $cvcl_160) $cvcl_153) $cvcl_146) $cvcl_147) $cvcl_143) ) (and (and (and (and (and (and (and (and (and (and (and (= x_75 7) $cvcl_137) $cvcl_157) $cvcl_149) $cvcl_150) $cvcl_151) $cvcl_152) $cvcl_128) $cvcl_120) $cvcl_153) $cvcl_146) $cvcl_147) ) (and (and (and (and (and (and (and (and (and (= x_75 8) $cvcl_161) $cvcl_170) (or $cvcl_164 $cvcl_163 )) (or $cvcl_165 $cvcl_163 )) (or (and $cvcl_164 $cvcl_165) (and (not (< (* x_74 2) (- (* x_61 2) x_63))) (<= x_74 ?cvcl_166)) )) (= x_71 (ite $cvcl_168 x_62 ?cvcl_167))) (= x_67 (ite $cvcl_168 x_58 ?cvcl_169))) (= x_70 (ite $cvcl_168 x_61 x_74))) $cvcl_143) )) $cvcl_170) (= x_64 (ite $cvcl_195 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_171) $cvcl_172) $cvcl_183) $cvcl_184) $cvcl_185) $cvcl_186) $cvcl_187) $cvcl_180) $cvcl_181) $cvcl_177) (and (and (and (and (and (and (and (= x_66 1) $cvcl_171) $cvcl_172) (or (or $cvcl_174 $cvcl_176 ) $cvcl_175 )) (= x_58 (ite $cvcl_174 0 x_49))) $cvcl_193) $cvcl_177) $cvcl_182) ) (and (and (and (and (and (and (and (= x_66 2) $cvcl_171) $cvcl_172) $cvcl_189) $cvcl_190) $cvcl_180) $cvcl_181) $cvcl_182) ) (and (and (and (and (and (and (and (and (and (and (and (= x_66 3) $cvcl_171) $cvcl_172) $cvcl_183) $cvcl_184) $cvcl_185) $cvcl_194) x_59) $cvcl_154) $cvcl_187) $cvcl_180) $cvcl_181) ) (and (and (and (and (and (and (and (= x_66 4) $cvcl_171) $cvcl_191) $cvcl_189) $cvcl_190) $cvcl_180) $cvcl_181) $cvcl_182) ) (and (and (and (and (and (and (and (= x_66 5) $cvcl_171) $cvcl_191) (or (or $cvcl_192 $cvcl_176 ) $cvcl_175 )) (= x_58 (ite $cvcl_192 40 x_49))) $cvcl_193) $cvcl_177) $cvcl_182) ) (and (and (and (and (and (and (and (and (and (and (= x_66 6) $cvcl_171) $cvcl_191) $cvcl_183) $cvcl_184) $cvcl_185) $cvcl_194) $cvcl_187) $cvcl_180) $cvcl_181) $cvcl_177) ) (and (and (and (and (and (and (and (and (and (and (and (= x_66 7) $cvcl_171) $cvcl_191) $cvcl_183) $cvcl_184) $cvcl_185) $cvcl_186) $cvcl_162) $cvcl_154) $cvcl_187) $cvcl_180) $cvcl_181) ) (and (and (and (and (and (and (and (and (and (= x_66 8) $cvcl_195) $cvcl_204) (or $cvcl_198 $cvcl_197 )) (or $cvcl_199 $cvcl_197 )) (or (and $cvcl_198 $cvcl_199) (and (not (< (* x_65 2) (- (* x_52 2) x_54))) (<= x_65 ?cvcl_200)) )) (= x_62 (ite $cvcl_202 x_53 ?cvcl_201))) (= x_58 (ite $cvcl_202 x_49 ?cvcl_203))) (= x_61 (ite $cvcl_202 x_52 x_65))) $cvcl_177) )) $cvcl_204) (= x_55 (ite $cvcl_229 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_205) $cvcl_206) $cvcl_217) $cvcl_218) $cvcl_219) $cvcl_220) $cvcl_221) $cvcl_214) $cvcl_215) $cvcl_211) (and (and (and (and (and (and (and (= x_57 1) $cvcl_205) $cvcl_206) (or (or $cvcl_208 $cvcl_210 ) $cvcl_209 )) (= x_49 (ite $cvcl_208 0 x_40))) $cvcl_227) $cvcl_211) $cvcl_216) ) (and (and (and (and (and (and (and (= x_57 2) $cvcl_205) $cvcl_206) $cvcl_223) $cvcl_224) $cvcl_214) $cvcl_215) $cvcl_216) ) (and (and (and (and (and (and (and (and (and (and (and (= x_57 3) $cvcl_205) $cvcl_206) $cvcl_217) $cvcl_218) $cvcl_219) $cvcl_228) x_50) $cvcl_188) $cvcl_221) $cvcl_214) $cvcl_215) ) (and (and (and (and (and (and (and (= x_57 4) $cvcl_205) $cvcl_225) $cvcl_223) $cvcl_224) $cvcl_214) $cvcl_215) $cvcl_216) ) (and (and (and (and (and (and (and (= x_57 5) $cvcl_205) $cvcl_225) (or (or $cvcl_226 $cvcl_210 ) $cvcl_209 )) (= x_49 (ite $cvcl_226 40 x_40))) $cvcl_227) $cvcl_211) $cvcl_216) ) (and (and (and (and (and (and (and (and (and (and (= x_57 6) $cvcl_205) $cvcl_225) $cvcl_217) $cvcl_218) $cvcl_219) $cvcl_228) $cvcl_221) $cvcl_214) $cvcl_215) $cvcl_211) ) (and (and (and (and (and (and (and (and (and (and (and (= x_57 7) $cvcl_205) $cvcl_225) $cvcl_217) $cvcl_218) $cvcl_219) $cvcl_220) $cvcl_196) $cvcl_188) $cvcl_221) $cvcl_214) $cvcl_215) ) (and (and (and (and (and (and (and (and (and (= x_57 8) $cvcl_229) $cvcl_238) (or $cvcl_232 $cvcl_231 )) (or $cvcl_233 $cvcl_231 )) (or (and $cvcl_232 $cvcl_233) (and (not (< (* x_56 2) (- (* x_43 2) x_45))) (<= x_56 ?cvcl_234)) )) (= x_53 (ite $cvcl_236 x_44 ?cvcl_235))) (= x_49 (ite $cvcl_236 x_40 ?cvcl_237))) (= x_52 (ite $cvcl_236 x_43 x_56))) $cvcl_211) )) $cvcl_238) (= x_46 (ite $cvcl_263 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_239) $cvcl_240) $cvcl_251) $cvcl_252) $cvcl_253) $cvcl_254) $cvcl_255) $cvcl_248) $cvcl_249) $cvcl_245) (and (and (and (and (and (and (and (= x_48 1) $cvcl_239) $cvcl_240) (or (or $cvcl_242 $cvcl_244 ) $cvcl_243 )) (= x_40 (ite $cvcl_242 0 x_31))) $cvcl_261) $cvcl_245) $cvcl_250) ) (and (and (and (and (and (and (and (= x_48 2) $cvcl_239) $cvcl_240) $cvcl_257) $cvcl_258) $cvcl_248) $cvcl_249) $cvcl_250) ) (and (and (and (and (and (and (and (and (and (and (and (= x_48 3) $cvcl_239) $cvcl_240) $cvcl_251) $cvcl_252) $cvcl_253) $cvcl_262) x_41) $cvcl_222) $cvcl_255) $cvcl_248) $cvcl_249) ) (and (and (and (and (and (and (and (= x_48 4) $cvcl_239) $cvcl_259) $cvcl_257) $cvcl_258) $cvcl_248) $cvcl_249) $cvcl_250) ) (and (and (and (and (and (and (and (= x_48 5) $cvcl_239) $cvcl_259) (or (or $cvcl_260 $cvcl_244 ) $cvcl_243 )) (= x_40 (ite $cvcl_260 40 x_31))) $cvcl_261) $cvcl_245) $cvcl_250) ) (and (and (and (and (and (and (and (and (and (and (= x_48 6) $cvcl_239) $cvcl_259) $cvcl_251) $cvcl_252) $cvcl_253) $cvcl_262) $cvcl_255) $cvcl_248) $cvcl_249) $cvcl_245) ) (and (and (and (and (and (and (and (and (and (and (and (= x_48 7) $cvcl_239) $cvcl_259) $cvcl_251) $cvcl_252) $cvcl_253) $cvcl_254) $cvcl_230) $cvcl_222) $cvcl_255) $cvcl_248) $cvcl_249) ) (and (and (and (and (and (and (and (and (and (= x_48 8) $cvcl_263) $cvcl_272) (or $cvcl_266 $cvcl_265 )) (or $cvcl_267 $cvcl_265 )) (or (and $cvcl_266 $cvcl_267) (and (not (< (* x_47 2) (- (* x_34 2) x_36))) (<= x_47 ?cvcl_268)) )) (= x_44 (ite $cvcl_270 x_35 ?cvcl_269))) (= x_40 (ite $cvcl_270 x_31 ?cvcl_271))) (= x_43 (ite $cvcl_270 x_34 x_47))) $cvcl_245) )) $cvcl_272) (= x_37 (ite $cvcl_297 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_273) $cvcl_274) $cvcl_285) $cvcl_286) $cvcl_287) $cvcl_288) $cvcl_289) $cvcl_282) $cvcl_283) $cvcl_279) (and (and (and (and (and (and (and (= x_39 1) $cvcl_273) $cvcl_274) (or (or $cvcl_276 $cvcl_278 ) $cvcl_277 )) (= x_31 (ite $cvcl_276 0 x_22))) $cvcl_295) $cvcl_279) $cvcl_284) ) (and (and (and (and (and (and (and (= x_39 2) $cvcl_273) $cvcl_274) $cvcl_291) $cvcl_292) $cvcl_282) $cvcl_283) $cvcl_284) ) (and (and (and (and (and (and (and (and (and (and (and (= x_39 3) $cvcl_273) $cvcl_274) $cvcl_285) $cvcl_286) $cvcl_287) $cvcl_296) x_32) $cvcl_256) $cvcl_289) $cvcl_282) $cvcl_283) ) (and (and (and (and (and (and (and (= x_39 4) $cvcl_273) $cvcl_293) $cvcl_291) $cvcl_292) $cvcl_282) $cvcl_283) $cvcl_284) ) (and (and (and (and (and (and (and (= x_39 5) $cvcl_273) $cvcl_293) (or (or $cvcl_294 $cvcl_278 ) $cvcl_277 )) (= x_31 (ite $cvcl_294 40 x_22))) $cvcl_295) $cvcl_279) $cvcl_284) ) (and (and (and (and (and (and (and (and (and (and (= x_39 6) $cvcl_273) $cvcl_293) $cvcl_285) $cvcl_286) $cvcl_287) $cvcl_296) $cvcl_289) $cvcl_282) $cvcl_283) $cvcl_279) ) (and (and (and (and (and (and (and (and (and (and (and (= x_39 7) $cvcl_273) $cvcl_293) $cvcl_285) $cvcl_286) $cvcl_287) $cvcl_288) $cvcl_264) $cvcl_256) $cvcl_289) $cvcl_282) $cvcl_283) ) (and (and (and (and (and (and (and (and (and (= x_39 8) $cvcl_297) $cvcl_306) (or $cvcl_300 $cvcl_299 )) (or $cvcl_301 $cvcl_299 )) (or (and $cvcl_300 $cvcl_301) (and (not (< (* x_38 2) (- (* x_25 2) x_27))) (<= x_38 ?cvcl_302)) )) (= x_35 (ite $cvcl_304 x_26 ?cvcl_303))) (= x_31 (ite $cvcl_304 x_22 ?cvcl_305))) (= x_34 (ite $cvcl_304 x_25 x_38))) $cvcl_279) )) $cvcl_306) (= x_28 (ite $cvcl_331 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_307) $cvcl_308) $cvcl_319) $cvcl_320) $cvcl_321) $cvcl_322) $cvcl_323) $cvcl_316) $cvcl_317) $cvcl_313) (and (and (and (and (and (and (and (= x_30 1) $cvcl_307) $cvcl_308) (or (or $cvcl_310 $cvcl_312 ) $cvcl_311 )) (= x_22 (ite $cvcl_310 0 x_13))) $cvcl_329) $cvcl_313) $cvcl_318) ) (and (and (and (and (and (and (and (= x_30 2) $cvcl_307) $cvcl_308) $cvcl_325) $cvcl_326) $cvcl_316) $cvcl_317) $cvcl_318) ) (and (and (and (and (and (and (and (and (and (and (and (= x_30 3) $cvcl_307) $cvcl_308) $cvcl_319) $cvcl_320) $cvcl_321) $cvcl_330) x_23) $cvcl_290) $cvcl_323) $cvcl_316) $cvcl_317) ) (and (and (and (and (and (and (and (= x_30 4) $cvcl_307) $cvcl_327) $cvcl_325) $cvcl_326) $cvcl_316) $cvcl_317) $cvcl_318) ) (and (and (and (and (and (and (and (= x_30 5) $cvcl_307) $cvcl_327) (or (or $cvcl_328 $cvcl_312 ) $cvcl_311 )) (= x_22 (ite $cvcl_328 40 x_13))) $cvcl_329) $cvcl_313) $cvcl_318) ) (and (and (and (and (and (and (and (and (and (and (= x_30 6) $cvcl_307) $cvcl_327) $cvcl_319) $cvcl_320) $cvcl_321) $cvcl_330) $cvcl_323) $cvcl_316) $cvcl_317) $cvcl_313) ) (and (and (and (and (and (and (and (and (and (and (and (= x_30 7) $cvcl_307) $cvcl_327) $cvcl_319) $cvcl_320) $cvcl_321) $cvcl_322) $cvcl_298) $cvcl_290) $cvcl_323) $cvcl_316) $cvcl_317) ) (and (and (and (and (and (and (and (and (and (= x_30 8) $cvcl_331) $cvcl_340) (or $cvcl_334 $cvcl_333 )) (or $cvcl_335 $cvcl_333 )) (or (and $cvcl_334 $cvcl_335) (and (not (< (* x_29 2) (- (* x_16 2) x_18))) (<= x_29 ?cvcl_336)) )) (= x_26 (ite $cvcl_338 x_17 ?cvcl_337))) (= x_22 (ite $cvcl_338 x_13 ?cvcl_339))) (= x_25 (ite $cvcl_338 x_16 x_29))) $cvcl_313) )) $cvcl_340) (= x_19 (ite $cvcl_365 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_341) $cvcl_342) $cvcl_353) $cvcl_354) $cvcl_355) $cvcl_356) $cvcl_357) $cvcl_350) $cvcl_351) $cvcl_347) (and (and (and (and (and (and (and (= x_21 1) $cvcl_341) $cvcl_342) (or (or $cvcl_344 $cvcl_346 ) $cvcl_345 )) (= x_13 (ite $cvcl_344 0 x_3))) $cvcl_363) $cvcl_347) $cvcl_352) ) (and (and (and (and (and (and (and (= x_21 2) $cvcl_341) $cvcl_342) $cvcl_359) $cvcl_360) $cvcl_350) $cvcl_351) $cvcl_352) ) (and (and (and (and (and (and (and (and (and (and (and (= x_21 3) $cvcl_341) $cvcl_342) $cvcl_353) $cvcl_354) $cvcl_355) $cvcl_364) x_14) $cvcl_324) $cvcl_357) $cvcl_350) $cvcl_351) ) (and (and (and (and (and (and (and (= x_21 4) $cvcl_341) $cvcl_361) $cvcl_359) $cvcl_360) $cvcl_350) $cvcl_351) $cvcl_352) ) (and (and (and (and (and (and (and (= x_21 5) $cvcl_341) $cvcl_361) (or (or $cvcl_362 $cvcl_346 ) $cvcl_345 )) (= x_13 (ite $cvcl_362 40 x_3))) $cvcl_363) $cvcl_347) $cvcl_352) ) (and (and (and (and (and (and (and (and (and (and (= x_21 6) $cvcl_341) $cvcl_361) $cvcl_353) $cvcl_354) $cvcl_355) $cvcl_364) $cvcl_357) $cvcl_350) $cvcl_351) $cvcl_347) ) (and (and (and (and (and (and (and (and (and (and (and (= x_21 7) $cvcl_341) $cvcl_361) $cvcl_353) $cvcl_354) $cvcl_355) $cvcl_356) $cvcl_332) $cvcl_324) $cvcl_357) $cvcl_350) $cvcl_351) ) (and (and (and (and (and (and (and (and (and (= x_21 8) $cvcl_365) $cvcl_374) (or $cvcl_368 $cvcl_367 )) (or $cvcl_369 $cvcl_367 )) (or (and $cvcl_368 $cvcl_369) (and (not (< (* x_20 2) (- (* x_6 2) x_9))) (<= x_20 ?cvcl_370)) )) (= x_17 (ite $cvcl_372 x_7 ?cvcl_371))) (= x_13 (ite $cvcl_372 x_3 ?cvcl_373))) (= x_16 (ite $cvcl_372 x_6 x_20))) $cvcl_347) )) $cvcl_374) (= 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_378) $cvcl_379) $cvcl_391) $cvcl_392) $cvcl_393) $cvcl_394) $cvcl_395) $cvcl_388) $cvcl_389) $cvcl_384) (and (and (and (and (and (and (and (= x_12 1) $cvcl_378) $cvcl_379) (or (or $cvcl_381 $cvcl_383 ) $cvcl_382 )) (= x_3 (ite $cvcl_381 0 ?cvcl_376))) $cvcl_401) $cvcl_384) $cvcl_390) ) (and (and (and (and (and (and (and (= x_12 2) $cvcl_378) $cvcl_379) $cvcl_397) $cvcl_398) $cvcl_388) $cvcl_389) $cvcl_390) ) (and (and (and (and (and (and (and (and (and (and (and (= x_12 3) $cvcl_378) $cvcl_379) $cvcl_391) $cvcl_392) $cvcl_393) $cvcl_402) x_4) $cvcl_358) $cvcl_395) $cvcl_388) $cvcl_389) ) (and (and (and (and (and (and (and (= x_12 4) $cvcl_378) $cvcl_399) $cvcl_397) $cvcl_398) $cvcl_388) $cvcl_389) $cvcl_390) ) (and (and (and (and (and (and (and (= x_12 5) $cvcl_378) $cvcl_399) (or (or $cvcl_400 $cvcl_383 ) $cvcl_382 )) (= x_3 (ite $cvcl_400 40 ?cvcl_376))) $cvcl_401) $cvcl_384) $cvcl_390) ) (and (and (and (and (and (and (and (and (and (and (= x_12 6) $cvcl_378) $cvcl_399) $cvcl_391) $cvcl_392) $cvcl_393) $cvcl_402) $cvcl_395) $cvcl_388) $cvcl_389) $cvcl_384) ) (and (and (and (and (and (and (and (and (and (and (and (= x_12 7) $cvcl_378) $cvcl_399) $cvcl_391) $cvcl_392) $cvcl_393) $cvcl_394) $cvcl_366) $cvcl_358) $cvcl_395) $cvcl_388) $cvcl_389) ) (and (and (and (and (and (and (and (and (and (= x_12 8) x_8) (not (< x_2 0))) (or $cvcl_405 $cvcl_404 )) (or $cvcl_406 $cvcl_404 )) (or (and $cvcl_405 $cvcl_406) (and (not (< (* x_11 2) (- (* ?cvcl_377 2) x_2))) (<= x_11 ?cvcl_407)) )) (= x_7 (ite $cvcl_409 ?cvcl_385 ?cvcl_408))) (= x_3 (ite $cvcl_409 ?cvcl_376 ?cvcl_410))) (= x_6 (ite $cvcl_409 ?cvcl_377 x_11))) $cvcl_384) )) (or (or (or (or (or (or (or (or (or (or (or (or (= 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) ) (= ?cvcl_376 ?cvcl_377) )) (or $cvcl_396 $cvcl_403 )) (or $cvcl_358 $cvcl_366 )) (or $cvcl_324 $cvcl_332 )) (or $cvcl_290 $cvcl_298 )) (or $cvcl_256 $cvcl_264 )) (or $cvcl_222 $cvcl_230 )) (or $cvcl_188 $cvcl_196 )) (or $cvcl_154 $cvcl_162 )) (or $cvcl_120 $cvcl_128 )) (or $cvcl_86 $cvcl_94 )) (or $cvcl_52 $cvcl_60 )) (or $cvcl_16 $cvcl_26 )) (or $cvcl_24 $cvcl_23 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -) |