predicate all_different_int(array [int] of var int: x); predicate count(array [int] of var int: x, var int: y, var int: c); predicate fixed_cumulative(array [int] of var int: s, array [int] of int: d, array [int] of int: r, int: b); predicate global_cardinality(array [int] of var int: x, array [int] of int: cover, array [int] of var int: counts); predicate maximum_int(var int: m, array [int] of var int: x); predicate minimum_int(var int: m, array [int] of var int: x); predicate sliding_sum(int: low, int: up, int: seq, array [int] of var int: vs); predicate sort(array [int] of var int: x, array [int] of var int: y); predicate table_bool(array [int] of var bool: x, array [int, int] of bool: t); predicate table_int(array [int] of var int: x, array [int, int] of int: t); predicate var_cumulative(array [int] of var int: s, array [int] of int: d, array [int] of int: r, var int: b); array [1..64] of var 1..64: a :: output_array([1..8, 1..8]); var 1..64: a1 = a[1]; var 1..64: a2 = a[2]; var 1..64: a3 = a[3]; var 1..64: a4 = a[4]; var 1..64: a5 = a[5]; var 1..64: a6 = a[6]; var 1..64: a7 = a[7]; var 1..64: a8 = a[8]; var 1..64: b1 = a[9]; var 1..64: b2 = a[10]; var 1..64: b3 = a[11]; var 1..64: b4 = a[12]; var 1..64: b5 = a[13]; var 1..64: b6 = a[14]; var 1..64: b7 = a[15]; var 1..64: b8 = a[16]; var 1..64: c1 = a[17]; var 1..64: c2 = a[18]; var 1..64: c3 = a[19]; var 1..64: c4 = a[20]; var 1..64: c5 = a[21]; var 1..64: c6 = a[22]; var 1..64: c7 = a[23]; var 1..64: c8 = a[24]; var 1..64: d1 = a[25]; var 1..64: d2 = a[26]; var 1..64: d3 = a[27]; var 1..64: d4 = a[28]; var 1..64: d5 = a[29]; var 1..64: d6 = a[30]; var 1..64: d7 = a[31]; var 1..64: d8 = a[32]; var 1..64: e1 = a[33]; var 1..64: e2 = a[34]; var 1..64: e3 = a[35]; var 1..64: e4 = a[36]; var 1..64: e5 = a[37]; var 1..64: e6 = a[38]; var 1..64: e7 = a[39]; var 1..64: e8 = a[40]; var 1..64: f1 = a[41]; var 1..64: f2 = a[42]; var 1..64: f3 = a[43]; var 1..64: f4 = a[44]; var 1..64: f5 = a[45]; var 1..64: f6 = a[46]; var 1..64: f7 = a[47]; var 1..64: f8 = a[48]; var 1..64: g1 = a[49]; var 1..64: g2 = a[50]; var 1..64: g3 = a[51]; var 1..64: g4 = a[52]; var 1..64: g5 = a[53]; var 1..64: g6 = a[54]; var 1..64: g7 = a[55]; var 1..64: g8 = a[56]; var 1..64: h1 = a[57]; var 1..64: h2 = a[58]; var 1..64: h3 = a[59]; var 1..64: h4 = a[60]; var 1..64: h5 = a[61]; var 1..64: h6 = a[62]; var 1..64: h7 = a[63]; var 1..64: h8 = a[64]; constraint all_different_int([a[1], a[2], a[3], a[4], a[5], a[6], a[7], a[8]]); constraint all_different_int([a[1], a[9], a[17], a[25], a[33], a[41], a[49], a[57]]); constraint all_different_int([a[2], a[10], a[18], a[26], a[34], a[42], a[50], a[58]]); constraint all_different_int([a[3], a[11], a[19], a[27], a[35], a[43], a[51], a[59]]); constraint all_different_int([a[4], a[12], a[20], a[28], a[36], a[44], a[52], a[60]]); constraint all_different_int([a[5], a[13], a[21], a[29], a[37], a[45], a[53], a[61]]); constraint all_different_int([a[6], a[14], a[22], a[30], a[38], a[46], a[54], a[62]]); constraint all_different_int([a[7], a[15], a[23], a[31], a[39], a[47], a[55], a[63]]); constraint all_different_int([a[8], a[16], a[24], a[32], a[40], a[48], a[56], a[64]]); constraint all_different_int([a[9], a[10], a[11], a[12], a[13], a[14], a[15], a[16]]); constraint all_different_int([a[17], a[18], a[19], a[20], a[21], a[22], a[23], a[24]]); constraint all_different_int([a[25], a[26], a[27], a[28], a[29], a[30], a[31], a[32]]); constraint all_different_int([a[33], a[34], a[35], a[36], a[37], a[38], a[39], a[40]]); constraint all_different_int([a[41], a[42], a[43], a[44], a[45], a[46], a[47], a[48]]); constraint all_different_int([a[49], a[50], a[51], a[52], a[53], a[54], a[55], a[56]]); constraint all_different_int([a[57], a[58], a[59], a[60], a[61], a[62], a[63], a[64]]); constraint int_lin_eq([1, 1, 1, 1], [a[1], a[2], a[3], a[4]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[1], a[2], a[9], a[10]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[1], a[2], a[57], a[58]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[1], a[8], a[9], a[16]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[1], a[8], a[57], a[64]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[1], a[9], a[17], a[25]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[2], a[3], a[10], a[11]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[2], a[3], a[58], a[59]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[2], a[10], a[18], a[26]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[3], a[4], a[11], a[12]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[3], a[4], a[59], a[60]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[3], a[11], a[19], a[27]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[4], a[5], a[12], a[13]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[4], a[5], a[60], a[61]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[4], a[12], a[20], a[28]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[5], a[6], a[7], a[8]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[5], a[6], a[13], a[14]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[5], a[6], a[61], a[62]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[5], a[13], a[21], a[29]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[6], a[7], a[14], a[15]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[6], a[7], a[62], a[63]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[6], a[14], a[22], a[30]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[7], a[8], a[15], a[16]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[7], a[8], a[63], a[64]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[7], a[15], a[23], a[31]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[8], a[16], a[24], a[32]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[9], a[10], a[11], a[12]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[9], a[10], a[17], a[18]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[9], a[16], a[17], a[24]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[10], a[11], a[18], a[19]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[11], a[12], a[19], a[20]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[12], a[13], a[20], a[21]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[13], a[14], a[15], a[16]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[13], a[14], a[21], a[22]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[14], a[15], a[22], a[23]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[15], a[16], a[23], a[24]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[17], a[18], a[19], a[20]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[17], a[18], a[25], a[26]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[17], a[24], a[25], a[32]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[18], a[19], a[26], a[27]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[19], a[20], a[27], a[28]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[20], a[21], a[28], a[29]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[21], a[22], a[23], a[24]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[21], a[22], a[29], a[30]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[22], a[23], a[30], a[31]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[23], a[24], a[31], a[32]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[25], a[26], a[27], a[28]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[25], a[26], a[33], a[34]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[25], a[32], a[33], a[40]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[26], a[27], a[34], a[35]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[27], a[28], a[35], a[36]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[28], a[29], a[36], a[37]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[29], a[30], a[31], a[32]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[29], a[30], a[37], a[38]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[30], a[31], a[38], a[39]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[31], a[32], a[39], a[40]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[33], a[34], a[35], a[36]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[33], a[34], a[41], a[42]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[33], a[40], a[41], a[48]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[33], a[41], a[49], a[57]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[34], a[35], a[42], a[43]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[34], a[42], a[50], a[58]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[35], a[36], a[43], a[44]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[35], a[43], a[51], a[59]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[36], a[37], a[44], a[45]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[36], a[44], a[52], a[60]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[37], a[38], a[39], a[40]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[37], a[38], a[45], a[46]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[37], a[45], a[53], a[61]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[38], a[39], a[46], a[47]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[38], a[46], a[54], a[62]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[39], a[40], a[47], a[48]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[39], a[47], a[55], a[63]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[40], a[48], a[56], a[64]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[41], a[42], a[43], a[44]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[41], a[42], a[49], a[50]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[41], a[48], a[49], a[56]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[42], a[43], a[50], a[51]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[43], a[44], a[51], a[52]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[44], a[45], a[52], a[53]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[45], a[46], a[47], a[48]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[45], a[46], a[53], a[54]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[46], a[47], a[54], a[55]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[47], a[48], a[55], a[56]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[49], a[50], a[51], a[52]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[49], a[50], a[57], a[58]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[49], a[56], a[57], a[64]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[50], a[51], a[58], a[59]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[51], a[52], a[59], a[60]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[52], a[53], a[60], a[61]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[53], a[54], a[55], a[56]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[53], a[54], a[61], a[62]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[54], a[55], a[62], a[63]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[55], a[56], a[63], a[64]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[57], a[58], a[59], a[60]], 130); constraint int_lin_eq([1, 1, 1, 1], [a[61], a[62], a[63], a[64]], 130); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[1], a[8], a[10], a[15], a[19], a[22], a[28], a[29]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[1], a[8], a[44], a[45], a[51], a[54], a[58], a[63]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[1], a[10], a[19], a[28], a[36], a[43], a[50], a[57]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[1], a[16], a[23], a[30], a[38], a[47], a[56], a[57]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[2], a[7], a[9], a[16], a[52], a[53], a[59], a[62]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[2], a[7], a[11], a[14], a[20], a[21], a[57], a[64]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[2], a[9], a[24], a[31], a[39], a[48], a[49], a[58]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[2], a[11], a[20], a[29], a[37], a[44], a[51], a[58]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[3], a[6], a[10], a[15], a[17], a[24], a[60], a[61]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[3], a[6], a[12], a[13], a[49], a[56], a[58], a[63]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[3], a[10], a[17], a[32], a[40], a[41], a[50], a[59]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[3], a[12], a[21], a[30], a[38], a[45], a[52], a[59]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[4], a[5], a[11], a[14], a[18], a[23], a[25], a[32]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[4], a[5], a[41], a[48], a[50], a[55], a[59], a[62]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[4], a[11], a[18], a[25], a[33], a[42], a[51], a[60]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[4], a[13], a[22], a[31], a[39], a[46], a[53], a[60]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[5], a[12], a[19], a[26], a[34], a[43], a[52], a[61]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[5], a[14], a[23], a[32], a[40], a[47], a[54], a[61]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[6], a[13], a[20], a[27], a[35], a[44], a[53], a[62]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[6], a[15], a[24], a[25], a[33], a[48], a[55], a[62]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[7], a[14], a[21], a[28], a[36], a[45], a[54], a[63]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[7], a[16], a[17], a[26], a[34], a[41], a[56], a[63]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[8], a[9], a[18], a[27], a[35], a[42], a[49], a[64]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[8], a[15], a[22], a[29], a[37], a[46], a[55], a[64]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[9], a[16], a[18], a[23], a[27], a[30], a[36], a[37]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[12], a[13], a[19], a[22], a[26], a[31], a[33], a[40]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[17], a[24], a[26], a[31], a[35], a[38], a[44], a[45]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[20], a[21], a[27], a[30], a[34], a[39], a[41], a[48]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[25], a[32], a[34], a[39], a[43], a[46], a[52], a[53]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[28], a[29], a[35], a[38], a[42], a[47], a[49], a[56]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[33], a[40], a[42], a[47], a[51], a[54], a[60], a[61]], 260); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1], [a[36], a[37], a[43], a[46], a[50], a[55], a[57], a[64]], 260); constraint int_lt(a[8], a[1]); constraint int_lt(a[57], a[1]); constraint int_lt(a[57], a[8]); constraint int_lt(a[64], a[1]); solve :: int_search([a[1], a[2], a[3], a[4], a[5], a[6], a[7], a[8], a[9], a[10], a[11], a[12], a[13], a[14], a[15], a[16], a[17], a[18], a[19], a[20], a[21], a[22], a[23], a[24], a[25], a[26], a[27], a[28], a[29], a[30], a[31], a[32], a[33], a[34], a[35], a[36], a[37], a[38], a[39], a[40], a[41], a[42], a[43], a[44], a[45], a[46], a[47], a[48], a[49], a[50], a[51], a[52], a[53], a[54], a[55], a[56], a[57], a[58], a[59], a[60], a[61], a[62], a[63], a[64]], first_fail, indomain, complete) satisfy;