This work used CatGo (https://catgo-ucsd.org).

Requested acknowledgement and citation; not an additional condition of AGPL-3.0-or-later.
