qarma-milp-constant-128.cpp

#include <stdio.h>
#include<stdlib.h>
#include<time.h>
const int R_PARAM = 5;
int dummy = 0;         /* next unused dummy variable index */
int rel_count = 0;     /* relation number */
int y_count = 0;		/*intermediate variable number*/

int abs(int x) { return (x < 0 ? (-x) : x); };

// names of variables

// K_0 to K_15 cells of the key   (in this program)
// T_0 to T_15 cells of the tweak (not in this program)

// X_0_r to X_15_r cells of state at beginning of round r (or end of previous round)
// Y_0_r to Y_n_r cells of state after roundtweakey addition in round r (not in this program)

// ShuffleCells permutation (we use the MIDORI permutation)

//                             0, 1, 2, 3,   4, 5, 6, 7,   8, 9,10,11,  12,13,14,15
const int SHUFFLE_P[16] = { 0,11, 6,13,  10, 1,12, 7,   5,14, 3, 8,  15, 4, 9, 2 };
const int SHUFFLE_P_inv[16] = { 0, 5,15,10,  13, 8, 2, 7,  11,14, 4, 1,   6, 3, 9,12 };
//                             0, 1, 2, 3,   4, 5, 6, 7,   8, 9,10,11,  12,13,14,15
const int IDENTITY[16] = { 0, 1, 2, 3,   4, 5, 6, 7,   8, 9,10,11,  12,13,14,15 };


// In the internal state matrix the data is stored as follows
//
//  0  1  2  3
//  4  5  6  7
//  8  9 10 11
// 12 13 14 15

