include('Saturations/HWV082+1/Saturations/Vampire-SAT---4.7.ax').
fof(quant,conjecture,? [V15] : ? [V16] : ? [V17] : ? [V1] : ? [V2] : ? [V3] : ? [V4] : ? [V5] : ? [V6] : ? [V7] : ? [V8] : ? [V9] : ? [V10] : ? [V11] : ? [V12] : ? [V13] : ? [V14] : ? [V24] : ? [V25] : ? [V26] : ? [V27] : ? [V28] : ? [V29] : ? [V30] : ? [V31] : ? [V32] : ? [V33] : ? [V34] : ? [V35] : ? [V36] : ? [V37] : ? [V38] : ? [V39] : ? [V40] : ? [V41] : ? [V42] : ? [V43] : ? [V44] : ? [V45] : ? [V46] : ? [V47] : ? [V48] : ? [V49] : ? [V50] : ? [V51] : ? [V52] : ? [V53] : ? [V54] : ? [V55] : ? [V56] : ? [V57] : ? [V58] : ? [V59] : ? [V60] : ? [V61] : ? [V62] : ? [V63] : ? [V64] : ? [V65] : ? [V66] : ? [V67] : ? [V68] : ? [V69] : ? [V70] : ? [V71] : ? [V72] : ? [V73] : ? [V74] : ? [V75] : ? [V76] : ? [V77] : ? [V78] : ? [V79] : ? [V80] : ? [V81] : ? [V82] : ? [V83] : ? [V84] : ? [V85] : ? [V86] : ? [V87] : ? [V88] : ? [V89] : ? [V90] : ? [V91] : ? [V92] : ? [V93] : ? [V94] : ? [V95] : ? [V96] : ? [V97] : ? [V98] : ? [V99] : ? [V100] : ? [V101] : ? [V102] : ? [V103] : ? [V104] : ? [V105] : ? [V106] : ? [V107] : ? [V108] : ? [V109] : ? [V110] : ? [V111] : ? [V112] : ? [V113] : ? [V114] : ? [V115] : ? [V116] : ? [V117] : ? [V118] : ? [V119] : ? [V120] : ? [V121] : ? [V122] : ? [V123] : ? [V124] : ? [V125] : ? [V126] : ? [V127] : ? [V128] : ? [V129] : ? [V130] : ? [V131] : ? [V132] : ? [V133] : ? [V134] : ? [V135] : ? [V136] : ? [V259] : ? [V260] : ? [V261] : ? [V268] : ? [V269] : ? [V270] : ? [V271] : ? [V272] : ? [V273] : ? [V274] : ? [V275] : ? [V276] : ? [V277] : ? [V278] : ? [V279] : ? [V280] : ? [V281] : ? [V282] : ? [V283] : ? [V284] : ? [V285] : ? [V286] : ? [V287] : ? [V288] : ? [V289] : ? [V290] : ? [V291] : ? [V292] : ? [V293] : ? [V294] : ? [V295] : ? [V296] : ? [V297] : ? [V298] : ? [V299] : ? [V300] : ? [V301] : ? [V302] : ? [V303] : ? [V304] : ? [V305] : ? [V306] : ? [V307] : ? [V308] : ? [V309] : ? [V310] : ? [V311] : ? [V312] : ? [V313] : ? [V314] : ? [V315] : ? [V316] : ? [V317] : ? [V318] : ? [V319] : ? [V320] : ? [V321] : ? [V322] : ? [V323] : ? [V324] : ? [V325] : ? [V326] : ? [V327] : ? [V328] : ? [V329] : ? [V330] : ? [V331] : ? [V332] : ? [V333] : ? [V334] : ? [V335] : ? [V336] : ? [V337] : ? [V338] : ? [V339] : ? [V340] : ? [V341] : ? [V342] : ? [V343] : ? [V344] : ? [V345] : ? [V346] : ? [V347] : ? [V348] : ? [V349] : ? [V350] : ? [V351] : ? [V352] : ? [V353] : ? [V354] : ? [V355] : ? [V356] : ? [V357] : ? [V358] : ? [V359] : ? [V360] : ? [V361] : ? [V362] : ? [V363] : ? [V364] : ? [V365] : ? [V366] : ? [V367] : ? [V368] : ? [V369] : ? [V370] : ? [V371] : ? [V372] : ? [V373] : ? [V374] : ? [V375] : ? [V376] : ? [V377] : ? [V378] : ? [V379] : ? [V380] : ! [V137] : ! [V138] : ! [V139] : ! [V146] : ! [V147] : ! [V148] : ! [V149] : ! [V150] : ! [V151] : ! [V152] : ! [V153] : ! [V154] : ! [V155] : ! [V156] : ! [V157] : ! [V158] : ! [V159] : ! [V160] : ! [V161] : ! [V162] : ! [V163] : ! [V164] : ! [V165] : ! [V166] : ! [V167] : ! [V168] : ! [V169] : ! [V170] : ! [V171] : ! [V172] : ! [V173] : ! [V174] : ! [V175] : ! [V176] : ! [V177] : ! [V178] : ! [V179] : ! [V180] : ! [V181] : ! [V182] : ! [V183] : ! [V184] : ! [V185] : ! [V186] : ! [V187] : ! [V188] : ! [V189] : ! [V190] : ! [V191] : ! [V192] : ! [V193] : ! [V194] : ! [V195] : ! [V196] : ! [V197] : ! [V198] : ! [V199] : ! [V200] : ! [V201] : ! [V202] : ! [V203] : ! [V204] : ! [V205] : ! [V206] : ! [V207] : ! [V208] : ! [V209] : ! [V210] : ! [V211] : ! [V212] : ! [V213] : ! [V214] : ! [V215] : ! [V216] : ! [V217] : ! [V218] : ! [V219] : ! [V220] : ! [V221] : ! [V222] : ! [V223] : ! [V224] : ! [V225] : ! [V226] : ! [V227] : ! [V228] : ! [V229] : ! [V230] : ! [V231] : ! [V232] : ! [V233] : ! [V234] : ! [V235] : ! [V236] : ! [V237] : ! [V238] : ! [V239] : ! [V240] : ! [V241] : ! [V242] : ! [V243] : ! [V249] : ? [V503] : ? [V504] : ? [V505] : ? [V506] : ? [V507] : ? [V508] : ? [V509] : ? [V510] : ? [V511] : ? [V512] : ? [V513] : ? [V514] : ? [V515] : ? [V516] : ? [V517] : ? [V518] : ? [V519] : ? [V520] : ? [V521] : ? [V522] : ? [V523] : ? [V524] : ? [V525] : ? [V526] : ? [V527] : ? [V528] : ? [V529] : ? [V530] : ? [V531] : ? [V532] : ? [V533] : ? [V534] : ? [V535] : ? [V536] : ? [V537] : ? [V538] : ? [V539] : ? [V540] : ? [V541] : ? [V542] : ? [V543] : ? [V544] : ? [V545] : ? [V546] : ? [V547] : ? [V548] : ? [V549] : ? [V550] : ? [V551] : ? [V552] : ? [V553] : ? [V554] : ? [V555] : ? [V556] : ? [V557] : ? [V558] : ? [V559] : ? [V560] : ? [V561] : ? [V562] : ? [V563] : ? [V564] : ? [V565] : ? [V566] : ? [V567] : ? [V568] : ? [V569] : ? [V570] : ? [V571] : ? [V572] : ? [V573] : ? [V574] : ? [V575] : ? [V576] : ? [V577] : ? [V578] : ? [V579] : ? [V580] : ? [V581] : ? [V582] : ? [V583] : ? [V584] : ? [V585] : ? [V586] : ? [V587] : ? [V588] : ? [V589] : ? [V590] : ? [V591] : ? [V592] : ? [V593] : ? [V594] : ? [V595] : ? [V596] : ? [V597] : ? [V598] : ? [V599] : ? [V600] : ? [V601] : ? [V602] : ? [V603] : ? [V604] : ? [V605] : ? [V606] : ? [V607] : ? [V608] : ? [V609] : ? [V610] : ? [V611] : ? [V612] : ? [V613] : ? [V614] : ? [V615] : ? [V616] : ? [V617] : ? [V618] : ? [V619] : ? [V620] : ? [V621] : ? [V622] : ? [V623] : ? [V624] : ? [V625] : ? [V626] : ? [V627] : ? [V628] : ? [V629] : ? [V630] : ? [V631] : ? [V632] : ? [V633] : ? [V634] : ? [V635] : ? [V636] : ? [V637] : ? [V638] : ? [V639] : ? [V640] : ? [V641] : ? [V642] : ? [V643] : ? [V644] : ? [V645] : ? [V646] : ? [V647] : ? [V648] : ? [V649] : ? [V650] : ? [V651] : ? [V652] : ? [V653] : ? [V654] : ? [V655] : ? [V656] : ? [V657] : ? [V658] : ? [V659] : ? [V660] : ? [V661] : ? [V662] : ? [V663] : ? [V664] : ? [V665] : ? [V666] : ? [V667] : ? [V668] : ? [V669] : ? [V670] : ? [V671] : ? [V672] : ? [V673] : ? [V674] : ? [V675] : ? [V676] : ? [V677] : ? [V678] : ? [V679] : ? [V680] : ? [V681] : ? [V682] : ? [V683] : ? [V684] : ? [V685] : ? [V686] : ? [V687] : ? [V688] : ? [V689] : ? [V690] : ? [V691] : ? [V692] : ? [V693] : ? [V694] : ? [V695] : ? [V696] : ? [V697] : ? [V698] : ? [V699] : ? [V700] : ? [V701] : ? [V702] : ? [V703] : ? [V704] : ? [V705] : ? [V706] : ? [V707] : ? [V708] : ? [V709] : ? [V710] : ? [V711] : ? [V712] : ? [V713] : ? [V714] : ? [V715] : ? [V716] : ? [V717] : ? [V718] : ? [V719] : ? [V720] : ? [V721] : ? [V722] : ? [V723] : ? [V724] : ? [V725] : ? [V726] : ? [V727] : ? [V728] : ? [V729] : ? [V730] : ? [V731] : ? [V732] : ? [V733] : ? [V734] : ? [V735] : ? [V736] : ? [V737] : ? [V738] : ? [V739] : ? [V740] : ? [V741] : ? [V742] : ? [V743] : ? [V744] : ? [V745] : ? [V746] : ? [V747] : ? [V748] : ? [V749] : ? [V750] : ? [V751] : ? [V752] : ? [V753] : ? [V754] : ? [V755] : ? [V756] : ? [V757] : ? [V758] : ? [V759] : ? [V760] : ? [V761] : ? [V762] : ? [V763] : ? [V764] : ? [V765] : ? [V766] : ? [V767] : ? [V768] : ? [V769] : ? [V770] : ? [V771] : ? [V772] : ? [V773] : ? [V774] : ? [V775] : ? [V776] : ? [V777] : ? [V778] : ? [V779] : ? [V780] : ? [V781] : ? [V782] : ? [V783] : ? [V784] : ? [V785] : ? [V786] : ? [V787] : ? [V788] : ? [V789] : ? [V790] : ? [V791] : ? [V792] : ? [V793] : ? [V794] : ? [V795] : ? [V796] : ? [V797] : ? [V798] : ? [V799] : ? [V800] : ? [V801] : ? [V802] : ? [V803] : ? [V804] : ? [V805] : ? [V806] : ? [V807] : ? [V808] : ? [V809] : ? [V810] : ? [V811] : ? [V812] : ? [V813] : ? [V814] : ? [V815] : ? [V816] : ? [V817] : ? [V818] : ? [V819] : ? [V820] : ? [V821] : ? [V822] : ? [V823] : ? [V824] : ? [V825] : ? [V826] : ? [V827] : ? [V828] : ? [V829] : ? [V830] : ? [V831] : ? [V832] : ? [V833] : ? [V834] : ? [V835] : ? [V836] : ? [V837] : ? [V838] : ? [V839] : ? [V840] : ? [V841] : ? [V842] : ? [V843] : ? [V844] : ? [V845] : ? [V846] : ? [V847] : ? [V848] : ? [V849] : ? [V850] : ? [V851] : ? [V852] : ? [V853] : ( p(true) & ~ p(false) & ( p(V204) | p(V654) ) & ( ~ p(V203) | ~ p(V650) | p(V157) ) & ( p(V376) | p(V335) | p(V364) ) & ( p(V817) | ~ p(V370) ) & ( ~ p(V194) | p(V613) ) & ( ~ p(V314) | p(V272) ) & ( ~ p(V378) | ~ p(V365) ) & ( ~ p(V199) | ~ p(V633) | p(V2) ) & ( ~ p(V82) | p(V36) ) & ( p(V652) | p(V2) ) & ( ~ p(V5) | p(V657) ) & ( p(V604) | p(V150) ) & ( ~ p(V99) | ~ p(V136) ) & ( p(V784) | p(V237) ) & ( p(V808) | p(V368) ) & ( p(V528) | p(V158) ) & ( ~ p(V148) | ~ p(V716) | p(V223) ) & ( p(V652) | p(V156) ) & ( p(V359) | p(V362) ) & ( p(V146) | p(V504) ) & ( p(V4) | ~ p(V762) | p(V3) | ~ p(V235) ) & ( p(V2) | p(V757) ) & ( p(V132) | p(V295) ) & ( p(V798) | p(V366) ) & ( ~ p(V2) | p(V649) ) & ( ~ p(V90) | p(V3) ) & ( p(V336) | p(V327) | p(V328) ) & ( p(V243) | p(V234) | ~ p(V794) ) & ( p(V146) | p(V587) ) & ( p(V178) | ~ p(V710) | ~ p(V221) ) & ( ~ p(V95) | ~ p(V133) ) & ( p(V568) | ~ p(V179) ) & ( ~ p(V334) | p(V124) ) & ( ~ p(V124) | p(V346) ) & ( ~ p(V174) | ~ p(V176) | ~ p(V706) | p(V219) ) & ( p(V28) | ~ p(V69) ) & ( p(V361) | p(V346) ) & ( p(V673) | p(V210) ) & ( p(V47) | ~ p(V93) ) & ( p(V115) | ~ p(V42) ) & ( ~ p(V49) | ~ p(V12) ) & ( p(V269) | p(V314) | p(V312) | p(V313) | p(V368) ) & ( ~ p(V2) | p(V599) ) & ( p(V239) | p(V223) | ~ p(V776) ) & ( p(V222) | p(V851) ) & ( p(V807) | p(V368) ) & ( p(V26) | ~ p(V67) ) & ( p(V159) | p(V530) ) & ( ~ p(V224) | p(V777) ) & ( p(V2) | ~ p(V112) | p(V5) ) & ( ~ p(V165) | p(V673) ) & ( p(V686) | p(V168) ) & ( ~ p(V241) | p(V786) ) & ( ~ p(V238) | p(V773) ) & ( p(V281) | p(V129) ) & ( ~ p(V93) | p(V94) ) & ( ~ p(V220) | p(V175) | ~ p(V707) ) & ( ~ p(V148) | p(V724) ) & ( p(V742) | ~ p(V164) ) & ( ~ p(V69) | ~ p(V124) ) & ( p(V135) | p(V279) ) & ( p(V128) | p(V280) ) & ( p(V1) | p(V76) ) & ( ~ p(V289) | ~ p(V131) ) & ( ~ p(V319) | p(V275) ) & ( ~ p(V3) | p(V511) ) & ( ~ p(V146) | p(V503) ) & ( ~ p(V4) | ~ p(V33) ) & ( p(V168) | p(V754) ) & ( p(V819) | p(V249) ) & ( ~ p(V2) | ~ p(V29) ) & ( ~ p(V3) | ~ p(V156) | ~ p(V524) ) & ( ~ p(V379) | ~ p(V269) ) & ( p(V780) | ~ p(V240) ) & ( ~ p(V60) | ~ p(V57) ) & ( p(V136) | p(V302) ) & ( p(V126) | ~ p(V334) ) & ( ~ p(V341) | ~ p(V379) ) & ( ~ p(V11) | p(V108) ) & ( ~ p(V213) | p(V686) ) & ( p(V200) | ~ p(V651) | ~ p(V203) ) & ( p(V674) | p(V210) ) & ( ~ p(V205) | p(V659) ) & ( ~ p(V748) | ~ p(V670) | ~ p(V624) | ~ p(V736) | ~ p(V738) | ~ p(V683) | ~ p(V824) | ~ p(V521) | ~ p(V647) | ~ p(V754) | ~ p(V823) | ~ p(V621) | ~ p(V523) | ~ p(V567) | ~ p(V704) | ~ p(V765) | ~ p(V706) | ~ p(V830) | ~ p(V780) | ~ p(V620) | ~ p(V714) | ~ p(V668) | ~ p(V542) | ~ p(V682) | ~ p(V753) | ~ p(V514) | ~ p(V853) | ~ p(V583) | ~ p(V539) | ~ p(V827) | ~ p(V745) | ~ p(V687) | ~ p(V849) | ~ p(V759) | ~ p(V645) | ~ p(V666) | ~ p(V719) | ~ p(V783) | ~ p(V556) | ~ p(V690) | ~ p(V725) | ~ p(V576) | ~ p(V603) | ~ p(V756) | ~ p(V812) | ~ p(V551) | ~ p(V737) | ~ p(V515) | ~ p(V693) | ~ p(V544) | ~ p(V532) | ~ p(V701) | ~ p(V587) | ~ p(V663) | ~ p(V722) | ~ p(V654) | ~ p(V776) | ~ p(V527) | ~ p(V511) | ~ p(V778) | ~ p(V811) | ~ p(V813) | ~ p(V716) | ~ p(V664) | ~ p(V649) | ~ p(V622) | ~ p(V758) | ~ p(V800) | ~ p(V525) | ~ p(V847) | ~ p(V726) | ~ p(V522) | ~ p(V679) | ~ p(V712) | ~ p(V678) | ~ p(V807) | ~ p(V837) | ~ p(V686) | ~ p(V614) | ~ p(V825) | ~ p(V541) | ~ p(V744) | ~ p(V566) | ~ p(V733) | ~ p(V724) | ~ p(V790) | ~ p(V619) | ~ p(V634) | ~ p(V548) | ~ p(V613) | ~ p(V538) | ~ p(V585) | ~ p(V723) | ~ p(V743) | ~ p(V762) | ~ p(V555) | ~ p(V636) | ~ p(V766) | ~ p(V833) | ~ p(V558) | ~ p(V842) | ~ p(V816) | ~ p(V557) | ~ p(V559) | ~ p(V692) | ~ p(V677) | ~ p(V775) | ~ p(V546) | ~ p(V773) | ~ p(V516) | ~ p(V850) | ~ p(V571) | ~ p(V617) | ~ p(V793) | ~ p(V806) | ~ p(V791) | ~ p(V529) | ~ p(V564) | ~ p(V581) | ~ p(V702) | ~ p(V595) | ~ p(V851) | ~ p(V655) | ~ p(V573) | ~ p(V768) | ~ p(V665) | ~ p(V769) | ~ p(V711) | ~ p(V528) | ~ p(V797) | ~ p(V675) | ~ p(V681) | ~ p(V596) | ~ p(V846) | ~ p(V673) | ~ p(V730) | ~ p(V718) | ~ p(V708) | ~ p(V808) | ~ p(V652) | ~ p(V662) | ~ p(V657) | ~ p(V829) | ~ p(V618) | ~ p(V605) | ~ p(V503) | ~ p(V840) | ~ p(V820) | ~ p(V520) | ~ p(V691) | ~ p(V507) | ~ p(V750) | ~ p(V607) | ~ p(V661) | ~ p(V505) | ~ p(V739) | ~ p(V612) | ~ p(V839) | ~ p(V572) | ~ p(V680) | ~ p(V631) | ~ p(V650) | ~ p(V669) | ~ p(V540) | ~ p(V779) | ~ p(V641) | ~ p(V535) | ~ p(V742) | ~ p(V615) | ~ p(V513) | ~ p(V740) | ~ p(V510) | ~ p(V788) | ~ p(V689) | ~ p(V610) | ~ p(V592) | ~ p(V757) | ~ p(V699) | ~ p(V713) | ~ p(V597) | ~ p(V819) | ~ p(V519) | ~ p(V569) | ~ p(V582) | ~ p(V623) | ~ p(V575) | ~ p(V818) | ~ p(V721) | ~ p(V517) | ~ p(V848) | ~ p(V795) | ~ p(V627) | ~ p(V651) | ~ p(V709) | ~ p(V838) | ~ p(V565) | ~ p(V751) | ~ p(V547) | ~ p(V688) | ~ p(V717) | ~ p(V729) | ~ p(V784) | ~ p(V770) | ~ p(V781) | ~ p(V705) | ~ p(V512) | ~ p(V805) | ~ p(V646) | ~ p(V601) | ~ p(V789) | ~ p(V560) | ~ p(V637) | ~ p(V577) | ~ p(V639) | ~ p(V799) | ~ p(V598) | ~ p(V530) | ~ p(V802) | ~ p(V698) | ~ p(V844) | ~ p(V696) | ~ p(V764) | ~ p(V684) | ~ p(V584) | ~ p(V734) | ~ p(V749) | ~ p(V821) | ~ p(V772) | ~ p(V836) | ~ p(V828) | ~ p(V676) | ~ p(V671) | ~ p(V735) | ~ p(V561) | ~ p(V537) | ~ p(V640) | ~ p(V602) | ~ p(V792) | ~ p(V580) | ~ p(V656) | ~ p(V591) | ~ p(V804) | ~ p(V543) | ~ p(V732) | ~ p(V589) | ~ p(V549) | ~ p(V625) | ~ p(V841) | ~ p(V642) | ~ p(V845) | ~ p(V653) | ~ p(V590) | ~ p(V554) | ~ p(V563) | ~ p(V531) | ~ p(V755) | ~ p(V674) | ~ p(V695) | ~ p(V707) | ~ p(V568) | ~ p(V774) | ~ p(V586) | ~ p(V628) | ~ p(V672) | ~ p(V835) | ~ p(V630) | ~ p(V506) | ~ p(V633) | ~ p(V810) | ~ p(V794) | ~ p(V545) | ~ p(V832) | ~ p(V817) | ~ p(V731) | ~ p(V747) | ~ p(V809) | ~ p(V697) | ~ p(V746) | ~ p(V700) | ~ p(V536) | ~ p(V782) | ~ p(V644) | ~ p(V767) | ~ p(V608) | ~ p(V524) | ~ p(V629) | ~ p(V578) | ~ p(V570) | ~ p(V685) | ~ p(V606) | ~ p(V703) | ~ p(V648) | ~ p(V761) | ~ p(V552) | ~ p(V533) | ~ p(V720) | ~ p(V834) | ~ p(V787) | ~ p(V574) | ~ p(V727) | ~ p(V815) | ~ p(V600) | ~ p(V594) | ~ p(V609) | ~ p(V814) | ~ p(V694) | ~ p(V632) | ~ p(V526) | ~ p(V626) | ~ p(V509) | ~ p(V801) | ~ p(V752) | ~ p(V715) | ~ p(V667) | ~ p(V786) | ~ p(V593) | ~ p(V803) | ~ p(V831) | ~ p(V616) | ~ p(V660) | ~ p(V771) | ~ p(V785) | ~ p(V822) | ~ p(V504) | ~ p(V588) | ~ p(V534) | ~ p(V728) | ~ p(V760) | ~ p(V638) | ~ p(V635) | ~ p(V741) | ~ p(V852) | ~ p(V553) | ~ p(V763) | ~ p(V843) | ~ p(V579) | ~ p(V710) | ~ p(V658) | ~ p(V611) | ~ p(V643) | ~ p(V798) | ~ p(V550) | ~ p(V796) | ~ p(V599) | ~ p(V604) | ~ p(V562) | ~ p(V777) | ~ p(V826) | ~ p(V508) | ~ p(V659) | ~ p(V518) ) & ( ~ p(V185) | p(V584) ) & ( p(V1) | p(V39) ) & ( p(V363) | p(V375) | p(V334) ) & ( ~ p(V74) | ~ p(V30) ) & ( p(V555) | p(V12) ) & ( ~ p(V226) | p(V168) | p(V9) | ~ p(V732) ) & ( ~ p(V4) | p(V103) ) & ( p(V789) | p(V226) ) & ( ~ p(V216) | p(V695) ) & ( p(V229) | ~ p(V741) | ~ p(V11) ) & ( p(V212) | p(V241) | p(V375) | ~ p(V836) ) & ( p(V338) | p(V350) ) & ( p(V514) | p(V2) ) & ( p(V230) | ~ p(V743) | ~ p(V168) ) & ( ~ p(V205) | p(V5) | ~ p(V657) ) & ( p(V139) | p(V177) | ~ p(V566) ) & ( p(V125) | ~ p(V332) ) & ( ~ p(V123) | p(V356) ) & ( ~ p(V168) | p(V745) ) & ( p(V602) | p(V191) ) & ( ~ p(V48) | ~ p(V129) ) & ( p(V320) | p(V122) ) & ( p(V122) | p(V283) ) & ( ~ p(V368) | ~ p(V809) | ~ p(V147) ) & ( p(V361) | p(V345) ) & ( p(V147) | ~ p(V800) | p(V366) | p(V1) ) & ( p(V607) | p(V150) ) & ( p(V7) | p(V41) ) & ( ~ p(V48) | ~ p(V47) ) & ( p(V276) | p(V324) ) & ( p(V45) | ~ p(V90) ) & ( p(V9) | p(V50) ) & ( ~ p(V158) | p(V653) ) & ( ~ p(V373) | ~ p(V329) ) & ( ~ p(V155) | p(V639) ) & ( p(V152) | ~ p(V623) | ~ p(V197) ) & ( ~ p(V375) | ~ p(V334) ) & ( p(V228) | p(V697) ) & ( p(V3) | p(V737) ) & ( ~ p(V7) | ~ p(V530) | ~ p(V159) ) & ( ~ p(V339) | p(V292) ) & ( ~ p(V164) | p(V771) ) & ( p(V225) | ~ p(V2) | ~ p(V725) ) & ( ~ p(V353) | p(V132) | p(V292) | p(V290) | p(V288) ) & ( p(V162) | p(V768) ) & ( ~ p(V4) | ~ p(V198) | ~ p(V150) | ~ p(V1) | ~ p(V151) | ~ p(V631) ) & ( ~ p(V195) | p(V619) ) & ( p(V525) | ~ p(V13) ) & ( ~ p(V210) | p(V165) | ~ p(V673) ) & ( ~ p(V321) | p(V279) ) & ( ~ p(V89) | p(V44) ) & ( p(V5) | ~ p(V207) | ~ p(V664) ) & ( p(V596) | p(V189) ) & ( ~ p(V178) | p(V710) ) & ( p(V660) | ~ p(V162) ) & ( p(V156) | p(V647) ) & ( ~ p(V221) | p(V712) ) & ( ~ p(V311) | p(V270) ) & ( p(V792) | p(V242) ) & ( ~ p(V2) | ~ p(V520) | ~ p(V154) ) & ( ~ p(V835) | ~ p(V375) | ~ p(V241) ) & ( ~ p(V321) | p(V278) ) & ( p(V580) | ~ p(V12) ) & ( p(V204) | p(V653) ) & ( p(V148) | p(V508) ) & ( p(V149) | p(V196) | p(V152) | ~ p(V622) ) & ( p(V705) | ~ p(V176) ) & ( p(V610) | p(V194) ) & ( ~ p(V5) | p(V111) ) & ( ~ p(V331) | p(V286) ) & ( p(V48) | ~ p(V95) ) & ( p(V35) | ~ p(V81) ) & ( p(V151) | p(V607) ) & ( p(V163) | p(V538) ) & ( p(V750) | ~ p(V166) ) & ( ~ p(V17) | ~ p(V55) ) & ( p(V817) | ~ p(V197) ) & ( p(V31) | ~ p(V75) ) & ( p(V379) | p(V848) ) & ( p(V121) | p(V96) | p(V134) ) & ( ~ p(V5) | p(V696) ) & ( ~ p(V150) | ~ p(V3) | ~ p(V512) ) & ( p(V114) | ~ p(V4) ) & ( ~ p(V4) | p(V521) ) & ( ~ p(V292) | ~ p(V326) ) & ( p(V847) | p(V220) ) & ( p(V233) | p(V243) | ~ p(V793) ) & ( ~ p(V31) | ~ p(V14) ) & ( ~ p(V179) | p(V570) ) & ( p(V753) | p(V232) ) & ( p(V147) | p(V848) ) & ( p(V621) | p(V149) ) & ( p(V168) | ~ p(V683) | ~ p(V213) ) & ( ~ p(V378) | ~ p(V843) | ~ p(V218) ) & ( p(V153) | p(V626) ) & ( ~ p(V123) | ~ p(V276) ) & ( p(V600) | p(V190) ) & ( p(V733) | p(V168) ) & ( ~ p(V119) | ~ p(V131) ) & ( ~ p(V238) | p(V782) ) & ( p(V372) | p(V821) ) & ( p(V693) | ~ p(V216) ) & ( p(V71) | ~ p(V72) | ~ p(V27) ) & ( p(V579) | p(V11) ) & ( p(V5) | ~ p(V227) | p(V168) | ~ p(V735) ) & ( p(V113) | ~ p(V4) ) & ( p(V374) | p(V831) ) & ( ~ p(V124) | p(V312) | ~ p(V123) | ~ p(V122) ) & ( p(V579) | p(V183) ) & ( p(V793) | ~ p(V243) ) & ( ~ p(V5) | p(V756) ) & ( ~ p(V94) | ~ p(V5) | ~ p(V107) | ~ p(V108) | ~ p(V106) ) & ( ~ p(V10) | ~ p(V51) ) & ( p(V339) | p(V377) | p(V337) ) & ( ~ p(V311) | ~ p(V367) ) & ( p(V3) | p(V156) | ~ p(V523) ) & ( ~ p(V176) | p(V564) ) & ( p(V708) | p(V220) ) & ( p(V47) | p(V48) ) & ( p(V186) | p(V586) ) & ( ~ p(V231) | p(V747) ) & ( ~ p(V536) | ~ p(V2) | ~ p(V162) ) & ( p(V839) | ~ p(V376) ) & ( p(V744) | ~ p(V230) ) & ( ~ p(V3) | ~ p(V540) | ~ p(V164) ) & ( ~ p(V222) | p(V853) ) & ( ~ p(V126) | ~ p(V286) | ~ p(V284) | p(V328) ) & ( ~ p(V204) | p(V158) | ~ p(V653) ) & ( ~ p(V374) | ~ p(V832) | ~ p(V240) ) & ( p(V115) | ~ p(V40) ) & ( p(V621) | p(V196) ) & ( ~ p(V317) | p(V273) ) & ( p(V287) | p(V130) ) & ( ~ p(V39) | ~ p(V1) ) & ( ~ p(V152) | p(V623) ) & ( ~ p(V207) | p(V666) ) & ( p(V282) | p(V130) ) & ( p(V710) | p(V221) ) & ( p(V592) | ~ p(V1) ) & ( p(V58) | p(V14) ) & ( p(V2) | ~ p(V81) ) & ( p(V146) | p(V779) ) & ( ~ p(V66) | p(V1) ) & ( ~ p(V131) | p(V348) ) & ( ~ p(V54) | ~ p(V13) ) & ( ~ p(V133) | p(V352) ) & ( ~ p(V323) | p(V280) ) & ( p(V114) | p(V118) ) & ( p(V370) | p(V814) ) & ( ~ p(V582) | ~ p(V185) | p(V146) ) & ( ~ p(V203) | ~ p(V551) | ~ p(V170) ) & ( p(V309) | p(V311) | p(V367) | p(V310) | p(V269) ) & ( ~ p(V347) | ~ p(V363) | ~ p(V349) | ~ p(V348) | ~ p(V291) ) & ( p(V272) | ~ p(V317) ) & ( ~ p(V99) | p(V58) ) & ( p(V519) | ~ p(V2) ) & ( p(V272) | ~ p(V309) ) & ( p(V792) | p(V231) ) & ( p(V164) | p(V769) ) & ( ~ p(V313) | p(V270) ) & ( ~ p(V325) | p(V123) ) & ( p(V804) | p(V367) ) & ( ~ p(V249) | ~ p(V819) | ~ p(V186) ) & ( p(V631) | p(V1) ) & ( p(V714) | p(V222) ) & ( p(V163) | ~ p(V207) | ~ p(V665) ) & ( p(V702) | p(V218) ) & ( ~ p(V175) | p(V562) ) & ( p(V517) | ~ p(V153) ) & ( p(V170) | p(V550) ) & ( p(V842) | ~ p(V217) ) & ( p(V202) | ~ p(V204) | ~ p(V654) ) & ( p(V736) | ~ p(V228) ) & ( p(V135) | p(V324) ) & ( p(V4) | p(V46) ) & ( p(V678) | ~ p(V211) ) & ( p(V225) | ~ p(V728) | ~ p(V166) ) & ( p(V62) | p(V12) ) & ( p(V201) | p(V822) ) & ( ~ p(V233) | p(V793) ) & ( ~ p(V230) | ~ p(V216) | ~ p(V229) | ~ p(V5) | ~ p(V697) | ~ p(V228) ) & ( ~ p(V319) | ~ p(V370) ) & ( ~ p(V75) | p(V30) ) & ( p(V774) | ~ p(V238) ) & ( ~ p(V243) | p(V796) ) & ( p(V667) | p(V208) ) & ( ~ p(V215) | p(V692) ) & ( ~ p(V30) | p(V63) | ~ p(V24) ) & ( ~ p(V270) | ~ p(V122) ) & ( ~ p(V193) | ~ p(V609) | p(V194) ) & ( p(V663) | p(V5) ) & ( ~ p(V763) | p(V236) | ~ p(V2) ) & ( p(V1) | p(V614) ) & ( p(V368) | p(V809) ) & ( p(V103) | ~ p(V44) ) & ( p(V231) | ~ p(V166) | ~ p(V748) ) & ( p(V2) | p(V194) | ~ p(V612) ) & ( p(V45) | p(V9) ) & ( p(V682) | p(V3) ) & ( ~ p(V182) | p(V576) ) & ( ~ p(V124) | ~ p(V68) ) & ( p(V645) | ~ p(V13) ) & ( p(V373) | p(V826) ) & ( ~ p(V166) | p(V676) ) & ( ~ p(V749) | ~ p(V10) | p(V231) ) & ( ~ p(V202) | p(V641) ) & ( ~ p(V42) | ~ p(V3) ) & ( ~ p(V67) | p(V29) ) & ( ~ p(V569) | ~ p(V179) | ~ p(V178) ) & ( ~ p(V91) | ~ p(V132) ) & ( p(V631) | p(V198) ) & ( p(V186) | p(V249) | ~ p(V820) | p(V185) ) & ( p(V615) | ~ p(V150) ) & ( p(V225) | p(V729) ) & ( p(V150) | p(V591) ) & ( ~ p(V44) | ~ p(V4) | p(V89) ) & ( ~ p(V168) | ~ p(V166) | p(V208) | ~ p(V669) ) & ( ~ p(V326) | p(V324) ) & ( p(V349) | ~ p(V126) ) & ( p(V243) | p(V169) | ~ p(V796) ) & ( ~ p(V4) | ~ p(V727) | p(V225) ) & ( ~ p(V5) | ~ p(V10) | ~ p(V659) | p(V205) | ~ p(V3) ) & ( ~ p(V79) | p(V80) ) & ( ~ p(V84) | p(V5) ) & ( p(V260) | p(V304) ) & ( ~ p(V5) | p(V212) | ~ p(V3) | ~ p(V167) | ~ p(V682) ) & ( p(V682) | ~ p(V212) ) & ( p(V322) | ~ p(V325) ) & ( ~ p(V346) | p(V270) | p(V123) | p(V124) ) & ( ~ p(V782) | p(V238) | p(V240) ) & ( ~ p(V546) | ~ p(V9) | ~ p(V167) ) & ( ~ p(V170) | p(V750) ) & ( p(V771) | ~ p(V5) ) & ( p(V47) | p(V119) ) & ( ~ p(V195) | ~ p(V814) | ~ p(V370) ) & ( ~ p(V209) | p(V672) ) & ( ~ p(V120) | ~ p(V109) | ~ p(V110) ) & ( p(V76) | p(V28) ) & ( ~ p(V122) | ~ p(V272) | ~ p(V125) | p(V309) ) & ( ~ p(V205) | p(V689) ) & ( ~ p(V169) | p(V232) | ~ p(V751) ) & ( p(V188) | p(V592) ) & ( ~ p(V783) | p(V240) | p(V169) ) & ( ~ p(V802) | ~ p(V367) | ~ p(V188) ) & ( ~ p(V8) | p(V116) ) & ( p(V276) | p(V123) ) & ( p(V4) | p(V510) ) & ( ~ p(V3) | p(V106) ) & ( p(V680) | p(V212) ) & ( p(V353) | ~ p(V290) ) & ( ~ p(V47) | p(V93) | ~ p(V94) ) & ( p(V292) | p(V291) ) & ( ~ p(V6) | p(V527) ) & ( ~ p(V240) | p(V833) ) & ( ~ p(V170) | p(V699) ) & ( p(V362) | p(V358) ) & ( ~ p(V374) | p(V833) ) & ( ~ p(V517) | p(V153) | p(V14) ) & ( p(V270) | p(V122) ) & ( p(V131) | p(V290) | ~ p(V348) ) & ( p(V789) | p(V169) ) & ( p(V158) | p(V642) ) & ( ~ p(V212) | ~ p(V679) | p(V167) ) & ( ~ p(V547) | p(V168) | p(V4) ) & ( ~ p(V2) | ~ p(V722) | p(V224) ) & ( ~ p(V11) | ~ p(V61) ) & ( p(V226) | p(V732) ) & ( p(V3) | p(V726) ) & ( p(V237) | ~ p(V781) | p(V240) ) & ( p(V835) | p(V241) ) & ( ~ p(V115) | p(V40) | p(V5) | p(V42) ) & ( ~ p(V197) | p(V626) ) & ( p(V239) | ~ p(V813) | p(V193) | p(V369) ) & ( p(V7) | p(V37) ) & ( ~ p(V380) | ~ p(V269) ) & ( p(V208) | p(V826) ) & ( p(V1) | p(V26) ) & ( ~ p(V4) | ~ p(V548) | ~ p(V168) ) & ( p(V212) | p(V679) ) & ( p(V367) | p(V803) ) & ( p(V217) | p(V215) | ~ p(V842) | p(V377) ) & ( p(V846) | p(V219) ) & ( ~ p(V227) | p(V734) ) & ( p(V664) | ~ p(V5) ) & ( ~ p(V104) | ~ p(V105) | ~ p(V47) | ~ p(V119) | ~ p(V103) ) & ( ~ p(V161) | ~ p(V534) | ~ p(V1) ) & ( ~ p(V146) | p(V778) ) & ( ~ p(V371) | ~ p(V307) ) & ( p(V824) | ~ p(V372) ) & ( p(V512) | p(V3) ) & ( p(V775) | ~ p(V166) ) & ( p(V849) | ~ p(V379) ) & ( ~ p(V168) | p(V547) ) & ( p(V124) | ~ p(V327) ) & ( p(V228) | p(V739) ) & ( p(V203) | p(V551) ) & ( ~ p(V208) | ~ p(V826) | ~ p(V373) ) & ( p(V214) | ~ p(V685) | ~ p(V213) ) & ( ~ p(V701) | ~ p(V218) | p(V171) ) & ( ~ p(V635) | p(V200) | ~ p(V199) ) & ( ~ p(V171) | p(V554) ) & ( ~ p(V122) | ~ p(V25) ) & ( p(V123) | ~ p(V321) ) & ( ~ p(V84) | p(V40) ) & ( ~ p(V212) | p(V836) ) & ( ~ p(V164) | p(V229) | ~ p(V740) ) & ( ~ p(V272) | p(V345) ) & ( p(V25) | p(V59) ) & ( p(V271) | ~ p(V315) ) & ( ~ p(V133) | p(V351) ) & ( p(V560) | ~ p(V175) ) & ( p(V175) | ~ p(V560) | p(V174) ) & ( p(V107) | ~ p(V11) ) & ( ~ p(V13) | ~ p(V176) | ~ p(V565) ) & ( ~ p(V160) | p(V531) ) & ( p(V734) | p(V5) ) & ( p(V374) | p(V832) ) & ( ~ p(V148) | p(V602) ) & ( ~ p(V5) | ~ p(V44) ) & ( ~ p(V2) | p(V759) ) & ( p(V316) | p(V123) ) & ( ~ p(V192) | p(V150) | ~ p(V606) ) & ( ~ p(V199) | ~ p(V372) | ~ p(V821) ) & ( p(V557) | p(V172) ) & ( p(V722) | ~ p(V224) ) & ( ~ p(V200) | p(V646) ) & ( p(V361) | p(V268) ) & ( p(V209) | ~ p(V168) | ~ p(V672) | ~ p(V164) ) & ( p(V8) | p(V774) ) & ( p(V617) | p(V195) ) & ( p(V506) | p(V181) ) & ( ~ p(V85) | ~ p(V129) ) & ( ~ p(V130) | ~ p(V118) ) & ( ~ p(V292) | ~ p(V291) ) & ( ~ p(V280) | ~ p(V324) | p(V326) ) & ( ~ p(V291) | ~ p(V338) | p(V337) ) & ( ~ p(V4) | p(V729) ) & ( p(V708) | ~ p(V13) ) & ( p(V5) | p(V666) ) & ( p(V634) | p(V199) ) & ( ~ p(V274) | ~ p(V318) ) & ( p(V198) | ~ p(V629) | p(V151) ) & ( p(V11) | ~ p(V108) | p(V46) ) & ( p(V31) | ~ p(V64) ) & ( p(V202) | p(V647) ) & ( ~ p(V214) | ~ p(V168) | p(V213) | ~ p(V686) | ~ p(V169) ) & ( ~ p(V723) | p(V224) | ~ p(V3) ) & ( ~ p(V332) | p(V287) ) & ( p(V47) | p(V118) ) & ( p(V766) | ~ p(V236) ) & ( ~ p(V337) | p(V291) ) & ( p(V169) | p(V686) ) & ( p(V13) | ~ p(V220) | ~ p(V708) ) & ( ~ p(V3) | ~ p(V5) | ~ p(V45) | p(V90) ) & ( ~ p(V318) | ~ p(V271) ) & ( ~ p(V166) | p(V729) ) & ( ~ p(V224) | p(V721) ) & ( p(V48) | p(V81) | p(V82) ) & ( p(V320) | p(V272) ) & ( p(V802) | p(V367) ) & ( p(V296) | p(V297) ) & ( p(V11) | p(V741) ) & ( ~ p(V165) | ~ p(V8) | ~ p(V542) ) & ( ~ p(V126) | ~ p(V73) ) & ( ~ p(V356) | p(V123) | p(V126) ) & ( ~ p(V585) | ~ p(V186) | p(V153) ) & ( ~ p(V324) | ~ p(V135) | ~ p(V322) | ~ p(V276) | ~ p(V278) ) & ( ~ p(V357) | p(V125) | p(V124) ) & ( p(V811) | p(V193) ) & ( p(V799) | p(V147) ) & ( p(V784) | p(V169) ) & ( p(V139) | p(V567) ) & ( p(V150) | ~ p(V589) | ~ p(V187) ) & ( p(V156) | p(V636) ) & ( p(V147) | p(V181) | ~ p(V505) ) & ( ~ p(V126) | ~ p(V124) | p(V327) | ~ p(V132) ) & ( p(V164) | ~ p(V209) | ~ p(V670) ) & ( ~ p(V312) | p(V124) ) & ( ~ p(V312) | ~ p(V368) ) & ( p(V737) | ~ p(V228) ) & ( p(V625) | p(V197) ) & ( ~ p(V8) | ~ p(V160) | ~ p(V532) ) & ( ~ p(V3) | p(V656) ) & ( p(V78) | ~ p(V77) ) & ( p(V156) | ~ p(V632) | ~ p(V199) ) & ( ~ p(V4) | p(V627) ) & ( p(V161) | p(V534) ) & ( ~ p(V316) | p(V315) | ~ p(V271) ) & ( p(V112) | p(V121) ) & ( p(V113) | ~ p(V3) ) & ( p(V196) | p(V619) ) & ( p(V169) | ~ p(V753) | p(V161) | ~ p(V232) ) & ( ~ p(V9) | p(V104) ) & ( p(V363) | p(V349) ) & ( p(V9) | ~ p(V545) | p(V167) ) & ( p(V151) | p(V597) ) & ( ~ p(V122) | ~ p(V366) ) & ( p(V53) | p(V52) ) & ( ~ p(V186) | p(V820) ) & ( ~ p(V2) | p(V114) ) & ( p(V170) | p(V828) ) & ( ~ p(V223) | p(V719) ) & ( ~ p(V162) | p(V228) | ~ p(V736) ) & ( p(V63) | p(V64) | p(V127) ) & ( ~ p(V731) | ~ p(V9) | p(V226) ) & ( ~ p(V131) | ~ p(V90) ) & ( ~ p(V88) | p(V4) ) & ( ~ p(V790) | p(V242) | p(V231) ) & ( ~ p(V42) | p(V107) ) & ( ~ p(V201) | p(V158) | ~ p(V640) ) & ( ~ p(V376) | ~ p(V837) | ~ p(V213) ) & ( p(V731) | p(V9) ) & ( p(V106) | p(V94) ) & ( p(V1) | ~ p(V217) | ~ p(V698) ) & ( p(V785) | ~ p(V241) ) & ( p(V224) | p(V724) ) & ( p(V57) | ~ p(V100) ) & ( p(V168) | p(V730) ) & ( p(V3) | ~ p(V83) ) & ( ~ p(V216) | p(V694) ) & ( p(V838) | p(V376) ) & ( p(V609) | ~ p(V194) ) & ( ~ p(V594) | p(V188) | ~ p(V1) | ~ p(V2) ) & ( p(V113) | p(V121) ) & ( p(V4) | p(V765) ) & ( ~ p(V206) | ~ p(V661) | p(V164) ) & ( p(V67) | p(V65) | p(V25) | p(V123) | p(V66) ) & ( ~ p(V47) | p(V110) ) & ( p(V195) | p(V618) ) & ( ~ p(V128) | ~ p(V280) ) & ( p(V363) | p(V291) ) & ( p(V168) | p(V747) ) & ( p(V637) | p(V200) ) & ( p(V560) | ~ p(V174) ) & ( p(V100) | ~ p(V14) | ~ p(V57) ) & ( p(V610) | ~ p(V193) ) & ( ~ p(V161) | p(V232) | ~ p(V752) ) & ( p(V545) | ~ p(V167) ) & ( p(V27) | ~ p(V71) ) & ( ~ p(V804) | ~ p(V147) | ~ p(V367) ) & ( p(V829) | ~ p(V373) ) & ( p(V46) | p(V10) | p(V48) | p(V44) | ~ p(V109) ) & ( p(V5) | p(V703) ) & ( p(V134) | p(V293) ) & ( ~ p(V272) | ~ p(V273) | p(V314) ) & ( p(V636) | ~ p(V199) ) & ( ~ p(V240) | p(V781) ) & ( p(V146) | p(V584) ) & ( p(V539) | ~ p(V164) ) & ( p(V196) | ~ p(V195) | ~ p(V618) ) & ( p(V204) | p(V552) ) & ( ~ p(V1) | p(V588) ) & ( p(V111) | ~ p(V46) ) & ( ~ p(V342) | ~ p(V379) ) & ( ~ p(V199) | p(V824) ) & ( ~ p(V370) | ~ p(V317) ) & ( ~ p(V541) | p(V165) | p(V8) ) & ( p(V60) | p(V57) ) & ( ~ p(V236) | p(V780) ) & ( p(V628) | ~ p(V198) ) & ( ~ p(V211) | ~ p(V374) | ~ p(V831) ) & ( ~ p(V189) | p(V805) ) & ( ~ p(V34) | ~ p(V13) | ~ p(V80) | ~ p(V78) | ~ p(V32) ) & ( p(V42) | ~ p(V107) | p(V11) ) & ( p(V228) | ~ p(V693) | p(V216) ) & ( p(V290) | ~ p(V331) ) & ( p(V599) | p(V190) ) & ( p(V643) | ~ p(V202) ) & ( ~ p(V756) | p(V5) | ~ p(V233) | p(V168) ) & ( p(V608) | ~ p(V149) ) & ( p(V122) | ~ p(V312) ) & ( p(V303) | p(V259) ) & ( ~ p(V166) | p(V767) ) & ( p(V831) | p(V211) ) & ( ~ p(V26) | ~ p(V28) | p(V69) ) & ( p(V697) | p(V5) ) & ( p(V528) | p(V6) ) & ( p(V558) | ~ p(V173) ) & ( p(V269) | p(V303) ) & ( ~ p(V284) | ~ p(V123) ) & ( ~ p(V13) | ~ p(V35) ) & ( p(V538) | p(V7) ) & ( ~ p(V28) | ~ p(V74) | ~ p(V29) | ~ p(V1) | p(V73) ) & ( ~ p(V130) | p(V360) ) & ( ~ p(V166) | ~ p(V544) | ~ p(V5) ) & ( ~ p(V168) | p(V683) ) & ( ~ p(V275) | p(V319) | ~ p(V274) | ~ p(V320) ) & ( p(V535) | ~ p(V162) ) & ( ~ p(V310) | p(V123) ) & ( ~ p(V225) | p(V785) ) & ( p(V56) | p(V57) ) & ( ~ p(V204) | p(V655) ) & ( p(V213) | p(V685) ) & ( p(V122) | ~ p(V309) ) & ( p(V668) | p(V208) ) & ( ~ p(V291) | ~ p(V355) | ~ p(V357) | ~ p(V356) | ~ p(V365) ) & ( p(V355) | ~ p(V290) ) & ( ~ p(V112) | ~ p(V47) | ~ p(V113) | ~ p(V121) | ~ p(V111) ) & ( p(V54) | p(V13) ) & ( p(V72) | p(V1) ) & ( p(V234) | p(V797) ) & ( ~ p(V215) | ~ p(V690) | p(V169) ) & ( p(V116) | ~ p(V44) ) & ( p(V746) | ~ p(V231) ) & ( p(V643) | ~ p(V156) ) & ( p(V34) | ~ p(V77) ) & ( p(V541) | ~ p(V8) ) & ( ~ p(V268) | p(V308) | ~ p(V275) ) & ( p(V152) | p(V626) ) & ( ~ p(V292) | ~ p(V122) | p(V339) ) & ( p(V206) | p(V688) ) & ( p(V198) | ~ p(V630) | p(V1) ) & ( ~ p(V225) | p(V725) ) & ( p(V24) | ~ p(V63) ) & ( p(V300) | ~ p(V343) ) & ( ~ p(V98) | p(V53) ) & ( p(V711) | p(V221) ) & ( ~ p(V124) | ~ p(V70) ) & ( ~ p(V285) | ~ p(V129) ) & ( ~ p(V757) | p(V234) | ~ p(V2) ) & ( ~ p(V233) | p(V754) ) & ( p(V28) | ~ p(V65) ) & ( ~ p(V202) | p(V654) ) & ( p(V209) | p(V827) ) & ( p(V133) | p(V286) | ~ p(V351) ) & ( ~ p(V1) | p(V507) ) & ( ~ p(V240) | p(V783) ) & ( p(V178) | p(V712) ) & ( p(V166) | p(V773) ) & ( p(V1) | p(V700) ) & ( ~ p(V29) | ~ p(V28) | p(V70) ) & ( p(V125) | ~ p(V309) ) & ( p(V199) | p(V635) ) & ( p(V823) | p(V372) ) & ( ~ p(V5) | p(V543) ) & ( p(V316) | p(V122) ) & ( p(V1) | ~ p(V65) ) & ( ~ p(V166) | p(V238) | ~ p(V773) ) & ( p(V217) | ~ p(V1) | ~ p(V170) | ~ p(V700) ) & ( ~ p(V10) | p(V83) | ~ p(V5) | ~ p(V3) ) & ( ~ p(V833) | p(V374) | p(V240) | p(V210) | p(V211) ) & ( p(V609) | p(V193) ) & ( p(V554) | ~ p(V12) ) & ( p(V148) | p(V721) ) & ( p(V788) | ~ p(V241) ) & ( p(V207) | ~ p(V5) | ~ p(V163) | ~ p(V666) ) & ( ~ p(V655) | ~ p(V202) | ~ p(V158) | p(V204) ) & ( ~ p(V336) | ~ p(V327) ) & ( p(V812) | p(V239) ) & ( p(V228) | ~ p(V737) | ~ p(V3) ) & ~ p(V4) & ( ~ p(V315) | ~ p(V369) ) & ( ~ p(V268) | ~ p(V274) | p(V307) ) & ( p(V24) | p(V25) ) & ( p(V187) | ~ p(V4) | ~ p(V591) | ~ p(V1) | ~ p(V150) ) & ( p(V239) | p(V224) | ~ p(V777) ) & ( ~ p(V2) | p(V535) ) & ( ~ p(V116) | ~ p(V47) | ~ p(V114) | ~ p(V118) | ~ p(V115) ) & ( p(V833) | ~ p(V210) ) & ( p(V223) | ~ p(V719) | ~ p(V149) ) & ( p(V14) | ~ p(V100) ) & ( p(V642) | p(V202) ) & ( p(V732) | ~ p(V9) ) & ( ~ p(V168) | p(V667) ) & ( ~ p(V379) | ~ p(V220) | ~ p(V847) ) & ( p(V739) | ~ p(V162) ) & ( p(V575) | p(V181) ) & ( ~ p(V46) | p(V91) | ~ p(V92) | ~ p(V47) ) & ( p(V162) | ~ p(V237) | ~ p(V771) | p(V164) | p(V5) ) & ( p(V726) | ~ p(V225) ) & ( p(V777) | ~ p(V239) ) & ( p(V718) | ~ p(V223) ) & ( p(V25) | p(V97) | p(V135) | p(V98) ) & ( p(V698) | ~ p(V1) ) & ( ~ p(V123) | p(V358) ) & ( ~ p(V2) | ~ p(V32) ) & ( p(V322) | p(V324) ) & ( p(V147) | p(V221) | p(V380) | ~ p(V853) | p(V222) ) & ( p(V72) | p(V2) ) & ( p(V215) | p(V840) ) & ( p(V551) | p(V170) ) & ( ~ p(V2) | p(V729) ) & ( p(V779) | p(V239) ) & ( ~ p(V122) | p(V310) | ~ p(V123) ) & ( p(V290) | ~ p(V352) | p(V133) ) & ( ~ p(V168) | p(V671) ) & ( ~ p(V335) | p(V336) ) & ( ~ p(V132) | ~ p(V295) ) & ( p(V101) | ~ p(V26) ) & ~ p(V8) & ( p(V520) | p(V154) ) & ( p(V764) | p(V3) ) & ( ~ p(V373) | ~ p(V331) ) & ( ~ p(V181) | p(V505) ) & ( p(V240) | p(V832) ) & ( ~ p(V369) | ~ p(V812) | ~ p(V239) ) & ( ~ p(V241) | p(V787) ) & ( ~ p(V237) | p(V769) ) & ( ~ p(V136) | ~ p(V301) | p(V344) ) & ( p(V205) | p(V658) ) & ( p(V166) | p(V678) ) & ( ~ p(V373) | ~ p(V330) ) & ( p(V589) | ~ p(V150) ) & ( ~ p(V845) | p(V218) | p(V243) | p(V378) ) & ( p(V11) | ~ p(V742) | ~ p(V229) | p(V164) ) & ( ~ p(V190) | p(V810) ) & ( ~ p(V14) | p(V572) ) & ( p(V278) | ~ p(V325) ) & ( ~ p(V127) | ~ p(V63) ) & ( ~ p(V70) | p(V29) ) & ( p(V231) | ~ p(V170) | ~ p(V746) ) & ( ~ p(V335) | p(V290) ) & ( p(V652) | p(V157) ) & ( p(V2) | p(V3) | ~ p(V102) | p(V26) ) & ( ~ p(V71) | p(V72) ) & ( ~ p(V328) | ~ p(V336) ) & ( p(V651) | ~ p(V200) ) & ( p(V198) | p(V626) ) & ( p(V156) | ~ p(V648) | ~ p(V203) ) & ( ~ p(V99) | p(V56) ) & ( p(V1) | ~ p(V592) | ~ p(V188) ) & ( ~ p(V361) | ~ p(V345) | ~ p(V346) | ~ p(V268) ) & ( ~ p(V173) | ~ p(V559) | ~ p(V10) ) & ( p(V68) | ~ p(V2) | ~ p(V1) | ~ p(V3) ) & ( p(V539) | ~ p(V3) ) & ( p(V359) | ~ p(V284) ) & ( p(V92) | ~ p(V91) ) & ( p(V94) | p(V107) ) & ( p(V285) | ~ p(V329) ) & ( p(V813) | ~ p(V369) ) & ( p(V29) | p(V27) | ~ p(V101) | p(V26) | p(V28) ) & ( p(V610) | p(V149) ) & ( p(V83) | p(V84) | p(V92) ) & ~ p(V9) & ( ~ p(V319) | p(V274) ) & ( ~ p(V259) | ~ p(V303) ) & ( p(V844) | p(V243) ) & ( p(V782) | ~ p(V240) ) & ( p(V135) | ~ p(V342) ) & ( p(V323) | p(V321) | p(V269) | p(V372) ) & ( p(V672) | p(V164) ) & ( ~ p(V238) | p(V772) ) & ( p(V624) | p(V197) ) & ( p(V165) | p(V675) ) & ( ~ p(V81) | ~ p(V48) ) & ( ~ p(V44) | p(V114) ) & ( p(V622) | ~ p(V196) ) & ( ~ p(V153) | ~ p(V152) | p(V197) | ~ p(V626) | ~ p(V198) ) & ( p(V3) | p(V44) | p(V2) | p(V4) | ~ p(V103) ) & ( ~ p(V171) | p(V701) ) & ( ~ p(V170) | p(V829) ) & ( p(V7) | p(V163) | ~ p(V537) ) & ( p(V5) | p(V659) ) & ( p(V617) | ~ p(V1) ) & ( p(V2) | p(V725) ) & ( ~ p(V198) | p(V629) ) & ( p(V180) | p(V573) ) & ( ~ p(V147) | ~ p(V799) | ~ p(V366) ) & ( ~ p(V178) | p(V568) ) & ( p(V620) | p(V196) ) & ( p(V16) | p(V60) ) & ( p(V660) | p(V206) ) & ( p(V34) | p(V80) ) & ( ~ p(V16) | ~ p(V60) ) & ( ~ p(V285) | p(V329) | ~ p(V126) ) & ( p(V813) | ~ p(V193) ) & ( ~ p(V2) | p(V81) | ~ p(V35) | ~ p(V34) | ~ p(V78) ) & ( p(V13) | p(V647) ) & ( p(V373) | p(V825) ) & ( p(V291) | p(V362) ) & ( p(V639) | ~ p(V5) ) & ( ~ p(V136) | ~ p(V100) ) & ( ~ p(V11) | p(V745) ) & ( ~ p(V169) | p(V753) ) & ( ~ p(V24) | ~ p(V31) | p(V64) ) & ( p(V296) | ~ p(V341) ) & ( ~ p(V192) | p(V810) ) & ( p(V42) | ~ p(V84) ) & ( p(V35) | p(V13) ) & ( p(V1) | ~ p(V68) ) & ( p(V84) | ~ p(V40) | ~ p(V42) | ~ p(V5) ) & ( p(V354) | ~ p(V283) ) & ( p(V104) | p(V119) ) & ( p(V830) | p(V374) ) & ( p(V526) | p(V13) ) & ( p(V1) | p(V148) | ~ p(V507) ) & ( p(V569) | p(V179) ) & ( ~ p(V104) | p(V46) | p(V9) ) & ( p(V238) | p(V784) ) & ( p(V194) | p(V614) ) & ( p(V728) | ~ p(V225) ) & ( p(V625) | ~ p(V198) ) & ( p(V298) | p(V135) ) & ( p(V562) | ~ p(V177) ) & ( p(V690) | ~ p(V169) ) & ( ~ p(V370) | ~ p(V371) ) & ( ~ p(V308) | p(V275) ) & ( p(V380) | p(V850) ) & ( p(V767) | ~ p(V2) ) & ( p(V291) | ~ p(V335) ) & ( p(V689) | ~ p(V214) ) & ( p(V174) | p(V706) ) & ( p(V835) | p(V375) ) & ( p(V362) | p(V333) | p(V332) | p(V374) ) & ( ~ p(V307) | p(V268) ) & ( ~ p(V306) | ~ p(V134) ) & ( ~ p(V368) | p(V810) ) & ( p(V10) | p(V659) ) & ( p(V166) | p(V5) | ~ p(V543) ) & ( p(V150) | p(V619) ) & ( ~ p(V368) | ~ p(V314) ) & ( p(V629) | ~ p(V151) ) & ( p(V35) | ~ p(V77) ) & ( ~ p(V96) | p(V5) ) & ( p(V213) | p(V684) ) & ( ~ p(V86) | ~ p(V129) ) & ( p(V1) | p(V601) ) & ( p(V641) | p(V201) ) & ( p(V187) | p(V590) ) & ( p(V249) | p(V818) ) & ( p(V102) | ~ p(V2) ) & ( p(V201) | p(V199) | p(V147) | p(V372) | ~ p(V824) ) & ( p(V236) | ~ p(V4) | ~ p(V765) ) & ( p(V5) | ~ p(V90) ) & ( ~ p(V187) | ~ p(V588) | p(V1) ) & ( p(V767) | p(V236) ) & ( p(V795) | ~ p(V235) ) & ( p(V76) | p(V29) ) & ( p(V24) | ~ p(V64) ) & ( p(V509) | ~ p(V4) ) & ( ~ p(V6) | ~ p(V36) ) & ( p(V613) | ~ p(V1) ) & ( p(V532) | p(V160) ) & ( p(V4) | ~ p(V211) | ~ p(V677) ) & ( ~ p(V74) | ~ p(V27) ) & ( p(V750) | ~ p(V10) ) & ( p(V770) | ~ p(V237) ) & ( p(V689) | ~ p(V206) ) & ( ~ p(V162) | ~ p(V768) | p(V237) ) & ( ~ p(V183) | p(V578) ) & ( ~ p(V135) | ~ p(V98) ) & ( ~ p(V4) | p(V762) ) & ( ~ p(V332) | ~ p(V374) ) & ( ~ p(V3) | p(V724) ) & ( p(V8) | p(V43) ) & ( p(V370) | p(V816) ) & ( ~ p(V121) | ~ p(V134) ) & ( ~ p(V222) | ~ p(V380) | ~ p(V851) ) & ( p(V541) | ~ p(V165) ) & ( ~ p(V86) | p(V44) ) & ( p(V101) | ~ p(V27) ) & ( p(V272) | p(V271) | p(V270) | ~ p(V345) | p(V273) ) & ( p(V520) | p(V2) ) & ( p(V182) | p(V179) | ~ p(V570) ) & ( p(V115) | ~ p(V5) ) & ( p(V601) | p(V3) ) & ( p(V363) | p(V348) ) & ( ~ p(V553) | p(V204) | p(V170) | p(V203) ) & ( p(V105) | ~ p(V5) ) & ( p(V789) | p(V225) ) & ( p(V549) | ~ p(V169) ) & ( ~ p(V116) | p(V42) | p(V8) | p(V44) ) & ( p(V123) | p(V273) ) & ( p(V367) | p(V801) ) & ( ~ p(V130) | ~ p(V88) ) & ( ~ p(V374) | ~ p(V210) | ~ p(V830) ) & ( p(V853) | ~ p(V221) ) & ( ~ p(V146) | ~ p(V584) | ~ p(V152) | p(V185) ) & ( p(V743) | ~ p(V230) ) & ( p(V277) | p(V125) ) & ( ~ p(V208) | ~ p(V668) | p(V166) ) & ( ~ p(V150) | p(V606) ) & ( ~ p(V212) | p(V3) | ~ p(V681) ) & ( p(V808) | p(V192) ) & ( p(V657) | p(V205) ) & ( p(V206) | p(V662) ) & ( p(V288) | ~ p(V333) ) & ( p(V94) | p(V5) ) & ( p(V723) | p(V3) ) & ( p(V220) | p(V707) ) & ( ~ p(V13) | ~ p(V53) | p(V98) ) & ( p(V371) | p(V317) | p(V319) | p(V370) ) & ( ~ p(V269) | ~ p(V268) ) & ( ~ p(V147) | ~ p(V372) | ~ p(V823) ) & ( p(V321) | ~ p(V123) | ~ p(V322) | ~ p(V279) | ~ p(V278) ) & ( p(V846) | p(V379) ) & ( ~ p(V4) | p(V547) ) & ( ~ p(V378) | p(V845) ) & ( ~ p(V798) | ~ p(V366) | ~ p(V1) ) & ( ~ p(V128) | ~ p(V77) ) & ( p(V604) | ~ p(V191) ) & ( p(V46) | p(V5) | ~ p(V111) ) & ( p(V124) | p(V272) ) & ( p(V288) | p(V126) ) & ( p(V779) | p(V223) ) & ( p(V109) | ~ p(V44) ) & ( p(V802) | p(V188) ) & ( p(V31) | p(V14) ) & ( p(V127) | p(V73) | p(V75) | p(V126) ) & ( p(V36) | ~ p(V79) ) & ( p(V43) | ~ p(V88) ) & ( ~ p(V317) | p(V122) ) & ( ~ p(V376) | ~ p(V335) ) & ( p(V607) | ~ p(V192) ) & ( ~ p(V27) | ~ p(V4) ) & ( p(V290) | p(V125) ) & ( ~ p(V271) | ~ p(V125) ) & ( ~ p(V210) | p(V675) ) & ( ~ p(V261) | ~ p(V299) ) & ( ~ p(V367) | ~ p(V309) ) & ( ~ p(V154) | p(V644) ) & ( p(V813) | ~ p(V239) ) & ( p(V723) | ~ p(V224) ) & ( ~ p(V288) | p(V330) | ~ p(V290) ) & ( ~ p(V216) | p(V696) ) & ( p(V306) | p(V134) ) & ( ~ p(V166) | p(V543) ) & ( ~ p(V277) | ~ p(V322) ) & ( ~ p(V150) | ~ p(V607) | ~ p(V151) | p(V192) ) & ( p(V29) | p(V2) ) & ( p(V616) | ~ p(V151) ) & ( p(V508) | p(V1) ) & ( ~ p(V278) | ~ p(V124) ) & ( ~ p(V4) | ~ p(V1) | p(V65) | ~ p(V28) ) & ( ~ p(V581) | ~ p(V184) | ~ p(V12) ) & ( p(V365) | p(V357) ) & ( ~ p(V78) | ~ p(V33) ) & ( ~ p(V149) | p(V509) ) & ( ~ p(V298) | ~ p(V135) ) & ( ~ p(V226) | p(V730) ) & ( ~ p(V3) | ~ p(V764) | p(V236) ) & ( p(V603) | ~ p(V150) ) & ~ p(V11) & ( ~ p(V702) | ~ p(V218) | p(V5) ) & ( p(V7) | p(V530) ) & ( p(V206) | p(V661) ) & ( ~ p(V168) | ~ p(V754) | p(V233) ) & ( p(V2) | p(V763) ) & ( p(V717) | p(V151) ) & ( p(V155) | p(V638) ) & ( p(V186) | p(V819) ) & ( p(V776) | ~ p(V239) ) & ( p(V132) | p(V91) | p(V120) ) & ( p(V569) | p(V178) ) & ( ~ p(V156) | ~ p(V157) | ~ p(V200) | ~ p(V636) | p(V199) | ~ p(V2) ) & ( p(V546) | p(V167) ) & ( p(V48) | p(V85) | p(V87) | p(V86) | p(V129) ) & ( ~ p(V148) | p(V224) | ~ p(V721) ) & ( p(V532) | p(V8) ) & ( ~ p(V3) | ~ p(V28) ) & ( p(V521) | ~ p(V155) ) & ( ~ p(V304) | ~ p(V301) ) & ( p(V361) | p(V369) | p(V315) ) & ( p(V151) | ~ p(V616) | ~ p(V195) ) & ( p(V147) | p(V504) ) & ( p(V180) | p(V712) ) & ( ~ p(V323) | p(V324) ) & ( p(V360) | ~ p(V286) ) & ( p(V76) | ~ p(V75) ) & ( ~ p(V235) | p(V761) ) & ( ~ p(V355) | p(V126) | p(V290) ) & ( p(V149) | p(V719) ) & ( p(V78) | p(V5) | p(V33) ) & ( p(V201) | p(V640) ) & ( p(V356) | ~ p(V126) ) & ( ~ p(V126) | p(V355) ) & ( ~ p(V852) | ~ p(V147) | ~ p(V380) ) & ( p(V770) | p(V5) ) & ( ~ p(V174) | p(V704) ) & ( p(V8) | p(V542) ) & ( p(V377) | p(V841) ) & ( p(V697) | p(V230) ) & ( p(V13) | ~ p(V98) ) & ( p(V125) | p(V284) | ~ p(V350) | p(V124) ) & ( p(V820) | ~ p(V185) ) & ( p(V853) | ~ p(V380) ) & ( ~ p(V642) | ~ p(V202) | p(V201) | ~ p(V158) ) & ( p(V360) | ~ p(V288) ) & ( p(V681) | p(V212) ) & ( p(V176) | ~ p(V564) | p(V13) ) & ( ~ p(V130) | ~ p(V89) ) & ( p(V191) | ~ p(V604) | ~ p(V150) | ~ p(V148) ) & ( ~ p(V4) | p(V228) | ~ p(V738) ) & ( p(V759) | ~ p(V5) ) & ( ~ p(V85) | p(V5) ) & ( ~ p(V202) | p(V644) ) & ( p(V152) | p(V620) ) & ( ~ p(V66) | p(V2) ) & ( p(V740) | ~ p(V229) ) & ( ~ p(V688) | ~ p(V214) | ~ p(V206) ) & ( ~ p(V125) | ~ p(V320) | ~ p(V273) | ~ p(V122) | ~ p(V272) ) & ( ~ p(V3) | p(V225) | ~ p(V726) ) & ( p(V537) | ~ p(V163) ) & ( p(V124) | p(V123) | ~ p(V347) | p(V125) | p(V288) ) & ~ p(V7) & ( p(V597) | p(V148) ) & ( p(V117) | p(V24) ) & ( p(V749) | p(V10) ) & ( ~ p(V239) | p(V778) ) & ( ~ p(V1) | ~ p(V48) | p(V95) ) & ( ~ p(V153) | ~ p(V518) | ~ p(V14) ) & ( ~ p(V230) | p(V695) ) & ( ~ p(V75) | ~ p(V126) ) & ( ~ p(V526) | ~ p(V13) | ~ p(V157) ) & ( p(V155) | p(V522) ) & ( p(V44) | p(V5) ) & ( ~ p(V58) | ~ p(V14) ) & ( p(V285) | p(V129) ) & ( p(V116) | ~ p(V42) ) & ( ~ p(V287) | ~ p(V130) ) & ( p(V781) | ~ p(V237) ) & ( ~ p(V78) | p(V77) | ~ p(V35) | ~ p(V34) | ~ p(V2) ) & ( ~ p(V132) | p(V353) ) & ( ~ p(V8) | p(V531) ) & ( ~ p(V3) | p(V762) ) & ( p(V148) | ~ p(V595) | ~ p(V189) ) & ( p(V829) | ~ p(V207) ) & ( ~ p(V292) | ~ p(V373) ) & ( ~ p(V269) | ~ p(V303) ) & ( p(V5) | p(V30) ) & ( p(V588) | p(V187) ) & ( ~ p(V169) | p(V783) ) & ( ~ p(V48) | p(V109) ) & ( ~ p(V123) | p(V346) ) & ( ~ p(V148) | p(V595) ) & ( ~ p(V204) | p(V553) ) & ( p(V61) | p(V11) ) & ( p(V137) | p(V181) | ~ p(V574) ) & ( p(V583) | ~ p(V152) ) & ( p(V112) | ~ p(V2) ) & ( p(V202) | ~ p(V645) | p(V13) ) & ( p(V132) | ~ p(V327) ) & ( ~ p(V586) | p(V146) | ~ p(V186) ) & ( p(V763) | ~ p(V236) ) & ( ~ p(V46) | p(V87) | ~ p(V42) ) & ( p(V26) | ~ p(V69) ) & ( ~ p(V65) | p(V4) ) & ~ p(V13) & ( ~ p(V195) | ~ p(V615) | p(V150) ) & ( ~ p(V354) | ~ p(V364) | ~ p(V353) ) & ( p(V297) | ~ p(V342) ) & ( ~ p(V5) | p(V662) ) & ( ~ p(V317) | p(V318) ) & ( ~ p(V696) | p(V216) | p(V5) ) & ( ~ p(V7) | ~ p(V37) ) & ( p(V735) | ~ p(V168) ) & ( ~ p(V314) | p(V273) ) & ( ~ p(V359) | p(V286) | p(V284) | p(V126) ) & ( p(V829) | ~ p(V208) ) & ( ~ p(V10) | p(V109) ) & ( p(V148) | p(V604) ) & ( p(V4) | p(V76) ) & ( ~ p(V272) | ~ p(V273) | p(V317) | ~ p(V318) | ~ p(V122) ) & ( ~ p(V161) | p(V753) ) & ( p(V80) | p(V13) ) & ( ~ p(V12) | ~ p(V62) ) & ( ~ p(V368) | ~ p(V192) | ~ p(V808) ) & ( p(V727) | ~ p(V225) ) & ( p(V200) | p(V647) ) & ( ~ p(V124) | p(V358) ) & ( ~ p(V279) | p(V325) | ~ p(V278) | ~ p(V322) | ~ p(V123) ) & ( p(V55) | p(V17) ) & ( p(V772) | p(V164) ) & ~ p(V14) & ( p(V5) | p(V2) | ~ p(V759) | ~ p(V234) ) & ( p(V534) | p(V1) ) & ( ~ p(V340) | p(V126) ) & ( ~ p(V5) | p(V680) ) & ( p(V4) | p(V548) ) & ( p(V632) | p(V199) ) & ( p(V184) | p(V581) ) & ( p(V757) | ~ p(V234) ) & ( p(V365) | p(V340) | p(V378) ) & ( p(V709) | p(V175) ) & ( p(V1) | ~ p(V73) ) & ( p(V122) | ~ p(V339) ) & ( p(V845) | ~ p(V243) ) & ( p(V634) | ~ p(V157) ) & ( ~ p(V269) | ~ p(V368) ) & ( ~ p(V66) | ~ p(V123) ) & ( p(V171) | ~ p(V554) | p(V12) ) & ( ~ p(V846) | ~ p(V219) | ~ p(V379) ) & ( ~ p(V598) | ~ p(V190) | p(V1) ) & ( ~ p(V147) | p(V505) ) & ( p(V40) | p(V2) ) & ( p(V611) | ~ p(V194) ) & ( ~ p(V286) | ~ p(V124) ) & ( p(V147) | p(V809) ) & ( ~ p(V97) | ~ p(V135) ) & ( p(V591) | ~ p(V187) ) & ( ~ p(V330) | p(V290) ) & ( p(V294) | p(V131) ) & ( p(V2) | p(V32) ) & ( ~ p(V324) | ~ p(V280) | p(V323) ) & ( p(V362) | p(V360) ) & ( p(V598) | ~ p(V1) ) & ( ~ p(V127) | ~ p(V126) ) & ( p(V150) | ~ p(V603) | ~ p(V191) ) & ( p(V120) | p(V109) ) & ( ~ p(V14) | ~ p(V573) | ~ p(V180) ) & ( p(V274) | ~ p(V307) ) & ( p(V203) | p(V651) ) & ( p(V126) | ~ p(V328) ) & ( ~ p(V704) | p(V174) | ~ p(V219) ) & ( ~ p(V9) | p(V545) ) & ( p(V574) | ~ p(V181) ) & ( ~ p(V177) | ~ p(V139) | ~ p(V567) ) & ( p(V241) | ~ p(V786) | p(V226) ) & ( p(V834) | p(V212) ) & ( p(V2) | p(V594) ) & ( p(V5) | ~ p(V662) | ~ p(V206) ) & ( p(V691) | p(V215) ) & ( p(V168) | ~ p(V208) | ~ p(V667) ) & ( ~ p(V158) | p(V640) ) & ( ~ p(V174) | ~ p(V175) | ~ p(V561) ) & ( ~ p(V129) | ~ p(V281) ) & ( ~ p(V8) | p(V775) ) & ( p(V94) | p(V108) ) & ( ~ p(V583) | p(V152) | ~ p(V185) ) & ( ~ p(V226) | p(V731) ) & ( p(V47) | ~ p(V91) ) & ( p(V549) | ~ p(V170) ) & ( ~ p(V366) | ~ p(V269) ) & ( p(V297) | p(V299) ) & ( ~ p(V53) | ~ p(V52) ) & ( p(V286) | ~ p(V328) ) & ( p(V810) | ~ p(V191) ) & ( p(V839) | ~ p(V213) ) & ( p(V765) | ~ p(V236) ) & ( ~ p(V133) | ~ p(V93) ) & ( ~ p(V225) | ~ p(V789) | ~ p(V226) | ~ p(V169) | ~ p(V227) | ~ p(V241) ) & ( p(V223) | p(V720) ) & ( ~ p(V297) | ~ p(V299) ) & ( ~ p(V202) | p(V645) ) & ( p(V794) | ~ p(V234) ) & ( p(V790) | ~ p(V231) ) & ( p(V600) | ~ p(V3) ) & ( p(V34) | ~ p(V81) ) & ( p(V587) | p(V153) ) & ( ~ p(V516) | ~ p(V5) | ~ p(V152) ) & ( p(V767) | ~ p(V3) ) & ( p(V849) | ~ p(V219) ) & ( ~ p(V73) | p(V74) ) & ( ~ p(V778) | p(V146) | p(V239) ) & ( ~ p(V29) | ~ p(V4) | ~ p(V1) | ~ p(V28) | ~ p(V76) ) & ( p(V203) | p(V650) ) & ( p(V29) | ~ p(V73) ) & ( p(V177) | ~ p(V562) | p(V175) ) & ( p(V716) | p(V148) ) & ( p(V3) | p(V540) ) & ( p(V3) | p(V150) | ~ p(V511) ) & ( p(V6) | p(V36) ) & ( ~ p(V181) | ~ p(V575) | ~ p(V137) ) & ( ~ p(V29) | p(V67) | ~ p(V26) ) & ( p(V341) | p(V269) | p(V379) | p(V342) ) & ( p(V148) | ~ p(V602) | ~ p(V191) ) & ( p(V345) | ~ p(V273) ) & ( p(V5) | p(V200) | p(V155) | ~ p(V639) ) & ( p(V193) | p(V608) ) & ( ~ p(V96) | ~ p(V134) ) & ( p(V169) | p(V797) ) & ( p(V147) | p(V804) ) & ( p(V555) | p(V171) ) & ( ~ p(V182) | p(V570) ) & ( p(V74) | p(V27) | p(V30) ) & ( p(V694) | ~ p(V229) ) & ( p(V511) | ~ p(V150) ) & ( p(V347) | ~ p(V288) ) & ( p(V268) | ~ p(V308) ) & ( p(V586) | ~ p(V146) ) & ( p(V343) | ~ p(V302) | ~ p(V300) ) & ( ~ p(V590) | p(V4) | ~ p(V187) ) & ( p(V671) | p(V209) ) & ( ~ p(V147) | p(V824) ) & ( ~ p(V77) | p(V2) ) & ( p(V559) | p(V173) ) & ( ~ p(V4) | ~ p(V149) | ~ p(V510) ) & ( ~ p(V3) | p(V523) ) & ~ p(V5) & ( ~ p(V123) | p(V347) ) & ( p(V790) | ~ p(V242) ) & ( p(V166) | p(V728) ) & ( p(V298) | ~ p(V341) ) & ( p(V4) | p(V591) ) & ( p(V838) | p(V242) ) & ( ~ p(V372) | ~ p(V321) ) & ( ~ p(V321) | p(V322) ) & ( p(V503) | ~ p(V147) ) & ( p(V80) | p(V32) ) & ( p(V665) | ~ p(V163) ) & ( p(V288) | ~ p(V330) ) & ( ~ p(V85) | p(V41) ) & ( p(V357) | ~ p(V125) ) & ( p(V210) | ~ p(V675) | ~ p(V165) | ~ p(V4) ) & ( p(V291) | p(V365) ) & ( ~ p(V170) | ~ p(V552) | ~ p(V204) ) & ( ~ p(V232) | p(V752) ) & ( ~ p(V284) | p(V350) ) & ( ~ p(V368) | ~ p(V190) | ~ p(V806) ) & ( p(V844) | p(V378) ) & ( p(V572) | ~ p(V180) ) & ( p(V740) | p(V164) ) & ( p(V664) | p(V207) ) & ( ~ p(V216) | ~ p(V169) | ~ p(V692) | p(V215) ) & ( p(V124) | p(V286) ) & ( p(V791) | ~ p(V242) ) & ( p(V677) | ~ p(V4) ) & ( ~ p(V296) | p(V341) | ~ p(V298) ) & ( p(V825) | p(V207) ) & ( p(V137) | p(V575) ) & ( ~ p(V220) | p(V709) ) & ( p(V14) | ~ p(V572) | p(V180) ) & ( p(V182) | p(V577) ) & ( p(V195) | ~ p(V817) | p(V249) | p(V370) | p(V197) ) & ( p(V702) | ~ p(V5) ) & ( ~ p(V3) | p(V729) ) & ( p(V274) | p(V271) | p(V318) ) & ( ~ p(V2) | p(V103) ) & ( ~ p(V596) | ~ p(V189) | p(V151) ) & ( p(V2) | p(V636) ) & ( p(V2) | ~ p(V68) ) & ( p(V676) | p(V211) ) & ( p(V115) | p(V118) ) & ( p(V380) | p(V343) | p(V344) | p(V269) ) & ( p(V46) | ~ p(V87) ) & ( p(V195) | p(V616) ) & ( p(V238) | p(V775) ) & ( p(V594) | p(V1) ) & ( ~ p(V122) | ~ p(V1) ) & ( p(V529) | ~ p(V159) ) & ( p(V582) | ~ p(V146) ) & ( p(V700) | p(V170) ) & ( p(V42) | p(V3) ) & ( p(V4) | p(V675) ) & ( p(V150) | p(V198) | ~ p(V628) ) & ( p(V311) | ~ p(V273) | ~ p(V270) ) & ( ~ p(V848) | ~ p(V379) | ~ p(V147) ) & ( p(V1) | ~ p(V95) ) & ( ~ p(V291) | p(V354) ) & ( ~ p(V652) | ~ p(V156) | p(V203) | ~ p(V157) | ~ p(V200) | ~ p(V2) ) & ( p(V170) | p(V746) ) & ( p(V308) | p(V307) | p(V371) ) & ( p(V650) | ~ p(V157) ) & ( p(V166) | p(V669) ) & ( p(V34) | p(V3) ) & ( p(V622) | ~ p(V152) ) & ( p(V630) | ~ p(V198) ) & ( p(V218) | p(V701) ) & ( ~ p(V228) | p(V3) | ~ p(V739) | p(V4) | p(V162) ) & ( ~ p(V234) | ~ p(V243) | ~ p(V797) | ~ p(V235) | ~ p(V233) | ~ p(V169) ) & ( p(V102) | ~ p(V26) ) & ( ~ p(V713) | ~ p(V222) | p(V179) ) & ( ~ p(V292) | p(V353) ) & ( ~ p(V125) | ~ p(V117) ) & ( p(V768) | ~ p(V237) ) & ( p(V232) | p(V242) | ~ p(V791) ) & ( p(V658) | ~ p(V10) ) & ( ~ p(V563) | ~ p(V177) | ~ p(V175) ) & ( ~ p(V181) | ~ p(V506) | ~ p(V147) ) & ( p(V849) | ~ p(V220) ) & ( ~ p(V378) | ~ p(V340) ) & ( p(V176) | p(V565) ) & ( p(V619) | p(V1) ) & ( p(V720) | ~ p(V148) ) & ( p(V222) | p(V713) ) & ( ~ p(V216) | p(V691) ) & ( p(V647) | p(V154) ) & ( ~ p(V53) | ~ p(V55) ) & ( ~ p(V717) | p(V223) | ~ p(V151) ) & ~ p(V12) & ( p(V5) | ~ p(V105) | p(V46) ) & ( p(V54) | ~ p(V97) ) & ( ~ p(V218) | p(V703) ) & ( ~ p(V79) | ~ p(V128) ) & ( ~ p(V25) | ~ p(V123) ) & ( p(V690) | p(V215) ) & ( ~ p(V678) | ~ p(V166) | p(V211) | ~ p(V4) ) & ( ~ p(V46) | p(V108) ) & ( p(V157) | ~ p(V199) | ~ p(V634) ) & ( p(V659) | p(V3) ) & ( p(V269) | p(V268) ) & ( p(V28) | ~ p(V73) ) & ( p(V3) | p(V524) ) & ( p(V14) | p(V715) ) & ( p(V805) | ~ p(V188) ) & ( p(V655) | p(V202) ) & ( p(V806) | p(V368) ) & ( p(V205) | p(V687) ) & ( p(V226) | ~ p(V168) | ~ p(V730) ) & ( ~ p(V5) | p(V206) | ~ p(V162) | ~ p(V663) | ~ p(V164) ) & ( ~ p(V11) | p(V578) ) & ( p(V136) | p(V275) ) & ( ~ p(V138) | p(V576) ) & ( p(V611) | ~ p(V3) ) & ( p(V711) | ~ p(V180) ) & ( p(V230) | p(V745) ) & ( ~ p(V7) | ~ p(V41) ) & ( ~ p(V366) | p(V800) ) & ( ~ p(V550) | ~ p(V170) | ~ p(V169) ) & ( p(V536) | p(V2) ) & ( ~ p(V87) | p(V42) ) & ( p(V10) | p(V173) | ~ p(V558) ) & ( p(V133) | p(V93) | p(V95) ) & ( ~ p(V208) | p(V669) ) & ( p(V852) | p(V147) ) & ( ~ p(V215) | p(V842) ) & ( p(V166) | p(V766) ) & ( p(V4) | p(V678) ) & ( ~ p(V269) | ~ p(V367) ) & ( p(V759) | p(V234) ) & ( p(V739) | ~ p(V4) ) & ( p(V727) | p(V4) ) & ( ~ p(V125) | ~ p(V277) ) & ( ~ p(V57) | ~ p(V56) ) & ( p(V665) | p(V207) ) & ( p(V571) | p(V182) ) & ( ~ p(V24) | ~ p(V25) ) & ( p(V565) | p(V13) ) & ( ~ p(V839) | p(V376) | p(V242) | p(V213) ) & ( ~ p(V807) | ~ p(V191) | ~ p(V368) ) & ( p(V791) | ~ p(V232) ) & ( p(V125) | p(V123) | ~ p(V358) | p(V124) | p(V288) ) & ( p(V230) | ~ p(V695) | p(V216) ) & ( p(V3) | p(V760) ) & ( p(V550) | p(V169) ) & ( ~ p(V288) | p(V358) ) & ( ~ p(V59) | ~ p(V15) ) & ( p(V180) | ~ p(V221) | ~ p(V711) ) & ( ~ p(V290) | p(V331) | ~ p(V286) ) & ( p(V124) | p(V278) ) & ( p(V150) | p(V718) ) & ( p(V151) | ~ p(V513) | p(V2) ) & ( ~ p(V363) | ~ p(V375) ) & ( ~ p(V179) | p(V713) ) & ( ~ p(V522) | ~ p(V155) | ~ p(V4) ) & ( ~ p(V274) | ~ p(V126) ) & ( ~ p(V168) | p(V756) ) & ( p(V684) | ~ p(V169) ) & ( p(V332) | ~ p(V287) | ~ p(V125) ) & ( ~ p(V515) | p(V152) | p(V5) ) & ( p(V302) | ~ p(V343) ) & ( p(V200) | p(V636) ) & ( p(V853) | ~ p(V147) ) & ( ~ p(V25) | ~ p(V128) ) & ( p(V102) | p(V117) ) & ( p(V580) | ~ p(V184) ) & ( ~ p(V5) | ~ p(V200) | ~ p(V637) ) & ( p(V540) | p(V164) ) & ( p(V666) | p(V163) ) & ( ~ p(V183) | ~ p(V579) | ~ p(V11) ) & ( ~ p(V549) | p(V170) | p(V169) ) & ( p(V249) | p(V816) ) & ( p(V162) | ~ p(V660) | ~ p(V206) ) & ( p(V79) | p(V128) | p(V25) | p(V77) ) & ( ~ p(V2) | p(V724) ) & ( ~ p(V3) | p(V114) ) & ( p(V365) | p(V355) ) & ( ~ p(V760) | p(V235) | ~ p(V3) ) & ( p(V166) | p(V544) ) & ( p(V179) | p(V571) ) & ( p(V4) | p(V522) ) & ( ~ p(V242) | p(V839) ) & ( p(V348) | ~ p(V290) ) & ( p(V119) | p(V105) ) & ( ~ p(V124) | ~ p(V289) | ~ p(V126) | p(V334) ) & ( p(V96) | ~ p(V5) | ~ p(V49) ) & ( ~ p(V124) | p(V357) ) & ( ~ p(V362) | ~ p(V374) ) & ( p(V85) | ~ p(V5) | ~ p(V41) ) & ( p(V124) | p(V316) ) & ( p(V147) | p(V219) | ~ p(V849) | p(V379) | p(V220) ) & ( p(V767) | ~ p(V4) ) & ( p(V229) | p(V742) ) & ( ~ p(V822) | ~ p(V372) | ~ p(V201) ) & ( p(V1) | p(V798) ) & ( p(V320) | p(V125) ) & ( ~ p(V699) | p(V170) | ~ p(V217) ) & ( ~ p(V158) | p(V527) ) & ( ~ p(V129) | ~ p(V87) ) & ( ~ p(V344) | p(V136) ) & ( p(V214) | p(V686) ) & ( ~ p(V194) | ~ p(V1) | ~ p(V2) | ~ p(V614) | ~ p(V3) ) & ( p(V189) | p(V595) ) & ( ~ p(V46) | p(V104) ) & ( ~ p(V370) | ~ p(V249) | ~ p(V816) ) & ( p(V627) | ~ p(V198) ) & ( ~ p(V209) | ~ p(V827) | ~ p(V373) ) & ( p(V188) | p(V593) ) & ( p(V154) | p(V2) | ~ p(V519) ) & ( p(V213) | p(V837) ) & ( p(V13) | p(V709) ) & ( ~ p(V844) | ~ p(V378) | ~ p(V243) ) & ( p(V153) | p(V518) ) & ( p(V211) | p(V677) ) & ( p(V190) | p(V806) ) & ( p(V53) | p(V55) ) & ( p(V161) | p(V752) ) & ( ~ p(V377) | ~ p(V339) ) & ( p(V168) | p(V743) ) & ( p(V827) | p(V373) ) & ( ~ p(V148) | p(V507) ) & ( ~ p(V325) | p(V279) ) & ( p(V761) | p(V4) ) & ( ~ p(V372) | ~ p(V269) ) & ~ p(V10) & ( ~ p(V527) | p(V158) | p(V6) ) & ( p(V817) | ~ p(V249) ) & ( p(V148) | p(V3) | ~ p(V724) | ~ p(V224) | p(V2) ) & ( p(V149) | p(V151) | ~ p(V223) | p(V148) | ~ p(V720) | p(V150) ) & ( ~ p(V25) | ~ p(V59) ) & ( ~ p(V533) | p(V161) | p(V1) ) & ( p(V556) | ~ p(V9) ) & ( ~ p(V182) | ~ p(V571) | ~ p(V179) ) & ( ~ p(V207) | ~ p(V373) | ~ p(V825) ) & ( ~ p(V361) | ~ p(V369) ) & ( p(V236) | p(V240) | ~ p(V780) ) & ( ~ p(V80) | p(V82) | ~ p(V36) ) & ( ~ p(V232) | p(V751) ) & ( ~ p(V154) | p(V519) ) & ( p(V631) | p(V151) ) & ( ~ p(V96) | p(V49) ) & ( p(V529) | ~ p(V7) ) & ( p(V516) | p(V152) ) & ( ~ p(V44) | p(V86) | ~ p(V46) ) & ( ~ p(V5) | ~ p(V78) ) & ( ~ p(V238) | p(V164) | p(V8) | p(V166) | ~ p(V775) ) & ( p(V748) | ~ p(V231) ) & ( p(V552) | p(V170) ) & ( ~ p(V236) | ~ p(V767) | p(V166) | p(V2) | p(V3) | p(V4) ) & ( p(V200) | p(V202) | ~ p(V646) ) & ( p(V364) | p(V353) ) & ( ~ p(V599) | p(V2) | ~ p(V190) ) & ( p(V622) | ~ p(V149) ) & ( ~ p(V840) | ~ p(V215) | ~ p(V377) ) & ( p(V299) | p(V261) ) & ( p(V843) | p(V378) ) & ( p(V117) | p(V101) ) & ( p(V153) | ~ p(V197) | ~ p(V624) ) & ( ~ p(V150) | p(V195) | ~ p(V196) | ~ p(V619) | ~ p(V1) | ~ p(V151) ) & ( p(V30) | ~ p(V63) ) & ( ~ p(V162) | p(V771) ) & ( p(V824) | ~ p(V201) ) & ( ~ p(V327) | p(V126) ) & ( ~ p(V156) | p(V648) ) & ( ~ p(V92) | ~ p(V83) ) & ( p(V168) | p(V548) ) & ( p(V851) | p(V380) ) & ( ~ p(V168) | p(V750) ) & ( ~ p(V3) | p(V102) ) & ( p(V512) | p(V150) ) & ( p(V130) | p(V288) | p(V286) | ~ p(V360) ) & ( ~ p(V283) | ~ p(V122) ) & ( p(V233) | p(V756) ) & ( ~ p(V188) | p(V2) | ~ p(V593) ) & ( p(V284) | ~ p(V328) ) & ( ~ p(V684) | ~ p(V213) | p(V169) ) & ( p(V78) | ~ p(V81) ) & ( p(V66) | ~ p(V1) | ~ p(V2) ) & ( ~ p(V282) | ~ p(V130) ) & ( ~ p(V8) | p(V238) | ~ p(V774) ) & ( ~ p(V785) | p(V225) | p(V241) ) & ( p(V605) | ~ p(V151) ) & ( p(V632) | ~ p(V156) ) & ( ~ p(V336) | ~ p(V291) | p(V335) | ~ p(V290) ) & ( p(V603) | p(V191) ) & ( p(V216) | p(V692) ) & ( ~ p(V178) | ~ p(V180) | ~ p(V712) | p(V221) ) & ( ~ p(V243) | p(V794) ) & ( p(V672) | p(V168) ) & ( ~ p(V193) | ~ p(V608) | p(V149) ) & ( ~ p(V360) | ~ p(V358) | ~ p(V362) | ~ p(V359) | ~ p(V291) ) & ( ~ p(V30) | ~ p(V5) ) & ( p(V234) | ~ p(V758) | ~ p(V5) ) & ( p(V231) | ~ p(V747) | ~ p(V168) ) & ( ~ p(V597) | ~ p(V148) | p(V189) | ~ p(V151) ) & ( p(V669) | p(V168) ) & ( ~ p(V9) | ~ p(V45) ) & ( p(V346) | ~ p(V270) ) & ( ~ p(V203) | p(V553) ) & ( p(V524) | p(V156) ) & ( p(V631) | p(V4) ) & ( ~ p(V237) | ~ p(V240) | ~ p(V169) | ~ p(V238) | ~ p(V236) | ~ p(V784) ) & ( ~ p(V135) | ~ p(V297) | p(V342) ) & ( p(V126) | p(V290) | ~ p(V349) ) & ( p(V193) | ~ p(V194) | ~ p(V149) | ~ p(V610) ) & ( p(V359) | ~ p(V126) ) & ( p(V185) | p(V583) ) & ( ~ p(V239) | ~ p(V223) | ~ p(V224) | ~ p(V779) | ~ p(V146) ) & ( ~ p(V190) | p(V601) ) & ( ~ p(V200) | p(V639) ) & ( ~ p(V4) | p(V674) ) & ( ~ p(V203) | p(V652) ) & ( ~ p(V333) | ~ p(V374) ) & ( p(V126) | p(V274) ) & ( ~ p(V84) | ~ p(V92) ) & ( p(V366) | p(V799) ) & ( p(V828) | p(V373) ) & ( p(V748) | p(V166) ) & ( p(V331) | p(V330) | p(V373) | p(V292) | p(V329) ) & ( p(V784) | p(V240) ) & ( p(V739) | ~ p(V3) ) & ( ~ p(V3) | ~ p(V34) ) & ( p(V717) | ~ p(V223) ) & ( p(V668) | ~ p(V166) ) & ( p(V122) | p(V269) | p(V366) ) & ( p(V636) | p(V157) ) & ( ~ p(V205) | ~ p(V656) | p(V3) ) & ( p(V700) | ~ p(V217) ) & ( p(V301) | ~ p(V344) ) & ( p(V377) | p(V840) ) & ( ~ p(V340) | p(V293) ) & ( ~ p(V218) | p(V845) ) & ( p(V227) | p(V735) ) & ( ~ p(V25) | ~ p(V135) ) & ( ~ p(V136) | ~ p(V25) ) & ( p(V523) | ~ p(V156) ) & ( p(V106) | ~ p(V4) ) & ( p(V533) | ~ p(V161) ) & ( ~ p(V613) | p(V194) | p(V1) ) & ( p(V241) | p(V169) | ~ p(V788) ) & ( p(V749) | ~ p(V231) ) & ( p(V544) | p(V5) ) & ( p(V577) | p(V138) ) & ( ~ p(V195) | p(V817) ) & ( p(V289) | p(V131) ) & ( p(V612) | ~ p(V2) ) & ( p(V182) | ~ p(V576) | p(V138) ) & ( p(V683) | p(V213) ) & ( ~ p(V313) | p(V272) ) & ( ~ p(V343) | ~ p(V380) ) & ( p(V714) | ~ p(V14) ) & ( p(V200) | p(V652) ) & ( p(V655) | p(V158) ) & ( p(V585) | p(V186) ) & ( p(V105) | ~ p(V46) ) & ( ~ p(V125) | ~ p(V290) ) & ( p(V350) | ~ p(V125) ) & ( p(V13) | p(V157) | ~ p(V525) ) & ( p(V301) | p(V300) ) & ( p(V837) | p(V376) ) & ( ~ p(V333) | p(V125) ) & ( p(V51) | p(V10) ) & ( ~ p(V46) | p(V109) ) & ( ~ p(V177) | p(V566) ) & ( p(V177) | p(V567) ) & ( ~ p(V377) | ~ p(V217) | ~ p(V841) ) & ( p(V289) | ~ p(V334) ) & ( ~ p(V718) | ~ p(V150) | p(V223) ) & ( ~ p(V795) | p(V243) | p(V235) ) & ( ~ p(V364) | ~ p(V376) ) & ( p(V661) | ~ p(V164) ) & ( p(V755) | p(V5) ) & ( ~ p(V7) | ~ p(V538) | ~ p(V163) ) & ( ~ p(V189) | p(V597) ) & ( p(V836) | ~ p(V241) ) & ( p(V596) | ~ p(V151) ) & ( p(V198) | p(V4) | ~ p(V627) ) & ( ~ p(V133) | ~ p(V305) ) & ( p(V784) | p(V236) ) & ( ~ p(V509) | p(V4) | p(V149) ) & ( p(V553) | ~ p(V170) ) & ( p(V164) | p(V663) ) & ( p(V352) | p(V338) ) & ( p(V112) | ~ p(V5) ) & ( ~ p(V8) | ~ p(V43) ) & ( p(V192) | p(V191) | p(V190) | ~ p(V810) | p(V147) | p(V368) ) & ( p(V705) | p(V219) ) & ( p(V601) | p(V2) ) & ( ~ p(V71) | ~ p(V125) ) & ( p(V563) | p(V177) ) & ( ~ p(V3) | p(V103) ) & ( p(V687) | p(V214) ) & ( p(V3) | p(V164) | ~ p(V539) ) & ( ~ p(V352) | ~ p(V126) | ~ p(V338) | ~ p(V351) | ~ p(V350) ) & ( ~ p(V5) | ~ p(V734) | p(V227) ) & ( p(V46) | ~ p(V86) ) & ( ~ p(V5) | p(V735) ) & ( p(V190) | p(V598) ) & ( p(V174) | p(V561) ) & ( p(V762) | p(V235) ) & ( p(V345) | ~ p(V271) ) & ( ~ p(V325) | ~ p(V292) ) & ( p(V118) | p(V116) ) & ( ~ p(V146) | ~ p(V147) | ~ p(V504) ) & ( p(V168) | ~ p(V750) | p(V10) | p(V170) | ~ p(V231) | p(V166) ) & ( ~ p(V167) | p(V679) ) & ( p(V241) | p(V789) ) & ( p(V564) | ~ p(V13) ) & ( ~ p(V125) | p(V358) ) & ( p(V33) | p(V4) ) & ( ~ p(V647) | ~ p(V202) | ~ p(V200) | ~ p(V13) | ~ p(V154) | ~ p(V156) ) & ( ~ p(V125) | p(V347) ) & ( p(V101) | ~ p(V29) ) & ( p(V217) | p(V699) ) & ( p(V5) | p(V682) ) & ( p(V110) | p(V120) ) & ( p(V149) | p(V510) ) & ( ~ p(V196) | ~ p(V621) | ~ p(V149) ) & ( p(V340) | ~ p(V293) | ~ p(V126) ) & ( p(V4) | p(V3) | ~ p(V113) ) & ( ~ p(V367) | ~ p(V187) | ~ p(V801) ) & ( p(V325) | p(V326) | p(V292) ) & ( p(V704) | p(V219) ) & ( p(V359) | ~ p(V286) ) & ( ~ p(V3) | ~ p(V2) | ~ p(V72) | ~ p(V1) ) & ( p(V771) | p(V237) ) & ( ~ p(V151) | p(V720) ) & ( p(V584) | p(V152) ) & ( p(V518) | p(V14) ) & ( ~ p(V671) | p(V168) | ~ p(V209) ) & ( ~ p(V131) | ~ p(V294) ) & ( p(V167) | p(V682) ) & ( ~ p(V189) | ~ p(V803) | ~ p(V367) ) & ( p(V612) | ~ p(V194) ) & ( p(V197) | p(V815) ) & ( p(V733) | ~ p(V227) ) & ( ~ p(V153) | p(V624) ) & ( ~ p(V9) | ~ p(V557) | ~ p(V172) ) & ( p(V209) | p(V670) ) & ( p(V122) | p(V25) | p(V1) ) & ( p(V744) | p(V11) ) & ( p(V169) | p(V692) ) & ( ~ p(V125) | p(V333) | ~ p(V288) ) & ( p(V170) | p(V373) | p(V208) | p(V209) | ~ p(V829) | p(V207) ) & ( p(V273) | ~ p(V311) ) & ( p(V186) | ~ p(V587) | ~ p(V153) | ~ p(V146) ) & ( p(V649) | p(V203) ) & ( ~ p(V5) | ~ p(V770) | p(V237) ) & ( ~ p(V38) | ~ p(V8) ) & ~ p(V2) & ( ~ p(V124) | p(V347) ) & ( p(V670) | ~ p(V164) ) & ( p(V218) | ~ p(V703) | ~ p(V5) | ~ p(V171) ) & ( ~ p(V126) | ~ p(V322) ) & ( p(V88) | p(V118) | p(V89) | p(V130) ) & ( p(V775) | ~ p(V164) ) & ( p(V750) | p(V231) ) & ( ~ p(V2) | p(V593) ) & ( ~ p(V151) | p(V513) ) & ( ~ p(V1) | ~ p(V508) | ~ p(V148) ) & ( p(V12) | p(V581) ) & ( p(V833) | ~ p(V211) ) & ( p(V320) | ~ p(V319) ) & ( p(V210) | p(V830) ) & ( p(V117) | p(V125) | p(V71) ) & ( ~ p(V600) | ~ p(V190) | p(V3) ) & ( p(V49) | p(V12) ) & ( p(V706) | ~ p(V219) ) & ( ~ p(V147) | p(V849) ) & ( ~ p(V150) | p(V720) ) & ( p(V191) | p(V807) ) & ( p(V663) | ~ p(V206) ) & ( ~ p(V297) | ~ p(V296) ) & ( p(V11) | p(V168) | ~ p(V230) | ~ p(V745) ) & ( p(V836) | ~ p(V375) ) & ( p(V594) | ~ p(V188) ) & ( p(V685) | ~ p(V214) ) & ( ~ p(V302) | ~ p(V136) ) & ( p(V221) | p(V850) ) & ( ~ p(V514) | ~ p(V2) | ~ p(V151) ) & ( p(V365) | p(V356) ) & ( ~ p(V2) | p(V513) ) & ( ~ p(V578) | p(V11) | p(V183) ) & ( ~ p(V205) | ~ p(V214) | ~ p(V687) ) & ( ~ p(V68) | p(V3) ) & ( ~ p(V376) | ~ p(V838) | ~ p(V242) ) & ( p(V199) | p(V821) ) & ( ~ p(V123) | ~ p(V273) ) & ( p(V2) | p(V4) | p(V3) | ~ p(V114) | p(V44) ) & ( ~ p(V293) | ~ p(V134) ) & ( p(V628) | ~ p(V150) ) & ( ~ p(V369) | ~ p(V811) | ~ p(V193) ) & ( ~ p(V123) | ~ p(V67) ) & ( p(V5) | ~ p(V83) ) & ( p(V514) | p(V151) ) & ( p(V351) | ~ p(V286) ) & ( p(V2) | p(V162) | ~ p(V535) ) & ( p(V758) | ~ p(V234) ) & ( p(V202) | ~ p(V643) | p(V156) ) & ( ~ p(V40) | p(V106) ) & ( ~ p(V605) | p(V151) | ~ p(V192) ) & ( p(V741) | ~ p(V229) ) & ( ~ p(V30) | ~ p(V31) | p(V75) | ~ p(V76) ) & ( ~ p(V147) | p(V805) ) & ( ~ p(V290) | p(V352) ) & ( p(V187) | p(V801) ) & ( p(V347) | p(V363) ) & ( p(V338) | p(V126) ) & ( p(V800) | ~ p(V147) ) & ( p(V147) | p(V506) ) & ( p(V738) | ~ p(V228) ) & ( ~ p(V124) | ~ p(V25) ) & ( p(V795) | ~ p(V243) ) & ( ~ p(V2) | p(V633) ) & ( p(V697) | p(V229) ) & ( p(V797) | p(V243) ) & ( ~ p(V372) | ~ p(V323) ) & ( p(V165) | p(V542) ) & ( ~ p(V64) | ~ p(V127) ) & ( p(V301) | p(V304) ) & ( p(V3) | p(V28) ) & ( p(V582) | p(V185) ) & ( ~ p(V152) | p(V515) ) & ( p(V720) | ~ p(V149) ) & ( ~ p(V644) | p(V202) | p(V154) ) & ( ~ p(V82) | ~ p(V48) ) & ( p(V706) | p(V176) ) & ( p(V526) | p(V157) ) & ( p(V732) | ~ p(V168) ) & ( ~ p(V555) | ~ p(V171) | ~ p(V12) ) & ( ~ p(V170) | ~ p(V828) | ~ p(V373) ) & ( ~ p(V43) | ~ p(V4) | p(V88) ) & ( p(V516) | p(V5) ) & ( ~ p(V705) | p(V176) | ~ p(V219) ) & ( p(V338) | ~ p(V337) ) & ( p(V38) | p(V8) ) & ( p(V203) | p(V648) ) & ( p(V217) | p(V841) ) & ~ p(V1) & ( p(V787) | ~ p(V227) ) & ( p(V703) | p(V171) ) & ( p(V3) | p(V614) ) & ( ~ p(V709) | ~ p(V13) | ~ p(V175) | p(V220) ) & ( ~ p(V36) | ~ p(V80) | p(V79) ) & ( p(V375) | p(V834) ) & ( p(V742) | ~ p(V11) ) & ( ~ p(V200) | p(V635) ) & ( ~ p(V1) | p(V533) ) & ( ~ p(V187) | p(V805) ) & ( ~ p(V202) | p(V646) ) & ( p(V126) | p(V322) | p(V277) ) & ( p(V192) | p(V605) ) & ( p(V229) | p(V216) | ~ p(V694) ) & ( ~ p(V658) | p(V10) | ~ p(V205) ) & ( p(V194) | p(V3) | ~ p(V611) ) & ( ~ p(V138) | ~ p(V577) | ~ p(V182) ) & ( ~ p(V2) | ~ p(V40) ) & ( ~ p(V120) | ~ p(V132) ) & ( p(V125) | p(V271) ) & ( p(V195) | p(V615) ) & ( p(V379) | p(V847) ) & ( ~ p(V110) | p(V39) | p(V47) ) & ( p(V842) | ~ p(V377) ) & ( p(V205) | p(V656) ) & ( p(V316) | ~ p(V315) ) & ( p(V9) | p(V172) | ~ p(V556) ) & ( p(V364) | p(V354) ) & ( p(V369) | p(V812) ) & ( p(V852) | p(V380) ) & ( p(V760) | ~ p(V235) ) & ( ~ p(V380) | ~ p(V344) ) & ( p(V227) | ~ p(V787) | p(V241) ) & ( p(V800) | ~ p(V1) ) & ( ~ p(V689) | p(V214) | p(V205) | p(V206) ) & ( p(V121) | p(V47) ) & ( p(V273) | p(V320) ) & ( p(V546) | p(V9) ) & ( p(V235) | ~ p(V4) | ~ p(V761) ) & ( p(V192) | p(V606) ) & ( p(V147) | p(V823) ) & ( ~ p(V152) | ~ p(V196) | ~ p(V620) ) & ( p(V590) | ~ p(V4) ) & ( p(V663) | p(V162) ) & ( p(V237) | ~ p(V769) | ~ p(V164) ) & ( ~ p(V196) | p(V618) ) & ( p(V338) | p(V351) ) & ( p(V797) | p(V235) ) & ( p(V716) | ~ p(V223) ) & ( ~ p(V6) | ~ p(V158) | ~ p(V528) ) & ( p(V789) | p(V227) ) & ( p(V198) | ~ p(V197) | ~ p(V625) ) & ( ~ p(V380) | ~ p(V850) | ~ p(V221) ) & ( ~ p(V9) | ~ p(V50) ) & ( ~ p(V97) | p(V52) ) & ( p(V280) | ~ p(V326) ) & ( p(V197) | p(V623) ) & ( p(V59) | p(V15) ) & ( ~ p(V106) | p(V4) | p(V40) | p(V3) ) & ( ~ p(V65) | ~ p(V123) ) & ( ~ p(V222) | p(V715) ) & ( ~ p(V137) | p(V574) ) & ( ~ p(V226) | p(V786) ) & ( p(V370) | p(V815) ) & ( p(V556) | ~ p(V172) ) & ( p(V715) | p(V179) ) & ( p(V818) | p(V185) ) & ( ~ p(V5) | p(V233) | ~ p(V755) ) & ( ~ p(V126) | ~ p(V288) ) & ( p(V698) | p(V217) ) & ( ~ p(V155) | ~ p(V200) | ~ p(V638) ) & ( ~ p(V377) | ~ p(V337) ) & ( p(V90) | p(V131) | p(V119) ) & ( p(V751) | p(V169) ) & ( p(V1) | p(V591) ) & ( p(V1) | ~ p(V195) | ~ p(V617) ) & ( ~ p(V223) | p(V776) ) & ( p(V126) | ~ p(V329) ) & ( ~ p(V52) | ~ p(V54) | p(V97) ) & ( ~ p(V714) | p(V14) | ~ p(V222) ) & ( ~ p(V641) | p(V202) | ~ p(V201) ) & ~ p(V6) & ( p(V779) | p(V224) ) & ( p(V563) | p(V175) ) & ( ~ p(V124) | ~ p(V272) ) & ( p(V121) | p(V111) ) & ( ~ p(V157) | p(V525) ) & ( p(V349) | ~ p(V290) ) & ( p(V619) | p(V151) ) & ( p(V233) | p(V797) ) & ( p(V133) | p(V305) ) & ( ~ p(V139) | p(V566) ) & ( ~ p(V122) | ~ p(V123) | ~ p(V124) | ~ p(V316) ) & ( ~ p(V70) | p(V28) ) & ( p(V175) | p(V561) ) & ( p(V160) | ~ p(V531) | p(V8) ) & ( p(V166) | ~ p(V225) | p(V3) | p(V2) | p(V4) | ~ p(V729) ) & ( p(V369) | p(V811) ) & ( p(V722) | p(V2) ) & ( ~ p(V175) | p(V707) ) & ( p(V829) | ~ p(V209) ) & ( p(V688) | p(V214) ) & ( p(V4) | ~ p(V89) ) & ( ~ p(V580) | p(V12) | p(V184) ) & ( p(V5) | p(V758) ) & ( ~ p(V39) | p(V110) ) & ( p(V3) | p(V72) ) & ( p(V822) | p(V372) ) & ( p(V630) | ~ p(V1) ) & ( p(V820) | ~ p(V249) ) & ( ~ p(V300) | ~ p(V301) ) & ( p(V642) | ~ p(V201) ) & ( p(V2) | p(V614) ) & ( ~ p(V310) | ~ p(V367) ) & ( p(V150) | p(V631) ) & ( ~ p(V14) | p(V517) ) & ( ~ p(V4) | ~ p(V46) ) & ( ~ p(V312) | p(V123) ) & ( ~ p(V153) | p(V585) ) & ( ~ p(V10) | p(V558) ) & ( ~ p(V135) | ~ p(V279) ) & ( p(V101) | ~ p(V28) ) & ( p(V25) | p(V99) | p(V100) | p(V136) ) & ( p(V559) | p(V10) ) & ( ~ p(V117) | ~ p(V101) | ~ p(V24) | ~ p(V102) ) & ( p(V200) | p(V638) ) & ( p(V103) | p(V119) ) & ( ~ p(V185) | ~ p(V249) | ~ p(V818) ) & ( p(V693) | ~ p(V228) ) & ( p(V805) | ~ p(V367) ) & ( p(V4) | p(V27) ) & ( ~ p(V82) | p(V80) ) & ( p(V80) | p(V78) ) & ( p(V788) | ~ p(V169) ) & ( p(V283) | p(V291) | ~ p(V354) ) & ( ~ p(V2) | ~ p(V1) | p(V190) | ~ p(V601) | ~ p(V3) ) & ( p(V10) | ~ p(V83) ) & ( ~ p(V529) | p(V159) | p(V7) ) & ~ p(V3) & ( p(V537) | ~ p(V7) ) & ( p(V284) | p(V123) ) & ( p(V764) | ~ p(V236) ) & ( p(V637) | p(V5) ) & ( p(V796) | ~ p(V169) ) & ( ~ p(V147) | p(V810) ) & ( ~ p(V310) | p(V122) ) & ( ~ p(V270) | p(V345) ) & ( ~ p(V233) | p(V755) ) & ( p(V195) | p(V814) ) & ( p(V46) | ~ p(V91) ) & ( p(V2) | ~ p(V203) | ~ p(V649) ) & ( ~ p(V3) | p(V681) ) & ( ~ p(V368) | ~ p(V313) ) & ( p(V227) | ~ p(V733) | ~ p(V168) ) & ( ~ p(V834) | ~ p(V212) | ~ p(V375) ) & ( p(V792) | p(V232) ) & ( p(V843) | p(V218) ) & ( p(V633) | p(V199) ) & ( p(V216) | p(V697) ) & ( ~ p(V275) | ~ p(V136) ) & ( p(V350) | ~ p(V124) ) & ( ~ p(V231) | ~ p(V242) | ~ p(V232) | ~ p(V792) ) & ( ~ p(V304) | ~ p(V260) ) & ( ~ p(V288) | p(V353) ) & ( p(V155) | p(V4) | ~ p(V521) ) & ( p(V536) | p(V162) ) & ( p(V587) | ~ p(V186) ) & ( ~ p(V56) | ~ p(V58) | p(V99) ) & ( p(V178) | ~ p(V568) | p(V179) ) & ( ~ p(V197) | ~ p(V370) | ~ p(V815) ) & ( p(V236) | ~ p(V766) | ~ p(V166) ) & ( p(V69) | p(V70) | p(V25) | p(V124) | p(V68) ) & ( p(V738) | p(V4) ) & ( p(V5) | ~ p(V212) | ~ p(V680) ) & ( p(V14) | p(V573) ) & ( p(V147) | p(V367) | ~ p(V805) | p(V189) | p(V188) | p(V187) ) & ( ~ p(V371) | ~ p(V308) ) & ( p(V515) | ~ p(V5) ) & ( p(V146) | p(V147) | ~ p(V503) ) & ( p(V216) | ~ p(V215) | ~ p(V691) ) & ( p(V9) | p(V557) ) & ( p(V278) | p(V324) ) & ( ~ p(V744) | p(V230) | ~ p(V11) ) & ( p(V166) | ~ p(V676) | ~ p(V211) ) & ( p(V222) | ~ p(V14) | ~ p(V715) | ~ p(V179) ) & ( p(V162) | p(V736) ) & ( ~ p(V270) | p(V313) | ~ p(V272) ) & ( p(V803) | p(V189) ) & ( p(V187) | p(V589) ) & ( ~ p(V210) | p(V4) | ~ p(V674) ) & ( ~ p(V164) | ~ p(V772) | p(V238) ) & ( ~ p(V26) | ~ p(V1) ) ) ).
