This is very cool! I'm wondering how does it compare to classical ATPs like Waldmeister or Vampire, can SupGen compete in CASC (<a href="https://tptp.org/CASC/" rel="nofollow">https://tptp.org/CASC/</a>)?<p>For example, can it proof this example from the recent Stephen Wolfram's post <a href="https://writings.stephenwolfram.com/2025/01/who-can-understand-the-proof-a-window-on-formalized-mathematics/" rel="nofollow">https://writings.stephenwolfram.com/2025/01/who-can-understa...</a> ?
Which is basically about proving a•b=b•a from a single axiom ((a•b)•c)•(a•((a•c)•a))=c.<p>Is the source code available for this btw?
Reminds me of miniKanren but with static typing (which I’ve always wanted to see an implementation of).<p>Will be playing with the various releases of SupGen as you improve it