%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : COM219_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 : n010.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:45 PM UTC 2026
% Result : Theorem 0.22s 10.65s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 14
% Syntax : Number of formulae : 71 ( 37 unt; 0 typ; 0 def)
% Number of atoms : 197 ( 119 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 218 ( 92 ~; 76 |; 40 &)
% ( 1 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 7 con; 0-3 aty)
% Number of variables : 130 ( 0 sgn 121 !; 9 ?; 130 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
vOptTerm: $tType ).
tff(decl_sort2,type,
vTy: $tType ).
tff(decl_sort3,type,
vTerm: $tType ).
tff(decl_24,type,
vSucc: vTerm > vTerm ).
tff(decl_25,type,
vPred: vTerm > vTerm ).
tff(decl_26,type,
vsomeTerm: vTerm > vOptTerm ).
tff(decl_27,type,
vZero: vTerm ).
tff(decl_28,type,
vIszero: vTerm > vTerm ).
tff(decl_29,type,
vTrue: vTerm ).
tff(decl_30,type,
vFalse: vTerm ).
tff(decl_32,type,
vPlus: ( vTerm * vTerm ) > vTerm ).
tff(decl_34,type,
vIfelse: ( vTerm * ( vTerm * vTerm ) ) > vTerm ).
tff(decl_35,type,
vt1: vTerm ).
tff(decl_37,type,
visNV: vTerm > $o ).
tff(decl_38,type,
vreduce: vTerm > vOptTerm ).
tff(decl_40,type,
visSomeTerm: vOptTerm > $o ).
tff(decl_41,type,
vptchecksimple: ( vTy * vTerm ) > $o ).
tff(decl_43,type,
esk1_0: vTerm ).
tff(decl_44,type,
esk2_0: vTy ).
tff(decl_45,type,
esk3_0: vTerm ).
tff(decl_47,type,
esk5_1: vTerm > vTerm ).
tff(decl_48,type,
esk6_1: vTerm > vTerm ).
tff(decl_49,type,
esk7_1: vTerm > vTerm ).
tff(decl_50,type,
esk8_1: vTerm > vTerm ).
tff(decl_51,type,
esk9_1: vTerm > vTerm ).
tff(decl_52,type,
esk10_1: vTerm > vTerm ).
tff(decl_53,type,
esk11_1: vTerm > vTerm ).
tff(decl_54,type,
esk12_1: vTerm > vTerm ).
tff(decl_56,type,
esk14_1: vTerm > vTerm ).
tff('DIFF-Ifelse-Succ',axiom,
! [X2: vTerm,X3: vTerm,X4: vTerm,X5: vTerm] : ( vIfelse(X2,X3,X4) != vSucc(X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-Ifelse-Succ') ).
tff('DIFF-Succ-Plus',axiom,
! [X2: vTerm,X3: vTerm,X4: vTerm] : ( vSucc(X2) != vPlus(X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-Succ-Plus') ).
tff('DIFF-Succ-Iszero',axiom,
! [X2: vTerm,X3: vTerm] : ( vSucc(X2) != vIszero(X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-Succ-Iszero') ).
tff('DIFF-Succ-Pred',axiom,
! [X2: vTerm,X3: vTerm] : ( vSucc(X2) != vPred(X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-Succ-Pred') ).
tff('DIFF-False-Succ',axiom,
! [X2: vTerm] : ( vFalse != vSucc(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-False-Succ') ).
tff('DIFF-True-Succ',axiom,
! [X2: vTerm] : ( vTrue != vSucc(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-True-Succ') ).
tff('DIFF-Zero-Succ',axiom,
! [X2: vTerm] : ( vZero != vSucc(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-Zero-Succ') ).
tff('Preservation-Iszero-Succ-isNV-False',conjecture,
! [X11: vTerm,X98: vTy,X99: vTerm] :
( ( ( vreduce(vIszero(vt1)) = vsomeTerm(X99) )
& vptchecksimple(vIszero(vt1),X98)
& ( vt1 = vSucc(X11) )
& ( vt1 != vZero )
& ~ visNV(X11) )
=> vptchecksimple(X99,X98) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Preservation-Iszero-Succ-isNV-False') ).
tff('dom-Term',axiom,
! [X1: vTerm] :
( ? [X2: vTerm,X3: vTerm] : ( X1 = vPlus(X2,X3) )
| ? [X2: vTerm] : ( X1 = vIszero(X2) )
| ? [X2: vTerm] : ( X1 = vPred(X2) )
| ? [X2: vTerm] : ( X1 = vSucc(X2) )
| ( X1 = vZero )
| ? [X2: vTerm,X3: vTerm,X4: vTerm] : ( X1 = vIfelse(X2,X3,X4) )
| ( X1 = vFalse )
| ( X1 = vTrue ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-Term') ).
tff('isNV-1',axiom,
! [X11: vTerm] :
( visNV(vSucc(X11))
<=> visNV(X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isNV-1') ).
tff('EQ-Succ',axiom,
! [X2: vTerm,X3: vTerm] :
( ( vSucc(X2) = vSucc(X3) )
=> ( X2 = X3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-Succ') ).
tff('Preservation-Iszero-Succ-isNV-False-isSomeTerm-False',axiom,
! [X11: vTerm,X98: vTy,X99: vTerm] :
( ( ( vreduce(vIszero(vt1)) = vsomeTerm(X99) )
& vptchecksimple(vIszero(vt1),X98)
& ( vt1 = vSucc(X11) )
& ( vt1 != vZero )
& ~ visNV(X11)
& ~ visSomeTerm(vreduce(vSucc(X11))) )
=> vptchecksimple(X99,X98) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Preservation-Iszero-Succ-isNV-False-isSomeTerm-False') ).
tff('isNV-true-INV',axiom,
! [X2: vTerm] :
( visNV(X2)
=> ( ? [X11: vTerm] :
( visNV(X11)
& ( X2 = vSucc(X11) ) )
| ( X2 = vZero ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isNV-true-INV') ).
tff('Preservation-Iszero-Succ-isNV-False-isSomeTerm-True',axiom,
! [X11: vTerm,X98: vTy,X99: vTerm] :
( ( ( vreduce(vIszero(vt1)) = vsomeTerm(X99) )
& vptchecksimple(vIszero(vt1),X98)
& ( vt1 = vSucc(X11) )
& ( vt1 != vZero )
& ~ visNV(X11)
& visSomeTerm(vreduce(vSucc(X11))) )
=> vptchecksimple(X99,X98) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Preservation-Iszero-Succ-isNV-False-isSomeTerm-True') ).
tff(c_0_14,plain,
! [X2: vTerm,X3: vTerm,X4: vTerm,X5: vTerm] : ( vIfelse(X2,X3,X4) != vSucc(X5) ),
inference(fof_simplification,[status(thm)],['DIFF-Ifelse-Succ']) ).
tff(c_0_15,plain,
! [X2: vTerm,X3: vTerm,X4: vTerm] : ( vSucc(X2) != vPlus(X3,X4) ),
inference(fof_simplification,[status(thm)],['DIFF-Succ-Plus']) ).
tff(c_0_16,plain,
! [X2: vTerm,X3: vTerm] : ( vSucc(X2) != vIszero(X3) ),
inference(fof_simplification,[status(thm)],['DIFF-Succ-Iszero']) ).
tff(c_0_17,plain,
! [X2: vTerm,X3: vTerm] : ( vSucc(X2) != vPred(X3) ),
inference(fof_simplification,[status(thm)],['DIFF-Succ-Pred']) ).
tff(c_0_18,plain,
! [X2: vTerm] : ( vFalse != vSucc(X2) ),
inference(fof_simplification,[status(thm)],['DIFF-False-Succ']) ).
tff(c_0_19,plain,
! [X2: vTerm] : ( vTrue != vSucc(X2) ),
inference(fof_simplification,[status(thm)],['DIFF-True-Succ']) ).
tff(c_0_20,plain,
! [X2: vTerm] : ( vZero != vSucc(X2) ),
inference(fof_simplification,[status(thm)],['DIFF-Zero-Succ']) ).
tff(c_0_21,negated_conjecture,
~ ! [X11: vTerm,X98: vTy,X99: vTerm] :
( ( ( vreduce(vIszero(vt1)) = vsomeTerm(X99) )
& vptchecksimple(vIszero(vt1),X98)
& ( vt1 = vSucc(X11) )
& ( vt1 != vZero )
& ~ visNV(X11) )
=> vptchecksimple(X99,X98) ),
inference(assume_negation,[status(cth)],['Preservation-Iszero-Succ-isNV-False']) ).
tff(c_0_22,plain,
! [X185: vTerm,X186: vTerm,X187: vTerm,X188: vTerm] : ( vIfelse(X185,X186,X187) != vSucc(X188) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_14])]) ).
tff(c_0_23,plain,
! [X122: vTerm] :
( ( X122 = vPlus(esk11_1(X122),esk12_1(X122)) )
| ( X122 = vIszero(esk10_1(X122)) )
| ( X122 = vPred(esk9_1(X122)) )
| ( X122 = vSucc(esk8_1(X122)) )
| ( X122 = vZero )
| ( X122 = vIfelse(esk5_1(X122),esk6_1(X122),esk7_1(X122)) )
| ( X122 = vFalse )
| ( X122 = vTrue ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['dom-Term'])]) ).
tff(c_0_24,plain,
! [X246: vTerm,X247: vTerm,X248: vTerm] : ( vSucc(X246) != vPlus(X247,X248) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_15])]) ).
tff(c_0_25,plain,
! [X140: vTerm,X141: vTerm] : ( vSucc(X140) != vIszero(X141) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_16])]) ).
tff(c_0_26,plain,
! [X230: vTerm,X231: vTerm] : ( vSucc(X230) != vPred(X231) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_17])]) ).
tff(c_0_27,plain,
! [X224: vTerm] : ( vFalse != vSucc(X224) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_18])]) ).
tff(c_0_28,plain,
! [X220: vTerm] : ( vTrue != vSucc(X220) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_19])]) ).
tff(c_0_29,plain,
! [X157: vTerm] : ( vZero != vSucc(X157) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_20])]) ).
tff(c_0_30,negated_conjecture,
~ ! [X11: vTerm,X98: vTy,X99: vTerm] :
( ( ( vreduce(vIszero(vt1)) = vsomeTerm(X99) )
& vptchecksimple(vIszero(vt1),X98)
& ( vt1 = vSucc(X11) )
& ( vt1 != vZero )
& ~ visNV(X11) )
=> vptchecksimple(X99,X98) ),
inference(fof_simplification,[status(thm)],[c_0_21]) ).
tff(c_0_31,plain,
! [X172: vTerm] :
( ( visNV(vSucc(X172))
| ~ visNV(X172) )
& ( visNV(X172)
| ~ visNV(vSucc(X172)) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['isNV-1'])])]) ).
tcf(c_0_32,plain,
! [X1: vTerm,X2: vTerm,X3: vTerm,X4: vTerm] : vIfelse(X1,X2,X3) != vSucc(X4),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
tcf(c_0_33,plain,
! [X1: vTerm] :
( ( X1 = vPlus(esk11_1(X1),esk12_1(X1)) )
| ( X1 = vIszero(esk10_1(X1)) )
| ( X1 = vPred(esk9_1(X1)) )
| ( X1 = vSucc(esk8_1(X1)) )
| ( X1 = vZero )
| ( X1 = vIfelse(esk5_1(X1),esk6_1(X1),esk7_1(X1)) )
| ( X1 = vFalse )
| ( X1 = vTrue ) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
tcf(c_0_34,plain,
! [X1: vTerm,X2: vTerm,X3: vTerm] : vSucc(X1) != vPlus(X2,X3),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
tcf(c_0_35,plain,
! [X1: vTerm,X2: vTerm] : vSucc(X1) != vIszero(X2),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
tcf(c_0_36,plain,
! [X1: vTerm,X2: vTerm] : vSucc(X1) != vPred(X2),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
tcf(c_0_37,plain,
! [X1: vTerm] : vFalse != vSucc(X1),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
tcf(c_0_38,plain,
! [X1: vTerm] : vTrue != vSucc(X1),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
tcf(c_0_39,plain,
! [X1: vTerm] : vZero != vSucc(X1),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
tff(c_0_40,plain,
! [X155: vTerm,X156: vTerm] :
( ( X155 = X156 )
| ( vSucc(X155) != vSucc(X156) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['EQ-Succ'])])]) ).
tff(c_0_41,negated_conjecture,
( ~ vptchecksimple(esk3_0,esk2_0)
& ( vreduce(vIszero(vt1)) = vsomeTerm(esk3_0) )
& vptchecksimple(vIszero(vt1),esk2_0)
& ( vt1 = vSucc(esk1_0) )
& ( vt1 != vZero )
& ~ visNV(esk1_0) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_30])])])]) ).
tff(c_0_42,plain,
! [X11: vTerm,X98: vTy,X99: vTerm] :
( ( ( vreduce(vIszero(vt1)) = vsomeTerm(X99) )
& vptchecksimple(vIszero(vt1),X98)
& ( vt1 = vSucc(X11) )
& ( vt1 != vZero )
& ~ visNV(X11)
& ~ visSomeTerm(vreduce(vSucc(X11))) )
=> vptchecksimple(X99,X98) ),
inference(fof_simplification,[status(thm)],['Preservation-Iszero-Succ-isNV-False-isSomeTerm-False']) ).
tcf(c_0_43,plain,
! [X1: vTerm] :
( ~ visNV(vSucc(X1))
| visNV(X1) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
tcf(c_0_44,plain,
! [X1: vTerm] : vSucc(esk8_1(vSucc(X1))) = vSucc(X1),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_33])]),c_0_34]),c_0_35]),c_0_36]),c_0_37]),c_0_38]),c_0_39]) ).
tff(c_0_45,plain,
! [X166: vTerm] :
( ( ~ visNV(X166)
| ( X166 = vZero )
| visNV(esk14_1(X166)) )
& ( ~ visNV(X166)
| ( X166 = vZero )
| ( X166 = vSucc(esk14_1(X166)) ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['isNV-true-INV'])])])])]) ).
tcf(c_0_46,plain,
! [X1: vTerm,X2: vTerm] :
( ( vSucc(X1) != vSucc(X2) )
| ( X1 = X2 ) ),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
tcf(c_0_47,negated_conjecture,
vt1 = vSucc(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_41]) ).
tff(c_0_48,plain,
! [X11: vTerm,X98: vTy,X99: vTerm] :
( ( ( vreduce(vIszero(vt1)) = vsomeTerm(X99) )
& vptchecksimple(vIszero(vt1),X98)
& ( vt1 = vSucc(X11) )
& ( vt1 != vZero )
& ~ visNV(X11)
& visSomeTerm(vreduce(vSucc(X11))) )
=> vptchecksimple(X99,X98) ),
inference(fof_simplification,[status(thm)],['Preservation-Iszero-Succ-isNV-False-isSomeTerm-True']) ).
tff(c_0_49,plain,
! [X152: vTerm,X153: vTy,X154: vTerm] :
( vptchecksimple(X154,X153)
| ( vreduce(vIszero(vt1)) != vsomeTerm(X154) )
| ~ vptchecksimple(vIszero(vt1),X153)
| ( vt1 != vSucc(X152) )
| ( vt1 = vZero )
| visNV(X152)
| visSomeTerm(vreduce(vSucc(X152))) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_42])])]) ).
tcf(c_0_50,plain,
! [X1: vTerm] :
( ~ visNV(vSucc(X1))
| visNV(esk8_1(vSucc(X1))) ),
inference(spm,[status(thm)],[c_0_43,c_0_44]) ).
tcf(c_0_51,plain,
! [X1: vTerm] :
( ~ visNV(X1)
| ( X1 = vZero )
| ( X1 = vSucc(esk14_1(X1)) ) ),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
tcf(c_0_52,negated_conjecture,
! [X1: vTerm] :
( ( vSucc(X1) != vt1 )
| ( X1 = esk1_0 ) ),
inference(spm,[status(thm)],[c_0_46,c_0_47]) ).
tff(c_0_53,plain,
! [X149: vTerm,X150: vTy,X151: vTerm] :
( vptchecksimple(X151,X150)
| ( vreduce(vIszero(vt1)) != vsomeTerm(X151) )
| ~ vptchecksimple(vIszero(vt1),X150)
| ( vt1 != vSucc(X149) )
| ( vt1 = vZero )
| visNV(X149)
| ~ visSomeTerm(vreduce(vSucc(X149))) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_48])])]) ).
tcf(c_0_54,plain,
! [X1: vTerm,X9: vTy,X2: vTerm] :
( ( vreduce(vIszero(vt1)) != vsomeTerm(X2) )
| ~ vptchecksimple(vIszero(vt1),X9)
| ( vt1 != vSucc(X1) )
| vptchecksimple(X2,X9)
| ( vt1 = vZero )
| visNV(X1)
| visSomeTerm(vreduce(vSucc(X1))) ),
inference(split_conjunct,[status(thm)],[c_0_49]) ).
tcf(c_0_55,negated_conjecture,
vt1 != vZero,
inference(split_conjunct,[status(thm)],[c_0_41]) ).
tcf(c_0_56,plain,
! [X1: vTerm] :
( ~ visNV(X1)
| visNV(esk8_1(X1))
| ( X1 = vZero ) ),
inference(spm,[status(thm)],[c_0_50,c_0_51]) ).
tcf(c_0_57,negated_conjecture,
! [X1: vTerm] :
( ( vSucc(X1) != vt1 )
| ( esk8_1(vSucc(X1)) = esk1_0 ) ),
inference(spm,[status(thm)],[c_0_52,c_0_44]) ).
tcf(c_0_58,negated_conjecture,
~ visNV(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_41]) ).
tcf(c_0_59,plain,
! [X1: vTerm,X9: vTy,X2: vTerm] :
( ( vreduce(vIszero(vt1)) != vsomeTerm(X2) )
| ~ vptchecksimple(vIszero(vt1),X9)
| ( vt1 != vSucc(X1) )
| ~ visSomeTerm(vreduce(vSucc(X1)))
| vptchecksimple(X2,X9)
| ( vt1 = vZero )
| visNV(X1) ),
inference(split_conjunct,[status(thm)],[c_0_53]) ).
tcf(c_0_60,plain,
! [X1: vTerm,X2: vTerm,X9: vTy] :
( ~ vptchecksimple(vIszero(vt1),X9)
| ( vSucc(X2) != vt1 )
| ( vsomeTerm(X1) != vreduce(vIszero(vt1)) )
| visNV(X2)
| visSomeTerm(vreduce(vSucc(X2)))
| vptchecksimple(X1,X9) ),
inference(sr,[status(thm)],[c_0_54,c_0_55]) ).
tcf(c_0_61,negated_conjecture,
! [X1: vTerm] :
( ~ visNV(vSucc(X1))
| ( vSucc(X1) != vt1 ) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_56,c_0_57]),c_0_39]),c_0_58]) ).
tcf(c_0_62,plain,
! [X1: vTerm] :
( ~ visNV(X1)
| visNV(vSucc(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
tcf(c_0_63,plain,
! [X1: vTerm,X2: vTerm,X9: vTy] :
( ~ vptchecksimple(vIszero(vt1),X9)
| ( vSucc(X2) != vt1 )
| ( vsomeTerm(X1) != vreduce(vIszero(vt1)) )
| visNV(X2)
| vptchecksimple(X1,X9) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_59,c_0_55]),c_0_60]) ).
tcf(c_0_64,negated_conjecture,
vptchecksimple(vIszero(vt1),esk2_0),
inference(split_conjunct,[status(thm)],[c_0_41]) ).
tcf(c_0_65,negated_conjecture,
! [X1: vTerm] :
( ~ visNV(X1)
| ( vSucc(X1) != vt1 ) ),
inference(spm,[status(thm)],[c_0_61,c_0_62]) ).
tcf(c_0_66,negated_conjecture,
! [X1: vTerm,X2: vTerm] :
( ( vSucc(X2) != vt1 )
| ( vsomeTerm(X1) != vreduce(vIszero(vt1)) )
| vptchecksimple(X1,esk2_0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_63,c_0_64]),c_0_65]) ).
tcf(c_0_67,negated_conjecture,
vreduce(vIszero(vt1)) = vsomeTerm(esk3_0),
inference(split_conjunct,[status(thm)],[c_0_41]) ).
tcf(c_0_68,negated_conjecture,
~ vptchecksimple(esk3_0,esk2_0),
inference(split_conjunct,[status(thm)],[c_0_41]) ).
tcf(c_0_69,negated_conjecture,
! [X1: vTerm] : vSucc(X1) != vt1,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_66,c_0_67]),c_0_68]) ).
cnf(c_0_70,negated_conjecture,
$false,
inference(sr,[status(thm)],[c_0_47,c_0_69]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : COM219_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.08 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/10.46 % Computer : n010.cluster.edu
% 0.18/10.46 % Model : x86_64 x86_64
% 0.18/10.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/10.46 % Memory : 8046.5625MB
% 0.18/10.46 % OS : Linux 6.8.0-71-generic
% 0.18/10.46 % CPULimit : 300
% 0.18/10.46 % WCLimit : 300
% 0.18/10.46 % DateTime : Mon Sep 21 14:20:38 UTC 2026
% 0.18/10.46 % CPUTime :
% 0.18/10.46 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/10.50 Running first-order theorem proving
% 0.22/10.50 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
% 0.22/10.65 % Version: 3.5.1
% 0.22/10.65 % Preprocessing class: FSLSSMSSSSSNFFN.
% 0.22/10.65 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/10.65 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 0.22/10.65 % Starting new_bool_3 with 300s (1) cores
% 0.22/10.65 % Starting new_bool_1 with 300s (1) cores
% 0.22/10.65 % Starting sh5l with 300s (1) cores
% 0.22/10.65 % new_bool_3 with pid 1087691 completed with status 0
% 0.22/10.65 % Result found by new_bool_3
% 0.22/10.65 % Preprocessing class: FSLSSMSSSSSNFFN.
% 0.22/10.65 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/10.65 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 0.22/10.65 % Starting new_bool_3 with 300s (1) cores
% 0.22/10.65 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.22/10.65 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.22/10.65 % Search class: FGUSS-FFMM31-MFFFFFNN
% 0.22/10.65 % partial match(2): FGHSM-FFMM31-MFFFFFNN
% 0.22/10.65 % Scheduled 13 strats onto 1 cores with 300 seconds (300 total)
% 0.22/10.65 % Starting SubtermCWHack with 28s (1) cores
% 0.22/10.65 % SubtermCWHack with pid 1087694 completed with status 0
% 0.22/10.65 % Result found by SubtermCWHack
% 0.22/10.65 % Preprocessing class: FSLSSMSSSSSNFFN.
% 0.22/10.65 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/10.65 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 0.22/10.65 % Starting new_bool_3 with 300s (1) cores
% 0.22/10.65 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.22/10.65 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.22/10.65 % Search class: FGUSS-FFMM31-MFFFFFNN
% 0.22/10.65 % partial match(2): FGHSM-FFMM31-MFFFFFNN
% 0.22/10.65 % Scheduled 13 strats onto 1 cores with 300 seconds (300 total)
% 0.22/10.65 % Starting SubtermCWHack with 28s (1) cores
% 0.22/10.65 % Preprocessing time : 0.003 s
% 0.22/10.65
% 0.22/10.65 % Proof found!
% 0.22/10.65 % SZS status Theorem
% 0.22/10.65 % SZS output start CNFRefutation
% See solution above
% 0.22/10.65 % Parsed axioms : 131
% 0.22/10.65 % Removed by relevancy pruning/SinE : 52
% 0.22/10.65 % Initial clauses : 102
% 0.22/10.65 % Removed in clause preprocessing : 0
% 0.22/10.65 % Initial clauses in saturation : 102
% 0.22/10.65 % Processed clauses : 2267
% 0.22/10.65 % ...of these trivial : 18
% 0.22/10.65 % ...subsumed : 1456
% 0.22/10.65 % ...remaining for further processing : 793
% 0.22/10.65 % Other redundant clauses eliminated : 185
% 0.22/10.65 % Clauses deleted for lack of memory : 0
% 0.22/10.65 % Backward-subsumed : 16
% 0.22/10.65 % Backward-rewritten : 38
% 0.22/10.65 % Generated clauses : 5699
% 0.22/10.65 % ...of the previous two non-redundant : 4925
% 0.22/10.65 % ...aggressively subsumed : 0
% 0.22/10.65 % Contextual simplify-reflections : 21
% 0.22/10.65 % Paramodulations : 5500
% 0.22/10.65 % Factorizations : 0
% 0.22/10.65 % NegExts : 0
% 0.22/10.65 % Equation resolutions : 198
% 0.22/10.65 % Disequality decompositions : 0
% 0.22/10.65 % Total rewrite steps : 1105
% 0.22/10.65 % ...of those cached : 802
% 0.22/10.65 % Propositional unsat checks : 0
% 0.22/10.65 % Propositional check models : 0
% 0.22/10.65 % Propositional check unsatisfiable : 0
% 0.22/10.65 % Propositional clauses : 0
% 0.22/10.65 % Propositional clauses after purity: 0
% 0.22/10.65 % Propositional unsat core size : 0
% 0.22/10.65 % Propositional preprocessing time : 0.000
% 0.22/10.65 % Propositional encoding time : 0.000
% 0.22/10.65 % Propositional solver time : 0.000
% 0.22/10.65 % Success case prop preproc time : 0.000
% 0.22/10.65 % Success case prop encoding time : 0.000
% 0.22/10.65 % Success case prop solver time : 0.000
% 0.22/10.65 % Current number of processed clauses : 738
% 0.22/10.65 % Positive orientable unit clauses : 427
% 0.22/10.65 % Positive unorientable unit clauses: 11
% 0.22/10.65 % Negative unit clauses : 114
% 0.22/10.65 % Non-unit-clauses : 186
% 0.22/10.65 % Current number of unprocessed clauses: 2718
% 0.22/10.65 % ...number of literals in the above : 6597
% 0.22/10.65 % Current number of archived formulas : 0
% 0.22/10.65 % Current number of archived clauses : 55
% 0.22/10.65 % Clause-clause subsumption calls (NU) : 7772
% 0.22/10.65 % Rec. Clause-clause subsumption calls : 3403
% 0.22/10.65 % Non-unit clause-clause subsumptions : 241
% 0.22/10.65 % Unit Clause-clause subsumption calls : 1281
% 0.22/10.65 % Rewrite failures with RHS unbound : 305
% 0.22/10.65 % BW rewrite match attempts : 12522
% 0.22/10.65 % BW rewrite match successes : 75
% 0.22/10.65 % Condensation attempts : 0
% 0.22/10.65 % Condensation successes : 0
% 0.22/10.65 % Termbank termtop insertions : 102718
% 0.22/10.65 % Search garbage collected termcells : 1964
% 0.22/10.65
% 0.22/10.65 % -------------------------------------------------
% 0.22/10.65 % User time : 0.112 s
% 0.22/10.65 % System time : 0.012 s
% 0.22/10.65 % Total time : 0.124 s
% 0.22/10.65 % Maximum resident set size: 4100 pages
% 0.22/10.65
% 0.22/10.65 % -------------------------------------------------
% 0.22/10.65 % User time : 0.117 s
% 0.22/10.65 % System time : 0.016 s
% 0.22/10.65 % Total time : 0.133 s
% 0.22/10.65 % Maximum resident set size: 5120 pages
% 0.22/10.65 % E exiting
%------------------------------------------------------------------------------