Not satisfiable 3SAT instance implications
You are describing the Resolution refutation system, which is complete in the sense that if a CNF is unsatisfiable, then it can be proven using Resolution. Resolution is also implicitly used in most SAT solvers.
The width of a Resolution refutation is the maximal number of literals in a clause encountered during the refutation. There are 3CNFs on $n$ variables which require width $\Omega(n)$, for example Tseitin contradictions on 3-regular expanders; see for example Massimo Lauria's lecture notes. This means that every Resolution refutation of these 3CNFs must contain a clause having $\Omega(n)$ literals.