YES
(ignored inputs)COMMENT doi:10.1007/978-3-319-43144-4_18 [110] Example 7
Rewrite Rules:
   [ +(?x,?y) -> +(?y,?x),
     *(+(?x,?y),?z) -> +(*(?x,?z),*(?y,?z)),
     *(+(?y,?x),?z) -> +(*(?x,?z),*(?y,?z)) ]
Apply Direct Methods...
Inner CPs:
   [ *(+(?y,?x),?z_1) = +(*(?x,?z_1),*(?y,?z_1)),
     *(+(?y,?x),?z_2) = +(*(?y,?z_2),*(?x,?z_2)) ]
Outer CPs:
   [ +(*(?x_1,?z_1),*(?y_1,?z_1)) = +(*(?y_1,?z_1),*(?x_1,?z_1)) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Left-Linear, not Right-Linear
Development Closed
Direct Methods: CR

Combined result: CR
504.trs: Success(CR)
(0 msec.)