(benchmark fs_window.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 :extrapreds ((x_0)) :extrafuns ((x_1 Real)) :extrafuns ((x_2 Real)) :extrafuns ((x_3 Real)) :extrapreds ((x_4)) :extrafuns ((x_5 Real)) :extrapreds ((x_6)) :extrafuns ((x_7 Real)) :extrapreds ((x_8)) :extrafuns ((x_9 Real)) :extrafuns ((x_10 Real)) :extrapreds ((x_11)) :extrafuns ((x_12 Real)) :extrapreds ((x_13)) :extrafuns ((x_14 Real)) :extrapreds ((x_15)) :extrafuns ((x_16 Real)) :extrafuns ((x_17 Real)) :extrapreds ((x_18)) :extrafuns ((x_19 Real)) :extrapreds ((x_20)) :extrafuns ((x_21 Real)) :extrapreds ((x_22)) :extrapreds ((x_23)) :extrafuns ((x_24 Real)) :extrapreds ((x_25)) :extrapreds ((x_26)) :extrapreds ((x_27)) :extrapreds ((x_28)) :extrapreds ((x_29)) :extrafuns ((x_30 Real)) :extrapreds ((x_31)) :extrapreds ((x_32)) :extrapreds ((x_33)) :extrapreds ((x_34)) :extrapreds ((x_35)) :extrafuns ((x_36 Real)) :extrapreds ((x_37)) :extrapreds ((x_38)) :extrapreds ((x_39)) :extrapreds ((x_40)) :extrapreds ((x_41)) :extrapreds ((x_42)) :extrafuns ((x_43 Real)) :extrapreds ((x_44)) :extrapreds ((x_45)) :extrapreds ((x_46)) :extrapreds ((x_47)) :extrapreds ((x_48)) :extrafuns ((x_49 Real)) :extrafuns ((x_50 Real)) :extrafuns ((x_51 Real)) :extrafuns ((x_52 Real)) :extrapreds ((x_53)) :extrapreds ((x_54)) :extrapreds ((x_55)) :extrapreds ((x_56)) :extrapreds ((x_57)) :extrapreds ((x_58)) :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)) :extrafuns ((x_68 Real)) :extrafuns ((x_69 Real)) :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)) :extrafuns ((x_77 Real)) :extrapreds ((x_78)) :extrafuns ((x_79 Real)) :extrafuns ((x_80 Real)) :extrafuns ((x_81 Real)) :extrapreds ((x_82)) :extrapreds ((x_83)) :extrapreds ((x_84)) :extrapreds ((x_85)) :extrafuns ((x_86 Real)) :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)) :extrafuns ((x_105 Real)) :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)) :extrafuns ((x_113 Real)) :extrafuns ((x_114 Real)) :extrapreds ((x_115)) :extrafuns ((x_116 Real)) :extrafuns ((x_117 Real)) :extrafuns ((x_118 Real)) :formula (flet ($cvcl_25 x_22) (flet ($cvcl_26 x_23) (flet ($cvcl_27 x_0) (flet ($cvcl_16 x_28) (flet ($cvcl_17 x_29) (flet ($cvcl_18 x_8) (flet ($cvcl_7 x_34) (flet ($cvcl_8 x_35) (flet ($cvcl_9 x_15) (flet ($cvcl_0 x_40) (flet ($cvcl_1 x_41) (flet ($cvcl_2 x_42) (let (?cvcl_217 (+ x_3 x_1)) (flet ($cvcl_266 (<= x_2 x_9)) (flet ($cvcl_247 (iff x_28 x_22)) (flet ($cvcl_190 (= x_30 0)) (flet ($cvcl_203 $cvcl_190) (flet ($cvcl_204 (< x_2 x_52)) (flet ($cvcl_231 (= x_9 x_2)) (flet ($cvcl_255 $cvcl_231) (flet ($cvcl_248 (= x_30 2)) (flet ($cvcl_256 $cvcl_248) (flet ($cvcl_258 (iff x_53 x_54)) (flet ($cvcl_259 (and (iff x_32 x_26) (iff x_33 x_27))) (flet ($cvcl_245 (iff x_55 x_56)) (flet ($cvcl_246 (and (iff x_57 x_58) (iff x_59 x_60))) (flet ($cvcl_260 (= x_61 x_62)) (flet ($cvcl_261 (and (= x_63 x_64) (= x_65 x_66))) (flet ($cvcl_214 (= x_67 x_52)) (flet ($cvcl_244 (iff x_29 x_23)) (flet ($cvcl_242 (iff x_31 x_25)) (flet ($cvcl_243 (and (iff x_11 x_4) (iff x_13 x_6))) (flet ($cvcl_262 (iff x_8 x_0)) (let (?cvcl_268 (- x_10 x_3)) (flet ($cvcl_191 (= x_30 1)) (flet ($cvcl_235 $cvcl_191) (let (?cvcl_239 (+ x_1 x_3)) (flet ($cvcl_234 (<= x_68 x_9)) (flet ($cvcl_241 (iff x_53 (or x_54 (and $cvcl_234 x_25) ))) (flet ($cvcl_221 (<= x_5 ?cvcl_217)) (flet ($cvcl_223 (<= x_7 ?cvcl_217)) (flet ($cvcl_215 (<= x_5 x_1)) (flet ($cvcl_220 $cvcl_215) (flet ($cvcl_216 (<= x_7 x_1)) (flet ($cvcl_222 $cvcl_216) (flet ($cvcl_32 (not x_26)) (flet ($cvcl_226 $cvcl_32) (flet ($cvcl_249 (< x_5 x_2)) (flet ($cvcl_250 (= x_9 x_5)) (flet ($cvcl_33 (not x_27)) (flet ($cvcl_228 $cvcl_33) (flet ($cvcl_251 (< x_7 x_2)) (flet ($cvcl_252 (= x_9 x_7)) (flet ($cvcl_207 (not x_54)) (flet ($cvcl_230 $cvcl_207) (flet ($cvcl_269 (not $cvcl_266)) (flet ($cvcl_29 (not x_4)) (flet ($cvcl_225 $cvcl_29) (flet ($cvcl_30 (not x_6)) (flet ($cvcl_227 $cvcl_30) (flet ($cvcl_218 (not x_25)) (flet ($cvcl_229 $cvcl_218) (flet ($cvcl_232 (and (not $cvcl_215) (<= x_5 x_9))) (flet ($cvcl_233 (and (not $cvcl_216) (<= x_7 x_9))) (flet ($cvcl_240 (and (iff x_32 (or x_26 (and $cvcl_232 x_4) )) (iff x_33 (or x_27 (and $cvcl_233 x_6) )))) (flet ($cvcl_224 (<= x_68 ?cvcl_217)) (flet ($cvcl_253 (< x_68 x_2)) (flet ($cvcl_254 (= x_9 x_68)) (flet ($cvcl_257 (<= (ite x_56 (ite x_60 (ite x_58 3 2) x_69) (ite x_60 x_69 (ite x_58 1 0))) (* (* (ite x_54 (ite x_27 (ite x_26 0 1) x_70) (ite x_27 x_70 (ite x_26 2 3))) 1) (/ 1 2)))) (flet ($cvcl_272 $cvcl_234) (flet ($cvcl_236 (not $cvcl_221)) (flet ($cvcl_237 (not $cvcl_223)) (flet ($cvcl_34 (and (not (<= x_68 x_1)) $cvcl_234)) (flet ($cvcl_35 $cvcl_34) (flet ($cvcl_38 (and (not (<= x_71 x_1)) (<= x_71 x_9))) (flet ($cvcl_36 $cvcl_38) (flet ($cvcl_39 $cvcl_34) (flet ($cvcl_40 $cvcl_38) (flet ($cvcl_238 (not $cvcl_224)) (let (?cvcl_144 (+ x_3 x_9)) (flet ($cvcl_193 (<= x_10 x_16)) (flet ($cvcl_174 (iff x_34 x_28)) (flet ($cvcl_119 (= x_36 0)) (flet ($cvcl_130 $cvcl_119) (flet ($cvcl_131 (< x_10 x_67)) (flet ($cvcl_158 (= x_16 x_10)) (flet ($cvcl_182 $cvcl_158) (flet ($cvcl_175 (= x_36 2)) (flet ($cvcl_183 $cvcl_175) (flet ($cvcl_185 (iff x_82 x_53)) (flet ($cvcl_186 (and (iff x_38 x_32) (iff x_39 x_33))) (flet ($cvcl_172 (iff x_83 x_55)) (flet ($cvcl_173 (and (iff x_84 x_57) (iff x_85 x_59))) (flet ($cvcl_187 (= x_86 x_61)) (flet ($cvcl_188 (and (= x_87 x_63) (= x_88 x_65))) (flet ($cvcl_141 (= x_89 x_67)) (flet ($cvcl_171 (iff x_35 x_29)) (flet ($cvcl_169 (iff x_37 x_31)) (flet ($cvcl_170 (and (iff x_18 x_11) (iff x_20 x_13))) (flet ($cvcl_189 (iff x_15 x_8)) (let (?cvcl_195 (- x_17 x_3)) (flet ($cvcl_120 (= x_36 1)) (flet ($cvcl_162 $cvcl_120) (let (?cvcl_166 (+ x_9 x_3)) (flet ($cvcl_161 (<= x_79 x_16)) (flet ($cvcl_168 (iff x_82 (or x_53 (and $cvcl_161 x_31) ))) (flet ($cvcl_148 (<= x_12 ?cvcl_144)) (flet ($cvcl_150 (<= x_14 ?cvcl_144)) (flet ($cvcl_142 (<= x_12 x_9)) (flet ($cvcl_147 $cvcl_142) (flet ($cvcl_143 (<= x_14 x_9)) (flet ($cvcl_149 $cvcl_143) (flet ($cvcl_23 (not x_32)) (flet ($cvcl_153 $cvcl_23) (flet ($cvcl_176 (< x_12 x_10)) (flet ($cvcl_177 (= x_16 x_12)) (flet ($cvcl_24 (not x_33)) (flet ($cvcl_155 $cvcl_24) (flet ($cvcl_178 (< x_14 x_10)) (flet ($cvcl_179 (= x_16 x_14)) (flet ($cvcl_134 (not x_53)) (flet ($cvcl_157 $cvcl_134) (flet ($cvcl_196 (not $cvcl_193)) (flet ($cvcl_20 (not x_11)) (flet ($cvcl_152 $cvcl_20) (flet ($cvcl_21 (not x_13)) (flet ($cvcl_154 $cvcl_21) (flet ($cvcl_145 (not x_31)) (flet ($cvcl_156 $cvcl_145) (flet ($cvcl_159 (and (not $cvcl_142) (<= x_12 x_16))) (flet ($cvcl_160 (and (not $cvcl_143) (<= x_14 x_16))) (flet ($cvcl_167 (and (iff x_38 (or x_32 (and $cvcl_159 x_11) )) (iff x_39 (or x_33 (and $cvcl_160 x_13) )))) (flet ($cvcl_151 (<= x_79 ?cvcl_144)) (flet ($cvcl_180 (< x_79 x_10)) (flet ($cvcl_181 (= x_16 x_79)) (flet ($cvcl_184 (<= (ite x_55 (ite x_59 (ite x_57 3 2) x_90) (ite x_59 x_90 (ite x_57 1 0))) (* (* (ite x_53 (ite x_33 (ite x_32 0 1) x_91) (ite x_33 x_91 (ite x_32 2 3))) 1) (/ 1 2)))) (flet ($cvcl_199 $cvcl_161) (flet ($cvcl_163 (not $cvcl_148)) (flet ($cvcl_164 (not $cvcl_150)) (flet ($cvcl_270 (not (<= x_79 x_9))) (flet ($cvcl_41 (and $cvcl_270 $cvcl_161)) (flet ($cvcl_42 $cvcl_41) (flet ($cvcl_271 (not (<= x_80 x_9))) (flet ($cvcl_45 (and $cvcl_271 (<= x_80 x_16))) (flet ($cvcl_43 $cvcl_45) (flet ($cvcl_46 $cvcl_41) (flet ($cvcl_47 $cvcl_45) (flet ($cvcl_165 (not $cvcl_151)) (let (?cvcl_74 (+ x_3 x_16)) (flet ($cvcl_122 (<= x_17 x_100)) (flet ($cvcl_103 (iff x_40 x_34)) (flet ($cvcl_55 (= x_43 0)) (flet ($cvcl_59 $cvcl_55) (flet ($cvcl_60 (< x_17 x_89)) (flet ($cvcl_87 (= x_100 x_17)) (flet ($cvcl_111 $cvcl_87) (flet ($cvcl_104 (= x_43 2)) (flet ($cvcl_112 $cvcl_104) (flet ($cvcl_114 (iff x_101 x_82)) (flet ($cvcl_115 (and (iff x_47 x_38) (iff x_48 x_39))) (flet ($cvcl_101 (iff x_102 x_83)) (flet ($cvcl_102 (and (iff x_103 x_84) (iff x_104 x_85))) (flet ($cvcl_116 (= x_105 x_86)) (flet ($cvcl_117 (and (= x_106 x_87) (= x_107 x_88))) (flet ($cvcl_70 (= x_108 x_89)) (flet ($cvcl_100 (iff x_41 x_35)) (flet ($cvcl_98 (iff x_46 x_37)) (flet ($cvcl_99 (and (iff x_44 x_18) (iff x_45 x_20))) (flet ($cvcl_118 (iff x_42 x_15)) (let (?cvcl_124 (- x_49 x_3)) (flet ($cvcl_71 (= x_43 1)) (flet ($cvcl_91 $cvcl_71) (let (?cvcl_95 (+ x_16 x_3)) (flet ($cvcl_90 (<= x_97 x_100)) (flet ($cvcl_97 (iff x_101 (or x_82 (and $cvcl_90 x_37) ))) (flet ($cvcl_77 (<= x_19 ?cvcl_74)) (flet ($cvcl_79 (<= x_21 ?cvcl_74)) (flet ($cvcl_72 (<= x_19 x_16)) (flet ($cvcl_76 $cvcl_72) (flet ($cvcl_73 (<= x_21 x_16)) (flet ($cvcl_78 $cvcl_73) (flet ($cvcl_14 (not x_38)) (flet ($cvcl_82 $cvcl_14) (flet ($cvcl_105 (< x_19 x_17)) (flet ($cvcl_106 (= x_100 x_19)) (flet ($cvcl_15 (not x_39)) (flet ($cvcl_84 $cvcl_15) (flet ($cvcl_107 (< x_21 x_17)) (flet ($cvcl_108 (= x_100 x_21)) (flet ($cvcl_63 (not x_82)) (flet ($cvcl_86 $cvcl_63) (flet ($cvcl_125 (not $cvcl_122)) (flet ($cvcl_11 (not x_18)) (flet ($cvcl_81 $cvcl_11) (flet ($cvcl_12 (not x_20)) (flet ($cvcl_83 $cvcl_12) (flet ($cvcl_75 (not x_37)) (flet ($cvcl_85 $cvcl_75) (flet ($cvcl_88 (and (not $cvcl_72) (<= x_19 x_100))) (flet ($cvcl_89 (and (not $cvcl_73) (<= x_21 x_100))) (flet ($cvcl_96 (and (iff x_47 (or x_38 (and $cvcl_88 x_18) )) (iff x_48 (or x_39 (and $cvcl_89 x_20) )))) (flet ($cvcl_80 (<= x_97 ?cvcl_74)) (flet ($cvcl_109 (< x_97 x_17)) (flet ($cvcl_110 (= x_100 x_97)) (flet ($cvcl_113 (<= (ite x_83 (ite x_85 (ite x_84 3 2) x_109) (ite x_85 x_109 (ite x_84 1 0))) (* (* (ite x_82 (ite x_39 (ite x_38 0 1) x_110) (ite x_39 x_110 (ite x_38 2 3))) 1) (/ 1 2)))) (flet ($cvcl_126 $cvcl_90) (flet ($cvcl_92 (not $cvcl_77)) (flet ($cvcl_93 (not $cvcl_79)) (flet ($cvcl_197 (not (<= x_97 x_16))) (flet ($cvcl_48 (and $cvcl_197 $cvcl_90)) (flet ($cvcl_49 $cvcl_48) (flet ($cvcl_198 (not (<= x_98 x_16))) (flet ($cvcl_52 (and $cvcl_198 (<= x_98 x_100))) (flet ($cvcl_50 $cvcl_52) (flet ($cvcl_53 $cvcl_48) (flet ($cvcl_54 $cvcl_52) (flet ($cvcl_94 (not $cvcl_80)) (flet ($cvcl_213 (= x_61 0)) (flet ($cvcl_202 (= x_61 3)) (flet ($cvcl_209 (= x_63 0)) (flet ($cvcl_200 (= x_63 3)) (flet ($cvcl_211 (= x_65 0)) (flet ($cvcl_201 (= x_65 3)) (flet ($cvcl_140 (= x_86 0)) (flet ($cvcl_129 (= x_86 3)) (flet ($cvcl_136 (= x_87 0)) (flet ($cvcl_127 (= x_87 3)) (flet ($cvcl_138 (= x_88 0)) (flet ($cvcl_128 (= x_88 3)) (flet ($cvcl_69 (= x_105 0)) (flet ($cvcl_58 (= x_105 3)) (flet ($cvcl_65 (= x_106 0)) (flet ($cvcl_56 (= x_106 3)) (flet ($cvcl_67 (= x_107 0)) (flet ($cvcl_57 (= x_107 3)) (flet ($cvcl_3 (not $cvcl_55)) (flet ($cvcl_4 (not $cvcl_71)) (flet ($cvcl_5 (not x_47)) (flet ($cvcl_6 (not x_48)) (flet ($cvcl_121 (not (<= x_49 x_50))) (flet ($cvcl_123 (not (<= x_49 x_51))) (flet ($cvcl_10 (not $cvcl_119)) (flet ($cvcl_13 (not $cvcl_120)) (flet ($cvcl_192 (not (<= x_17 x_19))) (flet ($cvcl_194 (not (<= x_17 x_21))) (flet ($cvcl_19 (not $cvcl_190)) (flet ($cvcl_22 (not $cvcl_191)) (flet ($cvcl_265 (not (<= x_10 x_12))) (flet ($cvcl_267 (not (<= x_10 x_14))) (flet ($cvcl_263 (= x_24 0)) (flet ($cvcl_28 (not $cvcl_263)) (flet ($cvcl_264 (= x_24 1)) (flet ($cvcl_31 (not $cvcl_264)) (flet ($cvcl_37 (and (not (<= x_74 x_1)) (<= x_74 x_9))) (flet ($cvcl_44 (and (not (<= x_81 x_9)) (<= x_81 x_16))) (flet ($cvcl_51 (and (not (<= x_99 x_16)) (<= x_99 x_100))) (flet ($cvcl_61 (= x_106 (ite $cvcl_14 (ite (and $cvcl_88 (< x_87 3)) (+ x_87 1) x_87) x_87))) (flet ($cvcl_62 (= x_107 (ite $cvcl_15 (ite (and $cvcl_89 (< x_88 3)) (+ x_88 1) x_88) x_88))) (flet ($cvcl_64 (or x_38 $cvcl_56 )) (flet ($cvcl_66 (or x_39 $cvcl_57 )) (flet ($cvcl_68 (or x_82 $cvcl_58 )) (flet ($cvcl_273 (not x_42)) (flet ($cvcl_146 (not x_15)) (flet ($cvcl_132 (= x_87 (ite $cvcl_23 (ite (and $cvcl_159 (< x_63 3)) (+ x_63 1) x_63) x_63))) (flet ($cvcl_133 (= x_88 (ite $cvcl_24 (ite (and $cvcl_160 (< x_65 3)) (+ x_65 1) x_65) x_65))) (flet ($cvcl_135 (or x_32 $cvcl_127 )) (flet ($cvcl_137 (or x_33 $cvcl_128 )) (flet ($cvcl_139 (or x_53 $cvcl_129 )) (flet ($cvcl_219 (not x_8)) (flet ($cvcl_205 (= x_63 (ite $cvcl_32 (ite (and $cvcl_232 (< x_64 3)) (+ x_64 1) x_64) x_64))) (flet ($cvcl_206 (= x_65 (ite $cvcl_33 (ite (and $cvcl_233 (< x_66 3)) (+ x_66 1) x_66) x_66))) (flet ($cvcl_208 (or x_26 $cvcl_200 )) (flet ($cvcl_210 (or x_27 $cvcl_201 )) (flet ($cvcl_212 (or x_54 $cvcl_202 )) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (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_43 2) (>= x_43 0)) (<= x_36 2)) (>= x_36 0)) (<= x_30 2)) (>= x_30 0)) (<= x_24 2)) (>= x_24 0)) (>= x_1 0)) (>= x_2 0)) (> x_3 0)) (>= x_3 0)) (>= x_5 0)) (>= x_7 0)) (>= x_9 0)) (>= x_10 0)) (>= x_12 0)) (>= x_14 0)) (>= x_16 0)) (>= x_17 0)) (>= x_19 0)) (>= x_21 0)) (>= x_49 0)) (>= x_50 0)) (>= x_51 0)) (>= x_52 0)) (or (or (or $cvcl_213 (= x_61 1) ) (= x_61 2) ) $cvcl_202 )) (not (< x_61 0))) (<= x_61 3)) (or (or (or (= x_62 0) (= x_62 1) ) (= x_62 2) ) (= x_62 3) )) (not (< x_62 0))) (<= x_62 3)) (or (or (or $cvcl_209 (= x_63 1) ) (= x_63 2) ) $cvcl_200 )) (not (< x_63 0))) (<= x_63 3)) (or (or (or (= x_64 0) (= x_64 1) ) (= x_64 2) ) (= x_64 3) )) (not (< x_64 0))) (<= x_64 3)) (or (or (or $cvcl_211 (= x_65 1) ) (= x_65 2) ) $cvcl_201 )) (not (< x_65 0))) (<= x_65 3)) (or (or (or (= x_66 0) (= x_66 1) ) (= x_66 2) ) (= x_66 3) )) (not (< x_66 0))) (<= x_66 3)) (>= x_67 0)) (>= x_68 0)) (>= x_71 0)) (>= x_74 0)) (not (<= x_77 (* x_3 3)))) (>= x_77 0)) (>= x_79 0)) (>= x_80 0)) (>= x_81 0)) (or (or (or $cvcl_140 (= x_86 1) ) (= x_86 2) ) $cvcl_129 )) (not (< x_86 0))) (<= x_86 3)) (or (or (or $cvcl_136 (= x_87 1) ) (= x_87 2) ) $cvcl_127 )) (not (< x_87 0))) (<= x_87 3)) (or (or (or $cvcl_138 (= x_88 1) ) (= x_88 2) ) $cvcl_128 )) (not (< x_88 0))) (<= x_88 3)) (>= x_89 0)) (>= x_97 0)) (>= x_98 0)) (>= x_99 0)) (>= x_100 0)) (or (or (or $cvcl_69 (= x_105 1) ) (= x_105 2) ) $cvcl_58 )) (not (< x_105 0))) (<= x_105 3)) (or (or (or $cvcl_65 (= x_106 1) ) (= x_106 2) ) $cvcl_56 )) (not (< x_106 0))) (<= x_106 3)) (or (or (or $cvcl_67 (= x_107 1) ) (= x_107 2) ) $cvcl_57 )) (not (< x_107 0))) (<= x_107 3)) (>= x_108 0)) (>= x_116 0)) (>= x_117 0)) (>= x_118 0)) (or (or x_15 (<= x_16 (- x_17 x_3)) ) (and (or (or $cvcl_11 (= x_16 x_19) ) (not (<= x_16 x_19)) ) (or (or $cvcl_12 (= x_16 x_21) ) (not (<= x_16 x_21)) )) )) (or (or x_8 (<= x_9 (- x_10 x_3)) ) (and (or (or $cvcl_20 (= x_9 x_12) ) (not (<= x_9 x_12)) ) (or (or $cvcl_21 (= x_9 x_14) ) (not (<= x_9 x_14)) )) )) (or (or x_0 (<= x_1 (- x_2 x_3)) ) (and (or (or $cvcl_29 (= x_1 x_5) ) (not (<= x_1 x_5)) ) (or (or $cvcl_30 (= x_1 x_7) ) (not (<= x_1 x_7)) )) )) (or $cvcl_3 (and $cvcl_2 $cvcl_0) )) (or $cvcl_4 (and $cvcl_1 $cvcl_0) )) (or (not $cvcl_104) (and $cvcl_1 $cvcl_2) )) (or $cvcl_3 (and (and (not x_44) (not x_45)) (not x_46)) )) (or $cvcl_4 (and (or x_44 $cvcl_5 ) (or x_45 $cvcl_6 )) )) (or $cvcl_3 (and $cvcl_5 $cvcl_6) )) $cvcl_121) $cvcl_123) (< (- x_49 x_50) x_3)) (< (- x_49 x_51) x_3)) (or $cvcl_10 (and $cvcl_9 $cvcl_7) )) (or $cvcl_13 (and $cvcl_8 $cvcl_7) )) (or (not $cvcl_175) (and $cvcl_8 $cvcl_9) )) (or $cvcl_10 (and (and $cvcl_11 $cvcl_12) $cvcl_75) )) (or $cvcl_13 (and (or x_18 $cvcl_14 ) (or x_20 $cvcl_15 )) )) (or $cvcl_10 (and $cvcl_14 $cvcl_15) )) $cvcl_192) $cvcl_194) (< (- x_17 x_19) x_3)) (< (- x_17 x_21) x_3)) (or $cvcl_19 (and $cvcl_18 $cvcl_16) )) (or $cvcl_22 (and $cvcl_17 $cvcl_16) )) (or (not $cvcl_248) (and $cvcl_17 $cvcl_18) )) (or $cvcl_19 (and (and $cvcl_20 $cvcl_21) $cvcl_145) )) (or $cvcl_22 (and (or x_11 $cvcl_23 ) (or x_13 $cvcl_24 )) )) (or $cvcl_19 (and $cvcl_23 $cvcl_24) )) $cvcl_265) $cvcl_267) (< (- x_10 x_12) x_3)) (< (- x_10 x_14) x_3)) (or $cvcl_28 (and $cvcl_27 $cvcl_25) )) (or $cvcl_31 (and $cvcl_26 $cvcl_25) )) (or (not (= x_24 2)) (and $cvcl_26 $cvcl_27) )) (or $cvcl_28 (and (and $cvcl_29 $cvcl_30) $cvcl_218) )) (or $cvcl_31 (and (or x_4 $cvcl_32 ) (or x_6 $cvcl_33 )) )) (or $cvcl_28 (and $cvcl_32 $cvcl_33) )) (not (<= x_2 x_5))) (not (<= x_2 x_7))) (< (- x_2 x_5) x_3)) (< (- x_2 x_7) x_3)) (= x_69 (ite x_58 2 1))) (= x_70 (ite x_26 1 2))) (= x_72 (ite $cvcl_35 2 1))) (= x_73 (ite $cvcl_39 2 1))) (= x_75 (+ (ite $cvcl_37 (ite $cvcl_36 (ite $cvcl_35 3 2) x_72) (ite $cvcl_36 x_72 (ite $cvcl_35 1 0))) x_62))) (= x_76 (+ (ite $cvcl_37 (ite $cvcl_40 (ite $cvcl_39 3 2) x_73) (ite $cvcl_40 x_73 (ite $cvcl_39 1 0))) x_62))) (= x_90 (ite x_57 2 1))) (= x_91 (ite x_32 1 2))) (= x_92 (ite $cvcl_42 2 1))) (= x_93 (ite $cvcl_46 2 1))) (= x_94 (+ (ite $cvcl_44 (ite $cvcl_43 (ite $cvcl_42 3 2) x_92) (ite $cvcl_43 x_92 (ite $cvcl_42 1 0))) x_61))) (= x_95 (+ (ite $cvcl_44 (ite $cvcl_47 (ite $cvcl_46 3 2) x_93) (ite $cvcl_47 x_93 (ite $cvcl_46 1 0))) x_61))) (= x_109 (ite x_84 2 1))) (= x_110 (ite x_38 1 2))) (= x_111 (ite $cvcl_49 2 1))) (= x_112 (ite $cvcl_53 2 1))) (= x_113 (+ (ite $cvcl_51 (ite $cvcl_50 (ite $cvcl_49 3 2) x_111) (ite $cvcl_50 x_111 (ite $cvcl_49 1 0))) x_86))) (= x_114 (+ (ite $cvcl_51 (ite $cvcl_54 (ite $cvcl_53 3 2) x_112) (ite $cvcl_54 x_112 (ite $cvcl_53 1 0))) x_86))) (or (or (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and $cvcl_59 $cvcl_60) $cvcl_87) $cvcl_61) $cvcl_62) (= x_105 (ite $cvcl_63 (ite (not (< x_113 3)) 3 x_113) x_86))) (iff x_47 $cvcl_64)) (iff x_48 $cvcl_66)) (iff x_101 $cvcl_68)) $cvcl_100) $cvcl_70) (and (and (and (and (and (and (and (and (and (and $cvcl_59 (not $cvcl_60)) x_41) (= x_100 x_89)) $cvcl_61) $cvcl_62) (= x_105 (ite $cvcl_63 (ite (not (< x_114 3)) 3 x_114) x_86))) (iff x_47 (or $cvcl_64 $cvcl_65 ))) (iff x_48 (or $cvcl_66 $cvcl_67 ))) (iff x_101 (or $cvcl_68 $cvcl_69 ))) $cvcl_70) ) $cvcl_98) $cvcl_99) $cvcl_118) $cvcl_101) $cvcl_102) $cvcl_103) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_91 (or (or (and (and (and (not $cvcl_76) $cvcl_82) $cvcl_81) $cvcl_77) (and (and (and (not $cvcl_78) $cvcl_84) $cvcl_83) $cvcl_79) ) (and (and $cvcl_86 $cvcl_85) $cvcl_80) )) $cvcl_273) (or (or (or (or $cvcl_76 $cvcl_92 ) x_18 ) x_38 ) (not (< x_100 x_19)) )) (or (or (or (or $cvcl_78 $cvcl_93 ) x_20 ) x_39 ) (not (< x_100 x_21)) )) (or (or (or $cvcl_94 x_37 ) x_82 ) (not (< x_100 x_97)) )) (or (or (or (and (and (and (and $cvcl_81 $cvcl_82) $cvcl_77) $cvcl_105) $cvcl_106) (and (and (and (and $cvcl_83 $cvcl_84) $cvcl_79) $cvcl_107) $cvcl_108) ) (and (and (and (and $cvcl_85 $cvcl_86) $cvcl_80) $cvcl_109) $cvcl_110) ) (and (< x_17 ?cvcl_95) $cvcl_111) )) (iff x_44 (or x_18 $cvcl_88 ))) (iff x_45 (or x_20 $cvcl_89 ))) (iff x_46 (or x_37 $cvcl_90 ))) $cvcl_96) $cvcl_97) (and (and (and (and (and (and (and (and (and $cvcl_91 (or (or (or $cvcl_76 x_18 ) x_38 ) $cvcl_92 )) (or (or (or $cvcl_78 x_20 ) x_39 ) $cvcl_93 )) (or (or x_37 x_82 ) $cvcl_94 )) x_42) (= x_100 ?cvcl_95)) $cvcl_96) $cvcl_97) $cvcl_98) $cvcl_99) ) $cvcl_116) $cvcl_117) $cvcl_70) $cvcl_100) $cvcl_101) $cvcl_102) $cvcl_103) ) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_112 $cvcl_113) (not x_40)) (or (or (or $cvcl_76 x_84 ) x_38 ) (<= x_100 x_19) )) (or (or (or $cvcl_78 x_85 ) x_39 ) (<= x_100 x_21) )) (or (or x_83 x_82 ) (<= x_100 x_97) )) (or (or (or (and (and (and (and (not x_84) $cvcl_82) (< x_16 x_19)) $cvcl_105) $cvcl_106) (and (and (and (and (not x_85) $cvcl_84) (< x_16 x_21)) $cvcl_107) $cvcl_108) ) (and (and (and (not x_83) $cvcl_86) $cvcl_109) $cvcl_110) ) $cvcl_111 )) (iff x_103 (or x_84 (= x_19 x_100) ))) (iff x_104 (or x_85 (= x_21 x_100) ))) (iff x_102 (or x_83 (= x_97 x_100) ))) $cvcl_114) $cvcl_115) (and (and (and (and (and (and (and $cvcl_112 (not $cvcl_113)) x_40) $cvcl_114) $cvcl_115) (= x_100 x_16)) $cvcl_101) $cvcl_102) ) $cvcl_116) $cvcl_117) $cvcl_70) $cvcl_100) $cvcl_98) $cvcl_99) $cvcl_118) )) (or (or (and $cvcl_119 (= x_43 (ite (not x_35) x_36 1))) (and $cvcl_120 (= x_43 (ite $cvcl_146 x_36 2))) ) (and (and $cvcl_10 $cvcl_13) (= x_43 x_36)) )) (or (and (and $cvcl_122 $cvcl_121) (not (<= x_50 ?cvcl_124))) (and $cvcl_125 (= x_50 x_19)) )) (or (and (and $cvcl_122 $cvcl_123) (not (<= x_51 ?cvcl_124))) (and $cvcl_125 (= x_51 x_21)) )) (or (and (and $cvcl_122 (= x_49 (+ x_17 x_77))) x_115) (and (and $cvcl_125 (not x_115)) (= x_49 x_17)) )) (or (and (and (and (and $cvcl_126 (not (<= x_116 x_100))) (not (<= x_117 x_100))) (< x_116 x_117)) (< x_117 x_118)) (and (and (and (not $cvcl_126) (= x_116 x_97)) (= x_117 x_98)) (= x_118 x_99)) )) (or (or (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and $cvcl_130 $cvcl_131) $cvcl_158) $cvcl_132) $cvcl_133) (= x_86 (ite $cvcl_134 (ite (not (< x_94 3)) 3 x_94) x_61))) (iff x_38 $cvcl_135)) (iff x_39 $cvcl_137)) (iff x_82 $cvcl_139)) $cvcl_171) $cvcl_141) (and (and (and (and (and (and (and (and (and (and $cvcl_130 (not $cvcl_131)) x_35) (= x_16 x_67)) $cvcl_132) $cvcl_133) (= x_86 (ite $cvcl_134 (ite (not (< x_95 3)) 3 x_95) x_61))) (iff x_38 (or $cvcl_135 $cvcl_136 ))) (iff x_39 (or $cvcl_137 $cvcl_138 ))) (iff x_82 (or $cvcl_139 $cvcl_140 ))) $cvcl_141) ) $cvcl_169) $cvcl_170) $cvcl_189) $cvcl_172) $cvcl_173) $cvcl_174) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_162 (or (or (and (and (and (not $cvcl_147) $cvcl_153) $cvcl_152) $cvcl_148) (and (and (and (not $cvcl_149) $cvcl_155) $cvcl_154) $cvcl_150) ) (and (and $cvcl_157 $cvcl_156) $cvcl_151) )) $cvcl_146) (or (or (or (or $cvcl_147 $cvcl_163 ) x_11 ) x_32 ) (not (< x_16 x_12)) )) (or (or (or (or $cvcl_149 $cvcl_164 ) x_13 ) x_33 ) (not (< x_16 x_14)) )) (or (or (or $cvcl_165 x_31 ) x_53 ) (not (< x_16 x_79)) )) (or (or (or (and (and (and (and $cvcl_152 $cvcl_153) $cvcl_148) $cvcl_176) $cvcl_177) (and (and (and (and $cvcl_154 $cvcl_155) $cvcl_150) $cvcl_178) $cvcl_179) ) (and (and (and (and $cvcl_156 $cvcl_157) $cvcl_151) $cvcl_180) $cvcl_181) ) (and (< x_10 ?cvcl_166) $cvcl_182) )) (iff x_18 (or x_11 $cvcl_159 ))) (iff x_20 (or x_13 $cvcl_160 ))) (iff x_37 (or x_31 $cvcl_161 ))) $cvcl_167) $cvcl_168) (and (and (and (and (and (and (and (and (and $cvcl_162 (or (or (or $cvcl_147 x_11 ) x_32 ) $cvcl_163 )) (or (or (or $cvcl_149 x_13 ) x_33 ) $cvcl_164 )) (or (or x_31 x_53 ) $cvcl_165 )) x_15) (= x_16 ?cvcl_166)) $cvcl_167) $cvcl_168) $cvcl_169) $cvcl_170) ) $cvcl_187) $cvcl_188) $cvcl_141) $cvcl_171) $cvcl_172) $cvcl_173) $cvcl_174) ) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_183 $cvcl_184) (not x_34)) (or (or (or $cvcl_147 x_57 ) x_32 ) (<= x_16 x_12) )) (or (or (or $cvcl_149 x_59 ) x_33 ) (<= x_16 x_14) )) (or (or x_55 x_53 ) (<= x_16 x_79) )) (or (or (or (and (and (and (and (not x_57) $cvcl_153) (< x_9 x_12)) $cvcl_176) $cvcl_177) (and (and (and (and (not x_59) $cvcl_155) (< x_9 x_14)) $cvcl_178) $cvcl_179) ) (and (and (and (not x_55) $cvcl_157) $cvcl_180) $cvcl_181) ) $cvcl_182 )) (iff x_84 (or x_57 (= x_12 x_16) ))) (iff x_85 (or x_59 (= x_14 x_16) ))) (iff x_83 (or x_55 (= x_79 x_16) ))) $cvcl_185) $cvcl_186) (and (and (and (and (and (and (and $cvcl_183 (not $cvcl_184)) x_34) $cvcl_185) $cvcl_186) (= x_16 x_9)) $cvcl_172) $cvcl_173) ) $cvcl_187) $cvcl_188) $cvcl_141) $cvcl_171) $cvcl_169) $cvcl_170) $cvcl_189) )) (or (or (and $cvcl_190 (= x_36 (ite (not x_29) x_30 1))) (and $cvcl_191 (= x_36 (ite $cvcl_219 x_30 2))) ) (and (and $cvcl_19 $cvcl_22) (= x_36 x_30)) )) (or (and (and $cvcl_193 $cvcl_192) (not (<= x_19 ?cvcl_195))) (and $cvcl_196 (= x_19 x_12)) )) (or (and (and $cvcl_193 $cvcl_194) (not (<= x_21 ?cvcl_195))) (and $cvcl_196 (= x_21 x_14)) )) (or (and (and $cvcl_193 (= x_17 (+ x_10 x_77))) x_96) (and (and $cvcl_196 (not x_96)) (= x_17 x_10)) )) (or (and (and (and (and $cvcl_199 $cvcl_197) $cvcl_198) (< x_97 x_98)) (< x_98 x_99)) (and (and (and (not $cvcl_199) (= x_97 x_79)) (= x_98 x_80)) (= x_99 x_81)) )) (or (or (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and $cvcl_203 $cvcl_204) $cvcl_231) $cvcl_205) $cvcl_206) (= x_61 (ite $cvcl_207 (ite (not (< x_75 3)) 3 x_75) x_62))) (iff x_32 $cvcl_208)) (iff x_33 $cvcl_210)) (iff x_53 $cvcl_212)) $cvcl_244) $cvcl_214) (and (and (and (and (and (and (and (and (and (and $cvcl_203 (not $cvcl_204)) x_29) (= x_9 x_52)) $cvcl_205) $cvcl_206) (= x_61 (ite $cvcl_207 (ite (not (< x_76 3)) 3 x_76) x_62))) (iff x_32 (or $cvcl_208 $cvcl_209 ))) (iff x_33 (or $cvcl_210 $cvcl_211 ))) (iff x_53 (or $cvcl_212 $cvcl_213 ))) $cvcl_214) ) $cvcl_242) $cvcl_243) $cvcl_262) $cvcl_245) $cvcl_246) $cvcl_247) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_235 (or (or (and (and (and (not $cvcl_220) $cvcl_226) $cvcl_225) $cvcl_221) (and (and (and (not $cvcl_222) $cvcl_228) $cvcl_227) $cvcl_223) ) (and (and $cvcl_230 $cvcl_229) $cvcl_224) )) $cvcl_219) (or (or (or (or $cvcl_220 $cvcl_236 ) x_4 ) x_26 ) (not (< x_9 x_5)) )) (or (or (or (or $cvcl_222 $cvcl_237 ) x_6 ) x_27 ) (not (< x_9 x_7)) )) (or (or (or $cvcl_238 x_25 ) x_54 ) (not (< x_9 x_68)) )) (or (or (or (and (and (and (and $cvcl_225 $cvcl_226) $cvcl_221) $cvcl_249) $cvcl_250) (and (and (and (and $cvcl_227 $cvcl_228) $cvcl_223) $cvcl_251) $cvcl_252) ) (and (and (and (and $cvcl_229 $cvcl_230) $cvcl_224) $cvcl_253) $cvcl_254) ) (and (< x_2 ?cvcl_239) $cvcl_255) )) (iff x_11 (or x_4 $cvcl_232 ))) (iff x_13 (or x_6 $cvcl_233 ))) (iff x_31 (or x_25 $cvcl_234 ))) $cvcl_240) $cvcl_241) (and (and (and (and (and (and (and (and (and $cvcl_235 (or (or (or $cvcl_220 x_4 ) x_26 ) $cvcl_236 )) (or (or (or $cvcl_222 x_6 ) x_27 ) $cvcl_237 )) (or (or x_25 x_54 ) $cvcl_238 )) x_8) (= x_9 ?cvcl_239)) $cvcl_240) $cvcl_241) $cvcl_242) $cvcl_243) ) $cvcl_260) $cvcl_261) $cvcl_214) $cvcl_244) $cvcl_245) $cvcl_246) $cvcl_247) ) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_256 $cvcl_257) (not x_28)) (or (or (or $cvcl_220 x_58 ) x_26 ) (<= x_9 x_5) )) (or (or (or $cvcl_222 x_60 ) x_27 ) (<= x_9 x_7) )) (or (or x_56 x_54 ) (<= x_9 x_68) )) (or (or (or (and (and (and (and (not x_58) $cvcl_226) (< x_1 x_5)) $cvcl_249) $cvcl_250) (and (and (and (and (not x_60) $cvcl_228) (< x_1 x_7)) $cvcl_251) $cvcl_252) ) (and (and (and (not x_56) $cvcl_230) $cvcl_253) $cvcl_254) ) $cvcl_255 )) (iff x_57 (or x_58 (= x_5 x_9) ))) (iff x_59 (or x_60 (= x_7 x_9) ))) (iff x_55 (or x_56 (= x_68 x_9) ))) $cvcl_258) $cvcl_259) (and (and (and (and (and (and (and $cvcl_256 (not $cvcl_257)) x_28) $cvcl_258) $cvcl_259) (= x_9 x_1)) $cvcl_245) $cvcl_246) ) $cvcl_260) $cvcl_261) $cvcl_214) $cvcl_244) $cvcl_242) $cvcl_243) $cvcl_262) )) (or (or (and $cvcl_263 (= x_30 (ite (not x_23) x_24 1))) (and $cvcl_264 (= x_30 (ite (not x_0) x_24 2))) ) (and (and $cvcl_28 $cvcl_31) (= x_30 x_24)) )) (or (and (and $cvcl_266 $cvcl_265) (not (<= x_12 ?cvcl_268))) (and $cvcl_269 (= x_12 x_5)) )) (or (and (and $cvcl_266 $cvcl_267) (not (<= x_14 ?cvcl_268))) (and $cvcl_269 (= x_14 x_7)) )) (or (and (and $cvcl_266 (= x_10 (+ x_2 x_77))) x_78) (and (and $cvcl_269 (not x_78)) (= x_10 x_2)) )) (or (and (and (and (and $cvcl_272 $cvcl_270) $cvcl_271) (< x_79 x_80)) (< x_80 x_81)) (and (and (and (not $cvcl_272) (= x_79 x_68)) (= x_80 x_71)) (= x_81 x_74)) )) $cvcl_273) (not (<= x_100 (- x_49 x_3)))) (or (and (and x_44 (not (= x_100 x_50))) (<= x_100 x_50)) (and (and x_45 (not (= x_100 x_51))) (<= x_100 x_51)) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )