WYCS: working on the quantifier instantiation rule.