Thanks for posting this. This approach certainly seems like the most straightforward way to test systems. "Here are unacceptable ideas and some desirable ideas. Does this system generate the desirable ones and not the unacceptable ones?" The problem is that this isn't computationally reasonable, at least not generally. We could do it with tricks, though someone would have to develop those tricks first :)

I wonder what principles would lead a robot to create that list of unacceptable theorems?