Proof automation

1. REDIRECT Automated theorem proving

{{r from alternative name}}