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