WyCS: updated quantifier instantiation in the presence of quantifiers with multiple variables.