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