#define printrelheader() printf(" R%d: ",rel_count++)
//sigma_0
//const int Convex[27][9] = { { 3, 2, 4, 3, 1, -2, -1, -2, 0 },
//{ 1, -2, -1, -2, 3, 2, 4, 3, 0 },
//{ -1, 0, -1, -1, 0, 1, 0, 0, 2 },
//{ 0, 1, 0, 0, -1, 0, -1, -1, 2 },
//{ -1, -4, 2, 1, 4, -2, 2, 1, 3 },
//{ 3, -2, 1, -1, -2, -2, 1, 2, 4 },
//{ -1, -1, -3, 3, -2, -2, 3, -1, 7 },
//{ 3, 3, 1, 2, -2, 1, -1, 1, 0 },
//{ -2, 1, -1, 1, 3, 3, 1, 2, 0 },
//{ -2, -2, 3, -1, -1, -1, -3, 3, 7 },
//{ -3, 1, -1, -2, 2, 2, 1, -1, 4 },
//{ 2, 2, 1, -1, -3, 1, -1, -2, 4 },
//{ 1, 1, -1, 1, 1, -2, -2, 1, 3 },
//{ -2, -1, 2, 2, -1, 2, 1, 1, 2 },
//{ 0, -1, -1, 1, 1, 1, -1, 0, 2 },
//{ -2, -1, 1, -1, 1, -1, -1, 2, 4 },
//{ 1, -1, -1, 2, -2, -1, 1, -1, 4 },
//{ 0, 1, 1, 0, -1, -1, 1, 1, 1 },
//{ 1, 0, -1, -1, -1, -1, -1, 1, 4 },
//{ 0, 0, -1, -1, -1, 1, 1, -1, 3 },
//{ 1, 2, 2, 1, 1, -2, -1, -2, 2 },
//{ 2, 1, -1, 2, -2, 1, -1, 1, 2 },
//{ 1, 1, -1, -1, 1, -1, 1, 0, 2 },
//{ 0, 2, -1, -1, -1, 1, -1, -2, 4 },
//{ 1, -1, -1, -1, 1, -1, -1, -1, 5 },
//{ -1, -1, -1, 1, 1, 0, -1, -1, 4 },
//{ 1, -1, 1, -1, 0, 1, -1, -1, 3 } };
//sigma1
const int Convex[35][9] = { { 0, -1, -1, 0, 2, 1, 1, 2, 0 },
{ 1, 2, 2, 1, -1, 0, 0, -1, 0 },
{ 1, 0, 0, 1, 0, -1, -1, 0, 1 },
{ -1, 0, 0, -1, 0, 1, 1, 0, 1 },
{ 1, -3, -3, 1, 2, 1, -2, 1, 5 },
{ 1, 2, 1, -2, -3, 1, 1, -3, 5 },
{ -1, 1, 1, -2, 1, 2, -1, -2, 4 },
{ -2, 2, 1, 2, -3, 1, -1, -3, 6 },
{ -2, -2, 2, 2, 1, -2, 1, -1, 5 },
{ 2, 1, -2, -1, 1, -1, -2, 1, 4 },
{ 3, 3, 2, 4, 1, -1, -2, -1, 0 },
{ -1, -1, 1, -2, 3, 4, 3, 2, 0 },
{ -3, 1, -1, -3, -2, 2, 1, 2, 6 },
{ 1, -3, -3, -1, 2, -2, 2, 1, 6 },
{ 2, -2, 2, 1, 1, -3, -3, -1, 6 },
{ 0, -1, -2, 1, 1, -1, -1, 2, 3 },
{ -2, -2, 2, 2, -2, 1, -1, 1, 5 },
{ -1, 1, 2, -1, -1, 0, 1, -2, 3 },
{ 1, -2, 1, -1, -2, -2, 2, 2, 5 },
{ -2, 1, -1, 1, -2, -2, 2, 2, 5 },
{ -1, -1, -2, 1, 2, 1, 0, 1, 2 },
{ -1, 1, -1, -2, 2, 2, 3, 1, 1 },
{ 3, 4, 3, 2, -1, -1, 1, -2, 0 },
{ 1, 2, 2, 1, 1, 1, -2, 1, 0 },
{ 2, 1, 1, 2, 1, 1, 1, -2, 0 },
{ 2, 1, 2, 1, -2, -1, -2, -1, 3 },
{ 1, 1, 0, 1, -1, 1, 0, 1, 0 },
{ 1, -1, -1, -1, 0, 1, -1, -1, 4 },
{ 0, 1, 1, 1, -1, 0, 1, 0, 0 },
{ -1, 1, -1, -1, 1, 0, -1, -1, 4 },
{ 0, -1, -1, -1, 2, 2, 2, 3, 0 },
{ 2, -1, 0, 1, 1, -2, -1, 1, 2 },
{ -1, 1, -1, 1, 1, -1, 1, -1, 3 },
{ 1, 1, 1, -1, 1, 0, 1, 1, 0 },
{ 1, -1, 1, -1, -1, 1, -1, 1, 3 } };
int sig_ind[8] = { 0,2,4,6,1,3,5,7 };
unsigned long long randomvaule[3072] = { 0x329ff9a533f7dedb,0x95a79d3cc062a8e3,0x48c00910cdc691b3,0xecb7b1ec57d8e2d9,
0xb388fda995f7270e,0x440e9b4d0d0f92cd,0x08cf5c671fb90140,0xd4e5026b69975d95,
0x556fcbbdec0de018,0xa74a89ef531cdce3,0xefcaf5d30ff0c8ef,0x41cfd7dd5410899b,
0x1cfd4d718f51455e,0x704d11439a71c9ac,0xf64f4ce5e37e5947,0xba59e16404d819ee,
0x8011cac7db9f9441,0x323542d8fa053f8f,0xe952d4f2dfad5ee6,0x56c9e11002f646bf,
0xc254eeaa6f752135,0x3a6d8d1f9530d166,0x2e1769cfae318828,0xc91fc4e638046651,
0x8bac7bbabc381cdd,0xc1945a65cfcf9cf8,0xb4f57d4bbee3ffde,0x1728f9b17961a96a,
0xb64de36a4de81519,0x5f4b959f7de98bff,0x2ddd920bab088d91,0x6724fb57cc1953c1,
0x0827e7a6adf1901f,0xddd6d5ddcd9ffc9b,0x90ed1784df7a1b14,0x1e257243d9d10eb9,
0xb1cae8af38fc191c,0xca916a4e84fcb44b,0xf73f9b5ae49c422c,0xe38a877ff940e089,
0x928436872a8e08f2,0x9b9a0c1677bc2cbe,0x2f2e826c65b87603,0x47383727aa86c29d,
0x07ae9826c5127edb,0x3b04490d83536fbe,0x3514dfa56477fb84,0x359dde55e7c79e8c,
0xe43cc15d38b3b1f6,0x2b503be3f0bbfee5,0xf3107fbc623e8752,0xdb6543b7e541d877,
0x82bc8a67fdfedb76,0x940c4e1a8fce5706,0x7a579adcb9f0131c,0xf1835b5dbc2f0506,
0xb126adc1f1f16674,0xeb0b9efadc1636b6,0x045093ef2b67ed64,0xd2e5a04d5a2832d3,
0xef7e5bc90dfe8422,0x1b8a85ea2a6ca38e,0xb651bf3c6df14e65,0xe52a4d06e5f623a1,
0x47fb8a5748e79ddf,0x4843677799ef8c0c,0xbc80fa8015aa1a01,0x65cb401672976c49,
0x2cde333a84d29021,0x9d3ca7c42def6b22,0x244d6fd3a7f94b30,0x1fc861f42ba4c5e7,
0x371d86ccbf0103f6,0x0e6f514ba73097f3,0x02c78b8f75d5102e,0x31f2a2562b3a5007,
0xca5f84f0024e98dc,0x060ccf22a9ef4687,0x1d0ea0b12dfca4e0,0x917472e1245f2fc4,
0x2fd45a7eed03d231,0xfaae9429dd766cf3,0x4a6f294655abc7f8,0x2df4891eddec6506,
0x48a0d8ee9facebc3,0xecad7fe06977609d,0xe7847430a22e120d,0xef7f275c184f4df3,
0x4f2e81f174036915,0xcb5f9ed2462e0fef,0x712d11fc07d96e72,0xeccd101558736409,
0xc40520007bb27b22,0x9f2a7397e21247c9,0x06a1c836a8de3db9,0x4458d0a057ad5c87,
0x6f7e6f1bc88072eb,0x754e70cdfb607d8a,0x031fc138962954c3,0x06c4176a01bfa9d0,
0xe9172c0f52aa7702,0x7a348818f6f07dd6,0x8c1ff49b9dfdc2a5,0x454bf89f24c94246,
0xa3a96a8ea4b4756d,0x98327403c4d584f5,0xd6f21d36dfd559a7,0xe27aa5ea35de2659,
0xc458b0706eeb9c17,0xd8276b30a708f7b9,0x6d2b310a888b2af8,0x8d2ff25b89a126c5,
0xc1e270948f32c8e2,0x9e7d55c1b28198f0,0xa0d8c5bf10ee6e99,0x31eef50a6cdf206b,
0x4cf0f3ff84ccc86d,0xd16e3f74f22c1cb1,0x34a5c91f98873944,0x03eccdc486e2f853,
0xf53aea2736a2907a,0xd29efa243aa7a503,0x13c05e8ea41b9799,0x35e46434c85db30b,
0x88982db3f861bcba,0xd5dcce5c6db69df3,0x95d00766a18d086b,0xd97c3ed978a0f37c,
0xb585b567e645b636,0x121a6dcb03bbdde6,0xb9c5affdfa26c667,0xe7a1051306ac58b1,
0x0da68523c28d1e52,0xaa208cd0d6117ae7,0xaea96ebf22f3bcf6,0x0bdfc51ecaf33721,
0xe57635f6f5e66ba5,0x295bce07c4da0f1f,0x43e8acaef1cf2b8b,0x020fc56352ab165f,
0xa14217aad9e1a28a,0x12a0ffbdd526fa67,0x385830068b76b1e1,0xf5c1a3a527f365d2,
0xa721a0735f5c1106,0x03ce9390836bf5d4,0xe5973838f81a35f3,0x4fbc71e29a0d8c04,
0xba57f766b4809845,0x6713de58020a8af7,0x58a28fbada2cba5d,0xc3c5c5c3a96c978c,
0x80586daaef9cd96e,0x4d2e7904f008a36c,0x00942294cd229816,0x9d4da989e0814b93,
0x2a0fa8171598f87f,0xe0e2cc7ba9b49af0,0x1407a5cd89df7cd6,0x11f633f25250138e,
0xcb2928cb1c2dda86,0x779cccbb98e3b3f3,0xd3a52ccb5cf36cd8,0x011f6f851bba4d10,
0x89f00bcc3e81d241,0xb35cc522c925c506,0xfc43dcbed66a8a28,0x8a8ba95bfc1a0714,
0xefbd8a6bd070fb3a,0x4d511a553f9a8d72,0xb749cf3a662541f6,0xb7b1d48edc7f6f6d,
0xe4fcb1b94c7b0c62,0xee84ac5f92db6b05,0x83d4eff399450cec,0xcc124d40d0e89a52,
0x6757649a0cf0cfad,0xe2f181805a9edded,0x377cf46f42d2cfc9,0x3bd1b968ba3dd445,
0xa85d87e03fb40b6d,0x796472c740bec0aa,0xddaf0e8c82ebf0ac,0x1d4529c49792370a,
0x3d4531b339248378,0x9531a6a41212d8ae,0xabd41efa152ebe26,0x3fbbb3d1129e9e8e,
0x805d54274f385ded,0x471f70ad9e0b227a,0xaa7c143182d3502d,0x893afc259efecc31,
0x39b0ef35af8fafbb,0x21e064b9a60ad3bd,0xb26ccccdf7ed1fa3,0x8d0a3a704d83f2d4,
0x98ae61f7d1c7ea2e,0x8ddd43890c61c3cf,0x44aee41d80379cbc,0xbd573bbd98a48883,
0x0969086e9f7c7daf,0x2a617ec09465dffd,0xe1da601868fa7839,0x316f47d355011dc1,
0xf1bc709311552a85,0x3ec4f33667118cbd,0x85a26847a3b491f2,0xca3d5a62329f3c0b,
0xef4c5802697f76a9,0x147f14b1e1147b23,0xa4ea948fb16364af,0x8f1fa89f722956ec,
0x0da3d3433ea14520,0x27cc95270deab67c,0xeb1d8b452bb5c9b0,0x3a45ddca65b1f4d3,
0x4ede001dc3719e38,0xa58e0e89b2dbb064,0x6fe29679c2b318c8,0xf1923d7291409efd,
0x0870f611c685074c,0xc0e37473c2f73a10,0x6a6ee6573ccc763c,0xc13b37d595f07876,
0xcf35a90d7712c1ef,0x9ce3a42d9b6891cf,0xcb17c5492e44e499,0xa1f4a04a340f7c9b,
0x75dcf032ec18e60a,0x8efac3db3fff4008,0x6216114a0cea6ae6,0xd6c90a29da27584c,
0xed286be732dc4365,0x80dfcc5e2a03ea1d,0xf6b3b29404f0225c,0xa4e0b4289282c332,
0x0a677115c560a4a1,0x83147d4ca8fedbd8,0x02ebfb894ed2afe3,0xc2d22f4aedf60030,
0xbc80f42399c6acfd,0x8049d821e314eea1,0xce2fa7dab233690d,0x5e2808cf370ff01c,
0x3f806b0aa8bdfff8,0xb4bd67084bcf2f28,0xe190275dde752c1b,0x8a34bf73f2a0d61f,
0x3237d41e030d974c,0xaccf961a71cf0643,0x77a8b4e134a8ce4e,0xa3ece1f59e6f8e38,
0x90ac0cab54726fa3,0x1874488e371ef077,0x5107c65e5ab6406c,0x7b7a0caf8ccf2fb7,
0x9a31c74794c39be9,0xfae297bfc2d1c8df,0x25cd98fc9456f802,0x2f6f5ab1f08e4b79,
0x6fa530c47212dc63,0x6c706cb6130c63e2,0x6cf011955f62e5e5,0x583da1de35e746a5,
0x6f96dc8681962cbe,0x5b714e823812a910,0xa9e89006bea9a524,0x10e1b236a450c929,
0xb347c7e84da83f13,0x8d3471fb3084a461,0xb36c0a8520bef87a,0x4940bf71f64b9290,
0x594eb1341e941b73,0x864a6aa72af458d9,0x20d63e5a4880493a,0x1f14448f2c601066,
0x90593578d820d4eb,0x6c34f8cb650c5af1,0x050d676835c51642,0xe1ad56f74b55db8b,
0x99388f30c516db7d,0x75e785ca86feab34,0x15e11fda00e9aba0,0x30560b15ccd6364e,
0x46c4035038b1d620,0xab8abcfc1efd73d4,0x1e51ed042d775c00,0xf7237d824b800e2f,
0x711496a86c32cd35,0x582cc2be254a2eb2,0x42780448da3c9538,0x5b1d1e6a9110c70d,
0x2bef48f2fafef3e4,0x3acba042315d8ff7,0x1085162c0ed02fb4,0x5da40f043fdc8c70,
0x55e34b1124b4134e,0x85ee66ee3071dd8f,0x1a08b004a19af62a,0xbde750ac38b443a9,
0x5c926d5ba823a406,0x7e7fb6c9d51e9e84,0xdcd9f599206740a6,0xc5c77c2ea71214bf,
0x4d8b8b8a72e673d9,0xdd9b8d4102e86ad0,0x37e632b451a5afbe,0x2fc36f221a2fc62f,
0x5565be0a075d0eb4,0x907352d1e3f2fc76,0x5ca791f11e2f4f7f,0xc9bdb65cf6e990c3,
0xb4001c30be9de6f1,0x2b9ba3e381d6db63,0x96e5805273530dcd,0xe0fe5c2707d8e275,
0x2a76024e015e6630,0x5a501202d8cd0f57,0xb8d1d517b635d231,0xa1c53b7f11f69713,
0x5d5776546ab690c3,0x26c17b7add00366e,0x2c17dc09918e9c91,0xe161c6054c1231a5,
0x47263dc08cd3e987,0x58da45dcf615efbb,0x2dd48469587ae2cf,0x339ab14f099972b6,
0xbc1b4c6be81b65ff,0xe230bf0da7da5e24,0x512db5253cbe3ebf,0x1dc1b77f5683f72f,
0x7d633a878b1ad446,0x0384e8fb878d3bc2,0x2bf5cf3c15b7b5b1,0x656304993f27e514,
0x9405093b58019599,0x7f6c12dba9ba180b,0x1e6b4670c7ac0043,0x5fd3ab54cc6c3c91,
0xb5e74c938347844d,0x2a08b0b460bd55b3,0x51e4d5afacc15755,0xac14f42c48981a2f,
0xc69e9faf4984343c,0x7bc6d6420a56a379,0xb77b0a3cd42c4b04,0x271ebfa52f7a0928,
0xe778e60370fed0b1,0x20e01013eec12faf,0xad57ff1944e41280,0xb7fa68969d2b7bc2,
0x6f69aca9f5c3986c,0x77d98f4c0fad50f5,0x52a627b4404f6549,0x4a030e1385a0e63b,
0xdcb38c9766cb97c8,0x35e4850b31a5fca8,0x330643e362131f5f,0x535103ae80691a14,
0x1124147328ac1942,0xeee380ae61353435,0x0877258de15fa9ea,0x9e30545ff47895b2,
0x1b9a903c4cfd298e,0xf40e58770fb6aa10,0xe2fc6c8589773978,0xeadc8f447037fb07,
0x8916ce90bf9e5a88,0xbfcdcbdf3c82f56a,0x69d8427f11a3c24b,0xb8bdcdf797468469,
0x0f436218be0db17e,0xa7621f9755076793,0xe43409aef3e9fc9a,0x2bf4b96e2cb24336,
0x8ef0c8103e14f1e8,0x1b6db514f42cb3c3,0x3ffdd9b5a919ebdb,0x730152712e1af30b,
0x1beb26dba510014f,0x70d00db5e65d700e,0x74e78bd5d2e7376c,0x26627f60a9bb2a00,
0x7223a757020b8f8e,0x872d51b6aa52a353,0x05b0e6fd4379524e,0x93521d4ca11fcb5a,
0xc6f50cbc873749a9,0xc7ada2ea49545973,0x08c25e3ee906b684,0x17d4b8263d15f963,
0x9e17a99c37f78fe6,0x7a2e7ac8f03264c1,0x51c0600325a7b331,0x290e6f53d2194eeb,
0xc0a1e6d70414dee8,0xc561c348c4eae24a,0x4f9260883dbf10d7,0x901e3984ee2bf746,
0x9fc53ac3479a37f7,0xcb7316e3fc7713f5,0xf3f3485d92c59359,0xbbfc1b75e0f435ba,
0x908d8a6c169b844b,0x9ee39205cd6edf12,0xb8ae908aea0b8b12,0x1dade07857b5f714,
0x361d17d5705f27b8,0xe3e33877392649de,0xd0d8de2d5abb889c,0x52ebee152f0abc3e,
0x7b8f05f948c709fc,0xeb2f14e8af045b39,0x82144e38c711b5ec,0xfd57bf4109042325,
0x2dcd9e79a8c36ed2,0xd7e46882293686c7,0x514d49454ba12f2d,0xf2135a51cb48e016,
0x0bfa3d6dd2f26640,0x14afdbb6de622cb1,0x3a74c62087676c7f,0x97ccb1c3c094edc1,
0x8d32aacbd6c2d69f,0x7fbe7dead34a271c,0x0b6cf6dad651657a,0xa1ae9ca9422d5fea,
0x6bfa713feb643283,0xa57a6d74a7a73403,0x0567bb63f1d5e5ba,0x756b5f98ad19f520,
0xd0b24acd07006f31,0x03c19383e44c9b4f,0x9219f6ff93de2970,0x86652525a98a4862,
0xafbbe79d2ce21b15,0x15a81c8af4c9af88,0xfe632a6b9a94139f,0x424e520b4e744c2a,
0xeb3241f6a6fc2385,0xc0a12519e3feabec,0x8e7196eb2b2a7345,0x67ec3a356b9778e6,
0x99564b3c55177343,0x12cd9feb9b3f1f00,0x7db41c048c821379,0x0a7d8d4b73477f05,
0xa3ab4e11eac3334b,0x8f44591b9537cb16,0xeca4c6770c85df96,0x948c0b4bb598840b,
0x8a1ad23b8b597c24,0xe7ba6b51134cf11a,0xe92065f32e127799,0x78a2bb756a01f0c8,
0xe2b20c1c33827446,0xbbcfad314d0355b3,0xb78dc33f1bfeae5f,0x4afa305ddf9719bc,
0x76ceb634e0e2e936,0x04bbbfb258c56cb0,0xe35908163042c547,0x59c7f76de842632b,
0xe0edbded9bde72c7,0x195a195ca81bc7b7,0x2408a819075d449f,0xd3edb2fcac5d89ed,
0x2d591349723c3b67,0x29e21f773b9c42f9,0xf83df2fa2e3a1189,0xeb8684e5e2cab3a1,
0x30111c0acaccba4d,0xb616c31516f72d03,0x535edbc8d8a18de9,0xdbd790a1b783ddc2,
0x5203b9968df0630a,0xcad1e7dbab120217,0x3dc1f7156a833cb6,0x97ac95c8008a6306,
0x5b4fdfd5d11e38d6,0x547e405c9c4e2ff3,0x36e9e80a93688d5d,0x1f15c9c1a9bfc07b,
0x8adfdfcd5dbad11e,0x333a694abe552ad9,0x6d2c581a5349506a,0xc64aa7c09953a90c,
0xd86a5b75bf3e8442,0x47ebc181d3e9e65e,0x8397caa2e17f18ff,0x2aa924466cff288d,
0x0b8efa34632a7a44,0xf26658db735c1823,0x25fd17f218c08bbc,0xad280d489f6dbbda,
0x413e8382a635687a,0x08aef6a22e860f35,0xd96f7740b35a239a,0x730c531e15c6b8ff,
0xe1b8bfcc4475137a,0xe1eca3c3cfe78686,0x415b950f353ec093,0x4593a15ff0b240de,
0x395aef27f4a2daf4,0x213badcb81d360c0,0x480c4a0e53666d67,0x5db7548373d65127,
0x3760148f02324393,0x095235ee81fa4695,0x3018c730831a227a,0x7f12b56c18c23f80,
0x4ae3339f6d00f864,0x2b7c6c8b7c985c40,0x1048a05077301fdb,0xd99f57f75542017d,
0x6e3c14403dd44cea,0x0d88126c1d0bb52a,0x8f36b48abbf9684a,0x366cfe028a5f57f1,
0x30ab03b920c32e68,0x599045eb26d67994,0x7849165e071de78a,0x9df10bb0cf78d93e,
0x33f84beedbb11b1c,0x9574cc35039e69e2,0xaf097ae57d33d6b4,0x517672216f959411,
0x46a4f58d6846fafa,0xd39f47c9520ffdf4,0xa21b4687e458447d,0x5f723a64ae7a7b68,
0xc85336019693cee0,0x328de2290979d788,0xe72f8446033745b1,0xf7941475a43fcc29,
0xbd889b12c6fc4f22,0x342f22164e325526,0xc7f06bde595232ca,0xe2984a68e916331c,
0xd3250799d5b47ac3,0xf46defb34b362f6a,0x8d2c574755712315,0x6b14720550ff1ab1,
0xd74b7fc2f2dd11cd,0xfc131d6eca350645,0x4d5392d749570d18,0xe3033aad10e8a9ed,
0x72f741fe05c1eb0a,0x3395740912df2d4d,0x5d4708004ff950bf,0xf99d49141d87ee23,
0x525def032b884dec,0x15f3615c33bbeef3,0xb2d514c27385b17e,0xac66f96a9141953a,
0xfd62d384126da12c,0xb63010cf3409acdc,0x1c8ffb241b4c3c06,0x5c6c290a25248618,
0x732c7767eb7be5e3,0xe253355f87d1d6e9,0x13671dc0ba5fe8d9,0x106211718351e4e8,
0x8e9afec56322c559,0xb756c07379af220e,0xac66470ad2d6def7,0x669ed337b6c56a81,
0x7134e7f4f8a558d2,0x821109e05781c3f6,0xaf4c18b7da959b82,0x7a0662e1f2fcbf33,
0x0c370a02fbd03d8c,0x10e82e78fd0c58fe,0xba7c8896dcee723f,0xb7f1fc7fe3e167e6,
0xaa9acceaa1ecafe2,0xf11684ea75a604d7,0x8697945e6f6b0d97,0x88a87b5a0dca2c2b,
0x30a2f298cb24dd15,0xf78ab83a3acdb5b1,0x803550eae14790fa,0x0a3a7c5aedd72f26,
0x94211b4460c0129f,0xefdea866548d7a82,0xcd722c7abb6f868e,0xadbface3d2b525a4,
0xb7662f745bdadfbb,0x3d90cd7cfb006e10,0x972a839a9bdb398c,0xe6eb7355cf335a13,
0xbfd305846e31d109,0x05aa6614377d1f1a,0x6033bc062996a784,0x036e0b46a1901ffe,
0xd08d5560b5481b81,0xd73288a856c1a439,0xd673a0ac671749e0,0xc0d7318707dff70d,
0xca94f4e628693530,0x93293de18893b0c1,0x06e518ed34cf994d,0x48176aac5919016b,
0xb6a720723186f2b0,0xd140d00ff801ed5f,0x1b67bd9e7178660a,0xaa50e043f92146ad,
0xf823430ce9dffa8c,0xab4af76ce5433247,0x39c84cb7c0935dcd,0x26fc8b0cc4be6dca,
0xb629bd204d1cb695,0x6f0b766eae0d52bc,0x718b71394878d25d,0x0ede878922aaaec4,
0x080520a55bd9d4dc,0x26e4c74e4d4a2232,0x945ba27addaf1809,0xfe705fb4082d4af1,
0x1cfc7a58618e17d6,0x20ba9f09538e8b30,0x268af9d04c3ab570,0x3f9cbb9199b016f3,
0x61f4254469e991f8,0xc21f9dedac64f448,0x090b95b8c74447f3,0x90093d358d8c5061,
0xe93e68eb3657fc2d,0xfdcd66bb9e1cbd92,0xfdf3ac9493675f57,0xad59c20c7fa237ef,
0x5037be1faf0caa61,0xa16b24812e516a37,0xf2020e684f63485a,0x1e14d5863a34329b,
0xfa13069cdaa9b484,0x72095bde01718ac1,0x68b699a50b416fb1,0xb6b6c1b5ce3a83ea,
0x4e58adef858d7a05,0x5924c8c55ec55ded,0x6e1f4f69a425d9f3,0xa43c49e1e1b798ff,
0x2571373509b421bd,0x31b7a64fd5df6a2f,0x766087c26a809496,0xb37052eafe2cad39,
0xcf6e4bfc111b4c38,0x84950668d4bcbc34,0x5447f19c96eff052,0xc9408cc9de0538f3,
0x0830b04be0c62884,0x613e011f304fda2a,0x1a42dfa8bff1e1b1,0x0b15b5be7e1c5e8f,
0x34d38ce51f125dfc,0x1d070584c142903c,0x46b967cb2bd81b75,0xaa6825981e573c80,
0xcd7050021baa92c7,0x3eaac5a56a6a51ad,0x9d6e717dcd322400,0x903dbff65e500eb2,
0x1fbbb7611cf960c4,0xa526938731994f7c,0xbdda96b5b79e0c87,0xb156ba8d9bafbcbf,
0xf53552276298f690,0xe0db5c072bfd9e2e,0xa2b722087f54b4f1,0x02f0c92b01263603,
0x1712944f32b487df,0xa7a922526f39b29b,0xa66ef77486cc8382,0x6d5417f2f14057db,
0x4a57214eb80a50de,0x6aaf32ac7707ff3c,0x35dc189a6a507c68,0xf083cf55544bd77e,
0xd6a06f380b749a06,0xd209ca069d1f970e,0x1178aa352278f174,0xd72f98acc9a5fd78,
0xc53cfa1fb0c5cff4,0x0c47e95b2880de1b,0x4aac7c9a884cfe9c,0x6892e20711404beb,
0xf900f893d4921404,0x382877230137ab56,0x12347271f0af58c1,0x689dbdca7be47bdd,
0xf53f905741cf5620,0x2f40f8062d8429e6,0x4bab4b1988de256f,0xb87fd2f01dc3a3b9,
0x85256b85317b08cd,0x726a4e7bbde36aa3,0xa31cd80a375aabc3,0xa96d23559d0bff9c,
0xa0a4f4318728bfb5,0x175ecf3434618d6c,0x1c892ee837460832,0x7b6a3e9b1340762c,
0xfe8975fd3bc21b87,0x6bef9fe21ebe6a06,0x61fa5fedcb0db2b7,0x5bbbaf78354ffa05,
0x3906af5fe092319f,0x6940137b029e94c2,0xbb0d98f8edae7fbb,0xb3e62e3d9a12e74e,
0x5af64745676a9f94,0xe8d2d98dde03f9a1,0xef328215700d3510,0xcabc64ac43093762,
0x11f23a967ad128ab,0x5f84edc66b044550,0x88016668276eddb1,0xa8faad213411499c,
0x705875b2af716a39,0x7db9b1ed43043a18,0x8f65ee4ac9971607,0x814c33c39486349f,
0xc6fd166abf170d33,0xe2535cd5efee96d2,0xfec665876feb4871,0xdfdf6a0351aff9bf,
0x2a48be84fd652363,0x132c6ecafd436037,0x2ed53ad1c17a558e,0x94eacdf0127d80a8,
0x5cce0abebb1fd365,0x4bf93c069cbc07ef,0xea73601edf65ef69,0xb4728bb912cfe1f7,
0x84d7bb53a153949a,0xf48e2f68c0e46623,0x9eef836d6264ef02,0xe985937f0a7dbe6e,
0x7c47f8330305b4db,0x02f40b3d97f4faa0,0x40f77ce06b8fcb39,0x2d66262e78a4baf0,
0x869c5b0ac658711a,0xd8905536a4d07b9b,0xdb5a6f48c88b3ff1,0x30a4003daddcab15,
0x4dd0d1d577b034a5,0xeb514eca5925a20d,0xdca6be5602feee64,0xb3513d3c9b5a0b80,
0x69a541db8c3264e2,0xd6de9ee8a99a30d0,0x06d50e522758b19b,0x38c1fc7f52eccbb4,
0xa20422591fb98128,0x60e7903c68555e47,0xb2995db461eb482a,0x2383f46f10d14bd1,
0x8d59a2f7393b2bdb,0x471d29d896a13fc4,0xd68ab7bad2781d10,0x4b73260190bb9695,
0x214050f211f91a99,0xc5a668b9817cfc75,0x90ad849ef411227d,0xb4349abb2636c863,
0x6a3e1a1c3bf56f4c,0x69a2e4680d6a142f,0x70bd1936cd7f29c2,0x2c2976bf1e4b577f,
0x2c3792570fcdc765,0xeeae7c13dfeaf476,0x90da1dc9537a1fee,0x7c0007fe96fe8aa7,
0x7de08f43a411b95a,0x54c9859ac92130d4,0x8fa53fa7896f418d,0x8ee643b4994dec9f,
0xbd62669808f23894,0xe48696ae4b3dbf06,0x3e1b80bdbb3ac46b,0x5406e49c8a065b90,
0xb4dbee779ccd0217,0x625ccb67f0281867,0xa147f8d552030ab6,0x9603ff0b16a8f9ab,
0x02e9042e4ee366df,0xb73508e18fb95b6f,0x14f19c4176fddce4,0xf022ffcf3cc809de,
0xad1e2e700280b9a9,0x9ff56a50c0a235e7,0xe219046c907d2ad3,0xf132c352865c5fd8,
0xf6906d8313fc3118,0x77a985f782c1935c,0x20f02bb9b117088d,0x91f4c2656bbf812f,
0xf4c2cffc4d7b5847,0x414cc86412f701ad,0x5d2eaaf056a2da96,0x42a73a00b948a4e4,
0x2945d59fe3e566cc,0x20b3d14603f02b50,0x23d8bf038c039561,0x81aef97a46f62e71,
0x38f34b687b48cbf0,0xfe50d5afbdeb10c6,0x65cbe0943cf11eb9,0xbdbc71992fd93f3f,
0xde6814fc159bd429,0xf60f91e783116ab3,0x4fbee21f276a15e8,0x89a6f6147957b343,
0x7cefdb69145615c6,0xa250da91bdca20c0,0x059720bc0a4c7956,0xfbb72987d2058b5b,
0x09236cbf5721c198,0x94ad1daed7ad7db4,0x4e0e2c4ca8f127d0,0x5e11c988792d15c7,
0x8a017371ced8e585,0x51be6d1bc1bfdb66,0x1a3f897e6a223b94,0xf59d24945f3f9109,
0x6a4607518cedd0a2,0xe541d3374775e812,0x1167fad150c7b580,0x42ed022816c5d6e5,
0x2f323417b0f8c97c,0x1da17e47c05123b0,0xd718933856bdabbb,0x2404e077f2473733,
0xd1fab87cabe14cb9,0xb058a70c93b67867,0x1d7c09c95cf5ebca,0xe46190744df22979,
0xa6a17c8f79ecf521,0x4317ea72a6be9f47,0x92311fdf4313f8cf,0x1b78c2ce91436611,
0x0594a7c07dd8e9ed,0x68ced089dca85d65,0x715b01087b73fafd,0xd98fd791e269369a,
0x9dd5457983aea281,0x3f8dec93512cb44e,0xe0669000fd996475,0xd4e5af8e27f5b7a6,
0x8087f811cfdd2d54,0x47869b8eee3a933b,0x628f58429c0fffb5,0xf63a792651c76b6d,
0xb60203e0e85d4cb6,0x3d36aa19ce2d301b,0xb2fe0f14cfcb044b,0xf7b89a4e0b74f6cc,
0xa6a2690117f8d0db,0x81aa98965ba7b291,0xd1f6590899c67c0d,0x9ce49e32d85b6bb3,
0xb254e70a0f72dce9,0x0f35c24042270c34,0x1ff1b81141590ebd,0x88865eaa9ae5bd83,
0x8766c60312f68c80,0x27280a97c7f3d2e6,0xe30a9b326ada7709,0x79add545f625a913,
0x80ea105cd8a635f0,0xb7053af620e56855,0x145900695fb46bb3,0x379074b7e99246c9,
0x26cfa36909f75221,0x9d287df1f4b3897f,0xa36d1c65a90a9ca7,0x312a793ed52662b1,
0xb9586b1c45931d18,0x90f080e18535267f,0x88568fecfbad4f36,0x3da5c53016e7a853,
0xa12e72b2d9125dc6,0xd49f717bbfcb0a0f,0x865991af92a0ff8d,0x439672fbf377d529,
0xa98f4636bf673279,0xfa5e64f7e4d75504,0x4c75bc8f81a20470,0x9e720b5487c63317,
0xeee8da3484d7a4ab,0xfb19871bb3ee2f2e,0xda2f3e2b157c6557,0x01d082c2f51fecbd,
0x9f9c88186a28eb43,0xee8d26c304ca00b0,0xe6c627adf167c6d5,0xddb76776d1f7540b,
0xa50e387130eb9df7,0x25e896bd14f27d25,0xa7b541ea3c9249e0,0x0a5393ff65dadb04,
0xa1fa141b542d687b,0xb4bf6e52bf5de573,0x1387c094cc278e6e,0x30027223e86fb119,
0xddf446e3af6f7ef9,0x88b2a0938ac1449b,0x74856f394b211b13,0x9c94ec6170090335,
0x796c4de874c94aa1,0x7be2d68714baf87b,0x97b0c47b1bedd7f1,0x40c461074073de65,
0x4f7baab5aa0ec132,0x28c392687bdbe314,0x1bcc6f8c3811d0de,0xcf7b128b09f0733b,
0x3a4eb6d5ae81f306,0xd820fcbae65da6b8,0xa5dfe30df9f11ae5,0xe8809fa0e69af852,
0x16cebe7cca5d6a9f,0x33098aa32c224ea5,0x109d59103b3fc1dd,0x14c7cc19e5c4a6da,
0xea27adae40c37150,0xc0e4c05ffe69e5c9,0x4d91568ae5c9a1e7,0xd247224f18e09bed,
0x4815bb04b8a062d4,0xeedc8ca451b94e6a,0x0bffa0192206e168,0x7fb59cc9de2612fe,
0x631b3fd2bf704f99,0xc4604ee655eb34cc,0x4c16eba5bd74c357,0xa7a2a713b82b3357,
0xe95e71deec754462,0x9b7214c4b9f8bacd,0x7318b5224540eff7,0x74f0de1f3d37dd8f,
0x34284363bbb294d3,0x2ea26e404db13571,0x81e2ee1d1292d4f7,0xd81c4cc67a20454e,
0x8461458086814163,0xaa4c830f667630b4,0x5eab2a3a285f6d2f,0x225cc92202b5c2e7,
0xe6e71d3bbaba0488,0xba4bf474edbf6b58,0x2d897a977abf10bd,0xe501638521203c38,
0x770564ea401f0dd9,0xa875db1b35e56dcc,0x178b377e64115f2d,0x8655262c2abc9b53,
0x59daabfb4bb945ad,0x216f5d0e2931d93a,0xf0ecca51aa63fba6,0x39f855835d2a0553,
0xf3ab489a7efc9af2,0x09e9d52799b559a3,0x948c8d19a1a039e6,0x884fbbe4fadb07d9,
0xefa62c013fcf13c2,0xd183a3ebbd9175fe,0x5b7929e7c7958074,0xa5ee25a9acf8246b,
0x76e0bd060571044f,0x0de16b369169c172,0x6bfd5a38ba822c8b,0x1529d43606122f43,
0xf9dcb053d443d645,0x5fc06d4e3bc1ad59,0xf519b8a9c860f654,0xe8b3c85a5d77f487,
0x0d3ef4de4ecc092b,0x32b83d7b42d3c6fb,0xc8e08686fa6d0f8d,0x8dc171b40ba8be3d,
0x1653d2fbb7f5b47c,0x97f1ac6bb9d4392c,0x927badb77689bf12,0xb613129c0325db1f,
0x818e8b2aca236628,0x40a699d2e4dc10df,0xcac13ec03cbce6a8,0xd4198f2ab769edb8,
0x8c7a3ece877f7a88,0x2d0940d7cf6b3561,0x7f6e7fbac7eafdaa,0xa45d0f078e8f449f,
0x4d75773de00298d0,0xb58b21cf5b7499f3,0xa88484c2a93095f8,0xe5b71df2b61bb826,
0xa495026afd075fed,0xe1807fdc0534c172,0x8682576e7d1394e7,0x72ca74a0f4c3bd6b,
0xb0405d5519bf1ea9,0x03b9e3c66475b9bd,0x4ca1760f5fc51f18,0x2c92441bcf9e4165,
0x623f1bac3c1ce29c,0x59c4e6d316dfa370,0x3653c27dcba60bb3,0xb112532a083f8bde,
0x77a1c8c20e21c285,0x847fa9aeffd7c8fc,0x35c060564eedc18a,0x2100650699f9c5c2,
0xadf78f6e7db13c87,0x97b624bfd82a41de,0x623bd79e5e531776,0xb7af3a72de0ef27a,
0x2edb7a4028becc4e,0x6d6dc7a793bcd7f5,0xbfdf7287ee11953e,0x9cef457a13346d39,
0x9253139781d03abb,0xb527aa9a94bfaae6,0x09ed36759c8fcd1a,0x7710d0ddddcc6f1e,
0x224faefdccb6dd86,0x86fc90d8bd6f9bb9,0x80034f6c82cfeece,0x6a99541858115988,
0x072076705ca029f1,0x1c605aefc734b607,0xf83f7f21186fbce5,0x99e9208c94a2540c,
0x197e066f03f82c99,0x854c8142015e2d8e,0x3842a320f7e95265,0xba0a17d8ba0907bf,
0x8e20f382474946d5,0x03c5a177a5450616,0x2454abe7f507f38f,0x6326bff00314e26e,
0xc1670c6448ffa551,0x309dab2fa93c1f98,0xf7fd318844651607,0x5e1734e8bbf943e8,
0xbe12cd766be8bca6,0x8b8a5ce5e547c97c,0x6745b631b8043da0,0x4114d6965adbf82a,
0xebddb4b8b4d386d9,0xe1780bc521385f22,0x7116e0b5cae01a1f,0x3655aeb41e013354,
0x8a50e48d089f914e,0x7261861de7c89df5,0xc27590ac96092d96,0x889ac9e928a31145,
0x0e0c67b41862bd99,0x096c213d170a3f62,0x66a07185ab7b37c0,0x1d5859820a8bd3b6,
0x4e911d3b1842b050,0xa340eec0b8a0ce1a,0x06ebf46f86de371f,0x764e99a9ab734e5c,
0x89ec977dd4587beb,0x6dc1ed48276ab7d2,0xab94448d6b563162,0x7347574da405c0f2,
0x276999a60d475c99,0xa284eefa686a1704,0xff9cfb297f82d7a7,0xc2f8a9c231059103,
0x5d1aea6476b361f5,0xa01a03e177a40609,0x7e26c16cb9fb8bab,0x8289d4e69515ba75,
0x15814c7412be0b0a,0x9fc15151b703c85b,0x44dc82e810b313b1,0x594fb37835f62bab,
0x6c85198181d6823e,0x6d50d35a684bc388,0xf5d8263b94c974ff,0x6f78c01ab1bca6e9,
0x5adbf2bce040ca70,0xbb74cba7f51350f7,0xc37bdb89c9defa1b,0x1eb2687d044ba224,
0x63225a15f484351e,0x63be389fa3144ca2,0xbd9009935a3379b0,0xd0d079491e8b7c28,
0xd044a6e33ca06644,0x7165e53492f14bd2,0xc8c0729fc91bb7ce,0x88b42d7b785905c1,
0xa38e7adafe76993c,0xc9634d465388cbeb,0x4edc5d627ff65aac,0xc5d1cd605c3fe18b,
0x7ac11bf66ae0faaa,0xb0f987ee6dfd56aa,0xf642113f5040cb28,0xed08f1e853025a0a,
0x6f57edaa25a97026,0x74493a8f816f75e4,0x2fdbbb7778700de8,0xf280773ba1c4e628,
0xd290f48e7907df4c,0x77e78f7cfce61b57,0x07318220850c5610,0xf0d87cffeb3d20bd,
0x361abfb17a2779b6,0x3147cdf5bea2fd5c,0x97c5458cb23a45c3,0xe0f1c80d5b9f06c6,
0x6fb8e3f773639b0e,0xf69a775da1dcf0b6,0x99dcc6039b5ef671,0x2057f2c45b6467aa,
0x7703b9a7602af2bb,0x3424ad79c8d8fb7d,0x8476504304674d68,0xbc42a6a947ec9ede,
0x462d1362fdcb3712,0x74d6e29bc79cd246,0x6d8da5c41cadf3de,0xec393d633bffb725,
0x271ad718a8174e94,0xf2824483dc5581d5,0x95905dc0491f68a0,0xd92e11c91f191b46,
0x320307bbdb8cb60a,0xd5dfd0ca81074880,0xc510dfa7f126f952,0x45d83aca76799d65,
0x55608c2bd3725354,0xe7d2c0d6d2c4f0a6,0x69bfd676a24b6a0c,0xbbdaaa503df79c20,
0x1bd7c729547697cf,0x87864604ed628b15,0xf1deeb6475996097,0x63416c275c8164b4,
0x4f7f2aa373755fdf,0x95ac6d7c9b0edfa0,0xe47b04e0789df1c1,0x738ae4e75bf808fd,
0xc0bf7c525223a676,0xd3c509e2c7826669,0x4bf70126fbe593bc,0xfcc3cd42a8f19e3c,
0xfb2b876404d966c1,0x6868a55af2d321b5,0x8d3fe92bc223e3b3,0xb254cb057a72338c,
0x09b0f24697998031,0x365eb9b68bfbd085,0xcb94bae4869d4f9f,0xbbbddf076001a083,
0xbc28c0e6a40b97ca,0xfb894c15501fda8e,0x62f4eb50d2b18558,0xc4cba514b732a330,
0x14678d78a302efe0,0x278fec0bff827869,0x37dccdd798add51c,0xca43a1e914a6bb2d,
0x476a810d81fe9365,0x3cf1c412a5f4e52d,0x859d80263234292b,0xcb998eb32bb29417,
0xedba3df5934cb051,0x6e0aa7d6fc569afa,0x6fc6facad7ca1338,0x365ece256b9c77ce,
0x13326b6bf2209dfd,0x9a875bf9f7f8c723,0xe301afde59d057b5,0xbf940e05ad5ea09b,
0xee065da6e4f4f73c,0x7842a63d4b29bb81,0x27f57f9d326cfc8d,0xe5ed7c5234e8c34b,
0xcddc3d0e4bd2997e,0x1d4064f4296acfa9,0x64b6703f69981fe0,0x063731c3f4705710,
0xd21bb6eea4fa1be1,0xe77099b1596023ac,0x4cbc836a71fdf11c,0xa40c7e94fa60c60e,
0x3803e4609bd03441,0xfca9956cc61ad792,0x56b0b29169638b35,0x77c3112cb18ed6ca,
0x60d351d3202f0133,0x3b369c266fcd8a5e,0xde06e29886e8bb55,0x8fdca6eb9107762e,
0xca51a022d7ed707d,0x7ce31825b9f1d687,0xacc8e6b413fa154b,0x10579143d0df2e3d,
0x2f34e8541f94ff94,0xc80558ab3bc31b89,0xc9c0704083959d80,0xac09265ee1360769,
0xfc73b71bec28e236,0x4aa58583160e0107,0x9fa1701c2a78ec24,0x468c8770f05d36c0,
0x728654cb171c933b,0xaf644299caebeb5d,0x798db2bc26171def,0x2c2afd55d3f57d75,
0x3261614fc5cb1605,0x487e96304f7061d5,0x826873d5a8b6b329,0x343c2a19bf394910,
0x99041f96281761ea,0x4c04fbf27bad11a3,0x74c9c110ad5925c1,0x890c0cf3aafb081c,
0x7289925f5aca7859,0x45a37f05f3fb154d,0x3407ec99f7ea24eb,0x08042270365c7947,
0xed30336c47d38b65,0xdec6991ee5158343,0xc947882e43a4c3f8,0x1c34c45612203c52,
0xfa8e23610bf70de6,0x14cafb0434fbd9f1,0x7de9d73771019910,0xf3716988f3d38873,
0x985c407200ef8e5d,0x8b710617b517bcc4,0x22ba1d0d354d6339,0xc1407b3876f328bd,
0x6693978089520e9f,0x45554e321aa98300,0x6e7be054e5c68401,0x95645b01a02b8bf4,
0x9a5bd069db301ef2,0xc9e981a117115a42,0xcd76e5ba6deea041,0x77c40ba790522c34,
0x8b241d77f16683bf,0x38816df9a9f5f19e,0x8025e0a3f01ff211,0x80e9669ac8e61b5a,
0x284be6ef759b6acd,0xff8fd7cefe43e754,0xa82776a994ead17e,0xabce9447ad91d0a4,
0x078bcb6f66275a01,0x2cd1836dd047b41d,0x313c74d57e402c41,0xde19e72747334f47,
0x442b74d0fc217650,0xbc3e031855c9195a,0x7eaa6ec095e17edf,0x5ce9c721612e58e0,
0xf307ce0d7b805b31,0x605e99894dda7442,0xefd6c45509d31a59,0xea840419d3ac5a23,
0x107dd4c990328d16,0x2e7f035187d075e2,0x46d5c64014b678e4,0xc2fb9ea46d27a9df,
0x2de0f2cbf6ac95fa,0x15009ca6b7489aa7,0x68718cc347e8bd8d,0x1b2742bb80e681c6,
0x1b0bf132c81a166b,0x515c9120e800ce72,0xae2e74846db7bc8a,0x609dd5854a8488ef,
0xcab07edfa9c0f490,0xeefd587a5e2e2105,0x8103a15905b660bc,0x87fe1770d670f10b,
0xabbf8b1fa48df272,0x2cdaeb3d5d12ecb7,0x598f44a19b8cee75,0x3279869a92b80f99,
0x888cac0c38df9fc1,0x1d930515166f4f45,0x82edc74ef8730b16,0x4bbdb1dd553d8c2a,
0x19dae8d03784fdf4,0x0e5f307a3762d1ea,0x00c0bf3797ff7d0c,0x9f2a7f500cbac72d,
0x38d99be6fb69135d,0x39b6ba058d6dd622,0x5d732820971501da,0x4c9dacf397023624,
0x14b5cc64dbbc75f0,0x43cdd75318320d86,0x0055e33d34301525,0x67095e12d73674cd,
0x50512deec089573e,0x33318ee018c7a067,0x638e1e4f16023485,0x793ef3d1ee7e2392,
0x6b3f350112ba95ef,0xd7c23df96c2c73fa,0x803834c665ad42ea,0x96b3b688762c1830,
0xfdfd951d30779b67,0x8db158dfbb2ab55c,0xb66ab5d7831491bf,0x4795e6228e4e9f3f,
0xf4d269705898953c,0xf13d2f923e14616e,0x751c3fd74ea63c5e,0x16737424b6a46b7a,
0x167fd0dbc26fe30d,0xf563da9f6c842012,0xd28ffdbfc40d7957,0xee6cbd7b682d9806,
0x571034f5b9525dc8,0xe4967d42b0a80715,0x2dbc92c5cca9336c,0x9c7fa395c71890d8,
0x5c6b6b1be561e2da,0xe2828a48a38430b9,0x75ef9844a23487ee,0xcaad14100660c13d,
0xabc7c28127f6a9ac,0xd8c3414f0e0b3d90,0xc5367b39ae258c64,0xdbd37fa1cb3bf7a6,
0x2fb5f738f64dbdf3,0x9ed368340594526e,0x07879cd9d31023e8,0x1ceea7856baf2b6c,
0xce2cfb874a98b36f,0x89cd6af457ac309f,0x9412f6cfd66a032c,0xd8a6835b6ed024a2,
0x01b2442fa21807a4,0x2e94bee5a14ba70d,0xe7e3b04b2a22b4a6,0x63af7e3da589f0a4,
0xeccbb2699f5f70bf,0x0759d6a49e3ee045,0xed661f287190f0e5,0x7f3c4df2911c9d3d,
0x95c53c85e7ce86d2,0x90f82a948570515a,0x6c1d163a95d3da97,0xdd0f92b9e53d6a5b,
0x9b79128143ea8e48,0x029b099b6242a035,0xf93381a56e595710,0x92c53524737e79f3,
0xf06a5fc6ddb29e57,0x3bfae9d7f004768a,0x0823cce1518cce55,0x69506538b622a9dd,
0x74fe7c46b8dbd877,0xd407725eb2bf7800,0xd04fa2d09f0f7080,0x63538591b12989e5,
0x2f4458a0877d1f5f,0x71b6172dcb3612d3,0x38565e2122ac9049,0xe7fc948c976d45ea,
0x4b84358277621825,0x47aeb85aba3683c5,0x56150b485f35753b,0x9d7bd7d6d5748006,
0xdc5d6fdcaa06210c,0xde51a53f340cf8e2,0xbab0533aa442b9e8,0x0325f684ddb9abeb,
0x0bb6204131cab527,0xeb3108df5b68dba0,0x9071cf914a2f3c4d,0xea981089e089cf33,
0x5b2ae4cb75fd561e,0x17cb05f63b9a691d,0x43651e21d8b3db1d,0x95a21d28c14876a7,
0x9533c8b70d6b487e,0x5e070e9a53af1b16,0x1de4a4d65d495f53,0x3e3edd460dbc13c2,
0x5d70b4c5c6ee48fa,0x51bd2eac0ae2ec21,0x5d823961c565f56a,0x78f89f89f0fcdb6e,
0x040562eb99b05f59,0x2784991656dec572,0x2fd01270c4a9c87e,0x635d7db8a459cdf7,
0x5c11d23d3bdb3680,0x6a8537d17ed8b6b3,0x814d0dbc8922fcd4,0xd11f8ca55b1f2d31,
0x38e6036d1bb7e617,0xda382746c34ab6ad,0x14e6e252c2b51938,0xa610874690afcb38,
0x44298bf75855fe61,0x733b2958393c8d80,0xb3c6bdd133122ff9,0x60540411ee588c16,
0x6aa0130a969ec312,0x3de04c14776f164d,0xcf160579fe4b2ce9,0xfd1b583390300169,
0xd5162df376a8c165,0x5e52e2a2c8b6d718,0x08f6011f1d91d3ce,0x69d91b405c940978,
0x1a163101f79f9aa9,0x1b44d03c52a16a65,0xe8826207c1294d0f,0xa313f80f84a36e51,
0xad82cabee172ea7c,0x08b76cb36e7c3de4,0x78ff6b22172f5b1e,0xa9c219c04ea140f8,
0x64df1627f81d2edc,0x80f4a70ecc07cbbd,0x88d73cbf553f7744,0xcd86ab30373b4c47,
0xee7b0d964975458c,0x06807fbe84624571,0xe153d05edce89ac5,0x188df9170ca31e49,
0x85a194d8fb13117b,0x49d9f6fc4ef23569,0x7b42d9203c02a90d,0x0248b62acb1d612c,
0xd833db470ce82b96,0x054a03bf244d96ce,0x90eb1a9238e71eb8,0xa52a6642980f0f0c,
0xaf3dcae5c8af3488,0xd12fcc615156501d,0x10fadd9b66d88028,0x34784bcc62de58c4,
0x6cd8a81fa43f3c1f,0x225ad2af2ca22557,0x71478e8aba2d2c20,0xc2d090eca81ad2c8,
0x935a937a97317b96,0x48a96ff01810053c,0xf655319277b730a1,0x707c81c30f14e7c0,
0x599d01f2655d7843,0x8bd1eade97d1dfae,0x7f01c444bdff91e5,0x8bc0850710990568,
0xde2f1200013ccb43,0x558b2fcda10c94cb,0x5614cfb0072a9bf6,0x83c7b0912ae0047b,
0x241856ed408d8efc,0xf393f309a0914426,0xee14ac8efee8fa1f,0x6333868550e80368,
0x041f570089aacb59,0x18d971c52ac0b029,0xced0780669d6027d,0x2d91c1176275722f,
0x93926bc6c07ce9c5,0xc76428fae91b29fc,0x767d142caeeb197d,0xb5a9301c28349989,
0x027b2cc9f4a66a55,0x0463b98791c2bc6f,0x67c808012a321b11,0x8d7daaca47f3655a,
0xbf5e681c53f7952e,0x359069ff644e19be,0x4441f9e64dc761c2,0x4dcd30c58f2b7326,
0x468f21ca79f39ea3,0x3f59b471148a3824,0x9616d80a1cb74f80,0x6f35c921cc03cbf6,
0x1cd59c7d39703a36,0x7a82c31544493583,0xb63c69d4b7041e97,0x3ec41eb6dbc65b48,
0x2c27a848422fd4b9,0x940b4243026d9661,0xaa9ebe952e106cea,0x08700d449a3c68ec,
0xb3502771eca73064,0xbd6b45a9d73abfc4,0x6e5c2c26a92f1954,0x16d417c0e6dc0d50,
0xf3e60b97c86344c2,0x0efde8fbfd308f48,0x6bec72921d5c7d6e,0x7fb262411adecc7c,
0xe3902da1762ed63a,0x379ac83686c263df,0x5da56ccce2011e54,0xf4be374731e540f2,
0xc20fbe5a87b6b1b1,0xc090a30af7c85c62,0xc5033e91e2668544,0x3afe563c6c5ce047,
0x7ceffb210bd9a58a,0xab8bc98c1c8e1ddc,0xbe482fd0c481070c,0xad2405e1f32c0f08,
0xbd112614304a96b0,0x65f6b1ad25a45175,0xf11236aa64935289,0xe34b8a30f50e28a4,
0x042e3ff8e3acbb88,0x41af1b37b91349cb,0x1fca35020aff8606,0x11197361ef84d8cf,
0xbbe7273f846af118,0x3b418e91134cd0a8,0x1ae74414f9eac5fb,0xdc8554800823b7aa,
0x1a811eba90b15444,0x98f1808d3ba6c67d,0x7febaae2cc737af8,0xc4f7fba3f68f09f0,
0x099153c9cdcd1930,0x58f3d5f91bbbbbed,0x290f13a7d6a89ebf,0x47c8dbfafc093f5a,
0xb0cc2866468793f6,0x2405553c9a286e52,0xcc9defa721219536,0x59de415aeb7ae7e9,
0xd9fe783d64275d57,0xddac8f10a09925c5,0x97cfa2675cf327ad,0xad8e8184cb02b0e8,
0x2c3d9a541865a545,0x741ca45531153004,0x67e06bb2dd2771e4,0x20b7ada06e828d1f,
0xff7268da7ca25911,0xd5eb1bd832bf8954,0xe05ab20df7f738d0,0x32a90262c1ffbdb9,
0x05b4554743fd18f2,0x2431ef6eefb3c031,0x44157d9e1d0f168b,0x5c15604b0c27630f,
0xd70bbafb08406ce0,0x327bec42b4a02cd6,0x30e7d2dc3722a9fa,0xc1189ee6e101f5fd,
0x9a9c2d9a6d99d0f2,0x725c320e302d6574,0x8546aecb24e0af29,0x5b0a541f9617436d,
0x09078553ea366012,0x3f405c14b500d15d,0x2ee44dc1bfd706b8,0x6a8cd95a94ed856b,
0x3a2014304101fee1,0x33308b81d45bb8bc,0xf358abc0bb55f5c7,0xa9baeebbaced2773,
0x1b6960e7adbda62c,0x5a2f51452f23a009,0x35b68712001c1340,0x6ff56e413d29e576,
0x0751c5ec15b0fc7b,0xb2ad76d7acbd348b,0xd99bef6c05359e34,0x9f7768a0776c4ae2,
0x3c42b049b1dc66bb,0x5eaf172cf0eb116d,0x2baab2ff0631791c,0xfcfa03f9aee85c01,
0x224aa4c25c51e524,0x81f0d8b57154267a,0x0e30891d826d9c56,0xe5ba08c3bd252bf6,
0x0b869db61a4bce14,0x5af101ba30f8a1f1,0xac038b69392b6998,0x2e63887007f0ac42,
0x957c986e3b10cfa1,0xfe329953a3547241,0xf679002185b93e27,0x5ee80569afc6f4cf,
0x03ab592e1dc06fc3,0x84f625d54aac4d74,0xba629a7bb71bfab9,0xd0e859af418aa84d,
0xa0c068b84fdf0bfe,0x8b9ad64723725382,0xbc52b2ff37e96a5b,0xc201cfad15c868cc,
0x8276453b484bfb54,0x03fa7a7246c00b15,0x635a5182b183d9e6,0xaa4490b4863e4a12,
0x3d0df427b378ca5b,0x339a05c3cc9f415d,0xb8bd4ac37ea40346,0x24b043a8333eac4e,
0x06159afafa31da23,0x0041373e43416a38,0x6f550b27e9e935dd,0x758c7c895c5e0c4a,
0xb9a41a856adea741,0x26d0b0f012a5a727,0xb3077254c0c10653,0x4dc6f262d7606dbd,
0xd71e8859dfec0cb7,0x924418604c6cd696,0x251e1a9b4366c847,0x11d34089f5379dcd,
0x497f3a8d98d6a8bc,0x936744935bc02997,0xe59ba4d0a83b6a59,0xe8b0442fa30f9766,
0x873a0079760106a1,0x97ed4e7e9742ed0f,0x75da8b324db5a047,0x2b3371e8bc1ecd1e,
0xa40137be7c96d0fc,0x1e78403a2ab93056,0xb134fe9a44da28c4,0xe8602d02ca1d89ef,
0x6a9def48c0a884ec,0xd7725a9562e21ced,0xbb1b51211c9507d5,0xcf1a1c1f1e38c31f,
0x026818c3d2ca4d5a,0x808f4597ebba9040,0x635125ecb38b07f3,0xa9fd856ed19611f4,
0x317798cceb2ba044,0xd888fd2d5a675481,0xbb5749e38285abd8,0x267e2af1ac234df5,
0x1b0a171fe3d85afc,0x20938239828887fb,0xa0f29d2c56734f53,0x34063e16ce8a9c07,
0x83620825064ccf18,0x517d2b14f5627e2a,0xe8064139682c1467,0x321be27f81c4bd5f,
0x8644c5ce16b6c361,0x9124590b48708e4b,0x9a2b3c72d99d730c,0xc196b3e0b3542dfe,
0x9103840862658ccd,0xf5f773920d402422,0x90d0a7b438842bad,0xc907ee288ab7cc90,
0xee558e95a1e6456c,0xd0a5cdd91a4c9f75,0xaf7b4d0447aa3e9d,0x8adb7f4aec16d1a8,
0x34740187e66112ca,0x6534a6c9c0a47f99,0x47d3d4ef7fc5c0d7,0xf71d270df0404da9,
0x699d0b37c98a40f9,0x92f02920a071a334,0x6f73bcc7887a9885,0x76a9e8c729383721,
0xf0aec112a17d49dd,0x93a051fa8b8cb9a1,0x1373aff8e00f41f9,0xf29e783ccadf755c,
0xac8c4b1d20d0b71c,0xed15e6e94963717d,0x0c3f8ec7f03372b4,0x3b0bc38b5a28853e,
0xd20d157e0064edab,0xf44656e0d0349bad,0x761470db58c5181e,0x364944ce8a2a06d2,
0xf385ef718823963f,0x4914d100da60ab83,0xc5bd85d86826412b,0xb9b00734f0772cdc,
0x73a40e13f59d5fe1,0x0ebe503d96d47c51,0x96ef81b66e3e2a02,0xa7d37d47ffb846c5,
0x1529b80406b44b4e,0x9644c49d1301cd5a,0xd45b4208a8b13283,0x8bc82a9aef6d6790,
0x051f083b1f3f30a6,0xfe0a7715b2752732,0xcd7d52fb04a67d47,0x8e3cf0d7a091f5a5,
0xbffb5b2d01a19585,0x9c18b074d56f2a2d,0x609ca2e8de8d1795,0x0742780f4821ff6f,
0xbd88ca2d4e8316ac,0x0f37cae508c0468c,0xadb16e013ea0ac00,0xeacf578eb2a59839,
0xfd7eaea2fdf38f80,0x2d7f3f8de58c9a67,0x97e0fe9dfdcd14fa,0x345a71c4dc4569b9,
0xc3b59bd0414b4312,0x0ef976696bd77480,0x8e52f73522d287fa,0x32806a49247f9948,
0x8b0e82d84c173d23,0x3c7fe3c9633d1e44,0x70af3482926537c0,0x1af13ed6bb139b7a,
0xf1d3154f6360392d,0xc970e4e43f595f00,0xd2d8aea7f033eaf3,0x96c413e3d3165475,
0xa1b1dcb95efb0c06,0x428349babaff4520,0x384ebde4ac3c29a1,0x7b9bc89ae1474d16,
0x1f87e1a71d5f57e0,0x3a6dddb7d9ff0418,0x3cddf00608bc3375,0xb4300e39a572d80c,
0xe377bc1791e6d680,0x9cad757e1bb50cb8,0x7bc097520e1650b6,0xdf78dd28070be932,
0x2ed4000d2cc464de,0x62c99df49ad984b1,0x57dac85f1c976149,0x616d7c9d7b8ff424,
0x50aa1ebe53a55227,0x8805b152b1c712f6,0x1b86130febd0c797,0x6a5f533460d21c15,
0x6b205a28b08867fa,0x25f0b4f452356e59,0xb501cbc2da85ba6b,0xa22bd88abc39ec3b,
0x48d56703c97aa408,0x056a1d150f64856e,0xfec6a624536d614b,0xec2ee16242a8c32e,
0xc412ce1caec1dd2f,0x4da0c3f0d9c1b013,0x91cce18654d2ac89,0xf2bb21933d7965eb,
0xd374a6423e861fc9,0xaaffb58d5ae3ee91,0xf1bacfae4651073f,0x75925ebbc14e4005,
0x92a50441ec6853b5,0x80dbfea2f248e5fe,0x21caccb5349b241a,0x95d08d6f08aeeb35,
0xeb4abe614f254435,0x7c73108534b9fe4c,0x2264d181bf2c034f,0x4caa84af02b6284b,
0xa4ec7613a886daf3,0x0ad25e09b31fe555,0x3e39d1c8878b9df6,0x2a3b5c0559969593,
0x9d28e6a2edbd64d1,0x33d33c2e1b0aec66,0x3a3ca403bb4030f5,0x0c9ee60946415c6f,
0x4ae24473ad5104a0,0x2347b5ce88385792,0xae322952cda2e887,0xda35a5aa031ee822,
0x922bac465c10182a,0x317292c7f4168038,0x2ae061a054f23405,0x98f3c5b85f79c1b5,
0xedb18884e8efef4d,0x7093e64143776ace,0xae4847796de71bfe,0xa4917fdaca498af6,
0xac39f48fc2dbed91,0x68ff8109af4ed8fc,0xf08873ac44d6f5e4,0x115303e4bf654255,
0xe7b5353533519cdf,0x19ff8bfdac5fe60b,0x8576351c02e8bcb0,0x96007a5c0bb48b00,
0x5d7702b6fe3e99b0,0x6d1416a8b187e391,0x12cf67c5bec7f0e3,0xc81fa7c27bfa69a6,
0x8c8cf45c6ff76d0b,0x06c069996a2078b9,0xe8c98b81ea4d306f,0x466c2fd2a30cc88c,
0xeab18b14dbe45997,0x1a3cea5024548e5c,0xa2857f63cede58e2,0xfeb0c9edb387b730,
0x9a8e2eac60a99d5d,0x8509412a1e88055f,0x8865448dbba65db1,0xb545b5cccb261456,
0xa9c4867e45e78a6e,0x6a9fa358b341515b,0xf003fb85f76d9cb7,0x866a858141ada4bb,
0x514da90a2ad42d28,0xbd8b5c9f2bb0408a,0x8018a12f898d02bb,0x51695a0fbfb5a14d,
0x25c9d15cb32ffaf5,0x7e85758f4dc79ae2,0xb09dabe2556ed785,0xa4e38246c03ef193,
0x54376369b77be962,0x0ea30f8acb77dd1c,0xa7b29a8af76256d8,0x1e53f739cc76d26f,
0x3d30e4a21d10edfb,0x52b65fa2987ffaa6,0xa382553f27f870ab,0x14ccf003f58bd2c4,
0x6b001b5bccc40817,0x912d8a5780ec40d8,0xd173e6298e5ebd5c,0xaa1e68d6cf28b0fa,
0x0617f5d938a3a4dc,0xca49cbf577cfac9a,0xcce8d3837b6155a5,0x75ba5a697effb59f,
0xc9d54a64d7d53367,0x12d380c19a621bd9,0x0bf951fe21d41257,0x397b365101a5d0a4,
0x39d64f5da667ff04,0x0c094eca74b7dde7,0x1be6f5747347ae90,0x6bd46a6e00c5a0de,
0x9230120596b1285a,0xc77fde1e4479ee22,0x5c8673fb117440c8,0xd1df3ce0318835fb,
0x77b4a9d775e3e1d8,0x46a4e4fc01153600,0x08d9371dc2e5f2e9,0x3c2a928fd268ddac,
0x54f039947ca37a8d,0x4bd30ba0debcd93a,0xb69d822e982fde43,0xa20bea1125d03333,
0x172b03355982fcc5,0xa9b01f7079d236c6,0x36e3911396087a97,0x22c03df1ed8622ef,
0xde2a6c398e23c261,0xadedbe60dc911627,0xad13e6f32c9032ad,0xbda9164b938c8dd0,
0xe429c453ac053b33,0xde1c60e615b26d9a,0xf26f5379d76479ab,0x70566c33ac43572b,
0xd50ef73cbd1d0b7c,0xc05310b720d81962,0x386ba8cc69fa2b44,0x74d1eda389ee59e4,
0x94f19799032c4852,0x4a5ae76cca68526d,0xb0c61f14a89dd9f7,0xc2058a1a4a8de98a,
0x95224e21a359e430,0xe76bdb6de3c7b577,0xe63d568fe12c379f,0x40393d76c91e5fb1,
0x578ba23bcb9f2c50,0xc03c058af1910fa3,0x0b9080fde6afd1df,0xac2df10df77e0b7d,
0x7f6191e078823537,0x2465afeb92f19115,0xe6f77e44ef7b69b2,0x4c148942156a7569,
0xaa96aedf86212541,0x6967c9d6c534f7ba,0xbce3940640518d72,0xd7fd29d8533c9114,
0x413df4d9f2b51b94,0x782040eb52bb1ff7,0x16b5f57393c84393,0x48511ea8a34b934c,
0xa5529d2f9e180b9c,0xa0e20457a0ee8cc0,0x85ad49bad7c4b1b4,0x0db26c1da98a3d0e,
0xaeeda22ba1e6fd8c,0xb7c84285352f3fa6,0x4fddce30394c8d48,0xd94ab50a0c85c8fa,
0x5119730d618a0b39,0xecd818c1f3447f8e,0xeae889848ea9ec32,0x733934a66113fc8a,
0xad78fa630f91890f,0xb285b601928c9967,0xc780166642aa1aca,0xacb9f9e516eb586c,
0xdedc29d995f02922,0x4a8b2a27d4a1a246,0x021f7cbf0deafad3,0x9aa31c3e854488fc,
0x871d79f6d2990bef,0x96b076ff90ef5662,0x2fa059becfd32e77,0x42fbbe7cb1bb0108,
0x95bace515e23d8e8,0x5cfc3c6790fc2e32,0x00585cee7c0b81cf,0xf933297f8e48710d,
0xf170ca4306d9c27e,0x1c9ad734a3a84612,0x641dfdff5bc0410d,0xb636f0ee4933c880,
0x836e3b8444d99a4d,0x67a02c2d1c2139a3,0x451f306d82a8eaba,0x599ce454673132d9,
0x2b389bba89cf58d4,0xa91b9802b5ebf91e,0x794ea5ceaa892ca3,0x72e22236b083f059,
0x4075fe51083045f5,0xef054e11c62c56a0,0xc3287aa0cf76e92c,0xe757bf90bef0f62e,
0x4974afd0a3a7cf38,0x99b523098002faf3,0x370cab4cefd8fe22,0x6dc5aad378edf65b,
0x28ab0d008a67521a,0xf843417558cb200b,0x08d9d5955a49c8d3,0xa274c3e6d554c36b,
0xfe89ad8ca937b6af,0x725c803678b5122a,0xaf1ac2abbb880bc7,0x9a7abf92de5ffb0d,
0xd7b5f1506aa1b1d1,0x8945cffbc706d94d,0xc79c9bfb7620f9f6,0x99c5d03125123f1c,
0xb9fba80bd7a49a7a,0x8f0c02c1b86c8b0f,0xb4d2b27a285f6953,0xa014547bb0cc2cf7,
0x983fb0ea3b0ba275,0xfc74f050c7901655,0x4a22e16ef4a51987,0x6874bcf98fff38d4,
0x35a7373a198c4637,0x218343cafe36f02f,0xfe90ba59f997d08b,0x77070cdf2e26b55b,
0xd16c6ffb9010ab25,0x91c68339e4edb15f,0x36e5eafff40ac0e9,0x3306732827977332,
0x487a3891a476ac9a,0xd7e4485908175106,0x2f3ac8525bf08ef1,0x6b84204092f76bf4,
0x3cf652d5b805f0b0,0xe07d6e816813cc14,0x3a8da3e5a466213c,0xe1ec141b8796f489,
0x82414033074b629d,0x805b1f555994d6cc,0x2a5505f56f11039a,0x698e6c22727cff86,
0x460ef99541fb1613,0xe1d41f774c853909,0x1b9bc70bb5c2860b,0x8993263e7051b844,
0xe88df532445c7867,0x37e017b4f922fd24,0x17fe5304d8e7c4ce,0x49dceecd231e6db6,
0x9a4760a733c7cef2,0xd2bfdf9fbb50450a,0xa8e5a08028aefa3c,0x80ad8ff089b033fd,
0x268cc95bc170f098,0xf6f55ce508aa4ae9,0x72612f8ef15c42d9,0x1788c41b3f7672d0,
0xcedd59148ea3cfa8,0xba9fda428c317202,0xb80153fc536e8893,0x883932a4717e4348,
0xb0cfe80e0e9fd865,0xcf2886e8bf883d47,0x449bd7aea8b737fe,0x198b0f099698896d,
0xf65b5c940d939347,0x59d5894f8237488a,0x55d61c252cfb1293,0x572f14688694b183,
0xf8c5e0549fbaa3fa,0x7c702f8c3e7141f2,0xbc5a09db2308d152,0x449d52cb77a67b69,
0xecca22ea15f7d56c,0x03d0bb9bbf6a84f0,0xc44110a3cee36186,0x377ad0c81e0d3d6c,
0x06601fb52344e96f,0xe25a3a40113071ea,0x09d6f087534a4533,0x8f44c5872debd9f4,
0xf1d2cf6e8f69d787,0xe9abe90743c99c30,0x573563c6ca30927f,0x2cbc1e9ef779b565,
0x895c73194c3086b7,0xfa1263b5d3ab7c6e,0xd20ac7a60ff67642,0x22c852bcd25436bc,
0x1e1fb19ae9ec9a28,0xf354fc2355184376,0x38d51656348aca96,0xfc58c73334ca89a2,
0xb9247cd7de6dc9ef,0x82ed3fa8047b9161,0x1e082207bdebc53d,0x56c02ba5165bbed7,
0xec0c658888d2cbf5,0x092cf1900289a644,0x62c0178eaa446f3a,0x3b4165fbf9380595,
0x29142bd002dae9bc,0x62d7f97396289da9,0xeff04409723a4e05,0xf3c784aaedc08597,
0x86ac8bc817cde18d,0xc40594e2825ac54d,0x3c56ee593629692e,0x7892b4f16fcf0932,
0x4985fb5fbef6a0ab,0xd8927a1e3103b545,0xeccc202ce36a50e6,0xc455fa13bf9aabff,
0xac0e183d3a0be477,0x275a1863f8428aaa,0x984105e2b6ff4e1f,0x17407b81876edfdf,
0xd01ec8de76395ed6,0x1243ce25f6cfa0af,0x8ae77a8110d3f0be,0xc3dc0052a37460de,
0xee5fbbe3820f43cf,0x5beb61fc42ccc84a,0x9b607f5c0c2cc54f,0x20021a0f36835809,
0x03af145522e0164a,0xb5a3f72b9cc6c2c1,0x5c8e1a17474148e1,0xdec8be452ec3287d,
0x24aae9b035e63d74,0x29d1c12f7bcf174c,0x9f54abf6b717a95e,0x287ba4aee5b57da9,
0xcd0e14a2cba0d36f,0xdd73665a22b62a84,0x9cfee746b4995999,0x76e2ea730f4eb24b,
0x1cae73ed0538afa3,0xb3a79f044debca81,0xdd89ca2c44f74649,0x691dd484aabf1694,
0x7c0b91fe41b96eba,0x3c3db3d8d7592a2a,0x54a2537b1ac70230,0x86100ac0f35cc2a7,
0x9ca35e5fd9176ff1,0xd853e6c39bfbe007,0x54ce92b19699c1c8,0xc40fcc16a2379f9f,
0x101fffbd1b920e07,0x5151f44e1ad8d92b,0xe4fd7ba6c370d52c,0x1cb3669a0e2f3c09,
0x9a57706b2462da38,0x64b0da6cb83fdab3,0x7ac06ecdcd1eacaf,0xfc7bacc5cb560ce7,
0x85e57816a54f51c5,0xcbf0220b00716cba,0x166fcdbe520f6802,0x9c688c369d5e72d7,
0x8e43a1d26487ba02,0x7a41fea18320026f,0xed2dd4aa4482a7ce,0x47a1a2f01789a70e,
0xbe2522f4d1495241,0x2e9f4d4774256890,0x94380780edd4e449,0x9d0dcef9834fe8cc,
0xb1ac8d5589c637d9,0x39c4bfddc82390b3,0x0e87d826d1239a82,0xfe42d599f96064df,
0xcd177a4af9186505,0x4aa61916188d95cf,0x28cda0d0d29687e0,0xfa1195f79b5f0de9,
0x65088b1e07bfc16c,0xb786ac48b3cd0348,0x3dbc93f9d2f05a34,0xcb9fa441fb18aa8e,
0x2a101a2109d6aa32,0xd08299c00e93f82c,0x7b548d6b51abaeca,0x21c0fa86fbe5c691,
0xf7e4a73bdcf3a86c,0xac23fc0815014962,0x1124337e3d0c40cc,0x3b6d81b1193b8852,
0x3abf519eb9498228,0xfaa9d5d691ee9761,0x690c165d2d643c5f,0x8b07dde30eb46f68,
0x0806c5ed15a4be4f,0x459ff1a86ce33041,0xe53836be15554fe4,0x295863786302fab2,
0x1a4d95edd1406018,0xfd94a9ccb006a004,0xbde31309feb549f1,0xadb1eb77efea076f,
0xe32c9223e5727b1f,0xf7516a9857eab602,0x34d1329e23c3db0b,0x8049d85488aa94ed,
0x76ff00f2c84d88e3,0x23ffb7ad5de4f9cf,0xd7d73f3ffe055432,0xd4d01fb41a24966d,
0x0842157140af2cf9,0x577b0e5bd10995c8,0xe883e65517312e59,0x0d55985970ea531c,
0x2a063394f8afa2a4,0x0ca10053bba7b116,0x8daea32bf0190a0d,0xdc0339b2e00c6b04,
0x47db230f8bcf7488,0x43c18e897856f46e,0x4c49c15bff22217f,0xac26c862f4ee97df,
0x0b500943339053bd,0xd04269b78f41a2b1,0xf6ef2c4d1cdfd14b,0x72c71792ec349147,
0xa48fe78c7cffad00,0x594e9b2e4fc09998,0x99272410a43ea2c2,0x925b0da6dcf01a6a,
0xf3d6609cf35b08b0,0xeed91ef702f66220,0xb5b424bd42ca58c8,0x48aed86093dcf2ae,
0xcbafdf8ecb8783ca,0x84c82cf7c9b2a738,0x6e576d9117f834ef,0x6b7c9a8740b3153e,
0xd0e9d935aac4b754,0x4351bdb475eed811,0x156ee8b9b5ef9f1f,0x5db56aae200acce8,
0x2be6660ce6573767,0xfb7468b007295252,0x05285f076bfadd31,0xbbc0dfae3a66901e,
0xa9b6ae32fcc5831e,0x930604fbdf657efe,0x6b8f3a0ae644a80d,0xbe867d549b975064,
0x1537e1bc73a0c1c9,0xe626b3c990f85a7d,0xc331a2bd92d188c6,0x631b013a25005f78,
0xda4670e5c08e9cad,0xab54ec8caebcf8b8,0x4f29074f655097b7,0x51829fc5f6988cc7,
0x6e40f63229614baf,0x8cbab1758a52bde9,0x13c989219d558ddf,0x305fb8fc183e334b,
0xde9e3cf9532a882e,0x0eb02ffc8628d847,0x126d1099cb6d735c,0x2914a2c7bf4f54af,
0x91e7ad6e77ea55ac,0xd5188e22cbf389c3,0xa9fba5ca645cfb42,0x1e284af5640c82cb,
0x80abf36def87872f,0x5c1b53dd3c9cd0f5,0x987253d615e30d58,0xd8d9d387ef54ca3a,
0xb9ce5bbc633c98a8,0x78e3e1ff82c57445,0xbd42363f7074e879,0x5bfe3e564c0b7780,
0xc7b0b06725d5f8ac,0xadca42020c73254f,0xb528bea3ec6f5ca8,0x1ce882aff51ad3f1,
0xf7ede13cffb8ba20,0xfa5c2e7e1be87c9e,0xc835387444e2f9be,0xc5c77713d4d6a487,
0xabfeb579feb18939,0xd0d66fee84a24b99,0xef6660ddb33c77d7,0x169614b1d1c94d7e,
0x27be8d0093a0210d,0x03bc13d397bcf182,0x0f3cd42abcd23ed0,0xc724e575488244b3,
0x67d3e949cc390b1e,0xf29ab493ceed5227,0x88aa071ec4baf684,0xfe20277380e22367,
0x37a2a4e99676db76,0x20b852c667b42d66,0x97f219c80d242e74,0xfd04f09f90ffa369,
0x6114bf06385d98ea,0xc1c90fd30b14c7bd,0x3fcc4b4ec48ac19b,0x3de30bc900e3b6b3,
0x3d3b28201995b0be,0xf669ca1030957be0,0x9e48ddf4483aca1b,0x41eef58fdd0c9726,
0xcce18f0ac05c472f,0xa92ceae1c19af1d5,0xbd96a92c087334a1,0xaa311024c71a2816,
0xbf462d74709727e3,0xe2f55922a2bdc149,0x17b98fe8a90c87cc,0x9f458636ebb1f6c8,
0xd867f0ec4d4e87bf,0x29b9358b17739f25,0x7528fe773d961160,0x0cab5310f71985b3,
0xd6b144cd6b8f41f4,0xa21907d5c4b7b377,0xd3c78c5ce5cc1045,0x2e2e20f32eb63e09,
0x8692723124468fb9,0x5e139b0e4c6e27ab,0xb8e9163b627ad2e7,0x7eb5802730f5d592,
0x78f61ea660c9da5a,0x6c0fddd9516897b0,0x107ff40d5fd37c12,0x1ac48dfc12393091,
0x6480634380fc57c5,0x3d8654d56faaa4e7,0x21c9e686342ef867,0x69a9d3ad6fe10259,
0x3151b59cbf7767fe,0x9fe9cf2ad2665820,0x49030b7ba109e396,0x723926ec30ca1787,
0x989470787e87ea4f,0x00f831d6a38589f3,0x3ab23e8ae6fefe00,0x277758bfcfca0313,
0x3ad3d56255e91d50,0xf2df87b556b3612a,0xf67c765be84c10e6,0xe6421d4df7685afe,
0xcaab15f59d865c08,0xe093cfeee2337c06,0x69e2f860fb488485,0xe801cbb114a05481,
0x2610fa02d5157acf,0xe139a71253f381fb,0xe8795ee8bf400e01,0x27c24467687f42bc,
0xd01405ef9446803f,0xb7a16c8e1058a2ab,0xe8ee3fde3bf27246,0xd9c86d1b2a2868e1,
0xda69013e5a943342,0x9aac11d53cbe1acf,0x8f7a3309cf30a518,0xb01d5f448ee8bb3b,
0xa96be25ad762f847,0x99ac69cefaab920f,0x0d468d6eea644a90,0x01890df9f373f418,
0xd2eb21fd57d5583a,0x08e3317687ed7f33,0xf2887e38d8518a09,0xbe6882eb261ed18f,
0xd435d3998249c82b,0x034666724a5a439c,0x76148f4fb6b8313b,0x8148aa176ab5a8d4,
0x6561f83eda9f96d3,0xbb1369f4862850ac,0xcf6de429fa79b03a,0x71b2b7b78f41f322,
0x7b5198586288b463,0xaece6a3eda39360f,0x5d8c39ef0a19efaa,0x3cac2b1ac03d2a6d,
0x1ded9ab97bf27f2f,0x3cea4d472042303d,0x0c1a4e456d83738f,0x15881e9d9e23a15a,
0x8a777dcc9a2e4370,0x76dd9164cd21366d,0xafef663db3aeefdb,0xd0a77b6326f3aadc,
0x746f06f69676c58e,0x0cf1911c6ff3b61b,0x7a9bdac5391e1d8b,0x8ecfccc5c1bea9c8,
0x194a2ddb8bba9266,0x4b838366eebaff30,0xfe8eca93814ff21f,0xd4ee0c51e3c75383,
0x3e00cf5f4ce2a5a3,0xd235b104d5c9da6b,0x7b41bc326c9d0158,0x9781730e65614b96,
0x4dc39d1ba65b60ea,0xfad6ac983c352ef2,0xfe9e16ed82bd040c,0xff3d355f0fc58653,
0x37ea56def1db0423,0x80601389602b22f5,0xaeef1faba6c2fd44,0x61c6fce3a5028837,
0x4f7e451d3ed6bf25,0x5496b0e28e15d491,0x7ee18bff37d88f19,0x0caa7e2bf4b35df9,
0xfc7cda1427f72ff0,0x8f9fb3ae35c06d60,0x2099c7c7e2476835,0xbbb000dc15fd6c3b,
0x48c5fad75cdd59eb,0x4081017e250651c2,0xcf160d09ccab3b12,0x4eef01a49168149e,
0xf969d7cc90c6234b,0xc4d40b407387dc03,0xbee0b3e9939377ca,0xa7c0bdbed5618bc2,
0xc444b98fd705b80d,0xf0801ac7f8d39d25,0xec8e00241daf9704,0x55e2503455e7658a,
0x7eaeadc632c123e7,0xb87d499a45e37f8e,0xdeaef7f31d06b685,0x4dab984116ab4611,
0xfaded5704fc1b451,0x2b66584fcb1c463b,0x6bd8be9c6cb3cd41,0xe75a5b2c0516c28f,
0xda9009a6b896f217,0x29308ddf7daab1c5,0x41b3a4fe5c2cec4b,0x4c0f154505f4bd0b,
0xdc01e3c53c000665,0x3475c462ddd864a9,0x415c98e2549116e9,0xa7f7be8eca7a8371,
0x277164248e1847b6,0xb8c7072c9c6f1d71,0xf9d1e1721c654800,0x6067a3f67cbd6391,
0xae6894f0033f9de7,0x80bcf8daf5f26ad8,0x98cf0d44fb4a887f,0x1c405ad7bd57730a,
0x6c345bf997d8346d,0xe57d86d65c78255a,0x7ddfb7fff388040e,0xde4badded7406041,
0xe6b47bd6adac5e6b,0x5dd716ddd167ce4e,0x83f9189469f6fcdb,0xc4e0f9616f5b5474,
0x1d964e4bac8f065b,0x3aa08484037ffd48,0xf1fd776a98d3fb99,0xa1947bafdafe88d8,
0xdacec5f6ac16989c,0xc5de261ac2c291b9,0x2e3c901ce7ac1494,0x584086f64cef026e,
0xe7b30bf4be478987,0x387d99e69b8b71b6,0xcbd863b284d0dfc0,0xed4926b7253cb93a,
0x8d003a154d1c755a,0xe7979ba6405fc679,0x326be426aa47490a,0x6a0ad76ed8d05bfb,
0xa5da43351684213d,0xbe6b684e976acc74,0x8c7c1ecc315e28e7,0x341886743a699fb7,
0x4bf29c662bddb5a8,0x20e20f199a87dafc,0xf614b6cc1330f632,0x5acec3a3e20a3e74,
0x5852d0837baee997,0xcb1d0e63238a1398,0x8701d3314a060eef,0x22095b061ba892a6,
0x47badce10d4bba66,0xc3a0a12864164bc4,0x2f0257a04ed5878d,0xd82f07a4c5fd9ebc,
0xf970bba128ab953f,0xe45b50c00f206563,0x3202f7cda386fae1,0x749e94787e5dea20,
0xcec0829aaea10036,0xda7a631610787789,0x29fe02c53926c887,0x29b7195a89d669fa,
0xe97e9cec8dbc3327,0xe5460087477a9340,0x39c2681353030c68,0x039e4830c1ec6ca9,
0x129e7bb1a6da4368,0x75f60d29ce90a0db,0x5b07df0a26dc4294,0xe3d5c4f7f3838def,
0x99c06e61c406b312,0x615442d1dd16b1be,0x4d03015be8e7e6ee,0xd411c7053a087980,
0x05f826529e10659e,0x177ba33a1e7f152d,0x6ad5fd60d1a9a65c,0xcb247f1024708dc6,
0x90ff48eb25b6bf20,0x390138050db833b4,0x7b9360888020a818,0x416521bce25d6713,
0x2f5e1c0bfca9e5da,0x5f405c6f23eaa278,0x8ca705831f543ed7,0x1ef6497cc177e002,
0x4f2ca8e033ebdba8,0xa3f1479e46dceb02,0xcdb9c51101e1d28c,0x32cf1369b4e1ad53,
0xb5f399bd668642e5,0x921e5121d73bab2e,0xca487e397ee82d97,0xa64b6703f0383244,
0xe6de33742b93060c,0xc6f1354726dfcd17,0x04f38af7686ecc6f,0x392339f2bc4052f8,
0xe752e0c220586b58,0xf8f2e53c60e10918,0x73531e7f73a3bb12,0xce687d6102a4fb5d,
0x2037ac6ee52d0102,0x78893bf43745c951,0x9812fe448716be3b,0x7bc67b1d5e54067f,
0xa86cb333f8a45c23,0xae5a28c26c4efeb5,0xc5463ef6581a8956,0x020fb4957dd38fce,
0x9d5e5a8fcca55267,0xaeed96dfd8498acd,0xa340e0eae316b08c,0x63d92c529a4a83dd,
0xf63473a40d72bae0,0x84efbeb1d09626bb,0xd2c5c095f5a70fbb,0x75ca9316b7313b44,
0x50f2bef53098cf59,0x75ff1f0d442961d0,0x95cf9e95494778a5,0x30b289bebb31b227,
0xc743bbf1dcf68a60,0x271eed318fda9904,0x3ebd33f444fa6af2,0x5d594e3590d55e0f,
0x7b4de28dfb304c33,0x0aff8cd839e8e583,0x9987dfa166c1f773,0x9bf98a42886f65c8,
0xb4f44344c0bffbf7,0xab6372c171da0e05,0x2e2fa6467be943eb,0xcffc19f1edd74952,
0x0416da3aae4e902f,0x71253fb9dd3b830c,0x24b9178ff90c8c9f,0x732dcd2709ab0682,
0x19f0fe0776c818a0,0x17f22a0dd028d58c,0x22a23c7756fcb3b9,0x94ed3cfed32096bb,
0xa261df8354295857,0x1bee6b235e985381,0x82f79a06c785573f,0xf89e965be2cc9750,
0xba02a6a8977b50b8,0xea10acf1214be935,0x99a3e3d82fe68226,0xcc65cf4a7960f369,
0x8a5acc07ad4480dd,0x3003e73cb9e8d16d,0xb7cd67e853deac58,0xa12a490ed294fe20,
0x72dd1e8254047367,0xb3124f05888a9cc3,0x4c609f42a470391c,0xe9a207e4e09ce1d4,
0x81d9cf8be1a0921f,0x73ad3ca84c96ad87,0x61f01b60030b731c,0x3c3f8e345f4b8943,
0xfadbcd44c47c7eb0,0x09aaf05d60b07acd,0xd0fe8e77a8e189c3,0x15eb0ab3b71964bb,
0x492ea1f8bee4ebaf,0x82c080a7865303cf,0xa0f4ddfef22272a4,0xdb772eef14584cb7,
0x9a6eb833d466205d,0xce6fc1ada5bbd500,0x070eacd48e4e06c9,0x38a8f2e00f0ae21f,
0xe2ae2e488573bec7,0x976d77d11acbf64e,0xea4855a41ce9a0a7,0x035a550d049aa5ca,
0x248aee4db5fcd77b,0x306a846a6fe3d475,0x166b22a83a522c48,0x1919dfcaee0771a2,
0x01cc2e9c3dfb7852,0x90d3ba1bc040e840,0xec162bd1c530bd42,0xcd93dc2f6833678f,
0xa7b5abbf7e7af260,0xe2cb27ffd538b9d4,0xe8d71168897f04c7,0x788d54bbd009ac17,
0x76598f387ea69b8a,0xd2e86f0d1495a3e6,0x2d403ad711c6a6c7,0x9c15d369240227cb,
0x783111234513ae50,0x6241b478c6da0f0e,0xec42f694e96ee95a,0x339541b37c75b423,
0x3e9d626cbb1b7d2b,0xc3224fa38d9eadde,0x60eda07caac9c5cb,0x66d8ee08b733136b,
0xeb6c8a0387cd3ea9,0xac56ea08a1570000,0xb895aafbcb3afd03,0x7efea021cfb2640c,
0x228de8f1c34f464e,0xc2c700eddcc6d90b,0x7d5d6fe09ea33f1b,0xfc8e93c0e12e3233,
0x7aa76c245b57528d,0x7ef7420ec6079fc0,0x3bf0014925355d59,0x7ff1289434e16243,
0xdf05d2fecfd94d28,0xeaa95c6a5bf6fd67,0xa58837b2ec3a0551,0x95c1dfdaaeed6cc8,
0x63034af41ea82ebe,0x35b89cae76ac5ac8,0xedcc4570435c3d12,0xc4ffae1743728776,
0x8eec72f9572769bb,0x2f12691fac009074,0x0d7004038880f320,0xa2c6e20ce2527b65,
0x5ceaf6c89e8df4b2,0x49f60cb1cc1208bd,0x3c402a08d3e1ae63,0xe81e0dd56da05ae6,
0xd1d51bda46ef97b6,0xa8b354647c2283ce,0xe2f4f3bbad039f4e,0x96247db39717e10b,
0x3a0aefb42afea853,0xb520b7958cb97996,0x4733e43a6b13c638,0x0ff277aa56992b3e,
0xa5edfa6590b7af0c,0x2a01fc2cc131a750,0x78b2dd36ec2d3d18,0x84f96bb40492dc96,
0xe52cb2e2cc282815,0xd6d1167fa06d5ef4,0x1ff267cebfdfcf33,0xf14a572a7154bead,
0x8d8bf9f2b1576df9,0x2aece6d32fdfb634,0xf513bd8f2fd6e84e,0x5e5ceb0b8e549349,
0xe50a3cd646edecb9,0x6e2bb0be302911f9,0xf2206c828418fae9,0xaf5d6c68872be2c7,
0x655f69e5dfb9e84b,0x4d96e5774d127295,0x1c069e3400345bde,0xfac96651999bf06e,
0x59d87e095e81e252,0x931539601345fc09,0xa4108b4f2d1d24e0,0xd714d355a71ebcfc,
0xf85c98f185363cea,0x01df39ea3db0319d,0x12ab7442b4f9b206,0xb7ffba097609433c,
0xc4600f3f6e0fbf15,0xe3d013dbc4e886df,0xbcad23f253b25251,0x4a5359ce156f9011,
0xd875b8595ec93b07,0xf21c80d408134587,0xa0df1a96bb247169,0xeee4413dd154a789,
0xd76acbf204348412,0x004accabd834192b,0xf4c594f2d4b2abbc,0x9bf0f8bc97c30550,
0xf5b600fc4927d620,0xd4774e5300bebbe0,0x0d6f05d3db865eaa,0x424072bb531c51f6,
0x15929ab37de620b6,0xba858dfa31bccdfd,0x0054155cfd8ce590,0x3e0d075561addf34,
0x80708102000795ea,0x9f153c261b2b0159,0x3efed77988e3b9be,0x9cda3063ba5b4e09,
0x4feb64cba31f9969,0xd41ea20788323862,0x9bdd51f0bfb077f1,0x316339479bc68be7,
0xbb407697e73eadb0,0xeff171e9dd44d9e7,0x6ec1c8e4bd9cc665,0x0cca4bf9ba1c0c7b,
0xbd7f85aa170f7d3d,0x550d580364e88698,0x4b1f732fe1cd5d80,0x6acbfe785bdcb826,
0xb08a543c1efcd2d9,0x5eeb94deaacc39f7,0xb9c001cda0505fff,0x30ac9f82e80b3205,
0xc1b6fd0554112b74,0x27e39d5bb7d7e4ff,0x2cac27ca70fae10b,0x5feab4c5ca514777,
0xd7dbb70e27d512f2,0x5a37bb6f811ff85b,0x1b89fea90df49c62,0x54468267e123654b,
0x910dfbaeda747ee7,0x41322eddf57c9d67,0xd68cdb4aefd0ff9d,0x5137c05613d337a6,
0x775e27cfbcb4219d,0x96c1b4002a5d88ef,0x1888e9f58d94d499,0x1de978a69ef254a5,
0xcdcead0c21b449d5,0x14ea91911b03aef0,0xff1d039568720c60,0xcd52019e5abc13b3,
0xbf8cd0b146c113a0,0x99f3e7789f72bfbc,0xa2989588c538ed90,0x22549ebcc773a56e,
0x6b4da54f21d99039,0x153a8eab8a800b73,0x258af6b319003aa6,0xadc8dcec0b7e0d33,
0xfe3b794d866e149b,0x7543730d52fa4390,0xedf50103c0a3ac84,0x724b77cdd1625d84,
0x15e7ac5e217b3782,0x15831579fa12fd9d,0x7fdb4176cc4d4af4,0x623410b8482a7b3d,
0x1e883a45d13d062b,0xe29b47b0c56e3bc9,0x4eebdf24d23c4afc,0x0d5f7ec972db8edc,
0xf5258d6c66f487f1,0x5078a775d118e4c4,0xd1a863cea951f049,0x6571f51fa527f5b1,
0x86a56ecaf32529dd,0xcbc3574d8b95e99b,0x6f23fb2ce7657bcc,0x72a0870902e29322,
0x6337925b9e6d64eb,0xc94683788e3283b8,0x4f7db313767ab853,0xd19a66786c3f7528,
0xe50093d0577b68fb,0xa835cb44cacf3664,0xc834536330f3c536,0xb99f0d56deb353dd,
0x09d9e36a2f3f8d39,0xed800059257b365a,0x8edc848da8c18f83,0x18cee47bc8184923,
0xa323d8114cc38d93,0x760f34ec60a33044,0xf8fe687f42a922ad,0x949c8cf76ff993ab,
0x37ea750fb084cb9e,0x881f08631bf89ea2,0x38c10f7ac93658a4,0x2608eb353ac20342,
0xfd688404c122a402,0xf58b922d7c808b09,0xc8fa8fafb1dcdeb4,0x8070b02cd9032657,
0x90322eeed25c4469,0xbee96d5dee9d3f27,0x8d35c2d4bd9c50f6,0xe6973f93a13db6b0,
0x24a44eb47c17e327,0x3ee78e51531eb827,0xf1cbbb20c9a9c90b,0x4b5cfe6a6a994355,
0xdee979b124ff1df6,0xbd62100aa4828953,0x6433d04eafa99059,0x84f934648a1ef279,
0x26a6cdf8660b9864,0xee6d2d630f91608e,0x8f49df2363bc9e79,0x581ca010f89187cd,
0xb0a02b4197e2d0de,0x5229851e4953dc51,0x87ce647ebc730cc0,0xe2a280cc452d1d01,
0x56151b762bf39247,0xf48f5cfe414e2a95,0xe7f871a71c2c8046,0x80734a474ca92d63,
0xb227b93936d9c512,0x89fcf89df6ac0ae6,0x6a5138804853a54b,0x5c11c00b75649763,
0xa072ac78f8e5390b,0x9a7926cf47e0eb9f,0x1f80bd45392dd888,0x802604d856b7b2eb,
0x1418f3dff7cd2cdf,0x4defc1286e6ba2e5,0x885c3300281d9f48,0x965816cc6fdc448d,
0x19a8adf1f52d2667,0x0ec6dff6b127867b,0xbeffa26a0c47620e,0x9442ac9ccea31f95,
0xf29fda519d0694fa,0xcb983538dea47ad3,0x40929c1505ab9a88,0x094464b4fe28d1d7,
0x0ad0a37053984057,0x9c27f70ec05d25d4,0xd594dd6748eb7b41,0xa290ee8e9ed5c80b,
0x76400ef741409da7,0xf2cff6d0cc9fdbf7,0x708458dc1fd00abc,0x65816bb40bcb8bb8,
0x5ad363b88fb13a27,0xf5be452bb04dcea3,0x6f9ac85604b86f4c,0x2073d8816c183c34,
0xe1dc9e5011811990,0xdb3250e0f2fa9f0b,0x6736094dd876839d,0x495ecac97ccf5f39,
0xd0d251b2d9b101b4,0xd2840bc821848b94,0x62b280e22974bf6c,0xf500e90c238ee331,
0x944bbc1f259ed5e8,0x6a47cbb211c47bbc,0x354d31577e266b21,0xc5d9680a70eb3346,
0x600658eb6714a9c9,0x2a651a4f3cc0c364,0xbb4a7e3badb5daf2,0x7da453dda275397f,
0xd844e6a66672a985,0x4e38ec3ccb27e6a7,0xdc6744fcda009a62,0x3db54b155aa589a3,
0xca2887e2a4389278,0x284ca843490a3d39,0x369339ad575ed4d2,0xa139152596c22c9b,
0xc8200ba5c5e5c846,0xbb6fd007a534e172,0x5e3ee317cca5f1fa,0x1d1c2aefbb557f5b,
0x493e71aea95ad111,0xaea6117450d6ea52,0x204957b2cb95b79b,0x8d2200d6faf13ae0,
0x32f44bdb95faf5b8,0xf8f2e85b65bf732a,0x0ce4f16995ac6064,0x7380ac17891de69d,
0xd903d2c707c05c1b,0xa019bb27a03698d4,0x4a79b34c42688a0c,0xd3d0953a714a6ebf,
0xd01d77bd87667847,0x9fa72c7d730ffe74,0xb694db704c4cb53c,0xd1d9ff9bae6a6160,
0x9ccf6d486971fd8b,0x8b71d3063944bcac,0x4e38c25b62beff4c,0x8b8d5eec1278f7ce,
0x86167715ecd7b446,0x66509758eb47c871,0x404d5df3623e35b7,0xfd6645b9f0160c54,
0x8030fc83184b7cfc,0x8ff133163fed813a,0x8afcc55975ac3bf2,0xd22d1eef8f24107f,
0x23c8860e07966378,0x42774a126cef8f01,0x4fe490ce4af32c6c,0x277b6e694c29208c,
0x01b6b723dfe132e3,0x7daf051d2ec28a61,0x78b0f178732d9c83,0x678eb6cd08358a14,
0x67a1f673b9a98a99,0xec046a88596b1a2a,0xb5f8b8fedc88ad51,0x1be3afecbc31992e,
0xcbd19b5a6c881d93,0xc41a39f845c2be03,0x94718d0007fbd12f,0x5e37fc2779b63467,
0xb4b7ac9143c2385e,0xf89357e9bba6aaa7,0xbb11830c610f9afc,0x7c06c9aebdb3c7be,
0xa65aa0636826af3c,0x4a89409b780d7878,0xf1e2358f22bcfec4,0xe8efebecd3bc6c6b,
0x3db9cccfdc05224a,0x2d5c9b73e9d12902,0x2d7582d0f69a3fb1,0xe4e27eb452e4597e,
0x0700a41fa51d0c84,0x948fe141b42aae0e,0xdc527f3dae30c790,0x1127daeb6bafe488,
0xd0015f594e59c6bb,0xdff0a9112db7a4bc,0x77b0ac69812e6bee,0xcd8a2ae69f51217e,
0x8ccdd6ba1796c40a,0x897c195132ba3c6f,0xef4caa240bebef20,0x7d2d1a4afe080ad5,
0x43a9d0b5834d4ecf,0x9dc72e6c3df5019f,0xa20d104f471eac7f,0x133bd235eaf47d61,
0x1f4433e4f88cd044,0x4e4ad38388a11390,0x1340934ca121800b,0xbd3c2a1d11e252d5,
0x208b63b7e0389439,0x44e4ba7be04250f8,0x1915dc563c38ce8d,0x0b739f186dae0ace,
0x4b5e0f7cf3f0cc6d,0xe9d2991e674bd1df,0x0375dd4f5f53a837,0x117f6ebe485873f2,
0x8afbcca67e97ea22,0x30edbbc350a682dc,0xd0f9cb5cca5bd3cf,0x369eb0778aff00dd,
0x481c6b51b7276ff7,0x413b9cebaca8b4a7,0x3f651c35ada140d6,0xeabf96afdc811b8b,
0x5929b4a7b97b4b82,0xe8203ec53c1836e4,0x7f02ca6b872edb90,0xa419d15126373133,
0x5a4488d317a3fbde,0x2643c6c7e441db1e,0x0d42bf1990fd2eed,0x4357bd3fc555ec15,
0xd2bf6b9881072a54,0xe147c86bfc5f5247,0xa8f1a854a7f3142d,0x6ffefbecfdad0181,
0xc468fa09281497e2,0xc5ce301ab0186e5b,0x7d2c0542013c66d4,0x91b7210f3cad9e3f,
0x11fd2900fd57b1ad,0x5f488ea57d2ce7ae,0xb80c166db7bfdbba,0x3f6f070d48d76f45,
0xc2fea9b9a8ff8780,0x4b3c7153ff1de1b8,0x6ef10078c26f77b9,0x449dfacd858668e6,
0xb635d3947b189635,0x4e123ba58070ac7f,0x0bcf276757c97c5f,0x6b6309e8483086d5,
0xf15427ad90e60fd7,0x01b5740c2940782e,0xd0c796f6b37d958c,0x8ae1b131227b97ab,
0x16fc3216c2154764,0xc49ffdc76d4cbebc,0x6df91d9b57c20d15,0xf800b7d7755a4751,
0x2035dc82115ec8df,0x9519e29c7b1f8227,0x17a2b9d22afe8950,0xb672f0e558e59786,
0x7cdd79b9bfbe5317,0x9cc69a804fd7ca9f,0x31a72a1ce6960509,0xc1df36bd66165d98,
0x81ed4e16f7a1b705,0x21f0a38b0ed4403e,0xbef9db1d866fa36f,0x6ea673e13f3d549e,
0xfe15611a4ddcf9ba,0xc17516b6a35fdaaf,0x3d2f3328f2737f60,0xc1d75a8e0e8304d7,
0x25c681ecd2a88379,0x865f82404d0f487b,0x01e067e032c6b251,0x79679b187ee2c472,
0xe2d4fa0c807c7785,0x96bc8a244925a153,0x5422caa26f3dbd8e,0xee441b473dab8cfc,
0x1db93e814e81efb0,0x39fdda766702d406,0x786c847b8e3556f3,0x40e39db48419e5b6,
0x737fd7ff96da316d,0x8a876122a718b435,0x5c29ac0b6c63620c,0x1611fadedd26275e,
0x007c503ab5d7dcf1,0x47e501b86d7c118d,0xeed929faa5f59510,0xb458daa942a89f4f,
0x1aeb7538f87788d1,0x78bcc40a245293d2,0x86fcd2f34dc3c053,0xfef30375e91f6686,
0xbc2aa72529a5edcc,0x6cd0ff757068a611,0x55c330310b2ad312,0xfd3524ce4a4b4078,
0x56bf24752e03b016,0x60a1d5c4aa0000e7,0x961a8bb638197c86,0xa445b6aeaa6fabeb,
0xb7b3d7d14ae193ac,0xf2721fea0686105b,0xca9062a2971700ae,0x793413d2c8a0a9a1,
0x5c60ccecfa926416,0x4c605b0645083b64,0x2a43ad10a741e894,0x56a077757336a295,
0x204f2c757c2e810b,0x7be8ec237a6b2575,0x5766fd71f7d010e0,0x3233c9a1e3eed89e,
0xf30f500a2f8c6c6a,0xa616bc1eb0a54f33,0xf1264b209a120e60,0x44db17cd3b32d81a,
0x1dc8536d468aca4a,0xb3e2475f1ec6054b,0x2d1eeb06dbae9282,0x7cd1efb9080818b7,
0x48122c662703ec2e,0x875aff854184e2af,0x15101d682f0c1963,0x1f0ab71a13726077,
0x79b957407f2e9ccd,0xdc0dc6105e7fc8ca,0xd2f91cc1429bf89a,0xbd8115f8d410a7ea,
0xdd6d84b17a0368ae,0xe7e0c0d03929ace6,0x57ab6f7691aa209a,0xb30dc2214f815d66,
0x53f7700298d60c93,0x6ebc64510f6dc9a4,0x888a1ccc29289e08,0x6944739577038afb };
void Add_KEY(FILE *f, char input, int inround, int index[128], int add)
{
	int i;
	int tmp[128] = { 0 }, tmp1;

	for (i = 0; i < 128; i++)
	{
		fprintf(f, "%c_%i_%i + ", input, index[i], inround);
		fprintf(f, "c_%i + ", (inround - 1) * 128 + i);
		fprintf(f, "y_%i_%i", y_count, inround);
		fprintf(f, " - 2 A%i = 0 \n", dummy);

		fprintf(f, "A%i - %c_%i_%i >= 0 \n", dummy, input, index[i], inround);
		fprintf(f, "A%i - c_%i >= 0 \n", dummy, (inround - 1) * 128 + i);
		fprintf(f, "A%i - y_%i_%i >= 0 \n", dummy, y_count, inround);

		if (i < 64)
		{
			tmp1 = (randomvaule[(R_PARAM - 1) * 2 * add + 2 * inround] >> i) & 0x1;
		}
		else
		{
			tmp1 = (randomvaule[(R_PARAM - 1) * 2 * add + 2 * inround + 1] >> i) & 0x1;
		}
		
		fprintf(f, "c_%i = %i\n", (inround - 1) * 128 + i, tmp1);//constant_c[128 * (inround - 1) + i] ^ constant_c1[128 * (inround - 1) + i]);//rand() % 2);

		index[i] = y_count;
		y_count++; dummy++;
	}
}
void SC(FILE *f, const int shuffle[16], int index[128])
{
	int i, j;
	int tmp[128];

	for (i = 0; i < 16; i++)
	{
		for (j = 0; j < 8; j++)
		{
			tmp[8 * i + j] = index[8 * shuffle[i] + j];
		}
	}

	for (i = 0; i < 128; i++)
	{
		index[i] = tmp[i];
	}
}

