%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : COM264_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 : 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:49 PM UTC 2026
% Result : Theorem 70.94s 9.50s
% Output : CNFRefutation 70.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 31
% Syntax : Number of formulae : 153 ( 95 unt; 0 typ; 0 def)
% Number of atoms : 273 ( 230 equ)
% Maximal formula atoms : 24 ( 1 avg)
% Number of connectives : 199 ( 79 ~; 84 |; 24 &)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 19 ( 18 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 59 ( 59 usr; 15 con; 0-5 aty)
% Number of variables : 296 ( 0 sgn 266 !; 30 ?; 296 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
vAval: $tType ).
tff(decl_sort2,type,
vExp: $tType ).
tff(decl_sort3,type,
vQMap: $tType ).
tff(decl_sort4,type,
vQID: $tType ).
tff(decl_sort5,type,
vAType: $tType ).
tff(decl_sort6,type,
vMapConf: $tType ).
tff(decl_sort7,type,
vOptExp: $tType ).
tff(decl_sort8,type,
vQuestionnaire: $tType ).
tff(decl_sort9,type,
vBinOpT: $tType ).
tff(decl_sort10,type,
vUnOpT: $tType ).
tff(decl_sort11,type,
vnat: $tType ).
tff(decl_sort12,type,
vOptAType: $tType ).
tff(decl_sort13,type,
vYN: $tType ).
tff(decl_sort14,type,
vstring: $tType ).
tff(decl_sort15,type,
vAnsMap: $tType ).
tff(decl_sort16,type,
vQConf: $tType ).
tff(decl_sort17,type,
vOptQConf: $tType ).
tff(decl_sort18,type,
vATMap: $tType ).
tff(decl_23,type,
vconstant: vAval > vExp ).
tff(decl_27,type,
vsomeExp: vExp > vOptExp ).
tff(decl_29,type,
vqcond: ( vQuestionnaire * ( vQuestionnaire * vExp ) ) > vQuestionnaire ).
tff(decl_31,type,
vnotop: vUnOpT ).
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_44,type,
vunop: ( vExp * vUnOpT ) > vExp ).
tff(decl_48,type,
vqseq: ( vQuestionnaire * vQuestionnaire ) > vQuestionnaire ).
tff(decl_51,type,
vsomeQConf: vQConf > vOptQConf ).
tff(decl_52,type,
vnoQConf: vOptQConf ).
tff(decl_53,type,
vnoExp: vOptExp ).
tff(decl_54,type,
vbinop: ( vExp * ( vBinOpT * vExp ) ) > vExp ).
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_67,type,
vqvar: vQID > vExp ).
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_93,type,
vexpIsValue: vExp > $o ).
tff(decl_95,type,
visValue: vQuestionnaire > $o ).
tff(decl_96,type,
vtypeAM: vAnsMap > vATMap ).
tff(decl_106,type,
vqcappend: ( vQuestionnaire * vQConf ) > vQConf ).
tff(decl_112,type,
vevalUnOp: ( vAval * vUnOpT ) > vOptExp ).
tff(decl_114,type,
vnot: vYN > vYN ).
tff(decl_115,type,
vreduce: ( vQMap * ( vAnsMap * vQuestionnaire ) ) > vOptQConf ).
tff(decl_119,type,
vtypeQM: vQMap > vATMap ).
tff(decl_120,type,
visSomeExp: vOptExp > $o ).
tff(decl_132,type,
vptcheck: ( vMapConf * ( vQuestionnaire * vMapConf ) ) > $o ).
tff(decl_140,type,
vgetExpValue: vExp > vAval ).
tff(decl_181,type,
esk17_1: vExp > vAval ).
tff(decl_182,type,
esk18_1: vExp > vQID ).
tff(decl_183,type,
esk19_1: vExp > vExp ).
tff(decl_184,type,
esk20_1: vExp > vBinOpT ).
tff(decl_185,type,
esk21_1: vExp > vExp ).
tff(decl_186,type,
esk22_1: vExp > vUnOpT ).
tff(decl_187,type,
esk23_1: vExp > vExp ).
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_300,type,
esk136_1: vExp > vAval ).
tff(decl_315,type,
esk151_2: ( vAval * vUnOpT ) > vYN ).
tff(decl_409,type,
esk245_5: ( vAnsMap * ( vExp * ( vATMap * ( vATMap * vQMap ) ) ) ) > vAval ).
tff(decl_410,type,
esk246_5: ( vAnsMap * ( vExp * ( vATMap * ( vATMap * vQMap ) ) ) ) > vAnsMap ).
tff(decl_411,type,
esk247_5: ( vAnsMap * ( vExp * ( vATMap * ( vATMap * vQMap ) ) ) ) > vQMap ).
tff(decl_412,type,
esk248_5: ( vAnsMap * ( vExp * ( vATMap * ( vATMap * vQMap ) ) ) ) > vQuestionnaire ).
tff(decl_413,type,
esk249_0: vQMap ).
tff(decl_414,type,
esk250_0: vATMap ).
tff(decl_415,type,
esk251_0: vATMap ).
tff(decl_416,type,
esk252_0: vExp ).
tff(decl_417,type,
esk253_0: vAnsMap ).
tff('Progress-qcond',conjecture,
! [X150: vQMap,X359: vATMap,X500: vATMap,X75: vExp,X126: vAnsMap] :
( ( vptcheck(vMC(vtypeAM(X126),vtypeQM(X150)),vqcond(X75,vq1,vq2),vMC(X359,X500))
& ~ visValue(vqcond(X75,vq1,vq2)) )
=> ? [X501: vAnsMap,X502: vQMap,X503: vQuestionnaire] : ( vreduce(vqcond(X75,vq1,vq2),X126,X150) = vsomeQConf(vQC(X501,X502,X503)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Progress-qcond') ).
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('Progress-qcond-e',axiom,
! [X150: vQMap,X359: vATMap,X500: vATMap,X75: vExp,X126: vAnsMap] :
( ( vptcheck(vMC(vtypeAM(X126),vtypeQM(X150)),vqcond(X75,vq1,vq2),vMC(X359,X500))
& ~ visValue(vqcond(X75,vq1,vq2))
& ! [X507: vAval] : ( X75 != vconstant(X507) ) )
=> ? [X501: vAnsMap,X502: vQMap,X503: vQuestionnaire] : ( vreduce(vqcond(X75,vq1,vq2),X126,X150) = vsomeQConf(vQC(X501,X502,X503)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Progress-qcond-e') ).
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('DIFF-constant-binop',axiom,
! [X21: vAval,X5: vExp,X22: vBinOpT,X9: vExp] : ( vconstant(X21) != vbinop(X5,X22,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','DIFF-constant-binop') ).
tff('DIFF-constant-unop',axiom,
! [X21: vAval,X23: vUnOpT,X5: vExp] : ( vconstant(X21) != vunop(X23,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','DIFF-constant-unop') ).
tff('DIFF-constant-qvar',axiom,
! [X21: vAval,X2: vQID] : ( vconstant(X21) != vqvar(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','DIFF-constant-qvar') ).
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('dom-Exp',axiom,
! [X20: vExp] :
( ? [X23: vUnOpT,X5: vExp] : ( X20 = vunop(X23,X5) )
| ? [X5: vExp,X22: vBinOpT,X9: vExp] : ( X20 = vbinop(X5,X22,X9) )
| ? [X2: vQID] : ( X20 = vqvar(X2) )
| ? [X21: vAval] : ( X20 = vconstant(X21) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','dom-Exp') ).
tff('dom-UnOpT',axiom,
! [X52: vUnOpT] : ( X52 = vnotop ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','dom-UnOpT') ).
tff('DIFF-YesNo-Number',axiom,
vYesNo != vNumber,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','DIFF-YesNo-Number') ).
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('getExpValue-0',axiom,
! [X76: vAval] : ( vgetExpValue(vconstant(X76)) = X76 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','getExpValue-0') ).
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('isSomeExp-1',axiom,
! [X170: vExp] : visSomeExp(vsomeExp(X170)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','isSomeExp-1') ).
tff('evalUnOp-0',axiom,
! [X220: vYN] : ( vevalUnOp(vnotop,vB(X220)) = vsomeExp(vconstant(vB(vnot(X220)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','evalUnOp-0') ).
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('DIFF-Number-Text',axiom,
vNumber != vText,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','DIFF-Number-Text') ).
tff('EQ-B',axiom,
! [X48: vYN,X50: vYN] :
( ( vB(X48) = vB(X50) )
=> ( X48 = X50 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','EQ-B') ).
tff('typeOf-0',axiom,
! [X78: vYN] : ( vtypeOf(vB(X78)) = vYesNo ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','typeOf-0') ).
tff('evalUnOp-1',axiom,
! [X221: vUnOpT,X222: vAval] :
( ( ! [X223: vYN] : ( X222 != vB(X223) )
| ( X221 != vnotop ) )
=> ( vevalUnOp(X221,X222) = vnoExp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','evalUnOp-1') ).
tff('expIsValue-1',axiom,
! [X75: vExp] :
( ! [X174: vAval] : ( X75 != vconstant(X174) )
=> ~ vexpIsValue(X75) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','expIsValue-1') ).
tff('isSomeExp-0',axiom,
~ visSomeExp(vnoExp),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','isSomeExp-0') ).
tff('dom-YN',axiom,
! [X10: vYN] :
( ( X10 = vno )
| ( X10 = vyes ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','dom-YN') ).
tff('expIsValue-0',axiom,
! [X173: vAval] : vexpIsValue(vconstant(X173)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','expIsValue-0') ).
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('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(c_0_31,negated_conjecture,
~ ! [X150: vQMap,X359: vATMap,X500: vATMap,X75: vExp,X126: vAnsMap] :
( ( vptcheck(vMC(vtypeAM(X126),vtypeQM(X150)),vqcond(X75,vq1,vq2),vMC(X359,X500))
& ~ visValue(vqcond(X75,vq1,vq2)) )
=> ? [X501: vAnsMap,X502: vQMap,X503: vQuestionnaire] : ( vreduce(vqcond(X75,vq1,vq2),X126,X150) = vsomeQConf(vQC(X501,X502,X503)) ) ),
inference(assume_negation,[status(cth)],['Progress-qcond']) ).
tff(c_0_32,negated_conjecture,
~ ! [X150: vQMap,X359: vATMap,X500: vATMap,X75: vExp,X126: vAnsMap] :
( ( vptcheck(vMC(vtypeAM(X126),vtypeQM(X150)),vqcond(X75,vq1,vq2),vMC(X359,X500))
& ~ visValue(vqcond(X75,vq1,vq2)) )
=> ? [X501: vAnsMap,X502: vQMap,X503: vQuestionnaire] : ( vreduce(vqcond(X75,vq1,vq2),X126,X150) = vsomeQConf(vQC(X501,X502,X503)) ) ),
inference(fof_simplification,[status(thm)],[c_0_31]) ).
tff(c_0_33,negated_conjecture,
! [X1658: vAnsMap,X1659: vQMap,X1660: vQuestionnaire] :
( ( vreduce(vqcond(esk252_0,vq1,vq2),esk253_0,esk249_0) != vsomeQConf(vQC(X1658,X1659,X1660)) )
& vptcheck(vMC(vtypeAM(esk253_0),vtypeQM(esk249_0)),vqcond(esk252_0,vq1,vq2),vMC(esk250_0,esk251_0))
& ~ visValue(vqcond(esk252_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_32])])])])]) ).
tff(c_0_34,plain,
! [X1027: vQConf,X1028: vQuestionnaire] :
( ( vqcappend(X1027,X1028) = vQC(esk131_2(X1027,X1028),esk132_2(X1027,X1028),vqseq(esk133_2(X1027,X1028),esk134_2(X1027,X1028))) )
& ( X1028 = esk134_2(X1027,X1028) )
& ( X1027 = vQC(esk131_2(X1027,X1028),esk132_2(X1027,X1028),esk133_2(X1027,X1028)) ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['qcappend-INV'])]) ).
tff(c_0_35,plain,
! [X150: vQMap,X359: vATMap,X500: vATMap,X75: vExp,X126: vAnsMap] :
( ( vptcheck(vMC(vtypeAM(X126),vtypeQM(X150)),vqcond(X75,vq1,vq2),vMC(X359,X500))
& ~ visValue(vqcond(X75,vq1,vq2))
& ! [X507: vAval] : ( X75 != vconstant(X507) ) )
=> ? [X501: vAnsMap,X502: vQMap,X503: vQuestionnaire] : ( vreduce(vqcond(X75,vq1,vq2),X126,X150) = vsomeQConf(vQC(X501,X502,X503)) ) ),
inference(fof_simplification,[status(thm)],['Progress-qcond-e']) ).
tcf(c_0_36,negated_conjecture,
! [X11: vQMap,X55: vAnsMap,X32: vQuestionnaire] : vreduce(vqcond(esk252_0,vq1,vq2),esk253_0,esk249_0) != vsomeQConf(vQC(X55,X11,X32)),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
tcf(c_0_37,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_34]) ).
tff(c_0_38,plain,
! [X706: vOptQConf] :
( ( X706 = vsomeQConf(esk33_1(X706)) )
| ( X706 = vnoQConf ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['dom-OptQConf'])]) ).
tff(c_0_39,plain,
! [X44: vQConf] : ( vnoQConf != vsomeQConf(X44) ),
inference(fof_simplification,[status(thm)],['DIFF-noQConf-someQConf']) ).
tff(c_0_40,plain,
! [X21: vAval,X5: vExp,X22: vBinOpT,X9: vExp] : ( vconstant(X21) != vbinop(X5,X22,X9) ),
inference(fof_simplification,[status(thm)],['DIFF-constant-binop']) ).
tff(c_0_41,plain,
! [X1644: vQMap,X1645: vATMap,X1646: vATMap,X1647: vExp,X1648: vAnsMap] :
( ( vreduce(vqcond(X1647,vq1,vq2),X1648,X1644) = vsomeQConf(vQC(esk246_5(X1644,X1645,X1646,X1647,X1648),esk247_5(X1644,X1645,X1646,X1647,X1648),esk248_5(X1644,X1645,X1646,X1647,X1648))) )
| ~ vptcheck(vMC(vtypeAM(X1648),vtypeQM(X1644)),vqcond(X1647,vq1,vq2),vMC(X1645,X1646))
| visValue(vqcond(X1647,vq1,vq2))
| ( X1647 = vconstant(esk245_5(X1644,X1645,X1646,X1647,X1648)) ) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_35])])])]) ).
tcf(c_0_42,negated_conjecture,
! [X44: vQConf] : vreduce(vqcond(esk252_0,vq1,vq2),esk253_0,esk249_0) != vsomeQConf(X44),
inference(spm,[status(thm)],[c_0_36,c_0_37]) ).
tcf(c_0_43,plain,
! [X43: vOptQConf] :
( ( X43 = vsomeQConf(esk33_1(X43)) )
| ( X43 = vnoQConf ) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
tff(c_0_44,plain,
! [X710: vQConf] : ( vnoQConf != vsomeQConf(X710) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_39])]) ).
tff(c_0_45,plain,
! [X21: vAval,X23: vUnOpT,X5: vExp] : ( vconstant(X21) != vunop(X23,X5) ),
inference(fof_simplification,[status(thm)],['DIFF-constant-unop']) ).
tff(c_0_46,plain,
! [X21: vAval,X2: vQID] : ( vconstant(X21) != vqvar(X2) ),
inference(fof_simplification,[status(thm)],['DIFF-constant-qvar']) ).
tff(c_0_47,plain,
! [X713: vAType,X714: vAType] :
( ( X713 = X714 )
| ( vsomeAType(X713) != vsomeAType(X714) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['EQ-someAType'])])]) ).
tff(c_0_48,plain,
! [X1339: vATMap,X1340: vYN] : ( vecheck(X1339,vconstant(vB(X1340))) = vsomeAType(vYesNo) ),
inference(variable_rename,[status(thm)],['echeck-0']) ).
tff(c_0_49,plain,
vYesNo != vText,
inference(fof_simplification,[status(thm)],['DIFF-YesNo-Text']) ).
tff(c_0_50,plain,
! [X622: vAval,X623: vExp,X624: vBinOpT,X625: vExp] : ( vconstant(X622) != vbinop(X623,X624,X625) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_40])]) ).
tcf(c_0_51,plain,
! [X5: vExp,X11: vQMap,X15: vATMap,X55: vAnsMap,X16: vATMap] :
( ~ vptcheck(vMC(vtypeAM(X55),vtypeQM(X11)),vqcond(X5,vq1,vq2),vMC(X15,X16))
| ( vreduce(vqcond(X5,vq1,vq2),X55,X11) = vsomeQConf(vQC(esk246_5(X11,X15,X16,X5,X55),esk247_5(X11,X15,X16,X5,X55),esk248_5(X11,X15,X16,X5,X55))) )
| visValue(vqcond(X5,vq1,vq2))
| ( X5 = vconstant(esk245_5(X11,X15,X16,X5,X55)) ) ),
inference(split_conjunct,[status(thm)],[c_0_41]) ).
tcf(c_0_52,negated_conjecture,
vptcheck(vMC(vtypeAM(esk253_0),vtypeQM(esk249_0)),vqcond(esk252_0,vq1,vq2),vMC(esk250_0,esk251_0)),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
tcf(c_0_53,negated_conjecture,
vreduce(vqcond(esk252_0,vq1,vq2),esk253_0,esk249_0) = vnoQConf,
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_42,c_0_43])]) ).
tcf(c_0_54,plain,
! [X44: vQConf] : vnoQConf != vsomeQConf(X44),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
tcf(c_0_55,negated_conjecture,
~ visValue(vqcond(esk252_0,vq1,vq2)),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
tff(c_0_56,plain,
! [X598: vExp] :
( ( X598 = vunop(esk22_1(X598),esk23_1(X598)) )
| ( X598 = vbinop(esk19_1(X598),esk20_1(X598),esk21_1(X598)) )
| ( X598 = vqvar(esk18_1(X598)) )
| ( X598 = vconstant(esk17_1(X598)) ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['dom-Exp'])]) ).
tff(c_0_57,plain,
! [X732: vUnOpT] : ( X732 = vnotop ),
inference(variable_rename,[status(thm)],['dom-UnOpT']) ).
tff(c_0_58,plain,
! [X626: vAval,X627: vUnOpT,X628: vExp] : ( vconstant(X626) != vunop(X627,X628) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_45])]) ).
tff(c_0_59,plain,
! [X620: vAval,X621: vQID] : ( vconstant(X620) != vqvar(X621) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_46])]) ).
tff(c_0_60,plain,
vYesNo != vNumber,
inference(fof_simplification,[status(thm)],['DIFF-YesNo-Number']) ).
tcf(c_0_61,plain,
! [X4: vAType,X8: vAType] :
( ( vsomeAType(X4) != vsomeAType(X8) )
| ( X4 = X8 ) ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
tcf(c_0_62,plain,
! [X15: vATMap,X10: vYN] : vecheck(X15,vconstant(vB(X10))) = vsomeAType(vYesNo),
inference(split_conjunct,[status(thm)],[c_0_48]) ).
tff(c_0_63,plain,
! [X1343: vATMap,X1344: vstring] : ( vecheck(X1343,vconstant(vT(X1344))) = vsomeAType(vText) ),
inference(variable_rename,[status(thm)],['echeck-2']) ).
tff(c_0_64,plain,
vYesNo != vText,
inference(fof_nnf,[status(thm)],[c_0_49]) ).
tcf(c_0_65,plain,
! [X5: vExp,X22: vBinOpT,X21: vAval,X9: vExp] : vconstant(X21) != vbinop(X5,X22,X9),
inference(split_conjunct,[status(thm)],[c_0_50]) ).
tcf(c_0_66,negated_conjecture,
vconstant(esk245_5(esk249_0,esk250_0,esk251_0,esk252_0,esk253_0)) = esk252_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_52]),c_0_53]),c_0_54]),c_0_55]) ).
tcf(c_0_67,plain,
! [X5: vExp] :
( ( X5 = vunop(esk22_1(X5),esk23_1(X5)) )
| ( X5 = vbinop(esk19_1(X5),esk20_1(X5),esk21_1(X5)) )
| ( X5 = vqvar(esk18_1(X5)) )
| ( X5 = vconstant(esk17_1(X5)) ) ),
inference(split_conjunct,[status(thm)],[c_0_56]) ).
tcf(c_0_68,plain,
! [X23: vUnOpT] : X23 = vnotop,
inference(split_conjunct,[status(thm)],[c_0_57]) ).
tcf(c_0_69,plain,
! [X23: vUnOpT,X21: vAval,X5: vExp] : vconstant(X21) != vunop(X23,X5),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
tcf(c_0_70,plain,
! [X21: vAval,X2: vQID] : vconstant(X21) != vqvar(X2),
inference(split_conjunct,[status(thm)],[c_0_59]) ).
tff(c_0_71,plain,
! [X1341: vATMap,X1342: vnat] : ( vecheck(X1341,vconstant(vNum(X1342))) = vsomeAType(vNumber) ),
inference(variable_rename,[status(thm)],['echeck-1']) ).
tff(c_0_72,plain,
vYesNo != vNumber,
inference(fof_nnf,[status(thm)],[c_0_60]) ).
tcf(c_0_73,plain,
! [X15: vATMap,X10: vYN,X4: vAType] :
( ( vecheck(X15,vconstant(vB(X10))) != vsomeAType(X4) )
| ( vYesNo = X4 ) ),
inference(spm,[status(thm)],[c_0_61,c_0_62]) ).
tcf(c_0_74,plain,
! [X15: vATMap,X49: vstring] : vecheck(X15,vconstant(vT(X49))) = vsomeAType(vText),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
tcf(c_0_75,plain,
vYesNo != vText,
inference(split_conjunct,[status(thm)],[c_0_64]) ).
tff(c_0_76,plain,
! [X835: vAval] : ( vgetExpValue(vconstant(X835)) = X835 ),
inference(variable_rename,[status(thm)],['getExpValue-0']) ).
tcf(c_0_77,negated_conjecture,
! [X5: vExp,X22: vBinOpT,X9: vExp] : esk252_0 != vbinop(X5,X22,X9),
inference(spm,[status(thm)],[c_0_65,c_0_66]) ).
tcf(c_0_78,plain,
! [X5: vExp] :
( ( vconstant(esk17_1(X5)) = X5 )
| ( vqvar(esk18_1(X5)) = X5 )
| ( vunop(vnotop,esk23_1(X5)) = X5 )
| ( vbinop(esk19_1(X5),esk20_1(X5),esk21_1(X5)) = X5 ) ),
inference(rw,[status(thm)],[c_0_67,c_0_68]) ).
tcf(c_0_79,negated_conjecture,
! [X23: vUnOpT,X5: vExp] : esk252_0 != vunop(X23,X5),
inference(spm,[status(thm)],[c_0_69,c_0_66]) ).
tcf(c_0_80,negated_conjecture,
! [X2: vQID] : esk252_0 != vqvar(X2),
inference(spm,[status(thm)],[c_0_70,c_0_66]) ).
tcf(c_0_81,plain,
! [X15: vATMap,X29: vnat] : vecheck(X15,vconstant(vNum(X29))) = vsomeAType(vNumber),
inference(split_conjunct,[status(thm)],[c_0_71]) ).
tcf(c_0_82,plain,
vYesNo != vNumber,
inference(split_conjunct,[status(thm)],[c_0_72]) ).
tcf(c_0_83,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_73,c_0_74]),c_0_75]) ).
tff(c_0_84,plain,
! [X918: vAval] :
( ( ( vtypeOf(X918) = vYesNo )
| ( vtypeOf(X918) = vNumber )
| ( vtypeOf(X918) = vText ) )
& ( ( vtypeOf(X918) = vYesNo )
| ( vtypeOf(X918) = vNumber )
| ( X918 = vT(esk87_1(X918)) ) )
& ( ( vtypeOf(X918) = vYesNo )
| ( X918 = vNum(esk86_1(X918)) )
| ( vtypeOf(X918) = vText ) )
& ( ( vtypeOf(X918) = vYesNo )
| ( X918 = vNum(esk86_1(X918)) )
| ( X918 = vT(esk87_1(X918)) ) )
& ( ( X918 = vB(esk85_1(X918)) )
| ( vtypeOf(X918) = vNumber )
| ( vtypeOf(X918) = vText ) )
& ( ( X918 = vB(esk85_1(X918)) )
| ( vtypeOf(X918) = vNumber )
| ( X918 = vT(esk87_1(X918)) ) )
& ( ( X918 = vB(esk85_1(X918)) )
| ( X918 = vNum(esk86_1(X918)) )
| ( vtypeOf(X918) = vText ) )
& ( ( X918 = vB(esk85_1(X918)) )
| ( X918 = vNum(esk86_1(X918)) )
| ( X918 = vT(esk87_1(X918)) ) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],['typeOf-INV'])])])]) ).
tcf(c_0_85,plain,
! [X21: vAval] : vgetExpValue(vconstant(X21)) = X21,
inference(split_conjunct,[status(thm)],[c_0_76]) ).
tcf(c_0_86,negated_conjecture,
vconstant(esk17_1(esk252_0)) = esk252_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_77,c_0_78])]),c_0_79]),c_0_80]) ).
tcf(c_0_87,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_73,c_0_81]),c_0_82]) ).
tff(c_0_88,plain,
! [X1033: vExp] : visSomeExp(vsomeExp(X1033)),
inference(variable_rename,[status(thm)],['isSomeExp-1']) ).
tff(c_0_89,plain,
! [X1103: vYN] : ( vevalUnOp(vnotop,vB(X1103)) = vsomeExp(vconstant(vB(vnot(X1103)))) ),
inference(variable_rename,[status(thm)],['evalUnOp-0']) ).
tcf(c_0_90,plain,
! [X15: vATMap,X49: vstring] : vecheck(X15,vconstant(vT(X49))) != vsomeAType(vYesNo),
inference(spm,[status(thm)],[c_0_83,c_0_62]) ).
tcf(c_0_91,plain,
! [X21: vAval] :
( ( vtypeOf(X21) = vYesNo )
| ( vtypeOf(X21) = vNumber )
| ( X21 = vT(esk87_1(X21)) ) ),
inference(split_conjunct,[status(thm)],[c_0_84]) ).
tcf(c_0_92,negated_conjecture,
esk17_1(esk252_0) = vgetExpValue(esk252_0),
inference(spm,[status(thm)],[c_0_85,c_0_86]) ).
tff(c_0_93,plain,
! [X1551: vATMap,X1552: vQuestionnaire,X1553: vATMap,X1554: vATMap,X1555: vATMap,X1556: vExp,X1557: vQuestionnaire] :
( ( vecheck(X1553,X1556) = vsomeAType(vYesNo) )
| ~ vptcheck(vMC(X1553,X1551),vqcond(X1556,X1552,X1557),vMC(X1554,X1555)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['Tqcond_inv1'])])]) ).
tcf(c_0_94,plain,
! [X15: vATMap,X29: vnat] : vsomeAType(vYesNo) != vecheck(X15,vconstant(vNum(X29))),
inference(spm,[status(thm)],[c_0_87,c_0_62]) ).
tcf(c_0_95,plain,
! [X21: vAval] :
( ( vtypeOf(X21) = vYesNo )
| ( X21 = vNum(esk86_1(X21)) )
| ( vtypeOf(X21) = vText ) ),
inference(split_conjunct,[status(thm)],[c_0_84]) ).
tcf(c_0_96,plain,
! [X5: vExp] : visSomeExp(vsomeExp(X5)),
inference(split_conjunct,[status(thm)],[c_0_88]) ).
tcf(c_0_97,plain,
! [X10: vYN] : vevalUnOp(vnotop,vB(X10)) = vsomeExp(vconstant(vB(vnot(X10)))),
inference(split_conjunct,[status(thm)],[c_0_89]) ).
tcf(c_0_98,plain,
! [X15: vATMap,X21: vAval] :
( ( vecheck(X15,vconstant(X21)) != vsomeAType(vYesNo) )
| ( vtypeOf(X21) = vNumber )
| ( vtypeOf(X21) = vYesNo ) ),
inference(spm,[status(thm)],[c_0_90,c_0_91]) ).
tcf(c_0_99,negated_conjecture,
vconstant(vgetExpValue(esk252_0)) = esk252_0,
inference(rw,[status(thm)],[c_0_86,c_0_92]) ).
tcf(c_0_100,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_93]) ).
tcf(c_0_101,plain,
! [X15: vATMap,X21: vAval] :
( ( vsomeAType(vYesNo) != vecheck(X15,vconstant(X21)) )
| ( vtypeOf(X21) = vYesNo )
| ( vtypeOf(X21) = vText ) ),
inference(spm,[status(thm)],[c_0_94,c_0_95]) ).
tff(c_0_102,plain,
vNumber != vText,
inference(fof_simplification,[status(thm)],['DIFF-Number-Text']) ).
tff(c_0_103,plain,
! [X720: vYN,X721: vYN] :
( ( X720 = X721 )
| ( vB(X720) != vB(X721) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['EQ-B'])])]) ).
tff(c_0_104,plain,
! [X915: vYN] : ( vtypeOf(vB(X915)) = vYesNo ),
inference(variable_rename,[status(thm)],['typeOf-0']) ).
tff(c_0_105,plain,
! [X221: vUnOpT,X222: vAval] :
( ( ! [X223: vYN] : ( X222 != vB(X223) )
| ( X221 != vnotop ) )
=> ( vevalUnOp(X221,X222) = vnoExp ) ),
inference(fof_simplification,[status(thm)],['evalUnOp-1']) ).
tcf(c_0_106,plain,
! [X10: vYN] : visSomeExp(vevalUnOp(vnotop,vB(X10))),
inference(spm,[status(thm)],[c_0_96,c_0_97]) ).
tcf(c_0_107,plain,
! [X23: vUnOpT,X28: vUnOpT] : X23 = X28,
inference(spm,[status(thm)],[c_0_68,c_0_68]) ).
tcf(c_0_108,negated_conjecture,
! [X15: vATMap] :
( ( vecheck(X15,esk252_0) != vsomeAType(vYesNo) )
| ( vtypeOf(vgetExpValue(esk252_0)) = vYesNo )
| ( vtypeOf(vgetExpValue(esk252_0)) = vNumber ) ),
inference(spm,[status(thm)],[c_0_98,c_0_99]) ).
tcf(c_0_109,negated_conjecture,
vecheck(vtypeAM(esk253_0),esk252_0) = vsomeAType(vYesNo),
inference(spm,[status(thm)],[c_0_100,c_0_52]) ).
tcf(c_0_110,negated_conjecture,
! [X15: vATMap] :
( ( vecheck(X15,esk252_0) != vsomeAType(vYesNo) )
| ( vtypeOf(vgetExpValue(esk252_0)) = vText )
| ( vtypeOf(vgetExpValue(esk252_0)) = vYesNo ) ),
inference(spm,[status(thm)],[c_0_101,c_0_99]) ).
tff(c_0_111,plain,
vNumber != vText,
inference(fof_nnf,[status(thm)],[c_0_102]) ).
tcf(c_0_112,plain,
! [X10: vYN,X48: vYN] :
( ( vB(X10) != vB(X48) )
| ( X10 = X48 ) ),
inference(split_conjunct,[status(thm)],[c_0_103]) ).
tcf(c_0_113,plain,
! [X21: vAval] :
( ( X21 = vB(esk85_1(X21)) )
| ( vtypeOf(X21) = vNumber )
| ( vtypeOf(X21) = vText ) ),
inference(split_conjunct,[status(thm)],[c_0_84]) ).
tcf(c_0_114,plain,
! [X10: vYN] : vtypeOf(vB(X10)) = vYesNo,
inference(split_conjunct,[status(thm)],[c_0_104]) ).
tff(c_0_115,plain,
! [X1104: vUnOpT,X1105: vAval] :
( ( ( vevalUnOp(X1104,X1105) = vnoExp )
| ( X1105 = vB(esk151_2(X1104,X1105)) ) )
& ( ( vevalUnOp(X1104,X1105) = vnoExp )
| ( X1104 = vnotop ) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_105])])])]) ).
tff(c_0_116,plain,
! [X75: vExp] :
( ! [X174: vAval] : ( X75 != vconstant(X174) )
=> ~ vexpIsValue(X75) ),
inference(fof_simplification,[status(thm)],['expIsValue-1']) ).
tcf(c_0_117,plain,
! [X23: vUnOpT,X10: vYN] : visSomeExp(vevalUnOp(X23,vB(X10))),
inference(spm,[status(thm)],[c_0_106,c_0_107]) ).
tcf(c_0_118,negated_conjecture,
( ( vtypeOf(vgetExpValue(esk252_0)) = vNumber )
| ( vtypeOf(vgetExpValue(esk252_0)) = vYesNo ) ),
inference(spm,[status(thm)],[c_0_108,c_0_109]) ).
tcf(c_0_119,negated_conjecture,
( ( vtypeOf(vgetExpValue(esk252_0)) = vYesNo )
| ( vtypeOf(vgetExpValue(esk252_0)) = vText ) ),
inference(spm,[status(thm)],[c_0_110,c_0_109]) ).
tcf(c_0_120,plain,
vNumber != vText,
inference(split_conjunct,[status(thm)],[c_0_111]) ).
tcf(c_0_121,plain,
! [X10: vYN] : esk85_1(vB(X10)) = X10,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_112,c_0_113])]),c_0_114]),c_0_114]),c_0_82]),c_0_75]) ).
tcf(c_0_122,plain,
! [X23: vUnOpT,X21: vAval] :
( ( vevalUnOp(X23,X21) = vnoExp )
| ( X21 = vB(esk151_2(X23,X21)) ) ),
inference(split_conjunct,[status(thm)],[c_0_115]) ).
tff(c_0_123,plain,
~ visSomeExp(vnoExp),
inference(fof_simplification,[status(thm)],['isSomeExp-0']) ).
tff(c_0_124,plain,
! [X1038: vExp] :
( ~ vexpIsValue(X1038)
| ( X1038 = vconstant(esk136_1(X1038)) ) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_116])])])]) ).
tcf(c_0_125,plain,
! [X23: vUnOpT,X21: vAval] :
( visSomeExp(vevalUnOp(X23,X21))
| ( vtypeOf(X21) = vNumber )
| ( vtypeOf(X21) = vText ) ),
inference(spm,[status(thm)],[c_0_117,c_0_113]) ).
tcf(c_0_126,negated_conjecture,
vtypeOf(vgetExpValue(esk252_0)) = vYesNo,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_118,c_0_119]),c_0_75]),c_0_120]) ).
tcf(c_0_127,plain,
! [X23: vUnOpT,X21: vAval] :
( ( vevalUnOp(X23,X21) = vnoExp )
| ( esk151_2(X23,X21) = esk85_1(X21) ) ),
inference(spm,[status(thm)],[c_0_121,c_0_122]) ).
tff(c_0_128,plain,
~ visSomeExp(vnoExp),
inference(fof_nnf,[status(thm)],[c_0_123]) ).
tff(c_0_129,plain,
! [X569: vYN] :
( ( X569 = vno )
| ( X569 = vyes ) ),
inference(variable_rename,[status(thm)],['dom-YN']) ).
tcf(c_0_130,plain,
! [X5: vExp] :
( ~ vexpIsValue(X5)
| ( X5 = vconstant(esk136_1(X5)) ) ),
inference(split_conjunct,[status(thm)],[c_0_124]) ).
tcf(c_0_131,negated_conjecture,
! [X23: vUnOpT] : visSomeExp(vevalUnOp(X23,vgetExpValue(esk252_0))),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_125,c_0_126]),c_0_75]),c_0_82]) ).
tcf(c_0_132,plain,
! [X23: vUnOpT,X21: vAval] :
( ( vB(esk85_1(X21)) = X21 )
| ( vevalUnOp(X23,X21) = vnoExp ) ),
inference(spm,[status(thm)],[c_0_122,c_0_127]) ).
tcf(c_0_133,plain,
~ visSomeExp(vnoExp),
inference(split_conjunct,[status(thm)],[c_0_128]) ).
tcf(c_0_134,plain,
! [X10: vYN] :
( ( X10 = vno )
| ( X10 = vyes ) ),
inference(split_conjunct,[status(thm)],[c_0_129]) ).
tff(c_0_135,plain,
! [X1037: vAval] : vexpIsValue(vconstant(X1037)),
inference(variable_rename,[status(thm)],['expIsValue-0']) ).
tcf(c_0_136,plain,
! [X5: vExp] :
( ~ vexpIsValue(X5)
| ( esk136_1(X5) = vgetExpValue(X5) ) ),
inference(spm,[status(thm)],[c_0_85,c_0_130]) ).
tcf(c_0_137,negated_conjecture,
vB(esk85_1(vgetExpValue(esk252_0))) = vgetExpValue(esk252_0),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_131,c_0_132]),c_0_133]) ).
tcf(c_0_138,plain,
! [X21: vAval] :
( ( vB(vno) = X21 )
| ( vtypeOf(X21) = vNumber )
| ( vtypeOf(X21) = vText )
| ( esk85_1(X21) = vyes ) ),
inference(spm,[status(thm)],[c_0_113,c_0_134]) ).
tcf(c_0_139,plain,
! [X21: vAval] : vexpIsValue(vconstant(X21)),
inference(split_conjunct,[status(thm)],[c_0_135]) ).
tcf(c_0_140,plain,
! [X5: vExp] :
( ~ vexpIsValue(X5)
| ( vconstant(vgetExpValue(X5)) = X5 ) ),
inference(spm,[status(thm)],[c_0_130,c_0_136]) ).
tcf(c_0_141,negated_conjecture,
( ( vgetExpValue(esk252_0) = vB(vyes) )
| ( vgetExpValue(esk252_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_137,c_0_138]),c_0_126]),c_0_126]),c_0_75]),c_0_82]) ).
tcf(c_0_142,negated_conjecture,
vexpIsValue(esk252_0),
inference(spm,[status(thm)],[c_0_139,c_0_66]) ).
tff(c_0_143,plain,
! [X1200: vQuestionnaire,X1201: vQuestionnaire,X1202: vAnsMap,X1203: vQMap] : ( vreduce(vqcond(vconstant(vB(vyes)),X1200,X1201),X1202,X1203) = vsomeQConf(vQC(X1202,X1203,X1200)) ),
inference(variable_rename,[status(thm)],['reduce-11']) ).
tff(c_0_144,plain,
! [X1204: vQuestionnaire,X1205: vQuestionnaire,X1206: vAnsMap,X1207: vQMap] : ( vreduce(vqcond(vconstant(vB(vno)),X1204,X1205),X1206,X1207) = vsomeQConf(vQC(X1206,X1207,X1205)) ),
inference(variable_rename,[status(thm)],['reduce-12']) ).
tcf(c_0_145,negated_conjecture,
( ( esk252_0 = vconstant(vB(vno)) )
| ( vgetExpValue(esk252_0) = vB(vyes) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_140,c_0_141]),c_0_142])]) ).
tcf(c_0_146,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_143]) ).
tcf(c_0_147,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_144]) ).
tcf(c_0_148,negated_conjecture,
( ( esk252_0 = vconstant(vB(vyes)) )
| ( esk252_0 = vconstant(vB(vno)) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_140,c_0_145]),c_0_142])]) ).
tcf(c_0_149,plain,
! [X34: vQuestionnaire,X32: vQuestionnaire,X55: vAnsMap,X35: vQuestionnaire,X11: vQMap] : vreduce(vqcond(vconstant(vB(vyes)),X32,X34),X55,X11) = vreduce(vqcond(vconstant(vB(vno)),X35,X32),X55,X11),
inference(spm,[status(thm)],[c_0_146,c_0_147]) ).
tcf(c_0_150,plain,
! [X55: vAnsMap,X34: vQuestionnaire,X32: vQuestionnaire,X11: vQMap] : vnoQConf != vreduce(vqcond(vconstant(vB(vyes)),X32,X34),X55,X11),
inference(spm,[status(thm)],[c_0_54,c_0_146]) ).
tcf(c_0_151,negated_conjecture,
esk252_0 = vconstant(vB(vyes)),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_148]),c_0_149]),c_0_150]) ).
cnf(c_0_152,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_151]),c_0_150]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM264_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 14:23:32 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 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
% 70.94/9.50 % Version: 3.5.1
% 70.94/9.50 % Preprocessing class: FSLMSMSMSSSNFFN.
% 70.94/9.50 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 70.94/9.50 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 70.94/9.50 % Starting new_bool_3 with 600s (2) cores
% 70.94/9.50 % Starting new_bool_1 with 300s (1) cores
% 70.94/9.50 % Starting sh5l with 300s (1) cores
% 70.94/9.50 % G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with pid 342343 completed with status 0
% 70.94/9.50 % Result found by G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S
% 70.94/9.50 % Preprocessing class: FSLMSMSMSSSNFFN.
% 70.94/9.50 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 70.94/9.50 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 70.94/9.50 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 70.94/9.50 % No SInE strategy applied
% 70.94/9.50 % Search class: FGUSM-SMLM32-DFFFFFNN
% 70.94/9.50 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 70.94/9.50 % Starting SubtermCWHack with 109s (1) cores
% 70.94/9.50 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 121s (1) cores
% 70.94/9.50 % Starting sh3 with 217s (1) cores
% 70.94/9.50 % Starting ho_unfolding_3 with 217s (1) cores
% 70.94/9.50 % ho_unfolding_3 with pid 342392 completed with status 0
% 70.94/9.50 % Result found by ho_unfolding_3
% 70.94/9.50 % Preprocessing class: FSLMSMSMSSSNFFN.
% 70.94/9.50 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 70.94/9.50 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 70.94/9.50 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 70.94/9.50 % No SInE strategy applied
% 70.94/9.50 % Search class: FGUSM-SMLM32-DFFFFFNN
% 70.94/9.50 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 70.94/9.50 % Starting SubtermCWHack with 109s (1) cores
% 70.94/9.50 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 121s (1) cores
% 70.94/9.50 % Starting sh3 with 217s (1) cores
% 70.94/9.50 % Starting ho_unfolding_3 with 217s (1) cores
% 70.94/9.50 % Preprocessing time : 0.033 s
% 70.94/9.50 % Presaturation interreduction done
% 70.94/9.50
% 70.94/9.50 % Proof found!
% 70.94/9.50 % SZS status Theorem
% 70.94/9.50 % SZS output start CNFRefutation
% See solution above
% 70.94/9.50 % Parsed axioms : 510
% 70.94/9.50 % Removed by relevancy pruning/SinE : 0
% 70.94/9.50 % Initial clauses : 2530
% 70.94/9.50 % Removed in clause preprocessing : 152
% 70.94/9.50 % Initial clauses in saturation : 2378
% 70.94/9.50 % Processed clauses : 30395
% 70.94/9.50 % ...of these trivial : 615
% 70.94/9.50 % ...subsumed : 21589
% 70.94/9.50 % ...remaining for further processing : 8191
% 70.94/9.50 % Other redundant clauses eliminated : 19110
% 70.94/9.50 % Clauses deleted for lack of memory : 0
% 70.94/9.50 % Backward-subsumed : 302
% 70.94/9.50 % Backward-rewritten : 375
% 70.94/9.50 % Generated clauses : 253696
% 70.94/9.50 % ...of the previous two non-redundant : 203498
% 70.94/9.50 % ...aggressively subsumed : 0
% 70.94/9.50 % Contextual simplify-reflections : 63
% 70.94/9.50 % Paramodulations : 233722
% 70.94/9.50 % Factorizations : 684
% 70.94/9.50 % NegExts : 0
% 70.94/9.50 % Equation resolutions : 19304
% 70.94/9.50 % Disequality decompositions : 0
% 70.94/9.50 % Total rewrite steps : 67275
% 70.94/9.50 % ...of those cached : 65637
% 70.94/9.50 % Propositional unsat checks : 0
% 70.94/9.50 % Propositional check models : 0
% 70.94/9.50 % Propositional check unsatisfiable : 0
% 70.94/9.50 % Propositional clauses : 0
% 70.94/9.50 % Propositional clauses after purity: 0
% 70.94/9.50 % Propositional unsat core size : 0
% 70.94/9.50 % Propositional preprocessing time : 0.000
% 70.94/9.50 % Propositional encoding time : 0.000
% 70.94/9.50 % Propositional solver time : 0.000
% 70.94/9.50 % Success case prop preproc time : 0.000
% 70.94/9.50 % Success case prop encoding time : 0.000
% 70.94/9.50 % Success case prop solver time : 0.000
% 70.94/9.50 % Current number of processed clauses : 5397
% 70.94/9.50 % Positive orientable unit clauses : 453
% 70.94/9.50 % Positive unorientable unit clauses: 41
% 70.94/9.50 % Negative unit clauses : 729
% 70.94/9.50 % Non-unit-clauses : 4174
% 70.94/9.50 % Current number of unprocessed clauses: 175795
% 70.94/9.50 % ...number of literals in the above : 735038
% 70.94/9.50 % Current number of archived formulas : 0
% 70.94/9.50 % Current number of archived clauses : 2775
% 70.94/9.50 % Clause-clause subsumption calls (NU) : 5436882
% 70.94/9.50 % Rec. Clause-clause subsumption calls : 2517530
% 70.94/9.50 % Non-unit clause-clause subsumptions : 18074
% 70.94/9.50 % Unit Clause-clause subsumption calls : 1400678
% 70.94/9.50 % Rewrite failures with RHS unbound : 0
% 70.94/9.50 % BW rewrite match attempts : 658
% 70.94/9.50 % BW rewrite match successes : 293
% 70.94/9.50 % Condensation attempts : 30395
% 70.94/9.50 % Condensation successes : 2119
% 70.94/9.50 % Termbank termtop insertions : 2854196
% 70.94/9.50 % Search garbage collected termcells : 16522
% 70.94/9.50
% 70.94/9.50 % -------------------------------------------------
% 70.94/9.50 % User time : 8.666 s
% 70.94/9.50 % System time : 0.159 s
% 70.94/9.50 % Total time : 8.825 s
% 70.94/9.50 % Maximum resident set size: 8896 pages
% 70.94/9.50
% 70.94/9.50 % -------------------------------------------------
% 70.94/9.50 % User time : 34.154 s
% 70.94/9.50 % System time : 1.043 s
% 70.94/9.50 % Total time : 35.197 s
% 70.94/9.50 % Maximum resident set size: 5632 pages
% 70.94/9.50 % E exiting
%------------------------------------------------------------------------------