A system for distributed simplification-based theorem proving