Parser now supports implication, equivalence; also in KB.

So far KB formulas had to be quasiprimitive clauses.
Now they can be arbitrary formulas provided their NF is a clause with
universally quantified variables, that is, a clause with a prefix
over the set {~, Ex x | x is variable}*, where there is an odd number of
'~' to the left of every 'Ex x' and an odd number of '~' to its right.