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()) Usable Rule Processor: DPs: g#(a()) -> b#() g#(a()) -> g#(b()) b#() -> f#(a(),a()) f#(a(),a()) -> g#(d()) TRS: b() -> f(a(),a()) f(a(),a()) -> g(d()) CDG Processor: DPs: g#(a()) -> b#() g#(a()) -> g#(b()) b#() -> f#(a(),a()) f#(a(),a()) -> g#(d()) TRS: 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()) Restore Modifier: 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()) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/16