% SZS status Success for abelian_groups_homomorphism.trs 4.79 (total time) S-CONVERGENT TRS: one() -> zero() g(p(y(),x)) -> p(g(y()),g(x)) g(zero()) -> zero() g(i(y())) -> i(g(y())) STATISTICS Theory convergent system S: theories/groups1.trs General number of iterations: 13 number of nodes: 104 number of processes: 9 time for orient: 2.95 time for rewrite: 0.93 time for S-rewrite: 0.14 time for deduce: 0.37 Selection strategy: (el(min(e(sum(smax)) + c(sum(smax)))), (data(smax), ( -el(#), ?))) time for selection: 0.06 Termination Checks (external with callmuterm ) termination checks: 30 (yes: 29, timeouts: 0) time limit for check: 2.50 termination time: 1.35 Critical pair criterion (primality) redundant CPs in total: 38 for successful process: 4 time to check: 0.06 Indexing techniques: code tree (rewriting) discrimination tree (overlaps) variants: 0.06 encompassments: 0.37 overlaps: 0.00 maintenance: 0.00 One: 0.000064 Two: 2.952704 Total time: 4.799113