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

_ :: Bool
_ :: Int
_ :: [Int]
[] :: [Int]
(:) :: Int -> [Int] -> [Int]
insert :: Int -> [Int] -> [Int]
sort :: [Int] -> [Int]
(<=) :: Int -> Int -> Bool
(<) :: Int -> Int -> Bool
True :: Bool
False :: Bool
(==) :: Bool -> Bool -> Bool
(==) :: Int -> Int -> Bool
(==) :: [Int] -> [Int] -> Bool

   (sort xs == []) == (xs == [])
           sort [] == []
    sort (sort xs) == sort xs
       insert x [] == [x]
sort (insert x xs) == insert x (sort xs)
       sort (x:xs) == insert x (sort xs)