%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP197^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:39 AM UTC 2026
% Result : Theorem 0.42s 0.45s
% Output : CNFRefutation 0.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 5
% Syntax : Number of formulae : 25 ( 14 unt; 0 typ; 0 def)
% Number of atoms : 42 ( 31 equ; 0 cnn)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 156 ( 16 ~; 12 |; 3 &; 123 @)
% ( 1 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Number of types : 5 ( 4 usr)
% Number of type conns : 3 ( 3 >; 0 *; 0 +; 0 <<)
% Number of symbols : 13 ( 11 usr; 4 con; 0-2 aty)
% Number of variables : 22 ( 0 ^; 22 !; 0 ?; 22 :)
% Comments :
%------------------------------------------------------------------------------
thf(decl_sort1,type,
nat: $tType ).
thf(decl_sort2,type,
type_Mirabelle_typ: $tType ).
thf(decl_sort3,type,
set_nat: $tType ).
thf(decl_sort4,type,
type_M1694694083scheme: $tType ).
thf(decl_51,type,
bot_bot_set_nat: set_nat ).
thf(decl_56,type,
insert_nat: nat > set_nat > set_nat ).
thf(decl_63,type,
type_M1006385707scheme: type_Mirabelle_typ > type_M1694694083scheme ).
thf(decl_79,type,
type_M876316792e_FVar: nat > type_M1694694083scheme ).
thf(decl_89,type,
type_M1690910139scheme: ( nat > type_Mirabelle_typ ) > type_M1694694083scheme > type_M1694694083scheme ).
thf(decl_106,type,
type_M1050318637scheme: type_M1694694083scheme > set_nat ).
thf(decl_107,type,
member_nat: nat > set_nat > $o ).
thf(decl_108,type,
s1: nat > type_Mirabelle_typ ).
thf(decl_109,type,
s2: nat > type_Mirabelle_typ ).
thf(decl_110,type,
n: nat ).
thf(decl_111,type,
x: nat ).
thf(conj_0,conjecture,
( ( ( type_M1690910139scheme @ s1 @ ( type_M876316792e_FVar @ x ) )
!= ( type_M1690910139scheme @ s2 @ ( type_M876316792e_FVar @ x ) ) )
| ~ ( member_nat @ n @ ( type_M1050318637scheme @ ( type_M876316792e_FVar @ x ) ) )
| ( ( s1 @ n )
= ( s2 @ n ) ) ),
file('/export/starexec/sandbox/tmp/tmp.3Yu0lO2n5o/E---3.1_583945.p',conj_0) ).
thf(fact_3_app__subst__type__scheme_Osimps_I1_J,axiom,
! [X7: nat > type_Mirabelle_typ,X10: nat] :
( ( type_M1690910139scheme @ X7 @ ( type_M876316792e_FVar @ X10 ) )
= ( type_M1006385707scheme @ ( X7 @ X10 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.3Yu0lO2n5o/E---3.1_583945.p',fact_3_app__subst__type__scheme_Osimps_I1_J) ).
thf(fact_35_mk__scheme__injective,axiom,
! [X28: type_Mirabelle_typ,X50: type_Mirabelle_typ] :
( ( ( type_M1006385707scheme @ X28 )
= ( type_M1006385707scheme @ X50 ) )
=> ( X28 = X50 ) ),
file('/export/starexec/sandbox/tmp/tmp.3Yu0lO2n5o/E---3.1_583945.p',fact_35_mk__scheme__injective) ).
thf(fact_15_free__tv__type__scheme_Osimps_I1_J,axiom,
! [X29: nat] :
( ( type_M1050318637scheme @ ( type_M876316792e_FVar @ X29 ) )
= ( insert_nat @ X29 @ bot_bot_set_nat ) ),
file('/export/starexec/sandbox/tmp/tmp.3Yu0lO2n5o/E---3.1_583945.p',fact_15_free__tv__type__scheme_Osimps_I1_J) ).
thf(fact_89_singleton__iff,axiom,
! [X74: nat,X69: nat] :
( ( member_nat @ X74 @ ( insert_nat @ X69 @ bot_bot_set_nat ) )
<=> ( X74 = X69 ) ),
file('/export/starexec/sandbox/tmp/tmp.3Yu0lO2n5o/E---3.1_583945.p',fact_89_singleton__iff) ).
thf(c_0_5,negated_conjecture,
~ ( ( ( type_M1690910139scheme @ s1 @ ( type_M876316792e_FVar @ x ) )
!= ( type_M1690910139scheme @ s2 @ ( type_M876316792e_FVar @ x ) ) )
| ~ ( member_nat @ n @ ( type_M1050318637scheme @ ( type_M876316792e_FVar @ x ) ) )
| ( ( s1 @ n )
= ( s2 @ n ) ) ),
inference(assume_negation,[status(cth)],[conj_0]) ).
thf(c_0_6,negated_conjecture,
~ ( ( ( type_M1690910139scheme @ s1 @ ( type_M876316792e_FVar @ x ) )
!= ( type_M1690910139scheme @ s2 @ ( type_M876316792e_FVar @ x ) ) )
| ~ ( member_nat @ n @ ( type_M1050318637scheme @ ( type_M876316792e_FVar @ x ) ) )
| ( ( s1 @ n )
= ( s2 @ n ) ) ),
inference(fof_simplification,[status(thm)],[c_0_5]) ).
thf(c_0_7,negated_conjecture,
( ( ( type_M1690910139scheme @ s1 @ ( type_M876316792e_FVar @ x ) )
= ( type_M1690910139scheme @ s2 @ ( type_M876316792e_FVar @ x ) ) )
& ( member_nat @ n @ ( type_M1050318637scheme @ ( type_M876316792e_FVar @ x ) ) )
& ( ( s1 @ n )
!= ( s2 @ n ) ) ),
inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_6])]) ).
thf(c_0_8,plain,
! [X1666: nat > type_Mirabelle_typ,X1667: nat] :
( ( type_M1690910139scheme @ X1666 @ ( type_M876316792e_FVar @ X1667 ) )
= ( type_M1006385707scheme @ ( X1666 @ X1667 ) ) ),
inference(variable_rename,[status(thm)],[fact_3_app__subst__type__scheme_Osimps_I1_J]) ).
thf(c_0_9,plain,
! [X1758: type_Mirabelle_typ,X1759: type_Mirabelle_typ] :
( ( ( type_M1006385707scheme @ X1758 )
!= ( type_M1006385707scheme @ X1759 ) )
| ( X1758 = X1759 ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_35_mk__scheme__injective])])]) ).
thf(c_0_10,negated_conjecture,
( ( type_M1690910139scheme @ s1 @ ( type_M876316792e_FVar @ x ) )
= ( type_M1690910139scheme @ s2 @ ( type_M876316792e_FVar @ x ) ) ),
inference(split_conjunct,[status(thm)],[c_0_7]) ).
thf(c_0_11,plain,
! [X4: nat > type_Mirabelle_typ,X1: nat] :
( ( type_M1690910139scheme @ X4 @ ( type_M876316792e_FVar @ X1 ) )
= ( type_M1006385707scheme @ ( X4 @ X1 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_8]) ).
thf(c_0_12,plain,
! [X1697: nat] :
( ( type_M1050318637scheme @ ( type_M876316792e_FVar @ X1697 ) )
= ( insert_nat @ X1697 @ bot_bot_set_nat ) ),
inference(variable_rename,[status(thm)],[fact_15_free__tv__type__scheme_Osimps_I1_J]) ).
thf(c_0_13,plain,
! [X22: type_Mirabelle_typ,X28: type_Mirabelle_typ] :
( ( X22 = X28 )
| ( ( type_M1006385707scheme @ X22 )
!= ( type_M1006385707scheme @ X28 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
thf(c_0_14,negated_conjecture,
( ( type_M1006385707scheme @ ( s1 @ x ) )
= ( type_M1006385707scheme @ ( s2 @ x ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_10,c_0_11]),c_0_11]) ).
thf(c_0_15,plain,
! [X1927: nat,X1928: nat] :
( ( ~ ( member_nat @ X1927 @ ( insert_nat @ X1928 @ bot_bot_set_nat ) )
| ( X1927 = X1928 ) )
& ( ( X1927 != X1928 )
| ( member_nat @ X1927 @ ( insert_nat @ X1928 @ bot_bot_set_nat ) ) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_89_singleton__iff])])]) ).
thf(c_0_16,negated_conjecture,
member_nat @ n @ ( type_M1050318637scheme @ ( type_M876316792e_FVar @ x ) ),
inference(split_conjunct,[status(thm)],[c_0_7]) ).
thf(c_0_17,plain,
! [X1: nat] :
( ( type_M1050318637scheme @ ( type_M876316792e_FVar @ X1 ) )
= ( insert_nat @ X1 @ bot_bot_set_nat ) ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
thf(c_0_18,negated_conjecture,
! [X22: type_Mirabelle_typ] :
( ( X22
= ( s1 @ x ) )
| ( ( type_M1006385707scheme @ X22 )
!= ( type_M1006385707scheme @ ( s2 @ x ) ) ) ),
inference(spm,[status(thm)],[c_0_13,c_0_14]) ).
thf(c_0_19,plain,
! [X1: nat,X2: nat] :
( ( X1 = X2 )
| ~ ( member_nat @ X1 @ ( insert_nat @ X2 @ bot_bot_set_nat ) ) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
thf(c_0_20,negated_conjecture,
member_nat @ n @ ( insert_nat @ x @ bot_bot_set_nat ),
inference(rw,[status(thm)],[c_0_16,c_0_17]) ).
thf(c_0_21,negated_conjecture,
( ( s1 @ x )
= ( s2 @ x ) ),
inference(er,[status(thm)],[c_0_18]) ).
thf(c_0_22,negated_conjecture,
x = n,
inference(spm,[status(thm)],[c_0_19,c_0_20]) ).
thf(c_0_23,negated_conjecture,
( ( s1 @ n )
!= ( s2 @ n ) ),
inference(split_conjunct,[status(thm)],[c_0_7]) ).
thf(c_0_24,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_21,c_0_22]),c_0_22]),c_0_23]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP197^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n018.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 20:12:56 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running higher-order theorem proving
% 0.22/0.29 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.3Yu0lO2n5o/E---3.1_583945.p
% 0.42/0.45 % Version: 3.5.1-ho
% 0.42/0.45 % Preprocessing class: HSLSSMSMSSLCHSA.
% 0.42/0.45 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.42/0.45 % Starting lpo5_fix with 1500s (5) cores
% 0.42/0.45 % Starting lpo8_s with 300s (1) cores
% 0.42/0.45 % Starting sh4 with 300s (1) cores
% 0.42/0.45 % Starting sh2lt with 300s (1) cores
% 0.42/0.45 % lpo5_fix with pid 583958 completed with status 0
% 0.42/0.45 % Result found by lpo5_fix
% 0.42/0.45 % Preprocessing class: HSLSSMSMSSLCHSA.
% 0.42/0.45 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.42/0.45 % Starting lpo5_fix with 1500s (5) cores
% 0.42/0.45 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.42/0.45 % No SInE strategy applied
% 0.42/0.45 % Search class: HGHSM-FSLM32-MHSFFSBC
% 0.42/0.45 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.42/0.45 % Starting SubtermCWHack with 136s (1) cores
% 0.42/0.45 % Starting lpo5_fix with 151s (1) cores
% 0.42/0.45 % Starting post_as_ho12 with 228s (1) cores
% 0.42/0.45 % Starting sh1 with 136s (1) cores
% 0.42/0.45 % Starting almost_fo_4 with 136s (1) cores
% 0.42/0.45 % post_as_ho12 with pid 583976 completed with status 0
% 0.42/0.45 % Result found by post_as_ho12
% 0.42/0.45 % Preprocessing class: HSLSSMSMSSLCHSA.
% 0.42/0.45 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.42/0.45 % Starting lpo5_fix with 1500s (5) cores
% 0.42/0.45 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.42/0.45 % No SInE strategy applied
% 0.42/0.45 % Search class: HGHSM-FSLM32-MHSFFSBC
% 0.42/0.45 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.42/0.45 % Starting SubtermCWHack with 136s (1) cores
% 0.42/0.45 % Starting lpo5_fix with 151s (1) cores
% 0.42/0.45 % Starting post_as_ho12 with 228s (1) cores
% 0.42/0.45 % Preprocessing time : 0.010 s
% 0.42/0.45 % Presaturation interreduction done
% 0.42/0.45
% 0.42/0.45 % Proof found!
% 0.42/0.45 % SZS status Theorem
% 0.42/0.45 % SZS output start CNFRefutation
% See solution above
% 0.42/0.45 % Parsed axioms : 463
% 0.42/0.45 % Removed by relevancy pruning/SinE : 0
% 0.42/0.45 % Initial clauses : 902
% 0.42/0.45 % Removed in clause preprocessing : 134
% 0.42/0.45 % Initial clauses in saturation : 768
% 0.42/0.45 % Processed clauses : 1036
% 0.42/0.45 % ...of these trivial : 8
% 0.42/0.45 % ...subsumed : 141
% 0.42/0.45 % ...remaining for further processing : 887
% 0.42/0.45 % Other redundant clauses eliminated : 140
% 0.42/0.45 % Clauses deleted for lack of memory : 0
% 0.42/0.45 % Backward-subsumed : 1
% 0.42/0.45 % Backward-rewritten : 13
% 0.42/0.45 % Generated clauses : 294
% 0.42/0.45 % ...of the previous two non-redundant : 226
% 0.42/0.45 % ...aggressively subsumed : 0
% 0.42/0.45 % Contextual simplify-reflections : 6
% 0.42/0.45 % Paramodulations : 108
% 0.42/0.45 % Factorizations : 0
% 0.42/0.45 % NegExts : 8
% 0.42/0.45 % Equation resolutions : 148
% 0.42/0.45 % Disequality decompositions : 0
% 0.42/0.45 % Total rewrite steps : 101
% 0.42/0.45 % ...of those cached : 58
% 0.42/0.45 % Propositional unsat checks : 0
% 0.42/0.45 % Propositional check models : 0
% 0.42/0.45 % Propositional check unsatisfiable : 0
% 0.42/0.45 % Propositional clauses : 0
% 0.42/0.45 % Propositional clauses after purity: 0
% 0.42/0.45 % Propositional unsat core size : 0
% 0.42/0.45 % Propositional preprocessing time : 0.000
% 0.42/0.45 % Propositional encoding time : 0.000
% 0.42/0.45 % Propositional solver time : 0.000
% 0.42/0.45 % Success case prop preproc time : 0.000
% 0.42/0.45 % Success case prop encoding time : 0.000
% 0.42/0.45 % Success case prop solver time : 0.000
% 0.42/0.45 % Current number of processed clauses : 144
% 0.42/0.45 % Positive orientable unit clauses : 61
% 0.42/0.45 % Positive unorientable unit clauses: 0
% 0.42/0.45 % Negative unit clauses : 29
% 0.42/0.45 % Non-unit-clauses : 54
% 0.42/0.45 % Current number of unprocessed clauses: 572
% 0.42/0.45 % ...number of literals in the above : 1633
% 0.42/0.45 % Current number of archived formulas : 0
% 0.42/0.45 % Current number of archived clauses : 635
% 0.42/0.45 % Clause-clause subsumption calls (NU) : 59508
% 0.42/0.45 % Rec. Clause-clause subsumption calls : 33757
% 0.42/0.45 % Non-unit clause-clause subsumptions : 94
% 0.42/0.45 % Unit Clause-clause subsumption calls : 739
% 0.42/0.45 % Rewrite failures with RHS unbound : 0
% 0.42/0.45 % BW rewrite match attempts : 271
% 0.42/0.45 % BW rewrite match successes : 35
% 0.42/0.45 % Condensation attempts : 0
% 0.42/0.45 % Condensation successes : 0
% 0.42/0.45 % Termbank termtop insertions : 98793
% 0.42/0.45 % Search garbage collected termcells : 17037
% 0.42/0.45
% 0.42/0.45 % -------------------------------------------------
% 0.42/0.45 % User time : 0.109 s
% 0.42/0.45 % System time : 0.015 s
% 0.42/0.45 % Total time : 0.124 s
% 0.42/0.45 % Maximum resident set size: 7676 pages
% 0.42/0.45
% 0.42/0.45 % -------------------------------------------------
% 0.42/0.45 % User time : 0.362 s
% 0.42/0.45 % System time : 0.060 s
% 0.42/0.45 % Total time : 0.423 s
% 0.42/0.45 % Maximum resident set size: 5888 pages
% 0.42/0.45 % E exiting
%------------------------------------------------------------------------------