Proceeding from constructor terms to atomic formulas,
we come to the LISP-inspired PROLOG extension of
*varying-arity relation applications*
i.e., clause heads and bodies directly containing a ```|`''.
Thus, both structures and applications can be ended by a vertical bar followed by an ordinary variable; equivalently, they could
be ended by a ``sequence variable'' as used in
KIF [GF91].
Varying-arity applications give
argument sequences the
flavor of an implicit list data structure. For instance, the
N-ary version (N 0) of the `sorted` relation

permits calls likesorted(). sorted(X). sorted(X,Y|Z) :- lesseq(X,Y), sorted(Y|Z).

As in LISP, the N-ary flexibility gained can be used,
among other things, to flatten
nestings of binary associative operators like `+` and `append`.
Their output cannot go to the (usual) last argument position
because of the asymmetry of ```|`''-list-splicing;
the only uniformly usable output argument is the first one.

For example, while ordinary PROLOGs' ternary `append` relation
is already quite flexible, LM-PROLOG [CK85] defines a natural
N-ary extension (N > 0), which in RELFUN is rewritten as

It `contains' LISP's unaryappend([]). append(Total,[]|Back) :- append(Total|Back). append([First|Total],[First|Front]|Back) :- append(Total,Front|Back).

Of course, a simple transformer can put the varying number of arguments of such relations into a single list.
For `sorted` the additional brackets would
lead back to the original definition; for `append`, with
its distinguished first argument, however, they would
become a syntactic burden.
Also, the transformation
can result in serious problems for even the standard
WAM-indexing scheme because the first
(and only) relation argument becomes of type `list` indiscriminately.
This could be
remedied by a version of the semi-listifying arity-fixing technique
sketched for structures in subsection 2.3
(e.g., listifying only the N-1 input lists
of `append`).