MAYBE Trs: { cond(true(), x, y) -> s(minus(x, s(y))), cond(false(), x, y) -> 0(), minus(x, y) -> cond(ge(x, s(y)), x, y), ge(0(), s(v)) -> false(), ge(s(u), s(v)) -> ge(u, v), ge(u, 0()) -> true()} Comment: We consider a duplicating trs. FAIL: Open