(not a or not b) implies c <==> not (not a or not b) or c
so negating gives
not [(not a or not b) implies c] <==> not[ not (not a or not b) or c]
which we can simplify somewhat to
not (not (not a or not b)) and not c
(not a or not b) and not c
(not a and not c) or (not b and not c)
not (a or c) or not (b or c)
not ((a or c) and (b or c))
not ((a and b) or c)
