From Newsgroup: sci.logic

Dear All,

Lets posit this Autum Challenge 2025.
The idea is to forget about Robert St|nrks
proof framework, although impressive,

and it can possibly proof:

a + (b + c) = (a + b) + c

In the natural numbers. Why not try
an entropy based iterative deepening,
and simply find a proof justification

for the above in a more undisciplined manner:

Canonical for Automated Theorem Proving in Lean https://arxiv.org/abs/2504.06239

Unfortunately the above seems to be a Rust
program. Can we implement it in Prolog itself?
Disclaimer: Here canonical doesn't meen minimal DFA ,

just in case Julio Di Egidio thinks otherwise.

Bye
--- Synchronet 3.21a-Linux NewsLink 1.2