A first-order structure and an assignment determine the value of every term recursively: a variable has its assigned value, a constant has its interpreted value, and a compound function term is evaluated by applying the interpreted function to the recursively evaluated arguments. This operation supplies the input values for the satisfaction clauses of atomic formulas.
New to topics? Read the docs here!