Summary: We formalize the idea that a set of propositional clauses that is not Horn-renamable can still be partially so. We show that for any finite set of clauses \(S\) defined on a set of variables \(V\), there exists a largest subset \(U\) of \(V\), with regard to inclusion, such that \(S\) is Horn-renamable with respect to \(U\); we call it the Horn basis of \(S\). If the Horn basis is not empty and \(S\) contains no unit clause, then deciding whether \(S\) is satisfiable reduces to deciding whether a proper subset of \(S\) is satisfiable. We show that the Horn basis can be computed in linear time.