void MixColumns(FILE *f, char input, int inround, int index[128])//M_4_1 is used in this program.
{
	int column, i, j, tmp1, tmp2;
	int tmp_index[128] = { 0 };
	for (column = 0; column < 4; column++) /* column */
	{
		for (j = 0; j < 8; j++)//for each bit in 0 cell
		{
			tmp1 = index[8 * (4 * 1 + column) + (j + 1) % 8];
			fprintf(f, "%c_%i_%i + ", input, tmp1, inround);
			tmp2 = index[8 * (4 * 2 + column) + (j + 4) % 8];
			fprintf(f, "%c_%i_%i + ", input, tmp2, inround);
			fprintf(f, "y_%i_%i ", y_count, inround);
			fprintf(f, " - 2 A%i = 0 \n", dummy);

			//fprintf(f, "2 ");
			//fprintf(f, "- %c_%i_%i ", input, tmp1, inround);
			//fprintf(f, "- %c_%i_%i ", input, tmp2, inround);
			//fprintf(f, "- y_%i_%i >= 0 \n", y_count, inround);

			fprintf(f, "A%i - %c_%i_%i >= 0 \n", dummy, input, tmp1, inround);
			fprintf(f, "A%i - %c_%i_%i >= 0 \n", dummy, input, tmp2, inround);
			fprintf(f, "A%i - y_%i_%i >= 0 \n", dummy, y_count, inround);
			y_count++; dummy++;

			fprintf(f, "y_%i_%i + ", y_count - 1, inround);
			tmp1 = index[8 * (4 * 3 + column) + (j + 5) % 8];
			fprintf(f, "%c_%i_%i + ", input, tmp1, inround);
			fprintf(f, "y_%i_%i ", y_count, inround);
			fprintf(f, " - 2 A%i = 0 \n", dummy);

			//fprintf(f, "2 -");
			//fprintf(f, " y_%i_%i -", y_count - 1, inround);
			//fprintf(f, " %c_%i_%i -", input, tmp1, inround);
			//fprintf(f, " y_%i_%i >= 0 \n", y_count, inround);

			fprintf(f, "A%i - y_%i_%i >= 0 \n", dummy, y_count - 1, inround);
			fprintf(f, "A%i - %c_%i_%i >= 0 \n", dummy, input, tmp1, inround);
			fprintf(f, "A%i - y_%i_%i >= 0 \n", dummy, y_count, inround);

			tmp_index[8 * (4 * 0 + column) + j] = y_count;
			y_count++; dummy++;
		}

		for (j = 0; j < 8; j++)//for each bit in 1 cell
		{
			tmp1 = index[8 * (4 * 0 + column) + (j + 5) % 8];
			fprintf(f, "%c_%i_%i + ", input, tmp1, inround);
			tmp2 = index[8 * (4 * 2 + column) + (j + 1) % 8];
			fprintf(f, "%c_%i_%i + ", input, tmp2, inround);
			fprintf(f, "y_%i_%i ", y_count, inround);
			fprintf(f, " - 2 A%i = 0 \n", dummy);

			//fprintf(f, "2 ");
			//fprintf(f, "- %c_%i_%i ", input, tmp1, inround);
			//fprintf(f, "- %c_%i_%i ", input, tmp2, inround);
			//fprintf(f, "- y_%i_%i >= 0 \n", y_count, inround);

			fprintf(f, "A%i - %c_%i_%i >= 0 \n", dummy, input, tmp1, inround);
			fprintf(f, "A%i - %c_%i_%i >= 0 \n", dummy, input, tmp2, inround);
			fprintf(f, "A%i - y_%i_%i >= 0 \n", dummy, y_count, inround);
			y_count++; dummy++;

			fprintf(f, "y_%i_%i + ", y_count - 1, inround);
			tmp1 = index[8 * (4 * 3 + column) + (j + 4) % 8];
			fprintf(f, "%c_%i_%i + ", input, tmp1, inround);
			fprintf(f, "y_%i_%i ", y_count, inround);
			fprintf(f, " - 2 A%i = 0 \n", dummy);

			//fprintf(f, "2 -");
			//fprintf(f, " y_%i_%i -", y_count - 1, inround);
			//fprintf(f, " %c_%i_%i -", input, tmp1, inround);
			//fprintf(f, " y_%i_%i >= 0 \n", y_count, inround);

			fprintf(f, "A%i - y_%i_%i >= 0 \n", dummy, y_count - 1, inround);
			fprintf(f, "A%i - %c_%i_%i >= 0 \n", dummy, input, tmp1, inround);
			fprintf(f, "A%i - y_%i_%i >= 0 \n", dummy, y_count, inround);

			tmp_index[8 * (4 * 1 + column) + j] = y_count;
			y_count++; dummy++;
		}

		for (j = 0; j < 8; j++)//for each bit in 2 cell
		{
			tmp1 = index[8 * (4 * 0 + column) + (j + 4) % 8];
			fprintf(f, "%c_%i_%i + ", input, tmp1, inround);
			tmp2 = index[8 * (4 * 1 + column) + (j + 5) % 8];
			fprintf(f, "%c_%i_%i + ", input, tmp2, inround);
			fprintf(f, "y_%i_%i ", y_count, inround);
			fprintf(f, " - 2 A%i = 0 \n", dummy);

			//fprintf(f, "2 ");
			//fprintf(f, "- %c_%i_%i ", input, tmp1, inround);
			//fprintf(f, "- %c_%i_%i ", input, tmp2, inround);
			//fprintf(f, "- y_%i_%i >= 0 \n", y_count, inround);

			fprintf(f, "A%i - %c_%i_%i >= 0 \n", dummy, input, tmp1, inround);
			fprintf(f, "A%i - %c_%i_%i >= 0 \n", dummy, input, tmp2, inround);
			fprintf(f, "A%i - y_%i_%i >= 0 \n", dummy, y_count, inround);
			y_count++; dummy++;

			fprintf(f, "y_%i_%i + ", y_count - 1, inround);
			tmp1 = index[8 * (4 * 3 + column) + (j + 1) % 8];
			fprintf(f, "%c_%i_%i + ", input, tmp1, inround);
			fprintf(f, "y_%i_%i ", y_count, inround);
			fprintf(f, " - 2 A%i = 0 \n", dummy);

			//fprintf(f, "2 -");
			//fprintf(f, " y_%i_%i -", y_count - 1, inround);
			//fprintf(f, " %c_%i_%i -", input, tmp1, inround);
			//fprintf(f, " y_%i_%i >= 0 \n", y_count, inround);


			fprintf(f, "A%i - y_%i_%i >= 0 \n", dummy, y_count - 1, inround);
			fprintf(f, "A%i - %c_%i_%i >= 0 \n", dummy, input, tmp1, inround);
			fprintf(f, "A%i - y_%i_%i >= 0 \n", dummy, y_count, inround);

			tmp_index[8 * (4 * 2 + column) + j] = y_count;
			y_count++; dummy++;
		}

		for (j = 0; j < 8; j++)//for each bit in 3 cell
		{
			tmp1 = index[8 * (4 * 0 + column) + (j + 1) % 8];
			fprintf(f, "%c_%i_%i + ", input, tmp1, inround);
			tmp2 = index[8 * (4 * 1 + column) + (j + 4) % 8];
			fprintf(f, "%c_%i_%i + ", input, tmp2, inround);
			fprintf(f, "y_%i_%i ", y_count, inround);
			fprintf(f, " - 2 A%i = 0 \n", dummy);

			//fprintf(f, "2 ");
			//fprintf(f, "- %c_%i_%i ", input, tmp1, inround);
			//fprintf(f, "- %c_%i_%i ", input, tmp2, inround);
			//fprintf(f, "- y_%i_%i >= 0 \n", y_count, inround);

			fprintf(f, "A%i - %c_%i_%i >= 0 \n", dummy, input, tmp1, inround);
			fprintf(f, "A%i - %c_%i_%i >= 0 \n", dummy, input, tmp2, inround);
			fprintf(f, "A%i - y_%i_%i >= 0 \n", dummy, y_count, inround);
			y_count++; dummy++;

			fprintf(f, "y_%i_%i + ", y_count - 1, inround);
			tmp1 = index[8 * (4 * 2 + column) + (j + 5) % 8];
			fprintf(f, "%c_%i_%i + ", input, tmp1, inround);
			fprintf(f, "y_%i_%i ", y_count, inround);
			fprintf(f, " - 2 A%i = 0 \n", dummy);

			//fprintf(f, "2 -");
			//fprintf(f, " y_%i_%i -", y_count - 1, inround);
			//fprintf(f, " %c_%i_%i -", input, tmp1, inround);
			//fprintf(f, " y_%i_%i >= 0 \n", y_count, inround);

			fprintf(f, "A%i - y_%i_%i >= 0 \n", dummy, y_count - 1, inround);
			fprintf(f, "A%i - %c_%i_%i >= 0 \n", dummy, input, tmp1, inround);
			fprintf(f, "A%i - y_%i_%i >= 0 \n", dummy, y_count, inround);

			tmp_index[8 * (4 * 3 + column) + j] = y_count;
			y_count++; dummy++;
		}

	}

	for (i = 0; i < 128; i++)
	{
		index[i] = tmp_index[i];
	}
}

