%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM837+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 : 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.27s 1.61s
% Output : CNFRefutation 0.27s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_30)
% Comments :
%------------------------------------------------------------------------------
fof('qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))',axiom,
! [X32,X33] :
( vplus(X32,vsucc(X33)) = vsucc(vplus(X32,X33))
& vplus(X32,v1) = vsucc(X32) ),
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('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('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,
! [X29,X30,X31] : vplus(vplus(X29,X30),X31) = vplus(X29,vplus(X30,X31)),
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(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('holds(conjunct1(170), 270, 0)',axiom,
less(vd268,vd269),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(170), 270, 0)') ).
fof('(conjunct2(170),272,0)',axiom,
less(vd269,vd271),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','(conjunct2(170),272,0)') ).
fof(i_0_22,plain,
! [X136,X137] :
( vplus(X136,vsucc(X137)) = vsucc(vplus(X136,X137))
& vplus(X136,v1) = vsucc(X136) ),
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_23,plain,
! [X14,X15] :
( ~ greater(X14,X15)
| ~ less(X14,X15) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 2)']) ).
fof(i_0_24,plain,
! [X14,X15] :
( X14 != X15
| ~ greater(X14,X15) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 3)']) ).
fof(i_0_25,plain,
! [X14,X15] :
( X14 != X15
| ~ less(X14,X15) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 1)']) ).
fof(i_0_26,negated_conjecture,
~ ? [X1] : vd269 = vplus(vd268,X1),
inference(assume_negation,[status(cth)],['qe(171)']) ).
fof(i_0_27,plain,
! [X116,X117] :
( X116 = X117
| X116 = vplus(X117,esk3_2(X116,X117))
| X117 = vplus(X116,esk4_2(X116,X117)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['ass(cond(goal(88), 0), 0)'])]) ).
fof(i_0_28,plain,
! [X133,X134,X135] : vplus(vplus(X133,X134),X135) = vplus(X133,vplus(X134,X135)),
inference(variable_rename,[status(thm)],['ass(cond(33, 0), 0)']) ).
cnf(i_0_29,plain,
vplus(X1,vsucc(X2)) = vsucc(vplus(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_22]) ).
cnf(i_0_30,plain,
vplus(X1,v1) = vsucc(X1),
inference(split_conjunct,[status(thm)],[i_0_22]) ).
fof(i_0_31,plain,
! [X110,X111,X113,X114,X115] :
( ( ~ greater(X111,X110)
| X111 = vplus(X110,esk2_2(X110,X111)) )
& ( X114 != vplus(X113,X115)
| greater(X114,X113) ) ),
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_32,plain,
! [X104,X105,X107,X108,X109] :
( ( ~ less(X105,X104)
| X104 = vplus(X105,esk1_2(X104,X105)) )
& ( X107 != vplus(X108,X109)
| less(X108,X107) ) ),
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_33,plain,
! [X123,X124,X125,X126] :
( X123 != vplus(X124,X125)
| X124 != vplus(X123,X126) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 2)'])])]) ).
fof(i_0_34,plain,
! [X130,X131,X132] :
( X130 = X131
| vplus(X132,X130) != vplus(X132,X131) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(81, 0), 0)'])])]) ).
fof(i_0_35,plain,
! [X100,X101] :
( ~ greater(X100,X101)
| ~ less(X100,X101) ),
inference(variable_rename,[status(thm)],[i_0_23]) ).
fof(i_0_36,plain,
! [X90,X91] :
( ( ~ geq(X91,X90)
| greater(X91,X90)
| X91 = X90 )
& ( ~ greater(X91,X90)
| geq(X91,X90) )
& ( X91 != X90
| geq(X91,X90) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['def(cond(conseq(axiom(3)), 16), 1)'])])]) ).
fof(i_0_37,plain,
! [X88,X89] :
( ( ~ leq(X89,X88)
| less(X89,X88)
| X89 = X88 )
& ( ~ less(X89,X88)
| leq(X89,X88) )
& ( X89 != X88
| leq(X89,X88) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['def(cond(conseq(axiom(3)), 17), 1)'])])]) ).
fof(i_0_38,plain,
! [X92,X93] :
( ~ less(X92,X93)
| greater(X93,X92) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(147, 0), 0)'])]) ).
fof(i_0_39,plain,
! [X84,X85] :
( ~ leq(X84,X85)
| geq(X85,X84) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(163, 0), 0)'])]) ).
fof(i_0_40,plain,
! [X86,X87] :
( ~ geq(X86,X87)
| leq(X87,X86) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(158, 0), 0)'])]) ).
fof(i_0_41,plain,
! [X94,X95] :
( ~ greater(X94,X95)
| less(X95,X94) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(140, 0), 0)'])]) ).
fof(i_0_42,plain,
! [X96,X97] :
( X96 = X97
| greater(X96,X97)
| less(X96,X97) ),
inference(variable_rename,[status(thm)],['ass(cond(goal(130), 0), 0)']) ).
fof(i_0_43,plain,
! [X127,X128,X129] :
( X127 != X128
| X127 != vplus(X128,X129) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 3)'])])]) ).
fof(i_0_44,plain,
! [X120,X121,X122] :
( X120 != X121
| X121 != vplus(X120,X122) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 1)'])])]) ).
fof(i_0_45,plain,
! [X102,X103] :
( X102 != X103
| ~ greater(X102,X103) ),
inference(variable_rename,[status(thm)],[i_0_24]) ).
fof(i_0_46,plain,
! [X98,X99] :
( X98 != X99
| ~ less(X98,X99) ),
inference(variable_rename,[status(thm)],[i_0_25]) ).
fof(i_0_47,negated_conjecture,
! [X83] : vd269 != vplus(vd268,X83),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_26])]) ).
cnf(i_0_48,plain,
( X1 = X2
| X1 = vplus(X2,esk3_2(X1,X2))
| X2 = vplus(X1,esk4_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_27]),
[final] ).
cnf(i_0_49,plain,
vplus(vplus(X1,X2),X3) = vplus(X1,vplus(X2,X3)),
inference(split_conjunct,[status(thm)],[i_0_28]),
[final] ).
cnf(i_0_50,plain,
vplus(X1,vplus(X2,v1)) = vplus(vplus(X1,X2),v1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_29,c_0_30]),c_0_30]),
[final] ).
cnf(i_0_51,plain,
( X1 = vplus(X2,esk2_2(X2,X1))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_31]),
[final] ).
cnf(i_0_52,plain,
( X2 = vplus(X1,esk1_2(X2,X1))
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_53,plain,
( X1 != vplus(X2,X3)
| X2 != vplus(X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_54,plain,
( X1 = X2
| vplus(X3,X1) != vplus(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_55,plain,
( ~ greater(X1,X2)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_56,plain,
( greater(X1,X2)
| X1 = X2
| ~ geq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_57,plain,
( less(X1,X2)
| X1 = X2
| ~ leq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_58,plain,
( greater(X1,X2)
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_31]),
[final] ).
cnf(i_0_59,plain,
( less(X2,X1)
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_60,plain,
( greater(X2,X1)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_38]),
[final] ).
cnf(i_0_61,plain,
( geq(X1,X2)
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_62,plain,
( geq(X2,X1)
| ~ leq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_63,plain,
( leq(X1,X2)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_64,plain,
( leq(X2,X1)
| ~ geq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_65,plain,
( less(X2,X1)
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_66,plain,
( X1 = X2
| greater(X1,X2)
| less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_67,plain,
( X1 != X2
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_68,plain,
( X1 != X2
| X2 != vplus(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_69,plain,
( X1 != X2
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_70,plain,
( X1 != X2
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_71,negated_conjecture,
vd269 != vplus(vd268,X1),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_72,plain,
( geq(X1,X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_73,plain,
( leq(X1,X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_74,plain,
less(vd268,vd269),
inference(split_conjunct,[status(thm)],['holds(conjunct1(170), 270, 0)']),
[final] ).
cnf(i_0_75,plain,
less(vd269,vd271),
inference(split_conjunct,[status(thm)],['(conjunct2(170),272,0)']),
[final] ).
cnf(i_0_76,axiom,
X1 = X1 ).
cnf(i_0_77,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_78,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_79,axiom,
( X1 != X2
| vplus(X1,X3) = vplus(X2,X3) ) ).
cnf(i_0_80,axiom,
( X1 != X2
| vplus(X3,X1) = vplus(X3,X2) ) ).
cnf(i_0_81,axiom,
( X1 != X2
| ~ greater(X1,X3)
| greater(X2,X3) ) ).
cnf(i_0_82,axiom,
( X1 != X2
| ~ greater(X3,X1)
| greater(X3,X2) ) ).
cnf(i_0_83,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_84,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_85,axiom,
( X1 != X2
| ~ geq(X1,X3)
| geq(X2,X3) ) ).
cnf(i_0_86,axiom,
( X1 != X2
| ~ geq(X3,X1)
| geq(X3,X2) ) ).
cnf(i_0_87,axiom,
( X1 != X2
| ~ leq(X1,X3)
| leq(X2,X3) ) ).
cnf(i_0_88,axiom,
( X1 != X2
| ~ leq(X3,X1)
| leq(X3,X2) ) ).
cnf(i_0_76_001,axiom,
X1 = X1 ).
cnf(i_0_77_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_78_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_79_004,axiom,
( X1 != X2
| vplus(X1,X3) = vplus(X2,X3) ) ).
cnf(i_0_80_005,axiom,
( X1 != X2
| vplus(X3,X1) = vplus(X3,X2) ) ).
cnf(i_0_81_006,axiom,
( X1 != X2
| ~ greater(X1,X3)
| greater(X2,X3) ) ).
cnf(i_0_82_007,axiom,
( X1 != X2
| ~ greater(X3,X1)
| greater(X3,X2) ) ).
cnf(i_0_83_008,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_84_009,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_85_010,axiom,
( X1 != X2
| ~ geq(X1,X3)
| geq(X2,X3) ) ).
cnf(i_0_86_011,axiom,
( X1 != X2
| ~ geq(X3,X1)
| geq(X3,X2) ) ).
cnf(i_0_87_012,axiom,
( X1 != X2
| ~ leq(X1,X3)
| leq(X2,X3) ) ).
cnf(i_0_88_013,axiom,
( X1 != X2
| ~ leq(X3,X1)
| leq(X3,X2) ) ).
cnf(i_0_89,plain,
X1 = X1,
inference(equality_inference,[],[54]) ).
cnf(i_0_90,plain,
greater(vplus(X1,X2),X1),
inference(equality_inference,[],[58]) ).
cnf(i_0_91,plain,
less(X1,vplus(X1,X2)),
inference(equality_inference,[],[59]) ).
cnf(i_0_92,plain,
~ greater(X1,X1),
inference(equality_inference,[],[69]) ).
cnf(i_0_93,plain,
~ less(X1,X1),
inference(equality_inference,[],[70]) ).
cnf(i_0_94,plain,
geq(X1,X1),
inference(equality_inference,[],[72]) ).
cnf(i_0_95,plain,
leq(X1,X1),
inference(equality_inference,[],[73]) ).
cnf(i_0_96,plain,
$false,
inference(scs_inference,[],[i_0_71,i_0_74,i_0_52]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM837+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.14/0.33 % Computer : n016.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Tue May 5 01:15:36 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 0.27/1.61 % Version : CSE_E---1.7
% 0.27/1.61 % Problem : theBenchmark.p
% 0.27/1.61 % SZS status Theorem for theBenchmark.p
% 0.27/1.61 % SZS output start CNFRefutation
% See solution above
% 0.27/1.63 % Total time : 1.271s
%------------------------------------------------------------------------------