1. tarball for a satisfiability checker for description logic ALC with inverse roles (ALCI) also known as propositional mutimodal Kt written in Ocaml.