Below, all structures are finite, in a finite language, with underlying set an initial segment of the natural numbers.

For $\mathcal{A}$ a structure, let $\mathit{Th}_2(\mathcal{A})$ be the (real coding the) full second-order theory of $\mathcal{A}$. Given two isomorphic structures $\mathcal{X}\cong\mathcal{Y}$, an isomorphism between them is clearly computable in linear time from $\mathit{Th}_2(\mathcal{X}\sqcup\mathcal{Y})$; indeed, we only need the existential second-order theory 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:

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. Note that if we restrict attention to rigid structures then the answer becomes affirmative (e.g. we can have $F$ pick out a distinguished linear-order-with-successor on the isomorphism type of the structure involved), but that's a very strong assumption.

This question is motivated by the analogue for infinite structures; unfortunately, the techniques used in that case are obviously not relevant in the finite setting.