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.)