denis_berthier wrote:ryokousha wrote:btw. Marek told on discord he has a proof it is in T&E(3), so I was expecting that.
As he doesn't have a solver, I guess he used SudoRules. There's no way one could find manually a proof in T&E(3).
I'll take it as a compliment.
Knowing about the exocet made it quite easy, actually.
(After the quads (which are themselves in T&E(3)):)
Depth 1 and 2: 1r7c5 2r7c6 (no loss of generality here).
The finish on depth 3 was quite lengthy, I'll only write the sequence of candidates which (if I didn't make a mistake) break with singles:
3r3c4, 4r3c4, 3r5c4, 4r5c4, 1r6c9, 2r6c9, 1r3c1, 2r3c1, 3r6c1, 4r6c1, 3r3c7, 4r3c7, 1r3c2, 2r3c2, 3r5c2, 4r5c2, 1r6c2, 2r6c2, 3r6c2, 4r6c2
no digit left in r6c2
As there was no loss of generality at depth 1 and 2, analogous proofs exist for other options at these depths.
What isn't feasible manually is to proof whether the pattern was also in T&E(2), all I could say was that it seemed unlikely.
(Had I actually used a solver, this wouldn't have been an issue.)
Marek