> 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$][1] model of $\sf NFU$. But, is this the case with $\sf NF$? 

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


  [1]: https://randall-holmes.github.io/Papers/nfumcorrected.pdf
  [2]: https://mathoverflow.net/q/353428/95347