%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP207_1 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n013.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:54:31 PM UTC 2026
% Result : Theorem 3.46s 2.21s
% Output : CNFRefutation 3.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 5
% Syntax : Number of formulae : 20 ( 13 unt; 0 typ; 0 def)
% Number of atoms : 27 ( 12 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 19 ( 12 ~; 4 |; 0 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 14 ( 13 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-2 aty)
% Number of variables : 21 ( 0 sgn 21 !; 0 ?; 21 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
nat: $tType ).
tff(decl_sort2,type,
heap_Time_Heap_a: $tType ).
tff(decl_sort3,type,
fun_he6201055237484778573t_bool: $tType ).
tff(decl_sort4,type,
fun_he1921015881043195817it_nat: $tType ).
tff(decl_sort5,type,
a: $tType ).
tff(decl_sort6,type,
fun_a_6093291656547882009Heap_a: $tType ).
tff(decl_sort7,type,
bool: $tType ).
tff(decl_sort8,type,
heap_e7401611519738050253t_unit: $tType ).
tff(decl_sort9,type,
fun_a_bool: $tType ).
tff(decl_sort10,type,
option3562590408128118217it_nat: $tType ).
tff(decl_sort11,type,
fun_Pr2403869735082759103it_nat: $tType ).
tff(decl_sort12,type,
produc3260487557148687353it_nat: $tType ).
tff(decl_sort13,type,
produc6653097349344004940it_nat: $tType ).
tff(decl_1198,type,
one_one_nat: nat ).
tff(decl_1302,type,
heap_Time_assert_a: fun_a_bool > fun_a_6093291656547882009Heap_a ).
tff(decl_1310,type,
heap_Time_execute_a: heap_Time_Heap_a > fun_he1921015881043195817it_nat ).
tff(decl_1320,type,
heap_Time_success_a: heap_Time_Heap_a > fun_he6201055237484778573t_bool ).
tff(decl_1512,type,
none_P2651198173097904984it_nat: option3562590408128118217it_nat ).
tff(decl_1515,type,
some_P7913643980934408916it_nat: fun_Pr2403869735082759103it_nat ).
tff(decl_1629,type,
produc584006145561248582it_nat: ( nat * heap_e7401611519738050253t_unit ) > produc6653097349344004940it_nat ).
tff(decl_1653,type,
produc9178034014595674355it_nat: ( produc6653097349344004940it_nat * a ) > produc3260487557148687353it_nat ).
tff(decl_2050,type,
aa_hea1793595068369496646t_bool: ( heap_e7401611519738050253t_unit * fun_he6201055237484778573t_bool ) > bool ).
tff(decl_2052,type,
aa_hea4724376117875161946it_nat: ( heap_e7401611519738050253t_unit * fun_he1921015881043195817it_nat ) > option3562590408128118217it_nat ).
tff(decl_2273,type,
aa_Pro5302094286594872192it_nat: ( produc3260487557148687353it_nat * fun_Pr2403869735082759103it_nat ) > option3562590408128118217it_nat ).
tff(decl_2597,type,
aa_a_bool: ( a * fun_a_bool ) > bool ).
tff(decl_2599,type,
aa_a_H8829438773920479562Heap_a: ( a * fun_a_6093291656547882009Heap_a ) > heap_Time_Heap_a ).
tff(decl_2645,type,
pp: bool > $o ).
tff(decl_2646,type,
p: fun_a_bool ).
tff(decl_2647,type,
h: heap_e7401611519738050253t_unit ).
tff(decl_2648,type,
x: a ).
tff(conj_1,conjecture,
pp(aa_hea1793595068369496646t_bool(heap_Time_success_a(aa_a_H8829438773920479562Heap_a(heap_Time_assert_a(p),x)),h)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1) ).
tff(fact_10_successI,axiom,
! [X21: heap_Time_Heap_a,X3: heap_e7401611519738050253t_unit] :
( ( aa_hea4724376117875161946it_nat(heap_Time_execute_a(X21),X3) != none_P2651198173097904984it_nat )
=> pp(aa_hea1793595068369496646t_bool(heap_Time_success_a(X21),X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_successI) ).
tff(fact_76_option_Odistinct_I1_J,axiom,
! [X155: produc3260487557148687353it_nat] : ( none_P2651198173097904984it_nat != aa_Pro5302094286594872192it_nat(some_P7913643980934408916it_nat,X155) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_option_Odistinct_I1_J) ).
tff(fact_350_execute__assert_I1_J,axiom,
! [X891: fun_a_bool,X8: a,X3: heap_e7401611519738050253t_unit] :
( pp(aa_a_bool(X891,X8))
=> ( aa_hea4724376117875161946it_nat(heap_Time_execute_a(aa_a_H8829438773920479562Heap_a(heap_Time_assert_a(X891),X8)),X3) = aa_Pro5302094286594872192it_nat(some_P7913643980934408916it_nat,produc9178034014595674355it_nat(X8,produc584006145561248582it_nat(X3,one_one_nat))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_350_execute__assert_I1_J) ).
tff(conj_0,hypothesis,
pp(aa_a_bool(p,x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
tff(c_0_5,negated_conjecture,
~ pp(aa_hea1793595068369496646t_bool(heap_Time_success_a(aa_a_H8829438773920479562Heap_a(heap_Time_assert_a(p),x)),h)),
inference(assume_negation,[status(cth)],[conj_1]) ).
tff(c_0_6,negated_conjecture,
~ pp(aa_hea1793595068369496646t_bool(heap_Time_success_a(aa_a_H8829438773920479562Heap_a(heap_Time_assert_a(p),x)),h)),
inference(fof_simplification,[status(thm)],[c_0_5]) ).
tff(c_0_7,plain,
! [X21: heap_Time_Heap_a,X3: heap_e7401611519738050253t_unit] :
( ( aa_hea4724376117875161946it_nat(heap_Time_execute_a(X21),X3) != none_P2651198173097904984it_nat )
=> pp(aa_hea1793595068369496646t_bool(heap_Time_success_a(X21),X3)) ),
inference(fof_simplification,[status(thm)],[fact_10_successI]) ).
tff(c_0_8,negated_conjecture,
~ pp(aa_hea1793595068369496646t_bool(heap_Time_success_a(aa_a_H8829438773920479562Heap_a(heap_Time_assert_a(p),x)),h)),
inference(fof_nnf,[status(thm)],[c_0_6]) ).
tff(c_0_9,plain,
! [X17152: heap_Time_Heap_a,X17153: heap_e7401611519738050253t_unit] :
( pp(aa_hea1793595068369496646t_bool(heap_Time_success_a(X17152),X17153))
| ( aa_hea4724376117875161946it_nat(heap_Time_execute_a(X17152),X17153) = none_P2651198173097904984it_nat ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_7])]) ).
tff(c_0_10,plain,
! [X155: produc3260487557148687353it_nat] : ( none_P2651198173097904984it_nat != aa_Pro5302094286594872192it_nat(some_P7913643980934408916it_nat,X155) ),
inference(fof_simplification,[status(thm)],[fact_76_option_Odistinct_I1_J]) ).
tcf(c_0_11,negated_conjecture,
~ pp(aa_hea1793595068369496646t_bool(heap_Time_success_a(aa_a_H8829438773920479562Heap_a(heap_Time_assert_a(p),x)),h)),
inference(split_conjunct,[status(thm)],[c_0_8]) ).
tcf(c_0_12,plain,
! [X2: heap_Time_Heap_a,X3: heap_e7401611519738050253t_unit] :
( pp(aa_hea1793595068369496646t_bool(heap_Time_success_a(X2),X3))
| ( aa_hea4724376117875161946it_nat(heap_Time_execute_a(X2),X3) = none_P2651198173097904984it_nat ) ),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
tff(c_0_13,plain,
! [X17139: fun_a_bool,X17140: a,X17141: heap_e7401611519738050253t_unit] :
( ( aa_hea4724376117875161946it_nat(heap_Time_execute_a(aa_a_H8829438773920479562Heap_a(heap_Time_assert_a(X17139),X17140)),X17141) = aa_Pro5302094286594872192it_nat(some_P7913643980934408916it_nat,produc9178034014595674355it_nat(X17140,produc584006145561248582it_nat(X17141,one_one_nat))) )
| ~ pp(aa_a_bool(X17139,X17140)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_350_execute__assert_I1_J])])]) ).
tff(c_0_14,plain,
! [X17184: produc3260487557148687353it_nat] : ( none_P2651198173097904984it_nat != aa_Pro5302094286594872192it_nat(some_P7913643980934408916it_nat,X17184) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_10])]) ).
tcf(c_0_15,negated_conjecture,
aa_hea4724376117875161946it_nat(heap_Time_execute_a(aa_a_H8829438773920479562Heap_a(heap_Time_assert_a(p),x)),h) = none_P2651198173097904984it_nat,
inference(spm,[status(thm)],[c_0_11,c_0_12]) ).
tcf(c_0_16,plain,
! [X3: heap_e7401611519738050253t_unit,X18: fun_a_bool,X8: a] :
( ~ pp(aa_a_bool(X18,X8))
| ( aa_hea4724376117875161946it_nat(heap_Time_execute_a(aa_a_H8829438773920479562Heap_a(heap_Time_assert_a(X18),X8)),X3) = aa_Pro5302094286594872192it_nat(some_P7913643980934408916it_nat,produc9178034014595674355it_nat(X8,produc584006145561248582it_nat(X3,one_one_nat))) ) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
tcf(c_0_17,hypothesis,
pp(aa_a_bool(p,x)),
inference(split_conjunct,[status(thm)],[conj_0]) ).
tcf(c_0_18,plain,
! [X50: produc3260487557148687353it_nat] : none_P2651198173097904984it_nat != aa_Pro5302094286594872192it_nat(some_P7913643980934408916it_nat,X50),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
cnf(c_0_19,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_15,c_0_16]),c_0_17])]),c_0_18]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP207_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.06 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n013.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 20 22:06:36 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.45 Running first-order theorem proving
% 0.13/0.45 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
% 3.46/2.21 % Version: 3.5.1
% 3.46/2.21 % Preprocessing class: FMLLSMLLSSSNFFN.
% 3.46/2.21 % Scheduled 4 strats onto 8 cores with 299 seconds (2392 total)
% 3.46/2.21 % Starting new_bool_3 with 897s (3) cores
% 3.46/2.21 % Starting new_bool_1 with 897s (3) cores
% 3.46/2.21 % Starting sh5l with 299s (1) cores
% 3.46/2.21 % Starting G-E--_301_C18_F1_URBAN_S5PRR_RG_S0Y with 299s (1) cores
% 3.46/2.21 % new_bool_1 with pid 3495628 completed with status 0
% 3.46/2.21 % Result found by new_bool_1
% 3.46/2.21 % Preprocessing class: FMLLSMLLSSSNFFN.
% 3.46/2.21 % Scheduled 4 strats onto 8 cores with 299 seconds (2392 total)
% 3.46/2.21 % Starting new_bool_3 with 897s (3) cores
% 3.46/2.21 % Starting new_bool_1 with 897s (3) cores
% 3.46/2.21 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 3.46/2.21 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 3.46/2.21 % Search class: FGHSM-FSLM31-DFFFFFNN
% 3.46/2.21 % Scheduled 7 strats onto 3 cores with 897 seconds (897 total)
% 3.46/2.21 % Starting SubtermCWHack with 81s (1) cores
% 3.46/2.21 % Starting new_bool_1 with 90s (1) cores
% 3.46/2.21 % Starting C07_19_nc_SAT001_MinMin_p005000_rr with 212s (1) cores
% 3.46/2.21 % SubtermCWHack with pid 3495631 completed with status 0
% 3.46/2.21 % Result found by SubtermCWHack
% 3.46/2.21 % Preprocessing class: FMLLSMLLSSSNFFN.
% 3.46/2.21 % Scheduled 4 strats onto 8 cores with 299 seconds (2392 total)
% 3.46/2.21 % Starting new_bool_3 with 897s (3) cores
% 3.46/2.21 % Starting new_bool_1 with 897s (3) cores
% 3.46/2.21 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 3.46/2.21 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 3.46/2.21 % Search class: FGHSM-FSLM31-DFFFFFNN
% 3.46/2.21 % Scheduled 7 strats onto 3 cores with 897 seconds (897 total)
% 3.46/2.21 % Starting SubtermCWHack with 81s (1) cores
% 3.46/2.21 % Preprocessing time : 0.020 s
% 3.46/2.21
% 3.46/2.21 % Proof found!
% 3.46/2.21 % SZS status Theorem
% 3.46/2.21 % SZS output start CNFRefutation
% See solution above
% 3.46/2.21 % Parsed axioms : 12423
% 3.46/2.21 % Removed by relevancy pruning/SinE : 11868
% 3.46/2.21 % Initial clauses : 850
% 3.46/2.21 % Removed in clause preprocessing : 28
% 3.46/2.21 % Initial clauses in saturation : 822
% 3.46/2.21 % Processed clauses : 1518
% 3.46/2.21 % ...of these trivial : 84
% 3.46/2.21 % ...subsumed : 859
% 3.46/2.21 % ...remaining for further processing : 575
% 3.46/2.21 % Other redundant clauses eliminated : 249
% 3.46/2.21 % Clauses deleted for lack of memory : 0
% 3.46/2.21 % Backward-subsumed : 15
% 3.46/2.21 % Backward-rewritten : 16
% 3.46/2.21 % Generated clauses : 4959
% 3.46/2.21 % ...of the previous two non-redundant : 3604
% 3.46/2.21 % ...aggressively subsumed : 0
% 3.46/2.21 % Contextual simplify-reflections : 0
% 3.46/2.21 % Paramodulations : 4710
% 3.46/2.21 % Factorizations : 4
% 3.46/2.21 % NegExts : 0
% 3.46/2.21 % Equation resolutions : 256
% 3.46/2.21 % Disequality decompositions : 0
% 3.46/2.21 % Total rewrite steps : 2266
% 3.46/2.21 % ...of those cached : 1960
% 3.46/2.21 % Propositional unsat checks : 0
% 3.46/2.21 % Propositional check models : 0
% 3.46/2.21 % Propositional check unsatisfiable : 0
% 3.46/2.21 % Propositional clauses : 0
% 3.46/2.21 % Propositional clauses after purity: 0
% 3.46/2.21 % Propositional unsat core size : 0
% 3.46/2.21 % Propositional preprocessing time : 0.000
% 3.46/2.21 % Propositional encoding time : 0.000
% 3.46/2.21 % Propositional solver time : 0.000
% 3.46/2.21 % Success case prop preproc time : 0.000
% 3.46/2.21 % Success case prop encoding time : 0.000
% 3.46/2.21 % Success case prop solver time : 0.000
% 3.46/2.21 % Current number of processed clauses : 468
% 3.46/2.21 % Positive orientable unit clauses : 141
% 3.46/2.21 % Positive unorientable unit clauses: 6
% 3.46/2.21 % Negative unit clauses : 53
% 3.46/2.21 % Non-unit-clauses : 268
% 3.46/2.21 % Current number of unprocessed clauses: 2792
% 3.46/2.21 % ...number of literals in the above : 6520
% 3.46/2.21 % Current number of archived formulas : 0
% 3.46/2.21 % Current number of archived clauses : 31
% 3.46/2.21 % Clause-clause subsumption calls (NU) : 19479
% 3.46/2.21 % Rec. Clause-clause subsumption calls : 17672
% 3.46/2.21 % Non-unit clause-clause subsumptions : 420
% 3.46/2.21 % Unit Clause-clause subsumption calls : 2807
% 3.46/2.21 % Rewrite failures with RHS unbound : 0
% 3.46/2.21 % BW rewrite match attempts : 863
% 3.46/2.21 % BW rewrite match successes : 44
% 3.46/2.21 % Condensation attempts : 0
% 3.46/2.21 % Condensation successes : 0
% 3.46/2.21 % Termbank termtop insertions : 299715
% 3.46/2.21 % Search garbage collected termcells : 117365
% 3.46/2.21
% 3.46/2.21 % -------------------------------------------------
% 3.46/2.21 % User time : 0.363 s
% 3.46/2.21 % System time : 0.085 s
% 3.46/2.21 % Total time : 0.447 s
% 3.46/2.21 % Maximum resident set size: 32468 pages
% 3.46/2.21
% 3.46/2.21 % -------------------------------------------------
% 3.46/2.21 % User time : 1.858 s
% 3.46/2.21 % System time : 0.199 s
% 3.46/2.21 % Total time : 2.057 s
% 3.46/2.21 % Maximum resident set size: 28416 pages
% 3.46/2.21 % E exiting
%------------------------------------------------------------------------------