var bool: BOOL____00001 :: is_defined_var :: var_is_introduced; var bool: BOOL____00003 :: is_defined_var :: var_is_introduced; var bool: BOOL____00005 :: 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____00017 :: 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____00023 :: 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____00030 :: 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____00040 :: is_defined_var :: var_is_introduced; var bool: BOOL____00042 :: 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____00050 :: 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____00056 :: is_defined_var :: var_is_introduced; var bool: BOOL____00057 :: is_defined_var :: var_is_introduced; var bool: BOOL____00060 :: 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____00070 :: 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____00080 :: is_defined_var :: var_is_introduced; var bool: BOOL____00081 :: is_defined_var :: var_is_introduced; var bool: BOOL____00084 :: 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____00090 :: 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____00098 :: is_defined_var :: var_is_introduced; var bool: BOOL____00100 :: 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____00110 :: is_defined_var :: var_is_introduced; var bool: BOOL____00112 :: 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____00120 :: 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____00126 :: is_defined_var :: var_is_introduced; var bool: BOOL____00127 :: is_defined_var :: var_is_introduced; var bool: BOOL____00130 :: 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 bool: BOOL____00137 :: is_defined_var :: var_is_introduced; var bool: BOOL____00140 :: is_defined_var :: var_is_introduced; var bool: BOOL____00141 :: is_defined_var :: var_is_introduced; var bool: BOOL____00143 :: is_defined_var :: var_is_introduced; var bool: BOOL____00145 :: is_defined_var :: var_is_introduced; var bool: BOOL____00147 :: is_defined_var :: var_is_introduced; var bool: BOOL____00150 :: is_defined_var :: var_is_introduced; var bool: BOOL____00151 :: is_defined_var :: var_is_introduced; var bool: BOOL____00154 :: is_defined_var :: var_is_introduced; var bool: BOOL____00155 :: is_defined_var :: var_is_introduced; var bool: BOOL____00157 :: is_defined_var :: var_is_introduced; var bool: BOOL____00160 :: is_defined_var :: var_is_introduced; var bool: BOOL____00161 :: is_defined_var :: var_is_introduced; var bool: BOOL____00163 :: is_defined_var :: var_is_introduced; var bool: BOOL____00165 :: is_defined_var :: var_is_introduced; var bool: BOOL____00168 :: is_defined_var :: var_is_introduced; var bool: BOOL____00170 :: is_defined_var :: var_is_introduced; var bool: BOOL____00171 :: is_defined_var :: var_is_introduced; var bool: BOOL____00173 :: is_defined_var :: var_is_introduced; var bool: BOOL____00175 :: is_defined_var :: var_is_introduced; var bool: BOOL____00177 :: is_defined_var :: var_is_introduced; var bool: BOOL____00180 :: is_defined_var :: var_is_introduced; var bool: BOOL____00182 :: is_defined_var :: var_is_introduced; var bool: BOOL____00183 :: is_defined_var :: var_is_introduced; var bool: BOOL____00185 :: is_defined_var :: var_is_introduced; var bool: BOOL____00187 :: is_defined_var :: var_is_introduced; var bool: BOOL____00190 :: is_defined_var :: var_is_introduced; var bool: BOOL____00191 :: is_defined_var :: var_is_introduced; var bool: BOOL____00193 :: is_defined_var :: var_is_introduced; var bool: BOOL____00196 :: is_defined_var :: var_is_introduced; var bool: BOOL____00197 :: is_defined_var :: var_is_introduced; var bool: BOOL____00200 :: is_defined_var :: var_is_introduced; var 0..100: INT____00201 :: is_defined_var :: var_is_introduced; array [1..100] of var 0..1: drinking :: output_array([1..100]); array [1..100] of var int: last_8min; var 0..100: num_drinks :: output_var = INT____00201; constraint int_eq_reif(drinking[1], 1, false); constraint int_eq_reif(drinking[2], 1, false); constraint int_eq_reif(drinking[3], 1, false); constraint int_eq_reif(drinking[4], 1, false); constraint int_eq_reif(drinking[5], 1, BOOL____00010) :: defines_var(BOOL____00010); constraint int_eq_reif(drinking[6], 1, false); constraint int_eq_reif(drinking[7], 1, BOOL____00014) :: defines_var(BOOL____00014); constraint int_eq_reif(drinking[8], 1, false); constraint int_eq_reif(drinking[9], 1, false); constraint int_eq_reif(drinking[10], 1, BOOL____00020) :: defines_var(BOOL____00020); constraint int_eq_reif(drinking[11], 1, false); constraint int_eq_reif(drinking[12], 1, false); constraint int_eq_reif(drinking[13], 1, false); constraint int_eq_reif(drinking[14], 1, BOOL____00028) :: defines_var(BOOL____00028); constraint int_eq_reif(drinking[15], 1, BOOL____00030) :: defines_var(BOOL____00030); constraint int_eq_reif(drinking[16], 1, false); constraint int_eq_reif(drinking[17], 1, false); constraint int_eq_reif(drinking[18], 1, false); constraint int_eq_reif(drinking[19], 1, false); constraint int_eq_reif(drinking[20], 1, BOOL____00040) :: defines_var(BOOL____00040); constraint int_eq_reif(drinking[21], 1, BOOL____00042) :: defines_var(BOOL____00042); constraint int_eq_reif(drinking[22], 1, false); constraint int_eq_reif(drinking[23], 1, false); constraint int_eq_reif(drinking[24], 1, false); constraint int_eq_reif(drinking[25], 1, BOOL____00050) :: defines_var(BOOL____00050); constraint int_eq_reif(drinking[26], 1, false); constraint int_eq_reif(drinking[27], 1, false); constraint int_eq_reif(drinking[28], 1, BOOL____00056) :: defines_var(BOOL____00056); constraint int_eq_reif(drinking[29], 1, false); constraint int_eq_reif(drinking[30], 1, BOOL____00060) :: defines_var(BOOL____00060); constraint int_eq_reif(drinking[31], 1, false); constraint int_eq_reif(drinking[32], 1, false); constraint int_eq_reif(drinking[33], 1, false); constraint int_eq_reif(drinking[34], 1, false); constraint int_eq_reif(drinking[35], 1, BOOL____00070) :: defines_var(BOOL____00070); constraint int_eq_reif(drinking[36], 1, false); constraint int_eq_reif(drinking[37], 1, false); constraint int_eq_reif(drinking[38], 1, false); constraint int_eq_reif(drinking[39], 1, false); constraint int_eq_reif(drinking[40], 1, BOOL____00080) :: defines_var(BOOL____00080); constraint int_eq_reif(drinking[41], 1, false); constraint int_eq_reif(drinking[42], 1, BOOL____00084) :: defines_var(BOOL____00084); constraint int_eq_reif(drinking[43], 1, false); constraint int_eq_reif(drinking[44], 1, false); constraint int_eq_reif(drinking[45], 1, BOOL____00090) :: defines_var(BOOL____00090); constraint int_eq_reif(drinking[46], 1, false); constraint int_eq_reif(drinking[47], 1, false); constraint int_eq_reif(drinking[48], 1, false); constraint int_eq_reif(drinking[49], 1, BOOL____00098) :: defines_var(BOOL____00098); constraint int_eq_reif(drinking[50], 1, BOOL____00100) :: defines_var(BOOL____00100); constraint int_eq_reif(drinking[51], 1, false); constraint int_eq_reif(drinking[52], 1, false); constraint int_eq_reif(drinking[53], 1, false); constraint int_eq_reif(drinking[54], 1, false); constraint int_eq_reif(drinking[55], 1, BOOL____00110) :: defines_var(BOOL____00110); constraint int_eq_reif(drinking[56], 1, BOOL____00112) :: defines_var(BOOL____00112); constraint int_eq_reif(drinking[57], 1, false); constraint int_eq_reif(drinking[58], 1, false); constraint int_eq_reif(drinking[59], 1, false); constraint int_eq_reif(drinking[60], 1, BOOL____00120) :: defines_var(BOOL____00120); constraint int_eq_reif(drinking[61], 1, false); constraint int_eq_reif(drinking[62], 1, false); constraint int_eq_reif(drinking[63], 1, BOOL____00126) :: defines_var(BOOL____00126); constraint int_eq_reif(drinking[64], 1, false); constraint int_eq_reif(drinking[65], 1, BOOL____00130) :: defines_var(BOOL____00130); constraint int_eq_reif(drinking[66], 1, false); constraint int_eq_reif(drinking[67], 1, false); constraint int_eq_reif(drinking[68], 1, false); constraint int_eq_reif(drinking[69], 1, false); constraint int_eq_reif(drinking[70], 1, BOOL____00140) :: defines_var(BOOL____00140); constraint int_eq_reif(drinking[71], 1, false); constraint int_eq_reif(drinking[72], 1, false); constraint int_eq_reif(drinking[73], 1, false); constraint int_eq_reif(drinking[74], 1, false); constraint int_eq_reif(drinking[75], 1, BOOL____00150) :: defines_var(BOOL____00150); constraint int_eq_reif(drinking[76], 1, false); constraint int_eq_reif(drinking[77], 1, BOOL____00154) :: defines_var(BOOL____00154); constraint int_eq_reif(drinking[78], 1, false); constraint int_eq_reif(drinking[79], 1, false); constraint int_eq_reif(drinking[80], 1, BOOL____00160) :: defines_var(BOOL____00160); constraint int_eq_reif(drinking[81], 1, false); constraint int_eq_reif(drinking[82], 1, false); constraint int_eq_reif(drinking[83], 1, false); constraint int_eq_reif(drinking[84], 1, BOOL____00168) :: defines_var(BOOL____00168); constraint int_eq_reif(drinking[85], 1, BOOL____00170) :: defines_var(BOOL____00170); constraint int_eq_reif(drinking[86], 1, false); constraint int_eq_reif(drinking[87], 1, false); constraint int_eq_reif(drinking[88], 1, false); constraint int_eq_reif(drinking[89], 1, false); constraint int_eq_reif(drinking[90], 1, BOOL____00180) :: defines_var(BOOL____00180); constraint int_eq_reif(drinking[91], 1, BOOL____00182) :: defines_var(BOOL____00182); constraint int_eq_reif(drinking[92], 1, false); constraint int_eq_reif(drinking[93], 1, false); constraint int_eq_reif(drinking[94], 1, false); constraint int_eq_reif(drinking[95], 1, BOOL____00190) :: defines_var(BOOL____00190); constraint int_eq_reif(drinking[96], 1, false); constraint int_eq_reif(drinking[97], 1, false); constraint int_eq_reif(drinking[98], 1, BOOL____00196) :: defines_var(BOOL____00196); constraint int_eq_reif(drinking[99], 1, false); constraint int_eq_reif(drinking[100], 1, BOOL____00200) :: defines_var(BOOL____00200); constraint int_eq_reif(last_8min[1], 0, BOOL____00001) :: defines_var(BOOL____00001); constraint int_eq_reif(last_8min[2], 0, BOOL____00003) :: defines_var(BOOL____00003); constraint int_eq_reif(last_8min[3], 0, BOOL____00005) :: defines_var(BOOL____00005); constraint int_eq_reif(last_8min[4], 0, BOOL____00007) :: defines_var(BOOL____00007); constraint int_eq_reif(last_8min[5], 0, BOOL____00010); constraint int_eq_reif(last_8min[6], 0, BOOL____00011) :: defines_var(BOOL____00011); constraint int_eq_reif(last_8min[7], 0, BOOL____00014); constraint int_eq_reif(last_8min[8], 0, BOOL____00015) :: defines_var(BOOL____00015); constraint int_eq_reif(last_8min[9], 0, BOOL____00017) :: defines_var(BOOL____00017); constraint int_eq_reif(last_8min[10], 0, BOOL____00020); constraint int_eq_reif(last_8min[11], 0, BOOL____00021) :: defines_var(BOOL____00021); constraint int_eq_reif(last_8min[12], 0, BOOL____00023) :: defines_var(BOOL____00023); constraint int_eq_reif(last_8min[13], 0, BOOL____00025) :: defines_var(BOOL____00025); constraint int_eq_reif(last_8min[14], 0, BOOL____00028); constraint int_eq_reif(last_8min[15], 0, BOOL____00030); constraint int_eq_reif(last_8min[16], 0, BOOL____00031) :: defines_var(BOOL____00031); constraint int_eq_reif(last_8min[17], 0, BOOL____00033) :: defines_var(BOOL____00033); constraint int_eq_reif(last_8min[18], 0, BOOL____00035) :: defines_var(BOOL____00035); constraint int_eq_reif(last_8min[19], 0, BOOL____00037) :: defines_var(BOOL____00037); constraint int_eq_reif(last_8min[20], 0, BOOL____00040); constraint int_eq_reif(last_8min[21], 0, BOOL____00042); constraint int_eq_reif(last_8min[22], 0, BOOL____00043) :: defines_var(BOOL____00043); constraint int_eq_reif(last_8min[23], 0, BOOL____00045) :: defines_var(BOOL____00045); constraint int_eq_reif(last_8min[24], 0, BOOL____00047) :: defines_var(BOOL____00047); constraint int_eq_reif(last_8min[25], 0, BOOL____00050); constraint int_eq_reif(last_8min[26], 0, BOOL____00051) :: defines_var(BOOL____00051); constraint int_eq_reif(last_8min[27], 0, BOOL____00053) :: defines_var(BOOL____00053); constraint int_eq_reif(last_8min[28], 0, BOOL____00056); constraint int_eq_reif(last_8min[29], 0, BOOL____00057) :: defines_var(BOOL____00057); constraint int_eq_reif(last_8min[30], 0, BOOL____00060); constraint int_eq_reif(last_8min[31], 0, BOOL____00061) :: defines_var(BOOL____00061); constraint int_eq_reif(last_8min[32], 0, BOOL____00063) :: defines_var(BOOL____00063); constraint int_eq_reif(last_8min[33], 0, BOOL____00065) :: defines_var(BOOL____00065); constraint int_eq_reif(last_8min[34], 0, BOOL____00067) :: defines_var(BOOL____00067); constraint int_eq_reif(last_8min[35], 0, BOOL____00070); constraint int_eq_reif(last_8min[36], 0, BOOL____00071) :: defines_var(BOOL____00071); constraint int_eq_reif(last_8min[37], 0, BOOL____00073) :: defines_var(BOOL____00073); constraint int_eq_reif(last_8min[38], 0, BOOL____00075) :: defines_var(BOOL____00075); constraint int_eq_reif(last_8min[39], 0, BOOL____00077) :: defines_var(BOOL____00077); constraint int_eq_reif(last_8min[40], 0, BOOL____00080); constraint int_eq_reif(last_8min[41], 0, BOOL____00081) :: defines_var(BOOL____00081); constraint int_eq_reif(last_8min[42], 0, BOOL____00084); constraint int_eq_reif(last_8min[43], 0, BOOL____00085) :: defines_var(BOOL____00085); constraint int_eq_reif(last_8min[44], 0, BOOL____00087) :: defines_var(BOOL____00087); constraint int_eq_reif(last_8min[45], 0, BOOL____00090); constraint int_eq_reif(last_8min[46], 0, BOOL____00091) :: defines_var(BOOL____00091); constraint int_eq_reif(last_8min[47], 0, BOOL____00093) :: defines_var(BOOL____00093); constraint int_eq_reif(last_8min[48], 0, BOOL____00095) :: defines_var(BOOL____00095); constraint int_eq_reif(last_8min[49], 0, BOOL____00098); constraint int_eq_reif(last_8min[50], 0, BOOL____00100); constraint int_eq_reif(last_8min[51], 0, BOOL____00101) :: defines_var(BOOL____00101); constraint int_eq_reif(last_8min[52], 0, BOOL____00103) :: defines_var(BOOL____00103); constraint int_eq_reif(last_8min[53], 0, BOOL____00105) :: defines_var(BOOL____00105); constraint int_eq_reif(last_8min[54], 0, BOOL____00107) :: defines_var(BOOL____00107); constraint int_eq_reif(last_8min[55], 0, BOOL____00110); constraint int_eq_reif(last_8min[56], 0, BOOL____00112); constraint int_eq_reif(last_8min[57], 0, BOOL____00113) :: defines_var(BOOL____00113); constraint int_eq_reif(last_8min[58], 0, BOOL____00115) :: defines_var(BOOL____00115); constraint int_eq_reif(last_8min[59], 0, BOOL____00117) :: defines_var(BOOL____00117); constraint int_eq_reif(last_8min[60], 0, BOOL____00120); constraint int_eq_reif(last_8min[61], 0, BOOL____00121) :: defines_var(BOOL____00121); constraint int_eq_reif(last_8min[62], 0, BOOL____00123) :: defines_var(BOOL____00123); constraint int_eq_reif(last_8min[63], 0, BOOL____00126); constraint int_eq_reif(last_8min[64], 0, BOOL____00127) :: defines_var(BOOL____00127); constraint int_eq_reif(last_8min[65], 0, BOOL____00130); constraint int_eq_reif(last_8min[66], 0, BOOL____00131) :: defines_var(BOOL____00131); constraint int_eq_reif(last_8min[67], 0, BOOL____00133) :: defines_var(BOOL____00133); constraint int_eq_reif(last_8min[68], 0, BOOL____00135) :: defines_var(BOOL____00135); constraint int_eq_reif(last_8min[69], 0, BOOL____00137) :: defines_var(BOOL____00137); constraint int_eq_reif(last_8min[70], 0, BOOL____00140); constraint int_eq_reif(last_8min[71], 0, BOOL____00141) :: defines_var(BOOL____00141); constraint int_eq_reif(last_8min[72], 0, BOOL____00143) :: defines_var(BOOL____00143); constraint int_eq_reif(last_8min[73], 0, BOOL____00145) :: defines_var(BOOL____00145); constraint int_eq_reif(last_8min[74], 0, BOOL____00147) :: defines_var(BOOL____00147); constraint int_eq_reif(last_8min[75], 0, BOOL____00150); constraint int_eq_reif(last_8min[76], 0, BOOL____00151) :: defines_var(BOOL____00151); constraint int_eq_reif(last_8min[77], 0, BOOL____00154); constraint int_eq_reif(last_8min[78], 0, BOOL____00155) :: defines_var(BOOL____00155); constraint int_eq_reif(last_8min[79], 0, BOOL____00157) :: defines_var(BOOL____00157); constraint int_eq_reif(last_8min[80], 0, BOOL____00160); constraint int_eq_reif(last_8min[81], 0, BOOL____00161) :: defines_var(BOOL____00161); constraint int_eq_reif(last_8min[82], 0, BOOL____00163) :: defines_var(BOOL____00163); constraint int_eq_reif(last_8min[83], 0, BOOL____00165) :: defines_var(BOOL____00165); constraint int_eq_reif(last_8min[84], 0, BOOL____00168); constraint int_eq_reif(last_8min[85], 0, BOOL____00170); constraint int_eq_reif(last_8min[86], 0, BOOL____00171) :: defines_var(BOOL____00171); constraint int_eq_reif(last_8min[87], 0, BOOL____00173) :: defines_var(BOOL____00173); constraint int_eq_reif(last_8min[88], 0, BOOL____00175) :: defines_var(BOOL____00175); constraint int_eq_reif(last_8min[89], 0, BOOL____00177) :: defines_var(BOOL____00177); constraint int_eq_reif(last_8min[90], 0, BOOL____00180); constraint int_eq_reif(last_8min[91], 0, BOOL____00182); constraint int_eq_reif(last_8min[92], 0, BOOL____00183) :: defines_var(BOOL____00183); constraint int_eq_reif(last_8min[93], 0, BOOL____00185) :: defines_var(BOOL____00185); constraint int_eq_reif(last_8min[94], 0, BOOL____00187) :: defines_var(BOOL____00187); constraint int_eq_reif(last_8min[95], 0, BOOL____00190); constraint int_eq_reif(last_8min[96], 0, BOOL____00191) :: defines_var(BOOL____00191); constraint int_eq_reif(last_8min[97], 0, BOOL____00193) :: defines_var(BOOL____00193); constraint int_eq_reif(last_8min[98], 0, BOOL____00196); constraint int_eq_reif(last_8min[99], 0, BOOL____00197) :: defines_var(BOOL____00197); constraint int_eq_reif(last_8min[100], 0, BOOL____00200); constraint int_lin_eq([-1, 1], [drinking[1], last_8min[1]], 0); constraint int_lin_eq([-1, 1], [drinking[1], last_8min[2]], 0); constraint int_lin_eq([-1, -1, 1], [drinking[1], drinking[2], last_8min[3]], 0); constraint int_lin_eq([-1, -1, -1, 1], [drinking[1], drinking[2], drinking[3], last_8min[4]], 0); constraint int_lin_eq([-1, -1, -1, -1, 1], [drinking[1], drinking[2], drinking[3], drinking[4], last_8min[5]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, 1], [drinking[1], drinking[2], drinking[3], drinking[4], drinking[5], last_8min[6]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, 1], [drinking[1], drinking[2], drinking[3], drinking[4], drinking[5], drinking[6], last_8min[7]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, 1], [drinking[1], drinking[2], drinking[3], drinking[4], drinking[5], drinking[6], drinking[7], last_8min[8]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[1], drinking[2], drinking[3], drinking[4], drinking[5], drinking[6], drinking[7], drinking[8], last_8min[9]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[2], drinking[3], drinking[4], drinking[5], drinking[6], drinking[7], drinking[8], drinking[9], last_8min[10]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[3], drinking[4], drinking[5], drinking[6], drinking[7], drinking[8], drinking[9], drinking[10], last_8min[11]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[4], drinking[5], drinking[6], drinking[7], drinking[8], drinking[9], drinking[10], drinking[11], last_8min[12]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[5], drinking[6], drinking[7], drinking[8], drinking[9], drinking[10], drinking[11], drinking[12], last_8min[13]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[6], drinking[7], drinking[8], drinking[9], drinking[10], drinking[11], drinking[12], drinking[13], last_8min[14]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[7], drinking[8], drinking[9], drinking[10], drinking[11], drinking[12], drinking[13], drinking[14], last_8min[15]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[8], drinking[9], drinking[10], drinking[11], drinking[12], drinking[13], drinking[14], drinking[15], last_8min[16]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[9], drinking[10], drinking[11], drinking[12], drinking[13], drinking[14], drinking[15], drinking[16], last_8min[17]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[10], drinking[11], drinking[12], drinking[13], drinking[14], drinking[15], drinking[16], drinking[17], last_8min[18]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[11], drinking[12], drinking[13], drinking[14], drinking[15], drinking[16], drinking[17], drinking[18], last_8min[19]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[12], drinking[13], drinking[14], drinking[15], drinking[16], drinking[17], drinking[18], drinking[19], last_8min[20]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[13], drinking[14], drinking[15], drinking[16], drinking[17], drinking[18], drinking[19], drinking[20], last_8min[21]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[14], drinking[15], drinking[16], drinking[17], drinking[18], drinking[19], drinking[20], drinking[21], last_8min[22]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[15], drinking[16], drinking[17], drinking[18], drinking[19], drinking[20], drinking[21], drinking[22], last_8min[23]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[16], drinking[17], drinking[18], drinking[19], drinking[20], drinking[21], drinking[22], drinking[23], last_8min[24]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[17], drinking[18], drinking[19], drinking[20], drinking[21], drinking[22], drinking[23], drinking[24], last_8min[25]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[18], drinking[19], drinking[20], drinking[21], drinking[22], drinking[23], drinking[24], drinking[25], last_8min[26]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[19], drinking[20], drinking[21], drinking[22], drinking[23], drinking[24], drinking[25], drinking[26], last_8min[27]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[20], drinking[21], drinking[22], drinking[23], drinking[24], drinking[25], drinking[26], drinking[27], last_8min[28]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[21], drinking[22], drinking[23], drinking[24], drinking[25], drinking[26], drinking[27], drinking[28], last_8min[29]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[22], drinking[23], drinking[24], drinking[25], drinking[26], drinking[27], drinking[28], drinking[29], last_8min[30]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[23], drinking[24], drinking[25], drinking[26], drinking[27], drinking[28], drinking[29], drinking[30], last_8min[31]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[24], drinking[25], drinking[26], drinking[27], drinking[28], drinking[29], drinking[30], drinking[31], last_8min[32]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[25], drinking[26], drinking[27], drinking[28], drinking[29], drinking[30], drinking[31], drinking[32], last_8min[33]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[26], drinking[27], drinking[28], drinking[29], drinking[30], drinking[31], drinking[32], drinking[33], last_8min[34]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[27], drinking[28], drinking[29], drinking[30], drinking[31], drinking[32], drinking[33], drinking[34], last_8min[35]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[28], drinking[29], drinking[30], drinking[31], drinking[32], drinking[33], drinking[34], drinking[35], last_8min[36]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[29], drinking[30], drinking[31], drinking[32], drinking[33], drinking[34], drinking[35], drinking[36], last_8min[37]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[30], drinking[31], drinking[32], drinking[33], drinking[34], drinking[35], drinking[36], drinking[37], last_8min[38]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[31], drinking[32], drinking[33], drinking[34], drinking[35], drinking[36], drinking[37], drinking[38], last_8min[39]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[32], drinking[33], drinking[34], drinking[35], drinking[36], drinking[37], drinking[38], drinking[39], last_8min[40]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[33], drinking[34], drinking[35], drinking[36], drinking[37], drinking[38], drinking[39], drinking[40], last_8min[41]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[34], drinking[35], drinking[36], drinking[37], drinking[38], drinking[39], drinking[40], drinking[41], last_8min[42]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[35], drinking[36], drinking[37], drinking[38], drinking[39], drinking[40], drinking[41], drinking[42], last_8min[43]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[36], drinking[37], drinking[38], drinking[39], drinking[40], drinking[41], drinking[42], drinking[43], last_8min[44]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[37], drinking[38], drinking[39], drinking[40], drinking[41], drinking[42], drinking[43], drinking[44], last_8min[45]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[38], drinking[39], drinking[40], drinking[41], drinking[42], drinking[43], drinking[44], drinking[45], last_8min[46]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[39], drinking[40], drinking[41], drinking[42], drinking[43], drinking[44], drinking[45], drinking[46], last_8min[47]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[40], drinking[41], drinking[42], drinking[43], drinking[44], drinking[45], drinking[46], drinking[47], last_8min[48]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[41], drinking[42], drinking[43], drinking[44], drinking[45], drinking[46], drinking[47], drinking[48], last_8min[49]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[42], drinking[43], drinking[44], drinking[45], drinking[46], drinking[47], drinking[48], drinking[49], last_8min[50]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[43], drinking[44], drinking[45], drinking[46], drinking[47], drinking[48], drinking[49], drinking[50], last_8min[51]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[44], drinking[45], drinking[46], drinking[47], drinking[48], drinking[49], drinking[50], drinking[51], last_8min[52]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[45], drinking[46], drinking[47], drinking[48], drinking[49], drinking[50], drinking[51], drinking[52], last_8min[53]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[46], drinking[47], drinking[48], drinking[49], drinking[50], drinking[51], drinking[52], drinking[53], last_8min[54]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[47], drinking[48], drinking[49], drinking[50], drinking[51], drinking[52], drinking[53], drinking[54], last_8min[55]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[48], drinking[49], drinking[50], drinking[51], drinking[52], drinking[53], drinking[54], drinking[55], last_8min[56]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[49], drinking[50], drinking[51], drinking[52], drinking[53], drinking[54], drinking[55], drinking[56], last_8min[57]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[50], drinking[51], drinking[52], drinking[53], drinking[54], drinking[55], drinking[56], drinking[57], last_8min[58]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[51], drinking[52], drinking[53], drinking[54], drinking[55], drinking[56], drinking[57], drinking[58], last_8min[59]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[52], drinking[53], drinking[54], drinking[55], drinking[56], drinking[57], drinking[58], drinking[59], last_8min[60]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[53], drinking[54], drinking[55], drinking[56], drinking[57], drinking[58], drinking[59], drinking[60], last_8min[61]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[54], drinking[55], drinking[56], drinking[57], drinking[58], drinking[59], drinking[60], drinking[61], last_8min[62]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[55], drinking[56], drinking[57], drinking[58], drinking[59], drinking[60], drinking[61], drinking[62], last_8min[63]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[56], drinking[57], drinking[58], drinking[59], drinking[60], drinking[61], drinking[62], drinking[63], last_8min[64]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[57], drinking[58], drinking[59], drinking[60], drinking[61], drinking[62], drinking[63], drinking[64], last_8min[65]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[58], drinking[59], drinking[60], drinking[61], drinking[62], drinking[63], drinking[64], drinking[65], last_8min[66]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[59], drinking[60], drinking[61], drinking[62], drinking[63], drinking[64], drinking[65], drinking[66], last_8min[67]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[60], drinking[61], drinking[62], drinking[63], drinking[64], drinking[65], drinking[66], drinking[67], last_8min[68]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[61], drinking[62], drinking[63], drinking[64], drinking[65], drinking[66], drinking[67], drinking[68], last_8min[69]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[62], drinking[63], drinking[64], drinking[65], drinking[66], drinking[67], drinking[68], drinking[69], last_8min[70]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[63], drinking[64], drinking[65], drinking[66], drinking[67], drinking[68], drinking[69], drinking[70], last_8min[71]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[64], drinking[65], drinking[66], drinking[67], drinking[68], drinking[69], drinking[70], drinking[71], last_8min[72]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[65], drinking[66], drinking[67], drinking[68], drinking[69], drinking[70], drinking[71], drinking[72], last_8min[73]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[66], drinking[67], drinking[68], drinking[69], drinking[70], drinking[71], drinking[72], drinking[73], last_8min[74]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[67], drinking[68], drinking[69], drinking[70], drinking[71], drinking[72], drinking[73], drinking[74], last_8min[75]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[68], drinking[69], drinking[70], drinking[71], drinking[72], drinking[73], drinking[74], drinking[75], last_8min[76]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[69], drinking[70], drinking[71], drinking[72], drinking[73], drinking[74], drinking[75], drinking[76], last_8min[77]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[70], drinking[71], drinking[72], drinking[73], drinking[74], drinking[75], drinking[76], drinking[77], last_8min[78]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[71], drinking[72], drinking[73], drinking[74], drinking[75], drinking[76], drinking[77], drinking[78], last_8min[79]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[72], drinking[73], drinking[74], drinking[75], drinking[76], drinking[77], drinking[78], drinking[79], last_8min[80]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[73], drinking[74], drinking[75], drinking[76], drinking[77], drinking[78], drinking[79], drinking[80], last_8min[81]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[74], drinking[75], drinking[76], drinking[77], drinking[78], drinking[79], drinking[80], drinking[81], last_8min[82]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[75], drinking[76], drinking[77], drinking[78], drinking[79], drinking[80], drinking[81], drinking[82], last_8min[83]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[76], drinking[77], drinking[78], drinking[79], drinking[80], drinking[81], drinking[82], drinking[83], last_8min[84]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[77], drinking[78], drinking[79], drinking[80], drinking[81], drinking[82], drinking[83], drinking[84], last_8min[85]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[78], drinking[79], drinking[80], drinking[81], drinking[82], drinking[83], drinking[84], drinking[85], last_8min[86]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[79], drinking[80], drinking[81], drinking[82], drinking[83], drinking[84], drinking[85], drinking[86], last_8min[87]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[80], drinking[81], drinking[82], drinking[83], drinking[84], drinking[85], drinking[86], drinking[87], last_8min[88]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[81], drinking[82], drinking[83], drinking[84], drinking[85], drinking[86], drinking[87], drinking[88], last_8min[89]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[82], drinking[83], drinking[84], drinking[85], drinking[86], drinking[87], drinking[88], drinking[89], last_8min[90]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[83], drinking[84], drinking[85], drinking[86], drinking[87], drinking[88], drinking[89], drinking[90], last_8min[91]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[84], drinking[85], drinking[86], drinking[87], drinking[88], drinking[89], drinking[90], drinking[91], last_8min[92]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[85], drinking[86], drinking[87], drinking[88], drinking[89], drinking[90], drinking[91], drinking[92], last_8min[93]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[86], drinking[87], drinking[88], drinking[89], drinking[90], drinking[91], drinking[92], drinking[93], last_8min[94]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[87], drinking[88], drinking[89], drinking[90], drinking[91], drinking[92], drinking[93], drinking[94], last_8min[95]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[88], drinking[89], drinking[90], drinking[91], drinking[92], drinking[93], drinking[94], drinking[95], last_8min[96]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[89], drinking[90], drinking[91], drinking[92], drinking[93], drinking[94], drinking[95], drinking[96], last_8min[97]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[90], drinking[91], drinking[92], drinking[93], drinking[94], drinking[95], drinking[96], drinking[97], last_8min[98]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[91], drinking[92], drinking[93], drinking[94], drinking[95], drinking[96], drinking[97], drinking[98], last_8min[99]], 0); constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [drinking[92], drinking[93], drinking[94], drinking[95], drinking[96], drinking[97], drinking[98], drinking[99], last_8min[100]], 0); constraint int_lin_eq([-1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [INT____00201, drinking[1], drinking[2], drinking[3], drinking[4], drinking[5], drinking[6], drinking[7], drinking[8], drinking[9], drinking[10], drinking[11], drinking[12], drinking[13], drinking[14], drinking[15], drinking[16], drinking[17], drinking[18], drinking[19], drinking[20], drinking[21], drinking[22], drinking[23], drinking[24], drinking[25], drinking[26], drinking[27], drinking[28], drinking[29], drinking[30], drinking[31], drinking[32], drinking[33], drinking[34], drinking[35], drinking[36], drinking[37], drinking[38], drinking[39], drinking[40], drinking[41], drinking[42], drinking[43], drinking[44], drinking[45], drinking[46], drinking[47], drinking[48], drinking[49], drinking[50], drinking[51], drinking[52], drinking[53], drinking[54], drinking[55], drinking[56], drinking[57], drinking[58], drinking[59], drinking[60], drinking[61], drinking[62], drinking[63], drinking[64], drinking[65], drinking[66], drinking[67], drinking[68], drinking[69], drinking[70], drinking[71], drinking[72], drinking[73], drinking[74], drinking[75], drinking[76], drinking[77], drinking[78], drinking[79], drinking[80], drinking[81], drinking[82], drinking[83], drinking[84], drinking[85], drinking[86], drinking[87], drinking[88], drinking[89], drinking[90], drinking[91], drinking[92], drinking[93], drinking[94], drinking[95], drinking[96], drinking[97], drinking[98], drinking[99], drinking[100]], 0) :: defines_var(INT____00201); solve satisfy;