diff --git a/Kernel/Inference.cpp b/Kernel/Inference.cpp
index 1ff8af68e..df3d76aa8 100644
--- a/Kernel/Inference.cpp
+++ b/Kernel/Inference.cpp
@@ -673,6 +673,8 @@ std::string Kernel::ruleName(InferenceRule rule)
     return "unused predicate definition removal";
   case InferenceRule::PURE_PREDICATE_REMOVAL:
     return "pure predicate removal";
+  case InferenceRule::PREDICATE_ELIMINATION:
+    return "predicate elimination";
   case InferenceRule::INEQUALITY_SPLITTING:
     return "inequality splitting";
   case InferenceRule::INEQUALITY_SPLITTING_NAME_INTRODUCTION:
diff --git a/Kernel/Inference.hpp b/Kernel/Inference.hpp
index 7ef5f3e2d..573e344ae 100644
--- a/Kernel/Inference.hpp
+++ b/Kernel/Inference.hpp
@@ -389,6 +389,8 @@ enum class InferenceRule : unsigned char {
   UNUSED_PREDICATE_DEFINITION_REMOVAL,
   /** pure predicate removal */
   PURE_PREDICATE_REMOVAL,
+  /** predicate elimination by exhaustive resolution (preprocessing) */
+  PREDICATE_ELIMINATION,
   /** inequality splitting */
   INEQUALITY_SPLITTING,
   /** inequality splitting name introduction */
diff --git a/Makefile b/Makefile
index 317ccb48c..58259fb17 100644
--- a/Makefile
+++ b/Makefile
@@ -392,6 +392,7 @@ VS_OBJ = Shell/AnswerLiteralManager.o\
          Shell/TheoryFlattening.o\
          Shell/TweeGoalTransformation.o\
          Shell/BlockedClauseElimination.o\
+         Shell/PredicateElimination.o\
          Shell/Token.o\
          Shell/TPTPPrinter.o\
          Shell/UIHelper.o\
diff --git a/Shell/Options.cpp b/Shell/Options.cpp
index d2b102602..3c8ad328f 100644
--- a/Shell/Options.cpp
+++ b/Shell/Options.cpp
@@ -570,6 +570,34 @@ void Options::init()
     _blockedClauseElimination.tag(OptionTag::PREPROCESSING);
     _blockedClauseElimination.addProblemConstraint(notWithCat(Property::UEQ));
 
+    _predicateElimination = BoolOptionValue("predicate_elimination","pel",false);
+    _predicateElimination.description=
+      "After clausification, eliminate predicates that occur at most once in every clause"
+      " by replacing their clauses with all pairwise resolvents (cf. Khasidashvili and Korovin, SAT 2016)."
+      " On problems without equality and theories, resolvents are computed with an mgu;"
+      " otherwise argument disequalities are introduced via (virtual) flattening,"
+      " which may add equality to a problem previously without it.";
+    _lookup.insert(&_predicateElimination);
+    _predicateElimination.tag(OptionTag::PREPROCESSING);
+    _predicateElimination.addProblemConstraint(notWithCat(Property::UEQ));
+
+    _predicateEliminationTotalLimit = FloatOptionValue("predicate_elimination_total_limit","peltl",2.0);
+    _predicateEliminationTotalLimit.description=
+      "A predicate elimination step is only performed if the estimated number of clauses afterwards"
+      " (current - |S_P| - |S_~P| + |S_P|*|S_~P|) does not exceed the number of clauses"
+      " before predicate elimination started times this factor.";
+    _lookup.insert(&_predicateEliminationTotalLimit);
+    _predicateEliminationTotalLimit.tag(OptionTag::PREPROCESSING);
+    _predicateEliminationTotalLimit.addConstraint(greaterThanEq(0.0f));
+    _predicateEliminationTotalLimit.onlyUsefulWith(_predicateElimination.is(equal(true)));
+
+    _predicateEliminationSubsumption = BoolOptionValue("predicate_elimination_subsumption","pels",true);
+    _predicateEliminationSubsumption.description=
+      "Keep the clause set forward-inter-subsumed and subsumption-resolved during predicate elimination.";
+    _lookup.insert(&_predicateEliminationSubsumption);
+    _predicateEliminationSubsumption.tag(OptionTag::PREPROCESSING);
+    _predicateEliminationSubsumption.onlyUsefulWith(_predicateElimination.is(equal(true)));
+
     _distinctGroupExpansionLimit = UnsignedOptionValue("distinct_group_expansion_limit","dgel",140);
     _distinctGroupExpansionLimit.description = "If a distinct group (defined, e.g., via TPTP's $distinct)"
          " is not larger than this limit, it will be expanded during preprocessing into quadratically many disequalities."
diff --git a/Shell/Options.hpp b/Shell/Options.hpp
index ee8465a28..79c83d47c 100644
--- a/Shell/Options.hpp
+++ b/Shell/Options.hpp
@@ -2059,6 +2059,9 @@ bool _hard;
 
   bool unusedPredicateDefinitionRemoval() const { return _unusedPredicateDefinitionRemoval.actualValue; }
   bool blockedClauseElimination() const { return _blockedClauseElimination.actualValue; }
+  bool predicateElimination() const { return _predicateElimination.actualValue; }
+  float predicateEliminationTotalLimit() const { return _predicateEliminationTotalLimit.actualValue; }
+  bool predicateEliminationSubsumption() const { return _predicateEliminationSubsumption.actualValue; }
   unsigned distinctGroupExpansionLimit() const { return _distinctGroupExpansionLimit.actualValue; }
   void setUnusedPredicateDefinitionRemoval(bool newVal) { _unusedPredicateDefinitionRemoval.actualValue = newVal; }
   SatSolver satSolver() const { return _satSolver.actualValue; }
@@ -2703,6 +2706,9 @@ bool _hard;
   ChoiceOptionValue<URResolution> _unitResultingResolution;
   BoolOptionValue _unusedPredicateDefinitionRemoval;
   BoolOptionValue _blockedClauseElimination;
+  BoolOptionValue _predicateElimination;
+  FloatOptionValue _predicateEliminationTotalLimit;
+  BoolOptionValue _predicateEliminationSubsumption;
   UnsignedOptionValue _distinctGroupExpansionLimit;
 
   OptionChoiceValues _tagNames;
diff --git a/Shell/PredicateElimination.cpp b/Shell/PredicateElimination.cpp
new file mode 100644
index 000000000..3a3904aa7
--- /dev/null
+++ b/Shell/PredicateElimination.cpp
@@ -0,0 +1,694 @@
+/*
+ * 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
+ */
+/**
+ * @file PredicateElimination.cpp
+ * Implements class PredicateElimination.
+ */
+
+#include "PredicateElimination.hpp"
+
+#include "Kernel/Clause.hpp"
+#include "Kernel/EqHelper.hpp"
+#include "Kernel/Formula.hpp"
+#include "Kernel/FormulaUnit.hpp"
+#include "Kernel/Inference.hpp"
+#include "Kernel/LiteralByMatchability.hpp"
+#include "Kernel/Problem.hpp"
+#include "Kernel/RobSubstitution.hpp"
+#include "Kernel/Signature.hpp"
+#include "Kernel/SortHelper.hpp"
+#include "Kernel/SubstHelper.hpp"
+#include "Kernel/Term.hpp"
+#include "Kernel/Unit.hpp"
+
+#include "Inferences/InferenceEngine.hpp"
+
+#include "Lib/Environment.hpp"
+
+#include "Shell/Options.hpp"
+#include "Shell/Shuffling.hpp"
+#include "Shell/Statistics.hpp"
+
+#include "Debug/TimeProfiling.hpp"
+
+#include <algorithm>
+
+namespace Shell {
+
+using namespace std;
+using namespace Lib;
+using namespace Kernel;
+using namespace Indexing;
+
+/**
+ * Renames variables by adding a fixed offset.
+ */
+struct VarShiftApplicator {
+  unsigned off;
+  TermList apply(unsigned var) const { return TermList(var + off, false); }
+};
+
+/**
+ * Replaces a single variable by a term, leaving other variables intact.
+ */
+struct SingleVarApplicator {
+  unsigned var;
+  TermList term;
+  TermList apply(unsigned v) const { return v == var ? term : TermList(v, false); }
+};
+
+void PredicateElimination::apply(Problem &prb)
+{
+  TIME_TRACE("predicate elimination");
+
+  // resolving clauses of different colours could produce colour-mixing resolvents
+  if (env.colorUsed) {
+    return;
+  }
+
+  // dropping non-unifiable pairs is only sound if equality and theories don't interfere
+  _equational = _forceEquationally || prb.hasEquality() || prb.hasInterpretedOperations() || prb.hasNumerals();
+
+  if (_useSubsumption) {
+    _subsIndex = new LiteralSubstitutionTree<LiteralClause>();
+  }
+
+  _preds.ensure(env.signature->predicates());
+
+  // clauses may still contain duplicate literals at this stage of preprocessing;
+  // besides making our occurrence counting needlessly conservative, they would,
+  // more importantly, violate an invariant of SATSubsumptionAndResolution
+  // (which in saturation is maintained by running this very simplification on every new clause)
+  Inferences::DuplicateLiteralRemovalISE duplicateLiteralRemoval;
+
+  Stack<Clause *> input;
+  UnitList::Iterator uit(prb.units());
+  while (uit.hasNext()) {
+    Unit *u = uit.next();
+    ASS(u->isClause());
+    Clause *cl = static_cast<Clause *>(u);
+    Clause *dedup = duplicateLiteralRemoval.simplify(cl);
+    if (dedup != cl) {
+      _modified = true;
+      cl = dedup;
+    }
+    input.push(cl);
+  }
+
+  if (_useSubsumption) {
+    // inserting shorter clauses first, the forward check below
+    // makes the initial clause set fully inter-subsumed
+    std::stable_sort(input.begin(), input.end(),
+                     [](Clause *a, Clause *b) { return a->length() < b->length(); });
+  }
+
+  for (Clause *cl : input) {
+    if (_useSubsumption) {
+      Clause *simplified = forwardSimplify(cl);
+      if (simplified != cl) { // subsumed away, or replaced by a subsumption resolution descendant
+        _modified = true;
+        if (!simplified) {
+          continue;
+        }
+        cl = simplified;
+      }
+    }
+    _all.push(cl);
+    registerClause(cl);
+    if (_useSubsumption) {
+      indexInsert(cl);
+    }
+  }
+  _curTotal = _origTotal = _all.size();
+
+  for (;;) {
+    int pred = pickCandidate();
+    if (pred < 0) {
+      break;
+    }
+    eliminate(prb, (unsigned)pred);
+  }
+
+  if (_modified) {
+    UnitList *res = 0;
+    Stack<Clause *>::Iterator it(_all);
+    while (it.hasNext()) {
+      Clause *cl = it.next();
+      if (!_deleted.contains(cl)) {
+        UnitList::push(cl, res);
+      }
+    }
+    prb.units() = res;
+    if (_keptDisequality) {
+      prb.reportEqualityAdded(true, _keptVarVarDisequality);
+    }
+    prb.invalidateProperty();
+  }
+
+  delete _subsIndex;
+  _subsIndex = nullptr;
+}
+
+void PredicateElimination::registerClause(Clause *cl)
+{
+  // for each tracked predicate of cl: +1/-1 for a single positive/negative occurrence, 2 for more than one
+  static DHMap<unsigned, int> occ;
+  occ.reset();
+
+  for (unsigned i = 0; i < cl->length(); i++) {
+    Literal *lit = (*cl)[i];
+    unsigned pred = lit->functor();
+    if (env.signature->getPredicate(pred)->protectedSymbol()) { // includes equality, interpreted and answer predicates
+      continue;
+    }
+    ASS(pred); // equality predicate is protected
+    int *val;
+    if (occ.getValuePtr(pred, val)) {
+      *val = lit->isPositive() ? 1 : -1;
+    }
+    else {
+      *val = 2;
+    }
+  }
+
+  DHMap<unsigned, int>::Iterator oit(occ);
+  while (oit.hasNext()) {
+    unsigned pred;
+    int val;
+    oit.next(pred, val);
+    if (val == 2) {
+      _preds[pred].blockers++;
+    }
+    else if (val == 1) {
+      _preds[pred].pos.insert(cl);
+    }
+    else {
+      _preds[pred].neg.insert(cl);
+    }
+  }
+}
+
+void PredicateElimination::unregisterClause(Clause *cl)
+{
+  static DHMap<unsigned, int> occ;
+  occ.reset();
+
+  for (unsigned i = 0; i < cl->length(); i++) {
+    Literal *lit = (*cl)[i];
+    unsigned pred = lit->functor();
+    if (env.signature->getPredicate(pred)->protectedSymbol()) {
+      continue;
+    }
+    int *val;
+    if (occ.getValuePtr(pred, val)) {
+      *val = lit->isPositive() ? 1 : -1;
+    }
+    else {
+      *val = 2;
+    }
+  }
+
+  DHMap<unsigned, int>::Iterator oit(occ);
+  while (oit.hasNext()) {
+    unsigned pred;
+    int val;
+    oit.next(pred, val);
+    if (val == 2) {
+      ASS_G(_preds[pred].blockers, 0);
+      _preds[pred].blockers--;
+    }
+    else if (val == 1) {
+      ALWAYS(_preds[pred].pos.remove(cl));
+    }
+    else {
+      ALWAYS(_preds[pred].neg.remove(cl));
+    }
+  }
+}
+
+bool PredicateElimination::eligible(unsigned pred) const
+{
+  const PredInfo &info = _preds[pred];
+  return !info.eliminated && info.blockers == 0 && (info.pos.size() + info.neg.size() > 0);
+}
+
+double PredicateElimination::estimatedTotalAfter(unsigned pred) const
+{
+  double sp = _preds[pred].pos.size();
+  double sn = _preds[pred].neg.size();
+  return (double)_curTotal - sp - sn + sp * sn;
+}
+
+bool PredicateElimination::admissible(unsigned pred) const
+{
+  return estimatedTotalAfter(pred) <= (double)_origTotal * _totalLimit;
+}
+
+int PredicateElimination::pickCandidate() const
+{
+  static Stack<unsigned> order;
+  order.reset();
+  for (unsigned pred = 1; pred < _preds.size(); pred++) {
+    order.push(pred);
+  }
+  if (env.options->randomTraversals()) {
+    // ties on the estimate get broken randomly
+    Shuffling::shuffleArray(order, order.size());
+  }
+
+  int best = -1;
+  double bestEst = 0.0;
+  for (unsigned pred : order) {
+    if (eligible(pred) && admissible(pred)) {
+      double est = estimatedTotalAfter(pred);
+      if (best < 0 || est < bestEst) {
+        best = pred;
+        bestEst = est;
+      }
+    }
+  }
+  return best;
+}
+
+Literal *PredicateElimination::findPredLiteral(Clause *cl, unsigned pred, bool polarity) const
+{
+  for (unsigned i = 0; i < cl->length(); i++) {
+    Literal *lit = (*cl)[i];
+    if (lit->functor() == pred && lit->isPositive() == polarity) {
+      return lit;
+    }
+  }
+  ASSERTION_VIOLATION;
+  return nullptr;
+}
+
+void PredicateElimination::eliminate(Problem &prb, unsigned pred)
+{
+  ASS(eligible(pred));
+
+  Stack<Clause *> posCls;
+  Stack<Clause *> negCls;
+  {
+    DHSet<Clause *>::Iterator pit(_preds[pred].pos);
+    while (pit.hasNext()) {
+      posCls.push(pit.next());
+    }
+    DHSet<Clause *>::Iterator nit(_preds[pred].neg);
+    while (nit.hasNext()) {
+      negCls.push(nit.next());
+    }
+  }
+
+  if (env.options->showPreprocessing()) {
+    cout << "[PP] pel eliminating " << env.signature->predicateName(pred)
+         << " (|S_P| = " << posCls.size() << ", |S_~P| = " << negCls.size() << ")" << endl;
+  }
+
+  // record the model-repairing definition while S_P is still at hand
+  recordElimination(prb, pred, posCls, negCls);
+
+  Stack<Clause *> resolvents;
+  for (Clause *c : posCls) {
+    Literal *plitC = findPredLiteral(c, pred, true);
+    for (Clause *d : negCls) {
+      Literal *plitD = findPredLiteral(d, pred, false);
+      Clause *r = buildResolvent(c, plitC, d, plitD);
+      if (r && _useSubsumption) {
+        r = forwardSimplify(r);
+      }
+      if (r) {
+        resolvents.push(r);
+        env.statistics->predicateEliminationResolvents++;
+        if (env.options->showPreprocessing()) {
+          cout << "[PP] pel resolvent: " << r->toString() << endl;
+        }
+      }
+    }
+  }
+
+  for (Clause *cl : posCls) {
+    unregisterClause(cl);
+    if (_useSubsumption) {
+      indexRemove(cl);
+    }
+    _deleted.insert(cl);
+  }
+  for (Clause *cl : negCls) {
+    unregisterClause(cl);
+    if (_useSubsumption) {
+      indexRemove(cl);
+    }
+    _deleted.insert(cl);
+  }
+  _curTotal -= posCls.size() + negCls.size();
+
+  for (Clause *r : resolvents) {
+    _all.push(r);
+    registerClause(r);
+    if (_useSubsumption) {
+      indexInsert(r);
+    }
+  }
+  _curTotal += resolvents.size();
+
+  _preds[pred].eliminated = true;
+  ASS(_preds[pred].pos.isEmpty());
+  ASS(_preds[pred].neg.isEmpty());
+
+  _modified = true;
+  env.statistics->eliminatedPredicates++;
+}
+
+Clause *PredicateElimination::buildResolvent(Clause *c, Literal *plitC, Clause *d, Literal *plitD)
+{
+  if (_equational) {
+    return buildResolventEq(c, plitC, d, plitD);
+  }
+  else {
+    return buildResolventMgu(c, plitC, d, plitD);
+  }
+}
+
+Clause *PredicateElimination::buildResolventMgu(Clause *c, Literal *plitC, Clause *d, Literal *plitD)
+{
+  static RobSubstitution subst;
+  subst.reset();
+  if (!subst.unifyArgs(plitC, 0, plitD, 1)) {
+    return nullptr; // sound to drop, since there is no equality (and no theories) around
+  }
+
+  static Stack<Literal *> lits;
+  lits.reset();
+  for (unsigned i = 0; i < c->length(); i++) {
+    Literal *lit = (*c)[i];
+    if (lit != plitC) {
+      lits.push(subst.apply(lit, 0));
+    }
+  }
+  for (unsigned i = 0; i < d->length(); i++) {
+    Literal *lit = (*d)[i];
+    if (lit != plitD) {
+      lits.push(subst.apply(lit, 1));
+    }
+  }
+  return assembleClause(lits, c, d);
+}
+
+Clause *PredicateElimination::buildResolventEq(Clause *c, Literal *plitC, Clause *d, Literal *plitD)
+{
+  ASS_EQ(plitC->arity(), plitD->arity());
+
+  VarShiftApplicator shift{c->maxVar() + 1};
+
+  static Stack<Literal *> lits;
+  lits.reset();
+  for (unsigned i = 0; i < c->length(); i++) {
+    Literal *lit = (*c)[i];
+    if (lit != plitC) {
+      lits.push(lit);
+    }
+  }
+  for (unsigned i = 0; i < d->length(); i++) {
+    Literal *lit = (*d)[i];
+    if (lit != plitD) {
+      lits.push(SubstHelper::apply(lit, shift));
+    }
+  }
+  // this is where the "virtual flattening" happens
+  for (unsigned i = 0; i < plitC->arity(); i++) {
+    lits.push(Literal::createEquality(false,
+                                      *plitC->nthArgument(i),
+                                      SubstHelper::apply(*plitD->nthArgument(i), shift),
+                                      SortHelper::getArgSort(plitC, i)));
+  }
+
+  // exhaustive equality substitution (note: no decomposition, so this is weaker than unification)
+  for (bool changed = true; changed;) {
+    changed = false;
+    for (unsigned idx = 0; idx < lits.size(); idx++) {
+      Literal *l = lits[idx];
+      if (!l->isEquality() || l->isPositive()) {
+        continue;
+      }
+      TermList a0 = *l->nthArgument(0);
+      TermList a1 = *l->nthArgument(1);
+      if (a0 == a1) { // t != t is simply false
+        swap(lits[idx], lits.top());
+        lits.pop();
+        changed = true;
+        break;
+      }
+      TermList var, tgt;
+      if (a0.isVar() && !a1.containsSubterm(a0)) {
+        var = a0;
+        tgt = a1;
+      }
+      else if (a1.isVar() && !a0.containsSubterm(a1)) {
+        var = a1;
+        tgt = a0;
+      }
+      else {
+        continue; // a residual disequality (to be kept)
+      }
+      swap(lits[idx], lits.top());
+      lits.pop();
+      SingleVarApplicator app{var.var(), tgt};
+      for (unsigned j = 0; j < lits.size(); j++) {
+        lits[j] = SubstHelper::apply(lits[j], app);
+      }
+      changed = true;
+      break;
+    }
+  }
+
+  return assembleClause(lits, c, d);
+}
+
+Clause *PredicateElimination::assembleClause(Stack<Literal *> &lits, Clause *c, Clause *d)
+{
+  static DHSet<Literal *> seen;
+  seen.reset();
+
+  static Stack<Literal *> out;
+  out.reset();
+
+  bool keptDiseq = false;
+  bool keptVarVarDiseq = false;
+
+  for (unsigned i = 0; i < lits.size(); i++) {
+    Literal *l = lits[i];
+    if (EqHelper::isEqTautology(l)) { // s = s
+      return nullptr;
+    }
+    if (l->isEquality() && l->isNegative() && *l->nthArgument(0) == *l->nthArgument(1)) {
+      continue; // t != t is simply false
+    }
+    if (seen.contains(Literal::complementaryLiteral(l))) { // a tautology
+      return nullptr;
+    }
+    if (!seen.insert(l)) {
+      continue; // a duplicate literal
+    }
+    out.push(l);
+    if (l->isEquality() && l->isNegative()) {
+      keptDiseq = true;
+      if (l->nthArgument(0)->isVar() && l->nthArgument(1)->isVar()) {
+        keptVarVarDiseq = true;
+      }
+    }
+  }
+
+  _keptDisequality |= keptDiseq;
+  _keptVarVarDisequality |= keptVarVarDiseq;
+
+  return Clause::fromStack(out, NonspecificInference2(InferenceRule::PREDICATE_ELIMINATION, c, d));
+}
+
+void PredicateElimination::recordElimination(Problem &prb, unsigned pred,
+                                             Stack<Clause *> const &posCls, Stack<Clause *> const &negCls)
+{
+  if (posCls.isEmpty()) { // P occurs only negatively; setting it to false satisfies all its clauses
+    prb.addTrivialPredicate(pred, false);
+    return;
+  }
+  if (negCls.isEmpty()) { // P occurs only positively
+    prb.addTrivialPredicate(pred, true);
+    return;
+  }
+
+  /* Following the model construction from the proof (cf. the paper):
+   * P(x0,...,xn-1) <=> \/_{D \/ P(ts) in S_P} exists ys. (x0 = ts[0] /\ ... /\ xn-1 = ts[n-1] /\ ~D)
+   * where each clause's variables ys are renamed away from the head variables x0,...,xn-1.
+   */
+  unsigned ar = env.signature->predicateArity(pred);
+
+  TermStack hargs;
+  for (unsigned v = 0; v < ar; v++) {
+    hargs.push(TermList::var(v));
+  }
+  Literal *head = Literal::create(pred, ar, true, hargs.begin());
+
+  VarShiftApplicator shift{ar}; // clause variables become >= ar, i.e. disjoint from the head's
+
+  FormulaList *disjuncts = FormulaList::empty();
+  Stack<Clause *>::ConstIterator cit(posCls);
+  while (cit.hasNext()) {
+    Clause *c = cit.next();
+    Literal *plit = findPredLiteral(c, pred, true);
+
+    FormulaList *conjuncts = FormulaList::empty();
+    for (unsigned i = 0; i < ar; i++) {
+      FormulaList::push(new AtomicFormula(Literal::createEquality(true,
+                                                                  TermList::var(i),
+                                                                  SubstHelper::apply(*plit->nthArgument(i), shift),
+                                                                  SortHelper::getArgSort(plit, i))),
+                        conjuncts);
+    }
+    for (unsigned i = 0; i < c->length(); i++) {
+      Literal *lit = (*c)[i];
+      if (lit != plit) {
+        FormulaList::push(new AtomicFormula(
+                              Literal::complementaryLiteral(SubstHelper::apply(lit, shift))),
+                          conjuncts);
+      }
+    }
+    Formula *inner = JunctionFormula::generalJunction(AND, conjuncts);
+
+    // existentially close over the (shifted) clause variables
+    DHMap<unsigned, TermList> varSorts;
+    SortHelper::collectVariableSorts(inner, varSorts);
+    VSList *vs = VSList::empty();
+    DHMap<unsigned, TermList>::Iterator vit(varSorts);
+    while (vit.hasNext()) {
+      unsigned var;
+      TermList sort;
+      vit.next(var, sort);
+      if (var >= ar) { // skip the head variables
+        VSList::push(VarSort(var, sort), vs);
+      }
+    }
+    Formula *disjunct = vs ? (Formula *)new QuantifiedFormula(EXISTS, vs, inner) : inner;
+    FormulaList::push(disjunct, disjuncts);
+  }
+
+  Formula *body = JunctionFormula::generalJunction(OR, disjuncts);
+  prb.addEliminatedPredicate(pred, new BinaryFormula(IFF, new AtomicFormula(head), body));
+}
+
+Clause *PredicateElimination::forwardSimplify(Clause *cl)
+{
+  ASS(_useSubsumption);
+
+  // every subsumption resolution step strictly shrinks the clause, so this terminates
+  for (;;) {
+    Clause *replacement = nullptr;
+    if (forwardSubsumedOrResolved(cl, replacement)) {
+      env.statistics->predicateEliminationSubsumed++;
+      return nullptr;
+    }
+    if (!replacement) {
+      return cl;
+    }
+    env.statistics->predicateEliminationSRs++;
+    if (env.options->showPreprocessing()) {
+      cout << "[PP] pel subsumption resolution: " << replacement->toString() << endl;
+    }
+    cl = replacement;
+  }
+}
+
+// a port of ForwardSubsumptionAndResolution::perform to our single-index setting
+// (unit and multi-literal clauses share one tree, distinguished by their length)
+bool PredicateElimination::forwardSubsumedOrResolved(Clause *cl, Clause *&replacement)
+{
+  ASS(_useSubsumption);
+  ASS(!replacement);
+
+  static DHSet<Clause *> checked; // shared by both passes below, as in FSAR
+  checked.reset();
+
+  Clause *conclusion = nullptr;
+
+  // pass 1: subsumption (and cheap subsumption resolution setup on the side)
+  for (unsigned i = 0; i < cl->length(); i++) {
+    Literal *lit = (*cl)[i];
+    auto rit = _subsIndex->getGeneralizations(lit, /*complementary=*/false, /*retrieveSubstitutions=*/false);
+    while (rit.hasNext()) {
+      Clause *mcl = rit.next().data->clause;
+      if (!checked.insert(mcl)) {
+        continue;
+      }
+      if (mcl->length() == 1) {
+        return true; // a unit generalization subsumes outright
+      }
+      bool checkS = mcl->length() <= cl->length();
+      bool checkSR = !conclusion;
+      if (checkS && _satSubs.checkSubsumption(mcl, cl, /*setSR=*/checkSR)) {
+        return true;
+      }
+      if (checkSR) {
+        // subsumption is preferred, so just remember the conclusion and keep scanning
+        conclusion = _satSubs.checkSubsumptionResolution(mcl, cl, /*forward=*/true, /*usePreviousSetUp=*/checkS);
+      }
+    }
+  }
+
+  if (conclusion) {
+    replacement = conclusion;
+    return false;
+  }
+
+  // pass 2: subsumption resolution against complementary matches
+  for (unsigned i = 0; i < cl->length(); i++) {
+    Literal *lit = (*cl)[i];
+    auto rit = _subsIndex->getGeneralizations(lit, /*complementary=*/true, /*retrieveSubstitutions=*/false);
+    while (rit.hasNext()) {
+      Clause *mcl = rit.next().data->clause;
+      if (mcl->length() == 1) { // the resolved literal is lit itself, no need to involve the SAT solver
+        replacement = SATSubsumption::SATSubsumptionAndResolution::getSubsumptionResolutionConclusion(cl, lit, mcl, /*forward=*/true);
+        return false;
+      }
+      if (!checked.insert(mcl)) {
+        continue;
+      }
+      conclusion = _satSubs.checkSubsumptionResolution(mcl, cl, /*forward=*/true, /*usePreviousSetUp=*/false);
+      if (conclusion) {
+        replacement = conclusion;
+        return false;
+      }
+    }
+  }
+
+  return false;
+}
+
+void PredicateElimination::indexInsert(Clause *cl)
+{
+  ASS(_useSubsumption);
+
+  if (cl->length() == 0) {
+    return; // the empty clause subsumes everything, but saturation will pick it up immediately anyway
+  }
+  Literal *key = (cl->length() == 1) ? (*cl)[0] : LiteralByMatchability::find_least_matchable_in(cl).lit();
+  ALWAYS(_indexedKey.insert(cl, key));
+  _subsIndex->insert(LiteralClause{key, cl});
+}
+
+void PredicateElimination::indexRemove(Clause *cl)
+{
+  ASS(_useSubsumption);
+
+  Literal *key;
+  if (_indexedKey.pop(cl, key)) {
+    _subsIndex->remove(LiteralClause{key, cl});
+  }
+}
+
+} // namespace Shell
diff --git a/Shell/PredicateElimination.hpp b/Shell/PredicateElimination.hpp
new file mode 100644
index 000000000..91a905502
--- /dev/null
+++ b/Shell/PredicateElimination.hpp
@@ -0,0 +1,132 @@
+/*
+ * 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
+ */
+/**
+ * @file PredicateElimination.hpp
+ * Defines class PredicateElimination.
+ */
+
+#ifndef __PredicateElimination__
+#define __PredicateElimination__
+
+#include "Forwards.hpp"
+
+#include "Kernel/Problem.hpp"
+
+#include "Lib/DArray.hpp"
+#include "Lib/DHMap.hpp"
+#include "Lib/DHSet.hpp"
+#include "Lib/Stack.hpp"
+
+#include "Indexing/Index.hpp"
+#include "Indexing/LiteralSubstitutionTree.hpp"
+#include "SATSubsumption/SATSubsumptionAndResolution.hpp"
+
+namespace Shell {
+
+using namespace Kernel;
+
+/**
+ * Predicate elimination for preprocessing of clausified problems,
+ * after Khasidashvili and Korovin: "Predicate Elimination for Preprocessing
+ * in First-Order Theorem Proving" (SAT 2016).
+ *
+ * A predicate P which occurs at most once in every clause (is "non-self-referential")
+ * can be eliminated by replacing the clauses S_P and S_~P (those containing P positively,
+ * respectively, negatively) by all the pairwise resolvents on P. In the presence
+ * of equality (or theories), the resolvents need to be computed via (virtual) flattening
+ * of the P-literals, i.e. C \/ P(ts) and D \/ ~P(ss) yield C \/ D' \/ t1 != s1' \/ ... \/ tn != sn'
+ * (with D renamed apart), simplified by the equality substitution rule
+ * (x != t \/ C ==> C[t/x], when x not in t). Without equality/theories it is
+ * sound (and avoids introducing equality) to use an mgu instead and drop
+ * the non-unifiable pairs.
+ *
+ * Elimination steps are subject to clause-growth limits estimated
+ * SAT-style as |S_P|*|S_~P| resolvents replacing |S_P|+|S_~P| clauses.
+ */
+class PredicateElimination {
+public:
+  /**
+   * @param forceEquationally  force the flattening-based resolvent computation even on
+   *        problems without equality/theories (required under FMB, whose model
+   *        reconstruction cannot rely on the Herbrand-interpretation argument
+   *        that justifies the mgu mode)
+   * @param totalLimit  an elimination step is admissible only if the estimated
+   *        number of clauses afterwards does not exceed the initial number times this factor
+   * @param useSubsumption  keep the clause set forward-inter-subsumed and
+   *        subsumption-resolved
+   */
+  PredicateElimination(bool forceEquationally, float totalLimit, bool useSubsumption)
+      : _forceEquationally(forceEquationally),
+        _totalLimit(totalLimit), _useSubsumption(useSubsumption) {}
+
+  void apply(Kernel::Problem &prb);
+
+private:
+  struct PredInfo {
+    Lib::DHSet<Clause *> pos; // S_P: clauses in which P occurs exactly once, positively
+    Lib::DHSet<Clause *> neg; // S_~P: dtto, negatively
+    unsigned blockers = 0;    // number of clauses in which P occurs more than once
+    bool eliminated = false;
+  };
+
+  // options
+  bool _forceEquationally;
+  float _totalLimit;
+  bool _useSubsumption;
+
+  // clause set state
+  Lib::Stack<Clause *> _all;     // all clauses ever seen, in insertion order
+  Lib::DHSet<Clause *> _deleted; // those of _all that have been eliminated
+  Lib::DArray<PredInfo> _preds;
+  size_t _curTotal = 0;
+  size_t _origTotal = 0;
+  bool _equational = false;
+  bool _modified = false;
+  bool _keptDisequality = false;       // some resolvent kept a residual disequality
+  bool _keptVarVarDisequality = false; // ... between two variables
+
+  void registerClause(Clause *cl);
+  void unregisterClause(Clause *cl);
+
+  bool eligible(unsigned pred) const;
+  double estimatedTotalAfter(unsigned pred) const;
+  bool admissible(unsigned pred) const;
+  int pickCandidate() const;
+
+  void eliminate(Problem &prb, unsigned pred);
+  Literal *findPredLiteral(Clause *cl, unsigned pred, bool polarity) const;
+
+  // resolvent construction; nullptr means no clause results (tautology / non-unifiable pair)
+  Clause *buildResolvent(Clause *c, Literal *plitC, Clause *d, Literal *plitD);
+  Clause *buildResolventMgu(Clause *c, Literal *plitC, Clause *d, Literal *plitD);
+  Clause *buildResolventEq(Clause *c, Literal *plitC, Clause *d, Literal *plitD);
+  Clause *assembleClause(Lib::Stack<Literal *> &lits, Clause *c, Clause *d);
+
+  // model reconstruction
+  void recordElimination(Problem &prb, unsigned pred, Lib::Stack<Clause *> const &posCls, Lib::Stack<Clause *> const &negCls);
+
+  // forward subsumption (and subsumption resolution) machinery, only used with _useSubsumption;
+  // the backward direction (new clauses simplifying older ones) is left as future work
+  Indexing::LiteralSubstitutionTree<Indexing::LiteralClause> *_subsIndex = nullptr;
+  Lib::DHMap<Clause *, Literal *> _indexedKey; // under which literal a clause got indexed
+  SATSubsumption::SATSubsumptionAndResolution _satSubs;
+  // simplify cl against the indexed clause set (to fixpoint): returns nullptr if cl
+  // is subsumed, otherwise cl itself or a subsumption-resolution descendant of it
+  Clause *forwardSimplify(Clause *cl);
+  // one round: true means subsumed; otherwise replacement is set to the
+  // subsumption resolution conclusion (or nullptr, if nothing applied)
+  bool forwardSubsumedOrResolved(Clause *cl, Clause *&replacement);
+  void indexInsert(Clause *cl);
+  void indexRemove(Clause *cl);
+};
+
+} // namespace Shell
+
+#endif /* __PredicateElimination__ */
diff --git a/Shell/Preprocess.cpp b/Shell/Preprocess.cpp
index 1a5b5c0f9..95a2fa00b 100644
--- a/Shell/Preprocess.cpp
+++ b/Shell/Preprocess.cpp
@@ -54,6 +54,7 @@
 #include "TheoryFlattening.hpp"
 #include "TweeGoalTransformation.hpp"
 #include "BlockedClauseElimination.hpp"
+#include "PredicateElimination.hpp"
 
 #include "UIHelper.hpp"
 #include "Lib/List.hpp"
@@ -466,6 +467,24 @@ void Preprocess::preprocess(Problem& prb)
      bce.apply(prb);
    }
 
