MAYBE Trs: {f(f(x, y, a()), z, w) -> f(z, w, f(y, x, z))} Comment: We consider a duplicating trs. FAIL: Open