%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM837+1 : TPTP v9.2.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n031.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:58:40 PM UTC 2026
% Result : Theorem 0.28s 1.62s
% Output : CNFRefutation 0.28s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_46)
% Comments :
%------------------------------------------------------------------------------
fof('ass(cond(52, 0), 0)',axiom,
! [X33,X34] : vplus(vsucc(X33),X34) = vsucc(vplus(X33,X34)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(52, 0), 0)') ).
fof('qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))',axiom,
! [X39,X40] :
( vplus(X39,vsucc(X40)) = vsucc(vplus(X39,X40))
& vplus(X39,v1) = vsucc(X39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))') ).
fof('ass(cond(goal(130), 0), 2)',axiom,
! [X14,X15] :
( ~ greater(X14,X15)
| ~ less(X14,X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 2)') ).
fof('qu(antec(axiom(3)), imp(antec(axiom(3))))',axiom,
! [X45,X46] :
( vsucc(X45) = vsucc(X46)
=> X45 = X46 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(antec(axiom(3)), imp(antec(axiom(3))))') ).
fof('ass(cond(6, 0), 0)',axiom,
! [X43,X44] :
( X43 != X44
=> vsucc(X43) != vsucc(X44) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(6, 0), 0)') ).
fof('ass(cond(goal(130), 0), 3)',axiom,
! [X14,X15] :
( X14 != X15
| ~ greater(X14,X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 3)') ).
fof('ass(cond(goal(130), 0), 1)',axiom,
! [X14,X15] :
( X14 != X15
| ~ less(X14,X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 1)') ).
fof('ass(cond(43, 0), 0)',axiom,
! [X35] : vplus(v1,X35) = vsucc(X35),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(43, 0), 0)') ).
fof('ass(cond(12, 0), 0)',axiom,
! [X42] : vsucc(X42) != X42,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(12, 0), 0)') ).
fof('ass(cond(20, 0), 0)',axiom,
! [X41] :
( X41 != v1
=> X41 = vsucc(vskolem2(X41)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(20, 0), 0)') ).
fof('qu(restrictor(axiom(1)), holds(scope(axiom(1)), 2, 0))',axiom,
! [X47] : vsucc(X47) != v1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(restrictor(axiom(1)), holds(scope(axiom(1)), 2, 0))') ).
fof('qe(171)',conjecture,
? [X1] : vd269 = vplus(vd268,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qe(171)') ).
fof('ass(cond(goal(88), 0), 0)',axiom,
! [X22,X23] :
( X22 = X23
| ? [X24] : X22 = vplus(X23,X24)
| ? [X25] : X23 = vplus(X22,X25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 0)') ).
fof('ass(cond(33, 0), 0)',axiom,
! [X36,X37,X38] : vplus(vplus(X36,X37),X38) = vplus(X36,vplus(X37,X38)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(33, 0), 0)') ).
fof('def(cond(conseq(axiom(3)), 11), 1)',axiom,
! [X19,X20] :
( greater(X20,X19)
<=> ? [X21] : X20 = vplus(X19,X21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 11), 1)') ).
fof('def(cond(conseq(axiom(3)), 12), 1)',axiom,
! [X16,X17] :
( less(X17,X16)
<=> ? [X18] : X16 = vplus(X17,X18) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 12), 1)') ).
fof('ass(cond(goal(88), 0), 2)',axiom,
! [X22,X23] :
( ~ ? [X24] : X22 = vplus(X23,X24)
| ~ ? [X25] : X23 = vplus(X22,X25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 2)') ).
fof('ass(cond(81, 0), 0)',axiom,
! [X26,X27] :
( X26 != X27
=> ! [X28] : vplus(X28,X26) != vplus(X28,X27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(81, 0), 0)') ).
fof('def(cond(conseq(axiom(3)), 16), 1)',axiom,
! [X8,X9] :
( geq(X9,X8)
<=> ( greater(X9,X8)
| X9 = X8 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 16), 1)') ).
fof('def(cond(conseq(axiom(3)), 17), 1)',axiom,
! [X6,X7] :
( leq(X7,X6)
<=> ( less(X7,X6)
| X7 = X6 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 17), 1)') ).
fof('ass(cond(147, 0), 0)',axiom,
! [X10,X11] :
( less(X10,X11)
=> greater(X11,X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(147, 0), 0)') ).
fof('ass(cond(163, 0), 0)',axiom,
! [X2,X3] :
( leq(X2,X3)
=> geq(X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(163, 0), 0)') ).
fof('ass(cond(158, 0), 0)',axiom,
! [X4,X5] :
( geq(X4,X5)
=> leq(X5,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(158, 0), 0)') ).
fof('ass(cond(140, 0), 0)',axiom,
! [X12,X13] :
( greater(X12,X13)
=> less(X13,X12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(140, 0), 0)') ).
fof('ass(cond(goal(130), 0), 0)',axiom,
! [X14,X15] :
( X14 = X15
| greater(X14,X15)
| less(X14,X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 0)') ).
fof('ass(cond(61, 0), 0)',axiom,
! [X31,X32] : vplus(X32,X31) = vplus(X31,X32),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(61, 0), 0)') ).
fof('ass(cond(goal(88), 0), 3)',axiom,
! [X22,X23] :
( X22 != X23
| ~ ? [X24] : X22 = vplus(X23,X24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 3)') ).
fof('ass(cond(goal(88), 0), 1)',axiom,
! [X22,X23] :
( X22 != X23
| ~ ? [X25] : X23 = vplus(X22,X25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 1)') ).
fof('ass(cond(73, 0), 0)',axiom,
! [X29,X30] : X30 != vplus(X29,X30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(73, 0), 0)') ).
fof('holds(conjunct1(170), 270, 0)',axiom,
less(vd268,vd269),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(170), 270, 0)') ).
fof('holds(conjunct2(170), 272, 0)',axiom,
less(vd269,vd271),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(170), 272, 0)') ).
fof(i_0_31,plain,
! [X165,X166] : vplus(vsucc(X165),X166) = vsucc(vplus(X165,X166)),
inference(variable_rename,[status(thm)],['ass(cond(52, 0), 0)']) ).
fof(i_0_32,plain,
! [X171,X172] :
( vplus(X171,vsucc(X172)) = vsucc(vplus(X171,X172))
& vplus(X171,v1) = vsucc(X171) ),
inference(variable_rename,[status(thm)],['qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))']) ).
fof(i_0_33,plain,
! [X14,X15] :
( ~ greater(X14,X15)
| ~ less(X14,X15) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 2)']) ).
fof(i_0_34,plain,
! [X177,X178] :
( vsucc(X177) != vsucc(X178)
| X177 = X178 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(antec(axiom(3)), imp(antec(axiom(3))))'])]) ).
fof(i_0_35,plain,
! [X175,X176] :
( X175 = X176
| vsucc(X175) != vsucc(X176) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(6, 0), 0)'])]) ).
fof(i_0_36,plain,
! [X14,X15] :
( X14 != X15
| ~ greater(X14,X15) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 3)']) ).
fof(i_0_37,plain,
! [X14,X15] :
( X14 != X15
| ~ less(X14,X15) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 1)']) ).
fof(i_0_38,plain,
! [X167] : vplus(v1,X167) = vsucc(X167),
inference(variable_rename,[status(thm)],['ass(cond(43, 0), 0)']) ).
fof(i_0_39,plain,
! [X174] : vsucc(X174) != X174,
inference(variable_rename,[status(thm)],['ass(cond(12, 0), 0)']) ).
fof(i_0_40,plain,
! [X173] :
( X173 = v1
| X173 = vsucc(vskolem2(X173)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(20, 0), 0)'])]) ).
fof(i_0_41,plain,
! [X179] : vsucc(X179) != v1,
inference(variable_rename,[status(thm)],['qu(restrictor(axiom(1)), holds(scope(axiom(1)), 2, 0))']) ).
fof(i_0_42,negated_conjecture,
~ ? [X1] : vd269 = vplus(vd268,X1),
inference(assume_negation,[status(cth)],['qe(171)']) ).
fof(i_0_43,plain,
! [X144,X145] :
( X144 = X145
| X144 = vplus(X145,esk3_2(X144,X145))
| X145 = vplus(X144,esk4_2(X144,X145)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['ass(cond(goal(88), 0), 0)'])]) ).
fof(i_0_44,plain,
! [X168,X169,X170] : vplus(vplus(X168,X169),X170) = vplus(X168,vplus(X169,X170)),
inference(variable_rename,[status(thm)],['ass(cond(33, 0), 0)']) ).
cnf(i_0_45,plain,
vplus(vsucc(X1),X2) = vsucc(vplus(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_31]) ).
cnf(i_0_46,plain,
vplus(X1,v1) = vsucc(X1),
inference(split_conjunct,[status(thm)],[i_0_32]) ).
cnf(i_0_47,plain,
vplus(X1,vsucc(X2)) = vsucc(vplus(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_32]) ).
fof(i_0_48,plain,
! [X138,X139,X141,X142,X143] :
( ( ~ greater(X139,X138)
| X139 = vplus(X138,esk2_2(X138,X139)) )
& ( X142 != vplus(X141,X143)
| greater(X142,X141) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],['def(cond(conseq(axiom(3)), 11), 1)'])])])])]) ).
fof(i_0_49,plain,
! [X132,X133,X135,X136,X137] :
( ( ~ less(X133,X132)
| X132 = vplus(X133,esk1_2(X132,X133)) )
& ( X135 != vplus(X136,X137)
| less(X136,X135) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],['def(cond(conseq(axiom(3)), 12), 1)'])])])])]) ).
fof(i_0_50,plain,
! [X151,X152,X153,X154] :
( X151 != vplus(X152,X153)
| X152 != vplus(X151,X154) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 2)'])])]) ).
fof(i_0_51,plain,
! [X158,X159,X160] :
( X158 = X159
| vplus(X160,X158) != vplus(X160,X159) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(81, 0), 0)'])])]) ).
fof(i_0_52,plain,
! [X128,X129] :
( ~ greater(X128,X129)
| ~ less(X128,X129) ),
inference(variable_rename,[status(thm)],[i_0_33]) ).
cnf(i_0_53,plain,
( X1 = X2
| vsucc(X1) != vsucc(X2) ),
inference(split_conjunct,[status(thm)],[i_0_34]) ).
cnf(i_0_54,plain,
( X1 = X2
| vsucc(X1) != vsucc(X2) ),
inference(split_conjunct,[status(thm)],[i_0_35]) ).
fof(i_0_55,plain,
! [X118,X119] :
( ( ~ geq(X119,X118)
| greater(X119,X118)
| X119 = X118 )
& ( ~ greater(X119,X118)
| geq(X119,X118) )
& ( X119 != X118
| geq(X119,X118) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['def(cond(conseq(axiom(3)), 16), 1)'])])]) ).
fof(i_0_56,plain,
! [X116,X117] :
( ( ~ leq(X117,X116)
| less(X117,X116)
| X117 = X116 )
& ( ~ less(X117,X116)
| leq(X117,X116) )
& ( X117 != X116
| leq(X117,X116) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['def(cond(conseq(axiom(3)), 17), 1)'])])]) ).
fof(i_0_57,plain,
! [X120,X121] :
( ~ less(X120,X121)
| greater(X121,X120) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(147, 0), 0)'])]) ).
fof(i_0_58,plain,
! [X112,X113] :
( ~ leq(X112,X113)
| geq(X113,X112) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(163, 0), 0)'])]) ).
fof(i_0_59,plain,
! [X114,X115] :
( ~ geq(X114,X115)
| leq(X115,X114) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(158, 0), 0)'])]) ).
fof(i_0_60,plain,
! [X122,X123] :
( ~ greater(X122,X123)
| less(X123,X122) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(140, 0), 0)'])]) ).
fof(i_0_61,plain,
! [X124,X125] :
( X124 = X125
| greater(X124,X125)
| less(X124,X125) ),
inference(variable_rename,[status(thm)],['ass(cond(goal(130), 0), 0)']) ).
fof(i_0_62,plain,
! [X163,X164] : vplus(X164,X163) = vplus(X163,X164),
inference(variable_rename,[status(thm)],['ass(cond(61, 0), 0)']) ).
fof(i_0_63,plain,
! [X155,X156,X157] :
( X155 != X156
| X155 != vplus(X156,X157) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 3)'])])]) ).
fof(i_0_64,plain,
! [X148,X149,X150] :
( X148 != X149
| X149 != vplus(X148,X150) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 1)'])])]) ).
fof(i_0_65,plain,
! [X130,X131] :
( X130 != X131
| ~ greater(X130,X131) ),
inference(variable_rename,[status(thm)],[i_0_36]) ).
fof(i_0_66,plain,
! [X126,X127] :
( X126 != X127
| ~ less(X126,X127) ),
inference(variable_rename,[status(thm)],[i_0_37]) ).
cnf(i_0_67,plain,
vplus(v1,X1) = vsucc(X1),
inference(split_conjunct,[status(thm)],[i_0_38]) ).
fof(i_0_68,plain,
! [X161,X162] : X162 != vplus(X161,X162),
inference(variable_rename,[status(thm)],['ass(cond(73, 0), 0)']) ).
cnf(i_0_69,plain,
vsucc(X1) != X1,
inference(split_conjunct,[status(thm)],[i_0_39]) ).
cnf(i_0_70,plain,
( X1 = v1
| X1 = vsucc(vskolem2(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_40]) ).
cnf(i_0_71,plain,
vsucc(X1) != v1,
inference(split_conjunct,[status(thm)],[i_0_41]) ).
fof(i_0_72,negated_conjecture,
! [X111] : vd269 != vplus(vd268,X111),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_42])]) ).
cnf(i_0_73,plain,
( X1 = X2
| X1 = vplus(X2,esk3_2(X1,X2))
| X2 = vplus(X1,esk4_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_74,plain,
vplus(vplus(X1,X2),X3) = vplus(X1,vplus(X2,X3)),
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_75,plain,
vplus(vplus(X1,v1),X2) = vplus(vplus(X1,X2),v1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_45,c_0_46]),c_0_46]),
[final] ).
cnf(i_0_76,plain,
vplus(X1,vplus(X2,v1)) = vplus(vplus(X1,X2),v1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_47,c_0_46]),c_0_46]),
[final] ).
cnf(i_0_77,plain,
( X1 = vplus(X2,esk2_2(X2,X1))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_78,plain,
( X2 = vplus(X1,esk1_2(X2,X1))
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_79,plain,
( X1 != vplus(X2,X3)
| X2 != vplus(X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_80,plain,
( X1 = X2
| vplus(X3,X1) != vplus(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_81,plain,
( ~ greater(X1,X2)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_82,plain,
( X1 = X2
| vplus(X1,v1) != vplus(X2,v1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_53,c_0_46]),c_0_46]),
[final] ).
cnf(i_0_83,plain,
( X1 = X2
| vplus(X1,v1) != vplus(X2,v1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_54,c_0_46]),c_0_46]),
[final] ).
cnf(i_0_84,plain,
( greater(X1,X2)
| X1 = X2
| ~ geq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_85,plain,
( less(X1,X2)
| X1 = X2
| ~ leq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_86,plain,
( greater(X1,X2)
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_87,plain,
( less(X2,X1)
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_88,plain,
( greater(X2,X1)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_89,plain,
( geq(X1,X2)
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_90,plain,
( geq(X2,X1)
| ~ leq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_91,plain,
( leq(X1,X2)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_92,plain,
( leq(X2,X1)
| ~ geq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_93,plain,
( less(X2,X1)
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_94,plain,
( X1 = X2
| greater(X1,X2)
| less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_95,plain,
vplus(X1,X2) = vplus(X2,X1),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_96,plain,
( X1 != X2
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_97,plain,
( X1 != X2
| X2 != vplus(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_98,plain,
( X1 != X2
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_99,plain,
( X1 != X2
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_100,plain,
vplus(v1,X1) = vplus(X1,v1),
inference(rw,[status(thm)],[i_0_67,c_0_46]),
[final] ).
cnf(i_0_101,plain,
X1 != vplus(X2,X1),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_102,plain,
vplus(X1,v1) != X1,
inference(rw,[status(thm)],[i_0_69,c_0_46]),
[final] ).
cnf(i_0_103,plain,
( X1 = v1
| X1 = vplus(vskolem2(X1),v1) ),
inference(rw,[status(thm)],[i_0_70,c_0_46]),
[final] ).
cnf(i_0_104,plain,
vplus(X1,v1) != v1,
inference(rw,[status(thm)],[i_0_71,c_0_46]),
[final] ).
cnf(i_0_105,negated_conjecture,
vd269 != vplus(vd268,X1),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_106,plain,
( geq(X1,X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_107,plain,
( leq(X1,X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_108,plain,
less(vd268,vd269),
inference(split_conjunct,[status(thm)],['holds(conjunct1(170), 270, 0)']),
[final] ).
cnf(i_0_109,plain,
less(vd269,vd271),
inference(split_conjunct,[status(thm)],['holds(conjunct2(170), 272, 0)']),
[final] ).
cnf(i_0_110,axiom,
X1 = X1 ).
cnf(i_0_111,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_112,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_113,axiom,
( X1 != X2
| vplus(X1,X3) = vplus(X2,X3) ) ).
cnf(i_0_114,axiom,
( X1 != X2
| vplus(X3,X1) = vplus(X3,X2) ) ).
cnf(i_0_115,axiom,
( X1 != X2
| ~ greater(X1,X3)
| greater(X2,X3) ) ).
cnf(i_0_116,axiom,
( X1 != X2
| ~ greater(X3,X1)
| greater(X3,X2) ) ).
cnf(i_0_117,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_118,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_119,axiom,
( X1 != X2
| ~ geq(X1,X3)
| geq(X2,X3) ) ).
cnf(i_0_120,axiom,
( X1 != X2
| ~ geq(X3,X1)
| geq(X3,X2) ) ).
cnf(i_0_121,axiom,
( X1 != X2
| ~ leq(X1,X3)
| leq(X2,X3) ) ).
cnf(i_0_122,axiom,
( X1 != X2
| ~ leq(X3,X1)
| leq(X3,X2) ) ).
cnf(i_0_110_001,axiom,
X1 = X1 ).
cnf(i_0_111_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_112_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_113_004,axiom,
( X1 != X2
| vplus(X1,X3) = vplus(X2,X3) ) ).
cnf(i_0_114_005,axiom,
( X1 != X2
| vplus(X3,X1) = vplus(X3,X2) ) ).
cnf(i_0_115_006,axiom,
( X1 != X2
| ~ greater(X1,X3)
| greater(X2,X3) ) ).
cnf(i_0_116_007,axiom,
( X1 != X2
| ~ greater(X3,X1)
| greater(X3,X2) ) ).
cnf(i_0_117_008,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_118_009,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_119_010,axiom,
( X1 != X2
| ~ geq(X1,X3)
| geq(X2,X3) ) ).
cnf(i_0_120_011,axiom,
( X1 != X2
| ~ geq(X3,X1)
| geq(X3,X2) ) ).
cnf(i_0_121_012,axiom,
( X1 != X2
| ~ leq(X1,X3)
| leq(X2,X3) ) ).
cnf(i_0_122_013,axiom,
( X1 != X2
| ~ leq(X3,X1)
| leq(X3,X2) ) ).
cnf(i_0_123,plain,
X1 = X1,
inference(equality_inference,[],[80]) ).
cnf(i_0_124,plain,
X1 = X1,
inference(equality_inference,[],[83]) ).
cnf(i_0_125,plain,
greater(vplus(X1,X2),X1),
inference(equality_inference,[],[86]) ).
cnf(i_0_126,plain,
less(X1,vplus(X1,X2)),
inference(equality_inference,[],[87]) ).
cnf(i_0_127,plain,
~ greater(X1,X1),
inference(equality_inference,[],[98]) ).
cnf(i_0_128,plain,
~ less(X1,X1),
inference(equality_inference,[],[99]) ).
cnf(i_0_129,plain,
geq(X1,X1),
inference(equality_inference,[],[106]) ).
cnf(i_0_130,plain,
leq(X1,X1),
inference(equality_inference,[],[107]) ).
cnf(i_0_131,plain,
$false,
inference(scs_inference,[],[i_0_105,i_0_108,i_0_78]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.13 % Problem : NUM837+1 : TPTP v9.2.1. Released v4.1.0.
% 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n031.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 01:17:08 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.35 % start to proof: theBenchmark
% 0.28/1.62 % Version : CSE_E---1.7
% 0.28/1.62 % Problem : theBenchmark.p
% 0.28/1.62 % SZS status Theorem for theBenchmark.p
% 0.28/1.62 % SZS output start CNFRefutation
% See solution above
% 0.28/1.64 % Total time : 1.271s
%------------------------------------------------------------------------------