|
|
$$\begin{array}{rlrl}
1&{_{\:\!\mathbf|}}~(W\lor X)\lor (Y\lor Z)\\[-5pt]
2&\big|~X\to Y\\[-5pt]
3&\big|\!\underline{\,~\neg Z~}\\[-5pt]
4&\big|~{_{\:\!\mathbf|}}\!\underline{\,~W\lor X~}\\[-5pt]
5&\big|~\big|~{_{\:\!\mathbf|}}\!\underline{\,~W~}\\[-5pt]
6&\big|~\big|~\big|~W\lor Y&\rm{{\lor}I}&\rm{5}\\[-5pt]
7&\big|~\big|~{_{\:\!\mathbf|}}\!\underline{\,~X~}\\[-5pt]
8&\big|~\big|~\big|~Y&\rm{{\to}E}&\rm{2,7}\\[-5pt]
9&\big|~\big|~\big|~W\lor Y&\rm{{\lor}I}&\rm{8}\\[-5pt]
10&\big|~\big|~W\lor Y&\rm{{\lor}E}&\rm{4,5{-}6,7{-}9}\\[-5pt]
11&\big|~{_{\:\!\mathbf|}}\!\underline{\,~Y\lor Z~}\\[-5pt]
12&\big|~\big|~{_{\:\!\mathbf|}}\!\underline{\,~Y~}\\[-5pt]
13&\big|~\big|~\big|~W\lor Y&\rm{{\lor}I}&\rm{12}\\[-5pt]
14&\big|~\big|~{_{\:\!\mathbf|}}\!\underline{\,~Z~}\\[-5pt]
15&\big|~\big|~\big|~\bot&\rm{{\neg}E}&\rm{3,14}\\[-5pt]
16&\big|~\big|~\big|~\forall x\exists yPxy&\rm{X}&\rm{15}\\[-5pt]
17&\big|~\big|~\big|~A\leftrightarrow (B\to C)&\rm{X}&\rm{15}\\[-5pt]
18&\big|~\big|~\big|~W\lor Y&\rm{X}&\rm{15}\\[-5pt]
19&\big|~\big|~W\lor Y&\rm{{\lor}E}&\rm{11,12{-}13,14{-}18}\\[-5pt]
20&\big|~W\lor Y&\rm{{\lor}E}&\rm{1,4{-}10,11{-}19}\\[-5pt]
\end{array}$$
|
|
|