[sw1sh]

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/)?

For example, can it proof this example from the recent Stephen Wolfram's post 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?