%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO556^1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:43:24 AM UTC 2026
% Result : Theorem 0.25s 0.35s
% Output : CNFRefutation 0.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO556^1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 % Computer : n014.cluster.edu
% 0.08/0.22 % Model : x86_64 x86_64
% 0.08/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.22 % Memory : 8046.5625MB
% 0.08/0.22 % OS : Linux 6.8.0-71-generic
% 0.08/0.22 % CPULimit : 300
% 0.08/0.22 % WCLimit : 300
% 0.08/0.22 % DateTime : Tue Sep 29 17:14:44 UTC 2026
% 0.08/0.22 % CPUTime :
% 0.08/0.22 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.29 Running higher-order theorem proving
% 0.25/0.30 Running: /export/starexec/sandbox/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/sandbox/tmp/tmp.LPLKO4a83o/E---3.1_2950106.p
% 0.25/0.35 % Version: 3.5.1-ho
% 0.25/0.35 % Preprocessing class: HSSSSMSSSSMCSSA.
% 0.25/0.35 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.25/0.35 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.25/0.35 % Starting ehoh_best_sine_rwall with 300s (1) cores
% 0.25/0.35 % Starting new_bool_3 with 300s (1) cores
% 0.25/0.35 % Starting new_bool_1 with 300s (1) cores
% 0.25/0.35 % ho_unfolding_3 with pid 2950119 completed with status 0
% 0.25/0.35 % Result found by ho_unfolding_3
% 0.25/0.35 % Preprocessing class: HSSSSMSSSSMCSSA.
% 0.25/0.35 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.25/0.35 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.25/0.35 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.25/0.35 % No SInE strategy applied
% 0.25/0.35 % Search class: HGHSF-FFSF11-MSSFFFBC
% 0.25/0.35 % partial match(3): HGHSF-FFSF11-SSSFFMBN
% 0.25/0.35 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.25/0.35 % Starting SubtermCWHack with 136s (1) cores
% 0.25/0.35 % Starting ho_unfolding_3 with 151s (1) cores
% 0.25/0.35 % Starting ehoh_best_sine_rwall with 136s (1) cores
% 0.25/0.35 % Starting sh2lt with 136s (1) cores
% 0.25/0.35 % Starting sh2l with 136s (1) cores
% 0.25/0.35 % SubtermCWHack with pid 2950124 completed with status 10
% 0.25/0.35 % Starting ehoh_best_sine with 136s (1) cores
% 0.25/0.35 % ehoh_best_sine_rwall with pid 2950126 completed with status 0
% 0.25/0.35 % Result found by ehoh_best_sine_rwall
% 0.25/0.35 % Preprocessing class: HSSSSMSSSSMCSSA.
% 0.25/0.35 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.25/0.35 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.25/0.35 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.25/0.35 % No SInE strategy applied
% 0.25/0.35 % Search class: HGHSF-FFSF11-MSSFFFBC
% 0.25/0.35 % partial match(3): HGHSF-FFSF11-SSSFFMBN
% 0.25/0.35 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.25/0.35 % Starting SubtermCWHack with 136s (1) cores
% 0.25/0.35 % Starting ho_unfolding_3 with 151s (1) cores
% 0.25/0.35 % Starting ehoh_best_sine_rwall with 136s (1) cores
% 0.25/0.35 % Preprocessing time : 0.002 s
% 0.25/0.35 % Presaturation interreduction done
% 0.25/0.35
% 0.25/0.35 % Proof found!
% 0.25/0.35 % SZS status Theorem
% 0.25/0.35 % SZS output start CNFRefutation
% 0.25/0.35 thf(decl_23, type, eps: ($i > $o) > $i).
% 0.25/0.35 thf(decl_24, type, if: $o > $i > $i > $i).
% 0.25/0.35 thf(decl_25, type, epred1_0: $i > $o).
% 0.25/0.35 thf(decl_26, type, esk1_0: $i).
% 0.25/0.35 thf(decl_27, type, epred2_3: $i > $o > $i > $i > $o).
% 0.25/0.35 thf(decl_28, type, epred3_0: $i > $o).
% 0.25/0.35 thf(decl_55, type, esk30_0: $i).
% 0.25/0.35 thf(conj, conjecture, ![X1:$i > $o]:(((eps @ X1)=(if @ (?[X2:$i]:((X1 @ X2))) @ (eps @ X1) @ (eps @ (^[X2:$i]:(~($true))))))), file('/export/starexec/sandbox/tmp/tmp.LPLKO4a83o/E---3.1_2950106.p', conj)).
% 0.25/0.35 thf(ifd, axiom, ((if)=(^[X3:$o, X2:$i, X4:$i]:(eps @ (^[X5:$i]:((((((X3))&(((X5)=(X2)))))|(((~((X3)))&(((X5)=(X4))))))))))), file('/export/starexec/sandbox/tmp/tmp.LPLKO4a83o/E---3.1_2950106.p', ifd)).
% 0.25/0.35 thf(choiceax, axiom, ![X1:$i > $o]:((?[X2:$i]:((X1 @ X2))=>(X1 @ (eps @ X1)))), file('/export/starexec/sandbox/tmp/tmp.LPLKO4a83o/E---3.1_2950106.p', choiceax)).
% 0.25/0.35 thf(c_0_3, negated_conjecture, ~(![X1:$i > $o]:(((eps @ X1)=(if @ (?[X2:$i]:((X1 @ X2))) @ (eps @ X1) @ (eps @ (^[X2:$i]:(~($true)))))))), inference(assume_negation,[status(cth)],[conj])).
% 0.25/0.35 thf(c_0_4, negated_conjecture, ~(![X1:$i > $o]:(((~(?[X2:$i]:((X1 @ X2)))|((eps @ X1)=(if @ $true @ (eps @ X1) @ (eps @ (^[Z0:$i]:(~($true)))))))&(?[X2:$i]:((X1 @ X2))|((eps @ X1)=(if @ $false @ (eps @ X1) @ (eps @ (^[Z0:$i]:(~($true)))))))))), inference(fool_unroll,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_3])])).
% 0.25/0.35 thf(c_0_5, plain, ![X9:$o, X10:$i, X11:$i]:(((if @ ((X9)) @ X10 @ X11)=(eps @ (^[Z0:$i]:((((((X9))&(((Z0)=(X10)))))|(((~((X9)))&(((Z0)=(X11))))))))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ifd])])).
% 0.25/0.35 thf(c_0_6, plain, ![X25:$i, X26:$i, X27:$o, X28:$i]:(((((~(X27)|(X27)|~(epred2_3 @ X28 @ X27 @ X26 @ X25))&(((X25)=(X28))|(X27)|~(epred2_3 @ X28 @ X27 @ X26 @ X25)))&((~(X27)|((X25)=(X26))|~(epred2_3 @ X28 @ X27 @ X26 @ X25))&(((X25)=(X28))|((X25)=(X26))|~(epred2_3 @ X28 @ X27 @ X26 @ X25))))&((~(X27)|((X25)!=(X26))|(epred2_3 @ X28 @ X27 @ X26 @ X25))&((X27)|((X25)!=(X28))|(epred2_3 @ X28 @ X27 @ X26 @ X25))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[])])])])])).
% 0.25/0.35 thf(c_0_7, negated_conjecture, ![X19:$i]:((((~(epred1_0 @ X19)|(epred1_0 @ esk1_0))&(((eps @ epred1_0)!=(if @ $false @ (eps @ epred1_0) @ (eps @ (^[Z0:$i]:(~($true))))))|(epred1_0 @ esk1_0)))&((~(epred1_0 @ X19)|((eps @ epred1_0)!=(if @ $true @ (eps @ epred1_0) @ (eps @ (^[Z0:$i]:(~($true)))))))&(((eps @ epred1_0)!=(if @ $false @ (eps @ epred1_0) @ (eps @ (^[Z0:$i]:(~($true))))))|((eps @ epred1_0)!=(if @ $true @ (eps @ epred1_0) @ (eps @ (^[Z0:$i]:(~($true)))))))))), 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_4])])])])])])).
% 0.25/0.35 thf(c_0_8, plain, ![X21:$i]:(((epred3_0 @ X21)<=>~(($true)))), introduced(definition)).
% 0.25/0.35 thf(c_0_9, plain, ![X14:$o, X15:$i, X16:$i]:(((if @ ((X14)) @ X15 @ X16)=(eps @ (^[Z0:$i]:((((((X14))&(((Z0)=(X15)))))|(((~((X14)))&(((Z0)=(X16))))))))))), inference(variable_rename,[status(thm)],[c_0_5])).
% 0.25/0.35 thf(c_0_10, plain, ![X20:$i, X2:$i, X3:$o, X4:$i]:(((epred2_3 @ X4 @ X3 @ X2 @ X20)<=>(((X3)&((X20)=(X2)))|(~((X3))&((X20)=(X4)))))), introduced(definition)).
% 0.25/0.35 thf(c_0_11, plain, ![X12:$i > $o, X13:$i]:((~(X12 @ X13)|(X12 @ (eps @ X12)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[choiceax])])])])).
% 0.25/0.35 thf(c_0_12, plain, ![X2:$i, X5:$i, X4:$i]:(((epred2_3 @ X5 @ (($true)) @ X4 @ X2)|((X2)!=(X4)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_6])])])).
% 0.25/0.35 thf(c_0_13, negated_conjecture, (((eps @ epred1_0)!=(if @ (((($true))!=(($true)))) @ (eps @ epred1_0) @ (eps @ epred3_0)))|((eps @ epred1_0)!=(if @ (((($true))=(($true)))) @ (eps @ epred1_0) @ (eps @ epred3_0)))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_7]), c_0_8]), c_0_8])).
% 0.25/0.35 thf(c_0_14, plain, ![X4:$i, X3:$o, X2:$i]:(((if @ ((X3)) @ X2 @ X4)=(eps @ (epred2_3 @ X4 @ ((X3)) @ X2)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_9]), c_0_10])).
% 0.25/0.35 thf(c_0_15, plain, ![X1:$i > $o, X2:$i]:(((X1 @ (eps @ X1))|~((X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.25/0.35 thf(c_0_16, plain, ![X2:$i, X4:$i]:((epred2_3 @ X2 @ (($true)) @ X4 @ X4)), inference(er,[status(thm)],[c_0_12])).
% 0.25/0.35 thf(c_0_17, plain, ![X2:$i, X5:$i, X4:$i]:(((epred2_3 @ X4 @ (~($true)) @ X5 @ X2)|((X2)!=(X4)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_6])])])).
% 0.25/0.35 thf(c_0_18, negated_conjecture, (((eps @ epred1_0)!=(eps @ (epred2_3 @ (eps @ epred3_0) @ (((($true))=(($true)))) @ (eps @ epred1_0))))|((eps @ epred1_0)!=(eps @ (epred2_3 @ (eps @ epred3_0) @ (((($true))!=(($true)))) @ (eps @ epred1_0))))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_13, c_0_14]), c_0_14])).
% 0.25/0.35 thf(c_0_19, plain, ![X5:$i, X4:$i, X2:$i]:((((X2)=(X4))|~((epred2_3 @ X5 @ (($true)) @ X4 @ X2)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_6])])])).
% 0.25/0.35 thf(c_0_20, plain, ![X2:$i, X4:$i]:((epred2_3 @ X2 @ (($true)) @ X4 @ (eps @ (epred2_3 @ X2 @ (($true)) @ X4)))), inference(spm,[status(thm)],[c_0_15, c_0_16])).
% 0.25/0.35 thf(c_0_21, plain, ![X4:$i, X2:$i]:((epred2_3 @ X2 @ (~($true)) @ X4 @ X2)), inference(er,[status(thm)],[c_0_17])).
% 0.25/0.35 thf(c_0_22, negated_conjecture, (((eps @ (epred2_3 @ (eps @ epred3_0) @ (($true)) @ (eps @ epred1_0)))!=(eps @ epred1_0))|((eps @ (epred2_3 @ (eps @ epred3_0) @ (~($true)) @ (eps @ epred1_0)))!=(eps @ epred1_0))), inference(cn,[status(thm)],[c_0_18])).
% 0.25/0.35 thf(c_0_23, plain, ![X2:$i, X4:$i]:(((eps @ (epred2_3 @ X2 @ (($true)) @ X4))=(X4))), inference(spm,[status(thm)],[c_0_19, c_0_20])).
% 0.25/0.35 thf(c_0_24, plain, ![X5:$i, X4:$i, X2:$i]:((((X2)=(X4))|~((epred2_3 @ X4 @ (~($true)) @ X5 @ X2)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_6])])])).
% 0.25/0.35 thf(c_0_25, plain, ![X2:$i, X4:$i]:((epred2_3 @ X2 @ (~($true)) @ X4 @ (eps @ (epred2_3 @ X2 @ (~($true)) @ X4)))), inference(spm,[status(thm)],[c_0_15, c_0_21])).
% 0.25/0.35 thf(c_0_26, negated_conjecture, ((eps @ (epred2_3 @ (eps @ epred3_0) @ (~($true)) @ (eps @ epred1_0)))!=(eps @ epred1_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23])])).
% 0.25/0.35 thf(c_0_27, plain, ![X4:$i, X2:$i]:(((eps @ (epred2_3 @ X2 @ (~($true)) @ X4))=(X2))), inference(spm,[status(thm)],[c_0_24, c_0_25])).
% 0.25/0.35 thf(c_0_28, negated_conjecture, ![X2:$i]:((~((epred1_0 @ X2))|((eps @ epred1_0)!=(if @ (((($true))=(($true)))) @ (eps @ epred1_0) @ (eps @ epred3_0))))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_7]), c_0_8])).
% 0.25/0.35 thf(c_0_29, negated_conjecture, ((eps @ epred3_0)!=(eps @ epred1_0)), inference(rw,[status(thm)],[c_0_26, c_0_27])).
% 0.25/0.35 thf(c_0_30, plain, ![X29:$i]:(((~(epred3_0 @ X29)|~($true))&(($true)|(epred3_0 @ X29)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[])])])).
% 0.25/0.35 thf(c_0_31, negated_conjecture, ![X2:$i]:((((eps @ epred1_0)!=(eps @ (epred2_3 @ (eps @ epred3_0) @ (((($true))=(($true)))) @ (eps @ epred1_0))))|~((epred1_0 @ X2)))), inference(rw,[status(thm)],[c_0_28, c_0_14])).
% 0.25/0.35 thf(c_0_32, negated_conjecture, ((epred3_0)!=(epred1_0)), inference(ext_eqres,[status(thm)],[c_0_29])).
% 0.25/0.35 thf(c_0_33, plain, ![X2:$i]:((~((epred3_0 @ X2))|~(($true)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.25/0.35 thf(c_0_34, negated_conjecture, ![X2:$i]:((((eps @ (epred2_3 @ (eps @ epred3_0) @ (($true)) @ (eps @ epred1_0)))!=(eps @ epred1_0))|~((epred1_0 @ X2)))), inference(cn,[status(thm)],[c_0_31])).
% 0.25/0.35 thf(c_0_35, negated_conjecture, ((epred3_0 @ esk30_0)<~>(epred1_0 @ esk30_0)), inference(neg_ext,[status(thm)],[c_0_32])).
% 0.25/0.35 thf(c_0_36, plain, ![X2:$i]:(~((epred3_0 @ X2))), inference(cn,[status(thm)],[c_0_33])).
% 0.25/0.35 thf(c_0_37, negated_conjecture, ![X2:$i]:(~((epred1_0 @ X2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_34, c_0_23])])).
% 0.25/0.35 thf(c_0_38, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_35]), c_0_36]), c_0_37]), ['proof']).
% 0.25/0.35 % SZS output end CNFRefutation
% 0.25/0.35 % Parsed axioms : 5
% 0.25/0.35 % Removed by relevancy pruning/SinE : 0
% 0.25/0.35 % Initial clauses : 16
% 0.25/0.35 % Removed in clause preprocessing : 5
% 0.25/0.35 % Initial clauses in saturation : 11
% 0.25/0.35 % Processed clauses : 111
% 0.25/0.35 % ...of these trivial : 0
% 0.25/0.35 % ...subsumed : 28
% 0.25/0.35 % ...remaining for further processing : 83
% 0.25/0.35 % Other redundant clauses eliminated : 18
% 0.25/0.35 % Clauses deleted for lack of memory : 0
% 0.25/0.35 % Backward-subsumed : 23
% 0.25/0.35 % Backward-rewritten : 6
% 0.25/0.35 % Generated clauses : 259
% 0.25/0.35 % ...of the previous two non-redundant : 207
% 0.25/0.35 % ...aggressively subsumed : 0
% 0.25/0.35 % Contextual simplify-reflections : 3
% 0.25/0.35 % Paramodulations : 59
% 0.25/0.35 % Factorizations : 0
% 0.25/0.35 % NegExts : 27
% 0.25/0.35 % Equation resolutions : 18
% 0.25/0.35 % Disequality decompositions : 0
% 0.25/0.35 % Total rewrite steps : 15
% 0.25/0.35 % ...of those cached : 4
% 0.25/0.35 % Propositional unsat checks : 0
% 0.25/0.35 % Propositional check models : 0
% 0.25/0.35 % Propositional check unsatisfiable : 0
% 0.25/0.35 % Propositional clauses : 0
% 0.25/0.35 % Propositional clauses after purity: 0
% 0.25/0.35 % Propositional unsat core size : 0
% 0.25/0.35 % Propositional preprocessing time : 0.000
% 0.25/0.35 % Propositional encoding time : 0.000
% 0.25/0.35 % Propositional solver time : 0.000
% 0.25/0.35 % Success case prop preproc time : 0.000
% 0.25/0.35 % Success case prop encoding time : 0.000
% 0.25/0.35 % Success case prop solver time : 0.000
% 0.25/0.35 % Current number of processed clauses : 25
% 0.25/0.35 % Positive orientable unit clauses : 4
% 0.25/0.35 % Positive unorientable unit clauses: 1
% 0.25/0.35 % Negative unit clauses : 6
% 0.25/0.35 % Non-unit-clauses : 14
% 0.25/0.35 % Current number of unprocessed clauses: 118
% 0.25/0.35 % ...number of literals in the above : 338
% 0.25/0.35 % Current number of archived formulas : 0
% 0.25/0.35 % Current number of archived clauses : 57
% 0.25/0.35 % Clause-clause subsumption calls (NU) : 194
% 0.25/0.35 % Rec. Clause-clause subsumption calls : 136
% 0.25/0.35 % Non-unit clause-clause subsumptions : 26
% 0.25/0.35 % Unit Clause-clause subsumption calls : 54
% 0.25/0.35 % Rewrite failures with RHS unbound : 0
% 0.25/0.35 % BW rewrite match attempts : 59
% 0.25/0.35 % BW rewrite match successes : 14
% 0.25/0.35 % Condensation attempts : 0
% 0.25/0.35 % Condensation successes : 0
% 0.25/0.35 % Termbank termtop insertions : 9248
% 0.25/0.35 % Search garbage collected termcells : 249
% 0.25/0.35
% 0.25/0.35 % -------------------------------------------------
% 0.25/0.35 % User time : 0.026 s
% 0.25/0.35 % System time : 0.006 s
% 0.25/0.35 % Total time : 0.032 s
% 0.25/0.35 % Maximum resident set size: 3632 pages
% 0.25/0.35
% 0.25/0.35 % -------------------------------------------------
% 0.25/0.35 % User time : 0.102 s
% 0.25/0.35 % System time : 0.023 s
% 0.25/0.35 % Total time : 0.125 s
% 0.25/0.35 % Maximum resident set size: 4608 pages
% 0.25/0.35 % E exiting
%------------------------------------------------------------------------------