% SZS status Success for abelian_groups_comm_action.trs
15.40 (total time)

S-CONVERGENT TRS: 
g1(zero()) -> zero()
g2(zero()) -> zero()
phi(zero(),x) -> x
phi(x,phi(y,z)) -> phi(p(x,y),z)
phi(g2(x),g1(y)) -> phi(g1(y),g2(x))
g1(p(y(),x)) -> p(g1(y()),g1(x))
g2(p(y(),x)) -> p(g2(y()),g2(x))
g1(i(y())) -> i(g1(y()))
g2(i(y())) -> i(g2(y()))


STATISTICS 
Theory
 convergent system S:     theories/groups1.trs 

General
 number of iterations:    13 
 number of nodes:         486 
 number of processes:     35 
 time for orient:         5.77
 time for rewrite:        3.56
 time for S-rewrite:      0.12
 time for deduce:         0.52

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

Termination Checks (external with callmuterm )
 termination checks:      125 (yes: 105, timeouts: 0)
 time limit for check:    2.50
 termination time:        4.64

Critical pair criterion (primality) 
 redundant CPs in total:  57
 for successful process:  17
 time to check:      0.10

Indexing
 techniques: code tree (rewriting) discrimination tree (overlaps)
 variants:                0.26
 encompassments:          1.76
 overlaps:                0.00
 maintenance:             0.00
    One: 0.000063
    Two: 5.769415
Total time: 15.410008