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