Proof of simple conditional logic with resolution I have a problem where there are two traffic lights in a junction. If the red light $R_i$ in traffic light $i=1,2$ is on, then green either $R$ or yellow $Y$ is on the other light and vice versa. I think this can be expressed as
$$(R_1 \leftrightarrow (G_2 \lor Y_2)) \land (R_2 \leftrightarrow(G_1 \lor Y_1))$$
Also we need to enforce that two lights cannot be on simultaneously and one light exactly is on at each time,
\begin{align}\neg (G_i \land Y_i)\land \neg(G_i \land R_i) \land \neg (Y_i \land R_i)\land(G_i\lor Y_i \lor R_i)\end{align}
How would one proof with resolution that two red lights cannot be on simultaneously? 
Obviously if $R_i=1$, then either $G_{i^\prime}$ or $Y_{i^\prime}$ is 1 ($i^\prime = 1$ if $i = 2$ and vice versa) because otherwise $R_i \leftrightarrow (G_{i^\prime} \lor Y_{i^\prime}) =0$. Thus because $G_{i^\prime}$ or $Y_{i^\prime}$ is 1, $R_{i^\prime}$ cannot be 1 simultaneously because we would violate the clauses that exactly one light is on (To be more specific either $\neg(G_i \land R_i) \land \neg (Y_i \lor R_i)=0$). It seems clear cut, but I cannot formulate the formal resolution proof. Any help?

We have to write down all the clauses corresponding to the premises, with the negation of the sought conclusion.
If the conclusion is "that two red lights cannot be on simultaneously", we can formalize it as :

$\lnot (R_1 \land R_2)$.

There are four clauses produced from the second premise:
1) $¬G_1 ∨ ¬Y_1$
2) $¬G_1 ∨ ¬ R_1$
3) $¬Y_1 ∨ ¬R_1$
4) $G_1 ∨ Y_1 ∨ R_1$
and the same : 5)-8) for $i=2$.
From the other premise we have : $R_1 \to (G_2 ∨ Y_2)$ i.e. 
9) $¬R_1 ∨ G_2 ∨ Y_2$
and : $¬(G_2 ∨ Y_2) ∨ R_1$ i.e. 
10) $¬G_2 ∨ R_1$
11) $¬Y_2 ∨ R_1$
and the same : 12)-14) for $i=2$.
Finally, we have to add the negation of the conclusion:
15) $R_1$
16) $R_2$.
Finally, we apply the resolution procedure.
