None, but the tactic may fail finding a proof if every proof is in the search space that is pruned away. Pruning is controlled by d and w. Moreover, only lemmas whose type signature is a subset of the signature of the current sequent are considered. The signature of a sequent is ...TODO

It closes the current sequent by repeated application of rewriting steps (unless paramodulation is omitted), hypothesis and lemmas in the library.

None