@article{Beckert2003,
  author        = {Bernhard Beckert},
  title         = {Depth-first Proof Search without Backtracking for
                   Free-variable Clausal Tableaux},
  journal       = {Journal of Symbolic Computation},
  volume        = {36},
  number        = {1-2},
  pages         = {117--138},
  doi           = {10.1016/S0747-7171(03)00026-9},
  year          = {2003}
}