Input TRS: 1: and(tt(),X) -> activate(X) 2: plus(N,0()) -> N 3: plus(N,s(M)) -> s(plus(N,M)) 4: activate(X) -> X Number of strict rules: 4 Direct Order(PosReal,>,Poly) ... removes: 4 1 3 2 s(x1) weight: (/ 1 4) + x1 activate(x1) weight: (/ 1 4) + x1 and(x1,x2) weight: (/ 1 2) + x1 + x2 0() weight: 0 plus(x1,x2) weight: (/ 1 4) + x1 + 2 * x2 tt() weight: 0 Number of strict rules: 0 YES