 To be frank, the program is supplied with key information to establish the lemmas that lead to this theorem but the amount and type of deductive work done by the program is certainly nontrivial. (Clarke &amp; Zhao 1994) provides examples of fully automated proofs using problems in Chapter 2 of Ramanujan’s Notebooks (Berndt 1985) including the following example that the reader is invited to try. Show that: