The operative phrase is "at least 8"! The funny thing about 3SAT is that every clause with 3 distinct variables eliminates a full 1/8th of the model space. So how is it that you can have a formula with hundreds of clauses in it and not completely obliterate all of the possible solutions? The answer, of course, is that most of the clauses overlap in the portions of the model space that they exclude; and the more variables you have, the more "volume" each clause overlaps in the model space. The scenario where 8 clauses is sufficient to make a formula unsatisfiable is obviously where those 8 "blocks" have no overlap.
Geometrically speaking, one can view the model space for a formula as an $n$-dimensional hypercube of width $2$, where each dimension corresponds to a variable in the formula, and can have the value $true$ or $false$. Since it's hard to visualize hypercubes with more than 3 dimensions, it's helpful to project them down onto 2 dimensions like so:
Here I've rendered the formula provided by @rus9384 as a table showing how the model space is covered. The "canonical" unsatisfiable core with only 3 variables would replace the last 2 clauses with $(\lnot x, \lnot y, z)$ and $(\lnot x, \lnot y, \lnot z)$. In this case, all the "blocks" would be "aligned". If you could see this properly in 4 dimensions, it would look like we are building a 4-dimensional LEGO cube by stacking a bunch of 1x2 bricks in the same direction. What <PERSON> has done is take 2 of the "bricks" (which logically form a 2x2 block) and "rotated" them 90 degrees. Of course, this still covers the model space exactly.
Now, to see why an unsatisfiable core might contain more than 8 clauses, we should first think about what a 2-clause looks like. 399
Suppose our formula contained $(x, y)$. This is actually the resolution of 1 and 2, so in a way, you could say that it does contain this 2-clause. And note that 1 and 2 together cover 1/4th of the space. In general, a clause with $k$ distinct variables covers $\frac{1}{2^k}$th of the model space (assuming no tautologies, of course). Thus, to force more than 8 clauses in the Minimal Unsatisfiable Core (MUC), we need to cover less than 1/8th of the model space with one or more of the clauses! Using the formula above, we can do that by introducing a clause with 4 variables, which only excludes 1/16th of the space (e.g., $(x, y, z, t)$ only takes up 1 cell in the table).
"But wait!" you say: "...we were talking about 3SAT! You can't have 4-clauses!" @Max showed that you can run Resolution forwards and backwards to get the desired clauses. So, for instance, we can introduce a new variable, $w$, and add $(\lnot x, \lnot y, \lnot w)$ and $(w, \lnot z, \lnot t)$, which resolve to the 4-clause $(\lnot x, \lnot y, \lnot z, \lnot t)$. If we replaced clause 8 in our formula with this new 4-clause (or its 3-clause "parents"), then suddenly our formula becomes satisfiable, because we have left a "hole" in the model! We would need at least one more formula to patch it up. As you can imagine, one can force a MUC to be larger than any fixed size ($\geq 8$) simply by building it with "blocks" that are arbitrarily small.
"But wait!" you say: "...you already said that all 3-clauses cover 1/8th of the model space! They are all the same size!!!" And indeed that is true. What's really going on is that we are shifting the overlap into other variables/dimensions so that the intersection with the "MUC core", if you will, is less than 1/8th, if that makes sense. 399