On Superposition-Based Satisfiability Procedures and Their Combination