%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : HWV068-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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 : Thu Sep 24 12:48:24 PM UTC 2026
% Result : Unsatisfiable 37.64s 32.83s
% Output : CNFRefutation 37.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 17
% Syntax : Number of clauses : 50 ( 11 unt; 6 nHn; 50 RR)
% Number of literals : 131 ( 0 equ; 81 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 17 ( 16 usr; 3 prp; 0-4 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 168 ( 12 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_33259,axiom,
( ~ esk16222_4(X1,X2,X3,X4)
| esk16220_4(X1,X2,X3,X4)
| esk16221_4(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_33259) ).
cnf(i_0_25870,axiom,
( ~ esk16349_4(X1,X2,X3,X4)
| esk16347_4(X1,X2,X3,X4)
| esk16348_4(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_25870) ).
cnf(i_0_45914,axiom,
( ~ esk17147_4(X1,X2,X3,X4)
| esk16222_4(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_45914) ).
cnf(i_0_26220,axiom,
( ~ esk16347_4(X1,X2,X3,X4)
| esk17148_4(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_26220) ).
cnf(i_0_47728,axiom,
( ~ esk16220_4(X1,X2,X3,X4)
| esk16349_4(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_47728) ).
cnf(i_0_3266,axiom,
( ~ esk17157_4(X1,X2,X3,X4)
| esk16516_4(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3266) ).
cnf(i_0_32779,axiom,
( ~ esk16348_4(X1,X2,X3,X4)
| esk17504_4(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_32779) ).
cnf(i_0_20513,axiom,
( ~ esk17504_4(X1,X2,X3,X4)
| esk16333_4(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_20513) ).
cnf(i_0_22074,axiom,
( ~ esk17148_4(X1,X2,X3,X4)
| esk17564_4(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_22074) ).
cnf(i_0_41865,axiom,
( ~ esk16221_4(X1,X2,X3,X4)
| esk17157_4(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_41865) ).
cnf(i_0_14736,axiom,
( ~ p(X4)
| ~ p(X2)
| ~ p(X3)
| ~ esk16333_4(X2,X3,X1,X4)
| ~ p(X1)
| esk1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_14736) ).
cnf(i_0_43176,axiom,
( ~ p(X3)
| ~ p(X4)
| ~ esk17564_4(X2,X3,X4,X1)
| ~ p(X2)
| ~ p(X1)
| esk1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_43176) ).
cnf(i_0_34555,axiom,
( ~ p(X4)
| ~ esk2_0
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| esk17147_4(X1,X4,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_34555) ).
cnf(i_0_21184,axiom,
~ esk16516_4(X1,X2,X3,X4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_21184) ).
cnf(i_0_37238,axiom,
~ esk1_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_37238) ).
cnf(rule_true,axiom,
p(true),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_true) ).
cnf(i_0_4556,axiom,
esk2_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4556) ).
cnf(c_0_47746,plain,
( ~ esk16222_4(X1,X2,X3,X4)
| esk16220_4(X1,X2,X3,X4)
| esk16221_4(X1,X2,X3,X4) ),
inference(fof_simplification,[status(thm)],[i_0_33259]) ).
cnf(c_0_47747,plain,
( ~ esk16349_4(X1,X2,X3,X4)
| esk16347_4(X1,X2,X3,X4)
| esk16348_4(X1,X2,X3,X4) ),
inference(fof_simplification,[status(thm)],[i_0_25870]) ).
cnf(c_0_47748,plain,
( ~ esk17147_4(X1,X2,X3,X4)
| esk16222_4(X1,X2,X3,X4) ),
inference(fof_simplification,[status(thm)],[i_0_45914]) ).
cnf(c_0_47749,plain,
( ~ esk16347_4(X1,X2,X3,X4)
| esk17148_4(X1,X2,X3,X4) ),
inference(fof_simplification,[status(thm)],[i_0_26220]) ).
cnf(c_0_47750,plain,
( ~ esk16220_4(X1,X2,X3,X4)
| esk16349_4(X1,X2,X3,X4) ),
inference(fof_simplification,[status(thm)],[i_0_47728]) ).
cnf(c_0_47751,plain,
( ~ esk17157_4(X1,X2,X3,X4)
| esk16516_4(X1,X2,X3,X4) ),
inference(fof_simplification,[status(thm)],[i_0_3266]) ).
cnf(c_0_47752,plain,
( ~ esk16348_4(X1,X2,X3,X4)
| esk17504_4(X1,X2,X3,X4) ),
inference(fof_simplification,[status(thm)],[i_0_32779]) ).
cnf(c_0_47753,plain,
( ~ esk17504_4(X1,X2,X3,X4)
| esk16333_4(X1,X2,X3,X4) ),
inference(fof_simplification,[status(thm)],[i_0_20513]) ).
cnf(c_0_47754,plain,
( ~ esk17148_4(X1,X2,X3,X4)
| esk17564_4(X1,X2,X3,X4) ),
inference(fof_simplification,[status(thm)],[i_0_22074]) ).
cnf(c_0_47755,plain,
( ~ esk16221_4(X1,X2,X3,X4)
| esk17157_4(X1,X2,X3,X4) ),
inference(fof_simplification,[status(thm)],[i_0_41865]) ).
cnf(c_0_47756,plain,
( ~ p(X4)
| ~ p(X2)
| ~ p(X3)
| ~ esk16333_4(X2,X3,X1,X4)
| ~ p(X1)
| esk1_0 ),
inference(fof_simplification,[status(thm)],[i_0_14736]) ).
cnf(c_0_47757,plain,
( ~ p(X3)
| ~ p(X4)
| ~ esk17564_4(X2,X3,X4,X1)
| ~ p(X2)
| ~ p(X1)
| esk1_0 ),
inference(fof_simplification,[status(thm)],[i_0_43176]) ).
cnf(c_0_47758,plain,
( ~ p(X4)
| ~ esk2_0
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| esk17147_4(X1,X4,X2,X3) ),
inference(fof_simplification,[status(thm)],[i_0_34555]) ).
cnf(c_0_47759,plain,
~ esk16516_4(X1,X2,X3,X4),
inference(fof_simplification,[status(thm)],[i_0_21184]) ).
cnf(c_0_47760,plain,
~ esk1_0,
inference(fof_simplification,[status(thm)],[i_0_37238]) ).
cnf(c_0_47761,plain,
( ~ esk16222_4(X1,X2,X3,X4)
| esk16220_4(X1,X2,X3,X4)
| esk16221_4(X1,X2,X3,X4) ),
c_0_47746 ).
cnf(c_0_47762,plain,
( ~ esk16349_4(X1,X2,X3,X4)
| esk16347_4(X1,X2,X3,X4)
| esk16348_4(X1,X2,X3,X4) ),
c_0_47747 ).
cnf(c_0_47763,plain,
( ~ esk17147_4(X1,X2,X3,X4)
| esk16222_4(X1,X2,X3,X4) ),
c_0_47748 ).
cnf(c_0_47764,plain,
( ~ esk16347_4(X1,X2,X3,X4)
| esk17148_4(X1,X2,X3,X4) ),
c_0_47749 ).
cnf(c_0_47765,plain,
( ~ esk16220_4(X1,X2,X3,X4)
| esk16349_4(X1,X2,X3,X4) ),
c_0_47750 ).
cnf(c_0_47766,plain,
( ~ esk17157_4(X1,X2,X3,X4)
| esk16516_4(X1,X2,X3,X4) ),
c_0_47751 ).
cnf(c_0_47767,plain,
( ~ esk16348_4(X1,X2,X3,X4)
| esk17504_4(X1,X2,X3,X4) ),
c_0_47752 ).
cnf(c_0_47768,plain,
( ~ esk17504_4(X1,X2,X3,X4)
| esk16333_4(X1,X2,X3,X4) ),
c_0_47753 ).
cnf(c_0_47769,plain,
( ~ esk17148_4(X1,X2,X3,X4)
| esk17564_4(X1,X2,X3,X4) ),
c_0_47754 ).
cnf(c_0_47770,plain,
( ~ esk16221_4(X1,X2,X3,X4)
| esk17157_4(X1,X2,X3,X4) ),
c_0_47755 ).
cnf(c_0_47771,plain,
( ~ p(X4)
| ~ p(X2)
| ~ p(X3)
| ~ esk16333_4(X2,X3,X1,X4)
| ~ p(X1)
| esk1_0 ),
c_0_47756 ).
cnf(c_0_47772,plain,
( ~ p(X3)
| ~ p(X4)
| ~ esk17564_4(X2,X3,X4,X1)
| ~ p(X2)
| ~ p(X1)
| esk1_0 ),
c_0_47757 ).
cnf(c_0_47773,plain,
( ~ p(X4)
| ~ esk2_0
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| esk17147_4(X1,X4,X2,X3) ),
c_0_47758 ).
cnf(c_0_47774,plain,
~ esk16516_4(X1,X2,X3,X4),
c_0_47759 ).
cnf(c_0_47775,plain,
~ esk1_0,
c_0_47760 ).
cnf(c_0_47776,axiom,
p(true),
rule_true ).
cnf(c_0_47777,axiom,
esk2_0,
i_0_4556 ).
cnf(c_0_47778,plain,
$false,
inference(cdclpropres,[status(thm)],[c_0_47761,c_0_47762,c_0_47763,c_0_47764,c_0_47765,c_0_47766,c_0_47767,c_0_47768,c_0_47769,c_0_47770,c_0_47771,c_0_47772,c_0_47773,c_0_47774,c_0_47775,c_0_47776,c_0_47777]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : HWV068-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 0.00/0.03 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.05/0.31 % Computer : n012.cluster.edu
% 0.05/0.31 % Model : x86_64 x86_64
% 0.05/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.31 % Memory : 8046.5625MB
% 0.05/0.31 % OS : Linux 6.8.0-71-generic
% 0.05/0.31 % CPULimit : 300
% 0.05/0.31 % WCLimit : 300
% 0.05/0.31 % DateTime : Sun Sep 20 21:10:51 UTC 2026
% 0.05/0.31 % CPUTime :
% 0.05/0.31 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.34 Running first-order theorem proving
% 0.08/0.34 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 37.64/32.83 % Version: 3.5.1
% 37.64/32.83 % Preprocessing class: FMLLLLSSSSSNFFN.
% 37.64/32.83 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 37.64/32.83 % Starting new_bool_3 with 900s (3) cores
% 37.64/32.83 % Starting new_bool_1 with 900s (3) cores
% 37.64/32.83 % Starting sh5l with 300s (1) cores
% 37.64/32.83 % Starting SAT001_MinMin_p005000_rr_RG with 300s (1) cores
% 37.64/32.83 % new_bool_3 with pid 858265 completed with status 9
% 37.64/32.83 % new_bool_1 with pid 858266 completed with status 9
% 37.64/32.83 % sh5l with pid 858267 completed with status 9
% 37.64/32.83 % SAT001_MinMin_p005000_rr_RG with pid 858268 completed with status 0
% 37.64/32.83 % Result found by SAT001_MinMin_p005000_rr_RG
% 37.64/32.83 % Preprocessing class: FMLLLLSSSSSNFFN.
% 37.64/32.83 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 37.64/32.83 % Starting new_bool_3 with 900s (3) cores
% 37.64/32.83 % Starting new_bool_1 with 900s (3) cores
% 37.64/32.83 % Starting sh5l with 300s (1) cores
% 37.64/32.83 % Starting SAT001_MinMin_p005000_rr_RG with 300s (1) cores
% 37.64/32.83 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 37.64/32.83 % No SInE strategy applied
% 37.64/32.83 % Search class: FGHSM-SMLF00-SFFFFFNN
% 37.64/32.83 % Scheduled 6 strats onto 1 cores with 299 seconds (299 total)
% 37.64/32.83 % Starting SubtermCWHack with 30s (1) cores
% 37.64/32.83 % SubtermCWHack with pid 858349 completed with status 8
% 37.64/32.83 % Starting SAT001_MinMin_p005000_rr_RG with 129s (1) cores
% 37.64/32.83 % SAT001_MinMin_p005000_rr_RG with pid 858353 completed with status 0
% 37.64/32.83 % Result found by SAT001_MinMin_p005000_rr_RG
% 37.64/32.83 % Preprocessing class: FMLLLLSSSSSNFFN.
% 37.64/32.83 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 37.64/32.83 % Starting new_bool_3 with 900s (3) cores
% 37.64/32.83 % Starting new_bool_1 with 900s (3) cores
% 37.64/32.83 % Starting sh5l with 300s (1) cores
% 37.64/32.83 % Starting SAT001_MinMin_p005000_rr_RG with 300s (1) cores
% 37.64/32.83 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 37.64/32.83 % No SInE strategy applied
% 37.64/32.83 % Search class: FGHSM-SMLF00-SFFFFFNN
% 37.64/32.83 % Scheduled 6 strats onto 1 cores with 299 seconds (299 total)
% 37.64/32.83 % Starting SubtermCWHack with 30s (1) cores
% 37.64/32.83 % SubtermCWHack with pid 858349 completed with status 8
% 37.64/32.83 % Starting SAT001_MinMin_p005000_rr_RG with 129s (1) cores
% 37.64/32.83 % Preprocessing time : 0.394 s
% 37.64/32.83 % SatCheck found unsatisfiable ground set
% 37.64/32.83 % Presaturation interreduction done
% 37.64/32.83
% 37.64/32.83 % Proof found!
% 37.64/32.83 % SZS status Unsatisfiable
% 37.64/32.83 % SZS output start CNFRefutation
% See solution above
% 37.64/32.83 % Parsed axioms : 49913
% 37.64/32.83 % Removed by relevancy pruning/SinE : 0
% 37.64/32.83 % Initial clauses : 49913
% 37.64/32.83 % Removed in clause preprocessing : 0
% 37.64/32.83 % Initial clauses in saturation : 49913
% 37.64/32.83 % Processed clauses : 5090
% 37.64/32.83 % ...of these trivial : 0
% 37.64/32.83 % ...subsumed : 90
% 37.64/32.83 % ...remaining for further processing : 5000
% 37.64/32.83 % Other redundant clauses eliminated : 0
% 37.64/32.83 % Clauses deleted for lack of memory : 0
% 37.64/32.83 % Backward-subsumed : 1
% 37.64/32.83 % Backward-rewritten : 0
% 37.64/32.83 % Generated clauses : 0
% 37.64/32.83 % ...of the previous two non-redundant : 0
% 37.64/32.83 % ...aggressively subsumed : 0
% 37.64/32.83 % Contextual simplify-reflections : 0
% 37.64/32.83 % Paramodulations : 0
% 37.64/32.83 % Factorizations : 0
% 37.64/32.83 % NegExts : 0
% 37.64/32.83 % Equation resolutions : 0
% 37.64/32.83 % Disequality decompositions : 0
% 37.64/32.83 % Total rewrite steps : 0
% 37.64/32.83 % ...of those cached : 0
% 37.64/32.83 % Propositional unsat checks : 1
% 37.64/32.83 % Propositional check models : 0
% 37.64/32.83 % Propositional check unsatisfiable : 1
% 37.64/32.83 % Propositional clauses : 49822
% 37.64/32.83 % Propositional clauses after purity: 49820
% 37.64/32.83 % Propositional unsat core size : 17
% 37.64/32.83 % Propositional preprocessing time : 0.000
% 37.64/32.83 % Propositional encoding time : 0.055
% 37.64/32.83 % Propositional solver time : 0.013
% 37.64/32.83 % Success case prop preproc time : 0.000
% 37.64/32.83 % Success case prop encoding time : 0.055
% 37.64/32.83 % Success case prop solver time : 0.013
% 37.64/32.83 % Current number of processed clauses : 4999
% 37.64/32.83 % Positive orientable unit clauses : 34
% 37.64/32.83 % Positive unorientable unit clauses: 0
% 37.64/32.83 % Negative unit clauses : 36
% 37.64/32.83 % Non-unit-clauses : 4929
% 37.64/32.83 % Current number of unprocessed clauses: 44823
% 37.64/32.83 % ...number of literals in the above : 123102
% 37.64/32.83 % Current number of archived formulas : 0
% 37.64/32.83 % Current number of archived clauses : 1
% 37.64/32.83 % Clause-clause subsumption calls (NU) : 5601948
% 37.64/32.83 % Rec. Clause-clause subsumption calls : 3391159
% 37.64/32.83 % Non-unit clause-clause subsumptions : 0
% 37.64/32.83 % Unit Clause-clause subsumption calls : 17623
% 37.64/32.83 % Rewrite failures with RHS unbound : 0
% 37.64/32.83 % BW rewrite match attempts : 0
% 37.64/32.83 % BW rewrite match successes : 0
% 37.64/32.83 % Condensation attempts : 0
% 37.64/32.83 % Condensation successes : 0
% 37.64/32.83 % Termbank termtop insertions : 1431167
% 37.64/32.83 % Search garbage collected termcells : 85656
% 37.64/32.83
% 37.64/32.83 % -------------------------------------------------
% 37.64/32.83 % User time : 31.724 s
% 37.64/32.83 % System time : 0.264 s
% 37.64/32.83 % Total time : 31.988 s
% 37.64/32.83 % Maximum resident set size: 96476 pages
% 37.64/32.83
% 37.64/32.83 % -------------------------------------------------
% 37.64/32.83 % User time : 36.134 s
% 37.64/32.83 % System time : 1.501 s
% 37.64/32.83 % Total time : 37.634 s
% 37.64/32.83 % Maximum resident set size: 36608 pages
% 37.64/32.83 % E exiting
%------------------------------------------------------------------------------