(0) Obligation:
Clauses:
p(X) :- ','(q(f(Y)), p(Y)).
q(g(Y)).
Query: p(a)
(1) LPReorderTransformerProof (EQUIVALENT transformation)
Reordered facts before rules in definite LP [PROLOG].
(2) Obligation:
Clauses:
q(g(Y)).
p(X) :- ','(q(f(Y)), p(Y)).
Query: p(a)
(3) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:none
Defined Pair Symbols:none
Compound Symbols:none
(5) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(6) BOUNDS(O(1), O(1))
(7) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:none
Defined Pair Symbols:none
Compound Symbols:none