YES We show the termination of the TRS R: -(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -(-(x,y),-(x,y)) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: -#(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -#(-(x,y),-(x,y)) p2: -#(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -#(x,y) and R consists of: r1: -(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -(-(x,y),-(x,y)) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: -#(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -#(-(x,y),-(x,y)) p2: -#(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -#(x,y) and R consists of: r1: -(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -(-(x,y),-(x,y)) The set of usable rules consists of r1 Take the reduction pair: matrix interpretations: carrier: N^3 order: lexicographic order interpretations: -#_A(x1,x2) = ((0,0,0),(0,0,0),(1,0,0)) x2 -_A(x1,x2) = ((0,0,0),(1,0,0),(1,0,0)) x1 + ((1,0,0),(1,1,0),(1,0,1)) x2 + (0,1,0) neg_A(x1) = x1 + (1,1,0) The next rules are strictly ordered: p1, p2 We remove them from the problem. Then no dependency pair remains.