YES Problem: f(x,y) -> g1(x,x,y) f(x,y) -> g1(y,x,x) f(x,y) -> g2(x,y,y) f(x,y) -> g2(y,y,x) g1(x,x,y) -> h(x,y) g1(y,x,x) -> h(x,y) g2(x,y,y) -> h(x,y) g2(y,y,x) -> h(x,y) h(x,x) -> x Proof: DP Processor: DPs: f#(x,y) -> g1#(x,x,y) f#(x,y) -> g1#(y,x,x) f#(x,y) -> g2#(x,y,y) f#(x,y) -> g2#(y,y,x) g1#(x,x,y) -> h#(x,y) g1#(y,x,x) -> h#(x,y) g2#(x,y,y) -> h#(x,y) g2#(y,y,x) -> h#(x,y) TRS: f(x,y) -> g1(x,x,y) f(x,y) -> g1(y,x,x) f(x,y) -> g2(x,y,y) f(x,y) -> g2(y,y,x) g1(x,x,y) -> h(x,y) g1(y,x,x) -> h(x,y) g2(x,y,y) -> h(x,y) g2(y,y,x) -> h(x,y) h(x,x) -> x TDG Processor: DPs: f#(x,y) -> g1#(x,x,y) f#(x,y) -> g1#(y,x,x) f#(x,y) -> g2#(x,y,y) f#(x,y) -> g2#(y,y,x) g1#(x,x,y) -> h#(x,y) g1#(y,x,x) -> h#(x,y) g2#(x,y,y) -> h#(x,y) g2#(y,y,x) -> h#(x,y) TRS: f(x,y) -> g1(x,x,y) f(x,y) -> g1(y,x,x) f(x,y) -> g2(x,y,y) f(x,y) -> g2(y,y,x) g1(x,x,y) -> h(x,y) g1(y,x,x) -> h(x,y) g2(x,y,y) -> h(x,y) g2(y,y,x) -> h(x,y) h(x,x) -> x graph: f#(x,y) -> g2#(y,y,x) -> g2#(y,y,x) -> h#(x,y) f#(x,y) -> g2#(y,y,x) -> g2#(x,y,y) -> h#(x,y) f#(x,y) -> g2#(x,y,y) -> g2#(y,y,x) -> h#(x,y) f#(x,y) -> g2#(x,y,y) -> g2#(x,y,y) -> h#(x,y) f#(x,y) -> g1#(y,x,x) -> g1#(y,x,x) -> h#(x,y) f#(x,y) -> g1#(y,x,x) -> g1#(x,x,y) -> h#(x,y) f#(x,y) -> g1#(x,x,y) -> g1#(y,x,x) -> h#(x,y) f#(x,y) -> g1#(x,x,y) -> g1#(x,x,y) -> h#(x,y) SCC Processor: #sccs: 0 #rules: 0 #arcs: 8/64