% SZS status Success for field.trs 1.62 (total time) STATISTICS: General number of iterations: 36 number of nodes: 375 number of processes: 3 time for orient: 1.33 time for rewrite: 0.16 time for deduce: 0.04 Isomorphism Check: none (detected automatically) Selection strategy: (el(min(e(sum(smax)) + c(sum(smax)))), (data(smax), ( -el(#), ?))) time for selection: 0.02 Process Killing killed 0 exceeding best by: 401% required time: 0.00 Termination Checks (internal) strategy: acrpo -direct termination checks: 81 (yes: 65, timeouts: 0) time limit for check: 1.50 termination time: 1.28 Deduction critical pair criterion: primality redundant CPs in total: 187 for successful process: 11 required time: 0.00 small lemmata propagation: 5 Indexing techniques: code tree (rewriting) discrimination tree (overlaps) variants: 0.01 encompassments: 0.01 overlaps: 0.01 maintenance: 0.00 One: 0.006648 Two: 0.000000 COMPLETE SYSTEM: m(one(),x) -> x m(x,one()) -> x m(d(x),x) -> one() d(one()) -> one() m(m(x,y),z) -> m(x,m(y,z)) m(d(x),m(x,y)) -> y d(d(x)) -> x m(x,d(x)) -> one() m(x,m(d(x),y)) -> y pAC(x,x) -> x pAC(x,y) -> x i(x) -> zero() d(m(x,y)) -> m(d(y),d(x))