%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : GEO319+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:30:04 PM UTC 2026
% Result : Theorem 268.29s 34.94s
% Output : CNFRefutation 268.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 31
% Syntax : Number of formulae : 199 ( 61 unt; 0 def)
% Number of atoms : 933 ( 343 equ)
% Maximal formula atoms : 32 ( 4 avg)
% Number of connectives : 1280 ( 546 ~; 544 |; 166 &)
% ( 2 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 14 con; 0-3 aty)
% Number of variables : 462 ( 0 sgn 166 !; 48 ?)
% Comments :
%------------------------------------------------------------------------------
fof('qu(cond(axiom(160), 0), imp(cond(axiom(160), 0)))',axiom,
! [X64,X65] :
( ( ? [X67] :
( rpoint(X67)
& X64 = X67 )
& ? [X66] :
( rpoint(X66)
& X65 = X66 ) )
=> ? [X68] :
( rreal(X68)
& vf(X64,X65) = X68 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(160), 0), imp(cond(axiom(160), 0)))') ).
fof('qu(cond(axiom(180), 0), imp(cond(axiom(180), 0)))',axiom,
! [X199,X200,X201] :
( ( ? [X204] :
( rpoint(X204)
& X199 = X204 )
& ? [X203] :
( rpoint(X203)
& X200 = X203 )
& ? [X202] :
( rpoint(X202)
& X201 = X202 )
& rR(X200,X199,X201) )
=> vplus(vf(X199,X200),vf(X200,X201)) = vf(X199,X201) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(180), 0), imp(cond(axiom(180), 0)))') ).
fof('qu(cond(axiom(166), 0), imp(cond(axiom(166), 0)))',axiom,
! [X60,X61] :
( ( ? [X63] :
( rpoint(X63)
& X60 = X63 )
& ? [X62] :
( rpoint(X62)
& X61 = X62 ) )
=> vf(X60,X61) = vf(X61,X60) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(166), 0), imp(cond(axiom(166), 0)))') ).
fof('and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))',axiom,
( ? [X9] :
( rpoint(X9)
& vd1287 = X9 )
& ? [X8] :
( rpoint(X8)
& vd1288 = X8 )
& ? [X7] :
( rpoint(X7)
& vd1289 = X7 )
& vd1287 != vd1288
& vd1287 != vd1289
& vd1288 != vd1289
& vf(vd1287,vd1288) = vf(vd1287,vd1289) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))') ).
fof('qu(cond(axiom(143), 0), imp(cond(axiom(143), 0)))',axiom,
! [X181,X182,X183,X184] :
( ( rreal(X182)
& X181 = X182
& rreal(X184)
& X183 = X184 )
=> vplus(X181,X183) = vplus(X183,X181) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(143), 0), imp(cond(axiom(143), 0)))') ).
fof('qu(cond(axiom(81), 0), imp(cond(axiom(81), 0)))',axiom,
! [X1,X2,X3] :
( ( ? [X6] :
( rpoint(X6)
& X1 = X6 )
& ? [X5] :
( rpoint(X5)
& X2 = X5 )
& ? [X4] :
( rpoint(X4)
& X3 = X4 )
& rR(X2,X1,X3) )
=> ( rR(X2,X3,X1)
& X1 != X2
& X1 != X3
& ~ rR(X1,X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(81), 0), imp(cond(axiom(81), 0)))') ).
fof('ass(cond(156, 0), 0)',axiom,
! [X171,X172,X173,X174,X175,X176] :
( ( rreal(X172)
& X171 = X172
& rreal(X174)
& X173 = X174
& rreal(X176)
& X175 = X176
& vplus(X171,X175) = vplus(X173,X175) )
=> X171 = X173 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(156, 0), 0)') ).
fof('holds(conjunct1(conjunct2(conjunct2(368))), 1333, 0)',conjecture,
vd1329 != vd1302,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conjunct1(conjunct2(conjunct2(368))), 1333, 0)') ).
fof('pred(348, 1)',axiom,
rpoint(vd1300),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(348, 1)') ).
fof('pred(348, 4)',axiom,
vd1299 = vd1300,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(348, 4)') ).
fof('qu(cond(axiom(87), 0), imp(cond(axiom(87), 0)))',axiom,
! [X420,X421,X422,X423] :
( ( ? [X427] :
( rpoint(X427)
& X420 = X427 )
& ? [X426] :
( rpoint(X426)
& X421 = X426 )
& ? [X425] :
( rpoint(X425)
& X422 = X425 )
& ? [X424] :
( rpoint(X424)
& X423 = X424 )
& rR(X421,X420,X422)
& rR(X423,X420,X421) )
=> rR(X423,X420,X422) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(87), 0), imp(cond(axiom(87), 0)))') ).
fof('and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))',axiom,
( rR(vd1288,vd1287,vd1299)
& rpoint(vd1303)
& rR(vd1289,vd1287,vd1302)
& vd1302 = vd1303 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))') ).
fof('holds(conjunct1(367), 1330, 0)',axiom,
rR(vd1329,vd1287,vd1299),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conjunct1(367), 1330, 0)') ).
fof('pred(367, 0)',axiom,
rpoint(vd1329),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(367, 0)') ).
fof('qu(cond(axiom(149), 0), imp(cond(axiom(149), 0)))',axiom,
! [X69,X70] :
( ( rreal(X70)
& X69 = X70 )
=> ~ rless(X69,X69) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(149), 0), imp(cond(axiom(149), 0)))') ).
fof('qu(cond(axiom(153), 0), imp(cond(axiom(153), 0)))',axiom,
! [X224,X225,X226,X227,X228,X229] :
( ( rreal(X225)
& X224 = X225
& rreal(X227)
& X226 = X227
& rreal(X229)
& X228 = X229
& rless(X224,X226) )
=> rless(vplus(X224,X228),vplus(X226,X228)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(153), 0), imp(cond(axiom(153), 0)))') ).
fof('qu(cond(axiom(141), 0), imp(cond(axiom(141), 0)))',axiom,
! [X185,X186] :
( ( rreal(X186)
& X185 = X186 )
=> vplus(X185,v0) = X185 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(141), 0), imp(cond(axiom(141), 0)))') ).
fof('qu(cond(axiom(53), 0), imp(cond(axiom(53), 0)))',axiom,
! [X146,X147] :
( ( ? [X149] :
( rpoint(X149)
& X146 = X149 )
& ? [X148] :
( rpoint(X148)
& X147 = X148 )
& X146 != X147 )
=> ? [X150] :
( rcircle(X150)
& rcenter(X146,X150)
& ron(X147,X150) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(53), 0), imp(cond(axiom(53), 0)))') ).
fof('pred(axiom(137), 1)',axiom,
rreal(vd684),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(axiom(137), 1)') ).
fof('pred(axiom(137), 2)',axiom,
v0 = vd684,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(axiom(137), 2)') ).
fof('qu(cond(axiom(186), 0), imp(cond(axiom(186), 0)))',axiom,
! [X97,X98,X99,X100] :
( ( ? [X102] :
( rpoint(X102)
& X97 = X102 )
& ? [X101] :
( rpoint(X101)
& X98 = X101 )
& rcenter(X99,X100)
& ron(X98,X100) )
=> ( rless(vf(X99,X97),vf(X99,X98))
<=> rinside(X97,X100) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(186), 0), imp(cond(axiom(186), 0)))') ).
fof('qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))',axiom,
! [X205,X206] :
( rcenter(X205,X206)
=> rinside(X205,X206) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))') ).
fof('qu(cond(axiom(139), 0), imp(cond(axiom(139), 0)))',axiom,
! [X240,X241,X242,X243] :
( ( rreal(X241)
& X240 = X241
& rreal(X243)
& X242 = X243 )
=> ? [X244] :
( rreal(X244)
& vplus(X240,X242) = X244 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(139), 0), imp(cond(axiom(139), 0)))') ).
fof('qu(cond(axiom(91), 0), imp(cond(axiom(91), 0)))',axiom,
! [X187,X188,X189,X190,X191] :
( ( ? [X194] :
( rpoint(X194)
& X187 = X194 )
& ? [X193] :
( rpoint(X193)
& X188 = X193 )
& ? [X192] :
( rpoint(X192)
& X189 = X192 )
& X187 != X188
& X187 != X189
& X188 != X189
& rline(X191)
& ron(X187,X190)
& ron(X188,X190)
& ron(X189,X190)
& X190 = X191 )
=> ( rR(X189,X187,X188)
| rR(X187,X188,X189)
| rR(X188,X187,X189) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(91), 0), imp(cond(axiom(91), 0)))') ).
fof('qu(cond(axiom(85), 0), imp(cond(axiom(85), 0)))',axiom,
! [X10,X11,X12,X13,X14] :
( ( ? [X17] :
( rpoint(X17)
& X10 = X17 )
& ? [X16] :
( rpoint(X16)
& X11 = X16 )
& ? [X15] :
( rpoint(X15)
& X12 = X15 )
& rline(X14)
& rR(X11,X10,X12)
& ron(X10,X13)
& ron(X12,X13)
& X13 = X14 )
=> ron(X11,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(85), 0), imp(cond(axiom(85), 0)))') ).
fof('qu(cond(axiom(162), 0), imp(cond(axiom(162), 0)))',axiom,
! [X109,X110] :
( ( ? [X112] :
( rpoint(X112)
& X109 = X112 )
& ? [X111] :
( rpoint(X111)
& X110 = X111 ) )
=> ( vf(X109,X110) = v0
<=> X109 = X110 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(162), 0), imp(cond(axiom(162), 0)))') ).
fof('qu(cond(axiom(89), 0), imp(cond(axiom(89), 0)))',axiom,
! [X77,X78,X79,X80] :
( ( ? [X84] :
( rpoint(X84)
& X77 = X84 )
& ? [X83] :
( rpoint(X83)
& X78 = X83 )
& ? [X82] :
( rpoint(X82)
& X79 = X82 )
& ? [X81] :
( rpoint(X81)
& X80 = X81 )
& rR(X78,X77,X79)
& rR(X79,X78,X80) )
=> rR(X78,X77,X80) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(89), 0), imp(cond(axiom(89), 0)))') ).
fof('pred(s2(plural(346)), 0)',axiom,
ron(vd1288,vd1295),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(s2(plural(346)), 0)') ).
fof('pred(346, 0)',axiom,
rline(vd1295),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(346, 0)') ).
fof('pred(conjunct1(368), 0)',axiom,
ron(vd1329,vd1295),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(conjunct1(368), 0)') ).
fof('pred(s1(plural(346)), 0)',axiom,
ron(vd1287,vd1295),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(s1(plural(346)), 0)') ).
fof(c_0_31,plain,
! [X866,X867,X868,X869] :
( ( ~ rpoint(X869)
| X866 != X869
| ~ rpoint(X868)
| X867 != X868
| rreal(esk8_2(X866,X867)) )
& ( ~ rpoint(X869)
| X866 != X869
| ~ rpoint(X868)
| X867 != X868
| vf(X866,X867) = esk8_2(X866,X867) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(160), 0), imp(cond(axiom(160), 0)))'])])])])])]) ).
fof(c_0_32,plain,
! [X1015,X1016,X1017,X1018,X1019,X1020] :
( vplus(vf(X1015,X1016),vf(X1016,X1017)) = vf(X1015,X1017)
| ~ rpoint(X1020)
| X1015 != X1020
| ~ rpoint(X1019)
| X1016 != X1019
| ~ rpoint(X1018)
| X1017 != X1018
| ~ rR(X1016,X1015,X1017) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(180), 0), imp(cond(axiom(180), 0)))'])])])]) ).
fof(c_0_33,plain,
! [X862,X863,X864,X865] :
( vf(X862,X863) = vf(X863,X862)
| ~ rpoint(X865)
| X862 != X865
| ~ rpoint(X864)
| X863 != X864 ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(166), 0), imp(cond(axiom(166), 0)))'])])])]) ).
fof(c_0_34,plain,
( ? [X9] :
( rpoint(X9)
& vd1287 = X9 )
& ? [X8] :
( rpoint(X8)
& vd1288 = X8 )
& ? [X7] :
( rpoint(X7)
& vd1289 = X7 )
& vd1287 != vd1288
& vd1287 != vd1289
& vd1288 != vd1289
& vf(vd1287,vd1288) = vf(vd1287,vd1289) ),
inference(fof_simplification,[status(thm)],['and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))']) ).
fof(c_0_35,plain,
! [X989,X990,X991,X992] :
( vplus(X989,X991) = vplus(X991,X989)
| ~ rreal(X990)
| X989 != X990
| ~ rreal(X992)
| X991 != X992 ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(143), 0), imp(cond(axiom(143), 0)))'])])]) ).
cnf(c_0_36,plain,
( ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3
| rreal(esk8_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
cnf(c_0_37,plain,
( ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3
| vf(X1,X2) = esk8_2(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
cnf(c_0_38,plain,
( ~ rpoint(X6)
| X2 != X6
| ~ rpoint(X5)
| X1 != X5
| ~ rpoint(X4)
| X3 != X4
| ~ rR(X1,X2,X3)
| vplus(vf(X2,X1),vf(X1,X3)) = vf(X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
cnf(c_0_39,plain,
( ~ rpoint(X4)
| X3 != X4
| ~ rpoint(X2)
| X1 != X2
| vf(X3,X1) = vf(X1,X3) ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
fof(c_0_40,plain,
( rpoint(esk3_0)
& vd1287 = esk3_0
& rpoint(esk2_0)
& vd1288 = esk2_0
& rpoint(esk1_0)
& vd1289 = esk1_0
& vd1287 != vd1288
& vd1287 != vd1289
& vd1288 != vd1289
& vf(vd1287,vd1288) = vf(vd1287,vd1289) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[c_0_34])])]) ).
cnf(c_0_41,plain,
( ~ rreal(X4)
| X3 != X4
| ~ rreal(X2)
| X1 != X2
| vplus(X3,X1) = vplus(X1,X3) ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
cnf(c_0_42,plain,
( ~ rpoint(X2)
| ~ rpoint(X1)
| rreal(esk8_2(X1,X2)) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_36])]) ).
cnf(c_0_43,plain,
( ~ rpoint(X2)
| ~ rpoint(X1)
| esk8_2(X1,X2) = vf(X1,X2) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_37])]) ).
cnf(c_0_44,plain,
( ~ rR(X2,X1,X3)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X1)
| vplus(vf(X1,X2),vf(X2,X3)) = vf(X1,X3) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_38])])]) ).
cnf(c_0_45,plain,
( ~ rpoint(X1)
| ~ rpoint(X2)
| vf(X1,X2) = vf(X2,X1) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_39])]) ).
cnf(c_0_46,plain,
rpoint(esk2_0),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_47,plain,
vd1288 = esk2_0,
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_48,plain,
rpoint(esk3_0),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_49,plain,
vd1287 = esk3_0,
inference(split_conjunct,[status(thm)],[c_0_40]) ).
fof(c_0_50,plain,
! [X1,X2,X3] :
( ( ? [X6] :
( rpoint(X6)
& X1 = X6 )
& ? [X5] :
( rpoint(X5)
& X2 = X5 )
& ? [X4] :
( rpoint(X4)
& X3 = X4 )
& rR(X2,X1,X3) )
=> ( rR(X2,X3,X1)
& X1 != X2
& X1 != X3
& ~ rR(X1,X2,X3) ) ),
inference(fof_simplification,[status(thm)],['qu(cond(axiom(81), 0), imp(cond(axiom(81), 0)))']) ).
fof(c_0_51,plain,
! [X979,X980,X981,X982,X983,X984] :
( X979 = X981
| ~ rreal(X980)
| X979 != X980
| ~ rreal(X982)
| X981 != X982
| ~ rreal(X984)
| X983 != X984
| vplus(X979,X983) != vplus(X981,X983) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(156, 0), 0)'])])]) ).
cnf(c_0_52,plain,
( ~ rreal(X1)
| ~ rreal(X2)
| vplus(X1,X2) = vplus(X2,X1) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_41])]) ).
cnf(c_0_53,plain,
( ~ rpoint(X2)
| ~ rpoint(X1)
| rreal(vf(X1,X2)) ),
inference(spm,[status(thm)],[c_0_42,c_0_43]) ).
cnf(c_0_54,plain,
( ~ rR(X2,X1,X3)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X1)
| vplus(vf(X1,X2),vf(X3,X2)) = vf(X1,X3) ),
inference(spm,[status(thm)],[c_0_44,c_0_45]) ).
cnf(c_0_55,plain,
vf(vd1287,vd1288) = vf(vd1287,vd1289),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_56,plain,
rpoint(vd1288),
inference(rw,[status(thm)],[c_0_46,c_0_47]) ).
cnf(c_0_57,plain,
rpoint(vd1287),
inference(rw,[status(thm)],[c_0_48,c_0_49]) ).
fof(c_0_58,plain,
! [X761,X762,X763,X764,X765,X766] :
( ( ~ rpoint(X766)
| X761 != X766
| ~ rpoint(X765)
| X762 != X765
| ~ rpoint(X764)
| X763 != X764
| ~ rR(X762,X761,X763)
| rR(X762,X763,X761) )
& ( ~ rpoint(X766)
| X761 != X766
| ~ rpoint(X765)
| X762 != X765
| ~ rpoint(X764)
| X763 != X764
| ~ rR(X762,X761,X763)
| X761 != X762 )
& ( ~ rpoint(X766)
| X761 != X766
| ~ rpoint(X765)
| X762 != X765
| ~ rpoint(X764)
| X763 != X764
| ~ rR(X762,X761,X763)
| X761 != X763 )
& ( ~ rpoint(X766)
| X761 != X766
| ~ rpoint(X765)
| X762 != X765
| ~ rpoint(X764)
| X763 != X764
| ~ rR(X762,X761,X763)
| ~ rR(X761,X762,X763) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_50])])])])]) ).
fof(c_0_59,negated_conjecture,
~ ( vd1329 != vd1302 ),
inference(assume_negation,[status(cth)],['holds(conjunct1(conjunct2(conjunct2(368))), 1333, 0)']) ).
cnf(c_0_60,plain,
( ~ rreal(X6)
| X1 != X6
| ~ rreal(X5)
| X3 != X5
| ~ rreal(X4)
| X2 != X4
| vplus(X1,X2) != vplus(X3,X2)
| X1 = X3 ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
cnf(c_0_61,plain,
( ~ rR(X1,X3,X2)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X3)
| vplus(vf(X1,X2),vf(X3,X1)) = vf(X3,X2) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_52,c_0_44]),c_0_53]),c_0_53]) ).
cnf(c_0_62,plain,
( ~ rR(vd1288,X1,vd1287)
| ~ rpoint(X1)
| vplus(vf(X1,vd1288),vf(vd1287,vd1289)) = vf(X1,vd1287) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54,c_0_55]),c_0_56]),c_0_57])]) ).
cnf(c_0_63,plain,
( ~ rpoint(X6)
| X3 != X6
| ~ rpoint(X5)
| X1 != X5
| ~ rpoint(X4)
| X2 != X4
| ~ rR(X1,X3,X2)
| rR(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
cnf(c_0_64,plain,
rpoint(vd1300),
inference(split_conjunct,[status(thm)],['pred(348, 1)']) ).
cnf(c_0_65,plain,
vd1299 = vd1300,
inference(split_conjunct,[status(thm)],['pred(348, 4)']) ).
fof(c_0_66,plain,
! [X1236,X1237,X1238,X1239,X1240,X1241,X1242,X1243] :
( rR(X1239,X1236,X1238)
| ~ rpoint(X1243)
| X1236 != X1243
| ~ rpoint(X1242)
| X1237 != X1242
| ~ rpoint(X1241)
| X1238 != X1241
| ~ rpoint(X1240)
| X1239 != X1240
| ~ rR(X1237,X1236,X1238)
| ~ rR(X1239,X1236,X1237) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(87), 0), imp(cond(axiom(87), 0)))'])])])]) ).
fof(c_0_67,negated_conjecture,
vd1329 = vd1302,
inference(fof_simplification,[status(thm)],[c_0_59]) ).
cnf(c_0_68,plain,
( ~ rreal(X3)
| ~ rreal(X2)
| ~ rreal(X1)
| vplus(X1,X3) != vplus(X2,X3)
| X1 = X2 ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_60])])]) ).
cnf(c_0_69,plain,
( ~ rR(vd1288,vd1287,X1)
| ~ rpoint(X1)
| vplus(vf(vd1288,X1),vf(vd1287,vd1289)) = vf(vd1287,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61,c_0_55]),c_0_57]),c_0_56])]) ).
cnf(c_0_70,plain,
( ~ rR(vd1288,X1,vd1287)
| ~ rpoint(X1)
| vplus(vf(vd1288,X1),vf(vd1287,vd1289)) = vf(X1,vd1287) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62,c_0_45]),c_0_56])]) ).
cnf(c_0_71,plain,
( ~ rR(X1,X3,X2)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X3)
| rR(X1,X2,X3) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_63])])]) ).
cnf(c_0_72,plain,
rR(vd1288,vd1287,vd1299),
inference(split_conjunct,[status(thm)],['and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))']) ).
cnf(c_0_73,plain,
rpoint(vd1299),
inference(rw,[status(thm)],[c_0_64,c_0_65]) ).
cnf(c_0_74,plain,
( ~ rpoint(X8)
| X2 != X8
| ~ rpoint(X7)
| X3 != X7
| ~ rpoint(X6)
| X4 != X6
| ~ rpoint(X5)
| X1 != X5
| ~ rR(X3,X2,X4)
| ~ rR(X1,X2,X3)
| rR(X1,X2,X4) ),
inference(split_conjunct,[status(thm)],[c_0_66]) ).
cnf(c_0_75,plain,
rR(vd1329,vd1287,vd1299),
inference(split_conjunct,[status(thm)],['holds(conjunct1(367), 1330, 0)']) ).
cnf(c_0_76,negated_conjecture,
vd1329 = vd1302,
inference(split_conjunct,[status(thm)],[c_0_67]) ).
cnf(c_0_77,plain,
rpoint(vd1329),
inference(split_conjunct,[status(thm)],['pred(367, 0)']) ).
fof(c_0_78,plain,
! [X69,X70] :
( ( rreal(X70)
& X69 = X70 )
=> ~ rless(X69,X69) ),
inference(fof_simplification,[status(thm)],['qu(cond(axiom(149), 0), imp(cond(axiom(149), 0)))']) ).
fof(c_0_79,plain,
! [X1040,X1041,X1042,X1043,X1044,X1045] :
( rless(vplus(X1040,X1044),vplus(X1042,X1044))
| ~ rreal(X1041)
| X1040 != X1041
| ~ rreal(X1043)
| X1042 != X1043
| ~ rreal(X1045)
| X1044 != X1045
| ~ rless(X1040,X1042) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(153), 0), imp(cond(axiom(153), 0)))'])])]) ).
fof(c_0_80,plain,
! [X993,X994] :
( vplus(X993,v0) = X993
| ~ rreal(X994)
| X993 != X994 ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(141), 0), imp(cond(axiom(141), 0)))'])])]) ).
fof(c_0_81,plain,
! [X146,X147] :
( ( ? [X149] :
( rpoint(X149)
& X146 = X149 )
& ? [X148] :
( rpoint(X148)
& X147 = X148 )
& X146 != X147 )
=> ? [X150] :
( rcircle(X150)
& rcenter(X146,X150)
& ron(X147,X150) ) ),
inference(fof_simplification,[status(thm)],['qu(cond(axiom(53), 0), imp(cond(axiom(53), 0)))']) ).
cnf(c_0_82,plain,
( ~ rR(X3,X2,X4)
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rreal(X1)
| vplus(X1,vf(X3,X4)) != vf(X2,X4)
| X1 = vf(X2,X3) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_68,c_0_44]),c_0_53]),c_0_53]) ).
cnf(c_0_83,plain,
( ~ rR(X1,X2,X3)
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| vplus(vf(X1,X2),vf(X1,X3)) = vf(X2,X3) ),
inference(spm,[status(thm)],[c_0_44,c_0_45]) ).
cnf(c_0_84,plain,
( ~ rR(vd1288,X1,vd1287)
| ~ rR(vd1288,vd1287,X1)
| ~ rpoint(X1)
| vf(X1,vd1287) = vf(vd1287,X1) ),
inference(spm,[status(thm)],[c_0_69,c_0_70]) ).
cnf(c_0_85,plain,
rR(vd1288,vd1299,vd1287),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_71,c_0_72]),c_0_57]),c_0_56]),c_0_73])]) ).
cnf(c_0_86,plain,
( ~ rR(X1,X2,X4)
| ~ rR(X4,X2,X3)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X2)
| rR(X1,X2,X3) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_74])])])]) ).
cnf(c_0_87,plain,
rR(vd1302,vd1287,vd1299),
inference(rw,[status(thm)],[c_0_75,c_0_76]) ).
cnf(c_0_88,plain,
rpoint(vd1302),
inference(rw,[status(thm)],[c_0_77,c_0_76]) ).
cnf(c_0_89,plain,
rpoint(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_90,plain,
vd1289 = esk1_0,
inference(split_conjunct,[status(thm)],[c_0_40]) ).
fof(c_0_91,plain,
! [X871,X872] :
( ~ rless(X871,X871)
| ~ rreal(X872)
| X871 != X872 ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_78])])]) ).
cnf(c_0_92,plain,
( ~ rreal(X6)
| X1 != X6
| ~ rreal(X5)
| X2 != X5
| ~ rreal(X4)
| X3 != X4
| ~ rless(X1,X2)
| rless(vplus(X1,X3),vplus(X2,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_79]) ).
cnf(c_0_93,plain,
( ~ rreal(X2)
| X1 != X2
| vplus(X1,v0) = X1 ),
inference(split_conjunct,[status(thm)],[c_0_80]) ).
cnf(c_0_94,plain,
rreal(vd684),
inference(split_conjunct,[status(thm)],['pred(axiom(137), 1)']) ).
cnf(c_0_95,plain,
v0 = vd684,
inference(split_conjunct,[status(thm)],['pred(axiom(137), 2)']) ).
fof(c_0_96,plain,
! [X948,X949,X950,X951] :
( ( ~ rpoint(X951)
| X948 != X951
| ~ rpoint(X950)
| X949 != X950
| X948 = X949
| rcircle(esk12_2(X948,X949)) )
& ( ~ rpoint(X951)
| X948 != X951
| ~ rpoint(X950)
| X949 != X950
| X948 = X949
| rcenter(X948,esk12_2(X948,X949)) )
& ( ~ rpoint(X951)
| X948 != X951
| ~ rpoint(X950)
| X949 != X950
| X948 = X949
| ron(X949,esk12_2(X948,X949)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_81])])])])])]) ).
cnf(c_0_97,plain,
( ~ rR(X1,X2,X4)
| ~ rR(X1,X3,X4)
| ~ rpoint(X2)
| ~ rpoint(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| vf(X2,X4) != vf(X3,X4)
| vf(X1,X2) = vf(X3,X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_82,c_0_83]),c_0_53]) ).
cnf(c_0_98,plain,
vf(vd1299,vd1287) = vf(vd1287,vd1299),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_84,c_0_72]),c_0_73]),c_0_85])]) ).
cnf(c_0_99,plain,
( ~ rR(X1,vd1287,vd1302)
| ~ rpoint(X1)
| rR(X1,vd1287,vd1299) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_87]),c_0_57]),c_0_88]),c_0_73])]) ).
cnf(c_0_100,plain,
rR(vd1289,vd1287,vd1302),
inference(split_conjunct,[status(thm)],['and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))']) ).
cnf(c_0_101,plain,
rpoint(vd1289),
inference(rw,[status(thm)],[c_0_89,c_0_90]) ).
cnf(c_0_102,plain,
( ~ rless(X1,X1)
| ~ rreal(X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[c_0_91]) ).
cnf(c_0_103,plain,
( ~ rless(X1,X3)
| ~ rreal(X2)
| ~ rreal(X3)
| ~ rreal(X1)
| rless(vplus(X1,X2),vplus(X3,X2)) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_92])])]) ).
cnf(c_0_104,plain,
( ~ rreal(X1)
| vplus(X1,v0) = X1 ),
inference(er,[status(thm)],[c_0_93]) ).
cnf(c_0_105,plain,
rreal(v0),
inference(rw,[status(thm)],[c_0_94,c_0_95]) ).
fof(c_0_106,plain,
! [X899,X900,X901,X902,X903,X904] :
( ( ~ rpoint(X904)
| X899 != X904
| ~ rpoint(X903)
| X900 != X903
| ~ rcenter(X901,X902)
| ~ ron(X900,X902)
| rless(vf(X901,X899),vf(X901,X900))
| ~ rinside(X899,X902) )
& ( ~ rpoint(X904)
| X899 != X904
| ~ rpoint(X903)
| X900 != X903
| ~ rcenter(X901,X902)
| ~ ron(X900,X902)
| rinside(X899,X902)
| ~ rless(vf(X901,X899),vf(X901,X900)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(186), 0), imp(cond(axiom(186), 0)))'])])])])]) ).
fof(c_0_107,plain,
! [X1021,X1022] :
( rinside(X1021,X1022)
| ~ rcenter(X1021,X1022) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))'])])]) ).
cnf(c_0_108,plain,
( ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3
| X1 = X2
| rcenter(X1,esk12_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_96]) ).
cnf(c_0_109,plain,
( ~ rreal(X3)
| ~ rreal(X2)
| ~ rreal(X1)
| vplus(X1,X3) != vplus(X3,X2)
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_68,c_0_52]) ).
cnf(c_0_110,plain,
( ~ rR(vd1288,X1,vd1287)
| ~ rpoint(X1)
| vf(X1,vd1287) != vf(vd1287,vd1299)
| vf(vd1288,X1) = vf(vd1299,vd1288) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_85]),c_0_98]),c_0_73]),c_0_56]),c_0_57])]) ).
cnf(c_0_111,plain,
rR(vd1289,vd1287,vd1299),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_99,c_0_100]),c_0_101])]) ).
cnf(c_0_112,plain,
( ~ rless(X1,X1)
| ~ rreal(X1) ),
inference(er,[status(thm)],[c_0_102]) ).
cnf(c_0_113,plain,
( ~ rless(X1,X2)
| ~ rreal(X2)
| ~ rreal(X1)
| rless(X1,vplus(X2,v0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_103,c_0_104]),c_0_105])]) ).
cnf(c_0_114,plain,
( ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X4 != X5
| ~ rcenter(X3,X2)
| ~ ron(X4,X2)
| ~ rinside(X1,X2)
| rless(vf(X3,X1),vf(X3,X4)) ),
inference(split_conjunct,[status(thm)],[c_0_106]) ).
cnf(c_0_115,plain,
( ~ rcenter(X1,X2)
| rinside(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_107]) ).
cnf(c_0_116,plain,
( ~ rpoint(X2)
| ~ rpoint(X1)
| rcenter(X1,esk12_2(X1,X2))
| X1 = X2 ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_108])]) ).
cnf(c_0_117,plain,
( ~ rreal(X3)
| ~ rreal(X2)
| ~ rreal(X1)
| vplus(X3,X1) != vplus(X3,X2)
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_109,c_0_52]) ).
cnf(c_0_118,plain,
( ~ rR(vd1288,vd1287,X1)
| ~ rpoint(X1)
| vplus(vf(vd1287,vd1289),vf(vd1288,X1)) = vf(vd1287,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44,c_0_55]),c_0_57]),c_0_56])]) ).
cnf(c_0_119,plain,
vf(vd1288,vd1299) = vf(vd1299,vd1288),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_110,c_0_85]),c_0_98]),c_0_73])]) ).
cnf(c_0_120,plain,
rR(vd1289,vd1299,vd1287),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_71,c_0_111]),c_0_57]),c_0_101]),c_0_73])]) ).
fof(c_0_121,plain,
! [X1056,X1057,X1058,X1059] :
( ( ~ rreal(X1057)
| X1056 != X1057
| ~ rreal(X1059)
| X1058 != X1059
| rreal(esk14_3(X1056,X1057,X1058)) )
& ( ~ rreal(X1057)
| X1056 != X1057
| ~ rreal(X1059)
| X1058 != X1059
| vplus(X1056,X1058) = esk14_3(X1056,X1057,X1058) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(139), 0), imp(cond(axiom(139), 0)))'])])])])])])]) ).
fof(c_0_122,plain,
! [X187,X188,X189,X190,X191] :
( ( ? [X194] :
( rpoint(X194)
& X187 = X194 )
& ? [X193] :
( rpoint(X193)
& X188 = X193 )
& ? [X192] :
( rpoint(X192)
& X189 = X192 )
& X187 != X188
& X187 != X189
& X188 != X189
& rline(X191)
& ron(X187,X190)
& ron(X188,X190)
& ron(X189,X190)
& X190 = X191 )
=> ( rR(X189,X187,X188)
| rR(X187,X188,X189)
| rR(X188,X187,X189) ) ),
inference(fof_simplification,[status(thm)],['qu(cond(axiom(91), 0), imp(cond(axiom(91), 0)))']) ).
cnf(c_0_123,plain,
( ~ rless(vplus(X1,v0),X1)
| ~ rreal(X1)
| ~ rreal(vplus(X1,v0)) ),
inference(spm,[status(thm)],[c_0_112,c_0_113]) ).
cnf(c_0_124,plain,
( ~ rless(X1,X3)
| ~ rreal(X2)
| ~ rreal(X3)
| ~ rreal(X1)
| rless(vplus(X1,X2),vplus(X2,X3)) ),
inference(spm,[status(thm)],[c_0_103,c_0_52]) ).
cnf(c_0_125,plain,
rreal(vf(vd1287,vd1289)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_55]),c_0_57]),c_0_56])]) ).
cnf(c_0_126,plain,
( ~ ron(X3,X4)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rcenter(X1,X4)
| ~ rinside(X2,X4)
| rless(vf(X1,X2),vf(X1,X3)) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_114])]) ).
cnf(c_0_127,plain,
( ~ rpoint(X2)
| ~ rpoint(X1)
| rinside(X1,esk12_2(X1,X2))
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_115,c_0_116]) ).
cnf(c_0_128,plain,
( ~ rR(X2,X4,X3)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X4)
| ~ rreal(X1)
| vplus(vf(X4,X2),X1) != vf(X4,X3)
| X1 = vf(X2,X3) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_117,c_0_44]),c_0_53]),c_0_53]) ).
cnf(c_0_129,plain,
vplus(vf(vd1287,vd1289),vf(vd1299,vd1288)) = vf(vd1287,vd1299),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_118,c_0_119]),c_0_73]),c_0_72])]) ).
cnf(c_0_130,plain,
rreal(vf(vd1299,vd1288)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_119]),c_0_56]),c_0_73])]) ).
cnf(c_0_131,plain,
( ~ rR(vd1289,X1,vd1287)
| ~ rpoint(X1)
| vf(X1,vd1287) != vf(vd1287,vd1299)
| vf(vd1289,X1) = vf(vd1299,vd1289) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_120]),c_0_98]),c_0_73]),c_0_101]),c_0_57])]) ).
cnf(c_0_132,plain,
( ~ rreal(X2)
| X1 != X2
| ~ rreal(X4)
| X3 != X4
| rreal(esk14_3(X1,X2,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_121]) ).
cnf(c_0_133,plain,
( ~ rreal(X3)
| X1 != X3
| ~ rreal(X4)
| X2 != X4
| vplus(X1,X2) = esk14_3(X1,X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_121]) ).
cnf(c_0_134,plain,
( ~ rR(vd1289,X1,vd1302)
| ~ rpoint(X1)
| vf(X1,vd1302) != vf(vd1287,vd1302)
| vf(vd1289,X1) = vf(vd1287,vd1289) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_100]),c_0_57]),c_0_101]),c_0_88])]) ).
fof(c_0_135,plain,
! [X995,X996,X997,X998,X999,X1000,X1001,X1002] :
( rR(X997,X995,X996)
| rR(X995,X996,X997)
| rR(X996,X995,X997)
| ~ rpoint(X1002)
| X995 != X1002
| ~ rpoint(X1001)
| X996 != X1001
| ~ rpoint(X1000)
| X997 != X1000
| X995 = X996
| X995 = X997
| X996 = X997
| ~ rline(X999)
| ~ ron(X995,X998)
| ~ ron(X996,X998)
| ~ ron(X997,X998)
| X998 != X999 ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_122])])])]) ).
fof(c_0_136,plain,
! [X770,X771,X772,X773,X774,X775,X776,X777] :
( ron(X771,X773)
| ~ rpoint(X777)
| X770 != X777
| ~ rpoint(X776)
| X771 != X776
| ~ rpoint(X775)
| X772 != X775
| ~ rline(X774)
| ~ rR(X771,X770,X772)
| ~ ron(X770,X773)
| ~ ron(X772,X773)
| X773 != X774 ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(85), 0), imp(cond(axiom(85), 0)))'])])])]) ).
cnf(c_0_137,plain,
( ~ rless(vplus(v0,X1),X1)
| ~ rreal(X1)
| ~ rreal(vplus(v0,X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_123,c_0_52]),c_0_105])]) ).
cnf(c_0_138,plain,
( ~ rR(vd1288,vd1287,X2)
| ~ rpoint(X2)
| ~ rless(X1,vf(vd1288,X2))
| ~ rreal(X1)
| ~ rreal(vf(vd1288,X2))
| rless(vplus(X1,vf(vd1287,vd1289)),vf(vd1287,X2)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_124,c_0_118]),c_0_125])]) ).
cnf(c_0_139,plain,
( ~ ron(X4,esk12_2(X1,X2))
| ~ rpoint(X2)
| ~ rpoint(X4)
| ~ rpoint(X1)
| ~ rcenter(X3,esk12_2(X1,X2))
| rless(vf(X3,X1),vf(X3,X4))
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_126,c_0_127]) ).
cnf(c_0_140,plain,
( ~ rpoint(X4)
| X2 != X4
| ~ rpoint(X3)
| X1 != X3
| X2 = X1
| ron(X1,esk12_2(X2,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_96]) ).
fof(c_0_141,plain,
! [X911,X912,X913,X914] :
( ( ~ rpoint(X914)
| X911 != X914
| ~ rpoint(X913)
| X912 != X913
| vf(X911,X912) = v0
| X911 != X912 )
& ( ~ rpoint(X914)
| X911 != X914
| ~ rpoint(X913)
| X912 != X913
| X911 = X912
| vf(X911,X912) != v0 ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(162), 0), imp(cond(axiom(162), 0)))'])])])])]) ).
cnf(c_0_142,plain,
( ~ rR(vd1289,vd1287,X1)
| ~ rpoint(X1)
| vf(vd1287,vd1299) != vf(vd1287,X1)
| vf(vd1289,X1) = vf(vd1299,vd1288) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_128,c_0_129]),c_0_130]),c_0_57]),c_0_101])]) ).
cnf(c_0_143,plain,
vf(vd1289,vd1299) = vf(vd1299,vd1289),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_131,c_0_120]),c_0_98]),c_0_73])]) ).
cnf(c_0_144,plain,
( ~ rreal(X1)
| ~ rreal(X2)
| rreal(esk14_3(X1,X1,X2)) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_132])]) ).
cnf(c_0_145,plain,
( ~ rreal(X1)
| ~ rreal(X2)
| esk14_3(X1,X1,X2) = vplus(X1,X2) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_133])]) ).
cnf(c_0_146,plain,
( ~ rR(X1,X2,X3)
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| vplus(vf(X1,X2),vf(X3,X1)) = vf(X2,X3) ),
inference(spm,[status(thm)],[c_0_54,c_0_45]) ).
cnf(c_0_147,plain,
vf(vd1289,vd1287) = vf(vd1287,vd1289),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_134,c_0_100]),c_0_57])]) ).
cnf(c_0_148,plain,
( ~ rpoint(X8)
| X5 != X8
| ~ rpoint(X7)
| X4 != X7
| ~ rpoint(X6)
| X3 != X6
| ~ rline(X2)
| ~ ron(X5,X1)
| ~ ron(X4,X1)
| ~ ron(X3,X1)
| X1 != X2
| rR(X3,X5,X4)
| rR(X5,X4,X3)
| rR(X4,X5,X3)
| X5 = X4
| X5 = X3
| X4 = X3 ),
inference(split_conjunct,[status(thm)],[c_0_135]) ).
cnf(c_0_149,plain,
( ~ rpoint(X8)
| X4 != X8
| ~ rpoint(X7)
| X5 != X7
| ~ rpoint(X6)
| X3 != X6
| ~ rline(X2)
| ~ rR(X5,X4,X3)
| ~ ron(X4,X1)
| ~ ron(X3,X1)
| X1 != X2
| ron(X5,X1) ),
inference(split_conjunct,[status(thm)],[c_0_136]) ).
cnf(c_0_150,plain,
( ~ rR(vd1288,vd1287,vd1289)
| ~ rless(v0,vf(vd1288,vd1289))
| ~ rreal(vf(vd1288,vd1289))
| ~ rreal(vplus(v0,vf(vd1287,vd1289))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_137,c_0_138]),c_0_125]),c_0_105]),c_0_101])]) ).
cnf(c_0_151,plain,
( ~ rreal(X1)
| vplus(v0,X1) = X1 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_104,c_0_52]),c_0_105])]) ).
cnf(c_0_152,plain,
( ~ ron(X3,esk12_2(X1,X2))
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ rpoint(X1)
| rless(vf(X1,X1),vf(X1,X3))
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_139,c_0_116]) ).
cnf(c_0_153,plain,
( ~ rpoint(X1)
| ~ rpoint(X2)
| ron(X1,esk12_2(X2,X1))
| X1 = X2 ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_140])]) ).
cnf(c_0_154,plain,
( ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3
| X1 != X2
| vf(X1,X2) = v0 ),
inference(split_conjunct,[status(thm)],[c_0_141]) ).
cnf(c_0_155,plain,
vf(vd1299,vd1288) = vf(vd1299,vd1289),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_142,c_0_111]),c_0_143]),c_0_73])]) ).
cnf(c_0_156,plain,
( ~ rreal(X1)
| ~ rreal(X2)
| rreal(vplus(X1,X2)) ),
inference(spm,[status(thm)],[c_0_144,c_0_145]) ).
cnf(c_0_157,plain,
( ~ rR(vd1287,X1,vd1289)
| ~ rpoint(X1)
| vplus(vf(vd1287,X1),vf(vd1287,vd1289)) = vf(X1,vd1289) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_146,c_0_147]),c_0_57]),c_0_101])]) ).
fof(c_0_158,plain,
! [X879,X880,X881,X882,X883,X884,X885,X886] :
( rR(X880,X879,X882)
| ~ rpoint(X886)
| X879 != X886
| ~ rpoint(X885)
| X880 != X885
| ~ rpoint(X884)
| X881 != X884
| ~ rpoint(X883)
| X882 != X883
| ~ rR(X880,X879,X881)
| ~ rR(X881,X880,X882) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(89), 0), imp(cond(axiom(89), 0)))'])])])]) ).
cnf(c_0_159,plain,
( ~ ron(X3,X4)
| ~ ron(X1,X4)
| ~ ron(X2,X4)
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rline(X4)
| rR(X3,X2,X1)
| rR(X1,X2,X3)
| rR(X2,X1,X3)
| X3 = X1
| X3 = X2
| X1 = X2 ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_148])])])]) ).
cnf(c_0_160,plain,
ron(vd1288,vd1295),
inference(split_conjunct,[status(thm)],['pred(s2(plural(346)), 0)']) ).
cnf(c_0_161,plain,
rline(vd1295),
inference(split_conjunct,[status(thm)],['pred(346, 0)']) ).
cnf(c_0_162,plain,
( ~ ron(X4,X2)
| ~ ron(X3,X2)
| ~ rR(X1,X3,X4)
| ~ rpoint(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rline(X2)
| ron(X1,X2) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_149])])])]) ).
cnf(c_0_163,plain,
ron(vd1329,vd1295),
inference(split_conjunct,[status(thm)],['pred(conjunct1(368), 0)']) ).
cnf(c_0_164,plain,
( ~ rR(vd1288,vd1287,vd1289)
| ~ rless(v0,vf(vd1288,vd1289))
| ~ rreal(vf(vd1288,vd1289)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_150,c_0_151]),c_0_125])]) ).
cnf(c_0_165,plain,
( ~ rpoint(X2)
| ~ rpoint(X1)
| rless(vf(X1,X1),vf(X1,X2))
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_152,c_0_153]) ).
cnf(c_0_166,plain,
( ~ rpoint(X1)
| vf(X1,X1) = v0 ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_154])])]) ).
cnf(c_0_167,plain,
( ~ rreal(X2)
| ~ rreal(X1)
| vplus(X1,X2) != X2
| X1 = v0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68,c_0_151]),c_0_105])]) ).
cnf(c_0_168,plain,
( ~ rR(vd1288,vd1299,X1)
| ~ rpoint(X1)
| vplus(vf(vd1288,X1),vf(vd1299,vd1289)) = vf(vd1299,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61,c_0_155]),c_0_73]),c_0_56])]) ).
cnf(c_0_169,plain,
rreal(vf(vd1299,vd1289)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_143]),c_0_101]),c_0_73])]) ).
cnf(c_0_170,plain,
( ~ rR(vd1287,X1,vd1289)
| ~ rpoint(X1)
| ~ rreal(vf(vd1287,X1))
| rreal(vf(X1,vd1289)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_156,c_0_157]),c_0_125])]) ).
cnf(c_0_171,plain,
( ~ rpoint(X8)
| X4 != X8
| ~ rpoint(X7)
| X2 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X3 != X5
| ~ rR(X2,X4,X1)
| ~ rR(X1,X2,X3)
| rR(X2,X4,X3) ),
inference(split_conjunct,[status(thm)],[c_0_158]) ).
cnf(c_0_172,plain,
( ~ ron(X2,vd1295)
| ~ ron(X1,vd1295)
| ~ rpoint(X2)
| ~ rpoint(X1)
| rR(X2,vd1288,X1)
| rR(X1,vd1288,X2)
| rR(vd1288,X1,X2)
| X2 = X1
| X2 = vd1288
| X1 = vd1288 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_159,c_0_160]),c_0_161]),c_0_56])]) ).
cnf(c_0_173,plain,
ron(vd1287,vd1295),
inference(split_conjunct,[status(thm)],['pred(s1(plural(346)), 0)']) ).
cnf(c_0_174,plain,
vd1287 != vd1288,
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_175,plain,
( ~ ron(vd1302,X1)
| ~ ron(vd1287,X1)
| ~ rline(X1)
| ron(vd1289,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_162,c_0_100]),c_0_57]),c_0_101]),c_0_88])]) ).
cnf(c_0_176,plain,
ron(vd1302,vd1295),
inference(rw,[status(thm)],[c_0_163,c_0_76]) ).
cnf(c_0_177,plain,
( ~ rR(vd1288,vd1287,vd1289)
| ~ rless(v0,vf(vd1288,vd1289)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_164,c_0_53]),c_0_56]),c_0_101])]) ).
cnf(c_0_178,plain,
( ~ rpoint(X2)
| ~ rpoint(X1)
| rless(v0,vf(X1,X2))
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_165,c_0_166]) ).
cnf(c_0_179,plain,
vd1288 != vd1289,
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_180,plain,
( ~ rR(X2,X4,X3)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X4)
| ~ rreal(X1)
| vplus(X1,vf(X4,X2)) != vf(X4,X3)
| X1 = vf(X2,X3) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_109,c_0_44]),c_0_53]),c_0_53]) ).
cnf(c_0_181,plain,
( ~ rR(vd1288,vd1299,X1)
| ~ rpoint(X1)
| ~ rreal(vf(vd1288,X1))
| vf(vd1299,X1) != vf(vd1299,vd1289)
| vf(vd1288,X1) = v0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_167,c_0_168]),c_0_169])]) ).
cnf(c_0_182,plain,
( ~ rR(vd1287,X1,vd1289)
| ~ rpoint(X1)
| rreal(vf(X1,vd1289)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_170,c_0_53]),c_0_57])]) ).
cnf(c_0_183,plain,
( ~ rR(X4,X1,X3)
| ~ rR(X1,X2,X4)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X1)
| ~ rpoint(X2)
| rR(X1,X2,X3) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_171])])])]) ).
cnf(c_0_184,plain,
( ~ ron(X1,vd1295)
| ~ rpoint(X1)
| rR(vd1288,vd1287,X1)
| rR(vd1287,vd1288,X1)
| rR(X1,vd1288,vd1287)
| X1 = vd1288
| X1 = vd1287 ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_172,c_0_173]),c_0_57])]),c_0_174]) ).
cnf(c_0_185,plain,
ron(vd1289,vd1295),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_175,c_0_161]),c_0_173]),c_0_176])]) ).
cnf(c_0_186,plain,
vd1287 != vd1289,
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_187,plain,
~ rR(vd1288,vd1287,vd1289),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_177,c_0_178]),c_0_56]),c_0_101])]),c_0_179]) ).
cnf(c_0_188,plain,
( ~ rR(vd1288,vd1299,X1)
| ~ rpoint(X1)
| vf(vd1299,X1) != vf(vd1287,vd1299)
| vf(vd1288,X1) = vf(vd1287,vd1289) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_180,c_0_129]),c_0_125]),c_0_73]),c_0_56])]) ).
cnf(c_0_189,plain,
( ~ rR(vd1287,vd1288,vd1289)
| ~ rR(vd1288,vd1299,vd1289)
| vf(vd1288,vd1289) = v0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_181,c_0_182]),c_0_101]),c_0_56])]) ).
cnf(c_0_190,plain,
( ~ rR(vd1287,vd1288,X1)
| ~ rpoint(X1)
| rR(vd1288,vd1299,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_183,c_0_85]),c_0_73]),c_0_56]),c_0_57])]) ).
cnf(c_0_191,plain,
( ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3
| vf(X1,X2) != v0
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[c_0_141]) ).
cnf(c_0_192,plain,
( ~ rR(X2,X1,X3)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X1)
| vf(X1,X3) != vf(X2,X3)
| vf(X1,X2) = v0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_167,c_0_44]),c_0_53]),c_0_53]) ).
cnf(c_0_193,plain,
( rR(vd1289,vd1288,vd1287)
| rR(vd1287,vd1288,vd1289) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_184,c_0_185]),c_0_101])]),c_0_186]),c_0_179]),c_0_187]) ).
cnf(c_0_194,plain,
vf(vd1288,vd1287) = vf(vd1287,vd1289),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_188,c_0_85]),c_0_98]),c_0_57])]) ).
cnf(c_0_195,plain,
( ~ rR(vd1287,vd1288,vd1289)
| vf(vd1288,vd1289) = v0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_189,c_0_190]),c_0_101])]) ).
cnf(c_0_196,plain,
( ~ rpoint(X2)
| ~ rpoint(X1)
| vf(X1,X2) != v0
| X1 = X2 ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_191])]) ).
cnf(c_0_197,plain,
vf(vd1288,vd1289) = v0,
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_192,c_0_193]),c_0_194]),c_0_147]),c_0_56]),c_0_101]),c_0_57])]),c_0_195]) ).
cnf(c_0_198,plain,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_196,c_0_197]),c_0_56]),c_0_101])]),c_0_179]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GEO319+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Sun Sep 20 15:19:22 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.03/0.32 Running first-order theorem proving
% 0.03/0.32 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 268.29/34.94 % Version: 3.5.1
% 268.29/34.94 % Preprocessing class: FSLSSMSMSSSNFFN.
% 268.29/34.94 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 268.29/34.94 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 268.29/34.94 % Starting new_bool_3 with 300s (1) cores
% 268.29/34.94 % Starting new_bool_1 with 300s (1) cores
% 268.29/34.94 % Starting sh5l with 300s (1) cores
% 268.29/34.94 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 409492 completed with status 0
% 268.29/34.94 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 268.29/34.94 % Preprocessing class: FSLSSMSMSSSNFFN.
% 268.29/34.94 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 268.29/34.94 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 268.29/34.94 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 268.29/34.94 % No SInE strategy applied
% 268.29/34.94 % Search class: FGHSF-FSLM33-SFFFFFNN
% 268.29/34.94 % Scheduled 11 strats onto 5 cores with 1500 seconds (1500 total)
% 268.29/34.94 % Starting SubtermCWHack with 136s (1) cores
% 268.29/34.94 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 268.29/34.94 % Starting G-E--_302_C18_F1_URBAN_S0Y with 136s (1) cores
% 268.29/34.94 % Starting H----_102_C18_F1_PI_AE_CS_SP_PS_S0Y with 136s (1) cores
% 268.29/34.94 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 136s (1) cores
% 268.29/34.94 % H----_102_C18_F1_PI_AE_CS_SP_PS_S0Y with pid 409514 completed with status 0
% 268.29/34.94 % Result found by H----_102_C18_F1_PI_AE_CS_SP_PS_S0Y
% 268.29/34.94 % Preprocessing class: FSLSSMSMSSSNFFN.
% 268.29/34.94 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 268.29/34.94 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 268.29/34.94 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 268.29/34.94 % No SInE strategy applied
% 268.29/34.94 % Search class: FGHSF-FSLM33-SFFFFFNN
% 268.29/34.94 % Scheduled 11 strats onto 5 cores with 1500 seconds (1500 total)
% 268.29/34.94 % Starting SubtermCWHack with 136s (1) cores
% 268.29/34.94 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 268.29/34.94 % Starting G-E--_302_C18_F1_URBAN_S0Y with 136s (1) cores
% 268.29/34.94 % Starting H----_102_C18_F1_PI_AE_CS_SP_PS_S0Y with 136s (1) cores
% 268.29/34.94 % Preprocessing time : 0.009 s
% 268.29/34.94 % Presaturation interreduction done
% 268.29/34.94
% 268.29/34.94 % Proof found!
% 268.29/34.94 % SZS status Theorem
% 268.29/34.94 % SZS output start CNFRefutation
% See solution above
% 268.29/34.94 % Parsed axioms : 163
% 268.29/34.94 % Removed by relevancy pruning/SinE : 0
% 268.29/34.94 % Initial clauses : 330
% 268.29/34.94 % Removed in clause preprocessing : 2
% 268.29/34.94 % Initial clauses in saturation : 328
% 268.29/34.94 % Processed clauses : 96423
% 268.29/34.94 % ...of these trivial : 235
% 268.29/34.94 % ...subsumed : 77112
% 268.29/34.94 % ...remaining for further processing : 19076
% 268.29/34.94 % Other redundant clauses eliminated : 1194
% 268.29/34.94 % Clauses deleted for lack of memory : 0
% 268.29/34.94 % Backward-subsumed : 3948
% 268.29/34.94 % Backward-rewritten : 1207
% 268.29/34.94 % Generated clauses : 836842
% 268.29/34.94 % ...of the previous two non-redundant : 808105
% 268.29/34.94 % ...aggressively subsumed : 0
% 268.29/34.94 % Contextual simplify-reflections : 4004
% 268.29/34.94 % Paramodulations : 836475
% 268.29/34.94 % Factorizations : 6
% 268.29/34.94 % NegExts : 0
% 268.29/34.94 % Equation resolutions : 1293
% 268.29/34.94 % Disequality decompositions : 0
% 268.29/34.94 % Total rewrite steps : 876499
% 268.29/34.94 % ...of those cached : 876390
% 268.29/34.94 % Propositional unsat checks : 0
% 268.29/34.94 % Propositional check models : 0
% 268.29/34.94 % Propositional check unsatisfiable : 0
% 268.29/34.94 % Propositional clauses : 0
% 268.29/34.94 % Propositional clauses after purity: 0
% 268.29/34.94 % Propositional unsat core size : 0
% 268.29/34.94 % Propositional preprocessing time : 0.000
% 268.29/34.94 % Propositional encoding time : 0.000
% 268.29/34.94 % Propositional solver time : 0.000
% 268.29/34.94 % Success case prop preproc time : 0.000
% 268.29/34.94 % Success case prop encoding time : 0.000
% 268.29/34.94 % Success case prop solver time : 0.000
% 268.29/34.94 % Current number of processed clauses : 13376
% 268.29/34.94 % Positive orientable unit clauses : 102
% 268.29/34.94 % Positive unorientable unit clauses: 0
% 268.29/34.94 % Negative unit clauses : 74
% 268.29/34.94 % Non-unit-clauses : 13200
% 268.29/34.94 % Current number of unprocessed clauses: 695332
% 268.29/34.94 % ...number of literals in the above : 8673757
% 268.29/34.94 % Current number of archived formulas : 0
% 268.29/34.94 % Current number of archived clauses : 5448
% 268.29/34.94 % Clause-clause subsumption calls (NU) : 36263899
% 268.29/34.94 % Rec. Clause-clause subsumption calls : 958094
% 268.29/34.94 % Non-unit clause-clause subsumptions : 50837
% 268.29/34.94 % Unit Clause-clause subsumption calls : 86004
% 268.29/34.94 % Rewrite failures with RHS unbound : 0
% 268.29/34.94 % BW rewrite match attempts : 89
% 268.29/34.94 % BW rewrite match successes : 31
% 268.29/34.94 % Condensation attempts : 0
% 268.29/34.94 % Condensation successes : 0
% 268.29/34.94 % Termbank termtop insertions : 29007814
% 268.29/34.94 % Search garbage collected termcells : 15182
% 268.29/34.94
% 268.29/34.94 % -------------------------------------------------
% 268.29/34.94 % User time : 33.765 s
% 268.29/34.94 % System time : 0.609 s
% 268.29/34.94 % Total time : 34.374 s
% 268.29/34.94 % Maximum resident set size: 6256 pages
% 268.29/34.94
% 268.29/34.94 % -------------------------------------------------
% 268.29/34.94 % User time : 168.924 s
% 268.29/34.94 % System time : 2.555 s
% 268.29/34.94 % Total time : 171.479 s
% 268.29/34.94 % Maximum resident set size: 5376 pages
% 268.29/34.94 % E exiting
%------------------------------------------------------------------------------