Can this set of propositions be represented and proved in Haskell?

Question

I used a set of natural language statements and their formalization from Gries and Schneider. I attempted to transform the propositions into Haskell equations. For example, for S0 : $a \land w \Rightarrow p$ the conjunction was split giving $a \Rightarrow p$ and $w \Rightarrow p$ and then the contrapositive rule was applied giving $\neg p \Rightarrow \neg a$ and $\neg p \Rightarrow \neg w$. I then translated those propositions into Haskell conditional equations.

Is the Haskell representation a reasonable transformation? Is there a relation between the execution of the Haskell expression not e a proof of theorem $\neg e$?

Natural language

If Superman were able and willing to prevent evil, he would do so. If Superman were unable to prevent evil, he would be ineffective; if he were unwilling to prevent evil, he would be malevolent. Superman does not prevent evil. If Superman exists, he is neither ineffective nor malevolent. Therefore Superman does not exist.

Formalize

$a$: Superman is able to prevent evil.

$w$: Superman is willing to prevent evil.

$i$: Superman is ineffective.

$m$: Superman is malevolent.

$p$: Superman prevents evil.

$e$: Superman exists.

S0 : $a \land w \Rightarrow p$

S1 : $(\neg a \Rightarrow i) \land (\neg w \Rightarrow \neg m)$

S2 : $\neg p$

S3 : $e \Rightarrow \neg i \land \neg m$

module SUPERMAN where
 a::Bool
 w::Bool
 i::Bool
 p::Bool
 e::Bool

 a | (not p) = False  -- S0a
 w | (not p)  = False -- S0b
 i | (not a) = True   -- S1a
 m | (not w) = True   -- S1b
 p = False            -- S2
 e | (i || m) = False -- S3
-- Theorems (not e), (i || m), and (i && a) all hold