% SZS status Success for exponentiate.trs
15.89 (total time)

S-CONVERGENT TRS: 
p(x,m_AC(a_AC(y,z),x3)) -> m_AC(p(x,m_AC(y,x3)),p(x,m_AC(z,x3)))

% SZS status Success for exponentiate.trs
15.86 (total time)

S-CONVERGENT TRS: 
p(x,m_AC(a_AC(y,z),x3)) -> m_AC(p(x,m_AC(y,x3)),p(x,m_AC(z,x3)))

Total time: 15.876299