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() Usable Rule Processor: DPs: g#(b()) -> f#(b()) f#(a()) -> g#(a()) TRS: b() -> a() EDG Processor: DPs: g#(b()) -> f#(b()) f#(a()) -> g#(a()) TRS: b() -> a() graph: g#(b()) -> f#(b()) -> f#(a()) -> g#(a()) Restore Modifier: DPs: g#(b()) -> f#(b()) f#(a()) -> g#(a()) TRS: g(b()) -> f(b()) f(a()) -> g(a()) b() -> a() SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/4