% SZS status Success for ring_unit.trs
8.31 (total time)

S-CONVERGENT TRS: 
m(one(),x) -> x
m(p(x,z),y) -> p(m(x,y),m(z,y))
m(zero(),x) -> zero()
m(i(x),y) -> i(m(x,y))

Total time: 8.310606