And that is so much better because it's executed top-down, with unification like in Prolog, and so it doesn't have to ground the entire Herbrand base and make l

And that is so much better because it's executed top-down, with unification like in Prolog, and so it doesn't have to ground the entire Herbrand base and make little kittens called Skolem cry.