YES Problem: f(a()) -> f(b()) g(b()) -> g(a()) f(x) -> g(x) Proof: DP Processor: DPs: f#(a()) -> f#(b()) g#(b()) -> g#(a()) f#(x) -> g#(x) TRS: f(a()) -> f(b()) g(b()) -> g(a()) f(x) -> g(x) TDG Processor: DPs: f#(a()) -> f#(b()) g#(b()) -> g#(a()) f#(x) -> g#(x) TRS: f(a()) -> f(b()) g(b()) -> g(a()) f(x) -> g(x) graph: g#(b()) -> g#(a()) -> g#(b()) -> g#(a()) f#(a()) -> f#(b()) -> f#(x) -> g#(x) f#(a()) -> f#(b()) -> f#(a()) -> f#(b()) f#(x) -> g#(x) -> g#(b()) -> g#(a()) EDG Processor: DPs: f#(a()) -> f#(b()) g#(b()) -> g#(a()) f#(x) -> g#(x) TRS: f(a()) -> f(b()) g(b()) -> g(a()) f(x) -> g(x) graph: f#(a()) -> f#(b()) -> f#(x) -> g#(x) f#(x) -> g#(x) -> g#(b()) -> g#(a()) CDG Processor: DPs: f#(a()) -> f#(b()) g#(b()) -> g#(a()) f#(x) -> g#(x) TRS: f(a()) -> f(b()) g(b()) -> g(a()) f(x) -> g(x) graph: f#(a()) -> f#(b()) -> f#(x) -> g#(x) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/9