diff --git a/Inferences/Factoring.cpp b/Inferences/Factoring.cpp
index 010624a2e..28720d8c1 100644
--- a/Inferences/Factoring.cpp
+++ b/Inferences/Factoring.cpp
@@ -31,89 +31,6 @@
 namespace Inferences
 {
 
-/**
- * This functor given a pair of literal indices
- * removes the second literal from the clause specified in constructor,
- * applies the substitution, and returns resulting clause.
- * (Also it records this to statistics as factoring.)
- */
-class Factoring::ResultsFn
-{
-public:
-  ResultsFn(Clause* cl, bool afterCheck, LiteralSelector &sel, Ordering& ord)
-  : _cl(cl), _cLen(cl->length()), _afterCheck(afterCheck), _sel(sel), _ord(ord) {}
-  Clause* operator() (std::pair<unsigned,unsigned> nums)
-  {
-    Literal* l1 = (*_cl)[nums.first];
-    Literal* l2 = (*_cl)[nums.second];
-
-    //we assume there are no duplicate literals
-    ASS(l1!=l2);
-
-    if(l1->isEquality())
-      //We don't perform factoring with equalities
-      return nullptr;
-
-    // check polarity and functor matches
-    if(!Literal::headersMatch(l1, l2, false))
-      return nullptr;
-
-    if(_sel.isNegativeForSelection(l1)) {
-      //We don't perform factoring on negative literals
-      // (this check only becomes relevant, when there is more than one literal selected
-      // and yet the selected ones are not all positive -- see the check in generateClauses)
-      return nullptr;
-    }
-
-    subst.reset();
-    if(!subst.unify(TermList(l1), 0, TermList(l2), 0))
-      return nullptr;
-
-    RStack<Literal*> resLits;
-
-    Literal *skipped = l2;
-
-    Literal* skippedAfter = 0;
-    if (_afterCheck && _cl->numSelected() > 1) {
-      TIME_TRACE(TimeTrace::LITERAL_ORDER_AFTERCHECK);
-
-      skippedAfter = subst.apply(skipped, 0);
-    }
-
-    for(unsigned i=0;i<_cLen;i++) {
-      Literal* curr=(*_cl)[i];
-      if(curr!=skipped) {
-        Literal* currAfter = subst.apply(curr, 0);
-
-        if (skippedAfter) {
-          TIME_TRACE(TimeTrace::LITERAL_ORDER_AFTERCHECK);
-
-          if (i < _cl->numSelected() && _ord.compare(currAfter,skippedAfter) == Ordering::GREATER) {
-            env.statistics->inferencesBlockedDueToOrderingAftercheck++;
-            return nullptr;
-          }
-        }
-
-        resLits->push(currAfter);
-      }
-    }
-
-    Clause *cl = Clause::fromStack(*resLits, GeneratingInference1(InferenceRule::FACTORING,_cl));
-    if(env.options->proofExtra() == Options::ProofExtra::FULL)
-      env.proofExtra.insert(cl, new FactoringExtra(l1, l2));
-    return cl;
-  }
-private:
-  static RobSubstitution subst;
-  Clause* _cl;
-  ///length of the premise clause
-  unsigned _cLen;
-  bool _afterCheck;
-  LiteralSelector& _sel;
-  Ordering& _ord;
-};
-RobSubstitution Factoring::ResultsFn::subst;
-
 /**
  * Return ClauseIterator, that yields clauses generated from
  * @b premise by the factoring inference rule.
@@ -132,6 +49,7 @@ RobSubstitution Factoring::ResultsFn::subst;
  */
 ClauseIterator Factoring::generateClauses(Clause* premise)
 {
+  // bail out before even creating a coroutine frame
   if(premise->length()<=1) {
     return ClauseIterator::getEmpty();
   }
@@ -139,15 +57,91 @@ ClauseIterator Factoring::generateClauses(Clause* premise)
     return ClauseIterator::getEmpty();
   }
 
-  auto it1 = getCombinationIterator(0u,premise->numSelected(),premise->length());
+  return pvi(factorings(premise));
+}
 
