Input TRS: 1: f(s(s(s(s(s(s(s(s(x)))))))),y,y) -> f(id(s(s(s(s(s(s(s(s(x))))))))),y,y) 2: id(s(x)) -> s(id(x)) 3: id(0()) -> 0() Number of Rules: 3 Direct QWPOS(mSum) ... failed.