tuned messages: implement "verbose = false", but there is no theory output anyway;