max expr size  =    5
  |- on ineqs  =    4
  |- on conds  =    4
max  #-tests   =  500
min  #-tests   =   25  (to consider p ==> q true)
max  #-vars    =    2  (for inequational and conditional laws)

_ :: Bool
False :: Bool
True :: Bool
not :: Bool -> Bool
(&&) :: Bool -> Bool -> Bool
(||) :: Bool -> Bool -> Bool
(==) :: Bool -> Bool -> Bool

       (p && p) == p
       (p || p) == p
    not (not p) == p
    (p && True) == p
   (p || False) == p
       (p == p) == True
    (p == True) == p
   (p && False) == False
    (p || True) == True
   (p && not p) == False
   (p == False) == not p
       (p && q) == (q && p)
       (p || q) == (q || p)
(p && (p || q)) == p
  (p || p && q) == p
  (p && p == q) == (p && q)
   (p == not q) == not (p == q)
   not (p || q) == (not p && not q)
   (p || not q) == not (q && not p)
((p && q) && r) == (p && (q && r))
((p || q) || r) == (p || (q || r))
(p == (p && q)) == not (p && not q)
  (p || p == q) == not (q && not p)
(p == (p || q)) == not (q && not p)

           p ==> True
       False ==> p
           p ==> p || q
      p && q ==> p
      p && q ==> p == q
       not p ==> not (p && q)
not (p || q) ==> p == q
not (p == q) ==> p || q
  p && not q ==> q || p
      p == q ==> p || not q
  p && not q ==> not (q && p)
not (p == q) ==> not (p && q)
  p && not q ==> not (p == q)