On the notion of complexity of search in theorem proving