%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : SYO593+1 : TPTP v8.1.0. Bugfixed v5.5.1. % Transfm : none % Format : tptp:raw % Command : sos-script %s % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 21 19:49:48 EDT 2022 % Result : Unknown 0.19s 0.46s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.11 % Problem : SYO593+1 : TPTP v8.1.0. Bugfixed v5.5.1. % 0.12/0.12 % Command : sos-script %s % 0.12/0.33 % Computer : n015.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Sat Jul 9 14:51:07 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.45 ----- Otter 3.2, August 2001 ----- % 0.19/0.45 The process was started by sandbox on n015.cluster.edu, % 0.19/0.45 Sat Jul 9 14:51:07 2022 % 0.19/0.45 The command was "./sos". The process ID is 9269. % 0.19/0.45 % 0.19/0.45 set(prolog_style_variables). % 0.19/0.45 set(auto). % 0.19/0.45 dependent: set(auto1). % 0.19/0.45 dependent: set(process_input). % 0.19/0.45 dependent: clear(print_kept). % 0.19/0.45 dependent: clear(print_new_demod). % 0.19/0.45 dependent: clear(print_back_demod). % 0.19/0.45 dependent: clear(print_back_sub). % 0.19/0.45 dependent: set(control_memory). % 0.19/0.45 dependent: assign(max_mem, 12000). % 0.19/0.45 dependent: assign(pick_given_ratio, 4). % 0.19/0.45 dependent: assign(stats_level, 1). % 0.19/0.45 dependent: assign(pick_semantic_ratio, 3). % 0.19/0.45 dependent: assign(sos_limit, 5000). % 0.19/0.45 dependent: assign(max_weight, 60). % 0.19/0.45 clear(print_given). % 0.19/0.45 % 0.19/0.45 formula_list(usable). % 0.19/0.45 % 0.19/0.45 ERROR, term too big: % 0.19/0.45 % 0.19/0.45 % 0.19/0.45 ( exists V532 V1 V531 ( % 0.19/0.45 ( all V124 ( % 0.19/0.45 ( exists V152 V530 V7 V6 V5 V4 V3 V2 V155 V529 ( % 0.19/0.45 ( all V125 V126 ( % 0.19/0.45 ( exists V158 V528 V17 V16 V15 V14 V13 V12 V11 V10 V9 V8 V161 V167 V170 V173 V175 V176 V527 ( % 0.19/0.45 ( all V127 V128 ( % 0.19/0.45 ( exists V180 V526 V27 V26 V25 V24 V23 V22 V21 V20 V19 V18 V183 V189 V192 V195 V198 V201 V203 V205 V206 V525 ( % 0.19/0.45 ( all V129 V130 ( % 0.19/0.45 ( exists V210 V524 V37 V36 V35 V34 V33 V32 V31 V30 V29 V28 V213 V219 V222 V225 V228 V231 V233 V235 V236 V523 ( % 0.19/0.45 ( all V131 V132 ( % 0.19/0.45 ( exists V240 V522 V47 V46 V45 V44 V43 V42 V41 V40 V39 V38 V243 V249 V252 V255 V258 V261 V263 V265 V266 V521 ( % 0.19/0.45 ( all V133 V134 ( % 0.19/0.45 ( exists V270 V520 V55 V54 V53 V52 V51 V50 V49 V48 V273 V278 V281 V284 V287 V290 V292 V294 V295 V519 ( % 0.19/0.45 ( all V135 V136 ( % 0.19/0.45 ( exists V298 V518 V62 V61 V60 V59 V58 V57 V56 V301 V306 V309 V312 V314 V316 V317 V517 ( % 0.19/0.45 ( all V137 V138 ( % 0.19/0.45 ( exists V320 V516 V72 V71 V70 V69 V68 V67 V66 V65 V64 V63 V323 V329 V332 V335 V337 V338 V515 ( % 0.19/0.45 ( all V139 V140 ( % 0.19/0.45 ( exists V342 V514 V82 V81 V80 V79 V78 V77 V76 V75 V74 V73 V345 V351 V354 V357 V360 V363 V365 V367 V368 V513 ( % 0.19/0.45 ( all V141 V142 ( % 0.19/0.45 ( exists V372 V512 V90 V89 V88 V87 V86 V85 V84 V83 V375 V380 V383 V386 V389 V392 V394 V396 V397 V511 ( % 0.19/0.45 ( all V143 V144 ( % 0.19/0.45 ( exists V400 V510 V102 V101 V100 V99 V98 V97 V96 V95 V94 V93 V92 V91 V403 V410 V413 V416 V419 V421 V422 V509 ( % 0.19/0.45 ( all V145 V146 ( % 0.19/0.45 ( exists V426 V508 V111 V110 V109 V108 V107 V106 V105 V104 V103 V429 V432 V435 V438 V441 V444 V447 V450 V453 V455 V456 V507 ( % 0.19/0.45 ( all V147 V148 ( % 0.19/0.45 ( exists V459 V506 V117 V116 V115 V114 V113 V112 V462 V466 V469 V472 V475 V478 V480 V481 V505 ( % 0.19/0.45 ( all V149 V150 ( % 0.19/0.45 ( exists V484 V504 V121 V120 V119 V118 V487 V490 V493 V495 V496 V503 ( % 0.19/0.45 ( all V151 ( % 0.19/0.45 ( exists V497 V502 V123 V122 V499 V500 V501 V498 V494 V491 V492 V489 V488 V486 V485 V482 V483 V479 V476 V477 V474 V473 V471 V470 V468 V467 V464 V465 V463 V461 V460 V457 V458 V454 V451 V452 V448 V449 V446 V445 V443 V442 V440 V439 V437 V436 V434 V433 V431 V430 V428 V427 V423 V424 V425 V420 V417 V418 V415 V414 V412 V411 V405 V409 V406 V407 V408 V404 V402 V401 V398 V399 V395 V393 V390 V391 V388 V387 V385 V384 V382 V381 V377 V379 V378 V376 V374 V373 V369 V370 V371 V366 V364 V361 V362 V359 V358 V356 V355 V353 V352 V347 V350 V348 V349 V346 V344 V343 V339 V340 V341 V336 V333 V334 V331 V330 V325 V328 V326 V327 V324 V322 V321 V318 V319 V315 V313 V311 V310 V308 V307 V303 V305 V304 V302 V300 V299 V296 V297 V293 V291 V288 V289 V286 V285 V283 V282 V280 V279 V275 V277 V276 V274 V272 V271 V267 V268 V269 V264 V262 V259 V260 V257 V256 V254 V253 V251 V250 V245 V248 V246 V247 V244 V242 V241 V237 V238 V239 V234 V232 V229 V230 V227 V226 V224 V223 V221 V220 V215 V218 V216 V217 V214 V212 V211 V207 V208 V209 V204 V202 V199 V200 V197 V196 V194 V193 V191 V190 V185 V188 V186 V187 V184 V182 V181 V177 V178 V179 V174 V171 V172 V169 V168 V163 V166 V164 V165 V162 V160 V159 V156 V157 V154 V153 ( % 0.19/0.45 ( p(true) % 0.19/0.45 & -p(false) % 0.19/0.45 & ( -p(V506) % 0.19/0.45 | p(V469) ) % 0.19/0.45 & ( p(V459) % 0.19/0.45 | -p(V458) % 0.19/0.45 | -p(V457) ) % 0.19/0.45 & ( p(V331) % 0.19/0.45 | -p(V332) % 0.19/0.45 | p(V64) ) % 0.19/0.45 & ( p(V12) % 0.19/0.45 | p(V9) % 0.19/0.45 | -p(V164) ) % 0.19/0.45 & ( -p(V426) % 0.19/0.45 | p(V424) ) % 0.19/0.45 & ( p(V268) % 0.19/0.45 | -p(V133) ) % 0.19/0.45 & ( p(V331) % 0.19/0.45 | -p(V330) ) % 0.19/0.45 & ( p(V441) % 0.19/0.45 | -p(V106) ) % 0.19/0.45 & ( -p(V27) % 0.19/0.45 | p(V187) ) % 0.19/0.45 & ( -p(V147) % 0.19/0.45 | p(V457) ) % 0.19/0.45 & ( p(V462) % 0.19/0.45 | -p(V117) ) % 0.19/0.45 & ( -p(V85) % 0.19/0.45 | p(V414) % 0.19/0.45 | -p(V415) ) % 0.19/0.45 & ( p(V255) % 0.19/0.45 | -p(V522) ) % 0.19/0.45 & ( -p(V532) % 0.19/0.45 | p(V531) ) % 0.19/0.45 & ( p(V108) % 0.19/0.45 | -p(V449) ) % 0.19/0.45 & ( -p(V81) % 0.19/0.45 | p(V354) ) % 0.19/0.45 & ( p(V428) % 0.19/0.45 | -p(V427) ) % 0.19/0.45 & ( p(V457) % 0.19/0.45 | p(V104) ) % 0.19/0.45 & ( -p(V135) % 0.19/0.45 | -p(V315) % 0.19/0.45 | -p(V136) ) % 0.19/0.45 & ( p(V337) % 0.19/0.45 | -p(V336) ) % 0.19/0.45 & ( p(V62) % 0.19/0.45 | p(V300) % 0.19/0.45 | -p(V301) ) % 0.19/0.45 & ( p(V361) % 0.19/0.45 | -p(V140) ) % 0.19/0.45 & ( -p(V253) % 0.19/0.45 | -p(V28) ) % 0.19/0.45 & ( p(V297) % 0.19/0.45 | p(V135) ) % 0.19/0.45 & ( p(V456) % 0.19/0.45 | p(V110) ) % 0.19/0.45 & ( -p(V196) % 0.19/0.45 | p(V197) ) % 0.19/0.45 & ( p(V54) % 0.19/0.45 | -p(V292) % 0.19/0.45 | p(V291) ) % 0.19/0.45 & ( -p(V369) % 0.19/0.45 | p(V142) % 0.19/0.45 | -p(V75) % 0.19/0.45 | -p(V141) ) % 0.19/0.45 & ( -p(V510) % 0.19/0.45 | p(V403) ) % 0.19/0.45 & ( p(V389) % 0.19/0.45 | -p(V388) ) % 0.19/0.45 & ( p(V132) % 0.19/0.45 | p(V238) ) % 0.19/0.45 & ( -p(V386) % 0.19/0.45 | p(V385) % 0.19/0.45 | p(V88) ) % 0.19/0.45 & ( p(V290) % 0.19/0.45 | -p(V288) ) % 0.19/0.45 & ( p(V314) % 0.19/0.45 | -p(V518) ) % 0.19/0.45 & ( -p(V40) % 0.19/0.45 | p(V247) ) % 0.19/0.45 & ( -p(V128) % 0.19/0.45 | p(V177) ) % 0.19/0.45 & ( p(V136) % 0.19/0.45 | p(V313) ) % 0.19/0.45 & ( -p(V477) % 0.19/0.45 | p(V117) ) % 0.19/0.45 & ( p(V199) % 0.19/0.45 | p(V127) ) % 0.19/0.45 & ( -p(V31) % 0.19/0.45 | p(V217) ) % 0.19/0.45 & ( -p(V166) % 0.19/0.45 | p(V14) ) % 0.19/0.45 & ( p(V323) % 0.19/0.45 | -p(V322) ) % 0.19/0.45 & ( -p(V102) % 0.19/0.45 | p(V407) ) % 0.19/0.45 & ( p(V141) % 0.19/0.45 | p(V395) ) % 0.19/0.45 & ( p(V80) % 0.19/0.45 | p(V374) ) % 0.19/0.45 & ( p(V452) % 0.19/0.45 | -p(V110) % 0.19/0.45 | -p(V107) ) % 0.19/0.45 & ( -p(V526) % 0.19/0.45 | p(V527) ) % 0.19/0.45 & ( -p(V352) % 0.19/0.45 | -p(V65) ) % 0.19/0.45 & ( -p(V373) % 0.19/0.45 | -p(V75) ) % 0.19/0.45 & ( -p(V214) % 0.19/0.45 | -p(V18) ) % 0.19/0.45 & ( p(V477) % 0.19/0.45 | -p(V117) % 0.19/0.45 | -p(V112) ) % 0.19/0.45 & ( p(V490) % 0.19/0.45 | -p(V489) ) % 0.19/0.45 & ( p(V354) % 0.19/0.45 | -p(V514) ) % 0.19/0.45 & ( p(V173) % 0.19/0.45 | -p(V528) ) % 0.19/0.45 & ( -p(V248) % 0.19/0.45 | p(V247) ) % 0.19/0.45 & ( p(V199) % 0.19/0.45 | -p(V128) ) % 0.19/0.45 & ( p(V482) % 0.19/0.45 | -p(V149) ) % 0.19/0.45 & ( p(V527) % 0.19/0.45 | -p(V180) ) % 0.19/0.45 & ( -p(V381) % 0.19/0.45 | -p(V74) ) % 0.19/0.45 & ( p(V229) % 0.19/0.45 | p(V129) ) % 0.19/0.45 & ( -p(V244) % 0.19/0.45 | -p(V28) ) % 0.19/0.45 & ( -p(V248) % 0.19/0.45 | p(V44) ) % 0.19/0.45 & ( -p(V10) % 0.19/0.45 | -p(V181) ) % 0.19/0.45 & ( -p(V30) % 0.19/0.45 | -p(V250) ) % 0.19/0.45 & ( -p(V272) % 0.19/0.45 | p(V273) ) % 0.19/0.45 & ( p(V340) % 0.19/0.45 | p(V64) ) % 0.19/0.45 & ( p(V68) % 0.19/0.45 | -p(V334) ) % 0.19/0.45 & ( -p(V125) % 0.19/0.45 | p(V156) ) % 0.19/0.45 & ( p(V293) % 0.19/0.45 | p(V48) % 0.19/0.45 | -p(V294) ) % 0.19/0.45 & ( p(V332) % 0.19/0.45 | -p(V331) ) % 0.19/0.45 & ( p(V158) % 0.19/0.45 | p(V528) % 0.19/0.45 | -p(V529) ) % 0.19/0.45 & ( p(V349) % 0.19/0.45 | -p(V350) ) % 0.19/0.45 & ( p(V334) % 0.19/0.45 | -p(V335) % 0.19/0.45 | p(V333) ) % 0.19/0.45 & ( p(V144) % 0.19/0.45 | p(V398) ) % 0.19/0.45 & ( p(V169) % 0.19/0.45 | -p(V168) ) % 0.19/0.45 & ( -p(V259) % 0.19/0.45 | -p(V131) % 0.19/0.45 | p(V132) ) % 0.19/0.45 & ( p(V289) % 0.19/0.45 | -p(V290) % 0.19/0.45 | p(V288) ) % 0.19/0.45 & ( -p(V330) % 0.19/0.45 | -p(V57) ) % 0.19/0.45 & ( p(V25) % 0.19/0.45 | p(V212) ) % 0.19/0.45 & ( -p(V114) % 0.19/0.45 | p(V488) % 0.19/0.45 | -p(V489) ) % 0.19/0.45 & ( -p(V148) % 0.19/0.45 | -p(V104) % 0.19/0.45 | p(V147) % 0.19/0.45 | -p(V457) ) % 0.19/0.45 & ( p(V480) % 0.19/0.45 | -p(V479) ) % 0.19/0.45 & ( p(V466) % 0.19/0.45 | -p(V465) ) % 0.19/0.45 & ( -p(V154) % 0.19/0.45 | p(V153) ) % 0.19/0.45 & ( p(V143) % 0.19/0.45 | -p(V84) % 0.19/0.45 | -p(V144) % 0.19/0.45 | -p(V398) ) % 0.19/0.45 & ( p(V175) % 0.19/0.45 | -p(V528) ) % 0.19/0.45 & ( p(V327) % 0.19/0.45 | -p(V66) ) % 0.19/0.45 & ( -p(V526) % 0.19/0.45 | p(V205) ) % 0.19/0.45 & ( p(V397) % 0.19/0.45 | -p(V512) ) % 0.19/0.45 & ( -p(V94) % 0.19/0.45 | p(V445) % 0.19/0.45 | -p(V446) ) % 0.19/0.45 & ( p(V129) % 0.19/0.45 | p(V209) ) % 0.19/0.45 & ( p(V214) % 0.19/0.45 | -p(V215) % 0.19/0.45 | -p(V24) ) % 0.19/0.45 & ( p(V497) % 0.19/0.45 | p(V118) ) % 0.19/0.45 & ( p(V425) % 0.19/0.45 | -p(V426) ) % 0.19/0.45 & ( p(V187) % 0.19/0.45 | -p(V188) ) % 0.19/0.45 & ( p(V291) % 0.19/0.45 | -p(V133) ) % 0.19/0.45 & ( -p(V514) % 0.19/0.45 | p(V351) ) % 0.19/0.45 & ( -p(V86) % 0.19/0.45 | p(V391) % 0.19/0.45 | -p(V89) ) % 0.19/0.45 & ( p(V461) % 0.19/0.45 | p(V109) ) % 0.19/0.45 & ( p(V74) % 0.19/0.45 | p(V73) % 0.19/0.45 | p(V381) % 0.19/0.45 | p(V75) ) % 0.19/0.45 & ( p(V286) % 0.19/0.45 | p(V41) ) % 0.19/0.45 & ( -p(V308) % 0.19/0.45 | p(V307) % 0.19/0.45 | -p(V51) ) % 0.19/0.45 & ( -p(V12) % 0.19/0.45 | p(V193) % 0.19/0.45 | -p(V194) ) % 0.19/0.45 & ( p(V83) % 0.19/0.45 | p(V411) % 0.19/0.45 | p(V84) ) % 0.19/0.45 & ( p(V523) % 0.19/0.45 | -p(V240) ) % 0.19/0.45 & ( -p(V271) % 0.19/0.45 | -p(V40) ) % 0.19/0.45 & ( p(V45) % 0.19/0.45 | p(V40) % 0.19/0.45 | -p(V247) % 0.19/0.45 | p(V41) % 0.19/0.45 | p(V47) ) % 0.19/0.45 & ( p(V39) % 0.19/0.45 | p(V38) % 0.19/0.45 | p(V271) % 0.19/0.45 | p(V40) ) % 0.19/0.45 & ( p(V313) % 0.19/0.45 | -p(V135) ) % 0.19/0.45 & ( -p(V140) % 0.19/0.45 | -p(V366) % 0.19/0.45 | -p(V139) ) % 0.19/0.45 & ( -p(V143) % 0.19/0.45 | p(V417) ) % 0.19/0.45 & ( -p(V160) % 0.19/0.45 | p(V161) ) % 0.19/0.45 & ( -p(V162) % 0.19/0.45 | p(V163) ) % 0.19/0.45 & ( -p(V277) % 0.19/0.45 | p(V52) ) % 0.19/0.45 & ( p(V196) % 0.19/0.45 | -p(V11) % 0.19/0.45 | -p(V197) ) % 0.19/0.45 & ( -p(V166) % 0.19/0.45 | p(V164) ) % 0.19/0.45 & ( p(V148) % 0.19/0.45 | p(V458) ) % 0.19/0.45 & ( -p(V57) % 0.19/0.45 | -p(V324) ) % 0.19/0.45 & ( -p(V103) % 0.19/0.45 | p(V447) ) % 0.19/0.45 & ( p(V110) % 0.19/0.45 | p(V431) % 0.19/0.45 | p(V109) % 0.19/0.45 | -p(V432) ) % 0.19/0.45 & ( p(V72) % 0.19/0.45 | p(V66) % 0.19/0.45 | p(V70) % 0.19/0.45 | p(V65) % 0.19/0.45 | -p(V327) ) % 0.19/0.45 & ( p(V498) % 0.19/0.45 | -p(V499) % 0.19/0.45 | p(V123) ) % 0.19/0.45 & ( -p(V470) % 0.19/0.45 | -p(V104) ) % 0.19/0.45 & ( -p(V64) % 0.19/0.45 | -p(V352) ) % 0.19/0.45 & ( p(V133) % 0.19/0.45 | p(V293) ) % 0.19/0.45 & ( -p(V121) % 0.19/0.45 | p(V487) ) % 0.19/0.45 & ( -p(V416) % 0.19/0.45 | p(V100) % 0.19/0.45 | p(V415) ) % 0.19/0.45 & ( p(V304) % 0.19/0.45 | -p(V58) ) % 0.19/0.45 & ( -p(V29) % 0.19/0.45 | -p(V253) ) % 0.19/0.45 & ( p(V93) % 0.19/0.45 | p(V436) % 0.19/0.45 | p(V92) % 0.19/0.45 | p(V91) ) % 0.19/0.45 & ( -p(V508) % 0.19/0.45 | p(V453) ) % 0.19/0.45 & ( -p(V348) % 0.19/0.45 | p(V74) % 0.19/0.45 | p(V77) ) % 0.19/0.45 & ( -p(V477) % 0.19/0.45 | p(V112) ) % 0.19/0.45 & ( p(V278) % 0.19/0.45 | -p(V275) ) % 0.19/0.45 & ( p(V197) % 0.19/0.45 | p(V19) % 0.19/0.45 | -p(V198) ) % 0.19/0.45 & ( p(V104) % 0.19/0.45 | p(V103) % 0.19/0.45 | p(V467) ) % 0.19/0.45 & ( p(V95) % 0.19/0.45 | p(V100) % 0.19/0.45 | p(V101) % 0.19/0.45 | p(V99) % 0.19/0.45 | p(V93) % 0.19/0.45 | -p(V406) ) % 0.19/0.45 & ( -p(V65) % 0.19/0.45 | -p(V355) ) % 0.19/0.45 & ( p(V463) % 0.19/0.45 | -p(V108) % 0.19/0.45 | -p(V464) ) % 0.19/0.45 & ( -p(V452) % 0.19/0.45 | p(V107) ) % 0.19/0.45 & ( -p(V343) % 0.19/0.45 | -p(V65) ) % 0.19/0.45 & ( -p(V520) % 0.19/0.45 | p(V521) ) % 0.19/0.45 & ( p(V325) % 0.19/0.45 | p(V59) ) % 0.19/0.45 & ( p(V351) % 0.19/0.45 | -p(V347) ) % 0.19/0.45 & ( p(V120) % 0.19/0.45 | p(V496) ) % 0.19/0.45 & ( -p(V271) % 0.19/0.45 | -p(V38) ) % 0.19/0.45 & ( p(V396) % 0.19/0.45 | -p(V395) ) % 0.19/0.45 & ( -p(V466) % 0.19/0.45 | -p(V462) % 0.19/0.45 | p(V506) % 0.19/0.45 | -p(V478) % 0.19/0.45 | -p(V475) % 0.19/0.45 | -p(V469) % 0.19/0.45 | -p(V505) % 0.19/0.45 | -p(V480) % 0.19/0.45 | -p(V472) % 0.19/0.45 | -p(V481) ) % 0.19/0.45 & ( -p(V342) % 0.19/0.45 | p(V339) ) % 0.19/0.45 & ( -p(V427) % 0.19/0.45 | -p(V93) ) % 0.19/0.45 & ( -p(V504) % 0.19/0.45 | p(V505) ) % 0.19/0.45 & ( p(V143) % 0.19/0.45 | p(V420) ) % 0.19/0.45 & ( p(V215) % 0.19/0.45 | -p(V214) ) % 0.19/0.45 & ( p(V286) % 0.19/0.45 | -p(V287) % 0.19/0.45 | p(V49) ) % 0.19/0.45 & ( p(V202) % 0.19/0.45 | -p(V127) ) % 0.19/0.45 & ( p(V25) % 0.19/0.45 | p(V27) % 0.19/0.45 | p(V20) % 0.19/0.45 | p(V21) % 0.19/0.45 | -p(V187) ) % 0.19/0.45 & ( -p(V144) % 0.19/0.45 | p(V143) % 0.19/0.45 | -p(V417) ) % 0.19/0.45 & ( -p(V361) % 0.19/0.45 | p(V363) ) % 0.19/0.45 & ( -p(V64) % 0.19/0.45 | p(V332) ) % 0.19/0.45 & ( p(V170) % 0.19/0.45 | -p(V169) ) % 0.19/0.45 & ( -p(V168) % 0.19/0.45 | -p(V2) ) % 0.19/0.45 & ( p(V183) % 0.19/0.45 | -p(V182) ) % 0.19/0.45 & ( p(V48) % 0.19/0.45 | p(V49) % 0.19/0.45 | p(V310) ) % 0.19/0.45 & ( p(V239) % 0.19/0.45 | p(V132) ) % 0.19/0.45 & ( p(V499) % 0.19/0.45 | -p(V502) ) % 0.19/0.45 & ( p(V341) % 0.19/0.45 | p(V139) ) % 0.19/0.45 & ( p(V216) % 0.19/0.45 | -p(V29) ) % 0.19/0.45 & ( -p(V350) % 0.19/0.45 | p(V351) ) % 0.19/0.45 & ( -p(V254) % 0.19/0.45 | p(V253) % 0.19/0.45 | -p(V32) ) % 0.19/0.45 & ( -p(V510) % 0.19/0.45 | p(V410) ) % 0.19/0.45 & ( p(V153) % 0.19/0.45 | -p(V4) ) % 0.19/0.45 & ( -p(V158) % 0.19/0.45 | p(V156) ) % 0.19/0.45 & ( -p(V384) % 0.19/0.45 | -p(V75) ) % 0.19/0.45 & ( p(V386) % 0.19/0.45 | -p(V512) ) % 0.19/0.45 & ( -p(V524) % 0.19/0.45 | p(V523) ) % 0.19/0.45 & ( p(V429) % 0.19/0.45 | -p(V428) ) % 0.19/0.45 & ( -p(V115) % 0.19/0.45 | p(V485) % 0.19/0.45 | -p(V486) ) % 0.19/0.45 & ( -p(V54) % 0.19/0.45 | p(V292) ) % 0.19/0.45 & ( -p(V430) % 0.19/0.45 | -p(V93) ) % 0.19/0.45 & ( p(V34) % 0.19/0.45 | p(V245) ) % 0.19/0.45 & ( p(V408) % 0.19/0.45 | -p(V96) ) % 0.19/0.45 & ( p(V479) % 0.19/0.45 | p(V116) % 0.19/0.45 | -p(V480) ) % 0.19/0.45 & ( p(V30) % 0.19/0.45 | p(V237) ) % 0.19/0.45 & ( p(V360) % 0.19/0.45 | -p(V514) ) % 0.19/0.45 & ( p(V128) % 0.19/0.45 | p(V204) ) % 0.19/0.45 & ( p(V121) % 0.19/0.45 | p(V496) ) % 0.19/0.45 & ( p(V179) % 0.19/0.45 | p(V127) ) % 0.19/0.45 & ( p(V393) % 0.19/0.45 | -p(V141) ) % 0.19/0.45 & ( -p(V217) % 0.19/0.45 | p(V31) % 0.19/0.45 | p(V37) % 0.19/0.45 | p(V30) % 0.19/0.45 | p(V35) ) % 0.19/0.45 & ( p(V34) % 0.19/0.45 | -p(V218) ) % 0.19/0.45 & ( p(V323) % 0.19/0.45 | -p(V516) ) % 0.19/0.45 & ( p(V267) % 0.19/0.45 | p(V40) ) % 0.19/0.45 & ( p(V393) % 0.19/0.45 | p(V142) ) % 0.19/0.45 & ( p(V261) % 0.19/0.45 | -p(V259) ) % 0.19/0.45 & ( -p(V379) % 0.19/0.45 | p(V378) ) % 0.19/0.45 & ( -p(V26) % 0.19/0.45 | p(V203) ) % 0.19/0.45 & ( -p(V9) % 0.19/0.45 | p(V164) ) % 0.19/0.45 & ( -p(V58) % 0.19/0.45 | -p(V331) % 0.19/0.45 | p(V330) ) % 0.19/0.45 & ( p(V329) % 0.19/0.45 | -p(V516) ) % 0.19/0.45 & ( -p(V349) % 0.19/0.45 | p(V350) % 0.19/0.45 | -p(V79) % 0.19/0.45 | -p(V348) ) % 0.19/0.45 & ( p(V89) % 0.19/0.45 | p(V88) % 0.19/0.45 | -p(V383) % 0.19/0.45 | p(V382) ) % 0.19/0.45 & ( p(V152) % 0.19/0.45 | p(V1) ) % 0.19/0.45 & ( p(V163) % 0.19/0.45 | p(V5) ) % 0.19/0.45 & ( p(V399) % 0.19/0.45 | p(V143) ) % 0.19/0.45 & ( -p(V28) % 0.19/0.45 | -p(V256) ) % 0.19/0.45 & ( p(V358) % 0.19/0.45 | p(V63) % 0.19/0.45 | p(V64) % 0.19/0.45 | p(V65) ) % 0.19/0.45 & ( -p(V140) % 0.19/0.45 | p(V339) ) % 0.19/0.45 & ( p(V267) % 0.19/0.45 | -p(V134) ) % 0.19/0.45 & ( p(V81) % 0.19/0.45 | -p(V362) ) % 0.19/0.45 & ( -p(V151) % 0.19/0.45 | -p(V118) % 0.19/0.45 | -p(V497) ) % 0.19/0.45 & ( -p(V42) % 0.19/0.45 | p(V282) % 0.19/0.45 | -p(V283) ) % 0.19/0.45 & ( p(V462) % 0.19/0.45 | -p(V506) ) % 0.19/0.45 & ( -p(V270) % 0.19/0.45 | p(V269) ) % 0.19/0.45 & ( p(V217) % 0.19/0.45 | -p(V30) ) % 0.19/0.45 & ( p(V429) % 0.19/0.45 | -p(V111) ) % 0.19/0.45 & ( p(V284) % 0.19/0.45 | -p(V520) ) % 0.19/0.45 & ( p(V252) % 0.19/0.45 | -p(V45) ) % 0.19/0.45 & ( p(V176) % 0.19/0.45 | -p(V528) ) % 0.19/0.45 & ( -p(V427) % 0.19/0.45 | -p(V92) ) % 0.19/0.45 & ( p(V472) % 0.19/0.45 | -p(V117) ) % 0.19/0.45 & ( p(V246) % 0.19/0.45 | -p(V39) ) % 0.19/0.45 & ( p(V375) % 0.19/0.45 | -p(V374) ) % 0.19/0.45 & ( p(V405) % 0.19/0.45 | -p(V410) % 0.19/0.45 | p(V409) ) % 0.19/0.45 & ( p(V168) % 0.19/0.45 | p(V2) % 0.19/0.45 | p(V3) ) % 0.19/0.45 & ( -p(V22) % 0.19/0.45 | p(V186) ) % 0.19/0.45 & ( p(V201) % 0.19/0.45 | -p(V199) ) % 0.19/0.45 & ( p(V176) % 0.19/0.45 | p(V17) ) % 0.19/0.45 & ( p(V53) % 0.19/0.45 | p(V300) ) % 0.19/0.45 & ( -p(V15) % 0.19/0.45 | p(V165) ) % 0.19/0.45 & ( -p(V48) % 0.19/0.45 | -p(V302) ) % 0.19/0.45 & ( -p(V274) % 0.19/0.45 | -p(V40) ) % 0.19/0.45 & ( -p(V20) % 0.19/0.45 | -p(V220) ) % 0.19/0.45 & ( -p(V127) % 0.19/0.45 | -p(V204) % 0.19/0.45 | -p(V128) ) % 0.19/0.45 & ( p(V400) % 0.19/0.45 | -p(V511) % 0.19/0.45 | p(V510) ) % 0.19/0.45 & ( p(V141) % 0.19/0.45 | p(V371) ) % 0.19/0.45 & ( p(V335) % 0.19/0.45 | -p(V516) ) % 0.19/0.45 & ( p(V517) % 0.19/0.45 | -p(V516) ) % 0.19/0.45 & ( -p(V520) % 0.19/0.45 | p(V281) ) % 0.19/0.45 & ( -p(V210) % 0.19/0.45 | p(V525) ) % 0.19/0.45 & ( p(V65) % 0.19/0.45 | p(V64) % 0.19/0.45 | p(V343) % 0.19/0.45 | p(V63) ) % 0.19/0.45 & ( p(V264) % 0.19/0.45 | p(V132) ) % 0.19/0.45 & ( -p(V498) % 0.19/0.45 | p(V499) ) % 0.19/0.45 & ( p(V509) % 0.19/0.45 | -p(V508) ) % 0.19/0.45 & ( p(V267) % 0.19/0.45 | p(V133) ) % 0.19/0.45 & ( -p(V281) % 0.19/0.45 | p(V53) % 0.19/0.45 | p(V54) % 0.19/0.45 | p(V280) ) % 0.19/0.45 & ( p(V17) % 0.19/0.45 | -p(V161) % 0.19/0.45 | p(V160) ) % 0.19/0.45 & ( p(V131) % 0.19/0.45 | p(V237) ) % 0.19/0.45 & ( p(V97) % 0.19/0.45 | p(V437) ) % 0.19/0.45 & ( p(V185) % 0.19/0.45 | p(V14) ) % 0.19/0.45 & ( p(V471) % 0.19/0.45 | -p(V472) % 0.19/0.45 | p(V117) % 0.19/0.45 | p(V113) ) % 0.19/0.45 & ( -p(V74) % 0.19/0.45 | -p(V387) ) % 0.19/0.45 & ( p(V379) % 0.19/0.45 | -p(V87) % 0.19/0.45 | -p(V378) ) % 0.19/0.45 & ( -p(V344) % 0.19/0.45 | p(V345) ) % 0.19/0.45 & ( p(V74) % 0.19/0.45 | p(V370) ) % 0.19/0.45 & ( p(V459) % 0.19/0.45 | p(V506) % 0.19/0.45 | -p(V507) ) % 0.19/0.45 & ( p(V472) % 0.19/0.45 | -p(V506) ) % 0.19/0.45 & ( -p(V157) % 0.19/0.45 | -p(V2) % 0.19/0.45 | -p(V126) % 0.19/0.45 | -p(V125) ) % 0.19/0.45 & ( p(V276) % 0.19/0.45 | -p(V277) ) % 0.19/0.45 & ( p(V167) % 0.19/0.45 | -p(V166) ) % 0.19/0.45 & ( -p(V150) % 0.19/0.45 | -p(V482) % 0.19/0.45 | p(V149) % 0.19/0.45 | -p(V113) ) % 0.19/0.45 & ( -p(V309) % 0.19/0.45 | p(V308) % 0.19/0.45 | p(V61) % 0.19/0.45 | p(V60) ) % 0.19/0.45 & ( p(V171) % 0.19/0.45 | p(V126) ) % 0.19/0.45 & ( p(V449) % 0.19/0.45 | -p(V450) % 0.19/0.45 | p(V448) ) % 0.19/0.45 & ( -p(V234) % 0.19/0.45 | p(V235) ) % 0.19/0.45 & ( p(V498) % 0.19/0.45 | p(V118) ) % 0.19/0.45 & ( p(V57) % 0.19/0.45 | p(V56) % 0.19/0.45 | p(V321) ) % 0.19/0.45 & ( p(V27) % 0.19/0.45 | -p(V183) % 0.19/0.45 | p(V182) ) % 0.19/0.45 & ( p(V474) % 0.19/0.45 | -p(V473) ) % 0.19/0.45 & ( p(V511) % 0.19/0.45 | -p(V510) ) % 0.19/0.45 & ( p(V471) % 0.19/0.45 | -p(V470) ) % 0.19/0.45 & ( p(V150) % 0.19/0.45 | p(V494) ) % 0.19/0.45 & ( p(V174) % 0.19/0.45 | p(V8) % 0.19/0.45 | -p(V175) ) % 0.19/0.45 & ( -p(V47) % 0.19/0.45 | p(V243) ) % 0.19/0.45 & ( p(V421) % 0.19/0.45 | -p(V101) ) % 0.19/0.45 & ( -p(V116) % 0.19/0.45 | p(V469) ) % 0.19/0.45 & ( -p(V504) % 0.19/0.45 | p(V495) ) % 0.19/0.45 & ( p(V145) % 0.19/0.45 | p(V423) ) % 0.19/0.45 & ( p(V226) % 0.19/0.45 | -p(V227) % 0.19/0.45 | -p(V21) ) % 0.19/0.45 & ( p(V130) % 0.19/0.45 | p(V209) ) % 0.19/0.45 & ( -p(V211) % 0.19/0.45 | -p(V20) ) % 0.19/0.45 & ( p(V426) % 0.19/0.45 | -p(V423) % 0.19/0.45 | -p(V425) % 0.19/0.45 | -p(V424) ) % 0.19/0.45 & ( p(V166) % 0.19/0.45 | -p(V167) % 0.19/0.45 | p(V163) ) % 0.19/0.45 & ( p(V496) % 0.19/0.45 | -p(V504) ) % 0.19/0.45 & ( p(V390) % 0.19/0.45 | -p(V142) ) % 0.19/0.45 & ( p(V130) % 0.19/0.45 | -p(V229) % 0.19/0.45 | -p(V129) ) % 0.19/0.45 & ( -p(V451) % 0.19/0.45 | p(V453) ) % 0.19/0.45 & ( -p(V356) % 0.19/0.45 | p(V357) ) % 0.19/0.45 & ( p(V116) % 0.19/0.45 | p(V481) ) % 0.19/0.45 & ( -p(V166) % 0.19/0.45 | p(V165) ) % 0.19/0.45 & ( -p(V445) % 0.19/0.45 | -p(V92) ) % 0.19/0.45 & ( p(V160) % 0.19/0.45 | p(V6) ) % 0.19/0.45 & ( -p(V177) % 0.19/0.45 | -p(V179) % 0.19/0.45 | p(V180) % 0.19/0.45 | -p(V178) ) % 0.19/0.45 & ( p(V385) % 0.19/0.45 | -p(V384) ) % 0.19/0.45 & ( p(V237) % 0.19/0.45 | -p(V132) ) % 0.19/0.45 & ( -p(V436) % 0.19/0.45 | p(V437) ) % 0.19/0.45 & ( -p(V367) % 0.19/0.45 | -p(V368) % 0.19/0.45 | p(V514) % 0.19/0.45 | -p(V365) % 0.19/0.45 | -p(V363) % 0.19/0.45 | -p(V354) % 0.19/0.45 | -p(V345) % 0.19/0.45 | -p(V513) % 0.19/0.45 | -p(V357) % 0.19/0.45 | -p(V360) % 0.19/0.45 | -p(V351) ) % 0.19/0.45 & ( p(V92) % 0.19/0.45 | p(V424) ) % 0.19/0.45 & ( p(V380) % 0.19/0.45 | -p(V512) ) % 0.19/0.45 & ( p(V402) % 0.19/0.45 | -p(V401) ) % 0.19/0.45 & ( -p(V19) % 0.19/0.45 | p(V198) ) % 0.19/0.45 & ( p(V474) % 0.19/0.45 | p(V105) ) % 0.19/0.45 & ( p(V280) % 0.19/0.45 | p(V43) ) % 0.19/0.45 & ( -p(V49) % 0.19/0.45 | -p(V299) ) % 0.19/0.45 & ( p(V90) % 0.19/0.45 | -p(V375) % 0.19/0.45 | p(V374) ) % 0.19/0.45 & ( -p(V62) % 0.19/0.45 | -p(V317) % 0.19/0.45 | -p(V61) ) % 0.19/0.45 & ( -p(V114) % 0.19/0.45 | p(V466) ) % 0.19/0.45 & ( -p(V9) % 0.19/0.45 | -p(V184) ) % 0.19/0.45 & ( p(V8) % 0.19/0.45 | p(V9) % 0.19/0.45 | p(V10) % 0.19/0.45 | p(V190) ) % 0.19/0.45 & ( -p(V260) % 0.19/0.45 | p(V43) ) % 0.19/0.45 & ( p(V486) % 0.19/0.45 | p(V121) % 0.19/0.45 | -p(V487) ) % 0.19/0.45 & ( p(V503) % 0.19/0.45 | -p(V504) ) % 0.19/0.45 & ( -p(V54) % 0.19/0.45 | p(V281) ) % 0.19/0.45 & ( -p(V518) % 0.19/0.45 | p(V316) ) % 0.19/0.45 & ( p(V57) % 0.19/0.45 | p(V318) ) % 0.19/0.45 & ( p(V513) % 0.19/0.45 | -p(V512) ) % 0.19/0.45 & ( -p(V38) % 0.19/0.45 | -p(V285) ) % 0.19/0.45 & ( -p(V149) % 0.19/0.45 | -p(V494) % 0.19/0.45 | -p(V150) ) % 0.19/0.45 & ( -p(V223) % 0.19/0.45 | p(V224) ) % 0.19/0.45 & ( -p(V43) % 0.19/0.45 | -p(V280) % 0.19/0.45 | p(V279) ) % 0.19/0.45 & ( -p(V147) % 0.19/0.45 | p(V476) ) % 0.19/0.45 & ( -p(V223) % 0.19/0.45 | -p(V18) ) % 0.19/0.45 & ( p(V182) % 0.19/0.45 | -p(V181) ) % 0.19/0.45 & ( p(V46) % 0.19/0.45 | p(V266) ) % 0.19/0.45 & ( -p(V492) % 0.19/0.45 | p(V493) ) % 0.19/0.45 & ( p(V4) % 0.19/0.45 | p(V3) % 0.19/0.45 | p(V7) % 0.19/0.45 | -p(V153) % 0.19/0.45 | p(V6) ) % 0.19/0.45 & ( -p(V405) % 0.19/0.45 | p(V410) ) % 0.19/0.45 & ( -p(V488) % 0.19/0.45 | -p(V113) ) % 0.19/0.45 & ( -p(V414) % 0.19/0.45 | -p(V84) ) % 0.19/0.45 & ( -p(V36) % 0.19/0.45 | p(V222) ) % 0.19/0.45 & ( -p(V34) % 0.19/0.45 | -p(V245) % 0.19/0.45 | p(V244) ) % 0.19/0.45 & ( p(V139) % 0.19/0.45 | p(V339) ) % 0.19/0.45 & ( p(V235) % 0.19/0.45 | -p(V524) ) % 0.19/0.45 & ( p(V483) % 0.19/0.45 | p(V149) ) % 0.19/0.45 & ( p(V304) % 0.19/0.45 | -p(V305) ) % 0.19/0.45 & ( -p(V26) % 0.19/0.45 | -p(V23) % 0.19/0.45 | p(V200) ) % 0.19/0.45 & ( -p(V255) % 0.19/0.45 | p(V254) % 0.19/0.45 | p(V45) ) % 0.19/0.45 & ( -p(V82) % 0.19/0.45 | p(V349) ) % 0.19/0.45 & ( -p(V246) % 0.19/0.45 | -p(V247) % 0.19/0.45 | -p(V44) % 0.19/0.45 | p(V248) ) % 0.19/0.45 & ( -p(V122) % 0.19/0.45 | -p(V501) % 0.19/0.45 | -p(V123) ) % 0.19/0.45 & ( p(V316) % 0.19/0.45 | -p(V56) ) % 0.19/0.45 & ( p(V207) % 0.19/0.45 | p(V20) ) % 0.19/0.45 & ( -p(V82) % 0.19/0.45 | p(V345) ) % 0.19/0.45 & ( p(V243) % 0.19/0.45 | -p(V242) ) % 0.19/0.45 & ( p(V300) % 0.19/0.45 | -p(V299) ) % 0.19/0.45 & ( p(V92) % 0.19/0.45 | p(V91) % 0.19/0.45 | p(V439) % 0.19/0.45 | p(V93) ) % 0.19/0.45 & ( -p(V448) % 0.19/0.45 | p(V450) ) % 0.19/0.45 & ( -p(V149) % 0.19/0.45 | -p(V112) % 0.19/0.45 | -p(V483) % 0.19/0.45 | -p(V150) ) % 0.19/0.45 & ( p(V370) % 0.19/0.45 | -p(V372) ) % 0.19/0.45 & ( p(V405) % 0.19/0.45 | -p(V404) ) % 0.19/0.45 & ( p(V171) % 0.19/0.45 | -p(V125) ) % 0.19/0.45 & ( p(V411) % 0.19/0.45 | -p(V86) % 0.19/0.45 | -p(V412) ) % 0.19/0.45 & ( p(V149) % 0.19/0.45 | p(V494) ) % 0.19/0.45 & ( p(V259) % 0.19/0.45 | p(V131) ) % 0.19/0.45 & ( -p(V35) % 0.19/0.45 | p(V225) ) % 0.19/0.45 & ( p(V217) % 0.19/0.45 | -p(V35) ) % 0.19/0.45 & ( -p(V91) % 0.19/0.45 | -p(V430) ) % 0.19/0.45 & ( -p(V120) % 0.19/0.45 | p(V495) ) % 0.19/0.45 & ( -p(V528) % 0.19/0.45 | p(V161) ) % 0.19/0.45 & ( p(V333) % 0.19/0.45 | -p(V137) ) % 0.19/0.45 & ( p(V74) % 0.19/0.45 | p(V376) % 0.19/0.45 | p(V73) % 0.19/0.45 | p(V75) ) % 0.19/0.45 & ( p(V2) % 0.19/0.45 | -p(V154) ) % 0.19/0.45 & ( p(V75) % 0.19/0.45 | p(V369) ) % 0.19/0.45 & ( p(V150) % 0.19/0.45 | p(V482) ) % 0.19/0.45 & ( -p(V104) % 0.19/0.45 | -p(V460) ) % 0.19/0.45 & ( p(V338) % 0.19/0.45 | -p(V516) ) % 0.19/0.45 & ( p(V58) % 0.19/0.45 | p(V62) % 0.19/0.45 | p(V60) % 0.19/0.45 | -p(V304) % 0.19/0.45 | p(V57) ) % 0.19/0.45 & ( -p(V200) % 0.19/0.45 | p(V201) ) % 0.19/0.45 & ( p(V107) % 0.19/0.45 | p(V468) ) % 0.19/0.45 & ( p(V18) % 0.19/0.45 | p(V20) % 0.19/0.45 | p(V223) % 0.19/0.45 | p(V19) ) % 0.19/0.45 & ( p(V359) % 0.19/0.45 | -p(V360) % 0.19/0.45 | p(V74) ) % 0.19/0.45 & ( p(V233) % 0.19/0.45 | -p(V232) ) % 0.19/0.45 & ( p(V328) % 0.19/0.45 | p(V325) % 0.19/0.45 | -p(V329) ) % 0.19/0.45 & ( -p(V197) % 0.19/0.45 | p(V198) ) % 0.19/0.45 & ( -p(V341) % 0.19/0.45 | -p(V140) % 0.19/0.45 | -p(V139) % 0.19/0.45 | -p(V63) ) % 0.19/0.45 & ( -p(V240) % 0.19/0.45 | p(V239) ) % 0.19/0.45 & ( p(V461) % 0.19/0.45 | p(V117) % 0.19/0.45 | -p(V462) ) % 0.19/0.45 & ( -p(V372) % 0.19/0.45 | p(V369) ) % 0.19/0.45 & ( p(V40) % 0.19/0.45 | p(V39) % 0.19/0.45 | p(V38) % 0.19/0.45 | p(V279) ) % 0.19/0.45 & ( p(V326) % 0.19/0.45 | -p(V328) ) % 0.19/0.45 & ( -p(V141) % 0.19/0.45 | -p(V142) % 0.19/0.45 | -p(V371) % 0.19/0.45 | -p(V73) ) % 0.19/0.45 & ( p(V348) % 0.19/0.45 | -p(V350) ) % 0.19/0.45 & ( -p(V490) % 0.19/0.45 | p(V119) % 0.19/0.45 | p(V489) % 0.19/0.45 | p(V120) ) % 0.19/0.45 & ( -p(V409) % 0.19/0.45 | p(V406) ) % 0.19/0.45 & ( -p(V439) % 0.19/0.45 | -p(V92) ) % 0.19/0.45 & ( -p(V512) % 0.19/0.45 | p(V394) ) % 0.19/0.45 & ( p(V19) % 0.19/0.45 | p(V20) % 0.19/0.45 | p(V226) % 0.19/0.45 | p(V18) ) % 0.19/0.45 & ( p(V277) % 0.19/0.45 | p(V275) % 0.19/0.45 | -p(V278) ) % 0.19/0.45 & ( p(V191) % 0.19/0.45 | p(V13) ) % 0.19/0.45 & ( -p(V493) % 0.19/0.45 | p(V504) % 0.19/0.45 | -p(V503) % 0.19/0.45 | -p(V487) % 0.19/0.45 | -p(V496) % 0.19/0.45 | -p(V495) % 0.19/0.45 | -p(V490) ) % 0.19/0.45 & ( -p(V524) % 0.19/0.45 | p(V236) ) % 0.19/0.45 & ( -p(V301) % 0.19/0.45 | -p(V314) % 0.19/0.45 | -p(V312) % 0.19/0.45 | -p(V316) % 0.19/0.45 | -p(V517) % 0.19/0.45 | -p(V309) % 0.19/0.45 | -p(V306) % 0.19/0.45 | p(V518) % 0.19/0.45 | -p(V317) ) % 0.19/0.45 & ( -p(V2) % 0.19/0.45 | p(V154) % 0.19/0.45 | -p(V153) % 0.19/0.45 | -p(V5) ) % 0.19/0.45 & ( -p(V134) % 0.19/0.45 | -p(V38) % 0.19/0.45 | -p(V133) % 0.19/0.45 | -p(V269) ) % 0.19/0.45 & ( -p(V302) % 0.19/0.45 | p(V303) ) % 0.19/0.45 & ( -p(V377) % 0.19/0.45 | p(V376) % 0.19/0.45 | -p(V79) ) % 0.19/0.45 & ( -p(V376) % 0.19/0.45 | p(V377) ) % 0.19/0.45 & ( -p(V212) % 0.19/0.45 | p(V213) ) % 0.19/0.45 & ( -p(V78) % 0.19/0.45 | -p(V382) % 0.19/0.45 | p(V381) ) % 0.19/0.45 & ( -p(V357) % 0.19/0.45 | p(V80) % 0.19/0.45 | p(V356) ) % 0.19/0.45 & ( -p(V241) % 0.19/0.45 | -p(V28) ) % 0.19/0.45 & ( -p(V5) % 0.19/0.45 | p(V162) % 0.19/0.45 | -p(V163) ) % 0.19/0.45 & ( p(V412) % 0.19/0.45 | -p(V411) ) % 0.19/0.45 & ( -p(V159) % 0.19/0.45 | -p(V2) ) % 0.19/0.45 & ( -p(V75) % 0.19/0.45 | -p(V376) ) % 0.19/0.45 & ( -p(V287) % 0.19/0.45 | p(V520) % 0.19/0.45 | -p(V519) % 0.19/0.45 | -p(V278) % 0.19/0.45 | -p(V294) % 0.19/0.45 | -p(V295) % 0.19/0.45 | -p(V273) % 0.19/0.45 | -p(V290) % 0.19/0.45 | -p(V281) % 0.19/0.45 | -p(V292) % 0.19/0.45 | -p(V284) ) % 0.19/0.45 & ( -p(V418) % 0.19/0.45 | p(V419) ) % 0.19/0.45 & ( p(V404) % 0.19/0.45 | -p(V405) % 0.19/0.45 | -p(V87) ) % 0.19/0.45 & ( -p(V373) % 0.19/0.45 | p(V374) ) % 0.19/0.45 & ( p(V209) % 0.19/0.45 | p(V18) ) % 0.19/0.45 & ( -p(V145) % 0.19/0.45 | p(V451) ) % 0.19/0.45 & ( -p(V316) % 0.19/0.45 | p(V56) % 0.19/0.45 | p(V315) ) % 0.19/0.45 & ( p(V476) % 0.19/0.45 | p(V148) ) % 0.19/0.45 & ( -p(V518) % 0.19/0.45 | p(V517) ) % 0.19/0.45 & ( -p(V450) % 0.19/0.45 | -p(V447) % 0.19/0.45 | p(V508) % 0.19/0.45 | -p(V432) % 0.19/0.45 | -p(V429) % 0.19/0.45 | -p(V507) % 0.19/0.45 | -p(V455) % 0.19/0.45 | -p(V438) % 0.19/0.45 | -p(V444) % 0.19/0.45 | -p(V456) % 0.19/0.45 | -p(V453) % 0.19/0.45 | -p(V435) % 0.19/0.45 | -p(V441) ) % 0.19/0.45 & ( -p(V338) % 0.19/0.45 | -p(V71) % 0.19/0.45 | -p(V72) ) % 0.19/0.45 & ( p(V36) % 0.19/0.45 | p(V236) ) % 0.19/0.45 & ( p(V238) % 0.19/0.45 | -p(V240) ) % 0.19/0.45 & ( p(V255) % 0.19/0.45 | -p(V254) ) % 0.19/0.45 & ( -p(V279) % 0.19/0.45 | p(V280) ) % 0.19/0.45 & ( -p(V291) % 0.19/0.45 | -p(V134) % 0.19/0.45 | p(V133) ) % 0.19/0.45 & ( p(V167) % 0.19/0.45 | -p(V163) ) % 0.19/0.45 & ( p(V325) % 0.19/0.45 | -p(V324) ) % 0.19/0.45 & ( p(V472) % 0.19/0.45 | -p(V471) ) % 0.19/0.45 & ( p(V440) % 0.19/0.45 | p(V96) ) % 0.19/0.45 & ( -p(V520) % 0.19/0.45 | p(V294) ) % 0.19/0.45 & ( -p(V92) % 0.19/0.45 | -p(V433) ) % 0.19/0.45 & ( p(V212) % 0.19/0.45 | -p(V211) ) % 0.19/0.45 & ( -p(V174) % 0.19/0.45 | p(V175) ) % 0.19/0.45 & ( -p(V109) % 0.19/0.45 | p(V455) ) % 0.19/0.45 & ( p(V114) % 0.19/0.45 | p(V489) ) % 0.19/0.45 & ( p(V187) % 0.19/0.45 | -p(V20) ) % 0.19/0.45 & ( -p(V41) % 0.19/0.45 | p(V285) % 0.19/0.45 | -p(V286) ) % 0.19/0.45 & ( p(V224) % 0.19/0.45 | p(V35) % 0.19/0.45 | -p(V225) ) % 0.19/0.45 & ( p(V119) % 0.19/0.45 | p(V498) ) % 0.19/0.45 & ( p(V292) % 0.19/0.45 | -p(V291) ) % 0.19/0.45 & ( p(V490) % 0.19/0.45 | -p(V120) ) % 0.19/0.45 & ( p(V80) % 0.19/0.45 | p(V353) % 0.19/0.45 | p(V81) % 0.19/0.45 | -p(V354) ) % 0.19/0.45 & ( p(V9) % 0.19/0.45 | p(V10) % 0.19/0.45 | p(V196) % 0.19/0.45 | p(V8) ) % 0.19/0.45 & ( -p(V520) % 0.19/0.45 | p(V295) ) % 0.19/0.45 & ( -p(V518) % 0.19/0.45 | p(V309) ) % 0.19/0.45 & ( p(V63) % 0.19/0.45 | p(V341) ) % 0.19/0.45 & ( -p(V2) % 0.19/0.45 | -p(V162) ) % 0.19/0.45 & ( -p(V271) % 0.19/0.45 | p(V272) ) % 0.19/0.45 & ( p(V39) % 0.19/0.45 | p(V274) % 0.19/0.45 | p(V40) % 0.19/0.45 | p(V38) ) % 0.19/0.45 & ( p(V258) % 0.19/0.45 | -p(V257) ) % 0.19/0.45 & ( p(V64) % 0.19/0.45 | p(V63) % 0.19/0.45 | p(V65) % 0.19/0.45 | p(V355) ) % 0.19/0.45 & ( p(V364) % 0.19/0.45 | p(V140) ) % 0.19/0.45 & ( -p(V36) % 0.19/0.45 | p(V233) ) % 0.19/0.45 & ( -p(V307) % 0.19/0.45 | p(V308) ) % 0.19/0.45 & ( -p(V143) % 0.19/0.45 | -p(V144) % 0.19/0.45 | -p(V83) % 0.19/0.45 | -p(V399) ) % 0.19/0.45 & ( -p(V49) % 0.19/0.45 | p(V276) ) % 0.19/0.45 & ( -p(V307) % 0.19/0.45 | -p(V48) ) % 0.19/0.45 & ( -p(V469) % 0.19/0.45 | p(V115) % 0.19/0.45 | p(V116) % 0.19/0.45 | p(V468) ) % 0.19/0.45 & ( -p(V66) % 0.19/0.45 | p(V358) % 0.19/0.45 | -p(V359) ) % 0.19/0.45 & ( -p(V29) % 0.19/0.45 | -p(V241) ) % 0.19/0.45 & ( -p(V381) % 0.19/0.45 | -p(V75) ) % 0.19/0.45 & ( -p(V403) % 0.19/0.45 | p(V102) % 0.19/0.45 | p(V402) ) % 0.19/0.45 & ( -p(V91) % 0.19/0.45 | -p(V439) ) % 0.19/0.45 & ( p(V336) % 0.19/0.45 | p(V138) ) % 0.19/0.45 & ( -p(V279) % 0.19/0.45 | -p(V38) ) % 0.19/0.45 & ( -p(V104) % 0.19/0.45 | -p(V473) ) % 0.19/0.45 & ( p(V134) % 0.19/0.45 | -p(V40) % 0.19/0.45 | -p(V133) % 0.19/0.45 | -p(V267) ) % 0.19/0.45 & ( p(V337) % 0.19/0.45 | -p(V516) ) % 0.19/0.45 & ( p(V138) % 0.19/0.45 | p(V319) ) % 0.19/0.45 & ( p(V431) % 0.19/0.45 | p(V99) ) % 0.19/0.45 & ( p(V356) % 0.19/0.45 | p(V67) ) % 0.19/0.45 & ( p(V505) % 0.19/0.45 | -p(V506) ) % 0.19/0.45 & ( -p(V188) % 0.19/0.45 | p(V189) ) % 0.19/0.45 & ( -p(V436) % 0.19/0.45 | -p(V91) ) % 0.19/0.45 & ( p(V435) % 0.19/0.45 | -p(V434) ) % 0.19/0.45 & ( -p(V355) % 0.19/0.45 | -p(V63) ) % 0.19/0.45 & ( p(V269) % 0.19/0.45 | p(V133) ) % 0.19/0.45 & ( p(V228) % 0.19/0.45 | -p(V227) ) % 0.19/0.45 & ( -p(V217) % 0.19/0.45 | p(V218) % 0.19/0.45 | -p(V216) % 0.19/0.45 | -p(V34) ) % 0.19/0.45 & ( -p(V508) % 0.19/0.45 | p(V450) ) % 0.19/0.45 & ( -p(V468) % 0.19/0.45 | p(V469) ) % 0.19/0.45 & ( -p(V524) % 0.19/0.45 | p(V219) ) % 0.19/0.45 & ( p(V320) % 0.19/0.45 | p(V516) % 0.19/0.45 | -p(V517) ) % 0.19/0.45 & ( p(V82) % 0.19/0.45 | p(V368) ) % 0.19/0.45 & ( -p(V99) % 0.19/0.45 | p(V406) ) % 0.19/0.45 & ( p(V56) % 0.19/0.45 | p(V319) ) % 0.19/0.45 & ( p(V164) % 0.19/0.45 | -p(V12) ) % 0.19/0.45 & ( p(V88) % 0.19/0.45 | p(V402) ) % 0.19/0.45 & ( -p(V218) % 0.19/0.45 | p(V217) ) % 0.19/0.45 & ( p(V219) % 0.19/0.45 | -p(V218) ) % 0.19/0.45 & ( -p(V20) % 0.19/0.45 | -p(V226) ) % 0.19/0.45 & ( -p(V256) % 0.19/0.45 | -p(V30) ) % 0.19/0.45 & ( -p(V28) % 0.19/0.45 | p(V235) ) % 0.19/0.45 & ( -p(V49) % 0.19/0.45 | -p(V310) ) % 0.19/0.45 & ( p(V132) % 0.19/0.45 | -p(V30) % 0.19/0.45 | -p(V237) % 0.19/0.45 | -p(V131) ) % 0.19/0.45 & ( -p(V193) % 0.19/0.45 | -p(V9) ) % 0.19/0.45 & ( p(V240) % 0.19/0.45 | p(V522) % 0.19/0.45 | -p(V523) ) % 0.19/0.45 & ( p(V212) % 0.19/0.45 | -p(V213) % 0.19/0.45 | p(V37) ) % 0.19/0.45 & ( -p(V93) % 0.19/0.45 | -p(V445) ) % 0.19/0.45 & ( p(V412) % 0.19/0.45 | p(V86) ) % 0.19/0.45 & ( -p(V48) % 0.19/0.45 | -p(V299) ) % 0.19/0.45 & ( -p(V200) % 0.19/0.45 | p(V23) ) % 0.19/0.45 & ( -p(V122) % 0.19/0.45 | p(V500) ) % 0.19/0.45 & ***HERE*** ( -p(V508) % 0.19/0.45 | p(V432) ) % 0.19/0.45 & ( p(V230) % 0.19/0.45 | -p(V231) % 0.19/0.45 | p(V229) ) % 0.19/0.45 & ( -p(V209) % 0.19/0.45 | p(V210) % 0.19/0.45 | -p(V207) % 0.19/0.45 | -p(V208) ) % 0.19/0.45 & ( p(V438) % 0.19/0.45 | -p(V103) ) % 0.19/0.45 & ( p(V192) % 0.19/0.45 | -p(V191) ) % 0.19/0.45 & ( -p(V502) % 0.19/0.45 | p(V503) ) % 0.19/0.45 & ( -p(V352) % 0.19/0.45 | p(V353) ) % 0.19/0.45 & ( -p(V421) % 0.19/0.45 | p(V101) % 0.19/0.45 | p(V420) ) % 0.19/0.45 & ( -p(V408) % 0.19/0.45 | -p(V406) % 0.19/0.45 | p(V409) % 0.19/0.45 | -p(V407) % 0.19/0.45 | -p(V97) ) % 0.19/0.45 & ( p(V228) % 0.19/0.45 | -p(V29) ) % 0.19/0.45 & ( p(V295) % 0.19/0.45 | p(V55) ) % 0.19/0.45 & ( -p(V463) % 0.19/0.45 | -p(V103) ) % 0.19/0.45 & ( -p(V230) % 0.19/0.45 | p(V231) ) % 0.19/0.45 & ( -p(V215) % 0.19/0.45 | p(V219) ) % 0.19/0.45 & ( -p(V508) % 0.19/0.45 | p(V435) ) % 0.19/0.45 & ( -p(V248) % 0.19/0.45 | p(V246) ) % 0.19/0.45 & ( p(V517) % 0.19/0.45 | -p(V320) ) % 0.19/0.45 & ( -p(V77) % 0.19/0.45 | p(V348) ) % 0.19/0.45 & ( p(V91) % 0.19/0.45 | p(V92) % 0.19/0.45 | p(V442) % 0.19/0.45 | p(V93) ) % 0.19/0.45 & ( p(V79) % 0.19/0.45 | p(V377) ) % 0.19/0.45 & ( p(V208) % 0.19/0.45 | -p(V210) ) % 0.19/0.45 & ( p(V144) % 0.19/0.45 | p(V420) ) % 0.19/0.45 & ( p(V263) % 0.19/0.45 | -p(V262) ) % 0.19/0.45 & ( p(V81) % 0.19/0.45 | p(V368) ) % 0.19/0.45 & ( -p(V127) % 0.19/0.45 | -p(V128) % 0.19/0.45 | -p(V179) % 0.19/0.45 | -p(V8) ) % 0.19/0.45 & ( -p(V29) % 0.19/0.45 | p(V131) % 0.19/0.45 | -p(V132) % 0.19/0.45 | -p(V238) ) % 0.19/0.45 & ( -p(V152) % 0.19/0.45 | p(V531) ) % 0.19/0.45 & ( -p(V219) % 0.19/0.45 | p(V218) % 0.19/0.45 | p(V215) ) % 0.19/0.45 & ( p(V87) % 0.19/0.45 | p(V405) ) % 0.19/0.45 & ( p(V254) % 0.19/0.45 | -p(V253) ) % 0.19/0.45 & ( p(V134) % 0.19/0.45 | p(V268) ) % 0.19/0.45 & ( -p(V95) % 0.19/0.45 | -p(V443) % 0.19/0.45 | p(V442) ) % 0.19/0.45 & ( -p(V113) % 0.19/0.45 | -p(V485) ) % 0.19/0.45 & ( -p(V400) % 0.19/0.45 | p(V398) ) % 0.19/0.45 & ( p(V361) % 0.19/0.45 | p(V139) ) % 0.19/0.45 & ( p(V438) % 0.19/0.45 | -p(V508) ) % 0.19/0.45 & ( p(V371) % 0.19/0.45 | p(V142) ) % 0.19/0.45 & ( -p(V510) % 0.19/0.45 | p(V416) ) % 0.19/0.45 & ( p(V24) % 0.19/0.45 | p(V215) ) % 0.19/0.45 & ( -p(V330) % 0.19/0.45 | -p(V56) ) % 0.19/0.45 & ( -p(V74) % 0.19/0.45 | p(V348) ) % 0.19/0.45 & ( p(V322) % 0.19/0.45 | -p(V321) ) % 0.19/0.45 & ( -p(V81) % 0.19/0.45 | p(V365) ) % 0.19/0.45 & ( p(V169) % 0.19/0.45 | p(V4) ) % 0.19/0.45 & ( -p(V39) % 0.19/0.45 | p(V258) ) % 0.19/0.45 & ( p(V98) % 0.19/0.45 | p(V434) ) % 0.19/0.45 & ( p(V438) % 0.19/0.45 | -p(V105) ) % 0.19/0.45 & ( p(V525) % 0.19/0.45 | -p(V524) ) % 0.19/0.45 & ( p(V22) % 0.19/0.45 | -p(V186) % 0.19/0.45 | p(V19) ) % 0.19/0.45 & ( p(V213) % 0.19/0.45 | -p(V37) ) % 0.19/0.45 & ( -p(V503) % 0.19/0.45 | p(V502) % 0.19/0.45 | p(V497) ) % 0.19/0.45 & ( -p(V286) % 0.19/0.45 | p(V287) ) % 0.19/0.45 & ( -p(V100) % 0.19/0.45 | p(V407) ) % 0.19/0.45 & ( -p(V103) % 0.19/0.45 | -p(V108) % 0.19/0.45 | -p(V111) % 0.19/0.45 | p(V449) ) % 0.19/0.45 & ( p(V488) % 0.19/0.45 | p(V112) % 0.19/0.45 | p(V113) ) % 0.19/0.45 & ( -p(V418) % 0.19/0.45 | p(V98) ) % 0.19/0.45 & ( p(V268) % 0.19/0.45 | -p(V270) ) % 0.19/0.45 & ( p(V259) % 0.19/0.45 | -p(V132) ) % 0.19/0.45 & ( p(V399) % 0.19/0.45 | -p(V400) ) % 0.19/0.45 & ( p(V423) % 0.19/0.45 | p(V93) ) % 0.19/0.45 & ( -p(V178) % 0.19/0.45 | -p(V9) % 0.19/0.45 | p(V127) % 0.19/0.45 | -p(V128) ) % 0.19/0.45 & ( -p(V498) % 0.19/0.45 | -p(V119) % 0.19/0.45 | -p(V118) ) % 0.19/0.45 & ( -p(V353) % 0.19/0.45 | p(V354) ) % 0.19/0.45 & ( -p(V74) % 0.19/0.45 | -p(V373) ) % 0.19/0.45 & ( p(V521) % 0.19/0.45 | -p(V522) ) % 0.19/0.45 & ( p(V247) % 0.19/0.45 | -p(V47) ) % 0.19/0.45 & ( p(V125) % 0.19/0.45 | p(V157) ) % 0.19/0.45 & ( -p(V363) % 0.19/0.45 | p(V362) % 0.19/0.45 | p(V361) ) % 0.19/0.45 & ( p(V203) % 0.19/0.45 | -p(V526) ) % 0.19/0.45 & ( -p(V61) % 0.19/0.45 | p(V314) ) % 0.19/0.45 & ( p(V140) % 0.19/0.45 | p(V366) ) % 0.19/0.45 & ( -p(V486) % 0.19/0.45 | p(V487) ) % 0.19/0.45 & ( -p(V272) % 0.19/0.45 | p(V271) % 0.19/0.45 | -p(V45) ) % 0.19/0.45 & ( -p(V74) % 0.19/0.45 | p(V360) ) % 0.19/0.45 & ( p(V520) % 0.19/0.45 | -p(V521) % 0.19/0.45 | p(V270) ) % 0.19/0.45 & ( -p(V434) % 0.19/0.45 | -p(V98) % 0.19/0.45 | p(V433) ) % 0.19/0.45 & ( p(V170) % 0.19/0.45 | -p(V9) ) % 0.19/0.45 & ( -p(V506) % 0.19/0.45 | p(V480) ) % 0.19/0.45 & ( -p(V112) % 0.19/0.45 | -p(V485) ) % 0.19/0.45 & ( p(V131) % 0.19/0.45 | p(V264) ) % 0.19/0.45 & ( -p(V470) % 0.19/0.45 | -p(V103) ) % 0.19/0.45 & ( -p(V138) % 0.19/0.45 | -p(V56) % 0.19/0.45 | -p(V319) % 0.19/0.45 | -p(V137) ) % 0.19/0.45 & ( p(V309) % 0.19/0.45 | -p(V308) ) % 0.19/0.45 & ( p(V21) % 0.19/0.45 | p(V227) ) % 0.19/0.45 & ( -p(V17) % 0.19/0.45 | p(V165) ) % 0.19/0.45 & ( -p(V526) % 0.19/0.45 | p(V183) ) % 0.19/0.45 & ( -p(V8) % 0.19/0.45 | -p(V193) ) % 0.19/0.45 & ( p(V118) % 0.19/0.45 | -p(V492) ) % 0.19/0.45 & ( p(V222) % 0.19/0.45 | -p(V221) ) % 0.19/0.45 & ( -p(V250) % 0.19/0.45 | -p(V28) ) % 0.19/0.45 & ( -p(V146) % 0.19/0.45 | p(V448) ) % 0.19/0.45 & ( -p(V181) % 0.19/0.45 | -p(V8) ) % 0.19/0.45 & ( p(V81) % 0.19/0.45 | p(V364) % 0.19/0.45 | -p(V365) ) % 0.19/0.45 & ( -p(V131) % 0.19/0.45 | -p(V264) % 0.19/0.45 | -p(V132) ) % 0.19/0.45 & ( p(V91) % 0.19/0.45 | p(V93) % 0.19/0.45 | p(V92) % 0.19/0.45 | p(V430) ) % 0.19/0.45 & ( p(V293) % 0.19/0.45 | p(V134) ) % 0.19/0.45 & ( -p(V488) % 0.19/0.45 | -p(V112) ) % 0.19/0.45 & ( -p(V437) % 0.19/0.45 | p(V438) ) % 0.19/0.45 & ( p(V289) % 0.19/0.45 | -p(V54) % 0.19/0.45 | -p(V51) ) % 0.19/0.45 & ( -p(V172) % 0.19/0.45 | p(V13) ) % 0.19/0.45 & ( p(V135) % 0.19/0.45 | -p(V296) % 0.19/0.45 | -p(V136) % 0.19/0.45 | -p(V49) ) % 0.19/0.45 & ( -p(V26) % 0.19/0.45 | -p(V27) % 0.19/0.45 | -p(V206) ) % 0.19/0.45 & ( p(V321) % 0.19/0.45 | -p(V322) % 0.19/0.45 | -p(V60) ) % 0.19/0.45 & ( -p(V130) % 0.19/0.45 | p(V229) ) % 0.19/0.45 & ( p(V251) % 0.19/0.45 | p(V46) % 0.19/0.45 | -p(V252) % 0.19/0.45 | p(V45) ) % 0.19/0.45 & ( -p(V342) % 0.19/0.45 | p(V515) ) % 0.19/0.45 & ( -p(V19) % 0.19/0.45 | -p(V214) ) % 0.19/0.45 & ( p(V126) % 0.19/0.45 | p(V174) ) % 0.19/0.45 & ( p(V466) % 0.19/0.45 | -p(V506) ) % 0.19/0.45 & ( p(V103) % 0.19/0.45 | p(V458) ) % 0.19/0.45 & ( p(V302) % 0.19/0.45 | p(V48) % 0.19/0.45 | p(V49) ) % 0.19/0.45 & ( -p(V515) % 0.19/0.45 | p(V342) % 0.19/0.45 | p(V514) ) % 0.19/0.45 & ( p(V141) % 0.19/0.45 | -p(V393) % 0.19/0.45 | -p(V142) ) % 0.19/0.45 & ( p(V25) % 0.19/0.45 | p(V26) % 0.19/0.45 | p(V191) % 0.19/0.45 | -p(V192) ) % 0.19/0.45 & ( p(V473) % 0.19/0.45 | p(V104) % 0.19/0.45 | p(V103) ) % 0.19/0.45 & ( p(V501) % 0.19/0.45 | p(V123) ) % 0.19/0.45 & ( p(V178) % 0.19/0.45 | p(V128) ) % 0.19/0.45 & ( -p(V266) % 0.19/0.45 | -p(V47) % 0.19/0.45 | -p(V46) ) % 0.19/0.45 & ( -p(V93) % 0.19/0.45 | -p(V439) ) % 0.19/0.45 & ( p(V28) % 0.19/0.45 | p(V241) % 0.19/0.45 | p(V29) % 0.19/0.45 | p(V30) ) % 0.19/0.45 & ( -p(V367) % 0.19/0.45 | p(V73) % 0.19/0.45 | p(V366) ) % 0.19/0.45 & ( -p(V520) % 0.19/0.45 | p(V273) ) % 0.19/0.45 & ( p(V174) % 0.19/0.45 | p(V125) ) % 0.19/0.45 & ( p(V532) % 0.19/0.45 | -p(V531) % 0.19/0.45 | -p(V1) ) % 0.19/0.45 & ( -p(V136) % 0.19/0.45 | -p(V297) % 0.19/0.45 | -p(V48) % 0.19/0.45 | -p(V135) ) % 0.19/0.45 & ( -p(V13) % 0.19/0.45 | -p(V191) % 0.19/0.45 | p(V190) ) % 0.19/0.45 & ( -p(V522) % 0.19/0.45 | p(V263) ) % 0.19/0.45 & ( -p(V420) % 0.19/0.45 | p(V421) ) % 0.19/0.45 & ( p(V392) % 0.19/0.45 | -p(V512) ) % 0.19/0.45 & ( -p(V129) % 0.19/0.45 | p(V208) ) % 0.19/0.45 & ( -p(V414) % 0.19/0.45 | -p(V83) ) % 0.19/0.45 & ( -p(V106) % 0.19/0.45 | -p(V471) % 0.19/0.45 | p(V470) ) % 0.19/0.45 & ( -p(V506) % 0.19/0.45 | p(V481) ) % 0.19/0.45 & ( p(V51) % 0.19/0.45 | -p(V289) ) % 0.19/0.45 & ( p(V134) % 0.19/0.45 | p(V291) ) % 0.19/0.45 & ( -p(V443) % 0.19/0.45 | p(V444) ) % 0.19/0.45 & ( -p(V532) % 0.19/0.45 | p(V1) ) % 0.19/0.45 & ( -p(V72) % 0.19/0.45 | p(V323) ) % 0.19/0.45 & ( -p(V265) % 0.19/0.45 | p(V38) % 0.19/0.45 | p(V264) ) % 0.19/0.45 & ( p(V124) % 0.19/0.45 | p(V155) ) % 0.19/0.45 & ( -p(V83) % 0.19/0.45 | -p(V401) ) % 0.19/0.45 & ( p(V429) % 0.19/0.45 | -p(V508) ) % 0.19/0.45 & ( p(V360) % 0.19/0.45 | -p(V359) ) % 0.19/0.45 & ( p(V225) % 0.19/0.45 | -p(V224) ) % 0.19/0.45 & ( -p(V143) % 0.19/0.45 | p(V398) ) % 0.19/0.45 & ( p(V299) % 0.19/0.45 | p(V49) % 0.19/0.45 | p(V48) ) % 0.19/0.45 & ( -p(V210) % 0.19/0.45 | p(V207) ) % 0.19/0.45 & ( p(V450) % 0.19/0.45 | -p(V449) ) % 0.19/0.45 & ( -p(V115) % 0.19/0.45 | p(V469) ) % 0.19/0.45 & ( p(V106) % 0.19/0.45 | p(V471) ) % 0.19/0.45 & ( -p(V88) % 0.19/0.45 | p(V386) ) % 0.19/0.45 & ( -p(V378) % 0.19/0.45 | p(V83) % 0.19/0.45 | p(V85) ) % 0.19/0.45 & ( -p(V391) % 0.19/0.45 | p(V392) ) % 0.19/0.45 & ( p(V200) % 0.19/0.45 | -p(V201) % 0.19/0.45 | p(V199) ) % 0.19/0.45 & ( -p(V91) % 0.19/0.45 | -p(V433) ) % 0.19/0.45 & ( -p(V97) % 0.19/0.45 | p(V436) % 0.19/0.45 | -p(V437) ) % 0.19/0.45 & ( -p(V55) % 0.19/0.45 | p(V273) ) % 0.19/0.45 & ( -p(V109) % 0.19/0.45 | p(V432) ) % 0.19/0.45 & ( -p(V522) % 0.19/0.45 | p(V252) ) % 0.19/0.45 & ( p(V122) % 0.19/0.45 | -p(V500) % 0.19/0.45 | -p(V151) ) % 0.19/0.45 & ( -p(V312) % 0.19/0.45 | p(V60) % 0.19/0.45 | p(V311) ) % 0.19/0.45 & ( p(V125) % 0.19/0.45 | -p(V126) % 0.19/0.45 | -p(V3) % 0.19/0.45 | -p(V156) ) % 0.19/0.45 & ( p(V49) % 0.19/0.45 | p(V50) % 0.19/0.45 | -p(V276) ) % 0.19/0.45 & ( p(V456) % 0.19/0.45 | p(V111) ) % 0.19/0.45 & ( -p(V205) % 0.19/0.45 | -p(V195) % 0.19/0.45 | -p(V203) % 0.19/0.45 | -p(V192) % 0.19/0.45 | -p(V201) % 0.19/0.45 | -p(V206) % 0.19/0.45 | -p(V189) % 0.19/0.45 | -p(V183) % 0.19/0.45 | -p(V198) % 0.19/0.45 | p(V526) % 0.19/0.45 | -p(V525) ) % 0.19/0.45 & ( -p(V75) % 0.19/0.45 | p(V349) ) % 0.19/0.45 & ( p(V371) % 0.19/0.45 | p(V73) ) % 0.19/0.45 & ( -p(V100) % 0.19/0.45 | p(V406) ) % 0.19/0.45 & ( -p(V514) % 0.19/0.45 | p(V367) ) % 0.19/0.45 & ( -p(V270) % 0.19/0.45 | p(V521) ) % 0.19/0.45 & ( -p(V59) % 0.19/0.45 | -p(V304) % 0.19/0.45 | p(V305) ) % 0.19/0.45 & ( -p(V473) % 0.19/0.45 | -p(V103) ) % 0.19/0.45 & ( -p(V134) % 0.19/0.45 | p(V288) ) % 0.19/0.45 & ( -p(V258) % 0.19/0.45 | p(V257) % 0.19/0.45 | p(V39) ) % 0.19/0.45 & ( p(V209) % 0.19/0.45 | -p(V210) ) % 0.19/0.45 & ( -p(V152) % 0.19/0.45 | -p(V124) % 0.19/0.45 | -p(V1) ) % 0.19/0.45 & ( p(V347) % 0.19/0.45 | -p(V351) % 0.19/0.45 | p(V350) ) % 0.19/0.45 & ( -p(V223) % 0.19/0.45 | -p(V19) ) % 0.19/0.45 & ( -p(V327) % 0.19/0.45 | -p(V326) % 0.19/0.45 | p(V328) % 0.19/0.45 | -p(V69) ) % 0.19/0.45 & ( -p(V336) % 0.19/0.45 | -p(V138) % 0.19/0.45 | -p(V137) ) % 0.19/0.45 & ( p(V344) % 0.19/0.45 | -p(V345) % 0.19/0.45 | p(V82) ) % 0.19/0.45 & ( p(V92) % 0.19/0.45 | p(V96) % 0.19/0.45 | -p(V408) ) % 0.19/0.45 & ( -p(V285) % 0.19/0.45 | -p(V40) ) % 0.19/0.45 & ( -p(V427) % 0.19/0.45 | -p(V91) ) % 0.19/0.45 & ( p(V297) % 0.19/0.45 | p(V48) ) % 0.19/0.45 & ( p(V104) % 0.19/0.45 | p(V460) % 0.19/0.45 | p(V103) ) % 0.19/0.45 & ( -p(V484) % 0.19/0.45 | p(V482) ) % 0.19/0.45 & ( -p(V56) % 0.19/0.45 | -p(V324) ) % 0.19/0.45 & ( p(V422) % 0.19/0.45 | -p(V510) ) % 0.19/0.45 & ( p(V46) % 0.19/0.45 | -p(V260) ) % 0.19/0.45 & ( -p(V26) % 0.19/0.45 | p(V192) ) % 0.19/0.45 & ( p(V372) % 0.19/0.45 | -p(V513) % 0.19/0.45 | p(V512) ) % 0.19/0.45 & ( -p(V83) % 0.19/0.45 | p(V389) ) % 0.19/0.45 & ( p(V276) % 0.19/0.45 | -p(V50) ) % 0.19/0.45 & ( p(V28) % 0.19/0.45 | p(V234) % 0.19/0.45 | -p(V235) ) % 0.19/0.45 & ( p(V9) % 0.19/0.45 | p(V178) ) % 0.19/0.45 & ( -p(V305) % 0.19/0.45 | p(V306) ) % 0.19/0.45 & ( -p(V133) % 0.19/0.45 | p(V134) % 0.19/0.45 | -p(V288) ) % 0.19/0.45 & ( p(V148) % 0.19/0.45 | p(V457) ) % 0.19/0.45 & ( p(V208) % 0.19/0.45 | p(V130) ) % 0.19/0.45 & ( p(V8) % 0.19/0.45 | p(V179) ) % 0.19/0.45 & ( -p(V289) % 0.19/0.45 | p(V54) ) % 0.19/0.45 & ( -p(V459) % 0.19/0.45 | p(V457) ) % 0.19/0.45 & ( -p(V430) % 0.19/0.45 | -p(V92) ) % 0.19/0.45 & ( -p(V110) % 0.19/0.45 | -p(V111) % 0.19/0.45 | -p(V456) ) % 0.19/0.45 & ( p(V210) % 0.19/0.45 | p(V524) % 0.19/0.45 | -p(V525) ) % 0.19/0.45 & ( p(V410) % 0.19/0.45 | -p(V409) ) % 0.19/0.45 & ( -p(V315) % 0.19/0.45 | p(V316) ) % 0.19/0.45 & ( p(V380) % 0.19/0.45 | -p(V379) ) % 0.19/0.45 & ( p(V10) % 0.19/0.45 | p(V177) ) % 0.19/0.45 & ( p(V140) % 0.19/0.45 | -p(V139) % 0.19/0.45 | -p(V361) ) % 0.19/0.45 & ( -p(V310) % 0.19/0.45 | p(V311) ) % 0.19/0.45 & ( -p(V196) % 0.19/0.45 | -p(V8) ) % 0.19/0.45 & ( p(V26) % 0.19/0.45 | -p(V200) ) % 0.19/0.45 & ( p(V283) % 0.19/0.45 | -p(V282) ) % 0.19/0.45 & ( -p(V430) % 0.19/0.45 | p(V431) ) % 0.19/0.45 & ( p(V207) % 0.19/0.45 | -p(V130) ) % 0.19/0.45 & ( -p(V143) % 0.19/0.45 | -p(V144) % 0.19/0.45 | -p(V420) ) % 0.19/0.45 & ( -p(V199) % 0.19/0.45 | p(V128) % 0.19/0.45 | -p(V127) ) % 0.19/0.46 & ( p(V152) % 0.19/0.46 | p(V124) ) % 0.19/0.46 & ( p(V55) % 0.19/0.46 | p(V272) % 0.19/0.46 | -p(V273) ) % 0.19/0.46 & ( -p(V46) % 0.19/0.46 | p(V260) % 0.19/0.46 | -p(V43) ) % 0.19/0.46 & ( -p(V326) % 0.19/0.46 | p(V67) % 0.19/0.46 | p(V64) ) % 0.19/0.46 & ( p(V357) % 0.19/0.46 | -p(V514) ) % 0.19/0.46 & ( -p(V298) % 0.19/0.46 | p(V296) ) % 0.19/0.46 & ( p(V56) % 0.19/0.46 | p(V57) % 0.19/0.46 | p(V324) ) % 0.19/0.46 & ( -p(V477) % 0.19/0.46 | p(V478) ) % 0.19/0.46 & ( p(V413) % 0.19/0.46 | -p(V510) ) % 0.19/0.46 & ( -p(V110) % 0.19/0.46 | p(V432) ) % 0.19/0.46 & ( -p(V147) % 0.19/0.46 | -p(V148) % 0.19/0.46 | -p(V479) ) % 0.19/0.46 & ( p(V2) % 0.19/0.46 | p(V3) % 0.19/0.46 | p(V162) ) % 0.19/0.46 & ( -p(V32) % 0.19/0.46 | p(V216) ) % 0.19/0.46 & ( p(V427) % 0.19/0.46 | p(V92) % 0.19/0.46 | p(V91) % 0.19/0.46 | p(V93) ) % 0.19/0.46 & ( p(V434) % 0.19/0.46 | p(V111) % 0.19/0.46 | p(V104) % 0.19/0.46 | -p(V435) ) % 0.19/0.46 & ( -p(V233) % 0.19/0.46 | -p(V236) % 0.19/0.46 | -p(V228) % 0.19/0.46 | -p(V523) % 0.19/0.46 | -p(V222) % 0.19/0.46 | p(V524) % 0.19/0.46 | -p(V213) % 0.19/0.46 | -p(V231) % 0.19/0.46 | -p(V219) % 0.19/0.46 | -p(V235) % 0.19/0.46 | -p(V225) ) % 0.19/0.46 & ( -p(V119) % 0.19/0.46 | p(V490) ) % 0.19/0.46 & ( p(V128) % 0.19/0.46 | p(V179) ) % 0.19/0.46 & ( -p(V63) % 0.19/0.46 | -p(V358) ) % 0.19/0.46 & ( -p(V466) % 0.19/0.46 | p(V464) % 0.19/0.46 | p(V465) % 0.19/0.46 | p(V114) ) % 0.19/0.46 & ( p(V425) % 0.19/0.46 | p(V146) ) % 0.19/0.46 & ( -p(V436) % 0.19/0.46 | -p(V93) ) % 0.19/0.46 & ( -p(V93) % 0.19/0.46 | -p(V433) ) % 0.19/0.46 & ( p(V75) % 0.19/0.46 | p(V73) % 0.19/0.46 | p(V74) % 0.19/0.46 | p(V387) ) % 0.19/0.46 & ( p(V146) % 0.19/0.46 | -p(V423) % 0.19/0.46 | -p(V93) % 0.19/0.46 | -p(V145) ) % 0.19/0.46 & ( p(V386) % 0.19/0.46 | -p(V385) ) % 0.19/0.46 & ( p(V507) % 0.19/0.46 | -p(V508) ) % 0.19/0.46 & ( p(V173) % 0.19/0.46 | -p(V171) ) % 0.19/0.46 & ( p(V108) % 0.19/0.46 | p(V464) ) % 0.19/0.46 & ( -p(V24) % 0.19/0.46 | p(V188) % 0.19/0.46 | -p(V186) % 0.19/0.46 | -p(V187) ) % 0.19/0.46 & ( p(V173) % 0.19/0.46 | -p(V172) ) % 0.19/0.46 & ( p(V39) % 0.19/0.46 | p(V38) % 0.19/0.46 | p(V282) % 0.19/0.46 | p(V40) ) % 0.19/0.46 & ( p(V354) % 0.19/0.46 | -p(V80) ) % 0.19/0.46 & ( -p(V21) % 0.19/0.46 | p(V187) ) % 0.19/0.46 & ( -p(V455) % 0.19/0.46 | p(V109) % 0.19/0.46 | p(V454) ) % 0.19/0.46 & ( -p(V520) % 0.19/0.46 | p(V278) ) % 0.19/0.46 & ( p(V136) % 0.19/0.46 | p(V315) ) % 0.19/0.46 & ( -p(V446) % 0.19/0.46 | p(V447) ) % 0.19/0.46 & ( p(V258) % 0.19/0.46 | -p(V522) ) % 0.19/0.46 & ( -p(V147) % 0.19/0.46 | -p(V458) % 0.19/0.46 | -p(V148) % 0.19/0.46 | -p(V103) ) % 0.19/0.46 & ( -p(V127) % 0.19/0.46 | -p(V10) % 0.19/0.46 | -p(V177) % 0.19/0.46 | p(V128) ) % 0.19/0.46 & ( -p(V126) % 0.19/0.46 | -p(V125) % 0.19/0.46 | -p(V174) ) % 0.19/0.46 & ( p(V518) % 0.19/0.46 | -p(V519) % 0.19/0.46 | p(V298) ) % 0.19/0.46 & ( p(V419) % 0.19/0.46 | -p(V417) ) % 0.19/0.46 & ( p(V191) % 0.19/0.46 | -p(V190) ) % 0.19/0.46 & ( p(V157) % 0.19/0.46 | p(V2) ) % 0.19/0.46 & ( -p(V180) % 0.19/0.46 | p(V178) ) % 0.19/0.46 & ( -p(V10) % 0.19/0.46 | -p(V190) ) % 0.19/0.46 & ( p(V304) % 0.19/0.46 | -p(V60) ) % 0.19/0.46 & ( -p(V224) % 0.19/0.46 | -p(V22) % 0.19/0.46 | p(V223) ) % 0.19/0.46 & ( p(V259) % 0.19/0.46 | p(V260) % 0.19/0.46 | -p(V261) ) % 0.19/0.46 & ( p(V75) % 0.19/0.46 | -p(V349) % 0.19/0.46 | p(V82) % 0.19/0.46 | p(V80) % 0.19/0.46 | p(V76) ) % 0.19/0.46 & ( -p(V514) % 0.19/0.46 | p(V515) ) % 0.19/0.46 & ( -p(V77) % 0.19/0.46 | p(V384) % 0.19/0.46 | -p(V385) ) % 0.19/0.46 & ( -p(V524) % 0.19/0.46 | p(V222) ) % 0.19/0.46 & ( p(V42) % 0.19/0.46 | p(V283) ) % 0.19/0.46 & ( p(V423) % 0.19/0.46 | -p(V146) ) % 0.19/0.46 & ( -p(V92) % 0.19/0.46 | p(V407) ) % 0.19/0.46 & ( -p(V431) % 0.19/0.46 | p(V430) % 0.19/0.46 | -p(V99) ) % 0.19/0.46 & ( p(V257) % 0.19/0.46 | -p(V256) ) % 0.19/0.46 & ( -p(V73) % 0.19/0.46 | -p(V376) ) % 0.19/0.46 & ( -p(V121) % 0.19/0.46 | -p(V118) % 0.19/0.46 | p(V492) ) % 0.19/0.46 & ( -p(V57) % 0.19/0.46 | -p(V321) ) % 0.19/0.46 & ( p(V265) % 0.19/0.46 | -p(V264) ) % 0.19/0.46 & ( -p(V334) % 0.19/0.46 | p(V71) ) % 0.19/0.46 & ( -p(V526) % 0.19/0.46 | p(V189) ) % 0.19/0.46 & ( p(V288) % 0.19/0.46 | p(V133) ) % 0.19/0.46 & ( p(V491) % 0.19/0.46 | -p(V149) ) % 0.19/0.46 & ( p(V408) % 0.19/0.46 | -p(V409) ) % 0.19/0.46 & ( p(V151) % 0.19/0.46 | p(V500) ) % 0.19/0.46 & ( -p(V67) % 0.19/0.46 | p(V326) ) % 0.19/0.46 & ( -p(V131) % 0.19/0.46 | p(V262) ) % 0.19/0.46 & ( -p(V132) % 0.19/0.46 | p(V131) % 0.19/0.46 | -p(V262) ) % 0.19/0.46 & ( -p(V429) % 0.19/0.46 | p(V428) % 0.19/0.46 | p(V111) ) % 0.19/0.46 & ( -p(V464) % 0.19/0.46 | p(V466) ) % 0.19/0.46 & ( p(V367) % 0.19/0.46 | -p(V73) ) % 0.19/0.46 & ( -p(V508) % 0.19/0.46 | p(V441) ) % 0.19/0.46 & ( p(V515) % 0.19/0.46 | -p(V516) ) % 0.19/0.46 & ( p(V91) % 0.19/0.46 | p(V93) % 0.19/0.46 | p(V433) % 0.19/0.46 | p(V92) ) % 0.19/0.46 & ( -p(V185) % 0.19/0.46 | p(V189) ) % 0.19/0.46 & ( -p(V204) % 0.19/0.46 | p(V205) ) % 0.19/0.46 & ( -p(V485) % 0.19/0.46 | p(V486) ) % 0.19/0.46 & ( p(V236) % 0.19/0.46 | p(V37) ) % 0.19/0.46 & ( -p(V412) % 0.19/0.46 | p(V413) ) % 0.19/0.46 & ( -p(V91) % 0.19/0.46 | -p(V445) ) % 0.19/0.46 & ( -p(V102) % 0.19/0.46 | p(V403) ) % 0.19/0.46 & ( p(V251) % 0.19/0.46 | -p(V250) ) % 0.19/0.46 & ( p(V19) % 0.19/0.46 | p(V208) ) % 0.19/0.46 & ( -p(V263) % 0.19/0.46 | p(V46) % 0.19/0.46 | p(V262) ) % 0.19/0.46 & ( -p(V242) % 0.19/0.46 | p(V241) % 0.19/0.46 | -p(V35) ) % 0.19/0.46 & ( p(V197) % 0.19/0.46 | p(V11) ) % 0.19/0.46 & ( p(V421) % 0.19/0.46 | -p(V510) ) % 0.19/0.46 & ( p(V343) % 0.19/0.46 | -p(V344) % 0.19/0.46 | -p(V70) ) % 0.19/0.46 & ( p(V452) % 0.19/0.46 | -p(V453) % 0.19/0.46 | p(V451) ) % 0.19/0.46 & ( p(V9) % 0.19/0.46 | p(V8) % 0.19/0.46 | p(V181) % 0.19/0.46 | p(V10) ) % 0.19/0.46 & ( p(V175) % 0.19/0.46 | -p(V8) ) % 0.19/0.46 & ( -p(V342) % 0.19/0.46 | p(V341) ) % 0.19/0.46 & ( -p(V161) % 0.19/0.46 | -p(V527) % 0.19/0.46 | -p(V170) % 0.19/0.46 | -p(V167) % 0.19/0.46 | p(V528) % 0.19/0.46 | -p(V176) % 0.19/0.46 | -p(V173) % 0.19/0.46 | -p(V175) ) % 0.19/0.46 & ( p(V423) % 0.19/0.46 | -p(V426) ) % 0.19/0.46 & ( -p(V356) % 0.19/0.46 | p(V355) % 0.19/0.46 | -p(V67) ) % 0.19/0.46 & ( -p(V483) % 0.19/0.46 | p(V484) % 0.19/0.46 | -p(V482) ) % 0.19/0.46 & ( -p(V526) % 0.19/0.46 | p(V206) ) % 0.19/0.46 & ( -p(V70) % 0.19/0.46 | p(V327) ) % 0.19/0.46 & ( p(V373) % 0.19/0.46 | p(V74) % 0.19/0.46 | p(V75) % 0.19/0.46 | p(V73) ) % 0.19/0.46 & ( p(V149) % 0.19/0.46 | -p(V491) % 0.19/0.46 | -p(V150) ) % 0.19/0.46 & ( p(V508) % 0.19/0.46 | -p(V509) % 0.19/0.46 | p(V426) ) % 0.19/0.46 & ( p(V394) % 0.19/0.46 | -p(V89) ) % 0.19/0.46 & ( p(V243) % 0.19/0.46 | -p(V522) ) % 0.19/0.46 & ( p(V3) % 0.19/0.46 | p(V156) ) % 0.19/0.46 & ( p(V327) % 0.19/0.46 | -p(V328) ) % 0.19/0.46 & ( p(V233) % 0.19/0.46 | -p(V524) ) % 0.19/0.46 & ( p(V160) % 0.19/0.46 | -p(V159) ) % 0.19/0.46 & ( p(V478) % 0.19/0.46 | -p(V476) ) % 0.19/0.46 & ( p(V131) % 0.19/0.46 | p(V239) ) % 0.19/0.46 & ( p(V335) % 0.19/0.46 | -p(V334) ) % 0.19/0.46 & ( p(V365) % 0.19/0.46 | -p(V364) ) % 0.19/0.46 & ( p(V195) % 0.19/0.46 | -p(V25) ) % 0.19/0.46 & ( p(V207) % 0.19/0.46 | p(V129) ) % 0.19/0.46 & ( p(V306) % 0.19/0.46 | -p(V518) ) % 0.19/0.46 & ( -p(V343) % 0.19/0.46 | -p(V63) ) % 0.19/0.46 & ( -p(V74) % 0.19/0.46 | -p(V384) ) % 0.19/0.46 & ( -p(V37) % 0.19/0.46 | p(V217) ) % 0.19/0.46 & ( -p(V100) % 0.19/0.46 | p(V413) ) % 0.19/0.46 & ( p(V317) % 0.19/0.46 | p(V62) ) % 0.19/0.46 & ( -p(V512) % 0.19/0.46 | p(V389) ) % 0.19/0.46 & ( p(V228) % 0.19/0.46 | -p(V524) ) % 0.19/0.46 & ( -p(V15) % 0.19/0.46 | p(V181) % 0.19/0.46 | -p(V182) ) % 0.19/0.46 & ( -p(V142) % 0.19/0.46 | p(V369) ) % 0.19/0.46 & ( -p(V35) % 0.19/0.46 | p(V222) ) % 0.19/0.46 & ( -p(V241) % 0.19/0.46 | -p(V30) ) % 0.19/0.46 & ( -p(V355) % 0.19/0.46 | p(V356) ) % 0.19/0.46 & ( -p(V237) % 0.19/0.46 | -p(V238) % 0.19/0.46 | -p(V239) % 0.19/0.46 | p(V240) ) % 0.19/0.46 & ( -p(V448) % 0.19/0.46 | p(V146) % 0.19/0.46 | -p(V145) ) % 0.19/0.46 & ( -p(V134) % 0.19/0.46 | p(V133) % 0.19/0.46 | -p(V39) % 0.19/0.46 | -p(V268) ) % 0.19/0.46 & ( p(V84) % 0.19/0.46 | p(V398) ) % 0.19/0.46 & ( p(V509) % 0.19/0.46 | -p(V426) ) % 0.19/0.46 & ( p(V245) % 0.19/0.46 | -p(V244) ) % 0.19/0.46 & ( p(V115) % 0.19/0.46 | p(V474) % 0.19/0.46 | -p(V475) ) % 0.19/0.46 & ( -p(V419) % 0.19/0.46 | p(V417) % 0.19/0.46 | p(V418) ) % 0.19/0.46 & ( -p(V504) % 0.19/0.46 | p(V490) ) % 0.19/0.46 & ( -p(V138) % 0.19/0.46 | p(V137) % 0.19/0.46 | -p(V333) ) % 0.19/0.46 & ( -p(V461) % 0.19/0.46 | -p(V109) % 0.19/0.46 | p(V460) ) % 0.19/0.46 & ( -p(V465) % 0.19/0.46 | p(V117) ) % 0.19/0.46 & ( p(V285) % 0.19/0.46 | p(V39) % 0.19/0.46 | p(V40) % 0.19/0.46 | p(V38) ) % 0.19/0.46 & ( -p(V202) % 0.19/0.46 | p(V203) ) % 0.19/0.46 & ( -p(V284) % 0.19/0.46 | p(V53) % 0.19/0.46 | p(V283) ) % 0.19/0.46 & ( -p(V280) % 0.19/0.46 | p(V281) ) % 0.19/0.46 & ( p(V206) % 0.19/0.46 | p(V27) ) % 0.19/0.46 & ( -p(V321) % 0.19/0.46 | -p(V56) ) % 0.19/0.46 & ( -p(V522) % 0.19/0.46 | p(V266) ) % 0.19/0.46 & ( p(V29) % 0.19/0.46 | -p(V228) % 0.19/0.46 | p(V227) ) % 0.19/0.46 & ( p(V274) % 0.19/0.46 | -p(V44) % 0.19/0.46 | -p(V275) ) % 0.19/0.46 & ( p(V347) % 0.19/0.46 | p(V69) ) % 0.19/0.46 & ( -p(V370) % 0.19/0.46 | -p(V371) % 0.19/0.46 | p(V372) % 0.19/0.46 | -p(V369) ) % 0.19/0.46 & ( -p(V139) % 0.19/0.46 | p(V364) ) % 0.19/0.46 & p(V532) % 0.19/0.46 & ( -p(V234) % 0.19/0.46 | -p(V130) % 0.19/0.46 | -p(V129) ) % 0.19/0.46 & ( p(V85) % 0.19/0.46 | p(V415) ) % 0.19/0.46 & ( p(V19) % 0.19/0.46 | p(V20) % 0.19/0.46 | p(V214) % 0.19/0.46 | p(V18) ) % 0.19/0.46 & ( -p(V241) % 0.19/0.46 | p(V242) ) % 0.19/0.46 & ( p(V251) % 0.19/0.46 | p(V33) ) % 0.19/0.46 & ( p(V29) % 0.19/0.46 | p(V28) % 0.19/0.46 | p(V30) % 0.19/0.46 | p(V250) ) % 0.19/0.46 & ( -p(V211) % 0.19/0.46 | -p(V19) ) % 0.19/0.46 & ( p(V451) % 0.19/0.46 | p(V146) ) % 0.19/0.46 & ( p(V158) % 0.19/0.46 | -p(V157) % 0.19/0.46 | -p(V156) ) % 0.19/0.46 & ( p(V130) % 0.19/0.46 | p(V232) ) % 0.19/0.46 & ( -p(V10) % 0.19/0.46 | -p(V184) ) % 0.19/0.46 & ( -p(V193) % 0.19/0.46 | -p(V10) ) % 0.19/0.46 & ( p(V287) % 0.19/0.46 | -p(V520) ) % 0.19/0.46 & ( p(V327) % 0.19/0.46 | -p(V72) ) % 0.19/0.46 & ( p(V417) % 0.19/0.46 | p(V144) ) % 0.19/0.46 & ( -p(V3) % 0.19/0.46 | p(V153) ) % 0.19/0.46 & ( -p(V250) % 0.19/0.46 | -p(V29) ) % 0.19/0.46 & ( p(V242) % 0.19/0.46 | p(V35) ) % 0.19/0.46 & ( p(V148) % 0.19/0.46 | p(V479) ) % 0.19/0.46 & ( -p(V256) % 0.19/0.46 | -p(V29) ) % 0.19/0.46 & ( -p(V323) % 0.19/0.46 | -p(V338) % 0.19/0.46 | -p(V337) % 0.19/0.46 | -p(V332) % 0.19/0.46 | -p(V515) % 0.19/0.46 | p(V516) % 0.19/0.46 | -p(V335) % 0.19/0.46 | -p(V329) ) % 0.19/0.46 & ( -p(V449) % 0.19/0.46 | p(V111) ) % 0.19/0.46 & ( -p(V302) % 0.19/0.46 | -p(V49) ) % 0.19/0.46 & ( p(V112) % 0.19/0.46 | p(V113) % 0.19/0.46 | p(V485) ) % 0.19/0.46 & ( -p(V38) % 0.19/0.46 | -p(V282) ) % 0.19/0.46 & ( p(V500) % 0.19/0.46 | -p(V502) ) % 0.19/0.46 & ( -p(V46) % 0.19/0.46 | p(V263) ) % 0.19/0.46 & ( -p(V366) % 0.19/0.46 | p(V367) ) % 0.19/0.46 & ( -p(V274) % 0.19/0.46 | p(V275) ) % 0.19/0.46 & ( -p(V101) % 0.19/0.46 | p(V418) % 0.19/0.46 | -p(V98) % 0.19/0.46 | -p(V91) ) % 0.19/0.46 & ( -p(V6) % 0.19/0.46 | p(V153) ) % 0.19/0.46 & ( -p(V145) % 0.19/0.46 | -p(V146) % 0.19/0.46 | -p(V425) % 0.19/0.46 | -p(V91) ) % 0.19/0.46 & ( -p(V341) % 0.19/0.46 | -p(V339) % 0.19/0.46 | -p(V340) % 0.19/0.46 | p(V342) ) % 0.19/0.46 & ( -p(V29) % 0.19/0.46 | -p(V244) ) % 0.19/0.46 & ( p(V176) % 0.19/0.46 | p(V16) ) % 0.19/0.46 & ( -p(V397) % 0.19/0.46 | -p(V90) % 0.19/0.46 | -p(V89) ) % 0.19/0.46 & ( -p(V137) % 0.19/0.46 | p(V318) ) % 0.19/0.46 & ( -p(V184) % 0.19/0.46 | p(V185) ) % 0.19/0.46 & ( -p(V65) % 0.19/0.46 | p(V140) % 0.19/0.46 | -p(V339) % 0.19/0.46 | -p(V139) ) % 0.19/0.46 & ( p(V28) % 0.19/0.46 | p(V29) % 0.19/0.46 | p(V256) % 0.19/0.46 | p(V30) ) % 0.19/0.46 & ( p(V30) % 0.19/0.46 | p(V29) % 0.19/0.46 | p(V253) % 0.19/0.46 | p(V28) ) % 0.19/0.46 & ( p(V427) % 0.19/0.46 | -p(V100) % 0.19/0.46 | -p(V428) ) % 0.19/0.46 & ( -p(V83) % 0.19/0.46 | -p(V411) ) % 0.19/0.46 & ( -p(V155) % 0.19/0.46 | -p(V529) % 0.19/0.46 | p(V530) ) % 0.19/0.46 & ( -p(V104) % 0.19/0.46 | p(V435) ) % 0.19/0.46 & ( p(V65) % 0.19/0.46 | p(V64) % 0.19/0.46 | p(V63) % 0.19/0.46 | p(V352) ) % 0.19/0.46 & ( -p(V104) % 0.19/0.46 | -p(V463) ) % 0.19/0.46 & ( p(V3) % 0.19/0.46 | p(V159) % 0.19/0.46 | p(V2) ) % 0.19/0.46 & ( -p(V207) % 0.19/0.46 | p(V130) % 0.19/0.46 | -p(V129) % 0.19/0.46 | -p(V20) ) % 0.19/0.46 & ( p(V266) % 0.19/0.46 | p(V47) ) % 0.19/0.46 & ( -p(V442) % 0.19/0.46 | -p(V92) ) % 0.19/0.46 & ( -p(V447) % 0.19/0.46 | p(V103) % 0.19/0.46 | p(V446) ) % 0.19/0.46 & ( p(V340) % 0.19/0.46 | -p(V342) ) % 0.19/0.46 & ( p(V29) % 0.19/0.46 | p(V238) ) % 0.19/0.46 & ( p(V77) % 0.19/0.46 | p(V385) ) % 0.19/0.46 & ( p(V95) % 0.19/0.46 | p(V443) ) % 0.19/0.46 & ( p(V513) % 0.19/0.46 | -p(V372) ) % 0.19/0.46 & ( p(V523) % 0.19/0.46 | -p(V522) ) % 0.19/0.46 & ( -p(V313) % 0.19/0.46 | p(V135) % 0.19/0.46 | -p(V136) ) % 0.19/0.46 & ( p(V357) % 0.19/0.46 | -p(V80) ) % 0.19/0.46 & ( p(V153) % 0.19/0.46 | -p(V7) ) % 0.19/0.46 & ( -p(V69) % 0.19/0.46 | -p(V347) % 0.19/0.46 | p(V346) ) % 0.19/0.46 & ( -p(V260) % 0.19/0.46 | p(V261) ) % 0.19/0.46 & ( p(V322) % 0.19/0.46 | p(V60) ) % 0.19/0.46 & ( p(V145) % 0.19/0.46 | p(V425) ) % 0.19/0.46 & ( -p(V337) % 0.19/0.46 | p(V336) % 0.19/0.46 | p(V63) ) % 0.19/0.46 & ( p(V406) % 0.19/0.46 | -p(V101) ) % 0.19/0.46 & ( -p(V274) % 0.19/0.46 | -p(V39) ) % 0.19/0.46 & ( p(V313) % 0.19/0.46 | -p(V314) % 0.19/0.46 | p(V61) ) % 0.19/0.46 & ( -p(V27) % 0.19/0.46 | p(V183) ) % 0.19/0.46 & ( p(V317) % 0.19/0.46 | p(V61) ) % 0.19/0.46 & ( p(V309) % 0.19/0.46 | -p(V60) ) % 0.19/0.46 & ( -p(V172) % 0.19/0.46 | p(V16) ) % 0.19/0.46 & ( p(V10) % 0.19/0.46 | p(V9) % 0.19/0.46 | p(V184) % 0.19/0.46 | p(V8) ) % 0.19/0.46 & ( p(V91) % 0.19/0.46 | p(V92) % 0.19/0.46 | p(V93) % 0.19/0.46 | p(V445) ) % 0.19/0.46 & ( p(V308) % 0.19/0.46 | p(V51) ) % 0.19/0.46 & ( -p(V61) % 0.19/0.46 | p(V309) ) % 0.19/0.46 & ( -p(V55) % 0.19/0.46 | -p(V295) % 0.19/0.46 | -p(V54) ) % 0.19/0.46 & ( p(V432) % 0.19/0.46 | -p(V431) ) % 0.19/0.46 & ( p(V414) % 0.19/0.46 | p(V84) % 0.19/0.46 | p(V83) ) % 0.19/0.46 & ( p(V139) % 0.19/0.46 | -p(V364) % 0.19/0.46 | -p(V140) ) % 0.19/0.46 & ( p(V269) % 0.19/0.46 | p(V38) ) % 0.19/0.46 & ( p(V499) % 0.19/0.46 | -p(V123) ) % 0.19/0.46 & ( p(V206) % 0.19/0.46 | p(V26) ) % 0.19/0.46 & ( -p(V303) % 0.19/0.46 | p(V302) % 0.19/0.46 | -p(V52) ) % 0.19/0.46 & ( p(V363) % 0.19/0.46 | -p(V362) ) % 0.19/0.46 & ( -p(V116) % 0.19/0.46 | p(V480) ) % 0.19/0.46 & ( p(V145) % 0.19/0.46 | p(V448) ) % 0.19/0.46 & ( p(V314) % 0.19/0.46 | -p(V313) ) % 0.19/0.46 & ( -p(V504) % 0.19/0.46 | p(V487) ) % 0.19/0.46 & ( p(V383) % 0.19/0.46 | -p(V382) ) % 0.19/0.46 & ( -p(V240) % 0.19/0.46 | p(V237) ) % 0.19/0.46 & ( -p(V414) % 0.19/0.46 | p(V415) ) % 0.19/0.46 & ( p(V136) % 0.19/0.46 | p(V296) ) % 0.19/0.46 & ( -p(V145) % 0.19/0.46 | -p(V146) % 0.19/0.46 | -p(V454) ) % 0.19/0.46 & ( -p(V190) % 0.19/0.46 | -p(V9) ) % 0.19/0.46 & ( -p(V449) % 0.19/0.46 | p(V103) ) % 0.19/0.46 & ( p(V456) % 0.19/0.46 | -p(V508) ) % 0.19/0.46 & ( p(V526) % 0.19/0.46 | p(V180) % 0.19/0.46 | -p(V527) ) % 0.19/0.46 & ( -p(V346) % 0.19/0.46 | -p(V63) ) % 0.19/0.46 & ( -p(V491) % 0.19/0.46 | p(V493) ) % 0.19/0.46 & ( -p(V271) % 0.19/0.46 | -p(V39) ) % 0.19/0.46 & ( p(V363) % 0.19/0.46 | -p(V514) ) % 0.19/0.46 & ( -p(V358) % 0.19/0.46 | -p(V64) ) % 0.19/0.46 & ( p(V301) % 0.19/0.46 | -p(V62) ) % 0.19/0.46 & ( -p(V530) % 0.19/0.46 | p(V531) ) % 0.19/0.46 & ( p(V406) % 0.19/0.46 | -p(V95) ) % 0.19/0.46 & ( -p(V220) % 0.19/0.46 | p(V221) ) % 0.19/0.46 & ( -p(V381) % 0.19/0.46 | p(V382) ) % 0.19/0.46 & ( p(V101) % 0.19/0.46 | p(V412) % 0.19/0.46 | -p(V413) % 0.19/0.46 | p(V100) ) % 0.19/0.46 & ( p(V128) % 0.19/0.46 | p(V202) ) % 0.19/0.46 & ( -p(V343) % 0.19/0.46 | p(V344) ) % 0.19/0.46 & ( p(V151) % 0.19/0.46 | p(V497) ) % 0.19/0.46 & ( p(V129) % 0.19/0.46 | -p(V232) % 0.19/0.46 | -p(V130) ) % 0.19/0.46 & ( -p(V76) % 0.19/0.46 | p(V349) ) % 0.19/0.46 & ( p(V346) % 0.19/0.46 | p(V63) % 0.19/0.46 | p(V65) % 0.19/0.46 | p(V64) ) % 0.19/0.46 & ( -p(V159) % 0.19/0.46 | -p(V3) ) % 0.19/0.46 & ( -p(V168) % 0.19/0.46 | -p(V3) ) % 0.19/0.46 & ( p(V247) % 0.19/0.46 | -p(V45) ) % 0.19/0.46 & ( p(V221) % 0.19/0.46 | -p(V222) % 0.19/0.46 | p(V36) % 0.19/0.46 | p(V35) ) % 0.19/0.46 & ( -p(V33) % 0.19/0.46 | -p(V251) % 0.19/0.46 | p(V250) ) % 0.19/0.46 & ( -p(V83) % 0.19/0.46 | -p(V404) ) % 0.19/0.46 & ( -p(V14) % 0.19/0.46 | -p(V185) % 0.19/0.46 | p(V184) ) % 0.19/0.46 & ( p(V304) % 0.19/0.46 | -p(V57) ) % 0.19/0.46 & ( -p(V352) % 0.19/0.46 | -p(V63) ) % 0.19/0.46 & ( p(V312) % 0.19/0.46 | -p(V60) ) % 0.19/0.46 & ( -p(V409) % 0.19/0.46 | p(V407) ) % 0.19/0.46 & ( -p(V395) % 0.19/0.46 | -p(V141) % 0.19/0.46 | -p(V142) ) % 0.19/0.46 & ( p(V69) % 0.19/0.46 | -p(V328) ) % 0.19/0.46 & ( p(V242) % 0.19/0.46 | -p(V243) % 0.19/0.46 | p(V47) ) % 0.19/0.46 & ( p(V529) % 0.19/0.46 | -p(V158) ) % 0.19/0.46 & ( -p(V510) % 0.19/0.46 | p(V419) ) % 0.19/0.46 & ( p(V140) % 0.19/0.46 | p(V341) ) % 0.19/0.46 & ( p(V20) % 0.19/0.46 | p(V19) % 0.19/0.46 | p(V211) % 0.19/0.46 | p(V18) ) % 0.19/0.46 & ( -p(V518) % 0.19/0.46 | p(V312) ) % 0.19/0.46 & ( -p(V409) % 0.19/0.46 | p(V97) ) % 0.19/0.46 & ( -p(V512) % 0.19/0.46 | p(V383) ) % 0.19/0.46 & ( -p(V126) % 0.19/0.46 | -p(V171) % 0.19/0.46 | p(V125) ) % 0.19/0.46 & ( p(V390) % 0.19/0.46 | p(V391) % 0.19/0.46 | -p(V392) ) % 0.19/0.46 & ( -p(V400) % 0.19/0.46 | p(V511) ) % 0.19/0.46 & ( -p(V214) % 0.19/0.46 | -p(V20) ) % 0.19/0.46 & ( -p(V451) % 0.19/0.46 | -p(V146) % 0.19/0.46 | p(V145) ) % 0.19/0.46 & ( -p(V279) % 0.19/0.46 | -p(V39) ) % 0.19/0.46 & ( p(V144) % 0.19/0.46 | p(V399) ) % 0.19/0.46 & ( p(V122) % 0.19/0.46 | p(V501) ) % 0.19/0.46 & ( p(V8) % 0.19/0.46 | p(V10) % 0.19/0.46 | p(V9) % 0.19/0.46 | p(V193) ) % 0.19/0.46 & ( p(V177) % 0.19/0.46 | p(V127) ) % 0.19/0.46 & ( -p(V176) % 0.19/0.46 | -p(V17) % 0.19/0.46 | -p(V16) ) % 0.19/0.46 & ( -p(V530) % 0.19/0.46 | p(V529) ) % 0.19/0.46 & ( p(V424) % 0.19/0.46 | p(V146) ) % 0.19/0.46 & ( p(V319) % 0.19/0.46 | -p(V320) ) % 0.19/0.46 & ( -p(V297) % 0.19/0.46 | p(V298) % 0.19/0.46 | -p(V296) ) % 0.19/0.46 & ( -p(V112) % 0.19/0.46 | p(V465) % 0.19/0.46 | -p(V117) ) % 0.19/0.46 & ( p(V290) % 0.19/0.46 | -p(V520) ) % 0.19/0.46 & ( p(V501) % 0.19/0.46 | -p(V502) ) % 0.19/0.46 & ( -p(V528) % 0.19/0.46 | p(V167) ) % 0.19/0.46 & ( p(V491) % 0.19/0.46 | p(V492) % 0.19/0.46 | -p(V493) ) % 0.19/0.46 & ( p(V268) % 0.19/0.46 | p(V39) ) % 0.19/0.46 & ( -p(V310) % 0.19/0.46 | -p(V48) ) % 0.19/0.46 & ( p(V195) % 0.19/0.46 | -p(V194) ) % 0.19/0.46 & ( -p(V211) % 0.19/0.46 | -p(V18) ) % 0.19/0.46 & ( p(V416) % 0.19/0.46 | -p(V100) ) % 0.19/0.46 & ( p(V182) % 0.19/0.46 | p(V15) ) % 0.19/0.46 & ( -p(V520) % 0.19/0.46 | p(V292) ) % 0.19/0.46 & ( p(V65) % 0.19/0.46 | p(V339) ) % 0.19/0.46 & ( p(V186) % 0.19/0.46 | -p(V188) ) % 0.19/0.46 & ( -p(V13) % 0.19/0.46 | p(V172) % 0.19/0.46 | -p(V16) ) % 0.19/0.46 & ( -p(V154) % 0.19/0.46 | p(V5) ) % 0.19/0.46 & ( -p(V418) % 0.19/0.46 | p(V101) ) % 0.19/0.46 & ( p(V455) % 0.19/0.46 | -p(V454) ) % 0.19/0.46 & ( p(V312) % 0.19/0.46 | -p(V311) ) % 0.19/0.46 & ( -p(V53) % 0.19/0.46 | p(V281) ) % 0.19/0.46 & ( p(V169) % 0.19/0.46 | -p(V170) % 0.19/0.46 | p(V9) ) % 0.19/0.46 & ( -p(V268) % 0.19/0.46 | -p(V269) % 0.19/0.46 | -p(V267) % 0.19/0.46 | p(V270) ) % 0.19/0.46 & ( p(V154) % 0.19/0.46 | -p(V124) % 0.19/0.46 | -p(V155) ) % 0.19/0.46 & ( p(V255) % 0.19/0.46 | -p(V45) ) % 0.19/0.46 & ( -p(V64) % 0.19/0.46 | -p(V355) ) % 0.19/0.46 & ( p(V54) % 0.19/0.46 | p(V295) ) % 0.19/0.46 & ( p(V483) % 0.19/0.46 | p(V112) ) % 0.19/0.46 & ( -p(V372) % 0.19/0.46 | p(V371) ) % 0.19/0.46 & ( -p(V92) % 0.19/0.46 | -p(V436) ) % 0.19/0.46 & ( p(V395) % 0.19/0.46 | p(V142) ) % 0.19/0.46 & ( p(V294) % 0.19/0.46 | -p(V48) ) % 0.19/0.46 & ( p(V57) % 0.19/0.46 | p(V56) % 0.19/0.46 | p(V330) ) % 0.19/0.46 & ( -p(V90) % 0.19/0.46 | p(V375) ) % 0.19/0.46 & ( -p(V526) % 0.19/0.46 | p(V198) ) % 0.19/0.46 & ( -p(V133) % 0.19/0.46 | -p(V134) % 0.19/0.46 | -p(V293) ) % 0.19/0.46 & ( -p(V303) % 0.19/0.46 | p(V306) ) % 0.19/0.46 & ( -p(V96) % 0.19/0.46 | p(V439) % 0.19/0.46 | -p(V440) ) % 0.19/0.46 & ( -p(V323) % 0.19/0.46 | p(V72) % 0.19/0.46 | p(V322) ) % 0.19/0.46 & ( -p(V226) % 0.19/0.46 | -p(V18) ) % 0.19/0.46 & ( p(V396) % 0.19/0.46 | -p(V512) ) % 0.19/0.46 & ( -p(V358) % 0.19/0.46 | p(V359) ) % 0.19/0.46 & ( p(V407) % 0.19/0.46 | -p(V94) ) % 0.19/0.46 & ( p(V137) % 0.19/0.46 | p(V336) ) % 0.19/0.46 & ( -p(V528) % 0.19/0.46 | p(V527) ) % 0.19/0.46 & ( p(V422) % 0.19/0.46 | p(V102) ) % 0.19/0.46 & ( p(V252) % 0.19/0.46 | -p(V46) ) % 0.19/0.46 & ( p(V491) % 0.19/0.46 | p(V150) ) % 0.19/0.46 & ( -p(V249) % 0.19/0.46 | -p(V261) % 0.19/0.46 | -p(V252) % 0.19/0.46 | -p(V243) % 0.19/0.46 | p(V522) % 0.19/0.46 | -p(V266) % 0.19/0.46 | -p(V255) % 0.19/0.46 | -p(V521) % 0.19/0.46 | -p(V263) % 0.19/0.46 | -p(V265) % 0.19/0.46 | -p(V258) ) % 0.19/0.46 & ( -p(V401) % 0.19/0.46 | -p(V84) ) % 0.19/0.46 & ( -p(V282) % 0.19/0.46 | -p(V40) ) % 0.19/0.46 & ( -p(V30) % 0.19/0.46 | -p(V253) ) % 0.19/0.46 & ( -p(V158) % 0.19/0.46 | p(V157) ) % 0.19/0.46 & ( -p(V274) % 0.19/0.46 | -p(V38) ) % 0.19/0.46 & ( p(V315) % 0.19/0.46 | p(V135) ) % 0.19/0.46 & ( p(V92) % 0.19/0.46 | -p(V407) % 0.19/0.46 | p(V94) % 0.19/0.46 | p(V102) % 0.19/0.46 | p(V100) ) % 0.19/0.46 & ( p(V232) % 0.19/0.46 | -p(V129) ) % 0.19/0.46 & ( p(V416) % 0.19/0.46 | -p(V415) ) % 0.19/0.46 & ( -p(V223) % 0.19/0.46 | -p(V20) ) % 0.19/0.46 & ( -p(V387) % 0.19/0.46 | -p(V75) ) % 0.19/0.46 & ( p(V262) % 0.19/0.46 | p(V132) ) % 0.19/0.46 & ( p(V458) % 0.19/0.46 | -p(V459) ) % 0.19/0.46 & ( p(V284) % 0.19/0.46 | -p(V53) ) % 0.19/0.46 & ( p(V344) % 0.19/0.46 | p(V70) ) % 0.19/0.46 & ( -p(V82) % 0.19/0.46 | -p(V368) % 0.19/0.46 | -p(V81) ) % 0.19/0.46 & ( -p(V73) % 0.19/0.46 | -p(V387) ) % 0.19/0.46 & ( -p(V73) % 0.19/0.46 | -p(V381) ) % 0.19/0.46 & ( p(V303) % 0.19/0.46 | p(V52) ) % 0.19/0.46 & ( p(V377) % 0.19/0.46 | p(V379) % 0.19/0.46 | -p(V380) ) % 0.19/0.46 & ( -p(V84) % 0.19/0.46 | -p(V404) ) % 0.19/0.46 & ( p(V112) % 0.19/0.46 | -p(V465) ) % 0.19/0.46 & ( p(V495) % 0.19/0.46 | -p(V494) ) % 0.19/0.46 & ( p(V470) % 0.19/0.46 | p(V104) % 0.19/0.46 | p(V103) ) % 0.19/0.46 & ( p(V446) % 0.19/0.46 | -p(V445) ) % 0.19/0.46 & ( -p(V376) % 0.19/0.46 | -p(V74) ) % 0.19/0.46 & ( p(V39) % 0.19/0.46 | -p(V246) % 0.19/0.46 | p(V42) ) % 0.19/0.46 & ( p(V44) % 0.19/0.46 | p(V275) ) % 0.19/0.46 & ( p(V26) % 0.19/0.46 | p(V202) % 0.19/0.46 | -p(V203) ) % 0.19/0.46 & ( -p(V398) % 0.19/0.46 | -p(V399) % 0.19/0.46 | p(V400) ) % 0.19/0.46 & ( -p(V102) % 0.19/0.46 | -p(V101) % 0.19/0.46 | -p(V422) ) % 0.19/0.46 & ( -p(V9) % 0.19/0.46 | -p(V196) ) % 0.19/0.46 & ( p(V141) % 0.19/0.46 | p(V369) ) % 0.19/0.46 & ( p(V137) % 0.19/0.46 | p(V319) ) % 0.19/0.46 & ( -p(V31) % 0.19/0.46 | -p(V257) % 0.19/0.46 | p(V256) ) % 0.19/0.46 & ( p(V10) % 0.19/0.46 | p(V17) % 0.19/0.46 | -p(V165) % 0.19/0.46 | p(V11) % 0.19/0.46 | p(V15) ) % 0.19/0.46 & ( -p(V283) % 0.19/0.46 | p(V284) ) % 0.19/0.46 & ( p(V378) % 0.19/0.46 | -p(V85) ) % 0.19/0.46 & ( -p(V65) % 0.19/0.46 | -p(V358) ) % 0.19/0.46 & ( -p(V218) % 0.19/0.46 | p(V216) ) % 0.19/0.46 & ( -p(V131) % 0.19/0.46 | p(V238) ) % 0.19/0.46 & ( p(V294) % 0.19/0.46 | -p(V293) ) % 0.19/0.46 & ( -p(V52) % 0.19/0.46 | p(V277) % 0.19/0.46 | -p(V276) ) % 0.19/0.46 & ( p(V257) % 0.19/0.46 | p(V31) ) % 0.19/0.46 & ( -p(V452) % 0.19/0.46 | p(V453) ) % 0.19/0.46 & ( p(V90) % 0.19/0.46 | p(V397) ) % 0.19/0.46 & ( -p(V8) % 0.19/0.46 | -p(V184) ) % 0.19/0.46 & ( p(V408) % 0.19/0.46 | -p(V92) ) % 0.19/0.46 & ( -p(V19) % 0.19/0.46 | p(V186) ) % 0.19/0.46 & ( -p(V509) % 0.19/0.46 | -p(V403) % 0.19/0.46 | -p(V419) % 0.19/0.46 | -p(V410) % 0.19/0.46 | -p(V421) % 0.19/0.46 | -p(V413) % 0.19/0.46 | -p(V416) % 0.19/0.46 | p(V510) % 0.19/0.46 | -p(V422) ) % 0.19/0.46 & ( -p(V514) % 0.19/0.46 | p(V513) ) % 0.19/0.46 & ( -p(V39) % 0.19/0.46 | -p(V285) ) % 0.19/0.46 & ( p(V462) % 0.19/0.46 | -p(V461) ) % 0.19/0.46 & ( -p(V526) % 0.19/0.46 | p(V201) ) % 0.19/0.46 & ( -p(V14) % 0.19/0.46 | p(V166) % 0.19/0.46 | -p(V165) % 0.19/0.46 | -p(V164) ) % 0.19/0.46 & ( -p(V181) % 0.19/0.46 | -p(V9) ) % 0.19/0.46 & ( -p(V506) % 0.19/0.46 | p(V507) ) % 0.19/0.46 & ( -p(V526) % 0.19/0.46 | p(V195) ) % 0.19/0.46 & ( p(V87) % 0.19/0.46 | -p(V379) ) % 0.19/0.46 & ( p(V320) % 0.19/0.46 | -p(V319) % 0.19/0.46 | -p(V318) ) % 0.19/0.46 & ( p(V362) % 0.19/0.46 | -p(V78) % 0.19/0.46 | -p(V81) ) % 0.19/0.46 & ( p(V340) % 0.19/0.46 | p(V140) ) % 0.19/0.46 & ( p(V126) % 0.19/0.46 | p(V157) ) % 0.19/0.46 & ( -p(V141) % 0.19/0.46 | -p(V390) % 0.19/0.46 | p(V142) ) % 0.19/0.46 & ( -p(V180) % 0.19/0.46 | p(V177) ) % 0.19/0.46 & ( -p(V333) % 0.19/0.46 | p(V335) ) % 0.19/0.46 & ( -p(V411) % 0.19/0.46 | -p(V84) ) % 0.19/0.46 & ( p(V297) % 0.19/0.46 | p(V136) ) % 0.19/0.46 & ( p(V446) % 0.19/0.46 | p(V94) ) % 0.19/0.46 & ( -p(V418) % 0.19/0.46 | p(V91) ) % 0.19/0.46 & ( p(V28) % 0.19/0.46 | p(V239) ) % 0.19/0.46 & ( p(V165) % 0.19/0.46 | -p(V10) ) % 0.19/0.46 & ( p(V393) % 0.19/0.46 | p(V89) % 0.19/0.46 | -p(V394) ) % 0.19/0.46 & ( p(V511) % 0.19/0.46 | -p(V512) ) % 0.19/0.46 & ( p(V73) % 0.19/0.46 | p(V384) % 0.19/0.46 | p(V74) % 0.19/0.46 | p(V75) ) % 0.19/0.46 & ( -p(V526) % 0.19/0.46 | p(V525) ) % 0.19/0.46 & ( p(V503) % 0.19/0.46 | -p(V497) ) % 0.19/0.46 & ( p(V340) % 0.19/0.46 | -p(V139) ) % 0.19/0.46 & ( -p(V300) % 0.19/0.46 | p(V301) ) % 0.19/0.46 & ( p(V265) % 0.19/0.46 | -p(V38) ) % 0.19/0.46 & ( p(V83) % 0.19/0.46 | p(V399) ) % 0.19/0.46 & ( -p(V135) % 0.19/0.46 | p(V296) ) % 0.19/0.46 & ( p(V401) % 0.19/0.46 | -p(V402) % 0.19/0.46 | -p(V88) ) % 0.19/0.46 & ( -p(V478) % 0.19/0.46 | p(V477) % 0.19/0.46 | p(V476) ) % 0.19/0.46 & ( -p(V508) % 0.19/0.46 | p(V444) ) % 0.19/0.46 & ( p(V185) % 0.19/0.46 | p(V188) % 0.19/0.46 | -p(V189) ) % 0.19/0.46 & ( p(V380) % 0.19/0.46 | -p(V377) ) % 0.19/0.46 & ( p(V139) % 0.19/0.46 | -p(V140) % 0.19/0.46 | -p(V64) % 0.19/0.46 | -p(V340) ) % 0.19/0.46 & ( -p(V64) % 0.19/0.46 | -p(V346) ) % 0.19/0.46 & ( p(V152) % 0.19/0.46 | p(V530) % 0.19/0.46 | -p(V531) ) % 0.19/0.46 & ( p(V317) % 0.19/0.46 | -p(V518) ) % 0.19/0.46 & ( p(V71) % 0.19/0.46 | p(V338) ) % 0.19/0.46 & ( p(V529) % 0.19/0.46 | -p(V528) ) % 0.19/0.46 & ( -p(V298) % 0.19/0.46 | p(V519) ) % 0.19/0.46 & ( p(V84) % 0.19/0.46 | p(V401) % 0.19/0.46 | p(V83) ) % 0.19/0.46 & ( -p(V25) % 0.19/0.46 | p(V192) ) % 0.19/0.46 & ( -p(V59) % 0.19/0.46 | -p(V325) % 0.19/0.46 | p(V324) ) % 0.19/0.46 & ( p(V278) % 0.19/0.46 | -p(V277) ) % 0.19/0.46 & ( -p(V71) % 0.19/0.46 | -p(V68) % 0.19/0.46 | p(V334) ) % 0.19/0.46 & ( -p(V188) % 0.19/0.46 | p(V24) ) % 0.19/0.46 & ( -p(V467) % 0.19/0.46 | -p(V104) ) % 0.19/0.46 & ( -p(V282) % 0.19/0.46 | -p(V39) ) % 0.19/0.46 & ( -p(V190) % 0.19/0.46 | -p(V8) ) % 0.19/0.46 & ( -p(V307) % 0.19/0.46 | -p(V49) ) % 0.19/0.46 & ( -p(V117) % 0.19/0.46 | -p(V481) % 0.19/0.46 | -p(V116) ) % 0.19/0.46 & ( p(V138) % 0.19/0.46 | p(V318) ) % 0.19/0.46 & ( p(V375) % 0.19/0.46 | -p(V512) ) % 0.19/0.46 & ( -p(V111) % 0.19/0.46 | p(V435) ) % 0.19/0.46 & ( -p(V306) % 0.19/0.46 | p(V303) % 0.19/0.46 | p(V305) ) % 0.19/0.46 & ( p(V318) % 0.19/0.46 | -p(V320) ) % 0.19/0.46 & ( p(V441) % 0.19/0.46 | -p(V440) ) % 0.19/0.46 & ( p(V387) % 0.19/0.46 | -p(V388) % 0.19/0.46 | -p(V76) ) % 0.19/0.46 & ( p(V261) % 0.19/0.46 | -p(V522) ) % 0.19/0.46 & ( p(V468) % 0.19/0.46 | -p(V467) ) % 0.19/0.46 & ( -p(V496) % 0.19/0.46 | -p(V120) % 0.19/0.46 | -p(V121) ) % 0.19/0.46 & ( -p(V251) % 0.19/0.46 | p(V252) ) % 0.19/0.46 & ( -p(V162) % 0.19/0.46 | -p(V3) ) % 0.19/0.46 & ( p(V505) % 0.19/0.46 | -p(V484) ) % 0.19/0.46 & ( -p(V518) % 0.19/0.46 | p(V519) ) % 0.19/0.46 & ( p(V382) % 0.19/0.46 | p(V78) ) % 0.19/0.46 & ( p(V392) % 0.19/0.46 | -p(V390) ) % 0.19/0.46 & ( -p(V508) % 0.19/0.46 | p(V455) ) % 0.19/0.46 & ( p(V76) % 0.19/0.46 | p(V388) ) % 0.19/0.46 & ( -p(V391) % 0.19/0.46 | p(V89) ) % 0.19/0.46 & ( -p(V101) % 0.19/0.46 | p(V413) ) % 0.19/0.46 & ( -p(V524) % 0.19/0.46 | p(V213) ) % 0.19/0.46 & ( -p(V474) % 0.19/0.46 | p(V475) ) % 0.19/0.46 & ( -p(V520) % 0.19/0.46 | p(V519) ) % 0.19/0.46 & ( -p(V130) % 0.19/0.46 | -p(V18) % 0.19/0.46 | -p(V209) % 0.19/0.46 | -p(V129) ) % 0.19/0.46 & ( p(V406) % 0.19/0.46 | -p(V93) ) % 0.19/0.46 & ( -p(V444) % 0.19/0.46 | p(V443) % 0.19/0.46 | p(V104) ) % 0.19/0.46 & ( p(V179) % 0.19/0.46 | -p(V180) ) % 0.19/0.46 & ( p(V117) % 0.19/0.46 | p(V481) ) % 0.19/0.46 & ( -p(V19) % 0.19/0.46 | -p(V220) ) % 0.19/0.46 & ( p(V138) % 0.19/0.46 | p(V333) ) % 0.19/0.46 & ( p(V194) % 0.19/0.46 | -p(V193) ) % 0.19/0.46 & ( p(V425) % 0.19/0.46 | p(V91) ) % 0.19/0.46 & ( p(V463) % 0.19/0.46 | p(V104) % 0.19/0.46 | p(V103) ) % 0.19/0.46 & ( p(V84) % 0.19/0.46 | p(V404) % 0.19/0.46 | p(V83) ) % 0.19/0.46 & ( p(V227) % 0.19/0.46 | -p(V226) ) % 0.19/0.46 & ( p(V353) % 0.19/0.46 | p(V68) ) % 0.19/0.46 & ( p(V397) % 0.19/0.46 | p(V89) ) % 0.19/0.46 & ( p(V349) % 0.19/0.46 | -p(V80) ) % 0.19/0.46 & ( p(V159) % 0.19/0.46 | -p(V160) % 0.19/0.46 | -p(V6) ) % 0.19/0.46 & ( p(V479) % 0.19/0.46 | p(V147) ) % 0.19/0.46 & ( -p(V433) % 0.19/0.46 | p(V434) ) % 0.19/0.46 & ( -p(V270) % 0.19/0.46 | p(V267) ) % 0.19/0.46 & ( p(V33) % 0.19/0.46 | -p(V230) ) % 0.19/0.46 & ( -p(V128) % 0.19/0.46 | p(V127) % 0.19/0.46 | -p(V202) ) % 0.19/0.46 & ( p(V304) % 0.19/0.46 | -p(V62) ) % 0.19/0.46 & ( p(V458) % 0.19/0.46 | p(V147) ) % 0.19/0.46 & ( -p(V524) % 0.19/0.46 | p(V225) ) % 0.19/0.46 & ( p(V329) % 0.19/0.46 | -p(V328) ) % 0.19/0.46 & ( p(V507) % 0.19/0.46 | -p(V459) ) % 0.19/0.46 & ( -p(V115) % 0.19/0.46 | p(V475) ) % 0.19/0.46 & ( p(V126) % 0.19/0.46 | p(V156) ) % 0.19/0.46 & ( p(V428) % 0.19/0.46 | p(V100) ) % 0.19/0.46 & ( p(V105) % 0.19/0.46 | p(V103) % 0.19/0.46 | p(V437) % 0.19/0.46 | -p(V438) ) % 0.19/0.46 & ( -p(V424) % 0.19/0.46 | p(V145) % 0.19/0.46 | -p(V146) % 0.19/0.46 | -p(V92) ) % 0.19/0.46 & ( -p(V522) % 0.19/0.46 | p(V249) ) % 0.19/0.46 & ( p(V170) % 0.19/0.46 | -p(V528) ) % 0.19/0.46 & ( -p(V19) % 0.19/0.46 | -p(V208) % 0.19/0.46 | p(V129) % 0.19/0.46 | -p(V130) ) % 0.19/0.46 & ( p(V368) % 0.19/0.46 | -p(V514) ) % 0.19/0.46 & ( -p(V305) % 0.19/0.46 | p(V59) ) % 0.19/0.46 & ( p(V36) % 0.19/0.46 | -p(V233) % 0.19/0.46 | p(V232) ) % 0.19/0.46 & ( p(V493) % 0.19/0.46 | -p(V504) ) % 0.19/0.46 & ( p(V106) % 0.19/0.46 | -p(V441) % 0.19/0.46 | p(V440) ) % 0.19/0.46 & ( p(V461) % 0.19/0.46 | -p(V460) ) % 0.19/0.46 & ( p(V378) % 0.19/0.46 | -p(V83) ) % 0.19/0.46 & ( p(V338) % 0.19/0.46 | p(V72) ) % 0.19/0.46 & ( p(V150) % 0.19/0.46 | p(V483) ) % 0.19/0.46 & ( p(V58) % 0.19/0.46 | p(V331) ) % 0.19/0.46 & ( -p(V88) % 0.19/0.46 | p(V383) ) % 0.19/0.46 & ( p(V447) % 0.19/0.46 | -p(V508) ) % 0.19/0.46 & ( -p(V40) % 0.19/0.46 | -p(V279) ) % 0.19/0.46 & ( p(V352) % 0.19/0.46 | -p(V68) % 0.19/0.46 | -p(V353) ) % 0.19/0.46 & ( p(V494) % 0.19/0.46 | p(V120) % 0.19/0.46 | -p(V495) ) % 0.19/0.46 & ( -p(V452) % 0.19/0.46 | p(V110) ) % 0.19/0.46 & ( -p(V11) % 0.19/0.46 | p(V165) ) % 0.19/0.46 & ( -p(V442) % 0.19/0.46 | -p(V91) ) % 0.19/0.46 & ( -p(V530) % 0.19/0.46 | p(V155) ) % 0.19/0.46 & ( -p(V524) % 0.19/0.46 | p(V231) ) % 0.19/0.46 & ( p(V127) % 0.19/0.46 | p(V204) ) % 0.19/0.46 & ( -p(V343) % 0.19/0.46 | -p(V64) ) % 0.19/0.46 & ( p(V234) % 0.19/0.46 | p(V129) ) % 0.19/0.46 & ( p(V231) % 0.19/0.46 | -p(V229) ) % 0.19/0.46 & ( p(V121) % 0.19/0.46 | -p(V492) ) % 0.19/0.46 & ( p(V482) % 0.19/0.46 | p(V113) ) % 0.19/0.46 & ( -p(V212) % 0.19/0.46 | p(V211) % 0.19/0.46 | -p(V25) ) % 0.19/0.46 & ( -p(V439) % 0.19/0.46 | p(V440) ) % 0.19/0.46 & ( -p(V103) % 0.19/0.46 | -p(V460) ) % 0.19/0.46 & ( p(V265) % 0.19/0.46 | -p(V522) ) % 0.19/0.46 & ( p(V192) % 0.19/0.46 | -p(V526) ) % 0.19/0.46 & ( -p(V350) % 0.19/0.46 | p(V79) ) % 0.19/0.46 & ( -p(V380) % 0.19/0.46 | -p(V386) % 0.19/0.46 | -p(V375) % 0.19/0.46 | -p(V394) % 0.19/0.46 | -p(V511) % 0.19/0.46 | -p(V396) % 0.19/0.46 | -p(V383) % 0.19/0.46 | -p(V397) % 0.19/0.46 | -p(V389) % 0.19/0.46 | p(V512) % 0.19/0.46 | -p(V392) ) % 0.19/0.46 & ( p(V424) % 0.19/0.46 | -p(V145) ) % 0.19/0.46 & ( -p(V506) % 0.19/0.46 | p(V478) ) % 0.19/0.46 & ( p(V373) % 0.19/0.46 | -p(V374) % 0.19/0.46 | -p(V80) ) % 0.19/0.46 & ( -p(V488) % 0.19/0.46 | p(V489) ) % 0.19/0.46 & ( p(V297) % 0.19/0.46 | -p(V298) ) % 0.19/0.46 & ( -p(V468) % 0.19/0.46 | p(V467) % 0.19/0.46 | -p(V107) ) % 0.19/0.46 & ( p(V394) % 0.19/0.46 | -p(V393) ) % 0.19/0.46 & ( -p(V245) % 0.19/0.46 | p(V249) ) % 0.19/0.46 & ( p(V390) % 0.19/0.46 | p(V141) ) % 0.19/0.46 & ( p(V422) % 0.19/0.46 | p(V101) ) % 0.19/0.46 & ( p(V178) % 0.19/0.46 | -p(V127) ) % 0.19/0.46 & ( p(V475) % 0.19/0.46 | -p(V506) ) % 0.19/0.46 & ( -p(V17) % 0.19/0.46 | p(V161) ) % 0.19/0.46 & ( p(V19) % 0.19/0.46 | p(V18) % 0.19/0.46 | p(V20) % 0.19/0.46 | p(V220) ) % 0.19/0.46 & ( p(V142) % 0.19/0.46 | p(V370) ) % 0.19/0.46 & ( p(V66) % 0.19/0.46 | p(V359) ) % 0.19/0.46 & ( p(V12) % 0.19/0.46 | p(V194) ) % 0.19/0.46 & ( -p(V373) % 0.19/0.46 | -p(V73) ) % 0.19/0.46 & ( -p(V28) % 0.19/0.46 | -p(V131) % 0.19/0.46 | -p(V132) % 0.19/0.46 | -p(V239) ) % 0.19/0.46 & ( -p(V474) % 0.19/0.46 | -p(V105) % 0.19/0.46 | p(V473) ) % 0.19/0.46 & ( p(V504) % 0.19/0.46 | -p(V505) % 0.19/0.46 | p(V484) ) % 0.19/0.46 & ( -p(V10) % 0.19/0.46 | -p(V196) ) % 0.19/0.46 & ( p(V254) % 0.19/0.46 | p(V32) ) % 0.19/0.46 & ( p(V483) % 0.19/0.46 | -p(V484) ) % 0.19/0.46 & ( p(V332) % 0.19/0.46 | -p(V516) ) % 0.19/0.46 & ( p(V301) % 0.19/0.46 | -p(V518) ) % 0.19/0.46 & ( p(V249) % 0.19/0.46 | -p(V248) ) % 0.19/0.46 & ( -p(V476) % 0.19/0.46 | -p(V148) % 0.19/0.46 | p(V147) ) % 0.19/0.46 & ( p(V30) % 0.19/0.46 | p(V28) % 0.19/0.46 | p(V244) % 0.19/0.46 | p(V29) ) % 0.19/0.46 & ( -p(V169) % 0.19/0.46 | p(V168) % 0.19/0.46 | -p(V4) ) % 0.19/0.46 & ( -p(V467) % 0.19/0.46 | -p(V103) ) % 0.19/0.46 & ( -p(V73) % 0.19/0.46 | -p(V384) ) % 0.19/0.46 & ( -p(V154) % 0.19/0.46 | p(V155) ) % 0.19/0.46 & ( -p(V89) % 0.19/0.46 | p(V383) ) % 0.19/0.46 & ( p(V443) % 0.19/0.46 | -p(V442) ) % 0.19/0.46 & ( -p(V63) % 0.19/0.46 | p(V337) ) % 0.19/0.46 & ( -p(V33) % 0.19/0.46 | -p(V36) % 0.19/0.46 | p(V230) ) % 0.19/0.46 & ( p(V50) % 0.19/0.46 | p(V311) ) % 0.19/0.46 & ( -p(V501) % 0.19/0.46 | p(V502) % 0.19/0.46 | -p(V500) % 0.19/0.46 | -p(V499) ) % 0.19/0.46 & ( -p(V220) % 0.19/0.46 | -p(V18) ) % 0.19/0.46 & ( -p(V141) % 0.19/0.46 | p(V370) ) % 0.19/0.46 & ( p(V310) % 0.19/0.46 | -p(V311) % 0.19/0.46 | -p(V50) ) % 0.19/0.46 & ( -p(V173) % 0.19/0.46 | p(V171) % 0.19/0.46 | p(V172) ) % 0.19/0.46 & ( p(V187) % 0.19/0.46 | -p(V25) ) % 0.19/0.46 & ( -p(V49) % 0.19/0.46 | p(V287) ) % 0.19/0.46 & ( -p(V30) % 0.19/0.46 | -p(V244) ) % 0.19/0.46 & ( -p(V23) % 0.19/0.46 | p(V220) % 0.19/0.46 | -p(V221) ) % 0.19/0.46 & ( -p(V514) % 0.19/0.46 | p(V345) ) % 0.19/0.46 & ( p(V327) % 0.19/0.46 | -p(V65) ) % 0.19/0.46 & ( p(V18) % 0.19/0.46 | -p(V205) % 0.19/0.46 | p(V204) ) % 0.19/0.46 & ( -p(V346) % 0.19/0.46 | -p(V65) ) % 0.19/0.46 & ( p(V245) % 0.19/0.46 | p(V248) % 0.19/0.46 | -p(V249) ) % 0.19/0.46 & ( p(V36) % 0.19/0.46 | -p(V230) ) % 0.19/0.46 & ( p(V115) % 0.19/0.46 | p(V486) ) % 0.19/0.46 & ( p(V286) % 0.19/0.46 | -p(V285) ) % 0.19/0.46 & ( -p(V514) % 0.19/0.46 | p(V365) ) % 0.19/0.46 & ( p(V49) % 0.19/0.46 | p(V296) ) % 0.19/0.46 & ( p(V444) % 0.19/0.46 | -p(V104) ) % 0.19/0.46 & ( -p(V510) % 0.19/0.46 | p(V509) ) % 0.19/0.46 & ( p(V234) % 0.19/0.46 | p(V130) ) % 0.19/0.46 & ( p(V221) % 0.19/0.46 | p(V23) ) % 0.19/0.46 & ( p(V396) % 0.19/0.46 | -p(V84) ) % 0.19/0.46 & ( -p(V442) % 0.19/0.46 | -p(V93) ) % 0.19/0.46 & ( p(V78) % 0.19/0.46 | -p(V362) ) % 0.19/0.46 & ( p(V472) % 0.19/0.46 | -p(V113) ) % 0.19/0.46 & ( -p(V396) % 0.19/0.46 | p(V84) % 0.19/0.46 | p(V395) ) % 0.19/0.46 & ( -p(V142) % 0.19/0.46 | -p(V74) % 0.19/0.46 | p(V141) % 0.19/0.46 | -p(V370) ) % 0.19/0.46 & ( -p(V226) % 0.19/0.46 | -p(V19) ) % 0.19/0.46 & ( p(V464) % 0.19/0.46 | -p(V463) ) % 0.19/0.46 & ( -p(V37) % 0.19/0.46 | -p(V36) % 0.19/0.46 | -p(V236) ) % 0.19/0.46 & ( p(V246) % 0.19/0.46 | -p(V42) ) % 0.19/0.46 & ( p(V32) % 0.19/0.46 | -p(V216) % 0.19/0.46 | p(V29) ) % 0.19/0.46 & ( -p(V57) % 0.19/0.46 | p(V137) % 0.19/0.46 | -p(V318) % 0.19/0.46 | -p(V138) ) % 0.19/0.46 & ( -p(V402) % 0.19/0.46 | p(V403) ) % 0.19/0.46 & ( p(V139) % 0.19/0.46 | p(V366) ) % 0.19/0.46 & ( -p(V389) % 0.19/0.46 | p(V83) % 0.19/0.46 | p(V388) ) % 0.19/0.46 & ( -p(V346) % 0.19/0.46 | p(V347) ) % 0.19/0.46 & ( p(V247) % 0.19/0.46 | -p(V41) ) % 0.19/0.46 & ( p(V299) % 0.19/0.46 | -p(V300) % 0.19/0.46 | -p(V53) ) % 0.19/0.46 & ( p(V224) % 0.19/0.46 | p(V22) ) % 0.19/0.46 & ( p(V290) % 0.19/0.46 | -p(V289) ) % 0.19/0.46 & ( p(V205) % 0.19/0.46 | -p(V18) ) % 0.19/0.46 & ( p(V48) % 0.19/0.46 | p(V49) % 0.19/0.46 | p(V307) ) % 0.19/0.46 & ( p(V326) % 0.19/0.46 | -p(V64) ) % 0.19/0.46 & ( p(V25) % 0.19/0.46 | -p(V195) % 0.19/0.46 | p(V194) ) % 0.19/0.46 & ( p(V134) % 0.19/0.46 | p(V269) ) % 0.19/0.46 & ( -p(V325) % 0.19/0.46 | p(V329) ) % 0.19/0.46 & ( p(V145) % 0.19/0.46 | p(V454) ) % 0.19/0.46 & ( p(V86) % 0.19/0.46 | -p(V391) ) % 0.19/0.46 & ( p(V388) % 0.19/0.46 | -p(V387) ) % 0.19/0.46 & ( p(V146) % 0.19/0.46 | p(V454) ) % 0.19/0.46 & ( p(V272) % 0.19/0.46 | p(V45) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ). % 0.19/0.46 % 0.19/0.46 ======= end of input processing ======= % 0.19/0.46 % 0.19/0.46 1 input errors were found. % 0.19/0.46 % 0.19/0.46 1 input errors were found. %------------------------------------------------------------------------------