%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEV167^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:35:08 AM UTC 2026
% Result : Theorem 13.96s 13.94s
% Output : CNFRefutation 13.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV167^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n006.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 15:17:54 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running higher-order theorem proving
% 0.09/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.U5fsROB8zN/E---3.1_853611.p
% 13.96/13.94 % Version: 3.5.1-ho
% 13.96/13.94 % Preprocessing class: HSSSSMSSSSLNHHA.
% 13.96/13.94 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 13.96/13.94 % Starting new_ho_10 with 600s (2) cores
% 13.96/13.94 % Starting sh5l with 600s (2) cores
% 13.96/13.94 % Starting new_bool_1 with 600s (2) cores
% 13.96/13.94 % Starting new_bool_2 with 600s (2) cores
% 13.96/13.94 % sh5l with pid 853625 completed with status 9
% 13.96/13.94 % new_bool_1 with pid 853626 completed with status 9
% 13.96/13.94 % new_bool_2 with pid 853627 completed with status 9
% 13.96/13.94 % new_ho_10 with pid 853624 completed with status 0
% 13.96/13.94 % Result found by new_ho_10
% 13.96/13.94 % Preprocessing class: HSSSSMSSSSLNHHA.
% 13.96/13.94 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 13.96/13.94 % Starting new_ho_10 with 600s (2) cores
% 13.96/13.94 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 13.96/13.94 % No SInE strategy applied
% 13.96/13.94 % Search class: HHHSS-FFSF00-SHHFFFNN
% 13.96/13.94 % partial match(1): HGHSS-FFSF00-SHHFFFNN
% 13.96/13.94 % Scheduled 7 strats onto 2 cores with 600 seconds (600 total)
% 13.96/13.94 % Starting SubtermCWHack with 55s (1) cores
% 13.96/13.94 % Starting new_ho_10 with 61s (1) cores
% 13.96/13.94 % new_ho_10 with pid 853635 completed with status 10
% 13.96/13.94 % Starting new_ho_8 with 55s (1) cores
% 13.96/13.94 % SubtermCWHack with pid 853632 completed with status 10
% 13.96/13.94 % Starting new_ho_4 with 55s (1) cores
% 13.96/13.94 % new_ho_4 with pid 853652 completed with status 0
% 13.96/13.94 % Result found by new_ho_4
% 13.96/13.94 % Preprocessing class: HSSSSMSSSSLNHHA.
% 13.96/13.94 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 13.96/13.94 % Starting new_ho_10 with 600s (2) cores
% 13.96/13.94 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 13.96/13.94 % No SInE strategy applied
% 13.96/13.94 % Search class: HHHSS-FFSF00-SHHFFFNN
% 13.96/13.94 % partial match(1): HGHSS-FFSF00-SHHFFFNN
% 13.96/13.94 % Scheduled 7 strats onto 2 cores with 600 seconds (600 total)
% 13.96/13.94 % Starting SubtermCWHack with 55s (1) cores
% 13.96/13.94 % Starting new_ho_10 with 61s (1) cores
% 13.96/13.94 % new_ho_10 with pid 853635 completed with status 10
% 13.96/13.94 % Starting new_ho_8 with 55s (1) cores
% 13.96/13.94 % SubtermCWHack with pid 853632 completed with status 10
% 13.96/13.94 % Starting new_ho_4 with 55s (1) cores
% 13.96/13.94 % Preprocessing time : 0.001 s
% 13.96/13.94 % Presaturation interreduction done
% 13.96/13.94
% 13.96/13.94 % Proof found!
% 13.96/13.94 % SZS status Theorem
% 13.96/13.94 % SZS output start CNFRefutation
% 13.96/13.94 thf(decl_sort1, type, a: $tType).
% 13.96/13.94 thf(decl_23, type, epred1_0: a > a > a > a > $o).
% 13.96/13.94 thf(decl_24, type, esk1_0: a).
% 13.96/13.94 thf(decl_25, type, esk2_0: a).
% 13.96/13.94 thf(decl_26, type, esk3_0: a).
% 13.96/13.94 thf(decl_27, type, esk4_0: a).
% 13.96/13.94 thf(decl_28, type, esk5_0: a > a > a).
% 13.96/13.94 thf(decl_29, type, esk6_0: a > a > a).
% 13.96/13.94 thf(cTHM189_pme, conjecture, ![X1:a > a > a > a > $o]:((![X2:(a > a > a) > a, X3:(a > a > a) > a]:(((X1 @ (X2 @ (^[X4:a, X5:a]:(X4))) @ (X2 @ (^[X4:a, X5:a]:(X5))) @ (X3 @ (^[X4:a, X5:a]:(X4))) @ (X3 @ (^[X4:a, X5:a]:(X5))))=>((X2)=(X3))))=>![X6:a, X7:a, X8:a, X9:a]:(((X1 @ X6 @ X7 @ X8 @ X9)=>(((X6)=(X8))&((X7)=(X9))))))), file('/export/starexec/sandbox2/tmp/tmp.U5fsROB8zN/E---3.1_853611.p', cTHM189_pme)).
% 13.96/13.94 thf(c_0_1, negated_conjecture, ~(![X1:a > a > a > a > $o]:((![X2:(a > a > a) > a, X3:(a > a > a) > a]:(((X1 @ (X2 @ (^[X4:a, X5:a]:(X4))) @ (X2 @ (^[X4:a, X5:a]:(X5))) @ (X3 @ (^[X4:a, X5:a]:(X4))) @ (X3 @ (^[X4:a, X5:a]:(X5))))=>((X2)=(X3))))=>![X6:a, X7:a, X8:a, X9:a]:(((X1 @ X6 @ X7 @ X8 @ X9)=>(((X6)=(X8))&((X7)=(X9)))))))), inference(assume_negation,[status(cth)],[cTHM189_pme])).
% 13.96/13.94 thf(c_0_2, negated_conjecture, ~(![X1:a > a > a > a > $o]:((![X2:(a > a > a) > a, X3:(a > a > a) > a]:(((X1 @ (X2 @ (^[Z0:a, Z1:a]:(Z0))) @ (X2 @ (^[Z0:a, Z1:a]:(Z1))) @ (X3 @ (^[Z0:a, Z1:a]:(Z0))) @ (X3 @ (^[Z0:a, Z1:a]:(Z1))))=>((X2)=(X3))))=>![X6:a, X7:a, X8:a, X9:a]:(((X1 @ X6 @ X7 @ X8 @ X9)=>(((X6)=(X8))&((X7)=(X9)))))))), inference(fof_simplification,[status(thm)],[c_0_1])).
% 13.96/13.94 thf(c_0_3, negated_conjecture, ![X18:(a > a > a) > a, X19:(a > a > a) > a]:(((~(epred1_0 @ (X18 @ (^[Z0:a, Z1:a]:(Z0))) @ (X18 @ (^[Z0:a, Z1:a]:(Z1))) @ (X19 @ (^[Z0:a, Z1:a]:(Z0))) @ (X19 @ (^[Z0:a, Z1:a]:(Z1))))|((X18)=(X19)))&((epred1_0 @ esk1_0 @ esk2_0 @ esk3_0 @ esk4_0)&(((esk1_0)!=(esk3_0))|((esk2_0)!=(esk4_0)))))), 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_2])])])])])).
% 13.96/13.94 thf(c_0_4, plain, ![X27:a, X26:a]:(((esk6_0 @ X26 @ X27)=(X27))), introduced(definition)).
% 13.96/13.94 thf(c_0_5, plain, ![X25:a, X24:a]:(((esk5_0 @ X24 @ X25)=(X24))), introduced(definition)).
% 13.96/13.94 thf(c_0_6, negated_conjecture, ![X2:(a > a > a) > a, X3:(a > a > a) > a]:((((X2)=(X3))|~((((epred1_0 @ (X2 @ esk5_0) @ (X2 @ esk6_0) @ (X3 @ esk5_0) @ (X3 @ esk6_0)))=(($true)))))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_4]), c_0_5]), c_0_4]), c_0_5])).
% 13.96/13.94 thf(c_0_7, plain, ![X34:a, X35:a]:(((esk6_0 @ X35 @ X34)=(X34))), inference(variable_rename,[status(thm)],[])).
% 13.96/13.94 thf(c_0_8, plain, ![X32:a, X33:a]:(((esk5_0 @ X33 @ X32)=(X33))), inference(variable_rename,[status(thm)],[])).
% 13.96/13.94 thf(c_0_9, negated_conjecture, ![X2:(a > a > a) > a, X3:(a > a > a) > a]:((((X2)=(X3))|~((epred1_0 @ (X2 @ esk5_0) @ (X2 @ esk6_0) @ (X3 @ esk5_0) @ (X3 @ esk6_0))))), inference(cn,[status(thm)],[c_0_6])).
% 13.96/13.94 thf(c_0_10, plain, ![X4:a, X5:a]:(((esk6_0 @ X4 @ X5)=(X5))), inference(split_conjunct,[status(thm)],[c_0_7])).
% 13.96/13.94 thf(c_0_11, plain, ![X5:a, X4:a]:(((esk5_0 @ X4 @ X5)=(X4))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 13.96/13.94 thf(c_0_12, plain, ![X3:(a > a > a) > a, X2:(a > a > a) > a, X11:(a > a > a) > a]:((((X2)=(^[Z0:a > a > a]:(Z0 @ (X3 @ Z0) @ (X11 @ Z0))))|~((epred1_0 @ (X2 @ esk5_0) @ (X2 @ esk6_0) @ (X3 @ esk5_0) @ (X11 @ esk6_0))))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_9, c_0_10]), c_0_11])).
% 13.96/13.94 thf(c_0_13, plain, ![X3:(a > a > a) > a, X2:(a > a > a) > a, X11:(a > a > a) > a, X12:(a > a > a) > a]:((((^[Z0:a > a > a]:(Z0 @ (X2 @ Z0) @ (X3 @ Z0)))=(^[Z0:a > a > a]:(Z0 @ (X11 @ Z0) @ (X12 @ Z0))))|~((epred1_0 @ (X2 @ esk5_0) @ (X3 @ esk6_0) @ (X11 @ esk5_0) @ (X12 @ esk6_0))))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_10]), c_0_11])).
% 13.96/13.94 thf(c_0_14, plain, ![X3:(a > a > a) > a, X2:(a > a > a) > a, X11:(a > a > a) > a, X36:a > a > a, X12:(a > a > a) > a]:((((X36 @ (X2 @ X36) @ (X3 @ X36))=(X36 @ (X11 @ X36) @ (X12 @ X36)))|~((epred1_0 @ (X2 @ esk5_0) @ (X3 @ esk6_0) @ (X11 @ esk5_0) @ (X12 @ esk6_0))))), inference(arg_cong,[status(thm)],[c_0_13])).
% 13.96/13.94 thf(c_0_15, negated_conjecture, (epred1_0 @ esk1_0 @ esk2_0 @ esk3_0 @ esk4_0), inference(split_conjunct,[status(thm)],[c_0_3])).
% 13.96/13.94 thf(c_0_16, negated_conjecture, (((esk1_0)!=(esk3_0))|((esk2_0)!=(esk4_0))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 13.96/13.94 thf(c_0_17, negated_conjecture, ![X36:a > a > a]:(((X36 @ esk1_0 @ esk2_0)=(X36 @ esk3_0 @ esk4_0))), inference(spm,[status(thm)],[c_0_14, c_0_15])).
% 13.96/13.94 thf(c_0_18, negated_conjecture, ((esk3_0)!=(esk1_0)), inference(spm,[status(thm)],[c_0_16, c_0_17])).
% 13.96/13.94 thf(c_0_19, negated_conjecture, ($false), inference(spm,[status(thm)],[c_0_18, c_0_17]), ['proof']).
% 13.96/13.94 % SZS output end CNFRefutation
% 13.96/13.94 % Parsed axioms : 2
% 13.96/13.94 % Removed by relevancy pruning/SinE : 0
% 13.96/13.94 % Initial clauses : 6
% 13.96/13.94 % Removed in clause preprocessing : 1
% 13.96/13.94 % Initial clauses in saturation : 5
% 13.96/13.94 % Processed clauses : 2406
% 13.96/13.94 % ...of these trivial : 0
% 13.96/13.94 % ...subsumed : 1976
% 13.96/13.94 % ...remaining for further processing : 430
% 13.96/13.94 % Other redundant clauses eliminated : 1743
% 13.96/13.94 % Clauses deleted for lack of memory : 0
% 13.96/13.94 % Backward-subsumed : 140
% 13.96/13.94 % Backward-rewritten : 0
% 13.96/13.94 % Generated clauses : 433067
% 13.96/13.94 % ...of the previous two non-redundant : 430667
% 13.96/13.94 % ...aggressively subsumed : 0
% 13.96/13.94 % Contextual simplify-reflections : 6
% 13.96/13.94 % Paramodulations : 431236
% 13.96/13.94 % Factorizations : 0
% 13.96/13.94 % NegExts : 0
% 13.96/13.94 % Equation resolutions : 1765
% 13.96/13.94 % Disequality decompositions : 0
% 13.96/13.94 % Total rewrite steps : 374408
% 13.96/13.94 % ...of those cached : 373503
% 13.96/13.94 % Propositional unsat checks : 0
% 13.96/13.94 % Propositional check models : 0
% 13.96/13.94 % Propositional check unsatisfiable : 0
% 13.96/13.94 % Propositional clauses : 0
% 13.96/13.94 % Propositional clauses after purity: 0
% 13.96/13.94 % Propositional unsat core size : 0
% 13.96/13.94 % Propositional preprocessing time : 0.000
% 13.96/13.94 % Propositional encoding time : 0.000
% 13.96/13.94 % Propositional solver time : 0.000
% 13.96/13.94 % Success case prop preproc time : 0.000
% 13.96/13.94 % Success case prop encoding time : 0.000
% 13.96/13.94 % Success case prop solver time : 0.000
% 13.96/13.94 % Current number of processed clauses : 285
% 13.96/13.94 % Positive orientable unit clauses : 3
% 13.96/13.94 % Positive unorientable unit clauses: 1
% 13.96/13.94 % Negative unit clauses : 1
% 13.96/13.94 % Non-unit-clauses : 280
% 13.96/13.94 % Current number of unprocessed clauses: 427908
% 13.96/13.94 % ...number of literals in the above : 1914217
% 13.96/13.94 % Current number of archived formulas : 0
% 13.96/13.94 % Current number of archived clauses : 145
% 13.96/13.94 % Clause-clause subsumption calls (NU) : 30483
% 13.96/13.94 % Rec. Clause-clause subsumption calls : 13667
% 13.96/13.94 % Non-unit clause-clause subsumptions : 2020
% 13.96/13.94 % Unit Clause-clause subsumption calls : 214
% 13.96/13.94 % Rewrite failures with RHS unbound : 0
% 13.96/13.94 % BW rewrite match attempts : 604
% 13.96/13.94 % BW rewrite match successes : 2
% 13.96/13.94 % Condensation attempts : 0
% 13.96/13.94 % Condensation successes : 0
% 13.96/13.94 % Termbank termtop insertions : 64435713
% 13.96/13.94 % Search garbage collected termcells : 138
% 13.96/13.94
% 13.96/13.94 % -------------------------------------------------
% 13.96/13.94 % User time : 13.172 s
% 13.96/13.94 % System time : 0.448 s
% 13.96/13.94 % Total time : 13.620 s
% 13.96/13.94 % Maximum resident set size: 3636 pages
% 13.96/13.94
% 13.96/13.94 % -------------------------------------------------
% 13.96/13.94 % User time : 26.464 s
% 13.96/13.94 % System time : 0.944 s
% 13.96/13.94 % Total time : 27.408 s
% 13.96/13.94 % Maximum resident set size: 4864 pages
% 13.96/13.94 % E exiting
%------------------------------------------------------------------------------