YES ---- CR(R) ---- R : left-linear, C : CR and CP-closing, and Cdup/R : SN R: a(x) -> x a(a(x)) -> b(c(x)) b(x) -> x c(x) -> x c(b(x)) -> b(a(c(x))) CP(R): a(___y4) -> b(c(___y4)) a(___y3) -> b(c(___y3)) b(c(___y11)) -> a(___y11) a(b(c(___y13))) -> b(c(a(___y13))) c(___y29) -> b(a(c(___y29))) b(___y40) -> b(a(c(___y40))) b(a(c(___y47))) -> b(___y47) critical-pair-closing system C: a(x) -> x b(x) -> x c(x) -> x CR(C): see below. ---- CR(R) ---- R : linear and strongly closed [Huet, 1980] R: a(x) -> x b(x) -> x c(x) -> x CP(R):