(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. 
Implied Clause and Resolvent
cc.complexity theory;lo.logic;sat;resolution
Here is a counterexample:$$(a \lor y \lor s) \land (\overline{y} \lor b \lor z) \land (\overline{z} \lor c \lor d) \land (\overline{s} \lor b \lor t) \land (\overline{t} \lor c \lor d).$$This formula implies $a \lor b \lor c \lor d$, but only the five listed 3-clauses, no two of which resolve to $a\lor b\lor c\lor d$.