%------------------------------------------------------------------------------
% File : ET---2.0
% Problem : GEO346+1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_ET %s %d
% Computer : n003.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 : 600s
% DateTime : Sat Jul 16 04:05:31 EDT 2022
% Result : Theorem 1.32s 209.48s
% Output : CNFRefutation 1.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 18
% Syntax : Number of formulae : 122 ( 48 unt; 0 def)
% Number of atoms : 774 ( 326 equ)
% Maximal formula atoms : 43 ( 6 avg)
% Number of connectives : 1059 ( 407 ~; 525 |; 117 &)
% ( 1 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 41 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 15 con; 0-3 aty)
% Number of variables : 294 ( 0 sgn 96 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
fof('qu(cond(axiom(194), 0), imp(cond(axiom(194), 0)))',axiom,
! [X255,X256,X257,X258,X259,X260,X261] :
( ( ~ rR(X255,X257,X259)
& ~ rR(X255,X256,X258)
& X259 != X255
& X258 != X255
& X257 != X255
& X256 != X255
& ron(X259,X261)
& ron(X257,X261)
& ron(X258,X260)
& ron(X256,X260)
& ron(X255,X260)
& ? [X262] :
( X261 = X262
& rline(X262) )
& ? [X263] :
( X260 = X263
& rline(X263) )
& ? [X264] :
( X259 = X264
& rpoint(X264) )
& ? [X265] :
( X258 = X265
& rpoint(X265) )
& ? [X266] :
( X257 = X266
& rpoint(X266) )
& ? [X267] :
( X256 = X267
& rpoint(X267) )
& ? [X268] :
( X255 = X268
& rpoint(X268) ) )
=> vangle(X256,X255,X257) = vangle(X258,X255,X259) ),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','qu(cond(axiom(194), 0), imp(cond(axiom(194), 0)))') ).
fof('qu(cond(axiom(51), 0), imp(cond(axiom(51), 0)))',axiom,
! [X33,X34] :
( ( X33 != X34
& ? [X35] :
( X34 = X35
& rpoint(X35) )
& ? [X36] :
( X33 = X36
& rpoint(X36) ) )
=> ? [X37] :
( ron(X34,X37)
& ron(X33,X37)
& rline(X37) ) ),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','qu(cond(axiom(51), 0), imp(cond(axiom(51), 0)))') ).
fof('pred(406, 0)',axiom,
rpoint(vd1409),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','pred(406, 0)') ).
fof('qu(cond(axiom(81), 0), imp(cond(axiom(81), 0)))',axiom,
! [X171,X172,X173] :
( ( rR(X172,X171,X173)
& ? [X174] :
( X173 = X174
& rpoint(X174) )
& ? [X175] :
( X172 = X175
& rpoint(X175) )
& ? [X176] :
( X171 = X176
& rpoint(X176) ) )
=> ( ~ rR(X171,X172,X173)
& X171 != X173
& X171 != X172
& rR(X172,X173,X171) ) ),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','qu(cond(axiom(81), 0), imp(cond(axiom(81), 0)))') ).
fof('and(pred(conjunct2(405), 5), and(pred(s2(plural(conjunct2(405))), 0), and(pred(s1(plural(conjunct2(405))), 0), and(pred(conjunct2(405), 1), and(pred(conjunct1(405), 9), and(pred(conjunct1(405), 8), and(pred(conjunct1(405), 7), and(qe(s3(plural(405))), and(qe(s2(plural(405))), qe(s1(plural(405))))))))))))',axiom,
( vd1406 = vd1407
& ron(vd1400,vd1406)
& ron(vd1399,vd1406)
& rline(vd1407)
& vd1400 != vd1401
& vd1399 != vd1401
& vd1399 != vd1400
& ? [X14] :
( vd1401 = X14
& rpoint(X14) )
& ? [X15] :
( vd1400 = X15
& rpoint(X15) )
& ? [X16] :
( vd1399 = X16
& rpoint(X16) ) ),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','and(pred(conjunct2(405), 5), and(pred(s2(plural(conjunct2(405))), 0), and(pred(s1(plural(conjunct2(405))), 0), and(pred(conjunct2(405), 1), and(pred(conjunct1(405), 9), and(pred(conjunct1(405), 8), and(pred(conjunct1(405), 7), and(qe(s3(plural(405))), and(qe(s2(plural(405))), qe(s1(plural(405))))))))))))') ).
fof('qu(cond(axiom(188), 0), imp(cond(axiom(188), 0)))',axiom,
! [X25,X26,X27,X28,X29,X30,X31,X32] :
( ( ron(X27,X31)
& ron(X25,X31)
& X25 != X29
& X25 != X27
& X31 = X32
& rline(X32)
& X29 = X30
& rpoint(X30)
& X27 = X28
& rpoint(X28)
& X25 = X26
& rpoint(X26) )
=> ( ( ~ rR(X25,X27,X29)
& ron(X29,X31) )
<=> vangle(X27,X25,X29) = v0 ) ),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','qu(cond(axiom(188), 0), imp(cond(axiom(188), 0)))') ).
fof('qu(cond(axiom(83), 0), imp(cond(axiom(83), 0)))',axiom,
! [X133,X134,X135,X136,X137] :
( ( X136 = X137
& ron(X134,X136)
& ron(X133,X136)
& rR(X134,X133,X135)
& rline(X137)
& ? [X138] :
( X135 = X138
& rpoint(X138) )
& ? [X139] :
( X134 = X139
& rpoint(X139) )
& ? [X140] :
( X133 = X140
& rpoint(X140) ) )
=> ron(X135,X136) ),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','qu(cond(axiom(83), 0), imp(cond(axiom(83), 0)))') ).
fof('pred(axiom(137), 2)',axiom,
v0 = vd684,
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','pred(axiom(137), 2)') ).
fof('replace(replace(and(pred(s2(plural(the(409))), 0), and(pred(s1(plural(the(409))), 0), pred(the(409), 0)))))',axiom,
( ron(vd1409,vskolem1419)
& ron(vd1401,vskolem1419)
& rline(vskolem1419) ),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','replace(replace(and(pred(s2(plural(the(409))), 0), and(pred(s1(plural(the(409))), 0), pred(the(409), 0)))))') ).
fof('replace(pred(409, 2))',axiom,
vd1418 = vskolem1419,
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','replace(pred(409, 2))') ).
fof('qu(cond(axiom(168), 0), imp(cond(axiom(168), 0)))',axiom,
! [X195,X196,X197] :
( ( X195 != X197
& X195 != X196
& ? [X198] :
( X197 = X198
& rpoint(X198) )
& ? [X199] :
( X196 = X199
& rpoint(X199) )
& ? [X200] :
( X195 = X200
& rpoint(X200) ) )
=> vangle(X195,X196,X197) = vangle(X197,X196,X195) ),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','qu(cond(axiom(168), 0), imp(cond(axiom(168), 0)))') ).
fof('replace(replace(and(pred(s2(plural(the(408))), 0), and(pred(s1(plural(the(408))), 0), pred(the(408), 0)))))',axiom,
( ron(vd1399,vskolem1416)
& ron(vd1401,vskolem1416)
& rline(vskolem1416) ),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','replace(replace(and(pred(s2(plural(the(408))), 0), and(pred(s1(plural(the(408))), 0), pred(the(408), 0)))))') ).
fof('replace(pred(408, 2))',axiom,
vd1415 = vskolem1416,
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','replace(pred(408, 2))') ).
fof('holds(conjunct2(conjunct2(conjunct2(406))), 1413, 0)',axiom,
vd1409 != vd1401,
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','holds(conjunct2(conjunct2(conjunct2(406))), 1413, 0)') ).
fof('replace(qu(theu(the(409), 1), imp(the(409))))',axiom,
! [X1] :
( ( ron(vd1409,X1)
& ron(vd1401,X1)
& rline(X1) )
=> X1 = vskolem1419 ),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','replace(qu(theu(the(409), 1), imp(the(409))))') ).
fof('qu(cond(axiom(97), 0), imp(cond(axiom(97), 0)))',axiom,
! [X205,X206,X207,X208] :
( ( rS(X205,X206,X207)
& X207 = X208
& rline(X208)
& ? [X209] :
( X206 = X209
& rpoint(X209) )
& ? [X210] :
( X205 = X210
& rpoint(X210) ) )
=> rS(X206,X205,X207) ),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','qu(cond(axiom(97), 0), imp(cond(axiom(97), 0)))') ).
fof('qu(cond(axiom(99), 0), imp(cond(axiom(99), 0)))',axiom,
! [X315,X316,X317,X318] :
( ( rS(X315,X316,X317)
& X317 = X318
& rline(X318)
& ? [X319] :
( X316 = X319
& rpoint(X319) )
& ? [X320] :
( X315 = X320
& rpoint(X320) ) )
=> ~ ron(X315,X317) ),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','qu(cond(axiom(99), 0), imp(cond(axiom(99), 0)))') ).
fof('holds(conjunct1(406), 1410, 0)',axiom,
rS(vd1401,vd1409,vd1406),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p','holds(conjunct1(406), 1410, 0)') ).
fof(c_0_18,plain,
! [X269,X270,X271,X272,X273,X274,X275,X276,X277,X278,X279,X280,X281,X282] :
( rR(X269,X271,X273)
| rR(X269,X270,X272)
| X273 = X269
| X272 = X269
| X271 = X269
| X270 = X269
| ~ ron(X273,X275)
| ~ ron(X271,X275)
| ~ ron(X272,X274)
| ~ ron(X270,X274)
| ~ ron(X269,X274)
| X275 != X276
| ~ rline(X276)
| X274 != X277
| ~ rline(X277)
| X273 != X278
| ~ rpoint(X278)
| X272 != X279
| ~ rpoint(X279)
| X271 != X280
| ~ rpoint(X280)
| X270 != X281
| ~ rpoint(X281)
| X269 != X282
| ~ rpoint(X282)
| vangle(X270,X269,X271) = vangle(X272,X269,X273) ),
inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],['qu(cond(axiom(194), 0), imp(cond(axiom(194), 0)))'])])])])])]) ).
fof(c_0_19,plain,
! [X38,X39,X40,X41] :
( ( ron(X39,esk4_2(X38,X39))
| X38 = X39
| X39 != X40
| ~ rpoint(X40)
| X38 != X41
| ~ rpoint(X41) )
& ( ron(X38,esk4_2(X38,X39))
| X38 = X39
| X39 != X40
| ~ rpoint(X40)
| X38 != X41
| ~ rpoint(X41) )
& ( rline(esk4_2(X38,X39))
| X38 = X39
| X39 != X40
| ~ rpoint(X40)
| X38 != X41
| ~ rpoint(X41) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(51), 0), imp(cond(axiom(51), 0)))'])])])])])])]) ).
cnf(c_0_20,plain,
( vangle(X1,X2,X3) = vangle(X4,X2,X5)
| X1 = X2
| X3 = X2
| X4 = X2
| X5 = X2
| rR(X2,X1,X4)
| rR(X2,X3,X5)
| ~ rpoint(X6)
| X2 != X6
| ~ rpoint(X7)
| X1 != X7
| ~ rpoint(X8)
| X3 != X8
| ~ rpoint(X9)
| X4 != X9
| ~ rpoint(X10)
| X5 != X10
| ~ rline(X11)
| X12 != X11
| ~ rline(X13)
| X14 != X13
| ~ ron(X2,X12)
| ~ ron(X1,X12)
| ~ ron(X4,X12)
| ~ ron(X3,X14)
| ~ ron(X5,X14) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_21,plain,
( X2 = X4
| ron(X2,esk4_2(X2,X4))
| ~ rpoint(X1)
| X2 != X1
| ~ rpoint(X3)
| X4 != X3 ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
cnf(c_0_22,plain,
( vangle(X1,X2,X3) = vangle(X4,X2,X5)
| X2 = X5
| X2 = X4
| X2 = X3
| X1 = X2
| rR(X2,X3,X5)
| rR(X2,X1,X4)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rline(X6)
| ~ rline(X7)
| ~ ron(X5,X6)
| ~ ron(X4,X7)
| ~ ron(X3,X6)
| ~ ron(X2,X7)
| ~ ron(X1,X7) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_20])])])])])])]) ).
cnf(c_0_23,plain,
( X1 = X2
| ron(X1,esk4_2(X1,X2))
| ~ rpoint(X2)
| ~ rpoint(X1) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_21])]) ).
cnf(c_0_24,plain,
( X2 = X4
| ron(X4,esk4_2(X2,X4))
| ~ rpoint(X1)
| X2 != X1
| ~ rpoint(X3)
| X4 != X3 ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
cnf(c_0_25,plain,
( vangle(X1,X2,X3) = vangle(X4,X2,X5)
| X2 = X5
| X2 = X4
| X2 = X3
| X1 = X2
| X5 = X6
| rR(X2,X3,X5)
| rR(X2,X1,X4)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X6)
| ~ rline(esk4_2(X5,X6))
| ~ rline(X7)
| ~ ron(X3,esk4_2(X5,X6))
| ~ ron(X4,X7)
| ~ ron(X2,X7)
| ~ ron(X1,X7) ),
inference(spm,[status(thm)],[c_0_22,c_0_23]) ).
cnf(c_0_26,plain,
( X1 = X2
| ron(X2,esk4_2(X1,X2))
| ~ rpoint(X2)
| ~ rpoint(X1) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_24])]) ).
cnf(c_0_27,plain,
( X2 = X4
| rline(esk4_2(X2,X4))
| ~ rpoint(X1)
| X2 != X1
| ~ rpoint(X3)
| X4 != X3 ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
cnf(c_0_28,plain,
( vangle(X1,X2,X3) = vangle(X4,X2,X5)
| X2 = X5
| X2 = X4
| X2 = X3
| X1 = X2
| X5 = X3
| rR(X2,X3,X5)
| rR(X2,X1,X4)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rline(esk4_2(X5,X3))
| ~ rline(X6)
| ~ ron(X4,X6)
| ~ ron(X2,X6)
| ~ ron(X1,X6) ),
inference(spm,[status(thm)],[c_0_25,c_0_26]) ).
cnf(c_0_29,plain,
( X1 = X2
| rline(esk4_2(X1,X2))
| ~ rpoint(X2)
| ~ rpoint(X1) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_27])]) ).
cnf(c_0_30,plain,
( vangle(X1,X2,X3) = vangle(X4,X2,X5)
| X2 = X5
| X2 = X4
| X2 = X3
| X1 = X2
| X5 = X3
| rR(X2,X3,X5)
| rR(X2,X1,X4)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rline(X6)
| ~ ron(X4,X6)
| ~ ron(X2,X6)
| ~ ron(X1,X6) ),
inference(spm,[status(thm)],[c_0_28,c_0_29]) ).
cnf(c_0_31,plain,
( vangle(X1,X2,X3) = vangle(X4,X2,X5)
| X2 = X5
| X2 = X4
| X2 = X3
| X1 = X2
| X5 = X3
| X4 = X6
| rR(X2,X3,X5)
| rR(X2,X1,X4)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X6)
| ~ rline(esk4_2(X4,X6))
| ~ ron(X2,esk4_2(X4,X6))
| ~ ron(X1,esk4_2(X4,X6)) ),
inference(spm,[status(thm)],[c_0_30,c_0_23]) ).
cnf(c_0_32,plain,
( vangle(X1,X2,X3) = vangle(X4,X2,X5)
| X2 = X5
| X2 = X4
| X2 = X3
| X1 = X2
| X5 = X3
| rR(X2,X3,X5)
| rR(X2,X1,X4)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rline(esk4_2(X4,X2))
| ~ ron(X1,esk4_2(X4,X2)) ),
inference(spm,[status(thm)],[c_0_31,c_0_26]) ).
cnf(c_0_33,plain,
( vangle(X1,X2,X3) = vangle(X1,X2,X4)
| X2 = X4
| X2 = X1
| X2 = X3
| X4 = X3
| rR(X2,X3,X4)
| rR(X2,X1,X1)
| ~ rpoint(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rline(esk4_2(X1,X2)) ),
inference(spm,[status(thm)],[c_0_32,c_0_23]) ).
cnf(c_0_34,plain,
( vangle(X1,X2,X3) = vangle(X1,X2,X4)
| X2 = X4
| X2 = X1
| X2 = X3
| X4 = X3
| rR(X2,X3,X4)
| rR(X2,X1,X1)
| ~ rpoint(X4)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(spm,[status(thm)],[c_0_33,c_0_29]) ).
cnf(c_0_35,plain,
rpoint(vd1409),
inference(split_conjunct,[status(thm)],['pred(406, 0)']) ).
fof(c_0_36,plain,
! [X177,X178,X179,X180,X181,X182] :
( ( ~ rR(X177,X178,X179)
| ~ rR(X178,X177,X179)
| X179 != X180
| ~ rpoint(X180)
| X178 != X181
| ~ rpoint(X181)
| X177 != X182
| ~ rpoint(X182) )
& ( X177 != X179
| ~ rR(X178,X177,X179)
| X179 != X180
| ~ rpoint(X180)
| X178 != X181
| ~ rpoint(X181)
| X177 != X182
| ~ rpoint(X182) )
& ( X177 != X178
| ~ rR(X178,X177,X179)
| X179 != X180
| ~ rpoint(X180)
| X178 != X181
| ~ rpoint(X181)
| X177 != X182
| ~ rpoint(X182) )
& ( rR(X178,X179,X177)
| ~ rR(X178,X177,X179)
| X179 != X180
| ~ rpoint(X180)
| X178 != X181
| ~ rpoint(X181)
| X177 != X182
| ~ rpoint(X182) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],['qu(cond(axiom(81), 0), imp(cond(axiom(81), 0)))'])])])])])])]) ).
cnf(c_0_37,plain,
( vangle(X1,X2,X3) = vangle(X1,X2,vd1409)
| X2 = vd1409
| vd1409 = X3
| X2 = X1
| X2 = X3
| rR(X2,X3,vd1409)
| rR(X2,X1,X1)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(spm,[status(thm)],[c_0_34,c_0_35]) ).
fof(c_0_38,plain,
( vd1406 = vd1407
& ron(vd1400,vd1406)
& ron(vd1399,vd1406)
& rline(vd1407)
& vd1400 != vd1401
& vd1399 != vd1401
& vd1399 != vd1400
& vd1401 = esk1_0
& rpoint(esk1_0)
& vd1400 = esk2_0
& rpoint(esk2_0)
& vd1399 = esk3_0
& rpoint(esk3_0) ),
inference(skolemize,[status(esa)],[inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],['and(pred(conjunct2(405), 5), and(pred(s2(plural(conjunct2(405))), 0), and(pred(s1(plural(conjunct2(405))), 0), and(pred(conjunct2(405), 1), and(pred(conjunct1(405), 9), and(pred(conjunct1(405), 8), and(pred(conjunct1(405), 7), and(qe(s3(plural(405))), and(qe(s2(plural(405))), qe(s1(plural(405))))))))))))'])])])]) ).
fof(c_0_39,plain,
! [X33,X34,X35,X36,X37,X38,X39,X40] :
( ( rR(X33,X35,X37)
| ~ ron(X37,X39)
| vangle(X35,X33,X37) = v0
| ~ ron(X35,X39)
| ~ ron(X33,X39)
| X33 = X37
| X33 = X35
| X39 != X40
| ~ rline(X40)
| X37 != X38
| ~ rpoint(X38)
| X35 != X36
| ~ rpoint(X36)
| X33 != X34
| ~ rpoint(X34) )
& ( ~ rR(X33,X35,X37)
| vangle(X35,X33,X37) != v0
| ~ ron(X35,X39)
| ~ ron(X33,X39)
| X33 = X37
| X33 = X35
| X39 != X40
| ~ rline(X40)
| X37 != X38
| ~ rpoint(X38)
| X35 != X36
| ~ rpoint(X36)
| X33 != X34
| ~ rpoint(X34) )
& ( ron(X37,X39)
| vangle(X35,X33,X37) != v0
| ~ ron(X35,X39)
| ~ ron(X33,X39)
| X33 = X37
| X33 = X35
| X39 != X40
| ~ rline(X40)
| X37 != X38
| ~ rpoint(X38)
| X35 != X36
| ~ rpoint(X36)
| X33 != X34
| ~ rpoint(X34) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],['qu(cond(axiom(188), 0), imp(cond(axiom(188), 0)))'])])])])])]) ).
fof(c_0_40,plain,
! [X141,X142,X143,X144,X145,X146,X147,X148] :
( X144 != X145
| ~ ron(X142,X144)
| ~ ron(X141,X144)
| ~ rR(X142,X141,X143)
| ~ rline(X145)
| X143 != X146
| ~ rpoint(X146)
| X142 != X147
| ~ rpoint(X147)
| X141 != X148
| ~ rpoint(X148)
| ron(X143,X144) ),
inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(83), 0), imp(cond(axiom(83), 0)))'])])])])]) ).
cnf(c_0_41,plain,
( ~ rpoint(X1)
| X2 != X1
| ~ rpoint(X3)
| X4 != X3
| ~ rpoint(X5)
| X6 != X5
| ~ rR(X4,X2,X6)
| X2 != X6 ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
cnf(c_0_42,plain,
( vangle(vd1409,X1,X2) = vangle(vd1409,X1,vd1409)
| X1 = vd1409
| vd1409 = X2
| X1 = X2
| rR(X1,vd1409,vd1409)
| rR(X1,X2,vd1409)
| ~ rpoint(X2)
| ~ rpoint(X1) ),
inference(spm,[status(thm)],[c_0_37,c_0_35]) ).
cnf(c_0_43,plain,
rpoint(esk3_0),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_44,plain,
( X2 = X4
| X2 = X6
| vangle(X4,X2,X6) = v0
| rR(X2,X4,X6)
| ~ rpoint(X1)
| X2 != X1
| ~ rpoint(X3)
| X4 != X3
| ~ rpoint(X5)
| X6 != X5
| ~ rline(X7)
| X8 != X7
| ~ ron(X2,X8)
| ~ ron(X4,X8)
| ~ ron(X6,X8) ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_45,plain,
v0 = vd684,
inference(split_conjunct,[status(thm)],['pred(axiom(137), 2)']) ).
cnf(c_0_46,plain,
ron(vd1409,vskolem1419),
inference(split_conjunct,[status(thm)],['replace(replace(and(pred(s2(plural(the(409))), 0), and(pred(s1(plural(the(409))), 0), pred(the(409), 0)))))']) ).
cnf(c_0_47,plain,
vd1418 = vskolem1419,
inference(split_conjunct,[status(thm)],['replace(pred(409, 2))']) ).
cnf(c_0_48,plain,
rline(vskolem1419),
inference(split_conjunct,[status(thm)],['replace(replace(and(pred(s2(plural(the(409))), 0), and(pred(s1(plural(the(409))), 0), pred(the(409), 0)))))']) ).
cnf(c_0_49,plain,
( ron(X1,X2)
| ~ rpoint(X3)
| X4 != X3
| ~ rpoint(X5)
| X6 != X5
| ~ rpoint(X7)
| X1 != X7
| ~ rline(X8)
| ~ rR(X6,X4,X1)
| ~ ron(X4,X2)
| ~ ron(X6,X2)
| X2 != X8 ),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_50,plain,
( ~ rR(X1,X2,X2)
| ~ rpoint(X2)
| ~ rpoint(X1) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_41])])])]) ).
cnf(c_0_51,plain,
( vangle(vd1409,X1,vd1409) = vangle(vd1409,X1,esk3_0)
| vd1409 = esk3_0
| X1 = vd1409
| X1 = esk3_0
| rR(X1,vd1409,vd1409)
| rR(X1,esk3_0,vd1409)
| ~ rpoint(X1) ),
inference(spm,[status(thm)],[c_0_42,c_0_43]) ).
fof(c_0_52,plain,
! [X201,X202,X203,X204,X205,X206] :
( X201 = X203
| X201 = X202
| X203 != X204
| ~ rpoint(X204)
| X202 != X205
| ~ rpoint(X205)
| X201 != X206
| ~ rpoint(X206)
| vangle(X201,X202,X203) = vangle(X203,X202,X201) ),
inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(168), 0), imp(cond(axiom(168), 0)))'])])])])]) ).
cnf(c_0_53,plain,
( vangle(X1,X2,X3) = vd684
| X2 = X3
| X2 = X1
| rR(X2,X1,X3)
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rline(X4)
| ~ ron(X3,X4)
| ~ ron(X1,X4)
| ~ ron(X2,X4) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(rw,[status(thm)],[c_0_44,c_0_45])])])])]) ).
cnf(c_0_54,plain,
ron(vd1409,vd1418),
inference(rw,[status(thm)],[c_0_46,c_0_47]) ).
cnf(c_0_55,plain,
rline(vd1418),
inference(rw,[status(thm)],[c_0_48,c_0_47]) ).
cnf(c_0_56,plain,
( ron(X1,X2)
| ~ rR(X3,X4,X1)
| ~ rpoint(X1)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rline(X2)
| ~ ron(X3,X2)
| ~ ron(X4,X2) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_49])])])]) ).
cnf(c_0_57,plain,
( vangle(vd1409,X1,vd1409) = vangle(vd1409,X1,esk3_0)
| vd1409 = esk3_0
| X1 = vd1409
| X1 = esk3_0
| rR(X1,esk3_0,vd1409)
| ~ rpoint(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_51]),c_0_35])]) ).
cnf(c_0_58,plain,
ron(vd1401,vskolem1416),
inference(split_conjunct,[status(thm)],['replace(replace(and(pred(s2(plural(the(408))), 0), and(pred(s1(plural(the(408))), 0), pred(the(408), 0)))))']) ).
cnf(c_0_59,plain,
vd1401 = esk1_0,
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_60,plain,
vd1415 = vskolem1416,
inference(split_conjunct,[status(thm)],['replace(pred(408, 2))']) ).
cnf(c_0_61,plain,
rline(vskolem1416),
inference(split_conjunct,[status(thm)],['replace(replace(and(pred(s2(plural(the(408))), 0), and(pred(s1(plural(the(408))), 0), pred(the(408), 0)))))']) ).
cnf(c_0_62,plain,
ron(vd1399,vskolem1416),
inference(split_conjunct,[status(thm)],['replace(replace(and(pred(s2(plural(the(408))), 0), and(pred(s1(plural(the(408))), 0), pred(the(408), 0)))))']) ).
cnf(c_0_63,plain,
vd1399 = esk3_0,
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_64,plain,
vd1409 != vd1401,
inference(split_conjunct,[status(thm)],['holds(conjunct2(conjunct2(conjunct2(406))), 1413, 0)']) ).
cnf(c_0_65,plain,
vd1399 != vd1401,
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_66,plain,
( X2 = X4
| X2 = X6
| ron(X6,X8)
| ~ rpoint(X1)
| X2 != X1
| ~ rpoint(X3)
| X4 != X3
| ~ rpoint(X5)
| X6 != X5
| ~ rline(X7)
| X8 != X7
| ~ ron(X2,X8)
| ~ ron(X4,X8)
| vangle(X4,X2,X6) != v0 ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_67,plain,
( vangle(X1,X2,X3) = vangle(X3,X2,X1)
| X1 = X2
| X1 = X3
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X5)
| X2 != X5
| ~ rpoint(X6)
| X3 != X6 ),
inference(split_conjunct,[status(thm)],[c_0_52]) ).
cnf(c_0_68,plain,
( vangle(X1,X2,vd1409) = vd684
| X2 = vd1409
| X2 = X1
| rR(X2,X1,vd1409)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ ron(X1,vd1418)
| ~ ron(X2,vd1418) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_54]),c_0_35]),c_0_55])]) ).
cnf(c_0_69,plain,
( vangle(vd1409,X1,vd1409) = vangle(vd1409,X1,esk3_0)
| vd1409 = esk3_0
| X1 = vd1409
| X1 = esk3_0
| ron(vd1409,X2)
| ~ rpoint(X1)
| ~ rline(X2)
| ~ ron(esk3_0,X2)
| ~ ron(X1,X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56,c_0_57]),c_0_35]),c_0_43])]) ).
cnf(c_0_70,plain,
ron(esk1_0,vd1415),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_58,c_0_59]),c_0_60]) ).
cnf(c_0_71,plain,
rpoint(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_72,plain,
rline(vd1415),
inference(rw,[status(thm)],[c_0_61,c_0_60]) ).
cnf(c_0_73,plain,
ron(esk3_0,vd1415),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_62,c_0_63]),c_0_60]) ).
cnf(c_0_74,plain,
vd1409 != esk1_0,
inference(rw,[status(thm)],[c_0_64,c_0_59]) ).
cnf(c_0_75,plain,
esk3_0 != esk1_0,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_65,c_0_59]),c_0_63]) ).
cnf(c_0_76,plain,
ron(vd1401,vskolem1419),
inference(split_conjunct,[status(thm)],['replace(replace(and(pred(s2(plural(the(409))), 0), and(pred(s1(plural(the(409))), 0), pred(the(409), 0)))))']) ).
fof(c_0_77,plain,
! [X2] :
( ~ ron(vd1409,X2)
| ~ ron(vd1401,X2)
| ~ rline(X2)
| X2 = vskolem1419 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['replace(qu(theu(the(409), 1), imp(the(409))))'])]) ).
cnf(c_0_78,plain,
( X1 = X2
| X1 = X3
| ron(X2,X4)
| vangle(X3,X1,X2) != vd684
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rline(X4)
| ~ ron(X3,X4)
| ~ ron(X1,X4) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(rw,[status(thm)],[c_0_66,c_0_45])])])])]) ).
cnf(c_0_79,plain,
( vangle(X1,X2,X3) = vangle(X3,X2,X1)
| X1 = X3
| X1 = X2
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X1) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_67])])]) ).
cnf(c_0_80,plain,
( vangle(vd1409,X1,vd1409) = vd684
| X1 = vd1409
| ~ rpoint(X1)
| ~ ron(X1,vd1418) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_68]),c_0_35]),c_0_54])]) ).
cnf(c_0_81,plain,
( vangle(vd1409,esk1_0,vd1409) = vangle(vd1409,esk1_0,esk3_0)
| vd1409 = esk3_0
| ron(vd1409,vd1415) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_70]),c_0_71]),c_0_72]),c_0_73])]),c_0_74]),c_0_75]) ).
cnf(c_0_82,plain,
ron(esk1_0,vd1418),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_76,c_0_59]),c_0_47]) ).
fof(c_0_83,plain,
! [X211,X212,X213,X214,X215,X216] :
( ~ rS(X211,X212,X213)
| X213 != X214
| ~ rline(X214)
| X212 != X215
| ~ rpoint(X215)
| X211 != X216
| ~ rpoint(X216)
| rS(X212,X211,X213) ),
inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['qu(cond(axiom(97), 0), imp(cond(axiom(97), 0)))'])])])])]) ).
cnf(c_0_84,plain,
( X1 = vskolem1419
| ~ rline(X1)
| ~ ron(vd1401,X1)
| ~ ron(vd1409,X1) ),
inference(split_conjunct,[status(thm)],[c_0_77]) ).
cnf(c_0_85,plain,
( X1 = X2
| X1 = X3
| X3 = X2
| ron(X2,X4)
| vangle(X2,X1,X3) != vd684
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rline(X4)
| ~ ron(X3,X4)
| ~ ron(X1,X4) ),
inference(pm,[status(thm)],[c_0_78,c_0_79]) ).
cnf(c_0_86,plain,
( vangle(vd1409,esk1_0,esk3_0) = vd684
| vd1409 = esk3_0
| ron(vd1409,vd1415) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_80,c_0_81]),c_0_71]),c_0_82])]),c_0_74]) ).
cnf(c_0_87,plain,
rpoint(esk2_0),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
fof(c_0_88,plain,
! [X321,X322,X323,X324,X325,X326] :
( ~ rS(X321,X322,X323)
| X323 != X324
| ~ rline(X324)
| X322 != X325
| ~ rpoint(X325)
| X321 != X326
| ~ rpoint(X326)
| ~ ron(X321,X323) ),
inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],['qu(cond(axiom(99), 0), imp(cond(axiom(99), 0)))'])])])])])]) ).
cnf(c_0_89,plain,
( rS(X1,X2,X3)
| ~ rpoint(X4)
| X2 != X4
| ~ rpoint(X5)
| X1 != X5
| ~ rline(X6)
| X3 != X6
| ~ rS(X2,X1,X3) ),
inference(split_conjunct,[status(thm)],[c_0_83]) ).
cnf(c_0_90,plain,
rS(vd1401,vd1409,vd1406),
inference(split_conjunct,[status(thm)],['holds(conjunct1(406), 1410, 0)']) ).
cnf(c_0_91,plain,
vd1406 = vd1407,
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_92,plain,
( X1 = vd1418
| ~ rline(X1)
| ~ ron(vd1409,X1)
| ~ ron(esk1_0,X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_84,c_0_47]),c_0_59]) ).
cnf(c_0_93,plain,
( vd1409 = esk3_0
| ron(vd1409,vd1415)
| ron(vd1409,X1)
| ~ rline(X1)
| ~ ron(esk3_0,X1)
| ~ ron(esk1_0,X1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_85,c_0_86]),c_0_35]),c_0_43]),c_0_71])]),c_0_74]),c_0_75]) ).
cnf(c_0_94,plain,
( vangle(vd1409,X1,vd1409) = vangle(vd1409,X1,esk2_0)
| vd1409 = esk2_0
| X1 = vd1409
| X1 = esk2_0
| rR(X1,vd1409,vd1409)
| rR(X1,esk2_0,vd1409)
| ~ rpoint(X1) ),
inference(spm,[status(thm)],[c_0_42,c_0_87]) ).
cnf(c_0_95,plain,
( ~ ron(X1,X2)
| ~ rpoint(X3)
| X1 != X3
| ~ rpoint(X4)
| X5 != X4
| ~ rline(X6)
| X2 != X6
| ~ rS(X1,X5,X2) ),
inference(split_conjunct,[status(thm)],[c_0_88]) ).
cnf(c_0_96,plain,
( rS(X1,X2,X3)
| ~ rS(X2,X1,X3)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rline(X3) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_89])])]) ).
cnf(c_0_97,plain,
rS(esk1_0,vd1409,vd1407),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_90,c_0_59]),c_0_91]) ).
cnf(c_0_98,plain,
rline(vd1407),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_99,plain,
( vd1415 = vd1418
| ~ ron(vd1409,vd1415) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_92,c_0_72]),c_0_70])]) ).
cnf(c_0_100,plain,
( vd1409 = esk3_0
| ron(vd1409,vd1415) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_93,c_0_72]),c_0_73]),c_0_70])]) ).
cnf(c_0_101,plain,
( vangle(vd1409,X1,vd1409) = vangle(vd1409,X1,esk2_0)
| vd1409 = esk2_0
| X1 = vd1409
| X1 = esk2_0
| rR(X1,esk2_0,vd1409)
| ~ rpoint(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_94]),c_0_35])]) ).
cnf(c_0_102,plain,
ron(vd1399,vd1406),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_103,plain,
ron(vd1400,vd1406),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_104,plain,
vd1400 = esk2_0,
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_105,plain,
vd1399 != vd1400,
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_106,plain,
( ~ rS(X1,X2,X3)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rline(X3)
| ~ ron(X1,X3) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_95])])]) ).
cnf(c_0_107,plain,
rS(vd1409,esk1_0,vd1407),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_96,c_0_97]),c_0_35]),c_0_71]),c_0_98])]) ).
cnf(c_0_108,plain,
( vd1415 = vd1418
| vd1409 = esk3_0 ),
inference(spm,[status(thm)],[c_0_99,c_0_100]) ).
cnf(c_0_109,plain,
( vangle(vd1409,X1,vd1409) = vangle(vd1409,X1,esk2_0)
| vd1409 = esk2_0
| X1 = vd1409
| X1 = esk2_0
| ron(vd1409,X2)
| ~ rpoint(X1)
| ~ rline(X2)
| ~ ron(esk2_0,X2)
| ~ ron(X1,X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56,c_0_101]),c_0_35]),c_0_87])]) ).
cnf(c_0_110,plain,
ron(esk3_0,vd1407),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_102,c_0_63]),c_0_91]) ).
cnf(c_0_111,plain,
ron(esk2_0,vd1407),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_103,c_0_104]),c_0_91]) ).
cnf(c_0_112,plain,
esk3_0 != esk2_0,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_105,c_0_104]),c_0_63]) ).
cnf(c_0_113,plain,
~ ron(vd1409,vd1407),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_106,c_0_107]),c_0_71]),c_0_35]),c_0_98])]) ).
cnf(c_0_114,plain,
vd1415 = vd1418,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_99,c_0_108]),c_0_73])]) ).
cnf(c_0_115,plain,
( vangle(vd1409,esk3_0,vd1409) = vangle(vd1409,esk3_0,esk2_0)
| vd1409 = esk2_0
| vd1409 = esk3_0 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_109,c_0_110]),c_0_43]),c_0_98]),c_0_111])]),c_0_112]),c_0_113]) ).
cnf(c_0_116,plain,
ron(esk3_0,vd1418),
inference(rw,[status(thm)],[c_0_73,c_0_114]) ).
cnf(c_0_117,plain,
( vangle(vd1409,esk3_0,esk2_0) = vd684
| vd1409 = esk3_0
| vd1409 = esk2_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_80,c_0_115]),c_0_43]),c_0_116])]) ).
cnf(c_0_118,plain,
( vd1409 = esk3_0
| vd1409 = esk2_0
| ron(vd1409,X1)
| ~ rline(X1)
| ~ ron(esk2_0,X1)
| ~ ron(esk3_0,X1) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_85,c_0_117]),c_0_35]),c_0_87]),c_0_43])]),c_0_112]) ).
cnf(c_0_119,plain,
( vd1409 = esk3_0
| vd1409 = esk2_0 ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_118,c_0_98]),c_0_111]),c_0_110])]),c_0_113]) ).
cnf(c_0_120,plain,
vd1409 = esk2_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_113,c_0_119]),c_0_110])]) ).
cnf(c_0_121,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_113,c_0_120]),c_0_111])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO346+1 : TPTP v8.1.0. Released v4.1.0.
% 0.07/0.13 % Command : run_ET %s %d
% 0.13/0.34 % Computer : n003.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Sat Jun 18 00:11:42 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.36/23.42 eprover: CPU time limit exceeded, terminating
% 0.36/23.43 eprover: CPU time limit exceeded, terminating
% 0.36/23.43 eprover: CPU time limit exceeded, terminating
% 0.36/23.44 eprover: CPU time limit exceeded, terminating
% 0.48/46.44 eprover: CPU time limit exceeded, terminating
% 0.48/46.44 eprover: CPU time limit exceeded, terminating
% 0.48/46.45 eprover: CPU time limit exceeded, terminating
% 0.48/46.46 eprover: CPU time limit exceeded, terminating
% 0.60/69.45 eprover: eprover: CPU time limit exceeded, terminatingCPU time limit exceeded, terminating
% 0.60/69.45
% 0.60/69.46 eprover: CPU time limit exceeded, terminating
% 0.60/69.48 eprover: CPU time limit exceeded, terminating
% 0.71/92.46 eprover: eprover: CPU time limit exceeded, terminatingCPU time limit exceeded, terminating
% 0.71/92.46
% 0.71/92.48 eprover: CPU time limit exceeded, terminating
% 0.71/92.50 eprover: CPU time limit exceeded, terminating
% 0.85/115.48 eprover: CPU time limit exceeded, terminating
% 0.85/115.48 eprover: CPU time limit exceeded, terminating
% 0.85/115.50 eprover: CPU time limit exceeded, terminating
% 0.85/115.52 eprover: CPU time limit exceeded, terminating
% 0.96/138.50 eprover: CPU time limit exceeded, terminating
% 0.96/138.50 eprover: CPU time limit exceeded, terminating
% 0.96/138.51 eprover: CPU time limit exceeded, terminating
% 0.96/138.53 eprover: CPU time limit exceeded, terminating
% 1.08/161.52 eprover: CPU time limit exceeded, terminating
% 1.08/161.53 eprover: eprover: CPU time limit exceeded, terminatingCPU time limit exceeded, terminating
% 1.08/161.53
% 1.08/161.55 eprover: CPU time limit exceeded, terminating
% 1.20/184.53 eprover: CPU time limit exceeded, terminating
% 1.20/184.55 eprover: CPU time limit exceeded, terminating
% 1.20/184.56 eprover: CPU time limit exceeded, terminating
% 1.20/184.57 eprover: CPU time limit exceeded, terminating
% 1.31/207.55 eprover: CPU time limit exceeded, terminating
% 1.31/207.56 eprover: CPU time limit exceeded, terminating
% 1.31/207.58 eprover: CPU time limit exceeded, terminating
% 1.31/207.66 eprover: CPU time limit exceeded, terminating
% 1.32/209.48 # Running protocol protocol_eprover_2d86bd69119e7e9cc4417c0ee581499eaf828bb2 for 23 seconds:
% 1.32/209.48
% 1.32/209.48 # Failure: Resource limit exceeded (time)
% 1.32/209.48 # OLD status Res
% 1.32/209.48 # SinE strategy is GSinE(CountFormulas,,1.1,,02,500,1.0)
% 1.32/209.48 # Preprocessing time : 0.056 s
% 1.32/209.48 # Running protocol protocol_eprover_230b6c199cce1dcf6700db59e75a93feb83d1bd9 for 23 seconds:
% 1.32/209.48
% 1.32/209.48 # Failure: Resource limit exceeded (time)
% 1.32/209.48 # OLD status Res
% 1.32/209.48 # SinE strategy is GSinE(CountFormulas,hypos,1.1,,01,20000,1.0)
% 1.32/209.48 # Preprocessing time : 0.022 s
% 1.32/209.48 # Running protocol protocol_eprover_48e494e00e0717ec2eabf59b73b2d711334607de for 23 seconds:
% 1.32/209.48
% 1.32/209.48 # Failure: Resource limit exceeded (time)
% 1.32/209.48 # OLD status Res
% 1.32/209.48 # SinE strategy is GSinE(CountFormulas,hypos,1.1,,03,20000,1.0)
% 1.32/209.48 # Preprocessing time : 0.033 s
% 1.32/209.48 # Running protocol protocol_eprover_33aa8a325940064c53b389b41203bb48a5cb5006 for 23 seconds:
% 1.32/209.48
% 1.32/209.48 # Failure: Resource limit exceeded (time)
% 1.32/209.48 # OLD status Res
% 1.32/209.48 # Preprocessing time : 0.035 s
% 1.32/209.48 # Running protocol protocol_eprover_260890dcdd2d907655d788d68835201aeffdef4a for 23 seconds:
% 1.32/209.48
% 1.32/209.48 # Failure: Resource limit exceeded (time)
% 1.32/209.48 # OLD status Res
% 1.32/209.48 # SinE strategy is GSinE(CountFormulas,,1.5,,03,100,1.0)
% 1.32/209.48 # Preprocessing time : 0.064 s
% 1.32/209.48 # Running protocol protocol_eprover_9a428cb4e1feff5dec19b8494e78e7f0e8ede446 for 23 seconds:
% 1.32/209.48
% 1.32/209.48 # Failure: Resource limit exceeded (time)
% 1.32/209.48 # OLD status Res
% 1.32/209.48 # Preprocessing time : 0.067 s
% 1.32/209.48 # Running protocol protocol_eprover_e6b386026570787d4ac06e541c4634c5e3f09cc5 for 23 seconds:
% 1.32/209.48
% 1.32/209.48 # Failure: Resource limit exceeded (time)
% 1.32/209.48 # OLD status Res
% 1.32/209.48 # SinE strategy is GSinE(CountFormulas,hypos,1.4,,02,100,1.0)
% 1.32/209.48 # Preprocessing time : 0.062 s
% 1.32/209.48 # Running protocol protocol_eprover_2e85aeff02a0bd3743f362014f6604d7fba54d74 for 23 seconds:
% 1.32/209.48
% 1.32/209.48 # Failure: Resource limit exceeded (time)
% 1.32/209.48 # OLD status Res
% 1.32/209.48 # SinE strategy is GSinE(CountFormulas,hypos,1.1,,02,500,1.0)
% 1.32/209.48 # Preprocessing time : 0.029 s
% 1.32/209.48 # Running protocol protocol_eprover_334d43c175335e554899225728a5c2ebd420f86b for 23 seconds:
% 1.32/209.48
% 1.32/209.48 # Failure: Resource limit exceeded (time)
% 1.32/209.48 # OLD status Res
% 1.32/209.48 # Preprocessing time : 0.063 s
% 1.32/209.48 # Running protocol protocol_eprover_13918ce26d63c8fe682016bfda2032977bcbf85b for 23 seconds:
% 1.32/209.48 # Preprocessing time : 0.074 s
% 1.32/209.48
% 1.32/209.48 # Proof found!
% 1.32/209.48 # SZS status Theorem
% 1.32/209.48 # SZS output start CNFRefutation
% See solution above
% 1.32/209.48 # Proof object total steps : 122
% 1.32/209.48 # Proof object clause steps : 94
% 1.32/209.48 # Proof object formula steps : 28
% 1.32/209.48 # Proof object conjectures : 0
% 1.32/209.48 # Proof object clause conjectures : 0
% 1.32/209.48 # Proof object formula conjectures : 0
% 1.32/209.48 # Proof object initial clauses used : 36
% 1.32/209.48 # Proof object initial formulas used : 18
% 1.32/209.48 # Proof object generating inferences : 32
% 1.32/209.48 # Proof object simplifying inferences : 133
% 1.32/209.48 # Training examples: 0 positive, 0 negative
% 1.32/209.48 # Parsed axioms : 131
% 1.32/209.48 # Removed by relevancy pruning/SinE : 0
% 1.32/209.48 # Initial clauses : 302
% 1.32/209.48 # Removed in clause preprocessing : 2
% 1.32/209.48 # Initial clauses in saturation : 300
% 1.32/209.48 # Processed clauses : 4395
% 1.32/209.48 # ...of these trivial : 10
% 1.32/209.48 # ...subsumed : 2613
% 1.32/209.48 # ...remaining for further processing : 1772
% 1.32/209.48 # Other redundant clauses eliminated : 1197
% 1.32/209.48 # Clauses deleted for lack of memory : 0
% 1.32/209.48 # Backward-subsumed : 155
% 1.32/209.48 # Backward-rewritten : 485
% 1.32/209.48 # Generated clauses : 28646
% 1.32/209.48 # ...of the previous two non-trivial : 28170
% 1.32/209.48 # Contextual simplify-reflections : 0
% 1.32/209.48 # Paramodulations : 28355
% 1.32/209.48 # Factorizations : 1
% 1.32/209.48 # Equation resolutions : 1232
% 1.32/209.48 # Current number of processed clauses : 877
% 1.32/209.48 # Positive orientable unit clauses : 31
% 1.32/209.48 # Positive unorientable unit clauses: 0
% 1.32/209.48 # Negative unit clauses : 8
% 1.32/209.48 # Non-unit-clauses : 838
% 1.32/209.48 # Current number of unprocessed clauses: 11168
% 1.32/209.48 # ...number of literals in the above : 169446
% 1.32/209.48 # Current number of archived formulas : 0
% 1.32/209.48 # Current number of archived clauses : 640
% 1.32/209.48 # Clause-clause subsumption calls (NU) : 265737
% 1.32/209.48 # Rec. Clause-clause subsumption calls : 7798
% 1.32/209.48 # Non-unit clause-clause subsumptions : 2712
% 1.32/209.48 # Unit Clause-clause subsumption calls : 4093
% 1.32/209.48 # Rewrite failures with RHS unbound : 0
% 1.32/209.48 # BW rewrite match attempts : 12
% 1.32/209.48 # BW rewrite match successes : 10
% 1.32/209.48 # Condensation attempts : 0
% 1.32/209.48 # Condensation successes : 0
% 1.32/209.48 # Termbank termtop insertions : 1044184
% 1.32/209.48
% 1.32/209.48 # -------------------------------------------------
% 1.32/209.48 # User time : 0.975 s
% 1.32/209.48 # System time : 0.022 s
% 1.32/209.48 # Total time : 0.997 s
% 1.32/209.48 # Maximum resident set size: 35920 pages
% 1.34/230.58 eprover: CPU time limit exceeded, terminating
% 1.34/230.60 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 1.34/230.60 eprover: No such file or directory
% 1.34/230.60 eprover: CPU time limit exceeded, terminating
% 1.34/230.60 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 1.34/230.60 eprover: No such file or directory
% 1.34/230.61 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 1.34/230.61 eprover: No such file or directory
% 1.34/230.62 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 1.34/230.62 eprover: No such file or directory
% 1.34/230.67 eprover: CPU time limit exceeded, terminating
% 1.34/230.68 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 1.34/230.68 eprover: No such file or directory
% 1.34/230.69 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 1.34/230.69 eprover: No such file or directory
%------------------------------------------------------------------------------