Implements the axiomatic translation principle introduced in Schmidt and Hustadt (2003) for a range of modal logics. In conjunction with the translator FLOTTER and dfg2tptp (both are part of the MSPASS distribution) it can be used with any first-order logic theorem prover recognising DFG or TPTP input. This combination of tools effectively renders the most powerful and flexible fully automated theorem prover for modal logic and first-order logic available to date.