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..169] of var 0..1: x :: output_array([1..13, 1..13]); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[1], x[2], x[3], x[14], x[16], x[27], x[28], x[29]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[2], x[3], x[4], x[15], x[17], x[28], x[29], x[30]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[3], x[4], x[5], x[16], x[18], x[29], x[30], x[31]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[4], x[5], x[6], x[17], x[19], x[30], x[31], x[32]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[5], x[6], x[7], x[18], x[20], x[31], x[32], x[33]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[6], x[7], x[8], x[19], x[21], x[32], x[33], x[34]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[7], x[8], x[9], x[20], x[22], x[33], x[34], x[35]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[8], x[9], x[10], x[21], x[23], x[34], x[35], x[36]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[9], x[10], x[11], x[22], x[24], x[35], x[36], x[37]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[10], x[11], x[12], x[23], x[25], x[36], x[37], x[38]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[11], x[12], x[13], x[24], x[26], x[37], x[38], x[39]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[14], x[15], x[16], x[27], x[29], x[40], x[41], x[42]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[15], x[16], x[17], x[28], x[30], x[41], x[42], x[43]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[16], x[17], x[18], x[29], x[31], x[42], x[43], x[44]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[17], x[18], x[19], x[30], x[32], x[43], x[44], x[45]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[18], x[19], x[20], x[31], x[33], x[44], x[45], x[46]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[19], x[20], x[21], x[32], x[34], x[45], x[46], x[47]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[20], x[21], x[22], x[33], x[35], x[46], x[47], x[48]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[21], x[22], x[23], x[34], x[36], x[47], x[48], x[49]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[22], x[23], x[24], x[35], x[37], x[48], x[49], x[50]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[23], x[24], x[25], x[36], x[38], x[49], x[50], x[51]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[24], x[25], x[26], x[37], x[39], x[50], x[51], x[52]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[27], x[28], x[29], x[40], x[42], x[53], x[54], x[55]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[28], x[29], x[30], x[41], x[43], x[54], x[55], x[56]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[29], x[30], x[31], x[42], x[44], x[55], x[56], x[57]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[30], x[31], x[32], x[43], x[45], x[56], x[57], x[58]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[31], x[32], x[33], x[44], x[46], x[57], x[58], x[59]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[32], x[33], x[34], x[45], x[47], x[58], x[59], x[60]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[33], x[34], x[35], x[46], x[48], x[59], x[60], x[61]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[34], x[35], x[36], x[47], x[49], x[60], x[61], x[62]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[35], x[36], x[37], x[48], x[50], x[61], x[62], x[63]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[36], x[37], x[38], x[49], x[51], x[62], x[63], x[64]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[37], x[38], x[39], x[50], x[52], x[63], x[64], x[65]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[40], x[41], x[42], x[53], x[55], x[66], x[67], x[68]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[41], x[42], x[43], x[54], x[56], x[67], x[68], x[69]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[42], x[43], x[44], x[55], x[57], x[68], x[69], x[70]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[43], x[44], x[45], x[56], x[58], x[69], x[70], x[71]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[44], x[45], x[46], x[57], x[59], x[70], x[71], x[72]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[45], x[46], x[47], x[58], x[60], x[71], x[72], x[73]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[46], x[47], x[48], x[59], x[61], x[72], x[73], x[74]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[47], x[48], x[49], x[60], x[62], x[73], x[74], x[75]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[48], x[49], x[50], x[61], x[63], x[74], x[75], x[76]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[49], x[50], x[51], x[62], x[64], x[75], x[76], x[77]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[50], x[51], x[52], x[63], x[65], x[76], x[77], x[78]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[53], x[54], x[55], x[66], x[68], x[79], x[80], x[81]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[54], x[55], x[56], x[67], x[69], x[80], x[81], x[82]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[55], x[56], x[57], x[68], x[70], x[81], x[82], x[83]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[56], x[57], x[58], x[69], x[71], x[82], x[83], x[84]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[57], x[58], x[59], x[70], x[72], x[83], x[84], x[85]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[58], x[59], x[60], x[71], x[73], x[84], x[85], x[86]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[59], x[60], x[61], x[72], x[74], x[85], x[86], x[87]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[60], x[61], x[62], x[73], x[75], x[86], x[87], x[88]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[61], x[62], x[63], x[74], x[76], x[87], x[88], x[89]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[62], x[63], x[64], x[75], x[77], x[88], x[89], x[90]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[63], x[64], x[65], x[76], x[78], x[89], x[90], x[91]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[66], x[67], x[68], x[79], x[81], x[92], x[93], x[94]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[67], x[68], x[69], x[80], x[82], x[93], x[94], x[95]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[68], x[69], x[70], x[81], x[83], x[94], x[95], x[96]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[69], x[70], x[71], x[82], x[84], x[95], x[96], x[97]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[70], x[71], x[72], x[83], x[85], x[96], x[97], x[98]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[71], x[72], x[73], x[84], x[86], x[97], x[98], x[99]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[72], x[73], x[74], x[85], x[87], x[98], x[99], x[100]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[73], x[74], x[75], x[86], x[88], x[99], x[100], x[101]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[74], x[75], x[76], x[87], x[89], x[100], x[101], x[102]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[75], x[76], x[77], x[88], x[90], x[101], x[102], x[103]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[76], x[77], x[78], x[89], x[91], x[102], x[103], x[104]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[79], x[80], x[81], x[92], x[94], x[105], x[106], x[107]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[80], x[81], x[82], x[93], x[95], x[106], x[107], x[108]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[81], x[82], x[83], x[94], x[96], x[107], x[108], x[109]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[82], x[83], x[84], x[95], x[97], x[108], x[109], x[110]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[83], x[84], x[85], x[96], x[98], x[109], x[110], x[111]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[84], x[85], x[86], x[97], x[99], x[110], x[111], x[112]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[85], x[86], x[87], x[98], x[100], x[111], x[112], x[113]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[86], x[87], x[88], x[99], x[101], x[112], x[113], x[114]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[87], x[88], x[89], x[100], x[102], x[113], x[114], x[115]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[88], x[89], x[90], x[101], x[103], x[114], x[115], x[116]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[89], x[90], x[91], x[102], x[104], x[115], x[116], x[117]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[92], x[93], x[94], x[105], x[107], x[118], x[119], x[120]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[93], x[94], x[95], x[106], x[108], x[119], x[120], x[121]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[94], x[95], x[96], x[107], x[109], x[120], x[121], x[122]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[95], x[96], x[97], x[108], x[110], x[121], x[122], x[123]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[96], x[97], x[98], x[109], x[111], x[122], x[123], x[124]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[97], x[98], x[99], x[110], x[112], x[123], x[124], x[125]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[98], x[99], x[100], x[111], x[113], x[124], x[125], x[126]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[99], x[100], x[101], x[112], x[114], x[125], x[126], x[127]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[100], x[101], x[102], x[113], x[115], x[126], x[127], x[128]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[101], x[102], x[103], x[114], x[116], x[127], x[128], x[129]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[102], x[103], x[104], x[115], x[117], x[128], x[129], x[130]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[105], x[106], x[107], x[118], x[120], x[131], x[132], x[133]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[106], x[107], x[108], x[119], x[121], x[132], x[133], x[134]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[107], x[108], x[109], x[120], x[122], x[133], x[134], x[135]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[108], x[109], x[110], x[121], x[123], x[134], x[135], x[136]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[109], x[110], x[111], x[122], x[124], x[135], x[136], x[137]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[110], x[111], x[112], x[123], x[125], x[136], x[137], x[138]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[111], x[112], x[113], x[124], x[126], x[137], x[138], x[139]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[112], x[113], x[114], x[125], x[127], x[138], x[139], x[140]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[113], x[114], x[115], x[126], x[128], x[139], x[140], x[141]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[114], x[115], x[116], x[127], x[129], x[140], x[141], x[142]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[115], x[116], x[117], x[128], x[130], x[141], x[142], x[143]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[118], x[119], x[120], x[131], x[133], x[144], x[145], x[146]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[119], x[120], x[121], x[132], x[134], x[145], x[146], x[147]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[120], x[121], x[122], x[133], x[135], x[146], x[147], x[148]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[121], x[122], x[123], x[134], x[136], x[147], x[148], x[149]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[122], x[123], x[124], x[135], x[137], x[148], x[149], x[150]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[123], x[124], x[125], x[136], x[138], x[149], x[150], x[151]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[124], x[125], x[126], x[137], x[139], x[150], x[151], x[152]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[125], x[126], x[127], x[138], x[140], x[151], x[152], x[153]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[126], x[127], x[128], x[139], x[141], x[152], x[153], x[154]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[127], x[128], x[129], x[140], x[142], x[153], x[154], x[155]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[128], x[129], x[130], x[141], x[143], x[154], x[155], x[156]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[131], x[132], x[133], x[144], x[146], x[157], x[158], x[159]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[132], x[133], x[134], x[145], x[147], x[158], x[159], x[160]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[133], x[134], x[135], x[146], x[148], x[159], x[160], x[161]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[134], x[135], x[136], x[147], x[149], x[160], x[161], x[162]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[135], x[136], x[137], x[148], x[150], x[161], x[162], x[163]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[136], x[137], x[138], x[149], x[151], x[162], x[163], x[164]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[137], x[138], x[139], x[150], x[152], x[163], x[164], x[165]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[138], x[139], x[140], x[151], x[153], x[164], x[165], x[166]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[139], x[140], x[141], x[152], x[154], x[165], x[166], x[167]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[140], x[141], x[142], x[153], x[155], x[166], x[167], x[168]], -4); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1], [x[141], x[142], x[143], x[154], x[156], x[167], x[168], x[169]], -4); solve satisfy;