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.

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; unfortunately, the techniques used in that case are obviously not relevant in the finite setting.