Inprocessing is to apply clause simplification techniques during search and is a very attractive idea since it allows to apply computationally expensive techniques. In this paper we present the search space decomposition formalism SSD that models parallel SAT solvers with clause sharing and inprocessing. The main result of this paper is that the sharing model SSD is sound. In the formalism, we combine clause addition and clause elimination techniques, and it covers many SAT solvers such as PaSAT, PaMira, PMSat, MiraXT and ccc. Inprocessing is not used in these solvers, and we therefore propose a novel way how to combine clause sharing, search space decomposition and inprocessing.