diff --git a/Indexing/ClauseCodeTree.cpp b/Indexing/ClauseCodeTree.cpp
index b820f4e3ef..a2023edeec 100644
--- a/Indexing/ClauseCodeTree.cpp
+++ b/Indexing/ClauseCodeTree.cpp
@@ -36,14 +36,16 @@ using namespace std;
 using namespace Lib;
 using namespace Kernel;
 
-void ClauseCodeTree::onCodeOpDestroying(CodeOp* op)
+template<bool higherOrder>
+void ClauseCodeTree<higherOrder>::onCodeOpDestroying(CodeOp* op)
 {
   if (op->isLitEnd()) {
     delete op->getILS(); 
   }
 }
 
-ClauseCodeTree::ClauseCodeTree()
+template<bool higherOrder>
+ClauseCodeTree<higherOrder>::ClauseCodeTree()
 {
   _clauseCodeTree=true;
   _onCodeOpDestroying = onCodeOpDestroying;
@@ -54,7 +56,8 @@ ClauseCodeTree::ClauseCodeTree()
 
 //////////////// insertion ////////////////////
 
-void ClauseCodeTree::insert(Clause* cl)
+template<bool higherOrder>
+void ClauseCodeTree<higherOrder>::insert(Clause* cl)
 {
   unsigned clen=cl->length();
   static DArray<Literal*> lits;
@@ -77,7 +80,8 @@ void ClauseCodeTree::insert(Clause* cl)
   ASS(code.isEmpty());
 }
 
-struct ClauseCodeTree::InitialLiteralOrderingComparator
+template<bool higherOrder>
+struct ClauseCodeTree<higherOrder>::InitialLiteralOrderingComparator
 {
   Comparison compare(Literal* l1, Literal* l2)
   {
@@ -88,7 +92,8 @@ struct ClauseCodeTree::InitialLiteralOrderingComparator
   }
 };
 
-void ClauseCodeTree::optimizeLiteralOrder(DArray<Literal*>& lits)
+template<bool higherOrder>
+void ClauseCodeTree<higherOrder>::optimizeLiteralOrder(DArray<Literal*>& lits)
 {
   unsigned clen=lits.size();
   if(isEmpty() || clen<=1) {
@@ -139,7 +144,8 @@ void ClauseCodeTree::optimizeLiteralOrder(DArray<Literal*>& lits)
   }
 }
 
-void ClauseCodeTree::evalSharing(Literal* lit, CodeOp* startOp, size_t& sharedLen, size_t& unsharedLen, CodeOp*& nextOp)
+template<bool higherOrder>
+void ClauseCodeTree<higherOrder>::evalSharing(Literal* lit, CodeOp* startOp, size_t& sharedLen, size_t& unsharedLen, CodeOp*& nextOp)
 {
   CodeStack code;
   LitCompiler compiler(code);
@@ -163,7 +169,8 @@ void ClauseCodeTree::evalSharing(Literal* lit, CodeOp* startOp, size_t& sharedLe
  * it is the first operation on which mismatch occurred and there was no alternative to
  * proceed to (in this case it therefore holds that @b lastAttemptedOp->alternative==0 ).
  */
-void ClauseCodeTree::matchCode(CodeStack& code, CodeOp* startOp, size_t& matchedCnt, CodeOp*& nextOp)
+template<bool higherOrder>
+void ClauseCodeTree<higherOrder>::matchCode(CodeStack& code, CodeOp* startOp, size_t& matchedCnt, CodeOp*& nextOp)
 {
   size_t clen=code.length();
   CodeOp* treeOp=startOp;
@@ -207,7 +214,8 @@ void ClauseCodeTree::matchCode(CodeStack& code, CodeOp* startOp, size_t& matched
 
 //////////////// removal ////////////////////
 
-void ClauseCodeTree::remove(Clause* cl)
+template<bool higherOrder>
+void ClauseCodeTree<higherOrder>::remove(Clause* cl)
 {
   static DArray<LitInfo> lInfos;
   Recycled<Stack<CodeOp*>> firstsInBlocks;
@@ -283,19 +291,21 @@ void ClauseCodeTree::remove(Clause* cl)
   }
 }
 
-void ClauseCodeTree::RemovingLiteralMatcher::init(CodeOp* entry_, LitInfo* linfos_,
+template<bool higherOrder>
+void ClauseCodeTree<higherOrder>::RemovingLiteralMatcher::init(CodeOp* entry_, LitInfo* linfos_,
     size_t linfoCnt_, ClauseCodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_)
 {
-  Matcher::init(tree_, entry_, linfos_, linfoCnt_, firstsInBlocks_);
+  Base::init(tree_, entry_, linfos_, linfoCnt_, firstsInBlocks_);
 
-  ALWAYS(prepareLiteral());
+  ALWAYS(Base::prepareLiteral());
 }
 
 /**
  * The first operation of the CodeBlock containing @b op
  * must already be on the @b firstsInBlocks stack.
  */
-bool ClauseCodeTree::removeOneOfAlternatives(CodeOp* op, Clause* cl, Stack<CodeOp*>* firstsInBlocks)
+template<bool higherOrder>
+bool ClauseCodeTree<higherOrder>::removeOneOfAlternatives(CodeOp* op, Clause* cl, Stack<CodeOp*>* firstsInBlocks)
 {
   unsigned initDepth=firstsInBlocks->size();
 
@@ -320,13 +330,14 @@ bool ClauseCodeTree::removeOneOfAlternatives(CodeOp* op, Clause* cl, Stack<CodeO
  * If @b seekOnlySuccess if true, we will look only for immediate SUCCESS operations
  *  and fail if there isn't any at the beginning (possibly also among alternatives).
  */
-void ClauseCodeTree::LiteralMatcher::init(CodeTree* tree_, CodeOp* entry_,
+template<bool higherOrder>
+void ClauseCodeTree<higherOrder>::LiteralMatcher::init(CodeTree* tree_, CodeOp* entry_,
 					  LitInfo* linfos_, size_t linfoCnt_,
 					  bool seekOnlySuccess)
 {
   ASS_G(linfoCnt_,0);
 
-  Matcher::init(tree_,entry_,linfos_,linfoCnt_);
+  Base::init(tree_,entry_,linfos_,linfoCnt_);
 
   _eagerlyMatched=false;
   eagerResults.reset();
@@ -338,24 +349,25 @@ void ClauseCodeTree::LiteralMatcher::init(CodeTree* tree_, CodeOp* entry_,
     //(and those must be at the entry point or its alternatives)
 
     _eagerlyMatched=true;
-    fresh=false;
-    CodeOp* sop=entry;
+    Base::fresh=false;
+    CodeOp* sop=Base::entry;
     while(sop) {
       if(sop->isSuccess()) {
-	eagerResults.push(sop);
+        eagerResults.push(sop);
       }
       sop=sop->alternative();
     }
     return;
   }
 
-  ALWAYS(prepareLiteral());
+  ALWAYS(Base::prepareLiteral());
 }
 
 /**
  * Try to find a match, and if one is found, return true
  */
-bool ClauseCodeTree::LiteralMatcher::next()
+template<bool higherOrder>
+bool ClauseCodeTree<higherOrder>::LiteralMatcher::next()
 {
   if(eagerlyMatched()) {
     _matched=!eagerResults.isEmpty();
@@ -386,7 +398,8 @@ bool ClauseCodeTree::LiteralMatcher::next()
 /**
  * Perform eager matching and return true iff new matches were found
  */
-bool ClauseCodeTree::LiteralMatcher::doEagerMatching()
+template<bool higherOrder>
+bool ClauseCodeTree<higherOrder>::LiteralMatcher::doEagerMatching()
 {
   ASS(!eagerlyMatched()); //eager matching can be done only once
   ASS(eagerResults.isEmpty());
@@ -430,21 +443,22 @@ bool ClauseCodeTree::LiteralMatcher::doEagerMatching()
   return eagerResults.isNonEmpty();
 }
 
-void ClauseCodeTree::LiteralMatcher::recordMatch()
+template<bool higherOrder>
+void ClauseCodeTree<higherOrder>::LiteralMatcher::recordMatch()
 {
-  ASS(matched());
+  ASS(_matched);
 
   ILStruct* ils=op->getILS();
-  ils->ensureFreshness(tree->_curTimeStamp);
+  ils->ensureFreshness(Base::tree->_curTimeStamp);
   if(ils->finished) {
     //no need to record matches which we already know will not lead to anything
     return;
   }
-  if(!ils->matchCnt && linfos[curLInfo].opposite) {
+  if(!ils->matchCnt && Base::linfos[Base::curLInfo].opposite) {
     //if we're matching opposite matches, we have already tried all non-opposite ones
     ils->noNonOppositeMatches=true;
   }
-  ils->addMatch(linfos[curLInfo].liIndex, bindings);
+  ils->addMatch(Base::linfos[Base::curLInfo].liIndex, Base::bindings);
 }
 
 
@@ -455,7 +469,8 @@ void ClauseCodeTree::LiteralMatcher::recordMatch()
  * of the @b query_ clause.
  * If @b sres_ if true, we perform subsumption resolution
  */
-void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Clause* query_, bool sres_)
+template<bool higherOrder>
+void ClauseCodeTree<higherOrder>::ClauseMatcher::init(ClauseCodeTree* tree_, Clause* query_, bool sres_)
 {
   ASS(!tree_->isEmpty());
 
@@ -521,7 +536,8 @@ void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Clause* query_,
   enterLiteral(tree->getEntryPoint(), clen==0);
 }
 
-void ClauseCodeTree::ClauseMatcher::reset()
+template<bool higherOrder>
+void ClauseCodeTree<higherOrder>::ClauseMatcher::reset()
 {
   unsigned liCnt=lInfos.size();
   for(unsigned i=0;i<liCnt;i++) {
@@ -538,7 +554,8 @@ void ClauseCodeTree::ClauseMatcher::reset()
 /**
  * Return next clause matching query or 0 if there is not such
  */
-Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit)
+template<bool higherOrder>
+Clause* ClauseCodeTree<higherOrder>::ClauseMatcher::next(int& resolvedQueryLit)
 {
   if(lms.isEmpty()) {
     return 0;
@@ -558,7 +575,7 @@ Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit)
       }
     }
     else if(lm->op->isSuccess()) {
-      Clause* candidate=lm->op->getSuccessResult<Clause>();
+      Clause* candidate=lm->op->template getSuccessResult<Clause>();
       RSTAT_MCTR_INC("candidates", lms.size()-1);
       if(checkCandidate(candidate, resolvedQueryLit)) {
 	RSTAT_MCTR_INC("candidates (success)", lms.size()-1);
@@ -589,7 +606,8 @@ Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit)
   }
 }
 
-inline bool ClauseCodeTree::ClauseMatcher::canEnterLiteral(CodeOp* op)
+template<bool higherOrder>
+inline bool ClauseCodeTree<higherOrder>::ClauseMatcher::canEnterLiteral(CodeOp* op)
 {
   ASS(op->isLitEnd());
   ASS_EQ(lms.top()->op, op);
@@ -638,7 +656,8 @@ inline bool ClauseCodeTree::ClauseMatcher::canEnterLiteral(CodeOp* op)
  *   (this is to be used when all literals are matched so we want
  *   to see just clauses that end at this point).
  */
-void ClauseCodeTree::ClauseMatcher::enterLiteral(CodeOp* entry, bool seekOnlySuccess)
+template<bool higherOrder>
+void ClauseCodeTree<higherOrder>::ClauseMatcher::enterLiteral(CodeOp* entry, bool seekOnlySuccess)
 {
   if(!seekOnlySuccess) {
     RSTAT_MCTR_INC("enterLiteral levels (non-sos)", lms.size());
@@ -669,7 +688,8 @@ void ClauseCodeTree::ClauseMatcher::enterLiteral(CodeOp* entry, bool seekOnlySuc
   lms.push(std::move(lm));
 }
 
-void ClauseCodeTree::ClauseMatcher::leaveLiteral()
+template<bool higherOrder>
+void ClauseCodeTree<higherOrder>::ClauseMatcher::leaveLiteral()
 {
   ASS(lms.isNonEmpty());
 
@@ -697,7 +717,8 @@ void ClauseCodeTree::ClauseMatcher::leaveLiteral()
 
 //////////////// Multi-literal matching
 
-bool ClauseCodeTree::ClauseMatcher::checkCandidate(Clause* cl, int& resolvedQueryLit)
+template<bool higherOrder>
+bool ClauseCodeTree<higherOrder>::ClauseMatcher::checkCandidate(Clause* cl, int& resolvedQueryLit)
 {
   unsigned clen=cl->length();
   //the last matcher in mls is the one that yielded the SUCCESS operation
@@ -752,7 +773,8 @@ bool ClauseCodeTree::ClauseMatcher::checkCandidate(Clause* cl, int& resolvedQuer
 //  return newMatches && matchGlobalVars(resolvedQueryLit);
 }
 
-bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQueryLit)
+template<bool higherOrder>
+bool ClauseCodeTree<higherOrder>::ClauseMatcher::matchGlobalVars(int& resolvedQueryLit)
 {
   //TODO: perform _set_, not _multiset_ subsumption for subsumption resolution
 
@@ -849,7 +871,8 @@ bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQueryLit)
   return true;
 }
 
-bool ClauseCodeTree::ClauseMatcher::compatible(ILStruct* bi, MatchInfo* bq, ILStruct* ni, MatchInfo* nq)
+template<bool higherOrder>
+bool ClauseCodeTree<higherOrder>::ClauseMatcher::compatible(ILStruct* bi, MatchInfo* bq, ILStruct* ni, MatchInfo* nq)
 {
   if( lInfos[bq->liIndex].litIndex==lInfos[nq->liIndex].litIndex ||
       (lInfos[bq->liIndex].opposite && lInfos[nq->liIndex].opposite) ) {
@@ -894,7 +917,8 @@ bool ClauseCodeTree::ClauseMatcher::compatible(ILStruct* bi, MatchInfo* bq, ILSt
   return true;
 }
 
-bool ClauseCodeTree::ClauseMatcher::existsCompatibleMatch(ILStruct* si, MatchInfo* sq, ILStruct* targets)
+template<bool higherOrder>
+bool ClauseCodeTree<higherOrder>::ClauseMatcher::existsCompatibleMatch(ILStruct* si, MatchInfo* sq, ILStruct* targets)
 {
   size_t tcnt=targets->matchCnt;
   for(size_t i=0;i<tcnt;i++) {
@@ -905,4 +929,7 @@ bool ClauseCodeTree::ClauseMatcher::existsCompatibleMatch(ILStruct* si, MatchInf
   return false;
 }
 
+template class ClauseCodeTree<false>;
+template class ClauseCodeTree<true>;
+
 }
diff --git a/Indexing/ClauseCodeTree.hpp b/Indexing/ClauseCodeTree.hpp
index a6eb6298a2..8aed172fc6 100644
--- a/Indexing/ClauseCodeTree.hpp
+++ b/Indexing/ClauseCodeTree.hpp
@@ -29,6 +29,7 @@ namespace Indexing {
 using namespace Lib;
 using namespace Kernel;
 
+template<bool higherOrder>
 class ClauseCodeTree : public CodeTree
 {
 protected:
@@ -55,8 +56,10 @@ class ClauseCodeTree : public CodeTree
   bool removeOneOfAlternatives(CodeOp* op, Clause* cl, Stack<CodeOp*>* firstsInBlocks);
 
   struct RemovingLiteralMatcher
-  : public Matcher</*removing*/true,false>
+  : public Matcher</*removing*/true,false,higherOrder>
   {
+    using Base = Matcher</*removing*/true,false,higherOrder>;
+
     void init(CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_,
 	ClauseCodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_);
 
@@ -69,15 +72,21 @@ class ClauseCodeTree : public CodeTree
    *
    * Here the actual execution of the code of the tree takes place */
   struct LiteralMatcher
-  : public Matcher</*removing*/false,false>
+  : public Matcher</*removing*/false,false,higherOrder>
   {
+    using Base = Matcher</*removing*/false,false,higherOrder>;
+    using Base::op;
+    using Base::_matched;
+    using Base::finished;
+    using Base::execute;
+
     void init(CodeTree* tree, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, bool seekOnlySuccess=false);
     bool next();
     bool doEagerMatching();
 
     inline bool eagerlyMatched() const { return _eagerlyMatched; }
 
-    inline ILStruct* getILS() { ASS(matched()); return op->getILS(); }
+    inline ILStruct* getILS() { ASS(Base::matched()); return op->getILS(); }
 
     USE_ALLOCATOR(LiteralMatcher);
 
diff --git a/Indexing/CodeTree.cpp b/Indexing/CodeTree.cpp
index 64deb82d2e..99331ce533 100644
--- a/Indexing/CodeTree.cpp
+++ b/Indexing/CodeTree.cpp
@@ -522,8 +522,8 @@ CodeTree::CodeOp*& CodeTree::SearchStructImpl<k>::targetOp(const T& val)
 
 //////////////// Matcher ////////////////////
 
-template<bool removing, bool checkRange>
-bool CodeTree::Matcher<removing, checkRange>::execute()
+template<bool removing, bool checkRange, bool higherOrder>
+bool CodeTree::Matcher<removing, checkRange, higherOrder>::execute()
 {
   if(fresh) {
     fresh=false;
@@ -582,11 +582,7 @@ bool CodeTree::Matcher<removing, checkRange>::execute()
         shouldBacktrack=!doCheckFun();
         break;
       case ASSIGN_VAR:
-        if constexpr (removing) {
-          shouldBacktrack=!doAssignVar();
-        } else {
-          doAssignVar();
-        }
+        shouldBacktrack=!doAssignVar();
         break;
       case CHECK_VAR:
         shouldBacktrack=!doCheckVar();
@@ -621,8 +617,8 @@ bool CodeTree::Matcher<removing, checkRange>::execute()
   }
 }
 
-template<bool removing, bool checkRange>
-void CodeTree::Matcher<removing, checkRange>::init(CodeTree* tree_, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, Stack<CodeOp*>* firstsInBlocks_)
+template<bool removing, bool checkRange, bool higherOrder>
+void CodeTree::Matcher<removing, checkRange, higherOrder>::init(CodeTree* tree_, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, Stack<CodeOp*>* firstsInBlocks_)
 {
   tree=tree_;
   entry=entry_;
@@ -651,8 +647,8 @@ void CodeTree::Matcher<removing, checkRange>::init(CodeTree* tree_, CodeOp* entr
  * entry point and starts evaluating new literal info (if there
  * is some left).
  */
-template<bool removing, bool checkRange>
-bool CodeTree::Matcher<removing, checkRange>::backtrack()
+template<bool removing, bool checkRange, bool higherOrder>
+bool CodeTree::Matcher<removing, checkRange, higherOrder>::backtrack()
 {
   if(btStack.isEmpty()) {
     curLInfo++;
@@ -668,8 +664,8 @@ bool CodeTree::Matcher<removing, checkRange>::backtrack()
   return true;
 }
 
-template<bool removing, bool checkRange>
-bool CodeTree::Matcher<removing, checkRange>::prepareLiteral()
+template<bool removing, bool checkRange, bool higherOrder>
+bool CodeTree::Matcher<removing, checkRange, higherOrder>::prepareLiteral()
 {
   if constexpr (removing) {
     RemovingBase::firstsInBlocks->truncate(RemovingBase::initFIBDepth);
@@ -683,8 +679,8 @@ bool CodeTree::Matcher<removing, checkRange>::prepareLiteral()
   return true;
 }
 
-template<bool removing, bool checkRange>
-inline bool CodeTree::Matcher<removing, checkRange>::doAssignVar()
+template<bool removing, bool checkRange, bool higherOrder>
+inline bool CodeTree::Matcher<removing, checkRange, higherOrder>::doAssignVar()
 {
   ASS_EQ(op->_instruction(), ASSIGN_VAR);
 
@@ -709,6 +705,13 @@ inline bool CodeTree::Matcher<removing, checkRange>::doAssignVar()
     fte++;
     ASS_EQ(fte->_tag(), FlatTerm::FUN_TERM_PTR);
     ASS(fte->_term());
+    if constexpr (higherOrder) {
+      // When dealing with HOL we want to avoid binding to
+      // any terms that contain loose DB indices.
+      if (TermList(fte->_term()).containsLooseDBIndex()) {
+        return false;
+      }
+    }
     bindings[var]=TermList(fte->_term());
     fte++;
     ASS_EQ(fte->_tag(), FlatTerm::FUN_RIGHT_OFS);
@@ -717,8 +720,8 @@ inline bool CodeTree::Matcher<removing, checkRange>::doAssignVar()
   return true;
 }
 
-template<bool removing, bool checkRange>
-inline bool CodeTree::Matcher<removing, checkRange>::doCheckVar()
+template<bool removing, bool checkRange, bool higherOrder>
+inline bool CodeTree::Matcher<removing, checkRange, higherOrder>::doCheckVar()
 {
   ASS_EQ(op->_instruction(), CHECK_VAR);
 
@@ -749,8 +752,8 @@ inline bool CodeTree::Matcher<removing, checkRange>::doCheckVar()
   return true;
 }
 
-template<bool removing, bool checkRange>
-inline bool CodeTree::Matcher<removing, checkRange>::doCheckFun()
+template<bool removing, bool checkRange, bool higherOrder>
+inline bool CodeTree::Matcher<removing, checkRange, higherOrder>::doCheckFun()
 {
   ASS_EQ(op->_instruction(), CHECK_FUN);
 
@@ -764,8 +767,8 @@ inline bool CodeTree::Matcher<removing, checkRange>::doCheckFun()
   return true;
 }
 
-template<bool removing, bool checkRange>
-inline bool CodeTree::Matcher<removing, checkRange>::doCheckGroundTerm()
+template<bool removing, bool checkRange, bool higherOrder>
+inline bool CodeTree::Matcher<removing, checkRange, higherOrder>::doCheckGroundTerm()
 {
   ASS_EQ(op->_instruction(), CHECK_GROUND_TERM);
 
@@ -788,8 +791,8 @@ inline bool CodeTree::Matcher<removing, checkRange>::doCheckGroundTerm()
   return true;
 }
 
-template<bool removing, bool checkRange>
-inline bool CodeTree::Matcher<removing, checkRange>::doSearchStruct()
+template<bool removing, bool checkRange, bool higherOrder>
+inline bool CodeTree::Matcher<removing, checkRange, higherOrder>::doSearchStruct()
 {
   ASS_EQ(op->_instruction(), SEARCH_STRUCT);
 
@@ -805,9 +808,11 @@ inline bool CodeTree::Matcher<removing, checkRange>::doSearchStruct()
   return true;
 }
 
-template struct CodeTree::Matcher<true, false>;
-template struct CodeTree::Matcher<true, true>;
-template struct CodeTree::Matcher<false, false>;
+template struct CodeTree::Matcher<true, false, false>;
+template struct CodeTree::Matcher<true, false, true>;
+template struct CodeTree::Matcher<true, true, false>;
+template struct CodeTree::Matcher<false, false, false>;
+template struct CodeTree::Matcher<false, false, true>;
 
 //////////////// auxiliary ////////////////////
 
diff --git a/Indexing/CodeTree.hpp b/Indexing/CodeTree.hpp
index 58ab1e56ce..02d7a0aacc 100644
--- a/Indexing/CodeTree.hpp
+++ b/Indexing/CodeTree.hpp
@@ -20,6 +20,7 @@
 #include "Lib/Allocator.hpp"
 #include "Lib/DArray.hpp"
 #include "Lib/DHMap.hpp"
+#include "Lib/Environment.hpp"
 #include "Lib/Stack.hpp"
 #include "Lib/Vector.hpp"
 
@@ -326,7 +327,7 @@ class CodeTree
    * this one. After use, the @b deinit function should be called (if
    * present). This allows for reuse of a single object.
    */
-  template<bool removing, bool checkRange>
+  template<bool removing, bool checkRange, bool higherOrder>
   struct Matcher
     : public std::conditional<removing, RemovingBase, NonRemovingBase>::type
   {
diff --git a/Indexing/CodeTreeInterfaces.cpp b/Indexing/CodeTreeInterfaces.cpp
index ce73a90480..0e973033f0 100644
--- a/Indexing/CodeTreeInterfaces.cpp
+++ b/Indexing/CodeTreeInterfaces.cpp
@@ -86,8 +86,8 @@ class CodeTreeSubstitution
 
 ///////////////////////////////////////
 
-template<class Data>
-class CodeTreeTIS<Data>::ResultIterator
+template<bool higherOrder, class Data>
+class CodeTreeTIS<higherOrder, Data>::ResultIterator
 : public IteratorCore<QueryRes<ResultSubstitutionSP, Data>>
 {
 public:
@@ -150,11 +150,11 @@ class CodeTreeTIS<Data>::ResultIterator
   Data* _found;
   bool _finished;
   CodeTreeTIS* _tree;
-  Recycled<typename TermCodeTree<Data>::TermMatcher> _matcher;
+  Recycled<typename TermCodeTree<higherOrder, Data>::TermMatcher> _matcher;
 };
 
-template<class Data>
-VirtualIterator<QueryRes<ResultSubstitutionSP, Data>> CodeTreeTIS<Data>::getGeneralizations(TypedTermList t, bool retrieveSubstitutions)
+template<bool higherOrder, class Data>
+VirtualIterator<QueryRes<ResultSubstitutionSP, Data>> CodeTreeTIS<higherOrder, Data>::getGeneralizations(TypedTermList t, bool retrieveSubstitutions)
 {
   if(_ct.isEmpty()) {
     return VirtualIterator<QueryRes<ResultSubstitutionSP, Data>>::getEmpty();
@@ -163,14 +163,14 @@ VirtualIterator<QueryRes<ResultSubstitutionSP, Data>> CodeTreeTIS<Data>::getGene
   return vi( new ResultIterator(this, t, retrieveSubstitutions) );
 }
 
-template<class Data>
-bool CodeTreeTIS<Data>::generalizationExists(TermList t)
+template<bool higherOrder, class Data>
+bool CodeTreeTIS<higherOrder, Data>::generalizationExists(TermList t)
 {
   if(_ct.isEmpty()) {
     return false;
   }
 
-  static typename TermCodeTree<Data>::TermMatcher tm;
+  static typename TermCodeTree<higherOrder, Data>::TermMatcher tm;
   
   tm.init(&_ct, t);
   bool res=tm.next();
@@ -179,12 +179,15 @@ bool CodeTreeTIS<Data>::generalizationExists(TermList t)
   return res;
 }
 
-template class CodeTreeTIS<TermLiteralClause>;
-template class CodeTreeTIS<DemodulatorData>;
+template class CodeTreeTIS<false, TermLiteralClause>;
+template class CodeTreeTIS<true,  TermLiteralClause>;
+template class CodeTreeTIS<false, DemodulatorData>;
+template class CodeTreeTIS<true,  DemodulatorData>;
 
 /////////////////   CodeTreeSubsumptionIndex   //////////////////////
 
-void CodeTreeSubsumptionIndex::handleClause(Clause* cl, bool adding)
+template<bool higherOrder>
+void CodeTreeSubsumptionIndex<higherOrder>::handleClause(Clause* cl, bool adding)
 {
   TIME_TRACE("codetree subsumption index maintenance");
 
@@ -196,4 +199,7 @@ void CodeTreeSubsumptionIndex::handleClause(Clause* cl, bool adding)
   }
 }
 
+template class CodeTreeSubsumptionIndex<false>;
+template class CodeTreeSubsumptionIndex<true>;
+
 }
diff --git a/Indexing/CodeTreeInterfaces.hpp b/Indexing/CodeTreeInterfaces.hpp
index aecf1a733d..db5b25fd02 100644
--- a/Indexing/CodeTreeInterfaces.hpp
+++ b/Indexing/CodeTreeInterfaces.hpp
@@ -34,7 +34,7 @@ using namespace Lib;
  * Term indexing structure using code trees to retrieve generalizations
  */
 
-template<class Data>
+template<bool higherOrder, class Data>
 class CodeTreeTIS : public TermIndexingStructure<Data>
 {
 public:
@@ -60,20 +60,21 @@ class CodeTreeTIS : public TermIndexingStructure<Data>
 private:
   class ResultIterator;
 
-  TermCodeTree<Data> _ct;
+  TermCodeTree<higherOrder, Data> _ct;
 };
 
+template<bool higherOrder>
 class CodeTreeSubsumptionIndex
 : public Index
 {
 public:
   CodeTreeSubsumptionIndex(SaturationAlgorithm&) {}
-  ClauseCodeTree* getClauseCodeTree() { return &_ct; }
+  ClauseCodeTree<higherOrder>* getClauseCodeTree() { return &_ct; }
 protected:
   void handleClause(Clause* c, bool adding) override;
 private:
 
-  ClauseCodeTree _ct;
+  ClauseCodeTree<higherOrder> _ct;
 };
 
 };
diff --git a/Indexing/IndexManager.cpp b/Indexing/IndexManager.cpp
index d6b2d70f28..8e3b382497 100644
--- a/Indexing/IndexManager.cpp
+++ b/Indexing/IndexManager.cpp
@@ -33,14 +33,16 @@ using namespace Indexing;
 
 SIMP_INDEX_IMPL(AlascaIndex<ALASCA::Demodulation::Lhs>)
 SIMP_INDEX_IMPL(AlascaIndex<ALASCA::Demodulation::Rhs>)
-SIMP_INDEX_IMPL(DemodulationLHSIndex)
-SIMP_INDEX_IMPL(CodeTreeSubsumptionIndex)
+SIMP_INDEX_IMPL(DemodulationLHSIndex<false>)
+SIMP_INDEX_IMPL(DemodulationLHSIndex<true>)
+SIMP_INDEX_IMPL(CodeTreeSubsumptionIndex<false>)
+SIMP_INDEX_IMPL(CodeTreeSubsumptionIndex<true>)
 SIMP_INDEX_IMPL(BackwardSubsumptionIndex)
 SIMP_INDEX_IMPL(FwSubsSimplifyingLiteralIndex)
 SIMP_INDEX_IMPL(RewriteRuleIndex)
 SIMP_INDEX_IMPL(UnitClauseLiteralIndex)
-SIMP_INDEX_IMPL(DemodulationSubtermIndex<true>)
 SIMP_INDEX_IMPL(DemodulationSubtermIndex<false>)
+SIMP_INDEX_IMPL(DemodulationSubtermIndex<true>)
 SIMP_INDEX_IMPL(SkolemisingFormulaIndex)
 SIMP_INDEX_IMPL(FSDLiteralIndex)
 
diff --git a/Indexing/TermCodeTree.cpp b/Indexing/TermCodeTree.cpp
index b4822683bf..e16ce5de87 100644
--- a/Indexing/TermCodeTree.cpp
+++ b/Indexing/TermCodeTree.cpp
@@ -25,23 +25,23 @@ namespace Indexing
 using namespace Lib;
 using namespace Kernel;
 
-template<class Data>
-void TermCodeTree<Data>::onCodeOpDestroying(CodeOp* op)
+template<bool higherOrder, class Data>
+void TermCodeTree<higherOrder, Data>::onCodeOpDestroying(CodeOp* op)
 {
   if (op->isSuccess()) {
     delete op->getSuccessResult<Data>();
   }
 }
 
-template<class Data>
-TermCodeTree<Data>::TermCodeTree()
+template<bool higherOrder, class Data>
+TermCodeTree<higherOrder, Data>::TermCodeTree()
 {
   _clauseCodeTree=false;
   _onCodeOpDestroying = onCodeOpDestroying;
 }
 
-template<class Data>
-void TermCodeTree<Data>::insert(Data* data)
+template<bool higherOrder, class Data>
+void TermCodeTree<higherOrder, Data>::insert(Data* data)
 {
   static CodeStack code;
   code.reset();
@@ -66,8 +66,8 @@ void TermCodeTree<Data>::insert(Data* data)
 
 //////////////// removal ////////////////////
 
-template<class Data>
-void TermCodeTree<Data>::remove(const Data& data)
+template<bool higherOrder, class Data>
+void TermCodeTree<higherOrder, Data>::remove(const Data& data)
 {
   static RemovingTermMatcher rtm;
   static Stack<CodeOp*> firstsInBlocks;
@@ -118,46 +118,43 @@ void TermCodeTree<Data>::remove(const Data& data)
   */
 } // TermCodeTree::remove
 
-template<class Data>
-void TermCodeTree<Data>::RemovingTermMatcher::init(FlatTerm* ft_,
+template<bool higherOrder, class Data>
+void TermCodeTree<higherOrder, Data>::RemovingTermMatcher::init(FlatTerm* ft_,
 					     TermCodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_)
 {
-  Matcher::init(tree_, tree_->getEntryPoint(), 0, 0, firstsInBlocks_);
+  Base::init(tree_, tree_->getEntryPoint(), /*linfos_=*/0, /*linfoCnt_=*/0, firstsInBlocks_);
   
-  firstsInBlocks->push(entry);
+  Base::firstsInBlocks->push(Base::entry);
 
-  ft=ft_;
-  tp=0;
-  op=entry;
+  Base::ft=ft_;
+  Base::tp=0;
+  Base::op=Base::entry;
 }
 
 //////////////// retrieval ////////////////////
 
-template<class Data>
-TermCodeTree<Data>::TermMatcher::TermMatcher()
+template<bool higherOrder, class Data>
+TermCodeTree<higherOrder, Data>::TermMatcher::TermMatcher()
 {
 #if VDEBUG
   ft=0;
 #endif
 }
 
-template<class Data>
-void TermCodeTree<Data>::TermMatcher::init(CodeTree* tree, TermList t)
+template<bool higherOrder, class Data>
+void TermCodeTree<higherOrder, Data>::TermMatcher::init(CodeTree* tree, TermList t)
 {
-  Matcher::init(tree,tree->getEntryPoint());
-
-  linfos=0;
-  linfoCnt=0;
+  Base::init(tree,tree->getEntryPoint(),/*linfos_=*/0,/*linfoCnt_=*/0);
 
   ASS(!ft);
   ft = FlatTerm::createUnexpanded(t);
 
-  op=entry;
-  tp=0;
+  Base::op=Base::entry;
+  Base::tp=0;
 }
 
-template<class Data>
-void TermCodeTree<Data>::TermMatcher::reset()
+template<bool higherOrder, class Data>
+void TermCodeTree<higherOrder, Data>::TermMatcher::reset()
 {
   ft->destroy();
 #if VDEBUG
@@ -165,24 +162,26 @@ void TermCodeTree<Data>::TermMatcher::reset()
 #endif
 }
 
-template<class Data>
-Data* TermCodeTree<Data>::TermMatcher::next()
+template<bool higherOrder, class Data>
+Data* TermCodeTree<higherOrder, Data>::TermMatcher::next()
 {
-  if (finished()) {
+  if (Base::finished()) {
     //all possible matches are exhausted
     return 0;
   }
   
-  _matched=execute();
-  if (!_matched) {
+  Base::_matched=Base::execute();
+  if (!Base::_matched) {
     return 0;
   }
 
-  ASS(op->isSuccess());
-  return op->getSuccessResult<Data>();
+  ASS(Base::op->isSuccess());
+  return Base::op->template getSuccessResult<Data>();
 }
 
-template class TermCodeTree<TermLiteralClause>;
-template class TermCodeTree<DemodulatorData>;
+template class TermCodeTree<false, TermLiteralClause>;
+template class TermCodeTree<true,  TermLiteralClause>;
+template class TermCodeTree<false, DemodulatorData>;
+template class TermCodeTree<true,  DemodulatorData>;
 
 };
diff --git a/Indexing/TermCodeTree.hpp b/Indexing/TermCodeTree.hpp
index 75aa8f790c..1119a2b6f9 100644
--- a/Indexing/TermCodeTree.hpp
+++ b/Indexing/TermCodeTree.hpp
@@ -19,7 +19,6 @@
 
 #include "Lib/Allocator.hpp"
 #include "Lib/Stack.hpp"
-#include "Lib/Vector.hpp"
 
 #include "CodeTree.hpp"
 
@@ -29,7 +28,7 @@ namespace Indexing {
 using namespace Lib;
 using namespace Kernel;
 
-template<class Data>
+template<bool higherOrder, class Data>
 class TermCodeTree : public CodeTree 
 {
 protected:
@@ -43,19 +42,23 @@ class TermCodeTree : public CodeTree
 
 private:
   struct RemovingTermMatcher
-  : public Matcher</*removing*/true,false>
+  : public Matcher</*removing*/true,false,higherOrder>
   {
   public:
-    void init(FlatTerm* ft_, TermCodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_);
+    using Base = Matcher</*removing*/true,false,higherOrder>;
 
+    void init(FlatTerm* ft_, TermCodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_);
   };
 
 public:
   struct TermMatcher
-  : public Matcher</*removing*/false,false>
+  : public Matcher</*removing*/false,false,higherOrder>
   {
     TermMatcher();
 
+    using Base = Matcher</*removing*/false,false,higherOrder>;
+    using Base::ft;
+
     void init(CodeTree* tree, TermList t);
     void reset();
     
diff --git a/Indexing/TermIndex.cpp b/Indexing/TermIndex.cpp
index 1afbe03d5b..f46774570a 100644
--- a/Indexing/TermIndex.cpp
+++ b/Indexing/TermIndex.cpp
@@ -112,11 +112,13 @@ void DemodulationSubtermIndex<higherOrder>::handleClause(Clause* c, bool adding)
 template class DemodulationSubtermIndex<true>;
 template class DemodulationSubtermIndex<false>;
 
-DemodulationLHSIndex::DemodulationLHSIndex(SaturationAlgorithm& salg)
-: TermIndex(new CodeTreeTIS<DemodulatorData>()), _ord(salg.getOrdering()),
+template<bool higherOrder>
+DemodulationLHSIndex<higherOrder>::DemodulationLHSIndex(SaturationAlgorithm& salg)
+: TermIndex(new CodeTreeTIS<higherOrder, DemodulatorData>()), _ord(salg.getOrdering()),
   _preordered(salg.getOptions().forwardDemodulation()==Options::Demodulation::PREORDERED) {};
 
-void DemodulationLHSIndex::handleClause(Clause* c, bool adding)
+template<bool higherOrder>
+void DemodulationLHSIndex<higherOrder>::handleClause(Clause* c, bool adding)
 {
   if (c->length()!=1) {
     return;
@@ -143,6 +145,9 @@ void DemodulationLHSIndex::handleClause(Clause* c, bool adding)
   }
 }
 
+template class DemodulationLHSIndex<true>;
+template class DemodulationLHSIndex<false>;
+
 InductionTermIndex::InductionTermIndex(SaturationAlgorithm& salg)
 : TermIndex(new TermSubstitutionTree<TermLiteralClause>()), _inductionGroundOnly(salg.getOptions().inductionGroundOnly()) {}
 
diff --git a/Indexing/TermIndex.hpp b/Indexing/TermIndex.hpp
index 549268f9e7..95a0ad57e4 100644
--- a/Indexing/TermIndex.hpp
+++ b/Indexing/TermIndex.hpp
@@ -90,6 +90,7 @@ class DemodulationSubtermIndex
 /**
  * Term index for forward demodulation
  */
+template<bool higherOrder>
 class DemodulationLHSIndex
 : public TermIndex<DemodulatorData>
 {
diff --git a/Inferences/BackwardSubsumptionDemodulation.cpp b/Inferences/BackwardSubsumptionDemodulation.cpp
index 05d91b6098..22ffde8977 100644
--- a/Inferences/BackwardSubsumptionDemodulation.cpp
+++ b/Inferences/BackwardSubsumptionDemodulation.cpp
@@ -48,8 +48,8 @@ using namespace Kernel;
 using namespace Indexing;
 using namespace Saturation;
 
-
-BackwardSubsumptionDemodulation::BackwardSubsumptionDemodulation(SaturationAlgorithm& salg)
+template<bool higherOrder>
+BackwardSubsumptionDemodulation<higherOrder>::BackwardSubsumptionDemodulation(SaturationAlgorithm& salg)
   : _ord(salg.getOrdering())
   , _index(salg.getSimplifyingIndex<BackwardSubsumptionIndex>())
   , _preorderedOnly{false}
@@ -61,7 +61,8 @@ BackwardSubsumptionDemodulation::BackwardSubsumptionDemodulation(SaturationAlgor
   , _backwardSubsumptionDemodulationMaxMatches(salg.getOptions().backwardSubsumptionDemodulationMaxMatches())
 { }
 
-void BackwardSubsumptionDemodulation::perform(Clause* sideCl, BwSimplificationRecordIterator& simplifications)
+template<bool higherOrder>
+void BackwardSubsumptionDemodulation<higherOrder>::perform(Clause* sideCl, BwSimplificationRecordIterator& simplifications)
 {
   ASSERT_VALID(*sideCl);
 
@@ -118,8 +119,8 @@ void BackwardSubsumptionDemodulation::perform(Clause* sideCl, BwSimplificationRe
   simplificationsStorage.clear();
 }  // perform
 
-
-void BackwardSubsumptionDemodulation::performWithQueryLit(Clause* sideCl, Literal* candidateQueryLit, std::vector<BwSimplificationRecord>& simplifications)
+template<bool higherOrder>
+void BackwardSubsumptionDemodulation<higherOrder>::performWithQueryLit(Clause* sideCl, Literal* candidateQueryLit, std::vector<BwSimplificationRecord>& simplifications)
 {
   //   sideCl
   // vvvvvvvvvv
@@ -243,7 +244,8 @@ void BackwardSubsumptionDemodulation::performWithQueryLit(Clause* sideCl, Litera
 
 /// Handles the matching part.
 /// Returns true iff the main premise has been simplified.
-bool BackwardSubsumptionDemodulation::simplifyCandidate(Clause* sideCl, Clause* mainCl, std::vector<BwSimplificationRecord>& simplifications)
+template<bool higherOrder>
+bool BackwardSubsumptionDemodulation<higherOrder>::simplifyCandidate(Clause* sideCl, Clause* mainCl, std::vector<BwSimplificationRecord>& simplifications)
 {
     static std::vector<LiteralList*> alts;
 
@@ -337,7 +339,8 @@ bool BackwardSubsumptionDemodulation::simplifyCandidate(Clause* sideCl, Clause*
 
 /// Handles the rewriting part.
 /// Returns true iff the main premise has been simplified.
-bool BackwardSubsumptionDemodulation::rewriteCandidate(Clause* sideCl, Clause* mainCl, MLMatcherSD const& matcher, Clause*& replacement)
+template<bool higherOrder>
+bool BackwardSubsumptionDemodulation<higherOrder>::rewriteCandidate(Clause* sideCl, Clause* mainCl, MLMatcherSD const& matcher, Clause*& replacement)
 {
   // to see why we use this have a look at the respective line in ForwardSubsumptionDemodulation
   DEBUG_CODE(static bool isAlascaOrdering = env.options->termOrdering () == Shell::Options::TermOrdering::QKBO
@@ -435,7 +438,7 @@ bool BackwardSubsumptionDemodulation::rewriteCandidate(Clause* sideCl, Clause* m
       continue;
     }
 
-    NonVariableNonTypeIterator nvi(dlit);
+    RewritableSubtermIterator<higherOrder> nvi(dlit);
     while (nvi.hasNext()) {
       TypedTermList lhsS = nvi.next();  // named 'lhsS' because it will be matched against 'lhs'
 
@@ -663,5 +666,7 @@ bool BackwardSubsumptionDemodulation::rewriteCandidate(Clause* sideCl, Clause* m
   return false;
 }  // rewriteCandidate
 
+template class BackwardSubsumptionDemodulation<false>;
+template class BackwardSubsumptionDemodulation<true>;
 
 }
diff --git a/Inferences/BackwardSubsumptionDemodulation.hpp b/Inferences/BackwardSubsumptionDemodulation.hpp
index e7e655e02d..c84ec33d9b 100644
--- a/Inferences/BackwardSubsumptionDemodulation.hpp
+++ b/Inferences/BackwardSubsumptionDemodulation.hpp
@@ -44,6 +44,7 @@ using namespace Kernel;
  *
  * This class implements the backward direction.
  */
+template<bool higherOrder>
 class BackwardSubsumptionDemodulation
   : public BackwardSimplificationEngine
 {
diff --git a/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp b/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp
index b029029430..c030aba225 100644
--- a/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp
+++ b/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp
@@ -19,19 +19,21 @@
 
 namespace Inferences {
 
-CodeTreeForwardSubsumptionAndResolution::CodeTreeForwardSubsumptionAndResolution(SaturationAlgorithm& salg)
+template<bool higherOrder>
+CodeTreeForwardSubsumptionAndResolution<higherOrder>::CodeTreeForwardSubsumptionAndResolution(SaturationAlgorithm& salg)
   : _subsumptionResolution(salg.getOptions().forwardSubsumptionResolution()),
-    _index(salg.getSimplifyingIndex<CodeTreeSubsumptionIndex>()),
+    _index(salg.getSimplifyingIndex<CodeTreeSubsumptionIndex<higherOrder>>()),
     _ct(_index->getClauseCodeTree())
 {}
 
-bool CodeTreeForwardSubsumptionAndResolution::perform(Clause *cl, Clause *&replacement, ClauseIterator &premises)
+template<bool higherOrder>
+bool CodeTreeForwardSubsumptionAndResolution<higherOrder>::perform(Clause *cl, Clause *&replacement, ClauseIterator &premises)
 {
   if (_ct->isEmpty()) {
     return false;
   }
 
-  static ClauseCodeTree::ClauseMatcher cm;
+  static typename ClauseCodeTree<higherOrder>::ClauseMatcher cm;
 
   cm.init(_ct, cl, _subsumptionResolution);
 
@@ -67,4 +69,7 @@ bool CodeTreeForwardSubsumptionAndResolution::perform(Clause *cl, Clause *&repla
   return false;
 }
 
+template class CodeTreeForwardSubsumptionAndResolution<false>;
+template class CodeTreeForwardSubsumptionAndResolution<true>;
+
 } // namespace Inferences
diff --git a/Inferences/CodeTreeForwardSubsumptionAndResolution.hpp b/Inferences/CodeTreeForwardSubsumptionAndResolution.hpp
index d3c892b534..5a30489375 100644
--- a/Inferences/CodeTreeForwardSubsumptionAndResolution.hpp
+++ b/Inferences/CodeTreeForwardSubsumptionAndResolution.hpp
@@ -23,6 +23,7 @@
 
 namespace Inferences {
 
+template<bool higherOrder>
 class CodeTreeForwardSubsumptionAndResolution
   : public ForwardSimplificationEngine
 {
@@ -35,8 +36,8 @@ class CodeTreeForwardSubsumptionAndResolution
 
 private:
   const bool _subsumptionResolution;
-  std::shared_ptr<Indexing::CodeTreeSubsumptionIndex> _index;
-  Indexing::ClauseCodeTree* _ct;
+  std::shared_ptr<Indexing::CodeTreeSubsumptionIndex<higherOrder>> _index;
+  Indexing::ClauseCodeTree<higherOrder>* _ct;
 #if VDEBUG
   SATSubsumption::SATSubsumptionAndResolution satSubs;
 #endif
diff --git a/Inferences/ForwardDemodulation.cpp b/Inferences/ForwardDemodulation.cpp
index a02d1a8f2b..dc27c6905b 100644
--- a/Inferences/ForwardDemodulation.cpp
+++ b/Inferences/ForwardDemodulation.cpp
@@ -76,7 +76,7 @@ ForwardDemodulation<higherOrder>::ForwardDemodulation(SaturationAlgorithm& salg)
     _skipNonequationalLiterals(salg.getOptions().demodulationOnlyEquational()),
     _helper(DemodulationHelper(salg.getOptions(), &salg.getOrdering())),
     _ord(salg.getOrdering()),
-    _index(salg.getSimplifyingIndex<DemodulationLHSIndex>())
+    _index(salg.getSimplifyingIndex<DemodulationLHSIndex<higherOrder>>())
 {}
 
 template<bool higherOrder>
diff --git a/Inferences/ForwardDemodulation.hpp b/Inferences/ForwardDemodulation.hpp
index 83da1e6132..6f07f58e00 100644
--- a/Inferences/ForwardDemodulation.hpp
+++ b/Inferences/ForwardDemodulation.hpp
@@ -44,7 +44,7 @@ class ForwardDemodulation
   const bool _skipNonequationalLiterals;
   const DemodulationHelper _helper;
   const Ordering& _ord;
-  std::shared_ptr<DemodulationLHSIndex> _index;
+  std::shared_ptr<DemodulationLHSIndex<higherOrder>> _index;
 };
 
 using ForwardDemodulationExtra = RewriteInferenceExtra;
diff --git a/Inferences/ForwardGroundJoinability.cpp b/Inferences/ForwardGroundJoinability.cpp
index 07bfb709c2..ea7e0af657 100644
--- a/Inferences/ForwardGroundJoinability.cpp
+++ b/Inferences/ForwardGroundJoinability.cpp
@@ -48,14 +48,16 @@ struct Applicator : SubstApplicator {
 
 } // end namespace
 
-ForwardGroundJoinability::ForwardGroundJoinability(SaturationAlgorithm& salg)
+template<bool higherOrder>
+ForwardGroundJoinability<higherOrder>::ForwardGroundJoinability(SaturationAlgorithm& salg)
   : _ord(salg.getOrdering()),
-    _index(salg.getSimplifyingIndex<DemodulationLHSIndex>())
+    _index(salg.getSimplifyingIndex<DemodulationLHSIndex<higherOrder>>())
 {}
 
 #define ITERATION_LIMIT 500
 
-bool ForwardGroundJoinability::perform(Clause* cl, Clause*& replacement, ClauseIterator& premises)
+template<bool higherOrder>
+bool ForwardGroundJoinability<higherOrder>::perform(Clause* cl, Clause*& replacement, ClauseIterator& premises)
 {
   // cout << "trying " << *cl << endl;
 
@@ -182,7 +184,8 @@ bool ForwardGroundJoinability::perform(Clause* cl, Clause*& replacement, ClauseI
   return true;
 }
 
-ForwardGroundJoinability::RedundancyCheck::RedundancyCheck(const Ordering& ord, Literal* data)
+template<bool higherOrder>
+ForwardGroundJoinability<higherOrder>::RedundancyCheck::RedundancyCheck(const Ordering& ord, Literal* data)
   : tod(ord.createTermOrderingDiagram(/*ground=*/true)), traversal(tod.get(), nullptr)
 {
   tod->_source = Branch(data, tod->_sink);
@@ -191,7 +194,8 @@ ForwardGroundJoinability::RedundancyCheck::RedundancyCheck(const Ordering& ord,
   ASS_EQ(_curr,&tod->_source);
 }
 
-std::pair<Literal*,const TermPartialOrdering*> ForwardGroundJoinability::RedundancyCheck::next(
+template<bool higherOrder>
+std::pair<Literal*,const TermPartialOrdering*> ForwardGroundJoinability<higherOrder>::RedundancyCheck::next(
   Stack<TermOrderingConstraint> ordCons, Literal* data)
 {
   static Ordering::Result ordVals[] = { Ordering::EQUAL, Ordering::GREATER, Ordering::INCOMPARABLE };
@@ -250,7 +254,8 @@ std::pair<Literal*,const TermPartialOrdering*> ForwardGroundJoinability::Redunda
   return { nullptr, nullptr };
 }
 
-bool ForwardGroundJoinability::makeEqual(Literal* lit, Stack<TermOrderingConstraint>& res)
+template<bool higherOrder>
+bool ForwardGroundJoinability<higherOrder>::makeEqual(Literal* lit, Stack<TermOrderingConstraint>& res)
 {
   ASS(lit->isEquality());
   ASS(lit->isPositive());
@@ -291,4 +296,7 @@ bool ForwardGroundJoinability::makeEqual(Literal* lit, Stack<TermOrderingConstra
   return true;
 }
 
+template class ForwardGroundJoinability<false>;
+template class ForwardGroundJoinability<true>;
+
 }
diff --git a/Inferences/ForwardGroundJoinability.hpp b/Inferences/ForwardGroundJoinability.hpp
index c549882d71..1a3e29f0e1 100644
--- a/Inferences/ForwardGroundJoinability.hpp
+++ b/Inferences/ForwardGroundJoinability.hpp
@@ -27,6 +27,7 @@ using namespace Kernel;
 using namespace Indexing;
 using namespace Saturation;
 
+template<bool higherOrder>
 class ForwardGroundJoinability
 : public ForwardSimplificationEngine
 {
@@ -54,7 +55,7 @@ class ForwardGroundJoinability
   };
 
   const Ordering& _ord;
-  std::shared_ptr<DemodulationLHSIndex> _index;
+  std::shared_ptr<DemodulationLHSIndex<higherOrder>> _index;
 };
 
 };
diff --git a/Inferences/ForwardSubsumptionDemodulation.cpp b/Inferences/ForwardSubsumptionDemodulation.cpp
index 942369cacf..fb71cdb97a 100644
--- a/Inferences/ForwardSubsumptionDemodulation.cpp
+++ b/Inferences/ForwardSubsumptionDemodulation.cpp
@@ -28,10 +28,13 @@
 
 using namespace Kernel;
 using namespace Lib;
-using namespace Inferences;
 using namespace Saturation;
 
-ForwardSubsumptionDemodulation::ForwardSubsumptionDemodulation(SaturationAlgorithm& salg)
+namespace Inferences
+{
+
+template<bool higherOrder>
+ForwardSubsumptionDemodulation<higherOrder>::ForwardSubsumptionDemodulation(SaturationAlgorithm& salg)
   : _preorderedOnly(false),
     _allowIncompleteness(false),
     _enableOrderingOptimizations(
@@ -43,7 +46,8 @@ ForwardSubsumptionDemodulation::ForwardSubsumptionDemodulation(SaturationAlgorit
     _index(salg.getSimplifyingIndex<FSDLiteralIndex>())
 {}
 
-bool ForwardSubsumptionDemodulation::perform(Clause* cl, Clause*& replacement, ClauseIterator& premises)
+template<bool higherOrder>
+bool ForwardSubsumptionDemodulation<higherOrder>::perform(Clause* cl, Clause*& replacement, ClauseIterator& premises)
 {
   //                        cl
   //                 vvvvvvvvvvvvvvvv
@@ -361,7 +365,7 @@ bool ForwardSubsumptionDemodulation::perform(Clause* cl, Clause*& replacement, C
             continue;
           }
 
-          NonVariableNonTypeIterator nvi(dlit);
+          RewritableSubtermIterator<higherOrder> nvi(dlit);
           while (nvi.hasNext()) {
             TypedTermList lhsS = nvi.next();  // named 'lhsS' because it will be matched against 'lhs'
 
@@ -637,3 +641,8 @@ bool ForwardSubsumptionDemodulation::perform(Clause* cl, Clause*& replacement, C
 
   return false;
 }
+
+template class ForwardSubsumptionDemodulation<false>;
+template class ForwardSubsumptionDemodulation<true>;
+
+}
\ No newline at end of file
diff --git a/Inferences/ForwardSubsumptionDemodulation.hpp b/Inferences/ForwardSubsumptionDemodulation.hpp
index 60938de200..0fbea6224c 100644
--- a/Inferences/ForwardSubsumptionDemodulation.hpp
+++ b/Inferences/ForwardSubsumptionDemodulation.hpp
@@ -43,6 +43,7 @@ using namespace Saturation;
  *
  * This class implements the forward direction.
  */
+template<bool higherOrder>
 class ForwardSubsumptionDemodulation
   : public ForwardSimplificationEngine
 {
diff --git a/Kernel/Clause.cpp b/Kernel/Clause.cpp
index 25716005e7..4419652452 100644
--- a/Kernel/Clause.cpp
+++ b/Kernel/Clause.cpp
@@ -75,6 +75,12 @@ Clause::Clause(Literal* const* lits, unsigned length, Inference inf)
     (*this)[i] = lits[i];
   }
 
+#if VDEBUG
+  // check that the variable sorts are consistent
+  DHMap<unsigned, TermList> temp;
+  SortHelper::collectVariableSorts(this, temp);
+#endif
+
   doUnitTracing();
 }
 
diff --git a/Kernel/TermOrderingDiagram.hpp b/Kernel/TermOrderingDiagram.hpp
index f6830cf25d..2f864deb7b 100644
--- a/Kernel/TermOrderingDiagram.hpp
+++ b/Kernel/TermOrderingDiagram.hpp
@@ -21,7 +21,7 @@
 #include "Ordering.hpp"
 
 namespace Inferences {
-  class ForwardGroundJoinability;
+  template<bool higherOrder> class ForwardGroundJoinability;
 }
 
 namespace Kernel {
@@ -195,7 +195,7 @@ struct TermOrderingDiagram
   const SubstApplicator* _appl;
   bool _ground;
 
-  friend class Inferences::ForwardGroundJoinability;
+  template<bool higherOrder> friend class Inferences::ForwardGroundJoinability;
 
 public:
   template<class Iterator, typename ...Args>
diff --git a/Lib/Vector.hpp b/Lib/Vector.hpp
index 8a6c4f625d..4eab9000d5 100644
--- a/Lib/Vector.hpp
+++ b/Lib/Vector.hpp
@@ -25,7 +25,7 @@
 
 namespace Indexing {
   class CodeTree;
-  class ClauseCodeTree;
+  template<bool> class ClauseCodeTree;
 }
 
 namespace Lib {
@@ -117,7 +117,7 @@ class Vector
   } // toString
 
   friend class Indexing::CodeTree;
-  friend class Indexing::ClauseCodeTree;
+  template<bool> friend class Indexing::ClauseCodeTree;
 
   /**
    * Iterator that deallocates the vector when it yields the last value.
diff --git a/Saturation/ProvingHelper.cpp b/Saturation/ProvingHelper.cpp
index 89d47d9f8f..a58413fb3d 100644
--- a/Saturation/ProvingHelper.cpp
+++ b/Saturation/ProvingHelper.cpp
@@ -132,6 +132,8 @@ void ProvingHelper::runVampire(Problem& prb, const Options& opt)
   //decide whether to use poly or mono well-typedness test
   //after options have been read. Equality Proxy can introduce poly in mono.
   env.sharing->setPoly();
+  // Preprocessing can alter whether a problem is HO, update it here.
+  env.setHigherOrder(env.getMainProblem()->isHigherOrder());
 
   env.options->resolveAwayAutoValues(prb);
 
diff --git a/Saturation/SaturationAlgorithm.cpp b/Saturation/SaturationAlgorithm.cpp
index 88c6ebc696..4a58305e0f 100644
--- a/Saturation/SaturationAlgorithm.cpp
+++ b/Saturation/SaturationAlgorithm.cpp
@@ -1381,6 +1381,9 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const
 {
   bool alascaTakesOver = doesAlascaTakeOver(prb, opt);
 
+  // For the following part, we want these two values to be synced
+  ASS_EQ(env.higherOrder(), prb.isHigherOrder());
+
   SaturationAlgorithm* res;
   switch(opt.saturationAlgorithm()) {
   case Shell::Options::SaturationAlgorithm::DISCOUNT:
@@ -1592,12 +1595,20 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const
     // fsd should be performed after forward subsumption,
     // because every successful forward subsumption will lead to a (useless) match in fsd.
     if (opt.forwardSubsumptionDemodulation()) {
-      res->addForwardSimplifierToFront<ForwardSubsumptionDemodulation>();
+      if (prb.isHigherOrder()) {
+        res->addForwardSimplifierToFront<ForwardSubsumptionDemodulation<true>>();
+      } else {
+        res->addForwardSimplifierToFront<ForwardSubsumptionDemodulation<false>>();
+      }
     }
   }
   if (mayHaveEquality) {
     if (opt.forwardGroundJoinability()) {
-      res->addExpensiveForwardSimplifierToFront<ForwardGroundJoinability>();
+      if (prb.isHigherOrder()) {
+        res->addExpensiveForwardSimplifierToFront<ForwardGroundJoinability<true>>();
+      } else {
+        res->addExpensiveForwardSimplifierToFront<ForwardGroundJoinability<false>>();
+      }
     }
     switch (opt.forwardDemodulation()) {
       case Options::Demodulation::ALL:
@@ -1619,7 +1630,11 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const
 
   if (opt.forwardSubsumption()) {
     if (opt.codeTreeSubsumption()) {
-      res->addForwardSimplifierToFront<CodeTreeForwardSubsumptionAndResolution>();
+      if (prb.isHigherOrder()) {
+        res->addForwardSimplifierToFront<CodeTreeForwardSubsumptionAndResolution<true>>();
+      } else {
+        res->addForwardSimplifierToFront<CodeTreeForwardSubsumptionAndResolution<false>>();
+      }
     } else {
       res->addForwardSimplifierToFront<ForwardSubsumptionAndResolution>();
     }
@@ -1649,7 +1664,11 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const
   }
   
   if (mayHaveEquality && opt.backwardSubsumptionDemodulation()) {
-    res->addBackwardSimplifierToFront<BackwardSubsumptionDemodulation>();
+    if (prb.isHigherOrder()) {
+      res->addBackwardSimplifierToFront<BackwardSubsumptionDemodulation<true>>();
+    } else {
+      res->addBackwardSimplifierToFront<BackwardSubsumptionDemodulation<false>>();
+    }
   }
 
   bool backSubsumption = opt.backwardSubsumption() != Options::Subsumption::OFF;
diff --git a/Shell/FunctionDefinitionHandler.cpp b/Shell/FunctionDefinitionHandler.cpp
index a2a3d20263..12f725df50 100644
--- a/Shell/FunctionDefinitionHandler.cpp
+++ b/Shell/FunctionDefinitionHandler.cpp
@@ -88,7 +88,7 @@ void FunctionDefinitionHandler::initAndPreprocessEarly(Problem& prb)
 void FunctionDefinitionHandler::initAndPreprocessLate(Problem& prb,const Options& opts)
 {
   // reset state
-  _is = new CodeTreeTIS<TermLiteralClause>();
+  _is = new CodeTreeTIS</*higherOrder=*/false, TermLiteralClause>();
   _templates.reset();
 
   UnitList::DelIterator it(prb.units());
diff --git a/Shell/FunctionDefinitionHandler.hpp b/Shell/FunctionDefinitionHandler.hpp
index 104a0b86ea..0ecf8b9467 100644
--- a/Shell/FunctionDefinitionHandler.hpp
+++ b/Shell/FunctionDefinitionHandler.hpp
@@ -111,7 +111,7 @@ class FunctionDefinitionHandler
   const InductionTemplate* matchesTerm(Term* t, Stack<Term*>& inductionTerms) const;
 
 private:
-  ScopedPtr<CodeTreeTIS<TermLiteralClause>> _is;
+  ScopedPtr<CodeTreeTIS</*higherOrder=*/false, TermLiteralClause>> _is;
   DHMap<std::pair<unsigned, SymbolType>, RecursionTemplate> _templates;
 };
 
diff --git a/Shell/PartialRedundancyHandler.cpp b/Shell/PartialRedundancyHandler.cpp
index 8a76779bd7..8e470681a9 100644
--- a/Shell/PartialRedundancyHandler.cpp
+++ b/Shell/PartialRedundancyHandler.cpp
@@ -246,7 +246,7 @@ class PartialRedundancyHandler::ConstraintIndex
   }
 
   struct SubstMatcher
-  : public Matcher</*removing*/false,false>
+  : public Matcher</*removing*/false,false,/*higherOrder=*/false>
   {
     void init(CodeTree* tree, const TermStack& ts)
     {
@@ -281,7 +281,7 @@ class PartialRedundancyHandler::ConstraintIndex
   };
 
   struct VariantMatcher
-  : public Matcher</*removing*/true,true>
+  : public Matcher</*removing*/true,true,/*higherOrder=*/false>
   {
   public:
     void init(FlatTerm* ft_, CodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_) {
diff --git a/Shell/TweeGoalTransformation.cpp b/Shell/TweeGoalTransformation.cpp
index 290dc67ea7..93cebf3bf5 100644
--- a/Shell/TweeGoalTransformation.cpp
+++ b/Shell/TweeGoalTransformation.cpp
@@ -115,6 +115,11 @@ class Definizator : public BottomUpTermTransformer {
       Term* t = trm.term();
       if (t->isSort() || t->arity() == 0 || (!t->ground() && _groundOnly)) return trm;
 
+      // TODO(HOL): try to lift this restriction
+      if (env.higherOrder() && trm.containsLooseDBIndex()) {
+        return trm;
+      }
+
       Term* key = t;
       if (!t->ground()) {
         // as we go bottom up, t is never too big (well, it could be wide, but at least not deep)
diff --git a/UnitTests/tALASCA_Superposition.cpp b/UnitTests/tALASCA_Superposition.cpp
index 6cd5c71f6d..36e1a1d9cd 100644
--- a/UnitTests/tALASCA_Superposition.cpp
+++ b/UnitTests/tALASCA_Superposition.cpp
@@ -548,7 +548,7 @@ TEST_GENERATION(bug03,
     alascaSymmetricTest()
       .inputs  ({ 
           clause({ pa(aa)   })
-        , clause({ x == sorted(y, alpha), fa(x) != fa(y) })
+        , clause({ x == sorted(y, Rat), fa(x) != fa(y) })
         })
       .expected(exactly(
           /* nothing */
diff --git a/UnitTests/tFunctionDefinitionHandler.cpp b/UnitTests/tFunctionDefinitionHandler.cpp
index 50f8b1b375..31832220c9 100644
--- a/UnitTests/tFunctionDefinitionHandler.cpp
+++ b/UnitTests/tFunctionDefinitionHandler.cpp
@@ -75,9 +75,9 @@ TEST_FUN(test_01) {
     clause({ def_s(f(r(x), r(y)), f(f(x, r(r(y))), y)) }),
     clause({ def_s(g(r(x)), g(f(x,x))) }),
     clause({ def_u(h(x, y, r1(x, z)), h(y, y, z)) }),
-    clause({ def_u(h(r(x), y, z), h(x, x, r2(y,z))) }),
+    clause({ def_u(h(r(x), y, z), h(x, x, r2(z,y))) }),
     clause({ def_p(r(r(x))), p(y) }),
-    clause({ def_q(r1(x,y),r(z)), q(y,r(z)), g(b) == b, ~q(z,b) }),
+    clause({ def_q(r1(x,y),r(z)), q(y,r(z)), g(b) == b, ~q(b1,b) }),
   });
 
   ASS(!handler.getRecursionTemplate(f(x,y).sugaredExpr().term()));
diff --git a/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp b/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp
index 351432a28e..34b0c605bd 100644
--- a/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp
+++ b/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp
@@ -61,7 +61,7 @@ using namespace Test;
 namespace {
 
 inline auto tester() {
-  return FwdBwdSimplification::TestCase<CodeTreeForwardSubsumptionAndResolution, BackwardSubsumptionAndResolution>()
+  return FwdBwdSimplification::TestCase<CodeTreeForwardSubsumptionAndResolution</*higherOrder=*/false>, BackwardSubsumptionAndResolution>()
     .options({
       { "backward_subsumption", "on" },
       { "backward_subsumption_resolution", "on" }
diff --git a/UnitTests/tInferences_ForwardGroundJoinability.cpp b/UnitTests/tInferences_ForwardGroundJoinability.cpp
index 8e1c5fb0c4..bb8bb5b4b6 100644
--- a/UnitTests/tInferences_ForwardGroundJoinability.cpp
+++ b/UnitTests/tInferences_ForwardGroundJoinability.cpp
@@ -71,7 +71,7 @@ void joinabilityTest(ClauseStack axioms, Clause* cl, bool joinable, bool useKbo)
   env.options->set("term_ordering", useKbo ? "kbo" : "lpo");
   Test::MockedSaturationAlgorithm salg(p, o);
 
-  ForwardGroundJoinability fgj(salg);
+  ForwardGroundJoinability</*higherOrder=*/false> fgj(salg);
 
   auto container = salg.getSimplifyingClauseContainer();
 
diff --git a/UnitTests/tInferences_SubsumptionDemodulation.cpp b/UnitTests/tInferences_SubsumptionDemodulation.cpp
index 00d1649e63..61088f3cd7 100644
--- a/UnitTests/tInferences_SubsumptionDemodulation.cpp
+++ b/UnitTests/tInferences_SubsumptionDemodulation.cpp
@@ -37,7 +37,7 @@ using namespace Test;
 namespace {
 
 inline auto tester() {
-  return FwdBwdSimplification::TestCase<ForwardSubsumptionDemodulation, BackwardSubsumptionDemodulation>();
+  return FwdBwdSimplification::TestCase<ForwardSubsumptionDemodulation<false>, BackwardSubsumptionDemodulation<false>>();
 }
 
 // subsumption demodulation with preordered equation
diff --git a/UnitTests/tInferences_TheoryInstAndSimp.cpp b/UnitTests/tInferences_TheoryInstAndSimp.cpp
index d3f1e153da..746801cf69 100644
--- a/UnitTests/tInferences_TheoryInstAndSimp.cpp
+++ b/UnitTests/tInferences_TheoryInstAndSimp.cpp
@@ -125,7 +125,7 @@ TEST_GENERATION_WITH_SUGAR(test_03,
     Generation::SymmetricTest()
       .options(options("all"))
       .inputs({    clause({  cons(a, nil()) != cons(x, nil()), 
-          p(x)  })   })
+          p(cons(x, nil()))  })   })
       .expected(exactly(
       ))
       .premiseRedundant(false)
diff --git a/samplers/samplerHOL.smp b/samplers/samplerHOL.smp
new file mode 100644
index 0000000000..908e5895b0
--- /dev/null
+++ b/samplers/samplerHOL.smp
@@ -0,0 +1,404 @@
+# MACRO DEFINITIONS
+
+# set $has_z3 to false, if you want to sample without it
+> $has_z3 ~cat true:1
+
+# PREPROCESSING
+
+# blocked_clause_elimination
+> bce ~cat off:5,on:1
+
+# equality_proxy
+intent=unsat > ep ~cat off:70,RST:2,R:3,RSTC:2,RS:3
+# mono_ep
+ep!=off > mep ~cat on:10,off:1
+
+# equality_resolution_with_deletion
+> erd ~cat on:10,off:1
+
+# function_definition_elimination
+> fde ~cat all:5,none:1,unused:1
+
+# general_splitting
+> gsp ~cat off:8,on:1
+
+# newcnf
+> newcnf ~cat on:9,off:25
+
+# inline_let -- this is probably irrelevant on TPTP anyway
+newcnf=on > ile ~cat off:10,on:1
+
+# naming
+> $nm ~cat Z:1,NZ:5
+$nm=Z > nm ~cat 0:1
+$nm=NZ > nm ~sgd 0.07,2
+
+# inequality_splitting
+> $ins ~cat Z:2,NZ:1
+$ins=Z > ins ~cat 0:1
+$ins=NZ > ins ~sgd 0.4,1
+
+# random_polarities
+> rp ~cat off:3,on:1
+
+# twee_goal_transformation
+> tgt ~cat off:10,ground:6,full:5
+
+# sine_selection
+intent=unsat > ss ~cat off:1182,included:135,axioms:392
+
+# sine_depth
+intent=unsat ss!=off > sd ~cat 0:45,1:13,2:12,3:5,4:4,5:4,7:3,10:2,12:1,15:1
+
+# sine_generality_threshold
+intent=unsat ss!=off > sgt ~cat 0:7,5:1,10:1,15:1,20:1,30:1,50:1,100:1
+
+# sine_tolerance
+intent=unsat ss!=off > st ~cat -1.0:50,1.0:150,1.5:37,2.0:60,2.5:20,3.0:70,3.5:15,4.0:60,4.5:15,5.0:50,5.5:10,6.0:30,7.0:20
+
+# unused_predicate_definition_removal
+> updr ~cat on:16,off:1
+
+# SATURATION
+
+# saturation_algorithms
+intent=unsat ep=off > sa ~cat fmb:10,lrs:600,discount:572,otter:236
+intent=unsat ep!=off > sa ~cat lrs:600,discount:572,otter:236
+intent=sat > sa ~cat fmb:22,otter:60,discount:28
+
+# set_of_support
+intent=unsat sa!=fmb > sos ~cat off:80,on:17,all:10
+
+# lrs_first_time_check
+> $lftc ~cat N:5,Y:1
+sa=lrs $lftc=Y > lftc ~ui 5,95
+
+# literal selection
+> $s_pos ~cat Y:4,N:1
+intent=unsat sa!=fmb $s_pos=Y > s ~cat 0:11,1:31,2:52,3:21,4:22,10:300,11:131,20:11,21:66,22:11,30:6,31:14,32:4,33:10,34:3,35:8,666:50,1002:141,1003:14,1004:23,1010:145,1011:357,1666:50
+intent=unsat sa!=fmb $s_pos=N > s ~cat -1:31,-2:52,-3:21,-4:22,-10:300,-11:131,-20:11,-21:66,-22:11,-30:6,-31:14,-32:4,-33:10,-34:3,-35:8,-666:50,-1002:141,-1003:14,-1004:23,-1010:145,-1011:357,-1666:50
+
+intent=sat sa!=fmb $s_pos=Y > s ~cat 0:11,1:31,2:52,3:21,4:22,10:300,11:131,20:11,21:66,22:11,30:6,31:14,32:4,33:10,34:3,35:8,666:50
+intent=sat sa!=fmb $s_pos=N > s ~cat -1:31,-2:52,-3:21,-4:22,-10:300,-11:131,-20:11,-21:66,-22:11,-30:6,-31:14,-32:4,-33:10,-34:3,-35:8,-666:50
+
+# lookahaed_delay
+> $ls ~cat off:1
+sa!=fmb s=11 > $ls ~cat on:1
+sa!=fmb s=-11 > $ls ~cat on:1
+sa!=fmb s=1011 > $ls ~cat on:1
+sa!=fmb s=-1011 > $ls ~cat on:1
+
+sa!=fmb $ls=on > lsd ~cat 0:20,1:1,5:1,10:1,20:1,50:1,100:1
+
+# age_weight_ratio
+sa!=fmb > $awr ~cat A:1,W:1,AW:98
+sa!=fmb $awr=A > awr ~set 1:0
+sa!=fmb $awr=W > awr ~set 0:1
+sa!=fmb $awr=AW > awr ~u2r -10;4;:
+
+# random_awr
+sa!=fmb > rawr ~cat on:4,off:1
+
+# lrs_weight_limit_only
+sa=lrs > lwlo ~cat off:5,on:1
+
+# lrs_retroactive_deletes
+sa=lrs > lrd ~cat off:1,on:1
+
+# lrs_estimate_correction_coef
+# > $lecc ~cat 1:1
+# sa=lrs > $lecc ~cat 1:10,666:1
+# sa=lrs $lecc=1 > lecc ~cat 1.0:1
+# sa=lrs $lecc!=1 > lecc ~uf 0.5,2.0
+# TODO: leaving out weird timing dependent options
+
+# nongoal_weight_coefficient
+sa!=fmb > $nwc ~cat 1:2,666:1
+sa!=fmb $nwc=1 > nwc ~cat 1:1
+sa!=fmb $nwc!=1 > nwc ~uf 0.5,15.0
+# TODO: we will most likely want a new distribution here for ($nwc!=1) just above!
+
+# restrict_nwc_to_goal_constants
+sa!=fmb nwc!=1 > rnwc ~cat off:5,on:1
+
+# literal_maximality_aftercheck
+sa!=fmb > lma ~cat off:500,on:83
+
+# POSITIVE LITERAL SPLIT QUEUE
+sa!=fmb > plsq ~cat off:4,on:1
+
+# positive_literal_split_queue_layered_arrangement
+plsq=on > plsql ~cat on:66,off:162
+
+# positive_literal_split_queue_cutoffs
+plsq=on > plsqc ~cat 0:117,1:92,2:19,3:5,4:1
+
+# positive_literal_split_queue_ratios
+plsq=on > plsqr ~u2r -5;7;,
+
+# INFERENCES
+
+# superposition (don't turn this off at home!)
+intent=unsat sa!=fmb > sup ~cat on:100,off:1
+
+# simultaneous_superposition
+sa!=fmb sup=on > sims ~cat on:50,off:1
+
+# superposition_from_variables
+intent=unsat sa!=fmb sup=on > sfv ~cat on:38,off:1
+
+# code_tree_subsumption
+sa!=fmb > cts ~cat on:3,off:1
+
+# forward_subsumption
+sa!=fmb > fs ~cat on:500,off:31
+
+# forward_subsumption_resolution
+sa!=fmb fs=off > fsr ~cat off:1
+sa!=fmb fs=on  > fsr ~cat on:500,off:193
+
+# forward_subsumption_demodulation
+sa!=fmb > fsd ~cat off:500,on:90
+
+# forward_subsumption_demodulation_max_matches
+sa!=fmb fsd=on > fsdmm ~cat 0:10,1:3,2:2,3:1
+
+# backward_demodulation
+sa!=fmb > bd ~cat all:500,off:245,preordered:91
+
+# backward_subsumption
+sa!=fmb fs!=off > bs ~cat off:500,unit_only:74,on:64
+
+# backward_subsumption_resolution
+sa!=fmb > bsr ~cat off:500,unit_only:118,on:75
+
+# backward_subsumption_demodulation
+sa!=fmb > bsd ~cat off:500,on:74
+
+# backward_subsumption_demodulation_max_matches
+sa!=fmb bsd=on > bsdmm ~cat 0:10,1:3,2:2,3:1
+
+# condensation
+sa!=fmb > cond ~cat off:500,on:89,fast:61
+
+# equational_tautology_removal
+sa!=fmb > etr ~cat off:500,on:30
+
+# extensionality_resolution
+sa!=fmb ins=0 > er ~cat off:500,known:25,filter:26
+
+# extensionality_allow_pos_eq
+sa!=fmb er=filter > eape ~cat off:3,on:1
+
+# extensionality_max_length
+sa!=fmb er!=off > erml ~cat 0:3,2:1,3:1
+
+# fool_paramodulation
+sa!=fmb > foolp ~cat off:10,on:1
+
+# forward_demodulation
+sa!=fmb > fd ~cat all:500,off:41,preordered:168
+
+# demodulation_redundancy_check
+> $drc ~cat 0:1
+fd!=off > $drc ~cat 1:1
+bd!=off > $drc ~cat 1:1
+intent=unsat sa!=fmb $drc=1 > drc ~cat encompass:500,ordering:500,off:354
+intent=sat sa!=fmb $drc=1 > drc ~cat ordering:643,encompass:554
+
+# forward_demodulation_term_ordering_diagrams
+sa!=fmb fd!=off > fdtod ~cat on:1,off:1
+
+# demodulation_only_equational
+sa!=fmb $drc=1 > doe ~cat on:1,off:1
+
+# forward_ground_joinability
+sa!=fmb > fgj ~cat on:1,off:1
+
+# forward_literal_rewriting
+intent=unsat sa!=fmb > flr ~cat off:8,on:1
+
+# function_definition_introduction
+# TODO fix this
+# sa!=fmb > fdi ~cat 0:100,2:1,4:1,8:1,16:1,32:1,64:1,128:1,256:1,512:1,1024:1
+
+# inner_rewriting
+sa!=fmb > irw ~cat off:165,on:6
+
+# SINE LEVELS and shit
+
+# sine_to_age
+sa!=fmb > s2a ~cat off:2,on:1
+
+# sine_level_split_queue
+sa!=fmb > slsq ~cat off:5,on:1
+
+# sine_level_split_queue_layered_arrangement
+sa!=fmb slsq=on > slsql ~cat on:1,off:1
+
+# sine_level_split_queue_cutoffs
+sa!=fmb slsq=on > slsqc ~cat 0:10,1:10,2:6,3:3,4:1
+
+# sine_level_split_queue_ratios
+sa!=fmb slsq=on > slsqr ~u2r -5;2;,
+
+# ORDERING
+
+# term_ordering
+sa!=fmb > to ~cat kbo:13,lpo:4
+
+# symbol_precedence
+sa!=fmb > sp ~cat arity:100,const_min:72,frequency:130,const_frequency:49,reverse_frequency:55,reverse_arity:72,weighted_frequency:24,unary_first:28,occurrence:82,unary_frequency:14,const_max:18
+# symbol_precedence_boost
+sa!=fmb > spb ~cat none:200,units:78,goal:91,goal_then_units:93,non_intro:14,intro:12
+
+# kbo_max_zero
+sa!=fmb to=kbo > kmz ~cat off:200,on:1
+# kbo_weight_scheme
+sa!=fmb to=kbo > kws ~cat const:50,inv_arity_squared:6,precedence:28,arity_squared:1,inv_arity:5,inv_frequency:8,frequency:2
+
+# literal_comparison_mode
+intent=unsat sa!=fmb > lcm ~cat standard:500,reverse:66,predicate:51
+intent=sat sa!=fmb > lcm ~cat standard:500,reverse:66,predicate:51
+
+# sine_to_pred_levels
+sa!=fmb lcm=standard > s2pl ~cat off:50,on:2,no:3
+
+# SINE LEVELS - configure (must come after sine_to_age & slsq & s2pl)
+
+# set $s2a as the disjunction: s2a=on | slsq=on | s2pl!=off
+> $s2a ~cat off:1
+s2a=on    > $s2a ~cat on:1
+slsq=on   > $s2a ~cat on:1
+s2pl!=off > $s2a ~cat on:1
+
+# now configure (stealing the values from sine proper, which is not ideal, but should do)
+
+# sine_to_age_generality_threshold
+$s2a=on > s2agt ~cat 0:7,5:1,10:1,15:1,20:1,30:1,50:1,100:1
+
+# sine_to_age_tolerance
+$s2a=on > s2at ~cat -1.0:50,1.0:150,1.5:37,2.0:60,2.5:20,3.0:70,3.5:15,4.0:60,4.5:15,5.0:50,5.5:10,6.0:30,7.0:20
+
+# AVATAR
+sa!=fmb > av ~cat on:15,off:4
+
+# partial_redundancy_check
+sa!=fmb > prc ~cat on:3,off:5
+
+# partial_redundancy_ordering_constraints
+sa!=fmb prc=on > proc ~cat on:1,off:1
+
+# partial_redundancy_avatar_constraints
+sa!=fmb av=on prc=on > prac ~cat on:1,off:1
+
+# partial_redundancy_literal_constraints
+sa!=fmb prc=on > prlc ~cat on:1,off:1
+
+# sat_solver
+sa!=fmb $has_z3=true av=on > sas ~cat minisat:10,cadical:7,z3:3
+sa!=fmb $has_z3!=true av=on > sas ~cat minisat:10,cadical:7
+sa=fmb > sas ~cat minisat:7,cadical:10
+
+# avatar_add_complementary
+sa!=fmb av=on > aac ~cat none:147,ground:600
+
+# avatar_congruence_closure
+sa!=fmb sas!=z3 av=on > acc ~cat off:600,on:58
+
+# avatar_minimize_model
+sa!=fmb av=on > amm ~cat on:600,off:69
+
+# avatar_delete_deactivated
+sa!=fmb av=on > add ~cat on:300,large:55,off:8
+
+# avatar_literal_polarity_advice
+sa!=fmb av=on > alpa ~cat none:300,false:13,true:6,random:4
+
+# avatar_nonsplittable_components
+sa!=fmb av=on > anc ~cat known:300,all_dependent:38,all:45,none:48
+
+# avatar_turn_off_time_frac
+# sa!=fmb av=on > $atotf ~cat 1:10,666:1
+# sa!=fmb av=on $atotf=1 > atotf ~cat 1:1
+# sa!=fmb av=on $atotf!=1 > atotf ~uf 0.0,0.7
+# TODO: leaving out weird timing dependent options
+
+# nonliterals_in_clause_weight
+sa!=fmb av=on > nicw ~cat off:600,on:76
+
+# split_at_activation
+sa!=fmb av=on > sac ~cat off:3,on:1
+
+# Michael's clause cleaving TODO
+# intent=sat av=on > cm ~cat on:1
+
+# BACK TO INFERENCES
+
+# unit_resulting_resolution
+sa!=fmb av=on  > urr ~cat off:1200,ec_only:162,on:300,full:40
+sa!=fmb av=off > urr ~cat off:1200,ec_only:162,on:340
+
+# binary_resolution
+intent=unsat sa!=fmb > br ~cat on:8,off:1
+intent=sat sa!=fmb urr=on > br ~cat on:10,off:1
+
+# AVATAR SPLIT QUEUE
+
+# avatar_split_queue
+sa!=fmb av=on > avsq ~cat off:5,on:1
+
+# avatar_split_queue_layered_arrangement
+sa!=fmb avsq=on > avsql ~cat off:4,on:1
+
+# avatar_split_queue_cutoffs
+sa!=fmb avsq=on > avsqc ~cat 0:80,1:30,2:20,3:20,4:10,5:5
+
+# avatar_split_queue_ratios
+sa!=fmb avsq=on > avsqr ~u2r -5;3;,
+
+# GLOBAL SUBSUMPTION
+# global_subsumption
+sa!=fmb > gs ~cat off:5,on:1
+
+# FMB options
+
+# TODO: a candidate for hardwiring "on" (go an collect the data)
+# fmb_use_simplifying_solver
+sa=fmb sas=minisat > fmbuss ~cat off:1,on:5
+
+# fmb_enumeration_strategy (TODO: in the multi-sorted setting, sbeam makes only sense with intent=sat)
+$has_z3=true  sa=fmb > fmbes ~cat sbeam:1,smt:1,contour:1
+$has_z3!=true sa=fmb > fmbes ~cat sbeam:1,contour:1
+
+# fmb_size_weight_ratio
+fmbes=contour > fmbswr ~ui 0,5
+
+# fmb_adjust_sorts
+sa=fmb fmbes!=contour > fmbas ~cat group:36,predicate:4,expand:4,off:1,function:1
+sa=fmb fmbes=contour > fmbas ~cat group:36,predicate:4,off:1,function:1
+
+# fmb_detect_sort_bounds
+sa=fmb fmbas!=predicate fmbas!=function > fmbdsb ~cat off:5,on:1
+
+# fmb_detect_sort_bounds_time_limit
+fmbdsb=on > fmbdsbt ~cat 1:5,2:2,3:1
+
+# fmb_keep_sbeam_generators
+sa=fmb fmbes=sbeam > fmbksg ~cat off:2,on:1
+
+# fmb_start_size - setting this to values > 1 is making things "finite model incomplete" (but could save time for some problems)
+intent=sat sa=fmb > $fmbss ~cat 1:5,666:1
+intent=sat sa=fmb $fmbss=1 > fmbss ~cat 1:1
+intent=sat sa=fmb $fmbss=666 > fmbss ~sgd 0.1,1
+
+# fmb_symmetry_symbol_order
+sa=fmb > fmbsso ~cat occurrence:22,input_usage:1,preprocessed_usage:1
+
+# fmb_symmetry_ratio
+sa=fmb > fmbsr ~uf 1.0,2.5
+
+# MISSING:
+# Any theory reasoning options (including term algebras and sa=z3)
+# Any induction options
+# Any higher-order options (Higher-order options section)