Knuth defines in  a resolution operator for arbitrary clauses which sets $C = C' \diamond C'' = (C' \lor C'')$ when there is no literal $x$ such that $x \in C'$ and $\neg x \in C''$. I skimmed over ,  and  and could not find any references to this particular style.
Why is this definition sensible for general clauses? How is it different from, say, defining $C = C' \diamond C'' = \top$, a tautology, in such case?
 Knuth, TAOCP, Volume 4 Fascicle 6, Satisfiability
 Buss, Samuel R. (ed.), Handbook of proof theory, Studies in Logic and the Foundations of Mathematics. 137. Amsterdam: Elsevier. 811 p. (1998). ZBL0898.03001.