Automated Theorem Proving: Assignments