variable
  public a : array 1761 of boolean ; 

rule
( 
 ( 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[73] ) 
 and  ( not a[74] ) 
 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[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[75] ) 
 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[82] ) 
 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[83] ) 
 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[84] ) 
 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[86] ) 
 and  ( not a[87] ) 
 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[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[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[1326] ) 
 and  ( not a[340] ) 
 and  ( not a[341] ) 
 and  ( not a[342] ) 
 and  ( not a[343] ) 
 and  ( not a[344] ) 
 and  ( not a[345] ) 
 and  ( not a[346] ) 
 and  ( not a[347] ) 
 and  ( not a[348] ) 
 and  ( not a[349] ) 
 and  ( not a[350] ) 
 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[358] ) 
 and  ( not a[359] ) 
 and  ( not a[360] ) 
 and  ( not a[368] ) 
 and  ( not a[369] ) 
 and  ( not a[370] ) 
 and  ( not a[371] ) 
 and  ( not a[361] ) 
 and  ( not a[363] ) 
 and  ( not a[365] ) 
 and  ( not a[367] ) 
 and  ( not a[1327] ) 
 and  ( not a[1328] ) 
 and  ( not a[1329] ) 
 and  ( not a[1330] ) 
 and  ( not a[382] ) 
 and  ( not a[373] ) 
 and  ( not a[383] ) 
 and  ( not a[1331] ) 
 and  ( not a[374] ) 
 and  ( not a[375] ) 
 and  ( not a[376] ) 
 and  ( not a[386] ) 
 and  ( not a[1332] ) 
 and  ( not a[1333] ) 
 and  ( not a[381] ) 
 and  ( not a[385] ) 
 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[390] ) 
 and  ( not a[395] ) 
 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[1364] ) 
 and  ( not a[1365] ) 
 and  ( not a[1366] ) 
 and  ( not a[1367] ) 
 and  ( not a[446] ) 
 and  ( not a[1368] ) 
 and  ( not a[1369] ) 
 and  ( not a[1370] ) 
 and  ( not a[407] ) 
 and  ( not a[408] ) 
 and  ( not a[1371] ) 
 and  ( not a[410] ) 
 and  ( not a[409] ) 
 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[447] ) 
 and  ( not a[1394] ) 
 and  ( not a[434] ) 
 and  ( not a[435] ) 
 and  ( not a[1395] ) 
 and  ( not a[405] ) 
 and  ( not a[413] ) 
 and  ( not a[414] ) 
 and  ( not a[415] ) 
 and  ( not a[416] ) 
 and  ( not a[417] ) 
 and  ( not a[418] ) 
 and  ( not a[442] ) 
 and  ( not a[443] ) 
 and  ( not a[444] ) 
 and  ( not a[445] ) 
 and  ( not a[422] ) 
 and  ( not a[423] ) 
 and  ( not a[425] ) 
 and  ( not a[426] ) 
 and  ( not a[427] ) 
 and  ( not a[428] ) 
 and  ( not a[429] ) 
 and  ( not a[430] ) 
 and  ( not a[432] ) 
 and  ( not a[433] ) 
 and  ( not a[436] ) 
 and  ( not a[437] ) 
 and  ( not a[438] ) 
 and  ( not a[439] ) 
 and  ( not a[440] ) 
 and  ( not a[441] ) 
 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[463] ) 
 and  ( not a[464] ) 
 and  ( not a[465] ) 
 and  ( not a[466] ) 
 and  ( not a[467] ) 
 and  ( not a[468] ) 
 and  ( not a[1396] ) 
 and  ( not a[469] ) 
 and  ( not a[470] ) 
 and  ( not a[471] ) 
 and  ( not a[1397] ) 
 and  ( not a[1398] ) 
 and  ( not a[1399] ) 
 and  ( not a[472] ) 
 and  ( not a[1400] ) 
 and  ( not a[1401] ) 
 and  ( not a[1402] ) 
 and  ( not a[1403] ) 
 and  ( not a[473] ) 
 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[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[498] ) 
 and  ( not a[493] ) 
 and  ( not a[499] ) 
 and  ( not a[1444] ) 
 and  ( not a[494] ) 
 and  ( not a[495] ) 
 and  ( not a[487] ) 
 and  ( not a[488] ) 
 and  ( not a[496] ) 
 and  ( not a[497] ) 
 and  ( not a[489] ) 
 and  ( not a[490] ) 
 and  ( not a[491] ) 
 and  ( not a[492] ) 
 and  ( not a[1445] ) 
 and  ( not a[486] ) 
 and  ( not a[503] ) 
 and  ( not a[504] ) 
 and  ( not a[524] ) 
 and  ( not a[514] ) 
 and  ( not a[515] ) 
 and  ( not a[527] ) 
 and  ( not a[1446] ) 
 and  ( not a[528] ) 
 and  ( not a[505] ) 
 and  ( not a[1447] ) 
 and  ( not a[512] ) 
 and  ( not a[507] ) 
 and  ( not a[1448] ) 
 and  ( not a[506] ) 
 and  ( not a[513] ) 
 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[574] ) 
 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[575] ) 
 and  ( not a[1456] ) 
 and  ( not a[1457] ) 
 and  ( not a[483] ) 
 and  ( not a[572] ) 
 and  ( not a[1458] ) 
 and  ( not a[1459] ) 
 and  ( not a[1460] ) 
 and  ( not a[586] ) 
 and  ( not a[587] ) 
 and  ( not a[1461] ) 
 and  ( not a[1462] ) 
 and  ( not a[1463] ) 
 and  ( not a[1464] ) 
 and  ( not a[1465] ) 
 and  ( not a[1466] ) 
 and  ( not a[1467] ) 
 and  ( not a[1468] ) 
 and  ( not a[1469] ) 
 and  ( not a[1470] ) 
 and  ( not a[1471] ) 
 and  ( not a[1472] ) 
 and  ( not a[1473] ) 
 and  ( not a[1474] ) 
 and  ( not a[1475] ) 
 and  ( not a[1476] ) 
 and  ( not a[1477] ) 
 and  ( not a[1478] ) 
 and  ( not a[1479] ) 
 and  ( not a[1480] ) 
 and  ( not a[1481] ) 
 and  ( not a[1482] ) 
 and  ( not a[1483] ) 
 and  ( not a[1484] ) 
 and  ( not a[1485] ) 
 and  ( not a[1486] ) 
 and  ( not a[1487] ) 
 and  ( not a[1488] ) 
 and  ( not a[1489] ) 
 and  ( not a[1490] ) 
 and  ( not a[1491] ) 
 and  ( not a[1492] ) 
 and  ( not a[1493] ) 
 and  ( not a[1494] ) 
 and  ( not a[1495] ) 
 and  ( not a[1496] ) 
 and  ( not a[1497] ) 
 and  ( not a[1498] ) 
 and  ( not a[1499] ) 
 and  ( not a[1500] ) 
 and  ( not a[1501] ) 
 and  ( not a[1502] ) 
 and  ( not a[1503] ) 
 and  ( not a[1504] ) 
 and  ( not a[1505] ) 
 and  ( not a[1506] ) 
 and  ( not a[592] ) 
 and  ( not a[593] ) 
 and  ( not a[594] ) 
 and  ( not a[595] ) 
 and  ( not a[1507] ) 
 and  ( not a[596] ) 
 and  ( not a[1508] ) 
 and  ( not a[500] ) 
 and  ( not a[1509] ) 
 and  ( not a[1510] ) 
 and  ( not a[1511] ) 
 and  ( not a[1512] ) 
 and  ( not a[1513] ) 
 and  ( not a[1514] ) 
 and  ( not a[1515] ) 
 and  ( not a[1516] ) 
 and  ( not a[1517] ) 
 and  ( not a[1518] ) 
 and  ( not a[1519] ) 
 and  ( not a[1520] ) 
 and  ( not a[1521] ) 
 and  ( not a[1522] ) 
 and  ( not a[1523] ) 
 and  ( not a[1524] ) 
 and  ( not a[1525] ) 
 and  ( not a[1526] ) 
 and  ( not a[1527] ) 
 and  ( not a[1528] ) 
 and  ( not a[1529] ) 
 and  ( not a[601] ) 
 and  ( not a[1530] ) 
 and  ( not a[1531] ) 
 and  ( not a[1532] ) 
 and  ( not a[1533] ) 
 and  ( not a[1534] ) 
 and  ( not a[1535] ) 
 and  ( not a[1536] ) 
 and  ( not a[602] ) 
 and  ( not a[603] ) 
 and  ( not a[590] ) 
 and  ( not a[591] ) 
 and  ( not a[604] ) 
 and  ( not a[607] ) 
 and  ( not a[608] ) 
 and  ( not a[609] ) 
 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[598] ) 
 and  ( not a[1537] ) 
 and  ( not a[617] ) 
 and  ( not a[606] ) 
 and  ( not a[1538] ) 
 and  ( not a[1539] ) 
 and  ( not a[1540] ) 
 and  ( not a[501] ) 
 and  ( not a[502] ) 
 and  ( not a[1541] ) 
 and  ( not a[1542] ) 
 and  ( not a[1543] ) 
 and  ( not a[1544] ) 
 and  ( not a[1545] ) 
 and  ( not a[1546] ) 
 and  ( not a[508] ) 
 and  ( not a[1547] ) 
 and  ( not a[1548] ) 
 and  ( not a[1549] ) 
 and  ( not a[1550] ) 
 and  ( not a[1551] ) 
 and  ( not a[1552] ) 
 and  ( not a[1553] ) 
 and  ( not a[1554] ) 
 and  ( not a[1555] ) 
 and  ( not a[1556] ) 
 and  ( not a[1557] ) 
 and  ( not a[1558] ) 
 and  ( not a[1559] ) 
 and  ( not a[1560] ) 
 and  ( not a[1561] ) 
 and  ( not a[1562] ) 
 and  ( not a[1563] ) 
 and  ( not a[1564] ) 
 and  ( not a[1565] ) 
 and  ( not a[1566] ) 
 and  ( not a[1567] ) 
 and  ( not a[1568] ) 
 and  ( not a[1569] ) 
 and  ( not a[623] ) 
 and  ( not a[625] ) 
 and  ( not a[626] ) 
 and  ( not a[627] ) 
 and  ( not a[628] ) 
 and  ( not a[1570] ) 
 and  ( not a[1571] ) 
 and  ( not a[629] ) 
 and  ( not a[630] ) 
 and  ( not a[631] ) 
 and  ( not a[632] ) 
 and  ( not a[1572] ) 
 and  ( not a[377] ) 
 and  ( not a[378] ) 
 and  ( not a[1573] ) 
 and  ( not a[1574] ) 
 and  ( not a[379] ) 
 and  ( not a[380] ) 
 and  ( not a[624] ) 
 and  ( not a[1575] ) 
 and  ( not a[656] ) 
 and  ( not a[657] ) 
 and  ( not a[658] ) 
 and  ( not a[659] ) 
 and  ( not a[660] ) 
 and  ( not a[661] ) 
 and  ( not a[636] ) 
 and  ( not a[651] ) 
 and  ( not a[652] ) 
 and  ( not a[653] ) 
 and  ( not a[648] ) 
 and  ( not a[649] ) 
 and  ( not a[650] ) 
 and  ( not a[635] ) 
 and  ( not a[637] ) 
 and  ( not a[638] ) 
 and  ( not a[654] ) 
 and  ( not a[655] ) 
 and  ( not a[662] ) 
 and  ( not a[1576] ) 
 and  ( not a[1577] ) 
 and  ( not a[675] ) 
 and  ( not a[668] ) 
 and  ( not a[676] ) 
 and  ( not a[518] ) 
 and  ( not a[519] ) 
 and  ( not a[1578] ) 
 and  ( not a[520] ) 
 and  ( not a[521] ) 
 and  ( not a[1579] ) 
 and  ( not a[677] ) 
 and  ( not a[1580] ) 
 and  ( not a[1581] ) 
 and  ( not a[1582] ) 
 and  ( not a[693] ) 
 and  ( not a[525] ) 
 and  ( not a[522] ) 
 and  ( not a[523] ) 
 and  ( not a[1583] ) 
 and  ( not a[664] ) 
 and  ( not a[669] ) 
 and  ( not a[665] ) 
 and  ( not a[670] ) 
 and  ( not a[666] ) 
 and  ( not a[671] ) 
 and  ( not a[667] ) 
 and  ( not a[672] ) 
 and  ( not a[1584] ) 
 and  ( not a[1585] ) 
 and  ( not a[674] ) 
 and  ( not a[1586] ) 
 and  ( not a[1587] ) 
 and  ( not a[1588] ) 
 and  ( not a[1589] ) 
 and  ( not a[1590] ) 
 and  ( not a[1591] ) 
 and  ( not a[1592] ) 
 and  ( not a[1593] ) 
 and  ( not a[1594] ) 
 and  ( not a[689] ) 
 and  ( not a[690] ) 
 and  ( not a[691] ) 
 and  ( not a[1595] ) 
 and  ( not a[1596] ) 
 and  ( not a[1597] ) 
 and  ( not a[1598] ) 
 and  ( not a[1599] ) 
 and  ( not a[1600] ) 
 and  ( not a[1601] ) 
 and  ( not a[1602] ) 
 and  ( not a[1603] ) 
 and  ( not a[1604] ) 
 and  ( not a[1605] ) 
 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[1606] ) 
 and  ( not a[1607] ) 
 and  ( not a[701] ) 
 and  ( not a[1608] ) 
 and  ( not a[1609] ) 
 and  ( not a[1610] ) 
 and  ( not a[1611] ) 
 and  ( not a[1612] ) 
 and  ( not a[1613] ) 
 and  ( not a[683] ) 
 and  ( not a[684] ) 
 and  ( not a[685] ) 
 and  ( not a[702] ) 
 and  ( not a[686] ) 
 and  ( not a[687] ) 
 and  ( not a[1614] ) 
 and  ( not a[1615] ) 
 and  ( not a[1616] ) 
 and  ( not a[1617] ) 
 and  ( not a[1618] ) 
 and  ( not a[1619] ) 
 and  ( not a[703] ) 
 and  ( not a[1620] ) 
 and  ( not a[1621] ) 
 and  ( not a[1622] ) 
 and  ( not a[1623] ) 
 and  ( not a[1624] ) 
 and  ( not a[1625] ) 
 and  ( not a[707] ) 
 and  ( not a[1626] ) 
 and  ( not a[1627] ) 
 and  ( not a[1628] ) 
 and  ( not a[1629] ) 
 and  ( not a[1630] ) 
 and  ( not a[1631] ) 
 and  ( not a[1632] ) 
 and  ( not a[1633] ) 
 and  ( not a[1634] ) 
 and  ( not a[1635] ) 
 and  ( not a[1636] ) 
 and  ( not a[1637] ) 
 and  ( not a[1638] ) 
 and  ( not a[1639] ) 
 and  ( not a[709] ) 
 and  ( not a[1640] ) 
 and  ( not a[1641] ) 
 and  ( not a[1642] ) 
 and  ( not a[1643] ) 
 and  ( not a[1644] ) 
 and  ( not a[1645] ) 
 and  ( not a[1646] ) 
 and  ( not a[1647] ) 
 and  ( not a[1648] ) 
 and  ( not a[1649] ) 
 and  ( not a[1650] ) 
 and  ( not a[1651] ) 
 and  ( not a[1652] ) 
 and  ( not a[1653] ) 
 and  ( not a[1654] ) 
 and  ( not a[1655] ) 
 and  ( not a[1656] ) 
 and  ( not a[1657] ) 
 and  ( not a[1658] ) 
 and  ( not a[1659] ) 
 and  ( not a[1660] ) 
 and  ( not a[1661] ) 
 and  ( not a[1662] ) 
 and  ( not a[633] ) 
 and  ( not a[634] ) 
 and  ( not a[1663] ) 
 and  ( not a[1664] ) 
 and  ( not a[1665] ) 
 and  ( not a[1666] ) 
 and  ( not a[1667] ) 
 and  ( not a[1668] ) 
 and  ( not a[1669] ) 
 and  ( not a[1670] ) 
 and  ( not a[1671] ) 
 and  ( not a[1672] ) 
 and  ( not a[1673] ) 
 and  ( not a[1674] ) 
 and  ( not a[1675] ) 
 and  ( not a[1676] ) 
 and  ( not a[1677] ) 
 and  ( not a[1678] ) 
 and  ( not a[1679] ) 
 and  ( not a[1680] ) 
 and  ( not a[1681] ) 
 and  ( not a[1682] ) 
 and  ( not a[1683] ) 
 and  ( not a[1684] ) 
 and  ( not a[1685] ) 
 and  ( not a[1686] ) 
 and  ( not a[1687] ) 
 and  ( not a[1688] ) 
 and  ( not a[1689] ) 
 and  ( not a[722] ) 
 and  ( not a[1690] ) 
 and  ( not a[1691] ) 
 and  ( not a[1692] ) 
 and  ( not a[1693] ) 
 and  ( not a[1694] ) 
 and  ( not a[1695] ) 
 and  ( not a[1696] ) 
 and  ( not a[1697] ) 
 and  ( not a[1698] ) 
 and  ( not a[1699] ) 
 and  ( not a[1700] ) 
 and  ( not a[1701] ) 
 and  ( not a[1702] ) 
 and  ( not a[1703] ) 
 and  ( not a[1704] ) 
 and  ( not a[1705] ) 
 and  ( not a[1706] ) 
 and  ( not a[1707] ) 
 and  ( not a[1708] ) 
 and  ( not a[1709] ) 
 and  ( not a[1710] ) 
 and  ( not a[712] ) 
 and  ( not a[713] ) 
 and  ( not a[1711] ) 
 and  ( not a[1712] ) 
 and  ( not a[1713] ) 
 and  ( not a[1714] ) 
 and  ( not a[1715] ) 
 and  ( not a[1716] ) 
 and  ( not a[1717] ) 
 and  ( not a[1718] ) 
 and  ( not a[1719] ) 
 and  ( not a[1720] ) 
 and  ( not a[1721] ) 
 and  ( not a[1722] ) 
 and  ( not a[1723] ) 
 and  ( not a[1724] ) 
 and  ( not a[1725] ) 
 and  ( not a[734] ) 
 and  ( not a[735] ) 
 and  ( not a[733] ) 
 and  ( not a[682] ) 
 and  ( not a[1726] ) 
 and  ( not a[1727] ) 
 and  ( not a[1728] ) 
 and  ( not a[1729] ) 
 and  ( not a[1730] ) 
 and  ( not a[1731] ) 
 and  ( not a[1732] ) 
 and  ( not a[1733] ) 
 and  ( not a[1734] ) 
 and  ( not a[1735] ) 
 and  ( not a[1736] ) 
 and  ( not a[1737] ) 
 and  ( not a[1738] ) 
 and  ( not a[1739] ) 
 and  ( not a[1740] ) 
 and  ( not a[1741] ) 
 and  ( not a[1742] ) 
 and  ( not a[1743] ) 
 and  ( not a[1744] ) 
 and  ( not a[1745] ) 
 and  ( not a[1746] ) 
 and  ( not a[1747] ) 
 and  ( not a[1748] ) 
 and  ( not a[1749] ) 
 and  ( not a[1750] ) 
 and  ( not a[1751] ) 
 and  ( not a[1752] ) 
 and  ( not a[1753] ) 
 and  ( not a[1754] ) 
 and  ( not a[1755] ) 
 and  ( not a[1756] ) 
 and  ( not a[1757] ) 
 and  ( not a[1758] ) 
 and  ( not a[1759] ) 
 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[87]  or not a[72] ) 
 and  ( not a[88]  or not a[72] ) 
 and  ( not a[89]  or not a[72] ) 
 and  ( not a[90]  or not a[72] ) 
 and  ( not a[91]  or not a[72] ) 
 and  ( not a[76]  or not a[73] ) 
 and  ( not a[76]  or not a[74] ) 
 and  ( not a[76]  or not a[75] ) 
 and  ( not a[76]  or not a[72] ) 
 and  ( not a[77]  or not a[76] ) 
 and  ( not a[78]  or not a[76] ) 
 and  ( not a[79]  or not a[76] ) 
 and  ( not a[80]  or not a[76] ) 
 and  ( not a[81]  or not a[76] ) 
 and  ( not a[82]  or not a[76] ) 
 and  ( not a[83]  or not a[76] ) 
 and  ( not a[84]  or not a[76] ) 
 and  ( not a[85]  or not a[76] ) 
 and  ( not a[86]  or not a[76] ) 
 and  ( not a[87]  or not a[76] ) 
 and  ( not a[88]  or not a[76] ) 
 and  ( not a[89]  or not a[76] ) 
 and  ( not a[90]  or not a[76] ) 
 and  ( not a[91]  or not a[76] ) 
 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[77]  or not a[72] ) 
 and  ( not a[77]  or not a[76] ) 
 and  ( not a[78]  or not a[77] ) 
 and  ( not a[79]  or not a[77] ) 
 and  ( not a[80]  or not a[77] ) 
 and  ( not a[81]  or not a[77] ) 
 and  ( not a[82]  or not a[77] ) 
 and  ( not a[83]  or not a[77] ) 
 and  ( not a[84]  or not a[77] ) 
 and  ( not a[85]  or not a[77] ) 
 and  ( not a[86]  or not a[77] ) 
 and  ( not a[87]  or not a[77] ) 
 and  ( not a[88]  or not a[77] ) 
 and  ( not a[89]  or not a[77] ) 
 and  ( not a[90]  or not a[77] ) 
 and  ( not a[91]  or not a[77] ) 
 and  ( not a[95]  or  a[96]  or  a[97]  or  a[99]  or  a[100]  or  a[101] ) 
 and  ( not a[95]  or  a[98]  or  a[99]  or  a[100]  or  a[101] ) 
 and  ( not a[103]  or  a[96]  or  a[97]  or  a[99]  or  a[100]  or  a[101] ) 
 and  ( not a[103]  or  a[98]  or  a[99]  or  a[100]  or  a[101] ) 
 and  ( not a[78]  or not a[73] ) 
 and  ( not a[78]  or not a[74] ) 
 and  ( not a[78]  or not a[75] ) 
 and  ( not a[78]  or not a[72] ) 
 and  ( not a[78]  or not a[76] ) 
 and  ( not a[78]  or not a[77] ) 
 and  ( not a[79]  or not a[78] ) 
 and  ( not a[80]  or not a[78] ) 
 and  ( not a[81]  or not a[78] ) 
 and  ( not a[82]  or not a[78] ) 
 and  ( not a[83]  or not a[78] ) 
 and  ( not a[84]  or not a[78] ) 
 and  ( not a[85]  or not a[78] ) 
 and  ( not a[86]  or not a[78] ) 
 and  ( not a[87]  or not a[78] ) 
 and  ( not a[88]  or not a[78] ) 
 and  ( not a[89]  or not a[78] ) 
 and  ( not a[90]  or not a[78] ) 
 and  ( not a[91]  or not a[78] ) 
 and  ( not a[107]  or not a[105] ) 
 and  ( not a[105]  or  a[106] ) 
 and  ( not a[108]  or not a[107] ) 
 and  ( not a[108]  or  a[106] ) 
 and  ( not a[110]  or not a[107] ) 
 and  ( not a[110]  or  a[106] ) 
 and  ( not a[111]  or not a[107] ) 
 and  ( not a[111]  or  a[106] ) 
 and  ( not a[112]  or not a[107] ) 
 and  ( not a[112]  or  a[106] ) 
 and  ( not a[114]  or not a[107] ) 
 and  ( not a[114]  or  a[106] ) 
 and  ( not a[116]  or not a[107] ) 
 and  ( not a[116]  or  a[106] ) 
 and  ( not a[117]  or not a[107] ) 
 and  ( not a[117]  or  a[106] ) 
 and  ( not a[123]  or not a[107] ) 
 and  ( not a[123]  or  a[106] ) 
 and  ( not a[124]  or not a[107] ) 
 and  ( not a[124]  or  a[106] ) 
 and  ( not a[79]  or not a[73] ) 
 and  ( not a[79]  or not a[74] ) 
 and  ( not a[79]  or not a[75] ) 
 and  ( not a[79]  or not a[72] ) 
 and  ( not a[79]  or not a[76] ) 
 and  ( not a[79]  or not a[77] ) 
 and  ( not a[79]  or not a[78] ) 
 and  ( not a[80]  or not a[79] ) 
 and  ( not a[81]  or not a[79] ) 
 and  ( not a[82]  or not a[79] ) 
 and  ( not a[83]  or not a[79] ) 
 and  ( not a[84]  or not a[79] ) 
 and  ( not a[85]  or not a[79] ) 
 and  ( not a[86]  or not a[79] ) 
 and  ( not a[87]  or not a[79] ) 
 and  ( not a[88]  or not a[79] ) 
 and  ( not a[89]  or not a[79] ) 
 and  ( not a[90]  or not a[79] ) 
 and  ( not a[91]  or not a[79] ) 
 and  ( not a[80]  or not a[73] ) 
 and  ( not a[80]  or not a[74] ) 
 and  ( not a[80]  or not a[75] ) 
 and  ( not a[80]  or not a[72] ) 
 and  ( not a[80]  or not a[76] ) 
 and  ( not a[80]  or not a[77] ) 
 and  ( not a[80]  or not a[78] ) 
 and  ( not a[80]  or not a[79] ) 
 and  ( not a[81]  or not a[80] ) 
 and  ( not a[82]  or not a[80] ) 
 and  ( not a[83]  or not a[80] ) 
 and  ( not a[84]  or not a[80] ) 
 and  ( not a[85]  or not a[80] ) 
 and  ( not a[86]  or not a[80] ) 
 and  ( not a[87]  or not a[80] ) 
 and  ( not a[88]  or not a[80] ) 
 and  ( not a[89]  or not a[80] ) 
 and  ( not a[90]  or not a[80] ) 
 and  ( not a[91]  or not a[80] ) 
 and  ( not a[81]  or not a[73] ) 
 and  ( not a[81]  or not a[74] ) 
 and  ( not a[81]  or not a[75] ) 
 and  ( not a[81]  or not a[72] ) 
 and  ( not a[81]  or not a[76] ) 
 and  ( not a[81]  or not a[77] ) 
 and  ( not a[81]  or not a[78] ) 
 and  ( not a[81]  or not a[79] ) 
 and  ( not a[81]  or not a[80] ) 
 and  ( not a[82]  or not a[81] ) 
 and  ( not a[83]  or not a[81] ) 
 and  ( not a[84]  or not a[81] ) 
 and  ( not a[85]  or not a[81] ) 
 and  ( not a[86]  or not a[81] ) 
 and  ( not a[87]  or not a[81] ) 
 and  ( not a[88]  or not a[81] ) 
 and  ( not a[89]  or not a[81] ) 
 and  ( not a[90]  or not a[81] ) 
 and  ( not a[91]  or not a[81] ) 
 and  ( not a[144]  or not a[107] ) 
 and  ( not a[144]  or  a[106] ) 
 and  ( not a[154]  or  a[155] ) 
 and  ( not a[161]  or not a[107] ) 
 and  ( not a[161]  or  a[106] ) 
 and  ( not a[163]  or not a[107] ) 
 and  ( not a[163]  or  a[106] ) 
 and  ( not a[164]  or not a[107] ) 
 and  ( not a[164]  or  a[106] ) 
 and  ( not a[166]  or not a[107] ) 
 and  ( not a[166]  or  a[106] ) 
 and  ( not a[167]  or not a[107] ) 
 and  ( not a[167]  or  a[106] ) 
 and  ( not a[168]  or not a[107] ) 
 and  ( not a[168]  or  a[106] ) 
 and  ( not a[169]  or not a[107] ) 
 and  ( not a[169]  or  a[106] ) 
 and  ( not a[170]  or not a[106] ) 
 and  ( not a[170]  or  a[107] ) 
 and  ( not a[171]  or not a[107] ) 
 and  ( not a[171]  or  a[106] ) 
 and  ( not a[173]  or not a[107] ) 
 and  ( not a[173]  or  a[106] ) 
 and  ( not a[177]  or  a[155] ) 
 and  ( not a[184]  or not a[107] ) 
 and  ( not a[184]  or  a[106] ) 
 and  ( not a[193]  or  a[155] ) 
 and  ( not a[85]  or not a[73] ) 
 and  ( not a[85]  or not a[74] ) 
 and  ( not a[85]  or not a[75] ) 
 and  ( not a[85]  or not a[72] ) 
 and  ( not a[85]  or not a[76] ) 
 and  ( not a[85]  or not a[77] ) 
 and  ( not a[85]  or not a[78] ) 
 and  ( not a[85]  or not a[79] ) 
 and  ( not a[85]  or not a[80] ) 
 and  ( not a[85]  or not a[81] ) 
 and  ( not a[85]  or not a[82] ) 
 and  ( not a[85]  or not a[83] ) 
 and  ( not a[85]  or not a[84] ) 
 and  ( not a[86]  or not a[85] ) 
 and  ( not a[87]  or not a[85] ) 
 and  ( not a[88]  or not a[85] ) 
 and  ( not a[89]  or not a[85] ) 
 and  ( not a[90]  or not a[85] ) 
 and  ( not a[91]  or not a[85] ) 
 and  ( not a[200]  or not a[107] ) 
 and  ( not a[200]  or  a[106] ) 
 and  ( not a[208]  or not a[106] ) 
 and  ( not a[208]  or  a[107] ) 
 and  ( not a[213]  or not a[107] ) 
 and  ( not a[213]  or  a[106] ) 
 and  ( not a[88]  or not a[73] ) 
 and  ( not a[88]  or not a[74] ) 
 and  ( not a[88]  or not a[75] ) 
 and  ( not a[88]  or not a[72] ) 
 and  ( not a[88]  or not a[76] ) 
 and  ( not a[88]  or not a[77] ) 
 and  ( not a[88]  or not a[78] ) 
 and  ( not a[88]  or not a[79] ) 
 and  ( not a[88]  or not a[80] ) 
 and  ( not a[88]  or not a[81] ) 
 and  ( not a[88]  or not a[82] ) 
 and  ( not a[88]  or not a[83] ) 
 and  ( not a[88]  or not a[84] ) 
 and  ( not a[88]  or not a[85] ) 
 and  ( not a[88]  or not a[86] ) 
 and  ( not a[88]  or not a[87] ) 
 and  ( not a[89]  or not a[88] ) 
 and  ( not a[90]  or not a[88] ) 
 and  ( not a[91]  or not a[88] ) 
 and  ( not a[219]  or not a[107] ) 
 and  ( not a[219]  or  a[106] ) 
 and  ( not a[225]  or not a[107] ) 
 and  ( not a[225]  or  a[106] ) 
 and  ( not a[226]  or not a[107] ) 
 and  ( not a[226]  or  a[106] ) 
 and  ( not a[227]  or not a[106] ) 
 and  ( not a[227]  or  a[107] ) 
 and  ( not a[228]  or not a[107] ) 
 and  ( not a[228]  or  a[106] ) 
 and  ( not a[229]  or not a[107] ) 
 and  ( not a[229]  or  a[106] ) 
 and  ( not a[230]  or not a[107] ) 
 and  ( not a[230]  or  a[106] ) 
 and  ( not a[231]  or not a[107] ) 
 and  ( not a[231]  or  a[106] ) 
 and  ( not a[237]  or not a[107] ) 
 and  ( not a[237]  or  a[106] ) 
 and  ( not a[245]  or not a[106] ) 
 and  ( not a[245]  or  a[107] ) 
 and  ( not a[247]  or not a[107] ) 
 and  ( not a[247]  or  a[106] ) 
 and  ( not a[248]  or not a[107] ) 
 and  ( not a[248]  or  a[106] ) 
 and  ( not a[252]  or not a[106] ) 
 and  ( not a[252]  or  a[107] ) 
 and  ( not a[253]  or not a[107] ) 
 and  ( not a[253]  or  a[106] ) 
 and  ( not a[254]  or not a[106] ) 
 and  ( not a[254]  or  a[107] ) 
 and  ( not a[256]  or not a[107] ) 
 and  ( not a[256]  or  a[106] ) 
 and  ( not a[257]  or not a[107] ) 
 and  ( not a[257]  or  a[106] ) 
 and  ( not a[258]  or not a[107] ) 
 and  ( not a[258]  or  a[106] ) 
 and  ( not a[259]  or not a[107] ) 
 and  ( not a[259]  or  a[106] ) 
 and  ( not a[260]  or not a[107] ) 
 and  ( not a[260]  or  a[106] ) 
 and  ( not a[269]  or not a[107] ) 
 and  ( not a[269]  or  a[106] ) 
 and  ( not a[270]  or not a[107] ) 
 and  ( not a[270]  or  a[106] ) 
 and  ( not a[272]  or not a[106] ) 
 and  ( not a[272]  or  a[107] ) 
 and  ( not a[276]  or not a[106] ) 
 and  ( not a[276]  or  a[107] ) 
 and  ( not a[282]  or not a[107] ) 
 and  ( not a[282]  or  a[106] ) 
 and  ( not a[284]  or not a[106] ) 
 and  ( not a[284]  or  a[107] ) 
 and  ( not a[285]  or not a[106] ) 
 and  ( not a[285]  or  a[107] ) 
 and  ( not a[307]  or not a[106] ) 
 and  ( not a[307]  or  a[107] ) 
 and  ( not a[317]  or not a[106] ) 
 and  ( not a[317]  or  a[107] ) 
 and  ( not a[318]  or not a[106] ) 
 and  ( not a[318]  or  a[107] ) 
 and  ( not a[89]  or not a[73] ) 
 and  ( not a[89]  or not a[74] ) 
 and  ( not a[89]  or not a[75] ) 
 and  ( not a[89]  or not a[72] ) 
 and  ( not a[89]  or not a[76] ) 
 and  ( not a[89]  or not a[77] ) 
 and  ( not a[89]  or not a[78] ) 
 and  ( not a[89]  or not a[79] ) 
 and  ( not a[89]  or not a[80] ) 
 and  ( not a[89]  or not a[81] ) 
 and  ( not a[89]  or not a[82] ) 
 and  ( not a[89]  or not a[83] ) 
 and  ( not a[89]  or not a[84] ) 
 and  ( not a[89]  or not a[85] ) 
 and  ( not a[89]  or not a[86] ) 
 and  ( not a[89]  or not a[87] ) 
 and  ( not a[89]  or not a[88] ) 
 and  ( not a[90]  or not a[89] ) 
 and  ( not a[91]  or not a[89] ) 
 and  ( not a[90]  or not a[73] ) 
 and  ( not a[90]  or not a[74] ) 
 and  ( not a[90]  or not a[75] ) 
 and  ( not a[90]  or not a[72] ) 
 and  ( not a[90]  or not a[76] ) 
 and  ( not a[90]  or not a[77] ) 
 and  ( not a[90]  or not a[78] ) 
 and  ( not a[90]  or not a[79] ) 
 and  ( not a[90]  or not a[80] ) 
 and  ( not a[90]  or not a[81] ) 
 and  ( not a[90]  or not a[82] ) 
 and  ( not a[90]  or not a[83] ) 
 and  ( not a[90]  or not a[84] ) 
 and  ( not a[90]  or not a[85] ) 
 and  ( not a[90]  or not a[86] ) 
 and  ( not a[90]  or not a[87] ) 
 and  ( not a[90]  or not a[88] ) 
 and  ( not a[90]  or not a[89] ) 
 and  ( not a[91]  or not a[90] ) 
 and  ( not a[326]  or not a[107] ) 
 and  ( not a[326]  or  a[106] ) 
 and  ( not a[328]  or not a[106] ) 
 and  ( not a[328]  or  a[107] ) 
 and  ( not a[91]  or not a[73] ) 
 and  ( not a[91]  or not a[74] ) 
 and  ( not a[91]  or not a[75] ) 
 and  ( not a[91]  or not a[72] ) 
 and  ( not a[91]  or not a[76] ) 
 and  ( not a[91]  or not a[77] ) 
 and  ( not a[91]  or not a[78] ) 
 and  ( not a[91]  or not a[79] ) 
 and  ( not a[91]  or not a[80] ) 
 and  ( not a[91]  or not a[81] ) 
 and  ( not a[91]  or not a[82] ) 
 and  ( not a[91]  or not a[83] ) 
 and  ( not a[91]  or not a[84] ) 
 and  ( not a[91]  or not a[85] ) 
 and  ( not a[91]  or not a[86] ) 
 and  ( not a[91]  or not a[87] ) 
 and  ( not a[91]  or not a[88] ) 
 and  ( not a[91]  or not a[89] ) 
 and  ( not a[91]  or not a[90] ) 
 and  ( not a[339]  or not a[338] ) 
 and  ( not a[338]  or not a[99] ) 
 and  ( not a[338]  or not a[100] ) 
 and  ( not a[338]  or not a[101] ) 
 and  ( not a[340]  or not a[338] ) 
 and  ( not a[341]  or not a[338] ) 
 and  ( not a[342]  or not a[338] ) 
 and  ( not a[343]  or not a[338] ) 
 and  ( not a[344]  or not a[338] ) 
 and  ( not a[345]  or not a[338] ) 
 and  ( not a[346]  or not a[338] ) 
 and  ( not a[347]  or not a[338] ) 
 and  ( not a[348]  or not a[338] ) 
 and  ( not a[349]  or not a[338] ) 
 and  ( not a[350]  or not a[338] ) 
 and  ( not a[351]  or not a[338] ) 
 and  ( not a[352]  or not a[338] ) 
 and  ( not a[353]  or not a[338] ) 
 and  ( not a[354]  or not a[338] ) 
 and  ( not a[355]  or not a[338] ) 
 and  ( not a[356]  or not a[338] ) 
 and  ( not a[357]  or not a[338] ) 
 and  ( not a[358]  or not a[338] ) 
 and  ( not a[359]  or not a[338] ) 
 and  ( not a[360]  or not a[338] ) 
 and  ( not a[361]  or not a[338] ) 
 and  ( not a[362]  or not a[338] ) 
 and  ( not a[363]  or not a[338] ) 
 and  ( not a[364]  or not a[338] ) 
 and  ( not a[365]  or not a[338] ) 
 and  ( not a[366]  or not a[338] ) 
 and  ( not a[367]  or not a[338] ) 
 and  ( not a[368]  or not a[338] ) 
 and  ( not a[369]  or not a[338] ) 
 and  ( not a[370]  or not a[338] ) 
 and  ( not a[371]  or not a[338] ) 
 and  ( not a[351]  or not a[339] ) 
 and  ( not a[351]  or  a[99]  or  a[100] ) 
 and  ( not a[351]  or not a[338] ) 
 and  ( not a[351]  or not a[340] ) 
 and  ( not a[351]  or not a[341] ) 
 and  ( not a[351]  or not a[342] ) 
 and  ( not a[351]  or not a[343] ) 
 and  ( not a[351]  or not a[344] ) 
 and  ( not a[351]  or not a[345] ) 
 and  ( not a[351]  or not a[346] ) 
 and  ( not a[351]  or not a[347] ) 
 and  ( not a[351]  or not a[348] ) 
 and  ( not a[351]  or not a[349] ) 
 and  ( not a[351]  or not a[350] ) 
 and  ( not a[352]  or not a[351] ) 
 and  ( not a[353]  or not a[351] ) 
 and  ( not a[354]  or not a[351] ) 
 and  ( not a[355]  or not a[351] ) 
 and  ( not a[356]  or not a[351] ) 
 and  ( not a[357]  or not a[351] ) 
 and  ( not a[358]  or not a[351] ) 
 and  ( not a[359]  or not a[351] ) 
 and  ( not a[360]  or not a[351] ) 
 and  ( not a[361]  or not a[351] ) 
 and  ( not a[362]  or not a[351] ) 
 and  ( not a[363]  or not a[351] ) 
 and  ( not a[364]  or not a[351] ) 
 and  ( not a[365]  or not a[351] ) 
 and  ( not a[366]  or not a[351] ) 
 and  ( not a[367]  or not a[351] ) 
 and  ( not a[368]  or not a[351] ) 
 and  ( not a[369]  or not a[351] ) 
 and  ( not a[370]  or not a[351] ) 
 and  ( not a[371]  or not a[351] ) 
 and  ( not a[362]  or  a[101] ) 
 and  ( not a[362]  or not a[338] ) 
 and  ( not a[362]  or not a[340] ) 
 and  ( not a[362]  or not a[341] ) 
 and  ( not a[362]  or not a[342] ) 
 and  ( not a[362]  or not a[343] ) 
 and  ( not a[362]  or not a[344] ) 
 and  ( not a[362]  or not a[345] ) 
 and  ( not a[362]  or not a[346] ) 
 and  ( not a[362]  or not a[347] ) 
 and  ( not a[362]  or not a[348] ) 
 and  ( not a[362]  or not a[349] ) 
 and  ( not a[362]  or not a[350] ) 
 and  ( not a[362]  or not a[351] ) 
 and  ( not a[362]  or not a[352] ) 
 and  ( not a[362]  or not a[353] ) 
 and  ( not a[362]  or not a[354] ) 
 and  ( not a[362]  or not a[355] ) 
 and  ( not a[362]  or not a[356] ) 
 and  ( not a[362]  or not a[357] ) 
 and  ( not a[362]  or not a[358] ) 
 and  ( not a[362]  or not a[359] ) 
 and  ( not a[362]  or not a[360] ) 
 and  ( not a[362]  or not a[361] ) 
 and  ( not a[363]  or not a[362] ) 
 and  ( not a[364]  or not a[362] ) 
 and  ( not a[365]  or not a[362] ) 
 and  ( not a[366]  or not a[362] ) 
 and  ( not a[367]  or not a[362] ) 
 and  ( not a[368]  or not a[362] ) 
 and  ( not a[369]  or not a[362] ) 
 and  ( not a[370]  or not a[362] ) 
 and  ( not a[371]  or not a[362] ) 
 and  ( not a[364]  or  a[339] ) 
 and  ( not a[364]  or  a[99]  or  a[100] ) 
 and  ( not a[364]  or not a[338] ) 
 and  ( not a[364]  or not a[340] ) 
 and  ( not a[364]  or not a[341] ) 
 and  ( not a[364]  or not a[342] ) 
 and  ( not a[364]  or not a[343] ) 
 and  ( not a[364]  or not a[344] ) 
 and  ( not a[364]  or not a[345] ) 
 and  ( not a[364]  or not a[346] ) 
 and  ( not a[364]  or not a[347] ) 
 and  ( not a[364]  or not a[348] ) 
 and  ( not a[364]  or not a[349] ) 
 and  ( not a[364]  or not a[350] ) 
 and  ( not a[364]  or not a[351] ) 
 and  ( not a[364]  or not a[352] ) 
 and  ( not a[364]  or not a[353] ) 
 and  ( not a[364]  or not a[354] ) 
 and  ( not a[364]  or not a[355] ) 
 and  ( not a[364]  or not a[356] ) 
 and  ( not a[364]  or not a[357] ) 
 and  ( not a[364]  or not a[358] ) 
 and  ( not a[364]  or not a[359] ) 
 and  ( not a[364]  or not a[360] ) 
 and  ( not a[364]  or not a[361] ) 
 and  ( not a[364]  or not a[362] ) 
 and  ( not a[364]  or not a[363] ) 
 and  ( not a[365]  or not a[364] ) 
 and  ( not a[366]  or not a[364] ) 
 and  ( not a[367]  or not a[364] ) 
 and  ( not a[368]  or not a[364] ) 
 and  ( not a[369]  or not a[364] ) 
 and  ( not a[370]  or not a[364] ) 
 and  ( not a[371]  or not a[364] ) 
 and  ( not a[366]  or  a[339] ) 
 and  ( not a[366]  or  a[96]  or  a[97] ) 
 and  ( not a[366]  or not a[338] ) 
 and  ( not a[366]  or not a[340] ) 
 and  ( not a[366]  or not a[341] ) 
 and  ( not a[366]  or not a[342] ) 
 and  ( not a[366]  or not a[343] ) 
 and  ( not a[366]  or not a[344] ) 
 and  ( not a[366]  or not a[345] ) 
 and  ( not a[366]  or not a[346] ) 
 and  ( not a[366]  or not a[347] ) 
 and  ( not a[366]  or not a[348] ) 
 and  ( not a[366]  or not a[349] ) 
 and  ( not a[366]  or not a[350] ) 
 and  ( not a[366]  or not a[351] ) 
 and  ( not a[366]  or not a[352] ) 
 and  ( not a[366]  or not a[353] ) 
 and  ( not a[366]  or not a[354] ) 
 and  ( not a[366]  or not a[355] ) 
 and  ( not a[366]  or not a[356] ) 
 and  ( not a[366]  or not a[357] ) 
 and  ( not a[366]  or not a[358] ) 
 and  ( not a[366]  or not a[359] ) 
 and  ( not a[366]  or not a[360] ) 
 and  ( not a[366]  or not a[361] ) 
 and  ( not a[366]  or not a[362] ) 
 and  ( not a[366]  or not a[363] ) 
 and  ( not a[366]  or not a[364] ) 
 and  ( not a[366]  or not a[365] ) 
 and  ( not a[367]  or not a[366] ) 
 and  ( not a[368]  or not a[366] ) 
 and  ( not a[369]  or not a[366] ) 
 and  ( not a[370]  or not a[366] ) 
 and  ( not a[371]  or not a[366] ) 
 and  ( not a[373]  or not a[372] ) 
 and  ( not a[374]  or not a[372] ) 
 and  ( not a[375]  or not a[372] ) 
 and  ( not a[376]  or not a[372] ) 
 and  ( not a[377]  or not a[372] ) 
 and  ( not a[378]  or not a[372] ) 
 and  ( not a[379]  or not a[372] ) 
 and  ( not a[380]  or not a[372] ) 
 and  ( not a[381]  or not a[372] ) 
 and  ( not a[382]  or not a[372] ) 
 and  ( not a[383]  or not a[372] ) 
 and  ( not a[385]  or not a[384] ) 
 and  ( not a[386]  or not a[384] ) 
 and  ( not a[388]  or not a[72] ) 
 and  ( not a[388]  or not a[76] ) 
 and  ( not a[388]  or not a[77] ) 
 and  ( not a[388]  or not a[78] ) 
 and  ( not a[388]  or not a[79] ) 
 and  ( not a[388]  or not a[80] ) 
 and  ( not a[388]  or not a[81] ) 
 and  ( not a[388]  or not a[85] ) 
 and  ( not a[388]  or not a[88] ) 
 and  ( not a[388]  or not a[89] ) 
 and  ( not a[388]  or not a[90] ) 
 and  ( not a[388]  or not a[91] ) 
 and  ( not a[390]  or not a[389] ) 
 and  ( not a[391]  or  a[392] ) 
 and  ( not a[393]  or not a[391] ) 
 and  ( not a[391]  or not a[390] ) 
 and  ( not a[393]  or  a[394] ) 
 and  ( not a[393]  or not a[391] ) 
 and  ( not a[393]  or not a[390] ) 
 and  ( not a[395]  or not a[393] ) 
 and  ( not a[394]  or not a[392] ) 
 and  ( not a[394]  or not a[390] ) 
 and  ( not a[394]  or not a[392] ) 
 and  ( not a[392]  or not a[390] ) 
 and  ( not a[396]  or  a[99]  or  a[100] ) 
 and  ( not a[396]  or  a[397]  or  a[398]  or  a[404] ) 
 and  ( not a[396]  or not a[339]  or  a[397]  or  a[398] ) 
 and  ( not a[399]  or not a[396]  or  a[397]  or  a[398] ) 
 and  ( not a[400]  or not a[396]  or  a[397]  or  a[398] ) 
 and  ( not a[401]  or not a[396]  or  a[397]  or  a[398] ) 
 and  ( not a[402]  or not a[396]  or  a[397]  or  a[398] ) 
 and  ( not a[403]  or not a[400]  or not a[399]  or not a[396]  or not a[339] ) 
 and  ( not a[403]  or not a[401]  or not a[399]  or not a[396]  or not a[339] ) 
 and  ( not a[403]  or not a[402]  or not a[399]  or not a[396]  or not a[339] ) 
 and  ( not a[405]  or not a[396] ) 
 and  ( not a[406]  or not a[396] ) 
 and  ( not a[407]  or not a[396] ) 
 and  ( not a[408]  or not a[396] ) 
 and  ( not a[409]  or not a[396] ) 
 and  ( not a[406]  or not a[405] ) 
 and  ( not a[407]  or not a[406] ) 
 and  ( not a[406]  or not a[396] ) 
 and  ( not a[408]  or not a[406] ) 
 and  ( not a[410]  or not a[406] ) 
 and  ( not a[409]  or not a[406] ) 
 and  ( not a[412]  or not a[411] ) 
 and  ( not a[413]  or not a[411] ) 
 and  ( not a[414]  or not a[411] ) 
 and  ( not a[415]  or not a[411] ) 
 and  ( not a[416]  or not a[411] ) 
 and  ( not a[417]  or not a[411] ) 
 and  ( not a[418]  or not a[411] ) 
 and  ( not a[419]  or not a[411] ) 
 and  ( not a[420]  or not a[411] ) 
 and  ( not a[421]  or not a[411] ) 
 and  ( not a[422]  or not a[411] ) 
 and  ( not a[423]  or not a[411] ) 
 and  ( not a[424]  or not a[411] ) 
 and  ( not a[425]  or not a[411] ) 
 and  ( not a[426]  or not a[411] ) 
 and  ( not a[427]  or not a[411] ) 
 and  ( not a[428]  or not a[411] ) 
 and  ( not a[429]  or not a[411] ) 
 and  ( not a[430]  or not a[411] ) 
 and  ( not a[431]  or not a[411] ) 
 and  ( not a[432]  or not a[411] ) 
 and  ( not a[433]  or not a[411] ) 
 and  ( not a[434]  or not a[411] ) 
 and  ( not a[435]  or not a[411] ) 
 and  ( not a[436]  or not a[411] ) 
 and  ( not a[437]  or not a[411] ) 
 and  ( not a[438]  or not a[411] ) 
 and  ( not a[439]  or not a[411] ) 
 and  ( not a[440]  or not a[411] ) 
 and  ( not a[441]  or not a[411] ) 
 and  ( not a[442]  or not a[411] ) 
 and  ( not a[443]  or not a[411] ) 
 and  ( not a[444]  or not a[411] ) 
 and  ( not a[445]  or not a[411] ) 
 and  ( not a[419]  or not a[411] ) 
 and  ( not a[419]  or not a[414] ) 
 and  ( not a[419]  or not a[415] ) 
 and  ( not a[419]  or not a[416] ) 
 and  ( not a[420]  or not a[419] ) 
 and  ( not a[421]  or not a[419] ) 
 and  ( not a[422]  or not a[419] ) 
 and  ( not a[426]  or not a[419] ) 
 and  ( not a[427]  or not a[419] ) 
 and  ( not a[428]  or not a[419] ) 
 and  ( not a[429]  or not a[419] ) 
 and  ( not a[430]  or not a[419] ) 
 and  ( not a[431]  or not a[419] ) 
 and  ( not a[432]  or not a[419] ) 
 and  ( not a[433]  or not a[419] ) 
 and  ( not a[446]  or not a[419] ) 
 and  ( not a[447]  or not a[419] ) 
 and  ( not a[435]  or not a[419] ) 
 and  ( not a[436]  or not a[419] ) 
 and  ( not a[437]  or not a[419] ) 
 and  ( not a[438]  or not a[419] ) 
 and  ( not a[439]  or not a[419] ) 
 and  ( not a[440]  or not a[419] ) 
 and  ( not a[441]  or not a[419] ) 
 and  ( not a[442]  or not a[419] ) 
 and  ( not a[443]  or not a[419] ) 
 and  ( not a[444]  or not a[419] ) 
 and  ( not a[445]  or not a[419] ) 
 and  ( not a[420]  or not a[411] ) 
 and  ( not a[420]  or not a[414] ) 
 and  ( not a[420]  or not a[415] ) 
 and  ( not a[420]  or not a[416] ) 
 and  ( not a[420]  or not a[419] ) 
 and  ( not a[421]  or not a[420] ) 
 and  ( not a[422]  or not a[420] ) 
 and  ( not a[426]  or not a[420] ) 
 and  ( not a[427]  or not a[420] ) 
 and  ( not a[428]  or not a[420] ) 
 and  ( not a[429]  or not a[420] ) 
 and  ( not a[430]  or not a[420] ) 
 and  ( not a[431]  or not a[420] ) 
 and  ( not a[432]  or not a[420] ) 
 and  ( not a[433]  or not a[420] ) 
 and  ( not a[446]  or not a[420] ) 
 and  ( not a[447]  or not a[420] ) 
 and  ( not a[435]  or not a[420] ) 
 and  ( not a[436]  or not a[420] ) 
 and  ( not a[437]  or not a[420] ) 
 and  ( not a[438]  or not a[420] ) 
 and  ( not a[439]  or not a[420] ) 
 and  ( not a[440]  or not a[420] ) 
 and  ( not a[441]  or not a[420] ) 
 and  ( not a[442]  or not a[420] ) 
 and  ( not a[443]  or not a[420] ) 
 and  ( not a[444]  or not a[420] ) 
 and  ( not a[445]  or not a[420] ) 
 and  ( not a[421]  or not a[412] ) 
 and  ( not a[421]  or not a[411] ) 
 and  ( not a[421]  or not a[414] ) 
 and  ( not a[421]  or not a[415] ) 
 and  ( not a[421]  or not a[416] ) 
 and  ( not a[421]  or not a[419] ) 
 and  ( not a[421]  or not a[420] ) 
 and  ( not a[422]  or not a[421] ) 
 and  ( not a[423]  or not a[421] ) 
 and  ( not a[424]  or not a[421] ) 
 and  ( not a[425]  or not a[421] ) 
 and  ( not a[426]  or not a[421] ) 
 and  ( not a[427]  or not a[421] ) 
 and  ( not a[428]  or not a[421] ) 
 and  ( not a[429]  or not a[421] ) 
 and  ( not a[430]  or not a[421] ) 
 and  ( not a[431]  or not a[421] ) 
 and  ( not a[432]  or not a[421] ) 
 and  ( not a[433]  or not a[421] ) 
 and  ( not a[434]  or not a[421] ) 
 and  ( not a[435]  or not a[421] ) 
 and  ( not a[436]  or not a[421] ) 
 and  ( not a[437]  or not a[421] ) 
 and  ( not a[438]  or not a[421] ) 
 and  ( not a[439]  or not a[421] ) 
 and  ( not a[440]  or not a[421] ) 
 and  ( not a[441]  or not a[421] ) 
 and  ( not a[442]  or not a[421] ) 
 and  ( not a[443]  or not a[421] ) 
 and  ( not a[444]  or not a[421] ) 
 and  ( not a[445]  or not a[421] ) 
 and  ( not a[424]  or not a[411] ) 
 and  ( not a[424]  or not a[421] ) 
 and  ( not a[424]  or not a[422] ) 
 and  ( not a[424]  or not a[423] ) 
 and  ( not a[425]  or not a[424] ) 
 and  ( not a[426]  or not a[424] ) 
 and  ( not a[427]  or not a[424] ) 
 and  ( not a[428]  or not a[424] ) 
 and  ( not a[429]  or not a[424] ) 
 and  ( not a[430]  or not a[424] ) 
 and  ( not a[431]  or not a[424] ) 
 and  ( not a[432]  or not a[424] ) 
 and  ( not a[433]  or not a[424] ) 
 and  ( not a[434]  or not a[424] ) 
 and  ( not a[435]  or not a[424] ) 
 and  ( not a[436]  or not a[424] ) 
 and  ( not a[437]  or not a[424] ) 
 and  ( not a[438]  or not a[424] ) 
 and  ( not a[439]  or not a[424] ) 
 and  ( not a[440]  or not a[424] ) 
 and  ( not a[441]  or not a[424] ) 
 and  ( not a[442]  or not a[424] ) 
 and  ( not a[443]  or not a[424] ) 
 and  ( not a[444]  or not a[424] ) 
 and  ( not a[445]  or not a[424] ) 
 and  ( not a[448]  or  a[419]  or  a[420]  or  a[421]  or  a[431] ) 
 and  ( not a[450]  or not a[431] ) 
 and  ( not a[451]  or not a[431] ) 
 and  ( not a[431]  or not a[411] ) 
 and  ( not a[431]  or not a[414] ) 
 and  ( not a[431]  or not a[415] ) 
 and  ( not a[431]  or not a[416] ) 
 and  ( not a[431]  or not a[419] ) 
 and  ( not a[431]  or not a[420] ) 
 and  ( not a[431]  or not a[421] ) 
 and  ( not a[431]  or not a[422] ) 
 and  ( not a[431]  or not a[423] ) 
 and  ( not a[431]  or not a[424] ) 
 and  ( not a[431]  or not a[425] ) 
 and  ( not a[431]  or not a[426] ) 
 and  ( not a[431]  or not a[427] ) 
 and  ( not a[431]  or not a[428] ) 
 and  ( not a[431]  or not a[429] ) 
 and  ( not a[431]  or not a[430] ) 
 and  ( not a[432]  or not a[431] ) 
 and  ( not a[433]  or not a[431] ) 
 and  ( not a[434]  or not a[431] ) 
 and  ( not a[435]  or not a[431] ) 
 and  ( not a[436]  or not a[431] ) 
 and  ( not a[437]  or not a[431] ) 
 and  ( not a[438]  or not a[431] ) 
 and  ( not a[439]  or not a[431] ) 
 and  ( not a[440]  or not a[431] ) 
 and  ( not a[441]  or not a[431] ) 
 and  ( not a[442]  or not a[431] ) 
 and  ( not a[443]  or not a[431] ) 
 and  ( not a[444]  or not a[431] ) 
 and  ( not a[445]  or not a[431] ) 
 and  ( not a[454]  or not a[453] ) 
 and  ( not a[455]  or not a[453] ) 
 and  ( not a[456]  or not a[453] ) 
 and  ( not a[457]  or not a[453] ) 
 and  ( not a[458]  or not a[453] ) 
 and  ( not a[459]  or not a[453] ) 
 and  ( not a[460]  or not a[453] ) 
 and  ( not a[461]  or not a[453] ) 
 and  ( not a[462]  or not a[453] ) 
 and  ( not a[463]  or not a[453] ) 
 and  ( not a[464]  or not a[453] ) 
 and  ( not a[465]  or not a[453] ) 
 and  ( not a[466]  or not a[453] ) 
 and  ( not a[467]  or not a[453] ) 
 and  ( not a[468]  or not a[453] ) 
 and  ( not a[469]  or not a[453] ) 
 and  ( not a[470]  or not a[453] ) 
 and  ( not a[471]  or not a[453] ) 
 and  ( not a[472]  or not a[453] ) 
 and  ( not a[473]  or not a[453] ) 
 and  ( not a[476]  or not a[475] ) 
 and  ( not a[477]  or not a[475] ) 
 and  ( not a[478]  or not a[475] ) 
 and  ( not a[481]  or not a[480] ) 
 and  ( not a[482]  or not a[480] ) 
 and  ( not a[483]  or not a[480] ) 
 and  ( not a[482]  or not a[481] ) 
 and  ( not a[481]  or not a[109] ) 
 and  ( not a[481]  or not a[127] ) 
 and  ( not a[481]  or not a[140] ) 
 and  ( not a[481]  or not a[480] ) 
 and  ( not a[483]  or not a[481] ) 
 and  ( not a[482]  or not a[481] ) 
 and  ( not a[482]  or not a[480] ) 
 and  ( not a[483]  or not a[482] ) 
 and  ( not a[403]  or not a[339]  or  a[484]  or  a[485] ) 
 and  ( not a[404]  or not a[339]  or not a[96]  or  a[484]  or  a[485] ) 
 and  ( not a[404]  or not a[339]  or not a[97]  or  a[484]  or  a[485] ) 
 and  ( not a[339]  or not a[99]  or  a[484]  or  a[485] ) 
 and  ( not a[339]  or not a[100]  or  a[484]  or  a[485] ) 
 and  ( not a[486]  or not a[339] ) 
 and  ( not a[487]  or not a[339] ) 
 and  ( not a[488]  or not a[339] ) 
 and  ( not a[489]  or not a[339] ) 
 and  ( not a[490]  or not a[339] ) 
 and  ( not a[491]  or not a[339] ) 
 and  ( not a[492]  or not a[339] ) 
 and  ( not a[493]  or not a[339] ) 
 and  ( not a[494]  or not a[339] ) 
 and  ( not a[495]  or not a[339] ) 
 and  ( not a[496]  or not a[339] ) 
 and  ( not a[497]  or not a[339] ) 
 and  ( not a[498]  or not a[339] ) 
 and  ( not a[499]  or not a[339] ) 
 and  ( not a[500]  or not a[339] ) 
 and  ( not a[501]  or not a[339] ) 
 and  ( not a[502]  or not a[339] ) 
 and  ( not a[404]  or not a[400]  or not a[399]  or not a[339]  or  a[485] ) 
 and  ( not a[404]  or not a[403]  or not a[400]  or not a[399]  or  a[485] ) 
 and  ( not a[399]  or  a[484]  or  a[485] ) 
 and  ( not a[503]  or not a[399] ) 
 and  ( not a[504]  or not a[399] ) 
 and  ( not a[505]  or not a[399] ) 
 and  ( not a[506]  or not a[399] ) 
 and  ( not a[507]  or not a[399] ) 
 and  ( not a[508]  or not a[399] ) 
 and  ( not a[510]  or not a[509] ) 
 and  ( not a[511]  or not a[509] ) 
 and  ( not a[512]  or not a[509] ) 
 and  ( not a[513]  or not a[509] ) 
 and  ( not a[514]  or not a[509] ) 
 and  ( not a[515]  or not a[509] ) 
 and  ( not a[516]  or  a[400] ) 
 and  ( not a[517]  or not a[516] ) 
 and  ( not a[518]  or not a[516] ) 
 and  ( not a[519]  or not a[516] ) 
 and  ( not a[520]  or not a[516] ) 
 and  ( not a[521]  or not a[516] ) 
 and  ( not a[522]  or not a[516] ) 
 and  ( not a[523]  or not a[516] ) 
 and  ( not a[524]  or not a[516] ) 
 and  ( not a[400]  or not a[399]  or not a[107]  or  a[484]  or  a[485] ) 
 and  ( not a[403]  or not a[400]  or not a[107]  or  a[484]  or  a[485] ) 
 and  ( not a[404]  or not a[400]  or not a[107]  or  a[484]  or  a[485] ) 
 and  ( not a[401]  or not a[400]  or not a[106] ) 
 and  ( not a[400]  or not a[107]  or  a[516] ) 
 and  ( not a[401]  or not a[400]  or not a[107] ) 
 and  ( not a[524]  or not a[400] ) 
 and  ( not a[525]  or not a[400] ) 
 and  ( not a[527]  or not a[526] ) 
 and  ( not a[528]  or not a[526] ) 
 and  ( not a[511]  or not a[510] ) 
 and  ( not a[511]  or not a[509] ) 
 and  ( not a[511]  or  a[96]  or  a[97] ) 
 and  ( not a[512]  or not a[511] ) 
 and  ( not a[513]  or not a[511] ) 
 and  ( not a[514]  or not a[511] ) 
 and  ( not a[515]  or not a[511] ) 
 and  ( not a[529]  or  a[399] ) 
 and  ( not a[529]  or not a[391] ) 
 and  ( not a[529]  or not a[393] ) 
 and  ( not a[529]  or not a[480] ) 
 and  ( not a[529]  or not a[481] ) 
 and  ( not a[530]  or not a[529] ) 
 and  ( not a[531]  or not a[529] ) 
 and  ( not a[532]  or not a[529] ) 
 and  ( not a[533]  or  a[509]  or  a[510] ) 
 and  ( not a[510]  or not a[509] ) 
 and  ( not a[511]  or not a[510] ) 
 and  ( not a[510]  or  a[96]  or  a[97] ) 
 and  ( not a[512]  or not a[510] ) 
 and  ( not a[513]  or not a[510] ) 
 and  ( not a[514]  or not a[510] ) 
 and  ( not a[515]  or not a[510] ) 
 and  ( not a[555]  or not a[534] ) 
 and  ( not a[554]  or not a[534] ) 
 and  ( not a[553]  or not a[534] ) 
 and  ( not a[552]  or not a[534] ) 
 and  ( not a[551]  or not a[534] ) 
 and  ( not a[550]  or not a[534] ) 
 and  ( not a[549]  or not a[534] ) 
 and  ( not a[548]  or not a[534] ) 
 and  ( not a[547]  or not a[534] ) 
 and  ( not a[546]  or not a[534] ) 
 and  ( not a[545]  or not a[534] ) 
 and  ( not a[544]  or not a[534] ) 
 and  ( not a[543]  or not a[534] ) 
 and  ( not a[542]  or not a[534] ) 
 and  ( not a[541]  or not a[534] ) 
 and  ( not a[540]  or not a[534] ) 
 and  ( not a[539]  or not a[534] ) 
 and  ( not a[538]  or not a[534] ) 
 and  ( not a[537]  or not a[534] ) 
 and  ( not a[534]  or  a[535]  or  a[536] ) 
 and  ( not a[534]  or not a[336] ) 
 and  ( not a[534]  or not a[335] ) 
 and  ( not a[534]  or not a[334] ) 
 and  ( not a[534]  or not a[333] ) 
 and  ( not a[534]  or not a[332] ) 
 and  ( not a[534]  or not a[331] ) 
 and  ( not a[534]  or not a[330] ) 
 and  ( not a[534]  or not a[329] ) 
 and  ( not a[534]  or not a[328] ) 
 and  ( not a[534]  or not a[327] ) 
 and  ( not a[534]  or not a[326] ) 
 and  ( not a[534]  or not a[325] ) 
 and  ( not a[534]  or not a[324] ) 
 and  ( not a[534]  or not a[323] ) 
 and  ( not a[534]  or not a[322] ) 
 and  ( not a[534]  or not a[321] ) 
 and  ( not a[534]  or not a[320] ) 
 and  ( not a[534]  or not a[319] ) 
 and  ( not a[534]  or not a[318] ) 
 and  ( not a[534]  or not a[317] ) 
 and  ( not a[534]  or not a[315] ) 
 and  ( not a[534]  or not a[314] ) 
 and  ( not a[534]  or not a[313] ) 
 and  ( not a[534]  or not a[312] ) 
 and  ( not a[534]  or not a[311] ) 
 and  ( not a[534]  or not a[310] ) 
 and  ( not a[534]  or not a[309] ) 
 and  ( not a[534]  or not a[308] ) 
 and  ( not a[534]  or not a[307] ) 
 and  ( not a[534]  or not a[306] ) 
 and  ( not a[534]  or not a[305] ) 
 and  ( not a[534]  or not a[304] ) 
 and  ( not a[534]  or not a[303] ) 
 and  ( not a[534]  or not a[302] ) 
 and  ( not a[534]  or not a[301] ) 
 and  ( not a[534]  or not a[300] ) 
 and  ( not a[534]  or not a[299] ) 
 and  ( not a[534]  or not a[298] ) 
 and  ( not a[534]  or not a[297] ) 
 and  ( not a[534]  or not a[296] ) 
 and  ( not a[534]  or not a[295] ) 
 and  ( not a[534]  or not a[294] ) 
 and  ( not a[534]  or not a[293] ) 
 and  ( not a[534]  or not a[292] ) 
 and  ( not a[534]  or not a[291] ) 
 and  ( not a[534]  or not a[290] ) 
 and  ( not a[534]  or not a[289] ) 
 and  ( not a[534]  or not a[288] ) 
 and  ( not a[534]  or not a[287] ) 
 and  ( not a[534]  or not a[286] ) 
 and  ( not a[534]  or not a[285] ) 
 and  ( not a[534]  or not a[284] ) 
 and  ( not a[534]  or not a[283] ) 
 and  ( not a[534]  or not a[282] ) 
 and  ( not a[534]  or not a[281] ) 
 and  ( not a[534]  or not a[280] ) 
 and  ( not a[534]  or not a[279] ) 
 and  ( not a[534]  or not a[278] ) 
 and  ( not a[534]  or not a[277] ) 
 and  ( not a[534]  or not a[276] ) 
 and  ( not a[534]  or not a[275] ) 
 and  ( not a[534]  or not a[274] ) 
 and  ( not a[534]  or not a[273] ) 
 and  ( not a[534]  or not a[272] ) 
 and  ( not a[534]  or not a[271] ) 
 and  ( not a[534]  or not a[270] ) 
 and  ( not a[534]  or not a[269] ) 
 and  ( not a[534]  or not a[266] ) 
 and  ( not a[534]  or not a[265] ) 
 and  ( not a[534]  or not a[264] ) 
 and  ( not a[534]  or not a[263] ) 
 and  ( not a[534]  or not a[262] ) 
 and  ( not a[534]  or not a[261] ) 
 and  ( not a[534]  or not a[260] ) 
 and  ( not a[534]  or not a[259] ) 
 and  ( not a[534]  or not a[258] ) 
 and  ( not a[534]  or not a[257] ) 
 and  ( not a[534]  or not a[256] ) 
 and  ( not a[534]  or not a[255] ) 
 and  ( not a[534]  or not a[254] ) 
 and  ( not a[534]  or not a[253] ) 
 and  ( not a[534]  or not a[252] ) 
 and  ( not a[534]  or not a[251] ) 
 and  ( not a[534]  or not a[250] ) 
 and  ( not a[534]  or not a[249] ) 
 and  ( not a[534]  or not a[248] ) 
 and  ( not a[534]  or not a[247] ) 
 and  ( not a[534]  or not a[246] ) 
 and  ( not a[534]  or not a[245] ) 
 and  ( not a[534]  or not a[243] ) 
 and  ( not a[534]  or not a[242] ) 
 and  ( not a[534]  or not a[241] ) 
 and  ( not a[534]  or not a[240] ) 
 and  ( not a[534]  or not a[239] ) 
 and  ( not a[534]  or not a[238] ) 
 and  ( not a[534]  or not a[237] ) 
 and  ( not a[534]  or not a[236] ) 
 and  ( not a[534]  or not a[235] ) 
 and  ( not a[534]  or not a[234] ) 
 and  ( not a[534]  or not a[233] ) 
 and  ( not a[534]  or not a[232] ) 
 and  ( not a[534]  or not a[231] ) 
 and  ( not a[534]  or not a[230] ) 
 and  ( not a[534]  or not a[229] ) 
 and  ( not a[534]  or not a[228] ) 
 and  ( not a[534]  or not a[227] ) 
 and  ( not a[534]  or not a[226] ) 
 and  ( not a[534]  or not a[225] ) 
 and  ( not a[534]  or not a[224] ) 
 and  ( not a[534]  or not a[223] ) 
 and  ( not a[534]  or not a[222] ) 
 and  ( not a[534]  or not a[221] ) 
 and  ( not a[534]  or not a[219] ) 
 and  ( not a[534]  or not a[218] ) 
 and  ( not a[534]  or not a[216] ) 
 and  ( not a[534]  or not a[215] ) 
 and  ( not a[534]  or not a[214] ) 
 and  ( not a[534]  or not a[213] ) 
 and  ( not a[534]  or not a[212] ) 
 and  ( not a[534]  or not a[211] ) 
 and  ( not a[534]  or not a[210] ) 
 and  ( not a[534]  or not a[209] ) 
 and  ( not a[534]  or not a[208] ) 
 and  ( not a[534]  or not a[207] ) 
 and  ( not a[534]  or not a[206] ) 
 and  ( not a[534]  or not a[205] ) 
 and  ( not a[534]  or not a[204] ) 
 and  ( not a[534]  or not a[203] ) 
 and  ( not a[534]  or not a[202] ) 
 and  ( not a[534]  or not a[201] ) 
 and  ( not a[534]  or not a[200] ) 
 and  ( not a[534]  or not a[199] ) 
 and  ( not a[534]  or not a[198] ) 
 and  ( not a[534]  or not a[197] ) 
 and  ( not a[534]  or not a[196] ) 
 and  ( not a[534]  or not a[195] ) 
 and  ( not a[534]  or not a[194] ) 
 and  ( not a[534]  or not a[193] ) 
 and  ( not a[534]  or not a[192] ) 
 and  ( not a[534]  or not a[191] ) 
 and  ( not a[534]  or not a[190] ) 
 and  ( not a[534]  or not a[189] ) 
 and  ( not a[534]  or not a[188] ) 
 and  ( not a[534]  or not a[187] ) 
 and  ( not a[534]  or not a[186] ) 
 and  ( not a[534]  or not a[185] ) 
 and  ( not a[534]  or not a[184] ) 
 and  ( not a[534]  or not a[183] ) 
 and  ( not a[534]  or not a[182] ) 
 and  ( not a[534]  or not a[181] ) 
 and  ( not a[534]  or not a[180] ) 
 and  ( not a[534]  or not a[179] ) 
 and  ( not a[534]  or not a[178] ) 
 and  ( not a[534]  or not a[177] ) 
 and  ( not a[534]  or not a[176] ) 
 and  ( not a[534]  or not a[175] ) 
 and  ( not a[534]  or not a[174] ) 
 and  ( not a[534]  or not a[173] ) 
 and  ( not a[534]  or not a[172] ) 
 and  ( not a[534]  or not a[171] ) 
 and  ( not a[534]  or not a[170] ) 
 and  ( not a[534]  or not a[169] ) 
 and  ( not a[534]  or not a[168] ) 
 and  ( not a[534]  or not a[167] ) 
 and  ( not a[534]  or not a[166] ) 
 and  ( not a[534]  or not a[165] ) 
 and  ( not a[534]  or not a[164] ) 
 and  ( not a[534]  or not a[163] ) 
 and  ( not a[534]  or not a[162] ) 
 and  ( not a[534]  or not a[161] ) 
 and  ( not a[534]  or not a[160] ) 
 and  ( not a[534]  or not a[158] ) 
 and  ( not a[534]  or not a[157] ) 
 and  ( not a[534]  or not a[156] ) 
 and  ( not a[534]  or not a[154] ) 
 and  ( not a[534]  or not a[153] ) 
 and  ( not a[534]  or not a[152] ) 
 and  ( not a[534]  or not a[151] ) 
 and  ( not a[534]  or not a[150] ) 
 and  ( not a[534]  or not a[149] ) 
 and  ( not a[534]  or not a[148] ) 
 and  ( not a[534]  or not a[147] ) 
 and  ( not a[534]  or not a[146] ) 
 and  ( not a[534]  or not a[145] ) 
 and  ( not a[534]  or not a[144] ) 
 and  ( not a[534]  or not a[143] ) 
 and  ( not a[534]  or not a[142] ) 
 and  ( not a[534]  or not a[141] ) 
 and  ( not a[534]  or not a[140] ) 
 and  ( not a[534]  or not a[139] ) 
 and  ( not a[534]  or not a[138] ) 
 and  ( not a[534]  or not a[137] ) 
 and  ( not a[534]  or not a[136] ) 
 and  ( not a[534]  or not a[135] ) 
 and  ( not a[534]  or not a[134] ) 
 and  ( not a[534]  or not a[133] ) 
 and  ( not a[534]  or not a[132] ) 
 and  ( not a[534]  or not a[131] ) 
 and  ( not a[534]  or not a[129] ) 
 and  ( not a[534]  or not a[128] ) 
 and  ( not a[534]  or not a[127] ) 
 and  ( not a[534]  or not a[126] ) 
 and  ( not a[534]  or not a[125] ) 
 and  ( not a[534]  or not a[124] ) 
 and  ( not a[534]  or not a[123] ) 
 and  ( not a[534]  or not a[122] ) 
 and  ( not a[534]  or not a[121] ) 
 and  ( not a[534]  or not a[120] ) 
 and  ( not a[534]  or not a[119] ) 
 and  ( not a[534]  or not a[118] ) 
 and  ( not a[534]  or not a[117] ) 
 and  ( not a[534]  or not a[116] ) 
 and  ( not a[534]  or not a[115] ) 
 and  ( not a[534]  or not a[114] ) 
 and  ( not a[534]  or not a[113] ) 
 and  ( not a[534]  or not a[112] ) 
 and  ( not a[534]  or not a[111] ) 
 and  ( not a[534]  or not a[110] ) 
 and  ( not a[534]  or not a[109] ) 
 and  ( not a[534]  or not a[108] ) 
 and  ( not a[534]  or not a[105] ) 
 and  ( not a[534]  or not a[103] ) 
 and  ( not a[534]  or not a[102] ) 
 and  ( not a[534]  or  a[98]  or  a[99]  or  a[100]  or  a[101] ) 
 and  ( not a[534]  or  a[96]  or  a[97]  or  a[99]  or  a[100]  or  a[101] ) 
 and  ( not a[534]  or not a[95] ) 
 and  ( not a[564]  or not a[538] ) 
 and  ( not a[563]  or not a[538] ) 
 and  ( not a[562]  or not a[538] ) 
 and  ( not a[561]  or not a[538] ) 
 and  ( not a[560]  or not a[538] ) 
 and  ( not a[559]  or not a[538] ) 
 and  ( not a[558]  or not a[538] ) 
 and  ( not a[557]  or not a[538] ) 
 and  ( not a[556]  or not a[538] ) 
 and  ( not a[552]  or not a[538] ) 
 and  ( not a[538]  or not a[537] ) 
 and  ( not a[538]  or not a[534] ) 
 and  ( not a[538]  or not a[336] ) 
 and  ( not a[538]  or not a[335] ) 
 and  ( not a[538]  or not a[334] ) 
 and  ( not a[538]  or not a[333] ) 
 and  ( not a[538]  or not a[331] ) 
 and  ( not a[538]  or not a[330] ) 
 and  ( not a[538]  or not a[329] ) 
 and  ( not a[538]  or not a[324] ) 
 and  ( not a[538]  or not a[323] ) 
 and  ( not a[538]  or not a[321] ) 
 and  ( not a[538]  or not a[320] ) 
 and  ( not a[538]  or not a[319] ) 
 and  ( not a[538]  or not a[315] ) 
 and  ( not a[538]  or not a[308] ) 
 and  ( not a[538]  or not a[307] ) 
 and  ( not a[538]  or not a[306] ) 
 and  ( not a[538]  or not a[305] ) 
 and  ( not a[538]  or not a[299] ) 
 and  ( not a[538]  or not a[295] ) 
 and  ( not a[538]  or not a[288] ) 
 and  ( not a[538]  or not a[287] ) 
 and  ( not a[538]  or not a[278] ) 
 and  ( not a[538]  or not a[274] ) 
 and  ( not a[538]  or not a[272] ) 
 and  ( not a[538]  or not a[269] ) 
 and  ( not a[538]  or not a[244] ) 
 and  ( not a[538]  or not a[242] ) 
 and  ( not a[538]  or not a[218] ) 
 and  ( not a[538]  or not a[194] ) 
 and  ( not a[538]  or not a[187] ) 
 and  ( not a[538]  or not a[183] ) 
 and  ( not a[538]  or not a[173] ) 
 and  ( not a[538]  or not a[172] ) 
 and  ( not a[538]  or not a[166] ) 
 and  ( not a[538]  or not a[94] ) 
 and  ( not a[538]  or not a[93] ) 
 and  ( not a[538]  or not a[92] ) 
 and  ( not a[538]  or not a[70] ) 
 and  ( not a[538]  or not a[69] ) 
 and  ( not a[538]  or not a[68] ) 
 and  ( not a[538]  or not a[67] ) 
 and  ( not a[538]  or not a[66] ) 
 and  ( not a[538]  or not a[65] ) 
 and  ( not a[538]  or not a[63] ) 
 and  ( not a[538]  or not a[59] ) 
 and  ( not a[538]  or not a[58] ) 
 and  ( not a[538]  or not a[57] ) 
 and  ( not a[538]  or not a[56] ) 
 and  ( not a[538]  or not a[51] ) 
 and  ( not a[538]  or not a[50] ) 
 and  ( not a[538]  or not a[49] ) 
 and  ( not a[538]  or not a[48] ) 
 and  ( not a[538]  or not a[47] ) 
 and  ( not a[538]  or not a[46] ) 
 and  ( not a[538]  or not a[45] ) 
 and  ( not a[538]  or not a[44] ) 
 and  ( not a[538]  or not a[43] ) 
 and  ( not a[538]  or not a[42] ) 
 and  ( not a[538]  or not a[41] ) 
 and  ( not a[538]  or not a[40] ) 
 and  ( not a[538]  or not a[39] ) 
 and  ( not a[538]  or not a[38] ) 
 and  ( not a[538]  or not a[37] ) 
 and  ( not a[538]  or not a[36] ) 
 and  ( not a[538]  or not a[35] ) 
 and  ( not a[538]  or not a[34] ) 
 and  ( not a[538]  or not a[33] ) 
 and  ( not a[538]  or not a[32] ) 
 and  ( not a[538]  or not a[31] ) 
 and  ( not a[538]  or not a[30] ) 
 and  ( not a[538]  or not a[29] ) 
 and  ( not a[538]  or not a[28] ) 
 and  ( not a[538]  or not a[27] ) 
 and  ( not a[538]  or not a[26] ) 
 and  ( not a[538]  or not a[25] ) 
 and  ( not a[538]  or not a[24] ) 
 and  ( not a[538]  or not a[23] ) 
 and  ( not a[538]  or not a[22] ) 
 and  ( not a[538]  or not a[21] ) 
 and  ( not a[538]  or not a[20] ) 
 and  ( not a[538]  or not a[19] ) 
 and  ( not a[538]  or not a[18] ) 
 and  ( not a[538]  or not a[17] ) 
 and  ( not a[538]  or not a[16] ) 
 and  ( not a[538]  or not a[15] ) 
 and  ( not a[538]  or not a[14] ) 
 and  ( not a[538]  or not a[13] ) 
 and  ( not a[538]  or not a[12] ) 
 and  ( not a[538]  or not a[11] ) 
 and  ( not a[538]  or not a[10] ) 
 and  ( not a[538]  or not a[9] ) 
 and  ( not a[538]  or not a[8] ) 
 and  ( not a[538]  or not a[7] ) 
 and  ( not a[538]  or not a[6] ) 
 and  ( not a[538]  or not a[5] ) 
 and  ( not a[538]  or not a[4] ) 
 and  ( not a[538]  or not a[3] ) 
 and  ( not a[538]  or not a[2] ) 
 and  ( not a[538]  or not a[1] ) 
 and  ( not a[538]  or not a[0] ) 
 and  ( not a[565]  or not a[106] ) 
 and  ( not a[565]  or  a[107] ) 
 and  ( not a[566]  or not a[565] ) 
 and  ( not a[567]  or not a[565] ) 
 and  ( not a[568]  or not a[565] ) 
 and  ( not a[569]  or not a[565] ) 
 and  ( not a[570]  or not a[565] ) 
 and  ( not a[571]  or not a[565] ) 
 and  ( not a[572]  or not a[565] ) 
 and  ( not a[573]  or not a[101] ) 
 and  ( not a[573]  or not a[450] ) 
 and  ( not a[573]  or not a[451] ) 
 and  ( not a[574]  or not a[573] ) 
 and  ( not a[573]  or not a[567] ) 
 and  ( not a[573]  or not a[568] ) 
 and  ( not a[573]  or not a[569] ) 
 and  ( not a[573]  or not a[570] ) 
 and  ( not a[573]  or not a[571] ) 
 and  ( not a[575]  or not a[573] ) 
 and  ( not a[573]  or not a[572] ) 
 and  ( not a[576]  or not a[530] ) 
 and  ( not a[577]  or not a[106] ) 
 and  ( not a[577]  or not a[107]  or  a[578] ) 
 and  ( not a[577]  or  a[107] ) 
 and  ( not a[580]  or not a[101] ) 
 and  ( not a[581]  or  a[411]  or  a[419]  or  a[420]  or  a[421]  or  a[424]  or  a[431] ) 
 and  ( not a[582]  or not a[581] ) 
 and  ( not a[583]  or not a[581] ) 
 and  ( not a[583]  or not a[538] ) 
 and  ( not a[583]  or not a[582] ) 
 and  ( not a[583]  or not a[581] ) 
 and  ( not a[582]  or  a[411]  or  a[419]  or  a[420]  or  a[421]  or  a[424]  or  a[431] ) 
 and  ( not a[582]  or not a[581] ) 
 and  ( not a[583]  or not a[582] ) 
 and  ( not a[584]  or  a[96]  or  a[97] ) 
 and  ( not a[585]  or  a[99]  or  a[100]  or  a[101] ) 
 and  ( not a[586]  or not a[585] ) 
 and  ( not a[587]  or not a[585] ) 
 and  ( not a[404]  or not a[403]  or not a[96]  or  a[484]  or  a[485] ) 
 and  ( not a[404]  or not a[403]  or not a[97]  or  a[484]  or  a[485] ) 
 and  ( not a[403]  or not a[99]  or  a[484]  or  a[485] ) 
 and  ( not a[403]  or not a[100]  or  a[484]  or  a[485] ) 
 and  ( not a[589]  or not a[107] ) 
 and  ( not a[589]  or  a[106] ) 
 and  ( not a[484]  or not a[101] ) 
 and  ( not a[590]  or not a[484] ) 
 and  ( not a[591]  or not a[484] ) 
 and  ( not a[592]  or not a[484] ) 
 and  ( not a[593]  or not a[484] ) 
 and  ( not a[485]  or not a[484] ) 
 and  ( not a[594]  or not a[484] ) 
 and  ( not a[595]  or not a[484] ) 
 and  ( not a[596]  or not a[484] ) 
 and  ( not a[590]  or not a[485] ) 
 and  ( not a[591]  or not a[485] ) 
 and  ( not a[592]  or not a[485] ) 
 and  ( not a[485]  or not a[484] ) 
 and  ( not a[593]  or not a[485] ) 
 and  ( not a[594]  or not a[485] ) 
 and  ( not a[595]  or not a[485] ) 
 and  ( not a[596]  or not a[485] ) 
 and  ( not a[597]  or not a[339] ) 
 and  ( not a[597]  or not a[101] ) 
 and  ( not a[598]  or not a[597] ) 
 and  ( not a[599]  or  a[339] ) 
 and  ( not a[600]  or  a[96]  or  a[97]  or  a[99]  or  a[100] ) 
 and  ( not a[601]  or not a[600] ) 
 and  ( not a[602]  or not a[600] ) 
 and  ( not a[603]  or not a[600] ) 
 and  ( not a[604]  or not a[600] ) 
 and  ( not a[600]  or not a[98] ) 
 and  ( not a[605]  or not a[600] ) 
 and  ( not a[606]  or not a[600] ) 
 and  ( not a[607]  or not a[96] ) 
 and  ( not a[608]  or not a[96] ) 
 and  ( not a[609]  or not a[96] ) 
 and  ( not a[610]  or not a[96] ) 
 and  ( not a[611]  or not a[96] ) 
 and  ( not a[612]  or not a[96] ) 
 and  ( not a[97]  or not a[96] ) 
 and  ( not a[613]  or not a[96] ) 
 and  ( not a[614]  or not a[96] ) 
 and  ( not a[615]  or not a[96] ) 
 and  ( not a[616]  or not a[96] ) 
 and  ( not a[99]  or not a[96] ) 
 and  ( not a[100]  or not a[96] ) 
 and  ( not a[101]  or not a[96] ) 
 and  ( not a[617]  or not a[96] ) 
 and  ( not a[607]  or not a[97] ) 
 and  ( not a[608]  or not a[97] ) 
 and  ( not a[609]  or not a[97] ) 
 and  ( not a[610]  or not a[97] ) 
 and  ( not a[611]  or not a[97] ) 
 and  ( not a[612]  or not a[97] ) 
 and  ( not a[97]  or not a[96] ) 
 and  ( not a[613]  or not a[97] ) 
 and  ( not a[614]  or not a[97] ) 
 and  ( not a[615]  or not a[97] ) 
 and  ( not a[616]  or not a[97] ) 
 and  ( not a[99]  or not a[97] ) 
 and  ( not a[100]  or not a[97] ) 
 and  ( not a[101]  or not a[97] ) 
 and  ( not a[617]  or not a[97] ) 
 and  ( not a[99]  or  a[126]  or  a[133]  or  a[146] ) 
 and  ( not a[404]  or not a[99]  or  a[484]  or  a[485] ) 
 and  ( not a[607]  or not a[99] ) 
 and  ( not a[608]  or not a[99] ) 
 and  ( not a[609]  or not a[99] ) 
 and  ( not a[610]  or not a[99] ) 
 and  ( not a[611]  or not a[99] ) 
 and  ( not a[612]  or not a[99] ) 
 and  ( not a[99]  or not a[96] ) 
 and  ( not a[99]  or not a[97] ) 
 and  ( not a[613]  or not a[99] ) 
 and  ( not a[614]  or not a[99] ) 
 and  ( not a[615]  or not a[99] ) 
 and  ( not a[100]  or not a[99] ) 
 and  ( not a[101]  or not a[99] ) 
 and  ( not a[99]  or not a[98] ) 
 and  ( not a[617]  or not a[99] ) 
 and  ( not a[404]  or not a[100]  or  a[484]  or  a[485] ) 
 and  ( not a[607]  or not a[100] ) 
 and  ( not a[608]  or not a[100] ) 
 and  ( not a[609]  or not a[100] ) 
 and  ( not a[610]  or not a[100] ) 
 and  ( not a[611]  or not a[100] ) 
 and  ( not a[612]  or not a[100] ) 
 and  ( not a[100]  or not a[96] ) 
 and  ( not a[100]  or not a[97] ) 
 and  ( not a[613]  or not a[100] ) 
 and  ( not a[614]  or not a[100] ) 
 and  ( not a[615]  or not a[100] ) 
 and  ( not a[100]  or not a[99] ) 
 and  ( not a[101]  or not a[100] ) 
 and  ( not a[100]  or not a[98] ) 
 and  ( not a[101]  or  a[339] ) 
 and  ( not a[101]  or  a[599] ) 
 and  ( not a[101]  or  a[485] ) 
 and  ( not a[101]  or  a[578]  or  a[618]  or  a[619] ) 
 and  ( not a[101]  or  a[578]  or  a[618]  or  a[620] ) 
 and  ( not a[573]  or not a[101] ) 
 and  ( not a[597]  or not a[101] ) 
 and  ( not a[484]  or not a[101] ) 
 and  ( not a[621]  or not a[101] ) 
 and  ( not a[450]  or not a[101] ) 
 and  ( not a[451]  or not a[101] ) 
 and  ( not a[607]  or not a[101] ) 
 and  ( not a[608]  or not a[101] ) 
 and  ( not a[609]  or not a[101] ) 
 and  ( not a[610]  or not a[101] ) 
 and  ( not a[611]  or not a[101] ) 
 and  ( not a[612]  or not a[101] ) 
 and  ( not a[101]  or not a[96] ) 
 and  ( not a[101]  or not a[97] ) 
 and  ( not a[613]  or not a[101] ) 
 and  ( not a[614]  or not a[101] ) 
 and  ( not a[615]  or not a[101] ) 
 and  ( not a[101]  or not a[99] ) 
 and  ( not a[101]  or not a[100] ) 
 and  ( not a[101]  or not a[98] ) 
 and  ( not a[605]  or not a[101] ) 
 and  ( not a[617]  or not a[101] ) 
 and  ( not a[98]  or  a[96]  or  a[97] ) 
 and  ( not a[601]  or not a[98] ) 
 and  ( not a[600]  or not a[98] ) 
 and  ( not a[604]  or not a[98] ) 
 and  ( not a[605]  or not a[98] ) 
 and  ( not a[606]  or not a[98] ) 
 and  ( not a[605]  or  a[96]  or  a[97]  or  a[99]  or  a[100] ) 
 and  ( not a[605]  or not a[339]  or  a[96]  or  a[97]  or  a[100] ) 
 and  ( not a[605]  or not a[601] ) 
 and  ( not a[605]  or not a[600] ) 
 and  ( not a[605]  or not a[604] ) 
 and  ( not a[605]  or not a[98] ) 
 and  ( not a[606]  or not a[605] ) 
 and  ( not a[576]  or not a[530] ) 
 and  ( not a[622]  or not a[530]  or not a[101] ) 
 and  ( not a[623]  or not a[530] ) 
 and  ( not a[624]  or not a[530] ) 
 and  ( not a[625]  or not a[530] ) 
 and  ( not a[626]  or not a[530] ) 
 and  ( not a[627]  or not a[530] ) 
 and  ( not a[628]  or not a[530] ) 
 and  ( not a[629]  or not a[530] ) 
 and  ( not a[630]  or not a[530] ) 
 and  ( not a[631]  or not a[530] ) 
 and  ( not a[632]  or not a[530] ) 
 and  ( not a[633]  or not a[530] ) 
 and  ( not a[634]  or not a[530] ) 
 and  ( not a[620]  or not a[618] ) 
 and  ( not a[621]  or not a[620] ) 
 and  ( not a[635]  or not a[620] ) 
 and  ( not a[636]  or not a[620] ) 
 and  ( not a[637]  or not a[620] ) 
 and  ( not a[638]  or not a[620] ) 
 and  ( not a[639]  or  a[640]  or  a[641]  or  a[642]  or  a[643]  or  a[644]  or  a[645]  or  a[646] ) 
 and  ( not a[647]  or not a[639] ) 
 and  ( not a[647]  or not a[640] ) 
 and  ( not a[647]  or not a[641] ) 
 and  ( not a[648]  or not a[647] ) 
 and  ( not a[647]  or not a[642] ) 
 and  ( not a[647]  or not a[643] ) 
 and  ( not a[647]  or not a[644] ) 
 and  ( not a[649]  or not a[647] ) 
 and  ( not a[650]  or not a[647] ) 
 and  ( not a[647]  or not a[645] ) 
 and  ( not a[647]  or not a[646] ) 
 and  ( not a[640]  or not a[619] ) 
 and  ( not a[640]  or not a[618] ) 
 and  ( not a[640]  or not a[621] ) 
 and  ( not a[640]  or not a[620] ) 
 and  ( not a[647]  or not a[640] ) 
 and  ( not a[641]  or not a[640] ) 
 and  ( not a[648]  or not a[640] ) 
 and  ( not a[642]  or not a[640] ) 
 and  ( not a[643]  or not a[640] ) 
 and  ( not a[644]  or not a[640] ) 
 and  ( not a[649]  or not a[640] ) 
 and  ( not a[650]  or not a[640] ) 
 and  ( not a[645]  or not a[640] ) 
 and  ( not a[646]  or not a[640] ) 
 and  ( not a[641]  or not a[578]  or  a[620] ) 
 and  ( not a[647]  or not a[641] ) 
 and  ( not a[641]  or not a[640] ) 
 and  ( not a[648]  or not a[641] ) 
 and  ( not a[642]  or not a[641] ) 
 and  ( not a[643]  or not a[641] ) 
 and  ( not a[644]  or not a[641] ) 
 and  ( not a[649]  or not a[641] ) 
 and  ( not a[650]  or not a[641] ) 
 and  ( not a[645]  or not a[641] ) 
 and  ( not a[646]  or not a[641] ) 
 and  ( not a[642]  or not a[619]  or  a[620] ) 
 and  ( not a[642]  or not a[618] ) 
 and  ( not a[642]  or not a[621] ) 
 and  ( not a[647]  or not a[642] ) 
 and  ( not a[642]  or not a[640] ) 
 and  ( not a[642]  or not a[641] ) 
 and  ( not a[648]  or not a[642] ) 
 and  ( not a[643]  or not a[642] ) 
 and  ( not a[644]  or not a[642] ) 
 and  ( not a[649]  or not a[642] ) 
 and  ( not a[650]  or not a[642] ) 
 and  ( not a[645]  or not a[642] ) 
 and  ( not a[646]  or not a[642] ) 
 and  ( not a[643]  or  a[619]  or  a[621] ) 
 and  ( not a[643]  or not a[620]  or  a[621] ) 
 and  ( not a[647]  or not a[643] ) 
 and  ( not a[643]  or not a[640] ) 
 and  ( not a[643]  or not a[641] ) 
 and  ( not a[648]  or not a[643] ) 
 and  ( not a[643]  or not a[642] ) 
 and  ( not a[644]  or not a[643] ) 
 and  ( not a[649]  or not a[643] ) 
 and  ( not a[650]  or not a[643] ) 
 and  ( not a[645]  or not a[643] ) 
 and  ( not a[646]  or not a[643] ) 
 and  ( not a[644]  or not a[619] ) 
 and  ( not a[644]  or not a[621] ) 
 and  ( not a[644]  or not a[620] ) 
 and  ( not a[647]  or not a[644] ) 
 and  ( not a[644]  or not a[640] ) 
 and  ( not a[644]  or not a[641] ) 
 and  ( not a[648]  or not a[644] ) 
 and  ( not a[644]  or not a[642] ) 
 and  ( not a[644]  or not a[643] ) 
 and  ( not a[649]  or not a[644] ) 
 and  ( not a[650]  or not a[644] ) 
 and  ( not a[645]  or not a[644] ) 
 and  ( not a[646]  or not a[644] ) 
 and  ( not a[645]  or not a[618] ) 
 and  ( not a[645]  or not a[620] ) 
 and  ( not a[647]  or not a[645] ) 
 and  ( not a[645]  or not a[640] ) 
 and  ( not a[645]  or not a[641] ) 
 and  ( not a[648]  or not a[645] ) 
 and  ( not a[645]  or not a[642] ) 
 and  ( not a[645]  or not a[643] ) 
 and  ( not a[645]  or not a[644] ) 
 and  ( not a[649]  or not a[645] ) 
 and  ( not a[650]  or not a[645] ) 
 and  ( not a[646]  or not a[645] ) 
 and  ( not a[646]  or not a[619] ) 
 and  ( not a[646]  or not a[618]  or not a[155] ) 
 and  ( not a[646]  or not a[621] ) 
 and  ( not a[646]  or not a[620] ) 
 and  ( not a[647]  or not a[646] ) 
 and  ( not a[646]  or not a[640] ) 
 and  ( not a[646]  or not a[641] ) 
 and  ( not a[648]  or not a[646] ) 
 and  ( not a[646]  or not a[642] ) 
 and  ( not a[646]  or not a[643] ) 
 and  ( not a[646]  or not a[644] ) 
 and  ( not a[649]  or not a[646] ) 
 and  ( not a[650]  or not a[646] ) 
 and  ( not a[646]  or not a[645] ) 
 and  ( not a[621]  or not a[619] ) 
 and  ( not a[619]  or not a[101]  or  a[578]  or  a[620] ) 
 and  ( not a[619]  or not a[404]  or  a[578]  or  a[620] ) 
 and  ( not a[651]  or not a[619] ) 
 and  ( not a[652]  or not a[619] ) 
 and  ( not a[653]  or not a[619] ) 
 and  ( not a[654]  or not a[619] ) 
 and  ( not a[655]  or not a[619] ) 
 and  ( not a[656]  or not a[619] ) 
 and  ( not a[657]  or not a[619] ) 
 and  ( not a[658]  or not a[619] ) 
 and  ( not a[659]  or not a[619] ) 
 and  ( not a[660]  or not a[619] ) 
 and  ( not a[661]  or not a[619] ) 
 and  ( not a[619]  or not a[618] ) 
 and  ( not a[635]  or not a[619] ) 
 and  ( not a[638]  or not a[619] ) 
 and  ( not a[662]  or not a[619] ) 
 and  ( not a[636]  or not a[619] ) 
 and  ( not a[621]  or not a[618] ) 
 and  ( not a[620]  or not a[618] ) 
 and  ( not a[618]  or not a[578] ) 
 and  ( not a[651]  or not a[618] ) 
 and  ( not a[652]  or not a[618] ) 
 and  ( not a[653]  or not a[618] ) 
 and  ( not a[654]  or not a[618] ) 
 and  ( not a[655]  or not a[618] ) 
 and  ( not a[656]  or not a[618] ) 
 and  ( not a[657]  or not a[618] ) 
 and  ( not a[658]  or not a[618] ) 
 and  ( not a[659]  or not a[618] ) 
 and  ( not a[660]  or not a[618] ) 
 and  ( not a[661]  or not a[618] ) 
 and  ( not a[619]  or not a[618] ) 
 and  ( not a[635]  or not a[618] ) 
 and  ( not a[662]  or not a[618] ) 
 and  ( not a[636]  or not a[618] ) 
 and  ( not a[638]  or not a[618] ) 
 and  ( not a[621]  or not a[101] ) 
 and  ( not a[621]  or not a[619] ) 
 and  ( not a[621]  or not a[618] ) 
 and  ( not a[621]  or not a[620] ) 
 and  ( not a[621]  or not a[404] ) 
 and  ( not a[663]  or not a[155] ) 
 and  ( not a[401]  or not a[400] ) 
 and  ( not a[401]  or  a[517] ) 
 and  ( not a[578]  or not a[401] ) 
 and  ( not a[403]  or not a[401]  or  a[484]  or  a[485] ) 
 and  ( not a[664]  or not a[401] ) 
 and  ( not a[665]  or not a[401] ) 
 and  ( not a[666]  or not a[401] ) 
 and  ( not a[667]  or not a[401] ) 
 and  ( not a[402]  or not a[401] ) 
 and  ( not a[668]  or not a[401] ) 
 and  ( not a[525]  or not a[401] ) 
 and  ( not a[517]  or not a[516] ) 
 and  ( not a[517]  or  a[401] ) 
 and  ( not a[578]  or not a[517] ) 
 and  ( not a[669]  or not a[517] ) 
 and  ( not a[670]  or not a[517] ) 
 and  ( not a[671]  or not a[517] ) 
 and  ( not a[672]  or not a[517] ) 
 and  ( not a[673]  or not a[517] ) 
 and  ( not a[674]  or not a[517] ) 
 and  ( not a[675]  or not a[517] ) 
 and  ( not a[676]  or not a[517] ) 
 and  ( not a[518]  or not a[517] ) 
 and  ( not a[519]  or not a[517] ) 
 and  ( not a[520]  or not a[517] ) 
 and  ( not a[521]  or not a[517] ) 
 and  ( not a[677]  or not a[517] ) 
 and  ( not a[522]  or not a[517] ) 
 and  ( not a[523]  or not a[517] ) 
 and  ( not a[402]  or not a[400] ) 
 and  ( not a[402]  or  a[673] ) 
 and  ( not a[403]  or not a[402]  or  a[484]  or  a[485] ) 
 and  ( not a[664]  or not a[402] ) 
 and  ( not a[666]  or not a[402] ) 
 and  ( not a[402]  or not a[401] ) 
 and  ( not a[667]  or not a[402] ) 
 and  ( not a[673]  or not a[516] ) 
 and  ( not a[673]  or  a[402] ) 
 and  ( not a[673]  or not a[669] ) 
 and  ( not a[673]  or not a[671] ) 
 and  ( not a[673]  or not a[517] ) 
 and  ( not a[673]  or not a[672] ) 
 and  ( not a[674]  or not a[673] ) 
 and  ( not a[673]  or not a[520] ) 
 and  ( not a[476]  or not a[475] ) 
 and  ( not a[678]  or not a[476] ) 
 and  ( not a[477]  or not a[476] ) 
 and  ( not a[679]  or not a[476] ) 
 and  ( not a[622]  or not a[476] ) 
 and  ( not a[476]  or not a[398]  or  a[478] ) 
 and  ( not a[476]  or not a[404]  or  a[680] ) 
 and  ( not a[476]  or not a[404]  or  a[478] ) 
 and  ( not a[476]  or not a[404]  or  a[681] ) 
 and  ( not a[682]  or not a[476] ) 
 and  ( not a[683]  or not a[476] ) 
 and  ( not a[684]  or not a[476] ) 
 and  ( not a[685]  or not a[476] ) 
 and  ( not a[686]  or not a[476] ) 
 and  ( not a[687]  or not a[476] ) 
 and  ( not a[688]  or not a[107] ) 
 and  ( not a[688]  or  a[106] ) 
 and  ( not a[689]  or not a[688] ) 
 and  ( not a[690]  or not a[688] ) 
 and  ( not a[691]  or not a[688] ) 
 and  ( not a[692]  or not a[398] ) 
 and  ( not a[693]  or not a[692] ) 
 and  ( not a[694]  or not a[692] ) 
 and  ( not a[695]  or not a[692] ) 
 and  ( not a[696]  or not a[692] ) 
 and  ( not a[697]  or not a[692] ) 
 and  ( not a[698]  or not a[692] ) 
 and  ( not a[699]  or not a[692] ) 
 and  ( not a[700]  or not a[692] ) 
 and  ( not a[701]  or not a[692] ) 
 and  ( not a[678]  or not a[622]  or  a[404] ) 
 and  ( not a[678]  or not a[622]  or  a[680] ) 
 and  ( not a[622]  or not a[530]  or not a[101] ) 
 and  ( not a[622]  or not a[476] ) 
 and  ( not a[702]  or not a[622] ) 
 and  ( not a[703]  or not a[531] ) 
 and  ( not a[706]  or not a[705] ) 
 and  ( not a[706]  or not a[398] ) 
 and  ( not a[706]  or not a[705] ) 
 and  ( not a[707]  or not a[397] ) 
 and  ( not a[398]  or not a[397] ) 
 and  ( not a[404]  or not a[397] ) 
 and  ( not a[398]  or  a[475]  or  a[477]  or  a[478] ) 
 and  ( not a[398]  or not a[397] ) 
 and  ( not a[404]  or not a[398] ) 
 and  ( not a[404]  or  a[387] ) 
 and  ( not a[404]  or  a[578]  or  a[618]  or  a[619] ) 
 and  ( not a[404]  or  a[578]  or  a[618]  or  a[620] ) 
 and  ( not a[404]  or  a[475]  or  a[477]  or  a[478] ) 
 and  ( not a[404]  or  a[692] ) 
 and  ( not a[404]  or  a[678]  or  a[680] ) 
 and  ( not a[404]  or  a[679]  or  a[681] ) 
 and  ( not a[404]  or not a[99]  or  a[484]  or  a[485] ) 
 and  ( not a[404]  or not a[100]  or  a[484]  or  a[485] ) 
 and  ( not a[404]  or not a[397] ) 
 and  ( not a[404]  or not a[398] ) 
 and  ( not a[709]  or not a[708] ) 
 and  ( not a[710]  or  a[708] ) 
 and  ( not a[536]  or not a[535] ) 
 and  ( not a[536]  or not a[535] ) 
 and  ( not a[712]  or not a[711] ) 
 and  ( not a[713]  or not a[711] ) 
 and  ( not a[714]  or not a[711] ) 
 and  ( not a[715]  or not a[711] ) 
 and  ( not a[716]  or not a[711] ) 
 and  ( not a[717]  or not a[711] ) 
 and  ( not a[718]  or not a[711] ) 
 and  ( not a[719]  or not a[711] ) 
 and  ( not a[720]  or not a[711] ) 
 and  ( not a[721]  or not a[711] ) 
 and  ( not a[722]  or not a[711] ) 
 and  ( not a[714]  or not a[712] ) 
 and  ( not a[714]  or not a[713] ) 
 and  ( not a[714]  or not a[711] ) 
 and  ( not a[715]  or not a[714] ) 
 and  ( not a[716]  or not a[714] ) 
 and  ( not a[717]  or not a[714] ) 
 and  ( not a[718]  or not a[714] ) 
 and  ( not a[719]  or not a[714] ) 
 and  ( not a[720]  or not a[714] ) 
 and  ( not a[721]  or not a[714] ) 
 and  ( not a[722]  or not a[714] ) 
 and  ( not a[715]  or not a[712] ) 
 and  ( not a[715]  or not a[713] ) 
 and  ( not a[715]  or not a[711] ) 
 and  ( not a[715]  or not a[714] ) 
 and  ( not a[716]  or not a[715] ) 
 and  ( not a[717]  or not a[715] ) 
 and  ( not a[718]  or not a[715] ) 
 and  ( not a[719]  or not a[715] ) 
 and  ( not a[720]  or not a[715] ) 
 and  ( not a[721]  or not a[715] ) 
 and  ( not a[722]  or not a[715] ) 
 and  ( not a[716]  or not a[712] ) 
 and  ( not a[716]  or not a[713] ) 
 and  ( not a[716]  or not a[711] ) 
 and  ( not a[716]  or not a[714] ) 
 and  ( not a[716]  or not a[715] ) 
 and  ( not a[717]  or not a[716] ) 
 and  ( not a[718]  or not a[716] ) 
 and  ( not a[719]  or not a[716] ) 
 and  ( not a[720]  or not a[716] ) 
 and  ( not a[721]  or not a[716] ) 
 and  ( not a[722]  or not a[716] ) 
 and  ( not a[717]  or not a[712] ) 
 and  ( not a[717]  or not a[713] ) 
 and  ( not a[717]  or not a[711] ) 
 and  ( not a[717]  or not a[714] ) 
 and  ( not a[717]  or not a[715] ) 
 and  ( not a[717]  or not a[716] ) 
 and  ( not a[718]  or not a[717] ) 
 and  ( not a[719]  or not a[717] ) 
 and  ( not a[720]  or not a[717] ) 
 and  ( not a[721]  or not a[717] ) 
 and  ( not a[722]  or not a[717] ) 
 and  ( not a[718]  or not a[712] ) 
 and  ( not a[718]  or not a[713] ) 
 and  ( not a[718]  or not a[711] ) 
 and  ( not a[718]  or not a[714] ) 
 and  ( not a[718]  or not a[715] ) 
 and  ( not a[718]  or not a[716] ) 
 and  ( not a[718]  or not a[717] ) 
 and  ( not a[719]  or not a[718] ) 
 and  ( not a[720]  or not a[718] ) 
 and  ( not a[721]  or not a[718] ) 
 and  ( not a[722]  or not a[718] ) 
 and  ( not a[719]  or not a[712] ) 
 and  ( not a[719]  or not a[713] ) 
 and  ( not a[719]  or not a[711] ) 
 and  ( not a[719]  or not a[714] ) 
 and  ( not a[719]  or not a[715] ) 
 and  ( not a[719]  or not a[716] ) 
 and  ( not a[719]  or not a[717] ) 
 and  ( not a[719]  or not a[718] ) 
 and  ( not a[720]  or not a[719] ) 
 and  ( not a[721]  or not a[719] ) 
 and  ( not a[722]  or not a[719] ) 
 and  ( not a[720]  or not a[712] ) 
 and  ( not a[720]  or not a[713] ) 
 and  ( not a[720]  or not a[711] ) 
 and  ( not a[720]  or not a[714] ) 
 and  ( not a[720]  or not a[715] ) 
 and  ( not a[720]  or not a[716] ) 
 and  ( not a[720]  or not a[717] ) 
 and  ( not a[720]  or not a[718] ) 
 and  ( not a[720]  or not a[719] ) 
 and  ( not a[721]  or not a[720] ) 
 and  ( not a[722]  or not a[720] ) 
 and  ( not a[721]  or not a[712] ) 
 and  ( not a[721]  or not a[713] ) 
 and  ( not a[721]  or not a[711] ) 
 and  ( not a[721]  or not a[714] ) 
 and  ( not a[721]  or not a[715] ) 
 and  ( not a[721]  or not a[716] ) 
 and  ( not a[721]  or not a[717] ) 
 and  ( not a[721]  or not a[718] ) 
 and  ( not a[721]  or not a[719] ) 
 and  ( not a[721]  or not a[720] ) 
 and  ( not a[722]  or not a[721] ) 
 and  ( not a[731]  or not a[730] ) 
 and  ( not a[731]  or not a[730] ) 
 and  ( not a[733]  or not a[732] ) 
 and  ( not a[734]  or not a[732] ) 
 and  ( not a[735]  or not a[732] ) 
 and  ( not a[663]  or not a[155] ) 
 and  ( not a[678]  or  a[406] ) 
 and  ( not a[678]  or  a[485] ) 
 and  ( not a[678]  or not a[476] ) 
 and  ( not a[678]  or not a[622] ) 
 and  ( not a[680]  or not a[678] ) 
 and  ( not a[477]  or not a[475] ) 
 and  ( not a[477]  or not a[476] ) 
 and  ( not a[478]  or not a[477] ) 
 and  ( not a[679]  or not a[476] ) 
 and  ( not a[681]  or not a[679] ) 
 and  ( not a[680]  or  a[476]  or  a[622] ) 
 and  ( not a[680]  or  a[404] ) 
 and  ( not a[680]  or not a[678] ) 
 and  ( not a[478]  or  a[398]  or  a[404] ) 
 and  ( not a[478]  or not a[475] ) 
 and  ( not a[478]  or not a[477] ) 
 and  ( not a[681]  or  a[476] ) 
 and  ( not a[681]  or  a[404] ) 
 and  ( not a[681]  or not a[679] ) 
 and  ( not a[736]  or  a[534] ) 
 and  ( not a[738]  or  a[129] ) 
 and  ( not a[740]  or not a[106]  or  a[97]  or  a[100] ) 
 and  ( not a[740]  or not a[106]  or  a[723] ) 
 and  ( not a[740]  or not a[106]  or  a[253] ) 
 and  ( not a[740]  or not a[107] ) 
 and  ( not a[740]  or  a[106] ) 
 and  ( not a[578]  or not a[106] ) 
 and  ( not a[618]  or not a[578]  or not a[107] ) 
 and  ( not a[578]  or not a[401]  or not a[107] ) 
 and  ( not a[578]  or not a[517]  or not a[107] ) 
 and  ( not a[578]  or not a[107]  or  a[577] ) 
 and  ( not a[578]  or not a[107]  or  a[100]  or  a[101] ) 
 and  ( not a[578]  or not a[107]  or  a[100]  or  a[404] ) 
 and  ( not a[578]  or not a[404]  or not a[107]  or  a[101] ) 
 and  ( not a[578]  or not a[107]  or  a[619] ) 
 and  ( not a[578]  or not a[107]  or  a[292] ) 
 and  ( not a[578]  or  a[107] ) 
 and  ( not a[573]  or not a[450]  or not a[106] ) 
 and  ( not a[450]  or not a[431]  or not a[106] ) 
 and  ( not a[450]  or not a[106]  or not a[101] ) 
 and  ( not a[450]  or not a[107] ) 
 and  ( not a[450]  or  a[106] ) 
 and  ( not a[451]  or not a[450] ) 
 and  ( not a[573]  or not a[451] ) 
 and  ( not a[451]  or not a[431] ) 
 and  ( not a[451]  or not a[101] ) 
 and  ( not a[451]  or not a[450] ) 
 and  ( not a[741]  or not a[106] ) 
 and  ( not a[741]  or  a[107] ) 
 and  (  a[72]  or  a[73]  or  a[74]  or  a[75]  or  a[76]  or  a[77]  or  a[78]  or  a[79]  or  a[80]  or  a[81]  or  a[82]  or  a[83]  or  a[84]  or  a[85]  or  a[86]  or  a[87]  or  a[88]  or  a[89]  or  a[90]  or  a[91] ) 
 and  (  a[99]  or  a[100]  or  a[101]  or  a[338]  or  a[339]  or  a[340]  or  a[341]  or  a[342]  or  a[343]  or  a[344]  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]  or  a[360]  or  a[361]  or  a[362]  or  a[363]  or  a[364]  or  a[365]  or  a[366]  or  a[367]  or  a[368]  or  a[369]  or  a[370]  or  a[371] ) 
 and  ( not a[99]  or  a[338]  or  a[339]  or  a[340]  or  a[341]  or  a[342]  or  a[343]  or  a[344]  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]  or  a[360]  or  a[361]  or  a[362]  or  a[363]  or  a[364]  or  a[365]  or  a[366]  or  a[367]  or  a[368]  or  a[369]  or  a[370]  or  a[371] ) 
 and  ( not a[100]  or  a[338]  or  a[339]  or  a[340]  or  a[341]  or  a[342]  or  a[343]  or  a[344]  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]  or  a[360]  or  a[361]  or  a[362]  or  a[363]  or  a[364]  or  a[365]  or  a[366]  or  a[367]  or  a[368]  or  a[369]  or  a[370]  or  a[371] ) 
 and  ( not a[101]  or  a[338]  or  a[340]  or  a[341]  or  a[342]  or  a[343]  or  a[344]  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]  or  a[360]  or  a[361]  or  a[362]  or  a[363]  or  a[364]  or  a[365]  or  a[366]  or  a[367]  or  a[368]  or  a[369]  or  a[370]  or  a[371] ) 
 and  ( not a[339]  or not a[99]  or  a[338]  or  a[340]  or  a[341]  or  a[342]  or  a[343]  or  a[344]  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]  or  a[360]  or  a[361]  or  a[362]  or  a[363]  or  a[364]  or  a[365]  or  a[366]  or  a[367]  or  a[368]  or  a[369]  or  a[370]  or  a[371] ) 
 and  ( not a[339]  or not a[100]  or  a[338]  or  a[340]  or  a[341]  or  a[342]  or  a[343]  or  a[344]  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]  or  a[360]  or  a[361]  or  a[362]  or  a[363]  or  a[364]  or  a[365]  or  a[366]  or  a[367]  or  a[368]  or  a[369]  or  a[370]  or  a[371] ) 
 and  ( not a[339]  or not a[96]  or  a[99]  or  a[100]  or  a[101]  or  a[338]  or  a[340]  or  a[341]  or  a[342]  or  a[343]  or  a[344]  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]  or  a[360]  or  a[361]  or  a[362]  or  a[363]  or  a[364]  or  a[365]  or  a[366]  or  a[367]  or  a[368]  or  a[369]  or  a[370]  or  a[371] ) 
 and  ( not a[339]  or not a[97]  or  a[99]  or  a[100]  or  a[101]  or  a[338]  or  a[340]  or  a[341]  or  a[342]  or  a[343]  or  a[344]  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]  or  a[360]  or  a[361]  or  a[362]  or  a[363]  or  a[364]  or  a[365]  or  a[366]  or  a[367]  or  a[368]  or  a[369]  or  a[370]  or  a[371] ) 
 and  ( not a[404]  or  a[387] ) 
 and  ( not a[101]  or  a[96]  or  a[97]  or  a[99]  or  a[100]  or  a[339]  or  a[403]  or  a[486]  or  a[487]  or  a[488]  or  a[489]  or  a[490]  or  a[491]  or  a[492]  or  a[493]  or  a[494]  or  a[495]  or  a[496]  or  a[497]  or  a[498]  or  a[499]  or  a[500]  or  a[501]  or  a[502] ) 
 and  ( not a[101]  or  a[99]  or  a[100]  or  a[339]  or  a[403]  or  a[404]  or  a[486]  or  a[487]  or  a[488]  or  a[489]  or  a[490]  or  a[491]  or  a[492]  or  a[493]  or  a[494]  or  a[495]  or  a[496]  or  a[497]  or  a[498]  or  a[499]  or  a[500]  or  a[501]  or  a[502] ) 
 and  ( not a[484]  or not a[403]  or not a[101]  or  a[339]  or  a[486]  or  a[487]  or  a[488]  or  a[489]  or  a[490]  or  a[491]  or  a[492]  or  a[493]  or  a[494]  or  a[495]  or  a[496]  or  a[497]  or  a[498]  or  a[499]  or  a[500]  or  a[501]  or  a[502] ) 
 and  ( not a[485]  or not a[403]  or not a[101]  or  a[339]  or  a[486]  or  a[487]  or  a[488]  or  a[489]  or  a[490]  or  a[491]  or  a[492]  or  a[493]  or  a[494]  or  a[495]  or  a[496]  or  a[497]  or  a[498]  or  a[499]  or  a[500]  or  a[501]  or  a[502] ) 
 and  ( not a[484]  or not a[404]  or not a[101]  or not a[96]  or  a[339]  or  a[486]  or  a[487]  or  a[488]  or  a[489]  or  a[490]  or  a[491]  or  a[492]  or  a[493]  or  a[494]  or  a[495]  or  a[496]  or  a[497]  or  a[498]  or  a[499]  or  a[500]  or  a[501]  or  a[502] ) 
 and  ( not a[485]  or not a[404]  or not a[101]  or not a[96]  or  a[339]  or  a[486]  or  a[487]  or  a[488]  or  a[489]  or  a[490]  or  a[491]  or  a[492]  or  a[493]  or  a[494]  or  a[495]  or  a[496]  or  a[497]  or  a[498]  or  a[499]  or  a[500]  or  a[501]  or  a[502] ) 
 and  ( not a[484]  or not a[404]  or not a[101]  or not a[97]  or  a[339]  or  a[486]  or  a[487]  or  a[488]  or  a[489]  or  a[490]  or  a[491]  or  a[492]  or  a[493]  or  a[494]  or  a[495]  or  a[496]  or  a[497]  or  a[498]  or  a[499]  or  a[500]  or  a[501]  or  a[502] ) 
 and  ( not a[485]  or not a[404]  or not a[101]  or not a[97]  or  a[339]  or  a[486]  or  a[487]  or  a[488]  or  a[489]  or  a[490]  or  a[491]  or  a[492]  or  a[493]  or  a[494]  or  a[495]  or  a[496]  or  a[497]  or  a[498]  or  a[499]  or  a[500]  or  a[501]  or  a[502] ) 
 and  ( not a[484]  or not a[101]  or not a[99]  or  a[339]  or  a[486]  or  a[487]  or  a[488]  or  a[489]  or  a[490]  or  a[491]  or  a[492]  or  a[493]  or  a[494]  or  a[495]  or  a[496]  or  a[497]  or  a[498]  or  a[499]  or  a[500]  or  a[501]  or  a[502] ) 
 and  ( not a[485]  or not a[101]  or not a[99]  or  a[339]  or  a[486]  or  a[487]  or  a[488]  or  a[489]  or  a[490]  or  a[491]  or  a[492]  or  a[493]  or  a[494]  or  a[495]  or  a[496]  or  a[497]  or  a[498]  or  a[499]  or  a[500]  or  a[501]  or  a[502] ) 
 and  ( not a[484]  or not a[101]  or not a[100]  or  a[339]  or  a[486]  or  a[487]  or  a[488]  or  a[489]  or  a[490]  or  a[491]  or  a[492]  or  a[493]  or  a[494]  or  a[495]  or  a[496]  or  a[497]  or  a[498]  or  a[499]  or  a[500]  or  a[501]  or  a[502] ) 
 and  ( not a[485]  or not a[101]  or not a[100]  or  a[339]  or  a[486]  or  a[487]  or  a[488]  or  a[489]  or  a[490]  or  a[491]  or  a[492]  or  a[493]  or  a[494]  or  a[495]  or  a[496]  or  a[497]  or  a[498]  or  a[499]  or  a[500]  or  a[501]  or  a[502] ) 
 and  (  a[95]  or  a[102]  or  a[103]  or  a[105]  or  a[108]  or  a[109]  or  a[110]  or  a[111]  or  a[112]  or  a[113]  or  a[114]  or  a[115]  or  a[116]  or  a[117]  or  a[118]  or  a[119]  or  a[120]  or  a[121]  or  a[122]  or  a[123]  or  a[124]  or  a[125]  or  a[126]  or  a[127]  or  a[128]  or  a[129]  or  a[131]  or  a[132]  or  a[133]  or  a[134]  or  a[135]  or  a[136]  or  a[137]  or  a[138]  or  a[139]  or  a[140]  or  a[141]  or  a[142]  or  a[143]  or  a[144]  or  a[145]  or  a[146]  or  a[147]  or  a[148]  or  a[149]  or  a[150]  or  a[151]  or  a[152]  or  a[153]  or  a[154]  or  a[156]  or  a[157]  or  a[158]  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]  or  a[171]  or  a[172]  or  a[173]  or  a[174]  or  a[175]  or  a[176]  or  a[177]  or  a[178]  or  a[179]  or  a[180]  or  a[181]  or  a[182]  or  a[183]  or  a[184]  or  a[185]  or  a[186]  or  a[187]  or  a[188]  or  a[189]  or  a[190]  or  a[191]  or  a[192]  or  a[193]  or  a[194]  or  a[195]  or  a[196]  or  a[197]  or  a[198]  or  a[199]  or  a[200]  or  a[201]  or  a[202]  or  a[203]  or  a[204]  or  a[205]  or  a[206]  or  a[207]  or  a[208]  or  a[209]  or  a[210]  or  a[211]  or  a[212]  or  a[213]  or  a[214]  or  a[215]  or  a[216]  or  a[218]  or  a[219]  or  a[221]  or  a[222]  or  a[223]  or  a[224]  or  a[225]  or  a[226]  or  a[227]  or  a[228]  or  a[229]  or  a[230]  or  a[231]  or  a[232]  or  a[233]  or  a[234]  or  a[235]  or  a[236]  or  a[237]  or  a[238]  or  a[239]  or  a[240]  or  a[241]  or  a[242]  or  a[243]  or  a[245]  or  a[246]  or  a[247]  or  a[248]  or  a[249]  or  a[250]  or  a[251]  or  a[252]  or  a[253]  or  a[254]  or  a[255]  or  a[256]  or  a[257]  or  a[258]  or  a[259]  or  a[260]  or  a[261]  or  a[262]  or  a[263]  or  a[264]  or  a[265]  or  a[266]  or  a[269]  or  a[270]  or  a[271]  or  a[272]  or  a[273]  or  a[274]  or  a[275]  or  a[276]  or  a[277]  or  a[278]  or  a[279]  or  a[280]  or  a[281]  or  a[282]  or  a[283]  or  a[284]  or  a[285]  or  a[286]  or  a[287]  or  a[288]  or  a[289]  or  a[290]  or  a[291]  or  a[292]  or  a[293]  or  a[294]  or  a[295]  or  a[296]  or  a[297]  or  a[298]  or  a[299]  or  a[300]  or  a[301]  or  a[302]  or  a[303]  or  a[304]  or  a[305]  or  a[306]  or  a[307]  or  a[308]  or  a[309]  or  a[310]  or  a[311]  or  a[312]  or  a[313]  or  a[314]  or  a[315]  or  a[317]  or  a[318]  or  a[319]  or  a[320]  or  a[321]  or  a[322]  or  a[323]  or  a[324]  or  a[325]  or  a[326]  or  a[327]  or  a[328]  or  a[329]  or  a[330]  or  a[331]  or  a[332]  or  a[333]  or  a[334]  or  a[335]  or  a[336]  or  a[534]  or  a[537]  or  a[538]  or  a[539]  or  a[540]  or  a[541]  or  a[542]  or  a[543]  or  a[544]  or  a[545]  or  a[546]  or  a[547]  or  a[548]  or  a[549]  or  a[550]  or  a[551]  or  a[552]  or  a[553]  or  a[554]  or  a[555] ) 
 and  (  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]  or  a[34]  or  a[35]  or  a[36]  or  a[37]  or  a[38]  or  a[39]  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]  or  a[50]  or  a[51]  or  a[56]  or  a[57]  or  a[58]  or  a[59]  or  a[63]  or  a[65]  or  a[66]  or  a[67]  or  a[68]  or  a[69]  or  a[70]  or  a[92]  or  a[93]  or  a[94]  or  a[534]  or  a[537]  or  a[538]  or  a[556]  or  a[557]  or  a[558]  or  a[559]  or  a[560]  or  a[561]  or  a[562]  or  a[563]  or  a[564] ) 
 and  ( not a[578]  or not a[107]  or  a[577] ) 
 and  ( not a[101]  or  a[484]  or  a[485]  or  a[590]  or  a[591]  or  a[592]  or  a[593]  or  a[594]  or  a[595]  or  a[596] ) 
 and  ( not a[339]  or not a[101]  or  a[599] ) 
 and  (  a[96]  or  a[97]  or  a[99]  or  a[100]  or  a[101]  or  a[607]  or  a[608]  or  a[609]  or  a[610]  or  a[611]  or  a[612]  or  a[613]  or  a[614]  or  a[615]  or  a[616]  or  a[617] ) 
 and  ( not a[578]  or  a[96]  or  a[97]  or  a[98]  or  a[99]  or  a[100]  or  a[101]  or  a[404]  or  a[607]  or  a[608]  or  a[609]  or  a[610]  or  a[611]  or  a[612]  or  a[613]  or  a[614]  or  a[615] ) 
 and  ( not a[599]  or not a[578]  or not a[485]  or not a[404]  or not a[339]  or  a[96]  or  a[97]  or  a[98]  or  a[99]  or  a[100]  or  a[101]  or  a[450]  or  a[451]  or  a[484]  or  a[573]  or  a[597]  or  a[605]  or  a[607]  or  a[608]  or  a[609]  or  a[610]  or  a[611]  or  a[612]  or  a[613]  or  a[614]  or  a[615]  or  a[617]  or  a[621] ) 
 and  ( not a[534]  or not a[96]  or  a[98]  or  a[99]  or  a[100]  or  a[101]  or  a[600]  or  a[601]  or  a[604]  or  a[605]  or  a[606] ) 
 and  ( not a[534]  or not a[97]  or  a[98]  or  a[99]  or  a[100]  or  a[101]  or  a[600]  or  a[601]  or  a[604]  or  a[605]  or  a[606] ) 
 and  ( not a[96]  or not a[95]  or  a[98]  or  a[99]  or  a[100]  or  a[101]  or  a[600]  or  a[601]  or  a[604]  or  a[605]  or  a[606] ) 
 and  ( not a[97]  or not a[95]  or  a[98]  or  a[99]  or  a[100]  or  a[101]  or  a[600]  or  a[601]  or  a[604]  or  a[605]  or  a[606] ) 
 and  ( not a[103]  or not a[96]  or  a[98]  or  a[99]  or  a[100]  or  a[101]  or  a[600]  or  a[601]  or  a[604]  or  a[605]  or  a[606] ) 
 and  ( not a[103]  or not a[97]  or  a[98]  or  a[99]  or  a[100]  or  a[101]  or  a[600]  or  a[601]  or  a[604]  or  a[605]  or  a[606] ) 
 and  (  a[578]  or  a[640]  or  a[641]  or  a[642]  or  a[643]  or  a[644]  or  a[645]  or  a[646]  or  a[647]  or  a[648]  or  a[649]  or  a[650] ) 
 and  ( not a[620]  or  a[640]  or  a[641]  or  a[642]  or  a[643]  or  a[644]  or  a[645]  or  a[646]  or  a[647]  or  a[648]  or  a[649]  or  a[650] ) 
 and  ( not a[619]  or not a[578]  or  a[620]  or  a[640]  or  a[641]  or  a[642]  or  a[643]  or  a[644]  or  a[645]  or  a[646]  or  a[647]  or  a[648]  or  a[649]  or  a[650] ) 
 and  ( not a[621]  or not a[578]  or  a[620]  or  a[640]  or  a[641]  or  a[642]  or  a[643]  or  a[644]  or  a[645]  or  a[646]  or  a[647]  or  a[648]  or  a[649]  or  a[650] ) 
 and  ( not a[578]  or  a[618]  or  a[619]  or  a[621]  or  a[635]  or  a[636]  or  a[638]  or  a[651]  or  a[652]  or  a[653]  or  a[654]  or  a[655]  or  a[656]  or  a[657]  or  a[658]  or  a[659]  or  a[660]  or  a[661]  or  a[662] ) 
 and  ( not a[101]  or  a[578]  or  a[618]  or  a[619]  or  a[620]  or  a[621]  or  a[635]  or  a[636]  or  a[638]  or  a[651]  or  a[652]  or  a[653]  or  a[654]  or  a[655]  or  a[656]  or  a[657]  or  a[658]  or  a[659]  or  a[660]  or  a[661]  or  a[662] ) 
 and  ( not a[404]  or  a[578]  or  a[618]  or  a[619]  or  a[620]  or  a[621]  or  a[635]  or  a[636]  or  a[638]  or  a[651]  or  a[652]  or  a[653]  or  a[654]  or  a[655]  or  a[656]  or  a[657]  or  a[658]  or  a[659]  or  a[660]  or  a[661]  or  a[662] ) 
 and  ( not a[404]  or  a[398]  or  a[692]  or  a[693]  or  a[694]  or  a[695]  or  a[696]  or  a[697]  or  a[698]  or  a[699]  or  a[700]  or  a[701] ) 
 and  (  a[101]  or  a[397]  or  a[398]  or  a[404]  or  a[707] ) 
 and  (  a[397]  or  a[398]  or  a[404]  or  a[578]  or  a[707] ) 
 and  ( not a[692]  or not a[679]  or not a[678]  or not a[578]  or not a[477]  or not a[387]  or not a[101]  or  a[397]  or  a[398]  or  a[404] ) 
 and  ( not a[692]  or not a[681]  or not a[678]  or not a[578]  or not a[477]  or not a[387]  or not a[101]  or  a[397]  or  a[398]  or  a[404] ) 
 and  ( not a[692]  or not a[680]  or not a[679]  or not a[578]  or not a[477]  or not a[387]  or not a[101]  or  a[397]  or  a[398]  or  a[404] ) 
 and  ( not a[692]  or not a[681]  or not a[680]  or not a[578]  or not a[477]  or not a[387]  or not a[101]  or  a[397]  or  a[398]  or  a[404] ) 
 and  ( not a[692]  or not a[679]  or not a[678]  or not a[578]  or not a[478]  or not a[387]  or not a[101]  or  a[397]  or  a[398]  or  a[404] ) 
 and  ( not a[692]  or not a[681]  or not a[678]  or not a[578]  or not a[478]  or not a[387]  or not a[101]  or  a[397]  or  a[398]  or  a[404] ) 
 and  ( not a[692]  or not a[680]  or not a[679]  or not a[578]  or not a[478]  or not a[387]  or not a[101]  or  a[397]  or  a[398]  or  a[404] ) 
 and  ( not a[692]  or not a[681]  or not a[680]  or not a[578]  or not a[478]  or not a[387]  or not a[101]  or  a[397]  or  a[398]  or  a[404] ) 
 and  ( not a[692]  or not a[679]  or not a[678]  or not a[578]  or not a[475]  or not a[387]  or not a[101]  or  a[397]  or  a[398]  or  a[404] ) 
 and  ( not a[692]  or not a[681]  or not a[678]  or not a[578]  or not a[475]  or not a[387]  or not a[101]  or  a[397]  or  a[398]  or  a[404] ) 
 and  ( not a[692]  or not a[680]  or not a[679]  or not a[578]  or not a[475]  or not a[387]  or not a[101]  or  a[397]  or  a[398]  or  a[404] ) 
 and  ( not a[692]  or not a[681]  or not a[680]  or not a[578]  or not a[475]  or not a[387]  or not a[101]  or  a[397]  or  a[398]  or  a[404] ) 
 and  ( not a[534]  or  a[535]  or  a[536] ) 
 and  ( not a[740]  or  a[723] ) 
 and  ( not a[485]  or not a[406]  or not a[404]  or  a[476]  or  a[622]  or  a[678]  or  a[680] ) 
 and  ( not a[398]  or  a[475]  or  a[476]  or  a[477]  or  a[478] ) 
 and  ( not a[404]  or  a[475]  or  a[476]  or  a[477]  or  a[478] ) 
 and  ( not a[404]  or  a[476]  or  a[679]  or  a[681] ) 
 and  (  a[106]  or  a[107] ) 
 and  ( not a[107]  or not a[106] ) 
 and  ( not a[1760] ) 
 ) ;