Footnote:The order of list elements in ?refs is used to represent quantifier scope. Go back to paper