-  auto it2 = getMappingIterator(it1,ResultsFn(premise,
-      _salg.getOptions().literalMaximalityAftercheck() && _salg.getLiteralSelector().isBGComplete(),
-      _salg.getLiteralSelector(), _salg.getOrdering()));
+/**
+ * For each unordered pair of literals of @b premise with at least one of them selected,
+ * unify them, drop the second, apply the substitution to the rest, and yield the result.
+ */
+Generator<Clause*> Factoring::factorings(Clause* premise)
+{
+  LiteralSelector& sel = _salg.getLiteralSelector();
+  const Ordering& ord = _salg.getOrdering();
+  bool afterCheck = _salg.getOptions().literalMaximalityAftercheck() && sel.isBGComplete();
+  unsigned cLen = premise->length();
+
+  RobSubstitution subst;
+
+  for(unsigned fst=0; fst<premise->numSelected(); fst++) {
+    Literal* l1 = (*premise)[fst];
+
+    //We don't perform factoring with equalities
+    if(l1->isEquality())
+      continue;
+
+    //We don't perform factoring on negative literals
+    // (this check only becomes relevant, when there is more than one literal selected
+    // and yet the selected ones are not all positive -- see the check in generateClauses)
+    if(sel.isNegativeForSelection(l1))
+      continue;
+
+    for(unsigned snd=fst+1; snd<cLen; snd++) {
+      Literal* skipped = (*premise)[snd];
+
+      //we assume there are no duplicate literals
+      ASS(l1!=skipped);
+
+      // check polarity and functor matches
+      if(!Literal::headersMatch(l1, skipped, false))
+        continue;
+
+      subst.reset();
+      if(!subst.unify(TermList(l1), 0, TermList(skipped), 0))
+        continue;
+
+      Clause* factor;
+      {
+        RStack<Literal*> resLits;
+
+        Literal* skippedAfter = 0;
+        if (afterCheck && premise->numSelected() > 1) {
+          TIME_TRACE(TimeTrace::LITERAL_ORDER_AFTERCHECK);
+
+          skippedAfter = subst.apply(skipped, 0);
+        }
+
+        bool blocked = false;
+        for(unsigned i=0;i<cLen;i++) {
+          Literal* curr=(*premise)[i];
+          if(curr!=skipped) {
+            Literal* currAfter = subst.apply(curr, 0);
 
-  auto it3 = getFilteredIterator(it2, NonzeroFn());
+            if (skippedAfter) {
+              TIME_TRACE(TimeTrace::LITERAL_ORDER_AFTERCHECK);
 
-  return pvi( it3 );
+              if (i < premise->numSelected() && ord.compare(currAfter,skippedAfter) == Ordering::GREATER) {
+                env.statistics->inferencesBlockedDueToOrderingAftercheck++;
+                blocked = true;
+                break;
+              }
+            }
+
+            resLits->push(currAfter);
+          }
+        }
+        if(blocked)
+          continue;
+
+        factor = Clause::fromStack(*resLits, GeneratingInference1(InferenceRule::FACTORING,premise));
+      }
+
+      if(env.options->proofExtra() == Options::ProofExtra::FULL)
+        env.proofExtra.insert(factor, new FactoringExtra(l1, skipped));
+
+      co_yield factor;
+    }
+  }
 }
 
 }
diff --git a/Inferences/Factoring.hpp b/Inferences/Factoring.hpp
index 60c4af7a2..560139828 100644
--- a/Inferences/Factoring.hpp
+++ b/Inferences/Factoring.hpp
@@ -17,6 +17,7 @@
 #define __Factoring__
 
 #include "Forwards.hpp"
+#include "Lib/Generator.hpp"
 
 #include "InferenceEngine.hpp"
 #include "ProofExtra.hpp"
@@ -30,7 +31,9 @@ class Factoring
   Factoring(SaturationAlgorithm& salg) : _salg(salg) {}
   ClauseIterator generateClauses(Kernel::Clause* premise) override;
 private:
-  class ResultsFn;
+  /** every factor of @b premise, yielded lazily */
+  Lib::Generator<Kernel::Clause*> factorings(Kernel::Clause* premise);
+
   const SaturationAlgorithm& _salg;
 };
 
diff --git a/Inferences/Superposition.cpp b/Inferences/Superposition.cpp
index ac286282e..e21c65cd7 100644
--- a/Inferences/Superposition.cpp
+++ b/Inferences/Superposition.cpp
@@ -17,7 +17,6 @@
 #include "Forwards.hpp"
 #include "Lib/Environment.hpp"
 #include "Lib/Metaiterators.hpp"
-#include "Lib/PairUtils.hpp"
 #include "Lib/Recycled.hpp"
 #include "Lib/VirtualIterator.hpp"
 
@@ -50,7 +49,6 @@ using namespace Lib;
 using namespace Kernel;
 using namespace Indexing;
 using namespace Saturation;
