The goals of automated theorem
proving are: 1. to prove theorems, and 2. to do it automatically, or
mechanically. However, these goals sound easier than they really are.
One of the obstacles of automated theorem proving is that as the theorems
get more complicated, the time that the theorem prover spends increase
exponentially.

**Report**