xref: /dports/math/py-or-tools/or-tools-9.2/examples/flatzinc/coins_grid.fzn

var 0..153760: INT____00001 :: is_defined_var :: var_is_introduced;
array [1..961] of var 0..1: x :: output_array([1..31, 1..31]);
var 0..153760: z :: output_var = INT____00001;
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[1], x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9], x[10], x[11], x[12], x[13], x[14], x[15], x[16], x[17], x[18], x[19], x[20], x[21], x[22], x[23], x[24], x[25], x[26], x[27], x[28], x[29], x[30], x[31]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[1], x[32], x[63], x[94], x[125], x[156], x[187], x[218], x[249], x[280], x[311], x[342], x[373], x[404], x[435], x[466], x[497], x[528], x[559], x[590], x[621], x[652], x[683], x[714], x[745], x[776], x[807], x[838], x[869], x[900], x[931]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[2], x[33], x[64], x[95], x[126], x[157], x[188], x[219], x[250], x[281], x[312], x[343], x[374], x[405], x[436], x[467], x[498], x[529], x[560], x[591], x[622], x[653], x[684], x[715], x[746], x[777], x[808], x[839], x[870], x[901], x[932]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[3], x[34], x[65], x[96], x[127], x[158], x[189], x[220], x[251], x[282], x[313], x[344], x[375], x[406], x[437], x[468], x[499], x[530], x[561], x[592], x[623], x[654], x[685], x[716], x[747], x[778], x[809], x[840], x[871], x[902], x[933]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[4], x[35], x[66], x[97], x[128], x[159], x[190], x[221], x[252], x[283], x[314], x[345], x[376], x[407], x[438], x[469], x[500], x[531], x[562], x[593], x[624], x[655], x[686], x[717], x[748], x[779], x[810], x[841], x[872], x[903], x[934]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[5], x[36], x[67], x[98], x[129], x[160], x[191], x[222], x[253], x[284], x[315], x[346], x[377], x[408], x[439], x[470], x[501], x[532], x[563], x[594], x[625], x[656], x[687], x[718], x[749], x[780], x[811], x[842], x[873], x[904], x[935]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[6], x[37], x[68], x[99], x[130], x[161], x[192], x[223], x[254], x[285], x[316], x[347], x[378], x[409], x[440], x[471], x[502], x[533], x[564], x[595], x[626], x[657], x[688], x[719], x[750], x[781], x[812], x[843], x[874], x[905], x[936]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[7], x[38], x[69], x[100], x[131], x[162], x[193], x[224], x[255], x[286], x[317], x[348], x[379], x[410], x[441], x[472], x[503], x[534], x[565], x[596], x[627], x[658], x[689], x[720], x[751], x[782], x[813], x[844], x[875], x[906], x[937]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[8], x[39], x[70], x[101], x[132], x[163], x[194], x[225], x[256], x[287], x[318], x[349], x[380], x[411], x[442], x[473], x[504], x[535], x[566], x[597], x[628], x[659], x[690], x[721], x[752], x[783], x[814], x[845], x[876], x[907], x[938]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[9], x[40], x[71], x[102], x[133], x[164], x[195], x[226], x[257], x[288], x[319], x[350], x[381], x[412], x[443], x[474], x[505], x[536], x[567], x[598], x[629], x[660], x[691], x[722], x[753], x[784], x[815], x[846], x[877], x[908], x[939]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[10], x[41], x[72], x[103], x[134], x[165], x[196], x[227], x[258], x[289], x[320], x[351], x[382], x[413], x[444], x[475], x[506], x[537], x[568], x[599], x[630], x[661], x[692], x[723], x[754], x[785], x[816], x[847], x[878], x[909], x[940]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[11], x[42], x[73], x[104], x[135], x[166], x[197], x[228], x[259], x[290], x[321], x[352], x[383], x[414], x[445], x[476], x[507], x[538], x[569], x[600], x[631], x[662], x[693], x[724], x[755], x[786], x[817], x[848], x[879], x[910], x[941]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[12], x[43], x[74], x[105], x[136], x[167], x[198], x[229], x[260], x[291], x[322], x[353], x[384], x[415], x[446], x[477], x[508], x[539], x[570], x[601], x[632], x[663], x[694], x[725], x[756], x[787], x[818], x[849], x[880], x[911], x[942]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[13], x[44], x[75], x[106], x[137], x[168], x[199], x[230], x[261], x[292], x[323], x[354], x[385], x[416], x[447], x[478], x[509], x[540], x[571], x[602], x[633], x[664], x[695], x[726], x[757], x[788], x[819], x[850], x[881], x[912], x[943]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[14], x[45], x[76], x[107], x[138], x[169], x[200], x[231], x[262], x[293], x[324], x[355], x[386], x[417], x[448], x[479], x[510], x[541], x[572], x[603], x[634], x[665], x[696], x[727], x[758], x[789], x[820], x[851], x[882], x[913], x[944]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[15], x[46], x[77], x[108], x[139], x[170], x[201], x[232], x[263], x[294], x[325], x[356], x[387], x[418], x[449], x[480], x[511], x[542], x[573], x[604], x[635], x[666], x[697], x[728], x[759], x[790], x[821], x[852], x[883], x[914], x[945]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[16], x[47], x[78], x[109], x[140], x[171], x[202], x[233], x[264], x[295], x[326], x[357], x[388], x[419], x[450], x[481], x[512], x[543], x[574], x[605], x[636], x[667], x[698], x[729], x[760], x[791], x[822], x[853], x[884], x[915], x[946]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[17], x[48], x[79], x[110], x[141], x[172], x[203], x[234], x[265], x[296], x[327], x[358], x[389], x[420], x[451], x[482], x[513], x[544], x[575], x[606], x[637], x[668], x[699], x[730], x[761], x[792], x[823], x[854], x[885], x[916], x[947]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[18], x[49], x[80], x[111], x[142], x[173], x[204], x[235], x[266], x[297], x[328], x[359], x[390], x[421], x[452], x[483], x[514], x[545], x[576], x[607], x[638], x[669], x[700], x[731], x[762], x[793], x[824], x[855], x[886], x[917], x[948]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[19], x[50], x[81], x[112], x[143], x[174], x[205], x[236], x[267], x[298], x[329], x[360], x[391], x[422], x[453], x[484], x[515], x[546], x[577], x[608], x[639], x[670], x[701], x[732], x[763], x[794], x[825], x[856], x[887], x[918], x[949]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[20], x[51], x[82], x[113], x[144], x[175], x[206], x[237], x[268], x[299], x[330], x[361], x[392], x[423], x[454], x[485], x[516], x[547], x[578], x[609], x[640], x[671], x[702], x[733], x[764], x[795], x[826], x[857], x[888], x[919], x[950]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[21], x[52], x[83], x[114], x[145], x[176], x[207], x[238], x[269], x[300], x[331], x[362], x[393], x[424], x[455], x[486], x[517], x[548], x[579], x[610], x[641], x[672], x[703], x[734], x[765], x[796], x[827], x[858], x[889], x[920], x[951]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[22], x[53], x[84], x[115], x[146], x[177], x[208], x[239], x[270], x[301], x[332], x[363], x[394], x[425], x[456], x[487], x[518], x[549], x[580], x[611], x[642], x[673], x[704], x[735], x[766], x[797], x[828], x[859], x[890], x[921], x[952]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[23], x[54], x[85], x[116], x[147], x[178], x[209], x[240], x[271], x[302], x[333], x[364], x[395], x[426], x[457], x[488], x[519], x[550], x[581], x[612], x[643], x[674], x[705], x[736], x[767], x[798], x[829], x[860], x[891], x[922], x[953]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[24], x[55], x[86], x[117], x[148], x[179], x[210], x[241], x[272], x[303], x[334], x[365], x[396], x[427], x[458], x[489], x[520], x[551], x[582], x[613], x[644], x[675], x[706], x[737], x[768], x[799], x[830], x[861], x[892], x[923], x[954]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[25], x[56], x[87], x[118], x[149], x[180], x[211], x[242], x[273], x[304], x[335], x[366], x[397], x[428], x[459], x[490], x[521], x[552], x[583], x[614], x[645], x[676], x[707], x[738], x[769], x[800], x[831], x[862], x[893], x[924], x[955]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[26], x[57], x[88], x[119], x[150], x[181], x[212], x[243], x[274], x[305], x[336], x[367], x[398], x[429], x[460], x[491], x[522], x[553], x[584], x[615], x[646], x[677], x[708], x[739], x[770], x[801], x[832], x[863], x[894], x[925], x[956]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[27], x[58], x[89], x[120], x[151], x[182], x[213], x[244], x[275], x[306], x[337], x[368], x[399], x[430], x[461], x[492], x[523], x[554], x[585], x[616], x[647], x[678], x[709], x[740], x[771], x[802], x[833], x[864], x[895], x[926], x[957]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[28], x[59], x[90], x[121], x[152], x[183], x[214], x[245], x[276], x[307], x[338], x[369], x[400], x[431], x[462], x[493], x[524], x[555], x[586], x[617], x[648], x[679], x[710], x[741], x[772], x[803], x[834], x[865], x[896], x[927], x[958]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[29], x[60], x[91], x[122], x[153], x[184], x[215], x[246], x[277], x[308], x[339], x[370], x[401], x[432], x[463], x[494], x[525], x[556], x[587], x[618], x[649], x[680], x[711], x[742], x[773], x[804], x[835], x[866], x[897], x[928], x[959]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[30], x[61], x[92], x[123], x[154], x[185], x[216], x[247], x[278], x[309], x[340], x[371], x[402], x[433], x[464], x[495], x[526], x[557], x[588], x[619], x[650], x[681], x[712], x[743], x[774], x[805], x[836], x[867], x[898], x[929], x[960]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[31], x[62], x[93], x[124], x[155], x[186], x[217], x[248], x[279], x[310], x[341], x[372], x[403], x[434], x[465], x[496], x[527], x[558], x[589], x[620], x[651], x[682], x[713], x[744], x[775], x[806], x[837], x[868], x[899], x[930], x[961]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[32], x[33], x[34], x[35], x[36], x[37], x[38], x[39], x[40], x[41], x[42], x[43], x[44], x[45], x[46], x[47], x[48], x[49], x[50], x[51], x[52], x[53], x[54], x[55], x[56], x[57], x[58], x[59], x[60], x[61], x[62]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[63], x[64], x[65], x[66], x[67], x[68], x[69], x[70], x[71], x[72], x[73], x[74], x[75], x[76], x[77], x[78], x[79], x[80], x[81], x[82], x[83], x[84], x[85], x[86], x[87], x[88], x[89], x[90], x[91], x[92], x[93]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[94], x[95], x[96], x[97], x[98], x[99], x[100], x[101], x[102], x[103], x[104], x[105], x[106], x[107], x[108], x[109], x[110], x[111], x[112], x[113], x[114], x[115], x[116], x[117], x[118], x[119], x[120], x[121], x[122], x[123], x[124]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[125], x[126], x[127], x[128], x[129], x[130], x[131], x[132], x[133], x[134], x[135], x[136], x[137], x[138], x[139], x[140], x[141], x[142], x[143], x[144], x[145], x[146], x[147], x[148], x[149], x[150], x[151], x[152], x[153], x[154], x[155]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[156], x[157], x[158], x[159], x[160], x[161], x[162], x[163], x[164], x[165], x[166], x[167], x[168], x[169], x[170], x[171], x[172], x[173], x[174], x[175], x[176], x[177], x[178], x[179], x[180], x[181], x[182], x[183], x[184], x[185], x[186]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[187], x[188], x[189], x[190], x[191], x[192], x[193], x[194], x[195], x[196], x[197], x[198], x[199], x[200], x[201], x[202], x[203], x[204], x[205], x[206], x[207], x[208], x[209], x[210], x[211], x[212], x[213], x[214], x[215], x[216], x[217]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[218], x[219], x[220], x[221], x[222], x[223], x[224], x[225], x[226], x[227], x[228], x[229], x[230], x[231], x[232], x[233], x[234], x[235], x[236], x[237], x[238], x[239], x[240], x[241], x[242], x[243], x[244], x[245], x[246], x[247], x[248]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[249], x[250], x[251], x[252], x[253], x[254], x[255], x[256], x[257], x[258], x[259], x[260], x[261], x[262], x[263], x[264], x[265], x[266], x[267], x[268], x[269], x[270], x[271], x[272], x[273], x[274], x[275], x[276], x[277], x[278], x[279]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[280], x[281], x[282], x[283], x[284], x[285], x[286], x[287], x[288], x[289], x[290], x[291], x[292], x[293], x[294], x[295], x[296], x[297], x[298], x[299], x[300], x[301], x[302], x[303], x[304], x[305], x[306], x[307], x[308], x[309], x[310]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[311], x[312], x[313], x[314], x[315], x[316], x[317], x[318], x[319], x[320], x[321], x[322], x[323], x[324], x[325], x[326], x[327], x[328], x[329], x[330], x[331], x[332], x[333], x[334], x[335], x[336], x[337], x[338], x[339], x[340], x[341]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[342], x[343], x[344], x[345], x[346], x[347], x[348], x[349], x[350], x[351], x[352], x[353], x[354], x[355], x[356], x[357], x[358], x[359], x[360], x[361], x[362], x[363], x[364], x[365], x[366], x[367], x[368], x[369], x[370], x[371], x[372]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[373], x[374], x[375], x[376], x[377], x[378], x[379], x[380], x[381], x[382], x[383], x[384], x[385], x[386], x[387], x[388], x[389], x[390], x[391], x[392], x[393], x[394], x[395], x[396], x[397], x[398], x[399], x[400], x[401], x[402], x[403]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[404], x[405], x[406], x[407], x[408], x[409], x[410], x[411], x[412], x[413], x[414], x[415], x[416], x[417], x[418], x[419], x[420], x[421], x[422], x[423], x[424], x[425], x[426], x[427], x[428], x[429], x[430], x[431], x[432], x[433], x[434]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[435], x[436], x[437], x[438], x[439], x[440], x[441], x[442], x[443], x[444], x[445], x[446], x[447], x[448], x[449], x[450], x[451], x[452], x[453], x[454], x[455], x[456], x[457], x[458], x[459], x[460], x[461], x[462], x[463], x[464], x[465]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[466], x[467], x[468], x[469], x[470], x[471], x[472], x[473], x[474], x[475], x[476], x[477], x[478], x[479], x[480], x[481], x[482], x[483], x[484], x[485], x[486], x[487], x[488], x[489], x[490], x[491], x[492], x[493], x[494], x[495], x[496]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[497], x[498], x[499], x[500], x[501], x[502], x[503], x[504], x[505], x[506], x[507], x[508], x[509], x[510], x[511], x[512], x[513], x[514], x[515], x[516], x[517], x[518], x[519], x[520], x[521], x[522], x[523], x[524], x[525], x[526], x[527]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[528], x[529], x[530], x[531], x[532], x[533], x[534], x[535], x[536], x[537], x[538], x[539], x[540], x[541], x[542], x[543], x[544], x[545], x[546], x[547], x[548], x[549], x[550], x[551], x[552], x[553], x[554], x[555], x[556], x[557], x[558]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[559], x[560], x[561], x[562], x[563], x[564], x[565], x[566], x[567], x[568], x[569], x[570], x[571], x[572], x[573], x[574], x[575], x[576], x[577], x[578], x[579], x[580], x[581], x[582], x[583], x[584], x[585], x[586], x[587], x[588], x[589]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[590], x[591], x[592], x[593], x[594], x[595], x[596], x[597], x[598], x[599], x[600], x[601], x[602], x[603], x[604], x[605], x[606], x[607], x[608], x[609], x[610], x[611], x[612], x[613], x[614], x[615], x[616], x[617], x[618], x[619], x[620]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[621], x[622], x[623], x[624], x[625], x[626], x[627], x[628], x[629], x[630], x[631], x[632], x[633], x[634], x[635], x[636], x[637], x[638], x[639], x[640], x[641], x[642], x[643], x[644], x[645], x[646], x[647], x[648], x[649], x[650], x[651]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[652], x[653], x[654], x[655], x[656], x[657], x[658], x[659], x[660], x[661], x[662], x[663], x[664], x[665], x[666], x[667], x[668], x[669], x[670], x[671], x[672], x[673], x[674], x[675], x[676], x[677], x[678], x[679], x[680], x[681], x[682]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[683], x[684], x[685], x[686], x[687], x[688], x[689], x[690], x[691], x[692], x[693], x[694], x[695], x[696], x[697], x[698], x[699], x[700], x[701], x[702], x[703], x[704], x[705], x[706], x[707], x[708], x[709], x[710], x[711], x[712], x[713]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[714], x[715], x[716], x[717], x[718], x[719], x[720], x[721], x[722], x[723], x[724], x[725], x[726], x[727], x[728], x[729], x[730], x[731], x[732], x[733], x[734], x[735], x[736], x[737], x[738], x[739], x[740], x[741], x[742], x[743], x[744]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[745], x[746], x[747], x[748], x[749], x[750], x[751], x[752], x[753], x[754], x[755], x[756], x[757], x[758], x[759], x[760], x[761], x[762], x[763], x[764], x[765], x[766], x[767], x[768], x[769], x[770], x[771], x[772], x[773], x[774], x[775]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[776], x[777], x[778], x[779], x[780], x[781], x[782], x[783], x[784], x[785], x[786], x[787], x[788], x[789], x[790], x[791], x[792], x[793], x[794], x[795], x[796], x[797], x[798], x[799], x[800], x[801], x[802], x[803], x[804], x[805], x[806]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[807], x[808], x[809], x[810], x[811], x[812], x[813], x[814], x[815], x[816], x[817], x[818], x[819], x[820], x[821], x[822], x[823], x[824], x[825], x[826], x[827], x[828], x[829], x[830], x[831], x[832], x[833], x[834], x[835], x[836], x[837]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[838], x[839], x[840], x[841], x[842], x[843], x[844], x[845], x[846], x[847], x[848], x[849], x[850], x[851], x[852], x[853], x[854], x[855], x[856], x[857], x[858], x[859], x[860], x[861], x[862], x[863], x[864], x[865], x[866], x[867], x[868]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[869], x[870], x[871], x[872], x[873], x[874], x[875], x[876], x[877], x[878], x[879], x[880], x[881], x[882], x[883], x[884], x[885], x[886], x[887], x[888], x[889], x[890], x[891], x[892], x[893], x[894], x[895], x[896], x[897], x[898], x[899]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[900], x[901], x[902], x[903], x[904], x[905], x[906], x[907], x[908], x[909], x[910], x[911], x[912], x[913], x[914], x[915], x[916], x[917], x[918], x[919], x[920], x[921], x[922], x[923], x[924], x[925], x[926], x[927], x[928], x[929], x[930]], 14);
constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[931], x[932], x[933], x[934], x[935], x[936], x[937], x[938], x[939], x[940], x[941], x[942], x[943], x[944], x[945], x[946], x[947], x[948], x[949], x[950], x[951], x[952], x[953], x[954], x[955], x[956], x[957], x[958], x[959], x[960], x[961]], 14);
constraint int_lin_eq([-1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256, 289, 324, 361, 400, 441, 484, 529, 576, 625, 676, 729, 784, 841, 900, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256, 289, 324, 361, 400, 441, 484, 529, 576, 625, 676, 729, 784, 841, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256, 289, 324, 361, 400, 441, 484, 529, 576, 625, 676, 729, 784, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256, 289, 324, 361, 400, 441, 484, 529, 576, 625, 676, 729, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256, 289, 324, 361, 400, 441, 484, 529, 576, 625, 676, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256, 289, 324, 361, 400, 441, 484, 529, 576, 625, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256, 289, 324, 361, 400, 441, 484, 529, 576, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256, 289, 324, 361, 400, 441, 484, 529, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256, 289, 324, 361, 400, 441, 484, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256, 289, 324, 361, 400, 441, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256, 289, 324, 361, 400, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256, 289, 324, 361, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256, 289, 324, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256, 289, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256, 225, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256, 225, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 289, 256, 225, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 324, 289, 256, 225, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 361, 324, 289, 256, 225, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 400, 361, 324, 289, 256, 225, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 441, 400, 361, 324, 289, 256, 225, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 81, 484, 441, 400, 361, 324, 289, 256, 225, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 64, 529, 484, 441, 400, 361, 324, 289, 256, 225, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 49, 576, 529, 484, 441, 400, 361, 324, 289, 256, 225, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 36, 625, 576, 529, 484, 441, 400, 361, 324, 289, 256, 225, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 25, 676, 625, 576, 529, 484, 441, 400, 361, 324, 289, 256, 225, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 16, 729, 676, 625, 576, 529, 484, 441, 400, 361, 324, 289, 256, 225, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 9, 784, 729, 676, 625, 576, 529, 484, 441, 400, 361, 324, 289, 256, 225, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 4, 841, 784, 729, 676, 625, 576, 529, 484, 441, 400, 361, 324, 289, 256, 225, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1, 1, 900, 841, 784, 729, 676, 625, 576, 529, 484, 441, 400, 361, 324, 289, 256, 225, 196, 169, 144, 121, 100, 81, 64, 49, 36, 25, 16, 9, 4, 1], [INT____00001, x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9], x[10], x[11], x[12], x[13], x[14], x[15], x[16], x[17], x[18], x[19], x[20], x[21], x[22], x[23], x[24], x[25], x[26], x[27], x[28], x[29], x[30], x[31], x[32], x[34], x[35], x[36], x[37], x[38], x[39], x[40], x[41], x[42], x[43], x[44], x[45], x[46], x[47], x[48], x[49], x[50], x[51], x[52], x[53], x[54], x[55], x[56], x[57], x[58], x[59], x[60], x[61], x[62], x[63], x[64], x[66], x[67], x[68], x[69], x[70], x[71], x[72], x[73], x[74], x[75], x[76], x[77], x[78], x[79], x[80], x[81], x[82], x[83], x[84], x[85], x[86], x[87], x[88], x[89], x[90], x[91], x[92], x[93], x[94], x[95], x[96], x[98], x[99], x[100], x[101], x[102], x[103], x[104], x[105], x[106], x[107], x[108], x[109], x[110], x[111], x[112], x[113], x[114], x[115], x[116], x[117], x[118], x[119], x[120], x[121], x[122], x[123], x[124], x[125], x[126], x[127], x[128], x[130], x[131], x[132], x[133], x[134], x[135], x[136], x[137], x[138], x[139], x[140], x[141], x[142], x[143], x[144], x[145], x[146], x[147], x[148], x[149], x[150], x[151], x[152], x[153], x[154], x[155], x[156], x[157], x[158], x[159], x[160], x[162], x[163], x[164], x[165], x[166], x[167], x[168], x[169], x[170], x[171], x[172], x[173], x[174], x[175], x[176], x[177], x[178], x[179], x[180], x[181], x[182], x[183], x[184], x[185], x[186], x[187], x[188], x[189], x[190], x[191], x[192], x[194], x[195], x[196], x[197], x[198], x[199], x[200], x[201], x[202], x[203], x[204], x[205], x[206], x[207], x[208], x[209], x[210], x[211], x[212], x[213], x[214], x[215], x[216], x[217], x[218], x[219], x[220], x[221], x[222], x[223], x[224], x[226], x[227], x[228], x[229], x[230], x[231], x[232], x[233], x[234], x[235], x[236], x[237], x[238], x[239], x[240], x[241], x[242], x[243], x[244], x[245], x[246], x[247], x[248], x[249], x[250], x[251], x[252], x[253], x[254], x[255], x[256], x[258], x[259], x[260], x[261], x[262], x[263], x[264], x[265], x[266], x[267], x[268], x[269], x[270], x[271], x[272], x[273], x[274], x[275], x[276], x[277], x[278], x[279], x[280], x[281], x[282], x[283], x[284], x[285], x[286], x[287], x[288], x[290], x[291], x[292], x[293], x[294], x[295], x[296], x[297], x[298], x[299], x[300], x[301], x[302], x[303], x[304], x[305], x[306], x[307], x[308], x[309], x[310], x[311], x[312], x[313], x[314], x[315], x[316], x[317], x[318], x[319], x[320], x[322], x[323], x[324], x[325], x[326], x[327], x[328], x[329], x[330], x[331], x[332], x[333], x[334], x[335], x[336], x[337], x[338], x[339], x[340], x[341], x[342], x[343], x[344], x[345], x[346], x[347], x[348], x[349], x[350], x[351], x[352], x[354], x[355], x[356], x[357], x[358], x[359], x[360], x[361], x[362], x[363], x[364], x[365], x[366], x[367], x[368], x[369], x[370], x[371], x[372], x[373], x[374], x[375], x[376], x[377], x[378], x[379], x[380], x[381], x[382], x[383], x[384], x[386], x[387], x[388], x[389], x[390], x[391], x[392], x[393], x[394], x[395], x[396], x[397], x[398], x[399], x[400], x[401], x[402], x[403], x[404], x[405], x[406], x[407], x[408], x[409], x[410], x[411], x[412], x[413], x[414], x[415], x[416], x[418], x[419], x[420], x[421], x[422], x[423], x[424], x[425], x[426], x[427], x[428], x[429], x[430], x[431], x[432], x[433], x[434], x[435], x[436], x[437], x[438], x[439], x[440], x[441], x[442], x[443], x[444], x[445], x[446], x[447], x[448], x[450], x[451], x[452], x[453], x[454], x[455], x[456], x[457], x[458], x[459], x[460], x[461], x[462], x[463], x[464], x[465], x[466], x[467], x[468], x[469], x[470], x[471], x[472], x[473], x[474], x[475], x[476], x[477], x[478], x[479], x[480], x[482], x[483], x[484], x[485], x[486], x[487], x[488], x[489], x[490], x[491], x[492], x[493], x[494], x[495], x[496], x[497], x[498], x[499], x[500], x[501], x[502], x[503], x[504], x[505], x[506], x[507], x[508], x[509], x[510], x[511], x[512], x[514], x[515], x[516], x[517], x[518], x[519], x[520], x[521], x[522], x[523], x[524], x[525], x[526], x[527], x[528], x[529], x[530], x[531], x[532], x[533], x[534], x[535], x[536], x[537], x[538], x[539], x[540], x[541], x[542], x[543], x[544], x[546], x[547], x[548], x[549], x[550], x[551], x[552], x[553], x[554], x[555], x[556], x[557], x[558], x[559], x[560], x[561], x[562], x[563], x[564], x[565], x[566], x[567], x[568], x[569], x[570], x[571], x[572], x[573], x[574], x[575], x[576], x[578], x[579], x[580], x[581], x[582], x[583], x[584], x[585], x[586], x[587], x[588], x[589], x[590], x[591], x[592], x[593], x[594], x[595], x[596], x[597], x[598], x[599], x[600], x[601], x[602], x[603], x[604], x[605], x[606], x[607], x[608], x[610], x[611], x[612], x[613], x[614], x[615], x[616], x[617], x[618], x[619], x[620], x[621], x[622], x[623], x[624], x[625], x[626], x[627], x[628], x[629], x[630], x[631], x[632], x[633], x[634], x[635], x[636], x[637], x[638], x[639], x[640], x[642], x[643], x[644], x[645], x[646], x[647], x[648], x[649], x[650], x[651], x[652], x[653], x[654], x[655], x[656], x[657], x[658], x[659], x[660], x[661], x[662], x[663], x[664], x[665], x[666], x[667], x[668], x[669], x[670], x[671], x[672], x[674], x[675], x[676], x[677], x[678], x[679], x[680], x[681], x[682], x[683], x[684], x[685], x[686], x[687], x[688], x[689], x[690], x[691], x[692], x[693], x[694], x[695], x[696], x[697], x[698], x[699], x[700], x[701], x[702], x[703], x[704], x[706], x[707], x[708], x[709], x[710], x[711], x[712], x[713], x[714], x[715], x[716], x[717], x[718], x[719], x[720], x[721], x[722], x[723], x[724], x[725], x[726], x[727], x[728], x[729], x[730], x[731], x[732], x[733], x[734], x[735], x[736], x[738], x[739], x[740], x[741], x[742], x[743], x[744], x[745], x[746], x[747], x[748], x[749], x[750], x[751], x[752], x[753], x[754], x[755], x[756], x[757], x[758], x[759], x[760], x[761], x[762], x[763], x[764], x[765], x[766], x[767], x[768], x[770], x[771], x[772], x[773], x[774], x[775], x[776], x[777], x[778], x[779], x[780], x[781], x[782], x[783], x[784], x[785], x[786], x[787], x[788], x[789], x[790], x[791], x[792], x[793], x[794], x[795], x[796], x[797], x[798], x[799], x[800], x[802], x[803], x[804], x[805], x[806], x[807], x[808], x[809], x[810], x[811], x[812], x[813], x[814], x[815], x[816], x[817], x[818], x[819], x[820], x[821], x[822], x[823], x[824], x[825], x[826], x[827], x[828], x[829], x[830], x[831], x[832], x[834], x[835], x[836], x[837], x[838], x[839], x[840], x[841], x[842], x[843], x[844], x[845], x[846], x[847], x[848], x[849], x[850], x[851], x[852], x[853], x[854], x[855], x[856], x[857], x[858], x[859], x[860], x[861], x[862], x[863], x[864], x[866], x[867], x[868], x[869], x[870], x[871], x[872], x[873], x[874], x[875], x[876], x[877], x[878], x[879], x[880], x[881], x[882], x[883], x[884], x[885], x[886], x[887], x[888], x[889], x[890], x[891], x[892], x[893], x[894], x[895], x[896], x[898], x[899], x[900], x[901], x[902], x[903], x[904], x[905], x[906], x[907], x[908], x[909], x[910], x[911], x[912], x[913], x[914], x[915], x[916], x[917], x[918], x[919], x[920], x[921], x[922], x[923], x[924], x[925], x[926], x[927], x[928], x[930], x[931], x[932], x[933], x[934], x[935], x[936], x[937], x[938], x[939], x[940], x[941], x[942], x[943], x[944], x[945], x[946], x[947], x[948], x[949], x[950], x[951], x[952], x[953], x[954], x[955], x[956], x[957], x[958], x[959], x[960]], 0) :: defines_var(INT____00001);
solve  :: int_search([x[1], x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9], x[10], x[11], x[12], x[13], x[14], x[15], x[16], x[17], x[18], x[19], x[20], x[21], x[22], x[23], x[24], x[25], x[26], x[27], x[28], x[29], x[30], x[31], x[32], x[33], x[34], x[35], x[36], x[37], x[38], x[39], x[40], x[41], x[42], x[43], x[44], x[45], x[46], x[47], x[48], x[49], x[50], x[51], x[52], x[53], x[54], x[55], x[56], x[57], x[58], x[59], x[60], x[61], x[62], x[63], x[64], x[65], x[66], x[67], x[68], x[69], x[70], x[71], x[72], x[73], x[74], x[75], x[76], x[77], x[78], x[79], x[80], x[81], x[82], x[83], x[84], x[85], x[86], x[87], x[88], x[89], x[90], x[91], x[92], x[93], x[94], x[95], x[96], x[97], x[98], x[99], x[100], x[101], x[102], x[103], x[104], x[105], x[106], x[107], x[108], x[109], x[110], x[111], x[112], x[113], x[114], x[115], x[116], x[117], x[118], x[119], x[120], x[121], x[122], x[123], x[124], x[125], x[126], x[127], x[128], x[129], x[130], x[131], x[132], x[133], x[134], x[135], x[136], x[137], x[138], x[139], x[140], x[141], x[142], x[143], x[144], x[145], x[146], x[147], x[148], x[149], x[150], x[151], x[152], x[153], x[154], x[155], x[156], x[157], x[158], x[159], x[160], x[161], x[162], x[163], x[164], x[165], x[166], x[167], x[168], x[169], x[170], x[171], x[172], x[173], x[174], x[175], x[176], x[177], x[178], x[179], x[180], x[181], x[182], x[183], x[184], x[185], x[186], x[187], x[188], x[189], x[190], x[191], x[192], x[193], x[194], x[195], x[196], x[197], x[198], x[199], x[200], x[201], x[202], x[203], x[204], x[205], x[206], x[207], x[208], x[209], x[210], x[211], x[212], x[213], x[214], x[215], x[216], x[217], x[218], x[219], x[220], x[221], x[222], x[223], x[224], x[225], x[226], x[227], x[228], x[229], x[230], x[231], x[232], x[233], x[234], x[235], x[236], x[237], x[238], x[239], x[240], x[241], x[242], x[243], x[244], x[245], x[246], x[247], x[248], x[249], x[250], x[251], x[252], x[253], x[254], x[255], x[256], x[257], x[258], x[259], x[260], x[261], x[262], x[263], x[264], x[265], x[266], x[267], x[268], x[269], x[270], x[271], x[272], x[273], x[274], x[275], x[276], x[277], x[278], x[279], x[280], x[281], x[282], x[283], x[284], x[285], x[286], x[287], x[288], x[289], x[290], x[291], x[292], x[293], x[294], x[295], x[296], x[297], x[298], x[299], x[300], x[301], x[302], x[303], x[304], x[305], x[306], x[307], x[308], x[309], x[310], x[311], x[312], x[313], x[314], x[315], x[316], x[317], x[318], x[319], x[320], x[321], x[322], x[323], x[324], x[325], x[326], x[327], x[328], x[329], x[330], x[331], x[332], x[333], x[334], x[335], x[336], x[337], x[338], x[339], x[340], x[341], x[342], x[343], x[344], x[345], x[346], x[347], x[348], x[349], x[350], x[351], x[352], x[353], x[354], x[355], x[356], x[357], x[358], x[359], x[360], x[361], x[362], x[363], x[364], x[365], x[366], x[367], x[368], x[369], x[370], x[371], x[372], x[373], x[374], x[375], x[376], x[377], x[378], x[379], x[380], x[381], x[382], x[383], x[384], x[385], x[386], x[387], x[388], x[389], x[390], x[391], x[392], x[393], x[394], x[395], x[396], x[397], x[398], x[399], x[400], x[401], x[402], x[403], x[404], x[405], x[406], x[407], x[408], x[409], x[410], x[411], x[412], x[413], x[414], x[415], x[416], x[417], x[418], x[419], x[420], x[421], x[422], x[423], x[424], x[425], x[426], x[427], x[428], x[429], x[430], x[431], x[432], x[433], x[434], x[435], x[436], x[437], x[438], x[439], x[440], x[441], x[442], x[443], x[444], x[445], x[446], x[447], x[448], x[449], x[450], x[451], x[452], x[453], x[454], x[455], x[456], x[457], x[458], x[459], x[460], x[461], x[462], x[463], x[464], x[465], x[466], x[467], x[468], x[469], x[470], x[471], x[472], x[473], x[474], x[475], x[476], x[477], x[478], x[479], x[480], x[481], x[482], x[483], x[484], x[485], x[486], x[487], x[488], x[489], x[490], x[491], x[492], x[493], x[494], x[495], x[496], x[497], x[498], x[499], x[500], x[501], x[502], x[503], x[504], x[505], x[506], x[507], x[508], x[509], x[510], x[511], x[512], x[513], x[514], x[515], x[516], x[517], x[518], x[519], x[520], x[521], x[522], x[523], x[524], x[525], x[526], x[527], x[528], x[529], x[530], x[531], x[532], x[533], x[534], x[535], x[536], x[537], x[538], x[539], x[540], x[541], x[542], x[543], x[544], x[545], x[546], x[547], x[548], x[549], x[550], x[551], x[552], x[553], x[554], x[555], x[556], x[557], x[558], x[559], x[560], x[561], x[562], x[563], x[564], x[565], x[566], x[567], x[568], x[569], x[570], x[571], x[572], x[573], x[574], x[575], x[576], x[577], x[578], x[579], x[580], x[581], x[582], x[583], x[584], x[585], x[586], x[587], x[588], x[589], x[590], x[591], x[592], x[593], x[594], x[595], x[596], x[597], x[598], x[599], x[600], x[601], x[602], x[603], x[604], x[605], x[606], x[607], x[608], x[609], x[610], x[611], x[612], x[613], x[614], x[615], x[616], x[617], x[618], x[619], x[620], x[621], x[622], x[623], x[624], x[625], x[626], x[627], x[628], x[629], x[630], x[631], x[632], x[633], x[634], x[635], x[636], x[637], x[638], x[639], x[640], x[641], x[642], x[643], x[644], x[645], x[646], x[647], x[648], x[649], x[650], x[651], x[652], x[653], x[654], x[655], x[656], x[657], x[658], x[659], x[660], x[661], x[662], x[663], x[664], x[665], x[666], x[667], x[668], x[669], x[670], x[671], x[672], x[673], x[674], x[675], x[676], x[677], x[678], x[679], x[680], x[681], x[682], x[683], x[684], x[685], x[686], x[687], x[688], x[689], x[690], x[691], x[692], x[693], x[694], x[695], x[696], x[697], x[698], x[699], x[700], x[701], x[702], x[703], x[704], x[705], x[706], x[707], x[708], x[709], x[710], x[711], x[712], x[713], x[714], x[715], x[716], x[717], x[718], x[719], x[720], x[721], x[722], x[723], x[724], x[725], x[726], x[727], x[728], x[729], x[730], x[731], x[732], x[733], x[734], x[735], x[736], x[737], x[738], x[739], x[740], x[741], x[742], x[743], x[744], x[745], x[746], x[747], x[748], x[749], x[750], x[751], x[752], x[753], x[754], x[755], x[756], x[757], x[758], x[759], x[760], x[761], x[762], x[763], x[764], x[765], x[766], x[767], x[768], x[769], x[770], x[771], x[772], x[773], x[774], x[775], x[776], x[777], x[778], x[779], x[780], x[781], x[782], x[783], x[784], x[785], x[786], x[787], x[788], x[789], x[790], x[791], x[792], x[793], x[794], x[795], x[796], x[797], x[798], x[799], x[800], x[801], x[802], x[803], x[804], x[805], x[806], x[807], x[808], x[809], x[810], x[811], x[812], x[813], x[814], x[815], x[816], x[817], x[818], x[819], x[820], x[821], x[822], x[823], x[824], x[825], x[826], x[827], x[828], x[829], x[830], x[831], x[832], x[833], x[834], x[835], x[836], x[837], x[838], x[839], x[840], x[841], x[842], x[843], x[844], x[845], x[846], x[847], x[848], x[849], x[850], x[851], x[852], x[853], x[854], x[855], x[856], x[857], x[858], x[859], x[860], x[861], x[862], x[863], x[864], x[865], x[866], x[867], x[868], x[869], x[870], x[871], x[872], x[873], x[874], x[875], x[876], x[877], x[878], x[879], x[880], x[881], x[882], x[883], x[884], x[885], x[886], x[887], x[888], x[889], x[890], x[891], x[892], x[893], x[894], x[895], x[896], x[897], x[898], x[899], x[900], x[901], x[902], x[903], x[904], x[905], x[906], x[907], x[908], x[909], x[910], x[911], x[912], x[913], x[914], x[915], x[916], x[917], x[918], x[919], x[920], x[921], x[922], x[923], x[924], x[925], x[926], x[927], x[928], x[929], x[930], x[931], x[932], x[933], x[934], x[935], x[936], x[937], x[938], x[939], x[940], x[941], x[942], x[943], x[944], x[945], x[946], x[947], x[948], x[949], x[950], x[951], x[952], x[953], x[954], x[955], x[956], x[957], x[958], x[959], x[960], x[961], INT____00001], most_constrained, indomain_max, complete) minimize INT____00001;