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