This question is largely connected to the question presented here.
Let $T$ be the theory extending first order logic with equality, with primitives of a binary symbol $\in$, an unary symbol $S$; and the following axioms:
Axiom of extension: \begin{equation} \forall x \forall y (\forall z (z \in x \leftrightarrow z \in y) \rightarrow x = y) \end{equation}
Axiom of heredity:\begin{equation} \forall x \forall y (S x \land (y \in x \lor y \subset x) \to S y) \end{equation}
Axiom schema of reflection:\begin{equation} S p_1,...,S p_n \to \\ \forall y (\phi y \rightarrow S y) \rightarrow \exists x: S x \land \forall y (y \in x \leftrightarrow \phi y) \end{equation} for every formula $\phi$ not containing $S$ nor $``x"$, whose parameters are among $p_1,..,p_n$ symbols.
Axiom of $\neg S$-separation: \begin{equation} \forall a \exists x \forall y (y \in x \leftrightarrow y \in a \land \neg Sy) \end{equation}
This theory is a proper fragment of Muller's class theory. It can prove axioms of: empty set, pairing, set union, power, separation, and infinity over objects fulfilling $S$. It is stronger than Zermelo since it can prove the existence of $\aleph_{\omega}$ that fulfills $S$, and much higher cardinals!
Question: What's the exact consistency strength of this theory? And in particular can it interpret $ZFC$ the way Ackermann set theory does?
