[newacctjhro]

Resolution isn't really brute force search, in that it doesn't search all possible solutions at random; the search is directed by the programmer's rules.

But yeah, it involves quite a lot of backtracking, that happens when the resolution engine needs to go back and try something different. When this is a problem you can sometimes use the cut rule http://www.cse.unsw.edu.au/~billw/dictionaries/prolog/cut.ht...