predicate all_different_int(array [int] of var int: x); predicate count_eq(array [int] of var int: x, var int: y, var int: c); predicate count_reif(array [int] of var int: x, var int: y, var int: c, var bool: b); 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 global_cardinality_closed(array [int] of var int: x, array [int] of int: cover, array [int] of var int: counts); predicate global_cardinality_low_up(array [int] of var int: x, array [int] of int: cover, array [int] of int: lbound, array [int] of int: ubound); predicate global_cardinality_low_up_closed(array [int] of var int: x, array [int] of int: cover, array [int] of int: lbound, array [int] of int: ubound); 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..27] of var 0..2: bin_code :: output_array([1..27]); array [1..81] of var 0..2: binary; array [1..3] of var 0..2: t____00001; array [1..3] of var 0..2: t____00002; array [1..3] of var 0..2: t____00003; array [1..3] of var 0..2: t____00004; array [1..3] of var 0..2: t____00005; array [1..3] of var 0..2: t____00006; array [1..3] of var 0..2: t____00007; array [1..3] of var 0..2: t____00008; array [1..3] of var 0..2: t____00009; array [1..3] of var 0..2: t____00010; array [1..3] of var 0..2: t____00011; array [1..3] of var 0..2: t____00012; array [1..3] of var 0..2: t____00013; array [1..3] of var 0..2: t____00014; array [1..3] of var 0..2: t____00015; array [1..3] of var 0..2: t____00016; array [1..3] of var 0..2: t____00017; array [1..3] of var 0..2: t____00018; array [1..3] of var 0..2: t____00019; array [1..3] of var 0..2: t____00020; array [1..3] of var 0..2: t____00021; array [1..3] of var 0..2: t____00022; array [1..3] of var 0..2: t____00023; array [1..3] of var 0..2: t____00024; array [1..3] of var 0..2: t____00025; array [1..3] of var 0..2: t____00026; array [1..3] of var 0..2: t____00027; array [1..27] of var 0..26: x :: output_array([1..27]); constraint all_different_int(x); constraint int_eq(binary[1], t____00001[1]); constraint int_eq(binary[2], binary[4]); constraint int_eq(binary[2], t____00001[2]); constraint int_eq(binary[3], binary[5]); constraint int_eq(binary[3], t____00001[3]); constraint int_eq(binary[4], t____00002[1]); constraint int_eq(binary[5], binary[7]); constraint int_eq(binary[5], t____00002[2]); constraint int_eq(binary[6], binary[8]); constraint int_eq(binary[6], t____00002[3]); constraint int_eq(binary[7], t____00003[1]); constraint int_eq(binary[8], binary[10]); constraint int_eq(binary[8], t____00003[2]); constraint int_eq(binary[9], binary[11]); constraint int_eq(binary[9], t____00003[3]); constraint int_eq(binary[10], t____00004[1]); constraint int_eq(binary[11], binary[13]); constraint int_eq(binary[11], t____00004[2]); constraint int_eq(binary[12], binary[14]); constraint int_eq(binary[12], t____00004[3]); constraint int_eq(binary[13], t____00005[1]); constraint int_eq(binary[14], binary[16]); constraint int_eq(binary[14], t____00005[2]); constraint int_eq(binary[15], binary[17]); constraint int_eq(binary[15], t____00005[3]); constraint int_eq(binary[16], t____00006[1]); constraint int_eq(binary[17], binary[19]); constraint int_eq(binary[17], t____00006[2]); constraint int_eq(binary[18], binary[20]); constraint int_eq(binary[18], t____00006[3]); constraint int_eq(binary[19], t____00007[1]); constraint int_eq(binary[20], binary[22]); constraint int_eq(binary[20], t____00007[2]); constraint int_eq(binary[21], binary[23]); constraint int_eq(binary[21], t____00007[3]); constraint int_eq(binary[22], t____00008[1]); constraint int_eq(binary[23], binary[25]); constraint int_eq(binary[23], t____00008[2]); constraint int_eq(binary[24], binary[26]); constraint int_eq(binary[24], t____00008[3]); constraint int_eq(binary[25], t____00009[1]); constraint int_eq(binary[26], binary[28]); constraint int_eq(binary[26], t____00009[2]); constraint int_eq(binary[27], binary[29]); constraint int_eq(binary[27], t____00009[3]); constraint int_eq(binary[28], t____00010[1]); constraint int_eq(binary[29], binary[31]); constraint int_eq(binary[29], t____00010[2]); constraint int_eq(binary[30], binary[32]); constraint int_eq(binary[30], t____00010[3]); constraint int_eq(binary[31], t____00011[1]); constraint int_eq(binary[32], binary[34]); constraint int_eq(binary[32], t____00011[2]); constraint int_eq(binary[33], binary[35]); constraint int_eq(binary[33], t____00011[3]); constraint int_eq(binary[34], t____00012[1]); constraint int_eq(binary[35], binary[37]); constraint int_eq(binary[35], t____00012[2]); constraint int_eq(binary[36], binary[38]); constraint int_eq(binary[36], t____00012[3]); constraint int_eq(binary[37], t____00013[1]); constraint int_eq(binary[38], binary[40]); constraint int_eq(binary[38], t____00013[2]); constraint int_eq(binary[39], binary[41]); constraint int_eq(binary[39], t____00013[3]); constraint int_eq(binary[40], t____00014[1]); constraint int_eq(binary[41], binary[43]); constraint int_eq(binary[41], t____00014[2]); constraint int_eq(binary[42], binary[44]); constraint int_eq(binary[42], t____00014[3]); constraint int_eq(binary[43], t____00015[1]); constraint int_eq(binary[44], binary[46]); constraint int_eq(binary[44], t____00015[2]); constraint int_eq(binary[45], binary[47]); constraint int_eq(binary[45], t____00015[3]); constraint int_eq(binary[46], t____00016[1]); constraint int_eq(binary[47], binary[49]); constraint int_eq(binary[47], t____00016[2]); constraint int_eq(binary[48], binary[50]); constraint int_eq(binary[48], t____00016[3]); constraint int_eq(binary[49], t____00017[1]); constraint int_eq(binary[50], binary[52]); constraint int_eq(binary[50], t____00017[2]); constraint int_eq(binary[51], binary[53]); constraint int_eq(binary[51], t____00017[3]); constraint int_eq(binary[52], t____00018[1]); constraint int_eq(binary[53], binary[55]); constraint int_eq(binary[53], t____00018[2]); constraint int_eq(binary[54], binary[56]); constraint int_eq(binary[54], t____00018[3]); constraint int_eq(binary[55], t____00019[1]); constraint int_eq(binary[56], binary[58]); constraint int_eq(binary[56], t____00019[2]); constraint int_eq(binary[57], binary[59]); constraint int_eq(binary[57], t____00019[3]); constraint int_eq(binary[58], t____00020[1]); constraint int_eq(binary[59], binary[61]); constraint int_eq(binary[59], t____00020[2]); constraint int_eq(binary[60], binary[62]); constraint int_eq(binary[60], t____00020[3]); constraint int_eq(binary[61], t____00021[1]); constraint int_eq(binary[62], binary[64]); constraint int_eq(binary[62], t____00021[2]); constraint int_eq(binary[63], binary[65]); constraint int_eq(binary[63], t____00021[3]); constraint int_eq(binary[64], t____00022[1]); constraint int_eq(binary[65], binary[67]); constraint int_eq(binary[65], t____00022[2]); constraint int_eq(binary[66], binary[68]); constraint int_eq(binary[66], t____00022[3]); constraint int_eq(binary[67], t____00023[1]); constraint int_eq(binary[68], binary[70]); constraint int_eq(binary[68], t____00023[2]); constraint int_eq(binary[69], binary[71]); constraint int_eq(binary[69], t____00023[3]); constraint int_eq(binary[70], t____00024[1]); constraint int_eq(binary[71], binary[73]); constraint int_eq(binary[71], t____00024[2]); constraint int_eq(binary[72], binary[74]); constraint int_eq(binary[72], t____00024[3]); constraint int_eq(binary[73], t____00025[1]); constraint int_eq(binary[74], binary[76]); constraint int_eq(binary[74], t____00025[2]); constraint int_eq(binary[75], binary[77]); constraint int_eq(binary[75], t____00025[3]); constraint int_eq(binary[76], t____00026[1]); constraint int_eq(binary[77], binary[79]); constraint int_eq(binary[77], t____00026[2]); constraint int_eq(binary[78], binary[80]); constraint int_eq(binary[78], t____00026[3]); constraint int_eq(binary[79], t____00027[1]); constraint int_eq(binary[80], binary[1]); constraint int_eq(binary[80], t____00027[2]); constraint int_eq(binary[81], binary[2]); constraint int_eq(binary[81], t____00027[3]); constraint int_lin_eq([-9, -3, -1, 1], [t____00001[1], t____00001[2], t____00001[3], x[1]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00002[1], t____00002[2], t____00002[3], x[2]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00003[1], t____00003[2], t____00003[3], x[3]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00004[1], t____00004[2], t____00004[3], x[4]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00005[1], t____00005[2], t____00005[3], x[5]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00006[1], t____00006[2], t____00006[3], x[6]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00007[1], t____00007[2], t____00007[3], x[7]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00008[1], t____00008[2], t____00008[3], x[8]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00009[1], t____00009[2], t____00009[3], x[9]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00010[1], t____00010[2], t____00010[3], x[10]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00011[1], t____00011[2], t____00011[3], x[11]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00012[1], t____00012[2], t____00012[3], x[12]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00013[1], t____00013[2], t____00013[3], x[13]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00014[1], t____00014[2], t____00014[3], x[14]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00015[1], t____00015[2], t____00015[3], x[15]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00016[1], t____00016[2], t____00016[3], x[16]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00017[1], t____00017[2], t____00017[3], x[17]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00018[1], t____00018[2], t____00018[3], x[18]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00019[1], t____00019[2], t____00019[3], x[19]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00020[1], t____00020[2], t____00020[3], x[20]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00021[1], t____00021[2], t____00021[3], x[21]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00022[1], t____00022[2], t____00022[3], x[22]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00023[1], t____00023[2], t____00023[3], x[23]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00024[1], t____00024[2], t____00024[3], x[24]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00025[1], t____00025[2], t____00025[3], x[25]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00026[1], t____00026[2], t____00026[3], x[26]], 0); constraint int_lin_eq([-9, -3, -1, 1], [t____00027[1], t____00027[2], t____00027[3], x[27]], 0); constraint int_ne(bin_code[1], bin_code[2]); constraint int_ne(bin_code[1], bin_code[27]); constraint int_ne(bin_code[2], bin_code[3]); constraint int_ne(bin_code[3], bin_code[4]); constraint int_ne(bin_code[4], bin_code[5]); constraint int_ne(bin_code[5], bin_code[6]); constraint int_ne(bin_code[6], bin_code[7]); constraint int_ne(bin_code[7], bin_code[8]); constraint int_ne(bin_code[8], bin_code[9]); constraint int_ne(bin_code[9], bin_code[10]); constraint int_ne(bin_code[10], bin_code[11]); constraint int_ne(bin_code[11], bin_code[12]); constraint int_ne(bin_code[12], bin_code[13]); constraint int_ne(bin_code[13], bin_code[14]); constraint int_ne(bin_code[14], bin_code[15]); constraint int_ne(bin_code[15], bin_code[16]); constraint int_ne(bin_code[16], bin_code[17]); constraint int_ne(bin_code[17], bin_code[18]); constraint int_ne(bin_code[18], bin_code[19]); constraint int_ne(bin_code[19], bin_code[20]); constraint int_ne(bin_code[20], bin_code[21]); constraint int_ne(bin_code[21], bin_code[22]); constraint int_ne(bin_code[22], bin_code[23]); constraint int_ne(bin_code[23], bin_code[24]); constraint int_ne(bin_code[24], bin_code[25]); constraint int_ne(bin_code[25], bin_code[26]); constraint int_ne(bin_code[26], bin_code[27]); 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], bin_code[1], bin_code[2], bin_code[3], bin_code[4], bin_code[5], bin_code[6], bin_code[7], bin_code[8], bin_code[9], bin_code[10], bin_code[11], bin_code[12], bin_code[13], bin_code[14], bin_code[15], bin_code[16], bin_code[17], bin_code[18], bin_code[19], bin_code[20], bin_code[21], bin_code[22], bin_code[23], bin_code[24], bin_code[25], bin_code[26], bin_code[27]], first_fail, indomain_split, credit(5, bbs(1))) satisfy;