1var bool: BOOL____00002 :: is_defined_var :: var_is_introduced; 2var bool: BOOL____00003 :: is_defined_var :: var_is_introduced; 3var bool: BOOL____00005 :: is_defined_var :: var_is_introduced; 4var bool: BOOL____00006 :: is_defined_var :: var_is_introduced; 5var bool: BOOL____00007 :: is_defined_var :: var_is_introduced; 6var bool: BOOL____00008 :: is_defined_var :: var_is_introduced; 7var bool: BOOL____00010 :: is_defined_var :: var_is_introduced; 8var bool: BOOL____00011 :: is_defined_var :: var_is_introduced; 9var bool: BOOL____00012 :: is_defined_var :: var_is_introduced; 10var bool: BOOL____00013 :: is_defined_var :: var_is_introduced; 11var bool: BOOL____00014 :: is_defined_var :: var_is_introduced; 12var bool: BOOL____00015 :: is_defined_var :: var_is_introduced; 13var bool: BOOL____00017 :: is_defined_var :: var_is_introduced; 14var bool: BOOL____00018 :: is_defined_var :: var_is_introduced; 15var bool: BOOL____00019 :: is_defined_var :: var_is_introduced; 16var bool: BOOL____00020 :: is_defined_var :: var_is_introduced; 17var bool: BOOL____00021 :: is_defined_var :: var_is_introduced; 18var bool: BOOL____00022 :: is_defined_var :: var_is_introduced; 19var bool: BOOL____00024 :: is_defined_var :: var_is_introduced; 20var bool: BOOL____00025 :: is_defined_var :: var_is_introduced; 21var bool: BOOL____00028 :: is_defined_var :: var_is_introduced; 22var bool: BOOL____00029 :: is_defined_var :: var_is_introduced; 23var bool: BOOL____00031 :: is_defined_var :: var_is_introduced; 24var bool: BOOL____00032 :: is_defined_var :: var_is_introduced; 25var bool: BOOL____00033 :: is_defined_var :: var_is_introduced; 26var bool: BOOL____00034 :: is_defined_var :: var_is_introduced; 27var bool: BOOL____00036 :: is_defined_var :: var_is_introduced; 28var bool: BOOL____00037 :: is_defined_var :: var_is_introduced; 29var bool: BOOL____00038 :: is_defined_var :: var_is_introduced; 30var bool: BOOL____00039 :: is_defined_var :: var_is_introduced; 31var bool: BOOL____00040 :: is_defined_var :: var_is_introduced; 32var bool: BOOL____00041 :: is_defined_var :: var_is_introduced; 33var bool: BOOL____00043 :: is_defined_var :: var_is_introduced; 34var bool: BOOL____00044 :: is_defined_var :: var_is_introduced; 35var bool: BOOL____00045 :: is_defined_var :: var_is_introduced; 36var bool: BOOL____00046 :: is_defined_var :: var_is_introduced; 37var bool: BOOL____00047 :: is_defined_var :: var_is_introduced; 38var bool: BOOL____00048 :: is_defined_var :: var_is_introduced; 39var bool: BOOL____00050 :: is_defined_var :: var_is_introduced; 40var bool: BOOL____00051 :: is_defined_var :: var_is_introduced; 41var bool: BOOL____00055 :: is_defined_var :: var_is_introduced; 42var bool: BOOL____00056 :: is_defined_var :: var_is_introduced; 43var bool: BOOL____00058 :: is_defined_var :: var_is_introduced; 44var bool: BOOL____00059 :: is_defined_var :: var_is_introduced; 45var bool: BOOL____00061 :: is_defined_var :: var_is_introduced; 46var bool: BOOL____00062 :: is_defined_var :: var_is_introduced; 47var bool: BOOL____00066 :: is_defined_var :: var_is_introduced; 48var bool: BOOL____00067 :: is_defined_var :: var_is_introduced; 49var bool: BOOL____00069 :: is_defined_var :: var_is_introduced; 50var bool: BOOL____00070 :: is_defined_var :: var_is_introduced; 51var bool: BOOL____00071 :: is_defined_var :: var_is_introduced; 52var bool: BOOL____00072 :: is_defined_var :: var_is_introduced; 53var bool: BOOL____00074 :: is_defined_var :: var_is_introduced; 54var bool: BOOL____00075 :: is_defined_var :: var_is_introduced; 55var bool: BOOL____00076 :: is_defined_var :: var_is_introduced; 56var bool: BOOL____00077 :: is_defined_var :: var_is_introduced; 57var bool: BOOL____00078 :: is_defined_var :: var_is_introduced; 58var bool: BOOL____00079 :: is_defined_var :: var_is_introduced; 59var bool: BOOL____00081 :: is_defined_var :: var_is_introduced; 60var bool: BOOL____00082 :: is_defined_var :: var_is_introduced; 61var bool: BOOL____00083 :: is_defined_var :: var_is_introduced; 62var bool: BOOL____00084 :: is_defined_var :: var_is_introduced; 63var bool: BOOL____00085 :: is_defined_var :: var_is_introduced; 64var bool: BOOL____00086 :: is_defined_var :: var_is_introduced; 65var bool: BOOL____00088 :: is_defined_var :: var_is_introduced; 66var bool: BOOL____00089 :: is_defined_var :: var_is_introduced; 67var bool: BOOL____00094 :: is_defined_var :: var_is_introduced; 68var bool: BOOL____00095 :: is_defined_var :: var_is_introduced; 69var bool: BOOL____00097 :: is_defined_var :: var_is_introduced; 70var bool: BOOL____00098 :: is_defined_var :: var_is_introduced; 71var bool: BOOL____00104 :: is_defined_var :: var_is_introduced; 72var bool: BOOL____00105 :: is_defined_var :: var_is_introduced; 73var bool: BOOL____00107 :: is_defined_var :: var_is_introduced; 74var bool: BOOL____00108 :: is_defined_var :: var_is_introduced; 75var bool: BOOL____00112 :: is_defined_var :: var_is_introduced; 76var bool: BOOL____00113 :: is_defined_var :: var_is_introduced; 77var bool: BOOL____00115 :: is_defined_var :: var_is_introduced; 78var bool: BOOL____00116 :: is_defined_var :: var_is_introduced; 79var bool: BOOL____00117 :: is_defined_var :: var_is_introduced; 80var bool: BOOL____00118 :: is_defined_var :: var_is_introduced; 81var bool: BOOL____00119 :: is_defined_var :: var_is_introduced; 82var bool: BOOL____00120 :: is_defined_var :: var_is_introduced; 83var bool: BOOL____00122 :: is_defined_var :: var_is_introduced; 84var bool: BOOL____00123 :: is_defined_var :: var_is_introduced; 85var bool: BOOL____00124 :: is_defined_var :: var_is_introduced; 86var bool: BOOL____00125 :: is_defined_var :: var_is_introduced; 87var bool: BOOL____00126 :: is_defined_var :: var_is_introduced; 88var bool: BOOL____00127 :: is_defined_var :: var_is_introduced; 89var bool: BOOL____00129 :: is_defined_var :: var_is_introduced; 90var bool: BOOL____00130 :: is_defined_var :: var_is_introduced; 91var bool: BOOL____00131 :: is_defined_var :: var_is_introduced; 92var bool: BOOL____00132 :: is_defined_var :: var_is_introduced; 93var bool: BOOL____00133 :: is_defined_var :: var_is_introduced; 94var bool: BOOL____00134 :: is_defined_var :: var_is_introduced; 95var bool: BOOL____00136 :: is_defined_var :: var_is_introduced; 96var bool: BOOL____00137 :: is_defined_var :: var_is_introduced; 97var bool: BOOL____00140 :: is_defined_var :: var_is_introduced; 98var bool: BOOL____00141 :: is_defined_var :: var_is_introduced; 99var bool: BOOL____00143 :: is_defined_var :: var_is_introduced; 100var bool: BOOL____00144 :: is_defined_var :: var_is_introduced; 101var bool: BOOL____00146 :: is_defined_var :: var_is_introduced; 102var bool: BOOL____00147 :: is_defined_var :: var_is_introduced; 103var bool: BOOL____00148 :: is_defined_var :: var_is_introduced; 104var bool: BOOL____00149 :: is_defined_var :: var_is_introduced; 105var bool: BOOL____00150 :: is_defined_var :: var_is_introduced; 106var bool: BOOL____00151 :: is_defined_var :: var_is_introduced; 107var bool: BOOL____00153 :: is_defined_var :: var_is_introduced; 108var bool: BOOL____00154 :: is_defined_var :: var_is_introduced; 109var bool: BOOL____00155 :: is_defined_var :: var_is_introduced; 110var bool: BOOL____00156 :: is_defined_var :: var_is_introduced; 111var bool: BOOL____00157 :: is_defined_var :: var_is_introduced; 112var bool: BOOL____00158 :: is_defined_var :: var_is_introduced; 113var bool: BOOL____00160 :: is_defined_var :: var_is_introduced; 114var bool: BOOL____00161 :: is_defined_var :: var_is_introduced; 115var bool: BOOL____00164 :: is_defined_var :: var_is_introduced; 116var bool: BOOL____00165 :: is_defined_var :: var_is_introduced; 117var bool: BOOL____00167 :: is_defined_var :: var_is_introduced; 118var bool: BOOL____00168 :: is_defined_var :: var_is_introduced; 119var bool: BOOL____00170 :: is_defined_var :: var_is_introduced; 120var bool: BOOL____00171 :: is_defined_var :: var_is_introduced; 121var bool: BOOL____00172 :: is_defined_var :: var_is_introduced; 122var bool: BOOL____00173 :: is_defined_var :: var_is_introduced; 123var bool: BOOL____00174 :: is_defined_var :: var_is_introduced; 124var bool: BOOL____00175 :: is_defined_var :: var_is_introduced; 125var bool: BOOL____00177 :: is_defined_var :: var_is_introduced; 126var bool: BOOL____00178 :: is_defined_var :: var_is_introduced; 127var bool: BOOL____00179 :: is_defined_var :: var_is_introduced; 128var bool: BOOL____00180 :: is_defined_var :: var_is_introduced; 129var bool: BOOL____00181 :: is_defined_var :: var_is_introduced; 130var bool: BOOL____00182 :: is_defined_var :: var_is_introduced; 131var bool: BOOL____00184 :: is_defined_var :: var_is_introduced; 132var bool: BOOL____00185 :: is_defined_var :: var_is_introduced; 133array [1..25] of var bool: a :: output_array([1..5, 1..5]); 134array [1..2] of var 1..5: s____00001; 135array [1..2] of var 1..5: s____00027; 136array [1..1] of var 1..5: s____00053; 137array [1..2] of var 1..5: s____00065; 138array [1..1] of var 1..5: s____00091; 139array [1..1] of var 1..5: s____00101; 140array [1..2] of var 1..5: s____00111; 141array [1..2] of var 1..5: s____00139; 142array [1..2] of var 1..5: s____00163; 143constraint array_bool_and([BOOL____00006, BOOL____00007], BOOL____00008) :: defines_var(BOOL____00008); 144constraint array_bool_and([BOOL____00010, BOOL____00011], BOOL____00014) :: defines_var(BOOL____00014); 145constraint array_bool_and([BOOL____00012, BOOL____00013], BOOL____00015) :: defines_var(BOOL____00015); 146constraint array_bool_and([BOOL____00017, BOOL____00018], BOOL____00021) :: defines_var(BOOL____00021); 147constraint array_bool_and([BOOL____00019, BOOL____00020], BOOL____00022) :: defines_var(BOOL____00022); 148constraint array_bool_and([BOOL____00032, BOOL____00033], BOOL____00034) :: defines_var(BOOL____00034); 149constraint array_bool_and([BOOL____00036, BOOL____00037], BOOL____00040) :: defines_var(BOOL____00040); 150constraint array_bool_and([BOOL____00038, BOOL____00039], BOOL____00041) :: defines_var(BOOL____00041); 151constraint array_bool_and([BOOL____00043, BOOL____00044], BOOL____00047) :: defines_var(BOOL____00047); 152constraint array_bool_and([BOOL____00045, BOOL____00046], BOOL____00048) :: defines_var(BOOL____00048); 153constraint array_bool_and([BOOL____00055, BOOL____00056], a[8]); 154constraint array_bool_and([BOOL____00058, BOOL____00059], a[13]); 155constraint array_bool_and([BOOL____00061, BOOL____00062], a[18]); 156constraint array_bool_and([BOOL____00070, BOOL____00071], BOOL____00072) :: defines_var(BOOL____00072); 157constraint array_bool_and([BOOL____00074, BOOL____00075], BOOL____00078) :: defines_var(BOOL____00078); 158constraint array_bool_and([BOOL____00076, BOOL____00077], BOOL____00079) :: defines_var(BOOL____00079); 159constraint array_bool_and([BOOL____00081, BOOL____00082], BOOL____00085) :: defines_var(BOOL____00085); 160constraint array_bool_and([BOOL____00083, BOOL____00084], BOOL____00086) :: defines_var(BOOL____00086); 161constraint array_bool_and([BOOL____00094, BOOL____00095], a[11]); 162constraint array_bool_and([BOOL____00097, BOOL____00098], a[16]); 163constraint array_bool_and([BOOL____00104, BOOL____00105], a[23]); 164constraint array_bool_and([BOOL____00107, BOOL____00108], a[24]); 165constraint array_bool_and([BOOL____00115, BOOL____00116], BOOL____00119) :: defines_var(BOOL____00119); 166constraint array_bool_and([BOOL____00117, BOOL____00118], BOOL____00120) :: defines_var(BOOL____00120); 167constraint array_bool_and([BOOL____00122, BOOL____00123], BOOL____00126) :: defines_var(BOOL____00126); 168constraint array_bool_and([BOOL____00124, BOOL____00125], BOOL____00127) :: defines_var(BOOL____00127); 169constraint array_bool_and([BOOL____00129, BOOL____00130], BOOL____00133) :: defines_var(BOOL____00133); 170constraint array_bool_and([BOOL____00131, BOOL____00132], BOOL____00134) :: defines_var(BOOL____00134); 171constraint array_bool_and([BOOL____00146, BOOL____00147], BOOL____00150) :: defines_var(BOOL____00150); 172constraint array_bool_and([BOOL____00148, BOOL____00149], BOOL____00151) :: defines_var(BOOL____00151); 173constraint array_bool_and([BOOL____00153, BOOL____00154], BOOL____00157) :: defines_var(BOOL____00157); 174constraint array_bool_and([BOOL____00155, BOOL____00156], BOOL____00158) :: defines_var(BOOL____00158); 175constraint array_bool_and([BOOL____00170, BOOL____00171], BOOL____00174) :: defines_var(BOOL____00174); 176constraint array_bool_and([BOOL____00172, BOOL____00173], BOOL____00175) :: defines_var(BOOL____00175); 177constraint array_bool_and([BOOL____00177, BOOL____00178], BOOL____00181) :: defines_var(BOOL____00181); 178constraint array_bool_and([BOOL____00179, BOOL____00180], BOOL____00182) :: defines_var(BOOL____00182); 179constraint array_bool_or([BOOL____00003, BOOL____00002], a[5]); 180constraint array_bool_or([BOOL____00005, BOOL____00008], a[10]); 181constraint array_bool_or([BOOL____00014, BOOL____00015], a[15]); 182constraint array_bool_or([BOOL____00021, BOOL____00022], a[20]); 183constraint array_bool_or([BOOL____00025, BOOL____00024], a[25]); 184constraint array_bool_or([BOOL____00029, BOOL____00028], a[4]); 185constraint array_bool_or([BOOL____00031, BOOL____00034], a[9]); 186constraint array_bool_or([BOOL____00040, BOOL____00041], a[14]); 187constraint array_bool_or([BOOL____00047, BOOL____00048], a[19]); 188constraint array_bool_or([BOOL____00051, BOOL____00050], a[24]); 189constraint array_bool_or([BOOL____00067, BOOL____00066], a[2]); 190constraint array_bool_or([BOOL____00069, BOOL____00072], a[7]); 191constraint array_bool_or([BOOL____00078, BOOL____00079], a[12]); 192constraint array_bool_or([BOOL____00085, BOOL____00086], a[17]); 193constraint array_bool_or([BOOL____00089, BOOL____00088], a[22]); 194constraint array_bool_or([BOOL____00113, BOOL____00112], a[16]); 195constraint array_bool_or([BOOL____00119, BOOL____00120], a[17]); 196constraint array_bool_or([BOOL____00126, BOOL____00127], a[18]); 197constraint array_bool_or([BOOL____00133, BOOL____00134], a[19]); 198constraint array_bool_or([BOOL____00137, BOOL____00136], a[20]); 199constraint array_bool_or([BOOL____00141, BOOL____00140], a[6]); 200constraint array_bool_or([BOOL____00144, BOOL____00143], a[7]); 201constraint array_bool_or([BOOL____00150, BOOL____00151], a[8]); 202constraint array_bool_or([BOOL____00157, BOOL____00158], a[9]); 203constraint array_bool_or([BOOL____00161, BOOL____00160], a[10]); 204constraint array_bool_or([BOOL____00165, BOOL____00164], a[1]); 205constraint array_bool_or([BOOL____00168, BOOL____00167], a[2]); 206constraint array_bool_or([BOOL____00174, BOOL____00175], a[3]); 207constraint array_bool_or([BOOL____00181, BOOL____00182], a[4]); 208constraint array_bool_or([BOOL____00185, BOOL____00184], a[5]); 209constraint bool_eq(a[11], false); 210constraint bool_eq(a[12], false); 211constraint bool_eq(a[13], false); 212constraint bool_eq(a[14], false); 213constraint bool_eq(a[15], false); 214constraint int_le_reif(s____00001[1], 1, BOOL____00002) :: defines_var(BOOL____00002); 215constraint int_le_reif(s____00001[1], 2, BOOL____00005) :: defines_var(BOOL____00005); 216constraint int_le_reif(s____00001[1], 3, BOOL____00010) :: defines_var(BOOL____00010); 217constraint int_le_reif(s____00001[1], 4, BOOL____00017) :: defines_var(BOOL____00017); 218constraint int_le_reif(s____00001[2], 1, BOOL____00003) :: defines_var(BOOL____00003); 219constraint int_le_reif(s____00001[2], 2, BOOL____00006) :: defines_var(BOOL____00006); 220constraint int_le_reif(s____00001[2], 3, BOOL____00012) :: defines_var(BOOL____00012); 221constraint int_le_reif(s____00001[2], 4, BOOL____00019) :: defines_var(BOOL____00019); 222constraint int_le_reif(s____00027[1], 1, BOOL____00028) :: defines_var(BOOL____00028); 223constraint int_le_reif(s____00027[1], 2, BOOL____00031) :: defines_var(BOOL____00031); 224constraint int_le_reif(s____00027[1], 3, BOOL____00036) :: defines_var(BOOL____00036); 225constraint int_le_reif(s____00027[1], 4, BOOL____00043) :: defines_var(BOOL____00043); 226constraint int_le_reif(s____00027[2], 1, BOOL____00029) :: defines_var(BOOL____00029); 227constraint int_le_reif(s____00027[2], 2, BOOL____00032) :: defines_var(BOOL____00032); 228constraint int_le_reif(s____00027[2], 3, BOOL____00038) :: defines_var(BOOL____00038); 229constraint int_le_reif(s____00027[2], 4, BOOL____00045) :: defines_var(BOOL____00045); 230constraint int_le_reif(s____00053[1], 1, a[3]); 231constraint int_le_reif(s____00053[1], 2, BOOL____00055) :: defines_var(BOOL____00055); 232constraint int_le_reif(s____00053[1], 3, BOOL____00058) :: defines_var(BOOL____00058); 233constraint int_le_reif(s____00053[1], 4, BOOL____00061) :: defines_var(BOOL____00061); 234constraint int_le_reif(s____00065[1], 1, BOOL____00066) :: defines_var(BOOL____00066); 235constraint int_le_reif(s____00065[1], 2, BOOL____00069) :: defines_var(BOOL____00069); 236constraint int_le_reif(s____00065[1], 3, BOOL____00074) :: defines_var(BOOL____00074); 237constraint int_le_reif(s____00065[1], 4, BOOL____00081) :: defines_var(BOOL____00081); 238constraint int_le_reif(s____00065[2], 1, BOOL____00067) :: defines_var(BOOL____00067); 239constraint int_le_reif(s____00065[2], 2, BOOL____00070) :: defines_var(BOOL____00070); 240constraint int_le_reif(s____00065[2], 3, BOOL____00076) :: defines_var(BOOL____00076); 241constraint int_le_reif(s____00065[2], 4, BOOL____00083) :: defines_var(BOOL____00083); 242constraint int_le_reif(s____00091[1], 1, a[1]); 243constraint int_le_reif(s____00091[1], 2, a[6]); 244constraint int_le_reif(s____00091[1], 3, BOOL____00094) :: defines_var(BOOL____00094); 245constraint int_le_reif(s____00091[1], 4, BOOL____00097) :: defines_var(BOOL____00097); 246constraint int_le_reif(s____00101[1], 1, a[21]); 247constraint int_le_reif(s____00101[1], 2, a[22]); 248constraint int_le_reif(s____00101[1], 3, BOOL____00104) :: defines_var(BOOL____00104); 249constraint int_le_reif(s____00101[1], 4, BOOL____00107) :: defines_var(BOOL____00107); 250constraint int_le_reif(s____00111[1], 1, BOOL____00112) :: defines_var(BOOL____00112); 251constraint int_le_reif(s____00111[1], 2, BOOL____00115) :: defines_var(BOOL____00115); 252constraint int_le_reif(s____00111[1], 3, BOOL____00122) :: defines_var(BOOL____00122); 253constraint int_le_reif(s____00111[1], 4, BOOL____00129) :: defines_var(BOOL____00129); 254constraint int_le_reif(s____00111[2], 1, BOOL____00113) :: defines_var(BOOL____00113); 255constraint int_le_reif(s____00111[2], 2, BOOL____00117) :: defines_var(BOOL____00117); 256constraint int_le_reif(s____00111[2], 3, BOOL____00124) :: defines_var(BOOL____00124); 257constraint int_le_reif(s____00111[2], 4, BOOL____00131) :: defines_var(BOOL____00131); 258constraint int_le_reif(s____00139[1], 1, BOOL____00140) :: defines_var(BOOL____00140); 259constraint int_le_reif(s____00139[1], 2, BOOL____00143) :: defines_var(BOOL____00143); 260constraint int_le_reif(s____00139[1], 3, BOOL____00146) :: defines_var(BOOL____00146); 261constraint int_le_reif(s____00139[1], 4, BOOL____00153) :: defines_var(BOOL____00153); 262constraint int_le_reif(s____00139[2], 1, BOOL____00141) :: defines_var(BOOL____00141); 263constraint int_le_reif(s____00139[2], 2, BOOL____00144) :: defines_var(BOOL____00144); 264constraint int_le_reif(s____00139[2], 3, BOOL____00148) :: defines_var(BOOL____00148); 265constraint int_le_reif(s____00139[2], 4, BOOL____00155) :: defines_var(BOOL____00155); 266constraint int_le_reif(s____00163[1], 1, BOOL____00164) :: defines_var(BOOL____00164); 267constraint int_le_reif(s____00163[1], 2, BOOL____00167) :: defines_var(BOOL____00167); 268constraint int_le_reif(s____00163[1], 3, BOOL____00170) :: defines_var(BOOL____00170); 269constraint int_le_reif(s____00163[1], 4, BOOL____00177) :: defines_var(BOOL____00177); 270constraint int_le_reif(s____00163[2], 1, BOOL____00165) :: defines_var(BOOL____00165); 271constraint int_le_reif(s____00163[2], 2, BOOL____00168) :: defines_var(BOOL____00168); 272constraint int_le_reif(s____00163[2], 3, BOOL____00172) :: defines_var(BOOL____00172); 273constraint int_le_reif(s____00163[2], 4, BOOL____00179) :: defines_var(BOOL____00179); 274constraint int_lin_le([1], [s____00091[1]], 4); 275constraint int_lin_le([1], [s____00101[1]], 4); 276constraint int_lin_le([1], [s____00139[2]], 4); 277constraint int_lin_le([1], [s____00163[2]], 4); 278constraint int_lin_le([1, -1], [s____00001[1], s____00001[2]], -3); 279constraint int_lin_le([1, -1], [s____00027[1], s____00027[2]], -3); 280constraint int_lin_le([1, -1], [s____00065[1], s____00065[2]], -3); 281constraint int_lin_le([1, -1], [s____00111[1], s____00111[2]], -2); 282constraint int_lin_le([1, -1], [s____00139[1], s____00139[2]], -3); 283constraint int_lin_le([1, -1], [s____00163[1], s____00163[2]], -3); 284constraint int_lin_le_reif([-1], [s____00001[1]], -4, BOOL____00024) :: defines_var(BOOL____00024); 285constraint int_lin_le_reif([-1], [s____00001[1]], -3, BOOL____00018) :: defines_var(BOOL____00018); 286constraint int_lin_le_reif([-1], [s____00001[1]], -2, BOOL____00011) :: defines_var(BOOL____00011); 287constraint int_lin_le_reif([-1], [s____00001[2]], -5, BOOL____00025) :: defines_var(BOOL____00025); 288constraint int_lin_le_reif([-1], [s____00001[2]], -4, BOOL____00020) :: defines_var(BOOL____00020); 289constraint int_lin_le_reif([-1], [s____00001[2]], -3, BOOL____00013) :: defines_var(BOOL____00013); 290constraint int_lin_le_reif([-1], [s____00001[2]], -2, BOOL____00007) :: defines_var(BOOL____00007); 291constraint int_lin_le_reif([-1], [s____00027[1]], -4, BOOL____00050) :: defines_var(BOOL____00050); 292constraint int_lin_le_reif([-1], [s____00027[1]], -3, BOOL____00044) :: defines_var(BOOL____00044); 293constraint int_lin_le_reif([-1], [s____00027[1]], -2, BOOL____00037) :: defines_var(BOOL____00037); 294constraint int_lin_le_reif([-1], [s____00027[2]], -5, BOOL____00051) :: defines_var(BOOL____00051); 295constraint int_lin_le_reif([-1], [s____00027[2]], -4, BOOL____00046) :: defines_var(BOOL____00046); 296constraint int_lin_le_reif([-1], [s____00027[2]], -3, BOOL____00039) :: defines_var(BOOL____00039); 297constraint int_lin_le_reif([-1], [s____00027[2]], -2, BOOL____00033) :: defines_var(BOOL____00033); 298constraint int_lin_le_reif([-1], [s____00053[1]], -5, a[23]); 299constraint int_lin_le_reif([-1], [s____00053[1]], -4, BOOL____00062) :: defines_var(BOOL____00062); 300constraint int_lin_le_reif([-1], [s____00053[1]], -3, BOOL____00059) :: defines_var(BOOL____00059); 301constraint int_lin_le_reif([-1], [s____00053[1]], -2, BOOL____00056) :: defines_var(BOOL____00056); 302constraint int_lin_le_reif([-1], [s____00065[1]], -4, BOOL____00088) :: defines_var(BOOL____00088); 303constraint int_lin_le_reif([-1], [s____00065[1]], -3, BOOL____00082) :: defines_var(BOOL____00082); 304constraint int_lin_le_reif([-1], [s____00065[1]], -2, BOOL____00075) :: defines_var(BOOL____00075); 305constraint int_lin_le_reif([-1], [s____00065[2]], -5, BOOL____00089) :: defines_var(BOOL____00089); 306constraint int_lin_le_reif([-1], [s____00065[2]], -4, BOOL____00084) :: defines_var(BOOL____00084); 307constraint int_lin_le_reif([-1], [s____00065[2]], -3, BOOL____00077) :: defines_var(BOOL____00077); 308constraint int_lin_le_reif([-1], [s____00065[2]], -2, BOOL____00071) :: defines_var(BOOL____00071); 309constraint int_lin_le_reif([-1], [s____00091[1]], -4, a[21]); 310constraint int_lin_le_reif([-1], [s____00091[1]], -3, BOOL____00098) :: defines_var(BOOL____00098); 311constraint int_lin_le_reif([-1], [s____00091[1]], -2, BOOL____00095) :: defines_var(BOOL____00095); 312constraint int_lin_le_reif([-1], [s____00101[1]], -4, a[25]); 313constraint int_lin_le_reif([-1], [s____00101[1]], -3, BOOL____00108) :: defines_var(BOOL____00108); 314constraint int_lin_le_reif([-1], [s____00101[1]], -2, BOOL____00105) :: defines_var(BOOL____00105); 315constraint int_lin_le_reif([-1], [s____00111[1]], -5, BOOL____00136) :: defines_var(BOOL____00136); 316constraint int_lin_le_reif([-1], [s____00111[1]], -4, BOOL____00130) :: defines_var(BOOL____00130); 317constraint int_lin_le_reif([-1], [s____00111[1]], -3, BOOL____00123) :: defines_var(BOOL____00123); 318constraint int_lin_le_reif([-1], [s____00111[1]], -2, BOOL____00116) :: defines_var(BOOL____00116); 319constraint int_lin_le_reif([-1], [s____00111[2]], -5, BOOL____00137) :: defines_var(BOOL____00137); 320constraint int_lin_le_reif([-1], [s____00111[2]], -4, BOOL____00132) :: defines_var(BOOL____00132); 321constraint int_lin_le_reif([-1], [s____00111[2]], -3, BOOL____00125) :: defines_var(BOOL____00125); 322constraint int_lin_le_reif([-1], [s____00111[2]], -2, BOOL____00118) :: defines_var(BOOL____00118); 323constraint int_lin_le_reif([-1], [s____00139[1]], -4, BOOL____00160) :: defines_var(BOOL____00160); 324constraint int_lin_le_reif([-1], [s____00139[1]], -3, BOOL____00154) :: defines_var(BOOL____00154); 325constraint int_lin_le_reif([-1], [s____00139[1]], -2, BOOL____00147) :: defines_var(BOOL____00147); 326constraint int_lin_le_reif([-1], [s____00139[2]], -4, BOOL____00161) :: defines_var(BOOL____00161); 327constraint int_lin_le_reif([-1], [s____00139[2]], -3, BOOL____00156) :: defines_var(BOOL____00156); 328constraint int_lin_le_reif([-1], [s____00139[2]], -2, BOOL____00149) :: defines_var(BOOL____00149); 329constraint int_lin_le_reif([-1], [s____00163[1]], -4, BOOL____00184) :: defines_var(BOOL____00184); 330constraint int_lin_le_reif([-1], [s____00163[1]], -3, BOOL____00178) :: defines_var(BOOL____00178); 331constraint int_lin_le_reif([-1], [s____00163[1]], -2, BOOL____00171) :: defines_var(BOOL____00171); 332constraint int_lin_le_reif([-1], [s____00163[2]], -4, BOOL____00185) :: defines_var(BOOL____00185); 333constraint int_lin_le_reif([-1], [s____00163[2]], -3, BOOL____00180) :: defines_var(BOOL____00180); 334constraint int_lin_le_reif([-1], [s____00163[2]], -2, BOOL____00173) :: defines_var(BOOL____00173); 335solve satisfy; 336