%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO337+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:24:55 PM UTC 2026
% Result : Theorem 54.65s 7.39s
% Output : CNFRefutation 54.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 16
% Syntax : Number of formulae : 115 ( 32 unt; 0 def)
% Number of atoms : 688 ( 206 equ)
% Maximal formula atoms : 26 ( 5 avg)
% Number of connectives : 1031 ( 458 ~; 507 |; 62 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 41 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-3 aty)
% Number of variables : 240 ( 220 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
vangle(vd1378,vd1363,vd1362) = vangle(vd1361,vd1362,vd1363),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
vangle(vd1378,vd1363,vd1362) != vangle(vd1361,vd1362,vd1363),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
vf(vd1378,vd1363) = vf(vd1361,vd1362),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
rR(vd1378,vd1361,vd1363),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
rpoint(vd1378),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
? [Vd1368] :
( rpoint(Vd1368)
& vd1363 = Vd1368 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
vangle(vd1361,vd1362,vd1363) = vangle(vd1361,vd1363,vd1362),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
vd1362 != vd1363,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
vd1361 != vd1363,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
vd1361 != vd1362,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
? [Vd1367] :
( rpoint(Vd1367)
& vd1362 = Vd1367 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
? [Vd1366] :
( rpoint(Vd1366)
& vd1361 = Vd1366 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [Vd340,Vd341,Vd342] :
( ( ? [Vd344] :
( rpoint(Vd344)
& Vd340 = Vd344 )
& ? [Vd345] :
( rpoint(Vd345)
& Vd341 = Vd345 )
& ? [Vd346] :
( rpoint(Vd346)
& Vd342 = Vd346 )
& rR(Vd341,Vd340,Vd342) )
=> ( rR(Vd341,Vd342,Vd340)
& Vd340 != Vd341
& Vd340 != Vd342
& ~ rR(Vd340,Vd341,Vd342) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
vf(vd1361,vd1362) != vf(vd1361,vd1363),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [Vd352,Vd353,Vd354,Vd359,Vd360] :
( ( ? [Vd356] :
( rpoint(Vd356)
& Vd352 = Vd356 )
& ? [Vd357] :
( rpoint(Vd357)
& Vd353 = Vd357 )
& ? [Vd358] :
( rpoint(Vd358)
& Vd354 = Vd358 )
& rline(Vd360)
& rR(Vd353,Vd352,Vd354)
& ron(Vd352,Vd359)
& ron(Vd353,Vd359)
& Vd359 = Vd360 )
=> ron(Vd354,Vd359) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [Vd908,Vd909,Vd910,Vd911,Vd912,Vd919,Vd920] :
( ( ? [Vd914] :
( rpoint(Vd914)
& Vd908 = Vd914 )
& ? [Vd915] :
( rpoint(Vd915)
& Vd909 = Vd915 )
& ? [Vd916] :
( rpoint(Vd916)
& Vd910 = Vd916 )
& ? [Vd917] :
( rpoint(Vd917)
& Vd911 = Vd917 )
& ? [Vd918] :
( rpoint(Vd918)
& Vd912 = Vd918 )
& ? [Vd922] :
( rline(Vd922)
& Vd919 = Vd922 )
& ? [Vd923] :
( rline(Vd923)
& Vd920 = Vd923 )
& ron(Vd908,Vd919)
& ron(Vd909,Vd919)
& ron(Vd911,Vd919)
& ron(Vd910,Vd920)
& ron(Vd912,Vd920)
& Vd909 != Vd908
& Vd910 != Vd908
& Vd911 != Vd908
& Vd912 != Vd908
& ~ rR(Vd908,Vd909,Vd911)
& ~ rR(Vd908,Vd910,Vd912) )
=> vangle(Vd909,Vd908,Vd910) = vangle(Vd911,Vd908,Vd912) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [Vd217,Vd218] :
( ( ? [Vd220] :
( rpoint(Vd220)
& Vd217 = Vd220 )
& ? [Vd221] :
( rpoint(Vd221)
& Vd218 = Vd221 )
& Vd217 != Vd218 )
=> ? [Vd223] :
( rline(Vd223)
& ron(Vd217,Vd223)
& ron(Vd218,Vd223) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f132,plain,
vangle(vd1378,vd1363,vd1362) != vangle(vd1361,vd1362,vd1363),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f133,plain,
vf(vd1378,vd1363) = vf(vd1361,vd1362),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f135,plain,
rR(vd1378,vd1361,vd1363),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f136,plain,
rpoint(vd1378),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f137,plain,
( rpoint(sK0_skl)
& vd1363 = sK0_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vd1368,sK0_skl)],[f7]) ).
fof(f138,plain,
vd1363 = sK0_skl,
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f139,plain,
rpoint(sK0_skl),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f142,plain,
vangle(vd1361,vd1363,vd1362) = vangle(vd1361,vd1362,vd1363),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f143,plain,
vd1363 != vd1362,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f144,plain,
vd1363 != vd1361,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f145,plain,
vd1362 != vd1361,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f146,plain,
( rpoint(sK1_skl)
& vd1362 = sK1_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Vd1367,sK1_skl)],[f13]) ).
fof(f147,plain,
vd1362 = sK1_skl,
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f148,plain,
rpoint(sK1_skl),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f149,plain,
( rpoint(sK2_skl)
& vd1361 = sK2_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Vd1366,sK2_skl)],[f14]) ).
fof(f150,plain,
sK2_skl = vd1361,
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f151,plain,
rpoint(sK2_skl),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f208,plain,
! [Vd340,Vd341,Vd342] :
( ( rR(Vd341,Vd342,Vd340)
& Vd340 != Vd341
& Vd340 != Vd342
& ~ rR(Vd340,Vd341,Vd342) )
| ! [Vd344] :
( ~ rpoint(Vd344)
| Vd340 != Vd344 )
| ! [Vd345] :
( ~ rpoint(Vd345)
| Vd341 != Vd345 )
| ! [Vd346] :
( ~ rpoint(Vd346)
| Vd342 != Vd346 )
| ~ rR(Vd341,Vd340,Vd342) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f209,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ rR(X1,X0,X2)
| ~ rpoint(X5)
| X1 != X5
| ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X2 != X3
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f210,plain,
! [X0,X1,X2,X3,X4,X5] :
( X1 != X2
| ~ rpoint(X5)
| X1 != X5
| ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X2 != X3
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f211,plain,
! [X0,X1,X2,X3,X4,X5] :
( X1 != X0
| ~ rpoint(X5)
| X1 != X5
| ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X2 != X3
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f212,plain,
! [X0,X1,X2,X3,X4,X5] :
( rR(X0,X2,X1)
| ~ rpoint(X5)
| X1 != X5
| ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X2 != X3
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f238,plain,
vf(vd1361,vd1363) != vf(vd1361,vd1362),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f286,plain,
! [Vd352,Vd353,Vd354,Vd359,Vd360] :
( ron(Vd354,Vd359)
| ! [Vd356] :
( ~ rpoint(Vd356)
| Vd352 != Vd356 )
| ! [Vd357] :
( ~ rpoint(Vd357)
| Vd353 != Vd357 )
| ! [Vd358] :
( ~ rpoint(Vd358)
| Vd354 != Vd358 )
| ~ rline(Vd360)
| ~ rR(Vd353,Vd352,Vd354)
| ~ ron(Vd352,Vd359)
| ~ ron(Vd353,Vd359)
| Vd359 != Vd360 ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f287,plain,
! [Vd354,Vd359] :
( ron(Vd354,Vd359)
| ! [Vd352] :
( ! [Vd356] :
( ~ rpoint(Vd356)
| Vd352 != Vd356 )
| ! [Vd353] :
( ! [Vd357] :
( ~ rpoint(Vd357)
| Vd353 != Vd357 )
| ! [Vd358] :
( ~ rpoint(Vd358)
| Vd354 != Vd358 )
| ! [Vd360] :
( ~ rline(Vd360)
| ~ rR(Vd353,Vd352,Vd354)
| ~ ron(Vd352,Vd359)
| ~ ron(Vd353,Vd359)
| Vd359 != Vd360 ) ) ) ),
inference(miniscoping,[status(thm)],[f286]) ).
fof(f288,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ron(X4,X0)
| ~ rpoint(X7)
| X3 != X7
| ~ rpoint(X6)
| X2 != X6
| ~ rpoint(X5)
| X4 != X5
| ~ rline(X1)
| ~ rR(X2,X3,X4)
| ~ ron(X3,X0)
| ~ ron(X2,X0)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f287]) ).
fof(f295,plain,
! [Vd908,Vd909,Vd910,Vd911,Vd912,Vd919,Vd920] :
( vangle(Vd909,Vd908,Vd910) = vangle(Vd911,Vd908,Vd912)
| ! [Vd914] :
( ~ rpoint(Vd914)
| Vd908 != Vd914 )
| ! [Vd915] :
( ~ rpoint(Vd915)
| Vd909 != Vd915 )
| ! [Vd916] :
( ~ rpoint(Vd916)
| Vd910 != Vd916 )
| ! [Vd917] :
( ~ rpoint(Vd917)
| Vd911 != Vd917 )
| ! [Vd918] :
( ~ rpoint(Vd918)
| Vd912 != Vd918 )
| ! [Vd922] :
( ~ rline(Vd922)
| Vd919 != Vd922 )
| ! [Vd923] :
( ~ rline(Vd923)
| Vd920 != Vd923 )
| ~ ron(Vd908,Vd919)
| ~ ron(Vd909,Vd919)
| ~ ron(Vd911,Vd919)
| ~ ron(Vd910,Vd920)
| ~ ron(Vd912,Vd920)
| Vd909 = Vd908
| Vd910 = Vd908
| Vd911 = Vd908
| Vd912 = Vd908
| rR(Vd908,Vd909,Vd911)
| rR(Vd908,Vd910,Vd912) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f296,plain,
! [Vd908,Vd909,Vd910,Vd911,Vd912] :
( vangle(Vd909,Vd908,Vd910) = vangle(Vd911,Vd908,Vd912)
| ! [Vd914] :
( ~ rpoint(Vd914)
| Vd908 != Vd914 )
| ! [Vd915] :
( ~ rpoint(Vd915)
| Vd909 != Vd915 )
| ! [Vd916] :
( ~ rpoint(Vd916)
| Vd910 != Vd916 )
| ! [Vd917] :
( ~ rpoint(Vd917)
| Vd911 != Vd917 )
| ! [Vd918] :
( ~ rpoint(Vd918)
| Vd912 != Vd918 )
| ! [Vd919] :
( ! [Vd922] :
( ~ rline(Vd922)
| Vd919 != Vd922 )
| ! [Vd920] :
( ! [Vd923] :
( ~ rline(Vd923)
| Vd920 != Vd923 )
| ~ ron(Vd908,Vd919)
| ~ ron(Vd909,Vd919)
| ~ ron(Vd911,Vd919)
| ~ ron(Vd910,Vd920)
| ~ ron(Vd912,Vd920)
| Vd909 = Vd908
| Vd910 = Vd908
| Vd911 = Vd908
| Vd912 = Vd908
| rR(Vd908,Vd909,Vd911)
| rR(Vd908,Vd910,Vd912) ) ) ),
inference(miniscoping,[status(thm)],[f295]) ).
fof(f297,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13] :
( vangle(X3,X0,X1) = vangle(X4,X0,X2)
| ~ rpoint(X13)
| X0 != X13
| ~ rpoint(X12)
| X3 != X12
| ~ rpoint(X11)
| X1 != X11
| ~ rpoint(X10)
| X4 != X10
| ~ rpoint(X9)
| X2 != X9
| ~ rline(X8)
| X6 != X8
| ~ rline(X7)
| X5 != X7
| ~ ron(X0,X6)
| ~ ron(X3,X6)
| ~ ron(X4,X6)
| ~ ron(X1,X5)
| ~ ron(X2,X5)
| X3 = X0
| X1 = X0
| X4 = X0
| X2 = X0
| rR(X0,X3,X4)
| rR(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f303,plain,
! [Vd217,Vd218] :
( ? [Vd223] :
( rline(Vd223)
& ron(Vd217,Vd223)
& ron(Vd218,Vd223) )
| ! [Vd220] :
( ~ rpoint(Vd220)
| Vd217 != Vd220 )
| ! [Vd221] :
( ~ rpoint(Vd221)
| Vd218 != Vd221 )
| Vd217 = Vd218 ),
inference(pre_NNF_transformation,[status(thm)],[f60]) ).
fof(f304,plain,
! [Vd217,Vd218] :
( ( rline(sK11_skl(Vd218,Vd217))
& ron(Vd217,sK11_skl(Vd218,Vd217))
& ron(Vd218,sK11_skl(Vd218,Vd217)) )
| ! [Vd220] :
( ~ rpoint(Vd220)
| Vd217 != Vd220 )
| ! [Vd221] :
( ~ rpoint(Vd221)
| Vd218 != Vd221 )
| Vd217 = Vd218 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(Vd223,sK11_skl(Vd218,Vd217))],[f303]) ).
fof(f305,plain,
! [X0,X1,X2,X3] :
( ron(X1,sK11_skl(X1,X0))
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f306,plain,
! [X0,X1,X2,X3] :
( ron(X0,sK11_skl(X1,X0))
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f307,plain,
! [X0,X1,X2,X3] :
( rline(sK11_skl(X1,X0))
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f680,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ ron(X1,X5)
| X1 = X4
| ~ ron(X2,X6)
| rR(X1,X0,X2)
| ~ ron(X0,X6)
| rR(X1,X3,X4)
| ~ rline(X5)
| ~ rline(X6)
| ~ rpoint(X1)
| ~ ron(X3,X5)
| X3 = X1
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ ron(X4,X5)
| ~ rpoint(X4)
| vangle(X3,X1,X0) = vangle(X4,X1,X2)
| X0 = X1
| X1 = X2
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f297]) ).
fof(f721,plain,
! [X0,X1] :
( ~ rpoint(X0)
| X1 = X0
| ~ rpoint(X1)
| ron(X0,sK11_skl(X1,X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f306]) ).
fof(f736,plain,
! [X0,X1] :
( X0 = X1
| ~ rpoint(X1)
| ~ rpoint(X0)
| rline(sK11_skl(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f307]) ).
fof(f763,plain,
! [X4,X3] :
( ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rR(X4,X3,X3) ),
inference(destructive_equality_resolution,[status(thm)],[f210]) ).
fof(f764,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rR(X1,X0,X0)
| ~ rpoint(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f763]) ).
fof(f771,plain,
! [X0,X1,X2] :
( ~ rR(X1,X0,X2)
| ~ rpoint(X2)
| ~ rR(X0,X1,X2)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f209]) ).
fof(f815,plain,
! [X0,X1,X2,X3] :
( ~ rR(X3,X1,X0)
| ~ rpoint(X3)
| ~ rline(X2)
| ron(X0,X2)
| ~ ron(X3,X2)
| ~ ron(X1,X2)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f288]) ).
fof(f824,plain,
! [X4,X3] :
( ~ rpoint(X4)
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rR(X4,X4,X3) ),
inference(destructive_equality_resolution,[status(thm)],[f211]) ).
fof(f825,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rR(X0,X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f824]) ).
fof(f835,plain,
! [X0,X1] :
( ron(X0,sK11_skl(X0,X1))
| ~ rpoint(X1)
| ~ rpoint(X0)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f305]) ).
fof(f867,plain,
! [X0,X1,X2] :
( rR(X2,X0,X1)
| ~ rR(X2,X1,X0)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f212]) ).
fof(f916,plain,
vangle(vd1361,vd1363,vd1362) != vangle(vd1378,vd1363,vd1362),
inference(backward_demodulation,[status(thm)],[f142,f132]) ).
fof(f921,plain,
! [X0,X1] :
( ~ ron(vd1363,X0)
| vd1363 = vd1378
| ~ ron(vd1362,X1)
| rR(vd1363,vd1362,vd1362)
| ~ ron(vd1362,X1)
| rR(vd1363,vd1361,vd1378)
| ~ rline(X0)
| ~ rline(X1)
| ~ rpoint(vd1363)
| ~ ron(vd1361,X0)
| vd1361 = vd1363
| ~ rpoint(vd1362)
| ~ rpoint(vd1361)
| ~ ron(vd1378,X0)
| ~ rpoint(vd1378)
| vd1362 = vd1363
| vd1363 = vd1362
| ~ rpoint(vd1362) ),
inference(resolution,[status(thm)],[f916,f680]) ).
fof(f925,plain,
! [X0,X1] :
( ~ ron(vd1363,X0)
| vd1363 = vd1378
| rR(vd1363,vd1362,vd1362)
| ~ ron(vd1362,X1)
| rR(vd1363,vd1361,vd1378)
| ~ rline(X0)
| ~ rline(X1)
| ~ rpoint(vd1363)
| ~ ron(vd1361,X0)
| vd1361 = vd1363
| ~ rpoint(vd1361)
| ~ ron(vd1378,X0)
| ~ rpoint(vd1378)
| vd1363 = vd1362
| ~ rpoint(vd1362) ),
inference(duplicate_literals_removal,[status(thm)],[f921]) ).
fof(f926,plain,
! [X0,X1] :
( vd1378 = vd1363
| ~ ron(vd1361,X0)
| ~ rline(X1)
| ~ ron(vd1362,X1)
| ~ ron(vd1363,X0)
| rR(vd1363,vd1362,vd1362)
| ~ rpoint(vd1363)
| vd1363 = vd1361
| ~ rpoint(vd1362)
| ~ rpoint(vd1378)
| rR(vd1363,vd1361,vd1378)
| ~ rline(X0)
| ~ ron(vd1378,X0)
| ~ rpoint(vd1361) ),
inference(forward_subsumption_resolution,[status(thm)],[f925,f143]) ).
fof(f928,plain,
! [X0,X1] :
( ~ rline(X0)
| ~ ron(vd1363,X0)
| ~ ron(vd1362,X1)
| ~ rpoint(vd1363)
| vd1363 = vd1378
| ~ rline(X1)
| ~ rpoint(vd1361)
| ~ rpoint(vd1362)
| vd1361 = vd1363
| rR(vd1363,vd1361,vd1378)
| rR(vd1363,vd1362,vd1362)
| ~ ron(vd1378,X0)
| ~ ron(vd1361,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f926,f136]) ).
fof(f929,plain,
! [X0,X1] :
( ~ rline(X0)
| ~ ron(vd1363,X0)
| ~ ron(vd1362,X1)
| ~ rpoint(vd1363)
| vd1363 = vd1378
| ~ rline(X1)
| ~ rpoint(vd1362)
| vd1361 = vd1363
| rR(vd1363,vd1361,vd1378)
| rR(vd1363,vd1362,vd1362)
| ~ ron(vd1378,X0)
| ~ ron(vd1361,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f928,f931]) ).
fof(f931,plain,
rpoint(vd1361),
inference(forward_demodulation,[status(thm)],[f150,f151]) ).
fof(f933,plain,
! [X0,X1] :
( ~ ron(vd1361,X1)
| ~ ron(vd1378,X1)
| ~ rpoint(vd1363)
| rR(vd1363,vd1362,vd1362)
| ~ rline(X1)
| rR(vd1363,vd1361,vd1378)
| ~ rpoint(vd1362)
| ~ ron(vd1363,X1)
| ~ rline(X0)
| ~ ron(vd1362,X0)
| vd1363 = vd1378 ),
inference(forward_subsumption_resolution,[status(thm)],[f929,f144]) ).
fof(f937,plain,
rpoint(vd1363),
inference(backward_demodulation,[status(thm)],[f138,f139]) ).
fof(f938,plain,
rpoint(vd1362),
inference(backward_demodulation,[status(thm)],[f147,f148]) ).
fof(f951,plain,
! [X0,X1] :
( ~ ron(vd1362,X0)
| ~ ron(vd1363,X1)
| vd1378 = vd1363
| rR(vd1363,vd1362,vd1362)
| ~ ron(vd1361,X1)
| ~ ron(vd1378,X1)
| rR(vd1363,vd1361,vd1378)
| ~ rpoint(vd1362)
| ~ rline(X1)
| ~ rline(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f933,f937]) ).
fof(f955,plain,
! [X0,X1] :
( rR(vd1363,vd1361,vd1378)
| ~ ron(vd1378,X0)
| ~ ron(vd1362,X1)
| ~ rline(X1)
| rR(vd1363,vd1362,vd1362)
| vd1378 = vd1363
| ~ ron(vd1363,X0)
| ~ ron(vd1361,X0)
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f951,f938]) ).
fof(f977,plain,
! [X0,X1] :
( rR(vd1363,vd1361,vd1378)
| ~ ron(vd1378,X0)
| ~ ron(vd1362,X1)
| ~ rline(X1)
| vd1378 = vd1363
| ~ ron(vd1363,X0)
| ~ ron(vd1361,X0)
| ~ rline(X0)
| ~ rpoint(vd1363)
| ~ rpoint(vd1362) ),
inference(resolution,[status(thm)],[f764,f955]) ).
fof(f978,plain,
! [X0,X1] :
( ~ rline(X0)
| ~ rline(X1)
| ~ ron(vd1378,X0)
| ~ ron(vd1362,X1)
| vd1363 = vd1378
| ~ rpoint(vd1363)
| ~ ron(vd1363,X0)
| rR(vd1363,vd1361,vd1378)
| ~ ron(vd1361,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f977,f938]) ).
fof(f979,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ rline(X0)
| ~ ron(vd1362,X1)
| ~ ron(vd1378,X0)
| vd1363 = vd1378
| ~ ron(vd1363,X0)
| rR(vd1363,vd1361,vd1378)
| ~ ron(vd1361,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f978,f937]) ).
fof(f1670,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ rline(X0)
| ~ ron(vd1362,X1)
| ~ ron(vd1378,X0)
| vd1363 = vd1378
| ~ ron(vd1363,X0)
| ~ ron(vd1361,X0)
| rR(vd1363,vd1378,vd1361)
| ~ rpoint(vd1363)
| ~ rpoint(vd1361)
| ~ rpoint(vd1378) ),
inference(resolution,[status(thm)],[f867,f979]) ).
fof(f1672,plain,
( rR(vd1378,vd1363,vd1361)
| ~ rpoint(vd1378)
| ~ rpoint(vd1361)
| ~ rpoint(vd1363) ),
inference(resolution,[status(thm)],[f867,f135]) ).
fof(f1678,plain,
! [X0,X1] :
( ~ rpoint(vd1361)
| ~ ron(vd1362,X0)
| ~ ron(vd1378,X1)
| ~ ron(vd1361,X1)
| vd1363 = vd1378
| rR(vd1363,vd1378,vd1361)
| ~ rline(X1)
| ~ ron(vd1363,X1)
| ~ rpoint(vd1363)
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1670,f136]) ).
fof(f1679,plain,
( rR(vd1378,vd1363,vd1361)
| ~ rpoint(vd1378)
| ~ rpoint(vd1361) ),
inference(forward_subsumption_resolution,[status(thm)],[f1672,f937]) ).
fof(f1682,plain,
! [X0,X1] :
( ~ ron(vd1361,X0)
| rR(vd1363,vd1378,vd1361)
| ~ ron(vd1362,X1)
| ~ ron(vd1378,X0)
| ~ rline(X1)
| vd1363 = vd1378
| ~ rpoint(vd1361)
| ~ ron(vd1363,X0)
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1678,f937]) ).
fof(f1694,plain,
( ~ rpoint(vd1378)
| rR(vd1378,vd1363,vd1361) ),
inference(forward_subsumption_resolution,[status(thm)],[f1679,f931]) ).
fof(f1697,plain,
( ~ rpoint(vd1361)
| ~ rR(vd1363,vd1378,vd1361)
| ~ rpoint(vd1378)
| ~ rpoint(vd1363)
| ~ rpoint(vd1378) ),
inference(resolution,[status(thm)],[f1694,f771]) ).
fof(f1706,plain,
( ~ rpoint(vd1361)
| ~ rR(vd1363,vd1378,vd1361)
| ~ rpoint(vd1363)
| ~ rpoint(vd1378) ),
inference(duplicate_literals_removal,[status(thm)],[f1697]) ).
fof(f1707,plain,
( ~ rpoint(vd1361)
| ~ rpoint(vd1363)
| ~ rR(vd1363,vd1378,vd1361) ),
inference(forward_subsumption_resolution,[status(thm)],[f1706,f136]) ).
fof(f1712,plain,
! [X0,X1] :
( ~ ron(vd1361,X0)
| ~ ron(vd1362,X1)
| ~ ron(vd1378,X0)
| ~ rline(X1)
| vd1363 = vd1378
| ~ rpoint(vd1361)
| ~ ron(vd1363,X0)
| ~ rline(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1682,f1713]) ).
fof(f1713,plain,
( ~ rR(vd1363,vd1378,vd1361)
| ~ rpoint(vd1361) ),
inference(forward_subsumption_resolution,[status(thm)],[f1707,f937]) ).
fof(f1715,plain,
! [X0,X1] :
( ~ ron(vd1363,X0)
| ~ rline(X1)
| vd1378 = vd1363
| ~ ron(vd1361,X0)
| ~ ron(vd1362,X1)
| ~ rline(X0)
| ~ ron(vd1378,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1712,f931]) ).
fof(f1721,plain,
! [X0,X1] :
( ~ rpoint(vd1378)
| X0 = vd1378
| ~ rpoint(X0)
| ~ ron(vd1363,sK11_skl(X0,vd1378))
| ~ rline(X1)
| vd1378 = vd1363
| ~ ron(vd1361,sK11_skl(X0,vd1378))
| ~ ron(vd1362,X1)
| ~ rline(sK11_skl(X0,vd1378)) ),
inference(resolution,[status(thm)],[f1715,f721]) ).
fof(f1724,plain,
! [X0,X1] :
( ~ rline(X0)
| vd1363 = vd1378
| vd1378 = X1
| ~ rpoint(vd1378)
| ~ ron(vd1363,sK11_skl(X1,vd1378))
| ~ ron(vd1361,sK11_skl(X1,vd1378))
| ~ rpoint(X1)
| ~ ron(vd1362,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1721,f736]) ).
fof(f1875,plain,
! [X0,X1] :
( ~ ron(vd1362,X1)
| ~ ron(vd1361,sK11_skl(X0,vd1378))
| ~ rline(X1)
| ~ ron(vd1363,sK11_skl(X0,vd1378))
| vd1363 = vd1378
| vd1378 = X0
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1724,f136]) ).
fof(f5267,plain,
! [X0] :
( ~ rpoint(vd1378)
| ~ rline(X0)
| ron(vd1363,X0)
| ~ ron(vd1378,X0)
| ~ ron(vd1361,X0)
| ~ rpoint(vd1361)
| ~ rpoint(vd1363) ),
inference(resolution,[status(thm)],[f815,f135]) ).
fof(f5299,plain,
! [X0] :
( ~ rline(X0)
| ron(vd1363,X0)
| ~ ron(vd1378,X0)
| ~ ron(vd1361,X0)
| ~ rpoint(vd1378)
| ~ rpoint(vd1361) ),
inference(forward_subsumption_resolution,[status(thm)],[f5267,f937]) ).
fof(f5326,plain,
! [X0] :
( ~ rpoint(vd1378)
| ron(vd1363,X0)
| ~ rline(X0)
| ~ ron(vd1378,X0)
| ~ ron(vd1361,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5299,f931]) ).
fof(f5341,plain,
! [X0,X1] :
( ~ ron(vd1362,X1)
| ~ ron(vd1361,sK11_skl(X0,vd1378))
| ~ rline(X1)
| vd1363 = vd1378
| vd1378 = X0
| ~ rpoint(X0)
| ~ rpoint(vd1378)
| ~ rline(sK11_skl(X0,vd1378))
| ~ ron(vd1378,sK11_skl(X0,vd1378))
| ~ ron(vd1361,sK11_skl(X0,vd1378)) ),
inference(resolution,[status(thm)],[f5326,f1875]) ).
fof(f5377,plain,
! [X0,X1] :
( ~ ron(vd1362,X1)
| ~ rline(X1)
| vd1363 = vd1378
| vd1378 = X0
| ~ rpoint(X0)
| ~ rpoint(vd1378)
| ~ rline(sK11_skl(X0,vd1378))
| ~ ron(vd1378,sK11_skl(X0,vd1378))
| ~ ron(vd1361,sK11_skl(X0,vd1378)) ),
inference(duplicate_literals_removal,[status(thm)],[f5341]) ).
fof(f5378,plain,
! [X0,X1] :
( vd1378 = X0
| vd1378 = vd1363
| ~ ron(vd1362,X1)
| ~ rline(X1)
| ~ rline(sK11_skl(X0,vd1378))
| ~ rpoint(X0)
| ~ rpoint(vd1378)
| ~ ron(vd1361,sK11_skl(X0,vd1378)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5377,f721]) ).
fof(f5462,plain,
! [X0,X1] :
( ~ rpoint(X0)
| X0 = vd1378
| ~ rline(X1)
| ~ ron(vd1362,X1)
| vd1378 = vd1363
| ~ rline(sK11_skl(X0,vd1378))
| ~ ron(vd1361,sK11_skl(X0,vd1378)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5378,f136]) ).
fof(f5463,plain,
! [X0] :
( ~ rpoint(vd1378)
| ~ rpoint(vd1361)
| vd1361 = vd1378
| ~ rpoint(vd1361)
| vd1361 = vd1378
| ~ rline(X0)
| ~ ron(vd1362,X0)
| vd1378 = vd1363
| ~ rline(sK11_skl(vd1361,vd1378)) ),
inference(resolution,[status(thm)],[f5462,f835]) ).
fof(f5464,plain,
! [X0] :
( ~ rpoint(vd1378)
| ~ rpoint(vd1361)
| vd1361 = vd1378
| ~ rline(X0)
| ~ ron(vd1362,X0)
| vd1378 = vd1363
| ~ rline(sK11_skl(vd1361,vd1378)) ),
inference(duplicate_literals_removal,[status(thm)],[f5463]) ).
fof(f5465,plain,
! [X0] :
( ~ ron(vd1362,X0)
| ~ rpoint(vd1361)
| ~ rline(X0)
| vd1361 = vd1378
| vd1378 = vd1363
| ~ rpoint(vd1378) ),
inference(forward_subsumption_resolution,[status(thm)],[f5464,f736]) ).
fof(f5466,plain,
! [X0] :
( ~ rpoint(vd1361)
| ~ rline(X0)
| vd1378 = vd1363
| vd1378 = vd1361
| ~ ron(vd1362,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5465,f136]) ).
fof(f5472,plain,
! [X0] :
( ~ rpoint(X0)
| ~ rpoint(vd1362)
| vd1362 = X0
| ~ rpoint(vd1361)
| ~ rline(sK11_skl(vd1362,X0))
| vd1378 = vd1363
| vd1378 = vd1361 ),
inference(resolution,[status(thm)],[f5466,f835]) ).
fof(f5479,plain,
! [X0] :
( ~ rpoint(vd1361)
| vd1378 = vd1363
| vd1361 = vd1378
| ~ rpoint(X0)
| ~ rpoint(vd1362)
| X0 = vd1362 ),
inference(forward_subsumption_resolution,[status(thm)],[f5472,f736]) ).
fof(f5489,plain,
! [X0] :
( ~ rpoint(X0)
| vd1378 = vd1363
| ~ rpoint(vd1361)
| X0 = vd1362
| vd1361 = vd1378 ),
inference(forward_subsumption_resolution,[status(thm)],[f5479,f938]) ).
fof(f5490,plain,
( vd1378 = vd1363
| vd1361 = vd1362
| vd1361 = vd1378 ),
inference(resolution,[status(thm)],[f5489,f931]) ).
fof(f5567,plain,
( vd1378 = vd1361
| vd1378 = vd1363 ),
inference(forward_subsumption_resolution,[status(thm)],[f5490,f145]) ).
fof(f5650,plain,
( vd1378 = vd1361
| ~ rpoint(vd1378)
| rR(vd1363,vd1363,vd1361) ),
inference(paramodulation,[status(thm)],[f5567,f1694]) ).
fof(f5679,plain,
( vd1378 = vd1361
| rR(vd1363,vd1363,vd1361) ),
inference(forward_subsumption_resolution,[status(thm)],[f5650,f136]) ).
fof(f5746,plain,
( ~ rpoint(vd1361)
| ~ rpoint(vd1363)
| vd1378 = vd1361 ),
inference(resolution,[status(thm)],[f5679,f825]) ).
fof(f5760,plain,
( vd1361 = vd1378
| ~ rpoint(vd1361) ),
inference(forward_subsumption_resolution,[status(thm)],[f5746,f937]) ).
fof(f5926,plain,
vf(vd1361,vd1363) = vf(vd1361,vd1362),
inference(backward_demodulation,[status(thm)],[f5930,f133]) ).
fof(f5930,plain,
vd1378 = vd1361,
inference(forward_subsumption_resolution,[status(thm)],[f5760,f931]) ).
fof(f5976,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f5926,f238]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO337+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n001.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sun Sep 20 15:36:42 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 54.65/7.39 % Refutation found
% 54.65/7.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 54.65/7.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 18.35/7.43 % Elapsed time: 7.063958 seconds
% 18.35/7.43 % CPU time: 55.585964 seconds
% 18.35/7.43 % Total memory used: 273.134 MB
% 18.35/7.43 % Net memory used: 257.449 MB
%------------------------------------------------------------------------------