[rhelz]

I was writing a theorem prover for higher-order modal logic. All the theorem provers written in C or C++ were tens of thousands of lines, and even at that they had only a fraction of what I needed. What's more, they were all like 100 times *slower* at proving theorems which prolog could prove out of the box.

So I decided to try to implement the features I needed on top of the theorem prover which prolog already is.

Took me forever, but eventually it all came together like a thunderclap, and I was able to implement a theorem prover for quantified, higher-order modal logic which was amazingly-blazingly fast--in 67 lines of prolog.

In terms of lines-of-code per day, its the least productive I've ever been :-)