%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : COM284_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 : n009.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.90s 0.61s
% Output : CNFRefutation 0.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 6
% Syntax : Number of formulae : 28 ( 20 unt; 0 typ; 0 def)
% Number of atoms : 59 ( 43 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 58 ( 27 ~; 15 |; 12 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 9 ( 8 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 7 con; 0-3 aty)
% Number of variables : 59 ( 0 sgn 57 !; 2 ?; 59 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
vExp: $tType ).
tff(decl_sort2,type,
vName: $tType ).
tff(decl_sort3,type,
vAttrL: $tType ).
tff(decl_sort4,type,
vFType: $tType ).
tff(decl_sort5,type,
vOptFType: $tType ).
tff(decl_sort6,type,
vTType: $tType ).
tff(decl_sort7,type,
vRawTable: $tType ).
tff(decl_sort8,type,
vOptRawTable: $tType ).
tff(decl_25,type,
vlookup: vName > vExp ).
tff(decl_27,type,
vacons: ( vAttrL * vName ) > vAttrL ).
tff(decl_29,type,
vsomeFType: vFType > vOptFType ).
tff(decl_32,type,
vttcons: ( vTType * ( vFType * vName ) ) > vTType ).
tff(decl_35,type,
vaempty: vAttrL ).
tff(decl_42,type,
vsomeRawTable: vRawTable > vOptRawTable ).
tff(decl_48,type,
vttempty: vTType ).
tff(decl_51,type,
vnoFType: vOptFType ).
tff(decl_64,type,
vmatchingAttrL: ( vAttrL * vTType ) > $o ).
tff(decl_78,type,
vwelltypedRawtable: ( vRawTable * vTType ) > $o ).
tff(decl_93,type,
vfindCol: ( vRawTable * ( vAttrL * vName ) ) > vOptRawTable ).
tff(decl_98,type,
vtypeOfExp: ( vTType * vExp ) > vOptFType ).
tff(decl_100,type,
vfindColType: ( vTType * vName ) > vOptFType ).
tff(decl_122,type,
esk1_0: vTType ).
tff(decl_123,type,
esk2_0: vRawTable ).
tff(decl_124,type,
esk3_0: vName ).
tff(decl_125,type,
esk4_0: vFType ).
tff(decl_151,type,
esk30_2: ( vAttrL * vTType ) > vName ).
tff(decl_152,type,
esk31_2: ( vAttrL * vTType ) > vFType ).
tff(decl_153,type,
esk32_2: ( vAttrL * vTType ) > vTType ).
tff(decl_154,type,
esk33_2: ( vAttrL * vTType ) > vName ).
tff(decl_155,type,
esk34_2: ( vAttrL * vTType ) > vAttrL ).
tff('DIFF-aempty-acons',axiom,
! [X7: vName,X2: vAttrL] : ( vaempty != vacons(X7,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-aempty-acons') ).
tff('matchingAttrL-2',axiom,
! [X76: vTType,X77: vAttrL] :
( ( ( ! [X81: vName,X70: vAttrL] : ( X77 != vacons(X81,X70) )
| ! [X78: vName,X79: vFType,X80: vTType] : ( X76 != vttcons(X78,X79,X80) ) )
& ( ( X77 != vaempty )
| ( X76 != vttempty ) ) )
=> ~ vmatchingAttrL(X76,X77) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','matchingAttrL-2') ).
tff('findColTypeImpliesfindCol-aempty',conjecture,
! [X54: vTType,X52: vRawTable,X179: vName,X86: vFType] :
( ( ( vfindColType(X179,X54) = vsomeFType(X86) )
& vmatchingAttrL(X54,vaempty)
& vwelltypedRawtable(X54,X52) )
=> ? [X167: vRawTable] : ( vfindCol(X179,vaempty,X52) = vsomeRawTable(X167) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','findColTypeImpliesfindCol-aempty') ).
tff('DIFF-noFType-someFType',axiom,
! [X19: vFType] : ( vnoFType != vsomeFType(X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noFType-someFType') ).
tff('typeOfExp-2',axiom,
! [X75: vName,X86: vFType,X72: vTType] : ( vtypeOfExp(vlookup(X75),vttcons(X75,X86,X72)) = vsomeFType(X86) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeOfExp-2') ).
tff('findColType-0',axiom,
! [X179: vName] : ( vfindColType(X179,vttempty) = vnoFType ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','findColType-0') ).
tff(c_0_6,plain,
! [X7: vName,X2: vAttrL] : ( vaempty != vacons(X7,X2) ),
inference(fof_simplification,[status(thm)],['DIFF-aempty-acons']) ).
tff(c_0_7,plain,
! [X76: vTType,X77: vAttrL] :
( ( ( ! [X81: vName,X70: vAttrL] : ( X77 != vacons(X81,X70) )
| ! [X78: vName,X79: vFType,X80: vTType] : ( X76 != vttcons(X78,X79,X80) ) )
& ( ( X77 != vaempty )
| ( X76 != vttempty ) ) )
=> ~ vmatchingAttrL(X76,X77) ),
inference(fof_simplification,[status(thm)],['matchingAttrL-2']) ).
tff(c_0_8,negated_conjecture,
~ ! [X54: vTType,X52: vRawTable,X179: vName,X86: vFType] :
( ( ( vfindColType(X179,X54) = vsomeFType(X86) )
& vmatchingAttrL(X54,vaempty)
& vwelltypedRawtable(X54,X52) )
=> ? [X167: vRawTable] : ( vfindCol(X179,vaempty,X52) = vsomeRawTable(X167) ) ),
inference(assume_negation,[status(cth)],['findColTypeImpliesfindCol-aempty']) ).
tff(c_0_9,plain,
! [X502: vName,X503: vAttrL] : ( vaempty != vacons(X502,X503) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_6])]) ).
tff(c_0_10,plain,
! [X543: vTType,X544: vAttrL] :
( ( ~ vmatchingAttrL(X543,X544)
| ( X544 = vaempty )
| ( X544 = vacons(esk33_2(X543,X544),esk34_2(X543,X544)) ) )
& ( ~ vmatchingAttrL(X543,X544)
| ( X544 = vaempty )
| ( X543 = vttcons(esk30_2(X543,X544),esk31_2(X543,X544),esk32_2(X543,X544)) ) )
& ( ~ vmatchingAttrL(X543,X544)
| ( X543 = vttempty )
| ( X544 = vacons(esk33_2(X543,X544),esk34_2(X543,X544)) ) )
& ( ~ vmatchingAttrL(X543,X544)
| ( X543 = vttempty )
| ( X543 = vttcons(esk30_2(X543,X544),esk31_2(X543,X544),esk32_2(X543,X544)) ) ) ),
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_7])])])])]) ).
tff(c_0_11,plain,
! [X19: vFType] : ( vnoFType != vsomeFType(X19) ),
inference(fof_simplification,[status(thm)],['DIFF-noFType-someFType']) ).
tff(c_0_12,negated_conjecture,
! [X464: vRawTable] :
( ( vfindCol(esk3_0,vaempty,esk2_0) != vsomeRawTable(X464) )
& ( vfindColType(esk3_0,esk1_0) = vsomeFType(esk4_0) )
& vmatchingAttrL(esk1_0,vaempty)
& vwelltypedRawtable(esk1_0,esk2_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_8])])])])]) ).
tff(c_0_13,plain,
! [X527: vName,X528: vFType,X529: vTType] : ( vtypeOfExp(vlookup(X527),vttcons(X527,X528,X529)) = vsomeFType(X528) ),
inference(variable_rename,[status(thm)],['typeOfExp-2']) ).
tcf(c_0_14,plain,
! [X7: vName,X2: vAttrL] : vaempty != vacons(X7,X2),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
tcf(c_0_15,plain,
! [X18: vTType,X2: vAttrL] :
( ~ vmatchingAttrL(X18,X2)
| ( X18 = vttempty )
| ( X2 = vacons(esk33_2(X18,X2),esk34_2(X18,X2)) ) ),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
tff(c_0_16,plain,
! [X508: vFType] : ( vnoFType != vsomeFType(X508) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_11])]) ).
tcf(c_0_17,negated_conjecture,
vfindColType(esk3_0,esk1_0) = vsomeFType(esk4_0),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
tcf(c_0_18,plain,
! [X7: vName,X18: vTType,X19: vFType] : vtypeOfExp(vlookup(X7),vttcons(X7,X19,X18)) = vsomeFType(X19),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
tcf(c_0_19,plain,
! [X18: vTType] :
( ~ vmatchingAttrL(X18,vaempty)
| ( X18 = vttempty ) ),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_14,c_0_15])]) ).
tcf(c_0_20,negated_conjecture,
vmatchingAttrL(esk1_0,vaempty),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
tff(c_0_21,plain,
! [X530: vName] : ( vfindColType(X530,vttempty) = vnoFType ),
inference(variable_rename,[status(thm)],['findColType-0']) ).
tcf(c_0_22,plain,
! [X19: vFType] : vnoFType != vsomeFType(X19),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
tcf(c_0_23,negated_conjecture,
! [X7: vName,X18: vTType] : vtypeOfExp(vlookup(X7),vttcons(X7,esk4_0,X18)) = vfindColType(esk3_0,esk1_0),
inference(spm,[status(thm)],[c_0_17,c_0_18]) ).
tcf(c_0_24,negated_conjecture,
esk1_0 = vttempty,
inference(spm,[status(thm)],[c_0_19,c_0_20]) ).
tcf(c_0_25,plain,
! [X7: vName] : vfindColType(X7,vttempty) = vnoFType,
inference(split_conjunct,[status(thm)],[c_0_21]) ).
tcf(c_0_26,plain,
! [X7: vName,X19: vFType,X18: vTType] : vtypeOfExp(vlookup(X7),vttcons(X7,X19,X18)) != vnoFType,
inference(spm,[status(thm)],[c_0_22,c_0_18]) ).
cnf(c_0_27,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_23,c_0_24]),c_0_25]),c_0_26]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM284_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n009.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 14:22:13 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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.90/0.61 % Version: 3.5.1
% 0.90/0.61 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.90/0.61 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.90/0.61 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.90/0.61 % Starting new_bool_3 with 300s (1) cores
% 0.90/0.61 % Starting new_bool_1 with 300s (1) cores
% 0.90/0.61 % Starting sh5l with 300s (1) cores
% 0.90/0.61 % new_bool_3 with pid 1995882 completed with status 0
% 0.90/0.61 % Result found by new_bool_3
% 0.90/0.61 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.90/0.61 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.90/0.61 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.90/0.61 % Starting new_bool_3 with 300s (1) cores
% 0.90/0.61 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.90/0.61 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.90/0.61 % Search class: FGHSM-SSLM31-MFFFFFNN
% 0.90/0.61 % partial match(1): FGHSM-SMLM31-MFFFFFNN
% 0.90/0.61 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 0.90/0.61 % Starting SubtermCWHack with 31s (1) cores
% 0.90/0.61 % SubtermCWHack with pid 1995896 completed with status 0
% 0.90/0.61 % Result found by SubtermCWHack
% 0.90/0.61 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.90/0.61 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.90/0.61 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.90/0.61 % Starting new_bool_3 with 300s (1) cores
% 0.90/0.61 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.90/0.61 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.90/0.61 % Search class: FGHSM-SSLM31-MFFFFFNN
% 0.90/0.61 % partial match(1): FGHSM-SMLM31-MFFFFFNN
% 0.90/0.61 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 0.90/0.61 % Starting SubtermCWHack with 31s (1) cores
% 0.90/0.61 % Preprocessing time : 0.012 s
% 0.90/0.61
% 0.90/0.61 % Proof found!
% 0.90/0.61 % SZS status Theorem
% 0.90/0.61 % SZS output start CNFRefutation
% See solution above
% 0.90/0.61 % Parsed axioms : 408
% 0.90/0.61 % Removed by relevancy pruning/SinE : 227
% 0.90/0.61 % Initial clauses : 1077
% 0.90/0.61 % Removed in clause preprocessing : 0
% 0.90/0.61 % Initial clauses in saturation : 1077
% 0.90/0.61 % Processed clauses : 1487
% 0.90/0.61 % ...of these trivial : 50
% 0.90/0.61 % ...subsumed : 729
% 0.90/0.61 % ...remaining for further processing : 708
% 0.90/0.61 % Other redundant clauses eliminated : 350
% 0.90/0.61 % Clauses deleted for lack of memory : 0
% 0.90/0.61 % Backward-subsumed : 8
% 0.90/0.61 % Backward-rewritten : 38
% 0.90/0.61 % Generated clauses : 4867
% 0.90/0.61 % ...of the previous two non-redundant : 3876
% 0.90/0.61 % ...aggressively subsumed : 0
% 0.90/0.61 % Contextual simplify-reflections : 0
% 0.90/0.61 % Paramodulations : 4482
% 0.90/0.61 % Factorizations : 0
% 0.90/0.61 % NegExts : 0
% 0.90/0.61 % Equation resolutions : 385
% 0.90/0.61 % Disequality decompositions : 0
% 0.90/0.61 % Total rewrite steps : 1055
% 0.90/0.61 % ...of those cached : 861
% 0.90/0.61 % Propositional unsat checks : 0
% 0.90/0.61 % Propositional check models : 0
% 0.90/0.61 % Propositional check unsatisfiable : 0
% 0.90/0.61 % Propositional clauses : 0
% 0.90/0.61 % Propositional clauses after purity: 0
% 0.90/0.61 % Propositional unsat core size : 0
% 0.90/0.61 % Propositional preprocessing time : 0.000
% 0.90/0.61 % Propositional encoding time : 0.000
% 0.90/0.61 % Propositional solver time : 0.000
% 0.90/0.61 % Success case prop preproc time : 0.000
% 0.90/0.61 % Success case prop encoding time : 0.000
% 0.90/0.61 % Success case prop solver time : 0.000
% 0.90/0.61 % Current number of processed clauses : 662
% 0.90/0.61 % Positive orientable unit clauses : 96
% 0.90/0.61 % Positive unorientable unit clauses: 9
% 0.90/0.61 % Negative unit clauses : 49
% 0.90/0.61 % Non-unit-clauses : 508
% 0.90/0.61 % Current number of unprocessed clauses: 3432
% 0.90/0.61 % ...number of literals in the above : 11409
% 0.90/0.61 % Current number of archived formulas : 0
% 0.90/0.61 % Current number of archived clauses : 46
% 0.90/0.61 % Clause-clause subsumption calls (NU) : 58714
% 0.90/0.61 % Rec. Clause-clause subsumption calls : 49970
% 0.90/0.61 % Non-unit clause-clause subsumptions : 572
% 0.90/0.61 % Unit Clause-clause subsumption calls : 3622
% 0.90/0.61 % Rewrite failures with RHS unbound : 132
% 0.90/0.61 % BW rewrite match attempts : 39
% 0.90/0.61 % BW rewrite match successes : 26
% 0.90/0.61 % Condensation attempts : 0
% 0.90/0.61 % Condensation successes : 0
% 0.90/0.61 % Termbank termtop insertions : 83633
% 0.90/0.61 % Search garbage collected termcells : 9039
% 0.90/0.61
% 0.90/0.61 % -------------------------------------------------
% 0.90/0.61 % User time : 0.143 s
% 0.90/0.61 % System time : 0.012 s
% 0.90/0.61 % Total time : 0.155 s
% 0.90/0.61 % Maximum resident set size: 6224 pages
% 0.90/0.61
% 0.90/0.61 % -------------------------------------------------
% 0.90/0.61 % User time : 0.157 s
% 0.90/0.61 % System time : 0.018 s
% 0.90/0.61 % Total time : 0.175 s
% 0.90/0.61 % Maximum resident set size: 5632 pages
% 0.90/0.61 % E exiting
%------------------------------------------------------------------------------