array [1..6] of int: sums1 = [2, 3, 4, 4, 0, 4];
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____00009 :: 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____00015 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00017 :: 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____00023 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00025 :: 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____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____00039 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00041 :: 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____00049 :: 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____00055 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00057 :: 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____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____00069 :: 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____00079 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00081 :: 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____00087 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00089 :: 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____00097 :: 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____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____00109 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00111 :: 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____00119 :: 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____00125 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00127 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00129 :: 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____00139 :: 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____00149 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00151 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00153 :: 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____00159 :: 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____00167 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00169 :: 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____00179 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00181 :: 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____00189 :: 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____00195 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00197 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00199 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00201 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00203 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00205 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00207 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00209 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00211 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00213 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00215 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00217 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00219 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00221 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00223 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00225 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00227 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00229 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00231 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00233 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00235 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00237 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00239 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00241 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00243 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00245 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00247 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00249 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00251 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00253 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00255 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00257 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00259 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00261 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00263 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00002 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00004 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00006 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00008 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00010 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00012 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00014 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00016 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00018 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00020 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00022 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00024 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00026 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00028 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00030 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00032 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00034 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00036 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00038 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00040 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00042 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00044 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00046 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00048 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00050 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00052 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00054 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00056 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00058 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00060 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00062 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00064 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00066 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00068 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00070 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00072 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00074 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00076 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00078 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00080 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00082 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00084 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00086 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00088 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00090 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00092 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00094 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00096 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00098 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00100 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00102 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00104 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00106 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00108 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00110 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00112 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00114 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00116 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00118 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00120 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00122 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00124 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00126 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00128 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00130 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00132 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00134 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00136 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00138 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00140 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00142 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00144 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00146 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00148 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00150 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00152 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00154 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00156 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00158 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00160 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00162 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00164 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00166 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00168 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00170 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00172 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00174 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00176 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00178 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00180 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00182 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00184 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00186 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00188 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00190 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00192 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00194 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00196 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00198 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00200 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00202 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00204 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00206 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00208 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00210 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00212 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00214 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00216 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00218 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00220 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00222 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00224 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00226 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00228 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00230 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00232 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00234 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00236 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00238 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00240 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00242 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00244 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00246 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00248 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00250 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00252 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00254 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00256 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00258 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00260 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00262 :: is_defined_var :: var_is_introduced;
var 0..1: INT____00264 :: is_defined_var :: var_is_introduced;
array [1..12] of var 0..1: disk1 :: output_array([1..12]);
array [1..144] of var 0..1: disk2 :: output_array([1..12, 1..12]);
array [1..12] of var 0..12: sums;
constraint bool2int(BOOL____00001, INT____00002) :: defines_var(INT____00002);
constraint bool2int(BOOL____00003, INT____00004) :: defines_var(INT____00004);
constraint bool2int(BOOL____00005, INT____00006) :: defines_var(INT____00006);
constraint bool2int(BOOL____00007, INT____00008) :: defines_var(INT____00008);
constraint bool2int(BOOL____00009, INT____00010) :: defines_var(INT____00010);
constraint bool2int(BOOL____00011, INT____00012) :: defines_var(INT____00012);
constraint bool2int(BOOL____00013, INT____00014) :: defines_var(INT____00014);
constraint bool2int(BOOL____00015, INT____00016) :: defines_var(INT____00016);
constraint bool2int(BOOL____00017, INT____00018) :: defines_var(INT____00018);
constraint bool2int(BOOL____00019, INT____00020) :: defines_var(INT____00020);
constraint bool2int(BOOL____00021, INT____00022) :: defines_var(INT____00022);
constraint bool2int(BOOL____00023, INT____00024) :: defines_var(INT____00024);
constraint bool2int(BOOL____00025, INT____00026) :: defines_var(INT____00026);
constraint bool2int(BOOL____00027, INT____00028) :: defines_var(INT____00028);
constraint bool2int(BOOL____00029, INT____00030) :: defines_var(INT____00030);
constraint bool2int(BOOL____00031, INT____00032) :: defines_var(INT____00032);
constraint bool2int(BOOL____00033, INT____00034) :: defines_var(INT____00034);
constraint bool2int(BOOL____00035, INT____00036) :: defines_var(INT____00036);
constraint bool2int(BOOL____00037, INT____00038) :: defines_var(INT____00038);
constraint bool2int(BOOL____00039, INT____00040) :: defines_var(INT____00040);
constraint bool2int(BOOL____00041, INT____00042) :: defines_var(INT____00042);
constraint bool2int(BOOL____00043, INT____00044) :: defines_var(INT____00044);
constraint bool2int(BOOL____00045, INT____00046) :: defines_var(INT____00046);
constraint bool2int(BOOL____00047, INT____00048) :: defines_var(INT____00048);
constraint bool2int(BOOL____00049, INT____00050) :: defines_var(INT____00050);
constraint bool2int(BOOL____00051, INT____00052) :: defines_var(INT____00052);
constraint bool2int(BOOL____00053, INT____00054) :: defines_var(INT____00054);
constraint bool2int(BOOL____00055, INT____00056) :: defines_var(INT____00056);
constraint bool2int(BOOL____00057, INT____00058) :: defines_var(INT____00058);
constraint bool2int(BOOL____00059, INT____00060) :: defines_var(INT____00060);
constraint bool2int(BOOL____00061, INT____00062) :: defines_var(INT____00062);
constraint bool2int(BOOL____00063, INT____00064) :: defines_var(INT____00064);
constraint bool2int(BOOL____00065, INT____00066) :: defines_var(INT____00066);
constraint bool2int(BOOL____00067, INT____00068) :: defines_var(INT____00068);
constraint bool2int(BOOL____00069, INT____00070) :: defines_var(INT____00070);
constraint bool2int(BOOL____00071, INT____00072) :: defines_var(INT____00072);
constraint bool2int(BOOL____00073, INT____00074) :: defines_var(INT____00074);
constraint bool2int(BOOL____00075, INT____00076) :: defines_var(INT____00076);
constraint bool2int(BOOL____00077, INT____00078) :: defines_var(INT____00078);
constraint bool2int(BOOL____00079, INT____00080) :: defines_var(INT____00080);
constraint bool2int(BOOL____00081, INT____00082) :: defines_var(INT____00082);
constraint bool2int(BOOL____00083, INT____00084) :: defines_var(INT____00084);
constraint bool2int(BOOL____00085, INT____00086) :: defines_var(INT____00086);
constraint bool2int(BOOL____00087, INT____00088) :: defines_var(INT____00088);
constraint bool2int(BOOL____00089, INT____00090) :: defines_var(INT____00090);
constraint bool2int(BOOL____00091, INT____00092) :: defines_var(INT____00092);
constraint bool2int(BOOL____00093, INT____00094) :: defines_var(INT____00094);
constraint bool2int(BOOL____00095, INT____00096) :: defines_var(INT____00096);
constraint bool2int(BOOL____00097, INT____00098) :: defines_var(INT____00098);
constraint bool2int(BOOL____00099, INT____00100) :: defines_var(INT____00100);
constraint bool2int(BOOL____00101, INT____00102) :: defines_var(INT____00102);
constraint bool2int(BOOL____00103, INT____00104) :: defines_var(INT____00104);
constraint bool2int(BOOL____00105, INT____00106) :: defines_var(INT____00106);
constraint bool2int(BOOL____00107, INT____00108) :: defines_var(INT____00108);
constraint bool2int(BOOL____00109, INT____00110) :: defines_var(INT____00110);
constraint bool2int(BOOL____00111, INT____00112) :: defines_var(INT____00112);
constraint bool2int(BOOL____00113, INT____00114) :: defines_var(INT____00114);
constraint bool2int(BOOL____00115, INT____00116) :: defines_var(INT____00116);
constraint bool2int(BOOL____00117, INT____00118) :: defines_var(INT____00118);
constraint bool2int(BOOL____00119, INT____00120) :: defines_var(INT____00120);
constraint bool2int(BOOL____00121, INT____00122) :: defines_var(INT____00122);
constraint bool2int(BOOL____00123, INT____00124) :: defines_var(INT____00124);
constraint bool2int(BOOL____00125, INT____00126) :: defines_var(INT____00126);
constraint bool2int(BOOL____00127, INT____00128) :: defines_var(INT____00128);
constraint bool2int(BOOL____00129, INT____00130) :: defines_var(INT____00130);
constraint bool2int(BOOL____00131, INT____00132) :: defines_var(INT____00132);
constraint bool2int(BOOL____00133, INT____00134) :: defines_var(INT____00134);
constraint bool2int(BOOL____00135, INT____00136) :: defines_var(INT____00136);
constraint bool2int(BOOL____00137, INT____00138) :: defines_var(INT____00138);
constraint bool2int(BOOL____00139, INT____00140) :: defines_var(INT____00140);
constraint bool2int(BOOL____00141, INT____00142) :: defines_var(INT____00142);
constraint bool2int(BOOL____00143, INT____00144) :: defines_var(INT____00144);
constraint bool2int(BOOL____00145, INT____00146) :: defines_var(INT____00146);
constraint bool2int(BOOL____00147, INT____00148) :: defines_var(INT____00148);
constraint bool2int(BOOL____00149, INT____00150) :: defines_var(INT____00150);
constraint bool2int(BOOL____00151, INT____00152) :: defines_var(INT____00152);
constraint bool2int(BOOL____00153, INT____00154) :: defines_var(INT____00154);
constraint bool2int(BOOL____00155, INT____00156) :: defines_var(INT____00156);
constraint bool2int(BOOL____00157, INT____00158) :: defines_var(INT____00158);
constraint bool2int(BOOL____00159, INT____00160) :: defines_var(INT____00160);
constraint bool2int(BOOL____00161, INT____00162) :: defines_var(INT____00162);
constraint bool2int(BOOL____00163, INT____00164) :: defines_var(INT____00164);
constraint bool2int(BOOL____00165, INT____00166) :: defines_var(INT____00166);
constraint bool2int(BOOL____00167, INT____00168) :: defines_var(INT____00168);
constraint bool2int(BOOL____00169, INT____00170) :: defines_var(INT____00170);
constraint bool2int(BOOL____00171, INT____00172) :: defines_var(INT____00172);
constraint bool2int(BOOL____00173, INT____00174) :: defines_var(INT____00174);
constraint bool2int(BOOL____00175, INT____00176) :: defines_var(INT____00176);
constraint bool2int(BOOL____00177, INT____00178) :: defines_var(INT____00178);
constraint bool2int(BOOL____00179, INT____00180) :: defines_var(INT____00180);
constraint bool2int(BOOL____00181, INT____00182) :: defines_var(INT____00182);
constraint bool2int(BOOL____00183, INT____00184) :: defines_var(INT____00184);
constraint bool2int(BOOL____00185, INT____00186) :: defines_var(INT____00186);
constraint bool2int(BOOL____00187, INT____00188) :: defines_var(INT____00188);
constraint bool2int(BOOL____00189, INT____00190) :: defines_var(INT____00190);
constraint bool2int(BOOL____00191, INT____00192) :: defines_var(INT____00192);
constraint bool2int(BOOL____00193, INT____00194) :: defines_var(INT____00194);
constraint bool2int(BOOL____00195, INT____00196) :: defines_var(INT____00196);
constraint bool2int(BOOL____00197, INT____00198) :: defines_var(INT____00198);
constraint bool2int(BOOL____00199, INT____00200) :: defines_var(INT____00200);
constraint bool2int(BOOL____00201, INT____00202) :: defines_var(INT____00202);
constraint bool2int(BOOL____00203, INT____00204) :: defines_var(INT____00204);
constraint bool2int(BOOL____00205, INT____00206) :: defines_var(INT____00206);
constraint bool2int(BOOL____00207, INT____00208) :: defines_var(INT____00208);
constraint bool2int(BOOL____00209, INT____00210) :: defines_var(INT____00210);
constraint bool2int(BOOL____00211, INT____00212) :: defines_var(INT____00212);
constraint bool2int(BOOL____00213, INT____00214) :: defines_var(INT____00214);
constraint bool2int(BOOL____00215, INT____00216) :: defines_var(INT____00216);
constraint bool2int(BOOL____00217, INT____00218) :: defines_var(INT____00218);
constraint bool2int(BOOL____00219, INT____00220) :: defines_var(INT____00220);
constraint bool2int(BOOL____00221, INT____00222) :: defines_var(INT____00222);
constraint bool2int(BOOL____00223, INT____00224) :: defines_var(INT____00224);
constraint bool2int(BOOL____00225, INT____00226) :: defines_var(INT____00226);
constraint bool2int(BOOL____00227, INT____00228) :: defines_var(INT____00228);
constraint bool2int(BOOL____00229, INT____00230) :: defines_var(INT____00230);
constraint bool2int(BOOL____00231, INT____00232) :: defines_var(INT____00232);
constraint bool2int(BOOL____00233, INT____00234) :: defines_var(INT____00234);
constraint bool2int(BOOL____00235, INT____00236) :: defines_var(INT____00236);
constraint bool2int(BOOL____00237, INT____00238) :: defines_var(INT____00238);
constraint bool2int(BOOL____00239, INT____00240) :: defines_var(INT____00240);
constraint bool2int(BOOL____00241, INT____00242) :: defines_var(INT____00242);
constraint bool2int(BOOL____00243, INT____00244) :: defines_var(INT____00244);
constraint bool2int(BOOL____00245, INT____00246) :: defines_var(INT____00246);
constraint bool2int(BOOL____00247, INT____00248) :: defines_var(INT____00248);
constraint bool2int(BOOL____00249, INT____00250) :: defines_var(INT____00250);
constraint bool2int(BOOL____00251, INT____00252) :: defines_var(INT____00252);
constraint bool2int(BOOL____00253, INT____00254) :: defines_var(INT____00254);
constraint bool2int(BOOL____00255, INT____00256) :: defines_var(INT____00256);
constraint bool2int(BOOL____00257, INT____00258) :: defines_var(INT____00258);
constraint bool2int(BOOL____00259, INT____00260) :: defines_var(INT____00260);
constraint bool2int(BOOL____00261, INT____00262) :: defines_var(INT____00262);
constraint bool2int(BOOL____00263, INT____00264) :: defines_var(INT____00264);
constraint int_eq(disk2[1], disk1[12]);
constraint int_eq(disk2[2], disk1[11]);
constraint int_eq(disk2[3], disk1[10]);
constraint int_eq(disk2[4], disk1[9]);
constraint int_eq(disk2[5], disk1[8]);
constraint int_eq(disk2[6], disk1[7]);
constraint int_eq(disk2[7], disk1[6]);
constraint int_eq(disk2[8], disk1[5]);
constraint int_eq(disk2[9], disk1[4]);
constraint int_eq(disk2[10], disk1[3]);
constraint int_eq(disk2[11], disk1[2]);
constraint int_eq(disk2[12], disk1[1]);
constraint int_eq(disk2[13], disk2[2]);
constraint int_eq(disk2[14], disk2[3]);
constraint int_eq(disk2[15], disk2[4]);
constraint int_eq(disk2[16], disk2[5]);
constraint int_eq(disk2[17], disk2[6]);
constraint int_eq(disk2[18], disk2[7]);
constraint int_eq(disk2[19], disk2[8]);
constraint int_eq(disk2[20], disk2[9]);
constraint int_eq(disk2[21], disk2[10]);
constraint int_eq(disk2[22], disk2[11]);
constraint int_eq(disk2[23], disk2[12]);
constraint int_eq(disk2[24], disk2[1]);
constraint int_eq(disk2[25], disk2[14]);
constraint int_eq(disk2[26], disk2[15]);
constraint int_eq(disk2[27], disk2[16]);
constraint int_eq(disk2[28], disk2[17]);
constraint int_eq(disk2[29], disk2[18]);
constraint int_eq(disk2[30], disk2[19]);
constraint int_eq(disk2[31], disk2[20]);
constraint int_eq(disk2[32], disk2[21]);
constraint int_eq(disk2[33], disk2[22]);
constraint int_eq(disk2[34], disk2[23]);
constraint int_eq(disk2[35], disk2[24]);
constraint int_eq(disk2[36], disk2[13]);
constraint int_eq(disk2[37], disk2[26]);
constraint int_eq(disk2[38], disk2[27]);
constraint int_eq(disk2[39], disk2[28]);
constraint int_eq(disk2[40], disk2[29]);
constraint int_eq(disk2[41], disk2[30]);
constraint int_eq(disk2[42], disk2[31]);
constraint int_eq(disk2[43], disk2[32]);
constraint int_eq(disk2[44], disk2[33]);
constraint int_eq(disk2[45], disk2[34]);
constraint int_eq(disk2[46], disk2[35]);
constraint int_eq(disk2[47], disk2[36]);
constraint int_eq(disk2[48], disk2[25]);
constraint int_eq(disk2[49], disk2[38]);
constraint int_eq(disk2[50], disk2[39]);
constraint int_eq(disk2[51], disk2[40]);
constraint int_eq(disk2[52], disk2[41]);
constraint int_eq(disk2[53], disk2[42]);
constraint int_eq(disk2[54], disk2[43]);
constraint int_eq(disk2[55], disk2[44]);
constraint int_eq(disk2[56], disk2[45]);
constraint int_eq(disk2[57], disk2[46]);
constraint int_eq(disk2[58], disk2[47]);
constraint int_eq(disk2[59], disk2[48]);
constraint int_eq(disk2[60], disk2[37]);
constraint int_eq(disk2[61], disk2[50]);
constraint int_eq(disk2[62], disk2[51]);
constraint int_eq(disk2[63], disk2[52]);
constraint int_eq(disk2[64], disk2[53]);
constraint int_eq(disk2[65], disk2[54]);
constraint int_eq(disk2[66], disk2[55]);
constraint int_eq(disk2[67], disk2[56]);
constraint int_eq(disk2[68], disk2[57]);
constraint int_eq(disk2[69], disk2[58]);
constraint int_eq(disk2[70], disk2[59]);
constraint int_eq(disk2[71], disk2[60]);
constraint int_eq(disk2[72], disk2[49]);
constraint int_eq(disk2[73], disk2[62]);
constraint int_eq(disk2[74], disk2[63]);
constraint int_eq(disk2[75], disk2[64]);
constraint int_eq(disk2[76], disk2[65]);
constraint int_eq(disk2[77], disk2[66]);
constraint int_eq(disk2[78], disk2[67]);
constraint int_eq(disk2[79], disk2[68]);
constraint int_eq(disk2[80], disk2[69]);
constraint int_eq(disk2[81], disk2[70]);
constraint int_eq(disk2[82], disk2[71]);
constraint int_eq(disk2[83], disk2[72]);
constraint int_eq(disk2[84], disk2[61]);
constraint int_eq(disk2[85], disk2[74]);
constraint int_eq(disk2[86], disk2[75]);
constraint int_eq(disk2[87], disk2[76]);
constraint int_eq(disk2[88], disk2[77]);
constraint int_eq(disk2[89], disk2[78]);
constraint int_eq(disk2[90], disk2[79]);
constraint int_eq(disk2[91], disk2[80]);
constraint int_eq(disk2[92], disk2[81]);
constraint int_eq(disk2[93], disk2[82]);
constraint int_eq(disk2[94], disk2[83]);
constraint int_eq(disk2[95], disk2[84]);
constraint int_eq(disk2[96], disk2[73]);
constraint int_eq(disk2[97], disk2[86]);
constraint int_eq(disk2[98], disk2[87]);
constraint int_eq(disk2[99], disk2[88]);
constraint int_eq(disk2[100], disk2[89]);
constraint int_eq(disk2[101], disk2[90]);
constraint int_eq(disk2[102], disk2[91]);
constraint int_eq(disk2[103], disk2[92]);
constraint int_eq(disk2[104], disk2[93]);
constraint int_eq(disk2[105], disk2[94]);
constraint int_eq(disk2[106], disk2[95]);
constraint int_eq(disk2[107], disk2[96]);
constraint int_eq(disk2[108], disk2[85]);
constraint int_eq(disk2[109], disk2[98]);
constraint int_eq(disk2[110], disk2[99]);
constraint int_eq(disk2[111], disk2[100]);
constraint int_eq(disk2[112], disk2[101]);
constraint int_eq(disk2[113], disk2[102]);
constraint int_eq(disk2[114], disk2[103]);
constraint int_eq(disk2[115], disk2[104]);
constraint int_eq(disk2[116], disk2[105]);
constraint int_eq(disk2[117], disk2[106]);
constraint int_eq(disk2[118], disk2[107]);
constraint int_eq(disk2[119], disk2[108]);
constraint int_eq(disk2[120], disk2[97]);
constraint int_eq(disk2[121], disk2[110]);
constraint int_eq(disk2[122], disk2[111]);
constraint int_eq(disk2[123], disk2[112]);
constraint int_eq(disk2[124], disk2[113]);
constraint int_eq(disk2[125], disk2[114]);
constraint int_eq(disk2[126], disk2[115]);
constraint int_eq(disk2[127], disk2[116]);
constraint int_eq(disk2[128], disk2[117]);
constraint int_eq(disk2[129], disk2[118]);
constraint int_eq(disk2[130], disk2[119]);
constraint int_eq(disk2[131], disk2[120]);
constraint int_eq(disk2[132], disk2[109]);
constraint int_eq(disk2[133], disk2[122]);
constraint int_eq(disk2[134], disk2[123]);
constraint int_eq(disk2[135], disk2[124]);
constraint int_eq(disk2[136], disk2[125]);
constraint int_eq(disk2[137], disk2[126]);
constraint int_eq(disk2[138], disk2[127]);
constraint int_eq(disk2[139], disk2[128]);
constraint int_eq(disk2[140], disk2[129]);
constraint int_eq(disk2[141], disk2[130]);
constraint int_eq(disk2[142], disk2[131]);
constraint int_eq(disk2[143], disk2[132]);
constraint int_eq(disk2[144], disk2[121]);
constraint int_eq(sums[1], 2);
constraint int_eq(sums[2], 3);
constraint int_eq(sums[3], 4);
constraint int_eq(sums[4], 4);
constraint int_eq(sums[5], 0);
constraint int_eq(sums[6], 4);
constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 1], [INT____00002, INT____00004, INT____00006, INT____00008, INT____00010, INT____00012, INT____00014, INT____00016, INT____00018, INT____00020, INT____00022, INT____00024, sums[2]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 1], [INT____00026, INT____00028, INT____00030, INT____00032, INT____00034, INT____00036, INT____00038, INT____00040, INT____00042, INT____00044, INT____00046, INT____00048, sums[3]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 1], [INT____00050, INT____00052, INT____00054, INT____00056, INT____00058, INT____00060, INT____00062, INT____00064, INT____00066, INT____00068, INT____00070, INT____00072, sums[4]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 1], [INT____00074, INT____00076, INT____00078, INT____00080, INT____00082, INT____00084, INT____00086, INT____00088, INT____00090, INT____00092, INT____00094, INT____00096, sums[5]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 1], [INT____00098, INT____00100, INT____00102, INT____00104, INT____00106, INT____00108, INT____00110, INT____00112, INT____00114, INT____00116, INT____00118, INT____00120, sums[6]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 1], [INT____00122, INT____00124, INT____00126, INT____00128, INT____00130, INT____00132, INT____00134, INT____00136, INT____00138, INT____00140, INT____00142, INT____00144, sums[7]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 1], [INT____00146, INT____00148, INT____00150, INT____00152, INT____00154, INT____00156, INT____00158, INT____00160, INT____00162, INT____00164, INT____00166, INT____00168, sums[8]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 1], [INT____00170, INT____00172, INT____00174, INT____00176, INT____00178, INT____00180, INT____00182, INT____00184, INT____00186, INT____00188, INT____00190, INT____00192, sums[9]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 1], [INT____00194, INT____00196, INT____00198, INT____00200, INT____00202, INT____00204, INT____00206, INT____00208, INT____00210, INT____00212, INT____00214, INT____00216, sums[10]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 1], [INT____00218, INT____00220, INT____00222, INT____00224, INT____00226, INT____00228, INT____00230, INT____00232, INT____00234, INT____00236, INT____00238, INT____00240, sums[11]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 1], [INT____00242, INT____00244, INT____00246, INT____00248, INT____00250, INT____00252, INT____00254, INT____00256, INT____00258, INT____00260, INT____00262, INT____00264, sums[12]], 0);
constraint int_lin_eq_reif([1, 1], [disk1[1], disk2[13]], 2, BOOL____00001) :: defines_var(BOOL____00001);
constraint int_lin_eq_reif([1, 1], [disk1[1], disk2[25]], 2, BOOL____00025) :: defines_var(BOOL____00025);
constraint int_lin_eq_reif([1, 1], [disk1[1], disk2[37]], 2, BOOL____00049) :: defines_var(BOOL____00049);
constraint int_lin_eq_reif([1, 1], [disk1[1], disk2[49]], 2, BOOL____00073) :: defines_var(BOOL____00073);
constraint int_lin_eq_reif([1, 1], [disk1[1], disk2[61]], 2, BOOL____00097) :: defines_var(BOOL____00097);
constraint int_lin_eq_reif([1, 1], [disk1[1], disk2[73]], 2, BOOL____00121) :: defines_var(BOOL____00121);
constraint int_lin_eq_reif([1, 1], [disk1[1], disk2[85]], 2, BOOL____00145) :: defines_var(BOOL____00145);
constraint int_lin_eq_reif([1, 1], [disk1[1], disk2[97]], 2, BOOL____00169) :: defines_var(BOOL____00169);
constraint int_lin_eq_reif([1, 1], [disk1[1], disk2[109]], 2, BOOL____00193) :: defines_var(BOOL____00193);
constraint int_lin_eq_reif([1, 1], [disk1[1], disk2[121]], 2, BOOL____00217) :: defines_var(BOOL____00217);
constraint int_lin_eq_reif([1, 1], [disk1[1], disk2[133]], 2, BOOL____00241) :: defines_var(BOOL____00241);
constraint int_lin_eq_reif([1, 1], [disk1[2], disk2[14]], 2, BOOL____00003) :: defines_var(BOOL____00003);
constraint int_lin_eq_reif([1, 1], [disk1[2], disk2[26]], 2, BOOL____00027) :: defines_var(BOOL____00027);
constraint int_lin_eq_reif([1, 1], [disk1[2], disk2[38]], 2, BOOL____00051) :: defines_var(BOOL____00051);
constraint int_lin_eq_reif([1, 1], [disk1[2], disk2[50]], 2, BOOL____00075) :: defines_var(BOOL____00075);
constraint int_lin_eq_reif([1, 1], [disk1[2], disk2[62]], 2, BOOL____00099) :: defines_var(BOOL____00099);
constraint int_lin_eq_reif([1, 1], [disk1[2], disk2[74]], 2, BOOL____00123) :: defines_var(BOOL____00123);
constraint int_lin_eq_reif([1, 1], [disk1[2], disk2[86]], 2, BOOL____00147) :: defines_var(BOOL____00147);
constraint int_lin_eq_reif([1, 1], [disk1[2], disk2[98]], 2, BOOL____00171) :: defines_var(BOOL____00171);
constraint int_lin_eq_reif([1, 1], [disk1[2], disk2[110]], 2, BOOL____00195) :: defines_var(BOOL____00195);
constraint int_lin_eq_reif([1, 1], [disk1[2], disk2[122]], 2, BOOL____00219) :: defines_var(BOOL____00219);
constraint int_lin_eq_reif([1, 1], [disk1[2], disk2[134]], 2, BOOL____00243) :: defines_var(BOOL____00243);
constraint int_lin_eq_reif([1, 1], [disk1[3], disk2[15]], 2, BOOL____00005) :: defines_var(BOOL____00005);
constraint int_lin_eq_reif([1, 1], [disk1[3], disk2[27]], 2, BOOL____00029) :: defines_var(BOOL____00029);
constraint int_lin_eq_reif([1, 1], [disk1[3], disk2[39]], 2, BOOL____00053) :: defines_var(BOOL____00053);
constraint int_lin_eq_reif([1, 1], [disk1[3], disk2[51]], 2, BOOL____00077) :: defines_var(BOOL____00077);
constraint int_lin_eq_reif([1, 1], [disk1[3], disk2[63]], 2, BOOL____00101) :: defines_var(BOOL____00101);
constraint int_lin_eq_reif([1, 1], [disk1[3], disk2[75]], 2, BOOL____00125) :: defines_var(BOOL____00125);
constraint int_lin_eq_reif([1, 1], [disk1[3], disk2[87]], 2, BOOL____00149) :: defines_var(BOOL____00149);
constraint int_lin_eq_reif([1, 1], [disk1[3], disk2[99]], 2, BOOL____00173) :: defines_var(BOOL____00173);
constraint int_lin_eq_reif([1, 1], [disk1[3], disk2[111]], 2, BOOL____00197) :: defines_var(BOOL____00197);
constraint int_lin_eq_reif([1, 1], [disk1[3], disk2[123]], 2, BOOL____00221) :: defines_var(BOOL____00221);
constraint int_lin_eq_reif([1, 1], [disk1[3], disk2[135]], 2, BOOL____00245) :: defines_var(BOOL____00245);
constraint int_lin_eq_reif([1, 1], [disk1[4], disk2[16]], 2, BOOL____00007) :: defines_var(BOOL____00007);
constraint int_lin_eq_reif([1, 1], [disk1[4], disk2[28]], 2, BOOL____00031) :: defines_var(BOOL____00031);
constraint int_lin_eq_reif([1, 1], [disk1[4], disk2[40]], 2, BOOL____00055) :: defines_var(BOOL____00055);
constraint int_lin_eq_reif([1, 1], [disk1[4], disk2[52]], 2, BOOL____00079) :: defines_var(BOOL____00079);
constraint int_lin_eq_reif([1, 1], [disk1[4], disk2[64]], 2, BOOL____00103) :: defines_var(BOOL____00103);
constraint int_lin_eq_reif([1, 1], [disk1[4], disk2[76]], 2, BOOL____00127) :: defines_var(BOOL____00127);
constraint int_lin_eq_reif([1, 1], [disk1[4], disk2[88]], 2, BOOL____00151) :: defines_var(BOOL____00151);
constraint int_lin_eq_reif([1, 1], [disk1[4], disk2[100]], 2, BOOL____00175) :: defines_var(BOOL____00175);
constraint int_lin_eq_reif([1, 1], [disk1[4], disk2[112]], 2, BOOL____00199) :: defines_var(BOOL____00199);
constraint int_lin_eq_reif([1, 1], [disk1[4], disk2[124]], 2, BOOL____00223) :: defines_var(BOOL____00223);
constraint int_lin_eq_reif([1, 1], [disk1[4], disk2[136]], 2, BOOL____00247) :: defines_var(BOOL____00247);
constraint int_lin_eq_reif([1, 1], [disk1[5], disk2[17]], 2, BOOL____00009) :: defines_var(BOOL____00009);
constraint int_lin_eq_reif([1, 1], [disk1[5], disk2[29]], 2, BOOL____00033) :: defines_var(BOOL____00033);
constraint int_lin_eq_reif([1, 1], [disk1[5], disk2[41]], 2, BOOL____00057) :: defines_var(BOOL____00057);
constraint int_lin_eq_reif([1, 1], [disk1[5], disk2[53]], 2, BOOL____00081) :: defines_var(BOOL____00081);
constraint int_lin_eq_reif([1, 1], [disk1[5], disk2[65]], 2, BOOL____00105) :: defines_var(BOOL____00105);
constraint int_lin_eq_reif([1, 1], [disk1[5], disk2[77]], 2, BOOL____00129) :: defines_var(BOOL____00129);
constraint int_lin_eq_reif([1, 1], [disk1[5], disk2[89]], 2, BOOL____00153) :: defines_var(BOOL____00153);
constraint int_lin_eq_reif([1, 1], [disk1[5], disk2[101]], 2, BOOL____00177) :: defines_var(BOOL____00177);
constraint int_lin_eq_reif([1, 1], [disk1[5], disk2[113]], 2, BOOL____00201) :: defines_var(BOOL____00201);
constraint int_lin_eq_reif([1, 1], [disk1[5], disk2[125]], 2, BOOL____00225) :: defines_var(BOOL____00225);
constraint int_lin_eq_reif([1, 1], [disk1[5], disk2[137]], 2, BOOL____00249) :: defines_var(BOOL____00249);
constraint int_lin_eq_reif([1, 1], [disk1[6], disk2[18]], 2, BOOL____00011) :: defines_var(BOOL____00011);
constraint int_lin_eq_reif([1, 1], [disk1[6], disk2[30]], 2, BOOL____00035) :: defines_var(BOOL____00035);
constraint int_lin_eq_reif([1, 1], [disk1[6], disk2[42]], 2, BOOL____00059) :: defines_var(BOOL____00059);
constraint int_lin_eq_reif([1, 1], [disk1[6], disk2[54]], 2, BOOL____00083) :: defines_var(BOOL____00083);
constraint int_lin_eq_reif([1, 1], [disk1[6], disk2[66]], 2, BOOL____00107) :: defines_var(BOOL____00107);
constraint int_lin_eq_reif([1, 1], [disk1[6], disk2[78]], 2, BOOL____00131) :: defines_var(BOOL____00131);
constraint int_lin_eq_reif([1, 1], [disk1[6], disk2[90]], 2, BOOL____00155) :: defines_var(BOOL____00155);
constraint int_lin_eq_reif([1, 1], [disk1[6], disk2[102]], 2, BOOL____00179) :: defines_var(BOOL____00179);
constraint int_lin_eq_reif([1, 1], [disk1[6], disk2[114]], 2, BOOL____00203) :: defines_var(BOOL____00203);
constraint int_lin_eq_reif([1, 1], [disk1[6], disk2[126]], 2, BOOL____00227) :: defines_var(BOOL____00227);
constraint int_lin_eq_reif([1, 1], [disk1[6], disk2[138]], 2, BOOL____00251) :: defines_var(BOOL____00251);
constraint int_lin_eq_reif([1, 1], [disk1[7], disk2[19]], 2, BOOL____00013) :: defines_var(BOOL____00013);
constraint int_lin_eq_reif([1, 1], [disk1[7], disk2[31]], 2, BOOL____00037) :: defines_var(BOOL____00037);
constraint int_lin_eq_reif([1, 1], [disk1[7], disk2[43]], 2, BOOL____00061) :: defines_var(BOOL____00061);
constraint int_lin_eq_reif([1, 1], [disk1[7], disk2[55]], 2, BOOL____00085) :: defines_var(BOOL____00085);
constraint int_lin_eq_reif([1, 1], [disk1[7], disk2[67]], 2, BOOL____00109) :: defines_var(BOOL____00109);
constraint int_lin_eq_reif([1, 1], [disk1[7], disk2[79]], 2, BOOL____00133) :: defines_var(BOOL____00133);
constraint int_lin_eq_reif([1, 1], [disk1[7], disk2[91]], 2, BOOL____00157) :: defines_var(BOOL____00157);
constraint int_lin_eq_reif([1, 1], [disk1[7], disk2[103]], 2, BOOL____00181) :: defines_var(BOOL____00181);
constraint int_lin_eq_reif([1, 1], [disk1[7], disk2[115]], 2, BOOL____00205) :: defines_var(BOOL____00205);
constraint int_lin_eq_reif([1, 1], [disk1[7], disk2[127]], 2, BOOL____00229) :: defines_var(BOOL____00229);
constraint int_lin_eq_reif([1, 1], [disk1[7], disk2[139]], 2, BOOL____00253) :: defines_var(BOOL____00253);
constraint int_lin_eq_reif([1, 1], [disk1[8], disk2[20]], 2, BOOL____00015) :: defines_var(BOOL____00015);
constraint int_lin_eq_reif([1, 1], [disk1[8], disk2[32]], 2, BOOL____00039) :: defines_var(BOOL____00039);
constraint int_lin_eq_reif([1, 1], [disk1[8], disk2[44]], 2, BOOL____00063) :: defines_var(BOOL____00063);
constraint int_lin_eq_reif([1, 1], [disk1[8], disk2[56]], 2, BOOL____00087) :: defines_var(BOOL____00087);
constraint int_lin_eq_reif([1, 1], [disk1[8], disk2[68]], 2, BOOL____00111) :: defines_var(BOOL____00111);
constraint int_lin_eq_reif([1, 1], [disk1[8], disk2[80]], 2, BOOL____00135) :: defines_var(BOOL____00135);
constraint int_lin_eq_reif([1, 1], [disk1[8], disk2[92]], 2, BOOL____00159) :: defines_var(BOOL____00159);
constraint int_lin_eq_reif([1, 1], [disk1[8], disk2[104]], 2, BOOL____00183) :: defines_var(BOOL____00183);
constraint int_lin_eq_reif([1, 1], [disk1[8], disk2[116]], 2, BOOL____00207) :: defines_var(BOOL____00207);
constraint int_lin_eq_reif([1, 1], [disk1[8], disk2[128]], 2, BOOL____00231) :: defines_var(BOOL____00231);
constraint int_lin_eq_reif([1, 1], [disk1[8], disk2[140]], 2, BOOL____00255) :: defines_var(BOOL____00255);
constraint int_lin_eq_reif([1, 1], [disk1[9], disk2[21]], 2, BOOL____00017) :: defines_var(BOOL____00017);
constraint int_lin_eq_reif([1, 1], [disk1[9], disk2[33]], 2, BOOL____00041) :: defines_var(BOOL____00041);
constraint int_lin_eq_reif([1, 1], [disk1[9], disk2[45]], 2, BOOL____00065) :: defines_var(BOOL____00065);
constraint int_lin_eq_reif([1, 1], [disk1[9], disk2[57]], 2, BOOL____00089) :: defines_var(BOOL____00089);
constraint int_lin_eq_reif([1, 1], [disk1[9], disk2[69]], 2, BOOL____00113) :: defines_var(BOOL____00113);
constraint int_lin_eq_reif([1, 1], [disk1[9], disk2[81]], 2, BOOL____00137) :: defines_var(BOOL____00137);
constraint int_lin_eq_reif([1, 1], [disk1[9], disk2[93]], 2, BOOL____00161) :: defines_var(BOOL____00161);
constraint int_lin_eq_reif([1, 1], [disk1[9], disk2[105]], 2, BOOL____00185) :: defines_var(BOOL____00185);
constraint int_lin_eq_reif([1, 1], [disk1[9], disk2[117]], 2, BOOL____00209) :: defines_var(BOOL____00209);
constraint int_lin_eq_reif([1, 1], [disk1[9], disk2[129]], 2, BOOL____00233) :: defines_var(BOOL____00233);
constraint int_lin_eq_reif([1, 1], [disk1[9], disk2[141]], 2, BOOL____00257) :: defines_var(BOOL____00257);
constraint int_lin_eq_reif([1, 1], [disk1[10], disk2[22]], 2, BOOL____00019) :: defines_var(BOOL____00019);
constraint int_lin_eq_reif([1, 1], [disk1[10], disk2[34]], 2, BOOL____00043) :: defines_var(BOOL____00043);
constraint int_lin_eq_reif([1, 1], [disk1[10], disk2[46]], 2, BOOL____00067) :: defines_var(BOOL____00067);
constraint int_lin_eq_reif([1, 1], [disk1[10], disk2[58]], 2, BOOL____00091) :: defines_var(BOOL____00091);
constraint int_lin_eq_reif([1, 1], [disk1[10], disk2[70]], 2, BOOL____00115) :: defines_var(BOOL____00115);
constraint int_lin_eq_reif([1, 1], [disk1[10], disk2[82]], 2, BOOL____00139) :: defines_var(BOOL____00139);
constraint int_lin_eq_reif([1, 1], [disk1[10], disk2[94]], 2, BOOL____00163) :: defines_var(BOOL____00163);
constraint int_lin_eq_reif([1, 1], [disk1[10], disk2[106]], 2, BOOL____00187) :: defines_var(BOOL____00187);
constraint int_lin_eq_reif([1, 1], [disk1[10], disk2[118]], 2, BOOL____00211) :: defines_var(BOOL____00211);
constraint int_lin_eq_reif([1, 1], [disk1[10], disk2[130]], 2, BOOL____00235) :: defines_var(BOOL____00235);
constraint int_lin_eq_reif([1, 1], [disk1[10], disk2[142]], 2, BOOL____00259) :: defines_var(BOOL____00259);
constraint int_lin_eq_reif([1, 1], [disk1[11], disk2[23]], 2, BOOL____00021) :: defines_var(BOOL____00021);
constraint int_lin_eq_reif([1, 1], [disk1[11], disk2[35]], 2, BOOL____00045) :: defines_var(BOOL____00045);
constraint int_lin_eq_reif([1, 1], [disk1[11], disk2[47]], 2, BOOL____00069) :: defines_var(BOOL____00069);
constraint int_lin_eq_reif([1, 1], [disk1[11], disk2[59]], 2, BOOL____00093) :: defines_var(BOOL____00093);
constraint int_lin_eq_reif([1, 1], [disk1[11], disk2[71]], 2, BOOL____00117) :: defines_var(BOOL____00117);
constraint int_lin_eq_reif([1, 1], [disk1[11], disk2[83]], 2, BOOL____00141) :: defines_var(BOOL____00141);
constraint int_lin_eq_reif([1, 1], [disk1[11], disk2[95]], 2, BOOL____00165) :: defines_var(BOOL____00165);
constraint int_lin_eq_reif([1, 1], [disk1[11], disk2[107]], 2, BOOL____00189) :: defines_var(BOOL____00189);
constraint int_lin_eq_reif([1, 1], [disk1[11], disk2[119]], 2, BOOL____00213) :: defines_var(BOOL____00213);
constraint int_lin_eq_reif([1, 1], [disk1[11], disk2[131]], 2, BOOL____00237) :: defines_var(BOOL____00237);
constraint int_lin_eq_reif([1, 1], [disk1[11], disk2[143]], 2, BOOL____00261) :: defines_var(BOOL____00261);
constraint int_lin_eq_reif([1, 1], [disk1[12], disk2[24]], 2, BOOL____00023) :: defines_var(BOOL____00023);
constraint int_lin_eq_reif([1, 1], [disk1[12], disk2[36]], 2, BOOL____00047) :: defines_var(BOOL____00047);
constraint int_lin_eq_reif([1, 1], [disk1[12], disk2[48]], 2, BOOL____00071) :: defines_var(BOOL____00071);
constraint int_lin_eq_reif([1, 1], [disk1[12], disk2[60]], 2, BOOL____00095) :: defines_var(BOOL____00095);
constraint int_lin_eq_reif([1, 1], [disk1[12], disk2[72]], 2, BOOL____00119) :: defines_var(BOOL____00119);
constraint int_lin_eq_reif([1, 1], [disk1[12], disk2[84]], 2, BOOL____00143) :: defines_var(BOOL____00143);
constraint int_lin_eq_reif([1, 1], [disk1[12], disk2[96]], 2, BOOL____00167) :: defines_var(BOOL____00167);
constraint int_lin_eq_reif([1, 1], [disk1[12], disk2[108]], 2, BOOL____00191) :: defines_var(BOOL____00191);
constraint int_lin_eq_reif([1, 1], [disk1[12], disk2[120]], 2, BOOL____00215) :: defines_var(BOOL____00215);
constraint int_lin_eq_reif([1, 1], [disk1[12], disk2[132]], 2, BOOL____00239) :: defines_var(BOOL____00239);
constraint int_lin_eq_reif([1, 1], [disk1[12], disk2[144]], 2, BOOL____00263) :: defines_var(BOOL____00263);
solve  :: int_search([disk2[1], disk2[2], disk2[3], disk2[4], disk2[5], disk2[6], disk2[7], disk2[8], disk2[9], disk2[10], disk2[11], disk2[12], disk2[13], disk2[14], disk2[15], disk2[16], disk2[17], disk2[18], disk2[19], disk2[20], disk2[21], disk2[22], disk2[23], disk2[24], disk2[25], disk2[26], disk2[27], disk2[28], disk2[29], disk2[30], disk2[31], disk2[32], disk2[33], disk2[34], disk2[35], disk2[36], disk2[37], disk2[38], disk2[39], disk2[40], disk2[41], disk2[42], disk2[43], disk2[44], disk2[45], disk2[46], disk2[47], disk2[48], disk2[49], disk2[50], disk2[51], disk2[52], disk2[53], disk2[54], disk2[55], disk2[56], disk2[57], disk2[58], disk2[59], disk2[60], disk2[61], disk2[62], disk2[63], disk2[64], disk2[65], disk2[66], disk2[67], disk2[68], disk2[69], disk2[70], disk2[71], disk2[72], disk2[73], disk2[74], disk2[75], disk2[76], disk2[77], disk2[78], disk2[79], disk2[80], disk2[81], disk2[82], disk2[83], disk2[84], disk2[85], disk2[86], disk2[87], disk2[88], disk2[89], disk2[90], disk2[91], disk2[92], disk2[93], disk2[94], disk2[95], disk2[96], disk2[97], disk2[98], disk2[99], disk2[100], disk2[101], disk2[102], disk2[103], disk2[104], disk2[105], disk2[106], disk2[107], disk2[108], disk2[109], disk2[110], disk2[111], disk2[112], disk2[113], disk2[114], disk2[115], disk2[116], disk2[117], disk2[118], disk2[119], disk2[120], disk2[121], disk2[122], disk2[123], disk2[124], disk2[125], disk2[126], disk2[127], disk2[128], disk2[129], disk2[130], disk2[131], disk2[132], disk2[133], disk2[134], disk2[135], disk2[136], disk2[137], disk2[138], disk2[139], disk2[140], disk2[141], disk2[142], disk2[143], disk2[144], disk1[1], disk1[2], disk1[3], disk1[4], disk1[5], disk1[6], disk1[7], disk1[8], disk1[9], disk1[10], disk1[11], disk1[12], sums[1], sums[2], sums[3], sums[4], sums[5], sums[6], sums[7], sums[8], sums[9], sums[10], sums[11], sums[12]], occurrence, indomain_min, complete) satisfy;