(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