UPDATE: There is still another version, less exotic, at github. Both are working versions of kali. For those with mathematical inclinations there are explanations in the tool rhs.js. This will come to a conclusion with the explanations about FO and with the tools to choose optimal collections of rewrites.
There is a working version of kali which I posted today. Enjoy and wonder how can it (sometimes!) reduce lambda terms even if it has nothing to do with lambda calculus in the background. The js script is interesting to read, or better the script from the page which generates DIST rewrites (which you can add in your copy of the main script and play with it, it is enough to add it to the list of rewrites).
It is comical how does it fail sometimes. Space is symmetrical and logic is constrained.
Also I think I’ll pursue the idea to train the (choice of rewrites, probabilities) for certain tasks, as evoked here.