%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : COM265_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 : 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:11:49 PM UTC 2026
% Result : Theorem 23.91s 3.95s
% Output : CNFRefutation 23.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 16
% Syntax : Number of formulae : 81 ( 48 unt; 0 typ; 0 def)
% Number of atoms : 156 ( 143 equ)
% Maximal formula atoms : 24 ( 1 avg)
% Number of connectives : 111 ( 36 ~; 51 |; 19 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 15 ( 14 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 37 ( 37 usr; 13 con; 0-3 aty)
% Number of variables : 155 ( 0 sgn 138 !; 17 ?; 155 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
vAval: $tType ).
tff(decl_sort2,type,
vExp: $tType ).
tff(decl_sort3,type,
vQMap: $tType ).
tff(decl_sort4,type,
vAType: $tType ).
tff(decl_sort5,type,
vMapConf: $tType ).
tff(decl_sort6,type,
vQuestionnaire: $tType ).
tff(decl_sort7,type,
vnat: $tType ).
tff(decl_sort8,type,
vOptAType: $tType ).
tff(decl_sort9,type,
vYN: $tType ).
tff(decl_sort10,type,
vstring: $tType ).
tff(decl_sort11,type,
vAnsMap: $tType ).
tff(decl_sort12,type,
vQConf: $tType ).
tff(decl_sort13,type,
vOptQConf: $tType ).
tff(decl_sort14,type,
vATMap: $tType ).
tff(decl_23,type,
vconstant: vAval > vExp ).
tff(decl_29,type,
vqcond: ( vQuestionnaire * ( vQuestionnaire * vExp ) ) > vQuestionnaire ).
tff(decl_32,type,
vNum: vnat > vAval ).
tff(decl_34,type,
vyes: vYN ).
tff(decl_35,type,
vT: vstring > vAval ).
tff(decl_36,type,
vNumber: vAType ).
tff(decl_42,type,
vYesNo: vAType ).
tff(decl_48,type,
vqseq: ( vQuestionnaire * vQuestionnaire ) > vQuestionnaire ).
tff(decl_51,type,
vsomeQConf: vQConf > vOptQConf ).
tff(decl_52,type,
vnoQConf: vOptQConf ).
tff(decl_55,type,
vB: vYN > vAval ).
tff(decl_56,type,
vQC: ( vQuestionnaire * ( vQMap * vAnsMap ) ) > vQConf ).
tff(decl_60,type,
vText: vAType ).
tff(decl_63,type,
vMC: ( vATMap * vATMap ) > vMapConf ).
tff(decl_74,type,
vsomeAType: vAType > vOptAType ).
tff(decl_76,type,
vq1: vQuestionnaire ).
tff(decl_79,type,
vno: vYN ).
tff(decl_81,type,
vq2: vQuestionnaire ).
tff(decl_83,type,
vecheck: ( vExp * vATMap ) > vOptAType ).
tff(decl_88,type,
vtypeOf: vAval > vAType ).
tff(decl_95,type,
visValue: vQuestionnaire > $o ).
tff(decl_96,type,
vtypeAM: vAnsMap > vATMap ).
tff(decl_106,type,
vqcappend: ( vQuestionnaire * vQConf ) > vQConf ).
tff(decl_115,type,
vreduce: ( vQMap * ( vAnsMap * vQuestionnaire ) ) > vOptQConf ).
tff(decl_119,type,
vtypeQM: vQMap > vATMap ).
tff(decl_132,type,
vptcheck: ( vMapConf * ( vQuestionnaire * vMapConf ) ) > $o ).
tff(decl_197,type,
esk33_1: vOptQConf > vQConf ).
tff(decl_249,type,
esk85_1: vAval > vYN ).
tff(decl_250,type,
esk86_1: vAval > vnat ).
tff(decl_251,type,
esk87_1: vAval > vstring ).
tff(decl_295,type,
esk131_2: ( vQuestionnaire * vQConf ) > vAnsMap ).
tff(decl_296,type,
esk132_2: ( vQuestionnaire * vQConf ) > vQMap ).
tff(decl_297,type,
esk133_2: ( vQuestionnaire * vQConf ) > vQuestionnaire ).
tff(decl_298,type,
esk134_2: ( vQuestionnaire * vQConf ) > vQuestionnaire ).
tff(decl_409,type,
esk245_0: vQMap ).
tff(decl_410,type,
esk246_0: vATMap ).
tff(decl_411,type,
esk247_0: vATMap ).
tff(decl_412,type,
esk248_0: vAval ).
tff(decl_413,type,
esk249_0: vAnsMap ).
tff('EQ-someAType',axiom,
! [X4: vAType,X8: vAType] :
( ( vsomeAType(X4) = vsomeAType(X8) )
=> ( X4 = X8 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','EQ-someAType') ).
tff('echeck-0',axiom,
! [X391: vATMap,X392: vYN] : ( vecheck(X391,vconstant(vB(X392))) = vsomeAType(vYesNo) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','echeck-0') ).
tff('DIFF-YesNo-Text',axiom,
vYesNo != vText,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','DIFF-YesNo-Text') ).
tff('DIFF-YesNo-Number',axiom,
vYesNo != vNumber,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','DIFF-YesNo-Number') ).
tff('Progress-qcond-constant',conjecture,
! [X150: vQMap,X359: vATMap,X500: vATMap,X181: vAval,X126: vAnsMap] :
( ( vptcheck(vMC(vtypeAM(X126),vtypeQM(X150)),vqcond(vconstant(X181),vq1,vq2),vMC(X359,X500))
& ~ visValue(vqcond(vconstant(X181),vq1,vq2)) )
=> ? [X508: vAnsMap,X509: vQMap,X510: vQuestionnaire] : ( vreduce(vqcond(vconstant(X181),vq1,vq2),X126,X150) = vsomeQConf(vQC(X508,X509,X510)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Progress-qcond-constant') ).
tff('echeck-2',axiom,
! [X394: vATMap,X395: vstring] : ( vecheck(X394,vconstant(vT(X395))) = vsomeAType(vText) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','echeck-2') ).
tff('echeck-1',axiom,
! [X393: vATMap,X82: vnat] : ( vecheck(X393,vconstant(vNum(X82))) = vsomeAType(vNumber) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','echeck-1') ).
tff('Tqcond_inv1',axiom,
! [X476: vATMap,X420: vQuestionnaire,X355: vATMap,X461: vATMap,X477: vATMap,X275: vExp,X422: vQuestionnaire] :
( vptcheck(vMC(X355,X476),vqcond(X275,X420,X422),vMC(X461,X477))
=> ( vecheck(X355,X275) = vsomeAType(vYesNo) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Tqcond_inv1') ).
tff('typeOf-INV',axiom,
! [X21: vAval] :
( ? [X107: vstring] :
( ( vtypeOf(X21) = vText )
& ( X21 = vT(X107) ) )
| ? [X89: vnat] :
( ( vtypeOf(X21) = vNumber )
& ( X21 = vNum(X89) ) )
| ? [X80: vYN] :
( ( vtypeOf(X21) = vYesNo )
& ( X21 = vB(X80) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','typeOf-INV') ).
tff('DIFF-Number-Text',axiom,
vNumber != vText,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','DIFF-Number-Text') ).
tff('qcappend-INV',axiom,
! [X44: vQConf,X34: vQuestionnaire] :
? [X127: vAnsMap,X153: vQMap,X168: vQuestionnaire,X169: vQuestionnaire] :
( ( vqcappend(X44,X34) = vQC(X127,X153,vqseq(X168,X169)) )
& ( X34 = X169 )
& ( X44 = vQC(X127,X153,X168) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qcappend-INV') ).
tff('dom-YN',axiom,
! [X10: vYN] :
( ( X10 = vno )
| ( X10 = vyes ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','dom-YN') ).
tff('dom-OptQConf',axiom,
! [X43: vOptQConf] :
( ? [X44: vQConf] : ( X43 = vsomeQConf(X44) )
| ( X43 = vnoQConf ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','dom-OptQConf') ).
tff('DIFF-noQConf-someQConf',axiom,
! [X44: vQConf] : ( vnoQConf != vsomeQConf(X44) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','DIFF-noQConf-someQConf') ).
tff('reduce-12',axiom,
! [X166: vQuestionnaire,X167: vQuestionnaire,X126: vAnsMap,X150: vQMap] : ( vreduce(vqcond(vconstant(vB(vno)),X166,X167),X126,X150) = vsomeQConf(vQC(X126,X150,X167)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','reduce-12') ).
tff('reduce-11',axiom,
! [X166: vQuestionnaire,X167: vQuestionnaire,X126: vAnsMap,X150: vQMap] : ( vreduce(vqcond(vconstant(vB(vyes)),X166,X167),X126,X150) = vsomeQConf(vQC(X126,X150,X166)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','reduce-11') ).
tff(c_0_16,plain,
! [X716: vAType,X717: vAType] :
( ( X716 = X717 )
| ( vsomeAType(X716) != vsomeAType(X717) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['EQ-someAType'])])]) ).
tff(c_0_17,plain,
! [X1342: vATMap,X1343: vYN] : ( vecheck(X1342,vconstant(vB(X1343))) = vsomeAType(vYesNo) ),
inference(variable_rename,[status(thm)],['echeck-0']) ).
tff(c_0_18,plain,
vYesNo != vText,
inference(fof_simplification,[status(thm)],['DIFF-YesNo-Text']) ).
tff(c_0_19,plain,
vYesNo != vNumber,
inference(fof_simplification,[status(thm)],['DIFF-YesNo-Number']) ).
tff(c_0_20,negated_conjecture,
~ ! [X150: vQMap,X359: vATMap,X500: vATMap,X181: vAval,X126: vAnsMap] :
( ( vptcheck(vMC(vtypeAM(X126),vtypeQM(X150)),vqcond(vconstant(X181),vq1,vq2),vMC(X359,X500))
& ~ visValue(vqcond(vconstant(X181),vq1,vq2)) )
=> ? [X508: vAnsMap,X509: vQMap,X510: vQuestionnaire] : ( vreduce(vqcond(vconstant(X181),vq1,vq2),X126,X150) = vsomeQConf(vQC(X508,X509,X510)) ) ),
inference(assume_negation,[status(cth)],['Progress-qcond-constant']) ).
tcf(c_0_21,plain,
! [X4: vAType,X8: vAType] :
( ( vsomeAType(X4) != vsomeAType(X8) )
| ( X4 = X8 ) ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
tcf(c_0_22,plain,
! [X15: vATMap,X10: vYN] : vecheck(X15,vconstant(vB(X10))) = vsomeAType(vYesNo),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
tff(c_0_23,plain,
! [X1346: vATMap,X1347: vstring] : ( vecheck(X1346,vconstant(vT(X1347))) = vsomeAType(vText) ),
inference(variable_rename,[status(thm)],['echeck-2']) ).
tff(c_0_24,plain,
vYesNo != vText,
inference(fof_nnf,[status(thm)],[c_0_18]) ).
tff(c_0_25,plain,
! [X1344: vATMap,X1345: vnat] : ( vecheck(X1344,vconstant(vNum(X1345))) = vsomeAType(vNumber) ),
inference(variable_rename,[status(thm)],['echeck-1']) ).
tff(c_0_26,plain,
vYesNo != vNumber,
inference(fof_nnf,[status(thm)],[c_0_19]) ).
tff(c_0_27,negated_conjecture,
~ ! [X150: vQMap,X359: vATMap,X500: vATMap,X181: vAval,X126: vAnsMap] :
( ( vptcheck(vMC(vtypeAM(X126),vtypeQM(X150)),vqcond(vconstant(X181),vq1,vq2),vMC(X359,X500))
& ~ visValue(vqcond(vconstant(X181),vq1,vq2)) )
=> ? [X508: vAnsMap,X509: vQMap,X510: vQuestionnaire] : ( vreduce(vqcond(vconstant(X181),vq1,vq2),X126,X150) = vsomeQConf(vQC(X508,X509,X510)) ) ),
inference(fof_simplification,[status(thm)],[c_0_20]) ).
tcf(c_0_28,plain,
! [X15: vATMap,X10: vYN,X4: vAType] :
( ( vecheck(X15,vconstant(vB(X10))) != vsomeAType(X4) )
| ( vYesNo = X4 ) ),
inference(spm,[status(thm)],[c_0_21,c_0_22]) ).
tcf(c_0_29,plain,
! [X15: vATMap,X49: vstring] : vecheck(X15,vconstant(vT(X49))) = vsomeAType(vText),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
tcf(c_0_30,plain,
vYesNo != vText,
inference(split_conjunct,[status(thm)],[c_0_24]) ).
tcf(c_0_31,plain,
! [X15: vATMap,X29: vnat] : vecheck(X15,vconstant(vNum(X29))) = vsomeAType(vNumber),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
tcf(c_0_32,plain,
vYesNo != vNumber,
inference(split_conjunct,[status(thm)],[c_0_26]) ).
tff(c_0_33,plain,
! [X1554: vATMap,X1555: vQuestionnaire,X1556: vATMap,X1557: vATMap,X1558: vATMap,X1559: vExp,X1560: vQuestionnaire] :
( ( vecheck(X1556,X1559) = vsomeAType(vYesNo) )
| ~ vptcheck(vMC(X1556,X1554),vqcond(X1559,X1555,X1560),vMC(X1557,X1558)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['Tqcond_inv1'])])]) ).
tff(c_0_34,negated_conjecture,
! [X1652: vAnsMap,X1653: vQMap,X1654: vQuestionnaire] :
( ( vreduce(vqcond(vconstant(esk248_0),vq1,vq2),esk249_0,esk245_0) != vsomeQConf(vQC(X1652,X1653,X1654)) )
& vptcheck(vMC(vtypeAM(esk249_0),vtypeQM(esk245_0)),vqcond(vconstant(esk248_0),vq1,vq2),vMC(esk246_0,esk247_0))
& ~ visValue(vqcond(vconstant(esk248_0),vq1,vq2)) ),
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_27])])])])]) ).
tff(c_0_35,plain,
! [X921: vAval] :
( ( ( vtypeOf(X921) = vYesNo )
| ( vtypeOf(X921) = vNumber )
| ( vtypeOf(X921) = vText ) )
& ( ( vtypeOf(X921) = vYesNo )
| ( vtypeOf(X921) = vNumber )
| ( X921 = vT(esk87_1(X921)) ) )
& ( ( vtypeOf(X921) = vYesNo )
| ( X921 = vNum(esk86_1(X921)) )
| ( vtypeOf(X921) = vText ) )
& ( ( vtypeOf(X921) = vYesNo )
| ( X921 = vNum(esk86_1(X921)) )
| ( X921 = vT(esk87_1(X921)) ) )
& ( ( X921 = vB(esk85_1(X921)) )
| ( vtypeOf(X921) = vNumber )
| ( vtypeOf(X921) = vText ) )
& ( ( X921 = vB(esk85_1(X921)) )
| ( vtypeOf(X921) = vNumber )
| ( X921 = vT(esk87_1(X921)) ) )
& ( ( X921 = vB(esk85_1(X921)) )
| ( X921 = vNum(esk86_1(X921)) )
| ( vtypeOf(X921) = vText ) )
& ( ( X921 = vB(esk85_1(X921)) )
| ( X921 = vNum(esk86_1(X921)) )
| ( X921 = vT(esk87_1(X921)) ) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],['typeOf-INV'])])])]) ).
tcf(c_0_36,plain,
! [X10: vYN,X15: vATMap,X16: vATMap,X49: vstring] : vecheck(X15,vconstant(vB(X10))) != vecheck(X16,vconstant(vT(X49))),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_28,c_0_29]),c_0_30]) ).
tcf(c_0_37,plain,
! [X10: vYN,X15: vATMap,X16: vATMap,X29: vnat] : vecheck(X15,vconstant(vB(X10))) != vecheck(X16,vconstant(vNum(X29))),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_28,c_0_31]),c_0_32]) ).
tcf(c_0_38,plain,
! [X5: vExp,X15: vATMap,X16: vATMap,X17: vATMap,X34: vQuestionnaire,X32: vQuestionnaire,X18: vATMap] :
( ~ vptcheck(vMC(X15,X16),vqcond(X5,X32,X34),vMC(X17,X18))
| ( vecheck(X15,X5) = vsomeAType(vYesNo) ) ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
tcf(c_0_39,negated_conjecture,
vptcheck(vMC(vtypeAM(esk249_0),vtypeQM(esk245_0)),vqcond(vconstant(esk248_0),vq1,vq2),vMC(esk246_0,esk247_0)),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
tcf(c_0_40,plain,
! [X21: vAval] :
( ( vtypeOf(X21) = vYesNo )
| ( vtypeOf(X21) = vNumber )
| ( X21 = vT(esk87_1(X21)) ) ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
tcf(c_0_41,plain,
! [X15: vATMap,X49: vstring] : vecheck(X15,vconstant(vT(X49))) != vsomeAType(vYesNo),
inference(spm,[status(thm)],[c_0_36,c_0_22]) ).
tcf(c_0_42,plain,
! [X21: vAval] :
( ( vtypeOf(X21) = vYesNo )
| ( X21 = vNum(esk86_1(X21)) )
| ( vtypeOf(X21) = vText ) ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
tcf(c_0_43,plain,
! [X15: vATMap,X10: vYN] : vecheck(X15,vconstant(vB(X10))) != vsomeAType(vNumber),
inference(spm,[status(thm)],[c_0_37,c_0_31]) ).
tff(c_0_44,plain,
vNumber != vText,
inference(fof_simplification,[status(thm)],['DIFF-Number-Text']) ).
tcf(c_0_45,negated_conjecture,
vecheck(vtypeAM(esk249_0),vconstant(esk248_0)) = vsomeAType(vYesNo),
inference(spm,[status(thm)],[c_0_38,c_0_39]) ).
tcf(c_0_46,plain,
! [X15: vATMap,X21: vAval] :
( ( vtypeOf(X21) = vNumber )
| ( vtypeOf(X21) = vYesNo )
| ( vecheck(X15,vconstant(X21)) = vsomeAType(vText) ) ),
inference(spm,[status(thm)],[c_0_29,c_0_40]) ).
tcf(c_0_47,plain,
vsomeAType(vText) != vsomeAType(vYesNo),
inference(spm,[status(thm)],[c_0_41,c_0_29]) ).
tcf(c_0_48,plain,
! [X15: vATMap,X21: vAval] :
( ( vtypeOf(X21) = vYesNo )
| ( vtypeOf(X21) = vText )
| ( vecheck(X15,vconstant(X21)) = vsomeAType(vNumber) ) ),
inference(spm,[status(thm)],[c_0_31,c_0_42]) ).
tcf(c_0_49,plain,
vsomeAType(vYesNo) != vsomeAType(vNumber),
inference(spm,[status(thm)],[c_0_43,c_0_22]) ).
tff(c_0_50,plain,
vNumber != vText,
inference(fof_nnf,[status(thm)],[c_0_44]) ).
tcf(c_0_51,plain,
! [X21: vAval] :
( ( X21 = vB(esk85_1(X21)) )
| ( vtypeOf(X21) = vNumber )
| ( vtypeOf(X21) = vText ) ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
tcf(c_0_52,negated_conjecture,
( ( vtypeOf(esk248_0) = vYesNo )
| ( vtypeOf(esk248_0) = vNumber ) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_45,c_0_46]),c_0_47]) ).
tcf(c_0_53,negated_conjecture,
( ( vtypeOf(esk248_0) = vText )
| ( vtypeOf(esk248_0) = vYesNo ) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_45,c_0_48]),c_0_49]) ).
tcf(c_0_54,plain,
vNumber != vText,
inference(split_conjunct,[status(thm)],[c_0_50]) ).
tff(c_0_55,plain,
! [X1030: vQConf,X1031: vQuestionnaire] :
( ( vqcappend(X1030,X1031) = vQC(esk131_2(X1030,X1031),esk132_2(X1030,X1031),vqseq(esk133_2(X1030,X1031),esk134_2(X1030,X1031))) )
& ( X1031 = esk134_2(X1030,X1031) )
& ( X1030 = vQC(esk131_2(X1030,X1031),esk132_2(X1030,X1031),esk133_2(X1030,X1031)) ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['qcappend-INV'])]) ).
tcf(c_0_56,plain,
! [X15: vATMap,X21: vAval] :
( ( vtypeOf(X21) = vNumber )
| ( vtypeOf(X21) = vText )
| ( vecheck(X15,vconstant(X21)) = vsomeAType(vYesNo) ) ),
inference(spm,[status(thm)],[c_0_22,c_0_51]) ).
tcf(c_0_57,negated_conjecture,
vtypeOf(esk248_0) = vYesNo,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_52,c_0_53]),c_0_54]),c_0_30]) ).
tcf(c_0_58,plain,
! [X21: vAval] :
( ( X21 = vB(esk85_1(X21)) )
| ( vtypeOf(X21) = vNumber )
| ( X21 = vT(esk87_1(X21)) ) ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
tff(c_0_59,plain,
! [X572: vYN] :
( ( X572 = vno )
| ( X572 = vyes ) ),
inference(variable_rename,[status(thm)],['dom-YN']) ).
tcf(c_0_60,negated_conjecture,
! [X11: vQMap,X55: vAnsMap,X32: vQuestionnaire] : vreduce(vqcond(vconstant(esk248_0),vq1,vq2),esk249_0,esk245_0) != vsomeQConf(vQC(X55,X11,X32)),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
tcf(c_0_61,plain,
! [X44: vQConf,X32: vQuestionnaire] : X44 = vQC(esk131_2(X44,X32),esk132_2(X44,X32),esk133_2(X44,X32)),
inference(split_conjunct,[status(thm)],[c_0_55]) ).
tff(c_0_62,plain,
! [X709: vOptQConf] :
( ( X709 = vsomeQConf(esk33_1(X709)) )
| ( X709 = vnoQConf ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['dom-OptQConf'])]) ).
tcf(c_0_63,negated_conjecture,
! [X15: vATMap] : vecheck(X15,vconstant(esk248_0)) = vsomeAType(vYesNo),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_56,c_0_57]),c_0_30]),c_0_32]) ).
tcf(c_0_64,plain,
! [X15: vATMap,X21: vAval] :
( ( vtypeOf(X21) = vNumber )
| ( vB(esk85_1(X21)) = X21 )
| ( vecheck(X15,vconstant(X21)) = vsomeAType(vText) ) ),
inference(spm,[status(thm)],[c_0_29,c_0_58]) ).
tcf(c_0_65,plain,
! [X10: vYN] :
( ( X10 = vno )
| ( X10 = vyes ) ),
inference(split_conjunct,[status(thm)],[c_0_59]) ).
tff(c_0_66,plain,
! [X44: vQConf] : ( vnoQConf != vsomeQConf(X44) ),
inference(fof_simplification,[status(thm)],['DIFF-noQConf-someQConf']) ).
tcf(c_0_67,negated_conjecture,
! [X44: vQConf] : vreduce(vqcond(vconstant(esk248_0),vq1,vq2),esk249_0,esk245_0) != vsomeQConf(X44),
inference(spm,[status(thm)],[c_0_60,c_0_61]) ).
tcf(c_0_68,plain,
! [X43: vOptQConf] :
( ( X43 = vsomeQConf(esk33_1(X43)) )
| ( X43 = vnoQConf ) ),
inference(split_conjunct,[status(thm)],[c_0_62]) ).
tcf(c_0_69,negated_conjecture,
vB(esk85_1(esk248_0)) = esk248_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63,c_0_64]),c_0_57]),c_0_47]),c_0_32]) ).
tcf(c_0_70,plain,
! [X21: vAval] :
( ( vB(vno) = X21 )
| ( vtypeOf(X21) = vNumber )
| ( vtypeOf(X21) = vText )
| ( esk85_1(X21) = vyes ) ),
inference(spm,[status(thm)],[c_0_51,c_0_65]) ).
tff(c_0_71,plain,
! [X1207: vQuestionnaire,X1208: vQuestionnaire,X1209: vAnsMap,X1210: vQMap] : ( vreduce(vqcond(vconstant(vB(vno)),X1207,X1208),X1209,X1210) = vsomeQConf(vQC(X1209,X1210,X1208)) ),
inference(variable_rename,[status(thm)],['reduce-12']) ).
tff(c_0_72,plain,
! [X713: vQConf] : ( vnoQConf != vsomeQConf(X713) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_66])]) ).
tcf(c_0_73,negated_conjecture,
vreduce(vqcond(vconstant(esk248_0),vq1,vq2),esk249_0,esk245_0) = vnoQConf,
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_67,c_0_68])]) ).
tcf(c_0_74,negated_conjecture,
( ( esk248_0 = vB(vyes) )
| ( esk248_0 = vB(vno) ) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_70]),c_0_57]),c_0_57]),c_0_30]),c_0_32]) ).
tcf(c_0_75,plain,
! [X11: vQMap,X32: vQuestionnaire,X55: vAnsMap,X34: vQuestionnaire] : vreduce(vqcond(vconstant(vB(vno)),X32,X34),X55,X11) = vsomeQConf(vQC(X55,X11,X34)),
inference(split_conjunct,[status(thm)],[c_0_71]) ).
tcf(c_0_76,plain,
! [X44: vQConf] : vnoQConf != vsomeQConf(X44),
inference(split_conjunct,[status(thm)],[c_0_72]) ).
tff(c_0_77,plain,
! [X1203: vQuestionnaire,X1204: vQuestionnaire,X1205: vAnsMap,X1206: vQMap] : ( vreduce(vqcond(vconstant(vB(vyes)),X1203,X1204),X1205,X1206) = vsomeQConf(vQC(X1205,X1206,X1203)) ),
inference(variable_rename,[status(thm)],['reduce-11']) ).
tcf(c_0_78,negated_conjecture,
esk248_0 = vB(vyes),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_74]),c_0_75]),c_0_76]) ).
tcf(c_0_79,plain,
! [X11: vQMap,X34: vQuestionnaire,X55: vAnsMap,X32: vQuestionnaire] : vreduce(vqcond(vconstant(vB(vyes)),X32,X34),X55,X11) = vsomeQConf(vQC(X55,X11,X32)),
inference(split_conjunct,[status(thm)],[c_0_77]) ).
cnf(c_0_80,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_78]),c_0_79]),c_0_76]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM265_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.35 % Computer : n013.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 14:21:23 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 Running first-order theorem proving
% 0.11/0.40 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
% 23.91/3.95 % Version: 3.5.1
% 23.91/3.95 % Preprocessing class: FSLMSMSMSSSNFFN.
% 23.91/3.95 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 23.91/3.95 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 23.91/3.95 % Starting new_bool_3 with 600s (2) cores
% 23.91/3.95 % Starting new_bool_1 with 300s (1) cores
% 23.91/3.95 % Starting sh5l with 300s (1) cores
% 23.91/3.95 % G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with pid 985923 completed with status 0
% 23.91/3.95 % Result found by G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S
% 23.91/3.95 % Preprocessing class: FSLMSMSMSSSNFFN.
% 23.91/3.95 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 23.91/3.95 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 23.91/3.95 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 23.91/3.95 % No SInE strategy applied
% 23.91/3.95 % Search class: FGUSM-SMLM32-DFFFFFNN
% 23.91/3.95 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 23.91/3.95 % Starting SubtermCWHack with 109s (1) cores
% 23.91/3.95 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 121s (1) cores
% 23.91/3.95 % Starting sh3 with 217s (1) cores
% 23.91/3.95 % Starting ho_unfolding_3 with 217s (1) cores
% 23.91/3.95 % sh3 with pid 985933 completed with status 0
% 23.91/3.95 % Result found by sh3
% 23.91/3.95 % Preprocessing class: FSLMSMSMSSSNFFN.
% 23.91/3.95 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 23.91/3.95 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 23.91/3.95 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 23.91/3.95 % No SInE strategy applied
% 23.91/3.95 % Search class: FGUSM-SMLM32-DFFFFFNN
% 23.91/3.95 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 23.91/3.95 % Starting SubtermCWHack with 109s (1) cores
% 23.91/3.95 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 121s (1) cores
% 23.91/3.95 % Starting sh3 with 217s (1) cores
% 23.91/3.95 % Preprocessing time : 0.035 s
% 23.91/3.95 % Presaturation interreduction done
% 23.91/3.95
% 23.91/3.95 % Proof found!
% 23.91/3.95 % SZS status Theorem
% 23.91/3.95 % SZS output start CNFRefutation
% See solution above
% 23.91/3.95 % Parsed axioms : 509
% 23.91/3.95 % Removed by relevancy pruning/SinE : 0
% 23.91/3.95 % Initial clauses : 2529
% 23.91/3.95 % Removed in clause preprocessing : 152
% 23.91/3.95 % Initial clauses in saturation : 2377
% 23.91/3.95 % Processed clauses : 9638
% 23.91/3.95 % ...of these trivial : 315
% 23.91/3.95 % ...subsumed : 3686
% 23.91/3.95 % ...remaining for further processing : 5637
% 23.91/3.95 % Other redundant clauses eliminated : 10162
% 23.91/3.95 % Clauses deleted for lack of memory : 0
% 23.91/3.95 % Backward-subsumed : 68
% 23.91/3.95 % Backward-rewritten : 86
% 23.91/3.95 % Generated clauses : 87310
% 23.91/3.95 % ...of the previous two non-redundant : 72923
% 23.91/3.95 % ...aggressively subsumed : 0
% 23.91/3.95 % Contextual simplify-reflections : 35
% 23.91/3.95 % Paramodulations : 76928
% 23.91/3.95 % Factorizations : 132
% 23.91/3.95 % NegExts : 0
% 23.91/3.95 % Equation resolutions : 10266
% 23.91/3.95 % Disequality decompositions : 0
% 23.91/3.95 % Total rewrite steps : 8357
% 23.91/3.95 % ...of those cached : 7499
% 23.91/3.95 % Propositional unsat checks : 1
% 23.91/3.95 % Propositional check models : 1
% 23.91/3.95 % Propositional check unsatisfiable : 0
% 23.91/3.95 % Propositional clauses : 0
% 23.91/3.95 % Propositional clauses after purity: 0
% 23.91/3.95 % Propositional unsat core size : 0
% 23.91/3.95 % Propositional preprocessing time : 0.000
% 23.91/3.95 % Propositional encoding time : 0.070
% 23.91/3.95 % Propositional solver time : 0.017
% 23.91/3.95 % Success case prop preproc time : 0.000
% 23.91/3.95 % Success case prop encoding time : 0.000
% 23.91/3.95 % Success case prop solver time : 0.000
% 23.91/3.95 % Current number of processed clauses : 3369
% 23.91/3.95 % Positive orientable unit clauses : 351
% 23.91/3.95 % Positive unorientable unit clauses: 22
% 23.91/3.95 % Negative unit clauses : 228
% 23.91/3.95 % Non-unit-clauses : 2768
% 23.91/3.95 % Current number of unprocessed clauses: 67351
% 23.91/3.95 % ...number of literals in the above : 325184
% 23.91/3.95 % Current number of archived formulas : 0
% 23.91/3.95 % Current number of archived clauses : 2249
% 23.91/3.95 % Clause-clause subsumption calls (NU) : 2085507
% 23.91/3.95 % Rec. Clause-clause subsumption calls : 694695
% 23.91/3.95 % Non-unit clause-clause subsumptions : 2563
% 23.91/3.95 % Unit Clause-clause subsumption calls : 189653
% 23.91/3.95 % Rewrite failures with RHS unbound : 388
% 23.91/3.95 % BW rewrite match attempts : 397
% 23.91/3.95 % BW rewrite match successes : 108
% 23.91/3.95 % Condensation attempts : 0
% 23.91/3.95 % Condensation successes : 0
% 23.91/3.95 % Termbank termtop insertions : 1548626
% 23.91/3.95 % Search garbage collected termcells : 16468
% 23.91/3.95
% 23.91/3.95 % -------------------------------------------------
% 23.91/3.95 % User time : 3.366 s
% 23.91/3.95 % System time : 0.077 s
% 23.91/3.95 % Total time : 3.443 s
% 23.91/3.95 % Maximum resident set size: 8844 pages
% 23.91/3.95
% 23.91/3.95 % -------------------------------------------------
% 23.91/3.95 % User time : 13.220 s
% 23.91/3.95 % System time : 0.362 s
% 23.91/3.95 % Total time : 13.581 s
% 23.91/3.95 % Maximum resident set size: 5632 pages
% 23.91/3.95 % E exiting
%------------------------------------------------------------------------------