MAYBE MAYBE TRS: { +(+(x, y), z) -> +(x, +(y, z)), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(+(y, z), x) -> +(*(x, y), *(x, z)), *(*(x, y), z) -> *(x, *(y, z)) } DUP: We consider a duplicating system. Trs: { +(+(x, y), z) -> +(x, +(y, z)), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(+(y, z), x) -> +(*(x, y), *(x, z)), *(*(x, y), z) -> *(x, *(y, z)) } Fail