% SZS status GaveUp (Completion failed.) for sum.trs 30.22 (total time) STATISTICS: General number of iterations: 54 number of nodes: 623 number of processes: 0 time for orient: 28.04 time for rewrite: 0.68 time for deduce: 0.57 Isomorphism Check: none (detected automatically) Selection strategy: (el(min(e(sum(smax)) + c(sum(smax)))), (data(smax), ( -el(#), ?))) time for selection: 0.04 Process Killing killed 1 exceeding best by: 401% required time: 0.00 Termination Checks (internal) strategy: matrix -ac -ib 2 -ob 3 -dim 1 -direct termination checks: 144 (yes: 51, timeouts: 0) time limit for check: 1.50 termination time: 27.25 Deduction critical pair criterion: primality redundant CPs in total: 368 for successful process: 0 required time: 0.01 small lemmata propagation: 5 Indexing techniques: code tree (rewriting) discrimination tree (overlaps) variants: 0.01 encompassments: 0.02 overlaps: 0.06 maintenance: 0.00 One: 0.007235 Two: 0.000000