YES # orthogonality Consider the left-linear TRS R: g(a(),y) -> y f(x,a()) -> f(x,g(x,b())) g(h(x),y) -> g(x,h(y)) The left-linear and non-overlapping TRS is confluent