(benchmark op_seen_less2.induction.smt :source { The Formal Verification of a Reintegration Protocol. Author: Lee Pike. Website: http://www.cs.indiana.edu/~lepike/pub_pages/emsoft.html. This benchmark was automatically translated into SMT-LIB format from CVC format using CVC Lite } :status unsat :category { industrial } :difficulty { 0 } :logic QF_LRA :extrafuns ((x_0 Real)) :extrafuns ((x_1 Real)) :extrafuns ((x_2 Real)) :extrafuns ((x_3 Real)) :extrafuns ((x_4 Real)) :extrafuns ((x_5 Real)) :extrafuns ((x_6 Real)) :extrafuns ((x_7 Real)) :extrafuns ((x_8 Real)) :extrafuns ((x_9 Real)) :extrafuns ((x_10 Real)) :extrapreds ((x_11)) :extrapreds ((x_12)) :extrapreds ((x_13)) :extrafuns ((x_14 Real)) :extrafuns ((x_15 Real)) :extrapreds ((x_16)) :extrapreds ((x_17)) :extrapreds ((x_18)) :extrafuns ((x_19 Real)) :extrafuns ((x_20 Real)) :extrapreds ((x_21)) :extrapreds ((x_22)) :extrapreds ((x_23)) :extrafuns ((x_24 Real)) :extrafuns ((x_25 Real)) :extrapreds ((x_26)) :extrapreds ((x_27)) :extrapreds ((x_28)) :extrafuns ((x_29 Real)) :extrafuns ((x_30 Real)) :extrapreds ((x_31)) :extrapreds ((x_32)) :extrapreds ((x_33)) :extrafuns ((x_34 Real)) :extrafuns ((x_35 Real)) :extrafuns ((x_36 Real)) :extrafuns ((x_37 Real)) :extrapreds ((x_38)) :extrapreds ((x_39)) :extrapreds ((x_40)) :extrapreds ((x_41)) :extrapreds ((x_42)) :extrapreds ((x_43)) :extrapreds ((x_44)) :extrapreds ((x_45)) :extrapreds ((x_46)) :extrapreds ((x_47)) :extrapreds ((x_48)) :extrapreds ((x_49)) :extrafuns ((x_50 Real)) :extrafuns ((x_51 Real)) :extrapreds ((x_52)) :extrapreds ((x_53)) :extrapreds ((x_54)) :extrapreds ((x_55)) :extrapreds ((x_56)) :extrapreds ((x_57)) :extrafuns ((x_58 Real)) :extrafuns ((x_59 Real)) :extrafuns ((x_60 Real)) :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)) :extrafuns ((x_68 Real)) :extrafuns ((x_69 Real)) :extrafuns ((x_70 Real)) :extrafuns ((x_71 Real)) :extrapreds ((x_72)) :extrafuns ((x_73 Real)) :extrafuns ((x_74 Real)) :extrafuns ((x_75 Real)) :extrafuns ((x_76 Real)) :extrapreds ((x_77)) :extrapreds ((x_78)) :extrapreds ((x_79)) :extrapreds ((x_80)) :extrapreds ((x_81)) :extrapreds ((x_82)) :extrafuns ((x_83 Real)) :extrapreds ((x_84)) :extrapreds ((x_85)) :extrapreds ((x_86)) :extrafuns ((x_87 Real)) :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)) :extrafuns ((x_95 Real)) :extrapreds ((x_96)) :extrafuns ((x_97 Real)) :extrafuns ((x_98 Real)) :extrafuns ((x_99 Real)) :extrafuns ((x_100 Real)) :extrapreds ((x_101)) :extrapreds ((x_102)) :extrapreds ((x_103)) :extrapreds ((x_104)) :extrapreds ((x_105)) :extrapreds ((x_106)) :extrafuns ((x_107 Real)) :extrapreds ((x_108)) :extrapreds ((x_109)) :extrapreds ((x_110)) :extrafuns ((x_111 Real)) :extrafuns ((x_112 Real)) :extrafuns ((x_113 Real)) :extrafuns ((x_114 Real)) :extrafuns ((x_115 Real)) :extrafuns ((x_116 Real)) :extrafuns ((x_117 Real)) :extrafuns ((x_118 Real)) :extrafuns ((x_119 Real)) :extrapreds ((x_120)) :extrafuns ((x_121 Real)) :extrafuns ((x_122 Real)) :extrafuns ((x_123 Real)) :extrafuns ((x_124 Real)) :extrapreds ((x_125)) :extrapreds ((x_126)) :extrapreds ((x_127)) :extrapreds ((x_128)) :extrapreds ((x_129)) :extrapreds ((x_130)) :extrafuns ((x_131 Real)) :extrafuns ((x_132 Real)) :extrafuns ((x_133 Real)) :extrapreds ((x_134)) :extrapreds ((x_135)) :extrapreds ((x_136)) :extrafuns ((x_137 Real)) :extrafuns ((x_138 Real)) :extrafuns ((x_139 Real)) :extrafuns ((x_140 Real)) :extrafuns ((x_141 Real)) :extrafuns ((x_142 Real)) :extrafuns ((x_143 Real)) :extrafuns ((x_144 Real)) :extrafuns ((x_145 Real)) :extrapreds ((x_146)) :extrafuns ((x_147 Real)) :extrafuns ((x_148 Real)) :extrafuns ((x_149 Real)) :formula (flet ($cvcl_12 x_11) (flet ($cvcl_13 x_12) (flet ($cvcl_14 x_13) (flet ($cvcl_9 x_16) (flet ($cvcl_10 x_17) (flet ($cvcl_11 x_18) (flet ($cvcl_6 x_21) (flet ($cvcl_7 x_22) (flet ($cvcl_8 x_23) (flet ($cvcl_3 x_26) (flet ($cvcl_4 x_27) (flet ($cvcl_5 x_28) (flet ($cvcl_0 x_31) (flet ($cvcl_1 x_32) (flet ($cvcl_2 x_33) (let (?cvcl_283 (+ x_9 x_35)) (flet ($cvcl_332 (<= x_36 x_37)) (flet ($cvcl_312 (iff x_16 x_11)) (flet ($cvcl_254 (= x_19 0)) (flet ($cvcl_267 $cvcl_254) (flet ($cvcl_268 (< x_36 x_8)) (flet ($cvcl_296 (= x_37 x_36)) (flet ($cvcl_320 $cvcl_296) (flet ($cvcl_313 (= x_19 2)) (flet ($cvcl_321 $cvcl_313) (flet ($cvcl_323 (iff x_38 x_39)) (flet ($cvcl_324 (and (iff x_40 x_41) (iff x_42 x_43))) (flet ($cvcl_310 (iff x_44 x_45)) (flet ($cvcl_311 (and (iff x_46 x_47) (iff x_48 x_49))) (flet ($cvcl_325 (= x_50 x_51)) (flet ($cvcl_326 (and (= x_2 x_0) (= x_3 x_1))) (flet ($cvcl_278 (= x_15 x_8)) (flet ($cvcl_309 (iff x_17 x_12)) (flet ($cvcl_307 (iff x_52 x_53)) (flet ($cvcl_308 (and (iff x_54 x_55) (iff x_56 x_57))) (flet ($cvcl_327 (iff x_18 x_13)) (let (?cvcl_333 (- x_58 x_9)) (flet ($cvcl_255 (= x_19 1)) (flet ($cvcl_300 $cvcl_255) (let (?cvcl_304 (+ x_35 x_9)) (flet ($cvcl_299 (<= x_59 x_37)) (flet ($cvcl_306 (iff x_38 (or x_39 (and $cvcl_299 x_53) ))) (flet ($cvcl_286 (<= x_62 ?cvcl_283)) (flet ($cvcl_288 (<= x_63 ?cvcl_283)) (flet ($cvcl_279 (<= x_62 x_35)) (flet ($cvcl_285 $cvcl_279) (flet ($cvcl_281 (<= x_63 x_35)) (flet ($cvcl_287 $cvcl_281) (flet ($cvcl_280 (not x_41)) (flet ($cvcl_291 $cvcl_280) (flet ($cvcl_314 (< x_62 x_36)) (flet ($cvcl_315 (= x_37 x_62)) (flet ($cvcl_282 (not x_43)) (flet ($cvcl_293 $cvcl_282) (flet ($cvcl_316 (< x_63 x_36)) (flet ($cvcl_317 (= x_37 x_63)) (flet ($cvcl_271 (not x_39)) (flet ($cvcl_295 $cvcl_271) (flet ($cvcl_334 (not $cvcl_332)) (flet ($cvcl_290 (not x_55)) (flet ($cvcl_292 (not x_57)) (flet ($cvcl_294 (not x_53)) (flet ($cvcl_297 (and (not $cvcl_279) (<= x_62 x_37))) (flet ($cvcl_298 (and (not $cvcl_281) (<= x_63 x_37))) (flet ($cvcl_305 (and (iff x_40 (or x_41 (and $cvcl_297 x_55) )) (iff x_42 (or x_43 (and $cvcl_298 x_57) )))) (flet ($cvcl_289 (<= x_59 ?cvcl_283)) (flet ($cvcl_318 (< x_59 x_36)) (flet ($cvcl_319 (= x_37 x_59)) (flet ($cvcl_322 (<= (ite x_45 (ite x_49 (ite x_47 3 2) x_60) (ite x_49 x_60 (ite x_47 1 0))) (* (* (ite x_39 (ite x_43 (ite x_41 0 1) x_61) (ite x_43 x_61 (ite x_41 2 3))) 1) (/ 1 2)))) (flet ($cvcl_337 $cvcl_299) (flet ($cvcl_301 (not $cvcl_286)) (flet ($cvcl_302 (not $cvcl_288)) (flet ($cvcl_15 (and (not (<= x_59 x_35)) $cvcl_299)) (flet ($cvcl_16 $cvcl_15) (flet ($cvcl_19 (and (not (<= x_64 x_35)) (<= x_64 x_37))) (flet ($cvcl_17 $cvcl_19) (flet ($cvcl_20 $cvcl_15) (flet ($cvcl_21 $cvcl_19) (flet ($cvcl_303 (not $cvcl_289)) (let (?cvcl_209 (+ x_9 x_37)) (flet ($cvcl_258 (<= x_58 x_76)) (flet ($cvcl_238 (iff x_21 x_16)) (flet ($cvcl_180 (= x_24 0)) (flet ($cvcl_193 $cvcl_180) (flet ($cvcl_194 (< x_58 x_15)) (flet ($cvcl_222 (= x_76 x_58)) (flet ($cvcl_246 $cvcl_222) (flet ($cvcl_239 (= x_24 2)) (flet ($cvcl_247 $cvcl_239) (flet ($cvcl_249 (iff x_77 x_38)) (flet ($cvcl_250 (and (iff x_78 x_40) (iff x_79 x_42))) (flet ($cvcl_236 (iff x_80 x_44)) (flet ($cvcl_237 (and (iff x_81 x_46) (iff x_82 x_48))) (flet ($cvcl_251 (= x_83 x_50)) (flet ($cvcl_252 (and (= x_4 x_2) (= x_5 x_3))) (flet ($cvcl_204 (= x_20 x_15)) (flet ($cvcl_235 (iff x_22 x_17)) (flet ($cvcl_233 (iff x_84 x_52)) (flet ($cvcl_234 (and (iff x_85 x_54) (iff x_86 x_56))) (flet ($cvcl_253 (iff x_23 x_18)) (let (?cvcl_259 (- x_87 x_9)) (flet ($cvcl_181 (= x_24 1)) (flet ($cvcl_226 $cvcl_181) (let (?cvcl_230 (+ x_37 x_9)) (flet ($cvcl_225 (<= x_73 x_76)) (flet ($cvcl_232 (iff x_77 (or x_38 (and $cvcl_225 x_52) ))) (flet ($cvcl_212 (<= x_70 ?cvcl_209)) (flet ($cvcl_214 (<= x_71 ?cvcl_209)) (flet ($cvcl_205 (<= x_70 x_37)) (flet ($cvcl_211 $cvcl_205) (flet ($cvcl_207 (<= x_71 x_37)) (flet ($cvcl_213 $cvcl_207) (flet ($cvcl_206 (not x_40)) (flet ($cvcl_217 $cvcl_206) (flet ($cvcl_240 (< x_70 x_58)) (flet ($cvcl_241 (= x_76 x_70)) (flet ($cvcl_208 (not x_42)) (flet ($cvcl_219 $cvcl_208) (flet ($cvcl_242 (< x_71 x_58)) (flet ($cvcl_243 (= x_76 x_71)) (flet ($cvcl_197 (not x_38)) (flet ($cvcl_221 $cvcl_197) (flet ($cvcl_260 (not $cvcl_258)) (flet ($cvcl_216 (not x_54)) (flet ($cvcl_218 (not x_56)) (flet ($cvcl_220 (not x_52)) (flet ($cvcl_223 (and (not $cvcl_205) (<= x_70 x_76))) (flet ($cvcl_224 (and (not $cvcl_207) (<= x_71 x_76))) (flet ($cvcl_231 (and (iff x_78 (or x_40 (and $cvcl_223 x_54) )) (iff x_79 (or x_42 (and $cvcl_224 x_56) )))) (flet ($cvcl_215 (<= x_73 ?cvcl_209)) (flet ($cvcl_244 (< x_73 x_58)) (flet ($cvcl_245 (= x_76 x_73)) (flet ($cvcl_248 (<= (ite x_44 (ite x_48 (ite x_46 3 2) x_88) (ite x_48 x_88 (ite x_46 1 0))) (* (* (ite x_38 (ite x_42 (ite x_40 0 1) x_89) (ite x_42 x_89 (ite x_40 2 3))) 1) (/ 1 2)))) (flet ($cvcl_263 $cvcl_225) (flet ($cvcl_227 (not $cvcl_212)) (flet ($cvcl_228 (not $cvcl_214)) (flet ($cvcl_335 (not (<= x_73 x_37))) (flet ($cvcl_22 (and $cvcl_335 $cvcl_225)) (flet ($cvcl_23 $cvcl_22) (flet ($cvcl_336 (not (<= x_74 x_37))) (flet ($cvcl_26 (and $cvcl_336 (<= x_74 x_76))) (flet ($cvcl_24 $cvcl_26) (flet ($cvcl_27 $cvcl_22) (flet ($cvcl_28 $cvcl_26) (flet ($cvcl_229 (not $cvcl_215)) (let (?cvcl_135 (+ x_9 x_76)) (flet ($cvcl_184 (<= x_87 x_100)) (flet ($cvcl_164 (iff x_26 x_21)) (flet ($cvcl_108 (= x_29 0)) (flet ($cvcl_119 $cvcl_108) (flet ($cvcl_120 (< x_87 x_20)) (flet ($cvcl_148 (= x_100 x_87)) (flet ($cvcl_172 $cvcl_148) (flet ($cvcl_165 (= x_29 2)) (flet ($cvcl_173 $cvcl_165) (flet ($cvcl_175 (iff x_101 x_77)) (flet ($cvcl_176 (and (iff x_102 x_78) (iff x_103 x_79))) (flet ($cvcl_162 (iff x_104 x_80)) (flet ($cvcl_163 (and (iff x_105 x_81) (iff x_106 x_82))) (flet ($cvcl_177 (= x_107 x_83)) (flet ($cvcl_178 (and (= x_6 x_4) (= x_7 x_5))) (flet ($cvcl_130 (= x_25 x_20)) (flet ($cvcl_161 (iff x_27 x_22)) (flet ($cvcl_159 (iff x_108 x_84)) (flet ($cvcl_160 (and (iff x_109 x_85) (iff x_110 x_86))) (flet ($cvcl_179 (iff x_28 x_23)) (let (?cvcl_185 (- x_111 x_9)) (flet ($cvcl_109 (= x_29 1)) (flet ($cvcl_152 $cvcl_109) (let (?cvcl_156 (+ x_76 x_9)) (flet ($cvcl_151 (<= x_97 x_100)) (flet ($cvcl_158 (iff x_101 (or x_77 (and $cvcl_151 x_84) ))) (flet ($cvcl_138 (<= x_94 ?cvcl_135)) (flet ($cvcl_140 (<= x_95 ?cvcl_135)) (flet ($cvcl_131 (<= x_94 x_76)) (flet ($cvcl_137 $cvcl_131) (flet ($cvcl_133 (<= x_95 x_76)) (flet ($cvcl_139 $cvcl_133) (flet ($cvcl_132 (not x_78)) (flet ($cvcl_143 $cvcl_132) (flet ($cvcl_166 (< x_94 x_87)) (flet ($cvcl_167 (= x_100 x_94)) (flet ($cvcl_134 (not x_79)) (flet ($cvcl_145 $cvcl_134) (flet ($cvcl_168 (< x_95 x_87)) (flet ($cvcl_169 (= x_100 x_95)) (flet ($cvcl_123 (not x_77)) (flet ($cvcl_147 $cvcl_123) (flet ($cvcl_186 (not $cvcl_184)) (flet ($cvcl_142 (not x_85)) (flet ($cvcl_144 (not x_86)) (flet ($cvcl_146 (not x_84)) (flet ($cvcl_149 (and (not $cvcl_131) (<= x_94 x_100))) (flet ($cvcl_150 (and (not $cvcl_133) (<= x_95 x_100))) (flet ($cvcl_157 (and (iff x_102 (or x_78 (and $cvcl_149 x_85) )) (iff x_103 (or x_79 (and $cvcl_150 x_86) )))) (flet ($cvcl_141 (<= x_97 ?cvcl_135)) (flet ($cvcl_170 (< x_97 x_87)) (flet ($cvcl_171 (= x_100 x_97)) (flet ($cvcl_174 (<= (ite x_80 (ite x_82 (ite x_81 3 2) x_112) (ite x_82 x_112 (ite x_81 1 0))) (* (* (ite x_77 (ite x_79 (ite x_78 0 1) x_113) (ite x_79 x_113 (ite x_78 2 3))) 1) (/ 1 2)))) (flet ($cvcl_189 $cvcl_151) (flet ($cvcl_153 (not $cvcl_138)) (flet ($cvcl_154 (not $cvcl_140)) (flet ($cvcl_261 (not (<= x_97 x_76))) (flet ($cvcl_29 (and $cvcl_261 $cvcl_151)) (flet ($cvcl_30 $cvcl_29) (flet ($cvcl_262 (not (<= x_98 x_76))) (flet ($cvcl_33 (and $cvcl_262 (<= x_98 x_100))) (flet ($cvcl_31 $cvcl_33) (flet ($cvcl_34 $cvcl_29) (flet ($cvcl_35 $cvcl_33) (flet ($cvcl_155 (not $cvcl_141)) (let (?cvcl_64 (+ x_9 x_100)) (flet ($cvcl_112 (<= x_111 x_124)) (flet ($cvcl_92 (iff x_31 x_26)) (flet ($cvcl_43 (= x_34 0)) (flet ($cvcl_47 $cvcl_43) (flet ($cvcl_48 (< x_111 x_25)) (flet ($cvcl_76 (= x_124 x_111)) (flet ($cvcl_100 $cvcl_76) (flet ($cvcl_93 (= x_34 2)) (flet ($cvcl_101 $cvcl_93) (flet ($cvcl_103 (iff x_125 x_101)) (flet ($cvcl_104 (and (iff x_126 x_102) (iff x_127 x_103))) (flet ($cvcl_90 (iff x_128 x_104)) (flet ($cvcl_91 (and (iff x_129 x_105) (iff x_130 x_106))) (flet ($cvcl_105 (= x_131 x_107)) (flet ($cvcl_106 (and (= x_132 x_6) (= x_133 x_7))) (flet ($cvcl_58 (= x_30 x_25)) (flet ($cvcl_89 (iff x_32 x_27)) (flet ($cvcl_87 (iff x_134 x_108)) (flet ($cvcl_88 (and (iff x_135 x_109) (iff x_136 x_110))) (flet ($cvcl_107 (iff x_33 x_28)) (let (?cvcl_113 (- x_137 x_9)) (flet ($cvcl_59 (= x_34 1)) (flet ($cvcl_80 $cvcl_59) (let (?cvcl_84 (+ x_100 x_9)) (flet ($cvcl_79 (<= x_121 x_124)) (flet ($cvcl_86 (iff x_125 (or x_101 (and $cvcl_79 x_108) ))) (flet ($cvcl_66 (<= x_118 ?cvcl_64)) (flet ($cvcl_68 (<= x_119 ?cvcl_64)) (flet ($cvcl_60 (<= x_118 x_100)) (flet ($cvcl_65 $cvcl_60) (flet ($cvcl_62 (<= x_119 x_100)) (flet ($cvcl_67 $cvcl_62) (flet ($cvcl_61 (not x_102)) (flet ($cvcl_71 $cvcl_61) (flet ($cvcl_94 (< x_118 x_111)) (flet ($cvcl_95 (= x_124 x_118)) (flet ($cvcl_63 (not x_103)) (flet ($cvcl_73 $cvcl_63) (flet ($cvcl_96 (< x_119 x_111)) (flet ($cvcl_97 (= x_124 x_119)) (flet ($cvcl_51 (not x_101)) (flet ($cvcl_75 $cvcl_51) (flet ($cvcl_114 (not $cvcl_112)) (flet ($cvcl_70 (not x_109)) (flet ($cvcl_72 (not x_110)) (flet ($cvcl_74 (not x_108)) (flet ($cvcl_77 (and (not $cvcl_60) (<= x_118 x_124))) (flet ($cvcl_78 (and (not $cvcl_62) (<= x_119 x_124))) (flet ($cvcl_85 (and (iff x_126 (or x_102 (and $cvcl_77 x_109) )) (iff x_127 (or x_103 (and $cvcl_78 x_110) )))) (flet ($cvcl_69 (<= x_121 ?cvcl_64)) (flet ($cvcl_98 (< x_121 x_111)) (flet ($cvcl_99 (= x_124 x_121)) (flet ($cvcl_102 (<= (ite x_104 (ite x_106 (ite x_105 3 2) x_138) (ite x_106 x_138 (ite x_105 1 0))) (* (* (ite x_101 (ite x_103 (ite x_102 0 1) x_139) (ite x_103 x_139 (ite x_102 2 3))) 1) (/ 1 2)))) (flet ($cvcl_115 $cvcl_79) (flet ($cvcl_81 (not $cvcl_66)) (flet ($cvcl_82 (not $cvcl_68)) (flet ($cvcl_187 (not (<= x_121 x_100))) (flet ($cvcl_36 (and $cvcl_187 $cvcl_79)) (flet ($cvcl_37 $cvcl_36) (flet ($cvcl_188 (not (<= x_122 x_100))) (flet ($cvcl_40 (and $cvcl_188 (<= x_122 x_124))) (flet ($cvcl_38 $cvcl_40) (flet ($cvcl_41 $cvcl_36) (flet ($cvcl_42 $cvcl_40) (flet ($cvcl_83 (not $cvcl_69)) (flet ($cvcl_273 (= x_2 0)) (flet ($cvcl_264 (= x_2 3)) (flet ($cvcl_275 (= x_3 0)) (flet ($cvcl_265 (= x_3 3)) (flet ($cvcl_199 (= x_4 0)) (flet ($cvcl_190 (= x_4 3)) (flet ($cvcl_201 (= x_5 0)) (flet ($cvcl_191 (= x_5 3)) (flet ($cvcl_125 (= x_6 0)) (flet ($cvcl_116 (= x_6 3)) (flet ($cvcl_127 (= x_7 0)) (flet ($cvcl_117 (= x_7 3)) (flet ($cvcl_277 (= x_50 0)) (flet ($cvcl_266 (= x_50 3)) (flet ($cvcl_203 (= x_83 0)) (flet ($cvcl_192 (= x_83 3)) (flet ($cvcl_129 (= x_107 0)) (flet ($cvcl_118 (= x_107 3)) (flet ($cvcl_57 (= x_131 0)) (flet ($cvcl_46 (= x_131 3)) (flet ($cvcl_53 (= x_132 0)) (flet ($cvcl_44 (= x_132 3)) (flet ($cvcl_55 (= x_133 0)) (flet ($cvcl_45 (= x_133 3)) (flet ($cvcl_110 (not $cvcl_108)) (flet ($cvcl_111 (not $cvcl_109)) (flet ($cvcl_182 (not $cvcl_180)) (flet ($cvcl_183 (not $cvcl_181)) (flet ($cvcl_256 (not $cvcl_254)) (flet ($cvcl_257 (not $cvcl_255)) (flet ($cvcl_328 (= x_14 0)) (flet ($cvcl_330 (not $cvcl_328)) (flet ($cvcl_329 (= x_14 1)) (flet ($cvcl_331 (not $cvcl_329)) (flet ($cvcl_18 (and (not (<= x_67 x_35)) (<= x_67 x_37))) (flet ($cvcl_25 (and (not (<= x_75 x_37)) (<= x_75 x_76))) (flet ($cvcl_32 (and (not (<= x_99 x_76)) (<= x_99 x_100))) (flet ($cvcl_39 (and (not (<= x_123 x_100)) (<= x_123 x_124))) (flet ($cvcl_49 (= x_132 (ite $cvcl_61 (ite (and $cvcl_77 (< x_6 3)) (+ x_6 1) x_6) x_6))) (flet ($cvcl_50 (= x_133 (ite $cvcl_63 (ite (and $cvcl_78 (< x_7 3)) (+ x_7 1) x_7) x_7))) (flet ($cvcl_52 (or x_102 $cvcl_44 )) (flet ($cvcl_54 (or x_103 $cvcl_45 )) (flet ($cvcl_56 (or x_101 $cvcl_46 )) (flet ($cvcl_136 (not x_28)) (flet ($cvcl_121 (= x_6 (ite $cvcl_132 (ite (and $cvcl_149 (< x_4 3)) (+ x_4 1) x_4) x_4))) (flet ($cvcl_122 (= x_7 (ite $cvcl_134 (ite (and $cvcl_150 (< x_5 3)) (+ x_5 1) x_5) x_5))) (flet ($cvcl_124 (or x_78 $cvcl_116 )) (flet ($cvcl_126 (or x_79 $cvcl_117 )) (flet ($cvcl_128 (or x_77 $cvcl_118 )) (flet ($cvcl_210 (not x_23)) (flet ($cvcl_195 (= x_4 (ite $cvcl_206 (ite (and $cvcl_223 (< x_2 3)) (+ x_2 1) x_2) x_2))) (flet ($cvcl_196 (= x_5 (ite $cvcl_208 (ite (and $cvcl_224 (< x_3 3)) (+ x_3 1) x_3) x_3))) (flet ($cvcl_198 (or x_40 $cvcl_190 )) (flet ($cvcl_200 (or x_42 $cvcl_191 )) (flet ($cvcl_202 (or x_38 $cvcl_192 )) (flet ($cvcl_284 (not x_18)) (flet ($cvcl_269 (= x_2 (ite $cvcl_280 (ite (and $cvcl_297 (< x_0 3)) (+ x_0 1) x_0) x_0))) (flet ($cvcl_270 (= x_3 (ite $cvcl_282 (ite (and $cvcl_298 (< x_1 3)) (+ x_1 1) x_1) x_1))) (flet ($cvcl_272 (or x_41 $cvcl_264 )) (flet ($cvcl_274 (or x_43 $cvcl_265 )) (flet ($cvcl_276 (or x_39 $cvcl_266 )) (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 (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_34 2) (>= x_34 0)) (<= x_29 2)) (>= x_29 0)) (<= x_24 2)) (>= x_24 0)) (<= x_19 2)) (>= x_19 0)) (<= x_14 2)) (>= x_14 0)) (or (or (or (= x_0 0) (= x_0 1) ) (= x_0 2) ) (= x_0 3) )) (not (< x_0 0))) (<= x_0 3)) (or (or (or (= x_1 0) (= x_1 1) ) (= x_1 2) ) (= x_1 3) )) (not (< x_1 0))) (<= x_1 3)) (or (or (or $cvcl_273 (= x_2 1) ) (= x_2 2) ) $cvcl_264 )) (not (< x_2 0))) (<= x_2 3)) (or (or (or $cvcl_275 (= x_3 1) ) (= x_3 2) ) $cvcl_265 )) (not (< x_3 0))) (<= x_3 3)) (or (or (or $cvcl_199 (= x_4 1) ) (= x_4 2) ) $cvcl_190 )) (not (< x_4 0))) (<= x_4 3)) (or (or (or $cvcl_201 (= x_5 1) ) (= x_5 2) ) $cvcl_191 )) (not (< x_5 0))) (<= x_5 3)) (or (or (or $cvcl_125 (= x_6 1) ) (= x_6 2) ) $cvcl_116 )) (not (< x_6 0))) (<= x_6 3)) (or (or (or $cvcl_127 (= x_7 1) ) (= x_7 2) ) $cvcl_117 )) (not (< x_7 0))) (<= x_7 3)) (>= x_8 0)) (> x_9 0)) (>= x_9 0)) (not (<= x_10 (* x_9 3)))) (>= x_10 0)) (>= x_15 0)) (>= x_20 0)) (>= x_25 0)) (>= x_30 0)) (>= x_35 0)) (>= x_36 0)) (>= x_37 0)) (or (or (or $cvcl_277 (= x_50 1) ) (= x_50 2) ) $cvcl_266 )) (not (< x_50 0))) (<= x_50 3)) (or (or (or (= x_51 0) (= x_51 1) ) (= x_51 2) ) (= x_51 3) )) (not (< x_51 0))) (<= x_51 3)) (>= x_58 0)) (>= x_59 0)) (>= x_62 0)) (>= x_63 0)) (>= x_64 0)) (>= x_67 0)) (>= x_70 0)) (>= x_71 0)) (>= x_73 0)) (>= x_74 0)) (>= x_75 0)) (>= x_76 0)) (or (or (or $cvcl_203 (= x_83 1) ) (= x_83 2) ) $cvcl_192 )) (not (< x_83 0))) (<= x_83 3)) (>= x_87 0)) (>= x_94 0)) (>= x_95 0)) (>= x_97 0)) (>= x_98 0)) (>= x_99 0)) (>= x_100 0)) (or (or (or $cvcl_129 (= x_107 1) ) (= x_107 2) ) $cvcl_118 )) (not (< x_107 0))) (<= x_107 3)) (>= x_111 0)) (>= x_118 0)) (>= x_119 0)) (>= x_121 0)) (>= x_122 0)) (>= x_123 0)) (>= x_124 0)) (or (or (or $cvcl_57 (= x_131 1) ) (= x_131 2) ) $cvcl_46 )) (not (< x_131 0))) (<= x_131 3)) (or (or (or $cvcl_53 (= x_132 1) ) (= x_132 2) ) $cvcl_44 )) (not (< x_132 0))) (<= x_132 3)) (or (or (or $cvcl_55 (= x_133 1) ) (= x_133 2) ) $cvcl_45 )) (not (< x_133 0))) (<= x_133 3)) (>= x_137 0)) (>= x_144 0)) (>= x_145 0)) (>= x_147 0)) (>= x_148 0)) (>= x_149 0)) (<= x_6 2)) (<= x_7 2)) (<= x_4 2)) (<= x_5 2)) (<= x_2 2)) (<= x_3 2)) (<= x_0 2)) (<= x_1 2)) (< x_30 (+ (* x_10 2) x_9))) (or (not $cvcl_43) (and $cvcl_2 $cvcl_0) )) (or (not $cvcl_59) (and $cvcl_1 $cvcl_0) )) (or (not $cvcl_93) (and $cvcl_1 $cvcl_2) )) (< x_25 (+ (* x_10 2) x_9))) (or $cvcl_110 (and $cvcl_5 $cvcl_3) )) (or $cvcl_111 (and $cvcl_4 $cvcl_3) )) (or (not $cvcl_165) (and $cvcl_4 $cvcl_5) )) (< x_20 (+ (* x_10 2) x_9))) (or $cvcl_182 (and $cvcl_8 $cvcl_6) )) (or $cvcl_183 (and $cvcl_7 $cvcl_6) )) (or (not $cvcl_239) (and $cvcl_7 $cvcl_8) )) (< x_15 (+ (* x_10 2) x_9))) (or $cvcl_256 (and $cvcl_11 $cvcl_9) )) (or $cvcl_257 (and $cvcl_10 $cvcl_9) )) (or (not $cvcl_313) (and $cvcl_10 $cvcl_11) )) (< x_8 (+ (* x_10 2) x_9))) (or $cvcl_330 (and $cvcl_14 $cvcl_12) )) (or $cvcl_331 (and $cvcl_13 $cvcl_12) )) (or (not (= x_14 2)) (and $cvcl_13 $cvcl_14) )) (= x_60 (ite x_47 2 1))) (= x_61 (ite x_41 1 2))) (= x_65 (ite $cvcl_16 2 1))) (= x_66 (ite $cvcl_20 2 1))) (= x_68 (+ (ite $cvcl_18 (ite $cvcl_17 (ite $cvcl_16 3 2) x_65) (ite $cvcl_17 x_65 (ite $cvcl_16 1 0))) x_51))) (= x_69 (+ (ite $cvcl_18 (ite $cvcl_21 (ite $cvcl_20 3 2) x_66) (ite $cvcl_21 x_66 (ite $cvcl_20 1 0))) x_51))) (= x_88 (ite x_46 2 1))) (= x_89 (ite x_40 1 2))) (= x_90 (ite $cvcl_23 2 1))) (= x_91 (ite $cvcl_27 2 1))) (= x_92 (+ (ite $cvcl_25 (ite $cvcl_24 (ite $cvcl_23 3 2) x_90) (ite $cvcl_24 x_90 (ite $cvcl_23 1 0))) x_50))) (= x_93 (+ (ite $cvcl_25 (ite $cvcl_28 (ite $cvcl_27 3 2) x_91) (ite $cvcl_28 x_91 (ite $cvcl_27 1 0))) x_50))) (= x_112 (ite x_81 2 1))) (= x_113 (ite x_78 1 2))) (= x_114 (ite $cvcl_30 2 1))) (= x_115 (ite $cvcl_34 2 1))) (= x_116 (+ (ite $cvcl_32 (ite $cvcl_31 (ite $cvcl_30 3 2) x_114) (ite $cvcl_31 x_114 (ite $cvcl_30 1 0))) x_83))) (= x_117 (+ (ite $cvcl_32 (ite $cvcl_35 (ite $cvcl_34 3 2) x_115) (ite $cvcl_35 x_115 (ite $cvcl_34 1 0))) x_83))) (= x_138 (ite x_105 2 1))) (= x_139 (ite x_102 1 2))) (= x_140 (ite $cvcl_37 2 1))) (= x_141 (ite $cvcl_41 2 1))) (= x_142 (+ (ite $cvcl_39 (ite $cvcl_38 (ite $cvcl_37 3 2) x_140) (ite $cvcl_38 x_140 (ite $cvcl_37 1 0))) x_107))) (= x_143 (+ (ite $cvcl_39 (ite $cvcl_42 (ite $cvcl_41 3 2) x_141) (ite $cvcl_42 x_141 (ite $cvcl_41 1 0))) x_107))) (or (or (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and $cvcl_47 $cvcl_48) $cvcl_76) $cvcl_49) $cvcl_50) (= x_131 (ite $cvcl_51 (ite (not (< x_142 3)) 3 x_142) x_107))) (iff x_126 $cvcl_52)) (iff x_127 $cvcl_54)) (iff x_125 $cvcl_56)) $cvcl_89) $cvcl_58) (and (and (and (and (and (and (and (and (and (and $cvcl_47 (not $cvcl_48)) x_32) (= x_124 x_25)) $cvcl_49) $cvcl_50) (= x_131 (ite $cvcl_51 (ite (not (< x_143 3)) 3 x_143) x_107))) (iff x_126 (or $cvcl_52 $cvcl_53 ))) (iff x_127 (or $cvcl_54 $cvcl_55 ))) (iff x_125 (or $cvcl_56 $cvcl_57 ))) $cvcl_58) ) $cvcl_87) $cvcl_88) $cvcl_107) $cvcl_90) $cvcl_91) $cvcl_92) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_80 (or (or (and (and (and (not $cvcl_65) $cvcl_71) $cvcl_70) $cvcl_66) (and (and (and (not $cvcl_67) $cvcl_73) $cvcl_72) $cvcl_68) ) (and (and $cvcl_75 $cvcl_74) $cvcl_69) )) (not x_33)) (or (or (or (or $cvcl_65 $cvcl_81 ) x_109 ) x_102 ) (not (< x_124 x_118)) )) (or (or (or (or $cvcl_67 $cvcl_82 ) x_110 ) x_103 ) (not (< x_124 x_119)) )) (or (or (or $cvcl_83 x_108 ) x_101 ) (not (< x_124 x_121)) )) (or (or (or (and (and (and (and $cvcl_70 $cvcl_71) $cvcl_66) $cvcl_94) $cvcl_95) (and (and (and (and $cvcl_72 $cvcl_73) $cvcl_68) $cvcl_96) $cvcl_97) ) (and (and (and (and $cvcl_74 $cvcl_75) $cvcl_69) $cvcl_98) $cvcl_99) ) (and (< x_111 ?cvcl_84) $cvcl_100) )) (iff x_135 (or x_109 $cvcl_77 ))) (iff x_136 (or x_110 $cvcl_78 ))) (iff x_134 (or x_108 $cvcl_79 ))) $cvcl_85) $cvcl_86) (and (and (and (and (and (and (and (and (and $cvcl_80 (or (or (or $cvcl_65 x_109 ) x_102 ) $cvcl_81 )) (or (or (or $cvcl_67 x_110 ) x_103 ) $cvcl_82 )) (or (or x_108 x_101 ) $cvcl_83 )) x_33) (= x_124 ?cvcl_84)) $cvcl_85) $cvcl_86) $cvcl_87) $cvcl_88) ) $cvcl_105) $cvcl_106) $cvcl_58) $cvcl_89) $cvcl_90) $cvcl_91) $cvcl_92) ) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_101 $cvcl_102) (not x_31)) (or (or (or $cvcl_65 x_105 ) x_102 ) (<= x_124 x_118) )) (or (or (or $cvcl_67 x_106 ) x_103 ) (<= x_124 x_119) )) (or (or x_104 x_101 ) (<= x_124 x_121) )) (or (or (or (and (and (and (and (not x_105) $cvcl_71) (< x_100 x_118)) $cvcl_94) $cvcl_95) (and (and (and (and (not x_106) $cvcl_73) (< x_100 x_119)) $cvcl_96) $cvcl_97) ) (and (and (and (not x_104) $cvcl_75) $cvcl_98) $cvcl_99) ) $cvcl_100 )) (iff x_129 (or x_105 (= x_118 x_124) ))) (iff x_130 (or x_106 (= x_119 x_124) ))) (iff x_128 (or x_104 (= x_121 x_124) ))) $cvcl_103) $cvcl_104) (and (and (and (and (and (and (and $cvcl_101 (not $cvcl_102)) x_31) $cvcl_103) $cvcl_104) (= x_124 x_100)) $cvcl_90) $cvcl_91) ) $cvcl_105) $cvcl_106) $cvcl_58) $cvcl_89) $cvcl_87) $cvcl_88) $cvcl_107) )) (or (or (and $cvcl_108 (= x_34 (ite (not x_27) x_29 1))) (and $cvcl_109 (= x_34 (ite $cvcl_136 x_29 2))) ) (and (and $cvcl_110 $cvcl_111) (= x_34 x_29)) )) (or (and (and $cvcl_112 (not (<= x_137 x_144))) (not (<= x_144 ?cvcl_113))) (and $cvcl_114 (= x_144 x_118)) )) (or (and (and $cvcl_112 (not (<= x_137 x_145))) (not (<= x_145 ?cvcl_113))) (and $cvcl_114 (= x_145 x_119)) )) (or (and (and $cvcl_112 (= x_137 (+ x_111 x_10))) x_146) (and (and $cvcl_114 (not x_146)) (= x_137 x_111)) )) (or (and (and (and (and $cvcl_115 (not (<= x_147 x_124))) (not (<= x_148 x_124))) (< x_147 x_148)) (< x_148 x_149)) (and (and (and (not $cvcl_115) (= x_147 x_121)) (= x_148 x_122)) (= x_149 x_123)) )) (or (or (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and $cvcl_119 $cvcl_120) $cvcl_148) $cvcl_121) $cvcl_122) (= x_107 (ite $cvcl_123 (ite (not (< x_116 3)) 3 x_116) x_83))) (iff x_102 $cvcl_124)) (iff x_103 $cvcl_126)) (iff x_101 $cvcl_128)) $cvcl_161) $cvcl_130) (and (and (and (and (and (and (and (and (and (and $cvcl_119 (not $cvcl_120)) x_27) (= x_100 x_20)) $cvcl_121) $cvcl_122) (= x_107 (ite $cvcl_123 (ite (not (< x_117 3)) 3 x_117) x_83))) (iff x_102 (or $cvcl_124 $cvcl_125 ))) (iff x_103 (or $cvcl_126 $cvcl_127 ))) (iff x_101 (or $cvcl_128 $cvcl_129 ))) $cvcl_130) ) $cvcl_159) $cvcl_160) $cvcl_179) $cvcl_162) $cvcl_163) $cvcl_164) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_152 (or (or (and (and (and (not $cvcl_137) $cvcl_143) $cvcl_142) $cvcl_138) (and (and (and (not $cvcl_139) $cvcl_145) $cvcl_144) $cvcl_140) ) (and (and $cvcl_147 $cvcl_146) $cvcl_141) )) $cvcl_136) (or (or (or (or $cvcl_137 $cvcl_153 ) x_85 ) x_78 ) (not (< x_100 x_94)) )) (or (or (or (or $cvcl_139 $cvcl_154 ) x_86 ) x_79 ) (not (< x_100 x_95)) )) (or (or (or $cvcl_155 x_84 ) x_77 ) (not (< x_100 x_97)) )) (or (or (or (and (and (and (and $cvcl_142 $cvcl_143) $cvcl_138) $cvcl_166) $cvcl_167) (and (and (and (and $cvcl_144 $cvcl_145) $cvcl_140) $cvcl_168) $cvcl_169) ) (and (and (and (and $cvcl_146 $cvcl_147) $cvcl_141) $cvcl_170) $cvcl_171) ) (and (< x_87 ?cvcl_156) $cvcl_172) )) (iff x_109 (or x_85 $cvcl_149 ))) (iff x_110 (or x_86 $cvcl_150 ))) (iff x_108 (or x_84 $cvcl_151 ))) $cvcl_157) $cvcl_158) (and (and (and (and (and (and (and (and (and $cvcl_152 (or (or (or $cvcl_137 x_85 ) x_78 ) $cvcl_153 )) (or (or (or $cvcl_139 x_86 ) x_79 ) $cvcl_154 )) (or (or x_84 x_77 ) $cvcl_155 )) x_28) (= x_100 ?cvcl_156)) $cvcl_157) $cvcl_158) $cvcl_159) $cvcl_160) ) $cvcl_177) $cvcl_178) $cvcl_130) $cvcl_161) $cvcl_162) $cvcl_163) $cvcl_164) ) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_173 $cvcl_174) (not x_26)) (or (or (or $cvcl_137 x_81 ) x_78 ) (<= x_100 x_94) )) (or (or (or $cvcl_139 x_82 ) x_79 ) (<= x_100 x_95) )) (or (or x_80 x_77 ) (<= x_100 x_97) )) (or (or (or (and (and (and (and (not x_81) $cvcl_143) (< x_76 x_94)) $cvcl_166) $cvcl_167) (and (and (and (and (not x_82) $cvcl_145) (< x_76 x_95)) $cvcl_168) $cvcl_169) ) (and (and (and (not x_80) $cvcl_147) $cvcl_170) $cvcl_171) ) $cvcl_172 )) (iff x_105 (or x_81 (= x_94 x_100) ))) (iff x_106 (or x_82 (= x_95 x_100) ))) (iff x_104 (or x_80 (= x_97 x_100) ))) $cvcl_175) $cvcl_176) (and (and (and (and (and (and (and $cvcl_173 (not $cvcl_174)) x_26) $cvcl_175) $cvcl_176) (= x_100 x_76)) $cvcl_162) $cvcl_163) ) $cvcl_177) $cvcl_178) $cvcl_130) $cvcl_161) $cvcl_159) $cvcl_160) $cvcl_179) )) (or (or (and $cvcl_180 (= x_29 (ite (not x_22) x_24 1))) (and $cvcl_181 (= x_29 (ite $cvcl_210 x_24 2))) ) (and (and $cvcl_182 $cvcl_183) (= x_29 x_24)) )) (or (and (and $cvcl_184 (not (<= x_111 x_118))) (not (<= x_118 ?cvcl_185))) (and $cvcl_186 (= x_118 x_94)) )) (or (and (and $cvcl_184 (not (<= x_111 x_119))) (not (<= x_119 ?cvcl_185))) (and $cvcl_186 (= x_119 x_95)) )) (or (and (and $cvcl_184 (= x_111 (+ x_87 x_10))) x_120) (and (and $cvcl_186 (not x_120)) (= x_111 x_87)) )) (or (and (and (and (and $cvcl_189 $cvcl_187) $cvcl_188) (< x_121 x_122)) (< x_122 x_123)) (and (and (and (not $cvcl_189) (= x_121 x_97)) (= x_122 x_98)) (= x_123 x_99)) )) (or (or (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and $cvcl_193 $cvcl_194) $cvcl_222) $cvcl_195) $cvcl_196) (= x_83 (ite $cvcl_197 (ite (not (< x_92 3)) 3 x_92) x_50))) (iff x_78 $cvcl_198)) (iff x_79 $cvcl_200)) (iff x_77 $cvcl_202)) $cvcl_235) $cvcl_204) (and (and (and (and (and (and (and (and (and (and $cvcl_193 (not $cvcl_194)) x_22) (= x_76 x_15)) $cvcl_195) $cvcl_196) (= x_83 (ite $cvcl_197 (ite (not (< x_93 3)) 3 x_93) x_50))) (iff x_78 (or $cvcl_198 $cvcl_199 ))) (iff x_79 (or $cvcl_200 $cvcl_201 ))) (iff x_77 (or $cvcl_202 $cvcl_203 ))) $cvcl_204) ) $cvcl_233) $cvcl_234) $cvcl_253) $cvcl_236) $cvcl_237) $cvcl_238) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_226 (or (or (and (and (and (not $cvcl_211) $cvcl_217) $cvcl_216) $cvcl_212) (and (and (and (not $cvcl_213) $cvcl_219) $cvcl_218) $cvcl_214) ) (and (and $cvcl_221 $cvcl_220) $cvcl_215) )) $cvcl_210) (or (or (or (or $cvcl_211 $cvcl_227 ) x_54 ) x_40 ) (not (< x_76 x_70)) )) (or (or (or (or $cvcl_213 $cvcl_228 ) x_56 ) x_42 ) (not (< x_76 x_71)) )) (or (or (or $cvcl_229 x_52 ) x_38 ) (not (< x_76 x_73)) )) (or (or (or (and (and (and (and $cvcl_216 $cvcl_217) $cvcl_212) $cvcl_240) $cvcl_241) (and (and (and (and $cvcl_218 $cvcl_219) $cvcl_214) $cvcl_242) $cvcl_243) ) (and (and (and (and $cvcl_220 $cvcl_221) $cvcl_215) $cvcl_244) $cvcl_245) ) (and (< x_58 ?cvcl_230) $cvcl_246) )) (iff x_85 (or x_54 $cvcl_223 ))) (iff x_86 (or x_56 $cvcl_224 ))) (iff x_84 (or x_52 $cvcl_225 ))) $cvcl_231) $cvcl_232) (and (and (and (and (and (and (and (and (and $cvcl_226 (or (or (or $cvcl_211 x_54 ) x_40 ) $cvcl_227 )) (or (or (or $cvcl_213 x_56 ) x_42 ) $cvcl_228 )) (or (or x_52 x_38 ) $cvcl_229 )) x_23) (= x_76 ?cvcl_230)) $cvcl_231) $cvcl_232) $cvcl_233) $cvcl_234) ) $cvcl_251) $cvcl_252) $cvcl_204) $cvcl_235) $cvcl_236) $cvcl_237) $cvcl_238) ) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_247 $cvcl_248) (not x_21)) (or (or (or $cvcl_211 x_46 ) x_40 ) (<= x_76 x_70) )) (or (or (or $cvcl_213 x_48 ) x_42 ) (<= x_76 x_71) )) (or (or x_44 x_38 ) (<= x_76 x_73) )) (or (or (or (and (and (and (and (not x_46) $cvcl_217) (< x_37 x_70)) $cvcl_240) $cvcl_241) (and (and (and (and (not x_48) $cvcl_219) (< x_37 x_71)) $cvcl_242) $cvcl_243) ) (and (and (and (not x_44) $cvcl_221) $cvcl_244) $cvcl_245) ) $cvcl_246 )) (iff x_81 (or x_46 (= x_70 x_76) ))) (iff x_82 (or x_48 (= x_71 x_76) ))) (iff x_80 (or x_44 (= x_73 x_76) ))) $cvcl_249) $cvcl_250) (and (and (and (and (and (and (and $cvcl_247 (not $cvcl_248)) x_21) $cvcl_249) $cvcl_250) (= x_76 x_37)) $cvcl_236) $cvcl_237) ) $cvcl_251) $cvcl_252) $cvcl_204) $cvcl_235) $cvcl_233) $cvcl_234) $cvcl_253) )) (or (or (and $cvcl_254 (= x_24 (ite (not x_17) x_19 1))) (and $cvcl_255 (= x_24 (ite $cvcl_284 x_19 2))) ) (and (and $cvcl_256 $cvcl_257) (= x_24 x_19)) )) (or (and (and $cvcl_258 (not (<= x_87 x_94))) (not (<= x_94 ?cvcl_259))) (and $cvcl_260 (= x_94 x_70)) )) (or (and (and $cvcl_258 (not (<= x_87 x_95))) (not (<= x_95 ?cvcl_259))) (and $cvcl_260 (= x_95 x_71)) )) (or (and (and $cvcl_258 (= x_87 (+ x_58 x_10))) x_96) (and (and $cvcl_260 (not x_96)) (= x_87 x_58)) )) (or (and (and (and (and $cvcl_263 $cvcl_261) $cvcl_262) (< x_97 x_98)) (< x_98 x_99)) (and (and (and (not $cvcl_263) (= x_97 x_73)) (= x_98 x_74)) (= x_99 x_75)) )) (or (or (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and $cvcl_267 $cvcl_268) $cvcl_296) $cvcl_269) $cvcl_270) (= x_50 (ite $cvcl_271 (ite (not (< x_68 3)) 3 x_68) x_51))) (iff x_40 $cvcl_272)) (iff x_42 $cvcl_274)) (iff x_38 $cvcl_276)) $cvcl_309) $cvcl_278) (and (and (and (and (and (and (and (and (and (and $cvcl_267 (not $cvcl_268)) x_17) (= x_37 x_8)) $cvcl_269) $cvcl_270) (= x_50 (ite $cvcl_271 (ite (not (< x_69 3)) 3 x_69) x_51))) (iff x_40 (or $cvcl_272 $cvcl_273 ))) (iff x_42 (or $cvcl_274 $cvcl_275 ))) (iff x_38 (or $cvcl_276 $cvcl_277 ))) $cvcl_278) ) $cvcl_307) $cvcl_308) $cvcl_327) $cvcl_310) $cvcl_311) $cvcl_312) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_300 (or (or (and (and (and (not $cvcl_285) $cvcl_291) $cvcl_290) $cvcl_286) (and (and (and (not $cvcl_287) $cvcl_293) $cvcl_292) $cvcl_288) ) (and (and $cvcl_295 $cvcl_294) $cvcl_289) )) $cvcl_284) (or (or (or (or $cvcl_285 $cvcl_301 ) x_55 ) x_41 ) (not (< x_37 x_62)) )) (or (or (or (or $cvcl_287 $cvcl_302 ) x_57 ) x_43 ) (not (< x_37 x_63)) )) (or (or (or $cvcl_303 x_53 ) x_39 ) (not (< x_37 x_59)) )) (or (or (or (and (and (and (and $cvcl_290 $cvcl_291) $cvcl_286) $cvcl_314) $cvcl_315) (and (and (and (and $cvcl_292 $cvcl_293) $cvcl_288) $cvcl_316) $cvcl_317) ) (and (and (and (and $cvcl_294 $cvcl_295) $cvcl_289) $cvcl_318) $cvcl_319) ) (and (< x_36 ?cvcl_304) $cvcl_320) )) (iff x_54 (or x_55 $cvcl_297 ))) (iff x_56 (or x_57 $cvcl_298 ))) (iff x_52 (or x_53 $cvcl_299 ))) $cvcl_305) $cvcl_306) (and (and (and (and (and (and (and (and (and $cvcl_300 (or (or (or $cvcl_285 x_55 ) x_41 ) $cvcl_301 )) (or (or (or $cvcl_287 x_57 ) x_43 ) $cvcl_302 )) (or (or x_53 x_39 ) $cvcl_303 )) x_18) (= x_37 ?cvcl_304)) $cvcl_305) $cvcl_306) $cvcl_307) $cvcl_308) ) $cvcl_325) $cvcl_326) $cvcl_278) $cvcl_309) $cvcl_310) $cvcl_311) $cvcl_312) ) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_321 $cvcl_322) (not x_16)) (or (or (or $cvcl_285 x_47 ) x_41 ) (<= x_37 x_62) )) (or (or (or $cvcl_287 x_49 ) x_43 ) (<= x_37 x_63) )) (or (or x_45 x_39 ) (<= x_37 x_59) )) (or (or (or (and (and (and (and (not x_47) $cvcl_291) (< x_35 x_62)) $cvcl_314) $cvcl_315) (and (and (and (and (not x_49) $cvcl_293) (< x_35 x_63)) $cvcl_316) $cvcl_317) ) (and (and (and (not x_45) $cvcl_295) $cvcl_318) $cvcl_319) ) $cvcl_320 )) (iff x_46 (or x_47 (= x_62 x_37) ))) (iff x_48 (or x_49 (= x_63 x_37) ))) (iff x_44 (or x_45 (= x_59 x_37) ))) $cvcl_323) $cvcl_324) (and (and (and (and (and (and (and $cvcl_321 (not $cvcl_322)) x_16) $cvcl_323) $cvcl_324) (= x_37 x_35)) $cvcl_310) $cvcl_311) ) $cvcl_325) $cvcl_326) $cvcl_278) $cvcl_309) $cvcl_307) $cvcl_308) $cvcl_327) )) (or (or (and $cvcl_328 (= x_19 (ite (not x_12) x_14 1))) (and $cvcl_329 (= x_19 (ite (not x_13) x_14 2))) ) (and (and $cvcl_330 $cvcl_331) (= x_19 x_14)) )) (or (and (and $cvcl_332 (not (<= x_58 x_70))) (not (<= x_70 ?cvcl_333))) (and $cvcl_334 (= x_70 x_62)) )) (or (and (and $cvcl_332 (not (<= x_58 x_71))) (not (<= x_71 ?cvcl_333))) (and $cvcl_334 (= x_71 x_63)) )) (or (and (and $cvcl_332 (= x_58 (+ x_36 x_10))) x_72) (and (and $cvcl_334 (not x_72)) (= x_58 x_36)) )) (or (and (and (and (and $cvcl_337 $cvcl_335) $cvcl_336) (< x_73 x_74)) (< x_74 x_75)) (and (and (and (not $cvcl_337) (= x_73 x_59)) (= x_74 x_64)) (= x_75 x_67)) )) (or (not (<= x_132 2)) (not (<= x_133 2)) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )