1. tarball for a satisfiability checker for propositional logic of common knowledge with S5 agent modalities written in Ocaml.