* minor doc fixes
* Added optmization level to KIF
* if o_level > 0 then 'distinct' and 'not' premisses are reordered accordingly
* minor doc fixes