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