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
id :: Int -> Int
(+) :: Int -> Int -> Int
f :: Int -> Int -> Int
g :: Int -> Int -> Int
h :: Int -> Int -> Int

       id x == x
      x + 0 == x
      g x y == g z x'
      f x y == f x z
      h x y == h z y
      x + y == y + x
(x + y) + z == x + (y + z)

x <= g y y
x <= f 0 y
x <= h y 0