To be honest I'd like it to be possible to completely do away with graph search in Resolution-based theorem proving. Resolution itself assumes no search, it's only an inference rule that removes contradictions from a theory. The original paper on Resolution proposes various ways to implement it but they all come down to search of some sort. I guess that's all we know how to do in AI: search :/