diff --git a/Kernel/InterpretedLiteralEvaluator.cpp b/Kernel/InterpretedLiteralEvaluator.cpp
index 48b4ed6bd3..91820cd66f 100644
--- a/Kernel/InterpretedLiteralEvaluator.cpp
+++ b/Kernel/InterpretedLiteralEvaluator.cpp
@@ -281,13 +281,6 @@ class InterpretedLiteralEvaluator::TypedEvaluator : public Evaluator
   virtual bool canEvaluate(Interpretation interp)
   {
     CALL("InterpretedLiteralEvaluator::TypedEvaluator::canEvaluate");
-
-    //only interpreted operations with non-single argument sort are array operations
-    if (theory->isArrayOperation(interp))
-    {
-        unsigned opSort = theory->getArrayOperationSort(interp);
-        return opSort==T::getSort();
-    }
     
     // This is why we cannot evaluate Equality here... we cannot determine its sort
     if (!theory->hasSingleSort(interp)) { return false; } //To skip conversions and EQUAL
diff --git a/Kernel/Signature.cpp b/Kernel/Signature.cpp
index b09bb069f7..39ed6d77ca 100644
--- a/Kernel/Signature.cpp
+++ b/Kernel/Signature.cpp
@@ -261,69 +261,6 @@ Signature::~Signature ()
   }
 } // Signature::~Signature
 
-/**
- * Add interpreted function
- */
-unsigned Signature::addInterpretedFunction(Interpretation interpretation, const vstring& name)
-{
-  CALL("Signature::addInterpretedFunction");
-  ASS(Theory::isFunction(interpretation));
-
-  unsigned res;
-  if (_iSymbols.find(interpretation,res)) { // already declared
-    if (name!=functionName(res)) {
-      USER_ERROR("Interpreted function '"+functionName(res)+"' has the same interpretation as '"+name+"' should have");
-    }
-    return res;
-  }
-
-  vstring symbolKey = name+"_i"+Int::toString(interpretation);
-  ASS(!_funNames.find(symbolKey));
-
-  unsigned fnNum = _funs.length();
-  InterpretedSymbol* sym = new InterpretedSymbol(name, interpretation);
-  _funs.push(sym);
-  _funNames.insert(symbolKey, fnNum);
-  ALWAYS(_iSymbols.insert(interpretation, fnNum));
-  OperatorType* fnType = Theory::getOperationType(interpretation);
-  ASS(fnType->isFunctionType());
-  sym->setType(fnType);
-  return fnNum;
-} // Signature::addInterpretedFunction
-
-/**
- * Add interpreted predicate
- */
-unsigned Signature::addInterpretedPredicate(Interpretation interpretation, const vstring& name)
-{
-  CALL("Signature::addInterpretedPredicate");
-  ASS(!Theory::isFunction(interpretation));
-
-  unsigned res;
-  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;
-  }
-
-  vstring symbolKey = name+"_i"+Int::toString(interpretation);
-
-  ASS(!_predNames.find(symbolKey));
-
-  unsigned predNum = _preds.length();
-  InterpretedSymbol* sym = new InterpretedSymbol(name, interpretation);
-  _preds.push(sym);
-  _predNames.insert(symbolKey,predNum);
-  ALWAYS(_iSymbols.insert(interpretation, predNum));
-  if (predNum!=0) {
-    OperatorType* predType = Theory::getOperationType(interpretation);
-    ASS_REP(!predType->isFunctionType(), predType->toString());
-    sym->setType(predType);
-  }
-  return predNum;
-} // Signature::addInterpretedPredicate
-
 /**
  * Add an integer constant to the signature. If defaultSort is true, treat it as
  * a term of the default sort, otherwise as an interepreted integer value.
@@ -475,19 +412,88 @@ unsigned Signature::addRealConstant(const RealConstantType& value)
   return result;
 }
 
+/**
+ * Add interpreted function
+ */
+unsigned Signature::addInterpretedFunction(Interpretation interpretation, OperatorType* type, const vstring& name)
+{
+  CALL("Signature::addInterpretedFunction(Interpretation,OperatorType*,const vstring&)");
+  ASS(Theory::isFunction(interpretation));
+
+  Theory::MonomorphisedInterpretation mi = std::make_pair(interpretation,type);
+
+  unsigned res;
+  if (_iSymbols.find(mi,res)) { // already declared
+    if (name!=functionName(res)) {
+      USER_ERROR("Interpreted function '"+functionName(res)+"' has the same interpretation as '"+name+"' should have");
+    }
+    return res;
+  }
+
+  vstring symbolKey = name+"_i"+Int::toString(interpretation)+(Theory::isPolymorphic(interpretation) ? type->toString() : "");
+  ASS(!_funNames.find(symbolKey));
+
+  unsigned fnNum = _funs.length();
+  InterpretedSymbol* sym = new InterpretedSymbol(name, interpretation);
+  _funs.push(sym);
+  _funNames.insert(symbolKey, fnNum);
+  ALWAYS(_iSymbols.insert(mi, fnNum));
+
+  OperatorType* fnType = Theory::getNonpolymorphicOperatorType(interpretation);
+  ASS(fnType->isFunctionType());
+  sym->setType(fnType);
+  return fnNum;
+} // Signature::addInterpretedFunction
+
+/**
+ * Add interpreted predicate
+ */
+unsigned Signature::addInterpretedPredicate(Interpretation interpretation, OperatorType* type, const vstring& name)
+{
+  CALL("Signature::addInterpretedPredicate(Interpretation,OperatorType*,const vstring&)");
+  ASS(!Theory::isFunction(interpretation));
+
+  Theory::MonomorphisedInterpretation mi = std::make_pair(interpretation,type);
+
+  unsigned res;
+  if (_iSymbols.find(mi,res)) { // already declared
+    if (name!=predicateName(res)) {
+      USER_ERROR("Interpreted predicate '"+predicateName(res)+"' has the same interpretation as '"+name+"' should have");
+    }
+    return res;
+  }
+
+  vstring symbolKey = name+"_i"+Int::toString(interpretation)+(Theory::isPolymorphic(interpretation) ? type->toString() : "");
+
+  ASS(!_predNames.find(symbolKey));
+
+  unsigned predNum = _preds.length();
+  InterpretedSymbol* sym = new InterpretedSymbol(name, interpretation);
+  _preds.push(sym);
+  _predNames.insert(symbolKey,predNum);
+  ALWAYS(_iSymbols.insert(mi, predNum));
+  if (predNum!=0) {
+    OperatorType* predType = Theory::getNonpolymorphicOperatorType(interpretation);
+    ASS_REP(!predType->isFunctionType(), predType->toString());
+    sym->setType(predType);
+  }
+  return predNum;
+} // Signature::addInterpretedPredicate
+
+
 /**
  * Return number of symbol that is interpreted by Interpretation @b interp.
  *
  * If no such symbol exists, it is created.
  */
-unsigned Signature::getInterpretingSymbol(Interpretation interp)
+unsigned Signature::getInterpretingSymbol(Interpretation interp, OperatorType* type)
 {
-  CALL("Signature::getInterpretingSymbol");
+  CALL("Signature::getInterpretingSymbol(Interpretation,OperatorType*)");
   
-  ASS(Theory::instance()->isValidInterpretation(interp));
-    
+  Theory::MonomorphisedInterpretation mi = std::make_pair(interp,type);
+
   unsigned res;
-  if (_iSymbols.find(interp, res)) {
+  if (_iSymbols.find(mi, res)) {
     return res;
   }
 
@@ -502,7 +508,7 @@ unsigned Signature::getInterpretingSymbol(Interpretation interp)
       }
       name=name+Int::toString(i);
     }
-    addInterpretedFunction(interp, name);
+    addInterpretedFunction(interp, type, name);
   }
   else {
     if (predicateExists(name, arity)) {
@@ -512,17 +518,11 @@ unsigned Signature::getInterpretingSymbol(Interpretation interp)
       }
       name=name+Int::toString(i);
     }
