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