@TECHREPORT{BarST-RR-05,
  author =	 {Clark Barrett and Igor Shikanian and Cesare Tinelli},
  title =	 {An Abstract Decision Procedure for Satisfiability in
                  the Theory of Recursive Data Types},
  Institution =	 {Department of Computer Science, New York University},
  month =	 nov,
  year =	 2005,
  number =	 {TR2005-878},
  url =
                  {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BarST-RR-05.pdf},
}