% SZS status Satisfiable for semiring.trs
25.49 (total time)

AC-COMPLETE TRS: 
p(zero(),x) -> x
p(zero(),p(x,z)) -> p(x,z)
m(one(),x) -> x
m(one(),m(x,z)) -> m(x,z)
m(p(z,y),x) -> p(m(x,z),m(x,y))
m(p(z,y),m(x,x3)) -> m(p(m(x,z),m(x,y)),x3)
p(m(zero(),z),m(x,z)) -> m(x,z)
p(m(zero(),x),p(m(x,z),y)) -> p(m(x,z),y)
p(m(zero(),x),x) -> x
p(m(zero(),x),p(x,z)) -> p(x,z)
m(zero(),zero()) -> zero()
m(zero(),m(zero(),x)) -> m(zero(),x)


STATISTICS 
General
 number of iterations:    16 
 number of nodes:         400 
 number of processes:     2 
 time for orient:         18.44
 time for rewrite:        4.31
 time for deduce:         2.63

Selection
 strategy: (el(min(e(sum(smax)) + c(sum(smax)))), (data(smax), ( -el(#), ?)))
 time for selection:      0.07

Termination Checks (external with callaprove)
 termination checks:      13 (yes: 9, timeouts: 4)
 time limit for check:    3.00
 termination time:        18.40

Critical pair criterion (primality) 
 redundant CPs in total:  561
 for successful process:  295

Indexing
 techniques: code tree (rewriting) discrimination tree (overlaps)
 variants:                0.26
 encompassments:          0.93
 overlaps:                0.00
 maintenance:             0.01
Total time: 25.513219