%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO283+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 : 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:24:49 PM UTC 2026
% Result : Theorem 9.23s 1.58s
% Output : CNFRefutation 9.23s
% 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,
? [Vd1147] :
( rpoint(Vd1147)
& ron(Vd1147,vd1145)
& ron(Vd1147,vd1146)
& rR(Vd1147,vd1123,vd1125) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ? [Vd1147] :
( rpoint(Vd1147)
& ron(Vd1147,vd1145)
& ron(Vd1147,vd1146)
& rR(Vd1147,vd1123,vd1125) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
~ ron(vd1125,vd1146),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
~ rinside(vd1125,vd1146),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
( ron(vd1123,vd1145)
& ron(vd1125,vd1145)
& rcircle(vd1146)
& rcenter(vd1123,vd1146)
& ron(vd1129,vd1146) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
vd1123 = vd1127,
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(f10,axiom,
rline(vd1145),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,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(f38,axiom,
! [Vd334,Vd335] :
( rcenter(Vd334,Vd335)
=> rinside(Vd334,Vd335) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f128,plain,
! [Vd1147] :
( ~ rpoint(Vd1147)
| ~ ron(Vd1147,vd1145)
| ~ ron(Vd1147,vd1146)
| ~ rR(Vd1147,vd1123,vd1125) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f129,plain,
! [X0] :
( ~ rpoint(X0)
| ~ ron(X0,vd1145)
| ~ ron(X0,vd1146)
| ~ rR(X0,vd1123,vd1125) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
~ ron(vd1125,vd1146),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f131,plain,
~ rinside(vd1125,vd1146),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f133,plain,
rcenter(vd1123,vd1146),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f134,plain,
rcircle(vd1146),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f135,plain,
ron(vd1125,vd1145),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f136,plain,
ron(vd1123,vd1145),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f137,plain,
vd1123 = vd1127,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f143,plain,
vd1127 = vd1128,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f145,plain,
vd1125 = vd1126,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f146,plain,
rpoint(vd1126),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f147,plain,
vd1123 = vd1124,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f148,plain,
rpoint(vd1124),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f156,plain,
rline(vd1145),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f179,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)],[f15]) ).
fof(f180,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)],[f179]) ).
fof(f181,plain,
! [Vd253,Vd255,Vd257,Vd259] :
( ( rpoint(sK2_skl(Vd259,Vd257,Vd255,Vd253))
& ron(sK2_skl(Vd259,Vd257,Vd255,Vd253),Vd255)
& ron(sK2_skl(Vd259,Vd257,Vd255,Vd253),Vd253)
& rR(sK2_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,[sK2_skl]),skolemize(Vd261,sK2_skl(Vd259,Vd257,Vd255,Vd253))],[f180]) ).
fof(f182,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( rR(sK2_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)],[f181]) ).
fof(f183,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ron(sK2_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)],[f181]) ).
fof(f184,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ron(sK2_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)],[f181]) ).
fof(f185,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( rpoint(sK2_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)],[f181]) ).
fof(f259,plain,
! [Vd334,Vd335] :
( rinside(Vd334,Vd335)
| ~ rcenter(Vd334,Vd335) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f260,plain,
! [X0,X1] :
( rinside(X0,X1)
| ~ rcenter(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f259]) ).
fof(f688,plain,
! [X0,X1,X2,X3] :
( rR(sK2_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)],[f182]) ).
fof(f689,plain,
! [X0,X1,X2,X3] :
( ron(sK2_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)],[f183]) ).
fof(f690,plain,
! [X0,X1,X2,X3] :
( ron(sK2_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)],[f184]) ).
fof(f691,plain,
! [X0,X1,X2,X3] :
( rpoint(sK2_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)],[f185]) ).
fof(f906,plain,
ron(vd1127,vd1145),
inference(backward_demodulation,[status(thm)],[f137,f136]) ).
fof(f907,plain,
rcenter(vd1127,vd1146),
inference(backward_demodulation,[status(thm)],[f137,f133]) ).
fof(f909,plain,
! [X0] :
( ~ rpoint(X0)
| ~ ron(X0,vd1145)
| ~ ron(X0,vd1146)
| ~ rR(X0,vd1127,vd1125) ),
inference(backward_demodulation,[status(thm)],[f137,f129]) ).
fof(f912,plain,
vd1123 = vd1128,
inference(backward_demodulation,[status(thm)],[f143,f137]) ).
fof(f913,plain,
ron(vd1126,vd1145),
inference(backward_demodulation,[status(thm)],[f145,f135]) ).
fof(f914,plain,
~ rinside(vd1126,vd1146),
inference(backward_demodulation,[status(thm)],[f145,f131]) ).
fof(f915,plain,
~ ron(vd1126,vd1146),
inference(backward_demodulation,[status(thm)],[f145,f130]) ).
fof(f918,plain,
! [X0] :
( ~ rpoint(X0)
| ~ ron(X0,vd1145)
| ~ ron(X0,vd1146)
| ~ rR(X0,vd1128,vd1125) ),
inference(forward_demodulation,[status(thm)],[f143,f909]) ).
fof(f919,plain,
! [X0] :
( ~ rpoint(X0)
| ~ ron(X0,vd1145)
| ~ ron(X0,vd1146)
| ~ rR(X0,vd1128,vd1126) ),
inference(forward_demodulation,[status(thm)],[f145,f918]) ).
fof(f971,plain,
ron(vd1128,vd1145),
inference(forward_demodulation,[status(thm)],[f143,f906]) ).
fof(f974,plain,
rcenter(vd1128,vd1146),
inference(forward_demodulation,[status(thm)],[f143,f907]) ).
fof(f992,plain,
rcenter(vd1124,vd1146),
inference(backward_demodulation,[status(thm)],[f998,f974]) ).
fof(f993,plain,
ron(vd1124,vd1145),
inference(backward_demodulation,[status(thm)],[f998,f971]) ).
fof(f995,plain,
! [X0] :
( ~ rpoint(X0)
| ~ ron(X0,vd1145)
| ~ ron(X0,vd1146)
| ~ rR(X0,vd1124,vd1126) ),
inference(backward_demodulation,[status(thm)],[f998,f919]) ).
fof(f998,plain,
vd1124 = vd1128,
inference(forward_demodulation,[status(thm)],[f147,f912]) ).
fof(f1081,plain,
rinside(vd1124,vd1146),
inference(resolution,[status(thm)],[f260,f992]) ).
fof(f1734,plain,
! [X0,X1] :
( ~ rpoint(sK2_skl(vd1126,vd1124,X0,X1))
| ~ ron(sK2_skl(vd1126,vd1124,X0,X1),vd1145)
| ~ ron(sK2_skl(vd1126,vd1124,X0,X1),vd1146)
| ~ 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)],[f688,f995]) ).
fof(f1756,plain,
! [X0,X1] :
( ~ rpoint(sK2_skl(vd1126,vd1124,X0,X1))
| ~ ron(sK2_skl(vd1126,vd1124,X0,X1),vd1145)
| ~ ron(sK2_skl(vd1126,vd1124,X0,X1),vd1146)
| ~ 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)],[f1734,f146]) ).
fof(f1960,plain,
! [X0,X1] :
( ~ rpoint(sK2_skl(vd1126,vd1124,X0,X1))
| ~ ron(sK2_skl(vd1126,vd1124,X0,X1),vd1145)
| ~ ron(sK2_skl(vd1126,vd1124,X0,X1),vd1146)
| ~ 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)],[f1756,f148]) ).
fof(f1962,plain,
! [X0] :
( ~ rcircle(vd1146)
| ~ rline(X0)
| ~ rpoint(vd1124)
| ~ rinside(vd1124,vd1146)
| ~ ron(vd1124,X0)
| ~ rpoint(vd1126)
| rinside(vd1126,vd1146)
| ron(vd1126,vd1146)
| ~ ron(vd1126,X0)
| ~ rpoint(sK2_skl(vd1126,vd1124,X0,vd1146))
| ~ ron(sK2_skl(vd1126,vd1124,X0,vd1146),vd1145)
| ~ rcircle(vd1146)
| ~ rline(X0)
| ~ rinside(vd1124,vd1146)
| ~ ron(vd1124,X0)
| rinside(vd1126,vd1146)
| ron(vd1126,vd1146)
| ~ ron(vd1126,X0) ),
inference(resolution,[status(thm)],[f1960,f689]) ).
fof(f1964,plain,
! [X0] :
( ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rpoint(sK2_skl(vd1126,vd1124,X0,vd1146))
| ~ ron(sK2_skl(vd1126,vd1124,X0,vd1146),vd1145)
| ~ rcircle(vd1146)
| ~ rline(X0)
| ~ rinside(vd1124,vd1146)
| ~ ron(vd1124,X0)
| rinside(vd1126,vd1146)
| ron(vd1126,vd1146)
| ~ ron(vd1126,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1962]) ).
fof(f1965,plain,
! [X0] :
( ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rpoint(sK2_skl(vd1126,vd1124,X0,vd1146))
| ~ ron(sK2_skl(vd1126,vd1124,X0,vd1146),vd1145)
| ~ rcircle(vd1146)
| ~ rline(X0)
| ~ rinside(vd1124,vd1146)
| ~ ron(vd1124,X0)
| rinside(vd1126,vd1146)
| ~ ron(vd1126,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1964,f915]) ).
fof(f2330,plain,
! [X0] :
( ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rpoint(sK2_skl(vd1126,vd1124,X0,vd1146))
| ~ ron(sK2_skl(vd1126,vd1124,X0,vd1146),vd1145)
| ~ rcircle(vd1146)
| ~ rline(X0)
| ~ rinside(vd1124,vd1146)
| ~ ron(vd1124,X0)
| ~ ron(vd1126,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1965,f914]) ).
fof(f2331,plain,
( ~ rcircle(vd1146)
| ~ rline(vd1145)
| ~ rpoint(vd1124)
| ~ rinside(vd1124,vd1146)
| ~ ron(vd1124,vd1145)
| ~ rpoint(vd1126)
| rinside(vd1126,vd1146)
| ron(vd1126,vd1146)
| ~ ron(vd1126,vd1145)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rpoint(sK2_skl(vd1126,vd1124,vd1145,vd1146))
| ~ rcircle(vd1146)
| ~ rline(vd1145)
| ~ rinside(vd1124,vd1146)
| ~ ron(vd1124,vd1145)
| ~ ron(vd1126,vd1145) ),
inference(resolution,[status(thm)],[f2330,f690]) ).
fof(f2332,plain,
( rinside(vd1126,vd1146)
| ron(vd1126,vd1146)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rpoint(sK2_skl(vd1126,vd1124,vd1145,vd1146))
| ~ rcircle(vd1146)
| ~ rline(vd1145)
| ~ rinside(vd1124,vd1146)
| ~ ron(vd1124,vd1145)
| ~ ron(vd1126,vd1145) ),
inference(duplicate_literals_removal,[status(thm)],[f2331]) ).
fof(f2333,plain,
( rinside(vd1126,vd1146)
| ron(vd1126,vd1146)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rpoint(sK2_skl(vd1126,vd1124,vd1145,vd1146))
| ~ rcircle(vd1146)
| ~ rline(vd1145)
| ~ rinside(vd1124,vd1146)
| ~ ron(vd1124,vd1145) ),
inference(forward_subsumption_resolution,[status(thm)],[f2332,f913]) ).
fof(f2334,plain,
( rinside(vd1126,vd1146)
| ron(vd1126,vd1146)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rpoint(sK2_skl(vd1126,vd1124,vd1145,vd1146))
| ~ rcircle(vd1146)
| ~ rline(vd1145)
| ~ rinside(vd1124,vd1146) ),
inference(forward_subsumption_resolution,[status(thm)],[f2333,f993]) ).
fof(f2335,plain,
( ~ rcircle(vd1146)
| ~ rline(vd1145)
| ~ rpoint(vd1124)
| ~ rinside(vd1124,vd1146)
| ~ ron(vd1124,vd1145)
| ~ rpoint(vd1126)
| rinside(vd1126,vd1146)
| ron(vd1126,vd1146)
| ~ ron(vd1126,vd1145)
| rinside(vd1126,vd1146)
| ron(vd1126,vd1146)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rcircle(vd1146)
| ~ rline(vd1145)
| ~ rinside(vd1124,vd1146) ),
inference(resolution,[status(thm)],[f2334,f691]) ).
fof(f2336,plain,
( ~ ron(vd1124,vd1145)
| ~ ron(vd1126,vd1145)
| rinside(vd1126,vd1146)
| ron(vd1126,vd1146)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rcircle(vd1146)
| ~ rline(vd1145)
| ~ rinside(vd1124,vd1146) ),
inference(duplicate_literals_removal,[status(thm)],[f2335]) ).
fof(f2337,plain,
( ~ ron(vd1124,vd1145)
| ~ ron(vd1126,vd1145)
| rinside(vd1126,vd1146)
| ron(vd1126,vd1146)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rcircle(vd1146)
| ~ rline(vd1145) ),
inference(forward_subsumption_resolution,[status(thm)],[f2336,f1081]) ).
fof(f2509,plain,
( ~ ron(vd1124,vd1145)
| ~ ron(vd1126,vd1145)
| rinside(vd1126,vd1146)
| ron(vd1126,vd1146)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rcircle(vd1146) ),
inference(forward_subsumption_resolution,[status(thm)],[f2337,f156]) ).
fof(f2510,plain,
( ~ ron(vd1124,vd1145)
| rinside(vd1126,vd1146)
| ron(vd1126,vd1146)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126)
| ~ rcircle(vd1146) ),
inference(resolution,[status(thm)],[f2509,f913]) ).
fof(f2511,plain,
( ~ ron(vd1124,vd1145)
| rinside(vd1126,vd1146)
| ron(vd1126,vd1146)
| ~ rpoint(vd1124)
| ~ rpoint(vd1126) ),
inference(forward_subsumption_resolution,[status(thm)],[f2510,f134]) ).
fof(f2512,plain,
( ~ ron(vd1124,vd1145)
| rinside(vd1126,vd1146)
| ron(vd1126,vd1146)
| ~ rpoint(vd1124) ),
inference(forward_subsumption_resolution,[status(thm)],[f2511,f146]) ).
fof(f2513,plain,
( rinside(vd1126,vd1146)
| ron(vd1126,vd1146)
| ~ rpoint(vd1124) ),
inference(resolution,[status(thm)],[f2512,f993]) ).
fof(f2514,plain,
( rinside(vd1126,vd1146)
| ron(vd1126,vd1146) ),
inference(forward_subsumption_resolution,[status(thm)],[f2513,f148]) ).
fof(f2516,plain,
rinside(vd1126,vd1146),
inference(forward_subsumption_resolution,[status(thm)],[f2514,f915]) ).
fof(f2517,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f914,f2516]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GEO283+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 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:05:37 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.31 % Drodi V4.1.1
% 9.23/1.58 % Refutation found
% 9.23/1.58 % SZS status Theorem for theBenchmark: Theorem is valid
% 9.23/1.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.76/1.60 % Elapsed time: 1.293509 seconds
% 0.76/1.60 % CPU time: 10.031526 seconds
% 0.76/1.60 % Total memory used: 187.556 MB
% 0.76/1.60 % Net memory used: 178.343 MB
%------------------------------------------------------------------------------