This is the Logic Theorist: https://en.wikipedia.org/wiki/Logic_Theorist

I love Simon's anecdote of using his wife and children as the stack as he developed IPS.

This eventually was replaced by GPS, which has a good description in Norvig's Paradigms of Artificial Programming, here: https://github.com/norvig/paip-lisp