kill
% SZS status Success for example13.trs
19.06 (total time)

S-CONVERGENT TRS: 
g1(zero()) -> zero()
g2(zero()) -> zero()
phi(zero(),x) -> x
phi(x,phi(y1,y2)) -> phi(p_AC(x,y1),y2)
phi(g2(x),zero()) -> g2(x)
phi(g1(x),zero()) -> g1(x)
g1(p_AC(y(),x)) -> p_AC(g1(y()),g1(x))
g2(p_AC(y(),x)) -> p_AC(g2(y()),g2(x))
phi(y1,g2(x)) -> phi(p_AC(g2(x),y1),zero())
phi(y1,g1(x)) -> phi(p_AC(g1(x),y1),zero())
p_AC(g1(y()),g1(i(y()))) -> zero()
i(g1(y())) -> g1(i(y()))
i(g1(i(y()))) -> g1(y())
p_AC(g2(y()),g2(i(y()))) -> zero()
i(g2(y())) -> g2(i(y()))
i(g2(i(y()))) -> g2(y())

kill
% SZS status Success for example13.trs
19.10 (total time)

S-CONVERGENT TRS: 
g1(zero()) -> zero()
g2(zero()) -> zero()
phi(zero(),x) -> x
phi(x,phi(y1,y2)) -> phi(p_AC(x,y1),y2)
phi(g2(x),zero()) -> g2(x)
phi(g1(x),zero()) -> g1(x)
g1(p_AC(y(),x)) -> p_AC(g1(y()),g1(x))
g2(p_AC(y(),x)) -> p_AC(g2(y()),g2(x))
phi(y1,g2(x)) -> phi(p_AC(g2(x),y1),zero())
phi(y1,g1(x)) -> phi(p_AC(g1(x),y1),zero())
p_AC(g1(y()),g1(i(y()))) -> zero()
i(g1(y())) -> g1(i(y()))
i(g1(i(y()))) -> g1(y())
p_AC(g2(y()),g2(i(y()))) -> zero()
i(g2(y())) -> g2(i(y()))
i(g2(i(y()))) -> g2(y())

Total time: 19.116740