High performance simplification-based automated deduction