%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEU821^2 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.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:25:46 AM UTC 2026
% Result : Theorem 0.24s 0.27s
% Output : CNFRefutation 0.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU821^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n019.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 14:34:48 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running higher-order theorem proving
% 0.08/0.25 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.YPJosYD686/E---3.1_868188.p
% 0.24/0.27 % Version: 3.5.1-ho
% 0.24/0.27 % Preprocessing class: HSSSSMSSSLSNSFN.
% 0.24/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.24/0.27 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.24/0.27 % Starting post_as_ho5 with 300s (1) cores
% 0.24/0.27 % Starting sh4l with 300s (1) cores
% 0.24/0.27 % Starting ho_unfolding_2 with 300s (1) cores
% 0.24/0.27 % sh4l with pid 868225 completed with status 0
% 0.24/0.27 % Result found by sh4l
% 0.24/0.27 % Preprocessing class: HSSSSMSSSLSNSFN.
% 0.24/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.24/0.27 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.24/0.27 % Starting post_as_ho5 with 300s (1) cores
% 0.24/0.27 % Starting sh4l with 300s (1) cores
% 0.24/0.27 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 1, sine = Auto)
% 0.24/0.27 % No SInE strategy applied
% 0.24/0.27 % Search class: HGHSF-FFSS21-SSFFMFNN
% 0.24/0.27 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.24/0.27 % Starting SubtermCWHack with 28s (1) cores
% 0.24/0.27 % SubtermCWHack with pid 868232 completed with status 0
% 0.24/0.27 % Result found by SubtermCWHack
% 0.24/0.27 % Preprocessing class: HSSSSMSSSLSNSFN.
% 0.24/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.24/0.27 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.24/0.27 % Starting post_as_ho5 with 300s (1) cores
% 0.24/0.27 % Starting sh4l with 300s (1) cores
% 0.24/0.27 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 1, sine = Auto)
% 0.24/0.27 % No SInE strategy applied
% 0.24/0.27 % Search class: HGHSF-FFSS21-SSFFMFNN
% 0.24/0.27 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.24/0.27 % Starting SubtermCWHack with 28s (1) cores
% 0.24/0.27 % Preprocessing time : 0.001 s
% 0.24/0.27
% 0.24/0.27 % Proof found!
% 0.24/0.27 % SZS status Theorem
% 0.24/0.27 % SZS output start CNFRefutation
% 0.24/0.27 thf(decl_23, type, in: $i > $i > $o).
% 0.24/0.27 thf(decl_24, type, powerset: $i > $i).
% 0.24/0.27 thf(decl_25, type, nonempty: $i > $o).
% 0.24/0.27 thf(decl_26, type, transitiveset: $i > $o).
% 0.24/0.27 thf(decl_27, type, stricttotalorderedByIn: $i > $o).
% 0.24/0.27 thf(decl_28, type, wellorderedByIn: $i > $o).
% 0.24/0.27 thf(decl_29, type, ordinal: $i > $o).
% 0.24/0.27 thf(decl_30, type, epred1_1: $i > $o).
% 0.24/0.27 thf(decl_31, type, esk1_0: $i).
% 0.24/0.27 thf(decl_32, type, esk2_0: $i).
% 0.24/0.27 thf(decl_33, type, esk3_2: $i > $i > $i).
% 0.24/0.27 thf(wellorderedByIn, axiom, ((wellorderedByIn)=(^[X1:$i]:((((stricttotalorderedByIn @ X1))&(![X3:$i]:((((in @ X3 @ (powerset @ X1)))=>((((nonempty @ X3))=>(?[X2:$i]:((((in @ X2 @ X3))&(![X4:$i]:((((in @ X4 @ X3))=>(((((X2)=(X4)))|((in @ X2 @ X4))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.YPJosYD686/E---3.1_868188.p', wellorderedByIn)).
% 0.24/0.27 thf(stricttotalorderedByIn, axiom, ((stricttotalorderedByIn)=(^[X1:$i]:(((((![X2:$i]:((((in @ X2 @ X1))=>(![X3:$i]:((((in @ X3 @ X1))=>(![X4:$i]:((((in @ X4 @ X1))=>((((((in @ X2 @ X3))&((in @ X3 @ X4))))=>((in @ X2 @ X4)))))))))))))&(![X3:$i]:((((in @ X3 @ X1))=>(![X4:$i]:((((in @ X4 @ X1))=>(((((((X3)=(X4)))|((in @ X3 @ X4))))|((in @ X4 @ X3))))))))))))&(![X3:$i]:((((in @ X3 @ X1))=>(~((in @ X3 @ X3)))))))))), file('/export/starexec/sandbox2/tmp/tmp.YPJosYD686/E---3.1_868188.p', stricttotalorderedByIn)).
% 0.24/0.27 thf(ordinal, axiom, ((ordinal)=(^[X2:$i]:((((transitiveset @ X2))&((wellorderedByIn @ X2)))))), file('/export/starexec/sandbox2/tmp/tmp.YPJosYD686/E---3.1_868188.p', ordinal)).
% 0.24/0.27 thf(ordinalIrrefl, conjecture, ![X3:$i]:(((ordinal @ X3)=>![X1:$i]:(((in @ X1 @ X3)=>~((in @ X1 @ X1)))))), file('/export/starexec/sandbox2/tmp/tmp.YPJosYD686/E---3.1_868188.p', ordinalIrrefl)).
% 0.24/0.27 thf(c_0_4, plain, ((wellorderedByIn)=(^[Z0:$i]:((((((((![X7:$i]:((((in @ X7 @ Z0))=>(![X8:$i]:((((in @ X8 @ Z0))=>(![X9:$i]:((((in @ X9 @ Z0))=>((((((in @ X7 @ X8))&((in @ X8 @ X9))))=>((in @ X7 @ X9)))))))))))))&(![X10:$i]:((((in @ X10 @ Z0))=>(![X11:$i]:((((in @ X11 @ Z0))=>(((((((X10)=(X11)))|((in @ X10 @ X11))))|((in @ X11 @ X10))))))))))))&(![X12:$i]:((((in @ X12 @ Z0))=>(~((in @ X12 @ X12)))))))))&(![X3:$i]:((((in @ X3 @ (powerset @ Z0)))=>((((nonempty @ X3))=>(?[X2:$i]:((((in @ X2 @ X3))&(![X4:$i]:((((in @ X4 @ X3))=>(((((X2)=(X4)))|((in @ X2 @ X4))))))))))))))))))), inference(fof_simplification,[status(thm)],[wellorderedByIn])).
% 0.24/0.27 thf(c_0_5, plain, ((stricttotalorderedByIn)=(^[Z0:$i]:(((((![X2:$i]:((((in @ X2 @ Z0))=>(![X3:$i]:((((in @ X3 @ Z0))=>(![X4:$i]:((((in @ X4 @ Z0))=>((((((in @ X2 @ X3))&((in @ X3 @ X4))))=>((in @ X2 @ X4)))))))))))))&(![X3:$i]:((((in @ X3 @ Z0))=>(![X4:$i]:((((in @ X4 @ Z0))=>(((((((X3)=(X4)))|((in @ X3 @ X4))))|((in @ X4 @ X3))))))))))))&(![X3:$i]:((((in @ X3 @ Z0))=>(~((in @ X3 @ X3)))))))))), inference(fof_simplification,[status(thm)],[stricttotalorderedByIn])).
% 0.24/0.27 thf(c_0_6, plain, ((ordinal)=(^[Z0:$i]:((((transitiveset @ Z0))&(((((((((![X13:$i]:((((in @ X13 @ Z0))=>(![X14:$i]:((((in @ X14 @ Z0))=>(![X15:$i]:((((in @ X15 @ Z0))=>((((((in @ X13 @ X14))&((in @ X14 @ X15))))=>((in @ X13 @ X15)))))))))))))&(![X16:$i]:((((in @ X16 @ Z0))=>(![X17:$i]:((((in @ X17 @ Z0))=>(((((((X16)=(X17)))|((in @ X16 @ X17))))|((in @ X17 @ X16))))))))))))&(![X18:$i]:((((in @ X18 @ Z0))=>(~((in @ X18 @ X18)))))))))&(![X19:$i]:((((in @ X19 @ (powerset @ Z0)))=>((((nonempty @ X19))=>(?[X20:$i]:((((in @ X20 @ X19))&(![X21:$i]:((((in @ X21 @ X19))=>(((((X20)=(X21)))|((in @ X20 @ X21)))))))))))))))))))))), inference(fof_simplification,[status(thm)],[ordinal])).
% 0.24/0.27 thf(c_0_7, plain, ((wellorderedByIn)=(^[Z0:$i]:((((((((![X7:$i]:((((in @ X7 @ Z0))=>(![X8:$i]:((((in @ X8 @ Z0))=>(![X9:$i]:((((in @ X9 @ Z0))=>((((((in @ X7 @ X8))&((in @ X8 @ X9))))=>((in @ X7 @ X9)))))))))))))&(![X10:$i]:((((in @ X10 @ Z0))=>(![X11:$i]:((((in @ X11 @ Z0))=>(((((((X10)=(X11)))|((in @ X10 @ X11))))|((in @ X11 @ X10))))))))))))&(![X12:$i]:((((in @ X12 @ Z0))=>(~((in @ X12 @ X12)))))))))&(![X3:$i]:((((in @ X3 @ (powerset @ Z0)))=>((((nonempty @ X3))=>(?[X2:$i]:((((in @ X2 @ X3))&(![X4:$i]:((((in @ X4 @ X3))=>(((((X2)=(X4)))|((in @ X2 @ X4))))))))))))))))))), inference(apply_def,[status(thm)],[c_0_4, c_0_5])).
% 0.24/0.27 thf(c_0_8, plain, ![X3:$i]:(((epred1_1 @ X3)<=>((transitiveset @ X3)&(((![X22:$i]:(((in @ X22 @ X3)=>![X23:$i]:(((in @ X23 @ X3)=>![X24:$i]:(((in @ X24 @ X3)=>(((in @ X22 @ X23)&(in @ X23 @ X24))=>(in @ X22 @ X24))))))))&![X25:$i]:(((in @ X25 @ X3)=>![X26:$i]:(((in @ X26 @ X3)=>(((X25)=(X26))|(in @ X25 @ X26)|(in @ X26 @ X25)))))))&![X27:$i]:(((in @ X27 @ X3)=>~(in @ X27 @ X27))))&![X28:$i]:(((in @ X28 @ (powerset @ X3))=>((nonempty @ X28)=>?[X29:$i]:(((in @ X29 @ X28)&![X30:$i]:(((in @ X30 @ X28)=>(((X29)=(X30))|(in @ X29 @ X30))))))))))))), introduced(definition)).
% 0.24/0.27 thf(c_0_9, negated_conjecture, ~(![X3:$i]:(((ordinal @ X3)=>![X1:$i]:(((in @ X1 @ X3)=>~((in @ X1 @ X1))))))), inference(assume_negation,[status(cth)],[ordinalIrrefl])).
% 0.24/0.27 thf(c_0_10, plain, ((ordinal)=(^[Z0:$i]:((((transitiveset @ Z0))&(((((((((![X13:$i]:((((in @ X13 @ Z0))=>(![X14:$i]:((((in @ X14 @ Z0))=>(![X15:$i]:((((in @ X15 @ Z0))=>((((((in @ X13 @ X14))&((in @ X14 @ X15))))=>((in @ X13 @ X15)))))))))))))&(![X16:$i]:((((in @ X16 @ Z0))=>(![X17:$i]:((((in @ X17 @ Z0))=>(((((((X16)=(X17)))|((in @ X16 @ X17))))|((in @ X17 @ X16))))))))))))&(![X18:$i]:((((in @ X18 @ Z0))=>(~((in @ X18 @ X18)))))))))&(![X19:$i]:((((in @ X19 @ (powerset @ Z0)))=>((((nonempty @ X19))=>(?[X20:$i]:((((in @ X20 @ X19))&(![X21:$i]:((((in @ X21 @ X19))=>(((((X20)=(X21)))|((in @ X20 @ X21)))))))))))))))))))))), inference(apply_def,[status(thm)],[c_0_6, c_0_7])).
% 0.24/0.27 thf(c_0_11, plain, ![X3:$i]:(((epred1_1 @ X3)=>((transitiveset @ X3)&(((![X22:$i]:(((in @ X22 @ X3)=>![X23:$i]:(((in @ X23 @ X3)=>![X24:$i]:(((in @ X24 @ X3)=>(((in @ X22 @ X23)&(in @ X23 @ X24))=>(in @ X22 @ X24))))))))&![X25:$i]:(((in @ X25 @ X3)=>![X26:$i]:(((in @ X26 @ X3)=>(((X25)=(X26))|(in @ X25 @ X26)|(in @ X26 @ X25)))))))&![X27:$i]:(((in @ X27 @ X3)=>~(in @ X27 @ X27))))&![X28:$i]:(((in @ X28 @ (powerset @ X3))=>((nonempty @ X28)=>?[X29:$i]:(((in @ X29 @ X28)&![X30:$i]:(((in @ X30 @ X28)=>(((X29)=(X30))|(in @ X29 @ X30))))))))))))), inference(split_equiv,[status(thm)],[c_0_8])).
% 0.24/0.27 thf(c_0_12, negated_conjecture, ~(![X3:$i]:(((epred1_1 @ X3)=>![X1:$i]:(((in @ X1 @ X3)=>~(in @ X1 @ X1)))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[c_0_9, c_0_10])]), c_0_8])).
% 0.24/0.27 thf(c_0_13, plain, ![X33:$i, X34:$i, X35:$i, X36:$i, X37:$i, X38:$i, X39:$i, X40:$i, X42:$i]:((((transitiveset @ X33)|~(epred1_1 @ X33))&((((~(in @ X34 @ X33)|(~(in @ X35 @ X33)|(~(in @ X36 @ X33)|(~(in @ X34 @ X35)|~(in @ X35 @ X36)|(in @ X34 @ X36))))|~(epred1_1 @ X33))&(~(in @ X37 @ X33)|(~(in @ X38 @ X33)|(((X37)=(X38))|(in @ X37 @ X38)|(in @ X38 @ X37)))|~(epred1_1 @ X33)))&(~(in @ X39 @ X33)|~(in @ X39 @ X39)|~(epred1_1 @ X33)))&(((in @ (esk3_2 @ X33 @ X40) @ X40)|~(nonempty @ X40)|~(in @ X40 @ (powerset @ X33))|~(epred1_1 @ X33))&(~(in @ X42 @ X40)|(((esk3_2 @ X33 @ X40)=(X42))|(in @ (esk3_2 @ X33 @ X40) @ X42))|~(nonempty @ X40)|~(in @ X40 @ (powerset @ X33))|~(epred1_1 @ X33)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_11])])])])])])).
% 0.24/0.27 thf(c_0_14, negated_conjecture, ((epred1_1 @ esk1_0)&((in @ esk2_0 @ esk1_0)&(in @ esk2_0 @ esk2_0))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_12])])])).
% 0.24/0.27 thf(c_0_15, plain, ![X1:$i, X2:$i]:((~((in @ X1 @ X2))|~((in @ X1 @ X1))|~((epred1_1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.24/0.27 thf(c_0_16, negated_conjecture, (in @ esk2_0 @ esk1_0), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.24/0.27 thf(c_0_17, negated_conjecture, (in @ esk2_0 @ esk2_0), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.24/0.27 thf(c_0_18, negated_conjecture, (epred1_1 @ esk1_0), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.24/0.27 thf(c_0_19, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_15, c_0_16]), c_0_17]), c_0_18])]), ['proof']).
% 0.24/0.27 % SZS output end CNFRefutation
% 0.24/0.27 % Parsed axioms : 11
% 0.24/0.27 % Removed by relevancy pruning/SinE : 0
% 0.24/0.27 % Initial clauses : 16
% 0.24/0.27 % Removed in clause preprocessing : 7
% 0.24/0.27 % Initial clauses in saturation : 9
% 0.24/0.27 % Processed clauses : 5
% 0.24/0.27 % ...of these trivial : 0
% 0.24/0.27 % ...subsumed : 0
% 0.24/0.27 % ...remaining for further processing : 5
% 0.24/0.27 % Other redundant clauses eliminated : 0
% 0.24/0.27 % Clauses deleted for lack of memory : 0
% 0.24/0.27 % Backward-subsumed : 0
% 0.24/0.27 % Backward-rewritten : 0
% 0.24/0.27 % Generated clauses : 2
% 0.24/0.27 % ...of the previous two non-redundant : 1
% 0.24/0.27 % ...aggressively subsumed : 0
% 0.24/0.27 % Contextual simplify-reflections : 0
% 0.24/0.27 % Paramodulations : 2
% 0.24/0.27 % Factorizations : 0
% 0.24/0.27 % NegExts : 0
% 0.24/0.27 % Equation resolutions : 0
% 0.24/0.27 % Disequality decompositions : 0
% 0.24/0.27 % Total rewrite steps : 3
% 0.24/0.27 % ...of those cached : 1
% 0.24/0.27 % Propositional unsat checks : 0
% 0.24/0.27 % Propositional check models : 0
% 0.24/0.27 % Propositional check unsatisfiable : 0
% 0.24/0.27 % Propositional clauses : 0
% 0.24/0.27 % Propositional clauses after purity: 0
% 0.24/0.27 % Propositional unsat core size : 0
% 0.24/0.27 % Propositional preprocessing time : 0.000
% 0.24/0.27 % Propositional encoding time : 0.000
% 0.24/0.27 % Propositional solver time : 0.000
% 0.24/0.27 % Success case prop preproc time : 0.000
% 0.24/0.27 % Success case prop encoding time : 0.000
% 0.24/0.27 % Success case prop solver time : 0.000
% 0.24/0.27 % Current number of processed clauses : 5
% 0.24/0.27 % Positive orientable unit clauses : 3
% 0.24/0.27 % Positive unorientable unit clauses: 0
% 0.24/0.27 % Negative unit clauses : 0
% 0.24/0.27 % Non-unit-clauses : 2
% 0.24/0.27 % Current number of unprocessed clauses: 4
% 0.24/0.27 % ...number of literals in the above : 23
% 0.24/0.27 % Current number of archived formulas : 0
% 0.24/0.27 % Current number of archived clauses : 0
% 0.24/0.27 % Clause-clause subsumption calls (NU) : 0
% 0.24/0.27 % Rec. Clause-clause subsumption calls : 0
% 0.24/0.27 % Non-unit clause-clause subsumptions : 0
% 0.24/0.27 % Unit Clause-clause subsumption calls : 0
% 0.24/0.27 % Rewrite failures with RHS unbound : 0
% 0.24/0.27 % BW rewrite match attempts : 0
% 0.24/0.27 % BW rewrite match successes : 0
% 0.24/0.27 % Condensation attempts : 0
% 0.24/0.27 % Condensation successes : 0
% 0.24/0.27 % Termbank termtop insertions : 1337
% 0.24/0.27 % Search garbage collected termcells : 300
% 0.24/0.27
% 0.24/0.27 % -------------------------------------------------
% 0.24/0.27 % User time : 0.006 s
% 0.24/0.27 % System time : 0.001 s
% 0.24/0.27 % Total time : 0.007 s
% 0.24/0.27 % Maximum resident set size: 3896 pages
% 0.24/0.27
% 0.24/0.27 % -------------------------------------------------
% 0.24/0.27 % User time : 0.006 s
% 0.24/0.27 % System time : 0.007 s
% 0.24/0.27 % Total time : 0.013 s
% 0.24/0.27 % Maximum resident set size: 4864 pages
% 0.24/0.27 % E exiting
%------------------------------------------------------------------------------