Fix three positive integers n, k, m.
Prove that a group subgroup H of S_{6+(n+k+m)} generated by
g1:=G!(1,6,4,3,a_1,...a_n);
g2:=G!(1,2,4,5,b_1,...,b_k);
g3:=G!(5,6,2,3,c_1,...,c_m);
H:=sub<G|[g1,g2,g3]>;
satisfies H = S_{6+(n+k+m)} or H = A_{6+(n+k+m)}.
ChatGPT-Pro-5.1 informal sketch
https://chatgpt.com/share/69339179-a46c-8007-bed0-56c25556492a
The informal sketch has been completely formalized in Harmonic Aristotle in about 20 hours, during two mixed runs. The code is more than 2000 lines.