%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : COM273_1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:11:50 PM UTC 2026
% Result : Theorem 11.42s 2.38s
% Output : CNFRefutation 11.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 14
% Syntax : Number of formulae : 69 ( 41 unt; 0 typ; 0 def)
% Number of atoms : 148 ( 128 equ)
% Maximal formula atoms : 27 ( 2 avg)
% Number of connectives : 119 ( 40 ~; 40 |; 30 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 10 ( 9 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 9 con; 0-2 aty)
% Number of variables : 123 ( 0 sgn 119 !; 4 ?; 123 :)
% 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,
vOptAType: $tType ).
tff(decl_sort8,type,
vYN: $tType ).
tff(decl_sort9,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_33,type,
vnoAType: vOptAType ).
tff(decl_35,type,
ve1: vExp ).
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_75,type,
vsomeAType: vAType > vOptAType ).
tff(decl_82,type,
vecheck: ( vExp * vATMap ) > vOptAType ).
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_117,type,
vcheckUnOp: ( vAType * vUnOpT ) > vOptAType ).
tff(decl_127,type,
vreduceExp: ( vAnsMap * vExp ) > vOptExp ).
tff(decl_136,type,
vgetAType: vOptAType > vAType ).
tff(decl_139,type,
vgetExpValue: vExp > vAval ).
tff(decl_314,type,
esk151_2: ( vAval * vUnOpT ) > vYN ).
tff(decl_380,type,
esk217_2: ( vAType * vUnOpT ) > vUnOpT ).
tff(decl_381,type,
esk218_2: ( vAType * vUnOpT ) > vAType ).
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('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/sandbox2/benchmark/theBenchmark.p','reduceExpPreservation-unop-expIsValue-True') ).
tff('dom-UnOpT',axiom,
! [X52: vUnOpT] : ( X52 = vnotop ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-UnOpT') ).
tff('reduceExp-8',axiom,
! [X228: vExp,X231: vUnOpT,X126: vAnsMap] :
( vexpIsValue(X228)
=> ( vreduceExp(vunop(X231,X228),X126) = vevalUnOp(X231,vgetExpValue(X228)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-8') ).
tff('evalUnOp-1',axiom,
! [X221: vUnOpT,X222: vAval] :
( ( ! [X223: vYN] : ( X222 != vB(X223) )
| ( X221 != vnotop ) )
=> ( vevalUnOp(X221,X222) = vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalUnOp-1') ).
tff('echeck-0',axiom,
! [X391: vATMap,X392: vYN] : ( vecheck(X391,vconstant(vB(X392))) = vsomeAType(vYesNo) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-0') ).
tff('DIFF-noExp-someExp',axiom,
! [X5: vExp] : ( vnoExp != vsomeExp(X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noExp-someExp') ).
tff('echeck-7',axiom,
! [X355: vATMap,X75: vExp,X397: vUnOpT] :
( ~ visSomeAType(vecheck(X355,X75))
=> ( vecheck(X355,vunop(X397,X75)) = vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-7') ).
tff('DIFF-noAType-someAType',axiom,
! [X4: vAType] : ( vnoAType != vsomeAType(X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noAType-someAType') ).
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/sandbox2/benchmark/theBenchmark.p','echeck-6') ).
tff('getAType-0',axiom,
! [X70: vAType] : ( vgetAType(vsomeAType(X70)) = X70 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAType-0') ).
tff('checkUnOp-0',axiom,
vcheckUnOp(vnotop,vYesNo) = vsomeAType(vYesNo),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkUnOp-0') ).
tff('isSomeAType-1',axiom,
! [X102: vAType] : visSomeAType(vsomeAType(X102)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAType-1') ).
tff('checkUnOp-INV',axiom,
! [X23: vUnOpT,X4: vAType] :
( ? [X389: vUnOpT,X390: vAType] :
( ( vcheckUnOp(X23,X4) = vnoAType )
& ( X4 = X390 )
& ( X23 = X389 )
& ( ( X390 != vYesNo )
| ( X389 != vnotop ) ) )
| ( ( vcheckUnOp(X23,X4) = vsomeAType(vYesNo) )
& ( X4 = vYesNo )
& ( X23 = vnotop ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkUnOp-INV') ).
tff(evalUnOpPreservation,axiom,
! [X502: vExp,X355: vATMap,X73: vAType,X76: vAval,X501: vUnOpT] :
( ( ( vevalUnOp(X501,X76) = vsomeExp(X502) )
& ( vecheck(X355,vunop(X501,vconstant(X76))) = vsomeAType(X73) ) )
=> ( vecheck(X355,X502) = vsomeAType(X73) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',evalUnOpPreservation) ).
tff(c_0_14,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_15,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_14])])])]) ).
tff(c_0_16,plain,
! [X727: vUnOpT] : ( X727 = vnotop ),
inference(variable_rename,[status(thm)],['dom-UnOpT']) ).
tcf(c_0_17,negated_conjecture,
vreduceExp(vunop(esk238_0,ve1),esk237_0) = vsomeExp(esk240_0),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
tcf(c_0_18,plain,
! [X23: vUnOpT] : X23 = vnotop,
inference(split_conjunct,[status(thm)],[c_0_16]) ).
tff(c_0_19,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_20,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_21,negated_conjecture,
vreduceExp(vunop(vnotop,ve1),esk237_0) = vsomeExp(esk240_0),
inference(spm,[status(thm)],[c_0_17,c_0_18]) ).
tcf(c_0_22,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_19]) ).
tff(c_0_23,plain,
! [X1334: vATMap,X1335: vYN] : ( vecheck(X1334,vconstant(vB(X1335))) = vsomeAType(vYesNo) ),
inference(variable_rename,[status(thm)],['echeck-0']) ).
tff(c_0_24,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_20])])])]) ).
tcf(c_0_25,negated_conjecture,
! [X23: vUnOpT] : vreduceExp(vunop(X23,ve1),esk237_0) = vsomeExp(esk240_0),
inference(spm,[status(thm)],[c_0_21,c_0_18]) ).
tcf(c_0_26,plain,
! [X23: vUnOpT,X56: vAnsMap,X55: vAnsMap,X5: vExp] :
( ~ vexpIsValue(X5)
| ( vreduceExp(vunop(X23,X5),X55) = vreduceExp(vunop(X23,X5),X56) ) ),
inference(spm,[status(thm)],[c_0_22,c_0_22]) ).
tcf(c_0_27,negated_conjecture,
vexpIsValue(ve1),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
tff(c_0_28,plain,
! [X5: vExp] : ( vnoExp != vsomeExp(X5) ),
inference(fof_simplification,[status(thm)],['DIFF-noExp-someExp']) ).
tff(c_0_29,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_30,plain,
! [X4: vAType] : ( vnoAType != vsomeAType(X4) ),
inference(fof_simplification,[status(thm)],['DIFF-noAType-someAType']) ).
tcf(c_0_31,plain,
! [X15: vATMap,X10: vYN] : vecheck(X15,vconstant(vB(X10))) = vsomeAType(vYesNo),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
tcf(c_0_32,plain,
! [X23: vUnOpT,X21: vAval] :
( ( vevalUnOp(X23,X21) = vnoExp )
| ( X21 = vB(esk151_2(X23,X21)) ) ),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
tcf(c_0_33,negated_conjecture,
! [X23: vUnOpT,X55: vAnsMap] : vreduceExp(vunop(X23,ve1),X55) = vsomeExp(esk240_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25,c_0_26]),c_0_27])]) ).
tff(c_0_34,plain,
! [X732: vExp] : ( vnoExp != vsomeExp(X732) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_28])]) ).
tff(c_0_35,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_29])]) ).
tff(c_0_36,plain,
! [X710: vAType] : ( vnoAType != vsomeAType(X710) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_30])]) ).
tff(c_0_37,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_38,plain,
! [X15: vATMap,X23: vUnOpT,X21: vAval] :
( ( vevalUnOp(X23,X21) = vnoExp )
| ( vecheck(X15,vconstant(X21)) = vsomeAType(vYesNo) ) ),
inference(spm,[status(thm)],[c_0_31,c_0_32]) ).
tcf(c_0_39,negated_conjecture,
! [X23: vUnOpT] : vevalUnOp(X23,vgetExpValue(ve1)) = vsomeExp(esk240_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_22,c_0_33]),c_0_27])]) ).
tcf(c_0_40,plain,
! [X5: vExp] : vnoExp != vsomeExp(X5),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
tff(c_0_41,plain,
! [X818: vAType] : ( vgetAType(vsomeAType(X818)) = X818 ),
inference(variable_rename,[status(thm)],['getAType-0']) ).
tcf(c_0_42,plain,
vcheckUnOp(vnotop,vYesNo) = vsomeAType(vYesNo),
inference(split_conjunct,[status(thm)],['checkUnOp-0']) ).
tcf(c_0_43,plain,
! [X23: vUnOpT,X28: vUnOpT] : X23 = X28,
inference(spm,[status(thm)],[c_0_18,c_0_18]) ).
tff(c_0_44,plain,
! [X906: vAType] : visSomeAType(vsomeAType(X906)),
inference(variable_rename,[status(thm)],['isSomeAType-1']) ).
tff(c_0_45,plain,
! [X23: vUnOpT,X4: vAType] :
( ? [X389: vUnOpT,X390: vAType] :
( ( vcheckUnOp(X23,X4) = vnoAType )
& ( X4 = X390 )
& ( X23 = X389 )
& ( ( X390 != vYesNo )
| ( X389 != vnotop ) ) )
| ( ( vcheckUnOp(X23,X4) = vsomeAType(vYesNo) )
& ( X4 = vYesNo )
& ( X23 = vnotop ) ) ),
inference(fof_simplification,[status(thm)],['checkUnOp-INV']) ).
tcf(c_0_46,negated_conjecture,
vecheck(vtypeAM(esk237_0),vunop(esk238_0,ve1)) = vsomeAType(esk239_0),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
tcf(c_0_47,plain,
! [X23: vUnOpT,X15: vATMap,X5: vExp] :
( ( vecheck(X15,vunop(X23,X5)) = vnoAType )
| visSomeAType(vecheck(X15,X5)) ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
tcf(c_0_48,plain,
! [X4: vAType] : vnoAType != vsomeAType(X4),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
tff(c_0_49,plain,
! [X1625: vExp,X1626: vATMap,X1627: vAType,X1628: vAval,X1629: vUnOpT] :
( ( vecheck(X1626,X1625) = vsomeAType(X1627) )
| ( vevalUnOp(X1629,X1628) != vsomeExp(X1625) )
| ( vecheck(X1626,vunop(X1629,vconstant(X1628))) != vsomeAType(X1627) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[evalUnOpPreservation])])]) ).
tcf(c_0_50,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_37]) ).
tcf(c_0_51,negated_conjecture,
! [X15: vATMap] : vecheck(X15,vconstant(vgetExpValue(ve1))) = vsomeAType(vYesNo),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_38,c_0_39]),c_0_40]) ).
tcf(c_0_52,plain,
! [X4: vAType] : vgetAType(vsomeAType(X4)) = X4,
inference(split_conjunct,[status(thm)],[c_0_41]) ).
tcf(c_0_53,plain,
! [X23: vUnOpT] : vcheckUnOp(X23,vYesNo) = vsomeAType(vYesNo),
inference(spm,[status(thm)],[c_0_42,c_0_43]) ).
tcf(c_0_54,plain,
! [X4: vAType] : visSomeAType(vsomeAType(X4)),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
tff(c_0_55,plain,
! [X1330: vUnOpT,X1331: vAType] :
( ( ( vcheckUnOp(X1330,X1331) = vsomeAType(vYesNo) )
| ( vcheckUnOp(X1330,X1331) = vnoAType ) )
& ( ( vcheckUnOp(X1330,X1331) = vsomeAType(vYesNo) )
| ( X1331 = esk218_2(X1330,X1331) ) )
& ( ( vcheckUnOp(X1330,X1331) = vsomeAType(vYesNo) )
| ( X1330 = esk217_2(X1330,X1331) ) )
& ( ( vcheckUnOp(X1330,X1331) = vsomeAType(vYesNo) )
| ( esk218_2(X1330,X1331) != vYesNo )
| ( esk217_2(X1330,X1331) != vnotop ) )
& ( ( X1331 = vYesNo )
| ( vcheckUnOp(X1330,X1331) = vnoAType ) )
& ( ( X1331 = vYesNo )
| ( X1331 = esk218_2(X1330,X1331) ) )
& ( ( X1331 = vYesNo )
| ( X1330 = esk217_2(X1330,X1331) ) )
& ( ( X1331 = vYesNo )
| ( esk218_2(X1330,X1331) != vYesNo )
| ( esk217_2(X1330,X1331) != vnotop ) )
& ( ( X1330 = vnotop )
| ( vcheckUnOp(X1330,X1331) = vnoAType ) )
& ( ( X1330 = vnotop )
| ( X1331 = esk218_2(X1330,X1331) ) )
& ( ( X1330 = vnotop )
| ( X1330 = esk217_2(X1330,X1331) ) )
& ( ( X1330 = vnotop )
| ( esk218_2(X1330,X1331) != vYesNo )
| ( esk217_2(X1330,X1331) != vnotop ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[c_0_45])])])])]) ).
tcf(c_0_56,negated_conjecture,
visSomeAType(vecheck(vtypeAM(esk237_0),ve1)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_46,c_0_47]),c_0_48]) ).
tcf(c_0_57,negated_conjecture,
! [X23: vUnOpT] : vecheck(vtypeAM(esk237_0),vunop(X23,ve1)) = vsomeAType(esk239_0),
inference(spm,[status(thm)],[c_0_46,c_0_43]) ).
tcf(c_0_58,plain,
! [X4: vAType,X23: vUnOpT,X21: vAval,X15: vATMap,X5: vExp] :
( ( vevalUnOp(X23,X21) != vsomeExp(X5) )
| ( vecheck(X15,vunop(X23,vconstant(X21))) != vsomeAType(X4) )
| ( vecheck(X15,X5) = vsomeAType(X4) ) ),
inference(split_conjunct,[status(thm)],[c_0_49]) ).
tcf(c_0_59,negated_conjecture,
! [X15: vATMap,X23: vUnOpT] : vecheck(X15,vunop(X23,vconstant(vgetExpValue(ve1)))) = vsomeAType(vYesNo),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_51]),c_0_52]),c_0_53]),c_0_54])]) ).
tcf(c_0_60,plain,
! [X23: vUnOpT,X4: vAType] :
( ( vcheckUnOp(X23,X4) = vsomeAType(vYesNo) )
| ( vcheckUnOp(X23,X4) = vnoAType ) ),
inference(split_conjunct,[status(thm)],[c_0_55]) ).
tcf(c_0_61,negated_conjecture,
! [X23: vUnOpT] : vcheckUnOp(X23,vgetAType(vecheck(vtypeAM(esk237_0),ve1))) = vsomeAType(esk239_0),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_56]),c_0_57]) ).
tcf(c_0_62,negated_conjecture,
! [X4: vAType,X15: vATMap,X5: vExp] :
( ( vsomeExp(esk240_0) != vsomeExp(X5) )
| ( vsomeAType(vYesNo) != vsomeAType(X4) )
| ( vecheck(X15,X5) = vsomeAType(X4) ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_58,c_0_39]),c_0_59]) ).
tcf(c_0_63,negated_conjecture,
vecheck(vtypeAM(esk237_0),esk240_0) != vsomeAType(esk239_0),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
tcf(c_0_64,negated_conjecture,
vsomeAType(esk239_0) = vsomeAType(vYesNo),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_60,c_0_61]),c_0_48]) ).
tcf(c_0_65,negated_conjecture,
! [X15: vATMap,X5: vExp] :
( ( vsomeExp(esk240_0) != vsomeExp(X5) )
| ( vecheck(X15,X5) = vsomeAType(vYesNo) ) ),
inference(er,[status(thm)],[c_0_62]) ).
tcf(c_0_66,negated_conjecture,
vecheck(vtypeAM(esk237_0),esk240_0) != vsomeAType(vYesNo),
inference(rw,[status(thm)],[c_0_63,c_0_64]) ).
tcf(c_0_67,negated_conjecture,
! [X15: vATMap] : vecheck(X15,esk240_0) = vsomeAType(vYesNo),
inference(er,[status(thm)],[c_0_65]) ).
cnf(c_0_68,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_66,c_0_67])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM273_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.58 % Computer : n009.cluster.edu
% 0.12/0.58 % Model : x86_64 x86_64
% 0.12/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.58 % Memory : 8046.5625MB
% 0.12/0.58 % OS : Linux 6.8.0-71-generic
% 0.12/0.58 % CPULimit : 300
% 0.12/0.58 % WCLimit : 300
% 0.12/0.58 % DateTime : Mon Sep 21 14:22:43 UTC 2026
% 0.12/0.58 % CPUTime :
% 0.12/0.58 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.62 Running first-order theorem proving
% 0.12/0.62 Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.42/2.37 % Version: 3.5.1
% 11.42/2.37 % Preprocessing class: FSLMSMSMSSSNFFN.
% 11.42/2.37 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 11.42/2.37 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 11.42/2.37 % Starting new_bool_3 with 600s (2) cores
% 11.42/2.37 % Starting new_bool_1 with 300s (1) cores
% 11.42/2.37 % Starting sh5l with 300s (1) cores
% 11.42/2.37 % G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with pid 1997217 completed with status 0
% 11.42/2.37 % Result found by G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S
% 11.42/2.37 % Preprocessing class: FSLMSMSMSSSNFFN.
% 11.42/2.37 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 11.42/2.37 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 11.42/2.37 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 11.42/2.37 % No SInE strategy applied
% 11.42/2.37 % Search class: FGUSM-SMLM32-DFFFFFNN
% 11.42/2.37 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 11.42/2.37 % Starting SubtermCWHack with 109s (1) cores
% 11.42/2.37 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 121s (1) cores
% 11.42/2.37 % Starting sh3 with 217s (1) cores
% 11.42/2.37 % Starting ho_unfolding_3 with 217s (1) cores
% 11.42/2.37 % G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with pid 1997235 completed with status 0
% 11.42/2.38 % Result found by G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S
% 11.42/2.38 % Preprocessing class: FSLMSMSMSSSNFFN.
% 11.42/2.38 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 11.42/2.38 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 11.42/2.38 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 11.42/2.38 % No SInE strategy applied
% 11.42/2.38 % Search class: FGUSM-SMLM32-DFFFFFNN
% 11.42/2.38 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 11.42/2.38 % Starting SubtermCWHack with 109s (1) cores
% 11.42/2.38 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 121s (1) cores
% 11.42/2.38 % Preprocessing time : 0.027 s
% 11.42/2.38 % Presaturation interreduction done
% 11.42/2.38
% 11.42/2.38 % Proof found!
% 11.42/2.38 % SZS status Theorem
% 11.42/2.38 % SZS output start CNFRefutation
% See solution above
% 11.42/2.38 % Parsed axioms : 508
% 11.42/2.38 % Removed by relevancy pruning/SinE : 0
% 11.42/2.38 % Initial clauses : 2529
% 11.42/2.38 % Removed in clause preprocessing : 151
% 11.42/2.38 % Initial clauses in saturation : 2378
% 11.42/2.38 % Processed clauses : 7355
% 11.42/2.38 % ...of these trivial : 24
% 11.42/2.38 % ...subsumed : 2204
% 11.42/2.38 % ...remaining for further processing : 5127
% 11.42/2.38 % Other redundant clauses eliminated : 1467
% 11.42/2.38 % Clauses deleted for lack of memory : 0
% 11.42/2.38 % Backward-subsumed : 8
% 11.42/2.38 % Backward-rewritten : 47
% 11.42/2.38 % Generated clauses : 27103
% 11.42/2.38 % ...of the previous two non-redundant : 23952
% 11.42/2.38 % ...aggressively subsumed : 0
% 11.42/2.38 % Contextual simplify-reflections : 38
% 11.42/2.38 % Paramodulations : 25259
% 11.42/2.38 % Factorizations : 95
% 11.42/2.38 % NegExts : 0
% 11.42/2.38 % Equation resolutions : 1749
% 11.42/2.38 % Disequality decompositions : 0
% 11.42/2.38 % Total rewrite steps : 3902
% 11.42/2.38 % ...of those cached : 3443
% 11.42/2.38 % Propositional unsat checks : 0
% 11.42/2.38 % Propositional check models : 0
% 11.42/2.38 % Propositional check unsatisfiable : 0
% 11.42/2.38 % Propositional clauses : 0
% 11.42/2.38 % Propositional clauses after purity: 0
% 11.42/2.38 % Propositional unsat core size : 0
% 11.42/2.38 % Propositional preprocessing time : 0.000
% 11.42/2.38 % Propositional encoding time : 0.000
% 11.42/2.38 % Propositional solver time : 0.000
% 11.42/2.38 % Success case prop preproc time : 0.000
% 11.42/2.38 % Success case prop encoding time : 0.000
% 11.42/2.38 % Success case prop solver time : 0.000
% 11.42/2.38 % Current number of processed clauses : 2982
% 11.42/2.38 % Positive orientable unit clauses : 227
% 11.42/2.38 % Positive unorientable unit clauses: 22
% 11.42/2.38 % Negative unit clauses : 196
% 11.42/2.38 % Non-unit-clauses : 2537
% 11.42/2.38 % Current number of unprocessed clauses: 20885
% 11.42/2.38 % ...number of literals in the above : 80749
% 11.42/2.38 % Current number of archived formulas : 0
% 11.42/2.38 % Current number of archived clauses : 2151
% 11.42/2.38 % Clause-clause subsumption calls (NU) : 1703140
% 11.42/2.38 % Rec. Clause-clause subsumption calls : 605991
% 11.42/2.38 % Non-unit clause-clause subsumptions : 1417
% 11.42/2.38 % Unit Clause-clause subsumption calls : 128204
% 11.42/2.38 % Rewrite failures with RHS unbound : 309
% 11.42/2.38 % BW rewrite match attempts : 2612
% 11.42/2.38 % BW rewrite match successes : 110
% 11.42/2.38 % Condensation attempts : 0
% 11.42/2.38 % Condensation successes : 0
% 11.42/2.38 % Termbank termtop insertions : 389422
% 11.42/2.38 % Search garbage collected termcells : 16399
% 11.42/2.38
% 11.42/2.38 % -------------------------------------------------
% 11.42/2.38 % User time : 1.629 s
% 11.42/2.38 % System time : 0.043 s
% 11.42/2.38 % Total time : 1.672 s
% 11.42/2.38 % Maximum resident set size: 8840 pages
% 11.42/2.38
% 11.42/2.38 % -------------------------------------------------
% 11.42/2.38 % User time : 6.309 s
% 11.42/2.38 % System time : 0.179 s
% 11.42/2.38 % Total time : 6.488 s
% 11.42/2.38 % Maximum resident set size: 5632 pages
% 11.42/2.38 % E exiting
%------------------------------------------------------------------------------