sidekick/tests/unsat/NEQ041_size7.smt2

(set-info :smt-lib-version 2.6)
(set-logic QF_UF)
(set-info :source |
CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC
 for more information. 

This benchmark was obtained by trying to find a finite model of a first-order 
formula (Albert Oliveras).
|)
(set-info :category "crafted")
(set-info :status unsat)
(declare-sort U 0)
(declare-fun f4 (U U) U)
(declare-fun f3 (U) U)
(declare-fun p5 (U U) Bool)
(declare-fun c6 () U)
(declare-fun f1 (U) U)
(declare-fun f2 (U U) U)
(declare-fun c_0 () U)
(declare-fun c_1 () U)
(declare-fun c_2 () U)
(declare-fun c_3 () U)
(declare-fun c_4 () U)
(declare-fun c_5 () U)
(declare-fun c_6 () U)
(assert (let ((?v_232 (f4 c_0 c_0)) (?v_0 (f3 c_0))) (let ((?v_224 (p5 c_0 ?v_0))) (let ((?v_231 (not ?v_224)) (?v_1 (p5 c_0 c6)) (?v_246 (f4 c_0 c_1)) (?v_245 (not (p5 c_1 ?v_0))) (?v_260 (f4 c_0 c_2)) (?v_259 (not (p5 c_2 ?v_0))) (?v_274 (f4 c_0 c_3)) (?v_273 (not (p5 c_3 ?v_0))) (?v_288 (f4 c_0 c_4)) (?v_287 (not (p5 c_4 ?v_0))) (?v_302 (f4 c_0 c_5)) (?v_301 (not (p5 c_5 ?v_0))) (?v_316 (f4 c_0 c_6)) (?v_315 (not (p5 c_6 ?v_0))) (?v_234 (f4 c_1 c_0)) (?v_2 (f3 c_1))) (let ((?v_233 (not (p5 c_0 ?v_2))) (?v_3 (p5 c_1 c6)) (?v_248 (f4 c_1 c_1)) (?v_225 (p5 c_1 ?v_2))) (let ((?v_247 (not ?v_225)) (?v_262 (f4 c_1 c_2)) (?v_261 (not (p5 c_2 ?v_2))) (?v_276 (f4 c_1 c_3)) (?v_275 (not (p5 c_3 ?v_2))) (?v_290 (f4 c_1 c_4)) (?v_289 (not (p5 c_4 ?v_2))) (?v_304 (f4 c_1 c_5)) (?v_303 (not (p5 c_5 ?v_2))) (?v_318 (f4 c_1 c_6)) (?v_317 (not (p5 c_6 ?v_2))) (?v_236 (f4 c_2 c_0)) (?v_4 (f3 c_2))) (let ((?v_235 (not (p5 c_0 ?v_4))) (?v_5 (p5 c_2 c6)) (?v_250 (f4 c_2 c_1)) (?v_249 (not (p5 c_1 ?v_4))) (?v_264 (f4 c_2 c_2)) (?v_226 (p5 c_2 ?v_4))) (let ((?v_263 (not ?v_226)) (?v_278 (f4 c_2 c_3)) (?v_277 (not (p5 c_3 ?v_4))) (?v_292 (f4 c_2 c_4)) (?v_291 (not (p5 c_4 ?v_4))) (?v_306 (f4 c_2 c_5)) (?v_305 (not (p5 c_5 ?v_4))) (?v_320 (f4 c_2 c_6)) (?v_319 (not (p5 c_6 ?v_4))) (?v_238 (f4 c_3 c_0)) (?v_6 (f3 c_3))) (let ((?v_237 (not (p5 c_0 ?v_6))) (?v_7 (p5 c_3 c6)) (?v_252 (f4 c_3 c_1)) (?v_251 (not (p5 c_1 ?v_6))) (?v_266 (f4 c_3 c_2)) (?v_265 (not (p5 c_2 ?v_6))) (?v_280 (f4 c_3 c_3)) (?v_227 (p5 c_3 ?v_6))) (let ((?v_279 (not ?v_227)) (?v_294 (f4 c_3 c_4)) (?v_293 (not (p5 c_4 ?v_6))) (?v_308 (f4 c_3 c_5)) (?v_307 (not (p5 c_5 ?v_6))) (?v_322 (f4 c_3 c_6)) (?v_321 (not (p5 c_6 ?v_6))) (?v_240 (f4 c_4 c_0)) (?v_8 (f3 c_4))) (let ((?v_239 (not (p5 c_0 ?v_8))) (?v_9 (p5 c_4 c6)) (?v_254 (f4 c_4 c_1)) (?v_253 (not (p5 c_1 ?v_8))) (?v_268 (f4 c_4 c_2)) (?v_267 (not (p5 c_2 ?v_8))) (?v_282 (f4 c_4 c_3)) (?v_281 (not (p5 c_3 ?v_8))) (?v_296 (f4 c_4 c_4)) (?v_228 (p5 c_4 ?v_8))) (let ((?v_295 (not ?v_228)) (?v_310 (f4 c_4 c_5)) (?v_309 (not (p5 c_5 ?v_8))) (?v_324 (f4 c_4 c_6)) (?v_323 (not (p5 c_6 ?v_8))) (?v_242 (f4 c_5 c_0)) (?v_10 (f3 c_5))) (let ((?v_241 (not (p5 c_0 ?v_10))) (?v_11 (p5 c_5 c6)) (?v_256 (f4 c_5 c_1)) (?v_255 (not (p5 c_1 ?v_10))) (?v_270 (f4 c_5 c_2)) (?v_269 (not (p5 c_2 ?v_10))) (?v_284 (f4 c_5 c_3)) (?v_283 (not (p5 c_3 ?v_10))) (?v_298 (f4 c_5 c_4)) (?v_297 (not (p5 c_4 ?v_10))) (?v_312 (f4 c_5 c_5)) (?v_229 (p5 c_5 ?v_10))) (let ((?v_311 (not ?v_229)) (?v_326 (f4 c_5 c_6)) (?v_325 (not (p5 c_6 ?v_10))) (?v_244 (f4 c_6 c_0)) (?v_12 (f3 c_6))) (let ((?v_243 (not (p5 c_0 ?v_12))) (?v_13 (p5 c_6 c6)) (?v_258 (f4 c_6 c_1)) (?v_257 (not (p5 c_1 ?v_12))) (?v_272 (f4 c_6 c_2)) (?v_271 (not (p5 c_2 ?v_12))) (?v_286 (f4 c_6 c_3)) (?v_285 (not (p5 c_3 ?v_12))) (?v_300 (f4 c_6 c_4)) (?v_299 (not (p5 c_4 ?v_12))) (?v_314 (f4 c_6 c_5)) (?v_313 (not (p5 c_5 ?v_12))) (?v_328 (f4 c_6 c_6)) (?v_230 (p5 c_6 ?v_12))) (let ((?v_327 (not ?v_230)) (?v_127 (= c_0 c_0)) (?v_14 (f1 c_0))) (let ((?v_126 (p5 c_0 ?v_14)) (?v_129 (= c_0 c_1)) (?v_15 (f1 c_1))) (let ((?v_128 (p5 c_0 ?v_15)) (?v_131 (= c_0 c_2)) (?v_16 (f1 c_2))) (let ((?v_130 (p5 c_0 ?v_16)) (?v_133 (= c_0 c_3)) (?v_17 (f1 c_3))) (let ((?v_132 (p5 c_0 ?v_17)) (?v_135 (= c_0 c_4)) (?v_18 (f1 c_4))) (let ((?v_134 (p5 c_0 ?v_18)) (?v_137 (= c_0 c_5)) (?v_19 (f1 c_5))) (let ((?v_136 (p5 c_0 ?v_19)) (?v_139 (= c_0 c_6)) (?v_20 (f1 c_6))) (let ((?v_138 (p5 c_0 ?v_20)) (?v_141 (= c_1 c_0)) (?v_140 (p5 c_1 ?v_14)) (?v_143 (= c_1 c_1)) (?v_142 (p5 c_1 ?v_15)) (?v_145 (= c_1 c_2)) (?v_144 (p5 c_1 ?v_16)) (?v_147 (= c_1 c_3)) (?v_146 (p5 c_1 ?v_17)) (?v_149 (= c_1 c_4)) (?v_148 (p5 c_1 ?v_18)) (?v_151 (= c_1 c_5)) (?v_150 (p5 c_1 ?v_19)) (?v_153 (= c_1 c_6)) (?v_152 (p5 c_1 ?v_20)) (?v_155 (= c_2 c_0)) (?v_154 (p5 c_2 ?v_14)) (?v_157 (= c_2 c_1)) (?v_156 (p5 c_2 ?v_15)) (?v_159 (= c_2 c_2)) (?v_158 (p5 c_2 ?v_16)) (?v_161 (= c_2 c_3)) (?v_160 (p5 c_2 ?v_17)) (?v_163 (= c_2 c_4)) (?v_162 (p5 c_2 ?v_18)) (?v_165 (= c_2 c_5)) (?v_164 (p5 c_2 ?v_19)) (?v_167 (= c_2 c_6)) (?v_166 (p5 c_2 ?v_20)) (?v_169 (= c_3 c_0)) (?v_168 (p5 c_3 ?v_14)) (?v_171 (= c_3 c_1)) (?v_170 (p5 c_3 ?v_15)) (?v_173 (= c_3 c_2)) (?v_172 (p5 c_3 ?v_16)) (?v_175 (= c_3 c_3)) (?v_174 (p5 c_3 ?v_17)) (?v_177 (= c_3 c_4)) (?v_176 (p5 c_3 ?v_18)) (?v_179 (= c_3 c_5)) (?v_178 (p5 c_3 ?v_19)) (?v_181 (= c_3 c_6)) (?v_180 (p5 c_3 ?v_20)) (?v_183 (= c_4 c_0)) (?v_182 (p5 c_4 ?v_14)) (?v_185 (= c_4 c_1)) (?v_184 (p5 c_4 ?v_15)) (?v_187 (= c_4 c_2)) (?v_186 (p5 c_4 ?v_16)) (?v_189 (= c_4 c_3)) (?v_188 (p5 c_4 ?v_17)) (?v_191 (= c_4 c_4)) (?v_190 (p5 c_4 ?v_18)) (?v_193 (= c_4 c_5)) (?v_192 (p5 c_4 ?v_19)) (?v_195 (= c_4 c_6)) (?v_194 (p5 c_4 ?v_20)) (?v_197 (= c_5 c_0)) (?v_196 (p5 c_5 ?v_14)) (?v_199 (= c_5 c_1)) (?v_198 (p5 c_5 ?v_15)) (?v_201 (= c_5 c_2)) (?v_200 (p5 c_5 ?v_16)) (?v_203 (= c_5 c_3)) (?v_202 (p5 c_5 ?v_17)) (?v_205 (= c_5 c_4)) (?v_204 (p5 c_5 ?v_18)) (?v_207 (= c_5 c_5)) (?v_206 (p5 c_5 ?v_19)) (?v_209 (= c_5 c_6)) (?v_208 (p5 c_5 ?v_20)) (?v_211 (= c_6 c_0)) (?v_210 (p5 c_6 ?v_14)) (?v_213 (= c_6 c_1)) (?v_212 (p5 c_6 ?v_15)) (?v_215 (= c_6 c_2)) (?v_214 (p5 c_6 ?v_16)) (?v_217 (= c_6 c_3)) (?v_216 (p5 c_6 ?v_17)) (?v_219 (= c_6 c_4)) (?v_218 (p5 c_6 ?v_18)) (?v_221 (= c_6 c_5)) (?v_220 (p5 c_6 ?v_19)) (?v_223 (= c_6 c_6)) (?v_222 (p5 c_6 ?v_20)) (?v_21 (not (p5 c_0 c_0))) (?v_22 (not ?v_1)) (?v_23 (f2 c_0 c_0)) (?v_36 (not (p5 c_1 c_0))) (?v_39 (not (p5 c_2 c_0))) (?v_40 (not (p5 c_3 c_0))) (?v_41 (not (p5 c_4 c_0))) (?v_42 (not (p5 c_5 c_0))) (?v_43 (not (p5 c_6 c_0))) (?v_24 (not (p5 c_0 c_1))) (?v_25 (f2 c_0 c_1)) (?v_44 (not (p5 c_1 c_1))) (?v_46 (not (p5 c_2 c_1))) (?v_47 (not (p5 c_3 c_1))) (?v_48 (not (p5 c_4 c_1))) (?v_49 (not (p5 c_5 c_1))) (?v_50 (not (p5 c_6 c_1))) (?v_26 (not (p5 c_0 c_2))) (?v_27 (f2 c_0 c_2)) (?v_51 (not (p5 c_1 c_2))) (?v_53 (not (p5 c_2 c_2))) (?v_54 (not (p5 c_3 c_2))) (?v_55 (not (p5 c_4 c_2))) (?v_56 (not (p5 c_5 c_2))) (?v_57 (not (p5 c_6 c_2))) (?v_28 (not (p5 c_0 c_3))) (?v_29 (f2 c_0 c_3)) (?v_58 (not (p5 c_1 c_3))) (?v_60 (not (p5 c_2 c_3))) (?v_61 (not (p5 c_3 c_3))) (?v_62 (not (p5 c_4 c_3))) (?v_63 (not (p5 c_5 c_3))) (?v_64 (not (p5 c_6 c_3))) (?v_30 (not (p5 c_0 c_4))) (?v_31 (f2 c_0 c_4)) (?v_65 (not (p5 c_1 c_4))) (?v_67 (not (p5 c_2 c_4))) (?v_68 (not (p5 c_3 c_4))) (?v_69 (not (p5 c_4 c_4))) (?v_70 (not (p5 c_5 c_4))) (?v_71 (not (p5 c_6 c_4))) (?v_32 (not (p5 c_0 c_5))) (?v_33 (f2 c_0 c_5)) (?v_72 (not (p5 c_1 c_5))) (?v_74 (not (p5 c_2 c_5))) (?v_75 (not (p5 c_3 c_5))) (?v_76 (not (p5 c_4 c_5))) (?v_77 (not (p5 c_5 c_5))) (?v_78 (not (p5 c_6 c_5))) (?v_34 (not (p5 c_0 c_6))) (?v_35 (f2 c_0 c_6)) (?v_79 (not (p5 c_1 c_6))) (?v_81 (not (p5 c_2 c_6))) (?v_82 (not (p5 c_3 c_6))) (?v_83 (not (p5 c_4 c_6))) (?v_84 (not (p5 c_5 c_6))) (?v_85 (not (p5 c_6 c_6))) (?v_37 (not ?v_3)) (?v_38 (f2 c_1 c_0)) (?v_45 (f2 c_1 c_1)) (?v_52 (f2 c_1 c_2)) (?v_59 (f2 c_1 c_3)) (?v_66 (f2 c_1 c_4)) (?v_73 (f2 c_1 c_5)) (?v_80 (f2 c_1 c_6)) (?v_86 (not ?v_5)) (?v_87 (f2 c_2 c_0)) (?v_88 (f2 c_2 c_1)) (?v_89 (f2 c_2 c_2)) (?v_90 (f2 c_2 c_3)) (?v_91 (f2 c_2 c_4)) (?v_92 (f2 c_2 c_5)) (?v_93 (f2 c_2 c_6)) (?v_94 (not ?v_7)) (?v_95 (f2 c_3 c_0)) (?v_96 (f2 c_3 c_1)) (?v_97 (f2 c_3 c_2)) (?v_98 (f2 c_3 c_3)) (?v_99 (f2 c_3 c_4)) (?v_100 (f2 c_3 c_5)) (?v_101 (f2 c_3 c_6)) (?v_102 (not ?v_9)) (?v_103 (f2 c_4 c_0)) (?v_104 (f2 c_4 c_1)) (?v_105 (f2 c_4 c_2)) (?v_106 (f2 c_4 c_3)) (?v_107 (f2 c_4 c_4)) (?v_108 (f2 c_4 c_5)) (?v_109 (f2 c_4 c_6)) (?v_110 (not ?v_11)) (?v_111 (f2 c_5 c_0)) (?v_112 (f2 c_5 c_1)) (?v_113 (f2 c_5 c_2)) (?v_114 (f2 c_5 c_3)) (?v_115 (f2 c_5 c_4)) (?v_116 (f2 c_5 c_5)) (?v_117 (f2 c_5 c_6)) (?v_118 (not ?v_13)) (?v_119 (f2 c_6 c_0)) (?v_120 (f2 c_6 c_1)) (?v_121 (f2 c_6 c_2)) (?v_122 (f2 c_6 c_3)) (?v_123 (f2 c_6 c_4)) (?v_124 (f2 c_6 c_5)) (?v_125 (f2 c_6 c_6))) (and (distinct c_0 c_1 c_2 c_3 c_4 c_5 c_6) (or (p5 ?v_232 ?v_0) ?v_231 ?v_1) (or (p5 ?v_246 ?v_0) ?v_245 ?v_1) (or (p5 ?v_260 ?v_0) ?v_259 ?v_1) (or (p5 ?v_274 ?v_0) ?v_273 ?v_1) (or (p5 ?v_288 ?v_0) ?v_287 ?v_1) (or (p5 ?v_302 ?v_0) ?v_301 ?v_1) (or (p5 ?v_316 ?v_0) ?v_315 ?v_1) (or (p5 ?v_234 ?v_2) ?v_233 ?v_3) (or (p5 ?v_248 ?v_2) ?v_247 ?v_3) (or (p5 ?v_262 ?v_2) ?v_261 ?v_3) (or (p5 ?v_276 ?v_2) ?v_275 ?v_3) (or (p5 ?v_290 ?v_2) ?v_289 ?v_3) (or (p5 ?v_304 ?v_2) ?v_303 ?v_3) (or (p5 ?v_318 ?v_2) ?v_317 ?v_3) (or (p5 ?v_236 ?v_4) ?v_235 ?v_5) (or (p5 ?v_250 ?v_4) ?v_249 ?v_5) (or (p5 ?v_264 ?v_4) ?v_263 ?v_5) (or (p5 ?v_278 ?v_4) ?v_277 ?v_5) (or (p5 ?v_292 ?v_4) ?v_291 ?v_5) (or (p5 ?v_306 ?v_4) ?v_305 ?v_5) (or (p5 ?v_320 ?v_4) ?v_319 ?v_5) (or (p5 ?v_238 ?v_6) ?v_237 ?v_7) (or (p5 ?v_252 ?v_6) ?v_251 ?v_7) (or (p5 ?v_266 ?v_6) ?v_265 ?v_7) (or (p5 ?v_280 ?v_6) ?v_279 ?v_7) (or (p5 ?v_294 ?v_6) ?v_293 ?v_7) (or (p5 ?v_308 ?v_6) ?v_307 ?v_7) (or (p5 ?v_322 ?v_6) ?v_321 ?v_7) (or (p5 ?v_240 ?v_8) ?v_239 ?v_9) (or (p5 ?v_254 ?v_8) ?v_253 ?v_9) (or (p5 ?v_268 ?v_8) ?v_267 ?v_9) (or (p5 ?v_282 ?v_8) ?v_281 ?v_9) (or (p5 ?v_296 ?v_8) ?v_295 ?v_9) (or (p5 ?v_310 ?v_8) ?v_309 ?v_9) (or (p5 ?v_324 ?v_8) ?v_323 ?v_9) (or (p5 ?v_242 ?v_10) ?v_241 ?v_11) (or (p5 ?v_256 ?v_10) ?v_255 ?v_11) (or (p5 ?v_270 ?v_10) ?v_269 ?v_11) (or (p5 ?v_284 ?v_10) ?v_283 ?v_11) (or (p5 ?v_298 ?v_10) ?v_297 ?v_11) (or (p5 ?v_312 ?v_10) ?v_311 ?v_11) (or (p5 ?v_326 ?v_10) ?v_325 ?v_11) (or (p5 ?v_244 ?v_12) ?v_243 ?v_13) (or (p5 ?v_258 ?v_12) ?v_257 ?v_13) (or (p5 ?v_272 ?v_12) ?v_271 ?v_13) (or (p5 ?v_286 ?v_12) ?v_285 ?v_13) (or (p5 ?v_300 ?v_12) ?v_299 ?v_13) (or (p5 ?v_314 ?v_12) ?v_313 ?v_13) (or (p5 ?v_328 ?v_12) ?v_327 ?v_13) (or (not ?v_127) ?v_126) (or (not ?v_129) ?v_128) (or (not ?v_131) ?v_130) (or (not ?v_133) ?v_132) (or (not ?v_135) ?v_134) (or (not ?v_137) ?v_136) (or (not ?v_139) ?v_138) (or (not ?v_141) ?v_140) (or (not ?v_143) ?v_142) (or (not ?v_145) ?v_144) (or (not ?v_147) ?v_146) (or (not ?v_149) ?v_148) (or (not ?v_151) ?v_150) (or (not ?v_153) ?v_152) (or (not ?v_155) ?v_154) (or (not ?v_157) ?v_156) (or (not ?v_159) ?v_158) (or (not ?v_161) ?v_160) (or (not ?v_163) ?v_162) (or (not ?v_165) ?v_164) (or (not ?v_167) ?v_166) (or (not ?v_169) ?v_168) (or (not ?v_171) ?v_170) (or (not ?v_173) ?v_172) (or (not ?v_175) ?v_174) (or (not ?v_177) ?v_176) (or (not ?v_179) ?v_178) (or (not ?v_181) ?v_180) (or (not ?v_183) ?v_182) (or (not ?v_185) ?v_184) (or (not ?v_187) ?v_186) (or (not ?v_189) ?v_188) (or (not ?v_191) ?v_190) (or (not ?v_193) ?v_192) (or (not ?v_195) ?v_194) (or (not ?v_197) ?v_196) (or (not ?v_199) ?v_198) (or (not ?v_201) ?v_200) (or (not ?v_203) ?v_202) (or (not ?v_205) ?v_204) (or (not ?v_207) ?v_206) (or (not ?v_209) ?v_208) (or (not ?v_211) ?v_210) (or (not ?v_213) ?v_212) (or (not ?v_215) ?v_214) (or (not ?v_217) ?v_216) (or (not ?v_219) ?v_218) (or (not ?v_221) ?v_220) (or (not ?v_223) ?v_222) (or ?v_21 ?v_22 (not (p5 c_0 ?v_23)) ?v_21) (or ?v_21 ?v_22 (not (p5 c_1 ?v_23)) ?v_36) (or ?v_21 ?v_22 (not (p5 c_2 ?v_23)) ?v_39) (or ?v_21 ?v_22 (not (p5 c_3 ?v_23)) ?v_40) (or ?v_21 ?v_22 (not (p5 c_4 ?v_23)) ?v_41) (or ?v_21 ?v_22 (not (p5 c_5 ?v_23)) ?v_42) (or ?v_21 ?v_22 (not (p5 c_6 ?v_23)) ?v_43) (or ?v_24 ?v_22 (not (p5 c_0 ?v_25)) ?v_24) (or ?v_24 ?v_22 (not (p5 c_1 ?v_25)) ?v_44) (or ?v_24 ?v_22 (not (p5 c_2 ?v_25)) ?v_46) (or ?v_24 ?v_22 (not (p5 c_3 ?v_25)) ?v_47) (or ?v_24 ?v_22 (not (p5 c_4 ?v_25)) ?v_48) (or ?v_24 ?v_22 (not (p5 c_5 ?v_25)) ?v_49) (or ?v_24 ?v_22 (not (p5 c_6 ?v_25)) ?v_50) (or ?v_26 ?v_22 (not (p5 c_0 ?v_27)) ?v_26) (or ?v_26 ?v_22 (not (p5 c_1 ?v_27)) ?v_51) (or ?v_26 ?v_22 (not (p5 c_2 ?v_27)) ?v_53) (or ?v_26 ?v_22 (not (p5 c_3 ?v_27)) ?v_54) (or ?v_26 ?v_22 (not (p5 c_4 ?v_27)) ?v_55) (or ?v_26 ?v_22 (not (p5 c_5 ?v_27)) ?v_56) (or ?v_26 ?v_22 (not (p5 c_6 ?v_27)) ?v_57) (or ?v_28 ?v_22 (not (p5 c_0 ?v_29)) ?v_28) (or ?v_28 ?v_22 (not (p5 c_1 ?v_29)) ?v_58) (or ?v_28 ?v_22 (not (p5 c_2 ?v_29)) ?v_60) (or ?v_28 ?v_22 (not (p5 c_3 ?v_29)) ?v_61) (or ?v_28 ?v_22 (not (p5 c_4 ?v_29)) ?v_62) (or ?v_28 ?v_22 (not (p5 c_5 ?v_29)) ?v_63) (or ?v_28 ?v_22 (not (p5 c_6 ?v_29)) ?v_64) (or ?v_30 ?v_22 (not (p5 c_0 ?v_31)) ?v_30) (or ?v_30 ?v_22 (not (p5 c_1 ?v_31)) ?v_65) (or ?v_30 ?v_22 (not (p5 c_2 ?v_31)) ?v_67) (or ?v_30 ?v_22 (not (p5 c_3 ?v_31)) ?v_68) (or ?v_30 ?v_22 (not (p5 c_4 ?v_31)) ?v_69) (or ?v_30 ?v_22 (not (p5 c_5 ?v_31)) ?v_70) (or ?v_30 ?v_22 (not (p5 c_6 ?v_31)) ?v_71) (or ?v_32 ?v_22 (not (p5 c_0 ?v_33)) ?v_32) (or ?v_32 ?v_22 (not (p5 c_1 ?v_33)) ?v_72) (or ?v_32 ?v_22 (not (p5 c_2 ?v_33)) ?v_74) (or ?v_32 ?v_22 (not (p5 c_3 ?v_33)) ?v_75) (or ?v_32 ?v_22 (not (p5 c_4 ?v_33)) ?v_76) (or ?v_32 ?v_22 (not (p5 c_5 ?v_33)) ?v_77) (or ?v_32 ?v_22 (not (p5 c_6 ?v_33)) ?v_78) (or ?v_34 ?v_22 (not (p5 c_0 ?v_35)) ?v_34) (or ?v_34 ?v_22 (not (p5 c_1 ?v_35)) ?v_79) (or ?v_34 ?v_22 (not (p5 c_2 ?v_35)) ?v_81) (or ?v_34 ?v_22 (not (p5 c_3 ?v_35)) ?v_82) (or ?v_34 ?v_22 (not (p5 c_4 ?v_35)) ?v_83) (or ?v_34 ?v_22 (not (p5 c_5 ?v_35)) ?v_84) (or ?v_34 ?v_22 (not (p5 c_6 ?v_35)) ?v_85) (or ?v_36 ?v_37 (not (p5 c_0 ?v_38)) ?v_21) (or ?v_36 ?v_37 (not (p5 c_1 ?v_38)) ?v_36) (or ?v_36 ?v_37 (not (p5 c_2 ?v_38)) ?v_39) (or ?v_36 ?v_37 (not (p5 c_3 ?v_38)) ?v_40) (or ?v_36 ?v_37 (not (p5 c_4 ?v_38)) ?v_41) (or ?v_36 ?v_37 (not (p5 c_5 ?v_38)) ?v_42) (or ?v_36 ?v_37 (not (p5 c_6 ?v_38)) ?v_43) (or ?v_44 ?v_37 (not (p5 c_0 ?v_45)) ?v_24) (or ?v_44 ?v_37 (not (p5 c_1 ?v_45)) ?v_44) (or ?v_44 ?v_37 (not (p5 c_2 ?v_45)) ?v_46) (or ?v_44 ?v_37 (not (p5 c_3 ?v_45)) ?v_47) (or ?v_44 ?v_37 (not (p5 c_4 ?v_45)) ?v_48) (or ?v_44 ?v_37 (not (p5 c_5 ?v_45)) ?v_49) (or ?v_44 ?v_37 (not (p5 c_6 ?v_45)) ?v_50) (or ?v_51 ?v_37 (not (p5 c_0 ?v_52)) ?v_26) (or ?v_51 ?v_37 (not (p5 c_1 ?v_52)) ?v_51) (or ?v_51 ?v_37 (not (p5 c_2 ?v_52)) ?v_53) (or ?v_51 ?v_37 (not (p5 c_3 ?v_52)) ?v_54) (or ?v_51 ?v_37 (not (p5 c_4 ?v_52)) ?v_55) (or ?v_51 ?v_37 (not (p5 c_5 ?v_52)) ?v_56) (or ?v_51 ?v_37 (not (p5 c_6 ?v_52)) ?v_57) (or ?v_58 ?v_37 (not (p5 c_0 ?v_59)) ?v_28) (or ?v_58 ?v_37 (not (p5 c_1 ?v_59)) ?v_58) (or ?v_58 ?v_37 (not (p5 c_2 ?v_59)) ?v_60) (or ?v_58 ?v_37 (not (p5 c_3 ?v_59)) ?v_61) (or ?v_58 ?v_37 (not (p5 c_4 ?v_59)) ?v_62) (or ?v_58 ?v_37 (not (p5 c_5 ?v_59)) ?v_63) (or ?v_58 ?v_37 (not (p5 c_6 ?v_59)) ?v_64) (or ?v_65 ?v_37 (not (p5 c_0 ?v_66)) ?v_30) (or ?v_65 ?v_37 (not (p5 c_1 ?v_66)) ?v_65) (or ?v_65 ?v_37 (not (p5 c_2 ?v_66)) ?v_67) (or ?v_65 ?v_37 (not (p5 c_3 ?v_66)) ?v_68) (or ?v_65 ?v_37 (not (p5 c_4 ?v_66)) ?v_69) (or ?v_65 ?v_37 (not (p5 c_5 ?v_66)) ?v_70) (or ?v_65 ?v_37 (not (p5 c_6 ?v_66)) ?v_71) (or ?v_72 ?v_37 (not (p5 c_0 ?v_73)) ?v_32) (or ?v_72 ?v_37 (not (p5 c_1 ?v_73)) ?v_72) (or ?v_72 ?v_37 (not (p5 c_2 ?v_73)) ?v_74) (or ?v_72 ?v_37 (not (p5 c_3 ?v_73)) ?v_75) (or ?v_72 ?v_37 (not (p5 c_4 ?v_73)) ?v_76) (or ?v_72 ?v_37 (not (p5 c_5 ?v_73)) ?v_77) (or ?v_72 ?v_37 (not (p5 c_6 ?v_73)) ?v_78) (or ?v_79 ?v_37 (not (p5 c_0 ?v_80)) ?v_34) (or ?v_79 ?v_37 (not (p5 c_1 ?v_80)) ?v_79) (or ?v_79 ?v_37 (not (p5 c_2 ?v_80)) ?v_81) (or ?v_79 ?v_37 (not (p5 c_3 ?v_80)) ?v_82) (or ?v_79 ?v_37 (not (p5 c_4 ?v_80)) ?v_83) (or ?v_79 ?v_37 (not (p5 c_5 ?v_80)) ?v_84) (or ?v_79 ?v_37 (not (p5 c_6 ?v_80)) ?v_85) (or ?v_39 ?v_86 (not (p5 c_0 ?v_87)) ?v_21) (or ?v_39 ?v_86 (not (p5 c_1 ?v_87)) ?v_36) (or ?v_39 ?v_86 (not (p5 c_2 ?v_87)) ?v_39) (or ?v_39 ?v_86 (not (p5 c_3 ?v_87)) ?v_40) (or ?v_39 ?v_86 (not (p5 c_4 ?v_87)) ?v_41) (or ?v_39 ?v_86 (not (p5 c_5 ?v_87)) ?v_42) (or ?v_39 ?v_86 (not (p5 c_6 ?v_87)) ?v_43) (or ?v_46 ?v_86 (not (p5 c_0 ?v_88)) ?v_24) (or ?v_46 ?v_86 (not (p5 c_1 ?v_88)) ?v_44) (or ?v_46 ?v_86 (not (p5 c_2 ?v_88)) ?v_46) (or ?v_46 ?v_86 (not (p5 c_3 ?v_88)) ?v_47) (or ?v_46 ?v_86 (not (p5 c_4 ?v_88)) ?v_48) (or ?v_46 ?v_86 (not (p5 c_5 ?v_88)) ?v_49) (or ?v_46 ?v_86 (not (p5 c_6 ?v_88)) ?v_50) (or ?v_53 ?v_86 (not (p5 c_0 ?v_89)) ?v_26) (or ?v_53 ?v_86 (not (p5 c_1 ?v_89)) ?v_51) (or ?v_53 ?v_86 (not (p5 c_2 ?v_89)) ?v_53) (or ?v_53 ?v_86 (not (p5 c_3 ?v_89)) ?v_54) (or ?v_53 ?v_86 (not (p5 c_4 ?v_89)) ?v_55) (or ?v_53 ?v_86 (not (p5 c_5 ?v_89)) ?v_56) (or ?v_53 ?v_86 (not (p5 c_6 ?v_89)) ?v_57) (or ?v_60 ?v_86 (not (p5 c_0 ?v_90)) ?v_28) (or ?v_60 ?v_86 (not (p5 c_1 ?v_90)) ?v_58) (or ?v_60 ?v_86 (not (p5 c_2 ?v_90)) ?v_60) (or ?v_60 ?v_86 (not (p5 c_3 ?v_90)) ?v_61) (or ?v_60 ?v_86 (not (p5 c_4 ?v_90)) ?v_62) (or ?v_60 ?v_86 (not (p5 c_5 ?v_90)) ?v_63) (or ?v_60 ?v_86 (not (p5 c_6 ?v_90)) ?v_64) (or ?v_67 ?v_86 (not (p5 c_0 ?v_91)) ?v_30) (or ?v_67 ?v_86 (not (p5 c_1 ?v_91)) ?v_65) (or ?v_67 ?v_86 (not (p5 c_2 ?v_91)) ?v_67) (or ?v_67 ?v_86 (not (p5 c_3 ?v_91)) ?v_68) (or ?v_67 ?v_86 (not (p5 c_4 ?v_91)) ?v_69) (or ?v_67 ?v_86 (not (p5 c_5 ?v_91)) ?v_70) (or ?v_67 ?v_86 (not (p5 c_6 ?v_91)) ?v_71) (or ?v_74 ?v_86 (not (p5 c_0 ?v_92)) ?v_32) (or ?v_74 ?v_86 (not (p5 c_1 ?v_92)) ?v_72) (or ?v_74 ?v_86 (not (p5 c_2 ?v_92)) ?v_74) (or ?v_74 ?v_86 (not (p5 c_3 ?v_92)) ?v_75) (or ?v_74 ?v_86 (not (p5 c_4 ?v_92)) ?v_76) (or ?v_74 ?v_86 (not (p5 c_5 ?v_92)) ?v_77) (or ?v_74 ?v_86 (not (p5 c_6 ?v_92)) ?v_78) (or ?v_81 ?v_86 (not (p5 c_0 ?v_93)) ?v_34) (or ?v_81 ?v_86 (not (p5 c_1 ?v_93)) ?v_79) (or ?v_81 ?v_86 (not (p5 c_2 ?v_93)) ?v_81) (or ?v_81 ?v_86 (not (p5 c_3 ?v_93)) ?v_82) (or ?v_81 ?v_86 (not (p5 c_4 ?v_93)) ?v_83) (or ?v_81 ?v_86 (not (p5 c_5 ?v_93)) ?v_84) (or ?v_81 ?v_86 (not (p5 c_6 ?v_93)) ?v_85) (or ?v_40 ?v_94 (not (p5 c_0 ?v_95)) ?v_21) (or ?v_40 ?v_94 (not (p5 c_1 ?v_95)) ?v_36) (or ?v_40 ?v_94 (not (p5 c_2 ?v_95)) ?v_39) (or ?v_40 ?v_94 (not (p5 c_3 ?v_95)) ?v_40) (or ?v_40 ?v_94 (not (p5 c_4 ?v_95)) ?v_41) (or ?v_40 ?v_94 (not (p5 c_5 ?v_95)) ?v_42) (or ?v_40 ?v_94 (not (p5 c_6 ?v_95)) ?v_43) (or ?v_47 ?v_94 (not (p5 c_0 ?v_96)) ?v_24) (or ?v_47 ?v_94 (not (p5 c_1 ?v_96)) ?v_44) (or ?v_47 ?v_94 (not (p5 c_2 ?v_96)) ?v_46) (or ?v_47 ?v_94 (not (p5 c_3 ?v_96)) ?v_47) (or ?v_47 ?v_94 (not (p5 c_4 ?v_96)) ?v_48) (or ?v_47 ?v_94 (not (p5 c_5 ?v_96)) ?v_49) (or ?v_47 ?v_94 (not (p5 c_6 ?v_96)) ?v_50) (or ?v_54 ?v_94 (not (p5 c_0 ?v_97)) ?v_26) (or ?v_54 ?v_94 (not (p5 c_1 ?v_97)) ?v_51) (or ?v_54 ?v_94 (not (p5 c_2 ?v_97)) ?v_53) (or ?v_54 ?v_94 (not (p5 c_3 ?v_97)) ?v_54) (or ?v_54 ?v_94 (not (p5 c_4 ?v_97)) ?v_55) (or ?v_54 ?v_94 (not (p5 c_5 ?v_97)) ?v_56) (or ?v_54 ?v_94 (not (p5 c_6 ?v_97)) ?v_57) (or ?v_61 ?v_94 (not (p5 c_0 ?v_98)) ?v_28) (or ?v_61 ?v_94 (not (p5 c_1 ?v_98)) ?v_58) (or ?v_61 ?v_94 (not (p5 c_2 ?v_98)) ?v_60) (or ?v_61 ?v_94 (not (p5 c_3 ?v_98)) ?v_61) (or ?v_61 ?v_94 (not (p5 c_4 ?v_98)) ?v_62) (or ?v_61 ?v_94 (not (p5 c_5 ?v_98)) ?v_63) (or ?v_61 ?v_94 (not (p5 c_6 ?v_98)) ?v_64) (or ?v_68 ?v_94 (not (p5 c_0 ?v_99)) ?v_30) (or ?v_68 ?v_94 (not (p5 c_1 ?v_99)) ?v_65) (or ?v_68 ?v_94 (not (p5 c_2 ?v_99)) ?v_67) (or ?v_68 ?v_94 (not (p5 c_3 ?v_99)) ?v_68) (or ?v_68 ?v_94 (not (p5 c_4 ?v_99)) ?v_69) (or ?v_68 ?v_94 (not (p5 c_5 ?v_99)) ?v_70) (or ?v_68 ?v_94 (not (p5 c_6 ?v_99)) ?v_71) (or ?v_75 ?v_94 (not (p5 c_0 ?v_100)) ?v_32) (or ?v_75 ?v_94 (not (p5 c_1 ?v_100)) ?v_72) (or ?v_75 ?v_94 (not (p5 c_2 ?v_100)) ?v_74) (or ?v_75 ?v_94 (not (p5 c_3 ?v_100)) ?v_75) (or ?v_75 ?v_94 (not (p5 c_4 ?v_100)) ?v_76) (or ?v_75 ?v_94 (not (p5 c_5 ?v_100)) ?v_77) (or ?v_75 ?v_94 (not (p5 c_6 ?v_100)) ?v_78) (or ?v_82 ?v_94 (not (p5 c_0 ?v_101)) ?v_34) (or ?v_82 ?v_94 (not (p5 c_1 ?v_101)) ?v_79) (or ?v_82 ?v_94 (not (p5 c_2 ?v_101)) ?v_81) (or ?v_82 ?v_94 (not (p5 c_3 ?v_101)) ?v_82) (or ?v_82 ?v_94 (not (p5 c_4 ?v_101)) ?v_83) (or ?v_82 ?v_94 (not (p5 c_5 ?v_101)) ?v_84) (or ?v_82 ?v_94 (not (p5 c_6 ?v_101)) ?v_85) (or ?v_41 ?v_102 (not (p5 c_0 ?v_103)) ?v_21) (or ?v_41 ?v_102 (not (p5 c_1 ?v_103)) ?v_36) (or ?v_41 ?v_102 (not (p5 c_2 ?v_103)) ?v_39) (or ?v_41 ?v_102 (not (p5 c_3 ?v_103)) ?v_40) (or ?v_41 ?v_102 (not (p5 c_4 ?v_103)) ?v_41) (or ?v_41 ?v_102 (not (p5 c_5 ?v_103)) ?v_42) (or ?v_41 ?v_102 (not (p5 c_6 ?v_103)) ?v_43) (or ?v_48 ?v_102 (not (p5 c_0 ?v_104)) ?v_24) (or ?v_48 ?v_102 (not (p5 c_1 ?v_104)) ?v_44) (or ?v_48 ?v_102 (not (p5 c_2 ?v_104)) ?v_46) (or ?v_48 ?v_102 (not (p5 c_3 ?v_104)) ?v_47) (or ?v_48 ?v_102 (not (p5 c_4 ?v_104)) ?v_48) (or ?v_48 ?v_102 (not (p5 c_5 ?v_104)) ?v_49) (or ?v_48 ?v_102 (not (p5 c_6 ?v_104)) ?v_50) (or ?v_55 ?v_102 (not (p5 c_0 ?v_105)) ?v_26) (or ?v_55 ?v_102 (not (p5 c_1 ?v_105)) ?v_51) (or ?v_55 ?v_102 (not (p5 c_2 ?v_105)) ?v_53) (or ?v_55 ?v_102 (not (p5 c_3 ?v_105)) ?v_54) (or ?v_55 ?v_102 (not (p5 c_4 ?v_105)) ?v_55) (or ?v_55 ?v_102 (not (p5 c_5 ?v_105)) ?v_56) (or ?v_55 ?v_102 (not (p5 c_6 ?v_105)) ?v_57) (or ?v_62 ?v_102 (not (p5 c_0 ?v_106)) ?v_28) (or ?v_62 ?v_102 (not (p5 c_1 ?v_106)) ?v_58) (or ?v_62 ?v_102 (not (p5 c_2 ?v_106)) ?v_60) (or ?v_62 ?v_102 (not (p5 c_3 ?v_106)) ?v_61) (or ?v_62 ?v_102 (not (p5 c_4 ?v_106)) ?v_62) (or ?v_62 ?v_102 (not (p5 c_5 ?v_106)) ?v_63) (or ?v_62 ?v_102 (not (p5 c_6 ?v_106)) ?v_64) (or ?v_69 ?v_102 (not (p5 c_0 ?v_107)) ?v_30) (or ?v_69 ?v_102 (not (p5 c_1 ?v_107)) ?v_65) (or ?v_69 ?v_102 (not (p5 c_2 ?v_107)) ?v_67) (or ?v_69 ?v_102 (not (p5 c_3 ?v_107)) ?v_68) (or ?v_69 ?v_102 (not (p5 c_4 ?v_107)) ?v_69) (or ?v_69 ?v_102 (not (p5 c_5 ?v_107)) ?v_70) (or ?v_69 ?v_102 (not (p5 c_6 ?v_107)) ?v_71) (or ?v_76 ?v_102 (not (p5 c_0 ?v_108)) ?v_32) (or ?v_76 ?v_102 (not (p5 c_1 ?v_108)) ?v_72) (or ?v_76 ?v_102 (not (p5 c_2 ?v_108)) ?v_74) (or ?v_76 ?v_102 (not (p5 c_3 ?v_108)) ?v_75) (or ?v_76 ?v_102 (not (p5 c_4 ?v_108)) ?v_76) (or ?v_76 ?v_102 (not (p5 c_5 ?v_108)) ?v_77) (or ?v_76 ?v_102 (not (p5 c_6 ?v_108)) ?v_78) (or ?v_83 ?v_102 (not (p5 c_0 ?v_109)) ?v_34) (or ?v_83 ?v_102 (not (p5 c_1 ?v_109)) ?v_79) (or ?v_83 ?v_102 (not (p5 c_2 ?v_109)) ?v_81) (or ?v_83 ?v_102 (not (p5 c_3 ?v_109)) ?v_82) (or ?v_83 ?v_102 (not (p5 c_4 ?v_109)) ?v_83) (or ?v_83 ?v_102 (not (p5 c_5 ?v_109)) ?v_84) (or ?v_83 ?v_102 (not (p5 c_6 ?v_109)) ?v_85) (or ?v_42 ?v_110 (not (p5 c_0 ?v_111)) ?v_21) (or ?v_42 ?v_110 (not (p5 c_1 ?v_111)) ?v_36) (or ?v_42 ?v_110 (not (p5 c_2 ?v_111)) ?v_39) (or ?v_42 ?v_110 (not (p5 c_3 ?v_111)) ?v_40) (or ?v_42 ?v_110 (not (p5 c_4 ?v_111)) ?v_41) (or ?v_42 ?v_110 (not (p5 c_5 ?v_111)) ?v_42) (or ?v_42 ?v_110 (not (p5 c_6 ?v_111)) ?v_43) (or ?v_49 ?v_110 (not (p5 c_0 ?v_112)) ?v_24) (or ?v_49 ?v_110 (not (p5 c_1 ?v_112)) ?v_44) (or ?v_49 ?v_110 (not (p5 c_2 ?v_112)) ?v_46) (or ?v_49 ?v_110 (not (p5 c_3 ?v_112)) ?v_47) (or ?v_49 ?v_110 (not (p5 c_4 ?v_112)) ?v_48) (or ?v_49 ?v_110 (not (p5 c_5 ?v_112)) ?v_49) (or ?v_49 ?v_110 (not (p5 c_6 ?v_112)) ?v_50) (or ?v_56 ?v_110 (not (p5 c_0 ?v_113)) ?v_26) (or ?v_56 ?v_110 (not (p5 c_1 ?v_113)) ?v_51) (or ?v_56 ?v_110 (not (p5 c_2 ?v_113)) ?v_53) (or ?v_56 ?v_110 (not (p5 c_3 ?v_113)) ?v_54) (or ?v_56 ?v_110 (not (p5 c_4 ?v_113)) ?v_55) (or ?v_56 ?v_110 (not (p5 c_5 ?v_113)) ?v_56) (or ?v_56 ?v_110 (not (p5 c_6 ?v_113)) ?v_57) (or ?v_63 ?v_110 (not (p5 c_0 ?v_114)) ?v_28) (or ?v_63 ?v_110 (not (p5 c_1 ?v_114)) ?v_58) (or ?v_63 ?v_110 (not (p5 c_2 ?v_114)) ?v_60) (or ?v_63 ?v_110 (not (p5 c_3 ?v_114)) ?v_61) (or ?v_63 ?v_110 (not (p5 c_4 ?v_114)) ?v_62) (or ?v_63 ?v_110 (not (p5 c_5 ?v_114)) ?v_63) (or ?v_63 ?v_110 (not (p5 c_6 ?v_114)) ?v_64) (or ?v_70 ?v_110 (not (p5 c_0 ?v_115)) ?v_30) (or ?v_70 ?v_110 (not (p5 c_1 ?v_115)) ?v_65) (or ?v_70 ?v_110 (not (p5 c_2 ?v_115)) ?v_67) (or ?v_70 ?v_110 (not (p5 c_3 ?v_115)) ?v_68) (or ?v_70 ?v_110 (not (p5 c_4 ?v_115)) ?v_69) (or ?v_70 ?v_110 (not (p5 c_5 ?v_115)) ?v_70) (or ?v_70 ?v_110 (not (p5 c_6 ?v_115)) ?v_71) (or ?v_77 ?v_110 (not (p5 c_0 ?v_116)) ?v_32) (or ?v_77 ?v_110 (not (p5 c_1 ?v_116)) ?v_72) (or ?v_77 ?v_110 (not (p5 c_2 ?v_116)) ?v_74) (or ?v_77 ?v_110 (not (p5 c_3 ?v_116)) ?v_75) (or ?v_77 ?v_110 (not (p5 c_4 ?v_116)) ?v_76) (or ?v_77 ?v_110 (not (p5 c_5 ?v_116)) ?v_77) (or ?v_77 ?v_110 (not (p5 c_6 ?v_116)) ?v_78) (or ?v_84 ?v_110 (not (p5 c_0 ?v_117)) ?v_34) (or ?v_84 ?v_110 (not (p5 c_1 ?v_117)) ?v_79) (or ?v_84 ?v_110 (not (p5 c_2 ?v_117)) ?v_81) (or ?v_84 ?v_110 (not (p5 c_3 ?v_117)) ?v_82) (or ?v_84 ?v_110 (not (p5 c_4 ?v_117)) ?v_83) (or ?v_84 ?v_110 (not (p5 c_5 ?v_117)) ?v_84) (or ?v_84 ?v_110 (not (p5 c_6 ?v_117)) ?v_85) (or ?v_43 ?v_118 (not (p5 c_0 ?v_119)) ?v_21) (or ?v_43 ?v_118 (not (p5 c_1 ?v_119)) ?v_36) (or ?v_43 ?v_118 (not (p5 c_2 ?v_119)) ?v_39) (or ?v_43 ?v_118 (not (p5 c_3 ?v_119)) ?v_40) (or ?v_43 ?v_118 (not (p5 c_4 ?v_119)) ?v_41) (or ?v_43 ?v_118 (not (p5 c_5 ?v_119)) ?v_42) (or ?v_43 ?v_118 (not (p5 c_6 ?v_119)) ?v_43) (or ?v_50 ?v_118 (not (p5 c_0 ?v_120)) ?v_24) (or ?v_50 ?v_118 (not (p5 c_1 ?v_120)) ?v_44) (or ?v_50 ?v_118 (not (p5 c_2 ?v_120)) ?v_46) (or ?v_50 ?v_118 (not (p5 c_3 ?v_120)) ?v_47) (or ?v_50 ?v_118 (not (p5 c_4 ?v_120)) ?v_48) (or ?v_50 ?v_118 (not (p5 c_5 ?v_120)) ?v_49) (or ?v_50 ?v_118 (not (p5 c_6 ?v_120)) ?v_50) (or ?v_57 ?v_118 (not (p5 c_0 ?v_121)) ?v_26) (or ?v_57 ?v_118 (not (p5 c_1 ?v_121)) ?v_51) (or ?v_57 ?v_118 (not (p5 c_2 ?v_121)) ?v_53) (or ?v_57 ?v_118 (not (p5 c_3 ?v_121)) ?v_54) (or ?v_57 ?v_118 (not (p5 c_4 ?v_121)) ?v_55) (or ?v_57 ?v_118 (not (p5 c_5 ?v_121)) ?v_56) (or ?v_57 ?v_118 (not (p5 c_6 ?v_121)) ?v_57) (or ?v_64 ?v_118 (not (p5 c_0 ?v_122)) ?v_28) (or ?v_64 ?v_118 (not (p5 c_1 ?v_122)) ?v_58) (or ?v_64 ?v_118 (not (p5 c_2 ?v_122)) ?v_60) (or ?v_64 ?v_118 (not (p5 c_3 ?v_122)) ?v_61) (or ?v_64 ?v_118 (not (p5 c_4 ?v_122)) ?v_62) (or ?v_64 ?v_118 (not (p5 c_5 ?v_122)) ?v_63) (or ?v_64 ?v_118 (not (p5 c_6 ?v_122)) ?v_64) (or ?v_71 ?v_118 (not (p5 c_0 ?v_123)) ?v_30) (or ?v_71 ?v_118 (not (p5 c_1 ?v_123)) ?v_65) (or ?v_71 ?v_118 (not (p5 c_2 ?v_123)) ?v_67) (or ?v_71 ?v_118 (not (p5 c_3 ?v_123)) ?v_68) (or ?v_71 ?v_118 (not (p5 c_4 ?v_123)) ?v_69) (or ?v_71 ?v_118 (not (p5 c_5 ?v_123)) ?v_70) (or ?v_71 ?v_118 (not (p5 c_6 ?v_123)) ?v_71) (or ?v_78 ?v_118 (not (p5 c_0 ?v_124)) ?v_32) (or ?v_78 ?v_118 (not (p5 c_1 ?v_124)) ?v_72) (or ?v_78 ?v_118 (not (p5 c_2 ?v_124)) ?v_74) (or ?v_78 ?v_118 (not (p5 c_3 ?v_124)) ?v_75) (or ?v_78 ?v_118 (not (p5 c_4 ?v_124)) ?v_76) (or ?v_78 ?v_118 (not (p5 c_5 ?v_124)) ?v_77) (or ?v_78 ?v_118 (not (p5 c_6 ?v_124)) ?v_78) (or ?v_85 ?v_118 (not (p5 c_0 ?v_125)) ?v_34) (or ?v_85 ?v_118 (not (p5 c_1 ?v_125)) ?v_79) (or ?v_85 ?v_118 (not (p5 c_2 ?v_125)) ?v_81) (or ?v_85 ?v_118 (not (p5 c_3 ?v_125)) ?v_82) (or ?v_85 ?v_118 (not (p5 c_4 ?v_125)) ?v_83) (or ?v_85 ?v_118 (not (p5 c_5 ?v_125)) ?v_84) (or ?v_85 ?v_118 (not (p5 c_6 ?v_125)) ?v_85) (or (p5 ?v_23 c_0) ?v_21 ?v_22) (or (p5 ?v_25 c_1) ?v_24 ?v_22) (or (p5 ?v_27 c_2) ?v_26 ?v_22) (or (p5 ?v_29 c_3) ?v_28 ?v_22) (or (p5 ?v_31 c_4) ?v_30 ?v_22) (or (p5 ?v_33 c_5) ?v_32 ?v_22) (or (p5 ?v_35 c_6) ?v_34 ?v_22) (or (p5 ?v_38 c_0) ?v_36 ?v_37) (or (p5 ?v_45 c_1) ?v_44 ?v_37) (or (p5 ?v_52 c_2) ?v_51 ?v_37) (or (p5 ?v_59 c_3) ?v_58 ?v_37) (or (p5 ?v_66 c_4) ?v_65 ?v_37) (or (p5 ?v_73 c_5) ?v_72 ?v_37) (or (p5 ?v_80 c_6) ?v_79 ?v_37) (or (p5 ?v_87 c_0) ?v_39 ?v_86) (or (p5 ?v_88 c_1) ?v_46 ?v_86) (or (p5 ?v_89 c_2) ?v_53 ?v_86) (or (p5 ?v_90 c_3) ?v_60 ?v_86) (or (p5 ?v_91 c_4) ?v_67 ?v_86) (or (p5 ?v_92 c_5) ?v_74 ?v_86) (or (p5 ?v_93 c_6) ?v_81 ?v_86) (or (p5 ?v_95 c_0) ?v_40 ?v_94) (or (p5 ?v_96 c_1) ?v_47 ?v_94) (or (p5 ?v_97 c_2) ?v_54 ?v_94) (or (p5 ?v_98 c_3) ?v_61 ?v_94) (or (p5 ?v_99 c_4) ?v_68 ?v_94) (or (p5 ?v_100 c_5) ?v_75 ?v_94) (or (p5 ?v_101 c_6) ?v_82 ?v_94) (or (p5 ?v_103 c_0) ?v_41 ?v_102) (or (p5 ?v_104 c_1) ?v_48 ?v_102) (or (p5 ?v_105 c_2) ?v_55 ?v_102) (or (p5 ?v_106 c_3) ?v_62 ?v_102) (or (p5 ?v_107 c_4) ?v_69 ?v_102) (or (p5 ?v_108 c_5) ?v_76 ?v_102) (or (p5 ?v_109 c_6) ?v_83 ?v_102) (or (p5 ?v_111 c_0) ?v_42 ?v_110) (or (p5 ?v_112 c_1) ?v_49 ?v_110) (or (p5 ?v_113 c_2) ?v_56 ?v_110) (or (p5 ?v_114 c_3) ?v_63 ?v_110) (or (p5 ?v_115 c_4) ?v_70 ?v_110) (or (p5 ?v_116 c_5) ?v_77 ?v_110) (or (p5 ?v_117 c_6) ?v_84 ?v_110) (or (p5 ?v_119 c_0) ?v_43 ?v_118) (or (p5 ?v_120 c_1) ?v_50 ?v_118) (or (p5 ?v_121 c_2) ?v_57 ?v_118) (or (p5 ?v_122 c_3) ?v_64 ?v_118) (or (p5 ?v_123 c_4) ?v_71 ?v_118) (or (p5 ?v_124 c_5) ?v_78 ?v_118) (or (p5 ?v_125 c_6) ?v_85 ?v_118) (or (not ?v_126) ?v_127) (or (not ?v_128) ?v_129) (or (not ?v_130) ?v_131) (or (not ?v_132) ?v_133) (or (not ?v_134) ?v_135) (or (not ?v_136) ?v_137) (or (not ?v_138) ?v_139) (or (not ?v_140) ?v_141) (or (not ?v_142) ?v_143) (or (not ?v_144) ?v_145) (or (not ?v_146) ?v_147) (or (not ?v_148) ?v_149) (or (not ?v_150) ?v_151) (or (not ?v_152) ?v_153) (or (not ?v_154) ?v_155) (or (not ?v_156) ?v_157) (or (not ?v_158) ?v_159) (or (not ?v_160) ?v_161) (or (not ?v_162) ?v_163) (or (not ?v_164) ?v_165) (or (not ?v_166) ?v_167) (or (not ?v_168) ?v_169) (or (not ?v_170) ?v_171) (or (not ?v_172) ?v_173) (or (not ?v_174) ?v_175) (or (not ?v_176) ?v_177) (or (not ?v_178) ?v_179) (or (not ?v_180) ?v_181) (or (not ?v_182) ?v_183) (or (not ?v_184) ?v_185) (or (not ?v_186) ?v_187) (or (not ?v_188) ?v_189) (or (not ?v_190) ?v_191) (or (not ?v_192) ?v_193) (or (not ?v_194) ?v_195) (or (not ?v_196) ?v_197) (or (not ?v_198) ?v_199) (or (not ?v_200) ?v_201) (or (not ?v_202) ?v_203) (or (not ?v_204) ?v_205) (or (not ?v_206) ?v_207) (or (not ?v_208) ?v_209) (or (not ?v_210) ?v_211) (or (not ?v_212) ?v_213) (or (not ?v_214) ?v_215) (or (not ?v_216) ?v_217) (or (not ?v_218) ?v_219) (or (not ?v_220) ?v_221) (or (not ?v_222) ?v_223) (or ?v_1 ?v_224) (or ?v_3 ?v_225) (or ?v_5 ?v_226) (or ?v_7 ?v_227) (or ?v_9 ?v_228) (or ?v_11 ?v_229) (or ?v_13 ?v_230) (or ?v_231 (p5 ?v_232 c_0) ?v_1) (or ?v_233 (p5 ?v_234 c_0) ?v_3) (or ?v_235 (p5 ?v_236 c_0) ?v_5) (or ?v_237 (p5 ?v_238 c_0) ?v_7) (or ?v_239 (p5 ?v_240 c_0) ?v_9) (or ?v_241 (p5 ?v_242 c_0) ?v_11) (or ?v_243 (p5 ?v_244 c_0) ?v_13) (or ?v_245 (p5 ?v_246 c_1) ?v_1) (or ?v_247 (p5 ?v_248 c_1) ?v_3) (or ?v_249 (p5 ?v_250 c_1) ?v_5) (or ?v_251 (p5 ?v_252 c_1) ?v_7) (or ?v_253 (p5 ?v_254 c_1) ?v_9) (or ?v_255 (p5 ?v_256 c_1) ?v_11) (or ?v_257 (p5 ?v_258 c_1) ?v_13) (or ?v_259 (p5 ?v_260 c_2) ?v_1) (or ?v_261 (p5 ?v_262 c_2) ?v_3) (or ?v_263 (p5 ?v_264 c_2) ?v_5) (or ?v_265 (p5 ?v_266 c_2) ?v_7) (or ?v_267 (p5 ?v_268 c_2) ?v_9) (or ?v_269 (p5 ?v_270 c_2) ?v_11) (or ?v_271 (p5 ?v_272 c_2) ?v_13) (or ?v_273 (p5 ?v_274 c_3) ?v_1) (or ?v_275 (p5 ?v_276 c_3) ?v_3) (or ?v_277 (p5 ?v_278 c_3) ?v_5) (or ?v_279 (p5 ?v_280 c_3) ?v_7) (or ?v_281 (p5 ?v_282 c_3) ?v_9) (or ?v_283 (p5 ?v_284 c_3) ?v_11) (or ?v_285 (p5 ?v_286 c_3) ?v_13) (or ?v_287 (p5 ?v_288 c_4) ?v_1) (or ?v_289 (p5 ?v_290 c_4) ?v_3) (or ?v_291 (p5 ?v_292 c_4) ?v_5) (or ?v_293 (p5 ?v_294 c_4) ?v_7) (or ?v_295 (p5 ?v_296 c_4) ?v_9) (or ?v_297 (p5 ?v_298 c_4) ?v_11) (or ?v_299 (p5 ?v_300 c_4) ?v_13) (or ?v_301 (p5 ?v_302 c_5) ?v_1) (or ?v_303 (p5 ?v_304 c_5) ?v_3) (or ?v_305 (p5 ?v_306 c_5) ?v_5) (or ?v_307 (p5 ?v_308 c_5) ?v_7) (or ?v_309 (p5 ?v_310 c_5) ?v_9) (or ?v_311 (p5 ?v_312 c_5) ?v_11) (or ?v_313 (p5 ?v_314 c_5) ?v_13) (or ?v_315 (p5 ?v_316 c_6) ?v_1) (or ?v_317 (p5 ?v_318 c_6) ?v_3) (or ?v_319 (p5 ?v_320 c_6) ?v_5) (or ?v_321 (p5 ?v_322 c_6) ?v_7) (or ?v_323 (p5 ?v_324 c_6) ?v_9) (or ?v_325 (p5 ?v_326 c_6) ?v_11) (or ?v_327 (p5 ?v_328 c_6) ?v_13) (or (= ?v_232 c_0) (= ?v_232 c_1) (= ?v_232 c_2) (= ?v_232 c_3) (= ?v_232 c_4) (= ?v_232 c_5) (= ?v_232 c_6)) (or (= ?v_246 c_0) (= ?v_246 c_1) (= ?v_246 c_2) (= ?v_246 c_3) (= ?v_246 c_4) (= ?v_246 c_5) (= ?v_246 c_6)) (or (= ?v_260 c_0) (= ?v_260 c_1) (= ?v_260 c_2) (= ?v_260 c_3) (= ?v_260 c_4) (= ?v_260 c_5) (= ?v_260 c_6)) (or (= ?v_274 c_0) (= ?v_274 c_1) (= ?v_274 c_2) (= ?v_274 c_3) (= ?v_274 c_4) (= ?v_274 c_5) (= ?v_274 c_6)) (or (= ?v_288 c_0) (= ?v_288 c_1) (= ?v_288 c_2) (= ?v_288 c_3) (= ?v_288 c_4) (= ?v_288 c_5) (= ?v_288 c_6)) (or (= ?v_302 c_0) (= ?v_302 c_1) (= ?v_302 c_2) (= ?v_302 c_3) (= ?v_302 c_4) (= ?v_302 c_5) (= ?v_302 c_6)) (or (= ?v_316 c_0) (= ?v_316 c_1) (= ?v_316 c_2) (= ?v_316 c_3) (= ?v_316 c_4) (= ?v_316 c_5) (= ?v_316 c_6)) (or (= ?v_234 c_0) (= ?v_234 c_1) (= ?v_234 c_2) (= ?v_234 c_3) (= ?v_234 c_4) (= ?v_234 c_5) (= ?v_234 c_6)) (or (= ?v_248 c_0) (= ?v_248 c_1) (= ?v_248 c_2) (= ?v_248 c_3) (= ?v_248 c_4) (= ?v_248 c_5) (= ?v_248 c_6)) (or (= ?v_262 c_0) (= ?v_262 c_1) (= ?v_262 c_2) (= ?v_262 c_3) (= ?v_262 c_4) (= ?v_262 c_5) (= ?v_262 c_6)) (or (= ?v_276 c_0) (= ?v_276 c_1) (= ?v_276 c_2) (= ?v_276 c_3) (= ?v_276 c_4) (= ?v_276 c_5) (= ?v_276 c_6)) (or (= ?v_290 c_0) (= ?v_290 c_1) (= ?v_290 c_2) (= ?v_290 c_3) (= ?v_290 c_4) (= ?v_290 c_5) (= ?v_290 c_6)) (or (= ?v_304 c_0) (= ?v_304 c_1) (= ?v_304 c_2) (= ?v_304 c_3) (= ?v_304 c_4) (= ?v_304 c_5) (= ?v_304 c_6)) (or (= ?v_318 c_0) (= ?v_318 c_1) (= ?v_318 c_2) (= ?v_318 c_3) (= ?v_318 c_4) (= ?v_318 c_5) (= ?v_318 c_6)) (or (= ?v_236 c_0) (= ?v_236 c_1) (= ?v_236 c_2) (= ?v_236 c_3) (= ?v_236 c_4) (= ?v_236 c_5) (= ?v_236 c_6)) (or (= ?v_250 c_0) (= ?v_250 c_1) (= ?v_250 c_2) (= ?v_250 c_3) (= ?v_250 c_4) (= ?v_250 c_5) (= ?v_250 c_6)) (or (= ?v_264 c_0) (= ?v_264 c_1) (= ?v_264 c_2) (= ?v_264 c_3) (= ?v_264 c_4) (= ?v_264 c_5) (= ?v_264 c_6)) (or (= ?v_278 c_0) (= ?v_278 c_1) (= ?v_278 c_2) (= ?v_278 c_3) (= ?v_278 c_4) (= ?v_278 c_5) (= ?v_278 c_6)) (or (= ?v_292 c_0) (= ?v_292 c_1) (= ?v_292 c_2) (= ?v_292 c_3) (= ?v_292 c_4) (= ?v_292 c_5) (= ?v_292 c_6)) (or (= ?v_306 c_0) (= ?v_306 c_1) (= ?v_306 c_2) (= ?v_306 c_3) (= ?v_306 c_4) (= ?v_306 c_5) (= ?v_306 c_6)) (or (= ?v_320 c_0) (= ?v_320 c_1) (= ?v_320 c_2) (= ?v_320 c_3) (= ?v_320 c_4) (= ?v_320 c_5) (= ?v_320 c_6)) (or (= ?v_238 c_0) (= ?v_238 c_1) (= ?v_238 c_2) (= ?v_238 c_3) (= ?v_238 c_4) (= ?v_238 c_5) (= ?v_238 c_6)) (or (= ?v_252 c_0) (= ?v_252 c_1) (= ?v_252 c_2) (= ?v_252 c_3) (= ?v_252 c_4) (= ?v_252 c_5) (= ?v_252 c_6)) (or (= ?v_266 c_0) (= ?v_266 c_1) (= ?v_266 c_2) (= ?v_266 c_3) (= ?v_266 c_4) (= ?v_266 c_5) (= ?v_266 c_6)) (or (= ?v_280 c_0) (= ?v_280 c_1) (= ?v_280 c_2) (= ?v_280 c_3) (= ?v_280 c_4) (= ?v_280 c_5) (= ?v_280 c_6)) (or (= ?v_294 c_0) (= ?v_294 c_1) (= ?v_294 c_2) (= ?v_294 c_3) (= ?v_294 c_4) (= ?v_294 c_5) (= ?v_294 c_6)) (or (= ?v_308 c_0) (= ?v_308 c_1) (= ?v_308 c_2) (= ?v_308 c_3) (= ?v_308 c_4) (= ?v_308 c_5) (= ?v_308 c_6)) (or (= ?v_322 c_0) (= ?v_322 c_1) (= ?v_322 c_2) (= ?v_322 c_3) (= ?v_322 c_4) (= ?v_322 c_5) (= ?v_322 c_6)) (or (= ?v_240 c_0) (= ?v_240 c_1) (= ?v_240 c_2) (= ?v_240 c_3) (= ?v_240 c_4) (= ?v_240 c_5) (= ?v_240 c_6)) (or (= ?v_254 c_0) (= ?v_254 c_1) (= ?v_254 c_2) (= ?v_254 c_3) (= ?v_254 c_4) (= ?v_254 c_5) (= ?v_254 c_6)) (or (= ?v_268 c_0) (= ?v_268 c_1) (= ?v_268 c_2) (= ?v_268 c_3) (= ?v_268 c_4) (= ?v_268 c_5) (= ?v_268 c_6)) (or (= ?v_282 c_0) (= ?v_282 c_1) (= ?v_282 c_2) (= ?v_282 c_3) (= ?v_282 c_4) (= ?v_282 c_5) (= ?v_282 c_6)) (or (= ?v_296 c_0) (= ?v_296 c_1) (= ?v_296 c_2) (= ?v_296 c_3) (= ?v_296 c_4) (= ?v_296 c_5) (= ?v_296 c_6)) (or (= ?v_310 c_0) (= ?v_310 c_1) (= ?v_310 c_2) (= ?v_310 c_3) (= ?v_310 c_4) (= ?v_310 c_5) (= ?v_310 c_6)) (or (= ?v_324 c_0) (= ?v_324 c_1) (= ?v_324 c_2) (= ?v_324 c_3) (= ?v_324 c_4) (= ?v_324 c_5) (= ?v_324 c_6)) (or (= ?v_242 c_0) (= ?v_242 c_1) (= ?v_242 c_2) (= ?v_242 c_3) (= ?v_242 c_4) (= ?v_242 c_5) (= ?v_242 c_6)) (or (= ?v_256 c_0) (= ?v_256 c_1) (= ?v_256 c_2) (= ?v_256 c_3) (= ?v_256 c_4) (= ?v_256 c_5) (= ?v_256 c_6)) (or (= ?v_270 c_0) (= ?v_270 c_1) (= ?v_270 c_2) (= ?v_270 c_3) (= ?v_270 c_4) (= ?v_270 c_5) (= ?v_270 c_6)) (or (= ?v_284 c_0) (= ?v_284 c_1) (= ?v_284 c_2) (= ?v_284 c_3) (= ?v_284 c_4) (= ?v_284 c_5) (= ?v_284 c_6)) (or (= ?v_298 c_0) (= ?v_298 c_1) (= ?v_298 c_2) (= ?v_298 c_3) (= ?v_298 c_4) (= ?v_298 c_5) (= ?v_298 c_6)) (or (= ?v_312 c_0) (= ?v_312 c_1) (= ?v_312 c_2) (= ?v_312 c_3) (= ?v_312 c_4) (= ?v_312 c_5) (= ?v_312 c_6)) (or (= ?v_326 c_0) (= ?v_326 c_1) (= ?v_326 c_2) (= ?v_326 c_3) (= ?v_326 c_4) (= ?v_326 c_5) (= ?v_326 c_6)) (or (= ?v_244 c_0) (= ?v_244 c_1) (= ?v_244 c_2) (= ?v_244 c_3) (= ?v_244 c_4) (= ?v_244 c_5) (= ?v_244 c_6)) (or (= ?v_258 c_0) (= ?v_258 c_1) (= ?v_258 c_2) (= ?v_258 c_3) (= ?v_258 c_4) (= ?v_258 c_5) (= ?v_258 c_6)) (or (= ?v_272 c_0) (= ?v_272 c_1) (= ?v_272 c_2) (= ?v_272 c_3) (= ?v_272 c_4) (= ?v_272 c_5) (= ?v_272 c_6)) (or (= ?v_286 c_0) (= ?v_286 c_1) (= ?v_286 c_2) (= ?v_286 c_3) (= ?v_286 c_4) (= ?v_286 c_5) (= ?v_286 c_6)) (or (= ?v_300 c_0) (= ?v_300 c_1) (= ?v_300 c_2) (= ?v_300 c_3) (= ?v_300 c_4) (= ?v_300 c_5) (= ?v_300 c_6)) (or (= ?v_314 c_0) (= ?v_314 c_1) (= ?v_314 c_2) (= ?v_314 c_3) (= ?v_314 c_4) (= ?v_314 c_5) (= ?v_314 c_6)) (or (= ?v_328 c_0) (= ?v_328 c_1) (= ?v_328 c_2) (= ?v_328 c_3) (= ?v_328 c_4) (= ?v_328 c_5) (= ?v_328 c_6)) (or (= ?v_23 c_0) (= ?v_23 c_1) (= ?v_23 c_2) (= ?v_23 c_3) (= ?v_23 c_4) (= ?v_23 c_5) (= ?v_23 c_6)) (or (= ?v_25 c_0) (= ?v_25 c_1) (= ?v_25 c_2) (= ?v_25 c_3) (= ?v_25 c_4) (= ?v_25 c_5) (= ?v_25 c_6)) (or (= ?v_27 c_0) (= ?v_27 c_1) (= ?v_27 c_2) (= ?v_27 c_3) (= ?v_27 c_4) (= ?v_27 c_5) (= ?v_27 c_6)) (or (= ?v_29 c_0) (= ?v_29 c_1) (= ?v_29 c_2) (= ?v_29 c_3) (= ?v_29 c_4) (= ?v_29 c_5) (= ?v_29 c_6)) (or (= ?v_31 c_0) (= ?v_31 c_1) (= ?v_31 c_2) (= ?v_31 c_3) (= ?v_31 c_4) (= ?v_31 c_5) (= ?v_31 c_6)) (or (= ?v_33 c_0) (= ?v_33 c_1) (= ?v_33 c_2) (= ?v_33 c_3) (= ?v_33 c_4) (= ?v_33 c_5) (= ?v_33 c_6)) (or (= ?v_35 c_0) (= ?v_35 c_1) (= ?v_35 c_2) (= ?v_35 c_3) (= ?v_35 c_4) (= ?v_35 c_5) (= ?v_35 c_6)) (or (= ?v_38 c_0) (= ?v_38 c_1) (= ?v_38 c_2) (= ?v_38 c_3) (= ?v_38 c_4) (= ?v_38 c_5) (= ?v_38 c_6)) (or (= ?v_45 c_0) (= ?v_45 c_1) (= ?v_45 c_2) (= ?v_45 c_3) (= ?v_45 c_4) (= ?v_45 c_5) (= ?v_45 c_6)) (or (= ?v_52 c_0) (= ?v_52 c_1) (= ?v_52 c_2) (= ?v_52 c_3) (= ?v_52 c_4) (= ?v_52 c_5) (= ?v_52 c_6)) (or (= ?v_59 c_0) (= ?v_59 c_1) (= ?v_59 c_2) (= ?v_59 c_3) (= ?v_59 c_4) (= ?v_59 c_5) (= ?v_59 c_6)) (or (= ?v_66 c_0) (= ?v_66 c_1) (= ?v_66 c_2) (= ?v_66 c_3) (= ?v_66 c_4) (= ?v_66 c_5) (= ?v_66 c_6)) (or (= ?v_73 c_0) (= ?v_73 c_1) (= ?v_73 c_2) (= ?v_73 c_3) (= ?v_73 c_4) (= ?v_73 c_5) (= ?v_73 c_6)) (or (= ?v_80 c_0) (= ?v_80 c_1) (= ?v_80 c_2) (= ?v_80 c_3) (= ?v_80 c_4) (= ?v_80 c_5) (= ?v_80 c_6)) (or (= ?v_87 c_0) (= ?v_87 c_1) (= ?v_87 c_2) (= ?v_87 c_3) (= ?v_87 c_4) (= ?v_87 c_5) (= ?v_87 c_6)) (or (= ?v_88 c_0) (= ?v_88 c_1) (= ?v_88 c_2) (= ?v_88 c_3) (= ?v_88 c_4) (= ?v_88 c_5) (= ?v_88 c_6)) (or (= ?v_89 c_0) (= ?v_89 c_1) (= ?v_89 c_2) (= ?v_89 c_3) (= ?v_89 c_4) (= ?v_89 c_5) (= ?v_89 c_6)) (or (= ?v_90 c_0) (= ?v_90 c_1) (= ?v_90 c_2) (= ?v_90 c_3) (= ?v_90 c_4) (= ?v_90 c_5) (= ?v_90 c_6)) (or (= ?v_91 c_0) (= ?v_91 c_1) (= ?v_91 c_2) (= ?v_91 c_3) (= ?v_91 c_4) (= ?v_91 c_5) (= ?v_91 c_6)) (or (= ?v_92 c_0) (= ?v_92 c_1) (= ?v_92 c_2) (= ?v_92 c_3) (= ?v_92 c_4) (= ?v_92 c_5) (= ?v_92 c_6)) (or (= ?v_93 c_0) (= ?v_93 c_1) (= ?v_93 c_2) (= ?v_93 c_3) (= ?v_93 c_4) (= ?v_93 c_5) (= ?v_93 c_6)) (or (= ?v_95 c_0) (= ?v_95 c_1) (= ?v_95 c_2) (= ?v_95 c_3) (= ?v_95 c_4) (= ?v_95 c_5) (= ?v_95 c_6)) (or (= ?v_96 c_0) (= ?v_96 c_1) (= ?v_96 c_2) (= ?v_96 c_3) (= ?v_96 c_4) (= ?v_96 c_5) (= ?v_96 c_6)) (or (= ?v_97 c_0) (= ?v_97 c_1) (= ?v_97 c_2) (= ?v_97 c_3) (= ?v_97 c_4) (= ?v_97 c_5) (= ?v_97 c_6)) (or (= ?v_98 c_0) (= ?v_98 c_1) (= ?v_98 c_2) (= ?v_98 c_3) (= ?v_98 c_4) (= ?v_98 c_5) (= ?v_98 c_6)) (or (= ?v_99 c_0) (= ?v_99 c_1) (= ?v_99 c_2) (= ?v_99 c_3) (= ?v_99 c_4) (= ?v_99 c_5) (= ?v_99 c_6)) (or (= ?v_100 c_0) (= ?v_100 c_1) (= ?v_100 c_2) (= ?v_100 c_3) (= ?v_100 c_4) (= ?v_100 c_5) (= ?v_100 c_6)) (or (= ?v_101 c_0) (= ?v_101 c_1) (= ?v_101 c_2) (= ?v_101 c_3) (= ?v_101 c_4) (= ?v_101 c_5) (= ?v_101 c_6)) (or (= ?v_103 c_0) (= ?v_103 c_1) (= ?v_103 c_2) (= ?v_103 c_3) (= ?v_103 c_4) (= ?v_103 c_5) (= ?v_103 c_6)) (or (= ?v_104 c_0) (= ?v_104 c_1) (= ?v_104 c_2) (= ?v_104 c_3) (= ?v_104 c_4) (= ?v_104 c_5) (= ?v_104 c_6)) (or (= ?v_105 c_0) (= ?v_105 c_1) (= ?v_105 c_2) (= ?v_105 c_3) (= ?v_105 c_4) (= ?v_105 c_5) (= ?v_105 c_6)) (or (= ?v_106 c_0) (= ?v_106 c_1) (= ?v_106 c_2) (= ?v_106 c_3) (= ?v_106 c_4) (= ?v_106 c_5) (= ?v_106 c_6)) (or (= ?v_107 c_0) (= ?v_107 c_1) (= ?v_107 c_2) (= ?v_107 c_3) (= ?v_107 c_4) (= ?v_107 c_5) (= ?v_107 c_6)) (or (= ?v_108 c_0) (= ?v_108 c_1) (= ?v_108 c_2) (= ?v_108 c_3) (= ?v_108 c_4) (= ?v_108 c_5) (= ?v_108 c_6)) (or (= ?v_109 c_0) (= ?v_109 c_1) (= ?v_109 c_2) (= ?v_109 c_3) (= ?v_109 c_4) (= ?v_109 c_5) (= ?v_109 c_6)) (or (= ?v_111 c_0) (= ?v_111 c_1) (= ?v_111 c_2) (= ?v_111 c_3) (= ?v_111 c_4) (= ?v_111 c_5) (= ?v_111 c_6)) (or (= ?v_112 c_0) (= ?v_112 c_1) (= ?v_112 c_2) (= ?v_112 c_3) (= ?v_112 c_4) (= ?v_112 c_5) (= ?v_112 c_6)) (or (= ?v_113 c_0) (= ?v_113 c_1) (= ?v_113 c_2) (= ?v_113 c_3) (= ?v_113 c_4) (= ?v_113 c_5) (= ?v_113 c_6)) (or (= ?v_114 c_0) (= ?v_114 c_1) (= ?v_114 c_2) (= ?v_114 c_3) (= ?v_114 c_4) (= ?v_114 c_5) (= ?v_114 c_6)) (or (= ?v_115 c_0) (= ?v_115 c_1) (= ?v_115 c_2) (= ?v_115 c_3) (= ?v_115 c_4) (= ?v_115 c_5) (= ?v_115 c_6)) (or (= ?v_116 c_0) (= ?v_116 c_1) (= ?v_116 c_2) (= ?v_116 c_3) (= ?v_116 c_4) (= ?v_116 c_5) (= ?v_116 c_6)) (or (= ?v_117 c_0) (= ?v_117 c_1) (= ?v_117 c_2) (= ?v_117 c_3) (= ?v_117 c_4) (= ?v_117 c_5) (= ?v_117 c_6)) (or (= ?v_119 c_0) (= ?v_119 c_1) (= ?v_119 c_2) (= ?v_119 c_3) (= ?v_119 c_4) (= ?v_119 c_5) (= ?v_119 c_6)) (or (= ?v_120 c_0) (= ?v_120 c_1) (= ?v_120 c_2) (= ?v_120 c_3) (= ?v_120 c_4) (= ?v_120 c_5) (= ?v_120 c_6)) (or (= ?v_121 c_0) (= ?v_121 c_1) (= ?v_121 c_2) (= ?v_121 c_3) (= ?v_121 c_4) (= ?v_121 c_5) (= ?v_121 c_6)) (or (= ?v_122 c_0) (= ?v_122 c_1) (= ?v_122 c_2) (= ?v_122 c_3) (= ?v_122 c_4) (= ?v_122 c_5) (= ?v_122 c_6)) (or (= ?v_123 c_0) (= ?v_123 c_1) (= ?v_123 c_2) (= ?v_123 c_3) (= ?v_123 c_4) (= ?v_123 c_5) (= ?v_123 c_6)) (or (= ?v_124 c_0) (= ?v_124 c_1) (= ?v_124 c_2) (= ?v_124 c_3) (= ?v_124 c_4) (= ?v_124 c_5) (= ?v_124 c_6)) (or (= ?v_125 c_0) (= ?v_125 c_1) (= ?v_125 c_2) (= ?v_125 c_3) (= ?v_125 c_4) (= ?v_125 c_5) (= ?v_125 c_6)) (or (= ?v_0 c_0) (= ?v_0 c_1) (= ?v_0 c_2) (= ?v_0 c_3) (= ?v_0 c_4) (= ?v_0 c_5) (= ?v_0 c_6)) (or (= ?v_2 c_0) (= ?v_2 c_1) (= ?v_2 c_2) (= ?v_2 c_3) (= ?v_2 c_4) (= ?v_2 c_5) (= ?v_2 c_6)) (or (= ?v_4 c_0) (= ?v_4 c_1) (= ?v_4 c_2) (= ?v_4 c_3) (= ?v_4 c_4) (= ?v_4 c_5) (= ?v_4 c_6)) (or (= ?v_6 c_0) (= ?v_6 c_1) (= ?v_6 c_2) (= ?v_6 c_3) (= ?v_6 c_4) (= ?v_6 c_5) (= ?v_6 c_6)) (or (= ?v_8 c_0) (= ?v_8 c_1) (= ?v_8 c_2) (= ?v_8 c_3) (= ?v_8 c_4) (= ?v_8 c_5) (= ?v_8 c_6)) (or (= ?v_10 c_0) (= ?v_10 c_1) (= ?v_10 c_2) (= ?v_10 c_3) (= ?v_10 c_4) (= ?v_10 c_5) (= ?v_10 c_6)) (or (= ?v_12 c_0) (= ?v_12 c_1) (= ?v_12 c_2) (= ?v_12 c_3) (= ?v_12 c_4) (= ?v_12 c_5) (= ?v_12 c_6)) (or (= ?v_14 c_0) (= ?v_14 c_1) (= ?v_14 c_2) (= ?v_14 c_3) (= ?v_14 c_4) (= ?v_14 c_5) (= ?v_14 c_6)) (or (= ?v_15 c_0) (= ?v_15 c_1) (= ?v_15 c_2) (= ?v_15 c_3) (= ?v_15 c_4) (= ?v_15 c_5) (= ?v_15 c_6)) (or (= ?v_16 c_0) (= ?v_16 c_1) (= ?v_16 c_2) (= ?v_16 c_3) (= ?v_16 c_4) (= ?v_16 c_5) (= ?v_16 c_6)) (or (= ?v_17 c_0) (= ?v_17 c_1) (= ?v_17 c_2) (= ?v_17 c_3) (= ?v_17 c_4) (= ?v_17 c_5) (= ?v_17 c_6)) (or (= ?v_18 c_0) (= ?v_18 c_1) (= ?v_18 c_2) (= ?v_18 c_3) (= ?v_18 c_4) (= ?v_18 c_5) (= ?v_18 c_6)) (or (= ?v_19 c_0) (= ?v_19 c_1) (= ?v_19 c_2) (= ?v_19 c_3) (= ?v_19 c_4) (= ?v_19 c_5) (= ?v_19 c_6)) (or (= ?v_20 c_0) (= ?v_20 c_1) (= ?v_20 c_2) (= ?v_20 c_3) (= ?v_20 c_4) (= ?v_20 c_5) (= ?v_20 c_6)) (or (= c6 c_0) (= c6 c_1) (= c6 c_2) (= c6 c_3) (= c6 c_4) (= c6 c_5) (= c6 c_6))))))))))))))))))))))))))
(check-sat)
(exit)