% SZS status Satisfiable for LS94_G0.trs
3.71 (total time)

AC-COMPLETE TRS: 
p(zero(),x) -> x
a(a(x)) -> x
b(b(x)) -> x
i(zero()) -> zero()
i(i(x)) -> x
i(p(x,x1)) -> p(i(x),i(x1))
p(i(x),x) -> zero()
b(a(b(x))) -> a(b(a(x)))


STATISTICS 
General
 number of iterations:    15 
 number of nodes:         163 
 number of processes:     3 
 time for orient:         1.57
 time for rewrite:        1.06
 time for deduce:         0.86

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

Termination Checks (external with callmuterm )
 termination checks:      25 (yes: 20, timeouts: 0)
 time limit for check:    2.50
 termination time:        1.51

Critical pair criterion (primality) 
 redundant CPs in total:  131
 for successful process:  76

Indexing
 techniques: code tree (rewriting) discrimination tree (overlaps)
 variants:                0.06
 encompassments:          0.22
 overlaps:                0.00
 maintenance:             0.00
    One: 0.000000
    Two: 0.000000
Total time: 3.720998