%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO281+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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 0.14s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO281+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n007.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 20 15:05:05 UTC 2026
% 0.14/0.37 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 0.14/0.45 % Refutation found
% 0.14/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.45 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.45 fof(f1,conjecture,(
% 0.14/0.45 (? [Vd1140] :( rR(Vd1140,vd1123,vd1125)& ron(Vd1140,vd1139)& ron(Vd1140,vd1138)& rpoint(Vd1140) ) )),
% 0.14/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.45 fof(f2,negated_conjecture,(
% 0.14/0.45 ~((? [Vd1140] :( rR(Vd1140,vd1123,vd1125)& ron(Vd1140,vd1139)& ron(Vd1140,vd1138)& rpoint(Vd1140) ) ))),
% 0.14/0.45 inference(negated_conjecture,[status(cth)],[f1])).
% 0.14/0.45 fof(f3,axiom,(
% 0.14/0.45 ~ ron(vd1125,vd1139) ),
% 0.14/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.45 fof(f4,axiom,(
% 0.14/0.45 ~ rinside(vd1125,vd1139) ),
% 0.14/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.45 fof(f5,axiom,(
% 0.14/0.45 ( ron(vd1136,vd1139)& rcenter(vd1123,vd1139)& rcircle(vd1139)& ron(vd1125,vd1138)& ron(vd1123,vd1138) ) ),
% 0.14/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.45 fof(f8,axiom,(
% 0.14/0.45 ( 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) ) ),
% 0.14/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.45 fof(f12,axiom,(
% 0.14/0.45 rline(vd1138) ),
% 0.14/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.45 fof(f15,axiom,(
% 0.14/0.45 (! [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) ) )) )),
% 0.14/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.45 fof(f69,axiom,(
% 0.14/0.45 (! [Vd334,Vd335] :( rcenter(Vd334,Vd335)=> rinside(Vd334,Vd335) ) )),
% 0.14/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.45 fof(f119,plain,(
% 0.14/0.45 (![Vd1140]: (((~rR(Vd1140,vd1123,vd1125)|~ron(Vd1140,vd1139))|~ron(Vd1140,vd1138))|~rpoint(Vd1140)))),
% 0.14/0.45 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.14/0.45 fof(f120,plain,(
% 0.14/0.45 ![X0]: (~rR(X0,vd1123,vd1125)|~ron(X0,vd1139)|~ron(X0,vd1138)|~rpoint(X0))),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f119])).
% 0.14/0.45 fof(f121,plain,(
% 0.14/0.45 ~ron(vd1125,vd1139)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f3])).
% 0.14/0.45 fof(f122,plain,(
% 0.14/0.45 ~rinside(vd1125,vd1139)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/0.45 fof(f124,plain,(
% 0.14/0.45 rcenter(vd1123,vd1139)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/0.45 fof(f125,plain,(
% 0.14/0.45 rcircle(vd1139)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/0.45 fof(f126,plain,(
% 0.14/0.45 ron(vd1125,vd1138)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/0.45 fof(f127,plain,(
% 0.14/0.45 ron(vd1123,vd1138)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/0.45 fof(f137,plain,(
% 0.14/0.45 vd1125=vd1126),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/0.45 fof(f138,plain,(
% 0.14/0.45 rpoint(vd1126)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/0.45 fof(f139,plain,(
% 0.14/0.45 vd1123=vd1124),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/0.45 fof(f140,plain,(
% 0.14/0.45 rpoint(vd1124)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/0.45 fof(f153,plain,(
% 0.14/0.45 rline(vd1138)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.45 fof(f161,plain,(
% 0.14/0.45 ![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))))),
% 0.14/0.45 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.14/0.45 fof(f162,plain,(
% 0.14/0.45 ![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))))),
% 0.14/0.45 inference(miniscoping,[status(thm)],[f161])).
% 0.14/0.45 fof(f163,plain,(
% 0.14/0.45 ![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(sK1_skl(Vd259,Vd257,Vd255,Vd253),Vd257,Vd259)&ron(sK1_skl(Vd259,Vd257,Vd255,Vd253),Vd253))&ron(sK1_skl(Vd259,Vd257,Vd255,Vd253),Vd255))&rpoint(sK1_skl(Vd259,Vd257,Vd255,Vd253))))),
% 0.14/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Vd261,sK1_skl(Vd259,Vd257,Vd255,Vd253))],[f162])).
% 0.14/0.45 fof(f164,plain,(
% 0.14/0.45 ![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(sK1_skl(X0,X4,X1,X2),X4,X0))),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f163])).
% 0.14/0.45 fof(f165,plain,(
% 0.14/0.45 ![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(sK1_skl(X0,X4,X1,X2),X2))),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f163])).
% 0.14/0.45 fof(f166,plain,(
% 0.14/0.45 ![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(sK1_skl(X0,X4,X1,X2),X1))),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f163])).
% 0.14/0.45 fof(f167,plain,(
% 0.14/0.45 ![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(sK1_skl(X0,X4,X1,X2)))),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f163])).
% 0.14/0.45 fof(f350,plain,(
% 0.14/0.45 ![Vd334,Vd335]: (~rcenter(Vd334,Vd335)|rinside(Vd334,Vd335))),
% 0.14/0.45 inference(pre_NNF_transformation,[status(thm)],[f69])).
% 0.14/0.45 fof(f351,plain,(
% 0.14/0.45 ![X0,X1]: (~rcenter(X0,X1)|rinside(X0,X1))),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f350])).
% 0.14/0.45 fof(f676,plain,(
% 0.14/0.45 ![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(sK1_skl(X0,X3,X1,X2),X3,X0))),
% 0.14/0.45 inference(destructive_equality_resolution,[status(thm)],[f164])).
% 0.14/0.45 fof(f677,plain,(
% 0.14/0.45 ![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(sK1_skl(X0,X3,X1,X2),X2))),
% 0.14/0.45 inference(destructive_equality_resolution,[status(thm)],[f165])).
% 0.14/0.45 fof(f678,plain,(
% 0.14/0.45 ![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(sK1_skl(X0,X3,X1,X2),X1))),
% 0.14/0.45 inference(destructive_equality_resolution,[status(thm)],[f166])).
% 0.14/0.45 fof(f679,plain,(
% 0.14/0.45 ![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(sK1_skl(X0,X3,X1,X2)))),
% 0.14/0.45 inference(destructive_equality_resolution,[status(thm)],[f167])).
% 0.14/0.45 fof(f900,definition,(
% 0.14/0.45 sQ9_spl <=> (rline(vd1138))),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f902,plain,(
% 0.14/0.45 ~rline(vd1138)|sQ9_spl),
% 0.14/0.45 inference(component_clause,[status(thm)],[f900])).
% 0.14/0.45 fof(f903,definition,(
% 0.14/0.45 sQ10_spl <=> (rpoint(vd1123))),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f905,plain,(
% 0.14/0.45 ~rpoint(vd1123)|sQ10_spl),
% 0.14/0.45 inference(component_clause,[status(thm)],[f903])).
% 0.14/0.45 fof(f910,definition,(
% 0.14/0.45 sQ12_spl <=> (rpoint(vd1125))),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f912,plain,(
% 0.14/0.45 ~rpoint(vd1125)|sQ12_spl),
% 0.14/0.45 inference(component_clause,[status(thm)],[f910])).
% 0.14/0.45 fof(f924,plain,(
% 0.14/0.45 $false|sQ9_spl),
% 0.14/0.45 inference(forward_subsumption_resolution,[status(thm)],[f902,f153])).
% 0.14/0.45 fof(f925,plain,(
% 0.14/0.45 sQ9_spl),
% 0.14/0.45 inference(contradiction_clause,[status(thm)],[f924])).
% 0.14/0.45 fof(f961,plain,(
% 0.14/0.45 rpoint(vd1125)),
% 0.14/0.45 inference(forward_demodulation,[status(thm)],[f137,f138])).
% 0.14/0.45 fof(f962,plain,(
% 0.14/0.45 rpoint(vd1123)),
% 0.14/0.45 inference(forward_demodulation,[status(thm)],[f139,f140])).
% 0.14/0.45 fof(f978,plain,(
% 0.14/0.45 $false|sQ10_spl),
% 0.14/0.45 inference(forward_subsumption_resolution,[status(thm)],[f905,f962])).
% 0.14/0.45 fof(f979,plain,(
% 0.14/0.45 sQ10_spl),
% 0.14/0.45 inference(contradiction_clause,[status(thm)],[f978])).
% 0.14/0.45 fof(f980,plain,(
% 0.14/0.45 $false|sQ12_spl),
% 0.14/0.45 inference(forward_subsumption_resolution,[status(thm)],[f912,f961])).
% 0.14/0.45 fof(f981,plain,(
% 0.14/0.45 sQ12_spl),
% 0.14/0.45 inference(contradiction_clause,[status(thm)],[f980])).
% 0.14/0.45 fof(f1117,plain,(
% 0.14/0.45 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~rpoint(vd1125)|~ron(X1,vd1138)|~rinside(X1,X0)|~rpoint(X1)|~rline(vd1138)|~rcircle(X0)|rR(sK1_skl(vd1125,X1,vd1138,X0),X1,vd1125))),
% 0.14/0.45 inference(resolution,[status(thm)],[f676,f126])).
% 0.14/0.45 fof(f1123,definition,(
% 0.14/0.45 ![X0,X1]: (sQ53_spl <=> (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1138)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|rR(sK1_skl(vd1125,X1,vd1138,X0),X1,vd1125)))),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f1124,plain,(
% 0.14/0.45 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1138)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|rR(sK1_skl(vd1125,X1,vd1138,X0),X1,vd1125)|~sQ53_spl)),
% 0.14/0.45 inference(component_clause,[status(thm)],[f1123])).
% 0.14/0.45 fof(f1126,plain,(
% 0.14/0.45 sQ53_spl|~sQ12_spl|~sQ9_spl),
% 0.14/0.45 inference(split_clause,[status(thm)],[f1117,f1123,f910,f900])).
% 0.14/0.45 fof(f1132,plain,(
% 0.14/0.45 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~rpoint(vd1125)|~ron(X1,vd1138)|~rinside(X1,X0)|~rpoint(X1)|~rline(vd1138)|~rcircle(X0)|ron(sK1_skl(vd1125,X1,vd1138,X0),X0))),
% 0.14/0.45 inference(resolution,[status(thm)],[f677,f126])).
% 0.14/0.45 fof(f1138,definition,(
% 0.14/0.45 ![X0,X1]: (sQ56_spl <=> (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1138)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|ron(sK1_skl(vd1125,X1,vd1138,X0),X0)))),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f1139,plain,(
% 0.14/0.45 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1138)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|ron(sK1_skl(vd1125,X1,vd1138,X0),X0)|~sQ56_spl)),
% 0.14/0.45 inference(component_clause,[status(thm)],[f1138])).
% 0.14/0.45 fof(f1141,plain,(
% 0.14/0.45 sQ56_spl|~sQ12_spl|~sQ9_spl),
% 0.14/0.45 inference(split_clause,[status(thm)],[f1132,f1138,f910,f900])).
% 0.14/0.45 fof(f1147,plain,(
% 0.14/0.45 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~rpoint(vd1125)|~ron(X1,vd1138)|~rinside(X1,X0)|~rpoint(X1)|~rline(vd1138)|~rcircle(X0)|ron(sK1_skl(vd1125,X1,vd1138,X0),vd1138))),
% 0.14/0.45 inference(resolution,[status(thm)],[f678,f126])).
% 0.14/0.45 fof(f1153,definition,(
% 0.14/0.45 ![X0,X1]: (sQ59_spl <=> (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1138)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|ron(sK1_skl(vd1125,X1,vd1138,X0),vd1138)))),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f1154,plain,(
% 0.14/0.45 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1138)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|ron(sK1_skl(vd1125,X1,vd1138,X0),vd1138)|~sQ59_spl)),
% 0.14/0.45 inference(component_clause,[status(thm)],[f1153])).
% 0.14/0.45 fof(f1156,plain,(
% 0.14/0.45 sQ59_spl|~sQ12_spl|~sQ9_spl),
% 0.14/0.45 inference(split_clause,[status(thm)],[f1147,f1153,f910,f900])).
% 0.14/0.45 fof(f1176,definition,(
% 0.14/0.45 sQ64_spl <=> (ron(vd1123,vd1138))),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f1178,plain,(
% 0.14/0.45 ~ron(vd1123,vd1138)|sQ64_spl),
% 0.14/0.45 inference(component_clause,[status(thm)],[f1176])).
% 0.14/0.45 fof(f1216,plain,(
% 0.14/0.45 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~rpoint(vd1125)|~ron(X1,vd1138)|~rinside(X1,X0)|~rpoint(X1)|~rline(vd1138)|~rcircle(X0)|rpoint(sK1_skl(vd1125,X1,vd1138,X0)))),
% 0.14/0.45 inference(resolution,[status(thm)],[f679,f126])).
% 0.14/0.45 fof(f1222,definition,(
% 0.14/0.45 ![X0,X1]: (sQ76_spl <=> (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1138)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|rpoint(sK1_skl(vd1125,X1,vd1138,X0))))),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f1223,plain,(
% 0.14/0.45 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1138)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|rpoint(sK1_skl(vd1125,X1,vd1138,X0))|~sQ76_spl)),
% 0.14/0.45 inference(component_clause,[status(thm)],[f1222])).
% 0.14/0.45 fof(f1225,plain,(
% 0.14/0.45 sQ76_spl|~sQ12_spl|~sQ9_spl),
% 0.14/0.45 inference(split_clause,[status(thm)],[f1216,f1222,f910,f900])).
% 0.14/0.45 fof(f1608,plain,(
% 0.14/0.45 rinside(vd1123,vd1139)),
% 0.14/0.45 inference(resolution,[status(thm)],[f351,f124])).
% 0.14/0.45 fof(f1609,plain,(
% 0.14/0.45 ron(vd1125,vd1139)|rinside(vd1125,vd1139)|~ron(vd1123,vd1138)|~rpoint(vd1123)|~rcircle(vd1139)|rpoint(sK1_skl(vd1125,vd1123,vd1138,vd1139))|~sQ76_spl),
% 0.14/0.45 inference(resolution,[status(thm)],[f1608,f1223])).
% 0.14/0.45 fof(f1611,plain,(
% 0.14/0.45 ron(vd1125,vd1139)|rinside(vd1125,vd1139)|~ron(vd1123,vd1138)|~rpoint(vd1123)|~rcircle(vd1139)|ron(sK1_skl(vd1125,vd1123,vd1138,vd1139),vd1138)|~sQ59_spl),
% 0.14/0.45 inference(resolution,[status(thm)],[f1608,f1154])).
% 0.14/0.45 fof(f1613,plain,(
% 0.14/0.45 ron(vd1125,vd1139)|rinside(vd1125,vd1139)|~ron(vd1123,vd1138)|~rpoint(vd1123)|~rcircle(vd1139)|ron(sK1_skl(vd1125,vd1123,vd1138,vd1139),vd1139)|~sQ56_spl),
% 0.14/0.45 inference(resolution,[status(thm)],[f1608,f1139])).
% 0.14/0.45 fof(f1615,plain,(
% 0.14/0.45 ron(vd1125,vd1139)|rinside(vd1125,vd1139)|~ron(vd1123,vd1138)|~rpoint(vd1123)|~rcircle(vd1139)|rR(sK1_skl(vd1125,vd1123,vd1138,vd1139),vd1123,vd1125)|~sQ53_spl),
% 0.14/0.45 inference(resolution,[status(thm)],[f1608,f1124])).
% 0.14/0.45 fof(f1617,definition,(
% 0.14/0.45 sQ131_spl <=> (ron(vd1125,vd1139))),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f1618,plain,(
% 0.14/0.45 ron(vd1125,vd1139)|~sQ131_spl),
% 0.14/0.45 inference(component_clause,[status(thm)],[f1617])).
% 0.14/0.45 fof(f1620,definition,(
% 0.14/0.45 sQ132_spl <=> (rinside(vd1125,vd1139))),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f1621,plain,(
% 0.14/0.45 rinside(vd1125,vd1139)|~sQ132_spl),
% 0.14/0.45 inference(component_clause,[status(thm)],[f1620])).
% 0.14/0.45 fof(f1623,definition,(
% 0.14/0.45 sQ133_spl <=> (rcircle(vd1139))),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f1625,plain,(
% 0.14/0.45 ~rcircle(vd1139)|sQ133_spl),
% 0.14/0.45 inference(component_clause,[status(thm)],[f1623])).
% 0.14/0.45 fof(f1626,definition,(
% 0.14/0.45 sQ134_spl <=> (rpoint(sK1_skl(vd1125,vd1123,vd1138,vd1139)))),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f1629,plain,(
% 0.14/0.45 sQ131_spl|sQ132_spl|~sQ64_spl|~sQ10_spl|~sQ133_spl|sQ134_spl|~sQ76_spl),
% 0.14/0.45 inference(split_clause,[status(thm)],[f1609,f1617,f1620,f1176,f903,f1623,f1626,f1222])).
% 0.14/0.45 fof(f1640,definition,(
% 0.14/0.45 sQ138_spl <=> (ron(sK1_skl(vd1125,vd1123,vd1138,vd1139),vd1138))),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f1643,plain,(
% 0.14/0.45 sQ131_spl|sQ132_spl|~sQ64_spl|~sQ10_spl|~sQ133_spl|sQ138_spl|~sQ59_spl),
% 0.14/0.45 inference(split_clause,[status(thm)],[f1611,f1617,f1620,f1176,f903,f1623,f1640,f1153])).
% 0.14/0.45 fof(f1648,definition,(
% 0.14/0.45 sQ140_spl <=> (ron(sK1_skl(vd1125,vd1123,vd1138,vd1139),vd1139))),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f1651,plain,(
% 0.14/0.45 sQ131_spl|sQ132_spl|~sQ64_spl|~sQ10_spl|~sQ133_spl|sQ140_spl|~sQ56_spl),
% 0.14/0.45 inference(split_clause,[status(thm)],[f1613,f1617,f1620,f1176,f903,f1623,f1648,f1138])).
% 0.14/0.45 fof(f1656,definition,(
% 0.14/0.45 sQ142_spl <=> (rR(sK1_skl(vd1125,vd1123,vd1138,vd1139),vd1123,vd1125))),
% 0.14/0.45 introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition])).
% 0.14/0.45 fof(f1657,plain,(
% 0.14/0.45 rR(sK1_skl(vd1125,vd1123,vd1138,vd1139),vd1123,vd1125)|~sQ142_spl),
% 0.14/0.45 inference(component_clause,[status(thm)],[f1656])).
% 0.14/0.45 fof(f1659,plain,(
% 0.14/0.45 sQ131_spl|sQ132_spl|~sQ64_spl|~sQ10_spl|~sQ133_spl|sQ142_spl|~sQ53_spl),
% 0.14/0.45 inference(split_clause,[status(thm)],[f1615,f1617,f1620,f1176,f903,f1623,f1656,f1123])).
% 0.14/0.45 fof(f1664,plain,(
% 0.14/0.45 $false|sQ133_spl),
% 0.14/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1625,f125])).
% 0.14/0.45 fof(f1665,plain,(
% 0.14/0.45 sQ133_spl),
% 0.14/0.45 inference(contradiction_clause,[status(thm)],[f1664])).
% 0.14/0.45 fof(f1666,plain,(
% 0.14/0.45 $false|~sQ132_spl),
% 0.14/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1621,f122])).
% 0.14/0.45 fof(f1667,plain,(
% 0.14/0.45 ~sQ132_spl),
% 0.14/0.45 inference(contradiction_clause,[status(thm)],[f1666])).
% 0.14/0.45 fof(f1668,plain,(
% 0.14/0.45 $false|~sQ131_spl),
% 0.14/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1618,f121])).
% 0.14/0.45 fof(f1669,plain,(
% 0.14/0.45 ~sQ131_spl),
% 0.14/0.45 inference(contradiction_clause,[status(thm)],[f1668])).
% 0.14/0.45 fof(f1670,plain,(
% 0.14/0.45 $false|sQ64_spl),
% 0.14/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1178,f127])).
% 0.14/0.45 fof(f1671,plain,(
% 0.14/0.45 sQ64_spl),
% 0.14/0.45 inference(contradiction_clause,[status(thm)],[f1670])).
% 0.14/0.45 fof(f1814,plain,(
% 0.14/0.45 ~ron(sK1_skl(vd1125,vd1123,vd1138,vd1139),vd1139)|~ron(sK1_skl(vd1125,vd1123,vd1138,vd1139),vd1138)|~rpoint(sK1_skl(vd1125,vd1123,vd1138,vd1139))|~sQ142_spl),
% 0.14/0.45 inference(resolution,[status(thm)],[f1657,f120])).
% 0.14/0.45 fof(f1821,plain,(
% 0.14/0.45 ~sQ140_spl|~sQ138_spl|~sQ134_spl|~sQ142_spl),
% 0.14/0.45 inference(split_clause,[status(thm)],[f1814,f1648,f1640,f1626,f1656])).
% 0.14/0.45 fof(f1843,plain,(
% 0.14/0.45 $false),
% 0.14/0.45 inference(sat_refutation,[status(thm)],[f925,f979,f981,f1126,f1141,f1156,f1225,f1629,f1643,f1651,f1659,f1665,f1667,f1669,f1671,f1821])).
% 0.14/0.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.48 % Elapsed time: 0.112987 seconds
% 0.14/0.48 % CPU time: 0.571698 seconds
% 0.14/0.48 % Total memory used: 123.054 MB
% 0.14/0.48 % Net memory used: 122.282 MB
%------------------------------------------------------------------------------