variable
  public a : array 1465 of boolean ; 

rule
( 
 (  a[482] ) 
 and  (  a[509] ) 
 and  (  a[510] ) 
 and  (  a[511]  or  a[512] ) 
 and  ( not a[512]  or not a[511] ) 
 and  ( not a[513] ) 
 and  ( not a[514] ) 
 and  ( not a[515] ) 
 and  ( not a[516] ) 
 and  ( not a[517] ) 
 and  ( not a[1] ) 
 and  ( not a[220] ) 
 and  ( not a[518] ) 
 and  ( not a[519] ) 
 and  ( not a[520] ) 
 and  ( not a[521] ) 
 and  ( not a[522] ) 
 and  ( not a[523] ) 
 and  ( not a[524] ) 
 and  ( not a[525] ) 
 and  ( not a[526] ) 
 and  ( not a[527] ) 
 and  ( not a[528] ) 
 and  ( not a[40] ) 
 and  ( not a[529] ) 
 and  ( not a[530] ) 
 and  ( not a[531] ) 
 and  ( not a[532] ) 
 and  ( not a[533] ) 
 and  ( not a[3] ) 
 and  ( not a[534] ) 
 and  ( not a[4] ) 
 and  ( not a[535] ) 
 and  ( not a[536] ) 
 and  ( not a[537] ) 
 and  ( not a[538] ) 
 and  ( not a[62] ) 
 and  ( not a[63] ) 
 and  ( not a[65] ) 
 and  ( not a[66] ) 
 and  ( not a[78] ) 
 and  ( not a[539] ) 
 and  ( not a[540] ) 
 and  ( not a[79] ) 
 and  ( not a[541] ) 
 and  ( not a[68] ) 
 and  ( not a[80] ) 
 and  ( not a[69] ) 
 and  ( not a[81] ) 
 and  ( not a[70] ) 
 and  ( not a[249] ) 
 and  ( not a[542] ) 
 and  ( not a[71] ) 
 and  ( not a[543] ) 
 and  ( not a[72] ) 
 and  ( not a[544] ) 
 and  ( not a[73] ) 
 and  ( not a[545] ) 
 and  ( not a[85] ) 
 and  ( not a[546] ) 
 and  ( not a[6] ) 
 and  ( not a[547] ) 
 and  ( not a[548] ) 
 and  ( not a[549] ) 
 and  ( not a[107] ) 
 and  ( not a[550] ) 
 and  ( not a[551] ) 
 and  ( not a[552] ) 
 and  ( not a[553] ) 
 and  ( not a[250] ) 
 and  ( not a[554] ) 
 and  ( not a[555] ) 
 and  ( not a[7] ) 
 and  ( not a[556] ) 
 and  ( not a[8] ) 
 and  ( not a[557] ) 
 and  ( not a[558] ) 
 and  ( not a[9] ) 
 and  ( not a[559] ) 
 and  ( not a[10] ) 
 and  ( not a[560] ) 
 and  ( not a[251] ) 
 and  ( not a[561] ) 
 and  ( not a[11] ) 
 and  ( not a[12] ) 
 and  ( not a[13] ) 
 and  ( not a[562] ) 
 and  ( not a[184] ) 
 and  ( not a[563] ) 
 and  ( not a[564] ) 
 and  ( not a[173] ) 
 and  ( not a[565] ) 
 and  ( not a[174] ) 
 and  ( not a[148] ) 
 and  ( not a[160] ) 
 and  ( not a[566] ) 
 and  ( not a[567] ) 
 and  ( not a[568] ) 
 and  ( not a[569] ) 
 and  ( not a[570] ) 
 and  ( not a[571] ) 
 and  ( not a[572] ) 
 and  ( not a[94] ) 
 and  ( not a[573] ) 
 and  ( not a[574] ) 
 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[150] ) 
 and  ( not a[115] ) 
 and  ( not a[582] ) 
 and  ( not a[116] ) 
 and  ( not a[117] ) 
 and  ( not a[583] ) 
 and  ( not a[584] ) 
 and  ( not a[585] ) 
 and  ( not a[586] ) 
 and  ( not a[587] ) 
 and  ( not a[588] ) 
 and  ( not a[135] ) 
 and  ( not a[589] ) 
 and  ( not a[590] ) 
 and  ( not a[369] ) 
 and  ( not a[591] ) 
 and  ( not a[592] ) 
 and  ( not a[593] ) 
 and  ( not a[594] ) 
 and  ( not a[151] ) 
 and  ( not a[252] ) 
 and  ( not a[374] ) 
 and  ( not a[595] ) 
 and  ( not a[596] ) 
 and  ( not a[355] ) 
 and  ( not a[175] ) 
 and  ( not a[118] ) 
 and  ( not a[597] ) 
 and  ( not a[119] ) 
 and  ( not a[253] ) 
 and  ( not a[143] ) 
 and  ( not a[176] ) 
 and  ( not a[177] ) 
 and  ( not a[598] ) 
 and  ( not a[254] ) 
 and  ( not a[255] ) 
 and  ( not a[214] ) 
 and  ( not a[256] ) 
 and  ( not a[104] ) 
 and  ( not a[599] ) 
 and  ( not a[600] ) 
 and  ( not a[257] ) 
 and  ( not a[258] ) 
 and  ( not a[601] ) 
 and  ( not a[124] ) 
 and  ( not a[161] ) 
 and  ( not a[142] ) 
 and  ( not a[602] ) 
 and  ( not a[178] ) 
 and  ( not a[179] ) 
 and  ( not a[603] ) 
 and  ( not a[604] ) 
 and  ( not a[605] ) 
 and  ( not a[606] ) 
 and  ( not a[607] ) 
 and  ( not a[14] ) 
 and  ( not a[608] ) 
 and  ( not a[456] ) 
 and  ( not a[457] ) 
 and  ( not a[458] ) 
 and  ( not a[459] ) 
 and  ( not a[460] ) 
 and  ( not a[609] ) 
 and  ( not a[15] ) 
 and  ( not a[610] ) 
 and  ( not a[611] ) 
 and  ( not a[612] ) 
 and  ( not a[613] ) 
 and  ( not a[614] ) 
 and  ( not a[615] ) 
 and  ( not a[616] ) 
 and  ( not a[202] ) 
 and  ( not a[203] ) 
 and  ( not a[204] ) 
 and  ( not a[481] ) 
 and  ( not a[205] ) 
 and  ( not a[206] ) 
 and  ( not a[617] ) 
 and  ( not a[618] ) 
 and  ( not a[16] ) 
 and  ( not a[619] ) 
 and  ( not a[620] ) 
 and  ( not a[222] ) 
 and  ( not a[17] ) 
 and  ( not a[621] ) 
 and  ( not a[622] ) 
 and  ( not a[191] ) 
 and  ( not a[623] ) 
 and  ( not a[624] ) 
 and  ( not a[41] ) 
 and  ( not a[87] ) 
 and  ( not a[625] ) 
 and  ( not a[626] ) 
 and  ( not a[627] ) 
 and  ( not a[230] ) 
 and  ( not a[259] ) 
 and  ( not a[18] ) 
 and  ( not a[628] ) 
 and  ( not a[629] ) 
 and  ( not a[630] ) 
 and  ( not a[631] ) 
 and  ( not a[19] ) 
 and  ( not a[632] ) 
 and  ( not a[633] ) 
 and  ( not a[634] ) 
 and  ( not a[635] ) 
 and  ( not a[636] ) 
 and  ( not a[20] ) 
 and  ( not a[637] ) 
 and  ( not a[638] ) 
 and  ( not a[21] ) 
 and  ( not a[639] ) 
 and  ( not a[640] ) 
 and  ( not a[641] ) 
 and  ( not a[642] ) 
 and  ( not a[643] ) 
 and  ( not a[644] ) 
 and  ( not a[645] ) 
 and  ( not a[646] ) 
 and  ( not a[647] ) 
 and  ( not a[152] ) 
 and  ( not a[164] ) 
 and  ( not a[453] ) 
 and  ( not a[648] ) 
 and  ( not a[454] ) 
 and  ( not a[370] ) 
 and  ( not a[42] ) 
 and  ( not a[649] ) 
 and  ( not a[43] ) 
 and  ( not a[44] ) 
 and  ( not a[56] ) 
 and  ( not a[372] ) 
 and  ( not a[650] ) 
 and  ( not a[651] ) 
 and  ( not a[57] ) 
 and  ( not a[652] ) 
 and  ( not a[653] ) 
 and  ( not a[58] ) 
 and  ( not a[261] ) 
 and  ( not a[45] ) 
 and  ( not a[262] ) 
 and  ( not a[263] ) 
 and  ( not a[46] ) 
 and  ( not a[654] ) 
 and  ( not a[655] ) 
 and  ( not a[47] ) 
 and  ( not a[656] ) 
 and  ( not a[657] ) 
 and  ( not a[658] ) 
 and  ( not a[108] ) 
 and  ( not a[375] ) 
 and  ( not a[22] ) 
 and  ( not a[23] ) 
 and  ( not a[659] ) 
 and  ( not a[24] ) 
 and  ( not a[660] ) 
 and  ( not a[661] ) 
 and  ( not a[662] ) 
 and  ( not a[25] ) 
 and  ( not a[26] ) 
 and  ( not a[378] ) 
 and  ( not a[663] ) 
 and  ( not a[165] ) 
 and  ( not a[379] ) 
 and  ( not a[664] ) 
 and  ( not a[380] ) 
 and  ( not a[381] ) 
 and  ( not a[27] ) 
 and  ( not a[665] ) 
 and  ( not a[387] ) 
 and  ( not a[666] ) 
 and  ( not a[223] ) 
 and  ( not a[667] ) 
 and  ( not a[98] ) 
 and  ( not a[668] ) 
 and  ( not a[266] ) 
 and  ( not a[267] ) 
 and  ( not a[28] ) 
 and  ( not a[669] ) 
 and  ( not a[424] ) 
 and  ( not a[268] ) 
 and  ( not a[670] ) 
 and  ( not a[425] ) 
 and  ( not a[671] ) 
 and  ( not a[426] ) 
 and  ( not a[672] ) 
 and  ( not a[673] ) 
 and  ( not a[270] ) 
 and  ( not a[427] ) 
 and  ( not a[674] ) 
 and  ( not a[428] ) 
 and  ( not a[429] ) 
 and  ( not a[271] ) 
 and  ( not a[430] ) 
 and  ( not a[431] ) 
 and  ( not a[675] ) 
 and  ( not a[357] ) 
 and  ( not a[432] ) 
 and  ( not a[433] ) 
 and  ( not a[434] ) 
 and  ( not a[435] ) 
 and  ( not a[436] ) 
 and  ( not a[676] ) 
 and  ( not a[677] ) 
 and  ( not a[273] ) 
 and  ( not a[678] ) 
 and  ( not a[358] ) 
 and  ( not a[679] ) 
 and  ( not a[680] ) 
 and  ( not a[215] ) 
 and  ( not a[29] ) 
 and  ( not a[437] ) 
 and  ( not a[438] ) 
 and  ( not a[681] ) 
 and  ( not a[274] ) 
 and  ( not a[275] ) 
 and  ( not a[441] ) 
 and  ( not a[682] ) 
 and  ( not a[48] ) 
 and  ( not a[276] ) 
 and  ( not a[683] ) 
 and  ( not a[684] ) 
 and  ( not a[685] ) 
 and  ( not a[686] ) 
 and  ( not a[687] ) 
 and  ( not a[278] ) 
 and  ( not a[688] ) 
 and  ( not a[689] ) 
 and  ( not a[690] ) 
 and  ( not a[382] ) 
 and  ( not a[691] ) 
 and  ( not a[383] ) 
 and  ( not a[279] ) 
 and  ( not a[692] ) 
 and  ( not a[384] ) 
 and  ( not a[385] ) 
 and  ( not a[693] ) 
 and  ( not a[30] ) 
 and  ( not a[694] ) 
 and  ( not a[280] ) 
 and  ( not a[224] ) 
 and  ( not a[225] ) 
 and  ( not a[226] ) 
 and  ( not a[281] ) 
 and  ( not a[282] ) 
 and  ( not a[695] ) 
 and  ( not a[696] ) 
 and  ( not a[697] ) 
 and  ( not a[698] ) 
 and  ( not a[699] ) 
 and  ( not a[283] ) 
 and  ( not a[284] ) 
 and  ( not a[700] ) 
 and  ( not a[701] ) 
 and  ( not a[285] ) 
 and  ( not a[702] ) 
 and  ( not a[703] ) 
 and  ( not a[704] ) 
 and  ( not a[705] ) 
 and  ( not a[706] ) 
 and  ( not a[707] ) 
 and  ( not a[31] ) 
 and  ( not a[708] ) 
 and  ( not a[709] ) 
 and  ( not a[710] ) 
 and  ( not a[711] ) 
 and  ( not a[712] ) 
 and  ( not a[166] ) 
 and  ( not a[59] ) 
 and  ( not a[167] ) 
 and  ( not a[168] ) 
 and  ( not a[169] ) 
 and  ( not a[286] ) 
 and  ( not a[170] ) 
 and  ( not a[713] ) 
 and  ( not a[171] ) 
 and  ( not a[172] ) 
 and  ( not a[439] ) 
 and  ( not a[714] ) 
 and  ( not a[715] ) 
 and  ( not a[360] ) 
 and  ( not a[416] ) 
 and  ( not a[32] ) 
 and  ( not a[716] ) 
 and  ( not a[717] ) 
 and  ( not a[287] ) 
 and  ( not a[718] ) 
 and  ( not a[417] ) 
 and  ( not a[49] ) 
 and  ( not a[288] ) 
 and  ( not a[719] ) 
 and  ( not a[418] ) 
 and  ( not a[88] ) 
 and  ( not a[89] ) 
 and  ( not a[90] ) 
 and  ( not a[720] ) 
 and  ( not a[289] ) 
 and  ( not a[419] ) 
 and  ( not a[290] ) 
 and  ( not a[361] ) 
 and  ( not a[420] ) 
 and  ( not a[721] ) 
 and  ( not a[421] ) 
 and  ( not a[440] ) 
 and  ( not a[422] ) 
 and  ( not a[146] ) 
 and  ( not a[722] ) 
 and  ( not a[723] ) 
 and  ( not a[724] ) 
 and  ( not a[725] ) 
 and  ( not a[726] ) 
 and  ( not a[727] ) 
 and  ( not a[728] ) 
 and  ( not a[729] ) 
 and  ( not a[730] ) 
 and  ( not a[731] ) 
 and  ( not a[732] ) 
 and  ( not a[455] ) 
 and  ( not a[733] ) 
 and  ( not a[734] ) 
 and  ( not a[415] ) 
 and  ( not a[291] ) 
 and  ( not a[292] ) 
 and  ( not a[293] ) 
 and  ( not a[294] ) 
 and  ( not a[141] ) 
 and  ( not a[295] ) 
 and  ( not a[296] ) 
 and  ( not a[297] ) 
 and  ( not a[298] ) 
 and  ( not a[299] ) 
 and  ( not a[300] ) 
 and  ( not a[147] ) 
 and  ( not a[301] ) 
 and  ( not a[302] ) 
 and  ( not a[303] ) 
 and  ( not a[125] ) 
 and  ( not a[735] ) 
 and  ( not a[736] ) 
 and  ( not a[737] ) 
 and  ( not a[126] ) 
 and  ( not a[127] ) 
 and  ( not a[128] ) 
 and  ( not a[129] ) 
 and  ( not a[471] ) 
 and  ( not a[738] ) 
 and  ( not a[739] ) 
 and  ( not a[376] ) 
 and  ( not a[740] ) 
 and  ( not a[741] ) 
 and  ( not a[304] ) 
 and  ( not a[742] ) 
 and  ( not a[743] ) 
 and  ( not a[744] ) 
 and  ( not a[33] ) 
 and  ( not a[99] ) 
 and  ( not a[745] ) 
 and  ( not a[746] ) 
 and  ( not a[747] ) 
 and  ( not a[132] ) 
 and  ( not a[748] ) 
 and  ( not a[91] ) 
 and  ( not a[749] ) 
 and  ( not a[750] ) 
 and  ( not a[751] ) 
 and  ( not a[207] ) 
 and  ( not a[752] ) 
 and  ( not a[753] ) 
 and  ( not a[754] ) 
 and  ( not a[755] ) 
 and  ( not a[305] ) 
 and  ( not a[756] ) 
 and  ( not a[757] ) 
 and  ( not a[306] ) 
 and  ( not a[758] ) 
 and  ( not a[130] ) 
 and  ( not a[362] ) 
 and  ( not a[309] ) 
 and  ( not a[216] ) 
 and  ( not a[310] ) 
 and  ( not a[759] ) 
 and  ( not a[760] ) 
 and  ( not a[311] ) 
 and  ( not a[312] ) 
 and  ( not a[761] ) 
 and  ( not a[762] ) 
 and  ( not a[217] ) 
 and  ( not a[763] ) 
 and  ( not a[133] ) 
 and  ( not a[134] ) 
 and  ( not a[218] ) 
 and  ( not a[219] ) 
 and  ( not a[194] ) 
 and  ( not a[195] ) 
 and  ( not a[764] ) 
 and  ( not a[155] ) 
 and  ( not a[765] ) 
 and  ( not a[156] ) 
 and  ( not a[766] ) 
 and  ( not a[157] ) 
 and  ( not a[196] ) 
 and  ( not a[313] ) 
 and  ( not a[314] ) 
 and  ( not a[315] ) 
 and  ( not a[767] ) 
 and  ( not a[316] ) 
 and  ( not a[317] ) 
 and  ( not a[318] ) 
 and  ( not a[319] ) 
 and  ( not a[768] ) 
 and  ( not a[769] ) 
 and  ( not a[320] ) 
 and  ( not a[321] ) 
 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[464] ) 
 and  ( not a[873] ) 
 and  ( not a[874] ) 
 and  ( not a[875] ) 
 and  ( not a[876] ) 
 and  ( not a[465] ) 
 and  ( not a[466] ) 
 and  ( not a[467] ) 
 and  ( not a[469] ) 
 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[912] ) 
 and  ( not a[913] ) 
 and  ( not a[914] ) 
 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[97] ) 
 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[1055] ) 
 and  ( not a[1056] ) 
 and  ( not a[1057] ) 
 and  ( not a[1058] ) 
 and  ( not a[1059] ) 
 and  ( not a[1060] ) 
 and  ( not a[1061] ) 
 and  ( not a[1062] ) 
 and  ( not a[1063] ) 
 and  ( not a[1064] ) 
 and  ( not a[1065] ) 
 and  ( not a[1066] ) 
 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[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[484] ) 
 and  ( not a[485] ) 
 and  ( not a[1100] ) 
 and  ( not a[486] ) 
 and  ( not a[487] ) 
 and  ( not a[488] ) 
 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[1101] ) 
 and  ( not a[495] ) 
 and  ( not a[496] ) 
 and  ( not a[497] ) 
 and  ( not a[498] ) 
 and  ( not a[1102] ) 
 and  ( not a[499] ) 
 and  ( not a[1103] ) 
 and  ( not a[1104] ) 
 and  ( not a[1105] ) 
 and  ( not a[500] ) 
 and  ( not a[501] ) 
 and  ( not a[1106] ) 
 and  ( not a[502] ) 
 and  ( not a[1107] ) 
 and  ( not a[503] ) 
 and  ( not a[504] ) 
 and  ( not a[505] ) 
 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[506] ) 
 and  ( not a[507] ) 
 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[423] ) 
 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[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[371] ) 
 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[468] ) 
 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[1326] ) 
 and  ( not a[1327] ) 
 and  ( not a[1328] ) 
 and  ( not a[1329] ) 
 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[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[238] ) 
 and  ( not a[239] ) 
 and  ( not a[240] ) 
 and  ( not a[241] ) 
 and  ( not a[242] ) 
 and  ( not a[243] ) 
 and  ( not a[349] ) 
 and  ( not a[244] ) 
 and  ( not a[350] ) 
 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[351] ) 
 and  ( not a[245] ) 
 and  ( not a[246] ) 
 and  ( not a[247] ) 
 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[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[322] ) 
 and  ( not a[323] ) 
 and  ( not a[324] ) 
 and  ( not a[325] ) 
 and  ( not a[326] ) 
 and  ( not a[327] ) 
 and  ( not a[328] ) 
 and  ( not a[329] ) 
 and  ( not a[1380] ) 
 and  ( not a[1381] ) 
 and  ( not a[1382] ) 
 and  ( not a[330] ) 
 and  ( not a[331] ) 
 and  ( not a[332] ) 
 and  ( not a[333] ) 
 and  ( not a[334] ) 
 and  ( not a[1383] ) 
 and  ( not a[335] ) 
 and  ( not a[336] ) 
 and  ( not a[337] ) 
 and  ( not a[363] ) 
 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[338] ) 
 and  ( not a[339] ) 
 and  ( not a[364] ) 
 and  ( not a[340] ) 
 and  ( not a[341] ) 
 and  ( not a[365] ) 
 and  ( not a[342] ) 
 and  ( not a[343] ) 
 and  ( not a[366] ) 
 and  ( not a[344] ) 
 and  ( not a[345] ) 
 and  ( not a[367] ) 
 and  ( not a[346] ) 
 and  ( not a[347] ) 
 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  ( not a[1411] ) 
 and  ( not a[1412] ) 
 and  ( not a[1413] ) 
 and  ( not a[1414] ) 
 and  ( not a[1415] ) 
 and  ( not a[1416] ) 
 and  ( not a[1417] ) 
 and  ( not a[248] ) 
 and  ( not a[136] ) 
 and  ( not a[137] ) 
 and  ( not a[138] ) 
 and  ( not a[352] ) 
 and  ( not a[353] ) 
 and  ( not a[354] ) 
 and  ( not a[1418] ) 
 and  ( not a[1419] ) 
 and  ( not a[1420] ) 
 and  ( not a[1421] ) 
 and  ( not a[1422] ) 
 and  ( not a[1423] ) 
 and  ( not a[1424] ) 
 and  ( not a[1425] ) 
 and  ( not a[1426] ) 
 and  ( not a[1427] ) 
 and  ( not a[1428] ) 
 and  ( not a[1429] ) 
 and  ( not a[1430] ) 
 and  ( not a[1431] ) 
 and  ( not a[1432] ) 
 and  ( not a[1433] ) 
 and  ( not a[1434] ) 
 and  ( not a[1435] ) 
 and  ( not a[1436] ) 
 and  ( not a[1437] ) 
 and  ( not a[1438] ) 
 and  ( not a[1439] ) 
 and  ( not a[1440] ) 
 and  ( not a[1441] ) 
 and  ( not a[1442] ) 
 and  ( not a[1443] ) 
 and  ( not a[1444] ) 
 and  ( not a[1445] ) 
 and  ( not a[1446] ) 
 and  ( not a[1447] ) 
 and  ( not a[1448] ) 
 and  ( not a[1449] ) 
 and  ( not a[1450] ) 
 and  ( not a[1451] ) 
 and  ( not a[1452] ) 
 and  ( not a[1453] ) 
 and  ( not a[1454] ) 
 and  ( not a[1455] ) 
 and  ( not a[1456] ) 
 and  ( not a[1457] ) 
 and  ( not a[1458] ) 
 and  ( not a[1459] ) 
 and  ( not a[1460] ) 
 and  ( not a[1461] ) 
 and  ( not a[1462] ) 
 and  ( not a[1463] ) 
 and  ( not a[1464] ) 
 and  (  a[508] ) 
 and  (  a[483] ) 
 and  ( not a[1]  or not a[0] ) 
 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  a[0] ) 
 and  ( not a[35]  or  a[0] ) 
 and  ( not a[36]  or  a[0] ) 
 and  ( not a[38]  or  a[0] ) 
 and  ( not a[2]  or not a[0] ) 
 and  ( not a[2]  or not a[1] ) 
 and  ( not a[40]  or not a[2] ) 
 and  ( not a[5]  or not a[2] ) 
 and  ( not a[15]  or not a[2] ) 
 and  ( not a[16]  or not a[2] ) 
 and  ( not a[41]  or not a[2] ) 
 and  ( not a[18]  or not a[2] ) 
 and  ( not a[42]  or not a[2] ) 
 and  ( not a[43]  or not a[2] ) 
 and  ( not a[44]  or not a[2] ) 
 and  ( not a[45]  or not a[2] ) 
 and  ( not a[46]  or not a[2] ) 
 and  ( not a[47]  or not a[2] ) 
 and  ( not a[22]  or not a[2] ) 
 and  ( not a[27]  or not a[2] ) 
 and  ( not a[28]  or not a[2] ) 
 and  ( not a[48]  or not a[2] ) 
 and  ( not a[30]  or not a[2] ) 
 and  ( not a[31]  or not a[2] ) 
 and  ( not a[49]  or not a[2] ) 
 and  ( not a[33]  or not a[2] ) 
 and  ( not a[50]  or  a[2] ) 
 and  ( not a[51]  or  a[2] ) 
 and  ( not a[52]  or  a[2] ) 
 and  ( not a[53]  or  a[2] ) 
 and  ( not a[5]  or not a[0] ) 
 and  ( not a[5]  or not a[1] ) 
 and  ( not a[40]  or not a[5] ) 
 and  ( not a[5]  or not a[2] ) 
 and  ( not a[5]  or not a[3] ) 
 and  ( not a[5]  or not a[4] ) 
 and  ( not a[6]  or not a[5] ) 
 and  ( not a[13]  or not a[5] ) 
 and  ( not a[14]  or not a[5] ) 
 and  ( not a[15]  or not a[5] ) 
 and  ( not a[16]  or not a[5] ) 
 and  ( not a[17]  or not a[5] ) 
 and  ( not a[41]  or not a[5] ) 
 and  ( not a[18]  or not a[5] ) 
 and  ( not a[19]  or not a[5] ) 
 and  ( not a[20]  or not a[5] ) 
 and  ( not a[21]  or not a[5] ) 
 and  ( not a[56]  or not a[5] ) 
 and  ( not a[57]  or not a[5] ) 
 and  ( not a[58]  or not a[5] ) 
 and  ( not a[22]  or not a[5] ) 
 and  ( not a[27]  or not a[5] ) 
 and  ( not a[28]  or not a[5] ) 
 and  ( not a[29]  or not a[5] ) 
 and  ( not a[48]  or not a[5] ) 
 and  ( not a[30]  or not a[5] ) 
 and  ( not a[31]  or not a[5] ) 
 and  ( not a[59]  or not a[5] ) 
 and  ( not a[32]  or not a[5] ) 
 and  ( not a[33]  or not a[5] ) 
 and  ( not a[60]  or  a[5] ) 
 and  ( not a[62]  or not a[61] ) 
 and  ( not a[63]  or not a[61] ) 
 and  ( not a[64]  or not a[61] ) 
 and  ( not a[65]  or not a[61] ) 
 and  ( not a[66]  or not a[61] ) 
 and  ( not a[67]  or not a[61] ) 
 and  ( not a[68]  or not a[61] ) 
 and  ( not a[69]  or not a[61] ) 
 and  ( not a[70]  or not a[61] ) 
 and  ( not a[71]  or not a[61] ) 
 and  ( not a[72]  or not a[61] ) 
 and  ( not a[73]  or not a[61] ) 
 and  ( not a[74]  or not a[61] ) 
 and  ( not a[75]  or not a[61] ) 
 and  ( not a[76]  or  a[5] ) 
 and  ( not a[64]  or not a[61] ) 
 and  ( not a[77]  or not a[64] ) 
 and  ( not a[78]  or not a[64] ) 
 and  ( not a[79]  or not a[64] ) 
 and  ( not a[80]  or not a[64] ) 
 and  ( not a[81]  or not a[64] ) 
 and  ( not a[77]  or not a[62] ) 
 and  ( not a[77]  or not a[63] ) 
 and  ( not a[77]  or not a[64] ) 
 and  ( not a[77]  or not a[65] ) 
 and  ( not a[77]  or not a[66] ) 
 and  ( not a[77]  or not a[67] ) 
 and  ( not a[77]  or not a[68] ) 
 and  ( not a[77]  or not a[69] ) 
 and  ( not a[77]  or not a[70] ) 
 and  ( not a[77]  or not a[71] ) 
 and  ( not a[77]  or not a[72] ) 
 and  ( not a[77]  or not a[73] ) 
 and  ( not a[77]  or not a[74] ) 
 and  ( not a[77]  or not a[75] ) 
 and  ( not a[82]  or  a[5] ) 
 and  ( not a[67]  or not a[61] ) 
 and  ( not a[77]  or not a[67] ) 
 and  ( not a[78]  or not a[67] ) 
 and  ( not a[79]  or not a[67] ) 
 and  ( not a[80]  or not a[67] ) 
 and  ( not a[81]  or not a[67] ) 
 and  ( not a[83]  or  a[5] ) 
 and  ( not a[85]  or not a[84] ) 
 and  ( not a[86]  or not a[84] ) 
 and  ( not a[87]  or not a[84] ) 
 and  ( not a[88]  or not a[84] ) 
 and  ( not a[89]  or not a[84] ) 
 and  ( not a[90]  or not a[84] ) 
 and  ( not a[91]  or not a[84] ) 
 and  ( not a[94]  or not a[93] ) 
 and  ( not a[95]  or  a[96] ) 
 and  ( not a[95]  or not a[74]  or  a[97] ) 
 and  ( not a[95]  or not a[75] ) 
 and  ( not a[98]  or not a[95] ) 
 and  ( not a[99]  or not a[95] ) 
 and  ( not a[100]  or  a[74]  or  a[101]  or  a[102]  or  a[103] ) 
 and  ( not a[104]  or not a[100] ) 
 and  ( not a[105]  or  a[106] ) 
 and  ( not a[107]  or not a[105] ) 
 and  ( not a[108]  or not a[105] ) 
 and  ( not a[110]  or not a[109] ) 
 and  ( not a[113]  or  a[114] ) 
 and  ( not a[113]  or not a[98] ) 
 and  ( not a[115]  or not a[113] ) 
 and  ( not a[116]  or not a[113] ) 
 and  ( not a[117]  or not a[113] ) 
 and  ( not a[118]  or not a[113] ) 
 and  ( not a[119]  or not a[113] ) 
 and  ( not a[120]  or not a[113] ) 
 and  ( not a[121]  or not a[113] ) 
 and  ( not a[122]  or not a[113] ) 
 and  ( not a[123]  or not a[113] ) 
 and  ( not a[124]  or not a[113] ) 
 and  ( not a[113]  or not a[74] ) 
 and  ( not a[113]  or not a[75] ) 
 and  ( not a[125]  or not a[113] ) 
 and  ( not a[126]  or not a[113] ) 
 and  ( not a[127]  or not a[113] ) 
 and  ( not a[128]  or not a[113] ) 
 and  ( not a[129]  or not a[113] ) 
 and  ( not a[130]  or not a[113] ) 
 and  ( not a[132]  or not a[131] ) 
 and  ( not a[133]  or not a[131] ) 
 and  ( not a[134]  or not a[131] ) 
 and  ( not a[135]  or not a[131] ) 
 and  ( not a[136]  or not a[131] ) 
 and  ( not a[137]  or not a[131] ) 
 and  ( not a[138]  or not a[131] ) 
 and  ( not a[141]  or not a[101] ) 
 and  ( not a[120]  or  a[114] ) 
 and  ( not a[120]  or not a[115] ) 
 and  ( not a[120]  or not a[116] ) 
 and  ( not a[120]  or not a[117] ) 
 and  ( not a[120]  or not a[113] ) 
 and  ( not a[120]  or not a[119] ) 
 and  ( not a[121]  or not a[120] ) 
 and  ( not a[122]  or not a[120] ) 
 and  ( not a[123]  or not a[120] ) 
 and  ( not a[124]  or not a[120] ) 
 and  ( not a[142]  or not a[120] ) 
 and  ( not a[120]  or not a[74] ) 
 and  ( not a[120]  or not a[75] ) 
 and  ( not a[120]  or not a[98] ) 
 and  ( not a[125]  or not a[120] ) 
 and  ( not a[126]  or not a[120] ) 
 and  ( not a[127]  or not a[120] ) 
 and  ( not a[128]  or not a[120] ) 
 and  ( not a[129]  or not a[120] ) 
 and  ( not a[130]  or not a[120] ) 
 and  ( not a[121]  or  a[114] ) 
 and  ( not a[121]  or not a[115] ) 
 and  ( not a[121]  or not a[116] ) 
 and  ( not a[121]  or not a[117] ) 
 and  ( not a[121]  or not a[113] ) 
 and  ( not a[121]  or not a[118] ) 
 and  ( not a[121]  or not a[119] ) 
 and  ( not a[121]  or not a[120] ) 
 and  ( not a[143]  or not a[121] ) 
 and  ( not a[122]  or not a[121] ) 
 and  ( not a[123]  or not a[121] ) 
 and  ( not a[124]  or not a[121] ) 
 and  ( not a[121]  or not a[74] ) 
 and  ( not a[121]  or not a[75] ) 
 and  ( not a[121]  or not a[98] ) 
 and  ( not a[125]  or not a[121] ) 
 and  ( not a[126]  or not a[121] ) 
 and  ( not a[127]  or not a[121] ) 
 and  ( not a[128]  or not a[121] ) 
 and  ( not a[129]  or not a[121] ) 
 and  ( not a[130]  or not a[121] ) 
 and  ( not a[144]  or not a[74] ) 
 and  ( not a[144]  or not a[75] ) 
 and  ( not a[122]  or  a[145]  or  a[146]  or  a[147] ) 
 and  ( not a[122]  or  a[148]  or  a[149] ) 
 and  ( not a[150]  or not a[122] ) 
 and  ( not a[122]  or not a[115] ) 
 and  ( not a[122]  or not a[116] ) 
 and  ( not a[122]  or not a[117] ) 
 and  ( not a[122]  or not a[113] ) 
 and  ( not a[151]  or not a[122] ) 
 and  ( not a[122]  or not a[118] ) 
 and  ( not a[122]  or not a[119] ) 
 and  ( not a[122]  or not a[120] ) 
 and  ( not a[122]  or not a[121] ) 
 and  ( not a[123]  or not a[122] ) 
 and  ( not a[124]  or not a[122] ) 
 and  ( not a[122]  or not a[114] ) 
 and  ( not a[122]  or not a[74] ) 
 and  ( not a[122]  or not a[75] ) 
 and  ( not a[152]  or not a[122] ) 
 and  ( not a[122]  or not a[98] ) 
 and  ( not a[153]  or not a[122] ) 
 and  ( not a[154]  or not a[122] ) 
 and  ( not a[126]  or not a[122] ) 
 and  ( not a[127]  or not a[122] ) 
 and  ( not a[128]  or not a[122] ) 
 and  ( not a[129]  or not a[122] ) 
 and  ( not a[130]  or not a[122] ) 
 and  ( not a[155]  or not a[122] ) 
 and  ( not a[156]  or not a[122] ) 
 and  ( not a[157]  or not a[122] ) 
 and  ( not a[123]  or not a[114] ) 
 and  ( not a[123]  or not a[115] ) 
 and  ( not a[123]  or not a[116] ) 
 and  ( not a[123]  or not a[117] ) 
 and  ( not a[123]  or not a[113] ) 
 and  ( not a[123]  or not a[118] ) 
 and  ( not a[123]  or not a[119] ) 
 and  ( not a[123]  or not a[120] ) 
 and  ( not a[123]  or not a[121] ) 
 and  ( not a[123]  or not a[122] ) 
 and  ( not a[124]  or not a[123] ) 
 and  ( not a[123]  or not a[74] ) 
 and  ( not a[123]  or not a[75] ) 
 and  ( not a[123]  or not a[98] ) 
 and  ( not a[125]  or not a[123] ) 
 and  ( not a[126]  or not a[123] ) 
 and  ( not a[127]  or not a[123] ) 
 and  ( not a[128]  or not a[123] ) 
 and  ( not a[129]  or not a[123] ) 
 and  ( not a[130]  or not a[123] ) 
 and  ( not a[155]  or not a[123] ) 
 and  ( not a[156]  or not a[123] ) 
 and  ( not a[157]  or not a[123] ) 
 and  ( not a[159]  or  a[74]  or  a[75] ) 
 and  ( not a[149]  or not a[114] ) 
 and  ( not a[149]  or not a[148] ) 
 and  ( not a[160]  or not a[149] ) 
 and  ( not a[161]  or not a[149] ) 
 and  ( not a[149]  or not a[142] ) 
 and  ( not a[162]  or not a[149] ) 
 and  ( not a[163]  or not a[149] ) 
 and  ( not a[164]  or not a[149] ) 
 and  ( not a[165]  or not a[149] ) 
 and  ( not a[166]  or not a[149] ) 
 and  ( not a[167]  or not a[149] ) 
 and  ( not a[168]  or not a[149] ) 
 and  ( not a[169]  or not a[149] ) 
 and  ( not a[170]  or not a[149] ) 
 and  ( not a[162]  or not a[114] ) 
 and  ( not a[162]  or not a[148] ) 
 and  ( not a[162]  or not a[160] ) 
 and  ( not a[162]  or not a[161] ) 
 and  ( not a[162]  or not a[142] ) 
 and  ( not a[162]  or not a[149] ) 
 and  ( not a[164]  or not a[162] ) 
 and  ( not a[166]  or not a[162] ) 
 and  ( not a[167]  or not a[162] ) 
 and  ( not a[168]  or not a[162] ) 
 and  ( not a[169]  or not a[162] ) 
 and  ( not a[170]  or not a[162] ) 
 and  ( not a[171]  or not a[162] ) 
 and  ( not a[172]  or not a[162] ) 
 and  ( not a[123]  or not a[114] ) 
 and  ( not a[149]  or not a[114] ) 
 and  ( not a[162]  or not a[114] ) 
 and  ( not a[173]  or not a[114] ) 
 and  ( not a[174]  or not a[114] ) 
 and  ( not a[150]  or not a[114] ) 
 and  ( not a[175]  or not a[114] ) 
 and  ( not a[176]  or not a[114] ) 
 and  ( not a[177]  or not a[114] ) 
 and  ( not a[122]  or not a[114] ) 
 and  ( not a[124]  or not a[114] ) 
 and  ( not a[161]  or not a[114] ) 
 and  ( not a[142]  or not a[114] ) 
 and  ( not a[178]  or not a[114] ) 
 and  ( not a[179]  or not a[114] ) 
 and  ( not a[114]  or not a[74] ) 
 and  ( not a[114]  or not a[75] ) 
 and  ( not a[130]  or not a[114] ) 
 and  ( not a[180]  or  a[5] ) 
 and  ( not a[180]  or  a[96] ) 
 and  ( not a[181]  or not a[180] ) 
 and  ( not a[182]  or  a[5] ) 
 and  ( not a[182]  or  a[180] ) 
 and  ( not a[182]  or not a[110] ) 
 and  ( not a[184]  or not a[183] ) 
 and  ( not a[183]  or not a[91] ) 
 and  ( not a[185]  or not a[184] ) 
 and  ( not a[185]  or not a[91] ) 
 and  ( not a[187]  or not a[149] ) 
 and  ( not a[188]  or not a[187] ) 
 and  ( not a[189]  or not a[187] ) 
 and  ( not a[190]  or not a[187] ) 
 and  ( not a[191]  or not a[187] ) 
 and  ( not a[188]  or not a[149] ) 
 and  ( not a[188]  or not a[187] ) 
 and  ( not a[189]  or not a[188] ) 
 and  ( not a[190]  or not a[188] ) 
 and  ( not a[191]  or not a[188] ) 
 and  ( not a[189]  or not a[149] ) 
 and  ( not a[189]  or not a[187] ) 
 and  ( not a[189]  or not a[188] ) 
 and  ( not a[190]  or not a[189] ) 
 and  ( not a[191]  or not a[189] ) 
 and  ( not a[190]  or not a[149] ) 
 and  ( not a[190]  or not a[187] ) 
 and  ( not a[190]  or not a[188] ) 
 and  ( not a[190]  or not a[189] ) 
 and  ( not a[191]  or not a[190] ) 
 and  ( not a[193]  or not a[192] ) 
 and  ( not a[194]  or not a[192] ) 
 and  ( not a[195]  or not a[192] ) 
 and  ( not a[196]  or not a[192] ) 
 and  ( not a[193]  or not a[192] ) 
 and  ( not a[202]  or not a[201] ) 
 and  ( not a[203]  or not a[201] ) 
 and  ( not a[204]  or not a[201] ) 
 and  ( not a[205]  or not a[201] ) 
 and  ( not a[206]  or not a[201] ) 
 and  ( not a[207]  or not a[201] ) 
 and  ( not a[184]  or not a[163] ) 
 and  ( not a[173]  or not a[163] ) 
 and  ( not a[174]  or not a[163] ) 
 and  ( not a[214]  or not a[163] ) 
 and  ( not a[163]  or not a[161] ) 
 and  ( not a[163]  or not a[149] ) 
 and  ( not a[163]  or not a[74] ) 
 and  ( not a[163]  or not a[75] ) 
 and  ( not a[163]  or not a[98] ) 
 and  ( not a[215]  or not a[163] ) 
 and  ( not a[207]  or not a[163] ) 
 and  ( not a[216]  or not a[163] ) 
 and  ( not a[217]  or not a[163] ) 
 and  ( not a[163]  or not a[133] ) 
 and  ( not a[218]  or not a[163] ) 
 and  ( not a[219]  or not a[163] ) 
 and  ( not a[163]  or not a[155] ) 
 and  ( not a[163]  or not a[156] ) 
 and  ( not a[163]  or not a[157] ) 
 and  ( not a[220]  or not a[163] ) 
 and  ( not a[222]  or not a[221] ) 
 and  ( not a[221]  or not a[75] ) 
 and  ( not a[223]  or not a[221] ) 
 and  ( not a[221]  or not a[98] ) 
 and  ( not a[224]  or not a[221] ) 
 and  ( not a[225]  or not a[221] ) 
 and  ( not a[226]  or not a[221] ) 
 and  ( not a[228]  or not a[227] ) 
 and  ( not a[86]  or not a[84] ) 
 and  ( not a[86]  or not a[85] ) 
 and  ( not a[87]  or not a[86] ) 
 and  ( not a[230]  or not a[86] ) 
 and  ( not a[231]  or not a[74] ) 
 and  ( not a[347]  or not a[74] ) 
 and  ( not a[346]  or not a[74] ) 
 and  ( not a[345]  or not a[74] ) 
 and  ( not a[344]  or not a[74] ) 
 and  ( not a[343]  or not a[74] ) 
 and  ( not a[342]  or not a[74] ) 
 and  ( not a[341]  or not a[74] ) 
 and  ( not a[340]  or not a[74] ) 
 and  ( not a[339]  or not a[74] ) 
 and  ( not a[338]  or not a[74] ) 
 and  ( not a[337]  or not a[74] ) 
 and  ( not a[336]  or not a[74] ) 
 and  ( not a[335]  or not a[74] ) 
 and  ( not a[334]  or not a[74] ) 
 and  ( not a[333]  or not a[74] ) 
 and  ( not a[332]  or not a[74] ) 
 and  ( not a[331]  or not a[74] ) 
 and  ( not a[330]  or not a[74] ) 
 and  ( not a[329]  or not a[74] ) 
 and  ( not a[328]  or not a[74] ) 
 and  ( not a[327]  or not a[74] ) 
 and  ( not a[326]  or not a[74] ) 
 and  ( not a[325]  or not a[74] ) 
 and  ( not a[324]  or not a[74] ) 
 and  ( not a[323]  or not a[74] ) 
 and  ( not a[322]  or not a[74] ) 
 and  ( not a[321]  or not a[74] ) 
 and  ( not a[320]  or not a[74] ) 
 and  ( not a[319]  or not a[74] ) 
 and  ( not a[318]  or not a[74] ) 
 and  ( not a[317]  or not a[74] ) 
 and  ( not a[316]  or not a[74] ) 
 and  ( not a[315]  or not a[74] ) 
 and  ( not a[314]  or not a[74] ) 
 and  ( not a[313]  or not a[74] ) 
 and  ( not a[312]  or not a[74] ) 
 and  ( not a[311]  or not a[74] ) 
 and  ( not a[310]  or not a[74] ) 
 and  ( not a[309]  or not a[74] ) 
 and  ( not a[308]  or not a[74] ) 
 and  ( not a[307]  or not a[74] ) 
 and  ( not a[306]  or not a[74] ) 
 and  ( not a[305]  or not a[74] ) 
 and  ( not a[304]  or not a[74] ) 
 and  ( not a[303]  or not a[74] ) 
 and  ( not a[302]  or not a[74] ) 
 and  ( not a[301]  or not a[74] ) 
 and  ( not a[300]  or not a[74] ) 
 and  ( not a[299]  or not a[74] ) 
 and  ( not a[298]  or not a[74] ) 
 and  ( not a[297]  or not a[74] ) 
 and  ( not a[296]  or not a[74] ) 
 and  ( not a[295]  or not a[74] ) 
 and  ( not a[294]  or not a[74] ) 
 and  ( not a[293]  or not a[74] ) 
 and  ( not a[292]  or not a[74] ) 
 and  ( not a[291]  or not a[74] ) 
 and  ( not a[290]  or not a[74] ) 
 and  ( not a[289]  or not a[74] ) 
 and  ( not a[288]  or not a[74] ) 
 and  ( not a[287]  or not a[74] ) 
 and  ( not a[286]  or not a[74] ) 
 and  ( not a[285]  or not a[74] ) 
 and  ( not a[284]  or not a[74] ) 
 and  ( not a[283]  or not a[74] ) 
 and  ( not a[282]  or not a[74] ) 
 and  ( not a[281]  or not a[74] ) 
 and  ( not a[280]  or not a[74] ) 
 and  ( not a[279]  or not a[74] ) 
 and  ( not a[278]  or not a[74] ) 
 and  ( not a[277]  or not a[74] ) 
 and  ( not a[276]  or not a[74] ) 
 and  ( not a[275]  or not a[74] ) 
 and  ( not a[274]  or not a[74] ) 
 and  ( not a[273]  or not a[74] ) 
 and  ( not a[272]  or not a[74] ) 
 and  ( not a[271]  or not a[74] ) 
 and  ( not a[270]  or not a[74] ) 
 and  ( not a[269]  or not a[74] ) 
 and  ( not a[268]  or not a[74] ) 
 and  ( not a[267]  or not a[74] ) 
 and  ( not a[266]  or not a[74] ) 
 and  ( not a[265]  or not a[74] ) 
 and  ( not a[264]  or not a[74] ) 
 and  ( not a[263]  or not a[74] ) 
 and  ( not a[262]  or not a[74] ) 
 and  ( not a[261]  or not a[74] ) 
 and  ( not a[260]  or not a[74] ) 
 and  ( not a[259]  or not a[74] ) 
 and  ( not a[258]  or not a[74] ) 
 and  ( not a[257]  or not a[74] ) 
 and  ( not a[256]  or not a[74] ) 
 and  ( not a[255]  or not a[74] ) 
 and  ( not a[254]  or not a[74] ) 
 and  ( not a[253]  or not a[74] ) 
 and  ( not a[252]  or not a[74] ) 
 and  ( not a[251]  or not a[74] ) 
 and  ( not a[250]  or not a[74] ) 
 and  ( not a[249]  or not a[74] ) 
 and  ( not a[248]  or not a[74] ) 
 and  ( not a[247]  or not a[74] ) 
 and  ( not a[246]  or not a[74] ) 
 and  ( not a[245]  or not a[74] ) 
 and  ( not a[244]  or not a[74] ) 
 and  ( not a[243]  or not a[74] ) 
 and  ( not a[242]  or not a[74] ) 
 and  ( not a[241]  or not a[74] ) 
 and  ( not a[240]  or not a[74] ) 
 and  ( not a[239]  or not a[74] ) 
 and  ( not a[238]  or not a[74] ) 
 and  ( not a[74]  or  a[237] ) 
 and  ( not a[74]  or  a[236] ) 
 and  ( not a[74]  or  a[235] ) 
 and  ( not a[74]  or  a[234] ) 
 and  ( not a[74]  or  a[233] ) 
 and  ( not a[74]  or  a[232] ) 
 and  ( not a[225]  or not a[74] ) 
 and  ( not a[224]  or not a[74] ) 
 and  ( not a[223]  or not a[74] ) 
 and  ( not a[74]  or  a[221] ) 
 and  ( not a[219]  or not a[74] ) 
 and  ( not a[218]  or not a[74] ) 
 and  ( not a[216]  or not a[74] ) 
 and  ( not a[74]  or  a[213] ) 
 and  ( not a[207]  or not a[74] ) 
 and  ( not a[74]  or  a[201] ) 
 and  ( not a[196]  or not a[74] ) 
 and  ( not a[184]  or not a[74] ) 
 and  ( not a[179]  or not a[74] ) 
 and  ( not a[172]  or not a[74] ) 
 and  ( not a[170]  or not a[74] ) 
 and  ( not a[169]  or not a[74] ) 
 and  ( not a[168]  or not a[74] ) 
 and  ( not a[167]  or not a[74] ) 
 and  ( not a[166]  or not a[74] ) 
 and  ( not a[165]  or not a[74] ) 
 and  ( not a[164]  or not a[74] ) 
 and  ( not a[163]  or not a[74] ) 
 and  ( not a[161]  or not a[74] ) 
 and  ( not a[157]  or not a[74] ) 
 and  ( not a[156]  or not a[74] ) 
 and  ( not a[155]  or not a[74] ) 
 and  ( not a[150]  or not a[74] ) 
 and  ( not a[74]  or  a[149] ) 
 and  ( not a[147]  or not a[74] ) 
 and  ( not a[144]  or not a[74] ) 
 and  ( not a[142]  or not a[74] ) 
 and  ( not a[141]  or not a[74] ) 
 and  ( not a[74]  or  a[140] ) 
 and  ( not a[74]  or  a[131] ) 
 and  ( not a[129]  or not a[74] ) 
 and  ( not a[128]  or not a[74] ) 
 and  ( not a[127]  or not a[74] ) 
 and  ( not a[126]  or not a[74] ) 
 and  ( not a[125]  or not a[74] ) 
 and  ( not a[123]  or not a[74] ) 
 and  ( not a[121]  or not a[74] ) 
 and  ( not a[120]  or not a[74] ) 
 and  ( not a[118]  or not a[74] ) 
 and  ( not a[116]  or not a[74] ) 
 and  ( not a[114]  or not a[74] ) 
 and  ( not a[113]  or not a[74] ) 
 and  ( not a[74]  or  a[111] ) 
 and  ( not a[74]  or  a[106] ) 
 and  ( not a[74]  or  a[105] ) 
 and  ( not a[74]  or  a[100] ) 
 and  ( not a[98]  or not a[74] ) 
 and  ( not a[74]  or  a[96] ) 
 and  ( not a[95]  or not a[74] ) 
 and  ( not a[74]  or  a[93] ) 
 and  ( not a[87]  or not a[74] ) 
 and  ( not a[81]  or not a[74] ) 
 and  ( not a[80]  or not a[74] ) 
 and  ( not a[79]  or not a[74] ) 
 and  ( not a[78]  or not a[74] ) 
 and  ( not a[77]  or not a[74] ) 
 and  ( not a[75]  or not a[74] ) 
 and  ( not a[74]  or not a[61] ) 
 and  ( not a[74]  or  a[5] ) 
 and  ( not a[367]  or not a[75] ) 
 and  ( not a[366]  or not a[75] ) 
 and  ( not a[365]  or not a[75] ) 
 and  ( not a[364]  or not a[75] ) 
 and  ( not a[363]  or not a[75] ) 
 and  ( not a[362]  or not a[75] ) 
 and  ( not a[361]  or not a[75] ) 
 and  ( not a[360]  or not a[75] ) 
 and  ( not a[359]  or not a[75] ) 
 and  ( not a[358]  or not a[75] ) 
 and  ( not a[357]  or not a[75] ) 
 and  ( not a[356]  or not a[75] ) 
 and  ( not a[355]  or not a[75] ) 
 and  ( not a[354]  or not a[75] ) 
 and  ( not a[353]  or not a[75] ) 
 and  ( not a[352]  or not a[75] ) 
 and  ( not a[351]  or not a[75] ) 
 and  ( not a[350]  or not a[75] ) 
 and  ( not a[349]  or not a[75] ) 
 and  ( not a[75]  or  a[348] ) 
 and  ( not a[347]  or not a[75] ) 
 and  ( not a[346]  or not a[75] ) 
 and  ( not a[345]  or not a[75] ) 
 and  ( not a[344]  or not a[75] ) 
 and  ( not a[343]  or not a[75] ) 
 and  ( not a[342]  or not a[75] ) 
 and  ( not a[341]  or not a[75] ) 
 and  ( not a[340]  or not a[75] ) 
 and  ( not a[339]  or not a[75] ) 
 and  ( not a[338]  or not a[75] ) 
 and  ( not a[337]  or not a[75] ) 
 and  ( not a[336]  or not a[75] ) 
 and  ( not a[335]  or not a[75] ) 
 and  ( not a[334]  or not a[75] ) 
 and  ( not a[333]  or not a[75] ) 
 and  ( not a[332]  or not a[75] ) 
 and  ( not a[331]  or not a[75] ) 
 and  ( not a[330]  or not a[75] ) 
 and  ( not a[329]  or not a[75] ) 
 and  ( not a[328]  or not a[75] ) 
 and  ( not a[327]  or not a[75] ) 
 and  ( not a[326]  or not a[75] ) 
 and  ( not a[325]  or not a[75] ) 
 and  ( not a[324]  or not a[75] ) 
 and  ( not a[323]  or not a[75] ) 
 and  ( not a[322]  or not a[75] ) 
 and  ( not a[321]  or not a[75] ) 
 and  ( not a[320]  or not a[75] ) 
 and  ( not a[319]  or not a[75] ) 
 and  ( not a[317]  or not a[75] ) 
 and  ( not a[316]  or not a[75] ) 
 and  ( not a[315]  or not a[75] ) 
 and  ( not a[314]  or not a[75] ) 
 and  ( not a[313]  or not a[75] ) 
 and  ( not a[310]  or not a[75] ) 
 and  ( not a[309]  or not a[75] ) 
 and  ( not a[307]  or not a[75] ) 
 and  ( not a[306]  or not a[75] ) 
 and  ( not a[305]  or not a[75] ) 
 and  ( not a[304]  or not a[75] ) 
 and  ( not a[303]  or not a[75] ) 
 and  ( not a[301]  or not a[75] ) 
 and  ( not a[300]  or not a[75] ) 
 and  ( not a[299]  or not a[75] ) 
 and  ( not a[298]  or not a[75] ) 
 and  ( not a[297]  or not a[75] ) 
 and  ( not a[296]  or not a[75] ) 
 and  ( not a[295]  or not a[75] ) 
 and  ( not a[294]  or not a[75] ) 
 and  ( not a[293]  or not a[75] ) 
 and  ( not a[292]  or not a[75] ) 
 and  ( not a[291]  or not a[75] ) 
 and  ( not a[289]  or not a[75] ) 
 and  ( not a[288]  or not a[75] ) 
 and  ( not a[286]  or not a[75] ) 
 and  ( not a[284]  or not a[75] ) 
 and  ( not a[283]  or not a[75] ) 
 and  ( not a[282]  or not a[75] ) 
 and  ( not a[281]  or not a[75] ) 
 and  ( not a[280]  or not a[75] ) 
 and  ( not a[278]  or not a[75] ) 
 and  ( not a[277]  or not a[75] ) 
 and  ( not a[273]  or not a[75] ) 
 and  ( not a[271]  or not a[75] ) 
 and  ( not a[269]  or not a[75] ) 
 and  ( not a[268]  or not a[75] ) 
 and  ( not a[267]  or not a[75] ) 
 and  ( not a[266]  or not a[75] ) 
 and  ( not a[75]  or  a[264] ) 
 and  ( not a[263]  or not a[75] ) 
 and  ( not a[260]  or not a[75] ) 
 and  ( not a[259]  or not a[75] ) 
 and  ( not a[258]  or not a[75] ) 
 and  ( not a[257]  or not a[75] ) 
 and  ( not a[256]  or not a[75] ) 
 and  ( not a[254]  or not a[75] ) 
 and  ( not a[253]  or not a[75] ) 
 and  ( not a[251]  or not a[75] ) 
 and  ( not a[250]  or not a[75] ) 
 and  ( not a[249]  or not a[75] ) 
 and  ( not a[248]  or not a[75] ) 
 and  ( not a[247]  or not a[75] ) 
 and  ( not a[246]  or not a[75] ) 
 and  ( not a[245]  or not a[75] ) 
 and  ( not a[244]  or not a[75] ) 
 and  ( not a[243]  or not a[75] ) 
 and  ( not a[242]  or not a[75] ) 
 and  ( not a[241]  or not a[75] ) 
 and  ( not a[240]  or not a[75] ) 
 and  ( not a[239]  or not a[75] ) 
 and  ( not a[238]  or not a[75] ) 
 and  ( not a[235]  or not a[75] ) 
 and  ( not a[234]  or not a[75] ) 
 and  ( not a[75]  or  a[233] ) 
 and  ( not a[75]  or  a[228] ) 
 and  ( not a[225]  or not a[75] ) 
 and  ( not a[224]  or not a[75] ) 
 and  ( not a[223]  or not a[75] ) 
 and  ( not a[222]  or not a[75] ) 
 and  ( not a[221]  or not a[75] ) 
 and  ( not a[219]  or not a[75] ) 
 and  ( not a[216]  or not a[75] ) 
 and  ( not a[75]  or  a[213] ) 
 and  ( not a[207]  or not a[75] ) 
 and  ( not a[203]  or not a[75] ) 
 and  ( not a[196]  or not a[75] ) 
 and  ( not a[195]  or not a[75] ) 
 and  ( not a[194]  or not a[75] ) 
 and  ( not a[75]  or  a[180] ) 
 and  ( not a[179]  or not a[75] ) 
 and  ( not a[172]  or not a[75] ) 
 and  ( not a[171]  or not a[75] ) 
 and  ( not a[170]  or not a[75] ) 
 and  ( not a[169]  or not a[75] ) 
 and  ( not a[168]  or not a[75] ) 
 and  ( not a[167]  or not a[75] ) 
 and  ( not a[166]  or not a[75] ) 
 and  ( not a[165]  or not a[75] ) 
 and  ( not a[164]  or not a[75] ) 
 and  ( not a[163]  or not a[75] ) 
 and  ( not a[157]  or not a[75] ) 
 and  ( not a[156]  or not a[75] ) 
 and  ( not a[155]  or not a[75] ) 
 and  ( not a[150]  or not a[75] ) 
 and  ( not a[75]  or  a[149] ) 
 and  ( not a[148]  or not a[75] ) 
 and  ( not a[147]  or not a[75] ) 
 and  ( not a[144]  or not a[75] ) 
 and  ( not a[142]  or not a[75] ) 
 and  ( not a[141]  or not a[75] ) 
 and  ( not a[138]  or not a[75] ) 
 and  ( not a[137]  or not a[75] ) 
 and  ( not a[136]  or not a[75] ) 
 and  ( not a[129]  or not a[75] ) 
 and  ( not a[128]  or not a[75] ) 
 and  ( not a[127]  or not a[75] ) 
 and  ( not a[126]  or not a[75] ) 
 and  ( not a[125]  or not a[75] ) 
 and  ( not a[123]  or not a[75] ) 
 and  ( not a[122]  or not a[75] ) 
 and  ( not a[121]  or not a[75] ) 
 and  ( not a[120]  or not a[75] ) 
 and  ( not a[118]  or not a[75] ) 
 and  ( not a[116]  or not a[75] ) 
 and  ( not a[114]  or not a[75] ) 
 and  ( not a[113]  or not a[75] ) 
 and  ( not a[75]  or  a[111] ) 
 and  ( not a[100]  or not a[75] ) 
 and  ( not a[98]  or not a[75] ) 
 and  ( not a[75]  or  a[96] ) 
 and  ( not a[95]  or not a[75] ) 
 and  ( not a[87]  or not a[75] ) 
 and  ( not a[81]  or not a[75] ) 
 and  ( not a[80]  or not a[75] ) 
 and  ( not a[79]  or not a[75] ) 
 and  ( not a[78]  or not a[75] ) 
 and  ( not a[77]  or not a[75] ) 
 and  ( not a[75]  or not a[74] ) 
 and  ( not a[75]  or not a[61] ) 
 and  ( not a[348]  or not a[147] ) 
 and  ( not a[369]  or not a[368] ) 
 and  ( not a[370]  or not a[368] ) 
 and  ( not a[368]  or not a[196] ) 
 and  ( not a[371]  or not a[368] ) 
 and  ( not a[260]  or not a[74] ) 
 and  ( not a[260]  or not a[75] ) 
 and  ( not a[260]  or not a[98] ) 
 and  ( not a[260]  or not a[196] ) 
 and  ( not a[372]  or not a[232] ) 
 and  ( not a[374]  or not a[233] ) 
 and  ( not a[375]  or not a[233] ) 
 and  ( not a[233]  or not a[215] ) 
 and  ( not a[376]  or not a[233] ) 
 and  ( not a[233]  or not a[207] ) 
 and  ( not a[378]  or not a[377] ) 
 and  ( not a[377]  or not a[165] ) 
 and  ( not a[379]  or not a[377] ) 
 and  ( not a[380]  or not a[377] ) 
 and  ( not a[381]  or not a[377] ) 
 and  ( not a[382]  or not a[377] ) 
 and  ( not a[383]  or not a[377] ) 
 and  ( not a[377]  or not a[279] ) 
 and  ( not a[384]  or not a[377] ) 
 and  ( not a[385]  or not a[377] ) 
 and  ( not a[356]  or  a[386] ) 
 and  ( not a[356]  or not a[75] ) 
 and  ( not a[356]  or not a[264] ) 
 and  ( not a[356]  or not a[265] ) 
 and  ( not a[387]  or not a[356] ) 
 and  ( not a[356]  or not a[98] ) 
 and  ( not a[388]  or not a[356] ) 
 and  ( not a[389]  or not a[356] ) 
 and  ( not a[390]  or not a[356] ) 
 and  ( not a[391]  or not a[356] ) 
 and  ( not a[392]  or not a[356] ) 
 and  ( not a[393]  or not a[356] ) 
 and  ( not a[394]  or not a[356] ) 
 and  ( not a[395]  or not a[356] ) 
 and  ( not a[396]  or not a[356] ) 
 and  ( not a[356]  or not a[91] ) 
 and  ( not a[397]  or not a[356] ) 
 and  ( not a[264]  or not a[74] ) 
 and  ( not a[356]  or not a[264] ) 
 and  ( not a[265]  or not a[264] ) 
 and  ( not a[387]  or not a[264] ) 
 and  ( not a[265]  or  a[386] ) 
 and  ( not a[356]  or not a[265] ) 
 and  ( not a[265]  or not a[264] ) 
 and  ( not a[387]  or not a[265] ) 
 and  ( not a[265]  or not a[222] ) 
 and  ( not a[265]  or not a[74] ) 
 and  ( not a[293]  or not a[265] ) 
 and  ( not a[265]  or not a[101] ) 
 and  ( not a[398]  or not a[265] ) 
 and  ( not a[399]  or not a[265] ) 
 and  ( not a[400]  or not a[265] ) 
 and  ( not a[401]  or not a[265] ) 
 and  ( not a[402]  or not a[265] ) 
 and  ( not a[403]  or not a[265] ) 
 and  ( not a[404]  or not a[265] ) 
 and  ( not a[405]  or not a[265] ) 
 and  ( not a[406]  or not a[265] ) 
 and  ( not a[407]  or not a[265] ) 
 and  ( not a[408]  or not a[265] ) 
 and  ( not a[409]  or not a[265] ) 
 and  ( not a[410]  or not a[265] ) 
 and  ( not a[411]  or not a[265] ) 
 and  ( not a[412]  or not a[265] ) 
 and  ( not a[413]  or not a[265] ) 
 and  ( not a[414]  or not a[265] ) 
 and  ( not a[234]  or not a[75] ) 
 and  ( not a[234]  or not a[98] ) 
 and  ( not a[415]  or not a[234] ) 
 and  ( not a[235]  or not a[75] ) 
 and  ( not a[235]  or not a[98]  or  a[225] ) 
 and  ( not a[266]  or not a[235] ) 
 and  ( not a[415]  or not a[235] ) 
 and  ( not a[269]  or not a[74] ) 
 and  ( not a[269]  or not a[75] ) 
 and  ( not a[269]  or not a[98] ) 
 and  ( not a[416]  or not a[269] ) 
 and  ( not a[417]  or not a[269] ) 
 and  ( not a[288]  or not a[269] ) 
 and  ( not a[418]  or not a[269] ) 
 and  ( not a[269]  or not a[88] ) 
 and  ( not a[269]  or not a[89] ) 
 and  ( not a[269]  or not a[90] ) 
 and  ( not a[289]  or not a[269] ) 
 and  ( not a[419]  or not a[269] ) 
 and  ( not a[290]  or not a[269] ) 
 and  ( not a[361]  or not a[269] ) 
 and  ( not a[420]  or not a[269] ) 
 and  ( not a[421]  or not a[269] ) 
 and  ( not a[422]  or not a[269] ) 
 and  ( not a[423]  or not a[269] ) 
 and  ( not a[272]  or not a[74] ) 
 and  ( not a[272]  or not a[267] ) 
 and  ( not a[424]  or not a[272] ) 
 and  ( not a[272]  or not a[268] ) 
 and  ( not a[425]  or not a[272] ) 
 and  ( not a[426]  or not a[272] ) 
 and  ( not a[427]  or not a[272] ) 
 and  ( not a[428]  or not a[272] ) 
 and  ( not a[429]  or not a[272] ) 
 and  ( not a[272]  or not a[271] ) 
 and  ( not a[430]  or not a[272] ) 
 and  ( not a[431]  or not a[272] ) 
 and  ( not a[357]  or not a[272] ) 
 and  ( not a[432]  or not a[272] ) 
 and  ( not a[433]  or not a[272] ) 
 and  ( not a[434]  or not a[272] ) 
 and  ( not a[435]  or not a[272] ) 
 and  ( not a[436]  or not a[272] ) 
 and  ( not a[437]  or not a[272] ) 
 and  ( not a[438]  or not a[272] ) 
 and  ( not a[275]  or not a[272] ) 
 and  ( not a[439]  or not a[272] ) 
 and  ( not a[360]  or not a[272] ) 
 and  ( not a[288]  or not a[272] ) 
 and  ( not a[272]  or not a[89] ) 
 and  ( not a[272]  or not a[90] ) 
 and  ( not a[290]  or not a[272] ) 
 and  ( not a[361]  or not a[272] ) 
 and  ( not a[421]  or not a[272] ) 
 and  ( not a[440]  or not a[272] ) 
 and  ( not a[422]  or not a[272] ) 
 and  ( not a[441]  or not a[272] ) 
 and  ( not a[277]  or not a[74] ) 
 and  ( not a[277]  or not a[75] ) 
 and  ( not a[442]  or not a[277] ) 
 and  ( not a[277]  or not a[98] ) 
 and  ( not a[443]  or not a[133] ) 
 and  ( not a[444]  or not a[237] ) 
 and  ( not a[228]  or  a[75] ) 
 and  ( not a[228]  or not a[227] ) 
 and  ( not a[228]  or not a[74] ) 
 and  ( not a[359]  or not a[228] ) 
 and  ( not a[304]  or not a[228] ) 
 and  ( not a[359]  or  a[98]  or  a[391]  or  a[394]  or  a[446]  or  a[447]  or  a[448]  or  a[449]  or  a[450]  or  a[451] ) 
 and  ( not a[359]  or not a[74] ) 
 and  ( not a[359]  or not a[228] ) 
 and  ( not a[359]  or not a[304] ) 
 and  ( not a[452]  or  a[187]  or  a[188]  or  a[189]  or  a[190] ) 
 and  ( not a[452]  or not a[164] ) 
 and  ( not a[453]  or not a[452] ) 
 and  ( not a[454]  or not a[452] ) 
 and  ( not a[452]  or not a[263] ) 
 and  ( not a[455]  or not a[452] ) 
 and  ( not a[452]  or not a[155] ) 
 and  ( not a[452]  or not a[156] ) 
 and  ( not a[452]  or not a[157] ) 
 and  ( not a[452]  or not a[196] ) 
 and  ( not a[153]  or  a[113]  or  a[120]  or  a[121]  or  a[123] ) 
 and  ( not a[153]  or not a[115] ) 
 and  ( not a[153]  or not a[116] ) 
 and  ( not a[153]  or not a[122] ) 
 and  ( not a[153]  or not a[124] ) 
 and  ( not a[153]  or not a[142] ) 
 and  ( not a[456]  or not a[153] ) 
 and  ( not a[457]  or not a[153] ) 
 and  ( not a[458]  or not a[153] ) 
 and  ( not a[459]  or not a[153] ) 
 and  ( not a[460]  or not a[153] ) 
 and  ( not a[153]  or not a[125] ) 
 and  ( not a[154]  or  a[101] ) 
 and  ( not a[154]  or not a[115] ) 
 and  ( not a[154]  or not a[116] ) 
 and  ( not a[154]  or not a[117] ) 
 and  ( not a[154]  or not a[119] ) 
 and  ( not a[154]  or not a[122] ) 
 and  ( not a[154]  or not a[124] ) 
 and  ( not a[154]  or not a[74] ) 
 and  ( not a[154]  or not a[75] ) 
 and  ( not a[154]  or not a[98] ) 
 and  ( not a[154]  or not a[125] ) 
 and  ( not a[461]  or not a[98] ) 
 and  ( not a[462]  or  a[187]  or  a[188]  or  a[189]  or  a[190] ) 
 and  ( not a[462]  or not a[161] ) 
 and  ( not a[462]  or not a[155] ) 
 and  ( not a[462]  or not a[156] ) 
 and  ( not a[462]  or not a[157] ) 
 and  ( not a[444]  or not a[237] ) 
 and  ( not a[464]  or not a[237] ) 
 and  ( not a[465]  or not a[237] ) 
 and  ( not a[466]  or not a[237] ) 
 and  ( not a[467]  or not a[237] ) 
 and  ( not a[468]  or not a[237] ) 
 and  ( not a[469]  or not a[237] ) 
 and  ( not a[470]  or  a[149] ) 
 and  ( not a[471]  or not a[470] ) 
 and  ( not a[472]  or  a[470] ) 
 and  ( not a[472]  or not a[471] ) 
 and  ( not a[110]  or  a[181] ) 
 and  ( not a[110]  or not a[109] ) 
 and  ( not a[182]  or not a[110] ) 
 and  ( not a[181]  or  a[96] ) 
 and  ( not a[181]  or not a[180] ) 
 and  ( not a[473]  or not a[98] ) 
 and  ( not a[474]  or  a[232] ) 
 and  ( not a[474]  or not a[196] ) 
 and  ( not a[307]  or not a[74] ) 
 and  ( not a[307]  or not a[75] ) 
 and  ( not a[307]  or not a[98] ) 
 and  ( not a[308]  or not a[74] ) 
 and  ( not a[476]  or  a[224]  or  a[225]  or  a[299]  or  a[390]  or  a[399]  or  a[447] ) 
 and  ( not a[480]  or not a[479] ) 
 and  ( not a[480]  or not a[479] ) 
 and  ( not a[480]  or not a[202] ) 
 and  ( not a[480]  or not a[201] ) 
 and  ( not a[481]  or not a[480] ) 
 and  ( not a[484]  or not a[483] ) 
 and  ( not a[485]  or not a[483] ) 
 and  ( not a[486]  or not a[483] ) 
 and  ( not a[487]  or not a[483] ) 
 and  ( not a[488]  or not a[483] ) 
 and  ( not a[489]  or not a[483] ) 
 and  ( not a[490]  or not a[483] ) 
 and  ( not a[491]  or not a[483] ) 
 and  ( not a[492]  or not a[483] ) 
 and  ( not a[493]  or not a[483] ) 
 and  ( not a[494]  or not a[483] ) 
 and  ( not a[495]  or not a[483] ) 
 and  ( not a[496]  or not a[483] ) 
 and  ( not a[497]  or not a[483] ) 
 and  ( not a[498]  or not a[483] ) 
 and  ( not a[499]  or not a[483] ) 
 and  ( not a[500]  or not a[483] ) 
 and  ( not a[501]  or not a[483] ) 
 and  ( not a[502]  or not a[483] ) 
 and  ( not a[503]  or not a[483] ) 
 and  ( not a[504]  or not a[483] ) 
 and  ( not a[505]  or not a[483] ) 
 and  ( not a[506]  or not a[483] ) 
 and  ( not a[507]  or not a[483] ) 
 and  ( not a[34]  or  a[0]  or  a[1]  or  a[2]  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] ) 
 and  ( not a[35]  or  a[0]  or  a[1]  or  a[2]  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] ) 
 and  ( not a[36]  or  a[0]  or  a[1]  or  a[2]  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] ) 
 and  ( not a[38]  or  a[0]  or  a[1]  or  a[2]  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] ) 
 and  ( not a[50]  or  a[0]  or  a[1]  or  a[2]  or  a[5]  or  a[15]  or  a[16]  or  a[18]  or  a[22]  or  a[27]  or  a[28]  or  a[30]  or  a[31]  or  a[33]  or  a[40]  or  a[41]  or  a[42]  or  a[43]  or  a[44]  or  a[45]  or  a[46]  or  a[47]  or  a[48]  or  a[49] ) 
 and  ( not a[51]  or  a[0]  or  a[1]  or  a[2]  or  a[5]  or  a[15]  or  a[16]  or  a[18]  or  a[22]  or  a[27]  or  a[28]  or  a[30]  or  a[31]  or  a[33]  or  a[40]  or  a[41]  or  a[42]  or  a[43]  or  a[44]  or  a[45]  or  a[46]  or  a[47]  or  a[48]  or  a[49] ) 
 and  ( not a[52]  or  a[0]  or  a[1]  or  a[2]  or  a[5]  or  a[15]  or  a[16]  or  a[18]  or  a[22]  or  a[27]  or  a[28]  or  a[30]  or  a[31]  or  a[33]  or  a[40]  or  a[41]  or  a[42]  or  a[43]  or  a[44]  or  a[45]  or  a[46]  or  a[47]  or  a[48]  or  a[49] ) 
 and  ( not a[53]  or  a[0]  or  a[1]  or  a[2]  or  a[5]  or  a[15]  or  a[16]  or  a[18]  or  a[22]  or  a[27]  or  a[28]  or  a[30]  or  a[31]  or  a[33]  or  a[40]  or  a[41]  or  a[42]  or  a[43]  or  a[44]  or  a[45]  or  a[46]  or  a[47]  or  a[48]  or  a[49] ) 
 and  ( not a[60]  or  a[0]  or  a[1]  or  a[2]  or  a[3]  or  a[4]  or  a[5]  or  a[6]  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[27]  or  a[28]  or  a[29]  or  a[30]  or  a[31]  or  a[32]  or  a[33]  or  a[40]  or  a[41]  or  a[48]  or  a[56]  or  a[57]  or  a[58]  or  a[59] ) 
 and  ( not a[76]  or  a[0]  or  a[1]  or  a[2]  or  a[3]  or  a[4]  or  a[5]  or  a[6]  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[27]  or  a[28]  or  a[29]  or  a[30]  or  a[31]  or  a[32]  or  a[33]  or  a[40]  or  a[41]  or  a[48]  or  a[56]  or  a[57]  or  a[58]  or  a[59] ) 
 and  ( not a[82]  or  a[0]  or  a[1]  or  a[2]  or  a[3]  or  a[4]  or  a[5]  or  a[6]  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[27]  or  a[28]  or  a[29]  or  a[30]  or  a[31]  or  a[32]  or  a[33]  or  a[40]  or  a[41]  or  a[48]  or  a[56]  or  a[57]  or  a[58]  or  a[59] ) 
 and  ( not a[83]  or  a[0]  or  a[1]  or  a[2]  or  a[3]  or  a[4]  or  a[5]  or  a[6]  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[27]  or  a[28]  or  a[29]  or  a[30]  or  a[31]  or  a[32]  or  a[33]  or  a[40]  or  a[41]  or  a[48]  or  a[56]  or  a[57]  or  a[58]  or  a[59] ) 
 and  ( not a[74]  or  a[0]  or  a[1]  or  a[2]  or  a[3]  or  a[4]  or  a[5]  or  a[6]  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[27]  or  a[28]  or  a[29]  or  a[30]  or  a[31]  or  a[32]  or  a[33]  or  a[40]  or  a[41]  or  a[48]  or  a[56]  or  a[57]  or  a[58]  or  a[59] ) 
 and  ( not a[101]  or  a[61]  or  a[64]  or  a[77]  or  a[78]  or  a[79]  or  a[80]  or  a[81] ) 
 and  ( not a[74]  or  a[100]  or  a[104] ) 
 and  ( not a[106]  or not a[74]  or  a[105]  or  a[107]  or  a[108] ) 
 and  ( not a[74]  or  a[111] ) 
 and  ( not a[75]  or  a[111] ) 
 and  ( not a[105]  or  a[106] ) 
 and  ( not a[74]  or  a[106] ) 
 and  ( not a[74]  or  a[131]  or  a[132]  or  a[133]  or  a[134]  or  a[135]  or  a[136]  or  a[137]  or  a[138] ) 
 and  ( not a[75]  or  a[131]  or  a[132]  or  a[133]  or  a[134]  or  a[135]  or  a[136]  or  a[137]  or  a[138] ) 
 and  ( not a[74]  or  a[140] ) 
 and  ( not a[74]  or  a[114]  or  a[142]  or  a[148]  or  a[149]  or  a[160]  or  a[161]  or  a[162]  or  a[163]  or  a[164]  or  a[165]  or  a[166]  or  a[167]  or  a[168]  or  a[169]  or  a[170] ) 
 and  ( not a[75]  or  a[114]  or  a[142]  or  a[148]  or  a[149]  or  a[160]  or  a[161]  or  a[162]  or  a[163]  or  a[164]  or  a[165]  or  a[166]  or  a[167]  or  a[168]  or  a[169]  or  a[170] ) 
 and  ( not a[113]  or  a[74]  or  a[75]  or  a[114]  or  a[122]  or  a[123]  or  a[124]  or  a[130]  or  a[142]  or  a[149]  or  a[150]  or  a[161]  or  a[162]  or  a[173]  or  a[174]  or  a[175]  or  a[176]  or  a[177]  or  a[178]  or  a[179] ) 
 and  ( not a[120]  or  a[74]  or  a[75]  or  a[114]  or  a[122]  or  a[123]  or  a[124]  or  a[130]  or  a[142]  or  a[149]  or  a[150]  or  a[161]  or  a[162]  or  a[173]  or  a[174]  or  a[175]  or  a[176]  or  a[177]  or  a[178]  or  a[179] ) 
 and  ( not a[121]  or  a[74]  or  a[75]  or  a[114]  or  a[122]  or  a[123]  or  a[124]  or  a[130]  or  a[142]  or  a[149]  or  a[150]  or  a[161]  or  a[162]  or  a[173]  or  a[174]  or  a[175]  or  a[176]  or  a[177]  or  a[178]  or  a[179] ) 
 and  ( not a[182]  or not a[96]  or not a[5]  or  a[180]  or  a[181] ) 
 and  ( not a[96]  or not a[75]  or not a[5]  or  a[180]  or  a[181] ) 
 and  ( not a[74]  or  a[201]  or  a[202]  or  a[203]  or  a[204]  or  a[205]  or  a[206]  or  a[207] ) 
 and  (  a[211] ) 
 and  ( not a[74]  or  a[213] ) 
 and  ( not a[75]  or  a[213] ) 
 and  ( not a[74]  or  a[75]  or  a[98]  or  a[221]  or  a[222]  or  a[223]  or  a[224]  or  a[225]  or  a[226] ) 
 and  ( not a[75]  or  a[147]  or  a[348] ) 
 and  ( not a[474]  or  a[232]  or  a[372] ) 
 and  ( not a[74]  or  a[232]  or  a[372] ) 
 and  ( not a[74]  or  a[207]  or  a[215]  or  a[233]  or  a[374]  or  a[375]  or  a[376] ) 
 and  ( not a[75]  or  a[207]  or  a[215]  or  a[233]  or  a[374]  or  a[375]  or  a[376] ) 
 and  ( not a[356]  or  a[386] ) 
 and  ( not a[265]  or  a[386] ) 
 and  ( not a[75]  or  a[74]  or  a[264]  or  a[265]  or  a[356]  or  a[387] ) 
 and  ( not a[74]  or  a[75]  or  a[98]  or  a[234]  or  a[415] ) 
 and  ( not a[74]  or  a[75]  or  a[98]  or  a[235]  or  a[266]  or  a[415] ) 
 and  ( not a[225]  or not a[74]  or  a[75]  or  a[235]  or  a[266]  or  a[415] ) 
 and  ( not a[180]  or  a[96] ) 
 and  ( not a[74]  or  a[96] ) 
 and  ( not a[75]  or  a[96] ) 
 and  ( not a[233]  or  a[96] ) 
 and  ( not a[181]  or  a[96] ) 
 and  ( not a[74]  or  a[236] ) 
 and  ( not a[74]  or  a[237]  or  a[444]  or  a[464]  or  a[465]  or  a[466]  or  a[467]  or  a[468]  or  a[469] ) 
 and  (  a[74]  or  a[75]  or  a[98]  or  a[307] ) 
 and  ( not a[399]  or  a[476] ) 
 and  (  a[201]  or  a[202]  or  a[479]  or  a[480]  or  a[481] ) 
 and  (  a[37] ) 
 ) ;