YES Problem: f(f(X,Y),Z) -> f(X,f(Y,Z)) f(X,f(Y,Z)) -> f(Y,Y) Proof: DP Processor: DPs: f#(f(X,Y),Z) -> f#(Y,Z) f#(f(X,Y),Z) -> f#(X,f(Y,Z)) f#(X,f(Y,Z)) -> f#(Y,Y) TRS: f(f(X,Y),Z) -> f(X,f(Y,Z)) f(X,f(Y,Z)) -> f(Y,Y) EDG Processor: DPs: f#(f(X,Y),Z) -> f#(Y,Z) f#(f(X,Y),Z) -> f#(X,f(Y,Z)) f#(X,f(Y,Z)) -> f#(Y,Y) TRS: f(f(X,Y),Z) -> f(X,f(Y,Z)) f(X,f(Y,Z)) -> f(Y,Y) graph: f#(f(X,Y),Z) -> f#(Y,Z) -> f#(X,f(Y,Z)) -> f#(Y,Y) f#(f(X,Y),Z) -> f#(X,f(Y,Z)) -> f#(X,f(Y,Z)) -> f#(Y,Y) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/9