(0) Obligation:

Clauses:

p(X, Y, Z) :- append(.(X, Y), Z, Y).
append([], Y, Y).
append(.(H, Xs), Ys, .(H, Zs)) :- append(Xs, Ys, Zs).

Query: p(a,a,a)

(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)

The root node satisfies the determinacy criterion.

(2) YES