Where is my mistake in this proof? $(A \lor B) \land (A \rightarrow C) \lor (B \rightarrow D) \rightarrow (C \lor D)$ Here is what I finished with, although the problem states that it is a tautology and not a contingency. 
$$For :(A \lor B) \land (A \rightarrow C) \lor (B \rightarrow D) \rightarrow (C \lor D)$$     
$W(A/true)$  $ = (True \lor B) \land (True \rightarrow C) \lor (B \rightarrow D) \rightarrow (C \lor D)$ ---  First condition
 $\equiv  True \land (True \rightarrow C) \lor (B \rightarrow D) \rightarrow (C \lor D)$ ~~~~~~ $True \lor B \equiv True$
 $\equiv  True \land (C) \lor (B \rightarrow D) \rightarrow (C \lor D)$ ~~~~~~  $True \rightarrow C \equiv C$
 $\equiv  C \lor (B \rightarrow D) \rightarrow (C \lor D)$ ~~~~~~  $True \land C \equiv C$   
$X1(D/True) $  $\equiv  C \lor (B \rightarrow True) \rightarrow (C \lor True)$ ~~~~~~  First condition
 $\equiv C \lor (B \rightarrow True) \rightarrow True$ ~~~~~~  $C \lor True \equiv True$
 $\equiv C \lor True \rightarrow True$ ~~~~~~  $B \rightarrow True \equiv True$
 $\equiv True \rightarrow True$ ~~~~~~  $C \lor True \equiv True$
 $\equiv True$ ~~~~~~  $True \rightarrow True \equiv True$  
$X1(D/False) $ $ \equiv  C \lor (B \rightarrow False) \rightarrow (C \lor False)$ ~~~ ~~~  First condition
 $\equiv C \lor B \rightarrow (C \lor False)$~~~~~~$ B \rightarrow False \equiv \neg B$
 $\equiv C \lor B \rightarrow C$~~~~~~$ C \lor False \equiv C$
 $\equiv C \rightarrow C$~~~~~~$ C \lor B \rightarrow C \equiv C \rightarrow C$
 $\equiv True$~~~~~~$ C \rightarrow C \equiv True$   
$W(A/False)$ $= (False \lor B) \land (False \rightarrow C) \lor (B \rightarrow D) \rightarrow (C \lor D)$ ~~~  First condition
 $\equiv  B \land (False \rightarrow C) \lor (B \rightarrow D) \rightarrow (C \lor D)$~~~~~~$ False \lor B \equiv B$
 $\equiv  B \land True \lor (B \rightarrow D) \rightarrow (C \lor D)$~~~~~~$ False \rightarrow C \equiv True$
 $\equiv  B \lor (B \rightarrow D) \rightarrow (C \lor D)$~~~~~~$ B \land True \equiv B$   
$X2(D/True) $ $ = B \lor (B \rightarrow True) \rightarrow (C \lor True)$ ~~~ ~~~  First Condition
 $\equiv B \lor True \rightarrow (C \lor True)$~~~~~~$ B \rightarrow True \equiv True$
 $\equiv (B \lor True) \rightarrow True$~~~~~~$ C \lor True \equiv True$
 $\equiv True \rightarrow True$~~~~~~$ B \lor True \equiv True$
 $\equiv True$  Because $True \rightarrow True \equiv True$     
$X2(D/False) $ $= B \lor (B \rightarrow False) \rightarrow (C \lor False)$ ~~~ ~~~  First Condition
 $\equiv B \lor (\neg B) \rightarrow (C \lor False)$~~~~~~$ B \rightarrow False \equiv \neg B$
 $\equiv True \rightarrow (C \lor False)$~~~~~~$ B \lor (\neg B) \equiv True$
 $\equiv True \rightarrow C$~~~~~~$ C \lor False \equiv C$
 $\equiv C$~~~~~~$ True \rightarrow C \equiv C$
 Contingency!?
It is supposed to come out as a tautology. I'm using Quine's method of substitution.
Edit: cleaned up  
 A: There are 5 ways to unambiguously bracket the expression, as follows:
\begin{array}{cc}
\text{Case 1:} &    (((w \vee x) \wedge (w \rightarrow y)) \vee (x \rightarrow z)) \rightarrow (y \vee z), \\
\text{Case 2:} &    ((w \vee x) \wedge ((w \rightarrow y) \vee (x \rightarrow z))) \rightarrow (y \vee z), \\
\text{Case 3:} &    ((w \vee x) \wedge (w \rightarrow y)) \vee ((x \rightarrow z) \rightarrow (y \vee z)), \\
\text{Case 4:} &    (w \vee x) \wedge (((w \rightarrow y) \vee (x \rightarrow z)) \rightarrow (y \vee z)), \\
\text{Case 5:} &    (w \vee x) \wedge ((w \rightarrow y) \vee ((x \rightarrow z) \rightarrow (y \vee z))). \\
\end{array}
None of these are tautologies.  They are FALSE precisely in the following cases:
        wxyz wxyz wxyz wxyz wxyz wxyz
Case 1: 0000 0100 1000
Case 2: 0100 1000
Case 3: 0000 1000
Case 4: 0000 0001 0010 0011 0100 1000
Case 5: 0000 0001 0010 0011 1000

where 0=FALSE and 1=TRUE.
This is a complete list of counter-examples, and they were found by Mace4 with the following code:
assign(max_models, -1).
assign(domain_size, 2).

formulas(assumptions).

% associativity of "or" and "and"
x v (y v z) = (x v y) v z.
x ^ (y ^ z) = (x ^ y) ^ z.

% commutativity of "or" and "and"
x v y = y v x.
x ^ y = y ^ x.

% distributivity
x ^ (y v z) = (x ^ y) v (x ^ z).
x v (y ^ z) = (x v y) ^ (x v z).

% idempotence
x v x = x.
x ^ x = x.

% absorption
x ^ (x v y) = x.
x v (x ^ y) = x.

% a = false; b = true
x v a = x.
x v b = b.
x ^ b = x.
x ^ a = a.

% negation laws
x ^ (-x) = a.
x v -x = b.
-(-x) = x.

% De Morgan's laws
(-x) ^ (-y) = -(x v y).
(-x) v (-y) = -(x ^ y).

% define * = IMPLIES
x * y = (-x) v y.

end_of_list.

formulas(goals).

(((w v x) ^ (w * y)) v (x * z)) * (y v z) = b.
% ((w v x) ^ ((w * y) v (x * z))) * (y v z) = b.
% ((w v x) ^ (w * y)) v ((x * z) * (y v z)) = b.
% (w v x) ^ (((w * y) v (x * z)) * (y v z)) = b.
% (w v x) ^ ((w * y) v ((x * z) * (y v z))) = b.

end_of_list.

I un-remarked out the case I wished to find a counter-example to, and ran Mace4 five times.
