Due to its computational interpretation, there has been a lot of interest in intuitinistic logic in computer science. Adding combinations of the intuitionistic modal axioms to intuitionistic modal logic IK results in different systems. Together they constitute the  intuitionistic modal logic cube. We use an embedding of intuitionistic model logic in higher order logic to verify this cube.  Automatic reasoning tools, such as Sledgehammer and Nitpick, were used to prove the inclusion relations between the cube's logics and the equality of some logics.