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] )
) ;