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