korf@maui.cs.ucla.edu (11/19/88)
Another reference on this subject is: "An analysis of consecutively bounded depth-first search with applications in automated deduction", by Mark E. Stickel and W. Mabry Tyson, in IJCAI-85, pp. 1073-1075.