%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : COM286_1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n019.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:11:52 PM UTC 2026
% Result : Theorem 0.52s 0.69s
% Output : CNFRefutation 0.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 5
% Syntax : Number of formulae : 28 ( 14 unt; 0 typ; 0 def)
% Number of atoms : 71 ( 34 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 68 ( 25 ~; 12 |; 24 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 7 ( 6 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-3 aty)
% Number of variables : 46 ( 0 sgn 46 !; 0 ?; 46 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
vTStore: $tType ).
tff(decl_sort2,type,
vTable: $tType ).
tff(decl_sort3,type,
vQuery: $tType ).
tff(decl_sort4,type,
vOptQuery: $tType ).
tff(decl_sort5,type,
vTType: $tType ).
tff(decl_sort6,type,
vTTContext: $tType ).
tff(decl_26,type,
vtvalue: vTable > vQuery ).
tff(decl_28,type,
vsomeQuery: vQuery > vOptQuery ).
tff(decl_44,type,
vnoQuery: vOptQuery ).
tff(decl_50,type,
vDifference: ( vQuery * vQuery ) > vQuery ).
tff(decl_53,type,
vq1: vQuery ).
tff(decl_64,type,
vq2: vQuery ).
tff(decl_97,type,
vreduce: ( vTStore * vQuery ) > vOptQuery ).
tff(decl_109,type,
visSomeQuery: vOptQuery > $o ).
tff(decl_110,type,
vstoreContextConsistent: ( vTTContext * vTStore ) > $o ).
tff(decl_112,type,
vptcheck: ( vTType * ( vQuery * vTTContext ) ) > $o ).
tff(decl_120,type,
esk1_0: vQuery ).
tff(decl_121,type,
esk2_0: vTable ).
tff(decl_122,type,
esk3_0: vTTContext ).
tff(decl_123,type,
esk4_0: vTStore ).
tff(decl_124,type,
esk5_0: vTType ).
tff(decl_137,type,
esk18_3: ( vTStore * ( vQuery * vTable ) ) > vTable ).
tff(decl_138,type,
esk19_3: ( vTStore * ( vQuery * vTable ) ) > vTable ).
tff('Preservation-Difference-tvalue-q2-isSomeQuery-False',conjecture,
! [X461: vQuery,X53: vTable,X460: vTTContext,X294: vTStore,X54: vTType] :
( ( ( vreduce(vDifference(vq1,vq2),X294) = vsomeQuery(X461) )
& vptcheck(X460,vDifference(vq1,vq2),X54)
& vstoreContextConsistent(X294,X460)
& ( vq1 = vtvalue(X53) )
& ! [X299: vTable] : ( vq2 != vtvalue(X299) )
& ~ visSomeQuery(vreduce(vq2,X294)) )
=> vptcheck(X460,X461,X54) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Preservation-Difference-tvalue-q2-isSomeQuery-False') ).
tff('reduce-16',axiom,
! [X53: vTable,X297: vQuery,X294: vTStore] :
( ( ~ visSomeQuery(vreduce(X297,X294))
& ! [X298: vTable,X299: vTable] :
( ( X297 != vtvalue(X299) )
| ( X53 != X298 ) ) )
=> ( vreduce(vDifference(vtvalue(X53),X297),X294) = vnoQuery ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','reduce-16') ).
tff('isSomeQuery-false-INV',axiom,
! [X219: vOptQuery] :
( ~ visSomeQuery(X219)
=> ( X219 = vnoQuery ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','isSomeQuery-false-INV') ).
tff('isSomeQuery-1',axiom,
! [X218: vQuery] : visSomeQuery(vsomeQuery(X218)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','isSomeQuery-1') ).
tff('isSomeQuery-0',axiom,
~ visSomeQuery(vnoQuery),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','isSomeQuery-0') ).
tff(c_0_5,negated_conjecture,
~ ! [X461: vQuery,X53: vTable,X460: vTTContext,X294: vTStore,X54: vTType] :
( ( ( vreduce(vDifference(vq1,vq2),X294) = vsomeQuery(X461) )
& vptcheck(X460,vDifference(vq1,vq2),X54)
& vstoreContextConsistent(X294,X460)
& ( vq1 = vtvalue(X53) )
& ! [X299: vTable] : ( vq2 != vtvalue(X299) )
& ~ visSomeQuery(vreduce(vq2,X294)) )
=> vptcheck(X460,X461,X54) ),
inference(assume_negation,[status(cth)],['Preservation-Difference-tvalue-q2-isSomeQuery-False']) ).
tff(c_0_6,negated_conjecture,
~ ! [X461: vQuery,X53: vTable,X460: vTTContext,X294: vTStore,X54: vTType] :
( ( ( vreduce(vDifference(vq1,vq2),X294) = vsomeQuery(X461) )
& vptcheck(X460,vDifference(vq1,vq2),X54)
& vstoreContextConsistent(X294,X460)
& ( vq1 = vtvalue(X53) )
& ! [X299: vTable] : ( vq2 != vtvalue(X299) )
& ~ visSomeQuery(vreduce(vq2,X294)) )
=> vptcheck(X460,X461,X54) ),
inference(fof_simplification,[status(thm)],[c_0_5]) ).
tff(c_0_7,plain,
! [X53: vTable,X297: vQuery,X294: vTStore] :
( ( ~ visSomeQuery(vreduce(X297,X294))
& ! [X298: vTable,X299: vTable] :
( ( X297 != vtvalue(X299) )
| ( X53 != X298 ) ) )
=> ( vreduce(vDifference(vtvalue(X53),X297),X294) = vnoQuery ) ),
inference(fof_simplification,[status(thm)],['reduce-16']) ).
tff(c_0_8,negated_conjecture,
! [X467: vTable] :
( ~ vptcheck(esk3_0,esk1_0,esk5_0)
& ( vreduce(vDifference(vq1,vq2),esk4_0) = vsomeQuery(esk1_0) )
& vptcheck(esk3_0,vDifference(vq1,vq2),esk5_0)
& vstoreContextConsistent(esk4_0,esk3_0)
& ( vq1 = vtvalue(esk2_0) )
& ( vq2 != vtvalue(X467) )
& ~ visSomeQuery(vreduce(vq2,esk4_0)) ),
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_6])])])])]) ).
tff(c_0_9,plain,
! [X556: vTable,X557: vQuery,X558: vTStore] :
( ( ( vreduce(vDifference(vtvalue(X556),X557),X558) = vnoQuery )
| visSomeQuery(vreduce(X557,X558))
| ( X557 = vtvalue(esk19_3(X556,X557,X558)) ) )
& ( ( vreduce(vDifference(vtvalue(X556),X557),X558) = vnoQuery )
| visSomeQuery(vreduce(X557,X558))
| ( X556 = esk18_3(X556,X557,X558) ) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_7])])])])]) ).
tff(c_0_10,plain,
! [X219: vOptQuery] :
( ~ visSomeQuery(X219)
=> ( X219 = vnoQuery ) ),
inference(fof_simplification,[status(thm)],['isSomeQuery-false-INV']) ).
tff(c_0_11,plain,
! [X522: vQuery] : visSomeQuery(vsomeQuery(X522)),
inference(variable_rename,[status(thm)],['isSomeQuery-1']) ).
tcf(c_0_12,negated_conjecture,
! [X5: vTable] : vq2 != vtvalue(X5),
inference(split_conjunct,[status(thm)],[c_0_8]) ).
tcf(c_0_13,plain,
! [X4: vQuery,X5: vTable,X47: vTStore] :
( ( vreduce(vDifference(vtvalue(X5),X4),X47) = vnoQuery )
| visSomeQuery(vreduce(X4,X47))
| ( X4 = vtvalue(esk19_3(X5,X4,X47)) ) ),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
tff(c_0_14,plain,
! [X616: vOptQuery] :
( ( X616 = vnoQuery )
| visSomeQuery(X616) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_10])]) ).
tff(c_0_15,plain,
~ visSomeQuery(vnoQuery),
inference(fof_simplification,[status(thm)],['isSomeQuery-0']) ).
tcf(c_0_16,plain,
! [X4: vQuery] : visSomeQuery(vsomeQuery(X4)),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
tcf(c_0_17,negated_conjecture,
vreduce(vDifference(vq1,vq2),esk4_0) = vsomeQuery(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_8]) ).
tcf(c_0_18,negated_conjecture,
! [X5: vTable,X47: vTStore] :
( visSomeQuery(vreduce(vq2,X47))
| ( vreduce(vDifference(vtvalue(X5),vq2),X47) = vnoQuery ) ),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_12,c_0_13])]) ).
tcf(c_0_19,negated_conjecture,
vq1 = vtvalue(esk2_0),
inference(split_conjunct,[status(thm)],[c_0_8]) ).
tcf(c_0_20,negated_conjecture,
~ visSomeQuery(vreduce(vq2,esk4_0)),
inference(split_conjunct,[status(thm)],[c_0_8]) ).
tcf(c_0_21,plain,
! [X36: vOptQuery] :
( ( X36 = vnoQuery )
| visSomeQuery(X36) ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
tff(c_0_22,plain,
~ visSomeQuery(vnoQuery),
inference(fof_nnf,[status(thm)],[c_0_15]) ).
tcf(c_0_23,negated_conjecture,
visSomeQuery(vreduce(vDifference(vq1,vq2),esk4_0)),
inference(spm,[status(thm)],[c_0_16,c_0_17]) ).
tcf(c_0_24,negated_conjecture,
! [X47: vTStore] :
( visSomeQuery(vreduce(vq2,X47))
| ( vreduce(vDifference(vq1,vq2),X47) = vnoQuery ) ),
inference(spm,[status(thm)],[c_0_18,c_0_19]) ).
tcf(c_0_25,negated_conjecture,
vreduce(vq2,esk4_0) = vnoQuery,
inference(spm,[status(thm)],[c_0_20,c_0_21]) ).
tcf(c_0_26,plain,
~ visSomeQuery(vnoQuery),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_27,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23,c_0_24]),c_0_25])]),c_0_26]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : COM286_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.07 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.17/0.43 % Computer : n019.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 14:22:20 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.27/0.50 Running first-order theorem proving
% 0.27/0.50 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
% 0.52/0.69 % Version: 3.5.1
% 0.52/0.69 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.52/0.69 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.52/0.69 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.52/0.69 % Starting new_bool_3 with 300s (1) cores
% 0.52/0.69 % Starting new_bool_1 with 300s (1) cores
% 0.52/0.69 % Starting sh5l with 300s (1) cores
% 0.52/0.69 % new_bool_3 with pid 2805839 completed with status 0
% 0.52/0.69 % Result found by new_bool_3
% 0.52/0.69 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.52/0.69 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.52/0.69 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.52/0.69 % Starting new_bool_3 with 300s (1) cores
% 0.52/0.69 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.52/0.69 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.52/0.69 % Search class: FGUSM-FSLM31-MFFFFFNN
% 0.52/0.69 % partial match(1): FGHSM-FSLM31-MFFFFFNN
% 0.52/0.69 % Scheduled 8 strats onto 1 cores with 300 seconds (300 total)
% 0.52/0.69 % Starting SubtermCWHack with 28s (1) cores
% 0.52/0.69 % SubtermCWHack with pid 2805842 completed with status 0
% 0.52/0.69 % Result found by SubtermCWHack
% 0.52/0.69 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.52/0.69 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.52/0.69 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.52/0.69 % Starting new_bool_3 with 300s (1) cores
% 0.52/0.69 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.52/0.69 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.52/0.69 % Search class: FGUSM-FSLM31-MFFFFFNN
% 0.52/0.69 % partial match(1): FGHSM-FSLM31-MFFFFFNN
% 0.52/0.69 % Scheduled 8 strats onto 1 cores with 300 seconds (300 total)
% 0.52/0.69 % Starting SubtermCWHack with 28s (1) cores
% 0.52/0.69 % Preprocessing time : 0.004 s
% 0.52/0.69
% 0.52/0.69 % Proof found!
% 0.52/0.69 % SZS status Theorem
% 0.52/0.69 % SZS output start CNFRefutation
% See solution above
% 0.52/0.69 % Parsed axioms : 412
% 0.52/0.69 % Removed by relevancy pruning/SinE : 316
% 0.52/0.69 % Initial clauses : 288
% 0.52/0.69 % Removed in clause preprocessing : 0
% 0.52/0.69 % Initial clauses in saturation : 288
% 0.52/0.69 % Processed clauses : 1487
% 0.52/0.69 % ...of these trivial : 19
% 0.52/0.69 % ...subsumed : 832
% 0.52/0.69 % ...remaining for further processing : 636
% 0.52/0.69 % Other redundant clauses eliminated : 540
% 0.52/0.69 % Clauses deleted for lack of memory : 0
% 0.52/0.69 % Backward-subsumed : 31
% 0.52/0.69 % Backward-rewritten : 18
% 0.52/0.69 % Generated clauses : 6987
% 0.52/0.69 % ...of the previous two non-redundant : 6110
% 0.52/0.69 % ...aggressively subsumed : 0
% 0.52/0.69 % Contextual simplify-reflections : 3
% 0.52/0.69 % Paramodulations : 6414
% 0.52/0.69 % Factorizations : 3
% 0.52/0.69 % NegExts : 0
% 0.52/0.69 % Equation resolutions : 570
% 0.52/0.69 % Disequality decompositions : 0
% 0.52/0.69 % Total rewrite steps : 415
% 0.52/0.69 % ...of those cached : 327
% 0.52/0.69 % Propositional unsat checks : 0
% 0.52/0.69 % Propositional check models : 0
% 0.52/0.69 % Propositional check unsatisfiable : 0
% 0.52/0.69 % Propositional clauses : 0
% 0.52/0.69 % Propositional clauses after purity: 0
% 0.52/0.69 % Propositional unsat core size : 0
% 0.52/0.69 % Propositional preprocessing time : 0.000
% 0.52/0.69 % Propositional encoding time : 0.000
% 0.52/0.69 % Propositional solver time : 0.000
% 0.52/0.69 % Success case prop preproc time : 0.000
% 0.52/0.69 % Success case prop encoding time : 0.000
% 0.52/0.69 % Success case prop solver time : 0.000
% 0.52/0.69 % Current number of processed clauses : 586
% 0.52/0.69 % Positive orientable unit clauses : 52
% 0.52/0.69 % Positive unorientable unit clauses: 4
% 0.52/0.69 % Negative unit clauses : 24
% 0.52/0.69 % Non-unit-clauses : 506
% 0.52/0.69 % Current number of unprocessed clauses: 4866
% 0.52/0.69 % ...number of literals in the above : 19513
% 0.52/0.69 % Current number of archived formulas : 0
% 0.52/0.69 % Current number of archived clauses : 49
% 0.52/0.69 % Clause-clause subsumption calls (NU) : 61004
% 0.52/0.69 % Rec. Clause-clause subsumption calls : 49455
% 0.52/0.69 % Non-unit clause-clause subsumptions : 763
% 0.52/0.69 % Unit Clause-clause subsumption calls : 2305
% 0.52/0.69 % Rewrite failures with RHS unbound : 127
% 0.52/0.69 % BW rewrite match attempts : 39
% 0.52/0.69 % BW rewrite match successes : 34
% 0.52/0.69 % Condensation attempts : 0
% 0.52/0.69 % Condensation successes : 0
% 0.52/0.69 % Termbank termtop insertions : 77078
% 0.52/0.69 % Search garbage collected termcells : 5740
% 0.52/0.69
% 0.52/0.69 % -------------------------------------------------
% 0.52/0.69 % User time : 0.131 s
% 0.52/0.69 % System time : 0.011 s
% 0.52/0.69 % Total time : 0.142 s
% 0.52/0.69 % Maximum resident set size: 4928 pages
% 0.52/0.69
% 0.52/0.69 % -------------------------------------------------
% 0.52/0.69 % User time : 0.157 s
% 0.52/0.69 % System time : 0.017 s
% 0.52/0.69 % Total time : 0.174 s
% 0.52/0.69 % Maximum resident set size: 5376 pages
% 0.52/0.69 % E exiting
%------------------------------------------------------------------------------