%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO286+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 : n016.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 15.69s 2.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GEO286+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n016.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Sun Sep 20 15:12:22 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.52 % Drodi V4.1.1
% 15.69/2.65 % Refutation found
% 15.69/2.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.69/2.65 % SZS output start CNFRefutation for theBenchmark
% 15.69/2.65 fof(f1,conjecture,(
% 15.69/2.65 (? [Vd1153] :( rR(Vd1153,vd1123,vd1125)& ron(Vd1153,vd1152)& ron(Vd1153,vd1151)& rpoint(Vd1153) ) )),
% 15.69/2.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.69/2.65 fof(f2,negated_conjecture,(
% 15.69/2.65 ~((? [Vd1153] :( rR(Vd1153,vd1123,vd1125)& ron(Vd1153,vd1152)& ron(Vd1153,vd1151)& rpoint(Vd1153) ) ))),
% 15.69/2.65 inference(negated_conjecture,[status(cth)],[f1])).
% 15.69/2.65 fof(f3,axiom,(
% 15.69/2.65 ~ ron(vd1125,vd1152) ),
% 15.69/2.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.69/2.65 fof(f4,axiom,(
% 15.69/2.65 ~ rinside(vd1125,vd1152) ),
% 15.69/2.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.69/2.65 fof(f5,axiom,(
% 15.69/2.65 ( ron(vd1127,vd1152)& rcenter(vd1123,vd1152)& rcircle(vd1152)& ron(vd1125,vd1151)& ron(vd1123,vd1151) ) ),
% 15.69/2.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.69/2.65 fof(f6,axiom,(
% 15.69/2.65 vd1123 = vd1129 ),
% 15.69/2.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.69/2.65 fof(f7,axiom,(
% 15.69/2.65 ( 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) ) ),
% 15.69/2.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.69/2.65 fof(f12,axiom,(
% 15.69/2.65 rline(vd1151) ),
% 15.69/2.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.69/2.65 fof(f18,axiom,(
% 15.69/2.65 (! [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) ) )) )),
% 15.69/2.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.69/2.65 fof(f84,axiom,(
% 15.69/2.65 (! [Vd334,Vd335] :( rcenter(Vd334,Vd335)=> rinside(Vd334,Vd335) ) )),
% 15.69/2.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.69/2.65 fof(f93,axiom,(
% 15.69/2.65 (! [Vd214,Vd215] :( ( Vd214 = Vd215& rcircle(Vd215) )=> (? [Vd216] :( ~ ron(Vd216,Vd214)& ~ rinside(Vd216,Vd214)& rpoint(Vd216) ) )) )),
% 15.69/2.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.69/2.65 fof(f94,axiom,(
% 15.69/2.65 (! [Vd211,Vd212] :( ( Vd211 = Vd212& rcircle(Vd212) )=> (? [Vd213] :( rinside(Vd213,Vd211)& rpoint(Vd213) ) )) )),
% 15.69/2.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.69/2.65 fof(f97,axiom,(
% 15.69/2.65 (! [Vd191,Vd192] :( ( Vd191 = Vd192& rcircle(Vd192) )=> (? [Vd193] :( ron(Vd193,Vd191)& rpoint(Vd193) ) )) )),
% 15.69/2.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.69/2.65 fof(f110,axiom,(
% 15.69/2.65 (! [Vd52,Vd53] :( ( Vd52 = Vd53& rline(Vd53) )=> (? [Vd54] :( ron(Vd54,Vd52)& rpoint(Vd54) ) )) )),
% 15.69/2.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.69/2.65 fof(f114,axiom,(
% 15.69/2.65 (! [Vd15,Vd16] :( ( Vd15 = Vd16& rpoint(Vd16) )=> (? [Vd17] :( Vd17 != Vd15& rpoint(Vd17) ) )) )),
% 15.69/2.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.69/2.65 fof(f115,axiom,(
% 15.69/2.65 rpoint(vd14) ),
% 15.69/2.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.69/2.65 fof(f137,plain,(
% 15.69/2.65 (![Vd1153]: (((~rR(Vd1153,vd1123,vd1125)|~ron(Vd1153,vd1152))|~ron(Vd1153,vd1151))|~rpoint(Vd1153)))),
% 15.69/2.65 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 15.69/2.65 fof(f138,plain,(
% 15.69/2.65 ![X0]: (~rR(X0,vd1123,vd1125)|~ron(X0,vd1152)|~ron(X0,vd1151)|~rpoint(X0))),
% 15.69/2.65 inference(cnf_transformation,[status(thm)],[f137])).
% 15.69/2.65 fof(f139,plain,(
% 15.69/2.65 ~ron(vd1125,vd1152)),
% 15.69/2.65 inference(cnf_transformation,[status(thm)],[f3])).
% 15.69/2.65 fof(f140,plain,(
% 15.69/2.65 ~rinside(vd1125,vd1152)),
% 15.69/2.65 inference(cnf_transformation,[status(thm)],[f4])).
% 15.69/2.65 fof(f142,plain,(
% 15.69/2.65 rcenter(vd1123,vd1152)),
% 15.69/2.65 inference(cnf_transformation,[status(thm)],[f5])).
% 15.69/2.65 fof(f143,plain,(
% 15.69/2.65 rcircle(vd1152)),
% 15.69/2.65 inference(cnf_transformation,[status(thm)],[f5])).
% 15.69/2.65 fof(f144,plain,(
% 15.69/2.65 ron(vd1125,vd1151)),
% 15.69/2.65 inference(cnf_transformation,[status(thm)],[f5])).
% 15.69/2.65 fof(f145,plain,(
% 15.69/2.65 ron(vd1123,vd1151)),
% 15.69/2.65 inference(cnf_transformation,[status(thm)],[f5])).
% 15.69/2.65 fof(f146,plain,(
% 15.69/2.65 vd1123=vd1129),
% 15.69/2.65 inference(cnf_transformation,[status(thm)],[f6])).
% 15.69/2.65 fof(f150,plain,(
% 15.69/2.65 vd1129=vd1130),
% 15.69/2.65 inference(cnf_transformation,[status(thm)],[f7])).
% 15.69/2.66 fof(f151,plain,(
% 15.69/2.66 rpoint(vd1130)),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f7])).
% 15.69/2.66 fof(f152,plain,(
% 15.69/2.66 vd1127=vd1128),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f7])).
% 15.69/2.66 fof(f153,plain,(
% 15.69/2.66 rpoint(vd1128)),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f7])).
% 15.69/2.66 fof(f154,plain,(
% 15.69/2.66 vd1125=vd1126),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f7])).
% 15.69/2.66 fof(f155,plain,(
% 15.69/2.66 rpoint(vd1126)),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f7])).
% 15.69/2.66 fof(f172,plain,(
% 15.69/2.66 rline(vd1151)),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f12])).
% 15.69/2.66 fof(f197,plain,(
% 15.69/2.66 ![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))))),
% 15.69/2.66 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 15.69/2.66 fof(f198,plain,(
% 15.69/2.66 ![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))))),
% 15.69/2.66 inference(miniscoping,[status(thm)],[f197])).
% 15.69/2.66 fof(f199,plain,(
% 15.69/2.66 ![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(sK3_skl(Vd259,Vd257,Vd255,Vd253),Vd257,Vd259)&ron(sK3_skl(Vd259,Vd257,Vd255,Vd253),Vd253))&ron(sK3_skl(Vd259,Vd257,Vd255,Vd253),Vd255))&rpoint(sK3_skl(Vd259,Vd257,Vd255,Vd253))))),
% 15.69/2.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(Vd261,sK3_skl(Vd259,Vd257,Vd255,Vd253))],[f198])).
% 15.69/2.66 fof(f200,plain,(
% 15.69/2.66 ![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(sK3_skl(X0,X4,X1,X2),X4,X0))),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f199])).
% 15.69/2.66 fof(f201,plain,(
% 15.69/2.66 ![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(sK3_skl(X0,X4,X1,X2),X2))),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f199])).
% 15.69/2.66 fof(f202,plain,(
% 15.69/2.66 ![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(sK3_skl(X0,X4,X1,X2),X1))),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f199])).
% 15.69/2.66 fof(f203,plain,(
% 15.69/2.66 ![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(sK3_skl(X0,X4,X1,X2)))),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f199])).
% 15.69/2.66 fof(f408,plain,(
% 15.69/2.66 ![Vd334,Vd335]: (~rcenter(Vd334,Vd335)|rinside(Vd334,Vd335))),
% 15.69/2.66 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 15.69/2.66 fof(f409,plain,(
% 15.69/2.66 ![X0,X1]: (~rcenter(X0,X1)|rinside(X0,X1))),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f408])).
% 15.69/2.66 fof(f455,plain,(
% 15.69/2.66 ![Vd214,Vd215]: ((~Vd214=Vd215|~rcircle(Vd215))|(?[Vd216]: ((~ron(Vd216,Vd214)&~rinside(Vd216,Vd214))&rpoint(Vd216))))),
% 15.69/2.66 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 15.69/2.66 fof(f456,plain,(
% 15.69/2.66 ![Vd214]: ((![Vd215]: (~Vd214=Vd215|~rcircle(Vd215)))|(?[Vd216]: ((~ron(Vd216,Vd214)&~rinside(Vd216,Vd214))&rpoint(Vd216))))),
% 15.69/2.66 inference(miniscoping,[status(thm)],[f455])).
% 15.69/2.66 fof(f457,plain,(
% 15.69/2.66 ![Vd214]: ((![Vd215]: (~Vd214=Vd215|~rcircle(Vd215)))|((~ron(sK19_skl(Vd214),Vd214)&~rinside(sK19_skl(Vd214),Vd214))&rpoint(sK19_skl(Vd214))))),
% 15.69/2.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl]),skolemize(Vd216,sK19_skl(Vd214))],[f456])).
% 15.69/2.66 fof(f460,plain,(
% 15.69/2.66 ![X0,X1]: (~X0=X1|~rcircle(X1)|rpoint(sK19_skl(X0)))),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f457])).
% 15.69/2.66 fof(f461,plain,(
% 15.69/2.66 ![Vd211,Vd212]: ((~Vd211=Vd212|~rcircle(Vd212))|(?[Vd213]: (rinside(Vd213,Vd211)&rpoint(Vd213))))),
% 15.69/2.66 inference(pre_NNF_transformation,[status(thm)],[f94])).
% 15.69/2.66 fof(f462,plain,(
% 15.69/2.66 ![Vd211]: ((![Vd212]: (~Vd211=Vd212|~rcircle(Vd212)))|(?[Vd213]: (rinside(Vd213,Vd211)&rpoint(Vd213))))),
% 15.69/2.66 inference(miniscoping,[status(thm)],[f461])).
% 15.69/2.66 fof(f463,plain,(
% 15.69/2.66 ![Vd211]: ((![Vd212]: (~Vd211=Vd212|~rcircle(Vd212)))|(rinside(sK20_skl(Vd211),Vd211)&rpoint(sK20_skl(Vd211))))),
% 15.69/2.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(Vd213,sK20_skl(Vd211))],[f462])).
% 15.69/2.66 fof(f465,plain,(
% 15.69/2.66 ![X0,X1]: (~X0=X1|~rcircle(X1)|rpoint(sK20_skl(X0)))),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f463])).
% 15.69/2.66 fof(f479,plain,(
% 15.69/2.66 ![Vd191,Vd192]: ((~Vd191=Vd192|~rcircle(Vd192))|(?[Vd193]: (ron(Vd193,Vd191)&rpoint(Vd193))))),
% 15.69/2.66 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 15.69/2.66 fof(f480,plain,(
% 15.69/2.66 ![Vd191]: ((![Vd192]: (~Vd191=Vd192|~rcircle(Vd192)))|(?[Vd193]: (ron(Vd193,Vd191)&rpoint(Vd193))))),
% 15.69/2.66 inference(miniscoping,[status(thm)],[f479])).
% 15.69/2.66 fof(f481,plain,(
% 15.69/2.66 ![Vd191]: ((![Vd192]: (~Vd191=Vd192|~rcircle(Vd192)))|(ron(sK23_skl(Vd191),Vd191)&rpoint(sK23_skl(Vd191))))),
% 15.69/2.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(Vd193,sK23_skl(Vd191))],[f480])).
% 15.69/2.66 fof(f483,plain,(
% 15.69/2.66 ![X0,X1]: (~X0=X1|~rcircle(X1)|rpoint(sK23_skl(X0)))),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f481])).
% 15.69/2.66 fof(f559,plain,(
% 15.69/2.66 ![Vd52,Vd53]: ((~Vd52=Vd53|~rline(Vd53))|(?[Vd54]: (ron(Vd54,Vd52)&rpoint(Vd54))))),
% 15.69/2.66 inference(pre_NNF_transformation,[status(thm)],[f110])).
% 15.69/2.66 fof(f560,plain,(
% 15.69/2.66 ![Vd52]: ((![Vd53]: (~Vd52=Vd53|~rline(Vd53)))|(?[Vd54]: (ron(Vd54,Vd52)&rpoint(Vd54))))),
% 15.69/2.66 inference(miniscoping,[status(thm)],[f559])).
% 15.69/2.66 fof(f561,plain,(
% 15.69/2.66 ![Vd52]: ((![Vd53]: (~Vd52=Vd53|~rline(Vd53)))|(ron(sK36_skl(Vd52),Vd52)&rpoint(sK36_skl(Vd52))))),
% 15.69/2.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl]),skolemize(Vd54,sK36_skl(Vd52))],[f560])).
% 15.69/2.66 fof(f563,plain,(
% 15.69/2.66 ![X0,X1]: (~X0=X1|~rline(X1)|rpoint(sK36_skl(X0)))),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f561])).
% 15.69/2.66 fof(f582,plain,(
% 15.69/2.66 ![Vd15,Vd16]: ((~Vd15=Vd16|~rpoint(Vd16))|(?[Vd17]: (~Vd17=Vd15&rpoint(Vd17))))),
% 15.69/2.66 inference(pre_NNF_transformation,[status(thm)],[f114])).
% 15.69/2.66 fof(f583,plain,(
% 15.69/2.66 ![Vd15]: ((![Vd16]: (~Vd15=Vd16|~rpoint(Vd16)))|(?[Vd17]: (~Vd17=Vd15&rpoint(Vd17))))),
% 15.69/2.66 inference(miniscoping,[status(thm)],[f582])).
% 15.69/2.66 fof(f584,plain,(
% 15.69/2.66 ![Vd15]: ((![Vd16]: (~Vd15=Vd16|~rpoint(Vd16)))|(~sK40_skl(Vd15)=Vd15&rpoint(sK40_skl(Vd15))))),
% 15.69/2.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK40_skl]),skolemize(Vd17,sK40_skl(Vd15))],[f583])).
% 15.69/2.66 fof(f586,plain,(
% 15.69/2.66 ![X0,X1]: (~X0=X1|~rpoint(X1)|rpoint(sK40_skl(X0)))),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f584])).
% 15.69/2.66 fof(f587,plain,(
% 15.69/2.66 rpoint(vd14)),
% 15.69/2.66 inference(cnf_transformation,[status(thm)],[f115])).
% 15.69/2.66 fof(f874,plain,(
% 15.69/2.66 ![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(sK3_skl(X0,X3,X1,X2),X3,X0))),
% 15.69/2.66 inference(destructive_equality_resolution,[status(thm)],[f200])).
% 15.69/2.66 fof(f875,plain,(
% 15.69/2.66 ![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(sK3_skl(X0,X3,X1,X2),X2))),
% 15.69/2.66 inference(destructive_equality_resolution,[status(thm)],[f201])).
% 15.69/2.66 fof(f876,plain,(
% 15.69/2.66 ![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(sK3_skl(X0,X3,X1,X2),X1))),
% 15.69/2.66 inference(destructive_equality_resolution,[status(thm)],[f202])).
% 15.69/2.66 fof(f877,plain,(
% 15.69/2.66 ![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(sK3_skl(X0,X3,X1,X2)))),
% 15.69/2.66 inference(destructive_equality_resolution,[status(thm)],[f203])).
% 15.69/2.66 fof(f959,plain,(
% 15.69/2.66 ![X0]: (~rcircle(X0)|rpoint(sK19_skl(X0)))),
% 15.69/2.66 inference(destructive_equality_resolution,[status(thm)],[f460])).
% 15.69/2.66 fof(f961,plain,(
% 15.69/2.66 ![X0]: (~rcircle(X0)|rpoint(sK20_skl(X0)))),
% 15.69/2.66 inference(destructive_equality_resolution,[status(thm)],[f465])).
% 15.69/2.66 fof(f970,plain,(
% 15.69/2.66 ![X0]: (~rcircle(X0)|rpoint(sK23_skl(X0)))),
% 15.69/2.66 inference(destructive_equality_resolution,[status(thm)],[f483])).
% 15.69/2.66 fof(f1011,plain,(
% 15.69/2.66 ![X0]: (~rline(X0)|rpoint(sK36_skl(X0)))),
% 15.69/2.66 inference(destructive_equality_resolution,[status(thm)],[f563])).
% 15.69/2.66 fof(f1025,plain,(
% 15.69/2.66 ![X0]: (~rpoint(X0)|rpoint(sK40_skl(X0)))),
% 15.69/2.66 inference(destructive_equality_resolution,[status(thm)],[f586])).
% 15.69/2.66 fof(f1088,definition,(
% 15.69/2.66 sQ40_spl <=> (rline(vd1151))),
% 15.69/2.66 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 15.69/2.66 fof(f1090,plain,(
% 15.69/2.66 ~rline(vd1151)|sQ40_spl),
% 15.69/2.66 inference(component_clause,[status(thm)],[f1088])).
% 15.69/2.66 fof(f1091,definition,(
% 15.69/2.66 sQ41_spl <=> (rpoint(vd1123))),
% 15.69/2.66 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 15.69/2.66 fof(f1093,plain,(
% 15.69/2.66 ~rpoint(vd1123)|sQ41_spl),
% 15.69/2.66 inference(component_clause,[status(thm)],[f1091])).
% 15.69/2.66 fof(f1098,definition,(
% 15.69/2.66 sQ43_spl <=> (rpoint(vd1125))),
% 15.69/2.66 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 15.69/2.66 fof(f1100,plain,(
% 15.69/2.66 ~rpoint(vd1125)|sQ43_spl),
% 15.69/2.66 inference(component_clause,[status(thm)],[f1098])).
% 15.69/2.66 fof(f1112,plain,(
% 15.69/2.66 $false|sQ40_spl),
% 15.69/2.66 inference(forward_subsumption_resolution,[status(thm)],[f1090,f172])).
% 15.69/2.66 fof(f1113,plain,(
% 15.69/2.66 sQ40_spl),
% 15.69/2.66 inference(contradiction_clause,[status(thm)],[f1112])).
% 15.69/2.66 fof(f1115,plain,(
% 15.69/2.66 vd1123=vd1130),
% 15.69/2.66 inference(forward_demodulation,[status(thm)],[f146,f150])).
% 15.69/2.66 fof(f1116,plain,(
% 15.69/2.66 rpoint(vd1123)),
% 15.69/2.66 inference(forward_demodulation,[status(thm)],[f1115,f151])).
% 15.69/2.66 fof(f1117,plain,(
% 15.69/2.66 rpoint(vd1127)),
% 15.69/2.66 inference(forward_demodulation,[status(thm)],[f152,f153])).
% 15.69/2.66 fof(f1135,plain,(
% 15.69/2.66 $false|sQ41_spl),
% 15.69/2.66 inference(forward_subsumption_resolution,[status(thm)],[f1093,f1116])).
% 15.69/2.66 fof(f1136,plain,(
% 15.69/2.66 sQ41_spl),
% 15.69/2.66 inference(contradiction_clause,[status(thm)],[f1135])).
% 15.69/2.66 fof(f1137,plain,(
% 15.69/2.66 rpoint(vd1125)),
% 15.69/2.66 inference(forward_demodulation,[status(thm)],[f154,f155])).
% 15.69/2.66 fof(f1172,plain,(
% 15.69/2.66 $false|sQ43_spl),
% 15.69/2.66 inference(forward_subsumption_resolution,[status(thm)],[f1100,f1137])).
% 15.69/2.66 fof(f1173,plain,(
% 15.69/2.66 sQ43_spl),
% 15.69/2.66 inference(contradiction_clause,[status(thm)],[f1172])).
% 15.69/2.66 fof(f1231,definition,(
% 15.69/2.66 sQ66_spl <=> (ron(vd1125,vd1152))),
% 15.69/2.66 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 15.69/2.66 fof(f1232,plain,(
% 15.69/2.66 ron(vd1125,vd1152)|~sQ66_spl),
% 15.69/2.66 inference(component_clause,[status(thm)],[f1231])).
% 15.69/2.66 fof(f1321,plain,(
% 15.69/2.66 rinside(vd1123,vd1152)),
% 15.69/2.66 inference(resolution,[status(thm)],[f409,f142])).
% 15.69/2.66 fof(f1330,definition,(
% 15.69/2.66 sQ84_spl <=> (rcircle(vd1152))),
% 15.69/2.66 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 15.69/2.66 fof(f1332,plain,(
% 15.69/2.66 ~rcircle(vd1152)|sQ84_spl),
% 15.69/2.66 inference(component_clause,[status(thm)],[f1330])).
% 15.69/2.66 fof(f1342,plain,(
% 15.69/2.66 $false|sQ84_spl),
% 15.69/2.66 inference(forward_subsumption_resolution,[status(thm)],[f1332,f143])).
% 15.69/2.66 fof(f1343,plain,(
% 15.69/2.66 sQ84_spl),
% 15.69/2.66 inference(contradiction_clause,[status(thm)],[f1342])).
% 15.69/2.66 fof(f1375,plain,(
% 15.69/2.66 rpoint(sK19_skl(vd1152))),
% 15.69/2.66 inference(resolution,[status(thm)],[f959,f143])).
% 15.69/2.66 fof(f1388,plain,(
% 15.69/2.66 rpoint(sK20_skl(vd1152))),
% 15.69/2.66 inference(resolution,[status(thm)],[f961,f143])).
% 15.69/2.66 fof(f1390,plain,(
% 15.69/2.66 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~rpoint(vd1125)|~ron(X1,vd1151)|~rinside(X1,X0)|~rpoint(X1)|~rline(vd1151)|~rcircle(X0)|rR(sK3_skl(vd1125,X1,vd1151,X0),X1,vd1125))),
% 15.69/2.66 inference(resolution,[status(thm)],[f874,f144])).
% 15.69/2.66 fof(f1396,definition,(
% 15.69/2.66 ![X0,X1]: (sQ97_spl <=> (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1151)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|rR(sK3_skl(vd1125,X1,vd1151,X0),X1,vd1125)))),
% 15.69/2.66 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 15.69/2.66 fof(f1397,plain,(
% 15.69/2.66 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1151)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|rR(sK3_skl(vd1125,X1,vd1151,X0),X1,vd1125)|~sQ97_spl)),
% 15.69/2.66 inference(component_clause,[status(thm)],[f1396])).
% 15.69/2.66 fof(f1399,plain,(
% 15.69/2.66 sQ97_spl|~sQ43_spl|~sQ40_spl),
% 15.69/2.66 inference(split_clause,[status(thm)],[f1390,f1396,f1098,f1088])).
% 15.69/2.66 fof(f1405,plain,(
% 15.69/2.66 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~rpoint(vd1125)|~ron(X1,vd1151)|~rinside(X1,X0)|~rpoint(X1)|~rline(vd1151)|~rcircle(X0)|ron(sK3_skl(vd1125,X1,vd1151,X0),X0))),
% 15.69/2.66 inference(resolution,[status(thm)],[f875,f144])).
% 15.69/2.66 fof(f1411,definition,(
% 15.69/2.66 ![X0,X1]: (sQ100_spl <=> (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1151)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|ron(sK3_skl(vd1125,X1,vd1151,X0),X0)))),
% 15.69/2.66 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 15.69/2.66 fof(f1412,plain,(
% 15.69/2.66 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1151)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|ron(sK3_skl(vd1125,X1,vd1151,X0),X0)|~sQ100_spl)),
% 15.69/2.66 inference(component_clause,[status(thm)],[f1411])).
% 15.69/2.66 fof(f1414,plain,(
% 15.69/2.66 sQ100_spl|~sQ43_spl|~sQ40_spl),
% 15.69/2.66 inference(split_clause,[status(thm)],[f1405,f1411,f1098,f1088])).
% 15.69/2.66 fof(f1435,definition,(
% 15.69/2.66 sQ105_spl <=> (ron(vd1123,vd1151))),
% 15.69/2.66 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 15.69/2.66 fof(f1437,plain,(
% 15.69/2.66 ~ron(vd1123,vd1151)|sQ105_spl),
% 15.69/2.66 inference(component_clause,[status(thm)],[f1435])).
% 15.69/2.66 fof(f1442,plain,(
% 15.69/2.66 $false|sQ105_spl),
% 15.69/2.66 inference(forward_subsumption_resolution,[status(thm)],[f1437,f145])).
% 15.69/2.66 fof(f1443,plain,(
% 15.69/2.66 sQ105_spl),
% 15.69/2.66 inference(contradiction_clause,[status(thm)],[f1442])).
% 15.69/2.66 fof(f1499,plain,(
% 15.69/2.66 ron(vd1125,vd1152)|rinside(vd1125,vd1152)|~ron(vd1123,vd1151)|~rpoint(vd1123)|~rcircle(vd1152)|rR(sK3_skl(vd1125,vd1123,vd1151,vd1152),vd1123,vd1125)|~sQ97_spl),
% 15.69/2.66 inference(resolution,[status(thm)],[f1397,f1321])).
% 15.69/2.66 fof(f1500,definition,(
% 15.69/2.66 sQ114_spl <=> (rinside(vd1125,vd1152))),
% 15.69/2.66 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 15.69/2.66 fof(f1501,plain,(
% 15.69/2.66 rinside(vd1125,vd1152)|~sQ114_spl),
% 15.69/2.66 inference(component_clause,[status(thm)],[f1500])).
% 15.69/2.66 fof(f1503,definition,(
% 15.69/2.66 sQ115_spl <=> (rR(sK3_skl(vd1125,vd1123,vd1151,vd1152),vd1123,vd1125))),
% 15.69/2.66 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 15.69/2.66 fof(f1504,plain,(
% 15.69/2.66 rR(sK3_skl(vd1125,vd1123,vd1151,vd1152),vd1123,vd1125)|~sQ115_spl),
% 15.69/2.66 inference(component_clause,[status(thm)],[f1503])).
% 15.69/2.66 fof(f1506,plain,(
% 15.69/2.66 sQ66_spl|sQ114_spl|~sQ105_spl|~sQ41_spl|~sQ84_spl|sQ115_spl|~sQ97_spl),
% 15.69/2.66 inference(split_clause,[status(thm)],[f1499,f1231,f1500,f1435,f1091,f1330,f1503,f1396])).
% 15.69/2.66 fof(f1507,plain,(
% 15.69/2.66 $false|~sQ66_spl),
% 15.69/2.66 inference(forward_subsumption_resolution,[status(thm)],[f1232,f139])).
% 15.69/2.66 fof(f1508,plain,(
% 15.69/2.66 ~sQ66_spl),
% 15.69/2.66 inference(contradiction_clause,[status(thm)],[f1507])).
% 15.69/2.66 fof(f1509,plain,(
% 15.69/2.66 $false|~sQ114_spl),
% 15.69/2.66 inference(forward_subsumption_resolution,[status(thm)],[f1501,f140])).
% 15.69/2.66 fof(f1510,plain,(
% 15.69/2.66 ~sQ114_spl),
% 15.69/2.66 inference(contradiction_clause,[status(thm)],[f1509])).
% 15.69/2.66 fof(f1589,plain,(
% 15.69/2.66 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~rpoint(vd1125)|~ron(X1,vd1151)|~rinside(X1,X0)|~rpoint(X1)|~rline(vd1151)|~rcircle(X0)|ron(sK3_skl(vd1125,X1,vd1151,X0),vd1151))),
% 15.69/2.66 inference(resolution,[status(thm)],[f876,f144])).
% 15.69/2.66 fof(f1595,definition,(
% 15.69/2.66 ![X0,X1]: (sQ132_spl <=> (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1151)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|ron(sK3_skl(vd1125,X1,vd1151,X0),vd1151)))),
% 15.69/2.66 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 15.69/2.66 fof(f1596,plain,(
% 15.69/2.66 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1151)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|ron(sK3_skl(vd1125,X1,vd1151,X0),vd1151)|~sQ132_spl)),
% 15.69/2.66 inference(component_clause,[status(thm)],[f1595])).
% 15.69/2.66 fof(f1598,plain,(
% 15.69/2.66 sQ132_spl|~sQ43_spl|~sQ40_spl),
% 15.69/2.66 inference(split_clause,[status(thm)],[f1589,f1595,f1098,f1088])).
% 15.69/2.66 fof(f1604,plain,(
% 15.69/2.66 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~rpoint(vd1125)|~ron(X1,vd1151)|~rinside(X1,X0)|~rpoint(X1)|~rline(vd1151)|~rcircle(X0)|rpoint(sK3_skl(vd1125,X1,vd1151,X0)))),
% 15.69/2.66 inference(resolution,[status(thm)],[f877,f144])).
% 15.69/2.66 fof(f1610,definition,(
% 15.69/2.66 ![X0,X1]: (sQ135_spl <=> (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1151)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|rpoint(sK3_skl(vd1125,X1,vd1151,X0))))),
% 14.63/2.67 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 14.63/2.67 fof(f1611,plain,(
% 14.63/2.67 ![X0,X1]: (ron(vd1125,X0)|rinside(vd1125,X0)|~ron(X1,vd1151)|~rinside(X1,X0)|~rpoint(X1)|~rcircle(X0)|rpoint(sK3_skl(vd1125,X1,vd1151,X0))|~sQ135_spl)),
% 14.63/2.67 inference(component_clause,[status(thm)],[f1610])).
% 14.63/2.67 fof(f1613,plain,(
% 14.63/2.67 sQ135_spl|~sQ43_spl|~sQ40_spl),
% 14.63/2.67 inference(split_clause,[status(thm)],[f1604,f1610,f1098,f1088])).
% 14.63/2.67 fof(f1654,plain,(
% 14.63/2.67 ron(vd1125,vd1152)|rinside(vd1125,vd1152)|~ron(vd1123,vd1151)|~rpoint(vd1123)|~rcircle(vd1152)|ron(sK3_skl(vd1125,vd1123,vd1151,vd1152),vd1152)|~sQ100_spl),
% 14.63/2.67 inference(resolution,[status(thm)],[f1412,f1321])).
% 14.63/2.67 fof(f1655,definition,(
% 14.63/2.67 sQ141_spl <=> (ron(sK3_skl(vd1125,vd1123,vd1151,vd1152),vd1152))),
% 14.63/2.67 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 14.63/2.67 fof(f1658,plain,(
% 14.63/2.67 sQ66_spl|sQ114_spl|~sQ105_spl|~sQ41_spl|~sQ84_spl|sQ141_spl|~sQ100_spl),
% 14.63/2.67 inference(split_clause,[status(thm)],[f1654,f1231,f1500,f1435,f1091,f1330,f1655,f1411])).
% 14.63/2.67 fof(f1664,plain,(
% 14.63/2.67 rpoint(sK23_skl(vd1152))),
% 14.63/2.67 inference(resolution,[status(thm)],[f970,f143])).
% 14.63/2.67 fof(f1678,plain,(
% 14.63/2.67 rpoint(sK36_skl(vd1151))),
% 14.63/2.67 inference(resolution,[status(thm)],[f1011,f172])).
% 14.63/2.67 fof(f1716,plain,(
% 14.63/2.67 ron(vd1125,vd1152)|rinside(vd1125,vd1152)|~ron(vd1123,vd1151)|~rpoint(vd1123)|~rcircle(vd1152)|ron(sK3_skl(vd1125,vd1123,vd1151,vd1152),vd1151)|~sQ132_spl),
% 14.63/2.67 inference(resolution,[status(thm)],[f1596,f1321])).
% 14.63/2.67 fof(f1717,definition,(
% 14.63/2.67 sQ147_spl <=> (ron(sK3_skl(vd1125,vd1123,vd1151,vd1152),vd1151))),
% 14.63/2.67 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 14.63/2.67 fof(f1720,plain,(
% 14.63/2.67 sQ66_spl|sQ114_spl|~sQ105_spl|~sQ41_spl|~sQ84_spl|sQ147_spl|~sQ132_spl),
% 14.63/2.67 inference(split_clause,[status(thm)],[f1716,f1231,f1500,f1435,f1091,f1330,f1717,f1595])).
% 14.63/2.67 fof(f1726,plain,(
% 14.63/2.67 ron(vd1125,vd1152)|rinside(vd1125,vd1152)|~ron(vd1123,vd1151)|~rpoint(vd1123)|~rcircle(vd1152)|rpoint(sK3_skl(vd1125,vd1123,vd1151,vd1152))|~sQ135_spl),
% 14.63/2.67 inference(resolution,[status(thm)],[f1611,f1321])).
% 14.63/2.67 fof(f1727,definition,(
% 14.63/2.67 sQ149_spl <=> (rpoint(sK3_skl(vd1125,vd1123,vd1151,vd1152)))),
% 14.63/2.67 introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 14.63/2.67 fof(f1730,plain,(
% 14.63/2.67 sQ66_spl|sQ114_spl|~sQ105_spl|~sQ41_spl|~sQ84_spl|sQ149_spl|~sQ135_spl),
% 14.63/2.67 inference(split_clause,[status(thm)],[f1726,f1231,f1500,f1435,f1091,f1330,f1727,f1610])).
% 14.63/2.67 fof(f1735,plain,(
% 14.63/2.67 rpoint(sK40_skl(vd14))),
% 14.63/2.67 inference(resolution,[status(thm)],[f1025,f587])).
% 14.63/2.67 fof(f1736,plain,(
% 14.63/2.67 rpoint(sK40_skl(vd1125))),
% 14.63/2.67 inference(resolution,[status(thm)],[f1025,f1137])).
% 14.63/2.67 fof(f1737,plain,(
% 14.63/2.67 rpoint(sK40_skl(vd1127))),
% 14.63/2.67 inference(resolution,[status(thm)],[f1025,f1117])).
% 14.63/2.67 fof(f1738,plain,(
% 14.63/2.67 rpoint(sK40_skl(vd1123))),
% 14.63/2.67 inference(resolution,[status(thm)],[f1025,f1116])).
% 14.63/2.67 fof(f2221,definition,(
% 14.63/2.67 ![X0]: (sQ190_spl <=> (~vf(X0,vd1127)=vf(X0,vd1127)|~rcenter(X0,vd1152)|~rcenter(X0,vd1152)))),
% 14.63/2.67 introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition])).
% 14.63/2.67 fof(f2222,plain,(
% 14.63/2.67 ![X0]: (~vf(X0,vd1127)=vf(X0,vd1127)|~rcenter(X0,vd1152)|~rcenter(X0,vd1152)|~sQ190_spl)),
% 14.63/2.67 inference(component_clause,[status(thm)],[f2221])).
% 14.63/2.67 fof(f2228,plain,(
% 14.63/2.67 ![X0]: (~vf(X0,vd1127)=vf(X0,vd1127)|~rcenter(X0,vd1152)|~sQ190_spl)),
% 14.63/2.67 inference(duplicate_literals_removal,[status(thm)],[f2222])).
% 14.63/2.67 fof(f2229,plain,(
% 14.63/2.67 ![X0]: (~rcenter(X0,vd1152)|~sQ190_spl)),
% 14.63/2.67 inference(trivial_equality_resolution,[status(thm)],[f2228])).
% 14.63/2.67 fof(f2365,plain,(
% 14.63/2.67 $false|~sQ190_spl),
% 14.63/2.67 inference(backward_subsumption_resolution,[status(thm)],[f142,f2229])).
% 14.63/2.67 fof(f2366,plain,(
% 14.63/2.67 ~sQ190_spl),
% 14.63/2.67 inference(contradiction_clause,[status(thm)],[f2365])).
% 14.63/2.67 fof(f2848,definition,(
% 14.63/2.67 sQ245_spl <=> (rpoint(sK20_skl(vd1152)))),
% 14.63/2.67 introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition])).
% 14.63/2.67 fof(f2850,plain,(
% 14.63/2.67 ~rpoint(sK20_skl(vd1152))|sQ245_spl),
% 14.63/2.67 inference(component_clause,[status(thm)],[f2848])).
% 14.63/2.67 fof(f2907,plain,(
% 14.63/2.67 $false|sQ245_spl),
% 14.63/2.67 inference(forward_subsumption_resolution,[status(thm)],[f2850,f1388])).
% 14.63/2.67 fof(f2908,plain,(
% 14.63/2.67 sQ245_spl),
% 14.63/2.67 inference(contradiction_clause,[status(thm)],[f2907])).
% 14.63/2.67 fof(f3027,definition,(
% 14.63/2.67 sQ269_spl <=> (rpoint(sK23_skl(vd1152)))),
% 14.63/2.67 introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition])).
% 14.63/2.67 fof(f3029,plain,(
% 14.63/2.67 ~rpoint(sK23_skl(vd1152))|sQ269_spl),
% 14.63/2.67 inference(component_clause,[status(thm)],[f3027])).
% 14.63/2.67 fof(f3123,plain,(
% 14.63/2.67 $false|sQ269_spl),
% 14.63/2.67 inference(forward_subsumption_resolution,[status(thm)],[f3029,f1664])).
% 14.63/2.67 fof(f3124,plain,(
% 14.63/2.67 sQ269_spl),
% 14.63/2.67 inference(contradiction_clause,[status(thm)],[f3123])).
% 14.63/2.67 fof(f3297,definition,(
% 14.63/2.67 sQ310_spl <=> (rpoint(sK36_skl(vd1151)))),
% 14.63/2.67 introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition])).
% 14.63/2.67 fof(f3299,plain,(
% 14.63/2.67 ~rpoint(sK36_skl(vd1151))|sQ310_spl),
% 14.63/2.67 inference(component_clause,[status(thm)],[f3297])).
% 14.63/2.67 fof(f3416,plain,(
% 14.63/2.67 $false|sQ310_spl),
% 14.63/2.67 inference(forward_subsumption_resolution,[status(thm)],[f3299,f1678])).
% 14.63/2.67 fof(f3417,plain,(
% 14.63/2.67 sQ310_spl),
% 14.63/2.67 inference(contradiction_clause,[status(thm)],[f3416])).
% 14.63/2.67 fof(f3918,definition,(
% 14.63/2.67 sQ411_spl <=> (rpoint(vd14))),
% 14.63/2.67 introduced(definition,[new_symbols(definition,[sQ411_spl])],[split_symbol_definition])).
% 14.63/2.67 fof(f3920,plain,(
% 14.63/2.67 ~rpoint(vd14)|sQ411_spl),
% 14.63/2.67 inference(component_clause,[status(thm)],[f3918])).
% 14.63/2.67 fof(f3942,plain,(
% 14.63/2.67 $false|sQ411_spl),
% 14.63/2.67 inference(forward_subsumption_resolution,[status(thm)],[f3920,f587])).
% 14.63/2.67 fof(f3943,plain,(
% 14.63/2.67 sQ411_spl),
% 14.63/2.67 inference(contradiction_clause,[status(thm)],[f3942])).
% 14.63/2.67 fof(f5555,definition,(
% 14.63/2.67 sQ726_spl <=> (rpoint(sK19_skl(vd1152)))),
% 14.63/2.67 introduced(definition,[new_symbols(definition,[sQ726_spl])],[split_symbol_definition])).
% 14.63/2.67 fof(f5557,plain,(
% 14.63/2.67 ~rpoint(sK19_skl(vd1152))|sQ726_spl),
% 14.63/2.67 inference(component_clause,[status(thm)],[f5555])).
% 14.63/2.67 fof(f5745,plain,(
% 14.63/2.67 $false|sQ726_spl),
% 14.63/2.67 inference(forward_subsumption_resolution,[status(thm)],[f5557,f1375])).
% 14.63/2.67 fof(f5746,plain,(
% 14.63/2.67 sQ726_spl),
% 14.63/2.67 inference(contradiction_clause,[status(thm)],[f5745])).
% 14.63/2.67 fof(f5799,definition,(
% 14.63/2.67 sQ775_spl <=> (rpoint(sK40_skl(vd14)))),
% 14.63/2.67 introduced(definition,[new_symbols(definition,[sQ775_spl])],[split_symbol_definition])).
% 14.63/2.67 fof(f5801,plain,(
% 14.63/2.67 ~rpoint(sK40_skl(vd14))|sQ775_spl),
% 14.63/2.67 inference(component_clause,[status(thm)],[f5799])).
% 14.63/2.67 fof(f5989,plain,(
% 14.63/2.67 $false|sQ775_spl),
% 14.63/2.67 inference(forward_subsumption_resolution,[status(thm)],[f5801,f1735])).
% 14.63/2.67 fof(f5990,plain,(
% 14.63/2.67 sQ775_spl),
% 14.63/2.67 inference(contradiction_clause,[status(thm)],[f5989])).
% 14.63/2.67 fof(f6080,definition,(
% 14.63/2.67 sQ832_spl <=> (rpoint(sK40_skl(vd1125)))),
% 14.63/2.67 introduced(definition,[new_symbols(definition,[sQ832_spl])],[split_symbol_definition])).
% 14.63/2.67 fof(f6082,plain,(
% 14.63/2.67 ~rpoint(sK40_skl(vd1125))|sQ832_spl),
% 14.63/2.67 inference(component_clause,[status(thm)],[f6080])).
% 14.63/2.67 fof(f6270,plain,(
% 14.63/2.67 $false|sQ832_spl),
% 14.63/2.67 inference(forward_subsumption_resolution,[status(thm)],[f6082,f1736])).
% 14.63/2.67 fof(f6271,plain,(
% 14.63/2.67 sQ832_spl),
% 14.63/2.67 inference(contradiction_clause,[status(thm)],[f6270])).
% 14.63/2.67 fof(f6366,definition,(
% 14.63/2.67 sQ889_spl <=> (rpoint(sK40_skl(vd1127)))),
% 14.63/2.67 introduced(definition,[new_symbols(definition,[sQ889_spl])],[split_symbol_definition])).
% 14.63/2.67 fof(f6368,plain,(
% 14.63/2.67 ~rpoint(sK40_skl(vd1127))|sQ889_spl),
% 14.63/2.67 inference(component_clause,[status(thm)],[f6366])).
% 14.63/2.67 fof(f6564,plain,(
% 14.63/2.67 $false|sQ889_spl),
% 14.63/2.67 inference(forward_subsumption_resolution,[status(thm)],[f6368,f1737])).
% 14.63/2.67 fof(f6565,plain,(
% 14.63/2.67 sQ889_spl),
% 14.63/2.67 inference(contradiction_clause,[status(thm)],[f6564])).
% 14.63/2.67 fof(f6625,definition,(
% 14.63/2.67 sQ941_spl <=> (rpoint(sK40_skl(vd1123)))),
% 14.63/2.67 introduced(definition,[new_symbols(definition,[sQ941_spl])],[split_symbol_definition])).
% 14.63/2.67 fof(f6627,plain,(
% 14.63/2.67 ~rpoint(sK40_skl(vd1123))|sQ941_spl),
% 14.63/2.67 inference(component_clause,[status(thm)],[f6625])).
% 14.63/2.67 fof(f6823,plain,(
% 14.63/2.67 $false|sQ941_spl),
% 14.63/2.67 inference(forward_subsumption_resolution,[status(thm)],[f6627,f1738])).
% 14.63/2.67 fof(f6824,plain,(
% 14.63/2.67 sQ941_spl),
% 14.63/2.67 inference(contradiction_clause,[status(thm)],[f6823])).
% 14.63/2.67 fof(f12196,plain,(
% 14.63/2.67 ~ron(sK3_skl(vd1125,vd1123,vd1151,vd1152),vd1152)|~ron(sK3_skl(vd1125,vd1123,vd1151,vd1152),vd1151)|~rpoint(sK3_skl(vd1125,vd1123,vd1151,vd1152))|~sQ115_spl),
% 14.63/2.68 inference(resolution,[status(thm)],[f1504,f138])).
% 14.63/2.68 fof(f12215,plain,(
% 14.63/2.68 ~sQ141_spl|~sQ147_spl|~sQ149_spl|~sQ115_spl),
% 14.63/2.68 inference(split_clause,[status(thm)],[f12196,f1655,f1717,f1727,f1503])).
% 14.63/2.68 fof(f12291,plain,(
% 14.63/2.68 $false),
% 14.63/2.68 inference(sat_refutation,[status(thm)],[f1113,f1136,f1173,f1343,f1399,f1414,f1443,f1506,f1508,f1510,f1598,f1613,f1658,f1720,f1730,f2366,f2908,f3124,f3417,f3943,f5746,f5990,f6271,f6565,f6824,f12215])).
% 14.63/2.68 % SZS output end CNFRefutation for theBenchmark.p
% 14.63/2.70 % Elapsed time: 2.224183 seconds
% 14.63/2.70 % CPU time: 16.849021 seconds
% 14.63/2.70 % Total memory used: 194.161 MB
% 14.63/2.70 % Net memory used: 187.829 MB
%------------------------------------------------------------------------------