(I posted this question on MathSE first, no answer, that is the reason why I come here.)
Let $F$ be a 3-CNF formula on $n$ variables. A clause $c$ is implied by the formula if $F$ and $F \wedge c$ are equivalent.
Question : Is it true that each 4-clause implied by $F$ (if there are any) is also the resolvent of two implied 3-clauses ? By extension, is it true that each $k$-clause ($k> 3$) implied by $F$ is also the resolvent of two strictly smaller implied clauses ? (a $k$-clause ($k\leq n$) contains exactly $k$ literals in it).
Thank you for your answers.