--pre-skolem-quant=on --enum-inst
