--decision=internal --simplification=none --no-inst-no-entail --no-cbqi --enum-inst
