%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : SYO591+1 : TPTP v8.1.0. Bugfixed v5.5.1. % Transfm : none % Format : tptp:raw % Command : sos-script %s % Computer : n029.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:47 EDT 2022 % Result : Unknown 0.18s 0.43s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYO591+1 : TPTP v8.1.0. Bugfixed v5.5.1. % 0.11/0.12 % Command : sos-script %s % 0.12/0.33 % Computer : n029.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 09:17:00 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.42 ----- Otter 3.2, August 2001 ----- % 0.18/0.42 The process was started by sandbox2 on n029.cluster.edu, % 0.18/0.42 Sat Jul 9 09:17:00 2022 % 0.18/0.42 The command was "./sos". The process ID is 29721. % 0.18/0.42 % 0.18/0.42 set(prolog_style_variables). % 0.18/0.42 set(auto). % 0.18/0.42 dependent: set(auto1). % 0.18/0.42 dependent: set(process_input). % 0.18/0.42 dependent: clear(print_kept). % 0.18/0.42 dependent: clear(print_new_demod). % 0.18/0.42 dependent: clear(print_back_demod). % 0.18/0.42 dependent: clear(print_back_sub). % 0.18/0.42 dependent: set(control_memory). % 0.18/0.42 dependent: assign(max_mem, 12000). % 0.18/0.42 dependent: assign(pick_given_ratio, 4). % 0.18/0.42 dependent: assign(stats_level, 1). % 0.18/0.42 dependent: assign(pick_semantic_ratio, 3). % 0.18/0.42 dependent: assign(sos_limit, 5000). % 0.18/0.42 dependent: assign(max_weight, 60). % 0.18/0.42 clear(print_given). % 0.18/0.42 % 0.18/0.42 formula_list(usable). % 0.18/0.42 % 0.18/0.42 ERROR, term too big: % 0.18/0.42 % 0.18/0.42 % 0.18/0.42 ( exists V395 V1 V394 ( % 0.18/0.42 ( all V94 ( % 0.18/0.42 ( exists V117 V393 V3 V2 V119 V392 ( % 0.18/0.42 ( all V95 ( % 0.18/0.42 ( exists V120 V391 V14 V13 V12 V11 V10 V9 V8 V7 V6 V5 V4 V121 V128 V129 V390 ( % 0.18/0.42 ( all V96 V97 V98 ( % 0.18/0.42 ( exists V134 V389 V28 V27 V26 V25 V24 V23 V22 V21 V20 V19 V18 V17 V16 V15 V142 V145 V148 V151 V154 V156 V158 V160 V161 V388 ( % 0.18/0.42 ( all V99 V100 V101 ( % 0.18/0.42 ( exists V167 V387 V42 V41 V40 V39 V38 V37 V36 V35 V34 V33 V32 V31 V30 V29 V170 V178 V181 V184 V187 V190 V193 V195 V197 V199 V201 V202 V386 ( % 0.18/0.42 ( all V102 V103 V104 ( % 0.18/0.42 ( exists V208 V385 V56 V55 V54 V53 V52 V51 V50 V49 V48 V47 V46 V45 V44 V43 V211 V219 V222 V225 V228 V231 V234 V236 V238 V240 V242 V243 V384 ( % 0.18/0.42 ( all V105 V106 V107 ( % 0.18/0.42 ( exists V249 V383 V70 V69 V68 V67 V66 V65 V64 V63 V62 V61 V60 V59 V58 V57 V252 V260 V263 V266 V269 V272 V275 V277 V279 V281 V283 V284 V382 ( % 0.18/0.42 ( all V108 V109 V110 ( % 0.18/0.42 ( exists V290 V381 V82 V81 V80 V79 V78 V77 V76 V75 V74 V73 V72 V71 V293 V301 V304 V307 V310 V313 V316 V318 V321 V323 V325 V326 V380 ( % 0.18/0.42 ( all V111 V112 V113 ( % 0.18/0.42 ( exists V331 V379 V89 V88 V87 V86 V85 V84 V83 V334 V337 V340 V343 V346 V349 V351 V353 V355 V356 V378 ( % 0.18/0.42 ( all V114 V115 ( % 0.18/0.42 ( exists V359 V377 V92 V91 V90 V362 V365 V368 V370 V372 V373 V376 ( % 0.18/0.42 ( all V116 ( % 0.18/0.42 ( exists V374 V375 V93 V371 V369 V367 V366 V364 V363 V361 V360 V357 V358 V354 V352 V350 V348 V347 V345 V344 V342 V341 V339 V338 V336 V335 V333 V332 V327 V328 V329 V330 V324 V322 V319 V320 V317 V315 V314 V312 V311 V309 V308 V306 V305 V303 V302 V295 V300 V296 V297 V298 V299 V294 V292 V291 V285 V286 V287 V288 V289 V282 V280 V278 V276 V274 V273 V271 V270 V268 V267 V265 V264 V262 V261 V254 V259 V255 V256 V257 V258 V253 V251 V250 V244 V245 V246 V247 V248 V241 V239 V237 V235 V233 V232 V230 V229 V227 V226 V224 V223 V221 V220 V213 V218 V214 V215 V216 V217 V212 V210 V209 V203 V204 V205 V206 V207 V200 V198 V196 V194 V192 V191 V189 V188 V186 V185 V183 V182 V180 V179 V172 V177 V173 V174 V175 V176 V171 V169 V168 V162 V163 V164 V165 V166 V159 V157 V155 V153 V152 V150 V149 V147 V146 V144 V143 V136 V141 V137 V138 V139 V140 V135 V130 V131 V132 V133 V122 V127 V123 V124 V125 V126 V118 ( % 0.18/0.42 ( p(true) % 0.18/0.42 & -p(false) % 0.18/0.42 & ( -p(V135) % 0.18/0.42 | p(V136) ) % 0.18/0.42 & ( p(V175) % 0.18/0.42 | -p(V36) ) % 0.18/0.42 & ( -p(V47) % 0.18/0.42 | -p(V270) ) % 0.18/0.42 & ( -p(V130) % 0.18/0.42 | p(V134) % 0.18/0.42 | -p(V133) % 0.18/0.42 | -p(V132) % 0.18/0.42 | -p(V131) ) % 0.18/0.42 & ( p(V354) % 0.18/0.42 | p(V113) ) % 0.18/0.42 & ( p(V215) % 0.18/0.42 | -p(V55) ) % 0.18/0.42 & ( p(V274) % 0.18/0.42 | p(V58) % 0.18/0.42 | -p(V275) ) % 0.18/0.42 & ( p(V374) % 0.18/0.42 | p(V116) ) % 0.18/0.42 & ( -p(V149) % 0.18/0.42 | -p(V7) ) % 0.18/0.42 & ( -p(V109) % 0.18/0.42 | -p(V108) % 0.18/0.42 | -p(V324) % 0.18/0.42 | -p(V110) ) % 0.18/0.42 & ( -p(V381) % 0.18/0.42 | p(V326) ) % 0.18/0.42 & ( p(V349) % 0.18/0.42 | -p(V348) ) % 0.18/0.42 & ( p(V41) % 0.18/0.42 | -p(V197) % 0.18/0.42 | p(V196) ) % 0.18/0.42 & ( -p(V395) % 0.18/0.42 | p(V394) ) % 0.18/0.42 & ( p(V249) % 0.18/0.42 | p(V383) % 0.18/0.42 | -p(V384) ) % 0.18/0.42 & ( -p(V381) % 0.18/0.42 | p(V321) ) % 0.18/0.42 & ( p(V84) % 0.18/0.42 | p(V83) % 0.18/0.42 | p(V360) ) % 0.18/0.42 & ( p(V373) % 0.18/0.42 | -p(V377) ) % 0.18/0.42 & ( -p(V259) % 0.18/0.42 | p(V257) ) % 0.18/0.42 & ( -p(V70) % 0.18/0.42 | p(V277) ) % 0.18/0.42 & ( p(V246) % 0.18/0.42 | -p(V106) ) % 0.18/0.42 & ( p(V74) % 0.18/0.42 | -p(V300) ) % 0.18/0.42 & ( -p(V385) % 0.18/0.42 | p(V211) ) % 0.18/0.42 & ( p(V244) % 0.18/0.42 | p(V105) ) % 0.18/0.42 & ( -p(V41) % 0.18/0.42 | p(V197) ) % 0.18/0.42 & ( p(V98) % 0.18/0.42 | p(V157) ) % 0.18/0.42 & ( p(V240) % 0.18/0.42 | -p(V239) ) % 0.18/0.42 & ( -p(V306) % 0.18/0.42 | p(V307) ) % 0.18/0.42 & ( p(V356) % 0.18/0.42 | -p(V379) ) % 0.18/0.42 & ( -p(V325) % 0.18/0.42 | p(V79) % 0.18/0.42 | p(V324) ) % 0.18/0.42 & ( -p(V16) % 0.18/0.42 | -p(V191) ) % 0.18/0.42 & ( p(V319) % 0.18/0.42 | p(V110) ) % 0.18/0.42 & ( p(V237) % 0.18/0.42 | p(V55) % 0.18/0.42 | -p(V238) ) % 0.18/0.42 & ( p(V245) % 0.18/0.42 | p(V107) ) % 0.18/0.42 & ( p(V102) % 0.18/0.42 | p(V203) ) % 0.18/0.42 & ( -p(V135) % 0.18/0.42 | -p(V5) ) % 0.18/0.42 & ( -p(V256) % 0.18/0.42 | -p(V67) % 0.18/0.42 | -p(V257) % 0.18/0.42 | p(V259) % 0.18/0.42 | -p(V61) % 0.18/0.42 | -p(V258) % 0.18/0.42 | -p(V255) ) % 0.18/0.42 & ( -p(V45) % 0.18/0.42 | -p(V273) ) % 0.18/0.42 & ( p(V161) % 0.18/0.42 | p(V27) ) % 0.18/0.42 & ( -p(V177) % 0.18/0.42 | p(V176) ) % 0.18/0.42 & ( p(V134) % 0.18/0.42 | p(V389) % 0.18/0.42 | -p(V390) ) % 0.18/0.42 & ( p(V266) % 0.18/0.42 | -p(V68) ) % 0.18/0.42 & ( p(V342) % 0.18/0.42 | -p(V341) ) % 0.18/0.42 & ( -p(V329) % 0.18/0.42 | -p(V72) % 0.18/0.42 | p(V111) % 0.18/0.42 | -p(V112) % 0.18/0.42 | -p(V113) ) % 0.18/0.42 & ( p(V312) % 0.18/0.42 | p(V63) ) % 0.18/0.42 & ( -p(V6) % 0.18/0.42 | -p(V152) ) % 0.18/0.42 & ( p(V142) % 0.18/0.42 | -p(V136) ) % 0.18/0.42 & ( -p(V292) % 0.18/0.42 | p(V293) ) % 0.18/0.42 & ( -p(V311) % 0.18/0.42 | -p(V61) ) % 0.18/0.42 & ( -p(V19) % 0.18/0.42 | -p(V171) ) % 0.18/0.42 & ( p(V357) % 0.18/0.42 | -p(V359) ) % 0.18/0.42 & ( -p(V6) % 0.18/0.42 | -p(V149) ) % 0.18/0.42 & ( p(V382) % 0.18/0.42 | -p(V290) ) % 0.18/0.42 & ( p(V122) % 0.18/0.42 | p(V2) ) % 0.18/0.42 & ( p(V205) % 0.18/0.42 | -p(V208) ) % 0.18/0.42 & ( p(V28) % 0.18/0.42 | p(V161) ) % 0.18/0.42 & ( p(V126) % 0.18/0.42 | -p(V127) ) % 0.18/0.42 & ( -p(V142) % 0.18/0.42 | p(V136) % 0.18/0.42 | p(V141) ) % 0.18/0.42 & ( p(V319) % 0.18/0.42 | p(V108) ) % 0.18/0.42 & ( p(V186) % 0.18/0.42 | p(V35) % 0.18/0.42 | -p(V187) ) % 0.18/0.42 & ( -p(V385) % 0.18/0.42 | p(V386) ) % 0.18/0.42 & ( p(V203) % 0.18/0.42 | -p(V208) ) % 0.18/0.42 & ( p(V6) % 0.18/0.42 | p(V7) % 0.18/0.42 | p(V4) % 0.18/0.42 | p(V143) % 0.18/0.42 | p(V5) ) % 0.18/0.42 & ( p(V104) % 0.18/0.42 | p(V205) ) % 0.18/0.42 & ( -p(V30) % 0.18/0.42 | -p(V220) ) % 0.18/0.42 & ( p(V283) % 0.18/0.42 | -p(V282) ) % 0.18/0.42 & ( -p(V273) % 0.18/0.42 | -p(V43) ) % 0.18/0.42 & ( p(V129) % 0.18/0.42 | -p(V391) ) % 0.18/0.42 & ( p(V43) % 0.18/0.42 | p(V241) % 0.18/0.42 | -p(V242) ) % 0.18/0.42 & ( -p(V46) % 0.18/0.42 | -p(V270) ) % 0.18/0.42 & ( -p(V120) % 0.18/0.42 | p(V392) ) % 0.18/0.42 & ( p(V289) % 0.18/0.42 | p(V109) ) % 0.18/0.42 & ( p(V274) % 0.18/0.42 | p(V48) ) % 0.18/0.42 & ( -p(V379) % 0.18/0.42 | p(V343) ) % 0.18/0.42 & ( p(V131) % 0.18/0.42 | -p(V97) ) % 0.18/0.42 & ( p(V211) % 0.18/0.42 | -p(V210) ) % 0.18/0.42 & ( p(V104) % 0.18/0.42 | p(V235) ) % 0.18/0.42 & ( -p(V58) % 0.18/0.42 | p(V275) ) % 0.18/0.42 & ( p(V26) % 0.18/0.42 | p(V169) ) % 0.18/0.42 & ( p(V174) % 0.18/0.42 | -p(V35) ) % 0.18/0.42 & ( -p(V380) % 0.18/0.42 | p(V331) % 0.18/0.42 | p(V379) ) % 0.18/0.42 & ( p(V244) % 0.18/0.42 | -p(V249) ) % 0.18/0.42 & ( -p(V383) % 0.18/0.42 | p(V284) ) % 0.18/0.42 & ( p(V2) % 0.18/0.42 | -p(V118) ) % 0.18/0.42 & ( p(V334) % 0.18/0.42 | -p(V379) ) % 0.18/0.42 & ( -p(V125) % 0.18/0.42 | -p(V12) % 0.18/0.42 | -p(V123) % 0.18/0.42 | p(V127) % 0.18/0.42 | -p(V124) % 0.18/0.42 | -p(V7) % 0.18/0.42 | -p(V126) ) % 0.18/0.42 & ( p(V49) % 0.18/0.42 | p(V271) ) % 0.18/0.42 & ( p(V139) % 0.18/0.42 | -p(V22) ) % 0.18/0.42 & ( -p(V58) % 0.18/0.42 | -p(V308) ) % 0.18/0.42 & ( -p(V39) % 0.18/0.42 | p(V212) % 0.18/0.42 | -p(V213) ) % 0.18/0.42 & ( -p(V387) % 0.18/0.42 | p(V170) ) % 0.18/0.42 & ( p(V178) % 0.18/0.42 | -p(V172) ) % 0.18/0.42 & ( p(V110) % 0.18/0.42 | p(V322) ) % 0.18/0.42 & ( -p(V356) % 0.18/0.42 | -p(V89) % 0.18/0.42 | -p(V88) ) % 0.18/0.42 & ( p(V18) % 0.18/0.42 | p(V150) % 0.18/0.42 | -p(V151) ) % 0.18/0.42 & ( p(V103) % 0.18/0.42 | p(V239) ) % 0.18/0.42 & ( p(V290) % 0.18/0.42 | p(V381) % 0.18/0.42 | -p(V382) ) % 0.18/0.42 & ( p(V328) % 0.18/0.42 | -p(V331) ) % 0.18/0.42 & ( p(V313) % 0.18/0.42 | -p(V381) ) % 0.18/0.42 & ( p(V321) % 0.18/0.42 | -p(V320) ) % 0.18/0.42 & ( p(V235) % 0.18/0.42 | p(V56) % 0.18/0.42 | -p(V236) ) % 0.18/0.42 & ( p(V251) % 0.18/0.42 | p(V54) ) % 0.18/0.42 & ( p(V156) % 0.18/0.42 | -p(V155) ) % 0.18/0.42 & ( p(V344) % 0.18/0.42 | p(V72) % 0.18/0.42 | p(V71) % 0.18/0.42 | p(V74) % 0.18/0.42 | p(V73) ) % 0.18/0.42 & ( -p(V188) % 0.18/0.42 | -p(V17) ) % 0.18/0.42 & ( p(V224) % 0.18/0.42 | p(V37) ) % 0.18/0.42 & ( p(V33) % 0.18/0.42 | p(V203) ) % 0.18/0.42 & ( p(V223) % 0.18/0.42 | -p(V37) % 0.18/0.42 | -p(V224) ) % 0.18/0.42 & ( -p(V43) % 0.18/0.42 | -p(V253) ) % 0.18/0.42 & ( -p(V304) % 0.18/0.42 | p(V303) % 0.18/0.42 | p(V81) ) % 0.18/0.42 & ( p(V89) % 0.18/0.42 | p(V350) % 0.18/0.42 | -p(V351) ) % 0.18/0.42 & ( p(V125) % 0.18/0.42 | -p(V127) ) % 0.18/0.42 & ( p(V126) % 0.18/0.42 | -p(V6) ) % 0.18/0.42 & ( p(V30) % 0.18/0.42 | p(V32) % 0.18/0.42 | p(V33) % 0.18/0.42 | p(V226) % 0.18/0.42 | p(V31) % 0.18/0.42 | p(V29) ) % 0.18/0.42 & ( -p(V96) % 0.18/0.42 | p(V157) ) % 0.18/0.42 & ( p(V390) % 0.18/0.42 | -p(V134) ) % 0.18/0.42 & ( -p(V220) % 0.18/0.42 | -p(V32) ) % 0.18/0.42 & ( p(V268) % 0.18/0.42 | -p(V267) ) % 0.18/0.42 & ( p(V107) % 0.18/0.42 | p(V246) ) % 0.18/0.42 & ( p(V365) % 0.18/0.42 | -p(V91) ) % 0.18/0.42 & ( p(V272) % 0.18/0.42 | -p(V60) ) % 0.18/0.42 & ( -p(V237) % 0.18/0.42 | p(V238) ) % 0.18/0.42 & ( -p(V98) % 0.18/0.42 | p(V97) % 0.18/0.42 | -p(V7) % 0.18/0.42 | p(V96) % 0.18/0.42 | -p(V130) ) % 0.18/0.42 & ( -p(V82) % 0.18/0.42 | p(V293) ) % 0.18/0.42 & ( p(V241) % 0.18/0.42 | p(V102) ) % 0.18/0.42 & ( p(V105) % 0.18/0.42 | -p(V276) % 0.18/0.42 | -p(V107) % 0.18/0.42 | p(V106) ) % 0.18/0.42 & ( -p(V344) % 0.18/0.42 | -p(V72) ) % 0.18/0.42 & ( p(V283) % 0.18/0.42 | -p(V383) ) % 0.18/0.42 & ( -p(V228) % 0.18/0.42 | -p(V384) % 0.18/0.42 | -p(V236) % 0.18/0.42 | -p(V231) % 0.18/0.42 | -p(V238) % 0.18/0.42 | -p(V234) % 0.18/0.42 | -p(V211) % 0.18/0.42 | -p(V219) % 0.18/0.42 | -p(V243) % 0.18/0.42 | -p(V240) % 0.18/0.42 | -p(V225) % 0.18/0.42 | -p(V222) % 0.18/0.42 | -p(V242) % 0.18/0.42 | p(V385) ) % 0.18/0.42 & ( p(V91) % 0.18/0.42 | p(V373) ) % 0.18/0.42 & ( p(V372) % 0.18/0.42 | -p(V377) ) % 0.18/0.42 & ( p(V289) % 0.18/0.42 | p(V110) ) % 0.18/0.42 & ( -p(V63) % 0.18/0.42 | -p(V312) % 0.18/0.42 | p(V311) ) % 0.18/0.42 & ( -p(V32) % 0.18/0.42 | -p(V223) ) % 0.18/0.42 & ( p(V158) % 0.18/0.42 | -p(V157) ) % 0.18/0.42 & ( -p(V127) % 0.18/0.42 | p(V7) ) % 0.18/0.42 & ( -p(V74) % 0.18/0.42 | -p(V338) ) % 0.18/0.42 & ( -p(V57) % 0.18/0.42 | -p(V291) ) % 0.18/0.42 & ( p(V193) % 0.18/0.42 | -p(V387) ) % 0.18/0.42 & ( -p(V46) % 0.18/0.42 | -p(V250) ) % 0.18/0.42 & ( p(V286) % 0.18/0.42 | -p(V108) ) % 0.18/0.42 & ( -p(V215) % 0.18/0.42 | -p(V216) % 0.18/0.42 | -p(V217) % 0.18/0.42 | -p(V214) % 0.18/0.42 | -p(V53) % 0.18/0.42 | p(V218) % 0.18/0.42 | -p(V47) ) % 0.18/0.42 & ( -p(V63) % 0.18/0.42 | p(V269) ) % 0.18/0.42 & ( p(V59) % 0.18/0.42 | p(V287) ) % 0.18/0.42 & ( p(V204) % 0.18/0.42 | -p(V102) ) % 0.18/0.42 & ( p(V223) % 0.18/0.42 | p(V31) % 0.18/0.42 | p(V29) % 0.18/0.42 | p(V32) % 0.18/0.42 | p(V30) % 0.18/0.42 | p(V33) ) % 0.18/0.42 & ( p(V328) % 0.18/0.42 | p(V111) ) % 0.18/0.42 & ( p(V166) % 0.18/0.42 | p(V101) ) % 0.18/0.42 & ( p(V66) % 0.18/0.42 | -p(V281) % 0.18/0.42 | p(V280) ) % 0.18/0.42 & ( -p(V360) % 0.18/0.42 | -p(V83) ) % 0.18/0.42 & ( -p(V305) % 0.18/0.42 | -p(V60) ) % 0.18/0.42 & ( -p(V352) % 0.18/0.42 | p(V111) % 0.18/0.42 | -p(V113) % 0.18/0.42 | -p(V112) ) % 0.18/0.42 & ( p(V171) % 0.18/0.42 | -p(V25) % 0.18/0.42 | -p(V172) ) % 0.18/0.42 & ( -p(V232) % 0.18/0.42 | -p(V32) ) % 0.18/0.42 & ( p(V165) % 0.18/0.42 | -p(V167) ) % 0.18/0.42 & ( p(V9) % 0.18/0.42 | p(V150) ) % 0.18/0.42 & ( -p(V71) % 0.18/0.42 | -p(V347) ) % 0.18/0.42 & ( -p(V300) % 0.18/0.42 | p(V296) ) % 0.18/0.42 & ( -p(V270) % 0.18/0.42 | -p(V45) ) % 0.18/0.42 & ( p(V98) % 0.18/0.42 | p(V130) ) % 0.18/0.42 & ( p(V132) % 0.18/0.42 | p(V5) ) % 0.18/0.42 & ( p(V26) % 0.18/0.42 | -p(V145) % 0.18/0.42 | p(V144) ) % 0.18/0.42 & ( p(V254) % 0.18/0.42 | p(V53) ) % 0.18/0.42 & ( p(V195) % 0.18/0.42 | -p(V42) ) % 0.18/0.42 & ( p(V203) % 0.18/0.42 | p(V103) ) % 0.18/0.42 & ( p(V107) % 0.18/0.42 | p(V282) ) % 0.18/0.42 & ( -p(V177) % 0.18/0.42 | p(V39) ) % 0.18/0.42 & ( p(V108) % 0.18/0.42 | p(V287) ) % 0.18/0.42 & ( -p(V207) % 0.18/0.42 | -p(V102) % 0.18/0.42 | -p(V29) % 0.18/0.42 | -p(V104) % 0.18/0.42 | -p(V103) ) % 0.18/0.42 & ( p(V378) % 0.18/0.42 | -p(V379) ) % 0.18/0.42 & ( -p(V118) % 0.18/0.42 | p(V2) ) % 0.18/0.42 & ( p(V120) % 0.18/0.42 | p(V2) ) % 0.18/0.42 & ( -p(V110) % 0.18/0.42 | -p(V322) % 0.18/0.42 | -p(V109) % 0.18/0.42 | p(V108) ) % 0.18/0.42 & ( -p(V308) % 0.18/0.42 | p(V309) ) % 0.18/0.42 & ( -p(V387) % 0.18/0.42 | p(V386) ) % 0.18/0.42 & ( p(V362) % 0.18/0.42 | -p(V92) ) % 0.18/0.42 & ( -p(V35) % 0.18/0.42 | p(V187) ) % 0.18/0.42 & ( -p(V103) % 0.18/0.42 | p(V102) % 0.18/0.42 | -p(V104) % 0.18/0.42 | -p(V239) ) % 0.18/0.42 & ( p(V368) % 0.18/0.42 | -p(V367) ) % 0.18/0.42 & ( -p(V42) % 0.18/0.42 | -p(V202) % 0.18/0.42 | -p(V41) ) % 0.18/0.42 & ( -p(V72) % 0.18/0.42 | -p(V341) ) % 0.18/0.42 & ( -p(V49) % 0.18/0.42 | -p(V271) % 0.18/0.42 | p(V270) ) % 0.18/0.42 & ( p(V20) % 0.18/0.42 | p(V192) ) % 0.18/0.42 & ( -p(V288) % 0.18/0.42 | -p(V289) % 0.18/0.42 | p(V290) % 0.18/0.42 | -p(V285) % 0.18/0.42 | -p(V287) % 0.18/0.42 | -p(V286) ) % 0.18/0.42 & ( p(V100) % 0.18/0.42 | -p(V101) % 0.18/0.42 | -p(V18) % 0.18/0.42 | p(V99) % 0.18/0.42 | -p(V163) ) % 0.18/0.42 & ( -p(V188) % 0.18/0.42 | p(V189) ) % 0.18/0.42 & ( -p(V141) % 0.18/0.42 | p(V140) ) % 0.18/0.42 & ( p(V327) % 0.18/0.42 | p(V113) ) % 0.18/0.42 & ( -p(V177) % 0.18/0.42 | p(V174) ) % 0.18/0.42 & ( -p(V171) % 0.18/0.42 | -p(V17) ) % 0.18/0.42 & ( p(V43) % 0.18/0.42 | p(V44) % 0.18/0.42 | p(V45) % 0.18/0.42 | p(V261) % 0.18/0.42 | p(V47) % 0.18/0.42 | p(V46) ) % 0.18/0.42 & ( -p(V218) % 0.18/0.42 | p(V47) ) % 0.18/0.42 & ( -p(V328) % 0.18/0.42 | -p(V113) % 0.18/0.42 | p(V112) % 0.18/0.42 | -p(V73) % 0.18/0.42 | -p(V111) ) % 0.18/0.42 & ( -p(V385) % 0.18/0.42 | p(V384) ) % 0.18/0.42 & ( -p(V314) % 0.18/0.42 | -p(V58) ) % 0.18/0.42 & ( -p(V167) % 0.18/0.42 | p(V163) ) % 0.18/0.42 & ( p(V130) % 0.18/0.42 | -p(V134) ) % 0.18/0.42 & ( -p(V44) % 0.18/0.42 | -p(V270) ) % 0.18/0.42 & ( -p(V261) % 0.18/0.42 | -p(V47) ) % 0.18/0.42 & ( -p(V289) % 0.18/0.42 | -p(V108) % 0.18/0.42 | -p(V109) % 0.18/0.42 | -p(V57) % 0.18/0.42 | -p(V110) ) % 0.18/0.42 & ( p(V318) % 0.18/0.42 | -p(V82) ) % 0.18/0.42 & ( p(V1) % 0.18/0.42 | p(V117) ) % 0.18/0.42 & ( p(V11) % 0.18/0.42 | p(V6) % 0.18/0.42 | -p(V126) ) % 0.18/0.42 & ( p(V351) % 0.18/0.42 | -p(V379) ) % 0.18/0.42 & ( -p(V385) % 0.18/0.42 | p(V242) ) % 0.18/0.42 & ( -p(V294) % 0.18/0.42 | -p(V60) ) % 0.18/0.42 & ( p(V107) % 0.18/0.42 | p(V280) ) % 0.18/0.42 & ( p(V214) % 0.18/0.42 | -p(V56) ) % 0.18/0.42 & ( p(V296) % 0.18/0.42 | -p(V75) ) % 0.18/0.42 & ( -p(V74) % 0.18/0.42 | -p(V332) ) % 0.18/0.42 & ( -p(V233) % 0.18/0.42 | p(V234) ) % 0.18/0.42 & ( -p(V73) % 0.18/0.42 | -p(V338) ) % 0.18/0.42 & ( -p(V218) % 0.18/0.42 | p(V216) ) % 0.18/0.42 & ( p(V175) % 0.18/0.42 | -p(V177) ) % 0.18/0.42 & ( -p(V87) % 0.18/0.42 | p(V360) % 0.18/0.42 | -p(V361) ) % 0.18/0.42 & ( p(V222) % 0.18/0.42 | -p(V55) ) % 0.18/0.42 & ( p(V104) % 0.18/0.42 | p(V204) ) % 0.18/0.42 & ( p(V12) % 0.18/0.42 | -p(V127) ) % 0.18/0.42 & ( p(V91) % 0.18/0.42 | -p(V365) % 0.18/0.42 | p(V364) ) % 0.18/0.42 & ( -p(V377) % 0.18/0.42 | p(V368) ) % 0.18/0.42 & ( p(V207) % 0.18/0.42 | -p(V208) ) % 0.18/0.42 & ( p(V313) % 0.18/0.42 | -p(V312) ) % 0.18/0.42 & ( p(V79) % 0.18/0.42 | p(V336) ) % 0.18/0.42 & ( p(V98) % 0.18/0.42 | p(V131) ) % 0.18/0.42 & ( p(V149) % 0.18/0.42 | -p(V9) % 0.18/0.42 | -p(V150) ) % 0.18/0.42 & ( p(V97) % 0.18/0.42 | p(V159) ) % 0.18/0.42 & ( -p(V389) % 0.18/0.42 | p(V161) ) % 0.18/0.42 & ( p(V247) % 0.18/0.42 | -p(V105) ) % 0.18/0.42 & ( p(V130) % 0.18/0.42 | -p(V96) ) % 0.18/0.42 & ( p(V269) % 0.18/0.42 | -p(V383) ) % 0.18/0.42 & ( p(V228) % 0.18/0.42 | -p(V49) ) % 0.18/0.42 & ( -p(V176) % 0.18/0.42 | p(V37) % 0.18/0.42 | p(V31) ) % 0.18/0.42 & ( p(V100) % 0.18/0.42 | p(V162) ) % 0.18/0.42 & ( -p(V113) % 0.18/0.42 | -p(V112) % 0.18/0.42 | -p(V111) % 0.18/0.42 | -p(V71) % 0.18/0.42 | -p(V330) ) % 0.18/0.42 & ( -p(V57) % 0.18/0.42 | -p(V305) ) % 0.18/0.42 & ( -p(V261) % 0.18/0.42 | -p(V45) ) % 0.18/0.42 & ( -p(V63) % 0.18/0.42 | p(V256) ) % 0.18/0.42 & ( -p(V221) % 0.18/0.42 | p(V222) ) % 0.18/0.42 & ( -p(V17) % 0.18/0.42 | -p(V99) % 0.18/0.42 | p(V100) % 0.18/0.42 | -p(V164) % 0.18/0.42 | -p(V101) ) % 0.18/0.42 & ( p(V60) % 0.18/0.42 | p(V286) ) % 0.18/0.42 & ( p(V212) % 0.18/0.42 | p(V31) % 0.18/0.42 | p(V29) % 0.18/0.42 | p(V30) % 0.18/0.42 | p(V33) % 0.18/0.42 | p(V32) ) % 0.18/0.42 & ( p(V162) % 0.18/0.42 | p(V99) ) % 0.18/0.42 & ( -p(V113) % 0.18/0.42 | -p(V112) % 0.18/0.42 | -p(V354) % 0.18/0.42 | -p(V111) ) % 0.18/0.42 & ( -p(V214) % 0.18/0.42 | p(V48) % 0.18/0.42 | p(V56) ) % 0.18/0.42 & ( -p(V29) % 0.18/0.42 | -p(V226) ) % 0.18/0.42 & ( -p(V127) % 0.18/0.42 | p(V124) ) % 0.18/0.42 & ( p(V192) % 0.18/0.42 | -p(V191) ) % 0.18/0.42 & ( p(V371) % 0.18/0.42 | p(V115) ) % 0.18/0.42 & ( -p(V21) % 0.18/0.42 | p(V148) ) % 0.18/0.42 & ( -p(V46) % 0.18/0.42 | p(V105) % 0.18/0.42 | -p(V245) % 0.18/0.42 | -p(V107) % 0.18/0.42 | p(V106) ) % 0.18/0.42 & ( -p(V326) % 0.18/0.42 | -p(V82) % 0.18/0.42 | -p(V81) ) % 0.18/0.42 & ( -p(V60) % 0.18/0.42 | -p(V314) ) % 0.18/0.42 & ( p(V285) % 0.18/0.42 | p(V61) ) % 0.18/0.42 & ( p(V305) % 0.18/0.42 | p(V60) % 0.18/0.42 | p(V58) % 0.18/0.42 | p(V59) % 0.18/0.42 | p(V57) % 0.18/0.42 | p(V61) ) % 0.18/0.42 & ( p(V182) % 0.18/0.42 | p(V15) % 0.18/0.42 | p(V18) % 0.18/0.42 | p(V17) % 0.18/0.42 | p(V16) % 0.18/0.42 | p(V19) ) % 0.18/0.42 & ( p(V176) % 0.18/0.42 | -p(V31) ) % 0.18/0.42 & ( p(V4) % 0.18/0.42 | -p(V95) % 0.18/0.42 | -p(V121) ) % 0.18/0.42 & ( -p(V226) % 0.18/0.42 | -p(V33) ) % 0.18/0.42 & ( p(V125) % 0.18/0.42 | -p(V5) ) % 0.18/0.42 & ( -p(V15) % 0.18/0.42 | -p(V191) ) % 0.18/0.42 & ( p(V70) % 0.18/0.42 | -p(V252) % 0.18/0.42 | p(V251) ) % 0.18/0.42 & ( p(V133) % 0.18/0.42 | p(V96) ) % 0.18/0.42 & ( -p(V57) % 0.18/0.42 | -p(V311) ) % 0.18/0.42 & ( p(V189) % 0.18/0.42 | p(V32) % 0.18/0.42 | -p(V190) ) % 0.18/0.42 & ( p(V51) % 0.18/0.42 | p(V45) % 0.18/0.42 | -p(V217) ) % 0.18/0.42 & ( -p(V47) % 0.18/0.42 | -p(V264) ) % 0.18/0.42 & ( -p(V23) % 0.18/0.42 | p(V140) ) % 0.18/0.42 & ( -p(V17) % 0.18/0.42 | -p(V182) ) % 0.18/0.42 & ( p(V111) % 0.18/0.42 | p(V330) ) % 0.18/0.42 & ( p(V328) % 0.18/0.42 | -p(V112) ) % 0.18/0.42 & ( p(V306) % 0.18/0.42 | -p(V305) ) % 0.18/0.42 & ( -p(V389) % 0.18/0.42 | p(V142) ) % 0.18/0.42 & ( -p(V38) % 0.18/0.42 | p(V199) ) % 0.18/0.42 & ( -p(V352) % 0.18/0.42 | p(V353) ) % 0.18/0.42 & ( p(V288) % 0.18/0.42 | -p(V290) ) % 0.18/0.42 & ( p(V279) % 0.18/0.42 | -p(V69) ) % 0.18/0.42 & ( p(V359) % 0.18/0.42 | p(V377) % 0.18/0.42 | -p(V378) ) % 0.18/0.42 & ( -p(V183) % 0.18/0.42 | p(V184) ) % 0.18/0.42 & ( -p(V387) % 0.18/0.42 | p(V178) ) % 0.18/0.42 & ( -p(V168) % 0.18/0.42 | -p(V19) ) % 0.18/0.42 & ( p(V354) % 0.18/0.42 | p(V111) ) % 0.18/0.42 & ( p(V124) % 0.18/0.42 | -p(V9) ) % 0.18/0.42 & ( p(V109) % 0.18/0.42 | p(V322) ) % 0.18/0.42 & ( -p(V331) % 0.18/0.42 | p(V327) ) % 0.18/0.42 & ( -p(V15) % 0.18/0.42 | -p(V182) ) % 0.18/0.42 & ( -p(V223) % 0.18/0.42 | -p(V31) ) % 0.18/0.42 & ( p(V292) % 0.18/0.42 | -p(V291) ) % 0.18/0.42 & ( p(V25) % 0.18/0.42 | -p(V141) ) % 0.18/0.42 & ( p(V390) % 0.18/0.42 | -p(V389) ) % 0.18/0.42 & ( -p(V377) % 0.18/0.42 | p(V365) ) % 0.18/0.42 & ( -p(V123) % 0.18/0.42 | p(V14) % 0.18/0.42 | p(V8) ) % 0.18/0.42 & ( p(V142) % 0.18/0.42 | -p(V141) ) % 0.18/0.42 & ( -p(V322) % 0.18/0.42 | p(V323) ) % 0.18/0.42 & ( p(V17) % 0.18/0.42 | p(V19) % 0.18/0.42 | p(V16) % 0.18/0.42 | p(V191) % 0.18/0.42 | p(V15) % 0.18/0.42 | p(V18) ) % 0.18/0.42 & ( -p(V91) % 0.18/0.42 | -p(V373) % 0.18/0.42 | -p(V92) ) % 0.18/0.42 & ( p(V69) % 0.18/0.42 | p(V284) ) % 0.18/0.42 & ( -p(V357) % 0.18/0.42 | p(V359) % 0.18/0.42 | -p(V358) ) % 0.18/0.42 & ( -p(V64) % 0.18/0.42 | -p(V309) % 0.18/0.42 | p(V308) ) % 0.18/0.42 & ( p(V336) % 0.18/0.42 | p(V88) % 0.18/0.42 | -p(V337) ) % 0.18/0.42 & ( -p(V98) % 0.18/0.42 | -p(V157) % 0.18/0.42 | -p(V97) % 0.18/0.42 | p(V96) ) % 0.18/0.42 & ( -p(V21) % 0.18/0.42 | p(V188) % 0.18/0.42 | -p(V189) ) % 0.18/0.42 & ( p(V230) % 0.18/0.42 | p(V35) ) % 0.18/0.42 & ( -p(V43) % 0.18/0.42 | -p(V107) % 0.18/0.42 | -p(V248) % 0.18/0.42 | -p(V106) % 0.18/0.42 | -p(V105) ) % 0.18/0.42 & ( p(V73) % 0.18/0.42 | p(V312) % 0.18/0.42 | -p(V313) ) % 0.18/0.42 & ( -p(V255) % 0.18/0.42 | p(V70) % 0.18/0.42 | p(V62) ) % 0.18/0.42 & ( -p(V387) % 0.18/0.42 | p(V197) ) % 0.18/0.42 & ( p(V5) % 0.18/0.42 | p(V6) % 0.18/0.42 | p(V4) % 0.18/0.42 | p(V7) % 0.18/0.42 | p(V146) ) % 0.18/0.42 & ( -p(V152) % 0.18/0.42 | p(V153) ) % 0.18/0.42 & ( p(V210) % 0.18/0.42 | -p(V209) ) % 0.18/0.42 & ( -p(V108) % 0.18/0.42 | p(V317) ) % 0.18/0.42 & ( -p(V118) % 0.18/0.42 | p(V119) ) % 0.18/0.42 & ( -p(V230) % 0.18/0.42 | p(V231) ) % 0.18/0.42 & ( -p(V105) % 0.18/0.42 | -p(V246) % 0.18/0.42 | -p(V45) % 0.18/0.42 | -p(V107) % 0.18/0.42 | p(V106) ) % 0.18/0.42 & ( p(V258) % 0.18/0.42 | -p(V58) ) % 0.18/0.42 & ( -p(V60) % 0.18/0.42 | -p(V302) ) % 0.18/0.42 & ( p(V235) % 0.18/0.42 | -p(V103) ) % 0.18/0.42 & ( p(V317) % 0.18/0.42 | -p(V109) ) % 0.18/0.42 & ( p(V180) % 0.18/0.42 | -p(V179) ) % 0.18/0.42 & ( -p(V35) % 0.18/0.42 | p(V229) % 0.18/0.42 | -p(V230) ) % 0.18/0.42 & ( p(V289) % 0.18/0.42 | p(V57) ) % 0.18/0.42 & ( -p(V179) % 0.18/0.42 | -p(V17) ) % 0.18/0.42 & ( p(V11) % 0.18/0.42 | p(V144) ) % 0.18/0.42 & ( -p(V212) % 0.18/0.42 | -p(V32) ) % 0.18/0.42 & ( p(V236) % 0.18/0.42 | -p(V235) ) % 0.18/0.42 & ( p(V2) % 0.18/0.42 | -p(V118) ) % 0.18/0.42 & ( -p(V335) % 0.18/0.42 | p(V336) ) % 0.18/0.42 & ( -p(V108) % 0.18/0.42 | p(V288) ) % 0.18/0.42 & ( p(V348) % 0.18/0.42 | -p(V347) ) % 0.18/0.42 & ( -p(V174) % 0.18/0.42 | p(V41) % 0.18/0.42 | p(V35) ) % 0.18/0.42 & ( p(V200) % 0.18/0.42 | p(V101) ) % 0.18/0.42 & ( p(V280) % 0.18/0.42 | p(V106) ) % 0.18/0.42 & ( -p(V387) % 0.18/0.42 | p(V201) ) % 0.18/0.42 & ( -p(V46) % 0.18/0.42 | -p(V261) ) % 0.18/0.42 & ( -p(V383) % 0.18/0.42 | p(V277) ) % 0.18/0.42 & ( p(V167) % 0.18/0.42 | p(V387) % 0.18/0.42 | -p(V388) ) % 0.18/0.42 & ( p(V206) % 0.18/0.42 | -p(V102) ) % 0.18/0.42 & ( p(V310) % 0.18/0.42 | -p(V381) ) % 0.18/0.42 & ( -p(V206) % 0.18/0.42 | -p(V207) % 0.18/0.42 | -p(V205) % 0.18/0.42 | -p(V204) % 0.18/0.42 | -p(V203) % 0.18/0.42 | p(V208) ) % 0.18/0.42 & ( p(V108) % 0.18/0.42 | p(V324) ) % 0.18/0.42 & ( p(V256) % 0.18/0.42 | -p(V259) ) % 0.18/0.42 & ( -p(V99) % 0.18/0.42 | p(V165) ) % 0.18/0.42 & ( p(V285) % 0.18/0.42 | p(V108) ) % 0.18/0.42 & ( p(V199) % 0.18/0.42 | -p(V198) ) % 0.18/0.42 & ( p(V106) % 0.18/0.42 | p(V247) ) % 0.18/0.42 & ( -p(V93) % 0.18/0.42 | p(V375) ) % 0.18/0.42 & ( p(V282) % 0.18/0.42 | -p(V283) % 0.18/0.42 | p(V59) ) % 0.18/0.42 & ( p(V29) % 0.18/0.42 | p(V207) ) % 0.18/0.42 & ( -p(V57) % 0.18/0.42 | -p(V302) ) % 0.18/0.42 & ( -p(V335) % 0.18/0.42 | -p(V72) ) % 0.18/0.42 & ( p(V4) % 0.18/0.42 | p(V133) ) % 0.18/0.42 & ( p(V344) % 0.18/0.42 | -p(V345) % 0.18/0.42 | -p(V76) ) % 0.18/0.42 & ( p(V73) % 0.18/0.42 | p(V328) ) % 0.18/0.42 & ( p(V211) % 0.18/0.42 | -p(V56) ) % 0.18/0.42 & ( -p(V41) % 0.18/0.42 | p(V181) ) % 0.18/0.42 & ( p(V42) % 0.18/0.42 | p(V34) % 0.18/0.42 | -p(V173) ) % 0.18/0.42 & ( p(V366) % 0.18/0.42 | -p(V85) % 0.18/0.42 | -p(V367) ) % 0.18/0.42 & ( p(V296) % 0.18/0.42 | -p(V82) ) % 0.18/0.42 & ( p(V128) % 0.18/0.42 | -p(V127) ) % 0.18/0.42 & ( -p(V273) % 0.18/0.42 | -p(V46) ) % 0.18/0.42 & ( p(V315) % 0.18/0.42 | p(V62) ) % 0.18/0.42 & ( p(V2) % 0.18/0.42 | -p(V118) ) % 0.18/0.42 & ( -p(V80) % 0.18/0.42 | p(V307) ) % 0.18/0.42 & ( p(V160) % 0.18/0.42 | -p(V159) ) % 0.18/0.42 & ( -p(V369) % 0.18/0.42 | p(V370) ) % 0.18/0.42 & ( -p(V43) % 0.18/0.42 | -p(V261) ) % 0.18/0.42 & ( -p(V383) % 0.18/0.42 | p(V279) ) % 0.18/0.42 & ( p(V98) % 0.18/0.42 | p(V159) ) % 0.18/0.42 & ( p(V6) % 0.18/0.42 | p(V131) ) % 0.18/0.42 & ( p(V16) % 0.18/0.42 | p(V18) % 0.18/0.42 | p(V19) % 0.18/0.42 | p(V15) % 0.18/0.42 | p(V17) % 0.18/0.42 | p(V179) ) % 0.18/0.42 & ( p(V301) % 0.18/0.42 | -p(V300) ) % 0.18/0.42 & ( p(V185) % 0.18/0.42 | p(V15) % 0.18/0.42 | p(V17) % 0.18/0.42 | p(V16) % 0.18/0.42 | p(V19) % 0.18/0.42 | p(V18) ) % 0.18/0.42 & ( -p(V264) % 0.18/0.42 | -p(V44) ) % 0.18/0.42 & ( -p(V24) % 0.18/0.42 | p(V158) ) % 0.18/0.42 & ( p(V105) % 0.18/0.42 | p(V282) ) % 0.18/0.42 & ( -p(V31) % 0.18/0.42 | p(V193) ) % 0.18/0.42 & ( -p(V71) % 0.18/0.42 | -p(V335) ) % 0.18/0.42 & ( -p(V58) % 0.18/0.42 | -p(V302) ) % 0.18/0.42 & ( p(V29) % 0.18/0.42 | p(V31) % 0.18/0.42 | p(V30) % 0.18/0.42 | p(V33) % 0.18/0.42 | p(V32) % 0.18/0.42 | p(V229) ) % 0.18/0.42 & ( -p(V267) % 0.18/0.42 | -p(V45) ) % 0.18/0.42 & ( -p(V305) % 0.18/0.42 | -p(V59) ) % 0.18/0.42 & ( p(V289) % 0.18/0.42 | p(V108) ) % 0.18/0.42 & ( p(V132) % 0.18/0.42 | -p(V96) ) % 0.18/0.42 & ( p(V78) % 0.18/0.42 | p(V339) ) % 0.18/0.42 & ( p(V135) % 0.18/0.42 | -p(V12) % 0.18/0.42 | -p(V136) ) % 0.18/0.42 & ( -p(V308) % 0.18/0.42 | -p(V60) ) % 0.18/0.42 & ( p(V23) % 0.18/0.42 | p(V183) ) % 0.18/0.42 & ( -p(V33) % 0.18/0.42 | -p(V223) ) % 0.18/0.42 & ( p(V152) % 0.18/0.42 | -p(V153) % 0.18/0.42 | -p(V8) ) % 0.18/0.42 & ( p(V200) % 0.18/0.42 | p(V100) ) % 0.18/0.42 & ( -p(V387) % 0.18/0.42 | p(V202) ) % 0.18/0.42 & ( -p(V107) % 0.18/0.42 | p(V244) ) % 0.18/0.42 & ( p(V118) % 0.18/0.42 | -p(V3) % 0.18/0.42 | -p(V2) ) % 0.18/0.42 & ( -p(V216) % 0.18/0.42 | p(V44) % 0.18/0.42 | p(V50) ) % 0.18/0.42 & ( p(V260) % 0.18/0.42 | -p(V383) ) % 0.18/0.42 & ( -p(V315) % 0.18/0.42 | p(V316) ) % 0.18/0.42 & ( p(V314) % 0.18/0.42 | -p(V315) % 0.18/0.42 | -p(V62) ) % 0.18/0.42 & ( -p(V169) % 0.18/0.42 | p(V170) ) % 0.18/0.42 & ( p(V317) % 0.18/0.42 | p(V110) ) % 0.18/0.42 & ( p(V68) % 0.18/0.42 | p(V292) ) % 0.18/0.42 & ( -p(V29) % 0.18/0.42 | p(V201) ) % 0.18/0.42 & ( p(V125) % 0.18/0.42 | -p(V10) ) % 0.18/0.42 & ( p(V345) % 0.18/0.42 | -p(V344) ) % 0.18/0.42 & ( -p(V13) % 0.18/0.42 | p(V124) ) % 0.18/0.42 & ( p(V315) % 0.18/0.42 | -p(V314) ) % 0.18/0.42 & ( -p(V45) % 0.18/0.42 | p(V217) ) % 0.18/0.42 & ( -p(V72) % 0.18/0.42 | -p(V347) ) % 0.18/0.42 & ( -p(V74) % 0.18/0.42 | -p(V335) ) % 0.18/0.42 & ( p(V312) % 0.18/0.42 | -p(V311) ) % 0.18/0.42 & ( -p(V193) % 0.18/0.42 | -p(V197) % 0.18/0.42 | -p(V190) % 0.18/0.42 | p(V387) % 0.18/0.42 | -p(V170) % 0.18/0.42 | -p(V187) % 0.18/0.42 | -p(V178) % 0.18/0.42 | -p(V201) % 0.18/0.42 | -p(V199) % 0.18/0.42 | -p(V181) % 0.18/0.42 | -p(V202) % 0.18/0.42 | -p(V195) % 0.18/0.42 | -p(V184) % 0.18/0.42 | -p(V386) ) % 0.18/0.42 & ( p(V82) % 0.18/0.42 | p(V317) % 0.18/0.42 | -p(V318) ) % 0.18/0.42 & ( -p(V259) % 0.18/0.42 | p(V67) ) % 0.18/0.42 & ( p(V310) % 0.18/0.42 | -p(V309) ) % 0.18/0.42 & ( p(V105) % 0.18/0.42 | p(V246) ) % 0.18/0.42 & ( -p(V358) % 0.18/0.42 | -p(V114) % 0.18/0.42 | -p(V115) % 0.18/0.42 | -p(V83) ) % 0.18/0.42 & ( p(V278) % 0.18/0.42 | -p(V279) % 0.18/0.42 | p(V69) ) % 0.18/0.42 & ( p(V188) % 0.18/0.42 | p(V17) % 0.18/0.42 | p(V18) % 0.18/0.42 | p(V15) % 0.18/0.42 | p(V19) % 0.18/0.42 | p(V16) ) % 0.18/0.42 & ( p(V193) % 0.18/0.42 | -p(V192) ) % 0.18/0.42 & ( p(V103) % 0.18/0.42 | p(V206) ) % 0.18/0.42 & ( p(V230) % 0.18/0.42 | -p(V229) ) % 0.18/0.42 & ( p(V239) % 0.18/0.42 | -p(V102) ) % 0.18/0.42 & ( p(V5) % 0.18/0.42 | p(V10) % 0.18/0.42 | -p(V125) ) % 0.18/0.42 & ( -p(V268) % 0.18/0.42 | -p(V50) % 0.18/0.42 | p(V267) ) % 0.18/0.42 & ( -p(V43) % 0.18/0.42 | -p(V270) ) % 0.18/0.42 & ( p(V93) % 0.18/0.42 | -p(V375) % 0.18/0.42 | -p(V116) ) % 0.18/0.42 & ( p(V30) % 0.18/0.42 | p(V220) % 0.18/0.42 | p(V29) % 0.18/0.42 | p(V31) % 0.18/0.42 | p(V32) % 0.18/0.42 | p(V33) ) % 0.18/0.42 & ( p(V369) % 0.18/0.42 | -p(V114) ) % 0.18/0.42 & ( p(V169) % 0.18/0.42 | -p(V168) ) % 0.18/0.42 & ( -p(V389) % 0.18/0.42 | p(V145) ) % 0.18/0.42 & ( -p(V366) % 0.18/0.42 | -p(V84) ) % 0.18/0.42 & ( p(V284) % 0.18/0.42 | p(V70) ) % 0.18/0.42 & ( p(V150) % 0.18/0.42 | -p(V149) ) % 0.18/0.42 & ( -p(V29) % 0.18/0.42 | -p(V232) ) % 0.18/0.42 & ( p(V180) % 0.18/0.42 | p(V41) % 0.18/0.42 | -p(V181) ) % 0.18/0.42 & ( -p(V5) % 0.18/0.42 | -p(V152) ) % 0.18/0.42 & ( -p(V52) % 0.18/0.42 | p(V240) ) % 0.18/0.42 & ( -p(V30) % 0.18/0.42 | -p(V232) ) % 0.18/0.42 & ( p(V316) % 0.18/0.42 | -p(V381) ) % 0.18/0.42 & ( p(V159) % 0.18/0.42 | -p(V160) % 0.18/0.42 | p(V15) ) % 0.18/0.42 & ( -p(V220) % 0.18/0.42 | -p(V33) ) % 0.18/0.42 & ( -p(V105) % 0.18/0.42 | p(V245) ) % 0.18/0.42 & ( p(V106) % 0.18/0.42 | p(V282) ) % 0.18/0.42 & ( p(V13) % 0.18/0.42 | p(V129) ) % 0.18/0.42 & ( -p(V54) % 0.18/0.42 | p(V225) ) % 0.18/0.42 & ( -p(V227) % 0.18/0.42 | p(V228) ) % 0.18/0.42 & ( p(V222) % 0.18/0.42 | -p(V385) ) % 0.18/0.42 & ( -p(V58) % 0.18/0.42 | -p(V291) ) % 0.18/0.42 & ( p(V298) % 0.18/0.42 | -p(V77) ) % 0.18/0.42 & ( -p(V185) % 0.18/0.42 | -p(V19) ) % 0.18/0.42 & ( p(V250) % 0.18/0.42 | p(V47) % 0.18/0.42 | p(V43) % 0.18/0.42 | p(V45) % 0.18/0.42 | p(V44) % 0.18/0.42 | p(V46) ) % 0.18/0.42 & ( -p(V379) % 0.18/0.42 | p(V346) ) % 0.18/0.42 & ( -p(V31) % 0.18/0.42 | -p(V226) ) % 0.18/0.42 & ( -p(V45) % 0.18/0.42 | -p(V250) ) % 0.18/0.42 & ( p(V122) % 0.18/0.42 | p(V3) ) % 0.18/0.42 & ( p(V295) % 0.18/0.42 | -p(V294) ) % 0.18/0.42 & ( -p(V200) % 0.18/0.42 | p(V201) ) % 0.18/0.42 & ( -p(V319) % 0.18/0.42 | -p(V108) % 0.18/0.42 | -p(V110) % 0.18/0.42 | p(V109) ) % 0.18/0.42 & ( p(V73) % 0.18/0.42 | p(V72) % 0.18/0.42 | p(V71) % 0.18/0.42 | p(V74) % 0.18/0.42 | p(V332) ) % 0.18/0.42 & ( p(V274) % 0.18/0.42 | -p(V273) ) % 0.18/0.42 & ( p(V107) % 0.18/0.42 | p(V276) ) % 0.18/0.42 & ( -p(V31) % 0.18/0.42 | -p(V229) ) % 0.18/0.42 & ( -p(V109) % 0.18/0.42 | p(V286) ) % 0.18/0.42 & ( p(V217) % 0.18/0.42 | -p(V218) ) % 0.18/0.42 & ( -p(V261) % 0.18/0.42 | -p(V44) ) % 0.18/0.42 & ( p(V52) % 0.18/0.42 | p(V262) ) % 0.18/0.42 & ( -p(V84) % 0.18/0.42 | -p(V363) ) % 0.18/0.42 & ( -p(V291) % 0.18/0.42 | -p(V60) ) % 0.18/0.42 & ( -p(V101) % 0.18/0.42 | p(V162) ) % 0.18/0.42 & ( -p(V148) % 0.18/0.42 | p(V21) % 0.18/0.42 | p(V147) ) % 0.18/0.42 & ( p(V376) % 0.18/0.42 | -p(V374) ) % 0.18/0.42 & ( -p(V366) % 0.18/0.42 | p(V367) ) % 0.18/0.42 & ( -p(V295) % 0.18/0.42 | p(V301) ) % 0.18/0.42 & ( p(V216) % 0.18/0.42 | -p(V50) ) % 0.18/0.42 & ( -p(V179) % 0.18/0.42 | -p(V15) ) % 0.18/0.42 & ( -p(V171) % 0.18/0.42 | -p(V18) ) % 0.18/0.42 & ( p(V370) % 0.18/0.42 | -p(V377) ) % 0.18/0.42 & ( -p(V100) % 0.18/0.42 | -p(V166) % 0.18/0.42 | -p(V15) % 0.18/0.42 | -p(V99) % 0.18/0.42 | -p(V101) ) % 0.18/0.42 & ( -p(V387) % 0.18/0.42 | p(V187) ) % 0.18/0.42 & ( p(V63) % 0.18/0.42 | p(V69) % 0.18/0.42 | -p(V256) ) % 0.18/0.42 & ( -p(V302) % 0.18/0.42 | p(V303) ) % 0.18/0.42 & ( -p(V71) % 0.18/0.42 | -p(V338) ) % 0.18/0.42 & ( p(V263) % 0.18/0.42 | -p(V69) ) % 0.18/0.42 & ( p(V131) % 0.18/0.42 | -p(V134) ) % 0.18/0.42 & ( -p(V71) % 0.18/0.42 | -p(V332) ) % 0.18/0.42 & ( -p(V171) % 0.18/0.42 | -p(V15) ) % 0.18/0.42 & ( -p(V178) % 0.18/0.42 | p(V172) % 0.18/0.42 | p(V177) ) % 0.18/0.42 & ( -p(V182) % 0.18/0.42 | p(V183) ) % 0.18/0.42 & ( p(V238) % 0.18/0.42 | -p(V385) ) % 0.18/0.42 & ( p(V190) % 0.18/0.42 | -p(V189) ) % 0.18/0.42 & ( -p(V253) % 0.18/0.42 | p(V254) ) % 0.18/0.42 & ( -p(V20) % 0.18/0.42 | -p(V192) % 0.18/0.42 | p(V191) ) % 0.18/0.42 & ( p(V155) % 0.18/0.42 | p(V98) ) % 0.18/0.42 & ( -p(V188) % 0.18/0.42 | -p(V18) ) % 0.18/0.42 & ( -p(V170) % 0.18/0.42 | p(V169) % 0.18/0.42 | p(V42) ) % 0.18/0.42 & ( p(V375) % 0.18/0.42 | p(V116) ) % 0.18/0.42 & ( p(V76) % 0.18/0.42 | p(V345) ) % 0.18/0.42 & ( p(V43) % 0.18/0.42 | p(V248) ) % 0.18/0.42 & ( p(V388) % 0.18/0.42 | -p(V167) ) % 0.18/0.42 & ( -p(V331) % 0.18/0.42 | p(V329) ) % 0.18/0.42 & ***HERE*** ( p(V358) % 0.18/0.42 | p(V114) ) % 0.18/0.42 & ( -p(V18) % 0.18/0.42 | -p(V182) ) % 0.18/0.42 & ( p(V164) % 0.18/0.42 | p(V99) ) % 0.18/0.42 & ( -p(V91) % 0.18/0.42 | p(V372) ) % 0.18/0.42 & ( -p(V4) % 0.18/0.42 | -p(V149) ) % 0.18/0.42 & ( -p(V258) % 0.18/0.42 | p(V65) % 0.18/0.42 | p(V58) ) % 0.18/0.42 & ( -p(V381) % 0.18/0.42 | p(V380) ) % 0.18/0.42 & ( p(V350) % 0.18/0.42 | p(V113) ) % 0.18/0.42 & ( p(V340) % 0.18/0.42 | -p(V87) ) % 0.18/0.42 & ( p(V40) % 0.18/0.42 | p(V183) % 0.18/0.42 | -p(V184) ) % 0.18/0.42 & ( p(V243) % 0.18/0.42 | p(V55) ) % 0.18/0.42 & ( -p(V360) % 0.18/0.42 | p(V361) ) % 0.18/0.42 & ( -p(V16) % 0.18/0.42 | -p(V182) ) % 0.18/0.42 & ( -p(V15) % 0.18/0.42 | -p(V168) ) % 0.18/0.42 & ( p(V358) % 0.18/0.42 | p(V115) ) % 0.18/0.42 & ( -p(V208) % 0.18/0.42 | p(V204) ) % 0.18/0.42 & ( -p(V69) % 0.18/0.42 | p(V256) ) % 0.18/0.42 & ( -p(V381) % 0.18/0.42 | p(V293) ) % 0.18/0.42 & ( p(V112) % 0.18/0.42 | -p(V113) % 0.18/0.42 | -p(V74) % 0.18/0.42 | -p(V327) % 0.18/0.42 | p(V111) ) % 0.18/0.42 & ( p(V316) % 0.18/0.42 | -p(V72) ) % 0.18/0.42 & ( p(V164) % 0.18/0.42 | p(V101) ) % 0.18/0.42 & ( -p(V111) % 0.18/0.42 | p(V352) ) % 0.18/0.42 & ( -p(V209) % 0.18/0.42 | -p(V32) ) % 0.18/0.42 & ( p(V303) % 0.18/0.42 | p(V66) ) % 0.18/0.42 & ( p(V138) % 0.18/0.42 | -p(V141) ) % 0.18/0.42 & ( -p(V191) % 0.18/0.42 | -p(V19) ) % 0.18/0.42 & ( -p(V117) % 0.18/0.42 | p(V394) ) % 0.18/0.42 & ( -p(V168) % 0.18/0.42 | -p(V16) ) % 0.18/0.42 & ( -p(V335) % 0.18/0.42 | -p(V73) ) % 0.18/0.42 & ( p(V207) % 0.18/0.42 | p(V102) ) % 0.18/0.42 & ( -p(V49) % 0.18/0.42 | p(V215) ) % 0.18/0.42 & ( p(V350) % 0.18/0.42 | p(V111) ) % 0.18/0.42 & ( -p(V61) % 0.18/0.42 | -p(V305) ) % 0.18/0.42 & ( p(V330) % 0.18/0.42 | p(V113) ) % 0.18/0.42 & ( p(V299) % 0.18/0.42 | -p(V300) ) % 0.18/0.42 & ( -p(V368) % 0.18/0.42 | -p(V376) % 0.18/0.42 | -p(V362) % 0.18/0.42 | -p(V370) % 0.18/0.42 | -p(V373) % 0.18/0.42 | -p(V365) % 0.18/0.42 | -p(V372) % 0.18/0.42 | p(V377) ) % 0.18/0.42 & ( p(V309) % 0.18/0.42 | -p(V310) % 0.18/0.42 | p(V76) ) % 0.18/0.42 & ( p(V334) % 0.18/0.42 | -p(V333) ) % 0.18/0.42 & ( p(V178) % 0.18/0.42 | -p(V177) ) % 0.18/0.42 & ( p(V273) % 0.18/0.42 | -p(V274) % 0.18/0.42 | -p(V48) ) % 0.18/0.42 & ( -p(V316) % 0.18/0.42 | -p(V325) % 0.18/0.42 | -p(V321) % 0.18/0.42 | -p(V326) % 0.18/0.42 | -p(V323) % 0.18/0.42 | -p(V301) % 0.18/0.42 | -p(V310) % 0.18/0.42 | -p(V307) % 0.18/0.42 | -p(V380) % 0.18/0.42 | -p(V304) % 0.18/0.42 | p(V381) % 0.18/0.42 | -p(V293) % 0.18/0.42 | -p(V318) % 0.18/0.42 | -p(V313) ) % 0.18/0.42 & ( p(V44) % 0.18/0.42 | p(V45) % 0.18/0.42 | p(V43) % 0.18/0.42 | p(V264) % 0.18/0.42 | p(V47) % 0.18/0.42 | p(V46) ) % 0.18/0.42 & ( -p(V76) % 0.18/0.42 | p(V297) ) % 0.18/0.42 & ( p(V131) % 0.18/0.42 | p(V96) ) % 0.18/0.42 & ( p(V225) % 0.18/0.42 | -p(V385) ) % 0.18/0.42 & ( p(V92) % 0.18/0.42 | -p(V370) % 0.18/0.42 | p(V369) ) % 0.18/0.42 & ( -p(V114) % 0.18/0.42 | -p(V371) % 0.18/0.42 | -p(V115) ) % 0.18/0.42 & ( p(V17) % 0.18/0.42 | p(V164) ) % 0.18/0.42 & ( -p(V150) % 0.18/0.42 | p(V151) ) % 0.18/0.42 & ( -p(V42) % 0.18/0.42 | p(V170) ) % 0.18/0.42 & ( -p(V33) % 0.18/0.42 | -p(V203) % 0.18/0.42 | -p(V102) % 0.18/0.42 | p(V104) % 0.18/0.42 | -p(V103) ) % 0.18/0.42 & ( -p(V31) % 0.18/0.42 | -p(V232) ) % 0.18/0.42 & ( p(V74) % 0.18/0.42 | p(V71) % 0.18/0.42 | p(V72) % 0.18/0.42 | p(V73) % 0.18/0.42 | p(V341) ) % 0.18/0.42 & ( -p(V95) % 0.18/0.42 | -p(V2) % 0.18/0.42 | -p(V120) ) % 0.18/0.42 & ( -p(V19) % 0.18/0.42 | p(V101) % 0.18/0.42 | -p(V162) % 0.18/0.42 | -p(V99) % 0.18/0.42 | -p(V100) ) % 0.18/0.42 & ( -p(V350) % 0.18/0.42 | p(V112) % 0.18/0.42 | -p(V113) % 0.18/0.42 | -p(V111) ) % 0.18/0.42 & ( p(V215) % 0.18/0.42 | -p(V218) ) % 0.18/0.42 & ( p(V209) % 0.18/0.42 | -p(V210) % 0.18/0.42 | -p(V40) ) % 0.18/0.42 & ( -p(V346) % 0.18/0.42 | -p(V378) % 0.18/0.42 | -p(V349) % 0.18/0.42 | -p(V353) % 0.18/0.42 | p(V379) % 0.18/0.42 | -p(V343) % 0.18/0.42 | -p(V355) % 0.18/0.42 | -p(V334) % 0.18/0.42 | -p(V351) % 0.18/0.42 | -p(V340) % 0.18/0.42 | -p(V356) % 0.18/0.42 | -p(V337) ) % 0.18/0.42 & ( p(V89) % 0.18/0.42 | p(V356) ) % 0.18/0.42 & ( -p(V135) % 0.18/0.42 | -p(V4) ) % 0.18/0.42 & ( -p(V272) % 0.18/0.42 | p(V271) % 0.18/0.42 | p(V60) ) % 0.18/0.42 & ( p(V318) % 0.18/0.42 | -p(V381) ) % 0.18/0.42 & ( -p(V60) % 0.18/0.42 | -p(V311) ) % 0.18/0.42 & ( p(V101) % 0.18/0.42 | p(V196) ) % 0.18/0.42 & ( -p(V104) % 0.18/0.42 | p(V203) ) % 0.18/0.42 & ( -p(V4) % 0.18/0.42 | p(V121) ) % 0.18/0.42 & ( p(V300) % 0.18/0.42 | -p(V299) % 0.18/0.42 | -p(V297) % 0.18/0.42 | -p(V74) % 0.18/0.42 | -p(V296) % 0.18/0.42 | -p(V298) ) % 0.18/0.42 & ( p(V139) % 0.18/0.42 | -p(V16) ) % 0.18/0.42 & ( -p(V253) % 0.18/0.42 | -p(V45) ) % 0.18/0.42 & ( p(V304) % 0.18/0.42 | -p(V81) ) % 0.18/0.42 & ( -p(V134) % 0.18/0.42 | p(V133) ) % 0.18/0.42 & ( p(V54) % 0.18/0.42 | -p(V225) % 0.18/0.42 | p(V224) ) % 0.18/0.42 & ( p(V67) % 0.18/0.42 | p(V295) ) % 0.18/0.42 & ( -p(V30) % 0.18/0.42 | -p(V212) ) % 0.18/0.42 & ( -p(V366) % 0.18/0.42 | -p(V83) ) % 0.18/0.42 & ( -p(V6) % 0.18/0.42 | p(V97) % 0.18/0.42 | -p(V131) % 0.18/0.42 | -p(V96) % 0.18/0.42 | -p(V98) ) % 0.18/0.42 & ( -p(V155) % 0.18/0.42 | p(V97) % 0.18/0.42 | -p(V96) % 0.18/0.42 | -p(V98) ) % 0.18/0.42 & ( p(V260) % 0.18/0.42 | -p(V254) ) % 0.18/0.42 & ( p(V213) % 0.18/0.42 | -p(V212) ) % 0.18/0.42 & ( -p(V17) % 0.18/0.42 | p(V140) ) % 0.18/0.42 & ( -p(V262) % 0.18/0.42 | p(V263) ) % 0.18/0.42 & ( p(V252) % 0.18/0.42 | -p(V251) ) % 0.18/0.42 & ( p(V184) % 0.18/0.42 | -p(V40) ) % 0.18/0.42 & ( p(V7) % 0.18/0.42 | p(V130) ) % 0.18/0.42 & ( -p(V28) % 0.18/0.42 | p(V137) ) % 0.18/0.42 & ( -p(V158) % 0.18/0.42 | p(V157) % 0.18/0.42 | p(V24) ) % 0.18/0.42 & ( p(V30) % 0.18/0.42 | p(V36) % 0.18/0.42 | -p(V175) ) % 0.18/0.42 & ( -p(V34) % 0.18/0.42 | p(V173) ) % 0.18/0.42 & ( p(V206) % 0.18/0.42 | p(V30) ) % 0.18/0.42 & ( p(V279) % 0.18/0.42 | -p(V278) ) % 0.18/0.42 & ( -p(V6) % 0.18/0.42 | -p(V143) ) % 0.18/0.42 & ( -p(V297) % 0.18/0.42 | p(V81) % 0.18/0.42 | p(V76) ) % 0.18/0.42 & ( p(V39) % 0.18/0.42 | p(V213) ) % 0.18/0.42 & ( p(V367) % 0.18/0.42 | p(V90) % 0.18/0.42 | -p(V368) ) % 0.18/0.42 & ( p(V241) % 0.18/0.42 | p(V103) ) % 0.18/0.42 & ( -p(V99) % 0.18/0.42 | -p(V100) % 0.18/0.42 | -p(V200) % 0.18/0.42 | -p(V101) ) % 0.18/0.42 & ( -p(V371) % 0.18/0.42 | p(V372) ) % 0.18/0.42 & ( p(V237) % 0.18/0.42 | -p(V103) ) % 0.18/0.42 & ( p(V98) % 0.18/0.42 | p(V133) ) % 0.18/0.42 & ( -p(V249) % 0.18/0.42 | p(V245) ) % 0.18/0.42 & ( p(V163) % 0.18/0.42 | p(V18) ) % 0.18/0.42 & ( p(V51) % 0.18/0.42 | p(V265) ) % 0.18/0.42 & ( p(V187) % 0.18/0.42 | -p(V186) ) % 0.18/0.42 & ( p(V32) % 0.18/0.42 | p(V204) ) % 0.18/0.42 & ( p(V105) % 0.18/0.42 | p(V278) ) % 0.18/0.42 & ( p(V15) % 0.18/0.42 | p(V18) % 0.18/0.42 | p(V17) % 0.18/0.42 | p(V19) % 0.18/0.42 | p(V16) % 0.18/0.42 | p(V171) ) % 0.18/0.42 & ( -p(V389) % 0.18/0.42 | p(V156) ) % 0.18/0.42 & ( -p(V344) % 0.18/0.42 | -p(V74) ) % 0.18/0.42 & ( p(V184) % 0.18/0.42 | -p(V387) ) % 0.18/0.42 & ( -p(V383) % 0.18/0.42 | p(V263) ) % 0.18/0.42 & ( -p(V105) % 0.18/0.42 | -p(V107) % 0.18/0.42 | -p(V278) % 0.18/0.42 | p(V106) ) % 0.18/0.42 & ( p(V327) % 0.18/0.42 | -p(V112) ) % 0.18/0.42 & ( -p(V149) % 0.18/0.42 | -p(V5) ) % 0.18/0.42 & ( p(V189) % 0.18/0.42 | p(V21) ) % 0.18/0.42 & ( -p(V224) % 0.18/0.42 | p(V225) ) % 0.18/0.42 & ( -p(V141) % 0.18/0.42 | p(V137) ) % 0.18/0.42 & ( -p(V33) % 0.18/0.42 | -p(V212) ) % 0.18/0.42 & ( -p(V379) % 0.18/0.42 | p(V380) ) % 0.18/0.42 & ( p(V101) % 0.18/0.42 | p(V198) ) % 0.18/0.42 & ( p(V72) % 0.18/0.42 | p(V78) % 0.18/0.42 | -p(V299) ) % 0.18/0.42 & ( p(V217) % 0.18/0.42 | -p(V51) ) % 0.18/0.42 & ( p(V154) % 0.18/0.42 | -p(V389) ) % 0.18/0.42 & ( -p(V1) % 0.18/0.42 | p(V395) % 0.18/0.42 | -p(V394) ) % 0.18/0.42 & ( p(V107) % 0.18/0.42 | -p(V105) % 0.18/0.42 | -p(V106) % 0.18/0.42 | -p(V47) % 0.18/0.42 | -p(V244) ) % 0.18/0.42 & ( p(V154) % 0.18/0.42 | -p(V17) ) % 0.18/0.42 & ( -p(V196) % 0.18/0.42 | -p(V99) % 0.18/0.42 | p(V100) % 0.18/0.42 | -p(V101) ) % 0.18/0.42 & ( p(V88) % 0.18/0.42 | p(V352) % 0.18/0.42 | -p(V353) ) % 0.18/0.42 & ( -p(V308) % 0.18/0.42 | -p(V61) ) % 0.18/0.42 & ( p(V99) % 0.18/0.42 | p(V166) ) % 0.18/0.42 & ( p(V74) % 0.18/0.42 | p(V347) % 0.18/0.42 | p(V73) % 0.18/0.42 | p(V71) % 0.18/0.42 | p(V72) ) % 0.18/0.42 & ( -p(V229) % 0.18/0.42 | -p(V33) ) % 0.18/0.42 & ( p(V357) % 0.18/0.42 | p(V84) ) % 0.18/0.42 & ( p(V237) % 0.18/0.42 | p(V104) ) % 0.18/0.42 & ( p(V104) % 0.18/0.42 | p(V239) ) % 0.18/0.42 & ( p(V244) % 0.18/0.42 | p(V106) ) % 0.18/0.42 & ( -p(V395) % 0.18/0.42 | p(V1) ) % 0.18/0.42 & ( -p(V265) % 0.18/0.42 | p(V264) % 0.18/0.42 | -p(V51) ) % 0.18/0.42 & ( p(V219) % 0.18/0.42 | -p(V213) ) % 0.18/0.42 & ( p(V119) % 0.18/0.42 | p(V94) ) % 0.18/0.42 & ( -p(V79) % 0.18/0.42 | p(V335) % 0.18/0.42 | -p(V336) ) % 0.18/0.42 & ( p(V83) % 0.18/0.42 | p(V358) ) % 0.18/0.42 & ( -p(V67) % 0.18/0.42 | -p(V295) % 0.18/0.42 | p(V294) ) % 0.18/0.42 & ( p(V181) % 0.18/0.42 | -p(V180) ) % 0.18/0.42 & ( -p(V379) % 0.18/0.42 | p(V340) ) % 0.18/0.42 & ( p(V107) % 0.18/0.42 | p(V247) ) % 0.18/0.42 & ( -p(V100) % 0.18/0.42 | p(V164) ) % 0.18/0.42 & ( p(V288) % 0.18/0.42 | p(V109) ) % 0.18/0.42 & ( -p(V383) % 0.18/0.42 | p(V275) ) % 0.18/0.42 & ( -p(V381) % 0.18/0.42 | p(V325) ) % 0.18/0.42 & ( -p(V320) % 0.18/0.42 | p(V80) ) % 0.18/0.42 & ( -p(V314) % 0.18/0.42 | -p(V57) ) % 0.18/0.42 & ( p(V380) % 0.18/0.42 | -p(V331) ) % 0.18/0.42 & ( p(V159) % 0.18/0.42 | p(V96) ) % 0.18/0.42 & ( p(V115) % 0.18/0.42 | p(V369) ) % 0.18/0.42 & ( p(V371) % 0.18/0.42 | p(V114) ) % 0.18/0.42 & ( -p(V220) % 0.18/0.42 | -p(V29) ) % 0.18/0.42 & ( p(V364) % 0.18/0.42 | -p(V363) ) % 0.18/0.42 & ( p(V101) % 0.18/0.42 | p(V194) ) % 0.18/0.42 & ( -p(V43) % 0.18/0.42 | -p(V264) ) % 0.18/0.42 & ( -p(V44) % 0.18/0.42 | -p(V250) ) % 0.18/0.42 & ( p(V121) % 0.18/0.42 | -p(V391) ) % 0.18/0.42 & ( -p(V226) % 0.18/0.42 | -p(V32) ) % 0.18/0.42 & ( -p(V375) % 0.18/0.42 | p(V376) ) % 0.18/0.42 & ( p(V20) % 0.18/0.42 | p(V28) % 0.18/0.42 | -p(V137) ) % 0.18/0.42 & ( p(V304) % 0.18/0.42 | -p(V381) ) % 0.18/0.42 & ( -p(V305) % 0.18/0.42 | -p(V58) ) % 0.18/0.42 & ( -p(V342) % 0.18/0.42 | p(V343) ) % 0.18/0.42 & ( p(V287) % 0.18/0.42 | -p(V290) ) % 0.18/0.42 & ( -p(V212) % 0.18/0.42 | -p(V29) ) % 0.18/0.42 & ( p(V272) % 0.18/0.42 | -p(V383) ) % 0.18/0.42 & ( p(V168) % 0.18/0.42 | -p(V169) % 0.18/0.42 | -p(V26) ) % 0.18/0.42 & ( p(V237) % 0.18/0.42 | p(V102) ) % 0.18/0.42 & ( -p(V385) % 0.18/0.42 | p(V219) ) % 0.18/0.42 & ( -p(V101) % 0.18/0.42 | -p(V100) % 0.18/0.42 | -p(V16) % 0.18/0.42 | -p(V165) % 0.18/0.42 | p(V99) ) % 0.18/0.42 & ( -p(V94) % 0.18/0.42 | -p(V1) % 0.18/0.42 | -p(V117) ) % 0.18/0.42 & ( -p(V110) % 0.18/0.42 | -p(V59) % 0.18/0.42 | -p(V108) % 0.18/0.42 | -p(V287) % 0.18/0.42 | p(V109) ) % 0.18/0.42 & ( -p(V179) % 0.18/0.42 | -p(V18) ) % 0.18/0.42 & ( -p(V267) % 0.18/0.42 | -p(V47) ) % 0.18/0.42 & ( -p(V105) % 0.18/0.42 | p(V276) ) % 0.18/0.42 & ( p(V110) % 0.18/0.42 | -p(V108) % 0.18/0.42 | -p(V285) % 0.18/0.42 | -p(V109) % 0.18/0.42 | -p(V61) ) % 0.18/0.42 & ( -p(V74) % 0.18/0.42 | -p(V341) ) % 0.18/0.42 & ( p(V102) % 0.18/0.42 | p(V103) % 0.18/0.42 | -p(V104) % 0.18/0.42 | -p(V235) ) % 0.18/0.42 & ( -p(V364) % 0.18/0.42 | p(V365) ) % 0.18/0.42 & ( p(V244) % 0.18/0.42 | p(V47) ) % 0.18/0.42 & ( p(V99) % 0.18/0.42 | p(V200) ) % 0.18/0.42 & ( p(V156) % 0.18/0.42 | -p(V27) ) % 0.18/0.42 & ( p(V45) % 0.18/0.42 | p(V47) % 0.18/0.42 | p(V43) % 0.18/0.42 | p(V44) % 0.18/0.42 | p(V46) % 0.18/0.42 | p(V267) ) % 0.18/0.42 & ( p(V80) % 0.18/0.42 | p(V333) ) % 0.18/0.42 & ( p(V33) % 0.18/0.42 | p(V30) % 0.18/0.42 | p(V31) % 0.18/0.42 | p(V29) % 0.18/0.42 | p(V209) % 0.18/0.42 | p(V32) ) % 0.18/0.42 & ( p(V17) % 0.18/0.42 | p(V153) % 0.18/0.42 | -p(V154) ) % 0.18/0.42 & ( p(V59) % 0.18/0.42 | p(V302) % 0.18/0.42 | p(V60) % 0.18/0.42 | p(V61) % 0.18/0.42 | p(V57) % 0.18/0.42 | p(V58) ) % 0.18/0.42 & ( p(V325) % 0.18/0.42 | -p(V324) ) % 0.18/0.42 & ( -p(V226) % 0.18/0.42 | -p(V30) ) % 0.18/0.42 & ( -p(V15) % 0.18/0.42 | -p(V185) ) % 0.18/0.42 & ( -p(V139) % 0.18/0.42 | -p(V140) % 0.18/0.42 | p(V141) % 0.18/0.42 | -p(V138) % 0.18/0.42 | -p(V25) % 0.18/0.42 | -p(V137) % 0.18/0.42 | -p(V19) ) % 0.18/0.42 & ( p(V248) % 0.18/0.42 | p(V107) ) % 0.18/0.42 & ( p(V238) % 0.18/0.42 | -p(V55) ) % 0.18/0.42 & ( p(V330) % 0.18/0.42 | -p(V331) ) % 0.18/0.42 & ( p(V166) % 0.18/0.42 | p(V100) ) % 0.18/0.42 & ( p(V139) % 0.18/0.42 | -p(V141) ) % 0.18/0.42 & ( -p(V240) % 0.18/0.42 | p(V52) % 0.18/0.42 | p(V239) ) % 0.18/0.42 & ( p(V384) % 0.18/0.42 | -p(V249) ) % 0.18/0.42 & ( -p(V90) % 0.18/0.42 | p(V368) ) % 0.18/0.42 & ( -p(V79) % 0.18/0.42 | p(V325) ) % 0.18/0.42 & ( p(V163) % 0.18/0.42 | p(V101) ) % 0.18/0.42 & ( p(V72) % 0.18/0.42 | p(V71) % 0.18/0.42 | p(V73) % 0.18/0.42 | p(V74) % 0.18/0.42 | p(V335) ) % 0.18/0.42 & ( -p(V259) % 0.18/0.42 | p(V255) ) % 0.18/0.42 & ( p(V72) % 0.18/0.42 | -p(V316) % 0.18/0.42 | p(V315) ) % 0.18/0.42 & ( -p(V7) % 0.18/0.42 | -p(V135) ) % 0.18/0.42 & ( -p(V300) % 0.18/0.42 | p(V298) ) % 0.18/0.42 & ( -p(V53) % 0.18/0.42 | p(V253) % 0.18/0.42 | -p(V254) ) % 0.18/0.42 & ( -p(V96) % 0.18/0.42 | -p(V97) % 0.18/0.42 | -p(V98) % 0.18/0.42 | -p(V159) ) % 0.18/0.42 & ( p(V388) % 0.18/0.42 | -p(V387) ) % 0.18/0.42 & ( -p(V233) % 0.18/0.42 | p(V232) % 0.18/0.42 | -p(V34) ) % 0.18/0.42 & ( -p(V83) % 0.18/0.42 | -p(V363) ) % 0.18/0.42 & ( p(V165) % 0.18/0.42 | p(V101) ) % 0.18/0.42 & ( -p(V88) % 0.18/0.42 | p(V353) ) % 0.18/0.42 & ( -p(V161) % 0.18/0.42 | -p(V28) % 0.18/0.42 | -p(V27) ) % 0.18/0.42 & ( p(V94) % 0.18/0.42 | p(V117) ) % 0.18/0.42 & ( -p(V220) % 0.18/0.42 | -p(V31) ) % 0.18/0.42 & ( p(V40) % 0.18/0.42 | p(V210) ) % 0.18/0.42 & ( -p(V267) % 0.18/0.42 | -p(V43) ) % 0.18/0.42 & ( p(V382) % 0.18/0.42 | -p(V381) ) % 0.18/0.42 & ( -p(V247) % 0.18/0.42 | p(V249) % 0.18/0.42 | -p(V248) % 0.18/0.42 | -p(V245) % 0.18/0.42 | -p(V246) % 0.18/0.42 | -p(V244) ) % 0.18/0.42 & ( p(V268) % 0.18/0.42 | p(V50) ) % 0.18/0.42 & ( p(V196) % 0.18/0.42 | p(V99) ) % 0.18/0.42 & ( p(V333) % 0.18/0.42 | p(V89) % 0.18/0.42 | -p(V334) ) % 0.18/0.42 & ( p(V86) % 0.18/0.42 | p(V364) ) % 0.18/0.42 & ( p(V74) % 0.18/0.42 | p(V327) ) % 0.18/0.42 & ( p(V126) % 0.18/0.42 | -p(V11) ) % 0.18/0.42 & ( p(V173) % 0.18/0.42 | -p(V177) ) % 0.18/0.42 & ( -p(V84) % 0.18/0.42 | -p(V360) ) % 0.18/0.42 & ( p(V85) % 0.18/0.42 | p(V367) ) % 0.18/0.42 & ( -p(V387) % 0.18/0.42 | p(V181) ) % 0.18/0.42 & ( p(V385) % 0.18/0.42 | p(V208) % 0.18/0.42 | -p(V386) ) % 0.18/0.42 & ( p(V19) % 0.18/0.42 | -p(V141) ) % 0.18/0.42 & ( -p(V294) % 0.18/0.42 | -p(V57) ) % 0.18/0.42 & ( -p(V186) % 0.18/0.42 | -p(V22) % 0.18/0.42 | p(V185) ) % 0.18/0.42 & ( p(V357) % 0.18/0.42 | p(V115) ) % 0.18/0.42 & ( p(V92) % 0.18/0.42 | p(V373) ) % 0.18/0.42 & ( -p(V369) % 0.18/0.42 | -p(V115) % 0.18/0.42 | p(V114) ) % 0.18/0.42 & ( p(V324) % 0.18/0.42 | p(V109) ) % 0.18/0.42 & ( p(V88) % 0.18/0.42 | p(V356) ) % 0.18/0.42 & ( -p(V80) % 0.18/0.42 | -p(V81) % 0.18/0.42 | p(V320) ) % 0.18/0.42 & ( p(V361) % 0.18/0.42 | p(V92) % 0.18/0.42 | -p(V362) ) % 0.18/0.42 & ( p(V132) % 0.18/0.42 | p(V97) ) % 0.18/0.42 & ( p(V63) % 0.18/0.42 | -p(V269) % 0.18/0.42 | p(V268) ) % 0.18/0.42 & ( -p(V146) % 0.18/0.42 | -p(V6) ) % 0.18/0.42 & ( p(V98) % 0.18/0.42 | p(V132) ) % 0.18/0.42 & ( p(V233) % 0.18/0.42 | p(V34) ) % 0.18/0.42 & ( p(V323) % 0.18/0.42 | -p(V381) ) % 0.18/0.42 & ( p(V5) % 0.18/0.42 | p(V149) % 0.18/0.42 | p(V4) % 0.18/0.42 | p(V7) % 0.18/0.42 | p(V6) ) % 0.18/0.42 & ( -p(V263) % 0.18/0.42 | p(V69) % 0.18/0.42 | p(V262) ) % 0.18/0.42 & ( p(V55) % 0.18/0.42 | p(V221) % 0.18/0.42 | -p(V222) ) % 0.18/0.42 & ( -p(V259) % 0.18/0.42 | p(V61) ) % 0.18/0.42 & ( -p(V59) % 0.18/0.42 | p(V283) ) % 0.18/0.42 & ( -p(V196) % 0.18/0.42 | p(V197) ) % 0.18/0.42 & ( -p(V345) % 0.18/0.42 | p(V346) ) % 0.18/0.42 & ( p(V7) % 0.18/0.42 | p(V5) % 0.18/0.42 | p(V4) % 0.18/0.42 | p(V6) % 0.18/0.42 | p(V135) ) % 0.18/0.42 & ( -p(V389) % 0.18/0.42 | p(V151) ) % 0.18/0.42 & ( p(V243) % 0.18/0.42 | p(V56) ) % 0.18/0.42 & ( -p(V73) % 0.18/0.42 | -p(V347) ) % 0.18/0.42 & ( p(V8) % 0.18/0.42 | p(V153) ) % 0.18/0.42 & ( p(V95) % 0.18/0.42 | p(V121) ) % 0.18/0.42 & ( p(V12) % 0.18/0.42 | p(V136) ) % 0.18/0.42 & ( p(V4) % 0.18/0.42 | p(V6) % 0.18/0.42 | p(V5) % 0.18/0.42 | p(V7) % 0.18/0.42 | p(V152) ) % 0.18/0.42 & ( p(V382) % 0.18/0.42 | -p(V383) ) % 0.18/0.42 & ( -p(V24) % 0.18/0.42 | -p(V180) % 0.18/0.42 | p(V179) ) % 0.18/0.42 & ( -p(V385) % 0.18/0.42 | p(V243) ) % 0.18/0.42 & ( p(V301) % 0.18/0.42 | -p(V381) ) % 0.18/0.42 & ( -p(V106) % 0.18/0.42 | p(V278) ) % 0.18/0.42 & ( p(V81) % 0.18/0.42 | -p(V320) ) % 0.18/0.42 & ( -p(V387) % 0.18/0.42 | p(V190) ) % 0.18/0.42 & ( -p(V45) % 0.18/0.42 | p(V234) ) % 0.18/0.42 & ( -p(V359) % 0.18/0.42 | p(V378) ) % 0.18/0.42 & ( -p(V77) % 0.18/0.42 | p(V341) % 0.18/0.42 | -p(V342) ) % 0.18/0.42 & ( p(V83) % 0.18/0.42 | p(V84) % 0.18/0.42 | p(V363) ) % 0.18/0.42 & ( -p(V385) % 0.18/0.42 | p(V234) ) % 0.18/0.42 & ( -p(V314) % 0.18/0.42 | -p(V61) ) % 0.18/0.42 & ( -p(V332) % 0.18/0.42 | p(V333) ) % 0.18/0.42 & ( -p(V46) % 0.18/0.42 | -p(V264) ) % 0.18/0.42 & ( p(V219) % 0.18/0.42 | -p(V218) ) % 0.18/0.42 & ( -p(V277) % 0.18/0.42 | p(V70) % 0.18/0.42 | p(V276) ) % 0.18/0.42 & ( p(V137) % 0.18/0.42 | -p(V20) ) % 0.18/0.42 & ( p(V103) % 0.18/0.42 | -p(V104) % 0.18/0.42 | -p(V237) % 0.18/0.42 | -p(V102) ) % 0.18/0.42 & ( -p(V249) % 0.18/0.42 | p(V246) ) % 0.18/0.42 & ( p(V73) % 0.18/0.42 | p(V72) % 0.18/0.42 | p(V74) % 0.18/0.42 | p(V338) % 0.18/0.42 | p(V71) ) % 0.18/0.42 & ( p(V257) % 0.18/0.42 | -p(V57) ) % 0.18/0.42 & ( p(V272) % 0.18/0.42 | -p(V271) ) % 0.18/0.42 & ( -p(V29) % 0.18/0.42 | -p(V209) ) % 0.18/0.42 & ( -p(V209) % 0.18/0.42 | -p(V30) ) % 0.18/0.42 & ( p(V362) % 0.18/0.42 | -p(V361) ) % 0.18/0.42 & ( -p(V167) % 0.18/0.42 | p(V164) ) % 0.18/0.42 & ( -p(V78) % 0.18/0.42 | p(V299) ) % 0.18/0.42 & ( -p(V377) % 0.18/0.42 | p(V362) ) % 0.18/0.42 & ( -p(V266) % 0.18/0.42 | p(V68) % 0.18/0.42 | p(V265) ) % 0.18/0.42 & ( -p(V92) % 0.18/0.42 | p(V370) ) % 0.18/0.42 & ( -p(V143) % 0.18/0.42 | -p(V4) ) % 0.18/0.42 & ( p(V162) % 0.18/0.42 | p(V19) ) % 0.18/0.42 & ( p(V108) % 0.18/0.42 | -p(V109) % 0.18/0.42 | -p(V110) % 0.18/0.42 | -p(V288) % 0.18/0.42 | -p(V58) ) % 0.18/0.42 & ( -p(V188) % 0.18/0.42 | -p(V19) ) % 0.18/0.42 & ( -p(V346) % 0.18/0.42 | p(V345) % 0.18/0.42 | p(V84) ) % 0.18/0.42 & ( -p(V5) % 0.18/0.42 | -p(V143) ) % 0.18/0.42 & ( -p(V73) % 0.18/0.42 | -p(V332) ) % 0.18/0.42 & ( p(V205) % 0.18/0.42 | p(V102) ) % 0.18/0.42 & ( p(V166) % 0.18/0.42 | p(V15) ) % 0.18/0.42 & ( -p(V209) % 0.18/0.42 | -p(V33) ) % 0.18/0.42 & ( p(V99) % 0.18/0.42 | -p(V101) % 0.18/0.42 | -p(V100) % 0.18/0.42 | -p(V198) ) % 0.18/0.42 & ( p(V157) % 0.18/0.42 | p(V97) ) % 0.18/0.42 & ( -p(V80) % 0.18/0.42 | -p(V333) % 0.18/0.42 | p(V332) ) % 0.18/0.42 & ( p(V285) % 0.18/0.42 | p(V109) ) % 0.18/0.42 & ( p(V269) % 0.18/0.42 | -p(V268) ) % 0.18/0.42 & ( -p(V143) % 0.18/0.42 | p(V144) ) % 0.18/0.42 & ( -p(V389) % 0.18/0.42 | p(V148) ) % 0.18/0.42 & ( -p(V66) % 0.18/0.42 | p(V281) ) % 0.18/0.42 & ( p(V128) % 0.18/0.42 | -p(V122) ) % 0.18/0.42 & ( p(V112) % 0.18/0.42 | p(V354) ) % 0.18/0.42 & ( -p(V291) % 0.18/0.42 | -p(V61) ) % 0.18/0.42 & ( p(V61) % 0.18/0.42 | p(V58) % 0.18/0.42 | p(V60) % 0.18/0.42 | p(V59) % 0.18/0.42 | p(V57) % 0.18/0.42 | p(V294) ) % 0.18/0.42 & ( -p(V140) % 0.18/0.42 | p(V23) % 0.18/0.42 | p(V17) ) % 0.18/0.42 & ( p(V270) % 0.18/0.42 | p(V43) % 0.18/0.42 | p(V47) % 0.18/0.42 | p(V46) % 0.18/0.42 | p(V44) % 0.18/0.42 | p(V45) ) % 0.18/0.42 & ( p(V60) % 0.18/0.42 | p(V58) % 0.18/0.42 | p(V59) % 0.18/0.42 | p(V311) % 0.18/0.42 | p(V61) % 0.18/0.42 | p(V57) ) % 0.18/0.42 & ( -p(V290) % 0.18/0.42 | p(V286) ) % 0.18/0.42 & ( -p(V354) % 0.18/0.42 | p(V355) ) % 0.18/0.42 & ( -p(V111) % 0.18/0.42 | p(V327) ) % 0.18/0.42 & ( -p(V99) % 0.18/0.42 | p(V194) ) % 0.18/0.42 & ( -p(V391) % 0.18/0.42 | p(V128) ) % 0.18/0.42 & ( -p(V44) % 0.18/0.42 | -p(V267) ) % 0.18/0.42 & ( -p(V387) % 0.18/0.42 | p(V199) ) % 0.18/0.42 & ( p(V123) % 0.18/0.42 | -p(V14) ) % 0.18/0.42 & ( -p(V218) % 0.18/0.42 | p(V214) ) % 0.18/0.42 & ( p(V195) % 0.18/0.42 | -p(V194) ) % 0.18/0.42 & ( p(V44) % 0.18/0.42 | p(V46) % 0.18/0.42 | p(V273) % 0.18/0.42 | p(V43) % 0.18/0.42 | p(V45) % 0.18/0.42 | p(V47) ) % 0.18/0.42 & ( p(V297) % 0.18/0.42 | -p(V81) ) % 0.18/0.42 & ( p(V27) % 0.18/0.42 | -p(V156) % 0.18/0.42 | p(V155) ) % 0.18/0.42 & ( p(V100) % 0.18/0.42 | p(V165) ) % 0.18/0.42 & ( p(V46) % 0.18/0.42 | p(V245) ) % 0.18/0.42 & ( p(V110) % 0.18/0.42 | p(V286) ) % 0.18/0.42 & ( -p(V108) % 0.18/0.42 | p(V322) ) % 0.18/0.42 & ( -p(V177) % 0.18/0.42 | p(V33) ) % 0.18/0.42 & ( -p(V84) % 0.18/0.42 | p(V346) ) % 0.18/0.42 & ( p(V255) % 0.18/0.42 | -p(V62) ) % 0.18/0.42 & ( p(V308) % 0.18/0.42 | p(V60) % 0.18/0.42 | p(V61) % 0.18/0.42 | p(V59) % 0.18/0.42 | p(V58) % 0.18/0.42 | p(V57) ) % 0.18/0.42 & ( p(V195) % 0.18/0.42 | -p(V387) ) % 0.18/0.42 & ( -p(V26) % 0.18/0.42 | p(V145) ) % 0.18/0.42 & ( p(V306) % 0.18/0.42 | p(V65) ) % 0.18/0.42 & ( p(V174) % 0.18/0.42 | -p(V41) ) % 0.18/0.42 & ( p(V200) % 0.18/0.42 | p(V29) % 0.18/0.42 | -p(V201) ) % 0.18/0.42 & ( -p(V291) % 0.18/0.42 | -p(V59) ) % 0.18/0.42 & ( -p(V15) % 0.18/0.42 | -p(V188) ) % 0.18/0.42 & ( p(V393) % 0.18/0.42 | p(V117) % 0.18/0.42 | -p(V394) ) % 0.18/0.42 & ( -p(V48) % 0.18/0.42 | p(V214) ) % 0.18/0.42 & ( -p(V379) % 0.18/0.42 | p(V337) ) % 0.18/0.42 & ( p(V355) % 0.18/0.42 | -p(V86) ) % 0.18/0.42 & ( p(V202) % 0.18/0.42 | p(V41) ) % 0.18/0.42 & ( -p(V393) % 0.18/0.42 | p(V119) ) % 0.18/0.42 & ( -p(V347) % 0.18/0.42 | -p(V74) ) % 0.18/0.42 & ( p(V42) % 0.18/0.42 | p(V202) ) % 0.18/0.42 & ( -p(V47) % 0.18/0.42 | -p(V273) ) % 0.18/0.42 & ( p(V329) % 0.18/0.42 | p(V112) ) % 0.18/0.42 & ( -p(V377) % 0.18/0.42 | p(V378) ) % 0.18/0.42 & ( -p(V56) % 0.18/0.42 | p(V236) ) % 0.18/0.42 & ( p(V162) % 0.18/0.42 | -p(V167) ) % 0.18/0.42 & ( -p(V30) % 0.18/0.42 | -p(V229) ) % 0.18/0.42 & ( -p(V231) % 0.18/0.42 | p(V46) % 0.18/0.42 | p(V230) ) % 0.18/0.42 & ( -p(V100) % 0.18/0.42 | p(V163) ) % 0.18/0.42 & ( -p(V45) % 0.18/0.42 | -p(V264) ) % 0.18/0.42 & ( p(V196) % 0.18/0.42 | -p(V100) ) % 0.18/0.42 & ( -p(V179) % 0.18/0.42 | -p(V16) ) % 0.18/0.42 & ( -p(V30) % 0.18/0.42 | -p(V223) ) % 0.18/0.42 & ( p(V110) % 0.18/0.42 | p(V287) ) % 0.18/0.42 & ( -p(V59) % 0.18/0.42 | -p(V302) ) % 0.18/0.42 & ( p(V298) % 0.18/0.42 | -p(V71) ) % 0.18/0.42 & p(V395) % 0.18/0.42 & ( -p(V32) % 0.18/0.42 | p(V190) ) % 0.18/0.42 & ( -p(V83) % 0.18/0.42 | p(V349) ) % 0.18/0.42 & ( p(V172) % 0.18/0.42 | p(V25) ) % 0.18/0.42 & ( p(V100) % 0.18/0.42 | p(V198) ) % 0.18/0.42 & ( p(V31) % 0.18/0.42 | p(V205) ) % 0.18/0.42 & ( p(V205) % 0.18/0.42 | -p(V103) ) % 0.18/0.42 & ( -p(V18) % 0.18/0.42 | -p(V168) ) % 0.18/0.42 & ( p(V33) % 0.18/0.42 | p(V30) % 0.18/0.42 | p(V32) % 0.18/0.43 | p(V232) % 0.18/0.43 | p(V29) % 0.18/0.43 | p(V31) ) % 0.18/0.43 & ( p(V95) % 0.18/0.43 | p(V120) ) % 0.18/0.43 & ( -p(V16) % 0.18/0.43 | -p(V185) ) % 0.18/0.43 & ( -p(V146) % 0.18/0.43 | p(V147) ) % 0.18/0.43 & ( -p(V97) % 0.18/0.43 | p(V155) ) % 0.18/0.43 & ( p(V220) % 0.18/0.43 | -p(V221) % 0.18/0.43 | -p(V38) ) % 0.18/0.43 & ( -p(V270) % 0.18/0.43 | p(V271) ) % 0.18/0.43 & ( p(V351) % 0.18/0.43 | -p(V350) ) % 0.18/0.43 & ( -p(V118) % 0.18/0.43 | p(V2) ) % 0.18/0.43 & ( -p(V104) % 0.18/0.43 | -p(V30) % 0.18/0.43 | -p(V206) % 0.18/0.43 | p(V102) % 0.18/0.43 | -p(V103) ) % 0.18/0.43 & ( -p(V99) % 0.18/0.43 | p(V198) ) % 0.18/0.43 & ( -p(V328) % 0.18/0.43 | -p(V329) % 0.18/0.43 | p(V331) % 0.18/0.43 | -p(V330) % 0.18/0.43 | -p(V327) ) % 0.18/0.43 & ( p(V240) % 0.18/0.43 | -p(V385) ) % 0.18/0.43 & ( p(V262) % 0.18/0.43 | -p(V261) ) % 0.18/0.43 & ( p(V337) % 0.18/0.43 | -p(V336) ) % 0.18/0.43 & ( p(V266) % 0.18/0.43 | -p(V383) ) % 0.18/0.43 & ( -p(V37) % 0.18/0.43 | p(V176) ) % 0.18/0.43 & ( -p(V232) % 0.18/0.43 | -p(V33) ) % 0.18/0.43 & ( p(V247) % 0.18/0.43 | p(V44) ) % 0.18/0.43 & ( -p(V209) % 0.18/0.43 | -p(V31) ) % 0.18/0.43 & ( p(V299) % 0.18/0.43 | -p(V72) ) % 0.18/0.43 & ( p(V49) % 0.18/0.43 | p(V227) % 0.18/0.43 | -p(V228) ) % 0.18/0.43 & ( -p(V89) % 0.18/0.43 | p(V351) ) % 0.18/0.43 & ( -p(V392) % 0.18/0.43 | p(V120) % 0.18/0.43 | p(V391) ) % 0.18/0.43 & ( p(V114) % 0.18/0.43 | -p(V357) % 0.18/0.43 | -p(V84) % 0.18/0.43 | -p(V115) ) % 0.18/0.43 & ( p(V107) % 0.18/0.43 | p(V278) ) % 0.18/0.43 & ( -p(V208) % 0.18/0.43 | p(V386) ) % 0.18/0.43 & ( -p(V389) % 0.18/0.43 | p(V160) ) % 0.18/0.43 & ( -p(V111) % 0.18/0.43 | p(V329) ) % 0.18/0.43 & ( -p(V65) % 0.18/0.43 | p(V258) ) % 0.18/0.43 & ( -p(V147) % 0.18/0.43 | -p(V10) % 0.18/0.43 | p(V146) ) % 0.18/0.43 & ( -p(V106) % 0.18/0.43 | p(V105) % 0.18/0.43 | -p(V280) % 0.18/0.43 | -p(V107) ) % 0.18/0.43 & ( p(V236) % 0.18/0.43 | -p(V385) ) % 0.18/0.43 & ( p(V103) % 0.18/0.43 | p(V207) ) % 0.18/0.43 & ( p(V361) % 0.18/0.43 | p(V87) ) % 0.18/0.43 & ( -p(V344) % 0.18/0.43 | -p(V73) ) % 0.18/0.43 & ( -p(V392) % 0.18/0.43 | -p(V119) % 0.18/0.43 | p(V393) ) % 0.18/0.43 & ( p(V84) % 0.18/0.43 | p(V366) % 0.18/0.43 | p(V83) ) % 0.18/0.43 & ( p(V292) % 0.18/0.43 | p(V82) % 0.18/0.43 | -p(V293) ) % 0.18/0.43 & ( p(V390) % 0.18/0.43 | -p(V391) ) % 0.18/0.43 & ( -p(V8) % 0.18/0.43 | p(V123) ) % 0.18/0.43 & ( p(V165) % 0.18/0.43 | p(V16) ) % 0.18/0.43 & ( -p(V212) % 0.18/0.43 | -p(V31) ) % 0.18/0.43 & ( p(V323) % 0.18/0.43 | -p(V81) ) % 0.18/0.43 & ( -p(V176) % 0.18/0.43 | -p(V39) % 0.18/0.43 | -p(V173) % 0.18/0.43 | -p(V33) % 0.18/0.43 | -p(V175) % 0.18/0.43 | -p(V174) % 0.18/0.43 | p(V177) ) % 0.18/0.43 & ( p(V281) % 0.18/0.43 | -p(V280) ) % 0.18/0.43 & ( -p(V191) % 0.18/0.43 | -p(V18) ) % 0.18/0.43 & ( p(V322) % 0.18/0.43 | -p(V323) % 0.18/0.43 | p(V81) ) % 0.18/0.43 & ( -p(V195) % 0.18/0.43 | p(V42) % 0.18/0.43 | p(V194) ) % 0.18/0.43 & ( -p(V302) % 0.18/0.43 | -p(V61) ) % 0.18/0.43 & ( -p(V188) % 0.18/0.43 | -p(V16) ) % 0.18/0.43 & ( -p(V253) % 0.18/0.43 | -p(V44) ) % 0.18/0.43 & ( p(V59) % 0.18/0.43 | p(V61) % 0.18/0.43 | p(V57) % 0.18/0.43 | p(V60) % 0.18/0.43 | p(V291) % 0.18/0.43 | p(V58) ) % 0.18/0.43 & ( p(V2) % 0.18/0.43 | -p(V118) ) % 0.18/0.43 & ( -p(V109) % 0.18/0.43 | p(V287) ) % 0.18/0.43 & ( -p(V211) % 0.18/0.43 | p(V210) % 0.18/0.43 | p(V56) ) % 0.18/0.43 & ( -p(V264) % 0.18/0.43 | p(V265) ) % 0.18/0.43 & ( -p(V114) % 0.18/0.43 | p(V357) ) % 0.18/0.43 & ( -p(V276) % 0.18/0.43 | p(V277) ) % 0.18/0.43 & ( p(V342) % 0.18/0.43 | -p(V343) % 0.18/0.43 | p(V85) ) % 0.18/0.43 & ( p(V226) % 0.18/0.43 | -p(V227) % 0.18/0.43 | -p(V36) ) % 0.18/0.43 & ( -p(V47) % 0.18/0.43 | -p(V253) ) % 0.18/0.43 & ( -p(V144) % 0.18/0.43 | p(V145) ) % 0.18/0.43 & ( -p(V70) % 0.18/0.43 | p(V255) ) % 0.18/0.43 & ( -p(V54) % 0.18/0.43 | -p(V251) % 0.18/0.43 | p(V250) ) % 0.18/0.43 & ( -p(V161) % 0.18/0.43 | -p(V154) % 0.18/0.43 | -p(V142) % 0.18/0.43 | -p(V156) % 0.18/0.43 | -p(V160) % 0.18/0.43 | -p(V151) % 0.18/0.43 | p(V389) % 0.18/0.43 | -p(V158) % 0.18/0.43 | -p(V388) % 0.18/0.43 | -p(V145) % 0.18/0.43 | -p(V148) ) % 0.18/0.43 & ( p(V10) % 0.18/0.43 | p(V147) ) % 0.18/0.43 & ( -p(V332) % 0.18/0.43 | -p(V72) ) % 0.18/0.43 & ( p(V251) % 0.18/0.43 | -p(V250) ) % 0.18/0.43 & ( -p(V70) % 0.18/0.43 | p(V252) ) % 0.18/0.43 & ( p(V241) % 0.18/0.43 | p(V104) ) % 0.18/0.43 & ( -p(V364) % 0.18/0.43 | p(V363) % 0.18/0.43 | -p(V86) ) % 0.18/0.43 & ( p(V75) % 0.18/0.43 | p(V348) ) % 0.18/0.43 & ( p(V71) % 0.18/0.43 | p(V77) % 0.18/0.43 | -p(V298) ) % 0.18/0.43 & ( p(V216) % 0.18/0.43 | -p(V44) ) % 0.18/0.43 & ( -p(V250) % 0.18/0.43 | -p(V47) ) % 0.18/0.43 & ( -p(V99) % 0.18/0.43 | p(V163) ) % 0.18/0.43 & ( -p(V382) % 0.18/0.43 | -p(V269) % 0.18/0.43 | -p(V252) % 0.18/0.43 | -p(V275) % 0.18/0.43 | -p(V260) % 0.18/0.43 | -p(V263) % 0.18/0.43 | -p(V284) % 0.18/0.43 | -p(V272) % 0.18/0.43 | p(V383) % 0.18/0.43 | -p(V283) % 0.18/0.43 | -p(V279) % 0.18/0.43 | -p(V281) % 0.18/0.43 | -p(V277) % 0.18/0.43 | -p(V266) ) % 0.18/0.43 & ( p(V297) % 0.18/0.43 | -p(V300) ) % 0.18/0.43 & ( -p(V185) % 0.18/0.43 | p(V186) ) % 0.18/0.43 & ( p(V45) % 0.18/0.43 | p(V246) ) % 0.18/0.43 & ( -p(V253) % 0.18/0.43 | -p(V46) ) % 0.18/0.43 & ( p(V21) % 0.18/0.43 | p(V27) % 0.18/0.43 | -p(V138) ) % 0.18/0.43 & ( -p(V317) % 0.18/0.43 | -p(V110) % 0.18/0.43 | p(V108) % 0.18/0.43 | p(V109) ) % 0.18/0.43 & ( p(V31) % 0.18/0.43 | -p(V193) % 0.18/0.43 | p(V192) ) % 0.18/0.43 & ( -p(V75) % 0.18/0.43 | -p(V348) % 0.18/0.43 | p(V347) ) % 0.18/0.43 & ( -p(V249) % 0.18/0.43 | p(V248) ) % 0.18/0.43 & ( p(V248) % 0.18/0.43 | p(V105) ) % 0.18/0.43 & ( -p(V152) % 0.18/0.43 | -p(V7) ) % 0.18/0.43 & ( -p(V153) % 0.18/0.43 | p(V154) ) % 0.18/0.43 & ( -p(V377) % 0.18/0.43 | p(V376) ) % 0.18/0.43 & ( -p(V389) % 0.18/0.43 | p(V388) ) % 0.18/0.43 & ( p(V288) % 0.18/0.43 | p(V110) ) % 0.18/0.43 & ( -p(V259) % 0.18/0.43 | p(V260) ) % 0.18/0.43 & ( p(V224) % 0.18/0.43 | -p(V223) ) % 0.18/0.43 & ( p(V285) % 0.18/0.43 | -p(V290) ) % 0.18/0.43 & ( -p(V58) % 0.18/0.43 | -p(V294) ) % 0.18/0.43 & ( p(V105) % 0.18/0.43 | -p(V107) % 0.18/0.43 | -p(V106) % 0.18/0.43 | -p(V247) % 0.18/0.43 | -p(V44) ) % 0.18/0.43 & ( -p(V393) % 0.18/0.43 | p(V394) ) % 0.18/0.43 & ( -p(V338) % 0.18/0.43 | -p(V72) ) % 0.18/0.43 & ( -p(V30) % 0.18/0.43 | p(V175) ) % 0.18/0.43 & ( -p(V319) % 0.18/0.43 | p(V321) ) % 0.18/0.43 & ( -p(V71) % 0.18/0.43 | -p(V341) ) % 0.18/0.43 & ( p(V166) % 0.18/0.43 | -p(V167) ) % 0.18/0.43 & ( p(V109) % 0.18/0.43 | -p(V60) % 0.18/0.43 | p(V108) % 0.18/0.43 | -p(V286) % 0.18/0.43 | -p(V110) ) % 0.18/0.43 & ( -p(V303) % 0.18/0.43 | p(V304) ) % 0.18/0.43 & ( -p(V185) % 0.18/0.43 | -p(V18) ) % 0.18/0.43 & ( p(V307) % 0.18/0.43 | -p(V381) ) % 0.18/0.43 & ( p(V288) % 0.18/0.43 | p(V58) ) % 0.18/0.43 & ( -p(V124) % 0.18/0.43 | p(V13) % 0.18/0.43 | p(V9) ) % 0.18/0.43 & ( -p(V5) % 0.18/0.43 | -p(V97) % 0.18/0.43 | -p(V98) % 0.18/0.43 | -p(V132) % 0.18/0.43 | p(V96) ) % 0.18/0.43 & ( p(V102) % 0.18/0.43 | -p(V204) % 0.18/0.43 | p(V103) % 0.18/0.43 | -p(V104) % 0.18/0.43 | -p(V32) ) % 0.18/0.43 & ( p(V173) % 0.18/0.43 | -p(V42) ) % 0.18/0.43 & ( -p(V104) % 0.18/0.43 | -p(V205) % 0.18/0.43 | -p(V102) % 0.18/0.43 | -p(V31) % 0.18/0.43 | p(V103) ) % 0.18/0.43 & ( -p(V339) % 0.18/0.43 | p(V340) ) % 0.18/0.43 & ( -p(V147) % 0.18/0.43 | p(V148) ) % 0.18/0.43 & ( -p(V383) % 0.18/0.43 | p(V281) ) % 0.18/0.43 & ( -p(V68) % 0.18/0.43 | p(V291) % 0.18/0.43 | -p(V292) ) % 0.18/0.43 & ( p(V259) % 0.18/0.43 | -p(V260) % 0.18/0.43 | p(V254) ) % 0.18/0.43 & ( p(V339) % 0.18/0.43 | -p(V338) ) % 0.18/0.43 & ( p(V328) % 0.18/0.43 | p(V113) ) % 0.18/0.43 & ( -p(V267) % 0.18/0.43 | -p(V46) ) % 0.18/0.43 & ( p(V38) % 0.18/0.43 | -p(V199) % 0.18/0.43 | p(V198) ) % 0.18/0.43 & ( p(V392) % 0.18/0.43 | -p(V391) ) % 0.18/0.43 & ( p(V334) % 0.18/0.43 | -p(V89) ) % 0.18/0.43 & ( -p(V69) % 0.18/0.43 | -p(V284) % 0.18/0.43 | -p(V70) ) % 0.18/0.43 & ( p(V16) % 0.18/0.43 | p(V18) % 0.18/0.43 | p(V17) % 0.18/0.43 | p(V15) % 0.18/0.43 | p(V168) % 0.18/0.43 | p(V19) ) % 0.18/0.43 & ( p(V245) % 0.18/0.43 | -p(V106) ) % 0.18/0.43 & ( -p(V339) % 0.18/0.43 | p(V338) % 0.18/0.43 | -p(V78) ) % 0.18/0.43 & ( p(V309) % 0.18/0.43 | p(V64) ) % 0.18/0.43 & ( -p(V98) % 0.18/0.43 | -p(V96) % 0.18/0.43 | -p(V133) % 0.18/0.43 | -p(V97) % 0.18/0.43 | -p(V4) ) % 0.18/0.43 & ( p(V326) % 0.18/0.43 | p(V82) ) % 0.18/0.43 & ( p(V330) % 0.18/0.43 | p(V71) ) % 0.18/0.43 & ( -p(V171) % 0.18/0.43 | p(V172) ) % 0.18/0.43 & ( -p(V146) % 0.18/0.43 | -p(V5) ) % 0.18/0.43 & ( -p(V229) % 0.18/0.43 | -p(V32) ) % 0.18/0.43 & ( p(V353) % 0.18/0.43 | -p(V379) ) % 0.18/0.43 & ( -p(V374) % 0.18/0.43 | -p(V90) % 0.18/0.43 | -p(V116) ) % 0.18/0.43 & ( p(V155) % 0.18/0.43 | p(V96) ) % 0.18/0.43 & ( -p(V135) % 0.18/0.43 | -p(V6) ) % 0.18/0.43 & ( -p(V389) % 0.18/0.43 | p(V158) ) % 0.18/0.43 & ( p(V392) % 0.18/0.43 | -p(V393) ) % 0.18/0.43 & ( p(V358) % 0.18/0.43 | -p(V359) ) % 0.18/0.43 & ( -p(V64) % 0.18/0.43 | p(V257) ) % 0.18/0.43 & ( -p(V383) % 0.18/0.43 | p(V384) ) % 0.18/0.43 & ( -p(V372) % 0.18/0.43 | p(V91) % 0.18/0.43 | p(V371) ) % 0.18/0.43 & ( p(V38) % 0.18/0.43 | p(V221) ) % 0.18/0.43 & ( p(V180) % 0.18/0.43 | p(V24) ) % 0.18/0.43 & ( -p(V2) % 0.18/0.43 | -p(V3) % 0.18/0.43 | -p(V122) ) % 0.18/0.43 & ( p(V186) % 0.18/0.43 | p(V22) ) % 0.18/0.43 & ( -p(V215) % 0.18/0.43 | p(V55) % 0.18/0.43 | p(V49) ) % 0.18/0.43 & ( p(V46) % 0.18/0.43 | p(V47) % 0.18/0.43 | p(V44) % 0.18/0.43 | p(V45) % 0.18/0.43 | p(V253) % 0.18/0.43 | p(V43) ) % 0.18/0.43 & ( -p(V4) % 0.18/0.43 | -p(V152) ) % 0.18/0.43 & ( -p(V168) % 0.18/0.43 | -p(V17) ) % 0.18/0.43 & ( -p(V349) % 0.18/0.43 | p(V83) % 0.18/0.43 | p(V348) ) % 0.18/0.43 & ( p(V143) % 0.18/0.43 | -p(V11) % 0.18/0.43 | -p(V144) ) % 0.18/0.43 & ( p(V221) % 0.18/0.43 | -p(V220) ) % 0.18/0.43 & ( -p(V105) % 0.18/0.43 | p(V280) ) % 0.18/0.43 & ( -p(V4) % 0.18/0.43 | -p(V146) ) % 0.18/0.43 & ( p(V97) % 0.18/0.43 | p(V133) ) % 0.18/0.43 & ( -p(V118) % 0.18/0.43 | p(V3) ) % 0.18/0.43 & ( -p(V112) % 0.18/0.43 | p(V350) ) % 0.18/0.43 & ( p(V310) % 0.18/0.43 | -p(V76) ) % 0.18/0.43 & ( -p(V43) % 0.18/0.43 | -p(V250) ) % 0.18/0.43 & ( p(V231) % 0.18/0.43 | -p(V46) ) % 0.18/0.43 & ( p(V130) % 0.18/0.43 | -p(V97) ) % 0.18/0.43 & ( p(V53) % 0.18/0.43 | -p(V218) ) % 0.18/0.43 & ( -p(V94) % 0.18/0.43 | -p(V119) % 0.18/0.43 | p(V118) ) % 0.18/0.43 & ( p(V104) % 0.18/0.43 | p(V206) ) % 0.18/0.43 & ( p(V300) % 0.18/0.43 | p(V295) % 0.18/0.43 | -p(V301) ) % 0.18/0.43 & ( -p(V243) % 0.18/0.43 | -p(V56) % 0.18/0.43 | -p(V55) ) % 0.18/0.43 & ( -p(V59) % 0.18/0.43 | -p(V311) ) % 0.18/0.43 & ( -p(V307) % 0.18/0.43 | p(V306) % 0.18/0.43 | p(V80) ) % 0.18/0.43 & ( p(V375) % 0.18/0.43 | p(V374) % 0.18/0.43 | -p(V376) ) % 0.18/0.43 & ( p(V72) % 0.18/0.43 | p(V329) ) % 0.18/0.43 & ( p(V242) % 0.18/0.43 | -p(V43) ) % 0.18/0.43 & ( -p(V274) % 0.18/0.43 | p(V275) ) % 0.18/0.43 & ( p(V313) % 0.18/0.43 | -p(V73) ) % 0.18/0.43 & ( p(V138) % 0.18/0.43 | -p(V21) ) % 0.18/0.43 & ( -p(V104) % 0.18/0.43 | -p(V103) % 0.18/0.43 | -p(V241) % 0.18/0.43 | -p(V102) ) % 0.18/0.43 & ( p(V248) % 0.18/0.43 | p(V106) ) % 0.18/0.43 & ( p(V90) % 0.18/0.43 | p(V374) ) % 0.18/0.43 & ( p(V266) % 0.18/0.43 | -p(V265) ) % 0.18/0.43 & ( -p(V19) % 0.18/0.43 | -p(V182) ) % 0.18/0.43 & ( -p(V59) % 0.18/0.43 | -p(V308) ) % 0.18/0.43 & ( -p(V61) % 0.18/0.43 | -p(V294) ) % 0.18/0.43 & ( p(V342) % 0.18/0.43 | p(V77) ) % 0.18/0.43 & ( -p(V106) % 0.18/0.43 | p(V276) ) % 0.18/0.43 & ( p(V123) % 0.18/0.43 | -p(V127) ) % 0.18/0.43 & ( p(V354) % 0.18/0.43 | -p(V355) % 0.18/0.43 | p(V86) ) % 0.18/0.43 & ( p(V204) % 0.18/0.43 | -p(V103) ) % 0.18/0.43 & ( -p(V379) % 0.18/0.43 | p(V349) ) % 0.18/0.43 & ( p(V99) % 0.18/0.43 | p(V100) % 0.18/0.43 | -p(V194) % 0.18/0.43 | -p(V101) ) % 0.18/0.43 & ( p(V337) % 0.18/0.43 | -p(V88) ) % 0.18/0.43 & ( p(V233) % 0.18/0.43 | -p(V232) ) % 0.18/0.43 & ( p(V104) % 0.18/0.43 | p(V207) ) % 0.18/0.43 & ( -p(V121) % 0.18/0.43 | -p(V128) % 0.18/0.43 | -p(V390) % 0.18/0.43 | -p(V129) % 0.18/0.43 | p(V391) ) % 0.18/0.43 & ( p(V36) % 0.18/0.43 | p(V227) ) % 0.18/0.43 & ( -p(V259) % 0.18/0.43 | p(V258) ) % 0.18/0.43 & ( -p(V85) % 0.18/0.43 | p(V343) ) % 0.18/0.43 & ( -p(V17) % 0.18/0.43 | -p(V185) ) % 0.18/0.43 & ( -p(V344) % 0.18/0.43 | -p(V71) ) % 0.18/0.43 & ( -p(V179) % 0.18/0.43 | -p(V19) ) % 0.18/0.43 & ( p(V110) % 0.18/0.43 | p(V324) ) % 0.18/0.43 & ( -p(V219) % 0.18/0.43 | p(V213) % 0.18/0.43 | p(V218) ) % 0.18/0.43 & ( p(V320) % 0.18/0.43 | p(V319) % 0.18/0.43 | -p(V321) ) % 0.18/0.43 & ( p(V233) % 0.18/0.43 | -p(V234) % 0.18/0.43 | p(V45) ) % 0.18/0.43 & ( p(V285) % 0.18/0.43 | -p(V110) ) % 0.18/0.43 & ( -p(V303) % 0.18/0.43 | p(V302) % 0.18/0.43 | -p(V66) ) % 0.18/0.43 & ( p(V326) % 0.18/0.43 | p(V81) ) % 0.18/0.43 & ( -p(V109) % 0.18/0.43 | p(V319) ) % 0.18/0.43 & ( p(V252) % 0.18/0.43 | -p(V383) ) % 0.18/0.43 & ( -p(V58) % 0.18/0.43 | -p(V311) ) % 0.18/0.43 & ( p(V339) % 0.18/0.43 | p(V87) % 0.18/0.43 | -p(V340) ) % 0.18/0.43 & ( -p(V100) % 0.18/0.43 | p(V194) ) % 0.18/0.43 & ( -p(V57) % 0.18/0.43 | -p(V308) ) % 0.18/0.43 & ( p(V352) % 0.18/0.43 | p(V113) ) % 0.18/0.43 & ( p(V247) % 0.18/0.43 | -p(V249) ) % 0.18/0.43 & ( p(V314) % 0.18/0.43 | p(V61) % 0.18/0.43 | p(V57) % 0.18/0.43 | p(V60) % 0.18/0.43 | p(V59) % 0.18/0.43 | p(V58) ) % 0.18/0.43 & ( p(V206) % 0.18/0.43 | -p(V208) ) % 0.18/0.43 & ( -p(V223) % 0.18/0.43 | -p(V29) ) % 0.18/0.43 & ( -p(V164) % 0.18/0.43 | -p(V162) % 0.18/0.43 | -p(V165) % 0.18/0.43 | -p(V163) % 0.18/0.43 | -p(V166) % 0.18/0.43 | p(V167) ) % 0.18/0.43 & ( p(V330) % 0.18/0.43 | p(V112) ) % 0.18/0.43 & ( p(V112) % 0.18/0.43 | p(V352) ) % 0.18/0.43 & ( -p(V15) % 0.18/0.43 | p(V160) ) % 0.18/0.43 & ( p(V305) % 0.18/0.43 | -p(V306) % 0.18/0.43 | -p(V65) ) % 0.18/0.43 & ( -p(V262) % 0.18/0.43 | -p(V52) % 0.18/0.43 | p(V261) ) % 0.18/0.43 & ( -p(V385) % 0.18/0.43 | p(V228) ) % 0.18/0.43 & ( -p(V134) % 0.18/0.43 | p(V132) ) % 0.18/0.43 & ( -p(V229) % 0.18/0.43 | -p(V29) ) % 0.18/0.43 & ( -p(V317) % 0.18/0.43 | p(V318) ) % 0.18/0.43 & ( -p(V294) % 0.18/0.43 | -p(V59) ) % 0.18/0.43 & ( -p(V16) % 0.18/0.43 | -p(V171) ) % 0.18/0.43 & ( -p(V17) % 0.18/0.43 | -p(V191) ) % 0.18/0.43 & ( -p(V241) % 0.18/0.43 | p(V242) ) % 0.18/0.43 & ( p(V227) % 0.18/0.43 | -p(V226) ) % 0.18/0.43 & ( -p(V385) % 0.18/0.43 | p(V231) ) % 0.18/0.43 & ( -p(V273) % 0.18/0.43 | -p(V44) ) % 0.18/0.43 & ( p(V113) % 0.18/0.43 | p(V329) ) % 0.18/0.43 & ( -p(V146) % 0.18/0.43 | -p(V7) ) % 0.18/0.43 & ( -p(V73) % 0.18/0.43 | -p(V341) ) % 0.18/0.43 & ( p(V151) % 0.18/0.43 | -p(V18) ) % 0.18/0.43 & ( -p(V379) % 0.18/0.43 | p(V355) ) % 0.18/0.43 & ( p(V289) % 0.18/0.43 | -p(V290) ) % 0.18/0.43 & ( -p(V102) % 0.18/0.43 | p(V235) ) % 0.18/0.43 & ( -p(V183) % 0.18/0.43 | p(V182) % 0.18/0.43 | -p(V23) ) % 0.18/0.43 & ( -p(V139) % 0.18/0.43 | p(V16) % 0.18/0.43 | p(V22) ) % 0.18/0.43 & ( p(V14) % 0.18/0.43 | p(V129) ) % 0.18/0.43 & ( -p(V7) % 0.18/0.43 | -p(V143) ) % 0.18/0.43 & ( -p(V13) % 0.18/0.43 | -p(V129) % 0.18/0.43 | -p(V14) ) % 0.18/0.43 & ( p(V138) % 0.18/0.43 | -p(V27) ) % 0.18/0.43 & ( -p(V59) % 0.18/0.43 | -p(V314) ) % 0.18/0.43 & ( p(V57) % 0.18/0.43 | -p(V257) % 0.18/0.43 | p(V64) ) % 0.18/0.43 & ( -p(V296) % 0.18/0.43 | p(V82) % 0.18/0.43 | p(V75) ) % 0.18/0.43 & ( -p(V106) % 0.18/0.43 | -p(V107) % 0.18/0.43 | -p(V105) % 0.18/0.43 | -p(V282) ) % 0.18/0.43 & ( p(V127) % 0.18/0.43 | p(V122) % 0.18/0.43 | -p(V128) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ). % 0.18/0.43 % 0.18/0.43 ======= end of input processing ======= % 0.18/0.43 % 0.18/0.43 1 input errors were found. % 0.18/0.43 % 0.18/0.43 1 input errors were found. %------------------------------------------------------------------------------