Detecting if three Turing Machines halt given a magic oracle that is only used twice

We were given a question in class as follows:

You have a "magic oracle" that can decide if a Turing Machine halts. You have three TMs $T_1, T_2, T_3$. Device an algorithm that decides which of the TMs halt and which do not by asking the oracle at most twice.

The sketch of the solution given was

Construct a new TM $T_A$ that terminates if at least 2 TMs (from $T_1, T_2, T_3$) halts.
Construct a new TM $T_B$ that terminates if one TM halts.

First call oracle on $T_A$.
If $T_A$ halts:
Run $T_1, T_2, T_3$ in parallel until two of them halt, then call the oracle on the last TM that does not finish running.

If $T_A$ doesn’t halt:

Call oracle on $T_B$,
If $T_B$ halts:
Then run $T_1, T_2, T_3$ in parallel until one of them halts. That TM is the only one that halts

If $T_B$ does not halt:
then $T_1, T_2, T_3$ all do not halt.

I did not agree with this solution, as formalising the proof would mean $T_A$ and $T_B$ are Oracle Turing Machines that must ask the oracle about the termination of $T_1, T_2, T_3$. The professor replied

They don't use magic oracles internally, because they are not claimed to detect termination, they just terminate if and only if other machines terminate, which can be achieved through concurrent interpretation of that machines.

Is this right? How would you go about formalising this? Thanks.

One way to built $T_A$ works is roughly as follows:

While (true) {
   run $T_1$ for 10 steps, if $T_1$ halts during that time, $i := 1$, break;
   run $T_2$ for 10 steps, if $T_2$ halts during that time, $i := 2$, break;
   run $T_3$ for 10 steps, if $T_3$ halts during that time, $i := 3$, break;
}

While (true) {
   if not $i = 1$
       run $T_1$ for 10 steps, if $T_1$ halts during that time, break;
   if not $i = 2$
       run $T_2$ for 10 steps, if $T_2$ halts during that time, break;
   if not $i = 3$
       run $T_3$ for 10 steps, if $T_3$ halts during that time, break;
}

halt

As you see, there is no magic involved.

StackExchange Computer Science Q#157212, answer score: 18