Yeah, I tried Z3 (and other things) for the typewriter (my write up is linked at the bottom of the original linear typewriter post) and got nothing useful out of it - even with extra constraints like "make sure E and T are close together".
(But your 13M years is a lot quicker than my projected seven hundred ninety-eight trillion, seven hundred twenty billion, nine hundred fifty-two million, one hundred seventy-six thousand, seven hundred and forty-five years you'd need for an exhaustive search of the 26! possibilities.)
However, trying to use his method to optimise a linear typewriter[2] proved unsuccessful, as projected solving time was around 13 million years.
[1]https://yurichev.com/blog/cabling_Z3/ [2]https://www.benjaminpoilve.com/projects/typewriter-optimisat...