(0) Obligation:
Clauses:
p(X) :- ','(q(X), r(X)).
p(X) :- =(X, 2).
q(X) :- ','(=(X, 1), !).
q(X) :- =(X, 3).
r(X) :- ','(=(X, 1), !).
r(X) :- =(X, 4).
=(X, X).
Query: p(a)
(1) BuiltinConflictTransformerProof (BOTH BOUNDS(ID, ID) transformation)
Renamed defined predicates conflicting with built-in predicates [PROLOG].
(2) Obligation:
Clauses:
p(X) :- ','(q(X), r(X)).
p(X) :- user_defined_=(X, 2).
q(X) :- ','(user_defined_=(X, 1), !).
q(X) :- user_defined_=(X, 3).
r(X) :- ','(user_defined_=(X, 1), !).
r(X) :- user_defined_=(X, 4).
user_defined_=(X, X).
Query: p(a)
(3) NoRecursionProof (EQUIVALENT transformation)
The program does not contain any calls to recursive predicates [PROLOG].
(4) BOUNDS(O(1), O(1))