Input TRS: 1: f(c(X,s(Y))) -> f(c(s(X),Y)) 2: g(c(s(X),Y)) -> f(c(X,s(Y))) Number of strict rules: 2 Direct Order(PosReal,>,Poly) ... removes: 2 s(x1) weight: (/ 1 8) + x1 c(x1,x2) weight: x1 + x2 f(x1) weight: x1 g(x1) weight: (/ 1 8) + x1 Number of strict rules: 1 Direct Order(PosReal,>,Poly) ... removes: 1 s(x1) weight: (/ 1 4) + x1 c(x1,x2) weight: 5853 + x1 + 2 * x2 f(x1) weight: x1 g(x1) weight: (/ 1 2) + x1 Number of strict rules: 0 YES