That gave me something to play with with these models and this came out as a claimed disproof of the Dixmier Conjecture:

https://gist.githubusercontent.com/pedrocr/51157b9b2eed8152e...

It seems mathematics has at least gotten a powerful new tool to automate the work to cascade results after breakthroughs are made.