The performance of automatic reasoning procedures relies on solving easy parts of a problem efficiently. For example, the CDCL calculus as well as SMT rely on partial models build from Horn clauses, actually literals. In the talk I discuss the role of Horn clause fragments in automatic reasoning for model building and simplification.