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