If I had these clauses: {x,y,z},{¬x,¬y,¬z},{x,¬y},{¬x,z}. Why is it not possible to derive the empty clause from these by a resolution proof?
Also, is there a relationship between resolution proof and satisfiability? That is, if I find the clauses are satisfiable, does that cancel out automatically anything about having to use a resolution proof?