WyCS: working on a likely bug in the Inequality closure rule.
WyCS: fixed critical bug in handling of inequality closure.
The problem was that the inequality closure rule was not properly handling the four cases for multiplication by negative values.  The rule was just wrong, and it needed three additional cases as well.