YES Problem: a() -> g(c()) g(a()) -> b() f(g(X),b()) -> f(a(),X) Proof: DP Processor: DPs: a#() -> g#(c()) f#(g(X),b()) -> a#() f#(g(X),b()) -> f#(a(),X) TRS: a() -> g(c()) g(a()) -> b() f(g(X),b()) -> f(a(),X) TDG Processor: DPs: a#() -> g#(c()) f#(g(X),b()) -> a#() f#(g(X),b()) -> f#(a(),X) TRS: a() -> g(c()) g(a()) -> b() f(g(X),b()) -> f(a(),X) graph: f#(g(X),b()) -> f#(a(),X) -> f#(g(X),b()) -> f#(a(),X) f#(g(X),b()) -> f#(a(),X) -> f#(g(X),b()) -> a#() f#(g(X),b()) -> a#() -> a#() -> g#(c()) SCC Processor: #sccs: 1 #rules: 1 #arcs: 3/9 DPs: f#(g(X),b()) -> f#(a(),X) TRS: a() -> g(c()) g(a()) -> b() f(g(X),b()) -> f(a(),X) CDG Processor: DPs: f#(g(X),b()) -> f#(a(),X) TRS: a() -> g(c()) g(a()) -> b() f(g(X),b()) -> f(a(),X) graph: Qed