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