# Is formula satisfiable using resolution

When I use the resolution "tree" to determine whether formula is satisfiable, it gives me wrong result:

Can you find my mistake and explain how is it done right?

Grant

-
You can resolve something of the form $(X\lor Y)\land (\lnot X \lor Z)$ to $(Y\lor Z)$.
You did the first resolution correctly, resolving $(\lnot A \lor B) \land (\lnot B \lor C)$ to $(\lnot A \lor C)$. But you skipped a step in the second resolution. You should have resolved $(\lnot A\lor C) \land (\lnot C\lor A)$ to $(C \lor \lnot C)$, which is $\top$, but instead you resolved it to $\bot$.
You can, but the result of crossing them all out is $\top$, not $\bot$, because you are crossing them out from a conjunction, and an empty conjunction is true, not false. –  MJD Dec 30 '12 at 18:34