Input TRS: 1: d(x) -> e(u(x)) 2: d(u(x)) -> c(x) 3: c(u(x)) -> b(x) 4: v(e(x)) -> x 5: b(u(x)) -> a(e(x)) Number of strict rules: 5 Direct Order(PosReal,>,Poly) ... removes: 4 1 3 5 2 a(x1) weight: x1 d(x1) weight: (/ 3 4) + 2 * x1 v(x1) weight: 2 * x1 b(x1) weight: (/ 1 4) + x1 u(x1) weight: (/ 1 4) + 2 * x1 c(x1) weight: 2 * x1 e(x1) weight: (/ 1 4) + x1 Number of strict rules: 0 YES