%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO281+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 0.10s 0.40s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 8
% Syntax : Number of formulae : 83 ( 26 unt; 0 def)
% Number of atoms : 417 ( 40 equ)
% Maximal formula atoms : 17 ( 5 avg)
% Number of connectives : 582 ( 248 ~; 288 |; 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 : 13 ( 13 usr; 11 con; 0-4 aty)
% Number of variables : 119 ( 114 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
? [Vd1140] :
( rpoint(Vd1140)
& ron(Vd1140,vd1138)
& ron(Vd1140,vd1139)
& rR(Vd1140,vd1123,vd1125) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ? [Vd1140] :
( rpoint(Vd1140)
& ron(Vd1140,vd1138)
& ron(Vd1140,vd1139)
& rR(Vd1140,vd1123,vd1125) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
~ ron(vd1125,vd1139),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
~ rinside(vd1125,vd1139),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
( ron(vd1123,vd1138)
& ron(vd1125,vd1138)
& rcircle(vd1139)
& rcenter(vd1123,vd1139)
& ron(vd1136,vd1139) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,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(vd1138),
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(f69,axiom,
! [Vd334,Vd335] :
( rcenter(Vd334,Vd335)
=> rinside(Vd334,Vd335) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f119,plain,
! [Vd1140] :
( ~ rpoint(Vd1140)
| ~ ron(Vd1140,vd1138)
| ~ ron(Vd1140,vd1139)
| ~ rR(Vd1140,vd1123,vd1125) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f120,plain,
! [X0] :
( ~ rpoint(X0)
| ~ ron(X0,vd1138)
| ~ ron(X0,vd1139)
| ~ rR(X0,vd1123,vd1125) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f121,plain,
~ ron(vd1125,vd1139),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f122,plain,
~ rinside(vd1125,vd1139),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f124,plain,
rcenter(vd1123,vd1139),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f125,plain,
rcircle(vd1139),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f126,plain,
ron(vd1125,vd1138),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f127,plain,
ron(vd1123,vd1138),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f137,plain,
vd1125 = vd1126,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f138,plain,
rpoint(vd1126),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f139,plain,
vd1123 = vd1124,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f140,plain,
rpoint(vd1124),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f153,plain,
rline(vd1138),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f161,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(f162,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)],[f161]) ).
fof(f163,plain,
! [Vd253,Vd255,Vd257,Vd259] :
( ( rpoint(sK1_skl(Vd259,Vd257,Vd255,Vd253))
& ron(sK1_skl(Vd259,Vd257,Vd255,Vd253),Vd255)
& ron(sK1_skl(Vd259,Vd257,Vd255,Vd253),Vd253)
& rR(sK1_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,[sK1_skl]),skolemize(Vd261,sK1_skl(Vd259,Vd257,Vd255,Vd253))],[f162]) ).
fof(f164,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( rR(sK1_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)],[f163]) ).
fof(f165,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ron(sK1_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)],[f163]) ).
fof(f166,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ron(sK1_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)],[f163]) ).
fof(f167,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( rpoint(sK1_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)],[f163]) ).
fof(f350,plain,
! [Vd334,Vd335] :
( rinside(Vd334,Vd335)
| ~ rcenter(Vd334,Vd335) ),
inference(pre_NNF_transformation,[status(thm)],[f69]) ).
fof(f351,plain,
! [X0,X1] :
( rinside(X0,X1)
| ~ rcenter(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f647,plain,
! [X0,X1,X2,X3] :
( rR(sK1_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)],[f164]) ).
fof(f648,plain,
! [X0,X1,X2,X3] :
( ron(sK1_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)],[f165]) ).
fof(f649,plain,
! [X0,X1,X2,X3] :
( ron(sK1_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)],[f166]) ).
fof(f650,plain,
! [X0,X1,X2,X3] :
( rpoint(sK1_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)],[f167]) ).
fof(f875,plain,
ron(vd1126,vd1138),
inference(backward_demodulation,[status(thm)],[f137,f126]) ).
fof(f876,plain,
~ rinside(vd1126,vd1139),
inference(backward_demodulation,[status(thm)],[f137,f122]) ).
fof(f878,plain,
~ ron(vd1126,vd1139),
inference(backward_demodulation,[status(thm)],[f137,f121]) ).
fof(f879,plain,
! [X0] :
( ~ rpoint(X0)
| ~ ron(X0,vd1138)
| ~ ron(X0,vd1139)
| ~ rR(X0,vd1123,vd1126) ),
inference(backward_demodulation,[status(thm)],[f137,f120]) ).
fof(f881,plain,
ron(vd1124,vd1138),
inference(backward_demodulation,[status(thm)],[f139,f127]) ).
fof(f882,plain,
rcenter(vd1124,vd1139),
inference(backward_demodulation,[status(thm)],[f139,f124]) ).
fof(f894,plain,
! [X0] :
( ~ rpoint(X0)
| ~ ron(X0,vd1138)
| ~ ron(X0,vd1139)
| ~ rR(X0,vd1124,vd1126) ),
inference(forward_demodulation,[status(thm)],[f139,f879]) ).
fof(f920,plain,
! [X0,X1,X2] :
( rR(sK1_skl(X0,X2,vd1138,X1),X2,X0)
| ~ rcircle(X1)
| ~ rpoint(X2)
| ~ rinside(X2,X1)
| ~ ron(X2,vd1138)
| ~ rpoint(X0)
| rinside(X0,X1)
| ron(X0,X1)
| ~ ron(X0,vd1138) ),
inference(resolution,[status(thm)],[f647,f153]) ).
fof(f922,plain,
! [X0,X1] :
( rR(sK1_skl(X0,X1,vd1138,vd1139),X1,X0)
| ~ rpoint(X1)
| ~ rinside(X1,vd1139)
| ~ ron(X1,vd1138)
| ~ rpoint(X0)
| rinside(X0,vd1139)
| ron(X0,vd1139)
| ~ ron(X0,vd1138) ),
inference(resolution,[status(thm)],[f920,f125]) ).
fof(f949,plain,
rinside(vd1124,vd1139),
inference(resolution,[status(thm)],[f351,f882]) ).
fof(f950,plain,
! [X0] :
( rR(sK1_skl(X0,vd1124,vd1138,vd1139),vd1124,X0)
| ~ rpoint(vd1124)
| ~ ron(vd1124,vd1138)
| ~ rpoint(X0)
| rinside(X0,vd1139)
| ron(X0,vd1139)
| ~ ron(X0,vd1138) ),
inference(resolution,[status(thm)],[f949,f922]) ).
fof(f952,plain,
! [X0] :
( rR(sK1_skl(X0,vd1124,vd1138,vd1139),vd1124,X0)
| ~ rpoint(vd1124)
| ~ rpoint(X0)
| rinside(X0,vd1139)
| ron(X0,vd1139)
| ~ ron(X0,vd1138) ),
inference(forward_subsumption_resolution,[status(thm)],[f950,f881]) ).
fof(f954,plain,
! [X0,X1,X2] :
( ron(sK1_skl(X0,X2,vd1138,X1),X1)
| ~ rcircle(X1)
| ~ rpoint(X2)
| ~ rinside(X2,X1)
| ~ ron(X2,vd1138)
| ~ rpoint(X0)
| rinside(X0,X1)
| ron(X0,X1)
| ~ ron(X0,vd1138) ),
inference(resolution,[status(thm)],[f648,f153]) ).
fof(f955,plain,
! [X0,X1,X2] :
( ron(sK1_skl(X0,X2,vd1138,X1),vd1138)
| ~ rcircle(X1)
| ~ rpoint(X2)
| ~ rinside(X2,X1)
| ~ ron(X2,vd1138)
| ~ rpoint(X0)
| rinside(X0,X1)
| ron(X0,X1)
| ~ ron(X0,vd1138) ),
inference(resolution,[status(thm)],[f649,f153]) ).
fof(f960,plain,
! [X0,X1] :
( ron(sK1_skl(X0,X1,vd1138,vd1139),vd1139)
| ~ rpoint(X1)
| ~ rinside(X1,vd1139)
| ~ ron(X1,vd1138)
| ~ rpoint(X0)
| rinside(X0,vd1139)
| ron(X0,vd1139)
| ~ ron(X0,vd1138) ),
inference(resolution,[status(thm)],[f954,f125]) ).
fof(f962,plain,
! [X0] :
( rR(sK1_skl(X0,vd1124,vd1138,vd1139),vd1124,X0)
| ~ rpoint(X0)
| rinside(X0,vd1139)
| ron(X0,vd1139)
| ~ ron(X0,vd1138) ),
inference(forward_subsumption_resolution,[status(thm)],[f952,f140]) ).
fof(f964,plain,
( rR(sK1_skl(vd1126,vd1124,vd1138,vd1139),vd1124,vd1126)
| ~ rpoint(vd1126)
| rinside(vd1126,vd1139)
| ron(vd1126,vd1139) ),
inference(resolution,[status(thm)],[f962,f875]) ).
fof(f965,plain,
( rR(sK1_skl(vd1126,vd1124,vd1138,vd1139),vd1124,vd1126)
| ~ rpoint(vd1126)
| rinside(vd1126,vd1139) ),
inference(forward_subsumption_resolution,[status(thm)],[f964,f878]) ).
fof(f966,plain,
( rR(sK1_skl(vd1126,vd1124,vd1138,vd1139),vd1124,vd1126)
| ~ rpoint(vd1126) ),
inference(forward_subsumption_resolution,[status(thm)],[f965,f876]) ).
fof(f967,plain,
rR(sK1_skl(vd1126,vd1124,vd1138,vd1139),vd1124,vd1126),
inference(resolution,[status(thm)],[f966,f138]) ).
fof(f984,plain,
! [X0,X1] :
( ron(sK1_skl(X0,X1,vd1138,vd1139),vd1138)
| ~ rpoint(X1)
| ~ rinside(X1,vd1139)
| ~ ron(X1,vd1138)
| ~ rpoint(X0)
| rinside(X0,vd1139)
| ron(X0,vd1139)
| ~ ron(X0,vd1138) ),
inference(resolution,[status(thm)],[f955,f125]) ).
fof(f1011,plain,
! [X0] :
( ron(sK1_skl(X0,vd1124,vd1138,vd1139),vd1139)
| ~ rpoint(vd1124)
| ~ rinside(vd1124,vd1139)
| ~ rpoint(X0)
| rinside(X0,vd1139)
| ron(X0,vd1139)
| ~ ron(X0,vd1138) ),
inference(resolution,[status(thm)],[f960,f881]) ).
fof(f1013,plain,
! [X0] :
( ron(sK1_skl(X0,vd1124,vd1138,vd1139),vd1139)
| ~ rpoint(vd1124)
| ~ rpoint(X0)
| rinside(X0,vd1139)
| ron(X0,vd1139)
| ~ ron(X0,vd1138) ),
inference(forward_subsumption_resolution,[status(thm)],[f1011,f949]) ).
fof(f1014,plain,
! [X0] :
( ron(sK1_skl(X0,vd1124,vd1138,vd1139),vd1139)
| ~ rpoint(X0)
| rinside(X0,vd1139)
| ron(X0,vd1139)
| ~ ron(X0,vd1138) ),
inference(forward_subsumption_resolution,[status(thm)],[f1013,f140]) ).
fof(f1016,plain,
( ron(sK1_skl(vd1126,vd1124,vd1138,vd1139),vd1139)
| ~ rpoint(vd1126)
| rinside(vd1126,vd1139)
| ron(vd1126,vd1139) ),
inference(resolution,[status(thm)],[f1014,f875]) ).
fof(f1017,plain,
( ron(sK1_skl(vd1126,vd1124,vd1138,vd1139),vd1139)
| ~ rpoint(vd1126)
| rinside(vd1126,vd1139) ),
inference(forward_subsumption_resolution,[status(thm)],[f1016,f878]) ).
fof(f1018,plain,
( ron(sK1_skl(vd1126,vd1124,vd1138,vd1139),vd1139)
| ~ rpoint(vd1126) ),
inference(forward_subsumption_resolution,[status(thm)],[f1017,f876]) ).
fof(f1019,plain,
ron(sK1_skl(vd1126,vd1124,vd1138,vd1139),vd1139),
inference(resolution,[status(thm)],[f1018,f138]) ).
fof(f1026,plain,
! [X0] :
( ron(sK1_skl(X0,vd1124,vd1138,vd1139),vd1138)
| ~ rpoint(vd1124)
| ~ rinside(vd1124,vd1139)
| ~ rpoint(X0)
| rinside(X0,vd1139)
| ron(X0,vd1139)
| ~ ron(X0,vd1138) ),
inference(resolution,[status(thm)],[f984,f881]) ).
fof(f1028,plain,
! [X0] :
( ron(sK1_skl(X0,vd1124,vd1138,vd1139),vd1138)
| ~ rpoint(vd1124)
| ~ rpoint(X0)
| rinside(X0,vd1139)
| ron(X0,vd1139)
| ~ ron(X0,vd1138) ),
inference(forward_subsumption_resolution,[status(thm)],[f1026,f949]) ).
fof(f1037,plain,
! [X0] :
( ron(sK1_skl(X0,vd1124,vd1138,vd1139),vd1138)
| ~ rpoint(X0)
| rinside(X0,vd1139)
| ron(X0,vd1139)
| ~ ron(X0,vd1138) ),
inference(forward_subsumption_resolution,[status(thm)],[f1028,f140]) ).
fof(f1039,plain,
( ron(sK1_skl(vd1126,vd1124,vd1138,vd1139),vd1138)
| ~ rpoint(vd1126)
| rinside(vd1126,vd1139)
| ron(vd1126,vd1139) ),
inference(resolution,[status(thm)],[f1037,f875]) ).
fof(f1040,plain,
( ron(sK1_skl(vd1126,vd1124,vd1138,vd1139),vd1138)
| ~ rpoint(vd1126)
| rinside(vd1126,vd1139) ),
inference(forward_subsumption_resolution,[status(thm)],[f1039,f878]) ).
fof(f1041,plain,
( ron(sK1_skl(vd1126,vd1124,vd1138,vd1139),vd1138)
| ~ rpoint(vd1126) ),
inference(forward_subsumption_resolution,[status(thm)],[f1040,f876]) ).
fof(f1042,plain,
ron(sK1_skl(vd1126,vd1124,vd1138,vd1139),vd1138),
inference(resolution,[status(thm)],[f1041,f138]) ).
fof(f1058,plain,
( ~ rpoint(sK1_skl(vd1126,vd1124,vd1138,vd1139))
| ~ ron(sK1_skl(vd1126,vd1124,vd1138,vd1139),vd1139)
| ~ rR(sK1_skl(vd1126,vd1124,vd1138,vd1139),vd1124,vd1126) ),
inference(resolution,[status(thm)],[f1042,f894]) ).
fof(f1059,plain,
( ~ rpoint(sK1_skl(vd1126,vd1124,vd1138,vd1139))
| ~ ron(sK1_skl(vd1126,vd1124,vd1138,vd1139),vd1139) ),
inference(forward_subsumption_resolution,[status(thm)],[f1058,f967]) ).
fof(f1060,plain,
~ rpoint(sK1_skl(vd1126,vd1124,vd1138,vd1139)),
inference(forward_subsumption_resolution,[status(thm)],[f1059,f1019]) ).
fof(f1061,plain,
( ~ rcircle(vd1139)
| ~ rline(vd1138)
| ~ rpoint(vd1124)
| ~ rinside(vd1124,vd1139)
| ~ ron(vd1124,vd1138)
| ~ rpoint(vd1126)
| rinside(vd1126,vd1139)
| ron(vd1126,vd1139)
| ~ ron(vd1126,vd1138) ),
inference(resolution,[status(thm)],[f1060,f650]) ).
fof(f1062,plain,
( ~ rcircle(vd1139)
| ~ rline(vd1138)
| ~ rpoint(vd1124)
| ~ rinside(vd1124,vd1139)
| ~ ron(vd1124,vd1138)
| ~ rpoint(vd1126)
| rinside(vd1126,vd1139)
| ron(vd1126,vd1139) ),
inference(forward_subsumption_resolution,[status(thm)],[f1061,f875]) ).
fof(f1074,plain,
( ~ rcircle(vd1139)
| ~ rline(vd1138)
| ~ rpoint(vd1124)
| ~ rinside(vd1124,vd1139)
| ~ ron(vd1124,vd1138)
| ~ rpoint(vd1126)
| rinside(vd1126,vd1139) ),
inference(forward_subsumption_resolution,[status(thm)],[f1062,f878]) ).
fof(f1075,plain,
( ~ rcircle(vd1139)
| ~ rline(vd1138)
| ~ rinside(vd1124,vd1139)
| ~ ron(vd1124,vd1138)
| ~ rpoint(vd1126)
| rinside(vd1126,vd1139) ),
inference(resolution,[status(thm)],[f1074,f140]) ).
fof(f1076,plain,
( ~ rcircle(vd1139)
| ~ rline(vd1138)
| ~ rinside(vd1124,vd1139)
| ~ ron(vd1124,vd1138)
| ~ rpoint(vd1126) ),
inference(forward_subsumption_resolution,[status(thm)],[f1075,f876]) ).
fof(f1077,plain,
( ~ rcircle(vd1139)
| ~ rline(vd1138)
| ~ rinside(vd1124,vd1139)
| ~ ron(vd1124,vd1138) ),
inference(forward_subsumption_resolution,[status(thm)],[f1076,f138]) ).
fof(f1078,plain,
( ~ rcircle(vd1139)
| ~ rline(vd1138)
| ~ rinside(vd1124,vd1139) ),
inference(resolution,[status(thm)],[f1077,f881]) ).
fof(f1079,plain,
( ~ rcircle(vd1139)
| ~ rline(vd1138) ),
inference(forward_subsumption_resolution,[status(thm)],[f1078,f949]) ).
fof(f1081,plain,
~ rcircle(vd1139),
inference(forward_subsumption_resolution,[status(thm)],[f1079,f153]) ).
fof(f1082,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f125,f1081]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GEO281+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.02/0.29 % Computer : n012.cluster.edu
% 0.02/0.29 % Model : x86_64 x86_64
% 0.02/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.29 % Memory : 8046.5625MB
% 0.02/0.29 % OS : Linux 6.8.0-71-generic
% 0.02/0.30 % CPULimit : 300
% 0.02/0.30 % WCLimit : 300
% 0.02/0.30 % DateTime : Sun Sep 20 15:06:52 UTC 2026
% 0.02/0.30 % CPUTime :
% 0.02/0.32 % Drodi V4.1.1
% 0.10/0.40 % Refutation found
% 0.10/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.10/0.42 % Elapsed time: 0.119870 seconds
% 0.10/0.42 % CPU time: 0.669738 seconds
% 0.10/0.42 % Total memory used: 124.888 MB
% 0.10/0.42 % Net memory used: 124.070 MB
%------------------------------------------------------------------------------