Is this theory consistent?

Language: first order language of set theory,

Extra-logical axioms:

1. Extensionality: as in $\sf NF$.

2. Stratified Comprehension: as in $\sf NF$.

Define: a set is said to be well founded if it is not an element of a descending membership set. Formally:

$$\operatorname {well-founded}(s) \iff \neg \exists x: s \in x \land \forall y \in x \exists z: z \in y \cap x $$

3. Replacement: if $A$ is a well founded set, and $\phi(x,y)$ is a formula standing for a many-to-one relation from well founded sets to well founded sets, that doesn't mention "$B$", then there is a set $B=\{y \mid \exists x \in A : \phi(x,y)\}$.

4. Infinity: There is a well-founded set having the empty set among its elements, that is closed under singletons.

5. Choice: For every nonempty set of pairwise disjoint well-founded nonempty sets, there is a set that has singleton intersections with each of its elements.

So, this theory has a universe obeying the rules of $\sf NF $, and has its well founded realm obeying the rules of $\sf ZFC$.

It is known that there is a consistent similar theory that extends $\sf NFU$. A corollary of Randall Holmes theory that speaks about the $\sf BEST$ model of $\sf NFU$. But, is this the case with $\sf NF$?

I've asked a similar question before but in terms of $\sf ML$, this question is in terms of $\sf NF$.