EQUATIONS: divide(a,divide(divide(divide(identity(),b),c),divide(divide(divide(a,a),a),c))) = b multiply(a,b) = divide(a,divide(identity(),b)) inverse(a) = divide(identity(),a) identity() = divide(a,a) COMPLETE TRS: RULES: inverse(identity()) -> identity() divide(x,identity()) -> x inverse(inverse(x)) -> x divide(x,divide(y,inverse(x))) -> inverse(y) divide(inverse(x),divide(y,x)) -> inverse(y) multiply(x,y) -> divide(x,inverse(y)) divide(divide(x,y),z) -> divide(x,divide(z,inverse(y))) divide(inverse(x),divide(y,divide(x,z))) -> divide(inverse(z),y) divide(identity(),a) -> inverse(a) divide(a,a) -> identity() inverse(divide(y,x)) -> divide(x,y) divide(z,divide(y,divide(inverse(z),x))) -> divide(inverse(x),y) SUCCESS MaxTRS: 2 Search time: 2.91 seconds