% SZS status Success for LS94_G0.trs 0.10 (total time) S-CONVERGENT TRS: a(a(x)) -> x b(b(x)) -> x a(b(a(b(a(b(x)))))) -> x STATISTICS Theory convergent system S: theories/groups1.trs General number of iterations: 4 number of nodes: 8 number of processes: 0 time for orient: 0.05 time for rewrite: 0.00 time for S-rewrite: 0.03 time for deduce: 0.01 Selection strategy: (el(min(e(sum(smax)) + c(sum(smax)))), (data(smax), ( -el(#), ?))) time for selection: 0.00 Termination Checks (external with callmuterm ) termination checks: 3 (yes: 3, timeouts: 0) time limit for check: 2.50 termination time: 0.03 Critical pair criterion (primality) redundant CPs in total: 2 for successful process: 2 time to check: 0.00 Indexing techniques: code tree (rewriting) discrimination tree (overlaps) variants: 0.00 encompassments: 0.00 overlaps: 0.00 maintenance: 0.00 One: 0.000015 Two: 0.047360 Total time: 0.108940