(0) Obligation:

Clauses:

p1(f(X)) :- p1(X).
p2(f(X)) :- p2(X).

Query: p1(g)

(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)

The root node satisfies the determinacy criterion.

(2) YES