% SZS status Success for nats_mul.trs
2.41 (total time)

S-CONVERGENT TRS: 
-(zero(),x) -> zero()
-(x,zero()) -> x
+_AC(zero(),x) -> x
*_AC(zero(),x) -> zero()
+_AC(s(x),y) -> s(+_AC(x,y))
-(s(x),s(y)) -> -(x,y)
*_AC(s(x),y) -> +_AC(*_AC(x,y),y)
*_AC(+_AC(x,y),z) -> +_AC(*_AC(x,z),*_AC(y,z))

% SZS status Success for nats_mul.trs
2.40 (total time)

S-CONVERGENT TRS: 
-(zero(),x) -> zero()
-(x,zero()) -> x
+_AC(zero(),x) -> x
*_AC(zero(),x) -> zero()
+_AC(s(x),y) -> s(+_AC(x,y))
-(s(x),s(y)) -> -(x,y)
*_AC(s(x),y) -> +_AC(*_AC(x,y),y)
*_AC(+_AC(x,y),z) -> +_AC(*_AC(x,z),*_AC(y,z))

Total time: 2.416974