(benchmark frugal200
  :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 ((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))
  :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 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)
(store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (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)
))
)