OTTER is not particularly conveniently structured as a library. While Overbeek was visiting the University of Texas in 1989, he wrote a library of formula management routines called FDB (Formula DataBase), in order to make some of the new indexing techniques available in library form. He and Ralph Butler turned this into a theorem prover that was competitive with OTTER in speed[1]. It is a good place to start for someone who wants to build his own system without re-implementing basic indexing routines and inference rules.