code: private void backward(final int lit) {
          assert this.level == 0;
          assert this.dense;
          assert this.tostrengthen.empty();
          final CLOccs os = occs(lit);
          for (final CLClause c : os) {
              assert !c.redundant();
              this.stats.steps++;
              if (c.dumped()) { continue; }
              if (c.size() >= this.config.bwclslim) { continue; }
              if (satisfied(c)) { continue; }
              backward(c, lit);
          }
          while (!this.tostrengthen.empty()) {
              final Pair<CLClause, Integer> cplp = this.tostrengthen.back();
              this.tostrengthen.pop();
              strengthen(cplp.first(), cplp.second());
          }
      }
docs: Backward subsumes from clauses in the occurrence list of a given literal.
  @param lit the literal