%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : ITP042^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:05:21 AM UTC 2026
% Result : Theorem 0.25s 0.37s
% Output : CNFRefutation 0.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP042^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.18 % Computer : n026.cluster.edu
% 0.10/0.18 % Model : x86_64 x86_64
% 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.18 % Memory : 8046.5625MB
% 0.10/0.18 % OS : Linux 6.8.0-71-generic
% 0.10/0.18 % CPULimit : 300
% 0.10/0.18 % WCLimit : 300
% 0.10/0.18 % DateTime : Tue Sep 29 19:43:27 UTC 2026
% 0.10/0.18 % CPUTime :
% 0.10/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.23 Running higher-order theorem proving
% 0.10/0.28 Running: /export/starexec/sandbox2/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/tmp/tmp.XthW0FekP7/E---3.1_1088897.p
% 0.25/0.37 % Version: 3.5.1-ho
% 0.25/0.37 % Preprocessing class: HSLSSMSMSSLNHSA.
% 0.25/0.37 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 0.25/0.37 % Starting ho_unfolding_8 with 900s (3) cores
% 0.25/0.37 % Starting new_bool_8 with 300s (1) cores
% 0.25/0.37 % Starting post_as_ho6 with 300s (1) cores
% 0.25/0.37 % Starting ho_unfolding_1 with 300s (1) cores
% 0.25/0.37 % Starting full_lambda_4 with 300s (1) cores
% 0.25/0.37 % Starting pre_casc_5 with 300s (1) cores
% 0.25/0.37 % new_bool_8 with pid 1088933 completed with status 0
% 0.25/0.37 % Result found by new_bool_8
% 0.25/0.37 % Preprocessing class: HSLSSMSMSSLNHSA.
% 0.25/0.37 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 0.25/0.37 % Starting ho_unfolding_8 with 900s (3) cores
% 0.25/0.37 % Starting new_bool_8 with 300s (1) cores
% 0.25/0.37 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,1,,2,20000,1.0))
% 0.25/0.37 % SinE strategy is GSinE(CountFormulas,hypos,1,,2,20000,1.0)
% 0.25/0.37 % Search class: HGUSM-FFLM32-MHSFFSBN
% 0.25/0.37 % partial match(1): HGUSM-FSLM32-MHSFFSBN
% 0.25/0.37 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.25/0.37 % Starting SubtermCWHack with 28s (1) cores
% 0.25/0.37 % SubtermCWHack with pid 1088940 completed with status 0
% 0.25/0.37 % Result found by SubtermCWHack
% 0.25/0.37 % Preprocessing class: HSLSSMSMSSLNHSA.
% 0.25/0.37 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 0.25/0.37 % Starting ho_unfolding_8 with 900s (3) cores
% 0.25/0.37 % Starting new_bool_8 with 300s (1) cores
% 0.25/0.37 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,1,,2,20000,1.0))
% 0.25/0.37 % SinE strategy is GSinE(CountFormulas,hypos,1,,2,20000,1.0)
% 0.25/0.37 % Search class: HGUSM-FFLM32-MHSFFSBN
% 0.25/0.37 % partial match(1): HGUSM-FSLM32-MHSFFSBN
% 0.25/0.37 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.25/0.37 % Starting SubtermCWHack with 28s (1) cores
% 0.25/0.37 % Preprocessing time : 0.005 s
% 0.25/0.37
% 0.25/0.37 % Proof found!
% 0.25/0.37 % SZS status Theorem
% 0.25/0.37 % SZS output start CNFRefutation
% 0.25/0.37 thf(decl_sort1, type, set_Su111624115um_c_b: $tType).
% 0.25/0.37 thf(decl_sort2, type, denota723907260t_unit: $tType).
% 0.25/0.37 thf(decl_sort3, type, a: $tType).
% 0.25/0.37 thf(decl_sort4, type, trm_a_b: $tType).
% 0.25/0.37 thf(decl_sort5, type, sum_su1965225555um_c_b: $tType).
% 0.25/0.37 thf(decl_sort6, type, set_a: $tType).
% 0.25/0.37 thf(decl_23, type, denota896875430_a_c_b: denota723907260t_unit > denota723907260t_unit > set_Su111624115um_c_b > $o).
% 0.25/0.37 thf(decl_63, type, ord_le1404954451um_c_b: set_Su111624115um_c_b > set_Su111624115um_c_b > $o).
% 0.25/0.37 thf(decl_84, type, collec1166375742um_c_b: (sum_su1965225555um_c_b > $o) > set_Su111624115um_c_b).
% 0.25/0.37 thf(decl_91, type, static_SIGT_a_b: trm_a_b > set_a).
% 0.25/0.37 thf(decl_93, type, sum_In811702836um_c_b: a > sum_su1965225555um_c_b).
% 0.25/0.37 thf(decl_111, type, member_a: a > set_a > $o).
% 0.25/0.37 thf(decl_112, type, i: denota723907260t_unit).
% 0.25/0.37 thf(decl_113, type, j: denota723907260t_unit).
% 0.25/0.37 thf(decl_116, type, theta_1: trm_a_b).
% 0.25/0.37 thf(decl_117, type, theta_2: trm_a_b).
% 0.25/0.37 thf(decl_119, type, esk2_2: (sum_su1965225555um_c_b > $o) > (sum_su1965225555um_c_b > $o) > sum_su1965225555um_c_b).
% 0.25/0.37 thf(decl_138, type, epred1_0: sum_su1965225555um_c_b > $o).
% 0.25/0.37 thf(decl_143, type, epred6_0: sum_su1965225555um_c_b > $o).
% 0.25/0.37 thf(decl_144, type, esk21_1: sum_su1965225555um_c_b > a).
% 0.25/0.37 thf(decl_147, type, esk24_1: sum_su1965225555um_c_b > a).
% 0.25/0.37 thf(conj_0, conjecture, (denota896875430_a_c_b @ i @ j @ (collec1166375742um_c_b @ (^[X3:sum_su1965225555um_c_b]:(?[X4:a]:(((((X3)=(sum_In811702836um_c_b @ X4)))&((member_a @ X4 @ (static_SIGT_a_b @ theta_1))))))))), file('/export/starexec/sandbox2/tmp/tmp.XthW0FekP7/E---3.1_1088897.p', conj_0)).
% 0.25/0.37 thf(fact_2_IA, axiom, (denota896875430_a_c_b @ i @ j @ (collec1166375742um_c_b @ (^[X3:sum_su1965225555um_c_b]:(?[X4:a]:(((((X3)=(sum_In811702836um_c_b @ X4)))&((((member_a @ X4 @ (static_SIGT_a_b @ theta_1)))|((member_a @ X4 @ (static_SIGT_a_b @ theta_2))))))))))), file('/export/starexec/sandbox2/tmp/tmp.XthW0FekP7/E---3.1_1088897.p', fact_2_IA)).
% 0.25/0.37 thf(fact_178_Collect__mono, axiom, ![X363:sum_su1965225555um_c_b > $o, X364:sum_su1965225555um_c_b > $o]:((![X365:sum_su1965225555um_c_b]:(((X363 @ X365)=>(X364 @ X365)))=>(ord_le1404954451um_c_b @ (collec1166375742um_c_b @ X363) @ (collec1166375742um_c_b @ X364)))), file('/export/starexec/sandbox2/tmp/tmp.XthW0FekP7/E---3.1_1088897.p', fact_178_Collect__mono)).
% 0.25/0.37 thf(fact_52_Iagree__sub, axiom, ![X88:set_Su111624115um_c_b, X89:set_Su111624115um_c_b, X1:denota723907260t_unit, X2:denota723907260t_unit]:(((ord_le1404954451um_c_b @ X88 @ X89)=>((denota896875430_a_c_b @ X1 @ X2 @ X89)=>(denota896875430_a_c_b @ X1 @ X2 @ X88)))), file('/export/starexec/sandbox2/tmp/tmp.XthW0FekP7/E---3.1_1088897.p', fact_52_Iagree__sub)).
% 0.25/0.37 thf(c_0_4, plain, ![X1374:sum_su1965225555um_c_b, X1376:sum_su1965225555um_c_b, X1377:a]:((((((X1374)=(sum_In811702836um_c_b @ (esk21_1 @ X1374)))|~(epred6_0 @ X1374))&((member_a @ (esk21_1 @ X1374) @ (static_SIGT_a_b @ theta_1))|(member_a @ (esk21_1 @ X1374) @ (static_SIGT_a_b @ theta_2))|~(epred6_0 @ X1374)))&((~(member_a @ X1377 @ (static_SIGT_a_b @ theta_1))|((X1376)!=(sum_In811702836um_c_b @ X1377))|(epred6_0 @ X1376))&(~(member_a @ X1377 @ (static_SIGT_a_b @ theta_2))|((X1376)!=(sum_In811702836um_c_b @ X1377))|(epred6_0 @ X1376))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[])])])])])])])).
% 0.25/0.37 thf(c_0_5, plain, ![X3:sum_su1965225555um_c_b, X4:a]:(((epred6_0 @ X3)|~((member_a @ X4 @ (static_SIGT_a_b @ theta_1)))|((X3)!=(sum_In811702836um_c_b @ X4)))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.37 thf(c_0_6, plain, ![X1392:sum_su1965225555um_c_b, X1394:sum_su1965225555um_c_b, X1395:a]:((((((X1392)=(sum_In811702836um_c_b @ (esk24_1 @ X1392)))|~(epred1_0 @ X1392))&((member_a @ (esk24_1 @ X1392) @ (static_SIGT_a_b @ theta_1))|~(epred1_0 @ X1392)))&(((X1394)!=(sum_In811702836um_c_b @ X1395))|~(member_a @ X1395 @ (static_SIGT_a_b @ theta_1))|(epred1_0 @ X1394)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[])])])])])])])).
% 0.25/0.37 thf(c_0_7, negated_conjecture, ~((denota896875430_a_c_b @ i @ j @ (collec1166375742um_c_b @ (^[X3:sum_su1965225555um_c_b]:(?[X4:a]:(((((X3)=(sum_In811702836um_c_b @ X4)))&((member_a @ X4 @ (static_SIGT_a_b @ theta_1)))))))))), inference(assume_negation,[status(cth)],[conj_0])).
% 0.25/0.37 thf(c_0_8, plain, ![X4:a]:(((epred6_0 @ (sum_In811702836um_c_b @ X4))|~((member_a @ X4 @ (static_SIGT_a_b @ theta_1))))), inference(er,[status(thm)],[c_0_5])).
% 0.25/0.37 thf(c_0_9, plain, ![X3:sum_su1965225555um_c_b]:(((member_a @ (esk24_1 @ X3) @ (static_SIGT_a_b @ theta_1))|~((epred1_0 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.25/0.37 thf(c_0_10, negated_conjecture, ~(denota896875430_a_c_b @ i @ j @ (collec1166375742um_c_b @ (^[Z0:sum_su1965225555um_c_b]:(?[X4:a]:(((((Z0)=(sum_In811702836um_c_b @ X4)))&((member_a @ X4 @ (static_SIGT_a_b @ theta_1))))))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_7])])).
% 0.25/0.37 thf(c_0_11, plain, (denota896875430_a_c_b @ i @ j @ (collec1166375742um_c_b @ (^[Z0:sum_su1965225555um_c_b]:(?[X4:a]:(((((Z0)=(sum_In811702836um_c_b @ X4)))&((((member_a @ X4 @ (static_SIGT_a_b @ theta_1)))|((member_a @ X4 @ (static_SIGT_a_b @ theta_2))))))))))), inference(fof_simplification,[status(thm)],[fact_2_IA])).
% 0.25/0.37 thf(c_0_12, plain, ![X1367:sum_su1965225555um_c_b]:(((epred6_0 @ X1367)<=>?[X1366:a]:((((X1367)=(sum_In811702836um_c_b @ X1366))&((member_a @ X1366 @ (static_SIGT_a_b @ theta_1))|(member_a @ X1366 @ (static_SIGT_a_b @ theta_2))))))), introduced(definition)).
% 0.25/0.37 thf(c_0_13, plain, ![X1077:sum_su1965225555um_c_b > $o, X1078:sum_su1965225555um_c_b > $o]:((((X1077 @ (esk2_2 @ X1077 @ X1078))|(ord_le1404954451um_c_b @ (collec1166375742um_c_b @ X1077) @ (collec1166375742um_c_b @ X1078)))&(~(X1078 @ (esk2_2 @ X1077 @ X1078))|(ord_le1404954451um_c_b @ (collec1166375742um_c_b @ X1077) @ (collec1166375742um_c_b @ X1078))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_178_Collect__mono])])])])])).
% 0.25/0.37 thf(c_0_14, plain, ![X3:sum_su1965225555um_c_b]:(((epred6_0 @ (sum_In811702836um_c_b @ (esk24_1 @ X3)))|~((epred1_0 @ X3)))), inference(spm,[status(thm)],[c_0_8, c_0_9])).
% 0.25/0.37 thf(c_0_15, plain, ![X3:sum_su1965225555um_c_b]:((((X3)=(sum_In811702836um_c_b @ (esk24_1 @ X3)))|~((epred1_0 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.25/0.37 thf(c_0_16, negated_conjecture, ~(denota896875430_a_c_b @ i @ j @ (collec1166375742um_c_b @ (^[Z0:sum_su1965225555um_c_b]:(?[X4:a]:(((((Z0)=(sum_In811702836um_c_b @ X4)))&((member_a @ X4 @ (static_SIGT_a_b @ theta_1))))))))), inference(fof_nnf,[status(thm)],[c_0_10])).
% 0.25/0.37 thf(c_0_17, plain, ![X1345:sum_su1965225555um_c_b]:(((epred1_0 @ X1345)<=>?[X1344:a]:((((X1345)=(sum_In811702836um_c_b @ X1344))&(member_a @ X1344 @ (static_SIGT_a_b @ theta_1)))))), introduced(definition)).
% 0.25/0.37 thf(c_0_18, plain, ![X1070:set_Su111624115um_c_b, X1071:set_Su111624115um_c_b, X1072:denota723907260t_unit, X1073:denota723907260t_unit]:((~(ord_le1404954451um_c_b @ X1070 @ X1071)|(~(denota896875430_a_c_b @ X1072 @ X1073 @ X1071)|(denota896875430_a_c_b @ X1072 @ X1073 @ X1070)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_52_Iagree__sub])])])).
% 0.25/0.37 thf(c_0_19, plain, (((denota896875430_a_c_b @ i @ j @ (collec1166375742um_c_b @ epred6_0)))=(($true))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_11]), c_0_12])).
% 0.25/0.37 thf(c_0_20, plain, ![X137:sum_su1965225555um_c_b > $o, X110:sum_su1965225555um_c_b > $o]:(((ord_le1404954451um_c_b @ (collec1166375742um_c_b @ X137) @ (collec1166375742um_c_b @ X110))|~((X110 @ (esk2_2 @ X137 @ X110))))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.25/0.37 thf(c_0_21, plain, ![X3:sum_su1965225555um_c_b]:(((epred6_0 @ X3)|~((epred1_0 @ X3)))), inference(spm,[status(thm)],[c_0_14, c_0_15])).
% 0.25/0.37 thf(c_0_22, negated_conjecture, ~((((denota896875430_a_c_b @ i @ j @ (collec1166375742um_c_b @ epred1_0)))=(($true)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_16]), c_0_17])).
% 0.25/0.37 thf(c_0_23, plain, ![X1:denota723907260t_unit, X2:denota723907260t_unit, X11:set_Su111624115um_c_b, X12:set_Su111624115um_c_b]:(((denota896875430_a_c_b @ X1 @ X2 @ X11)|~((ord_le1404954451um_c_b @ X11 @ X12))|~((denota896875430_a_c_b @ X1 @ X2 @ X12)))), inference(split_conjunct,[status(thm)],[c_0_18])).
% 0.25/0.37 thf(c_0_24, plain, (denota896875430_a_c_b @ i @ j @ (collec1166375742um_c_b @ epred6_0)), inference(cn,[status(thm)],[c_0_19])).
% 0.25/0.37 thf(c_0_25, plain, ![X110:sum_su1965225555um_c_b > $o]:(((ord_le1404954451um_c_b @ (collec1166375742um_c_b @ X110) @ (collec1166375742um_c_b @ epred6_0))|~((epred1_0 @ (esk2_2 @ X110 @ epred6_0))))), inference(spm,[status(thm)],[c_0_20, c_0_21])).
% 0.25/0.37 thf(c_0_26, plain, ![X110:sum_su1965225555um_c_b > $o, X137:sum_su1965225555um_c_b > $o]:(((X110 @ (esk2_2 @ X110 @ X137))|(ord_le1404954451um_c_b @ (collec1166375742um_c_b @ X110) @ (collec1166375742um_c_b @ X137)))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.25/0.37 thf(c_0_27, negated_conjecture, ~((denota896875430_a_c_b @ i @ j @ (collec1166375742um_c_b @ epred1_0))), inference(cn,[status(thm)],[c_0_22])).
% 0.25/0.37 thf(c_0_28, plain, ![X11:set_Su111624115um_c_b]:(((denota896875430_a_c_b @ i @ j @ X11)|~((ord_le1404954451um_c_b @ X11 @ (collec1166375742um_c_b @ epred6_0))))), inference(spm,[status(thm)],[c_0_23, c_0_24])).
% 0.25/0.37 thf(c_0_29, plain, (ord_le1404954451um_c_b @ (collec1166375742um_c_b @ epred1_0) @ (collec1166375742um_c_b @ epred6_0)), inference(spm,[status(thm)],[c_0_25, c_0_26])).
% 0.25/0.37 thf(c_0_30, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_28]), c_0_29])]), ['proof']).
% 0.25/0.37 % SZS output end CNFRefutation
% 0.25/0.37 % Parsed axioms : 482
% 0.25/0.37 % Removed by relevancy pruning/SinE : 365
% 0.25/0.37 % Initial clauses : 182
% 0.25/0.37 % Removed in clause preprocessing : 6
% 0.25/0.37 % Initial clauses in saturation : 176
% 0.25/0.37 % Processed clauses : 421
% 0.25/0.37 % ...of these trivial : 12
% 0.25/0.37 % ...subsumed : 216
% 0.25/0.37 % ...remaining for further processing : 193
% 0.25/0.37 % Other redundant clauses eliminated : 34
% 0.25/0.37 % Clauses deleted for lack of memory : 0
% 0.25/0.37 % Backward-subsumed : 1
% 0.25/0.37 % Backward-rewritten : 2
% 0.25/0.37 % Generated clauses : 787
% 0.25/0.37 % ...of the previous two non-redundant : 489
% 0.25/0.37 % ...aggressively subsumed : 0
% 0.25/0.37 % Contextual simplify-reflections : 5
% 0.25/0.37 % Paramodulations : 750
% 0.25/0.37 % Factorizations : 2
% 0.25/0.37 % NegExts : 0
% 0.25/0.37 % Equation resolutions : 35
% 0.25/0.37 % Disequality decompositions : 0
% 0.25/0.37 % Total rewrite steps : 234
% 0.25/0.37 % ...of those cached : 168
% 0.25/0.37 % Propositional unsat checks : 0
% 0.25/0.37 % Propositional check models : 0
% 0.25/0.37 % Propositional check unsatisfiable : 0
% 0.25/0.37 % Propositional clauses : 0
% 0.25/0.37 % Propositional clauses after purity: 0
% 0.25/0.37 % Propositional unsat core size : 0
% 0.25/0.37 % Propositional preprocessing time : 0.000
% 0.25/0.37 % Propositional encoding time : 0.000
% 0.25/0.37 % Propositional solver time : 0.000
% 0.25/0.37 % Success case prop preproc time : 0.000
% 0.25/0.37 % Success case prop encoding time : 0.000
% 0.25/0.37 % Success case prop solver time : 0.000
% 0.25/0.37 % Current number of processed clauses : 172
% 0.25/0.37 % Positive orientable unit clauses : 50
% 0.25/0.37 % Positive unorientable unit clauses: 0
% 0.25/0.37 % Negative unit clauses : 1
% 0.25/0.37 % Non-unit-clauses : 121
% 0.25/0.37 % Current number of unprocessed clauses: 242
% 0.25/0.37 % ...number of literals in the above : 571
% 0.25/0.37 % Current number of archived formulas : 0
% 0.25/0.37 % Current number of archived clauses : 6
% 0.25/0.37 % Clause-clause subsumption calls (NU) : 4553
% 0.25/0.37 % Rec. Clause-clause subsumption calls : 4401
% 0.25/0.37 % Non-unit clause-clause subsumptions : 222
% 0.25/0.37 % Unit Clause-clause subsumption calls : 22
% 0.25/0.37 % Rewrite failures with RHS unbound : 0
% 0.25/0.37 % BW rewrite match attempts : 52
% 0.25/0.37 % BW rewrite match successes : 1
% 0.25/0.37 % Condensation attempts : 0
% 0.25/0.37 % Condensation successes : 0
% 0.25/0.37 % Termbank termtop insertions : 24411
% 0.25/0.37 % Search garbage collected termcells : 5761
% 0.25/0.37
% 0.25/0.37 % -------------------------------------------------
% 0.25/0.37 % User time : 0.038 s
% 0.25/0.37 % System time : 0.009 s
% 0.25/0.37 % Total time : 0.047 s
% 0.25/0.37 % Maximum resident set size: 5108 pages
% 0.25/0.37
% 0.25/0.37 % -------------------------------------------------
% 0.25/0.37 % User time : 0.062 s
% 0.25/0.37 % System time : 0.019 s
% 0.25/0.37 % Total time : 0.080 s
% 0.25/0.37 % Maximum resident set size: 5632 pages
% 0.25/0.37 % E exiting
%------------------------------------------------------------------------------