2IMF25 (2018-GS2) Automated reasoning