%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO282+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 : n006.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 68.69s 9.12s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO282+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.37 % Computer : n006.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8046.5625MB
% 0.13/0.37 % OS : Linux 6.8.0-71-generic
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Sun Sep 20 15:04:58 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.41 % Drodi V4.1.1
% 68.69/9.12 % Refutation found
% 68.69/9.12 % SZS status Theorem for theBenchmark: Theorem is valid
% 68.69/9.12 % SZS output start CNFRefutation for theBenchmark
% 68.69/9.12 fof(f1,conjecture,(
% 68.69/9.12 ~ rinside(vd1125,vd1146) ),
% 68.69/9.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 68.69/9.12 fof(f2,negated_conjecture,(
% 68.69/9.12 ~(~ rinside(vd1125,vd1146) )),
% 68.69/9.12 inference(negated_conjecture,[status(cth)],[f1])).
% 68.69/9.12 fof(f3,axiom,(
% 68.69/9.12 ( ron(vd1129,vd1146)& rcenter(vd1123,vd1146)& rcircle(vd1146)& ron(vd1125,vd1145)& ron(vd1123,vd1145) ) ),
% 68.69/9.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 68.69/9.12 fof(f5,axiom,(
% 68.69/9.12 vd1123 = vd1127 ),
% 68.69/9.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 68.69/9.12 fof(f18,axiom,(
% 68.69/9.12 ( 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) ) ),
% 68.69/9.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 68.69/9.12 fof(f21,axiom,(
% 68.69/9.12 (! [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) ) ) )),
% 68.69/9.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 68.69/9.12 fof(f23,axiom,(
% 68.69/9.12 (! [Vd741,Vd742] :( ( (? [Vd745] :( Vd742 = Vd745& rpoint(Vd745) ))& (? [Vd744] :( Vd741 = Vd744& rpoint(Vd744) ) ))=> (? [Vd747] :( vf(Vd741,Vd742) = Vd747& rreal(Vd747) ) )) )),
% 68.69/9.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 68.69/9.12 fof(f24,axiom,(
% 68.69/9.12 (! [Vd713,Vd714] :( ( Vd713 = Vd714& rreal(Vd714) )=> ~ rless(Vd713,Vd713) ) )),
% 68.69/9.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 68.69/9.12 fof(f45,axiom,(
% 68.69/9.12 (! [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) ) )),
% 68.69/9.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 68.69/9.12 fof(f126,plain,(
% 68.69/9.12 rinside(vd1125,vd1146)),
% 68.69/9.12 inference(cnf_transformation,[status(thm)],[f2])).
% 68.69/9.12 fof(f127,plain,(
% 68.69/9.12 ron(vd1129,vd1146)),
% 68.69/9.12 inference(cnf_transformation,[status(thm)],[f3])).
% 68.69/9.12 fof(f128,plain,(
% 68.69/9.12 rcenter(vd1123,vd1146)),
% 68.69/9.12 inference(cnf_transformation,[status(thm)],[f3])).
% 68.69/9.12 fof(f133,plain,(
% 68.69/9.12 vd1123=vd1127),
% 68.69/9.12 inference(cnf_transformation,[status(thm)],[f5])).
% 68.69/9.12 fof(f162,plain,(
% 68.69/9.12 rless(vf(vd1127,vd1129),vf(vd1123,vd1125))),
% 68.69/9.12 inference(cnf_transformation,[status(thm)],[f18])).
% 68.69/9.12 fof(f165,plain,(
% 68.69/9.12 vd1129=vd1130),
% 68.69/9.12 inference(cnf_transformation,[status(thm)],[f18])).
% 68.69/9.12 fof(f166,plain,(
% 68.69/9.12 rpoint(vd1130)),
% 68.69/9.12 inference(cnf_transformation,[status(thm)],[f18])).
% 68.69/9.12 fof(f167,plain,(
% 68.69/9.12 vd1127=vd1128),
% 68.69/9.12 inference(cnf_transformation,[status(thm)],[f18])).
% 68.69/9.12 fof(f168,plain,(
% 68.69/9.12 rpoint(vd1128)),
% 68.69/9.12 inference(cnf_transformation,[status(thm)],[f18])).
% 68.69/9.12 fof(f169,plain,(
% 68.69/9.12 vd1125=vd1126),
% 68.69/9.12 inference(cnf_transformation,[status(thm)],[f18])).
% 68.69/9.12 fof(f170,plain,(
% 68.69/9.12 rpoint(vd1126)),
% 68.69/9.12 inference(cnf_transformation,[status(thm)],[f18])).
% 68.69/9.12 fof(f183,plain,(
% 68.69/9.12 ![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)))),
% 68.69/9.12 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 68.69/9.12 fof(f184,plain,(
% 68.69/9.12 ![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))))),
% 68.69/9.12 inference(NNF_transformation,[status(thm)],[f183])).
% 68.69/9.12 fof(f186,plain,(
% 68.69/9.12 ![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))),
% 68.69/9.12 inference(cnf_transformation,[status(thm)],[f184])).
% 68.69/9.12 fof(f192,plain,(
% 68.69/9.12 ![Vd741,Vd742]: (((![Vd745]: (~Vd742=Vd745|~rpoint(Vd745)))|(![Vd744]: (~Vd741=Vd744|~rpoint(Vd744))))|(?[Vd747]: (vf(Vd741,Vd742)=Vd747&rreal(Vd747))))),
% 68.69/9.12 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 68.69/9.12 fof(f193,plain,(
% 68.69/9.12 ![Vd741,Vd742]: (((![Vd745]: (~Vd742=Vd745|~rpoint(Vd745)))|(![Vd744]: (~Vd741=Vd744|~rpoint(Vd744))))|(vf(Vd741,Vd742)=sK2_skl(Vd742,Vd741)&rreal(sK2_skl(Vd742,Vd741))))),
% 68.69/9.12 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Vd747,sK2_skl(Vd742,Vd741))],[f192])).
% 68.69/9.12 fof(f194,plain,(
% 68.69/9.12 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|vf(X2,X0)=sK2_skl(X0,X2))),
% 68.69/9.12 inference(cnf_transformation,[status(thm)],[f193])).
% 68.69/9.12 fof(f195,plain,(
% 68.69/9.12 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|rreal(sK2_skl(X0,X2)))),
% 68.69/9.12 inference(cnf_transformation,[status(thm)],[f193])).
% 68.69/9.12 fof(f196,plain,(
% 68.69/9.12 ![Vd713,Vd714]: ((~Vd713=Vd714|~rreal(Vd714))|~rless(Vd713,Vd713))),
% 68.69/9.12 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 68.69/9.12 fof(f197,plain,(
% 68.69/9.12 ![Vd713]: ((![Vd714]: (~Vd713=Vd714|~rreal(Vd714)))|~rless(Vd713,Vd713))),
% 68.69/9.12 inference(miniscoping,[status(thm)],[f196])).
% 68.69/9.12 fof(f198,plain,(
% 68.69/9.12 ![X0,X1]: (~X0=X1|~rreal(X1)|~rless(X0,X0))),
% 68.69/9.12 inference(cnf_transformation,[status(thm)],[f197])).
% 68.69/9.12 fof(f277,plain,(
% 68.69/9.12 ![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))),
% 68.69/9.12 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 68.69/9.12 fof(f278,plain,(
% 68.69/9.12 ![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))),
% 68.69/9.12 inference(miniscoping,[status(thm)],[f277])).
% 68.69/9.12 fof(f279,plain,(
% 68.69/9.12 ![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))),
% 68.69/9.12 inference(cnf_transformation,[status(thm)],[f278])).
% 68.69/9.12 fof(f675,plain,(
% 68.69/9.12 ![X0,X1,X2,X3]: (~ron(X0,X1)|~rcenter(X2,X1)|~rpoint(X0)|~rpoint(X3)|rless(vf(X2,X3),vf(X2,X0))|~rinside(X3,X1))),
% 68.69/9.12 inference(destructive_equality_resolution,[status(thm)],[f186])).
% 68.69/9.12 fof(f678,plain,(
% 68.69/9.12 ![X0,X1]: (~rpoint(X0)|~rpoint(X1)|vf(X1,X0)=sK2_skl(X0,X1))),
% 68.69/9.12 inference(destructive_equality_resolution,[status(thm)],[f194])).
% 68.69/9.12 fof(f679,plain,(
% 68.69/9.12 ![X0,X1]: (~rpoint(X0)|~rpoint(X1)|rreal(sK2_skl(X0,X1)))),
% 68.69/9.12 inference(destructive_equality_resolution,[status(thm)],[f195])).
% 68.69/9.12 fof(f680,plain,(
% 68.69/9.12 ![X0]: (~rreal(X0)|~rless(X0,X0))),
% 68.69/9.12 inference(destructive_equality_resolution,[status(thm)],[f198])).
% 68.69/9.12 fof(f717,plain,(
% 68.69/9.12 ![X0,X1,X2]: (~rless(X0,X1)|~rless(X2,X0)|~rreal(X1)|~rreal(X0)|~rreal(X2)|rless(X2,X1))),
% 68.69/9.12 inference(destructive_equality_resolution,[status(thm)],[f279])).
% 68.69/9.12 fof(f887,plain,(
% 68.69/9.12 rless(vf(vd1123,vd1129),vf(vd1123,vd1125))),
% 68.69/9.12 inference(backward_demodulation,[status(thm)],[f133,f162])).
% 68.69/9.12 fof(f891,plain,(
% 68.69/9.12 rpoint(vd1129)),
% 68.69/9.12 inference(forward_demodulation,[status(thm)],[f165,f166])).
% 68.69/9.12 fof(f893,plain,(
% 68.69/9.12 vd1123=vd1128),
% 68.69/9.12 inference(forward_demodulation,[status(thm)],[f133,f167])).
% 68.69/9.12 fof(f896,plain,(
% 68.69/9.12 rpoint(vd1123)),
% 68.69/9.12 inference(forward_demodulation,[status(thm)],[f893,f168])).
% 68.69/9.12 fof(f898,plain,(
% 68.69/9.12 rpoint(vd1125)),
% 68.69/9.12 inference(forward_demodulation,[status(thm)],[f169,f170])).
% 68.69/9.12 fof(f2603,plain,(
% 68.69/9.12 ![X0,X1]: (~rcenter(X0,vd1146)|~rpoint(vd1129)|~rpoint(X1)|rless(vf(X0,X1),vf(X0,vd1129))|~rinside(X1,vd1146))),
% 68.69/9.12 inference(resolution,[status(thm)],[f675,f127])).
% 68.69/9.12 fof(f2608,plain,(
% 68.69/9.12 ![X0,X1]: (~rcenter(X0,vd1146)|~rpoint(X1)|rless(vf(X0,X1),vf(X0,vd1129))|~rinside(X1,vd1146))),
% 68.69/9.12 inference(forward_subsumption_resolution,[status(thm)],[f2603,f891])).
% 68.69/9.12 fof(f2714,plain,(
% 68.69/9.12 ![X0]: (~rpoint(X0)|rless(vf(vd1123,X0),vf(vd1123,vd1129))|~rinside(X0,vd1146))),
% 68.69/9.12 inference(resolution,[status(thm)],[f2608,f128])).
% 68.69/9.12 fof(f2848,plain,(
% 68.69/9.12 ![X0]: (~rpoint(X0)|rreal(sK2_skl(vd1125,X0)))),
% 68.69/9.12 inference(resolution,[status(thm)],[f679,f898])).
% 68.69/9.12 fof(f2850,plain,(
% 68.69/9.12 ![X0]: (~rpoint(X0)|rreal(sK2_skl(vd1129,X0)))),
% 68.69/9.12 inference(resolution,[status(thm)],[f679,f891])).
% 68.69/9.12 fof(f2943,plain,(
% 68.69/9.12 rreal(sK2_skl(vd1125,vd1123))),
% 68.69/9.12 inference(resolution,[status(thm)],[f2848,f896])).
% 68.69/9.12 fof(f3010,plain,(
% 68.69/9.12 ![X0]: (~rpoint(X0)|vf(X0,vd1125)=sK2_skl(vd1125,X0))),
% 68.69/9.12 inference(resolution,[status(thm)],[f678,f898])).
% 68.69/9.16 fof(f3012,plain,(
% 68.69/9.16 ![X0]: (~rpoint(X0)|vf(X0,vd1129)=sK2_skl(vd1129,X0))),
% 68.69/9.16 inference(resolution,[status(thm)],[f678,f891])).
% 68.69/9.16 fof(f3303,plain,(
% 68.69/9.16 rreal(sK2_skl(vd1129,vd1123))),
% 68.69/9.16 inference(resolution,[status(thm)],[f2850,f896])).
% 68.69/9.16 fof(f16659,plain,(
% 68.69/9.16 ~rpoint(vd1125)|rless(vf(vd1123,vd1125),vf(vd1123,vd1129))),
% 68.69/9.16 inference(resolution,[status(thm)],[f2714,f126])).
% 68.69/9.16 fof(f16663,plain,(
% 68.69/9.16 rless(vf(vd1123,vd1125),vf(vd1123,vd1129))),
% 68.69/9.16 inference(forward_subsumption_resolution,[status(thm)],[f16659,f898])).
% 68.69/9.16 fof(f17349,plain,(
% 68.69/9.16 ![X0]: (~rless(X0,vf(vd1123,vd1125))|~rreal(vf(vd1123,vd1129))|~rreal(vf(vd1123,vd1125))|~rreal(X0)|rless(X0,vf(vd1123,vd1129)))),
% 68.69/9.16 inference(resolution,[status(thm)],[f717,f16663])).
% 68.69/9.16 fof(f17674,plain,(
% 68.69/9.16 ~rreal(vf(vd1123,vd1129))|~rreal(vf(vd1123,vd1125))|~rreal(vf(vd1123,vd1129))|rless(vf(vd1123,vd1129),vf(vd1123,vd1129))),
% 68.69/9.16 inference(resolution,[status(thm)],[f17349,f887])).
% 68.69/9.16 fof(f17675,plain,(
% 68.69/9.16 ~rreal(vf(vd1123,vd1129))|~rreal(vf(vd1123,vd1125))|rless(vf(vd1123,vd1129),vf(vd1123,vd1129))),
% 68.69/9.16 inference(duplicate_literals_removal,[status(thm)],[f17674])).
% 68.69/9.16 fof(f17676,plain,(
% 68.69/9.16 ~rreal(vf(vd1123,vd1129))|~rreal(vf(vd1123,vd1125))),
% 68.69/9.16 inference(forward_subsumption_resolution,[status(thm)],[f17675,f680])).
% 68.69/9.16 fof(f77660,plain,(
% 68.69/9.16 vf(vd1123,vd1125)=sK2_skl(vd1125,vd1123)),
% 68.69/9.16 inference(resolution,[status(thm)],[f3010,f896])).
% 68.69/9.16 fof(f77675,plain,(
% 68.69/9.16 rreal(vf(vd1123,vd1125))),
% 68.69/9.16 inference(backward_demodulation,[status(thm)],[f77660,f2943])).
% 68.69/9.16 fof(f77676,plain,(
% 68.69/9.16 ~rreal(vf(vd1123,vd1129))),
% 68.69/9.16 inference(backward_subsumption_resolution,[status(thm)],[f17676,f77675])).
% 68.69/9.16 fof(f79025,plain,(
% 68.69/9.16 vf(vd1123,vd1129)=sK2_skl(vd1129,vd1123)),
% 68.69/9.16 inference(resolution,[status(thm)],[f3012,f896])).
% 68.69/9.16 fof(f80698,plain,(
% 68.69/9.16 rreal(vf(vd1123,vd1129))),
% 68.69/9.16 inference(backward_demodulation,[status(thm)],[f79025,f3303])).
% 68.69/9.16 fof(f80699,plain,(
% 68.69/9.16 $false),
% 68.69/9.16 inference(forward_subsumption_resolution,[status(thm)],[f80698,f77676])).
% 68.69/9.16 % SZS output end CNFRefutation for theBenchmark.p
% 68.69/9.17 % Elapsed time: 8.778970 seconds
% 68.69/9.17 % CPU time: 69.060431 seconds
% 68.69/9.17 % Total memory used: 418.201 MB
% 68.69/9.17 % Net memory used: 394.237 MB
%------------------------------------------------------------------------------