%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : COM283_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 : n003.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 38.03s 6.06s
% Output : CNFRefutation 38.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 13
% Syntax : Number of formulae : 65 ( 23 unt; 0 typ; 0 def)
% Number of atoms : 140 ( 85 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 126 ( 51 ~; 46 |; 18 &)
% ( 1 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 8 ( 7 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 9 con; 0-3 aty)
% Number of variables : 140 ( 0 sgn 131 !; 9 ?; 140 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
vName: $tType ).
tff(decl_sort2,type,
vAttrL: $tType ).
tff(decl_sort3,type,
vFType: $tType ).
tff(decl_sort4,type,
vOptFType: $tType ).
tff(decl_sort5,type,
vTType: $tType ).
tff(decl_sort6,type,
vRawTable: $tType ).
tff(decl_sort7,type,
vOptRawTable: $tType ).
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_36,type,
vnoRawTable: vOptRawTable ).
tff(decl_42,type,
vsomeRawTable: vRawTable > vOptRawTable ).
tff(decl_45,type,
val1: vAttrL ).
tff(decl_49,type,
vttempty: vTType ).
tff(decl_52,type,
vnoFType: vOptFType ).
tff(decl_65,type,
vmatchingAttrL: ( vAttrL * vTType ) > $o ).
tff(decl_79,type,
vwelltypedRawtable: ( vRawTable * vTType ) > $o ).
tff(decl_87,type,
visSomeFType: vOptFType > $o ).
tff(decl_94,type,
vfindCol: ( vRawTable * ( vAttrL * vName ) ) > vOptRawTable ).
tff(decl_100,type,
vdropFirstColRaw: vRawTable > vRawTable ).
tff(decl_101,type,
vfindColType: ( vTType * vName ) > vOptFType ).
tff(decl_148,type,
esk13_1: vTType > vName ).
tff(decl_149,type,
esk14_1: vTType > vFType ).
tff(decl_150,type,
esk15_1: vTType > vTType ).
tff(decl_154,type,
esk19_1: vOptRawTable > vRawTable ).
tff(decl_444,type,
esk309_1: vOptFType > vFType ).
tff(decl_513,type,
esk378_3: ( vName * ( vRawTable * vTType ) ) > vRawTable ).
tff(decl_514,type,
esk379_0: vName ).
tff(decl_515,type,
esk380_0: vRawTable ).
tff(decl_516,type,
esk381_0: vFType ).
tff(decl_517,type,
esk382_0: vName ).
tff(decl_518,type,
esk383_0: vTType ).
tff('findColTypeImpliesfindCol-acons-n-n1-False',conjecture,
! [X188: vName,X52: vRawTable,X86: vFType,X179: vName,X54: vTType] :
( ( ( vfindColType(X179,X54) = vsomeFType(X86) )
& vmatchingAttrL(X54,vacons(X188,val1))
& vwelltypedRawtable(X54,X52)
& ( X179 != X188 ) )
=> ? [X167: vRawTable] : ( vfindCol(X179,vacons(X188,val1),X52) = vsomeRawTable(X167) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','findColTypeImpliesfindCol-acons-n-n1-False') ).
tff('matchingAttrL-1',axiom,
! [X72: vTType,X73: vName,X74: vFType,X75: vName,X68: vAttrL] :
( vmatchingAttrL(vttcons(X73,X74,X72),vacons(X75,X68))
<=> ( vmatchingAttrL(X72,X68)
& ( X73 = X75 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','matchingAttrL-1') ).
tff('dom-TType',axiom,
! [X18: vTType] :
( ? [X7: vName,X19: vFType,X20: vTType] : ( X18 = vttcons(X7,X19,X20) )
| ( X18 = vttempty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-TType') ).
tff('DIFF-noRawTable-someRawTable',axiom,
! [X27: vRawTable] : ( vnoRawTable != vsomeRawTable(X27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noRawTable-someRawTable') ).
tff('findColTypeImpliesfindCol-acons-IH0',axiom,
! [X54: vTType,X52: vRawTable,X179: vName,X86: vFType] :
( ( ( vfindColType(X179,X54) = vsomeFType(X86) )
& vmatchingAttrL(X54,val1)
& vwelltypedRawtable(X54,X52) )
=> ? [X167: vRawTable] : ( vfindCol(X179,val1,X52) = vsomeRawTable(X167) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','findColTypeImpliesfindCol-acons-IH0') ).
tff('isSomeFType-true-INV',axiom,
! [X412: vOptFType] :
( visSomeFType(X412)
=> ? [X57: vFType] : ( X412 = vsomeFType(X57) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeFType-true-INV') ).
tff('findCol-2',axiom,
! [X179: vName,X188: vName,X222: vAttrL,X151: vRawTable] :
( ( X179 != X188 )
=> ( vfindCol(X179,vacons(X188,X222),X151) = vfindCol(X179,X222,vdropFirstColRaw(X151)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','findCol-2') ).
tff('dom-OptRawTable',axiom,
! [X26: vOptRawTable] :
( ? [X27: vRawTable] : ( X26 = vsomeRawTable(X27) )
| ( X26 = vnoRawTable ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-OptRawTable') ).
tff('findColType-2',axiom,
! [X179: vName,X414: vName,X86: vFType,X72: vTType] :
( ( X179 != X414 )
=> ( vfindColType(X179,vttcons(X414,X86,X72)) = vfindColType(X179,X72) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','findColType-2') ).
tff('isSomeFType-1',axiom,
! [X57: vFType] : visSomeFType(vsomeFType(X57)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeFType-1') ).
tff(dropFirstColRawPreservesWelltypedRaw,axiom,
! [X179: vName,X86: vFType,X460: vTType,X52: vRawTable] :
( vwelltypedRawtable(vttcons(X179,X86,X460),X52)
=> vwelltypedRawtable(X460,vdropFirstColRaw(X52)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dropFirstColRawPreservesWelltypedRaw) ).
tff('DIFF-noFType-someFType',axiom,
! [X19: vFType] : ( vnoFType != vsomeFType(X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noFType-someFType') ).
tff('findColType-0',axiom,
! [X179: vName] : ( vfindColType(X179,vttempty) = vnoFType ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','findColType-0') ).
tff(c_0_13,negated_conjecture,
~ ! [X188: vName,X52: vRawTable,X86: vFType,X179: vName,X54: vTType] :
( ( ( vfindColType(X179,X54) = vsomeFType(X86) )
& vmatchingAttrL(X54,vacons(X188,val1))
& vwelltypedRawtable(X54,X52)
& ( X179 != X188 ) )
=> ? [X167: vRawTable] : ( vfindCol(X179,vacons(X188,val1),X52) = vsomeRawTable(X167) ) ),
inference(assume_negation,[status(cth)],['findColTypeImpliesfindCol-acons-n-n1-False']) ).
tff(c_0_14,plain,
! [X757: vTType,X758: vName,X759: vFType,X760: vName,X761: vAttrL] :
( ( vmatchingAttrL(vttcons(X758,X759,X757),vacons(X760,X761))
| ~ vmatchingAttrL(X757,X761)
| ( X758 != X760 ) )
& ( ~ vmatchingAttrL(vttcons(X758,X759,X757),vacons(X760,X761))
| vmatchingAttrL(X757,X761) )
& ( ~ vmatchingAttrL(vttcons(X758,X759,X757),vacons(X760,X761))
| ( X758 = X760 ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['matchingAttrL-1'])])])]) ).
tff(c_0_15,plain,
! [X542: vTType] :
( ( X542 = vttcons(esk13_1(X542),esk14_1(X542),esk15_1(X542)) )
| ( X542 = vttempty ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['dom-TType'])]) ).
tff(c_0_16,negated_conjecture,
~ ! [X188: vName,X52: vRawTable,X86: vFType,X179: vName,X54: vTType] :
( ( ( vfindColType(X179,X54) = vsomeFType(X86) )
& vmatchingAttrL(X54,vacons(X188,val1))
& vwelltypedRawtable(X54,X52)
& ( X179 != X188 ) )
=> ? [X167: vRawTable] : ( vfindCol(X179,vacons(X188,val1),X52) = vsomeRawTable(X167) ) ),
inference(fof_simplification,[status(thm)],[c_0_13]) ).
tcf(c_0_17,plain,
! [X19: vFType,X18: vTType,X12: vName,X7: vName,X2: vAttrL] :
( ~ vmatchingAttrL(vttcons(X7,X19,X18),vacons(X12,X2))
| ( X7 = X12 ) ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
tcf(c_0_18,plain,
! [X18: vTType] :
( ( X18 = vttcons(esk13_1(X18),esk14_1(X18),esk15_1(X18)) )
| ( X18 = vttempty ) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
tff(c_0_19,negated_conjecture,
! [X1584: vRawTable] :
( ( vfindCol(esk382_0,vacons(esk379_0,val1),esk380_0) != vsomeRawTable(X1584) )
& ( vfindColType(esk382_0,esk383_0) = vsomeFType(esk381_0) )
& vmatchingAttrL(esk383_0,vacons(esk379_0,val1))
& vwelltypedRawtable(esk383_0,esk380_0)
& ( esk382_0 != esk379_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_16])])])])]) ).
tff(c_0_20,plain,
! [X27: vRawTable] : ( vnoRawTable != vsomeRawTable(X27) ),
inference(fof_simplification,[status(thm)],['DIFF-noRawTable-someRawTable']) ).
tff(c_0_21,plain,
! [X1569: vTType,X1570: vRawTable,X1571: vName,X1572: vFType] :
( ( vfindCol(X1571,val1,X1570) = vsomeRawTable(esk378_3(X1569,X1570,X1571)) )
| ( vfindColType(X1571,X1569) != vsomeFType(X1572) )
| ~ vmatchingAttrL(X1569,val1)
| ~ vwelltypedRawtable(X1569,X1570) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],['findColTypeImpliesfindCol-acons-IH0'])])])])])]) ).
tff(c_0_22,plain,
! [X1359: vOptFType] :
( ( X1359 = vsomeFType(esk309_1(X1359)) )
| ~ visSomeFType(X1359) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['isSomeFType-true-INV'])])])]) ).
tff(c_0_23,plain,
! [X179: vName,X188: vName,X222: vAttrL,X151: vRawTable] :
( ( X179 != X188 )
=> ( vfindCol(X179,vacons(X188,X222),X151) = vfindCol(X179,X222,vdropFirstColRaw(X151)) ) ),
inference(fof_simplification,[status(thm)],['findCol-2']) ).
tff(c_0_24,plain,
! [X568: vOptRawTable] :
( ( X568 = vsomeRawTable(esk19_1(X568)) )
| ( X568 = vnoRawTable ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['dom-OptRawTable'])]) ).
tcf(c_0_25,plain,
! [X18: vTType,X7: vName,X2: vAttrL] :
( ~ vmatchingAttrL(X18,vacons(X7,X2))
| ( X18 = vttempty )
| ( esk13_1(X18) = X7 ) ),
inference(spm,[status(thm)],[c_0_17,c_0_18]) ).
tcf(c_0_26,negated_conjecture,
vmatchingAttrL(esk383_0,vacons(esk379_0,val1)),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
tff(c_0_27,plain,
! [X572: vRawTable] : ( vnoRawTable != vsomeRawTable(X572) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_20])]) ).
tcf(c_0_28,plain,
! [X7: vName,X18: vTType,X27: vRawTable,X19: vFType] :
( ( vfindColType(X7,X18) != vsomeFType(X19) )
| ~ vmatchingAttrL(X18,val1)
| ~ vwelltypedRawtable(X18,X27)
| ( vfindCol(X7,val1,X27) = vsomeRawTable(esk378_3(X18,X27,X7)) ) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
tcf(c_0_29,plain,
! [X50: vOptFType] :
( ~ visSomeFType(X50)
| ( X50 = vsomeFType(esk309_1(X50)) ) ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
tff(c_0_30,plain,
! [X1083: vName,X1084: vName,X1085: vAttrL,X1086: vRawTable] :
( ( vfindCol(X1083,vacons(X1084,X1085),X1086) = vfindCol(X1083,X1085,vdropFirstColRaw(X1086)) )
| ( X1083 = X1084 ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_23])]) ).
tcf(c_0_31,negated_conjecture,
! [X27: vRawTable] : vfindCol(esk382_0,vacons(esk379_0,val1),esk380_0) != vsomeRawTable(X27),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
tcf(c_0_32,plain,
! [X26: vOptRawTable] :
( ( X26 = vsomeRawTable(esk19_1(X26)) )
| ( X26 = vnoRawTable ) ),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
tff(c_0_33,plain,
! [X179: vName,X414: vName,X86: vFType,X72: vTType] :
( ( X179 != X414 )
=> ( vfindColType(X179,vttcons(X414,X86,X72)) = vfindColType(X179,X72) ) ),
inference(fof_simplification,[status(thm)],['findColType-2']) ).
tcf(c_0_34,negated_conjecture,
( ( esk383_0 = vttempty )
| ( esk13_1(esk383_0) = esk379_0 ) ),
inference(spm,[status(thm)],[c_0_25,c_0_26]) ).
tcf(c_0_35,plain,
! [X27: vRawTable] : vnoRawTable != vsomeRawTable(X27),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
tcf(c_0_36,plain,
! [X7: vName,X27: vRawTable,X18: vTType] :
( ~ vmatchingAttrL(X18,val1)
| ~ vwelltypedRawtable(X18,X27)
| ~ visSomeFType(vfindColType(X7,X18))
| ( vsomeRawTable(esk378_3(X18,X27,X7)) = vfindCol(X7,val1,X27) ) ),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_28,c_0_29])]) ).
tcf(c_0_37,plain,
! [X2: vAttrL,X12: vName,X7: vName,X27: vRawTable] :
( ( vfindCol(X7,vacons(X12,X2),X27) = vfindCol(X7,X2,vdropFirstColRaw(X27)) )
| ( X7 = X12 ) ),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
tcf(c_0_38,negated_conjecture,
vfindCol(esk382_0,vacons(esk379_0,val1),esk380_0) = vnoRawTable,
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_31,c_0_32])]) ).
tcf(c_0_39,negated_conjecture,
esk382_0 != esk379_0,
inference(split_conjunct,[status(thm)],[c_0_19]) ).
tff(c_0_40,plain,
! [X1366: vName,X1367: vName,X1368: vFType,X1369: vTType] :
( ( vfindColType(X1366,vttcons(X1367,X1368,X1369)) = vfindColType(X1366,X1369) )
| ( X1366 = X1367 ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_33])]) ).
tcf(c_0_41,plain,
! [X19: vFType,X18: vTType,X12: vName,X7: vName,X2: vAttrL] :
( ~ vmatchingAttrL(vttcons(X7,X19,X18),vacons(X12,X2))
| vmatchingAttrL(X18,X2) ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
tcf(c_0_42,negated_conjecture,
( ( esk383_0 = vttempty )
| ( vttcons(esk379_0,esk14_1(esk383_0),esk15_1(esk383_0)) = esk383_0 ) ),
inference(spm,[status(thm)],[c_0_18,c_0_34]) ).
tcf(c_0_43,plain,
! [X7: vName,X27: vRawTable,X18: vTType] :
( ~ vmatchingAttrL(X18,val1)
| ~ vwelltypedRawtable(X18,X27)
| ~ visSomeFType(vfindColType(X7,X18))
| ( vfindCol(X7,val1,X27) != vnoRawTable ) ),
inference(spm,[status(thm)],[c_0_35,c_0_36]) ).
tcf(c_0_44,negated_conjecture,
vfindCol(esk382_0,val1,vdropFirstColRaw(esk380_0)) = vnoRawTable,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_37,c_0_38]),c_0_39]) ).
tcf(c_0_45,plain,
! [X7: vName,X12: vName,X19: vFType,X18: vTType] :
( ( vfindColType(X7,vttcons(X12,X19,X18)) = vfindColType(X7,X18) )
| ( X7 = X12 ) ),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
tff(c_0_46,plain,
! [X1358: vFType] : visSomeFType(vsomeFType(X1358)),
inference(variable_rename,[status(thm)],['isSomeFType-1']) ).
tcf(c_0_47,negated_conjecture,
! [X7: vName,X2: vAttrL] :
( ~ vmatchingAttrL(esk383_0,vacons(X7,X2))
| vmatchingAttrL(esk15_1(esk383_0),X2)
| ( esk383_0 = vttempty ) ),
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
tff(c_0_48,plain,
! [X1574: vName,X1575: vFType,X1576: vTType,X1577: vRawTable] :
( vwelltypedRawtable(X1576,vdropFirstColRaw(X1577))
| ~ vwelltypedRawtable(vttcons(X1574,X1575,X1576),X1577) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dropFirstColRawPreservesWelltypedRaw])])]) ).
tcf(c_0_49,negated_conjecture,
! [X18: vTType] :
( ~ vmatchingAttrL(X18,val1)
| ~ vwelltypedRawtable(X18,vdropFirstColRaw(esk380_0))
| ~ visSomeFType(vfindColType(esk382_0,X18)) ),
inference(spm,[status(thm)],[c_0_43,c_0_44]) ).
tcf(c_0_50,negated_conjecture,
! [X7: vName] :
( ( X7 = esk379_0 )
| ( esk383_0 = vttempty )
| ( vfindColType(X7,esk15_1(esk383_0)) = vfindColType(X7,esk383_0) ) ),
inference(spm,[status(thm)],[c_0_45,c_0_42]) ).
tcf(c_0_51,negated_conjecture,
vfindColType(esk382_0,esk383_0) = vsomeFType(esk381_0),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
tcf(c_0_52,plain,
! [X19: vFType] : visSomeFType(vsomeFType(X19)),
inference(split_conjunct,[status(thm)],[c_0_46]) ).
tcf(c_0_53,negated_conjecture,
( vmatchingAttrL(esk15_1(esk383_0),val1)
| ( esk383_0 = vttempty ) ),
inference(spm,[status(thm)],[c_0_47,c_0_26]) ).
tcf(c_0_54,plain,
! [X7: vName,X18: vTType,X19: vFType,X27: vRawTable] :
( ~ vwelltypedRawtable(vttcons(X7,X19,X18),X27)
| vwelltypedRawtable(X18,vdropFirstColRaw(X27)) ),
inference(split_conjunct,[status(thm)],[c_0_48]) ).
tff(c_0_55,plain,
! [X19: vFType] : ( vnoFType != vsomeFType(X19) ),
inference(fof_simplification,[status(thm)],['DIFF-noFType-someFType']) ).
tcf(c_0_56,negated_conjecture,
( ~ vwelltypedRawtable(esk15_1(esk383_0),vdropFirstColRaw(esk380_0))
| ( esk383_0 = vttempty ) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49,c_0_50]),c_0_51]),c_0_52])]),c_0_39]),c_0_53]) ).
tcf(c_0_57,plain,
! [X18: vTType,X27: vRawTable] :
( ~ vwelltypedRawtable(X18,X27)
| vwelltypedRawtable(esk15_1(X18),vdropFirstColRaw(X27))
| ( X18 = vttempty ) ),
inference(spm,[status(thm)],[c_0_54,c_0_18]) ).
tcf(c_0_58,negated_conjecture,
vwelltypedRawtable(esk383_0,esk380_0),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
tff(c_0_59,plain,
! [X1362: vName] : ( vfindColType(X1362,vttempty) = vnoFType ),
inference(variable_rename,[status(thm)],['findColType-0']) ).
tff(c_0_60,plain,
! [X721: vFType] : ( vnoFType != vsomeFType(X721) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_55])]) ).
tcf(c_0_61,negated_conjecture,
esk383_0 = vttempty,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56,c_0_57]),c_0_58])]) ).
tcf(c_0_62,plain,
! [X7: vName] : vfindColType(X7,vttempty) = vnoFType,
inference(split_conjunct,[status(thm)],[c_0_59]) ).
tcf(c_0_63,plain,
! [X19: vFType] : vnoFType != vsomeFType(X19),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
cnf(c_0_64,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_51,c_0_61]),c_0_62]),c_0_63]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM283_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.35 % Computer : n003.cluster.edu
% 0.11/0.35 % Model : x86_64 x86_64
% 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35 % Memory : 8046.5625MB
% 0.11/0.35 % OS : Linux 6.8.0-71-generic
% 0.11/0.35 % CPULimit : 300
% 0.11/0.35 % WCLimit : 300
% 0.11/0.35 % DateTime : Mon Sep 21 14:24:02 UTC 2026
% 0.11/0.35 % CPUTime :
% 0.11/0.35 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 Running first-order theorem proving
% 0.13/0.39 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
% 38.03/6.06 % Version: 3.5.1
% 38.03/6.06 % Preprocessing class: FSLSSMSMSSSNFFN.
% 38.03/6.06 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 38.03/6.06 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 38.03/6.06 % Starting new_bool_3 with 300s (1) cores
% 38.03/6.06 % Starting new_bool_1 with 300s (1) cores
% 38.03/6.06 % Starting sh5l with 300s (1) cores
% 38.03/6.06 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 343877 completed with status 0
% 38.03/6.06 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 38.03/6.06 % Preprocessing class: FSLSSMSMSSSNFFN.
% 38.03/6.06 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 38.03/6.06 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 38.03/6.06 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 38.03/6.06 % No SInE strategy applied
% 38.03/6.06 % Search class: FGHSM-SMLM32-DFFFFFNN
% 38.03/6.06 % Scheduled 13 strats onto 5 cores with 1500 seconds (1500 total)
% 38.03/6.06 % Starting SubtermCWHack with 136s (1) cores
% 38.03/6.06 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 38.03/6.06 % Starting G-E--_008_C45_F1_PI_SE_Q4_CS_SP_S4SI with 113s (1) cores
% 38.03/6.06 % Starting G-E--_207_C01_F1_SE_CS_SP_PI_S5PRR_S0Y with 113s (1) cores
% 38.03/6.06 % Starting G-E--_208_B07CMA_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with 113s (1) cores
% 38.03/6.06 % G-E--_207_C01_F1_SE_CS_SP_PI_S5PRR_S0Y with pid 343897 completed with status 0
% 38.03/6.06 % Result found by G-E--_207_C01_F1_SE_CS_SP_PI_S5PRR_S0Y
% 38.03/6.06 % Preprocessing class: FSLSSMSMSSSNFFN.
% 38.03/6.06 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 38.03/6.06 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 38.03/6.06 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 38.03/6.06 % No SInE strategy applied
% 38.03/6.06 % Search class: FGHSM-SMLM32-DFFFFFNN
% 38.03/6.06 % Scheduled 13 strats onto 5 cores with 1500 seconds (1500 total)
% 38.03/6.06 % Starting SubtermCWHack with 136s (1) cores
% 38.03/6.06 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 38.03/6.06 % Starting G-E--_008_C45_F1_PI_SE_Q4_CS_SP_S4SI with 113s (1) cores
% 38.03/6.06 % Starting G-E--_207_C01_F1_SE_CS_SP_PI_S5PRR_S0Y with 113s (1) cores
% 38.03/6.06 % Preprocessing time : 0.038 s
% 38.03/6.06
% 38.03/6.06 % Proof found!
% 38.03/6.06 % SZS status Theorem
% 38.03/6.06 % SZS output start CNFRefutation
% See solution above
% 38.03/6.06 % Parsed axioms : 412
% 38.03/6.06 % Removed by relevancy pruning/SinE : 0
% 38.03/6.06 % Initial clauses : 2915
% 38.03/6.06 % Removed in clause preprocessing : 123
% 38.03/6.06 % Initial clauses in saturation : 2792
% 38.03/6.06 % Processed clauses : 8188
% 38.03/6.06 % ...of these trivial : 143
% 38.03/6.06 % ...subsumed : 3452
% 38.03/6.06 % ...remaining for further processing : 4593
% 38.03/6.06 % Other redundant clauses eliminated : 10624
% 38.03/6.06 % Clauses deleted for lack of memory : 0
% 38.03/6.06 % Backward-subsumed : 190
% 38.03/6.06 % Backward-rewritten : 395
% 38.03/6.06 % Generated clauses : 79577
% 38.03/6.06 % ...of the previous two non-redundant : 66673
% 38.03/6.06 % ...aggressively subsumed : 0
% 38.03/6.06 % Contextual simplify-reflections : 39
% 38.03/6.06 % Paramodulations : 68893
% 38.03/6.06 % Factorizations : 2
% 38.03/6.06 % NegExts : 0
% 38.03/6.06 % Equation resolutions : 10693
% 38.03/6.06 % Disequality decompositions : 0
% 38.03/6.06 % Total rewrite steps : 7398
% 38.03/6.06 % ...of those cached : 6926
% 38.03/6.06 % Propositional unsat checks : 0
% 38.03/6.06 % Propositional check models : 0
% 38.03/6.06 % Propositional check unsatisfiable : 0
% 38.03/6.06 % Propositional clauses : 0
% 38.03/6.06 % Propositional clauses after purity: 0
% 38.03/6.06 % Propositional unsat core size : 0
% 38.03/6.06 % Propositional preprocessing time : 0.000
% 38.03/6.06 % Propositional encoding time : 0.000
% 38.03/6.06 % Propositional solver time : 0.000
% 38.03/6.06 % Success case prop preproc time : 0.000
% 38.03/6.06 % Success case prop encoding time : 0.000
% 38.03/6.06 % Success case prop solver time : 0.000
% 38.03/6.06 % Current number of processed clauses : 3856
% 38.03/6.06 % Positive orientable unit clauses : 185
% 38.03/6.06 % Positive unorientable unit clauses: 3
% 38.03/6.06 % Negative unit clauses : 89
% 38.03/6.06 % Non-unit-clauses : 3579
% 38.03/6.06 % Current number of unprocessed clauses: 60877
% 38.03/6.06 % ...number of literals in the above : 283263
% 38.03/6.06 % Current number of archived formulas : 0
% 38.03/6.06 % Current number of archived clauses : 592
% 38.03/6.06 % Clause-clause subsumption calls (NU) : 2011761
% 38.03/6.06 % Rec. Clause-clause subsumption calls : 761430
% 38.03/6.06 % Non-unit clause-clause subsumptions : 3244
% 38.03/6.06 % Unit Clause-clause subsumption calls : 118495
% 38.03/6.06 % Rewrite failures with RHS unbound : 12
% 38.03/6.06 % BW rewrite match attempts : 42
% 38.03/6.06 % BW rewrite match successes : 27
% 38.03/6.06 % Condensation attempts : 0
% 38.03/6.06 % Condensation successes : 0
% 38.03/6.06 % Termbank termtop insertions : 1161270
% 38.03/6.06 % Search garbage collected termcells : 19643
% 38.03/6.06
% 38.03/6.06 % -------------------------------------------------
% 38.03/6.06 % User time : 4.965 s
% 38.03/6.06 % System time : 0.128 s
% 38.03/6.06 % Total time : 5.092 s
% 38.03/6.06 % Maximum resident set size: 9556 pages
% 38.03/6.06
% 38.03/6.06 % -------------------------------------------------
% 38.03/6.06 % User time : 26.089 s
% 38.03/6.06 % System time : 0.658 s
% 38.03/6.06 % Total time : 26.747 s
% 38.03/6.06 % Maximum resident set size: 5376 pages
% 38.03/6.06 % E exiting
%------------------------------------------------------------------------------