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);
var bool: BOOL____00017 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00019 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00021 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00023 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00025 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00027 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00029 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00031 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00033 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00035 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00037 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00039 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00041 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00043 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00045 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00047 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00049 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00051 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00053 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00055 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00057 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00059 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00061 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00063 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00065 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00067 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00069 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00071 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00073 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00075 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00077 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00079 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00081 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00083 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00085 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00087 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00089 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00091 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00093 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00095 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00097 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00099 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00101 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00103 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00105 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00107 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00109 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00111 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00113 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00115 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00117 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00119 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00121 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00123 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00125 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00127 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00129 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00131 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00133 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00135 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00018 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00020 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00022 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00024 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00026 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00028 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00030 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00032 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00034 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00036 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00038 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00040 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00042 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00044 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00046 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00048 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00050 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00052 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00054 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00056 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00058 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00060 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00062 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00064 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00066 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00068 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00070 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00072 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00074 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00076 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00078 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00080 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00082 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00084 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00086 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00088 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00090 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00092 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00094 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00096 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00098 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00100 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00102 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00104 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00106 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00108 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00110 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00112 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00114 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00116 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00118 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00120 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00122 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00124 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00126 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00128 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00130 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00132 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00134 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00136 :: is_defined_var :: var_is_introduced;
array [1..64] of var 0..1: binary;
array [1..16] of var 0..4: num_bits :: output_array([1..16]);
array [1..4] of var 0..1: t____00001;
array [1..4] of var 0..1: t____00002;
array [1..4] of var 0..1: t____00003;
array [1..4] of var 0..1: t____00004;
array [1..4] of var 0..1: t____00005;
array [1..4] of var 0..1: t____00006;
array [1..4] of var 0..1: t____00007;
array [1..4] of var 0..1: t____00008;
array [1..4] of var 0..1: t____00009;
array [1..4] of var 0..1: t____00010;
array [1..4] of var 0..1: t____00011;
array [1..4] of var 0..1: t____00012;
array [1..4] of var 0..1: t____00013;
array [1..4] of var 0..1: t____00014;
array [1..4] of var 0..1: t____00015;
array [1..4] of var 0..1: t____00016;
array [1..16] of var 0..16: x :: output_array([1..16]);
constraint all_different_int(x);
constraint bool2int(BOOL____00017, INT____00018) :: defines_var(INT____00018);
constraint bool2int(BOOL____00019, INT____00020) :: defines_var(INT____00020);
constraint bool2int(BOOL____00021, INT____00022) :: defines_var(INT____00022);
constraint bool2int(BOOL____00023, INT____00024) :: defines_var(INT____00024);
constraint bool2int(BOOL____00025, INT____00026) :: defines_var(INT____00026);
constraint bool2int(BOOL____00027, INT____00028) :: defines_var(INT____00028);
constraint bool2int(BOOL____00029, INT____00030) :: defines_var(INT____00030);
constraint bool2int(BOOL____00031, INT____00032) :: defines_var(INT____00032);
constraint bool2int(BOOL____00033, INT____00034) :: defines_var(INT____00034);
constraint bool2int(BOOL____00035, INT____00036) :: defines_var(INT____00036);
constraint bool2int(BOOL____00037, INT____00038) :: defines_var(INT____00038);
constraint bool2int(BOOL____00039, INT____00040) :: defines_var(INT____00040);
constraint bool2int(BOOL____00041, INT____00042) :: defines_var(INT____00042);
constraint bool2int(BOOL____00043, INT____00044) :: defines_var(INT____00044);
constraint bool2int(BOOL____00045, INT____00046) :: defines_var(INT____00046);
constraint bool2int(BOOL____00047, INT____00048) :: defines_var(INT____00048);
constraint bool2int(BOOL____00049, INT____00050) :: defines_var(INT____00050);
constraint bool2int(BOOL____00051, INT____00052) :: defines_var(INT____00052);
constraint bool2int(BOOL____00053, INT____00054) :: defines_var(INT____00054);
constraint bool2int(BOOL____00055, INT____00056) :: defines_var(INT____00056);
constraint bool2int(BOOL____00057, INT____00058) :: defines_var(INT____00058);
constraint bool2int(BOOL____00059, INT____00060) :: defines_var(INT____00060);
constraint bool2int(BOOL____00061, INT____00062) :: defines_var(INT____00062);
constraint bool2int(BOOL____00063, INT____00064) :: defines_var(INT____00064);
constraint bool2int(BOOL____00065, INT____00066) :: defines_var(INT____00066);
constraint bool2int(BOOL____00067, INT____00068) :: defines_var(INT____00068);
constraint bool2int(BOOL____00069, INT____00070) :: defines_var(INT____00070);
constraint bool2int(BOOL____00071, INT____00072) :: defines_var(INT____00072);
constraint bool2int(BOOL____00073, INT____00074) :: defines_var(INT____00074);
constraint bool2int(BOOL____00075, INT____00076) :: defines_var(INT____00076);
constraint bool2int(BOOL____00077, INT____00078) :: defines_var(INT____00078);
constraint bool2int(BOOL____00079, INT____00080) :: defines_var(INT____00080);
constraint bool2int(BOOL____00081, INT____00082) :: defines_var(INT____00082);
constraint bool2int(BOOL____00083, INT____00084) :: defines_var(INT____00084);
constraint bool2int(BOOL____00085, INT____00086) :: defines_var(INT____00086);
constraint bool2int(BOOL____00087, INT____00088) :: defines_var(INT____00088);
constraint bool2int(BOOL____00089, INT____00090) :: defines_var(INT____00090);
constraint bool2int(BOOL____00091, INT____00092) :: defines_var(INT____00092);
constraint bool2int(BOOL____00093, INT____00094) :: defines_var(INT____00094);
constraint bool2int(BOOL____00095, INT____00096) :: defines_var(INT____00096);
constraint bool2int(BOOL____00097, INT____00098) :: defines_var(INT____00098);
constraint bool2int(BOOL____00099, INT____00100) :: defines_var(INT____00100);
constraint bool2int(BOOL____00101, INT____00102) :: defines_var(INT____00102);
constraint bool2int(BOOL____00103, INT____00104) :: defines_var(INT____00104);
constraint bool2int(BOOL____00105, INT____00106) :: defines_var(INT____00106);
constraint bool2int(BOOL____00107, INT____00108) :: defines_var(INT____00108);
constraint bool2int(BOOL____00109, INT____00110) :: defines_var(INT____00110);
constraint bool2int(BOOL____00111, INT____00112) :: defines_var(INT____00112);
constraint bool2int(BOOL____00113, INT____00114) :: defines_var(INT____00114);
constraint bool2int(BOOL____00115, INT____00116) :: defines_var(INT____00116);
constraint bool2int(BOOL____00117, INT____00118) :: defines_var(INT____00118);
constraint bool2int(BOOL____00119, INT____00120) :: defines_var(INT____00120);
constraint bool2int(BOOL____00121, INT____00122) :: defines_var(INT____00122);
constraint bool2int(BOOL____00123, INT____00124) :: defines_var(INT____00124);
constraint bool2int(BOOL____00125, INT____00126) :: defines_var(INT____00126);
constraint bool2int(BOOL____00127, INT____00128) :: defines_var(INT____00128);
constraint bool2int(BOOL____00129, INT____00130) :: defines_var(INT____00130);
constraint bool2int(BOOL____00131, INT____00132) :: defines_var(INT____00132);
constraint bool2int(BOOL____00133, INT____00134) :: defines_var(INT____00134);
constraint bool2int(BOOL____00135, INT____00136) :: defines_var(INT____00136);
constraint int_eq(binary[1], t____00001[1]);
constraint int_eq(binary[2], t____00001[2]);
constraint int_eq(binary[3], t____00001[3]);
constraint int_eq(binary[4], t____00001[4]);
constraint int_eq(binary[5], t____00002[1]);
constraint int_eq(binary[6], t____00002[2]);
constraint int_eq(binary[7], t____00002[3]);
constraint int_eq(binary[8], t____00002[4]);
constraint int_eq(binary[9], t____00003[1]);
constraint int_eq(binary[10], t____00003[2]);
constraint int_eq(binary[11], t____00003[3]);
constraint int_eq(binary[12], t____00003[4]);
constraint int_eq(binary[13], t____00004[1]);
constraint int_eq(binary[14], t____00004[2]);
constraint int_eq(binary[15], t____00004[3]);
constraint int_eq(binary[16], t____00004[4]);
constraint int_eq(binary[17], t____00005[1]);
constraint int_eq(binary[18], t____00005[2]);
constraint int_eq(binary[19], t____00005[3]);
constraint int_eq(binary[20], t____00005[4]);
constraint int_eq(binary[21], t____00006[1]);
constraint int_eq(binary[22], t____00006[2]);
constraint int_eq(binary[23], t____00006[3]);
constraint int_eq(binary[24], t____00006[4]);
constraint int_eq(binary[25], t____00007[1]);
constraint int_eq(binary[26], t____00007[2]);
constraint int_eq(binary[27], t____00007[3]);
constraint int_eq(binary[28], t____00007[4]);
constraint int_eq(binary[29], t____00008[1]);
constraint int_eq(binary[30], t____00008[2]);
constraint int_eq(binary[31], t____00008[3]);
constraint int_eq(binary[32], t____00008[4]);
constraint int_eq(binary[33], t____00009[1]);
constraint int_eq(binary[34], t____00009[2]);
constraint int_eq(binary[35], t____00009[3]);
constraint int_eq(binary[36], t____00009[4]);
constraint int_eq(binary[37], t____00010[1]);
constraint int_eq(binary[38], t____00010[2]);
constraint int_eq(binary[39], t____00010[3]);
constraint int_eq(binary[40], t____00010[4]);
constraint int_eq(binary[41], t____00011[1]);
constraint int_eq(binary[42], t____00011[2]);
constraint int_eq(binary[43], t____00011[3]);
constraint int_eq(binary[44], t____00011[4]);
constraint int_eq(binary[45], t____00012[1]);
constraint int_eq(binary[46], t____00012[2]);
constraint int_eq(binary[47], t____00012[3]);
constraint int_eq(binary[48], t____00012[4]);
constraint int_eq(binary[49], t____00013[1]);
constraint int_eq(binary[50], t____00013[2]);
constraint int_eq(binary[51], t____00013[3]);
constraint int_eq(binary[52], t____00013[4]);
constraint int_eq(binary[53], t____00014[1]);
constraint int_eq(binary[54], t____00014[2]);
constraint int_eq(binary[55], t____00014[3]);
constraint int_eq(binary[56], t____00014[4]);
constraint int_eq(binary[57], t____00015[1]);
constraint int_eq(binary[58], t____00015[2]);
constraint int_eq(binary[59], t____00015[3]);
constraint int_eq(binary[60], t____00015[4]);
constraint int_eq(binary[61], t____00016[1]);
constraint int_eq(binary[62], t____00016[2]);
constraint int_eq(binary[63], t____00016[3]);
constraint int_eq(binary[64], t____00016[4]);
constraint int_eq(x[1], 0);
constraint int_lin_eq([1, 1, 1, 1], [INT____00018, INT____00020, INT____00022, INT____00024], 1);
constraint int_lin_eq([1, 1, 1, 1], [INT____00026, INT____00028, INT____00030, INT____00032], 1);
constraint int_lin_eq([1, 1, 1, 1], [INT____00034, INT____00036, INT____00038, INT____00040], 1);
constraint int_lin_eq([1, 1, 1, 1], [INT____00042, INT____00044, INT____00046, INT____00048], 1);
constraint int_lin_eq([1, 1, 1, 1], [INT____00050, INT____00052, INT____00054, INT____00056], 1);
constraint int_lin_eq([1, 1, 1, 1], [INT____00058, INT____00060, INT____00062, INT____00064], 1);
constraint int_lin_eq([1, 1, 1, 1], [INT____00066, INT____00068, INT____00070, INT____00072], 1);
constraint int_lin_eq([1, 1, 1, 1], [INT____00074, INT____00076, INT____00078, INT____00080], 1);
constraint int_lin_eq([1, 1, 1, 1], [INT____00082, INT____00084, INT____00086, INT____00088], 1);
constraint int_lin_eq([1, 1, 1, 1], [INT____00090, INT____00092, INT____00094, INT____00096], 1);
constraint int_lin_eq([1, 1, 1, 1], [INT____00098, INT____00100, INT____00102, INT____00104], 1);
constraint int_lin_eq([1, 1, 1, 1], [INT____00106, INT____00108, INT____00110, INT____00112], 1);
constraint int_lin_eq([1, 1, 1, 1], [INT____00114, INT____00116, INT____00118, INT____00120], 1);
constraint int_lin_eq([1, 1, 1, 1], [INT____00122, INT____00124, INT____00126, INT____00128], 1);
constraint int_lin_eq([1, 1, 1, 1], [INT____00130, INT____00132, INT____00134, INT____00136], 1);
constraint int_lin_eq([1, 1, 1, 1], [binary[61], binary[62], binary[63], binary[64]], 1);
constraint int_lin_eq([-8, -4, -2, -1, 1], [t____00001[1], t____00001[2], t____00001[3], t____00001[4], x[1]], 0);
constraint int_lin_eq([-8, -4, -2, -1, 1], [t____00002[1], t____00002[2], t____00002[3], t____00002[4], x[2]], 0);
constraint int_lin_eq([-8, -4, -2, -1, 1], [t____00003[1], t____00003[2], t____00003[3], t____00003[4], x[3]], 0);
constraint int_lin_eq([-8, -4, -2, -1, 1], [t____00004[1], t____00004[2], t____00004[3], t____00004[4], x[4]], 0);
constraint int_lin_eq([-8, -4, -2, -1, 1], [t____00005[1], t____00005[2], t____00005[3], t____00005[4], x[5]], 0);
constraint int_lin_eq([-8, -4, -2, -1, 1], [t____00006[1], t____00006[2], t____00006[3], t____00006[4], x[6]], 0);
constraint int_lin_eq([-8, -4, -2, -1, 1], [t____00007[1], t____00007[2], t____00007[3], t____00007[4], x[7]], 0);
constraint int_lin_eq([-8, -4, -2, -1, 1], [t____00008[1], t____00008[2], t____00008[3], t____00008[4], x[8]], 0);
constraint int_lin_eq([-8, -4, -2, -1, 1], [t____00009[1], t____00009[2], t____00009[3], t____00009[4], x[9]], 0);
constraint int_lin_eq([-8, -4, -2, -1, 1], [t____00010[1], t____00010[2], t____00010[3], t____00010[4], x[10]], 0);
constraint int_lin_eq([-8, -4, -2, -1, 1], [t____00011[1], t____00011[2], t____00011[3], t____00011[4], x[11]], 0);
constraint int_lin_eq([-8, -4, -2, -1, 1], [t____00012[1], t____00012[2], t____00012[3], t____00012[4], x[12]], 0);
constraint int_lin_eq([-8, -4, -2, -1, 1], [t____00013[1], t____00013[2], t____00013[3], t____00013[4], x[13]], 0);
constraint int_lin_eq([-8, -4, -2, -1, 1], [t____00014[1], t____00014[2], t____00014[3], t____00014[4], x[14]], 0);
constraint int_lin_eq([-8, -4, -2, -1, 1], [t____00015[1], t____00015[2], t____00015[3], t____00015[4], x[15]], 0);
constraint int_lin_eq([-8, -4, -2, -1, 1], [t____00016[1], t____00016[2], t____00016[3], t____00016[4], x[16]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [binary[1], binary[2], binary[3], binary[4], num_bits[1]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [binary[5], binary[6], binary[7], binary[8], num_bits[2]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [binary[9], binary[10], binary[11], binary[12], num_bits[3]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [binary[13], binary[14], binary[15], binary[16], num_bits[4]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [binary[17], binary[18], binary[19], binary[20], num_bits[5]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [binary[21], binary[22], binary[23], binary[24], num_bits[6]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [binary[25], binary[26], binary[27], binary[28], num_bits[7]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [binary[29], binary[30], binary[31], binary[32], num_bits[8]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [binary[33], binary[34], binary[35], binary[36], num_bits[9]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [binary[37], binary[38], binary[39], binary[40], num_bits[10]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [binary[41], binary[42], binary[43], binary[44], num_bits[11]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [binary[45], binary[46], binary[47], binary[48], num_bits[12]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [binary[49], binary[50], binary[51], binary[52], num_bits[13]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [binary[53], binary[54], binary[55], binary[56], num_bits[14]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [binary[57], binary[58], binary[59], binary[60], num_bits[15]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [binary[61], binary[62], binary[63], binary[64], num_bits[16]], 0);
constraint int_ne_reif(binary[5], binary[1], BOOL____00017) :: defines_var(BOOL____00017);
constraint int_ne_reif(binary[6], binary[2], BOOL____00019) :: defines_var(BOOL____00019);
constraint int_ne_reif(binary[7], binary[3], BOOL____00021) :: defines_var(BOOL____00021);
constraint int_ne_reif(binary[8], binary[4], BOOL____00023) :: defines_var(BOOL____00023);
constraint int_ne_reif(binary[9], binary[5], BOOL____00025) :: defines_var(BOOL____00025);
constraint int_ne_reif(binary[10], binary[6], BOOL____00027) :: defines_var(BOOL____00027);
constraint int_ne_reif(binary[11], binary[7], BOOL____00029) :: defines_var(BOOL____00029);
constraint int_ne_reif(binary[12], binary[8], BOOL____00031) :: defines_var(BOOL____00031);
constraint int_ne_reif(binary[13], binary[9], BOOL____00033) :: defines_var(BOOL____00033);
constraint int_ne_reif(binary[14], binary[10], BOOL____00035) :: defines_var(BOOL____00035);
constraint int_ne_reif(binary[15], binary[11], BOOL____00037) :: defines_var(BOOL____00037);
constraint int_ne_reif(binary[16], binary[12], BOOL____00039) :: defines_var(BOOL____00039);
constraint int_ne_reif(binary[17], binary[13], BOOL____00041) :: defines_var(BOOL____00041);
constraint int_ne_reif(binary[18], binary[14], BOOL____00043) :: defines_var(BOOL____00043);
constraint int_ne_reif(binary[19], binary[15], BOOL____00045) :: defines_var(BOOL____00045);
constraint int_ne_reif(binary[20], binary[16], BOOL____00047) :: defines_var(BOOL____00047);
constraint int_ne_reif(binary[21], binary[17], BOOL____00049) :: defines_var(BOOL____00049);
constraint int_ne_reif(binary[22], binary[18], BOOL____00051) :: defines_var(BOOL____00051);
constraint int_ne_reif(binary[23], binary[19], BOOL____00053) :: defines_var(BOOL____00053);
constraint int_ne_reif(binary[24], binary[20], BOOL____00055) :: defines_var(BOOL____00055);
constraint int_ne_reif(binary[25], binary[21], BOOL____00057) :: defines_var(BOOL____00057);
constraint int_ne_reif(binary[26], binary[22], BOOL____00059) :: defines_var(BOOL____00059);
constraint int_ne_reif(binary[27], binary[23], BOOL____00061) :: defines_var(BOOL____00061);
constraint int_ne_reif(binary[28], binary[24], BOOL____00063) :: defines_var(BOOL____00063);
constraint int_ne_reif(binary[29], binary[25], BOOL____00065) :: defines_var(BOOL____00065);
constraint int_ne_reif(binary[30], binary[26], BOOL____00067) :: defines_var(BOOL____00067);
constraint int_ne_reif(binary[31], binary[27], BOOL____00069) :: defines_var(BOOL____00069);
constraint int_ne_reif(binary[32], binary[28], BOOL____00071) :: defines_var(BOOL____00071);
constraint int_ne_reif(binary[33], binary[29], BOOL____00073) :: defines_var(BOOL____00073);
constraint int_ne_reif(binary[34], binary[30], BOOL____00075) :: defines_var(BOOL____00075);
constraint int_ne_reif(binary[35], binary[31], BOOL____00077) :: defines_var(BOOL____00077);
constraint int_ne_reif(binary[36], binary[32], BOOL____00079) :: defines_var(BOOL____00079);
constraint int_ne_reif(binary[37], binary[33], BOOL____00081) :: defines_var(BOOL____00081);
constraint int_ne_reif(binary[38], binary[34], BOOL____00083) :: defines_var(BOOL____00083);
constraint int_ne_reif(binary[39], binary[35], BOOL____00085) :: defines_var(BOOL____00085);
constraint int_ne_reif(binary[40], binary[36], BOOL____00087) :: defines_var(BOOL____00087);
constraint int_ne_reif(binary[41], binary[37], BOOL____00089) :: defines_var(BOOL____00089);
constraint int_ne_reif(binary[42], binary[38], BOOL____00091) :: defines_var(BOOL____00091);
constraint int_ne_reif(binary[43], binary[39], BOOL____00093) :: defines_var(BOOL____00093);
constraint int_ne_reif(binary[44], binary[40], BOOL____00095) :: defines_var(BOOL____00095);
constraint int_ne_reif(binary[45], binary[41], BOOL____00097) :: defines_var(BOOL____00097);
constraint int_ne_reif(binary[46], binary[42], BOOL____00099) :: defines_var(BOOL____00099);
constraint int_ne_reif(binary[47], binary[43], BOOL____00101) :: defines_var(BOOL____00101);
constraint int_ne_reif(binary[48], binary[44], BOOL____00103) :: defines_var(BOOL____00103);
constraint int_ne_reif(binary[49], binary[45], BOOL____00105) :: defines_var(BOOL____00105);
constraint int_ne_reif(binary[50], binary[46], BOOL____00107) :: defines_var(BOOL____00107);
constraint int_ne_reif(binary[51], binary[47], BOOL____00109) :: defines_var(BOOL____00109);
constraint int_ne_reif(binary[52], binary[48], BOOL____00111) :: defines_var(BOOL____00111);
constraint int_ne_reif(binary[53], binary[49], BOOL____00113) :: defines_var(BOOL____00113);
constraint int_ne_reif(binary[54], binary[50], BOOL____00115) :: defines_var(BOOL____00115);
constraint int_ne_reif(binary[55], binary[51], BOOL____00117) :: defines_var(BOOL____00117);
constraint int_ne_reif(binary[56], binary[52], BOOL____00119) :: defines_var(BOOL____00119);
constraint int_ne_reif(binary[57], binary[53], BOOL____00121) :: defines_var(BOOL____00121);
constraint int_ne_reif(binary[58], binary[54], BOOL____00123) :: defines_var(BOOL____00123);
constraint int_ne_reif(binary[59], binary[55], BOOL____00125) :: defines_var(BOOL____00125);
constraint int_ne_reif(binary[60], binary[56], BOOL____00127) :: defines_var(BOOL____00127);
constraint int_ne_reif(binary[61], binary[57], BOOL____00129) :: defines_var(BOOL____00129);
constraint int_ne_reif(binary[62], binary[58], BOOL____00131) :: defines_var(BOOL____00131);
constraint int_ne_reif(binary[63], binary[59], BOOL____00133) :: defines_var(BOOL____00133);
constraint int_ne_reif(binary[64], binary[60], BOOL____00135) :: defines_var(BOOL____00135);
solve  :: int_search(x, first_fail, indomain_split, complete) satisfy;