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) TDG 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) graph: g#(a(),x) -> f#(b(),x) -> f#(a(),x) -> f#(b(),x) g#(a(),x) -> f#(b(),x) -> f#(a(),x) -> g#(a(),x) f#(a(),x) -> g#(a(),x) -> g#(a(),x) -> f#(b(),x) f#(a(),x) -> f#(b(),x) -> f#(a(),x) -> f#(b(),x) f#(a(),x) -> f#(b(),x) -> f#(a(),x) -> g#(a(),x) EDG 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) graph: f#(a(),x) -> g#(a(),x) -> g#(a(),x) -> f#(b(),x) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/9