Input TRS: 1: c(c(c(a(x,y)))) -> b(c(c(c(c(y)))),x) 2: c(c(b(c(y),|0|()))) -> a(|0|(),c(c(a(y,|0|())))) 3: c(c(a(a(y,|0|()),x))) -> c(y) Number of strict rules: 3 Direct Order(PosReal,>,Poly) ... removes: 1 3 2 |0|() weight: 0 a(x1,x2) weight: (/ 9 92) + x1 + 2 * x2 b(x1,x2) weight: (/ 81 368) + x1 + 2 * x2 c(x1) weight: (/ 1 16) + 2 * x1 Number of strict rules: 0 YES