-    addInterpretedPredicate(interp, name);
+    addInterpretedPredicate(interp, type, name);
   }
 
   //we have now registered a new function, so it should be present in the map
-  return _iSymbols.get(interp);
-}
-
-unsigned Signature::getStructureInterpretationFunctor(unsigned theorySort, Theory::StructuredSortInterpretation ssi) {
-  CALL("Signature::getStructureInterpretationFunctor");
-  Interpretation i = Theory::instance()->getInterpretation(theorySort, ssi);
-  return env.signature->getInterpretingSymbol(i);
+  return _iSymbols.get(mi);
 }
 
 const vstring& Signature::functionName(int number)
diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp
index 8421e7ab29..be53047459 100644
--- a/Kernel/Signature.hpp
+++ b/Kernel/Signature.hpp
@@ -335,10 +335,6 @@ class Signature
   unsigned addNamePredicate(unsigned arity);
 
   // Interpreted symbol declarations
-
-  unsigned addInterpretedFunction(Interpretation itp, const vstring& name);
-  unsigned addInterpretedPredicate(Interpretation itp, const vstring& name);
-
   unsigned addIntegerConstant(const vstring& number,bool defaultSort);
   unsigned addRationalConstant(const vstring& numerator, const vstring& denominator,bool defaultSort);
   unsigned addRealConstant(const vstring& number,bool defaultSort);
@@ -347,27 +343,40 @@ class Signature
   unsigned addRationalConstant(const RationalConstantType& number);
   unsigned addRealConstant(const RealConstantType& number);
 
-  vstring getInterpretationName(Interpretation interp);
-  unsigned getInterpretingSymbol(Interpretation interp);
-
-  unsigned getStructureInterpretationFunctor(unsigned theorySort, Theory::StructuredSortInterpretation ssi);
+  unsigned addInterpretedFunction(Interpretation itp, OperatorType* type, const vstring& name);
+  unsigned addInterpretedFunction(Interpretation itp, const vstring& name)
+  {
+    CALL("Signature::addInterpretedFunction(Interpretation,const vstring&)");
+    ASS(!Theory::isPolymorphic(itp));
+    return addInterpretedFunction(itp,Theory::getNonpolymorphicOperatorType(itp),name);
+  }
 
-  /** Return true iff there is a symbol interpreted by Interpretation @b interp */
-  bool haveInterpretingSymbol(Interpretation interp) const { return _iSymbols.find(interp); }
+  unsigned addInterpretedPredicate(Interpretation itp, OperatorType* type, const vstring& name);
+  unsigned addInterpretedPredicate(Interpretation itp, const vstring& name)
+  {
+    CALL("Signature::addInterpretedPredicate(Interpretation,const vstring&)");
+    ASS(!Theory::isPolymorphic(itp));
+    return addInterpretedPredicate(itp,Theory::getNonpolymorphicOperatorType(itp),name);
+  }
 
-  /**
-   * Return true iff we have any declared interpreted symbols
-   *
-   * The equality symbol is always present and is interpreted,
-   * so we return true only if we have any other interpreted
-   * symbols.
-   */
-  bool anyInterpretedSymbols() const
+  unsigned getInterpretingSymbol(Interpretation interp, OperatorType* type);
+  unsigned getInterpretingSymbol(Interpretation interp)
   {
-    CALL("Signature::anyInterpretedSymbols");
-    ASS_G(_iSymbols.size(),0); //we always have equality which is interpreted
+    CALL("Signature::getInterpretingSymbol(Interpretation)");
+    ASS(!Theory::isPolymorphic(interp));
+    return getInterpretingSymbol(interp,Theory::getNonpolymorphicOperatorType(interp));
+  }
 
-    return _iSymbols.size()!=1;
+  /** Return true iff there is a symbol interpreted by Interpretation @b interp */
+  bool haveInterpretingSymbol(Interpretation interp, OperatorType* type) const {
+    CALL("Signature::haveInterpretingSymbol(Interpretation, OperatorType*)");
+    return _iSymbols.find(std::make_pair(interp,type));
+  }
+  unsigned haveInterpretingSymbol(Interpretation interp)
+  {
+    CALL("Signature::haveInterpretingSymbol(Interpretation)");
+    ASS(!Theory::isPolymorphic(interp));
+    return haveInterpretingSymbol(interp,Theory::getNonpolymorphicOperatorType(interp));
   }
 
   /** return the name of a function with a given number */
@@ -533,13 +542,14 @@ class Signature
   bool _distinctGroupsAddedTo;
 
   /**
-   * Map from Interpretation values to function and predicate symbols representing them
+   * Map from MonomorphisedInterpretation values to function and predicate symbols representing them
    *
    * We mix here function and predicate symbols, but it is not a problem, as
-   * the Interpretation value already determines whether we deal with a function
+   * the MonomorphisedInterpretation value already determines whether we deal with a function
    * or a predicate.
    */
-  DHMap<Interpretation, unsigned> _iSymbols;
+  DHMap<Theory::MonomorphisedInterpretation, unsigned> _iSymbols;
+
   /** the number of string constants */
   unsigned _strings;
   /** the number of integer constants */
