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)

_ :: Int
0 :: Int
1 :: Int
(+) :: Int -> Int -> Int
(*) :: Int -> Int -> Int

      x + 0 == x
      x * 1 == x
      x * 0 == 0
      x + y == y + x
      x * y == y * x
(x + y) + z == x + (y + z)
(x * y) * z == x * (y * z)
(x + x) * y == x * (y + y)
x * (y + 1) == x + x * y

x <= x * x
x <= x + 1
0 <= x * x