In this talk we overview the AVATAR architecture for saturation-based theorem provers.

This invited talk was presented at the Special Session on the Past, Present and Future of Automated Deduction at the International Conference on Automated Deduction (CADE-25).