Automated theorem proving remains an active area of research at Argonne. In addition to continuing application of our existing systems to open problems in various domains, a number of research projects involve enhancements to OTTER and ROO. The first is AC unification, which is orthogonal to the closure approach. The next is induction, which will involve some modifications to the closure algorithm. We expect to (re)introduce interaction, in order to direct the system by hand when it is appropriate. And finally, we intend to address problems that require reasoning at multiple levels (the definition-unfolding problem). It remains to be seen just exactly how the closure algorithm itself will be modified, but we intend to preserve the overall approach.