%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO283+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:26:19 PM UTC 2026
% Result : Theorem 61.56s 8.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GEO283+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.48 % Computer : n011.cluster.edu
% 0.17/0.48 % Model : x86_64 x86_64
% 0.17/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.48 % Memory : 8046.5625MB
% 0.17/0.48 % OS : Linux 6.8.0-71-generic
% 0.17/0.48 % CPULimit : 300
% 0.17/0.48 % WCLimit : 300
% 0.17/0.48 % DateTime : Sun Sep 20 15:06:54 UTC 2026
% 0.17/0.48 % CPUTime :
% 0.22/0.52 % Drodi V4.1.1
% 61.56/8.83 % Refutation found
% 61.56/8.83 % SZS status Theorem for theBenchmark: Theorem is valid
% 61.56/8.83 % SZS output start CNFRefutation for theBenchmark
% 61.56/8.83 fof(f1,conjecture,(
% 61.56/8.83 (? [Vd1147] :( rR(Vd1147,vd1123,vd1125)& ron(Vd1147,vd1146)& ron(Vd1147,vd1145)& rpoint(Vd1147) ) )),
% 61.56/8.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 61.56/8.83 fof(f2,negated_conjecture,(
% 61.56/8.83 ~((? [Vd1147] :( rR(Vd1147,vd1123,vd1125)& ron(Vd1147,vd1146)& ron(Vd1147,vd1145)& rpoint(Vd1147) ) ))),
% 61.56/8.83 inference(negated_conjecture,[status(cth)],[f1])).
% 61.56/8.83 fof(f3,axiom,(
% 61.56/8.83 ~ ron(vd1125,vd1146) ),
% 61.56/8.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 61.56/8.83 fof(f4,axiom,(
% 61.56/8.83 ~ rinside(vd1125,vd1146) ),
% 61.56/8.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 61.56/8.83 fof(f5,axiom,(
% 61.56/8.83 ( ron(vd1129,vd1146)& rcenter(vd1123,vd1146)& rcircle(vd1146)& ron(vd1125,vd1145)& ron(vd1123,vd1145) ) ),
% 61.56/8.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 61.56/8.83 fof(f6,axiom,(
% 61.56/8.83 vd1123 = vd1127 ),
% 61.56/8.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 61.56/8.83 fof(f7,axiom,(
% 61.56/8.83 ( rless(vf(vd1127,vd1129),vf(vd1123,vd1125))& vd1127 != vd1129& vd1123 != vd1125& vd1129 = vd1130& rpoint(vd1130)& vd1127 = vd1128& rpoint(vd1128)& vd1125 = vd1126& rpoint(vd1126)& vd1123 = vd1124& rpoint(vd1124) ) ),
% 61.56/8.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 61.56/8.83 fof(f10,axiom,(
% 61.56/8.83 rline(vd1145) ),
% 61.56/8.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 61.56/8.83 fof(f15,axiom,(
% 61.56/8.83 (! [Vd253,Vd254,Vd255,Vd256,Vd257,Vd258,Vd259,Vd260] :( ( ron(Vd259,Vd255)& ~ ron(Vd259,Vd253)& ~ rinside(Vd259,Vd253)& Vd259 = Vd260& rpoint(Vd260)& ron(Vd257,Vd255)& rinside(Vd257,Vd253)& Vd257 = Vd258& rpoint(Vd258)& Vd255 = Vd256& rline(Vd256)& Vd253 = Vd254& rcircle(Vd254) )=> (? [Vd261] :( rR(Vd261,Vd257,Vd259)& ron(Vd261,Vd253)& ron(Vd261,Vd255)& rpoint(Vd261) ) )) )),
% 61.56/8.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 61.56/8.83 fof(f38,axiom,(
% 61.56/8.83 (! [Vd334,Vd335] :( rcenter(Vd334,Vd335)=> rinside(Vd334,Vd335) ) )),
% 61.56/8.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 61.56/8.83 fof(f128,plain,(
% 61.56/8.83 (![Vd1147]: (((~rR(Vd1147,vd1123,vd1125)|~ron(Vd1147,vd1146))|~ron(Vd1147,vd1145))|~rpoint(Vd1147)))),
% 61.56/8.83 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 61.56/8.83 fof(f129,plain,(
% 61.56/8.83 ![X0]: (~rR(X0,vd1123,vd1125)|~ron(X0,vd1146)|~ron(X0,vd1145)|~rpoint(X0))),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f128])).
% 61.56/8.83 fof(f130,plain,(
% 61.56/8.83 ~ron(vd1125,vd1146)),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f3])).
% 61.56/8.83 fof(f131,plain,(
% 61.56/8.83 ~rinside(vd1125,vd1146)),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f4])).
% 61.56/8.83 fof(f133,plain,(
% 61.56/8.83 rcenter(vd1123,vd1146)),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f5])).
% 61.56/8.83 fof(f134,plain,(
% 61.56/8.83 rcircle(vd1146)),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f5])).
% 61.56/8.83 fof(f135,plain,(
% 61.56/8.83 ron(vd1125,vd1145)),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f5])).
% 61.56/8.83 fof(f136,plain,(
% 61.56/8.83 ron(vd1123,vd1145)),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f5])).
% 61.56/8.83 fof(f137,plain,(
% 61.56/8.83 vd1123=vd1127),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f6])).
% 61.56/8.83 fof(f143,plain,(
% 61.56/8.83 vd1127=vd1128),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f7])).
% 61.56/8.83 fof(f144,plain,(
% 61.56/8.83 rpoint(vd1128)),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f7])).
% 61.56/8.83 fof(f145,plain,(
% 61.56/8.83 vd1125=vd1126),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f7])).
% 61.56/8.83 fof(f146,plain,(
% 61.56/8.83 rpoint(vd1126)),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f7])).
% 61.56/8.83 fof(f156,plain,(
% 61.56/8.83 rline(vd1145)),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f10])).
% 61.56/8.83 fof(f179,plain,(
% 61.56/8.83 ![Vd253,Vd254,Vd255,Vd256,Vd257,Vd258,Vd259,Vd260]: (((((((((((((~ron(Vd259,Vd255)|ron(Vd259,Vd253))|rinside(Vd259,Vd253))|~Vd259=Vd260)|~rpoint(Vd260))|~ron(Vd257,Vd255))|~rinside(Vd257,Vd253))|~Vd257=Vd258)|~rpoint(Vd258))|~Vd255=Vd256)|~rline(Vd256))|~Vd253=Vd254)|~rcircle(Vd254))|(?[Vd261]: (((rR(Vd261,Vd257,Vd259)&ron(Vd261,Vd253))&ron(Vd261,Vd255))&rpoint(Vd261))))),
% 61.56/8.83 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 61.56/8.83 fof(f180,plain,(
% 61.56/8.83 ![Vd253,Vd255,Vd257,Vd259]: ((![Vd254]: (((![Vd256]: (((![Vd258]: (((((![Vd260]: ((((~ron(Vd259,Vd255)|ron(Vd259,Vd253))|rinside(Vd259,Vd253))|~Vd259=Vd260)|~rpoint(Vd260)))|~ron(Vd257,Vd255))|~rinside(Vd257,Vd253))|~Vd257=Vd258)|~rpoint(Vd258)))|~Vd255=Vd256)|~rline(Vd256)))|~Vd253=Vd254)|~rcircle(Vd254)))|(?[Vd261]: (((rR(Vd261,Vd257,Vd259)&ron(Vd261,Vd253))&ron(Vd261,Vd255))&rpoint(Vd261))))),
% 61.56/8.83 inference(miniscoping,[status(thm)],[f179])).
% 61.56/8.83 fof(f181,plain,(
% 61.56/8.83 ![Vd253,Vd255,Vd257,Vd259]: ((![Vd254]: (((![Vd256]: (((![Vd258]: (((((![Vd260]: ((((~ron(Vd259,Vd255)|ron(Vd259,Vd253))|rinside(Vd259,Vd253))|~Vd259=Vd260)|~rpoint(Vd260)))|~ron(Vd257,Vd255))|~rinside(Vd257,Vd253))|~Vd257=Vd258)|~rpoint(Vd258)))|~Vd255=Vd256)|~rline(Vd256)))|~Vd253=Vd254)|~rcircle(Vd254)))|(((rR(sK2_skl(Vd259,Vd257,Vd255,Vd253),Vd257,Vd259)&ron(sK2_skl(Vd259,Vd257,Vd255,Vd253),Vd253))&ron(sK2_skl(Vd259,Vd257,Vd255,Vd253),Vd255))&rpoint(sK2_skl(Vd259,Vd257,Vd255,Vd253))))),
% 61.56/8.83 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Vd261,sK2_skl(Vd259,Vd257,Vd255,Vd253))],[f180])).
% 61.56/8.83 fof(f182,plain,(
% 61.56/8.83 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~ron(X0,X1)|ron(X0,X2)|rinside(X0,X2)|~X0=X3|~rpoint(X3)|~ron(X4,X1)|~rinside(X4,X2)|~X4=X5|~rpoint(X5)|~X1=X6|~rline(X6)|~X2=X7|~rcircle(X7)|rR(sK2_skl(X0,X4,X1,X2),X4,X0))),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f181])).
% 61.56/8.83 fof(f183,plain,(
% 61.56/8.83 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~ron(X0,X1)|ron(X0,X2)|rinside(X0,X2)|~X0=X3|~rpoint(X3)|~ron(X4,X1)|~rinside(X4,X2)|~X4=X5|~rpoint(X5)|~X1=X6|~rline(X6)|~X2=X7|~rcircle(X7)|ron(sK2_skl(X0,X4,X1,X2),X2))),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f181])).
% 61.56/8.83 fof(f184,plain,(
% 61.56/8.83 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~ron(X0,X1)|ron(X0,X2)|rinside(X0,X2)|~X0=X3|~rpoint(X3)|~ron(X4,X1)|~rinside(X4,X2)|~X4=X5|~rpoint(X5)|~X1=X6|~rline(X6)|~X2=X7|~rcircle(X7)|ron(sK2_skl(X0,X4,X1,X2),X1))),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f181])).
% 61.56/8.83 fof(f185,plain,(
% 61.56/8.83 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~ron(X0,X1)|ron(X0,X2)|rinside(X0,X2)|~X0=X3|~rpoint(X3)|~ron(X4,X1)|~rinside(X4,X2)|~X4=X5|~rpoint(X5)|~X1=X6|~rline(X6)|~X2=X7|~rcircle(X7)|rpoint(sK2_skl(X0,X4,X1,X2)))),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f181])).
% 61.56/8.83 fof(f259,plain,(
% 61.56/8.83 ![Vd334,Vd335]: (~rcenter(Vd334,Vd335)|rinside(Vd334,Vd335))),
% 61.56/8.83 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 61.56/8.83 fof(f260,plain,(
% 61.56/8.83 ![X0,X1]: (~rcenter(X0,X1)|rinside(X0,X1))),
% 61.56/8.83 inference(cnf_transformation,[status(thm)],[f259])).
% 61.56/8.83 fof(f787,plain,(
% 61.56/8.83 ![X0,X1,X2,X3]: (~ron(X0,X1)|ron(X0,X2)|rinside(X0,X2)|~rpoint(X0)|~ron(X3,X1)|~rinside(X3,X2)|~rpoint(X3)|~rline(X1)|~rcircle(X2)|rR(sK2_skl(X0,X3,X1,X2),X3,X0))),
% 61.56/8.83 inference(destructive_equality_resolution,[status(thm)],[f182])).
% 61.56/8.83 fof(f788,plain,(
% 61.56/8.83 ![X0,X1,X2,X3]: (~ron(X0,X1)|ron(X0,X2)|rinside(X0,X2)|~rpoint(X0)|~ron(X3,X1)|~rinside(X3,X2)|~rpoint(X3)|~rline(X1)|~rcircle(X2)|ron(sK2_skl(X0,X3,X1,X2),X2))),
% 61.56/8.83 inference(destructive_equality_resolution,[status(thm)],[f183])).
% 61.56/8.83 fof(f789,plain,(
% 61.56/8.83 ![X0,X1,X2,X3]: (~ron(X0,X1)|ron(X0,X2)|rinside(X0,X2)|~rpoint(X0)|~ron(X3,X1)|~rinside(X3,X2)|~rpoint(X3)|~rline(X1)|~rcircle(X2)|ron(sK2_skl(X0,X3,X1,X2),X1))),
% 61.56/8.83 inference(destructive_equality_resolution,[status(thm)],[f184])).
% 61.56/8.83 fof(f790,plain,(
% 61.56/8.83 ![X0,X1,X2,X3]: (~ron(X0,X1)|ron(X0,X2)|rinside(X0,X2)|~rpoint(X0)|~ron(X3,X1)|~rinside(X3,X2)|~rpoint(X3)|~rline(X1)|~rcircle(X2)|rpoint(sK2_skl(X0,X3,X1,X2)))),
% 61.56/8.83 inference(destructive_equality_resolution,[status(thm)],[f185])).
% 61.56/8.83 fof(f1019,definition,(
% 61.56/8.83 sQ29_spl <=> (rline(vd1145))),
% 61.56/8.83 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 61.56/8.83 fof(f1021,plain,(
% 61.56/8.83 ~rline(vd1145)|sQ29_spl),
% 61.56/8.83 inference(component_clause,[status(thm)],[f1019])).
% 61.56/8.83 fof(f1070,definition,(
% 61.56/8.83 sQ44_spl <=> (rpoint(vd1123))),
% 61.56/8.83 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 61.56/8.83 fof(f1072,plain,(
% 61.56/8.83 ~rpoint(vd1123)|sQ44_spl),
% 61.56/8.83 inference(component_clause,[status(thm)],[f1070])).
% 61.56/8.83 fof(f1084,definition,(
% 61.56/8.83 sQ48_spl <=> (rpoint(vd1125))),
% 61.56/8.83 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 61.56/8.83 fof(f1086,plain,(
% 61.56/8.83 ~rpoint(vd1125)|sQ48_spl),
% 61.56/8.83 inference(component_clause,[status(thm)],[f1084])).
% 61.56/8.83 fof(f1112,plain,(
% 61.56/8.83 $false|sQ29_spl),
% 61.56/8.83 inference(forward_subsumption_resolution,[status(thm)],[f1021,f156])).
% 61.56/8.83 fof(f1113,plain,(
% 61.56/8.83 sQ29_spl),
% 61.56/8.83 inference(contradiction_clause,[status(thm)],[f1112])).
% 61.56/8.83 fof(f1134,plain,(
% 61.56/8.83 vd1123=vd1128),
% 61.56/8.83 inference(forward_demodulation,[status(thm)],[f137,f143])).
% 61.56/8.83 fof(f1135,plain,(
% 61.56/8.83 rpoint(vd1123)),
% 61.56/8.83 inference(forward_demodulation,[status(thm)],[f1134,f144])).
% 61.56/8.83 fof(f1136,plain,(
% 61.56/8.83 $false|sQ44_spl),
% 61.56/8.83 inference(forward_subsumption_resolution,[status(thm)],[f1135,f1072])).
% 61.56/8.83 fof(f1137,plain,(
% 61.56/8.83 sQ44_spl),
% 61.56/8.83 inference(contradiction_clause,[status(thm)],[f1136])).
% 61.56/8.83 fof(f1227,plain,(
% 61.56/8.83 rpoint(vd1125)),
% 61.56/8.83 inference(forward_demodulation,[status(thm)],[f145,f146])).
% 61.56/8.83 fof(f1228,plain,(
% 61.56/8.83 $false|sQ48_spl),
% 61.56/8.83 inference(forward_subsumption_resolution,[status(thm)],[f1227,f1086])).
% 61.56/8.83 fof(f1229,plain,(
% 61.56/8.83 sQ48_spl),
% 61.56/8.83 inference(contradiction_clause,[status(thm)],[f1228])).
% 61.56/8.83 fof(f1395,definition,(
% 61.56/8.83 sQ90_spl <=> (ron(vd1125,vd1146))),
% 61.56/8.83 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 61.56/8.83 fof(f1396,plain,(
% 61.56/8.83 ron(vd1125,vd1146)|~sQ90_spl),
% 61.56/8.83 inference(component_clause,[status(thm)],[f1395])).
% 61.56/8.83 fof(f1426,plain,(
% 61.56/8.83 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~rpoint(vd1125)|~ron(X1,vd1145)|~rinside(X1,X0)|~rpoint(X1)|~rline(vd1145)|~rcircle(X0)|rR(sK2_skl(vd1125,X1,vd1145,X0),X1,vd1125))),
% 61.56/8.83 inference(resolution,[status(thm)],[f787,f135])).
% 61.56/8.83 fof(f1443,definition,(
% 61.56/8.83 ![X0,X1]: (sQ100_spl <=> (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1145)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|rR(sK2_skl(vd1125,X1,vd1145,X0),X1,vd1125)))),
% 61.56/8.83 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 61.56/8.83 fof(f1444,plain,(
% 61.56/8.83 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1145)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|rR(sK2_skl(vd1125,X1,vd1145,X0),X1,vd1125)|~sQ100_spl)),
% 61.56/8.83 inference(component_clause,[status(thm)],[f1443])).
% 61.56/8.83 fof(f1446,plain,(
% 61.56/8.83 sQ100_spl|~sQ48_spl|~sQ29_spl),
% 61.56/8.83 inference(split_clause,[status(thm)],[f1426,f1443,f1084,f1019])).
% 61.56/8.83 fof(f1451,plain,(
% 61.56/8.83 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~rpoint(vd1125)|~ron(X1,vd1145)|~rinside(X1,X0)|~rpoint(X1)|~rline(vd1145)|~rcircle(X0)|ron(sK2_skl(vd1125,X1,vd1145,X0),X0))),
% 61.56/8.83 inference(resolution,[status(thm)],[f788,f135])).
% 61.56/8.83 fof(f1468,definition,(
% 61.56/8.83 ![X0,X1]: (sQ105_spl <=> (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1145)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|ron(sK2_skl(vd1125,X1,vd1145,X0),X0)))),
% 61.56/8.83 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 61.56/8.83 fof(f1469,plain,(
% 61.56/8.83 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1145)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|ron(sK2_skl(vd1125,X1,vd1145,X0),X0)|~sQ105_spl)),
% 61.56/8.83 inference(component_clause,[status(thm)],[f1468])).
% 61.56/8.83 fof(f1471,plain,(
% 61.56/8.83 sQ105_spl|~sQ48_spl|~sQ29_spl),
% 61.56/8.83 inference(split_clause,[status(thm)],[f1451,f1468,f1084,f1019])).
% 61.56/8.83 fof(f1476,plain,(
% 61.56/8.83 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~rpoint(vd1125)|~ron(X1,vd1145)|~rinside(X1,X0)|~rpoint(X1)|~rline(vd1145)|~rcircle(X0)|ron(sK2_skl(vd1125,X1,vd1145,X0),vd1145))),
% 61.56/8.83 inference(resolution,[status(thm)],[f789,f135])).
% 61.56/8.83 fof(f1493,definition,(
% 61.56/8.83 ![X0,X1]: (sQ110_spl <=> (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1145)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|ron(sK2_skl(vd1125,X1,vd1145,X0),vd1145)))),
% 61.56/8.83 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 61.56/8.83 fof(f1494,plain,(
% 61.56/8.83 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1145)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|ron(sK2_skl(vd1125,X1,vd1145,X0),vd1145)|~sQ110_spl)),
% 61.56/8.83 inference(component_clause,[status(thm)],[f1493])).
% 61.56/8.83 fof(f1496,plain,(
% 61.56/8.83 sQ110_spl|~sQ48_spl|~sQ29_spl),
% 61.56/8.83 inference(split_clause,[status(thm)],[f1476,f1493,f1084,f1019])).
% 61.56/8.83 fof(f1501,plain,(
% 61.56/8.83 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~rpoint(vd1125)|~ron(X1,vd1145)|~rinside(X1,X0)|~rpoint(X1)|~rline(vd1145)|~rcircle(X0)|rpoint(sK2_skl(vd1125,X1,vd1145,X0)))),
% 61.56/8.83 inference(resolution,[status(thm)],[f790,f135])).
% 61.56/8.83 fof(f1518,definition,(
% 61.56/8.83 ![X0,X1]: (sQ115_spl <=> (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1145)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|rpoint(sK2_skl(vd1125,X1,vd1145,X0))))),
% 61.56/8.83 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 61.56/8.83 fof(f1519,plain,(
% 61.56/8.83 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1145)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|rpoint(sK2_skl(vd1125,X1,vd1145,X0))|~sQ115_spl)),
% 61.56/8.83 inference(component_clause,[status(thm)],[f1518])).
% 61.56/8.83 fof(f1521,plain,(
% 61.56/8.83 sQ115_spl|~sQ48_spl|~sQ29_spl),
% 61.56/8.83 inference(split_clause,[status(thm)],[f1501,f1518,f1084,f1019])).
% 61.56/8.83 fof(f1760,definition,(
% 61.56/8.83 sQ140_spl <=> (ron(vd1123,vd1145))),
% 61.56/8.83 introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 61.56/8.83 fof(f1762,plain,(
% 61.56/8.83 ~ron(vd1123,vd1145)|sQ140_spl),
% 61.56/8.83 inference(component_clause,[status(thm)],[f1760])).
% 61.56/8.83 fof(f1785,plain,(
% 61.56/8.83 $false|sQ140_spl),
% 61.56/8.83 inference(forward_subsumption_resolution,[status(thm)],[f1762,f136])).
% 61.56/8.83 fof(f1786,plain,(
% 61.56/8.83 sQ140_spl),
% 61.56/8.83 inference(contradiction_clause,[status(thm)],[f1785])).
% 61.56/8.83 fof(f1872,plain,(
% 61.56/8.83 rinside(vd1123,vd1146)),
% 61.56/8.83 inference(resolution,[status(thm)],[f260,f133])).
% 61.56/8.83 fof(f1975,definition,(
% 61.56/8.83 sQ178_spl <=> (rcircle(vd1146))),
% 61.56/8.83 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 61.56/8.83 fof(f1977,plain,(
% 61.56/8.83 ~rcircle(vd1146)|sQ178_spl),
% 61.56/8.83 inference(component_clause,[status(thm)],[f1975])).
% 61.56/8.83 fof(f1979,plain,(
% 61.56/8.83 $false|sQ178_spl),
% 61.56/8.83 inference(forward_subsumption_resolution,[status(thm)],[f1977,f134])).
% 61.56/8.83 fof(f1980,plain,(
% 61.56/8.83 sQ178_spl),
% 61.56/8.83 inference(contradiction_clause,[status(thm)],[f1979])).
% 61.56/8.83 fof(f3790,plain,(
% 61.56/8.83 ron(vd1125,vd1146)|rinside(vd1125,vd1146)|~ron(vd1123,vd1145)|~rpoint(vd1123)|~rcircle(vd1146)|rR(sK2_skl(vd1125,vd1123,vd1145,vd1146),vd1123,vd1125)|~sQ100_spl),
% 61.56/8.83 inference(resolution,[status(thm)],[f1872,f1444])).
% 61.56/8.83 fof(f3791,plain,(
% 61.56/8.83 ron(vd1125,vd1146)|rinside(vd1125,vd1146)|~ron(vd1123,vd1145)|~rpoint(vd1123)|~rcircle(vd1146)|rpoint(sK2_skl(vd1125,vd1123,vd1145,vd1146))|~sQ115_spl),
% 61.56/8.83 inference(resolution,[status(thm)],[f1872,f1519])).
% 61.56/8.83 fof(f3794,plain,(
% 61.56/8.83 ron(vd1125,vd1146)|rinside(vd1125,vd1146)|~ron(vd1123,vd1145)|~rpoint(vd1123)|~rcircle(vd1146)|ron(sK2_skl(vd1125,vd1123,vd1145,vd1146),vd1145)|~sQ110_spl),
% 61.56/8.83 inference(resolution,[status(thm)],[f1872,f1494])).
% 61.56/8.83 fof(f3796,plain,(
% 61.56/8.83 ron(vd1125,vd1146)|rinside(vd1125,vd1146)|~ron(vd1123,vd1145)|~rpoint(vd1123)|~rcircle(vd1146)|ron(sK2_skl(vd1125,vd1123,vd1145,vd1146),vd1146)|~sQ105_spl),
% 61.56/8.83 inference(resolution,[status(thm)],[f1872,f1469])).
% 61.56/8.83 fof(f3824,definition,(
% 61.56/8.83 sQ488_spl <=> (rinside(vd1125,vd1146))),
% 61.56/8.83 introduced(definition,[new_symbols(definition,[sQ488_spl])],[split_symbol_definition])).
% 61.56/8.83 fof(f3825,plain,(
% 61.56/8.83 rinside(vd1125,vd1146)|~sQ488_spl),
% 61.56/8.83 inference(component_clause,[status(thm)],[f3824])).
% 61.56/8.83 fof(f3827,definition,(
% 61.56/8.83 sQ489_spl <=> (rR(sK2_skl(vd1125,vd1123,vd1145,vd1146),vd1123,vd1125))),
% 61.56/8.83 introduced(definition,[new_symbols(definition,[sQ489_spl])],[split_symbol_definition])).
% 61.56/8.83 fof(f3828,plain,(
% 61.56/8.83 rR(sK2_skl(vd1125,vd1123,vd1145,vd1146),vd1123,vd1125)|~sQ489_spl),
% 61.56/8.83 inference(component_clause,[status(thm)],[f3827])).
% 61.56/8.83 fof(f3830,plain,(
% 61.56/8.83 sQ90_spl|sQ488_spl|~sQ140_spl|~sQ44_spl|~sQ178_spl|sQ489_spl|~sQ100_spl),
% 61.56/8.83 inference(split_clause,[status(thm)],[f3790,f1395,f3824,f1760,f1070,f1975,f3827,f1443])).
% 61.56/8.83 fof(f3831,definition,(
% 61.56/8.83 sQ490_spl <=> (rpoint(sK2_skl(vd1125,vd1123,vd1145,vd1146)))),
% 61.56/8.83 introduced(definition,[new_symbols(definition,[sQ490_spl])],[split_symbol_definition])).
% 61.56/8.83 fof(f3834,plain,(
% 61.56/8.83 sQ90_spl|sQ488_spl|~sQ140_spl|~sQ44_spl|~sQ178_spl|sQ490_spl|~sQ115_spl),
% 61.56/8.83 inference(split_clause,[status(thm)],[f3791,f1395,f3824,f1760,f1070,f1975,f3831,f1518])).
% 61.56/8.83 fof(f3843,definition,(
% 61.56/8.83 sQ493_spl <=> (ron(sK2_skl(vd1125,vd1123,vd1145,vd1146),vd1145))),
% 61.56/8.83 introduced(definition,[new_symbols(definition,[sQ493_spl])],[split_symbol_definition])).
% 61.56/8.83 fof(f3846,plain,(
% 61.56/8.83 sQ90_spl|sQ488_spl|~sQ140_spl|~sQ44_spl|~sQ178_spl|sQ493_spl|~sQ110_spl),
% 61.56/8.83 inference(split_clause,[status(thm)],[f3794,f1395,f3824,f1760,f1070,f1975,f3843,f1493])).
% 61.56/8.83 fof(f3851,definition,(
% 61.56/8.83 sQ495_spl <=> (ron(sK2_skl(vd1125,vd1123,vd1145,vd1146),vd1146))),
% 61.56/8.83 introduced(definition,[new_symbols(definition,[sQ495_spl])],[split_symbol_definition])).
% 42.61/8.88 fof(f3854,plain,(
% 42.61/8.88 sQ90_spl|sQ488_spl|~sQ140_spl|~sQ44_spl|~sQ178_spl|sQ495_spl|~sQ105_spl),
% 42.61/8.88 inference(split_clause,[status(thm)],[f3796,f1395,f3824,f1760,f1070,f1975,f3851,f1468])).
% 42.61/8.88 fof(f3859,plain,(
% 42.61/8.88 $false|~sQ488_spl),
% 42.61/8.88 inference(forward_subsumption_resolution,[status(thm)],[f3825,f131])).
% 42.61/8.88 fof(f3860,plain,(
% 42.61/8.88 ~sQ488_spl),
% 42.61/8.88 inference(contradiction_clause,[status(thm)],[f3859])).
% 42.61/8.88 fof(f11238,plain,(
% 42.61/8.88 ~ron(sK2_skl(vd1125,vd1123,vd1145,vd1146),vd1146)|~ron(sK2_skl(vd1125,vd1123,vd1145,vd1146),vd1145)|~rpoint(sK2_skl(vd1125,vd1123,vd1145,vd1146))|~sQ489_spl),
% 42.61/8.88 inference(resolution,[status(thm)],[f3828,f129])).
% 42.61/8.88 fof(f11260,plain,(
% 42.61/8.88 ~sQ495_spl|~sQ493_spl|~sQ490_spl|~sQ489_spl),
% 42.61/8.88 inference(split_clause,[status(thm)],[f11238,f3851,f3843,f3831,f3827])).
% 42.61/8.88 fof(f11532,plain,(
% 42.61/8.88 $false|~sQ90_spl),
% 42.61/8.88 inference(forward_subsumption_resolution,[status(thm)],[f1396,f130])).
% 42.61/8.88 fof(f11533,plain,(
% 42.61/8.88 ~sQ90_spl),
% 42.61/8.88 inference(contradiction_clause,[status(thm)],[f11532])).
% 42.61/8.88 fof(f11534,plain,(
% 42.61/8.88 $false),
% 42.61/8.88 inference(sat_refutation,[status(thm)],[f1113,f1137,f1229,f1446,f1471,f1496,f1521,f1786,f1980,f3830,f3834,f3846,f3854,f3860,f11260,f11533])).
% 42.61/8.88 % SZS output end CNFRefutation for theBenchmark.p
% 42.61/8.90 % Elapsed time: 8.402620 seconds
% 42.61/8.90 % CPU time: 65.713562 seconds
% 42.61/8.90 % Total memory used: 310.632 MB
% 42.61/8.90 % Net memory used: 292.046 MB
%------------------------------------------------------------------------------