%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM840+2 : 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 : n004.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:41 PM UTC 2026
% Result : Theorem 0.45s 1.61s
% Output : CNFRefutation 0.66s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_37)
% Comments :
%------------------------------------------------------------------------------
fof('ass(cond(52, 0), 0)',axiom,
! [X27,X28] : vplus(vsucc(X27),X28) = vsucc(vplus(X27,X28)),
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,
! [X33,X34] :
( vplus(X33,vsucc(X34)) = vsucc(vplus(X33,X34))
& vplus(X33,v1) = vsucc(X33) ),
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,
! [X8,X9] :
( ~ greater(X8,X9)
| ~ less(X8,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 2)') ).
fof('ass(cond(goal(130), 0), 3)',axiom,
! [X8,X9] :
( X8 != X9
| ~ greater(X8,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 3)') ).
fof('ass(cond(goal(130), 0), 1)',axiom,
! [X8,X9] :
( X8 != X9
| ~ less(X8,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 1)') ).
fof('ass(cond(43, 0), 0)',axiom,
! [X29] : vplus(v1,X29) = vsucc(X29),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(43, 0), 0)') ).
fof('ass(cond(conjunct1(204), 0), 0)',axiom,
( greater(vplus(vd328,vd330),vplus(vd329,vd330))
=> greater(vd328,vd329) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(conjunct1(204), 0), 0)') ).
fof('ass(cond(goal(193), 0), 2)',axiom,
! [X1,X2,X3] :
( greater(X1,X2)
=> greater(vplus(X1,X3),vplus(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(193), 0), 2)') ).
fof('ass(cond(goal(193), 0), 0)',axiom,
! [X1,X2,X3] :
( less(X1,X2)
=> less(vplus(X1,X3),vplus(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(193), 0), 0)') ).
fof('ass(cond(goal(88), 0), 0)',axiom,
! [X16,X17] :
( X16 = X17
| ? [X18] : X16 = vplus(X17,X18)
| ? [X19] : X17 = vplus(X16,X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 0)') ).
fof('ass(cond(33, 0), 0)',axiom,
! [X30,X31,X32] : vplus(vplus(X30,X31),X32) = vplus(X30,vplus(X31,X32)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(33, 0), 0)') ).
fof('def(cond(conseq(axiom(3)), 11), 1)',axiom,
! [X13,X14] :
( greater(X14,X13)
<=> ? [X15] : X14 = vplus(X13,X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 11), 1)') ).
fof('def(cond(conseq(axiom(3)), 12), 1)',axiom,
! [X10,X11] :
( less(X11,X10)
<=> ? [X12] : X10 = vplus(X11,X12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 12), 1)') ).
fof('ass(cond(goal(88), 0), 2)',axiom,
! [X16,X17] :
( ~ ? [X18] : X16 = vplus(X17,X18)
| ~ ? [X19] : X17 = vplus(X16,X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 2)') ).
fof('ass(cond(81, 0), 0)',axiom,
! [X20,X21] :
( X20 != X21
=> ! [X22] : vplus(X22,X20) != vplus(X22,X21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(81, 0), 0)') ).
fof('ass(cond(147, 0), 0)',axiom,
! [X4,X5] :
( less(X4,X5)
=> greater(X5,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(147, 0), 0)') ).
fof('ass(cond(140, 0), 0)',axiom,
! [X6,X7] :
( greater(X6,X7)
=> less(X7,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(140, 0), 0)') ).
fof('ass(cond(conjunct1(conjunct2(204)), 0), 0)',axiom,
( vplus(vd328,vd330) = vplus(vd329,vd330)
=> vd328 = vd329 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(conjunct1(conjunct2(204)), 0), 0)') ).
fof('ass(cond(goal(130), 0), 0)',axiom,
! [X8,X9] :
( X8 = X9
| greater(X8,X9)
| less(X8,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 0)') ).
fof('ass(cond(61, 0), 0)',axiom,
! [X25,X26] : vplus(X26,X25) = vplus(X25,X26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(61, 0), 0)') ).
fof('ass(cond(goal(88), 0), 3)',axiom,
! [X16,X17] :
( X16 != X17
| ~ ? [X18] : X16 = vplus(X17,X18) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 3)') ).
fof('ass(cond(goal(88), 0), 1)',axiom,
! [X16,X17] :
( X16 != X17
| ~ ? [X19] : X17 = vplus(X16,X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 1)') ).
fof('ass(cond(73, 0), 0)',axiom,
! [X23,X24] : X24 != vplus(X23,X24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(73, 0), 0)') ).
fof('holds(conseq(conjunct2(conjunct2(204))), 336, 0)',conjecture,
less(vd328,vd329),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conseq(conjunct2(conjunct2(204))), 336, 0)') ).
fof('holds(antec(conjunct2(conjunct2(204))), 335, 0)',axiom,
less(vplus(vd328,vd330),vplus(vd329,vd330)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(antec(conjunct2(conjunct2(204))), 335, 0)') ).
fof(i_0_25,plain,
! [X145,X146] : vplus(vsucc(X145),X146) = vsucc(vplus(X145,X146)),
inference(variable_rename,[status(thm)],['ass(cond(52, 0), 0)']) ).
fof(i_0_26,plain,
! [X151,X152] :
( vplus(X151,vsucc(X152)) = vsucc(vplus(X151,X152))
& vplus(X151,v1) = vsucc(X151) ),
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_27,plain,
! [X8,X9] :
( ~ greater(X8,X9)
| ~ less(X8,X9) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 2)']) ).
fof(i_0_28,plain,
! [X8,X9] :
( X8 != X9
| ~ greater(X8,X9) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 3)']) ).
fof(i_0_29,plain,
! [X8,X9] :
( X8 != X9
| ~ less(X8,X9) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 1)']) ).
fof(i_0_30,plain,
! [X147] : vplus(v1,X147) = vsucc(X147),
inference(variable_rename,[status(thm)],['ass(cond(43, 0), 0)']) ).
fof(i_0_31,plain,
( ~ greater(vplus(vd328,vd330),vplus(vd329,vd330))
| greater(vd328,vd329) ),
inference(fof_nnf,[status(thm)],['ass(cond(conjunct1(204), 0), 0)']) ).
fof(i_0_32,plain,
! [X97,X98,X99] :
( ~ greater(X97,X98)
| greater(vplus(X97,X99),vplus(X98,X99)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(193), 0), 2)'])]) ).
fof(i_0_33,plain,
! [X91,X92,X93] :
( ~ less(X91,X92)
| less(vplus(X91,X93),vplus(X92,X93)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(193), 0), 0)'])]) ).
fof(i_0_34,plain,
! [X124,X125] :
( X124 = X125
| X124 = vplus(X125,esk3_2(X124,X125))
| X125 = vplus(X124,esk4_2(X124,X125)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['ass(cond(goal(88), 0), 0)'])]) ).
fof(i_0_35,plain,
! [X148,X149,X150] : vplus(vplus(X148,X149),X150) = vplus(X148,vplus(X149,X150)),
inference(variable_rename,[status(thm)],['ass(cond(33, 0), 0)']) ).
cnf(i_0_36,plain,
vplus(vsucc(X1),X2) = vsucc(vplus(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_25]) ).
cnf(i_0_37,plain,
vplus(X1,v1) = vsucc(X1),
inference(split_conjunct,[status(thm)],[i_0_26]) ).
cnf(i_0_38,plain,
vplus(X1,vsucc(X2)) = vsucc(vplus(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_26]) ).
fof(i_0_39,plain,
! [X118,X119,X121,X122,X123] :
( ( ~ greater(X119,X118)
| X119 = vplus(X118,esk2_2(X118,X119)) )
& ( X122 != vplus(X121,X123)
| greater(X122,X121) ) ),
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_40,plain,
! [X112,X113,X115,X116,X117] :
( ( ~ less(X113,X112)
| X112 = vplus(X113,esk1_2(X112,X113)) )
& ( X115 != vplus(X116,X117)
| less(X116,X115) ) ),
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_41,plain,
! [X131,X132,X133,X134] :
( X131 != vplus(X132,X133)
| X132 != vplus(X131,X134) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 2)'])])]) ).
fof(i_0_42,plain,
! [X138,X139,X140] :
( X138 = X139
| vplus(X140,X138) != vplus(X140,X139) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(81, 0), 0)'])])]) ).
fof(i_0_43,plain,
! [X108,X109] :
( ~ greater(X108,X109)
| ~ less(X108,X109) ),
inference(variable_rename,[status(thm)],[i_0_27]) ).
fof(i_0_44,plain,
! [X100,X101] :
( ~ less(X100,X101)
| greater(X101,X100) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(147, 0), 0)'])]) ).
fof(i_0_45,plain,
! [X102,X103] :
( ~ greater(X102,X103)
| less(X103,X102) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(140, 0), 0)'])]) ).
fof(i_0_46,plain,
( vplus(vd328,vd330) != vplus(vd329,vd330)
| vd328 = vd329 ),
inference(fof_nnf,[status(thm)],['ass(cond(conjunct1(conjunct2(204)), 0), 0)']) ).
fof(i_0_47,plain,
! [X104,X105] :
( X104 = X105
| greater(X104,X105)
| less(X104,X105) ),
inference(variable_rename,[status(thm)],['ass(cond(goal(130), 0), 0)']) ).
fof(i_0_48,plain,
! [X143,X144] : vplus(X144,X143) = vplus(X143,X144),
inference(variable_rename,[status(thm)],['ass(cond(61, 0), 0)']) ).
fof(i_0_49,plain,
! [X135,X136,X137] :
( X135 != X136
| X135 != vplus(X136,X137) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 3)'])])]) ).
fof(i_0_50,plain,
! [X128,X129,X130] :
( X128 != X129
| X129 != vplus(X128,X130) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 1)'])])]) ).
fof(i_0_51,plain,
! [X110,X111] :
( X110 != X111
| ~ greater(X110,X111) ),
inference(variable_rename,[status(thm)],[i_0_28]) ).
fof(i_0_52,plain,
! [X106,X107] :
( X106 != X107
| ~ less(X106,X107) ),
inference(variable_rename,[status(thm)],[i_0_29]) ).
cnf(i_0_53,plain,
vplus(v1,X1) = vsucc(X1),
inference(split_conjunct,[status(thm)],[i_0_30]) ).
fof(i_0_54,plain,
! [X141,X142] : X142 != vplus(X141,X142),
inference(variable_rename,[status(thm)],['ass(cond(73, 0), 0)']) ).
fof(i_0_55,negated_conjecture,
~ less(vd328,vd329),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],['holds(conseq(conjunct2(conjunct2(204))), 336, 0)'])]) ).
cnf(i_0_56,plain,
( greater(vd328,vd329)
| ~ greater(vplus(vd328,vd330),vplus(vd329,vd330)) ),
inference(split_conjunct,[status(thm)],[i_0_31]),
[final] ).
cnf(i_0_57,plain,
( greater(vplus(X1,X3),vplus(X2,X3))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_58,plain,
( less(vplus(X1,X3),vplus(X2,X3))
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_59,plain,
( X1 = X2
| X1 = vplus(X2,esk3_2(X1,X2))
| X2 = vplus(X1,esk4_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_60,plain,
vplus(vplus(X1,X2),X3) = vplus(X1,vplus(X2,X3)),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_61,plain,
vplus(vplus(X1,v1),X2) = vplus(vplus(X1,X2),v1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_36,c_0_37]),c_0_37]),
[final] ).
cnf(i_0_62,plain,
vplus(X1,vplus(X2,v1)) = vplus(vplus(X1,X2),v1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_38,c_0_37]),c_0_37]),
[final] ).
cnf(i_0_63,plain,
( X1 = vplus(X2,esk2_2(X2,X1))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_64,plain,
( X2 = vplus(X1,esk1_2(X2,X1))
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_65,plain,
less(vplus(vd328,vd330),vplus(vd329,vd330)),
inference(split_conjunct,[status(thm)],['holds(antec(conjunct2(conjunct2(204))), 335, 0)']),
[final] ).
cnf(i_0_66,plain,
( X1 != vplus(X2,X3)
| X2 != vplus(X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_67,plain,
( X1 = X2
| vplus(X3,X1) != vplus(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_68,plain,
( ~ greater(X1,X2)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_69,plain,
( greater(X1,X2)
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_70,plain,
( less(X2,X1)
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_71,plain,
( greater(X2,X1)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_72,plain,
( less(X2,X1)
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_73,plain,
( vd328 = vd329
| vplus(vd328,vd330) != vplus(vd329,vd330) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_74,plain,
( X1 = X2
| greater(X1,X2)
| less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_75,plain,
vplus(X1,X2) = vplus(X2,X1),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_76,plain,
( X1 != X2
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_77,plain,
( X1 != X2
| X2 != vplus(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_78,plain,
( X1 != X2
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_79,plain,
( X1 != X2
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_80,plain,
vplus(v1,X1) = vplus(X1,v1),
inference(rw,[status(thm)],[i_0_53,c_0_37]),
[final] ).
cnf(i_0_81,plain,
X1 != vplus(X2,X1),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_82,negated_conjecture,
~ less(vd328,vd329),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_83,axiom,
X1 = X1 ).
cnf(i_0_84,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_85,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_86,axiom,
( X1 != X2
| vplus(X1,X3) = vplus(X2,X3) ) ).
cnf(i_0_87,axiom,
( X1 != X2
| vplus(X3,X1) = vplus(X3,X2) ) ).
cnf(i_0_88,axiom,
( X1 != X2
| ~ greater(X1,X3)
| greater(X2,X3) ) ).
cnf(i_0_89,axiom,
( X1 != X2
| ~ greater(X3,X1)
| greater(X3,X2) ) ).
cnf(i_0_90,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_91,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_83_001,axiom,
X1 = X1 ).
cnf(i_0_84_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_85_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_86_004,axiom,
( X1 != X2
| vplus(X1,X3) = vplus(X2,X3) ) ).
cnf(i_0_87_005,axiom,
( X1 != X2
| vplus(X3,X1) = vplus(X3,X2) ) ).
cnf(i_0_88_006,axiom,
( X1 != X2
| ~ greater(X1,X3)
| greater(X2,X3) ) ).
cnf(i_0_89_007,axiom,
( X1 != X2
| ~ greater(X3,X1)
| greater(X3,X2) ) ).
cnf(i_0_90_008,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_91_009,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_92,plain,
X1 = X1,
inference(equality_inference,[],[67]) ).
cnf(i_0_93,plain,
greater(vplus(X1,X2),X1),
inference(equality_inference,[],[69]) ).
cnf(i_0_94,plain,
less(X1,vplus(X1,X2)),
inference(equality_inference,[],[70]) ).
cnf(i_0_95,plain,
~ greater(X1,X1),
inference(equality_inference,[],[78]) ).
cnf(i_0_96,plain,
~ less(X1,X1),
inference(equality_inference,[],[79]) ).
cnf(i_0_97,plain,
less(X1,vplus(X2,X1)),
inference(scs_inference,[],[i_0_75,i_0_70]) ).
cnf(i_0_98,plain,
( X1 != vplus(X2,X3)
| less(X2,X1) ),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_99,plain,
X1 != vplus(vplus(X2,X1),X3),
inference(scs_inference,[],[i_0_75,i_0_70,i_0_66]) ).
cnf(i_0_100,plain,
( X1 != vplus(X2,X3)
| X2 != vplus(X1,X4) ),
inference(rename_variables,[],[i_0_66]) ).
cnf(i_0_101,plain,
~ greater(X1,vplus(X1,X2)),
inference(scs_inference,[],[i_0_94,i_0_75,i_0_70,i_0_66,i_0_68]) ).
cnf(i_0_102,plain,
( ~ less(X1,X2)
| ~ greater(X1,X2) ),
inference(rename_variables,[],[i_0_68]) ).
cnf(i_0_103,plain,
greater(vplus(X1,X2),X2),
inference(scs_inference,[],[i_0_94,i_0_75,i_0_70,i_0_66,i_0_68,i_0_69]) ).
cnf(i_0_104,plain,
( X1 != vplus(X2,X3)
| greater(X1,X2) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_105,plain,
greater(vplus(vd329,vd330),vplus(vd328,vd330)),
inference(scs_inference,[],[i_0_94,i_0_75,i_0_65,i_0_70,i_0_66,i_0_68,i_0_69,i_0_71]) ).
cnf(i_0_106,plain,
( ~ less(X1,X2)
| greater(X2,X1) ),
inference(rename_variables,[],[i_0_71]) ).
cnf(i_0_107,plain,
vplus(X1,X2) != X2,
inference(scs_inference,[],[i_0_94,i_0_75,i_0_65,i_0_70,i_0_66,i_0_68,i_0_69,i_0_71,i_0_76]) ).
cnf(i_0_108,plain,
( X1 != vplus(X2,X3)
| X1 != X2 ),
inference(rename_variables,[],[i_0_76]) ).
cnf(i_0_109,plain,
X1 != vplus(vplus(X1,X2),X3),
inference(scs_inference,[],[i_0_94,i_0_75,i_0_65,i_0_60,i_0_70,i_0_66,i_0_68,i_0_69,i_0_71,i_0_76,i_0_77]) ).
cnf(i_0_110,plain,
( X1 != vplus(X2,X3)
| X2 != X1 ),
inference(rename_variables,[],[i_0_77]) ).
cnf(i_0_111,plain,
vplus(X1,X2) != X1,
inference(scs_inference,[],[i_0_94,i_0_93,i_0_75,i_0_65,i_0_60,i_0_70,i_0_66,i_0_68,i_0_69,i_0_71,i_0_76,i_0_77,i_0_78]) ).
cnf(i_0_112,plain,
( ~ greater(X1,X2)
| X1 != X2 ),
inference(rename_variables,[],[i_0_78]) ).
cnf(i_0_113,plain,
X1 != vplus(X1,X2),
inference(scs_inference,[],[i_0_94,i_0_93,i_0_75,i_0_65,i_0_60,i_0_70,i_0_66,i_0_68,i_0_69,i_0_71,i_0_76,i_0_77,i_0_78,i_0_79]) ).
cnf(i_0_114,plain,
( ~ less(X1,X2)
| X1 != X2 ),
inference(rename_variables,[],[i_0_79]) ).
cnf(i_0_115,plain,
vplus(X1,vplus(X2,X3)) = vplus(vplus(X1,X2),X3),
inference(scs_inference,[],[i_0_94,i_0_93,i_0_75,i_0_65,i_0_60,i_0_70,i_0_66,i_0_68,i_0_69,i_0_71,i_0_76,i_0_77,i_0_78,i_0_79,i_0_84]) ).
cnf(i_0_116,plain,
X1 != vplus(X2,vplus(X1,X3)),
inference(scs_inference,[],[i_0_94,i_0_93,i_0_75,i_0_65,i_0_60,i_0_70,i_0_66,i_0_68,i_0_69,i_0_71,i_0_76,i_0_77,i_0_78,i_0_79,i_0_84,i_0_86]) ).
cnf(i_0_117,plain,
~ less(vplus(X1,vplus(X2,X3)),vplus(vplus(X2,X3),X1)),
inference(scs_inference,[],[i_0_94,i_0_96,i_0_93,i_0_75,i_0_65,i_0_60,i_0_70,i_0_66,i_0_68,i_0_69,i_0_71,i_0_76,i_0_77,i_0_78,i_0_79,i_0_84,i_0_86,i_0_90]) ).
cnf(i_0_118,plain,
~ less(X1,X1),
inference(rename_variables,[],[i_0_96]) ).
cnf(i_0_119,plain,
vplus(X1,X2) = vplus(X2,X1),
inference(rename_variables,[],[i_0_75]) ).
cnf(i_0_120,plain,
vplus(X1,X1) = vplus(X1,esk4_2(X1,vplus(X1,X1))),
inference(scs_inference,[],[i_0_94,i_0_96,i_0_93,i_0_75,i_0_81,i_0_65,i_0_60,i_0_70,i_0_66,i_0_68,i_0_69,i_0_71,i_0_76,i_0_77,i_0_78,i_0_79,i_0_84,i_0_86,i_0_90,i_0_59]) ).
cnf(i_0_121,plain,
X1 != vplus(X2,X1),
inference(rename_variables,[],[i_0_81]) ).
cnf(i_0_122,plain,
( X1 = vplus(X2,esk3_2(X1,X2))
| X2 = vplus(X1,esk4_2(X1,X2))
| X1 = X2 ),
inference(rename_variables,[],[i_0_59]) ).
cnf(i_0_123,plain,
v1 != vplus(X1,vplus(X2,v1)),
inference(scs_inference,[],[i_0_94,i_0_96,i_0_93,i_0_75,i_0_81,i_0_121,i_0_65,i_0_60,i_0_62,i_0_70,i_0_66,i_0_68,i_0_69,i_0_71,i_0_76,i_0_77,i_0_78,i_0_79,i_0_84,i_0_86,i_0_90,i_0_59,i_0_85]) ).
cnf(i_0_124,plain,
X1 != vplus(X2,X1),
inference(rename_variables,[],[i_0_81]) ).
cnf(i_0_125,plain,
~ greater(vplus(X1,X2),vplus(X2,X1)),
inference(scs_inference,[],[i_0_94,i_0_95,i_0_96,i_0_93,i_0_75,i_0_119,i_0_81,i_0_121,i_0_65,i_0_60,i_0_62,i_0_70,i_0_66,i_0_68,i_0_69,i_0_71,i_0_76,i_0_77,i_0_78,i_0_79,i_0_84,i_0_86,i_0_90,i_0_59,i_0_85,i_0_88]) ).
cnf(i_0_126,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_95]) ).
cnf(i_0_127,plain,
~ greater(X1,vplus(X2,X1)),
inference(scs_inference,[],[i_0_94,i_0_95,i_0_96,i_0_93,i_0_75,i_0_119,i_0_81,i_0_121,i_0_65,i_0_60,i_0_62,i_0_70,i_0_66,i_0_68,i_0_69,i_0_71,i_0_76,i_0_77,i_0_78,i_0_79,i_0_84,i_0_86,i_0_90,i_0_59,i_0_85,i_0_88,i_0_89]) ).
cnf(i_0_128,plain,
vplus(vd328,X1) != vd329,
inference(scs_inference,[],[i_0_82,i_0_94,i_0_95,i_0_96,i_0_93,i_0_75,i_0_119,i_0_81,i_0_121,i_0_65,i_0_60,i_0_62,i_0_70,i_0_66,i_0_68,i_0_69,i_0_71,i_0_76,i_0_77,i_0_78,i_0_79,i_0_84,i_0_86,i_0_90,i_0_59,i_0_85,i_0_88,i_0_89,i_0_91]) ).
cnf(i_0_129,plain,
less(X1,vplus(X1,X2)),
inference(rename_variables,[],[i_0_94]) ).
cnf(i_0_130,plain,
X1 = esk4_2(X1,vplus(X1,X1)),
inference(scs_inference,[],[i_0_82,i_0_94,i_0_95,i_0_96,i_0_93,i_0_75,i_0_119,i_0_81,i_0_121,i_0_65,i_0_60,i_0_62,i_0_70,i_0_66,i_0_68,i_0_69,i_0_71,i_0_76,i_0_77,i_0_78,i_0_79,i_0_84,i_0_86,i_0_90,i_0_59,i_0_85,i_0_88,i_0_89,i_0_91,i_0_67]) ).
cnf(i_0_131,plain,
( vplus(X1,X2) != vplus(X1,X3)
| X2 = X3 ),
inference(rename_variables,[],[i_0_67]) ).
cnf(i_0_132,plain,
~ less(vplus(X1,X2),X2),
inference(scs_inference,[],[i_0_99,i_0_64]) ).
cnf(i_0_133,plain,
X1 != vplus(vplus(X2,X1),X3),
inference(rename_variables,[],[i_0_99]) ).
cnf(i_0_134,plain,
( X1 = vplus(X2,esk1_2(X1,X2))
| ~ less(X2,X1) ),
inference(rename_variables,[],[i_0_64]) ).
cnf(i_0_135,plain,
less(vplus(X1,X2),vplus(X1,vplus(X2,X3))),
inference(scs_inference,[],[i_0_115,i_0_99,i_0_64,i_0_70]) ).
cnf(i_0_136,plain,
( X1 != vplus(X2,X3)
| less(X2,X1) ),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_137,plain,
vplus(X1,X2) != vplus(vplus(X1,vplus(X2,X3)),X4),
inference(scs_inference,[],[i_0_115,i_0_99,i_0_64,i_0_70,i_0_66]) ).
cnf(i_0_138,plain,
( X1 != vplus(X2,X3)
| X2 != vplus(X1,X4) ),
inference(rename_variables,[],[i_0_66]) ).
cnf(i_0_139,plain,
~ greater(vplus(vd328,vd330),vplus(vd329,vd330)),
inference(scs_inference,[],[i_0_115,i_0_99,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68]) ).
cnf(i_0_140,plain,
( ~ less(X1,X2)
| ~ greater(X1,X2) ),
inference(rename_variables,[],[i_0_68]) ).
cnf(i_0_141,plain,
greater(vplus(X1,vplus(X2,X3)),vplus(X1,X2)),
inference(scs_inference,[],[i_0_115,i_0_99,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69]) ).
cnf(i_0_142,plain,
( X1 != vplus(X2,X3)
| greater(X1,X2) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_143,plain,
vplus(X1,vplus(X2,X3)) != vplus(X1,X2),
inference(scs_inference,[],[i_0_115,i_0_99,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69,i_0_76]) ).
cnf(i_0_144,plain,
( X1 != vplus(X2,X3)
| X1 != X2 ),
inference(rename_variables,[],[i_0_76]) ).
cnf(i_0_145,plain,
vplus(vd329,vd330) != vplus(vd328,vd330),
inference(scs_inference,[],[i_0_115,i_0_99,i_0_105,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69,i_0_76,i_0_78]) ).
cnf(i_0_146,plain,
( ~ greater(X1,X2)
| X1 != X2 ),
inference(rename_variables,[],[i_0_78]) ).
cnf(i_0_147,plain,
vplus(vd328,vd330) != vplus(vd329,vd330),
inference(scs_inference,[],[i_0_115,i_0_99,i_0_105,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69,i_0_76,i_0_78,i_0_79]) ).
cnf(i_0_148,plain,
( ~ less(X1,X2)
| X1 != X2 ),
inference(rename_variables,[],[i_0_79]) ).
cnf(i_0_149,plain,
vplus(X1,X2) != vplus(X1,vplus(X2,X3)),
inference(scs_inference,[],[i_0_115,i_0_99,i_0_105,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69,i_0_76,i_0_78,i_0_79,i_0_77]) ).
cnf(i_0_150,plain,
( X1 != vplus(X2,X3)
| X2 != X1 ),
inference(rename_variables,[],[i_0_77]) ).
cnf(i_0_151,plain,
vd329 != vd328,
inference(scs_inference,[],[i_0_115,i_0_99,i_0_105,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69,i_0_76,i_0_78,i_0_79,i_0_77,i_0_86]) ).
cnf(i_0_152,plain,
esk4_2(X1,vplus(X1,X1)) = X1,
inference(scs_inference,[],[i_0_130,i_0_115,i_0_99,i_0_105,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69,i_0_76,i_0_78,i_0_79,i_0_77,i_0_86,i_0_84]) ).
cnf(i_0_153,plain,
vplus(X1,X2) = vplus(X1,esk4_2(X1,vplus(X1,X2))),
inference(scs_inference,[],[i_0_113,i_0_130,i_0_115,i_0_99,i_0_109,i_0_105,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69,i_0_76,i_0_78,i_0_79,i_0_77,i_0_86,i_0_84,i_0_59]) ).
cnf(i_0_154,plain,
X1 != vplus(vplus(X1,X2),X3),
inference(rename_variables,[],[i_0_109]) ).
cnf(i_0_155,plain,
( X1 = vplus(X2,esk3_2(X1,X2))
| X2 = vplus(X1,esk4_2(X1,X2))
| X1 = X2 ),
inference(rename_variables,[],[i_0_59]) ).
cnf(i_0_156,plain,
~ less(esk4_2(vd328,vplus(vd328,vd328)),vd329),
inference(scs_inference,[],[i_0_82,i_0_113,i_0_130,i_0_115,i_0_99,i_0_109,i_0_105,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69,i_0_76,i_0_78,i_0_79,i_0_77,i_0_86,i_0_84,i_0_59,i_0_90]) ).
cnf(i_0_157,plain,
~ greater(vplus(X1,vplus(X2,X3)),vplus(X3,vplus(X1,X2))),
inference(scs_inference,[],[i_0_82,i_0_125,i_0_113,i_0_130,i_0_115,i_0_99,i_0_109,i_0_105,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69,i_0_76,i_0_78,i_0_79,i_0_77,i_0_86,i_0_84,i_0_59,i_0_90,i_0_88]) ).
cnf(i_0_158,plain,
~ greater(vplus(X1,X2),vplus(X2,X1)),
inference(rename_variables,[],[i_0_125]) ).
cnf(i_0_159,plain,
vplus(X1,vd328) != vd329,
inference(scs_inference,[],[i_0_82,i_0_97,i_0_125,i_0_113,i_0_130,i_0_115,i_0_99,i_0_109,i_0_105,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69,i_0_76,i_0_78,i_0_79,i_0_77,i_0_86,i_0_84,i_0_59,i_0_90,i_0_88,i_0_91]) ).
cnf(i_0_160,plain,
less(X1,vplus(X2,X1)),
inference(rename_variables,[],[i_0_97]) ).
cnf(i_0_161,plain,
~ greater(vplus(X1,vplus(X2,X3)),vplus(X2,vplus(X3,X1))),
inference(scs_inference,[],[i_0_82,i_0_97,i_0_125,i_0_158,i_0_113,i_0_130,i_0_115,i_0_99,i_0_109,i_0_105,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69,i_0_76,i_0_78,i_0_79,i_0_77,i_0_86,i_0_84,i_0_59,i_0_90,i_0_88,i_0_91,i_0_89]) ).
cnf(i_0_162,plain,
~ greater(vplus(X1,X2),vplus(X2,X1)),
inference(rename_variables,[],[i_0_125]) ).
cnf(i_0_163,plain,
vplus(X1,esk4_2(vd328,vplus(vd328,vd328))) != vd328,
inference(scs_inference,[],[i_0_82,i_0_97,i_0_125,i_0_158,i_0_107,i_0_113,i_0_130,i_0_115,i_0_99,i_0_109,i_0_105,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69,i_0_76,i_0_78,i_0_79,i_0_77,i_0_86,i_0_84,i_0_59,i_0_90,i_0_88,i_0_91,i_0_89,i_0_85]) ).
cnf(i_0_164,plain,
X1 = esk4_2(X1,vplus(X1,X1)),
inference(rename_variables,[],[i_0_130]) ).
cnf(i_0_165,plain,
vplus(X1,X2) != X2,
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_166,plain,
~ greater(vplus(X1,X2),vplus(X1,vplus(X2,X3))),
inference(scs_inference,[],[i_0_82,i_0_97,i_0_125,i_0_158,i_0_107,i_0_113,i_0_130,i_0_115,i_0_99,i_0_109,i_0_105,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69,i_0_76,i_0_78,i_0_79,i_0_77,i_0_86,i_0_84,i_0_59,i_0_90,i_0_88,i_0_91,i_0_89,i_0_85,i_0_63]) ).
cnf(i_0_167,plain,
( X1 = vplus(X2,esk2_2(X2,X1))
| ~ greater(X1,X2) ),
inference(rename_variables,[],[i_0_63]) ).
cnf(i_0_168,plain,
~ greater(vd328,vd329),
inference(scs_inference,[],[i_0_82,i_0_97,i_0_125,i_0_158,i_0_107,i_0_113,i_0_130,i_0_115,i_0_99,i_0_109,i_0_105,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69,i_0_76,i_0_78,i_0_79,i_0_77,i_0_86,i_0_84,i_0_59,i_0_90,i_0_88,i_0_91,i_0_89,i_0_85,i_0_63,i_0_57]) ).
cnf(i_0_169,plain,
( greater(vplus(X1,X2),vplus(X3,X2))
| ~ greater(X1,X3) ),
inference(rename_variables,[],[i_0_57]) ).
cnf(i_0_170,plain,
X1 = esk4_2(X2,vplus(X2,X1)),
inference(scs_inference,[],[i_0_82,i_0_97,i_0_125,i_0_158,i_0_107,i_0_113,i_0_130,i_0_115,i_0_99,i_0_109,i_0_105,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69,i_0_76,i_0_78,i_0_79,i_0_77,i_0_86,i_0_84,i_0_59,i_0_90,i_0_88,i_0_91,i_0_89,i_0_85,i_0_63,i_0_57,i_0_67]) ).
cnf(i_0_171,plain,
( vplus(X1,X2) != vplus(X1,X3)
| X2 = X3 ),
inference(rename_variables,[],[i_0_67]) ).
cnf(i_0_172,plain,
vd328 = vd329,
inference(scs_inference,[],[i_0_82,i_0_97,i_0_125,i_0_158,i_0_107,i_0_113,i_0_130,i_0_115,i_0_99,i_0_109,i_0_105,i_0_65,i_0_64,i_0_70,i_0_66,i_0_68,i_0_69,i_0_76,i_0_78,i_0_79,i_0_77,i_0_86,i_0_84,i_0_59,i_0_90,i_0_88,i_0_91,i_0_89,i_0_85,i_0_63,i_0_57,i_0_67,i_0_74]) ).
cnf(i_0_173,plain,
( greater(X1,X2)
| less(X1,X2)
| X1 = X2 ),
inference(rename_variables,[],[i_0_74]) ).
cnf(i_0_174,plain,
~ less(vplus(X1,X2),X1),
inference(scs_inference,[],[i_0_109,i_0_64]) ).
cnf(i_0_175,plain,
X1 != vplus(vplus(X1,X2),X3),
inference(rename_variables,[],[i_0_109]) ).
cnf(i_0_176,plain,
( X1 = vplus(X2,esk1_2(X1,X2))
| ~ less(X2,X1) ),
inference(rename_variables,[],[i_0_64]) ).
cnf(i_0_177,plain,
less(X1,esk4_2(vplus(X1,X2),vplus(vplus(X1,X2),vplus(X1,X2)))),
inference(scs_inference,[],[i_0_152,i_0_109,i_0_64,i_0_70]) ).
cnf(i_0_178,plain,
esk4_2(X1,vplus(X1,X1)) = X1,
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_179,plain,
( X1 != vplus(X2,X3)
| less(X2,X1) ),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_180,plain,
vplus(X1,X2) != vplus(vplus(vplus(X1,v1),X2),X3),
inference(scs_inference,[],[i_0_152,i_0_61,i_0_109,i_0_64,i_0_70,i_0_66]) ).
cnf(i_0_181,plain,
( X1 != vplus(X2,X3)
| X2 != vplus(X1,X4) ),
inference(rename_variables,[],[i_0_66]) ).
cnf(i_0_182,plain,
greater(esk4_2(vplus(X1,X2),vplus(vplus(X1,X2),vplus(X1,X2))),X1),
inference(scs_inference,[],[i_0_152,i_0_178,i_0_61,i_0_109,i_0_64,i_0_70,i_0_66,i_0_69]) ).
cnf(i_0_183,plain,
esk4_2(X1,vplus(X1,X1)) = X1,
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_184,plain,
( X1 != vplus(X2,X3)
| greater(X1,X2) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_185,plain,
esk4_2(vplus(X1,X2),vplus(vplus(X1,X2),vplus(X1,X2))) != X1,
inference(scs_inference,[],[i_0_152,i_0_178,i_0_183,i_0_61,i_0_109,i_0_64,i_0_70,i_0_66,i_0_69,i_0_76]) ).
cnf(i_0_186,plain,
esk4_2(X1,vplus(X1,X1)) = X1,
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_187,plain,
( X1 != vplus(X2,X3)
| X1 != X2 ),
inference(rename_variables,[],[i_0_76]) ).
cnf(i_0_188,plain,
X1 != esk4_2(vplus(X1,X2),vplus(vplus(X1,X2),vplus(X1,X2))),
inference(scs_inference,[],[i_0_152,i_0_178,i_0_183,i_0_186,i_0_61,i_0_109,i_0_64,i_0_70,i_0_66,i_0_69,i_0_76,i_0_77]) ).
cnf(i_0_189,plain,
esk4_2(X1,vplus(X1,X1)) = X1,
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_190,plain,
( X1 != vplus(X2,X3)
| X2 != X1 ),
inference(rename_variables,[],[i_0_77]) ).
cnf(i_0_191,plain,
~ greater(X1,esk4_2(vplus(X1,X2),vplus(vplus(X1,X2),vplus(X1,X2)))),
inference(scs_inference,[],[i_0_152,i_0_178,i_0_183,i_0_186,i_0_61,i_0_109,i_0_64,i_0_70,i_0_66,i_0_69,i_0_76,i_0_77,i_0_68]) ).
cnf(i_0_192,plain,
( ~ less(X1,X2)
| ~ greater(X1,X2) ),
inference(rename_variables,[],[i_0_68]) ).
cnf(i_0_193,plain,
$false,
inference(scs_inference,[],[i_0_172,i_0_152,i_0_178,i_0_183,i_0_186,i_0_151,i_0_61,i_0_109,i_0_64,i_0_70,i_0_66,i_0_69,i_0_76,i_0_77,i_0_68,i_0_84]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM840+2 : TPTP v9.2.1. Released v4.1.0.
% 0.00/0.12 % 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.15/0.33 % Computer : n004.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 01:15:32 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 0.45/1.61 % Version : CSE_E---1.7
% 0.45/1.61 % Problem : theBenchmark.p
% 0.45/1.61 % SZS status Theorem for theBenchmark.p
% 0.45/1.61 % SZS output start CNFRefutation
% See solution above
% 0.66/1.90 % Total time : 1.273s
%------------------------------------------------------------------------------