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