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