The clauses of our problem: {x,y},{x,z},{y,z},{¬x,¬y},{¬x,¬z},{¬y,¬z}
How can we conclude from these clauses to {}?
I can see that this cannot be satisfied, but I am unable to find a solution in the Resolution Proof System as it seems that [{x,y},{{¬x,¬y}] results in {x,y,¬y} or {y,x,¬x} and then we can derive {x,¬x} and {y,¬y}. It seems that this is obvious as (T or F) will be always T.
I know that this is not satisfiable because there is no solution that satisfies the problem.
You can apply Davis-Putnam. This applies resolution in an exhaustive fashion that eliminates propositional variables one at a time. It is a complete method that is able to deduce {} iff a propositional CNF formula is unsatisfiable.
Here is a good introduction https://www.fi.muni.cz/~popel/lectures/complog/slides/davis-putnam.pdf . To produce the proof one just needs to track the resolutions it does that contribute to the final derivation.
For this problem if you apply it in the order x, y, z one gets the proof:
1. {x,y} . input
2. {x,z} . input
3. {y,z} . input
4. {~x,~y} . input
5. {~x,~z} . input
6. {~y,~z} . input
7. {y,~z} . resolve(x, 1, 5)
8. {~y,z} . resolve(x, 2, 4)
9. {~z} . resolve(y, 7, 6)
10. {z} . resolve(y, 3, 8)
11. {} . resolve(z, 10, 9)