YES Input TRS: 1: f(f(x,y),f(z,w)) -> f(f(x,z),f(y,w)) 2: f(f(x,y),x) -> x Infeasibility test: f(b(),a()) --> f(a(),b()) Symbol transition graph: f --> # a b f Collapsable symbols: { f }