@article{riazanov2002,
	title = {The design and implementation of VAMPIRE.},
	author = {Alexandre Riazanov and Andrei Voronkov},
	journal = {AI Commun.},
	number = {2-3},
	pages = {91-110},
	url = {http://dblp.uni-trier.de/db/journals/aicom/aicom15.html#RiazanovV02},
	volume = {15},
	year = {2002},
	biburl = {http://www.bibsonomy.org/bibtex/27383ce7fb56c880f52243294ad01421d/thau},
	description = {dblp},
	ee = {http://iospress.metapress.com/openurl.asp?genre=article&issn=0921-7126&volume=15&issue=2&spage=91}, date = {2003-11-27},
	keywords = {first-order reasoning }
}

@article{journals/aicom/RiazanovV02,
	title = {The design and implementation of VAMPIRE.},
	author = {Alexandre Riazanov and Andrei Voronkov},
	journal = {AI Commun.},
	number = {2-3},
	pages = {91-110},
	url = {http://dblp.uni-trier.de/db/journals/aicom/aicom15.html#RiazanovV02},
	volume = {15},
	year = {2002},
	biburl = {http://www.bibsonomy.org/bibtex/27383ce7fb56c880f52243294ad01421d/dblp},
	description = {dblp},
	ee = {http://iospress.metapress.com/openurl.asp?genre=article&issn=0921-7126&volume=15&issue=2&spage=91}, date = {2003-11-27},
	keywords = {dblp }
}