Today I played with SmallCheck. Interested in what happened when I tried to find a small unsatisfiable boolean formula that is not easily detected as such? Watch my attempts! (strip `.html`

suffix for executable Haskell file)

## Update

After realising that the crucial step to enable SmallCheck to find the formula was *not* the limitation to conjunctive normal form but the limitation to only two variables, I tried what happens when incorporating this limitation in the original `Serial`

instance for `Boolean`

s:

instance Serial Boolean where series = const [Var 0, Var 1] \/ cons0 Yes \/ cons0 No \/ cons1 Not \/ cons2 (:&&:) \/ cons2 (:||:)

Using this instance, SmallCheck finds a counter example at depth three in about 30 seconds:

Depth 3: Failed test no. 10682586. Test values follow. (Var 0 :&&: Not (Var 0)) :||: (Var 1 :&&: Not (Var 1))

This is a condensed version of the formula found before (which is the CNF of this one). Seems like by generating only CNFs I was barking up the wrong tree!