New results on rewrite-based satisfiability procedures