What is the proof-theoretic ordinal of bare $\mathsf{NFU}$? On the Stanford Encyclopedia of Philosophy article on alternative axiomatic set theories, it is stated without reference that bare $\mathsf{NFU}$ (i.e., $\mathsf{NFU}$ without the axiom of infinity) is weaker in consistency strength than $\mathsf{PA}$. In this Math SE answer, Randall Holmes states that $\mathsf{NFU}$ interprets Robinson arithmetic and furthermore says that it probably interprets bounded arithmetic with exponentiation (which I think means $\mathsf{I}\Delta_0 + \mathrm{exp}$, although I'm not completely familiar with the semi-formal terminology people use for these things).
This would put $\mathsf{NFU}$ right in the range of theories for which ordinal analysis should be well-behaved (i.e., those which are at least as strong as $\mathsf{I}\Delta_0$) but also should be feasible to actually do (e.g., those which are as strong as or not too much stronger than $\mathsf{PA}$). So this raises a question that I have been unable to find any discussion of.

Question 1. What is the proof-theoretic ordinal of bare $\mathsf{NFU}$?

More generally, a lot is known about consistency strength and interpretation of theories of first- and second-order arithmetic between $\mathsf{I}\Delta_0$ and $\mathsf{PA}$. Proof-theoretic ordinals are supposed to be a rough measure of consistency strength, but in principle this is a more fine grained issue.

Question 2. Where does bare $\mathsf{NFU}$ sit relative to well-known theories of arithmetic in terms of interpretation and consistency strength?

 A: As in the question, I will use $\mathsf{NFU}$ for "bare" $\mathsf{NFU}$, i.e., the result of weakening the extensionality axiom in Quine's $\mathsf{NF}$ so as to allow urelements. Let $\mathsf{NFU}^{-\infty}$ be $\mathsf{NFU} \cup \{\lnot \mathsf{Infinity} \}$, where $\mathsf{Infinity}$ is the axiom of infinity.
In 2002, Solovay proved the following results. The proofs were disseminated among some NFU enthusiasts, but alas, they remain unpublished. In what follows $\mathsf{Exp}$ is the statement asserting the totality of the exponential function, and $\mathsf{SupExp}$ is the statement asserting the totality of the superexponential function (also known as tetration), i.e.,  the "stack of twos"
function, $f(n)$, where $f(0) = 1$ and $f(n+1) = 2^{f(n)}$.
Theorem.
(1) $\mathrm{I}\Delta_{0} + \mathsf{SupExp} \vdash\mathsf{Con}(\mathsf{NFU}^{-\infty}) \leftrightarrow\mathsf{Con}(\mathrm{I}\Delta_{0} + \mathsf{Exp})$.
(2) $\mathrm{I}\Delta_{0} + \mathsf{Exp} \vdash \mathsf{Con} (\mathsf{NFU}^{-\infty})\rightarrow \mathsf{Con}(\mathrm{I}\Delta_{0} + \mathsf{Exp})$.
(3) $\mathrm{I}\Delta_{0} + \mathsf{Exp} \nvdash \mathsf{Con} (\mathrm{I}\Delta_{0} + \mathsf{Exp})\rightarrow\mathsf{Con} (\mathsf{NFU}^{-\infty})$.
Suspected Answer to Question 1.
Based on the above theorem (part 1), the proof theoretic ordinal of $\mathsf{NFU}^{-\infty}$ is likely to be the same as the proof theoretic ordinal of $\mathrm{I}\Delta_{0} + \mathsf{Exp}$, i.e., is $\omega^3$, if one were to follow the procedure given by Taranovsky to this question.
Answer to Question 2 Solovay's proof of the above theorem makes it clear that  $\mathsf{NFU}^{-\infty}$ interprets $\mathrm{I}\Delta_{0} + \mathsf{Exp}$, but not vice versa; thus the interpretability relation between $\mathsf{NFU}^{-\infty}$ and  $\mathrm{I}\Delta_{0} + \mathsf{Exp}$ is similar to the interpretability relation between $\mathsf{ACA}_0$ and $\mathsf{PA}$.
