%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO286+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:50 PM UTC 2026
% Result : Theorem 38.78s 5.51s
% Output : CNFRefutation 38.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 9
% Syntax : Number of formulae : 76 ( 31 unt; 0 def)
% Number of atoms : 434 ( 45 equ)
% Maximal formula atoms : 18 ( 5 avg)
% Number of connectives : 644 ( 286 ~; 312 |; 44 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-4 aty)
% Number of variables : 107 ( 102 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
? [Vd1153] :
( rpoint(Vd1153)
& ron(Vd1153,vd1151)
& ron(Vd1153,vd1152)
& rR(Vd1153,vd1123,vd1125) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ? [Vd1153] :
( rpoint(Vd1153)
& ron(Vd1153,vd1151)
& ron(Vd1153,vd1152)
& rR(Vd1153,vd1123,vd1125) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
~ ron(vd1125,vd1152),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
~ rinside(vd1125,vd1152),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
( ron(vd1123,vd1151)
& ron(vd1125,vd1151)
& rcircle(vd1152)
& rcenter(vd1123,vd1152)
& ron(vd1127,vd1152) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
vd1123 = vd1129,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
( rpoint(vd1124)
& vd1123 = vd1124
& rpoint(vd1126)
& vd1125 = vd1126
& rpoint(vd1128)
& vd1127 = vd1128
& rpoint(vd1130)
& vd1129 = vd1130
& vd1123 != vd1125
& vd1127 != vd1129
& rless(vf(vd1127,vd1129),vf(vd1123,vd1125)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
rline(vd1151),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [Vd253,Vd254,Vd255,Vd256,Vd257,Vd258,Vd259,Vd260] :
( ( rcircle(Vd254)
& Vd253 = Vd254
& rline(Vd256)
& Vd255 = Vd256
& rpoint(Vd258)
& Vd257 = Vd258
& rinside(Vd257,Vd253)
& ron(Vd257,Vd255)
& rpoint(Vd260)
& Vd259 = Vd260
& ~ rinside(Vd259,Vd253)
& ~ ron(Vd259,Vd253)
& ron(Vd259,Vd255) )
=> ? [Vd261] :
( rpoint(Vd261)
& ron(Vd261,Vd255)
& ron(Vd261,Vd253)
& rR(Vd261,Vd257,Vd259) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [Vd334,Vd335] :
( rcenter(Vd334,Vd335)
=> rinside(Vd334,Vd335) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f137,plain,
! [Vd1153] :
( ~ rpoint(Vd1153)
| ~ ron(Vd1153,vd1151)
| ~ ron(Vd1153,vd1152)
| ~ rR(Vd1153,vd1123,vd1125) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f138,plain,
! [X0] :
( ~ rpoint(X0)
| ~ ron(X0,vd1151)
| ~ ron(X0,vd1152)
| ~ rR(X0,vd1123,vd1125) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f139,plain,
~ ron(vd1125,vd1152),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f140,plain,
~ rinside(vd1125,vd1152),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f142,plain,
rcenter(vd1123,vd1152),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f143,plain,
rcircle(vd1152),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f144,plain,
ron(vd1125,vd1151),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f145,plain,
ron(vd1123,vd1151),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f146,plain,
vd1123 = vd1129,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f150,plain,
vd1129 = vd1130,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f154,plain,
vd1125 = vd1126,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f155,plain,
rpoint(vd1126),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f156,plain,
vd1123 = vd1124,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f157,plain,
rpoint(vd1124),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f172,plain,
rline(vd1151),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f197,plain,
! [Vd253,Vd254,Vd255,Vd256,Vd257,Vd258,Vd259,Vd260] :
( ? [Vd261] :
( rpoint(Vd261)
& ron(Vd261,Vd255)
& ron(Vd261,Vd253)
& rR(Vd261,Vd257,Vd259) )
| ~ rcircle(Vd254)
| Vd253 != Vd254
| ~ rline(Vd256)
| Vd255 != Vd256
| ~ rpoint(Vd258)
| Vd257 != Vd258
| ~ rinside(Vd257,Vd253)
| ~ ron(Vd257,Vd255)
| ~ rpoint(Vd260)
| Vd259 != Vd260
| rinside(Vd259,Vd253)
| ron(Vd259,Vd253)
| ~ ron(Vd259,Vd255) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f198,plain,
! [Vd253,Vd255,Vd257,Vd259] :
( ? [Vd261] :
( rpoint(Vd261)
& ron(Vd261,Vd255)
& ron(Vd261,Vd253)
& rR(Vd261,Vd257,Vd259) )
| ! [Vd254] :
( ~ rcircle(Vd254)
| Vd253 != Vd254
| ! [Vd256] :
( ~ rline(Vd256)
| Vd255 != Vd256
| ! [Vd258] :
( ~ rpoint(Vd258)
| Vd257 != Vd258
| ~ rinside(Vd257,Vd253)
| ~ ron(Vd257,Vd255)
| ! [Vd260] :
( ~ rpoint(Vd260)
| Vd259 != Vd260
| rinside(Vd259,Vd253)
| ron(Vd259,Vd253)
| ~ ron(Vd259,Vd255) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f197]) ).
fof(f199,plain,
! [Vd253,Vd255,Vd257,Vd259] :
( ( rpoint(sK3_skl(Vd259,Vd257,Vd255,Vd253))
& ron(sK3_skl(Vd259,Vd257,Vd255,Vd253),Vd255)
& ron(sK3_skl(Vd259,Vd257,Vd255,Vd253),Vd253)
& rR(sK3_skl(Vd259,Vd257,Vd255,Vd253),Vd257,Vd259) )
| ! [Vd254] :
( ~ rcircle(Vd254)
| Vd253 != Vd254
| ! [Vd256] :
( ~ rline(Vd256)
| Vd255 != Vd256
| ! [Vd258] :
( ~ rpoint(Vd258)
| Vd257 != Vd258
| ~ rinside(Vd257,Vd253)
| ~ ron(Vd257,Vd255)
| ! [Vd260] :
( ~ rpoint(Vd260)
| Vd259 != Vd260
| rinside(Vd259,Vd253)
| ron(Vd259,Vd253)
| ~ ron(Vd259,Vd255) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(Vd261,sK3_skl(Vd259,Vd257,Vd255,Vd253))],[f198]) ).
fof(f200,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( rR(sK3_skl(X0,X4,X1,X2),X4,X0)
| ~ rcircle(X7)
| X2 != X7
| ~ rline(X6)
| X1 != X6
| ~ rpoint(X5)
| X4 != X5
| ~ rinside(X4,X2)
| ~ ron(X4,X1)
| ~ rpoint(X3)
| X0 != X3
| rinside(X0,X2)
| ron(X0,X2)
| ~ ron(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f201,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ron(sK3_skl(X0,X4,X1,X2),X2)
| ~ rcircle(X7)
| X2 != X7
| ~ rline(X6)
| X1 != X6
| ~ rpoint(X5)
| X4 != X5
| ~ rinside(X4,X2)
| ~ ron(X4,X1)
| ~ rpoint(X3)
| X0 != X3
| rinside(X0,X2)
| ron(X0,X2)
| ~ ron(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f202,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ron(sK3_skl(X0,X4,X1,X2),X1)
| ~ rcircle(X7)
| X2 != X7
| ~ rline(X6)
| X1 != X6
| ~ rpoint(X5)
| X4 != X5
| ~ rinside(X4,X2)
| ~ ron(X4,X1)
| ~ rpoint(X3)
| X0 != X3
| rinside(X0,X2)
| ron(X0,X2)
| ~ ron(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f203,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( rpoint(sK3_skl(X0,X4,X1,X2))
| ~ rcircle(X7)
| X2 != X7
| ~ rline(X6)
| X1 != X6
| ~ rpoint(X5)
| X4 != X5
| ~ rinside(X4,X2)
| ~ ron(X4,X1)
| ~ rpoint(X3)
| X0 != X3
| rinside(X0,X2)
| ron(X0,X2)
| ~ ron(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f408,plain,
! [Vd334,Vd335] :
( rinside(Vd334,Vd335)
| ~ rcenter(Vd334,Vd335) ),
inference(pre_NNF_transformation,[status(thm)],[f84]) ).
fof(f409,plain,
! [X0,X1] :
( rinside(X0,X1)
| ~ rcenter(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f408]) ).
fof(f723,plain,
! [X0,X1,X2,X3] :
( rR(sK3_skl(X0,X3,X1,X2),X3,X0)
| ~ rcircle(X2)
| ~ rline(X1)
| ~ rpoint(X3)
| ~ rinside(X3,X2)
| ~ ron(X3,X1)
| ~ rpoint(X0)
| rinside(X0,X2)
| ron(X0,X2)
| ~ ron(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f200]) ).
fof(f724,plain,
! [X0,X1,X2,X3] :
( ron(sK3_skl(X0,X3,X1,X2),X2)
| ~ rcircle(X2)
| ~ rline(X1)
| ~ rpoint(X3)
| ~ rinside(X3,X2)
| ~ ron(X3,X1)
| ~ rpoint(X0)
| rinside(X0,X2)
| ron(X0,X2)
| ~ ron(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f201]) ).
fof(f725,plain,
! [X0,X1,X2,X3] :
( ron(sK3_skl(X0,X3,X1,X2),X1)
| ~ rcircle(X2)
| ~ rline(X1)
| ~ rpoint(X3)
| ~ rinside(X3,X2)
| ~ ron(X3,X1)
| ~ rpoint(X0)
| rinside(X0,X2)
| ron(X0,X2)
| ~ ron(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f202]) ).
fof(f726,plain,
! [X0,X1,X2,X3] :
( rpoint(sK3_skl(X0,X3,X1,X2))
| ~ rcircle(X2)
| ~ rline(X1)
| ~ rpoint(X3)
| ~ rinside(X3,X2)
| ~ ron(X3,X1)
| ~ rpoint(X0)
| rinside(X0,X2)
| ron(X0,X2)
| ~ ron(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f203]) ).
fof(f938,plain,
ron(vd1129,vd1151),
inference(backward_demodulation,[status(thm)],[f146,f145]) ).
fof(f939,plain,
rcenter(vd1129,vd1152),
inference(backward_demodulation,[status(thm)],[f146,f142]) ).
fof(f941,plain,
! [X0] :
( ~ rpoint(X0)
| ~ ron(X0,vd1151)
| ~ ron(X0,vd1152)
| ~ rR(X0,vd1129,vd1125) ),
inference(backward_demodulation,[status(thm)],[f146,f138]) ).
fof(f943,plain,
vd1123 = vd1130,
inference(backward_demodulation,[status(thm)],[f150,f146]) ).
fof(f945,plain,
ron(vd1126,vd1151),
inference(backward_demodulation,[status(thm)],[f154,f144]) ).
fof(f946,plain,
~ rinside(vd1126,vd1152),
inference(backward_demodulation,[status(thm)],[f154,f140]) ).
fof(f947,plain,
~ ron(vd1126,vd1152),
inference(backward_demodulation,[status(thm)],[f154,f139]) ).
fof(f955,plain,
! [X0] :
( ~ rpoint(X0)
| ~ ron(X0,vd1151)
| ~ ron(X0,vd1152)
| ~ rR(X0,vd1130,vd1125) ),
inference(forward_demodulation,[status(thm)],[f150,f941]) ).
fof(f956,plain,
! [X0] :
( ~ rpoint(X0)
| ~ ron(X0,vd1151)
| ~ ron(X0,vd1152)
| ~ rR(X0,vd1130,vd1126) ),
inference(forward_demodulation,[status(thm)],[f154,f955]) ).
fof(f1008,plain,
ron(vd1130,vd1151),
inference(forward_demodulation,[status(thm)],[f150,f938]) ).
fof(f1009,plain,
rcenter(vd1130,vd1152),
inference(forward_demodulation,[status(thm)],[f150,f939]) ).
fof(f1027,plain,
rcenter(vd1124,vd1152),
inference(backward_demodulation,[status(thm)],[f1033,f1009]) ).
fof(f1028,plain,
ron(vd1124,vd1151),
inference(backward_demodulation,[status(thm)],[f1033,f1008]) ).
fof(f1030,plain,
! [X0] :
( ~ rpoint(X0)
| ~ ron(X0,vd1151)
| ~ ron(X0,vd1152)
| ~ rR(X0,vd1124,vd1126) ),
inference(backward_demodulation,[status(thm)],[f1033,f956]) ).
fof(f1033,plain,
vd1124 = vd1130,
inference(forward_demodulation,[status(thm)],[f156,f943]) ).
fof(f1148,plain,
rinside(vd1124,vd1152),
inference(resolution,[status(thm)],[f409,f1027]) ).
fof(f1951,plain,
! [X0,X1] :
( ~ rpoint(sK3_skl(vd1126,vd1124,X0,X1))
| ~ ron(sK3_skl(vd1126,vd1124,X0,X1),vd1151)
| ~ ron(sK3_skl(vd1126,vd1124,X0,X1),vd1152)
| ~ rcircle(X1)
| ~ rline(X0)
| ~ rpoint(vd1124)
| ~ rinside(vd1124,X1)
| ~ ron(vd1124,X0)
| ~ rpoint(vd1126)
| rinside(vd1126,X1)
| ron(vd1126,X1)
| ~ ron(vd1126,X0) ),
inference(resolution,[status(thm)],[f723,f1030]) ).
fof(f1973,plain,
! [X0,X1] :
( ~ rpoint(sK3_skl(vd1126,vd1124,X0,X1))
| ~ ron(sK3_skl(vd1126,vd1124,X0,X1),vd1151)
| ~ ron(sK3_skl(vd1126,vd1124,X0,X1),vd1152)
| ~ rcircle(X1)
| ~ rline(X0)
| ~ rpoint(vd1124)
| ~ rinside(vd1124,X1)
| ~ ron(vd1124,X0)
| rinside(vd1126,X1)
| ron(vd1126,X1)
| ~ ron(vd1126,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1951,f155]) ).
fof(f2135,plain,
! [X0,X1] :
( ~ rpoint(sK3_skl(vd1126,vd1124,X0,X1))
| ~ ron(sK3_skl(vd1126,vd1124,X0,X1),vd1151)
| ~ ron(sK3_skl(vd1126,vd1124,X0,X1),vd1152)
| ~ rcircle(X1)
| ~ rline(X0)
| ~ rinside(vd1124,X1)
| ~ ron(vd1124,X0)
| rinside(vd1126,X1)
| ron(vd1126,X1)
| ~ ron(vd1126,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1973,f157]) ).
fof(f2137,plain,
! [X0] :
( ~ rcircle(vd1152)
| ~ rline(X0)
| ~ rpoint(vd1124)
| ~ rinside(vd1124,vd1152)
| ~ ron(vd1124,X0)
| ~ rpoint(vd1126)
| rinside(vd1126,vd1152)
| ron(vd1126,vd1152)
| ~ ron(vd1126,X0)
| ~ rpoint(sK3_skl(vd1126,vd1124,X0,vd1152))
| ~ ron(sK3_skl(vd1126,vd1124,X0,vd1152),vd1151)
| ~ rcircle(vd1152)
| ~ rline(X0)
| ~ rinside(vd1124,vd1152)
| ~ ron(vd1124,X0)
| rinside(vd1126,vd1152)
| ron(vd1126,vd1152)
| ~ ron(vd1126,X0) ),
inference(resolution,[status(thm)],[f2135,f724]) ).
fof(f2139,plain,
! [X0] :
( ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rpoint(sK3_skl(vd1126,vd1124,X0,vd1152))
| ~ ron(sK3_skl(vd1126,vd1124,X0,vd1152),vd1151)
| ~ rcircle(vd1152)
| ~ rline(X0)
| ~ rinside(vd1124,vd1152)
| ~ ron(vd1124,X0)
| rinside(vd1126,vd1152)
| ron(vd1126,vd1152)
| ~ ron(vd1126,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2137]) ).
fof(f2140,plain,
! [X0] :
( ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rpoint(sK3_skl(vd1126,vd1124,X0,vd1152))
| ~ ron(sK3_skl(vd1126,vd1124,X0,vd1152),vd1151)
| ~ rcircle(vd1152)
| ~ rline(X0)
| ~ rinside(vd1124,vd1152)
| ~ ron(vd1124,X0)
| rinside(vd1126,vd1152)
| ~ ron(vd1126,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2139,f947]) ).
fof(f2394,plain,
! [X0] :
( ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rpoint(sK3_skl(vd1126,vd1124,X0,vd1152))
| ~ ron(sK3_skl(vd1126,vd1124,X0,vd1152),vd1151)
| ~ rcircle(vd1152)
| ~ rline(X0)
| ~ rinside(vd1124,vd1152)
| ~ ron(vd1124,X0)
| ~ ron(vd1126,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2140,f946]) ).
fof(f2395,plain,
( ~ rcircle(vd1152)
| ~ rline(vd1151)
| ~ rpoint(vd1124)
| ~ rinside(vd1124,vd1152)
| ~ ron(vd1124,vd1151)
| ~ rpoint(vd1126)
| rinside(vd1126,vd1152)
| ron(vd1126,vd1152)
| ~ ron(vd1126,vd1151)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rpoint(sK3_skl(vd1126,vd1124,vd1151,vd1152))
| ~ rcircle(vd1152)
| ~ rline(vd1151)
| ~ rinside(vd1124,vd1152)
| ~ ron(vd1124,vd1151)
| ~ ron(vd1126,vd1151) ),
inference(resolution,[status(thm)],[f2394,f725]) ).
fof(f2396,plain,
( rinside(vd1126,vd1152)
| ron(vd1126,vd1152)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rpoint(sK3_skl(vd1126,vd1124,vd1151,vd1152))
| ~ rcircle(vd1152)
| ~ rline(vd1151)
| ~ rinside(vd1124,vd1152)
| ~ ron(vd1124,vd1151)
| ~ ron(vd1126,vd1151) ),
inference(duplicate_literals_removal,[status(thm)],[f2395]) ).
fof(f2397,plain,
( rinside(vd1126,vd1152)
| ron(vd1126,vd1152)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rpoint(sK3_skl(vd1126,vd1124,vd1151,vd1152))
| ~ rcircle(vd1152)
| ~ rline(vd1151)
| ~ rinside(vd1124,vd1152)
| ~ ron(vd1124,vd1151) ),
inference(forward_subsumption_resolution,[status(thm)],[f2396,f945]) ).
fof(f2398,plain,
( rinside(vd1126,vd1152)
| ron(vd1126,vd1152)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rpoint(sK3_skl(vd1126,vd1124,vd1151,vd1152))
| ~ rcircle(vd1152)
| ~ rline(vd1151)
| ~ rinside(vd1124,vd1152) ),
inference(forward_subsumption_resolution,[status(thm)],[f2397,f1028]) ).
fof(f2399,plain,
( ~ rcircle(vd1152)
| ~ rline(vd1151)
| ~ rpoint(vd1124)
| ~ rinside(vd1124,vd1152)
| ~ ron(vd1124,vd1151)
| ~ rpoint(vd1126)
| rinside(vd1126,vd1152)
| ron(vd1126,vd1152)
| ~ ron(vd1126,vd1151)
| rinside(vd1126,vd1152)
| ron(vd1126,vd1152)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rcircle(vd1152)
| ~ rline(vd1151)
| ~ rinside(vd1124,vd1152) ),
inference(resolution,[status(thm)],[f2398,f726]) ).
fof(f2400,plain,
( ~ ron(vd1124,vd1151)
| ~ ron(vd1126,vd1151)
| rinside(vd1126,vd1152)
| ron(vd1126,vd1152)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rcircle(vd1152)
| ~ rline(vd1151)
| ~ rinside(vd1124,vd1152) ),
inference(duplicate_literals_removal,[status(thm)],[f2399]) ).
fof(f2401,plain,
( ~ ron(vd1124,vd1151)
| ~ ron(vd1126,vd1151)
| rinside(vd1126,vd1152)
| ron(vd1126,vd1152)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rcircle(vd1152)
| ~ rline(vd1151) ),
inference(forward_subsumption_resolution,[status(thm)],[f2400,f1148]) ).
fof(f2402,plain,
( ~ ron(vd1124,vd1151)
| ~ ron(vd1126,vd1151)
| rinside(vd1126,vd1152)
| ron(vd1126,vd1152)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rcircle(vd1152) ),
inference(forward_subsumption_resolution,[status(thm)],[f2401,f172]) ).
fof(f2403,plain,
( ~ ron(vd1124,vd1151)
| rinside(vd1126,vd1152)
| ron(vd1126,vd1152)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rcircle(vd1152) ),
inference(resolution,[status(thm)],[f2402,f945]) ).
fof(f2404,plain,
( ~ ron(vd1124,vd1151)
| rinside(vd1126,vd1152)
| ron(vd1126,vd1152)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126) ),
inference(forward_subsumption_resolution,[status(thm)],[f2403,f143]) ).
fof(f2588,plain,
( ~ ron(vd1124,vd1151)
| rinside(vd1126,vd1152)
| ron(vd1126,vd1152)
| ~ rpoint(vd1124) ),
inference(forward_subsumption_resolution,[status(thm)],[f2404,f155]) ).
fof(f2589,plain,
( rinside(vd1126,vd1152)
| ron(vd1126,vd1152)
| ~ rpoint(vd1124) ),
inference(resolution,[status(thm)],[f2588,f1028]) ).
fof(f2590,plain,
( rinside(vd1126,vd1152)
| ron(vd1126,vd1152) ),
inference(forward_subsumption_resolution,[status(thm)],[f2589,f157]) ).
fof(f2592,plain,
rinside(vd1126,vd1152),
inference(forward_subsumption_resolution,[status(thm)],[f2590,f947]) ).
fof(f2593,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f946,f2592]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GEO286+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n004.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Sun Sep 20 15:07:35 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.54 % Drodi V4.1.1
% 38.78/5.51 % Refutation found
% 38.78/5.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 38.78/5.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 19.65/5.59 % Elapsed time: 5.117569 seconds
% 19.65/5.59 % CPU time: 39.529956 seconds
% 19.65/5.59 % Total memory used: 215.210 MB
% 19.65/5.59 % Net memory used: 201.785 MB
%------------------------------------------------------------------------------