*Below, all structures are finite, in a finite language, with underlying set an initial segment of the natural numbers. **This has been edited to fix errors pointed out by Emil Jerabek in his answer below.***

For $\mathcal{A}$ a structure, let $\mathit{Th}_2(\mathcal{A})$ be the (real coding the) full second-order diagram of $\mathcal{A}$; this is the set of all second-order sentences *with parameters from $\mathcal{A}$* which hold in $\mathcal{A}$. Given isomorphic structures $\mathcal{X}\cong\mathcal{Y}$, it's clear that $\mathit{Th}_2(\mathcal{X}\sqcup\mathcal{Y})$ helps us "efficiently" compute an isomorphism between them since this oracle can answer questions of the form "Does $a_1\mapsto b_1,...,a_n\mapsto b_n$ extend to an isomorphism?"; indeed, we only need the *existential* second-order diagram of their disjoint union to do this. However, it's not clear to me that the join of the second-order theories of the individual structures suffices (it's also not clear exactly what "efficiently" should mean, given that graph isomorphism is already fairly close to $\mathsf{P}$). Here is my attempt at formulating this problem.

> **Main question**: Is there a linear-time (in the length of the input $\mathcal{X}\sqcup\mathcal{Y}$) algorithm which finds an isomorphism between $\mathcal{X}$ and $\mathcal{Y}$ using oracle $\mathit{Th}_2(\mathcal{X})\oplus \mathit{Th}_2(\mathcal{Y})$?

Even a very weak version of this question is unclear to me:

> **Secondary question**: Is there a computable function $F$ such that there is a polynomial-time algorithm which finds an isomorphism between any pair of isomorphic structures $\mathcal{X},\mathcal{Y}$ using the oracle $F(\mathcal{X})\oplus F(\mathcal{Y})$?

(Again, "polynomial-time" here is with respect to the length of the input structures.) Given how close graph isomorphism is to polytime-computable, the answer to this question is "obviously" yes, but I don't immediately see it. This question is motivated by [the analogue for infinite structures](https://arxiv.org/abs/2408.10367); unfortunately, the techniques used in that case are obviously not relevant in the finite setting.