% SZS status GaveUp (Completion failed.) for ring_unit_homo.trs 13.65 (total time) STATISTICS: General number of iterations: 33 number of nodes: 181 number of processes: 0 time for orient: 13.49 time for rewrite: 0.07 time for deduce: 0.03 Isomorphism Check: none (detected automatically) Selection strategy: (el(min(e(sum(smax)) + c(sum(smax)))), (data(smax), ( -el(#), ?))) time for selection: 0.01 Process Killing killed 3 exceeding best by: 401% required time: 0.00 Termination Checks (internal) strategy: dp; (acrpo -af)* termination checks: 67 (yes: 32, timeouts: 0) time limit for check: 1.50 termination time: 13.45 Deduction critical pair criterion: primality redundant CPs in total: 119 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.01 maintenance: 0.00 One: 0.003656 Two: 0.000000