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 0..9: INT____00069 :: is_defined_var :: var_is_introduced; var 1..10: INT____00070 :: is_defined_var :: var_is_introduced; var 0..999: INT____00071 :: is_defined_var :: var_is_introduced; var 1..10: i____00065; var 0..999: ord_num____00004; var 0..999: ord_num____00011; var 0..999: ord_num____00018; var 0..999: ord_num____00025; var 0..999: ord_num____00032; var 0..999: ord_num____00039; var 0..999: ord_num____00046; var 0..999: ord_num____00053; var 0..999: ord_num____00060; var 1..10: pos :: output_var = i____00065; var 0..999: rev_num____00005; var 0..999: rev_num____00012; var 0..999: rev_num____00019; var 0..999: rev_num____00026; var 0..999: rev_num____00033; var 0..999: rev_num____00040; var 0..999: rev_num____00047; var 0..999: rev_num____00054; var 0..999: rev_num____00061; array [1..3] of var 0..9: s_num____00001; array [1..3] of var 0..9: s_num____00008; array [1..3] of var 0..9: s_num____00015; array [1..3] of var 0..9: s_num____00022; array [1..3] of var 0..9: s_num____00029; array [1..3] of var 0..9: s_num____00036; array [1..3] of var 0..9: s_num____00043; array [1..3] of var 0..9: s_num____00050; array [1..3] of var 0..9: s_num____00057; array [1..3] of var 0..9: s_ordered____00002; array [1..3] of var 0..9: s_ordered____00009; array [1..3] of var 0..9: s_ordered____00016; array [1..3] of var 0..9: s_ordered____00023; array [1..3] of var 0..9: s_ordered____00030; array [1..3] of var 0..9: s_ordered____00037; array [1..3] of var 0..9: s_ordered____00044; array [1..3] of var 0..9: s_ordered____00051; array [1..3] of var 0..9: s_ordered____00058; array [1..3] of var 0..9: s_reverse____00003; array [1..3] of var 0..9: s_reverse____00010; array [1..3] of var 0..9: s_reverse____00017; array [1..3] of var 0..9: s_reverse____00024; array [1..3] of var 0..9: s_reverse____00031; array [1..3] of var 0..9: s_reverse____00038; array [1..3] of var 0..9: s_reverse____00045; array [1..3] of var 0..9: s_reverse____00052; array [1..3] of var 0..9: s_reverse____00059; array [1..10] of var 0..999: 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, 495); constraint bool_le(BOOL____00067, BOOL____00073); constraint int_eq(s_reverse____00003[1], s_ordered____00002[3]); constraint int_eq(s_reverse____00003[2], s_ordered____00002[2]); constraint int_eq(s_reverse____00003[3], s_ordered____00002[1]); constraint int_eq(s_reverse____00010[1], s_ordered____00009[3]); constraint int_eq(s_reverse____00010[2], s_ordered____00009[2]); constraint int_eq(s_reverse____00010[3], s_ordered____00009[1]); constraint int_eq(s_reverse____00017[1], s_ordered____00016[3]); constraint int_eq(s_reverse____00017[2], s_ordered____00016[2]); constraint int_eq(s_reverse____00017[3], s_ordered____00016[1]); constraint int_eq(s_reverse____00024[1], s_ordered____00023[3]); constraint int_eq(s_reverse____00024[2], s_ordered____00023[2]); constraint int_eq(s_reverse____00024[3], s_ordered____00023[1]); constraint int_eq(s_reverse____00031[1], s_ordered____00030[3]); constraint int_eq(s_reverse____00031[2], s_ordered____00030[2]); constraint int_eq(s_reverse____00031[3], s_ordered____00030[1]); constraint int_eq(s_reverse____00038[1], s_ordered____00037[3]); constraint int_eq(s_reverse____00038[2], s_ordered____00037[2]); constraint int_eq(s_reverse____00038[3], s_ordered____00037[1]); constraint int_eq(s_reverse____00045[1], s_ordered____00044[3]); constraint int_eq(s_reverse____00045[2], s_ordered____00044[2]); constraint int_eq(s_reverse____00045[3], s_ordered____00044[1]); constraint int_eq(s_reverse____00052[1], s_ordered____00051[3]); constraint int_eq(s_reverse____00052[2], s_ordered____00051[2]); constraint int_eq(s_reverse____00052[3], s_ordered____00051[1]); constraint int_eq(s_reverse____00059[1], s_ordered____00058[3]); constraint int_eq(s_reverse____00059[2], s_ordered____00058[2]); constraint int_eq(s_reverse____00059[3], s_ordered____00058[1]); constraint int_eq_reif(INT____00069, INT____00070, BOOL____00068); constraint int_eq_reif(x[1], 495, false); 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([-100, -10, -1, 1], [s_num____00001[1], s_num____00001[2], s_num____00001[3], x[1]], 0); constraint int_lin_eq([-100, -10, -1, 1], [s_num____00008[1], s_num____00008[2], s_num____00008[3], x[2]], 0); constraint int_lin_eq([-100, -10, -1, 1], [s_num____00015[1], s_num____00015[2], s_num____00015[3], x[3]], 0); constraint int_lin_eq([-100, -10, -1, 1], [s_num____00022[1], s_num____00022[2], s_num____00022[3], x[4]], 0); constraint int_lin_eq([-100, -10, -1, 1], [s_num____00029[1], s_num____00029[2], s_num____00029[3], x[5]], 0); constraint int_lin_eq([-100, -10, -1, 1], [s_num____00036[1], s_num____00036[2], s_num____00036[3], x[6]], 0); constraint int_lin_eq([-100, -10, -1, 1], [s_num____00043[1], s_num____00043[2], s_num____00043[3], x[7]], 0); constraint int_lin_eq([-100, -10, -1, 1], [s_num____00050[1], s_num____00050[2], s_num____00050[3], x[8]], 0); constraint int_lin_eq([-100, -10, -1, 1], [s_num____00057[1], s_num____00057[2], s_num____00057[3], x[9]], 0); constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00004, s_ordered____00002[1], s_ordered____00002[2], s_ordered____00002[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00011, s_ordered____00009[1], s_ordered____00009[2], s_ordered____00009[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00018, s_ordered____00016[1], s_ordered____00016[2], s_ordered____00016[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00025, s_ordered____00023[1], s_ordered____00023[2], s_ordered____00023[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00032, s_ordered____00030[1], s_ordered____00030[2], s_ordered____00030[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00039, s_ordered____00037[1], s_ordered____00037[2], s_ordered____00037[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00046, s_ordered____00044[1], s_ordered____00044[2], s_ordered____00044[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00053, s_ordered____00051[1], s_ordered____00051[2], s_ordered____00051[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00060, s_ordered____00058[1], s_ordered____00058[2], s_ordered____00058[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00005, s_reverse____00003[1], s_reverse____00003[2], s_reverse____00003[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00012, s_reverse____00010[1], s_reverse____00010[2], s_reverse____00010[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00019, s_reverse____00017[1], s_reverse____00017[2], s_reverse____00017[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00026, s_reverse____00024[1], s_reverse____00024[2], s_reverse____00024[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00033, s_reverse____00031[1], s_reverse____00031[2], s_reverse____00031[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00040, s_reverse____00038[1], s_reverse____00038[2], s_reverse____00038[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00047, s_reverse____00045[1], s_reverse____00045[2], s_reverse____00045[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00054, s_reverse____00052[1], s_reverse____00052[2], s_reverse____00052[3]], 0); constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00061, s_reverse____00059[1], s_reverse____00059[2], s_reverse____00059[3]], 0); constraint int_lin_le_reif([-1], [i____00065], -2, BOOL____00068) :: defines_var(BOOL____00068); constraint int_ne_reif(INT____00071, 495, BOOL____00072) :: defines_var(BOOL____00072); 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); constraint int_eq(x[1], 0); solve :: int_search(x, input_order, indomain_min, complete) satisfy;