%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM854+1 : 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 : n021.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:44 PM UTC 2026
% Result : Theorem 0.31s 1.62s
% Output : CNFRefutation 0.31s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_87)
% Comments :
%------------------------------------------------------------------------------
fof('ass(cond(261, 0), 0)',axiom,
! [X25,X26] : vmul(vsucc(X25),X26) = vplus(vmul(X25,X26),X26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(261, 0), 0)') ).
fof('qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))',axiom,
! [X101,X102] :
( vplus(X101,vsucc(X102)) = vsucc(vplus(X101,X102))
& vplus(X101,v1) = vsucc(X101) ),
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('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/sandbox/benchmark/theBenchmark.p','qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0)))') ).
fof('ass(cond(52, 0), 0)',axiom,
! [X95,X96] : vplus(vsucc(X95),X96) = vsucc(vplus(X95,X96)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(52, 0), 0)') ).
fof('ass(cond(goal(130), 0), 2)',axiom,
! [X76,X77] :
( ~ greater(X76,X77)
| ~ less(X76,X77) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 2)') ).
fof('qu(antec(axiom(3)), imp(antec(axiom(3))))',axiom,
! [X107,X108] :
( vsucc(X107) = vsucc(X108)
=> X107 = X108 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(antec(axiom(3)), imp(antec(axiom(3))))') ).
fof('ass(cond(6, 0), 0)',axiom,
! [X105,X106] :
( X105 != X106
=> vsucc(X105) != vsucc(X106) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(6, 0), 0)') ).
fof('ass(cond(goal(130), 0), 1)',axiom,
! [X76,X77] :
( X76 != X77
| ~ less(X76,X77) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 1)') ).
fof('ass(cond(goal(130), 0), 3)',axiom,
! [X76,X77] :
( X76 != X77
| ~ greater(X76,X77) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 3)') ).
fof('ass(cond(43, 0), 0)',axiom,
! [X97] : vplus(v1,X97) = vsucc(X97),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(43, 0), 0)') ).
fof('ass(cond(12, 0), 0)',axiom,
! [X104] : vsucc(X104) != X104,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(12, 0), 0)') ).
fof('ass(cond(20, 0), 0)',axiom,
! [X103] :
( X103 != v1
=> X103 = vsucc(vskolem2(X103)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(20, 0), 0)') ).
fof('qu(restrictor(axiom(1)), holds(scope(axiom(1)), 2, 0))',axiom,
! [X109] : vsucc(X109) != v1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(restrictor(axiom(1)), holds(scope(axiom(1)), 2, 0))') ).
fof('ass(cond(goal(202), 0), 0)',axiom,
! [X47,X48,X49] :
( less(vplus(X47,X49),vplus(X48,X49))
=> less(X47,X48) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(202), 0), 0)') ).
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/sandbox/benchmark/theBenchmark.p','ass(cond(conjunct2(conjunct2(307)), 0), 0)') ).
fof('ass(cond(goal(202), 0), 2)',axiom,
! [X47,X48,X49] :
( greater(vplus(X47,X49),vplus(X48,X49))
=> greater(X47,X48) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(202), 0), 2)') ).
fof('ass(cond(conjunct1(307), 0), 0)',axiom,
! [X7,X8,X9] :
( greater(vmul(X7,X8),vmul(X9,X8))
=> greater(X7,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(conjunct1(307), 0), 0)') ).
fof('ass(cond(223, 0), 0)',axiom,
! [X35,X36,X37,X38] :
( ( geq(X37,X38)
& geq(X35,X36) )
=> geq(vplus(X35,X37),vplus(X36,X38)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(223, 0), 0)') ).
fof('ass(cond(goal(216), 0), 0)',axiom,
! [X39,X40,X41,X42] :
( ( ( greater(X41,X42)
& geq(X39,X40) )
| ( geq(X41,X42)
& greater(X39,X40) ) )
=> greater(vplus(X39,X41),vplus(X40,X42)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(216), 0), 0)') ).
fof('ass(cond(209, 0), 0)',axiom,
! [X43,X44,X45,X46] :
( ( greater(X45,X46)
& greater(X43,X44) )
=> greater(vplus(X43,X45),vplus(X44,X46)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(209, 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/sandbox/benchmark/theBenchmark.p','ass(cond(281, 0), 0)') ).
fof('ass(cond(goal(193), 0), 0)',axiom,
! [X50,X51,X52] :
( less(X50,X51)
=> less(vplus(X50,X52),vplus(X51,X52)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(193), 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/sandbox/benchmark/theBenchmark.p','ass(cond(299, 0), 0)') ).
fof('ass(cond(goal(193), 0), 2)',axiom,
! [X50,X51,X52] :
( greater(X50,X51)
=> greater(vplus(X50,X52),vplus(X51,X52)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(193), 0), 2)') ).
fof('ass(cond(299, 0), 2)',axiom,
! [X10,X15,X16] :
( greater(X15,X16)
=> greater(vmul(X15,X10),vmul(X16,X10)) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p','holds(conjunct1(315), 514, 0)') ).
fof('ass(cond(goal(88), 0), 0)',axiom,
! [X84,X85] :
( X84 = X85
| ? [X86] : X84 = vplus(X85,X86)
| ? [X87] : X85 = vplus(X84,X87) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 0)') ).
fof('ass(cond(33, 0), 0)',axiom,
! [X98,X99,X100] : vplus(vplus(X98,X99),X100) = vplus(X98,vplus(X99,X100)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(33, 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/sandbox/benchmark/theBenchmark.p','ass(cond(290, 0), 0)') ).
fof('ass(cond(241, 0), 0)',axiom,
! [X30,X31] :
( less(X30,vplus(X31,v1))
=> leq(X30,X31) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(241, 0), 0)') ).
fof('def(cond(conseq(axiom(3)), 11), 1)',axiom,
! [X81,X82] :
( greater(X82,X81)
<=> ? [X83] : X82 = vplus(X81,X83) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 11), 1)') ).
fof('def(cond(conseq(axiom(3)), 12), 1)',axiom,
! [X78,X79] :
( less(X79,X78)
<=> ? [X80] : X78 = vplus(X79,X80) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 12), 1)') ).
fof('ass(cond(234, 0), 0)',axiom,
! [X32,X33] :
( greater(X32,X33)
=> geq(X32,vplus(X33,v1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(234, 0), 0)') ).
fof('ass(cond(184, 0), 0)',axiom,
! [X55,X56,X57] :
( ( leq(X56,X57)
& leq(X55,X56) )
=> leq(X55,X57) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(184, 0), 0)') ).
fof('ass(cond(goal(177), 0), 0)',axiom,
! [X58,X59,X60] :
( ( ( less(X59,X60)
& leq(X58,X59) )
| ( leq(X59,X60)
& less(X58,X59) ) )
=> less(X58,X60) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(177), 0), 0)') ).
fof('ass(cond(168, 0), 0)',axiom,
! [X61,X62,X63] :
( ( less(X62,X63)
& less(X61,X62) )
=> less(X61,X63) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(168, 0), 0)') ).
fof('ass(cond(goal(88), 0), 2)',axiom,
! [X84,X85] :
( ~ ? [X86] : X84 = vplus(X85,X86)
| ~ ? [X87] : X85 = vplus(X84,X87) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 2)') ).
fof('ass(cond(81, 0), 0)',axiom,
! [X88,X89] :
( X88 != X89
=> ! [X90] : vplus(X90,X88) != vplus(X90,X89) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(81, 0), 0)') ).
fof('ass(cond(goal(202), 0), 1)',axiom,
! [X47,X48,X49] :
( vplus(X47,X49) = vplus(X48,X49)
=> X47 = X48 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(202), 0), 1)') ).
fof('ass(cond(conjunct1(conjunct2(307)), 0), 0)',axiom,
! [X4,X5,X6] :
( vmul(X4,X5) = vmul(X6,X5)
=> X4 = X6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(conjunct1(conjunct2(307)), 0), 0)') ).
fof('ass(cond(189, 0), 0)',axiom,
! [X53,X54] : greater(vplus(X53,X54),X53),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(189, 0), 0)') ).
fof('def(cond(conseq(axiom(3)), 17), 1)',axiom,
! [X68,X69] :
( leq(X69,X68)
<=> ( less(X69,X68)
| X69 = X68 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 17), 1)') ).
fof('def(cond(conseq(axiom(3)), 16), 1)',axiom,
! [X70,X71] :
( geq(X71,X70)
<=> ( greater(X71,X70)
| X71 = X70 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 16), 1)') ).
fof('ass(cond(163, 0), 0)',axiom,
! [X64,X65] :
( leq(X64,X65)
=> geq(X65,X64) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(163, 0), 0)') ).
fof('ass(cond(158, 0), 0)',axiom,
! [X66,X67] :
( geq(X66,X67)
=> leq(X67,X66) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(158, 0), 0)') ).
fof('ass(cond(140, 0), 0)',axiom,
! [X74,X75] :
( greater(X74,X75)
=> less(X75,X74) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(140, 0), 0)') ).
fof('ass(cond(147, 0), 0)',axiom,
! [X72,X73] :
( less(X72,X73)
=> greater(X73,X72) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(147, 0), 0)') ).
fof('ass(cond(goal(130), 0), 0)',axiom,
! [X76,X77] :
( X76 = X77
| greater(X76,X77)
| less(X76,X77) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 0)') ).
fof('ass(cond(61, 0), 0)',axiom,
! [X93,X94] : vplus(X94,X93) = vplus(X93,X94),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(61, 0), 0)') ).
fof('ass(cond(270, 0), 0)',axiom,
! [X23,X24] : vmul(X23,X24) = vmul(X24,X23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(270, 0), 0)') ).
fof('ass(cond(goal(88), 0), 3)',axiom,
! [X84,X85] :
( X84 != X85
| ~ ? [X86] : X84 = vplus(X85,X86) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 3)') ).
fof('ass(cond(goal(88), 0), 1)',axiom,
! [X84,X85] :
( X84 != X85
| ~ ? [X87] : X85 = vplus(X84,X87) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 1)') ).
fof('ass(cond(73, 0), 0)',axiom,
! [X91,X92] : X92 != vplus(X91,X92),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(73, 0), 0)') ).
fof('ass(cond(253, 0), 0)',axiom,
! [X27] : vmul(v1,X27) = X27,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(253, 0), 0)') ).
fof('ass(cond(228, 0), 0)',axiom,
! [X34] : geq(X34,v1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(228, 0), 0)') ).
fof('holds(conjunct2(314), 513, 0)',axiom,
greater(vd511,vd512),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conjunct2(314), 513, 0)') ).
fof('holds(conjunct1(314), 510, 0)',axiom,
greater(vd508,vd509),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conjunct1(314), 510, 0)') ).
fof(i_0_57,plain,
! [X275,X276] : vmul(vsucc(X275),X276) = vplus(vmul(X275,X276),X276),
inference(variable_rename,[status(thm)],['ass(cond(261, 0), 0)']) ).
fof(i_0_58,plain,
! [X385,X386] :
( vplus(X385,vsucc(X386)) = vsucc(vplus(X385,X386))
& vplus(X385,v1) = vsucc(X385) ),
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_59,plain,
! [X278,X279] :
( vmul(X278,vsucc(X279)) = vplus(vmul(X278,X279),X278)
& vmul(X278,v1) = X278 ),
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_60,plain,
! [X379,X380] : vplus(vsucc(X379),X380) = vsucc(vplus(X379,X380)),
inference(variable_rename,[status(thm)],['ass(cond(52, 0), 0)']) ).
fof(i_0_61,plain,
! [X76,X77] :
( ~ greater(X76,X77)
| ~ less(X76,X77) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 2)']) ).
fof(i_0_62,plain,
! [X391,X392] :
( vsucc(X391) != vsucc(X392)
| X391 = X392 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(antec(axiom(3)), imp(antec(axiom(3))))'])]) ).
fof(i_0_63,plain,
! [X389,X390] :
( X389 = X390
| vsucc(X389) != vsucc(X390) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(6, 0), 0)'])]) ).
fof(i_0_64,plain,
! [X76,X77] :
( X76 != X77
| ~ less(X76,X77) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 1)']) ).
fof(i_0_65,plain,
! [X76,X77] :
( X76 != X77
| ~ greater(X76,X77) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 3)']) ).
fof(i_0_66,plain,
! [X381] : vplus(v1,X381) = vsucc(X381),
inference(variable_rename,[status(thm)],['ass(cond(43, 0), 0)']) ).
fof(i_0_67,plain,
! [X388] : vsucc(X388) != X388,
inference(variable_rename,[status(thm)],['ass(cond(12, 0), 0)']) ).
fof(i_0_68,plain,
! [X387] :
( X387 = v1
| X387 = vsucc(vskolem2(X387)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(20, 0), 0)'])]) ).
fof(i_0_69,plain,
! [X393] : vsucc(X393) != v1,
inference(variable_rename,[status(thm)],['qu(restrictor(axiom(1)), holds(scope(axiom(1)), 2, 0))']) ).
fof(i_0_70,plain,
! [X297,X298,X299] :
( ~ less(vplus(X297,X299),vplus(X298,X299))
| less(X297,X298) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(202), 0), 0)'])]) ).
fof(i_0_71,plain,
! [X249,X250,X251] :
( ~ less(vmul(X249,X250),vmul(X251,X250))
| less(X249,X251) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(conjunct2(conjunct2(307)), 0), 0)'])]) ).
fof(i_0_72,plain,
! [X303,X304,X305] :
( ~ greater(vplus(X303,X305),vplus(X304,X305))
| greater(X303,X304) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(202), 0), 2)'])]) ).
fof(i_0_73,plain,
! [X255,X256,X257] :
( ~ greater(vmul(X255,X256),vmul(X257,X256))
| greater(X255,X257) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(conjunct1(307), 0), 0)'])]) ).
fof(i_0_74,plain,
! [X285,X286,X287,X288] :
( ~ geq(X287,X288)
| ~ geq(X285,X286)
| geq(vplus(X285,X287),vplus(X286,X288)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(223, 0), 0)'])]) ).
fof(i_0_75,plain,
! [X289,X290,X291,X292] :
( ( ~ greater(X291,X292)
| ~ geq(X289,X290)
| greater(vplus(X289,X291),vplus(X290,X292)) )
& ( ~ geq(X291,X292)
| ~ greater(X289,X290)
| greater(vplus(X289,X291),vplus(X290,X292)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(216), 0), 0)'])])]) ).
fof(i_0_76,plain,
! [X293,X294,X295,X296] :
( ~ greater(X295,X296)
| ~ greater(X293,X294)
| greater(vplus(X293,X295),vplus(X294,X296)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(209, 0), 0)'])]) ).
fof(i_0_77,plain,
! [X270,X271,X272] : vmul(X270,vplus(X271,X272)) = vplus(vmul(X270,X271),vmul(X270,X272)),
inference(variable_rename,[status(thm)],['ass(cond(281, 0), 0)']) ).
fof(i_0_78,plain,
! [X306,X307,X308] :
( ~ less(X306,X307)
| less(vplus(X306,X308),vplus(X307,X308)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(193), 0), 0)'])]) ).
fof(i_0_79,plain,
! [X258,X259,X260] :
( ~ less(X259,X260)
| less(vmul(X259,X258),vmul(X260,X258)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(299, 0), 0)'])]) ).
fof(i_0_80,plain,
! [X312,X313,X314] :
( ~ greater(X312,X313)
| greater(vplus(X312,X314),vplus(X313,X314)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(193), 0), 2)'])]) ).
fof(i_0_81,plain,
! [X264,X265,X266] :
( ~ greater(X265,X266)
| greater(vmul(X265,X264),vmul(X266,X264)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(299, 0), 2)'])]) ).
fof(i_0_82,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_83,plain,
! [X358,X359] :
( X358 = X359
| X358 = vplus(X359,esk3_2(X358,X359))
| X359 = vplus(X358,esk4_2(X358,X359)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['ass(cond(goal(88), 0), 0)'])]) ).
fof(i_0_84,plain,
! [X382,X383,X384] : vplus(vplus(X382,X383),X384) = vplus(X382,vplus(X383,X384)),
inference(variable_rename,[status(thm)],['ass(cond(33, 0), 0)']) ).
fof(i_0_85,plain,
! [X267,X268,X269] : vmul(vmul(X267,X268),X269) = vmul(X267,vmul(X268,X269)),
inference(variable_rename,[status(thm)],['ass(cond(290, 0), 0)']) ).
cnf(i_0_86,plain,
vmul(vsucc(X1),X2) = vplus(vmul(X1,X2),X2),
inference(split_conjunct,[status(thm)],[i_0_57]) ).
cnf(i_0_87,plain,
vplus(X1,v1) = vsucc(X1),
inference(split_conjunct,[status(thm)],[i_0_58]) ).
cnf(i_0_88,plain,
vmul(X1,vsucc(X2)) = vplus(vmul(X1,X2),X1),
inference(split_conjunct,[status(thm)],[i_0_59]) ).
cnf(i_0_89,plain,
vplus(vsucc(X1),X2) = vsucc(vplus(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_60]) ).
cnf(i_0_90,plain,
vplus(X1,vsucc(X2)) = vsucc(vplus(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_58]) ).
fof(i_0_91,plain,
! [X280,X281] :
( ~ less(X280,vplus(X281,v1))
| leq(X280,X281) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(241, 0), 0)'])]) ).
fof(i_0_92,plain,
! [X352,X353,X355,X356,X357] :
( ( ~ greater(X353,X352)
| X353 = vplus(X352,esk2_2(X352,X353)) )
& ( X356 != vplus(X355,X357)
| greater(X356,X355) ) ),
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_93,plain,
! [X346,X347,X349,X350,X351] :
( ( ~ less(X347,X346)
| X346 = vplus(X347,esk1_2(X346,X347)) )
& ( X349 != vplus(X350,X351)
| less(X350,X349) ) ),
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_94,plain,
! [X282,X283] :
( ~ greater(X282,X283)
| geq(X282,vplus(X283,v1)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(234, 0), 0)'])]) ).
fof(i_0_95,plain,
! [X317,X318,X319] :
( ~ leq(X318,X319)
| ~ leq(X317,X318)
| leq(X317,X319) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(184, 0), 0)'])]) ).
fof(i_0_96,plain,
! [X320,X321,X322] :
( ( ~ less(X321,X322)
| ~ leq(X320,X321)
| less(X320,X322) )
& ( ~ leq(X321,X322)
| ~ less(X320,X321)
| less(X320,X322) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(177), 0), 0)'])])]) ).
fof(i_0_97,plain,
! [X323,X324,X325] :
( ~ less(X324,X325)
| ~ less(X323,X324)
| less(X323,X325) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(168, 0), 0)'])]) ).
fof(i_0_98,plain,
! [X365,X366,X367,X368] :
( X365 != vplus(X366,X367)
| X366 != vplus(X365,X368) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 2)'])])]) ).
fof(i_0_99,plain,
! [X372,X373,X374] :
( X372 = X373
| vplus(X374,X372) != vplus(X374,X373) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(81, 0), 0)'])])]) ).
fof(i_0_100,plain,
! [X300,X301,X302] :
( vplus(X300,X302) != vplus(X301,X302)
| X300 = X301 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(202), 0), 1)'])]) ).
fof(i_0_101,plain,
! [X252,X253,X254] :
( vmul(X252,X253) != vmul(X254,X253)
| X252 = X254 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(conjunct1(conjunct2(307)), 0), 0)'])]) ).
fof(i_0_102,plain,
! [X342,X343] :
( ~ greater(X342,X343)
| ~ less(X342,X343) ),
inference(variable_rename,[status(thm)],[i_0_61]) ).
cnf(i_0_103,plain,
( X1 = X2
| vsucc(X1) != vsucc(X2) ),
inference(split_conjunct,[status(thm)],[i_0_62]) ).
cnf(i_0_104,plain,
( X1 = X2
| vsucc(X1) != vsucc(X2) ),
inference(split_conjunct,[status(thm)],[i_0_63]) ).
fof(i_0_105,plain,
! [X315,X316] : greater(vplus(X315,X316),X315),
inference(variable_rename,[status(thm)],['ass(cond(189, 0), 0)']) ).
fof(i_0_106,plain,
! [X330,X331] :
( ( ~ leq(X331,X330)
| less(X331,X330)
| X331 = X330 )
& ( ~ less(X331,X330)
| leq(X331,X330) )
& ( X331 != X330
| leq(X331,X330) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['def(cond(conseq(axiom(3)), 17), 1)'])])]) ).
fof(i_0_107,plain,
! [X332,X333] :
( ( ~ geq(X333,X332)
| greater(X333,X332)
| X333 = X332 )
& ( ~ greater(X333,X332)
| geq(X333,X332) )
& ( X333 != X332
| geq(X333,X332) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['def(cond(conseq(axiom(3)), 16), 1)'])])]) ).
fof(i_0_108,plain,
! [X326,X327] :
( ~ leq(X326,X327)
| geq(X327,X326) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(163, 0), 0)'])]) ).
fof(i_0_109,plain,
! [X328,X329] :
( ~ geq(X328,X329)
| leq(X329,X328) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(158, 0), 0)'])]) ).
fof(i_0_110,plain,
! [X336,X337] :
( ~ greater(X336,X337)
| less(X337,X336) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(140, 0), 0)'])]) ).
fof(i_0_111,plain,
! [X334,X335] :
( ~ less(X334,X335)
| greater(X335,X334) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(147, 0), 0)'])]) ).
fof(i_0_112,plain,
! [X338,X339] :
( X338 = X339
| greater(X338,X339)
| less(X338,X339) ),
inference(variable_rename,[status(thm)],['ass(cond(goal(130), 0), 0)']) ).
fof(i_0_113,plain,
! [X377,X378] : vplus(X378,X377) = vplus(X377,X378),
inference(variable_rename,[status(thm)],['ass(cond(61, 0), 0)']) ).
fof(i_0_114,plain,
! [X273,X274] : vmul(X273,X274) = vmul(X274,X273),
inference(variable_rename,[status(thm)],['ass(cond(270, 0), 0)']) ).
fof(i_0_115,plain,
! [X369,X370,X371] :
( X369 != X370
| X369 != vplus(X370,X371) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 3)'])])]) ).
fof(i_0_116,plain,
! [X362,X363,X364] :
( X362 != X363
| X363 != vplus(X362,X364) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(goal(88), 0), 1)'])])]) ).
fof(i_0_117,plain,
! [X340,X341] :
( X340 != X341
| ~ less(X340,X341) ),
inference(variable_rename,[status(thm)],[i_0_64]) ).
fof(i_0_118,plain,
! [X344,X345] :
( X344 != X345
| ~ greater(X344,X345) ),
inference(variable_rename,[status(thm)],[i_0_65]) ).
cnf(i_0_119,plain,
vplus(v1,X1) = vsucc(X1),
inference(split_conjunct,[status(thm)],[i_0_66]) ).
fof(i_0_120,plain,
! [X375,X376] : X376 != vplus(X375,X376),
inference(variable_rename,[status(thm)],['ass(cond(73, 0), 0)']) ).
cnf(i_0_121,plain,
vsucc(X1) != X1,
inference(split_conjunct,[status(thm)],[i_0_67]) ).
cnf(i_0_122,plain,
( X1 = v1
| X1 = vsucc(vskolem2(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_68]) ).
cnf(i_0_123,plain,
vsucc(X1) != v1,
inference(split_conjunct,[status(thm)],[i_0_69]) ).
fof(i_0_124,plain,
! [X277] : vmul(v1,X277) = X277,
inference(variable_rename,[status(thm)],['ass(cond(253, 0), 0)']) ).
fof(i_0_125,plain,
! [X284] : geq(X284,v1),
inference(variable_rename,[status(thm)],['ass(cond(228, 0), 0)']) ).
cnf(i_0_126,plain,
( less(X1,X3)
| ~ less(vplus(X1,X2),vplus(X3,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_127,plain,
( less(X1,X3)
| ~ less(vmul(X1,X2),vmul(X3,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_128,plain,
( greater(X1,X3)
| ~ greater(vplus(X1,X2),vplus(X3,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_129,plain,
( greater(X1,X3)
| ~ greater(vmul(X1,X2),vmul(X3,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_130,plain,
( geq(vplus(X3,X1),vplus(X4,X2))
| ~ geq(X1,X2)
| ~ geq(X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_131,plain,
( greater(vplus(X3,X1),vplus(X4,X2))
| ~ greater(X1,X2)
| ~ geq(X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_132,plain,
( greater(vplus(X3,X1),vplus(X4,X2))
| ~ geq(X1,X2)
| ~ greater(X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_133,plain,
( greater(vplus(X3,X1),vplus(X4,X2))
| ~ greater(X1,X2)
| ~ greater(X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_76]),
[final] ).
cnf(i_0_134,plain,
vmul(X1,vplus(X2,X3)) = vplus(vmul(X1,X2),vmul(X1,X3)),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_135,plain,
( less(vplus(X1,X3),vplus(X2,X3))
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_136,plain,
( less(vmul(X1,X3),vmul(X2,X3))
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_79]),
[final] ).
cnf(i_0_137,plain,
( greater(vplus(X1,X3),vplus(X2,X3))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_138,plain,
( greater(vmul(X1,X3),vmul(X2,X3))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_139,negated_conjecture,
~ greater(vmul(vd508,vd511),vmul(vd509,vd511)),
inference(split_conjunct,[status(thm)],[i_0_82]),
[final] ).
cnf(i_0_140,plain,
( X1 = X2
| X1 = vplus(X2,esk3_2(X1,X2))
| X2 = vplus(X1,esk4_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_141,plain,
vplus(vplus(X1,X2),X3) = vplus(X1,vplus(X2,X3)),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_142,plain,
vmul(vmul(X1,X2),X3) = vmul(X1,vmul(X2,X3)),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_143,plain,
vmul(vplus(X1,v1),X2) = vplus(vmul(X1,X2),X2),
inference(rw,[status(thm)],[i_0_86,c_0_87]),
[final] ).
cnf(i_0_144,plain,
vmul(X1,vplus(X2,v1)) = vplus(vmul(X1,X2),X1),
inference(rw,[status(thm)],[i_0_88,c_0_87]),
[final] ).
cnf(i_0_145,plain,
vplus(vplus(X1,v1),X2) = vplus(vplus(X1,X2),v1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_89,c_0_87]),c_0_87]),
[final] ).
cnf(i_0_146,plain,
vplus(X1,vplus(X2,v1)) = vplus(vplus(X1,X2),v1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_90,c_0_87]),c_0_87]),
[final] ).
cnf(i_0_147,plain,
( leq(X1,X2)
| ~ less(X1,vplus(X2,v1)) ),
inference(split_conjunct,[status(thm)],[i_0_91]),
[final] ).
cnf(i_0_148,plain,
( X1 = vplus(X2,esk2_2(X2,X1))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_92]),
[final] ).
cnf(i_0_149,plain,
( X2 = vplus(X1,esk1_2(X2,X1))
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_93]),
[final] ).
cnf(i_0_150,plain,
( geq(X1,vplus(X2,v1))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_94]),
[final] ).
cnf(i_0_151,plain,
( leq(X3,X2)
| ~ leq(X1,X2)
| ~ leq(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_95]),
[final] ).
cnf(i_0_152,plain,
( less(X3,X2)
| ~ less(X1,X2)
| ~ leq(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_96]),
[final] ).
cnf(i_0_153,plain,
( less(X3,X2)
| ~ leq(X1,X2)
| ~ less(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_96]),
[final] ).
cnf(i_0_154,plain,
( less(X3,X2)
| ~ less(X1,X2)
| ~ less(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_97]),
[final] ).
cnf(i_0_155,plain,
( X1 != vplus(X2,X3)
| X2 != vplus(X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_98]),
[final] ).
cnf(i_0_156,plain,
( X1 = X2
| vplus(X3,X1) != vplus(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_99]),
[final] ).
cnf(i_0_157,plain,
( X1 = X3
| vplus(X1,X2) != vplus(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_100]),
[final] ).
cnf(i_0_158,plain,
( X1 = X3
| vmul(X1,X2) != vmul(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_101]),
[final] ).
cnf(i_0_159,plain,
( ~ greater(X1,X2)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_102]),
[final] ).
cnf(i_0_160,plain,
( X1 = X2
| vplus(X1,v1) != vplus(X2,v1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_103,c_0_87]),c_0_87]),
[final] ).
cnf(i_0_161,plain,
( X1 = X2
| vplus(X1,v1) != vplus(X2,v1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_104,c_0_87]),c_0_87]),
[final] ).
cnf(i_0_162,plain,
greater(vplus(X1,X2),X1),
inference(split_conjunct,[status(thm)],[i_0_105]),
[final] ).
cnf(i_0_163,plain,
( less(X1,X2)
| X1 = X2
| ~ leq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_106]),
[final] ).
cnf(i_0_164,plain,
( greater(X1,X2)
| X1 = X2
| ~ geq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_107]),
[final] ).
cnf(i_0_165,plain,
( less(X2,X1)
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_93]),
[final] ).
cnf(i_0_166,plain,
( greater(X1,X2)
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_92]),
[final] ).
cnf(i_0_167,plain,
( geq(X1,X2)
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_107]),
[final] ).
cnf(i_0_168,plain,
( geq(X2,X1)
| ~ leq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_108]),
[final] ).
cnf(i_0_169,plain,
( leq(X1,X2)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_106]),
[final] ).
cnf(i_0_170,plain,
( leq(X2,X1)
| ~ geq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_171,plain,
( less(X2,X1)
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_110]),
[final] ).
cnf(i_0_172,plain,
( greater(X2,X1)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_111]),
[final] ).
cnf(i_0_173,plain,
( X1 = X2
| greater(X1,X2)
| less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_112]),
[final] ).
cnf(i_0_174,plain,
vplus(X1,X2) = vplus(X2,X1),
inference(split_conjunct,[status(thm)],[i_0_113]),
[final] ).
cnf(i_0_175,plain,
vmul(X1,X2) = vmul(X2,X1),
inference(split_conjunct,[status(thm)],[i_0_114]),
[final] ).
cnf(i_0_176,plain,
( X1 != X2
| X1 != vplus(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_115]),
[final] ).
cnf(i_0_177,plain,
( X1 != X2
| X2 != vplus(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_116]),
[final] ).
cnf(i_0_178,plain,
( X1 != X2
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_117]),
[final] ).
cnf(i_0_179,plain,
( X1 != X2
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_118]),
[final] ).
cnf(i_0_180,plain,
vplus(v1,X1) = vplus(X1,v1),
inference(rw,[status(thm)],[i_0_119,c_0_87]),
[final] ).
cnf(i_0_181,plain,
X1 != vplus(X2,X1),
inference(split_conjunct,[status(thm)],[i_0_120]),
[final] ).
cnf(i_0_182,plain,
vplus(X1,v1) != X1,
inference(rw,[status(thm)],[i_0_121,c_0_87]),
[final] ).
cnf(i_0_183,plain,
( X1 = v1
| X1 = vplus(vskolem2(X1),v1) ),
inference(rw,[status(thm)],[i_0_122,c_0_87]),
[final] ).
cnf(i_0_184,plain,
vplus(X1,v1) != v1,
inference(rw,[status(thm)],[i_0_123,c_0_87]),
[final] ).
cnf(i_0_185,plain,
( geq(X1,X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_107]),
[final] ).
cnf(i_0_186,plain,
( leq(X1,X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_106]),
[final] ).
cnf(i_0_187,plain,
vmul(v1,X1) = X1,
inference(split_conjunct,[status(thm)],[i_0_124]),
[final] ).
cnf(i_0_188,plain,
vmul(X1,v1) = X1,
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_189,plain,
geq(X1,v1),
inference(split_conjunct,[status(thm)],[i_0_125]),
[final] ).
cnf(i_0_190,plain,
greater(vd511,vd512),
inference(split_conjunct,[status(thm)],['holds(conjunct2(314), 513, 0)']),
[final] ).
cnf(i_0_191,plain,
greater(vd508,vd509),
inference(split_conjunct,[status(thm)],['holds(conjunct1(314), 510, 0)']),
[final] ).
cnf(i_0_192,axiom,
X1 = X1 ).
cnf(i_0_193,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_194,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_195,axiom,
( X1 != X2
| vplus(X1,X3) = vplus(X2,X3) ) ).
cnf(i_0_196,axiom,
( X1 != X2
| vplus(X3,X1) = vplus(X3,X2) ) ).
cnf(i_0_197,axiom,
( X1 != X2
| vmul(X1,X3) = vmul(X2,X3) ) ).
cnf(i_0_198,axiom,
( X1 != X2
| vmul(X3,X1) = vmul(X3,X2) ) ).
cnf(i_0_199,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_200,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_201,axiom,
( X1 != X2
| ~ greater(X1,X3)
| greater(X2,X3) ) ).
cnf(i_0_202,axiom,
( X1 != X2
| ~ greater(X3,X1)
| greater(X3,X2) ) ).
cnf(i_0_203,axiom,
( X1 != X2
| ~ geq(X1,X3)
| geq(X2,X3) ) ).
cnf(i_0_204,axiom,
( X1 != X2
| ~ geq(X3,X1)
| geq(X3,X2) ) ).
cnf(i_0_205,axiom,
( X1 != X2
| ~ leq(X1,X3)
| leq(X2,X3) ) ).
cnf(i_0_206,axiom,
( X1 != X2
| ~ leq(X3,X1)
| leq(X3,X2) ) ).
cnf(i_0_192_001,axiom,
X1 = X1 ).
cnf(i_0_193_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_194_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_195_004,axiom,
( X1 != X2
| vplus(X1,X3) = vplus(X2,X3) ) ).
cnf(i_0_196_005,axiom,
( X1 != X2
| vplus(X3,X1) = vplus(X3,X2) ) ).
cnf(i_0_197_006,axiom,
( X1 != X2
| vmul(X1,X3) = vmul(X2,X3) ) ).
cnf(i_0_198_007,axiom,
( X1 != X2
| vmul(X3,X1) = vmul(X3,X2) ) ).
cnf(i_0_199_008,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_200_009,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_201_010,axiom,
( X1 != X2
| ~ greater(X1,X3)
| greater(X2,X3) ) ).
cnf(i_0_202_011,axiom,
( X1 != X2
| ~ greater(X3,X1)
| greater(X3,X2) ) ).
cnf(i_0_203_012,axiom,
( X1 != X2
| ~ geq(X1,X3)
| geq(X2,X3) ) ).
cnf(i_0_204_013,axiom,
( X1 != X2
| ~ geq(X3,X1)
| geq(X3,X2) ) ).
cnf(i_0_205_014,axiom,
( X1 != X2
| ~ leq(X1,X3)
| leq(X2,X3) ) ).
cnf(i_0_206_015,axiom,
( X1 != X2
| ~ leq(X3,X1)
| leq(X3,X2) ) ).
cnf(i_0_207,plain,
X1 = X1,
inference(equality_inference,[],[156]) ).
cnf(i_0_208,plain,
X1 = X1,
inference(equality_inference,[],[157]) ).
cnf(i_0_209,plain,
X1 = X1,
inference(equality_inference,[],[158]) ).
cnf(i_0_210,plain,
less(X1,vplus(X1,X2)),
inference(equality_inference,[],[165]) ).
cnf(i_0_211,plain,
greater(vplus(X1,X2),X1),
inference(equality_inference,[],[166]) ).
cnf(i_0_212,plain,
~ less(X1,X1),
inference(equality_inference,[],[178]) ).
cnf(i_0_213,plain,
~ greater(X1,X1),
inference(equality_inference,[],[179]) ).
cnf(i_0_214,plain,
geq(X1,X1),
inference(equality_inference,[],[185]) ).
cnf(i_0_215,plain,
leq(X1,X1),
inference(equality_inference,[],[186]) ).
cnf(i_0_216,plain,
$false,
inference(scs_inference,[],[i_0_139,i_0_191,i_0_138]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM854+1 : 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.15/0.33 % Computer : n021.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:16:55 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 0.31/1.62 % Version : CSE_E---1.7
% 0.31/1.62 % Problem : theBenchmark.p
% 0.31/1.62 % SZS status Theorem for theBenchmark.p
% 0.31/1.62 % SZS output start CNFRefutation
% See solution above
% 0.31/1.64 % Total time : 1.272s
%------------------------------------------------------------------------------