code: private void elim() {
          final long steps = this.limits.simpSteps;
          assert this.level == 0;
          assert !this.config.plain;
          if (!this.config.elim) { return; }
          assert this.simplifier == Simplifier.TOPSIMP;
          this.simplifier = Simplifier.ELIM;
          updateCands();
          final long limit;
          if (this.stats.simplifications <= this.config.elmrtc) { limit = Long.MAX_VALUE; } else {
              limit = this.stats.steps + 10 * steps / sizePenalty();
          }
          while (this.empty == null && !this.candsElim.empty() && this.stats.steps++ < limit) {
              final int cand = this.candsElim.top();
              final long priority = this.candsElim.priority(cand);
              this.candsElim.pop(cand);
              if (priority == 0 || !var(cand).free() || donotelim(cand)) { continue; }
              backward(cand);
              backward(-cand);
              if (tryElim(cand)) { doElim(cand); }
          }
          assert this.schedule;
          this.schedule = false;
          assert this.simplifier == Simplifier.ELIM;
          this.simplifier = Simplifier.TOPSIMP;
          dumpEliminatedRedundant();
      }
docs: (Bounded) Variable Elimination = (B)VE = Clause Distribution = DP.
  <p>
  This is the same bounded variable elimination technique as in the SatElite paper except that it performs
  subsumption and self-subsuming resolution on-the-fly while trying to eliminate a candidate variable.  It is also
  limited by the number of resolution steps.