Automated deduction in equational logic and cubic curves - McCune, W. (Springer,)