Are predicate or function symbols with 3+ places actually used in mathematical logic

Question

Let $n$ be a nonnegative integer. The language of first-order logic includes the following symbols :

1. predicate symbols with $n$ places: $P^n_0$, $P^n_1$, $P^n_2$, $\dots$
2. function symbols with $n$ places: $f^n_0$, $f^n_1$, $f^n_2$, $\dots$

What is an example of a formal system which actually uses a predicate or function symbol with 3 or more places? I am asking about a specific symbol, not predicate variables. It seems that, in practice, only unary (1-place) and binary (2-place) symbols are used.

Examples.

1. Axiomatic set theory uses one binary predicate symbol (membership) and no function symbols.

2. Formal number theory uses one binary predicate symbol (equality), one unary function symbol (succession) and two binary function symbols (addition, multiplication).

3. Formal group theory uses one binary predicate symbol (equality), one unary function symbol (inversion), and one binary function symbol (multiplication).

*The last two systems use a constant symbol, which may be regarded as a 0-place function symbol.

Answer 1

Tarskian geometry uses 3-place and 4-place predicates (at least I think they are 3-place relations, not functions, I haven't studied it in detail). Here's an example paper on the topic.