(0) Obligation:
Clauses:
p(X, Y, Z) :- ','(=(X, Y), ','(=(Z, 1), !)).
p(X, Y, Z) :- ','(=(Z, 1), ','(=(Y, X), p(X, Y, Z))).
=(X, X).
Query: p(a,a,a)
(1) BuiltinConflictTransformerProof (EQUIVALENT transformation)
Renamed defined predicates conflicting with built-in predicates [PROLOG].
(2) Obligation:
Clauses:
p(X, Y, Z) :- ','(user_defined_=(X, Y), ','(user_defined_=(Z, 1), !)).
p(X, Y, Z) :- ','(user_defined_=(Z, 1), ','(user_defined_=(Y, X), p(X, Y, Z))).
user_defined_=(X, X).
Query: p(a,a,a)
(3) PrologDeterminacyProcessorProof (EQUIVALENT transformation)
The root node satisfies the determinacy criterion.
(4) YES