@article{BofillRubio13JAR,
year={2013},
issn={0168-7433},
journal={Journal of Automated Reasoning},
volume={50},
issue={1},
doi={10.1007/s10817-011-9244-z},
title={Paramodulation with Non-Monotonic Orderings and Simplification},
url={http://dx.doi.org/10.1007/s10817-011-9244-z},
publisher={Springer Netherlands},
keywords={Automated theorem proving; Equational reasoning; Ordered paramodulation; Knuth-Bendix completion},
author={Bofill, Miquel and Rubio, Albert},
pages={51-98},
language={English}
}