%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO285+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 : n018.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 128.36s 16.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO285+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.09/0.35 % Computer : n018.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 15:08:29 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 128.36/16.69 % Refutation found
% 128.36/16.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 128.36/16.69 % SZS output start CNFRefutation for theBenchmark
% 128.36/16.69 fof(f1,conjecture,(
% 128.36/16.69 ~ rinside(vd1125,vd1152) ),
% 128.36/16.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 128.36/16.69 fof(f2,negated_conjecture,(
% 128.36/16.69 ~(~ rinside(vd1125,vd1152) )),
% 128.36/16.69 inference(negated_conjecture,[status(cth)],[f1])).
% 128.36/16.69 fof(f3,axiom,(
% 128.36/16.69 ( ron(vd1127,vd1152)& rcenter(vd1123,vd1152)& rcircle(vd1152)& ron(vd1125,vd1151)& ron(vd1123,vd1151) ) ),
% 128.36/16.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 128.36/16.69 fof(f5,axiom,(
% 128.36/16.69 vd1123 = vd1129 ),
% 128.36/16.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 128.36/16.69 fof(f15,axiom,(
% 128.36/16.69 ( 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) ) ),
% 128.36/16.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 128.36/16.69 fof(f19,axiom,(
% 128.36/16.69 (! [Vd854,Vd855,Vd859,Vd860] :( ( ron(Vd855,Vd860)& rcenter(Vd859,Vd860)& (? [Vd858] :( Vd855 = Vd858& rpoint(Vd858) ))& (? [Vd857] :( Vd854 = Vd857& rpoint(Vd857) ) ))=> ( rless(vf(Vd859,Vd854),vf(Vd859,Vd855))<=> rinside(Vd854,Vd860) ) ) )),
% 128.36/16.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 128.36/16.69 fof(f38,axiom,(
% 128.36/16.69 (! [Vd741,Vd742] :( ( (? [Vd745] :( Vd742 = Vd745& rpoint(Vd745) ))& (? [Vd744] :( Vd741 = Vd744& rpoint(Vd744) ) ))=> (? [Vd747] :( vf(Vd741,Vd742) = Vd747& rreal(Vd747) ) )) )),
% 128.36/16.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 128.36/16.69 fof(f39,axiom,(
% 128.36/16.69 (! [Vd713,Vd714] :( ( Vd713 = Vd714& rreal(Vd714) )=> ~ rless(Vd713,Vd713) ) )),
% 128.36/16.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 128.36/16.69 fof(f68,axiom,(
% 128.36/16.69 (! [Vd716,Vd717,Vd718,Vd719,Vd720,Vd721] :( ( rless(Vd718,Vd720)& rless(Vd716,Vd718)& Vd720 = Vd721& rreal(Vd721)& Vd718 = Vd719& rreal(Vd719)& Vd716 = Vd717& rreal(Vd717) )=> rless(Vd716,Vd720) ) )),
% 128.36/16.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 128.36/16.69 fof(f125,axiom,(
% 128.36/16.69 (! [Vd761,Vd762] :( ( (? [Vd765] :( Vd762 = Vd765& rpoint(Vd765) ))& (? [Vd764] :( Vd761 = Vd764& rpoint(Vd764) ) ))=> vf(Vd761,Vd762) = vf(Vd762,Vd761) ) )),
% 128.36/16.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 128.36/16.69 fof(f135,plain,(
% 128.36/16.69 rinside(vd1125,vd1152)),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f2])).
% 128.36/16.69 fof(f136,plain,(
% 128.36/16.69 ron(vd1127,vd1152)),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f3])).
% 128.36/16.69 fof(f137,plain,(
% 128.36/16.69 rcenter(vd1123,vd1152)),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f3])).
% 128.36/16.69 fof(f142,plain,(
% 128.36/16.69 vd1123=vd1129),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f5])).
% 128.36/16.69 fof(f165,plain,(
% 128.36/16.69 rless(vf(vd1127,vd1129),vf(vd1123,vd1125))),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f15])).
% 128.36/16.69 fof(f168,plain,(
% 128.36/16.69 vd1129=vd1130),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f15])).
% 128.36/16.69 fof(f169,plain,(
% 128.36/16.69 rpoint(vd1130)),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f15])).
% 128.36/16.69 fof(f170,plain,(
% 128.36/16.69 vd1127=vd1128),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f15])).
% 128.36/16.69 fof(f171,plain,(
% 128.36/16.69 rpoint(vd1128)),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f15])).
% 128.36/16.69 fof(f172,plain,(
% 128.36/16.69 vd1125=vd1126),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f15])).
% 128.36/16.69 fof(f173,plain,(
% 128.36/16.69 rpoint(vd1126)),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f15])).
% 128.36/16.69 fof(f193,plain,(
% 128.36/16.69 ![Vd854,Vd855,Vd859,Vd860]: ((((~ron(Vd855,Vd860)|~rcenter(Vd859,Vd860))|(![Vd858]: (~Vd855=Vd858|~rpoint(Vd858))))|(![Vd857]: (~Vd854=Vd857|~rpoint(Vd857))))|(rless(vf(Vd859,Vd854),vf(Vd859,Vd855))<=>rinside(Vd854,Vd860)))),
% 128.36/16.69 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 128.36/16.69 fof(f194,plain,(
% 128.36/16.69 ![Vd854,Vd855,Vd859,Vd860]: ((((~ron(Vd855,Vd860)|~rcenter(Vd859,Vd860))|(![Vd858]: (~Vd855=Vd858|~rpoint(Vd858))))|(![Vd857]: (~Vd854=Vd857|~rpoint(Vd857))))|((~rless(vf(Vd859,Vd854),vf(Vd859,Vd855))|rinside(Vd854,Vd860))&(rless(vf(Vd859,Vd854),vf(Vd859,Vd855))|~rinside(Vd854,Vd860))))),
% 128.36/16.69 inference(NNF_transformation,[status(thm)],[f193])).
% 128.36/16.69 fof(f196,plain,(
% 128.36/16.69 ![X0,X1,X2,X3,X4,X5]: (~ron(X0,X1)|~rcenter(X2,X1)|~X0=X3|~rpoint(X3)|~X4=X5|~rpoint(X5)|rless(vf(X2,X4),vf(X2,X0))|~rinside(X4,X1))),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f194])).
% 128.36/16.69 fof(f257,plain,(
% 128.36/16.69 ![Vd741,Vd742]: (((![Vd745]: (~Vd742=Vd745|~rpoint(Vd745)))|(![Vd744]: (~Vd741=Vd744|~rpoint(Vd744))))|(?[Vd747]: (vf(Vd741,Vd742)=Vd747&rreal(Vd747))))),
% 128.36/16.69 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 128.36/16.69 fof(f258,plain,(
% 128.36/16.69 ![Vd741,Vd742]: (((![Vd745]: (~Vd742=Vd745|~rpoint(Vd745)))|(![Vd744]: (~Vd741=Vd744|~rpoint(Vd744))))|(vf(Vd741,Vd742)=sK7_skl(Vd742,Vd741)&rreal(sK7_skl(Vd742,Vd741))))),
% 128.36/16.69 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Vd747,sK7_skl(Vd742,Vd741))],[f257])).
% 128.36/16.69 fof(f259,plain,(
% 128.36/16.69 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|vf(X2,X0)=sK7_skl(X0,X2))),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f258])).
% 128.36/16.69 fof(f260,plain,(
% 128.36/16.69 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|rreal(sK7_skl(X0,X2)))),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f258])).
% 128.36/16.69 fof(f261,plain,(
% 128.36/16.69 ![Vd713,Vd714]: ((~Vd713=Vd714|~rreal(Vd714))|~rless(Vd713,Vd713))),
% 128.36/16.69 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 128.36/16.69 fof(f262,plain,(
% 128.36/16.69 ![Vd713]: ((![Vd714]: (~Vd713=Vd714|~rreal(Vd714)))|~rless(Vd713,Vd713))),
% 128.36/16.69 inference(miniscoping,[status(thm)],[f261])).
% 128.36/16.69 fof(f263,plain,(
% 128.36/16.69 ![X0,X1]: (~X0=X1|~rreal(X1)|~rless(X0,X0))),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f262])).
% 128.36/16.69 fof(f381,plain,(
% 128.36/16.69 ![Vd716,Vd717,Vd718,Vd719,Vd720,Vd721]: ((((((((~rless(Vd718,Vd720)|~rless(Vd716,Vd718))|~Vd720=Vd721)|~rreal(Vd721))|~Vd718=Vd719)|~rreal(Vd719))|~Vd716=Vd717)|~rreal(Vd717))|rless(Vd716,Vd720))),
% 128.36/16.69 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 128.36/16.69 fof(f382,plain,(
% 128.36/16.69 ![Vd716,Vd720]: ((![Vd717]: (((![Vd719]: ((![Vd718]: ((![Vd721]: (((~rless(Vd718,Vd720)|~rless(Vd716,Vd718))|~Vd720=Vd721)|~rreal(Vd721)))|~Vd718=Vd719))|~rreal(Vd719)))|~Vd716=Vd717)|~rreal(Vd717)))|rless(Vd716,Vd720))),
% 128.36/16.69 inference(miniscoping,[status(thm)],[f381])).
% 128.36/16.69 fof(f383,plain,(
% 128.36/16.69 ![X0,X1,X2,X3,X4,X5]: (~rless(X0,X1)|~rless(X2,X0)|~X1=X3|~rreal(X3)|~X0=X4|~rreal(X4)|~X2=X5|~rreal(X5)|rless(X2,X1))),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f382])).
% 128.36/16.69 fof(f636,plain,(
% 128.36/16.69 ![Vd761,Vd762]: (((![Vd765]: (~Vd762=Vd765|~rpoint(Vd765)))|(![Vd764]: (~Vd761=Vd764|~rpoint(Vd764))))|vf(Vd761,Vd762)=vf(Vd762,Vd761))),
% 128.36/16.69 inference(pre_NNF_transformation,[status(thm)],[f125])).
% 128.36/16.69 fof(f637,plain,(
% 128.36/16.69 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|vf(X2,X0)=vf(X0,X2))),
% 128.36/16.69 inference(cnf_transformation,[status(thm)],[f636])).
% 128.36/16.69 fof(f851,plain,(
% 128.36/16.69 rcenter(vd1129,vd1152)),
% 128.36/16.69 inference(backward_demodulation,[status(thm)],[f142,f137])).
% 128.36/16.69 fof(f852,plain,(
% 128.36/16.69 rless(vf(vd1127,vd1129),vf(vd1129,vd1125))),
% 128.36/16.69 inference(forward_demodulation,[status(thm)],[f142,f165])).
% 128.36/16.69 fof(f856,plain,(
% 128.36/16.69 rless(vf(vd1127,vd1129),vf(vd1130,vd1125))),
% 128.36/16.69 inference(backward_demodulation,[status(thm)],[f168,f852])).
% 128.36/16.69 fof(f858,plain,(
% 128.36/16.69 ron(vd1128,vd1152)),
% 128.36/16.69 inference(backward_demodulation,[status(thm)],[f170,f136])).
% 128.36/16.69 fof(f860,plain,(
% 128.36/16.69 rinside(vd1126,vd1152)),
% 128.36/16.69 inference(backward_demodulation,[status(thm)],[f172,f135])).
% 128.36/16.69 fof(f868,plain,(
% 128.36/16.69 ![X0,X1,X2,X3]: (~ron(X0,X1)|~rcenter(X2,X1)|~rpoint(X0)|~rpoint(X3)|rless(vf(X2,X3),vf(X2,X0))|~rinside(X3,X1))),
% 128.36/16.69 inference(destructive_equality_resolution,[status(thm)],[f196])).
% 128.36/16.69 fof(f887,plain,(
% 128.36/16.69 ![X0,X1]: (~rpoint(X0)|~rpoint(X1)|vf(X1,X0)=sK7_skl(X0,X1))),
% 128.36/16.69 inference(destructive_equality_resolution,[status(thm)],[f259])).
% 128.36/16.69 fof(f888,plain,(
% 128.36/16.69 ![X0,X1]: (~rpoint(X0)|~rpoint(X1)|rreal(sK7_skl(X0,X1)))),
% 128.36/16.69 inference(destructive_equality_resolution,[status(thm)],[f260])).
% 128.36/16.69 fof(f889,plain,(
% 128.36/16.69 ![X0]: (~rreal(X0)|~rless(X0,X0))),
% 128.36/16.69 inference(destructive_equality_resolution,[status(thm)],[f263])).
% 128.36/16.69 fof(f942,plain,(
% 128.36/16.69 ![X0,X1,X2]: (~rless(X0,X1)|~rless(X2,X0)|~rreal(X1)|~rreal(X0)|~rreal(X2)|rless(X2,X1))),
% 128.36/16.69 inference(destructive_equality_resolution,[status(thm)],[f383])).
% 128.36/16.69 fof(f1071,plain,(
% 128.36/16.69 ![X0,X1]: (~rpoint(X0)|~rpoint(X1)|vf(X1,X0)=vf(X0,X1))),
% 128.36/16.69 inference(destructive_equality_resolution,[status(thm)],[f637])).
% 128.36/16.69 fof(f1110,plain,(
% 128.36/16.69 rcenter(vd1130,vd1152)),
% 128.36/16.69 inference(forward_demodulation,[status(thm)],[f168,f851])).
% 128.36/16.69 fof(f1113,plain,(
% 128.36/16.69 rless(vf(vd1128,vd1129),vf(vd1130,vd1125))),
% 128.36/16.69 inference(forward_demodulation,[status(thm)],[f170,f856])).
% 128.36/16.69 fof(f1114,plain,(
% 128.36/16.69 rless(vf(vd1128,vd1130),vf(vd1130,vd1125))),
% 128.36/16.69 inference(forward_demodulation,[status(thm)],[f168,f1113])).
% 128.36/16.69 fof(f1115,plain,(
% 128.36/16.69 rless(vf(vd1128,vd1130),vf(vd1130,vd1126))),
% 128.36/16.69 inference(forward_demodulation,[status(thm)],[f172,f1114])).
% 128.36/16.69 fof(f1255,plain,(
% 128.36/16.69 ![X0]: (~rpoint(X0)|vf(vd1128,X0)=sK7_skl(X0,vd1128))),
% 128.36/16.69 inference(resolution,[status(thm)],[f887,f171])).
% 128.36/16.69 fof(f1256,plain,(
% 128.36/16.69 ![X0]: (~rpoint(X0)|vf(vd1130,X0)=sK7_skl(X0,vd1130))),
% 128.36/16.69 inference(resolution,[status(thm)],[f887,f169])).
% 128.36/16.69 fof(f1274,definition,(
% 128.36/16.69 sQ63_spl <=> (rless(vf(vd1130,vd1126),vf(vd1128,vd1130)))),
% 128.36/16.69 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 128.36/16.69 fof(f1276,plain,(
% 128.36/16.69 ~rless(vf(vd1130,vd1126),vf(vd1128,vd1130))|sQ63_spl),
% 128.36/16.69 inference(component_clause,[status(thm)],[f1274])).
% 128.36/16.69 fof(f1277,definition,(
% 128.36/16.69 sQ64_spl <=> (rreal(vf(vd1128,vd1130)))),
% 128.36/16.69 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 128.36/16.69 fof(f1280,definition,(
% 128.36/16.69 sQ65_spl <=> (rreal(vf(vd1130,vd1126)))),
% 128.36/16.69 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 128.36/16.69 fof(f3653,definition,(
% 128.36/16.69 sQ370_spl <=> (rpoint(vd1128))),
% 128.36/16.69 introduced(definition,[new_symbols(definition,[sQ370_spl])],[split_symbol_definition])).
% 128.36/16.69 fof(f3655,plain,(
% 128.36/16.69 ~rpoint(vd1128)|sQ370_spl),
% 128.36/16.69 inference(component_clause,[status(thm)],[f3653])).
% 128.36/16.69 fof(f3656,definition,(
% 128.36/16.69 sQ371_spl <=> (rpoint(vd1126))),
% 128.36/16.69 introduced(definition,[new_symbols(definition,[sQ371_spl])],[split_symbol_definition])).
% 128.36/16.69 fof(f3658,plain,(
% 128.36/16.69 ~rpoint(vd1126)|sQ371_spl),
% 128.36/16.69 inference(component_clause,[status(thm)],[f3656])).
% 128.36/16.69 fof(f3680,definition,(
% 128.36/16.69 sQ378_spl <=> (rpoint(vd1130))),
% 128.36/16.69 introduced(definition,[new_symbols(definition,[sQ378_spl])],[split_symbol_definition])).
% 128.36/16.69 fof(f3682,plain,(
% 128.36/16.69 ~rpoint(vd1130)|sQ378_spl),
% 128.36/16.69 inference(component_clause,[status(thm)],[f3680])).
% 128.36/16.69 fof(f3689,plain,(
% 128.36/16.69 $false|sQ370_spl),
% 128.36/16.69 inference(forward_subsumption_resolution,[status(thm)],[f3655,f171])).
% 128.36/16.69 fof(f3690,plain,(
% 128.36/16.69 sQ370_spl),
% 128.36/16.69 inference(contradiction_clause,[status(thm)],[f3689])).
% 128.36/16.69 fof(f3916,plain,(
% 128.36/16.69 $false|sQ378_spl),
% 128.36/16.69 inference(forward_subsumption_resolution,[status(thm)],[f3682,f169])).
% 128.36/16.69 fof(f3917,plain,(
% 128.36/16.69 sQ378_spl),
% 128.36/16.69 inference(contradiction_clause,[status(thm)],[f3916])).
% 128.36/16.69 fof(f4328,plain,(
% 128.36/16.69 $false|sQ371_spl),
% 128.36/16.69 inference(forward_subsumption_resolution,[status(thm)],[f3658,f173])).
% 128.36/16.69 fof(f4329,plain,(
% 128.36/16.69 sQ371_spl),
% 128.36/16.69 inference(contradiction_clause,[status(thm)],[f4328])).
% 128.36/16.69 fof(f4936,plain,(
% 128.36/16.69 ![X0]: (~rless(vf(vd1130,vd1126),X0)|~rreal(X0)|~rreal(vf(vd1130,vd1126))|~rreal(vf(vd1128,vd1130))|rless(vf(vd1128,vd1130),X0))),
% 128.36/16.69 inference(resolution,[status(thm)],[f942,f1115])).
% 128.36/16.69 fof(f4945,definition,(
% 128.36/16.69 ![X0]: (sQ432_spl <=> (~rless(vf(vd1130,vd1126),X0)|~rreal(X0)|rless(vf(vd1128,vd1130),X0)))),
% 128.36/16.69 introduced(definition,[new_symbols(definition,[sQ432_spl])],[split_symbol_definition])).
% 128.36/16.69 fof(f4946,plain,(
% 128.36/16.69 ![X0]: (~rless(vf(vd1130,vd1126),X0)|~rreal(X0)|rless(vf(vd1128,vd1130),X0)|~sQ432_spl)),
% 128.36/16.69 inference(component_clause,[status(thm)],[f4945])).
% 128.36/16.69 fof(f4948,plain,(
% 128.36/16.69 sQ432_spl|~sQ65_spl|~sQ64_spl),
% 128.36/16.69 inference(split_clause,[status(thm)],[f4936,f4945,f1280,f1277])).
% 128.36/16.69 fof(f4963,plain,(
% 128.36/16.69 ~rless(vf(vd1130,vd1126),vf(vd1128,vd1130))|~rreal(vf(vd1128,vd1130))|~rreal(vf(vd1128,vd1130))|~sQ432_spl),
% 128.36/16.69 inference(resolution,[status(thm)],[f4946,f889])).
% 128.36/16.69 fof(f4968,plain,(
% 128.36/16.69 ~sQ63_spl|~sQ64_spl|~sQ432_spl),
% 128.36/16.69 inference(split_clause,[status(thm)],[f4963,f1274,f1277,f4945])).
% 128.36/16.69 fof(f5157,plain,(
% 128.36/16.69 vf(vd1130,vd1126)=sK7_skl(vd1126,vd1130)),
% 128.36/16.69 inference(resolution,[status(thm)],[f1256,f173])).
% 128.36/16.69 fof(f5202,plain,(
% 128.36/16.69 ~rpoint(vd1126)|~rpoint(vd1130)|rreal(vf(vd1130,vd1126))),
% 128.36/16.69 inference(paramodulation,[status(thm)],[f5157,f888])).
% 128.36/16.69 fof(f5203,plain,(
% 128.36/16.69 ~sQ371_spl|~sQ378_spl|sQ65_spl),
% 128.36/16.69 inference(split_clause,[status(thm)],[f5202,f3656,f3680,f1280])).
% 128.36/16.69 fof(f5434,plain,(
% 128.36/16.69 vf(vd1128,vd1130)=sK7_skl(vd1130,vd1128)),
% 128.36/16.69 inference(resolution,[status(thm)],[f1255,f169])).
% 128.36/16.69 fof(f5451,plain,(
% 128.36/16.69 ~rpoint(vd1130)|~rpoint(vd1128)|rreal(vf(vd1128,vd1130))),
% 111.30/16.75 inference(paramodulation,[status(thm)],[f5434,f888])).
% 111.30/16.75 fof(f5452,plain,(
% 111.30/16.75 ~sQ378_spl|~sQ370_spl|sQ64_spl),
% 111.30/16.75 inference(split_clause,[status(thm)],[f5451,f3680,f3653,f1277])).
% 111.30/16.75 fof(f6081,plain,(
% 111.30/16.75 ![X0,X1]: (~ron(X0,vd1152)|~rpoint(X0)|~rpoint(X1)|rless(vf(vd1130,X1),vf(vd1130,X0))|~rinside(X1,vd1152))),
% 111.30/16.75 inference(resolution,[status(thm)],[f868,f1110])).
% 111.30/16.75 fof(f6538,plain,(
% 111.30/16.75 ![X0]: (~ron(X0,vd1152)|~rpoint(X0)|~rpoint(vd1126)|rless(vf(vd1130,vd1126),vf(vd1130,X0)))),
% 111.30/16.75 inference(resolution,[status(thm)],[f6081,f860])).
% 111.30/16.75 fof(f6542,definition,(
% 111.30/16.75 ![X0]: (sQ627_spl <=> (~ron(X0,vd1152)|~rpoint(X0)|rless(vf(vd1130,vd1126),vf(vd1130,X0))))),
% 111.30/16.75 introduced(definition,[new_symbols(definition,[sQ627_spl])],[split_symbol_definition])).
% 111.30/16.75 fof(f6543,plain,(
% 111.30/16.75 ![X0]: (~ron(X0,vd1152)|~rpoint(X0)|rless(vf(vd1130,vd1126),vf(vd1130,X0))|~sQ627_spl)),
% 111.30/16.75 inference(component_clause,[status(thm)],[f6542])).
% 111.30/16.75 fof(f6545,plain,(
% 111.30/16.75 sQ627_spl|~sQ371_spl),
% 111.30/16.75 inference(split_clause,[status(thm)],[f6538,f6542,f3656])).
% 111.30/16.75 fof(f8886,plain,(
% 111.30/16.75 ![X0]: (~rpoint(X0)|vf(vd1130,X0)=vf(X0,vd1130))),
% 111.30/16.75 inference(resolution,[status(thm)],[f1071,f169])).
% 111.30/16.75 fof(f9121,definition,(
% 111.30/16.75 sQ823_spl <=> (ron(vd1128,vd1152))),
% 111.30/16.75 introduced(definition,[new_symbols(definition,[sQ823_spl])],[split_symbol_definition])).
% 111.30/16.75 fof(f9123,plain,(
% 111.30/16.75 ~ron(vd1128,vd1152)|sQ823_spl),
% 111.30/16.75 inference(component_clause,[status(thm)],[f9121])).
% 111.30/16.75 fof(f9136,plain,(
% 111.30/16.75 $false|sQ823_spl),
% 111.30/16.75 inference(forward_subsumption_resolution,[status(thm)],[f9123,f858])).
% 111.30/16.75 fof(f9137,plain,(
% 111.30/16.75 sQ823_spl),
% 111.30/16.75 inference(contradiction_clause,[status(thm)],[f9136])).
% 111.30/16.75 fof(f9530,plain,(
% 111.30/16.75 vf(vd1130,vd1128)=vf(vd1128,vd1130)),
% 111.30/16.75 inference(resolution,[status(thm)],[f8886,f171])).
% 111.30/16.75 fof(f9540,plain,(
% 111.30/16.75 ~rless(vf(vd1130,vd1126),vf(vd1130,vd1128))|sQ63_spl),
% 111.30/16.75 inference(backward_demodulation,[status(thm)],[f9530,f1276])).
% 111.30/16.75 fof(f9635,plain,(
% 111.30/16.75 ~ron(vd1128,vd1152)|~rpoint(vd1128)|sQ63_spl|~sQ627_spl),
% 111.30/16.75 inference(resolution,[status(thm)],[f9540,f6543])).
% 111.30/16.75 fof(f9637,plain,(
% 111.30/16.75 ~sQ823_spl|~sQ370_spl|sQ63_spl|~sQ627_spl),
% 111.30/16.75 inference(split_clause,[status(thm)],[f9635,f9121,f3653,f1274,f6542])).
% 111.30/16.75 fof(f9642,plain,(
% 111.30/16.75 $false),
% 111.30/16.75 inference(sat_refutation,[status(thm)],[f3690,f3917,f4329,f4948,f4968,f5203,f5452,f6545,f9137,f9637])).
% 111.30/16.75 % SZS output end CNFRefutation for theBenchmark.p
% 111.30/16.77 % Elapsed time: 16.404135 seconds
% 111.30/16.77 % CPU time: 129.565055 seconds
% 111.30/16.77 % Total memory used: 585.971 MB
% 111.30/16.77 % Net memory used: 542.851 MB
%------------------------------------------------------------------------------