variable
public a : array 1411 of boolean ;
rule
(
( not a[1] or not a[0] )
and ( not a[413] )
and ( not a[414] )
and ( not a[415] )
and ( not a[3] )
and ( not a[416] )
and ( not a[417] )
and ( not a[418] )
and ( not a[419] )
and ( not a[420] )
and ( not a[421] )
and ( not a[422] )
and ( not a[423] )
and ( not a[424] )
and ( not a[425] )
and ( not a[426] )
and ( not a[427] )
and ( not a[428] )
and ( not a[4] )
and ( not a[429] )
and ( not a[430] )
and ( not a[431] )
and ( not a[432] )
and ( not a[433] )
and ( not a[5] )
and ( not a[434] )
and ( not a[6] )
and ( not a[435] )
and ( not a[436] )
and ( not a[437] )
and ( not a[438] )
and ( not a[7] )
and ( not a[439] )
and ( not a[440] )
and ( not a[164] )
and ( not a[441] )
and ( not a[442] )
and ( not a[443] )
and ( not a[444] )
and ( not a[165] )
and ( not a[445] )
and ( not a[446] )
and ( not a[166] )
and ( not a[447] )
and ( not a[448] )
and ( not a[167] )
and ( not a[449] )
and ( not a[450] )
and ( not a[168] )
and ( not a[451] )
and ( not a[169] )
and ( not a[452] )
and ( not a[170] )
and ( not a[453] )
and ( not a[454] )
and ( not a[455] )
and ( not a[456] )
and ( not a[457] )
and ( not a[458] )
and ( not a[459] )
and ( not a[460] )
and ( not a[461] )
and ( not a[462] )
and ( not a[8] )
and ( not a[463] )
and ( not a[53] )
and ( not a[464] )
and ( not a[56] )
and ( not a[465] )
and ( not a[466] )
and ( not a[467] )
and ( not a[468] )
and ( not a[171] )
and ( not a[469] )
and ( not a[470] )
and ( not a[294] )
and ( not a[9] )
and ( not a[471] )
and ( not a[10] )
and ( not a[472] )
and ( not a[473] )
and ( not a[11] )
and ( not a[474] )
and ( not a[12] )
and ( not a[475] )
and ( not a[172] )
and ( not a[476] )
and ( not a[13] )
and ( not a[14] )
and ( not a[15] )
and ( not a[173] )
and ( not a[477] )
and ( not a[478] )
and ( not a[479] )
and ( not a[87] )
and ( not a[480] )
and ( not a[88] )
and ( not a[74] )
and ( not a[75] )
and ( not a[481] )
and ( not a[482] )
and ( not a[483] )
and ( not a[484] )
and ( not a[485] )
and ( not a[486] )
and ( not a[487] )
and ( not a[488] )
and ( not a[41] )
and ( not a[489] )
and ( not a[490] )
and ( not a[491] )
and ( not a[492] )
and ( not a[493] )
and ( not a[494] )
and ( not a[495] )
and ( not a[496] )
and ( not a[497] )
and ( not a[89] )
and ( not a[498] )
and ( not a[499] )
and ( not a[174] )
and ( not a[500] )
and ( not a[175] )
and ( not a[501] )
and ( not a[502] )
and ( not a[503] )
and ( not a[504] )
and ( not a[505] )
and ( not a[506] )
and ( not a[64] )
and ( not a[507] )
and ( not a[508] )
and ( not a[509] )
and ( not a[510] )
and ( not a[511] )
and ( not a[512] )
and ( not a[513] )
and ( not a[514] )
and ( not a[515] )
and ( not a[176] )
and ( not a[315] )
and ( not a[516] )
and ( not a[517] )
and ( not a[295] )
and ( not a[90] )
and ( not a[177] )
and ( not a[518] )
and ( not a[519] )
and ( not a[178] )
and ( not a[179] )
and ( not a[180] )
and ( not a[181] )
and ( not a[520] )
and ( not a[91] )
and ( not a[92] )
and ( not a[521] )
and ( not a[182] )
and ( not a[93] )
and ( not a[183] )
and ( not a[522] )
and ( not a[184] )
and ( not a[523] )
and ( not a[524] )
and ( not a[525] )
and ( not a[185] )
and ( not a[186] )
and ( not a[526] )
and ( not a[187] )
and ( not a[94] )
and ( not a[76] )
and ( not a[77] )
and ( not a[78] )
and ( not a[527] )
and ( not a[95] )
and ( not a[96] )
and ( not a[528] )
and ( not a[529] )
and ( not a[530] )
and ( not a[531] )
and ( not a[532] )
and ( not a[16] )
and ( not a[533] )
and ( not a[534] )
and ( not a[535] )
and ( not a[536] )
and ( not a[537] )
and ( not a[538] )
and ( not a[539] )
and ( not a[17] )
and ( not a[540] )
and ( not a[541] )
and ( not a[542] )
and ( not a[543] )
and ( not a[544] )
and ( not a[545] )
and ( not a[546] )
and ( not a[547] )
and ( not a[548] )
and ( not a[108] )
and ( not a[549] )
and ( not a[111] )
and ( not a[112] )
and ( not a[363] )
and ( not a[114] )
and ( not a[115] )
and ( not a[550] )
and ( not a[551] )
and ( not a[18] )
and ( not a[188] )
and ( not a[552] )
and ( not a[553] )
and ( not a[296] )
and ( not a[297] )
and ( not a[19] )
and ( not a[554] )
and ( not a[555] )
and ( not a[104] )
and ( not a[556] )
and ( not a[557] )
and ( not a[558] )
and ( not a[559] )
and ( not a[560] )
and ( not a[189] )
and ( not a[561] )
and ( not a[562] )
and ( not a[563] )
and ( not a[190] )
and ( not a[20] )
and ( not a[564] )
and ( not a[565] )
and ( not a[566] )
and ( not a[567] )
and ( not a[21] )
and ( not a[568] )
and ( not a[569] )
and ( not a[570] )
and ( not a[571] )
and ( not a[572] )
and ( not a[22] )
and ( not a[573] )
and ( not a[574] )
and ( not a[23] )
and ( not a[575] )
and ( not a[576] )
and ( not a[577] )
and ( not a[578] )
and ( not a[579] )
and ( not a[580] )
and ( not a[581] )
and ( not a[582] )
and ( not a[583] )
and ( not a[584] )
and ( not a[79] )
and ( not a[585] )
and ( not a[586] )
and ( not a[587] )
and ( not a[588] )
and ( not a[589] )
and ( not a[590] )
and ( not a[591] )
and ( not a[592] )
and ( not a[593] )
and ( not a[594] )
and ( not a[595] )
and ( not a[596] )
and ( not a[597] )
and ( not a[598] )
and ( not a[599] )
and ( not a[600] )
and ( not a[601] )
and ( not a[602] )
and ( not a[192] )
and ( not a[603] )
and ( not a[193] )
and ( not a[194] )
and ( not a[604] )
and ( not a[605] )
and ( not a[606] )
and ( not a[607] )
and ( not a[608] )
and ( not a[54] )
and ( not a[57] )
and ( not a[316] )
and ( not a[24] )
and ( not a[25] )
and ( not a[609] )
and ( not a[26] )
and ( not a[319] )
and ( not a[610] )
and ( not a[27] )
and ( not a[28] )
and ( not a[322] )
and ( not a[611] )
and ( not a[195] )
and ( not a[323] )
and ( not a[612] )
and ( not a[324] )
and ( not a[325] )
and ( not a[29] )
and ( not a[613] )
and ( not a[196] )
and ( not a[197] )
and ( not a[331] )
and ( not a[614] )
and ( not a[198] )
and ( not a[615] )
and ( not a[47] )
and ( not a[616] )
and ( not a[199] )
and ( not a[299] )
and ( not a[300] )
and ( not a[120] )
and ( not a[30] )
and ( not a[617] )
and ( not a[121] )
and ( not a[122] )
and ( not a[123] )
and ( not a[200] )
and ( not a[124] )
and ( not a[618] )
and ( not a[619] )
and ( not a[620] )
and ( not a[621] )
and ( not a[125] )
and ( not a[126] )
and ( not a[622] )
and ( not a[127] )
and ( not a[128] )
and ( not a[129] )
and ( not a[130] )
and ( not a[131] )
and ( not a[132] )
and ( not a[623] )
and ( not a[133] )
and ( not a[134] )
and ( not a[624] )
and ( not a[135] )
and ( not a[136] )
and ( not a[137] )
and ( not a[625] )
and ( not a[626] )
and ( not a[201] )
and ( not a[627] )
and ( not a[301] )
and ( not a[628] )
and ( not a[629] )
and ( not a[317] )
and ( not a[31] )
and ( not a[630] )
and ( not a[631] )
and ( not a[632] )
and ( not a[138] )
and ( not a[139] )
and ( not a[633] )
and ( not a[634] )
and ( not a[635] )
and ( not a[202] )
and ( not a[636] )
and ( not a[637] )
and ( not a[638] )
and ( not a[639] )
and ( not a[640] )
and ( not a[204] )
and ( not a[641] )
and ( not a[642] )
and ( not a[643] )
and ( not a[326] )
and ( not a[644] )
and ( not a[327] )
and ( not a[205] )
and ( not a[645] )
and ( not a[328] )
and ( not a[329] )
and ( not a[646] )
and ( not a[32] )
and ( not a[647] )
and ( not a[206] )
and ( not a[648] )
and ( not a[207] )
and ( not a[208] )
and ( not a[649] )
and ( not a[209] )
and ( not a[210] )
and ( not a[650] )
and ( not a[651] )
and ( not a[652] )
and ( not a[653] )
and ( not a[654] )
and ( not a[211] )
and ( not a[212] )
and ( not a[655] )
and ( not a[656] )
and ( not a[657] )
and ( not a[213] )
and ( not a[658] )
and ( not a[659] )
and ( not a[660] )
and ( not a[661] )
and ( not a[662] )
and ( not a[663] )
and ( not a[33] )
and ( not a[664] )
and ( not a[665] )
and ( not a[666] )
and ( not a[667] )
and ( not a[668] )
and ( not a[80] )
and ( not a[669] )
and ( not a[81] )
and ( not a[82] )
and ( not a[83] )
and ( not a[214] )
and ( not a[84] )
and ( not a[670] )
and ( not a[85] )
and ( not a[86] )
and ( not a[140] )
and ( not a[671] )
and ( not a[302] )
and ( not a[672] )
and ( not a[673] )
and ( not a[303] )
and ( not a[674] )
and ( not a[34] )
and ( not a[312] )
and ( not a[675] )
and ( not a[215] )
and ( not a[676] )
and ( not a[141] )
and ( not a[677] )
and ( not a[142] )
and ( not a[678] )
and ( not a[143] )
and ( not a[144] )
and ( not a[679] )
and ( not a[145] )
and ( not a[680] )
and ( not a[146] )
and ( not a[147] )
and ( not a[148] )
and ( not a[149] )
and ( not a[150] )
and ( not a[681] )
and ( not a[151] )
and ( not a[682] )
and ( not a[152] )
and ( not a[683] )
and ( not a[684] )
and ( not a[685] )
and ( not a[686] )
and ( not a[687] )
and ( not a[688] )
and ( not a[689] )
and ( not a[690] )
and ( not a[691] )
and ( not a[692] )
and ( not a[693] )
and ( not a[694] )
and ( not a[695] )
and ( not a[696] )
and ( not a[697] )
and ( not a[698] )
and ( not a[699] )
and ( not a[700] )
and ( not a[701] )
and ( not a[702] )
and ( not a[216] )
and ( not a[217] )
and ( not a[218] )
and ( not a[219] )
and ( not a[71] )
and ( not a[220] )
and ( not a[221] )
and ( not a[222] )
and ( not a[223] )
and ( not a[224] )
and ( not a[225] )
and ( not a[226] )
and ( not a[227] )
and ( not a[228] )
and ( not a[229] )
and ( not a[230] )
and ( not a[703] )
and ( not a[704] )
and ( not a[705] )
and ( not a[706] )
and ( not a[231] )
and ( not a[232] )
and ( not a[233] )
and ( not a[234] )
and ( not a[707] )
and ( not a[708] )
and ( not a[709] )
and ( not a[710] )
and ( not a[711] )
and ( not a[59] )
and ( not a[318] )
and ( not a[712] )
and ( not a[713] )
and ( not a[714] )
and ( not a[235] )
and ( not a[715] )
and ( not a[716] )
and ( not a[717] )
and ( not a[35] )
and ( not a[48] )
and ( not a[718] )
and ( not a[719] )
and ( not a[720] )
and ( not a[61] )
and ( not a[721] )
and ( not a[340] )
and ( not a[722] )
and ( not a[723] )
and ( not a[724] )
and ( not a[116] )
and ( not a[725] )
and ( not a[726] )
and ( not a[727] )
and ( not a[728] )
and ( not a[236] )
and ( not a[729] )
and ( not a[730] )
and ( not a[237] )
and ( not a[731] )
and ( not a[97] )
and ( not a[238] )
and ( not a[239] )
and ( not a[304] )
and ( not a[240] )
and ( not a[241] )
and ( not a[242] )
and ( not a[732] )
and ( not a[733] )
and ( not a[243] )
and ( not a[244] )
and ( not a[734] )
and ( not a[735] )
and ( not a[1] )
and ( not a[2] )
and ( not a[62] )
and ( not a[63] )
and ( not a[245] )
and ( not a[246] )
and ( not a[305] )
and ( not a[306] )
and ( not a[736] )
and ( not a[247] )
and ( not a[737] )
and ( not a[248] )
and ( not a[738] )
and ( not a[249] )
and ( not a[250] )
and ( not a[251] )
and ( not a[252] )
and ( not a[253] )
and ( not a[739] )
and ( not a[254] )
and ( not a[255] )
and ( not a[256] )
and ( not a[257] )
and ( not a[740] )
and ( not a[741] )
and ( not a[742] )
and ( not a[258] )
and ( not a[259] )
and ( not a[743] )
and ( not a[744] )
and ( not a[745] )
and ( not a[746] )
and ( not a[747] )
and ( not a[748] )
and ( not a[749] )
and ( not a[750] )
and ( not a[751] )
and ( not a[752] )
and ( not a[753] )
and ( not a[754] )
and ( not a[755] )
and ( not a[756] )
and ( not a[757] )
and ( not a[758] )
and ( not a[759] )
and ( not a[760] )
and ( not a[761] )
and ( not a[762] )
and ( not a[763] )
and ( not a[764] )
and ( not a[765] )
and ( not a[766] )
and ( not a[767] )
and ( not a[768] )
and ( not a[769] )
and ( not a[770] )
and ( not a[771] )
and ( not a[772] )
and ( not a[773] )
and ( not a[774] )
and ( not a[775] )
and ( not a[776] )
and ( not a[777] )
and ( not a[778] )
and ( not a[779] )
and ( not a[780] )
and ( not a[781] )
and ( not a[782] )
and ( not a[783] )
and ( not a[784] )
and ( not a[785] )
and ( not a[786] )
and ( not a[787] )
and ( not a[788] )
and ( not a[789] )
and ( not a[790] )
and ( not a[791] )
and ( not a[792] )
and ( not a[793] )
and ( not a[794] )
and ( not a[795] )
and ( not a[796] )
and ( not a[797] )
and ( not a[798] )
and ( not a[799] )
and ( not a[800] )
and ( not a[801] )
and ( not a[802] )
and ( not a[803] )
and ( not a[804] )
and ( not a[805] )
and ( not a[806] )
and ( not a[807] )
and ( not a[808] )
and ( not a[809] )
and ( not a[810] )
and ( not a[811] )
and ( not a[812] )
and ( not a[813] )
and ( not a[814] )
and ( not a[815] )
and ( not a[816] )
and ( not a[817] )
and ( not a[818] )
and ( not a[819] )
and ( not a[820] )
and ( not a[821] )
and ( not a[822] )
and ( not a[823] )
and ( not a[824] )
and ( not a[825] )
and ( not a[826] )
and ( not a[827] )
and ( not a[828] )
and ( not a[829] )
and ( not a[830] )
and ( not a[831] )
and ( not a[832] )
and ( not a[833] )
and ( not a[834] )
and ( not a[835] )
and ( not a[836] )
and ( not a[837] )
and ( not a[838] )
and ( not a[839] )
and ( not a[840] )
and ( not a[841] )
and ( not a[842] )
and ( not a[843] )
and ( not a[844] )
and ( not a[845] )
and ( not a[846] )
and ( not a[847] )
and ( not a[848] )
and ( not a[849] )
and ( not a[850] )
and ( not a[851] )
and ( not a[852] )
and ( not a[853] )
and ( not a[854] )
and ( not a[855] )
and ( not a[856] )
and ( not a[857] )
and ( not a[858] )
and ( not a[859] )
and ( not a[860] )
and ( not a[861] )
and ( not a[862] )
and ( not a[863] )
and ( not a[864] )
and ( not a[865] )
and ( not a[866] )
and ( not a[867] )
and ( not a[868] )
and ( not a[869] )
and ( not a[870] )
and ( not a[871] )
and ( not a[872] )
and ( not a[873] )
and ( not a[874] )
and ( not a[875] )
and ( not a[876] )
and ( not a[877] )
and ( not a[878] )
and ( not a[879] )
and ( not a[880] )
and ( not a[881] )
and ( not a[882] )
and ( not a[883] )
and ( not a[884] )
and ( not a[885] )
and ( not a[886] )
and ( not a[887] )
and ( not a[888] )
and ( not a[889] )
and ( not a[890] )
and ( not a[891] )
and ( not a[892] )
and ( not a[893] )
and ( not a[894] )
and ( not a[895] )
and ( not a[896] )
and ( not a[897] )
and ( not a[898] )
and ( not a[899] )
and ( not a[900] )
and ( not a[901] )
and ( not a[902] )
and ( not a[903] )
and ( not a[904] )
and ( not a[905] )
and ( not a[906] )
and ( not a[907] )
and ( not a[908] )
and ( not a[909] )
and ( not a[910] )
and ( not a[911] )
and ( not a[346] )
and ( not a[347] )
and ( not a[45] )
and ( not a[912] )
and ( not a[348] )
and ( not a[349] )
and ( not a[350] )
and ( not a[351] )
and ( not a[352] )
and ( not a[353] )
and ( not a[354] )
and ( not a[355] )
and ( not a[356] )
and ( not a[357] )
and ( not a[913] )
and ( not a[358] )
and ( not a[914] )
and ( not a[359] )
and ( not a[915] )
and ( not a[916] )
and ( not a[917] )
and ( not a[918] )
and ( not a[919] )
and ( not a[920] )
and ( not a[921] )
and ( not a[922] )
and ( not a[923] )
and ( not a[924] )
and ( not a[925] )
and ( not a[926] )
and ( not a[927] )
and ( not a[928] )
and ( not a[929] )
and ( not a[930] )
and ( not a[931] )
and ( not a[932] )
and ( not a[933] )
and ( not a[934] )
and ( not a[935] )
and ( not a[936] )
and ( not a[937] )
and ( not a[938] )
and ( not a[939] )
and ( not a[940] )
and ( not a[941] )
and ( not a[942] )
and ( not a[943] )
and ( not a[944] )
and ( not a[945] )
and ( not a[946] )
and ( not a[947] )
and ( not a[948] )
and ( not a[949] )
and ( not a[950] )
and ( not a[951] )
and ( not a[952] )
and ( not a[953] )
and ( not a[954] )
and ( not a[955] )
and ( not a[956] )
and ( not a[957] )
and ( not a[958] )
and ( not a[959] )
and ( not a[960] )
and ( not a[961] )
and ( not a[962] )
and ( not a[963] )
and ( not a[964] )
and ( not a[965] )
and ( not a[966] )
and ( not a[967] )
and ( not a[968] )
and ( not a[969] )
and ( not a[970] )
and ( not a[971] )
and ( not a[972] )
and ( not a[973] )
and ( not a[974] )
and ( not a[975] )
and ( not a[976] )
and ( not a[977] )
and ( not a[978] )
and ( not a[979] )
and ( not a[980] )
and ( not a[981] )
and ( not a[982] )
and ( not a[983] )
and ( not a[984] )
and ( not a[985] )
and ( not a[986] )
and ( not a[987] )
and ( not a[988] )
and ( not a[989] )
and ( not a[990] )
and ( not a[991] )
and ( not a[992] )
and ( not a[993] )
and ( not a[994] )
and ( not a[995] )
and ( not a[996] )
and ( not a[997] )
and ( not a[998] )
and ( not a[999] )
and ( not a[1000] )
and ( not a[1001] )
and ( not a[1002] )
and ( not a[1003] )
and ( not a[1004] )
and ( not a[1005] )
and ( not a[1006] )
and ( not a[1007] )
and ( not a[1008] )
and ( not a[1009] )
and ( not a[1010] )
and ( not a[1011] )
and ( not a[1012] )
and ( not a[1013] )
and ( not a[1014] )
and ( not a[1015] )
and ( not a[1016] )
and ( not a[1017] )
and ( not a[1018] )
and ( not a[1019] )
and ( not a[1020] )
and ( not a[1021] )
and ( not a[1022] )
and ( not a[1023] )
and ( not a[1024] )
and ( not a[1025] )
and ( not a[1026] )
and ( not a[1027] )
and ( not a[1028] )
and ( not a[1029] )
and ( not a[1030] )
and ( not a[1031] )
and ( not a[1032] )
and ( not a[1033] )
and ( not a[1034] )
and ( not a[1035] )
and ( not a[1036] )
and ( not a[1037] )
and ( not a[1038] )
and ( not a[1039] )
and ( not a[1040] )
and ( not a[1041] )
and ( not a[1042] )
and ( not a[1043] )
and ( not a[1044] )
and ( not a[1045] )
and ( not a[1046] )
and ( not a[1047] )
and ( not a[1048] )
and ( not a[1049] )
and ( not a[1050] )
and ( not a[1051] )
and ( not a[1052] )
and ( not a[1053] )
and ( not a[1054] )
and ( not a[391] )
and ( not a[392] )
and ( not a[393] )
and ( not a[394] )
and ( not a[395] )
and ( not a[396] )
and ( not a[1055] )
and ( not a[1056] )
and ( not a[397] )
and ( not a[367] )
and ( not a[368] )
and ( not a[369] )
and ( not a[370] )
and ( not a[371] )
and ( not a[372] )
and ( not a[373] )
and ( not a[374] )
and ( not a[375] )
and ( not a[376] )
and ( not a[377] )
and ( not a[407] )
and ( not a[378] )
and ( not a[379] )
and ( not a[380] )
and ( not a[381] )
and ( not a[1057] )
and ( not a[382] )
and ( not a[1058] )
and ( not a[1059] )
and ( not a[1060] )
and ( not a[383] )
and ( not a[384] )
and ( not a[1061] )
and ( not a[385] )
and ( not a[1062] )
and ( not a[386] )
and ( not a[387] )
and ( not a[388] )
and ( not a[398] )
and ( not a[399] )
and ( not a[1063] )
and ( not a[400] )
and ( not a[401] )
and ( not a[402] )
and ( not a[403] )
and ( not a[404] )
and ( not a[405] )
and ( not a[1064] )
and ( not a[1065] )
and ( not a[1066] )
and ( not a[406] )
and ( not a[1067] )
and ( not a[1068] )
and ( not a[1069] )
and ( not a[1070] )
and ( not a[1071] )
and ( not a[1072] )
and ( not a[1073] )
and ( not a[389] )
and ( not a[390] )
and ( not a[1074] )
and ( not a[1075] )
and ( not a[1076] )
and ( not a[1077] )
and ( not a[1078] )
and ( not a[1079] )
and ( not a[1080] )
and ( not a[1081] )
and ( not a[1082] )
and ( not a[1083] )
and ( not a[1084] )
and ( not a[1085] )
and ( not a[1086] )
and ( not a[1087] )
and ( not a[1088] )
and ( not a[1089] )
and ( not a[1090] )
and ( not a[1091] )
and ( not a[1092] )
and ( not a[1093] )
and ( not a[1094] )
and ( not a[1095] )
and ( not a[1096] )
and ( not a[1097] )
and ( not a[1098] )
and ( not a[1099] )
and ( not a[1100] )
and ( not a[1101] )
and ( not a[1102] )
and ( not a[1103] )
and ( not a[1104] )
and ( not a[1105] )
and ( not a[1106] )
and ( not a[1107] )
and ( not a[1108] )
and ( not a[1109] )
and ( not a[1110] )
and ( not a[1111] )
and ( not a[1112] )
and ( not a[1113] )
and ( not a[1114] )
and ( not a[1115] )
and ( not a[1116] )
and ( not a[1117] )
and ( not a[1118] )
and ( not a[1119] )
and ( not a[1120] )
and ( not a[1121] )
and ( not a[1122] )
and ( not a[1123] )
and ( not a[1124] )
and ( not a[1125] )
and ( not a[1126] )
and ( not a[1127] )
and ( not a[1128] )
and ( not a[1129] )
and ( not a[1130] )
and ( not a[1131] )
and ( not a[1132] )
and ( not a[1133] )
and ( not a[1134] )
and ( not a[1135] )
and ( not a[1136] )
and ( not a[1137] )
and ( not a[1138] )
and ( not a[1139] )
and ( not a[1140] )
and ( not a[1141] )
and ( not a[1142] )
and ( not a[1143] )
and ( not a[1144] )
and ( not a[1145] )
and ( not a[1146] )
and ( not a[1147] )
and ( not a[1148] )
and ( not a[1149] )
and ( not a[1150] )
and ( not a[1151] )
and ( not a[1152] )
and ( not a[1153] )
and ( not a[1154] )
and ( not a[1155] )
and ( not a[1156] )
and ( not a[1157] )
and ( not a[1158] )
and ( not a[1159] )
and ( not a[1160] )
and ( not a[1161] )
and ( not a[1162] )
and ( not a[1163] )
and ( not a[1164] )
and ( not a[1165] )
and ( not a[1166] )
and ( not a[1167] )
and ( not a[1168] )
and ( not a[1169] )
and ( not a[1170] )
and ( not a[1171] )
and ( not a[1172] )
and ( not a[1173] )
and ( not a[1174] )
and ( not a[1175] )
and ( not a[1176] )
and ( not a[1177] )
and ( not a[1178] )
and ( not a[1179] )
and ( not a[1180] )
and ( not a[1181] )
and ( not a[1182] )
and ( not a[1183] )
and ( not a[1184] )
and ( not a[1185] )
and ( not a[1186] )
and ( not a[1187] )
and ( not a[1188] )
and ( not a[1189] )
and ( not a[1190] )
and ( not a[1191] )
and ( not a[1192] )
and ( not a[1193] )
and ( not a[1194] )
and ( not a[1195] )
and ( not a[1196] )
and ( not a[1197] )
and ( not a[1198] )
and ( not a[1199] )
and ( not a[1200] )
and ( not a[1201] )
and ( not a[1202] )
and ( not a[1203] )
and ( not a[1204] )
and ( not a[1205] )
and ( not a[1206] )
and ( not a[1207] )
and ( not a[1208] )
and ( not a[1209] )
and ( not a[1210] )
and ( not a[1211] )
and ( not a[1212] )
and ( not a[1213] )
and ( not a[1214] )
and ( not a[1215] )
and ( not a[1216] )
and ( not a[1217] )
and ( not a[1218] )
and ( not a[1219] )
and ( not a[1220] )
and ( not a[1221] )
and ( not a[1222] )
and ( not a[1223] )
and ( not a[1224] )
and ( not a[1225] )
and ( not a[1226] )
and ( not a[1227] )
and ( not a[1228] )
and ( not a[1229] )
and ( not a[1230] )
and ( not a[1231] )
and ( not a[1232] )
and ( not a[1233] )
and ( not a[1234] )
and ( not a[1235] )
and ( not a[1236] )
and ( not a[1237] )
and ( not a[1238] )
and ( not a[1239] )
and ( not a[1240] )
and ( not a[1241] )
and ( not a[1242] )
and ( not a[1243] )
and ( not a[1244] )
and ( not a[1245] )
and ( not a[1246] )
and ( not a[1247] )
and ( not a[1248] )
and ( not a[1249] )
and ( not a[1250] )
and ( not a[1251] )
and ( not a[1252] )
and ( not a[1253] )
and ( not a[1254] )
and ( not a[1255] )
and ( not a[1256] )
and ( not a[1257] )
and ( not a[1258] )
and ( not a[1259] )
and ( not a[1260] )
and ( not a[1261] )
and ( not a[1262] )
and ( not a[1263] )
and ( not a[1264] )
and ( not a[1265] )
and ( not a[1266] )
and ( not a[1267] )
and ( not a[1268] )
and ( not a[1269] )
and ( not a[1270] )
and ( not a[1271] )
and ( not a[1272] )
and ( not a[1273] )
and ( not a[1274] )
and ( not a[1275] )
and ( not a[1276] )
and ( not a[1277] )
and ( not a[1278] )
and ( not a[1279] )
and ( not a[1280] )
and ( not a[1281] )
and ( not a[1282] )
and ( not a[1283] )
and ( not a[1284] )
and ( not a[1285] )
and ( not a[1286] )
and ( not a[1287] )
and ( not a[1288] )
and ( not a[1289] )
and ( not a[1290] )
and ( not a[1291] )
and ( not a[1292] )
and ( not a[1293] )
and ( not a[1294] )
and ( not a[153] )
and ( not a[154] )
and ( not a[155] )
and ( not a[156] )
and ( not a[157] )
and ( not a[158] )
and ( not a[288] )
and ( not a[159] )
and ( not a[289] )
and ( not a[1295] )
and ( not a[1296] )
and ( not a[1297] )
and ( not a[1298] )
and ( not a[1299] )
and ( not a[1300] )
and ( not a[1301] )
and ( not a[1302] )
and ( not a[1303] )
and ( not a[290] )
and ( not a[160] )
and ( not a[161] )
and ( not a[162] )
and ( not a[1304] )
and ( not a[1305] )
and ( not a[1306] )
and ( not a[1307] )
and ( not a[1308] )
and ( not a[1309] )
and ( not a[1310] )
and ( not a[1311] )
and ( not a[1312] )
and ( not a[1313] )
and ( not a[1314] )
and ( not a[1315] )
and ( not a[1316] )
and ( not a[1317] )
and ( not a[1318] )
and ( not a[1319] )
and ( not a[1320] )
and ( not a[1321] )
and ( not a[1322] )
and ( not a[1323] )
and ( not a[1324] )
and ( not a[1325] )
and ( not a[260] )
and ( not a[261] )
and ( not a[262] )
and ( not a[263] )
and ( not a[264] )
and ( not a[265] )
and ( not a[266] )
and ( not a[267] )
and ( not a[1326] )
and ( not a[1327] )
and ( not a[1328] )
and ( not a[268] )
and ( not a[269] )
and ( not a[270] )
and ( not a[271] )
and ( not a[272] )
and ( not a[1329] )
and ( not a[273] )
and ( not a[274] )
and ( not a[275] )
and ( not a[307] )
and ( not a[1330] )
and ( not a[1331] )
and ( not a[1332] )
and ( not a[1333] )
and ( not a[1334] )
and ( not a[1335] )
and ( not a[1336] )
and ( not a[1337] )
and ( not a[1338] )
and ( not a[1339] )
and ( not a[1340] )
and ( not a[276] )
and ( not a[277] )
and ( not a[308] )
and ( not a[278] )
and ( not a[279] )
and ( not a[309] )
and ( not a[280] )
and ( not a[281] )
and ( not a[310] )
and ( not a[282] )
and ( not a[283] )
and ( not a[311] )
and ( not a[284] )
and ( not a[285] )
and ( not a[1341] )
and ( not a[1342] )
and ( not a[1343] )
and ( not a[1344] )
and ( not a[1345] )
and ( not a[1346] )
and ( not a[1347] )
and ( not a[1348] )
and ( not a[1349] )
and ( not a[1350] )
and ( not a[1351] )
and ( not a[1352] )
and ( not a[1353] )
and ( not a[1354] )
and ( not a[1355] )
and ( not a[1356] )
and ( not a[1357] )
and ( not a[1358] )
and ( not a[1359] )
and ( not a[1360] )
and ( not a[1361] )
and ( not a[1362] )
and ( not a[1363] )
and ( not a[163] )
and ( not a[65] )
and ( not a[66] )
and ( not a[67] )
and ( not a[291] )
and ( not a[292] )
and ( not a[293] )
and ( not a[1364] )
and ( not a[1365] )
and ( not a[1366] )
and ( not a[1367] )
and ( not a[1368] )
and ( not a[1369] )
and ( not a[1370] )
and ( not a[1371] )
and ( not a[1372] )
and ( not a[1373] )
and ( not a[1374] )
and ( not a[1375] )
and ( not a[1376] )
and ( not a[1377] )
and ( not a[1378] )
and ( not a[1379] )
and ( not a[1380] )
and ( not a[1381] )
and ( not a[1382] )
and ( not a[1383] )
and ( not a[1384] )
and ( not a[1385] )
and ( not a[1386] )
and ( not a[1387] )
and ( not a[1388] )
and ( not a[1389] )
and ( not a[1390] )
and ( not a[1391] )
and ( not a[1392] )
and ( not a[1393] )
and ( not a[1394] )
and ( not a[1395] )
and ( not a[1396] )
and ( not a[1397] )
and ( not a[1398] )
and ( not a[1399] )
and ( not a[1400] )
and ( not a[1401] )
and ( not a[1402] )
and ( not a[1403] )
and ( not a[1404] )
and ( not a[1405] )
and ( not a[1406] )
and ( not a[1407] )
and ( not a[1408] )
and ( not a[1409] )
and ( not a[1410] )
and ( a[366] )
and ( a[364] )
and ( a[411] )
and ( a[412] )
and ( a[365] )
and ( not a[2] or not a[0] )
and ( not a[3] or not a[0] )
and ( not a[4] or not a[0] )
and ( not a[5] or not a[0] )
and ( not a[6] or not a[0] )
and ( not a[7] or not a[0] )
and ( not a[8] or not a[0] )
and ( not a[9] or not a[0] )
and ( not a[10] or not a[0] )
and ( not a[11] or not a[0] )
and ( not a[12] or not a[0] )
and ( not a[13] or not a[0] )
and ( not a[14] or not a[0] )
and ( not a[15] or not a[0] )
and ( not a[16] or not a[0] )
and ( not a[17] or not a[0] )
and ( not a[18] or not a[0] )
and ( not a[19] or not a[0] )
and ( not a[20] or not a[0] )
and ( not a[21] or not a[0] )
and ( not a[22] or not a[0] )
and ( not a[23] or not a[0] )
and ( not a[24] or not a[0] )
and ( not a[25] or not a[0] )
and ( not a[26] or not a[0] )
and ( not a[27] or not a[0] )
and ( not a[28] or not a[0] )
and ( not a[29] or not a[0] )
and ( not a[30] or not a[0] )
and ( not a[31] or not a[0] )
and ( not a[32] or not a[0] )
and ( not a[33] or not a[0] )
and ( not a[34] or not a[0] )
and ( not a[35] or not a[0] )
and ( not a[36] or a[0] )
and ( not a[37] or a[0] )
and ( not a[38] or a[0] )
and ( not a[39] or a[0] )
and ( not a[41] or not a[40] )
and ( not a[42] or a[43] )
and ( not a[44] or not a[42] or a[45] )
and ( not a[46] or not a[42] )
and ( not a[47] or not a[42] )
and ( not a[48] or not a[42] )
and ( not a[50] or not a[49] )
and ( not a[51] or not a[49] or a[52] )
and ( not a[49] or a[51] )
and ( not a[53] or not a[49] )
and ( not a[54] or not a[49] )
and ( not a[55] or not a[50] or a[52] )
and ( not a[55] or not a[51] )
and ( not a[55] or a[50] )
and ( not a[56] or not a[55] )
and ( not a[57] or not a[55] )
and ( not a[59] or not a[58] )
and ( not a[61] or not a[60] )
and ( not a[62] or not a[60] )
and ( not a[63] or not a[60] )
and ( not a[64] or not a[60] )
and ( not a[65] or not a[60] )
and ( not a[66] or not a[60] )
and ( not a[67] or not a[60] )
and ( not a[71] or not a[70] )
and ( not a[72] or a[70] )
and ( not a[73] or not a[72] )
and ( not a[74] or not a[72] )
and ( not a[75] or not a[72] )
and ( not a[76] or not a[72] )
and ( not a[77] or not a[72] )
and ( not a[78] or not a[72] )
and ( not a[79] or not a[72] )
and ( not a[80] or not a[72] )
and ( not a[81] or not a[72] )
and ( not a[82] or not a[72] )
and ( not a[83] or not a[72] )
and ( not a[84] or not a[72] )
and ( not a[85] or not a[72] )
and ( not a[86] or not a[72] )
and ( not a[73] or not a[72] )
and ( not a[87] or not a[73] )
and ( not a[88] or not a[73] )
and ( not a[89] or not a[73] )
and ( not a[90] or not a[73] )
and ( not a[91] or not a[73] )
and ( not a[92] or not a[73] )
and ( not a[93] or not a[73] )
and ( not a[94] or not a[73] )
and ( not a[76] or not a[73] )
and ( not a[77] or not a[73] )
and ( not a[95] or not a[73] )
and ( not a[96] or not a[73] )
and ( not a[73] or not a[44] )
and ( not a[73] or not a[46] )
and ( not a[97] or not a[73] )
and ( not a[98] or a[7] )
and ( not a[98] or a[43] )
and ( not a[99] or not a[98] )
and ( not a[100] or not a[78] )
and ( not a[101] or not a[100] )
and ( not a[102] or not a[100] )
and ( not a[103] or not a[100] )
and ( not a[104] or not a[100] )
and ( not a[101] or not a[78] )
and ( not a[101] or not a[100] )
and ( not a[102] or not a[101] )
and ( not a[103] or not a[101] )
and ( not a[104] or not a[101] )
and ( not a[102] or not a[78] )
and ( not a[102] or not a[100] )
and ( not a[102] or not a[101] )
and ( not a[103] or not a[102] )
and ( not a[104] or not a[102] )
and ( not a[103] or not a[78] )
and ( not a[103] or not a[100] )
and ( not a[103] or not a[101] )
and ( not a[103] or not a[102] )
and ( not a[104] or not a[103] )
and ( not a[108] or not a[107] )
and ( not a[111] or not a[110] )
and ( not a[112] or not a[110] )
and ( not a[113] or not a[110] )
and ( not a[114] or not a[110] )
and ( not a[115] or not a[110] )
and ( not a[116] or not a[110] )
and ( not a[113] or not a[112] )
and ( not a[113] or not a[110] )
and ( not a[114] or not a[113] )
and ( not a[115] or not a[113] )
and ( not a[120] or not a[119] )
and ( not a[121] or not a[119] )
and ( not a[122] or not a[119] )
and ( not a[123] or not a[119] )
and ( not a[124] or not a[119] )
and ( not a[125] or not a[119] )
and ( not a[126] or not a[119] )
and ( not a[127] or not a[119] )
and ( not a[128] or not a[119] )
and ( not a[129] or not a[119] )
and ( not a[130] or not a[119] )
and ( not a[131] or not a[119] )
and ( not a[132] or not a[119] )
and ( not a[133] or not a[119] )
and ( not a[134] or not a[119] )
and ( not a[135] or not a[119] )
and ( not a[136] or not a[119] )
and ( not a[137] or not a[119] )
and ( not a[138] or not a[119] )
and ( not a[139] or not a[119] )
and ( not a[140] or not a[119] )
and ( not a[141] or not a[119] )
and ( not a[142] or not a[119] )
and ( not a[143] or not a[119] )
and ( not a[144] or not a[119] )
and ( not a[145] or not a[119] )
and ( not a[146] or not a[119] )
and ( not a[147] or not a[119] )
and ( not a[148] or not a[119] )
and ( not a[149] or not a[119] )
and ( not a[150] or not a[119] )
and ( not a[151] or not a[119] )
and ( not a[152] or not a[119] )
and ( not a[119] or not a[62] )
and ( not a[285] or not a[44] )
and ( not a[284] or not a[44] )
and ( not a[283] or not a[44] )
and ( not a[282] or not a[44] )
and ( not a[281] or not a[44] )
and ( not a[280] or not a[44] )
and ( not a[279] or not a[44] )
and ( not a[278] or not a[44] )
and ( not a[277] or not a[44] )
and ( not a[276] or not a[44] )
and ( not a[275] or not a[44] )
and ( not a[274] or not a[44] )
and ( not a[273] or not a[44] )
and ( not a[272] or not a[44] )
and ( not a[271] or not a[44] )
and ( not a[270] or not a[44] )
and ( not a[269] or not a[44] )
and ( not a[268] or not a[44] )
and ( not a[267] or not a[44] )
and ( not a[266] or not a[44] )
and ( not a[265] or not a[44] )
and ( not a[264] or not a[44] )
and ( not a[263] or not a[44] )
and ( not a[262] or not a[44] )
and ( not a[261] or not a[44] )
and ( not a[260] or not a[44] )
and ( not a[259] or not a[44] )
and ( not a[258] or not a[44] )
and ( not a[257] or not a[44] )
and ( not a[256] or not a[44] )
and ( not a[255] or not a[44] )
and ( not a[254] or not a[44] )
and ( not a[253] or not a[44] )
and ( not a[252] or not a[44] )
and ( not a[251] or not a[44] )
and ( not a[250] or not a[44] )
and ( not a[249] or not a[44] )
and ( not a[248] or not a[44] )
and ( not a[247] or not a[44] )
and ( not a[246] or not a[44] )
and ( not a[245] or not a[44] )
and ( not a[244] or not a[44] )
and ( not a[243] or not a[44] )
and ( not a[242] or not a[44] )
and ( not a[241] or not a[44] )
and ( not a[240] or not a[44] )
and ( not a[239] or not a[44] )
and ( not a[238] or not a[44] )
and ( not a[237] or not a[44] )
and ( not a[236] or not a[44] )
and ( not a[235] or not a[44] )
and ( not a[234] or not a[44] )
and ( not a[233] or not a[44] )
and ( not a[232] or not a[44] )
and ( not a[231] or not a[44] )
and ( not a[230] or not a[44] )
and ( not a[229] or not a[44] )
and ( not a[228] or not a[44] )
and ( not a[227] or not a[44] )
and ( not a[226] or not a[44] )
and ( not a[225] or not a[44] )
and ( not a[224] or not a[44] )
and ( not a[223] or not a[44] )
and ( not a[222] or not a[44] )
and ( not a[221] or not a[44] )
and ( not a[220] or not a[44] )
and ( not a[219] or not a[44] )
and ( not a[218] or not a[44] )
and ( not a[217] or not a[44] )
and ( not a[216] or not a[44] )
and ( not a[215] or not a[44] )
and ( not a[214] or not a[44] )
and ( not a[213] or not a[44] )
and ( not a[212] or not a[44] )
and ( not a[211] or not a[44] )
and ( not a[210] or not a[44] )
and ( not a[209] or not a[44] )
and ( not a[208] or not a[44] )
and ( not a[207] or not a[44] )
and ( not a[206] or not a[44] )
and ( not a[205] or not a[44] )
and ( not a[204] or not a[44] )
and ( not a[203] or not a[44] )
and ( not a[202] or not a[44] )
and ( not a[201] or not a[44] )
and ( not a[200] or not a[44] )
and ( not a[199] or not a[44] )
and ( not a[198] or not a[44] )
and ( not a[197] or not a[44] )
and ( not a[196] or not a[44] )
and ( not a[195] or not a[44] )
and ( not a[194] or not a[44] )
and ( not a[193] or not a[44] )
and ( not a[192] or not a[44] )
and ( not a[191] or not a[44] )
and ( not a[190] or not a[44] )
and ( not a[189] or not a[44] )
and ( not a[188] or not a[44] )
and ( not a[187] or not a[44] )
and ( not a[186] or not a[44] )
and ( not a[185] or not a[44] )
and ( not a[184] or not a[44] )
and ( not a[183] or not a[44] )
and ( not a[182] or not a[44] )
and ( not a[181] or not a[44] )
and ( not a[180] or not a[44] )
and ( not a[179] or not a[44] )
and ( not a[178] or not a[44] )
and ( not a[177] or not a[44] )
and ( not a[176] or not a[44] )
and ( not a[175] or not a[44] )
and ( not a[174] or not a[44] )
and ( not a[173] or not a[44] )
and ( not a[172] or not a[44] )
and ( not a[171] or not a[44] )
and ( not a[170] or not a[44] )
and ( not a[169] or not a[44] )
and ( not a[168] or not a[44] )
and ( not a[167] or not a[44] )
and ( not a[166] or not a[44] )
and ( not a[165] or not a[44] )
and ( not a[164] or not a[44] )
and ( not a[163] or not a[44] )
and ( not a[162] or not a[44] )
and ( not a[161] or not a[44] )
and ( not a[160] or not a[44] )
and ( not a[159] or not a[44] )
and ( not a[158] or not a[44] )
and ( not a[157] or not a[44] )
and ( not a[156] or not a[44] )
and ( not a[155] or not a[44] )
and ( not a[154] or not a[44] )
and ( not a[153] or not a[44] )
and ( not a[148] or not a[44] )
and ( not a[146] or not a[44] )
and ( not a[142] or not a[44] )
and ( not a[139] or not a[44] )
and ( not a[138] or not a[44] )
and ( not a[131] or not a[44] )
and ( not a[129] or not a[44] )
and ( not a[125] or not a[44] )
and ( not a[122] or not a[44] )
and ( not a[120] or not a[44] )
and ( not a[116] or not a[44] )
and ( not a[96] or not a[44] )
and ( not a[89] or not a[44] )
and ( not a[86] or not a[44] )
and ( not a[84] or not a[44] )
and ( not a[83] or not a[44] )
and ( not a[82] or not a[44] )
and ( not a[81] or not a[44] )
and ( not a[80] or not a[44] )
and ( not a[79] or not a[44] )
and ( not a[77] or not a[44] )
and ( not a[76] or not a[44] )
and ( not a[73] or not a[44] )
and ( not a[71] or not a[44] )
and ( not a[44] or a[68] )
and ( not a[51] or not a[44] )
and ( not a[44] or a[50] )
and ( not a[47] or not a[44] )
and ( not a[46] or not a[44] )
and ( not a[44] or not a[42] )
and ( not a[311] or not a[46] )
and ( not a[310] or not a[46] )
and ( not a[309] or not a[46] )
and ( not a[308] or not a[46] )
and ( not a[307] or not a[46] )
and ( not a[306] or not a[46] )
and ( not a[305] or not a[46] )
and ( not a[304] or not a[46] )
and ( not a[303] or not a[46] )
and ( not a[302] or not a[46] )
and ( not a[301] or not a[46] )
and ( not a[300] or not a[46] )
and ( not a[299] or not a[46] )
and ( not a[298] or not a[46] )
and ( not a[297] or not a[46] )
and ( not a[296] or not a[46] )
and ( not a[295] or not a[46] )
and ( not a[294] or not a[46] )
and ( not a[293] or not a[46] )
and ( not a[292] or not a[46] )
and ( not a[291] or not a[46] )
and ( not a[290] or not a[46] )
and ( not a[289] or not a[46] )
and ( not a[288] or not a[46] )
and ( not a[285] or not a[46] )
and ( not a[284] or not a[46] )
and ( not a[283] or not a[46] )
and ( not a[282] or not a[46] )
and ( not a[281] or not a[46] )
and ( not a[280] or not a[46] )
and ( not a[279] or not a[46] )
and ( not a[278] or not a[46] )
and ( not a[277] or not a[46] )
and ( not a[276] or not a[46] )
and ( not a[275] or not a[46] )
and ( not a[274] or not a[46] )
and ( not a[273] or not a[46] )
and ( not a[272] or not a[46] )
and ( not a[271] or not a[46] )
and ( not a[270] or not a[46] )
and ( not a[269] or not a[46] )
and ( not a[268] or not a[46] )
and ( not a[267] or not a[46] )
and ( not a[266] or not a[46] )
and ( not a[265] or not a[46] )
and ( not a[264] or not a[46] )
and ( not a[263] or not a[46] )
and ( not a[262] or not a[46] )
and ( not a[261] or not a[46] )
and ( not a[260] or not a[46] )
and ( not a[259] or not a[46] )
and ( not a[258] or not a[46] )
and ( not a[257] or not a[46] )
and ( not a[255] or not a[46] )
and ( not a[254] or not a[46] )
and ( not a[253] or not a[46] )
and ( not a[252] or not a[46] )
and ( not a[251] or not a[46] )
and ( not a[250] or not a[46] )
and ( not a[249] or not a[46] )
and ( not a[248] or not a[46] )
and ( not a[247] or not a[46] )
and ( not a[246] or not a[46] )
and ( not a[242] or not a[46] )
and ( not a[241] or not a[46] )
and ( not a[240] or not a[46] )
and ( not a[238] or not a[46] )
and ( not a[237] or not a[46] )
and ( not a[236] or not a[46] )
and ( not a[235] or not a[46] )
and ( not a[234] or not a[46] )
and ( not a[233] or not a[46] )
and ( not a[232] or not a[46] )
and ( not a[231] or not a[46] )
and ( not a[230] or not a[46] )
and ( not a[229] or not a[46] )
and ( not a[227] or not a[46] )
and ( not a[226] or not a[46] )
and ( not a[225] or not a[46] )
and ( not a[224] or not a[46] )
and ( not a[223] or not a[46] )
and ( not a[222] or not a[46] )
and ( not a[221] or not a[46] )
and ( not a[220] or not a[46] )
and ( not a[219] or not a[46] )
and ( not a[218] or not a[46] )
and ( not a[217] or not a[46] )
and ( not a[216] or not a[46] )
and ( not a[214] or not a[46] )
and ( not a[212] or not a[46] )
and ( not a[211] or not a[46] )
and ( not a[210] or not a[46] )
and ( not a[209] or not a[46] )
and ( not a[208] or not a[46] )
and ( not a[207] or not a[46] )
and ( not a[206] or not a[46] )
and ( not a[204] or not a[46] )
and ( not a[203] or not a[46] )
and ( not a[201] or not a[46] )
and ( not a[200] or not a[46] )
and ( not a[199] or not a[46] )
and ( not a[198] or not a[46] )
and ( not a[195] or not a[46] )
and ( not a[194] or not a[46] )
and ( not a[191] or not a[46] )
and ( not a[190] or not a[46] )
and ( not a[189] or not a[46] )
and ( not a[188] or not a[46] )
and ( not a[187] or not a[46] )
and ( not a[186] or not a[46] )
and ( not a[185] or not a[46] )
and ( not a[184] or not a[46] )
and ( not a[182] or not a[46] )
and ( not a[181] or not a[46] )
and ( not a[180] or not a[46] )
and ( not a[179] or not a[46] )
and ( not a[178] or not a[46] )
and ( not a[177] or not a[46] )
and ( not a[175] or not a[46] )
and ( not a[174] or not a[46] )
and ( not a[172] or not a[46] )
and ( not a[171] or not a[46] )
and ( not a[170] or not a[46] )
and ( not a[169] or not a[46] )
and ( not a[168] or not a[46] )
and ( not a[167] or not a[46] )
and ( not a[166] or not a[46] )
and ( not a[165] or not a[46] )
and ( not a[164] or not a[46] )
and ( not a[163] or not a[46] )
and ( not a[162] or not a[46] )
and ( not a[161] or not a[46] )
and ( not a[160] or not a[46] )
and ( not a[159] or not a[46] )
and ( not a[158] or not a[46] )
and ( not a[157] or not a[46] )
and ( not a[156] or not a[46] )
and ( not a[155] or not a[46] )
and ( not a[154] or not a[46] )
and ( not a[153] or not a[46] )
and ( not a[149] or not a[46] )
and ( not a[146] or not a[46] )
and ( not a[142] or not a[46] )
and ( not a[133] or not a[46] )
and ( not a[129] or not a[46] )
and ( not a[122] or not a[46] )
and ( not a[120] or not a[46] )
and ( not a[116] or not a[46] )
and ( not a[112] or not a[46] )
and ( not a[96] or not a[46] )
and ( not a[93] or not a[46] )
and ( not a[89] or not a[46] )
and ( not a[86] or not a[46] )
and ( not a[85] or not a[46] )
and ( not a[84] or not a[46] )
and ( not a[83] or not a[46] )
and ( not a[82] or not a[46] )
and ( not a[81] or not a[46] )
and ( not a[80] or not a[46] )
and ( not a[79] or not a[46] )
and ( not a[77] or not a[46] )
and ( not a[74] or not a[46] )
and ( not a[73] or not a[46] )
and ( not a[71] or not a[46] )
and ( not a[67] or not a[46] )
and ( not a[66] or not a[46] )
and ( not a[65] or not a[46] )
and ( not a[51] or not a[46] or a[287] )
and ( not a[51] or not a[46] or a[286] )
and ( not a[50] or not a[46] or a[287] )
and ( not a[50] or not a[46] or a[286] )
and ( not a[47] or not a[46] )
and ( not a[46] or not a[44] )
and ( not a[46] or not a[42] )
and ( not a[51] or not a[46] or not a[40] )
and ( not a[50] or not a[46] or not a[40] )
and ( not a[286] or not a[226] )
and ( not a[312] or not a[191] )
and ( not a[191] or not a[44] )
and ( not a[191] or not a[46] )
and ( not a[191] or not a[47] )
and ( not a[250] or not a[191] )
and ( not a[314] or a[43] )
and ( not a[315] or not a[314] )
and ( not a[316] or not a[314] )
and ( not a[317] or not a[314] )
and ( not a[318] or not a[314] )
and ( not a[314] or not a[116] )
and ( not a[319] or not a[287] )
and ( not a[321] or not a[320] )
and ( not a[322] or not a[320] )
and ( not a[320] or not a[195] )
and ( not a[323] or not a[320] )
and ( not a[324] or not a[320] )
and ( not a[325] or not a[320] )
and ( not a[326] or not a[320] )
and ( not a[327] or not a[320] )
and ( not a[320] or not a[205] )
and ( not a[328] or not a[320] )
and ( not a[329] or not a[320] )
and ( not a[298] or a[330] )
and ( not a[298] or not a[46] )
and ( not a[298] or not a[196] )
and ( not a[298] or not a[197] )
and ( not a[331] or not a[298] )
and ( not a[298] or not a[47] )
and ( not a[332] or not a[298] )
and ( not a[333] or not a[298] )
and ( not a[334] or not a[298] )
and ( not a[335] or not a[298] )
and ( not a[336] or not a[298] )
and ( not a[337] or not a[298] )
and ( not a[338] or not a[298] )
and ( not a[321] or not a[298] )
and ( not a[339] or not a[298] )
and ( not a[340] or not a[298] )
and ( not a[341] or not a[298] )
and ( not a[203] or not a[44] )
and ( not a[203] or not a[46] )
and ( not a[342] or not a[203] )
and ( not a[203] or not a[47] )
and ( not a[343] or a[72] or a[100] or a[101] or a[102] )
and ( not a[343] or not a[46] )
and ( not a[343] or not a[76] )
and ( not a[343] or not a[247] )
and ( not a[343] or not a[248] )
and ( not a[343] or not a[249] )
and ( not a[99] or not a[98] )
and ( not a[344] or not a[47] )
and ( not a[346] or not a[345] )
and ( not a[347] or not a[345] )
and ( not a[345] or not a[45] )
and ( not a[348] or not a[345] )
and ( not a[349] or not a[345] )
and ( not a[350] or not a[345] )
and ( not a[351] or not a[345] )
and ( not a[352] or not a[345] )
and ( not a[353] or not a[345] )
and ( not a[354] or not a[345] )
and ( not a[355] or not a[345] )
and ( not a[356] or not a[345] )
and ( not a[357] or not a[345] )
and ( not a[358] or not a[345] )
and ( not a[359] or not a[345] )
and ( not a[362] or not a[361] )
and ( not a[362] or not a[361] )
and ( not a[362] or not a[111] )
and ( not a[362] or not a[110] )
and ( not a[363] or not a[362] )
and ( not a[365] or a[366] )
and ( not a[367] or not a[365] )
and ( not a[368] or not a[365] )
and ( not a[369] or not a[365] )
and ( not a[370] or not a[365] )
and ( not a[371] or not a[365] )
and ( not a[372] or not a[365] )
and ( not a[373] or not a[365] )
and ( not a[374] or not a[365] )
and ( not a[375] or not a[365] )
and ( not a[376] or not a[365] )
and ( not a[377] or not a[365] )
and ( not a[378] or not a[365] )
and ( not a[379] or not a[365] )
and ( not a[380] or not a[365] )
and ( not a[381] or not a[365] )
and ( not a[382] or not a[365] )
and ( not a[383] or not a[365] )
and ( not a[384] or not a[365] )
and ( not a[385] or not a[365] )
and ( not a[386] or not a[365] )
and ( not a[387] or not a[365] )
and ( not a[388] or not a[365] )
and ( not a[389] or not a[365] )
and ( not a[390] or not a[365] )
and ( not a[366] or a[365] )
and ( not a[391] or not a[366] )
and ( not a[392] or not a[366] )
and ( not a[393] or not a[366] )
and ( not a[394] or not a[366] )
and ( not a[395] or not a[366] )
and ( not a[396] or not a[366] )
and ( not a[397] or not a[366] )
and ( not a[398] or not a[366] )
and ( not a[399] or not a[366] )
and ( not a[400] or not a[366] )
and ( not a[401] or not a[366] )
and ( not a[402] or not a[366] )
and ( not a[403] or not a[366] )
and ( not a[404] or not a[366] )
and ( not a[405] or not a[366] )
and ( not a[406] or not a[366] )
and ( not a[390] or not a[366] )
and ( not a[407] or not a[366] )
and ( not a[408] or a[58] )
and ( not a[36] or a[0] or a[3] or a[4] or a[5] or a[6] or a[7] or a[8] or a[9] or a[10] or a[11] or a[12] or a[13] or a[14] or a[15] or a[16] or a[17] or a[18] or a[19] or a[20] or a[21] or a[22] or a[23] or a[24] or a[25] or a[26] or a[27] or a[28] or a[29] or a[30] or a[31] or a[32] or a[33] or a[34] or a[35] )
and ( not a[37] or a[0] or a[3] or a[4] or a[5] or a[6] or a[7] or a[8] or a[9] or a[10] or a[11] or a[12] or a[13] or a[14] or a[15] or a[16] or a[17] or a[18] or a[19] or a[20] or a[21] or a[22] or a[23] or a[24] or a[25] or a[26] or a[27] or a[28] or a[29] or a[30] or a[31] or a[32] or a[33] or a[34] or a[35] )
and ( not a[38] or a[0] or a[3] or a[4] or a[5] or a[6] or a[7] or a[8] or a[9] or a[10] or a[11] or a[12] or a[13] or a[14] or a[15] or a[16] or a[17] or a[18] or a[19] or a[20] or a[21] or a[22] or a[23] or a[24] or a[25] or a[26] or a[27] or a[28] or a[29] or a[30] or a[31] or a[32] or a[33] or a[34] or a[35] )
and ( not a[39] or a[0] or a[3] or a[4] or a[5] or a[6] or a[7] or a[8] or a[9] or a[10] or a[11] or a[12] or a[13] or a[14] or a[15] or a[16] or a[17] or a[18] or a[19] or a[20] or a[21] or a[22] or a[23] or a[24] or a[25] or a[26] or a[27] or a[28] or a[29] or a[30] or a[31] or a[32] or a[33] or a[34] or a[35] )
and ( not a[408] or a[58] or a[59] )
and ( not a[55] or not a[50] or a[52] )
and ( not a[51] or not a[49] or a[52] )
and ( not a[44] or a[68] )
and ( not a[46] or a[226] or a[286] )
and ( not a[46] or a[313] )
and ( not a[46] or a[287] or a[319] )
and ( not a[298] or a[330] )
and ( a[45] or a[345] or a[346] or a[347] or a[348] or a[349] or a[350] or a[351] or a[352] or a[353] or a[354] or a[355] or a[356] or a[357] or a[358] or a[359] )
and ( not a[110] or a[361] or a[362] )
and ( a[110] or a[111] or a[361] or a[362] or a[363] )
and ( a[50] or a[51] )
and ( not a[51] or not a[50] )
) ;