YES We show the termination of the TRS R: f(f(a(),f(x,a())),a()) -> f(a(),f(f(x,a()),a())) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: f#(f(a(),f(x,a())),a()) -> f#(a(),f(f(x,a()),a())) p2: f#(f(a(),f(x,a())),a()) -> f#(f(x,a()),a()) and R consists of: r1: f(f(a(),f(x,a())),a()) -> f(a(),f(f(x,a()),a())) The estimated dependency graph contains the following SCCs: {p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: f#(f(a(),f(x,a())),a()) -> f#(f(x,a()),a()) and R consists of: r1: f(f(a(),f(x,a())),a()) -> f(a(),f(f(x,a()),a())) The set of usable rules consists of r1 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: f#_A(x1,x2) = ((1,0),(1,0)) x1 f_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (2,1) a_A() = (0,5) precedence: f# = f = a partial status: pi(f#) = [] pi(f) = [1] pi(a) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: f#_A(x1,x2) = (0,0) f_A(x1,x2) = (1,1) a_A() = (2,2) precedence: a > f# = f partial status: pi(f#) = [] pi(f) = [] pi(a) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.