code: private boolean tryResolve(final CLClause c, final int pivot, final CLClause d) {
          assert !c.dumped() && !c.satisfied();
          assert !d.dumped() && !d.satisfied();
          boolean res = true;
          assert this.seen.empty();
          this.stats.steps++;
          for (int i = 0; i < c.lits().size(); i++) {
              final int lit = c.lits().get(i);
              if (lit == pivot) { continue; }
              assert marked(lit) == 0;
              mark(lit);
          }
          this.stats.steps++;
          for (int p = 0; res && p < d.lits().size(); p++) {
              final int lit = d.lits().get(p);
              if (lit == -pivot) { continue; }
              final int m = marked(lit);
              if (m > 0) { continue; }
              if (m < 0) { res = false; } else { mark(lit); }
          }
          unmark();
          return res;
      }
docs: Tries to resolve to clauses with a given pivot literal.  Returns {@code true} if the resolvent is not trivial,
  {@code false} otherwise.
  @param c     the first clause
  @param pivot the pivot literal
  @param d     the second clause
  @return {@code true} if the resolvent is not trivial