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