%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : COM273_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 : n012.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:12:42 PM UTC 2026
% Result : Theorem 4.44s 6.52s
% Output : CNFRefutation 4.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 34
% Syntax : Number of formulae : 174 ( 98 unt; 0 typ; 0 def)
% Number of atoms : 304 ( 253 equ)
% Maximal formula atoms : 24 ( 1 avg)
% Number of connectives : 212 ( 82 ~; 94 |; 19 &)
% ( 0 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 12 ( 11 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 37 ( 37 usr; 13 con; 0-2 aty)
% Number of variables : 200 ( 0 sgn 195 !; 5 ?; 200 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
vAnsMap: $tType ).
tff(decl_sort2,type,
vAval: $tType ).
tff(decl_sort3,type,
vExp: $tType ).
tff(decl_sort4,type,
vAType: $tType ).
tff(decl_sort5,type,
vOptExp: $tType ).
tff(decl_sort6,type,
vUnOpT: $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,
vATMap: $tType ).
tff(decl_23,type,
vconstant: vAval > vExp ).
tff(decl_27,type,
vsomeExp: vExp > vOptExp ).
tff(decl_31,type,
vnotop: vUnOpT ).
tff(decl_32,type,
vNum: vnat > vAval ).
tff(decl_33,type,
vnoAType: vOptAType ).
tff(decl_34,type,
vyes: vYN ).
tff(decl_35,type,
ve1: vExp ).
tff(decl_36,type,
vT: vstring > vAval ).
tff(decl_37,type,
vNumber: vAType ).
tff(decl_43,type,
vYesNo: vAType ).
tff(decl_45,type,
vunop: ( vExp * vUnOpT ) > vExp ).
tff(decl_54,type,
vnoExp: vOptExp ).
tff(decl_56,type,
vB: vYN > vAval ).
tff(decl_61,type,
vText: vAType ).
tff(decl_75,type,
vsomeAType: vAType > vOptAType ).
tff(decl_79,type,
vno: vYN ).
tff(decl_82,type,
vecheck: ( vExp * vATMap ) > vOptAType ).
tff(decl_87,type,
vtypeOf: vAval > vAType ).
tff(decl_92,type,
vexpIsValue: vExp > $o ).
tff(decl_95,type,
vtypeAM: vAnsMap > vATMap ).
tff(decl_102,type,
visSomeAType: vOptAType > $o ).
tff(decl_111,type,
vevalUnOp: ( vAval * vUnOpT ) > vOptExp ).
tff(decl_113,type,
vnot: vYN > vYN ).
tff(decl_117,type,
vcheckUnOp: ( vAType * vUnOpT ) > vOptAType ).
tff(decl_119,type,
visSomeExp: vOptExp > $o ).
tff(decl_127,type,
vreduceExp: ( vAnsMap * vExp ) > vOptExp ).
tff(decl_136,type,
vgetAType: vOptAType > vAType ).
tff(decl_139,type,
vgetExpValue: vExp > vAval ).
tff(decl_141,type,
vgetExp: vOptExp > vExp ).
tff(decl_197,type,
esk34_1: vOptAType > vAType ).
tff(decl_247,type,
esk84_1: vOptAType > vAType ).
tff(decl_248,type,
esk85_1: vAval > vYN ).
tff(decl_249,type,
esk86_1: vAval > vnat ).
tff(decl_250,type,
esk87_1: vAval > vstring ).
tff(decl_299,type,
esk136_1: vExp > vAval ).
tff(decl_314,type,
esk151_2: ( vAval * vUnOpT ) > vYN ).
tff(decl_400,type,
esk237_0: vAnsMap ).
tff(decl_401,type,
esk238_0: vUnOpT ).
tff(decl_402,type,
esk239_0: vAType ).
tff(decl_403,type,
esk240_0: vExp ).
tff('DIFF-noAType-someAType',axiom,
! [X4: vAType] : ( vnoAType != vsomeAType(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','DIFF-noAType-someAType') ).
tff('EQ-someAType',axiom,
! [X4: vAType,X8: vAType] :
( ( vsomeAType(X4) = vsomeAType(X8) )
=> ( X4 = X8 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','EQ-someAType') ).
tff('dom-OptAType',axiom,
! [X46: vOptAType] :
( ? [X4: vAType] : ( X46 = vsomeAType(X4) )
| ( X46 = vnoAType ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','dom-OptAType') ).
tff('reduceExpPreservation-unop-expIsValue-True',conjecture,
! [X126: vAnsMap,X501: vUnOpT,X73: vAType,X500: vExp] :
( ( ( vreduceExp(vunop(X501,ve1),X126) = vsomeExp(X500) )
& ( vecheck(vtypeAM(X126),vunop(X501,ve1)) = vsomeAType(X73) )
& vexpIsValue(ve1) )
=> ( vecheck(vtypeAM(X126),X500) = vsomeAType(X73) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','reduceExpPreservation-unop-expIsValue-True') ).
tff('dom-UnOpT',axiom,
! [X52: vUnOpT] : ( X52 = vnotop ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','dom-UnOpT') ).
tff('isSomeAType-true-INV',axiom,
! [X103: vOptAType] :
( visSomeAType(X103)
=> ? [X104: vAType] : ( X103 = vsomeAType(X104) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','isSomeAType-true-INV') ).
tff('isSomeAType-1',axiom,
! [X102: vAType] : visSomeAType(vsomeAType(X102)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','isSomeAType-1') ).
tff('echeck-7',axiom,
! [X355: vATMap,X75: vExp,X397: vUnOpT] :
( ~ visSomeAType(vecheck(X355,X75))
=> ( vecheck(X355,vunop(X397,X75)) = vnoAType ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','echeck-7') ).
tff('isSomeAType-0',axiom,
~ visSomeAType(vnoAType),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','isSomeAType-0') ).
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('getAType-0',axiom,
! [X70: vAType] : ( vgetAType(vsomeAType(X70)) = X70 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','getAType-0') ).
tff('dom-AType',axiom,
! [X19: vAType] :
( ( X19 = vText )
| ( X19 = vNumber )
| ( X19 = vYesNo ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','dom-AType') ).
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('expIsValue-1',axiom,
! [X75: vExp] :
( ! [X174: vAval] : ( X75 != vconstant(X174) )
=> ~ vexpIsValue(X75) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','expIsValue-1') ).
tff('DIFF-noExp-someExp',axiom,
! [X5: vExp] : ( vnoExp != vsomeExp(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','DIFF-noExp-someExp') ).
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('getExpValue-0',axiom,
! [X76: vAval] : ( vgetExpValue(vconstant(X76)) = X76 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','getExpValue-0') ).
tff('DIFF-YesNo-Number',axiom,
vYesNo != vNumber,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','DIFF-YesNo-Number') ).
tff('isSomeExp-false-INV',axiom,
! [X171: vOptExp] :
( ~ visSomeExp(X171)
=> ( X171 = vnoExp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','isSomeExp-false-INV') ).
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-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('typeOf-0',axiom,
! [X78: vYN] : ( vtypeOf(vB(X78)) = vYesNo ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','typeOf-0') ).
tff('getExp-0',axiom,
! [X75: vExp] : ( vgetExp(vsomeExp(X75)) = X75 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','getExp-0') ).
tff('checkUnOp-1',axiom,
! [X387: vUnOpT,X388: vAType] :
( ( ( X388 != vYesNo )
| ( X387 != vnotop ) )
=> ( vcheckUnOp(X387,X388) = vnoAType ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','checkUnOp-1') ).
tff('echeck-6',axiom,
! [X355: vATMap,X75: vExp,X396: vUnOpT] :
( visSomeAType(vecheck(X355,X75))
=> ( vecheck(X355,vunop(X396,X75)) = vcheckUnOp(X396,vgetAType(vecheck(X355,X75))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','echeck-6') ).
tff('reduceExp-8',axiom,
! [X228: vExp,X231: vUnOpT,X126: vAnsMap] :
( vexpIsValue(X228)
=> ( vreduceExp(vunop(X231,X228),X126) = vevalUnOp(X231,vgetExpValue(X228)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','reduceExp-8') ).
tff('reduceExp-0',axiom,
! [X76: vAval,X227: vAnsMap] : ( vreduceExp(vconstant(X76),X227) = vnoExp ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','reduceExp-0') ).
tff('isSomeExp-0',axiom,
~ visSomeExp(vnoExp),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','isSomeExp-0') ).
tff('checkUnOp-0',axiom,
vcheckUnOp(vnotop,vYesNo) = vsomeAType(vYesNo),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','checkUnOp-0') ).
tff('dom-YN',axiom,
! [X10: vYN] :
( ( X10 = vno )
| ( X10 = vyes ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','dom-YN') ).
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('not-1',axiom,
vnot(vno) = vyes,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','not-1') ).
tff('not-0',axiom,
vnot(vyes) = vno,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','not-0') ).
tff(c_0_34,plain,
! [X4: vAType] : ( vnoAType != vsomeAType(X4) ),
inference(fof_simplification,[status(thm)],['DIFF-noAType-someAType']) ).
tff(c_0_35,plain,
! [X708: vAType,X709: vAType] :
( ( X708 = X709 )
| ( vsomeAType(X708) != vsomeAType(X709) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['EQ-someAType'])])]) ).
tff(c_0_36,plain,
! [X706: vOptAType] :
( ( X706 = vsomeAType(esk34_1(X706)) )
| ( X706 = vnoAType ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['dom-OptAType'])]) ).
tff(c_0_37,plain,
! [X710: vAType] : ( vnoAType != vsomeAType(X710) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_34])]) ).
tff(c_0_38,negated_conjecture,
~ ! [X126: vAnsMap,X501: vUnOpT,X73: vAType,X500: vExp] :
( ( ( vreduceExp(vunop(X501,ve1),X126) = vsomeExp(X500) )
& ( vecheck(vtypeAM(X126),vunop(X501,ve1)) = vsomeAType(X73) )
& vexpIsValue(ve1) )
=> ( vecheck(vtypeAM(X126),X500) = vsomeAType(X73) ) ),
inference(assume_negation,[status(cth)],['reduceExpPreservation-unop-expIsValue-True']) ).
tff(c_0_39,plain,
! [X727: vUnOpT] : ( X727 = vnotop ),
inference(variable_rename,[status(thm)],['dom-UnOpT']) ).
tcf(c_0_40,plain,
! [X4: vAType,X8: vAType] :
( ( vsomeAType(X4) != vsomeAType(X8) )
| ( X4 = X8 ) ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
tcf(c_0_41,plain,
! [X46: vOptAType] :
( ( X46 = vsomeAType(esk34_1(X46)) )
| ( X46 = vnoAType ) ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
tcf(c_0_42,plain,
! [X4: vAType] : vnoAType != vsomeAType(X4),
inference(split_conjunct,[status(thm)],[c_0_37]) ).
tff(c_0_43,plain,
! [X907: vOptAType] :
( ( X907 = vsomeAType(esk84_1(X907)) )
| ~ visSomeAType(X907) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['isSomeAType-true-INV'])])])]) ).
tff(c_0_44,plain,
! [X906: vAType] : visSomeAType(vsomeAType(X906)),
inference(variable_rename,[status(thm)],['isSomeAType-1']) ).
tff(c_0_45,negated_conjecture,
( ( vecheck(vtypeAM(esk237_0),esk240_0) != vsomeAType(esk239_0) )
& ( vreduceExp(vunop(esk238_0,ve1),esk237_0) = vsomeExp(esk240_0) )
& ( vecheck(vtypeAM(esk237_0),vunop(esk238_0,ve1)) = vsomeAType(esk239_0) )
& vexpIsValue(ve1) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_38])])])]) ).
tcf(c_0_46,plain,
! [X23: vUnOpT] : X23 = vnotop,
inference(split_conjunct,[status(thm)],[c_0_39]) ).
tcf(c_0_47,plain,
! [X4: vAType] : esk34_1(vsomeAType(X4)) = X4,
inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_40,c_0_41])]),c_0_42]) ).
tcf(c_0_48,plain,
! [X46: vOptAType] :
( ~ visSomeAType(X46)
| ( X46 = vsomeAType(esk84_1(X46)) ) ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
tcf(c_0_49,plain,
! [X4: vAType] : visSomeAType(vsomeAType(X4)),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
tcf(c_0_50,negated_conjecture,
vecheck(vtypeAM(esk237_0),vunop(esk238_0,ve1)) = vsomeAType(esk239_0),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
tcf(c_0_51,plain,
! [X23: vUnOpT,X28: vUnOpT] : X23 = X28,
inference(spm,[status(thm)],[c_0_46,c_0_46]) ).
tff(c_0_52,plain,
! [X355: vATMap,X75: vExp,X397: vUnOpT] :
( ~ visSomeAType(vecheck(X355,X75))
=> ( vecheck(X355,vunop(X397,X75)) = vnoAType ) ),
inference(fof_simplification,[status(thm)],['echeck-7']) ).
tff(c_0_53,plain,
~ visSomeAType(vnoAType),
inference(fof_simplification,[status(thm)],['isSomeAType-0']) ).
tff(c_0_54,plain,
! [X1334: vATMap,X1335: vYN] : ( vecheck(X1334,vconstant(vB(X1335))) = vsomeAType(vYesNo) ),
inference(variable_rename,[status(thm)],['echeck-0']) ).
tff(c_0_55,plain,
vYesNo != vText,
inference(fof_simplification,[status(thm)],['DIFF-YesNo-Text']) ).
tff(c_0_56,plain,
! [X818: vAType] : ( vgetAType(vsomeAType(X818)) = X818 ),
inference(variable_rename,[status(thm)],['getAType-0']) ).
tcf(c_0_57,plain,
! [X46: vOptAType] :
( ~ visSomeAType(X46)
| ( esk84_1(X46) = esk34_1(X46) ) ),
inference(spm,[status(thm)],[c_0_47,c_0_48]) ).
tff(c_0_58,plain,
! [X592: vAType] :
( ( X592 = vText )
| ( X592 = vNumber )
| ( X592 = vYesNo ) ),
inference(variable_rename,[status(thm)],['dom-AType']) ).
tcf(c_0_59,negated_conjecture,
visSomeAType(vecheck(vtypeAM(esk237_0),vunop(vnotop,ve1))),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49,c_0_50]),c_0_51]) ).
tff(c_0_60,plain,
! [X1353: vATMap,X1354: vExp,X1355: vUnOpT] :
( ( vecheck(X1353,vunop(X1355,X1354)) = vnoAType )
| visSomeAType(vecheck(X1353,X1354)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_52])]) ).
tff(c_0_61,plain,
~ visSomeAType(vnoAType),
inference(fof_nnf,[status(thm)],[c_0_53]) ).
tcf(c_0_62,plain,
! [X15: vATMap,X10: vYN] : vecheck(X15,vconstant(vB(X10))) = vsomeAType(vYesNo),
inference(split_conjunct,[status(thm)],[c_0_54]) ).
tff(c_0_63,plain,
! [X1338: vATMap,X1339: vstring] : ( vecheck(X1338,vconstant(vT(X1339))) = vsomeAType(vText) ),
inference(variable_rename,[status(thm)],['echeck-2']) ).
tff(c_0_64,plain,
vYesNo != vText,
inference(fof_nnf,[status(thm)],[c_0_55]) ).
tff(c_0_65,plain,
! [X75: vExp] :
( ! [X174: vAval] : ( X75 != vconstant(X174) )
=> ~ vexpIsValue(X75) ),
inference(fof_simplification,[status(thm)],['expIsValue-1']) ).
tcf(c_0_66,plain,
! [X4: vAType] : vgetAType(vsomeAType(X4)) = X4,
inference(split_conjunct,[status(thm)],[c_0_56]) ).
tcf(c_0_67,plain,
! [X46: vOptAType] :
( ~ visSomeAType(X46)
| ( vsomeAType(esk34_1(X46)) = X46 ) ),
inference(spm,[status(thm)],[c_0_48,c_0_57]) ).
tcf(c_0_68,plain,
! [X4: vAType] :
( ( X4 = vText )
| ( X4 = vNumber )
| ( X4 = vYesNo ) ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
tcf(c_0_69,negated_conjecture,
! [X23: vUnOpT] : visSomeAType(vecheck(vtypeAM(esk237_0),vunop(X23,ve1))),
inference(spm,[status(thm)],[c_0_59,c_0_51]) ).
tcf(c_0_70,plain,
! [X23: vUnOpT,X15: vATMap,X5: vExp] :
( ( vecheck(X15,vunop(X23,X5)) = vnoAType )
| visSomeAType(vecheck(X15,X5)) ),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
tcf(c_0_71,plain,
~ visSomeAType(vnoAType),
inference(split_conjunct,[status(thm)],[c_0_61]) ).
tff(c_0_72,plain,
! [X5: vExp] : ( vnoExp != vsomeExp(X5) ),
inference(fof_simplification,[status(thm)],['DIFF-noExp-someExp']) ).
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_40,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,
! [X221: vUnOpT,X222: vAval] :
( ( ! [X223: vYN] : ( X222 != vB(X223) )
| ( X221 != vnotop ) )
=> ( vevalUnOp(X221,X222) = vnoExp ) ),
inference(fof_simplification,[status(thm)],['evalUnOp-1']) ).
tff(c_0_77,plain,
! [X830: vAval] : ( vgetExpValue(vconstant(X830)) = X830 ),
inference(variable_rename,[status(thm)],['getExpValue-0']) ).
tff(c_0_78,plain,
! [X1033: vExp] :
( ~ vexpIsValue(X1033)
| ( X1033 = vconstant(esk136_1(X1033)) ) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_65])])])]) ).
tcf(c_0_79,plain,
! [X46: vOptAType] :
( ~ visSomeAType(X46)
| ( esk34_1(X46) = vgetAType(X46) ) ),
inference(spm,[status(thm)],[c_0_66,c_0_67]) ).
tcf(c_0_80,plain,
! [X46: vOptAType] :
( ~ visSomeAType(X46)
| ( vsomeAType(vText) = X46 )
| ( esk84_1(X46) = vNumber )
| ( esk84_1(X46) = vYesNo ) ),
inference(spm,[status(thm)],[c_0_48,c_0_68]) ).
tcf(c_0_81,negated_conjecture,
visSomeAType(vecheck(vtypeAM(esk237_0),ve1)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_70]),c_0_71]) ).
tff(c_0_82,plain,
! [X732: vExp] : ( vnoExp != vsomeExp(X732) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_72])]) ).
tff(c_0_83,plain,
vYesNo != vNumber,
inference(fof_simplification,[status(thm)],['DIFF-YesNo-Number']) ).
tcf(c_0_84,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_85,plain,
! [X1099: vUnOpT,X1100: vAval] :
( ( ( vevalUnOp(X1099,X1100) = vnoExp )
| ( X1100 = vB(esk151_2(X1099,X1100)) ) )
& ( ( vevalUnOp(X1099,X1100) = vnoExp )
| ( X1099 = vnotop ) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_76])])])]) ).
tcf(c_0_86,plain,
! [X21: vAval] : vgetExpValue(vconstant(X21)) = X21,
inference(split_conjunct,[status(thm)],[c_0_77]) ).
tcf(c_0_87,plain,
! [X5: vExp] :
( ~ vexpIsValue(X5)
| ( X5 = vconstant(esk136_1(X5)) ) ),
inference(split_conjunct,[status(thm)],[c_0_78]) ).
tcf(c_0_88,plain,
! [X4: vAType] : esk84_1(vsomeAType(X4)) = X4,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_40,c_0_48])]),c_0_49])]) ).
tcf(c_0_89,plain,
! [X46: vOptAType] :
( ~ visSomeAType(X46)
| ( vsomeAType(vgetAType(X46)) = X46 ) ),
inference(spm,[status(thm)],[c_0_67,c_0_79]) ).
tcf(c_0_90,negated_conjecture,
( ( esk84_1(vecheck(vtypeAM(esk237_0),ve1)) = vYesNo )
| ( esk84_1(vecheck(vtypeAM(esk237_0),ve1)) = vNumber )
| ( vecheck(vtypeAM(esk237_0),ve1) = vsomeAType(vText) ) ),
inference(spm,[status(thm)],[c_0_80,c_0_81]) ).
tcf(c_0_91,plain,
! [X5: vExp] : vnoExp != vsomeExp(X5),
inference(split_conjunct,[status(thm)],[c_0_82]) ).
tcf(c_0_92,negated_conjecture,
vreduceExp(vunop(esk238_0,ve1),esk237_0) = vsomeExp(esk240_0),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
tff(c_0_93,plain,
! [X171: vOptExp] :
( ~ visSomeExp(X171)
=> ( X171 = vnoExp ) ),
inference(fof_simplification,[status(thm)],['isSomeExp-false-INV']) ).
tff(c_0_94,plain,
! [X715: vYN,X716: vYN] :
( ( X715 = X716 )
| ( vB(X715) != vB(X716) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['EQ-B'])])]) ).
tff(c_0_95,plain,
! [X913: vAval] :
( ( ( vtypeOf(X913) = vYesNo )
| ( vtypeOf(X913) = vNumber )
| ( vtypeOf(X913) = vText ) )
& ( ( vtypeOf(X913) = vYesNo )
| ( vtypeOf(X913) = vNumber )
| ( X913 = vT(esk87_1(X913)) ) )
& ( ( vtypeOf(X913) = vYesNo )
| ( X913 = vNum(esk86_1(X913)) )
| ( vtypeOf(X913) = vText ) )
& ( ( vtypeOf(X913) = vYesNo )
| ( X913 = vNum(esk86_1(X913)) )
| ( X913 = vT(esk87_1(X913)) ) )
& ( ( X913 = vB(esk85_1(X913)) )
| ( vtypeOf(X913) = vNumber )
| ( vtypeOf(X913) = vText ) )
& ( ( X913 = vB(esk85_1(X913)) )
| ( vtypeOf(X913) = vNumber )
| ( X913 = vT(esk87_1(X913)) ) )
& ( ( X913 = vB(esk85_1(X913)) )
| ( X913 = vNum(esk86_1(X913)) )
| ( vtypeOf(X913) = vText ) )
& ( ( X913 = vB(esk85_1(X913)) )
| ( X913 = vNum(esk86_1(X913)) )
| ( X913 = vT(esk87_1(X913)) ) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],['typeOf-INV'])])])]) ).
tff(c_0_96,plain,
! [X910: vYN] : ( vtypeOf(vB(X910)) = vYesNo ),
inference(variable_rename,[status(thm)],['typeOf-0']) ).
tff(c_0_97,plain,
vYesNo != vNumber,
inference(fof_nnf,[status(thm)],[c_0_83]) ).
tff(c_0_98,plain,
! [X829: vExp] : ( vgetExp(vsomeExp(X829)) = X829 ),
inference(variable_rename,[status(thm)],['getExp-0']) ).
tcf(c_0_99,plain,
! [X15: vATMap,X10: vYN] : vecheck(X15,vconstant(vB(X10))) != vsomeAType(vText),
inference(spm,[status(thm)],[c_0_84,c_0_74]) ).
tcf(c_0_100,plain,
! [X23: vUnOpT,X21: vAval] :
( ( vevalUnOp(X23,X21) = vnoExp )
| ( X21 = vB(esk151_2(X23,X21)) ) ),
inference(split_conjunct,[status(thm)],[c_0_85]) ).
tcf(c_0_101,plain,
! [X5: vExp] :
( ~ vexpIsValue(X5)
| ( esk136_1(X5) = vgetExpValue(X5) ) ),
inference(spm,[status(thm)],[c_0_86,c_0_87]) ).
tff(c_0_102,plain,
! [X387: vUnOpT,X388: vAType] :
( ( ( X388 != vYesNo )
| ( X387 != vnotop ) )
=> ( vcheckUnOp(X387,X388) = vnoAType ) ),
inference(fof_simplification,[status(thm)],['checkUnOp-1']) ).
tff(c_0_103,plain,
! [X1350: vATMap,X1351: vExp,X1352: vUnOpT] :
( ( vecheck(X1350,vunop(X1352,X1351)) = vcheckUnOp(X1352,vgetAType(vecheck(X1350,X1351))) )
| ~ visSomeAType(vecheck(X1350,X1351)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['echeck-6'])])]) ).
tcf(c_0_104,plain,
! [X46: vOptAType] :
( ~ visSomeAType(X46)
| ( esk84_1(X46) = vgetAType(X46) ) ),
inference(spm,[status(thm)],[c_0_88,c_0_89]) ).
tcf(c_0_105,negated_conjecture,
( ( vecheck(vtypeAM(esk237_0),ve1) = vsomeAType(vYesNo) )
| ( vecheck(vtypeAM(esk237_0),ve1) = vsomeAType(vText) )
| ( esk84_1(vecheck(vtypeAM(esk237_0),ve1)) = vNumber ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48,c_0_90]),c_0_81])]) ).
tcf(c_0_106,negated_conjecture,
vreduceExp(vunop(vnotop,ve1),esk237_0) != vnoExp,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91,c_0_92]),c_0_51]) ).
tff(c_0_107,plain,
! [X1134: vExp,X1135: vUnOpT,X1136: vAnsMap] :
( ( vreduceExp(vunop(X1135,X1134),X1136) = vevalUnOp(X1135,vgetExpValue(X1134)) )
| ~ vexpIsValue(X1134) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['reduceExp-8'])])]) ).
tff(c_0_108,plain,
! [X1031: vOptExp] :
( ( X1031 = vnoExp )
| visSomeExp(X1031) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_93])]) ).
tff(c_0_109,plain,
! [X1108: vAval,X1109: vAnsMap] : ( vreduceExp(vconstant(X1108),X1109) = vnoExp ),
inference(variable_rename,[status(thm)],['reduceExp-0']) ).
tcf(c_0_110,plain,
! [X10: vYN,X48: vYN] :
( ( vB(X10) != vB(X48) )
| ( X10 = X48 ) ),
inference(split_conjunct,[status(thm)],[c_0_94]) ).
tcf(c_0_111,plain,
! [X21: vAval] :
( ( X21 = vB(esk85_1(X21)) )
| ( vtypeOf(X21) = vNumber )
| ( vtypeOf(X21) = vText ) ),
inference(split_conjunct,[status(thm)],[c_0_95]) ).
tcf(c_0_112,plain,
! [X10: vYN] : vtypeOf(vB(X10)) = vYesNo,
inference(split_conjunct,[status(thm)],[c_0_96]) ).
tcf(c_0_113,plain,
vYesNo != vNumber,
inference(split_conjunct,[status(thm)],[c_0_97]) ).
tcf(c_0_114,negated_conjecture,
vecheck(vtypeAM(esk237_0),esk240_0) != vsomeAType(esk239_0),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
tcf(c_0_115,plain,
! [X5: vExp] : vgetExp(vsomeExp(X5)) = X5,
inference(split_conjunct,[status(thm)],[c_0_98]) ).
tcf(c_0_116,plain,
! [X15: vATMap,X23: vUnOpT,X21: vAval] :
( ( vecheck(X15,vconstant(X21)) != vsomeAType(vText) )
| ( vevalUnOp(X23,X21) = vnoExp ) ),
inference(spm,[status(thm)],[c_0_99,c_0_100]) ).
tcf(c_0_117,plain,
! [X5: vExp] :
( ~ vexpIsValue(X5)
| ( vconstant(vgetExpValue(X5)) = X5 ) ),
inference(spm,[status(thm)],[c_0_87,c_0_101]) ).
tff(c_0_118,plain,
! [X1328: vUnOpT,X1329: vAType] :
( ( ( vcheckUnOp(X1328,X1329) = vnoAType )
| ( X1329 = vYesNo ) )
& ( ( vcheckUnOp(X1328,X1329) = vnoAType )
| ( X1328 = vnotop ) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_102])])]) ).
tcf(c_0_119,plain,
! [X23: vUnOpT,X15: vATMap,X5: vExp] :
( ~ visSomeAType(vecheck(X15,X5))
| ( vecheck(X15,vunop(X23,X5)) = vcheckUnOp(X23,vgetAType(vecheck(X15,X5))) ) ),
inference(split_conjunct,[status(thm)],[c_0_103]) ).
tcf(c_0_120,negated_conjecture,
( ( vgetAType(vecheck(vtypeAM(esk237_0),ve1)) = vNumber )
| ( vecheck(vtypeAM(esk237_0),ve1) = vsomeAType(vText) )
| ( vecheck(vtypeAM(esk237_0),ve1) = vsomeAType(vYesNo) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_104,c_0_105]),c_0_81])]) ).
tcf(c_0_121,negated_conjecture,
vecheck(vtypeAM(esk237_0),vunop(vnotop,ve1)) != vnoAType,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42,c_0_50]),c_0_51]) ).
tcf(c_0_122,negated_conjecture,
! [X23: vUnOpT] : vreduceExp(vunop(X23,ve1),esk237_0) != vnoExp,
inference(spm,[status(thm)],[c_0_106,c_0_51]) ).
tcf(c_0_123,plain,
! [X55: vAnsMap,X23: vUnOpT,X5: vExp] :
( ~ vexpIsValue(X5)
| ( vreduceExp(vunop(X23,X5),X55) = vevalUnOp(X23,vgetExpValue(X5)) ) ),
inference(split_conjunct,[status(thm)],[c_0_107]) ).
tcf(c_0_124,negated_conjecture,
vexpIsValue(ve1),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
tcf(c_0_125,plain,
! [X53: vOptExp] :
( ( X53 = vnoExp )
| visSomeExp(X53) ),
inference(split_conjunct,[status(thm)],[c_0_108]) ).
tcf(c_0_126,plain,
! [X21: vAval,X55: vAnsMap] : vreduceExp(vconstant(X21),X55) = vnoExp,
inference(split_conjunct,[status(thm)],[c_0_109]) ).
tcf(c_0_127,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_110,c_0_111])]),c_0_112]),c_0_112]),c_0_113]),c_0_75]) ).
tff(c_0_128,plain,
~ visSomeExp(vnoExp),
inference(fof_simplification,[status(thm)],['isSomeExp-0']) ).
tcf(c_0_129,negated_conjecture,
vecheck(vtypeAM(esk237_0),esk240_0) != vecheck(vtypeAM(esk237_0),vunop(esk238_0,ve1)),
inference(rw,[status(thm)],[c_0_114,c_0_50]) ).
tcf(c_0_130,negated_conjecture,
esk240_0 = vgetExp(vreduceExp(vunop(vnotop,ve1),esk237_0)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_115,c_0_92]),c_0_51]) ).
tcf(c_0_131,negated_conjecture,
( ( vgetAType(vecheck(vtypeAM(esk237_0),ve1)) = vYesNo )
| ( vecheck(vtypeAM(esk237_0),ve1) = vsomeAType(vText) )
| ( esk84_1(vecheck(vtypeAM(esk237_0),ve1)) = vNumber ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_104,c_0_90]),c_0_81])]) ).
tcf(c_0_132,plain,
vcheckUnOp(vnotop,vYesNo) = vsomeAType(vYesNo),
inference(split_conjunct,[status(thm)],['checkUnOp-0']) ).
tcf(c_0_133,plain,
! [X23: vUnOpT,X15: vATMap,X5: vExp] :
( ~ vexpIsValue(X5)
| ( vecheck(X15,X5) != vsomeAType(vText) )
| ( vevalUnOp(X23,vgetExpValue(X5)) = vnoExp ) ),
inference(spm,[status(thm)],[c_0_116,c_0_117]) ).
tcf(c_0_134,plain,
! [X23: vUnOpT,X4: vAType] :
( ( vcheckUnOp(X23,X4) = vnoAType )
| ( X4 = vYesNo ) ),
inference(split_conjunct,[status(thm)],[c_0_118]) ).
tcf(c_0_135,negated_conjecture,
! [X23: vUnOpT] :
( ( vecheck(vtypeAM(esk237_0),ve1) = vsomeAType(vYesNo) )
| ( vecheck(vtypeAM(esk237_0),ve1) = vsomeAType(vText) )
| ( vcheckUnOp(X23,vNumber) = vecheck(vtypeAM(esk237_0),vunop(X23,ve1)) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_119,c_0_120]),c_0_81])]) ).
tcf(c_0_136,negated_conjecture,
! [X23: vUnOpT] : vecheck(vtypeAM(esk237_0),vunop(X23,ve1)) != vnoAType,
inference(spm,[status(thm)],[c_0_121,c_0_51]) ).
tcf(c_0_137,negated_conjecture,
! [X23: vUnOpT] : vevalUnOp(X23,vgetExpValue(ve1)) != vnoExp,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_122,c_0_123]),c_0_124])]) ).
tcf(c_0_138,plain,
! [X21: vAval,X55: vAnsMap,X53: vOptExp] :
( visSomeExp(X53)
| ( X53 = vreduceExp(vconstant(X21),X55) ) ),
inference(spm,[status(thm)],[c_0_125,c_0_126]) ).
tcf(c_0_139,plain,
! [X23: vUnOpT,X21: vAval] :
( ( vevalUnOp(X23,X21) = vnoExp )
| ( esk151_2(X23,X21) = esk85_1(X21) ) ),
inference(spm,[status(thm)],[c_0_127,c_0_100]) ).
tff(c_0_140,plain,
~ visSomeExp(vnoExp),
inference(fof_nnf,[status(thm)],[c_0_128]) ).
tcf(c_0_141,negated_conjecture,
vecheck(vtypeAM(esk237_0),vgetExp(vreduceExp(vunop(vnotop,ve1),esk237_0))) != vecheck(vtypeAM(esk237_0),vunop(vnotop,ve1)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_129,c_0_130]),c_0_51]) ).
tcf(c_0_142,negated_conjecture,
( ( vgetAType(vecheck(vtypeAM(esk237_0),ve1)) = vNumber )
| ( vecheck(vtypeAM(esk237_0),ve1) = vsomeAType(vText) )
| ( vgetAType(vecheck(vtypeAM(esk237_0),ve1)) = vYesNo ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_104,c_0_131]),c_0_81])]) ).
tcf(c_0_143,plain,
! [X23: vUnOpT] : vcheckUnOp(X23,vYesNo) = vsomeAType(vYesNo),
inference(spm,[status(thm)],[c_0_132,c_0_51]) ).
tcf(c_0_144,negated_conjecture,
! [X23: vUnOpT,X15: vATMap] :
( ( vecheck(X15,ve1) != vsomeAType(vText) )
| ( vevalUnOp(X23,vgetExpValue(ve1)) = vnoExp ) ),
inference(spm,[status(thm)],[c_0_133,c_0_124]) ).
tcf(c_0_145,negated_conjecture,
( ( vecheck(vtypeAM(esk237_0),ve1) = vsomeAType(vText) )
| ( vecheck(vtypeAM(esk237_0),ve1) = vsomeAType(vYesNo) ) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_134,c_0_135]),c_0_136]),c_0_113]) ).
tcf(c_0_146,plain,
! [X15: vATMap,X49: vstring] : vecheck(X15,vconstant(vT(X49))) != vsomeAType(vYesNo),
inference(spm,[status(thm)],[c_0_84,c_0_62]) ).
tcf(c_0_147,negated_conjecture,
! [X23: vUnOpT] : visSomeExp(vevalUnOp(X23,vgetExpValue(ve1))),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_137,c_0_138]),c_0_126]) ).
tcf(c_0_148,plain,
! [X23: vUnOpT,X21: vAval] :
( ( vB(esk85_1(X21)) = X21 )
| ( vevalUnOp(X23,X21) = vnoExp ) ),
inference(spm,[status(thm)],[c_0_100,c_0_139]) ).
tcf(c_0_149,plain,
~ visSomeExp(vnoExp),
inference(split_conjunct,[status(thm)],[c_0_140]) ).
tff(c_0_150,plain,
! [X564: vYN] :
( ( X564 = vno )
| ( X564 = vyes ) ),
inference(variable_rename,[status(thm)],['dom-YN']) ).
tff(c_0_151,plain,
! [X1098: vYN] : ( vevalUnOp(vnotop,vB(X1098)) = vsomeExp(vconstant(vB(vnot(X1098)))) ),
inference(variable_rename,[status(thm)],['evalUnOp-0']) ).
tcf(c_0_152,negated_conjecture,
! [X23: vUnOpT] : vecheck(vtypeAM(esk237_0),vgetExp(vreduceExp(vunop(X23,ve1),esk237_0))) != vecheck(vtypeAM(esk237_0),vunop(X23,ve1)),
inference(spm,[status(thm)],[c_0_141,c_0_51]) ).
tcf(c_0_153,negated_conjecture,
! [X23: vUnOpT] :
( ( vecheck(vtypeAM(esk237_0),ve1) = vsomeAType(vText) )
| ( vgetAType(vecheck(vtypeAM(esk237_0),ve1)) = vNumber )
| ( vecheck(vtypeAM(esk237_0),vunop(X23,ve1)) = vsomeAType(vYesNo) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_119,c_0_142]),c_0_143]),c_0_81])]) ).
tcf(c_0_154,negated_conjecture,
vecheck(vtypeAM(esk237_0),ve1) = vsomeAType(vYesNo),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_144,c_0_145]),c_0_137]) ).
tcf(c_0_155,plain,
vsomeAType(vText) != vsomeAType(vYesNo),
inference(spm,[status(thm)],[c_0_146,c_0_74]) ).
tcf(c_0_156,negated_conjecture,
vB(esk85_1(vgetExpValue(ve1))) = vgetExpValue(ve1),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_147,c_0_148]),c_0_149]) ).
tcf(c_0_157,plain,
! [X10: vYN] :
( ( X10 = vno )
| ( X10 = vyes ) ),
inference(split_conjunct,[status(thm)],[c_0_150]) ).
tcf(c_0_158,plain,
! [X23: vUnOpT,X21: vAval] :
( ( vtypeOf(X21) = vYesNo )
| ( vevalUnOp(X23,X21) = vnoExp ) ),
inference(spm,[status(thm)],[c_0_112,c_0_100]) ).
tcf(c_0_159,plain,
! [X10: vYN] : vevalUnOp(vnotop,vB(X10)) = vsomeExp(vconstant(vB(vnot(X10)))),
inference(split_conjunct,[status(thm)],[c_0_151]) ).
tcf(c_0_160,plain,
vnot(vno) = vyes,
inference(split_conjunct,[status(thm)],['not-1']) ).
tcf(c_0_161,negated_conjecture,
! [X23: vUnOpT] : vecheck(vtypeAM(esk237_0),vgetExp(vevalUnOp(X23,vgetExpValue(ve1)))) != vecheck(vtypeAM(esk237_0),vunop(X23,ve1)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_152,c_0_123]),c_0_124])]) ).
tcf(c_0_162,negated_conjecture,
! [X23: vUnOpT] : vecheck(vtypeAM(esk237_0),vunop(X23,ve1)) = vsomeAType(vYesNo),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_153,c_0_154]),c_0_66]),c_0_154]),c_0_113]),c_0_155]) ).
tcf(c_0_163,negated_conjecture,
( ( vgetExpValue(ve1) = vB(vno) )
| ( esk85_1(vgetExpValue(ve1)) = vyes ) ),
inference(spm,[status(thm)],[c_0_156,c_0_157]) ).
tcf(c_0_164,negated_conjecture,
vtypeOf(vgetExpValue(ve1)) = vYesNo,
inference(spm,[status(thm)],[c_0_137,c_0_158]) ).
tcf(c_0_165,plain,
vevalUnOp(vnotop,vB(vno)) = vsomeExp(vconstant(vB(vyes))),
inference(spm,[status(thm)],[c_0_159,c_0_160]) ).
tcf(c_0_166,plain,
vnot(vyes) = vno,
inference(split_conjunct,[status(thm)],['not-0']) ).
tcf(c_0_167,negated_conjecture,
! [X23: vUnOpT] : vecheck(vtypeAM(esk237_0),vgetExp(vevalUnOp(X23,vgetExpValue(ve1)))) != vsomeAType(vYesNo),
inference(rw,[status(thm)],[c_0_161,c_0_162]) ).
tcf(c_0_168,negated_conjecture,
( ( vgetExpValue(ve1) = vB(vyes) )
| ( vgetExpValue(ve1) = vB(vno) ) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_111,c_0_163]),c_0_164]),c_0_164]),c_0_113]),c_0_75]) ).
tcf(c_0_169,plain,
! [X23: vUnOpT] : vevalUnOp(X23,vB(vno)) = vsomeExp(vconstant(vB(vyes))),
inference(spm,[status(thm)],[c_0_165,c_0_51]) ).
tcf(c_0_170,plain,
vevalUnOp(vnotop,vB(vyes)) = vsomeExp(vconstant(vB(vno))),
inference(spm,[status(thm)],[c_0_159,c_0_166]) ).
tcf(c_0_171,negated_conjecture,
vgetExpValue(ve1) = vB(vyes),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_167,c_0_168]),c_0_169]),c_0_115]),c_0_62]) ).
tcf(c_0_172,plain,
! [X23: vUnOpT] : vevalUnOp(X23,vB(vyes)) = vsomeExp(vconstant(vB(vno))),
inference(spm,[status(thm)],[c_0_170,c_0_51]) ).
cnf(c_0_173,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_167,c_0_171]),c_0_172]),c_0_115]),c_0_62]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : COM273_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.02 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.05/5.33 % Computer : n012.cluster.edu
% 0.05/5.33 % Model : x86_64 x86_64
% 0.05/5.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/5.33 % Memory : 8046.5625MB
% 0.05/5.33 % OS : Linux 6.8.0-71-generic
% 0.05/5.33 % CPULimit : 300
% 0.05/5.33 % WCLimit : 300
% 0.05/5.33 % DateTime : Mon Sep 21 14:22:31 UTC 2026
% 0.05/5.33 % CPUTime :
% 0.05/5.34 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.05/5.37 Running first-order theorem proving
% 0.05/5.37 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
% 4.44/6.52 % Version: 3.5.1
% 4.44/6.52 % Preprocessing class: FSLMSMSMSSSNFFN.
% 4.44/6.52 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 4.44/6.52 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 4.44/6.52 % Starting new_bool_3 with 600s (2) cores
% 4.44/6.52 % Starting new_bool_1 with 300s (1) cores
% 4.44/6.52 % Starting sh5l with 300s (1) cores
% 4.44/6.52 % G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with pid 2561365 completed with status 0
% 4.44/6.52 % Result found by G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S
% 4.44/6.52 % Preprocessing class: FSLMSMSMSSSNFFN.
% 4.44/6.52 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 4.44/6.52 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 4.44/6.52 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 4.44/6.52 % No SInE strategy applied
% 4.44/6.52 % Search class: FGUSM-SMLM32-DFFFFFNN
% 4.44/6.52 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 4.44/6.52 % Starting SubtermCWHack with 109s (1) cores
% 4.44/6.52 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 121s (1) cores
% 4.44/6.52 % Starting sh3 with 217s (1) cores
% 4.44/6.52 % Starting ho_unfolding_3 with 217s (1) cores
% 4.44/6.52 % ho_unfolding_3 with pid 2561376 completed with status 0
% 4.44/6.52 % Result found by ho_unfolding_3
% 4.44/6.52 % Preprocessing class: FSLMSMSMSSSNFFN.
% 4.44/6.52 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 4.44/6.52 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 4.44/6.52 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 4.44/6.52 % No SInE strategy applied
% 4.44/6.52 % Search class: FGUSM-SMLM32-DFFFFFNN
% 4.44/6.52 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 4.44/6.52 % Starting SubtermCWHack with 109s (1) cores
% 4.44/6.52 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 121s (1) cores
% 4.44/6.52 % Starting sh3 with 217s (1) cores
% 4.44/6.52 % Starting ho_unfolding_3 with 217s (1) cores
% 4.44/6.52 % Preprocessing time : 0.028 s
% 4.44/6.52 % Presaturation interreduction done
% 4.44/6.52
% 4.44/6.52 % Proof found!
% 4.44/6.52 % SZS status Theorem
% 4.44/6.52 % SZS output start CNFRefutation
% See solution above
% 4.44/6.52 % Parsed axioms : 508
% 4.44/6.52 % Removed by relevancy pruning/SinE : 0
% 4.44/6.52 % Initial clauses : 2529
% 4.44/6.52 % Removed in clause preprocessing : 151
% 4.44/6.52 % Initial clauses in saturation : 2378
% 4.44/6.52 % Processed clauses : 8274
% 4.44/6.52 % ...of these trivial : 338
% 4.44/6.52 % ...subsumed : 3961
% 4.44/6.52 % ...remaining for further processing : 3975
% 4.44/6.52 % Other redundant clauses eliminated : 2179
% 4.44/6.52 % Clauses deleted for lack of memory : 0
% 4.44/6.52 % Backward-subsumed : 47
% 4.44/6.52 % Backward-rewritten : 130
% 4.44/6.52 % Generated clauses : 21670
% 4.44/6.52 % ...of the previous two non-redundant : 16115
% 4.44/6.52 % ...aggressively subsumed : 0
% 4.44/6.52 % Contextual simplify-reflections : 31
% 4.44/6.52 % Paramodulations : 19286
% 4.44/6.52 % Factorizations : 93
% 4.44/6.52 % NegExts : 0
% 4.44/6.52 % Equation resolutions : 2307
% 4.44/6.52 % Disequality decompositions : 0
% 4.44/6.52 % Total rewrite steps : 6590
% 4.44/6.52 % ...of those cached : 6083
% 4.44/6.52 % Propositional unsat checks : 0
% 4.44/6.52 % Propositional check models : 0
% 4.44/6.52 % Propositional check unsatisfiable : 0
% 4.44/6.52 % Propositional clauses : 0
% 4.44/6.52 % Propositional clauses after purity: 0
% 4.44/6.52 % Propositional unsat core size : 0
% 4.44/6.52 % Propositional preprocessing time : 0.000
% 4.44/6.52 % Propositional encoding time : 0.000
% 4.44/6.52 % Propositional solver time : 0.000
% 4.44/6.52 % Success case prop preproc time : 0.000
% 4.44/6.52 % Success case prop encoding time : 0.000
% 4.44/6.52 % Success case prop solver time : 0.000
% 4.44/6.52 % Current number of processed clauses : 1683
% 4.44/6.52 % Positive orientable unit clauses : 260
% 4.44/6.52 % Positive unorientable unit clauses: 28
% 4.44/6.52 % Negative unit clauses : 306
% 4.44/6.52 % Non-unit-clauses : 1089
% 4.44/6.52 % Current number of unprocessed clauses: 11884
% 4.44/6.52 % ...number of literals in the above : 38728
% 4.44/6.52 % Current number of archived formulas : 0
% 4.44/6.52 % Current number of archived clauses : 2273
% 4.44/6.52 % Clause-clause subsumption calls (NU) : 1034680
% 4.44/6.52 % Rec. Clause-clause subsumption calls : 449846
% 4.44/6.52 % Non-unit clause-clause subsumptions : 1982
% 4.44/6.52 % Unit Clause-clause subsumption calls : 106384
% 4.44/6.52 % Rewrite failures with RHS unbound : 0
% 4.44/6.52 % BW rewrite match attempts : 330
% 4.44/6.52 % BW rewrite match successes : 126
% 4.44/6.52 % Condensation attempts : 8274
% 4.44/6.52 % Condensation successes : 58
% 4.44/6.52 % Termbank termtop insertions : 305916
% 4.44/6.52 % Search garbage collected termcells : 16399
% 4.44/6.52
% 4.44/6.52 % -------------------------------------------------
% 4.44/6.52 % User time : 1.067 s
% 4.44/6.52 % System time : 0.029 s
% 4.44/6.52 % Total time : 1.096 s
% 4.44/6.52 % Maximum resident set size: 8888 pages
% 4.44/6.52
% 4.44/6.52 % -------------------------------------------------
% 4.44/6.52 % User time : 4.051 s
% 4.44/6.52 % System time : 0.134 s
% 4.44/6.52 % Total time : 4.185 s
% 4.44/6.52 % Maximum resident set size: 5376 pages
% 4.44/6.52 % E exiting
%------------------------------------------------------------------------------