Dear all, the conversion to the new ARI format is done for all first-order TRS/SRS categories [1]. The tool to convert back and forth between XTC and ARI is available here [2] (note that you have to use the branch xtc, not the master branch). Some documentation for the new format is available here [3]. If you have suggestions to improve it, please let me know. Regarding valid identifiers, there might be (hopefully minimal) changes in the (near) future. In particular, the question which identifiers should be quoted is not entirely settled. If you're interested, please participate in the corresponding discussion on Github [4]. Nevertheless, I think the current version is good enough to start testing. Let me know if you run into any problems. Best Florian [1] https://github.com/TermCOMP/TPDB-ARI [2] https://github.com/TermCOMP/ari-conversion/tree/xtc [3] https://termination-portal.org/wiki/Term_Rewriting [4] https://github.com/orgs/TermCOMP/discussions/83#discussioncomment-8676014