2IMF25 (2023-GS1) Automated reasoning