Input TRS: 1: a__f(X,X) -> a__f(a(),b()) 2: a__b() -> a() 3: mark(f(X1,X2)) -> a__f(mark(X1),X2) 4: mark(b()) -> a__b() 5: mark(a()) -> a() 6: a__f(X1,X2) -> f(X1,X2) 7: a__b() -> b() Number of Rules: 7 Direct QWPOS(Sum) ... failed.