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____00003 :: is_defined_var :: var_is_introduced; var bool: BOOL____00005 :: is_defined_var :: var_is_introduced; var bool: BOOL____00011 :: is_defined_var :: var_is_introduced; var bool: BOOL____00013 :: 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____00027 :: is_defined_var :: var_is_introduced; var bool: BOOL____00029 :: 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____00043 :: is_defined_var :: var_is_introduced; var bool: BOOL____00045 :: 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____00059 :: is_defined_var :: var_is_introduced; var bool: BOOL____00061 :: 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____00075 :: is_defined_var :: var_is_introduced; var bool: BOOL____00077 :: 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____00091 :: is_defined_var :: var_is_introduced; var bool: BOOL____00093 :: 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____00107 :: is_defined_var :: var_is_introduced; var bool: BOOL____00109 :: 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____00123 :: is_defined_var :: var_is_introduced; var bool: BOOL____00125 :: 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____00139 :: is_defined_var :: var_is_introduced; var bool: BOOL____00141 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00006 :: is_defined_var :: var_is_introduced; var 0..300: INT____00008 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00014 :: is_defined_var :: var_is_introduced; var 0..300: INT____00016 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00022 :: is_defined_var :: var_is_introduced; var 0..300: INT____00024 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00030 :: is_defined_var :: var_is_introduced; var 0..300: INT____00032 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00038 :: is_defined_var :: var_is_introduced; var 0..300: INT____00040 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00046 :: is_defined_var :: var_is_introduced; var 0..300: INT____00048 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00054 :: is_defined_var :: var_is_introduced; var 0..300: INT____00056 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00062 :: is_defined_var :: var_is_introduced; var 0..300: INT____00064 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00070 :: is_defined_var :: var_is_introduced; var 0..300: INT____00072 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00078 :: is_defined_var :: var_is_introduced; var 0..300: INT____00080 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00086 :: is_defined_var :: var_is_introduced; var 0..300: INT____00088 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00094 :: is_defined_var :: var_is_introduced; var 0..300: INT____00096 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00102 :: is_defined_var :: var_is_introduced; var 0..300: INT____00104 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00110 :: is_defined_var :: var_is_introduced; var 0..300: INT____00112 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00118 :: is_defined_var :: var_is_introduced; var 0..300: INT____00120 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00126 :: is_defined_var :: var_is_introduced; var 0..300: INT____00128 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00134 :: is_defined_var :: var_is_introduced; var 0..300: INT____00136 :: is_defined_var :: var_is_introduced; var 1..90000: INT____00142 :: is_defined_var :: var_is_introduced; var 0..300: INT____00144 :: is_defined_var :: var_is_introduced; array [1..18] of var 1..2: ops :: output_array([1..18]); array [1..18] of var int: s____00001; var 666..666: total :: output_var = 666; array [1..19] of var 1..300: x :: output_array([1..19]); constraint int_div(x[1], x[2], INT____00008) :: defines_var(INT____00008); constraint int_div(x[2], x[3], INT____00016) :: defines_var(INT____00016); constraint int_div(x[3], x[4], INT____00024) :: defines_var(INT____00024); constraint int_div(x[4], x[5], INT____00032) :: defines_var(INT____00032); constraint int_div(x[5], x[6], INT____00040) :: defines_var(INT____00040); constraint int_div(x[6], x[7], INT____00048) :: defines_var(INT____00048); constraint int_div(x[7], x[8], INT____00056) :: defines_var(INT____00056); constraint int_div(x[8], x[9], INT____00064) :: defines_var(INT____00064); constraint int_div(x[9], x[10], INT____00072) :: defines_var(INT____00072); constraint int_div(x[10], x[11], INT____00080) :: defines_var(INT____00080); constraint int_div(x[11], x[12], INT____00088) :: defines_var(INT____00088); constraint int_div(x[12], x[13], INT____00096) :: defines_var(INT____00096); constraint int_div(x[13], x[14], INT____00104) :: defines_var(INT____00104); constraint int_div(x[14], x[15], INT____00112) :: defines_var(INT____00112); constraint int_div(x[15], x[16], INT____00120) :: defines_var(INT____00120); constraint int_div(x[16], x[17], INT____00128) :: defines_var(INT____00128); constraint int_div(x[17], x[18], INT____00136) :: defines_var(INT____00136); constraint int_div(x[18], x[19], INT____00144) :: defines_var(INT____00144); constraint int_eq(x[1], 72); constraint int_eq(x[2], 229); constraint int_eq(x[3], 107); constraint int_eq(x[4], 97); constraint int_eq(x[5], 110); constraint int_eq(x[6], 32); constraint int_eq(x[7], 75); constraint int_eq(x[8], 106); constraint int_eq(x[9], 101); constraint int_eq(x[10], 108); constraint int_eq(x[11], 108); constraint int_eq(x[12], 101); constraint int_eq(x[13], 114); constraint int_eq(x[14], 115); constraint int_eq(x[15], 116); constraint int_eq(x[16], 114); constraint int_eq(x[17], 97); constraint int_eq(x[18], 110); constraint int_eq(x[19], 100); constraint int_eq_reif(ops[1], 1, BOOL____00003); constraint int_eq_reif(ops[1], 2, BOOL____00005); constraint int_eq_reif(ops[2], 1, BOOL____00011); constraint int_eq_reif(ops[2], 2, BOOL____00013); constraint int_eq_reif(ops[3], 1, BOOL____00019); constraint int_eq_reif(ops[3], 2, BOOL____00021); constraint int_eq_reif(ops[4], 1, BOOL____00027); constraint int_eq_reif(ops[4], 2, BOOL____00029); constraint int_eq_reif(ops[5], 1, BOOL____00035); constraint int_eq_reif(ops[5], 2, BOOL____00037); constraint int_eq_reif(ops[6], 1, BOOL____00043); constraint int_eq_reif(ops[6], 2, BOOL____00045); constraint int_eq_reif(ops[7], 1, BOOL____00051); constraint int_eq_reif(ops[7], 2, BOOL____00053); constraint int_eq_reif(ops[8], 1, BOOL____00059); constraint int_eq_reif(ops[8], 2, BOOL____00061); constraint int_eq_reif(ops[9], 1, BOOL____00067); constraint int_eq_reif(ops[9], 2, BOOL____00069); constraint int_eq_reif(ops[10], 1, BOOL____00075); constraint int_eq_reif(ops[10], 2, BOOL____00077); constraint int_eq_reif(ops[11], 1, BOOL____00083); constraint int_eq_reif(ops[11], 2, BOOL____00085); constraint int_eq_reif(ops[12], 1, BOOL____00091); constraint int_eq_reif(ops[12], 2, BOOL____00093); constraint int_eq_reif(ops[13], 1, BOOL____00099); constraint int_eq_reif(ops[13], 2, BOOL____00101); constraint int_eq_reif(ops[14], 1, BOOL____00107); constraint int_eq_reif(ops[14], 2, BOOL____00109); constraint int_eq_reif(ops[15], 1, BOOL____00115); constraint int_eq_reif(ops[15], 2, BOOL____00117); constraint int_eq_reif(ops[16], 1, BOOL____00123); constraint int_eq_reif(ops[16], 2, BOOL____00125); constraint int_eq_reif(ops[17], 1, BOOL____00131); constraint int_eq_reif(ops[17], 2, BOOL____00133); constraint int_eq_reif(ops[18], 1, BOOL____00139); constraint int_eq_reif(ops[18], 2, BOOL____00141); constraint int_eq_reif(s____00001[1], INT____00006, false); constraint int_eq_reif(s____00001[1], INT____00008, false); constraint int_eq_reif(s____00001[2], INT____00014, false); constraint int_eq_reif(s____00001[2], INT____00016, false); constraint int_eq_reif(s____00001[3], INT____00022, false); constraint int_eq_reif(s____00001[3], INT____00024, false); constraint int_eq_reif(s____00001[4], INT____00030, false); constraint int_eq_reif(s____00001[4], INT____00032, false); constraint int_eq_reif(s____00001[5], INT____00038, false); constraint int_eq_reif(s____00001[5], INT____00040, false); constraint int_eq_reif(s____00001[6], INT____00046, false); constraint int_eq_reif(s____00001[6], INT____00048, false); constraint int_eq_reif(s____00001[7], INT____00054, false); constraint int_eq_reif(s____00001[7], INT____00056, false); constraint int_eq_reif(s____00001[8], INT____00062, false); constraint int_eq_reif(s____00001[8], INT____00064, false); constraint int_eq_reif(s____00001[9], INT____00070, false); constraint int_eq_reif(s____00001[9], INT____00072, false); constraint int_eq_reif(s____00001[10], INT____00078, false); constraint int_eq_reif(s____00001[10], INT____00080, false); constraint int_eq_reif(s____00001[11], INT____00086, false); constraint int_eq_reif(s____00001[11], INT____00088, false); constraint int_eq_reif(s____00001[12], INT____00094, false); constraint int_eq_reif(s____00001[12], INT____00096, false); constraint int_eq_reif(s____00001[13], INT____00102, false); constraint int_eq_reif(s____00001[13], INT____00104, false); constraint int_eq_reif(s____00001[14], INT____00110, false); constraint int_eq_reif(s____00001[14], INT____00112, false); constraint int_eq_reif(s____00001[15], INT____00118, false); constraint int_eq_reif(s____00001[15], INT____00120, false); constraint int_eq_reif(s____00001[16], INT____00126, false); constraint int_eq_reif(s____00001[16], INT____00128, false); constraint int_eq_reif(s____00001[17], INT____00134, false); constraint int_eq_reif(s____00001[17], INT____00136, false); constraint int_eq_reif(s____00001[18], INT____00142, false); constraint int_eq_reif(s____00001[18], INT____00144, false); constraint int_lin_eq([-1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [666, s____00001[1], s____00001[2], s____00001[3], s____00001[4], s____00001[5], s____00001[6], s____00001[7], s____00001[8], s____00001[9], s____00001[10], s____00001[11], s____00001[12], s____00001[13], s____00001[14], s____00001[15], s____00001[16], s____00001[17], s____00001[18]], 0); constraint int_lin_eq_reif([1, -1, -1], [s____00001[1], x[1], x[2]], 0, BOOL____00003) :: defines_var(BOOL____00003); constraint int_lin_eq_reif([1, -1, -1], [s____00001[2], x[2], x[3]], 0, BOOL____00011) :: defines_var(BOOL____00011); constraint int_lin_eq_reif([1, -1, -1], [s____00001[3], x[3], x[4]], 0, BOOL____00019) :: defines_var(BOOL____00019); constraint int_lin_eq_reif([1, -1, -1], [s____00001[4], x[4], x[5]], 0, BOOL____00027) :: defines_var(BOOL____00027); constraint int_lin_eq_reif([1, -1, -1], [s____00001[5], x[5], x[6]], 0, BOOL____00035) :: defines_var(BOOL____00035); constraint int_lin_eq_reif([1, -1, -1], [s____00001[6], x[6], x[7]], 0, BOOL____00043) :: defines_var(BOOL____00043); constraint int_lin_eq_reif([1, -1, -1], [s____00001[7], x[7], x[8]], 0, BOOL____00051) :: defines_var(BOOL____00051); constraint int_lin_eq_reif([1, -1, -1], [s____00001[8], x[8], x[9]], 0, BOOL____00059) :: defines_var(BOOL____00059); constraint int_lin_eq_reif([1, -1, -1], [s____00001[9], x[9], x[10]], 0, BOOL____00067) :: defines_var(BOOL____00067); constraint int_lin_eq_reif([1, -1, -1], [s____00001[10], x[10], x[11]], 0, BOOL____00075) :: defines_var(BOOL____00075); constraint int_lin_eq_reif([1, -1, -1], [s____00001[11], x[11], x[12]], 0, BOOL____00083) :: defines_var(BOOL____00083); constraint int_lin_eq_reif([1, -1, -1], [s____00001[12], x[12], x[13]], 0, BOOL____00091) :: defines_var(BOOL____00091); constraint int_lin_eq_reif([1, -1, -1], [s____00001[13], x[13], x[14]], 0, BOOL____00099) :: defines_var(BOOL____00099); constraint int_lin_eq_reif([1, -1, -1], [s____00001[14], x[14], x[15]], 0, BOOL____00107) :: defines_var(BOOL____00107); constraint int_lin_eq_reif([1, -1, -1], [s____00001[15], x[15], x[16]], 0, BOOL____00115) :: defines_var(BOOL____00115); constraint int_lin_eq_reif([1, -1, -1], [s____00001[16], x[16], x[17]], 0, BOOL____00123) :: defines_var(BOOL____00123); constraint int_lin_eq_reif([1, -1, -1], [s____00001[17], x[17], x[18]], 0, BOOL____00131) :: defines_var(BOOL____00131); constraint int_lin_eq_reif([1, -1, -1], [s____00001[18], x[18], x[19]], 0, BOOL____00139) :: defines_var(BOOL____00139); constraint int_lin_eq_reif([1, -1, 1], [s____00001[1], x[1], x[2]], 0, BOOL____00005) :: defines_var(BOOL____00005); constraint int_lin_eq_reif([1, -1, 1], [s____00001[2], x[2], x[3]], 0, BOOL____00013) :: defines_var(BOOL____00013); constraint int_lin_eq_reif([1, -1, 1], [s____00001[3], x[3], x[4]], 0, BOOL____00021) :: defines_var(BOOL____00021); constraint int_lin_eq_reif([1, -1, 1], [s____00001[4], x[4], x[5]], 0, BOOL____00029) :: defines_var(BOOL____00029); constraint int_lin_eq_reif([1, -1, 1], [s____00001[5], x[5], x[6]], 0, BOOL____00037) :: defines_var(BOOL____00037); constraint int_lin_eq_reif([1, -1, 1], [s____00001[6], x[6], x[7]], 0, BOOL____00045) :: defines_var(BOOL____00045); constraint int_lin_eq_reif([1, -1, 1], [s____00001[7], x[7], x[8]], 0, BOOL____00053) :: defines_var(BOOL____00053); constraint int_lin_eq_reif([1, -1, 1], [s____00001[8], x[8], x[9]], 0, BOOL____00061) :: defines_var(BOOL____00061); constraint int_lin_eq_reif([1, -1, 1], [s____00001[9], x[9], x[10]], 0, BOOL____00069) :: defines_var(BOOL____00069); constraint int_lin_eq_reif([1, -1, 1], [s____00001[10], x[10], x[11]], 0, BOOL____00077) :: defines_var(BOOL____00077); constraint int_lin_eq_reif([1, -1, 1], [s____00001[11], x[11], x[12]], 0, BOOL____00085) :: defines_var(BOOL____00085); constraint int_lin_eq_reif([1, -1, 1], [s____00001[12], x[12], x[13]], 0, BOOL____00093) :: defines_var(BOOL____00093); constraint int_lin_eq_reif([1, -1, 1], [s____00001[13], x[13], x[14]], 0, BOOL____00101) :: defines_var(BOOL____00101); constraint int_lin_eq_reif([1, -1, 1], [s____00001[14], x[14], x[15]], 0, BOOL____00109) :: defines_var(BOOL____00109); constraint int_lin_eq_reif([1, -1, 1], [s____00001[15], x[15], x[16]], 0, BOOL____00117) :: defines_var(BOOL____00117); constraint int_lin_eq_reif([1, -1, 1], [s____00001[16], x[16], x[17]], 0, BOOL____00125) :: defines_var(BOOL____00125); constraint int_lin_eq_reif([1, -1, 1], [s____00001[17], x[17], x[18]], 0, BOOL____00133) :: defines_var(BOOL____00133); constraint int_lin_eq_reif([1, -1, 1], [s____00001[18], x[18], x[19]], 0, BOOL____00141) :: defines_var(BOOL____00141); constraint int_times(x[1], x[2], INT____00006) :: defines_var(INT____00006); constraint int_times(x[2], x[3], INT____00014) :: defines_var(INT____00014); constraint int_times(x[3], x[4], INT____00022) :: defines_var(INT____00022); constraint int_times(x[4], x[5], INT____00030) :: defines_var(INT____00030); constraint int_times(x[5], x[6], INT____00038) :: defines_var(INT____00038); constraint int_times(x[6], x[7], INT____00046) :: defines_var(INT____00046); constraint int_times(x[7], x[8], INT____00054) :: defines_var(INT____00054); constraint int_times(x[8], x[9], INT____00062) :: defines_var(INT____00062); constraint int_times(x[9], x[10], INT____00070) :: defines_var(INT____00070); constraint int_times(x[10], x[11], INT____00078) :: defines_var(INT____00078); constraint int_times(x[11], x[12], INT____00086) :: defines_var(INT____00086); constraint int_times(x[12], x[13], INT____00094) :: defines_var(INT____00094); constraint int_times(x[13], x[14], INT____00102) :: defines_var(INT____00102); constraint int_times(x[14], x[15], INT____00110) :: defines_var(INT____00110); constraint int_times(x[15], x[16], INT____00118) :: defines_var(INT____00118); constraint int_times(x[16], x[17], INT____00126) :: defines_var(INT____00126); constraint int_times(x[17], x[18], INT____00134) :: defines_var(INT____00134); constraint int_times(x[18], x[19], INT____00142) :: defines_var(INT____00142); solve satisfy;