My main use of an automated reasoning program for applications is in the context of proving theorems from areas of mathematics and logic. With no intended denigration, I refer here to proof finding, rather than to proof checking. The goal of emulating the human mind is certainly not mine, when I focus on the automation of logical reasoning. Indeed, I think such emulation a goal essentially out of reach. For example, the mathematician uses instantiation when deducing that the square of yz is the identity from the hypothesis that the square of x is the identity, in the theorem that asserts that groups in which the square of every element is the identity are cmmutative.
Wise instantiation seems too difficult to automate.
Clearly, the mathematicians they quoted were unaware of the successes in answering open questions, where a key role was played by an automated reasoning program. In my own work, I freely admit to waking up with a solution to a problem. The explicit use of strategy, I have often said, is but one of the differences in some of automated reasoning as compared with research by mathematicians. Within twenty years, some mathematicians will have formed an impressive team with some automated reasoning program to answer a number of deep questions. But perhaps I have missed the point of the objection.