You can express an arbitrary first-order formula in an .mln file. The syntax for logical connectives is as follows: ! (not), ^ (and), v (or), => (implies), <=> (if and only if), FORALL/forall/Forall (universal quantification), and EXIST/exist/Exist (existential quantification). Operator precedence is as follows: not and or implies if and only if forall = exists. Operators with the same precedence are evaluated left to right. You can use parentheses to enforce a different precedence, or to make precedence explicit (e.g., (A=>B)=>C as opposed to A=>(B=>C)). Universal quantifiers at the outermost level can be omitted, i.e., free variables are interpreted as universally quantified at the outermost level. Quantifiers can be applied to more than one variable at once (e.g., forall x,y). The infix equality sign (e.g., x = y) can be used as a shorthand for the equality predicate (e.g., equals(x,y)).