EQUATIONS: double_divide(double_divide(double_divide(a,double_divide(b,identity())),double_divide(double_divide(c,double_divide(d,double_divide(d,identity()))),double_divide(a,identity()))),b) = c multiply(a,b) = double_divide(double_divide(b,a),identity()) inverse(a) = double_divide(a,identity()) identity() = double_divide(a,inverse(a)) COMPLETE TRS: RULES: inverse(identity()) -> identity() inverse(inverse(x)) -> x multiply(x,inverse(x)) -> identity() multiply(identity(),x) -> x multiply(inverse(x),multiply(x,y)) -> y inverse(multiply(x,y)) -> multiply(inverse(y),inverse(x)) multiply(multiply(x,y),z) -> multiply(x,multiply(y,z)) multiply(inverse(x),x) -> identity() multiply(x,identity()) -> x double_divide(y,x) -> multiply(inverse(y),inverse(x)) multiply(y,multiply(inverse(y),x)) -> x SUCCESS MaxTRS: 9 Search time: 57.20 seconds