%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : COM280_1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:51 PM UTC 2026
% Result : Theorem 0.17s 0.65s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 5
% Syntax : Number of formulae : 22 ( 11 unt; 0 typ; 0 def)
% Number of atoms : 56 ( 27 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 65 ( 31 ~; 20 |; 9 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 7 ( 6 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-3 aty)
% Number of variables : 54 ( 0 sgn 54 !; 0 ?; 54 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
vRow: $tType ).
tff(decl_sort2,type,
vVal: $tType ).
tff(decl_sort3,type,
vName: $tType ).
tff(decl_sort4,type,
vFType: $tType ).
tff(decl_sort5,type,
vTType: $tType ).
tff(decl_sort6,type,
vRawTable: $tType ).
tff(decl_23,type,
vrempty: vRow ).
tff(decl_31,type,
vrcons: ( vRow * vVal ) > vRow ).
tff(decl_32,type,
vttcons: ( vTType * ( vFType * vName ) ) > vTType ).
tff(decl_37,type,
vtcons: ( vRawTable * vRow ) > vRawTable ).
tff(decl_42,type,
vrt2: vRawTable ).
tff(decl_49,type,
vttempty: vTType ).
tff(decl_79,type,
vwelltypedRawtable: ( vRawTable * vTType ) > $o ).
tff(decl_100,type,
vdropFirstColRaw: vRawTable > vRawTable ).
tff(decl_106,type,
vwelltypedRow: ( vRow * vTType ) > $o ).
tff(decl_120,type,
esk1_0: vName ).
tff(decl_121,type,
esk2_0: vFType ).
tff(decl_122,type,
esk3_0: vTType ).
tff(decl_157,type,
esk38_2: ( vRow * vTType ) > vName ).
tff(decl_158,type,
esk39_2: ( vRow * vTType ) > vFType ).
tff(decl_159,type,
esk40_2: ( vRow * vTType ) > vTType ).
tff(decl_160,type,
esk41_2: ( vRow * vTType ) > vVal ).
tff(decl_161,type,
esk42_2: ( vRow * vTType ) > vRow ).
tff('DIFF-rempty-rcons',axiom,
! [X31: vVal,X32: vRow] : ( vrempty != vrcons(X31,X32) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-rempty-rcons') ).
tff('welltypedRow-2',axiom,
! [X89: vTType,X90: vRow] :
( ( ( ! [X93: vVal,X94: vRow] : ( X90 != vrcons(X93,X94) )
| ! [X91: vName,X92: vFType,X80: vTType] : ( X89 != vttcons(X91,X92,X80) ) )
& ( ( X90 != vrempty )
| ( X89 != vttempty ) ) )
=> ~ vwelltypedRow(X89,X90) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','welltypedRow-2') ).
tff('dropFirstColRawPreservesWelltypedRaw-tcons-rempty',conjecture,
! [X179: vName,X86: vFType,X460: vTType] :
( vwelltypedRawtable(vttcons(X179,X86,X460),vtcons(vrempty,vrt2))
=> vwelltypedRawtable(X460,vdropFirstColRaw(vtcons(vrempty,vrt2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dropFirstColRawPreservesWelltypedRaw-tcons-rempty') ).
tff('welltypedRawtable-1',axiom,
! [X54: vTType,X88: vRow,X101: vRawTable] :
( vwelltypedRawtable(X54,vtcons(X88,X101))
<=> ( vwelltypedRawtable(X54,X101)
& vwelltypedRow(X54,X88) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','welltypedRawtable-1') ).
tff('DIFF-ttempty-ttcons',axiom,
! [X7: vName,X19: vFType,X20: vTType] : ( vttempty != vttcons(X7,X19,X20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-ttempty-ttcons') ).
tff(c_0_5,plain,
! [X31: vVal,X32: vRow] : ( vrempty != vrcons(X31,X32) ),
inference(fof_simplification,[status(thm)],['DIFF-rempty-rcons']) ).
tff(c_0_6,plain,
! [X89: vTType,X90: vRow] :
( ( ( ! [X93: vVal,X94: vRow] : ( X90 != vrcons(X93,X94) )
| ! [X91: vName,X92: vFType,X80: vTType] : ( X89 != vttcons(X91,X92,X80) ) )
& ( ( X90 != vrempty )
| ( X89 != vttempty ) ) )
=> ~ vwelltypedRow(X89,X90) ),
inference(fof_simplification,[status(thm)],['welltypedRow-2']) ).
tff(c_0_7,negated_conjecture,
~ ! [X179: vName,X86: vFType,X460: vTType] :
( vwelltypedRawtable(vttcons(X179,X86,X460),vtcons(vrempty,vrt2))
=> vwelltypedRawtable(X460,vdropFirstColRaw(vtcons(vrempty,vrt2))) ),
inference(assume_negation,[status(cth)],['dropFirstColRawPreservesWelltypedRaw-tcons-rempty']) ).
tff(c_0_8,plain,
! [X533: vVal,X534: vRow] : ( vrempty != vrcons(X533,X534) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_5])]) ).
tff(c_0_9,plain,
! [X548: vTType,X549: vRow] :
( ( ~ vwelltypedRow(X548,X549)
| ( X549 = vrempty )
| ( X549 = vrcons(esk41_2(X548,X549),esk42_2(X548,X549)) ) )
& ( ~ vwelltypedRow(X548,X549)
| ( X549 = vrempty )
| ( X548 = vttcons(esk38_2(X548,X549),esk39_2(X548,X549),esk40_2(X548,X549)) ) )
& ( ~ vwelltypedRow(X548,X549)
| ( X548 = vttempty )
| ( X549 = vrcons(esk41_2(X548,X549),esk42_2(X548,X549)) ) )
& ( ~ vwelltypedRow(X548,X549)
| ( X548 = vttempty )
| ( X548 = vttcons(esk38_2(X548,X549),esk39_2(X548,X549),esk40_2(X548,X549)) ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_6])])])])]) ).
tff(c_0_10,plain,
! [X465: vTType,X466: vRow,X467: vRawTable] :
( ( vwelltypedRawtable(X465,vtcons(X466,X467))
| ~ vwelltypedRawtable(X465,X467)
| ~ vwelltypedRow(X465,X466) )
& ( ~ vwelltypedRawtable(X465,vtcons(X466,X467))
| vwelltypedRawtable(X465,X467) )
& ( ~ vwelltypedRawtable(X465,vtcons(X466,X467))
| vwelltypedRow(X465,X466) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['welltypedRawtable-1'])])])]) ).
tff(c_0_11,negated_conjecture,
( ~ vwelltypedRawtable(esk3_0,vdropFirstColRaw(vtcons(vrempty,vrt2)))
& vwelltypedRawtable(vttcons(esk1_0,esk2_0,esk3_0),vtcons(vrempty,vrt2)) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_7])])])]) ).
tff(c_0_12,plain,
! [X7: vName,X19: vFType,X20: vTType] : ( vttempty != vttcons(X7,X19,X20) ),
inference(fof_simplification,[status(thm)],['DIFF-ttempty-ttcons']) ).
tcf(c_0_13,plain,
! [X31: vVal,X30: vRow] : vrempty != vrcons(X31,X30),
inference(split_conjunct,[status(thm)],[c_0_8]) ).
tcf(c_0_14,plain,
! [X18: vTType,X30: vRow] :
( ~ vwelltypedRow(X18,X30)
| ( X18 = vttempty )
| ( X30 = vrcons(esk41_2(X18,X30),esk42_2(X18,X30)) ) ),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
tcf(c_0_15,plain,
! [X18: vTType,X30: vRow,X27: vRawTable] :
( ~ vwelltypedRawtable(X18,vtcons(X30,X27))
| vwelltypedRow(X18,X30) ),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
tcf(c_0_16,negated_conjecture,
vwelltypedRawtable(vttcons(esk1_0,esk2_0,esk3_0),vtcons(vrempty,vrt2)),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
tff(c_0_17,plain,
! [X545: vName,X546: vFType,X547: vTType] : ( vttempty != vttcons(X545,X546,X547) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_12])]) ).
tcf(c_0_18,plain,
! [X18: vTType] :
( ~ vwelltypedRow(X18,vrempty)
| ( X18 = vttempty ) ),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_13,c_0_14])]) ).
tcf(c_0_19,negated_conjecture,
vwelltypedRow(vttcons(esk1_0,esk2_0,esk3_0),vrempty),
inference(spm,[status(thm)],[c_0_15,c_0_16]) ).
tcf(c_0_20,plain,
! [X7: vName,X19: vFType,X18: vTType] : vttempty != vttcons(X7,X19,X18),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_21,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_18,c_0_19]),c_0_20]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM280_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.52 % Computer : n005.cluster.edu
% 0.11/0.52 % Model : x86_64 x86_64
% 0.11/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.52 % Memory : 8046.5625MB
% 0.11/0.52 % OS : Linux 6.8.0-71-generic
% 0.11/0.52 % CPULimit : 300
% 0.11/0.52 % WCLimit : 300
% 0.11/0.52 % DateTime : Mon Sep 21 14:22:19 UTC 2026
% 0.11/0.52 % CPUTime :
% 0.11/0.52 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.56 Running first-order theorem proving
% 0.17/0.56 Running: /export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p
% 0.17/0.65 % Version: 3.5.1
% 0.17/0.65 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.17/0.65 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.17/0.65 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.17/0.65 % Starting new_bool_3 with 300s (1) cores
% 0.17/0.65 % Starting new_bool_1 with 300s (1) cores
% 0.17/0.65 % Starting sh5l with 300s (1) cores
% 0.17/0.65 % new_bool_1 with pid 3720808 completed with status 0
% 0.17/0.65 % Result found by new_bool_1
% 0.17/0.65 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.17/0.65 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.17/0.65 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.17/0.65 % Starting new_bool_3 with 300s (1) cores
% 0.17/0.65 % Starting new_bool_1 with 300s (1) cores
% 0.17/0.65 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.17/0.65 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.17/0.65 % Search class: FGUSM-FSLM31-MFFFFFNN
% 0.17/0.65 % partial match(1): FGHSM-FSLM31-MFFFFFNN
% 0.17/0.65 % Scheduled 8 strats onto 1 cores with 300 seconds (300 total)
% 0.17/0.65 % Starting SubtermCWHack with 28s (1) cores
% 0.17/0.65 % SubtermCWHack with pid 3720810 completed with status 0
% 0.17/0.65 % Result found by SubtermCWHack
% 0.17/0.65 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.17/0.65 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.17/0.65 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.17/0.65 % Starting new_bool_3 with 300s (1) cores
% 0.17/0.65 % Starting new_bool_1 with 300s (1) cores
% 0.17/0.65 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.17/0.65 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.17/0.65 % Search class: FGUSM-FSLM31-MFFFFFNN
% 0.17/0.65 % partial match(1): FGHSM-FSLM31-MFFFFFNN
% 0.17/0.65 % Scheduled 8 strats onto 1 cores with 300 seconds (300 total)
% 0.17/0.65 % Starting SubtermCWHack with 28s (1) cores
% 0.17/0.65 % Preprocessing time : 0.006 s
% 0.17/0.65
% 0.17/0.65 % Proof found!
% 0.17/0.65 % SZS status Theorem
% 0.17/0.65 % SZS output start CNFRefutation
% See solution above
% 0.17/0.65 % Parsed axioms : 410
% 0.17/0.65 % Removed by relevancy pruning/SinE : 332
% 0.17/0.65 % Initial clauses : 405
% 0.17/0.65 % Removed in clause preprocessing : 0
% 0.17/0.65 % Initial clauses in saturation : 405
% 0.17/0.65 % Processed clauses : 650
% 0.17/0.65 % ...of these trivial : 32
% 0.17/0.65 % ...subsumed : 299
% 0.17/0.65 % ...remaining for further processing : 319
% 0.17/0.65 % Other redundant clauses eliminated : 170
% 0.17/0.65 % Clauses deleted for lack of memory : 0
% 0.17/0.65 % Backward-subsumed : 0
% 0.17/0.65 % Backward-rewritten : 7
% 0.17/0.65 % Generated clauses : 2362
% 0.17/0.65 % ...of the previous two non-redundant : 1889
% 0.17/0.65 % ...aggressively subsumed : 0
% 0.17/0.65 % Contextual simplify-reflections : 0
% 0.17/0.65 % Paramodulations : 2179
% 0.17/0.65 % Factorizations : 0
% 0.17/0.65 % NegExts : 0
% 0.17/0.65 % Equation resolutions : 183
% 0.17/0.65 % Disequality decompositions : 0
% 0.17/0.65 % Total rewrite steps : 483
% 0.17/0.65 % ...of those cached : 383
% 0.17/0.65 % Propositional unsat checks : 0
% 0.17/0.65 % Propositional check models : 0
% 0.17/0.65 % Propositional check unsatisfiable : 0
% 0.17/0.65 % Propositional clauses : 0
% 0.17/0.65 % Propositional clauses after purity: 0
% 0.17/0.65 % Propositional unsat core size : 0
% 0.17/0.65 % Propositional preprocessing time : 0.000
% 0.17/0.65 % Propositional encoding time : 0.000
% 0.17/0.65 % Propositional solver time : 0.000
% 0.17/0.65 % Success case prop preproc time : 0.000
% 0.17/0.65 % Success case prop encoding time : 0.000
% 0.17/0.65 % Success case prop solver time : 0.000
% 0.17/0.65 % Current number of processed clauses : 312
% 0.17/0.65 % Positive orientable unit clauses : 42
% 0.17/0.65 % Positive unorientable unit clauses: 8
% 0.17/0.65 % Negative unit clauses : 18
% 0.17/0.65 % Non-unit-clauses : 244
% 0.17/0.65 % Current number of unprocessed clauses: 1641
% 0.17/0.65 % ...number of literals in the above : 4793
% 0.17/0.65 % Current number of archived formulas : 0
% 0.17/0.65 % Current number of archived clauses : 7
% 0.17/0.65 % Clause-clause subsumption calls (NU) : 11363
% 0.17/0.65 % Rec. Clause-clause subsumption calls : 10312
% 0.17/0.65 % Non-unit clause-clause subsumptions : 203
% 0.17/0.65 % Unit Clause-clause subsumption calls : 376
% 0.17/0.65 % Rewrite failures with RHS unbound : 98
% 0.17/0.65 % BW rewrite match attempts : 28
% 0.17/0.65 % BW rewrite match successes : 15
% 0.17/0.65 % Condensation attempts : 0
% 0.17/0.65 % Condensation successes : 0
% 0.17/0.65 % Termbank termtop insertions : 39293
% 0.17/0.65 % Search garbage collected termcells : 5595
% 0.17/0.65
% 0.17/0.65 % -------------------------------------------------
% 0.17/0.65 % User time : 0.049 s
% 0.17/0.65 % System time : 0.008 s
% 0.17/0.65 % Total time : 0.057 s
% 0.17/0.65 % Maximum resident set size: 5200 pages
% 0.17/0.65
% 0.17/0.65 % -------------------------------------------------
% 0.17/0.65 % User time : 0.066 s
% 0.17/0.65 % System time : 0.011 s
% 0.17/0.65 % Total time : 0.076 s
% 0.17/0.65 % Maximum resident set size: 5376 pages
% 0.17/0.65 % E exiting
%------------------------------------------------------------------------------