%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM838+2 : TPTP v9.2.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n016.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_45)
% Comments :
%------------------------------------------------------------------------------
fof('ass(cond(52, 0), 0)',axiom,
! [X31,X32] : vplus(vsucc(X31),X32) = vsucc(vplus(X31,X32)),
file('/export/starexec/sandbox/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,
! [X36,X37] :
( vplus(X36,vsucc(X37)) = vsucc(vplus(X36,X37))
& vplus(X36,v1) = vsucc(X36) ),
file('/export/starexec/sandbox/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,
! [X17,X18] :
( ~ greater(X17,X18)
| ~ less(X17,X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 2)') ).
fof('ass(cond(goal(130), 0), 1)',axiom,
! [X17,X18] :
( X17 != X18
| ~ less(X17,X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 1)') ).
fof('ass(cond(goal(130), 0), 3)',axiom,
! [X17,X18] :
( X17 != X18
| ~ greater(X17,X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 3)') ).
fof('ass(cond(proof(196), 0), 7)',axiom,
! [X1,X6,X7] :
( greater(X6,X7)
=> vplus(vplus(X7,vskolem7(X6,X7)),X1) = vplus(vplus(vskolem7(X6,X7),X7),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(proof(196), 0), 7)') ).
fof('ass(cond(proof(196), 0), 6)',axiom,
! [X1,X6,X7] :
( greater(X6,X7)
=> vplus(vplus(vskolem7(X6,X7),X7),X1) = vplus(vskolem7(X6,X7),vplus(X7,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(proof(196), 0), 6)') ).
fof('ass(cond(proof(196), 0), 5)',axiom,
! [X1,X6,X7] :
( greater(X6,X7)
=> vplus(vskolem7(X6,X7),vplus(X7,X1)) = vplus(vplus(X7,X1),vskolem7(X6,X7)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(proof(196), 0), 5)') ).
fof('ass(cond(proof(196), 0), 8)',axiom,
! [X1,X6,X7] :
( greater(X6,X7)
=> vplus(X6,X1) = vplus(vplus(X7,vskolem7(X6,X7)),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(proof(196), 0), 8)') ).
fof('ass(cond(proof(196), 0), 0)',axiom,
! [X1,X2,X3] :
( less(X2,X3)
=> less(vplus(X2,X1),vplus(X3,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(proof(196), 0), 0)') ).
fof('ass(cond(proof(196), 0), 4)',axiom,
! [X1,X6,X7] :
( greater(X6,X7)
=> greater(vplus(X6,X1),vplus(X7,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(proof(196), 0), 4)') ).
fof('ass(cond(proof(196), 0), 1)',axiom,
! [X1,X2,X3] :
( less(X2,X3)
=> greater(vplus(X3,X1),vplus(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(proof(196), 0), 1)') ).
fof('holds(conseq(195), 305, 0)',conjecture,
greater(vplus(vd301,vd303),vplus(vd302,vd303)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conseq(195), 305, 0)') ).
fof('ass(cond(goal(88), 0), 0)',axiom,
! [X25,X26] :
( X25 = X26
| ? [X27] : X25 = vplus(X26,X27)
| ? [X28] : X26 = vplus(X25,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 0)') ).
fof('ass(cond(33, 0), 0)',axiom,
! [X33,X34,X35] : vplus(vplus(X33,X34),X35) = vplus(X33,vplus(X34,X35)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(33, 0), 0)') ).
fof('def(cond(conseq(axiom(3)), 11), 1)',axiom,
! [X22,X23] :
( greater(X23,X22)
<=> ? [X24] : X23 = vplus(X22,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 11), 1)') ).
fof('ass(cond(proof(196), 0), 9)',axiom,
! [X1,X6,X7] :
( greater(X6,X7)
=> X6 = vplus(X7,vskolem7(X6,X7)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(proof(196), 0), 9)') ).
fof('def(cond(conseq(axiom(3)), 12), 1)',axiom,
! [X19,X20] :
( less(X20,X19)
<=> ? [X21] : X19 = vplus(X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 12), 1)') ).
fof('ass(cond(184, 0), 0)',axiom,
! [X10,X11,X12] :
( ( leq(X11,X12)
& leq(X10,X11) )
=> leq(X10,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(184, 0), 0)') ).
fof('ass(cond(goal(88), 0), 2)',axiom,
! [X25,X26] :
( ~ ? [X27] : X25 = vplus(X26,X27)
| ~ ? [X28] : X26 = vplus(X25,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 2)') ).
fof('ass(cond(189, 0), 0)',axiom,
! [X8,X9] : greater(vplus(X8,X9),X8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(189, 0), 0)') ).
fof('ass(cond(140, 0), 0)',axiom,
! [X15,X16] :
( greater(X15,X16)
=> less(X16,X15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(140, 0), 0)') ).
fof('ass(cond(147, 0), 0)',axiom,
! [X13,X14] :
( less(X13,X14)
=> greater(X14,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(147, 0), 0)') ).
fof('ass(cond(proof(196), 0), 2)',axiom,
! [X1,X2,X3] :
( less(X2,X3)
=> greater(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(proof(196), 0), 2)') ).
fof('ass(cond(goal(130), 0), 0)',axiom,
! [X17,X18] :
( X17 = X18
| greater(X17,X18)
| less(X17,X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 0)') ).
fof('ass(cond(61, 0), 0)',axiom,
! [X29,X30] : vplus(X30,X29) = vplus(X29,X30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(61, 0), 0)') ).
fof('ass(cond(goal(88), 0), 3)',axiom,
! [X25,X26] :
( X25 != X26
| ~ ? [X27] : X25 = vplus(X26,X27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 3)') ).
fof('ass(cond(goal(88), 0), 1)',axiom,
! [X25,X26] :
( X25 != X26
| ~ ? [X28] : X26 = vplus(X25,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 1)') ).
fof('holds(antec(195), 304, 0)',axiom,
greater(vd301,vd302),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(antec(195), 304, 0)') ).
fof(i_0_29,plain,
! [X187,X188] : vplus(vsucc(X187),X188) = vsucc(vplus(X187,X188)),
inference(variable_rename,[status(thm)],['ass(cond(52, 0), 0)']) ).
fof(i_0_30,plain,
! [X192,X193] :
( vplus(X192,vsucc(X193)) = vsucc(vplus(X192,X193))
& vplus(X192,v1) = vsucc(X192) ),
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_31,plain,
! [X17,X18] :
( ~ greater(X17,X18)
| ~ less(X17,X18) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 2)']) ).
fof(i_0_32,plain,
! [X17,X18] :
( X17 != X18
| ~ less(X17,X18) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 1)']) ).
fof(i_0_33,plain,
! [X17,X18] :
( X17 != X18
| ~ greater(X17,X18) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 3)']) ).
fof(i_0_34,plain,
! [X134,X135,X136] :
( ~ greater(X135,X136)
| vplus(vplus(X136,vskolem7(X135,X136)),X134) = vplus(vplus(vskolem7(X135,X136),X136),X134) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(proof(196), 0), 7)'])]) ).
fof(i_0_35,plain,
! [X131,X132,X133] :
( ~ greater(X132,X133)
| vplus(vplus(vskolem7(X132,X133),X133),X131) = vplus(vskolem7(X132,X133),vplus(X133,X131)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(proof(196), 0), 6)'])]) ).
fof(i_0_36,plain,
! [X128,X129,X130] :
( ~ greater(X129,X130)
| vplus(vskolem7(X129,X130),vplus(X130,X128)) = vplus(vplus(X130,X128),vskolem7(X129,X130)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(proof(196), 0), 5)'])]) ).
fof(i_0_37,plain,
! [X137,X138,X139] :
( ~ greater(X138,X139)
| vplus(X138,X137) = vplus(vplus(X139,vskolem7(X138,X139)),X137) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(proof(196), 0), 8)'])]) ).
fof(i_0_38,plain,
! [X114,X115,X116] :
( ~ less(X115,X116)
| less(vplus(X115,X114),vplus(X116,X114)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(proof(196), 0), 0)'])]) ).
fof(i_0_39,plain,
! [X125,X126,X127] :
( ~ greater(X126,X127)
| greater(vplus(X126,X125),vplus(X127,X125)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(proof(196), 0), 4)'])]) ).
fof(i_0_40,plain,
! [X117,X118,X119] :
( ~ less(X118,X119)
| greater(vplus(X119,X117),vplus(X118,X117)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(proof(196), 0), 1)'])]) ).
fof(i_0_41,negated_conjecture,
~ greater(vplus(vd301,vd303),vplus(vd302,vd303)),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],['holds(conseq(195), 305, 0)'])]) ).
fof(i_0_42,plain,
! [X171,X172] :
( X171 = X172
| X171 = vplus(X172,esk3_2(X171,X172))
| X172 = vplus(X171,esk4_2(X171,X172)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['ass(cond(goal(88), 0), 0)'])]) ).
fof(i_0_43,plain,
! [X189,X190,X191] : vplus(vplus(X189,X190),X191) = vplus(X189,vplus(X190,X191)),
inference(variable_rename,[status(thm)],['ass(cond(33, 0), 0)']) ).
cnf(i_0_44,plain,
vplus(vsucc(X1),X2) = vsucc(vplus(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_29]) ).
cnf(i_0_45,plain,
vplus(X1,v1) = vsucc(X1),
inference(split_conjunct,[status(thm)],[i_0_30]) ).
cnf(i_0_46,plain,
vplus(X1,vsucc(X2)) = vsucc(vplus(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_30]) ).
fof(i_0_47,plain,
! [X165,X166,X168,X169,X170] :
( ( ~ greater(X166,X165)
| X166 = vplus(X165,esk2_2(X165,X166)) )
& ( X169 != vplus(X168,X170)
| greater(X169,X168) ) ),
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_48,plain,
! [X140,X141] :
( ~ greater(X140,X141)
| X140 = vplus(X141,vskolem7(X140,X141)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],['ass(cond(proof(196), 0), 9)'])])]) ).
fof(i_0_49,plain,
! [X159,X160,X162,X163,X164] :
( ( ~ less(X160,X159)
| X159 = vplus(X160,esk1_2(X159,X160)) )
& ( X162 != vplus(X163,X164)
| less(X163,X162) ) ),
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,
! [X144,X145,X146] :
( ~ leq(X145,X146)
| ~ leq(X144,X145)
| leq(X144,X146) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(184, 0), 0)'])]) ).
fof(i_0_51,plain,
! [X178,X179,X180,X181] :
( X178 != vplus(X179,X180)
| X179 != vplus(X178,X181) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 2)'])])]) ).
fof(i_0_52,plain,
! [X155,X156] :
( ~ greater(X155,X156)
| ~ less(X155,X156) ),
inference(variable_rename,[status(thm)],[i_0_31]) ).
fof(i_0_53,plain,
! [X142,X143] : greater(vplus(X142,X143),X142),
inference(variable_rename,[status(thm)],['ass(cond(189, 0), 0)']) ).
fof(i_0_54,plain,
! [X149,X150] :
( ~ greater(X149,X150)
| less(X150,X149) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(140, 0), 0)'])]) ).
fof(i_0_55,plain,
! [X147,X148] :
( ~ less(X147,X148)
| greater(X148,X147) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(147, 0), 0)'])]) ).
fof(i_0_56,plain,
! [X120,X121] :
( ~ less(X120,X121)
| greater(X121,X120) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],['ass(cond(proof(196), 0), 2)'])])]) ).
fof(i_0_57,plain,
! [X151,X152] :
( X151 = X152
| greater(X151,X152)
| less(X151,X152) ),
inference(variable_rename,[status(thm)],['ass(cond(goal(130), 0), 0)']) ).
fof(i_0_58,plain,
! [X185,X186] : vplus(X186,X185) = vplus(X185,X186),
inference(variable_rename,[status(thm)],['ass(cond(61, 0), 0)']) ).
fof(i_0_59,plain,
! [X182,X183,X184] :
( X182 != X183
| X182 != vplus(X183,X184) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 3)'])])]) ).
fof(i_0_60,plain,
! [X175,X176,X177] :
( X175 != X176
| X176 != vplus(X175,X177) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 1)'])])]) ).
fof(i_0_61,plain,
! [X153,X154] :
( X153 != X154
| ~ less(X153,X154) ),
inference(variable_rename,[status(thm)],[i_0_32]) ).
fof(i_0_62,plain,
! [X157,X158] :
( X157 != X158
| ~ greater(X157,X158) ),
inference(variable_rename,[status(thm)],[i_0_33]) ).
cnf(i_0_63,plain,
( vplus(vplus(X2,vskolem7(X1,X2)),X3) = vplus(vplus(vskolem7(X1,X2),X2),X3)
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_64,plain,
( vplus(vplus(vskolem7(X1,X2),X2),X3) = vplus(vskolem7(X1,X2),vplus(X2,X3))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_65,plain,
( vplus(vskolem7(X1,X2),vplus(X2,X3)) = vplus(vplus(X2,X3),vskolem7(X1,X2))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_66,plain,
( vplus(X1,X3) = vplus(vplus(X2,vskolem7(X1,X2)),X3)
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_67,plain,
( less(vplus(X1,X3),vplus(X2,X3))
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_38]),
[final] ).
cnf(i_0_68,plain,
( greater(vplus(X1,X3),vplus(X2,X3))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_69,plain,
( greater(vplus(X2,X3),vplus(X1,X3))
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_70,negated_conjecture,
~ greater(vplus(vd301,vd303),vplus(vd302,vd303)),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_71,plain,
( X1 = X2
| X1 = vplus(X2,esk3_2(X1,X2))
| X2 = vplus(X1,esk4_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_72,plain,
vplus(vplus(X1,X2),X3) = vplus(X1,vplus(X2,X3)),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_73,plain,
vplus(vplus(X1,v1),X2) = vplus(vplus(X1,X2),v1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_44,c_0_45]),c_0_45]),
[final] ).
cnf(i_0_74,plain,
vplus(X1,vplus(X2,v1)) = vplus(vplus(X1,X2),v1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_46,c_0_45]),c_0_45]),
[final] ).
cnf(i_0_75,plain,
( X1 = vplus(X2,esk2_2(X2,X1))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_76,plain,
( X1 = vplus(X2,vskolem7(X1,X2))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_77,plain,
( X2 = vplus(X1,esk1_2(X2,X1))
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_78,plain,
( leq(X3,X2)
| ~ leq(X1,X2)
| ~ leq(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_79,plain,
( X1 != vplus(X2,X3)
| X2 != vplus(X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_80,plain,
( ~ greater(X1,X2)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_81,plain,
greater(vplus(X1,X2),X1),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_82,plain,
( less(X2,X1)
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_83,plain,
( greater(X1,X2)
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_84,plain,
( less(X2,X1)
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_85,plain,
( greater(X2,X1)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_86,plain,
( greater(X2,X1)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_87,plain,
( X1 = X2
| greater(X1,X2)
| less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_88,plain,
vplus(X1,X2) = vplus(X2,X1),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_89,plain,
( X1 != X2
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_90,plain,
( X1 != X2
| X2 != vplus(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_91,plain,
( X1 != X2
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_92,plain,
( X1 != X2
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_93,plain,
greater(vd301,vd302),
inference(split_conjunct,[status(thm)],['holds(antec(195), 304, 0)']),
[final] ).
cnf(i_0_94,axiom,
X1 = X1 ).
cnf(i_0_95,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_96,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_97,axiom,
( X1 != X2
| vplus(X1,X3) = vplus(X2,X3) ) ).
cnf(i_0_98,axiom,
( X1 != X2
| vplus(X3,X1) = vplus(X3,X2) ) ).
cnf(i_0_99,axiom,
( X1 != X2
| ~ greater(X1,X3)
| greater(X2,X3) ) ).
cnf(i_0_100,axiom,
( X1 != X2
| ~ greater(X3,X1)
| greater(X3,X2) ) ).
cnf(i_0_101,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_102,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_103,axiom,
( X1 != X2
| ~ leq(X1,X3)
| leq(X2,X3) ) ).
cnf(i_0_104,axiom,
( X1 != X2
| ~ leq(X3,X1)
| leq(X3,X2) ) ).
cnf(i_0_94_001,axiom,
X1 = X1 ).
cnf(i_0_95_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_96_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_97_004,axiom,
( X1 != X2
| vplus(X1,X3) = vplus(X2,X3) ) ).
cnf(i_0_98_005,axiom,
( X1 != X2
| vplus(X3,X1) = vplus(X3,X2) ) ).
cnf(i_0_99_006,axiom,
( X1 != X2
| ~ greater(X1,X3)
| greater(X2,X3) ) ).
cnf(i_0_100_007,axiom,
( X1 != X2
| ~ greater(X3,X1)
| greater(X3,X2) ) ).
cnf(i_0_101_008,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_102_009,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_103_010,axiom,
( X1 != X2
| ~ leq(X1,X3)
| leq(X2,X3) ) ).
cnf(i_0_104_011,axiom,
( X1 != X2
| ~ leq(X3,X1)
| leq(X3,X2) ) ).
cnf(i_0_105,plain,
less(X1,vplus(X1,X2)),
inference(equality_inference,[],[82]) ).
cnf(i_0_106,plain,
greater(vplus(X1,X2),X1),
inference(equality_inference,[],[83]) ).
cnf(i_0_107,plain,
~ less(X1,X1),
inference(equality_inference,[],[91]) ).
cnf(i_0_108,plain,
~ greater(X1,X1),
inference(equality_inference,[],[92]) ).
cnf(i_0_109,plain,
$false,
inference(scs_inference,[],[i_0_70,i_0_93,i_0_68]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM838+2 : TPTP v9.2.1. Released v4.1.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n016.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:15:36 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % 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.63 % Total time : 1.271s
%------------------------------------------------------------------------------