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