We present new structural and algorithmic results on formulas without small subsets of contradicting clauses.