CK+CEM+MP(+ID), CK+CSO(+MP+CEM) are not available.
Remember that flat CK+ID+CSO=cumulative logic C
NESCOND implements the nested sequent calculi for normal conditional logics introduced and described in the following papers, where you can find more details about them:
Regis Alenda, Nicola Olivetti, Gian Luca Pozzato. Nested Sequents Calculi for Normal Conditional Logics, to appear in the Journal of Logic and Computation 
Regis Alenda, Nicola Olivetti, Gian Luca Pozzato, Nested Sequent Calculi for Conditional Logics. In Luis Farinas del Cerro, Andreas Herzig, Jéròme Mengin, Eds, Logics in Artificial Intelligence - 13th European Conference, JELIA 2012, Lecture Notes in Artificial Intelligence 7519, Springer, pp. 14 - 27, 2012
The theorem prover NESCOND is described in the following papers:
Nicola Olivetti, Gian Luca Pozzato. NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics, In Stephane Demri, Deepak Kapur, Christoph Weidenbach, Eds, Proceedings of IJCAR 2014 (7th International Joint Conference on Automated Reasoning), Lecture Notes in Artificial Intelligence LNAI 8562, Springer, pp. 511-518, 2014.
Nicola Olivetti, Gian Luca Pozzato. Nested Sequent Calculi and Theorem Proving for Normal Conditional Logics, In Marianna Nicolosi Asmundo, Domenico Cantone, Eds, Proceedings of CILC 2013, CEUR Workshop Proceedings 1068, pp. 49 - 63, 2013.
Copyright 2013 Nicola Olivetti, Gian Luca Pozzato. NESCOND is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. NESCOND is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with NESCOND. If not, see http://www.gnu.org/licenses/.