F ::= EXISTS EXISTS ::= exists var FORALL | FORALL FORALL ::= forall var IMP | IMP IMP ::= OR imp OR OR ::= AND (or AND)* AND ::= NOT (and NOT)* NOT ::= not? PRED PRED ::= pred opar TERM (comma TERM)* cpar TERM ::= | var | const | var opar TERM (comma TERM)* cpar