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?

Taelin is insane

Reminds me of miniKanren but with static typing (which I’ve always wanted to see an implementation of).

Will be playing with the various releases of SupGen as you improve it

Quite mindblowing to be totally honest.

Man, the future's gonna be crazy