kaprekars_constant_8.fzn

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 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 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);
array [1..9] of set of int: nums = [{}, 495..495, 6174..6174, {}, {549945, 631764}, {}, {63317664, 97508421}, {554999445, 864197532}, {6333176664, 9753086421, 9975084201}];
var bool: BOOL____00067 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00068 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00072 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00073 :: is_defined_var :: var_is_introduced;
var 63317664..97508421: INT____00066 :: is_defined_var :: var_is_introduced;
var 0..9: INT____00069 :: is_defined_var :: var_is_introduced;
var 1..10: INT____00070 :: is_defined_var :: var_is_introduced;
var 0..99999999: INT____00071 :: is_defined_var :: var_is_introduced;
var 1..10: i____00065;
var 0..99999999: ord_num____00004;
var 0..99999999: ord_num____00011;
var 0..99999999: ord_num____00018;
var 0..99999999: ord_num____00025;
var 0..99999999: ord_num____00032;
var 0..99999999: ord_num____00039;
var 0..99999999: ord_num____00046;
var 0..99999999: ord_num____00053;
var 0..99999999: ord_num____00060;
var 1..10: pos :: output_var = i____00065;
var 0..99999999: rev_num____00005;
var 0..99999999: rev_num____00012;
var 0..99999999: rev_num____00019;
var 0..99999999: rev_num____00026;
var 0..99999999: rev_num____00033;
var 0..99999999: rev_num____00040;
var 0..99999999: rev_num____00047;
var 0..99999999: rev_num____00054;
var 0..99999999: rev_num____00061;
array [1..8] of var 0..9: s_num____00001;
array [1..8] of var 0..9: s_num____00008;
array [1..8] of var 0..9: s_num____00015;
array [1..8] of var 0..9: s_num____00022;
array [1..8] of var 0..9: s_num____00029;
array [1..8] of var 0..9: s_num____00036;
array [1..8] of var 0..9: s_num____00043;
array [1..8] of var 0..9: s_num____00050;
array [1..8] of var 0..9: s_num____00057;
array [1..8] of var 0..9: s_ordered____00002;
array [1..8] of var 0..9: s_ordered____00009;
array [1..8] of var 0..9: s_ordered____00016;
array [1..8] of var 0..9: s_ordered____00023;
array [1..8] of var 0..9: s_ordered____00030;
array [1..8] of var 0..9: s_ordered____00037;
array [1..8] of var 0..9: s_ordered____00044;
array [1..8] of var 0..9: s_ordered____00051;
array [1..8] of var 0..9: s_ordered____00058;
array [1..8] of var 0..9: s_reverse____00003;
array [1..8] of var 0..9: s_reverse____00010;
array [1..8] of var 0..9: s_reverse____00017;
array [1..8] of var 0..9: s_reverse____00024;
array [1..8] of var 0..9: s_reverse____00031;
array [1..8] of var 0..9: s_reverse____00038;
array [1..8] of var 0..9: s_reverse____00045;
array [1..8] of var 0..9: s_reverse____00052;
array [1..8] of var 0..9: s_reverse____00059;
array [1..10] of var 0..99999999: x :: output_array([1..10]);
constraint array_bool_and([BOOL____00072, BOOL____00068, BOOL____00068], BOOL____00073) :: defines_var(BOOL____00073);
constraint array_var_int_element(INT____00070, x, INT____00071) :: defines_var(INT____00071);
constraint array_var_int_element(i____00065, x, INT____00066) :: defines_var(INT____00066);
constraint bool_le(BOOL____00067, BOOL____00073);
constraint int_eq(s_reverse____00003[1], s_ordered____00002[8]);
constraint int_eq(s_reverse____00003[2], s_ordered____00002[7]);
constraint int_eq(s_reverse____00003[3], s_ordered____00002[6]);
constraint int_eq(s_reverse____00003[4], s_ordered____00002[5]);
constraint int_eq(s_reverse____00003[5], s_ordered____00002[4]);
constraint int_eq(s_reverse____00003[6], s_ordered____00002[3]);
constraint int_eq(s_reverse____00003[7], s_ordered____00002[2]);
constraint int_eq(s_reverse____00003[8], s_ordered____00002[1]);
constraint int_eq(s_reverse____00010[1], s_ordered____00009[8]);
constraint int_eq(s_reverse____00010[2], s_ordered____00009[7]);
constraint int_eq(s_reverse____00010[3], s_ordered____00009[6]);
constraint int_eq(s_reverse____00010[4], s_ordered____00009[5]);
constraint int_eq(s_reverse____00010[5], s_ordered____00009[4]);
constraint int_eq(s_reverse____00010[6], s_ordered____00009[3]);
constraint int_eq(s_reverse____00010[7], s_ordered____00009[2]);
constraint int_eq(s_reverse____00010[8], s_ordered____00009[1]);
constraint int_eq(s_reverse____00017[1], s_ordered____00016[8]);
constraint int_eq(s_reverse____00017[2], s_ordered____00016[7]);
constraint int_eq(s_reverse____00017[3], s_ordered____00016[6]);
constraint int_eq(s_reverse____00017[4], s_ordered____00016[5]);
constraint int_eq(s_reverse____00017[5], s_ordered____00016[4]);
constraint int_eq(s_reverse____00017[6], s_ordered____00016[3]);
constraint int_eq(s_reverse____00017[7], s_ordered____00016[2]);
constraint int_eq(s_reverse____00017[8], s_ordered____00016[1]);
constraint int_eq(s_reverse____00024[1], s_ordered____00023[8]);
constraint int_eq(s_reverse____00024[2], s_ordered____00023[7]);
constraint int_eq(s_reverse____00024[3], s_ordered____00023[6]);
constraint int_eq(s_reverse____00024[4], s_ordered____00023[5]);
constraint int_eq(s_reverse____00024[5], s_ordered____00023[4]);
constraint int_eq(s_reverse____00024[6], s_ordered____00023[3]);
constraint int_eq(s_reverse____00024[7], s_ordered____00023[2]);
constraint int_eq(s_reverse____00024[8], s_ordered____00023[1]);
constraint int_eq(s_reverse____00031[1], s_ordered____00030[8]);
constraint int_eq(s_reverse____00031[2], s_ordered____00030[7]);
constraint int_eq(s_reverse____00031[3], s_ordered____00030[6]);
constraint int_eq(s_reverse____00031[4], s_ordered____00030[5]);
constraint int_eq(s_reverse____00031[5], s_ordered____00030[4]);
constraint int_eq(s_reverse____00031[6], s_ordered____00030[3]);
constraint int_eq(s_reverse____00031[7], s_ordered____00030[2]);
constraint int_eq(s_reverse____00031[8], s_ordered____00030[1]);
constraint int_eq(s_reverse____00038[1], s_ordered____00037[8]);
constraint int_eq(s_reverse____00038[2], s_ordered____00037[7]);
constraint int_eq(s_reverse____00038[3], s_ordered____00037[6]);
constraint int_eq(s_reverse____00038[4], s_ordered____00037[5]);
constraint int_eq(s_reverse____00038[5], s_ordered____00037[4]);
constraint int_eq(s_reverse____00038[6], s_ordered____00037[3]);
constraint int_eq(s_reverse____00038[7], s_ordered____00037[2]);
constraint int_eq(s_reverse____00038[8], s_ordered____00037[1]);
constraint int_eq(s_reverse____00045[1], s_ordered____00044[8]);
constraint int_eq(s_reverse____00045[2], s_ordered____00044[7]);
constraint int_eq(s_reverse____00045[3], s_ordered____00044[6]);
constraint int_eq(s_reverse____00045[4], s_ordered____00044[5]);
constraint int_eq(s_reverse____00045[5], s_ordered____00044[4]);
constraint int_eq(s_reverse____00045[6], s_ordered____00044[3]);
constraint int_eq(s_reverse____00045[7], s_ordered____00044[2]);
constraint int_eq(s_reverse____00045[8], s_ordered____00044[1]);
constraint int_eq(s_reverse____00052[1], s_ordered____00051[8]);
constraint int_eq(s_reverse____00052[2], s_ordered____00051[7]);
constraint int_eq(s_reverse____00052[3], s_ordered____00051[6]);
constraint int_eq(s_reverse____00052[4], s_ordered____00051[5]);
constraint int_eq(s_reverse____00052[5], s_ordered____00051[4]);
constraint int_eq(s_reverse____00052[6], s_ordered____00051[3]);
constraint int_eq(s_reverse____00052[7], s_ordered____00051[2]);
constraint int_eq(s_reverse____00052[8], s_ordered____00051[1]);
constraint int_eq(s_reverse____00059[1], s_ordered____00058[8]);
constraint int_eq(s_reverse____00059[2], s_ordered____00058[7]);
constraint int_eq(s_reverse____00059[3], s_ordered____00058[6]);
constraint int_eq(s_reverse____00059[4], s_ordered____00058[5]);
constraint int_eq(s_reverse____00059[5], s_ordered____00058[4]);
constraint int_eq(s_reverse____00059[6], s_ordered____00058[3]);
constraint int_eq(s_reverse____00059[7], s_ordered____00058[2]);
constraint int_eq(s_reverse____00059[8], s_ordered____00058[1]);
constraint int_eq_reif(INT____00069, INT____00070, BOOL____00068);
constraint int_le_reif(2, i____00065, BOOL____00067) :: defines_var(BOOL____00067);
constraint int_lin_eq([-1, 1], [INT____00069, i____00065], 1) :: defines_var(INT____00069) :: domain;
constraint int_lin_eq([1, -1, 1], [ord_num____00004, rev_num____00005, x[2]], 0);
constraint int_lin_eq([1, -1, 1], [ord_num____00011, rev_num____00012, x[3]], 0);
constraint int_lin_eq([1, -1, 1], [ord_num____00018, rev_num____00019, x[4]], 0);
constraint int_lin_eq([1, -1, 1], [ord_num____00025, rev_num____00026, x[5]], 0);
constraint int_lin_eq([1, -1, 1], [ord_num____00032, rev_num____00033, x[6]], 0);
constraint int_lin_eq([1, -1, 1], [ord_num____00039, rev_num____00040, x[7]], 0);
constraint int_lin_eq([1, -1, 1], [ord_num____00046, rev_num____00047, x[8]], 0);
constraint int_lin_eq([1, -1, 1], [ord_num____00053, rev_num____00054, x[9]], 0);
constraint int_lin_eq([1, -1, 1], [ord_num____00060, rev_num____00061, x[10]], 0);
constraint int_lin_eq([-10000000, -1000000, -100000, -10000, -1000, -100, -10, -1, 1], [s_num____00001[1], s_num____00001[2], s_num____00001[3], s_num____00001[4], s_num____00001[5], s_num____00001[6], s_num____00001[7], s_num____00001[8], x[1]], 0);
constraint int_lin_eq([-10000000, -1000000, -100000, -10000, -1000, -100, -10, -1, 1], [s_num____00008[1], s_num____00008[2], s_num____00008[3], s_num____00008[4], s_num____00008[5], s_num____00008[6], s_num____00008[7], s_num____00008[8], x[2]], 0);
constraint int_lin_eq([-10000000, -1000000, -100000, -10000, -1000, -100, -10, -1, 1], [s_num____00015[1], s_num____00015[2], s_num____00015[3], s_num____00015[4], s_num____00015[5], s_num____00015[6], s_num____00015[7], s_num____00015[8], x[3]], 0);
constraint int_lin_eq([-10000000, -1000000, -100000, -10000, -1000, -100, -10, -1, 1], [s_num____00022[1], s_num____00022[2], s_num____00022[3], s_num____00022[4], s_num____00022[5], s_num____00022[6], s_num____00022[7], s_num____00022[8], x[4]], 0);
constraint int_lin_eq([-10000000, -1000000, -100000, -10000, -1000, -100, -10, -1, 1], [s_num____00029[1], s_num____00029[2], s_num____00029[3], s_num____00029[4], s_num____00029[5], s_num____00029[6], s_num____00029[7], s_num____00029[8], x[5]], 0);
constraint int_lin_eq([-10000000, -1000000, -100000, -10000, -1000, -100, -10, -1, 1], [s_num____00036[1], s_num____00036[2], s_num____00036[3], s_num____00036[4], s_num____00036[5], s_num____00036[6], s_num____00036[7], s_num____00036[8], x[6]], 0);
constraint int_lin_eq([-10000000, -1000000, -100000, -10000, -1000, -100, -10, -1, 1], [s_num____00043[1], s_num____00043[2], s_num____00043[3], s_num____00043[4], s_num____00043[5], s_num____00043[6], s_num____00043[7], s_num____00043[8], x[7]], 0);
constraint int_lin_eq([-10000000, -1000000, -100000, -10000, -1000, -100, -10, -1, 1], [s_num____00050[1], s_num____00050[2], s_num____00050[3], s_num____00050[4], s_num____00050[5], s_num____00050[6], s_num____00050[7], s_num____00050[8], x[8]], 0);
constraint int_lin_eq([-10000000, -1000000, -100000, -10000, -1000, -100, -10, -1, 1], [s_num____00057[1], s_num____00057[2], s_num____00057[3], s_num____00057[4], s_num____00057[5], s_num____00057[6], s_num____00057[7], s_num____00057[8], x[9]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [ord_num____00004, s_ordered____00002[1], s_ordered____00002[2], s_ordered____00002[3], s_ordered____00002[4], s_ordered____00002[5], s_ordered____00002[6], s_ordered____00002[7], s_ordered____00002[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [ord_num____00011, s_ordered____00009[1], s_ordered____00009[2], s_ordered____00009[3], s_ordered____00009[4], s_ordered____00009[5], s_ordered____00009[6], s_ordered____00009[7], s_ordered____00009[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [ord_num____00018, s_ordered____00016[1], s_ordered____00016[2], s_ordered____00016[3], s_ordered____00016[4], s_ordered____00016[5], s_ordered____00016[6], s_ordered____00016[7], s_ordered____00016[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [ord_num____00025, s_ordered____00023[1], s_ordered____00023[2], s_ordered____00023[3], s_ordered____00023[4], s_ordered____00023[5], s_ordered____00023[6], s_ordered____00023[7], s_ordered____00023[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [ord_num____00032, s_ordered____00030[1], s_ordered____00030[2], s_ordered____00030[3], s_ordered____00030[4], s_ordered____00030[5], s_ordered____00030[6], s_ordered____00030[7], s_ordered____00030[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [ord_num____00039, s_ordered____00037[1], s_ordered____00037[2], s_ordered____00037[3], s_ordered____00037[4], s_ordered____00037[5], s_ordered____00037[6], s_ordered____00037[7], s_ordered____00037[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [ord_num____00046, s_ordered____00044[1], s_ordered____00044[2], s_ordered____00044[3], s_ordered____00044[4], s_ordered____00044[5], s_ordered____00044[6], s_ordered____00044[7], s_ordered____00044[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [ord_num____00053, s_ordered____00051[1], s_ordered____00051[2], s_ordered____00051[3], s_ordered____00051[4], s_ordered____00051[5], s_ordered____00051[6], s_ordered____00051[7], s_ordered____00051[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [ord_num____00060, s_ordered____00058[1], s_ordered____00058[2], s_ordered____00058[3], s_ordered____00058[4], s_ordered____00058[5], s_ordered____00058[6], s_ordered____00058[7], s_ordered____00058[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [rev_num____00005, s_reverse____00003[1], s_reverse____00003[2], s_reverse____00003[3], s_reverse____00003[4], s_reverse____00003[5], s_reverse____00003[6], s_reverse____00003[7], s_reverse____00003[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [rev_num____00012, s_reverse____00010[1], s_reverse____00010[2], s_reverse____00010[3], s_reverse____00010[4], s_reverse____00010[5], s_reverse____00010[6], s_reverse____00010[7], s_reverse____00010[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [rev_num____00019, s_reverse____00017[1], s_reverse____00017[2], s_reverse____00017[3], s_reverse____00017[4], s_reverse____00017[5], s_reverse____00017[6], s_reverse____00017[7], s_reverse____00017[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [rev_num____00026, s_reverse____00024[1], s_reverse____00024[2], s_reverse____00024[3], s_reverse____00024[4], s_reverse____00024[5], s_reverse____00024[6], s_reverse____00024[7], s_reverse____00024[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [rev_num____00033, s_reverse____00031[1], s_reverse____00031[2], s_reverse____00031[3], s_reverse____00031[4], s_reverse____00031[5], s_reverse____00031[6], s_reverse____00031[7], s_reverse____00031[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [rev_num____00040, s_reverse____00038[1], s_reverse____00038[2], s_reverse____00038[3], s_reverse____00038[4], s_reverse____00038[5], s_reverse____00038[6], s_reverse____00038[7], s_reverse____00038[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [rev_num____00047, s_reverse____00045[1], s_reverse____00045[2], s_reverse____00045[3], s_reverse____00045[4], s_reverse____00045[5], s_reverse____00045[6], s_reverse____00045[7], s_reverse____00045[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [rev_num____00054, s_reverse____00052[1], s_reverse____00052[2], s_reverse____00052[3], s_reverse____00052[4], s_reverse____00052[5], s_reverse____00052[6], s_reverse____00052[7], s_reverse____00052[8]], 0);
constraint int_lin_eq([-1, 10000000, 1000000, 100000, 10000, 1000, 100, 10, 1], [rev_num____00061, s_reverse____00059[1], s_reverse____00059[2], s_reverse____00059[3], s_reverse____00059[4], s_reverse____00059[5], s_reverse____00059[6], s_reverse____00059[7], s_reverse____00059[8]], 0);
constraint int_lin_le_reif([-1], [i____00065], -2, BOOL____00068) :: defines_var(BOOL____00068);
constraint int_ne_reif(INT____00071, INT____00066, BOOL____00072) :: defines_var(BOOL____00072);
constraint set_in(INT____00066, {63317664, 97508421});
constraint set_in_reif(x[1], {63317664, 97508421}, false);
constraint sort(s_num____00001, s_ordered____00002);
constraint sort(s_num____00008, s_ordered____00009);
constraint sort(s_num____00015, s_ordered____00016);
constraint sort(s_num____00022, s_ordered____00023);
constraint sort(s_num____00029, s_ordered____00030);
constraint sort(s_num____00036, s_ordered____00037);
constraint sort(s_num____00043, s_ordered____00044);
constraint sort(s_num____00050, s_ordered____00051);
constraint sort(s_num____00057, s_ordered____00058);
solve  :: int_search(x, input_order, indomain_min, complete) satisfy;