Propositional calculus resolution on pigeonhole principle Here are my premises: 
A v B, C v D, E v F, 
~A v ~C, ~B v ~D, ~A v ~E, ~B v ~F, ~C v ~E, ~D v ~F
Is this even possible? I can't get it down to a unit clause because a new clause is added back in anytime I perform a resolution. 
 A: I prefer to turn these into implications:
$$\begin{array}{ccccc} 
A\vee B& \text{becomes} &\lnot A \implies B&\text{and}& \lnot B \implies A \\
C\vee D& \text{becomes} &\lnot C \implies D&\text{and}& \lnot D \implies C \\
E\vee F& \text{becomes} &\lnot E \implies F&\text{and}& \lnot F \implies E \\
\lnot A\vee \lnot C& \text{becomes} & A \implies \lnot C&\text{and}& C \implies \lnot A \\
\lnot B\vee \lnot D& \text{becomes} & B \implies \lnot D&\text{and}& D \implies \lnot B \\
\lnot A\vee \lnot E& \text{becomes} & A \implies \lnot E&\text{and}& E \implies \lnot A \\
\lnot B\vee \lnot F& \text{becomes} & B \implies \lnot F&\text{and}& F \implies \lnot B \\
\lnot C\vee \lnot E& \text{becomes} & C \implies \lnot E&\text{and}& E \implies \lnot C \\
\lnot D\vee \lnot F& \text{becomes} & D \implies \lnot F&\text{and}& F \implies \lnot D \end{array}$$
Now follow the implications of $A$:
$$A \implies \lnot C \implies D \implies \lnot F \implies E \implies \lnot A$$
and $\lnot A$:
$$\lnot A \implies B \implies \lnot D \implies C \implies \lnot E \implies F \implies \lnot B \implies A$$
Thus $A$ can be neither true nor false.
