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