diff --git a/Indexing/TermSharing.cpp b/Indexing/TermSharing.cpp
index 133d28c72..d41679b3b 100644
--- a/Indexing/TermSharing.cpp
+++ b/Indexing/TermSharing.cpp
@@ -152,36 +152,33 @@ void TermSharing::computeAndSetSharedSortData(AtomicSort* sort)
 
   TIME_TRACE("sort sharing");
 
-    if(sort->isArraySort()){
-      _arraySorts.insert(TermList(sort));
+  unsigned weight = 1;
+  unsigned vars = 0;
+
+  for (TermList* tt = sort->args(); ! tt->isEmpty(); tt = tt->next()) {
+    if (tt->isVar()) {
+      ASS(tt->isOrdinaryVar());
+      vars++;
+      weight += 1;
     }
-    unsigned weight = 1;
-    unsigned vars = 0;
+    else {
+      ASS_REP(tt->term()->shared(), tt->term()->toString());
+      
+      Term* r = tt->term();
 
-    for (TermList* tt = sort->args(); ! tt->isEmpty(); tt = tt->next()) {
-      if (tt->isVar()) {
-        ASS(tt->isOrdinaryVar());
-        vars++;
-        weight += 1;
-      }
-      else {
-        ASS_REP(tt->term()->shared(), tt->term()->toString());
-        
-        Term* r = tt->term();
-  
-        vars += r->numVarOccs();
-        weight += r->weight();
-      }
-    }
-    sort->markShared();
-    sort->setId(_sorts.size());
-    sort->setNumVarOccs(vars);
-    sort->setWeight(weight);
-
-    ASS_REP(SortHelper::allTopLevelArgsAreSorts(sort), sort->toString());
-    if (!SortHelper::allTopLevelArgsAreSorts(sort)){
-      USER_ERROR("Immediate subterms of sort "+sort->toString()+" are not all sorts as mandated in rank-1 polymorphism!");      
+      vars += r->numVarOccs();
+      weight += r->weight();
     }
+  }
+  sort->markShared();
+  sort->setId(_sorts.size());
+  sort->setNumVarOccs(vars);
+  sort->setWeight(weight);
+
+  ASS_REP(SortHelper::allTopLevelArgsAreSorts(sort), sort->toString());
+  if (!SortHelper::allTopLevelArgsAreSorts(sort)){
+    USER_ERROR("Immediate subterms of sort "+sort->toString()+" are not all sorts as mandated in rank-1 polymorphism!");      
+  }
 } // TermSharing::computeAndSetSharedSortData
 
 /** same as `TermSharing::computeAndSetSharedTermData(Term*)` but for literals 
diff --git a/Indexing/TermSharing.hpp b/Indexing/TermSharing.hpp
index 67552a49e..f299c0b31 100644
--- a/Indexing/TermSharing.hpp
+++ b/Indexing/TermSharing.hpp
@@ -18,7 +18,6 @@
 #define __TermSharing__
 
 #include "Lib/Set.hpp"
-#include "Lib/DHSet.hpp"
 #include "Kernel/Term.hpp"
 
 using namespace Lib;
@@ -60,10 +59,6 @@ class TermSharing
         [&](auto i){ return *l2->nthArgument(i); }, 
         l2->arity(), someIf(l2->isTwoVarEquality(), [&](){ return l2->twoVarEqSort(); })); }
 
-  DHSet<TermList>* getArraySorts(){
-    return &_arraySorts;
-  }
-
   struct OpLitWrapper {
     OpLitWrapper(Literal* l) : l(l) {}
     Literal* l;
@@ -103,10 +98,6 @@ class TermSharing
   Set<Literal*,TermSharing> _literals;
   /** The set storing all sorts */
   Set<AtomicSort*,TermSharing> _sorts;
-  /* Set containing all array sorts. 
-   * Can be deleted once array axioms are made truly poltmorphic
-   */  
-  DHSet<TermList> _arraySorts;
 
   bool _poly;
   bool _wellSortednessCheckingDisabled;
diff --git a/Inferences/PolynomialEvaluation.cpp b/Inferences/PolynomialEvaluation.cpp
index 8a4dfb1ad..adeffede6 100644
--- a/Inferences/PolynomialEvaluation.cpp
+++ b/Inferences/PolynomialEvaluation.cpp
@@ -110,8 +110,6 @@ Option<LitSimplResult> PolynomialEvaluation::tryEvalPredicate(Literal* orig, Pol
 
       /* integer predicates */
       HANDLE_CASE(INT_DIVIDES)
-      case Interpretation::ARRAY_BOOL_SELECT:
-        return Option<LitSimplResult>();
 
       case ANY_INTERPRETED_FUNCTION: 
       case Kernel::Theory::INVALID_INTERPRETATION: 
diff --git a/Inferences/TheoryInstAndSimp.cpp b/Inferences/TheoryInstAndSimp.cpp
index 6cae61a6f..5bf90f561 100644
--- a/Inferences/TheoryInstAndSimp.cpp
+++ b/Inferences/TheoryInstAndSimp.cpp
@@ -169,7 +169,6 @@ bool TheoryInstAndSimp::isSupportedFunction(Term* trm) {
 
 bool TheoryInstAndSimp::isSupportedFunction(Theory::Interpretation itp) {
   switch (itp) {
-    case Theory::ARRAY_BOOL_SELECT:
     case Theory::ARRAY_SELECT:
     case Theory::ARRAY_STORE:
     case Theory::INT_SUCCESSOR:
diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp
index 148fb5361..f5267d0c1 100644
--- a/Kernel/InferenceStore.cpp
+++ b/Kernel/InferenceStore.cpp
@@ -1137,7 +1137,6 @@ struct InferenceStore::Smt2ProofCheckPrinter
       case Theory::REAL_QUOTIENT: out << "/"; return;
 
       // array functions
-      case Theory::ARRAY_BOOL_SELECT:
       case Theory::ARRAY_SELECT: out << "select"; return;
       case Theory::ARRAY_STORE: out << "store"; return;
 
@@ -1240,7 +1239,6 @@ struct InferenceStore::Smt2ProofCheckPrinter
       case Theory::INT_REMAINDER_E:                                                       \
       case Theory::INT_FLOOR:                                                             \
       case Theory::REAL_QUOTIENT:                                                         \
-      case Theory::ARRAY_BOOL_SELECT:                                                     \
       case Theory::ARRAY_SELECT:                                                          \
       case Theory::ARRAY_STORE
 
diff --git a/Kernel/Signature.cpp b/Kernel/Signature.cpp
index a23e966a8..a39477ba0 100644
--- a/Kernel/Signature.cpp
+++ b/Kernel/Signature.cpp
@@ -260,7 +260,7 @@ Signature::Signature ():
 void Signature::addEquality()
 {
   // initialize equality
-  addInterpretedPredicate(Theory::EQUAL, OperatorType::getPredicateType(2), "=");
+  addInterpretedPredicate(Theory::EQUAL, "=");
   ASS_EQ(predicateName(0), "="); //equality must have number 0
   getPredicate(0)->markSkip();
 }
@@ -285,14 +285,12 @@ Signature::~Signature ()
 /**
  * Add interpreted function
  */
-unsigned Signature::addInterpretedFunction(Interpretation interpretation, OperatorType* type, const std::string& name)
+unsigned Signature::addInterpretedFunction(Interpretation interpretation, const std::string& name)
 {
   ASS(Theory::isFunction(interpretation));
 
-  Theory::MonomorphisedInterpretation mi = std::make_pair(interpretation,type);
-
   unsigned res;
-  if (_iSymbols.find(mi,res)) { // already declared
+  if (_iSymbols.find(interpretation,res)) { // already declared
     // TODO should this really be done in release mode?
     if (name!=functionName(res)) {
       USER_ERROR("Interpreted function '"+functionName(res)+"' has the same interpretation as '"+name+"' should have");
@@ -300,6 +298,7 @@ unsigned Signature::addInterpretedFunction(Interpretation interpretation, Operat
     return res;
   }
 
+  auto type = Theory::getOperatorType(interpretation);
   auto symbolKey = SymbolKey(std::make_pair(interpretation, type));
   ASS_REP(!_funNames.find(symbolKey), name);
 
@@ -307,7 +306,7 @@ unsigned Signature::addInterpretedFunction(Interpretation interpretation, Operat
   InterpretedSymbol* sym = new InterpretedSymbol(name, interpretation);
   _funs.push(sym);
   _funNames.insert(symbolKey, fnNum);
-  ALWAYS(_iSymbols.insert(mi, fnNum));
+  ALWAYS(_iSymbols.insert(interpretation, fnNum));
 
   OperatorType* fnType = type;
   ASS(fnType->isFunctionType());
@@ -318,22 +317,21 @@ unsigned Signature::addInterpretedFunction(Interpretation interpretation, Operat
 /**
  * Add interpreted predicate
  */
-unsigned Signature::addInterpretedPredicate(Interpretation interpretation, OperatorType* type, const std::string& name)
+unsigned Signature::addInterpretedPredicate(Interpretation interpretation, const std::string& name)
 {
   ASS(!Theory::isFunction(interpretation));
 
   // cout << "addInterpretedPredicate " << (type ? type->toString() : "nullptr") << " " << name << endl;
 
-  Theory::MonomorphisedInterpretation mi = std::make_pair(interpretation,type);
-
   unsigned res;
-  if (_iSymbols.find(mi,res)) { // already declared
+  if (_iSymbols.find(interpretation,res)) { // already declared
     if (name!=predicateName(res)) {
       USER_ERROR("Interpreted predicate '"+predicateName(res)+"' has the same interpretation as '"+name+"' should have");
     }
     return res;
   }
 
+  auto type = Theory::getOperatorType(interpretation);
   auto symbolKey = SymbolKey(std::make_pair(interpretation, type));
 
   // cout << "symbolKey " << symbolKey << endl;
@@ -344,7 +342,7 @@ unsigned Signature::addInterpretedPredicate(Interpretation interpretation, Opera
   InterpretedSymbol* sym = new InterpretedSymbol(name, interpretation);
   _preds.push(sym);
   _predNames.insert(symbolKey,predNum);
-  ALWAYS(_iSymbols.insert(mi, predNum));
+  ALWAYS(_iSymbols.insert(interpretation, predNum));
   if (predNum!=0) {
     OperatorType* predType = type;
     ASS_REP(!predType->isFunctionType(), predType->toString());
@@ -359,12 +357,10 @@ unsigned Signature::addInterpretedPredicate(Interpretation interpretation, Opera
  *
  * If no such symbol exists, it is created.
  */
-unsigned Signature::getInterpretingSymbol(Interpretation interp, OperatorType* type)
+unsigned Signature::getInterpretingSymbol(Interpretation interp)
 {
-  Theory::MonomorphisedInterpretation mi = std::make_pair(interp,type);
-
   unsigned res;
-  if (_iSymbols.find(mi, res)) {
+  if (_iSymbols.find(interp, res)) {
     return res;
   }
 
@@ -379,7 +375,7 @@ unsigned Signature::getInterpretingSymbol(Interpretation interp, OperatorType* t
       }
       name=name+Int::toString(i);
     }
-    addInterpretedFunction(interp, type, name);
+    addInterpretedFunction(interp, name);
   }
   else {
     if (predicateExists(name, arity)) {
@@ -389,11 +385,11 @@ unsigned Signature::getInterpretingSymbol(Interpretation interp, OperatorType* t
       }
       name=name+Int::toString(i);
     }
-    addInterpretedPredicate(interp, type, name);
+    addInterpretedPredicate(interp, name);
   }
 
   //we have now registered a new function, so it should be present in the map
-  return _iSymbols.get(mi);
+  return _iSymbols.get(interp);
 }
 
 const std::string& Signature::functionName(int number)
diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp
index 66c67f4a7..0541497a4 100644
--- a/Kernel/Signature.hpp
+++ b/Kernel/Signature.hpp
@@ -593,36 +593,14 @@ class Signature
     }
   }
 
-
-  unsigned addInterpretedFunction(Interpretation itp, OperatorType* type, const std::string& name);
-  unsigned addInterpretedFunction(Interpretation itp, const std::string& name)
-  {
-    ASS(!Theory::isPolymorphic(itp));
-    return addInterpretedFunction(itp,Theory::getNonpolymorphicOperatorType(itp),name);
-  }
-
-  unsigned addInterpretedPredicate(Interpretation itp, OperatorType* type, const std::string& name);
-  unsigned addInterpretedPredicate(Interpretation itp, const std::string& name)
-  {
-    ASS(!Theory::isPolymorphic(itp));
-    return addInterpretedPredicate(itp,Theory::getNonpolymorphicOperatorType(itp),name);
-  }
-
-  unsigned getInterpretingSymbol(Interpretation interp, OperatorType* type);
-  unsigned getInterpretingSymbol(Interpretation interp)
-  {
-    ASS(!Theory::isPolymorphic(interp));
-    return getInterpretingSymbol(interp,Theory::getNonpolymorphicOperatorType(interp));
-  }
+  unsigned addInterpretedFunction(Interpretation itp, const std::string& name);
+  unsigned addInterpretedPredicate(Interpretation itp, const std::string& name);
+  unsigned getInterpretingSymbol(Interpretation interp);
 
   /** Return true iff there is a symbol interpreted by Interpretation @b interp */
-  bool haveInterpretingSymbol(Interpretation interp, OperatorType* type) const {
-    return _iSymbols.find(std::make_pair(interp,type));
-  }
-  bool haveInterpretingSymbol(Interpretation interp)
+  bool hasInterpretingSymbol(Interpretation interp) const
   {
-    ASS(!Theory::isPolymorphic(interp));
-    return haveInterpretingSymbol(interp,Theory::getNonpolymorphicOperatorType(interp));
+    return _iSymbols.find(interp);
   }
 
   /** return the name of a function with a given number */
@@ -1037,13 +1015,13 @@ class Signature
   bool _distinctGroupsAddedTo;
 
   /**
-   * Map from MonomorphisedInterpretation values to function and predicate symbols representing them
+   * Map from Interpretation values to function and predicate symbols representing them
    *
    * We mix here function and predicate symbols, but it is not a problem, as
-   * the MonomorphisedInterpretation value already determines whether we deal with a function
+   * the Interpretation value already determines whether we deal with a function
    * or a predicate.
    */
-  DHMap<Theory::MonomorphisedInterpretation, unsigned> _iSymbols;
+  DHMap<Theory::Interpretation, unsigned> _iSymbols;
 
   /** the number of string constants */
   unsigned _strings;
diff --git a/Kernel/Term.cpp b/Kernel/Term.cpp
index 9f503a217..8b7ccc1f3 100644
--- a/Kernel/Term.cpp
+++ b/Kernel/Term.cpp
@@ -554,7 +554,7 @@ std::string Term::headToString() const
         auto bindingLhs = binding->literal()->termArg(0).term();
 
         std::string type;
-        if (Theory::tuples()->isConstructor(bindingLhs)) {
+        if (Theory::isTupleConstructor(bindingLhs)) {
           type += "[";
           for (unsigned i = 0; i < bindingLhs->numTermArguments(); i++) {
             auto arg = bindingLhs->termArg(i);
@@ -614,7 +614,7 @@ std::string Term::headToString() const
     }
   } else {
     unsigned proj;
-    if (!isSort() && Theory::tuples()->findProjection(functor(), isLiteral(), proj)) {
+    if (!isSort() && Theory::findTupleProjection(functor(), isLiteral(), proj)) {
       return "$proj(" + Int::toString(proj) + ", ";
     }
     std::string name = "";
@@ -889,7 +889,7 @@ std::string Literal::toString(bool reverseEquality) const
   }
 
   unsigned proj;
-  if (Theory::tuples()->findProjection(functor(), true, proj)) {
+  if (Theory::findTupleProjection(functor(), true, proj)) {
     return s + "$proj(" + Int::toString(proj) + ", " + args()->asArgsToString();
   }
   s += predicateName();
diff --git a/Kernel/Theory.cpp b/Kernel/Theory.cpp
index 7e52f1dfa..0ba8b995b 100644
--- a/Kernel/Theory.cpp
+++ b/Kernel/Theory.cpp
@@ -19,8 +19,6 @@
 #include "Lib/Environment.hpp"
 #include "Lib/Int.hpp"
 
-#include "Shell/Skolem.hpp"
-
 #include "Signature.hpp"
 #include "SortHelper.hpp"
 #include "OperatorType.hpp"
@@ -422,10 +420,8 @@ namespace Kernel {
 //
 
 Theory Theory::theory_obj;  // to facilitate destructor call at deinitization
-Theory::Tuples Theory::tuples_obj;
 
 Theory* theory = &Theory::theory_obj;
-Theory::Tuples* theory_tuples = &Theory::tuples_obj;
 
 /**
  * Accessor for the singleton instance of the Theory class.
@@ -435,21 +431,6 @@ Theory* Theory::instance()
   return theory;
 }
 
-Theory::Tuples* Theory::tuples()
-{
-  return theory_tuples;
-}
-
-/**
- * Constructor of the Theory object
- *
- * The constructor is private, since Theory is a singleton class.
- */
-Theory::Theory()
-{
-
-}
-
 /**
  * Return arity of the symbol that is interpreted by Interpretation
  * @b i.
@@ -552,14 +533,15 @@ unsigned Theory::getArity(Interpretation i)
   case REAL_REMAINDER_T:
   case REAL_REMAINDER_F:
 
+    return 2;
+
   case ARRAY_SELECT:
-  case ARRAY_BOOL_SELECT:
 
-    return 2;
+    return 4;
 
   case ARRAY_STORE:
 
-    return 3;
+    return 5;
 
   default:
     ASSERTION_VIOLATION_REP(i);
@@ -668,8 +650,6 @@ bool Theory::isFunction(Interpretation i)
   case REAL_IS_RAT:
   case REAL_IS_REAL:
 
-  case ARRAY_BOOL_SELECT:
-
     return false;
 
   default:
@@ -723,7 +703,6 @@ bool Theory::hasSingleSort(Interpretation i)
   case REAL_TO_RAT:
 
   case ARRAY_SELECT:
-  case ARRAY_BOOL_SELECT:
   case ARRAY_STORE:
 
     return false;
@@ -741,7 +720,6 @@ bool Theory::isPolymorphic(Interpretation i)
   switch(i) {
   case EQUAL:
   case ARRAY_SELECT:
-  case ARRAY_BOOL_SELECT:
   case ARRAY_STORE:
 
     return true;
@@ -1017,47 +995,18 @@ bool Theory::partiallyDefinedFunctionUndefinedForArgs(Term* t) {
   }
 }
 
-
-/**
- * Get the number of the skolem function symbol used in the clause form of the
- * array extensionality axiom (of particular sort).
- *
- * select(X,sk(X,Y)) != select(Y,sk(X,Y)) | X = Y
- * 
- * If the symbol does not exist yet, it is added to the signature. We use 0 to
- * represent that the symbol not yet exists, assuming that at call time of this
- * method, at least the array function are already in the signature.
- *
- * We want to have this function available e.g. in simplification rules.
- */
-unsigned Theory::getArrayExtSkolemFunction(TermList sort) {
-  ASS(sort.isArraySort());
-
-  if(_arraySkolemFunctions.find(sort)){
-    return _arraySkolemFunctions.get(sort);
-  }
-
-  TermList indexSort = SortHelper::getIndexSort(sort);
-  TermList params[] = {sort, sort};
-  unsigned skolemFunction = Shell::Skolem::addSkolemFunction(2, 0, params, indexSort, "arrayDiff");
-
-  _arraySkolemFunctions.insert(sort,skolemFunction);
-
-  return skolemFunction; 
-}
-
-unsigned Theory::Tuples::getConstructor(unsigned arity)
+unsigned Theory::getTupleConstructor(unsigned arity)
 {
   return theory->getTupleTermAlgebra(arity)->constructor(0)->functor();
 }
 
-bool Theory::Tuples::isConstructor(Term* t)
+bool Theory::isTupleConstructor(Term* t)
 {
   return !t->isSpecial() && !t->isSort() && SortHelper::getResultSort(t).isTupleSort()
-    && getConstructor(t->numTypeArguments()) == t->functor();
+    && getTupleConstructor(t->numTypeArguments()) == t->functor();
 }
 
-unsigned Theory::Tuples::getProjectionFunctor(unsigned arity, unsigned proj)
+unsigned Theory::getTupleProjectionFunctor(unsigned arity, unsigned proj)
 {
   auto c = theory->getTupleTermAlgebra(arity)->constructor(0);
 
@@ -1067,7 +1016,7 @@ unsigned Theory::Tuples::getProjectionFunctor(unsigned arity, unsigned proj)
 }
 
 // TODO: replace with a constant time algorithm
-bool Theory::Tuples::findProjection(unsigned projFunctor, bool isPredicate, unsigned &proj) {
+bool Theory::findTupleProjection(unsigned projFunctor, bool isPredicate, unsigned &proj) {
   OperatorType* projType = isPredicate ? env.signature->getPredicate(projFunctor)->predType()
                                        : env.signature->getFunction(projFunctor)->fnType();
 
@@ -1241,7 +1190,6 @@ std::string Theory::getInterpretationName(Interpretation interp) {
     case REAL_CEILING:
       return "ceiling";
     case ARRAY_SELECT:
-    case ARRAY_BOOL_SELECT:
       return "$select";
     case ARRAY_STORE:
       return "$store";
@@ -1250,33 +1198,30 @@ std::string Theory::getInterpretationName(Interpretation interp) {
   }
 }
 
-OperatorType* Theory::getArrayOperatorType(TermList arraySort, Interpretation i) {
-  ASS(arraySort.isArraySort());
-
-  TermList indexSort = SortHelper::getIndexSort(arraySort);
-  TermList innerSort = SortHelper::getInnerSort(arraySort);
-
-  switch (i) {
-    case Interpretation::ARRAY_SELECT:
-      return OperatorType::getFunctionType({ arraySort, indexSort }, innerSort);
-
-    case Interpretation::ARRAY_BOOL_SELECT:
-      return OperatorType::getPredicateType({ arraySort, indexSort });
-
-    case Interpretation::ARRAY_STORE:
-      return OperatorType::getFunctionType({ arraySort, indexSort, innerSort }, arraySort);
-
-    default:
-      ASSERTION_VIOLATION;
-  }
-}
-
 /**
  * Return type of the function representing interpreted function/predicate @c i.
  */
-OperatorType* Theory::getNonpolymorphicOperatorType(Interpretation i)
-{
-  ASS(!isPolymorphic(i));
+OperatorType* Theory::getOperatorType(Interpretation i)
+{
+  // Equality is of predicate type with two arguments.
+  // Note that equality is treated specially as monomorphic,
+  // as deducing the actual arguments types from the arguments
+  // (except for two variable equalities where the type argument
+  // is stored as an extra in the Literal).
+  if (i == Interpretation::EQUAL) {
+    return OperatorType::getPredicateType(2);
+  }
+
+  // Array operators have two type arguments, index type and element type
+  if (i == Interpretation::ARRAY_SELECT || i == Interpretation::ARRAY_STORE) {
+    auto indexSort = TermList::var(0);
+    auto innerSort = TermList::var(1);
+    TermList arraySort(AtomicSort::create2(env.signature->getArrayConstructor(), indexSort, innerSort));
+    if (i == Interpretation::ARRAY_SELECT) {
+      return OperatorType::getFunctionType({ arraySort, indexSort }, innerSort, /*taArity=*/2);
+    }
+    return OperatorType::getFunctionType({ arraySort, indexSort, innerSort }, arraySort, /*taArity=*/2);
+  }
 
   if (isConversionOperation(i)) {
     return getConversionOperationType(i);
@@ -1697,7 +1642,6 @@ std::ostream& operator<<(std::ostream& out, Kernel::Theory::Interpretation const
     case Kernel::Theory::REAL_TO_RAT: return out << "REAL_TO_RAT";
     case Kernel::Theory::REAL_TO_REAL: return out << "REAL_TO_REAL";
     case Kernel::Theory::ARRAY_SELECT: return out << "ARRAY_SELECT";
-    case Kernel::Theory::ARRAY_BOOL_SELECT: return out << "ARRAY_BOOL_SELECT";
     case Kernel::Theory::ARRAY_STORE: return out << "ARRAY_STORE";
     case Kernel::Theory::INVALID_INTERPRETATION: return out << "INVALID_INTERPRETATION";
   }
diff --git a/Kernel/Theory.hpp b/Kernel/Theory.hpp
index 7fe876f1a..1f5de62d8 100644
--- a/Kernel/Theory.hpp
+++ b/Kernel/Theory.hpp
@@ -20,7 +20,6 @@
 #include "Forwards.hpp"
 #include "OperatorType.hpp"
 
-#include "Lib/DHMap.hpp"
 #include "Lib/Exception.hpp"
 #include "Lib/Reflection.hpp"
 
@@ -480,55 +479,17 @@ class Theory
 
     // array functions
     ARRAY_SELECT,
-    ARRAY_BOOL_SELECT,
     ARRAY_STORE,
 
     INVALID_INTERPRETATION // LEAVE THIS AS THE LAST ELEMENT OF THE ENUM
   };
 
-  enum IndexedInterpretation {
-    FOR_NOW_EMPTY
-  };
-
-  typedef std::pair<IndexedInterpretation, unsigned> ConcreteIndexedInterpretation;
-
-  /**
-   * Interpretations represent the abstract concept of an interpreted operation vampire knows about.
-   *
-   * Some of them are polymorphic, such the ones for ARRAYs, and only become a concrete operation when supplied with OperatorType*.
-   * To identify these, MonomorphisedInterpretation (see below) can be used. However, notice that the appropriate Symbol always carries
-   * an Interpretation (if interpreted) and an OperatorType*.
-   *
-   * Other operations might be, in fact, indexed families of operations, and need an additional index (unsigned) to be specified.
-   * To keep the Symbol structure from growing for their sake, these IndexedInterpretations are instantiated to a concrete member of a family on demand
-   * and we keep track of this instantiation in _indexedInterpretations (see below). Members of _indexedInterpretations
-   * implicitly "inhabit" a range of values in Interpretation after INVALID_INTERPRETATION, so that again an
-   * Interpretation (this time >= INVALID_INTERPRETATION) and an OperatorType* are enough to identify a member of an indexed family.
-   */
-
-  typedef std::pair<Interpretation, OperatorType*> MonomorphisedInterpretation;
-
-private:
-  DHMap<ConcreteIndexedInterpretation,Interpretation> _indexedInterpretations;
-
 public:
 
   static unsigned numberOfFixedInterpretations() {
     return INVALID_INTERPRETATION;
   }
 
-  Interpretation interpretationFromIndexedInterpretation(IndexedInterpretation ii, unsigned index)
-  {
-    ConcreteIndexedInterpretation cii = std::make_pair(ii,index);
-
-    Interpretation res;
-    if (!_indexedInterpretations.find(cii, res)) {
-      res = static_cast<Interpretation>(numberOfFixedInterpretations() + _indexedInterpretations.size());
-      _indexedInterpretations.insert(cii, res);
-    }
-    return res;
-  }
-
   static bool isPlus(Interpretation i){
     return i == INT_PLUS || i == RAT_PLUS || i == REAL_PLUS;
   }
@@ -537,9 +498,7 @@ class Theory
   static unsigned getArity(Interpretation i);
   static bool isFunction(Interpretation i);
   static bool isInequality(Interpretation i);
-  static OperatorType* getNonpolymorphicOperatorType(Interpretation i);
-
-  static OperatorType* getArrayOperatorType(TermList arraySort, Interpretation i);
+  static OperatorType* getOperatorType(Interpretation i);
 
   static bool hasSingleSort(Interpretation i);
   static TermList getOperationSort(Interpretation i);
@@ -548,12 +507,9 @@ class Theory
   static bool isNonLinearOperation(Interpretation i);
   bool isPartiallyInterpretedFunction(Term* t);
   bool partiallyDefinedFunctionUndefinedForArgs(Term* t);
-  // static bool isPartialFunction(Interpretation i);
 
   static bool isPolymorphic(Interpretation i);
 
-  unsigned getArrayExtSkolemFunction(TermList sort);
-
   static Theory theory_obj;
   static Theory* instance();
 
@@ -586,7 +542,6 @@ class Theory
   bool isInterpretedFunction(Term* t, Interpretation itp);
   bool isInterpretedFunction(TermList t, Interpretation itp);
 
-  // bool isInterpretedPartialFunction(unsigned func);
   bool isZero(TermList t);
 
   Interpretation interpretFunction(unsigned func);
@@ -642,22 +597,14 @@ class Theory
   Term* representConstant(const RealConstantType& num);
 
 private:
-  Theory();
+  Theory() = default;
   static OperatorType* getConversionOperationType(Interpretation i);
 
-  DHMap<TermList,unsigned> _arraySkolemFunctions;
-
 public:
-  class Tuples {
-  public:
-    bool isConstructor(Term* t);
-    unsigned getConstructor(unsigned arity);
-    unsigned getProjectionFunctor(unsigned arity, unsigned proj);
-    bool findProjection(unsigned projFunctor, bool isPredicate, unsigned &proj);
-  };
-
-  static Theory::Tuples tuples_obj;
-  static Theory::Tuples* tuples();
+  static bool isTupleConstructor(Term* t);
+  static unsigned getTupleConstructor(unsigned arity);
+  static unsigned getTupleProjectionFunctor(unsigned arity, unsigned proj);
+  static bool findTupleProjection(unsigned projFunctor, bool isPredicate, unsigned &proj);
 };
 
 #define ANY_INTERPRETED_PREDICATE                                                         \
@@ -683,7 +630,6 @@ class Theory
     case Kernel::Theory::REAL_GREATER:                                                    \
     case Kernel::Theory::REAL_GREATER_EQUAL:                                              \
     case Kernel::Theory::REAL_LESS:                                                       \
-    case Kernel::Theory::ARRAY_BOOL_SELECT:                                               \
     case Kernel::Theory::REAL_LESS_EQUAL
 
 #define ANY_INTERPRETED_FUNCTION                                                          \
diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp
index 7f45b67cc..99a5cfe03 100644
--- a/Parse/SMTLIB2.cpp
+++ b/Parse/SMTLIB2.cpp
@@ -2318,21 +2318,12 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const std::string& id, LExpr* exp)
         complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
       }
 
-      if (SortHelper::getInnerSort(arraySortIdx)== AtomicSort::boolSort()) {
-        OperatorType* predType = Theory::getArrayOperatorType(arraySortIdx,Theory::ARRAY_BOOL_SELECT);
-        unsigned pred = env.signature->getInterpretingSymbol(Theory::ARRAY_BOOL_SELECT,predType);
+      auto indexSort = SortHelper::getIndexSort(arraySortIdx);
+      auto innerSort = SortHelper::getInnerSort(arraySortIdx);
 
-        Formula* res = new AtomicFormula(Literal::create2(pred,true,theArray,theIndex));
-
-        _results.push(ParseResult(res));
-      } else {
-        OperatorType* funType = Theory::getArrayOperatorType(arraySortIdx,Theory::ARRAY_SELECT);
-        unsigned fun = env.signature->getInterpretingSymbol(Theory::ARRAY_SELECT,funType);
-
-        TermList res = TermList(Term::create2(fun,theArray,theIndex));
-
-        _results.push(ParseResult(SortHelper::getInnerSort(arraySortIdx),res));
-      }
+      TermList res(Term::create(env.signature->getInterpretingSymbol(Theory::ARRAY_SELECT),
+        { indexSort, innerSort, theArray, theIndex }));
+      _results.push(ParseResult(innerSort,res));
 
       return true;
     }
@@ -2359,11 +2350,13 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const std::string& id, LExpr* exp)
         complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
       }
 
-      OperatorType* funType = Theory::getArrayOperatorType(arraySortIdx,Theory::ARRAY_STORE);
-      unsigned fun = env.signature->getInterpretingSymbol(Theory::ARRAY_STORE,funType);
+      unsigned fun = env.signature->getInterpretingSymbol(Theory::ARRAY_STORE);
+
+      auto indexSort = SortHelper::getIndexSort(arraySortIdx);
+      auto innerSort = SortHelper::getInnerSort(arraySortIdx);
 
-      TermList args[] = {theArray, theIndex, theValue};
-      TermList res = TermList(Term::create(fun, 3, args));
+      TermList res(Term::create(fun,
+        { indexSort, innerSort, theArray, theIndex, theValue }));
 
       _results.push(ParseResult(arraySortIdx,res));
 
diff --git a/Parse/TPTP.cpp b/Parse/TPTP.cpp
index 776e8f2e0..c699d8bc5 100644
--- a/Parse/TPTP.cpp
+++ b/Parse/TPTP.cpp
@@ -1964,7 +1964,7 @@ void TPTP::endTheoryFunction() {
    */
 
   Theory::Interpretation itp;
-  TermList args[3]; // all theory function use up to 3 arguments as for now
+  TermList args[5]; // all theory function use up to 5 arguments as for now
   TermList arraySort;
 
   TheoryFunction tf = _theoryFunctions.pop();
@@ -1983,14 +1983,12 @@ void TPTP::endTheoryFunction() {
         USER_ERROR("sort of index is not the same as the index sort of the array");
       }
 
-      args[0] = array;
-      args[1] = index;
+      args[0] = indexSort;
+      args[1] = SortHelper::getInnerSort(arraySort);
+      args[2] = array;
+      args[3] = index;
 
-      if (SortHelper::getInnerSort(arraySort) == AtomicSort::boolSort()) {
-        itp = Theory::Interpretation::ARRAY_BOOL_SELECT;
-      } else {
-        itp = Theory::Interpretation::ARRAY_SELECT;
-      }
+      itp = Theory::Interpretation::ARRAY_SELECT;
       break;
     }
     case TF_STORE: {
@@ -2013,20 +2011,20 @@ void TPTP::endTheoryFunction() {
         USER_ERROR("sort of value is not the same as the value sort of the array");
       }
 
-      args[0] = array;
-      args[1] = index;
-      args[2] = value;
+      args[0] = indexSort;
+      args[1] = innerSort;
+      args[2] = array;
+      args[3] = index;
+      args[4] = value;
 
       itp = Theory::Interpretation::ARRAY_STORE;
-
       break;
     }
     default:
       ASSERTION_VIOLATION_REP(tf);
   }
 
-  OperatorType* type = Theory::getArrayOperatorType(arraySort,itp);
-  unsigned symbol = env.signature->getInterpretingSymbol(itp, type);
+  unsigned symbol = env.signature->getInterpretingSymbol(itp);
   unsigned arity = Theory::getArity(itp);
 
   if (Theory::isFunction(itp)) {
@@ -2594,7 +2592,7 @@ void TPTP::tupleDefinition()
     }
   } while (true);
 
-  auto tupleFunctor = Theory::tuples()->getConstructor(sorts.size());
+  auto tupleFunctor = Theory::getTupleConstructor(sorts.size());
 
   LetDefinitions definitions = _letDefinitions.pop();
   // TODO tuple $lets probably also need adjusting with polymorphic (implicit) types
@@ -2756,7 +2754,7 @@ void TPTP::endTuple()
     args[i] = sortOf(ts);
   }
 
-  auto t =  Term::create(Theory::tuples()->getConstructor(arity), 2*arity, args.begin());
+  auto t =  Term::create(Theory::getTupleConstructor(arity), 2*arity, args.begin());
   _termLists.push(TermList(t));
 } // endTuple
 
diff --git a/SAT/Z3Interfacing.cpp b/SAT/Z3Interfacing.cpp
index 52e5314b3..f6df245cb 100644
--- a/SAT/Z3Interfacing.cpp
+++ b/SAT/Z3Interfacing.cpp
@@ -1623,7 +1623,6 @@ z3::expr Z3Interfacing::getRepresentation(Term* trm)
           if (Theory::isPolymorphic(interp)) {
             switch(interp){
               case Theory::ARRAY_SELECT:
-              case Theory::ARRAY_BOOL_SELECT:
                 // select(array,index)
                 return select(args[0],args[1]);
 
diff --git a/Shell/FOOLElimination.cpp b/Shell/FOOLElimination.cpp
index 3c3cd5246..fa36b6860 100644
--- a/Shell/FOOLElimination.cpp
+++ b/Shell/FOOLElimination.cpp
@@ -595,7 +595,7 @@ void FOOLElimination::process(Term* term, Context context, TermList& termResult,
         auto bindingLhs = blit->termArg(0).term();
         auto bindingRhs = blit->termArg(1);
 
-        if (Theory::tuples()->isConstructor(bindingLhs)) {
+        if (Theory::isTupleConstructor(bindingLhs)) {
           NOT_IMPLEMENTED;
         }
 
diff --git a/Shell/InterpretedNormalizer.cpp b/Shell/InterpretedNormalizer.cpp
index 1695f4c75..54bc1bc5b 100644
--- a/Shell/InterpretedNormalizer.cpp
+++ b/Shell/InterpretedNormalizer.cpp
@@ -281,7 +281,7 @@ class InterpretedNormalizer::NLiteralTransformer : public BottomUpTermTransforme
    */
   void addMinusTransformer(Interpretation bMinus, Interpretation plus, Interpretation uMinus)
   {
-    if(!env.signature->haveInterpretingSymbol(bMinus)) {
+    if(!env.signature->hasInterpretingSymbol(bMinus)) {
       return; //the symbol to be transformed doesn't exist, so we don't need to worry
     }
     BinaryMinusTranslator* transl = new BinaryMinusTranslator(bMinus, plus, uMinus);
@@ -295,7 +295,7 @@ class InterpretedNormalizer::NLiteralTransformer : public BottomUpTermTransforme
    */
   void addSuccessorTransformer()
   {
-    if(!env.signature->haveInterpretingSymbol(Theory::INT_SUCCESSOR)) {
+    if(!env.signature->hasInterpretingSymbol(Theory::INT_SUCCESSOR)) {
       return; //the symbol to be transformed doesn't exist, so we don't need to worry
     }
     SuccessorTranslator* transl = new SuccessorTranslator();
@@ -309,7 +309,7 @@ class InterpretedNormalizer::NLiteralTransformer : public BottomUpTermTransforme
    */
   void addRoundingFunctionTransformer(Interpretation origF, Interpretation newF, Interpretation roundF)
   {
-    if(!env.signature->haveInterpretingSymbol(origF)) {
+    if(!env.signature->hasInterpretingSymbol(origF)) {
       return; //the symbol to be transformed doesn't exist, so we don't need to worry
     }
     RoundingFunctionTranslator* transl = new RoundingFunctionTranslator(origF,newF,roundF);
@@ -325,7 +325,7 @@ class InterpretedNormalizer::NLiteralTransformer : public BottomUpTermTransforme
    */
   void addIneqTransformer(Interpretation from, Interpretation to, bool swapArguments, bool reversePolarity)
   {
-    if(!env.signature->haveInterpretingSymbol(from)) {
+    if(!env.signature->hasInterpretingSymbol(from)) {
       return; //the symbol to be transformed doesn't exist, so we don't need to worry
     }
     IneqTranslator* transl = new IneqTranslator(from, to, swapArguments, reversePolarity);
diff --git a/Shell/NewCNF.cpp b/Shell/NewCNF.cpp
index 9c2f6daba..06f11f114 100644
--- a/Shell/NewCNF.cpp
+++ b/Shell/NewCNF.cpp
@@ -329,9 +329,9 @@ TermList NewCNF::findITEs(TermList ts, Stack<unsigned> &variables, Stack<Formula
     }
 
     unsigned proj;
-    if (Theory::tuples()->findProjection(term->functor(), false, proj)) {
+    if (Theory::findTupleProjection(term->functor(), false, proj)) {
       TermList* arg = arguments.begin();
-      if (arg->isTerm() && Theory::tuples()->isConstructor(arg->term())) {
+      if (arg->isTerm() && Theory::isTupleConstructor(arg->term())) {
         return *arg->term()->nthArgument(proj);
       }
     }
@@ -673,11 +673,11 @@ TermList NewCNF::eliminateLet(Term* term)
   auto bindingLhs = binding->literal()->termArg(0).term();
   auto bindingRhs = binding->literal()->termArg(1);
 
-  if (Theory::tuples()->isConstructor(bindingLhs)) {
+  if (Theory::isTupleConstructor(bindingLhs)) {
 
     TermList bodySort = sd->getSort();
 
-    if (bindingRhs.isTerm() && Theory::tuples()->isConstructor(bindingRhs.term())) {
+    if (bindingRhs.isTerm() && Theory::isTupleConstructor(bindingRhs.term())) {
       // binding of the form $let([x, y, z, ...] := [a, b, c, ...], ...) is processed
       // as $let(x := a, $let(y := b, $let(z := c, ...)))
 
@@ -708,7 +708,7 @@ TermList NewCNF::eliminateLet(Term* term)
           auto lhs = arg.term();
           ASS_EQ(lhs->numTermArguments(), 0);
 
-          unsigned projFunctor = Theory::tuples()->getProjectionFunctor(arity, i);
+          unsigned projFunctor = Theory::getTupleProjectionFunctor(arity, i);
           Term* projectedArgument = lhs->isBoolean()
             ? Term::createFormula(new AtomicFormula(Literal::create(projFunctor, args.size(), /*polarity*/true, args.begin())))
             : Term::create(projFunctor, args);
diff --git a/Shell/Property.cpp b/Shell/Property.cpp
index 666933a06..88bd4c8c7 100644
--- a/Shell/Property.cpp
+++ b/Shell/Property.cpp
@@ -16,6 +16,7 @@
  */
 
 
+#include "Kernel/Theory.hpp"
 #include "Lib/Int.hpp"
 #include "Lib/Environment.hpp"
 
@@ -773,16 +774,19 @@ void Property::scanForInterpreted(Term* t)
     _interpretationPresence[itp] = true;
   }
 
-  if(Theory::isConversionOperation(itp)){
-    addProp(PR_NUMBER_CONVERSION);
+  // TODO check whether this is enough for equality
+  if (itp == Interpretation::EQUAL) {
     return;
   }
 
-  if (Theory::isPolymorphic(itp)) {
-    OperatorType* type = t->isLiteral() ?
-        env.signature->getPredicate(t->functor())->predType() : env.signature->getFunction(t->functor())->fnType();
+  if (itp == Interpretation::ARRAY_SELECT || itp == Interpretation::ARRAY_STORE) {
+    // TODO this could be separated into store and select
+    addProp(PR_HAS_ARRAYS);
+    return;
+  }
 
-    _polymorphicInterpretations.insert(std::make_pair(itp,type));
+  if(Theory::isConversionOperation(itp)){
+    addProp(PR_NUMBER_CONVERSION);
     return;
   }
 
diff --git a/Shell/Property.hpp b/Shell/Property.hpp
index 46417936c..f3fef15f7 100644
--- a/Shell/Property.hpp
+++ b/Shell/Property.hpp
@@ -204,9 +204,6 @@ class Property
     if(i >= _interpretationPresence.size()){ return false; }
     return _interpretationPresence[i];
   }
-  bool hasInterpretedOperation(Interpretation i, OperatorType* type) const {
-    return _polymorphicInterpretations.find(std::make_pair(i,type));
-  }
 
   /** Problem contains an interpreted symbol excluding equality */
   bool hasInterpretedOperations() const { return _hasInterpreted; }
@@ -324,10 +321,6 @@ class Property
    *  the more precise information about which monomorphisations are present (see below).
    */
   DArray<bool> _interpretationPresence;
-  DHSet<Theory::MonomorphisedInterpretation> _polymorphicInterpretations;
-
-
-
 
   bool _hasFOOL;
   bool _hasArrowSort;
diff --git a/Shell/SMTCheck.cpp b/Shell/SMTCheck.cpp
index b71640218..76f2fa305 100644
--- a/Shell/SMTCheck.cpp
+++ b/Shell/SMTCheck.cpp
@@ -197,7 +197,6 @@ static std::ostream &operator<<(std::ostream &out, FunctionName name) {
   case Theory::INT_CEILING:
     ASSERTION_VIOLATION
   case Theory::ARRAY_SELECT:
-  case Theory::ARRAY_BOOL_SELECT:
   case Theory::ARRAY_STORE:
     NOT_IMPLEMENTED;
   case Theory::INVALID_INTERPRETATION:
@@ -308,7 +307,6 @@ static std::ostream &operator<<(std::ostream &out, PredicateName name) {
   case Theory::REAL_TO_RAT:
   case Theory::REAL_TO_REAL:
   case Theory::ARRAY_SELECT:
-  case Theory::ARRAY_BOOL_SELECT:
   case Theory::ARRAY_STORE:
     // should be predicates, not functions
     ASSERTION_VIOLATION
diff --git a/Shell/TheoryAxioms.cpp b/Shell/TheoryAxioms.cpp
index 0dc16b431..0b9dd04fd 100644
--- a/Shell/TheoryAxioms.cpp
+++ b/Shell/TheoryAxioms.cpp
@@ -14,7 +14,6 @@
 
 #include "Lib/Environment.hpp"
 #include "Lib/Stack.hpp"
-#include "Lib/DHSet.hpp"
 
 #include "Kernel/Clause.hpp"
 #include "Kernel/Formula.hpp"
@@ -24,12 +23,10 @@
 #include "Kernel/Signature.hpp"
 #include "Kernel/Term.hpp"
 #include "Kernel/Theory.hpp"
-#include "Kernel/SortHelper.hpp"
 #include "Kernel/NumTraits.hpp"
 
-#include "Indexing/TermSharing.hpp"
-
 #include "Property.hpp"
+#include "Skolem.hpp"
 #include "SymCounter.hpp"
 #include "TheoryAxioms.hpp"
 #include "Options.hpp"
@@ -796,7 +793,7 @@ void TheoryAxioms::addTruncateAxioms(Interpretation truncate, Interpretation les
 
 /**
  * Adds the extensionality axiom of arrays (of type array1 or array2): 
- * select(X,sk(X,Y)) != select(Y,sk(X,Y)) | X = Y
+ * select_{a,b}(X,sk_{a,b}(X,Y)) != select_{a,b}(Y,sk_{a,b}(X,Y)) | X = Y
  *
  * @author Laura Kovacs
  * @since 31/08/2012, Vienna
@@ -805,136 +802,62 @@ void TheoryAxioms::addTruncateAxioms(Interpretation truncate, Interpretation les
  * @since 05/01/2014 Vienna, add axiom in clause form (we need skolem function in other places)
  * @author Bernhard Kragl
 */
-void TheoryAxioms::addArrayExtensionalityAxioms(TermList arraySort, unsigned skolemFn)
+void TheoryAxioms::addArrayExtensionalityAxioms()
 {
-  unsigned sel = env.signature->getInterpretingSymbol(Theory::ARRAY_SELECT,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_SELECT));
+  unsigned sel = env.signature->getInterpretingSymbol(Kernel::Theory::ARRAY_SELECT);
 
-  TermList rangeSort = SortHelper::getInnerSort(arraySort);
+  auto indexSort = TermList::var(0);
+  auto innerSort = TermList::var(1);
+  auto x         = TermList::var(2);
+  auto y         = TermList::var(3);
 
-  TermList x(0,false);
-  TermList y(1,false);
+  TermList arraySort(AtomicSort::create2(env.signature->getArrayConstructor(), indexSort, innerSort));
+  TermStack args { arraySort, arraySort };
+  auto skolemFn = Skolem::addSkolemFunction(4, 2, args.begin(), indexSort, "arrayDiff");
 
-  TermList sk(Term::create2(skolemFn, x, y)); //sk(x,y)
-  TermList sel_x_sk(Term::create2(sel,x,sk)); //select(x,sk(x,y))
-  TermList sel_y_sk(Term::create2(sel,y,sk)); //select(y,sk(x,y))
-  Literal* eq = Literal::createEquality(true,x,y,arraySort); //x = y
-  Literal* ineq = Literal::createEquality(false,sel_x_sk,sel_y_sk,rangeSort); //select(x,sk(x,y) != select(y,z)
+  TermList sk(Term::create(skolemFn, { indexSort, innerSort, x, y })); //sk(x,y)
+  TermList sel_x_sk(Term::create(sel, { indexSort, innerSort, x, sk })); //select(x,sk(x,y))
+  TermList sel_y_sk(Term::create(sel, { indexSort, innerSort, y, sk })); //select(y,sk(x,y))
+  Literal* eq = Literal::createEquality(true, x, y, arraySort); //x = y
+  Literal* ineq = Literal::createEquality(false, sel_x_sk, sel_y_sk, innerSort); //select(x,sk(x,y) != select(y,z)
 
-  addTheoryClauseFromLits({eq,ineq}, InferenceRule::THA_ARRAY_EXTENSIONALITY, EXPENSIVE);
+  addTheoryClauseFromLits({eq, ineq}, InferenceRule::THA_ARRAY_EXTENSIONALITY, EXPENSIVE);
 } // addArrayExtensionalityAxiom
 
-/**
- * Adds the extensionality axiom of boolean arrays:
- * select(X, sk(X, Y)) <~> select(Y, sk(X, Y)) | X = Y
- *
- * @since 25/08/2015 Gothenburg
- * @author Evgeny Kotelnikov
- */
-void TheoryAxioms::addBooleanArrayExtensionalityAxioms(TermList arraySort, unsigned skolemFn)
-{
-  OperatorType* selectType = Theory::getArrayOperatorType(arraySort,Theory::ARRAY_BOOL_SELECT);
-
-  unsigned sel = env.signature->getInterpretingSymbol(Theory::ARRAY_BOOL_SELECT,selectType);
-
-  TermList x(0,false);
-  TermList y(1,false);
-
-  TermList sk(Term::create2(skolemFn, x, y)); //sk(x,y)
-  Formula* x_neq_y = new AtomicFormula(Literal::createEquality(false,x,y,arraySort)); //x != y
-
-  Formula* sel_x_sk = new AtomicFormula(Literal::create2(sel, true, x, sk)); //select(x,sk(x,y))
-  Formula* sel_y_sk = new AtomicFormula(Literal::create2(sel, true, y, sk)); //select(y,sk(x,y))
-  Formula* sx_neq_sy = new BinaryFormula(XOR, sel_x_sk, sel_y_sk); //select(x,sk(x,y)) <~> select(y,sk(x,y))
-
-  Formula* axiom = new QuantifiedFormula(FORALL, VList::cons(0, VList::cons(1, VList::empty())),
-                                         SList::cons(arraySort, SList::cons(arraySort,SList::empty())),
-                                         new BinaryFormula(IMP, x_neq_y, sx_neq_sy));
-
-  addAndOutputTheoryUnit(new FormulaUnit(axiom, TheoryAxiom(InferenceRule::THA_BOOLEAN_ARRAY_EXTENSIONALITY)),EXPENSIVE);
-} // addBooleanArrayExtensionalityAxiom
-
 /**
 * Adds the write/select axiom of arrays (of type array1 or array2),
  * @author Laura Kovacs
  * @since 31/08/2012, Vienna
 */
-void TheoryAxioms::addArrayWriteAxioms(TermList arraySort)
+void TheoryAxioms::addArrayWriteAxioms()
 {
-  unsigned func_select = env.signature->getInterpretingSymbol(Theory::ARRAY_SELECT,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_SELECT));
-  unsigned func_store = env.signature->getInterpretingSymbol(Theory::ARRAY_STORE,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_STORE));
-
-  TermList rangeSort = SortHelper::getInnerSort(arraySort);
-  TermList domainSort = SortHelper::getIndexSort(arraySort);
-
-  TermList i(0,false);
-  TermList j(1,false);
-  TermList v(2,false);
-  TermList a(3,false);
-  TermList args[] = {a, i, v};
-
-  //axiom (!A: arraySort, !I:domainSort, !V:rangeSort: (select(store(A,I,V), I) = V
-  TermList wAIV(Term::create(func_store, 3, args)); //store(A,I,V)
-  TermList sWI(Term::create2(func_select, wAIV,i)); //select(wAIV,I)
-  Literal* ax = Literal::createEquality(true, sWI, v, rangeSort);
+  unsigned func_select = env.signature->getInterpretingSymbol(Kernel::Theory::ARRAY_SELECT);
+  unsigned func_store = env.signature->getInterpretingSymbol(Kernel::Theory::ARRAY_STORE);
+
+  auto indexSort = TermList::var(0);
+  auto innerSort = TermList::var(1);
+  auto i = TermList::var(2);
+  auto j = TermList::var(3);
+  auto v = TermList::var(4);
+  auto a = TermList::var(5);
+
+  TermList arraySort(AtomicSort::create2(env.signature->getArrayConstructor(), indexSort, innerSort));
+
+  //axiom (!A: arraySort, !I:indexSort, !V:innerSort: (select(store(A,I,V), I) = V
+  TermList wAIV(Term::create(func_store, { indexSort, innerSort, a, i, v })); //store(A,I,V)
+  TermList sWI(Term::create(func_select, { indexSort, innerSort, wAIV, i })); //select(wAIV,I)
+  auto ax = Literal::createEquality(true, sWI, v, innerSort);
   addTheoryClauseFromLits({ax}, InferenceRule::THA_ARRAY_WRITE1, CHEAP);
 
-  //axiom (!A: arraySort, !I,J:domainSort, !V:rangeSort: (I!=J)->(select(store(A,I,V), J) = select(A,J)
-  TermList sWJ(Term::create2(func_select, wAIV,j)); //select(wAIV,J)
-  TermList sAJ(Term::create2(func_select, a, j)); //select(A,J)
+  //axiom (!A: arraySort, !I,J:indexSort, !V:innerSort: (I!=J)->(select(store(A,I,V), J) = select(A,J)
+  TermList sWJ(Term::create(func_select, { indexSort, innerSort, wAIV, j })); //select(wAIV,J)
+  TermList sAJ(Term::create(func_select, { indexSort, innerSort, a, j })); //select(A,J)
 
-  Literal* indexEq = Literal::createEquality(true, i, j, domainSort);//!(!(I=J)) === I=J
-  Literal* writeEq = Literal::createEquality(true, sWJ, sAJ, rangeSort);//(select(store(A,I,V), J) = select(A,J)
+  Literal* indexEq = Literal::createEquality(true, i, j, indexSort);//!(!(I=J)) === I=J
+  Literal* writeEq = Literal::createEquality(true, sWJ, sAJ, innerSort);//(select(store(A,I,V), J) = select(A,J)
   addTheoryClauseFromLits({indexEq,writeEq}, InferenceRule::THA_ARRAY_WRITE2, CHEAP);
 } //
 
-/**
-* Adds the write/select axiom of arrays (of type array1 or array2),
- * @author Laura Kovacs
- * @since 31/08/2012, Vienna
-*/
-void TheoryAxioms::addBooleanArrayWriteAxioms(TermList arraySort)
-{
-  unsigned pred_select = env.signature->getInterpretingSymbol(Theory::ARRAY_BOOL_SELECT,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_BOOL_SELECT));
-  unsigned func_store = env.signature->getInterpretingSymbol(Theory::ARRAY_STORE,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_STORE));
-
-  TermList domainSort = SortHelper::getIndexSort(arraySort);
-
-  TermList a(0,false);
-  TermList i(1,false);
-
-  TermList false_(Term::foolFalse());
-  TermList true_(Term::foolTrue());
-
-  // select(store(A,I,$$true), I)
-  //~select(store(A,I,$$false), I)
-
-  for (TermList bval : {false_,true_}) {
-    TermList args[] = {a, i, bval};
-    TermList wAIV(Term::create(func_store, 3, args)); //store(A,I,bval)
-    Literal* lit = Literal::create2(pred_select, true, wAIV,i);
-    if (bval == false_) {
-      lit = Literal::complementaryLiteral(lit);
-    }
-    Formula* ax = new AtomicFormula(lit);
-    addAndOutputTheoryUnit(new FormulaUnit(ax, TheoryAxiom(InferenceRule::THA_BOOLEAN_ARRAY_WRITE1)),CHEAP);
-  }
-
-  TermList v(2,false);
-  TermList j(3,false);
-
-  TermList args[] = {a, i, v};
-
-  //axiom (!A: arraySort, !I,J:domainSort, !V:rangeSort: (I!=J)->(select(store(A,I,V), J) <=> select(A,J)
-  TermList wAIV(Term::create(func_store, 3, args)); //store(A,I,V)
-  Formula* sWJ = new AtomicFormula(Literal::create2(pred_select, true, wAIV,j)); //select(wAIV,J)
-  Formula* sAJ = new AtomicFormula(Literal::create2(pred_select, true, a, j)); //select(A,J)
-
-  Formula* indexEq = new AtomicFormula(Literal::createEquality(false, i, j, domainSort));//I!=J
-  Formula* writeEq = new BinaryFormula(IFF, sWJ, sAJ);//(select(store(A,I,V), J) <=> select(A,J)
-  Formula* ax2 = new BinaryFormula(IMP, indexEq, writeEq);
-  addAndOutputTheoryUnit(new FormulaUnit(ax2, TheoryAxiom(InferenceRule::THA_BOOLEAN_ARRAY_WRITE2)),CHEAP);
-} //
-
 //Axioms for integer division that hven't been implemented yet
 //
 //axiom( (ige(X0,zero) & igt(X1,zero)) --> ( ilt(X0-X1, idiv(X0,X1)*X1) & ile(idiv(X0,X1)*X1, X0) ) );
@@ -1105,34 +1028,17 @@ void TheoryAxioms::apply()
     }
   }
 
-  DHSet<TermList>* arraySorts = env.sharing->getArraySorts();
-  DHSet<TermList>::Iterator it(*arraySorts);
-  while(it.hasNext()){
-    TermList arraySort = it.next();
+  // TODO this should probably come from parsing the properties
+  // Check if they are used
+  bool haveSelect = prop->hasInterpretedOperation(Theory::ARRAY_SELECT);
+  bool haveStore = prop->hasInterpretedOperation(Theory::ARRAY_STORE);
 
-    bool isBool = SortHelper::getInnerSort(arraySort) == AtomicSort::boolSort();
-    
-    // Check if they are used
-    Interpretation arraySelect = isBool ? Theory::ARRAY_BOOL_SELECT : Theory::ARRAY_SELECT;
-    bool haveSelect = prop->hasInterpretedOperation(arraySelect,Theory::getArrayOperatorType(arraySort,arraySelect));
-    bool haveStore = prop->hasInterpretedOperation(Theory::ARRAY_STORE,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_STORE));
-
-    if (haveSelect || haveStore) {
-      unsigned sk = theory->getArrayExtSkolemFunction(arraySort);
-      if (isBool) {
-        addBooleanArrayExtensionalityAxioms(arraySort, sk);
-      } else {
-        addArrayExtensionalityAxioms(arraySort, sk);
-      }
-      if (haveStore) {
-        if (isBool) {
-          addBooleanArrayWriteAxioms(arraySort);
-        } else {
-          addArrayWriteAxioms(arraySort);
-        }
-      }
-      modified = true;
+  if (haveSelect || haveStore) {
+    addArrayExtensionalityAxioms();
+    if (haveStore) {
+      addArrayWriteAxioms();
     }
+    modified = true;
   }
 
   VirtualIterator<TermAlgebra*> tas = env.signature->termAlgebrasIterator();
diff --git a/Shell/TheoryAxioms.hpp b/Shell/TheoryAxioms.hpp
index 2aa6d311e..ab498c755 100644
--- a/Shell/TheoryAxioms.hpp
+++ b/Shell/TheoryAxioms.hpp
@@ -81,13 +81,8 @@ class TheoryAxioms {
   friend struct AlascaAxioms;
   void addAlascaAxioms();
 
-  /**
-   * TODO: we should have polymorphic array axioms only!
-   **/
-  void addBooleanArrayExtensionalityAxioms(TermList arraySort, unsigned skolem);
-  void addArrayExtensionalityAxioms(TermList arraySort, unsigned skolem);
-  void addBooleanArrayWriteAxioms(TermList arraySort);
-  void addArrayWriteAxioms(TermList arraySort);
+  void addArrayExtensionalityAxioms();
+  void addArrayWriteAxioms();
 
   void addFloorAxioms(Interpretation floor, Interpretation less, Interpretation unaryMinus,
                       Interpretation plus, TermList oneElement);
diff --git a/Shell/UIHelper.cpp b/Shell/UIHelper.cpp
index 40a22c6a4..e03377884 100644
--- a/Shell/UIHelper.cpp
+++ b/Shell/UIHelper.cpp
@@ -653,7 +653,7 @@ void UIHelper::outputSymbolTypeDeclarationIfNeeded(std::ostream& out, bool funct
   }
 
   unsigned dummy;
-  if (!typeCon && Theory::tuples()->findProjection(symNumber, !function, dummy)) {
+  if (!typeCon && Theory::findTupleProjection(symNumber, !function, dummy)) {
     return;
   }
 
diff --git a/checks/sanity b/checks/sanity
index 9febb7fdd..677cab251 100755
--- a/checks/sanity
+++ b/checks/sanity
@@ -78,13 +78,17 @@ check_szs_status Unsatisfiable term-algebra/terms_distinct.smt2
 check_szs_status Unsatisfiable -tac axiom term-algebra/terms_acyclic.smt2
 
 # FOOL
-check_szs_status Theorem fool/let-function.p
-check_szs_status Theorem -newcnf on fool/let-function.p
-check_szs_status Theorem -newcnf on fool/let-tuple.p
-check_szs_status Theorem -newcnf on fool/let-tuple-bool.p
-check_szs_status Theorem -newcnf on -ile off fool/let-function.p
-check_szs_status Theorem -newcnf on -ile off fool/let-tuple.p
-check_szs_status Theorem -newcnf on -ile off fool/let-tuple-bool.p
+check_szs_status Theorem theory/let-function.p
+check_szs_status Theorem -newcnf on theory/let-function.p
+check_szs_status Theorem -newcnf on theory/let-tuple.p
+check_szs_status Theorem -newcnf on theory/let-tuple-bool.p
+check_szs_status Theorem -newcnf on -ile off theory/let-function.p
+check_szs_status Theorem -newcnf on -ile off theory/let-tuple.p
+check_szs_status Theorem -newcnf on -ile off theory/let-tuple-bool.p
+
+# Arrays
+check_szs_status Unsatisfiable theory/arrays.smt2
+check_szs_status Unsatisfiable -newcnf on theory/arrays.smt2
 
 # Integer induction problems
 check_szs_status Unsatisfiable -ind int induction/int_invariant_infinite_geq3_val3.smt2
diff --git a/checks/theory/arrays.smt2 b/checks/theory/arrays.smt2
new file mode 100644
index 000000000..f084435cf
--- /dev/null
+++ b/checks/theory/arrays.smt2
@@ -0,0 +1,13 @@
+
+(declare-sort S 0)
+
+(assert (not
+  (forall ((arr (Array Int S)) (a S) (b S) (i Int))
+    (=>
+      (forall ((i Int)) (= (select arr i) a))
+      (forall ((i Int) (j Int))
+        (and
+          (= (select (store (store arr (+ i 1) b) (- i 1) b) i) a)
+          (=> (= i j) (= (select (store arr i b) j) b))
+        ))
+    ))))
diff --git a/checks/fool/let-function.p b/checks/theory/let-function.p
similarity index 100%
rename from checks/fool/let-function.p
rename to checks/theory/let-function.p
diff --git a/checks/fool/let-tuple-bool.p b/checks/theory/let-tuple-bool.p
similarity index 100%
rename from checks/fool/let-tuple-bool.p
rename to checks/theory/let-tuple-bool.p
diff --git a/checks/fool/let-tuple.p b/checks/theory/let-tuple.p
similarity index 100%
rename from checks/fool/let-tuple.p
rename to checks/theory/let-tuple.p