array [1..4] of int: res = [1, 2, 5, 7];
var bool: BOOL____00002 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00003 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00006 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00007 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00010 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00011 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00014 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00015 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00018 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00020 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00021 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00024 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00025 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00028 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00029 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00032 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00034 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00036 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00037 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00040 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00041 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00044 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00046 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00048 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00050 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00051 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00054 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00056 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00058 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00060 :: is_defined_var :: var_is_introduced;
array [1..25] of var 0..3: matches;
array [1..5] of var 0..15: x :: output_array([1..5]);
constraint int_eq(matches[1], 0);
constraint int_eq(matches[7], 0);
constraint int_eq(matches[13], 0);
constraint int_eq(matches[19], 0);
constraint int_eq(matches[25], 0);
constraint int_eq(x[1], 1);
constraint int_eq(x[2], 2);
constraint int_eq(x[3], 5);
constraint int_eq(x[4], 7);
constraint int_eq_reif(matches[2], 0, BOOL____00018) :: defines_var(BOOL____00018);
constraint int_eq_reif(matches[2], 1, BOOL____00003) :: defines_var(BOOL____00003);
constraint int_eq_reif(matches[2], 3, BOOL____00002);
constraint int_eq_reif(matches[3], 0, BOOL____00032) :: defines_var(BOOL____00032);
constraint int_eq_reif(matches[3], 1, BOOL____00007) :: defines_var(BOOL____00007);
constraint int_eq_reif(matches[3], 3, BOOL____00006);
constraint int_eq_reif(matches[4], 0, BOOL____00044) :: defines_var(BOOL____00044);
constraint int_eq_reif(matches[4], 1, BOOL____00011) :: defines_var(BOOL____00011);
constraint int_eq_reif(matches[4], 3, BOOL____00010);
constraint int_eq_reif(matches[5], 0, BOOL____00054) :: defines_var(BOOL____00054);
constraint int_eq_reif(matches[5], 1, BOOL____00015) :: defines_var(BOOL____00015);
constraint int_eq_reif(matches[5], 3, BOOL____00014);
constraint int_eq_reif(matches[6], 0, BOOL____00002) :: defines_var(BOOL____00002);
constraint int_eq_reif(matches[6], 1, BOOL____00003);
constraint int_eq_reif(matches[6], 3, BOOL____00018);
constraint int_eq_reif(matches[8], 0, BOOL____00034) :: defines_var(BOOL____00034);
constraint int_eq_reif(matches[8], 1, BOOL____00021) :: defines_var(BOOL____00021);
constraint int_eq_reif(matches[8], 3, BOOL____00020);
constraint int_eq_reif(matches[9], 0, BOOL____00046) :: defines_var(BOOL____00046);
constraint int_eq_reif(matches[9], 1, BOOL____00025) :: defines_var(BOOL____00025);
constraint int_eq_reif(matches[9], 3, BOOL____00024);
constraint int_eq_reif(matches[10], 0, BOOL____00056) :: defines_var(BOOL____00056);
constraint int_eq_reif(matches[10], 1, BOOL____00029) :: defines_var(BOOL____00029);
constraint int_eq_reif(matches[10], 3, BOOL____00028);
constraint int_eq_reif(matches[11], 0, BOOL____00006) :: defines_var(BOOL____00006);
constraint int_eq_reif(matches[11], 1, BOOL____00007);
constraint int_eq_reif(matches[11], 3, BOOL____00032);
constraint int_eq_reif(matches[12], 0, BOOL____00020) :: defines_var(BOOL____00020);
constraint int_eq_reif(matches[12], 1, BOOL____00021);
constraint int_eq_reif(matches[12], 3, BOOL____00034);
constraint int_eq_reif(matches[14], 0, BOOL____00048) :: defines_var(BOOL____00048);
constraint int_eq_reif(matches[14], 1, BOOL____00037) :: defines_var(BOOL____00037);
constraint int_eq_reif(matches[14], 3, BOOL____00036);
constraint int_eq_reif(matches[15], 0, BOOL____00058) :: defines_var(BOOL____00058);
constraint int_eq_reif(matches[15], 1, BOOL____00041) :: defines_var(BOOL____00041);
constraint int_eq_reif(matches[15], 3, BOOL____00040);
constraint int_eq_reif(matches[16], 0, BOOL____00010) :: defines_var(BOOL____00010);
constraint int_eq_reif(matches[16], 1, BOOL____00011);
constraint int_eq_reif(matches[16], 3, BOOL____00044);
constraint int_eq_reif(matches[17], 0, BOOL____00024) :: defines_var(BOOL____00024);
constraint int_eq_reif(matches[17], 1, BOOL____00025);
constraint int_eq_reif(matches[17], 3, BOOL____00046);
constraint int_eq_reif(matches[18], 0, BOOL____00036) :: defines_var(BOOL____00036);
constraint int_eq_reif(matches[18], 1, BOOL____00037);
constraint int_eq_reif(matches[18], 3, BOOL____00048);
constraint int_eq_reif(matches[20], 0, BOOL____00060) :: defines_var(BOOL____00060);
constraint int_eq_reif(matches[20], 1, BOOL____00051) :: defines_var(BOOL____00051);
constraint int_eq_reif(matches[20], 3, BOOL____00050);
constraint int_eq_reif(matches[21], 0, BOOL____00014) :: defines_var(BOOL____00014);
constraint int_eq_reif(matches[21], 1, BOOL____00015);
constraint int_eq_reif(matches[21], 3, BOOL____00054);
constraint int_eq_reif(matches[22], 0, BOOL____00028) :: defines_var(BOOL____00028);
constraint int_eq_reif(matches[22], 1, BOOL____00029);
constraint int_eq_reif(matches[22], 3, BOOL____00056);
constraint int_eq_reif(matches[23], 0, BOOL____00040) :: defines_var(BOOL____00040);
constraint int_eq_reif(matches[23], 1, BOOL____00041);
constraint int_eq_reif(matches[23], 3, BOOL____00058);
constraint int_eq_reif(matches[24], 0, BOOL____00050) :: defines_var(BOOL____00050);
constraint int_eq_reif(matches[24], 1, BOOL____00051);
constraint int_eq_reif(matches[24], 3, BOOL____00060);
constraint int_lin_eq([-1, -1, -1, -1, -1, 1], [matches[1], matches[2], matches[3], matches[4], matches[5], x[1]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, 1], [matches[6], matches[7], matches[8], matches[9], matches[10], x[2]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, 1], [matches[11], matches[12], matches[13], matches[14], matches[15], x[3]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, 1], [matches[16], matches[17], matches[18], matches[19], matches[20], x[4]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, 1], [matches[21], matches[22], matches[23], matches[24], matches[25], x[5]], 0);
constraint set_in(matches[1], {0, 1, 3});
constraint set_in(matches[2], {0, 1, 3});
constraint set_in(matches[3], {0, 1, 3});
constraint set_in(matches[4], {0, 1, 3});
constraint set_in(matches[5], {0, 1, 3});
constraint set_in(matches[6], {0, 1, 3});
constraint set_in(matches[7], {0, 1, 3});
constraint set_in(matches[8], {0, 1, 3});
constraint set_in(matches[9], {0, 1, 3});
constraint set_in(matches[10], {0, 1, 3});
constraint set_in(matches[11], {0, 1, 3});
constraint set_in(matches[12], {0, 1, 3});
constraint set_in(matches[13], {0, 1, 3});
constraint set_in(matches[14], {0, 1, 3});
constraint set_in(matches[15], {0, 1, 3});
constraint set_in(matches[16], {0, 1, 3});
constraint set_in(matches[17], {0, 1, 3});
constraint set_in(matches[18], {0, 1, 3});
constraint set_in(matches[19], {0, 1, 3});
constraint set_in(matches[20], {0, 1, 3});
constraint set_in(matches[21], {0, 1, 3});
constraint set_in(matches[22], {0, 1, 3});
constraint set_in(matches[23], {0, 1, 3});
constraint set_in(matches[24], {0, 1, 3});
constraint set_in(matches[25], {0, 1, 3});
solve satisfy;