%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : ITP116^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 : n007.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:34 AM UTC 2026
% Result : Theorem 0.43s 0.44s
% Output : CNFRefutation 0.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP116^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n007.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 19:53:56 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running higher-order theorem proving
% 0.23/0.29 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.FXHecFXbGl/E---3.1_3847259.p
% 0.43/0.44 % Version: 3.5.1-ho
% 0.43/0.44 % Preprocessing class: HSLSSMSSSSLCHSA.
% 0.43/0.44 % Scheduled 5 strats onto 8 cores with 300 seconds (2400 total)
% 0.43/0.44 % Starting sh2 with 1200s (4) cores
% 0.43/0.44 % Starting full_lambda_3 with 300s (1) cores
% 0.43/0.44 % Starting ehoh_best7_lambda with 300s (1) cores
% 0.43/0.44 % Starting post_as_ho9 with 300s (1) cores
% 0.43/0.44 % Starting almost_fo_4 with 300s (1) cores
% 0.43/0.44 % sh2 with pid 3847299 completed with status 0
% 0.43/0.44 % Result found by sh2
% 0.43/0.44 % Preprocessing class: HSLSSMSSSSLCHSA.
% 0.43/0.44 % Scheduled 5 strats onto 8 cores with 300 seconds (2400 total)
% 0.43/0.44 % Starting sh2 with 1200s (4) cores
% 0.43/0.44 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.43/0.44 % No SInE strategy applied
% 0.43/0.44 % Search class: HGHSM-FSLS32-MHSFFSBN
% 0.43/0.44 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 0.43/0.44 % Starting SubtermCWHack with 109s (1) cores
% 0.43/0.44 % Starting sh2 with 121s (1) cores
% 0.43/0.44 % Starting new_ho_4 with 109s (1) cores
% 0.43/0.44 % Starting pre_casc_6 with 109s (1) cores
% 0.43/0.44 % sh2 with pid 3847320 completed with status 0
% 0.43/0.44 % Result found by sh2
% 0.43/0.44 % Preprocessing class: HSLSSMSSSSLCHSA.
% 0.43/0.44 % Scheduled 5 strats onto 8 cores with 300 seconds (2400 total)
% 0.43/0.44 % Starting sh2 with 1200s (4) cores
% 0.43/0.44 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.43/0.44 % No SInE strategy applied
% 0.43/0.44 % Search class: HGHSM-FSLS32-MHSFFSBN
% 0.43/0.44 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 0.43/0.44 % Starting SubtermCWHack with 109s (1) cores
% 0.43/0.44 % Starting sh2 with 121s (1) cores
% 0.43/0.44 % Preprocessing time : 0.012 s
% 0.43/0.44 % Presaturation interreduction done
% 0.43/0.44
% 0.43/0.44 % Proof found!
% 0.43/0.44 % SZS status Theorem
% 0.43/0.44 % SZS output start CNFRefutation
% 0.43/0.44 thf(decl_sort1, type, finite1489363574real_n: $tType).
% 0.43/0.44 thf(decl_sort2, type, sigma_1466784463real_n: $tType).
% 0.43/0.44 thf(decl_sort3, type, set_Fi1058188332real_n: $tType).
% 0.43/0.44 thf(decl_sort4, type, set_se2111327970real_n: $tType).
% 0.43/0.44 thf(decl_sort5, type, finite964658038_int_n: $tType).
% 0.43/0.44 thf(decl_25, type, comple230862828real_n: sigma_1466784463real_n > sigma_1466784463real_n).
% 0.43/0.44 thf(decl_35, type, plus_p585657087real_n: finite1489363574real_n > finite1489363574real_n > finite1489363574real_n).
% 0.43/0.44 thf(decl_48, type, inf_in1974387902real_n: set_Fi1058188332real_n > set_Fi1058188332real_n > set_Fi1058188332real_n).
% 0.43/0.44 thf(decl_50, type, lebesg260170249real_n: sigma_1466784463real_n).
% 0.43/0.44 thf(decl_51, type, minkow1134813771n_real: finite964658038_int_n > finite1489363574real_n).
% 0.43/0.44 thf(decl_71, type, vimage1233683625real_n: (finite1489363574real_n > finite1489363574real_n) > set_Fi1058188332real_n > set_Fi1058188332real_n).
% 0.43/0.44 thf(decl_88, type, sigma_346513458real_n: sigma_1466784463real_n > set_Fi1058188332real_n > sigma_1466784463real_n).
% 0.43/0.44 thf(decl_91, type, sigma_1235138647real_n: sigma_1466784463real_n > set_se2111327970real_n).
% 0.43/0.44 thf(decl_94, type, sigma_476185326real_n: sigma_1466784463real_n > set_Fi1058188332real_n).
% 0.43/0.44 thf(decl_110, type, member223413699real_n: set_Fi1058188332real_n > set_se2111327970real_n > $o).
% 0.43/0.44 thf(decl_114, type, t: finite964658038_int_n > set_Fi1058188332real_n).
% 0.43/0.44 thf(decl_115, type, t2: finite964658038_int_n > set_Fi1058188332real_n).
% 0.43/0.44 thf(decl_116, type, a: finite964658038_int_n).
% 0.43/0.44 thf(decl_163, type, esk47_1: finite964658038_int_n > finite1489363574real_n > finite1489363574real_n).
% 0.43/0.44 thf(conj_0, conjecture, (member223413699real_n @ (vimage1233683625real_n @ (^[X3:finite1489363574real_n]:(plus_p585657087real_n @ X3 @ (minkow1134813771n_real @ a))) @ (t2 @ a)) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n))), file('/export/starexec/sandbox2/tmp/tmp.FXHecFXbGl/E---3.1_3847259.p', conj_0)).
% 0.43/0.44 thf(fact_4_T_H__altdef, axiom, ![X1:finite964658038_int_n]:(((t @ X1)=(vimage1233683625real_n @ (^[X3:finite1489363574real_n]:(plus_p585657087real_n @ X3 @ (minkow1134813771n_real @ X1))) @ (t2 @ X1)))), file('/export/starexec/sandbox2/tmp/tmp.FXHecFXbGl/E---3.1_3847259.p', fact_4_T_H__altdef)).
% 0.43/0.44 thf(fact_2__092_060open_062_092_060And_062a_O_AT_Aa_A_092_060in_062_Asets_Alebesgue_A_092_060Longrightarrow_062_A_I_092_060lambda_062x_O_Ax_A_L_Aof__int__vec_Aa_J_A_N_096_AT_Aa_A_092_060inter_062_Aspace_Alebesgue_A_092_060in_062_Asets_Alebesgue_092_060close_062, axiom, ![X1:finite964658038_int_n]:(((member223413699real_n @ (t2 @ X1) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n)))=>(member223413699real_n @ (inf_in1974387902real_n @ (vimage1233683625real_n @ (^[X3:finite1489363574real_n]:(plus_p585657087real_n @ X3 @ (minkow1134813771n_real @ X1))) @ (t2 @ X1)) @ (sigma_476185326real_n @ (comple230862828real_n @ lebesg260170249real_n))) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n))))), file('/export/starexec/sandbox2/tmp/tmp.FXHecFXbGl/E---3.1_3847259.p', fact_2__092_060open_062_092_060And_062a_O_AT_Aa_A_092_060in_062_Asets_Alebesgue_A_092_060Longrightarrow_062_A_I_092_060lambda_062x_O_Ax_A_L_Aof__int__vec_Aa_J_A_N_096_AT_Aa_A_092_060inter_062_Aspace_Alebesgue_A_092_060in_062_Asets_Alebesgue_092_060close_062)).
% 0.43/0.44 thf(fact_275_space__lebesgue__on, axiom, ![X138:set_Fi1058188332real_n]:(((sigma_476185326real_n @ (sigma_346513458real_n @ (comple230862828real_n @ lebesg260170249real_n) @ X138))=(X138))), file('/export/starexec/sandbox2/tmp/tmp.FXHecFXbGl/E---3.1_3847259.p', fact_275_space__lebesgue__on)).
% 0.43/0.44 thf(fact_268_space__restrict__space, axiom, ![X5:sigma_1466784463real_n, X626:set_Fi1058188332real_n]:(((sigma_476185326real_n @ (sigma_346513458real_n @ X5 @ X626))=(inf_in1974387902real_n @ X626 @ (sigma_476185326real_n @ X5)))), file('/export/starexec/sandbox2/tmp/tmp.FXHecFXbGl/E---3.1_3847259.p', fact_268_space__restrict__space)).
% 0.43/0.44 thf(fact_43_space__completion, axiom, ![X5:sigma_1466784463real_n]:(((sigma_476185326real_n @ (comple230862828real_n @ X5))=(sigma_476185326real_n @ X5))), file('/export/starexec/sandbox2/tmp/tmp.FXHecFXbGl/E---3.1_3847259.p', fact_43_space__completion)).
% 0.43/0.44 thf(fact_3__092_060open_062_092_060And_062a_O_AT_Aa_A_092_060in_062_Asets_Alebesgue_092_060close_062, axiom, ![X1:finite964658038_int_n]:((member223413699real_n @ (t2 @ X1) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n)))), file('/export/starexec/sandbox2/tmp/tmp.FXHecFXbGl/E---3.1_3847259.p', fact_3__092_060open_062_092_060And_062a_O_AT_Aa_A_092_060in_062_Asets_Alebesgue_092_060close_062)).
% 0.43/0.44 thf(c_0_7, negated_conjecture, ~((member223413699real_n @ (vimage1233683625real_n @ (^[X3:finite1489363574real_n]:(plus_p585657087real_n @ X3 @ (minkow1134813771n_real @ a))) @ (t2 @ a)) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n)))), inference(assume_negation,[status(cth)],[conj_0])).
% 0.43/0.44 thf(c_0_8, negated_conjecture, ~(member223413699real_n @ (vimage1233683625real_n @ (^[Z0:finite1489363574real_n]:(plus_p585657087real_n @ Z0 @ (minkow1134813771n_real @ a))) @ (t2 @ a)) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_7])])).
% 0.43/0.44 thf(c_0_9, negated_conjecture, ~(member223413699real_n @ (vimage1233683625real_n @ (^[Z0:finite1489363574real_n]:(plus_p585657087real_n @ Z0 @ (minkow1134813771n_real @ a))) @ (t2 @ a)) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n))), inference(fof_nnf,[status(thm)],[c_0_8])).
% 0.43/0.44 thf(c_0_10, plain, ![X2846:finite1489363574real_n, X1:finite964658038_int_n]:(((esk47_1 @ X1 @ X2846)=(plus_p585657087real_n @ X2846 @ (minkow1134813771n_real @ X1)))), introduced(definition)).
% 0.43/0.44 thf(c_0_11, plain, ![X1:finite964658038_int_n]:(((t @ X1)=(vimage1233683625real_n @ (^[Z0:finite1489363574real_n]:(plus_p585657087real_n @ Z0 @ (minkow1134813771n_real @ X1))) @ (t2 @ X1)))), inference(fof_simplification,[status(thm)],[fact_4_T_H__altdef])).
% 0.43/0.44 thf(c_0_12, plain, ![X1:finite964658038_int_n]:(((member223413699real_n @ (t2 @ X1) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n)))=>(member223413699real_n @ (inf_in1974387902real_n @ (vimage1233683625real_n @ (^[Z0:finite1489363574real_n]:(plus_p585657087real_n @ Z0 @ (minkow1134813771n_real @ X1))) @ (t2 @ X1)) @ (sigma_476185326real_n @ (comple230862828real_n @ lebesg260170249real_n))) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n))))), inference(fof_simplification,[status(thm)],[fact_2__092_060open_062_092_060And_062a_O_AT_Aa_A_092_060in_062_Asets_Alebesgue_A_092_060Longrightarrow_062_A_I_092_060lambda_062x_O_Ax_A_L_Aof__int__vec_Aa_J_A_N_096_AT_Aa_A_092_060inter_062_Aspace_Alebesgue_A_092_060in_062_Asets_Alebesgue_092_060close_062])).
% 0.43/0.44 thf(c_0_13, plain, ![X2667:set_Fi1058188332real_n]:(((sigma_476185326real_n @ (sigma_346513458real_n @ (comple230862828real_n @ lebesg260170249real_n) @ X2667))=(X2667))), inference(variable_rename,[status(thm)],[fact_275_space__lebesgue__on])).
% 0.43/0.44 thf(c_0_14, plain, ![X2645:sigma_1466784463real_n, X2646:set_Fi1058188332real_n]:(((sigma_476185326real_n @ (sigma_346513458real_n @ X2645 @ X2646))=(inf_in1974387902real_n @ X2646 @ (sigma_476185326real_n @ X2645)))), inference(variable_rename,[status(thm)],[fact_268_space__restrict__space])).
% 0.43/0.44 thf(c_0_15, plain, ![X1909:sigma_1466784463real_n]:(((sigma_476185326real_n @ (comple230862828real_n @ X1909))=(sigma_476185326real_n @ X1909))), inference(variable_rename,[status(thm)],[fact_43_space__completion])).
% 0.43/0.44 thf(c_0_16, negated_conjecture, ~((((member223413699real_n @ (vimage1233683625real_n @ (esk47_1 @ a) @ (t2 @ a)) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n))))=(($true)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_9]), c_0_10])).
% 0.43/0.44 thf(c_0_17, plain, ![X1798:finite964658038_int_n]:(((t @ X1798)=(vimage1233683625real_n @ (^[Z0:finite1489363574real_n]:(plus_p585657087real_n @ Z0 @ (minkow1134813771n_real @ X1798))) @ (t2 @ X1798)))), inference(variable_rename,[status(thm)],[c_0_11])).
% 0.43/0.44 thf(c_0_18, plain, ![X1796:finite964658038_int_n]:((~(member223413699real_n @ (t2 @ X1796) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n)))|(member223413699real_n @ (inf_in1974387902real_n @ (vimage1233683625real_n @ (^[Z0:finite1489363574real_n]:(plus_p585657087real_n @ Z0 @ (minkow1134813771n_real @ X1796))) @ (t2 @ X1796)) @ (sigma_476185326real_n @ (comple230862828real_n @ lebesg260170249real_n))) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_12])])])).
% 0.43/0.44 thf(c_0_19, plain, ![X4:set_Fi1058188332real_n]:(((sigma_476185326real_n @ (sigma_346513458real_n @ (comple230862828real_n @ lebesg260170249real_n) @ X4))=(X4))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.43/0.44 thf(c_0_20, plain, ![X4:set_Fi1058188332real_n, X5:sigma_1466784463real_n]:(((sigma_476185326real_n @ (sigma_346513458real_n @ X5 @ X4))=(inf_in1974387902real_n @ X4 @ (sigma_476185326real_n @ X5)))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.43/0.44 thf(c_0_21, plain, ![X5:sigma_1466784463real_n]:(((sigma_476185326real_n @ (comple230862828real_n @ X5))=(sigma_476185326real_n @ X5))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.43/0.44 thf(c_0_22, plain, ![X1797:finite964658038_int_n]:((member223413699real_n @ (t2 @ X1797) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n)))), inference(variable_rename,[status(thm)],[fact_3__092_060open_062_092_060And_062a_O_AT_Aa_A_092_060in_062_Asets_Alebesgue_092_060close_062])).
% 0.43/0.44 thf(c_0_23, negated_conjecture, ~((member223413699real_n @ (vimage1233683625real_n @ (esk47_1 @ a) @ (t2 @ a)) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n)))), inference(cn,[status(thm)],[c_0_16])).
% 0.43/0.44 thf(c_0_24, plain, ![X1:finite964658038_int_n]:(((t @ X1)=(vimage1233683625real_n @ (esk47_1 @ X1) @ (t2 @ X1)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_17]), c_0_10])).
% 0.43/0.44 thf(c_0_25, plain, ![X1:finite964658038_int_n]:(((((member223413699real_n @ (inf_in1974387902real_n @ (vimage1233683625real_n @ (esk47_1 @ X1) @ (t2 @ X1)) @ (sigma_476185326real_n @ (comple230862828real_n @ lebesg260170249real_n))) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n))))=(($true)))|~((member223413699real_n @ (t2 @ X1) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n)))))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_18]), c_0_10])).
% 0.43/0.44 thf(c_0_26, plain, ![X4:set_Fi1058188332real_n]:(((inf_in1974387902real_n @ X4 @ (sigma_476185326real_n @ lebesg260170249real_n))=(X4))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_19, c_0_20]), c_0_21])).
% 0.43/0.44 thf(c_0_27, plain, ![X1:finite964658038_int_n]:((member223413699real_n @ (t2 @ X1) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n)))), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.43/0.44 thf(c_0_28, negated_conjecture, ~((member223413699real_n @ (t @ a) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n)))), inference(rw,[status(thm)],[c_0_23, c_0_24])).
% 0.43/0.44 thf(c_0_29, plain, ![X1:finite964658038_int_n]:((member223413699real_n @ (t @ X1) @ (sigma_1235138647real_n @ (comple230862828real_n @ lebesg260170249real_n)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[c_0_25]), c_0_24]), c_0_21]), c_0_26]), c_0_27])])).
% 0.43/0.44 thf(c_0_30, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_29])]), ['proof']).
% 0.43/0.44 % SZS output end CNFRefutation
% 0.43/0.44 % Parsed axioms : 476
% 0.43/0.44 % Removed by relevancy pruning/SinE : 0
% 0.43/0.44 % Initial clauses : 857
% 0.43/0.44 % Removed in clause preprocessing : 127
% 0.43/0.44 % Initial clauses in saturation : 730
% 0.43/0.44 % Processed clauses : 332
% 0.43/0.44 % ...of these trivial : 11
% 0.43/0.44 % ...subsumed : 50
% 0.43/0.44 % ...remaining for further processing : 271
% 0.43/0.44 % Other redundant clauses eliminated : 21
% 0.43/0.44 % Clauses deleted for lack of memory : 0
% 0.43/0.44 % Backward-subsumed : 0
% 0.43/0.44 % Backward-rewritten : 4
% 0.43/0.44 % Generated clauses : 19
% 0.43/0.44 % ...of the previous two non-redundant : 5
% 0.43/0.44 % ...aggressively subsumed : 0
% 0.43/0.44 % Contextual simplify-reflections : 0
% 0.43/0.44 % Paramodulations : 0
% 0.43/0.44 % Factorizations : 0
% 0.43/0.44 % NegExts : 0
% 0.43/0.44 % Equation resolutions : 21
% 0.43/0.44 % Disequality decompositions : 0
% 0.43/0.44 % Total rewrite steps : 43
% 0.43/0.44 % ...of those cached : 14
% 0.43/0.44 % Propositional unsat checks : 0
% 0.43/0.44 % Propositional check models : 0
% 0.43/0.44 % Propositional check unsatisfiable : 0
% 0.43/0.44 % Propositional clauses : 0
% 0.43/0.44 % Propositional clauses after purity: 0
% 0.43/0.44 % Propositional unsat core size : 0
% 0.43/0.44 % Propositional preprocessing time : 0.000
% 0.43/0.44 % Propositional encoding time : 0.000
% 0.43/0.44 % Propositional solver time : 0.000
% 0.43/0.44 % Success case prop preproc time : 0.000
% 0.43/0.44 % Success case prop encoding time : 0.000
% 0.43/0.44 % Success case prop solver time : 0.000
% 0.43/0.44 % Current number of processed clauses : 248
% 0.43/0.44 % Positive orientable unit clauses : 70
% 0.43/0.44 % Positive unorientable unit clauses: 2
% 0.43/0.44 % Negative unit clauses : 3
% 0.43/0.44 % Non-unit-clauses : 173
% 0.43/0.44 % Current number of unprocessed clauses: 403
% 0.43/0.44 % ...number of literals in the above : 1011
% 0.43/0.44 % Current number of archived formulas : 0
% 0.43/0.44 % Current number of archived clauses : 4
% 0.43/0.44 % Clause-clause subsumption calls (NU) : 12008
% 0.43/0.44 % Rec. Clause-clause subsumption calls : 10367
% 0.43/0.44 % Non-unit clause-clause subsumptions : 47
% 0.43/0.44 % Unit Clause-clause subsumption calls : 225
% 0.43/0.44 % Rewrite failures with RHS unbound : 0
% 0.43/0.44 % BW rewrite match attempts : 26
% 0.43/0.44 % BW rewrite match successes : 19
% 0.43/0.44 % Condensation attempts : 0
% 0.43/0.44 % Condensation successes : 0
% 0.43/0.44 % Termbank termtop insertions : 71351
% 0.43/0.44 % Search garbage collected termcells : 16738
% 0.43/0.44
% 0.43/0.44 % -------------------------------------------------
% 0.43/0.44 % User time : 0.088 s
% 0.43/0.44 % System time : 0.016 s
% 0.43/0.44 % Total time : 0.104 s
% 0.43/0.44 % Maximum resident set size: 9076 pages
% 0.43/0.44
% 0.43/0.44 % -------------------------------------------------
% 0.43/0.44 % User time : 0.156 s
% 0.43/0.44 % System time : 0.054 s
% 0.43/0.44 % Total time : 0.210 s
% 0.43/0.44 % Maximum resident set size: 5888 pages
% 0.43/0.44 % E exiting
%------------------------------------------------------------------------------