Clarification on "clause learning" in DPLL algorithm

I am struggling to understand the idea of conflict-driven clause learning, in particular, I can not understand why the clause we 'learned' is a substantially new (i.e. the clause database does not already contain it, neither any subset of it). Here is what Knuth in his book says:

A conflict clause $c$ on decision level $d$ has the form $\overline{l} \lor \overline{a}_1 \lor ··· \lor \overline{a}_k$, where $l$ and all the $a$’s belong to the trail; furthermore $l$ and at least one $a_i$ belong to level $d$. We can assume that $l$ is rightmost in the trail, of all the literals in $c$. Hence $l$ cannot be the $d$th decision; and it has a reason, say $l \lor \overline{a}′_1 \lor ··· \lor \overline{a}′_k$. Resolving $c$ with this reason gives the clause $c′ = \overline{a}_1 \lor ··· \lor \overline{a}_k \lor \overline{a}′_1 \lor ··· \lor \overline{a}′_k$, which includes at least one literal belonging to level $d$. If more than one such literal is present, then $c′$ is itself a conflict clause; we can set $c \leftarrow c′$ and repeat the process. Eventually we are bound to obtain a new clause $c′$ of the form $\overline{l}′ \lor \overline{b}_1 \lor ··· \lor \overline{b}_r$, where $l′$ is on level $d$ and where $b_1$ through $b_r$ are on lower levels.

Such a $c′$ is learnable, as desired, because it can’t contain any existing clauses. (Every subclause of $c′$, including $c′$ itself, would otherwise have given us something to force at a lower level.)

I can understand why the clause database has no subset of $c'$ that contains $\overline{l'}$ (because $\overline{l'}$ would have been forced (i.e. unit-propagated) at level lower than $d$), but what contradicts to the existence of clause, let's say, $\overline{b_1}\lor\overline{b_2}$?

All the literals in a conflict clause are set false by definition, else there would be no conflict. So if the clause $\overline{b_1}\lor\overline{b_2}$ existed, one of those false literals would have caused that clause to go unit before we reached the current level, which in turn would have forced one of the $\overline{b_1}$ or $\overline{b_2}$ literals true. But we already know that those literals must be false, so we have a contradiction. This contradiction shows that the clause $\overline{b_1}\lor\overline{b_2}$ cannot exist. The reasoning is the same for all clauses that are subsets of the conflict clause.

StackExchange Computer Science Q#121090, answer score: 3