% SZS status Success for integers.trs
3.98 (total time)

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

% SZS status Success for integers.trs
4.01 (total time)

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

Total time: 4.029563