diff --git a/Indexing/ClauseCodeTree.cpp b/Indexing/ClauseCodeTree.cpp
index 90fe223fc..89524c38d 100644
--- a/Indexing/ClauseCodeTree.cpp
+++ b/Indexing/ClauseCodeTree.cpp
@@ -290,7 +290,7 @@ void ClauseCodeTree::remove(Clause* cl)
 void ClauseCodeTree::RemovingLiteralMatcher::init(CodeOp* entry_, LitInfo* linfos_,
     size_t linfoCnt_, const ClauseCodeTree& tree_, Stack<CodeOp*>* firstsInBlocks_)
 {
-  Matcher::init(tree_, entry_, linfos_, linfoCnt_, firstsInBlocks_);
+  Matcher::init(tree_, entry_, /*canEnterOpposites*/ false, linfos_, linfoCnt_, firstsInBlocks_);
 
   ALWAYS(prepareLiteral());
 }
@@ -324,13 +324,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(const CodeTree& tree_, CodeOp* entry_,
+template<bool sres>
+void ClauseCodeTree::LiteralMatcher<sres>::init(const CodeTree& tree_, CodeOp* entry_,
 					  LitInfo* linfos_, size_t linfoCnt_,
-					  bool seekOnlySuccess)
+					  bool canEnterOpposites, bool seekOnlySuccess)
 {
   ASS_G(linfoCnt_,0);
 
-  Matcher::init(tree_,entry_,linfos_,linfoCnt_);
+  Base::init(tree_,entry_,canEnterOpposites, linfos_,linfoCnt_);
 
   _eagerlyMatched=false;
   eagerResults.reset();
@@ -342,8 +343,8 @@ void ClauseCodeTree::LiteralMatcher::init(const 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);
@@ -353,17 +354,18 @@ void ClauseCodeTree::LiteralMatcher::init(const CodeTree& tree_, CodeOp* entry_,
     return;
   }
 
-  ALWAYS(prepareLiteral());
+  ALWAYS(Base::prepareLiteral());
 }
 
 /**
  * Try to find a match, and if one is found, return true
  */
