This is very cool! I'm wondering how does it compare to classical ATPs like Waldmeister or Vampire, can SupGen compete in CASC (https://tptp.org/CASC/ https://t

This is very cool! I'm wondering how does it compare to classical ATPs like Waldmeister or Vampire, can SupGen compete in CASC (https://tptp.org/CASC/ https://tptp.org/CASC/)? For example, can it proof this example from the recent Stephen Wolfram's post https://writings.stephenwolfram.com/2025/01/who-can-understand-the-proof-a-window-on-formalized-mathematics/ https://writings.stephenwolfram.com/2025/01/who-can-understa... ? Which is basically about proving a•b=b•a from a single axiom ((a•b)•c)•(a•((a•c)•a))=c. Is the source code available for this btw?