On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal