Automated Theorem Proving: Practicum