%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP066^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 : n020.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:04:15 AM UTC 2026
% Result : Theorem 8.18s 1.48s
% Output : CNFRefutation 8.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 4
% Syntax : Number of formulae : 15 ( 15 unt; 0 typ; 0 def)
% Number of atoms : 15 ( 14 equ; 0 cnn)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 162 ( 4 ~; 0 |; 0 &; 158 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Number of types : 3 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 16 ( 14 usr; 10 con; 0-3 aty)
% Number of variables : 34 ( 0 ^; 34 !; 0 ?; 34 :)
% Comments :
%------------------------------------------------------------------------------
thf(decl_sort1,type,
a: $tType ).
thf(decl_sort2,type,
tree_a: $tType ).
thf(decl_sort3,type,
produc143150363Tree_a: $tType ).
thf(decl_40,type,
heapIm837449470Leaf_a: tree_a > produc143150363Tree_a ).
thf(decl_48,type,
t_a: a > tree_a > tree_a > tree_a ).
thf(decl_94,type,
produc686083979Tree_a: a > tree_a > produc143150363Tree_a ).
thf(decl_98,type,
product_fst_a_Tree_a: produc143150363Tree_a > a ).
thf(decl_102,type,
product_snd_a_Tree_a: produc143150363Tree_a > tree_a ).
thf(decl_129,type,
l1: tree_a ).
thf(decl_130,type,
l2: tree_a ).
thf(decl_131,type,
r1: tree_a ).
thf(decl_132,type,
r2: tree_a ).
thf(decl_135,type,
t_a2: tree_a ).
thf(decl_136,type,
v1: a ).
thf(decl_137,type,
v2: a ).
thf(decl_139,type,
v_a: a ).
thf(decl_140,type,
v3: a ).
thf(conj_0,conjecture,
( v_a
= ( product_fst_a_Tree_a @ ( heapIm837449470Leaf_a @ ( t_a @ v1 @ l1 @ r1 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.WkR9QQqpy1/E---3.1_1501719.p',conj_0) ).
thf(fact_22_fst__conv,axiom,
! [X47: a,X48: tree_a] :
( ( product_fst_a_Tree_a @ ( produc686083979Tree_a @ X47 @ X48 ) )
= X47 ),
file('/export/starexec/sandbox2/tmp/tmp.WkR9QQqpy1/E---3.1_1501719.p',fact_22_fst__conv) ).
thf(fact_5_removeLeaf_Osimps_I5_J,axiom,
! [X7: a,X8: a,X9: tree_a,X10: tree_a,X11: a,X12: tree_a,X13: tree_a] :
( ( heapIm837449470Leaf_a @ ( t_a @ X7 @ ( t_a @ X8 @ X9 @ X10 ) @ ( t_a @ X11 @ X12 @ X13 ) ) )
= ( produc686083979Tree_a @ ( product_fst_a_Tree_a @ ( heapIm837449470Leaf_a @ ( t_a @ X8 @ X9 @ X10 ) ) ) @ ( t_a @ X7 @ ( product_snd_a_Tree_a @ ( heapIm837449470Leaf_a @ ( t_a @ X8 @ X9 @ X10 ) ) ) @ ( t_a @ X11 @ X12 @ X13 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.WkR9QQqpy1/E---3.1_1501719.p',fact_5_removeLeaf_Osimps_I5_J) ).
thf(fact_0__C4__2_Oprems_C_I1_J,axiom,
( ( produc686083979Tree_a @ v_a @ t_a2 )
= ( heapIm837449470Leaf_a @ ( t_a @ v3 @ ( t_a @ v1 @ l1 @ r1 ) @ ( t_a @ v2 @ l2 @ r2 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.WkR9QQqpy1/E---3.1_1501719.p',fact_0__C4__2_Oprems_C_I1_J) ).
thf(c_0_4,negated_conjecture,
( v_a
!= ( product_fst_a_Tree_a @ ( heapIm837449470Leaf_a @ ( t_a @ v1 @ l1 @ r1 ) ) ) ),
inference(assume_negation,[status(cth)],[conj_0]) ).
thf(c_0_5,plain,
! [X2151: a,X2152: tree_a] :
( ( product_fst_a_Tree_a @ ( produc686083979Tree_a @ X2151 @ X2152 ) )
= X2151 ),
inference(variable_rename,[status(thm)],[fact_22_fst__conv]) ).
thf(c_0_6,plain,
! [X2098: a,X2099: a,X2100: tree_a,X2101: tree_a,X2102: a,X2103: tree_a,X2104: tree_a] :
( ( heapIm837449470Leaf_a @ ( t_a @ X2098 @ ( t_a @ X2099 @ X2100 @ X2101 ) @ ( t_a @ X2102 @ X2103 @ X2104 ) ) )
= ( produc686083979Tree_a @ ( product_fst_a_Tree_a @ ( heapIm837449470Leaf_a @ ( t_a @ X2099 @ X2100 @ X2101 ) ) ) @ ( t_a @ X2098 @ ( product_snd_a_Tree_a @ ( heapIm837449470Leaf_a @ ( t_a @ X2099 @ X2100 @ X2101 ) ) ) @ ( t_a @ X2102 @ X2103 @ X2104 ) ) ) ),
inference(variable_rename,[status(thm)],[fact_5_removeLeaf_Osimps_I5_J]) ).
thf(c_0_7,negated_conjecture,
( v_a
!= ( product_fst_a_Tree_a @ ( heapIm837449470Leaf_a @ ( t_a @ v1 @ l1 @ r1 ) ) ) ),
inference(fof_simplification,[status(thm)],[c_0_4]) ).
thf(c_0_8,plain,
! [X2: tree_a,X1: a] :
( ( product_fst_a_Tree_a @ ( produc686083979Tree_a @ X1 @ X2 ) )
= X1 ),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
thf(c_0_9,plain,
! [X1: a,X2: tree_a,X3: tree_a,X4: a,X5: tree_a,X7: a,X6: tree_a] :
( ( heapIm837449470Leaf_a @ ( t_a @ X1 @ ( t_a @ X4 @ X2 @ X3 ) @ ( t_a @ X7 @ X5 @ X6 ) ) )
= ( produc686083979Tree_a @ ( product_fst_a_Tree_a @ ( heapIm837449470Leaf_a @ ( t_a @ X4 @ X2 @ X3 ) ) ) @ ( t_a @ X1 @ ( product_snd_a_Tree_a @ ( heapIm837449470Leaf_a @ ( t_a @ X4 @ X2 @ X3 ) ) ) @ ( t_a @ X7 @ X5 @ X6 ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
thf(c_0_10,negated_conjecture,
( v_a
!= ( product_fst_a_Tree_a @ ( heapIm837449470Leaf_a @ ( t_a @ v1 @ l1 @ r1 ) ) ) ),
inference(fof_nnf,[status(thm)],[c_0_7]) ).
thf(c_0_11,plain,
! [X1: a,X2: tree_a,X7: a,X6: tree_a,X5: tree_a,X4: a,X3: tree_a] :
( ( product_fst_a_Tree_a @ ( heapIm837449470Leaf_a @ ( t_a @ X1 @ ( t_a @ X4 @ X2 @ X3 ) @ ( t_a @ X7 @ X5 @ X6 ) ) ) )
= ( product_fst_a_Tree_a @ ( heapIm837449470Leaf_a @ ( t_a @ X4 @ X2 @ X3 ) ) ) ),
inference(spm,[status(thm)],[c_0_8,c_0_9]) ).
thf(c_0_12,plain,
( ( produc686083979Tree_a @ v_a @ t_a2 )
= ( heapIm837449470Leaf_a @ ( t_a @ v3 @ ( t_a @ v1 @ l1 @ r1 ) @ ( t_a @ v2 @ l2 @ r2 ) ) ) ),
inference(split_conjunct,[status(thm)],[fact_0__C4__2_Oprems_C_I1_J]) ).
thf(c_0_13,negated_conjecture,
( v_a
!= ( product_fst_a_Tree_a @ ( heapIm837449470Leaf_a @ ( t_a @ v1 @ l1 @ r1 ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
thf(c_0_14,plain,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_11,c_0_12]),c_0_8]),c_0_13]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP066^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n020.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:47:04 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.22 Running higher-order theorem proving
% 0.20/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.WkR9QQqpy1/E---3.1_1501719.p
% 8.18/1.48 % Version: 3.5.1-ho
% 8.18/1.48 % Preprocessing class: HSLMSMSMSSLNHFA.
% 8.18/1.48 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 8.18/1.48 % Starting new_ho_11 with 1500s (5) cores
% 8.18/1.48 % Starting additional_ho_5 with 300s (1) cores
% 8.18/1.48 % Starting new_ho_10_cnf2 with 300s (1) cores
% 8.18/1.48 % Starting full_lambda_7 with 300s (1) cores
% 8.18/1.48 % new_ho_11 with pid 1501732 completed with status 0
% 8.18/1.48 % Result found by new_ho_11
% 8.18/1.48 % Preprocessing class: HSLMSMSMSSLNHFA.
% 8.18/1.48 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 8.18/1.48 % Starting new_ho_11 with 1500s (5) cores
% 8.18/1.48 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 8.18/1.48 % No SInE strategy applied
% 8.18/1.48 % Search class: HGHSM-FMLM32-DHFFFSBN
% 8.18/1.48 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 8.18/1.48 % Starting SubtermCWHack with 136s (1) cores
% 8.18/1.48 % Starting new_ho_11 with 151s (1) cores
% 8.18/1.48 % Starting sh5l with 136s (1) cores
% 8.18/1.48 % Starting new_bool_1 with 136s (1) cores
% 8.18/1.48 % Starting new_bool_2 with 136s (1) cores
% 8.18/1.48 % new_ho_11 with pid 1501739 completed with status 0
% 8.18/1.48 % Result found by new_ho_11
% 8.18/1.48 % Preprocessing class: HSLMSMSMSSLNHFA.
% 8.18/1.48 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 8.18/1.48 % Starting new_ho_11 with 1500s (5) cores
% 8.18/1.48 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 8.18/1.48 % No SInE strategy applied
% 8.18/1.48 % Search class: HGHSM-FMLM32-DHFFFSBN
% 8.18/1.48 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 8.18/1.48 % Starting SubtermCWHack with 136s (1) cores
% 8.18/1.48 % Starting new_ho_11 with 151s (1) cores
% 8.18/1.48 % Preprocessing time : 0.025 s
% 8.18/1.48 % Presaturation interreduction done
% 8.18/1.48
% 8.18/1.48 % Proof found!
% 8.18/1.48 % SZS status Theorem
% 8.18/1.48 % SZS output start CNFRefutation
% See solution above
% 8.18/1.48 % Parsed axioms : 507
% 8.18/1.48 % Removed by relevancy pruning/SinE : 0
% 8.18/1.48 % Initial clauses : 1137
% 8.18/1.48 % Removed in clause preprocessing : 192
% 8.18/1.48 % Initial clauses in saturation : 945
% 8.18/1.48 % Processed clauses : 2984
% 8.18/1.48 % ...of these trivial : 76
% 8.18/1.48 % ...subsumed : 876
% 8.18/1.48 % ...remaining for further processing : 2032
% 8.18/1.48 % Other redundant clauses eliminated : 394
% 8.18/1.48 % Clauses deleted for lack of memory : 0
% 8.18/1.48 % Backward-subsumed : 15
% 8.18/1.48 % Backward-rewritten : 42
% 8.18/1.48 % Generated clauses : 7880
% 8.18/1.48 % ...of the previous two non-redundant : 6891
% 8.18/1.48 % ...aggressively subsumed : 0
% 8.18/1.48 % Contextual simplify-reflections : 0
% 8.18/1.48 % Paramodulations : 7370
% 8.18/1.48 % Factorizations : 68
% 8.18/1.48 % NegExts : 0
% 8.18/1.48 % Equation resolutions : 429
% 8.18/1.48 % Disequality decompositions : 0
% 8.18/1.48 % Total rewrite steps : 3424
% 8.18/1.48 % ...of those cached : 2921
% 8.18/1.48 % Propositional unsat checks : 0
% 8.18/1.48 % Propositional check models : 0
% 8.18/1.48 % Propositional check unsatisfiable : 0
% 8.18/1.48 % Propositional clauses : 0
% 8.18/1.48 % Propositional clauses after purity: 0
% 8.18/1.48 % Propositional unsat core size : 0
% 8.18/1.48 % Propositional preprocessing time : 0.000
% 8.18/1.48 % Propositional encoding time : 0.000
% 8.18/1.48 % Propositional solver time : 0.000
% 8.18/1.48 % Success case prop preproc time : 0.000
% 8.18/1.48 % Success case prop encoding time : 0.000
% 8.18/1.48 % Success case prop solver time : 0.000
% 8.18/1.48 % Current number of processed clauses : 1177
% 8.18/1.48 % Positive orientable unit clauses : 190
% 8.18/1.48 % Positive unorientable unit clauses: 4
% 8.18/1.48 % Negative unit clauses : 108
% 8.18/1.48 % Non-unit-clauses : 875
% 8.18/1.48 % Current number of unprocessed clauses: 5353
% 8.18/1.48 % ...number of literals in the above : 21463
% 8.18/1.48 % Current number of archived formulas : 0
% 8.18/1.48 % Current number of archived clauses : 789
% 8.18/1.48 % Clause-clause subsumption calls (NU) : 619406
% 8.18/1.48 % Rec. Clause-clause subsumption calls : 58528
% 8.18/1.48 % Non-unit clause-clause subsumptions : 363
% 8.18/1.48 % Unit Clause-clause subsumption calls : 13080
% 8.18/1.48 % Rewrite failures with RHS unbound : 0
% 8.18/1.48 % BW rewrite match attempts : 212
% 8.18/1.48 % BW rewrite match successes : 109
% 8.18/1.48 % Condensation attempts : 0
% 8.18/1.48 % Condensation successes : 0
% 8.18/1.48 % Termbank termtop insertions : 274562
% 8.18/1.48 % Search garbage collected termcells : 19462
% 8.18/1.48
% 8.18/1.48 % -------------------------------------------------
% 8.18/1.48 % User time : 0.961 s
% 8.18/1.48 % System time : 0.038 s
% 8.18/1.48 % Total time : 0.999 s
% 8.18/1.48 % Maximum resident set size: 8896 pages
% 8.18/1.48
% 8.18/1.48 % -------------------------------------------------
% 8.18/1.48 % User time : 4.910 s
% 8.18/1.48 % System time : 0.154 s
% 8.18/1.48 % Total time : 5.065 s
% 8.18/1.48 % Maximum resident set size: 5888 pages
% 8.18/1.48 % E exiting
%------------------------------------------------------------------------------