-bool ClauseCodeTree::LiteralMatcher::next()
+template<bool sres>
+bool ClauseCodeTree::LiteralMatcher<sres>::next()
 {
   if(eagerlyMatched()) {
-    _matched=!eagerResults.isEmpty();
-    if(!_matched) {
+    _matched = eagerResults.isNonEmpty();
+    if (!_matched) {
       return false;
     }
     op=eagerResults.pop();
@@ -375,25 +377,37 @@ bool ClauseCodeTree::LiteralMatcher::next()
     return false;
   }
 
-  _matched=execute();
-  if(!_matched) {
-    return false;
+  while ((_matched = execute())) {
+    ASS(op->isLitEnd() || op->isSuccess());
+    if(op->isLitEnd()) {
+      recordMatch();
+    }
+    
+    /* Defer opposite matches so that non-opposite matches are always returned first */
+    if (opposite) {
+      eagerResults.push(op);
+      continue;
+    }
+
+    return true;
   }
 
-  ASS(op->isLitEnd() || op->isSuccess());
-  if(op->isLitEnd()) {
-    recordMatch();
+  /* No non-opposite matches remain, so fall back to the deferred opposite ones */
+  if (eagerResults.isNonEmpty()) {
+    op = eagerResults.pop();
+    _matched = true;
+    return true;
   }
-  return true;
+  return false;
 }
 
 /**
  * Perform eager matching and return true iff new matches were found
  */
-bool ClauseCodeTree::LiteralMatcher::doEagerMatching()
+template<bool sres>
+bool ClauseCodeTree::LiteralMatcher<sres>::doEagerMatching()
 {
   ASS(!eagerlyMatched()); //eager matching can be done only once
-  ASS(eagerResults.isEmpty());
   ASS(!finished());
 
   //backup the current op
@@ -407,7 +421,12 @@ bool ClauseCodeTree::LiteralMatcher::doEagerMatching()
   while(execute()) {
     if(op->isLitEnd()) {
       recordMatch();
-      eagerResultsRevOrder.push(op);
+      if (opposite) {
+        /* push straight to eagerResults so opposite matches end up after all non-opposite ones */
+        eagerResults.push(op);
+      } else {
+        eagerResultsRevOrder.push(op);
+      }
     }
     else {
       ASS(op->isSuccess());
@@ -434,21 +453,25 @@ bool ClauseCodeTree::LiteralMatcher::doEagerMatching()
   return eagerResults.isNonEmpty();
 }
 
-void ClauseCodeTree::LiteralMatcher::recordMatch()
+template<bool sres>
+void ClauseCodeTree::LiteralMatcher<sres>::recordMatch()
 {
   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 we're matching opposite matches, we have already tried all non-opposite ones
-    ils->noNonOppositeMatches=true;
+  if constexpr (sres) {
+    if(!ils->matchCnt && opposite) {
+      ils->noNonOppositeMatches=true;
+    } else if (ils->noNonOppositeMatches && !opposite) {
+      ils->noNonOppositeMatches=false;
+    }
   }
-  ils->addMatch(linfos[curLInfo].liIndex, bindings);
+  ils->template addMatch<sres>(Base::linfos[Base::curLInfo].liIndex, Base::bindings, opposite);
 }
 
 
@@ -457,15 +480,15 @@ void ClauseCodeTree::LiteralMatcher::recordMatch()
 /**
  * Initialize the ClauseMatcher to retrieve generalizetions
  * of the @b query_ clause.
- * If @b sres_ if true, we perform subsumption resolution
+ * If @b sres if true, we perform subsumption resolution
  */
-void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Clause* query_, bool sres_)
+template<bool sres>
+void ClauseCodeTree::ClauseMatcher<sres>::init(ClauseCodeTree* tree_, Clause* query_)
 {
   ASS(!tree_->isEmpty());
 
   query=query_;
   tree=tree_;
-  sres=sres_;
   lms.reset();
 
 #if VDEBUG
@@ -481,7 +504,7 @@ void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Clause* query_,
       baseLICnt++;
     }
   }
-  unsigned liCnt=sres ? (baseLICnt*2) : baseLICnt;
+  unsigned liCnt=baseLICnt;
   lInfos.ensure(liCnt);
 
   //we put ground literals first
@@ -512,20 +535,16 @@ void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Clause* query_,
       liIndex++;
     }
   }
-  if(sres) {
-    for(unsigned i=0;i<baseLICnt;i++) {
-      unsigned newIndex=i+baseLICnt;
-      lInfos[newIndex]=LitInfo::getOpposite(lInfos[i]);
-      lInfos[newIndex].liIndex=newIndex;
-    }
+  if constexpr (sres) {
     sresLiteral=sresNoLiteral;
   }
 
   tree->incTimeStamp();
-  enterLiteral(tree->getEntryPoint(), clen==0);
+  enterLiteral(tree->getEntryPoint(), clen==0, sres);
 }
 
-void ClauseCodeTree::ClauseMatcher::reset()
+template<bool sres>
+void ClauseCodeTree::ClauseMatcher<sres>::reset()
 {
   unsigned liCnt=lInfos.size();
   for(unsigned i=0;i<liCnt;i++) {
@@ -542,14 +561,15 @@ void ClauseCodeTree::ClauseMatcher::reset()
 /**
  * Return next clause matching query or 0 if there is not such
  */
-Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit)
+template<bool sres>
+Clause* ClauseCodeTree::ClauseMatcher<sres>::next(int& resolvedQueryLit)
 {
   if(lms.isEmpty()) {
     return 0;
   }
 
   for(;;) {
-    LiteralMatcher* lm = &*lms.top();
+    LiteralMatcher<sres>* lm = &*lms.top();
 
     //get next literal from the literal matcher
     bool found=lm->next();
@@ -577,23 +597,29 @@ Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit)
       //so we can increase here
       CodeOp* newLitEntry=lm->op+1;
 
-      //check that we have cleared the sresLiteral value if it is no longer valid
-      ASS(!sres || sresLiteral==sresNoLiteral || sresLiteral<lms.size()-1);
+      bool canEnterOpposites = false;
 
-      if(sres && sresLiteral==sresNoLiteral) {
-	//we check whether we haven't matched only opposite literals on the previous level
-	if(lm->getILS()->noNonOppositeMatches) {
-	  sresLiteral=lms.size()-1;
-	}
+      if constexpr (sres) {
+        //check that we have cleared the sresLiteral value if it is no longer valid
+        ASS(sresLiteral==sresNoLiteral || sresLiteral<lms.size()-1);
+
+        if(sresLiteral==sresNoLiteral) {
+          //we check whether we haven't matched only opposite literals on the previous level
+          if(lm->getILS()->noNonOppositeMatches) {
+            sresLiteral=lms.size()-1;
+          }
+        }
+        canEnterOpposites = (sresLiteral == sresNoLiteral);
       }
 
       bool seekOnlySuccess=lms.size()==query->length();
-      enterLiteral(newLitEntry, seekOnlySuccess);
+      enterLiteral(newLitEntry, seekOnlySuccess, canEnterOpposites);
     }
   }
 }
 
-inline bool ClauseCodeTree::ClauseMatcher::canEnterLiteral(CodeOp* op)
+template<bool sres>
+inline bool ClauseCodeTree::ClauseMatcher<sres>::canEnterLiteral(CodeOp* op)
 {
   ASS(op->isLitEnd());
   ASS_EQ(lms.top()->op, op);
@@ -622,7 +648,7 @@ inline bool ClauseCodeTree::ClauseMatcher::canEnterLiteral(CodeOp* op)
 	matchIndex--;
 	MatchInfo* mi=ils->getMatch(matchIndex);
 	if(!existsCompatibleMatch(ils, mi, prevILS)) {
-	  ils->deleteMatch(matchIndex); //decreases ils->matchCnt
+	  ils->template deleteMatch<sres>(matchIndex); //decreases ils->matchCnt
 	}
       }
       if(!ils->matchCnt) {
@@ -642,14 +668,15 @@ 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 sres>
+void ClauseCodeTree::ClauseMatcher<sres>::enterLiteral(CodeOp* entry, bool seekOnlySuccess, bool canEnterOpposites)
 {
   if(!seekOnlySuccess) {
     RSTAT_MCTR_INC("enterLiteral levels (non-sos)", lms.size());
   }
 
   if(lms.isNonEmpty()) {
-    Recycled<LiteralMatcher, NoReset>& prevLM = lms.top();
+    Recycled<LiteralMatcher<sres>, NoReset>& prevLM = lms.top();
     ILStruct* ils=prevLM->op->getILS();
     ASS_EQ(ils->timestamp,tree->_curTimeStamp);
     ASS(!ils->visited);
@@ -658,36 +685,28 @@ void ClauseCodeTree::ClauseMatcher::enterLiteral(CodeOp* entry, bool seekOnlySuc
   }
 
   size_t linfoCnt=lInfos.size();
-  if(sres && sresLiteral!=sresNoLiteral) {
-    ASS_L(sresLiteral,lms.size());
-    //we do not need to match index literals with opposite query
-    //literals, as one of already matched index literals matched only
-    //to opposite literals (and opposite literals cannot be matched
-    //on more than one index literal)
-    ASS_EQ(linfoCnt%2,0);
-    linfoCnt/=2;
-  }
-
-  Recycled<LiteralMatcher, NoReset> lm;
-  lm->init(*tree, entry, lInfos.array(), linfoCnt, seekOnlySuccess);
+
+  Recycled<LiteralMatcher<sres>, NoReset> lm;
+  lm->init(*tree, entry, lInfos.array(), linfoCnt, canEnterOpposites, seekOnlySuccess);
   lms.push(std::move(lm));
 }
 
-void ClauseCodeTree::ClauseMatcher::leaveLiteral()
+template<bool sres>
+void ClauseCodeTree::ClauseMatcher<sres>::leaveLiteral()
 {
   ASS(lms.isNonEmpty());
 
   lms.pop();
 
   if(lms.isNonEmpty()) {
-    LiteralMatcher* prevLM = &*lms.top();
+    LiteralMatcher<sres>* prevLM = &*lms.top();
     ILStruct* ils=prevLM->op->getILS();
     ASS_EQ(ils->timestamp,tree->_curTimeStamp);
     ASS(ils->visited);
 
     ils->finished=true;
 
-    if(sres) {
+    if constexpr (sres) {
       //clear the resolved literal flag if we have backtracked from it
       unsigned depth=lms.size()-1;
       if(sresLiteral==depth) {
@@ -701,7 +720,8 @@ void ClauseCodeTree::ClauseMatcher::leaveLiteral()
 
 //////////////// Multi-literal matching
 
-bool ClauseCodeTree::ClauseMatcher::checkCandidate(Clause* cl, int& resolvedQueryLit)
+template<bool sres>
+bool ClauseCodeTree::ClauseMatcher<sres>::checkCandidate(Clause* cl, int& resolvedQueryLit)
 {
   unsigned clen=cl->length();
   //the last matcher in mls is the one that yielded the SUCCESS operation
@@ -712,18 +732,20 @@ bool ClauseCodeTree::ClauseMatcher::checkCandidate(Clause* cl, int& resolvedQuer
     //if clause doesn't have multiple literals, there is no need
     //for multi-literal matching
     resolvedQueryLit=-1;
-    if(sres && clen==1) {
-      size_t matchCnt=lms[0]->getILS()->matchCnt;
-      for(size_t i=0;i<matchCnt;i++) {
-	MatchInfo* mi=lms[0]->getILS()->getMatch(i);
-	if(lInfos[mi->liIndex].opposite) {
-	  resolvedQueryLit=lInfos[mi->liIndex].litIndex;
-	}
-	else {
-	  //we prefer subsumption to subsumption resolution
-	  resolvedQueryLit=-1;
-	  break;
-	}
+    if constexpr (sres) {
+      if (clen==1) {
+        size_t matchCnt=lms[0]->getILS()->matchCnt;
+        for(size_t i=0;i<matchCnt;i++) {
+          MatchInfo* mi=lms[0]->getILS()->getMatch(i);
+          if(mi->opposite()) {
+            resolvedQueryLit=lInfos[mi->getLiIndex()].litIndex;
+          }
+          else {
+            //we prefer subsumption to subsumption resolution
+            resolvedQueryLit=-1;
+            break;
+          }
+        }
       }
     }
     return true;
@@ -735,7 +757,7 @@ bool ClauseCodeTree::ClauseMatcher::checkCandidate(Clause* cl, int& resolvedQuer
 
   bool newMatches=false;
   for(int i=clen-1;i>=0;i--) {
-    LiteralMatcher* lm = &*lms[i];
+    LiteralMatcher<sres>* lm = &*lms[i];
     if(lm->eagerlyMatched()) {
       break;
     }
@@ -756,7 +778,8 @@ bool ClauseCodeTree::ClauseMatcher::checkCandidate(Clause* cl, int& resolvedQuer
 //  return newMatches && matchGlobalVars(resolvedQueryLit);
 }
 
-bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQueryLit)
+template<bool sres>
+bool ClauseCodeTree::ClauseMatcher<sres>::matchGlobalVars(int& resolvedQueryLit)
 {
   //TODO: perform _set_, not _multiset_ subsumption for subsumption resolution
 
@@ -773,29 +796,30 @@ bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQueryLit)
   //  when we get to binding j-th literal
   //  Matches in ILStruct::matches are reordered, so that we always try
   //  the _first_ remaining[j,j] literals
+  // ILStruct::addMatch/deleteMatch maintain non-opposite matches in the
+  // prefix [0, nonOppositeMatchCnt). Try that prefix first to prefer
+  // subsumption over subsumption resolution.
   static TriangularArray<int> remaining(10);
+
+  static DArray<int> matchIndex;
+  matchIndex.ensure(clen);
+
+  /* First pass (allowOpposites=false) restricts remaining to non-opposite matches only.
+   * If that pass fails entirely, we retry allowing opposite matches too. */
+  bool allowOpposites=false;
+search_again:
   remaining.setSide(clen);
   for(unsigned j=0;j<clen;j++) {
     ILStruct* ils=lms[j]->getILS();
-    remaining.set(j,0,ils->matchCnt);
-
-//    VERB_OUT("matches "<<ils->matches.size()<<" index:"<<j<<" vars:"<<ils->varCnt<<" linfos:"<<lInfos.size());
-//    for(unsigned y=0;y<ils->matches.size();y++) {
-//      LitInfo* linf=&lInfos[ils->matches[y]->liIndex];
-//      VERB_OUT(" match "<<y<<" liIndex:"<<ils->matches[y]->liIndex<<" op: "<<linf->opposite);
-//      VERB_OUT(" hdr: "<<(*linf->ft)[0].number());
-//    }
-//    for(unsigned x=0;x<ils->varCnt;x++) {
-//      VERB_OUT(" glob var: "<<ils->sortedGlobalVarNumbers[x]);
-//      for(unsigned y=0;y<ils->matches.size();y++) {
-//	VERB_OUT(" match "<<y<<" binding: "<<ils->matches[y]->bindings[x]);
-//      }
-//    }
-  }
-//  VERB_OUT("secOp:"<<(lms[1]->op-1)->instr()<<" "<<(lms[1]->op-1)->arg());
+    unsigned matchesToTry = ils->matchCnt;
+    if constexpr (sres) {
+      if (!allowOpposites) {
+        matchesToTry = ils->nonOppositeMatchCnt;
+      }
+    }
+    remaining.set(j,0,matchesToTry);
+  }
 
-  static DArray<int> matchIndex;
-  matchIndex.ensure(clen);
   unsigned failLev=0;
   for(unsigned i=0;i<clen;i++) {
     matchIndex[i]=-1;
@@ -805,8 +829,15 @@ bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQueryLit)
     if(matchIndex[i]==remaining.get(i,i)) {
       //no more choices at this level, so try going up
       if(i==0) {
-	RSTAT_MCTR_INC("zero level fails at", failLev);
-	return false;
+        RSTAT_MCTR_INC("zero level fails at", failLev);
+        if constexpr (sres) {
+          if(!allowOpposites) {
+            /* Non-opposite-only pass failed, retry allowing opposite matches */
+            allowOpposites=true;
+            goto search_again;
+          }
+        }
+        return false;
       }
       i--;
       goto bind_next_match;
@@ -839,12 +870,12 @@ bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQueryLit)
   }
 
   resolvedQueryLit=-1;
-  if(sres) {
+  if constexpr (sres) {
     for(unsigned i=0;i<clen;i++) {
       ILStruct* ils=lms[i]->getILS();
       MatchInfo* mi=ils->getMatch(matchIndex[i]);
-      if(lInfos[mi->liIndex].opposite) {
-	resolvedQueryLit=lInfos[mi->liIndex].litIndex;
+      if(mi->opposite()) {
+	resolvedQueryLit=lInfos[mi->getLiIndex()].litIndex;
 	break;
       }
     }
@@ -853,20 +884,21 @@ bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQueryLit)
   return true;
 }
 
-bool ClauseCodeTree::ClauseMatcher::compatible(ILStruct* bi, MatchInfo* bq, ILStruct* ni, MatchInfo* nq)
+template<bool sres>
+bool ClauseCodeTree::ClauseMatcher<sres>::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) ) {
+  if( lInfos[bq->getLiIndex()].litIndex==lInfos[nq->getLiIndex()].litIndex ||
+      (bq->opposite() && nq->opposite()) ) {
     return false;
   }
 
   unsigned bvars=bi->varCnt;
   unsigned* bgvn=bi->sortedGlobalVarNumbers;
-  TermList* bb=bq->bindings;
+  TermList* bb=bq->getBindings();
 
   unsigned nvars=ni->varCnt;
   unsigned* ngvn=ni->sortedGlobalVarNumbers;
-  TermList* nb=nq->bindings;
+  TermList* nb=nq->getBindings();
 
   while(bvars && nvars) {
     while(bvars && *bgvn<*ngvn) {
@@ -898,7 +930,8 @@ bool ClauseCodeTree::ClauseMatcher::compatible(ILStruct* bi, MatchInfo* bq, ILSt
   return true;
 }
 
-bool ClauseCodeTree::ClauseMatcher::existsCompatibleMatch(ILStruct* si, MatchInfo* sq, ILStruct* targets)
+template<bool sres>
+bool ClauseCodeTree::ClauseMatcher<sres>::existsCompatibleMatch(ILStruct* si, MatchInfo* sq, ILStruct* targets)
 {
   size_t tcnt=targets->matchCnt;
   for(size_t i=0;i<tcnt;i++) {
@@ -909,4 +942,9 @@ bool ClauseCodeTree::ClauseMatcher::existsCompatibleMatch(ILStruct* si, MatchInf
   return false;
 }
 
+template struct ClauseCodeTree::LiteralMatcher<false>;
+template struct ClauseCodeTree::LiteralMatcher<true>;
+template struct ClauseCodeTree::ClauseMatcher<false>;
+template struct ClauseCodeTree::ClauseMatcher<true>;
+
 }
diff --git a/Indexing/ClauseCodeTree.hpp b/Indexing/ClauseCodeTree.hpp
index b1b9a3add..40a71aa54 100644
--- a/Indexing/ClauseCodeTree.hpp
+++ b/Indexing/ClauseCodeTree.hpp
@@ -56,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,/*sres*/false>
   {
+    using Base = Matcher</*removing*/true,false,/*sres*/false>;
+
     void init(CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_,
 	    const ClauseCodeTree& tree_, Stack<CodeOp*>* firstsInBlocks_);
 
@@ -68,17 +70,27 @@ class ClauseCodeTree : public CodeTree
 
   /** Context for finding matches of literals
    *
-   * Here the actual execution of the code of the tree takes place */
+   * Here the actual execution of the code of the tree takes place 
+   * sres selects between subsumption+resolution (true) and subsumption-only (false)
+   * */
+  template<bool sres>
   struct LiteralMatcher
-  : public Matcher</*removing*/false,false>
+  : public Matcher</*removing*/false,false,sres>
   {
-    void init(const CodeTree& tree, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, bool seekOnlySuccess=false);
+    using Base = Matcher</*removing*/false,false,sres>;
+    using Base::op;
+    using Base::_matched;
+    using Base::finished;
+    using Base::opposite;
+    using Base::execute;
+
+    void init(const CodeTree& tree, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, bool canEnterOpposites, bool seekOnlySuccess);
     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);
 
@@ -91,9 +103,10 @@ class ClauseCodeTree : public CodeTree
   };
 
 public:
+  template<bool sres>
   struct ClauseMatcher
   {
-    void init(ClauseCodeTree* tree_, Clause* query_, bool sres_);
+    void init(ClauseCodeTree* tree_, Clause* query_);
     void reset();
     bool keepRecycled() const { return lInfos.keepRecycled(); }
 
@@ -105,7 +118,7 @@ class ClauseCodeTree : public CodeTree
     USE_ALLOCATOR(ClauseMatcher);
 
   private:
-    void enterLiteral(CodeOp* entry, bool seekOnlySuccess);
+    void enterLiteral(CodeOp* entry, bool seekOnlySuccess, bool canEnterOpposites);
     void leaveLiteral();
     bool canEnterLiteral(CodeOp* op);
 
@@ -117,7 +130,6 @@ class ClauseCodeTree : public CodeTree
 
     Clause* query;
     ClauseCodeTree* tree;
-    bool sres;
 
     static const unsigned sresNoLiteral=static_cast<unsigned>(-1);
     unsigned sresLiteral;
@@ -134,7 +146,7 @@ class ClauseCodeTree : public CodeTree
      */
     DArray<LitInfo> lInfos;
 
-    Stack<Recycled<LiteralMatcher, NoReset>> lms;
+    Stack<Recycled<LiteralMatcher<sres>, NoReset>> lms;
   };
 
 private:
diff --git a/Indexing/CodeTree.cpp b/Indexing/CodeTree.cpp
index 0ce964484..0c356da19 100644
--- a/Indexing/CodeTree.cpp
+++ b/Indexing/CodeTree.cpp
@@ -39,6 +39,7 @@
 #define RED    ""
 #endif
 
+// If re-enabled, see the ASSERTION_VIOLATION in Matcher::init: opposite-literal matching doesn't support it yet.
 #define GROUND_TERM_CHECK 0
 
 #undef RSTAT_COLLECTION
@@ -132,9 +133,11 @@ void CodeTree::MatchInfo::destroy(unsigned bindCnt)
 }
 
 
-void CodeTree::MatchInfo::init(ILStruct* ils, unsigned liIndex_, DArray<TermList>& bindingArray)
+void CodeTree::MatchInfo::init(ILStruct* ils, unsigned liIndex_, DArray<TermList>& bindingArray, bool opposite)
 {
-  liIndex=liIndex_;
+  /* Pack liIndex and the opposite flag into _content (see getLiIndex/opposite) */
+  _setLiIndex(liIndex_);
+  _setOpposite(opposite);
   size_t bindCnt=ils->varCnt;
   if(bindCnt) {
     unsigned* perm=ils->globalVarPermutation;
@@ -261,11 +264,14 @@ void CodeTree::ILStruct::ensureFreshness(unsigned globalTimestamp)
     finished=false;
     noNonOppositeMatches=false;
     matchCnt=0;
+    nonOppositeMatchCnt=0;
   }
 }
 
-void CodeTree::ILStruct::addMatch(unsigned liIndex, DArray<TermList>& bindingArray)
+template<bool sres>
+void CodeTree::ILStruct::addMatch(unsigned liIndex, DArray<TermList>& bindingArray, bool opposite)
 {
+  ASS(sres || !opposite);
   if(matchCnt==matches.size()) {
     matches.expand(matchCnt ? (matchCnt*2) : 4);
     size_t newSize=matches.size();
@@ -277,7 +283,24 @@ void CodeTree::ILStruct::addMatch(unsigned liIndex, DArray<TermList>& bindingArr
   if(!matches[matchCnt]) {
     matches[matchCnt]=MatchInfo::alloc(varCnt);
   }
-  matches[matchCnt]->init(this, liIndex, bindingArray);
+  
+  if constexpr (sres) {
+    /* Maintain the invariant that non-opposite matches occupy [0, nonOppositeMatchCnt):
+    * an opposite match is simply appended, while a non-opposite match is swapped into
+    * position nonOppositeMatchCnt before that boundary is advanced. */
+    if(opposite) {
+      matches[matchCnt]->init(this, liIndex, bindingArray, /*opposite=*/true);
+    }
+    else {
+      if(nonOppositeMatchCnt!=matchCnt) {
+        swap(matches[nonOppositeMatchCnt], matches[matchCnt]);
+      }
+      matches[nonOppositeMatchCnt]->init(this, liIndex, bindingArray, /*opposite=*/false);
+      nonOppositeMatchCnt++;
+    }
+  } else {
+    matches[matchCnt]->init(this, liIndex, bindingArray, /*opposite=*/false);
+  }
   matchCnt++;
 }
 
@@ -289,14 +312,34 @@ void CodeTree::ILStruct::addMatch(unsigned liIndex, DArray<TermList>& bindingArr
  * to filter them by this function, the traversal should go from higher
  * indexes down to zero.
  */
+template<bool sres>
 void CodeTree::ILStruct::deleteMatch(unsigned matchIndex)
 {
   ASS_L(matchIndex, matchCnt);
 
   matchCnt--;
-  swap(matches[matchIndex], matches[matchCnt]);
+  if constexpr (sres) {
+    /* Removing a non-opposite match must preserve the [0, nonOppositeMatchCnt) invariant */
+    if(matchIndex<nonOppositeMatchCnt) {
+      nonOppositeMatchCnt--;
+      swap(matches[matchIndex], matches[nonOppositeMatchCnt]);
+      if(nonOppositeMatchCnt!=matchCnt) {
+        swap(matches[nonOppositeMatchCnt], matches[matchCnt]);
+      }
+    }
+    else {
+      swap(matches[matchIndex], matches[matchCnt]);
+    }
+  } else {
+    swap(matches[matchIndex], matches[matchCnt]);
+  }
 }
 
+template void CodeTree::ILStruct::addMatch<true>(unsigned, DArray<TermList>&, bool);
+template void CodeTree::ILStruct::addMatch<false>(unsigned, DArray<TermList>&, bool);
+template void CodeTree::ILStruct::deleteMatch<true>(unsigned);
+template void CodeTree::ILStruct::deleteMatch<false>(unsigned);
+
 CodeTree::MatchInfo*& CodeTree::ILStruct::getMatch(unsigned matchIndex)
 {
   ASS(!finished);
@@ -482,14 +525,19 @@ bool CodeTree::SearchStruct::getTargetOpPtr(const CodeOp& insertedOp, CodeOp**&
 // expose for ClauseCodeTree.cpp
 template bool CodeTree::SearchStruct::getTargetOpPtr<false>(const CodeOp&, CodeOp**&);
 
-CodeTree::CodeOp* CodeTree::SearchStruct::getTargetOp(const FlatTerm::Entry* ftPos)
+CodeTree::CodeOp* CodeTree::SearchStruct::getTargetOp(const FlatTerm::Entry* ftPos, bool opposite)
 {
   if(!ftPos->isFun()) { return 0; }
   switch(kind) {
   case FN_STRUCT:
+    /* if opposite is true, look up the negated predicate symbol instead */
+    if (opposite) {
+      return static_cast<FnSearchStruct*>(this)->targetOp<false>(ftPos->_number() ^ 1);
+    }
     return static_cast<FnSearchStruct*>(this)->targetOp<false>(ftPos->_number());
   case GROUND_TERM_STRUCT:
     ftPos++;
+    ASS(!opposite);
     ASS_EQ(ftPos->_tag(), FlatTerm::FUN_TERM_PTR);
     return static_cast<GroundTermSearchStruct*>(this)->targetOp<false>(ftPos->_term());
   default:
@@ -542,8 +590,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 sres>
+bool CodeTree::Matcher<removing, checkRange, sres>::execute()
 {
   if(fresh) {
     fresh=false;
@@ -557,11 +605,12 @@ bool CodeTree::Matcher<removing, checkRange>::execute()
 
   bool shouldBacktrack=false;
   for(;;) {
+    /* Note: doSearchStruct() also pushes onto btStack to handle opposite matches */
     if(op->alternative()) {
       if constexpr (removing) {
-        btStack.push(BTPointRemoving(tp, op->alternative(), RemovingBase::firstsInBlocks->size()));
+        btStack.push(BTPointRemoving(tp, MarkedOp(op->alternative(), opposite), RemovingBase::firstsInBlocks->size()));
       } else {
-        btStack.push(BTPoint(tp, op->alternative()));
+        btStack.push(BTPoint(tp, MarkedOp(op->alternative(), opposite)));
       }
     }
     switch(op->_instruction()) {
@@ -637,11 +686,16 @@ bool CodeTree::Matcher<removing, checkRange>::execute()
   }
 }
 
-template<bool removing, bool checkRange>
-void CodeTree::Matcher<removing, checkRange>::init(const CodeTree& tree_, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, Stack<CodeOp*>* firstsInBlocks_)
+template<bool removing, bool checkRange, bool sres>
+void CodeTree::Matcher<removing, checkRange, sres>::init(const CodeTree& tree_, CodeOp* entry_, bool canEnterOpposites_, LitInfo* linfos_, size_t linfoCnt_, Stack<CodeOp*>* firstsInBlocks_)
 {
   tree=&tree_;
+  canEnterOpposites=canEnterOpposites_;
+#if GROUND_TERM_CHECK
+  ASS(!canEnterOpposites);
+#endif
   entry=entry_;
+  opposite=false;
 
   linfos=linfos_;
   linfoCnt=linfoCnt_;
@@ -667,8 +721,8 @@ void CodeTree::Matcher<removing, checkRange>::init(const CodeTree& tree_, CodeOp
  * 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 sres>
+bool CodeTree::Matcher<removing, checkRange, sres>::backtrack()
 {
   if(btStack.isEmpty()) {
     curLInfo++;
@@ -676,7 +730,8 @@ bool CodeTree::Matcher<removing, checkRange>::backtrack()
   }
   auto bp=btStack.pop();
   tp=bp.tp;
-  op=bp.op;
+  op=bp.markedOp.getOp();
+  opposite=bp.markedOp.getMark();
   if constexpr (removing) {
     RemovingBase::firstsInBlocks->truncate(bp.fibDepth);
     RemovingBase::firstsInBlocks->push(op);
@@ -684,8 +739,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 sres>
+bool CodeTree::Matcher<removing, checkRange, sres>::prepareLiteral()
 {
   if constexpr (removing) {
     RemovingBase::firstsInBlocks->truncate(RemovingBase::initFIBDepth);
@@ -696,11 +751,12 @@ bool CodeTree::Matcher<removing, checkRange>::prepareLiteral()
   ft=linfos[curLInfo].ft;
   tp=0;
   op=entry;
+  opposite=false;
   return true;
 }
 
-template<bool removing, bool checkRange>
-inline bool CodeTree::Matcher<removing, checkRange>::doAssignVar()
+template<bool removing, bool checkRange, bool sres>
+inline bool CodeTree::Matcher<removing, checkRange, sres>::doAssignVar()
 {
   ASS_EQ(op->_instruction(), ASSIGN_VAR);
 
@@ -740,8 +796,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 sres>
+inline bool CodeTree::Matcher<removing, checkRange, sres>::doCheckVar()
 {
   ASS_EQ(op->_instruction(), CHECK_VAR);
 
@@ -772,23 +828,32 @@ 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 sres>
+inline bool CodeTree::Matcher<removing, checkRange, sres>::doCheckFun()
 {
   ASS_EQ(op->_instruction(), CHECK_FUN);
 
   unsigned functor=op->_arg();
   FlatTerm::Entry& fte=(*ft)[tp];
   if(!fte.isFun(functor)) {
-    return false;
+    /* the top-level predicate didn't match, so match 
+     * against negation for subsumption resolution */
+    if constexpr (!sres) {
+      return false;
+    }
+    if (canEnterOpposites && tp == 0 && fte.isOppositeFun(functor)) {
+      opposite=true;
+    } else {
+      return false;
+    }
   }
   fte.expand();
   tp+=FlatTerm::FUNCTION_ENTRY_COUNT;
   return true;
 }
 
-template<bool removing, bool checkRange>
-inline bool CodeTree::Matcher<removing, checkRange>::doCheckGroundTerm()
+template<bool removing, bool checkRange, bool sres>
+inline bool CodeTree::Matcher<removing, checkRange, sres>::doCheckGroundTerm()
 {
   ASS_EQ(op->_instruction(), CHECK_GROUND_TERM);
 
@@ -811,13 +876,29 @@ 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 sres>
+inline bool CodeTree::Matcher<removing, checkRange, sres>::doSearchStruct()
 {
   ASS_EQ(op->_instruction(), SEARCH_STRUCT);
 
   const FlatTerm::Entry* fte=&(*ft)[tp];
-  CodeOp* target=op->getSearchStruct()->getTargetOp(fte);
+  CodeOp* target=op->getSearchStruct()->getTargetOp(fte, /*opposite=*/false);
+  /* look up the branch for the negated predicate, so it
+   * can be tried on backtracking for subsumption resolution */
+  if constexpr (sres) {
+    if (canEnterOpposites && tp == 0 && op->getSearchStruct()->kind == SearchStruct::FN_STRUCT) {
+      CodeOp* alt = op->getSearchStruct()->getTargetOp(fte, /*opposite=*/true);
+      if (alt && target != alt) {
+        /* 'opposite' will be determined by doCheckFun
+        * when this backtracking point is resumed */
+        if constexpr (removing) {
+        btStack.emplace(tp, MarkedOp(alt, /*opposite=*/false), RemovingBase::firstsInBlocks->size());
+        } else {
+          btStack.emplace(tp, MarkedOp(alt, /*opposite=*/false));
+        }
+      }
+    }
+  }
   if(!target) {
     return false;
   }
@@ -828,9 +909,10 @@ 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, 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 11c81b11d..06274eece 100644
--- a/Indexing/CodeTree.hpp
+++ b/Indexing/CodeTree.hpp
@@ -18,6 +18,7 @@
 #include "Forwards.hpp"
 
 #include "Lib/Allocator.hpp"
+#include "Lib/BitUtils.hpp"
 #include "Lib/DArray.hpp"
 #include "Lib/DHMap.hpp"
 #include "Lib/Stack.hpp"
@@ -74,13 +75,23 @@ class CodeTree
 
   struct MatchInfo
   {
-    /** Index of the matched LitInfo in the EContext */
-    unsigned liIndex;
+    inline unsigned getLiIndex() const { return _liIndex(); }
+    inline TermList* getBindings() { return &bindings[0]; }
+    inline bool opposite() const { return _opposite(); }
+
+  private:
+    BITFIELD(64,
+      BITFIELD_MEMBER(bool, _opposite, _setOpposite, 1,
+      BITFIELD_MEMBER(unsigned, _liIndex, _setLiIndex, CHAR_BIT * sizeof(unsigned) - 1,
+      END_BITFIELD
+    )))
+    /** Index of the matched LitInfo in the EContext, with the opposite flag packed
+     * in alongside it. */
+    uint64_t _content = 0;
     /** array of bindings */
     TermList bindings[1];
 
-  private:
-    void init(ILStruct* ils, unsigned liIndex, DArray<TermList>& bindingArray);
+    void init(ILStruct* ils, unsigned liIndex, DArray<TermList>& bindingArray, bool opposite);
 
     static MatchInfo* alloc(unsigned bindCnt);
 
@@ -128,13 +139,19 @@ class CodeTree
     unsigned* globalVarPermutation;
 
     unsigned timestamp;
-    //from here on, the values are valid only if the timestamp is current
 
-    void addMatch(unsigned liIndex, DArray<TermList>& bindingArray);
-    void deleteMatch(unsigned matchIndex);
+    //from here on, the values are valid only if the timestamp is current
+    /** boolean template sres variable indicates whether this ILStruct supports subsumption resolution */
+    template<bool sres> void addMatch(unsigned liIndex, DArray<TermList>& bindingArray, bool opposite);
+    template<bool sres> void deleteMatch(unsigned matchIndex);
     MatchInfo*& getMatch(unsigned matchIndex);
 
     unsigned matchCnt;
+    /**
+    * non-opposite matches are stored first in [0, nonOppositeMatchCnt)
+    * opposite matches are stored after in [nonOppositeMatchCnt, matchCnt)
+    */
+    unsigned nonOppositeMatchCnt;
 
     /** all possible lits were tried to match */
     bool visited;
@@ -255,7 +272,7 @@ class CodeTree
      * Returns code op in the structure matching the content
      * of flat term entry @b ftPos.
      */
-    CodeOp* getTargetOp(const FlatTerm::Entry* ftPos);
+    CodeOp* getTargetOp(const FlatTerm::Entry* ftPos, bool opposite);
     inline size_t length() const { return targets.size(); }
 
     enum Kind
@@ -324,7 +341,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 sres>
   struct Matcher
     : public std::conditional<removing, RemovingBase, NonRemovingBase>::type
   {
@@ -332,26 +349,70 @@ class CodeTree
     // removing, which works on variables
     static_assert(removing || !checkRange);
 
+    /**
+     * A CodeOp* tagged in its lowest bit with the 'opposite' flag 
+     * When sres is false, it becomes a plain CodeOp*
+     */
+    class MarkedOp
+    {
+      using Content = typename std::conditional<sres, uint64_t, CodeOp*>::type;
+    public:
+      MarkedOp(CodeOp* op, bool mark) 
+      { 
+        if constexpr (sres) {
+          static_assert(alignof(CodeOp) >= 2, "CodeOp must be at least 2-byte aligned so its lowest bit is free for the mark");
+          static_assert(sizeof(void *) <= sizeof(uint64_t), "must be able to fit a pointer into a 64-bit integer");
+          _content = 0;
+          BitUtils::setBits<1, CHAR_BIT * sizeof(CodeOp*)>(_content, reinterpret_cast<uint64_t>(op));
+          BitUtils::setBits<0, 1>(_content, mark);
+        } else {
+          ASS(!mark);
+          _content = op;
+        }
+      }
+
+      CodeOp* getOp() const
+      {
+        if constexpr (sres) {
+          return reinterpret_cast<CodeOp*>(BitUtils::getBits<1, CHAR_BIT * sizeof(CodeOp*)>(_content));
+        } else {
+          return _content;
+        }
+      }
+
+      bool getMark() const
+      {
+        if constexpr (sres) {
+          return BitUtils::getBits<0, 1>(_content);
+        } else {
+          return false;
+        }
+      }
+
+    private:
+      Content _content = 0;
+    };
+
     /**
      * Backtracking point for the interpretation of the code tree.
      */
     struct BTPoint
     {
-      BTPoint(size_t tp, CodeOp* op) : tp(tp), op(op) {}
+      BTPoint(size_t tp, MarkedOp markedOp) : tp(tp), markedOp(markedOp) {}
 
       /** Position in the flat term */
       size_t tp;
-      /** Pointer to the next operation */
-      CodeOp* op;
+      /** Pointer to the next operation and mark encoding whether this is an opposite branch */
+      MarkedOp markedOp;
     };
 
     struct BTPointRemoving
     {
-      BTPointRemoving(size_t tp, CodeOp* op, size_t fibDepth)
-      : tp(tp), op(op), fibDepth(fibDepth) {}
+      BTPointRemoving(size_t tp, MarkedOp markedOp, size_t fibDepth)
+      : tp(tp), markedOp(markedOp), fibDepth(fibDepth) {}
 
       size_t tp;
-      CodeOp* op;
+      MarkedOp markedOp;
       size_t fibDepth;
     };
 
@@ -382,7 +443,7 @@ class CodeTree
     }
 
   protected:
-    void init(const CodeTree& tree_, CodeOp* entry_, LitInfo* linfos_ = 0,
+    void init(const CodeTree& tree_, CodeOp* entry_, bool canEnterOpposites, LitInfo* linfos_ = 0,
       size_t linfoCnt_ = 0, Stack<CodeOp*>* firstsInBlocks_ = 0);
 
     bool backtrack();
@@ -418,6 +479,15 @@ class CodeTree
     CodeOp* entry;
     CodeTree const* tree;
 
+    /** Whether the current execution branch matched via the opposite (negated) predicate */
+    bool opposite;
+
+    /**
+     * Whether this matcher is allowed to match a query literal against its opposite.
+     * False for e.g. RemovingLiteralMatcher, where subsumption resolution does not apply.
+     */
+    bool canEnterOpposites;
+
     /**
      * Array of alternative LitInfo objects
      *
diff --git a/Indexing/TermOrLiteralCodeTree.hpp b/Indexing/TermOrLiteralCodeTree.hpp
index a2fd5fb9b..81acbb779 100644
--- a/Indexing/TermOrLiteralCodeTree.hpp
+++ b/Indexing/TermOrLiteralCodeTree.hpp
@@ -97,11 +97,11 @@ class TermOrLiteralCodeTree : public CodeTree
 
 public:
   struct RemovingMatcher
-  : public Matcher</*removing=*/true,/*checkRange=*/false>
+  : public Matcher</*removing=*/true,/*checkRange=*/false,/*sres*/false>
   {
   public:
     void init(FlatTerm* ft_, const CodeTree& tree_, Stack<CodeOp*>* firstsInBlocks_) {
-      Matcher</*removing=*/true,/*checkRange=*/false>::init(tree_, tree_.getEntryPoint(), /*linfos_=*/0, /*linfoCnt_=*/0, firstsInBlocks_);
+      Matcher</*removing=*/true,/*checkRange=*/false,/*sres*/false>::init(tree_, tree_.getEntryPoint(), /*canEnterOpposites_=*/false, /*linfos_=*/0, /*linfoCnt_=*/0, firstsInBlocks_);
       firstsInBlocks->push(entry);
       ft=ft_;
       tp=0;
@@ -114,10 +114,10 @@ class TermOrLiteralCodeTree : public CodeTree
   };
 
   struct Matcher
-  : public CodeTree::Matcher</*removing*/false,/*checkRange=*/false>
+  : public CodeTree::Matcher</*removing*/false,/*checkRange=*/false,/*sres*/false>
   {
     void init(const CodeTree& tree, FlatTerm* ft_) {
-      CodeTree::Matcher</*removing*/false,/*checkRange=*/false>::init(tree,tree.getEntryPoint(), 0, 0);
+      CodeTree::Matcher</*removing*/false,/*checkRange=*/false,/*sres*/false>::init(tree,tree.getEntryPoint(), /*canEnterOpposites_=*/false, 0, 0);
       ft = ft_;
       tp = 0;
       op = entry;
diff --git a/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp b/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp
index 4823a311a..88568e796 100644
--- a/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp
+++ b/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp
@@ -29,6 +29,16 @@ CodeTreeForwardSubsumptionAndResolution::CodeTreeForwardSubsumptionAndResolution
 {}
 
 bool CodeTreeForwardSubsumptionAndResolution::perform(Clause *cl, Clause *&replacement, ClauseIterator &premises)
+{
+  if (_subsumptionResolution) {
+    return performWith</*sres=*/true>(cl, replacement, premises);
+  } else {
+    return performWith</*sres=*/false>(cl, replacement, premises);
+  }
+}
+
+template<bool sres>
+bool CodeTreeForwardSubsumptionAndResolution::performWith(Clause *cl, Clause *&replacement, ClauseIterator &premises)
 {
   if (_ct->isEmpty()) {
     return false;
@@ -40,9 +50,9 @@ bool CodeTreeForwardSubsumptionAndResolution::perform(Clause *cl, Clause *&repla
   constexpr double RSI_SKIP_PROB = 0.02;
   bool rsi = env.options->randomizedSimplifications();
 
-  static typename ClauseCodeTree::ClauseMatcher cm;
+  static typename ClauseCodeTree::template ClauseMatcher<sres> cm;
 
-  cm.init(_ct, cl, _subsumptionResolution);
+  cm.init(_ct, cl);
 
   Clause* premise;
   int resolvedQueryLit;
diff --git a/Inferences/CodeTreeForwardSubsumptionAndResolution.hpp b/Inferences/CodeTreeForwardSubsumptionAndResolution.hpp
index d3c892b53..7d8e5e5c5 100644
--- a/Inferences/CodeTreeForwardSubsumptionAndResolution.hpp
+++ b/Inferences/CodeTreeForwardSubsumptionAndResolution.hpp
@@ -34,6 +34,11 @@ class CodeTreeForwardSubsumptionAndResolution
                Kernel::ClauseIterator &premises) override;
 
 private:
+  template<bool sres>
+  bool performWith(Kernel::Clause *cl,
+               Kernel::Clause *&replacement,
+               Kernel::ClauseIterator &premises);
+
   const bool _subsumptionResolution;
   std::shared_ptr<Indexing::CodeTreeSubsumptionIndex> _index;
   Indexing::ClauseCodeTree* _ct;
diff --git a/Kernel/FlatTerm.hpp b/Kernel/FlatTerm.hpp
index 8afa86b12..2010c0cfc 100644
--- a/Kernel/FlatTerm.hpp
+++ b/Kernel/FlatTerm.hpp
@@ -61,6 +61,9 @@ class FlatTerm
     inline bool isVar(unsigned num) const { return isVar() && _number()==num; }
     inline bool isFun() const { return _tag()==FUN || _tag()==FUN_UNEXPANDED; }
     inline bool isFun(unsigned num) const { return isFun() && _number()==num; }
+    /* Literal headers encode polarity in their lowest bit, so xor-ing with 1
+     * gives the opposite (negated) predicate. Only meaningful for literal predicates. */
+    inline bool isOppositeFun(unsigned num) const { return isFun() && (_number()^1)==num; }
     /**
      * Should be called when @b isFun() is true.
      * If @b tag()==FUN_UNEXPANDED, it fills out entries for the functions
diff --git a/Shell/PartialRedundancyHandler.cpp b/Shell/PartialRedundancyHandler.cpp
index 3d273d0c6..adc187584 100644
--- a/Shell/PartialRedundancyHandler.cpp
+++ b/Shell/PartialRedundancyHandler.cpp
@@ -245,11 +245,12 @@ class PartialRedundancyHandler::ConstraintIndex
   }
 
   struct SubstMatcher
-  : public Matcher</*removing*/false,/*checkRange=*/false>
+  // TODO(HOL): consider turning higherOrder flag off for HOL
+  : public Matcher</*removing*/false,false,/*sres=*/false>
   {
     void init(const CodeTree& tree, const TermStack& ts)
     {
-      Matcher::init(tree,tree.getEntryPoint());
+      Matcher::init(tree, tree.getEntryPoint(), /*canEnterOpposites_=*/false);
 
       ft = FlatTerm::create(ts);
 
@@ -280,11 +281,11 @@ class PartialRedundancyHandler::ConstraintIndex
   };
 
   struct VariantMatcher
-  : public Matcher</*removing*/true,/*checkRange=*/true>
+  : public Matcher</*removing*/true,true,/*sres=*/false>
   {
   public:
     void init(FlatTerm* ft_, const CodeTree& tree_, Stack<CodeOp*>* firstsInBlocks_) {
-      Matcher::init(tree_, tree_.getEntryPoint(), 0, 0, firstsInBlocks_);
+      Matcher::init(tree_, tree_.getEntryPoint(), /*canEnterOpposites_=*/false, 0, 0, firstsInBlocks_);
       ft=ft_;
       tp=0;
       op=entry;
diff --git a/Shell/PredicateElimination.cpp b/Shell/PredicateElimination.cpp
index cade15932..bc9955ede 100644
--- a/Shell/PredicateElimination.cpp
+++ b/Shell/PredicateElimination.cpp
@@ -733,8 +733,8 @@ bool PredicateElimination::forwardSubsumedOrResolved(Clause *cl, Clause *&replac
     return false;
   }
 
-  static ClauseCodeTree::ClauseMatcher cm;
-  cm.init(&_ct, cl, /*sres=*/true);
+  static ClauseCodeTree::ClauseMatcher</*sres=*/true> cm;
+  cm.init(&_ct, cl);
 
   bool subsumed = false;
   Clause *premise;
diff --git a/UnitTests/tFlatTerm.cpp b/UnitTests/tFlatTerm.cpp
new file mode 100644
index 000000000..2918818a6
--- /dev/null
+++ b/UnitTests/tFlatTerm.cpp
@@ -0,0 +1,53 @@
+/*
+ * This file is part of the source code of the software program
+ * Vampire. It is protected by applicable
+ * copyright laws.
+ *
+ * This source code is distributed under the licence found here
+ * https://vprover.github.io/license.html
+ * and in the source directory
+ */
+
+#include "Test/UnitTesting.hpp"
+#include "Test/SyntaxSugar.hpp"
+#include "Kernel/FlatTerm.hpp"
+
+using namespace Kernel;
+
+/**
+ * FlatTerm::Entry::isOppositeFun relies on the fact that xor-ing a literal
+ * header with 1 gives the header of the complementary literal (see
+ * Literal::header/complementaryHeader in Kernel/Term.hpp). This test checks
+ * that relationship holds for the header actually stored in a FlatTerm built
+ * from a literal.
+ */
+TEST_FUN(isOppositeFun_matches_complementaryHeader) {
+  DECL_DEFAULT_VARS
+  DECL_SORT(srt)
+  DECL_CONST(a, srt)
+  DECL_PRED(p, {srt})
+  DECL_PRED(q, {srt})
+
+  Literal* lit1 = p(a);
+  Literal* lit2 = q(a);
+
+  FlatTerm* ft1 = FlatTerm::create(TermList(lit1));
+  FlatTerm* ft2 = FlatTerm::create(TermList(lit2));
+
+  ASS((*ft1)[0].isOppositeFun(lit1->complementaryHeader()))
+  ASS(!(*ft1)[0].isOppositeFun(lit1->header()))
+  ASS((*ft1)[0].isFun(lit1->header()))
+  ASS(!(*ft1)[0].isFun(lit1->complementaryHeader()))
+  ASS(!(*ft1)[0].isOppositeFun(lit2->header()))
+  ASS(!(*ft1)[0].isOppositeFun(lit2->complementaryHeader()))
+
+  ASS((*ft2)[0].isOppositeFun(lit2->complementaryHeader()))
+  ASS(!(*ft2)[0].isOppositeFun(lit2->header()))
+  ASS((*ft2)[0].isFun(lit2->header()))
+  ASS(!(*ft2)[0].isFun(lit2->complementaryHeader()))
+  ASS(!(*ft2)[0].isOppositeFun(lit1->header()))
+  ASS(!(*ft2)[0].isOppositeFun(lit1->complementaryHeader()))
+
+  ft1->destroy();
+  ft2->destroy();
+}
diff --git a/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp b/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp
index 3286cc7ed..3364714f8 100644
--- a/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp
+++ b/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp
@@ -50,12 +50,28 @@ using namespace Test;
     DECL_FUNC(i, {s}, s) \
     DECL_FUNC(i2, {s, s}, s) \
     DECL_PRED(p, {s}) \
+    DECL_PRED(p1, {s}) \
     DECL_PRED(p2, {s, s}) \
+    DECL_PRED(p2u, {s}) \
     DECL_PRED(p3, {s, s, s}) \
+    DECL_PRED(p3u, {s}) \
+    DECL_PRED(p4, {s}) \
+    DECL_PRED(p5, {s}) \
     DECL_PRED(q, {s}) \
+    DECL_PRED(q0, {s}) \
+    DECL_PRED(q1, {s}) \
     DECL_PRED(q2, {s, s}) \
     DECL_PRED(r, {s}) \
     DECL_PRED(r2, {s, s}) \
+    DECL_PRED(accessible_world, {s, s}) \
+    DECL_PRED(be, {s, s, s, s}) \
+    DECL_PRED(event, {s, s}) \
+    DECL_PRED(eventuality, {s, s}) \
+    DECL_PRED(human_person, {s, s}) \
+    DECL_PRED(proposition, {s, s}) \
+    DECL_PRED(smoke, {s, s}) \
+    DECL_PRED(state, {s, s}) \
+    DECL_PRED(think_believe_consider, {s, s}) \
   )
 
 namespace {
@@ -324,4 +340,70 @@ TEST_SIMPLIFICATION(neg_sub_res_test12,
     .justifications({ /* nothing */ })
 )
 
+TEST_SIMPLIFICATION(opposite_optimization_search_struct_1,
+  tester()
+    .simplifyWith({
+      clause({ accessible_world(x1, x2), ~human_person(x2, x3) }),
+      clause({ accessible_world(x1, x2), ~be(x2, x3, x4, x5) }),
+      clause({ think_believe_consider(x1, x3), ~think_believe_consider(x2, x3), accessible_world(x1, x2) }),
+      clause({ accessible_world(x1, x2), proposition(x1, x3) }),
+      clause({ ~state(x2, x3), accessible_world(x1, x2) }),
+      clause({ smoke(x1, x2), accessible_world(x1, x3) }),
+      clause({ accessible_world(x1, x3), ~event(x3, x2) }),
+      clause({ accessible_world(x1, x3), ~eventuality(x3, x2) }),
+      clause({ think_believe_consider(x1, x2), accessible_world(x1, x3) })
+    })
+    .toSimplify({
+      clause({
+        ~think_believe_consider(x1, x2),
+        accessible_world(x3, x1),
+        think_believe_consider(x4, x2),
+        accessible_world(x4, x3)
+      })
+    })
+    .expected({ /* nothing */ })
+    .justifications({
+      clause({
+        think_believe_consider(x1, x2),
+        accessible_world(x1, x3)
+      })
+    })
+)
+
+TEST_SIMPLIFICATION(opposite_optimization_search_struct_2,
+  tester()
+    .simplifyWith({
+      clause({ q0(f(x1)) }),
+      clause({ ~p1(x2) }),
+      clause({ ~p5(f(x1)) }),
+      clause({ ~r2(x1, x3), ~q1(x3) }),
+      clause({ ~p4(x2) }),
+      clause({ ~q1(d) }),
+      clause({ r2(x3, x1), ~p3u(x3) }),
+      clause({ r2(x3, x1), ~p1(x3) })
+    })
+    .toSimplify({
+      clause({
+        ~q0(x1),
+        ~q0(x4),
+        r2(x3, x2),
+        r2(x3, x1),
+        ~r2(x2, x4),
+        ~p2u(x3),
+        ~p3u(x2)
+      })
+    })
+    .expected({
+      clause({
+        ~q0(x1),
+        ~q0(x4),
+        r2(x3, x2),
+        r2(x3, x1),
+        ~p2u(x3),
+        ~p3u(x2)
+      })
+    })
+    .justifications({ clause({ r2(x3, x1), ~p3u(x3) }) })
+)
+
 }
diff --git a/cmake/sources.cmake b/cmake/sources.cmake
index 4469b0d77..eb0da6664 100644
--- a/cmake/sources.cmake
+++ b/cmake/sources.cmake
@@ -50,6 +50,7 @@ set(UNIT_TESTS
     UnitTests/tDeque.cpp
     UnitTests/tDisagreement.cpp
     UnitTests/tDynamicHeap.cpp
+    UnitTests/tFlatTerm.cpp
     UnitTests/tFunctionDefinitionHandler.cpp
     UnitTests/tHash.cpp
     UnitTests/tIndexManager.cpp