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