void Sbox_Layer_Bitwise(FILE *f, int inround, char output, int outround, int index[128], const int Convex[35][9])
{
	int i, j, k;

	for (i = 0; i < 16; i++)
	{
		for (j = 0; j < 35; j++)
		{
			//part1
			for (k = 0; k < 4; k++)
			{
				if (Convex[j][k] > 0)
				{
					fprintf(f, "+ %i y_%i_%i ", Convex[j][k], index[8 * i + k], inround);
				}
				else if (Convex[j][k] < 0)
				{
					fprintf(f, "%i y_%i_%i ", Convex[j][k], index[8 * i + k], inround);
				}
			}

			for (k = 0; k < 4; k++)
			{
				if (Convex[j][k + 4] > 0)
				{
					fprintf(f, "+ %i %c_%i_%i ", Convex[j][k + 4], output, 8 * i + sig_ind[k], outround);
				}
				else if (Convex[j][k + 4] < 0)
				{
					fprintf(f, "%i %c_%i_%i ", Convex[j][k + 4], output, 8 * i + sig_ind[k], outround);
				}
			}
			fprintf(f, ">= %i \n", -Convex[j][8]);

			//part2
			for (k = 4; k < 8; k++)
			{
				if (Convex[j][k-4] > 0)
				{
					fprintf(f, "+ %i y_%i_%i ", Convex[j][k-4], index[8 * i + k], inround);
				}
				else if (Convex[j][k-4] < 0)
				{
					fprintf(f, "%i y_%i_%i ", Convex[j][k-4], index[8 * i + k], inround);
				}
			}

			for (k = 4; k < 8; k++)
			{
				if (Convex[j][k] > 0)
				{
					fprintf(f, "+ %i %c_%i_%i ", Convex[j][k], output, 8 * i + sig_ind[k], outround);
				}
				else if (Convex[j][k] < 0)
				{
					fprintf(f, "%i %c_%i_%i ", Convex[j][k], output, 8 * i + sig_ind[k], outround);
				}
			}
			fprintf(f, ">= %i \n", -Convex[j][8]);
		}

		for (j = 0; j < 3; j++)
		{
			fprintf(f, "y_%i_%i + ", index[8 * i + j], inround);
		}
		fprintf(f, "y_%i_%i -", index[8 * i + 3], inround);
		fprintf(f, " B_%i_%i >= 0 \n", 2*i, inround);

		for (j = 4; j < 7; j++)
		{
			fprintf(f, "y_%i_%i + ", index[8 * i + j], inround);
		}
		fprintf(f, "y_%i_%i -", index[8 * i + 7], inround);
		fprintf(f, " B_%i_%i >= 0 \n", 2 * i+1, inround);

		for (j = 0; j < 4; j++)
		{
			fprintf(f, "B_%i_%i - y_%i_%i >= 0 \n", 2*i, inround, index[8 * i + j], inround);
			fprintf(f, "B_%i_%i - %c_%i_%i >= 0 \n", 2*i, inround, output, 8 * i + sig_ind[j], outround);
		}
		for (j = 4; j < 8; j++)
		{
			fprintf(f, "B_%i_%i - y_%i_%i >= 0 \n", 2 * i+1, inround, index[8 * i + j], inround);
			fprintf(f, "B_%i_%i - %c_%i_%i >= 0 \n", 2 * i+1, inround, output, 8 * i + sig_ind[j], outround);
		}
	}

	for (i = 0; i < 128; i++)
	{
		index[i] = i;
	}
}

