ABSTRACT. In a recent work we have proposed a calculus for the multimodal logic K, where clauses are labelled by the level in which they occur. The calculus has been implemented and the evaluation shows that the prover performs well if the propositional symbols are uniformly distributed over the levels. However, by construction, the set of propositional clauses is always satisfiable. We are investigating the combination of SAT provers with our prover, in order to extract relevant information that could help reducing the time currently used during saturation.