-using std::pair;
 
 namespace Inferences {
 
@@ -64,60 +62,53 @@ Superposition<higherOrder>::Superposition(SaturationAlgorithm& salg)
 template<bool higherOrder>
 ClauseIterator Superposition<higherOrder>::generateClauses(Clause* premise)
 {
-  auto itf = premise->getSelectedLiteralIterator()
-    // Get an iterator of pairs of selected literals and rewritable subterms of those literals
-    // A subterm is rewritable (see EqHelper) if it is a non-variable subterm of either
-    // a maximal side of an equality or of a non-equational literal
-    .flatMap([this](Literal* lit)
-      // returns an iterator over the rewritable subterms
-      { return pushPairIntoRightIterator(lit, EqHelper::getSubtermIterator<higherOrder>(lit, _salg.getOrdering())); })
-
-    // Get clauses with a literal whose complement unifies with the rewritable subterm,
-    // returns a pair with the original pair and the unification result (includes substitution)
-    .flatMap([this](pair<Literal*, TypedTermList> arg)
-      { return pushPairIntoRightIterator(arg, _lhsIndex->getUwa<higherOrder>(arg.second, _salg.getOptions())); })
-
-    // Perform forward superposition
-    .map([this,premise](pair<pair<Literal*, TypedTermList>, QueryRes<AbstractingUnifier*, TermLiteralClause>> arg)
-      {
-        auto& qr = arg.second;
-        return performSuperposition(premise, arg.first.first, arg.first.second,
-	        qr.data->clause, qr.data->literal, qr.data->term, qr.unifier, true);
-      });
-
-  auto itb = premise->getSelectedLiteralIterator()
-    // Get LHSs of all selected positive literals for superposition
-    .flatMap([this](Literal* lit)
-      { return pvi( pushPairIntoRightIterator(lit, EqHelper::getSuperpositionLHSIterator(lit, _salg.getOrdering(), _salg.getOptions())) ); })
-
-    // Get clauses that unify with these LHSs, modulo abstraction
-    .flatMap([this] (pair<Literal*, TermList> arg)
-      { return pushPairIntoRightIterator(arg,
-          _subtermIndex->template getUwa<higherOrder>(TypedTermList(arg.second, SortHelper::getEqualityArgumentSort(arg.first)), _salg.getOptions())); })
-
-    // Perform backward superposition
-    .map([this,premise](pair<pair<Literal*, TermList>, QueryRes<AbstractingUnifier*, TermLiteralClause>> arg) -> Clause*
-    {
-      // Self-superpositions are only done in forwards mode
-      if (premise == arg.second.data->clause) {
-        return nullptr;
-      }
-
-      auto& qr = arg.second;
-      return performSuperposition(qr.data->clause, qr.data->literal, qr.data->term,
-        premise, arg.first.first, arg.first.second, qr.unifier, false);
-    });
-
-  // Add the results of forward and backward together
-  auto it1 = concatIters(std::move(itf),std::move(itb));
-
-  // Remove null elements - these can come from performSuperposition
-  auto it2 = getFilteredIterator(std::move(it1),NonzeroFn());
+  // the outer iterator ensures we update the time counter for superposition
+  return pvi(TIME_TRACE_ITER("superposition", superpositions(premise)));
+}
 
-  // The outer iterator ensures we update the time counter for superposition
-  auto it3 = TIME_TRACE_ITER("superposition", std::move(it2));
+/**
+ * Yield the result of every superposition that can be performed with @b premise as one of
+ * the two parents: first forwards (equations from the index rewrite @b premise), then
+ * backwards (equations of @b premise rewrite clauses from the index).
+ *
+ * @warning @b qr.unifier below aliases state owned by the index query iterator that is
+ * still being walked, and that state is undone as soon as the query iterator is advanced
+ * -- which is exactly what happens when this coroutine is resumed. So the clause must be
+ * built *before* the co_yield; never carry a QueryRes across one.
+ */
+template<bool higherOrder>
+Generator<Clause*> Superposition<higherOrder>::superpositions(Clause* premise)
+{
+  for (Literal* lit : premise->getSelectedLiteralIterator()) {
+    // a subterm is rewritable (see EqHelper) if it is a non-variable subterm of either
+    // a maximal side of an equality or of a non-equational literal
+    for (Term* rw : iterTraits(EqHelper::getSubtermIterator<higherOrder>(lit, _salg.getOrdering()))) {
+      TypedTermList rwTerm(rw);
+      // clauses with a literal whose complement unifies with the rewritable subterm,
+      // modulo abstraction
+      for (auto qr : iterTraits(_lhsIndex->template getUwa<higherOrder>(rwTerm, _salg.getOptions())))
+        if (Clause* generated = performSuperposition(premise, lit, rwTerm,
+              qr.data->clause, qr.data->literal, qr.data->term, qr.unifier, /*eqIsResult=*/true))
+          co_yield generated;
+    }
+  }
 
-  return pvi( std::move(it3) );
+  for (Literal* lit : premise->getSelectedLiteralIterator()) {
+    // LHSs of the selected positive literals to superpose from
+    for (TermList eqLHS : iterTraits(EqHelper::getSuperpositionLHSIterator(lit, _salg.getOrdering(), _salg.getOptions()))) {
+      TypedTermList query(eqLHS, SortHelper::getEqualityArgumentSort(lit));
+      // clauses that unify with these LHSs, modulo abstraction
+      for (auto qr : iterTraits(_subtermIndex->template getUwa<higherOrder>(query, _salg.getOptions()))) {
+        // self-superpositions are only done in forwards mode
+        if (premise == qr.data->clause)
+          continue;
+
+        if (Clause* generated = performSuperposition(qr.data->clause, qr.data->literal, qr.data->term,
+              premise, lit, eqLHS, qr.unifier, /*eqIsResult=*/false))
+          co_yield generated;
+      }
+    }
+  }
 }
 
 /**
diff --git a/Inferences/Superposition.hpp b/Inferences/Superposition.hpp
index 088973fe9..8bc23bf26 100644
--- a/Inferences/Superposition.hpp
+++ b/Inferences/Superposition.hpp
@@ -18,6 +18,7 @@
 
 #include "Forwards.hpp"
 #include "Indexing/TermIndex.hpp"
+#include "Lib/Generator.hpp"
 
 #include "InferenceEngine.hpp"
 #include "Inferences/ProofExtra.hpp"
@@ -37,6 +38,9 @@ class Superposition
   ClauseIterator generateClauses(Clause* premise) override;
 
 private:
+  /** every opportunity to superpose with @b premise as a parent, yielded lazily */
+  Generator<Clause*> superpositions(Clause* premise);
+
   Clause* performSuperposition(
     Clause* rwClause, Literal* rwLiteral, TermList rwTerm,
     Clause* eqClause, Literal* eqLiteral, TermList eqLHS,
diff --git a/Kernel/LookaheadLiteralSelector.cpp b/Kernel/LookaheadLiteralSelector.cpp
index 5c4b70925..2ffb638d8 100644
--- a/Kernel/LookaheadLiteralSelector.cpp
+++ b/Kernel/LookaheadLiteralSelector.cpp
@@ -38,132 +38,65 @@ using namespace Indexing;
 using namespace Saturation;
 
 /**
- * Iterator that yields the same number of elements as there are inferences
- * that can be performed with a clause that has the literal passed to
- * the constructor selected
+ * Return iterator with the same number of elements as there are inferences
+ * that can be performed with @b lit literal selected
  */
-struct LookaheadLiteralSelector::GenIteratorIterator
+VirtualIterator<std::tuple<>> LookaheadLiteralSelector::getGeneraingInferenceIterator(Literal* lit)
 {
-  using TermIndex = Indexing::TermIndex<TermLiteralClause>;
-  DECL_ELEMENT_TYPE(VirtualIterator<std::tuple<>>);
-
-  GenIteratorIterator(Literal* lit, LookaheadLiteralSelector& parent) : stage(0), lit(lit), prepared(false), _parent(parent)
-  { ASS(!env.higherOrder()); }
-
-  bool hasNext()
-  {
-    if(prepared) {
-      return true;
-    }
-
-    SaturationAlgorithm* salg=SaturationAlgorithm::tryGetInstance();
-    if(!salg) {
-      static bool errAnnounced = false;
-      if(!errAnnounced) {
-	errAnnounced = true;
-  std::cout<<"Using LookaheadLiteralSelector without having an SaturationAlgorithm object\n";
-      }
-      //we are too early, there's no saturation algorithm and therefore no generating inferences
-      prepared=false;
-      return false;
-    }
-
-  start:
-    switch(stage) {
-    case 0:  //resolution
-    {
-      auto gli = salg->tryGetGeneratingIndex<BinaryResolutionIndex>();
-      if(!gli) { stage++; goto start; }
+  return pvi(generatingInferences(lit));
+}
 
-      nextIt=pvi( dropElementType(gli->getUnifications(lit,true,false)) );
-      break;
-    }
-    case 1:  //backward superposition
-    {
-      auto bsi = salg->tryGetGeneratingIndex<SuperpositionSubtermIndex</*higherOrder=*/false>>();
-      if(!bsi) { stage++; goto start; }
-
-      nextIt=pvi( getMapAndFlattenIterator(
-	       EqHelper::getLHSIterator(lit, _parent._ord),
-	       TermUnificationRetriever(bsi.get())) );
-      break;
-    }
-    case 2:  //forward superposition
-    {
-      auto fsi=salg->tryGetGeneratingIndex<SuperpositionLHSIndex>();
-      if(!fsi) { stage++; goto start; }
-
-      nextIt=pvi( getMapAndFlattenIterator(
-	       EqHelper::getSubtermIterator</*higherOrder=*/false>(lit, _parent._ord), //TODO update for HO superposition
-	       TermUnificationRetriever(fsi.get())) );
-      break;
-    }
-    case 3:  //equality resolution
-    {
-      bool haveEqRes=false;
-      if(lit->isNegative() && lit->isEquality()) {
-	RobSubstitution rs;
-	if(rs.unify(*lit->nthArgument(0), 0, *lit->nthArgument(1), 0)) {
-	  haveEqRes=true;
-	  nextIt=pvi( dropElementType(getSingletonIterator(0)) );
-	}
-      }
-      if(!haveEqRes) {
-	stage++;
-	goto start;
-      }
-      break;
-    }
-    default:
-      ASSERTION_VIOLATION;
-    case 4:  //finish
-    {
-      prepared=false;
-      return false;
-    }
+/**
+ * Yield one (empty) element for each inference that could be performed with a clause
+ * that has @b lit selected. Only the *number* of elements matters -- see pickTheBest,
+ * which races these iterators against each other and stops as soon as one runs dry, so
+ * the elements themselves are never inspected and the substitutions are not retrieved.
+ *
+ * Being a coroutine matters here beyond readability: the index handles below are frame
+ * locals, so each stays alive for exactly as long as the query walking into it. In the
+ * hand-written state machine they were locals of hasNext() that died at the end of their
+ * case block, while the iterator they had been queried from lived on -- which only
+ * worked because the IndexManager keeps the index alive independently.
+ */
+Generator<std::tuple<>> LookaheadLiteralSelector::generatingInferences(Literal* lit)
+{
+  ASS(!env.higherOrder());
+
+  SaturationAlgorithm* salg=SaturationAlgorithm::tryGetInstance();
+  if(!salg) {
+    static bool errAnnounced = false;
+    if(!errAnnounced) {
+      errAnnounced = true;
+      std::cout<<"Using LookaheadLiteralSelector without having an SaturationAlgorithm object\n";
     }
-    prepared=true;
-    return true;
+    //we are too early, there's no saturation algorithm and therefore no generating inferences
+    co_return;
   }
 
-  VirtualIterator<std::tuple<>> next()
-  {
-    if(!prepared) {
-      ALWAYS(hasNext());
-    }
-    ASS(prepared);
-    prepared=false;
-    stage++;
-    return std::move(nextIt);
+  //resolution
+  if(auto gli = salg->tryGetGeneratingIndex<BinaryResolutionIndex>())
+    for([[maybe_unused]] auto qr : iterTraits(gli->getUnifications(lit, /* complementary */ true, /* retrieveSubst */ false)))
+      co_yield {};
+
+  //backward superposition
+  if(auto bsi = salg->tryGetGeneratingIndex<SuperpositionSubtermIndex</*higherOrder=*/false>>())
+    for(TypedTermList lhs : iterTraits(EqHelper::getLHSIterator(lit, _ord)))
+      for([[maybe_unused]] auto qr : iterTraits(bsi->getUnifications(lhs, /* retrieveSubst */ false)))
+        co_yield {};
+
+  //forward superposition
+  if(auto fsi = salg->tryGetGeneratingIndex<SuperpositionLHSIndex>())
+    //TODO update for HO superposition
+    for(Term* trm : iterTraits(EqHelper::getSubtermIterator</*higherOrder=*/false>(lit, _ord)))
+      for([[maybe_unused]] auto qr : iterTraits(fsi->getUnifications(TypedTermList(trm), /* retrieveSubst */ false)))
+        co_yield {};
+
+  //equality resolution
+  if(lit->isNegative() && lit->isEquality()) {
+    RobSubstitution rs;
+    if(rs.unify(*lit->nthArgument(0), 0, *lit->nthArgument(1), 0))
+      co_yield {};
   }
-private:
-
-  struct TermUnificationRetriever
-  {
-    TermUnificationRetriever(TermIndex* index) : _index(index) {}
-    VirtualIterator<std::tuple<>> operator()(TypedTermList trm)
-    {
-      return pvi(dropElementType(_index->getUnifications(trm, /* retrieveSubst */ false)));
-    }
-  private:
-    TermIndex* _index;
-  };
-
-  int stage;
-  Literal* lit;
-  bool prepared;
-  VirtualIterator<std::tuple<>> nextIt;
-
-  LookaheadLiteralSelector& _parent;
-};
-
-/**
- * Return iterator with the same number of elements as there are inferences
- * that can be performed with @b lit literal selected
- */
-VirtualIterator<std::tuple<>> LookaheadLiteralSelector::getGeneraingInferenceIterator(Literal* lit)
-{
-  return pvi( getFlattenedIterator(GenIteratorIterator(lit, *this)) );
 }
 
 /**
diff --git a/Kernel/LookaheadLiteralSelector.hpp b/Kernel/LookaheadLiteralSelector.hpp
index a8dc10f2a..78201464e 100644
--- a/Kernel/LookaheadLiteralSelector.hpp
+++ b/Kernel/LookaheadLiteralSelector.hpp
@@ -16,6 +16,7 @@
 #define __LookaheadLiteralSelector__
 
 #include "Forwards.hpp"
+#include "Lib/Generator.hpp"
 #include "Shell/Options.hpp"
 #include "LiteralSelector.hpp"
 
@@ -47,8 +48,7 @@ class LookaheadLiteralSelector
   Literal* pickTheBest(Literal** lits, unsigned cnt);
   void removeVariants(LiteralStack& lits);
   VirtualIterator<std::tuple<>> getGeneraingInferenceIterator(Literal* lit);
-
-  struct GenIteratorIterator;
+  Lib::Generator<std::tuple<>> generatingInferences(Literal* lit);
 
   bool _completeSelection;
   LiteralSelector* _startupSelector;
diff --git a/Lib/Generator.hpp b/Lib/Generator.hpp
new file mode 100644
index 000000000..7bdd03852
--- /dev/null
+++ b/Lib/Generator.hpp
@@ -0,0 +1,173 @@
+/*
+ * 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 Generator.hpp
+ * Defines class Generator, a lazy sequence produced by a C++20 coroutine.
+ */
+
+#ifndef __Generator__
+#define __Generator__
+
+#include <coroutine>
+#include <exception>
+#include <utility>
+
+#include "Lib/Allocator.hpp"
+#include "Lib/Option.hpp"
+#include "Lib/Reflection.hpp"
+
+namespace Lib {
+
+/**
+ * A lazily evaluated sequence of @b T, written as an ordinary function with loops that
+ * @b co_yield s its elements.
+ *
+ * A Generator satisfies Vampire's duck-typed iterator protocol (DECL_ELEMENT_TYPE plus
+ * @b hasNext() / @b next()), so it can be handed to @b pvi(), @b iterTraits(),
+ * @b TIME_TRACE_ITER etc. exactly like any other iterator:
+ *
+ *   Generator<Clause*> myRule(Clause* premise) {
+ *     for (Literal* lit : premise->getSelectedLiteralIterator())
+ *       if (Clause* c = doSomething(premise, lit))
+ *         co_yield c;
+ *   }
+ *   ...
+ *   ClauseIterator generateClauses(Clause* premise) { return pvi(myRule(premise)); }
+ *
+ * The object is move-only, and nothing at all runs until the first call to hasNext():
+ * merely creating a Generator has no side effects. Destroying a partially consumed
+ * Generator destroys the coroutine frame, which runs the destructors of everything the
+ * suspended body still has in scope -- so iterators the body was walking are released
+ * (and, for substitution trees, backtracked) just as they would be in a hand-written
+ * iterator chain.
+ *
+ * @warning A value borrowed from an iterator the body itself is driving must be consumed
+ * *before* the co_yield, never carried across one. The important case is a
+ * QueryRes<AbstractingUnifier*, ...> coming out of an index query: its @b unifier aliases
+ * state owned by the still-live substitution-tree iterator, and is undone as soon as that
+ * iterator is advanced -- which is precisely what happens when the Generator is resumed.
+ *
+ * @warning For the same reason do not open a TIME_TRACE scope that spans a co_yield:
+ * Shell::TimeTrace keeps a stack of open scopes, so a scope left open across a suspension
+ * would be charged for the consumer's work as well, would adopt the consumer's scopes as
+ * its children, and would break the LIFO discipline when the frame is destroyed. Wrap the
+ * whole Generator in TIME_TRACE_ITER at the call site instead, which measures exactly the
+ * intervals during which the body is actually running.
+ */
+template<class T>
+class Generator {
+public:
+  DECL_ELEMENT_TYPE(T);
+
+  class promise_type {
+    friend class Generator;
+
+    Option<T> _value;
+    std::exception_ptr _exception;
+
+  public:
+    // route the coroutine frame through Vampire's allocator; the compiler prefers the
+    // sized deallocation function, which is the one Lib::free needs
+    void *operator new(size_t size) { return Lib::alloc(size); }
+    void operator delete(void *ptr, size_t size) { Lib::free(ptr, size); }
+
+    Generator get_return_object()
+    { return Generator(std::coroutine_handle<promise_type>::from_promise(*this)); }
+
+    /* suspend_always: creating the Generator runs none of the body */
+    std::suspend_always initial_suspend() noexcept { return {}; }
+    /* suspend_always: the frame outlives the body, so that done() can be observed */
+    std::suspend_always final_suspend() noexcept { return {}; }
+
+    std::suspend_always yield_value(T value)
+    {
+      _value = some(std::move(value));
+      return {};
+    }
+
+    void return_void() {}
+
+    /* stash rather than rethrow: an exception must not escape while the frame is only
+     * half unwound. Generator::hasNext() rethrows it on the consumer's stack instead. */
+    void unhandled_exception() { _exception = std::current_exception(); }
+
+    /* this is a generator, not a task: co_await makes no sense here */
+    template<class U> std::suspend_never await_transform(U &&) = delete;
+  };
+
+  Generator() = default;
+
+  Generator(Generator const&) = delete;
+  Generator &operator=(Generator const&) = delete;
+
+  Generator(Generator &&other) noexcept
+    : _handle(std::exchange(other._handle, {})) {}
+
+  Generator &operator=(Generator &&other) noexcept
+  {
+    if(this != &other) {
+      if(_handle)
+        _handle.destroy();
+      _handle = std::exchange(other._handle, {});
+    }
+    return *this;
+  }
+
+  ~Generator()
+  {
+    if(_handle)
+      _handle.destroy();
+  }
+
+  bool hasNext()
+  {
+    if(!_handle)
+      return false;
+    // an element produced by an earlier hasNext() is still waiting to be taken:
+    // hasNext() must be idempotent
+    if(_handle.promise()._value.isSome())
+      return true;
+    if(_handle.done())
+      return false;
+
+    _handle.resume();
+
+    if(_handle.promise()._exception) {
+      // clear it first: the frame is destroyed by ~Generator, which must not see it again
+      auto exception = std::exchange(_handle.promise()._exception, {});
+      std::rethrow_exception(exception);
+    }
+
+    return _handle.promise()._value.isSome();
+  }
+
+  /**
+   * Return the next element.
+   *
+   * @warning as everywhere in Vampire, hasNext() must be called (and return true) before
+   * each call to this function.
+   */
+  T next()
+  {
+    ASS(_handle)
+    ASS(_handle.promise()._value.isSome())
+
+    return _handle.promise()._value.take().unwrap();
+  }
+
+private:
+  explicit Generator(std::coroutine_handle<promise_type> handle) : _handle(handle) {}
+
+  std::coroutine_handle<promise_type> _handle = nullptr;
+};
+
+} // namespace Lib
+
+#endif // __Generator__
diff --git a/UnitTests/tGenerator.cpp b/UnitTests/tGenerator.cpp
new file mode 100644
index 000000000..460bb7015
--- /dev/null
+++ b/UnitTests/tGenerator.cpp
@@ -0,0 +1,217 @@
+/*
+ * 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 "Lib/Generator.hpp"
+#include "Lib/Metaiterators.hpp"
+#include "Lib/Stack.hpp"
+#include "Lib/VirtualIterator.hpp"
+#include "Test/UnitTesting.hpp"
+
+using namespace Lib;
+
+static Generator<int> countTo(int n)
+{
+  for (int i = 0; i < n; i++)
+    co_yield i;
+}
+
+static Generator<int> nestedLoops()
+{
+  for (int i = 0; i < 3; i++)
+    for (int j = 0; j < 2; j++)
+      co_yield 10 * i + j;
+}
+
+static Stack<int> drain(Generator<int> gen)
+{
+  Stack<int> out;
+  while (gen.hasNext())
+    out.push(gen.next());
+  return out;
+}
+
+TEST_FUN(empty)
+{
+  auto gen = countTo(0);
+  ASS(!gen.hasNext())
+  // asking again is still fine
+  ASS(!gen.hasNext())
+}
+
+TEST_FUN(single_element)
+{
+  ASS_EQ(drain(countTo(1)), Stack<int>({0}))
+}
+
+TEST_FUN(nested_loops)
+{
+  ASS_EQ(drain(nestedLoops()), Stack<int>({0, 1, 10, 11, 20, 21}))
+}
+
+/** creating a Generator must not run any of its body: the first hasNext() does */
+TEST_FUN(lazy_start)
+{
+  bool started = false;
+  auto gen = [](bool& started) -> Generator<int> {
+    started = true;
+    co_yield 1;
+  }(started);
+
+  ASS(!started)
+  ASS(gen.hasNext())
+  ASS(started)
+  ASS_EQ(gen.next(), 1)
+}
+
+/** hasNext() must be idempotent: calling it twice must not consume an element */
+TEST_FUN(has_next_idempotent)
+{
+  auto gen = countTo(3);
+  Stack<int> out;
+  while (gen.hasNext()) {
+    ASS(gen.hasNext())
+    ASS(gen.hasNext())
+    out.push(gen.next());
+  }
+  ASS_EQ(out, Stack<int>({0, 1, 2}))
+}
+
+/** an exception thrown by the body surfaces on the consumer's stack, out of hasNext() */
+TEST_FUN(exception_propagates)
+{
+  auto gen = []() -> Generator<int> {
+    co_yield 7;
+    throw 42;
+  }();
+
+  ASS(gen.hasNext())
+  ASS_EQ(gen.next(), 7)
+
+  bool caught = false;
+  try {
+    gen.hasNext();
+  } catch (int thrown) {
+    caught = thrown == 42;
+  }
+  ASS(caught)
+}
+
+/** RAII probe: records in a counter when it is destroyed */
+struct DtorProbe {
+  int* destroyed;
+  DtorProbe(int* destroyed) : destroyed(destroyed) {}
+  DtorProbe(DtorProbe const&) = delete;
+  ~DtorProbe() { (*destroyed)++; }
+};
+
+/**
+ * Destroying a *partially consumed* Generator must run the destructors of everything the
+ * suspended body still holds. This is what releases (and backtracks) the substitution-tree
+ * iterators an inference rule was walking, and LookaheadLiteralSelector::pickTheBest relies
+ * on it: it abandons partially consumed iterators by design.
+ */
+TEST_FUN(destroy_while_suspended_runs_destructors)
+{
+  int destroyed = 0;
+  {
+    auto gen = [](int* destroyed) -> Generator<int> {
+      DtorProbe probe(destroyed);
+      for (int i = 0; i < 100; i++)
+        co_yield i;
+    }(&destroyed);
+
+    ASS(gen.hasNext())
+    ASS_EQ(gen.next(), 0)
+    ASS(gen.hasNext())
+    ASS_EQ(gen.next(), 1)
+    ASS_EQ(destroyed, 0)
+    // gen goes out of scope here, still suspended in the middle of the loop
+  }
+  ASS_EQ(destroyed, 1)
+}
+
+/** move-assigning over a partially consumed Generator destroys it just as ~Generator does */
+TEST_FUN(move_assign_destroys_old)
+{
+  int destroyed = 0;
+  auto make = [](int* destroyed) -> Generator<int> {
+    DtorProbe probe(destroyed);
+    for (int i = 0; i < 100; i++)
+      co_yield i;
+  };
+
+  auto gen = make(&destroyed);
+  ASS(gen.hasNext())
+  ASS_EQ(gen.next(), 0)
+  ASS_EQ(destroyed, 0)
+
+  gen = countTo(2);
+  ASS_EQ(destroyed, 1)
+  ASS(gen.hasNext())
+  ASS_EQ(gen.next(), 0)
+}
+
+/**
+ * The LookaheadLiteralSelector::pickTheBest access pattern in miniature: several
+ * generators alive at once, advanced round-robin one element each until one runs dry,
+ * then all abandoned.
+ */
+TEST_FUN(round_robin_then_abandon)
+{
+  int destroyed = 0;
+  auto make = [](int* destroyed, int n) -> Generator<int> {
+    DtorProbe probe(destroyed);
+    for (int i = 0; i < n; i++)
+      co_yield i;
+  };
+
+  Stack<Generator<int>> gens;
+  gens.push(make(&destroyed, 5));
+  gens.push(make(&destroyed, 2));
+  gens.push(make(&destroyed, 7));
+
+  unsigned exhausted = 0;
+  unsigned rounds = 0;
+  while (exhausted == 0) {
+    rounds++;
+    for (auto& gen : gens) {
+      if (gen.hasNext())
+        gen.next();
+      else
+        exhausted++;
+    }
+  }
+  // the shortest generator yields 2 elements, so it runs dry in the third round
+  ASS_EQ(rounds, 3u)
+  ASS_EQ(exhausted, 1u)
+
+  gens.reset();
+  ASS_EQ(destroyed, 3)
+}
+
+/** a Generator boxed into a VirtualIterator behaves identically */
+TEST_FUN(pvi_roundtrip)
+{
+  VirtualIterator<int> it = pvi(nestedLoops());
+  Stack<int> out;
+  while (it.hasNext())
+    out.push(it.next());
+  ASS_EQ(out, Stack<int>({0, 1, 10, 11, 20, 21}))
+}
+
+/** ...and composes with the usual combinators */
+TEST_FUN(composes_with_iter_traits)
+{
+  auto out = iterTraits(countTo(5))
+    .filter([](int x) { return x % 2 == 0; })
+    .map([](int x) { return x * 10; })
+    .collect<Stack>();
+  ASS_EQ(out, Stack<int>({0, 20, 40}))
+}
diff --git a/cmake/sources.cmake b/cmake/sources.cmake
index ef6438d31..bd9f64fca 100644
--- a/cmake/sources.cmake
+++ b/cmake/sources.cmake
@@ -51,6 +51,7 @@ set(UNIT_TESTS
     UnitTests/tDisagreement.cpp
     UnitTests/tDynamicHeap.cpp
     UnitTests/tFunctionDefinitionHandler.cpp
+    UnitTests/tGenerator.cpp
     UnitTests/tHash.cpp
     UnitTests/tIndexManager.cpp
     UnitTests/tInferences_AnswerLiteralProcessors.cpp
@@ -535,6 +536,7 @@ set(SOURCES
     Lib/Event.hpp
     Lib/Exception.cpp
     Lib/Exception.hpp
+    Lib/Generator.hpp
     Lib/Hash.hpp
     Lib/Int.cpp
     Lib/Int.hpp