WYCS: possible bug fixes for quantifier instantiation.
WYCS: ok, bug fix for quantification!!!!!