%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM854+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 : n007.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:45 PM UTC 2026
% Result : Theorem 0.28s 1.62s
% Output : CNFRefutation 0.28s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 66)
% Comments :
%------------------------------------------------------------------------------
fof('ass(cond(goal(130), 0), 2)',axiom,
! [X34,X35] :
( ~ greater(X34,X35)
| ~ less(X34,X35) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 2)') ).
fof('ass(cond(goal(130), 0), 1)',axiom,
! [X34,X35] :
( X34 != X35
| ~ less(X34,X35) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 1)') ).
fof('ass(cond(goal(130), 0), 3)',axiom,
! [X34,X35] :
( X34 != X35
| ~ greater(X34,X35) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 3)') ).
fof('ass(cond(conjunct2(conjunct2(307)), 0), 0)',axiom,
! [X1,X2,X3] :
( less(vmul(X1,X2),vmul(X3,X2))
=> less(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(conjunct2(conjunct2(307)), 0), 0)') ).
fof('ass(cond(conjunct1(307), 0), 0)',axiom,
! [X7,X8,X9] :
( greater(vmul(X7,X8),vmul(X9,X8))
=> greater(X7,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(conjunct1(307), 0), 0)') ).
fof('ass(cond(281, 0), 0)',axiom,
! [X20,X21,X22] : vmul(X20,vplus(X21,X22)) = vplus(vmul(X20,X21),vmul(X20,X22)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(281, 0), 0)') ).
fof('ass(cond(299, 0), 0)',axiom,
! [X10,X11,X12] :
( less(X11,X12)
=> less(vmul(X11,X10),vmul(X12,X10)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(299, 0), 0)') ).
fof('ass(cond(299, 0), 2)',axiom,
! [X10,X15,X16] :
( greater(X15,X16)
=> greater(vmul(X15,X10),vmul(X16,X10)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(299, 0), 2)') ).
fof('holds(conjunct1(315), 514, 0)',conjecture,
greater(vmul(vd508,vd511),vmul(vd509,vd511)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(315), 514, 0)') ).
fof('ass(cond(goal(88), 0), 0)',axiom,
! [X42,X43] :
( X42 = X43
| ? [X44] : X42 = vplus(X43,X44)
| ? [X45] : X43 = vplus(X42,X45) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 0)') ).
fof('ass(cond(290, 0), 0)',axiom,
! [X17,X18,X19] : vmul(vmul(X17,X18),X19) = vmul(X17,vmul(X18,X19)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(290, 0), 0)') ).
fof('def(cond(conseq(axiom(3)), 11), 1)',axiom,
! [X39,X40] :
( greater(X40,X39)
<=> ? [X41] : X40 = vplus(X39,X41) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 11), 1)') ).
fof('def(cond(conseq(axiom(3)), 12), 1)',axiom,
! [X36,X37] :
( less(X37,X36)
<=> ? [X38] : X36 = vplus(X37,X38) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 12), 1)') ).
fof('ass(cond(261, 0), 0)',axiom,
! [X25,X26] : vmul(vsucc(X25),X26) = vplus(vmul(X25,X26),X26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(261, 0), 0)') ).
fof('qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0)))',axiom,
! [X28,X29] :
( vmul(X28,vsucc(X29)) = vplus(vmul(X28,X29),X28)
& vmul(X28,v1) = X28 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0)))') ).
fof('ass(cond(goal(88), 0), 2)',axiom,
! [X42,X43] :
( ~ ? [X44] : X42 = vplus(X43,X44)
| ~ ? [X45] : X43 = vplus(X42,X45) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 2)') ).
fof('ass(cond(conjunct1(conjunct2(307)), 0), 0)',axiom,
! [X4,X5,X6] :
( vmul(X4,X5) = vmul(X6,X5)
=> X4 = X6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(conjunct1(conjunct2(307)), 0), 0)') ).
fof('ass(cond(140, 0), 0)',axiom,
! [X32,X33] :
( greater(X32,X33)
=> less(X33,X32) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(140, 0), 0)') ).
fof('ass(cond(147, 0), 0)',axiom,
! [X30,X31] :
( less(X30,X31)
=> greater(X31,X30) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(147, 0), 0)') ).
fof('ass(cond(goal(130), 0), 0)',axiom,
! [X34,X35] :
( X34 = X35
| greater(X34,X35)
| less(X34,X35) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 0)') ).
fof('ass(cond(270, 0), 0)',axiom,
! [X23,X24] : vmul(X23,X24) = vmul(X24,X23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(270, 0), 0)') ).
fof('ass(cond(goal(88), 0), 3)',axiom,
! [X42,X43] :
( X42 != X43
| ~ ? [X44] : X42 = vplus(X43,X44) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 3)') ).
fof('ass(cond(goal(88), 0), 1)',axiom,
! [X42,X43] :
( X42 != X43
| ~ ? [X45] : X43 = vplus(X42,X45) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 1)') ).
fof('ass(cond(253, 0), 0)',axiom,
! [X27] : vmul(v1,X27) = X27,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(253, 0), 0)') ).
fof('holds(conjunct2(314), 513, 0)',axiom,
greater(vd511,vd512),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct2(314), 513, 0)') ).
fof('holds(conjunct1(314), 510, 0)',axiom,
greater(vd508,vd509),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conjunct1(314), 510, 0)') ).
fof(i_0_26,plain,
! [X34,X35] :
( ~ greater(X34,X35)
| ~ less(X34,X35) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 2)']) ).
fof(i_0_27,plain,
! [X34,X35] :
( X34 != X35
| ~ less(X34,X35) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 1)']) ).
fof(i_0_28,plain,
! [X34,X35] :
( X34 != X35
| ~ greater(X34,X35) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 3)']) ).
fof(i_0_29,plain,
! [X109,X110,X111] :
( ~ less(vmul(X109,X110),vmul(X111,X110))
| less(X109,X111) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(conjunct2(conjunct2(307)), 0), 0)'])]) ).
fof(i_0_30,plain,
! [X115,X116,X117] :
( ~ greater(vmul(X115,X116),vmul(X117,X116))
| greater(X115,X117) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(conjunct1(307), 0), 0)'])]) ).
fof(i_0_31,plain,
! [X130,X131,X132] : vmul(X130,vplus(X131,X132)) = vplus(vmul(X130,X131),vmul(X130,X132)),
inference(variable_rename,[status(thm)],['ass(cond(281, 0), 0)']) ).
fof(i_0_32,plain,
! [X118,X119,X120] :
( ~ less(X119,X120)
| less(vmul(X119,X118),vmul(X120,X118)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(299, 0), 0)'])]) ).
fof(i_0_33,plain,
! [X124,X125,X126] :
( ~ greater(X125,X126)
| greater(vmul(X125,X124),vmul(X126,X124)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(299, 0), 2)'])]) ).
fof(i_0_34,negated_conjecture,
~ greater(vmul(vd508,vd511),vmul(vd509,vd511)),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],['holds(conjunct1(315), 514, 0)'])]) ).
fof(i_0_35,plain,
! [X164,X165] :
( X164 = X165
| X164 = vplus(X165,esk3_2(X164,X165))
| X165 = vplus(X164,esk4_2(X164,X165)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['ass(cond(goal(88), 0), 0)'])]) ).
fof(i_0_36,plain,
! [X127,X128,X129] : vmul(vmul(X127,X128),X129) = vmul(X127,vmul(X128,X129)),
inference(variable_rename,[status(thm)],['ass(cond(290, 0), 0)']) ).
fof(i_0_37,plain,
! [X158,X159,X161,X162,X163] :
( ( ~ greater(X159,X158)
| X159 = vplus(X158,esk2_2(X158,X159)) )
& ( X162 != vplus(X161,X163)
| greater(X162,X161) ) ),
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_38,plain,
! [X152,X153,X155,X156,X157] :
( ( ~ less(X153,X152)
| X152 = vplus(X153,esk1_2(X152,X153)) )
& ( X155 != vplus(X156,X157)
| less(X156,X155) ) ),
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_39,plain,
! [X135,X136] : vmul(vsucc(X135),X136) = vplus(vmul(X135,X136),X136),
inference(variable_rename,[status(thm)],['ass(cond(261, 0), 0)']) ).
fof(i_0_40,plain,
! [X138,X139] :
( vmul(X138,vsucc(X139)) = vplus(vmul(X138,X139),X138)
& vmul(X138,v1) = X138 ),
inference(variable_rename,[status(thm)],['qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0)))']) ).
fof(i_0_41,plain,
! [X171,X172,X173,X174] :
( X171 != vplus(X172,X173)
| X172 != vplus(X171,X174) ),
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,
! [X112,X113,X114] :
( vmul(X112,X113) != vmul(X114,X113)
| X112 = X114 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(conjunct1(conjunct2(307)), 0), 0)'])]) ).
fof(i_0_43,plain,
! [X148,X149] :
( ~ greater(X148,X149)
| ~ less(X148,X149) ),
inference(variable_rename,[status(thm)],[i_0_26]) ).
fof(i_0_44,plain,
! [X142,X143] :
( ~ greater(X142,X143)
| less(X143,X142) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(140, 0), 0)'])]) ).
fof(i_0_45,plain,
! [X140,X141] :
( ~ less(X140,X141)
| greater(X141,X140) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(147, 0), 0)'])]) ).
fof(i_0_46,plain,
! [X144,X145] :
( X144 = X145
| greater(X144,X145)
| less(X144,X145) ),
inference(variable_rename,[status(thm)],['ass(cond(goal(130), 0), 0)']) ).
fof(i_0_47,plain,
! [X133,X134] : vmul(X133,X134) = vmul(X134,X133),
inference(variable_rename,[status(thm)],['ass(cond(270, 0), 0)']) ).
fof(i_0_48,plain,
! [X175,X176,X177] :
( X175 != X176
| X175 != vplus(X176,X177) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 3)'])])]) ).
fof(i_0_49,plain,
! [X168,X169,X170] :
( X168 != X169
| X169 != vplus(X168,X170) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 1)'])])]) ).
fof(i_0_50,plain,
! [X146,X147] :
( X146 != X147
| ~ less(X146,X147) ),
inference(variable_rename,[status(thm)],[i_0_27]) ).
fof(i_0_51,plain,
! [X150,X151] :
( X150 != X151
| ~ greater(X150,X151) ),
inference(variable_rename,[status(thm)],[i_0_28]) ).
fof(i_0_52,plain,
! [X137] : vmul(v1,X137) = X137,
inference(variable_rename,[status(thm)],['ass(cond(253, 0), 0)']) ).
cnf(i_0_53,plain,
( less(X1,X3)
| ~ less(vmul(X1,X2),vmul(X3,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_29]),
[final] ).
cnf(i_0_54,plain,
( greater(X1,X3)
| ~ greater(vmul(X1,X2),vmul(X3,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_55,plain,
vmul(X1,vplus(X2,X3)) = vplus(vmul(X1,X2),vmul(X1,X3)),
inference(split_conjunct,[status(thm)],[i_0_31]),
[final] ).
cnf(i_0_56,plain,
( less(vmul(X1,X3),vmul(X2,X3))
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_57,plain,
( greater(vmul(X1,X3),vmul(X2,X3))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_58,negated_conjecture,
~ greater(vmul(vd508,vd511),vmul(vd509,vd511)),
inference(split_conjunct,[status(thm)],[i_0_34]),
[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_35]),
[final] ).
cnf(i_0_60,plain,
vmul(vmul(X1,X2),X3) = vmul(X1,vmul(X2,X3)),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_61,plain,
( X1 = vplus(X2,esk2_2(X2,X1))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_62,plain,
( X2 = vplus(X1,esk1_2(X2,X1))
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_38]),
[final] ).
cnf(i_0_63,plain,
vmul(vsucc(X1),X2) = vplus(vmul(X1,X2),X2),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_64,plain,
vmul(X1,vsucc(X2)) = vplus(vmul(X1,X2),X1),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_65,plain,
( X1 != vplus(X2,X3)
| X2 != vplus(X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_66,plain,
( X1 = X3
| vmul(X1,X2) != vmul(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_67,plain,
( ~ greater(X1,X2)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_68,plain,
( less(X2,X1)
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_38]),
[final] ).
cnf(i_0_69,plain,
( greater(X1,X2)
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_70,plain,
( less(X2,X1)
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_71,plain,
( greater(X2,X1)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_72,plain,
( X1 = X2
| greater(X1,X2)
| less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_73,plain,
vmul(X1,X2) = vmul(X2,X1),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_74,plain,
( X1 != X2
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_75,plain,
( X1 != X2
| X2 != vplus(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_76,plain,
( X1 != X2
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_77,plain,
( X1 != X2
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_78,plain,
vmul(v1,X1) = X1,
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_79,plain,
vmul(X1,v1) = X1,
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_80,plain,
greater(vd511,vd512),
inference(split_conjunct,[status(thm)],['holds(conjunct2(314), 513, 0)']),
[final] ).
cnf(i_0_81,plain,
greater(vd508,vd509),
inference(split_conjunct,[status(thm)],['holds(conjunct1(314), 510, 0)']),
[final] ).
cnf(i_0_82,axiom,
X1 = X1 ).
cnf(i_0_83,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_84,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_85,axiom,
( X1 != X2
| vmul(X1,X3) = vmul(X2,X3) ) ).
cnf(i_0_86,axiom,
( X1 != X2
| vmul(X3,X1) = vmul(X3,X2) ) ).
cnf(i_0_87,axiom,
( X1 != X2
| vplus(X1,X3) = vplus(X2,X3) ) ).
cnf(i_0_88,axiom,
( X1 != X2
| vplus(X3,X1) = vplus(X3,X2) ) ).
cnf(i_0_89,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_90,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_91,axiom,
( X1 != X2
| ~ greater(X1,X3)
| greater(X2,X3) ) ).
cnf(i_0_92,axiom,
( X1 != X2
| ~ greater(X3,X1)
| greater(X3,X2) ) ).
cnf(i_0_82_001,axiom,
X1 = X1 ).
cnf(i_0_83_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_84_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_85_004,axiom,
( X1 != X2
| vmul(X1,X3) = vmul(X2,X3) ) ).
cnf(i_0_86_005,axiom,
( X1 != X2
| vmul(X3,X1) = vmul(X3,X2) ) ).
cnf(i_0_87_006,axiom,
( X1 != X2
| vplus(X1,X3) = vplus(X2,X3) ) ).
cnf(i_0_88_007,axiom,
( X1 != X2
| vplus(X3,X1) = vplus(X3,X2) ) ).
cnf(i_0_89_008,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_90_009,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_91_010,axiom,
( X1 != X2
| ~ greater(X1,X3)
| greater(X2,X3) ) ).
cnf(i_0_92_011,axiom,
( X1 != X2
| ~ greater(X3,X1)
| greater(X3,X2) ) ).
cnf(i_0_93,plain,
X1 = X1,
inference(equality_inference,[],[66]) ).
cnf(i_0_94,plain,
less(X1,vplus(X1,X2)),
inference(equality_inference,[],[68]) ).
cnf(i_0_95,plain,
greater(vplus(X1,X2),X1),
inference(equality_inference,[],[69]) ).
cnf(i_0_96,plain,
~ less(X1,X1),
inference(equality_inference,[],[76]) ).
cnf(i_0_97,plain,
~ greater(X1,X1),
inference(equality_inference,[],[77]) ).
cnf(i_0_98,plain,
$false,
inference(scs_inference,[],[i_0_58,i_0_81,i_0_57]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM854+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 : n007.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:24 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/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
%------------------------------------------------------------------------------