NP-completeness of testing whether a SAT formula does not contain any redundant clause
The proof in theorem 1 in [Liberatore'02] shows that irredundancy is NP-hard by reducing SAT to it. Considering any set of non-tautological clauses $\Gamma=\{\gamma_1,\dots,\gamma_m\}$ (think of this as the set of clauses of a CNF boolean formula), it builds in polytime a set of clauses $\Pi_\Gamma$ which is irrendundant iff $\Gamma$ is satisfiable (again, $\Gamma$ being satisfiable means the CNF formula $\bigwedge_{j=1}^m \gamma_1$ is). Therefore if you can solve irredundancy you can solve SAT.
[Liberatore'02]: Paolo Liberatore. 2002. The complexity of checking redundancy of CNF propositional formulae. In Proceedings of the 15th European Conference on Artificial Intelligence (ECAI'02). IOS Press, NLD, 262–266.