int main(int argc, char** argv)
//int main()
{
	int i, j, r;
	int index[128] = { 0 };
	for (i = 0; i < 128; i++)
	{
		index[i] = i;
	}
	int addr = atoi(argv[1]);
	// ///////////////////////////////////////////////////////////////////
	//
	// initially the tweak is in its input state, no permutation
	FILE *f;
	//f=fopen("qarma_milp_constant.lp", "w+");
	fopen_s(&f, "qarma_milp_constant_1.lp", "w+");
	fprintf(f, "Minimize\n"); /* print objective function */
							  //fprintf(f, "T\n");

	for (j = 0; j < R_PARAM; j++)
	{
		for (i = 0; i < 32; i++)
		{
			fprintf(f, "B_%i_%i", i, j);
			if ((j != R_PARAM - 1) || (i != 31)) fprintf(f, " + ");
			if (i == 31| i==15) fprintf(f, "\n");
		}
		/*if (j == R_PARAM - 1)
		{
		fprintf(f, "- T >= 0\n");
		}*/
	}
	fprintf(f, "Subject To\n"); /* round function constraints */
	srand((unsigned)time(NULL));
	// Exclude trivial solution (no active input)
	/*for (i = 0; i < 32; i++)
	{
		fprintf(f, "B_%i_%i", i, 0);
		if (i != 31) fprintf(f, " + ");
		if (i == 15) fprintf(f, "\n");
	}
	fprintf(f, " >= 1\n");*/

	/*for (j = 0; j < R_PARAM; j++)
	{
		for (i = 0; i < 16; i++)
		{
			fprintf(f, "B_%i_%i", i, j);
			if ((j != R_PARAM - 1) || (i != 15)) fprintf(f, " + ");
			if (j != R_PARAM - 1 & i == 15) fprintf(f, "\n");
		}
		if (j == R_PARAM - 1)
		{
			fprintf(f, " >= 29\n");
		}
	}*/
	// ///////////////////////////////////////////////////////////////////
	//
	// Now model the cipher 



	// FORWARD ROUNDS

	y_count = 0;
	SC(f, SHUFFLE_P, index);
	MixColumns(f, 'x', 0, index);
	Sbox_Layer_Bitwise(f, 0, 'x', 1, index, Convex);

	for (r = 1; r<R_PARAM; r++)
	{
		y_count = 0;
		Add_KEY(f, 'x', r, index, addr);
		SC(f, SHUFFLE_P, index);
		MixColumns(f, 'y', r, index);
		Sbox_Layer_Bitwise(f, r, 'x', r + 1, index, Convex);
	}


	// ///////////////////////////////////////////////////////////////////

	

	fprintf(f, "\n");



	// ///////////////////////////////////////////////////////////////////
	//
	// Declare variables as binary

	fprintf(f, "Binary\n"); /* binary constraints */

	for (r = 0; r <= R_PARAM; r++)
	{
		for (i = 0; i < 128; i++)
		{
			fprintf(f, "x_%i_%i\n", i, r);
		}
	}

	for (i = 0; i < 256; i++)
	{
		fprintf(f, "y_%i_0\n", i);
	}

	for (r = 1; r < R_PARAM; r++)
	{
		for (i = 0; i < y_count; i++)
		{
			fprintf(f, "y_%i_%i\n", i, r);
		}
	}

	for (i = 0; i < R_PARAM - 1; i++)
	{
		for (j = 0; j < 128; j++)
		{
			fprintf(f, "c_%i\n", 128 * i + j);
		}
	}


	for (r = 0; r < R_PARAM; r++)
	{
		for (i = 0; i < 32; i++)
		{
			fprintf(f, "B_%i_%i\n", i, r);
		}
	}

	for (i = 0; i < dummy; i++)
	{
		fprintf(f, "A%i\n", i);
	}
	// ///////////////////////////////////////////////////////////////////

	fprintf(f, "End\n");
	fclose(f);


	return 0;

	// ///////////////////////////////////////////////////////////////////
}