diff --git a/Kernel/Sorts.hpp b/Kernel/Sorts.hpp
index cd862cba93..3a74868ad7 100644
--- a/Kernel/Sorts.hpp
+++ b/Kernel/Sorts.hpp
@@ -61,8 +61,6 @@ class Sorts {
   enum class StructuredSort {
     /** The structured sort for arrays **/
     ARRAY,
-    /** The structured sort for lists, currently unused **/
-    LIST,
     /** The structured sort for tuples */
     TUPLE,
     /** not a real structured sort, it's here to denote the length of the StructuredSort enum */
diff --git a/Kernel/Theory.cpp b/Kernel/Theory.cpp
index 55b619605f..30cfc007b0 100644
--- a/Kernel/Theory.cpp
+++ b/Kernel/Theory.cpp
@@ -546,18 +546,6 @@ unsigned Theory::getArity(Interpretation i)
   CALL("Signature::InterpretedSymbol::getArity");
   ASS(theory->isValidInterpretation(i));
 
-  if (theory->isStructuredSortInterpretation(i)){
-    switch (theory->convertToStructured(i)) {
-      case StructuredSortInterpretation::ARRAY_SELECT:
-      case StructuredSortInterpretation::ARRAY_BOOL_SELECT:
-        return 2;
-      case StructuredSortInterpretation::ARRAY_STORE:
-        return 3;
-      default:
-        return 1;
-    }
-  }
-
   switch(i) {
   case INT_IS_INT:
   case INT_IS_RAT:
@@ -651,8 +639,15 @@ unsigned Theory::getArity(Interpretation i)
   case REAL_REMAINDER_E:
   case REAL_REMAINDER_T:
   case REAL_REMAINDER_F:
+
+  case ARRAY_SELECT:
+  case ARRAY_BOOL_SELECT:
+
     return 2;
           
+  case ARRAY_STORE:
+
+    return 3;
           
   default:
     ASSERTION_VIOLATION_REP(i);
@@ -668,15 +663,6 @@ bool Theory::isFunction(Interpretation i)
   CALL("Signature::InterpretedSymbol::isFunction");
   ASS(theory->isValidInterpretation(i));
 
-  if(theory->isStructuredSortInterpretation(i)){
-    switch(theory->convertToStructured(i)){
-      case StructuredSortInterpretation::ARRAY_BOOL_SELECT:
-        return false;
-      default:
-        return true;
-    }
-  }
-
   switch(i) {
   case INT_TO_INT:
   case INT_TO_RAT:
@@ -738,6 +724,9 @@ bool Theory::isFunction(Interpretation i)
   case REAL_TRUNCATE:
   case REAL_ROUND:
           
+  case ARRAY_SELECT:
+  case ARRAY_STORE:
+
     return true;
 
   case EQUAL:
@@ -767,6 +756,9 @@ bool Theory::isFunction(Interpretation i)
   case REAL_IS_INT:
   case REAL_IS_RAT:
   case REAL_IS_REAL:
+
+  case ARRAY_BOOL_SELECT:
+
     return false;
 
   default:
@@ -821,12 +813,35 @@ bool Theory::hasSingleSort(Interpretation i)
   case RAT_TO_REAL:
   case REAL_TO_INT:
   case REAL_TO_RAT:
+
+  case ARRAY_SELECT:
+  case ARRAY_BOOL_SELECT:
+  case ARRAY_STORE:
+
     return false;
   default:
     return true;
   }
 }
 
+bool Theory::isPolymorphic(Interpretation i)
+{
+  CALL("Theory::isPolymorphic");
+
+  switch(i) {
+  case EQUAL:
+    return false; // for historical reasons equality is treated specially and does not count as polymorphic
+
+  case ARRAY_SELECT:
+  case ARRAY_BOOL_SELECT:
+  case ARRAY_STORE:
+
+    return true;
+  default:
+    return false;
+  }
+}
+
 /**
  * This function can be called for operations for which  the
  * function @c hasSingleSort returns true
@@ -835,13 +850,9 @@ unsigned Theory::getOperationSort(Interpretation i)
 {
   CALL("Theory::getOperationSort");
 
-  
   ASS(hasSingleSort(i));
   ASS(theory->isValidInterpretation(i));
-
-  if (theory->isStructuredSortInterpretation(i)) {
-    return theory->getStructuredOperationSort(i);
-  }
+  ASS(!isPolymorphic(i));
 
   switch(i) {
   case INT_GREATER:
@@ -1032,66 +1043,6 @@ bool Theory::isPartialFunction(Interpretation i)
   }
 }
 
-unsigned Theory::getSymbolForStructuredSort(unsigned sort, StructuredSortInterpretation interp)
-{
-    return env.signature->getInterpretingSymbol(getInterpretation(sort,interp));
-}
-
-/**
- * Return true if interpreted function @c i is an array operation.
- * @author Laura Kovacs
- * @since 31/08/2012, Vienna
- */
-bool Theory::isArrayOperation(Interpretation i)
-{
-  CALL("Theory::isArrayFunction");
-  if(!theory->isStructuredSortInterpretation(i)) return false;
-  return env.sorts->isOfStructuredSort(theory->getSort(i),Sorts::StructuredSort::ARRAY);
-}
-
-/**
-* This function can be called for array operations 
-* it returns the range domain (the sort of the output) of select and store
-* @author Laura Kovacs
-* @since 31/08/2012, Vienna
-*/
-unsigned Theory::getArrayOperationSort(Interpretation i)
-{
-    CALL("Theory::getArrayOperationSort");
-    ASS(isArrayOperation(i));
-    
-    unsigned sort = theory->getSort(i);
-
-    switch(theory->convertToStructured(i))
-    {
-      case StructuredSortInterpretation::ARRAY_SELECT:
-      case StructuredSortInterpretation::ARRAY_BOOL_SELECT:
-        return env.sorts->getArraySort(sort)->getInnerSort();
-      case StructuredSortInterpretation::ARRAY_STORE:
-        return sort; 
-      default:
-        ASSERTION_VIOLATION;
-    }
-}
-    
-        
-    
-/**
-* This function returns the domain of array indexes (SRT_INT)
-* @author Laura Kovacs
-* @since 31/08/2012, Vienna
-* @since 7/10/2015 update to support polymorphism in the index sort
-*/
-unsigned Theory::getArrayDomainSort(Interpretation i)
-{
-    CALL("Theory::getArrayDomainSort");
-    ASS(isArrayOperation(i));
-        
-    unsigned sort = theory->getSort(i);
-
-    return  env.sorts->getArraySort(sort)->getIndexSort();
-}
-
 /**
  * Get the number of the skolem function symbol used in the clause form of the
  * array extensionality axiom (of particular sort).
@@ -1110,15 +1061,10 @@ unsigned Theory::getArrayExtSkolemFunction(unsigned sort) {
     return _arraySkolemFunctions.get(sort);
   }
 
-  bool isBool = (env.sorts->getArraySort(sort)->getInnerSort() == Sorts::SRT_BOOL);
-
-  Interpretation store = getInterpretation(sort, StructuredSortInterpretation::ARRAY_STORE);
-  Interpretation select = getInterpretation(sort, isBool ? StructuredSortInterpretation::ARRAY_BOOL_SELECT
-                                                         : StructuredSortInterpretation::ARRAY_SELECT);
+  Sorts::ArraySort* arraySort = env.sorts->getArraySort(sort);
 
-  unsigned arraySort = getArrayOperationSort(store);
-  unsigned indexSort = theory->getArrayDomainSort(select);
-  unsigned params[] = {arraySort, arraySort};
+  unsigned indexSort = arraySort->getIndexSort();
+  unsigned params[] = {sort, sort};
   unsigned skolemFunction = Shell::Skolem::addSkolemFunction(2, params, indexSort, "arrayDiff");
 
   _arraySkolemFunctions.insert(sort,skolemFunction);
@@ -1249,173 +1195,140 @@ OperatorType* Theory::getConversionOperationType(Interpretation i)
   return OperatorType::getFunctionType({from}, to);
 }
 
-Sorts::StructuredSort Theory::getInterpretedSort(StructuredSortInterpretation ssi) {
-  switch (ssi) {
-    case StructuredSortInterpretation::ARRAY_SELECT:
-    case StructuredSortInterpretation::ARRAY_BOOL_SELECT:
-    case StructuredSortInterpretation::ARRAY_STORE:
-      return Sorts::StructuredSort::ARRAY;
-    case StructuredSortInterpretation::LIST_HEAD:
-    case StructuredSortInterpretation::LIST_TAIL:
-    case StructuredSortInterpretation::LIST_CONS:
-    case StructuredSortInterpretation::LIST_IS_EMPTY:
-      return Sorts::StructuredSort::LIST;
-    default:
-      ASSERTION_VIOLATION;
-  }
-}
-
 vstring Theory::getInterpretationName(Interpretation interp) {
   CALL("Theory::getInterpretationName");
 
-  if (Theory::instance()->isStructuredSortInterpretation(interp)) {
-    switch (Theory::instance()->convertToStructured(interp)) {
-      case StructuredSortInterpretation::ARRAY_SELECT:
-      case StructuredSortInterpretation::ARRAY_BOOL_SELECT:
-        return "$select";
-      case StructuredSortInterpretation::ARRAY_STORE:
-        return "$store";
-      default:
-        ASSERTION_VIOLATION_REP(interp);
-    }
-  } else {
-    switch (interp) {
-      case Theory::INT_SUCCESSOR:
-        //this one is not according the TPTP arithmetic (it doesn't have successor)
-        return "$successor";
-      case Theory::INT_DIVIDES:
-        return "$divides";
-      case Theory::INT_UNARY_MINUS:
-      case Theory::RAT_UNARY_MINUS:
-      case Theory::REAL_UNARY_MINUS:
-        return "$uminus";
-      case Theory::INT_PLUS:
-      case Theory::RAT_PLUS:
-      case Theory::REAL_PLUS:
-        return "$sum";
-      case Theory::INT_MINUS:
-      case Theory::RAT_MINUS:
-      case Theory::REAL_MINUS:
-        return "$difference";
-      case Theory::INT_MULTIPLY:
-      case Theory::RAT_MULTIPLY:
-      case Theory::REAL_MULTIPLY:
-        return "$product";
-      case Theory::INT_GREATER:
-      case Theory::RAT_GREATER:
-      case Theory::REAL_GREATER:
-        return "$greater";
-      case Theory::INT_GREATER_EQUAL:
-      case Theory::RAT_GREATER_EQUAL:
-      case Theory::REAL_GREATER_EQUAL:
-        return "$greatereq";
-      case Theory::INT_LESS:
-      case Theory::RAT_LESS:
-      case Theory::REAL_LESS:
-        return "$less";
-      case Theory::INT_LESS_EQUAL:
-      case Theory::RAT_LESS_EQUAL:
-      case Theory::REAL_LESS_EQUAL:
-        return "$lesseq";
-      case Theory::INT_IS_INT:
-      case Theory::RAT_IS_INT:
-      case Theory::REAL_IS_INT:
-        return "$is_int";
-      case Theory::INT_IS_RAT:
-      case Theory::RAT_IS_RAT:
-      case Theory::REAL_IS_RAT:
-        return "$is_rat";
-      case Theory::INT_IS_REAL:
-      case Theory::RAT_IS_REAL:
-      case Theory::REAL_IS_REAL:
-        return "$is_real";
-      case Theory::INT_TO_INT:
-      case Theory::RAT_TO_INT:
-      case Theory::REAL_TO_INT:
-        return "$to_int";
-      case Theory::INT_TO_RAT:
-      case Theory::RAT_TO_RAT:
-      case Theory::REAL_TO_RAT:
-        return "$to_rat";
-      case Theory::INT_TO_REAL:
-      case Theory::RAT_TO_REAL:
-      case Theory::REAL_TO_REAL:
-        return "$to_real";
-      case Theory::INT_ABS:
-        return "$abs";
-      case Theory::INT_QUOTIENT_E:
-      case Theory::RAT_QUOTIENT_E:
-      case Theory::REAL_QUOTIENT_E:
-        return "$quotient_e";
-      case Theory::INT_QUOTIENT_T:
-      case Theory::RAT_QUOTIENT_T:
-      case Theory::REAL_QUOTIENT_T:
-        return "$quotient_t";
-      case Theory::INT_QUOTIENT_F:
-      case Theory::RAT_QUOTIENT_F:
-      case Theory::REAL_QUOTIENT_F:
-        return "$quotient_f";
-      case Theory::INT_REMAINDER_T:
-      case Theory::RAT_REMAINDER_T:
-      case Theory::REAL_REMAINDER_T:
-        return "$remainder_t";
-      case Theory::INT_REMAINDER_F:
-      case Theory::RAT_REMAINDER_F:
-      case Theory::REAL_REMAINDER_F:
-        return "$remainder_f";
-      case Theory::INT_REMAINDER_E:
-      case Theory::RAT_REMAINDER_E:
-      case Theory::REAL_REMAINDER_E:
-        return "$remainder_e";
-      case Theory::RAT_QUOTIENT:
-      case Theory::REAL_QUOTIENT:
-        return "$quotient";
-      case Theory::INT_TRUNCATE:
-      case Theory::RAT_TRUNCATE:
-      case Theory::REAL_TRUNCATE:
-        return "truncate";
-      case Theory::INT_FLOOR:
-      case Theory::RAT_FLOOR:
-      case Theory::REAL_FLOOR:
-        return "floor";
-      case Theory::INT_CEILING:
-      case Theory::RAT_CEILING:
-      case Theory::REAL_CEILING:
-        return "ceiling";
-      default:
-        ASSERTION_VIOLATION_REP(interp);
-    }
+  switch (interp) {
+    case INT_SUCCESSOR:
+      //this one is not according the TPTP arithmetic (it doesn't have successor)
+      return "$successor";
+    case INT_DIVIDES:
+      return "$divides";
+    case INT_UNARY_MINUS:
+    case RAT_UNARY_MINUS:
+    case REAL_UNARY_MINUS:
+      return "$uminus";
+    case INT_PLUS:
+    case RAT_PLUS:
+    case REAL_PLUS:
+      return "$sum";
+    case INT_MINUS:
+    case RAT_MINUS:
+    case REAL_MINUS:
+      return "$difference";
+    case INT_MULTIPLY:
+    case RAT_MULTIPLY:
+    case REAL_MULTIPLY:
+      return "$product";
+    case INT_GREATER:
+    case RAT_GREATER:
+    case REAL_GREATER:
+      return "$greater";
+    case INT_GREATER_EQUAL:
+    case RAT_GREATER_EQUAL:
+    case REAL_GREATER_EQUAL:
+      return "$greatereq";
+    case INT_LESS:
+    case RAT_LESS:
+    case REAL_LESS:
+      return "$less";
+    case INT_LESS_EQUAL:
+    case RAT_LESS_EQUAL:
+    case REAL_LESS_EQUAL:
+      return "$lesseq";
+    case INT_IS_INT:
+    case RAT_IS_INT:
+    case REAL_IS_INT:
+      return "$is_int";
+    case INT_IS_RAT:
+    case RAT_IS_RAT:
+    case REAL_IS_RAT:
+      return "$is_rat";
+    case INT_IS_REAL:
+    case RAT_IS_REAL:
+    case REAL_IS_REAL:
+      return "$is_real";
+    case INT_TO_INT:
+    case RAT_TO_INT:
+    case REAL_TO_INT:
+      return "$to_int";
+    case INT_TO_RAT:
+    case RAT_TO_RAT:
+    case REAL_TO_RAT:
+      return "$to_rat";
+    case INT_TO_REAL:
+    case RAT_TO_REAL:
+    case REAL_TO_REAL:
+      return "$to_real";
+    case INT_ABS:
+      return "$abs";
+    case INT_QUOTIENT_E:
+    case RAT_QUOTIENT_E:
+    case REAL_QUOTIENT_E:
+      return "$quotient_e";
+    case INT_QUOTIENT_T:
+    case RAT_QUOTIENT_T:
+    case REAL_QUOTIENT_T:
+      return "$quotient_t";
+    case INT_QUOTIENT_F:
+    case RAT_QUOTIENT_F:
+    case REAL_QUOTIENT_F:
+      return "$quotient_f";
+    case INT_REMAINDER_T:
+    case RAT_REMAINDER_T:
+    case REAL_REMAINDER_T:
+      return "$remainder_t";
+    case INT_REMAINDER_F:
+    case RAT_REMAINDER_F:
+    case REAL_REMAINDER_F:
+      return "$remainder_f";
+    case INT_REMAINDER_E:
+    case RAT_REMAINDER_E:
+    case REAL_REMAINDER_E:
+      return "$remainder_e";
+    case RAT_QUOTIENT:
+    case REAL_QUOTIENT:
+      return "$quotient";
+    case INT_TRUNCATE:
+    case RAT_TRUNCATE:
+    case REAL_TRUNCATE:
+      return "truncate";
+    case INT_FLOOR:
+    case RAT_FLOOR:
+    case REAL_FLOOR:
+      return "floor";
+    case INT_CEILING:
+    case RAT_CEILING:
+    case REAL_CEILING:
+      return "ceiling";
+    case ARRAY_SELECT:
+    case ARRAY_BOOL_SELECT:
+      return "$select";
+    case ARRAY_STORE:
+      return "$store";
+    default:
+      ASSERTION_VIOLATION_REP(interp);
   }
 }
 
-OperatorType* Theory::getStructuredSortOperationType(Interpretation i) {
-  CALL("Theory::getStructuredSortOperationType");
-
-  ASS(theory->isStructuredSortInterpretation(i));
+OperatorType* Theory::getArrayOperatorType(unsigned arraySort, Interpretation i) {
+  CALL("Theory::getArrayOperatorType");
 
-  unsigned theorySort = theory->getSort(i);
-  StructuredSortInterpretation ssi = theory->convertToStructured(i);
+  Sorts::ArraySort* info = env.sorts->getArraySort(arraySort);
 
-  switch (theory->getInterpretedSort(ssi)) {
-    case Sorts::StructuredSort::ARRAY: {
-      unsigned indexSort = getArrayDomainSort(i);
-      unsigned valueSort = getArrayOperationSort(i);
-      unsigned innerSort = env.sorts->getArraySort(theorySort)->getInnerSort();
+  unsigned indexSort = info->getIndexSort();
+  unsigned innerSort = info->getInnerSort();
 
-      switch (ssi) {
-        case StructuredSortInterpretation::ARRAY_SELECT:
-          return OperatorType::getFunctionType({ theorySort, indexSort }, valueSort);
+  switch (i) {
+    case Interpretation::ARRAY_SELECT:
+      return OperatorType::getFunctionType({ arraySort, indexSort }, innerSort);
 
-        case StructuredSortInterpretation::ARRAY_BOOL_SELECT:
-          return OperatorType::getPredicateType({ theorySort, indexSort });
+    case Interpretation::ARRAY_BOOL_SELECT:
+      return OperatorType::getPredicateType({ arraySort, indexSort });
 
-        case StructuredSortInterpretation::ARRAY_STORE:
-          return OperatorType::getFunctionType({ theorySort, indexSort, innerSort }, valueSort);
+    case Interpretation::ARRAY_STORE:
+      return OperatorType::getFunctionType({ arraySort, indexSort, innerSort }, arraySort);
 
-        default:
-          ASSERTION_VIOLATION;
-      }
-    }
     default:
       ASSERTION_VIOLATION;
   }
@@ -1424,19 +1337,15 @@ OperatorType* Theory::getStructuredSortOperationType(Interpretation i) {
 /**
  * Return type of the function representing interpreted function/predicate @c i.
  */
-OperatorType* Theory::getOperationType(Interpretation i)
+OperatorType* Theory::getNonpolymorphicOperatorType(Interpretation i)
 {
-  CALL("Theory::getOperationType");
-  ASS_NEQ(i, EQUAL);
+  CALL("Theory::getNonpolymorphicOperationType");
+  ASS(!isPolymorphic(i));
 
   if (isConversionOperation(i)) {
     return getConversionOperationType(i);
   }
 
-  if (theory->isStructuredSortInterpretation(i)) {
-    return getStructuredSortOperationType(i);
-  }
-
   unsigned sort;
   ASS(hasSingleSort(i));
   sort = getOperationSort(i);
@@ -1839,97 +1748,6 @@ Term* Theory::representRealConstant(vstring str)
   }
 }
 
-/**
- * Return term containing unary function interpreted as @b itp with
- * @b arg as its first argument
- */
-Term* Theory::fun1(Interpretation itp, TermList arg)
-{
-  CALL("Theory::fun1");
-  ASS(isFunction(itp));
-  ASS_EQ(getArity(itp), 1);
-
-  unsigned fn=theory->getFnNum(itp);
-  return Term::create(fn, 1, &arg);
-}
-
-/**
- * Return term containing binary function interpreted as @b itp with
- * arguments @b arg1 and @b arg2
- */
-Term* Theory::fun2(Interpretation itp, TermList arg1, TermList arg2)
-{
-  CALL("Theory::fun2");
-  ASS(isFunction(itp));
-  ASS_EQ(getArity(itp), 2);
-
-  TermList args[]= {arg1, arg2};
-
-  unsigned fn=theory->getFnNum(itp);
-  return Term::create(fn, 2, args);
-}
-
-    
-/**
-* Return term containing trenary function interpreted as @b itp with
-* arguments @b arg1 ,  @b arg2, @b arg3
-*/
-Term* Theory::fun3(Interpretation itp, TermList arg1, TermList arg2, TermList arg3)
-    {
-        CALL("Theory::fun3");
-        ASS(isFunction(itp));
-        ASS_EQ(getArity(itp), 3);
-        
-        TermList args[]= {arg1, arg2, arg3};
-        
-        unsigned fn=theory->getFnNum(itp);
-        return Term::create(fn, 3, args);
-    }
-
-
-    
-    
-/**
- * Return literal containing binary predicate interpreted as @b itp with
- * arguments @b arg1 and @b arg2
- *
- * Equality cannot be created using this function, Term::createEquality has to be used.
- */
-Literal* Theory::pred2(Interpretation itp, bool polarity, TermList arg1, TermList arg2)
-{
-  CALL("Theory::fun2");
-  ASS(!isFunction(itp));
-  ASS_EQ(getArity(itp), 2);
-  ASS_NEQ(itp,EQUAL);
-
-  TermList args[]= {arg1, arg2};
-
-  unsigned pred=theory->getPredNum(itp);
-  return Literal::create(pred, 2, polarity, false, args);
-}
-
-/**
- * Return number of function that is intepreted as @b itp
- */
-unsigned Theory::getFnNum(Interpretation itp)
-{
-  CALL("Theory::getFnNum");
-  ASS(isFunction(itp));
-  
-  return env.signature->getInterpretingSymbol(itp);
-}
-
-/**
- * Return number of predicate that is intepreted as @b itp
- */
-unsigned Theory::getPredNum(Interpretation itp)
-{
-  CALL("Theory::getPredNum");
-  ASS(!isFunction(itp));
-  
-  return env.signature->getInterpretingSymbol(itp);
-}
-
 /**
  * Register that a predicate pred with a given polarity has the given
  * template. See tryGetInterpretedLaTeXName for explanation of templates 
diff --git a/Kernel/Theory.hpp b/Kernel/Theory.hpp
index 5b0d87f590..f15e451766 100644
--- a/Kernel/Theory.hpp
+++ b/Kernel/Theory.hpp
@@ -138,8 +138,6 @@ std::ostream& operator<< (ostream& out, const IntegerConstantType& val) {
   return out << val.toInner();
 }
 
-
-
 /**
  * A class for representing rational numbers
  *
@@ -375,84 +373,38 @@ class Theory
     RAT_TO_REAL,
     REAL_TO_INT,
     REAL_TO_RAT,
-    REAL_TO_REAL
+    REAL_TO_REAL,
 
-    // IMPORTANT - if you add something to end of this, update it in LastNonStructuredInterepretation 
+    // array functions
+    ARRAY_SELECT,
+    ARRAY_BOOL_SELECT,
+    ARRAY_STORE,
     
-    //INVALID_INTERPRETATION // replaced by LastNonStructuredInterepretation
+    INVALID_INTERPRETATION // LEAVE THIS AS THE LAST ELEMENT OF THE ENUM
   };
 
-  unsigned LastNonStructuredInterepretation(){ return REAL_TO_REAL; }
+  typedef std::pair<Interpretation, OperatorType*> MonomorphisedInterpretation;
 
-    /**
-     * Maximal element number in the enum Interpretation
-     *
-     * At some points we make use of the fact that we can iterate through all
-     * interpretations by going through the set {0,...,MAX_INTERPRETED_ELEMENT}.
-     */
-  unsigned MaxInterpretedElement(){
-    return LastNonStructuredInterepretation() + _structuredSortInterpretations.size(); 
-  }
-
-  unsigned numberOfInterpretations(){
-    return LastNonStructuredInterepretation() + LastStructuredInterpretation();
+  bool isValidInterpretation(Interpretation i){
+    return i < INVALID_INTERPRETATION;
   }
 
-  bool isValidInterpretation(Interpretation i){
-    return i <= MaxInterpretedElement();
+  unsigned numberOfInterpretations() {
+    return INVALID_INTERPRETATION;
   }
 
   bool isPlus(Interpretation i){
     return i == INT_PLUS || i == RAT_PLUS || i == REAL_PLUS;
   }
 
- /*
-  * StructuredSortInterpretations begin from the last interpretation in Interpretation
-  *
-  * They will be initialised as MaxInterpretedElement()+1
-  *
-  */
-
-
-  /** enum for the kinds of StructuredSort interpretations **/
-  enum class StructuredSortInterpretation
-  {
-    ARRAY_SELECT,
-    ARRAY_BOOL_SELECT,
-    ARRAY_STORE,
-    // currently unused
-    LIST_HEAD,
-    LIST_TAIL,
-    LIST_CONS,
-    LIST_IS_EMPTY
-  };
-  unsigned LastStructuredInterpretation(){
-    return static_cast<unsigned>(StructuredSortInterpretation::LIST_IS_EMPTY);
-  }
-  unsigned getSymbolForStructuredSort(unsigned sort, StructuredSortInterpretation interp);
-  Interpretation getInterpretation(unsigned sort, StructuredSortInterpretation i){
-    auto key = make_pair(sort, i);
-    unsigned interpretation;
-    if (!_structuredSortInterpretations.find(key, interpretation)) {
-      interpretation = MaxInterpretedElement() + 1;
-      _structuredSortInterpretations.insert(key, interpretation);
-    }
-    return static_cast<Interpretation>(interpretation);
-  }
-  bool isStructuredSortInterpretation(Interpretation i){
-    return i > LastNonStructuredInterepretation();
-  }
-  unsigned getSort(Interpretation i){
-    return getData(i).first;
-  }
-
   static vstring getInterpretationName(Interpretation i);
   static unsigned getArity(Interpretation i);
   static bool isFunction(Interpretation i);
   static bool isInequality(Interpretation i);
-  static Sorts::StructuredSort getInterpretedSort(StructuredSortInterpretation ssi);
-  static OperatorType* getOperationType(Interpretation i);
-  static OperatorType* getStructuredSortOperationType(Interpretation i);
+  static OperatorType* getNonpolymorphicOperatorType(Interpretation i);
+
+  static OperatorType* getArrayOperatorType(unsigned arraySort, Interpretation i);
+
   static bool hasSingleSort(Interpretation i);
   static unsigned getOperationSort(Interpretation i);
   static bool isConversionOperation(Interpretation i);
@@ -460,9 +412,7 @@ class Theory
   static bool isNonLinearOperation(Interpretation i);
   static bool isPartialFunction(Interpretation i);
 
-  static bool isArrayOperation(Interpretation i);
-  static unsigned getArrayOperationSort(Interpretation i);
-  static unsigned getArrayDomainSort(Interpretation i);
+  static bool isPolymorphic(Interpretation i);
 
   unsigned getArrayExtSkolemFunction(unsigned i);
     
@@ -497,9 +447,6 @@ class Theory
   Interpretation interpretPredicate(unsigned pred);
   Interpretation interpretPredicate(Literal* t);
 
-  unsigned getFnNum(Interpretation itp);
-  unsigned getPredNum(Interpretation itp);
-
   void registerLaTeXPredName(unsigned func, bool polarity, vstring temp);
   void registerLaTeXFuncName(unsigned func, vstring temp);
   vstring tryGetInterpretedLaTeXName(unsigned func, bool pred,bool polarity=true);
@@ -512,11 +459,6 @@ class Theory
 
 public:
 
-  Term* fun1(Interpretation itp, TermList arg);
-  Term* fun2(Interpretation itp, TermList arg1, TermList arg2);
-  Term* fun3(Interpretation itp, TermList arg1, TermList arg2, TermList arg3);
-  Literal* pred2(Interpretation itp, bool polarity, TermList arg1, TermList arg2);
-
   /**
    * Try to interpret the term list as an integer constant. If it is an
    * integer constant, return true and save the constant in @c res, otherwise
@@ -572,26 +514,6 @@ class Theory
 
   DHMap<unsigned,unsigned> _arraySkolemFunctions;
 
-public:
-  unsigned getStructuredOperationSort(Interpretation i){
-    return getData(i).first;
-  }
-  StructuredSortInterpretation convertToStructured(Interpretation i){
-    return getData(i).second;
-  }
-private:    
-  pair<unsigned,StructuredSortInterpretation> getData(Interpretation i){
-    ASS(isStructuredSortInterpretation(i));
-    auto it = _structuredSortInterpretations.items();
-    while(it.hasNext()){
-      auto entry = it.next();
-      if(entry.second==i) return entry.first;
-    }
-    ASSERTION_VIOLATION;
-  }
-
-  DHMap<pair<unsigned,StructuredSortInterpretation>,unsigned> _structuredSortInterpretations;
-
 public:
   class Tuples {
   public:
diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp
index 36f574889e..5416523531 100644
--- a/Parse/SMTLIB2.cpp
+++ b/Parse/SMTLIB2.cpp
@@ -1650,7 +1650,7 @@ bool SMTLIB2::parseAsBuiltinFormulaSymbol(const vstring& id, LExpr* exp)
         lastConjunct = new AtomicFormula(Literal::createEquality(true, first, second, sort));
       } else {
         Interpretation intp = getFormulaSymbolInterpretation(fs,sort);
-        pred = Theory::instance()->getPredNum(intp);
+        pred = env.signature->getInterpretingSymbol(intp);
         lastConjunct = new AtomicFormula(Literal::create2(pred,true,first,second));
       }
 
@@ -1740,7 +1740,7 @@ bool SMTLIB2::parseAsBuiltinFormulaSymbol(const vstring& id, LExpr* exp)
         complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
       }
 
-      unsigned pred = Theory::instance()->getPredNum(Theory::REAL_IS_INT);
+      unsigned pred = env.signature->getInterpretingSymbol(Theory::REAL_IS_INT);
       Formula* res = new AtomicFormula(Literal::create1(pred,true,arg));
 
       _results.push(res);
@@ -1819,7 +1819,7 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp)
         complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
       }
 
-      unsigned fun = Theory::instance()->getFnNum(Theory::INT_TO_REAL);
+      unsigned fun = env.signature->getInterpretingSymbol(Theory::INT_TO_REAL);
       TermList res = TermList(Term::create1(fun,theInt));
 
       _results.push(ParseResult(Sorts::SRT_REAL,res));
@@ -1833,7 +1833,7 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp)
         complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
       }
 
-      unsigned fun = Theory::instance()->getFnNum(Theory::REAL_TO_INT);
+      unsigned fun = env.signature->getInterpretingSymbol(Theory::REAL_TO_INT);
       TermList res = TermList(Term::create1(fun,theReal));
 
       _results.push(ParseResult(Sorts::SRT_INTEGER,res));
@@ -1858,13 +1858,16 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp)
       }
 
       if (arraySort->getInnerSort() == Sorts::SRT_BOOL) {
-        unsigned pred = Theory::instance()->getSymbolForStructuredSort(arraySortIdx,Theory::StructuredSortInterpretation::ARRAY_BOOL_SELECT);
+        OperatorType* predType = Theory::getArrayOperatorType(arraySortIdx,Theory::ARRAY_BOOL_SELECT);
+        unsigned pred = env.signature->getInterpretingSymbol(Theory::ARRAY_BOOL_SELECT,predType);
 
         Formula* res = new AtomicFormula(Literal::create2(pred,true,theArray,theIndex));
 
         _results.push(ParseResult(res));
       } else {
-        unsigned fun = Theory::instance()->getSymbolForStructuredSort(arraySortIdx,Theory::StructuredSortInterpretation::ARRAY_SELECT);
+        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(arraySort->getInnerSort(),res));
@@ -1896,7 +1899,8 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp)
         complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
       }
 
-      unsigned fun = Theory::instance()->getSymbolForStructuredSort(arraySortIdx,Theory::StructuredSortInterpretation::ARRAY_STORE);
+      OperatorType* funType = Theory::getArrayOperatorType(arraySortIdx,Theory::ARRAY_STORE);
+      unsigned fun = env.signature->getInterpretingSymbol(Theory::ARRAY_STORE,funType);
 
       TermList args[] = {theArray, theIndex, theValue};
       TermList res = TermList(Term::Term::create(fun, 3, args));
@@ -1913,7 +1917,7 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp)
         complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
       }
 
-      unsigned fun = Theory::instance()->getFnNum(Theory::INT_ABS);
+      unsigned fun = env.signature->getInterpretingSymbol(Theory::INT_ABS);
       TermList res = TermList(Term::create1(fun,theInt));
 
       _results.push(ParseResult(Sorts::SRT_INTEGER,res));
@@ -1928,7 +1932,7 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp)
         complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
       }
 
-      unsigned fun = Theory::instance()->getFnNum(Theory::INT_REMAINDER_E); // TS_MOD is the always positive remainder, therefore INT_REMAINDER_E
+      unsigned fun = env.signature->getInterpretingSymbol(Theory::INT_REMAINDER_E); // TS_MOD is the always positive remainder, therefore INT_REMAINDER_E
       TermList res = TermList(Term::create2(fun,int1,int2));
 
       _results.push(ParseResult(Sorts::SRT_INTEGER,res));
@@ -1951,7 +1955,7 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp)
       if (_results.isEmpty() || _results.top().isSeparator()) {
         if (ts == TS_MINUS) { // unary minus
           Interpretation intp = getUnaryMinusInterpretation(sort);
-          unsigned fun = Theory::instance()->getFnNum(intp);
+          unsigned fun = env.signature->getInterpretingSymbol(intp);
 
           TermList res = TermList(Term::create1(fun,first));
 
@@ -1964,7 +1968,7 @@ bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp)
       }
 
       Interpretation intp = getTermSymbolInterpretation(ts,sort);
-      unsigned fun = Theory::instance()->getFnNum(intp);
+      unsigned fun = env.signature->getInterpretingSymbol(intp);
 
       TermList second;
       if (_results.pop().asTerm(second) != sort) {
@@ -2021,7 +2025,7 @@ void SMTLIB2::parseRankedFunctionApplication(LExpr* exp)
       complainAboutArgShortageOrWrongSorts("ranked function symbol",exp);
     }
 
-    unsigned pred = Theory::instance()->getPredNum(Theory::INT_DIVIDES);
+    unsigned pred = env.signature->getInterpretingSymbol(Theory::INT_DIVIDES);
     env.signature->recordDividesNvalue(divisorTerm);
 
     Formula* res = new AtomicFormula(Literal::create2(pred,true,divisorTerm,arg));
diff --git a/Parse/TPTP.cpp b/Parse/TPTP.cpp
index c7fc21d4ce..64ebd47a3a 100644
--- a/Parse/TPTP.cpp
+++ b/Parse/TPTP.cpp
@@ -1480,9 +1480,9 @@ void TPTP::endTheoryFunction() {
    * endTermAsFormula().
    */
 
-  Theory::StructuredSortInterpretation ssi;
+  Theory::Interpretation itp;
   TermList args[3]; // all theory function use up to 3 arguments as for now
-  unsigned theorySort;
+  unsigned arraySort;
 
   TheoryFunction tf = _theoryFunctions.pop();
   switch (tf) {
@@ -1490,7 +1490,7 @@ void TPTP::endTheoryFunction() {
       TermList index = _termLists.pop();
       TermList array = _termLists.pop();
 
-      unsigned arraySort = sortOf(array);
+      arraySort = sortOf(array);
       if (!env.sorts->isOfStructuredSort(arraySort, Sorts::StructuredSort::ARRAY)) {
         USER_ERROR("$select is being incorrectly used on a type of array " + env.sorts->sortName(arraySort) + " that has not be defined");
       }
@@ -1502,12 +1502,11 @@ void TPTP::endTheoryFunction() {
 
       args[0] = array;
       args[1] = index;
-      theorySort = arraySort;
 
       if (env.sorts->getArraySort(arraySort)->getInnerSort() == Sorts::SRT_BOOL) {
-        ssi = Theory::StructuredSortInterpretation::ARRAY_BOOL_SELECT;
+        itp = Theory::Interpretation::ARRAY_BOOL_SELECT;
       } else {
-        ssi = Theory::StructuredSortInterpretation::ARRAY_SELECT;
+        itp = Theory::Interpretation::ARRAY_SELECT;
       }
       break;
     }
@@ -1516,7 +1515,7 @@ void TPTP::endTheoryFunction() {
       TermList index = _termLists.pop();
       TermList array = _termLists.pop();
 
-      unsigned arraySort = sortOf(array);
+      arraySort = sortOf(array);
       if (!env.sorts->isOfStructuredSort(arraySort, Sorts::StructuredSort::ARRAY)) {
         USER_ERROR("store is being incorrectly used on a type of array that has not be defined");
       }
@@ -1535,8 +1534,7 @@ void TPTP::endTheoryFunction() {
       args[1] = index;
       args[2] = value;
 
-      ssi = Theory::StructuredSortInterpretation::ARRAY_STORE;
-      theorySort = arraySort;
+      itp = Theory::Interpretation::ARRAY_STORE;
 
       break;
     }
@@ -1544,11 +1542,11 @@ void TPTP::endTheoryFunction() {
       ASSERTION_VIOLATION_REP(tf);
   }
 
-  Interpretation i = Theory::instance()->getInterpretation(theorySort, ssi);
-  unsigned symbol = env.signature->getStructureInterpretationFunctor(theorySort, ssi);
-  unsigned arity = Theory::getArity(i);
+  OperatorType* type = Theory::getArrayOperatorType(arraySort,itp);
+  unsigned symbol = env.signature->getInterpretingSymbol(itp, type);
+  unsigned arity = Theory::getArity(itp);
 
-  if (Theory::isFunction(i)) {
+  if (Theory::isFunction(itp)) {
     Term* term = Term::create(symbol, arity, args);
     _termLists.push(TermList(term));
   } else {
diff --git a/Shell/Property.cpp b/Shell/Property.cpp
index 521b5d673c..63a218e059 100644
--- a/Shell/Property.cpp
+++ b/Shell/Property.cpp
@@ -90,8 +90,7 @@ Property::Property()
     _allQuantifiersEssentiallyExistential(true),
     _smtlibLogic(SMTLIBLogic::SMT_UNDEFINED)
 {
-  //TODO now MaxInterpretedElement is stateful this might be in the wrong place
-  _interpretationPresence.init(Theory::instance()->numberOfInterpretations()+1, false);
+  _interpretationPresence.init(Theory::instance()->numberOfInterpretations(), false);
   env.property = this;
 } // Property::Property
 
@@ -628,17 +627,22 @@ void Property::scanForInterpreted(Term* t)
     itp = theory->interpretFunction(t);
   }
   _hasInterpreted = true;
+
   if(itp < _interpretationPresence.size()){
     _interpretationPresence[itp] = true;
   }
+
+  if (Theory::isPolymorphic(itp)) {
+    OperatorType* type = t->isLiteral() ?
+        env.signature->getPredicate(t->functor())->predType() : env.signature->getFunction(t->functor())->fnType();
+
+    _polymorphicInterpretations.insert(std::make_pair(itp,type));
+  }
+
   if(Theory::isConversionOperation(itp)){
     addProp(PR_NUMBER_CONVERSION);
     return;
   }
-  if(Theory::isArrayOperation(itp)){
-    //addProp(PR_HAS_ARRAYS);
-    return;
-  }
 
   unsigned sort = Theory::getOperationSort(itp);
   if(Theory::isInequality(itp)){
diff --git a/Shell/Property.hpp b/Shell/Property.hpp
index 11139c9519..d760491be7 100644
--- a/Shell/Property.hpp
+++ b/Shell/Property.hpp
@@ -31,6 +31,7 @@
 
 #include "Lib/DArray.hpp"
 #include "Lib/Array.hpp"
+#include "Lib/DHSet.hpp"
 #include "Kernel/Unit.hpp"
 #include "Kernel/Theory.hpp"
 #include "Lib/VString.hpp"
@@ -215,11 +216,14 @@ class Property
    */
   void scanForInterpreted(Term* t);
 
-  bool hasInterpretedOperation(Interpretation i) const { 
+  bool hasInterpretedOperation(Interpretation i) const {
     if(i >= _interpretationPresence.size()){ return false; }
     return _interpretationPresence[i]; 
   }
-  //bool hasArrayOperation(Interpretation i) const { return true; }
+  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; }
   bool hasInterpretedEquality() const { return _hasInterpretedEquality; }
@@ -321,9 +325,14 @@ class Property
   /** Problem contains non-default sorts */
   bool _hasNonDefaultSorts;
   unsigned _sortsUsed;
-  DArray<bool> _interpretationPresence;
   Array<bool> _usesSort;
 
+  /** Makes sense for all interpretations, but for polymorphic ones we also keep
+   *  the more precise information about which monomorphisations are present (see below).
+   */
+  DArray<bool> _interpretationPresence;
+  DHSet<Theory::MonomorphisedInterpretation> _polymorphicInterpretations;
+
   bool _hasFOOL;
 
   bool _onlyFiniteDomainDatatypes;
diff --git a/Shell/TheoryAxioms.cpp b/Shell/TheoryAxioms.cpp
index 19330a6e0f..bd86f78c48 100644
--- a/Shell/TheoryAxioms.cpp
+++ b/Shell/TheoryAxioms.cpp
@@ -828,19 +828,14 @@ 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(Interpretation select,
-                                                Interpretation store,
-                                                unsigned skolemFn)
+void TheoryAxioms::addArrayExtensionalityAxioms(unsigned arraySort, unsigned skolemFn)
 {
   CALL("TheoryAxioms::addArrayExtenstionalityAxioms");
-        
-  ASS(theory->isFunction(select));
-  ASS(theory->isArrayOperation(select));
-  ASS_EQ(theory->getArity(select),2);
-              
-  unsigned sel = env.signature->getInterpretingSymbol(select);
-  unsigned rangeSort = theory->getArrayOperationSort(select);
-  unsigned arraySort = theory->getArrayOperationSort(store);
+
+  unsigned sel = env.signature->getInterpretingSymbol(Theory::ARRAY_SELECT,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_SELECT));
+
+  Sorts::ArraySort* si = env.sorts->getArraySort(arraySort);
+  unsigned rangeSort = si->getInnerSort();
 
   TermList x(0,false);
   TermList y(1,false);
@@ -861,18 +856,13 @@ void TheoryAxioms::addArrayExtensionalityAxioms(Interpretation select,
  * @since 25/08/2015 Gothenburg
  * @author Evgeny Kotelnikov
  */
-void TheoryAxioms::addBooleanArrayExtensionalityAxioms(Interpretation select,
-                                                       Interpretation store,
-                                                       unsigned skolemFn)
+void TheoryAxioms::addBooleanArrayExtensionalityAxioms(unsigned arraySort, unsigned skolemFn)
 {
   CALL("TheoryAxioms::addBooleanArrayExtenstionalityAxioms");
 
-  ASS(!theory->isFunction(select));
-  ASS(theory->isArrayOperation(select));
-  ASS_EQ(theory->getArity(select),2);
+  OperatorType* selectType = Theory::getArrayOperatorType(arraySort,Theory::ARRAY_BOOL_SELECT);
 
-  unsigned sel = env.signature->getInterpretingSymbol(select);
-  unsigned arraySort = theory->getArrayOperationSort(store);
+  unsigned sel = env.signature->getInterpretingSymbol(Theory::ARRAY_BOOL_SELECT,selectType);
 
   TermList x(0,false);
   TermList y(1,false);
@@ -896,22 +886,17 @@ void TheoryAxioms::addBooleanArrayExtensionalityAxioms(Interpretation select,
  * @author Laura Kovacs
  * @since 31/08/2012, Vienna
 */
-void TheoryAxioms::addArrayWriteAxioms(Interpretation select, Interpretation store)
+void TheoryAxioms::addArrayWriteAxioms(unsigned arraySort)
 {
   CALL("TheoryAxioms::addArrayWriteAxioms");
         
-  ASS(theory->isFunction(select));
-  ASS(theory->isArrayOperation(select));
-  ASS_EQ(theory->getArity(select),2);
-        
-        
-  unsigned func_select = env.signature->getInterpretingSymbol(select);
-  unsigned func_store = env.signature->getInterpretingSymbol(store);
+  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));
+
+  Sorts::ArraySort* si = env.sorts->getArraySort(arraySort);
+  unsigned rangeSort = si->getInnerSort();
+  unsigned domainSort = si->getIndexSort();
 
-  unsigned rangeSort = theory->getArrayOperationSort(select);
-  unsigned domainSort = theory->getArrayDomainSort(select);
-  //unsigned arraySort = theory->getOperationSort(store);
-        
   TermList i(0,false);
   TermList j(1,false);
   TermList v(2,false);
@@ -938,20 +923,15 @@ void TheoryAxioms::addArrayWriteAxioms(Interpretation select, Interpretation sto
  * @author Laura Kovacs
  * @since 31/08/2012, Vienna
 */
-void TheoryAxioms::addBooleanArrayWriteAxioms(Interpretation select, Interpretation store)
+void TheoryAxioms::addBooleanArrayWriteAxioms(unsigned arraySort)
 {
   CALL("TheoryAxioms::addArrayWriteAxioms");
 
-  ASS(!theory->isFunction(select));
-  ASS(theory->isArrayOperation(select));
-  ASS_EQ(theory->getArity(select),2);
+  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));
 
-  unsigned pred_select = env.signature->getInterpretingSymbol(select);
-  unsigned func_store = env.signature->getInterpretingSymbol(store);
-
-  //unsigned rangeSort = theory->getArrayOperationSort(select);
-  unsigned domainSort = theory->getArrayDomainSort(select);
-  //unsigned arraySort = theory->getOperationSort(store);
+  Sorts::ArraySort* si = env.sorts->getArraySort(arraySort);
+  unsigned domainSort = si->getIndexSort();
 
   TermList a(0,false);
   TermList i(1,false);
@@ -1161,28 +1141,24 @@ void TheoryAxioms::apply()
     unsigned arraySort = arraySorts.next();
 
     bool isBool = (env.sorts->getArraySort(arraySort)->getInnerSort() == Sorts::SRT_BOOL);
-
-    // Get Interpretation objects for functions 
-    Interpretation arraySelect = theory->getInterpretation(arraySort, isBool ? Theory::StructuredSortInterpretation::ARRAY_BOOL_SELECT
-                                                                             : Theory::StructuredSortInterpretation::ARRAY_SELECT);
-    Interpretation arrayStore  = theory->getInterpretation(arraySort,Theory::StructuredSortInterpretation::ARRAY_STORE);
     
     // Check if they are used
-    bool haveSelect = prop->hasInterpretedOperation(arraySelect);
-    bool haveStore = prop->hasInterpretedOperation(arrayStore);
+    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(arraySelect, arrayStore, sk);
+        addBooleanArrayExtensionalityAxioms(arraySort, sk);
       } else {
-        addArrayExtensionalityAxioms(arraySelect, arrayStore, sk);
+        addArrayExtensionalityAxioms(arraySort, sk);
       }
       if (haveStore) {
         if (isBool) {
-          addBooleanArrayWriteAxioms(arraySelect, arrayStore);
+          addBooleanArrayWriteAxioms(arraySort);
         } else {
-          addArrayWriteAxioms(arraySelect, arrayStore);
+          addArrayWriteAxioms(arraySort);
         }
       }
       modified = true;
diff --git a/Shell/TheoryAxioms.hpp b/Shell/TheoryAxioms.hpp
index b899995ee3..920c187270 100644
--- a/Shell/TheoryAxioms.hpp
+++ b/Shell/TheoryAxioms.hpp
@@ -89,9 +89,11 @@ static unsigned const EXPENSIVE = 1;
                            Interpretation unaryMinus, TermList zeroElement);
   void addIntegerDividesAxioms(Interpretation divides, Interpretation multiply, TermList zero, TermList n);
 
-  void addBooleanArrayExtensionalityAxioms(Interpretation select, Interpretation store, unsigned skolem);
-  void addArrayExtensionalityAxioms(Interpretation select, Interpretation store, unsigned skolem);
-  void addBooleanArrayWriteAxioms(Interpretation select, Interpretation store);
+  void addBooleanArrayExtensionalityAxioms(unsigned arraySort, unsigned skolem);
+  void addArrayExtensionalityAxioms(unsigned arraySort, unsigned skolem);
+  void addBooleanArrayWriteAxioms(unsigned arraySort);
+  void addArrayWriteAxioms(unsigned arraySort);
+
   void addTupleAxioms(unsigned tupleSort);
   void addFloorAxioms(Interpretation floor, Interpretation less, Interpretation unaryMinus,
                       Interpretation plus, TermList oneElement);
@@ -100,7 +102,6 @@ static unsigned const EXPENSIVE = 1;
   void addRoundAxioms(Interpretation round, Interpretation floor, Interpretation ceiling); 
   void addTruncateAxioms(Interpretation truncate, Interpretation less, Interpretation unaryMinus,
                       Interpretation plus, TermList zeroElement, TermList oneElement);
-  void addArrayWriteAxioms(Interpretation select, Interpretation store);
 
   // term algebra axioms
   void addExhaustivenessAxiom(TermAlgebra* ta);