The MODPROF theorem prover. This paper introduces MODPROF, a new theorem prover and model finder for propositional and modal logic K. MODPROF is based on labelled modal tableaux. Its novel feature is a sophisticated simplification algorithm using structural subsumption to detect redundancies. Further distinctive features are the use of syntactic branching, and an enhanced loop-checking algorithm using a cache of satisfiable worlds created in the course of the proof. Experimental results on problems of the TANCS 2000 Theorem Prover comparison are presented.