% SZS status Success for A95_ex4_2_4a.trs
1.42 (total time)

S-CONVERGENT TRS: 
s(p(x)) -> x
p(s(x)) -> x
m(x,zero()) -> x
m(x,s(y)) -> p(m(x,y))
a_AC(s(y),x) -> s(a_AC(x,y))
m(x,p(y)) -> s(m(x,y))
a_AC(p(x),y) -> p(a_AC(x,y))

% SZS status Success for A95_ex4_2_4a.trs
1.40 (total time)

S-CONVERGENT TRS: 
s(p(x)) -> x
p(s(x)) -> x
m(x,zero()) -> x
m(x,s(y)) -> p(m(x,y))
a_AC(s(y),x) -> s(a_AC(x,y))
m(x,p(y)) -> s(m(x,y))
a_AC(p(x),y) -> p(a_AC(x,y))

Total time: 1.412082