Comment by AxEy

> The real problem turns out to be the combinatorial explosion inherent in unstructured search through the Herbrand universe. One needs Unification and one needs a still missing ingredient to give search a sense of direction.

Shameless plug: I put together a Jupyter notebook walking through the use of Herbrand Universes for a semi-decision procedure for first order logic: https://github.com/aetilley/harrison-rust/blob/main/Herbrand...