YES # strong closedness (Huet 1980) Consider the left-linear TRS R: F(c(x)) -> G(x) G(x) -> F(x) c(x) -> x R is linear and every critical pair is strongly closed