Rewriting-Based Provers