YES Problem: f(a(),x) -> g(a(),x) g(a(),x) -> f(b(),x) f(a(),x) -> f(b(),x) Proof: DP Processor: DPs: f#(a(),x) -> g#(a(),x) g#(a(),x) -> f#(b(),x) f#(a(),x) -> f#(b(),x) TRS: f(a(),x) -> g(a(),x) g(a(),x) -> f(b(),x) f(a(),x) -> f(b(),x) Usable Rule Processor: DPs: f#(a(),x) -> g#(a(),x) g#(a(),x) -> f#(b(),x) f#(a(),x) -> f#(b(),x) TRS: ADG Processor: DPs: f#(a(),x) -> g#(a(),x) g#(a(),x) -> f#(b(),x) f#(a(),x) -> f#(b(),x) TRS: graph: f#(a(),x) -> g#(a(),x) -> g#(a(),x) -> f#(b(),x) Restore Modifier: DPs: f#(a(),x) -> g#(a(),x) g#(a(),x) -> f#(b(),x) f#(a(),x) -> f#(b(),x) TRS: f(a(),x) -> g(a(),x) g(a(),x) -> f(b(),x) f(a(),x) -> f(b(),x) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/9