NB: In der Tat hat aber der symbolische Theorembeweiser Otter von Bill McCune bereits im Oktober 1997 das Robbins-Problem (Jede Robbins-Algebra ist eine Boolesche Algebra) gelöst, das seit den 1930er Jahren offen war. Mit Hilfe des ILF-Systems, dass meine Arbeitsgruppe an der Humboldt-Universität zu Berlin entwickelte, konnte ich das unverständliche, weil zu detaillierte, Beweisprotokoll in einen Beweis transformieren, der mathematische Einsichten vermittelt und der 1998 im Journal of Algebra publiziert wurde.