Big proof engines as little proof engines: new results on rewrite-based satisfiability procedures