% SZS status Success for abelian_groups_homomorphism.trs 13.00 (total time) S-CONVERGENT TRS: g(one()) -> one() g(p(y(),x)) -> p(g(y()),g(x)) p(g(y()),p(g(i(y())),x)) -> x g(i(y())) -> i(g(y())) STATISTICS Theory convergent system S: G General number of iterations: 12 number of nodes: 114 number of processes: 17 time for orient: 9.76 time for rewrite: 1.65 time for S-rewrite: 0.22 time for deduce: 0.74 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: 52 (yes: 44, timeouts: 3) time limit for check: 2.50 termination time: 7.32 Critical pair criterion (primality) redundant CPs in total: 43 for successful process: 8 time to check: 0.08 Indexing techniques: code tree (rewriting) discrimination tree (overlaps) variants: 0.08 encompassments: 0.69 overlaps: 0.00 maintenance: 0.00 One: 0.000055 Two: 9.758346 Total time: 13.010210