Resolution Algorithm - No new clauses
When $new\subseteq clauses$ then, if we continued, the next line would be $clauses \leftarrow clauses\cup new$ but $clauses\cup new = clauses$ so we'd be doing the exact same calculation the next time through the loop deducing nothing new and looping forever.

The point is, if we "resolve" all pairs of clauses and deduce nothing new, then we've derived all the consequences from the original set of clauses. If we still haven't derived a contradiction at that point, then $\neg\alpha$ is consistent with $KB$ and thus $\alpha$ is not provable. This last isn't necessarily completely accurate either, as it only shows that $\alpha$ is not a propositional consequence of $KB$. For example, if $KB$ was $\forall x.P(x)$ and $\alpha$ was $P(t)$, then $\alpha$ is provable from $KB$ but not via propositional reasoning.