Input TRS: 1: f(g(x,y),f(y,y)) -> f(g(y,x),y) Number of strict rules: 1 Direct Order(PosReal,>,Poly) ... removes: 1 f(x1,x2) weight: (/ 1 4) + x1 + 2 * x2 g(x1,x2) weight: 2 * x1 + 2 * x2 Number of strict rules: 0 YES