I need to prove this is true using resolution.
Every horse can outrun every dog.
Some greyhounds can outrun every rabbit.
Show that every horse can outrun every rabbit.
So my FOL version of this is the following.
$\forall x \forall y (horse(x) \land dog(y) \to outrun (x, y))$
$\exists y (greyhound(y) \land \forall z (rabbit(z) \to outrun (y, z)))$
$\forall y (greyhound(y) \to dog(y))$
$\forall x \forall y \forall z (outrun(x, y) \land outrun(y, z) \to outrun(x, z))$
conclusion:
$\forall x \forall y (horse(x) \land rabbit(y) \to outrun(x, y))$
I negated the conclusion and then converted this to clausal form which looks like this.
$\{\neg horse(x), \neg dog(y), outrun(x, y)\}$
$\{greyhound(a), \neg rabbit(z)\}$
$\{greyhound(a), outrun(a, z)\}$
$\{\neg greyhound(y), dog(y)\}$
$\{\neg outrun(x, y), \neg outrun(y, z), outrun(x, z)\}$
$\{horse(a), rabbit(b), \neg outrun(a, b)\}$
The problem is that the resolution proof is taking awhile and I'm not sure my clausal form is correct. I don't want to waste time with this proof if I'm never going to derive the empty clause. So is my clausal form incorrect or am I doing something wrong with my resolution proof?
I can't comment on whether you are doing anything else wrong, but as you suspect, your causal forms are incorrect and that is not a good start. You've mostly got it, but there were a few mistakes. Keep trying.
Here is what you should use, and it can be resolved to emptiness.
$$\begin{align}1.~&\{\neg horse(x), \neg dog(y), outrun(x, y)\}\\2.~&\{greyhound(a)\}\\3.~&\{\neg rabbit(z), outrun(a,z)\}\\4.~&\{\neg greyhound(y), dog(y)\}\\5.~&\{\neg outrun(x, y), \neg outrun(y, z), outrun(x, z)\}\\6.~&\{horse(c)\}\\7.~&\{rabbit(b)\}\\8.~&\{\neg outrun(c, b)\}\end{align}$$
Here's where you went wrong (and right).
That's okay.
No, clauses are seperated by the conjunction. Witness that there is a greyhound. Also, anything can be outrun by that witness if it is a rabbit.
$\{greyhound(a)\} \\ \{\neg rabbit(z), outrun(a,z)\}$
Good work realising you need to add this analytical consequence. But, it is not the case that everything is a dog if witness $a$ is a greyhound.
The analytical consequence should either be included as a universal clause, $\{\neg greyhound(y), dog(y)\}$, or skip a step to intantiate it to the witness $\{\neg greyhound(a), dog(a)\}$. One or the other must be used; don't be half-hearted about it. And since you left the next as a universal, for consistency you should do so here too.
$\{\neg greyhound(y), dog(y)\}$
Good; again you recognised the need to include transitivity of outrun as an analytical consequence.
That is the correct approach, however, the technique is awry. Now, you have already instantiated witness $a$ (and it is a greyhound), so you cannot use it here. You must use new terms to witness different existentials. Additionally the negation of a conditional is a conjunction, vis: $\exists x \exists y~(horse(x) \land rabbit(y) \land\neg outrun(x, y))$, so that forms three witnessed clauses:
$\{horse(c)\}, \{rabbit(b)\}, \{\neg outrun(c, b)\}$
Overall, a commendable effort, but some practice is needed handling existential instances.
Carry on.