(benchmark frugal300
  :source {
   test for Yices (taken from SMT 2008 paper by Sava Krstic et al.)
  }
  :status unsat
  :category { crafted }
  :logic QF_AX
  :extrafuns ((a Array))
  :extrafuns ((b Array))
  :extrafuns ((i0 Index))
  :extrafuns ((i1 Index))
  :extrafuns ((i2 Index))
  :extrafuns ((i3 Index))
  :extrafuns ((i4 Index))
  :extrafuns ((i5 Index))
  :extrafuns ((i6 Index))
  :extrafuns ((i7 Index))
  :extrafuns ((i8 Index))
  :extrafuns ((i9 Index))
  :extrafuns ((i10 Index))
  :extrafuns ((i11 Index))
  :extrafuns ((i12 Index))
  :extrafuns ((i13 Index))
  :extrafuns ((i14 Index))
  :extrafuns ((i15 Index))
  :extrafuns ((i16 Index))
  :extrafuns ((i17 Index))
  :extrafuns ((i18 Index))
  :extrafuns ((i19 Index))
  :extrafuns ((i20 Index))
  :extrafuns ((i21 Index))
  :extrafuns ((i22 Index))
  :extrafuns ((i23 Index))
  :extrafuns ((i24 Index))
  :extrafuns ((i25 Index))
  :extrafuns ((i26 Index))
  :extrafuns ((i27 Index))
  :extrafuns ((i28 Index))
  :extrafuns ((i29 Index))
  :extrafuns ((i30 Index))
  :extrafuns ((i31 Index))
  :extrafuns ((i32 Index))
  :extrafuns ((i33 Index))
  :extrafuns ((i34 Index))
  :extrafuns ((i35 Index))
  :extrafuns ((i36 Index))
  :extrafuns ((i37 Index))
  :extrafuns ((i38 Index))
  :extrafuns ((i39 Index))
  :extrafuns ((i40 Index))
  :extrafuns ((i41 Index))
  :extrafuns ((i42 Index))
  :extrafuns ((i43 Index))
  :extrafuns ((i44 Index))
  :extrafuns ((i45 Index))
  :extrafuns ((i46 Index))
  :extrafuns ((i47 Index))
  :extrafuns ((i48 Index))
  :extrafuns ((i49 Index))
  :extrafuns ((i50 Index))
  :extrafuns ((i51 Index))
  :extrafuns ((i52 Index))
  :extrafuns ((i53 Index))
  :extrafuns ((i54 Index))
  :extrafuns ((i55 Index))
  :extrafuns ((i56 Index))
  :extrafuns ((i57 Index))
  :extrafuns ((i58 Index))
  :extrafuns ((i59 Index))
  :extrafuns ((i60 Index))
  :extrafuns ((i61 Index))
  :extrafuns ((i62 Index))
  :extrafuns ((i63 Index))
  :extrafuns ((i64 Index))
  :extrafuns ((i65 Index))
  :extrafuns ((i66 Index))
  :extrafuns ((i67 Index))
  :extrafuns ((i68 Index))
  :extrafuns ((i69 Index))
  :extrafuns ((i70 Index))
  :extrafuns ((i71 Index))
  :extrafuns ((i72 Index))
  :extrafuns ((i73 Index))
  :extrafuns ((i74 Index))
  :extrafuns ((i75 Index))
  :extrafuns ((i76 Index))
  :extrafuns ((i77 Index))
  :extrafuns ((i78 Index))
  :extrafuns ((i79 Index))
  :extrafuns ((i80 Index))
  :extrafuns ((i81 Index))
  :extrafuns ((i82 Index))
  :extrafuns ((i83 Index))
  :extrafuns ((i84 Index))
  :extrafuns ((i85 Index))
  :extrafuns ((i86 Index))
  :extrafuns ((i87 Index))
  :extrafuns ((i88 Index))
  :extrafuns ((i89 Index))
  :extrafuns ((i90 Index))
  :extrafuns ((i91 Index))
  :extrafuns ((i92 Index))
  :extrafuns ((i93 Index))
  :extrafuns ((i94 Index))
  :extrafuns ((i95 Index))
  :extrafuns ((i96 Index))
  :extrafuns ((i97 Index))
  :extrafuns ((i98 Index))
  :extrafuns ((i99 Index))
  :extrafuns ((i100 Index))
  :extrafuns ((i101 Index))
  :extrafuns ((i102 Index))
  :extrafuns ((i103 Index))
  :extrafuns ((i104 Index))
  :extrafuns ((i105 Index))
  :extrafuns ((i106 Index))
  :extrafuns ((i107 Index))
  :extrafuns ((i108 Index))
  :extrafuns ((i109 Index))
  :extrafuns ((i110 Index))
  :extrafuns ((i111 Index))
  :extrafuns ((i112 Index))
  :extrafuns ((i113 Index))
  :extrafuns ((i114 Index))
  :extrafuns ((i115 Index))
  :extrafuns ((i116 Index))
  :extrafuns ((i117 Index))
  :extrafuns ((i118 Index))
  :extrafuns ((i119 Index))
  :extrafuns ((i120 Index))
  :extrafuns ((i121 Index))
  :extrafuns ((i122 Index))
  :extrafuns ((i123 Index))
  :extrafuns ((i124 Index))
  :extrafuns ((i125 Index))
  :extrafuns ((i126 Index))
  :extrafuns ((i127 Index))
  :extrafuns ((i128 Index))
  :extrafuns ((i129 Index))
  :extrafuns ((i130 Index))
  :extrafuns ((i131 Index))
  :extrafuns ((i132 Index))
  :extrafuns ((i133 Index))
  :extrafuns ((i134 Index))
  :extrafuns ((i135 Index))
  :extrafuns ((i136 Index))
  :extrafuns ((i137 Index))
  :extrafuns ((i138 Index))
  :extrafuns ((i139 Index))
  :extrafuns ((i140 Index))
  :extrafuns ((i141 Index))
  :extrafuns ((i142 Index))
  :extrafuns ((i143 Index))
  :extrafuns ((i144 Index))
  :extrafuns ((i145 Index))
  :extrafuns ((i146 Index))
  :extrafuns ((i147 Index))
  :extrafuns ((i148 Index))
  :extrafuns ((i149 Index))
  :extrafuns ((i150 Index))
  :extrafuns ((i151 Index))
  :extrafuns ((i152 Index))
  :extrafuns ((i153 Index))
  :extrafuns ((i154 Index))
  :extrafuns ((i155 Index))
  :extrafuns ((i156 Index))
  :extrafuns ((i157 Index))
  :extrafuns ((i158 Index))
  :extrafuns ((i159 Index))
  :extrafuns ((i160 Index))
  :extrafuns ((i161 Index))
  :extrafuns ((i162 Index))
  :extrafuns ((i163 Index))
  :extrafuns ((i164 Index))
  :extrafuns ((i165 Index))
  :extrafuns ((i166 Index))
  :extrafuns ((i167 Index))
  :extrafuns ((i168 Index))
  :extrafuns ((i169 Index))
  :extrafuns ((i170 Index))
  :extrafuns ((i171 Index))
  :extrafuns ((i172 Index))
  :extrafuns ((i173 Index))
  :extrafuns ((i174 Index))
  :extrafuns ((i175 Index))
  :extrafuns ((i176 Index))
  :extrafuns ((i177 Index))
  :extrafuns ((i178 Index))
  :extrafuns ((i179 Index))
  :extrafuns ((i180 Index))
  :extrafuns ((i181 Index))
  :extrafuns ((i182 Index))
  :extrafuns ((i183 Index))
  :extrafuns ((i184 Index))
  :extrafuns ((i185 Index))
  :extrafuns ((i186 Index))
  :extrafuns ((i187 Index))
  :extrafuns ((i188 Index))
  :extrafuns ((i189 Index))
  :extrafuns ((i190 Index))
  :extrafuns ((i191 Index))
  :extrafuns ((i192 Index))
  :extrafuns ((i193 Index))
  :extrafuns ((i194 Index))
  :extrafuns ((i195 Index))
  :extrafuns ((i196 Index))
  :extrafuns ((i197 Index))
  :extrafuns ((i198 Index))
  :extrafuns ((i199 Index))
  :extrafuns ((i200 Index))
  :extrafuns ((i201 Index))
  :extrafuns ((i202 Index))
  :extrafuns ((i203 Index))
  :extrafuns ((i204 Index))
  :extrafuns ((i205 Index))
  :extrafuns ((i206 Index))
  :extrafuns ((i207 Index))
  :extrafuns ((i208 Index))
  :extrafuns ((i209 Index))
  :extrafuns ((i210 Index))
  :extrafuns ((i211 Index))
  :extrafuns ((i212 Index))
  :extrafuns ((i213 Index))
  :extrafuns ((i214 Index))
  :extrafuns ((i215 Index))
  :extrafuns ((i216 Index))
  :extrafuns ((i217 Index))
  :extrafuns ((i218 Index))
  :extrafuns ((i219 Index))
  :extrafuns ((i220 Index))
  :extrafuns ((i221 Index))
  :extrafuns ((i222 Index))
  :extrafuns ((i223 Index))
  :extrafuns ((i224 Index))
  :extrafuns ((i225 Index))
  :extrafuns ((i226 Index))
  :extrafuns ((i227 Index))
  :extrafuns ((i228 Index))
  :extrafuns ((i229 Index))
  :extrafuns ((i230 Index))
  :extrafuns ((i231 Index))
  :extrafuns ((i232 Index))
  :extrafuns ((i233 Index))
  :extrafuns ((i234 Index))
  :extrafuns ((i235 Index))
  :extrafuns ((i236 Index))
  :extrafuns ((i237 Index))
  :extrafuns ((i238 Index))
  :extrafuns ((i239 Index))
  :extrafuns ((i240 Index))
  :extrafuns ((i241 Index))
  :extrafuns ((i242 Index))
  :extrafuns ((i243 Index))
  :extrafuns ((i244 Index))
  :extrafuns ((i245 Index))
  :extrafuns ((i246 Index))
  :extrafuns ((i247 Index))
  :extrafuns ((i248 Index))
  :extrafuns ((i249 Index))
  :extrafuns ((i250 Index))
  :extrafuns ((i251 Index))
  :extrafuns ((i252 Index))
  :extrafuns ((i253 Index))
  :extrafuns ((i254 Index))
  :extrafuns ((i255 Index))
  :extrafuns ((i256 Index))
  :extrafuns ((i257 Index))
  :extrafuns ((i258 Index))
  :extrafuns ((i259 Index))
  :extrafuns ((i260 Index))
  :extrafuns ((i261 Index))
  :extrafuns ((i262 Index))
  :extrafuns ((i263 Index))
  :extrafuns ((i264 Index))
  :extrafuns ((i265 Index))
  :extrafuns ((i266 Index))
  :extrafuns ((i267 Index))
  :extrafuns ((i268 Index))
  :extrafuns ((i269 Index))
  :extrafuns ((i270 Index))
  :extrafuns ((i271 Index))
  :extrafuns ((i272 Index))
  :extrafuns ((i273 Index))
  :extrafuns ((i274 Index))
  :extrafuns ((i275 Index))
  :extrafuns ((i276 Index))
  :extrafuns ((i277 Index))
  :extrafuns ((i278 Index))
  :extrafuns ((i279 Index))
  :extrafuns ((i280 Index))
  :extrafuns ((i281 Index))
  :extrafuns ((i282 Index))
  :extrafuns ((i283 Index))
  :extrafuns ((i284 Index))
  :extrafuns ((i285 Index))
  :extrafuns ((i286 Index))
  :extrafuns ((i287 Index))
  :extrafuns ((i288 Index))
  :extrafuns ((i289 Index))
  :extrafuns ((i290 Index))
  :extrafuns ((i291 Index))
  :extrafuns ((i292 Index))
  :extrafuns ((i293 Index))
  :extrafuns ((i294 Index))
  :extrafuns ((i295 Index))
  :extrafuns ((i296 Index))
  :extrafuns ((i297 Index))
  :extrafuns ((i298 Index))
  :extrafuns ((i299 Index))
  :extrafuns ((x0 Element))
  :extrafuns ((x1 Element))
  :extrafuns ((x2 Element))
  :extrafuns ((x3 Element))
  :extrafuns ((x4 Element))
  :extrafuns ((x5 Element))
  :extrafuns ((x6 Element))
  :extrafuns ((x7 Element))
  :extrafuns ((x8 Element))
  :extrafuns ((x9 Element))
  :extrafuns ((x10 Element))
  :extrafuns ((x11 Element))
  :extrafuns ((x12 Element))
  :extrafuns ((x13 Element))
  :extrafuns ((x14 Element))
  :extrafuns ((x15 Element))
  :extrafuns ((x16 Element))
  :extrafuns ((x17 Element))
  :extrafuns ((x18 Element))
  :extrafuns ((x19 Element))
  :extrafuns ((x20 Element))
  :extrafuns ((x21 Element))
  :extrafuns ((x22 Element))
  :extrafuns ((x23 Element))
  :extrafuns ((x24 Element))
  :extrafuns ((x25 Element))
  :extrafuns ((x26 Element))
  :extrafuns ((x27 Element))
  :extrafuns ((x28 Element))
  :extrafuns ((x29 Element))
  :extrafuns ((x30 Element))
  :extrafuns ((x31 Element))
  :extrafuns ((x32 Element))
  :extrafuns ((x33 Element))
  :extrafuns ((x34 Element))
  :extrafuns ((x35 Element))
  :extrafuns ((x36 Element))
  :extrafuns ((x37 Element))
  :extrafuns ((x38 Element))
  :extrafuns ((x39 Element))
  :extrafuns ((x40 Element))
  :extrafuns ((x41 Element))
  :extrafuns ((x42 Element))
  :extrafuns ((x43 Element))
  :extrafuns ((x44 Element))
  :extrafuns ((x45 Element))
  :extrafuns ((x46 Element))
  :extrafuns ((x47 Element))
  :extrafuns ((x48 Element))
  :extrafuns ((x49 Element))
  :extrafuns ((x50 Element))
  :extrafuns ((x51 Element))
  :extrafuns ((x52 Element))
  :extrafuns ((x53 Element))
  :extrafuns ((x54 Element))
  :extrafuns ((x55 Element))
  :extrafuns ((x56 Element))
  :extrafuns ((x57 Element))
  :extrafuns ((x58 Element))
  :extrafuns ((x59 Element))
  :extrafuns ((x60 Element))
  :extrafuns ((x61 Element))
  :extrafuns ((x62 Element))
  :extrafuns ((x63 Element))
  :extrafuns ((x64 Element))
  :extrafuns ((x65 Element))
  :extrafuns ((x66 Element))
  :extrafuns ((x67 Element))
  :extrafuns ((x68 Element))
  :extrafuns ((x69 Element))
  :extrafuns ((x70 Element))
  :extrafuns ((x71 Element))
  :extrafuns ((x72 Element))
  :extrafuns ((x73 Element))
  :extrafuns ((x74 Element))
  :extrafuns ((x75 Element))
  :extrafuns ((x76 Element))
  :extrafuns ((x77 Element))
  :extrafuns ((x78 Element))
  :extrafuns ((x79 Element))
  :extrafuns ((x80 Element))
  :extrafuns ((x81 Element))
  :extrafuns ((x82 Element))
  :extrafuns ((x83 Element))
  :extrafuns ((x84 Element))
  :extrafuns ((x85 Element))
  :extrafuns ((x86 Element))
  :extrafuns ((x87 Element))
  :extrafuns ((x88 Element))
  :extrafuns ((x89 Element))
  :extrafuns ((x90 Element))
  :extrafuns ((x91 Element))
  :extrafuns ((x92 Element))
  :extrafuns ((x93 Element))
  :extrafuns ((x94 Element))
  :extrafuns ((x95 Element))
  :extrafuns ((x96 Element))
  :extrafuns ((x97 Element))
  :extrafuns ((x98 Element))
  :extrafuns ((x99 Element))
  :extrafuns ((x100 Element))
  :extrafuns ((x101 Element))
  :extrafuns ((x102 Element))
  :extrafuns ((x103 Element))
  :extrafuns ((x104 Element))
  :extrafuns ((x105 Element))
  :extrafuns ((x106 Element))
  :extrafuns ((x107 Element))
  :extrafuns ((x108 Element))
  :extrafuns ((x109 Element))
  :extrafuns ((x110 Element))
  :extrafuns ((x111 Element))
  :extrafuns ((x112 Element))
  :extrafuns ((x113 Element))
  :extrafuns ((x114 Element))
  :extrafuns ((x115 Element))
  :extrafuns ((x116 Element))
  :extrafuns ((x117 Element))
  :extrafuns ((x118 Element))
  :extrafuns ((x119 Element))
  :extrafuns ((x120 Element))
  :extrafuns ((x121 Element))
  :extrafuns ((x122 Element))
  :extrafuns ((x123 Element))
  :extrafuns ((x124 Element))
  :extrafuns ((x125 Element))
  :extrafuns ((x126 Element))
  :extrafuns ((x127 Element))
  :extrafuns ((x128 Element))
  :extrafuns ((x129 Element))
  :extrafuns ((x130 Element))
  :extrafuns ((x131 Element))
  :extrafuns ((x132 Element))
  :extrafuns ((x133 Element))
  :extrafuns ((x134 Element))
  :extrafuns ((x135 Element))
  :extrafuns ((x136 Element))
  :extrafuns ((x137 Element))
  :extrafuns ((x138 Element))
  :extrafuns ((x139 Element))
  :extrafuns ((x140 Element))
  :extrafuns ((x141 Element))
  :extrafuns ((x142 Element))
  :extrafuns ((x143 Element))
  :extrafuns ((x144 Element))
  :extrafuns ((x145 Element))
  :extrafuns ((x146 Element))
  :extrafuns ((x147 Element))
  :extrafuns ((x148 Element))
  :extrafuns ((x149 Element))
  :extrafuns ((x150 Element))
  :extrafuns ((x151 Element))
  :extrafuns ((x152 Element))
  :extrafuns ((x153 Element))
  :extrafuns ((x154 Element))
  :extrafuns ((x155 Element))
  :extrafuns ((x156 Element))
  :extrafuns ((x157 Element))
  :extrafuns ((x158 Element))
  :extrafuns ((x159 Element))
  :extrafuns ((x160 Element))
  :extrafuns ((x161 Element))
  :extrafuns ((x162 Element))
  :extrafuns ((x163 Element))
  :extrafuns ((x164 Element))
  :extrafuns ((x165 Element))
  :extrafuns ((x166 Element))
  :extrafuns ((x167 Element))
  :extrafuns ((x168 Element))
  :extrafuns ((x169 Element))
  :extrafuns ((x170 Element))
  :extrafuns ((x171 Element))
  :extrafuns ((x172 Element))
  :extrafuns ((x173 Element))
  :extrafuns ((x174 Element))
  :extrafuns ((x175 Element))
  :extrafuns ((x176 Element))
  :extrafuns ((x177 Element))
  :extrafuns ((x178 Element))
  :extrafuns ((x179 Element))
  :extrafuns ((x180 Element))
  :extrafuns ((x181 Element))
  :extrafuns ((x182 Element))
  :extrafuns ((x183 Element))
  :extrafuns ((x184 Element))
  :extrafuns ((x185 Element))
  :extrafuns ((x186 Element))
  :extrafuns ((x187 Element))
  :extrafuns ((x188 Element))
  :extrafuns ((x189 Element))
  :extrafuns ((x190 Element))
  :extrafuns ((x191 Element))
  :extrafuns ((x192 Element))
  :extrafuns ((x193 Element))
  :extrafuns ((x194 Element))
  :extrafuns ((x195 Element))
  :extrafuns ((x196 Element))
  :extrafuns ((x197 Element))
  :extrafuns ((x198 Element))
  :extrafuns ((x199 Element))
  :extrafuns ((x200 Element))
  :extrafuns ((x201 Element))
  :extrafuns ((x202 Element))
  :extrafuns ((x203 Element))
  :extrafuns ((x204 Element))
  :extrafuns ((x205 Element))
  :extrafuns ((x206 Element))
  :extrafuns ((x207 Element))
  :extrafuns ((x208 Element))
  :extrafuns ((x209 Element))
  :extrafuns ((x210 Element))
  :extrafuns ((x211 Element))
  :extrafuns ((x212 Element))
  :extrafuns ((x213 Element))
  :extrafuns ((x214 Element))
  :extrafuns ((x215 Element))
  :extrafuns ((x216 Element))
  :extrafuns ((x217 Element))
  :extrafuns ((x218 Element))
  :extrafuns ((x219 Element))
  :extrafuns ((x220 Element))
  :extrafuns ((x221 Element))
  :extrafuns ((x222 Element))
  :extrafuns ((x223 Element))
  :extrafuns ((x224 Element))
  :extrafuns ((x225 Element))
  :extrafuns ((x226 Element))
  :extrafuns ((x227 Element))
  :extrafuns ((x228 Element))
  :extrafuns ((x229 Element))
  :extrafuns ((x230 Element))
  :extrafuns ((x231 Element))
  :extrafuns ((x232 Element))
  :extrafuns ((x233 Element))
  :extrafuns ((x234 Element))
  :extrafuns ((x235 Element))
  :extrafuns ((x236 Element))
  :extrafuns ((x237 Element))
  :extrafuns ((x238 Element))
  :extrafuns ((x239 Element))
  :extrafuns ((x240 Element))
  :extrafuns ((x241 Element))
  :extrafuns ((x242 Element))
  :extrafuns ((x243 Element))
  :extrafuns ((x244 Element))
  :extrafuns ((x245 Element))
  :extrafuns ((x246 Element))
  :extrafuns ((x247 Element))
  :extrafuns ((x248 Element))
  :extrafuns ((x249 Element))
  :extrafuns ((x250 Element))
  :extrafuns ((x251 Element))
  :extrafuns ((x252 Element))
  :extrafuns ((x253 Element))
  :extrafuns ((x254 Element))
  :extrafuns ((x255 Element))
  :extrafuns ((x256 Element))
  :extrafuns ((x257 Element))
  :extrafuns ((x258 Element))
  :extrafuns ((x259 Element))
  :extrafuns ((x260 Element))
  :extrafuns ((x261 Element))
  :extrafuns ((x262 Element))
  :extrafuns ((x263 Element))
  :extrafuns ((x264 Element))
  :extrafuns ((x265 Element))
  :extrafuns ((x266 Element))
  :extrafuns ((x267 Element))
  :extrafuns ((x268 Element))
  :extrafuns ((x269 Element))
  :extrafuns ((x270 Element))
  :extrafuns ((x271 Element))
  :extrafuns ((x272 Element))
  :extrafuns ((x273 Element))
  :extrafuns ((x274 Element))
  :extrafuns ((x275 Element))
  :extrafuns ((x276 Element))
  :extrafuns ((x277 Element))
  :extrafuns ((x278 Element))
  :extrafuns ((x279 Element))
  :extrafuns ((x280 Element))
  :extrafuns ((x281 Element))
  :extrafuns ((x282 Element))
  :extrafuns ((x283 Element))
  :extrafuns ((x284 Element))
  :extrafuns ((x285 Element))
  :extrafuns ((x286 Element))
  :extrafuns ((x287 Element))
  :extrafuns ((x288 Element))
  :extrafuns ((x289 Element))
  :extrafuns ((x290 Element))
  :extrafuns ((x291 Element))
  :extrafuns ((x292 Element))
  :extrafuns ((x293 Element))
  :extrafuns ((x294 Element))
  :extrafuns ((x295 Element))
  :extrafuns ((x296 Element))
  :extrafuns ((x297 Element))
  :extrafuns ((x298 Element))
  :extrafuns ((x299 Element))
  :formula (not (= 
(store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store a i0 x0) i1 x1) i2 x2) i3 x3) i4 x4) i5 x5) i6 x6) i7 x7) i8 x8) i9 x9) i10 x10) i11 x11) i12 x12) i13 x13) i14 x14) i15 x15) i16 x16) i17 x17) i18 x18) i19 x19) i20 x20) i21 x21) i22 x22) i23 x23) i24 x24) i25 x25) i26 x26) i27 x27) i28 x28) i29 x29) i30 x30) i31 x31) i32 x32) i33 x33) i34 x34) i35 x35) i36 x36) i37 x37) i38 x38) i39 x39) i40 x40) i41 x41) i42 x42) i43 x43) i44 x44) i45 x45) i46 x46) i47 x47) i48 x48) i49 x49) i50 x50) i51 x51) i52 x52) i53 x53) i54 x54) i55 x55) i56 x56) i57 x57) i58 x58) i59 x59) i60 x60) i61 x61) i62 x62) i63 x63) i64 x64) i65 x65) i66 x66) i67 x67) i68 x68) i69 x69) i70 x70) i71 x71) i72 x72) i73 x73) i74 x74) i75 x75) i76 x76) i77 x77) i78 x78) i79 x79) i80 x80) i81 x81) i82 x82) i83 x83) i84 x84) i85 x85) i86 x86) i87 x87) i88 x88) i89 x89) i90 x90) i91 x91) i92 x92) i93 x93) i94 x94) i95 x95) i96 x96) i97 x97) i98 x98) i99 x99) i100 x100) i101 x101) i102 x102) i103 x103) i104 x104) i105 x105) i106 x106) i107 x107) i108 x108) i109 x109) i110 x110) i111 x111) i112 x112) i113 x113) i114 x114) i115 x115) i116 x116) i117 x117) i118 x118) i119 x119) i120 x120) i121 x121) i122 x122) i123 x123) i124 x124) i125 x125) i126 x126) i127 x127) i128 x128) i129 x129) i130 x130) i131 x131) i132 x132) i133 x133) i134 x134) i135 x135) i136 x136) i137 x137) i138 x138) i139 x139) i140 x140) i141 x141) i142 x142) i143 x143) i144 x144) i145 x145) i146 x146) i147 x147) i148 x148) i149 x149) i150 x150) i151 x151) i152 x152) i153 x153) i154 x154) i155 x155) i156 x156) i157 x157) i158 x158) i159 x159) i160 x160) i161 x161) i162 x162) i163 x163) i164 x164) i165 x165) i166 x166) i167 x167) i168 x168) i169 x169) i170 x170) i171 x171) i172 x172) i173 x173) i174 x174) i175 x175) i176 x176) i177 x177) i178 x178) i179 x179) i180 x180) i181 x181) i182 x182) i183 x183) i184 x184) i185 x185) i186 x186) i187 x187) i188 x188) i189 x189) i190 x190) i191 x191) i192 x192) i193 x193) i194 x194) i195 x195) i196 x196) i197 x197) i198 x198) i199 x199) i200 x200) i201 x201) i202 x202) i203 x203) i204 x204) i205 x205) i206 x206) i207 x207) i208 x208) i209 x209) i210 x210) i211 x211) i212 x212) i213 x213) i214 x214) i215 x215) i216 x216) i217 x217) i218 x218) i219 x219) i220 x220) i221 x221) i222 x222) i223 x223) i224 x224) i225 x225) i226 x226) i227 x227) i228 x228) i229 x229) i230 x230) i231 x231) i232 x232) i233 x233) i234 x234) i235 x235) i236 x236) i237 x237) i238 x238) i239 x239) i240 x240) i241 x241) i242 x242) i243 x243) i244 x244) i245 x245) i246 x246) i247 x247) i248 x248) i249 x249) i250 x250) i251 x251) i252 x252) i253 x253) i254 x254) i255 x255) i256 x256) i257 x257) i258 x258) i259 x259) i260 x260) i261 x261) i262 x262) i263 x263) i264 x264) i265 x265) i266 x266) i267 x267) i268 x268) i269 x269) i270 x270) i271 x271) i272 x272) i273 x273) i274 x274) i275 x275) i276 x276) i277 x277) i278 x278) i279 x279) i280 x280) i281 x281) i282 x282) i283 x283) i284 x284) i285 x285) i286 x286) i287 x287) i288 x288) i289 x289) i290 x290) i291 x291) i292 x292) i293 x293) i294 x294) i295 x295) i296 x296) i297 x297) i298 x298) i299 x299)
(store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store b i0 x0) i1 x1) i2 x2) i3 x3) i4 x4) i5 x5) i6 x6) i7 x7) i8 x8) i9 x9) i10 x10) i11 x11) i12 x12) i13 x13) i14 x14) i15 x15) i16 x16) i17 x17) i18 x18) i19 x19) i20 x20) i21 x21) i22 x22) i23 x23) i24 x24) i25 x25) i26 x26) i27 x27) i28 x28) i29 x29) i30 x30) i31 x31) i32 x32) i33 x33) i34 x34) i35 x35) i36 x36) i37 x37) i38 x38) i39 x39) i40 x40) i41 x41) i42 x42) i43 x43) i44 x44) i45 x45) i46 x46) i47 x47) i48 x48) i49 x49) i50 x50) i51 x51) i52 x52) i53 x53) i54 x54) i55 x55) i56 x56) i57 x57) i58 x58) i59 x59) i60 x60) i61 x61) i62 x62) i63 x63) i64 x64) i65 x65) i66 x66) i67 x67) i68 x68) i69 x69) i70 x70) i71 x71) i72 x72) i73 x73) i74 x74) i75 x75) i76 x76) i77 x77) i78 x78) i79 x79) i80 x80) i81 x81) i82 x82) i83 x83) i84 x84) i85 x85) i86 x86) i87 x87) i88 x88) i89 x89) i90 x90) i91 x91) i92 x92) i93 x93) i94 x94) i95 x95) i96 x96) i97 x97) i98 x98) i99 x99) i100 x100) i101 x101) i102 x102) i103 x103) i104 x104) i105 x105) i106 x106) i107 x107) i108 x108) i109 x109) i110 x110) i111 x111) i112 x112) i113 x113) i114 x114) i115 x115) i116 x116) i117 x117) i118 x118) i119 x119) i120 x120) i121 x121) i122 x122) i123 x123) i124 x124) i125 x125) i126 x126) i127 x127) i128 x128) i129 x129) i130 x130) i131 x131) i132 x132) i133 x133) i134 x134) i135 x135) i136 x136) i137 x137) i138 x138) i139 x139) i140 x140) i141 x141) i142 x142) i143 x143) i144 x144) i145 x145) i146 x146) i147 x147) i148 x148) i149 x149) i150 x150) i151 x151) i152 x152) i153 x153) i154 x154) i155 x155) i156 x156) i157 x157) i158 x158) i159 x159) i160 x160) i161 x161) i162 x162) i163 x163) i164 x164) i165 x165) i166 x166) i167 x167) i168 x168) i169 x169) i170 x170) i171 x171) i172 x172) i173 x173) i174 x174) i175 x175) i176 x176) i177 x177) i178 x178) i179 x179) i180 x180) i181 x181) i182 x182) i183 x183) i184 x184) i185 x185) i186 x186) i187 x187) i188 x188) i189 x189) i190 x190) i191 x191) i192 x192) i193 x193) i194 x194) i195 x195) i196 x196) i197 x197) i198 x198) i199 x199) i200 x200) i201 x201) i202 x202) i203 x203) i204 x204) i205 x205) i206 x206) i207 x207) i208 x208) i209 x209) i210 x210) i211 x211) i212 x212) i213 x213) i214 x214) i215 x215) i216 x216) i217 x217) i218 x218) i219 x219) i220 x220) i221 x221) i222 x222) i223 x223) i224 x224) i225 x225) i226 x226) i227 x227) i228 x228) i229 x229) i230 x230) i231 x231) i232 x232) i233 x233) i234 x234) i235 x235) i236 x236) i237 x237) i238 x238) i239 x239) i240 x240) i241 x241) i242 x242) i243 x243) i244 x244) i245 x245) i246 x246) i247 x247) i248 x248) i249 x249) i250 x250) i251 x251) i252 x252) i253 x253) i254 x254) i255 x255) i256 x256) i257 x257) i258 x258) i259 x259) i260 x260) i261 x261) i262 x262) i263 x263) i264 x264) i265 x265) i266 x266) i267 x267) i268 x268) i269 x269) i270 x270) i271 x271) i272 x272) i273 x273) i274 x274) i275 x275) i276 x276) i277 x277) i278 x278) i279 x279) i280 x280) i281 x281) i282 x282) i283 x283) i284 x284) i285 x285) i286 x286) i287 x287) i288 x288) i289 x289) i290 x290) i291 x291) i292 x292) i293 x293) i294 x294) i295 x295) i296 x296) i297 x297) i298 x298) i299 x299)
))
)