+   if (_options.predicateElimination()) {
+     if (prb.isHigherOrder() || prb.hasPolymorphicSym()) { // in both cases, predicates could hide inside terms, breaking the occurrence counting
+       if (outputAllowed()) {
+         addCommentSignForSZS(std::cout);
+         std::cout << "WARNING: Not using PredicateElimination currently not compatible with polymorphic/higher-order inputs." << endl;
+       }
+     } else {
+       env.statistics->phase=ExecutionPhase::PREDICATE_ELIMINATION;
+       if (env.options->showPreprocessing())
+         std::cout << "predicate elimination" << std::endl;
+
+       PredicateElimination pel(/*forceEquationally=*/_options.saturationAlgorithm() == Options::SaturationAlgorithm::FINITE_MODEL_BUILDING,
+                                _options.predicateEliminationTotalLimit(),
+                                _options.predicateEliminationSubsumption());
+       pel.apply(prb);
+     }
+   }
+
    if (_options.shuffleInput()) {
      TIME_TRACE(TimeTrace::SHUFFLING);
      env.statistics->phase=ExecutionPhase::SHUFFLING;
diff --git a/Shell/Statistics.cpp b/Shell/Statistics.cpp
index f7b4febd4..b462d9793 100644
--- a/Shell/Statistics.cpp
+++ b/Shell/Statistics.cpp
@@ -189,6 +189,10 @@ void Statistics::print(std::ostream& out)
     ENTRY("Selected by SInE selection", selectedBySine);
     ENTRY("SInE iterations", sineIterations);
     ENTRY("Blocked clauses", blockedClauses);
+    ENTRY("Eliminated predicates", eliminatedPredicates);
+    ENTRY("Predicate elimination resolvents", predicateEliminationResolvents);
+    ENTRY("Predicate elimination subsumed", predicateEliminationSubsumed);
+    ENTRY("Predicate elimination subsumption resolutions", predicateEliminationSRs);
     ENTRY("Split inequalities", splitInequalities);
 
     GROUP("SATURATION");
@@ -382,6 +386,8 @@ const char* Statistics::phaseToString(ExecutionPhase p)
     return "Unused predicate definition removal";
   case ExecutionPhase::BLOCKED_CLAUSE_ELIMINATION:
     return "Blocked clause elimination";
+  case ExecutionPhase::PREDICATE_ELIMINATION:
+    return "Predicate elimination";
   case ExecutionPhase::TWEE:
     return "Twee Goal Transformation";
   case ExecutionPhase::ANSWER_LITERAL:
diff --git a/Shell/Statistics.hpp b/Shell/Statistics.hpp
index 163388c84..b52c3c0c0 100644
--- a/Shell/Statistics.hpp
+++ b/Shell/Statistics.hpp
@@ -70,6 +70,7 @@ enum class ExecutionPhase {
   PREPROCESS_1,
   UNUSED_PREDICATE_DEFINITION_REMOVAL,
   BLOCKED_CLAUSE_ELIMINATION,
+  PREDICATE_ELIMINATION,
   TWEE,
   ANSWER_LITERAL,
   PREPROCESS_2,
@@ -123,6 +124,14 @@ class Statistics {
   unsigned sineIterations = 0;
   /** number of detected blocked clauses */
   unsigned blockedClauses = 0;
+  /** number of predicates eliminated by predicate elimination */
+  unsigned eliminatedPredicates = 0;
+  /** number of resolvents kept during predicate elimination */
+  unsigned predicateEliminationResolvents = 0;
+  /** number of clauses deleted as subsumed during predicate elimination */
+  unsigned predicateEliminationSubsumed = 0;
+  /** number of subsumption resolutions performed during predicate elimination */
+  unsigned predicateEliminationSRs = 0;
 
   // Induction
   unsigned maxInductionDepth = 0;
diff --git a/UnitTests/tPredicateElimination.cpp b/UnitTests/tPredicateElimination.cpp
new file mode 100644
index 000000000..af8de45fc
--- /dev/null
+++ b/UnitTests/tPredicateElimination.cpp
@@ -0,0 +1,374 @@
+/*
+ * 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 <initializer_list>
+
+#include "Test/UnitTesting.hpp"
+#include "Test/SyntaxSugar.hpp"
+
+#include "Lib/Environment.hpp"
+#include "Shell/Statistics.hpp"
+
+#include "Kernel/Clause.hpp"
+#include "Kernel/Inference.hpp"
+#include "Kernel/Problem.hpp"
+#include "Kernel/Unit.hpp"
+
+#include "Shell/PredicateElimination.hpp"
+
+using namespace Kernel;
+using namespace Shell;
+
+static Problem *problemFromClauses(std::initializer_list<Clause *> cls)
+{
+  UnitList *units = UnitList::empty();
+  for (Clause *cl : cls) {
+    UnitList::push(cl, units);
+  }
+  return new Problem(units);
+}
+
+static Stack<Clause *> collectClauses(Problem &prb)
+{
+  Stack<Clause *> res;
+  UnitList::Iterator it(prb.units());
+  while (it.hasNext()) {
+    Unit *u = it.next();
+    ASS(u->isClause());
+    res.push(static_cast<Clause *>(u));
+  }
+  return res;
+}
+
+static bool containsPredicate(const Stack<Clause *> &cls, unsigned pred)
+{
+  for (Clause *cl : cls) {
+    for (unsigned i = 0; i < cl->length(); i++) {
+      if ((*cl)[i]->functor() == pred) {
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+/** the clause of the given length -- expected to exist and be unique */
+static Clause *theClauseOfLength(const Stack<Clause *> &cls, unsigned len)
+{
+  Clause *found = nullptr;
+  for (Clause *cl : cls) {
+    if (cl->length() == len) {
+      ASS(!found);
+      found = cl;
+    }
+  }
+  ASS(found);
+  return found;
+}
+
+static Stack<Clause *> runPE(std::initializer_list<Clause *> cls,
+                             bool forceEquationally = false,
+                             float totalLimit = 2.0,
+                             bool useSubsumption = false)
+{
+  Problem *prb = problemFromClauses(cls);
+  PredicateElimination pe(forceEquationally, totalLimit, useSubsumption);
+  pe.apply(*prb);
+  return collectClauses(*prb);
+}
+
+/* Note: many tests below include the clause {q(y) \/ ~q(f(y))}, in which q is
+ * "self-referential" and thus protected from elimination. Without such an anchor,
+ * eliminating p typically leaves q occurring in one polarity only, whereupon
+ * PE (correctly, but distractingly for the tests) deletes all the q-clauses too. */
+
+#define MY_SYNTAX_SUGAR \
+  DECL_DEFAULT_VARS     \
+  DECL_SORT(s)          \
+  DECL_CONST(a, s)      \
+  DECL_CONST(b, s)      \
+  DECL_CONST(c, s)      \
+  DECL_FUNC(f, {s}, s)  \
+  DECL_PRED(p, {s})     \
+  DECL_PRED(q, {s})     \
+  DECL_PRED(r, {s})
+
+TEST_FUN(mgu_basic)
+{
+  MY_SYNTAX_SUGAR
+
+  // {p(a)}, {~p(x) \/ q(x)} ---> {q(a)}
+  auto res = runPE({clause({p(a)}), clause({~p(x), q(x)}),
+                    clause({q(y), ~q(f(y))})});
+
+  ASS_EQ(res.size(), 2);
+  ASS(!containsPredicate(res, p.functor()));
+  Clause *resolvent = theClauseOfLength(res, 1);
+  ASS_EQ(resolvent->literalsOnlyToString(), "q(a)");
+  ASS(resolvent->inference().rule() == InferenceRule::PREDICATE_ELIMINATION);
+}
+
+TEST_FUN(mgu_nonunifiable_pair_dropped)
+{
+  MY_SYNTAX_SUGAR
+
+  // no equality in the problem: the pair does not unify, no resolvent
+  auto res = runPE({clause({p(a)}), clause({~p(b), q(b)}),
+                    clause({q(y), ~q(f(y))})});
+
+  ASS_EQ(res.size(), 1); // just the q-anchor
+  ASS(!containsPredicate(res, p.functor()));
+}
+
+TEST_FUN(mgu_empty_clause)
+{
+  MY_SYNTAX_SUGAR
+
+  // {p(a)}, {~p(a)} ---> the empty clause
+  auto res = runPE({clause({p(a)}), clause({~p(a)})});
+
+  ASS_EQ(res.size(), 1);
+  ASS_EQ(res[0]->length(), 0);
+}
+
+TEST_FUN(eq_residual_disequality)
+{
+  MY_SYNTAX_SUGAR
+
+  // forcing the equational mode: the non-unifiable pair now leaves a residual disequality
+  auto res = runPE({clause({p(a)}), clause({~p(b), q(b)}),
+                    clause({q(y), ~q(f(y))})},
+                   /*forceEquationally=*/true);
+
+  ASS_EQ(res.size(), 2);
+  ASS(!containsPredicate(res, p.functor()));
+  bool sawDiseq = false;
+  for (Clause *cl : res) {
+    for (unsigned i = 0; i < cl->length(); i++) {
+      Literal *l = (*cl)[i];
+      sawDiseq |= (l->isEquality() && l->isNegative());
+    }
+  }
+  ASS(sawDiseq);
+}
+
+TEST_FUN(eq_subst_computes_unifier)
+{
+  MY_SYNTAX_SUGAR
+
+  // {p2(f(x),x)}, {~p2(y,a) \/ q(y)} ---> {q(f(a))}, even equationally,
+  // since equality substitution resolves all the introduced disequalities away
+  DECL_PRED(p2, {s, s})
+  auto res = runPE({clause({p2(f(x), x)}), clause({~p2(y, a), q(y)}),
+                    clause({q(y), ~q(f(y))})},
+                   /*forceEquationally=*/true);
+
+  ASS_EQ(res.size(), 2);
+  ASS(!containsPredicate(res, p2.functor()));
+  Clause *resolvent = theClauseOfLength(res, 1);
+  ASS_EQ(resolvent->literalsOnlyToString(), "q(f(a))");
+}
+
+TEST_FUN(tautologies_dropped)
+{
+  MY_SYNTAX_SUGAR
+
+  // resolving on p yields the tautology {q(x) \/ ~q(x)}; then q disappears as well
+  auto res = runPE({clause({p(x), q(x)}), clause({~p(y), ~q(y)})});
+
+  ASS_EQ(res.size(), 0);
+}
+
+TEST_FUN(self_referential_skipped)
+{
+  MY_SYNTAX_SUGAR
+
+  // p occurs twice in the first clause, so it must survive
+  auto res = runPE({clause({p(x), p(f(x))}), clause({~p(a)})});
+
+  ASS_EQ(res.size(), 2);
+  ASS(containsPredicate(res, p.functor()));
+}
+
+TEST_FUN(pure_predicate_clauses_deleted)
+{
+  MY_SYNTAX_SUGAR
+
+  // p occurs only positively: its clause can simply be deleted
+  Problem *prb = problemFromClauses({clause({p(a), q(b)}), clause({q(y), ~q(f(y))})});
+  PredicateElimination pe(false, 2.0, false);
+  pe.apply(*prb);
+  auto res = collectClauses(*prb);
+
+  ASS_EQ(res.size(), 1);
+  ASS(!containsPredicate(res, p.functor()));
+  ASS(prb->interferences.isNonEmpty()); // the model-repairing definition of p got recorded
+}
+
+TEST_FUN(growth_limits_respected)
+{
+  MY_SYNTAX_SUGAR
+
+  // 3 x 3 occurrences of both p and r: eliminating either would mean
+  // 9 resolvents replacing 6 clauses -- not admissible under total limit 1.0
+  std::initializer_list<Clause *> cls = {
+      clause({p(x), r(a)}), clause({p(x), r(b)}), clause({p(x), r(c)}),
+      clause({~p(y), ~r(a)}), clause({~p(y), ~r(b)}), clause({~p(y), ~r(c)})};
+
+  auto res = runPE(cls, false, /*totalLimit=*/1.0);
+  ASS_EQ(res.size(), 6);
+  ASS(containsPredicate(res, p.functor()));
+
+  // with a benevolent limit, p gets eliminated
+  // (of the 9 resolvents, 3 are tautologies; and r is self-referential in the remaining 6)
+  auto res2 = runPE(cls, false, /*totalLimit=*/2.0);
+  ASS_EQ(res2.size(), 6);
+  ASS(!containsPredicate(res2, p.functor()));
+}
+
+TEST_FUN(duplicate_literals_removed)
+{
+  MY_SYNTAX_SUGAR
+
+  // the resolvent {q(a) \/ q(a)} gets condensed to {q(a)}
+  auto res = runPE({clause({p(a), q(a)}), clause({~p(x), q(x)}),
+                    clause({q(y), ~q(f(y))})});
+
+  ASS_EQ(res.size(), 2);
+  Clause *resolvent = theClauseOfLength(res, 1);
+  ASS_EQ(resolvent->literalsOnlyToString(), "q(a)");
+}
+
+TEST_FUN(subsumed_resolvents_not_added)
+{
+  MY_SYNTAX_SUGAR
+
+  // the resolvent q(a) is subsumed by the input clause {q(a)}
+  std::initializer_list<Clause *> cls = {
+      clause({q(a)}), clause({p(a)}), clause({~p(x), q(x)}),
+      clause({q(y), ~q(f(y))})};
+
+  auto res = runPE(cls, false, 2.0, /*useSubsumption=*/true);
+  ASS_EQ(res.size(), 2); // {q(a)} and the anchor; without subsumption we'd also keep a second copy of {q(a)}
+  ASS(!containsPredicate(res, p.functor()));
+
+  auto res2 = runPE(cls, false, 2.0, /*useSubsumption=*/false);
+  ASS_EQ(res2.size(), 3);
+}
+
+/** the clause concluded by subsumption resolution -- expected to exist and be unique */
+static Clause *theSRConclusion(const Stack<Clause *> &cls)
+{
+  Clause *found = nullptr;
+  for (Clause *cl : cls) {
+    if (cl->inference().rule() == InferenceRule::FORWARD_SUBSUMPTION_RESOLUTION) {
+      ASS(!found);
+      found = cl;
+    }
+  }
+  ASS(found);
+  return found;
+}
+
+TEST_FUN(sr_simplifies_resolvent)
+{
+  MY_SYNTAX_SUGAR
+
+  // eliminating p yields the resolvent {q(a) \/ ~r(a)}, which subsumption
+  // resolution against the unit {r(a)} shrinks to {q(a)};
+  // (afterwards, r is pure and {r(a)} goes away too)
+  auto res = runPE({clause({r(a)}), clause({p(a)}), clause({~p(x), q(x), ~r(x)}),
+                    clause({q(y), ~q(f(y))})},
+                   false, 2.0, /*useSubsumption=*/true);
+
+  ASS_EQ(res.size(), 2);
+  ASS(!containsPredicate(res, p.functor()));
+  ASS(!containsPredicate(res, r.functor()));
+  Clause *conclusion = theClauseOfLength(res, 1);
+  ASS_EQ(conclusion->literalsOnlyToString(), "q(a)");
+  ASS(conclusion->inference().rule() == InferenceRule::FORWARD_SUBSUMPTION_RESOLUTION);
+}
+
+TEST_FUN(sr_on_input_pass)
+{
+  MY_SYNTAX_SUGAR
+
+  // already the initial pass resolves {q(b) \/ ~r(a)} against {r(x)} down to {q(b)}
+  auto res = runPE({clause({r(x)}), clause({q(b), ~r(a)}),
+                    clause({q(y), ~q(f(y))})},
+                   false, 2.0, /*useSubsumption=*/true);
+
+  ASS_EQ(res.size(), 2);
+  ASS(!containsPredicate(res, r.functor()));
+  Clause *conclusion = theClauseOfLength(res, 1);
+  ASS_EQ(conclusion->literalsOnlyToString(), "q(b)");
+  ASS(conclusion->inference().rule() == InferenceRule::FORWARD_SUBSUMPTION_RESOLUTION);
+}
+
+TEST_FUN(sr_chains_to_fixpoint)
+{
+  MY_SYNTAX_SUGAR
+
+  // {~p(x) \/ q(x) \/ ~r(x) \/ ~r3(x)} gets shrunk by two successive subsumption
+  // resolution steps (against {r(y)} and {r3(y)}) to {~p(x) \/ q(x)} within
+  // a single forwardSimplify call; eliminating p then yields {q(a)}
+  DECL_PRED(r3, {s})
+  unsigned srsBefore = env.statistics->predicateEliminationSRs;
+  auto res = runPE({clause({p(a)}), clause({~p(x), q(x), ~r(x), ~r3(x)}),
+                    clause({r(y)}), clause({r3(y)}),
+                    clause({q(y), ~q(f(y))})},
+                   false, 2.0, /*useSubsumption=*/true);
+
+  ASS_EQ(env.statistics->predicateEliminationSRs - srsBefore, 2);
+  ASS_EQ(res.size(), 2);
+  ASS(!containsPredicate(res, p.functor()));
+  ASS(!containsPredicate(res, r.functor()));
+  ASS(!containsPredicate(res, r3.functor()));
+  Clause *resolvent = theClauseOfLength(res, 1);
+  ASS_EQ(resolvent->literalsOnlyToString(), "q(a)");
+  ASS(resolvent->inference().rule() == InferenceRule::PREDICATE_ELIMINATION);
+}
+
+TEST_FUN(duplicate_literals_in_input)
+{
+  MY_SYNTAX_SUGAR
+
+  // clauses can still carry duplicate literals when they reach predicate elimination
+  // (e.g. created by EqResWithDeletion from p(X) \/ p(a) \/ X != a);
+  // they must be removed on input, since SATSubsumptionAndResolution relies on
+  // premises being duplicate-free -- feeding it {p(a) \/ p(a)} as the main premise
+  // against the side premise {p(x) \/ ~p(y)} used to "conclude" the empty clause!
+  auto res = runPE({clause({p(a), p(a)}), clause({p(x), ~p(y)})},
+                   false, 2.0, /*useSubsumption=*/true);
+
+  ASS_EQ(res.size(), 2);
+  for (Clause *cl : res) {
+    ASS_G(cl->length(), 0); // and in particular: no bogus empty clause
+  }
+  Clause *dedup = theClauseOfLength(res, 1);
+  ASS_EQ(dedup->literalsOnlyToString(), "p(a)");
+}
+
+TEST_FUN(sr_multiliteral)
+{
+  MY_SYNTAX_SUGAR
+
+  // a multi-literal side premise {q(x) \/ ~r(x)} resolves {q(a) \/ r(a) \/ w(a)}
+  // down to {q(a) \/ w(a)} (exercising the SAT-based path, not just the unit shortcut)
+  DECL_PRED(w, {s})
+  auto res = runPE({clause({q(x), ~r(x)}), clause({q(y), ~q(f(y))}), clause({w(y), ~w(f(y))}),
+                    clause({q(a), r(a), w(a)})},
+                   false, 2.0, /*useSubsumption=*/true);
+
+  ASS_EQ(res.size(), 3); // the conclusion and the two anchors ({q(x) \/ ~r(x)} dies with pure r)
+  ASS(!containsPredicate(res, r.functor()));
+  Clause *conclusion = theSRConclusion(res);
+  ASS_EQ(conclusion->length(), 2);
+}
diff --git a/cmake/sources.cmake b/cmake/sources.cmake
index bb6599d7f..68991c572 100644
--- a/cmake/sources.cmake
+++ b/cmake/sources.cmake
@@ -97,6 +97,7 @@ set(UNIT_TESTS
     UnitTests/tLPO.cpp
     UnitTests/tList.cpp
     UnitTests/tOption.cpp
+    UnitTests/tPredicateElimination.cpp
     UnitTests/tOptionConstraints.cpp
     UnitTests/tQKbo.cpp
     UnitTests/tQuotientE.cpp
@@ -732,6 +733,8 @@ set(SOURCES
     Shell/PartialRedundancyHandler.hpp
     Shell/PredicateDefinition.cpp
     Shell/PredicateDefinition.hpp
+    Shell/PredicateElimination.cpp
+    Shell/PredicateElimination.hpp
     Shell/Preprocess.cpp
     Shell/Preprocess.cpp
     Shell/Preprocess.hpp
diff --git a/samplers/samplerFNT.smp b/samplers/samplerFNT.smp
index 9459b3945..b0a39332b 100644
--- a/samplers/samplerFNT.smp
+++ b/samplers/samplerFNT.smp
@@ -33,6 +33,15 @@ $nm=NZ > nm ~sgd 0.07,2
 $ins=Z > ins ~cat 0:1
 $ins=NZ > ins ~sgd 0.4,1
 
+# predicate_elimination
+> pel ~cat off:1,on:1
+
+# predicate_elimination_subsumption
+pel=on > pels ~cat on:4,off:1
+
+# predicate_elimination_total_limit
+pel=on > peltl ~uf 0.9,5.0
+
 # random_polarities
 > rp ~cat off:3,on:1
 
diff --git a/samplers/samplerFOL.smp b/samplers/samplerFOL.smp
index e34cc7ba7..e9526931e 100644
--- a/samplers/samplerFOL.smp
+++ b/samplers/samplerFOL.smp
@@ -38,6 +38,15 @@ $nm=NZ > nm ~sgd 0.07,2
 $ins=Z > ins ~cat 0:1
 $ins=NZ > ins ~sgd 0.4,1
 
+# predicate_elimination
+> pel ~cat off:1,on:1
+
+# predicate_elimination_subsumption
+pel=on > pels ~cat on:4,off:1
+
+# predicate_elimination_total_limit
+pel=on > peltl ~uf 0.9,5.0
+
 # random_polarities
 > rp ~cat off:3,on:1
 
diff --git a/samplers/samplerHOL.smp b/samplers/samplerHOL.smp
index 109dfc250..a98ea55d3 100644
--- a/samplers/samplerHOL.smp
+++ b/samplers/samplerHOL.smp
@@ -38,6 +38,15 @@ $nm=NZ > nm ~sgd 0.07,2
 $ins=Z > ins ~cat 0:1
 $ins=NZ > ins ~sgd 0.4,1
 
+# predicate_elimination
+> pel ~cat off:1,on:1
+
+# predicate_elimination_subsumption
+pel=on > pels ~cat on:4,off:1
+
+# predicate_elimination_total_limit
+pel=on > peltl ~uf 0.9,5.0
+
 # random_polarities
 > rp ~cat off:3,on:1
 
diff --git a/samplers/samplerIND.smp b/samplers/samplerIND.smp
index d5417eccd..d75689734 100644
--- a/samplers/samplerIND.smp
+++ b/samplers/samplerIND.smp
@@ -33,6 +33,15 @@ $nm=NZ > nm ~sgd 0.07,2
 $ins=Z > ins ~cat 0:1
 $ins=NZ > ins ~sgd 0.4,1
 
+# predicate_elimination
+> pel ~cat off:1,on:1
+
+# predicate_elimination_subsumption
+pel=on > pels ~cat on:4,off:1
+
+# predicate_elimination_total_limit
+pel=on > peltl ~uf 0.9,5.0
+
 # random_polarities
 > rp ~cat off:3,on:1
 
diff --git a/samplers/samplerSMT.smp b/samplers/samplerSMT.smp
index c33048cee..09d596bec 100644
--- a/samplers/samplerSMT.smp
+++ b/samplers/samplerSMT.smp
@@ -36,6 +36,15 @@ $nm=NZ > nm ~sgd 0.07,2
 $ins=Z > ins ~cat 0:1
 $ins=NZ > ins ~sgd 0.4,1
 
+# predicate_elimination
+> pel ~cat off:1,on:1
+
+# predicate_elimination_subsumption
+pel=on > pels ~cat on:4,off:1
+
+# predicate_elimination_total_limit
+pel=on > peltl ~uf 0.9,5.0
+
 # random_polarities
 > rp ~cat off:3,on:1