% SZS status Success for A95_naturals.trs 0.39 (total time) STATISTICS: General number of iterations: 7 number of nodes: 17 number of processes: 4 time for orient: 0.36 time for rewrite: 0.00 time for deduce: 0.00 Isomorphism Check: none (detected automatically) Selection strategy: (el(min(e(sum(smax)) + c(sum(smax)))), (data(smax), ( -el(#), ?))) time for selection: 0.00 Process Killing killed 0 exceeding best by: 401% required time: 0.00 Termination Checks (internal) strategy: ackbo -ib 2 -ob 3 -direct -sc -nt termination checks: 15 (yes: 13, timeouts: 0) time limit for check: 1.50 termination time: 0.35 Deduction critical pair criterion: primality redundant CPs in total: 11 for successful process: 0 required time: 0.00 small lemmata propagation: 5 Indexing techniques: code tree (rewriting) discrimination tree (overlaps) variants: 0.00 encompassments: 0.00 overlaps: 0.00 maintenance: 0.00 One: 0.001056 Two: 0.000000 COMPLETE SYSTEM: plus(x,0()) -> x minAC(0(),x) -> 0() maxAC(0(),x) -> x plus(x,s(y)) -> s(plus(x,y)) minAC(s(x),s(y)) -> s(minAC(x,y)) maxAC(s(x),s(y)) -> s(maxAC(x,y))