I didn't remember that quote from O'Keefe. Prolog is indeed not trying to be smart and SLD-Resolution is dead simple - it's a sound and complete deductive inference system with a single rule. The reason Prolog is in turn so simple is because, thanks to the refutation-completeness of SLD-Resolution, you can implement it as a Depth-First Search for resolvents and then spam it until you get a result (or until you hit an infinite branch... oops). That's certainly orders of magnitude more simple than every other solver or automated theorem prover out there, like you say.

If that's what O'Keefe means, that Proolog is not trying to be smart, then OK, but that's not dumb. Every other solver tries to be smart and ends up having to solve an unsolvable problem. Who's dumb now then?

But maybe that's the compliment, I don't remember the context of O'Keefe's comment. Was it in the Craft of Prolog?