TRS: { or(true(), y) -> true(), or(x, true()) -> true(), or(false(), false()) -> false(), mem(x, nil()) -> false(), mem(x, set(y)) -> =(x, y), mem(x, union(y, z)) -> or(mem(x, y), mem(x, z))} MPO: Prec: mem > or, mem > false, mem > = empty Strict: {} Weak: {} Qed