YES ---- CR(R) ---- [Jouannaud and Kirchner, 1986] R: +(0(),x) -> x +(+(x,y),z) -> +(x,+(y,z)) +(x,y) -> +(y,x) CP_AC(R): x -> +(0(),x) +(x,y) -> +(0(),y,x) x -> +(x,0()) +(x,y) -> +(y,0(),x) +(x,y) -> +(x,y,0()) +(x,y,z) -> +(x,y,0(),z) +(x,y) -> +(x,0(),y) +(x,y,z) -> +(x,0(),y,z) +(x,y) -> +(0(),x,y) +(x,y,z) -> +(0(),x,y,z) +(x,y) -> +(x,0(),y) +(x,y,z) -> +(x,0(),y,z) +(x,y) -> +(0(),x,y) +(x,y,z) -> +(0(),x,y,z) +(x,y) -> +(x,y,0()) +(x,y,z) -> +(x,y,0(),z) +(x,y) -> +(x,0(),y) +(x,y,z) -> +(x,0(),y,z) +(x,y) -> +(0(),x,y) +(x,y,z) -> +(0(),x,y,z) +(x,y) -> +(x,y,0()) +(x,y,z) -> +(x,y,0(),z) +(x,y) -> +(x,0(),y) +(x,y,z) -> +(x,0(),y,z)