⋀ CLAUSAL ← All solvers
position decides: p(…) is a predicate, f(…) in the brackets a function. A quantifier reaches over one unit; the dot in forall x. widens it
Rules on the selected part