% SZS status Success for LS94_G2.trs 12.35 (total time) S-CONVERGENT TRS: p(a(),p(a(),p(b(),p(b(),x)))) -> x i(b()) -> p(a(),p(a(),b())) p(b(),b()) -> p(i(a()),i(a())) STATISTICS Theory convergent system S: theories/groups1.trs General number of iterations: 6 number of nodes: 49 number of processes: 11 time for orient: 6.16 time for rewrite: 4.67 time for S-rewrite: 0.29 time for deduce: 1.07 Selection strategy: (el(min(e(sum(smax)) + c(sum(smax)))), (data(smax), ( -el(#), ?))) time for selection: 0.02 Termination Checks (external with callmuterm ) termination checks: 23 (yes: 23, timeouts: 0) time limit for check: 2.50 termination time: 0.43 Critical pair criterion (primality) redundant CPs in total: 34 for successful process: 0 time to check: 0.07 Indexing techniques: code tree (rewriting) discrimination tree (overlaps) variants: 0.04 encompassments: 1.41 overlaps: 0.00 maintenance: 0.00 One: 0.000028 Two: 6.158063 Total time: 12.364460