Input TRS: 1: f(a(),b()) -> f(a(),c()) 2: f(c(),d()) -> f(b(),d()) Number of Rules: 2 Direct QWPOS(mSum) ... failed.