% SZS status Success for binarith.trs 2.87 (total time) S-CONVERGENT TRS: z(zero()) -> zero() p(zero(),x) -> x p(z(x),z(y)) -> z(p(x,y)) p(z(x),o(y)) -> o(p(x,y)) p(o(x),o(y)) -> z(p(o(zero()),p(x,y))) STATISTICS Theory convergent system S: theories/ac.trs General number of iterations: 7 number of nodes: 199 number of processes: 5 time for orient: 0.66 time for rewrite: 1.34 time for S-rewrite: 0.01 time for deduce: 0.53 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: 16 (yes: 14, timeouts: 0) time limit for check: 2.50 termination time: 0.63 Critical pair criterion (primality) redundant CPs in total: 82 for successful process: 12 time to check: 0.21 Indexing techniques: code tree (rewriting) discrimination tree (overlaps) variants: 0.07 encompassments: 0.52 overlaps: 0.00 maintenance: 0.00 One: 0.000032 Two: 0.660423 Total time: 2.884978