Conservativity of an ultrafilter of IP sets over \a0${\mathbf{ATR_0}}$

An IP set is a set of natural numbers containing all finite sums of an infinite sequence of natural numbers. Let $\mathfrak{U}$ be an ultrafilter on $\mathbb{N}$, and let $\mathbf{ATR_0}$ denote the corresponding subsystem of second-order arithmetic. IP-ultrafilter conservativity conjecture. The theory

$$\mathbf{ATR_0}+\exists\mathfrak{U}+\text{“every element of $\mathfrak{U}$ is IP”}$$

is a conservative extension of $\mathbf{ATR_0}$. This asks whether the existence of an ultrafilter all of whose members are IP sets adds no first-order consequences to $\mathbf{ATR_0}$; the source presents the claim in the context of the difficulty of separating Hindman's-type principles from $\mathbf{ACA_0}$, and gives no resolution.