(benchmark Carpark2_t1_4.smt :source { SAL benchmark suite. Created at SRI by Bruno Dutertre, John Rushby, Maria Sorea, and Leonardo de Moura. Contact demoura@csl.sri.com for more information. This benchmark was automatically translated into SMT-LIB format from CVC format using CVC Lite } :status unknown :logic QF_LRA :extrasorts (ANY) :extrapreds ((x_0)) :extrapreds ((x_1)) :extrapreds ((x_2)) :extrapreds ((x_3)) :extrapreds ((x_4)) :extrapreds ((x_5)) :extrapreds ((x_6)) :extrapreds ((x_7)) :extrapreds ((x_8)) :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)) :extrapreds ((x_20)) :extrafuns ((x_21 Real)) :extrafuns ((x_22 Real)) :extrapreds ((x_23)) :extrapreds ((x_24)) :extrapreds ((x_25)) :extrafuns ((x_26 Real)) :extrapreds ((x_27)) :extrafuns ((x_28 Real)) :extrafuns ((x_29 Real)) :extrafuns ((x_30 Real)) :extrapreds ((x_31)) :extrapreds ((x_32)) :extrapreds ((x_33)) :extrafuns ((x_34 Real)) :extrapreds ((x_35)) :extrapreds ((x_36)) :extrapreds ((x_37)) :extrafuns ((x_38 Real)) :extrapreds ((x_39)) :extrapreds ((x_40)) :extrapreds ((x_41)) :extrapreds ((x_42)) :extrapreds ((x_43)) :extrapreds ((x_44)) :extrapreds ((x_45)) :extrapreds ((x_46)) :extrapreds ((x_47)) :extrafuns ((x_48 Real)) :extrapreds ((x_49)) :extrapreds ((x_50)) :extrafuns ((x_51 Real)) :extrapreds ((x_52)) :extrafuns ((x_53 Real)) :extrapreds ((x_54)) :extrafuns ((x_55 Real)) :extrapreds ((x_56)) :extrapreds ((x_57)) :extrafuns ((x_58 Real)) :extrafuns ((x_59 Real)) :extrapreds ((x_60)) :extrafuns ((x_61 Real)) :extrapreds ((x_62)) :extrapreds ((x_63)) :extrafuns ((x_64 Real)) :extrafuns ((x_65 Real)) :extrafuns ((x_66 Real)) :extrafuns ((x_67 Real)) :extrapreds ((x_68)) :extrafuns ((x_69 Real)) :extrafuns ((x_70 Real)) :extrapreds ((x_71)) :extrafuns ((x_72 Real)) :extrapreds ((x_73)) :extrafuns ((x_74 Real)) :extrapreds ((x_75)) :extrapreds ((x_76)) :extrapreds ((x_77)) :extrafuns ((x_78 Real)) :extrapreds ((x_79)) :extrapreds ((x_80)) :extrapreds ((x_81)) :extrapreds ((x_82)) :extrapreds ((x_83)) :extrapreds ((x_84)) :extrapreds ((x_85)) :extrapreds ((x_86)) :extrapreds ((x_87)) :extrafuns ((x_88 Real)) :extrapreds ((x_89)) :extrapreds ((x_90)) :extrafuns ((x_91 Real)) :extrapreds ((x_92)) :extrafuns ((x_93 Real)) :extrapreds ((x_94)) :extrafuns ((x_95 Real)) :extrapreds ((x_96)) :extrapreds ((x_97)) :extrafuns ((x_98 Real)) :extrafuns ((x_99 Real)) :extrapreds ((x_100)) :extrafuns ((x_101 Real)) :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)) :extrafuns ((x_109 Real)) :extrafuns ((x_110 Real)) :extrapreds ((x_111)) :extrafuns ((x_112 Real)) :extrapreds ((x_113)) :extrafuns ((x_114 Real)) :extrapreds ((x_115)) :extrapreds ((x_116)) :extrapreds ((x_117)) :extrafuns ((x_118 Real)) :extrapreds ((x_119)) :extrapreds ((x_120)) :extrapreds ((x_121)) :extrapreds ((x_122)) :extrapreds ((x_123)) :extrapreds ((x_124)) :extrapreds ((x_125)) :extrapreds ((x_126)) :extrapreds ((x_127)) :extrafuns ((x_128 Real)) :extrapreds ((x_129)) :extrapreds ((x_130)) :extrafuns ((x_131 Real)) :extrapreds ((x_132)) :extrafuns ((x_133 Real)) :extrapreds ((x_134)) :extrafuns ((x_135 Real)) :extrapreds ((x_136)) :extrapreds ((x_137)) :extrafuns ((x_138 Real)) :extrafuns ((x_139 Real)) :extrapreds ((x_140)) :extrafuns ((x_141 Real)) :extrapreds ((x_142)) :extrapreds ((x_143)) :extrafuns ((x_144 Real)) :extrafuns ((x_145 Real)) :extrafuns ((x_146 Real)) :extrafuns ((x_147 Real)) :extrapreds ((x_148)) :extrafuns ((x_149 Real)) :extrafuns ((x_150 Real)) :extrapreds ((x_151)) :extrafuns ((x_152 Real)) :extrapreds ((x_153)) :extrafuns ((x_154 Real)) :extrapreds ((x_155)) :extrapreds ((x_156)) :extrapreds ((x_157)) :extrafuns ((x_158 Real)) :extrapreds ((x_159)) :extrapreds ((x_160)) :extrapreds ((x_161)) :extrapreds ((x_162)) :extrapreds ((x_163)) :extrapreds ((x_164)) :extrapreds ((x_165)) :extrapreds ((x_166)) :extrapreds ((x_167)) :extrafuns ((x_168 Real)) :extrapreds ((x_169)) :extrapreds ((x_170)) :extrafuns ((x_171 Real)) :extrapreds ((x_172)) :extrafuns ((x_173 Real)) :extrapreds ((x_174)) :extrafuns ((x_175 Real)) :extrapreds ((x_176)) :extrapreds ((x_177)) :extrafuns ((x_178 Real)) :extrafuns ((x_179 Real)) :extrapreds ((x_180)) :extrafuns ((x_181 Real)) :extrapreds ((x_182)) :extrapreds ((x_183)) :extrafuns ((x_184 Real)) :extrafuns ((x_185 Real)) :extrafuns ((x_186 Real)) :extrafuns ((x_187 Real)) :extrapreds ((x_188)) :extrafuns ((x_189 Real)) :extrafuns ((x_190 Real)) :extrapreds ((x_191)) :extrafuns ((x_192 Real)) :formula (flet ($cvcl_34 (< x_133 20)) (flet ($cvcl_32 (< x_133 50)) (flet ($cvcl_62 (<= x_131 x_139)) (flet ($cvcl_25 (< x_114 x_145)) (flet ($cvcl_26 (iff x_153 false)) (flet ($cvcl_19 (not x_129)) (flet ($cvcl_24 (and $cvcl_19 x_130)) (flet ($cvcl_23 (= x_154 x_114)) (flet ($cvcl_63 (not x_156)) (flet ($cvcl_68 (and x_155 $cvcl_63)) (flet ($cvcl_29 (and (iff x_157 false) (= x_158 x_10))) (flet ($cvcl_67 (not x_115)) (flet ($cvcl_58 (not x_116)) (flet ($cvcl_61 (and $cvcl_67 $cvcl_58)) (flet ($cvcl_2 (not x_160)) (flet ($cvcl_4 (and x_159 $cvcl_2)) (flet ($cvcl_3 (not x_161)) (flet ($cvcl_10 (and (and $cvcl_4 $cvcl_3) x_162)) (flet ($cvcl_5 (or x_159 x_160 )) (flet ($cvcl_1 (not x_162)) (flet ($cvcl_6 (and x_159 x_160)) (flet ($cvcl_11 (and (and $cvcl_6 x_161) $cvcl_1)) (flet ($cvcl_7 (or x_159 $cvcl_2 )) (flet ($cvcl_13 (and (and $cvcl_4 x_161) $cvcl_1)) (flet ($cvcl_15 (and (and $cvcl_6 $cvcl_3) $cvcl_1)) (flet ($cvcl_37 (or $cvcl_10 (and (or (or $cvcl_5 x_161 ) $cvcl_1 ) (or $cvcl_11 (and (or (or $cvcl_7 $cvcl_3 ) x_162 ) (or $cvcl_13 (and (or (or $cvcl_5 $cvcl_3 ) x_162 ) (or $cvcl_15 (and (and (and (and (or (or $cvcl_7 x_161 ) x_162 ) x_159) $cvcl_2) $cvcl_3) $cvcl_1) )) )) )) )) (flet ($cvcl_8 (and (and (and (iff x_163 false) (iff x_164 x_5)) (iff x_165 x_6)) (iff x_166 x_7))) (flet ($cvcl_55 (= x_168 x_10)) (flet ($cvcl_60 (and (iff x_167 false) $cvcl_55)) (flet ($cvcl_0 (not x_130)) (flet ($cvcl_41 (or $cvcl_19 $cvcl_0 )) (flet ($cvcl_39 (or x_129 $cvcl_0 )) (flet ($cvcl_28 (not x_170)) (flet ($cvcl_20 (and x_169 $cvcl_28)) (flet ($cvcl_52 (not x_136)) (flet ($cvcl_56 (or $cvcl_52 x_137 )) (flet ($cvcl_43 (< x_133 10)) (flet ($cvcl_30 (and x_129 x_130)) (flet ($cvcl_65 (= x_171 x_131)) (flet ($cvcl_45 (not x_137)) (flet ($cvcl_49 (and x_136 $cvcl_45)) (flet ($cvcl_47 (iff x_172 false)) (flet ($cvcl_40 (<= x_133 0)) (flet ($cvcl_18 (= x_173 x_133)) (flet ($cvcl_48 (and (iff x_174 false) (= x_175 x_10))) (flet ($cvcl_54 (not x_177)) (flet ($cvcl_46 (and x_176 $cvcl_54)) (flet ($cvcl_51 (= x_178 x_138)) (flet ($cvcl_69 (or x_115 x_116 )) (flet ($cvcl_66 (= x_179 x_139)) (flet ($cvcl_64 (and (iff x_180 false) (= x_181 x_10))) (flet ($cvcl_9 (iff x_182 false)) (flet ($cvcl_50 (and (iff x_183 false) (= x_184 x_10))) (flet ($cvcl_22 (= x_185 x_145)) (flet ($cvcl_31 (and x_169 x_170)) (flet ($cvcl_21 (iff x_153 true)) (flet ($cvcl_102 (< x_93 20)) (flet ($cvcl_100 (< x_93 50)) (flet ($cvcl_126 (<= x_91 x_99)) (flet ($cvcl_96 (< x_74 x_105)) (flet ($cvcl_97 (iff x_113 false)) (flet ($cvcl_90 (not x_89)) (flet ($cvcl_95 (and $cvcl_90 x_90)) (flet ($cvcl_94 (= x_114 x_74)) (flet ($cvcl_131 (and x_115 $cvcl_58)) (flet ($cvcl_98 (and (iff x_117 false) (= x_118 x_10))) (flet ($cvcl_130 (not x_75)) (flet ($cvcl_123 (not x_76)) (flet ($cvcl_125 (and $cvcl_130 $cvcl_123)) (flet ($cvcl_73 (not x_120)) (flet ($cvcl_75 (and x_119 $cvcl_73)) (flet ($cvcl_74 (not x_121)) (flet ($cvcl_81 (and (and $cvcl_75 $cvcl_74) x_122)) (flet ($cvcl_76 (or x_119 x_120 )) (flet ($cvcl_72 (not x_122)) (flet ($cvcl_77 (and x_119 x_120)) (flet ($cvcl_82 (and (and $cvcl_77 x_121) $cvcl_72)) (flet ($cvcl_78 (or x_119 $cvcl_73 )) (flet ($cvcl_84 (and (and $cvcl_75 x_121) $cvcl_72)) (flet ($cvcl_86 (and (and $cvcl_77 $cvcl_74) $cvcl_72)) (flet ($cvcl_105 (or $cvcl_81 (and (or (or $cvcl_76 x_121 ) $cvcl_72 ) (or $cvcl_82 (and (or (or $cvcl_78 $cvcl_74 ) x_122 ) (or $cvcl_84 (and (or (or $cvcl_76 $cvcl_74 ) x_122 ) (or $cvcl_86 (and (and (and (and (or (or $cvcl_78 x_121 ) x_122 ) x_119) $cvcl_73) $cvcl_74) $cvcl_72) )) )) )) )) (flet ($cvcl_79 (and (and (and (iff x_123 false) (iff x_124 x_5)) (iff x_125 x_6)) (iff x_126 x_7))) (flet ($cvcl_120 (= x_128 x_10)) (flet ($cvcl_124 (and (iff x_127 false) $cvcl_120)) (flet ($cvcl_71 (not x_90)) (flet ($cvcl_109 (or $cvcl_90 $cvcl_71 )) (flet ($cvcl_107 (or x_89 $cvcl_71 )) (flet ($cvcl_91 (and x_129 $cvcl_0)) (flet ($cvcl_119 (not x_96)) (flet ($cvcl_121 (or $cvcl_119 x_97 )) (flet ($cvcl_111 (< x_93 10)) (flet ($cvcl_99 (and x_89 x_90)) (flet ($cvcl_128 (= x_131 x_91)) (flet ($cvcl_113 (not x_97)) (flet ($cvcl_116 (and x_96 $cvcl_113)) (flet ($cvcl_114 (iff x_132 false)) (flet ($cvcl_108 (<= x_93 0)) (flet ($cvcl_89 (= x_133 x_93)) (flet ($cvcl_115 (and (iff x_134 false) (= x_135 x_10))) (flet ($cvcl_118 (= x_138 x_98)) (flet ($cvcl_132 (or x_75 x_76 )) (flet ($cvcl_129 (= x_139 x_99)) (flet ($cvcl_127 (and (iff x_140 false) (= x_141 x_10))) (flet ($cvcl_80 (iff x_142 false)) (flet ($cvcl_117 (and (iff x_143 false) (= x_144 x_10))) (flet ($cvcl_93 (= x_145 x_105)) (flet ($cvcl_92 (iff x_113 true)) (flet ($cvcl_165 (< x_53 20)) (flet ($cvcl_163 (< x_53 50)) (flet ($cvcl_189 (<= x_51 x_59)) (flet ($cvcl_159 (< x_34 x_65)) (flet ($cvcl_160 (iff x_73 false)) (flet ($cvcl_153 (not x_49)) (flet ($cvcl_158 (and $cvcl_153 x_50)) (flet ($cvcl_157 (= x_74 x_34)) (flet ($cvcl_194 (and x_75 $cvcl_123)) (flet ($cvcl_161 (and (iff x_77 false) (= x_78 x_10))) (flet ($cvcl_193 (not x_35)) (flet ($cvcl_186 (not x_36)) (flet ($cvcl_188 (and $cvcl_193 $cvcl_186)) (flet ($cvcl_136 (not x_80)) (flet ($cvcl_138 (and x_79 $cvcl_136)) (flet ($cvcl_137 (not x_81)) (flet ($cvcl_144 (and (and $cvcl_138 $cvcl_137) x_82)) (flet ($cvcl_139 (or x_79 x_80 )) (flet ($cvcl_135 (not x_82)) (flet ($cvcl_140 (and x_79 x_80)) (flet ($cvcl_145 (and (and $cvcl_140 x_81) $cvcl_135)) (flet ($cvcl_141 (or x_79 $cvcl_136 )) (flet ($cvcl_147 (and (and $cvcl_138 x_81) $cvcl_135)) (flet ($cvcl_149 (and (and $cvcl_140 $cvcl_137) $cvcl_135)) (flet ($cvcl_168 (or $cvcl_144 (and (or (or $cvcl_139 x_81 ) $cvcl_135 ) (or $cvcl_145 (and (or (or $cvcl_141 $cvcl_137 ) x_82 ) (or $cvcl_147 (and (or (or $cvcl_139 $cvcl_137 ) x_82 ) (or $cvcl_149 (and (and (and (and (or (or $cvcl_141 x_81 ) x_82 ) x_79) $cvcl_136) $cvcl_137) $cvcl_135) )) )) )) )) (flet ($cvcl_142 (and (and (and (iff x_83 false) (iff x_84 x_5)) (iff x_85 x_6)) (iff x_86 x_7))) (flet ($cvcl_183 (= x_88 x_10)) (flet ($cvcl_187 (and (iff x_87 false) $cvcl_183)) (flet ($cvcl_134 (not x_50)) (flet ($cvcl_172 (or $cvcl_153 $cvcl_134 )) (flet ($cvcl_170 (or x_49 $cvcl_134 )) (flet ($cvcl_154 (and x_89 $cvcl_71)) (flet ($cvcl_182 (not x_56)) (flet ($cvcl_184 (or $cvcl_182 x_57 )) (flet ($cvcl_174 (< x_53 10)) (flet ($cvcl_162 (and x_49 x_50)) (flet ($cvcl_191 (= x_91 x_51)) (flet ($cvcl_176 (not x_57)) (flet ($cvcl_179 (and x_56 $cvcl_176)) (flet ($cvcl_177 (iff x_92 false)) (flet ($cvcl_171 (<= x_53 0)) (flet ($cvcl_152 (= x_93 x_53)) (flet ($cvcl_178 (and (iff x_94 false) (= x_95 x_10))) (flet ($cvcl_181 (= x_98 x_58)) (flet ($cvcl_195 (or x_35 x_36 )) (flet ($cvcl_192 (= x_99 x_59)) (flet ($cvcl_190 (and (iff x_100 false) (= x_101 x_10))) (flet ($cvcl_143 (iff x_102 false)) (flet ($cvcl_180 (and (iff x_103 false) (= x_104 x_10))) (flet ($cvcl_156 (= x_105 x_65)) (flet ($cvcl_155 (iff x_73 true)) (flet ($cvcl_228 (< x_12 20)) (flet ($cvcl_226 (< x_12 50)) (flet ($cvcl_252 (<= x_29 x_30)) (flet ($cvcl_222 (< x_13 x_14)) (flet ($cvcl_223 (iff x_33 false)) (flet ($cvcl_197 (not x_15)) (flet ($cvcl_221 (and $cvcl_197 x_16)) (flet ($cvcl_220 (= x_34 x_13)) (flet ($cvcl_257 (and x_35 $cvcl_186)) (flet ($cvcl_224 (and (iff x_37 false) (= x_38 x_10))) (flet ($cvcl_256 (not x_31)) (flet ($cvcl_249 (not x_32)) (flet ($cvcl_251 (and $cvcl_256 $cvcl_249)) (flet ($cvcl_200 (not x_40)) (flet ($cvcl_202 (and x_39 $cvcl_200)) (flet ($cvcl_201 (not x_41)) (flet ($cvcl_208 (and (and $cvcl_202 $cvcl_201) x_42)) (flet ($cvcl_203 (or x_39 x_40 )) (flet ($cvcl_199 (not x_42)) (flet ($cvcl_204 (and x_39 x_40)) (flet ($cvcl_209 (and (and $cvcl_204 x_41) $cvcl_199)) (flet ($cvcl_205 (or x_39 $cvcl_200 )) (flet ($cvcl_211 (and (and $cvcl_202 x_41) $cvcl_199)) (flet ($cvcl_213 (and (and $cvcl_204 $cvcl_201) $cvcl_199)) (flet ($cvcl_231 (or $cvcl_208 (and (or (or $cvcl_203 x_41 ) $cvcl_199 ) (or $cvcl_209 (and (or (or $cvcl_205 $cvcl_201 ) x_42 ) (or $cvcl_211 (and (or (or $cvcl_203 $cvcl_201 ) x_42 ) (or $cvcl_213 (and (and (and (and (or (or $cvcl_205 x_41 ) x_42 ) x_39) $cvcl_200) $cvcl_201) $cvcl_199) )) )) )) )) (flet ($cvcl_206 (and (and (and (iff x_43 false) (iff x_44 x_5)) (iff x_45 x_6)) (iff x_46 x_7))) (flet ($cvcl_246 (= x_48 x_10)) (flet ($cvcl_250 (and (iff x_47 false) $cvcl_246)) (flet ($cvcl_198 (not x_16)) (flet ($cvcl_235 (or $cvcl_197 $cvcl_198 )) (flet ($cvcl_233 (or x_15 $cvcl_198 )) (flet ($cvcl_217 (and x_49 $cvcl_134)) (flet ($cvcl_239 (not x_23)) (flet ($cvcl_247 (or $cvcl_239 x_24 )) (flet ($cvcl_237 (< x_12 10)) (flet ($cvcl_225 (and x_15 x_16)) (flet ($cvcl_254 (= x_51 x_29)) (flet ($cvcl_240 (not x_24)) (flet ($cvcl_243 (and x_23 $cvcl_240)) (flet ($cvcl_241 (iff x_52 false)) (flet ($cvcl_234 (<= x_12 0)) (flet ($cvcl_216 (= x_53 x_12)) (flet ($cvcl_242 (and (iff x_54 false) (= x_55 x_10))) (flet ($cvcl_245 (= x_58 x_22)) (flet ($cvcl_259 (or x_31 x_32 )) (flet ($cvcl_255 (= x_59 x_30)) (flet ($cvcl_253 (and (iff x_60 false) (= x_61 x_10))) (flet ($cvcl_207 (iff x_62 false)) (flet ($cvcl_244 (and (iff x_63 false) (= x_64 x_10))) (flet ($cvcl_219 (= x_65 x_14)) (flet ($cvcl_218 (iff x_33 true)) (flet ($cvcl_261 (not x_11)) (flet ($cvcl_258 (not x_20)) (flet ($cvcl_27 (not x_169)) (flet ($cvcl_12 (not x_159)) (flet ($cvcl_14 (and $cvcl_12 $cvcl_2)) (flet ($cvcl_16 (and $cvcl_12 x_160)) (let (?cvcl_17 (ite $cvcl_10 4 (ite (and (and $cvcl_14 $cvcl_3) x_162) 4 (ite $cvcl_11 3 (ite (and (and $cvcl_16 x_161) $cvcl_1) 3 (ite $cvcl_13 2 (ite (and (and $cvcl_14 x_161) $cvcl_1) 2 (ite $cvcl_15 1 (ite (and (and $cvcl_16 $cvcl_3) $cvcl_1) 1 0))))))))) (flet ($cvcl_35 (not x_164)) (flet ($cvcl_33 (not x_166)) (flet ($cvcl_36 (not x_165)) (flet ($cvcl_57 (not x_167)) (flet ($cvcl_53 (not x_176)) (flet ($cvcl_59 (not x_155)) (flet ($cvcl_83 (not x_119)) (flet ($cvcl_85 (and $cvcl_83 $cvcl_73)) (flet ($cvcl_87 (and $cvcl_83 x_120)) (let (?cvcl_88 (ite $cvcl_81 4 (ite (and (and $cvcl_85 $cvcl_74) x_122) 4 (ite $cvcl_82 3 (ite (and (and $cvcl_87 x_121) $cvcl_72) 3 (ite $cvcl_84 2 (ite (and (and $cvcl_85 x_121) $cvcl_72) 2 (ite $cvcl_86 1 (ite (and (and $cvcl_87 $cvcl_74) $cvcl_72) 1 0))))))))) (flet ($cvcl_103 (not x_124)) (flet ($cvcl_101 (not x_126)) (flet ($cvcl_104 (not x_125)) (flet ($cvcl_122 (not x_127)) (flet ($cvcl_146 (not x_79)) (flet ($cvcl_148 (and $cvcl_146 $cvcl_136)) (flet ($cvcl_150 (and $cvcl_146 x_80)) (let (?cvcl_151 (ite $cvcl_144 4 (ite (and (and $cvcl_148 $cvcl_137) x_82) 4 (ite $cvcl_145 3 (ite (and (and $cvcl_150 x_81) $cvcl_135) 3 (ite $cvcl_147 2 (ite (and (and $cvcl_148 x_81) $cvcl_135) 2 (ite $cvcl_149 1 (ite (and (and $cvcl_150 $cvcl_137) $cvcl_135) 1 0))))))))) (flet ($cvcl_166 (not x_84)) (flet ($cvcl_164 (not x_86)) (flet ($cvcl_167 (not x_85)) (flet ($cvcl_185 (not x_87)) (flet ($cvcl_210 (not x_39)) (flet ($cvcl_212 (and $cvcl_210 $cvcl_200)) (flet ($cvcl_214 (and $cvcl_210 x_40)) (let (?cvcl_215 (ite $cvcl_208 4 (ite (and (and $cvcl_212 $cvcl_201) x_42) 4 (ite $cvcl_209 3 (ite (and (and $cvcl_214 x_41) $cvcl_199) 3 (ite $cvcl_211 2 (ite (and (and $cvcl_212 x_41) $cvcl_199) 2 (ite $cvcl_213 1 (ite (and (and $cvcl_214 $cvcl_201) $cvcl_199) 1 0))))))))) (flet ($cvcl_229 (not x_44)) (flet ($cvcl_227 (not x_46)) (flet ($cvcl_230 (not x_45)) (flet ($cvcl_248 (not x_47)) (flet ($cvcl_38 (not $cvcl_25)) (flet ($cvcl_42 (not $cvcl_32)) (flet ($cvcl_44 (not $cvcl_34)) (flet ($cvcl_70 (not $cvcl_62)) (flet ($cvcl_106 (not $cvcl_96)) (flet ($cvcl_110 (not $cvcl_100)) (flet ($cvcl_112 (not $cvcl_102)) (flet ($cvcl_133 (not $cvcl_126)) (flet ($cvcl_169 (not $cvcl_159)) (flet ($cvcl_173 (not $cvcl_163)) (flet ($cvcl_175 (not $cvcl_165)) (flet ($cvcl_196 (not $cvcl_189)) (flet ($cvcl_232 (not $cvcl_222)) (flet ($cvcl_236 (not $cvcl_226)) (flet ($cvcl_238 (not $cvcl_228)) (flet ($cvcl_260 (not $cvcl_252)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not x_0) true) (not x_1)) (and (and (iff x_2 x_5) (iff x_3 x_6)) (iff x_4 x_7))) (not x_8)) (= x_9 x_10)) $cvcl_261) true) (= x_12 0)) (= x_13 0)) (= x_14 0)) (and $cvcl_197 $cvcl_198)) (not x_17)) true) (not x_18)) (= x_19 x_10)) $cvcl_258) (= x_21 x_10)) (= x_22 0)) (and $cvcl_239 x_24)) (not x_25)) (= x_26 x_10)) (not x_27)) (= x_28 x_10)) (= x_29 0)) (= x_30 0)) (and x_31 $cvcl_249)) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (= x_186 0) $cvcl_19) $cvcl_0) x_180) $cvcl_20) x_157) (= x_158 x_181)) $cvcl_21) $cvcl_8) $cvcl_9) (= x_185 x_181)) $cvcl_18) $cvcl_23) (and (and (and (and (and (and (and (and (and (and (and (and (= x_186 1) x_129) $cvcl_0) $cvcl_37) $cvcl_27) x_170) $cvcl_8) $cvcl_26) $cvcl_29) $cvcl_9) (= x_154 (+ x_114 (* (ite (= ?cvcl_17 4) 20 (ite (= ?cvcl_17 3) 10 (ite (= ?cvcl_17 2) 5 (ite (= ?cvcl_17 1) 2 1)))) 10)))) $cvcl_22) $cvcl_18) ) (and (and (and (and (and (and (and (and (and (and (and (= x_186 2) $cvcl_24) $cvcl_25) $cvcl_20) $cvcl_21) x_157) (= x_158 (- x_145 x_114))) $cvcl_8) $cvcl_9) $cvcl_22) $cvcl_18) $cvcl_23) ) (and (and (and (and (and (and (and (and (and (and (and (= x_186 3) $cvcl_24) $cvcl_38) $cvcl_31) x_157) (= x_158 0)) x_182) $cvcl_8) $cvcl_26) (= x_173 (- x_114 x_145))) $cvcl_22) $cvcl_23) ) (and (and (and (and (and (and (and (and (and (and (and (= x_186 4) $cvcl_30) $cvcl_40) $cvcl_27) $cvcl_28) $cvcl_8) $cvcl_26) $cvcl_29) $cvcl_9) (= x_154 0)) (= x_173 0)) (= x_185 0)) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_186 5) $cvcl_30) $cvcl_42) $cvcl_31) x_163) $cvcl_35) x_165) $cvcl_33) $cvcl_26) $cvcl_29) $cvcl_9) (= x_173 (- x_133 50))) $cvcl_22) $cvcl_23) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_186 6) $cvcl_30) $cvcl_44) $cvcl_32) $cvcl_31) x_163) x_164) $cvcl_36) $cvcl_33) $cvcl_26) $cvcl_29) $cvcl_9) (= x_173 (- x_133 20))) $cvcl_22) $cvcl_23) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_186 7) $cvcl_30) (not $cvcl_43)) $cvcl_34) $cvcl_31) x_163) $cvcl_35) $cvcl_36) $cvcl_33) $cvcl_26) $cvcl_29) $cvcl_9) (= x_173 (- x_133 10))) $cvcl_22) $cvcl_23) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_186 8) (or (or x_129 x_130 ) (not x_180) )) (or (or $cvcl_19 x_130 ) (not $cvcl_37) )) (or $cvcl_39 $cvcl_38 )) (or $cvcl_39 $cvcl_25 )) (or $cvcl_41 (not $cvcl_40) )) (or $cvcl_41 $cvcl_32 )) (or (or $cvcl_41 $cvcl_34 ) $cvcl_42 )) (or (or $cvcl_41 $cvcl_43 ) $cvcl_44 )) $cvcl_26) $cvcl_8) $cvcl_29) $cvcl_9) (iff x_169 x_129)) (iff x_170 x_130)) $cvcl_22) $cvcl_18) $cvcl_23) )) (or (or (or (or (and (and (and (and (and (and (and (and (= x_187 0) $cvcl_52) $cvcl_45) x_188) $cvcl_46) $cvcl_47) $cvcl_50) $cvcl_48) (= x_178 x_189)) (and (and (and (and (and (and (and (and (and (= x_187 1) $cvcl_49) $cvcl_57) $cvcl_55) $cvcl_46) x_183) (= x_184 x_138)) $cvcl_47) $cvcl_48) $cvcl_51) ) (and (and (and (and (and (and (and (and (and (= x_187 2) $cvcl_49) x_167) $cvcl_53) x_177) x_174) (= x_175 x_168)) $cvcl_47) $cvcl_50) $cvcl_51) ) (and (and (and (and (and (and (and (and (= x_187 3) $cvcl_52) x_137) $cvcl_53) $cvcl_54) x_172) $cvcl_50) $cvcl_48) $cvcl_51) ) (and (and (and (and (and (and (and (and (and (and (= x_187 4) (or (or x_136 x_137 ) (not x_188) )) (or (or $cvcl_56 x_167 ) (not $cvcl_55) )) (or $cvcl_56 $cvcl_57 )) (or x_136 $cvcl_45 )) $cvcl_47) $cvcl_48) $cvcl_50) (iff x_176 x_136)) (iff x_177 x_137)) $cvcl_51) )) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_190 0) x_115) $cvcl_58) x_143) x_191) $cvcl_59) $cvcl_63) $cvcl_64) $cvcl_60) (= x_171 x_192)) (= x_179 x_144)) (and (and (and (and (and (and (and (and (and (= x_190 1) $cvcl_61) $cvcl_70) $cvcl_59) x_156) x_180) (= x_181 (* (- x_131 x_139) 10))) $cvcl_60) $cvcl_65) $cvcl_66) ) (and (and (and (and (and (and (and (and (= x_190 2) $cvcl_61) $cvcl_62) $cvcl_68) x_167) (= x_168 x_139)) $cvcl_64) $cvcl_65) $cvcl_66) ) (and (and (and (and (and (and (and (and (and (= x_190 3) $cvcl_67) x_116) x_142) $cvcl_68) x_167) (= x_168 (+ x_131 10))) $cvcl_64) $cvcl_65) $cvcl_66) ) (and (and (and (and (and (and (and (and (and (and (= x_190 4) (or (or (or $cvcl_67 x_116 ) (not x_143) ) (not x_191) )) (or $cvcl_69 $cvcl_62 )) (or $cvcl_69 $cvcl_70 )) (or (or x_115 $cvcl_58 ) (not x_142) )) $cvcl_60) $cvcl_64) (iff x_155 x_115)) (iff x_156 x_116)) $cvcl_65) $cvcl_66) )) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (= x_146 0) $cvcl_90) $cvcl_71) x_140) $cvcl_91) x_117) (= x_118 x_141)) $cvcl_92) $cvcl_79) $cvcl_80) (= x_145 x_141)) $cvcl_89) $cvcl_94) (and (and (and (and (and (and (and (and (and (and (and (and (= x_146 1) x_89) $cvcl_71) $cvcl_105) $cvcl_19) x_130) $cvcl_79) $cvcl_97) $cvcl_98) $cvcl_80) (= x_114 (+ x_74 (* (ite (= ?cvcl_88 4) 20 (ite (= ?cvcl_88 3) 10 (ite (= ?cvcl_88 2) 5 (ite (= ?cvcl_88 1) 2 1)))) 10)))) $cvcl_93) $cvcl_89) ) (and (and (and (and (and (and (and (and (and (and (and (= x_146 2) $cvcl_95) $cvcl_96) $cvcl_91) $cvcl_92) x_117) (= x_118 (- x_105 x_74))) $cvcl_79) $cvcl_80) $cvcl_93) $cvcl_89) $cvcl_94) ) (and (and (and (and (and (and (and (and (and (and (and (= x_146 3) $cvcl_95) $cvcl_106) $cvcl_30) x_117) (= x_118 0)) x_142) $cvcl_79) $cvcl_97) (= x_133 (- x_74 x_105))) $cvcl_93) $cvcl_94) ) (and (and (and (and (and (and (and (and (and (and (and (= x_146 4) $cvcl_99) $cvcl_108) $cvcl_19) $cvcl_0) $cvcl_79) $cvcl_97) $cvcl_98) $cvcl_80) (= x_114 0)) (= x_133 0)) (= x_145 0)) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_146 5) $cvcl_99) $cvcl_110) $cvcl_30) x_123) $cvcl_103) x_125) $cvcl_101) $cvcl_97) $cvcl_98) $cvcl_80) (= x_133 (- x_93 50))) $cvcl_93) $cvcl_94) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_146 6) $cvcl_99) $cvcl_112) $cvcl_100) $cvcl_30) x_123) x_124) $cvcl_104) $cvcl_101) $cvcl_97) $cvcl_98) $cvcl_80) (= x_133 (- x_93 20))) $cvcl_93) $cvcl_94) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_146 7) $cvcl_99) (not $cvcl_111)) $cvcl_102) $cvcl_30) x_123) $cvcl_103) $cvcl_104) $cvcl_101) $cvcl_97) $cvcl_98) $cvcl_80) (= x_133 (- x_93 10))) $cvcl_93) $cvcl_94) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_146 8) (or (or x_89 x_90 ) (not x_140) )) (or (or $cvcl_90 x_90 ) (not $cvcl_105) )) (or $cvcl_107 $cvcl_106 )) (or $cvcl_107 $cvcl_96 )) (or $cvcl_109 (not $cvcl_108) )) (or $cvcl_109 $cvcl_100 )) (or (or $cvcl_109 $cvcl_102 ) $cvcl_110 )) (or (or $cvcl_109 $cvcl_111 ) $cvcl_112 )) $cvcl_97) $cvcl_79) $cvcl_98) $cvcl_80) (iff x_129 x_89)) (iff x_130 x_90)) $cvcl_93) $cvcl_89) $cvcl_94) )) (or (or (or (or (and (and (and (and (and (and (and (and (= x_147 0) $cvcl_119) $cvcl_113) x_148) $cvcl_49) $cvcl_114) $cvcl_117) $cvcl_115) (= x_138 x_149)) (and (and (and (and (and (and (and (and (and (= x_147 1) $cvcl_116) $cvcl_122) $cvcl_120) $cvcl_49) x_143) (= x_144 x_98)) $cvcl_114) $cvcl_115) $cvcl_118) ) (and (and (and (and (and (and (and (and (and (= x_147 2) $cvcl_116) x_127) $cvcl_52) x_137) x_134) (= x_135 x_128)) $cvcl_114) $cvcl_117) $cvcl_118) ) (and (and (and (and (and (and (and (and (= x_147 3) $cvcl_119) x_97) $cvcl_52) $cvcl_45) x_132) $cvcl_117) $cvcl_115) $cvcl_118) ) (and (and (and (and (and (and (and (and (and (and (= x_147 4) (or (or x_96 x_97 ) (not x_148) )) (or (or $cvcl_121 x_127 ) (not $cvcl_120) )) (or $cvcl_121 $cvcl_122 )) (or x_96 $cvcl_113 )) $cvcl_114) $cvcl_115) $cvcl_117) (iff x_136 x_96)) (iff x_137 x_97)) $cvcl_118) )) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_150 0) x_75) $cvcl_123) x_103) x_151) $cvcl_67) $cvcl_58) $cvcl_127) $cvcl_124) (= x_131 x_152)) (= x_139 x_104)) (and (and (and (and (and (and (and (and (and (= x_150 1) $cvcl_125) $cvcl_133) $cvcl_67) x_116) x_140) (= x_141 (* (- x_91 x_99) 10))) $cvcl_124) $cvcl_128) $cvcl_129) ) (and (and (and (and (and (and (and (and (= x_150 2) $cvcl_125) $cvcl_126) $cvcl_131) x_127) (= x_128 x_99)) $cvcl_127) $cvcl_128) $cvcl_129) ) (and (and (and (and (and (and (and (and (and (= x_150 3) $cvcl_130) x_76) x_102) $cvcl_131) x_127) (= x_128 (+ x_91 10))) $cvcl_127) $cvcl_128) $cvcl_129) ) (and (and (and (and (and (and (and (and (and (and (= x_150 4) (or (or (or $cvcl_130 x_76 ) (not x_103) ) (not x_151) )) (or $cvcl_132 $cvcl_126 )) (or $cvcl_132 $cvcl_133 )) (or (or x_75 $cvcl_123 ) (not x_102) )) $cvcl_124) $cvcl_127) (iff x_115 x_75)) (iff x_116 x_76)) $cvcl_128) $cvcl_129) )) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (= x_106 0) $cvcl_153) $cvcl_134) x_100) $cvcl_154) x_77) (= x_78 x_101)) $cvcl_155) $cvcl_142) $cvcl_143) (= x_105 x_101)) $cvcl_152) $cvcl_157) (and (and (and (and (and (and (and (and (and (and (and (and (= x_106 1) x_49) $cvcl_134) $cvcl_168) $cvcl_90) x_90) $cvcl_142) $cvcl_160) $cvcl_161) $cvcl_143) (= x_74 (+ x_34 (* (ite (= ?cvcl_151 4) 20 (ite (= ?cvcl_151 3) 10 (ite (= ?cvcl_151 2) 5 (ite (= ?cvcl_151 1) 2 1)))) 10)))) $cvcl_156) $cvcl_152) ) (and (and (and (and (and (and (and (and (and (and (and (= x_106 2) $cvcl_158) $cvcl_159) $cvcl_154) $cvcl_155) x_77) (= x_78 (- x_65 x_34))) $cvcl_142) $cvcl_143) $cvcl_156) $cvcl_152) $cvcl_157) ) (and (and (and (and (and (and (and (and (and (and (and (= x_106 3) $cvcl_158) $cvcl_169) $cvcl_99) x_77) (= x_78 0)) x_102) $cvcl_142) $cvcl_160) (= x_93 (- x_34 x_65))) $cvcl_156) $cvcl_157) ) (and (and (and (and (and (and (and (and (and (and (and (= x_106 4) $cvcl_162) $cvcl_171) $cvcl_90) $cvcl_71) $cvcl_142) $cvcl_160) $cvcl_161) $cvcl_143) (= x_74 0)) (= x_93 0)) (= x_105 0)) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_106 5) $cvcl_162) $cvcl_173) $cvcl_99) x_83) $cvcl_166) x_85) $cvcl_164) $cvcl_160) $cvcl_161) $cvcl_143) (= x_93 (- x_53 50))) $cvcl_156) $cvcl_157) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_106 6) $cvcl_162) $cvcl_175) $cvcl_163) $cvcl_99) x_83) x_84) $cvcl_167) $cvcl_164) $cvcl_160) $cvcl_161) $cvcl_143) (= x_93 (- x_53 20))) $cvcl_156) $cvcl_157) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_106 7) $cvcl_162) (not $cvcl_174)) $cvcl_165) $cvcl_99) x_83) $cvcl_166) $cvcl_167) $cvcl_164) $cvcl_160) $cvcl_161) $cvcl_143) (= x_93 (- x_53 10))) $cvcl_156) $cvcl_157) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_106 8) (or (or x_49 x_50 ) (not x_100) )) (or (or $cvcl_153 x_50 ) (not $cvcl_168) )) (or $cvcl_170 $cvcl_169 )) (or $cvcl_170 $cvcl_159 )) (or $cvcl_172 (not $cvcl_171) )) (or $cvcl_172 $cvcl_163 )) (or (or $cvcl_172 $cvcl_165 ) $cvcl_173 )) (or (or $cvcl_172 $cvcl_174 ) $cvcl_175 )) $cvcl_160) $cvcl_142) $cvcl_161) $cvcl_143) (iff x_89 x_49)) (iff x_90 x_50)) $cvcl_156) $cvcl_152) $cvcl_157) )) (or (or (or (or (and (and (and (and (and (and (and (and (= x_107 0) $cvcl_182) $cvcl_176) x_108) $cvcl_116) $cvcl_177) $cvcl_180) $cvcl_178) (= x_98 x_109)) (and (and (and (and (and (and (and (and (and (= x_107 1) $cvcl_179) $cvcl_185) $cvcl_183) $cvcl_116) x_103) (= x_104 x_58)) $cvcl_177) $cvcl_178) $cvcl_181) ) (and (and (and (and (and (and (and (and (and (= x_107 2) $cvcl_179) x_87) $cvcl_119) x_97) x_94) (= x_95 x_88)) $cvcl_177) $cvcl_180) $cvcl_181) ) (and (and (and (and (and (and (and (and (= x_107 3) $cvcl_182) x_57) $cvcl_119) $cvcl_113) x_92) $cvcl_180) $cvcl_178) $cvcl_181) ) (and (and (and (and (and (and (and (and (and (and (= x_107 4) (or (or x_56 x_57 ) (not x_108) )) (or (or $cvcl_184 x_87 ) (not $cvcl_183) )) (or $cvcl_184 $cvcl_185 )) (or x_56 $cvcl_176 )) $cvcl_177) $cvcl_178) $cvcl_180) (iff x_96 x_56)) (iff x_97 x_57)) $cvcl_181) )) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_110 0) x_35) $cvcl_186) x_63) x_111) $cvcl_130) $cvcl_123) $cvcl_190) $cvcl_187) (= x_91 x_112)) (= x_99 x_64)) (and (and (and (and (and (and (and (and (and (= x_110 1) $cvcl_188) $cvcl_196) $cvcl_130) x_76) x_100) (= x_101 (* (- x_51 x_59) 10))) $cvcl_187) $cvcl_191) $cvcl_192) ) (and (and (and (and (and (and (and (and (= x_110 2) $cvcl_188) $cvcl_189) $cvcl_194) x_87) (= x_88 x_59)) $cvcl_190) $cvcl_191) $cvcl_192) ) (and (and (and (and (and (and (and (and (and (= x_110 3) $cvcl_193) x_36) x_62) $cvcl_194) x_87) (= x_88 (+ x_51 10))) $cvcl_190) $cvcl_191) $cvcl_192) ) (and (and (and (and (and (and (and (and (and (and (= x_110 4) (or (or (or $cvcl_193 x_36 ) (not x_63) ) (not x_111) )) (or $cvcl_195 $cvcl_189 )) (or $cvcl_195 $cvcl_196 )) (or (or x_35 $cvcl_186 ) (not x_62) )) $cvcl_187) $cvcl_190) (iff x_75 x_35)) (iff x_76 x_36)) $cvcl_191) $cvcl_192) )) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (= x_66 0) $cvcl_197) $cvcl_198) x_60) $cvcl_217) x_37) (= x_38 x_61)) $cvcl_218) $cvcl_206) $cvcl_207) (= x_65 x_61)) $cvcl_216) $cvcl_220) (and (and (and (and (and (and (and (and (and (and (and (and (= x_66 1) x_15) $cvcl_198) $cvcl_231) $cvcl_153) x_50) $cvcl_206) $cvcl_223) $cvcl_224) $cvcl_207) (= x_34 (+ x_13 (* (ite (= ?cvcl_215 4) 20 (ite (= ?cvcl_215 3) 10 (ite (= ?cvcl_215 2) 5 (ite (= ?cvcl_215 1) 2 1)))) 10)))) $cvcl_219) $cvcl_216) ) (and (and (and (and (and (and (and (and (and (and (and (= x_66 2) $cvcl_221) $cvcl_222) $cvcl_217) $cvcl_218) x_37) (= x_38 (- x_14 x_13))) $cvcl_206) $cvcl_207) $cvcl_219) $cvcl_216) $cvcl_220) ) (and (and (and (and (and (and (and (and (and (and (and (= x_66 3) $cvcl_221) $cvcl_232) $cvcl_162) x_37) (= x_38 0)) x_62) $cvcl_206) $cvcl_223) (= x_53 (- x_13 x_14))) $cvcl_219) $cvcl_220) ) (and (and (and (and (and (and (and (and (and (and (and (= x_66 4) $cvcl_225) $cvcl_234) $cvcl_153) $cvcl_134) $cvcl_206) $cvcl_223) $cvcl_224) $cvcl_207) (= x_34 0)) (= x_53 0)) (= x_65 0)) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_66 5) $cvcl_225) $cvcl_236) $cvcl_162) x_43) $cvcl_229) x_45) $cvcl_227) $cvcl_223) $cvcl_224) $cvcl_207) (= x_53 (- x_12 50))) $cvcl_219) $cvcl_220) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_66 6) $cvcl_225) $cvcl_238) $cvcl_226) $cvcl_162) x_43) x_44) $cvcl_230) $cvcl_227) $cvcl_223) $cvcl_224) $cvcl_207) (= x_53 (- x_12 20))) $cvcl_219) $cvcl_220) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_66 7) $cvcl_225) (not $cvcl_237)) $cvcl_228) $cvcl_162) x_43) $cvcl_229) $cvcl_230) $cvcl_227) $cvcl_223) $cvcl_224) $cvcl_207) (= x_53 (- x_12 10))) $cvcl_219) $cvcl_220) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_66 8) (or (or x_15 x_16 ) (not x_60) )) (or (or $cvcl_197 x_16 ) (not $cvcl_231) )) (or $cvcl_233 $cvcl_232 )) (or $cvcl_233 $cvcl_222 )) (or $cvcl_235 (not $cvcl_234) )) (or $cvcl_235 $cvcl_226 )) (or (or $cvcl_235 $cvcl_228 ) $cvcl_236 )) (or (or $cvcl_235 $cvcl_237 ) $cvcl_238 )) $cvcl_223) $cvcl_206) $cvcl_224) $cvcl_207) (iff x_49 x_15)) (iff x_50 x_16)) $cvcl_219) $cvcl_216) $cvcl_220) )) (or (or (or (or (and (and (and (and (and (and (and (and (= x_67 0) $cvcl_239) $cvcl_240) x_68) $cvcl_179) $cvcl_241) $cvcl_244) $cvcl_242) (= x_58 x_69)) (and (and (and (and (and (and (and (and (and (= x_67 1) $cvcl_243) $cvcl_248) $cvcl_246) $cvcl_179) x_63) (= x_64 x_22)) $cvcl_241) $cvcl_242) $cvcl_245) ) (and (and (and (and (and (and (and (and (and (= x_67 2) $cvcl_243) x_47) $cvcl_182) x_57) x_54) (= x_55 x_48)) $cvcl_241) $cvcl_244) $cvcl_245) ) (and (and (and (and (and (and (and (and (= x_67 3) $cvcl_239) x_24) $cvcl_182) $cvcl_176) x_52) $cvcl_244) $cvcl_242) $cvcl_245) ) (and (and (and (and (and (and (and (and (and (and (= x_67 4) (or (or x_23 x_24 ) (not x_68) )) (or (or $cvcl_247 x_47 ) (not $cvcl_246) )) (or $cvcl_247 $cvcl_248 )) (or x_23 $cvcl_240 )) $cvcl_241) $cvcl_242) $cvcl_244) (iff x_56 x_23)) (iff x_57 x_24)) $cvcl_245) )) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_70 0) x_31) $cvcl_249) x_20) x_71) $cvcl_193) $cvcl_186) $cvcl_253) $cvcl_250) (= x_51 x_72)) (= x_59 x_21)) (and (and (and (and (and (and (and (and (and (= x_70 1) $cvcl_251) $cvcl_260) $cvcl_193) x_36) x_60) (= x_61 (* (- x_29 x_30) 10))) $cvcl_250) $cvcl_254) $cvcl_255) ) (and (and (and (and (and (and (and (and (= x_70 2) $cvcl_251) $cvcl_252) $cvcl_257) x_47) (= x_48 x_30)) $cvcl_253) $cvcl_254) $cvcl_255) ) (and (and (and (and (and (and (and (and (and (= x_70 3) $cvcl_256) x_32) x_11) $cvcl_257) x_47) (= x_48 (+ x_29 10))) $cvcl_253) $cvcl_254) $cvcl_255) ) (and (and (and (and (and (and (and (and (and (and (= x_70 4) (or (or (or $cvcl_256 x_32 ) $cvcl_258 ) (not x_71) )) (or $cvcl_259 $cvcl_252 )) (or $cvcl_259 $cvcl_260 )) (or (or x_31 $cvcl_249 ) $cvcl_261 )) $cvcl_250) $cvcl_253) (iff x_35 x_31)) (iff x_36 x_32)) $cvcl_254) $cvcl_255) )) (or (or (or (or (not (<= x_179 0)) (not (<= x_139 0)) ) (not (<= x_99 0)) ) (not (<= x_59 0)) ) (not (<= x_30 0)) )) (or (not x_4) (and (not x_3) (not x_2)) )) (or (not x_7) (and (not x_6) (not x_5)) )) (or $cvcl_240 $cvcl_239 )) (or $cvcl_249 $cvcl_256 )) (or $cvcl_186 $cvcl_193 )) (or $cvcl_199 (and $cvcl_201 $cvcl_200) )) (or $cvcl_227 (and $cvcl_230 $cvcl_229) )) (or $cvcl_176 $cvcl_182 )) (or $cvcl_123 $cvcl_130 )) (or $cvcl_135 (and $cvcl_137 $cvcl_136) )) (or $cvcl_164 (and $cvcl_167 $cvcl_166) )) (or $cvcl_113 $cvcl_119 )) (or $cvcl_58 $cvcl_67 )) (or $cvcl_72 (and $cvcl_74 $cvcl_73) )) (or $cvcl_101 (and $cvcl_104 $cvcl_103) )) (or $cvcl_45 $cvcl_52 )) (or $cvcl_63 $cvcl_59 )) (or $cvcl_1 (and $cvcl_3 $cvcl_2) )) (or $cvcl_33 (and $cvcl_36 $cvcl_35) )) (or $cvcl_54 $cvcl_53 )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )